CBMC
concurrency.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Encoding for Threaded Goto Programs
4 
5 Author: Daniel Kroening
6 
7 Date: October 2012
8 
9 \*******************************************************************/
10 
13 
14 #include "concurrency.h"
15 
16 #include <util/find_symbols.h>
17 #include <util/invariant.h>
18 #include <util/replace_symbol.h>
19 #include <util/std_expr.h>
20 
21 #include <analyses/is_threaded.h>
22 
24 {
25 public:
27  value_setst &_value_sets,
28  symbol_tablet &_symbol_table):
29  value_sets(_value_sets),
30  symbol_table(_symbol_table)
31  {
32  }
33 
34  void operator()(goto_functionst &goto_functions)
35  {
36  instrument(goto_functions);
37  }
38 
39 protected:
42 
43  void instrument(goto_functionst &goto_functions);
44 
45  void instrument(goto_programt &goto_program);
46 
47  void instrument(exprt &expr);
48 
49  void collect(
50  const goto_programt &goto_program,
51  const is_threadedt &is_threaded);
52 
53  void collect(const exprt &expr);
54 
55  void add_array_symbols();
56 
58  {
59  public:
61  std::optional<symbol_exprt> array_symbol, w_index_symbol;
62  };
63 
65  {
66  public:
68  std::optional<symbol_exprt> array_symbol;
69  };
70 
71  typedef std::map<irep_idt, shared_vart> shared_varst;
73 
74  typedef std::map<irep_idt, thread_local_vart> thread_local_varst;
76 };
77 
79 {
80  replace_symbolt replace_symbol;
81 
82  for(const symbol_exprt &s : find_symbols(expr))
83  {
84  shared_varst::const_iterator v_it = shared_vars.find(s.get_identifier());
85 
86  if(v_it != shared_vars.end())
87  {
89  // not yet done: neither array_symbol nor w_index_symbol are actually
90  // initialized anywhere
91  const shared_vart &shared_var = v_it->second;
92  const index_exprt new_expr(
93  *shared_var.array_symbol, *shared_var.w_index_symbol);
94 
95  replace_symbol.insert(s, new_expr);
96  }
97  }
98 }
99 
101  goto_programt &goto_program)
102 {
103  for(goto_programt::instructionst::iterator
104  it=goto_program.instructions.begin();
105  it!=goto_program.instructions.end();
106  it++)
107  {
108  if(it->is_assign())
109  {
110  instrument(it->assign_rhs_nonconst());
111  }
112  else if(it->is_assume() || it->is_assert() || it->is_goto())
113  {
114  instrument(it->condition_nonconst());
115  }
116  else if(it->is_function_call())
117  {
118  code_function_callt &code = to_code_function_call(it->code_nonconst());
119  instrument(code.function());
120 
121  // instrument(code.lhs(), LHS);
122  for(auto &arg : code.arguments())
123  instrument(arg);
124  }
125  }
126 }
127 
129 {
130  for(const auto &identifier : find_symbol_identifiers(expr))
131  {
133  const symbolt &symbol = ns.lookup(identifier);
134 
135  if(!symbol.is_state_var)
136  continue;
137 
138  if(symbol.is_thread_local)
139  {
140  if(thread_local_vars.find(identifier) != thread_local_vars.end())
141  continue;
142 
143  thread_local_vart &thread_local_var = thread_local_vars[identifier];
144  thread_local_var.type = symbol.type;
145  }
146  else
147  {
148  if(shared_vars.find(identifier) != shared_vars.end())
149  continue;
150 
151  shared_vart &shared_var = shared_vars[identifier];
152  shared_var.type = symbol.type;
153  }
154  }
155 }
156 
158  const goto_programt &goto_program,
159  const is_threadedt &is_threaded)
160 {
161  forall_goto_program_instructions(i_it, goto_program)
162  {
163  if(is_threaded(i_it))
164  i_it->apply([this](const exprt &e) { collect(e); });
165  }
166 }
167 
169 {
170 // for(
171 }
172 
174  goto_functionst &goto_functions)
175 {
177  is_threadedt is_threaded(goto_functions);
178 
179  // this first collects all shared and thread-local variables
180  for(const auto &gf_entry : goto_functions.function_map)
181  collect(gf_entry.second.body, is_threaded);
182 
183  // add array symbols
185 
186  // now instrument
187  for(auto &gf_entry : goto_functions.function_map)
188  instrument(gf_entry.second.body);
189 }
190 
192  value_setst &value_sets,
193  goto_modelt &goto_model)
194 {
195  concurrency_instrumentationt concurrency_instrumentation(
196  value_sets, goto_model.symbol_table);
197  concurrency_instrumentation(goto_model.goto_functions);
198 }
goto_instruction_codet representation of a function call statement.
std::optional< symbol_exprt > array_symbol
Definition: concurrency.cpp:61
std::optional< symbol_exprt > w_index_symbol
Definition: concurrency.cpp:61
std::optional< symbol_exprt > array_symbol
Definition: concurrency.cpp:68
void collect(const goto_programt &goto_program, const is_threadedt &is_threaded)
void operator()(goto_functionst &goto_functions)
Definition: concurrency.cpp:34
concurrency_instrumentationt(value_setst &_value_sets, symbol_tablet &_symbol_table)
Definition: concurrency.cpp:26
std::map< irep_idt, thread_local_vart > thread_local_varst
Definition: concurrency.cpp:74
thread_local_varst thread_local_vars
Definition: concurrency.cpp:75
void instrument(goto_functionst &goto_functions)
symbol_tablet & symbol_table
Definition: concurrency.cpp:41
std::map< irep_idt, shared_vart > shared_varst
Definition: concurrency.cpp:71
Base class for all expressions.
Definition: expr.h:56
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
Array index operator.
Definition: std_expr.h:1465
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
Replace a symbol expression by a given expression.
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
bool is_thread_local
Definition: symbol.h:71
bool is_state_var
Definition: symbol.h:66
typet type
Type of symbol.
Definition: symbol.h:31
The type of an expression, extends irept.
Definition: type.h:29
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Encoding for Threaded Goto Programs.
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
find_symbols_sett find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol, considering both free and bound variables.
Definition: find_symbols.h:53
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
#define forall_goto_program_instructions(it, program)
Over-approximate Concurrency for Threaded Goto Programs.
#define UNIMPLEMENTED
Definition: invariant.h:558
API to expression classes.