cprover
symex_assign.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "symex_assign.h"
13 
14 #include "expr_skeleton.h"
15 #include "goto_symex.h"
16 #include "goto_symex_state.h"
17 #include <util/byte_operators.h>
18 #include <util/expr_util.h>
19 #include <util/format_expr.h>
20 
21 // We can either use with_exprt or update_exprt when building expressions that
22 // modify components of an array or a struct. Set USE_UPDATE to use
23 // update_exprt.
24 // #define USE_UPDATE
25 
26 constexpr bool use_update()
27 {
28 #ifdef USE_UPDATE
29  return true;
30 #else
31  return false;
32 #endif
33 }
34 
36  const exprt &lhs,
37  const expr_skeletont &full_lhs,
38  const exprt &rhs,
39  exprt::operandst &guard)
40 {
41  if(is_ssa_expr(lhs))
42  {
43  assign_symbol(to_ssa_expr(lhs), full_lhs, rhs, guard);
44  }
45  else if(lhs.id() == ID_index)
46  assign_array<use_update()>(to_index_expr(lhs), full_lhs, rhs, guard);
47  else if(lhs.id()==ID_member)
48  {
49  const typet &type = to_member_expr(lhs).struct_op().type();
50  if(type.id() == ID_struct || type.id() == ID_struct_tag)
51  {
52  assign_struct_member<use_update()>(
53  to_member_expr(lhs), full_lhs, rhs, guard);
54  }
55  else if(type.id() == ID_union || type.id() == ID_union_tag)
56  {
57  // should have been replaced by byte_extract
59  "assign_rec: unexpected assignment to union member");
60  }
61  else
63  "assign_rec: unexpected assignment to member of '" + type.id_string() +
64  "'");
65  }
66  else if(lhs.id()==ID_if)
67  assign_if(to_if_expr(lhs), full_lhs, rhs, guard);
68  else if(lhs.id()==ID_typecast)
69  assign_typecast(to_typecast_expr(lhs), full_lhs, rhs, guard);
71  {
72  // ignore
73  }
74  else if(lhs.id()==ID_byte_extract_little_endian ||
75  lhs.id()==ID_byte_extract_big_endian)
76  {
77  assign_byte_extract(to_byte_extract_expr(lhs), full_lhs, rhs, guard);
78  }
79  else if(lhs.id() == ID_complex_real)
80  {
81  // this is stuff like __real__ x = 1;
82  const complex_real_exprt &complex_real_expr = to_complex_real_expr(lhs);
83 
84  const complex_imag_exprt complex_imag_expr(complex_real_expr.op());
85 
86  complex_exprt new_rhs(
87  rhs, complex_imag_expr, to_complex_type(complex_real_expr.op().type()));
88 
89  assign_rec(complex_real_expr.op(), full_lhs, new_rhs, guard);
90  }
91  else if(lhs.id() == ID_complex_imag)
92  {
93  const complex_imag_exprt &complex_imag_expr = to_complex_imag_expr(lhs);
94 
95  const complex_real_exprt complex_real_expr(complex_imag_expr.op());
96 
97  complex_exprt new_rhs(
98  complex_real_expr, rhs, to_complex_type(complex_imag_expr.op().type()));
99 
100  assign_rec(complex_imag_expr.op(), full_lhs, new_rhs, guard);
101  }
102  else
104  "assignment to '" + lhs.id_string() + "' not handled");
105 }
106 
108 struct assignmentt final
109 {
114 };
115 
128  const ssa_exprt &lhs, // L1
129  const expr_skeletont &full_lhs,
130  const struct_exprt &rhs,
131  const exprt::operandst &guard)
132 {
133  const auto &components = to_struct_type(ns.follow(lhs.type())).components();
134  PRECONDITION(rhs.operands().size() == components.size());
135 
136  for(const auto &comp_rhs : make_range(components).zip(rhs.operands()))
137  {
138  const auto &comp = comp_rhs.first;
139  const exprt lhs_field = state.field_sensitivity.apply(
140  ns, state, member_exprt{lhs, comp.get_name(), comp.type()}, true);
141  INVARIANT(
142  lhs_field.id() == ID_symbol,
143  "member of symbol should be susceptible to field-sensitivity");
144 
145  assign_symbol(to_ssa_expr(lhs_field), full_lhs, comp_rhs.second, guard);
146  }
147 }
148 
150  const ssa_exprt &lhs, // L1
151  const expr_skeletont &full_lhs,
152  const exprt &rhs,
153  const exprt::operandst &guard)
154 {
155  exprt l2_rhs =
156  state
157  .rename(
158  // put assignment guard into the rhs
159  guard.empty()
160  ? rhs
161  : static_cast<exprt>(if_exprt{conjunction(guard), rhs, lhs}),
162  ns)
163  .get();
164 
165  assignmentt assignment{lhs, full_lhs, l2_rhs};
166 
168  assignment.rhs = simplify_expr(std::move(assignment.rhs), ns);
169 
170  const ssa_exprt l2_lhs = state
171  .assignment(
172  assignment.lhs,
173  assignment.rhs,
174  ns,
178  .get();
179 
180  state.record_events.push(false);
181  // Note any other symbols mentioned in the skeleton are rvalues -- for example
182  // array indices -- and were renamed to L2 at the start of
183  // goto_symext::symex_assign.
184  const exprt l2_full_lhs = assignment.original_lhs_skeleton.apply(l2_lhs);
186  {
187  INVARIANT(
188  !check_renaming(l2_full_lhs), "l2_full_lhs should be renamed to L2");
189  }
190  state.record_events.pop();
191 
192  auto current_assignment_type =
193  ns.lookup(l2_lhs.get_object_name()).is_auxiliary
195  : assignment_type;
196 
199  l2_lhs,
200  l2_full_lhs,
201  get_original_name(l2_full_lhs),
202  assignment.rhs,
203  state.source,
204  current_assignment_type);
205 
206  const ssa_exprt &l1_lhs = assignment.lhs;
208  {
209  // Split composite symbol lhs into its components
212  // Erase the composite symbol from our working state. Note that we need to
213  // have it in the propagation table and the value set while doing the field
214  // assignments, thus we cannot skip putting it in there above.
215  state.propagation.erase_if_exists(l1_lhs.get_identifier());
216  state.value_set.erase_symbol(l1_lhs, ns);
217  }
218 }
219 
221  const ssa_exprt &lhs, // L1
222  const expr_skeletont &full_lhs,
223  const exprt &rhs,
224  const exprt::operandst &guard)
225 {
226  // Shortcut the common case of a whole-struct initializer:
227  if(rhs.id() == ID_struct)
228  assign_from_struct(lhs, full_lhs, to_struct_expr(rhs), guard);
229  else
230  assign_non_struct_symbol(lhs, full_lhs, rhs, guard);
231 }
232 
234  const typecast_exprt &lhs,
235  const expr_skeletont &full_lhs,
236  const exprt &rhs,
237  exprt::operandst &guard)
238 {
239  // these may come from dereferencing on the lhs
240  exprt rhs_typecasted = typecast_exprt::conditional_cast(rhs, lhs.op().type());
241  expr_skeletont new_skeleton =
242  full_lhs.compose(expr_skeletont::remove_op0(lhs));
243  assign_rec(lhs.op(), new_skeleton, rhs_typecasted, guard);
244 }
245 
246 template <bool use_update>
248  const index_exprt &lhs,
249  const expr_skeletont &full_lhs,
250  const exprt &rhs,
251  exprt::operandst &guard)
252 {
253  const exprt &lhs_array=lhs.array();
254  const exprt &lhs_index=lhs.index();
255  const typet &lhs_index_type = lhs_array.type();
256 
257  PRECONDITION(lhs_index_type.id() == ID_array);
258 
259  if(use_update)
260  {
261  // turn
262  // a[i]=e
263  // into
264  // a'==UPDATE(a, [i], e)
265  const update_exprt new_rhs{lhs_array, index_designatort(lhs_index), rhs};
266  const expr_skeletont new_skeleton =
267  full_lhs.compose(expr_skeletont::remove_op0(lhs));
268  assign_rec(lhs, new_skeleton, new_rhs, guard);
269  }
270  else
271  {
272  // turn
273  // a[i]=e
274  // into
275  // a'==a WITH [i:=e]
276  const with_exprt new_rhs{lhs_array, lhs_index, rhs};
277  const expr_skeletont new_skeleton =
278  full_lhs.compose(expr_skeletont::remove_op0(lhs));
279  assign_rec(lhs_array, new_skeleton, new_rhs, guard);
280  }
281 }
282 
283 template <bool use_update>
285  const member_exprt &lhs,
286  const expr_skeletont &full_lhs,
287  const exprt &rhs,
288  exprt::operandst &guard)
289 {
290  // Symbolic execution of a struct member assignment.
291 
292  // lhs must be member operand, which
293  // takes one operand, which must be a structure.
294 
295  exprt lhs_struct = lhs.op();
296 
297  // typecasts involved? C++ does that for inheritance.
298  if(lhs_struct.id()==ID_typecast)
299  {
300  if(to_typecast_expr(lhs_struct).op().id() == ID_null_object)
301  {
302  // ignore, and give up
303  return;
304  }
305  else
306  {
307  // remove the type cast, we assume that the member is there
308  exprt tmp = to_typecast_expr(lhs_struct).op();
309 
310  if(tmp.type().id() == ID_struct || tmp.type().id() == ID_struct_tag)
311  lhs_struct=tmp;
312  else
313  return; // ignore and give up
314  }
315  }
316 
317  const irep_idt &component_name=lhs.get_component_name();
318 
319  if(use_update)
320  {
321  // turn
322  // a.c=e
323  // into
324  // a'==UPDATE(a, .c, e)
325  const update_exprt new_rhs{
326  lhs_struct, member_designatort(component_name), rhs};
327  const expr_skeletont new_skeleton =
328  full_lhs.compose(expr_skeletont::remove_op0(lhs));
329  assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
330  }
331  else
332  {
333  // turn
334  // a.c=e
335  // into
336  // a'==a WITH [c:=e]
337 
338  with_exprt new_rhs(lhs_struct, exprt(ID_member_name), rhs);
339  new_rhs.where().set(ID_component_name, component_name);
340  const expr_skeletont new_skeleton =
341  full_lhs.compose(expr_skeletont::remove_op0(lhs));
342  assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
343  }
344 }
345 
347  const if_exprt &lhs,
348  const expr_skeletont &full_lhs,
349  const exprt &rhs,
350  exprt::operandst &guard)
351 {
352  // we have (c?a:b)=e;
353 
354  guard.push_back(lhs.cond());
355  assign_rec(lhs.true_case(), full_lhs, rhs, guard);
356  guard.pop_back();
357 
358  guard.push_back(not_exprt(lhs.cond()));
359  assign_rec(lhs.false_case(), full_lhs, rhs, guard);
360  guard.pop_back();
361 }
362 
364  const byte_extract_exprt &lhs,
365  const expr_skeletont &full_lhs,
366  const exprt &rhs,
367  exprt::operandst &guard)
368 {
369  // we have byte_extract_X(object, offset)=value
370  // turn into object=byte_update_X(object, offset, value)
371 
373  if(lhs.id()==ID_byte_extract_little_endian)
374  byte_update_id = ID_byte_update_little_endian;
375  else if(lhs.id()==ID_byte_extract_big_endian)
376  byte_update_id = ID_byte_update_big_endian;
377  else
378  UNREACHABLE;
379 
380  const byte_update_exprt new_rhs{byte_update_id, lhs.op(), lhs.offset(), rhs};
381  const expr_skeletont new_skeleton =
382  full_lhs.compose(expr_skeletont::remove_op0(lhs));
383  assign_rec(lhs.op(), new_skeleton, new_rhs, guard);
384 }
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Complex constructor from a pair of numbers.
Definition: std_expr.h:1622
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1735
Real part of the expression describing a complex number.
Definition: std_expr.h:1690
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
expr_skeletont compose(expr_skeletont other) const
Replace the missing part of the current skeleton by another skeleton, ending in a bigger skeleton cor...
static expr_skeletont remove_op0(exprt e)
Create a skeleton by removing the first operand of e.
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
void field_assignments(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &lhs, symex_targett &target, bool allow_pointer_unsoundness)
Assign to the individual fields of a non-expanded symbol lhs.
NODISCARD exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
guardt guard
Definition: goto_state.h:54
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:67
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:47
std::stack< bool > record_events
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
NODISCARD renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
field_sensitivityt field_sensitivity
symex_targett::sourcet source
exprt as_expr() const
Definition: guard_expr.h:49
The trinary if-then-else operator.
Definition: std_expr.h:2087
exprt & true_case()
Definition: std_expr.h:2114
exprt & false_case()
Definition: std_expr.h:2124
exprt & cond()
Definition: std_expr.h:2104
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const std::string & id_string() const
Definition: irep.h:410
const irep_idt & id() const
Definition: irep.h:407
Extract member of struct or union.
Definition: std_expr.h:2528
const exprt & struct_op() const
Definition: std_expr.h:2558
irep_idt get_component_name() const
Definition: std_expr.h:2542
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
Boolean negation.
Definition: std_expr.h:2042
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
irep_idt get_object_name() const
Struct constructor from list of elements.
Definition: std_expr.h:1583
const componentst & components() const
Definition: std_types.h:142
const irep_idt & get_identifier() const
Definition: std_expr.h:110
void assign_byte_extract(const byte_extract_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_if(const if_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
const symex_configt & symex_config
Definition: symex_assign.h:62
void assign_non_struct_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
goto_symex_statet & state
Definition: symex_assign.h:59
void assign_array(const index_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
symex_targett & target
Definition: symex_assign.h:63
void assign_rec(const exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
Record the assignment of value rhs to variable lhs in state and add the equation to target: lhs#{n+1}...
void assign_struct_member(const member_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
symex_targett::assignment_typet assignment_type
Definition: symex_assign.h:60
const namespacet & ns
Definition: symex_assign.h:61
void assign_from_struct(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const struct_exprt &rhs, const exprt::operandst &guard)
Assign a struct expression to a symbol.
void assign_typecast(const typecast_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
Write to a local variable.
Semantic type conversion.
Definition: std_expr.h:1781
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
The type of an expression, extends irept.
Definition: type.h:28
const exprt & op() const
Definition: std_expr.h:294
Thrown when we encounter an instruction, parameters to an instruction etc.
Operator to update elements in structs and arrays.
Definition: std_expr.h:2357
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
Definition: value_set.cpp:1713
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
exprt & where()
Definition: std_expr.h:2193
Expression skeleton.
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:292
Deprecated expression utility functions.
Symbolic Execution.
Symbolic Execution.
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
exprt get_original_name(exprt expr)
Undo all levels of renaming.
bool check_renaming(const typet &type)
Check that type is correctly renamed to level 2 and return true in case an error is detected.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
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
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1716
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1606
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1761
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1829
Assignment from the rhs value to the lhs variable.
ssa_exprt lhs
expr_skeletont original_lhs_skeleton
Skeleton to reconstruct the original lhs in the assignment.
bool allow_pointer_unsoundness
Definition: symex_config.h:25
bool constant_propagation
Definition: symex_config.h:27
bool run_validation_checks
Should the additional validation checks be run? If this flag is set the checks for renaming (both lev...
Definition: symex_config.h:44
constexpr bool use_update()
Symbolic Execution of assignments.
irep_idt byte_update_id()