From 29e0e6375b3f2015643e9992ae91ea2128ce50af Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 4 Sep 2018 09:17:30 +0200 Subject: [PATCH 1/3] Mark native methods `java_method_typet` with `ID_is_native_method` --- jbmc/src/java_bytecode/java_bytecode_convert_method.cpp | 2 ++ src/util/irep_ids.def | 1 + 2 files changed, 3 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index d9229922ab7..1b2bc059ba9 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -372,6 +372,8 @@ void java_bytecode_convert_method_lazy( member_type.set(ID_is_synchronized, true); if(m.is_static) member_type.set(ID_is_static, true); + if(m.is_native) + member_type.set(ID_is_native_method, true); if(m.is_bridge) member_type.set(ID_is_bridge_method, m.is_bridge); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ca742f83b6f..cfbfe482ba0 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -387,6 +387,7 @@ IREP_ID_ONE(is_enum_constant) IREP_ID_ONE(is_inline) IREP_ID_ONE(is_extern) IREP_ID_ONE(is_synchronized) +IREP_ID_ONE(is_native_method) IREP_ID_ONE(is_global) IREP_ID_ONE(is_thread_local) IREP_ID_ONE(is_parameter) From dd0cc570b828b48d307787a3d16a6e5351b82b8b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 4 Sep 2018 14:04:49 +0200 Subject: [PATCH 2/3] Add getter/setter for `ID_is_native_method` --- .../src/java_bytecode/java_bytecode_convert_method.cpp | 3 +-- jbmc/src/java_bytecode/java_types.h | 10 ++++++++++ 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 1b2bc059ba9..668b2c1e02b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -372,8 +372,7 @@ void java_bytecode_convert_method_lazy( member_type.set(ID_is_synchronized, true); if(m.is_static) member_type.set(ID_is_static, true); - if(m.is_native) - member_type.set(ID_is_native_method, true); + member_type.set_native(m.is_native); if(m.is_bridge) member_type.set(ID_is_bridge_method, m.is_bridge); diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 4792231cdd7..2da36401905 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -288,6 +288,16 @@ class java_method_typet : public code_typet { set(ID_final, is_final); } + + bool get_native() const + { + return get_bool(ID_is_native_method); + } + + void set_native(bool is_native) + { + set(ID_is_native_method, is_native); + } }; template <> From dd0022510dc8940d484529251e37c2378fae3414 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 4 Sep 2018 14:19:21 +0200 Subject: [PATCH 3/3] Add unit test for `is_native` of `java_method_typet` --- .../ClassWithNativeMethod.class | Bin 0 -> 281 bytes .../ClassWithNativeMethod.java | 6 +++ .../convert_method.cpp | 41 +++++++++++++++++- 3 files changed, 46 insertions(+), 1 deletion(-) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.java diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.class b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.class new file mode 100644 index 0000000000000000000000000000000000000000..85b3b507176b2f67be88ea85322cda6ae0d219c2 GIT binary patch literal 281 zcmZvWKWhR(6vXGGpJ^E0;Ua)lX$(C8Y2J_@N}T zRw=T@{C4KeWA}Rdxd3=VBY}@vjE5L?LG)~LV_yV*r~4rYhQ(3~>Tf33ll^z9x9=*= zn8???^2thP)FqNxvEMHAt8vrTFjKqT+}QO*S#!{1ZP&%JzflKOMSxJy{I?-!xXvI` z`D!ptH+o^whQ|-Oy3n3_0;4h^f&%6i!Mg(>o^2+)9h|NY6h~|MmmA IikqPN3&V;q8UO$Q literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.java b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.java new file mode 100644 index 00000000000..58351bf9159 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithNativeMethod.java @@ -0,0 +1,6 @@ +public class ClassWithNativeMethod { + native boolean f(); + boolean f(int i) { + return false; + } +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index 8c0e45c18ef..db4ef399943 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ - Module: Unit tests for converting constructors and static initializers + Module: Unit tests for converting methods. Author: Diffblue Limited. @@ -56,6 +56,45 @@ SCENARIO( } } } + GIVEN("A class with a native method") + { + const symbol_tablet symbol_table = load_java_class( + "ClassWithNativeMethod", "./java_bytecode/java_bytecode_convert_method"); + + const std::string method_name = "java::ClassWithNativeMethod.f"; + + WHEN("When parsing the native method") + { + const symbolt function_symbol = + symbol_table.lookup_ref(method_name + ":()Z"); + + const java_method_typet &function_type = + require_type::require_java_method(function_symbol.type); + THEN("The method symbol should be of java_method_typet") + { + REQUIRE(function_type.get_bool(ID_C_java_method_type)); + } + THEN("And the method should be marked as a native method") + { + REQUIRE(to_java_method_type(function_type).get_native()); + } + } + WHEN("When parsing a non-native method") + { + THEN("THe method should not be marked as a native method") + { + const symbolt function_symbol = + symbol_table.lookup_ref(method_name + ":(I)Z"); + + const java_method_typet &function_type = + require_type::require_java_method(function_symbol.type); + THEN("The method should be marked as a native method") + { + REQUIRE_FALSE(to_java_method_type(function_type).get_native()); + } + } + } + } } SCENARIO(