cprover
precondition.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "precondition.h"
13 #include "goto_symex_state.h"
14 
15 #include <util/find_symbols.h>
16 
18 
20 
22 {
23 public:
25  const namespacet &_ns,
26  value_setst &_value_sets,
27  const goto_programt::const_targett _target,
28  const symex_target_equationt::SSA_stept &_SSA_step,
29  const goto_symex_statet &_s):
30  ns(_ns),
31  value_sets(_value_sets),
32  target(_target),
33  SSA_step(_SSA_step),
34  s(_s)
35  {
36  }
37 
38 protected:
39  const namespacet &ns;
44  void compute_rec(exprt &dest);
45 
46 public:
47  void compute(exprt &dest);
48 
49 protected:
50  void compute_address_of(exprt &dest);
51 };
52 
54  const namespacet &ns,
55  value_setst &value_sets,
56  const goto_programt::const_targett target,
57  const symex_target_equationt &equation,
58  const goto_symex_statet &s,
59  exprt &dest)
60 {
61  for(symex_target_equationt::SSA_stepst::const_reverse_iterator
62  it=equation.SSA_steps.rbegin();
63  it!=equation.SSA_steps.rend();
64  it++)
65  {
66  preconditiont precondition(ns, value_sets, target, *it, s);
67  precondition.compute(dest);
68  if(dest.is_false())
69  return;
70  }
71 }
72 
74 {
75  if(dest.id()==ID_symbol)
76  {
77  // leave alone
78  }
79  else if(dest.id()==ID_index)
80  {
81  assert(dest.operands().size()==2);
82  compute_address_of(dest.op0());
83  compute(dest.op1());
84  }
85  else if(dest.id()==ID_member)
86  {
87  assert(dest.operands().size()==1);
88  compute_address_of(dest.op0());
89  }
90  else if(dest.id()==ID_dereference)
91  {
92  assert(dest.operands().size()==1);
93  compute(dest.op0());
94  }
95 }
96 
98 {
99  compute_rec(dest);
100 }
101 
103 {
104  if(dest.id()==ID_address_of)
105  {
106  // only do index!
107  assert(dest.operands().size()==1);
108  compute_address_of(dest.op0());
109  }
110  else if(dest.id()==ID_dereference)
111  {
112  assert(dest.operands().size()==1);
113 
114  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
115 
116  // aliasing may happen here
117 
118  value_setst::valuest expr_set;
119  value_sets.get_values(target, dest.op0(), expr_set);
120  std::unordered_set<irep_idt> symbols;
121 
122  for(value_setst::valuest::const_iterator
123  it=expr_set.begin();
124  it!=expr_set.end();
125  it++)
126  find_symbols(*it, symbols);
127 
128  if(symbols.find(lhs_identifier)!=symbols.end())
129  {
130  // may alias!
131  exprt tmp;
132  tmp.swap(dest.op0());
134  dest.swap(tmp);
135  compute_rec(dest);
136  }
137  else
138  {
139  // nah, ok
140  compute_rec(dest.op0());
141  }
142  }
143  else if(dest==SSA_step.ssa_lhs.get_original_expr())
144  {
145  dest=SSA_step.ssa_rhs;
146  s.get_original_name(dest);
147  }
148  else
149  Forall_operands(it, dest)
150  compute_rec(*it);
151 }
void precondition(const namespacet &ns, value_setst &value_sets, const goto_programt::const_targett target, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
virtual void get_values(goto_programt::const_targett l, const exprt &expr, valuest &dest)=0
exprt & op0()
Definition: expr.h:72
value_setst & value_sets
preconditiont(const namespacet &_ns, value_setst &_value_sets, const goto_programt::const_targett _target, const symex_target_equationt::SSA_stept &_SSA_step, const goto_symex_statet &_s)
bool is_false() const
Definition: expr.cpp:131
Symbolic Execution.
const symex_target_equationt::SSA_stept & SSA_step
void compute_rec(exprt &dest)
void get_original_name(exprt &expr) const
const irep_idt & id() const
Definition: irep.h:189
Symbol Table + CFG.
exprt dereference(const exprt &pointer, const namespacet &ns)
Definition: dereference.h:88
void compute(exprt &dest)
exprt & op1()
Definition: expr.h:75
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const namespacet & ns
const goto_programt::const_targett target
const goto_symex_statet & s
void compute_address_of(exprt &dest)
Base class for all expressions.
Definition: expr.h:42
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
operandst & operands()
Definition: expr.h:66
std::list< exprt > valuest
Definition: value_sets.h:28
void find_symbols(const exprt &src, find_symbols_sett &dest)
Generate Equation using Symbolic Execution.