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/allocate_objects.h>
17 #include <util/arith_tools.h>
18 #include <util/c_types.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 
25 
36  code_blockt &assignments,
37  const exprt &expr,
38  const std::size_t depth,
39  recursion_sett recursion_set,
40  const bool assign_const)
41 {
42  const typet &type = expr.type();
43 
44  if(!assign_const && expr.type().get_bool(ID_C_constant))
45  {
46  return;
47  }
48 
49  if(type.id()==ID_pointer)
50  {
51  // dereferenced type
53  const typet &subtype = pointer_type.subtype();
54 
55  if(subtype.id() == ID_code)
56  {
57  // Handle the pointer-to-code case separately:
58  // leave as nondet_ptr to allow `remove_function_pointers`
59  // to replace the pointer.
60  assignments.add(
62  return;
63  }
64 
65  if(subtype.id() == ID_struct_tag)
66  {
67  const irep_idt struct_tag = to_struct_tag_type(subtype).get_identifier();
68 
69  if(
70  recursion_set.find(struct_tag) != recursion_set.end() &&
72  {
73  assignments.add(
75 
76  return;
77  }
78  }
79 
80  code_blockt non_null_inst;
81 
82  typet object_type = subtype;
83  if(object_type.id() == ID_empty)
84  object_type = char_type();
85 
87  non_null_inst, expr, object_type, lifetime);
88 
89  gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set, true);
90 
92  {
93  // Add the following code to assignments:
94  // <expr> = <aoe>;
95  assignments.append(non_null_inst);
96  }
97  else
98  {
99  // Add the following code to assignments:
100  // IF !NONDET(_Bool) THEN GOTO <label1>
101  // <expr> = <null pointer>
102  // GOTO <label2>
103  // <label1>: <expr> = &tmp$<temporary_counter>;
104  // <code from recursive call to gen_nondet_init() with
105  // tmp$<temporary_counter>>
106  // And the next line is labelled label2
107  const code_assignt set_null_inst{
109 
110  code_ifthenelset null_check(
112  std::move(set_null_inst),
113  std::move(non_null_inst));
114 
115  assignments.add(std::move(null_check));
116  }
117  }
118  else if(type.id() == ID_struct_tag)
119  {
120  const auto &struct_tag_type = to_struct_tag_type(type);
121 
122  const irep_idt struct_tag = struct_tag_type.get_identifier();
123 
124  recursion_set.insert(struct_tag);
125 
126  const auto &struct_type = to_struct_type(ns.follow_tag(struct_tag_type));
127 
128  for(const auto &component : struct_type.components())
129  {
130  const typet &component_type = component.type();
131 
132  if(!assign_const && component_type.get_bool(ID_C_constant))
133  {
134  continue;
135  }
136 
137  const irep_idt name = component.get_name();
138 
139  member_exprt me(expr, name, component_type);
140  me.add_source_location() = loc;
141 
142  gen_nondet_init(assignments, me, depth, recursion_set, assign_const);
143  }
144  }
145  else if(type.id() == ID_array)
146  {
147  gen_nondet_array_init(assignments, expr, depth, recursion_set);
148  }
149  else
150  {
151  // If type is a ID_c_bool then add the following code to assignments:
152  // <expr> = NONDET(_BOOL);
153  // Else add the following code to assignments:
154  // <expr> = NONDET(type);
155  exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
156  : side_effect_expr_nondett(type, loc);
157  code_assignt assign(expr, rhs);
158  assign.add_source_location()=loc;
159 
160  assignments.add(std::move(assign));
161  }
162 }
163 
165  code_blockt &assignments,
166  const exprt &expr,
167  std::size_t depth,
168  const recursion_sett &recursion_set)
169 {
170  auto const &array_type = to_array_type(expr.type());
171  const auto &size = array_type.size();
172  PRECONDITION(size.id() == ID_constant);
173  auto const array_size = numeric_cast_v<size_t>(to_constant_expr(size));
174  DATA_INVARIANT(array_size > 0, "Arrays should have positive size");
175  for(size_t index = 0; index < array_size; ++index)
176  {
178  assignments,
179  index_exprt(expr, from_integer(index, size_type())),
180  depth,
181  recursion_set);
182  }
183 }
184 
199  code_blockt &init_code,
200  symbol_tablet &symbol_table,
201  const irep_idt base_name,
202  const typet &type,
203  const source_locationt &loc,
204  const c_object_factory_parameterst &object_factory_parameters,
205  const lifetimet lifetime)
206 {
208  "::"+id2string(base_name);
209 
210  auxiliary_symbolt main_symbol;
211  main_symbol.mode=ID_C;
212  main_symbol.is_static_lifetime=false;
213  main_symbol.name=identifier;
214  main_symbol.base_name=base_name;
215  main_symbol.type=type;
216  main_symbol.location=loc;
217 
218  symbol_exprt main_symbol_expr=main_symbol.symbol_expr();
219 
220  symbolt *main_symbol_ptr;
221  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
222  CHECK_RETURN(!moving_symbol_failed);
223 
224  symbol_factoryt state(
225  symbol_table,
226  loc,
228  object_factory_parameters,
229  lifetime);
230 
231  code_blockt assignments;
232  state.gen_nondet_init(assignments, main_symbol_expr);
233 
234  state.add_created_symbol(main_symbol_ptr);
235  state.declare_created_symbols(init_code);
236 
237  init_code.append(assignments);
238 
239  state.mark_created_symbols_as_input(init_code);
240 
241  return main_symbol_expr;
242 }
lifetimet
Selects the kind of objects allocated.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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:58
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
bitvector_typet char_type()
Definition: c_types.cpp:114
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,...
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
The Boolean type.
Definition: std_types.h:36
A codet representing an assignment in the program.
Definition: std_code.h:293
A codet representing sequential composition of program statements.
Definition: std_code.h:168
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:206
codet representation of an if-then-else statement.
Definition: std_code.h:776
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_namet &name) const
Definition: irep.cpp:58
const irep_idt & id() const
Definition: irep.h:407
Extract member of struct or union.
Definition: std_expr.h:2613
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:703
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
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_ptr)
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
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_static_lifetime
Definition: symbol.h:65
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt mode
Language mode.
Definition: symbol.h:49
const irep_idt & get_identifier() const
Definition: std_types.h:410
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:62
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#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:2786
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:813
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.