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