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 }
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:221
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:41
rw_set_baset::entryt
Definition: rw_set.h:45
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
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:1297
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
_rw_set_loct::assign
void assign(const exprt &lhs, const exprt &rhs)
Definition: rw_set.cpp:80
_rw_set_loct::target
const goto_programt::const_targett target
Definition: rw_set.h:144
exprt
Base class for all expressions.
Definition: expr.h:54
rw_set_functiont::compute_rec
void compute_rec(const exprt &function)
Definition: rw_set.cpp:200
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:150
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:81
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:1240
local_may_aliast
Definition: local_may_alias.h:26
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
_rw_set_loct::function_id
const irep_idt function_id
Definition: rw_set.h:143
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:110
pointer_expr.h
API to expression classes for Pointers.
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
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:142
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:1260
rw_set_loct
Definition: rw_set.h:178
rw_set_functiont::value_sets
value_setst & value_sets
Definition: rw_set.h:220
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:86
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:1815
goto_program_dereference.h
Value Set.
_rw_set_loct::write
void write(const exprt &expr)
Definition: rw_set.h:160
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:74
rw_set_functiont::ns
const namespacet ns
Definition: rw_set.h:219
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
exprt::operands
operandst & operands()
Definition: expr.h:96
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:287
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:48
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:25
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1167
rw_set_baset::set_track_deref
virtual void set_track_deref()
Definition: rw_set.h:97
not_exprt
Boolean negation.
Definition: std_expr.h:2042