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