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  locationt from,
28  locationt to,
29  ai_baset &ai,
30  const namespacet &ns) final;
31 
32  void output(
33  std::ostream &out,
34  const ai_baset &ai,
35  const namespacet &ns) const final;
36 
37  void make_bottom() final
38  {
39  may_bits.clear();
40  must_bits.clear();
41  has_values=tvt(false);
42  }
43 
44  void make_top() final
45  {
46  may_bits.clear();
47  must_bits.clear();
48  has_values=tvt(true);
49  }
50 
51  void make_entry() final
52  {
53  make_top();
54  }
55 
56  bool merge(
57  const custom_bitvector_domaint &b,
58  locationt from,
59  locationt to);
60 
61  typedef unsigned long long bit_vectort;
62 
63  typedef std::map<irep_idt, bit_vectort> bitst;
64 
65  struct vectorst
66  {
69  {
70  }
71  };
72 
73  static vectorst merge(const vectorst &a, const vectorst &b)
74  {
75  vectorst result;
76  result.may_bits=a.may_bits|b.may_bits;
77  result.must_bits=a.must_bits&b.must_bits;
78  return result;
79  }
80 
82 
83  void assign_lhs(const exprt &, const vectorst &);
84  void assign_lhs(const irep_idt &, const vectorst &);
85  vectorst get_rhs(const exprt &) const;
86  vectorst get_rhs(const irep_idt &) const;
87 
89 
91  {
92  }
93 
94  static bool has_get_must_or_may(const exprt &);
95  exprt eval(
96  const exprt &src,
98 
99 private:
101 
102  void set_bit(const exprt &, unsigned bit_nr, modet);
103  void set_bit(const irep_idt &, unsigned bit_nr, modet);
104 
105  static inline void set_bit(bit_vectort &dest, unsigned bit_nr)
106  {
107  dest|=(1ll<<bit_nr);
108  }
109 
110  static inline void clear_bit(bit_vectort &dest, unsigned bit_nr)
111  {
112  dest|=(1ll<<bit_nr);
113  dest^=(1ll<<bit_nr);
114  }
115 
116  static inline bool get_bit(const bit_vectort src, unsigned bit_nr)
117  {
118  return (src&(1ll<<bit_nr))!=0;
119  }
120 
121  void erase_blank_vectors(bitst &);
122 
123  static irep_idt object2id(const exprt &);
124 };
125 
126 class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
127 {
128 public:
129  void instrument(goto_functionst &);
130  void check(
131  const namespacet &,
132  const goto_functionst &,
133  bool xml, std::ostream &);
134 
135  exprt eval(const exprt &src, locationt loc)
136  {
137  return operator[](loc).eval(src, *this);
138  }
139 
140  unsigned get_bit_nr(const exprt &);
141 
144 
145 protected:
146  virtual void initialize(const goto_functionst &_goto_functions)
147  {
149  local_may_alias_factory(_goto_functions);
150  }
151 
153 
155 
156  std::set<exprt> aliases(const exprt &, locationt loc);
157 };
158 
159 #endif // CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
#define loc()
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
goto_programt::const_targett locationt
Definition: ai.h:112
std::map< irep_idt, bit_vectort > bitst
Definition: ai.h:342
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
static bool get_bit(const bit_vectort src, unsigned bit_nr)
void assign_lhs(const exprt &, const vectorst &)
custom_bitvector_domaint & operator[](locationt l)
Definition: ai.h:352
void check(const namespacet &, const goto_functionst &, bool xml, std::ostream &)
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:62
static void set_bit(bit_vectort &dest, unsigned bit_nr)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
Abstract Interpretation.
Definition: ai.h:108
Base class for all expressions.
Definition: expr.h:46
exprt eval(const exprt &src, locationt loc)
virtual void initialize(const goto_programt &)
Definition: ai.cpp:269
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.h:42
static vectorst merge(const vectorst &a, const vectorst &b)
Field-insensitive, location-sensitive may-alias analysis.