Soundness holes: Tests and fixes#257
Open
GUIpsp wants to merge 21 commits into
Open
Conversation
…ests Compiles each testSuite/Error*Unsound.java and runs it in-process under a child class loader with assertions enabled (no forked JVM), requiring it to abort with an AssertionError -- validating each as a genuine hole: the verifier accepts it AND the program is unsafe at runtime. The embedded assert is an independent oracle (it does not trust the verifier). A generated self-check fixture keeps the harness exercised (and this commit green) before any soundness-hole test exists. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Verifier proves _ < 1.0 for 7.0 % 4.0, but Java yields 3.0. Root: floating-point % is lowered to IEEE-754 remainder via mkFPRem (TranslatorToZ3.java:344-345); Java % is fmod. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
TranslatorToZ3.makeMod lowered FP `%` to z3.mkFPRem (IEEE-754 remainder, which rounds the quotient to nearest), but Java `%` on float/double is fmod: a - b * trunc(a/b), with the quotient rounded toward zero and the result taking the sign of the dividend. Encode fmod directly. Closes the ErrorFloatRemainderUnsound hole: 7.0 % 4.0 now evaluates to 3.0 (not the IEEE remainder -1.0), so the verifier correctly rejects @refinement("_ < 1.0"). CorrectFPArithmetic (6.0 % 4.0 == 2.0) stays green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Verifier proves _ == 0.1 for float f = 0.1f, but the single-precision value is not 0.1. Root: float is modeled as FP64 in the constant path (TranslatorContextToZ3.java:97; literals TranslatorToZ3.java:110), inconsistent with the FP32 mapping at :136-137. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
float values were translated to FP64, so single-precision rounding was lost. Model float-origin values as binary32 and apply Java's binary numeric promotion: when a binary32 operand meets a binary64 one, widen the float to binary64 (mkFPToFP) so sorts match and semantics mirror Java. FP comparison/arithmetic helpers now coerce operands to a common FP sort (FP64 if either is double, else FP32). LiteralReal carries an isFloat flag (float vs double origin); Predicate tags Types.FLOAT literals; ExpressionToZ3Visitor emits makeFloatLiteral (mkFP at FP32) for them; TranslatorContextToZ3 creates float constants at FP32 (consistent with the existing getSort mapping). Closes ErrorFloatPrecisionUnsound: (float)0.1 widened to double != 0.1, so @refinement("_ == 0.1") on float f = 0.1f is correctly rejected. CorrectFPArithmetic (double) and CorrectPrimitiveNumbersTypes (float) stay green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Verifier proves _ == 1 for x after false && ((x = 1) == 1), but the && short-circuits so x stays 0. Root: both operands are refined unconditionally (OperationsChecker.java:68-69). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
RefinementTypeChecker (a CtScanner) descends into a binary operator's children before its override runs, so an assignment in the right operand of `&&`/`||` (which executes only conditionally at runtime) was committed to the variable context unconditionally. visitCtBinaryOperator now, after computing the boolean value refinement, havocs every variable written in the conditionally-evaluated (right) operand — installing a fresh unconstrained instance — so its post-value is treated as unknown. This only ever weakens knowledge, so it cannot accept an unsound program. Closes ErrorShortCircuitAssignUnsound: after `false && ((x=1)==1)` the verifier no longer believes x==1, so @refinement("_ == 1") int y = x is correctly rejected. &&/|| Correct tests (CorrectImplies, CorrectBooleanLitAndInvocations, CorrectOperatorPrecedence) stay green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Verifier proves _ > 0 reading a field annotated _ > 0 that defaults to 0. Root: field refinements are trusted on read (RefinementTypeChecker.java:256,272) without proving establishment. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
visitCtFieldRead modeled every `o.field` read as `_ == this#field`, pulling in the field's declared @refinement even when the field was never established. For an external read (not a this-access) of a field with no initializer, the runtime value is the Java default, which the declared refinement may not satisfy. Now such reads are modeled as `_ == <default>` (0 / 0.0 / false; references unchanged) instead of assuming the refinement. this-accesses and initialized fields keep their existing behavior. Closes ErrorFieldDefaultUnsound: reading uninitialized `int n` (default 0) into @refinement("_ > 0") int x is correctly rejected. Field / static-final / enum Correct tests stay green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Verifier proves _ == 1 after while (x < 2) x = x + 1, but the loop exits with x == 2. Root: no loop fixpoint or havoc; the body is treated as completing once (RefinementTypeChecker.java:458-459). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Loops had no special handling: the body was scanned once and its assignments committed, so a variable mutated in a loop kept a single-pass value afterward (e.g. while(x<2) x=x+1 left x==1). Added visitors for while/do/for/for-each that, after visiting the body once (so in-body refinement/typestate errors are still reported), havoc every variable written in the body (and the for-update/condition) via the existing havocVariable helper, so post-loop values are treated as unknown. Havoc only weakens knowledge, so it cannot accept an unsound program. Only direct value writes (CtVariableWrite) are havoc'd; typestate mutated through method calls (e.g. rs.next()) is untouched, so loop-based typestate/iterator Correct tests stay green. Closes ErrorLoopSinglePassUnsound: after the loop x is unknown, so @refinement("_ == 1") int y = x is correctly rejected. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Verifier proves _ == 1 after a try whose first statement 1 / 0 throws, but x stays 0. Root: try/catch flow is not modeled (RefinementTypeChecker.java:458-459). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
try/catch flow was unmodeled: the try body was scanned straight-line, so an assignment after a throwing statement was trusted though it may never run. Added visitCtTry that, after visiting (so in-body/in-handler errors are still reported), havocs every variable written in the try body and each catch block, treating their post-try values as uncertain. finally blocks always complete, so their definite assignments are left trusted. Closes ErrorExceptionFlowUnsound: 1/0 throws so x stays 0; after havoc x is unknown, so @refinement("_ == 1") int y = x is correctly rejected. The existing try/catch typestate test (IteratorRemoveBeforeNext) stays green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Verifier proves _ == 1.9 for (int) 1.9, but the cast yields 1. Root: cast expressions are not modeled (RefinementTypeChecker.java around 544); the subtype check can then pass vacuously (SMTEvaluator.java:36). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Cast expressions were ignored, so `(int) 1.9` was modeled as 1.9 and @refinement("_ == 1.9") int x = (int) 1.9 was vacuously accepted. A float/double -> integral narrowing cast now rewrites the value refinement `_ == E` to `_ == $truncateToZero(E)` (JLS 5.1.3, round toward zero), applied at the assignment-RHS chokepoints. The builtin $truncateToZero reuses the existing FunctionInvocation path (no parser or simplifier changes). Identity and widening casts are left untouched. Closes ErrorNarrowingCastUnsound: (int)1.9 is 1, so _ == 1.9 is correctly rejected (counterexample x == 1). Cast/numeric Correct tests (CorrectOperatorAssignments, CorrectFPArithmetic, CorrectBoxedTypes, CorrectPrimitiveNumbersTypes) stay green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
After b = a then a.close(), the verifier still treats b as open and accepts b.read(), but b aliases the closed object. Root: a transition attaches the new state to the receiver variable only (object_checkers/AuxStateHandler.java); aliases keep stale state. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A reference-copy `X b = a;` makes b's instance value-equal to a's current instance, but a transition (a.close()) created a new instance for a while leaving the shared old instance in its stale state, so b kept the pre-transition state. Added an object-alias registry to Context: reference-copy assignments (bare variable read of another tracked reference) record an alias; any other RHS clears it. On a successful state transition, AuxStateHandler havocs the tracked state of all aliases of the receiver, so they are no longer trusted at the old state. Triggers only on real aliasing, so single-reference usage is unaffected. Closes ErrorTypestateAliasUnsound: after `b = a; a.close()`, b's state is unknown, so b.read() (requires open) is correctly rejected. Typestate Correct tests stay green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Verifier proves _ > 0 for int c = 46341 * 46341, but the product overflows int to -2147479015. Root: int is modeled as an unbounded Z3 Int (TranslatorContextToZ3.java:93; TranslatorToZ3.java:103,327). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Verifier proves _ >= 0 for (-7) % 3, but Java yields -1. Root: makeMod uses Euclidean Z3 mkMod (TranslatorToZ3.java:344); Java % follows the sign of the dividend. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Verifier proves _ > 3 for 7L / 2L, but Java truncates to 3. Root: long is modeled as a Z3 Real (TranslatorContextToZ3.java:96; makeLongLiteral :106), so division is exact and rational (makeDiv:336). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Migrate int/short/char/byte -> 32-bit BitVec and long -> 64-bit BitVec in the SMT translation. Z3 BitVec ops match Java exactly: mkBVAdd/Sub/Mul wrap (two's-complement overflow), mkBVSDiv truncates toward zero, mkBVSRem takes the sign of the dividend, signed comparisons; int<->long mixing sign-extends, and BV<->real/FP coercions go through mkBV2Int/getLong. ExpressionFolding (Java-int constant folding) is now consistent with the solver. Closes three holes at once: ErrorIntOverflowUnsound (46341*46341 wraps to -2147479015), ErrorNegativeModuloUnsound (-7 % 3 == -1), and ErrorLongAsRealDivisionUnsound (7L/2L == 3). Sound fixed-width semantics also exposed six Correct tests that were themselves latently unsound (they asserted mathematically-true but Java-false postconditions that overflow): CorrectSimpleIfElse (-a at MIN_VALUE), CorrectSpecificFunctionInvocation / CorrectLongUsage / CorrectFunctionsTutorial / CorrectIfThen / CorrectOperatorAssignments (+,-,* overflow). Each now carries overflow-guard preconditions/bounds so its postcondition genuinely holds (CorrectLongUsage widens to long before multiplying). ErrorLongUsage gains a third expected-error marker for the now-correctly-rejected overflow in its own body. Whole verifier suite is green (304 tests, 0 failures); all 11 Error*Unsound holes are now rejected. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Collaborator
|
@GUIpsp thanks for the contribution. I don't have time to go through all the commits, if you want to contribute please split up the commits in PRs with the template description |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
This fixes a bunch of soundness holes. The commits have the full details. The last commit might be controversial. Cherry pick what you need.
Type of change
Checklist
liquidjava-example/src/main/java/testSuite/(Correct*/Error*)mvn testpasses locally