cprover
Loading...
Searching...
No Matches
recursive_initialization.h
Go to the documentation of this file.
1/******************************************************************\
2
3Module: recursive_initialization
4
5Author: Diffblue Ltd.
6
7\******************************************************************/
8
9#ifndef CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
10#define CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
11
12#include <map>
13#include <set>
14#include <unordered_set>
15
16#include <util/cprover_prefix.h>
17#include <util/optional.h>
18#include <util/prefix.h>
19#include <util/std_expr.h>
20#include <util/symbol.h>
21
22class code_blockt;
23class goto_modelt;
24
25#define GOTO_HARNESS_PREFIX "__GOTO_HARNESS"
27{
28 std::size_t min_null_tree_depth = 1;
29 std::size_t max_nondet_tree_depth = 2;
31 std::unordered_set<irep_idt> potential_null_function_pointers;
32
33 // array stuff
34 std::size_t max_dynamic_array_size = 2;
35 std::size_t min_dynamic_array_size = 1;
36
37 std::set<irep_idt> pointers_to_treat_as_arrays;
40
42 std::vector<std::set<irep_idt>> pointers_to_treat_equal;
43
45
46 std::vector<std::vector<irep_idt>> selection_specs;
47
48 std::string to_string() const; // for debugging purposes
49
55 bool handle_option(
56 const std::string &option,
57 const std::list<std::string> &values);
58};
59
63{
64public:
65 using recursion_sett = std::set<irep_idt>;
66 using equal_cluster_idt = std::size_t;
68 {
72 bool operator<(const constructor_keyt &other) const
73 {
75 std::tie(
76 other.constructor_type,
77 other.is_nullable,
78 other.has_size_parameter);
79 };
80 bool operator==(const constructor_keyt &other) const
81 {
83 std::tie(
84 other.constructor_type,
85 other.is_nullable,
86 other.has_size_parameter);
87 };
88 };
89 using type_constructor_namest = std::map<constructor_keyt, irep_idt>;
90
94
99 void initialize(const exprt &lhs, const exprt &depth, code_blockt &body);
100
105
106 static bool is_initialization_allowed(const symbolt &symbol)
107 {
108 auto const symbol_name = id2string(symbol.name);
109 return (
110 symbol.is_static_lifetime && symbol.is_lvalue &&
111 !symbol.type.get_bool(ID_C_constant) && symbol.type.id() != ID_code &&
114 }
115
116 bool needs_freeing(const exprt &expr) const;
117 void free_if_possible(const exprt &expr, code_blockt &body);
119
120private:
126 std::vector<optionalt<exprt>> common_arguments_origins;
127
132
139
147 const std::string &symbol_name,
148 const exprt &initial_value) const;
149
153 symbol_exprt get_fresh_global_symexpr(const std::string &symbol_name) const;
154
158 symbol_exprt get_fresh_local_symexpr(const std::string &symbol_name) const;
159
165 const std::string &symbol_name,
166 const typet &type) const;
167
172 const symbolt &
173 get_fresh_fun_symbol(const std::string &fun_name, const typet &fun_type);
174
180 const std::string &param_name,
181 const typet &param_type);
182
187
192 std::string type2id(const typet &type) const;
193
202 const exprt &depth_symbol,
206 const bool is_nullable);
207
212 irep_idt build_constructor(const exprt &expr);
213
219 const symbol_exprt &result,
220 bool is_nullable);
221
229 build_pointer_constructor(const exprt &depth, const symbol_exprt &result);
230
237 build_struct_constructor(const exprt &depth, const symbol_exprt &result);
238
243
250 build_array_constructor(const exprt &depth, const symbol_exprt &result);
251
260 const exprt &depth,
261 const symbol_exprt &result,
262 const exprt &size,
264
273 const exprt &lhs,
274 const exprt &depth,
275 code_blockt &body,
276 const std::vector<irep_idt> &selection_spec);
277};
278
279#endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
std::string array_name(const namespacet &ns, const exprt &expr)
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_table_baset &symbol_table)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
A codet representing sequential composition of program statements.
Definition std_code.h:130
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irep_idt & id() const
Definition irep.h:396
Class for generating initialisation code for compound structures.
void initialize_selected_member(const exprt &lhs, const exprt &depth, code_blockt &body, const std::vector< irep_idt > &selection_spec)
Select the specified struct-member to be non-deterministically initialized.
std::vector< optionalt< exprt > > common_arguments_origins
std::string type2id(const typet &type) const
Simple pretty-printer for typet.
void free_if_possible(const exprt &expr, code_blockt &body)
type_constructor_namest type_constructor_names
code_blockt build_nondet_constructor(const symbol_exprt &result) const
Default constructor: assigns non-deterministic value of the right type.
symbol_exprt get_malloc_function()
Get the malloc function as symbol exprt, and inserts it into the goto-model if it doesn't exist alrea...
code_blockt build_struct_constructor(const exprt &depth, const symbol_exprt &result)
Constructor for structures: simply iterates over members and initialise each one.
irep_idt build_constructor(const exprt &expr)
Check if a constructor for the type of expr already exists and create it if not.
irep_idt get_fresh_global_name(const std::string &symbol_name, const exprt &initial_value) const
Construct a new global symbol of type int and set it's value to initial_value.
code_blockt build_function_pointer_constructor(const symbol_exprt &result, bool is_nullable)
Constructor for function pointers.
const recursive_initialization_configt initialization_config
symbol_exprt get_fresh_local_typed_symexpr(const std::string &symbol_name, const typet &type) const
Construct a new local symbol of type type initialised to init_value.
static bool is_initialization_allowed(const symbolt &symbol)
code_blockt build_dynamic_array_constructor(const exprt &depth, const symbol_exprt &result, const exprt &size, const optionalt< irep_idt > &lhs_name)
Constructor for dynamic arrays: allocate memory for n elements (n is random but bounded) and initiali...
code_blockt build_array_constructor(const exprt &depth, const symbol_exprt &result)
Constructor for arrays: simply iterates over elements and initialise each one.
optionalt< equal_cluster_idt > find_equal_cluster(const irep_idt &name) const
recursive_initializationt(recursive_initialization_configt initialization_config, goto_modelt &goto_model)
std::map< constructor_keyt, irep_idt > type_constructor_namest
void free_cluster_origins(code_blockt &body)
bool should_be_treated_as_array(const irep_idt &pointer_name) const
code_blockt build_constructor_body(const exprt &depth_symbol, const symbol_exprt &result_symbol, const optionalt< exprt > &size_symbol, const optionalt< irep_idt > &lhs_name, const bool is_nullable)
Case analysis for which constructor should be used.
void initialize(const exprt &lhs, const exprt &depth, code_blockt &body)
Generate initialisation code for lhs into body.
symbol_exprt get_free_function()
Get the free function as symbol expression, and inserts it into the goto-model if it doesn't exist al...
bool needs_freeing(const exprt &expr) const
const symbolt & get_fresh_fun_symbol(const std::string &fun_name, const typet &fun_type)
Construct a new function symbol of type fun_type.
bool should_be_treated_as_cstring(const irep_idt &pointer_name) const
symbol_exprt get_fresh_local_symexpr(const std::string &symbol_name) const
Construct a new local symbol of type int initialised to 0.
bool is_array_size_parameter(const irep_idt &cmdline_arg) const
symbol_exprt get_symbol_expr(const irep_idt &symbol_name) const
Recover the symbol expression from symbol table.
symbol_exprt get_fresh_global_symexpr(const std::string &symbol_name) const
Construct a new global symbol of type int initialised to 0.
code_blockt build_pointer_constructor(const exprt &depth, const symbol_exprt &result)
Generic constructor for all pointers: only builds one pointee (not an array) but may recourse in case...
optionalt< irep_idt > get_associated_size_variable(const irep_idt &array_name) const
symbolt & get_fresh_param_symbol(const std::string &param_name, const typet &param_type)
Construct a new parameter symbol of type param_type.
Expression to hold a symbol (variable)
Definition std_expr.h:113
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
bool is_lvalue
Definition symbol.h:72
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
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
#define GOTO_HARNESS_PREFIX
API to expression classes.
std::vector< std::set< irep_idt > > pointers_to_treat_equal
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
bool handle_option(const std::string &option, const std::list< std::string > &values)
Parse the options specific for recursive initialisation.
std::vector< std::vector< irep_idt > > selection_specs
std::set< irep_idt > variables_that_hold_array_sizes
std::unordered_set< irep_idt > potential_null_function_pointers
bool operator==(const constructor_keyt &other) const
bool operator<(const constructor_keyt &other) const
Symbol table entry.