Skip to content

Commit 6724054

Browse files
committed
Move generic information from decorated pointers to decorated tags
This means that a pointer is once again just a pointer, and can be removed and reapplied without risking losing information. On the other hand tags now carry decorations more often (they already played this role when expressing a superclass, which is implemented as a nested struct), so `ns.follow` returns a type missing its decorations -- however this is hopefully a small risk, as code using the decorated-pointer implementation would already need to know that following the pointer, never mind the tag at the end of it, could lose information.
1 parent 88ab7d5 commit 6724054

File tree

2 files changed

+134
-68
lines changed

2 files changed

+134
-68
lines changed

jbmc/src/java_bytecode/java_types.h

Lines changed: 133 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -407,21 +407,21 @@ bool equal_java_types(const typet &type1, const typet &type2);
407407
/// Class to hold a Java generic type parameter (also called type variable),
408408
/// e.g., `T` in `List<T>`.
409409
/// The bound can specify type requirements.
410-
class java_generic_parametert:public reference_typet
410+
class java_generic_parameter_tagt : public struct_tag_typet
411411
{
412412
public:
413413
typedef struct_tag_typet type_variablet;
414414

415-
java_generic_parametert(
415+
java_generic_parameter_tagt(
416416
const irep_idt &_type_var_name,
417417
const struct_tag_typet &_bound)
418-
: reference_typet(java_reference_type(_bound))
418+
: struct_tag_typet(_bound)
419419
{
420420
set(ID_C_java_generic_parameter, true);
421421
type_variables().push_back(struct_tag_typet(_type_var_name));
422422
}
423423

424-
/// \return the type variable as symbol type
424+
/// \return the type variable as struct tag type
425425
const type_variablet &type_variable() const
426426
{
427427
PRECONDITION(!type_variables().empty());
@@ -431,7 +431,7 @@ class java_generic_parametert:public reference_typet
431431
type_variablet &type_variable_ref()
432432
{
433433
PRECONDITION(!type_variables().empty());
434-
return const_cast<type_variablet &>(type_variables().front());
434+
return type_variables().front();
435435
}
436436

437437
const irep_idt get_name() const
@@ -452,13 +452,73 @@ class java_generic_parametert:public reference_typet
452452
}
453453
};
454454

455+
/// Checks whether the type is a java generic parameter/variable, e.g., `T` in
456+
/// `List<T>`.
457+
/// \param type: the type to check
458+
/// \return true if type is a generic Java parameter tag type
459+
inline bool is_java_generic_parameter_tag(const typet &type)
460+
{
461+
return type.get_bool(ID_C_java_generic_parameter);
462+
}
463+
464+
/// \param type: source type
465+
/// \return cast of type into a java_generic_parametert
466+
inline const java_generic_parameter_tagt &to_java_generic_parameter_tag(
467+
const typet &type)
468+
{
469+
PRECONDITION(is_java_generic_parameter_tag(type));
470+
return static_cast<const java_generic_parameter_tagt &>(type);
471+
}
472+
473+
/// \param type: source type
474+
/// \return cast of type into a java_generic_parameter_tag
475+
inline java_generic_parameter_tagt &to_java_generic_parameter_tag(typet &type)
476+
{
477+
PRECONDITION(is_java_generic_parameter_tag(type));
478+
return static_cast<java_generic_parameter_tagt &>(type);
479+
}
480+
481+
/// Reference that points to a java_generic_parameter_tagt. All information is
482+
/// stored on the underlying tag.
483+
class java_generic_parametert:public reference_typet
484+
{
485+
public:
486+
typedef struct_tag_typet type_variablet;
487+
488+
java_generic_parametert(
489+
const irep_idt &_type_var_name,
490+
const struct_tag_typet &_bound)
491+
: reference_typet(
492+
java_reference_type(
493+
java_generic_parameter_tagt(_type_var_name, _bound)))
494+
{
495+
}
496+
497+
/// \return the type variable as symbol type
498+
const type_variablet &type_variable() const
499+
{
500+
return to_java_generic_parameter_tag(subtype()).type_variable();
501+
}
502+
503+
type_variablet &type_variable_ref()
504+
{
505+
return to_java_generic_parameter_tag(subtype()).type_variable_ref();
506+
}
507+
508+
const irep_idt get_name() const
509+
{
510+
return to_java_generic_parameter_tag(subtype()).get_name();
511+
}
512+
};
513+
455514
/// Checks whether the type is a java generic parameter/variable, e.g., `T` in
456515
/// `List<T>`.
457516
/// \param type: the type to check
458517
/// \return true if type is a generic Java parameter type
459518
inline bool is_java_generic_parameter(const typet &type)
460519
{
461-
return type.get_bool(ID_C_java_generic_parameter);
520+
return type.id() == ID_pointer &&
521+
is_java_generic_parameter_tag(type.subtype());
462522
}
463523

464524
/// \param type: source type
@@ -493,36 +553,94 @@ inline java_generic_parametert &to_java_generic_parameter(typet &type)
493553
/// - in `HashMap<List<T>, V>` it would contain two elements, the first of
494554
/// type `java_generic_typet` and the second of type
495555
/// `java_generic_parametert`.
556+
class java_generic_struct_tag_typet : public struct_tag_typet
557+
{
558+
public:
559+
typedef std::vector<reference_typet> generic_typest;
560+
561+
explicit java_generic_struct_tag_typet(
562+
const struct_tag_typet &type) :
563+
struct_tag_typet(type)
564+
{
565+
set(ID_C_java_generic_symbol, true);
566+
}
567+
568+
java_generic_struct_tag_typet(
569+
const struct_tag_typet &type,
570+
const std::string &base_ref,
571+
const std::string &class_name_prefix);
572+
573+
const generic_typest &generic_types() const
574+
{
575+
return (const generic_typest &)(find(ID_generic_types).get_sub());
576+
}
577+
578+
generic_typest &generic_types()
579+
{
580+
return (generic_typest &)(add(ID_generic_types).get_sub());
581+
}
582+
583+
optionalt<size_t>
584+
generic_type_index(const java_generic_parametert &type) const;
585+
};
586+
587+
/// \param type: the type to check
588+
/// \return true if the type is a symbol type with generics
589+
inline bool is_java_generic_struct_tag_type(const typet &type)
590+
{
591+
return type.get_bool(ID_C_java_generic_symbol);
592+
}
593+
594+
/// \param type: the type to convert
595+
/// \return the converted type
596+
inline const java_generic_struct_tag_typet &
597+
to_java_generic_struct_tag_type(const typet &type)
598+
{
599+
PRECONDITION(is_java_generic_struct_tag_type(type));
600+
return static_cast<const java_generic_struct_tag_typet &>(type);
601+
}
602+
603+
/// \param type: the type to convert
604+
/// \return the converted type
605+
inline java_generic_struct_tag_typet &
606+
to_java_generic_struct_tag_type(typet &type)
607+
{
608+
PRECONDITION(is_java_generic_struct_tag_type(type));
609+
return static_cast<java_generic_struct_tag_typet &>(type);
610+
}
611+
612+
/// Reference that points to a java_generic_struct_tag_typet. All information is
613+
/// stored on the underlying tag.
496614
class java_generic_typet:public reference_typet
497615
{
498616
public:
499-
typedef std::vector<reference_typet> generic_type_argumentst;
617+
typedef java_generic_struct_tag_typet::generic_typest generic_type_argumentst;
500618

501-
explicit java_generic_typet(const typet &_type):
502-
reference_typet(java_reference_type(_type))
619+
explicit java_generic_typet(const typet &_type) :
620+
reference_typet(
621+
java_reference_type(
622+
java_generic_struct_tag_typet(to_struct_tag_type(_type))))
503623
{
504-
set(ID_C_java_generic_type, true);
505624
}
506625

507626
/// \return vector of type variables
508627
const generic_type_argumentst &generic_type_arguments() const
509628
{
510-
return (const generic_type_argumentst &)(
511-
find(ID_type_variables).get_sub());
629+
return to_java_generic_struct_tag_type(subtype()).generic_types();
512630
}
513631

514632
/// \return vector of type variables
515633
generic_type_argumentst &generic_type_arguments()
516634
{
517-
return (generic_type_argumentst &)(
518-
add(ID_type_variables).get_sub());
635+
return to_java_generic_struct_tag_type(subtype()).generic_types();
519636
}
520637
};
521638

522639
template <>
523640
inline bool can_cast_type<java_generic_typet>(const typet &type)
524641
{
525-
return is_reference(type) && type.get_bool(ID_C_java_generic_type);
642+
return
643+
is_reference(type) && type.subtype().get_bool(ID_C_java_generic_symbol);
526644
}
527645

528646
/// \param type: the type to check
@@ -761,58 +879,6 @@ void get_dependencies_from_generic_parameters(
761879
const typet &,
762880
std::set<irep_idt> &);
763881

764-
/// Type for a generic symbol, extends struct_tag_typet with a
765-
/// vector of java generic types.
766-
/// This is used to store the type of generic superclasses and interfaces.
767-
class java_generic_struct_tag_typet : public struct_tag_typet
768-
{
769-
public:
770-
typedef std::vector<reference_typet> generic_typest;
771-
772-
java_generic_struct_tag_typet(
773-
const struct_tag_typet &type,
774-
const std::string &base_ref,
775-
const std::string &class_name_prefix);
776-
777-
const generic_typest &generic_types() const
778-
{
779-
return (const generic_typest &)(find(ID_generic_types).get_sub());
780-
}
781-
782-
generic_typest &generic_types()
783-
{
784-
return (generic_typest &)(add(ID_generic_types).get_sub());
785-
}
786-
787-
optionalt<size_t>
788-
generic_type_index(const java_generic_parametert &type) const;
789-
};
790-
791-
/// \param type: the type to check
792-
/// \return true if the type is a symbol type with generics
793-
inline bool is_java_generic_struct_tag_type(const typet &type)
794-
{
795-
return type.get_bool(ID_C_java_generic_symbol);
796-
}
797-
798-
/// \param type: the type to convert
799-
/// \return the converted type
800-
inline const java_generic_struct_tag_typet &
801-
to_java_generic_struct_tag_type(const typet &type)
802-
{
803-
PRECONDITION(is_java_generic_struct_tag_type(type));
804-
return static_cast<const java_generic_struct_tag_typet &>(type);
805-
}
806-
807-
/// \param type: the type to convert
808-
/// \return the converted type
809-
inline java_generic_struct_tag_typet &
810-
to_java_generic_struct_tag_type(typet &type)
811-
{
812-
PRECONDITION(is_java_generic_struct_tag_type(type));
813-
return static_cast<java_generic_struct_tag_typet &>(type);
814-
}
815-
816882
/// Take a signature string and remove everything in angle brackets allowing for
817883
/// the type to be parsed normally, for example
818884
/// `java.util.HashSet<java.lang.Integer>` will be turned into

src/util/irep_ids.def

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -652,7 +652,7 @@ IREP_ID_TWO(C_java_generic_type, #java_generic_type)
652652
IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type)
653653
IREP_ID_TWO(C_java_implicitly_generic_class_type, #java_implicitly_generic_class_type)
654654
IREP_ID_TWO(C_java_generic_symbol, #java_generic_symbol)
655-
IREP_ID_TWO(generic_types, #generic_types)
655+
IREP_ID_TWO(generic_types, generic_types)
656656
IREP_ID_TWO(implicit_generic_types, #implicit_generic_types)
657657
IREP_ID_ONE(type_variables)
658658
IREP_ID_TWO(java_lambda_method_handle_index, lambda_method_handle_index)

0 commit comments

Comments
 (0)