cprover
java_object_factory.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "java_object_factory.h"
10 
11 #include <unordered_set>
12 #include <sstream>
13 
14 #include <util/arith_tools.h>
15 #include <util/fresh_symbol.h>
16 #include <util/c_types.h>
17 #include <util/std_code.h>
18 #include <util/std_expr.h>
19 #include <util/namespace.h>
21 #include <util/prefix.h>
22 
24 
26 
27 #include "java_types.h"
28 #include "java_utils.h"
29 
31  symbol_tablet &symbol_table,
32  const source_locationt &loc,
33  const typet &type,
34  const std::string &prefix="tmp_object_factory")
35 {
36  return get_fresh_aux_symbol(
37  type,
38  "",
39  prefix,
40  loc,
41  ID_java,
42  symbol_table);
43 }
44 
47 static exprt get_nondet_bool(const typet &type)
48 {
49  // We force this to 0 and 1 and won't consider
50  // other values.
52 }
53 
55 {
56  std::vector<const symbolt *> &symbols_created;
58  std::unordered_set<irep_idt, irep_id_hash> recursion_set;
63 
65  const exprt &expr,
66  const pointer_typet &ptr_type);
67 
69  code_blockt &assignments,
70  const exprt &expr,
71  const typet &target_type,
72  bool create_dynamic_objects);
73 
75  code_blockt &assignments,
76  const exprt &lhs,
77  const exprt &max_length_expr,
78  const typet &element_type);
79 
80 public:
82  std::vector<const symbolt *> &_symbols_created,
83  const source_locationt &loc,
84  bool _assume_non_null,
85  size_t _max_nondet_array_length,
86  symbol_tablet &_symbol_table):
87  symbols_created(_symbols_created),
88  loc(loc),
89  assume_non_null(_assume_non_null),
90  max_nondet_array_length(_max_nondet_array_length),
91  symbol_table(_symbol_table),
92  ns(_symbol_table)
93  {}
94 
96  code_blockt &assignments,
97  const exprt &,
98  const typet &,
99  bool create_dynamic_objects);
100 
102  code_blockt &assignments,
103  const exprt &expr);
104 
105  void gen_nondet_init(
106  code_blockt &assignments,
107  const exprt &expr,
108  bool is_sub,
109  irep_idt class_identifier,
110  bool create_dynamic_objects,
111  bool override=false,
112  const typet &override_type=empty_typet());
113 
114 private:
116  code_blockt &assignments,
117  const exprt &expr,
118  const irep_idt &class_identifier,
119  bool create_dynamic_objects,
120  const pointer_typet &pointer_type);
121 
123  code_blockt &assignments,
124  const exprt &expr,
125  bool is_sub,
126  irep_idt class_identifier,
127  bool create_dynamic_objects,
128  const struct_typet &struct_type);
129 };
130 
137  code_blockt &assignments,
138  const exprt &target_expr,
139  const typet &allocate_type,
140  bool create_dynamic_objects)
141 {
142  const typet &allocate_type_resolved=ns.follow(allocate_type);
143  const typet &target_type=ns.follow(target_expr.type().subtype());
144  bool cast_needed=allocate_type_resolved!=target_type;
145  if(!create_dynamic_objects)
146  {
147  symbolt &aux_symbol=new_tmp_symbol(symbol_table, loc, allocate_type);
148  symbols_created.push_back(&aux_symbol);
149 
150  exprt object=aux_symbol.symbol_expr();
151  exprt aoe=address_of_exprt(object);
152  if(cast_needed)
153  aoe=typecast_exprt(aoe, target_expr.type());
154  code_assignt code(target_expr, aoe);
155  code.add_source_location()=loc;
156  assignments.copy_to_operands(code);
157  return aoe;
158  }
159  else
160  {
161  // build size expression
163 
164  if(allocate_type.id()!=ID_empty)
165  {
166  assert(!object_size.is_nil() && "size of Java objects should be known");
167  // malloc expression
168  exprt malloc_expr=side_effect_exprt(ID_malloc);
169  malloc_expr.copy_to_operands(object_size);
170  typet result_type=pointer_type(allocate_type);
171  malloc_expr.type()=result_type;
172  // Create a symbol for the malloc expression so we can initialize
173  // without having to do it potentially through a double-deref, which
174  // breaks the to-SSA phase.
175  symbolt &malloc_sym=new_tmp_symbol(
176  symbol_table,
177  loc,
178  pointer_type(allocate_type),
179  "malloc_site");
180  symbols_created.push_back(&malloc_sym);
181  code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
182  code_assignt &malloc_assign=assign;
183  malloc_assign.add_source_location()=loc;
184  assignments.copy_to_operands(malloc_assign);
185  malloc_expr=malloc_sym.symbol_expr();
186  if(cast_needed)
187  malloc_expr=typecast_exprt(malloc_expr, target_expr.type());
188  code_assignt code(target_expr, malloc_expr);
189  code.add_source_location()=loc;
190  assignments.copy_to_operands(code);
191  return malloc_sym.symbol_expr();
192  }
193  else
194  {
195  // make null
196  null_pointer_exprt null_pointer_expr(to_pointer_type(target_expr.type()));
197  code_assignt code(target_expr, null_pointer_expr);
198  code.add_source_location()=loc;
199  assignments.copy_to_operands(code);
200  return exprt();
201  }
202  }
203 }
204 
209  const exprt &expr,
210  const pointer_typet &ptr_type)
211 {
212  null_pointer_exprt null_pointer_expr(ptr_type);
213  code_assignt code(expr, null_pointer_expr);
214  code.add_source_location()=loc;
215  return code;
216 }
217 
230  code_blockt &assignments,
231  const exprt &expr,
232  const typet &target_type,
233  bool create_dynamic_objects)
234 {
235  if(target_type.id()==ID_struct &&
236  has_prefix(
237  id2string(to_struct_type(target_type).get_tag()),
238  "java::array["))
239  {
241  assignments,
242  expr);
243  }
244  else
245  {
246  exprt target;
247  target=allocate_object(
248  assignments,
249  expr,
250  target_type,
251  create_dynamic_objects);
252  exprt init_expr;
253  if(target.id()==ID_address_of)
254  init_expr=target.op0();
255  else
256  init_expr=
257  dereference_exprt(target, target.type().subtype());
259  assignments,
260  init_expr,
261  false,
262  "",
263  create_dynamic_objects,
264  false,
265  typet());
266  }
267 }
268 
280  code_blockt &assignments,
281  const exprt &expr,
282  const irep_idt &class_identifier,
283  bool create_dynamic_objects,
285 {
286  const typet &subtype=ns.follow(pointer_type.subtype());
287 
288  if(subtype.id()==ID_struct)
289  {
290  const struct_typet &struct_type=to_struct_type(subtype);
291  const irep_idt struct_tag=struct_type.get_tag();
292  // set to null if found in recursion set and not a sub-type
293  if(recursion_set.find(struct_tag)!=recursion_set.end() &&
294  struct_tag==class_identifier)
295  {
296  assignments.copy_to_operands(
298  return;
299  }
300  }
301 
302  code_blockt non_null_inst;
304  non_null_inst,
305  expr,
306  subtype,
307  create_dynamic_objects);
308 
309  if(assume_non_null)
310  {
311  // Add the following code to assignments:
312  // <expr> = <aoe>;
313  assignments.append(non_null_inst);
314  }
315  else
316  {
317  // if(NONDET(_Bool)
318  // {
319  // <expr> = <null pointer>
320  // }
321  // else
322  // {
323  // <code from recursive call to gen_nondet_init() with
324  // tmp$<temporary_counter>>
325  // }
326  auto set_null_inst=get_null_assignment(expr, pointer_type);
327 
328  code_ifthenelset null_check;
329  null_check.cond()=side_effect_expr_nondett(bool_typet());
330  null_check.then_case()=set_null_inst;
331  null_check.else_case()=non_null_inst;
332 
333  assignments.add(null_check);
334  }
335 }
336 
351  code_blockt &assignments,
352  const exprt &expr,
353  bool is_sub,
354  irep_idt class_identifier,
355  bool create_dynamic_objects,
356  const struct_typet &struct_type)
357 {
358  typedef struct_typet::componentst componentst;
359 
360  const irep_idt struct_tag=struct_type.get_tag();
361 
362  const componentst &components=struct_type.components();
363 
364  if(!is_sub)
365  class_identifier=struct_tag;
366 
367  recursion_set.insert(struct_tag);
368 
369  for(const auto &component : components)
370  {
371  const typet &component_type=component.type();
372  irep_idt name=component.get_name();
373 
374  member_exprt me(expr, name, component_type);
375 
376  if(name=="@class_identifier")
377  {
378  irep_idt qualified_clsid="java::"+as_string(class_identifier);
379  constant_exprt ci(qualified_clsid, string_typet());
380  code_assignt code(me, ci);
381  code.add_source_location()=loc;
382  assignments.copy_to_operands(code);
383  }
384  else if(name=="@lock")
385  {
386  code_assignt code(me, from_integer(0, me.type()));
387  code.add_source_location()=loc;
388  assignments.copy_to_operands(code);
389  }
390  else
391  {
392  INVARIANT(!name.empty(), "Each component of a struct must have a name");
393 
394  bool _is_sub=name[0]=='@';
395 
397  assignments,
398  me,
399  _is_sub,
400  class_identifier,
401  create_dynamic_objects);
402  }
403  }
404  recursion_set.erase(struct_tag);
405 }
406 
419  code_blockt &assignments,
420  const exprt &expr,
421  bool is_sub,
422  irep_idt class_identifier,
423  bool create_dynamic_objects,
424  bool override,
425  const typet &override_type)
426 {
427  const typet &type=
428  override ? ns.follow(override_type) : ns.follow(expr.type());
429 
430  if(type.id()==ID_pointer)
431  {
432  // dereferenced type
435  assignments,
436  expr,
437  class_identifier,
438  create_dynamic_objects,
439  pointer_type);
440  }
441  else if(type.id()==ID_struct)
442  {
443  const struct_typet &struct_type=to_struct_type(type);
445  assignments,
446  expr,
447  is_sub,
448  class_identifier,
449  create_dynamic_objects,
450  struct_type);
451  }
452  else
453  {
454  exprt rhs=type.id()==ID_c_bool?
455  get_nondet_bool(type):
457  code_assignt assign(expr, rhs);
458  assign.add_source_location()=loc;
459 
460  assignments.copy_to_operands(assign);
461  }
462 }
463 
474  code_blockt &assignments,
475  const exprt &lhs,
476  const exprt &max_length_expr,
477  const typet &element_type)
478 {
479  symbolt &length_sym=new_tmp_symbol(
480  symbol_table,
481  loc,
482  java_int_type(),
483  "nondet_array_length");
484  symbols_created.push_back(&length_sym);
485  const auto &length_sym_expr=length_sym.symbol_expr();
486 
487  // Initialize array with some undetermined length:
488  gen_nondet_init(assignments, length_sym_expr, false, irep_idt(), false);
489 
490  // Insert assumptions to bound its length:
492  assume1(length_sym_expr, ID_ge, from_integer(0, java_int_type()));
494  assume2(length_sym_expr, ID_le, max_length_expr);
495  code_assumet assume_inst1(assume1);
496  code_assumet assume_inst2(assume2);
497  assignments.move_to_operands(assume_inst1);
498  assignments.move_to_operands(assume_inst2);
499 
500  side_effect_exprt java_new_array(ID_java_new_array, lhs.type());
501  java_new_array.copy_to_operands(length_sym_expr);
502  java_new_array.set(ID_length_upper_bound, max_length_expr);
503  java_new_array.type().subtype().set(ID_C_element_type, element_type);
504  codet assign=code_assignt(lhs, java_new_array);
505  assign.add_source_location()=loc;
506  assignments.copy_to_operands(assign);
507 }
508 
512  code_blockt &assignments,
513  const exprt &expr)
514 {
515  assert(expr.type().id()==ID_pointer);
516  const typet &type=ns.follow(expr.type().subtype());
517  const struct_typet &struct_type=to_struct_type(type);
518  assert(expr.type().subtype().id()==ID_symbol);
519  const typet &element_type=
520  static_cast<const typet &>(expr.type().subtype().find(ID_C_element_type));
521 
522  auto max_length_expr=from_integer(max_nondet_array_length, java_int_type());
523 
525  assignments,
526  expr,
527  max_length_expr,
528  element_type);
529 
530  dereference_exprt deref_expr(expr, expr.type().subtype());
531  const auto &comps=struct_type.components();
532  exprt length_expr=member_exprt(deref_expr, "length", comps[1].type());
533  exprt init_array_expr=member_exprt(deref_expr, "data", comps[2].type());
534 
535  if(init_array_expr.type()!=pointer_type(element_type))
536  init_array_expr=
537  typecast_exprt(init_array_expr, pointer_type(element_type));
538 
539  // Interpose a new symbol, as the goto-symex stage can't handle array indexing
540  // via a cast.
541  symbolt &array_init_symbol=new_tmp_symbol(
542  symbol_table,
543  loc,
544  init_array_expr.type(),
545  "array_data_init");
546  symbols_created.push_back(&array_init_symbol);
547  const auto &array_init_symexpr=array_init_symbol.symbol_expr();
548  codet data_assign=code_assignt(array_init_symexpr, init_array_expr);
549  data_assign.add_source_location()=loc;
550  assignments.copy_to_operands(data_assign);
551 
552  // Emit init loop for(array_init_iter=0; array_init_iter!=array.length;
553  // ++array_init_iter) init(array[array_init_iter]);
554  symbolt &counter=new_tmp_symbol(
555  symbol_table,
556  loc,
557  length_expr.type(),
558  "array_init_iter");
559  symbols_created.push_back(&counter);
560  exprt counter_expr=counter.symbol_expr();
561 
562  exprt java_zero=from_integer(0, java_int_type());
563  assignments.copy_to_operands(code_assignt(counter_expr, java_zero));
564 
565  std::string head_name=as_string(counter.base_name)+"_header";
566  code_labelt init_head_label(head_name, code_skipt());
567  code_gotot goto_head(head_name);
568 
569  assignments.move_to_operands(init_head_label);
570 
571  std::string done_name=as_string(counter.base_name)+"_done";
572  code_labelt init_done_label(done_name, code_skipt());
573  code_gotot goto_done(done_name);
574 
575  code_ifthenelset done_test;
576  done_test.cond()=equal_exprt(counter_expr, length_expr);
577  done_test.then_case()=goto_done;
578 
579  assignments.move_to_operands(done_test);
580 
581  // Add a redundant if(counter == max_length) break that is easier for the
582  // unwinder to understand.
583  code_ifthenelset max_test;
584  max_test.cond()=equal_exprt(counter_expr, max_length_expr);
585  max_test.then_case()=goto_done;
586 
587  assignments.move_to_operands(max_test);
588 
589  exprt arraycellref=dereference_exprt(
590  plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.type()),
591  array_init_symexpr.type().subtype());
592 
594  assignments,
595  arraycellref,
596  false,
597  irep_idt(),
598  true,
599  true,
600  element_type);
601 
602  exprt java_one=from_integer(1, java_int_type());
603  code_assignt incr(counter_expr, plus_exprt(counter_expr, java_one));
604 
605  assignments.move_to_operands(incr);
606  assignments.move_to_operands(goto_head);
607  assignments.move_to_operands(init_done_label);
608 }
609 
611  const typet &type,
612  const irep_idt base_name,
613  code_blockt &init_code,
614  bool allow_null,
615  symbol_tablet &symbol_table,
616  size_t max_nondet_array_length,
617  const source_locationt &loc)
618 {
620  "::"+id2string(base_name);
621 
622  auxiliary_symbolt main_symbol;
623  main_symbol.mode=ID_java;
624  main_symbol.is_static_lifetime=false;
625  main_symbol.name=identifier;
626  main_symbol.base_name=base_name;
627  main_symbol.type=type;
628  main_symbol.location=loc;
629 
630  exprt object=main_symbol.symbol_expr();
631 
632  symbolt *main_symbol_ptr;
633  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
634  assert(!moving_symbol_failed);
635 
636  std::vector<const symbolt *> symbols_created;
637  symbols_created.push_back(main_symbol_ptr);
638 
639  java_object_factoryt state(
640  symbols_created,
641  loc,
642  !allow_null,
643  max_nondet_array_length,
644  symbol_table);
645  code_blockt assignments;
646  state.gen_nondet_init(
647  assignments,
648  object,
649  false,
650  "",
651  false);
652 
653  // Add the following code to init_code for each symbol that's been created:
654  // <type> <identifier>;
655  for(const symbolt * const symbol_ptr : symbols_created)
656  {
657  code_declt decl(symbol_ptr->symbol_expr());
658  decl.add_source_location()=loc;
659  init_code.add(decl);
660  }
661 
662  init_code.append(assignments);
663  return object;
664 }
#define loc()
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
exprt size_of_expr(const typet &type, const namespacet &ns)
const codet & then_case() const
Definition: std_code.h:370
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
semantic type conversion
Definition: std_expr.h:1725
Linking: Zero Initialization.
bool is_nil() const
Definition: irep.h:103
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
code_assignt get_null_assignment(const exprt &expr, const pointer_typet &ptr_type)
Adds an instruction to init_code null-initialising expr.
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
irep_idt mode
Language mode.
Definition: symbol.h:55
const exprt & cond() const
Definition: std_code.h:360
exprt allocate_object(code_blockt &assignments, const exprt &, const typet &, bool create_dynamic_objects)
typet java_int_type()
Definition: java_types.cpp:19
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
Goto Programs with Functions.
std::vector< componentt > componentst
Definition: std_types.h:240
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
Fresh auxiliary symbol creation.
The null pointer constant.
Definition: std_expr.h:3774
const componentst & components() const
Definition: std_types.h:242
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, size_t max_nondet_array_length, const source_locationt &loc)
void gen_pointer_target_init(code_blockt &assignments, const exprt &expr, const typet &target_type, bool create_dynamic_objects)
Initialises an object tree rooted at expr, allocating child objects as necessary and nondet-initialis...
A ‘goto’ instruction.
Definition: std_code.h:613
typet & type()
Definition: expr.h:60
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
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
void gen_nondet_array_init(code_blockt &assignments, const exprt &expr)
create code to initialize a Java array with size max_nondet_array_length, loop over elements and init...
bool is_static_lifetime
Definition: symbol.h:70
std::unordered_set< irep_idt, irep_id_hash > recursion_set
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:202
Extract member of struct or union.
Definition: std_expr.h:3214
TO_BE_DOCUMENTED.
Definition: std_types.h:1490
equality
Definition: std_expr.h:1082
const char * as_string(coverage_criteriont c)
Definition: cover.cpp:71
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:189
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
The empty type.
Definition: std_types.h:53
std::vector< const symbolt * > & symbols_created
Operator to dereference a pointer.
Definition: std_expr.h:2701
API to expression classes.
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
A label for branch targets.
Definition: std_code.h:760
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
symbol_tablet & symbol_table
The plus expression.
Definition: std_expr.h:702
static exprt get_nondet_bool(const typet &type)
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.
java_object_factoryt(std::vector< const symbolt *> &_symbols_created, const source_locationt &loc, bool _assume_non_null, size_t _max_nondet_array_length, symbol_tablet &_symbol_table)
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
static symbolt & new_tmp_symbol(symbol_tablet &symbol_table, const source_locationt &loc, const typet &type, const std::string &prefix="tmp_object_factory")
An assumption.
Definition: std_code.h:274
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
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
void gen_nondet_init(code_blockt &assignments, const exprt &expr, bool is_sub, irep_idt class_identifier, bool create_dynamic_objects, bool override=false, const typet &override_type=empty_typet())
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
void gen_nondet_struct_init(code_blockt &assignments, const exprt &expr, bool is_sub, irep_idt class_identifier, bool create_dynamic_objects, const struct_typet &struct_type)
Initialises an object tree rooted at expr, allocating child objects as necessary and nondet-initialis...
Base class for all expressions.
Definition: expr.h:46
void gen_nondet_pointer_init(code_blockt &assignments, const exprt &expr, const irep_idt &class_identifier, bool create_dynamic_objects, const pointer_typet &pointer_type)
Initialises a primitive or object tree rooted at expr, of type pointer.
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
void allocate_nondet_length_array(code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type)
Allocates a fresh array.
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
Skip.
Definition: std_code.h:134
An if-then-else.
Definition: std_code.h:350
dstringt irep_idt
Definition: irep.h:32
A statement in a programming language.
Definition: std_code.h:19
const typet & subtype() const
Definition: type.h:31
irep_idt get_tag() const
Definition: std_types.h:263
An expression containing a side effect.
Definition: std_code.h:997
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const codet & else_case() const
Definition: std_code.h:380
bool empty() const
Definition: dstring.h:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const source_locationt & loc
Assignment.
Definition: std_code.h:144