cprover
concurrency.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Encoding for Threaded Goto Programs
4
5Author: Daniel Kroening
6
7Date: 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
23
25{
26public:
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
40protected:
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 instrument(it->assign_rhs_nonconst());
112 }
113 else if(it->is_assume() || it->is_assert() || it->is_goto())
114 {
115 instrument(it->condition_nonconst());
116 }
117 else if(it->is_function_call())
118 {
119 code_function_callt &code = to_code_function_call(it->code_nonconst());
120 instrument(code.function());
121
122 // instrument(code.lhs(), LHS);
123 for(auto &arg : code.arguments())
124 instrument(arg);
125 }
126 }
127}
128
130{
131 for(const auto &identifier : find_symbol_identifiers(expr))
132 {
134 const symbolt &symbol = ns.lookup(identifier);
135
136 if(!symbol.is_state_var)
137 continue;
138
139 if(symbol.is_thread_local)
140 {
141 if(thread_local_vars.find(identifier) != thread_local_vars.end())
142 continue;
143
144 thread_local_vart &thread_local_var = thread_local_vars[identifier];
145 thread_local_var.type = symbol.type;
146 }
147 else
148 {
149 if(shared_vars.find(identifier) != shared_vars.end())
150 continue;
151
152 shared_vart &shared_var = shared_vars[identifier];
153 shared_var.type = symbol.type;
154 }
155 }
156}
157
159 const goto_programt &goto_program,
160 const is_threadedt &is_threaded)
161{
162 forall_goto_program_instructions(i_it, goto_program)
163 {
164 if(is_threaded(i_it))
165 i_it->apply([this](const exprt &e) { collect(e); });
166 }
167}
168
170{
171// for(
172}
173
175 goto_functionst &goto_functions)
176{
178 is_threadedt is_threaded(goto_functions);
179
180 // this first collects all shared and thread-local variables
181 for(const auto &gf_entry : goto_functions.function_map)
182 collect(gf_entry.second.body, is_threaded);
183
184 // add array symbols
186
187 // now instrument
188 for(auto &gf_entry : goto_functions.function_map)
189 instrument(gf_entry.second.body);
190}
191
193 value_setst &value_sets,
194 goto_modelt &goto_model)
195{
196 concurrency_instrumentationt concurrency_instrumentation(
197 value_sets, goto_model.symbol_table);
198 concurrency_instrumentation(goto_model.goto_functions);
199}
codet representation of a function call statement.
optionalt< symbol_exprt > array_symbol
Definition: concurrency.cpp:62
optionalt< symbol_exprt > w_index_symbol
Definition: concurrency.cpp:62
void collect(const goto_programt &goto_program, const is_threadedt &is_threaded)
void operator()(goto_functionst &goto_functions)
Definition: concurrency.cpp:35
concurrency_instrumentationt(value_setst &_value_sets, symbol_tablet &_symbol_table)
Definition: concurrency.cpp:27
std::map< irep_idt, thread_local_vart > thread_local_varst
Definition: concurrency.cpp:75
thread_local_varst thread_local_vars
Definition: concurrency.cpp:76
void instrument(goto_functionst &goto_functions)
symbol_tablet & symbol_table
Definition: concurrency.cpp:42
std::map< irep_idt, shared_vart > shared_varst
Definition: concurrency.cpp:72
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
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:598
Array index operator.
Definition: std_expr.h:1328
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Replace expression or type symbols by an expression or type, respectively.
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:80
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
bool is_thread_local
Definition: symbol.h:65
bool is_state_var
Definition: symbol.h:62
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.
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,...
std::unordered_set< irep_idt > find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol.
const code_function_callt & to_code_function_call(const codet &code)
#define forall_goto_program_instructions(it, program)
Over-approximate Concurrency for Threaded Goto Programs.
nonstd::optional< T > optionalt
Definition: optional.h:35
#define UNIMPLEMENTED
Definition: invariant.h:525
API to expression classes.