@@ -517,3 +517,163 @@ bool java_bytecode_convert_class(
517
517
518
518
return true ;
519
519
}
520
+
521
+ // / For a given generic type parameter, check if there is a parameter in the
522
+ // / given vector of replacement parameters with a matching name. If yes,
523
+ // / replace the identifier of the parameter at hand by the identifier of
524
+ // / the matching parameter.
525
+ // / Example: if \p parameter has identifier `java::Outer$Inner::T` and
526
+ // / there is a replacement parameter with identifier `java::Outer::T`, the
527
+ // / identifier of \p parameter gets set to `java::Outer::T`.
528
+ // / \param parameter
529
+ // / \param replacement_parameters vector of generic parameters (only viable
530
+ // / ones, i.e., only those that can actually appear here such as generic
531
+ // / parameters of outer classes of the class specified by the prefix of \p
532
+ // / parameter identifier)
533
+ static void find_and_replace_parameter (
534
+ java_generic_parametert ¶meter,
535
+ const std::vector<java_generic_parametert> &replacement_parameters)
536
+ {
537
+ // get the name of the parameter, e.g., `T` from `java::Class::T`
538
+ const std::string ¶meter_full_name =
539
+ as_string (parameter.type_variable_ref ().get_identifier ());
540
+ const std::string ¶meter_name =
541
+ parameter_full_name.substr (parameter_full_name.rfind (" ::" ) + 2 );
542
+
543
+ // check if there is a replacement parameter with the same name
544
+ const auto replacement_parameter_p = std::find_if (
545
+ replacement_parameters.begin (),
546
+ replacement_parameters.end (),
547
+ [¶meter_name](const java_generic_parametert &replacement_param)
548
+ {
549
+ const std::string &replacement_parameter_full_name =
550
+ as_string (replacement_param.type_variable ().get_identifier ());
551
+ return parameter_name.compare (
552
+ replacement_parameter_full_name.substr (
553
+ replacement_parameter_full_name.rfind (" ::" ) + 2 )) == 0 ;
554
+ });
555
+
556
+ // if a replacement parameter was found, update the identifier
557
+ if (replacement_parameter_p != replacement_parameters.end ())
558
+ {
559
+ const std::string &replacement_parameter_full_name =
560
+ as_string (replacement_parameter_p->type_variable ().get_identifier ());
561
+
562
+ // the replacement parameter is a viable one, i.e., it comes from an outer
563
+ // class
564
+ PRECONDITION (
565
+ parameter_full_name.substr (0 , parameter_full_name.rfind (" ::" ))
566
+ .compare (
567
+ replacement_parameter_full_name.substr (
568
+ 0 , replacement_parameter_full_name.rfind (" ::" ))) > 0 );
569
+
570
+ parameter.type_variable_ref ().set_identifier (
571
+ replacement_parameter_full_name);
572
+ }
573
+ }
574
+
575
+ // / Recursively find all generic type parameters of a given type and replace
576
+ // / their identifiers if matching replacement parameter exist.
577
+ // / Example: class `Outer<T>` has an inner class `Inner` that has a field
578
+ // / `t` of type `Generic<T>`. This function ensures that the parameter points to
579
+ // / `java::Outer::T` instead of `java::Outer$Inner::T`.
580
+ // / \param type
581
+ // / \param replacement_parameters
582
+ static void find_and_replace_parameters (
583
+ typet &type,
584
+ const std::vector<java_generic_parametert> &replacement_parameters)
585
+ {
586
+ if (is_java_generic_parameter (type))
587
+ {
588
+ find_and_replace_parameter (
589
+ to_java_generic_parameter (type), replacement_parameters);
590
+ }
591
+ else if (is_java_generic_type (type))
592
+ {
593
+ java_generic_typet &generic_type = to_java_generic_type (type);
594
+ std::vector<reference_typet> &arguments =
595
+ generic_type.generic_type_arguments ();
596
+ for (auto &argument : arguments)
597
+ {
598
+ find_and_replace_parameters (argument, replacement_parameters);
599
+ }
600
+ }
601
+ }
602
+
603
+ // / Checks if the class is implicitly generic, i.e., it is an inner class of
604
+ // / any generic class. All uses of the implicit generic type parameters within
605
+ // / the inner class are updated to point to the type parameters of the
606
+ // / corresponding outer classes.
607
+ // / \param class_name
608
+ // / \param symbol_table
609
+ void mark_java_implicitly_generic_class_type (
610
+ const irep_idt &class_name,
611
+ symbol_tablet &symbol_table)
612
+ {
613
+ const std::string qualified_class_name = " java::" + id2string (class_name);
614
+ PRECONDITION (symbol_table.has_symbol (qualified_class_name));
615
+ symbolt &class_symbol = symbol_table.get_writeable_ref (qualified_class_name);
616
+ java_class_typet &class_type = to_java_class_type (class_symbol.type );
617
+
618
+ // the class must be an inner non-static class, i.e., have a field this$*
619
+ // TODO this should be simplified once static inner classes are marked
620
+ // during parsing
621
+ bool no_this_field = std::none_of (
622
+ class_type.components ().begin (),
623
+ class_type.components ().end (),
624
+ [](const struct_union_typet::componentt &component)
625
+ {
626
+ return id2string (component.get_name ()).substr (0 , 5 ) == " this$" ;
627
+ });
628
+ if (no_this_field)
629
+ {
630
+ return ;
631
+ }
632
+
633
+ // create a vector of all generic type parameters of all outer classes, in
634
+ // the order from the outer-most inwards
635
+ std::vector<java_generic_parametert> implicit_generic_type_parameters;
636
+ std::string::size_type outer_class_delimiter =
637
+ qualified_class_name.rfind (" $" );
638
+ while (outer_class_delimiter != std::string::npos)
639
+ {
640
+ std::string outer_class_name =
641
+ qualified_class_name.substr (0 , outer_class_delimiter);
642
+ if (symbol_table.has_symbol (outer_class_name))
643
+ {
644
+ const symbolt &outer_class_symbol =
645
+ symbol_table.lookup_ref (outer_class_name);
646
+ const java_class_typet &outer_class_type =
647
+ to_java_class_type (outer_class_symbol.type );
648
+ if (is_java_generic_class_type (outer_class_type))
649
+ {
650
+ const auto &outer_generic_type_parameters =
651
+ to_java_generic_class_type (outer_class_type).generic_types ();
652
+ implicit_generic_type_parameters.insert (
653
+ implicit_generic_type_parameters.begin (),
654
+ outer_generic_type_parameters.begin (),
655
+ outer_generic_type_parameters.end ());
656
+ }
657
+ outer_class_delimiter = outer_class_name.rfind (" $" );
658
+ }
659
+ else
660
+ {
661
+ throw missing_outer_class_symbol_exceptiont (
662
+ outer_class_name, qualified_class_name);
663
+ }
664
+ }
665
+
666
+ // if there are any implicit generic type parameters, mark the class
667
+ // implicitly generic and update identifiers of type parameters used in fields
668
+ if (!implicit_generic_type_parameters.empty ())
669
+ {
670
+ class_symbol.type = java_implicitly_generic_class_typet (
671
+ class_type, implicit_generic_type_parameters);
672
+
673
+ for (auto &field : class_type.components ())
674
+ {
675
+ find_and_replace_parameters (
676
+ field.type (), implicit_generic_type_parameters);
677
+ }
678
+ }
679
+ }
0 commit comments