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  code_assignt assignment;
35  assignment.lhs()=lhs;
36  assignment.rhs() =
37  side_effect_expr_nondett(dest.type(), state.source.pc->source_location);
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 = instruction.get_other();
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  const codet clean_code = to_code(clean_expr(code, state, false));
93  symex_cpp_delete(state, clean_code);
94  }
95  else if(statement==ID_printf)
96  {
97  const codet clean_code = to_code(clean_expr(code, state, false));
98  symex_printf(state, clean_code);
99  }
100  else if(can_cast_expr<code_inputt>(code))
101  {
102  const codet clean_code = to_code(clean_expr(code, state, false));
103  symex_input(state, clean_code);
104  }
105  else if(can_cast_expr<code_outputt>(code))
106  {
107  const codet clean_code = to_code(clean_expr(code, state, false));
108  symex_output(state, clean_code);
109  }
110  else if(statement==ID_decl)
111  {
112  UNREACHABLE; // see symex_decl.cpp
113  }
114  else if(statement==ID_nondet)
115  {
116  // like skip
117  }
118  else if(statement==ID_asm)
119  {
120  // we ignore this for now
121  }
122  else if(statement==ID_array_copy ||
123  statement==ID_array_replace)
124  {
125  // array_copy and array_replace take two pointers (to arrays); we need to:
126  // 1. remove any dereference expressions (via clean_expr)
127  // 2. find the actual array objects/candidates for objects (via
128  // process_array_expr)
129  // 3. build an assignment where the type on lhs and rhs is:
130  // - array_copy: the type of the first array (even if the second is smaller)
131  // - array_replace: the type of the second array (even if it is smaller)
133  code.operands().size() == 2,
134  "expected array_copy/array_replace statement to have two operands");
135 
136  // we need to add dereferencing for both operands
137  exprt dest_array = clean_expr(code.op0(), state, false);
138  exprt src_array = clean_expr(code.op1(), state, false);
139 
140  // obtain the actual arrays
141  process_array_expr(state, dest_array);
142  process_array_expr(state, src_array);
143 
144  // check for size (or type) mismatch and adjust
145  if(dest_array.type() != src_array.type())
146  {
147  if(statement==ID_array_copy)
148  {
150  byte_extract_id(),
151  src_array,
152  from_integer(0, index_type()),
153  dest_array.type());
154  src_array.swap(be);
155  do_simplify(src_array);
156  }
157  else
158  {
159  // ID_array_replace
161  byte_extract_id(),
162  dest_array,
163  from_integer(0, index_type()),
164  src_array.type());
165  dest_array.swap(be);
166  do_simplify(dest_array);
167  }
168  }
169 
170  code_assignt assignment(dest_array, src_array);
171  symex_assign(state, assignment);
172  }
173  else if(statement==ID_array_set)
174  {
175  // array_set takes a pointer (to an array) and a value that each element
176  // should be set to; we need to:
177  // 1. remove any dereference expressions (via clean_expr)
178  // 2. find the actual array object/candidates for objects (via
179  // process_array_expr)
180  // 3. use the type of the resulting array to construct an array_of
181  // expression
183  code.operands().size() == 2,
184  "expected array_set statement to have two operands");
185 
186  // we need to add dereferencing for the first operand
187  exprt array_expr = clean_expr(code.op0(), state, false);
188 
189  // obtain the actual array(s)
190  process_array_expr(state, array_expr);
191 
192  // prepare to build the array_of
193  exprt value = clean_expr(code.op1(), state, false);
194 
195  // we might have a memset-style update of a non-array type - convert to a
196  // byte array
197  if(array_expr.type().id() != ID_array)
198  {
199  auto array_size = size_of_expr(array_expr.type(), ns);
200  CHECK_RETURN(array_size.has_value());
201  do_simplify(array_size.value());
202  array_expr = byte_extract_exprt(
203  byte_extract_id(),
204  array_expr,
205  from_integer(0, index_type()),
206  array_typet(char_type(), array_size.value()));
207  }
208 
209  const array_typet &array_type = to_array_type(array_expr.type());
210 
211  if(array_type.subtype() != value.type())
212  value = typecast_exprt(value, array_type.subtype());
213 
214  code_assignt assignment(array_expr, array_of_exprt(value, array_type));
215  symex_assign(state, assignment);
216  }
217  else if(statement==ID_array_equal)
218  {
219  // array_equal takes two pointers (to arrays) and the symbol that the result
220  // should get assigned to; we need to:
221  // 1. remove any dereference expressions (via clean_expr)
222  // 2. find the actual array objects/candidates for objects (via
223  // process_array_expr)
224  // 3. build an assignment where the lhs is the previous third argument, and
225  // the right-hand side is an equality over the arrays, if their types match;
226  // if the types don't match the result trivially is false
228  code.operands().size() == 3,
229  "expected array_equal statement to have three operands");
230 
231  // we need to add dereferencing for the first two
232  exprt array1 = clean_expr(code.op0(), state, false);
233  exprt array2 = clean_expr(code.op1(), state, false);
234 
235  // obtain the actual arrays
236  process_array_expr(state, array1);
237  process_array_expr(state, array2);
238 
239  code_assignt assignment(code.op2(), equal_exprt(array1, array2));
240 
241  // check for size (or type) mismatch
242  if(array1.type() != array2.type())
243  assignment.rhs() = false_exprt();
244 
245  symex_assign(state, assignment);
246  }
247  else if(statement==ID_user_specified_predicate ||
248  statement==ID_user_specified_parameter_predicates ||
249  statement==ID_user_specified_return_predicates)
250  {
251  // like skip
252  }
253  else if(statement==ID_fence)
254  {
255  target.memory_barrier(state.guard.as_expr(), state.source);
256  }
257  else if(statement==ID_havoc_object)
258  {
260  code.operands().size() == 1,
261  "expected havoc_object statement to have one operand");
262 
263  exprt object = clean_expr(code.op0(), state, false);
264 
265  process_array_expr(state, object);
266  havoc_rec(state, guardt(true_exprt(), guard_manager), object);
267  }
268  else
269  UNREACHABLE;
270 }
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:229
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:673
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:102
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:76
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
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:373
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
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:2964
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:53
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:1190
goto_symext::symex_assign
void symex_assign(statet &state, const code_assignt &code)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Definition: goto_symex.cpp:38
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:255
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:81
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:132
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:539
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:1367
goto_symex.h
Symbolic Execution.
goto_statet::guard
guardt guard
Definition: goto_state.h:50
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
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:428
irept::swap
void swap(irept &irep)
Definition: irep.h:463
codet::op2
exprt & op2()
Definition: expr.h:108
irept::id
const irep_idt & id() const
Definition: irep.h:418
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
goto_symext::do_simplify
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:32
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:1945
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:719
array_typet
Arrays with given size.
Definition: std_types.h:965
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
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:2047
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
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:1011
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
exprt::operands
operandst & operands()
Definition: expr.h:95
codet::op1
exprt & op1()
Definition: expr.h:105
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
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:179
c_types.h
goto_symext::symex_other
virtual void symex_other(statet &state)
Symbolically execute an OTHER instruction.
Definition: symex_other.cpp:76
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:450
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
not_exprt
Boolean negation.
Definition: std_expr.h:2843