From c1bc3808f4a03b825369a2a905709c0f68c3f0a1 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 22 Aug 2018 15:02:19 +0100 Subject: [PATCH 1/2] Expose a way for derived languages to specify additional entry points Lazy methods can be extened to load additional methods as entry points. This allows this to be meaningfully used by subclasses of java_bytecode_language --- jbmc/src/java_bytecode/java_bytecode_language.cpp | 13 +++++++++++++ jbmc/src/java_bytecode/java_bytecode_language.h | 2 ++ 2 files changed, 15 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 22a335d1be6..9d5297ea7bc 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -123,6 +123,9 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) extra_entry_points.end(), std::back_inserter(extra_methods), build_load_method_by_regex); + const auto &new_points = build_extra_entry_points(cmd); + extra_methods.insert( + extra_methods.end(), new_points.begin(), new_points.end()); if(cmd.isset("java-cp-include-files")) { @@ -1207,3 +1210,13 @@ bool java_bytecode_languaget::to_expr( java_bytecode_languaget::~java_bytecode_languaget() { } + +/// This method should be overloaded to provide alternative approaches for +/// specifying extra entry points. To provide a regex entry point, the command +/// line option `--lazy-methods-extra-entry-point` can be used directly. +std::vector +java_bytecode_languaget::build_extra_entry_points( + const cmdlinet &command_line) const +{ + return {}; +} diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index c754f59d8c6..c72a492f504 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -199,6 +199,8 @@ class java_bytecode_languaget:public languaget std::vector java_load_classes; private: + virtual std::vector + build_extra_entry_points(const cmdlinet &command_line) const; const std::unique_ptr pointer_type_selector; /// Maps synthetic method names on to the particular type of synthetic method From 232da1de63fc8341e8fe577211f9fed24a307800 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 23 Aug 2018 17:36:13 +0100 Subject: [PATCH 2/2] Add can_cast_type for java_generic_typet Note use is_reference since java_generic_typet inherits from reference_typet so this stronger requirement more closely matches the class hierarchy. --- jbmc/src/java_bytecode/java_types.h | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 0ca7538e95a..2fdcde619b0 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -452,11 +452,17 @@ class java_generic_typet:public reference_typet } }; +template <> +inline bool can_cast_type(const typet &type) +{ + return is_reference(type) && type.get_bool(ID_C_java_generic_type); +} + /// \param type: the type to check /// \return true if type is java type containing with generics, e.g., List inline bool is_java_generic_type(const typet &type) { - return type.get_bool(ID_C_java_generic_type); + return can_cast_type(type); } /// \param type: source type @@ -464,9 +470,7 @@ inline bool is_java_generic_type(const typet &type) inline const java_generic_typet &to_java_generic_type( const typet &type) { - PRECONDITION( - type.id()==ID_pointer && - is_java_generic_type(type)); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -474,9 +478,7 @@ inline const java_generic_typet &to_java_generic_type( /// \return cast of type into java type with generics inline java_generic_typet &to_java_generic_type(typet &type) { - PRECONDITION( - type.id()==ID_pointer && - is_java_generic_type(type)); + PRECONDITION(can_cast_type(type)); return static_cast(type); }