From e65c53679916ccec1b5306ab8d898890c54eaf9d Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 19 Apr 2026 11:15:13 +0000 Subject: [PATCH] Infer bounded type for untyped int literals in comparisons An untyped integer constant appearing as one operand of a comparison (==, !=, <, <=, >, >=, including ghost equality/inequality) now takes its context type from the other operand when that operand has a bounded integer type. This mirrors Go's implicit conversion of untyped constants in comparisons, so the desugarer and encoding never see mixed-sort operands like Int vs int8. Implemented by extending getTypeFromCtxt in ExprTyping with cases for the comparison AST nodes, delegating to a new boundedCtxFromComparison helper that resolves the other operand's type, unwraps any named wrappers via underlyingType, and returns the operand's declared type when its kind is a BoundedIntegerKind. --- .../implementation/typing/ExprTyping.scala | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala index 7f83e1ce8..9feed747f 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala @@ -1018,6 +1018,18 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case c => Violation.violation(s"This case should be unreachable, but got $c") } + // If expr is an operand of a comparison whose other operand has a bounded integer type, + // pin expr's context type to that bounded type. This mirrors Go's implicit conversion of + // untyped constants in comparisons and avoids mixed-sort operands reaching later stages. + case cmp: PEquals => boundedCtxFromComparison(cmp.left, cmp.right, expr) + case cmp: PUnequals => boundedCtxFromComparison(cmp.left, cmp.right, expr) + case cmp: PLess => boundedCtxFromComparison(cmp.left, cmp.right, expr) + case cmp: PAtMost => boundedCtxFromComparison(cmp.left, cmp.right, expr) + case cmp: PGreater => boundedCtxFromComparison(cmp.left, cmp.right, expr) + case cmp: PAtLeast => boundedCtxFromComparison(cmp.left, cmp.right, expr) + case cmp: PGhostEquals => boundedCtxFromComparison(cmp.left, cmp.right, expr) + case cmp: PGhostUnequals => boundedCtxFromComparison(cmp.left, cmp.right, expr) + // expr has the default type if it appears in any other kind of statement case x if x.isInstanceOf[PStatement] => Some(DEFAULT_INTEGER_TYPE) @@ -1059,6 +1071,18 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => } } + private def boundedCtxFromComparison( + left: PExpressionOrType, + right: PExpressionOrType, + expr: PExpression): Option[Type] = { + val other: PExpressionOrType = if (left eq expr) right else left + val otherType = exprOrTypeType(other) + underlyingType(otherType) match { + case IntT(_: BoundedIntegerKind) => Some(otherType) + case _ => None + } + } + def getBlankIdType(b: PBlankIdentifier): Type = b match { case tree.parent(p) => p match { case PAssignment(right, left) => getBlankAssigneeType(b, left, right)