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 
44  void instrument(
45  goto_programt &goto_program,
46  const is_threadedt &is_threaded);
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;
73  shared_varst shared_vars;
74 
75  typedef std::map<irep_idt, thread_local_vart> thread_local_varst;
76  thread_local_varst thread_local_vars;
77 };
78 
80 {
81  std::set<exprt> symbols;
82 
83  find_symbols(expr, symbols);
84 
85  replace_symbolt replace_symbol;
86 
87  for(std::set<exprt>::const_iterator
88  s_it=symbols.begin();
89  s_it!=symbols.end();
90  s_it++)
91  {
92  if(s_it->id()==ID_symbol)
93  {
94  const irep_idt identifier=
96 
97  shared_varst::const_iterator
98  v_it=shared_vars.find(identifier);
99 
100  if(v_it!=shared_vars.end())
101  {
102  index_exprt new_expr;
103  // new_expr.array()=symbol_expr();
104  // new_expr.index()=symbol_expr();
105 
106  replace_symbol.insert(identifier, new_expr);
107  }
108  }
109  }
110 }
111 
113  goto_programt &goto_program,
114  const is_threadedt &is_threaded)
115 {
116  for(goto_programt::instructionst::iterator
117  it=goto_program.instructions.begin();
118  it!=goto_program.instructions.end();
119  it++)
120  {
121  if(it->is_assign())
122  {
123  code_assignt &code=to_code_assign(it->code);
124  instrument(code.rhs());
125  }
126  else if(it->is_assume() || it->is_assert() || it->is_goto())
127  instrument(it->guard);
128  else if(it->is_function_call())
129  {
131  instrument(code.function());
132 
133  // instrument(code.lhs(), LHS);
134  Forall_expr(it, code.arguments())
135  instrument(*it);
136  }
137  }
138 }
139 
141 {
142  std::set<exprt> symbols;
143 
144  find_symbols(expr, symbols);
145 
146  for(std::set<exprt>::const_iterator
147  s_it=symbols.begin();
148  s_it!=symbols.end();
149  s_it++)
150  {
151  if(s_it->id()==ID_symbol)
152  {
153  const irep_idt identifier=
155 
157  const symbolt &symbol=ns.lookup(identifier);
158 
159  if(!symbol.is_state_var)
160  continue;
161 
162  if(symbol.is_thread_local)
163  {
164  if(thread_local_vars.find(identifier)!=thread_local_vars.end())
165  continue;
166 
167  thread_local_vart &thread_local_var=thread_local_vars[identifier];
168  thread_local_var.type=symbol.type;
169  }
170  else
171  {
172  if(shared_vars.find(identifier)!=shared_vars.end())
173  continue;
174 
175  shared_vart &shared_var=shared_vars[identifier];
176  shared_var.type=symbol.type;
177  }
178  }
179  }
180 }
181 
183  const goto_programt &goto_program,
184  const is_threadedt &is_threaded)
185 {
186  forall_goto_program_instructions(i_it, goto_program)
187  {
188  if(is_threaded(i_it))
189  {
190  if(i_it->is_assign())
191  collect(i_it->code);
192  else if(i_it->is_assume() || i_it->is_assert() || i_it->is_goto())
193  collect(i_it->guard);
194  else if(i_it->is_function_call())
195  collect(i_it->code);
196  }
197  }
198 }
199 
201 {
202 // for(
203 }
204 
206  goto_functionst &goto_functions)
207 {
209  is_threadedt is_threaded(goto_functions);
210 
211  // this first collects all shared and thread-local variables
212  forall_goto_functions(f_it, goto_functions)
213  collect(f_it->second.body, is_threaded);
214 
215  // add array symbols
217 
218  // now instrument
219  Forall_goto_functions(f_it, goto_functions)
220  instrument(f_it->second.body, is_threaded);
221 }
222 
226  goto_functionst &goto_functions)
227 {
228  concurrency_instrumentationt concurrency_instrumentation(
229  value_sets, symbol_table);
230  concurrency_instrumentation(goto_functions);
231 }
The type of an expression.
Definition: type.h:20
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
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:70
void instrument(goto_functionst &goto_functions)
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
Definition: std_expr.h:120
symbol_tablet & symbol_table
Definition: concurrency.cpp:40
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
std::map< irep_idt, thread_local_vart > thread_local_varst
Definition: concurrency.cpp:75
void concurrency(value_setst &value_sets, class symbol_tablet &symbol_table, goto_functionst &goto_functions)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
argumentst & arguments()
Definition: std_code.h:689
#define Forall_expr(it, expr)
Definition: expr.h:32
exprt & rhs()
Definition: std_code.h:162
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
thread_local_varst thread_local_vars
Definition: concurrency.cpp:76
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void operator()(goto_functionst &goto_functions)
Definition: concurrency.cpp:33
typet type
Type of symbol.
Definition: symbol.h:37
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
bool is_state_var
Definition: symbol.h:66
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
std::map< irep_idt, shared_vart > shared_varst
Definition: concurrency.cpp:72
#define Forall_goto_functions(it, functions)
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:82
Encoding for Threaded Goto Programs.
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
void find_symbols(const exprt &src, find_symbols_sett &dest)
Assignment.
Definition: std_code.h:144
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
array index operator
Definition: std_expr.h:1170