cprover
Loading...
Searching...
No Matches
static_lifetime_init.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
12
13#include <util/arith_tools.h>
14#include <util/c_types.h>
16#include <util/namespace.h>
17#include <util/prefix.h>
18#include <util/std_code.h>
19#include <util/symbol_table.h>
20
21#include <set>
22
24static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
25{
26 const namespacet ns(symbol_table);
27 const symbolt &symbol = ns.lookup(identifier);
28
29 if(!symbol.is_static_lifetime)
30 return {};
31
32 if(symbol.is_type || symbol.is_macro)
33 return {};
34
35 // special values
36 if(
37 identifier == CPROVER_PREFIX "constant_infinity_uint" ||
38 identifier == CPROVER_PREFIX "memory" || identifier == "__func__" ||
39 identifier == "__FUNCTION__" || identifier == "__PRETTY_FUNCTION__" ||
40 identifier == "argc'" || identifier == "argv'" || identifier == "envp'" ||
41 identifier == "envp_size'")
42 return {};
43
44 // just for linking
45 if(has_prefix(id2string(identifier), CPROVER_PREFIX "architecture_"))
46 return {};
47
48 const typet &type = ns.follow(symbol.type);
49
50 // check type
51 if(type.id() == ID_code || type.id() == ID_empty)
52 return {};
53
54 if(type.id() == ID_array && to_array_type(type).size().is_nil())
55 {
56 // C standard 6.9.2, paragraph 5
57 // adjust the type to an array of size 1
58 symbolt &writable_symbol = symbol_table.get_writeable_ref(identifier);
59 writable_symbol.type = type;
60 writable_symbol.type.set(ID_size, from_integer(1, size_type()));
61 }
62
63 if(
64 (type.id() == ID_struct || type.id() == ID_union) &&
65 to_struct_union_type(type).is_incomplete())
66 {
67 return {}; // do not initialize
68 }
69
70 exprt rhs;
71
72 if((symbol.value.is_nil() && symbol.is_extern) ||
73 symbol.value.id() == ID_nondet)
74 {
75 if(symbol.value.get_bool(ID_C_no_nondet_initialization))
76 return {};
77
78 // Nondet initialise if not linked, or if explicitly requested.
79 // Compilers would usually complain about the unlinked symbol case.
80 const auto nondet = nondet_initializer(symbol.type, symbol.location, ns);
81 CHECK_RETURN(nondet.has_value());
82 rhs = *nondet;
83 }
84 else if(symbol.value.is_nil())
85 {
86 const auto zero = zero_initializer(symbol.type, symbol.location, ns);
87 CHECK_RETURN(zero.has_value());
88 rhs = *zero;
89 }
90 else
91 rhs = symbol.value;
92
93 code_assignt code(symbol.symbol_expr(), rhs);
94 code.add_source_location() = symbol.location;
95
96 return std::move(code);
97}
98
100 symbol_tablet &symbol_table,
101 const source_locationt &source_location)
102{
104
105 const namespacet ns(symbol_table);
106
108
109 init_symbol.value=code_blockt();
110 init_symbol.value.add_source_location()=source_location;
111
113
114 // add the magic label to hide
115 dest.add(code_labelt(CPROVER_PREFIX "HIDE", code_skipt()));
116
117 // do assignments based on "value"
118
119 // sort alphabetically for reproducible results
120 std::set<std::string> symbols;
121
122 for(const auto &symbol_pair : symbol_table.symbols)
123 {
124 symbols.insert(id2string(symbol_pair.first));
125 }
126
127 // first do framework variables
128 for(const std::string &id : symbols)
130 {
131 auto code = static_lifetime_init(id, symbol_table);
132 if(code.has_value())
133 dest.add(std::move(*code));
134 }
135
136 // now all other variables
137 for(const std::string &id : symbols)
138 if(!has_prefix(id, CPROVER_PREFIX))
139 {
140 auto code = static_lifetime_init(id, symbol_table);
141 if(code.has_value())
142 dest.add(std::move(*code));
143 }
144
145 // now call designated "initialization" functions
146
147 for(const std::string &id : symbols)
148 {
149 const symbolt &symbol=ns.lookup(id);
150
151 if(symbol.type.id() != ID_code)
152 continue;
153
154 const code_typet &code_type = to_code_type(symbol.type);
155 if(
156 code_type.return_type().id() == ID_constructor &&
157 code_type.parameters().empty())
158 {
159 code_function_callt function_call(symbol.symbol_expr());
160 function_call.add_source_location()=source_location;
161 dest.add(function_call);
162 }
163 }
164}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
unsignedbv_typet size_type()
Definition: c_types.cpp:68
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
codet representation of a function call statement.
codet representation of a label for branch targets.
Definition: std_code.h:959
A codet representing a skip statement.
Definition: std_code.h:322
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
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
source_locationt & add_source_location()
Definition: expr.h:235
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
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
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
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
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
Symbol table entry.
Definition: symbol.h:28
bool is_extern
Definition: symbol.h:66
bool is_macro
Definition: symbol.h:61
bool is_static_lifetime
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
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
exprt value
Initial value of symbol.
Definition: symbol.h:34
The type of an expression, extends irept.
Definition: type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
optionalt< exprt > nondet_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create a non-deterministic value for type type, with all subtypes independently expanded as non-deter...
Expression Initialization.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static std::unordered_set< irep_idt > init_symbol(const symbolt &sym, code_blockt &code_block, symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
nonstd::optional< T > optionalt
Definition: optional.h:35
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
static optionalt< codet > static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
#define INITIALIZE_FUNCTION
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
const codet & to_code(const exprt &expr)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
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.