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 
14 #include <util/find_symbols.h>
15 
17 
18 #include "goto_symex_state.h"
19 
21 {
22 public:
24  const namespacet &_ns,
25  value_setst &_value_sets,
26  const goto_programt::const_targett _target,
27  const symex_target_equationt::SSA_stept &_SSA_step,
28  const goto_symex_statet &_s):
29  ns(_ns),
30  value_sets(_value_sets),
31  target(_target),
32  SSA_step(_SSA_step),
33  s(_s)
34  {
35  }
36 
37 protected:
38  const namespacet &ns;
43  void compute_rec(exprt &dest);
44 
45 public:
46  void compute(exprt &dest);
47 
48 protected:
49  void compute_address_of(exprt &dest);
50 };
51 
53  const namespacet &ns,
54  value_setst &value_sets,
55  const goto_programt::const_targett target,
56  const symex_target_equationt &equation,
57  const goto_symex_statet &s,
58  exprt &dest)
59 {
60  for(symex_target_equationt::SSA_stepst::const_reverse_iterator
61  it=equation.SSA_steps.rbegin();
62  it!=equation.SSA_steps.rend();
63  it++)
64  {
65  preconditiont precondition(ns, value_sets, target, *it, s);
66  precondition.compute(dest);
67  if(dest.is_false())
68  return;
69  }
70 }
71 
73 {
74  if(dest.id()==ID_symbol)
75  {
76  // leave alone
77  }
78  else if(dest.id()==ID_index)
79  {
80  assert(dest.operands().size()==2);
81  compute_address_of(dest.op0());
82  compute(dest.op1());
83  }
84  else if(dest.id()==ID_member)
85  {
86  assert(dest.operands().size()==1);
87  compute_address_of(dest.op0());
88  }
89  else if(dest.id()==ID_dereference)
90  {
91  assert(dest.operands().size()==1);
92  compute(dest.op0());
93  }
94 }
95 
97 {
98  compute_rec(dest);
99 }
100 
102 {
103  if(dest.id()==ID_address_of)
104  {
105  // only do index!
106  assert(dest.operands().size()==1);
107  compute_address_of(dest.op0());
108  }
109  else if(dest.id()==ID_dereference)
110  {
111  assert(dest.operands().size()==1);
112 
113  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
114 
115  // aliasing may happen here
116 
117  value_setst::valuest expr_set;
118  value_sets.get_values(target, dest.op0(), expr_set);
119  std::unordered_set<irep_idt, irep_id_hash> symbols;
120 
121  for(value_setst::valuest::const_iterator
122  it=expr_set.begin();
123  it!=expr_set.end();
124  it++)
125  find_symbols(*it, symbols);
126 
127  if(symbols.find(lhs_identifier)!=symbols.end())
128  {
129  // may alias!
130  exprt tmp;
131  tmp.swap(dest.op0());
133  dest.swap(tmp);
134  compute_rec(dest);
135  }
136  else
137  {
138  // nah, ok
139  compute_rec(dest.op0());
140  }
141  }
142  else if(dest==SSA_step.ssa_lhs.get_original_expr())
143  {
144  dest=SSA_step.ssa_rhs;
145  s.get_original_name(dest);
146  }
147  else
148  Forall_operands(it, dest)
149  compute_rec(*it);
150 }
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:84
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:140
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
instructionst::const_iterator const_targett
exprt dereference(const exprt &pointer, const namespacet &ns)
Definition: dereference.h:88
void compute(exprt &dest)
exprt & op1()
Definition: expr.h:87
TO_BE_DOCUMENTED.
Definition: namespace.h:62
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:46
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:70
std::list< exprt > valuest
Definition: value_sets.h:28
void find_symbols(const exprt &src, find_symbols_sett &dest)
Generate Equation using Symbolic Execution.