cprover
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:
62  };
63 
65  {
66  public:
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  std::set<exprt> symbols;
81 
82  find_symbols(expr, symbols);
83 
84  replace_symbolt replace_symbol;
85 
86  for(std::set<exprt>::const_iterator
87  s_it=symbols.begin();
88  s_it!=symbols.end();
89  s_it++)
90  {
91  if(s_it->id()==ID_symbol)
92  {
93  const symbol_exprt &s = to_symbol_expr(*s_it);
94 
95  shared_varst::const_iterator v_it = shared_vars.find(s.get_identifier());
96 
97  if(v_it!=shared_vars.end())
98  {
100  // not yet done: neither array_symbol nor w_index_symbol are actually
101  // initialized anywhere
102  const shared_vart &shared_var = v_it->second;
103  const index_exprt new_expr(
104  shared_var.array_symbol, shared_var.w_index_symbol);
105 
106  replace_symbol.insert(s, new_expr);
107  }
108  }
109  }
110 }
111 
113  goto_programt &goto_program)
114 {
115  for(goto_programt::instructionst::iterator
116  it=goto_program.instructions.begin();
117  it!=goto_program.instructions.end();
118  it++)
119  {
120  if(it->is_assign())
121  {
122  code_assignt &code=to_code_assign(it->code);
123  instrument(code.rhs());
124  }
125  else if(it->is_assume() || it->is_assert() || it->is_goto())
126  instrument(it->guard);
127  else if(it->is_function_call())
128  {
130  instrument(code.function());
131 
132  // instrument(code.lhs(), LHS);
133  for(auto &arg : code.arguments())
134  instrument(arg);
135  }
136  }
137 }
138 
140 {
141  std::set<exprt> symbols;
142 
143  find_symbols(expr, symbols);
144 
145  for(std::set<exprt>::const_iterator
146  s_it=symbols.begin();
147  s_it!=symbols.end();
148  s_it++)
149  {
150  if(s_it->id()==ID_symbol)
151  {
152  const irep_idt identifier=
154 
156  const symbolt &symbol=ns.lookup(identifier);
157 
158  if(!symbol.is_state_var)
159  continue;
160 
161  if(symbol.is_thread_local)
162  {
163  if(thread_local_vars.find(identifier)!=thread_local_vars.end())
164  continue;
165 
166  thread_local_vart &thread_local_var=thread_local_vars[identifier];
167  thread_local_var.type=symbol.type;
168  }
169  else
170  {
171  if(shared_vars.find(identifier)!=shared_vars.end())
172  continue;
173 
174  shared_vart &shared_var=shared_vars[identifier];
175  shared_var.type=symbol.type;
176  }
177  }
178  }
179 }
180 
182  const goto_programt &goto_program,
183  const is_threadedt &is_threaded)
184 {
185  forall_goto_program_instructions(i_it, goto_program)
186  {
187  if(is_threaded(i_it))
188  {
189  if(i_it->is_assign())
190  collect(i_it->code);
191  else if(i_it->is_assume() || i_it->is_assert() || i_it->is_goto())
192  collect(i_it->guard);
193  else if(i_it->is_function_call())
194  collect(i_it->code);
195  }
196  }
197 }
198 
200 {
201 // for(
202 }
203 
205  goto_functionst &goto_functions)
206 {
208  is_threadedt is_threaded(goto_functions);
209 
210  // this first collects all shared and thread-local variables
211  forall_goto_functions(f_it, goto_functions)
212  collect(f_it->second.body, is_threaded);
213 
214  // add array symbols
216 
217  // now instrument
218  Forall_goto_functions(f_it, goto_functions)
219  instrument(f_it->second.body);
220 }
221 
223  value_setst &value_sets,
224  goto_modelt &goto_model)
225 {
226  concurrency_instrumentationt concurrency_instrumentation(
227  value_sets, goto_model.symbol_table);
228  concurrency_instrumentation(goto_model.goto_functions);
229 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
concurrency_instrumentationt::thread_local_vars
thread_local_varst thread_local_vars
Definition: concurrency.cpp:75
concurrency.h
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:61
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
concurrency_instrumentationt::shared_varst
std::map< irep_idt, shared_vart > shared_varst
Definition: concurrency.cpp:71
concurrency_instrumentationt::shared_vart::w_index_symbol
symbol_exprt w_index_symbol
Definition: concurrency.cpp:61
concurrency_instrumentationt::add_array_symbols
void add_array_symbols()
Definition: concurrency.cpp:199
typet
The type of an expression, extends irept.
Definition: type.h:27
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
concurrency
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Definition: concurrency.cpp:222
concurrency_instrumentationt::thread_local_vart::type
typet type
Definition: concurrency.cpp:67
replace_symbol.h
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
invariant.h
concurrency_instrumentationt::thread_local_vart
Definition: concurrency.cpp:64
concurrency_instrumentationt::collect
void collect(const goto_programt &goto_program, const is_threadedt &is_threaded)
Definition: concurrency.cpp:181
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
concurrency_instrumentationt::shared_vars
shared_varst shared_vars
Definition: concurrency.cpp:72
is_threadedt
Definition: is_threaded.h:21
concurrency_instrumentationt::operator()
void operator()(goto_functionst &goto_functions)
Definition: concurrency.cpp:34
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:16
find_symbols.h
concurrency_instrumentationt::instrument
void instrument(goto_functionst &goto_functions)
Definition: concurrency.cpp:204
concurrency_instrumentationt::symbol_table
symbol_tablet & symbol_table
Definition: concurrency.cpp:41
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
concurrency_instrumentationt::concurrency_instrumentationt
concurrency_instrumentationt(value_setst &_value_sets, symbol_tablet &_symbol_table)
Definition: concurrency.cpp:26
is_threaded.h
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
concurrency_instrumentationt::shared_vart
Definition: concurrency.cpp:57
concurrency_instrumentationt::shared_vart::type
typet type
Definition: concurrency.cpp:60
concurrency_instrumentationt::shared_vart::array_symbol
symbol_exprt array_symbol
Definition: concurrency.cpp:61
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
replace_symbolt::insert
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...
Definition: replace_symbol.cpp:24
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1109
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
value_setst
Definition: value_sets.h:21
concurrency_instrumentationt::value_sets
value_setst & value_sets
Definition: concurrency.cpp:40
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:497
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
symbolt
Symbol table entry.
Definition: symbol.h:27
concurrency_instrumentationt::thread_local_vart::array_symbol
symbol_exprt array_symbol
Definition: concurrency.cpp:68
concurrency_instrumentationt::thread_local_varst
std::map< irep_idt, thread_local_vart > thread_local_varst
Definition: concurrency.cpp:74
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
index_exprt
Array index operator.
Definition: std_expr.h:1595
concurrency_instrumentationt
Definition: concurrency.cpp:23
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
std_expr.h
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:24