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(
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 = byte_extract_exprt(
96  expr,
98  array_typet(char_type(), array_size.value()));
99  }
100 
101  // given an array type T[N], i.e., an array of N elements of type T, and a
102  // byte offset B, compute the array offset B/sizeof(T) and build a new
103  // type T[N-(B/sizeof(T))]
104  const array_typet &prev_array_type = to_array_type(expr.type());
105  const typet &array_size_type = prev_array_type.size().type();
106  const typet &subtype = prev_array_type.subtype();
107 
108  exprt new_offset =
109  typecast_exprt::conditional_cast(ode.offset(), array_size_type);
110  auto subtype_size_opt = size_of_expr(subtype, ns);
111  CHECK_RETURN(subtype_size_opt.has_value());
113  subtype_size_opt.value(), array_size_type);
114  new_offset = div_exprt(new_offset, subtype_size);
115  minus_exprt subtraction{prev_array_type.size(), new_offset};
116  if_exprt new_size{
118  subtraction, ID_ge, from_integer(0, subtraction.type())},
119  subtraction,
120  from_integer(0, subtraction.type())};
121  if(do_simplify)
122  simplify(new_size, ns);
123 
124  array_typet new_array_type(subtype, new_size);
125 
126  expr =
128  byte_extract_id(),
129  expr,
130  ode.offset(),
131  new_array_type);
132  }
133  }
134 }
135 
137 {
138  symex_dereference_statet symex_dereference_state(state, ns);
139 
141  ns, state.symbol_table, symex_dereference_state, language_mode, false, log);
142 
143  expr = dereference.dereference(expr, symex_config.show_points_to_sets);
144  lift_lets(state, expr);
145 
147 }
148 
150 static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
151 {
152  Forall_operands(it, expr)
153  adjust_byte_extract_rec(*it, ns);
154 
155  if(expr.id()==ID_byte_extract_big_endian ||
156  expr.id()==ID_byte_extract_little_endian)
157  {
159  if(be.op().id()==ID_symbol &&
160  to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object))
161  return;
162 
164  ode.build(expr, ns);
165 
166  be.op()=ode.root_object();
167  be.offset()=ode.offset();
168  }
169 }
170 
171 static void
172 replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
173 {
174  if(expr.id() == ID_side_effect && expr.get(ID_statement) == ID_nondet)
175  {
176  expr = build_symex_nondet(expr.type(), expr.source_location());
177  }
178  else
179  {
180  Forall_operands(it, expr)
181  replace_nondet(*it, build_symex_nondet);
182  }
183 }
184 
185 void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
186 {
187  exprt let_value = clean_expr(let_expr.value(), state, false);
188  let_value = state.rename(std::move(let_value), ns).get();
189  do_simplify(let_value);
190 
191  exprt::operandst value_assignment_guard;
194  .assign_symbol(
195  to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),
196  expr_skeletont{},
197  let_value,
198  value_assignment_guard);
199 
200  // Schedule the bound variable to be cleaned up at the end of symex_step:
201  instruction_local_symbols.push_back(let_expr.symbol());
202 }
203 
205 {
206  for(auto it = rhs.depth_begin(), itend = rhs.depth_end(); it != itend;)
207  {
208  if(it->id() == ID_let)
209  {
210  // Visit post-order, so more-local definitions are made before usage:
211  exprt &replaced_expr = it.mutate();
212  let_exprt &replaced_let = to_let_expr(replaced_expr);
213  lift_lets(state, replaced_let.value());
214  lift_lets(state, replaced_let.where());
215 
216  lift_let(state, replaced_let);
217  replaced_expr = replaced_let.where();
218 
219  it.next_sibling_or_parent();
220  }
221  else if(it->id() == ID_exists || it->id() == ID_forall)
222  {
223  // expressions within exists/forall may depend on bound variables, we
224  // cannot safely lift let expressions out of those, just skip
225  it.next_sibling_or_parent();
226  }
227  else
228  ++it;
229  }
230 }
231 
233 goto_symext::clean_expr(exprt expr, statet &state, const bool write)
234 {
236  dereference(expr, state, write);
237  lift_lets(state, expr);
238 
239  // make sure all remaining byte extract operations use the root
240  // object to avoid nesting of with/update and byte_update when on
241  // lhs
242  if(write)
244  return expr;
245 }
goto_symext::clean_expr
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
Definition: symex_clean_expr.cpp:233
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:1789
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:25
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: pointer_expr.cpp:108
replace_nondet
static void replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
Definition: symex_clean_expr.cpp:172
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:209
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:279
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:28
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:1297
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
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:797
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:2087
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:21
let_exprt::symbol
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition: std_expr.h:2855
nodiscard.h
exprt
Base class for all expressions.
Definition: expr.h:54
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:185
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:981
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:2124
goto_symext::log
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:276
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:976
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:82
let_exprt::value
exprt & value()
convenience accessor for the value of a single binding
Definition: std_expr.h:2871
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
byte_operators.h
Expression classes for byte-level operators.
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
symex_configt::show_points_to_sets
bool show_points_to_sets
Definition: symex_config.h:49
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:136
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
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:399
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
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:644
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:2940
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:150
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:2524
index_exprt::array
exprt & array()
Definition: std_expr.h:1259
irept::swap
void swap(irept &irep)
Definition: irep.h:452
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: pointer_expr.cpp:125
goto_symext::do_simplify
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:33
minus_exprt
Binary minus.
Definition: std_expr.h:890
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:28
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
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:968
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:2114
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:204
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:1018
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:278
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...
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
symex_targett::assignment_typet::HIDDEN
@ HIDDEN
index_exprt
Array index operator.
Definition: std_expr.h:1243
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:281
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:2909
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
c_types.h
let_exprt
A let expression.
Definition: std_expr.h:2816
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: pointer_expr.h:59