cprover
create_array_with_type_intrinsic.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Implementation of CProver.createArrayWithType intrinsic
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
13 
15 
16 #include <util/fresh_symbol.h>
17 #include <util/namespace.h>
18 #include <util/pointer_expr.h>
19 #include <util/symbol_table_base.h>
20 
23 {
24  static irep_idt create_array_with_type_name =
25  "java::org.cprover.CProver.createArrayWithType:"
26  "(I[Ljava/lang/Object;)[Ljava/lang/Object;";
27  return create_array_with_type_name;
28 }
29 
41  const irep_idt &function_id,
42  symbol_table_baset &symbol_table,
43  message_handlert &message_handler)
44 {
45  // Replace CProver.createArrayWithType, which uses reflection to copy the
46  // type but not the content of a given array, with a java_new_array statement
47  // followed by overwriting its element type and dimension, similar to our
48  // implementation (in java_bytecode_convert_class.cpp) of the
49  // array[reference].clone() method.
50 
52 
53  namespacet ns{symbol_table};
54 
55  const symbolt &function_symbol =
57  const auto &function_type = to_code_type(function_symbol.type);
58  const auto &length_argument = function_type.parameters().at(0);
59  symbol_exprt length_argument_symbol_expr{length_argument.get_identifier(),
60  length_argument.type()};
61  const auto &existing_array_argument = function_type.parameters().at(1);
62  symbol_exprt existing_array_argument_symbol_expr{
63  existing_array_argument.get_identifier(), existing_array_argument.type()};
64 
65  symbolt &new_array_symbol = get_fresh_aux_symbol(
66  function_type.parameters().at(1).type(),
68  "new_array",
70  ID_java,
71  symbol_table);
72  const auto new_array_symbol_expr = new_array_symbol.symbol_expr();
73 
74  code_blockt code_block;
75 
76  // Declare new_array temporary:
77  code_block.add(code_declt(new_array_symbol_expr));
78 
79  // new_array = new Object[length];
80  side_effect_exprt new_array_expr{
81  ID_java_new_array, new_array_symbol.type, source_locationt{}};
82  new_array_expr.copy_to_operands(length_argument_symbol_expr);
83  code_block.add(code_assignt(new_array_symbol_expr, new_array_expr));
84 
85  dereference_exprt existing_array(existing_array_argument_symbol_expr);
86  dereference_exprt new_array(new_array_symbol_expr);
87 
88  // new_array.@array_dimensions = existing_array.@array_dimensions
89  // new_array.@element_class_identifier =
90  // existing_array.@element_class_identifier
91  member_exprt old_array_dimension(
93  member_exprt old_array_element_classid(
95 
96  member_exprt new_array_dimension(
98  member_exprt new_array_element_classid(
100 
101  code_block.add(code_assignt(new_array_dimension, old_array_dimension));
102  code_block.add(
103  code_assignt(new_array_element_classid, old_array_element_classid));
104 
105  // return new_array
106  code_block.add(code_returnt(new_array_symbol_expr));
107 
108  return std::move(code_block);
109 }
create_array_with_type_body
codet create_array_with_type_body(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Returns the internal implementation for org.cprover.CProver.createArrayWithType.
Definition: create_array_with_type_intrinsic.cpp:40
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME
#define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME
Definition: java_types.h:671
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:168
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
JAVA_ARRAY_DIMENSION_FIELD_NAME
#define JAVA_ARRAY_DIMENSION_FIELD_NAME
Definition: java_types.h:669
fresh_symbol.h
Fresh auxiliary symbol creation.
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:628
object_factory_parameterst::function_id
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Definition: object_factory_parameters.h:79
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:400
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
create_array_with_type_intrinsic.h
Implementation of CProver.createArrayWithType intrinsic.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
API to expression classes for Pointers.
message_handlert
Definition: message.h:28
code_blockt::add
void add(const codet &code)
Definition: std_code.h:206
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:31
source_locationt
Definition: source_location.h:19
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
symbolt
Symbol table entry.
Definition: symbol.h:28
string_typet
String type.
Definition: std_types.h:880
java_types.h
symbol_table_base.h
Author: Diffblue Ltd.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
get_fresh_aux_symbol
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, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1896
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
get_create_array_with_type_name
irep_idt get_create_array_with_type_name()
Returns the symbol name for org.cprover.CProver.createArrayWithType
Definition: create_array_with_type_intrinsic.cpp:22