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 
105  const prop_convt &prop_conv,
106  const namespacet &ns,
107  const exprt &src)
108 {
109  return nil_exprt();
110 }
111 
115  const exprt &expr,
116  goto_trace_stept &goto_trace_step,
117  const namespacet &ns)
118 {
119  if(expr.id()==ID_symbol)
120  {
121  const irep_idt &id=to_ssa_expr(expr).get_original_name();
122  const symbolt *symbol;
123  if(!ns.lookup(id, symbol))
124  {
125  bool result=symbol->type.get_bool("#dynamic");
126  if(result)
127  goto_trace_step.internal=true;
128  }
129  }
130  else
131  {
132  forall_operands(it, expr)
133  set_internal_dynamic_object(*it, goto_trace_step, ns);
134  }
135 }
136 
140  const symex_target_equationt::SSA_stept &SSA_step,
141  goto_trace_stept &goto_trace_step,
142  const namespacet &ns)
143 {
144  // set internal for dynamic_object in both lhs and rhs expressions
145  set_internal_dynamic_object(SSA_step.ssa_lhs, goto_trace_step, ns);
146  set_internal_dynamic_object(SSA_step.ssa_rhs, goto_trace_step, ns);
147 
148  // set internal field to CPROVER functions (e.g., __CPROVER_initialize)
149  if(SSA_step.is_function_call())
150  {
151  if(SSA_step.source.pc->source_location.as_string().empty())
152  goto_trace_step.internal=true;
153  }
154 
155  // set internal field to input and output steps
156  if(goto_trace_step.type==goto_trace_stept::typet::OUTPUT ||
157  goto_trace_step.type==goto_trace_stept::typet::INPUT)
158  {
159  goto_trace_step.internal=true;
160  }
161 
162  // set internal field to _start function-return step
163  if(SSA_step.source.pc->function==goto_functionst::entry_point())
164  {
165  // "__CPROVER_*" function calls in __CPROVER_start are already marked as
166  // internal. Don't mark any other function calls (i.e. "main"), function
167  // arguments or any other parts of a code_function_callt as internal.
168  if(SSA_step.source.pc->code.get_statement()!=ID_function_call)
169  goto_trace_step.internal=true;
170  }
171 }
172 
174  const symex_target_equationt &target,
175  symex_target_equationt::SSA_stepst::const_iterator end_step,
176  const prop_convt &prop_conv,
177  const namespacet &ns,
178  goto_tracet &goto_trace)
179 {
180  // We need to re-sort the steps according to their clock.
181  // Furthermore, read-events need to occur before write
182  // events with the same clock.
183 
184  typedef std::map<mp_integer, goto_tracet::stepst> time_mapt;
185  time_mapt time_map;
186 
187  mp_integer current_time=0;
188 
189  const goto_trace_stept *end_ptr=nullptr;
190  bool end_step_seen=false;
191 
192  for(symex_target_equationt::SSA_stepst::const_iterator
193  it=target.SSA_steps.begin();
194  it!=target.SSA_steps.end();
195  it++)
196  {
197  if(it==end_step)
198  end_step_seen=true;
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  to_integer(clock_value, current_time);
229  }
230  else if(it->is_atomic_end() && current_time<0)
231  current_time*=-1;
232 
233  assert(current_time>=0);
234  // move any steps gathered in an atomic section
235 
236  if(time_before<0)
237  {
238  time_mapt::iterator entry=
239  time_map.insert(std::make_pair(
240  current_time,
241  goto_tracet::stepst())).first;
242  entry->second.splice(entry->second.end(), time_map[time_before]);
243  time_map.erase(time_before);
244  }
245 
246  continue;
247  }
248 
249  // drop PHI and GUARD assignments altogether
250  if(it->is_assignment() &&
251  (SSA_step.assignment_type==
253  SSA_step.assignment_type==
255  {
256  continue;
257  }
258 
259  goto_tracet::stepst &steps=time_map[current_time];
260  steps.push_back(goto_trace_stept());
261  goto_trace_stept &goto_trace_step=steps.back();
262  if(!end_step_seen)
263  end_ptr=&goto_trace_step;
264 
265  goto_trace_step.thread_nr=SSA_step.source.thread_nr;
266  goto_trace_step.pc=SSA_step.source.pc;
267  goto_trace_step.comment=SSA_step.comment;
268  if(SSA_step.ssa_lhs.is_not_nil())
269  goto_trace_step.lhs_object=
270  ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
271  else
272  goto_trace_step.lhs_object.make_nil();
273  goto_trace_step.type=SSA_step.type;
274  goto_trace_step.hidden=SSA_step.hidden;
275  goto_trace_step.format_string=SSA_step.format_string;
276  goto_trace_step.io_id=SSA_step.io_id;
277  goto_trace_step.formatted=SSA_step.formatted;
278  goto_trace_step.identifier=SSA_step.identifier;
279 
280  // update internal field for specific variables in the counterexample
281  update_internal_field(SSA_step, goto_trace_step, ns);
282 
283  goto_trace_step.assignment_type=
284  (it->is_assignment()&&
285  (SSA_step.assignment_type==
287  SSA_step.assignment_type==
291 
292  if(SSA_step.original_full_lhs.is_not_nil())
293  goto_trace_step.full_lhs=
295  prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
296 
297  if(SSA_step.ssa_lhs.is_not_nil())
298  goto_trace_step.lhs_object_value=prop_conv.get(SSA_step.ssa_lhs);
299 
300  if(SSA_step.ssa_full_lhs.is_not_nil())
301  {
302  goto_trace_step.full_lhs_value=prop_conv.get(SSA_step.ssa_full_lhs);
303  simplify(goto_trace_step.full_lhs_value, ns);
304  }
305 
306  for(const auto &j : SSA_step.converted_io_args)
307  {
308  if(j.is_constant() ||
309  j.id()==ID_string_constant)
310  goto_trace_step.io_args.push_back(j);
311  else
312  {
313  exprt tmp=prop_conv.get(j);
314  goto_trace_step.io_args.push_back(tmp);
315  }
316  }
317 
318  if(SSA_step.is_assert() ||
319  SSA_step.is_assume() ||
320  SSA_step.is_goto())
321  {
322  goto_trace_step.cond_expr=SSA_step.cond_expr;
323 
324  goto_trace_step.cond_value=
325  prop_conv.l_get(SSA_step.cond_literal).is_true();
326  }
327  }
328 
329  // Now assemble into a single goto_trace.
330  // This exploits sorted-ness of the map.
331  for(auto &t_it : time_map)
332  goto_trace.steps.splice(goto_trace.steps.end(), t_it.second);
333 
334  // cut off the trace at the desired end
335  for(goto_tracet::stepst::iterator
336  s_it1=goto_trace.steps.begin();
337  s_it1!=goto_trace.steps.end();
338  ++s_it1)
339  if(end_step_seen && end_ptr==&(*s_it1))
340  {
341  goto_trace.trim_after(s_it1);
342  break;
343  }
344 
345  // produce the step numbers
346  unsigned step_nr=0;
347 
348  for(auto &s_it : goto_trace.steps)
349  s_it.step_nr=++step_nr;
350 }
351 
353  const symex_target_equationt &target,
354  const prop_convt &prop_conv,
355  const namespacet &ns,
356  goto_tracet &goto_trace)
357 {
359  target, target.SSA_steps.end(), prop_conv, ns, goto_trace);
360 
361  // Now delete anything after first failed assertion
362  for(goto_tracet::stepst::iterator
363  s_it1=goto_trace.steps.begin();
364  s_it1!=goto_trace.steps.end();
365  s_it1++)
366  if(s_it1->is_assert() && !s_it1->cond_value)
367  {
368  goto_trace.trim_after(s_it1);
369  break;
370  }
371 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
exprt & true_case()
Definition: std_expr.h:3395
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
bool is_not_nil() const
Definition: irep.h:103
void trim_after(stepst::iterator s)
Definition: goto_trace.h:191
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
exprt adjust_lhs_object(const prop_convt &prop_conv, const namespacet &ns, const exprt &src)
std::list< goto_trace_stept > stepst
Definition: goto_trace.h:155
virtual exprt get(const exprt &expr) const =0
The trinary if-then-else operator.
Definition: std_expr.h:3361
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.
Extract member of struct or union.
Definition: std_expr.h:3871
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:189
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
The NIL expression.
Definition: std_expr.h:4510
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:3955
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
exprt & false_case()
Definition: std_expr.h:3405
bool is_true() const
Definition: threeval.h:25
void build_goto_trace(const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator end_step, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
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:3911
ssa_exprt lhs_object
Definition: goto_trace.h:108
exprt full_lhs_value
Definition: goto_trace.h:114
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
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:243
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:130
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