CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
ai_storage.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Abstract Interpretation
4
5Author: Martin Brain, martin.brain@cs.ox.ac.uk
6
7\*******************************************************************/
8
22
23#ifndef CPROVER_ANALYSES_AI_STORAGE_H
24#define CPROVER_ANALYSES_AI_STORAGE_H
25
26#include <util/deprecate.h>
27
29
30#include "ai_domain.h"
31#include "ai_history.h"
32
36{
37protected:
39 {
40 }
41
42public:
44 {
45 }
46
48 typedef std::shared_ptr<statet> state_ptrt;
49 typedef std::shared_ptr<const statet> cstate_ptrt;
53 typedef std::shared_ptr<trace_sett> trace_set_ptrt;
54 typedef std::shared_ptr<const trace_sett> ctrace_set_ptrt;
56
60
67 trace_ptrt p,
68 const ai_domain_factory_baset &fac) const = 0;
69
71 locationt l,
72 const ai_domain_factory_baset &fac) const = 0;
73
76 virtual statet &
78
80 virtual void clear()
81 {
82 return;
83 }
84
91 virtual void prune(locationt l)
92 {
93 return;
94 }
95};
96
97// There are a number of options for how to store the history objects.
98// This implements a simple one. It is not in ai_storage_baset so that
99// storage implementations can implement their own, more specific, approaches
101{
102protected:
103 typedef std::map<locationt, trace_set_ptrt, goto_programt::target_less_than>
106
107 // This retains one part of a shared_ptr to the history object
109 {
110 // Save the trace_ptrt
111 trace_mapt::iterator it = trace_map.find(p->current_location());
112 if(it == trace_map.end())
113 {
114 trace_set_ptrt s(new trace_sett());
115 auto ins = trace_map.emplace(p->current_location(), s);
116 CHECK_RETURN(ins.second);
117 it = ins.first;
118 }
119 // Strictly this should be "it->second points to a trace_set"
120 POSTCONDITION(it->second != nullptr);
121
122 it->second->insert(p);
123
124 return;
125 }
126
127public:
129 {
130 trace_mapt::const_iterator it = trace_map.find(l);
131 if(it == trace_map.end())
132 return trace_set_ptrt(new trace_sett());
133
134 // Strictly this should be "it->second points to a trace_set"
135 POSTCONDITION(it->second != nullptr);
136 return it->second;
137 }
138
139 void clear() override
140 {
142 trace_map.clear();
143 return;
144 }
145};
146
147// A couple of older domains make direct use of the state map
151
154{
155protected:
157 typedef std::unordered_map<
158 locationt,
164
165 // Support some older domains that explicitly iterate across the state map
168 friend variable_sensitivity_dependence_grapht; // Based on dependence_grapht
170 {
171 return state_map;
172 }
173
174public:
176 trace_ptrt p,
177 const ai_domain_factory_baset &fac) const override
178 {
179 return abstract_state_before(p->current_location(), fac);
180 }
181
183 locationt l,
184 const ai_domain_factory_baset &fac) const override
185 {
186 typename state_mapt::const_iterator it = state_map.find(l);
187 if(it == state_map.end())
188 return fac.make(l);
189
190 return it->second;
191 }
192
194 {
196 return get_state(p->current_location(), fac);
197 }
198
199 // For backwards compatability
200 // Care should be exercised in using this. It is possible to create domains
201 // without any corresponding history object(s). This can lead to somewhat
202 // unexpected behaviour depending on which APIs you use.
203 DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
205 {
206 typename state_mapt::const_iterator it = state_map.find(l);
207 if(it == state_map.end())
208 {
209 std::shared_ptr<statet> d(fac.make(l));
210 auto p = state_map.emplace(l, d);
211 CHECK_RETURN(p.second);
212 it = p.first;
213 }
214
215 return *(it->second);
216 }
217
218 void clear() override
219 {
221 state_map.clear();
222 return;
223 }
224};
225
226// The most precise form of storage
228{
229protected:
230 typedef std::map<trace_ptrt, state_ptrt, ai_history_baset::compare_historyt>
233
234public:
236 trace_ptrt p,
237 const ai_domain_factory_baset &fac) const override
238 {
239 auto it = domain_map.find(p);
240 if(it == domain_map.end())
241 return fac.make(p->current_location());
242
243 return it->second;
244 }
245
247 locationt t,
248 const ai_domain_factory_baset &fac) const override
249 {
250 auto traces = abstract_traces_before(t);
251
252 if(traces->size() == 0)
253 {
254 return fac.make(t);
255 }
256 else if(traces->size() == 1)
257 {
258 auto it = domain_map.find(*(traces->begin()));
260 it != domain_map.end(), "domain_map must be in sync with trace_map");
261 return it->second;
262 }
263 else
264 {
265 // Need to merge all of the traces that reach this location
266 auto res = fac.make(t);
267
268 for(auto p : *traces)
269 {
270 auto it = domain_map.find(p);
272 it != domain_map.end(), "domain_map must be in sync with trace_map");
273 fac.merge(*res, *(it->second), p, p);
274 }
275
276 return cstate_ptrt(res.release());
277 }
278 }
279
281 {
283
284 auto it = domain_map.find(p);
285 if(it == domain_map.end())
286 {
287 std::shared_ptr<statet> d(fac.make(p->current_location()));
288 auto jt = domain_map.emplace(p, d);
289 CHECK_RETURN(jt.second);
290 it = jt.first;
291 }
292
293 return *(it->second);
294 }
295
296 void clear() override
297 {
299 domain_map.clear();
300 return;
301 }
302};
303
304#endif
Abstract Interpretation Domain.
Abstract Interpretation history.
virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)
Merge the state src, flowing from tracet from to tracet to, into the state currently stored for trace...
Definition ai.h:498
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:54
A history object is an abstraction / representation of the control-flow part of a set of traces.
Definition ai_history.h:37
std::shared_ptr< const ai_history_baset > trace_ptrt
History objects are intended to be immutable so they can be shared to reduce memory overhead.
Definition ai_history.h:43
std::set< trace_ptrt, compare_historyt > trace_sett
Definition ai_history.h:79
This is the basic interface for storing domains.
Definition ai_storage.h:36
virtual void clear()
Reset the abstract state.
Definition ai_storage.h:80
virtual statet & get_state(trace_ptrt p, const ai_domain_factory_baset &fac)=0
Look up the analysis state for a given history, instantiating a new domain if required.
virtual ~ai_storage_baset()
Definition ai_storage.h:43
goto_programt::const_targett locationt
Definition ai_storage.h:55
virtual cstate_ptrt abstract_state_before(trace_ptrt p, const ai_domain_factory_baset &fac) const =0
Non-modifying access to the stored domains, used in the ai_baset public interface.
std::shared_ptr< trace_sett > trace_set_ptrt
Definition ai_storage.h:53
ai_history_baset::trace_sett trace_sett
Definition ai_storage.h:52
virtual void prune(locationt l)
Notifies the storage that the user will not need the domain object(s) for this location.
Definition ai_storage.h:91
std::shared_ptr< const trace_sett > ctrace_set_ptrt
Definition ai_storage.h:54
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_storage.h:51
virtual cstate_ptrt abstract_state_before(locationt l, const ai_domain_factory_baset &fac) const =0
ai_history_baset tracet
Definition ai_storage.h:50
std::shared_ptr< statet > state_ptrt
Definition ai_storage.h:48
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const =0
Returns all of the histories that have reached the start of the instruction.
std::shared_ptr< const statet > cstate_ptrt
Definition ai_storage.h:49
ai_domain_baset statet
Definition ai_storage.h:47
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
instructionst::const_iterator const_targett
void clear() override
Reset the abstract state.
Definition ai_storage.h:296
cstate_ptrt abstract_state_before(trace_ptrt p, const ai_domain_factory_baset &fac) const override
Non-modifying access to the stored domains, used in the ai_baset public interface.
Definition ai_storage.h:235
std::map< trace_ptrt, state_ptrt, ai_history_baset::compare_historyt > domain_mapt
Definition ai_storage.h:231
statet & get_state(trace_ptrt p, const ai_domain_factory_baset &fac) override
Look up the analysis state for a given history, instantiating a new domain if required.
Definition ai_storage.h:280
cstate_ptrt abstract_state_before(locationt t, const ai_domain_factory_baset &fac) const override
Definition ai_storage.h:246
The most conventional storage; one domain per location.
Definition ai_storage.h:154
cstate_ptrt abstract_state_before(trace_ptrt p, const ai_domain_factory_baset &fac) const override
Non-modifying access to the stored domains, used in the ai_baset public interface.
Definition ai_storage.h:175
friend variable_sensitivity_dependence_grapht
Definition ai_storage.h:168
statet & get_state(trace_ptrt p, const ai_domain_factory_baset &fac) override
Look up the analysis state for a given history, instantiating a new domain if required.
Definition ai_storage.h:193
state_mapt & internal(void)
Definition ai_storage.h:169
cstate_ptrt abstract_state_before(locationt l, const ai_domain_factory_baset &fac) const override
Definition ai_storage.h:182
void clear() override
Reset the abstract state.
Definition ai_storage.h:218
std::unordered_map< locationt, state_ptrt, const_target_hash, pointee_address_equalt > state_mapt
This is location sensitive so we store one domain per location.
Definition ai_storage.h:162
ctrace_set_ptrt abstract_traces_before(locationt l) const override
Returns all of the histories that have reached the start of the instruction.
Definition ai_storage.h:128
std::map< locationt, trace_set_ptrt, goto_programt::target_less_than > trace_mapt
Definition ai_storage.h:104
void register_trace(trace_ptrt p)
Definition ai_storage.h:108
trace_mapt trace_map
Definition ai_storage.h:105
void clear() override
Reset the abstract state.
Definition ai_storage.h:139
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
Concrete Goto Program.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define POSTCONDITION(CONDITION)
Definition invariant.h:479
Functor to check whether iterators from different collections point at the same object.