From 47a8f4e550c2ccdd6a3b0acdb4ce7f4eed084af2 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Fri, 24 May 2019 14:56:13 +0100 Subject: [PATCH 1/2] Add function that checks if function id represents a clinit. A utility for checking whether the supplied function id corresponds to a clinit. --- jbmc/src/java_bytecode/java_static_initializers.cpp | 8 ++++++++ jbmc/src/java_bytecode/java_static_initializers.h | 1 + 2 files changed, 9 insertions(+) diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 9bb4ee4c0db..8d8e22cdb1b 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -80,6 +80,14 @@ bool is_clinit_wrapper_function(const irep_idt &function_id) return has_suffix(id2string(function_id), clinit_wrapper_suffix); } +/// Check if function_id is a clinit +/// \param function_id: some function identifier +/// \return true if the passed identifier is a clinit +bool is_clinit_function(const irep_idt &function_id) +{ + return has_suffix(id2string(function_id), clinit_function_suffix); +} + /// Add a new symbol to the symbol table. /// Note: assumes that a symbol with this name does not exist. /// /param name: name of the symbol to be generated diff --git a/jbmc/src/java_bytecode/java_static_initializers.h b/jbmc/src/java_bytecode/java_static_initializers.h index 70736244110..4ae6593f566 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.h +++ b/jbmc/src/java_bytecode/java_static_initializers.h @@ -25,6 +25,7 @@ irep_idt clinit_wrapper_name(const irep_idt &class_name); irep_idt user_specified_clinit_name(const irep_idt &class_name); bool is_clinit_wrapper_function(const irep_idt &function_id); +bool is_clinit_function(const irep_idt &function_id); void create_static_initializer_symbols( symbol_tablet &symbol_table, From c227ab5ca65bb56d2099e5b0214fed9d9b1e3af5 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Tue, 28 May 2019 10:42:47 +0100 Subject: [PATCH 2/2] Unit test for is_clinit_function Shows that is_clinit_function returns true iff input has method signature with a suffix that matches that of clinit --- jbmc/unit/Makefile | 1 + .../java_static_initializers.cpp | 26 +++++++++++++++++++ .../module_dependencies.txt | 2 ++ 3 files changed, 29 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp create mode 100644 jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 7753caca810..0ccebf80ce4 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -47,6 +47,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ java_bytecode/java_object_factory/struct_tag_types.cpp \ java_bytecode/java_replace_nondet/replace_nondet.cpp \ + java_bytecode/java_static_initializers/java_static_initializers.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ java_bytecode/java_types/erase_type_arguments.cpp \ java_bytecode/java_types/generic_type_index.cpp \ diff --git a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp new file mode 100644 index 00000000000..cdf2d3d7b13 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp @@ -0,0 +1,26 @@ +/*******************************************************************\ + +Module: Unit tests for java_types + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include + +SCENARIO("is_clinit_function", "[core][java_static_initializers]") +{ + GIVEN("A function id that represents a clinit") + THEN("is_clinit_function should return true.") + { + const std::string input = "com.something.package.TestClass.:()V"; + REQUIRE(is_clinit_function(input)); + } + GIVEN("A function id that does not represent a clinit") + THEN("is_clinit_function should return false.") + { + const std::string input = "com.something.package.TestClass.:()V"; + REQUIRE_FALSE(is_clinit_function(input)); + } +} diff --git a/jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt b/jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt new file mode 100644 index 00000000000..7c65cd85bde --- /dev/null +++ b/jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt @@ -0,0 +1,2 @@ +java_bytecode +testing-utils