cprover
Loading...
Searching...
No Matches
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> trace_mapt;
105
106 // This retains one part of a shared_ptr to the history object
108 {
109 // Save the trace_ptrt
110 trace_mapt::iterator it = trace_map.find(p->current_location());
111 if(it == trace_map.end())
112 {
113 trace_set_ptrt s(new trace_sett());
114 auto ins = trace_map.emplace(p->current_location(), s);
115 CHECK_RETURN(ins.second);
116 it = ins.first;
117 }
118 // Strictly this should be "it->second points to a trace_set"
119 POSTCONDITION(it->second != nullptr);
120
121 it->second->insert(p);
122
123 return;
124 }
125
126public:
128 {
129 trace_mapt::const_iterator it = trace_map.find(l);
130 if(it == trace_map.end())
131 return trace_set_ptrt(new trace_sett());
132
133 // Strictly this should be "it->second points to a trace_set"
134 POSTCONDITION(it->second != nullptr);
135 return it->second;
136 }
137
138 void clear() override
139 {
141 trace_map.clear();
142 return;
143 }
144};
145
146// A couple of older domains make direct use of the state map
150
153{
154protected:
156 typedef std::unordered_map<
157 locationt,
163
164 // Support some older domains that explicitly iterate across the state map
167 friend variable_sensitivity_dependence_grapht; // Based on dependence_grapht
169 {
170 return state_map;
171 }
172
173public:
175 trace_ptrt p,
176 const ai_domain_factory_baset &fac) const override
177 {
178 return abstract_state_before(p->current_location(), fac);
179 }
180
182 locationt l,
183 const ai_domain_factory_baset &fac) const override
184 {
185 typename state_mapt::const_iterator it = state_map.find(l);
186 if(it == state_map.end())
187 return fac.make(l);
188
189 return it->second;
190 }
191
193 {
195 return get_state(p->current_location(), fac);
196 }
197
198 // For backwards compatability
199 // Care should be exercised in using this. It is possible to create domains
200 // without any corresponding history object(s). This can lead to somewhat
201 // unexpected behaviour depending on which APIs you use.
202 DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
204 {
205 typename state_mapt::const_iterator it = state_map.find(l);
206 if(it == state_map.end())
207 {
208 std::shared_ptr<statet> d(fac.make(l));
209 auto p = state_map.emplace(l, d);
210 CHECK_RETURN(p.second);
211 it = p.first;
212 }
213
214 return *(it->second);
215 }
216
217 void clear() override
218 {
220 state_map.clear();
221 return;
222 }
223};
224
225// The most precise form of storage
227{
228protected:
229 typedef std::map<trace_ptrt, state_ptrt, ai_history_baset::compare_historyt>
232
233public:
235 trace_ptrt p,
236 const ai_domain_factory_baset &fac) const override
237 {
238 auto it = domain_map.find(p);
239 if(it == domain_map.end())
240 return fac.make(p->current_location());
241
242 return it->second;
243 }
244
246 locationt t,
247 const ai_domain_factory_baset &fac) const override
248 {
249 auto traces = abstract_traces_before(t);
250
251 if(traces->size() == 0)
252 {
253 return fac.make(t);
254 }
255 else if(traces->size() == 1)
256 {
257 auto it = domain_map.find(*(traces->begin()));
259 it != domain_map.end(), "domain_map must be in sync with trace_map");
260 return it->second;
261 }
262 else
263 {
264 // Need to merge all of the traces that reach this location
265 auto res = fac.make(t);
266
267 for(auto p : *traces)
268 {
269 auto it = domain_map.find(p);
271 it != domain_map.end(), "domain_map must be in sync with trace_map");
272 fac.merge(*res, *(it->second), p, p);
273 }
274
275 return cstate_ptrt(res.release());
276 }
277 }
278
280 {
282
283 auto it = domain_map.find(p);
284 if(it == domain_map.end())
285 {
286 std::shared_ptr<statet> d(fac.make(p->current_location()));
287 auto jt = domain_map.emplace(p, d);
288 CHECK_RETURN(jt.second);
289 it = jt.first;
290 }
291
292 return *(it->second);
293 }
294
295 void clear() override
296 {
298 domain_map.clear();
299 return;
300 }
301};
302
303#endif
Abstract Interpretation Domain.
Abstract Interpretation history.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:55
virtual std::unique_ptr< statet > make(locationt l) const =0
virtual bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) const =0
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
instructionst::const_iterator const_targett
Definition: goto_program.h:593
void clear() override
Reset the abstract state.
Definition: ai_storage.h:295
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:234
std::map< trace_ptrt, state_ptrt, ai_history_baset::compare_historyt > domain_mapt
Definition: ai_storage.h:230
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:279
cstate_ptrt abstract_state_before(locationt t, const ai_domain_factory_baset &fac) const override
Definition: ai_storage.h:245
The most conventional storage; one domain per location.
Definition: ai_storage.h:153
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:174
friend variable_sensitivity_dependence_grapht
Definition: ai_storage.h:167
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:192
state_mapt & internal(void)
Definition: ai_storage.h:168
cstate_ptrt abstract_state_before(locationt l, const ai_domain_factory_baset &fac) const override
Definition: ai_storage.h:181
void clear() override
Reset the abstract state.
Definition: ai_storage.h:217
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:161
std::map< locationt, trace_set_ptrt > trace_mapt
Definition: ai_storage.h:103
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:127
void register_trace(trace_ptrt p)
Definition: ai_storage.h:107
trace_mapt trace_map
Definition: ai_storage.h:104
void clear() override
Reset the abstract state.
Definition: ai_storage.h:138
#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:510
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
Functor to check whether iterators from different collections point at the same object.