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 <util/arith_tools.h>
13#include <util/byte_operators.h>
14#include <util/c_types.h>
15#include <util/expr_iterator.h>
17
19
20#include "expr_skeleton.h"
21#include "goto_symex.h"
22#include "path_storage.h"
23#include "symex_assign.h"
25
30static void process_array_expr(exprt &expr, const namespacet &ns)
31{
32 // This may change the type of the expression!
33
34 if(expr.id()==ID_if)
35 {
36 if_exprt &if_expr=to_if_expr(expr);
37 process_array_expr(if_expr.true_case(), ns);
38 process_array_expr(if_expr.false_case(), ns);
39
40 if(if_expr.true_case() != if_expr.false_case())
41 {
43 if_expr.false_case(),
45 if_expr.true_case().type());
46
47 if_expr.false_case().swap(be);
48 }
49
50 if_expr.type()=if_expr.true_case().type();
51 }
52 else if(expr.id()==ID_address_of)
53 {
54 // strip
55 exprt tmp = to_address_of_expr(expr).object();
56 expr.swap(tmp);
57 process_array_expr(expr, ns);
58 }
59 else if(
60 is_ssa_expr(expr) && to_ssa_expr(expr).get_original_expr().id() == ID_index)
61 {
62 const ssa_exprt &ssa=to_ssa_expr(expr);
63 const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
64 exprt tmp=index_expr.array();
65 expr.swap(tmp);
66
67 process_array_expr(expr, ns);
68 }
69 else if(expr.id() != ID_symbol)
70 {
72 ode.build(expr, ns);
73
74 expr = ode.root_object();
75
76 // If we arrive at a void-typed object (typically the result of failing to
77 // dereference a void* pointer) there is nothing else to be done - it has
78 // void-type and the caller needs to handle this case gracefully.
79 if(expr.type().id() == ID_empty)
80 return;
81
82 if(!ode.offset().is_zero())
83 {
84 if(expr.type().id() != ID_array)
85 {
86 auto array_size = size_of_expr(expr.type(), ns);
87 CHECK_RETURN(array_size.has_value());
88 expr = make_byte_extract(
89 expr,
91 array_typet(char_type(), array_size.value()));
92 }
93
94 // given an array type T[N], i.e., an array of N elements of type T, and a
95 // byte offset B, compute the array offset B/sizeof(T) and build a new
96 // type T[N-(B/sizeof(T))]
97 const array_typet &prev_array_type = to_array_type(expr.type());
98 const typet &array_size_type = prev_array_type.size().type();
99 const typet &subtype = prev_array_type.element_type();
100
101 exprt new_offset =
102 typecast_exprt::conditional_cast(ode.offset(), array_size_type);
103 auto subtype_size_opt = size_of_expr(subtype, ns);
104 CHECK_RETURN(subtype_size_opt.has_value());
106 subtype_size_opt.value(), array_size_type);
107 new_offset = div_exprt(new_offset, subtype_size);
108 minus_exprt subtraction{prev_array_type.size(), new_offset};
109 if_exprt new_size{
111 subtraction, ID_ge, from_integer(0, subtraction.type())},
112 subtraction,
113 from_integer(0, subtraction.type())};
114
115 array_typet new_array_type(subtype, new_size);
116
117 expr = make_byte_extract(expr, ode.offset(), new_array_type);
118 }
119 }
120}
121
123{
124 symex_dereference_statet symex_dereference_state(state, ns);
125
127 ns,
128 state.symbol_table,
129 symex_dereference_state,
131 false,
132 log.get_message_handler());
133
134 expr = dereference.dereference(expr, symex_config.show_points_to_sets);
135 lift_lets(state, expr);
136
138 do_simplify(expr, state.value_set);
139}
140
142static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
143{
144 Forall_operands(it, expr)
146
147 if(expr.id()==ID_byte_extract_big_endian ||
148 expr.id()==ID_byte_extract_little_endian)
149 {
151 if(be.op().id()==ID_symbol &&
152 to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object))
153 return;
154
156 ode.build(expr, ns);
157
158 be.op()=ode.root_object();
159 be.offset()=ode.offset();
160 }
161}
162
163static void
165{
166 if(expr.id() == ID_side_effect && expr.get(ID_statement) == ID_nondet)
167 {
168 expr = build_symex_nondet(expr.type(), expr.source_location());
169 }
170 else
171 {
172 Forall_operands(it, expr)
173 replace_nondet(*it, build_symex_nondet);
174 }
175}
176
177void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
178{
179 exprt let_value = clean_expr(let_expr.value(), state, false);
180 let_value = state.rename(std::move(let_value), ns).get();
181 do_simplify(let_value, state.value_set);
182
183 exprt::operandst value_assignment_guard;
184 symex_assignt{
186 state,
188 ns,
191 target}
192 .assign_symbol(
193 to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),
194 expr_skeletont{},
195 let_value,
196 value_assignment_guard);
197
198 // Schedule the bound variable to be cleaned up at the end of symex_step:
199 instruction_local_symbols.push_back(let_expr.symbol());
200}
201
202void goto_symext::lift_lets(statet &state, exprt &rhs)
203{
204 for(auto it = rhs.depth_begin(), itend = rhs.depth_end(); it != itend;)
205 {
206 if(it->id() == ID_let)
207 {
208 // Visit post-order, so more-local definitions are made before usage:
209 exprt &replaced_expr = it.mutate();
210 let_exprt &replaced_let = to_let_expr(replaced_expr);
211 lift_lets(state, replaced_let.value());
212 lift_lets(state, replaced_let.where());
213
214 lift_let(state, replaced_let);
215 replaced_expr = replaced_let.where();
216
217 it.next_sibling_or_parent();
218 }
219 else if(can_cast_expr<binding_exprt>(*it))
220 {
221 // expressions within exists/forall may depend on bound variables, we
222 // cannot safely lift let expressions out of those, just skip
223 it.next_sibling_or_parent();
224 }
225 else
226 ++it;
227 }
228}
229
230[[nodiscard]] exprt
231goto_symext::clean_expr(exprt expr, statet &state, const bool write)
232{
233 replace_nondet(expr, path_storage.build_symex_nondet);
234 dereference(expr, state, write);
235 lift_lets(state, expr);
236
237 // make sure all remaining byte extract operations use the root
238 // object to avoid nesting of with/update and byte_update when on
239 // lhs
240 if(write)
242 return expr;
243}
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
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition goto_state.h:51
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:41
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:242
symex_target_equationt & target
The equation that this execution is building up.
Definition goto_symex.h:267
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:840
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition goto_symex.h:259
friend class symex_dereference_statet
Definition goto_symex.h:281
virtual void do_simplify(exprt &expr, const value_sett &value_set)
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:279
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition goto_symex.h:186
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:276
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:2502
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 & 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:3332
exprt & value()
convenience accessor for the value of a single binding
Definition std_expr.h:3387
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3425
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition std_expr.h:3371
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:91
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
#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:3286
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3456
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2582
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 replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
static void process_array_expr(exprt &expr, const namespacet &ns)
Given an expression, find the root object and the offset into it.
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.