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,
29 {
30  namespacet ns(symbol_table);
31 
32  const auto maybe_symbol=symbol_table.get_writeable(INITIALIZE_FUNCTION);
33  if(!maybe_symbol)
34  return false;
35  symbolt &init_symbol=*maybe_symbol;
36 
37  init_symbol.value=code_blockt();
38  init_symbol.value.add_source_location()=source_location;
39 
40  code_blockt &dest=to_code_block(to_code(init_symbol.value));
41 
42  // add the magic label to hide
43  dest.add(code_labelt("__CPROVER_HIDE", code_skipt()));
44 
45  // do assignments based on "value"
46 
47  // sort alphabetically for reproducible results
48  std::set<std::string> symbols;
49 
50  for(const auto &symbol_pair : symbol_table.symbols)
51  {
52  symbols.insert(id2string(symbol_pair.first));
53  }
54 
55  for(const std::string &id : symbols)
56  {
57  const symbolt &symbol=ns.lookup(id);
58 
59  const irep_idt &identifier=symbol.name;
60 
61  if(!symbol.is_static_lifetime)
62  continue;
63 
64  if(symbol.is_type || symbol.is_macro)
65  continue;
66 
67  // special values
68  if(identifier==CPROVER_PREFIX "constant_infinity_uint" ||
69  identifier==CPROVER_PREFIX "memory" ||
70  identifier=="__func__" ||
71  identifier=="__FUNCTION__" ||
72  identifier=="__PRETTY_FUNCTION__" ||
73  identifier=="argc'" ||
74  identifier=="argv'" ||
75  identifier=="envp'" ||
76  identifier=="envp_size'")
77  continue;
78 
79  // just for linking
80  if(has_prefix(id, CPROVER_PREFIX "architecture_"))
81  continue;
82 
83  const typet &type=ns.follow(symbol.type);
84 
85  // check type
86  if(type.id()==ID_code ||
87  type.id()==ID_empty)
88  continue;
89 
90  // We won't try to initialize any symbols that have
91  // remained incomplete.
92 
93  if(symbol.value.is_nil() &&
94  symbol.is_extern)
95  // Compilers would usually complain about these
96  // symbols being undefined.
97  continue;
98 
99  if(type.id()==ID_array &&
100  to_array_type(type).size().is_nil())
101  {
102  // C standard 6.9.2, paragraph 5
103  // adjust the type to an array of size 1
104  symbolt &symbol=*symbol_table.get_writeable(identifier);
105  symbol.type=type;
106  symbol.type.set(ID_size, from_integer(1, size_type()));
107  }
108 
109  if(type.id()==ID_incomplete_struct ||
110  type.id()==ID_incomplete_union)
111  continue; // do not initialize
112 
113  if(symbol.value.id()==ID_nondet)
114  continue; // do not initialize
115 
116  exprt rhs;
117 
118  if(symbol.value.is_nil())
119  {
120  try
121  {
122  namespacet ns(symbol_table);
123  rhs=zero_initializer(symbol.type, symbol.location, ns, message_handler);
124  assert(rhs.is_not_nil());
125  }
126  catch(...)
127  {
128  return true;
129  }
130  }
131  else
132  rhs=symbol.value;
133 
134  code_assignt code(symbol.symbol_expr(), rhs);
135  code.add_source_location()=symbol.location;
136 
137  dest.move_to_operands(code);
138  }
139 
140  // call designated "initialization" functions
141 
142  for(const std::string &id : symbols)
143  {
144  const symbolt &symbol=ns.lookup(id);
145 
146  if(symbol.type.id() != ID_code)
147  continue;
148 
149  const code_typet &code_type = to_code_type(symbol.type);
150  if(
151  code_type.return_type().id() == ID_constructor &&
152  code_type.parameters().empty())
153  {
154  code_function_callt function_call;
155  function_call.function()=symbol.symbol_expr();
156  function_call.add_source_location()=source_location;
157  dest.move_to_operands(function_call);
158  }
159  }
160 
161  return false;
162 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
#define CPROVER_PREFIX
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
Goto Programs with Functions.
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
exprt value
Initial value of symbol.
Definition: symbol.h:37
bool static_lifetime_init(symbol_tablet &symbol_table, const source_locationt &source_location, message_handlert &message_handler)
unsignedbv_typet size_type()
Definition: c_types.cpp:58
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool is_static_lifetime
Definition: symbol.h:67
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
Definition: symbol_table.h:87
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
void add(const codet &code)
Definition: std_code.h:112
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
#define INITIALIZE_FUNCTION
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A label for branch targets.
Definition: std_code.h:977
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const exprt & size() const
Definition: std_types.h:1023
A function call.
Definition: std_code.h:858
const typet & follow(const typet &) const
Definition: namespace.cpp:55
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const symbolst & symbols
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
bool is_extern
Definition: symbol.h:68
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
exprt & function()
Definition: std_code.h:878
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:89
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
Skip.
Definition: std_code.h:179
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:165
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
bool is_type
Definition: symbol.h:63
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const typet & return_type() const
Definition: std_types.h:895
bool is_macro
Definition: symbol.h:63
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
Assignment.
Definition: std_code.h:196
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286