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/std_expr.h>
22 #include <util/std_types.h>
23 #include <util/string_constant.h>
24 
26 
28 {
29  std::vector<const symbolt *> &symbols_created;
34 
35  typedef std::set<irep_idt> recursion_sett;
36 
37 public:
39  std::vector<const symbolt *> &_symbols_created,
40  symbol_tablet &_symbol_table,
41  const source_locationt &loc,
43  : symbols_created(_symbols_created),
44  symbol_table(_symbol_table),
45  loc(loc),
46  ns(_symbol_table),
48  {}
49 
51  code_blockt &assignments,
52  const exprt &target_expr,
53  const typet &allocate_type,
54  const bool static_lifetime);
55 
56  void gen_nondet_init(
57  code_blockt &assignments,
58  const exprt &expr,
59  const std::size_t depth = 0,
60  recursion_sett recursion_set = recursion_sett());
61 
62 private:
70  code_blockt &assignments,
71  const exprt &expr,
72  std::size_t depth,
73  const recursion_sett &recursion_set);
74 };
75 
85  code_blockt &assignments,
86  const exprt &target_expr,
87  const typet &allocate_type,
88  const bool static_lifetime)
89 {
90  symbolt &aux_symbol = get_fresh_aux_symbol(
91  allocate_type,
93  "tmp",
94  loc,
95  ID_C,
96  symbol_table);
97  aux_symbol.is_static_lifetime = static_lifetime;
98  symbols_created.push_back(&aux_symbol);
99 
100  const typet &allocate_type_resolved=ns.follow(allocate_type);
101  const typet &target_type=ns.follow(target_expr.type().subtype());
102  bool cast_needed=allocate_type_resolved!=target_type;
103 
104  exprt aoe=address_of_exprt(aux_symbol.symbol_expr());
105  if(cast_needed)
106  {
107  aoe=typecast_exprt(aoe, target_expr.type());
108  }
109 
110  // Add the following code to assignments:
111  // <target_expr> = &tmp$<temporary_counter>
112  code_assignt assign(target_expr, aoe);
113  assign.add_source_location()=loc;
114  assignments.add(std::move(assign));
115 
116  return aoe;
117 }
118 
127  code_blockt &assignments,
128  const exprt &expr,
129  const std::size_t depth,
130  recursion_sett recursion_set)
131 {
132  const typet &type=ns.follow(expr.type());
133 
134  if(type.id()==ID_pointer)
135  {
136  // dereferenced type
138  const typet &subtype=ns.follow(pointer_type.subtype());
139 
140  if(subtype.id() == ID_struct)
141  {
142  const struct_typet &struct_type = to_struct_type(subtype);
143  const irep_idt struct_tag = struct_type.get_tag();
144 
145  if(
146  recursion_set.find(struct_tag) != recursion_set.end() &&
148  {
150  assignments.add(std::move(c));
151 
152  return;
153  }
154  }
155 
156  code_blockt non_null_inst;
157 
158  exprt allocated=allocate_object(non_null_inst, expr, subtype, false);
159 
160  exprt init_expr;
161  if(allocated.id()==ID_address_of)
162  {
163  init_expr=allocated.op0();
164  }
165  else
166  {
167  init_expr=dereference_exprt(allocated, allocated.type().subtype());
168  }
169  gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set);
170 
172  {
173  // Add the following code to assignments:
174  // <expr> = <aoe>;
175  assignments.append(non_null_inst);
176  }
177  else
178  {
179  // Add the following code to assignments:
180  // IF !NONDET(_Bool) THEN GOTO <label1>
181  // <expr> = <null pointer>
182  // GOTO <label2>
183  // <label1>: <expr> = &tmp$<temporary_counter>;
184  // <code from recursive call to gen_nondet_init() with
185  // tmp$<temporary_counter>>
186  // And the next line is labelled label2
187  auto set_null_inst=code_assignt(expr, null_pointer_exprt(pointer_type));
188  set_null_inst.add_source_location()=loc;
189 
190  code_ifthenelset null_check(
192  std::move(set_null_inst),
193  std::move(non_null_inst));
194 
195  assignments.add(std::move(null_check));
196  }
197  }
198  else if(type.id() == ID_struct)
199  {
200  const struct_typet &struct_type = to_struct_type(type);
201 
202  const irep_idt struct_tag = struct_type.get_tag();
203 
204  recursion_set.insert(struct_tag);
205 
206  for(const auto &component : struct_type.components())
207  {
208  const typet &component_type = component.type();
209  const irep_idt name = component.get_name();
210 
211  member_exprt me(expr, name, component_type);
212  me.add_source_location() = loc;
213 
214  gen_nondet_init(assignments, me, depth, recursion_set);
215  }
216  }
217  else if(type.id() == ID_array)
218  {
219  gen_nondet_array_init(assignments, expr, depth, recursion_set);
220  }
221  else
222  {
223  // If type is a ID_c_bool then add the following code to assignments:
224  // <expr> = NONDET(_BOOL);
225  // Else add the following code to assignments:
226  // <expr> = NONDET(type);
227  exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
228  : side_effect_expr_nondett(type, loc);
229  code_assignt assign(expr, rhs);
230  assign.add_source_location()=loc;
231 
232  assignments.add(std::move(assign));
233  }
234 }
235 
237  code_blockt &assignments,
238  const exprt &expr,
239  std::size_t depth,
240  const recursion_sett &recursion_set)
241 {
242  auto const &array_type = to_array_type(expr.type());
243  auto const array_size = numeric_cast_v<size_t>(array_type.size());
244  DATA_INVARIANT(array_size > 0, "Arrays should have positive size");
245  for(size_t index = 0; index < array_size; ++index)
246  {
248  assignments,
249  index_exprt(expr, from_integer(index, size_type())),
250  depth,
251  recursion_set);
252  }
253 }
254 
267  code_blockt &init_code,
268  symbol_tablet &symbol_table,
269  const irep_idt base_name,
270  const typet &type,
271  const source_locationt &loc,
272  const c_object_factory_parameterst &object_factory_parameters)
273 {
275  "::"+id2string(base_name);
276 
277  auxiliary_symbolt main_symbol;
278  main_symbol.mode=ID_C;
279  main_symbol.is_static_lifetime=false;
280  main_symbol.name=identifier;
281  main_symbol.base_name=base_name;
282  main_symbol.type=type;
283  main_symbol.location=loc;
284 
285  symbol_exprt main_symbol_expr=main_symbol.symbol_expr();
286 
287  symbolt *main_symbol_ptr;
288  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
289  CHECK_RETURN(!moving_symbol_failed);
290 
291  std::vector<const symbolt *> symbols_created;
292  symbols_created.push_back(main_symbol_ptr);
293 
294  symbol_factoryt state(
295  symbols_created, symbol_table, loc, object_factory_parameters);
296  code_blockt assignments;
297  state.gen_nondet_init(assignments, main_symbol_expr);
298 
299  // Add the following code to init_code for each symbol that's been created:
300  // <type> <identifier>;
301  for(const symbolt * const symbol_ptr : symbols_created)
302  {
303  code_declt decl(symbol_ptr->symbol_expr());
304  decl.add_source_location()=loc;
305  init_code.add(std::move(decl));
306  }
307 
308  init_code.append(assignments);
309 
310  // Add the following code to init_code for each symbol that's been created:
311  // INPUT("<identifier>", <identifier>);
312  for(symbolt const *symbol_ptr : symbols_created)
313  {
314  codet input_code(ID_input);
315  input_code.operands().resize(2);
316  input_code.op0()=
318  string_constantt(symbol_ptr->base_name),
319  from_integer(0, index_type())));
320  input_code.op1()=symbol_ptr->symbol_expr();
321  input_code.add_source_location()=loc;
322  init_code.add(std::move(input_code));
323  }
324 
325  return main_symbol_expr;
326 }
#define loc()
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt allocate_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const bool static_lifetime)
Create a symbol for a pointer to point to.
Semantic type conversion.
Definition: std_expr.h:2277
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
exprt & op0()
Definition: expr.h:84
C Nondet Symbol Factory.
irep_idt mode
Language mode.
Definition: symbol.h:49
const irep_idt & get_function() const
std::vector< const symbolt * > & symbols_created
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
Goto Programs with Functions.
symbol_factoryt(std::vector< const symbolt * > &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const c_object_factory_parameterst &object_factory_params)
Fresh auxiliary symbol creation.
The null pointer constant.
Definition: std_expr.h:4471
const componentst & components() const
Definition: std_types.h:205
Nondeterministic boolean helper.
typet & type()
Return the type of the expression.
Definition: expr.h:68
unsignedbv_typet size_type()
Definition: c_types.cpp:58
const source_locationt & loc
The Boolean type.
Definition: std_types.h:28
Symbol table entry.
Definition: symbol.h:27
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
Structure type, corresponds to C style structs.
Definition: std_types.h:276
bool is_static_lifetime
Definition: symbol.h:65
Extract member of struct or union.
Definition: std_expr.h:3890
const irep_idt & id() const
Definition: irep.h:259
symbol_tablet & symbol_table
void add(const codet &code)
Definition: std_code.h:189
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
size_t max_nondet_tree_depth
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects.
std::set< irep_idt > recursion_sett
A codet representing the declaration of a local variable.
Definition: std_code.h:352
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
void gen_nondet_init(code_blockt &assignments, const exprt &expr, const std::size_t depth=0, recursion_sett recursion_set=recursion_sett())
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
Operator to dereference a pointer.
Definition: std_expr.h:3355
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)
Creates a symbol and generates code so that it can vary over all possible values for its type.
API to expression classes.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:19
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:148
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:102
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Operator to return the address of an object.
Definition: std_expr.h:3255
size_t min_null_tree_depth
To force a certain depth of non-null objects.
const c_object_factory_parameterst & object_factory_params
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
Pre-defined types.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
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, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
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.
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition: nondet_bool.h:22
source_locationt & add_source_location()
Definition: expr.h:233
A codet representing sequential composition of program statements.
Definition: std_code.h:150
codet representation of an if-then-else statement.
Definition: std_code.h:614
Expression to hold a symbol (variable)
Definition: std_expr.h:143
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
const typet & subtype() const
Definition: type.h:38
irep_idt get_tag() const
Definition: std_types.h:226
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
A codet representing an assignment in the program.
Definition: std_code.h:256
Array index operator.
Definition: std_expr.h:1595