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 Limited. All rights reserved.
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <set>
15 #include <sstream>
16 
17 #include <util/arith_tools.h>
18 #include <util/c_types.h>
19 #include <util/fresh_symbol.h>
20 #include <util/std_types.h>
21 #include <util/std_code.h>
22 #include <util/std_expr.h>
23 #include <util/namespace.h>
25 #include <util/prefix.h>
26 
28 
29 #include <ansi-c/string_constant.h>
30 
32 
40 static const symbolt &c_new_tmp_symbol(
41  symbol_tablet &symbol_table,
42  const source_locationt &loc,
43  const typet &type,
44  const bool static_lifetime,
45  const std::string &prefix="tmp")
46 {
47  symbolt &tmp_symbol=
48  get_fresh_aux_symbol(type, "", prefix, loc, ID_C, symbol_table);
49  tmp_symbol.is_static_lifetime=static_lifetime;
50 
51  return tmp_symbol;
52 }
53 
56 static exprt c_get_nondet_bool(const typet &type)
57 {
58  // We force this to 0 and 1 and won't consider other values
60 }
61 
63 {
64  std::vector<symbolt const *> &symbols_created;
67  const bool assume_non_null;
69 
70 public:
72  std::vector<symbolt const *> &_symbols_created,
73  symbol_tablet &_symbol_table,
74  const source_locationt &loc,
75  const bool _assume_non_null):
76  symbols_created(_symbols_created),
77  symbol_table(_symbol_table),
78  loc(loc),
79  assume_non_null(_assume_non_null),
80  ns(_symbol_table)
81  {}
82 
84  code_blockt &assignments,
85  const exprt &target_expr,
86  const typet &allocate_type,
87  const bool static_lifetime);
88 
89  void gen_nondet_init(code_blockt &assignments, const exprt &expr);
90 };
91 
101  code_blockt &assignments,
102  const exprt &target_expr,
103  const typet &allocate_type,
104  const bool static_lifetime)
105 {
106  const symbolt &aux_symbol=
108  symbol_table,
109  loc,
110  allocate_type,
111  static_lifetime);
112  symbols_created.push_back(&aux_symbol);
113 
114  const typet &allocate_type_resolved=ns.follow(allocate_type);
115  const typet &target_type=ns.follow(target_expr.type().subtype());
116  bool cast_needed=allocate_type_resolved!=target_type;
117 
118  exprt aoe=address_of_exprt(aux_symbol.symbol_expr());
119  if(cast_needed)
120  {
121  aoe=typecast_exprt(aoe, target_expr.type());
122  }
123 
124  // Add the following code to assignments:
125  // <target_expr> = &tmp$<temporary_counter>
126  code_assignt assign(target_expr, aoe);
127  assign.add_source_location()=loc;
128  assignments.add(assign);
129 
130  return aoe;
131 }
132 
139  code_blockt &assignments,
140  const exprt &expr)
141 {
142  const typet &type=ns.follow(expr.type());
143 
144  if(type.id()==ID_pointer)
145  {
146  // dereferenced type
148  const typet &subtype=ns.follow(pointer_type.subtype());
149 
150  code_blockt non_null_inst;
151 
152  exprt allocated=allocate_object(non_null_inst, expr, subtype, false);
153 
154  exprt init_expr;
155  if(allocated.id()==ID_address_of)
156  {
157  init_expr=allocated.op0();
158  }
159  else
160  {
161  init_expr=dereference_exprt(allocated, allocated.type().subtype());
162  }
163  gen_nondet_init(non_null_inst, init_expr);
164 
165  if(assume_non_null)
166  {
167  // Add the following code to assignments:
168  // <expr> = <aoe>;
169  assignments.append(non_null_inst);
170  }
171  else
172  {
173  // Add the following code to assignments:
174  // IF !(NONDET(_Bool) == FALSE) THEN GOTO <label1>
175  // <expr> = <null pointer>
176  // GOTO <label2>
177  // <label1>: <expr> = &tmp$<temporary_counter>;
178  // <code from recursive call to gen_nondet_init() with
179  // tmp$<temporary_counter>>
180  // And the next line is labelled label2
181  auto set_null_inst=code_assignt(expr, null_pointer_exprt(pointer_type));
182  set_null_inst.add_source_location()=loc;
183 
184  code_ifthenelset null_check;
185  null_check.cond()=side_effect_expr_nondett(bool_typet());
186  null_check.then_case()=set_null_inst;
187  null_check.else_case()=non_null_inst;
188 
189  assignments.add(null_check);
190  }
191  }
192  // TODO(OJones): Add support for structs and arrays
193  else
194  {
195  // If type is a ID_c_bool then add the following code to assignments:
196  // <expr> = NONDET(_BOOL);
197  // Else add the following code to assignments:
198  // <expr> = NONDET(type);
199  exprt rhs=type.id()==ID_c_bool?
200  c_get_nondet_bool(type):
202  code_assignt assign(expr, rhs);
203  assign.add_source_location()=loc;
204 
205  assignments.add(assign);
206  }
207 }
208 
220  code_blockt &init_code,
222  const irep_idt base_name,
223  const typet &type,
224  const source_locationt &loc,
225  bool allow_null)
226 {
228  "::"+id2string(base_name);
229 
230  auxiliary_symbolt main_symbol;
231  main_symbol.mode=ID_C;
232  main_symbol.is_static_lifetime=false;
233  main_symbol.name=identifier;
234  main_symbol.base_name=base_name;
235  main_symbol.type=type;
236 
237  symbolt *main_symbol_ptr;
238  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
239  assert(!moving_symbol_failed);
240 
241  std::vector<symbolt const *> symbols_created;
242  symbol_exprt main_symbol_expr=(*main_symbol_ptr).symbol_expr();
243  symbols_created.push_back(main_symbol_ptr);
244 
245  symbol_factoryt state(
246  symbols_created,
247  symbol_table,
248  loc,
249  !allow_null);
250  code_blockt assignments;
251  state.gen_nondet_init(assignments, main_symbol_expr);
252 
253  // Add the following code to init_code for each symbol that's been created:
254  // <type> <identifier>;
255  for(symbolt const *symbol_ptr : symbols_created)
256  {
257  code_declt decl(symbol_ptr->symbol_expr());
258  decl.add_source_location()=loc;
259  init_code.add(decl);
260  }
261 
262  init_code.append(assignments);
263 
264  // Add the following code to init_code for each symbol that's been created:
265  // INPUT("<identifier>", <identifier>);
266  for(symbolt const *symbol_ptr : symbols_created)
267  {
268  codet input_code(ID_input);
269  input_code.operands().resize(2);
270  input_code.op0()=
272  string_constantt(symbol_ptr->base_name),
273  from_integer(0, index_type())));
274  input_code.op1()=symbol_ptr->symbol_expr();
275  input_code.add_source_location()=loc;
276  init_code.add(input_code);
277  }
278 
279  return main_symbol_expr;
280 }
#define loc()
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const codet & then_case() const
Definition: std_code.h:370
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
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:1725
Linking: Zero Initialization.
symbol_factoryt(std::vector< symbolt const *> &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const bool _assume_non_null)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
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_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & op0()
Definition: expr.h:84
C Nondet Symbol Factory.
irep_idt mode
Language mode.
Definition: symbol.h:55
const exprt & cond() const
Definition: std_code.h:360
Goto Programs with Functions.
Fresh auxiliary symbol creation.
The null pointer constant.
Definition: std_expr.h:3774
typet & type()
Definition: expr.h:60
const source_locationt & loc
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool is_static_lifetime
Definition: symbol.h:70
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
void add(const codet &code)
Definition: std_code.h:81
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
A declaration of a local variable.
Definition: std_code.h:192
The pointer type.
Definition: std_types.h:1343
Operator to dereference a pointer.
Definition: std_expr.h:2701
API to expression classes.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
TO_BE_DOCUMENTED.
Definition: namespace.h:62
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:1037
bitvector_typet index_type()
Definition: c_types.cpp:15
Operator to return the address of an object.
Definition: std_expr.h:2593
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
Pointer Logic.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1377
typet type
Type of symbol.
Definition: symbol.h:37
API to type classes.
Base class for all expressions.
Definition: expr.h:46
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
std::vector< symbolt const * > & symbols_created
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:147
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:63
static exprt c_get_nondet_bool(const typet &type)
An if-then-else.
Definition: std_code.h:350
Expression to hold a symbol (variable)
Definition: std_expr.h:82
A statement in a programming language.
Definition: std_code.h:19
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const codet & else_case() const
Definition: std_code.h:380
Assignment.
Definition: std_code.h:144
array index operator
Definition: std_expr.h:1170