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 
48 static exprt c_get_nondet_bool(const typet &type, const source_locationt &loc)
49 {
50  // We force this to 0 and 1 and won't consider other values
52 }
53 
55 {
56  std::vector<const symbolt *> &symbols_created;
59  const bool assume_non_null;
61 
62 public:
64  std::vector<const symbolt *> &_symbols_created,
65  symbol_tablet &_symbol_table,
66  const source_locationt &loc,
67  const bool _assume_non_null):
68  symbols_created(_symbols_created),
69  symbol_table(_symbol_table),
70  loc(loc),
71  assume_non_null(_assume_non_null),
72  ns(_symbol_table)
73  {}
74 
76  code_blockt &assignments,
77  const exprt &target_expr,
78  const typet &allocate_type,
79  const bool static_lifetime);
80 
81  void gen_nondet_init(code_blockt &assignments, const exprt &expr);
82 };
83 
93  code_blockt &assignments,
94  const exprt &target_expr,
95  const typet &allocate_type,
96  const bool static_lifetime)
97 {
98  const symbolt &aux_symbol=
100  symbol_table,
101  loc,
102  allocate_type,
103  static_lifetime);
104  symbols_created.push_back(&aux_symbol);
105 
106  const typet &allocate_type_resolved=ns.follow(allocate_type);
107  const typet &target_type=ns.follow(target_expr.type().subtype());
108  bool cast_needed=allocate_type_resolved!=target_type;
109 
110  exprt aoe=address_of_exprt(aux_symbol.symbol_expr());
111  if(cast_needed)
112  {
113  aoe=typecast_exprt(aoe, target_expr.type());
114  }
115 
116  // Add the following code to assignments:
117  // <target_expr> = &tmp$<temporary_counter>
118  code_assignt assign(target_expr, aoe);
119  assign.add_source_location()=loc;
120  assignments.move(assign);
121 
122  return aoe;
123 }
124 
131  code_blockt &assignments,
132  const exprt &expr)
133 {
134  const typet &type=ns.follow(expr.type());
135 
136  if(type.id()==ID_pointer)
137  {
138  // dereferenced type
140  const typet &subtype=ns.follow(pointer_type.subtype());
141 
142  code_blockt non_null_inst;
143 
144  exprt allocated=allocate_object(non_null_inst, expr, subtype, false);
145 
146  exprt init_expr;
147  if(allocated.id()==ID_address_of)
148  {
149  init_expr=allocated.op0();
150  }
151  else
152  {
153  init_expr=dereference_exprt(allocated, allocated.type().subtype());
154  }
155  gen_nondet_init(non_null_inst, init_expr);
156 
157  if(assume_non_null)
158  {
159  // Add the following code to assignments:
160  // <expr> = <aoe>;
161  assignments.append(non_null_inst);
162  }
163  else
164  {
165  // Add the following code to assignments:
166  // IF !NONDET(_Bool) THEN GOTO <label1>
167  // <expr> = <null pointer>
168  // GOTO <label2>
169  // <label1>: <expr> = &tmp$<temporary_counter>;
170  // <code from recursive call to gen_nondet_init() with
171  // tmp$<temporary_counter>>
172  // And the next line is labelled label2
173  auto set_null_inst=code_assignt(expr, null_pointer_exprt(pointer_type));
174  set_null_inst.add_source_location()=loc;
175 
176  code_ifthenelset null_check;
177  null_check.cond() = side_effect_expr_nondett(bool_typet(), loc);
178  null_check.then_case()=set_null_inst;
179  null_check.else_case()=non_null_inst;
180 
181  assignments.move(null_check);
182  }
183  }
184  // TODO(OJones): Add support for structs and arrays
185  else
186  {
187  // If type is a ID_c_bool then add the following code to assignments:
188  // <expr> = NONDET(_BOOL);
189  // Else add the following code to assignments:
190  // <expr> = NONDET(type);
191  exprt rhs = type.id() == ID_c_bool ? c_get_nondet_bool(type, loc)
192  : side_effect_expr_nondett(type, loc);
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:486
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:44
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:476
std::vector< const symbolt * > & symbols_created
Goto Programs with Functions.
Fresh auxiliary symbol creation.
The null pointer constant.
Definition: std_expr.h:4518
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:266
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:259
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:254
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
The pointer type.
Definition: std_types.h:1435
Operator to dereference a pointer.
Definition: std_expr.h:3282
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:100
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
symbol_factoryt(std::vector< const symbolt *> &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const bool _assume_non_null)
static exprt c_get_nondet_bool(const typet &type, const source_locationt &loc)
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:107
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:89
An if-then-else.
Definition: std_code.h:466
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:1459
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:496
Assignment.
Definition: std_code.h:196
array index operator
Definition: std_expr.h:1462