CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
value_set_domain.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
13#define CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
14
15#include <util/invariant.h>
16
17#include <analyses/ai.h>
18
19#include "value_set.h"
20
24template <class VST>
26{
27protected:
31
32public:
34
36 {
38 value_set.location_number = l->location_number;
39 }
40
41 void make_bottom() override
42 {
43 reachable = false;
44 value_set.clear(); //???
45 }
46
47 void make_top() override
48 {
50 }
51
52 void make_entry() override
53 {
54 reachable = true;
55 }
56
57 bool is_bottom() const override
58 {
59 return reachable == false && value_set.values.size() == 0;
60 }
61
62 bool is_top() const override
63 {
64 return false;
65 }
66
67 // overloading
68
69 bool
71 {
72 reachable |= other.reachable;
73 return value_set.make_union(other.value_set);
74 }
75
76 void
77 output(std::ostream &out, const ai_baset &, const namespacet &) const override
78 {
79 value_set.output(out);
80 }
81
82 void transform(
85 const irep_idt &function_to,
87 ai_baset &ai,
88 const namespacet &ns) override;
89
91 const namespacet &ns,
92 const exprt &expr,
94 {
95 value_set.get_reference_set(expr, dest, ns);
96 }
97
99 {
100 // get predecessor of "to"
101 to--;
102
103 if(to->is_end_function())
104 return static_cast<const exprt &>(get_nil_irep());
105
106 INVARIANT(to->is_function_call(), "must be the function call");
107
108 return to->call_lhs();
109 }
110
111 xmlt output_xml(const ai_baset &ai, const namespacet &ns) const override
112 {
113 return value_set.output_xml();
114 }
115};
116
118
119template <class VST>
121 const irep_idt &,
123 const irep_idt &function_to,
125 ai_baset &,
126 const namespacet &ns)
127{
128 if(!reachable)
129 return;
130
131 locationt from_l{from->current_location()};
132 locationt to_l{to->current_location()};
133
134 switch(from_l->type())
135 {
136 case GOTO:
137 // ignore for now
138 break;
139
140 case END_FUNCTION:
141 {
142 value_set.do_end_function(get_return_lhs(to_l), ns);
143 break;
144 }
145
146 // Note intentional fall-through here:
147 case SET_RETURN_VALUE:
148 case OTHER:
149 case ASSIGN:
150 case DECL:
151 case DEAD:
152 value_set.apply_code(from_l->code(), ns);
153 break;
154
155 case ASSUME:
156 value_set.guard(from_l->condition(), ns);
157 break;
158
159 case FUNCTION_CALL:
160 value_set.do_function_call(function_to, from_l->call_arguments(), ns);
161 break;
162
163 case ASSERT:
164 case SKIP:
165 case START_THREAD:
166 case END_THREAD:
167 case LOCATION:
168 case ATOMIC_BEGIN:
169 case ATOMIC_END:
170 case THROW:
171 case CATCH:
172 case INCOMPLETE_GOTO:
174 {
175 // do nothing
176 }
177 }
178}
179
180// To pass the correct location to the constructor we need a factory
183
184#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
Abstract Interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
virtual void clear()
Reset the abstract state.
Definition ai.h:265
virtual xmlt output_xml(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
Definition ai.cpp:136
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:54
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:73
goto_programt::const_targett locationt
Definition ai_domain.h:72
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
This is the domain for a value set analysis.
xmlt output_xml(const ai_baset &ai, const namespacet &ns) const override
exprt get_return_lhs(locationt to) const
void get_reference_set(const namespacet &ns, const exprt &expr, value_setst::valuest &dest)
bool merge(const value_set_domain_templatet< VST > &other, trace_ptrt, trace_ptrt)
bool reachable
ait checks whether domains are bottom to increase speed and accuracy.
void make_entry() override
Make this domain a reasonable entry-point state For most domains top is sufficient.
void make_bottom() override
no states
bool is_top() const override
value_set_domain_templatet(locationt l)
void transform(const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns) override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
bool is_bottom() const override
void output(std::ostream &out, const ai_baset &, const namespacet &) const override
void make_top() override
all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implem...
std::list< exprt > valuest
Definition value_sets.h:28
Definition xml.h:21
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
const irept & get_nil_irep()
Definition irep.cpp:19
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Value Set.
ai_domain_factory_location_constructort< value_set_domaint > value_set_domain_factoryt
value_set_domain_templatet< value_sett > value_set_domaint