cprover
Loading...
Searching...
No Matches
value_set_analysis_fi.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set Propagation (Flow Insensitive)
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
14
15#include <util/namespace.h>
16#include <util/pointer_expr.h>
18
20 const goto_programt &goto_program)
21{
22 baset::initialize(goto_program);
23 add_vars(goto_program);
24}
25
27 const goto_functionst &goto_functions)
28{
29 baset::initialize(goto_functions);
30 add_vars(goto_functions);
31}
32
34 const goto_programt &goto_program)
35{
36 typedef std::list<value_set_fit::entryt> entry_listt;
37
38 // get the globals
39 entry_listt globals;
40 get_globals(globals);
41
42 // get the locals
44 goto_program.get_decl_identifiers(locals);
45
46 // cache the list for the locals to speed things up
47 typedef std::unordered_map<irep_idt, entry_listt> entry_cachet;
48 entry_cachet entry_cache;
49
51
52 for(goto_programt::instructionst::const_iterator
53 i_it=goto_program.instructions.begin();
54 i_it!=goto_program.instructions.end();
55 i_it++)
56 {
57 v.add_vars(globals);
58
59 for(goto_programt::decl_identifierst::const_iterator
60 l_it=locals.begin();
61 l_it!=locals.end();
62 l_it++)
63 {
64 // cache hit?
65 entry_cachet::const_iterator e_it=entry_cache.find(*l_it);
66
67 if(e_it==entry_cache.end())
68 {
69 const symbolt &symbol=ns.lookup(*l_it);
70
71 std::list<value_set_fit::entryt> &entries=entry_cache[*l_it];
72 get_entries(symbol, entries);
73 v.add_vars(entries);
74 }
75 else
76 v.add_vars(e_it->second);
77 }
78 }
79}
80
82 const symbolt &symbol,
83 std::list<value_set_fit::entryt> &dest)
84{
85 get_entries_rec(symbol.name, "", symbol.type, dest);
86}
87
89 const irep_idt &identifier,
90 const std::string &suffix,
91 const typet &type,
92 std::list<value_set_fit::entryt> &dest)
93{
94 const typet &t=ns.follow(type);
95
96 if(t.id()==ID_struct ||
97 t.id()==ID_union)
98 {
99 for(const auto &c : to_struct_union_type(t).components())
100 {
102 identifier, suffix + "." + id2string(c.get_name()), c.type(), dest);
103 }
104 }
105 else if(t.id()==ID_array)
106 {
108 identifier, suffix + "[]", to_array_type(t).element_type(), dest);
109 }
110 else if(check_type(t))
111 {
112 dest.push_back(value_set_fit::entryt(identifier, suffix));
113 }
114}
115
117 const goto_functionst &goto_functions)
118{
119 // get the globals
120 std::list<value_set_fit::entryt> globals;
121 get_globals(globals);
122
124 v.add_vars(globals);
125
126 for(const auto &gf_entry : goto_functions.function_map)
127 {
128 // get the locals
129 std::set<irep_idt> locals;
130 get_local_identifiers(gf_entry.second, locals);
131
132 for(auto l : locals)
133 {
134 const symbolt &symbol=ns.lookup(l);
135
136 std::list<value_set_fit::entryt> entries;
137 get_entries(symbol, entries);
138 v.add_vars(entries);
139 }
140 }
141}
142
144 std::list<value_set_fit::entryt> &dest)
145{
146 // static ones
147 for(const auto &symbol_pair : ns.get_symbol_table().symbols)
148 {
149 if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
150 {
151 get_entries(symbol_pair.second, dest);
152 }
153 }
154}
155
157{
158 if(type.id()==ID_pointer)
159 {
160 switch(track_options)
161 {
163 { return true; break; }
165 {
166 if(type.id()==ID_pointer)
167 {
168 const typet *t = &type;
169 while(t->id() == ID_pointer)
170 t = &(to_pointer_type(*t).base_type());
171
172 return (t->id()==ID_code);
173 }
174
175 break;
176 }
177 default: // don't track.
178 break;
179 }
180 }
181 else if(type.id()==ID_struct ||
182 type.id()==ID_union)
183 {
184 for(const auto &c : to_struct_union_type(type).components())
185 {
186 if(check_type(c.type()))
187 return true;
188 }
189 }
190 else if(type.id()==ID_array)
191 return check_type(to_array_type(type).element_type());
192 else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
193 return check_type(ns.follow(type));
194
195 return false;
196}
197
199 const irep_idt &function_id,
201 const exprt &expr)
202{
207 state.value_set.from_target_index = l->location_number;
208 state.value_set.to_target_index = l->location_number;
209 return state.value_set.get_value_set(expr, ns);
210}
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
goto_programt::const_targett locationt
virtual void initialize(const goto_programt &)
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
std::set< irep_idt > decl_identifierst
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
const irep_idt & id() const
Definition irep.h:396
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition namespace.h:123
number_type number(const key_type &a)
Definition numbering.h:37
const typet & base_type() const
The type of the data what we point to.
const componentst & components() const
Definition std_types.h:147
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition symbol.h:28
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
The type of an expression, extends irept.
Definition type.h:29
bool check_type(const typet &type)
std::vector< exprt > get_values(const irep_idt &function_id, locationt l, const exprt &expr) override
void get_entries(const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
void add_vars(const goto_functionst &goto_functions)
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
void get_globals(std::list< value_set_fit::entryt > &dest)
void initialize(const goto_programt &goto_program) override
static numberingt< irep_idt > function_numbering
void add_vars(const std::list< entryt > &vars)
std::vector< exprt > get_value_set(const exprt &expr, const namespacet &ns) const
unsigned from_function
unsigned to_function
unsigned from_target_index
unsigned to_target_index
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
Author: Diffblue Ltd.
Value Set Propagation (flow insensitive)