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
27  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
28  final override;
29 
30  void output(
31  std::ostream &out,
32  const ai_baset &ai,
33  const namespacet &ns) const final override;
34 
35  void make_bottom() final override
36  {
37  may_bits.clear();
38  must_bits.clear();
39  has_values=tvt(false);
40  }
41 
42  void make_top() final override
43  {
44  may_bits.clear();
45  must_bits.clear();
46  has_values=tvt(true);
47  }
48 
49  void make_entry() final override
50  {
51  make_top();
52  }
53 
54  bool is_bottom() const final override
55  {
57  (may_bits.empty() && must_bits.empty()),
58  "If the domain is bottom, it must have no bits set");
59  return has_values.is_false();
60  }
61 
62  bool is_top() const final override
63  {
65  (may_bits.empty() && must_bits.empty()),
66  "If the domain is top, it must have no bits set");
67  return has_values.is_true();
68  }
69 
70  bool merge(
71  const custom_bitvector_domaint &b,
72  locationt from,
73  locationt to);
74 
75  typedef unsigned long long bit_vectort;
76 
77  typedef std::map<irep_idt, bit_vectort> bitst;
78 
79  struct vectorst
80  {
83  {
84  }
85  };
86 
87  static vectorst merge(const vectorst &a, const vectorst &b)
88  {
89  vectorst result;
90  result.may_bits=a.may_bits|b.may_bits;
91  result.must_bits=a.must_bits&b.must_bits;
92  return result;
93  }
94 
96 
97  void assign_struct_rec(
98  locationt from,
99  const exprt &lhs,
100  const exprt &rhs,
102  const namespacet &);
103 
104  void assign_lhs(const exprt &, const vectorst &);
105  void assign_lhs(const irep_idt &, const vectorst &);
106  vectorst get_rhs(const exprt &) const;
107  vectorst get_rhs(const irep_idt &) const;
108 
110 
112  {
113  }
114 
115  static bool has_get_must_or_may(const exprt &);
116  exprt eval(
117  const exprt &src,
119 
120 private:
122 
123  void set_bit(const exprt &, unsigned bit_nr, modet);
124  void set_bit(const irep_idt &, unsigned bit_nr, modet);
125 
126  static inline void set_bit(bit_vectort &dest, unsigned bit_nr)
127  {
128  dest|=(1ll<<bit_nr);
129  }
130 
131  static inline void clear_bit(bit_vectort &dest, unsigned bit_nr)
132  {
133  dest|=(1ll<<bit_nr);
134  dest^=(1ll<<bit_nr);
135  }
136 
137  static inline bool get_bit(const bit_vectort src, unsigned bit_nr)
138  {
139  return (src&(1ll<<bit_nr))!=0;
140  }
141 
142  void erase_blank_vectors(bitst &);
143 
144  static irep_idt object2id(const exprt &);
145 };
146 
147 class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
148 {
149 public:
150  void instrument(goto_functionst &);
151  void check(
152  const goto_modelt &,
153  bool xml, std::ostream &);
154 
155  exprt eval(const exprt &src, locationt loc)
156  {
157  return operator[](loc).eval(src, *this);
158  }
159 
160  unsigned get_bit_nr(const exprt &);
161 
164 
165 protected:
166  virtual void initialize(const goto_functionst &_goto_functions)
167  {
169  local_may_alias_factory(_goto_functions);
170  }
171 
173 
175 
176  std::set<exprt> aliases(const exprt &, locationt loc);
177 };
178 
179 #endif // CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
#define loc()
void transform(locationt from, locationt 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...
bool is_false() const
Definition: threeval.h:26
goto_programt::const_targett locationt
Definition: ai.h:36
std::map< irep_idt, bit_vectort > bitst
Definition: ai.h:294
bool is_bottom() const final override
local_may_alias_factoryt local_may_alias_factory
virtual void initialize(const goto_functionst &_goto_functions)
static irep_idt object2id(const exprt &)
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
void make_top() final override
all states – the analysis doesn&#39;t use this, and domains may refuse to implement it.
static bool get_bit(const bit_vectort src, unsigned bit_nr)
bool is_top() const final override
void make_bottom() final override
no states
void assign_lhs(const exprt &, const vectorst &)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
void check(const goto_modelt &, bool xml, std::ostream &)
custom_bitvector_domaint & operator[](locationt l)
Definition: ai.h:304
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
void set_bit(const exprt &, unsigned bit_nr, modet)
void erase_blank_vectors(bitst &)
erase blank bitvectors
static bool has_get_must_or_may(const exprt &)
Definition: threeval.h:19
exprt eval(const exprt &src, custom_bitvector_analysist &) const
vectorst get_rhs(const exprt &) const
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void make_entry() final override
a reasonable entry-point state
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bool is_true() const
Definition: threeval.h:25
static void set_bit(bit_vectort &dest, unsigned bit_nr)
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:42
exprt eval(const exprt &src, locationt loc)
virtual void initialize(const goto_programt &)
Definition: ai.cpp:202
bool merge(const custom_bitvector_domaint &b, locationt from, locationt to)
std::set< exprt > aliases(const exprt &, locationt loc)
goto_programt::const_targett locationt
Definition: ai_domain.h:40
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
static vectorst merge(const vectorst &a, const vectorst &b)
void assign_struct_rec(locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)
Field-insensitive, location-sensitive may-alias analysis.