cprover
build_goto_trace.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Traces of GOTO Programs
4 
5 Author: 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/threeval.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;
48  tmp.array() = build_full_lhs_rec(
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->code.get_statement()!=ID_function_call)
176  goto_trace_step.internal=true;
177  }
178 }
179 
182 static 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 
196 static 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 }
decision_proceduret::get
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
update_internal_field
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....
Definition: build_goto_trace.cpp:146
goto_trace_stept::full_lhs_value
exprt full_lhs_value
Definition: goto_trace.h:132
typet::subtype
const typet & subtype() const
Definition: type.h:47
goto_trace_stept::formatted
bool formatted
Definition: goto_trace.h:138
goto_trace_stept::comment
std::string comment
Definition: goto_trace.h:123
ssa_exprt::get_original_name
const irep_idt get_original_name() const
Definition: ssa_expr.h:49
build_goto_trace
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...
Definition: build_goto_trace.cpp:204
arith_tools.h
ssa_step_predicatet
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> ssa_step_predicatet
Definition: build_goto_trace.h:49
typet
The type of an expression, extends irept.
Definition: type.h:29
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:45
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
goto_trace_stept::assignment_typet::STATE
@ STATE
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
goto_trace_stept::internal
bool internal
Definition: goto_trace.h:103
threeval.h
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
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
decision_proceduret
Definition: decision_procedure.h:21
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:101
goto_trace_stept::type
typet type
Definition: goto_trace.h:97
SSA_stept::assignment_type
symex_targett::assignment_typet assignment_type
Definition: ssa_step.h:144
goto_tracet::steps
stepst steps
Definition: goto_trace.h:174
exprt
Base class for all expressions.
Definition: expr.h:53
is_failed_assertion_step
static bool is_failed_assertion_step(symex_target_equationt::SSA_stepst::const_iterator step, const decision_proceduret &decision_procedure)
Definition: build_goto_trace.cpp:435
set_internal_dynamic_object
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.
Definition: build_goto_trace.cpp:117
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
goto_trace_stept
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
SSA_stept::source
symex_targett::sourcet source
Definition: ssa_step.h:47
goto_trace_stept::called_function
irep_idt called_function
Definition: goto_trace.h:141
partial_order_concurrencyt::rw_clock_id
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
Build identifier for the read/write clock variable.
Definition: partial_order_concurrency.cpp:125
decision_procedure.h
Decision Procedure Interface.
replace_nondet_in_type
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.
Definition: build_goto_trace.cpp:183
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER
@ VISIBLE_ACTUAL_PARAMETER
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
byte_operators.h
Expression classes for byte-level operators.
goto_trace_stept::typet::OUTPUT
@ OUTPUT
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER
@ HIDDEN_ACTUAL_PARAMETER
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
goto_trace_stept::cond_expr
exprt cond_expr
Definition: goto_trace.h:119
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
goto_trace_stept::step_nr
std::size_t step_nr
Number of the step in the trace.
Definition: goto_trace.h:53
goto_trace_stept::full_lhs
exprt full_lhs
Definition: goto_trace.h:126
goto_trace_stept::function_arguments
std::vector< exprt > function_arguments
Definition: goto_trace.h:144
goto_trace_stept::pc
goto_programt::const_targett pc
Definition: goto_trace.h:112
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_trace_stept::assignment_typet::ACTUAL_PARAMETER
@ ACTUAL_PARAMETER
goto_trace_stept::typet::INPUT
@ INPUT
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
goto_trace_stept::thread_nr
unsigned thread_nr
Definition: goto_trace.h:115
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
simplify_expr.h
goto_trace_stept::property_id
irep_idt property_id
Definition: goto_trace.h:122
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
goto_trace_stept::cond_value
bool cond_value
Definition: goto_trace.h:118
symex_targett::assignment_typet::PHI
@ PHI
array_typet
Arrays with given size.
Definition: std_types.h:965
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
build_full_lhs_rec
static exprt build_full_lhs_rec(const decision_proceduret &decision_procedure, const namespacet &ns, const exprt &src_original, const exprt &src_ssa)
Definition: build_goto_trace.cpp:27
goto_trace_stept::assignment_type
assignment_typet assignment_type
Definition: goto_trace.h:107
symbolt
Symbol table entry.
Definition: symbol.h:28
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:364
SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: ssa_step.h:143
goto_trace_stept::hidden
bool hidden
Definition: goto_trace.h:100
build_goto_trace.h
Traces of GOTO Programs.
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
SSA_stept::guard_handle
exprt guard_handle
Definition: ssa_step.h:138
goto_trace_stept::format_string
irep_idt format_string
Definition: goto_trace.h:135
goto_functions.h
Goto Programs with Functions.
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
symex_targett::assignment_typet::GUARD
@ GUARD
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
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
index_exprt
Array index operator.
Definition: std_expr.h:1293
goto_trace_stept::io_id
irep_idt io_id
Definition: goto_trace.h:135
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
partial_order_concurrency.h
Add constraints to equation encoding partial orders on events.
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:40
goto_trace_stept::io_args
io_argst io_args
Definition: goto_trace.h:137
goto_trace_stept::function_id
irep_idt function_id
Definition: goto_trace.h:111
SSA_stept::is_function_call
bool is_function_call() const
Definition: ssa_step.h:90
validation_modet::INVARIANT
@ INVARIANT