CBMC
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/pointer_expr.h>
16#include <util/range.h>
17
18#include "expr_skeleton.h"
19#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 =
172 lhs.type().id() == ID_struct_tag
173 ? ns.follow_tag(to_struct_tag_type(lhs.type())).components()
174 : to_struct_type(lhs.type()).components();
175 PRECONDITION(rhs.operands().size() == components.size());
176
177 for(const auto &comp_rhs : make_range(components).zip(rhs.operands()))
178 {
179 const auto &comp = comp_rhs.first;
181 ns, state, member_exprt{lhs, comp.get_name(), comp.type()}, true);
182 INVARIANT(
183 lhs_field.id() == ID_symbol,
184 "member of symbol should be susceptible to field-sensitivity");
185
186 assign_symbol(to_ssa_expr(lhs_field), full_lhs, comp_rhs.second, guard);
187 }
188}
189
191 const ssa_exprt &lhs, // L1
192 const expr_skeletont &full_lhs,
193 const exprt &rhs,
194 const exprt::operandst &guard)
195{
196 exprt l2_rhs =
197 state
198 .rename(
199 // put assignment guard into the rhs
200 guard.empty()
201 ? rhs
202 : static_cast<exprt>(if_exprt{conjunction(guard), rhs, lhs}),
203 ns)
204 .get();
205
206 assignmentt assignment{lhs, full_lhs, l2_rhs};
207
208 if(symex_config.simplify_opt)
209 {
211 assignment.rhs);
212 }
213
214 const ssa_exprt l2_lhs = state
215 .assignment(
216 assignment.lhs,
217 assignment.rhs,
218 ns,
219 symex_config.simplify_opt,
220 symex_config.constant_propagation,
221 symex_config.allow_pointer_unsoundness)
222 .get();
223
224 state.record_events.push(false);
225 // Note any other symbols mentioned in the skeleton are rvalues -- for example
226 // array indices -- and were renamed to L2 at the start of
227 // goto_symext::symex_assign.
228 const exprt l2_full_lhs = assignment.original_lhs_skeleton.apply(l2_lhs);
229 if(symex_config.run_validation_checks)
230 {
231 INVARIANT(
232 !check_renaming(l2_full_lhs), "l2_full_lhs should be renamed to L2");
233 }
234 state.record_events.pop();
235
237 ns.lookup(l2_lhs.get_object_name()).is_auxiliary &&
238 id2string(l2_lhs.get_object_name()).find(SHADOW_MEMORY_SYMBOL_PREFIX) !=
239 std::string::npos
242
245 l2_lhs,
248 assignment.rhs,
251
252 const ssa_exprt &l1_lhs = assignment.lhs;
254 {
255 // Split composite symbol lhs into its components
257 ns,
258 state,
259 l1_lhs,
260 assignment.rhs,
261 target,
262 symex_config.allow_pointer_unsoundness);
263 }
264}
265
267 const ssa_exprt &lhs, // L1
268 const expr_skeletont &full_lhs,
269 const exprt &rhs,
270 const exprt::operandst &guard)
271{
272 // Shortcut the common case of a whole-struct initializer:
273 if(rhs.id() == ID_struct)
274 assign_from_struct(lhs, full_lhs, to_struct_expr(rhs), guard);
275 else
276 assign_non_struct_symbol(lhs, full_lhs, rhs, guard);
277}
278
280 const typecast_exprt &lhs,
281 const expr_skeletont &full_lhs,
282 const exprt &rhs,
284{
285 // these may come from dereferencing on the lhs
288 full_lhs.compose(expr_skeletont::remove_op0(lhs));
290}
291
292template <bool use_update>
294 const index_exprt &lhs,
295 const expr_skeletont &full_lhs,
296 const exprt &rhs,
298{
299 const exprt &lhs_array=lhs.array();
300 const exprt &lhs_index=lhs.index();
301 const typet &lhs_index_type = lhs_array.type();
302
304
305 if(use_update)
306 {
307 // turn
308 // a[i]=e
309 // into
310 // a'==UPDATE(a, [i], e)
313 full_lhs.compose(expr_skeletont::remove_op0(lhs));
315 }
316 else
317 {
318 // turn
319 // a[i]=e
320 // into
321 // a'==a WITH [i:=e]
324 full_lhs.compose(expr_skeletont::remove_op0(lhs));
326 }
327}
328
329template <bool use_update>
331 const member_exprt &lhs,
332 const expr_skeletont &full_lhs,
333 const exprt &rhs,
335{
336 // Symbolic execution of a struct member assignment.
337
338 // lhs must be member operand, which
339 // takes one operand, which must be a structure.
340
341 exprt lhs_struct = lhs.op();
342
343 // typecasts involved? C++ does that for inheritance.
344 if(lhs_struct.id()==ID_typecast)
345 {
347 {
348 // ignore, and give up
349 return;
350 }
351 else
352 {
353 // remove the type cast, we assume that the member is there
355
356 if(tmp.type().id() == ID_struct || tmp.type().id() == ID_struct_tag)
358 else
359 return; // ignore and give up
360 }
361 }
362
363 const irep_idt &component_name=lhs.get_component_name();
364
365 if(use_update)
366 {
367 // turn
368 // a.c=e
369 // into
370 // a'==UPDATE(a, .c, e)
371 const update_exprt new_rhs{
372 lhs_struct, member_designatort(component_name), rhs};
374 full_lhs.compose(expr_skeletont::remove_op0(lhs));
376 }
377 else
378 {
379 // turn
380 // a.c=e
381 // into
382 // a'==a WITH [c:=e]
383
385 new_rhs.where().set(ID_component_name, component_name);
387 full_lhs.compose(expr_skeletont::remove_op0(lhs));
389 }
390}
391
393 const if_exprt &lhs,
394 const expr_skeletont &full_lhs,
395 const exprt &rhs,
397{
398 // we have (c?a:b)=e;
399
400 guard.push_back(lhs.cond());
401 assign_rec(lhs.true_case(), full_lhs, rhs, guard);
402 guard.pop_back();
403
404 guard.push_back(not_exprt(lhs.cond()));
405 assign_rec(lhs.false_case(), full_lhs, rhs, guard);
406 guard.pop_back();
407}
408
410 const byte_extract_exprt &lhs,
411 const expr_skeletont &full_lhs,
412 const exprt &rhs,
414{
415 // we have byte_extract_X(object, offset)=value
416 // turn into object=byte_update_X(object, offset, value)
417
421 else if(lhs.id()==ID_byte_extract_big_endian)
423 else
425
427 byte_update_id, lhs.op(), lhs.offset(), rhs, lhs.get_bits_per_byte()};
429 full_lhs.compose(expr_skeletont::remove_op0(lhs));
431}
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:562
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:1916
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2027
Real part of the expression describing a complex number.
Definition std_expr.h:1984
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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
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.
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
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition goto_state.h:51
std::stack< bool > record_events
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)
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...
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:2502
exprt & cond()
Definition std_expr.h:2519
exprt & false_case()
Definition std_expr.h:2539
exprt & true_case()
Definition std_expr.h:2529
Array index operator.
Definition std_expr.h:1470
exprt & index()
Definition std_expr.h:1510
exprt & array()
Definition std_expr.h:1500
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2972
irep_idt get_component_name() const
Definition std_expr.h:2994
Boolean negation.
Definition std_expr.h:2459
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
Struct constructor from list of elements.
Definition std_expr.h:1877
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 irep_idt & language_mode
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)
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)
std::optional< shadow_memoryt > shadow_memory
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:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
Thrown when we encounter an instruction, parameters to an instruction etc.
Operator to update elements in structs and arrays.
Definition std_expr.h:2783
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
Expression skeleton.
Symbolic Execution.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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:522
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
#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(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:83
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_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:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2582
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:2053
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:2010
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
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.