cprover
Loading...
Searching...
No Matches
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 <util/byte_operators.h>
15#include <util/expr_util.h>
16#include <util/pointer_expr.h>
17#include <util/range.h>
18
19#include "expr_skeleton.h"
20#include "goto_symex_state.h"
21#include "symex_config.h"
22
23// We can either use with_exprt or update_exprt when building expressions that
24// modify components of an array or a struct. Set USE_UPDATE to use
25// update_exprt.
26// #define USE_UPDATE
27
28constexpr bool use_update()
29{
30#ifdef USE_UPDATE
31 return true;
32#else
33 return false;
34#endif
35}
36
42{
44 {
45 if(
46 const auto &index =
48 {
49 if(index->array().id() == ID_string_constant && index->index().is_zero())
50 {
51 return true;
52 }
53 }
54 }
55 return false;
56}
57
59 const exprt &lhs,
60 const expr_skeletont &full_lhs,
61 const exprt &rhs,
63{
64 if(is_ssa_expr(lhs))
65 {
66 assign_symbol(to_ssa_expr(lhs), full_lhs, rhs, guard);
67
68 // Allocate shadow memory
69 if(shadow_memory.has_value())
70 {
73 {
74 shadow_memory->symex_field_static_init_string_constant(
75 state, to_ssa_expr(lhs), rhs);
76 }
77 else
78 {
79 shadow_memory->symex_field_static_init(state, to_ssa_expr(lhs));
80 }
81 }
82 }
83 else if(lhs.id() == ID_index)
85 else if(lhs.id()==ID_member)
86 {
87 const typet &type = to_member_expr(lhs).struct_op().type();
88 if(type.id() == ID_struct || type.id() == ID_struct_tag)
89 {
91 to_member_expr(lhs), full_lhs, rhs, guard);
92 }
93 else if(type.id() == ID_union || type.id() == ID_union_tag)
94 {
95 // should have been replaced by byte_extract
97 "assign_rec: unexpected assignment to union member");
98 }
99 else
101 "assign_rec: unexpected assignment to member of '" + type.id_string() +
102 "'");
103 }
104 else if(lhs.id()==ID_if)
105 assign_if(to_if_expr(lhs), full_lhs, rhs, guard);
106 else if(lhs.id()==ID_typecast)
107 assign_typecast(to_typecast_expr(lhs), full_lhs, rhs, guard);
109 {
110 // ignore
111 }
112 else if(lhs.id()==ID_byte_extract_little_endian ||
114 {
115 assign_byte_extract(to_byte_extract_expr(lhs), full_lhs, rhs, guard);
116 }
117 else if(lhs.id() == ID_complex_real)
118 {
119 // this is stuff like __real__ x = 1;
121
123
126
127 assign_rec(complex_real_expr.op(), full_lhs, new_rhs, guard);
128 }
129 else if(lhs.id() == ID_complex_imag)
130 {
132
134
137
138 assign_rec(complex_imag_expr.op(), full_lhs, new_rhs, guard);
139 }
140 else
142 "assignment to '" + lhs.id_string() + "' not handled");
143}
144
153
166 const ssa_exprt &lhs, // L1
167 const expr_skeletont &full_lhs,
168 const struct_exprt &rhs,
169 const exprt::operandst &guard)
170{
171 const auto &components = to_struct_type(ns.follow(lhs.type())).components();
172 PRECONDITION(rhs.operands().size() == components.size());
173
174 for(const auto &comp_rhs : make_range(components).zip(rhs.operands()))
175 {
176 const auto &comp = comp_rhs.first;
178 ns, state, member_exprt{lhs, comp.get_name(), comp.type()}, true);
179 INVARIANT(
180 lhs_field.id() == ID_symbol,
181 "member of symbol should be susceptible to field-sensitivity");
182
183 assign_symbol(to_ssa_expr(lhs_field), full_lhs, comp_rhs.second, guard);
184 }
185}
186
188 const ssa_exprt &lhs, // L1
189 const expr_skeletont &full_lhs,
190 const exprt &rhs,
191 const exprt::operandst &guard)
192{
193 exprt l2_rhs =
194 state
195 .rename(
196 // put assignment guard into the rhs
197 guard.empty()
198 ? rhs
199 : static_cast<exprt>(if_exprt{conjunction(guard), rhs, lhs}),
200 ns)
201 .get();
202
203 assignmentt assignment{lhs, full_lhs, l2_rhs};
204
205 if(symex_config.simplify_opt)
206 assignment.rhs = simplify_expr(std::move(assignment.rhs), ns);
207
208 const ssa_exprt l2_lhs = state
209 .assignment(
210 assignment.lhs,
211 assignment.rhs,
212 ns,
213 symex_config.simplify_opt,
214 symex_config.constant_propagation,
215 symex_config.allow_pointer_unsoundness)
216 .get();
217
218 state.record_events.push(false);
219 // Note any other symbols mentioned in the skeleton are rvalues -- for example
220 // array indices -- and were renamed to L2 at the start of
221 // goto_symext::symex_assign.
222 const exprt l2_full_lhs = assignment.original_lhs_skeleton.apply(l2_lhs);
223 if(symex_config.run_validation_checks)
224 {
225 INVARIANT(
226 !check_renaming(l2_full_lhs), "l2_full_lhs should be renamed to L2");
227 }
228 state.record_events.pop();
229
231 ns.lookup(l2_lhs.get_object_name()).is_auxiliary &&
232 id2string(l2_lhs.get_object_name()).find(SHADOW_MEMORY_SYMBOL_PREFIX) !=
233 std::string::npos
236
239 l2_lhs,
242 assignment.rhs,
245
246 const ssa_exprt &l1_lhs = assignment.lhs;
248 {
249 // Split composite symbol lhs into its components
251 ns,
252 state,
253 l1_lhs,
254 assignment.rhs,
255 target,
256 symex_config.allow_pointer_unsoundness);
257 }
258}
259
261 const ssa_exprt &lhs, // L1
262 const expr_skeletont &full_lhs,
263 const exprt &rhs,
264 const exprt::operandst &guard)
265{
266 // Shortcut the common case of a whole-struct initializer:
267 if(rhs.id() == ID_struct)
268 assign_from_struct(lhs, full_lhs, to_struct_expr(rhs), guard);
269 else
270 assign_non_struct_symbol(lhs, full_lhs, rhs, guard);
271}
272
274 const typecast_exprt &lhs,
275 const expr_skeletont &full_lhs,
276 const exprt &rhs,
278{
279 // these may come from dereferencing on the lhs
282 full_lhs.compose(expr_skeletont::remove_op0(lhs));
284}
285
286template <bool use_update>
288 const index_exprt &lhs,
289 const expr_skeletont &full_lhs,
290 const exprt &rhs,
292{
293 const exprt &lhs_array=lhs.array();
294 const exprt &lhs_index=lhs.index();
295 const typet &lhs_index_type = lhs_array.type();
296
298
299 if(use_update)
300 {
301 // turn
302 // a[i]=e
303 // into
304 // a'==UPDATE(a, [i], e)
307 full_lhs.compose(expr_skeletont::remove_op0(lhs));
309 }
310 else
311 {
312 // turn
313 // a[i]=e
314 // into
315 // a'==a WITH [i:=e]
318 full_lhs.compose(expr_skeletont::remove_op0(lhs));
320 }
321}
322
323template <bool use_update>
325 const member_exprt &lhs,
326 const expr_skeletont &full_lhs,
327 const exprt &rhs,
329{
330 // Symbolic execution of a struct member assignment.
331
332 // lhs must be member operand, which
333 // takes one operand, which must be a structure.
334
335 exprt lhs_struct = lhs.op();
336
337 // typecasts involved? C++ does that for inheritance.
338 if(lhs_struct.id()==ID_typecast)
339 {
341 {
342 // ignore, and give up
343 return;
344 }
345 else
346 {
347 // remove the type cast, we assume that the member is there
349
350 if(tmp.type().id() == ID_struct || tmp.type().id() == ID_struct_tag)
352 else
353 return; // ignore and give up
354 }
355 }
356
357 const irep_idt &component_name=lhs.get_component_name();
358
359 if(use_update)
360 {
361 // turn
362 // a.c=e
363 // into
364 // a'==UPDATE(a, .c, e)
365 const update_exprt new_rhs{
366 lhs_struct, member_designatort(component_name), rhs};
368 full_lhs.compose(expr_skeletont::remove_op0(lhs));
370 }
371 else
372 {
373 // turn
374 // a.c=e
375 // into
376 // a'==a WITH [c:=e]
377
379 new_rhs.where().set(ID_component_name, component_name);
381 full_lhs.compose(expr_skeletont::remove_op0(lhs));
383 }
384}
385
387 const if_exprt &lhs,
388 const expr_skeletont &full_lhs,
389 const exprt &rhs,
391{
392 // we have (c?a:b)=e;
393
394 guard.push_back(lhs.cond());
395 assign_rec(lhs.true_case(), full_lhs, rhs, guard);
396 guard.pop_back();
397
398 guard.push_back(not_exprt(lhs.cond()));
399 assign_rec(lhs.false_case(), full_lhs, rhs, guard);
400 guard.pop_back();
401}
402
404 const byte_extract_exprt &lhs,
405 const expr_skeletont &full_lhs,
406 const exprt &rhs,
408{
409 // we have byte_extract_X(object, offset)=value
410 // turn into object=byte_update_X(object, offset, value)
411
415 else if(lhs.id()==ID_byte_extract_big_endian)
417 else
419
421 byte_update_id, lhs.op(), lhs.offset(), rhs, lhs.get_bits_per_byte()};
423 full_lhs.compose(expr_skeletont::remove_op0(lhs));
425}
static irep_idt byte_update_id()
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
static exprt guard(const exprt::operandst &guards, exprt cond)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Expression of type type extracted from some object op starting at position offset (given in number of...
std::size_t get_bits_per_byte() const
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:1858
Imaginary part of the expression describing a complex number.
Definition std_expr.h:1971
Real part of the expression describing a complex number.
Definition std_expr.h:1926
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Expression in which some part is missing and can be substituted for another expression.
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:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
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.
void field_assignments(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &lhs, const exprt &rhs, symex_targett &target, bool allow_pointer_unsoundness) const
Assign to the individual fields of a non-expanded symbol lhs.
NODISCARD bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
guardt guard
Definition goto_state.h:58
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:2323
exprt & cond()
Definition std_expr.h:2340
exprt & false_case()
Definition std_expr.h:2360
exprt & true_case()
Definition std_expr.h:2350
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
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:2794
irep_idt get_component_name() const
Definition std_expr.h:2816
Boolean negation.
Definition std_expr.h:2278
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
Struct constructor from list of elements.
Definition std_expr.h:1819
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
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
void assign_array(const index_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
symex_targett & target
void assign_rec(const exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
optionalt< shadow_memoryt > shadow_memory
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
const namespacet & ns
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:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:326
Thrown when we encounter an instruction, parameters to an instruction etc.
Operator to update elements in structs and arrays.
Definition std_expr.h:2608
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
Expression skeleton.
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Deprecated expression utility functions.
Symbolic Execution.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for Pointers.
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.
#define SHADOW_MEMORY_SYMBOL_PREFIX
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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:63
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1842
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:1997
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:1952
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:1102
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.
constexpr bool use_update()
static bool is_string_constant_initialization(const exprt &rhs)
Determine whether the RHS expression is a string constant initialization.
Symbolic Execution of assignments.
Symbolic Execution.