cprover
rw_set.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Race Detection for Threaded Goto Programs
4 
5 Author: Daniel Kroening
6 
7 Date: February 2006
8 
9 \*******************************************************************/
10 
13 
14 #include "rw_set.h"
15 
16 #include <util/std_expr.h>
17 #include <util/std_code.h>
18 #include <util/namespace.h>
19 
20 #include <langapi/language_util.h>
21 
23 
24 void rw_set_baset::output(std::ostream &out) const
25 {
26  out << "READ:\n";
27  for(entriest::const_iterator it=r_entries.begin();
28  it!=r_entries.end();
29  it++)
30  {
31  out << it->second.object << " if "
32  << from_expr(ns, it->second.object, it->second.guard) << '\n';
33  }
34 
35  out << '\n';
36 
37  out << "WRITE:\n";
38  for(entriest::const_iterator it=w_entries.begin();
39  it!=w_entries.end();
40  it++)
41  {
42  out << it->second.object << " if "
43  << from_expr(ns, it->second.object, it->second.guard) << '\n';
44  }
45 }
46 
48 {
49  if(target->is_assign())
50  {
51  assert(target->code.operands().size()==2);
52  assign(target->code.op0(), target->code.op1());
53  }
54  else if(target->is_goto() ||
55  target->is_assume() ||
56  target->is_assert())
57  {
58  read(target->guard);
59  }
60  else if(target->is_function_call())
61  {
62  const code_function_callt &code_function_call=
64 
65  read(code_function_call.function());
66 
67  // do operands
68  for(code_function_callt::argumentst::const_iterator
69  it=code_function_call.arguments().begin();
70  it!=code_function_call.arguments().end();
71  it++)
72  read(*it);
73 
74  if(code_function_call.lhs().is_not_nil())
75  write(code_function_call.lhs());
76  }
77 }
78 
79 void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs)
80 {
81  read(rhs);
82  read_write_rec(lhs, false, true, "", guardt());
83 }
84 
86  const exprt &expr,
87  bool r, bool w,
88  const std::string &suffix,
89  const guardt &guard)
90 {
91  if(expr.id()==ID_symbol)
92  {
93  const symbol_exprt &symbol_expr=to_symbol_expr(expr);
94 
95  irep_idt object=id2string(symbol_expr.get_identifier())+suffix;
96 
97  if(r)
98  {
99  entryt &entry=r_entries[object];
100  entry.object=object;
101  entry.symbol_expr=symbol_expr;
102  entry.guard=guard.as_expr(); // should 'OR'
103 
104  track_deref(entry, true);
105  }
106 
107  if(w)
108  {
109  entryt &entry=w_entries[object];
110  entry.object=object;
111  entry.symbol_expr=symbol_expr;
112  entry.guard=guard.as_expr(); // should 'OR'
113 
114  track_deref(entry, false);
115  }
116  }
117  else if(expr.id()==ID_member)
118  {
119  assert(expr.operands().size()==1);
120  const std::string &component_name=expr.get_string(ID_component_name);
121  read_write_rec(expr.op0(), r, w, "."+component_name+suffix, guard);
122  }
123  else if(expr.id()==ID_index)
124  {
125  // we don't distinguish the array elements for now
126  assert(expr.operands().size()==2);
127  read_write_rec(expr.op0(), r, w, "[]"+suffix, guard);
128  read(expr.op1(), guard);
129  }
130  else if(expr.id()==ID_dereference)
131  {
132  assert(expr.operands().size()==1);
133  set_track_deref();
134  read(expr.op0(), guard);
135 
136  exprt tmp=expr;
137  #ifdef LOCAL_MAY
138  const std::set<exprt> aliases=local_may.get(target, expr);
139  for(std::set<exprt>::const_iterator it=aliases.begin();
140  it!=aliases.end();
141  ++it)
142  {
143  #ifndef LOCAL_MAY_SOUND
144  if(it->id()==ID_unknown)
145  {
146  /* as an under-approximation */
147  // std::cout << "Sorry, LOCAL_MAY too imprecise. "
148  // << Omitting some variables.\n";
149  irep_idt object=ID_unknown;
150 
151  entryt &entry=r_entries[object];
152  entry.object=object;
153  entry.symbol_expr=symbol_exprt(ID_unknown);
154  entry.guard=guard.as_expr(); // should 'OR'
155 
156  continue;
157  }
158  #endif
159  read_write_rec(*it, r, w, suffix, guard);
160  }
161  #else
163 
164  read_write_rec(tmp, r, w, suffix, guard);
165  #endif
166 
168  }
169  else if(expr.id()==ID_typecast)
170  {
171  assert(expr.operands().size()==1);
172  read_write_rec(expr.op0(), r, w, suffix, guard);
173  }
174  else if(expr.id()==ID_address_of)
175  {
176  assert(expr.operands().size()==1);
177  }
178  else if(expr.id()==ID_if)
179  {
180  assert(expr.operands().size()==3);
181  read(expr.op0(), guard);
182 
183  guardt true_guard(guard);
184  true_guard.add(expr.op0());
185  read_write_rec(expr.op1(), r, w, suffix, true_guard);
186 
187  guardt false_guard(guard);
188  false_guard.add(not_exprt(expr.op0()));
189  read_write_rec(expr.op2(), r, w, suffix, false_guard);
190  }
191  else
192  {
193  forall_operands(it, expr)
194  read_write_rec(*it, r, w, suffix, guard);
195  }
196 }
197 
199 {
200  if(function.id()==ID_symbol)
201  {
202  const irep_idt &id=to_symbol_expr(function).get_identifier();
203 
204  goto_functionst::function_mapt::const_iterator f_it=
205  goto_functions.function_map.find(id);
206 
207  if(f_it!=goto_functions.function_map.end())
208  {
209  const goto_programt &body=f_it->second.body;
210 
211 #ifdef LOCAL_MAY
212  local_may_aliast local_may(f_it->second);
213 #if 0
214  for(goto_functionst::function_mapt::const_iterator
215  g_it=goto_functions.function_map.begin();
216  g_it!=goto_functions.function_map.end(); ++g_it)
217  local_may(g_it->second);
218 #endif
219 #endif
220 
222  {
223  *this+=rw_set_loct(ns, value_sets, i_it
224 #ifdef LOCAL_MAY
225  , local_may
226 #endif
227  ); // NOLINT(whitespace/parens)
228  }
229  }
230  }
231  else if(function.id()==ID_if)
232  {
233  compute_rec(to_if_expr(function).true_case());
234  compute_rec(to_if_expr(function).false_case());
235  }
236 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
exprt as_expr() const
Definition: guard.h:41
Boolean negation.
Definition: std_expr.h:3308
void compute()
Definition: rw_set.cpp:47
static int8_t r
Definition: irep_hash.h:59
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
exprt & op0()
Definition: expr.h:84
void output(std::ostream &out) const
Definition: rw_set.cpp:24
entriest r_entries
Definition: rw_set.h:57
const irep_idt & get_identifier() const
Definition: std_expr.h:176
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: guard.h:19
function_mapt function_map
virtual void reset_track_deref()
Definition: rw_set.h:95
void compute_rec(const exprt &function)
Definition: rw_set.cpp:198
value_setst & value_sets
Definition: rw_set.h:143
const irep_idt & id() const
Definition: irep.h:259
argumentst & arguments()
Definition: std_code.h:1109
exprt dereference(const exprt &pointer, const namespacet &ns)
Dereference the given pointer-expression.
Definition: dereference.h:75
const namespacet & ns
Definition: rw_set.h:97
virtual void track_deref(const entryt &, bool read)
Definition: rw_set.h:90
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
irep_idt object
Definition: rw_set.h:48
const goto_programt::const_targett target
Definition: rw_set.h:144
codet representation of a function call statement.
Definition: std_code.h:1036
#define forall_operands(it, expr)
Definition: expr.h:20
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
const goto_functionst & goto_functions
Definition: rw_set.h:218
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
entriest w_entries
Definition: rw_set.h:57
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const guardt &guard)
Definition: rw_set.cpp:85
value_setst & value_sets
Definition: rw_set.h:217
exprt & function()
Definition: std_code.h:1099
Base class for all expressions.
Definition: expr.h:54
symbol_exprt symbol_expr
Definition: rw_set.h:47
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
Expression to hold a symbol (variable)
Definition: std_expr.h:143
exprt & op2()
Definition: expr.h:90
void assign(const exprt &lhs, const exprt &rhs)
Definition: rw_set.cpp:79
void write(const exprt &expr)
Definition: rw_set.h:160
virtual void set_track_deref()
Definition: rw_set.h:94
operandst & operands()
Definition: expr.h:78
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
void read(const exprt &expr)
Definition: rw_set.h:150
const namespacet ns
Definition: rw_set.h:216
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
Race Detection for Threaded Goto Programs.