Repository navigation
Conversation
Contributor
Code coverage overviewLanguages: Java Java / code-coverage/jacoco-ubuntu-latest-21
View coverage of the 10 most impacted files.
ℹ️ Calculations represent line coverage. Results may change as calculations are updated. Updated |
Contributor
Author
|
@unp1 @mattulbrich If you want, feel free to poke it. Officially, the AI starts believing in this thing. I would have my doubts. |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
Parameterized tables for every binary operator in Int and BV arithmetic modes, all literal nodes, and compound expressions; dedicated tests for casts, instanceof, conditional/ite, array/null comparison special case, \result, \old/old (pre-state environment), name/field handler dispatching, JML infix operators, chained comparisons, JML quantifiers (forall/exists, range guards, array and non-primitive binders, bound-variable shadowing), array creation (length assertion vs. initializer), and constructor default handling. Also fixes a latent bug: the JML keyword form \old(x) is lexed with a leading backslash in the method name and was falling through to the call handler, silently becoming an unconstrained constant. Both 'old(x)' and '\old(x)' are now resolved against the pre-state environment.
VC-generation stage suite (VcgSemanticsTest.kt) covering proven, falsifiable and rejected-generation cases in both UNBOUNDED (Int) and BOUNDED (BV32) modes. Fixes uncovered while making the suite green: - execAssign now binds variables phi-style (v' = ite(g, rhs, prev)) so statements on dead paths (after break/continue/return) keep their previous value instead of leaking a fresh unconstrained constant into loop merges and postconditions. - setFlag and execReturn use the same phi form (hard equality) so abrupt completion flags are defined when their guard is false. - array lengths are axiomatised non-negative; without it a BV32 length could take a huge negative value that passes 'len <= 4' under signed comparison, turning a binary-search bound into nonsense (unsound BOUNDED binarySearch). - loop-exit merges fall back to an unconstrained constant of the correct sort ($undef_N) for locations absent from exit snapshots instead of makeFalse(). - array element sorts come from the array's declared sort (BV32 element in BOUNDED, Int in UNBOUNDED); bvsaddo/bvssubo/bvsmulo drop the extra width argument; IntArithmeticTranslator maps boolean/float/double primitives to their real SmtTypes.
Add 45 new corner-case fixtures and tests to the VC-generation suite: - MIN/MAX literals and boundary arithmetic (intMinLiteral, intMaxLiteral, nearMax, boundedIncrement, maxOverflow, minUnderflowWrap) - instanceof as a statement (stmtInstanceof, stmtInstanceofCount) - return/continue/break combined with loops and try-catch-finally (returnInsideLoop, plainReturnInLoop, tryBreakContinue, continueCountOnly, nonNormalLoopExit, nestedTry, tryReturnFinally) - falsifiable-by-design wrong-spec fixtures (returnEarlyNoContinue, tryBreakOnly, continueThenReturn, loopContinueNoTry, loopBreakNoTry, nestedCatchFinally, minUnderflow) - dedicated tests documenting that boxed parameter unboxing and boxed return types are rejected at generation time Engine fixes: - declare the String type sort in the hierarchy and qualify 'String' in instanceof translation (previously emitted an undeclared sort_string) - reject boxed return types (Integer etc.) up front with a clear error instead of emitting an ill-sorted query
Drive VcgResult.kt to 100% line / 100% branch coverage: - parameterized verdict mapping over the shared fixture bank with a stub solver: all-unsat -> PROVEN (95 rows, also asserting memoization and failedConditions reuse), all-sat -> FAILED (17 rows, failedConditions returns every condition), all-unknown -> UNKNOWN (20 rows) - dedicated checks of the verdict loop edge cases: mixed answers mapped in order, answers shorter/trailing/empty/malformed-error tokens, empty condition lists, memoized single solver invocation, copy() giving an independent cache, fresh results re-checking, Status enum, the VerificationCondition data class (components/copy/equality/hash/toString/ range default), and toString on both populated and empty results - checkProgressive: live+final streaming with correct totals, default-arg bridges, cancelled runs that leave unanswered conditions UNKNOWN and are NOT memoized, explicit timeout and failed-verdict reporting - end-to-end runs against the real Z3 solver (guarded by an installation assumption) for a proven, a falsifiable and a constructor fixture
Coverage for tools:vcg now at 97.85% instr / 98.52% line / 88.40% branch across the module, with the ir/ package fully covered (100%). Production: - Remove NfBlock and Statement.asNfOrigin from ir/NfStmt.kt; the IR never constructed a block, and all three walk sites in Vcg.kt (execStmt, modifiedLocations, collectCalleeDeclaredKeys) plus Normalizer.kt were dead. - Drop now-unused imports in Normalizer.kt and NormalizerTest.kt. Fixtures (VcgExamples.java) and rows (VcgSemanticsTest): - makeArray: `return new int[n]` covers ExprTranslator's ArrayCreationExpr visit and the anonymous-array naming (a declarator initializer would be cloned by the normalizer and detached, breaking calculateResolvedType). - returnsUnknown: unresolvable return type -> returnTypeOf fallback. - catchUnknownType: local declared with an unresolvable type -> tryResolve fallback through the assignment-target sort path (an unresolvable *catch* type would break the catch-match guard, which emits an undeclared sort). - callInlineSwitch/helperSwitch + rejection test: switch inside an inlined callee is collected by declared-locals walk before being rejected. - readUnknownField: host-selector fallback for a missing field on a resolved receiver, covering the backwards-sort fallback branch. Tests: - ExprTranslatorTest.testPrimitiveCastIsElided / testReferenceCastEmitsCastTerm cover both cast branches (elide vs. `(cast value sort_C)`). - switch-inline rejection, options lookup/value semantics, and orphan-callable context rejection tests cover the remaining option and context helpers. Suite: 682 tests green (132/202/158/163/27).
The VCG overflow obligations used Z3's bvsaddo/bvssubo/bvsmulo predicates, which do not exist in the Z3 4.8.12 that the CI installs via apt on Ubuntu 24.04, so the solver rejected the query and VcgSemanticsTest's bounded overflow cases (boundedAdd/boundedMul/boundedSub, overflowDetected, boundedOverflow) failed. Encode signed overflow portably instead: sign-extend both operands to a width in which the exact result cannot wrap (w+1 for +/-, 2w for *), compare the exact result against the sign-extended Java wrap-around result, and flag overflow when they differ. Adds SmtTermFactory.signExtend.
… string index Add four opt-in implicit-exception checks, each gated by a VcgOptions flag and a matching VcgCommand CLI option: - nullcheck: guard -> receiver != null on field-access receivers and instance method-call receivers (arrays exempt: encoded as value maps) - castcheck: guard -> instanceof(v, sort_T) for reference casts; new T(...) binds typeof/instanceof of the fresh object so casts of fresh objects prove - negative-array-size: guard -> dim >= 0 on new T[n] (always provable under the non-negative array-length axiom; test asserts emission + provability) - string-index: engine-internal String/StringBuilder specs (charAt, codePointAt, substring); stringLength function over U, String.length() modelled as a read, declared string-literal constants with length asserts Also folds in earlier uncommitted branch work: VcgFacade/VcgCache with the <fqdn>#method#kind-N@line:col condition-id convention, jmlstub JRE stub regeneration, and the SmtTermFactory idivide soundness fix for Z3 4.8.x.
…non-null The report of `jmltk vcg` is now emitted as soon as a callable's conditions have been solved instead of after all callables finish: VcgFacade gains a callback overload of verifyAndCheckAll that invokes the consumer from the worker thread (completion order) and still blocks until every callable is done; VcgCommand prints each outcome under an output lock so lines of one callable stay contiguous and the totals stay exact. String literals are now declared reference constants (declared once per value, asserted non-null) whenever a receiver-sensitive check is active, so `--check-null` on a literal receiver is provable instead of spuriously FAILing, identical literals no longer emit duplicate declarations, and `--check-string-index` still binds each literal's runtime length.
The solver watchdog used to wake every 100 ms and re-check the cancel flag and deadline. It now waits on a ReentrantLock Condition: the run loop signals it after every parsed answer (so a fresh cancellation is picked up at the latest when the next answer arrives) and shutdown() signals on teardown, while the deadline is handled exactly by awaitNanos. No timer-based polling remains: the watchdog wakes only on progress, shutdown, or deadline.
Model array `==`/`!=` as reference (identity) equality instead of extensional content equality: a store through one alias is exactly a store through the other, so when the identities match the last write wins. Identities are plain `U` values produced by the lazily-declared `$arrayref_<elem>` functions, so the solver can decide aliasing without extensional (content) reasoning. - `==`/`!=` on arrays translates to identity comparison in both the VCG atom and the expression translator (wired through `arrayRefHandler`). - every element store frames the other live array values with `ite(refEqual, store, old)` and preserves their lengths and identities; the stored array keeps its identity too. - copying an array reference (`y = x`) copies the identity, and if-merges emit identity phis so a merged array is whichever branch was taken. - fixtures: aliasArrayParams (the `a==b ==> a[0]==2` case), aliasArrayParamAliased, aliasArrayLocal, aliasArrayTwoLocals, inlineAliasedTwoArgs/bumpBoth.
Scalar/object instance fields of arbitrary receivers (parameters, locals, `this.<field>` objects) are versioned `(Array U T)` heap maps keyed globally by `fld$<tag>.<field>` and SSA-versioned like a local: a write is `map' = ite(g, store(map, receiver, v), map)`, a read is `select(map, receiver)`. Must-alias references (`b2 = b`) share one `U` identity, so `b2.value = 5` is observable as `b.value == 5`; distinct objects observe nothing. - reads of `scope.field` on arbitrary receivers prefer the identity map, then a per-receiver slot, then an unconstrained base (never the enclosing-class type). - `this`-receiver writes keep the flat per-path slot but also update the map, so inlined/contracted callee receivers and `this` aliases observe them. - assignable `this.f` clauses on receiver-bound contract calls refresh the map entry at the receiver; `\everything`/no-assignable havocs version every map. - loop merges and invariant havocs version field-map keys with their printable `(Array U …)` sort (the generic printer would emit the invalid `Object` placeholder), and `modifiedLocations` records map keys for field writes. - fixtures: aliasObjectLocal, aliasObjectTwice (proven in both modes).
Reads of `this`-receiver fields (explicit `this.f`, bare `f`) now go through the identity-keyed field map whenever it is live, so a write through a must-alias of the enclosing instance (`VcgExamples alias = this; alias.val = 9` or a parameter assumed `alias == this`) is observable as `this.val` / bare `val`. Previously such writes updated only the map entry of the alias and this-receiver reads kept returning the stale flat slot — the documented limitation. To keep the flat and map models consistent: - bare writes to fields of the enclosing instance (`counter = 0` normalizes to NfLocal) now update the field map like explicit `this.f = v` writes; - declaring a field map anchors `select(base, this)` to the flat `this.<field>` entry, so requires/entry assumptions on a this-field survive reads switching to the map; - loop merges (unroll final merge, invariant havoc) version this-receiver field-map keys like any modified location, and the invariant step-3 havoc declares map sorts with the printable `(Array U ...)` sort; - `assignable this.f` contract clauses refresh the map entry even without a receiver (plain `assigns f` on the enclosing instance), matching the receiver-bound case. `\old` resolution is fixed along the way: the this-read handler now takes the environment map explicitly so `old(...)` translates against the pre-state instead of the current state. New fixtures `aliasThisViaLocal`, `aliasThisViaParam`, `setValViaAlias` are proven in both UNBOUNDED and BOUNDED modes.
Class-level `invariant` clauses are gathered from the context (the enclosing type and its statically-visible ancestors in the same CU) and folded by a single code transformation into one large conjunction in which every clause is wrapped in a `\lblpos` label that keeps its identity: (\lblpos inv_1 e1 && \lblpos inv_2 e2 && ...) The folded expression is added to the entry assumptions (JML: a non-helper instance method may assume `\invariant_for(this)`) and to the exit obligation (every instance method and constructor must preserve it). `helper` methods and static methods are exempt. Literal `\invariant_for(..)` / `\static_invariant_for(..)` expressions - parsed as `\`-prefixed method calls - expand to the same fold, with a non-`this` receiver bound as the invariants' `this`. `\lbl`/`\lblpos`/`\lblneg` label nodes are transparent to translation. Also fixes the unknown-field/unknown-name fallback to be mode aware (BV32 in bounded mode), which surfaces when invariants read fields of a superclass that the engine does not track as flat slots.
Tie the havoced return/break/continue flags to 'the body did not return' on the loop's normal-exit path, so post-loop statements are not silently disabled (a return inside the loop must still allow the fall-through code to run). Add regression coverage for both the invariant-abstracted loop and KeY's binary search. Derive the SMT array type from the element type in arraySmtType so that new-array expressions on detached fragments (e.g. normalized new int[a.length]) resolve even when calculateResolvedType is unavailable. Keep declarator/plain-assign initializer expressions attached to their compilation unit instead of cloning, preserving symbol resolution. Add a scratch harness (KeyReverseScratchTest) exercising the original and normalized array-creation paths.
Prioritized (soundness -> completeness -> diagnostics -> design-level) work plan for the known Java/JML divergences of the VCG, with code locations, steps, tests, effort, and open decisions per item.
The six runtime-exception checks (checkNull, checkDivision, checkIndex,
checkCast, checkNegativeArraySize, checkStringIndex) are now ON by default
in VcgOptions, so a PROVEN method is also NPE/CCE/index/division-free
(KeY-style). checkOverflow stays opt-in: BOUNDED bit-vectors already wrap
exactly like Java, so the check only flags wraparounds (and is vacuous in
UNBOUNDED).
CLI: --checks=all|none|default selects the whole set; the missing
--check-overflow flag is added; individual --check-* flags enable a check
on top of the chosen policy. The LSP inherits the new policy via the
VcgOptions defaults.
Modeling fixes that the default-on checks exposed:
- new T(...) results are axiomatized non-null (Java new never returns
null), so a default-on nullcheck on a new T().m() receiver proves;
- the first store to an array-typed receiver field (h.vals[i] = v)
initializes the flat slot from the field-selector read instead of a
fresh unconstrained array, so a default-on index check discharges
against a requires h.vals.length >= n;
- stringLength is declared lazily at first use (string-free queries no
longer carry the declaration).
Tests: testRuntimeChecksOnByDefault replaces testRuntimeChecksOffByDefault;
testRuntimeChecksOffWithNonePolicy keeps the opt-out silent; arrayStoreInLoop
requires strengthened to a.length >= 3. Seven golden snapshots regenerated
with only the new default-on obligations plus obligation-id renumbering.
new T(...) is now a contract call site when the constructor is in the verified unit and carries a JML contract: - the caller must establish the disjunction of the per-case requires (a falsifiable "precondition of constructor" obligation at the site); - each case's ensures is assumed guarded by its own pre-state requires (same discipline as contractCall); - the constructed class's invariant is assumed (invariant_for(the fresh object) -- a valid constructor contract establishes it, exactly as checkPostcondition folds it into the constructor's own verification); - assignable: fresh-object state is already unconstrained, so only named aliasable caller-visible locations are refreshed; no assignable or \everything (the JML default) refreshes the reachable frame. The callee view binds this to the fresh object and exposes every non-static scalar/object field of the constructed class as select(field-map, fresh), declaring the maps eagerly so the clause reads and the caller's post-construction reads share the same select terms regardless of translation order. Supporting fix: locals now carry their resolved declared type on the SSA term (flatWrite), so receiver-bound views can expose the fields of a *local* receiver (c.get() reads count through the same identity-keyed field map the construction established); previously such reads fell back to an uninterpreted constant. Deviation from the plan sketch (documented in vcg-semantics-plan.md): unresolvable constructors (library classes like new Object() / new ArrayList<>(), implicit default constructors) are not rejected -- they keep the fresh-object model with unconstrained fields, a sound over-approximation that mirrors the P1.3 contractless-with-body carve-out (reads on such objects stay guarded by P1.3). Tests: useCountedCtor (both modes; construction then c.get() through the same field map), ctorRequiresViolated (falsifiable constructor precondition at the creation site), ctorInvariantUsable (body assert discharges only through the assumed invariant); golden guardrails useCountedCtor__U_CONTRACT and ctorInvariantUsable__U; 34 existing goldens regenerated (only the new sort_counted type declarations).
…state A constant folder (JLS-style constant expressions, fold-through of earlier-declared constants in textual declaration order, JLS 8.3.3) pins the slot where every legal execution reaches method entry with that value: - static final constants bind for every callable (also folds constants into reads of the enclosing class); - constant instance initializers bind when verifying a constructor (JLS 12.5: initializer-before-body - an empty default ctor now establishes its fields and the class invariant); - final instance constants bind for instance methods (no constructor can rewrite a final-with-initializer field). Not bound (documented, sound): mutable static fields, mutable instance fields in methods (a competing constructor may overwrite them), forward references, method-call/cast/array and reference-typed initializers. Folder details: literal parsing follows JLS 3.10.1 (decimal vs hex/octal/binary two's-complement typing, int vs long classification), unary + - ! ~, binary + - * / % << >> & | ^, comparisons and && || == !=. Every intermediate result must fit the promoted signed range, so folded values never wrap and agree with both BOUNDED and UNBOUNDED arithmetic; `1 << 31`, `>>>` and x/0 stay unconstrained. Emission is mode-aware (BV width vs Int). Tests: p22StaticFinalBlocks / p22ConstantShapes prove in U+B (were unprovable); p22NonConstInit and p22ForwardRefInstance stay falsifiable; the ConstantInitCtor fixture shows the constructor (int n) ctor entry binding, the final instance constant read in a method, and the mutable-instance-in-method soundness boundary (countAfterAnyCtor stays falsifiable). Golden guardrails: new p22StaticFinalBlocks__U snapshot; 36 existing goldens regenerated with only the new type constant, the new field slots/pins and the two new instance slots that the everything-assignable contract frame havocs.
…g it `new int[n][m]` used to be encoded as a 1-D array of the element type: only the first dimension was read off the levels and the element sort silently collapsed. Generation now rejects multi-dimensional array creation (any level count > 1) up front with a structured UnsupportedFeatureException that names the construct and carries the node's source range. Introduces io.github.jmltoolkit.vcg.UnsupportedFeatureException (extends UnsupportedOperationException) as the single diagnostic type for constructs the VCG cannot model; P3.2 routes the remaining unsupported constructs through it. Reflective array construction (java.lang.reflect.Array.newInstance) needs no extra guard: it resolves to an external call without contract or body and is already rejected by P1.3, or explicitly over-approximated under --allow-unrefined-calls. Tests: testMultiDimArrayGenerationRejected covers multiDim (new int[n][n]) and the jagged multiDimJagged (new int[n][]), asserting the message and the source range. Existing goldens unchanged - no fixture or golden case uses multi-dimensional arrays.
A pre-query validation pass (validateSupported, run at verify() entry before
any query work) aborts generation on the first construct the VCG cannot model
with UnsupportedFeatureException("unsupported: <construct> at line N")
carrying the node's source range. Covered: switch expressions (only switch
statements are modeled), lambdas, method references, anonymous classes, Java
assert statements (the supported form is a JML //@ assert), JML keywords
outside the supported set (\\fresh, \\reach, \\TYPE and friends would
otherwise be silently mis-modeled or fail with an unrelated resolver error),
and enum types (verifying an enum member is rejected up front). The supported
keyword whitelist: \\result, \\old, \\invariant_for, \\static_invariant_for,
\\everything, \\nothing; quantifier/label binders (\\forall, \\exists,
\\sum, \\lbl, ...) are separate AST node kinds and are unaffected.
UnsupportedFeatureException (introduced in P3.1) is now the single diagnostic
type for unsupported constructs: the Normalizer's generic statement /
expression-statement / assignment-target throws use it too. It extends
UnsupportedOperationException, so existing assertThrows(UnsupportedOperation
Exception) guards stay green.
Tests: testUnsupportedConstructsRejected (lambda, method reference, anonymous
class, Java assert, \\fresh, \\reach), testSwitchExpressionRejected (a switch
expression only parses at a JAVA_12+ language level, so the probe parses a
JAVA_17 snippet; the shared fixture file stays at the default JAVA_11 level),
testEnumVerificationRejected (the Color enum appended to VcgExamples.java).
The new top-level Color type adds the sort_color type constant and subtype
edge to every golden query - a purely additive change, confirmed by diffing
the 37 regenerated goldens.
Arrays now behave like ordinary references: nullable by default, with the JML modifiers steering nullability exactly as for objects. `non_null` is the opt-out for a location; array elements are non-null by default on every store; `nonnullelements` states that default explicitly. Encoding: - per-sort null-array constant `$null_array_<sort>` (declared lazily); `arr == null` is a real `(= arr $null_array_<sort>)` comparison instead of the constant-false folding - deref nullchecks on `a[i]`, `a.length` and element stores; `new T[n]` results are asserted non-null; `non_null` locations fold the comparison and skip deref checks, with entry assumptions (params = implicit `requires`, fields = type invariant asserted at entry but not in constructors, locals = store obligations in flatWrite) - object-array element stores obligate `e != null`; element reads stay unconstrained (folding would break fresh-array elements; documented deviation - the grammar has no nullable-elements keyword either) Supporting model fixes: reference-typed array element sorts print as `U` (the declared reference sort, not the never-declared `Object` placeholder - smt golden updated accordingly), per-sort `bv$length_<tag>` / `int$length_<tag>` length functions for non-int arrays (SMT-LIB forbids overloading), alias frames restricted to same-sort arrays (Java forbids mixed-sort identity), and a per-verification anonymous-array counter so identical inputs yield identical queries. Tests: 7 proven + 2 falsifiable array-nullability fixtures (incl. a `non_null` array field holder, `nullableArrayBranch`, element-store obligations), 6 new golden snapshots; VcgSemanticsTest grows 260 -> 277 and stays green. Goldens regenerated and diffed (mechanical: real `a != null` plus `$null_array_*` declarations). Spotless + whole-project compile green.
Every call to a non-helper instance method is a visible state: the receiver's class invariants are checked as an obligation before the call and re-assumed as an assumption afterwards (the callee's own exit discipline restores them, mirroring checkPostcondition). this-receivers fold the enclosing type's statically-visible invariants; explicit receivers o.m(...) fold the receiver's set, both through the existing InvariantFold/invariantForTerm machinery. Helper callees, static callees, and classes without in-CU invariants add nothing. The pre-call check and the contract view share a single receiver evaluation via needsEarlyReceiver; the same discipline applies around inlined calls. The visible-state pre-call check is the missing link between the long-standing entry assumption (assumeClassInvariant) and exit obligation (checkPostcondition): breaking an invariant mid-method and restoring it only after a call is now falsifiable, and after a call whose ensures says nothing about the havoced field the caller still reasons about the invariant. Tests: five new fixtures (callWithInvariantHeld proven, breakInvariantBeforeCall falsifiable - the guardrail, relyOnInvariantAfterCall proven on contract AND inline strategies with a load-bearing post-call assume, helperCallExempt proven, and the explicit-receiver pair receiverInvariantHeld/receiverInvariantBroken). VcgSemanticsTest grows 277 to 282 green cases (KeY binary-search stays green); new golden snapshots for all of them; among existing goldens only useCountedCtor changes semantically (pre-check becomes v3, the post-call assume is added, the exit postcondition renumbers to v4) and the rest gain only the sort_invariantreceiver declaration line.
Closes the last Java/JML semantic gap in the VCG per the plan: under the existing --check-string-index option, equals, charAt/codePointAt, concat and the int(char) overload of indexOf become reads of a per-position character-code model (steq/strval/strcat/strindex) instead of opaque unrefined library calls, so String-heavy methods verify. - equals is extensional equality cut by runtime length (both directions): s.equals(s) is provable, s.equals(null) is false (the argument stays a null-guarded reference) - charAt/codePointAt read (strval s i) under the stringIndexChecker bounds obligation; statement-position reads carry the real path guard - concat yields a non-null result whose length sums the parts and whose content prefixes the first argument, so s.concat(t).length() discharges its deref nullcheck - indexOf returns the first position of the character or -1 (completeness/found/absent/minimality axioms), with a char search argument upcast to the mode's int sort in BOUNDED mode Each operation declares its function and length-bounded axioms once, lazily, per operation behind the feature flag, so a charAt-only query never pays for the steq/strcat/strindex axioms. The quantified axioms carry explicit :pattern annotations so Z3's E-matching, not MBQI, drives them; absence and minimality are flattened to a single universal level over a strindex+strval multi-pattern, keeping satisfiability-only searches instant (spiked: without this, MBQI churned near-trivial checks to the 60s watchdog). Five new semantics fixtures (282 -> 287 green): stringSelfEquals, stringCharAtIndexOf, stringConcatLen (U+B), stringIndexOfAbsent proven; stringCharAtUnknown falsifiable. Six new goldens. Documented limits: BOUNDED-mode char reads compare 16-bit extracts of the 32-bit codepoint model, and a falsifiable claim cannot share a query carrying the indexOf axioms.
The 'Install Z3 SMT solver' step used apt-get, which only exists on Ubuntu, killing the macOS and Windows jobs of the test matrix before any test ran. Install Z3 with the cross-platform KeYProject/setup-smt action (pinned to v0.3.1 by commit SHA), which downloads the official z3 binary for the runner's OS and adds it to PATH; cvc5 is disabled as it is not used. Make the solver itself Windows-portable so the solver-backed tests in :tools:smt, :tools:vcg, :tools:lsp and :tools:wd actually run and verify on the Windows job instead of being silently skipped: - Z3.kt: probe for z3 via 'where z3' on Windows instead of relying on 'sh -c "which z3"' - Solver: start 'z3 -smt2 -in' directly; ProcessBuilder resolves it on PATH on every OS (z3.exe on Windows), no shell wrapper needed - SolverTest: the watchdog stubs used 'sleep 30', which does not exist on Windows cmd; use 'ping -n 31 127.0.0.1' there Also force LF for the VCG golden *.smt2 snapshots in .gitattributes so they stay byte-identical to the LF queries the generator emits on Windows (same fix as the existing *.symbols rule).
- SolverTest: use a silent long-running stub on Windows (`cmd /c "timeout /t 30 /nobreak >nul"`). `ping` prints headers/replies to stdout, which the Solver's incremental SMT parser chokes on before the watchdog kills the process — the `timeoutKillsExactlyAtTheDeadline` / `cancellationDestroysTheSolverProcess` tests then fail on Windows with IllegalStateException. - SmtQuery: serialize with a bare '\n' instead of PrintWriter.println (which emits the platform line separator). The generated query was CRLF on Windows while the committed .smt2 goldens are LF, so VcgGoldenQueriesTest drifted on Windows. Newlines are not semantic to SMT-LIB, so this only makes toString()/appendTo() byte-stable.
timeout.exe refuses to run when stdin is redirected, so the previous stub (cmd /c "timeout /t 30 /nobreak >nul") exited immediately and SolverTest.timeoutKillsExactlyAtTheDeadline returned before the 500 ms deadline on Windows. Use cmd /c "ping -n 31 127.0.0.1 >nul" instead: it stays alive ~30 s, writes nothing to stdout, and never reads stdin.
…3 extension) Extend the --check-string-index abstract-string model with the remaining common String reads so String-heavy methods verify: - substring(i)/substring(i,j) ≈ strsub/strsub2: non-null slice whose runtime length is the slice width and whose content is the receiver's shifted by the start index (position-wise, like strcat); the call-site bounds obligations come from the existing stringIndexChecker. - startsWith(String) ≈ strpre: the prefix relation in both directions — pre ⇒ len(p) <= len(s) and position-wise content agreement below len(p), and the converse proves literal-prefix claims from the literal's bound content. The argument is null-checked (s.startsWith(null) throws NPE). - replace(char,char) ≈ strrep: non-null length-preserving result whose content maps the replaced character to the replacement (ite per position). Dispatch restructured from a single-argument gate to per-op arity and resolved-parameter checking (replace is gated to the (char,char) overload; indexOf(String) stays unrefined/rejected by P1.3 — substring search over the char view is the remaining documented divergence, pinned by the stringIndexOfString fixture). String literals now bind per-position content (strval(strlit,i) = utf16-code(value[i])) under the feature. Z3 performance rule carried over from the indexOf spike: every content axiom is flattened to a single universal level with a pattern on the content-application term. A nested index quantifier whose index is the arithmetic (+ s s) cannot be E-matched, so Z3 falls back to MBQI and even a satisfiable bounds obligation (substringLen's string-index check alone) churned to the 60 s watchdog; the flattened pattern keeps the axiom inert until a ground content read appears. Tests: substringLen/substringLen2, literalStartsWith(+Broken falsifiable), startsWithLengthBound, replaceLen, replaceContentAt0, stringIndexOfString (rejected); 4 new U_STR goldens; :tools:vcg:test fully green (--rerun-tasks), spotlessCheck clean.
wadoon
marked this pull request as ready for review
October 31, 2026 23:20
wadoon
marked this pull request as draft
October 31, 2026 23:34
wadoon
marked this pull request as ready for review
October 31, 2026 23:39
Contributor
Author
|
All CI green on the new head The last commit extends the P4.3 abstract-string model (
Encoding detail for reviewers: every content axiom is flattened to a single universal level with a pattern on the content-application term (e.g. Plan doc ( |
indexOf(String) is now modeled: (seq.indexof (strContent s) (strContent t) 0) in UNBOUNDED mode, so the wrong-position claim (stringIndexOfWrong) is falsifiable and answers instantly (no quantified string axiom in the query). BOUNDED mode keeps the quantified axiom model (no native sequence sort over bit-vectors); its proven indexOf(String) directions stay in the suite, its falsifiable one is dropped (MBQI churn, documented). UNBOUNDED mode compiles the modeled String operations to direct sequence terms (length = seq.len, charAt = seq.nth, equals = content equality, concat/substring = fresh non-null consts bound by ground seq.++/seq.extract, startsWith = seq.prefixof), keeps quantified axioms only for strindex (char search; the native seq.indexof cannot derive its content lemmas) and strrep (replace(char,char); no seq.replace_all for (Seq Int)), and binds string literal content natively (seq.empty/seq.unit chain). tools:smt gains the Seq sort. 5 new U_STR goldens plus regenerated goldens; non-string U goldens change only cosmetically (the eager receiver path blank-declares strContent where base declared stringLength).
Mirror the real KeY teaching material (key.ui/examples/firstTouch) as fixtures in VcgExamples.java and wire them into the semantics + golden suites: - ReverseArray.reverse/reverse2: quantified \old content invariants — generation-only (a list of exact obligations is asserted; the content-level \old reasoning exceeds the solver budget, so the queries are pinned by new golden snapshots instead of a Z3 verdict). - BinarySearch.search: proven through the loop invariant (U_INV), with the KeY-assumed non-null parameter made explicit in the requires. - Java5.For.sum: the contract uses the \sum generalized quantifier. The VCG now REJECTS non-\forall/\exists binders loudly (P3.2 fail-fast pass) instead of silently encoding \sum as a universal quantifier, which the real example exposed. - SITA3.commonEntry/swap: proven through their loop invariants / old-based ensures (U and B for swap), again with explicit non-null requires. Golden snapshots: new cases for reverse/reverse2/search/commonEntry/swap; every existing snapshot gains the 4 new type sorts + Object-subtype edges (add-only churn, regenerated with UPDATE_GOLDEN=1).
…ects (P5.1/P5.2) Test coverage for every arithmetic/comparison/boolean operator through the real translators in both modes (fold* + arithOps) exposed four encoder defects, now fixed: - '>>>' emitted bvshr (not an SMT-LIB function); now bvlshr — the logical shift — so -8 >>> 2 proves 1073741822, not -2 - shift distance not masked (JLS 15.19): translator binary() now applies (bvand d ((_ int2bv w) (w-1))); shiftDistanceMasking proves x << 33 == x << 1 - xor unconditionally Bool-xor built ill-sorted (xor bv bv); polymorphic SmtTermFactory.xor: Bool -> xor, BitVec -> bvxor - makeLong used the raw literal string (L suffix): NumberFormatException on any long >= 2^31; shared JLS 3.10.1 longLiteralValue() parses radix/suffix Bit-width ops have no encoding on mathematical integers: UNBOUNDED mode now rejects << >> >>> & | ^ ~ loudly in both the runtime path (atom()) and the expression path (ExprTranslator: contract clauses + JML asserts), instead of a bare sort mismatch or a silently ill-sorted xor term. Loop contracts: \returns clauses are enforced at an in-loop return (LoopFrame.returns + execReturn obligation); a while(true) loop that leaves only via break keeps the post-loop statements enabled (loopExitsOnlyViaBreak). Rejections: block contracts (attached to BlockStmt) were silently dropped — now rejected with a source-anchored diagnostic; labeled statements get a dedicated message instead of the raw class-name fallback. Tests: 16 new fixtures (foldIntRadixes/ArithOps/BoolOps/UnaryOps/ShiftOps/ DivZero/FieldSorts, arithOps u+b, bitwiseOps BOUNDED-only, shiftOps, unsignedShiftNegative, shiftDistanceMasking, loopContractReturns[Wrong], loopExitsOnlyViaBreak, stringCodePointAt, invariantForInBody); parameterized proven/falsifiable/unsupported tables extended; ExprTranslatorTest goldens updated (masked shifts, bvlshr, bvxor, 1L -> 1); 60 goldens regenerated (add-only: 91 lines of AR_* entry-state declares each); whole-project suite (860 vcg tests) + smt/wd modules + spotless + checkstyle green.
The atom() UnaryExpr bitwise-complement rejection was unreachable: every fixture with a body-level '~' also contained a binary bitwise op (& | ^) that threw first. bitCompOnly (~ in a body statement only) now exercises it; the ExprTranslatorTest case for '~x' on Int sorts is tightened to assert the structured message (it previously only checked RuntimeException).
…h examples Spawns the real CLI (java -cp <test classpath> …MainKt vcg) as a subprocess on the KeY firstTouch material adapted for the VCG (05-ReverseArray, 06-BinarySearch, 08-Java5, 10-SITA), with a hard-kill watchdog so a stuck solver cannot hang the suite. Verdict signals are gated on Z3.z3Installed(), matching the in-process tests. Assertions avoid line-order dependence (conditions print in completion order): - 06-BinarySearch: all 20 conditions ok, exit 0. - 10-SITA: commonEntry/swap proven through their invariants; the rearranging driver is excluded from the report (its contract is weaker than the default runtime-check policy — the in-process suite also only asserts commonEntry/swap). - 08-Java5: the \sum binder is rejected loudly with the structured UnsupportedFeatureException and a non-zero exit, not silently mis-encoded. - 05-ReverseArray: UNBOUNDED+invariant (the U_INV config) — generation succeeds, both methods are reported (31 conditions total, generation-pinned by the goldens), reverse() itself never yields a counterexample; its quantified \old queries exceed the solver budget and are reported UNKNOWN (the in-process suite treats this fixture as generation-only and asserts no verdicts).
Bounded single-variable \sum ranges with a direct array-read body are translated to a recursive `jmlSum` function; other shapes abort with a structured UnsupportedFeatureException. Array-length terms of constant symbols in BOUNDED \sum queries fold into shared implicit `$len_*` constants (explicit declarations stall Z3's rec-fun instantiation on the invariant/variant checks), and every solver-answer walker skips the interleaved "unknown constant" warnings. \index and \strictly_nothing are supported; the KeyFor (08-Java5) fixture and the SITA3 search/swap examples verify in both modes.
08-Java5's \sum contract now verifies in the real CLI subprocess in both bounded and --unbounded mode (11 conditions, 0 failing — the fixture gains the explicit `requires a != null` the VCG needs) instead of being rejected. New shell-test fixtures cover BinarySearch, the \sum example, SITA (with the weak rearrange contract excluded) and ReverseArray's honest UNKNOWN/FAIL report; shelltester gains a `sortOutput` mode that compares sorted normalized lines so solver-completion order cannot fail the tests.
…(P3.2) \forall/\exists/\sum with an element or range domain (e.g. '(\forall int e : a; e > 0)', stored on JmlQuantifiedVariable per the merged core #83) have no VCG desugaring: the old path bound the variable by its declared type and translated the body, silently *dropping the domain* — '(forall ((e Int)) (> e 0))' — an unsound encoding (the requires collapses to false assumptions). checkSupported now aborts such quantifiers with a structured UnsupportedFeatureException naming the binding form, matching the existing loud-rejection policy. VcgSemanticsTest: two new unsupportedConstructs rows (quantIterableDomain, sumIterableDomain); suite 333->335, all green (vcg 873, cli 4).
The pinned setup-smt action installed Z3 4.13.3 on CI while local development uses 4.16.0. Z3 < 4.15 cannot terminate on quantified bit-vector obligations such as 06-BinarySearch's postcondition (the \exists over array indices under the nested sortedness \forall): the negated obligation runs until the solver watchdog cancels it, mapping the two postcondition conditions to UNKNOWN (`????`) and failing the new binarySearchIsVerifiedThroughItsLoopInvariant e2e test and the search.txt shell fixture. Verified: identical failure on the pre-merge tip (the merge with main and the element-domain guard are not involved), reproducible locally with 4.13.3; 4.15.4 decides the query instantly and the full :tools:smt/:tools:vcg/:tools:cli suites plus all shell tests pass. 4.15.4 is the newest Z3 the pinned action installs on every matrix OS (linux glibc 2.39, macos 13.7.6, windows): 4.16.0's macos asset (osx-15.7.3) needs a newer action, so 4.15.4 is the max compatible pin.
The Windows start script must use the %APP_HOME%\\lib\\* classpath wildcard:
cmd.exe expands %APP_HOME% when 'set CLASSPATH=' executes, so an explicit jar
list becomes an absolute-path classpath of >8k chars for 115 jars and blows
the 8191-char line limit on every continuation line ('The input line is too
long' — a chunked CLASSPATH variant fails exactly this way).
Java expands that wildcard in directory-enumeration order (first jar to offer
a class wins), so the distribution must not contain two com.github.javaparser
implementations. The LSP's key.core transitively pulls in
org.key-project.proofjava:javaparser-core(-serialization/symbol-solver-core)
3.28.0-K13.6, whose ParserConfiguration lacks setProcessJml; on Windows it
sorts before the fork core and 'jmltk vcg' died with NoSuchMethodError (Linux
start scripts list jars in dependency order and were unaffected; main's
VcgCommand predates the setProcessJml call, which is why main's Windows shell
tests were green).
Exclude the proofjava group from the :tools:lsp dependency so the
distribution ships exactly the fork core. Verified: proofjava-first classpath
reproduces the CI stack trace; the deduplicated lib\* wildcard proves all 20
binarySearch conditions; shell tests (6/6), :tools:cli:test and
:tools:lsp:test pass; spotless clean. Changelog updated.
The sita.txt shell fixture passes the --vcg-exclude glob inside single quotes, which group on POSIX sh but are literal characters on cmd.exe: on Windows the CLI received the pattern 'KeySITA3#rearrange()*' including the quote characters, matched nothing, and the weak rearrange() contract was reported (33 conditions, 10 failing) instead of being excluded (20, 0 failing). Double quotes group on both shells and cmd.exe does not glob, so the literal pattern reaches the CLI unchanged on every OS.
This branch has not been deployed
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
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.
Known semantic divergences (Java/JML)
Current implementation limits — where the encoded semantics differ from Java/JML. The soundness pass (
doc/vcg-semantics-plan.md) has resolved the original items (each bullet marks its plan phase); the mode-specific string-model divergences below remain.Multiple spec cases keep disjunctive semantics (P1.1) — JML
behaviorcases are unrolled but never merged: at a call site the caller must establish the disjunction of the per-caserequires, may assume each case'sensuresguarded by its ownrequires, and the assignable clause is the union across cases.\static_invariant_forfolds onlystaticinvariant clauses, so instance invariants (which readthis) no longer leak into static methods.Binary numeric promotion in BOUNDED mode (P1.2) —
byte/short/charoperands are widened toint(longwins;charzero-extends) before every binary and unary operation (JLS 5.6), shifts promote the left operand, the Java conversions are applied at stores and casts ((byte)300 == 44,b += 300truncates to54, JLS 5.1.2/5.1.3), conditional-expression branches are promoted (JLS 15.25), and overflow / div-by-zero checks test the promoted width.Unresolvable callees are rejected by default (P1.3) — a call whose callee has no JML contract and no body (unresolvable, or a bodyless native/abstract method without a contract) raises a loud diagnostic instead of silently returning an unconstrained result while assuming the call touched nothing.
--allow-unrefined-calls/allowUnrefinedCallsopts back into a sound over-approximation: the caller-visible frame (this.*, arrays, field maps) is havoced and the result stays unconstrained.Runtime exceptions are checked by default (P3.3) — the six runtime-exception checks (
checkNull,checkDivision,checkIndex,checkCast,checkNegativeArraySize,checkStringIndex) are ON by default, so a PROVEN method is also NPE/CCE/index/division-free (KeY-style); the CLI gained--checks=all|none|defaultand the missing--check-overflowflag (overflow stays opt-in: BOUNDED wrap-around already matches Java, the check only flags wraparounds). Supporting model fixes:new T(...)results are axiomatized non-null, a first store to an array-typed receiver field ties the flat slot to the field-selector read, andString.length()is a lazily-declared model read.Constructor contracts are applied at creation sites (P2.1) —
new T(...)is now a contract call site when the constructor is in the verified unit and carries a JML contract: the caller must establish the disjunction of the per-caserequires(a falsifiable "precondition of constructor" obligation), may assume each case'sensuresguarded by its own pre-staterequires, and may assume the constructed class's invariant; assignable is scoped likecontractCall(the fresh object's own state is already unconstrained, only named aliasable caller-visible locations are refreshed; no assignable /\everythingrefreshes the reachable frame). Supporting fixes: locals carry their resolved declared type on the SSA term, so contract calls on local receivers (c.get()) read through the same identity-keyed field map the construction established. Uncontracted constructors (library classes, implicit default constructors, contractless bodies) keep the fresh-object-with-unconstrained-fields model — a sound over-approximation, mirroring the P1.3 contractless-with-body carve-out (reads on such objects are still guarded by P1.3).Constant field /
static finalinitializers are folded into the entry state (P2.2, partial) — a constant folder (literals in decimal/hex/octal/binary,long,char,boolean, unary+ - ! ~,+ - * / % << >> & | ^, comparisons,&& || == !=, plus references into earlier-declared constants, JLS 8.3.3 textual order) pins the slot where every legal execution reaches entry with that value:static finalconstants for every callable (this also folds constants into reads), constant instance initializers when verifying constructors (JLS 12.5, initializer-before-body — an empty default ctor now establishes its fields and the class invariant), andfinalinstance constants in instance methods. Intermediate results are checked against the signed range of the promoted type, so folded values never wrap and agree with both arithmetic modes (1 << 31and>>>stay unconstrained). Not folded (documented, sound): mutable static fields, mutable instance fields in methods (a competing constructor may overwrite them), forward references, method-call/cast/array initializers, reference-typed initializers — those slots stay unconstrained as before.Multi-dimensional array creation is rejected (P3.1) —
new int[n][m]used to be silently encoded as a 1-D array of the base type (only the first dimension was bound); generation now refuses every array with more than one level (new int[n][n], jaggednew int[n][]) with anUnsupportedFeatureExceptionnaming the construct at its source range. Reflective array construction (Array.newInstance) never needed an extra guard: it resolves to an external call without contract/body and is rejected by P1.3 (or over-approximated under--allow-unrefined-calls).Unsupported constructs fail with structured diagnostics (P3.2) — a pre-query validation pass rejects what the VCG cannot model with
UnsupportedFeatureException("unsupported: <construct> at line N")carrying the node's sourceRange: switch expressions (switch statements are modeled), lambdas, method references, anonymous classes, Javaassertstatements (the JML//@ assertform is supported), JML keywords outside the supported set (\fresh,\reach,\TYPE, …; whitelisted are\result,\old,\invariant_for,\static_invariant_for,\everything,\nothing, plus the quantifier/label binder node kinds), and enum types (an ordinal/constant model would be required). TheNormalizerthrows the same type for generic unsupported statements.Arrays are ordinary (nullable-by-default) references (P4.2) —
arr == nullis a real comparison against a per-sort null-array constant$null_array_<sort>, dereferencing a possibly-null array (a[i],a.length, element stores) raises a nullcheck obligation,new T[n]results are asserted non-null, and JML modifiers steer reference nullability exactly as for objects:non_nulllocations (params = implicit requires, fields = type invariant asserted at entry, locals = store obligations) fold== null/!= nulland skip deref nullchecks. Elements are non-null by default: every element store obligese != null, andnonnullelementsis the explicit statement of that default (the grammar has nonullable-elements keyword, so a nullable-element store cannot be expressed — documented deviation; element reads stay unconstrained, since folding them would break fresh-array elements — documented deviation). Supporting model fixes: reference-typed array element sorts now print asU(the declared reference sort, not the never-declaredObjectplaceholder), array lengths use per-sortbv$length_<tag>/int$length_<tag>functions because SMT-LIB forbids overloading, alias frames only apply to same-sort arrays (Java forbids mixed-sort identity), and thenon_null-declared array field case is covered (this.data != $null_array_...assumed at method entry).Call sites are visible states for class invariants (P4.1) — every call to a non-helper instance method checks the receiver's class invariants before the call (a
class invariant at call to …obligation) and re-assumes them after it (the callee's own exit discipline restored them):this-receivers fold\invariant_for(this), explicit receiverso.m(...)fold\invariant_for(o)— the receiver's statically-visible set from the existing\invariant_formachinery.\helpercallees are exempt on both sides (helpers may break and need not preserve the invariants), static callees and classes without in-CU invariants add nothing, the pre-call check and the contract view share one receiver evaluation, and constructor sites keep the P2.1 constructed-invariant assumption (newis not a visible state for the caller'sthis). The post-call assume is load-bearing: after an assignable havoc whoseensuressays nothing about the field, the caller still proves invariant-constrained asserts/exit obligations from the re-assumed invariant.Common
Stringoperations become abstract-string model reads (P4.3, opt-in via--check-string-index) —equals,charAt/codePointAt,concat,length(), bothindexOfoverloads,substring(both overloads),startsWith(String)andreplace(char,char)translate to reads of a character-code model over the reference universe. In UNBOUNDED mode the model is native:strContent : U -> (Seq Int)is the single content view and the operations compile to direct sequence-theory terms —length()=(seq.len (strContent s)),charAt=(seq.nth …),equals= content-sequence equality,concat/substringresults are fresh non-null references bound by a ground(seq.++ …)/(seq.extract …)equality,startsWith=(seq.prefixof …),indexOf(String)=(seq.indexof … 0)— and string literals bind their whole content natively (seq.empty/seq.unitchain). BOUNDED mode keeps the quantified axiom model (stringLength/strval/steq/strcat/strindex/strfind/strsub/strsub2/strpre/strrep): the proven directions are the same, but the mode has no native sequence sort. Each operation declares its function and length-bounded axioms once, lazily; every quantified axiom carries an explicit:pattern(Z3's E-matching, not MBQI) and every content axiom is flattened to a single universal level over a pattern on the content-application term — so satisfiability-only searches stay instant.indexOf(char)= first position or-1(completeness / found / absent / minimality axioms; the only operation whose content lemmas the native theory cannot derive, sostrindexkeeps its axioms in U mode too);indexOf(String)= substring search whose found/empty/absent consequences are provable (k == indexOf(t) ∧ k >= 0⇒k + t.length() <= s.length(),indexOf("") == 0, a found result pins the matched suffix, a-1rules out any in-range suffix-prefix claim);replace(char,char)keeps the EUFstrrep(nativeseq.replace_allhas no(Seq Int)instance). Documented limits: BOUNDED-mode char-level reads compare 16-bit extracts of the 32-bit codepoint model (char-equality claims don't follow from codepoint inequalities), and a falsifiable claim cannot ride a query that carries thestrindex/strrepaxioms (MBQI mirroring defeats instant SAT answers).The JML
\sumgeneralized quantifier is modeled (P6.1) —\sum int j; lo <= j && j < hi; a[j]with a bounded integer range and a direct array-read body compiles to a single lazily-declared recursive SMT function(define-fun-rec jmlSum a lo hi …)that unfolds along the index range (hi <= lo→0, elsejmlSum(a, lo, hi − 1) + a[hi − 1]), so KeY's firstTouch 08-Java5 for-each sum (maintaining s == \sum int j; 0 <= j && j < \index; a[j]andensures \result == \sum … a.length) verifies in BOUNDED and UNBOUNDED mode alike. Every other shape is rejected with a structuredUnsupportedFeatureExceptionnaming the binder (no array-read term; no upper bound; extra range conjuncts; non-monotone bodies —KeySumBadShapes). Supporting mechanics: the KeY loop-position pseudo-variable\indexbinds the type-tagged loop-counter register$idxNin loop contracts,\strictly_nothingjoins the assignable whitelist, and BOUNDED\sumqueries fold length terms of constant array symbols (bv$length sym→ a shared implicit$len_<sym>constant plus one ground>= 0assert). The fold is what makes such queries terminate: under thejmlSumrecurrence axioms Z3's recursive-function instantiation stalls against an explicitlydeclare-consted length symbol (full timeout on KeyFor's invariant/variant checks) but answersunsatinstantly with the same symbol used implicitly. Solver-answer walkers (VcgResult.runCheckand the test helpers) skip the interleaved(error "…unknown constant…")notices before every verdict; non-\sumBOUNDED queries and all UNBOUNDED queries stay byte-identical. All four KeY firstTouch teaching examples run the VCG end-to-end: 05-ReverseArray keeps honest UNKNOWN/FAIL verdicts, 06-BinarySearch and 10-SITA (commonEntry,swap) prove through their loop invariants, and 08-Java5 proves its\sumcontract.Remaining divergences:
indexOf(String)wrong-position falsifiability is UNBOUNDED-only — the minimality direction (stringIndexOfWrong: the searched needle occurs at 0, the claim says 1) is satisfiable and answers instantly in UNBOUNDED mode, where the query is axiom-free by construction (nativeseq.indexof; no quantified string axiom to satisfy while building the model). BOUNDED mode keeps the quantifiedstrfind/strsub/strpresearch ladder, whose MBQI mirror makes the falsifiable direction churn to the watchdog — the proven directions are unaffected and B-mode runs remain in the suite for them, but the wrong-position claim is not part of the B-mode suite. Everything else listed in the P4.3 bullet is a model read (native in U, axioms in B) under--check-string-index.Design direction (recorded, not implemented): boxing the compared type to
(Seq (Seq Int))(boxIntVal) would let a string-valued substring view live inside the native sequence theory, the follow-up path if case-sensitive-suffix/regionMatches-style reasoning is ever needed.Testing
VcgSemanticsTest(335 cases, incl. P1.1 disjunctive spec cases, P1.2 promotion fixtures, P1.3 unrefined-call rejection/havoc, P2.1 creation-site constructor contracts, P2.2 constant field/static-final initializers, P3.3 default-on runtime-check policy, P3.1 multi-dim rejection, P3.2 structured unsupported-construct diagnostics, P4.2 array-nullability fixtures — 8 proven incl. anon_nullarray field, 2 falsifiable: dereferencing a possibly-null array and storingnullinto an object array — P4.1 visible-state invariant fixtures:callWithInvariantHeldproven,breakInvariantBeforeCallfalsifiable (the guardrail),relyOnInvariantAfterCallproven on contract and inline strategies (post-call assume load-bearing),helperCallExemptproven,receiverInvariantHeld/receiverInvariantBroken(explicit-receiver variants) — and P4.3 string-model fixtures:stringSelfEqualsproven,stringCharAtIndexOfproven (anindexOf >= 0result pins a content position),stringConcatLenproven in both modes,stringIndexOfAbsentproven (a reported-1discharges a groundedcharAtcontent read),stringCharAtUnknownfalsifiable (unguarded first-position claim),substringLen/substringLen2,literalStartsWithandliteralStartsWithBroken(provable / falsifiable literal-prefix claims),startsWithLengthBound,replaceLen,replaceContentAt0,stringIndexOfLen/stringIndexOfEmpty/stringIndexOfFoundSuffix/stringIndexOfAbsentSuffix(result-domain / empty-needle / found-suffix / absent-suffix consequences ofindexOf(String), proven in both modes under the native-vs-axiom encoding),stringIndexOfStringproven in U (nativeseq.indexof),stringIndexOfWrongfalsifiable in U (minimality: needle occurs at 0, claim says 1; the B-mode run churns and is not in the suite) — and regressions for loop-exit flag scoping and KeY's binary search through the loop invariant). — New P6.1 fixtures: the\sumsuite (sumInvariant/sumArray/sumBounded/sumBoundedArrunder their loop strategies, andKeyFor's for-each sum proven in both modes — the BOUNDEDINVARIANTrun exercises the length fold), sixunsupportedConstructsrows — fourKeySumBadShapes(no array term, no upper bound, extra conjunct, non-monotone body) plus the element/range-domain binder rejections from the merged core feat: element-domain quantifiers over arrays, ranges and Iterables #83 (quantIterableDomain,sumIterableDomain— the domain would otherwise be silently dropped), and SITA3'scommonEntry/swapproven withrearrangegeneration-only.ExprTranslatorTest(137 cases),NormalizerTest(204),VcgResultTest(158),VcgFacadeTest(10),VcgTest(27),VcgGoldenQueriesTest— curated goldenSmtQuerysnapshots (UPDATE_GOLDEN=1to regenerate; drift fails the build). New P4.2 goldens:nullableArrayBranch(U/B),nonNullParamArray,freshArrayNonNull,storeNonNullElement,derefNullableArray. New P4.1 goldens:callWithInvariantHeld(U/B),breakInvariantBeforeCall(U),relyOnInvariantAfterCall(U_CONTRACT/U_INLINE),helperCallExempt(U),receiverInvariantHeld/receiverInvariantBroken(U). New P4.3 goldens:stringSelfEquals,stringCharAtIndexOf(U_STR),stringConcatLen(U_STR/B_STR),stringIndexOfAbsent,stringCharAtUnknown,substringLen,substringLen2,literalStartsWith,replaceContentAt0(U_STR) — plus the U_STRindexOf(String)setstringIndexOfLen,stringIndexOfEmpty,stringIndexOfFoundSuffix,stringIndexOfAbsentSuffix,stringIndexOfString(regenerated under the native sequence encoding;stringIndexOfWrongstays golden-free — falsifiable).Supporting soundness fixes in
tools:smt(portable overflow encodings, watchdog → condition-based waits,JAVA_OBJECTsorts print asU).CLI end-to-end (
VcgCommandE2eTest, 4 runs spawning the real CLI as a subprocess) and shell tests (tools/cli/shell-tests/vcg/{search,sum,sita,reverse}.txt): 06-BinarySearch and 10-SITA (--vcg-excludefor the weakrearrangecontract) verify; 08-Java5 verifies in both bounded and--unboundedmode (11 conditions, 0 failing — the fixture now carries the explicitrequires a != nullthe VCG needs), and 05-ReverseArray reports its honest 31 conditions / 2 failing with UNKNOWN (????) verdicts. The shell tester gained asortOutputfrontmatter mode (comparison over sorted, normalized lines) so nondeterministic solver-completion order cannot fail the fixtures.CI solver alignment (
82933ddf7) — the Tests workflow installs Z3 4.15.4 (was 4.13.3). Z3 < 4.15 cannot terminate on quantified bit-vector obligations such as06-BinarySearch's postcondition (the\existsover array indices under the nested sortedness\forall): Z3 4.13.3 runs until the solver watchdog maps the two postcondition conditions to UNKNOWN (????), failingbinarySearchIsVerifiedThroughItsLoopInvariantand thesearch.txtshell fixture. Reproduced locally with 4.13.3 on the pre-merge tip (unrelated to the merge with main or the P3.2 element-domain guard); 4.15.4 decides the query instantly and the full:tools:smt/:tools:vcg/:tools:clisuites plus all six shell tests pass on it. 4.15.4 is the newest Z3 the pinnedKeYProject/setup-smtaction installs on every matrix OS (4.16.0's macOS asset needs a newer action revision).Windows
jmltkclasspath fix (4ee31f163) — the last CI flake was the Windows merge job's "Run shell scripts" step. The Windows start script must use the%APP_HOME%\lib\*classpath wildcard (cmd.exe cannot hold an explicit 115-jar classpath:%APP_HOME%expands to absolute paths, so anyset CLASSPATH=line — even split across continuations — exceeds the 8191-character limit). Java expands that wildcard in directory-enumeration order, and the distribution shipped twocom.github.javaparserimplementations: the fork core (jmlparser-core-1.2.0-SNAPSHOT.jar) and KeY's proofjava fork (javaparser-core-3.28.0-K13.6.jar, a transitive of the LSP'skey.core), whoseParserConfigurationlackssetProcessJml. On Windows the proofjava jar sorts first, sojmltk vcgcrashed withNoSuchMethodErroron every install (Linux start scripts list jars in dependency order and worked). The CLI runtime now excludes theorg.key-project.proofjavagroup, so the distribution carries exactly onecom.github.javaparserimplementation and directory order cannot decide behavior. Verified: proofjava-first classpath reproduces the exact CI stack trace; the deduplicatedlib\*wildcard proves all 20 binarySearch conditions; shell tests 6/6,:tools:cli:test,:tools:lsp:testand spotless all green.