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/fresh_symbol.h>
20 #include <util/namespace.h>
21 #include <util/nondet_bool.h>
22 #include <util/std_expr.h>
23 #include <util/std_types.h>
24 #include <util/string_constant.h>
25 
27 
38  code_blockt &assignments,
39  const exprt &expr,
40  const std::size_t depth,
41  recursion_sett recursion_set,
42  const bool assign_const)
43 {
44  const typet &type = expr.type();
45 
46  if(!assign_const && expr.type().get_bool(ID_C_constant))
47  {
48  return;
49  }
50 
51  if(type.id()==ID_pointer)
52  {
53  // dereferenced type
55  const typet &subtype = pointer_type.subtype();
56 
57  if(subtype.id() == ID_code)
58  {
59  // Handle the pointer-to-code case separately:
60  // leave as nondet_ptr to allow `remove_function_pointers`
61  // to replace the pointer.
62  assignments.add(
64  return;
65  }
66 
67  if(subtype.id() == ID_struct_tag)
68  {
69  const irep_idt struct_tag = to_struct_tag_type(subtype).get_identifier();
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 = subtype;
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_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_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 {
210  "::"+id2string(base_name);
211 
212  auxiliary_symbolt main_symbol;
213  main_symbol.mode=ID_C;
214  main_symbol.is_static_lifetime=false;
215  main_symbol.name=identifier;
216  main_symbol.base_name=base_name;
217  main_symbol.type=type;
218  main_symbol.location=loc;
219 
220  symbol_exprt main_symbol_expr=main_symbol.symbol_expr();
221 
222  symbolt *main_symbol_ptr;
223  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
224  CHECK_RETURN(!moving_symbol_failed);
225 
226  symbol_factoryt state(
227  symbol_table,
228  loc,
230  object_factory_parameters,
231  lifetime);
232 
233  code_blockt assignments;
234  state.gen_nondet_init(assignments, main_symbol_expr);
235 
236  state.add_created_symbol(main_symbol_ptr);
237  state.declare_created_symbols(init_code);
238 
239  init_code.append(assignments);
240 
241  state.mark_created_symbols_as_input(init_code);
242 
243  return main_symbol_expr;
244 }
c_nondet_symbol_factory.h
C Nondet Symbol Factory.
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
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
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
Fresh auxiliary symbol creation.
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
symbol_factoryt::object_factory_params
const c_object_factory_parameterst & object_factory_params
Definition: c_nondet_symbol_factory.h:29
string_constant.h
c_nondet_symbol_factory
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.
Definition: c_nondet_symbol_factory.cpp:200
exprt
Base class for all expressions.
Definition: expr.h:53
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
bool_typet
The Boolean type.
Definition: std_types.h:37
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:160
symbol_factoryt::gen_nondet_array_init
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.
Definition: c_nondet_symbol_factory.cpp:166
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
object_factory_parameterst::max_nondet_tree_depth
size_t max_nondet_tree_depth
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects.
Definition: object_factory_parameters.h:61
symbol_factoryt::ns
namespacet ns
Definition: c_nondet_symbol_factory.h:28
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
c_object_factory_parameters.h
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:15
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
std_types.h
Pre-defined types.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
symbol_factoryt::add_created_symbol
void add_created_symbol(const symbolt *symbol_ptr)
Definition: c_nondet_symbol_factory.h:60
allocate_objectst::allocate_object
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,...
Definition: allocate_objects.cpp:32
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:69
lifetimet
lifetimet
Selects the kind of objects allocated.
Definition: allocate_objects.h:21
object_factory_parameterst::min_null_tree_depth
size_t min_null_tree_depth
To force a certain depth of non-null objects.
Definition: object_factory_parameters.h:73
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
symbol_factoryt::gen_nondet_init
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 ...
Definition: c_nondet_symbol_factory.cpp:37
symbol_factoryt::loc
const source_locationt & loc
Definition: c_nondet_symbol_factory.h:27
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
code_blockt::append
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:87
symbol_factoryt::allocate_objects
allocate_objectst allocate_objects
Definition: c_nondet_symbol_factory.h:31
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_functions.h
Goto Programs with Functions.
symbol_factoryt::lifetime
const lifetimet lifetime
Definition: c_nondet_symbol_factory.h:33
get_nondet_bool
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition: nondet_bool.h:22
symbol_factoryt
Definition: c_nondet_symbol_factory.h:25
symbol_factoryt::recursion_sett
std::set< irep_idt > recursion_sett
Definition: c_nondet_symbol_factory.h:36
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
index_exprt
Array index operator.
Definition: std_expr.h:1293
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
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
symbol_factoryt::mark_created_symbols_as_input
void mark_created_symbols_as_input(code_blockt &init_code)
Definition: c_nondet_symbol_factory.h:70
std_expr.h
API to expression classes.
allocate_objects.h
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
nondet_bool.h
Nondeterministic boolean helper.
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
symbol_factoryt::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Definition: c_nondet_symbol_factory.h:65