CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 ||
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
50 guard_t.add(if_expr.cond());
51 havoc_rec(state, guard_t, if_expr.true_case());
52
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 {
72 false,
73 "Attempted to symex havoc applied to unsupported expression",
74 state.source.pc->code().pretty(),
75 dest.pretty());
76 }
77}
78
80 statet &state)
81{
82 const goto_programt::instructiont &instruction=*state.source.pc;
83
84 const codet &code = instruction.get_other();
85
86 const irep_idt &statement=code.get_statement();
87
88 if(statement==ID_expression)
89 {
90 // ignore
91 }
92 else if(statement==ID_cpp_delete ||
93 statement=="cpp_delete[]")
94 {
95 const codet clean_code = to_code(clean_expr(code, state, false));
96 symex_cpp_delete(state, clean_code);
97 }
98 else if(statement==ID_printf)
99 {
100 const codet clean_code = to_code(clean_expr(code, state, false));
101 symex_printf(state, clean_code);
102 }
103 else if(can_cast_expr<code_inputt>(code))
104 {
105 const codet clean_code = to_code(clean_expr(code, state, false));
106 symex_input(state, clean_code);
107 }
108 else if(can_cast_expr<code_outputt>(code))
109 {
110 const codet clean_code = to_code(clean_expr(code, state, false));
111 symex_output(state, clean_code);
112 }
113 else if(statement==ID_decl)
114 {
115 UNREACHABLE; // see symex_decl.cpp
116 }
117 else if(statement==ID_nondet)
118 {
119 // like skip
120 }
121 else if(statement==ID_asm)
122 {
123 // we ignore this for now
124 }
125 else if(statement==ID_array_copy ||
126 statement==ID_array_replace)
127 {
128 // array_copy and array_replace take two pointers (to arrays); we need to:
129 // 1. remove any dereference expressions (via clean_expr)
130 // 2. find the actual array objects/candidates for objects (via
131 // process_array_expr)
132 // 3. build an assignment where the type on lhs and rhs is:
133 // - array_copy: the type of the first array (even if the second is smaller)
134 // - array_replace: the type of the second array (even if it is smaller)
136 code.operands().size() == 2,
137 "expected array_copy/array_replace statement to have two operands");
138
139 // we need to add dereferencing for both operands
140 exprt dest_array = clean_expr(code.op0(), state, false);
141 exprt src_array = clean_expr(code.op1(), state, false);
142
143 // obtain the actual arrays
146
147 // check for size (or type) mismatch and adjust
148 if(dest_array.type() != src_array.type())
149 {
150 if(statement==ID_array_copy)
151 {
155 }
156 else
157 {
158 // ID_array_replace
162 }
163 }
164
166 }
167 else if(statement==ID_array_set)
168 {
169 // array_set takes a pointer (to an array) and a value that each element
170 // should be set to; we need to:
171 // 1. remove any dereference expressions (via clean_expr)
172 // 2. find the actual array object/candidates for objects (via
173 // process_array_expr)
174 // 3. use the type of the resulting array to construct an array_of
175 // expression
177 code.operands().size() == 2,
178 "expected array_set statement to have two operands");
179
180 // we need to add dereferencing for the first operand
181 exprt array_expr = clean_expr(code.op0(), state, false);
182
183 // obtain the actual array(s)
185
186 // if we dereferenced a void pointer, we may get a zero-sized (failed)
187 // object -- nothing to be assigned
188 if(array_expr.type().id() == ID_empty)
189 return;
190
191 // prepare to build the array_of
192 exprt value = clean_expr(code.op1(), state, false);
193
194 // we might have a memset-style update of a non-array type - convert to a
195 // byte array
196 if(array_expr.type().id() != ID_array)
197 {
198 auto array_size = size_of_expr(array_expr.type(), ns);
199 CHECK_RETURN(array_size.has_value());
200 do_simplify(array_size.value());
204 array_typet(char_type(), array_size.value()));
205 }
206
208
209 if(array_type.element_type() != value.type())
210 value = typecast_exprt(value, array_type.element_type());
211
213 }
214 else if(statement==ID_array_equal)
215 {
216 // array_equal takes two pointers (to arrays) and the symbol that the result
217 // should get assigned to; we need to:
218 // 1. remove any dereference expressions (via clean_expr)
219 // 2. find the actual array objects/candidates for objects (via
220 // process_array_expr)
221 // 3. build an assignment where the lhs is the previous third argument, and
222 // the right-hand side is an equality over the arrays, if their types match;
223 // if the types don't match the result trivially is false
225 code.operands().size() == 3,
226 "expected array_equal statement to have three operands");
227
228 // we need to add dereferencing for the first two
229 exprt array1 = clean_expr(code.op0(), state, false);
230 exprt array2 = clean_expr(code.op1(), state, false);
231
232 // obtain the actual arrays
235
236 exprt rhs;
237
238 // Types don't match? Make it 'false'.
239 if(array1.type() != array2.type())
240 rhs = false_exprt();
241 else
242 rhs = equal_exprt(array1, array2);
243
244 symex_assign(state, code.op2(), rhs);
245 }
246 else if(statement==ID_user_specified_predicate ||
249 {
250 // like skip
251 }
252 else if(statement==ID_fence)
253 {
254 target.memory_barrier(state.guard.as_expr(), state.source);
255 }
256 else if(statement==ID_havoc_object)
257 {
259 code.operands().size() == 1,
260 "expected havoc_object statement to have one operand");
261
262 exprt object = clean_expr(code.op0(), state, false);
263
264 process_array_expr(state, object);
265 havoc_rec(state, guardt(true_exprt(), guard_manager), object);
266 }
267 else
269}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
static exprt guard(const exprt::operandst &guards, exprt cond)
bitvector_typet char_type()
Definition c_types.cpp:106
bitvector_typet c_index_type()
Definition c_types.cpp:16
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from single element.
Definition std_expr.h:1558
Arrays with given size.
Definition std_types.h:807
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The Boolean constant false.
Definition std_expr.h:3199
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
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)
symex_target_equationt & target
The equation that this execution is building up.
Definition goto_symex.h:266
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:263
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition goto_symex.h:258
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.
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)
virtual void symex_other(statet &state)
Symbolically execute an OTHER instruction.
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
exprt as_expr() const
Definition guard_expr.h:46
The trinary if-then-else operator.
Definition std_expr.h:2497
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irep_idt & id() const
Definition irep.h:388
Boolean negation.
Definition std_expr.h:2454
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:3190
Semantic type conversion.
Definition std_expr.h:2073
Symbolic Execution.
guard_exprt guardt
Definition guard.h:29
std::optional< 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:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition invariant.h:437
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:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
goto_programt::const_targett pc