cprover
path_symex_state.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: State of path-based symbolic simulator
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "path_symex_state.h"
13 
14 #include <util/simplify_expr.h>
15 #include <util/arith_tools.h>
17 
18 #include <util/c_types.h>
19 
21 
23 
24 #ifdef DEBUG
25 #include <iostream>
26 #include <langapi/language_util.h>
27 #endif
28 
30  var_mapt &var_map,
31  const locst &locs,
32  path_symex_historyt &path_symex_history)
33 {
34  path_symex_statet s(var_map, locs, path_symex_history);
35 
36  // create one new thread
38  thread.pc=locs.entry_loc; // set its PC
39  s.set_current_thread(0);
40 
41  return s;
42 }
43 
44 void path_symex_statet::output(const threadt &thread, std::ostream &out) const
45 {
46  out << " PC: " << thread.pc << '\n';
47  out << " Call stack:";
48  for(call_stackt::const_iterator
49  it=thread.call_stack.begin();
50  it!=thread.call_stack.end();
51  it++)
52  out << " " << it->return_location << '\n';
53  out << '\n';
54 }
55 
56 void path_symex_statet::output(std::ostream &out) const
57 {
58  for(unsigned t=0; t<threads.size(); t++)
59  {
60  out << "*** Thread " << t << '\n';
61  output(threads[t], out);
62  out << '\n';
63  }
64 }
65 
67  const var_mapt::var_infot &var_info)
68 {
69  assert(current_thread<threads.size());
70 
71  var_valt &var_val=
72  var_info.is_shared()?shared_vars:threads[current_thread].local_vars;
73  if(var_val.size()<=var_info.number)
74  var_val.resize(var_info.number+1);
75  return var_val[var_info.number];
76 }
77 
79 {
80  // is there a context switch happening?
81  if(!history.is_nil() &&
84 
85  // update our statistics
86  depth++;
87 
88  if(get_instruction()->is_goto())
89  no_branches++;
90 
91  // add the step
93  stept &step=*history;
94 
95  // copy PC
96  assert(current_thread<threads.size());
97  step.pc=threads[current_thread].pc;
99 }
100 
102  decision_proceduret &decision_procedure) const
103 {
104  // feed path constraint to decision procedure
105  decision_procedure << history;
106 
107  // check whether SAT
108  switch(decision_procedure())
109  {
111 
113 
115  throw "error from decision procedure";
116  }
117 
118  return true; // not really reachable
119 }
120 
122  decision_proceduret &decision_procedure)
123 {
124  const goto_programt::instructiont &instruction=*get_instruction();
125 
126  // assert that this is an assertion
127  assert(instruction.is_assert());
128 
129  // the assertion in SSA
130  exprt assertion=read(instruction.guard);
131 
132  // trivial?
133  if(assertion.is_true())
134  return true; // no error
135 
136  // the path constraint
137  decision_procedure << history;
138 
139  // negate the assertion
140  decision_procedure.set_to(assertion, false);
141 
142  // check whether SAT
143  switch(decision_procedure.dec_solve())
144  {
146  return false; // error
147 
149  return true; // no error
150 
151  default:
152  throw "error from decision procedure";
153  }
154 
155  return true; // not really reachable
156 }
Symbolic Execution.
loc_reft entry_loc
Definition: locs.h:44
Decision Procedure Interface.
unsigned no_thread_interleavings
virtual resultt dec_solve()=0
exprt read(const exprt &src)
threadt & add_thread()
std::vector< var_statet > var_valt
bool is_feasible(class decision_proceduret &) const
var_statet & get_var_state(const var_mapt::var_infot &var_info)
virtual void set_to(const exprt &expr, bool value)=0
unsigned number
Definition: var_map.h:45
bool check_assertion(class decision_proceduret &)
goto_programt::const_targett get_instruction() const
State of path-based symbolic simulator.
Definition: locs.h:39
Base class for all expressions.
Definition: expr.h:46
bool is_shared() const
Definition: var_map.h:39
path_symex_statet initial_state(var_mapt &var_map, const locst &locs, path_symex_historyt &path_symex_history)
void set_current_thread(unsigned _thread)
Pointer Dereferencing.
path_symex_step_reft history
void output(std::ostream &out) const