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/pointer_expr.h>
23 #include <util/std_expr.h>
24 #include <util/std_types.h>
25 #include <util/string_constant.h>
26 
28 
39  code_blockt &assignments,
40  const exprt &expr,
41  const std::size_t depth,
42  recursion_sett recursion_set,
43  const bool assign_const)
44 {
45  const typet &type = expr.type();
46 
47  if(!assign_const && expr.type().get_bool(ID_C_constant))
48  {
49  return;
50  }
51 
52  if(type.id()==ID_pointer)
53  {
54  // dereferenced type
56  const typet &subtype = pointer_type.subtype();
57 
58  if(subtype.id() == ID_code)
59  {
60  // Handle the pointer-to-code case separately:
61  // leave as nondet_ptr to allow `remove_function_pointers`
62  // to replace the pointer.
63  assignments.add(
65  return;
66  }
67 
68  if(subtype.id() == ID_struct_tag)
69  {
70  const irep_idt struct_tag = to_struct_tag_type(subtype).get_identifier();
71 
72  if(
73  recursion_set.find(struct_tag) != recursion_set.end() &&
75  {
76  assignments.add(
78 
79  return;
80  }
81  }
82 
83  code_blockt non_null_inst;
84 
85  typet object_type = subtype;
86  if(object_type.id() == ID_empty)
87  object_type = char_type();
88 
90  non_null_inst, expr, object_type, lifetime);
91 
92  gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set, true);
93 
95  {
96  // Add the following code to assignments:
97  // <expr> = <aoe>;
98  assignments.append(non_null_inst);
99  }
100  else
101  {
102  // Add the following code to assignments:
103  // IF !NONDET(_Bool) THEN GOTO <label1>
104  // <expr> = <null pointer>
105  // GOTO <label2>
106  // <label1>: <expr> = &tmp$<temporary_counter>;
107  // <code from recursive call to gen_nondet_init() with
108  // tmp$<temporary_counter>>
109  // And the next line is labelled label2
110  const code_assignt set_null_inst{
112 
113  code_ifthenelset null_check(
115  std::move(set_null_inst),
116  std::move(non_null_inst));
117 
118  assignments.add(std::move(null_check));
119  }
120  }
121  else if(type.id() == ID_struct_tag)
122  {
123  const auto &struct_tag_type = to_struct_tag_type(type);
124 
125  const irep_idt struct_tag = struct_tag_type.get_identifier();
126 
127  recursion_set.insert(struct_tag);
128 
129  const auto &struct_type = to_struct_type(ns.follow_tag(struct_tag_type));
130 
131  for(const auto &component : struct_type.components())
132  {
133  const typet &component_type = component.type();
134 
135  if(!assign_const && component_type.get_bool(ID_C_constant))
136  {
137  continue;
138  }
139 
140  const irep_idt name = component.get_name();
141 
142  member_exprt me(expr, name, component_type);
143  me.add_source_location() = loc;
144 
145  gen_nondet_init(assignments, me, depth, recursion_set, assign_const);
146  }
147  }
148  else if(type.id() == ID_array)
149  {
150  gen_nondet_array_init(assignments, expr, depth, recursion_set);
151  }
152  else
153  {
154  // If type is a ID_c_bool then add the following code to assignments:
155  // <expr> = NONDET(_BOOL);
156  // Else add the following code to assignments:
157  // <expr> = NONDET(type);
158  exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
159  : side_effect_expr_nondett(type, loc);
160  code_assignt assign(expr, rhs);
161  assign.add_source_location()=loc;
162 
163  assignments.add(std::move(assign));
164  }
165 }
166 
168  code_blockt &assignments,
169  const exprt &expr,
170  std::size_t depth,
171  const recursion_sett &recursion_set)
172 {
173  auto const &array_type = to_array_type(expr.type());
174  const auto &size = array_type.size();
175  PRECONDITION(size.id() == ID_constant);
176  auto const array_size = numeric_cast_v<size_t>(to_constant_expr(size));
177  DATA_INVARIANT(array_size > 0, "Arrays should have positive size");
178  for(size_t index = 0; index < array_size; ++index)
179  {
181  assignments,
182  index_exprt(expr, from_integer(index, size_type())),
183  depth,
184  recursion_set);
185  }
186 }
187 
202  code_blockt &init_code,
203  symbol_tablet &symbol_table,
204  const irep_idt base_name,
205  const typet &type,
206  const source_locationt &loc,
207  const c_object_factory_parameterst &object_factory_parameters,
208  const lifetimet lifetime)
209 {
211  "::"+id2string(base_name);
212 
213  auxiliary_symbolt main_symbol;
214  main_symbol.mode=ID_C;
215  main_symbol.is_static_lifetime=false;
216  main_symbol.name=identifier;
217  main_symbol.base_name=base_name;
218  main_symbol.type=type;
219  main_symbol.location=loc;
220 
221  symbol_exprt main_symbol_expr=main_symbol.symbol_expr();
222 
223  symbolt *main_symbol_ptr;
224  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
225  CHECK_RETURN(!moving_symbol_failed);
226 
227  symbol_factoryt state(
228  symbol_table,
229  loc,
231  object_factory_parameters,
232  lifetime);
233 
234  code_blockt assignments;
235  state.gen_nondet_init(assignments, main_symbol_expr);
236 
237  state.add_created_symbol(main_symbol_ptr);
238  state.declare_created_symbols(init_code);
239 
240  init_code.append(assignments);
241 
242  state.mark_created_symbols_as_input(init_code);
243 
244  return main_symbol_expr;
245 }
c_nondet_symbol_factory.h
C Nondet Symbol Factory.
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:404
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:302
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
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:201
exprt
Base class for all expressions.
Definition: expr.h:54
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:66
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
bool_typet
The Boolean type.
Definition: std_types.h:36
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
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:167
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
namespace.h
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:778
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:82
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: pointer_expr.h:461
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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
pointer_expr.h
API to expression classes for Pointers.
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:33
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:468
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
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:1968
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
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:38
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:100
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:90
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:807
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:1242
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
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:2700
symbol_factoryt::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Definition: c_nondet_symbol_factory.h:65