cprover
symex_other.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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#include <util/std_code.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 auto rhs =
36 side_effect_expr_nondett(dest.type(), state.source.pc->source_location());
37
38 symex_assign(state, lhs, rhs);
39 }
40 else if(dest.id()==ID_byte_extract_little_endian ||
41 dest.id()==ID_byte_extract_big_endian)
42 {
43 havoc_rec(state, guard, to_byte_extract_expr(dest).op());
44 }
45 else if(dest.id()==ID_if)
46 {
47 const if_exprt &if_expr=to_if_expr(dest);
48
49 guardt guard_t=state.guard;
50 guard_t.add(if_expr.cond());
51 havoc_rec(state, guard_t, if_expr.true_case());
52
53 guardt guard_f=state.guard;
54 guard_f.add(not_exprt(if_expr.cond()));
55 havoc_rec(state, guard_f, if_expr.false_case());
56 }
57 else if(dest.id()==ID_typecast)
58 {
59 havoc_rec(state, guard, to_typecast_expr(dest).op());
60 }
61 else if(dest.id()==ID_index)
62 {
63 havoc_rec(state, guard, to_index_expr(dest).array());
64 }
65 else if(dest.id()==ID_member)
66 {
67 havoc_rec(state, guard, to_member_expr(dest).struct_op());
68 }
69 else
70 {
71 // consider printing a warning
72 }
73}
74
76 statet &state)
77{
78 const goto_programt::instructiont &instruction=*state.source.pc;
79
80 const codet &code = instruction.get_other();
81
82 const irep_idt &statement=code.get_statement();
83
84 if(statement==ID_expression)
85 {
86 // ignore
87 }
88 else if(statement==ID_cpp_delete ||
89 statement=="cpp_delete[]")
90 {
91 const codet clean_code = to_code(clean_expr(code, state, false));
92 symex_cpp_delete(state, clean_code);
93 }
94 else if(statement==ID_printf)
95 {
96 const codet clean_code = to_code(clean_expr(code, state, false));
97 symex_printf(state, clean_code);
98 }
99 else if(can_cast_expr<code_inputt>(code))
100 {
101 const codet clean_code = to_code(clean_expr(code, state, false));
102 symex_input(state, clean_code);
103 }
104 else if(can_cast_expr<code_outputt>(code))
105 {
106 const codet clean_code = to_code(clean_expr(code, state, false));
107 symex_output(state, clean_code);
108 }
109 else if(statement==ID_decl)
110 {
111 UNREACHABLE; // see symex_decl.cpp
112 }
113 else if(statement==ID_nondet)
114 {
115 // like skip
116 }
117 else if(statement==ID_asm)
118 {
119 // we ignore this for now
120 }
121 else if(statement==ID_array_copy ||
122 statement==ID_array_replace)
123 {
124 // array_copy and array_replace take two pointers (to arrays); we need to:
125 // 1. remove any dereference expressions (via clean_expr)
126 // 2. find the actual array objects/candidates for objects (via
127 // process_array_expr)
128 // 3. build an assignment where the type on lhs and rhs is:
129 // - array_copy: the type of the first array (even if the second is smaller)
130 // - array_replace: the type of the second array (even if it is smaller)
132 code.operands().size() == 2,
133 "expected array_copy/array_replace statement to have two operands");
134
135 // we need to add dereferencing for both operands
136 exprt dest_array = clean_expr(code.op0(), state, false);
137 exprt src_array = clean_expr(code.op1(), state, false);
138
139 // obtain the actual arrays
140 process_array_expr(state, dest_array);
141 process_array_expr(state, src_array);
142
143 // check for size (or type) mismatch and adjust
144 if(dest_array.type() != src_array.type())
145 {
146 if(statement==ID_array_copy)
147 {
148 src_array = make_byte_extract(
149 src_array, from_integer(0, c_index_type()), dest_array.type());
150 do_simplify(src_array);
151 }
152 else
153 {
154 // ID_array_replace
155 dest_array = make_byte_extract(
156 dest_array, from_integer(0, c_index_type()), src_array.type());
157 do_simplify(dest_array);
158 }
159 }
160
161 symex_assign(state, dest_array, src_array);
162 }
163 else if(statement==ID_array_set)
164 {
165 // array_set takes a pointer (to an array) and a value that each element
166 // should be set to; we need to:
167 // 1. remove any dereference expressions (via clean_expr)
168 // 2. find the actual array object/candidates for objects (via
169 // process_array_expr)
170 // 3. use the type of the resulting array to construct an array_of
171 // expression
173 code.operands().size() == 2,
174 "expected array_set statement to have two operands");
175
176 // we need to add dereferencing for the first operand
177 exprt array_expr = clean_expr(code.op0(), state, false);
178
179 // obtain the actual array(s)
180 process_array_expr(state, array_expr);
181
182 // prepare to build the array_of
183 exprt value = clean_expr(code.op1(), state, false);
184
185 // we might have a memset-style update of a non-array type - convert to a
186 // byte array
187 if(array_expr.type().id() != ID_array)
188 {
189 auto array_size = size_of_expr(array_expr.type(), ns);
190 CHECK_RETURN(array_size.has_value());
191 do_simplify(array_size.value());
192 array_expr = make_byte_extract(
193 array_expr,
195 array_typet(char_type(), array_size.value()));
196 }
197
198 const array_typet &array_type = to_array_type(array_expr.type());
199
200 if(array_type.element_type() != value.type())
201 value = typecast_exprt(value, array_type.element_type());
202
203 symex_assign(state, array_expr, array_of_exprt(value, array_type));
204 }
205 else if(statement==ID_array_equal)
206 {
207 // array_equal takes two pointers (to arrays) and the symbol that the result
208 // should get assigned to; we need to:
209 // 1. remove any dereference expressions (via clean_expr)
210 // 2. find the actual array objects/candidates for objects (via
211 // process_array_expr)
212 // 3. build an assignment where the lhs is the previous third argument, and
213 // the right-hand side is an equality over the arrays, if their types match;
214 // if the types don't match the result trivially is false
216 code.operands().size() == 3,
217 "expected array_equal statement to have three operands");
218
219 // we need to add dereferencing for the first two
220 exprt array1 = clean_expr(code.op0(), state, false);
221 exprt array2 = clean_expr(code.op1(), state, false);
222
223 // obtain the actual arrays
224 process_array_expr(state, array1);
225 process_array_expr(state, array2);
226
227 exprt rhs = equal_exprt(array1, array2);
228
229 // check for size (or type) mismatch
230 if(array1.type() != array2.type())
231 rhs = false_exprt();
232
233 symex_assign(state, code.op2(), rhs);
234 }
235 else if(statement==ID_user_specified_predicate ||
236 statement==ID_user_specified_parameter_predicates ||
237 statement==ID_user_specified_return_predicates)
238 {
239 // like skip
240 }
241 else if(statement==ID_fence)
242 {
243 target.memory_barrier(state.guard.as_expr(), state.source);
244 }
245 else if(statement==ID_havoc_object)
246 {
248 code.operands().size() == 1,
249 "expected havoc_object statement to have one operand");
250
251 exprt object = clean_expr(code.op0(), state, false);
252
253 process_array_expr(state, object);
254 havoc_rec(state, guardt(true_exprt(), guard_manager), object);
255 }
256 else
258}
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 char_type()
Definition: c_types.cpp:124
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Array constructor from single element.
Definition: std_expr.h:1411
Arrays with given size.
Definition: std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
const irep_idt & get_statement() const
Definition: std_code_base.h:65
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:2865
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:313
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:20
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:40
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:34
virtual void symex_other(statet &state)
Symbolically execute an OTHER instruction.
Definition: symex_other.cpp:75
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:2226
exprt & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
const irep_idt & id() const
Definition: irep.h:396
Boolean negation.
Definition: std_expr.h:2181
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
bool can_cast_expr< code_inputt >(const exprt &base)
bool can_cast_expr< code_outputt >(const exprt &base)
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
const codet & to_code(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
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.