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 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  auto &index_expr = to_index_expr(dest);
82  compute_address_of(index_expr.array());
83  compute(index_expr.index());
84  }
85  else if(dest.id()==ID_member)
86  {
87  compute_address_of(to_member_expr(dest).compound());
88  }
89  else if(dest.id()==ID_dereference)
90  {
91  compute(to_dereference_expr(dest).pointer());
92  }
93 }
94 
96 {
97  compute_rec(dest);
98 }
99 
101 {
102  if(dest.id()==ID_address_of)
103  {
104  // only do index!
105  compute_address_of(to_address_of_expr(dest).object());
106  }
107  else if(dest.id()==ID_dereference)
108  {
109  auto &deref_expr = to_dereference_expr(dest);
110 
111  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
112 
113  // aliasing may happen here
114 
115  const std::vector<exprt> expr_set = value_sets.get_values(
116  SSA_step.source.function_id, target, deref_expr.pointer());
117  const std::unordered_set<irep_idt> symbols =
118  find_symbols_or_nexts(expr_set.begin(), expr_set.end());
119 
120  if(symbols.find(lhs_identifier)!=symbols.end())
121  {
122  // may alias!
123  exprt tmp;
124  tmp.swap(deref_expr.pointer());
126  deref_expr.swap(tmp);
127  compute_rec(deref_expr);
128  }
129  else
130  {
131  // nah, ok
132  compute_rec(deref_expr.pointer());
133  }
134  }
135  else if(dest==SSA_step.ssa_lhs.get_original_expr())
136  {
138  }
139  else
140  Forall_operands(it, dest)
141  compute_rec(*it);
142 }
Single SSA step in the equation.
Definition: ssa_step.h:45
exprt ssa_rhs
Definition: ssa_step.h:143
symex_targett::sourcet source
Definition: ssa_step.h:47
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
instructionst::const_iterator const_targett
Definition: goto_program.h:551
Central data structure: state.
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:452
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
value_setst & value_sets
const goto_programt::const_targett target
const namespacet & ns
void compute_address_of(exprt &dest)
void compute_rec(exprt &dest)
const SSA_stept & SSA_step
preconditiont(const namespacet &_ns, value_setst &_value_sets, const goto_programt::const_targett _target, const SSA_stept &_SSA_step, const goto_symex_statet &_s)
const goto_symex_statet & s
void compute(exprt &dest)
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
irep_idt get_object_name() const
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual std::vector< exprt > get_values(const irep_idt &function_id, goto_programt::const_targett l, const exprt &expr)=0
#define Forall_operands(it, expr)
Definition: expr.h:25
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
Symbol Table + CFG.
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
Symbolic Execution.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
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)
Generate Equation using Symbolic Execution.
exprt get_original_name(exprt expr)
Undo all levels of renaming.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297