cprover
nondet_static.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: 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 
8 Author: Daniel Kroening, Michael Tautschnig
9 
10 Date: November 2011
11 
12 \*******************************************************************/
13 
19 
20 #include "nondet_static.h"
21 
22 #include <util/prefix.h>
23 
25 
27 
34  const symbol_exprt &symbol_expr,
35  const namespacet &ns)
36 {
37  const irep_idt &id = symbol_expr.get_identifier();
38 
39  // is it a __CPROVER_* variable?
41  return false;
42 
43  // variable not in symbol table such as symex variable?
44  if(!ns.get_symbol_table().has_symbol(id))
45  return false;
46 
47  const symbolt &symbol = ns.lookup(id);
48 
49  // is the symbol explicitly marked as not to be nondet initialized?
50  if(symbol.value.get_bool(ID_C_no_nondet_initialization))
51  {
52  return false;
53  }
54 
55  // is the type explicitly marked as not to be nondet initialized?
56  if(symbol.type.get_bool(ID_C_no_nondet_initialization))
57  return false;
58 
59  // is the type explicitly marked as not to be initialized?
60  if(symbol.type.get_bool(ID_C_no_initialization_required))
61  return false;
62 
63  // static lifetime?
64  if(!symbol.is_static_lifetime)
65  return false;
66 
67  // constant?
68  return !is_constant_or_has_constant_components(symbol_expr.type(), ns) &&
70 }
71 
80  const namespacet &ns,
81  goto_functionst &goto_functions,
82  const irep_idt &fct_name)
83 {
84  goto_functionst::function_mapt::iterator fct_entry =
85  goto_functions.function_map.find(fct_name);
86  CHECK_RETURN(fct_entry != goto_functions.function_map.end());
87 
88  goto_programt &init = fct_entry->second.body;
89 
90  for(auto &instruction : init.instructions)
91  {
92  if(instruction.is_assign())
93  {
94  const symbol_exprt sym =
95  to_symbol_expr(as_const(instruction).get_assign().lhs());
96 
98  {
99  const auto source_location = instruction.source_location;
100  instruction = goto_programt::make_assignment(
101  code_assignt(
102  sym, side_effect_expr_nondett(sym.type(), source_location)),
103  source_location);
104  }
105  }
106  else if(instruction.is_function_call())
107  {
108  const code_function_callt &fct = instruction.get_function_call();
109  const symbol_exprt &fsym=to_symbol_expr(fct.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 
124 void nondet_static(const namespacet &ns, goto_functionst &goto_functions)
125 {
126  nondet_static(ns, goto_functions, INITIALIZE_FUNCTION);
127 }
128 
134 void 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  }
192 
194 }
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
symbolt::display_name
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
prefix.h
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
optionst::value_listt
std::list< std::string > value_listt
Definition: options.h:25
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
nondet_static.h
Nondeterministically initializes global scope variables, except for constants (such as string literal...
nondet_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.
Definition: nondet_static.cpp:79
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1008
symbol_tablet::begin
virtual iteratort begin() override
Definition: symbol_table.h:114
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:141
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
is_nondet_initializable_static
bool is_nondet_initializable_static(const symbol_exprt &symbol_expr, const namespacet &ns)
See the return.
Definition: nondet_static.cpp:33
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
symbol_tablet::end
virtual iteratort end() override
Definition: symbol_table.h:118
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbol_table_baset::iteratort
Definition: symbol_table_base.h:155
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
is_constant_or_has_constant_components
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:175
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functionst::update
void update()
Definition: goto_functions.h:81
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
static_lifetime_init.h
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
code_function_callt::function
exprt & function()
Definition: std_code.h:1250