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/std_expr.h>
16 #include <util/cprover_prefix.h>
17 #include <util/base_type.h>
18 
19 #include <util/c_types.h>
20 
22  exprt &expr,
23  const typet &type) const
24 {
25  if(expr.id()==ID_if)
26  {
27  if_exprt &if_expr=to_if_expr(expr);
28  process_array_expr_rec(if_expr.true_case(), type);
29  process_array_expr_rec(if_expr.false_case(), type);
30  }
31  else if(expr.id()==ID_index)
32  {
33  // strip index
34  index_exprt &index_expr=to_index_expr(expr);
35  exprt tmp=index_expr.array();
36  expr.swap(tmp);
37  }
38  else if(expr.id()==ID_typecast)
39  {
40  // strip
41  exprt tmp=to_typecast_expr(expr).op0();
42  expr.swap(tmp);
43  process_array_expr_rec(expr, type);
44  }
45  else if(expr.id()==ID_address_of)
46  {
47  // strip
48  exprt tmp=to_address_of_expr(expr).op0();
49  expr.swap(tmp);
50  process_array_expr_rec(expr, type);
51  }
52  else if(expr.id()==ID_byte_extract_little_endian ||
53  expr.id()==ID_byte_extract_big_endian)
54  {
55  // pick the root object
56  exprt tmp=to_byte_extract_expr(expr).op();
57  expr.swap(tmp);
58  process_array_expr_rec(expr, type);
59  }
60  else if(expr.id()==ID_symbol &&
61  expr.get_bool(ID_C_SSA_symbol) &&
62  to_ssa_expr(expr).get_original_expr().id()==ID_index)
63  {
64  const ssa_exprt &ssa=to_ssa_expr(expr);
65  const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
66  exprt tmp=index_expr.array();
67  expr.swap(tmp);
68  }
69  else
70  Forall_operands(it, expr)
71  {
72  typet t=it->type();
73  process_array_expr_rec(*it, t);
74  }
75 
76  if(!base_type_eq(expr.type(), type, ns))
77  {
79  be.type()=type;
80  be.op()=expr;
81  be.offset()=from_integer(0, index_type());
82 
83  expr.swap(be);
84  }
85 }
86 
88 {
89  // This may change the type of the expression!
90 
91  if(expr.id()==ID_if)
92  {
93  if_exprt &if_expr=to_if_expr(expr);
94  process_array_expr(if_expr.true_case());
95 
97  if_expr.true_case().type());
98 
99  if_expr.type()=if_expr.true_case().type();
100  }
101  else if(expr.id()==ID_index)
102  {
103  // strip index
104  index_exprt &index_expr=to_index_expr(expr);
105  exprt tmp=index_expr.array();
106  expr.swap(tmp);
107  }
108  else if(expr.id()==ID_typecast)
109  {
110  // strip
111  exprt tmp=to_typecast_expr(expr).op0();
112  expr.swap(tmp);
113  process_array_expr(expr);
114  }
115  else if(expr.id()==ID_address_of)
116  {
117  // strip
118  exprt tmp=to_address_of_expr(expr).op0();
119  expr.swap(tmp);
120  process_array_expr(expr);
121  }
122  else if(expr.id()==ID_byte_extract_little_endian ||
123  expr.id()==ID_byte_extract_big_endian)
124  {
125  // pick the root object
126  exprt tmp=to_byte_extract_expr(expr).op();
127  expr.swap(tmp);
128  process_array_expr(expr);
129  }
130  else if(expr.id()==ID_symbol &&
131  expr.get_bool(ID_C_SSA_symbol) &&
132  to_ssa_expr(expr).get_original_expr().id()==ID_index)
133  {
134  const ssa_exprt &ssa=to_ssa_expr(expr);
135  const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
136  exprt tmp=index_expr.array();
137  expr.swap(tmp);
138  }
139  else
140  Forall_operands(it, expr)
141  process_array_expr(*it);
142 }
143 
145 {
146  if(expr.id()==ID_array_equal)
147  {
148  assert(expr.operands().size()==2);
149 
150  // we expect two index expressions
151  process_array_expr(expr.op0());
152  process_array_expr(expr.op1());
153 
154  // type checking
155  if(ns.follow(expr.op0().type())!=
156  ns.follow(expr.op1().type()))
157  expr=false_exprt();
158  else
159  {
160  equal_exprt equality_expr(expr.op0(), expr.op1());
161  expr.swap(equality_expr);
162  }
163  }
164 
165  Forall_operands(it, expr)
166  replace_array_equal(*it);
167 }
168 
170  exprt &expr,
171  statet &state,
172  const bool write)
173 {
174  replace_nondet(expr);
175  dereference(expr, state, write);
176  replace_array_equal(expr);
177 }
The type of an expression.
Definition: type.h:20
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
exprt & true_case()
Definition: std_expr.h:2805
exprt & op0()
Definition: expr.h:84
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
virtual void dereference(exprt &expr, statet &state, const bool write)
void process_array_expr_rec(exprt &expr, const typet &type) const
void replace_array_equal(exprt &expr)
The trinary if-then-else operator.
Definition: std_expr.h:2771
typet & type()
Definition: expr.h:60
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
void replace_nondet(exprt &expr)
Definition: goto_symex.cpp:25
equality
Definition: std_expr.h:1082
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const irep_idt & id() const
Definition: irep.h:189
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
Symbolic Execution.
API to expression classes.
exprt & op1()
Definition: expr.h:87
irep_idt byte_extract_id()
bitvector_typet index_type()
Definition: c_types.cpp:15
void clean_expr(exprt &expr, statet &state, bool write)
exprt & false_case()
Definition: std_expr.h:2815
The boolean constant false.
Definition: std_expr.h:3753
Base class for all expressions.
Definition: expr.h:46
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
void process_array_expr(exprt &expr)
Base Type Computation.
operandst & operands()
Definition: expr.h:70
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)
const namespacet & ns
Definition: goto_symex.h:104
exprt & array()
Definition: std_expr.h:1198
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
array index operator
Definition: std_expr.h:1170