cprover
Loading...
Searching...
No Matches
build_goto_trace.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Traces of GOTO Programs
4
5Author: Daniel Kroening
6
7 Date: July 2005
8
9\*******************************************************************/
10
13
14#include "build_goto_trace.h"
15
16#include <util/arith_tools.h>
17#include <util/byte_operators.h>
18#include <util/simplify_expr.h>
19#include <util/symbol.h>
20
22
24
26
28 const decision_proceduret &decision_procedure,
29 const namespacet &ns,
30 const exprt &src_original, // original identifiers
31 const exprt &src_ssa) // renamed identifiers
32{
33 if(src_ssa.id()!=src_original.id())
34 return src_original;
35
36 const irep_idt id=src_original.id();
37
38 if(id==ID_index)
39 {
40 // get index value from src_ssa
41 exprt index_value = decision_procedure.get(to_index_expr(src_ssa).index());
42
43 if(index_value.is_not_nil())
44 {
45 simplify(index_value, ns);
46 index_exprt tmp=to_index_expr(src_original);
47 tmp.index()=index_value;
49 decision_procedure,
50 ns,
51 to_index_expr(src_original).array(),
52 to_index_expr(src_ssa).array());
53 return std::move(tmp);
54 }
55
56 return src_original;
57 }
58 else if(id==ID_member)
59 {
60 member_exprt tmp=to_member_expr(src_original);
62 decision_procedure,
63 ns,
64 to_member_expr(src_original).struct_op(),
65 to_member_expr(src_ssa).struct_op());
66 }
67 else if(id==ID_if)
68 {
69 if_exprt tmp2=to_if_expr(src_original);
70
72 decision_procedure,
73 ns,
74 tmp2.false_case(),
75 to_if_expr(src_ssa).false_case());
76
78 decision_procedure,
79 ns,
80 tmp2.true_case(),
81 to_if_expr(src_ssa).true_case());
82
83 exprt tmp = decision_procedure.get(to_if_expr(src_ssa).cond());
84
85 if(tmp.is_true())
86 return tmp2.true_case();
87 else if(tmp.is_false())
88 return tmp2.false_case();
89 else
90 return std::move(tmp2);
91 }
92 else if(id==ID_typecast)
93 {
94 typecast_exprt tmp=to_typecast_expr(src_original);
95 tmp.op() = build_full_lhs_rec(
96 decision_procedure,
97 ns,
98 to_typecast_expr(src_original).op(),
99 to_typecast_expr(src_ssa).op());
100 return std::move(tmp);
101 }
102 else if(id==ID_byte_extract_little_endian ||
103 id==ID_byte_extract_big_endian)
104 {
105 byte_extract_exprt tmp = to_byte_extract_expr(src_original);
106 tmp.op() = build_full_lhs_rec(
107 decision_procedure, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());
108
109 // re-write into big case-split
110 }
111
112 return src_original;
113}
114
118 const exprt &expr,
119 goto_trace_stept &goto_trace_step,
120 const namespacet &ns)
121{
122 if(expr.id()==ID_symbol)
123 {
124 const auto &type = expr.type();
125 if(type.id() != ID_code && type.id() != ID_mathematical_function)
126 {
127 const irep_idt &id = to_ssa_expr(expr).get_original_name();
128 const symbolt *symbol;
129 if(!ns.lookup(id, symbol))
130 {
131 bool result = symbol->type.get_bool(ID_C_dynamic);
132 if(result)
133 goto_trace_step.internal = true;
134 }
135 }
136 }
137 else
138 {
139 forall_operands(it, expr)
140 set_internal_dynamic_object(*it, goto_trace_step, ns);
141 }
142}
143
147 const SSA_stept &SSA_step,
148 goto_trace_stept &goto_trace_step,
149 const namespacet &ns)
150{
151 // set internal for dynamic_object in both lhs and rhs expressions
152 set_internal_dynamic_object(SSA_step.ssa_lhs, goto_trace_step, ns);
153 set_internal_dynamic_object(SSA_step.ssa_rhs, goto_trace_step, ns);
154
155 // set internal field to CPROVER functions (e.g., __CPROVER_initialize)
156 if(SSA_step.is_function_call())
157 {
158 if(SSA_step.source.pc->source_location().as_string().empty())
159 goto_trace_step.internal=true;
160 }
161
162 // set internal field to input and output steps
163 if(goto_trace_step.type==goto_trace_stept::typet::OUTPUT ||
164 goto_trace_step.type==goto_trace_stept::typet::INPUT)
165 {
166 goto_trace_step.internal=true;
167 }
168
169 // set internal field to _start function-return step
171 {
172 // "__CPROVER_*" function calls in __CPROVER_start are already marked as
173 // internal. Don't mark any other function calls (i.e. "main"), function
174 // arguments or any other parts of a code_function_callt as internal.
175 if(SSA_step.source.pc->get_code().get_statement() != ID_function_call)
176 goto_trace_step.internal=true;
177 }
178}
179
182static void
184{
185 if(type.id() == ID_array)
186 {
187 array_typet &array_type = to_array_type(type);
188 array_type.size() = solver.get(array_type.size());
189 }
190 if(type.has_subtype())
192}
193
196static void
198{
200 for(auto &sub : expr.operands())
202}
203
205 const symex_target_equationt &target,
206 ssa_step_predicatet is_last_step_to_keep,
207 const decision_proceduret &decision_procedure,
208 const namespacet &ns,
209 goto_tracet &goto_trace)
210{
211 // We need to re-sort the steps according to their clock.
212 // Furthermore, read-events need to occur before write
213 // events with the same clock.
214
215 typedef symex_target_equationt::SSA_stepst::const_iterator ssa_step_iteratort;
216 typedef std::map<mp_integer, std::vector<ssa_step_iteratort>> time_mapt;
217 time_mapt time_map;
218
219 mp_integer current_time=0;
220
221 ssa_step_iteratort last_step_to_keep = target.SSA_steps.end();
222 bool last_step_was_kept = false;
223
224 // First sort the SSA steps by time, in the process dropping steps
225 // we definitely don't want to retain in the final trace:
226
227 for(ssa_step_iteratort it = target.SSA_steps.begin();
228 it != target.SSA_steps.end();
229 it++)
230 {
231 if(
232 last_step_to_keep == target.SSA_steps.end() &&
233 is_last_step_to_keep(it, decision_procedure))
234 {
235 last_step_to_keep = it;
236 }
237
238 const SSA_stept &SSA_step = *it;
239
240 if(!decision_procedure.get(SSA_step.guard_handle).is_true())
241 continue;
242
243 if(it->is_constraint() ||
244 it->is_spawn())
245 continue;
246 else if(it->is_atomic_begin())
247 {
248 // for atomic sections the timing can only be determined once we see
249 // a shared read or write (if there is none, the time will be
250 // reverted to the time before entering the atomic section); we thus
251 // use a temporary negative time slot to gather all events
252 current_time*=-1;
253 continue;
254 }
255 else if(it->is_shared_read() || it->is_shared_write() ||
256 it->is_atomic_end())
257 {
258 mp_integer time_before=current_time;
259
260 if(it->is_shared_read() || it->is_shared_write())
261 {
262 // these are just used to get the time stamp -- the clock type is
263 // computed to be of the minimal necessary size, but we don't need to
264 // know it to get the value so just use typeless
265 exprt clock_value = decision_procedure.get(
267
268 const auto cv = numeric_cast<mp_integer>(clock_value);
269 if(cv.has_value())
270 current_time = *cv;
271 else
272 current_time = 0;
273 }
274 else if(it->is_atomic_end() && current_time<0)
275 current_time*=-1;
276
277 INVARIANT(current_time >= 0, "time keeping inconsistency");
278 // move any steps gathered in an atomic section
279
280 if(time_before<0)
281 {
282 time_mapt::const_iterator time_before_steps_it =
283 time_map.find(time_before);
284
285 if(time_before_steps_it != time_map.end())
286 {
287 std::vector<ssa_step_iteratort> &current_time_steps =
288 time_map[current_time];
289
290 current_time_steps.insert(
291 current_time_steps.end(),
292 time_before_steps_it->second.begin(),
293 time_before_steps_it->second.end());
294
295 time_map.erase(time_before_steps_it);
296 }
297 }
298
299 continue;
300 }
301
302 // drop PHI and GUARD assignments altogether
303 if(it->is_assignment() &&
304 (SSA_step.assignment_type==
306 SSA_step.assignment_type==
308 {
309 continue;
310 }
311
312 if(it == last_step_to_keep)
313 {
314 last_step_was_kept = true;
315 }
316
317 time_map[current_time].push_back(it);
318 }
319
320 INVARIANT(
321 last_step_to_keep == target.SSA_steps.end() || last_step_was_kept,
322 "last step in SSA trace to keep must not be filtered out as a sync "
323 "instruction, not-taken branch, PHI node, or similar");
324
325 // Now build the GOTO trace, ordered by time, then by SSA trace order.
326
327 // produce the step numbers
328 unsigned step_nr = 0;
329
330 for(const auto &time_and_ssa_steps : time_map)
331 {
332 for(const auto &ssa_step_it : time_and_ssa_steps.second)
333 {
334 const auto &SSA_step = *ssa_step_it;
335 goto_trace.steps.push_back(goto_trace_stept());
336 goto_trace_stept &goto_trace_step = goto_trace.steps.back();
337
338 goto_trace_step.step_nr = ++step_nr;
339
340 goto_trace_step.thread_nr = SSA_step.source.thread_nr;
341 goto_trace_step.pc = SSA_step.source.pc;
342 goto_trace_step.function_id = SSA_step.source.function_id;
343 if(SSA_step.is_assert())
344 {
345 goto_trace_step.comment = SSA_step.comment;
346 goto_trace_step.property_id = SSA_step.get_property_id();
347 }
348 goto_trace_step.type = SSA_step.type;
349 goto_trace_step.hidden = SSA_step.hidden;
350 goto_trace_step.format_string = SSA_step.format_string;
351 goto_trace_step.io_id = SSA_step.io_id;
352 goto_trace_step.formatted = SSA_step.formatted;
353 goto_trace_step.called_function = SSA_step.called_function;
354 goto_trace_step.function_arguments = SSA_step.converted_function_arguments;
355
356 for(auto &arg : goto_trace_step.function_arguments)
357 arg = decision_procedure.get(arg);
358
359 // update internal field for specific variables in the counterexample
360 update_internal_field(SSA_step, goto_trace_step, ns);
361
362 goto_trace_step.assignment_type =
363 (SSA_step.is_assignment() &&
364 (SSA_step.assignment_type ==
366 SSA_step.assignment_type ==
370
371 if(SSA_step.original_full_lhs.is_not_nil())
372 {
373 goto_trace_step.full_lhs = simplify_expr(
375 decision_procedure,
376 ns,
377 SSA_step.original_full_lhs,
378 SSA_step.ssa_full_lhs),
379 ns);
380 replace_nondet_in_type(goto_trace_step.full_lhs, decision_procedure);
381 }
382
383 if(SSA_step.ssa_full_lhs.is_not_nil())
384 {
385 goto_trace_step.full_lhs_value =
386 decision_procedure.get(SSA_step.ssa_full_lhs);
387 simplify(goto_trace_step.full_lhs_value, ns);
389 goto_trace_step.full_lhs_value, decision_procedure);
390 }
391
392 for(const auto &j : SSA_step.converted_io_args)
393 {
394 if(j.is_constant() || j.id() == ID_string_constant)
395 {
396 goto_trace_step.io_args.push_back(j);
397 }
398 else
399 {
400 exprt tmp = decision_procedure.get(j);
401 goto_trace_step.io_args.push_back(tmp);
402 }
403 }
404
405 if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto())
406 {
407 goto_trace_step.cond_expr = SSA_step.cond_expr;
408
409 goto_trace_step.cond_value =
410 decision_procedure.get(SSA_step.cond_handle).is_true();
411 }
412
413 if(ssa_step_it == last_step_to_keep)
414 return;
415 }
416 }
417}
418
420 const symex_target_equationt &target,
421 symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
422 const decision_proceduret &decision_procedure,
423 const namespacet &ns,
424 goto_tracet &goto_trace)
425{
426 const auto is_last_step_to_keep =
427 [last_step_to_keep](
428 symex_target_equationt::SSA_stepst::const_iterator it,
429 const decision_proceduret &) { return last_step_to_keep == it; };
430
431 return build_goto_trace(
432 target, is_last_step_to_keep, decision_procedure, ns, goto_trace);
433}
434
436 symex_target_equationt::SSA_stepst::const_iterator step,
437 const decision_proceduret &decision_procedure)
438{
439 return step->is_assert() &&
440 decision_procedure.get(step->cond_handle).is_false();
441}
442
444 const symex_target_equationt &target,
445 const decision_proceduret &decision_procedure,
446 const namespacet &ns,
447 goto_tracet &goto_trace)
448{
450 target, is_failed_assertion_step, decision_procedure, ns, goto_trace);
451}
static exprt build_full_lhs_rec(const decision_proceduret &decision_procedure, const namespacet &ns, const exprt &src_original, const exprt &src_ssa)
static void set_internal_dynamic_object(const exprt &expr, goto_trace_stept &goto_trace_step, const namespacet &ns)
set internal field for variable assignment related to dynamic_object[0-9] and dynamic_[0-9]_array.
static void update_internal_field(const SSA_stept &SSA_step, goto_trace_stept &goto_trace_step, const namespacet &ns)
set internal for variables assignments related to dynamic_object and CPROVER internal functions (e....
static bool is_failed_assertion_step(symex_target_equationt::SSA_stepst::const_iterator step, const decision_proceduret &decision_procedure)
static void replace_nondet_in_type(typet &type, const decision_proceduret &solver)
Replace nondet values that appear in type by their values as found by solver.
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace)
Build a trace by going through the steps of target and stopping after the step matching a given condi...
Traces of GOTO Programs.
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> ssa_step_predicatet
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Single SSA step in the equation.
Definition: ssa_step.h:47
exprt guard_handle
Definition: ssa_step.h:140
symex_targett::assignment_typet assignment_type
Definition: ssa_step.h:146
exprt ssa_rhs
Definition: ssa_step.h:145
symex_targett::sourcet source
Definition: ssa_step.h:49
bool is_function_call() const
Definition: ssa_step.h:92
ssa_exprt ssa_lhs
Definition: ssa_step.h:143
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:790
Expression of type type extracted from some object op starting at position offset (given in number of...
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
std::vector< exprt > function_arguments
Definition: goto_trace.h:144
irep_idt format_string
Definition: goto_trace.h:135
std::string comment
Definition: goto_trace.h:123
exprt full_lhs_value
Definition: goto_trace.h:132
goto_programt::const_targett pc
Definition: goto_trace.h:112
irep_idt function_id
Definition: goto_trace.h:111
io_argst io_args
Definition: goto_trace.h:137
unsigned thread_nr
Definition: goto_trace.h:115
irep_idt property_id
Definition: goto_trace.h:122
irep_idt called_function
Definition: goto_trace.h:141
assignment_typet assignment_type
Definition: goto_trace.h:107
std::size_t step_nr
Number of the step in the trace.
Definition: goto_trace.h:53
irep_idt io_id
Definition: goto_trace.h:135
Trace of a GOTO program.
Definition: goto_trace.h:175
stepst steps
Definition: goto_trace.h:178
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
Build identifier for the read/write clock variable.
const irep_idt get_original_name() const
Definition: ssa_expr.h:49
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:99
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
bool has_subtype() const
Definition: type.h:66
const exprt & op() const
Definition: std_expr.h:293
Decision Procedure Interface.
#define forall_operands(it, expr)
Definition: expr.h:18
Goto Programs with Functions.
Add constraints to equation encoding partial orders on events.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
int solver(std::istream &in)
BigInt mp_integer
Definition: smt_terms.h:12
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
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
Symbol table entry.