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  const auto &assignment = target->get_assign();
52  assign(assignment.lhs(), assignment.rhs());
53  }
54  else if(target->is_goto() ||
55  target->is_assume() ||
56  target->is_assert())
57  {
58  read(target->get_condition());
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, "", exprt::operandst());
83 }
84 
86  const exprt &expr,
87  bool r,
88  bool w,
89  const std::string &suffix,
90  const exprt::operandst &guard_conjuncts)
91 {
92  if(expr.id()==ID_symbol)
93  {
94  const symbol_exprt &symbol_expr=to_symbol_expr(expr);
95 
96  irep_idt object=id2string(symbol_expr.get_identifier())+suffix;
97 
98  if(r)
99  {
100  const auto &entry = r_entries.emplace(
101  object, entryt(symbol_expr, object, conjunction(guard_conjuncts)));
102 
103  track_deref(entry.first->second, true);
104  }
105 
106  if(w)
107  {
108  const auto &entry = w_entries.emplace(
109  object, entryt(symbol_expr, object, conjunction(guard_conjuncts)));
110 
111  track_deref(entry.first->second, false);
112  }
113  }
114  else if(expr.id()==ID_member)
115  {
116  const auto &member_expr = to_member_expr(expr);
117  const std::string &component_name =
118  id2string(member_expr.get_component_name());
120  member_expr.compound(),
121  r,
122  w,
123  "." + component_name + suffix,
124  guard_conjuncts);
125  }
126  else if(expr.id()==ID_index)
127  {
128  // we don't distinguish the array elements for now
129  const auto &index_expr = to_index_expr(expr);
130  read_write_rec(index_expr.array(), r, w, "[]" + suffix, guard_conjuncts);
131  read(index_expr.index(), guard_conjuncts);
132  }
133  else if(expr.id()==ID_dereference)
134  {
135  set_track_deref();
136  read(to_dereference_expr(expr).pointer(), guard_conjuncts);
137 
138  exprt tmp=expr;
139  #ifdef LOCAL_MAY
140  const std::set<exprt> aliases=local_may.get(target, expr);
141  for(std::set<exprt>::const_iterator it=aliases.begin();
142  it!=aliases.end();
143  ++it)
144  {
145  #ifndef LOCAL_MAY_SOUND
146  if(it->id()==ID_unknown)
147  {
148  /* as an under-approximation */
149  // std::cout << "Sorry, LOCAL_MAY too imprecise. "
150  // << Omitting some variables.\n";
151  irep_idt object=ID_unknown;
152 
153  entryt &entry=r_entries[object];
154  entry.object=object;
155  entry.symbol_expr=symbol_exprt(ID_unknown);
156  entry.guard = conjunction(guard_conjuncts); // should 'OR'
157 
158  continue;
159  }
160  #endif
161  read_write_rec(*it, r, w, suffix, guard_conjuncts);
162  }
163  #else
165 
166  read_write_rec(tmp, r, w, suffix, guard_conjuncts);
167 #endif
168 
170  }
171  else if(expr.id()==ID_typecast)
172  {
173  read_write_rec(to_typecast_expr(expr).op(), r, w, suffix, guard_conjuncts);
174  }
175  else if(expr.id()==ID_address_of)
176  {
177  assert(expr.operands().size()==1);
178  }
179  else if(expr.id()==ID_if)
180  {
181  const auto &if_expr = to_if_expr(expr);
182  read(if_expr.cond(), guard_conjuncts);
183 
184  exprt::operandst true_guard = guard_conjuncts;
185  true_guard.push_back(if_expr.cond());
186  read_write_rec(if_expr.true_case(), r, w, suffix, true_guard);
187 
188  exprt::operandst false_guard = guard_conjuncts;
189  false_guard.push_back(not_exprt(if_expr.cond()));
190  read_write_rec(if_expr.false_case(), r, w, suffix, false_guard);
191  }
192  else
193  {
194  forall_operands(it, expr)
195  read_write_rec(*it, r, w, suffix, guard_conjuncts);
196  }
197 }
198 
200 {
201  if(function.id()==ID_symbol)
202  {
203  const irep_idt &function_id = to_symbol_expr(function).get_identifier();
204 
205  goto_functionst::function_mapt::const_iterator f_it =
206  goto_functions.function_map.find(function_id);
207 
208  if(f_it!=goto_functions.function_map.end())
209  {
210  const goto_programt &body=f_it->second.body;
211 
212 #ifdef LOCAL_MAY
213  local_may_aliast local_may(f_it->second);
214 #if 0
215  for(goto_functionst::function_mapt::const_iterator
216  g_it=goto_functions.function_map.begin();
217  g_it!=goto_functions.function_map.end(); ++g_it)
218  local_may(g_it->second);
219 #endif
220 #endif
221 
223  {
224  *this += rw_set_loct(
225  ns,
226  value_sets,
227  function_id,
228  i_it
229 #ifdef LOCAL_MAY
230  ,
231  local_may
232 #endif
233  ); // NOLINT(whitespace/parens)
234  }
235  }
236  }
237  else if(function.id()==ID_if)
238  {
239  compute_rec(to_if_expr(function).true_case());
240  compute_rec(to_if_expr(function).false_case());
241  }
242 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
rw_set_functiont::goto_functions
const goto_functionst & goto_functions
Definition: rw_set.h:229
conjunction
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:51
rw_set_baset::entryt
Definition: rw_set.h:45
rw_set_baset::entryt::guard
exprt guard
Definition: rw_set.h:48
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
_rw_set_loct::assign
void assign(const exprt &lhs, const exprt &rhs)
Definition: rw_set.cpp:79
_rw_set_loct::target
const goto_programt::const_targett target
Definition: rw_set.h:152
exprt
Base class for all expressions.
Definition: expr.h:53
rw_set_functiont::compute_rec
void compute_rec(const exprt &function)
Definition: rw_set.cpp:199
rw_set_baset::ns
const namespacet & ns
Definition: rw_set.h:100
_rw_set_loct::read
void read(const exprt &expr)
Definition: rw_set.h:158
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
rw_set_baset::reset_track_deref
virtual void reset_track_deref()
Definition: rw_set.h:98
rw_set_baset::r_entries
entriest r_entries
Definition: rw_set.h:60
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
local_may_aliast
Definition: local_may_alias.h:26
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
_rw_set_loct::function_id
const irep_idt function_id
Definition: rw_set.h:151
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
language_util.h
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
rw_set_baset::w_entries
entriest w_entries
Definition: rw_set.h:60
_rw_set_loct::value_sets
value_setst & value_sets
Definition: rw_set.h:150
rw_set_baset::track_deref
virtual void track_deref(const entryt &, bool read)
Definition: rw_set.h:93
std_code.h
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
rw_set_loct
Definition: rw_set.h:186
rw_set_functiont::value_sets
value_setst & value_sets
Definition: rw_set.h:228
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
_rw_set_loct::read_write_rec
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const exprt::operandst &guard_conjuncts)
Definition: rw_set.cpp:85
rw_set.h
Race Detection for Threaded Goto Programs.
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
goto_program_dereference.h
Value Set.
_rw_set_loct::write
void write(const exprt &expr)
Definition: rw_set.h:168
rw_set_baset::entryt::object
irep_idt object
Definition: rw_set.h:47
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
rw_set_functiont::ns
const namespacet ns
Definition: rw_set.h:227
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
exprt::operands
operandst & operands()
Definition: expr.h:95
r
static int8_t r
Definition: irep_hash.h:59
dereference
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...
Definition: goto_program_dereference.cpp:303
rw_set_baset::entryt::symbol_expr
symbol_exprt symbol_expr
Definition: rw_set.h:46
_rw_set_loct::compute
void compute()
Definition: rw_set.cpp:47
std_expr.h
API to expression classes.
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
rw_set_baset::output
void output(std::ostream &out) const
Definition: rw_set.cpp:24
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
rw_set_baset::set_track_deref
virtual void set_track_deref()
Definition: rw_set.h:97
not_exprt
Boolean negation.
Definition: std_expr.h:2843