CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 {
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))]
103 const typet &array_size_type = prev_array_type.size().type();
104 const typet &subtype = prev_array_type.element_type();
105
108 auto subtype_size_opt = size_of_expr(subtype, ns);
109 CHECK_RETURN(subtype_size_opt.has_value());
118 from_integer(0, subtraction.type())};
119 if(do_simplify)
120 simplify(new_size, ns);
121
123
124 expr = make_byte_extract(expr, ode.offset(), new_array_type);
125 }
126 }
127}
128
130{
132
134 ns,
135 state.symbol_table,
138 false,
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 ||
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
184{
185 exprt let_value = clean_expr(let_expr.value(), state, false);
186 let_value = state.rename(std::move(let_value), ns).get();
188
192 state,
194 ns,
196 target}
197 .assign_symbol(
198 to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),
200 let_value,
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
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();
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
236goto_symext::clean_expr(exprt expr, statet &state, const bool write)
237{
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Arrays with given size.
Definition std_types.h:807
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
Expression in which some part is missing and can be substituted for another expression.
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
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:231
Central data structure: state.
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:241
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:810
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
void lift_lets(statet &, exprt &)
Execute any let expressions in expr using symex_assignt::assign_symbol.
virtual void do_simplify(exprt &expr)
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
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: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:2497
Array index operator.
Definition std_expr.h:1470
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:3331
message_handlert & get_message_handler()
Definition message.h:183
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.
symex_nondet_generatort build_symex_nondet
Counter for nondet objects, which require unique names.
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
Functor for symex assignment.
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
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
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3455
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
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.
ssize_t write(int fildes, const void *buf, size_t nbyte)
Definition unistd.c:195
Pointer Dereferencing.