cprover
Loading...
Searching...
No Matches
symex_clean_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution of ANSI-C
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_symex.h"
13
14#include <util/arith_tools.h>
15#include <util/byte_operators.h>
16#include <util/c_types.h>
17#include <util/expr_iterator.h>
19#include <util/simplify_expr.h>
20
21#include "expr_skeleton.h"
22#include "path_storage.h"
23#include "symex_assign.h"
25
27
32static void
33process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
34{
35 // This may change the type of the expression!
36
37 if(expr.id()==ID_if)
38 {
39 if_exprt &if_expr=to_if_expr(expr);
40 process_array_expr(if_expr.true_case(), do_simplify, ns);
41 process_array_expr(if_expr.false_case(), do_simplify, ns);
42
43 if(if_expr.true_case() != if_expr.false_case())
44 {
46 if_expr.false_case(),
48 if_expr.true_case().type());
49
50 if_expr.false_case().swap(be);
51 }
52
53 if_expr.type()=if_expr.true_case().type();
54 }
55 else if(expr.id()==ID_address_of)
56 {
57 // strip
58 exprt tmp = to_address_of_expr(expr).object();
59 expr.swap(tmp);
60 process_array_expr(expr, do_simplify, ns);
61 }
62 else if(
63 is_ssa_expr(expr) && to_ssa_expr(expr).get_original_expr().id() == ID_index)
64 {
65 const ssa_exprt &ssa=to_ssa_expr(expr);
66 const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
67 exprt tmp=index_expr.array();
68 expr.swap(tmp);
69
70 process_array_expr(expr, do_simplify, ns);
71 }
72 else if(expr.id() != ID_symbol)
73 {
75 ode.build(expr, ns);
76
77 expr = ode.root_object();
78
79 // If we arrive at a void-typed object (typically the result of failing to
80 // dereference a void* pointer) there is nothing else to be done - it has
81 // void-type and the caller needs to handle this case gracefully.
82 if(expr.type().id() == ID_empty)
83 return;
84
85 if(!ode.offset().is_zero())
86 {
87 if(expr.type().id() != ID_array)
88 {
89 auto array_size = size_of_expr(expr.type(), ns);
90 CHECK_RETURN(array_size.has_value());
91 if(do_simplify)
92 simplify(array_size.value(), ns);
93 expr = make_byte_extract(
94 expr,
96 array_typet(char_type(), array_size.value()));
97 }
98
99 // given an array type T[N], i.e., an array of N elements of type T, and a
100 // byte offset B, compute the array offset B/sizeof(T) and build a new
101 // type T[N-(B/sizeof(T))]
102 const array_typet &prev_array_type = to_array_type(expr.type());
103 const typet &array_size_type = prev_array_type.size().type();
104 const typet &subtype = prev_array_type.element_type();
105
106 exprt new_offset =
107 typecast_exprt::conditional_cast(ode.offset(), array_size_type);
108 auto subtype_size_opt = size_of_expr(subtype, ns);
109 CHECK_RETURN(subtype_size_opt.has_value());
111 subtype_size_opt.value(), array_size_type);
112 new_offset = div_exprt(new_offset, subtype_size);
113 minus_exprt subtraction{prev_array_type.size(), new_offset};
114 if_exprt new_size{
116 subtraction, ID_ge, from_integer(0, subtraction.type())},
117 subtraction,
118 from_integer(0, subtraction.type())};
119 if(do_simplify)
120 simplify(new_size, ns);
121
122 array_typet new_array_type(subtype, new_size);
123
124 expr = make_byte_extract(expr, ode.offset(), new_array_type);
125 }
126 }
127}
128
130{
131 symex_dereference_statet symex_dereference_state(state, ns);
132
134 ns,
135 state.symbol_table,
136 symex_dereference_state,
138 false,
139 log.get_message_handler());
140
141 expr = dereference.dereference(expr, symex_config.show_points_to_sets);
142 lift_lets(state, expr);
143
144 ::process_array_expr(expr, symex_config.simplify_opt, ns);
145}
146
148static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
149{
150 Forall_operands(it, expr)
152
153 if(expr.id()==ID_byte_extract_big_endian ||
154 expr.id()==ID_byte_extract_little_endian)
155 {
157 if(be.op().id()==ID_symbol &&
158 to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object))
159 return;
160
162 ode.build(expr, ns);
163
164 be.op()=ode.root_object();
165 be.offset()=ode.offset();
166 }
167}
168
169static void
171{
172 if(expr.id() == ID_side_effect && expr.get(ID_statement) == ID_nondet)
173 {
174 expr = build_symex_nondet(expr.type(), expr.source_location());
175 }
176 else
177 {
178 Forall_operands(it, expr)
179 replace_nondet(*it, build_symex_nondet);
180 }
181}
182
183void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
184{
185 exprt let_value = clean_expr(let_expr.value(), state, false);
186 let_value = state.rename(std::move(let_value), ns).get();
187 do_simplify(let_value);
188
189 exprt::operandst value_assignment_guard;
190 symex_assignt{
192 state,
194 ns,
196 target}
197 .assign_symbol(
198 to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),
199 expr_skeletont{},
200 let_value,
201 value_assignment_guard);
202
203 // Schedule the bound variable to be cleaned up at the end of symex_step:
204 instruction_local_symbols.push_back(let_expr.symbol());
205}
206
207void goto_symext::lift_lets(statet &state, exprt &rhs)
208{
209 for(auto it = rhs.depth_begin(), itend = rhs.depth_end(); it != itend;)
210 {
211 if(it->id() == ID_let)
212 {
213 // Visit post-order, so more-local definitions are made before usage:
214 exprt &replaced_expr = it.mutate();
215 let_exprt &replaced_let = to_let_expr(replaced_expr);
216 lift_lets(state, replaced_let.value());
217 lift_lets(state, replaced_let.where());
218
219 lift_let(state, replaced_let);
220 replaced_expr = replaced_let.where();
221
222 it.next_sibling_or_parent();
223 }
224 else if(can_cast_expr<binding_exprt>(*it))
225 {
226 // expressions within exists/forall may depend on bound variables, we
227 // cannot safely lift let expressions out of those, just skip
228 it.next_sibling_or_parent();
229 }
230 else
231 ++it;
232 }
233}
234
235[[nodiscard]] exprt
236goto_symext::clean_expr(exprt expr, statet &state, const bool write)
237{
238 replace_nondet(expr, path_storage.build_symex_nondet);
239 dereference(expr, state, write);
240 lift_lets(state, expr);
241
242 // make sure all remaining byte extract operations use the root
243 // object to avoid nesting of with/update and byte_update when on
244 // lhs
245 if(write)
247 return expr;
248}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet char_type()
Definition c_types.cpp:106
bitvector_typet c_index_type()
Definition c_types.cpp:16
Arrays with given size.
Definition std_types.h:807
const exprt & size() const
Definition std_types.h:840
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
Expression of type type extracted from some object op starting at position offset (given in number of...
Division.
Definition std_expr.h:1157
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
depth_iteratort depth_end()
Definition expr.cpp:249
depth_iteratort depth_begin()
Definition expr.cpp:247
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:231
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
Definition goto_symex.h:40
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Definition goto_symex.h:241
symex_target_equationt & target
The equation that this execution is building up.
Definition goto_symex.h:266
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
Definition goto_symex.h:839
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition goto_symex.h:258
friend class symex_dereference_statet
Definition goto_symex.h:280
virtual void do_simplify(exprt &expr)
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
messaget log
The messaget to write log messages to.
Definition goto_symex.h:278
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition goto_symex.h:185
std::vector< symbol_exprt > instruction_local_symbols
Variables that should be killed at the end of the current symex_step invocation.
Definition goto_symex.h:275
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
The trinary if-then-else operator.
Definition std_expr.h:2375
exprt & false_case()
Definition std_expr.h:2412
exprt & true_case()
Definition std_expr.h:2402
Array index operator.
Definition std_expr.h:1470
exprt & array()
Definition std_expr.h:1500
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
A let expression.
Definition std_expr.h:3209
exprt & value()
convenience accessor for the value of a single binding
Definition std_expr.h:3264
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3302
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition std_expr.h:3248
Binary minus.
Definition std_expr.h:1061
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
Split an expression into a base object and a (byte) offset.
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
const exprt & get_original_expr() const
Definition ssa_expr.h:33
Functor generating fresh nondet symbols.
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
Wrapper for a function dereferencing pointer expressions using a value set.
#define Forall_operands(it, expr)
Definition expr.h:27
Forward depth-first search iterators These iterators' copy operations are expensive,...
Expression skeleton.
Symbolic Execution.
Storage of symbolic execution paths to resume.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
@ L1
Definition renamed.h:24
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
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
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
bool can_cast_expr< binding_exprt >(const exprt &base)
Definition std_expr.h:3163
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3333
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2455
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
Symbolic Execution of assignments.
static void process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
Given an expression, find the root object and the offset into it.
static void replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
Rewrite index/member expressions in byte_extract to offset.
Symbolic Execution of ANSI-C.
unsigned int statet
Pointer Dereferencing.