Fix integer literal type inference for subexpressions of binary expressions

[jcp19]

Summary

This PR fixes the type inference of integer literals that occur as subexpressions of binary expressions and, building on that, ports the parsing and type-checking half of the bounded-integer work (see #1083) ahead of its encoding. Along the way, it replaces the ambiguous fractional-permission syntax a/b with an explicit constructor perm(a, b).

Integer literal type inference

• Root cause: getTypeFromCtxt in ExprTyping.scala had no case for PBinaryExp or PBitNegation as parents, so integer literal subexpressions always kept the internal UNTYPED_INT_CONST type. In var x int = 1 + 2, the expression 1 + 2 got type int, but 1 and 2 individually stayed untyped.
• Fix: the cycle-free, structural predicate isUntypedIntConst decides whether an expression is a pure untyped integer constant (literals, iota, references to untyped named constants, and shifts, bit-negation and arithmetic on such). getTypeFromCtxt uses it to propagate the context type to the operands of arithmetic, shift and bit-negation expressions, and the type of a typed sibling to the untyped operand of a comparison (so that x < 1000 for x uint8 is rejected, as by gc).
• Untyped named constants are checked for representability in the type their context imposes, exactly like literals: with const c = 300, var x uint8 = c, return c, g(c) and x == c are rejected as by gc.
• Go-conformant constant expressions: constant expressions are evaluated exactly. Representability is checked only at the outermost node of an untyped constant expression, so var x uint16 = (1 << 16) - 1 and var x uint16 = (1 * 70000) - 69999 are accepted; the shift count is no longer bounded by the width of the left operand's type (var c uint8 = (1 << 10) >> 3 is valid Go), only the value of a constant shift has to be representable; and constant division by zero is a type error instead of an uncaught ArithmeticException.

Integer types

• TypeBounds.UntypedConstInteger distinguishes an untyped literal from the explicit ghost type integer.
• Every integer kind is assignable to integer; the converse requires an explicit conversion. integer is the common type of itself and any bounded kind, so mixed arithmetic and comparisons are well-typed.
• len/cap of a ghost collection, multiplicities, option projections and range sequences have type integer instead of an untyped constant.
• int(x)/uint(x) conversions use the configured integer kind, i.e. they are 64-bit in 64-bit mode (previously they were given 32-bit bounds).
• Bitwise NOT of an untyped constant is computed with arbitrary precision (-(x+1)), unsigned constant right shifts no longer overflow near MaxUint64, and constant shifts are folded by the desugarer so that Silicon can reason about them.

Fractional permission syntax

1/2 is now always integer division, as in Go (m := 1/2 + 1/2 yields 0). Fractional permission amounts are written perm(num, den); perm(p, n) divides a permission amount p by an integer n. Both arguments accept integers of any kind (a bounded operand is promoted to integer). Integer literals are no longer implicitly converted to perm, so p > 0 for a perm variable is written p > noPerm. All regression tests, the stubs and docs/tutorial.md are migrated. (Alternative designs, such as 1.0/2, were discussed in this PR.)

Other fixes

• PackageResolver closed the DirectoryStreams it opened only implicitly, leaking file handles.
• TypeEncoding.offendingNodeIn matches a ContractNotWellformed error to a contract when Viper reports a sub-expression of the contract as offending node (e.g. perm(1, 0) inside an accessibility predicate), so that such errors are reported as contract_not_well_formed instead of being dropped.
• int(1, 2) (a two-argument "conversion" other than perm) is a type error instead of an internal violation.

Test plan

• New unit tests in ExprTypingUnitTests.scala assert the types of literal subexpressions (typed context, typed siblings, function-call, method-call and field-access siblings, comparisons, shifts).
• New regression tests: integers/int-lit-subexpr-types.gobra, integers/const-folding-overflow.gobra, integers/const-expr-exact-eval{,-fail1}.gobra, integers/comparison-type-infer-fail1.gobra, integers/int-conversion-64bit.gobra, integers/integer-bounded-mix.gobra, integers/named-const-representability{,-fail1}.gobra, fractional_permissions/perm-constructor-{simple1,fail1}.gobra.
• sbt test with Z3 4.8.7 (Silicon); the two Carbon tests need Boogie and were not run locally.

https://claude.ai/code/session_01SJi7UpEB7rFRw39Q1Uo1R8

[jcp19]

@ArquintL do you oppose to the new syntax for permissions introduced in this PR?

[ArquintL]

@ArquintL do you oppose to the new syntax for permissions introduced in this PR?

@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 perm while avoiding the ambiguity with integer division: My first thought was that we could treat 1/2 consistently as integer division and require that permissions must be (unbounded) floats, such that one would have to write 1.0/2 or 1/2.0 instead (effectively making use of Go's special treatment of constants wrt. precision). Alternatively, I was thinking of adding syntactic sugar to denote rational division (with infinite precision) such that one could write 1 // 2 for half a permission.

[jcp19]

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; 1 // 2 introduces a comment (//). We could write 1 \ 2, but this is a bit ugly (kinda suggests that \ is the flip of /), or 1 # 2

[jcp19]

this is a bad motivation for mergeLenient, we could have made i an integer variable too

[jcp19]

Review: conformance with the Go spec

I checked this branch's integer/constant typing against the Go language specification, and verified every case twice — against gc 1.24.7 and against a build of this branch. Four divergences, one of which is a crash. Fixes are on claude/gobra-pr-1014-review-6au6g1 (branched from bdb3b0f).

Program	Go 1.24.7	this branch
assert 1 + 2 == 3 + 4	accepted	crash — IllegalStateException: Cycle detected in attribute evaluation 'store' at 1
var c uint8 = (1 << 10) >> 3	accepted	rejected: shift count 10 too large for type uint8
var x uint16 = (1 * 70000) - 69999	accepted	rejected twice, once per intermediate
const c = 300; var x uint8 = c - 100	accepted	rejected: constant expression c overflows uint8
const d = 1/0	invalid operation: division by zero	crash — java.lang.ArithmeticException

1. The comparison case in getTypeFromCtxt cycles

The new comparison case peeks at the sibling operand's type. When both operands are compound untyped constants, each side asks the other for its type until exprType re-enters a node still under evaluation:

exprType(1) → getTypeFromCtxt(1) → sibling 2 untyped → getTypeFromCtxt(1+2)
  → parent is PEquals → tryNumExprType(3+4) → exprType(3) → … → tryNumExprType(1+2)
  → exprOrTypeType(1) → exprType(1)   ← already in progress

tryNumExprType only catches Violation.LogicException, so Kiama's cycle error escapes. Commits 8c90008 and 008da.. already fixed cycles here; this case was added afterwards and reintroduces the shape.

Per the spec, a comparison of two untyped constants is itself an untyped constant with no representability requirement, so no type needs propagating in that case. Deciding that structurally, before computing any type, is both the spec rule and the cycle fix. uint8(4) < 1000 is still rejected, since there one operand is typed.

2. Representability is checked at every node, not just where the type is imposed

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.

The check belongs at the outermost node of an untyped constant expression only. isUntypedIntConst(n) handles the (1 << 16) - 1 shape, but the per-literal check in wellDefActualExpr and the per-node check still fire on intermediates, so (1 * 70000) - 69999 is rejected.

3. Shift counts are bounded by the left operand's type width

Go says "there is no upper limit on the shift count" — what makes int8(1) << 10 invalid is that 1024 is not representable in int8, not the count. v << 10 for a uint8 variable is valid Go (yields 0) and was rejected too.

Worth noting: const-folding-overflow.gobra passes only because the bound is v > nBits and the tests land on v == nBits exactly. (1 << 20) >> 8 breaks it. Replacing the width bound with a value-representability check removes that fragility; MAX_SHIFT stays as an implementation limit, so 1 << 1024 is still rejected.

4. Named untyped constants, and 1/0

isUntypedIntConst treats any PNamedOperand as typed, so const c = 300; var x uint8 = c - 100 is rejected. Following the name to its declaration fixes it — untyped only when the declaration gives no type and its defining expression is itself untyped, so const c = int8(5) correctly stays typed. Constant division by zero threw an uncaught ArithmeticException; it is now a type error with gc's wording.

I deliberately did not add a static check for perm(x, 0): it broke fractional_permissions/{fields,predicates}/fail3.gobra, which expect contract_not_well_formed — which is exactly what the offendingNodeIn change here exists to support. A non-constant denominator can't be caught statically anyway, and perm isn't a Go construct.

Test results: 2371/2376, the identical failure set as before the change. The 5 are pre-existing on this branch: atomicsAndInvariants/spinlock.gobra, issues/001029.gobra and issues/001057-2.gobra still use the old 1/2 permission syntax and were never touched by this PR (the perm(x, y) migration missed them — this is what CI is red on), plus two Carbon tests needing Boogie.

---

On the integer(n) question in waitgroup.gobra

The conversion isn't necessary. Assignability.scala now makes every integer kind implicitly assignable to integer, but the perm(num, den) well-definedness uses an ad-hoc isIntegerOrUntypedConst that rejects bounded kinds outright. Using assignableTo.errors(numT, IntT(UnboundedInteger), mayInit) instead would let perm(n, 1) work directly and leave one rule rather than two. (The -integer(n) on the n < 0 line is separately justified by its MinInt64 comment — that one should stay.)

On perm(a, b) vs 1/2

Go hit this exact ambiguity and resolved it the way @ArquintL proposed — from Constant expressions:

const Θ float64 = 3/2     // Θ == 1.0 (3/2 is integer division)
const Π float64 = 3/2.    // Π == 1.5 (3/2. is float division)

Note what that says: the declared type does not make 3/2 float division; the operand kinds do. So 1.0/2 vs 1/2 is a rule Go users already know, and it avoids both the verbosity and the AmbiguityResolution special case — which currently violations (internal error, not a type error) on any two-argument T(a, b) where T isn't the built-in perm, so a typo like int(1, 2) crashes.

Smaller things

• docs/tutorial.md is not updated. It teaches acc(x, 1/2) in ~10 places (287, 415–421, 490, 509, 515–517, 535, 677–678), all of which this PR turns into type errors.
• isLiteralCluster in ConstantEvaluation.scala is a byte-for-byte duplicate of isUntypedIntConst; both traits mix into TypeInfoImpl, so one can be shared.
• perm-fail1.gobra: test11 and test12 are now identical, and test15's comment ("the subexpressions … are treated as integer expressions and not as perms") is stale — the test now asserts the opposite.
• Convertibility drops (IntT(_), PermissionT), so one-arg perm(x) on an int no longer converts; the ap.Conversion-to-perm paths in Desugar/permConstantEval are now reachable only for perm→perm.
• The PR description still describes only the original literal-typing fix. The DirectoryStream leak fix, the 64-bit int()/uint() conversion fix and offendingNodeIn are independent of the perm syntax change and could land separately rather than waiting on that discussion.

---

Generated by Claude Code