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_printf)
98  {
99  codet clean_code=code;
100  clean_expr(clean_code, state, false);
101  symex_printf(state, clean_code);
102  }
103  else if(statement==ID_input)
104  {
105  codet clean_code(code);
106  clean_expr(clean_code, state, false);
107  symex_input(state, clean_code);
108  }
109  else if(statement==ID_output)
110  {
111  codet clean_code(code);
112  clean_expr(clean_code, state, false);
113  symex_output(state, clean_code);
114  }
115  else if(statement==ID_decl)
116  {
117  UNREACHABLE; // see symex_decl.cpp
118  }
119  else if(statement==ID_nondet)
120  {
121  // like skip
122  }
123  else if(statement==ID_asm)
124  {
125  // we ignore this for now
126  }
127  else if(statement==ID_array_copy ||
128  statement==ID_array_replace)
129  {
130  // array_copy and array_replace take two pointers (to arrays); we need to:
131  // 1. dereference the pointers (via clean_expr)
132  // 2. find the actual array objects/candidates for objects (via
133  // process_array_expr)
134  // 3. build an assignment where the type on lhs and rhs is:
135  // - array_copy: the type of the first array (even if the second is smaller)
136  // - array_replace: the type of the second array (even if it is smaller)
138  code.operands().size() == 2,
139  "expected array_copy/array_replace statement to have two operands");
140 
141  // we need to add dereferencing for both operands
142  dereference_exprt dest_array(code.op0());
143  clean_expr(dest_array, state, true);
144  dereference_exprt src_array(code.op1());
145  clean_expr(src_array, state, false);
146 
147  // obtain the actual arrays
148  process_array_expr(dest_array);
149  process_array_expr(src_array);
150 
151  // check for size (or type) mismatch and adjust
152  if(!base_type_eq(dest_array.type(), src_array.type(), ns))
153  {
155 
156  if(statement==ID_array_copy)
157  {
158  be.op()=src_array;
159  be.offset()=from_integer(0, index_type());
160  be.type()=dest_array.type();
161  src_array.swap(be);
162  do_simplify(src_array);
163  }
164  else
165  {
166  // ID_array_replace
167  be.op()=dest_array;
168  be.offset()=from_integer(0, index_type());
169  be.type()=src_array.type();
170  dest_array.swap(be);
171  do_simplify(dest_array);
172  }
173  }
174 
175  code_assignt assignment(dest_array, src_array);
176  symex_assign(state, assignment);
177  }
178  else if(statement==ID_array_set)
179  {
180  // array_set takes a pointer (to an array) and a value that each element
181  // should be set to; we need to:
182  // 1. dereference the pointer (via clean_expr)
183  // 2. find the actual array object/candidates for objects (via
184  // process_array_expr)
185  // 3. use the type of the resulting array to construct an array_of
186  // expression
188  code.operands().size() == 2,
189  "expected array_set statement to have two operands");
190 
191  // we need to add dereferencing for the first operand
192  exprt array_expr = dereference_exprt(code.op0());
193  clean_expr(array_expr, state, true);
194 
195  // obtain the actual array(s)
196  process_array_expr(array_expr);
197 
198  // prepare to build the array_of
199  exprt value = code.op1();
200  clean_expr(value, state, false);
201 
202  // we might have a memset-style update of a non-array type - convert to a
203  // byte array
204  if(array_expr.type().id() != ID_array)
205  {
206  exprt array_size = size_of_expr(array_expr.type(), ns);
207  do_simplify(array_size);
208  array_expr =
210  byte_extract_id(),
211  array_expr,
212  from_integer(0, index_type()),
213  array_typet(char_type(), array_size));
214  }
215 
216  const array_typet &array_type = to_array_type(array_expr.type());
217 
218  if(!base_type_eq(array_type.subtype(), value.type(), ns))
219  value.make_typecast(array_type.subtype());
220 
221  code_assignt assignment(array_expr, array_of_exprt(value, array_type));
222  symex_assign(state, assignment);
223  }
224  else if(statement==ID_array_equal)
225  {
226  // array_equal takes two pointers (to arrays) and the symbol that the result
227  // should get assigned to; we need to:
228  // 1. dereference the pointers (via clean_expr)
229  // 2. find the actual array objects/candidates for objects (via
230  // process_array_expr)
231  // 3. build an assignment where the lhs is the previous third argument, and
232  // the right-hand side is an equality over the arrays, if their types match;
233  // if the types don't match the result trivially is false
235  code.operands().size() == 3,
236  "expected array_equal statement to have three operands");
237 
238  // we need to add dereferencing for the first two
239  dereference_exprt array1(code.op0());
240  clean_expr(array1, state, false);
241  dereference_exprt array2(code.op1());
242  clean_expr(array2, state, false);
243 
244  // obtain the actual arrays
245  process_array_expr(array1);
246  process_array_expr(array2);
247 
248  code_assignt assignment(code.op2(), equal_exprt(array1, array2));
249 
250  // check for size (or type) mismatch
251  if(!base_type_eq(array1.type(), array2.type(), ns))
252  assignment.lhs() = false_exprt();
253 
254  symex_assign(state, assignment);
255  }
256  else if(statement==ID_user_specified_predicate ||
257  statement==ID_user_specified_parameter_predicates ||
258  statement==ID_user_specified_return_predicates)
259  {
260  // like skip
261  }
262  else if(statement==ID_fence)
263  {
264  target.memory_barrier(state.guard.as_expr(), state.source);
265  }
266  else if(statement==ID_havoc_object)
267  {
269  code.operands().size() == 1,
270  "expected havoc_object statement to 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  UNREACHABLE;
280 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
const irep_idt & get_statement() const
Definition: std_code.h:56
exprt as_expr() const
Definition: guard.h:41
exprt size_of_expr(const typet &type, const namespacet &ns)
Boolean negation.
Definition: std_expr.h:3308
exprt & true_case()
Definition: std_expr.h:3455
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
goto_programt::const_targett pc
Definition: symex_target.h:41
exprt & op0()
Definition: expr.h:84
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
exprt & cond()
Definition: std_expr.h:3445
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
Definition: guard.h:19
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
Equality.
Definition: std_expr.h:1484
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
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
exprt & lhs()
Definition: std_code.h:269
Expression classes for byte-level operators.
virtual void symex_other(statet &)
Definition: symex_other.cpp:77
exprt & rhs()
Definition: std_code.h:274
The empty type.
Definition: std_types.h:48
Operator to dereference a pointer.
Definition: std_expr.h:3355
Symbolic Execution.
symex_target_equationt & target
Definition: goto_symex.h:216
exprt & op1()
Definition: expr.h:87
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
Array constructor from single element.
Definition: std_expr.h:1678
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:35
exprt & false_case()
Definition: std_expr.h:3465
The Boolean constant false.
Definition: std_expr.h:4452
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 typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
virtual void symex_output(statet &, const codet &)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
void swap(irept &irep)
Definition: irep.h:303
Arrays with given size.
Definition: std_types.h:1000
virtual void symex_printf(statet &, const exprt &rhs)
exprt & op2()
Definition: expr.h:90
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
Base Type Computation.
const typet & subtype() const
Definition: type.h:38
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
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)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
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
A codet representing an assignment in the program.
Definition: std_code.h:256
void add(const exprt &expr)
Definition: guard.cpp:43
void havoc_rec(statet &, const guardt &, const exprt &)
Definition: symex_other.cpp:20
irep_idt byte_extract_id()
symex_targett::sourcet source