From c07cab58669814b57629fd1b791ff1748ec22233 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 14 Sep 2018 09:05:37 +0100 Subject: [PATCH 1/4] Document, overlay classes, overlay methods and ignored methods Future improvements: - move this documentation to a better place --- .../java_bytecode_convert_class.cpp | 33 +++++++++++++++++++ jbmc/src/java_bytecode/java_class_loader.cpp | 22 +++++++++++-- 2 files changed, 52 insertions(+), 3 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 2a8d909d10f..44e04124e42 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -118,11 +118,44 @@ class java_bytecode_convert_classt:public messaget // see definition below for more info static void add_array_types(symbol_tablet &symbol_table); + /// Check if a method is an overlay method by searching for + /// `ID_overlay_method` in its list of annotations. + /// + /// An overlay method is a method with the annotation + /// \@OverlayMethodImplementation. They should only appear in + /// [overlay classes](\ref java_class_loader.cpp::is_overlay_class). They + /// will be loaded by JBMC instead of the method with the same signature + /// in the underlying class. It is an error if there is no method with the + /// same signature in the underlying class. It is an error if a method in + /// an overlay class has the same signature as a method in the underlying + /// class and it isn't marked as an overlay method or an + /// [ignored method](\ref java_bytecode_convert_classt::is_ignored_method). + /// + /// \param method: a `methodt` object from a java bytecode parse tree + /// \return true if the method is an overlay method, else false static bool is_overlay_method(const methodt &method) { return method.has_annotation(ID_overlay_method); } + /// Check if a method is an ignored method by searching for + /// `ID_ignored_method` in its list of annotations. + /// + /// An ignored method is a method with the annotation + /// \@IgnoredMethodImplementation. They will be ignored by JBMC. They are + /// intended for use in + /// [overlay classes](\ref java_class_loader.cpp::is_overlay_class), in + /// particular for methods which must exist in the overlay class so that + /// it will compile, e.g. default constructors, but which we do not want + /// to overlay the corresponding method in the + /// underlying class. It is an error if a method in + /// an overlay class has the same signature as a method in the underlying + /// class and it isn't marked as an + /// [overlay method](\ref java_bytecode_convert_classt::is_overlay_method) + /// or an ignored method. + /// + /// \param method: a `methodt` object from a java bytecode parse tree + /// \return true if the method is an ignored method, else false static bool is_ignored_method(const methodt &method) { return method.has_annotation(ID_ignored_method); diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 97431351e33..2d155ddb8ee 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -69,9 +69,25 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()( } /// Check if class is an overlay class by searching for `ID_overlay_class` in -/// its list of annotations. TODO(nathan) give a short explanation about what -/// overlay classes are. -/// \param c: a `classt` object from a java byte code parse tree +/// its list of annotations. +/// +/// An overlay class is a class with the annotation +/// \@OverlayClassImplementation. They serve the following purpose. When the JVM +/// searches the classpath for a particular class, it uses the first match, +/// and ignores any later matches. JBMC, however, will take account of later +/// matches as long as they are overlay classes. The +/// first match is then referred to as the underlying class. The +/// overlay classes can change the methods of the underlying class in the +/// following ways: adding a field (by having a new field), adding a method +/// (by having a new method) or +/// [changing the definition of a method](\ref java_bytecode_convert_classt::is_overlay_method). +/// It is an error if a method in an overlay class has the same signature as +/// a method in the underlying class and it isn't marked as an +/// [overlay method](\ref java_bytecode_convert_classt::is_overlay_method) +/// or an +/// [ignored method](\ref java_bytecode_convert_classt::is_ignored_method). +/// +/// \param c: a `classt` object from a java bytecode parse tree /// \return true if parsed class is an overlay class, else false static bool is_overlay_class(const java_bytecode_parse_treet::classt &c) { From 7cf35b10481656f68044934fd30dd63f02f57b0e Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 14 Sep 2018 11:52:48 +0100 Subject: [PATCH 2/4] Document overlay class and overlay method models --- .../annotations/org/cprover/OverlayClassImplementation.java | 4 ++++ .../annotations/org/cprover/OverlayMethodImplementation.java | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java index 5262c83ab2f..81377c12f43 100644 --- a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java +++ b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java @@ -1,4 +1,8 @@ package org.cprover; +/** + * Overlay classes are documented above `is_overlay_class()` in + * jbmc/src/java_bytecode/java_class_loader.cpp. + */ public @interface OverlayClassImplementation { } diff --git a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java index b885d4b6348..337d8244d55 100644 --- a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java +++ b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java @@ -1,4 +1,8 @@ package org.cprover; +/** + * Overlay methods are documented above + * `java_bytecode_convert_classt::is_overlay_method`. + */ public @interface OverlayMethodImplementation { } From 1b15e89939e5a967eceb2783713c9e7cf106bba4 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 14 Sep 2018 11:50:43 +0100 Subject: [PATCH 3/4] Print debug message for ignored methods --- .../java_bytecode_convert_class.cpp | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 44e04124e42..306df0a0ef6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -501,11 +501,16 @@ void java_bytecode_convert_classt::convert( { for(const methodt &method : overlay_class.get().methods) { - if(is_ignored_method(method)) - continue; const irep_idt method_identifier = qualified_classname + "." + id2string(method.name) + ":" + method.descriptor; + if(is_ignored_method(method)) + { + debug() + << "Ignoring method: '" << method_identifier << "'" + << eom; + continue; + } if(method_bytecode.contains_method(method_identifier)) { // This method has already been discovered and added to method_bytecode @@ -544,11 +549,16 @@ void java_bytecode_convert_classt::convert( } for(const methodt &method : c.methods) { - if(is_ignored_method(method)) - continue; const irep_idt method_identifier= qualified_classname + "." + id2string(method.name) + ":" + method.descriptor; + if(is_ignored_method(method)) + { + debug() + << "Ignoring method: '" << method_identifier << "'" + << eom; + continue; + } if(method_bytecode.contains_method(method_identifier)) { // This method has already been discovered while parsing an overlay From 41300064067d3cd61b9543076fad88aed48c1071 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 14 Sep 2018 11:51:41 +0100 Subject: [PATCH 4/4] Add test for ignored method annotation --- .../org/cprover/IgnoredMethodImplementation.class | Bin 0 -> 186 bytes .../org/cprover/IgnoredMethodImplementation.java | 8 ++++++++ .../jbmc/overlay-class/ignored-method/Test.class | Bin 0 -> 496 bytes .../jbmc/overlay-class/ignored-method/Test.java | 12 ++++++++++++ .../jbmc/overlay-class/ignored-test.desc | 10 ++++++++++ 5 files changed, 30 insertions(+) create mode 100644 jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.class create mode 100644 jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.java create mode 100644 jbmc/regression/jbmc/overlay-class/ignored-method/Test.class create mode 100644 jbmc/regression/jbmc/overlay-class/ignored-method/Test.java create mode 100644 jbmc/regression/jbmc/overlay-class/ignored-test.desc diff --git a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.class b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.class new file mode 100644 index 0000000000000000000000000000000000000000..b4f2e7ea3a3b509ed85db797ed706b8e7f762655 GIT binary patch literal 186 zcmX^0Z`VEs1_l!bPId-1b_RBK1`b9BuHgLAqU2P!%$!t41_jUby!@in6yMa6jQkYO z+=86c+|<01#FEVXJiV;MvP4D(_57lA{p5n8{Ib*{eLTt;83aHY^m7vP()In5vQm>v m7#ZXdLWy~K`4EHk9pOwhMg~R(CLm@8x|0D&vj9mZ237!LBsR?e literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.java b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.java new file mode 100644 index 00000000000..6789123fa4c --- /dev/null +++ b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.java @@ -0,0 +1,8 @@ +package org.cprover; + +/** + * Ignored methods are documented above + * `java_bytecode_convert_classt::is_ignored_method`. + */ +public @interface IgnoredMethodImplementation { +} diff --git a/jbmc/regression/jbmc/overlay-class/ignored-method/Test.class b/jbmc/regression/jbmc/overlay-class/ignored-method/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..2809640b3bc2ad31e8aad9c8bd7a2146f08eb54b GIT binary patch literal 496 zcmZut%Sr<=6g`=~>_b~ytqWJ~S_Nn0t|CZ5D2x_t>Bdz$4bzmFq-4^9pXEw$;RpCp z;?1=94&*-0z31fKyuH7?0=U3Y1vwm)a9Bc{p?E2kv{wwdPItnP@9UXhs0UJsyHzq3 zX3VECAHCZhh< zKV^pF`<1dX5d*cBsia4)mC}}5sTFa$fi{sJE{$Fb;}0UGjhNjEJJ+*8vW!I{)TWol zsEqW=gyKfJ!OL#8b2kn{=ZDCUlw$tak9nH@(x@Si0`23t42`d4hSP-zEl%LkC%WT- z+E5@{q|7JJ$QMqZ!Je{miEMELVu#||HZG$=Ss7JAyo`KCxg-A}R=*J$cCklIb-GTr OLEgiDW}BaA3-|yVi)sG= literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/overlay-class/ignored-method/Test.java b/jbmc/regression/jbmc/overlay-class/ignored-method/Test.java new file mode 100644 index 00000000000..db380c6a7a9 --- /dev/null +++ b/jbmc/regression/jbmc/overlay-class/ignored-method/Test.java @@ -0,0 +1,12 @@ +import org.cprover.OverlayClassImplementation; +import org.cprover.IgnoredMethodImplementation; + +@OverlayClassImplementation +public class Test +{ + @IgnoredMethodImplementation + public static void main(String[] args) + { + assert(true); + } +} diff --git a/jbmc/regression/jbmc/overlay-class/ignored-test.desc b/jbmc/regression/jbmc/overlay-class/ignored-test.desc new file mode 100644 index 00000000000..3649feb74c9 --- /dev/null +++ b/jbmc/regression/jbmc/overlay-class/ignored-test.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--classpath `../../../../scripts/format_classpath.sh . annotations . ignored-method` --verbosity 10 +^Ignoring method: 'java::Test\.main:\(\[Ljava/lang/String;\)V'$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^Skipping class Test marked with OverlayClassImplementation but found before original definition$ +^Adding symbol from overlay class: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$