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 <cstdlib>
12 
13 #include <util/arith_tools.h>
14 #include <util/c_types.h>
15 #include <util/config.h>
16 #include <util/expr_initializer.h>
17 #include <util/namespace.h>
18 #include <util/prefix.h>
19 #include <util/std_code.h>
20 #include <util/std_expr.h>
21 
23 
24 static optionalt<codet>
25 static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
26 {
27  const namespacet ns(symbol_table);
28  const symbolt &symbol = ns.lookup(identifier);
29 
30  if(!symbol.is_static_lifetime)
31  return {};
32 
33  if(symbol.is_type || symbol.is_macro)
34  return {};
35 
36  // special values
37  if(
38  identifier == CPROVER_PREFIX "constant_infinity_uint" ||
39  identifier == CPROVER_PREFIX "memory" || identifier == "__func__" ||
40  identifier == "__FUNCTION__" || identifier == "__PRETTY_FUNCTION__" ||
41  identifier == "argc'" || identifier == "argv'" || identifier == "envp'" ||
42  identifier == "envp_size'")
43  return {};
44 
45  // just for linking
46  if(has_prefix(id2string(identifier), CPROVER_PREFIX "architecture_"))
47  return {};
48 
49  const typet &type = ns.follow(symbol.type);
50 
51  // check type
52  if(type.id() == ID_code || type.id() == ID_empty)
53  return {};
54 
55  if(type.id() == ID_array && to_array_type(type).size().is_nil())
56  {
57  // C standard 6.9.2, paragraph 5
58  // adjust the type to an array of size 1
59  symbolt &writable_symbol = symbol_table.get_writeable_ref(identifier);
60  writable_symbol.type = type;
61  writable_symbol.type.set(ID_size, from_integer(1, size_type()));
62  }
63 
64  if(
65  (type.id() == ID_struct || type.id() == ID_union) &&
66  to_struct_union_type(type).is_incomplete())
67  {
68  return {}; // do not initialize
69  }
70 
71  exprt rhs;
72 
73  if((symbol.value.is_nil() && symbol.is_extern) ||
74  symbol.value.id() == ID_nondet)
75  {
76  // Nondet initialise if not linked, or if explicitly requested.
77  // Compilers would usually complain about the unlinked symbol case.
78  const auto nondet = nondet_initializer(symbol.type, symbol.location, ns);
79  CHECK_RETURN(nondet.has_value());
80  rhs = *nondet;
81  }
82  else if(symbol.value.is_nil())
83  {
84  const auto zero = zero_initializer(symbol.type, symbol.location, ns);
85  CHECK_RETURN(zero.has_value());
86  rhs = *zero;
87  }
88  else
89  rhs = symbol.value;
90 
91  code_assignt code(symbol.symbol_expr(), rhs);
92  code.add_source_location() = symbol.location;
93 
94  return std::move(code);
95 }
96 
98  symbol_tablet &symbol_table,
99  const source_locationt &source_location)
100 {
102 
103  const namespacet ns(symbol_table);
104 
105  symbolt &init_symbol = symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
106 
107  init_symbol.value=code_blockt();
108  init_symbol.value.add_source_location()=source_location;
109 
110  code_blockt &dest=to_code_block(to_code(init_symbol.value));
111 
112  // add the magic label to hide
113  dest.add(code_labelt(CPROVER_PREFIX "HIDE", code_skipt()));
114 
115  // do assignments based on "value"
116 
117  // sort alphabetically for reproducible results
118  std::set<std::string> symbols;
119 
120  for(const auto &symbol_pair : symbol_table.symbols)
121  {
122  symbols.insert(id2string(symbol_pair.first));
123  }
124 
125  // first do framework variables
126  for(const std::string &id : symbols)
127  if(has_prefix(id, CPROVER_PREFIX))
128  {
129  auto code = static_lifetime_init(id, symbol_table);
130  if(code.has_value())
131  dest.add(std::move(*code));
132  }
133 
134  // now all other variables
135  for(const std::string &id : symbols)
136  if(!has_prefix(id, CPROVER_PREFIX))
137  {
138  auto code = static_lifetime_init(id, symbol_table);
139  if(code.has_value())
140  dest.add(std::move(*code));
141  }
142 
143  // now call designated "initialization" functions
144 
145  for(const std::string &id : symbols)
146  {
147  const symbolt &symbol=ns.lookup(id);
148 
149  if(symbol.type.id() != ID_code)
150  continue;
151 
152  const code_typet &code_type = to_code_type(symbol.type);
153  if(
154  code_type.return_type().id() == ID_constructor &&
155  code_type.parameters().empty())
156  {
157  code_function_callt function_call(symbol.symbol_expr());
158  function_call.add_source_location()=source_location;
159  dest.add(function_call);
160  }
161  }
162 }
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
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
arith_tools.h
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
prefix.h
nondet_initializer
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...
Definition: expr_initializer.cpp:333
exprt
Base class for all expressions.
Definition: expr.h:54
namespace.h
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:318
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
expr_initializer.h
Expression Initialization.
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1407
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
code_typet
Base type of functions.
Definition: std_types.h:744
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
source_locationt
Definition: source_location.h:20
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
code_skipt
A codet representing a skip statement.
Definition: std_code.h:270
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
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
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
static_lifetime_init
static optionalt< codet > static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
Definition: static_lifetime_init.cpp:25
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_functions.h
Goto Programs with Functions.
config.h
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:850
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
static_lifetime_init.h
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
std_expr.h
API to expression classes.
c_types.h