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  {
148  byte_extract_id(),
149  src_array,
150  from_integer(0, index_type()),
151  dest_array.type());
152  src_array.swap(be);
153  do_simplify(src_array);
154  }
155  else
156  {
157  // ID_array_replace
159  byte_extract_id(),
160  dest_array,
161  from_integer(0, index_type()),
162  src_array.type());
163  dest_array.swap(be);
164  do_simplify(dest_array);
165  }
166  }
167 
168  symex_assign(state, dest_array, src_array);
169  }
170  else if(statement==ID_array_set)
171  {
172  // array_set takes a pointer (to an array) and a value that each element
173  // should be set to; we need to:
174  // 1. remove any dereference expressions (via clean_expr)
175  // 2. find the actual array object/candidates for objects (via
176  // process_array_expr)
177  // 3. use the type of the resulting array to construct an array_of
178  // expression
180  code.operands().size() == 2,
181  "expected array_set statement to have two operands");
182 
183  // we need to add dereferencing for the first operand
184  exprt array_expr = clean_expr(code.op0(), state, false);
185 
186  // obtain the actual array(s)
187  process_array_expr(state, array_expr);
188 
189  // prepare to build the array_of
190  exprt value = clean_expr(code.op1(), state, false);
191 
192  // we might have a memset-style update of a non-array type - convert to a
193  // byte array
194  if(array_expr.type().id() != ID_array)
195  {
196  auto array_size = size_of_expr(array_expr.type(), ns);
197  CHECK_RETURN(array_size.has_value());
198  do_simplify(array_size.value());
199  array_expr = byte_extract_exprt(
200  byte_extract_id(),
201  array_expr,
202  from_integer(0, index_type()),
203  array_typet(char_type(), array_size.value()));
204  }
205 
206  const array_typet &array_type = to_array_type(array_expr.type());
207 
208  if(array_type.subtype() != value.type())
209  value = typecast_exprt(value, array_type.subtype());
210 
211  symex_assign(state, array_expr, array_of_exprt(value, array_type));
212  }
213  else if(statement==ID_array_equal)
214  {
215  // array_equal takes two pointers (to arrays) and the symbol that the result
216  // should get assigned to; we need to:
217  // 1. remove any dereference expressions (via clean_expr)
218  // 2. find the actual array objects/candidates for objects (via
219  // process_array_expr)
220  // 3. build an assignment where the lhs is the previous third argument, and
221  // the right-hand side is an equality over the arrays, if their types match;
222  // if the types don't match the result trivially is false
224  code.operands().size() == 3,
225  "expected array_equal statement to have three operands");
226 
227  // we need to add dereferencing for the first two
228  exprt array1 = clean_expr(code.op0(), state, false);
229  exprt array2 = clean_expr(code.op1(), state, false);
230 
231  // obtain the actual arrays
232  process_array_expr(state, array1);
233  process_array_expr(state, array2);
234 
235  exprt rhs = equal_exprt(array1, array2);
236 
237  // check for size (or type) mismatch
238  if(array1.type() != array2.type())
239  rhs = false_exprt();
240 
241  symex_assign(state, code.op2(), rhs);
242  }
243  else if(statement==ID_user_specified_predicate ||
244  statement==ID_user_specified_parameter_predicates ||
245  statement==ID_user_specified_return_predicates)
246  {
247  // like skip
248  }
249  else if(statement==ID_fence)
250  {
251  target.memory_barrier(state.guard.as_expr(), state.source);
252  }
253  else if(statement==ID_havoc_object)
254  {
256  code.operands().size() == 1,
257  "expected havoc_object statement to have one operand");
258 
259  exprt object = clean_expr(code.op0(), state, false);
260 
261  process_array_expr(state, object);
262  havoc_rec(state, guardt(true_exprt(), guard_manager), object);
263  }
264  else
265  UNREACHABLE;
266 }
guard_exprt
Definition: guard_expr.h:27
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
goto_symext::clean_expr
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
Definition: symex_clean_expr.cpp:233
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
typet::subtype
const typet & subtype() const
Definition: type.h:47
can_cast_expr< code_inputt >
bool can_cast_expr< code_inputt >(const exprt &base)
Definition: std_code.h:705
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:103
symex_target_equationt::memory_barrier
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
Definition: symex_target_equation.cpp:78
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
goto_symext::symex_printf
virtual void symex_printf(statet &state, const exprt &rhs)
Symbolically execute an OTHER instruction that does a CPP printf
Definition: symex_builtin_functions.cpp:368
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
goto_symext::target
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:264
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2087
goto_symext::guard_manager
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:261
exprt
Base class for all expressions.
Definition: expr.h:54
guard_exprt::is_true
bool is_true() const
Definition: guard_expr.h:63
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
guardt
guard_exprt guardt
Definition: guard.h:27
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1140
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2124
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:320
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
byte_operators.h
Expression classes for byte-level operators.
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
goto_symext::process_array_expr
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
Definition: symex_clean_expr.cpp:136
goto_symext::symex_cpp_delete
virtual void symex_cpp_delete(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP delete
Definition: symex_builtin_functions.cpp:534
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
guard_exprt::add
void add(const exprt &expr)
Definition: guard_expr.cpp:40
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1317
goto_symex.h
Symbolic Execution.
goto_statet::guard
guardt guard
Definition: goto_state.h:54
goto_symext::symex_input
virtual void symex_input(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP input.
Definition: symex_builtin_functions.cpp:423
irept::swap
void swap(irept &irep)
Definition: irep.h:452
codet::op2
exprt & op2()
Definition: expr.h:109
irept::id
const irep_idt & id() const
Definition: irep.h:407
false_exprt
The Boolean constant false.
Definition: std_expr.h:2726
goto_symext::do_simplify
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:33
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
goto_symext::havoc_rec
void havoc_rec(statet &state, const guardt &guard, const exprt &dest)
Definition: symex_other.cpp:19
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:256
can_cast_expr< code_outputt >
bool can_cast_expr< code_outputt >(const exprt &base)
Definition: std_code.h:751
array_typet
Arrays with given size.
Definition: std_types.h:968
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2114
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2104
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:278
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
exprt::operands
operandst & operands()
Definition: expr.h:96
codet::op1
exprt & op1()
Definition: expr.h:106
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
goto_symext::symex_assign
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
c_types.h
goto_symext::symex_other
virtual void symex_other(statet &state)
Symbolically execute an OTHER instruction.
Definition: symex_other.cpp:74
goto_symext::symex_output
virtual void symex_output(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP output.
Definition: symex_builtin_functions.cpp:445
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
not_exprt
Boolean negation.
Definition: std_expr.h:2042