Skip to content

Commit 98ad12a

Browse files
author
Matthias Güdemann
committed
Move add_array_types to java_utils
1 parent e1ec77a commit 98ad12a

File tree

3 files changed

+185
-179
lines changed

3 files changed

+185
-179
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

Lines changed: 0 additions & 179 deletions
Original file line numberDiff line numberDiff line change
@@ -115,9 +115,6 @@ class java_bytecode_convert_classt:public messaget
115115
void convert(const classt &c, const overlay_classest &overlay_classes);
116116
void convert(symbolt &class_symbol, const fieldt &f);
117117

118-
// see definition below for more info
119-
static void add_array_types(symbol_tablet &symbol_table);
120-
121118
static bool is_overlay_method(const methodt &method)
122119
{
123120
return method.has_annotation(ID_overlay_method);
@@ -716,182 +713,6 @@ void java_bytecode_convert_classt::convert(
716713
}
717714
}
718715

719-
/// Register in the \p symbol_table new symbols for the objects
720-
/// java::array[X] where X is byte, float, int, char...
721-
void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
722-
{
723-
const std::string letters="ijsbcfdza";
724-
725-
for(const char l : letters)
726-
{
727-
symbol_typet symbol_type=
728-
to_symbol_type(java_array_type(l).subtype());
729-
730-
const irep_idt &symbol_type_identifier=symbol_type.get_identifier();
731-
if(symbol_table.has_symbol(symbol_type_identifier))
732-
return;
733-
734-
java_class_typet class_type;
735-
// we have the base class, java.lang.Object, length and data
736-
// of appropriate type
737-
class_type.set_tag(symbol_type_identifier);
738-
// Note that non-array types don't have "java::" at the beginning of their
739-
// tag, and their name is "java::" + their tag. Since arrays do have
740-
// "java::" at the beginning of their tag we set the name to be the same as
741-
// the tag.
742-
class_type.set_name(symbol_type_identifier);
743-
744-
class_type.components().reserve(3);
745-
class_typet::componentt base_class_component(
746-
"@java.lang.Object", symbol_typet("java::java.lang.Object"));
747-
base_class_component.set_pretty_name("@java.lang.Object");
748-
base_class_component.set_base_name("@java.lang.Object");
749-
class_type.components().push_back(base_class_component);
750-
751-
class_typet::componentt length_component("length", java_int_type());
752-
length_component.set_pretty_name("length");
753-
length_component.set_base_name("length");
754-
class_type.components().push_back(length_component);
755-
756-
class_typet::componentt data_component(
757-
"data", java_reference_type(java_type_from_char(l)));
758-
data_component.set_pretty_name("data");
759-
data_component.set_base_name("data");
760-
class_type.components().push_back(data_component);
761-
762-
class_type.add_base(symbol_typet("java::java.lang.Object"));
763-
764-
INVARIANT(
765-
is_valid_java_array(class_type),
766-
"Constructed a new type representing a Java Array "
767-
"object that doesn't match expectations");
768-
769-
symbolt symbol;
770-
symbol.name=symbol_type_identifier;
771-
symbol.base_name=symbol_type.get(ID_C_base_name);
772-
symbol.is_type=true;
773-
symbol.type = class_type;
774-
symbol.mode = ID_java;
775-
symbol_table.add(symbol);
776-
777-
// Also provide a clone method:
778-
// ----------------------------
779-
780-
const irep_idt clone_name=
781-
id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;";
782-
code_typet::parametert this_param;
783-
this_param.set_identifier(id2string(clone_name)+"::this");
784-
this_param.set_base_name("this");
785-
this_param.set_this();
786-
this_param.type()=java_reference_type(symbol_type);
787-
const code_typet clone_type({this_param}, java_lang_object_type());
788-
789-
parameter_symbolt this_symbol;
790-
this_symbol.name=this_param.get_identifier();
791-
this_symbol.base_name=this_param.get_base_name();
792-
this_symbol.pretty_name=this_symbol.base_name;
793-
this_symbol.type=this_param.type();
794-
this_symbol.mode=ID_java;
795-
symbol_table.add(this_symbol);
796-
797-
const irep_idt local_name=
798-
id2string(clone_name)+"::cloned_array";
799-
auxiliary_symbolt local_symbol;
800-
local_symbol.name=local_name;
801-
local_symbol.base_name="cloned_array";
802-
local_symbol.pretty_name=local_symbol.base_name;
803-
local_symbol.type=java_reference_type(symbol_type);
804-
local_symbol.mode=ID_java;
805-
symbol_table.add(local_symbol);
806-
const auto &local_symexpr=local_symbol.symbol_expr();
807-
808-
code_blockt clone_body;
809-
810-
code_declt declare_cloned(local_symexpr);
811-
clone_body.move_to_operands(declare_cloned);
812-
813-
side_effect_exprt java_new_array(
814-
ID_java_new_array,
815-
java_reference_type(symbol_type));
816-
dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
817-
dereference_exprt new_array(local_symexpr, symbol_type);
818-
member_exprt old_length(
819-
old_array, length_component.get_name(), length_component.type());
820-
java_new_array.copy_to_operands(old_length);
821-
code_assignt create_blank(local_symexpr, java_new_array);
822-
clone_body.move_to_operands(create_blank);
823-
824-
member_exprt old_data(
825-
old_array, data_component.get_name(), data_component.type());
826-
member_exprt new_data(
827-
new_array, data_component.get_name(), data_component.type());
828-
829-
/*
830-
// TODO use this instead of a loop.
831-
codet array_copy;
832-
array_copy.set_statement(ID_array_copy);
833-
array_copy.move_to_operands(new_data);
834-
array_copy.move_to_operands(old_data);
835-
clone_body.move_to_operands(array_copy);
836-
*/
837-
838-
// Begin for-loop to replace:
839-
840-
const irep_idt index_name=
841-
id2string(clone_name)+"::index";
842-
auxiliary_symbolt index_symbol;
843-
index_symbol.name=index_name;
844-
index_symbol.base_name="index";
845-
index_symbol.pretty_name=index_symbol.base_name;
846-
index_symbol.type = length_component.type();
847-
index_symbol.mode=ID_java;
848-
symbol_table.add(index_symbol);
849-
const auto &index_symexpr=index_symbol.symbol_expr();
850-
851-
code_declt declare_index(index_symexpr);
852-
clone_body.move_to_operands(declare_index);
853-
854-
code_fort copy_loop;
855-
856-
copy_loop.init()=
857-
code_assignt(index_symexpr, from_integer(0, index_symexpr.type()));
858-
copy_loop.cond()=
859-
binary_relation_exprt(index_symexpr, ID_lt, old_length);
860-
861-
side_effect_exprt inc(ID_assign);
862-
inc.operands().resize(2);
863-
inc.op0()=index_symexpr;
864-
inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));
865-
copy_loop.iter()=inc;
866-
867-
dereference_exprt old_cell(
868-
plus_exprt(old_data, index_symexpr), old_data.type().subtype());
869-
dereference_exprt new_cell(
870-
plus_exprt(new_data, index_symexpr), new_data.type().subtype());
871-
code_assignt copy_cell(new_cell, old_cell);
872-
copy_loop.body()=copy_cell;
873-
874-
// End for-loop
875-
clone_body.move_to_operands(copy_loop);
876-
877-
member_exprt new_base_class(
878-
new_array, base_class_component.get_name(), base_class_component.type());
879-
address_of_exprt retval(new_base_class);
880-
code_returnt return_inst(retval);
881-
clone_body.move_to_operands(return_inst);
882-
883-
symbolt clone_symbol;
884-
clone_symbol.name=clone_name;
885-
clone_symbol.pretty_name=
886-
id2string(symbol_type_identifier)+".clone:()";
887-
clone_symbol.base_name="clone";
888-
clone_symbol.type=clone_type;
889-
clone_symbol.value=clone_body;
890-
clone_symbol.mode=ID_java;
891-
symbol_table.add(clone_symbol);
892-
}
893-
}
894-
895716
bool java_bytecode_convert_class(
896717
const java_class_loadert::parse_tree_with_overlayst &parse_trees,
897718
symbol_tablet &symbol_table,

‎jbmc/src/java_bytecode/java_utils.cpp

Lines changed: 182 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -445,3 +445,185 @@ const std::unordered_set<std::string> cprover_methods_to_ignore
445445
"endThread",
446446
"getCurrentThreadID"
447447
};
448+
449+
/// Register in the \p symbol_table new symbols for the objects
450+
/// java::array[X] where X is byte, float, int, char...
451+
void add_array_types(symbol_tablet &symbol_table)
452+
{
453+
const std::string letters = "ijsbcfdzaa";
454+
455+
bool use_array_copy = false;
456+
457+
for(const char l : letters)
458+
{
459+
symbol_typet symbol_type = to_symbol_type(java_array_type(l).subtype());
460+
461+
const std::string identifier = use_array_copy
462+
? "java::array[Enum]"
463+
: id2string(symbol_type.get_identifier());
464+
const irep_idt &symbol_type_identifier = identifier;
465+
if(symbol_table.has_symbol(symbol_type_identifier))
466+
return;
467+
468+
java_class_typet class_type;
469+
// we have the base class, java.lang.Object, length and data
470+
// of appropriate type
471+
class_type.set_tag(symbol_type_identifier);
472+
// Note that non-array types don't have "java::" at the beginning of their
473+
// tag, and their name is "java::" + their tag. Since arrays do have
474+
// "java::" at the beginning of their tag we set the name to be the same as
475+
// the tag.
476+
class_type.set_name(symbol_type_identifier);
477+
478+
class_type.components().reserve(3);
479+
class_typet::componentt base_class_component(
480+
"@java.lang.Object", symbol_typet("java::java.lang.Object"));
481+
base_class_component.set_pretty_name("@java.lang.Object");
482+
base_class_component.set_base_name("@java.lang.Object");
483+
class_type.components().push_back(base_class_component);
484+
485+
class_typet::componentt length_component("length", java_int_type());
486+
length_component.set_pretty_name("length");
487+
length_component.set_base_name("length");
488+
class_type.components().push_back(length_component);
489+
490+
class_typet::componentt data_component(
491+
"data", java_reference_type(java_type_from_char(l)));
492+
data_component.set_pretty_name("data");
493+
data_component.set_base_name("data");
494+
class_type.components().push_back(data_component);
495+
496+
class_type.add_base(symbol_typet("java::java.lang.Object"));
497+
498+
INVARIANT(
499+
is_valid_java_array(class_type),
500+
"Constructed a new type representing a Java Array "
501+
"object that doesn't match expectations");
502+
503+
symbolt symbol;
504+
symbol.name = symbol_type_identifier;
505+
symbol.base_name = symbol_type.get(ID_C_base_name);
506+
symbol.is_type = true;
507+
symbol.type = class_type;
508+
symbol.mode = ID_java;
509+
symbol_table.add(symbol);
510+
511+
// Also provide a clone method:
512+
// ----------------------------
513+
514+
const irep_idt clone_name = identifier + +".clone:()Ljava/lang/Object;";
515+
code_typet::parametert this_param;
516+
this_param.set_identifier(id2string(clone_name) + "::this");
517+
this_param.set_base_name("this");
518+
this_param.set_this();
519+
this_param.type() = java_reference_type(symbol_type);
520+
const code_typet clone_type({this_param}, java_lang_object_type());
521+
522+
parameter_symbolt this_symbol;
523+
this_symbol.name = this_param.get_identifier();
524+
this_symbol.base_name = this_param.get_base_name();
525+
this_symbol.pretty_name = this_symbol.base_name;
526+
this_symbol.type = this_param.type();
527+
this_symbol.mode = ID_java;
528+
symbol_table.add(this_symbol);
529+
530+
const irep_idt local_name = id2string(clone_name) + "::cloned_array";
531+
auxiliary_symbolt local_symbol;
532+
local_symbol.name = local_name;
533+
local_symbol.base_name = "cloned_array";
534+
local_symbol.pretty_name = local_symbol.base_name;
535+
local_symbol.type = java_reference_type(symbol_type);
536+
local_symbol.mode = ID_java;
537+
symbol_table.add(local_symbol);
538+
const auto &local_symexpr = local_symbol.symbol_expr();
539+
540+
code_blockt clone_body;
541+
542+
code_declt declare_cloned(local_symexpr);
543+
clone_body.move_to_operands(declare_cloned);
544+
545+
side_effect_exprt java_new_array(
546+
ID_java_new_array, java_reference_type(symbol_type));
547+
dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
548+
dereference_exprt new_array(local_symexpr, symbol_type);
549+
member_exprt old_length(
550+
old_array, length_component.get_name(), length_component.type());
551+
java_new_array.copy_to_operands(old_length);
552+
code_assignt create_blank(local_symexpr, java_new_array);
553+
clone_body.move_to_operands(create_blank);
554+
555+
member_exprt old_data(
556+
old_array, data_component.get_name(), data_component.type());
557+
member_exprt new_data(
558+
new_array, data_component.get_name(), data_component.type());
559+
560+
// if(l == 'a' && use_array_copy)
561+
// {
562+
// // TODO use this instead of a loop.
563+
// codet array_copy;
564+
// array_copy.set_statement(ID_array_copy);
565+
// array_copy.move_to_operands(new_data);
566+
// array_copy.move_to_operands(old_data);
567+
// clone_body.move_to_operands(array_copy);
568+
// }
569+
// else
570+
{
571+
// Begin for-loop to replace:
572+
573+
const irep_idt index_name = id2string(clone_name) + "::index";
574+
auxiliary_symbolt index_symbol;
575+
index_symbol.name = index_name;
576+
index_symbol.base_name = "index";
577+
index_symbol.pretty_name = index_symbol.base_name;
578+
index_symbol.type = length_component.type();
579+
index_symbol.mode = ID_java;
580+
symbol_table.add(index_symbol);
581+
const auto &index_symexpr = index_symbol.symbol_expr();
582+
583+
code_declt declare_index(index_symexpr);
584+
clone_body.move_to_operands(declare_index);
585+
586+
code_fort copy_loop;
587+
588+
copy_loop.init() =
589+
code_assignt(index_symexpr, from_integer(0, index_symexpr.type()));
590+
copy_loop.cond() =
591+
binary_relation_exprt(index_symexpr, ID_lt, old_length);
592+
593+
side_effect_exprt inc(ID_assign);
594+
inc.operands().resize(2);
595+
inc.op0() = index_symexpr;
596+
inc.op1() =
597+
plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));
598+
copy_loop.iter() = inc;
599+
600+
dereference_exprt old_cell(
601+
plus_exprt(old_data, index_symexpr), old_data.type().subtype());
602+
dereference_exprt new_cell(
603+
plus_exprt(new_data, index_symexpr), new_data.type().subtype());
604+
code_assignt copy_cell(new_cell, old_cell);
605+
copy_loop.body() = copy_cell;
606+
607+
// End for-loop
608+
clone_body.move_to_operands(copy_loop);
609+
}
610+
611+
member_exprt new_base_class(
612+
new_array, base_class_component.get_name(), base_class_component.type());
613+
address_of_exprt retval(new_base_class);
614+
code_returnt return_inst(retval);
615+
clone_body.move_to_operands(return_inst);
616+
617+
symbolt clone_symbol;
618+
clone_symbol.name = clone_name;
619+
clone_symbol.pretty_name = identifier + ".clone:()";
620+
clone_symbol.base_name = "clone";
621+
clone_symbol.type = clone_type;
622+
clone_symbol.value = clone_body;
623+
clone_symbol.mode = ID_java;
624+
symbol_table.add(clone_symbol);
625+
626+
if(l == 'a')
627+
use_array_copy = true;
628+
}
629+
}

‎jbmc/src/java_bytecode/java_utils.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include <unordered_set>
1313

14+
#include <util/arith_tools.h>
1415
#include <util/message.h>
1516
#include <util/std_expr.h>
1617
#include <util/symbol_table.h>
@@ -110,6 +111,8 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
110111

111112
bool is_non_null_library_global(const irep_idt &);
112113

114+
void add_array_types(symbol_tablet &symbol_table);
115+
113116
extern const std::unordered_set<std::string> cprover_methods_to_ignore;
114117

115118
#endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

0 commit comments

Comments
 (0)