From 97484c4d32cc8e2330863f1a9cec7900bd2be043 Mon Sep 17 00:00:00 2001 From: svorenova Date: Tue, 13 Nov 2018 10:44:03 +0000 Subject: [PATCH 1/7] Document pointer type selection interface --- jbmc/src/java_bytecode/README.md | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md index 598a6e9f0a..0e034c2df5 100644 --- a/jbmc/src/java_bytecode/README.md +++ b/jbmc/src/java_bytecode/README.md @@ -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. From 53126060ed61862d2637d6eb70c2ebe36355fb6e Mon Sep 17 00:00:00 2001 From: svorenova Date: Tue, 13 Nov 2018 10:54:41 +0000 Subject: [PATCH 2/7] Move documentation of public functions to the header --- .../src/java_bytecode/select_pointer_type.cpp | 27 ------------------ jbmc/src/java_bytecode/select_pointer_type.h | 28 +++++++++++++++++++ 2 files changed, 28 insertions(+), 27 deletions(-) diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index e0ec682857..048f8138ed 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -14,15 +14,6 @@ #include "java_types.h" #include -/// 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 diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h index 482c8fdbbd..97c5e3e294 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.h +++ b/jbmc/src/java_bytecode/select_pointer_type.h @@ -36,6 +36,16 @@ class select_pointer_typet public: virtual ~select_pointer_typet() = default; + + /// 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 virtual pointer_typet convert_pointer_type( const pointer_typet &pointer_type, const generic_parameter_specialization_mapt @@ -47,6 +57,24 @@ public: const irep_idt ¶meter_name, const namespacet &ns) const; + /// 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 specialize_generics( const pointer_typet &pointer_type, const generic_parameter_specialization_mapt From ea9bcc5d69f0bf9efc8463c97722c33fb66c8e74 Mon Sep 17 00:00:00 2001 From: svorenova Date: Tue, 13 Nov 2018 10:55:02 +0000 Subject: [PATCH 3/7] Document get_parameter_alternative_types --- jbmc/src/java_bytecode/select_pointer_type.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h index 97c5e3e294..f8daa1f476 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.h +++ b/jbmc/src/java_bytecode/select_pointer_type.h @@ -52,6 +52,9 @@ public: &generic_parameter_specialization_map, const namespacet &ns) const; + /// Get alternative types for a method parameter. For 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 get_parameter_alternative_types( const irep_idt &function_name, const irep_idt ¶meter_name, From eb9bb0686b2bfed6f437cee3f9b009138bcc749f Mon Sep 17 00:00:00 2001 From: svorenova Date: Tue, 13 Nov 2018 11:12:51 +0000 Subject: [PATCH 4/7] Document a function parameter And rename it to match the name used in the implementation file --- jbmc/src/java_bytecode/select_pointer_type.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h index f8daa1f476..5e7aaa91e5 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.h +++ b/jbmc/src/java_bytecode/select_pointer_type.h @@ -76,13 +76,15 @@ public: /// \param pointer_type 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 concrete /// 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 From 75b18015b98a1700ce865c80cba935a6f5ea193b Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 14 Nov 2018 10:32:48 +0000 Subject: [PATCH 5/7] Update function docs --- jbmc/src/java_bytecode/select_pointer_type.h | 45 +++++++++++--------- 1 file changed, 24 insertions(+), 21 deletions(-) diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h index 5e7aaa91e5..d8e508206c 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.h +++ b/jbmc/src/java_bytecode/select_pointer_type.h @@ -37,14 +37,14 @@ class select_pointer_typet public: virtual ~select_pointer_typet() = default; - /// Select what type should be used for a given pointer type. For the base + /// 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 - /// 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 + /// 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, @@ -52,19 +52,22 @@ public: &generic_parameter_specialization_map, const namespacet &ns) const; - /// Get alternative types for a method parameter. For the base class we - /// just return an empty set. Derived classes can override this behaviour - /// to provide more sophisticated alternative type identification. + /// 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 get_parameter_alternative_types( const irep_idt &function_name, const irep_idt ¶meter_name, const namespacet &ns) const; /// 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). + /// 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` 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 @@ -72,14 +75,14 @@ public: /// /// - 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 - /// \param visited_nodes set of parameter names already considered in + /// - 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 concrete - /// types, if set in the current scope + /// \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 From b12c80f9e4748985a39a44f90559792c7ec53764 Mon Sep 17 00:00:00 2001 From: svorenova Date: Thu, 15 Nov 2018 10:07:02 +0000 Subject: [PATCH 6/7] Fix doxygen warnings in java_bytecode/README.md --- jbmc/src/java_bytecode/README.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md index 0e034c2df5..46331a1d50 100644 --- a/jbmc/src/java_bytecode/README.md +++ b/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) @@ -96,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 From 175099d5be545fa6b4bdcd752d9fdef19c660ba8 Mon Sep 17 00:00:00 2001 From: svorenova Date: Thu, 15 Nov 2018 10:43:44 +0000 Subject: [PATCH 7/7] Remove expected doxygen warnings --- scripts/expected_doxygen_warnings.txt | 5 ----- 1 file changed, 5 deletions(-) diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index 3c08919551..fbf94c86f1 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -116,14 +116,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 ¶meter) 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: