cprover
ai_storage.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstract Interpretation
4 
5 Author: 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 
27 
28 #include "ai_domain.h"
29 #include "ai_history.h"
30 
34 {
35 protected:
37  {
38  }
39 
40 public:
42  {
43  }
44 
46  typedef std::shared_ptr<statet> state_ptrt;
47  typedef std::shared_ptr<const statet> cstate_ptrt;
51  typedef std::shared_ptr<trace_sett> trace_set_ptrt;
52  typedef std::shared_ptr<const trace_sett> ctrace_set_ptrt;
54 
58 
65  trace_ptrt p,
66  const ai_domain_factory_baset &fac) const = 0;
67 
69  locationt l,
70  const ai_domain_factory_baset &fac) const = 0;
71 
74  virtual statet &
76 
78  virtual void clear()
79  {
80  return;
81  }
82 
89  virtual void prune(locationt l)
90  {
91  return;
92  }
93 };
94 
95 // There are a number of options for how to store the history objects.
96 // This implements a simple one. It is not in ai_storage_baset so that
97 // storage implementations can implement their own, more specific, approaches
99 {
100 protected:
101  typedef std::map<locationt, trace_set_ptrt> trace_mapt;
103 
104  // This retains one part of a shared_ptr to the history object
106  {
107  // Save the trace_ptrt
108  trace_mapt::iterator it = trace_map.find(p->current_location());
109  if(it == trace_map.end())
110  {
111  trace_set_ptrt s(new trace_sett());
112  auto ins = trace_map.emplace(p->current_location(), s);
113  CHECK_RETURN(ins.second);
114  it = ins.first;
115  }
116  // Strictly this should be "it->second points to a trace_set"
117  POSTCONDITION(it->second != nullptr);
118 
119  it->second->insert(p);
120 
121  return;
122  }
123 
124 public:
126  {
127  trace_mapt::const_iterator it = trace_map.find(l);
128  if(it == trace_map.end())
129  return trace_set_ptrt(new trace_sett());
130 
131  // Strictly this should be "it->second points to a trace_set"
132  POSTCONDITION(it->second != nullptr);
133  return it->second;
134  }
135 
136  void clear() override
137  {
139  trace_map.clear();
140  return;
141  }
142 };
143 
144 // A couple of older domains make direct use of the state map
146 class dependence_grapht;
147 
150 {
151 protected:
153  typedef std::unordered_map<
154  locationt,
155  state_ptrt,
160 
161  // Support some older domains that explicitly iterate across the state map
164  state_mapt &internal(void)
165  {
166  return state_map;
167  }
168 
169 public:
171  trace_ptrt p,
172  const ai_domain_factory_baset &fac) const override
173  {
174  return abstract_state_before(p->current_location(), fac);
175  }
176 
178  locationt l,
179  const ai_domain_factory_baset &fac) const override
180  {
181  typename state_mapt::const_iterator it = state_map.find(l);
182  if(it == state_map.end())
183  return fac.make(l);
184 
185  return it->second;
186  }
187 
189  {
190  register_trace(p);
191  return get_state(p->current_location(), fac);
192  }
193 
194  // For backwards compatability
195  // Care should be exercised in using this. It is possible to create domains
196  // without any corresponding history object(s). This can lead to somewhat
197  // unexpected behaviour depending on which APIs you use.
198  DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
200  {
201  typename state_mapt::const_iterator it = state_map.find(l);
202  if(it == state_map.end())
203  {
204  std::shared_ptr<statet> d(fac.make(l));
205  auto p = state_map.emplace(l, d);
206  CHECK_RETURN(p.second);
207  it = p.first;
208  }
209 
210  return *(it->second);
211  }
212 
213  void clear() override
214  {
216  state_map.clear();
217  return;
218  }
219 };
220 
221 // The most precise form of storage
223 {
224 protected:
225  typedef std::map<trace_ptrt, state_ptrt, ai_history_baset::compare_historyt>
228 
229 public:
231  trace_ptrt p,
232  const ai_domain_factory_baset &fac) const override
233  {
234  auto it = domain_map.find(p);
235  if(it == domain_map.end())
236  return fac.make(p->current_location());
237 
238  return it->second;
239  }
240 
242  locationt t,
243  const ai_domain_factory_baset &fac) const override
244  {
245  auto traces = abstract_traces_before(t);
246 
247  if(traces->size() == 0)
248  {
249  return fac.make(t);
250  }
251  else if(traces->size() == 1)
252  {
253  auto it = domain_map.find(*(traces->begin()));
255  it != domain_map.end(), "domain_map must be in sync with trace_map");
256  return it->second;
257  }
258  else
259  {
260  // Need to merge all of the traces that reach this location
261  auto res = fac.make(t);
262 
263  for(auto p : *traces)
264  {
265  auto it = domain_map.find(p);
267  it != domain_map.end(), "domain_map must be in sync with trace_map");
268  fac.merge(*res, *(it->second), p, p);
269  }
270 
271  return cstate_ptrt(res.release());
272  }
273  }
274 
276  {
277  register_trace(p);
278 
279  auto it = domain_map.find(p);
280  if(it == domain_map.end())
281  {
282  std::shared_ptr<statet> d(fac.make(p->current_location()));
283  auto jt = domain_map.emplace(p, d);
284  CHECK_RETURN(jt.second);
285  it = jt.first;
286  }
287 
288  return *(it->second);
289  }
290 
291  void clear() override
292  {
294  domain_map.clear();
295  return;
296  }
297 };
298 
299 #endif
trace_map_storaget::clear
void clear() override
Reset the abstract state.
Definition: ai_storage.h:136
location_sensitive_storaget::invariant_propagationt
friend invariant_propagationt
Definition: ai_storage.h:162
history_sensitive_storaget::get_state
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:275
ai_domain_factory_baset::merge
virtual bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) const =0
ai_storage_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_storage.h:49
ai_storage_baset::abstract_state_before
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.
location_sensitive_storaget::dependence_grapht
friend dependence_grapht
Definition: ai_storage.h:163
ai_storage_baset::clear
virtual void clear()
Reset the abstract state.
Definition: ai_storage.h:78
history_sensitive_storaget
Definition: ai_storage.h:223
dependence_grapht
Definition: dependence_graph.h:217
trace_map_storaget
Definition: ai_storage.h:99
ai_domain.h
Abstract Interpretation Domain.
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
ai_storage_baset::locationt
goto_programt::const_targett locationt
Definition: ai_storage.h:53
location_sensitive_storaget::abstract_state_before
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:170
history_sensitive_storaget::domain_map
domain_mapt domain_map
Definition: ai_storage.h:227
ai_domain_factory_baset::make
virtual std::unique_ptr< statet > make(locationt l) const =0
history_sensitive_storaget::clear
void clear() override
Reset the abstract state.
Definition: ai_storage.h:291
pointee_address_equalt
Functor to check whether iterators from different collections point at the same object.
Definition: goto_program.h:1164
ai_domain_factory_baset
Definition: ai_domain.h:189
ai_storage_baset::trace_set_ptrt
std::shared_ptr< trace_sett > trace_set_ptrt
Definition: ai_storage.h:51
ai_storage_baset::tracet
ai_history_baset tracet
Definition: ai_storage.h:48
location_sensitive_storaget::get_state
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:188
ai_history_baset::trace_sett
std::set< trace_ptrt, compare_historyt > trace_sett
Definition: ai_history.h:79
location_sensitive_storaget::abstract_state_before
cstate_ptrt abstract_state_before(locationt l, const ai_domain_factory_baset &fac) const override
Definition: ai_storage.h:177
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
trace_map_storaget::abstract_traces_before
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:125
ai_storage_baset::ctrace_set_ptrt
std::shared_ptr< const trace_sett > ctrace_set_ptrt
Definition: ai_storage.h:52
ai_storage_baset::state_ptrt
std::shared_ptr< statet > state_ptrt
Definition: ai_storage.h:46
history_sensitive_storaget::abstract_state_before
cstate_ptrt abstract_state_before(locationt t, const ai_domain_factory_baset &fac) const override
Definition: ai_storage.h:241
ai_storage_baset::statet
ai_domain_baset statet
Definition: ai_storage.h:45
history_sensitive_storaget::abstract_state_before
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:230
trace_map_storaget::trace_mapt
std::map< locationt, trace_set_ptrt > trace_mapt
Definition: ai_storage.h:101
ai_storage_baset::ai_storage_baset
ai_storage_baset()
Definition: ai_storage.h:36
const_target_hash
Definition: goto_program.h:1152
ai_storage_baset::~ai_storage_baset
virtual ~ai_storage_baset()
Definition: ai_storage.h:41
ai_storage_baset::get_state
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.
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
location_sensitive_storaget
The most conventional storage; one domain per location.
Definition: ai_storage.h:150
goto_program.h
Concrete Goto Program.
ai_storage_baset::abstract_state_before
virtual cstate_ptrt abstract_state_before(locationt l, const ai_domain_factory_baset &fac) const =0
ai_history.h
Abstract Interpretation history.
ai_storage_baset::prune
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:89
location_sensitive_storaget::state_mapt
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:158
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
ai_history_baset
A history object is an abstraction / representation of the control-flow part of a set of traces.
Definition: ai_history.h:37
ai_history_baset::trace_ptrt
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
ai_storage_baset::cstate_ptrt
std::shared_ptr< const statet > cstate_ptrt
Definition: ai_storage.h:47
ai_storage_baset::trace_sett
ai_history_baset::trace_sett trace_sett
Definition: ai_storage.h:50
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
invariant_propagationt
Definition: invariant_propagation.h:24
trace_map_storaget::register_trace
void register_trace(trace_ptrt p)
Definition: ai_storage.h:105
location_sensitive_storaget::state_map
state_mapt state_map
Definition: ai_storage.h:159
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
ai_storage_baset
This is the basic interface for storing domains.
Definition: ai_storage.h:34
trace_map_storaget::trace_map
trace_mapt trace_map
Definition: ai_storage.h:102
location_sensitive_storaget::clear
void clear() override
Reset the abstract state.
Definition: ai_storage.h:213
ai_storage_baset::abstract_traces_before
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const =0
Returns all of the histories that have reached the start of the instruction.
history_sensitive_storaget::domain_mapt
std::map< trace_ptrt, state_ptrt, ai_history_baset::compare_historyt > domain_mapt
Definition: ai_storage.h:226