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