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/namespace.h>
17 #include <util/pointer_expr.h>
18 #include <util/std_code.h>
19 #include <util/std_expr.h>
20 
21 #include <langapi/language_util.h>
22 
24 
25 void rw_set_baset::output(std::ostream &out) const
26 {
27  out << "READ:\n";
28  for(entriest::const_iterator it=r_entries.begin();
29  it!=r_entries.end();
30  it++)
31  {
32  out << it->second.object << " if "
33  << from_expr(ns, it->second.object, it->second.guard) << '\n';
34  }
35 
36  out << '\n';
37 
38  out << "WRITE:\n";
39  for(entriest::const_iterator it=w_entries.begin();
40  it!=w_entries.end();
41  it++)
42  {
43  out << it->second.object << " if "
44  << from_expr(ns, it->second.object, it->second.guard) << '\n';
45  }
46 }
47 
49 {
50  if(target->is_assign())
51  {
52  const auto &assignment = target->get_assign();
53  assign(assignment.lhs(), assignment.rhs());
54  }
55  else if(target->is_goto() ||
56  target->is_assume() ||
57  target->is_assert())
58  {
59  read(target->get_condition());
60  }
61  else if(target->is_function_call())
62  {
63  const code_function_callt &code_function_call=
65 
66  read(code_function_call.function());
67 
68  // do operands
69  for(code_function_callt::argumentst::const_iterator
70  it=code_function_call.arguments().begin();
71  it!=code_function_call.arguments().end();
72  it++)
73  read(*it);
74 
75  if(code_function_call.lhs().is_not_nil())
76  write(code_function_call.lhs());
77  }
78 }
79 
80 void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs)
81 {
82  read(rhs);
83  read_write_rec(lhs, false, true, "", exprt::operandst());
84 }
85 
87  const exprt &expr,
88  bool r,
89  bool w,
90  const std::string &suffix,
91  const exprt::operandst &guard_conjuncts)
92 {
93  if(expr.id()==ID_symbol)
94  {
95  const symbol_exprt &symbol_expr=to_symbol_expr(expr);
96 
97  irep_idt object=id2string(symbol_expr.get_identifier())+suffix;
98 
99  if(r)
100  {
101  const auto &entry = r_entries.emplace(
102  object, entryt(symbol_expr, object, conjunction(guard_conjuncts)));
103 
104  track_deref(entry.first->second, true);
105  }
106 
107  if(w)
108  {
109  const auto &entry = w_entries.emplace(
110  object, entryt(symbol_expr, object, conjunction(guard_conjuncts)));
111 
112  track_deref(entry.first->second, false);
113  }
114  }
115  else if(expr.id()==ID_member)
116  {
117  const auto &member_expr = to_member_expr(expr);
118  const std::string &component_name =
119  id2string(member_expr.get_component_name());
121  member_expr.compound(),
122  r,
123  w,
124  "." + component_name + suffix,
125  guard_conjuncts);
126  }
127  else if(expr.id()==ID_index)
128  {
129  // we don't distinguish the array elements for now
130  const auto &index_expr = to_index_expr(expr);
131  read_write_rec(index_expr.array(), r, w, "[]" + suffix, guard_conjuncts);
132  read(index_expr.index(), guard_conjuncts);
133  }
134  else if(expr.id()==ID_dereference)
135  {
136  set_track_deref();
137  read(to_dereference_expr(expr).pointer(), guard_conjuncts);
138 
139  exprt tmp=expr;
140  #ifdef LOCAL_MAY
141  const std::set<exprt> aliases=local_may.get(target, expr);
142  for(std::set<exprt>::const_iterator it=aliases.begin();
143  it!=aliases.end();
144  ++it)
145  {
146  #ifndef LOCAL_MAY_SOUND
147  if(it->id()==ID_unknown)
148  {
149  /* as an under-approximation */
150  // std::cout << "Sorry, LOCAL_MAY too imprecise. "
151  // << Omitting some variables.\n";
152  irep_idt object=ID_unknown;
153 
154  entryt &entry=r_entries[object];
155  entry.object=object;
156  entry.symbol_expr=symbol_exprt(ID_unknown);
157  entry.guard = conjunction(guard_conjuncts); // should 'OR'
158 
159  continue;
160  }
161  #endif
162  read_write_rec(*it, r, w, suffix, guard_conjuncts);
163  }
164  #else
166 
167  read_write_rec(tmp, r, w, suffix, guard_conjuncts);
168 #endif
169 
171  }
172  else if(expr.id()==ID_typecast)
173  {
174  read_write_rec(to_typecast_expr(expr).op(), r, w, suffix, guard_conjuncts);
175  }
176  else if(expr.id()==ID_address_of)
177  {
178  assert(expr.operands().size()==1);
179  }
180  else if(expr.id()==ID_if)
181  {
182  const auto &if_expr = to_if_expr(expr);
183  read(if_expr.cond(), guard_conjuncts);
184 
185  exprt::operandst true_guard = guard_conjuncts;
186  true_guard.push_back(if_expr.cond());
187  read_write_rec(if_expr.true_case(), r, w, suffix, true_guard);
188 
189  exprt::operandst false_guard = guard_conjuncts;
190  false_guard.push_back(not_exprt(if_expr.cond()));
191  read_write_rec(if_expr.false_case(), r, w, suffix, false_guard);
192  }
193  else
194  {
195  forall_operands(it, expr)
196  read_write_rec(*it, r, w, suffix, guard_conjuncts);
197  }
198 }
199 
201 {
202  if(function.id()==ID_symbol)
203  {
204  const irep_idt &function_id = to_symbol_expr(function).get_identifier();
205 
206  goto_functionst::function_mapt::const_iterator f_it =
207  goto_functions.function_map.find(function_id);
208 
209  if(f_it!=goto_functions.function_map.end())
210  {
211  const goto_programt &body=f_it->second.body;
212 
213 #ifdef LOCAL_MAY
214  local_may_aliast local_may(f_it->second);
215 #if 0
216  for(goto_functionst::function_mapt::const_iterator
217  g_it=goto_functions.function_map.begin();
218  g_it!=goto_functions.function_map.end(); ++g_it)
219  local_may(g_it->second);
220 #endif
221 #endif
222 
224  {
225  *this += rw_set_loct(
226  ns,
227  value_sets,
228  function_id,
229  i_it
230 #ifdef LOCAL_MAY
231  ,
232  local_may
233 #endif
234  ); // NOLINT(whitespace/parens)
235  }
236  }
237  }
238  else if(function.id()==ID_if)
239  {
240  compute_rec(to_if_expr(function).true_case());
241  compute_rec(to_if_expr(function).false_case());
242  }
243 }
void assign(const exprt &lhs, const exprt &rhs)
Definition: rw_set.cpp:80
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const exprt::operandst &guard_conjuncts)
Definition: rw_set.cpp:86
const irep_idt function_id
Definition: rw_set.h:143
void read(const exprt &expr)
Definition: rw_set.h:150
value_setst & value_sets
Definition: rw_set.h:142
void compute()
Definition: rw_set.cpp:48
void write(const exprt &expr)
Definition: rw_set.h:160
const goto_programt::const_targett target
Definition: rw_set.h:144
codet representation of a function call statement.
Definition: std_code.h:1215
exprt & function()
Definition: std_code.h:1250
argumentst & arguments()
Definition: std_code.h:1260
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
operandst & operands()
Definition: expr.h:96
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
Boolean negation.
Definition: std_expr.h:2042
entriest r_entries
Definition: rw_set.h:60
virtual void track_deref(const entryt &, bool read)
Definition: rw_set.h:93
virtual void reset_track_deref()
Definition: rw_set.h:98
entriest w_entries
Definition: rw_set.h:60
void output(std::ostream &out) const
Definition: rw_set.cpp:25
const namespacet & ns
Definition: rw_set.h:100
virtual void set_track_deref()
Definition: rw_set.h:97
const goto_functionst & goto_functions
Definition: rw_set.h:221
void compute_rec(const exprt &function)
Definition: rw_set.cpp:200
const namespacet ns
Definition: rw_set.h:219
value_setst & value_sets
Definition: rw_set.h:220
Expression to hold a symbol (variable)
Definition: std_expr.h:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
#define forall_operands(it, expr)
Definition: expr.h:18
#define forall_goto_program_instructions(it, program)
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
static int8_t r
Definition: irep_hash.h:59
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
Race Detection for Threaded Goto Programs.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:41
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
irep_idt object
Definition: rw_set.h:47
symbol_exprt symbol_expr
Definition: rw_set.h:46