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
#define loc()
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:365
bool is_bottom() const final override
local_may_alias_factoryt local_may_alias_factory
virtual void initialize(const goto_functionst &_goto_functions)
Initialize all the abstract states for a whole program.
static irep_idt object2id(const exprt &)
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
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 &)
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:202
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:375
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void make_entry() final override
Make this domain a reasonable entry-point state.
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, 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...
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
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:54
exprt eval(const exprt &src, locationt loc)
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)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
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.