cprover
symex_assign.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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
27constexpr 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
109struct 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
197
200 l2_lhs,
201 l2_full_lhs,
202 get_original_name(l2_full_lhs),
203 assignment.rhs,
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());
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
247template <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
284template <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
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
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...
std::stack< bool > record_events
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 & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const std::string & id_string() const
Definition: irep.h:399
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
Definition: ssa_expr.cpp:144
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
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
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 struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1745
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
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 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_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()