cprover
Loading...
Searching...
No Matches
local_may_alias.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-insensitive, location-sensitive may-alias analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
13#define CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
14
15#include <memory>
16#include <stack>
17
18#include <util/union_find.h>
19#include <util/make_unique.h>
20
21#include "locals.h"
22#include "dirty.h"
23#include "local_cfg.h"
24
26{
27public:
29
38
39 void output(
40 std::ostream &out,
41 const goto_functiont &goto_function,
42 const namespacet &ns) const;
43
47
48 // given a pointer, returns possible aliases
49 std::set<exprt> get(
51 const exprt &src) const;
52
53 // returns 'true' when pointers src1 and src2 may be aliases
54 bool aliases(
56 const exprt &src1, const exprt &src2) const;
57
58protected:
59 void build(const goto_functiont &goto_function);
60
61 typedef std::stack<local_cfgt::node_nrt> work_queuet;
62
64
66
67 // the information tracked per program location
69 {
70 public:
72
73 bool merge(const loc_infot &src);
74 };
75
76 typedef std::vector<loc_infot> loc_infost;
78
79 void assign_lhs(
80 const exprt &lhs,
81 const exprt &rhs,
84
85 typedef std::set<unsigned> object_sett;
86
87 void get_rec(
89 const exprt &rhs,
90 const loc_infot &loc_info_src) const;
91
93};
94
96{
97public:
101
103 {
105
106 for(const auto &gf_entry : _goto_functions.function_map)
107 {
109 target_map[i_it] = gf_entry.first;
110 }
111 }
112
114 {
116 fkt_mapt::iterator f_it=fkt_map.find(fkt);
117 if(f_it!=fkt_map.end())
118 return *f_it->second;
119
120 goto_functionst::function_mapt::const_iterator f_it2=
121 goto_functions->function_map.find(fkt);
123 return *(fkt_map[fkt]=util_make_unique<local_may_aliast>(f_it2->second));
124 }
125
127 {
128 target_mapt::const_iterator t_it=
129 target_map.find(t);
130 assert(t_it!=target_map.end());
131 return operator()(t_it->second);
132 }
133
134 std::set<exprt> get(
136 const exprt &src) const;
137
138protected:
140 typedef std::map<irep_idt, std::unique_ptr<local_may_aliast> > fkt_mapt;
142
143 typedef std::map<goto_programt::const_targett, irep_idt > target_mapt;
145};
146
147#endif // CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition dirty.h:27
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.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
instructionst::const_iterator const_targett
local_may_aliast & operator()(const irep_idt &fkt)
local_may_aliast & operator()(goto_programt::const_targett t)
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
void operator()(const goto_functionst &_goto_functions)
std::map< irep_idt, std::unique_ptr< local_may_aliast > > fkt_mapt
std::map< goto_programt::const_targett, irep_idt > target_mapt
const goto_functionst * goto_functions
bool merge(const loc_infot &src)
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
void build(const goto_functiont &goto_function)
numberingt< exprt, irep_hash > objects
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
void get_rec(object_sett &dest, const exprt &rhs, const loc_infot &loc_info_src) const
std::stack< local_cfgt::node_nrt > work_queuet
std::vector< loc_infot > loc_infost
local_may_aliast(const goto_functiont &_goto_function)
unsigned_union_find alias_sett
bool aliases(const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const
std::set< unsigned > object_sett
goto_functionst::goto_functiont goto_functiont
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Variables whose address is taken.
#define forall_goto_program_instructions(it, program)
CFG for One Function.
Local variables whose address is taken.
#define PRECONDITION(CONDITION)
Definition invariant.h:463