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/pointer_expr.h>
16#include <util/symbol_table.h>
17
19 const goto_programt &goto_program)
20{
21 baset::initialize(goto_program);
22 add_vars(goto_program);
23}
24
26 const goto_functionst &goto_functions)
27{
28 baset::initialize(goto_functions);
29 add_vars(goto_functions);
30}
31
33 const goto_programt &goto_program)
34{
35 typedef std::list<value_set_fit::entryt> entry_listt;
36
37 // get the globals
40
41 // get the locals
43 goto_program.get_decl_identifiers(locals);
44
45 // cache the list for the locals to speed things up
46 typedef std::unordered_map<irep_idt, entry_listt> entry_cachet;
48
50
51 for(goto_programt::instructionst::const_iterator
52 i_it=goto_program.instructions.begin();
53 i_it!=goto_program.instructions.end();
54 i_it++)
55 {
57
58 for(goto_programt::decl_identifierst::const_iterator
59 l_it=locals.begin();
60 l_it!=locals.end();
61 l_it++)
62 {
63 // cache hit?
64 entry_cachet::const_iterator e_it=entry_cache.find(*l_it);
65
66 if(e_it==entry_cache.end())
67 {
68 const symbolt &symbol=ns.lookup(*l_it);
69
70 std::list<value_set_fit::entryt> &entries=entry_cache[*l_it];
71 get_entries(symbol, entries);
72 v.add_vars(entries);
73 }
74 else
75 v.add_vars(e_it->second);
76 }
77 }
78}
79
81 const symbolt &symbol,
82 std::list<value_set_fit::entryt> &dest)
83{
84 get_entries_rec(symbol.name, "", symbol.type, dest);
85}
86
88 const irep_idt &identifier,
89 const std::string &suffix,
90 const typet &type,
91 std::list<value_set_fit::entryt> &dest)
92{
93 const typet &t=ns.follow(type);
94
95 if(t.id()==ID_struct ||
96 t.id()==ID_union)
97 {
98 for(const auto &c : to_struct_union_type(t).components())
99 {
101 identifier, suffix + "." + id2string(c.get_name()), c.type(), dest);
102 }
103 }
104 else if(t.id()==ID_array)
105 {
107 identifier, suffix + "[]", to_array_type(t).element_type(), dest);
108 }
109 else if(check_type(t))
110 {
111 dest.push_back(value_set_fit::entryt(identifier, suffix));
112 }
113}
114
116 const goto_functionst &goto_functions)
117{
118 // get the globals
119 std::list<value_set_fit::entryt> globals;
121
123 v.add_vars(globals);
124
125 for(const auto &gf_entry : goto_functions.function_map)
126 {
127 // get the locals
128 std::set<irep_idt> locals;
129 get_local_identifiers(gf_entry.second, locals);
130
131 for(auto l : locals)
132 {
133 const symbolt &symbol=ns.lookup(l);
134
135 std::list<value_set_fit::entryt> entries;
136 get_entries(symbol, entries);
137 v.add_vars(entries);
138 }
139 }
140}
141
143 std::list<value_set_fit::entryt> &dest)
144{
145 // static ones
146 for(const auto &symbol_pair : ns.get_symbol_table().symbols)
147 {
148 if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
149 {
151 }
152 }
153}
154
156{
157 if(type.id()==ID_pointer)
158 {
159 switch(track_options)
160 {
162 { return true; break; }
164 {
165 if(type.id()==ID_pointer)
166 {
167 const typet *t = &type;
168 while(t->id() == ID_pointer)
169 t = &(to_pointer_type(*t).base_type());
170
171 return (t->id()==ID_code);
172 }
173
174 break;
175 }
176 default: // don't track.
177 break;
178 }
179 }
180 else if(type.id()==ID_struct ||
181 type.id()==ID_union)
182 {
183 for(const auto &c : to_struct_union_type(type).components())
184 {
185 if(check_type(c.type()))
186 return true;
187 }
188 }
189 else if(type.id()==ID_array)
190 return check_type(to_array_type(type).element_type());
191 else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
192 return check_type(ns.follow(type));
193
194 return false;
195}
196
198 const irep_idt &function_id,
200 const exprt &expr)
201{
203 state.value_set.function_numbering.number(function_id);
205 state.value_set.function_numbering.number(function_id);
206 state.value_set.from_target_index = l->location_number;
207 state.value_set.to_target_index = l->location_number;
208 return state.value_set.get_value_set(expr, ns);
209}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:777
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
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
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:832
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)