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 
113  const symex_target_equationt &target,
114  symex_target_equationt::SSA_stepst::const_iterator end_step,
115  const prop_convt &prop_conv,
116  const namespacet &ns,
117  goto_tracet &goto_trace)
118 {
119  // We need to re-sort the steps according to their clock.
120  // Furthermore, read-events need to occur before write
121  // events with the same clock.
122 
123  typedef std::map<mp_integer, goto_tracet::stepst> time_mapt;
124  time_mapt time_map;
125 
127 
128  const goto_trace_stept *end_ptr=nullptr;
129  bool end_step_seen=false;
130 
131  for(symex_target_equationt::SSA_stepst::const_iterator
132  it=target.SSA_steps.begin();
133  it!=target.SSA_steps.end();
134  it++)
135  {
136  if(it==end_step)
137  end_step_seen=true;
138 
139  const symex_target_equationt::SSA_stept &SSA_step=*it;
140 
141  if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
142  continue;
143 
144  if(it->is_constraint() ||
145  it->is_spawn())
146  continue;
147  else if(it->is_atomic_begin())
148  {
149  // for atomic sections the timing can only be determined once we see
150  // a shared read or write (if there is none, the time will be
151  // reverted to the time before entering the atomic section); we thus
152  // use a temporary negative time slot to gather all events
153  current_time*=-1;
154  continue;
155  }
156  else if(it->is_shared_read() || it->is_shared_write() ||
157  it->is_atomic_end())
158  {
159  mp_integer time_before=current_time;
160 
161  if(it->is_shared_read() || it->is_shared_write())
162  {
163  // these are just used to get the time stamp
164  exprt clock_value=prop_conv.get(
166 
167  to_integer(clock_value, current_time);
168  }
169  else if(it->is_atomic_end() && current_time<0)
170  current_time*=-1;
171 
172  assert(current_time>=0);
173  // move any steps gathered in an atomic section
174 
175  if(time_before<0)
176  {
177  time_mapt::iterator entry=
178  time_map.insert(std::make_pair(
179  current_time,
180  goto_tracet::stepst())).first;
181  entry->second.splice(entry->second.end(), time_map[time_before]);
182  time_map.erase(time_before);
183  }
184 
185  continue;
186  }
187 
188  // drop PHI and GUARD assignments altogether
189  if(it->is_assignment() &&
190  (SSA_step.assignment_type==
192  SSA_step.assignment_type==
194  {
195  continue;
196  }
197 
198  goto_tracet::stepst &steps=time_map[current_time];
199  steps.push_back(goto_trace_stept());
200  goto_trace_stept &goto_trace_step=steps.back();
201  if(!end_step_seen)
202  end_ptr=&goto_trace_step;
203 
204  goto_trace_step.thread_nr=SSA_step.source.thread_nr;
205  goto_trace_step.pc=SSA_step.source.pc;
206  goto_trace_step.comment=SSA_step.comment;
207  if(SSA_step.ssa_lhs.is_not_nil())
208  goto_trace_step.lhs_object=
209  ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
210  else
211  goto_trace_step.lhs_object.make_nil();
212  goto_trace_step.type=SSA_step.type;
213  goto_trace_step.hidden=SSA_step.hidden;
214  goto_trace_step.format_string=SSA_step.format_string;
215  goto_trace_step.io_id=SSA_step.io_id;
216  goto_trace_step.formatted=SSA_step.formatted;
217  goto_trace_step.identifier=SSA_step.identifier;
218 
219  goto_trace_step.assignment_type=
220  (it->is_assignment()&&
221  (SSA_step.assignment_type==
223  SSA_step.assignment_type==
227 
228  if(SSA_step.original_full_lhs.is_not_nil())
229  goto_trace_step.full_lhs=
231  prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
232 
233  if(SSA_step.ssa_lhs.is_not_nil())
234  goto_trace_step.lhs_object_value=prop_conv.get(SSA_step.ssa_lhs);
235 
236  if(SSA_step.ssa_full_lhs.is_not_nil())
237  {
238  goto_trace_step.full_lhs_value=prop_conv.get(SSA_step.ssa_full_lhs);
239  simplify(goto_trace_step.full_lhs_value, ns);
240  }
241 
242  for(const auto &j : SSA_step.converted_io_args)
243  {
244  if(j.is_constant() ||
245  j.id()==ID_string_constant)
246  goto_trace_step.io_args.push_back(j);
247  else
248  {
249  exprt tmp=prop_conv.get(j);
250  goto_trace_step.io_args.push_back(tmp);
251  }
252  }
253 
254  if(SSA_step.is_assert() ||
255  SSA_step.is_assume() ||
256  SSA_step.is_goto())
257  {
258  goto_trace_step.cond_expr=SSA_step.cond_expr;
259 
260  goto_trace_step.cond_value=
261  prop_conv.l_get(SSA_step.cond_literal).is_true();
262  }
263  }
264 
265  // Now assemble into a single goto_trace.
266  // This exploits sorted-ness of the map.
267  for(auto &t_it : time_map)
268  goto_trace.steps.splice(goto_trace.steps.end(), t_it.second);
269 
270  // cut off the trace at the desired end
271  for(goto_tracet::stepst::iterator
272  s_it1=goto_trace.steps.begin();
273  s_it1!=goto_trace.steps.end();
274  ++s_it1)
275  if(end_step_seen && end_ptr==&(*s_it1))
276  {
277  goto_trace.trim_after(s_it1);
278  break;
279  }
280 
281  // produce the step numbers
282  unsigned step_nr=0;
283 
284  for(auto &s_it : goto_trace.steps)
285  s_it.step_nr=++step_nr;
286 }
287 
289  const symex_target_equationt &target,
290  const prop_convt &prop_conv,
291  const namespacet &ns,
292  goto_tracet &goto_trace)
293 {
295  target, target.SSA_steps.end(), prop_conv, ns, goto_trace);
296 
297  // Now delete anything after first failed assertion
298  for(goto_tracet::stepst::iterator
299  s_it1=goto_trace.steps.begin();
300  s_it1!=goto_trace.steps.end();
301  s_it1++)
302  if(s_it1->is_assert() && !s_it1->cond_value)
303  {
304  goto_trace.trim_after(s_it1);
305  break;
306  }
307 }
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
exprt & true_case()
Definition: std_expr.h:2805
semantic type conversion
Definition: std_expr.h:1725
BigInt mp_integer
Definition: mp_arith.h:19
bool is_not_nil() const
Definition: irep.h:104
void trim_after(stepst::iterator s)
Definition: goto_trace.h:178
exprt & op0()
Definition: expr.h:84
exprt lhs_object_value
Definition: goto_trace.h:109
io_argst io_args
Definition: goto_trace.h:114
std::list< goto_trace_stept > stepst
Definition: goto_trace.h:149
virtual exprt get(const exprt &expr) const =0
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
The trinary if-then-else operator.
Definition: std_expr.h:2771
TO_BE_DOCUMENTED.
Definition: goto_trace.h:34
stepst steps
Definition: goto_trace.h:150
exprt & op()
Definition: std_expr.h:1739
goto_programt::const_targett pc
Definition: goto_trace.h:90
Add constraints to equation encoding partial orders on events.
Extract member of struct or union.
Definition: std_expr.h:3214
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
irep_idt io_id
Definition: goto_trace.h:112
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
const irep_idt & id() const
Definition: irep.h:189
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
The NIL expression.
Definition: std_expr.h:3764
Definition: threeval.h:19
unsigned thread_nr
Definition: goto_trace.h:93
TO_BE_DOCUMENTED.
Definition: namespace.h:62
exprt adjust_lhs_object(const prop_convt &prop_conv, const namespacet &ns, const exprt &src)
irep_idt identifier
Definition: goto_trace.h:118
exprt & false_case()
Definition: std_expr.h:2815
bool is_true() const
Definition: threeval.h:25
virtual tvt l_get(literalt a) const =0
absolute_timet current_time()
exprt build_full_lhs_rec(const prop_convt &prop_conv, const namespacet &ns, const exprt &src_original, const exprt &src_ssa)
exprt & index()
Definition: std_expr.h:1208
Base class for all expressions.
Definition: expr.h:46
const exprt & struct_op() const
Definition: std_expr.h:3270
ssa_exprt lhs_object
Definition: goto_trace.h:103
exprt full_lhs_value
Definition: goto_trace.h:109
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
std::string comment
Definition: goto_trace.h:100
Traces of GOTO Programs.
void make_nil()
Definition: irep.h:243
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
irep_idt format_string
Definition: goto_trace.h:112
operandst & operands()
Definition: expr.h:70
exprt & array()
Definition: std_expr.h:1198
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
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)
bool simplify(exprt &expr, const namespacet &ns)
assignment_typet assignment_type
Definition: goto_trace.h:88
array index operator
Definition: std_expr.h:1170