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  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 
98  void assign_struct_rec(
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 
121 private:
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 
143  void erase_blank_vectors(bitst &);
144 
145  static irep_idt object2id(const exprt &);
146 };
147 
148 class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
149 {
150 public:
151  void instrument(goto_functionst &);
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 
166 protected:
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