cprover
symex_clean_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: 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 "symex_assign.h"
25 
27 
32 static void
33 process_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  {
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(expr.id()==ID_symbol &&
64  expr.get_bool(ID_C_SSA_symbol) &&
65  to_ssa_expr(expr).get_original_expr().id()==ID_index)
66  {
67  const ssa_exprt &ssa=to_ssa_expr(expr);
68  const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
69  exprt tmp=index_expr.array();
70  expr.swap(tmp);
71 
72  process_array_expr(expr, do_simplify, ns);
73  }
74  else if(expr.id() != ID_symbol)
75  {
77  ode.build(expr, ns);
78 
79  expr = ode.root_object();
80 
81  // If we arrive at a void-typed object (typically the result of failing to
82  // dereference a void* pointer) there is nothing else to be done - it has
83  // void-type and the caller needs to handle this case gracefully.
84  if(expr.type().id() == ID_empty)
85  return;
86 
87  if(!ode.offset().is_zero())
88  {
89  if(expr.type().id() != ID_array)
90  {
91  auto array_size = size_of_expr(expr.type(), ns);
92  CHECK_RETURN(array_size.has_value());
93  if(do_simplify)
94  simplify(array_size.value(), ns);
95  expr = byte_extract_exprt(
97  expr,
99  array_typet(char_type(), array_size.value()));
100  }
101 
102  // given an array type T[N], i.e., an array of N elements of type T, and a
103  // byte offset B, compute the array offset B/sizeof(T) and build a new
104  // type T[N-(B/sizeof(T))]
105  const array_typet &prev_array_type = to_array_type(expr.type());
106  const typet &array_size_type = prev_array_type.size().type();
107  const typet &subtype = prev_array_type.subtype();
108 
109  exprt new_offset =
110  typecast_exprt::conditional_cast(ode.offset(), array_size_type);
111  auto subtype_size_opt = size_of_expr(subtype, ns);
112  CHECK_RETURN(subtype_size_opt.has_value());
114  subtype_size_opt.value(), array_size_type);
115  new_offset = div_exprt(new_offset, subtype_size);
116  minus_exprt new_size(prev_array_type.size(), new_offset);
117  if(do_simplify)
118  simplify(new_size, ns);
119 
120  array_typet new_array_type(subtype, new_size);
121 
122  expr =
124  byte_extract_id(),
125  expr,
126  ode.offset(),
127  new_array_type);
128  }
129  }
130 }
131 
133 {
134  symex_dereference_statet symex_dereference_state(state, ns);
135 
137  ns, state.symbol_table, symex_dereference_state, language_mode, false);
138 
139  expr = dereference.dereference(expr);
140  lift_lets(state, expr);
141 
143 }
144 
146 static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
147 {
148  Forall_operands(it, expr)
149  adjust_byte_extract_rec(*it, ns);
150 
151  if(expr.id()==ID_byte_extract_big_endian ||
152  expr.id()==ID_byte_extract_little_endian)
153  {
155  if(be.op().id()==ID_symbol &&
156  to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object))
157  return;
158 
160  ode.build(expr, ns);
161 
162  be.op()=ode.root_object();
163  be.offset()=ode.offset();
164  }
165 }
166 
167 static void
168 replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
169 {
170  if(expr.id() == ID_side_effect && expr.get(ID_statement) == ID_nondet)
171  {
172  expr = build_symex_nondet(expr.type(), expr.source_location());
173  }
174  else
175  {
176  Forall_operands(it, expr)
177  replace_nondet(*it, build_symex_nondet);
178  }
179 }
180 
181 void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
182 {
183  exprt let_value = clean_expr(let_expr.value(), state, false);
184  let_value = state.rename(std::move(let_value), ns).get();
185  do_simplify(let_value);
186 
187  exprt::operandst value_assignment_guard;
190  .assign_symbol(
191  to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),
192  expr_skeletont{},
193  let_value,
194  value_assignment_guard);
195 
196  // Schedule the bound variable to be cleaned up at the end of symex_step:
197  instruction_local_symbols.push_back(let_expr.symbol());
198 }
199 
201 {
202  for(auto it = rhs.depth_begin(), itend = rhs.depth_end(); it != itend;)
203  {
204  if(it->id() == ID_let)
205  {
206  // Visit post-order, so more-local definitions are made before usage:
207  exprt &replaced_expr = it.mutate();
208  let_exprt &replaced_let = to_let_expr(replaced_expr);
209  lift_lets(state, replaced_let.value());
210  lift_lets(state, replaced_let.where());
211 
212  lift_let(state, replaced_let);
213  replaced_expr = replaced_let.where();
214 
215  it.next_sibling_or_parent();
216  }
217  else if(it->id() == ID_exists || it->id() == ID_forall)
218  {
219  // expressions within exists/forall may depend on bound variables, we
220  // cannot safely lift let expressions out of those, just skip
221  it.next_sibling_or_parent();
222  }
223  else
224  ++it;
225  }
226 }
227 
229 goto_symext::clean_expr(exprt expr, statet &state, const bool write)
230 {
232  dereference(expr, state, write);
233  lift_lets(state, expr);
234 
235  // make sure all remaining byte extract operations use the root
236  // object to avoid nesting of with/update and byte_update when on
237  // lhs
238  if(write)
240  return expr;
241 }
goto_symext::clean_expr
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
Definition: symex_clean_expr.cpp:229
pointer_offset_size.h
Pointer Logic.
symex_nondet_generatort
Functor generating fresh nondet symbols.
Definition: path_storage.h:23
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
typet::subtype
const typet & subtype() const
Definition: type.h:47
symex_assign.h
Symbolic Execution of assignments.
goto_symext::instruction_local_symbols
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:273
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
NODISCARD
#define NODISCARD
Definition: nodiscard.h:22
path_storaget::build_symex_nondet
symex_nondet_generatort build_symex_nondet
Counter for nondet objects, which require unique names.
Definition: path_storage.h:91
arith_tools.h
object_descriptor_exprt::build
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...
Definition: std_expr.cpp:141
replace_nondet
static void replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
Definition: symex_clean_expr.cpp:168
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:331
L1
@ L1
Definition: renamed.h:18
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
expr_skeleton.h
Expression skeleton.
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
goto_symext::target
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:264
value_set_dereference.h
Pointer Dereferencing.
goto_symext::path_storage
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:796
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1832
let_exprt::symbol
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition: std_expr.h:4204
nodiscard.h
exprt
Base class for all expressions.
Definition: expr.h:53
goto_symext::lift_let
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...
Definition: symex_clean_expr.cpp:181
symex_assignt
Functor for symex assignment.
Definition: symex_assign.h:26
symex_dereference_state.h
Symbolic Execution of ANSI-C.
div_exprt
Division.
Definition: std_expr.h:1031
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
let_exprt::value
exprt & value()
convenience accessor for the value of a single binding
Definition: std_expr.h:4220
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
byte_operators.h
Expression classes for byte-level operators.
goto_symext::process_array_expr
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
Definition: symex_clean_expr.cpp:132
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
goto_symext::dereference
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
Definition: symex_dereference.cpp:398
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
goto_symex_statet::symbol_table
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
Definition: goto_symex_state.h:69
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
goto_symex.h
Symbolic Execution.
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4289
adjust_byte_extract_rec
static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
Rewrite index/member expressions in byte_extract to offset.
Definition: symex_clean_expr.cpp:146
symex_dereference_statet
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
Definition: symex_dereference_state.h:26
symex_configt::simplify_opt
bool simplify_opt
Definition: symex_config.h:31
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
irept::swap
void swap(irept &irep)
Definition: irep.h:463
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:218
goto_symext::do_simplify
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:32
minus_exprt
Binary minus.
Definition: std_expr.h:940
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
simplify_expr.h
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
value_set_dereferencet
Wrapper for a function dereferencing pointer expressions using a value set.
Definition: value_set_dereference.h:27
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:256
array_typet
Arrays with given size.
Definition: std_types.h:965
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
goto_symext::language_mode
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:239
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
goto_symext::lift_lets
void lift_lets(statet &, exprt &)
Execute any let expressions in expr using symex_assignt::assign_symbol.
Definition: symex_clean_expr.cpp:200
goto_symext::symex_config
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:183
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
goto_symex_statet::rename
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...
symex_targett::assignment_typet::HIDDEN
@ HIDDEN
index_exprt
Array index operator.
Definition: std_expr.h:1293
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:333
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:4258
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
c_types.h
let_exprt
A let expression.
Definition: std_expr.h:4165
expr_skeletont
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
process_array_expr
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.
Definition: symex_clean_expr.cpp:33
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:1870