cprover
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>
18#include <util/nodiscard.h>
20#include <util/simplify_expr.h>
21
22#include "expr_skeleton.h"
23#include "path_storage.h"
24#include "symex_assign.h"
26
28
33static void
34process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
35{
36 // This may change the type of the expression!
37
38 if(expr.id()==ID_if)
39 {
40 if_exprt &if_expr=to_if_expr(expr);
41 process_array_expr(if_expr.true_case(), do_simplify, ns);
42 process_array_expr(if_expr.false_case(), do_simplify, ns);
43
44 if(if_expr.true_case() != if_expr.false_case())
45 {
47 if_expr.false_case(),
49 if_expr.true_case().type());
50
51 if_expr.false_case().swap(be);
52 }
53
54 if_expr.type()=if_expr.true_case().type();
55 }
56 else if(expr.id()==ID_address_of)
57 {
58 // strip
59 exprt tmp = to_address_of_expr(expr).object();
60 expr.swap(tmp);
61 process_array_expr(expr, do_simplify, ns);
62 }
63 else if(
64 is_ssa_expr(expr) && to_ssa_expr(expr).get_original_expr().id() == ID_index)
65 {
66 const ssa_exprt &ssa=to_ssa_expr(expr);
67 const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
68 exprt tmp=index_expr.array();
69 expr.swap(tmp);
70
71 process_array_expr(expr, do_simplify, ns);
72 }
73 else if(expr.id() != ID_symbol)
74 {
76 ode.build(expr, ns);
77
78 expr = ode.root_object();
79
80 // If we arrive at a void-typed object (typically the result of failing to
81 // dereference a void* pointer) there is nothing else to be done - it has
82 // void-type and the caller needs to handle this case gracefully.
83 if(expr.type().id() == ID_empty)
84 return;
85
86 if(!ode.offset().is_zero())
87 {
88 if(expr.type().id() != ID_array)
89 {
90 auto array_size = size_of_expr(expr.type(), ns);
91 CHECK_RETURN(array_size.has_value());
92 if(do_simplify)
93 simplify(array_size.value(), ns);
94 expr = make_byte_extract(
95 expr,
97 array_typet(char_type(), array_size.value()));
98 }
99
100 // given an array type T[N], i.e., an array of N elements of type T, and a
101 // byte offset B, compute the array offset B/sizeof(T) and build a new
102 // type T[N-(B/sizeof(T))]
103 const array_typet &prev_array_type = to_array_type(expr.type());
104 const typet &array_size_type = prev_array_type.size().type();
105 const typet &subtype = prev_array_type.element_type();
106
107 exprt new_offset =
108 typecast_exprt::conditional_cast(ode.offset(), array_size_type);
109 auto subtype_size_opt = size_of_expr(subtype, ns);
110 CHECK_RETURN(subtype_size_opt.has_value());
112 subtype_size_opt.value(), array_size_type);
113 new_offset = div_exprt(new_offset, subtype_size);
114 minus_exprt subtraction{prev_array_type.size(), new_offset};
115 if_exprt new_size{
117 subtraction, ID_ge, from_integer(0, subtraction.type())},
118 subtraction,
119 from_integer(0, subtraction.type())};
120 if(do_simplify)
121 simplify(new_size, ns);
122
123 array_typet new_array_type(subtype, new_size);
124
125 expr = make_byte_extract(expr, ode.offset(), new_array_type);
126 }
127 }
128}
129
131{
132 symex_dereference_statet symex_dereference_state(state, ns);
133
135 ns, state.symbol_table, symex_dereference_state, language_mode, false, log);
136
137 expr = dereference.dereference(expr, symex_config.show_points_to_sets);
138 lift_lets(state, expr);
139
141}
142
144static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
145{
146 Forall_operands(it, expr)
148
149 if(expr.id()==ID_byte_extract_big_endian ||
150 expr.id()==ID_byte_extract_little_endian)
151 {
153 if(be.op().id()==ID_symbol &&
154 to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object))
155 return;
156
158 ode.build(expr, ns);
159
160 be.op()=ode.root_object();
161 be.offset()=ode.offset();
162 }
163}
164
165static void
167{
168 if(expr.id() == ID_side_effect && expr.get(ID_statement) == ID_nondet)
169 {
170 expr = build_symex_nondet(expr.type(), expr.source_location());
171 }
172 else
173 {
174 Forall_operands(it, expr)
175 replace_nondet(*it, build_symex_nondet);
176 }
177}
178
179void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
180{
181 exprt let_value = clean_expr(let_expr.value(), state, false);
182 let_value = state.rename(std::move(let_value), ns).get();
183 do_simplify(let_value);
184
185 exprt::operandst value_assignment_guard;
188 .assign_symbol(
189 to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),
191 let_value,
192 value_assignment_guard);
193
194 // Schedule the bound variable to be cleaned up at the end of symex_step:
195 instruction_local_symbols.push_back(let_expr.symbol());
196}
197
199{
200 for(auto it = rhs.depth_begin(), itend = rhs.depth_end(); it != itend;)
201 {
202 if(it->id() == ID_let)
203 {
204 // Visit post-order, so more-local definitions are made before usage:
205 exprt &replaced_expr = it.mutate();
206 let_exprt &replaced_let = to_let_expr(replaced_expr);
207 lift_lets(state, replaced_let.value());
208 lift_lets(state, replaced_let.where());
209
210 lift_let(state, replaced_let);
211 replaced_expr = replaced_let.where();
212
213 it.next_sibling_or_parent();
214 }
215 else if(it->id() == ID_exists || it->id() == ID_forall)
216 {
217 // expressions within exists/forall may depend on bound variables, we
218 // cannot safely lift let expressions out of those, just skip
219 it.next_sibling_or_parent();
220 }
221 else
222 ++it;
223 }
224}
225
227goto_symext::clean_expr(exprt expr, statet &state, const bool write)
228{
230 dereference(expr, state, write);
231 lift_lets(state, expr);
232
233 // make sure all remaining byte extract operations use the root
234 // object to avoid nesting of with/update and byte_update when on
235 // lhs
236 if(write)
238 return expr;
239}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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:124
bitvector_typet c_index_type()
Definition: c_types.cpp:16
exprt & object()
Definition: pointer_expr.h:370
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
Expression of type type extracted from some object op starting at position offset (given in number of...
Division.
Definition: std_expr.h:1064
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
depth_iteratort depth_end()
Definition: expr.cpp:267
depth_iteratort depth_begin()
Definition: expr.cpp:265
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
const source_locationt & source_location() const
Definition: expr.h:230
Central data structure: state.
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...
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
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:226
void lift_let(statet &state, const let_exprt &let_expr)
Execute a single let expression, which should not have any nested let expressions (use lift_lets inst...
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:788
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:251
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:243
void lift_lets(statet &, exprt &)
Execute any let expressions in expr using symex_assignt::assign_symbol.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:34
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:263
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:170
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
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:260
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:2226
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 & array()
Definition: std_expr.h:1353
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
A let expression.
Definition: std_expr.h:2973
exprt & value()
convenience accessor for the value of a single binding
Definition: std_expr.h:3028
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3066
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition: std_expr.h:3012
Binary minus.
Definition: std_expr.h:973
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.
Definition: pointer_expr.h:167
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)
symex_nondet_generatort build_symex_nondet
Counter for nondet objects, which require unique names.
Definition: path_storage.h:94
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 for symex assignment.
Definition: symex_assign.h:26
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
Functor generating fresh nondet symbols.
Definition: path_storage.h:23
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
Wrapper for a function dereferencing pointer expressions using a value set.
#define Forall_operands(it, expr)
Definition: expr.h:25
Forward depth-first search iterators These iterators' copy operations are expensive,...
Expression skeleton.
Symbolic Execution.
#define NODISCARD
Definition: nodiscard.h:22
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.
Definition: pointer_expr.h:398
optionalt< 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:1391
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3097
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
bool show_points_to_sets
Definition: symex_config.h:49
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.
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.
Pointer Dereferencing.