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 }
pointer_offset_size.h
symex_nondet_generatort
Functor generating fresh nondet symbols.
Definition: goto_symex.h:42
typet::subtype
const typet & subtype() const
Definition: type.h:38
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
arith_tools.h
nondet_symbol_exprt
Expression to hold a nondeterministic choice.
Definition: std_expr.h:277
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:123
replace_nondet
static void replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
Definition: symex_clean_expr.cpp:139
address_of_exprt::object
exprt & object()
Definition: std_expr.h:3265
goto_symext::process_array_expr
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
Definition: symex_clean_expr.cpp:24
typet
The type of an expression, extends irept.
Definition: type.h:27
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:53
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
goto_symex_statet
Definition: goto_symex_state.h:34
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
goto_symext::clean_expr
void clean_expr(exprt &, statet &, bool write)
Definition: symex_clean_expr.cpp:154
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symext::do_simplify
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
div_exprt
Division.
Definition: std_expr.h:1211
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:41
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
goto_symext::build_symex_nondet
symex_nondet_generatort build_symex_nondet
Definition: goto_symex.h:422
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:1010
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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:68
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
byte_operators.h
Expression classes for byte-level operators.
base_type.h
size_of_expr
exprt size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:292
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
goto_symext::dereference
virtual void dereference(exprt &, statet &, bool write)
Definition: symex_dereference.cpp:378
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:3282
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:46
base_type_eq
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
goto_symex.h
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:117
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
irept::swap
void swap(irept &irep)
Definition: irep.h:303
irept::id
const irep_idt & id() const
Definition: irep.h:259
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:199
minus_exprt
Binary minus.
Definition: std_expr.h:1106
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:47
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
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:215
array_typet
Arrays with given size.
Definition: std_types.h:1000
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
index_exprt
Array index operator.
Definition: std_expr.h:1595
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
c_types.h
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:2159