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_state.h"
16 #include <util/byte_operators.h>
17 #include <util/expr_util.h>
18 #include <util/range.h>
19 
20 #include "symex_config.h"
21 
22 // We can either use with_exprt or update_exprt when building expressions that
23 // modify components of an array or a struct. Set USE_UPDATE to use
24 // update_exprt.
25 // #define USE_UPDATE
26 
27 constexpr bool use_update()
28 {
29 #ifdef USE_UPDATE
30  return true;
31 #else
32  return false;
33 #endif
34 }
35 
37  const exprt &lhs,
38  const expr_skeletont &full_lhs,
39  const exprt &rhs,
40  exprt::operandst &guard)
41 {
42  if(is_ssa_expr(lhs))
43  {
44  assign_symbol(to_ssa_expr(lhs), full_lhs, rhs, guard);
45  }
46  else if(lhs.id() == ID_index)
47  assign_array<use_update()>(to_index_expr(lhs), full_lhs, rhs, guard);
48  else if(lhs.id()==ID_member)
49  {
50  const typet &type = to_member_expr(lhs).struct_op().type();
51  if(type.id() == ID_struct || type.id() == ID_struct_tag)
52  {
53  assign_struct_member<use_update()>(
54  to_member_expr(lhs), full_lhs, rhs, guard);
55  }
56  else if(type.id() == ID_union || type.id() == ID_union_tag)
57  {
58  // should have been replaced by byte_extract
60  "assign_rec: unexpected assignment to union member");
61  }
62  else
64  "assign_rec: unexpected assignment to member of '" + type.id_string() +
65  "'");
66  }
67  else if(lhs.id()==ID_if)
68  assign_if(to_if_expr(lhs), full_lhs, rhs, guard);
69  else if(lhs.id()==ID_typecast)
70  assign_typecast(to_typecast_expr(lhs), full_lhs, rhs, guard);
72  {
73  // ignore
74  }
75  else if(lhs.id()==ID_byte_extract_little_endian ||
76  lhs.id()==ID_byte_extract_big_endian)
77  {
78  assign_byte_extract(to_byte_extract_expr(lhs), full_lhs, rhs, guard);
79  }
80  else if(lhs.id() == ID_complex_real)
81  {
82  // this is stuff like __real__ x = 1;
83  const complex_real_exprt &complex_real_expr = to_complex_real_expr(lhs);
84 
85  const complex_imag_exprt complex_imag_expr(complex_real_expr.op());
86 
87  complex_exprt new_rhs(
88  rhs, complex_imag_expr, to_complex_type(complex_real_expr.op().type()));
89 
90  assign_rec(complex_real_expr.op(), full_lhs, new_rhs, guard);
91  }
92  else if(lhs.id() == ID_complex_imag)
93  {
94  const complex_imag_exprt &complex_imag_expr = to_complex_imag_expr(lhs);
95 
96  const complex_real_exprt complex_real_expr(complex_imag_expr.op());
97 
98  complex_exprt new_rhs(
99  complex_real_expr, rhs, to_complex_type(complex_imag_expr.op().type()));
100 
101  assign_rec(complex_imag_expr.op(), full_lhs, new_rhs, guard);
102  }
103  else
105  "assignment to '" + lhs.id_string() + "' not handled");
106 }
107 
109 struct assignmentt final
110 {
115 };
116 
129  const ssa_exprt &lhs, // L1
130  const expr_skeletont &full_lhs,
131  const struct_exprt &rhs,
132  const exprt::operandst &guard)
133 {
134  const auto &components = to_struct_type(ns.follow(lhs.type())).components();
135  PRECONDITION(rhs.operands().size() == components.size());
136 
137  for(const auto &comp_rhs : make_range(components).zip(rhs.operands()))
138  {
139  const auto &comp = comp_rhs.first;
140  const exprt lhs_field = state.field_sensitivity.apply(
141  ns, state, member_exprt{lhs, comp.get_name(), comp.type()}, true);
142  INVARIANT(
143  lhs_field.id() == ID_symbol,
144  "member of symbol should be susceptible to field-sensitivity");
145 
146  assign_symbol(to_ssa_expr(lhs_field), full_lhs, comp_rhs.second, guard);
147  }
148 }
149 
151  const ssa_exprt &lhs, // L1
152  const expr_skeletont &full_lhs,
153  const exprt &rhs,
154  const exprt::operandst &guard)
155 {
156  exprt l2_rhs =
157  state
158  .rename(
159  // put assignment guard into the rhs
160  guard.empty()
161  ? rhs
162  : static_cast<exprt>(if_exprt{conjunction(guard), rhs, lhs}),
163  ns)
164  .get();
165 
166  assignmentt assignment{lhs, full_lhs, l2_rhs};
167 
169  assignment.rhs = simplify_expr(std::move(assignment.rhs), ns);
170 
171  const ssa_exprt l2_lhs = state
172  .assignment(
173  assignment.lhs,
174  assignment.rhs,
175  ns,
179  .get();
180 
181  state.record_events.push(false);
182  // Note any other symbols mentioned in the skeleton are rvalues -- for example
183  // array indices -- and were renamed to L2 at the start of
184  // goto_symext::symex_assign.
185  const exprt l2_full_lhs = assignment.original_lhs_skeleton.apply(l2_lhs);
187  {
188  INVARIANT(
189  !check_renaming(l2_full_lhs), "l2_full_lhs should be renamed to L2");
190  }
191  state.record_events.pop();
192 
193  auto current_assignment_type =
194  ns.lookup(l2_lhs.get_object_name()).is_auxiliary
196  : assignment_type;
197 
200  l2_lhs,
201  l2_full_lhs,
202  get_original_name(l2_full_lhs),
203  assignment.rhs,
204  state.source,
205  current_assignment_type);
206 
207  const ssa_exprt &l1_lhs = assignment.lhs;
209  {
210  // Split composite symbol lhs into its components
213  // Erase the composite symbol from our working state. Note that we need to
214  // have it in the propagation table and the value set while doing the field
215  // assignments, thus we cannot skip putting it in there above.
216  state.propagation.erase_if_exists(l1_lhs.get_identifier());
217  state.value_set.erase_symbol(l1_lhs, ns);
218  }
219 }
220 
222  const ssa_exprt &lhs, // L1
223  const expr_skeletont &full_lhs,
224  const exprt &rhs,
225  const exprt::operandst &guard)
226 {
227  // Shortcut the common case of a whole-struct initializer:
228  if(rhs.id() == ID_struct)
229  assign_from_struct(lhs, full_lhs, to_struct_expr(rhs), guard);
230  else
231  assign_non_struct_symbol(lhs, full_lhs, rhs, guard);
232 }
233 
235  const typecast_exprt &lhs,
236  const expr_skeletont &full_lhs,
237  const exprt &rhs,
238  exprt::operandst &guard)
239 {
240  // these may come from dereferencing on the lhs
241  exprt rhs_typecasted = typecast_exprt::conditional_cast(rhs, lhs.op().type());
242  expr_skeletont new_skeleton =
243  full_lhs.compose(expr_skeletont::remove_op0(lhs));
244  assign_rec(lhs.op(), new_skeleton, rhs_typecasted, guard);
245 }
246 
247 template <bool use_update>
249  const index_exprt &lhs,
250  const expr_skeletont &full_lhs,
251  const exprt &rhs,
252  exprt::operandst &guard)
253 {
254  const exprt &lhs_array=lhs.array();
255  const exprt &lhs_index=lhs.index();
256  const typet &lhs_index_type = lhs_array.type();
257 
258  PRECONDITION(lhs_index_type.id() == ID_array);
259 
260  if(use_update)
261  {
262  // turn
263  // a[i]=e
264  // into
265  // a'==UPDATE(a, [i], e)
266  const update_exprt new_rhs{lhs_array, index_designatort(lhs_index), rhs};
267  const expr_skeletont new_skeleton =
268  full_lhs.compose(expr_skeletont::remove_op0(lhs));
269  assign_rec(lhs, new_skeleton, new_rhs, guard);
270  }
271  else
272  {
273  // turn
274  // a[i]=e
275  // into
276  // a'==a WITH [i:=e]
277  const with_exprt new_rhs{lhs_array, lhs_index, rhs};
278  const expr_skeletont new_skeleton =
279  full_lhs.compose(expr_skeletont::remove_op0(lhs));
280  assign_rec(lhs_array, new_skeleton, new_rhs, guard);
281  }
282 }
283 
284 template <bool use_update>
286  const member_exprt &lhs,
287  const expr_skeletont &full_lhs,
288  const exprt &rhs,
289  exprt::operandst &guard)
290 {
291  // Symbolic execution of a struct member assignment.
292 
293  // lhs must be member operand, which
294  // takes one operand, which must be a structure.
295 
296  exprt lhs_struct = lhs.op();
297 
298  // typecasts involved? C++ does that for inheritance.
299  if(lhs_struct.id()==ID_typecast)
300  {
301  if(to_typecast_expr(lhs_struct).op().id() == ID_null_object)
302  {
303  // ignore, and give up
304  return;
305  }
306  else
307  {
308  // remove the type cast, we assume that the member is there
309  exprt tmp = to_typecast_expr(lhs_struct).op();
310 
311  if(tmp.type().id() == ID_struct || tmp.type().id() == ID_struct_tag)
312  lhs_struct=tmp;
313  else
314  return; // ignore and give up
315  }
316  }
317 
318  const irep_idt &component_name=lhs.get_component_name();
319 
320  if(use_update)
321  {
322  // turn
323  // a.c=e
324  // into
325  // a'==UPDATE(a, .c, e)
326  const update_exprt new_rhs{
327  lhs_struct, member_designatort(component_name), rhs};
328  const expr_skeletont new_skeleton =
329  full_lhs.compose(expr_skeletont::remove_op0(lhs));
330  assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
331  }
332  else
333  {
334  // turn
335  // a.c=e
336  // into
337  // a'==a WITH [c:=e]
338 
339  with_exprt new_rhs(lhs_struct, exprt(ID_member_name), rhs);
340  new_rhs.where().set(ID_component_name, component_name);
341  const expr_skeletont new_skeleton =
342  full_lhs.compose(expr_skeletont::remove_op0(lhs));
343  assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
344  }
345 }
346 
348  const if_exprt &lhs,
349  const expr_skeletont &full_lhs,
350  const exprt &rhs,
351  exprt::operandst &guard)
352 {
353  // we have (c?a:b)=e;
354 
355  guard.push_back(lhs.cond());
356  assign_rec(lhs.true_case(), full_lhs, rhs, guard);
357  guard.pop_back();
358 
359  guard.push_back(not_exprt(lhs.cond()));
360  assign_rec(lhs.false_case(), full_lhs, rhs, guard);
361  guard.pop_back();
362 }
363 
365  const byte_extract_exprt &lhs,
366  const expr_skeletont &full_lhs,
367  const exprt &rhs,
368  exprt::operandst &guard)
369 {
370  // we have byte_extract_X(object, offset)=value
371  // turn into object=byte_update_X(object, offset, value)
372 
374  if(lhs.id()==ID_byte_extract_little_endian)
375  byte_update_id = ID_byte_update_little_endian;
376  else if(lhs.id()==ID_byte_extract_big_endian)
377  byte_update_id = ID_byte_update_big_endian;
378  else
379  UNREACHABLE;
380 
381  const byte_update_exprt new_rhs{byte_update_id, lhs.op(), lhs.offset(), rhs};
382  const expr_skeletont new_skeleton =
383  full_lhs.compose(expr_skeletont::remove_op0(lhs));
384  assign_rec(lhs.op(), new_skeleton, new_rhs, guard);
385 }
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:1761
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1874
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
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:92
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:58
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:71
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:51
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:46
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
const std::string & id_string() const
Definition: irep.h:399
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const irep_idt & id() const
Definition: irep.h:396
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
irep_idt get_component_name() const
Definition: std_expr.h:2681
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Boolean negation.
Definition: std_expr.h:2181
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:1722
const componentst & components() const
Definition: std_types.h:147
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
Thrown when we encounter an instruction, parameters to an instruction etc.
Operator to update elements in structs and arrays.
Definition: std_expr.h:2496
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
Definition: value_set.cpp:1780
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
exprt & where()
Definition: std_expr.h:2332
Expression skeleton.
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:291
Deprecated expression utility functions.
Symbolic Execution.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
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:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:34
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1855
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1745
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1900
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082
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.
Symbolic Execution.
static irep_idt byte_update_id()