cprover
Loading...
Searching...
No Matches
precondition.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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"
21
23{
24public:
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
39protected:
40 const namespacet &ns;
45 void compute_rec(exprt &dest);
46
47public:
48 void compute(exprt &dest);
49
50protected:
51 void compute_address_of(exprt &dest);
52};
53
55 const namespacet &ns,
56 value_setst &value_sets,
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!
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 bool may_alias = false;
117 for(const exprt &e : value_sets.get_values(
119 {
120 if(has_symbol_expr(e, lhs_identifier, false))
121 {
122 may_alias = true;
123 break;
124 }
125 }
126
127 if(may_alias)
128 {
129 exprt tmp;
130 tmp.swap(deref_expr.pointer());
132 deref_expr.swap(tmp);
134 }
135 else
136 {
137 // nah, ok
138 compute_rec(deref_expr.pointer());
139 }
140 }
141 else if(dest==SSA_step.ssa_lhs.get_original_expr())
142 {
144 }
145 else
146 Forall_operands(it, dest)
147 compute_rec(*it);
148}
Single SSA step in the equation.
Definition ssa_step.h:47
exprt ssa_rhs
Definition ssa_step.h:141
symex_targett::sourcet source
Definition ssa_step.h:49
ssa_exprt ssa_lhs
Definition ssa_step.h:139
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
instructionst::const_iterator const_targett
Central data structure: state.
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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
Definition ssa_expr.cpp:144
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:27
bool has_symbol_expr(const exprt &src, const irep_idt &identifier, bool include_bound_symbols)
Returns true if one of the symbol expressions in src has identifier identifier; if include_bound_symb...
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...
optionalt< exprt > may_alias(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
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.
Renaming levels.
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
Generate Equation using Symbolic Execution.