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/base_type.h>
16 #include <util/byte_operators.h>
17 #include <util/c_types.h>
19 
25 {
26  // This may change the type of the expression!
27 
28  if(expr.id()==ID_if)
29  {
30  if_exprt &if_expr=to_if_expr(expr);
31  process_array_expr(if_expr.true_case());
32  process_array_expr(if_expr.false_case());
33 
34  if(!base_type_eq(if_expr.true_case(), if_expr.false_case(), ns))
35  {
38  if_expr.false_case(),
40  if_expr.true_case().type());
41 
42  if_expr.false_case().swap(be);
43  }
44 
45  if_expr.type()=if_expr.true_case().type();
46  }
47  else if(expr.id()==ID_address_of)
48  {
49  // strip
50  exprt tmp = to_address_of_expr(expr).object();
51  expr.swap(tmp);
52  process_array_expr(expr);
53  }
54  else if(expr.id()==ID_symbol &&
55  expr.get_bool(ID_C_SSA_symbol) &&
56  to_ssa_expr(expr).get_original_expr().id()==ID_index)
57  {
58  const ssa_exprt &ssa=to_ssa_expr(expr);
59  const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
60  exprt tmp=index_expr.array();
61  expr.swap(tmp);
62 
63  process_array_expr(expr);
64  }
65  else if(expr.id() != ID_symbol)
66  {
68  ode.build(expr, ns);
69  do_simplify(ode.offset());
70 
71  expr = ode.root_object();
72 
73  if(!ode.offset().is_zero())
74  {
75  if(expr.type().id() != ID_array)
76  {
77  exprt array_size = size_of_expr(expr.type(), ns);
78  do_simplify(array_size);
79  expr =
82  expr,
84  array_typet(char_type(), array_size));
85  }
86 
87  // given an array type T[N], i.e., an array of N elements of type T, and a
88  // byte offset B, compute the array offset B/sizeof(T) and build a new
89  // type T[N-(B/sizeof(T))]
90  const array_typet &prev_array_type = to_array_type(expr.type());
91  const typet &array_size_type = prev_array_type.size().type();
92  const typet &subtype = prev_array_type.subtype();
93 
94  exprt new_offset(ode.offset());
95  if(new_offset.type() != array_size_type)
96  new_offset.make_typecast(array_size_type);
97  exprt subtype_size = size_of_expr(subtype, ns);
98  if(subtype_size.type() != array_size_type)
99  subtype_size.make_typecast(array_size_type);
100  new_offset = div_exprt(new_offset, subtype_size);
101  minus_exprt new_size(prev_array_type.size(), new_offset);
102  do_simplify(new_size);
103 
104  array_typet new_array_type(subtype, new_size);
105 
106  expr =
108  byte_extract_id(),
109  expr,
110  ode.offset(),
111  new_array_type);
112  }
113  }
114 }
115 
117 static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
118 {
119  Forall_operands(it, expr)
120  adjust_byte_extract_rec(*it, ns);
121 
122  if(expr.id()==ID_byte_extract_big_endian ||
123  expr.id()==ID_byte_extract_little_endian)
124  {
126  if(be.op().id()==ID_symbol &&
127  to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object))
128  return;
129 
131  ode.build(expr, ns);
132 
133  be.op()=ode.root_object();
134  be.offset()=ode.offset();
135  }
136 }
137 
138 static void
139 replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
140 {
141  if(expr.id() == ID_side_effect && expr.get(ID_statement) == ID_nondet)
142  {
143  nondet_symbol_exprt new_expr = build_symex_nondet(expr.type());
144  new_expr.add_source_location() = expr.source_location();
145  expr.swap(new_expr);
146  }
147  else
148  {
149  Forall_operands(it, expr)
150  replace_nondet(*it, build_symex_nondet);
151  }
152 }
153 
155  exprt &expr,
156  statet &state,
157  const bool write)
158 {
160  dereference(expr, state, write);
161 
162  // make sure all remaining byte extract operations use the root
163  // object to avoid nesting of with/update and byte_update when on
164  // lhs
165  if(write)
167 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
The type of an expression, extends irept.
Definition: type.h:27
exprt size_of_expr(const typet &type, const namespacet &ns)
exprt & true_case()
Definition: std_expr.h:3455
exprt & object()
Definition: std_expr.h:3265
static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
Rewrite index/member expressions in byte_extract to offset.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
The trinary if-then-else operator.
Definition: std_expr.h:3427
typet & type()
Return the type of the expression.
Definition: expr.h:68
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
symex_nondet_generatort build_symex_nondet
Definition: goto_symex.h:422
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:215
const irep_idt & id() const
Definition: irep.h:259
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
Expression classes for byte-level operators.
Division.
Definition: std_expr.h:1211
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:123
Symbolic Execution.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
static void replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
const exprt & size() const
Definition: std_types.h:1010
virtual void dereference(exprt &, statet &, bool write)
bitvector_typet index_type()
Definition: c_types.cpp:16
exprt & false_case()
Definition: std_expr.h:3465
Pointer Logic.
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
void clean_expr(exprt &, statet &, bool write)
Expression to hold a nondeterministic choice.
Definition: std_expr.h:277
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
const exprt & root_object() const
Definition: std_expr.cpp:199
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
const source_locationt & source_location() const
Definition: expr.h:228
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:26
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
source_locationt & add_source_location()
Definition: expr.h:233
Arrays with given size.
Definition: std_types.h:1000
Binary minus.
Definition: std_expr.h:1106
Base Type Computation.
const typet & subtype() const
Definition: type.h:38
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
exprt & array()
Definition: std_expr.h:1621
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
bitvector_typet char_type()
Definition: c_types.cpp:114
Functor generating fresh nondet symbols.
Definition: goto_symex.h:42
irep_idt byte_extract_id()
Array index operator.
Definition: std_expr.h:1595