cprover
static_lifetime_init.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "static_lifetime_init.h"
10 
11 #include <cassert>
12 #include <cstdlib>
13 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/config.h>
17 #include <util/expr_initializer.h>
18 #include <util/namespace.h>
19 #include <util/prefix.h>
20 #include <util/std_code.h>
21 #include <util/std_expr.h>
22 
24 
26  symbol_tablet &symbol_table,
27  const source_locationt &source_location)
28 {
30 
31  const namespacet ns(symbol_table);
32 
33  symbolt &init_symbol = symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
34 
35  init_symbol.value=code_blockt();
36  init_symbol.value.add_source_location()=source_location;
37 
38  code_blockt &dest=to_code_block(to_code(init_symbol.value));
39 
40  // add the magic label to hide
41  dest.add(code_labelt(CPROVER_PREFIX "HIDE", code_skipt()));
42 
43  // do assignments based on "value"
44 
45  // sort alphabetically for reproducible results
46  std::set<std::string> symbols;
47 
48  for(const auto &symbol_pair : symbol_table.symbols)
49  {
50  symbols.insert(id2string(symbol_pair.first));
51  }
52 
53  for(const std::string &id : symbols)
54  {
55  const symbolt &symbol=ns.lookup(id);
56 
57  const irep_idt &identifier=symbol.name;
58 
59  if(!symbol.is_static_lifetime)
60  continue;
61 
62  if(symbol.is_type || symbol.is_macro)
63  continue;
64 
65  // special values
66  if(identifier==CPROVER_PREFIX "constant_infinity_uint" ||
67  identifier==CPROVER_PREFIX "memory" ||
68  identifier=="__func__" ||
69  identifier=="__FUNCTION__" ||
70  identifier=="__PRETTY_FUNCTION__" ||
71  identifier=="argc'" ||
72  identifier=="argv'" ||
73  identifier=="envp'" ||
74  identifier=="envp_size'")
75  continue;
76 
77  // just for linking
78  if(has_prefix(id, CPROVER_PREFIX "architecture_"))
79  continue;
80 
81  const typet &type=ns.follow(symbol.type);
82 
83  // check type
84  if(type.id()==ID_code ||
85  type.id()==ID_empty)
86  continue;
87 
88  // We won't try to initialize any symbols that have
89  // remained incomplete.
90 
91  if(symbol.value.is_nil() &&
92  symbol.is_extern)
93  // Compilers would usually complain about these
94  // symbols being undefined.
95  continue;
96 
97  if(type.id()==ID_array &&
98  to_array_type(type).size().is_nil())
99  {
100  // C standard 6.9.2, paragraph 5
101  // adjust the type to an array of size 1
102  symbolt &writable_symbol = *symbol_table.get_writeable(identifier);
103  writable_symbol.type = type;
104  writable_symbol.type.set(ID_size, from_integer(1, size_type()));
105  }
106 
107  if(type.id()==ID_incomplete_struct ||
108  type.id()==ID_incomplete_union)
109  continue; // do not initialize
110 
111  if(symbol.value.id()==ID_nondet)
112  continue; // do not initialize
113 
114  exprt rhs;
115 
116  if(symbol.value.is_nil())
117  {
118  const auto zero = zero_initializer(symbol.type, symbol.location, ns);
119  CHECK_RETURN(zero.has_value());
120  rhs = *zero;
121  }
122  else
123  rhs=symbol.value;
124 
125  code_assignt code(symbol.symbol_expr(), rhs);
126  code.add_source_location()=symbol.location;
127 
128  dest.add(code);
129  }
130 
131  // call designated "initialization" functions
132 
133  for(const std::string &id : symbols)
134  {
135  const symbolt &symbol=ns.lookup(id);
136 
137  if(symbol.type.id() != ID_code)
138  continue;
139 
140  const code_typet &code_type = to_code_type(symbol.type);
141  if(
142  code_type.return_type().id() == ID_constructor &&
143  code_type.parameters().empty())
144  {
145  code_function_callt function_call(symbol.symbol_expr());
146  function_call.add_source_location()=source_location;
147  dest.add(function_call);
148  }
149  }
150 }
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
Base type of functions.
Definition: std_types.h:751
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define CPROVER_PREFIX
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
Goto Programs with Functions.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
exprt value
Initial value of symbol.
Definition: symbol.h:34
unsignedbv_typet size_type()
Definition: c_types.cpp:58
Symbol table entry.
Definition: symbol.h:27
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
bool is_static_lifetime
Definition: symbol.h:65
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
Definition: symbol_table.h:93
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
void add(const codet &code)
Definition: std_code.h:189
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
#define INITIALIZE_FUNCTION
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
codet representation of a label for branch targets.
Definition: std_code.h:1256
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const exprt & size() const
Definition: std_types.h:1010
codet representation of a function call statement.
Definition: std_code.h:1036
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
void static_lifetime_init(symbol_tablet &symbol_table, const source_locationt &source_location)
const symbolst & symbols
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool is_extern
Definition: symbol.h:66
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
const parameterst & parameters() const
Definition: std_types.h:893
source_locationt & add_source_location()
Definition: expr.h:233
A codet representing sequential composition of program statements.
Definition: std_code.h:150
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
A codet representing a skip statement.
Definition: std_code.h:237
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
bool is_type
Definition: symbol.h:61
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const typet & return_type() const
Definition: std_types.h:883
bool is_macro
Definition: symbol.h:61
A codet representing an assignment in the program.
Definition: std_code.h:256
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286