GeezerVison

…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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>

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) <[email protected]>