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 "java::" + id2string(lambda_entry.second.lambda_method_ref));
433 if(!c.annotations.empty())
434 convert_annotations(c.annotations, class_type.get_annotations());
437 const irep_idt base_name = [](const std::string &full_name) {
438 const size_t last_dot = full_name.find_last_of('.');
439 return last_dot == std::string::npos
441 : std::string(full_name, last_dot + 1, std::string::npos);
442 }(id2string(c.name));
446 new_symbol.base_name = base_name;
447 new_symbol.pretty_name=c.name;
448 new_symbol.name=qualified_classname;
449 class_type.set_name(new_symbol.name);
450 new_symbol.type=class_type;
451 new_symbol.mode=ID_java;
452 new_symbol.is_type=true;
454 symbolt *class_symbol;
457 debug() << "Adding symbol: class '" << c.name << "'" << eom;
458 if(symbol_table.move(new_symbol, class_symbol))
460 error() << "failed to add class symbol " << new_symbol.name << eom;
465 const class_typet::componentst &fields =
466 to_class_type(class_symbol->type).components();
469 for(auto overlay_class : overlay_classes)
471 for(const auto &field : overlay_class.get().fields)
473 std::string field_id = qualified_classname + "." + id2string(field.name);
474 if(check_field_exists(field, field_id, fields))
477 "Duplicate field definition for " + field_id + " in overlay class";
479 error() << err << eom;
483 << "Adding symbol from overlay class: field '" << field.name << "'"
485 convert(*class_symbol, field);
486 POSTCONDITION(check_field_exists(field, field_id, fields));
489 for(const auto &field : c.fields)
491 std::string field_id = qualified_classname + "." + id2string(field.name);
492 if(check_field_exists(field, field_id, fields))
496 << "Field definition for " << field_id
497 << " already loaded from overlay class" << eom;
500 debug() << "Adding symbol: field '" << field.name << "'" << eom;
501 convert(*class_symbol, field);
502 POSTCONDITION(check_field_exists(field, field_id, fields));
506 std::set<irep_idt> overlay_methods;
507 for(auto overlay_class : overlay_classes)
509 for(const methodt &method : overlay_class.get().methods)
511 const irep_idt method_identifier =
512 qualified_classname + "." + id2string(method.name)
513 + ":" + method.descriptor;
514 if(is_ignored_method(c.name, method))
517 << "Ignoring method: '" << method_identifier << "'"
521 if(method_bytecode.contains_method(method_identifier))
528 if(overlay_methods.count(method_identifier) == 0)
533 << "Method " << method_identifier
534 << " exists in an overlay class without being marked as an "
535 "overlay and also exists in another overlay class that appears "
536 "earlier in the classpath"
544 << "Adding symbol from overlay class: method '" << method_identifier
546 java_bytecode_convert_method_lazy(
551 get_message_handler());
552 method_bytecode.add(qualified_classname, method_identifier, method);
553 if(is_overlay_method(method))
554 overlay_methods.insert(method_identifier);
557 for(const methodt &method : c.methods)
559 const irep_idt method_identifier=
560 qualified_classname + "." + id2string(method.name)
561 + ":" + method.descriptor;
562 if(is_ignored_method(c.name, method))
565 << "Ignoring method: '" << method_identifier << "'"
569 if(method_bytecode.contains_method(method_identifier))
575 if(overlay_methods.erase(method_identifier) == 0)
580 << "Method " << method_identifier
581 << " exists in an overlay class without being marked as an overlay "
582 "and also exists in the underlying class"
589 debug() << "Adding symbol: method '" << method_identifier << "'" << eom;
590 java_bytecode_convert_method_lazy(
595 get_message_handler());
596 method_bytecode.add(qualified_classname, method_identifier, method);
597 if(is_overlay_method(method))
600 << "Method " << method_identifier
601 << " marked as an overlay where defined in the underlying class" << eom;
604 if(!overlay_methods.empty())
607 << "Overlay methods defined in overlay classes did not exist in the "
608 "underlying class:\n";
609 for(const irep_idt &method_id : overlay_methods)
610 error() << " " << method_id << "\n";
615 if(c.super_class.empty())
616 java_root_class(*class_symbol);
619 bool java_bytecode_convert_classt::check_field_exists(
620 const java_bytecode_parse_treet::fieldt &field,
621 const irep_idt &qualified_fieldname,
622 const struct_union_typet::componentst &fields) const
625 return symbol_table.has_symbol(qualified_fieldname);
627 auto existing_field = std::find_if(
630 [&field](const struct_union_typet::componentt &f)
632 return f.get_name() == field.name;
634 return existing_field != fields.end();
640 void java_bytecode_convert_classt::convert(
641 symbolt &class_symbol,
645 if(f.signature.has_value())
647 field_type = *java_type_from_string_with_exception(
648 f.descriptor, f.signature, id2string(class_symbol.name));
651 if(is_java_generic_parameter(field_type))
654 std::cout << "fieldtype: generic "
655 << to_java_generic_parameter(field_type).type_variable()
657 << " name " << f.name << "\n";
663 else if(is_java_generic_type(field_type))
665 java_generic_typet &with_gen_type=
666 to_java_generic_type(field_type);
668 std::cout << "fieldtype: generic container type "
669 << std::to_string(with_gen_type.generic_type_arguments().size())
670 << " type " << with_gen_type.id()
671 << " name " << f.name
672 << " subtype id " << with_gen_type.subtype().id() << "\n";
674 field_type=with_gen_type;
678 field_type = *java_type_from_string(f.descriptor);
685 else if(f.is_protected)
686 access = ID_protected;
692 auto &class_type = to_java_class_type(class_symbol.type);
697 const irep_idt field_identifier =
698 id2string(class_symbol.name) + "." + id2string(f.name);
700 class_type.static_members().emplace_back();
701 auto &component = class_type.static_members().back();
703 component.set_name(field_identifier);
704 component.set_base_name(f.name);
705 component.set_pretty_name(f.name);
706 component.set_access(access);
707 component.set_is_final(f.is_final);
708 component.type() = field_type;
713 new_symbol.is_static_lifetime=true;
714 new_symbol.is_lvalue=true;
715 new_symbol.is_state_var=true;
716 new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name);
717 new_symbol.base_name=f.name;
718 new_symbol.type=field_type;
721 set_declaring_class(new_symbol, class_symbol.name);
722 new_symbol.type.set(ID_C_field, f.name);
723 new_symbol.type.set(ID_C_constant, f.is_final);
724 new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
725 "."+id2string(f.name);
726 new_symbol.mode=ID_java;
727 new_symbol.is_type=false;
734 new_symbol.type.set(ID_C_access, ID_public);
735 else if(f.is_protected)
736 new_symbol.type.set(ID_C_access, ID_protected);
737 else if(f.is_private)
738 new_symbol.type.set(ID_C_access, ID_private);
740 new_symbol.type.set(ID_C_access, ID_default);
742 const namespacet ns(symbol_table);
743 const auto value = zero_initializer(field_type, class_symbol.location, ns);
744 if(!value.has_value())
746 error().source_location = class_symbol.location;
747 error() << "failed to zero-initialize " << f.name << eom;
750 new_symbol.value = *value;
753 if(!f.annotations.empty())
757 type_checked_cast<annotated_typet>(new_symbol.type).get_annotations());
761 const auto s_it=symbol_table.symbols.find(new_symbol.name);
762 if(s_it!=symbol_table.symbols.end())
763 symbol_table.erase(s_it);
765 if(symbol_table.add(new_symbol))
766 assert(false && "failed to add static field symbol");
770 class_type.components().emplace_back();
771 auto &component = class_type.components().back();
773 component.set_name(f.name);
774 component.set_base_name(f.name);
775 component.set_pretty_name(f.name);
776 component.set_access(access);
777 component.set_is_final(f.is_final);
778 component.type() = field_type;
781 if(!f.annotations.empty())
785 static_cast<annotated_typet &>(component.type()).get_annotations());
790 void add_java_array_types(symbol_tablet &symbol_table)
792 const std::string letters="ijsbcfdza";
794 for(const char l : letters)
796 struct_tag_typet struct_tag_type =
797 to_struct_tag_type(java_array_type(l).subtype());
799 const irep_idt &struct_tag_type_identifier =
800 struct_tag_type.get_identifier();
801 if(symbol_table.has_symbol(struct_tag_type_identifier))
804 java_class_typet class_type;
807 class_type.set_tag(struct_tag_type_identifier);
812 class_type.set_name(struct_tag_type_identifier);
814 class_type.components().reserve(3);
815 java_class_typet::componentt base_class_component(
816 "@java.lang.Object", struct_tag_typet("java::java.lang.Object"));
817 base_class_component.set_pretty_name("@java.lang.Object");
818 base_class_component.set_base_name("@java.lang.Object");
819 class_type.components().push_back(base_class_component);
821 java_class_typet::componentt length_component("length", java_int_type());
822 length_component.set_pretty_name("length");
823 length_component.set_base_name("length");
824 class_type.components().push_back(length_component);
826 java_class_typet::componentt data_component(
827 "data", java_reference_type(java_type_from_char(l)));
828 data_component.set_pretty_name("data");
829 data_component.set_base_name("data");
830 class_type.components().push_back(data_component);
836 java_class_typet::componentt array_element_classid_component(
837 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME, string_typet());
838 array_element_classid_component.set_pretty_name(
839 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
840 array_element_classid_component.set_base_name(
841 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
842 class_type.components().push_back(array_element_classid_component);
844 java_class_typet::componentt array_dimension_component(
845 JAVA_ARRAY_DIMENSION_FIELD_NAME, java_int_type());
846 array_dimension_component.set_pretty_name(
847 JAVA_ARRAY_DIMENSION_FIELD_NAME);
848 array_dimension_component.set_base_name(JAVA_ARRAY_DIMENSION_FIELD_NAME);
849 class_type.components().push_back(array_dimension_component);
852 class_type.add_base(struct_tag_typet("java::java.lang.Object"));
855 is_valid_java_array(class_type),
856 "Constructed a new type representing a Java Array "
857 "object that doesn't match expectations");
860 symbol.name = struct_tag_type_identifier;
861 symbol.base_name = struct_tag_type.get(ID_C_base_name);
863 symbol.type = class_type;
864 symbol.mode = ID_java;
865 symbol_table.add(symbol);
870 const irep_idt clone_name =
871 id2string(struct_tag_type_identifier) + ".clone:()Ljava/lang/Object;";
872 java_method_typet::parametert this_param(
873 java_reference_type(struct_tag_type));
874 this_param.set_identifier(id2string(clone_name)+"::this");
875 this_param.set_base_name(ID_this);
876 this_param.set_this();
877 const java_method_typet clone_type({this_param}, java_lang_object_type());
879 parameter_symbolt this_symbol;
880 this_symbol.name=this_param.get_identifier();
881 this_symbol.base_name=this_param.get_base_name();
882 this_symbol.pretty_name=this_symbol.base_name;
883 this_symbol.type=this_param.type();
884 this_symbol.mode=ID_java;
885 symbol_table.add(this_symbol);
887 const irep_idt local_name=
888 id2string(clone_name)+"::cloned_array";
889 auxiliary_symbolt local_symbol;
890 local_symbol.name=local_name;
891 local_symbol.base_name="cloned_array";
892 local_symbol.pretty_name=local_symbol.base_name;
893 local_symbol.type = java_reference_type(struct_tag_type);
894 local_symbol.mode=ID_java;
895 symbol_table.add(local_symbol);
896 const auto local_symexpr = local_symbol.symbol_expr();
898 code_declt declare_cloned(local_symexpr);
900 source_locationt location;
901 location.set_function(local_name);
902 side_effect_exprt java_new_array(
903 ID_java_new_array, java_reference_type(struct_tag_type), location);
904 dereference_exprt old_array{this_symbol.symbol_expr()};
905 dereference_exprt new_array{local_symexpr};
906 member_exprt old_length(
907 old_array, length_component.get_name(), length_component.type());
908 java_new_array.copy_to_operands(old_length);
909 code_assignt create_blank(local_symexpr, java_new_array);
911 codet copy_type_information = code_skipt();
916 const auto &array_dimension_component =
917 class_type.get_component(JAVA_ARRAY_DIMENSION_FIELD_NAME);
918 const auto &array_element_classid_component =
919 class_type.get_component(JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
921 member_exprt old_array_dimension(old_array, array_dimension_component);
922 member_exprt old_array_element_classid(
923 old_array, array_element_classid_component);
925 member_exprt new_array_dimension(new_array, array_dimension_component);
926 member_exprt new_array_element_classid(
927 new_array, array_element_classid_component);
929 copy_type_information = code_blockt{
930 {code_assignt(new_array_dimension, old_array_dimension),
931 code_assignt(new_array_element_classid, old_array_element_classid)}};
934 member_exprt old_data(
935 old_array, data_component.get_name(), data_component.type());
936 member_exprt new_data(
937 new_array, data_component.get_name(), data_component.type());
949 const irep_idt index_name=
950 id2string(clone_name)+"::index";
951 auxiliary_symbolt index_symbol;
952 index_symbol.name=index_name;
953 index_symbol.base_name="index";
954 index_symbol.pretty_name=index_symbol.base_name;
955 index_symbol.type = length_component.type();
956 index_symbol.mode=ID_java;
957 symbol_table.add(index_symbol);
958 const auto &index_symexpr=index_symbol.symbol_expr();
960 code_declt declare_index(index_symexpr);
962 dereference_exprt old_cell(
963 plus_exprt(old_data, index_symexpr), old_data.type().subtype());
964 dereference_exprt new_cell(
965 plus_exprt(new_data, index_symexpr), new_data.type().subtype());
967 const code_fort copy_loop = code_fort::from_index_bounds(
968 from_integer(0, index_symexpr.type()),
971 code_assignt(std::move(new_cell), std::move(old_cell)),
974 member_exprt new_base_class(
975 new_array, base_class_component.get_name(), base_class_component.type());
976 address_of_exprt retval(new_base_class);
977 code_returnt return_inst(retval);
979 const code_blockt clone_body({declare_cloned,
981 copy_type_information,
986 symbolt clone_symbol;
987 clone_symbol.name=clone_name;
988 clone_symbol.pretty_name =
989 id2string(struct_tag_type_identifier) + ".clone:()";
990 clone_symbol.base_name="clone";
991 clone_symbol.type=clone_type;
992 clone_symbol.value=clone_body;
993 clone_symbol.mode=ID_java;
994 symbol_table.add(clone_symbol);
998 bool java_bytecode_convert_class(
999 const java_class_loadert::parse_tree_with_overlayst &parse_trees,
1000 symbol_tablet &symbol_table,
1001 message_handlert &message_handler,
1002 size_t max_array_length,
1003 method_bytecodet &method_bytecode,
1004 java_string_library_preprocesst &string_preprocess,
1005 const std::unordered_set<std::string> &no_load_classes)
1007 java_bytecode_convert_classt java_bytecode_convert_class(
1017 java_bytecode_convert_class(parse_trees);
1025 catch(const char *e)
1027 java_bytecode_convert_class.error() << e << messaget::eom;
1030 catch(const std::string &e)
1032 java_bytecode_convert_class.error() << e << messaget::eom;
1038 static std::string get_final_name_component(const std::string &name)
1040 return name.substr(name.rfind("::") + 2);
1043 static std::string get_without_final_name_component(const std::string &name)
1045 return name.substr(0, name.rfind("::"));
1060 static void find_and_replace_parameter(
1061 java_generic_parametert ¶meter,
1062 const std::vector<java_generic_parametert> &replacement_parameters)
1065 const std::string ¶meter_full_name =
1066 id2string(parameter.type_variable_ref().get_identifier());
1067 const std::string parameter_name =
1068 get_final_name_component(parameter_full_name);
1071 const auto replacement_parameter_it = std::find_if(
1072 replacement_parameters.begin(),
1073 replacement_parameters.end(),
1074 [¶meter_name](const java_generic_parametert &replacement_param) {
1075 return parameter_name ==
1076 get_final_name_component(
1077 id2string(replacement_param.type_variable().get_identifier()));
1079 if(replacement_parameter_it == replacement_parameters.end())
1083 const std::string &replacement_parameter_full_name =
1084 id2string(replacement_parameter_it->type_variable().get_identifier());
1087 PRECONDITION(has_prefix(
1088 replacement_parameter_full_name,
1089 get_without_final_name_component(parameter_full_name)));
1091 parameter.type_variable_ref().set_identifier(replacement_parameter_full_name);
1099 static void find_and_replace_parameters(
1101 const std::vector<java_generic_parametert> &replacement_parameters)
1103 if(is_java_generic_parameter(type))
1105 find_and_replace_parameter(
1106 to_java_generic_parameter(type), replacement_parameters);
1108 else if(is_java_generic_type(type))
1110 java_generic_typet &generic_type = to_java_generic_type(type);
1111 std::vector<reference_typet> &arguments =
1112 generic_type.generic_type_arguments();
1113 for(auto &argument : arguments)
1115 find_and_replace_parameters(argument, replacement_parameters);
1118 else if(is_java_generic_struct_tag_type(type))
1120 java_generic_struct_tag_typet &generic_base =
1121 to_java_generic_struct_tag_type(type);
1122 std::vector<reference_typet> &gen_types = generic_base.generic_types();
1123 for(auto &gen_type : gen_types)
1125 find_and_replace_parameters(gen_type, replacement_parameters);
1133 void convert_annotations(
1134 const java_bytecode_parse_treet::annotationst &parsed_annotations,
1135 std::vector<java_annotationt> &java_annotations)
1137 for(const auto &annotation : parsed_annotations)
1139 java_annotations.emplace_back(annotation.type);
1140 std::vector<java_annotationt::valuet> &values =
1141 java_annotations.back().get_values();
1143 annotation.element_value_pairs.begin(),
1144 annotation.element_value_pairs.end(),
1145 std::back_inserter(values),
1146 [](const decltype(annotation.element_value_pairs)::value_type &value) {
1147 return java_annotationt::valuet(value.element_name, value.value);
1156 void convert_java_annotations(
1157 const std::vector<java_annotationt> &java_annotations,
1158 java_bytecode_parse_treet::annotationst &annotations)
1160 for(const auto &java_annotation : java_annotations)
1162 annotations.emplace_back(java_bytecode_parse_treet::annotationt());
1163 auto &annotation = annotations.back();
1164 annotation.type = java_annotation.get_type();
1167 java_annotation.get_values().begin(),
1168 java_annotation.get_values().end(),
1169 std::back_inserter(annotation.element_value_pairs),
1170 [](const java_annotationt::valuet &value)
1171 -> java_bytecode_parse_treet::annotationt::element_value_pairt {
1172 return {value.get_name(), value.get_value()};
1181 void mark_java_implicitly_generic_class_type(
1182 const irep_idt &class_name,
1183 symbol_tablet &symbol_table)
1185 const std::string qualified_class_name = "java::" + id2string(class_name);
1186 PRECONDITION(symbol_table.has_symbol(qualified_class_name));
1188 symbolt &class_symbol = symbol_table.get_writeable_ref(qualified_class_name);
1189 const java_class_typet &class_type = to_java_class_type(class_symbol.type);
1194 bool no_this_field = std::none_of(
1195 class_type.components().begin(),
1196 class_type.components().end(),
1197 [](const struct_union_typet::componentt &component)
1199 return id2string(component.get_name()).substr(0, 5) == "this$";
1208 std::vector<java_generic_parametert> implicit_generic_type_parameters;
1209 std::string::size_type outer_class_delimiter =
1210 qualified_class_name.rfind('$');
1211 while(outer_class_delimiter != std::string::npos)
1213 std::string outer_class_name =
1214 qualified_class_name.substr(0, outer_class_delimiter);
1215 if(symbol_table.has_symbol(outer_class_name))
1217 const symbolt &outer_class_symbol =
1218 symbol_table.lookup_ref(outer_class_name);
1219 const java_class_typet &outer_class_type =
1220 to_java_class_type(outer_class_symbol.type);
1221 if(is_java_generic_class_type(outer_class_type))
1223 for(const java_generic_parametert &outer_generic_type_parameter :
1224 to_java_generic_class_type(outer_class_type).generic_types())
1228 irep_idt identifier = qualified_class_name + "::" +
1229 id2string(strip_java_namespace_prefix(
1230 outer_generic_type_parameter.get_name()));
1231 java_generic_parameter_tagt bound = to_java_generic_parameter_tag(
1232 outer_generic_type_parameter.subtype());
1233 bound.type_variable_ref().set_identifier(identifier);
1234 implicit_generic_type_parameters.emplace_back(identifier, bound);
1237 outer_class_delimiter = outer_class_name.rfind('$');
1241 throw missing_outer_class_symbol_exceptiont(
1242 outer_class_name, qualified_class_name);
1248 if(!implicit_generic_type_parameters.empty())
1250 java_implicitly_generic_class_typet new_class_type(
1251 class_type, implicit_generic_type_parameters);
1254 if(is_java_generic_class_type(class_type))
1256 const java_generic_class_typet::generic_typest &class_type_params =
1257 to_java_generic_class_type(class_type).generic_types();
1258 implicit_generic_type_parameters.insert(
1259 implicit_generic_type_parameters.begin(),
1260 class_type_params.begin(),
1261 class_type_params.end());
1264 for(auto &field : new_class_type.components())
1266 find_and_replace_parameters(
1267 field.type(), implicit_generic_type_parameters);
1270 for(auto &base : new_class_type.bases())
1272 find_and_replace_parameters(
1273 base.type(), implicit_generic_type_parameters);
1276 class_symbol.type = new_class_type;