CBMC
local_may_alias.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive may-alias analysis
4 
5 Author: 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 
20 #include "locals.h"
21 #include "dirty.h"
22 #include "local_cfg.h"
23 
25 {
26 public:
28 
29  explicit local_may_aliast(
30  const goto_functiont &_goto_function):
31  dirty(_goto_function),
32  locals(_goto_function),
33  cfg(_goto_function.body)
34  {
35  build(_goto_function);
36  }
37 
38  void output(
39  std::ostream &out,
40  const goto_functiont &goto_function,
41  const namespacet &ns) const;
42 
46 
47  // given a pointer, returns possible aliases
48  std::set<exprt> get(
50  const exprt &src) const;
51 
52  // returns 'true' when pointers src1 and src2 may be aliases
53  bool aliases(
55  const exprt &src1, const exprt &src2) const;
56 
57 protected:
58  void build(const goto_functiont &goto_function);
59 
60  typedef std::stack<local_cfgt::node_nrt> work_queuet;
61 
63 
65 
66  // the information tracked per program location
67  class loc_infot
68  {
69  public:
71 
72  bool merge(const loc_infot &src);
73  };
74 
75  typedef std::vector<loc_infot> loc_infost;
77 
78  void assign_lhs(
79  const exprt &lhs,
80  const exprt &rhs,
81  const loc_infot &loc_info_src,
82  loc_infot &loc_info_dest);
83 
84  typedef std::set<unsigned> object_sett;
85 
86  void get_rec(
87  object_sett &dest,
88  const exprt &rhs,
89  const loc_infot &loc_info_src) const;
90 
91  unsigned unknown_object;
92 };
93 
95 {
96 public:
98  {
99  }
100 
101  void operator()(const goto_functionst &_goto_functions)
102  {
103  goto_functions=&_goto_functions;
104 
105  for(const auto &gf_entry : _goto_functions.function_map)
106  {
107  forall_goto_program_instructions(i_it, gf_entry.second.body)
108  target_map[i_it] = gf_entry.first;
109  }
110  }
111 
113  {
114  PRECONDITION(goto_functions!=nullptr);
115  fkt_mapt::iterator f_it=fkt_map.find(fkt);
116  if(f_it!=fkt_map.end())
117  return *f_it->second;
118 
119  goto_functionst::function_mapt::const_iterator f_it2=
120  goto_functions->function_map.find(fkt);
121  CHECK_RETURN(f_it2 != goto_functions->function_map.end());
122  return *(fkt_map[fkt] = std::make_unique<local_may_aliast>(f_it2->second));
123  }
124 
126  {
127  target_mapt::const_iterator t_it=
128  target_map.find(t);
129  CHECK_RETURN(t_it != target_map.end());
130  return operator()(t_it->second);
131  }
132 
133  std::set<exprt> get(
135  const exprt &src) const;
136 
137 protected:
139  typedef std::map<irep_idt, std::unique_ptr<local_may_aliast> > fkt_mapt;
141 
142  typedef std::
143  map<goto_programt::const_targett, irep_idt, goto_programt::target_less_than>
146 };
147 
148 #endif // CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:28
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 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...
Definition: goto_function.h:24
instructionst::const_iterator const_targett
Definition: goto_program.h:615
local_may_aliast & operator()(goto_programt::const_targett t)
local_may_aliast & operator()(const irep_idt &fkt)
std::map< goto_programt::const_targett, irep_idt, goto_programt::target_less_than > target_mapt
void operator()(const goto_functionst &_goto_functions)
std::map< irep_idt, std::unique_ptr< local_may_aliast > > fkt_mapt
const goto_functionst * goto_functions
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
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)
unsigned unknown_object
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
loc_infost loc_infos
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
Definition: locals.h:25
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Variables whose address is taken.
#define forall_goto_program_instructions(it, program)
CFG for One Function.
Local variables whose address is taken.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463