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/byte_operators.h>
16 #include <util/c_types.h>
18 
20  statet &state,
21  const guardt &guard,
22  const exprt &dest)
23 {
24  if(dest.id()==ID_symbol)
25  {
26  exprt lhs;
27 
28  if(guard.is_true())
29  lhs=dest;
30  else
31  lhs=if_exprt(
32  guard.as_expr(), dest, exprt(ID_null_object, dest.type()));
33 
34  auto rhs =
35  side_effect_expr_nondett(dest.type(), state.source.pc->source_location);
36 
37  symex_assign(state, lhs, rhs);
38  }
39  else if(dest.id()==ID_byte_extract_little_endian ||
40  dest.id()==ID_byte_extract_big_endian)
41  {
42  havoc_rec(state, guard, to_byte_extract_expr(dest).op());
43  }
44  else if(dest.id()==ID_if)
45  {
46  const if_exprt &if_expr=to_if_expr(dest);
47 
48  guardt guard_t=state.guard;
49  guard_t.add(if_expr.cond());
50  havoc_rec(state, guard_t, if_expr.true_case());
51 
52  guardt guard_f=state.guard;
53  guard_f.add(not_exprt(if_expr.cond()));
54  havoc_rec(state, guard_f, if_expr.false_case());
55  }
56  else if(dest.id()==ID_typecast)
57  {
58  havoc_rec(state, guard, to_typecast_expr(dest).op());
59  }
60  else if(dest.id()==ID_index)
61  {
62  havoc_rec(state, guard, to_index_expr(dest).array());
63  }
64  else if(dest.id()==ID_member)
65  {
66  havoc_rec(state, guard, to_member_expr(dest).struct_op());
67  }
68  else
69  {
70  // consider printing a warning
71  }
72 }
73 
75  statet &state)
76 {
77  const goto_programt::instructiont &instruction=*state.source.pc;
78 
79  const codet &code = instruction.get_other();
80 
81  const irep_idt &statement=code.get_statement();
82 
83  if(statement==ID_expression)
84  {
85  // ignore
86  }
87  else if(statement==ID_cpp_delete ||
88  statement=="cpp_delete[]")
89  {
90  const codet clean_code = to_code(clean_expr(code, state, false));
91  symex_cpp_delete(state, clean_code);
92  }
93  else if(statement==ID_printf)
94  {
95  const codet clean_code = to_code(clean_expr(code, state, false));
96  symex_printf(state, clean_code);
97  }
98  else if(can_cast_expr<code_inputt>(code))
99  {
100  const codet clean_code = to_code(clean_expr(code, state, false));
101  symex_input(state, clean_code);
102  }
103  else if(can_cast_expr<code_outputt>(code))
104  {
105  const codet clean_code = to_code(clean_expr(code, state, false));
106  symex_output(state, clean_code);
107  }
108  else if(statement==ID_decl)
109  {
110  UNREACHABLE; // see symex_decl.cpp
111  }
112  else if(statement==ID_nondet)
113  {
114  // like skip
115  }
116  else if(statement==ID_asm)
117  {
118  // we ignore this for now
119  }
120  else if(statement==ID_array_copy ||
121  statement==ID_array_replace)
122  {
123  // array_copy and array_replace take two pointers (to arrays); we need to:
124  // 1. remove any dereference expressions (via clean_expr)
125  // 2. find the actual array objects/candidates for objects (via
126  // process_array_expr)
127  // 3. build an assignment where the type on lhs and rhs is:
128  // - array_copy: the type of the first array (even if the second is smaller)
129  // - array_replace: the type of the second array (even if it is smaller)
131  code.operands().size() == 2,
132  "expected array_copy/array_replace statement to have two operands");
133 
134  // we need to add dereferencing for both operands
135  exprt dest_array = clean_expr(code.op0(), state, false);
136  exprt src_array = clean_expr(code.op1(), state, false);
137 
138  // obtain the actual arrays
139  process_array_expr(state, dest_array);
140  process_array_expr(state, src_array);
141 
142  // check for size (or type) mismatch and adjust
143  if(dest_array.type() != src_array.type())
144  {
145  if(statement==ID_array_copy)
146  {
147  src_array = make_byte_extract(
148  src_array, from_integer(0, index_type()), dest_array.type());
149  do_simplify(src_array);
150  }
151  else
152  {
153  // ID_array_replace
154  dest_array = make_byte_extract(
155  dest_array, from_integer(0, index_type()), src_array.type());
156  do_simplify(dest_array);
157  }
158  }
159 
160  symex_assign(state, dest_array, src_array);
161  }
162  else if(statement==ID_array_set)
163  {
164  // array_set takes a pointer (to an array) and a value that each element
165  // should be set to; we need to:
166  // 1. remove any dereference expressions (via clean_expr)
167  // 2. find the actual array object/candidates for objects (via
168  // process_array_expr)
169  // 3. use the type of the resulting array to construct an array_of
170  // expression
172  code.operands().size() == 2,
173  "expected array_set statement to have two operands");
174 
175  // we need to add dereferencing for the first operand
176  exprt array_expr = clean_expr(code.op0(), state, false);
177 
178  // obtain the actual array(s)
179  process_array_expr(state, array_expr);
180 
181  // prepare to build the array_of
182  exprt value = clean_expr(code.op1(), state, false);
183 
184  // we might have a memset-style update of a non-array type - convert to a
185  // byte array
186  if(array_expr.type().id() != ID_array)
187  {
188  auto array_size = size_of_expr(array_expr.type(), ns);
189  CHECK_RETURN(array_size.has_value());
190  do_simplify(array_size.value());
191  array_expr = make_byte_extract(
192  array_expr,
193  from_integer(0, index_type()),
194  array_typet(char_type(), array_size.value()));
195  }
196 
197  const array_typet &array_type = to_array_type(array_expr.type());
198 
199  if(array_type.subtype() != value.type())
200  value = typecast_exprt(value, array_type.subtype());
201 
202  symex_assign(state, array_expr, array_of_exprt(value, array_type));
203  }
204  else if(statement==ID_array_equal)
205  {
206  // array_equal takes two pointers (to arrays) and the symbol that the result
207  // should get assigned to; we need to:
208  // 1. remove any dereference expressions (via clean_expr)
209  // 2. find the actual array objects/candidates for objects (via
210  // process_array_expr)
211  // 3. build an assignment where the lhs is the previous third argument, and
212  // the right-hand side is an equality over the arrays, if their types match;
213  // if the types don't match the result trivially is false
215  code.operands().size() == 3,
216  "expected array_equal statement to have three operands");
217 
218  // we need to add dereferencing for the first two
219  exprt array1 = clean_expr(code.op0(), state, false);
220  exprt array2 = clean_expr(code.op1(), state, false);
221 
222  // obtain the actual arrays
223  process_array_expr(state, array1);
224  process_array_expr(state, array2);
225 
226  exprt rhs = equal_exprt(array1, array2);
227 
228  // check for size (or type) mismatch
229  if(array1.type() != array2.type())
230  rhs = false_exprt();
231 
232  symex_assign(state, code.op2(), rhs);
233  }
234  else if(statement==ID_user_specified_predicate ||
235  statement==ID_user_specified_parameter_predicates ||
236  statement==ID_user_specified_return_predicates)
237  {
238  // like skip
239  }
240  else if(statement==ID_fence)
241  {
242  target.memory_barrier(state.guard.as_expr(), state.source);
243  }
244  else if(statement==ID_havoc_object)
245  {
247  code.operands().size() == 1,
248  "expected havoc_object statement to have one operand");
249 
250  exprt object = clean_expr(code.op0(), state, false);
251 
252  process_array_expr(state, object);
253  havoc_rec(state, guardt(true_exprt(), guard_manager), object);
254  }
255  else
256  UNREACHABLE;
257 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet index_type()
Definition: c_types.cpp:16
bitvector_typet char_type()
Definition: c_types.cpp:114
Array constructor from single element.
Definition: std_expr.h:1402
Arrays with given size.
Definition: std_types.h:763
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code.h:69
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2811
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:417
guardt guard
Definition: goto_state.h:58
Central data structure: state.
symex_targett::sourcet source
virtual void symex_input(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP input.
void havoc_rec(statet &state, const guardt &guard, const exprt &dest)
Definition: symex_other.cpp:19
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:251
virtual void symex_cpp_delete(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP delete
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:248
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:243
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Definition: goto_symex.cpp:39
virtual void symex_printf(statet &state, const exprt &rhs)
Symbolically execute an OTHER instruction that does a CPP printf
virtual void symex_output(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP output.
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:33
virtual void symex_other(statet &state)
Symbolically execute an OTHER instruction.
Definition: symex_other.cpp:74
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
void add(const exprt &expr)
Definition: guard_expr.cpp:39
bool is_true() const
Definition: guard_expr.h:60
exprt as_expr() const
Definition: guard_expr.h:46
The trinary if-then-else operator.
Definition: std_expr.h:2172
exprt & true_case()
Definition: std_expr.h:2199
exprt & false_case()
Definition: std_expr.h:2209
exprt & cond()
Definition: std_expr.h:2189
const irep_idt & id() const
Definition: irep.h:407
Boolean negation.
Definition: std_expr.h:2127
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
The Boolean constant true.
Definition: std_expr.h:2802
Semantic type conversion.
Definition: std_expr.h:1866
const typet & subtype() const
Definition: type.h:47
Symbolic Execution.
guard_exprt guardt
Definition: guard.h:27
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
bool can_cast_expr< code_inputt >(const exprt &base)
Definition: std_code.h:703
bool can_cast_expr< code_outputt >(const exprt &base)
Definition: std_code.h:749
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
goto_programt::const_targett pc
Definition: symex_target.h:42
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.