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/optional.h>
19 #include <util/replace_symbol.h>
20 #include <util/std_expr.h>
21 
22 #include <analyses/is_threaded.h>
23 
25 {
26 public:
28  value_setst &_value_sets,
29  symbol_tablet &_symbol_table):
30  value_sets(_value_sets),
31  symbol_table(_symbol_table)
32  {
33  }
34 
35  void operator()(goto_functionst &goto_functions)
36  {
37  instrument(goto_functions);
38  }
39 
40 protected:
43 
44  void instrument(goto_functionst &goto_functions);
45 
46  void instrument(goto_programt &goto_program);
47 
48  void instrument(exprt &expr);
49 
50  void collect(
51  const goto_programt &goto_program,
52  const is_threadedt &is_threaded);
53 
54  void collect(const exprt &expr);
55 
56  void add_array_symbols();
57 
59  {
60  public:
63  };
64 
66  {
67  public:
70  };
71 
72  typedef std::map<irep_idt, shared_vart> shared_varst;
74 
75  typedef std::map<irep_idt, thread_local_vart> thread_local_varst;
77 };
78 
80 {
81  replace_symbolt replace_symbol;
82 
83  for(const symbol_exprt &s : find_symbols(expr))
84  {
85  shared_varst::const_iterator v_it = shared_vars.find(s.get_identifier());
86 
87  if(v_it != shared_vars.end())
88  {
90  // not yet done: neither array_symbol nor w_index_symbol are actually
91  // initialized anywhere
92  const shared_vart &shared_var = v_it->second;
93  const index_exprt new_expr(
94  *shared_var.array_symbol, *shared_var.w_index_symbol);
95 
96  replace_symbol.insert(s, new_expr);
97  }
98  }
99 }
100 
102  goto_programt &goto_program)
103 {
104  for(goto_programt::instructionst::iterator
105  it=goto_program.instructions.begin();
106  it!=goto_program.instructions.end();
107  it++)
108  {
109  if(it->is_assign())
110  {
111  code_assignt &code=to_code_assign(it->code);
112  instrument(code.rhs());
113  }
114  else if(it->is_assume() || it->is_assert() || it->is_goto())
115  {
116  exprt cond = it->get_condition();
117  instrument(cond);
118  it->set_condition(cond);
119  }
120  else if(it->is_function_call())
121  {
123  instrument(code.function());
124 
125  // instrument(code.lhs(), LHS);
126  for(auto &arg : code.arguments())
127  instrument(arg);
128  }
129  }
130 }
131 
133 {
134  for(const auto &identifier : find_symbol_identifiers(expr))
135  {
137  const symbolt &symbol = ns.lookup(identifier);
138 
139  if(!symbol.is_state_var)
140  continue;
141 
142  if(symbol.is_thread_local)
143  {
144  if(thread_local_vars.find(identifier) != thread_local_vars.end())
145  continue;
146 
147  thread_local_vart &thread_local_var = thread_local_vars[identifier];
148  thread_local_var.type = symbol.type;
149  }
150  else
151  {
152  if(shared_vars.find(identifier) != shared_vars.end())
153  continue;
154 
155  shared_vart &shared_var = shared_vars[identifier];
156  shared_var.type = symbol.type;
157  }
158  }
159 }
160 
162  const goto_programt &goto_program,
163  const is_threadedt &is_threaded)
164 {
165  forall_goto_program_instructions(i_it, goto_program)
166  {
167  if(is_threaded(i_it))
168  i_it->apply([this](const exprt &e) { collect(e); });
169  }
170 }
171 
173 {
174 // for(
175 }
176 
178  goto_functionst &goto_functions)
179 {
181  is_threadedt is_threaded(goto_functions);
182 
183  // this first collects all shared and thread-local variables
184  forall_goto_functions(f_it, goto_functions)
185  collect(f_it->second.body, is_threaded);
186 
187  // add array symbols
189 
190  // now instrument
191  Forall_goto_functions(f_it, goto_functions)
192  instrument(f_it->second.body);
193 }
194 
196  value_setst &value_sets,
197  goto_modelt &goto_model)
198 {
199  concurrency_instrumentationt concurrency_instrumentation(
200  value_sets, goto_model.symbol_table);
201  concurrency_instrumentation(goto_model.goto_functions);
202 }
concurrency_instrumentationt::thread_local_vars
thread_local_varst thread_local_vars
Definition: concurrency.cpp:76
concurrency.h
Encoding for Threaded Goto Programs.
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
concurrency_instrumentationt::shared_varst
std::map< irep_idt, shared_vart > shared_varst
Definition: concurrency.cpp:72
concurrency_instrumentationt::shared_vart::w_index_symbol
optionalt< symbol_exprt > w_index_symbol
Definition: concurrency.cpp:62
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:523
concurrency_instrumentationt::add_array_symbols
void add_array_symbols()
Definition: concurrency.cpp:172
typet
The type of an expression, extends irept.
Definition: type.h:29
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
optional.h
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:195
find_symbol_identifiers
std::unordered_set< irep_idt > find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol.
Definition: find_symbols.cpp:91
concurrency_instrumentationt::thread_local_vart::type
typet type
Definition: concurrency.cpp:68
replace_symbol.h
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
concurrency_instrumentationt::thread_local_vart
Definition: concurrency.cpp:66
concurrency_instrumentationt::collect
void collect(const goto_programt &goto_program, const is_threadedt &is_threaded)
Definition: concurrency.cpp:161
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
concurrency_instrumentationt::shared_vars
shared_varst shared_vars
Definition: concurrency.cpp:73
is_threadedt
Definition: is_threaded.h:22
concurrency_instrumentationt::operator()
void operator()(goto_functionst &goto_functions)
Definition: concurrency.cpp:35
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
find_symbols.h
concurrency_instrumentationt::instrument
void instrument(goto_functionst &goto_functions)
Definition: concurrency.cpp:177
concurrency_instrumentationt::symbol_table
symbol_tablet & symbol_table
Definition: concurrency.cpp:42
concurrency_instrumentationt::concurrency_instrumentationt
concurrency_instrumentationt(value_setst &_value_sets, symbol_tablet &_symbol_table)
Definition: concurrency.cpp:27
concurrency_instrumentationt::thread_local_vart::array_symbol
optionalt< symbol_exprt > array_symbol
Definition: concurrency.cpp:69
is_threaded.h
Over-approximate Concurrency for Threaded Goto Programs.
concurrency_instrumentationt::shared_vart
Definition: concurrency.cpp:59
concurrency_instrumentationt::shared_vart::type
typet type
Definition: concurrency.cpp:61
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
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
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest, bool current, bool next)
Add to the set dest the sub-expressions of src with id ID_symbol if current is true,...
Definition: find_symbols.cpp:23
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
value_setst
Definition: value_sets.h:22
concurrency_instrumentationt::value_sets
value_setst & value_sets
Definition: concurrency.cpp:41
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
symbolt
Symbol table entry.
Definition: symbol.h:28
concurrency_instrumentationt::thread_local_varst
std::map< irep_idt, thread_local_vart > thread_local_varst
Definition: concurrency.cpp:75
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
index_exprt
Array index operator.
Definition: std_expr.h:1293
concurrency_instrumentationt
Definition: concurrency.cpp:25
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
std_expr.h
API to expression classes.
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
concurrency_instrumentationt::shared_vart::array_symbol
optionalt< symbol_exprt > array_symbol
Definition: concurrency.cpp:62
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25