cprover
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
35 const symbol_exprt &symbol_expr,
36 const namespacet &ns)
37{
38 const irep_idt &id = symbol_expr.get_identifier();
39
40 // is it a __CPROVER_* variable?
42 return false;
43
44 // variable not in symbol table such as symex variable?
45 if(!ns.get_symbol_table().has_symbol(id))
46 return false;
47
48 const symbolt &symbol = ns.lookup(id);
49
50 // is the symbol explicitly marked as not to be nondet initialized?
51 if(symbol.value.get_bool(ID_C_no_nondet_initialization))
52 {
53 return false;
54 }
55
56 // is the type explicitly marked as not to be nondet initialized?
57 if(symbol.type.get_bool(ID_C_no_nondet_initialization))
58 return false;
59
60 // is the type explicitly marked as not to be initialized?
61 if(symbol.type.get_bool(ID_C_no_initialization_required))
62 return false;
63
64 // static lifetime?
65 if(!symbol.is_static_lifetime)
66 return false;
67
68 // constant?
69 return !is_constant_or_has_constant_components(symbol_expr.type(), ns) &&
71}
72
80static void nondet_static(
81 const namespacet &ns,
82 goto_functionst &goto_functions,
83 const irep_idt &fct_name)
84{
85 goto_functionst::function_mapt::iterator fct_entry =
86 goto_functions.function_map.find(fct_name);
87 CHECK_RETURN(fct_entry != goto_functions.function_map.end());
88
89 goto_programt &init = fct_entry->second.body;
90
91 for(auto &instruction : init.instructions)
92 {
93 if(instruction.is_assign())
94 {
95 const symbol_exprt sym =
96 to_symbol_expr(as_const(instruction).assign_lhs());
97
99 {
100 const auto source_location = instruction.source_location();
101 instruction = goto_programt::make_assignment(
103 sym, side_effect_expr_nondett(sym.type(), source_location)),
104 source_location);
105 }
106 }
107 else if(instruction.is_function_call())
108 {
109 const symbol_exprt &fsym = to_symbol_expr(instruction.call_function());
110
111 if(has_prefix(id2string(fsym.get_identifier()), "#ini#"))
112 nondet_static(ns, goto_functions, fsym.get_identifier());
113 }
114 }
115
116 // update counters etc.
117 goto_functions.update();
118}
119
124void nondet_static(const namespacet &ns, goto_functionst &goto_functions)
125{
126 nondet_static(ns, goto_functions, INITIALIZE_FUNCTION);
127}
128
134void nondet_static(goto_modelt &goto_model)
135{
136 const namespacet ns(goto_model.symbol_table);
137 nondet_static(ns, goto_model.goto_functions);
138}
139
147 goto_modelt &goto_model,
148 const optionst::value_listt &except_values)
149{
150 const namespacet ns(goto_model.symbol_table);
151 std::set<std::string> to_exclude;
152
153 for(auto const &except : except_values)
154 {
155 const bool file_prefix_found = except.find(":") != std::string::npos;
156
157 if(file_prefix_found)
158 {
159 to_exclude.insert(except);
160 if(has_prefix(except, "./"))
161 {
162 to_exclude.insert(except.substr(2, except.length() - 2));
163 }
164 else
165 {
166 to_exclude.insert("./" + except);
167 }
168 }
169 else
170 {
171 irep_idt symbol_name(except);
172 symbolt lookup_results = ns.lookup(symbol_name);
173 to_exclude.insert(
174 id2string(lookup_results.location.get_file()) + ":" + except);
175 }
176 }
177
178 symbol_tablet &symbol_table = goto_model.symbol_table;
179
180 for(symbol_tablet::iteratort symbol_it = symbol_table.begin();
181 symbol_it != symbol_table.end();
182 symbol_it++)
183 {
184 symbolt &symbol = symbol_it.get_writeable_symbol();
185 std::string qualified_name = id2string(symbol.location.get_file()) + ":" +
186 id2string(symbol.display_name());
187 if(to_exclude.find(qualified_name) != to_exclude.end())
188 {
189 symbol.value.set(ID_C_no_nondet_initialization, 1);
190 }
191 else if(is_nondet_initializable_static(symbol.symbol_expr(), ns))
192 {
193 symbol.value = side_effect_expr_nondett(symbol.type, symbol.location);
194 }
195 }
196
198}
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 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:37
typet & type()
Return the type of the expression.
Definition: expr.h:82
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
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:58
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().
Definition: namespace.cpp:138
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:123
std::list< std::string > value_listt
Definition: options.h:25
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:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
Definition: symbol_table.h:14
virtual iteratort begin() override
Definition: symbol_table.h:108
virtual iteratort end() override
Definition: symbol_table.h:112
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:65
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
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:189
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.
Definition: std_types.cpp:179