cprover
c_nondet_symbol_factory.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C Nondet Symbol Factory
4 
5 Author: 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);
142  me.add_source_location() = loc;
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)
158  : side_effect_expr_nondett(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)
Definition: arith_tools.cpp:99
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
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
source_locationt & add_source_location()
Definition: expr.h:235
typet & type()
Return the type of the expression.
Definition: expr.h:82
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.
Definition: pointer_expr.h:723
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
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
const lifetimet lifetime
The symbol table.
Definition: symbol_table.h:14
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.
Definition: pointer_expr.h:79
#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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
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.