cprover
symex_other.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
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 
21  statet &state,
22  const guardt &guard,
23  const exprt &dest)
24 {
25  if(dest.id()==ID_symbol)
26  {
27  exprt lhs;
28 
29  if(guard.is_true())
30  lhs=dest;
31  else
32  lhs=if_exprt(
33  guard.as_expr(), dest, exprt(ID_null_object, dest.type()));
34 
35  code_assignt assignment;
36  assignment.lhs()=lhs;
37  assignment.rhs()=side_effect_expr_nondett(dest.type());
38 
39  symex_assign(state, assignment);
40  }
41  else if(dest.id()==ID_byte_extract_little_endian ||
42  dest.id()==ID_byte_extract_big_endian)
43  {
44  havoc_rec(state, guard, to_byte_extract_expr(dest).op());
45  }
46  else if(dest.id()==ID_if)
47  {
48  const if_exprt &if_expr=to_if_expr(dest);
49 
50  guardt guard_t=state.guard;
51  guard_t.add(if_expr.cond());
52  havoc_rec(state, guard_t, if_expr.true_case());
53 
54  guardt guard_f=state.guard;
55  guard_f.add(not_exprt(if_expr.cond()));
56  havoc_rec(state, guard_f, if_expr.false_case());
57  }
58  else if(dest.id()==ID_typecast)
59  {
60  havoc_rec(state, guard, to_typecast_expr(dest).op());
61  }
62  else if(dest.id()==ID_index)
63  {
64  havoc_rec(state, guard, to_index_expr(dest).array());
65  }
66  else if(dest.id()==ID_member)
67  {
68  havoc_rec(state, guard, to_member_expr(dest).struct_op());
69  }
70  else
71  {
72  // consider printing a warning
73  }
74 }
75 
77  statet &state)
78 {
79  const goto_programt::instructiont &instruction=*state.source.pc;
80 
81  const codet &code=to_code(instruction.code);
82 
83  const irep_idt &statement=code.get_statement();
84 
85  if(statement==ID_expression)
86  {
87  // ignore
88  }
89  else if(statement==ID_cpp_delete ||
90  statement=="cpp_delete[]")
91  {
92  codet clean_code=code;
93  clean_expr(clean_code, state, false);
94  symex_cpp_delete(state, clean_code);
95  }
96  else if(statement==ID_free)
97  {
98  // ignore
99  }
100  else if(statement==ID_printf)
101  {
102  codet clean_code=code;
103  clean_expr(clean_code, state, false);
104  symex_printf(state, nil_exprt(), clean_code);
105  }
106  else if(statement==ID_input)
107  {
108  codet clean_code(code);
109  clean_expr(clean_code, state, false);
110  symex_input(state, clean_code);
111  }
112  else if(statement==ID_output)
113  {
114  codet clean_code(code);
115  clean_expr(clean_code, state, false);
116  symex_output(state, clean_code);
117  }
118  else if(statement==ID_decl)
119  {
120  UNREACHABLE; // see symex_decl.cpp
121  }
122  else if(statement==ID_nondet)
123  {
124  // like skip
125  }
126  else if(statement==ID_asm)
127  {
128  // we ignore this for now
129  }
130  else if(statement==ID_array_copy ||
131  statement==ID_array_replace)
132  {
133  // array_copy and array_replace take two pointers (to arrays); we need to:
134  // 1. dereference the pointers (via clean_expr)
135  // 2. find the actual array objects/candidates for objects (via
136  // process_array_expr)
137  // 3. build an assignment where the type on lhs and rhs is:
138  // - array_copy: the type of the first array (even if the second is smaller)
139  // - array_replace: the type of the second array (even if it is smaller)
141  code.operands().size() == 2,
142  "array_copy/array_replace takes two operands");
143 
144  // we need to add dereferencing for both operands
145  dereference_exprt dest_array(code.op0());
146  clean_expr(dest_array, state, true);
147  dereference_exprt src_array(code.op1());
148  clean_expr(src_array, state, false);
149 
150  // obtain the actual arrays
151  process_array_expr(dest_array);
152  process_array_expr(src_array);
153 
154  // check for size (or type) mismatch and adjust
155  if(!base_type_eq(dest_array.type(), src_array.type(), ns))
156  {
158 
159  if(statement==ID_array_copy)
160  {
161  be.op()=src_array;
162  be.offset()=from_integer(0, index_type());
163  be.type()=dest_array.type();
164  src_array.swap(be);
165  do_simplify(src_array);
166  }
167  else
168  {
169  // ID_array_replace
170  be.op()=dest_array;
171  be.offset()=from_integer(0, index_type());
172  be.type()=src_array.type();
173  dest_array.swap(be);
174  do_simplify(dest_array);
175  }
176  }
177 
178  code_assignt assignment(dest_array, src_array);
179  symex_assign(state, assignment);
180  }
181  else if(statement==ID_array_set)
182  {
183  // array_set takes a pointer (to an array) and a value that each element
184  // should be set to; we need to:
185  // 1. dereference the pointer (via clean_expr)
186  // 2. find the actual array object/candidates for objects (via
187  // process_array_expr)
188  // 3. use the type of the resulting array to construct an array_of
189  // expression
190  DATA_INVARIANT(code.operands().size() == 2, "array_set takes two operands");
191 
192  // we need to add dereferencing for the first operand
193  exprt array_expr = dereference_exprt(code.op0());
194  clean_expr(array_expr, state, true);
195 
196  // obtain the actual array(s)
197  process_array_expr(array_expr);
198 
199  // prepare to build the array_of
200  exprt value = code.op1();
201  clean_expr(value, state, false);
202 
203  // we might have a memset-style update of a non-array type - convert to a
204  // byte array
205  if(array_expr.type().id() != ID_array)
206  {
207  exprt array_size = size_of_expr(array_expr.type(), ns);
208  do_simplify(array_size);
209  array_expr =
211  byte_extract_id(),
212  array_expr,
213  from_integer(0, index_type()),
214  array_typet(char_type(), array_size));
215  }
216 
217  const array_typet &array_type = to_array_type(array_expr.type());
218 
219  if(!base_type_eq(array_type.subtype(), value.type(), ns))
220  value.make_typecast(array_type.subtype());
221 
222  code_assignt assignment(array_expr, array_of_exprt(value, array_type));
223  symex_assign(state, assignment);
224  }
225  else if(statement==ID_array_equal)
226  {
227  // array_equal takes two pointers (to arrays) and the symbol that the result
228  // should get assigned to; we need to:
229  // 1. dereference the pointers (via clean_expr)
230  // 2. find the actual array objects/candidates for objects (via
231  // process_array_expr)
232  // 3. build an assignment where the lhs is the previous third argument, and
233  // the right-hand side is an equality over the arrays, if their types match;
234  // if the types don't match the result trivially is false
236  code.operands().size() == 3,
237  "array_equal expected to take three arguments");
238 
239  // we need to add dereferencing for the first two
240  dereference_exprt array1(code.op0());
241  clean_expr(array1, state, false);
242  dereference_exprt array2(code.op1());
243  clean_expr(array2, state, false);
244 
245  // obtain the actual arrays
246  process_array_expr(array1);
247  process_array_expr(array2);
248 
249  code_assignt assignment(code.op2(), equal_exprt(array1, array2));
250 
251  // check for size (or type) mismatch
252  if(!base_type_eq(array1.type(), array2.type(), ns))
253  assignment.lhs() = false_exprt();
254 
255  symex_assign(state, assignment);
256  }
257  else if(statement==ID_user_specified_predicate ||
258  statement==ID_user_specified_parameter_predicates ||
259  statement==ID_user_specified_return_predicates)
260  {
261  // like skip
262  }
263  else if(statement==ID_fence)
264  {
265  target.memory_barrier(state.guard.as_expr(), state.source);
266  }
267  else if(statement==ID_havoc_object)
268  {
269  DATA_INVARIANT(code.operands().size()==1,
270  "havoc_object must have one operand");
271 
272  // we need to add dereferencing for the first operand
273  dereference_exprt object(code.op0(), empty_typet());
274  clean_expr(object, state, true);
275 
276  havoc_rec(state, guardt(), object);
277  }
278  else
279  throw "unexpected statement: "+id2string(statement);
280 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
const irep_idt & get_statement() const
Definition: std_code.h:39
exprt as_expr() const
Definition: guard.h:43
exprt size_of_expr(const typet &type, const namespacet &ns)
Boolean negation.
Definition: std_expr.h:3230
exprt & true_case()
Definition: std_expr.h:3395
virtual void memory_barrier(const exprt &guard, const sourcet &source)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
goto_programt::const_targett pc
Definition: symex_target.h:32
exprt & op0()
Definition: expr.h:72
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
bool is_true() const
Definition: expr.cpp:124
Definition: guard.h:19
typet & type()
Definition: expr.h:56
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:19
equality
Definition: std_expr.h:1354
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:237
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
Expression classes for byte-level operators.
virtual void symex_other(statet &)
Definition: symex_other.cpp:76
The NIL expression.
Definition: std_expr.h:4510
exprt & rhs()
Definition: std_code.h:213
The empty type.
Definition: std_types.h:54
Operator to dereference a pointer.
Definition: std_expr.h:3284
Symbolic Execution.
symex_target_equationt & target
Definition: goto_symex.h:238
exprt & op1()
Definition: expr.h:75
irep_idt byte_extract_id()
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
array constructor from single element
Definition: std_expr.h:1550
bitvector_typet index_type()
Definition: c_types.cpp:16
exprt & false_case()
Definition: std_expr.h:3405
The boolean constant false.
Definition: std_expr.h:4499
Pointer Logic.
virtual void symex_input(statet &, const codet &)
void symex_assign(statet &, const code_assignt &)
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
void clean_expr(exprt &, statet &, bool write)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
virtual void symex_output(statet &, const codet &)
#define UNREACHABLE
Definition: invariant.h:250
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
void swap(irept &irep)
Definition: irep.h:231
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
arrays with given size
Definition: std_types.h:1004
exprt & op2()
Definition: expr.h:78
virtual void symex_printf(statet &, const exprt &lhs, const exprt &rhs)
A statement in a programming language.
Definition: std_code.h:21
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
operandst & operands()
Definition: expr.h:66
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)
virtual void symex_cpp_delete(statet &, const codet &)
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
bitvector_typet char_type()
Definition: c_types.cpp:114
Assignment.
Definition: std_code.h:195
void add(const exprt &expr)
Definition: guard.cpp:64
void havoc_rec(statet &, const guardt &, const exprt &)
Definition: symex_other.cpp:20
symex_targett::sourcet source