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