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 #include <util/pointer_expr.h>
16 
18 
19 #include "renaming_level.h"
20 #include "symex_target_equation.h"
21 
23 {
24 public:
26  const namespacet &_ns,
27  value_setst &_value_sets,
28  const goto_programt::const_targett _target,
29  const SSA_stept &_SSA_step,
30  const goto_symex_statet &_s)
31  : ns(_ns),
32  value_sets(_value_sets),
33  target(_target),
34  SSA_step(_SSA_step),
35  s(_s)
36  {
37  }
38 
39 protected:
40  const namespacet &ns;
45  void compute_rec(exprt &dest);
46 
47 public:
48  void compute(exprt &dest);
49 
50 protected:
51  void compute_address_of(exprt &dest);
52 };
53 
55  const namespacet &ns,
56  value_setst &value_sets,
57  const goto_programt::const_targett target,
58  const symex_target_equationt &equation,
59  const goto_symex_statet &s,
60  exprt &dest)
61 {
62  for(symex_target_equationt::SSA_stepst::const_reverse_iterator
63  it=equation.SSA_steps.rbegin();
64  it!=equation.SSA_steps.rend();
65  it++)
66  {
67  preconditiont precondition(ns, value_sets, target, *it, s);
68  precondition.compute(dest);
69  if(dest.is_false())
70  return;
71  }
72 }
73 
75 {
76  if(dest.id()==ID_symbol)
77  {
78  // leave alone
79  }
80  else if(dest.id()==ID_index)
81  {
82  auto &index_expr = to_index_expr(dest);
83  compute_address_of(index_expr.array());
84  compute(index_expr.index());
85  }
86  else if(dest.id()==ID_member)
87  {
88  compute_address_of(to_member_expr(dest).compound());
89  }
90  else if(dest.id()==ID_dereference)
91  {
92  compute(to_dereference_expr(dest).pointer());
93  }
94 }
95 
97 {
98  compute_rec(dest);
99 }
100 
102 {
103  if(dest.id()==ID_address_of)
104  {
105  // only do index!
106  compute_address_of(to_address_of_expr(dest).object());
107  }
108  else if(dest.id()==ID_dereference)
109  {
110  auto &deref_expr = to_dereference_expr(dest);
111 
112  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
113 
114  // aliasing may happen here
115 
116  const std::vector<exprt> expr_set = value_sets.get_values(
117  SSA_step.source.function_id, target, deref_expr.pointer());
118  const std::unordered_set<irep_idt> symbols =
119  find_symbols_or_nexts(expr_set.begin(), expr_set.end());
120 
121  if(symbols.find(lhs_identifier)!=symbols.end())
122  {
123  // may alias!
124  exprt tmp;
125  tmp.swap(deref_expr.pointer());
127  deref_expr.swap(tmp);
128  compute_rec(deref_expr);
129  }
130  else
131  {
132  // nah, ok
133  compute_rec(deref_expr.pointer());
134  }
135  }
136  else if(dest==SSA_step.ssa_lhs.get_original_expr())
137  {
139  }
140  else
141  Forall_operands(it, dest)
142  compute_rec(*it);
143 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_target_equation.h
Generate Equation using Symbolic Execution.
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:47
find_symbols_or_nexts
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.
Definition: find_symbols.cpp:18
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:42
value_setst::get_values
virtual std::vector< exprt > get_values(const irep_idt &function_id, goto_programt::const_targett l, const exprt &expr)=0
exprt
Base class for all expressions.
Definition: expr.h:54
ssa_exprt::get_object_name
irep_idt get_object_name() const
SSA_stept::source
symex_targett::sourcet source
Definition: ssa_step.h:49
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
preconditiont::target
const goto_programt::const_targett target
Definition: precondition.cpp:42
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
preconditiont::compute_address_of
void compute_address_of(exprt &dest)
Definition: precondition.cpp:74
precondition.h
Generate Equation using Symbolic Execution.
preconditiont::compute_rec
void compute_rec(exprt &dest)
Definition: precondition.cpp:101
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
preconditiont::s
const goto_symex_statet & s
Definition: precondition.cpp:44
find_symbols.h
preconditiont
Definition: precondition.cpp:23
SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: ssa_step.h:143
preconditiont::SSA_step
const SSA_stept & SSA_step
Definition: precondition.cpp:43
renaming_level.h
Renaming levels.
pointer_expr.h
API to expression classes for Pointers.
preconditiont::compute
void compute(exprt &dest)
Definition: precondition.cpp:96
irept::swap
void swap(irept &irep)
Definition: irep.h:453
get_original_name
exprt get_original_name(exprt expr)
Undo all levels of renaming.
Definition: renaming_level.cpp:157
irept::id
const irep_idt & id() const
Definition: irep.h:407
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:34
value_setst
Definition: value_sets.h:22
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:250
preconditiont::preconditiont
preconditiont(const namespacet &_ns, value_setst &_value_sets, const goto_programt::const_targett _target, const SSA_stept &_SSA_step, const goto_symex_statet &_s)
Definition: precondition.cpp:25
preconditiont::ns
const namespacet & ns
Definition: precondition.cpp:40
SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: ssa_step.h:145
goto_program_dereference.h
Value Set.
precondition
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)
Definition: precondition.cpp:54
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
dereference
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...
Definition: goto_program_dereference.cpp:282
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:39
preconditiont::value_sets
value_setst & value_sets
Definition: precondition.cpp:41