Merge pull request #3382 from svorenova/doc-select-pointer-type

Document pointer type selection interface [DOC-113]

jbmc/src/java_bytecode/README.md

@@ -20,7 +20,7 @@ into a basic `codet` representation.
 - \ref java-bytecode-runtime-exceptions "Add runtime exceptions"
 - \ref java-bytecode-remove-java-new "Remove `new` calls"
 - \ref java-bytecode-remove-exceptions "Remove thrown exceptions"
-- \ref java-bytecode-remove-instance-of
+- \ref java-bytecode-remove-instanceof
 - As well as other non-Java specific transformations (see \ref goto-programs for
     details on these)
 
@@ -39,9 +39,21 @@ To be documented.
 
 \subsection java-bytecode-pointer-type-selection Pointer type selection
 
-To be documented.
+In Java, all variables that are of a non-primitive type are pointers to
+an object. When initializing such variables using \ref java_object_factoryt,
+e.g., as input arguments for the method under test, we may need to select the
+correct pointer type. For example, abstract classes can be replaced with their
+concrete implementations and type parameters in generic types can be replaced
+with their specialized types.
 
-\subsection java-bytecode-genereic-substitution Generic substitution
+The class \ref select_pointer_typet offers the basic interface for this
+functionality, in particular see
+\ref select_pointer_typet::convert_pointer_type. Note that this class only
+implements generic specialization (see \ref
+java-bytecode-generic-specialization), derived classes can override this
+behavior to provide more sophisticated type selection.
+
+\subsection java-bytecode-generic-specialization Generic specialization
 
 To be documented.
 
@@ -84,8 +96,11 @@ The JVM specification defines different access flags, e.g., `final`, `static`,
 itself, its fields or methods. All access flags are represented as bits, the set
 of bits that are defined for one entity is represented as disjunction of those
 values. Each of these values is defined as a constant with a name prefixed with
-`ACC_` in JBMC, e.g., as `#define ACC_PUBLIC 0x0001` or `#define ACC_ENUM
-0x4000`.
+`ACC_` in JBMC, e.g., as
+@code
+#define ACC_PUBLIC 0x0001
+#define ACC_ENUM 0x4000
+@endcode
 
 \subsection java-class-constant-pool Constant Pool
 

jbmc/src/java_bytecode/select_pointer_type.cpp

@@ -14,15 +14,6 @@
 #include "java_types.h"
 #include <util/std_types.h>
 
-/// Select what type should be used for a given pointer type. For the base class
-/// we just use the supplied type. Derived classes can override this behaviour
-/// to provide more sophisticated type selection. Generic parameters are
-/// replaced with their concrete type.
-/// \param pointer_type: The pointer type replace
-/// \param generic_parameter_specialization_map map of types for all generic
-/// parameters in the current scope
-/// \param ns Namespace for type lookups
-/// \return A pointer type where the subtype may have been modified
 pointer_typet select_pointer_typet::convert_pointer_type(
   const pointer_typet &pointer_type,
   const generic_parameter_specialization_mapt
@@ -46,24 +37,6 @@ pointer_typet select_pointer_typet::convert_pointer_type(
   }
 }
 
-/// Specialize generic parameters in a pointer type based on the current map
-/// of parameters -> types. We specialize generics if the pointer is a java
-/// generic parameter or an array with generic parameters (java generic types
-/// are specialized recursively, their concrete types are already stored in
-/// the map and will be retrieved when needed e.g., to initialize fields).
-/// Example:
-/// - generic type: T
-/// - map: T -> U; U -> String
-/// - result: String
-///
-/// - generic type: T[]
-/// - map: T -> U; U -> String
-/// - result: String
-/// \param pointer_type pointer to be specialized
-/// \param generic_parameter_specialization_map map of types for all generic
-/// parameters in the current scope
-/// \return pointer type where generic parameters are replaced with concrete
-/// types, if set in the current scope
 pointer_typet select_pointer_typet::specialize_generics(
   const pointer_typet &pointer_type,
   const generic_parameter_specialization_mapt

jbmc/src/java_bytecode/select_pointer_type.h

@@ -36,22 +36,58 @@ class select_pointer_typet
 
 public:
   virtual ~select_pointer_typet() = default;
+
+  /// Select what type should be used for a given pointer type. In the base
+  /// class we just use the supplied type. Derived classes can override this
+  /// behavior to provide more sophisticated type selection. Generic
+  /// parameters are replaced with their specialized type.
+  /// \param pointer_type: The pointer type to convert
+  /// \param generic_parameter_specialization_map: Map of types for all generic
+  ///   parameters in the current scope
+  /// \param ns: Namespace for type lookups
+  /// \return A pointer type where the subtype may have been modified
   virtual pointer_typet convert_pointer_type(
     const pointer_typet &pointer_type,
     const generic_parameter_specialization_mapt
       &generic_parameter_specialization_map,
     const namespacet &ns) const;
 
+  /// Get alternative types for a method parameter, e.g., based on the casts in
+  /// the function body. In the base class we just return an empty set.
+  /// Derived classes can override this behaviour to provide more
+  /// sophisticated alternative type identification.
   virtual std::set<symbol_typet> get_parameter_alternative_types(
     const irep_idt &function_name,
     const irep_idt &parameter_name,
     const namespacet &ns) const;
 
+  /// Specialize generic parameters in a pointer type based on the current map
+  /// of parameters -> types. We specialize generics only if the pointer is a
+  /// java generic parameter or an array with generic parameters. More
+  /// general generic types such as `MyGeneric<T>` are specialized
+  /// indirectly in \ref java_object_factoryt, their concrete types are already
+  /// stored in the map and will be retrieved when needed e.g., to initialize
+  /// fields.
+  /// Example:
+  /// - generic type: T
+  /// - map: T -> U; U -> String
+  /// - result: String
+  ///
+  /// - generic type: T[]
+  /// - map: T -> U; U -> String
+  /// - result: String[]
+  /// \param pointer_type: The pointer to be specialized
+  /// \param generic_parameter_specialization_map: Map of types for all
+  ///   generic parameters in the current scope
+  /// \param visited_nodes: Set of parameter names already considered in
+  ///   recursion, used to avoid infinite recursion
+  /// \return Pointer type where generic parameters are replaced with
+  ///   specialized types (if set in the current scope)
   pointer_typet specialize_generics(
     const pointer_typet &pointer_type,
     const generic_parameter_specialization_mapt
       &generic_parameter_specialization_map,
-    generic_parameter_recursion_trackingt &visited) const;
+    generic_parameter_recursion_trackingt &visited_nodes) const;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H

scripts/expected_doxygen_warnings.txt

@@ -91,14 +91,9 @@
 /cbmc/src/langapi/language.h:176: warning: The following parameters of languaget::build_stub_parameter_symbol(const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert &parameter) are not documented:
   parameter 'parameter'
 /cbmc/jbmc/src/java_bytecode/remove_exceptions.cpp:47: warning: Found unknown command `\class_identifier'
-/cbmc/jbmc/src/java_bytecode/select_pointer_type.h:50: warning: The following parameters of select_pointer_typet::specialize_generics(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, generic_parameter_recursion_trackingt &visited_nodes) const are not documented:
-  parameter 'visited_nodes'
 /cbmc/src/solvers/refinement/string_refinement.cpp:2099: warning: argument 'expr' of command @param is not found in the argument list of string_constraintt::universal_only_in_index(const string_constraintt &constr)
 /cbmc/src/solvers/refinement/string_refinement.cpp:2106: warning: The following parameters of string_constraintt::universal_only_in_index(const string_constraintt &constr) are not documented:
   parameter 'constr'
-/cbmc/jbmc/src/java_bytecode/README.md:26: warning: unable to resolve reference to `java-bytecode-remove-instance-of' for \ref command
-/cbmc/jbmc/src/java_bytecode/README.md:89: warning: explicit link request to 'define' could not be resolved
-/cbmc/jbmc/src/java_bytecode/README.md:89: warning: explicit link request to 'define' could not be resolved
 /cbmc/jbmc/src/java_bytecode/ci_lazy_methods_needed.h:40: warning: The following parameters of ci_lazy_methods_neededt::add_needed_class(const irep_idt &class_symbol_name) are not documented:
   parameter 'class_symbol_name'
 /cbmc/jbmc/src/java_bytecode/ci_lazy_methods_needed.h:38: warning: The following parameters of ci_lazy_methods_neededt::add_needed_method(const irep_idt &method_symbol_name) are not documented: