Fix integer literal type inference for subexpressions of binary expressions - #1014
Draft
jcp19 wants to merge 36 commits into
Draft
Fix integer literal type inference for subexpressions of binary expressions#1014jcp19 wants to merge 36 commits into
jcp19 wants to merge 36 commits into
Conversation
…ssions When an integer literal appears as a subexpression of a binary expression (e.g. `1` and `2` in `var x int = 1 + 2`), it previously kept the internal `UNTYPED_INT_CONST` type even though the outer context clearly implies `int`. Only the top-level binary expression `1 + 2` had its type resolved to `int` via `getTypeFromCtxt`; the individual operands were never updated. Fix: extend `getTypeFromCtxt` with new cases that walk from a subexpression up through its binary-expression parent when the sibling operand is itself a pure untyped integer constant: - For non-shift numeric binary expressions: if `isUntypedIntConst(sibling)`, propagate the context type of the parent binary expression. When the sibling already has a concrete type the case returns `None`, preserving the existing `typeMerge` behaviour (e.g. `1 + y` where `y: int8` still yields `int8`). - For shift expressions: the left operand follows the shift's context type; the right operand (shift count) is left as-is. - For unary bit-negation: the operand follows the negation's context type. A cycle-free helper `isUntypedIntConst` is added to check structurally (without calling `exprType`) whether an expression is composed solely of integer literals, iota, and arithmetic/bit operations on such expressions. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
jcp19
marked this pull request as draft
April 11, 2026 22:48
…'s type In a binary expression like `1 + x` where `x: uint8`, the literal `1` now also receives type `uint8` instead of staying as UNTYPED_INT_CONST. This matches Go's specification for untyped constants in mixed expressions. The fix updates the PBinaryExp case in getTypeFromCtxt: when the sibling operand is not a pure untyped integer constant, we call exprOrTypeType on it and, if the result is a concrete IntT, return that as the context type for the literal. No cycles are introduced because exprOrTypeType on a named/typed operand never recurses back through the literal's own type. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
In ExprTyping.scala the wildcard import brings the inner sealed trait Type into scope as the identifier 'Type', not the outer companion object. Using Type.IntT(_) in a pattern match therefore caused a compilation error. Replacing with the directly-imported IntT(_) fixes this. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
…face context
When an untyped integer constant appears in a binary expression whose
outer context type is an interface (e.g. `var y interface{} = bigLit + 2`),
the new getTypeFromCtxt cases for PBinaryExp/PShiftLeft/PShiftRight/PBitNegation
previously propagated `Some(InterfaceT)` down to the literal subexpressions.
This caused `numExprWithinTypeBounds` to fire an extra bounds-check error on
each literal subexpression in addition to the one already reported on the
binary expression as a whole, resulting in more errors than the
`//:: ExpectedOutput(type_error)` annotations expected.
Fix: in all four new cases, filter out `Some(InterfaceT)` results before
returning, falling back to `None`. The bounds check then happens only once
at the top-level binary expression node, preserving the pre-existing
error count for regression tests like issues/000157-3.gobra.
https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
The previous implementation of the 'typed sibling' case in
getTypeFromCtxt called exprOrTypeType(sibling) = exprType(sibling),
a Kiama cached attribute, from within another attribute computation.
This caused an evaluation cycle:
wellDefExpr(A op B) → getTypeFromCtxt(A) → exprType(B)
→ wellDefExpr.safe(B) → wellDefExpr(B)
→ getTypeFromCtxt(B) → exprType(A)
→ wellDefExpr.safe(A) → wellDefExpr(A op B) ← CYCLE
The cycle manifested as "Cycle detected in attribute evaluation
'store' at x * x" when checking subexpression_overflow.gobra.
Fix: replace exprType(sibling) with direct symbol-table lookups that
are cycle-safe. We only handle PNamedOperand with explicit type
annotations (the common case for `1 + x` where x: uint8). For other
sibling types, typeMerge at the binary expression level handles the
typing correctly without any context propagation needed.
https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Replaces the ambiguous x/y perm literal syntax with an explicit perm(x, y) constructor. Key changes: - Add ap.FractionalPermConstructor pattern to AstPattern.scala - Recognize perm(x, y) in AmbiguityResolution (2-arg PInvoke on perm type) - Add ExprTyping well-def/type rules for FractionalPermConstructor - Add in.PermConstructorFromInt / in.PermConstructorFromPerm to internal AST - Encode to $newPerm(x:Int,y:Int) and $newPermFromPerm(x:Perm,y:Int) Viper functions generated lazily via FunctionGeneratorWithoutContext - Remove int->perm assignability, convertibility, and type merging - Fix getTypeFromCtxt: block PermissionT propagation to int subexpressions in division (prevents Kiama cycle introduced by earlier commit) - Split perm guard in wellDefActualExpr: PDiv only fires on explicit perm operands, not from context - Update Desugar: handle FractionalPermConstructor, remove (IntT,IntT) PDiv path and int->perm fallback - Update ConstantEvaluation: handle FractionalPermConstructor, remove PDiv Test files still need updating (Step 10). https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Replace all old fractional permission literal syntax with the new perm(x, y) constructor throughout ~90 test and stub files: - acc(e, 1/2) → acc(e, perm(1, 2)) - acc(e, 1/4) → acc(e, perm(1, 4)), etc. - perm(1/2) → perm(1, 2) (old single-arg with fraction → 2-arg) - dividend/divisor in acc() → perm(dividend, divisor) - perm comparisons: p > 0 → p > noPerm, p == 1 → p == writePerm - Ghost var assignments: ghost var m5 perm = 1/2 → perm(1, 2) - perm-simple1.gobra: test9 updated to demonstrate PermDiv; m4 uses int - perm-fail1.gobra: test6/9 use int comparisons; test15 now provable - stubs: net/waitgroup/strconv updated for new perm syntax https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Add cases for the new ap.FractionalPermConstructor pattern in all PInvoke dispatch sites that were missing it, preventing violations: - GhostWellDef.scala: return noMessages (perm(x,y) is ghost, no issues) - GhostTyping.scala (ghostExprTyping): classify as isGhost (produces perm) - GhostTyping.scala (ghostExprResultTyping): classify result as isGhost - GhostTyping.scala (expectedArgGhostTyping): args are notGhost (integers) - GhostExprTyping.scala (isPureExpr): pure if both args are pure - Addressability.scala: AddrMod.rValue (perm value, not addressable) - Enclosing.scala (nilType): return None (no nil args in perm constructor) https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
After removing int→perm assignability, these files still compared perm variables directly to integer literals (0 or 1). Update to use noPerm/ writePerm constants or perm(x, y) constructor: - stubs/strconv/atoi.gobra: p > 0 → p > noPerm - stubs/time/time.gobra: p > 0 → p > noPerm (5 occurrences) - tutorial-examples/predicate.gobra: p > 0 → p > noPerm - globals/scion/monotonicset/bounded.gobra: 0 < p → p > noPerm (2 occurrences) - features/structs/structs-simple5.gobra: t.B(1/2) → t.B(perm(1, 2)) https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
After removing implicit int→perm assignability/convertibility: - `perm / int` (PermDiv) was incorrectly rejected because the well-def check for PDiv required both operands to be perm-assignable. - The result type of `perm / int` was computed as UnknownType because typeMerge(PermissionT, IntT) was removed. Fix: In wellDefActualExpr, for PDiv where left is perm, only check that the right (divisor) is an integer, not perm. In numExprType, return PermissionT directly when dividing a perm by anything. This restores correct behavior for `perm(1,2) / 4`, `p / 2` etc. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
After removing implicit int→perm coercion, several files still used integer expressions as perm arguments in acc() calls: - waitgroup-simple1.gobra: (i + 1)/1 → perm(i + 1, 1) - visitor_pattern.gobra (3 copies): 1/u → perm(1, u), 1/(u+1) → perm(1, u+1) (where u is an int variable) - binary_search_tree.gobra (3 copies): 1/dividend → perm(1, dividend) (where dividend is an int variable) - stubs/sync/waitgroup.gobra: -n/1 → perm(-n, 1), n/1 → perm(n, 1) All replacement expressions preserve the intended semantics and are valid for the perm(x, y) constructor since the denominators are guaranteed non-zero by existing preconditions. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
PermConstructorFromInt and PermConstructorFromPerm were added to the sealed Permission hierarchy but not handled in the showExpr match in PrettyPrinter.scala. This would cause a MatchError at runtime when these nodes appeared in error messages or debug output. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Replace the $newPerm/$newPermFromPerm Viper function generator approach with direct use of vpr.FractionalPerm and vpr.PermDiv. This preserves the exact offendingNode structure that Viper's ContractNotWellformed errors attach to, ensuring the causedBy check in Gobra's error transformer fires correctly for contract_not_well_formed errors. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
…on call siblings - fields/fail3.gobra: remove conjunction from preconditions so the contract IS the FieldAccessPredicate, matching what causedBy() checks. A conjunction encodes as And(A,B) in Viper; when A is ill-formed, Viper's offendingNode is A not And(A,B), so causedBy(And(A,B)) fails and produces imprecise_contract_not_well_formed instead of contract_not_well_formed. - ExprTyping.scala getTypeFromCtxt: extend sibling-type propagation to PInvoke (function calls). For `f() + (1 - 2)` where f(): uint8, the literals 1 and 2 now correctly receive type uint8. The lookup reads the callee's declared result type from the symbol table (cycle-safe), mirroring the existing PNamedOperand handling. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
For zero-divisor permission errors like perm(1, 0), Viper reports offendingNode = FractionalPerm(1, 0) — a subexpression of the contract — not the enclosing FieldAccessPredicate/PredicateAccessPredicate. The previous `e causedBy inv` check required exact equality between offendingNode and the entire contract expression, so it failed for this case, producing imprecise_contract_not_well_formed instead. Fix: replace `causedBy` in contractErr and invErr with a recursive subtree check `offendingNodeIn(target, root)` that succeeds whenever the offending node appears anywhere in the contract's Viper AST subtree. This preserves existing behaviour for access-permission errors (where offendingNode IS the whole contract) while also handling the sub- expression case needed by the perm(x, 0) fail tests. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
TypeEncoding.scala: replace `target.pos == root.pos` with `target eq root` in offendingNodeIn. vpr.Node does not extend vpr.Positioned, so calling .pos on a plain vpr.Node reference was a compile error that broke the Docker build. Reference equality (eq) is also semantically more correct: the error's offendingNode IS the actual object from the encoded AST, so reference identity correctly identifies it anywhere in the subtree without risk of false matches from structurally equal nodes at different positions. ExprTyping.scala: replace the manual symbol-table lookup block in the else-branch of getTypeFromCtxt (binary-expression sibling case) with a single exprType(sibling) call. The call is cycle-safe in the else-branch because the cycle exprType(A) → getTypeFromCtxt(A) → exprType(B) → getTypeFromCtxt(B) → exprType(A) only forms when isUntypedIntConst holds for BOTH operands; the else-branch is only reached when isUntypedIntConst is false for the sibling, breaking the cycle. This generalises type propagation to cover all context-independent expressions: method calls (m.f()), field accesses (s.field), type conversions, and complex sub-expressions — not just plain variables and free-function calls. int-lit-subexpr-types.gobra: add regression tests for function-call, method-call, and field-access siblings. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
testFunctionCallSibling: add postcondition `ensures ret == 42` to getUint8() so the verifier can prove assert(x == 43). Without a postcondition, the function's return value is opaque to callers. testMethodCallSibling: switch from pointer receiver (*S) to value receiver (S) to avoid heap-permission requirements, and use a named return value instead of an assertion (avoids needing to know the specific field value). testFieldAccessSibling: similarly use a named return value. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
The previous implementation used `eq` (reference equality), which would fail when Silver creates structurally-equal but distinct node copies during error reporting (e.g. after AbstractVerificationError.transformedError()). Use the same matching logic as `causedBy` in BackTranslator: structural equality (`==`) for the node, plus position equality for Positioned nodes. Apply this recursively to subnodes so that sub-expression offending nodes (e.g. FractionalPerm(1, 0) inside a FieldAccessPredicate) are found even when Silver reports the inner node rather than the outer contract expression. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
…ings When the sibling in a binary expression is a PNumExpression (e.g. x*x where x is an untyped named constant), calling exprType(sibling) causes a cycle: exprType(A) → getTypeFromCtxt(A) → isUntypedIntConst(B)=false → exprType(B) → getTypeFromCtxt(B) → exprType(A) → CYCLE The fix: for PNumExpression siblings, use numExprType(sibling) instead of exprType(sibling). numExprType only calls exprType on sub-nodes of the sibling expression (not on the sibling itself), and those sub-nodes go through exprAndTypeType (for named constants) which does NOT call getTypeFromCtxt, so no cycle can form. For non-PNumExpression siblings (variables, method calls, field accesses), exprType remains safe because those branches in actualExprType do not call getTypeFromCtxt on the expression itself. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Both FileResource and JarResource listContent() methods were not closing the DirectoryStream obtained from Files.newDirectoryStream(). Wrap the stream in a try/finally to ensure it is always closed. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
… folding Three targeted fixes: 1. bounded.gobra: Replace old `p/2` permission notation with `perm(p, 2)` in loop invariants of ContainsImpliesAbstractContains and DoesNotContainsImpliesAbstractDoesNotContain, which caused type errors. 2. ConstantEvaluation.scala (PBitNegation): Add isLiteralCluster helper to detect untyped constant operands. For untyped clusters, compute the arbitrary-precision NOT as -(x+1) instead of using exprType, which could be contaminated by the surrounding typed context. This restores the expected overflow error for `AND3 = uint32(1) & ^1`. 3. Desugar.scala (PShiftLeft/PShiftRight): Constant-fold shift expressions when intConstantEvaluation returns a value. Shift operations are encoded as uninterpreted Viper functions opaque to Z3, so `1 << 2` would not be provably equal to 4. With constant folding, the expression is replaced by IntLit(4) in the internal AST, making `assert(d == 4)` trivially provable. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Replace integer-division perm expressions (1/2, 1/4, 1/512) with the current perm constructor notation (perm(1,2), perm(1,4), perm(1,512)). The old notation is no longer valid and caused type errors. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Ignore *.bak backup files, JVM crash logs (hs_err_pid*.log), and local sbt/ directory that can appear during development. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Add five unit tests (and two TestFrontend helpers) that directly assert the types inferred for subexpressions, covering each scenario from the earlier discussion: - int8-typed declaration context: `var b int8 = 1 + 2` → both literals int8 - shift left operand: `n := 1 << 2` → left literal gets context type (int) - uint8 sibling variable: `n := 1 + x` (x: uint8) → literal gets uint8 - function-call sibling: `n := getUint8() + 1` → literal gets return type uint8 - field-access sibling: `n := s.field + 1` (field: uint8) → literal gets uint8 New helpers: singleExprTypedTypeInfo (typed-var-decl context) and singleExprWithFuncTypeInfo (program with an auxiliary function declaration). https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Go evaluates constant expressions with arbitrary precision; only the final value assigned to a typed constant needs to be representable in that type. Intermediate values (e.g. `1 << 16` in `(1 << 16) - 1`) are allowed to exceed the declared type's bounds. Fix: in the exprWithinBounds block for arithmetic/bitwise binary expressions, skip the per-operand bounds checks when the whole expression is a pure untyped integer constant (no explicit type conversions in the tree, as determined by isUntypedIntConst). Only the final-result check on `n` is kept. Per-operand checks are preserved for expressions involving explicit types (e.g. `uint8(1) * (-1)`) or variable operands (e.g. `300 + y` where y : uint8). Add regression test const-folding-overflow.gobra with: const MaxISD uint16 = (1 << 16) - 1 const MaxUint8 uint8 = (1 << 8) - 1 const MaxUint32 uint32 = (1 << 32) - 1 const MaxInt8 int8 = (1 << 7) - 1 https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
In test environments where `dependentTypeInfo` is initialized with `Map.empty` (e.g. minimal TypeInfoImpl stubs in unit tests), resolving a qualified expression like `PDot(s, "field")` could trigger `tryUnqualifiedBuiltInPackageLookup` which unconditionally called `tryPackageLookup(BuiltInImport, id)` — crashing with a LogicException because BuiltInImport is not present in the map. Guard the lookup with a presence check: return None when BuiltInImport is absent. In production, Info.scala always adds BuiltInImport for every non-builtin package, so the guard is never triggered there. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Go requires that untyped constant operands of comparisons be representable in the type of the other operand (e.g. `x < 1000` where x: uint8 must be rejected because 1000 overflows uint8). Previously, getTypeFromCtxt only handled PNumExpression binary ops, so comparison operands like PEquals, PLess, etc. returned None and literals stayed as UNTYPED_INT_CONST, bypassing bounds checks. Add a case in getTypeFromCtxt for comparison operators (== != < <= > >=) that propagates the sibling's concrete integer type to the literal operand. Unlike arithmetic expressions, comparisons return bool so there is no outer context type to propagate — only the sibling type matters. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Using `bExpr @ (_: PEquals | ...)` infers bExpr as PActualExpression (the LUB of the alternatives), not PBinaryExp, so .left/.right did not resolve. Switch to the same guard style as the PNumExpression case: `bExpr: PBinaryExp[_, _] if bExpr.isInstanceOf[...]`. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
numExprType can throw LogicException for ill-typed PNumExpression nodes (e.g. len applied to a non-collection argument). When such an expression appears as the sibling of a comparison or arithmetic operand, the call to numExprType inside getTypeFromCtxt would crash instead of gracefully returning None. Introduce tryNumExprType, which wraps numExprType in a try-catch for LogicException and returns None on failure. Use it at both call sites in getTypeFromCtxt (comparison case and arithmetic case). When a sibling is ill-typed, getTypeFromCtxt now returns None (no context type inferred), which is the correct fallback — the error on the ill-typed sibling is reported separately by its own well-definedness check. https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
PSub(PIntLit(0), expr) is Gobra's AST representation of unary minus. When a comparison such as `assert N3 == -128` (N3: int8) propagated int8 as context to PSub(0, 128), the arithmetic-sibling case would further propagate that int8 context to the inner PIntLit(128). Since 128 > 127 (max int8), this produced a spurious "constant expression 128 overflows int8" error even though -128 is the minimum int8 value. Fix: detect the PSub(PIntLit(0), expr) unary-negation pattern and skip propagating the parent context to expr. The correct bounds check already happens at the PSub level (value = -128, which fits in int8). https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8
Contributor
Author
|
@ArquintL do you oppose to the new syntax for permissions introduced in this PR? |
Member
@jcp19 I do understand that it helps in resolving parsing ambiguities but to be honest it's (1) changing the syntax for one of the most prevalent building blocks of Gobra programs, triggering many changes, and (2) the new syntax is quite verbose and imho makes programs less readable (but that's maybe just a getting used to). Regarding (2), I'm wondering whether there's an alternative to |
Contributor
Author
|
Regarding (1), I get that it is annoying to perform this change, but we are fixing an annoying ambiguity that hampers the type checker, and the change can be easily automated. As for (2), I agree with the verbosity but I don't immediately see a good solution: the proposal with the float notation is pushing the ambiguity down to floats/perms; |
…type-inference-UFkBe # Conflicts: # src/main/resources/stubs/sync/waitgroup.gobra # src/test/resources/regressions/examples/evaluation/impl_errors/parallel_search_replace.gobra # src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra # src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra # src/test/resources/regressions/examples/evaluation/parallel_sum.gobra # src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra # src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra # src/test/resources/regressions/examples/parallel_search_replace_shared.gobra # src/test/resources/regressions/examples/tutorial-examples/channels.gobra # src/test/resources/regressions/examples/tutorial-examples/multi-channel.gobra # src/test/resources/regressions/features/channels/channel-simple-buffered1.gobra # src/test/resources/regressions/features/channels/channel-simple-buffered2.gobra # src/test/resources/regressions/features/channels/channel-simple5.gobra # src/test/resources/regressions/features/channels/channel-simple6.gobra # src/test/resources/regressions/features/channels/channel-simple7.gobra # src/test/resources/regressions/features/channels/foo/foo.gobra # src/test/resources/regressions/features/channels/multi-channel-simple1.gobra # src/test/resources/regressions/features/defunc/waitgroup-fail1.gobra # src/test/resources/regressions/features/defunc/waitgroup-simple1.gobra # src/test/resources/regressions/issues/000695.gobra
…1083) * Port integer parsing/type-checking from integer-type-semantics Moves the frontend half of the bounded-integer work from claude/integer-type-semantics-RUVTQ down to this branch, so that it can ship ahead of the encoding. Only parsing and type-checking is ported; the domain-based encoding, the desugarer's int-kind alignment, the --unboundedIntegers flag and IntKindAlignment stay behind. Type-checking changes: * TypeBounds: add the UntypedConstInteger kind and make UntypedConst default to it, so untyped literals are distinguishable from the explicit `integer` ghost type. merge() becomes strict (`integer` no longer silently merges with a bounded kind); mergeLenient() keeps the old permissive behaviour for the internal AST. * Assignability: every integer kind is assignable to `integer`; the converse still requires an explicit conversion. * TypeMerging: `integer` is the common type of itself and any bounded kind, so mixed comparisons are well-typed. * ExprTyping: perm(num, den) requires `integer`/perm rather than any integer; len/cap of a ghost collection yields `integer`; bitwise and shift diagnostics account for the new kind. * GhostExprTyping: multiplicities, option projections and range sequences yield `integer` instead of an untyped constant. * IdTyping: resolve the int/uint built-in tags through the configured type bounds, so int(x) is 64-bit in 64-bit mode. * ConstantEvaluation: handle the new kind, and evaluate unsigned right shifts without the Long round-trip that overflowed near MaxUint64. Consequences outside the frontend, required by the above: * internal Program.scala uses mergeLenient for BinaryIntExpr and accepts an untyped constant next to a defined type. The desugarer synthesizes arithmetic mixing user expressions with `integer` nodes, which the strict frontend rule must not reject here. * the sync.WaitGroup stub converts explicitly in perm(integer(n), 1), since perm no longer accepts a bounded int. The encoding is untouched: this branch still encodes every integer kind as a mathematical Viper Int with overflow checks added by OverflowChecksTransform, so the new kind needs no encoding support. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Adapt regression tests to the ported integer type-checking rules Fallout from the type-checking port, applied minimally: only the changes that the new rules *require*, not the overflow hardening that accompanies them on claude/integer-type-semantics-RUVTQ. Two rules drive every change: * perm(num, den) now demands `integer`, so a bounded operand is wrapped: perm(1, dividend) -> perm(1, integer(dividend)). * len/cap/multiplicity on a ghost collection now yields `integer`, so results are either declared `integer` or converted back with int(...). Deliberately NOT taken from RUVTQ, since they serve the bounded-integer encoding this branch does not have: * `forall i int ::` -> `forall i integer ::` quantifier hardening, * math.MaxInt* bounds and the `math` stub import, * `// ##(--unboundedIntegers)` directives for a flag not ported, * the seqSum -> seqSumFrom restructuring in closures-calldesc4-map. Also ports features/integers/int-conversion-64bit.gobra, which covers the IdTyping change (int(x) must use the configured kind, not the statically 32-bit built-in tag). It verifies on this branch. ghost-pure-function.gobra and seq-convert-fail3.gobra still report type errors, but only the ones their ExpectedOutput annotations assert. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Correct the mergeLenient rationale and pin it with a test The comment added with the port claimed BinaryIntExpr.typ needs mergeLenient because the desugarer synthesizes arithmetic mixing user expressions with internally-created `integer` nodes, naming range-loop index increments as the example. That is wrong: the range-loop index i0 is declared as in.IntT(exclusiveVariable), which defaults to UnboundedInteger, and the synthesized in.IntLit(1) defaults to the same kind, so the two merge trivially. A range loop over a []int does not exercise it. The actual reason is the type-checker, not the desugarer: TypeMerging makes `integer` the common type of itself and any bounded kind, so user code may legitimately write `len(s) - i` for a ghost `s seq[int]` and a bounded `i int`. Both operand kinds survive desugaring, so BinaryIntExpr.typ has to merge `integer` with `int`. Verified by rebuilding with the strict merge: that expression fails with "kinds IntegerKind(integer) and IntegerKind(int) cannot be merged". Adds features/integers/integer-bounded-mix.gobra covering it, so the requirement cannot regress silently. Note that the strict/lenient split is otherwise vestigial on this branch: TypeBounds.merge has no caller besides mergeLenient's own fallback. It is kept as-is to stay identical to claude/integer-type-semantics-RUVTQ, so that branch merges without conflicting here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
jcp19
commented
Aug 9, 2026
Comment on lines
+13
to
+19
| ghost | ||
| requires 0 <= i && i <= len(s) | ||
| ensures res == len(s) - i | ||
| decreases | ||
| pure func remaining(s seq[int], i int) (res integer) { | ||
| return len(s) - i | ||
| } |
Contributor
Author
There was a problem hiding this comment.
this is a bad motivation for mergeLenient, we could have made i an integer variable too
jcp19
pushed a commit
that referenced
this pull request
Aug 15, 2026
Four places where Gobra's treatment of integer constant expressions differed from the Go language specification, found while reviewing #1014. 1. Untyped constant comparison crashed the type checker. `assert 1 + 2 == 3 + 4` is a valid untyped boolean constant expression in Go, but aborted Gobra with "Cycle detected in attribute evaluation 'store'". The comparison case of getTypeFromCtxt peeked at the sibling operand's type, and for two compound untyped operands each side asked the other for its type until exprType re-entered a node still under evaluation. Per the spec a comparison of two untyped constants is itself an untyped constant and imposes no representability requirement, so no type needs to be propagated in that case. Deciding this structurally, before computing any type, both matches the spec and removes the cycle. `uint8(4) < 1000` is still rejected, since there one operand is typed. 2. Representability was checked at every node of a constant expression. The spec requires it only where the constant is given a type: "constant expressions are always evaluated exactly; intermediate values and the constants themselves may require precision significantly larger than supported by any predeclared type in the language". Gobra rejected `var x uint16 = (1 * 70000) - 69999`, which Go accepts. The check now happens once, at the outermost node of an untyped constant expression. 3. Shift counts were bounded by the width of the left operand's type. Go states "there is no upper limit on the shift count"; what makes `int8(1) << 10` invalid is that the value 1024 is not representable in int8. Gobra rejected `var c uint8 = (1 << 10) >> 3`, whose result 128 does fit. The type-width bound is replaced by a check that the shift's value is representable in its type; MAX_SHIFT is kept as an implementation limit. 4. References to untyped constants were treated as typed, and constant division by zero crashed. `const c = 300; var x uint8 = c - 100` is valid Go but was rejected. isUntypedIntConst now follows a name to its constant declaration, treating it as untyped only when the declaration gives no type and its defining expression is itself untyped (so `const c = int8(5)` stays typed), with a visited set so a cyclic declaration cannot recurse forever. `const d = 1/0` aborted with java.lang.ArithmeticException. The spec says "the divisor of a constant division or remainder operation must not be zero"; it is now reported as a type error, matching gc's wording. perm(x, 0) is deliberately left to the Viper well-formedness check that reports it as contract_not_well_formed, since a non-constant denominator cannot be caught statically and `perm` is not a Go construct. Full regression suite: 2371 of 2376 pass, the same set as before this change. The 5 failures are pre-existing on this branch: three files still using the old `1/2` permission syntax that the perm(x, y) migration missed (atomicsAndInvariants/spinlock.gobra, issues/001029.gobra, issues/001057-2.gobra) and two Carbon tests needing Boogie. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XV3UW3HZD9Gcf2s462BLaZ
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
3 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.
Summary
getTypeFromCtxtinExprTyping.scalahad no case forPBinaryExporPBitNegationas parents, so integer literal subexpressions always fell through tocase _ => Noneand kept the internalUNTYPED_INT_CONSTtype. For example, invar x int = 1 + 2, the expression1 + 2correctly received typeint(via the existing context-propagation logic), but1and2individually stayed asUNTYPED_INT_CONST(unbounded int).isUntypedIntConstthat structurally checks whether an expression is a pure untyped integer constant (without callingexprType). ExtendgetTypeFromCtxtwith new cases: for numeric binary expressions whose sibling operand is also untyped, propagate the binary expression's own context type downward; for shift operations, propagate only to the left (value) operand; for unary bit-negation, propagate to the sole operand.typeMergebehaviour: when the sibling already has a concrete type (e.g.1 + ywherey: int8), the new case returnsNone, leaving1asUNTYPED_INT_CONSTso thattypeMerge(UNTYPED_INT_CONST, int8) = int8continues to work as before.Test plan
ExprTypingUnitTests.scaladirectly assert thatexprTypereturns the correct concrete type for literal subexpressions in binary expressions (1and2inn := 1 + 2→IntT(DefaultInt)), for nested expressions, and that the typed-sibling case is unchanged.int-lit-subexpr-types.gobraexercisesvar a int = 1 + 2,var b int8 = 1 + 2,var c int = 1 + 2 + 3, andvar d int = 1 << 2.int-bounds2.gobra(id(255+1)) andint-sizes1.gobra(u + 1whereu: int8) should continue to pass — the fix was designed to leave typed-sibling cases unchanged.sbt "testOnly viper.gobra.typing.ExprTypingUnitTests"andsbt test(with Z3 available) to confirm no regressions.https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8