cprover
custom_bitvector_analysis.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive bitvector analysis
4 
5 Author: 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 {
25 public:
26  void transform(
27  const irep_idt &function_from,
28  locationt from,
29  const irep_idt &function_to,
30  locationt 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(
75  const custom_bitvector_domaint &b,
76  locationt from,
77  locationt to);
78 
79  typedef unsigned long long bit_vectort;
80 
81  typedef std::map<irep_idt, bit_vectort> bitst;
82 
83  struct vectorst
84  {
87  {
88  }
89  };
90 
91  static vectorst merge(const vectorst &a, const vectorst &b)
92  {
93  vectorst result;
94  result.may_bits=a.may_bits|b.may_bits;
95  result.must_bits=a.must_bits&b.must_bits;
96  return result;
97  }
98 
100 
101  void assign_struct_rec(
102  locationt from,
103  const exprt &lhs,
104  const exprt &rhs,
106  const namespacet &);
107 
108  void assign_lhs(const exprt &, const vectorst &);
109  void assign_lhs(const irep_idt &, const vectorst &);
110  vectorst get_rhs(const exprt &) const;
111  vectorst get_rhs(const irep_idt &) const;
112 
114 
116  {
117  }
118 
119  static bool has_get_must_or_may(const exprt &);
120  exprt eval(
121  const exprt &src,
123 
124 private:
126 
127  void set_bit(const exprt &, unsigned bit_nr, modet);
128  void set_bit(const irep_idt &, unsigned bit_nr, modet);
129 
130  static inline void set_bit(bit_vectort &dest, unsigned bit_nr)
131  {
132  dest|=(1ll<<bit_nr);
133  }
134 
135  static inline void clear_bit(bit_vectort &dest, unsigned bit_nr)
136  {
137  dest|=(1ll<<bit_nr);
138  dest^=(1ll<<bit_nr);
139  }
140 
141  static inline bool get_bit(const bit_vectort src, unsigned bit_nr)
142  {
143  return (src&(1ll<<bit_nr))!=0;
144  }
145 
146  void erase_blank_vectors(bitst &);
147 
148  static irep_idt object2id(const exprt &);
149 };
150 
151 class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
152 {
153 public:
154  void instrument(goto_functionst &);
155  void check(
156  const goto_modelt &,
157  bool xml, std::ostream &);
158 
159  exprt eval(const exprt &src, locationt loc)
160  {
161  return operator[](loc).eval(src, *this);
162  }
163 
164  unsigned get_bit_nr(const exprt &);
165 
168 
169 protected:
170  virtual void initialize(const goto_functionst &_goto_functions)
171  {
173  local_may_alias_factory(_goto_functions);
174  }
175 
177 
179 
180  std::set<exprt> aliases(const exprt &, locationt loc);
181 };
182 
183 #endif // CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
custom_bitvector_domaint::modet::CLEAR_MAY
@ CLEAR_MAY
custom_bitvector_domaint::merge
static vectorst merge(const vectorst &a, const vectorst &b)
Definition: custom_bitvector_analysis.h:91
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
custom_bitvector_domaint::assign_lhs
void assign_lhs(const exprt &, const vectorst &)
Definition: custom_bitvector_analysis.cpp:110
custom_bitvector_domaint::object2id
static irep_idt object2id(const exprt &)
Definition: custom_bitvector_analysis.cpp:58
custom_bitvector_domaint::vectorst::must_bits
bit_vectort must_bits
Definition: custom_bitvector_analysis.h:85
custom_bitvector_domaint::modet::SET_MAY
@ SET_MAY
ai_baset::locationt
goto_programt::const_targett locationt
Definition: ai.h:126
custom_bitvector_domaint::assign_struct_rec
void assign_struct_rec(locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)
Definition: custom_bitvector_analysis.cpp:226
ait< custom_bitvector_domaint >::operator[]
const custom_bitvector_domaint & operator[](locationt l) const
Find the analysis result for a given location.
Definition: ai.h:587
custom_bitvector_domaint::erase_blank_vectors
void erase_blank_vectors(bitst &)
erase blank bitvectors
Definition: custom_bitvector_analysis.cpp:674
threeval.h
custom_bitvector_domaint::get_rhs
vectorst get_rhs(const exprt &) const
Definition: custom_bitvector_analysis.cpp:153
template_numberingt
Definition: numbering.h:22
custom_bitvector_domaint::modet::CLEAR_MUST
@ CLEAR_MUST
custom_bitvector_domaint::must_bits
bitst must_bits
Definition: custom_bitvector_analysis.h:99
custom_bitvector_domaint::make_top
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
Definition: custom_bitvector_analysis.h:46
custom_bitvector_domaint::vectorst::vectorst
vectorst()
Definition: custom_bitvector_analysis.h:86
custom_bitvector_analysist::bitst
numbering< irep_idt > bitst
Definition: custom_bitvector_analysis.h:166
exprt
Base class for all expressions.
Definition: expr.h:53
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:558
goto_modelt
Definition: goto_model.h:26
custom_bitvector_analysist::eval
exprt eval(const exprt &src, locationt loc)
Definition: custom_bitvector_analysis.h:159
custom_bitvector_domaint::set_bit
void set_bit(const exprt &, unsigned bit_nr, modet)
Definition: custom_bitvector_analysis.cpp:48
custom_bitvector_analysist::instrument
void instrument(goto_functionst &)
Definition: custom_bitvector_analysis.cpp:764
custom_bitvector_analysist::aliases
std::set< exprt > aliases(const exprt &, locationt loc)
Definition: custom_bitvector_analysis.cpp:191
custom_bitvector_domaint::may_bits
bitst may_bits
Definition: custom_bitvector_analysis.h:99
custom_bitvector_domaint::clear_bit
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
Definition: custom_bitvector_analysis.h:135
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
custom_bitvector_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Definition: custom_bitvector_analysis.cpp:562
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
custom_bitvector_domaint::modet
modet
Definition: custom_bitvector_analysis.h:125
custom_bitvector_domaint::modet::SET_MUST
@ SET_MUST
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
custom_bitvector_domaint
Definition: custom_bitvector_analysis.h:24
custom_bitvector_analysist
Definition: custom_bitvector_analysis.h:152
custom_bitvector_domaint::custom_bitvector_domaint
custom_bitvector_domaint()
Definition: custom_bitvector_analysis.h:115
numbering.h
ai.h
Abstract Interpretation.
tvt::is_false
bool is_false() const
Definition: threeval.h:26
custom_bitvector_domaint::is_top
bool is_top() const final override
Definition: custom_bitvector_analysis.h:66
tvt
Definition: threeval.h:20
local_may_alias_factoryt
Definition: local_may_alias.h:96
custom_bitvector_domaint::vectorst::may_bits
bit_vectort may_bits
Definition: custom_bitvector_analysis.h:85
custom_bitvector_domaint::make_entry
void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: custom_bitvector_analysis.h:53
ai_baset::initialize
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:190
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
custom_bitvector_domaint::has_get_must_or_may
static bool has_get_must_or_may(const exprt &)
Definition: custom_bitvector_analysis.cpp:687
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
custom_bitvector_domaint::bit_vectort
unsigned long long bit_vectort
Definition: custom_bitvector_analysis.h:79
custom_bitvector_domaint::vectorst
Definition: custom_bitvector_analysis.h:84
custom_bitvector_analysist::local_may_alias_factory
local_may_alias_factoryt local_may_alias_factory
Definition: custom_bitvector_analysis.h:178
custom_bitvector_analysist::initialize
virtual void initialize(const goto_functionst &_goto_functions)
Initialize all the abstract states for a whole program.
Definition: custom_bitvector_analysis.h:170
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
custom_bitvector_domaint::eval
exprt eval(const exprt &src, custom_bitvector_analysist &) const
Definition: custom_bitvector_analysis.cpp:699
custom_bitvector_domaint::transform
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Definition: custom_bitvector_analysis.cpp:268
custom_bitvector_analysist::check
void check(const goto_modelt &, bool xml, std::ostream &)
Definition: custom_bitvector_analysis.cpp:768
custom_bitvector_domaint::set_bit
static void set_bit(bit_vectort &dest, unsigned bit_nr)
Definition: custom_bitvector_analysis.h:130
custom_bitvector_domaint::is_bottom
bool is_bottom() const final override
Definition: custom_bitvector_analysis.h:58
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
custom_bitvector_analysist::bits
bitst bits
Definition: custom_bitvector_analysis.h:167
custom_bitvector_domaint::bitst
std::map< irep_idt, bit_vectort > bitst
Definition: custom_bitvector_analysis.h:81
custom_bitvector_domaint::has_values
tvt has_values
Definition: custom_bitvector_analysis.h:113
custom_bitvector_analysist::get_bit_nr
unsigned get_bit_nr(const exprt &)
Definition: custom_bitvector_analysis.cpp:176
tvt::is_true
bool is_true() const
Definition: threeval.h:25
custom_bitvector_domaint::merge
bool merge(const custom_bitvector_domaint &b, locationt from, locationt to)
Definition: custom_bitvector_analysis.cpp:609
custom_bitvector_domaint::get_bit
static bool get_bit(const bit_vectort src, unsigned bit_nr)
Definition: custom_bitvector_analysis.h:141
custom_bitvector_domaint::make_bottom
void make_bottom() final override
no states
Definition: custom_bitvector_analysis.h:39