40 size_t _max_array_length,
77 const bool loading_success =
83 for(
auto overlay_class_it = std::next(parse_trees.begin());
84 overlay_class_it != parse_trees.end();
87 overlay_classes.push_front(std::cref(overlay_class_it->parsed_class));
96 else if(!loading_success)
164 static irep_idt org_cprover_CProver_name =
"org.cprover.CProver";
166 (class_name == org_cprover_CProver_name &&
173 const irep_idt &qualified_fieldname,
192 if(signature.has_value())
197 signature.value().front() ==
'<'
204 const std::string superclass_ref =
205 signature.value().substr(start, (end - start) + 1);
211 if(superclass_ref.find(
'<') != std::string::npos)
212 return superclass_ref;
231 const std::string &interface_name)
233 if(signature.has_value())
238 signature.value().front() ==
'<'
248 std::string interface_name_slash_to_dot = interface_name;
250 interface_name_slash_to_dot.begin(),
251 interface_name_slash_to_dot.end(),
256 signature.value().find(
"L" + interface_name_slash_to_dot +
"<", start);
257 if(start != std::string::npos)
261 return signature.value().substr(start, (end - start) + 1);
277 debug() <<
"Skip class " << c.
name <<
" (already loaded)" <<
eom;
286 std::cout <<
"INFO: found generic class signature "
288 <<
" in parsed class "
296 for(
const typet &t : generic_types)
301 class_type=generic_class_type;
306 <<
"\n could not parse signature: " << c.
signature.value()
307 <<
"\n " << e.what() <<
"\n ignoring that the class is generic"
328 warning() <<
"Java Enum " << c.
name <<
" won't work properly because max "
333 ID_java_enum_static_unwind,
357 if(superclass_ref.has_value())
362 base, superclass_ref.value(), qualified_classname);
368 <<
"\n could not parse signature: " << superclass_ref.value()
370 <<
"\n ignoring that the superclass is generic" <<
eom;
379 base_class_field.type() = class_type.
bases().at(0).type();
383 class_type.
components().push_back(base_class_field);
397 if(interface_ref.has_value())
402 base, interface_ref.value(), qualified_classname);
407 debug() <<
"Interface: " <<
interface << " of class: " << c.name
408 << "\n could not parse signature: " << interface_ref.value()
410 << "\n ignoring that the interface is generic" << eom;
411 class_type.add_base(base);
416 class_type.add_base(base);
421 for(const auto &lambda_entry : c.lambda_method_handle_map)
426 lambda_entry.second.is_unknown_handle()
427 ? class_type.add_unknown_lambda_method_handle()
428 : class_type.add_lambda_method_handle(
429 lambda_entry.second.get_method_descriptor(),
430 lambda_entry.second.handle_type);
434 if(!c.annotations.empty())
435 convert_annotations(c.annotations, class_type.get_annotations());
438 const irep_idt base_name = [](const std::string &full_name) {
439 const size_t last_dot = full_name.find_last_of('.');
440 return last_dot == std::string::npos
442 : std::string(full_name, last_dot + 1, std::string::npos);
443 }(id2string(c.name));
447 new_symbol.base_name = base_name;
448 new_symbol.pretty_name=c.name;
449 new_symbol.name=qualified_classname;
450 class_type.set_name(new_symbol.name);
451 new_symbol.type=class_type;
452 new_symbol.mode=ID_java;
453 new_symbol.is_type=true;
455 symbolt *class_symbol;
458 debug() << "Adding symbol: class '" << c.name << "'" << eom;
459 if(symbol_table.move(new_symbol, class_symbol))
461 error() << "failed to add class symbol " << new_symbol.name << eom;
466 const class_typet::componentst &fields =
467 to_class_type(class_symbol->type).components();
470 for(auto overlay_class : overlay_classes)
472 for(const auto &field : overlay_class.get().fields)
474 std::string field_id = qualified_classname + "." + id2string(field.name);
475 if(check_field_exists(field, field_id, fields))
478 "Duplicate field definition for " + field_id + " in overlay class";
480 error() << err << eom;
484 << "Adding symbol from overlay class: field '" << field.name << "'"
486 convert(*class_symbol, field);
487 POSTCONDITION(check_field_exists(field, field_id, fields));
490 for(const auto &field : c.fields)
492 std::string field_id = qualified_classname + "." + id2string(field.name);
493 if(check_field_exists(field, field_id, fields))
497 << "Field definition for " << field_id
498 << " already loaded from overlay class" << eom;
501 debug() << "Adding symbol: field '" << field.name << "'" << eom;
502 convert(*class_symbol, field);
503 POSTCONDITION(check_field_exists(field, field_id, fields));
507 std::set<irep_idt> overlay_methods;
508 for(auto overlay_class : overlay_classes)
510 for(const methodt &method : overlay_class.get().methods)
512 const irep_idt method_identifier =
513 qualified_classname + "." + id2string(method.name)
514 + ":" + method.descriptor;
515 if(is_ignored_method(c.name, method))
518 << "Ignoring method: '" << method_identifier << "'"
522 if(method_bytecode.contains_method(method_identifier))
529 if(overlay_methods.count(method_identifier) == 0)
534 << "Method " << method_identifier
535 << " exists in an overlay class without being marked as an "
536 "overlay and also exists in another overlay class that appears "
537 "earlier in the classpath"
545 << "Adding symbol from overlay class: method '" << method_identifier
547 java_bytecode_convert_method_lazy(
552 get_message_handler());
553 method_bytecode.add(qualified_classname, method_identifier, method);
554 if(is_overlay_method(method))
555 overlay_methods.insert(method_identifier);
558 for(const methodt &method : c.methods)
560 const irep_idt method_identifier=
561 qualified_classname + "." + id2string(method.name)
562 + ":" + method.descriptor;
563 if(is_ignored_method(c.name, method))
566 << "Ignoring method: '" << method_identifier << "'"
570 if(method_bytecode.contains_method(method_identifier))
576 if(overlay_methods.erase(method_identifier) == 0)
581 << "Method " << method_identifier
582 << " exists in an overlay class without being marked as an overlay "
583 "and also exists in the underlying class"
590 debug() << "Adding symbol: method '" << method_identifier << "'" << eom;
591 java_bytecode_convert_method_lazy(
596 get_message_handler());
597 method_bytecode.add(qualified_classname, method_identifier, method);
598 if(is_overlay_method(method))
601 << "Method " << method_identifier
602 << " marked as an overlay where defined in the underlying class" << eom;
605 if(!overlay_methods.empty())
608 << "Overlay methods defined in overlay classes did not exist in the "
609 "underlying class:\n";
610 for(const irep_idt &method_id : overlay_methods)
611 error() << " " << method_id << "\n";
616 if(c.super_class.empty())
617 java_root_class(*class_symbol);
620 bool java_bytecode_convert_classt::check_field_exists(
621 const java_bytecode_parse_treet::fieldt &field,
622 const irep_idt &qualified_fieldname,
623 const struct_union_typet::componentst &fields) const
626 return symbol_table.has_symbol(qualified_fieldname);
628 auto existing_field = std::find_if(
631 [&field](const struct_union_typet::componentt &f)
633 return f.get_name() == field.name;
635 return existing_field != fields.end();
641 void java_bytecode_convert_classt::convert(
642 symbolt &class_symbol,
646 if(f.signature.has_value())
648 field_type = *java_type_from_string_with_exception(
649 f.descriptor, f.signature, id2string(class_symbol.name));
652 if(is_java_generic_parameter(field_type))
655 std::cout << "fieldtype: generic "
656 << to_java_generic_parameter(field_type).type_variable()
658 << " name " << f.name << "\n";
664 else if(is_java_generic_type(field_type))
666 java_generic_typet &with_gen_type=
667 to_java_generic_type(field_type);
669 std::cout << "fieldtype: generic container type "
670 << std::to_string(with_gen_type.generic_type_arguments().size())
671 << " type " << with_gen_type.id()
672 << " name " << f.name
673 << " subtype id " << with_gen_type.subtype().id() << "\n";
675 field_type=with_gen_type;
679 field_type = *java_type_from_string(f.descriptor);
686 else if(f.is_protected)
687 access = ID_protected;
693 auto &class_type = to_java_class_type(class_symbol.type);
698 const irep_idt field_identifier =
699 id2string(class_symbol.name) + "." + id2string(f.name);
701 class_type.static_members().emplace_back();
702 auto &component = class_type.static_members().back();
704 component.set_name(field_identifier);
705 component.set_base_name(f.name);
706 component.set_pretty_name(f.name);
707 component.set_access(access);
708 component.set_is_final(f.is_final);
709 component.type() = field_type;
714 new_symbol.is_static_lifetime=true;
715 new_symbol.is_lvalue=true;
716 new_symbol.is_state_var=true;
717 new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name);
718 new_symbol.base_name=f.name;
719 new_symbol.type=field_type;
722 set_declaring_class(new_symbol, class_symbol.name);
723 new_symbol.type.set(ID_C_field, f.name);
724 new_symbol.type.set(ID_C_constant, f.is_final);
725 new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
726 "."+id2string(f.name);
727 new_symbol.mode=ID_java;
728 new_symbol.is_type=false;
735 new_symbol.type.set(ID_C_access, ID_public);
736 else if(f.is_protected)
737 new_symbol.type.set(ID_C_access, ID_protected);
738 else if(f.is_private)
739 new_symbol.type.set(ID_C_access, ID_private);
741 new_symbol.type.set(ID_C_access, ID_default);
743 const namespacet ns(symbol_table);
744 const auto value = zero_initializer(field_type, class_symbol.location, ns);
745 if(!value.has_value())
747 error().source_location = class_symbol.location;
748 error() << "failed to zero-initialize " << f.name << eom;
751 new_symbol.value = *value;
754 if(!f.annotations.empty())
758 type_checked_cast<annotated_typet>(new_symbol.type).get_annotations());
762 const auto s_it=symbol_table.symbols.find(new_symbol.name);
763 if(s_it!=symbol_table.symbols.end())
764 symbol_table.erase(s_it);
766 if(symbol_table.add(new_symbol))
767 assert(false && "failed to add static field symbol");
771 class_type.components().emplace_back();
772 auto &component = class_type.components().back();
774 component.set_name(f.name);
775 component.set_base_name(f.name);
776 component.set_pretty_name(f.name);
777 component.set_access(access);
778 component.set_is_final(f.is_final);
779 component.type() = field_type;
782 if(!f.annotations.empty())
786 static_cast<annotated_typet &>(component.type()).get_annotations());
791 void add_java_array_types(symbol_tablet &symbol_table)
793 const std::string letters="ijsbcfdza";
795 for(const char l : letters)
797 struct_tag_typet struct_tag_type =
798 to_struct_tag_type(java_array_type(l).subtype());
800 const irep_idt &struct_tag_type_identifier =
801 struct_tag_type.get_identifier();
802 if(symbol_table.has_symbol(struct_tag_type_identifier))
805 java_class_typet class_type;
808 class_type.set_tag(struct_tag_type_identifier);
813 class_type.set_name(struct_tag_type_identifier);
815 class_type.components().reserve(3);
816 java_class_typet::componentt base_class_component(
817 "@java.lang.Object", struct_tag_typet("java::java.lang.Object"));
818 base_class_component.set_pretty_name("@java.lang.Object");
819 base_class_component.set_base_name("@java.lang.Object");
820 class_type.components().push_back(base_class_component);
822 java_class_typet::componentt length_component("length", java_int_type());
823 length_component.set_pretty_name("length");
824 length_component.set_base_name("length");
825 class_type.components().push_back(length_component);
827 java_class_typet::componentt data_component(
828 "data", java_reference_type(java_type_from_char(l)));
829 data_component.set_pretty_name("data");
830 data_component.set_base_name("data");
831 class_type.components().push_back(data_component);
837 java_class_typet::componentt array_element_classid_component(
838 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME, string_typet());
839 array_element_classid_component.set_pretty_name(
840 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
841 array_element_classid_component.set_base_name(
842 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
843 class_type.components().push_back(array_element_classid_component);
845 java_class_typet::componentt array_dimension_component(
846 JAVA_ARRAY_DIMENSION_FIELD_NAME, java_int_type());
847 array_dimension_component.set_pretty_name(
848 JAVA_ARRAY_DIMENSION_FIELD_NAME);
849 array_dimension_component.set_base_name(JAVA_ARRAY_DIMENSION_FIELD_NAME);
850 class_type.components().push_back(array_dimension_component);
853 class_type.add_base(struct_tag_typet("java::java.lang.Object"));
856 is_valid_java_array(class_type),
857 "Constructed a new type representing a Java Array "
858 "object that doesn't match expectations");
861 symbol.name = struct_tag_type_identifier;
862 symbol.base_name = struct_tag_type.get(ID_C_base_name);
864 symbol.type = class_type;
865 symbol.mode = ID_java;
866 symbol_table.add(symbol);
871 const irep_idt clone_name =
872 id2string(struct_tag_type_identifier) + ".clone:()Ljava/lang/Object;";
873 java_method_typet::parametert this_param(
874 java_reference_type(struct_tag_type));
875 this_param.set_identifier(id2string(clone_name)+"::this");
876 this_param.set_base_name(ID_this);
877 this_param.set_this();
878 const java_method_typet clone_type({this_param}, java_lang_object_type());
880 parameter_symbolt this_symbol;
881 this_symbol.name=this_param.get_identifier();
882 this_symbol.base_name=this_param.get_base_name();
883 this_symbol.pretty_name=this_symbol.base_name;
884 this_symbol.type=this_param.type();
885 this_symbol.mode=ID_java;
886 symbol_table.add(this_symbol);
888 const irep_idt local_name=
889 id2string(clone_name)+"::cloned_array";
890 auxiliary_symbolt local_symbol;
891 local_symbol.name=local_name;
892 local_symbol.base_name="cloned_array";
893 local_symbol.pretty_name=local_symbol.base_name;
894 local_symbol.type = java_reference_type(struct_tag_type);
895 local_symbol.mode=ID_java;
896 symbol_table.add(local_symbol);
897 const auto local_symexpr = local_symbol.symbol_expr();
899 code_declt declare_cloned(local_symexpr);
901 source_locationt location;
902 location.set_function(local_name);
903 side_effect_exprt java_new_array(
904 ID_java_new_array, java_reference_type(struct_tag_type), location);
905 dereference_exprt old_array{this_symbol.symbol_expr()};
906 dereference_exprt new_array{local_symexpr};
907 member_exprt old_length(
908 old_array, length_component.get_name(), length_component.type());
909 java_new_array.copy_to_operands(old_length);
910 code_assignt create_blank(local_symexpr, java_new_array);
912 codet copy_type_information = code_skipt();
917 const auto &array_dimension_component =
918 class_type.get_component(JAVA_ARRAY_DIMENSION_FIELD_NAME);
919 const auto &array_element_classid_component =
920 class_type.get_component(JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
922 member_exprt old_array_dimension(old_array, array_dimension_component);
923 member_exprt old_array_element_classid(
924 old_array, array_element_classid_component);
926 member_exprt new_array_dimension(new_array, array_dimension_component);
927 member_exprt new_array_element_classid(
928 new_array, array_element_classid_component);
930 copy_type_information = code_blockt{
931 {code_assignt(new_array_dimension, old_array_dimension),
932 code_assignt(new_array_element_classid, old_array_element_classid)}};
935 member_exprt old_data(
936 old_array, data_component.get_name(), data_component.type());
937 member_exprt new_data(
938 new_array, data_component.get_name(), data_component.type());
950 const irep_idt index_name=
951 id2string(clone_name)+"::index";
952 auxiliary_symbolt index_symbol;
953 index_symbol.name=index_name;
954 index_symbol.base_name="index";
955 index_symbol.pretty_name=index_symbol.base_name;
956 index_symbol.type = length_component.type();
957 index_symbol.mode=ID_java;
958 symbol_table.add(index_symbol);
959 const auto &index_symexpr=index_symbol.symbol_expr();
961 code_declt declare_index(index_symexpr);
963 dereference_exprt old_cell(
964 plus_exprt(old_data, index_symexpr), old_data.type().subtype());
965 dereference_exprt new_cell(
966 plus_exprt(new_data, index_symexpr), new_data.type().subtype());
968 const code_fort copy_loop = code_fort::from_index_bounds(
969 from_integer(0, index_symexpr.type()),
972 code_assignt(std::move(new_cell), std::move(old_cell)),
975 member_exprt new_base_class(
976 new_array, base_class_component.get_name(), base_class_component.type());
977 address_of_exprt retval(new_base_class);
978 code_returnt return_inst(retval);
980 const code_blockt clone_body({declare_cloned,
982 copy_type_information,
987 symbolt clone_symbol;
988 clone_symbol.name=clone_name;
989 clone_symbol.pretty_name =
990 id2string(struct_tag_type_identifier) + ".clone:()";
991 clone_symbol.base_name="clone";
992 clone_symbol.type=clone_type;
993 clone_symbol.value=clone_body;
994 clone_symbol.mode=ID_java;
995 symbol_table.add(clone_symbol);
999 bool java_bytecode_convert_class(
1000 const java_class_loadert::parse_tree_with_overlayst &parse_trees,
1001 symbol_tablet &symbol_table,
1002 message_handlert &message_handler,
1003 size_t max_array_length,
1004 method_bytecodet &method_bytecode,
1005 java_string_library_preprocesst &string_preprocess,
1006 const std::unordered_set<std::string> &no_load_classes)
1008 java_bytecode_convert_classt java_bytecode_convert_class(
1018 java_bytecode_convert_class(parse_trees);
1026 catch(const char *e)
1028 java_bytecode_convert_class.error() << e << messaget::eom;
1031 catch(const std::string &e)
1033 java_bytecode_convert_class.error() << e << messaget::eom;
1039 static std::string get_final_name_component(const std::string &name)
1041 return name.substr(name.rfind("::") + 2);
1044 static std::string get_without_final_name_component(const std::string &name)
1046 return name.substr(0, name.rfind("::"));
1061 static void find_and_replace_parameter(
1062 java_generic_parametert ¶meter,
1063 const std::vector<java_generic_parametert> &replacement_parameters)
1066 const std::string ¶meter_full_name =
1067 id2string(parameter.type_variable_ref().get_identifier());
1068 const std::string parameter_name =
1069 get_final_name_component(parameter_full_name);
1072 const auto replacement_parameter_it = std::find_if(
1073 replacement_parameters.begin(),
1074 replacement_parameters.end(),
1075 [¶meter_name](const java_generic_parametert &replacement_param) {
1076 return parameter_name ==
1077 get_final_name_component(
1078 id2string(replacement_param.type_variable().get_identifier()));
1080 if(replacement_parameter_it == replacement_parameters.end())
1084 const std::string &replacement_parameter_full_name =
1085 id2string(replacement_parameter_it->type_variable().get_identifier());
1088 PRECONDITION(has_prefix(
1089 replacement_parameter_full_name,
1090 get_without_final_name_component(parameter_full_name)));
1092 parameter.type_variable_ref().set_identifier(replacement_parameter_full_name);
1100 static void find_and_replace_parameters(
1102 const std::vector<java_generic_parametert> &replacement_parameters)
1104 if(is_java_generic_parameter(type))
1106 find_and_replace_parameter(
1107 to_java_generic_parameter(type), replacement_parameters);
1109 else if(is_java_generic_type(type))
1111 java_generic_typet &generic_type = to_java_generic_type(type);
1112 std::vector<reference_typet> &arguments =
1113 generic_type.generic_type_arguments();
1114 for(auto &argument : arguments)
1116 find_and_replace_parameters(argument, replacement_parameters);
1119 else if(is_java_generic_struct_tag_type(type))
1121 java_generic_struct_tag_typet &generic_base =
1122 to_java_generic_struct_tag_type(type);
1123 std::vector<reference_typet> &gen_types = generic_base.generic_types();
1124 for(auto &gen_type : gen_types)
1126 find_and_replace_parameters(gen_type, replacement_parameters);
1134 void convert_annotations(
1135 const java_bytecode_parse_treet::annotationst &parsed_annotations,
1136 std::vector<java_annotationt> &java_annotations)
1138 for(const auto &annotation : parsed_annotations)
1140 java_annotations.emplace_back(annotation.type);
1141 std::vector<java_annotationt::valuet> &values =
1142 java_annotations.back().get_values();
1144 annotation.element_value_pairs.begin(),
1145 annotation.element_value_pairs.end(),
1146 std::back_inserter(values),
1147 [](const decltype(annotation.element_value_pairs)::value_type &value) {
1148 return java_annotationt::valuet(value.element_name, value.value);
1157 void convert_java_annotations(
1158 const std::vector<java_annotationt> &java_annotations,
1159 java_bytecode_parse_treet::annotationst &annotations)
1161 for(const auto &java_annotation : java_annotations)
1163 annotations.emplace_back(java_bytecode_parse_treet::annotationt());
1164 auto &annotation = annotations.back();
1165 annotation.type = java_annotation.get_type();
1168 java_annotation.get_values().begin(),
1169 java_annotation.get_values().end(),
1170 std::back_inserter(annotation.element_value_pairs),
1171 [](const java_annotationt::valuet &value)
1172 -> java_bytecode_parse_treet::annotationt::element_value_pairt {
1173 return {value.get_name(), value.get_value()};
1182 void mark_java_implicitly_generic_class_type(
1183 const irep_idt &class_name,
1184 symbol_tablet &symbol_table)
1186 const std::string qualified_class_name = "java::" + id2string(class_name);
1187 PRECONDITION(symbol_table.has_symbol(qualified_class_name));
1189 symbolt &class_symbol = symbol_table.get_writeable_ref(qualified_class_name);
1190 const java_class_typet &class_type = to_java_class_type(class_symbol.type);
1195 bool no_this_field = std::none_of(
1196 class_type.components().begin(),
1197 class_type.components().end(),
1198 [](const struct_union_typet::componentt &component)
1200 return id2string(component.get_name()).substr(0, 5) == "this$";
1209 std::vector<java_generic_parametert> implicit_generic_type_parameters;
1210 std::string::size_type outer_class_delimiter =
1211 qualified_class_name.rfind('$');
1212 while(outer_class_delimiter != std::string::npos)
1214 std::string outer_class_name =
1215 qualified_class_name.substr(0, outer_class_delimiter);
1216 if(symbol_table.has_symbol(outer_class_name))
1218 const symbolt &outer_class_symbol =
1219 symbol_table.lookup_ref(outer_class_name);
1220 const java_class_typet &outer_class_type =
1221 to_java_class_type(outer_class_symbol.type);
1222 if(is_java_generic_class_type(outer_class_type))
1224 for(const java_generic_parametert &outer_generic_type_parameter :
1225 to_java_generic_class_type(outer_class_type).generic_types())
1229 irep_idt identifier = qualified_class_name + "::" +
1230 id2string(strip_java_namespace_prefix(
1231 outer_generic_type_parameter.get_name()));
1232 java_generic_parameter_tagt bound = to_java_generic_parameter_tag(
1233 outer_generic_type_parameter.subtype());
1234 bound.type_variable_ref().set_identifier(identifier);
1235 implicit_generic_type_parameters.emplace_back(identifier, bound);
1238 outer_class_delimiter = outer_class_name.rfind('$');
1242 throw missing_outer_class_symbol_exceptiont(
1243 outer_class_name, qualified_class_name);
1249 if(!implicit_generic_type_parameters.empty())
1251 java_implicitly_generic_class_typet new_class_type(
1252 class_type, implicit_generic_type_parameters);
1255 if(is_java_generic_class_type(class_type))
1257 const java_generic_class_typet::generic_typest &class_type_params =
1258 to_java_generic_class_type(class_type).generic_types();
1259 implicit_generic_type_parameters.insert(
1260 implicit_generic_type_parameters.begin(),
1261 class_type_params.begin(),
1262 class_type_params.end());
1265 for(auto &field : new_class_type.components())
1267 find_and_replace_parameters(
1268 field.type(), implicit_generic_type_parameters);
1271 for(auto &base : new_class_type.bases())
1273 find_and_replace_parameters(
1274 base.type(), implicit_generic_type_parameters);
1277 class_symbol.type = new_class_type;