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 }
The type of an expression, extends irept.
Definition: type.h:27
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...
Over-approximate Concurrency for Threaded Goto Programs.
concurrency_instrumentationt(value_setst &_value_sets, symbol_tablet &_symbol_table)
Definition: concurrency.cpp:26
bool is_thread_local
Definition: symbol.h:65
void instrument(goto_functionst &goto_functions)
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
const irep_idt & get_identifier() const
Definition: std_expr.h:176
symbol_tablet & symbol_table
Definition: concurrency.cpp:41
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
std::map< irep_idt, thread_local_vart > thread_local_varst
Definition: concurrency.cpp:74
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
argumentst & arguments()
Definition: std_code.h:1109
Replace expression or type symbols by an expression or type, respectively.
exprt & rhs()
Definition: std_code.h:274
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
thread_local_varst thread_local_vars
Definition: concurrency.cpp:75
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
void operator()(goto_functionst &goto_functions)
Definition: concurrency.cpp:34
typet type
Type of symbol.
Definition: symbol.h:31
#define UNIMPLEMENTED
Definition: invariant.h:497
exprt & function()
Definition: std_code.h:1099
Base class for all expressions.
Definition: expr.h:54
bool is_state_var
Definition: symbol.h:61
std::map< irep_idt, shared_vart > shared_varst
Definition: concurrency.cpp:71
#define Forall_goto_functions(it, functions)
void collect(const goto_programt &goto_program, const is_threadedt &is_threaded)
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Encoding for Threaded Goto Programs.
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
void find_symbols(const exprt &src, find_symbols_sett &dest)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
Array index operator.
Definition: std_expr.h:1595