cprover
Loading...
Searching...
No Matches
c_nondet_symbol_factory.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C Nondet Symbol Factory
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
13
15
16#include <util/arith_tools.h>
17#include <util/c_types.h>
18#include <util/fresh_symbol.h>
19#include <util/namespace.h>
20#include <util/nondet_bool.h>
21#include <util/pointer_expr.h>
22#include <util/std_expr.h>
23
26
37 code_blockt &assignments,
38 const exprt &expr,
39 const std::size_t depth,
40 recursion_sett recursion_set,
41 const bool assign_const)
42{
43 const typet &type = expr.type();
44
45 if(!assign_const && expr.type().get_bool(ID_C_constant))
46 {
47 return;
48 }
49
50 if(type.id()==ID_pointer)
51 {
52 // dereferenced type
55
56 if(base_type.id() == ID_code)
57 {
58 // Handle the pointer-to-code case separately:
59 // leave as nondet_ptr to allow `remove_function_pointers`
60 // to replace the pointer.
61 assignments.add(code_frontend_assignt{
63 return;
64 }
65
66 if(base_type.id() == ID_struct_tag)
67 {
68 const irep_idt struct_tag =
70
71 if(
72 recursion_set.find(struct_tag) != recursion_set.end() &&
74 {
75 assignments.add(
77
78 return;
79 }
80 }
81
82 code_blockt non_null_inst;
83
84 typet object_type = base_type;
85 if(object_type.id() == ID_empty)
86 object_type = char_type();
87
89 non_null_inst, expr, object_type, lifetime);
90
91 gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set, true);
92
94 {
95 // Add the following code to assignments:
96 // <expr> = <aoe>;
97 assignments.append(non_null_inst);
98 }
99 else
100 {
101 // Add the following code to assignments:
102 // IF !NONDET(_Bool) THEN GOTO <label1>
103 // <expr> = <null pointer>
104 // GOTO <label2>
105 // <label1>: <expr> = &tmp$<temporary_counter>;
106 // <code from recursive call to gen_nondet_init() with
107 // tmp$<temporary_counter>>
108 // And the next line is labelled label2
109 const code_frontend_assignt set_null_inst{
111
112 code_ifthenelset null_check(
114 std::move(set_null_inst),
115 std::move(non_null_inst));
116
117 assignments.add(std::move(null_check));
118 }
119 }
120 else if(type.id() == ID_struct_tag)
121 {
122 const auto &struct_tag_type = to_struct_tag_type(type);
123
124 const irep_idt struct_tag = struct_tag_type.get_identifier();
125
126 recursion_set.insert(struct_tag);
127
128 const auto &struct_type = to_struct_type(ns.follow_tag(struct_tag_type));
129
130 for(const auto &component : struct_type.components())
131 {
132 const typet &component_type = component.type();
133
134 if(!assign_const && component_type.get_bool(ID_C_constant))
135 {
136 continue;
137 }
138
139 const irep_idt name = component.get_name();
140
141 member_exprt me(expr, name, component_type);
143
144 gen_nondet_init(assignments, me, depth, recursion_set, assign_const);
145 }
146 }
147 else if(type.id() == ID_array)
148 {
149 gen_nondet_array_init(assignments, expr, depth, recursion_set);
150 }
151 else
152 {
153 // If type is a ID_c_bool then add the following code to assignments:
154 // <expr> = NONDET(_BOOL);
155 // Else add the following code to assignments:
156 // <expr> = NONDET(type);
157 exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
159 code_frontend_assignt assign(expr, rhs);
160 assign.add_source_location()=loc;
161
162 assignments.add(std::move(assign));
163 }
164}
165
167 code_blockt &assignments,
168 const exprt &expr,
169 std::size_t depth,
170 const recursion_sett &recursion_set)
171{
172 auto const &array_type = to_array_type(expr.type());
173 const auto &size = array_type.size();
174 PRECONDITION(size.id() == ID_constant);
175 auto const array_size = numeric_cast_v<size_t>(to_constant_expr(size));
176 DATA_INVARIANT(array_size > 0, "Arrays should have positive size");
177 for(size_t index = 0; index < array_size; ++index)
178 {
180 assignments,
181 index_exprt(expr, from_integer(index, size_type())),
182 depth,
183 recursion_set);
184 }
185}
186
201 code_blockt &init_code,
202 symbol_tablet &symbol_table,
203 const irep_idt base_name,
204 const typet &type,
205 const source_locationt &loc,
206 const c_object_factory_parameterst &object_factory_parameters,
207 const lifetimet lifetime)
208{
209 const symbolt &main_symbol = get_fresh_aux_symbol(
210 type,
212 id2string(base_name),
213 loc,
214 ID_C,
215 symbol_table);
216 symbol_exprt main_symbol_expr=main_symbol.symbol_expr();
217
218 symbol_factoryt state(
219 symbol_table,
220 loc,
222 object_factory_parameters,
223 lifetime);
224
225 code_blockt assignments;
226 state.gen_nondet_init(assignments, main_symbol_expr);
227
228 state.add_created_symbol(main_symbol);
229 state.declare_created_symbols(init_code);
230
231 init_code.append(assignments);
232
233 state.mark_created_symbols_as_input(init_code);
234
235 return main_symbol_expr;
236}
lifetimet
Selects the kind of objects allocated.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void base_type(typet &type, const namespacet &ns)
symbol_exprt c_nondet_symbol_factory(code_blockt &init_code, symbol_tablet &symbol_table, const irep_idt base_name, const typet &type, const source_locationt &loc, const c_object_factory_parameterst &object_factory_parameters, const lifetimet lifetime)
Creates a symbol and generates code so that it can vary over all possible values for its type.
C Nondet Symbol Factory.
unsignedbv_typet size_type()
Definition c_types.cpp:68
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
bitvector_typet char_type()
Definition c_types.cpp:124
exprt allocate_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const lifetimet lifetime, const irep_idt &basename_prefix="tmp")
Allocates a new object, either by creating a local variable with automatic lifetime,...
The Boolean type.
Definition std_types.h:36
A codet representing sequential composition of program statements.
Definition std_code.h:130
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition std_code.cpp:89
void add(const codet &code)
Definition std_code.h:168
A codet representing an assignment in the program.
Definition std_code.h:24
codet representation of an if-then-else statement.
Definition std_code.h:460
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
source_locationt & add_source_location()
Definition expr.h:235
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Array index operator.
Definition std_expr.h:1328
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2667
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
The null pointer constant.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Expression to hold a symbol (variable)
Definition std_expr.h:80
void gen_nondet_array_init(code_blockt &assignments, const exprt &expr, std::size_t depth, const recursion_sett &recursion_set)
Generate initialisation code for each array element.
void gen_nondet_init(code_blockt &assignments, const exprt &expr, const std::size_t depth=0, recursion_sett recursion_set=recursion_sett(), const bool assign_const=true)
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
allocate_objectst allocate_objects
void add_created_symbol(const symbolt &symbol)
std::set< irep_idt > recursion_sett
void mark_created_symbols_as_input(code_blockt &init_code)
const c_object_factory_parameterst & object_factory_params
void declare_created_symbols(code_blockt &init_code)
const source_locationt & loc
The symbol table.
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
const irep_idt & get_identifier() const
Definition std_types.h:410
The type of an expression, extends irept.
Definition type.h:29
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
Nondeterministic boolean helper.
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition nondet_bool.h:21
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:48
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
size_t max_nondet_tree_depth
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects.
size_t min_null_tree_depth
To force a certain depth of non-null objects.