cprover
build_goto_trace.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Build Goto Trace from State History
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "build_goto_trace.h"
13 
16  const path_symex_statet &state,
17  const decision_proceduret &decision_procedure,
18  goto_tracet &goto_trace)
19 {
20  // follow the history in the state,
21  // but in a forwards-fashion
22 
23  std::vector<path_symex_step_reft> steps;
24  state.history.build_history(steps);
25 
26  unsigned step_nr;
27 
28  for(step_nr=0; step_nr<steps.size(); step_nr++)
29  {
30  const path_symex_stept &step=*steps[step_nr];
31 
32  goto_trace_stept trace_step;
33 
34  assert(!step.pc.is_nil());
35  trace_step.pc=state.locs[step.pc].target;
36  trace_step.thread_nr=step.thread_nr;
37  trace_step.step_nr=step_nr;
38 
39  const goto_programt::instructiont &instruction=*trace_step.pc;
40 
41  switch(instruction.type)
42  {
43  case ASSIGN:
45  trace_step.full_lhs=step.full_lhs;
46  trace_step.full_lhs_value=decision_procedure.get(step.ssa_lhs);
47  break;
48 
49  case DECL:
51  trace_step.full_lhs=step.full_lhs;
52  trace_step.lhs_object=ssa_exprt(step.full_lhs);
53  trace_step.full_lhs_value=decision_procedure.get(step.ssa_lhs);
54  break;
55 
56  case DEAD:
58  break;
59 
60  case ASSUME:
62  break;
63 
64  case FUNCTION_CALL:
66  break;
67 
68  case END_FUNCTION:
70  break;
71 
72  case START_THREAD:
74  break;
75 
76  case ATOMIC_BEGIN:
78  break;
79 
80  case ATOMIC_END:
82  break;
83 
84  default:
86  }
87 
88  goto_trace.add_step(trace_step);
89  }
90 
91  // add assertion
92  const goto_programt::instructiont &instruction=
93  *state.get_instruction();
94 
95  assert(instruction.is_assert());
96 
97  {
98  goto_trace_stept trace_step;
99 
100  trace_step.pc=state.get_instruction();
101  trace_step.thread_nr=state.get_current_thread();
102  trace_step.step_nr=step_nr;
104 
105  const irep_idt &comment=
106  instruction.source_location.get_comment();
107 
108  if(!comment.empty())
109  trace_step.comment=id2string(comment);
110  else
111  trace_step.comment="assertion";
112 
113  goto_trace.add_step(trace_step);
114  }
115 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void build_history(std::vector< path_symex_step_reft > &dest) const
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:115
unsigned step_nr
Definition: goto_trace.h:37
virtual exprt get(const exprt &expr) const =0
bool is_nil() const
Definition: loc_ref.h:39
TO_BE_DOCUMENTED.
Definition: goto_trace.h:34
goto_programt::const_targett pc
Definition: goto_trace.h:90
void add_step(const goto_trace_stept &step)
Definition: goto_trace.h:172
const locst & locs
Build Goto Trace from Path Symex History.
unsigned thread_nr
Definition: goto_trace.h:93
unsigned get_current_thread() const
goto_programt::const_targett get_instruction() const
ssa_exprt lhs_object
Definition: goto_trace.h:103
exprt full_lhs_value
Definition: goto_trace.h:109
std::string comment
Definition: goto_trace.h:100
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
path_symex_step_reft history
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)