cprover
Loading...
Searching...
No Matches
nondet_static.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Nondeterministically initializes global scope variables, except for
4 constants (such as string literals, final fields) and internal variables
5 (such as CPROVER and symex variables, language specific internal
6 variables).
7
8Author: Daniel Kroening, Michael Tautschnig
9
10Date: November 2011
11
12\*******************************************************************/
13
19
20#include "nondet_static.h"
21
22#include <util/prefix.h>
23#include <util/std_code.h>
24
26
28
29#include <regex>
30
37 const symbol_exprt &symbol_expr,
38 const namespacet &ns)
39{
40 const irep_idt &id = symbol_expr.get_identifier();
41
42 // is it a __CPROVER_* variable?
44 return false;
45
46 // variable not in symbol table such as symex variable?
47 if(!ns.get_symbol_table().has_symbol(id))
48 return false;
49
50 const symbolt &symbol = ns.lookup(id);
51
52 // is the symbol explicitly marked as not to be nondet initialized?
53 if(symbol.value.get_bool(ID_C_no_nondet_initialization))
54 {
55 return false;
56 }
57
58 // is the type explicitly marked as not to be nondet initialized?
59 if(symbol.type.get_bool(ID_C_no_nondet_initialization))
60 return false;
61
62 // is the type explicitly marked as not to be initialized?
63 if(symbol.type.get_bool(ID_C_no_initialization_required))
64 return false;
65
66 // static lifetime?
67 if(!symbol.is_static_lifetime)
68 return false;
69
70 // constant?
71 return !is_constant_or_has_constant_components(symbol_expr.type(), ns) &&
73}
74
82static void nondet_static(
83 const namespacet &ns,
84 goto_functionst &goto_functions,
85 const irep_idt &fct_name)
86{
87 goto_functionst::function_mapt::iterator fct_entry =
88 goto_functions.function_map.find(fct_name);
89 CHECK_RETURN(fct_entry != goto_functions.function_map.end());
90
91 goto_programt &init = fct_entry->second.body;
92
93 for(auto &instruction : init.instructions)
94 {
95 if(instruction.is_assign())
96 {
97 const symbol_exprt sym =
98 to_symbol_expr(as_const(instruction).assign_lhs());
99
101 {
102 const auto source_location = instruction.source_location();
103 instruction = goto_programt::make_assignment(
105 sym, side_effect_expr_nondett(sym.type(), source_location)),
106 source_location);
107 }
108 }
109 else if(instruction.is_function_call())
110 {
111 const symbol_exprt &fsym = to_symbol_expr(instruction.call_function());
112
113 // see cpp/cpp_typecheck.cpp, which creates initialization functions
114 if(has_prefix(
115 id2string(fsym.get_identifier()), "#cpp_dynamic_initialization#"))
116 {
117 nondet_static(ns, goto_functions, fsym.get_identifier());
118 }
119 }
120 }
121
122 // update counters etc.
123 goto_functions.update();
124}
125
130void nondet_static(const namespacet &ns, goto_functionst &goto_functions)
131{
132 nondet_static(ns, goto_functions, INITIALIZE_FUNCTION);
133}
134
140void nondet_static(goto_modelt &goto_model)
141{
142 const namespacet ns(goto_model.symbol_table);
143 nondet_static(ns, goto_model.goto_functions);
144}
145
153 goto_modelt &goto_model,
154 const std::set<std::string> &except_values)
155{
156 const namespacet ns(goto_model.symbol_table);
157 std::set<std::string> to_exclude;
158
159 for(auto const &except : except_values)
160 {
161 const bool file_prefix_found = except.find(":") != std::string::npos;
162
163 if(file_prefix_found)
164 {
165 to_exclude.insert(except);
166 if(has_prefix(except, "./"))
167 {
168 to_exclude.insert(except.substr(2, except.length() - 2));
169 }
170 else
171 {
172 to_exclude.insert("./" + except);
173 }
174 }
175 else
176 {
177 irep_idt symbol_name(except);
178 symbolt lookup_results = ns.lookup(symbol_name);
179 to_exclude.insert(
180 id2string(lookup_results.location.get_file()) + ":" + except);
181 }
182 }
183
184 symbol_tablet &symbol_table = goto_model.symbol_table;
185
186 for(symbol_tablet::iteratort symbol_it = symbol_table.begin();
187 symbol_it != symbol_table.end();
188 symbol_it++)
189 {
190 symbolt &symbol = symbol_it.get_writeable_symbol();
191 std::string qualified_name = id2string(symbol.location.get_file()) + ":" +
192 id2string(symbol.display_name());
193 if(to_exclude.find(qualified_name) != to_exclude.end())
194 {
195 symbol.value.set(ID_C_no_nondet_initialization, 1);
196 }
197 else if(is_nondet_initializable_static(symbol.symbol_expr(), ns))
198 {
199 symbol.value = side_effect_expr_nondett(symbol.type, symbol.location);
200 }
201 }
202
204}
205
212void nondet_static_matching(goto_modelt &goto_model, const std::string &regex)
213{
214 const auto regex_matcher = std::regex(regex);
215 symbol_tablet &symbol_table = goto_model.symbol_table;
216
217 for(symbol_tablet::iteratort symbol_it = symbol_table.begin();
218 symbol_it != symbol_table.end();
219 symbol_it++)
220 {
221 symbolt &symbol = symbol_it.get_writeable_symbol();
222 std::string qualified_name = id2string(symbol.location.get_file()) + ":" +
223 id2string(symbol.display_name());
224 if(!std::regex_match(qualified_name, regex_matcher))
225 {
226 symbol.value.set(ID_C_no_nondet_initialization, 1);
227 }
228 }
229
230 const namespacet ns(goto_model.symbol_table);
232}
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
A goto_instruction_codet representing an assignment in the program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
typet & type()
Return the type of the expression.
Definition expr.h:84
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
const irep_idt & get_file() const
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
virtual iteratort begin() override
virtual iteratort end() override
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
exprt value
Initial value of symbol.
Definition symbol.h:34
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
void nondet_static_matching(goto_modelt &goto_model, const std::string &regex)
Nondeterministically initializes global scope variables that match the given regex.
bool is_nondet_initializable_static(const symbol_exprt &symbol_expr, const namespacet &ns)
See the return.
static void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify whether a given type is constant itself or contains constant components.