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/std_expr.h>
17 #include <util/find_symbols.h>
18 #include <util/replace_symbol.h>
19 
20 #include <analyses/is_threaded.h>
21 
23 {
24 public:
26  value_setst &_value_sets,
27  symbol_tablet &_symbol_table):
28  value_sets(_value_sets),
29  symbol_table(_symbol_table)
30  {
31  }
32 
33  void operator()(goto_functionst &goto_functions)
34  {
35  instrument(goto_functions);
36  }
37 
38 protected:
41 
42  void instrument(goto_functionst &goto_functions);
43 
45 
46  void instrument(exprt &expr);
47 
48  void collect(
50  const is_threadedt &is_threaded);
51 
52  void collect(const exprt &expr);
53 
54  void add_array_symbols();
55 
57  {
58  public:
61  };
62 
64  {
65  public:
68  };
69 
70  typedef std::map<irep_idt, shared_vart> shared_varst;
72 
73  typedef std::map<irep_idt, thread_local_vart> thread_local_varst;
75 };
76 
78 {
79  std::set<exprt> symbols;
80 
81  find_symbols(expr, symbols);
82 
83  replace_symbolt replace_symbol;
84 
85  for(std::set<exprt>::const_iterator
86  s_it=symbols.begin();
87  s_it!=symbols.end();
88  s_it++)
89  {
90  if(s_it->id()==ID_symbol)
91  {
92  const irep_idt identifier=
94 
95  shared_varst::const_iterator
96  v_it=shared_vars.find(identifier);
97 
98  if(v_it!=shared_vars.end())
99  {
100  index_exprt new_expr;
101  // new_expr.array()=symbol_expr();
102  // new_expr.index()=symbol_expr();
103 
104  replace_symbol.insert(identifier, new_expr);
105  }
106  }
107  }
108 }
109 
112 {
113  for(goto_programt::instructionst::iterator
114  it=goto_program.instructions.begin();
115  it!=goto_program.instructions.end();
116  it++)
117  {
118  if(it->is_assign())
119  {
120  code_assignt &code=to_code_assign(it->code);
121  instrument(code.rhs());
122  }
123  else if(it->is_assume() || it->is_assert() || it->is_goto())
124  instrument(it->guard);
125  else if(it->is_function_call())
126  {
128  instrument(code.function());
129 
130  // instrument(code.lhs(), LHS);
131  Forall_expr(it, code.arguments())
132  instrument(*it);
133  }
134  }
135 }
136 
138 {
139  std::set<exprt> symbols;
140 
141  find_symbols(expr, symbols);
142 
143  for(std::set<exprt>::const_iterator
144  s_it=symbols.begin();
145  s_it!=symbols.end();
146  s_it++)
147  {
148  if(s_it->id()==ID_symbol)
149  {
150  const irep_idt identifier=
152 
154  const symbolt &symbol=ns.lookup(identifier);
155 
156  if(!symbol.is_state_var)
157  continue;
158 
159  if(symbol.is_thread_local)
160  {
161  if(thread_local_vars.find(identifier)!=thread_local_vars.end())
162  continue;
163 
164  thread_local_vart &thread_local_var=thread_local_vars[identifier];
165  thread_local_var.type=symbol.type;
166  }
167  else
168  {
169  if(shared_vars.find(identifier)!=shared_vars.end())
170  continue;
171 
172  shared_vart &shared_var=shared_vars[identifier];
173  shared_var.type=symbol.type;
174  }
175  }
176  }
177 }
178 
181  const is_threadedt &is_threaded)
182 {
184  {
185  if(is_threaded(i_it))
186  {
187  if(i_it->is_assign())
188  collect(i_it->code);
189  else if(i_it->is_assume() || i_it->is_assert() || i_it->is_goto())
190  collect(i_it->guard);
191  else if(i_it->is_function_call())
192  collect(i_it->code);
193  }
194  }
195 }
196 
198 {
199 // for(
200 }
201 
203  goto_functionst &goto_functions)
204 {
206  is_threadedt is_threaded(goto_functions);
207 
208  // this first collects all shared and thread-local variables
209  forall_goto_functions(f_it, goto_functions)
210  collect(f_it->second.body, is_threaded);
211 
212  // add array symbols
214 
215  // now instrument
216  Forall_goto_functions(f_it, goto_functions)
217  instrument(f_it->second.body);
218 }
219 
221  value_setst &value_sets,
222  goto_modelt &goto_model)
223 {
224  concurrency_instrumentationt concurrency_instrumentation(
225  value_sets, goto_model.symbol_table);
226  concurrency_instrumentation(goto_model.goto_functions);
227 }
The type of an expression.
Definition: type.h:22
Over-approximate Concurrency for Threaded Goto Programs.
concurrency_instrumentationt(value_setst &_value_sets, symbol_tablet &_symbol_table)
Definition: concurrency.cpp:25
bool is_thread_local
Definition: symbol.h:67
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:128
symbol_tablet & symbol_table
Definition: concurrency.cpp:40
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
std::map< irep_idt, thread_local_vart > thread_local_varst
Definition: concurrency.cpp:73
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
argumentst & arguments()
Definition: std_code.h:890
#define Forall_expr(it, expr)
Definition: expr.h:32
exprt & rhs()
Definition: std_code.h:214
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
thread_local_varst thread_local_vars
Definition: concurrency.cpp:74
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void operator()(goto_functionst &goto_functions)
Definition: concurrency.cpp:33
typet type
Type of symbol.
Definition: symbol.h:34
exprt & function()
Definition: std_code.h:878
Base class for all expressions.
Definition: expr.h:42
bool is_state_var
Definition: symbol.h:63
std::map< irep_idt, shared_vart > shared_varst
Definition: concurrency.cpp:70
#define Forall_goto_functions(it, functions)
goto_programt & goto_program
Definition: cover.cpp:63
void insert(const irep_idt &identifier, const exprt &expr)
void collect(const goto_programt &goto_program, const is_threadedt &is_threaded)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
Encoding for Threaded Goto Programs.
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
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 namespace_baset::lookup().
Definition: namespace.cpp:136
Assignment.
Definition: std_code.h:196
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
array index operator
Definition: std_expr.h:1462