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 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/fresh_symbol.h>
17 #include <util/namespace.h>
18 #include <util/std_expr.h>
19 #include <util/std_types.h>
20 #include <util/string_constant.h>
21 
23 
31 static const symbolt &c_new_tmp_symbol(
32  symbol_tablet &symbol_table,
33  const source_locationt &loc,
34  const typet &type,
35  const bool static_lifetime,
36  const std::string &prefix="tmp")
37 {
38  symbolt &tmp_symbol = get_fresh_aux_symbol(
39  type, id2string(loc.get_function()), prefix, loc, ID_C, symbol_table);
40  tmp_symbol.is_static_lifetime=static_lifetime;
41 
42  return tmp_symbol;
43 }
44 
47 static exprt c_get_nondet_bool(const typet &type)
48 {
49  // We force this to 0 and 1 and won't consider other values
51 }
52 
54 {
55  std::vector<const symbolt *> &symbols_created;
58  const bool assume_non_null;
60 
61 public:
63  std::vector<const symbolt *> &_symbols_created,
64  symbol_tablet &_symbol_table,
65  const source_locationt &loc,
66  const bool _assume_non_null):
67  symbols_created(_symbols_created),
68  symbol_table(_symbol_table),
69  loc(loc),
70  assume_non_null(_assume_non_null),
71  ns(_symbol_table)
72  {}
73 
75  code_blockt &assignments,
76  const exprt &target_expr,
77  const typet &allocate_type,
78  const bool static_lifetime);
79 
80  void gen_nondet_init(code_blockt &assignments, const exprt &expr);
81 };
82 
92  code_blockt &assignments,
93  const exprt &target_expr,
94  const typet &allocate_type,
95  const bool static_lifetime)
96 {
97  const symbolt &aux_symbol=
100  loc,
101  allocate_type,
102  static_lifetime);
103  symbols_created.push_back(&aux_symbol);
104 
105  const typet &allocate_type_resolved=ns.follow(allocate_type);
106  const typet &target_type=ns.follow(target_expr.type().subtype());
107  bool cast_needed=allocate_type_resolved!=target_type;
108 
109  exprt aoe=address_of_exprt(aux_symbol.symbol_expr());
110  if(cast_needed)
111  {
112  aoe=typecast_exprt(aoe, target_expr.type());
113  }
114 
115  // Add the following code to assignments:
116  // <target_expr> = &tmp$<temporary_counter>
117  code_assignt assign(target_expr, aoe);
118  assign.add_source_location()=loc;
119  assignments.move(assign);
120 
121  return aoe;
122 }
123 
130  code_blockt &assignments,
131  const exprt &expr)
132 {
133  const typet &type=ns.follow(expr.type());
134 
135  if(type.id()==ID_pointer)
136  {
137  // dereferenced type
139  const typet &subtype=ns.follow(pointer_type.subtype());
140 
141  code_blockt non_null_inst;
142 
143  exprt allocated=allocate_object(non_null_inst, expr, subtype, false);
144 
145  exprt init_expr;
146  if(allocated.id()==ID_address_of)
147  {
148  init_expr=allocated.op0();
149  }
150  else
151  {
152  init_expr=dereference_exprt(allocated, allocated.type().subtype());
153  }
154  gen_nondet_init(non_null_inst, init_expr);
155 
156  if(assume_non_null)
157  {
158  // Add the following code to assignments:
159  // <expr> = <aoe>;
160  assignments.append(non_null_inst);
161  }
162  else
163  {
164  // Add the following code to assignments:
165  // IF !NONDET(_Bool) THEN GOTO <label1>
166  // <expr> = <null pointer>
167  // GOTO <label2>
168  // <label1>: <expr> = &tmp$<temporary_counter>;
169  // <code from recursive call to gen_nondet_init() with
170  // tmp$<temporary_counter>>
171  // And the next line is labelled label2
172  auto set_null_inst=code_assignt(expr, null_pointer_exprt(pointer_type));
173  set_null_inst.add_source_location()=loc;
174 
175  code_ifthenelset null_check;
176  null_check.cond()=side_effect_expr_nondett(bool_typet());
177  null_check.then_case()=set_null_inst;
178  null_check.else_case()=non_null_inst;
179 
180  assignments.move(null_check);
181  }
182  }
183  // TODO(OJones): Add support for structs and arrays
184  else
185  {
186  // If type is a ID_c_bool then add the following code to assignments:
187  // <expr> = NONDET(_BOOL);
188  // Else add the following code to assignments:
189  // <expr> = NONDET(type);
190  exprt rhs=type.id()==ID_c_bool?
191  c_get_nondet_bool(type):
193  code_assignt assign(expr, rhs);
194  assign.add_source_location()=loc;
195 
196  assignments.move(assign);
197  }
198 }
199 
211  code_blockt &init_code,
212  symbol_tablet &symbol_table,
213  const irep_idt base_name,
214  const typet &type,
215  const source_locationt &loc,
216  bool allow_null)
217 {
219  "::"+id2string(base_name);
220 
221  auxiliary_symbolt main_symbol;
222  main_symbol.mode=ID_C;
223  main_symbol.is_static_lifetime=false;
224  main_symbol.name=identifier;
225  main_symbol.base_name=base_name;
226  main_symbol.type=type;
227  main_symbol.location=loc;
228 
229  symbol_exprt main_symbol_expr=main_symbol.symbol_expr();
230 
231  symbolt *main_symbol_ptr;
232  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
233  CHECK_RETURN(!moving_symbol_failed);
234 
235  std::vector<const symbolt *> symbols_created;
236  symbols_created.push_back(main_symbol_ptr);
237 
238  symbol_factoryt state(
239  symbols_created,
240  symbol_table,
241  loc,
242  !allow_null);
243  code_blockt assignments;
244  state.gen_nondet_init(assignments, main_symbol_expr);
245 
246  // Add the following code to init_code for each symbol that's been created:
247  // <type> <identifier>;
248  for(const symbolt * const symbol_ptr : symbols_created)
249  {
250  code_declt decl(symbol_ptr->symbol_expr());
251  decl.add_source_location()=loc;
252  init_code.move(decl);
253  }
254 
255  init_code.append(assignments);
256 
257  // Add the following code to init_code for each symbol that's been created:
258  // INPUT("<identifier>", <identifier>);
259  for(symbolt const *symbol_ptr : symbols_created)
260  {
261  codet input_code(ID_input);
262  input_code.operands().resize(2);
263  input_code.op0()=
265  string_constantt(symbol_ptr->base_name),
266  from_integer(0, index_type())));
267  input_code.op1()=symbol_ptr->symbol_expr();
268  input_code.add_source_location()=loc;
269  init_code.move(input_code);
270  }
271 
272  return main_symbol_expr;
273 }
#define loc()
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
const codet & then_case() const
Definition: std_code.h:481
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:2111
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
exprt & op0()
Definition: expr.h:72
C Nondet Symbol Factory.
irep_idt mode
Language mode.
Definition: symbol.h:52
const exprt & cond() const
Definition: std_code.h:471
std::vector< const symbolt * > & symbols_created
Goto Programs with Functions.
Fresh auxiliary symbol creation.
The null pointer constant.
Definition: std_expr.h:4520
typet & type()
Definition: expr.h:56
const source_locationt & loc
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
bool is_static_lifetime
Definition: symbol.h:67
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, bool allow_null)
Creates a symbol and generates code so that it can vary over all possible values for its type...
const irep_idt & id() const
Definition: irep.h:189
symbol_tablet & symbol_table
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
A declaration of a local variable.
Definition: std_code.h:253
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
The pointer type.
Definition: std_types.h:1426
Operator to dereference a pointer.
Definition: std_expr.h:3284
API to expression classes.
exprt & op1()
Definition: expr.h:75
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:135
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:101
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: std_expr.h:3170
symbol_factoryt(std::vector< const symbolt *> &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const bool _assume_non_null)
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
API to type classes.
static irep_idt entry_point()
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.
Base class for all expressions.
Definition: expr.h:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
void move(codet &code)
Definition: std_code.h:106
static const symbolt & c_new_tmp_symbol(symbol_tablet &symbol_table, const source_locationt &loc, const typet &type, const bool static_lifetime, const std::string &prefix="tmp")
Create a new temporary static symbol.
source_locationt & add_source_location()
Definition: expr.h:130
void gen_nondet_init(code_blockt &assignments, const exprt &expr)
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
Sequential composition.
Definition: std_code.h:88
static exprt c_get_nondet_bool(const typet &type)
An if-then-else.
Definition: std_code.h:461
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
A statement in a programming language.
Definition: std_code.h:21
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const codet & else_case() const
Definition: std_code.h:491
Assignment.
Definition: std_code.h:195
array index operator
Definition: std_expr.h:1462