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 <cassert>
17 
18 #include <util/threeval.h>
19 #include <util/simplify_expr.h>
20 #include <util/arith_tools.h>
21 
22 #include <solvers/prop/prop_conv.h>
23 #include <solvers/prop/prop.h>
24 
26 
28  const prop_convt &prop_conv,
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=prop_conv.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()=
49  build_full_lhs_rec(prop_conv, ns,
50  to_index_expr(src_original).array(),
51  to_index_expr(src_ssa).array());
52  return tmp;
53  }
54 
55  return src_original;
56  }
57  else if(id==ID_member)
58  {
59  member_exprt tmp=to_member_expr(src_original);
61  prop_conv, ns,
62  to_member_expr(src_original).struct_op(),
63  to_member_expr(src_ssa).struct_op());
64  }
65  else if(id==ID_if)
66  {
67  if_exprt tmp2=to_if_expr(src_original);
68 
69  tmp2.false_case()=build_full_lhs_rec(prop_conv, ns,
70  tmp2.false_case(), to_if_expr(src_ssa).false_case());
71 
72  tmp2.true_case()=build_full_lhs_rec(prop_conv, ns,
73  tmp2.true_case(), to_if_expr(src_ssa).true_case());
74 
75  exprt tmp=prop_conv.get(to_if_expr(src_ssa).cond());
76 
77  if(tmp.is_true())
78  return tmp2.true_case();
79  else if(tmp.is_false())
80  return tmp2.false_case();
81  else
82  return tmp2;
83  }
84  else if(id==ID_typecast)
85  {
86  typecast_exprt tmp=to_typecast_expr(src_original);
87  tmp.op()=build_full_lhs_rec(prop_conv, ns,
88  to_typecast_expr(src_original).op(), to_typecast_expr(src_ssa).op());
89  return tmp;
90  }
91  else if(id==ID_byte_extract_little_endian ||
92  id==ID_byte_extract_big_endian)
93  {
94  exprt tmp=src_original;
95  assert(tmp.operands().size()==2);
96  tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());
97 
98  // re-write into big case-split
99  }
100 
101  return src_original;
102 }
103 
107  const exprt &expr,
108  goto_trace_stept &goto_trace_step,
109  const namespacet &ns)
110 {
111  if(expr.id()==ID_symbol)
112  {
113  const irep_idt &id=to_ssa_expr(expr).get_original_name();
114  const symbolt *symbol;
115  if(!ns.lookup(id, symbol))
116  {
117  bool result = symbol->type.get_bool(ID_C_dynamic);
118  if(result)
119  goto_trace_step.internal=true;
120  }
121  }
122  else
123  {
124  forall_operands(it, expr)
125  set_internal_dynamic_object(*it, goto_trace_step, ns);
126  }
127 }
128 
132  const symex_target_equationt::SSA_stept &SSA_step,
133  goto_trace_stept &goto_trace_step,
134  const namespacet &ns)
135 {
136  // set internal for dynamic_object in both lhs and rhs expressions
137  set_internal_dynamic_object(SSA_step.ssa_lhs, goto_trace_step, ns);
138  set_internal_dynamic_object(SSA_step.ssa_rhs, goto_trace_step, ns);
139 
140  // set internal field to CPROVER functions (e.g., __CPROVER_initialize)
141  if(SSA_step.is_function_call())
142  {
143  if(SSA_step.source.pc->source_location.as_string().empty())
144  goto_trace_step.internal=true;
145  }
146 
147  // set internal field to input and output steps
148  if(goto_trace_step.type==goto_trace_stept::typet::OUTPUT ||
149  goto_trace_step.type==goto_trace_stept::typet::INPUT)
150  {
151  goto_trace_step.internal=true;
152  }
153 
154  // set internal field to _start function-return step
155  if(SSA_step.source.pc->function==goto_functionst::entry_point())
156  {
157  // "__CPROVER_*" function calls in __CPROVER_start are already marked as
158  // internal. Don't mark any other function calls (i.e. "main"), function
159  // arguments or any other parts of a code_function_callt as internal.
160  if(SSA_step.source.pc->code.get_statement()!=ID_function_call)
161  goto_trace_step.internal=true;
162  }
163 }
164 
166  const symex_target_equationt &target,
167  ssa_step_predicatet is_last_step_to_keep,
168  const prop_convt &prop_conv,
169  const namespacet &ns,
170  goto_tracet &goto_trace)
171 {
172  // We need to re-sort the steps according to their clock.
173  // Furthermore, read-events need to occur before write
174  // events with the same clock.
175 
176  typedef symex_target_equationt::SSA_stepst::const_iterator ssa_step_iteratort;
177  typedef std::map<mp_integer, std::vector<ssa_step_iteratort>> time_mapt;
178  time_mapt time_map;
179 
180  mp_integer current_time=0;
181 
182  ssa_step_iteratort last_step_to_keep = target.SSA_steps.end();
183  bool last_step_was_kept = false;
184 
185  // First sort the SSA steps by time, in the process dropping steps
186  // we definitely don't want to retain in the final trace:
187 
188  for(ssa_step_iteratort it = target.SSA_steps.begin();
189  it != target.SSA_steps.end();
190  it++)
191  {
192  if(
193  last_step_to_keep == target.SSA_steps.end() &&
194  is_last_step_to_keep(it, prop_conv))
195  {
196  last_step_to_keep = it;
197  }
198 
199  const symex_target_equationt::SSA_stept &SSA_step=*it;
200 
201  if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
202  continue;
203 
204  if(it->is_constraint() ||
205  it->is_spawn())
206  continue;
207  else if(it->is_atomic_begin())
208  {
209  // for atomic sections the timing can only be determined once we see
210  // a shared read or write (if there is none, the time will be
211  // reverted to the time before entering the atomic section); we thus
212  // use a temporary negative time slot to gather all events
213  current_time*=-1;
214  continue;
215  }
216  else if(it->is_shared_read() || it->is_shared_write() ||
217  it->is_atomic_end())
218  {
219  mp_integer time_before=current_time;
220 
221  if(it->is_shared_read() || it->is_shared_write())
222  {
223  // these are just used to get the time stamp
224  exprt clock_value=prop_conv.get(
226 
227  to_integer(clock_value, current_time);
228  }
229  else if(it->is_atomic_end() && current_time<0)
230  current_time*=-1;
231 
232  assert(current_time>=0);
233  // move any steps gathered in an atomic section
234 
235  if(time_before<0)
236  {
237  time_mapt::const_iterator time_before_steps_it =
238  time_map.find(time_before);
239 
240  if(time_before_steps_it != time_map.end())
241  {
242  std::vector<ssa_step_iteratort> &current_time_steps =
243  time_map[current_time];
244 
245  current_time_steps.insert(
246  current_time_steps.end(),
247  time_before_steps_it->second.begin(),
248  time_before_steps_it->second.end());
249 
250  time_map.erase(time_before_steps_it);
251  }
252  }
253 
254  continue;
255  }
256 
257  // drop PHI and GUARD assignments altogether
258  if(it->is_assignment() &&
259  (SSA_step.assignment_type==
261  SSA_step.assignment_type==
263  {
264  continue;
265  }
266 
267  if(it == last_step_to_keep)
268  {
269  last_step_was_kept = true;
270  }
271 
272  time_map[current_time].push_back(it);
273  }
274 
275  INVARIANT(
276  last_step_to_keep == target.SSA_steps.end() || last_step_was_kept,
277  "last step in SSA trace to keep must not be filtered out as a sync "
278  "instruction, not-taken branch, PHI node, or similar");
279 
280  // Now build the GOTO trace, ordered by time, then by SSA trace order.
281 
282  // produce the step numbers
283  unsigned step_nr = 0;
284 
285  for(const auto &time_and_ssa_steps : time_map)
286  {
287  for(const auto ssa_step_it : time_and_ssa_steps.second)
288  {
289  const auto &SSA_step = *ssa_step_it;
290  goto_trace.steps.push_back(goto_trace_stept());
291  goto_trace_stept &goto_trace_step = goto_trace.steps.back();
292 
293  goto_trace_step.step_nr = ++step_nr;
294 
295  goto_trace_step.thread_nr = SSA_step.source.thread_nr;
296  goto_trace_step.pc = SSA_step.source.pc;
297  goto_trace_step.comment = SSA_step.comment;
298  if(SSA_step.ssa_lhs.is_not_nil())
299  {
300  goto_trace_step.lhs_object =
301  ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
302  }
303  else
304  {
305  goto_trace_step.lhs_object.make_nil();
306  }
307  goto_trace_step.type = SSA_step.type;
308  goto_trace_step.hidden = SSA_step.hidden;
309  goto_trace_step.format_string = SSA_step.format_string;
310  goto_trace_step.io_id = SSA_step.io_id;
311  goto_trace_step.formatted = SSA_step.formatted;
312  goto_trace_step.identifier = SSA_step.identifier;
313 
314  // update internal field for specific variables in the counterexample
315  update_internal_field(SSA_step, goto_trace_step, ns);
316 
317  goto_trace_step.assignment_type =
318  (SSA_step.is_assignment() &&
319  (SSA_step.assignment_type ==
321  SSA_step.assignment_type ==
325 
326  if(SSA_step.original_full_lhs.is_not_nil())
327  {
328  goto_trace_step.full_lhs = build_full_lhs_rec(
329  prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
330  }
331 
332  if(SSA_step.ssa_lhs.is_not_nil())
333  goto_trace_step.lhs_object_value = prop_conv.get(SSA_step.ssa_lhs);
334 
335  if(SSA_step.ssa_full_lhs.is_not_nil())
336  {
337  goto_trace_step.full_lhs_value = prop_conv.get(SSA_step.ssa_full_lhs);
338  simplify(goto_trace_step.full_lhs_value, ns);
339  }
340 
341  for(const auto &j : SSA_step.converted_io_args)
342  {
343  if(j.is_constant() || j.id() == ID_string_constant)
344  {
345  goto_trace_step.io_args.push_back(j);
346  }
347  else
348  {
349  exprt tmp = prop_conv.get(j);
350  goto_trace_step.io_args.push_back(tmp);
351  }
352  }
353 
354  if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto())
355  {
356  goto_trace_step.cond_expr = SSA_step.cond_expr;
357 
358  goto_trace_step.cond_value =
359  prop_conv.l_get(SSA_step.cond_literal).is_true();
360  }
361 
362  if(ssa_step_it == last_step_to_keep)
363  return;
364  }
365  }
366 }
367 
369  const symex_target_equationt &target,
370  symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
371  const prop_convt &prop_conv,
372  const namespacet &ns,
373  goto_tracet &goto_trace)
374 {
375  const auto is_last_step_to_keep = [last_step_to_keep](
376  symex_target_equationt::SSA_stepst::const_iterator it, const prop_convt &) {
377  return last_step_to_keep == it;
378  };
379 
380  return build_goto_trace(
381  target, is_last_step_to_keep, prop_conv, ns, goto_trace);
382 }
383 
385  symex_target_equationt::SSA_stepst::const_iterator step,
386  const prop_convt &prop_conv)
387 {
388  return step->is_assert() && prop_conv.l_get(step->cond_literal).is_false();
389 }
390 
392  const symex_target_equationt &target,
393  const prop_convt &prop_conv,
394  const namespacet &ns,
395  goto_tracet &goto_trace)
396 {
397  build_goto_trace(target, is_failed_assertion_step, prop_conv, ns, goto_trace);
398 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
bool is_false() const
Definition: threeval.h:26
exprt & true_case()
Definition: std_expr.h:3393
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
bool is_not_nil() const
Definition: irep.h:173
exprt & op0()
Definition: expr.h:72
exprt lhs_object_value
Definition: goto_trace.h:114
io_argst io_args
Definition: goto_trace.h:119
const exprt & op() const
Definition: std_expr.h:340
static bool is_failed_assertion_step(symex_target_equationt::SSA_stepst::const_iterator step, const prop_convt &prop_conv)
virtual exprt get(const exprt &expr) const =0
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)> ssa_step_predicatet
The trinary if-then-else operator.
Definition: std_expr.h:3359
std::size_t step_nr
Definition: goto_trace.h:39
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
TO_BE_DOCUMENTED.
Definition: goto_trace.h:36
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
stepst steps
Definition: goto_trace.h:156
goto_programt::const_targett pc
Definition: goto_trace.h:95
Add constraints to equation encoding partial orders on events.
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
Extract member of struct or union.
Definition: std_expr.h:3869
irep_idt io_id
Definition: goto_trace.h:117
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
const irep_idt & id() const
Definition: irep.h:259
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
Definition: threeval.h:19
unsigned thread_nr
Definition: goto_trace.h:98
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
const irep_idt get_original_name() const
Definition: ssa_expr.h:77
#define forall_operands(it, expr)
Definition: expr.h:17
irep_idt identifier
Definition: goto_trace.h:123
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
exprt & false_case()
Definition: std_expr.h:3403
bool is_true() const
Definition: threeval.h:25
typet type
Type of symbol.
Definition: symbol.h:34
virtual tvt l_get(literalt a) const =0
static irep_idt entry_point()
exprt & index()
Definition: std_expr.h:1496
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3909
ssa_exprt lhs_object
Definition: goto_trace.h:108
exprt full_lhs_value
Definition: goto_trace.h:114
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
std::string comment
Definition: goto_trace.h:105
void make_nil()
Definition: irep.h:315
void update_internal_field(const symex_target_equationt::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...
exprt build_full_lhs_rec(const prop_convt &prop_conv, const namespacet &ns, const exprt &src_original, const exprt &src_ssa)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
TO_BE_DOCUMENTED.
Definition: goto_trace.h:152
irep_idt format_string
Definition: goto_trace.h:117
operandst & operands()
Definition: expr.h:66
exprt & array()
Definition: std_expr.h:1486
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
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.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
Traces of GOTO Programs.
bool simplify(exprt &expr, const namespacet &ns)
assignment_typet assignment_type
Definition: goto_trace.h:93
array index operator
Definition: std_expr.h:1462