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 = target->get_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: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:442
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:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
_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: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: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: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:80
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:109
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:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
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: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:1814
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:2611
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:1180
rw_set_baset::set_track_deref
virtual void set_track_deref()
Definition: rw_set.h:97
not_exprt
Boolean negation.
Definition: std_expr.h:2041