40 size_t _max_array_length,
44 :
log(_message_handler),
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)
165 static irep_idt org_cprover_CProver_name =
"org.cprover.CProver";
167 (class_name == org_cprover_CProver_name &&
174 const irep_idt &qualified_fieldname,
193 if(signature.has_value())
198 signature.value().front() ==
'<'
205 const std::string superclass_ref =
206 signature.value().substr(start, (end - start) + 1);
212 if(superclass_ref.find(
'<') != std::string::npos)
213 return superclass_ref;
232 const std::string &interface_name)
234 if(signature.has_value())
239 signature.value().front() ==
'<'
249 std::string interface_name_slash_to_dot = interface_name;
251 interface_name_slash_to_dot.begin(),
252 interface_name_slash_to_dot.end(),
257 signature.value().find(
"L" + interface_name_slash_to_dot +
"<", start);
258 if(start != std::string::npos)
262 return signature.value().substr(start, (end - start) + 1);
278 log.
debug() <<
"Skip class " << c.
name <<
" (already loaded)"
288 std::cout <<
"INFO: found generic class signature "
290 <<
" in parsed class "
298 for(
const typet &t : generic_types)
303 class_type=generic_class_type;
308 <<
"\n could not parse signature: " << c.
signature.value()
331 <<
" won't work properly because max "
333 <<
") is less than the "
337 ID_java_enum_static_unwind,
361 if(superclass_ref.has_value())
366 base, superclass_ref.value(), qualified_classname);
372 <<
" of class: " << c.
name
373 <<
"\n could not parse signature: "
374 << superclass_ref.value() <<
"\n " << e.what()
375 <<
"\n ignoring that the superclass is generic"
385 base_class_field.type() = class_type.
bases().at(0).type();
389 class_type.
components().push_back(base_class_field);
403 if(interface_ref.has_value())
408 base, interface_ref.value(), qualified_classname);
413 log.
debug() <<
"Interface: " <<
interface << " of class: " << c.name
414 << "\n could not parse signature: " << interface_ref.value()
416 << "\n ignoring that the interface is generic"
418 class_type.add_base(base);
423 class_type.add_base(base);
428 for(const auto &lambda_entry : c.lambda_method_handle_map)
433 lambda_entry.second.is_unknown_handle()
434 ? class_type.add_unknown_lambda_method_handle()
435 : class_type.add_lambda_method_handle(
436 lambda_entry.second.get_method_descriptor(),
437 lambda_entry.second.handle_type);
441 if(!c.annotations.empty())
442 convert_annotations(c.annotations, class_type.get_annotations());
445 const irep_idt base_name = [](const std::string &full_name) {
446 const size_t last_dot = full_name.find_last_of('.');
447 return last_dot == std::string::npos
449 : std::string(full_name, last_dot + 1, std::string::npos);
450 }(id2string(c.name));
454 new_symbol.base_name = base_name;
455 new_symbol.pretty_name=c.name;
456 new_symbol.name=qualified_classname;
457 class_type.set_name(new_symbol.name);
458 new_symbol.type=class_type;
459 new_symbol.mode=ID_java;
460 new_symbol.is_type=true;
462 symbolt *class_symbol;
465 log.debug() << "Adding symbol: class '" << c.name << "'" << messaget::eom;
466 if(symbol_table.move(new_symbol, class_symbol))
468 log.error() << "failed to add class symbol " << new_symbol.name
474 const class_typet::componentst &fields =
475 to_class_type(class_symbol->type).components();
478 for(auto overlay_class : overlay_classes)
480 for(const auto &field : overlay_class.get().fields)
482 std::string field_id = qualified_classname + "." + id2string(field.name);
483 if(check_field_exists(field, field_id, fields))
486 "Duplicate field definition for " + field_id + " in overlay class";
488 log.error() << err << messaget::eom;
491 log.debug() << "Adding symbol from overlay class: field '" << field.name
492 << "'" << messaget::eom;
493 convert(*class_symbol, field);
494 POSTCONDITION(check_field_exists(field, field_id, fields));
497 for(const auto &field : c.fields)
499 std::string field_id = qualified_classname + "." + id2string(field.name);
500 if(check_field_exists(field, field_id, fields))
503 log.error() << "Field definition for " << field_id
504 << " already loaded from overlay class" << messaget::eom;
507 log.debug() << "Adding symbol: field '" << field.name << "'"
509 convert(*class_symbol, field);
510 POSTCONDITION(check_field_exists(field, field_id, fields));
514 std::set<irep_idt> overlay_methods;
515 for(auto overlay_class : overlay_classes)
517 for(const methodt &method : overlay_class.get().methods)
519 const irep_idt method_identifier =
520 qualified_classname + "." + id2string(method.name)
521 + ":" + method.descriptor;
522 if(is_ignored_method(c.name, method))
524 log.debug() << "Ignoring method: '" << method_identifier << "'"
528 if(method_bytecode.contains_method(method_identifier))
535 if(overlay_methods.count(method_identifier) == 0)
540 << "Method " << method_identifier
541 << " exists in an overlay class without being marked as an "
542 "overlay and also exists in another overlay class that appears "
543 "earlier in the classpath"
550 log.debug() << "Adding symbol from overlay class: method '"
551 << method_identifier << "'" << messaget::eom;
552 java_bytecode_convert_method_lazy(
557 log.get_message_handler());
558 method_bytecode.add(qualified_classname, method_identifier, method);
559 if(is_overlay_method(method))
560 overlay_methods.insert(method_identifier);
563 for(const methodt &method : c.methods)
565 const irep_idt method_identifier=
566 qualified_classname + "." + id2string(method.name)
567 + ":" + method.descriptor;
568 if(is_ignored_method(c.name, method))
570 log.debug() << "Ignoring method: '" << method_identifier << "'"
574 if(method_bytecode.contains_method(method_identifier))
580 if(overlay_methods.erase(method_identifier) == 0)
585 << "Method " << method_identifier
586 << " exists in an overlay class without being marked as an overlay "
587 "and also exists in the underlying class"
594 log.debug() << "Adding symbol: method '" << method_identifier << "'"
596 java_bytecode_convert_method_lazy(
601 log.get_message_handler());
602 method_bytecode.add(qualified_classname, method_identifier, method);
603 if(is_overlay_method(method))
606 << "Method " << method_identifier
607 << " marked as an overlay where defined in the underlying class"
611 if(!overlay_methods.empty())
614 << "Overlay methods defined in overlay classes did not exist in the "
615 "underlying class:\n";
616 for(const irep_idt &method_id : overlay_methods)
617 log.error() << " " << method_id << "\n";
618 log.error() << messaget::eom;
622 if(c.super_class.empty())
623 java_root_class(*class_symbol);
626 bool java_bytecode_convert_classt::check_field_exists(
627 const java_bytecode_parse_treet::fieldt &field,
628 const irep_idt &qualified_fieldname,
629 const struct_union_typet::componentst &fields) const
632 return symbol_table.has_symbol(qualified_fieldname);
634 auto existing_field = std::find_if(
637 [&field](const struct_union_typet::componentt &f)
639 return f.get_name() == field.name;
641 return existing_field != fields.end();
647 void java_bytecode_convert_classt::convert(
648 symbolt &class_symbol,
652 if(f.signature.has_value())
654 field_type = *java_type_from_string_with_exception(
655 f.descriptor, f.signature, id2string(class_symbol.name));
658 if(is_java_generic_parameter(field_type))
661 std::cout << "fieldtype: generic "
662 << to_java_generic_parameter(field_type).type_variable()
664 << " name " << f.name << "\n";
670 else if(is_java_generic_type(field_type))
672 java_generic_typet &with_gen_type=
673 to_java_generic_type(field_type);
675 std::cout << "fieldtype: generic container type "
676 << std::to_string(with_gen_type.generic_type_arguments().size())
677 << " type " << with_gen_type.id()
678 << " name " << f.name
679 << " subtype id " << with_gen_type.subtype().id() << "\n";
681 field_type=with_gen_type;
685 field_type = *java_type_from_string(f.descriptor);
692 else if(f.is_protected)
693 access = ID_protected;
699 auto &class_type = to_java_class_type(class_symbol.type);
704 const irep_idt field_identifier =
705 id2string(class_symbol.name) + "." + id2string(f.name);
707 class_type.static_members().emplace_back();
708 auto &component = class_type.static_members().back();
710 component.set_name(field_identifier);
711 component.set_base_name(f.name);
712 component.set_pretty_name(f.name);
713 component.set_access(access);
714 component.set_is_final(f.is_final);
715 component.type() = field_type;
720 new_symbol.is_static_lifetime=true;
721 new_symbol.is_lvalue=true;
722 new_symbol.is_state_var=true;
723 new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name);
724 new_symbol.base_name=f.name;
725 new_symbol.type=field_type;
728 set_declaring_class(new_symbol, class_symbol.name);
729 new_symbol.type.set(ID_C_field, f.name);
730 new_symbol.type.set(ID_C_constant, f.is_final);
731 new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
732 "."+id2string(f.name);
733 new_symbol.mode=ID_java;
734 new_symbol.is_type=false;
741 new_symbol.type.set(ID_C_access, ID_public);
742 else if(f.is_protected)
743 new_symbol.type.set(ID_C_access, ID_protected);
744 else if(f.is_private)
745 new_symbol.type.set(ID_C_access, ID_private);
747 new_symbol.type.set(ID_C_access, ID_default);
749 const namespacet ns(symbol_table);
750 const auto value = zero_initializer(field_type, class_symbol.location, ns);
751 if(!value.has_value())
753 log.error().source_location = class_symbol.location;
754 log.error() << "failed to zero-initialize " << f.name << messaget::eom;
757 new_symbol.value = *value;
760 if(!f.annotations.empty())
764 type_checked_cast<annotated_typet>(new_symbol.type).get_annotations());
768 const auto s_it=symbol_table.symbols.find(new_symbol.name);
769 if(s_it!=symbol_table.symbols.end())
770 symbol_table.erase(s_it);
772 if(symbol_table.add(new_symbol))
773 assert(false && "failed to add static field symbol");
777 class_type.components().emplace_back();
778 auto &component = class_type.components().back();
780 component.set_name(f.name);
781 component.set_base_name(f.name);
782 component.set_pretty_name(f.name);
783 component.set_access(access);
784 component.set_is_final(f.is_final);
785 component.type() = field_type;
788 if(!f.annotations.empty())
792 static_cast<annotated_typet &>(component.type()).get_annotations());
797 void add_java_array_types(symbol_tablet &symbol_table)
799 const std::string letters="ijsbcfdza";
801 for(const char l : letters)
803 struct_tag_typet struct_tag_type =
804 to_struct_tag_type(java_array_type(l).subtype());
806 const irep_idt &struct_tag_type_identifier =
807 struct_tag_type.get_identifier();
808 if(symbol_table.has_symbol(struct_tag_type_identifier))
811 java_class_typet class_type;
814 class_type.set_tag(struct_tag_type_identifier);
819 class_type.set_name(struct_tag_type_identifier);
821 class_type.components().reserve(3);
822 java_class_typet::componentt base_class_component(
823 "@java.lang.Object", struct_tag_typet("java::java.lang.Object"));
824 base_class_component.set_pretty_name("@java.lang.Object");
825 base_class_component.set_base_name("@java.lang.Object");
826 class_type.components().push_back(base_class_component);
828 java_class_typet::componentt length_component("length", java_int_type());
829 length_component.set_pretty_name("length");
830 length_component.set_base_name("length");
831 class_type.components().push_back(length_component);
833 java_class_typet::componentt data_component(
834 "data", java_reference_type(java_type_from_char(l)));
835 data_component.set_pretty_name("data");
836 data_component.set_base_name("data");
837 class_type.components().push_back(data_component);
843 java_class_typet::componentt array_element_classid_component(
844 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME, string_typet());
845 array_element_classid_component.set_pretty_name(
846 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
847 array_element_classid_component.set_base_name(
848 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
849 class_type.components().push_back(array_element_classid_component);
851 java_class_typet::componentt array_dimension_component(
852 JAVA_ARRAY_DIMENSION_FIELD_NAME, java_int_type());
853 array_dimension_component.set_pretty_name(
854 JAVA_ARRAY_DIMENSION_FIELD_NAME);
855 array_dimension_component.set_base_name(JAVA_ARRAY_DIMENSION_FIELD_NAME);
856 class_type.components().push_back(array_dimension_component);
859 class_type.add_base(struct_tag_typet("java::java.lang.Object"));
862 is_valid_java_array(class_type),
863 "Constructed a new type representing a Java Array "
864 "object that doesn't match expectations");
867 symbol.name = struct_tag_type_identifier;
868 symbol.base_name = struct_tag_type.get(ID_C_base_name);
870 symbol.type = class_type;
871 symbol.mode = ID_java;
872 symbol_table.add(symbol);
877 const irep_idt clone_name =
878 id2string(struct_tag_type_identifier) + ".clone:()Ljava/lang/Object;";
879 java_method_typet::parametert this_param(
880 java_reference_type(struct_tag_type));
881 this_param.set_identifier(id2string(clone_name)+"::this");
882 this_param.set_base_name(ID_this);
883 this_param.set_this();
884 const java_method_typet clone_type({this_param}, java_lang_object_type());
886 parameter_symbolt this_symbol;
887 this_symbol.name=this_param.get_identifier();
888 this_symbol.base_name=this_param.get_base_name();
889 this_symbol.pretty_name=this_symbol.base_name;
890 this_symbol.type=this_param.type();
891 this_symbol.mode=ID_java;
892 symbol_table.add(this_symbol);
894 const irep_idt local_name=
895 id2string(clone_name)+"::cloned_array";
896 auxiliary_symbolt local_symbol;
897 local_symbol.name=local_name;
898 local_symbol.base_name="cloned_array";
899 local_symbol.pretty_name=local_symbol.base_name;
900 local_symbol.type = java_reference_type(struct_tag_type);
901 local_symbol.mode=ID_java;
902 symbol_table.add(local_symbol);
903 const auto local_symexpr = local_symbol.symbol_expr();
905 code_declt declare_cloned(local_symexpr);
907 source_locationt location;
908 location.set_function(local_name);
909 side_effect_exprt java_new_array(
910 ID_java_new_array, java_reference_type(struct_tag_type), location);
911 dereference_exprt old_array{this_symbol.symbol_expr()};
912 dereference_exprt new_array{local_symexpr};
913 member_exprt old_length(
914 old_array, length_component.get_name(), length_component.type());
915 java_new_array.copy_to_operands(old_length);
916 code_assignt create_blank(local_symexpr, java_new_array);
918 codet copy_type_information = code_skipt();
923 const auto &array_dimension_component =
924 class_type.get_component(JAVA_ARRAY_DIMENSION_FIELD_NAME);
925 const auto &array_element_classid_component =
926 class_type.get_component(JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
928 member_exprt old_array_dimension(old_array, array_dimension_component);
929 member_exprt old_array_element_classid(
930 old_array, array_element_classid_component);
932 member_exprt new_array_dimension(new_array, array_dimension_component);
933 member_exprt new_array_element_classid(
934 new_array, array_element_classid_component);
936 copy_type_information = code_blockt{
937 {code_assignt(new_array_dimension, old_array_dimension),
938 code_assignt(new_array_element_classid, old_array_element_classid)}};
941 member_exprt old_data(
942 old_array, data_component.get_name(), data_component.type());
943 member_exprt new_data(
944 new_array, data_component.get_name(), data_component.type());
956 const irep_idt index_name=
957 id2string(clone_name)+"::index";
958 auxiliary_symbolt index_symbol;
959 index_symbol.name=index_name;
960 index_symbol.base_name="index";
961 index_symbol.pretty_name=index_symbol.base_name;
962 index_symbol.type = length_component.type();
963 index_symbol.mode=ID_java;
964 symbol_table.add(index_symbol);
965 const auto &index_symexpr=index_symbol.symbol_expr();
967 code_declt declare_index(index_symexpr);
969 dereference_exprt old_cell(
970 plus_exprt(old_data, index_symexpr), old_data.type().subtype());
971 dereference_exprt new_cell(
972 plus_exprt(new_data, index_symexpr), new_data.type().subtype());
974 const code_fort copy_loop = code_fort::from_index_bounds(
975 from_integer(0, index_symexpr.type()),
978 code_assignt(std::move(new_cell), std::move(old_cell)),
981 member_exprt new_base_class(
982 new_array, base_class_component.get_name(), base_class_component.type());
983 address_of_exprt retval(new_base_class);
984 code_returnt return_inst(retval);
986 const code_blockt clone_body({declare_cloned,
988 copy_type_information,
993 symbolt clone_symbol;
994 clone_symbol.name=clone_name;
995 clone_symbol.pretty_name =
996 id2string(struct_tag_type_identifier) + ".clone:()";
997 clone_symbol.base_name="clone";
998 clone_symbol.type=clone_type;
999 clone_symbol.value=clone_body;
1000 clone_symbol.mode=ID_java;
1001 symbol_table.add(clone_symbol);
1005 bool java_bytecode_convert_class(
1006 const java_class_loadert::parse_tree_with_overlayst &parse_trees,
1007 symbol_tablet &symbol_table,
1008 message_handlert &message_handler,
1009 size_t max_array_length,
1010 method_bytecodet &method_bytecode,
1011 java_string_library_preprocesst &string_preprocess,
1012 const std::unordered_set<std::string> &no_load_classes)
1014 java_bytecode_convert_classt java_bytecode_convert_class(
1024 java_bytecode_convert_class(parse_trees);
1032 catch(const char *e)
1034 messaget log{message_handler};
1035 log.error() << e << messaget::eom;
1038 catch(const std::string &e)
1040 messaget log{message_handler};
1041 log.error() << e << messaget::eom;
1047 static std::string get_final_name_component(const std::string &name)
1049 return name.substr(name.rfind("::") + 2);
1052 static std::string get_without_final_name_component(const std::string &name)
1054 return name.substr(0, name.rfind("::"));
1069 static void find_and_replace_parameter(
1070 java_generic_parametert ¶meter,
1071 const std::vector<java_generic_parametert> &replacement_parameters)
1074 const std::string ¶meter_full_name =
1075 id2string(parameter.type_variable_ref().get_identifier());
1076 const std::string parameter_name =
1077 get_final_name_component(parameter_full_name);
1080 const auto replacement_parameter_it = std::find_if(
1081 replacement_parameters.begin(),
1082 replacement_parameters.end(),
1083 [¶meter_name](const java_generic_parametert &replacement_param) {
1084 return parameter_name ==
1085 get_final_name_component(
1086 id2string(replacement_param.type_variable().get_identifier()));
1088 if(replacement_parameter_it == replacement_parameters.end())
1092 const std::string &replacement_parameter_full_name =
1093 id2string(replacement_parameter_it->type_variable().get_identifier());
1096 PRECONDITION(has_prefix(
1097 replacement_parameter_full_name,
1098 get_without_final_name_component(parameter_full_name)));
1100 parameter.type_variable_ref().set_identifier(replacement_parameter_full_name);
1108 static void find_and_replace_parameters(
1110 const std::vector<java_generic_parametert> &replacement_parameters)
1112 if(is_java_generic_parameter(type))
1114 find_and_replace_parameter(
1115 to_java_generic_parameter(type), replacement_parameters);
1117 else if(is_java_generic_type(type))
1119 java_generic_typet &generic_type = to_java_generic_type(type);
1120 std::vector<reference_typet> &arguments =
1121 generic_type.generic_type_arguments();
1122 for(auto &argument : arguments)
1124 find_and_replace_parameters(argument, replacement_parameters);
1127 else if(is_java_generic_struct_tag_type(type))
1129 java_generic_struct_tag_typet &generic_base =
1130 to_java_generic_struct_tag_type(type);
1131 std::vector<reference_typet> &gen_types = generic_base.generic_types();
1132 for(auto &gen_type : gen_types)
1134 find_and_replace_parameters(gen_type, replacement_parameters);
1142 void convert_annotations(
1143 const java_bytecode_parse_treet::annotationst &parsed_annotations,
1144 std::vector<java_annotationt> &java_annotations)
1146 for(const auto &annotation : parsed_annotations)
1148 java_annotations.emplace_back(annotation.type);
1149 std::vector<java_annotationt::valuet> &values =
1150 java_annotations.back().get_values();
1152 annotation.element_value_pairs.begin(),
1153 annotation.element_value_pairs.end(),
1154 std::back_inserter(values),
1155 [](const decltype(annotation.element_value_pairs)::value_type &value) {
1156 return java_annotationt::valuet(value.element_name, value.value);
1165 void convert_java_annotations(
1166 const std::vector<java_annotationt> &java_annotations,
1167 java_bytecode_parse_treet::annotationst &annotations)
1169 for(const auto &java_annotation : java_annotations)
1171 annotations.emplace_back(java_bytecode_parse_treet::annotationt());
1172 auto &annotation = annotations.back();
1173 annotation.type = java_annotation.get_type();
1176 java_annotation.get_values().begin(),
1177 java_annotation.get_values().end(),
1178 std::back_inserter(annotation.element_value_pairs),
1179 [](const java_annotationt::valuet &value)
1180 -> java_bytecode_parse_treet::annotationt::element_value_pairt {
1181 return {value.get_name(), value.get_value()};
1190 void mark_java_implicitly_generic_class_type(
1191 const irep_idt &class_name,
1192 symbol_tablet &symbol_table)
1194 const std::string qualified_class_name = "java::" + id2string(class_name);
1195 PRECONDITION(symbol_table.has_symbol(qualified_class_name));
1197 symbolt &class_symbol = symbol_table.get_writeable_ref(qualified_class_name);
1198 const java_class_typet &class_type = to_java_class_type(class_symbol.type);
1203 bool no_this_field = std::none_of(
1204 class_type.components().begin(),
1205 class_type.components().end(),
1206 [](const struct_union_typet::componentt &component)
1208 return id2string(component.get_name()).substr(0, 5) == "this$";
1217 std::vector<java_generic_parametert> implicit_generic_type_parameters;
1218 std::string::size_type outer_class_delimiter =
1219 qualified_class_name.rfind('$');
1220 while(outer_class_delimiter != std::string::npos)
1222 std::string outer_class_name =
1223 qualified_class_name.substr(0, outer_class_delimiter);
1224 if(symbol_table.has_symbol(outer_class_name))
1226 const symbolt &outer_class_symbol =
1227 symbol_table.lookup_ref(outer_class_name);
1228 const java_class_typet &outer_class_type =
1229 to_java_class_type(outer_class_symbol.type);
1230 if(is_java_generic_class_type(outer_class_type))
1232 for(const java_generic_parametert &outer_generic_type_parameter :
1233 to_java_generic_class_type(outer_class_type).generic_types())
1237 irep_idt identifier = qualified_class_name + "::" +
1238 id2string(strip_java_namespace_prefix(
1239 outer_generic_type_parameter.get_name()));
1240 java_generic_parameter_tagt bound = to_java_generic_parameter_tag(
1241 outer_generic_type_parameter.subtype());
1242 bound.type_variable_ref().set_identifier(identifier);
1243 implicit_generic_type_parameters.emplace_back(identifier, bound);
1246 outer_class_delimiter = outer_class_name.rfind('$');
1250 throw missing_outer_class_symbol_exceptiont(
1251 outer_class_name, qualified_class_name);
1257 if(!implicit_generic_type_parameters.empty())
1259 java_implicitly_generic_class_typet new_class_type(
1260 class_type, implicit_generic_type_parameters);
1263 if(is_java_generic_class_type(class_type))
1265 const java_generic_class_typet::generic_typest &class_type_params =
1266 to_java_generic_class_type(class_type).generic_types();
1267 implicit_generic_type_parameters.insert(
1268 implicit_generic_type_parameters.begin(),
1269 class_type_params.begin(),
1270 class_type_params.end());
1273 for(auto &field : new_class_type.components())
1275 find_and_replace_parameters(
1276 field.type(), implicit_generic_type_parameters);
1279 for(auto &base : new_class_type.bases())
1281 find_and_replace_parameters(
1282 base.type(), implicit_generic_type_parameters);
1285 class_symbol.type = new_class_type;