cprover
Loading...
Searching...
No Matches
custom_bitvector_analysis.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-insensitive, location-sensitive bitvector analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
13#define CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
14
15#include <util/numbering.h>
16#include <util/threeval.h>
17
18#include "ai.h"
19#include "local_may_alias.h"
20
22
24{
25public:
26 void transform(
27 const irep_idt &function_from,
28 trace_ptrt trace_from,
29 const irep_idt &function_to,
30 trace_ptrt trace_to,
31 ai_baset &ai,
32 const namespacet &ns) final override;
33
34 void output(
35 std::ostream &out,
36 const ai_baset &ai,
37 const namespacet &ns) const final override;
38
39 void make_bottom() final override
40 {
41 may_bits.clear();
42 must_bits.clear();
43 has_values=tvt(false);
44 }
45
46 void make_top() final override
47 {
48 may_bits.clear();
49 must_bits.clear();
50 has_values=tvt(true);
51 }
52
53 void make_entry() final override
54 {
55 make_top();
56 }
57
58 bool is_bottom() const final override
59 {
61 (may_bits.empty() && must_bits.empty()),
62 "If the domain is bottom, it must have no bits set");
63 return has_values.is_false();
64 }
65
66 bool is_top() const final override
67 {
69 (may_bits.empty() && must_bits.empty()),
70 "If the domain is top, it must have no bits set");
71 return has_values.is_true();
72 }
73
74 bool merge(const custom_bitvector_domaint &b, trace_ptrt from, trace_ptrt to);
75
76 typedef unsigned long long bit_vectort;
77
78 typedef std::map<irep_idt, bit_vectort> bitst;
79
80 struct vectorst
81 {
84 {
85 }
86 };
87
88 static vectorst merge(const vectorst &a, const vectorst &b)
89 {
90 vectorst result;
91 result.may_bits=a.may_bits|b.may_bits;
92 result.must_bits=a.must_bits&b.must_bits;
93 return result;
94 }
95
97
99 locationt from,
100 const exprt &lhs,
101 const exprt &rhs,
103 const namespacet &);
104
105 void assign_lhs(const exprt &, const vectorst &);
106 void assign_lhs(const irep_idt &, const vectorst &);
107 vectorst get_rhs(const exprt &) const;
108 vectorst get_rhs(const irep_idt &) const;
109
111
113 {
114 }
115
116 static bool has_get_must_or_may(const exprt &);
117 exprt eval(
118 const exprt &src,
120
121private:
123
124 void set_bit(const exprt &, unsigned bit_nr, modet);
125 void set_bit(const irep_idt &, unsigned bit_nr, modet);
126
127 static inline void set_bit(bit_vectort &dest, unsigned bit_nr)
128 {
129 dest|=(1ll<<bit_nr);
130 }
131
132 static inline void clear_bit(bit_vectort &dest, unsigned bit_nr)
133 {
134 dest|=(1ll<<bit_nr);
135 dest^=(1ll<<bit_nr);
136 }
137
138 static inline bool get_bit(const bit_vectort src, unsigned bit_nr)
139 {
140 return (src&(1ll<<bit_nr))!=0;
141 }
142
144
145 static irep_idt object2id(const exprt &);
146};
147
148class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
149{
150public:
152 void check(
153 const goto_modelt &,
154 bool xml, std::ostream &);
155
156 exprt eval(const exprt &src, locationt loc)
157 {
158 return operator[](loc).eval(src, *this);
159 }
160
161 unsigned get_bit_nr(const exprt &);
162
165
166protected:
167 virtual void initialize(const goto_functionst &_goto_functions)
168 {
170 local_may_alias_factory(_goto_functions);
171 }
172
174
176
177 std::set<exprt> aliases(const exprt &, locationt loc);
178};
179
180#endif // CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
Abstract Interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
goto_programt::const_targett locationt
Definition: ai.h:126
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:189
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:55
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
goto_programt::const_targett locationt
Definition: ai_domain.h:73
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:564
const custom_bitvector_domaint & operator[](locationt l) const
Find the analysis result for a given location.
Definition: ai.h:595
std::set< exprt > aliases(const exprt &, locationt loc)
local_may_alias_factoryt local_may_alias_factory
exprt eval(const exprt &src, locationt loc)
void check(const goto_modelt &, bool xml, std::ostream &)
virtual void initialize(const goto_functionst &_goto_functions)
Initialize all the abstract states for a whole program.
static void set_bit(bit_vectort &dest, unsigned bit_nr)
void set_bit(const exprt &, unsigned bit_nr, modet)
bool merge(const custom_bitvector_domaint &b, trace_ptrt from, trace_ptrt to)
std::map< irep_idt, bit_vectort > bitst
bool is_bottom() const final override
static irep_idt object2id(const exprt &)
bool is_top() const final override
void assign_struct_rec(locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
static bool has_get_must_or_may(const exprt &)
vectorst get_rhs(const exprt &) const
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
void assign_lhs(const exprt &, const vectorst &)
void erase_blank_vectors(bitst &)
erase blank bitvectors
void make_entry() final override
Make this domain a reasonable entry-point state.
static bool get_bit(const bit_vectort src, unsigned bit_nr)
void make_bottom() final override
no states
exprt eval(const exprt &src, custom_bitvector_analysist &) const
static vectorst merge(const vectorst &a, const vectorst &b)
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
A collection of goto functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Definition: threeval.h:20
bool is_false() const
Definition: threeval.h:26
bool is_true() const
Definition: threeval.h:25
Field-insensitive, location-sensitive may-alias analysis.
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510