Translate instance methods via static-call-with-self encoding

examples/src/test/java/org/strata/jverify/examples/SourceContract.java

@@ -7,7 +7,7 @@
 
 import static org.strata.jverify.JVerify.*;
 
-@JVerifyTest(methodsVerified = 3, errorCount = 0)
+@JVerifyTest(methodsVerified = 2, methodsSkipped = 1, errorCount = 0)
 public class SourceContract {
 
     @Contract(Foo.class)

verifier/src/main/java/org/strata/jverify/verifier/compiler/simplifications/VerifyAnnotationCompiler.java

@@ -239,6 +239,30 @@ public HashMap<URI, IntervalTree<Integer, JavaMethodVerificationStatus>> getMeth
         return methodStatusPerUri;
     }
 
+    /**
+     * Whether the given method was recorded as {@code Skipped} (e.g. via
+     * {@code @Verify(false)}). Such methods are opted out of verification: their
+     * body has already been stripped, so JavaToLaurelCompiler should not emit a
+     * procedure shell for them (which would otherwise hit Strata limits such as
+     * constrained return types on bodiless functions).
+     *
+     * Returns false when the method has no recorded entry (synthetic / no-body
+     * methods), matching {@link #markSkipped}'s no-entry semantics.
+     */
+    public boolean isSkipped(JCTree.JCCompilationUnit compilationUnit, JCTree.JCMethodDecl methodDecl) {
+        var uriStatuses = methodStatusPerUri.get(compilationUnit.getSourceFile().toUri());
+        if (uriStatuses == null) {
+            return false;
+        }
+        return uriStatuses.streamNodes()
+                .map(node -> node.getValue())
+                .filter(status -> status.getMethodTree() == methodDecl)
+                .findFirst()
+                .map(status -> status.getVerificationStatus()
+                        == JavaMethodVerificationStatus.VerificationStatus.Skipped)
+                .orElse(false);
+    }
+
     /**
      * Demote a method's entry from Verified to Skipped. Called by
      * JavaToLaurelCompiler when per-method translation throws

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/AvoidNameCollisionsTest.java

@@ -7,7 +7,7 @@
 
 import static org.strata.jverify.JVerify.postcondition;
 
-@JVerifyTest(methodsVerified = 26, errorCount = 0)
+@JVerifyTest(methodsVerified = 19, errorCount = 0)
 public class AvoidNameCollisionsTest {
 
     void set(int set, int r_set) {}

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/MangledNameSeparation.java

@@ -0,0 +1,33 @@
+package org.strata.jverify.verifier.tests.javasupport;
+
+import org.strata.jverify.Pure;
+import org.strata.jverify.testengine.JVerifyTest;
+
+/**
+ * The mangled procedure name joins the enclosing class and the method with a
+ * separator that cannot appear in a Java identifier ('?'), so two distinct
+ * methods can never mangle to the same name. These two would collide under a
+ * '_' join — {@code Foo_bar.baz} and {@code Foo.bar_baz} both give
+ * {@code ...Foo_bar_baz} — but with the '?' separator they are distinct
+ * ({@code ...Foo_bar?baz} vs {@code ...Foo?bar_baz}), so both verify.
+ *
+ * <p>All five methods verify: the two here plus the three implicit constructors
+ * (outer, Foo_bar, Foo).
+ */
+@JVerifyTest(methodsVerified = 5, errorCount = 0)
+class MangledNameSeparation {
+
+    static class Foo_bar {
+        @Pure
+        int baz() {
+            return 0;
+        }
+    }
+
+    static class Foo {
+        @Pure
+        int bar_baz() {
+            return 0;
+        }
+    }
+}

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/StaticOverloadRefusal.java

@@ -0,0 +1,43 @@
+package org.strata.jverify.verifier.tests.javasupport;
+
+import org.strata.jverify.Pure;
+import org.strata.jverify.testengine.JVerifyTest;
+
+import static org.strata.jverify.JVerify.*;
+
+/**
+ * Overloaded methods all mangle to the same flat {@code Class_name} Laurel
+ * procedure name, so they collide. Until overload disambiguation is supported,
+ * such methods are refused with a clear diagnostic and flipped to Skipped
+ * rather than silently producing colliding procedures. The non-overloaded
+ * {@code unique} method still verifies. The verified count is 2 — {@code unique}
+ * plus the synthetic default constructor — matching the convention in
+ * {@code TranslatorSkip}.
+ */
+@JVerifyTest(
+        continueOnErrors = true,
+        exitCode = 0,
+        methodsVerified = 2,
+        methodsSkipped = 2,
+        errorCount = 0
+)
+class StaticOverloadRefusal {
+
+    @Pure
+    static int dup(int x) {
+//             ^ error: overloaded method 'dup' (enclosing class declares 2 methods with this name); overloading is not supported
+        return x;
+    }
+
+    @Pure
+    static int dup(boolean b) {
+//             ^ error: overloaded method 'dup' (enclosing class declares 2 methods with this name); overloading is not supported
+        return b ? 1 : 0;
+    }
+
+    @Pure
+    static int unique(int x) {
+        postcondition((int r) -> r == x);
+        return x;
+    }
+}

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/classes/ClassesExtendingClassesVerification.java

@@ -6,7 +6,7 @@
 
 import static org.strata.jverify.JVerify.*;
 
-@JVerifyTest(methodsVerified = 11, errorCount = 0)
+@JVerifyTest(methodsVerified = 7, errorCount = 0)
 public class ClassesExtendingClassesVerification {
     public void root() {
         Extender extender = new Extender(4);

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/classes/InstanceMethodContractViolated.java

@@ -0,0 +1,28 @@
+package org.strata.jverify.verifier.tests.javasupport.classes;
+
+import org.strata.jverify.Pure;
+import org.strata.jverify.Unbounded;
+import org.strata.jverify.testengine.JVerifyTest;
+
+import static org.strata.jverify.JVerify.postcondition;
+
+/**
+ * Negative twin of {@link InstanceMethodVerifies}: proves the instance-method
+ * encoding actually CHECKS the contract rather than verifying vacuously. The body
+ * returns {@code x + 1} but the postcondition claims {@code r == x + 2}, so
+ * verification must FAIL — not silently pass. {@code @Unbounded} avoids the
+ * unrelated bounded-int overflow obligation, so the sole error is the genuine
+ * contract violation. The class is {@code final} so the method is translated (not
+ * refused for polymorphic dispatch).
+ */
+@JVerifyTest(exitCode = 4, methodsVerified = 1, errorCount = 1)
+final class InstanceMethodContractViolated {
+
+    @Pure
+    @Unbounded
+    int addOne(@Unbounded int x) {
+        postcondition((int r) -> r == x + 2);
+//                               ^^^^^^^^^^ Error: assertion does not hold
+        return x + 1;
+    }
+}

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/classes/InstanceMethodVerifies.java

@@ -0,0 +1,43 @@
+package org.strata.jverify.verifier.tests.javasupport.classes;
+
+import org.strata.jverify.Pure;
+import org.strata.jverify.Unbounded;
+import org.strata.jverify.testengine.JVerifyTest;
+
+import static org.strata.jverify.JVerify.*;
+
+/**
+ * Positive happy-path for the static-call-with-self encoding: instance methods'
+ * real contracts are actually CHECKED (not vacuously verified) through the
+ * {@code self}-parameter translation. The class is {@code final} so calls are
+ * monomorphic (pass refuseIfPolymorphicDispatch); {@code @Unbounded} avoids the
+ * unrelated bounded-int overflow obligation. Verified count 4 = 3 methods +
+ * implicit constructor. Negative twin: {@link InstanceMethodContractViolated}.
+ */
+@JVerifyTest(methodsVerified = 4, errorCount = 0)
+final class InstanceMethodVerifies {
+
+    // @Pure instance method proving its own postcondition. @Pure + postcondition
+    // emits an opaque procedure taking `self` as its first parameter.
+    @Pure
+    @Unbounded
+    int addOne(@Unbounded int x) {
+        postcondition((int r) -> r == x + 1);
+        return x + 1;
+    }
+
+    // Non-pure instance method with a postcondition over its return value.
+    @Unbounded
+    int clampLow(@Unbounded int a) {
+        postcondition((int r) -> r >= 0);
+        return a > 0 ? a : 0;
+    }
+
+    // Instance method with a precondition and an in-body check.
+    @Unbounded
+    int guarded(@Unbounded int a) {
+        precondition(a > 0);
+        check(a + 1 > a);
+        return a;
+    }
+}

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/classes/NewReceiverRefusal.java

@@ -0,0 +1,27 @@
+package org.strata.jverify.verifier.tests.javasupport.classes;
+
+import org.strata.jverify.Pure;
+import org.strata.jverify.testengine.JVerifyTest;
+
+/**
+ * A method call on a freshly-allocated receiver (`new T().m()`) is refused
+ * gracefully: the `new T()` receiver lowers to an opaque `new_(T)` value that
+ * has no shape to pass as the callee's `self` parameter, so emitting the call
+ * would make Strata fail to unify the argument. Capturing constructor-allocated
+ * values is Step 8a. The refusal is reported here because the enclosing method
+ * is static.
+ */
+@JVerifyTest(continueOnErrors = true, exitCode = 0, methodsVerified = 3, methodsSkipped = 1, errorCount = 0)
+class NewReceiverRefusal {
+    static class Box {
+        @Pure
+        int value() {
+            return 0;
+        }
+    }
+
+    static void callOnFreshReceiver() {
+//              ^ error: method call on a freshly-allocated receiver is not yet supported
+        var ignored = new Box().value();
+    }
+}

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/classes/PolyDispatchSoundness.java

@@ -0,0 +1,42 @@
+package org.strata.jverify.verifier.tests.javasupport.classes;
+
+import org.strata.jverify.Pure;
+import org.strata.jverify.testengine.JVerifyTest;
+
+import static org.strata.jverify.JVerify.*;
+
+/**
+ * Soundness regression for the static {@code Class_method} mangling encoding.
+ *
+ * <p>{@code Class_method} mangling resolves an instance call against the
+ * receiver's STATIC type, so emitting {@code b.compute()} below would route to
+ * {@code BaseP}'s contract ({@code r >= 0}) even though {@code b} holds a
+ * {@code SubP} whose override returns {@code -1}. JVerify enforces no
+ * behavioural subtyping, so {@code SubP.compute} verifies vacuously against its
+ * own (empty) contract while {@code root} would falsely verify the
+ * {@code check} against the wrong contract.
+ *
+ * <p>The fix refuses any call that is not provably monomorphic (callee/class
+ * final or callee private). The call here is none of those, so {@code root} is
+ * refused — translated to a graceful skip with a diagnostic (the enclosing
+ * method is static) — rather than verified clean. Both {@code compute} bodies
+ * and the three implicit constructors still verify on their own; only the
+ * unsound call site is dropped.
+ *
+ * <p>Re-enable verification of this call when runtime dispatch lands
+ * (Strata#1174).
+ */
+@JVerifyTest(continueOnErrors = true, exitCode = 0, methodsVerified = 5, methodsSkipped = 1, errorCount = 0)
+class PolyDispatchSoundness {
+    static class BaseP {
+        @Pure int compute() { postcondition((int r) -> r >= 0); return 0; }
+    }
+    static class SubP extends BaseP {
+        @Pure @Override int compute() { return -1; }
+    }
+    static void root() {
+//              ^ error: polymorphic dispatch through interface/superclass is not yet supported
+        BaseP b = new SubP();
+        check(b.compute() >= 0);
+    }
+}

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/classes/PureCallResultUsedDirectly.java

@@ -0,0 +1,39 @@
+package org.strata.jverify.verifier.tests.javasupport.classes;
+
+import org.strata.jverify.Pure;
+import org.strata.jverify.Unbounded;
+import org.strata.jverify.testengine.JVerifyTest;
+
+import static org.strata.jverify.JVerify.*;
+
+/**
+ * A parameter-dependent {@code @Pure} method's result CAN be used by a caller
+ * when the call appears directly in the assertion/contract: the transparent
+ * function inlines at the use site, so the caller sees {@code addOne(a) == a+1}.
+ *
+ * <p>Contrast {@link PureCallResultViaLocal}, where binding the same call to an
+ * intermediate local first loses the relationship to {@code a} — a Strata prover
+ * limitation, not a front-end one. Verified count is 4 (three methods + implicit
+ * constructor).
+ */
+@JVerifyTest(methodsVerified = 4, errorCount = 0)
+final class PureCallResultUsedDirectly {
+
+    @Pure
+    @Unbounded
+    static int addOne(@Unbounded int x) {
+        return x + 1;
+    }
+
+    // Call used directly inside the check.
+    static void inCheck(@Unbounded int a) {
+        check(addOne(a) == a + 1);
+    }
+
+    // Call used directly inside the postcondition.
+    @Unbounded
+    static int inPostcondition(@Unbounded int a) {
+        postcondition((int r) -> r == a + 1);
+        return addOne(a);
+    }
+}

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/classes/PureCallResultViaUnboundedLocal.java

@@ -0,0 +1,36 @@
+package org.strata.jverify.verifier.tests.javasupport.classes;
+
+import org.strata.jverify.Pure;
+import org.strata.jverify.Unbounded;
+import org.strata.jverify.testengine.JVerifyTest;
+
+import static org.strata.jverify.JVerify.*;
+
+/**
+ * A parameter-dependent {@code @Pure} call result CAN be bound to an intermediate
+ * local and then used — provided the local carries the same numeric bound as the
+ * values it relates. An unannotated {@code int} local defaults to a bounded type
+ * ({@code int8}); binding an {@code @Unbounded} result into it would require
+ * discharging that bound (not provable in general), so the local must also be
+ * {@code @Unbounded} for {@code r == a + 1} to verify. Annotated, the caller
+ * verifies through the local binding.
+ *
+ * <p>Companion to {@link PureCallResultUsedDirectly} (call used directly, no
+ * local). Verified count is 3 (two methods + implicit constructor).
+ */
+@JVerifyTest(methodsVerified = 3, errorCount = 0)
+final class PureCallResultViaUnboundedLocal {
+
+    @Pure
+    @Unbounded
+    static int addOne(@Unbounded int x) {
+        return x + 1;
+    }
+
+    static void viaLocal(@Unbounded int a) {
+        // The local must be @Unbounded too: an unannotated int is int8, and
+        // relating a bounded local to an unbounded value is not provable.
+        @Unbounded int r = addOne(a);
+        check(r == a + 1);
+    }
+}

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/classes/SkippedConstructorContractNotVerified.java

@@ -0,0 +1,24 @@
+package org.strata.jverify.verifier.tests.javasupport.classes;
+
+import org.strata.jverify.testengine.JVerifyTest;
+
+import static org.strata.jverify.JVerify.postcondition;
+
+/**
+ * Soundness regression: a skipped member's contract must never count as Verified.
+ * Constructor translation is deferred, so {@code Box}'s contract is never checked
+ * by Strata; its postcondition here is deliberately FALSE. It must be counted
+ * Skipped (not Verified — that would be a false Verified). The one Verified method
+ * is the outer class's implicit constructor. Before the fix: 2 Verified / 0 errors.
+ */
+@JVerifyTest(methodsVerified = 1, methodsSkipped = 1, errorCount = 0)
+public class SkippedConstructorContractNotVerified {
+    static class Box {
+        private final int value;
+
+        public Box(int value_) {
+            this.value = value_;
+            postcondition(this.value == value_ + 1);
+        }
+    }
+}