Fix bounded integer encoding with overflow checking

src/main/resources/stubs/math/const.gobra

@@ -0,0 +1,31 @@
+// Copyright 2009 The Go Authors. All rights reserved.
+// Use of this source code is governed by a BSD-style
+// license that can be found in https://golang.org/LICENSE
+
+// Signatures for the public declarations in file
+// https://github.com/golang/go/blob/master/src/math/const.go
+
+package math
+
+// Integer limit values.
+//
+// NOTE (Gobra): the architecture-dependent limits `MaxInt`, `MinInt`, and
+// `MaxUint` are deliberately NOT provided. Their values depend on the size of
+// the platform `int`/`uint` (32 or 64 bits), which the verifier does not fix,
+// so a proof relying on them would be unsound on some target. Use the
+// limits of a concrete sized type (e.g. `MaxInt64`, `MinInt32`, `MaxUint8`)
+// instead.
+const (
+	MaxInt8   = 1<<7 - 1   // 127
+	MinInt8   = -1 << 7    // -128
+	MaxInt16  = 1<<15 - 1  // 32767
+	MinInt16  = -1 << 15   // -32768
+	MaxInt32  = 1<<31 - 1  // 2147483647
+	MinInt32  = -1 << 31   // -2147483648
+	MaxInt64  = 1<<63 - 1  // 9223372036854775807
+	MinInt64  = -1 << 63   // -9223372036854775808
+	MaxUint8  = 1<<8 - 1   // 255
+	MaxUint16 = 1<<16 - 1  // 65535
+	MaxUint32 = 1<<32 - 1  // 4294967295
+	MaxUint64 = 1<<64 - 1  // 18446744073709551615
+)

src/main/scala/viper/gobra/Gobra.scala

@@ -15,7 +15,7 @@ import com.typesafe.scalalogging.StrictLogging
 import org.slf4j.LoggerFactory
 import scalaz.Scalaz.futureInstance
 import viper.gobra.ast.internal.Program
-import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, InternalTransform, OverflowChecksTransform}
+import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, InternalTransform}
 import viper.gobra.backend.BackendVerifier
 import viper.gobra.frontend.PackageResolver.{AbstractPackage, RegularPackage}
 import viper.gobra.frontend.Parser.ParseResult
@@ -50,6 +50,8 @@ object GoVerifier {
 
 trait GoVerifier extends StrictLogging {
 
+  protected val timeFormatter: DateTimeFormatter = DateTimeFormatter.ofPattern("HH:mm:ss")
+
   def name: String = {
     this.getClass.getSimpleName
   }
@@ -86,7 +88,6 @@ trait GoVerifier extends StrictLogging {
       }
     })
 
-    val timeFormatter = DateTimeFormatter.ofPattern("HH:mm:ss");
     config.packageInfoInputMap.keys.foreach(pkgInfo => {
       val pkgId = pkgInfo.id
       logger.info(s"Verifying package $pkgId [${LocalTime.now().format(timeFormatter)}]")
@@ -254,6 +255,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
   // that all imported packages have been parsed successfully (this is only checked during type-checking)
   private def performParsing(config: Config, pkgInfo: PackageInfo)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, Map[AbstractPackage, ParseResult]] = {
     if (config.shouldParse) {
+      logger.info(s"Phase 1/6: parsing [${LocalTime.now().format(timeFormatter)}]")
       val startMs = System.currentTimeMillis()
       val res = Parser.parse(config, pkgInfo)
       logger.debug {
@@ -268,6 +270,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
 
   private def performTypeChecking(config: Config, pkgInfo: PackageInfo, parseResults: Map[AbstractPackage, ParseResult])(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, TypeInfo] = {
     if (config.shouldTypeCheck) {
+      logger.info(s"Phase 2/6: type-checking [${LocalTime.now().format(timeFormatter)}]")
       Info.check(config, RegularPackage(pkgInfo.id), parseResults)
     } else {
       EitherT.left(Vector.empty)
@@ -276,6 +279,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
 
   private def performDesugaring(config: Config, typeInfo: TypeInfo)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, Program] = {
     if (config.shouldDesugar) {
+      logger.info(s"Phase 3/6: desugaring [${LocalTime.now().format(timeFormatter)}]")
       val startMs = System.currentTimeMillis()
       val res = EitherT.right[Vector[VerifierError], Future, Program](Desugar.desugar(config, typeInfo)(executor))
       logger.debug {
@@ -289,18 +293,12 @@ class Gobra extends GoVerifier with GoIdeVerifier {
   }
 
   /**
-    * Applies transformations to programs in the internal language. Currently, only adds overflow checks but it can
-    * be easily extended to perform more transformations
+    * Applies transformations to programs in the internal language.
     */
   private def performInternalTransformations(config: Config, pkgInfo: PackageInfo, program: Program)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, Program] = {
-    // constant propagation does not cause duplication of verification errors caused
-    // by overflow checks (if enabled) because all overflows in constant declarations 
-    // can be found by the well-formedness checks.
+    logger.info(s"Phase 4/6: internal transformations [${LocalTime.now().format(timeFormatter)}]")
     val startMs = System.currentTimeMillis()
-    var transformations: Vector[InternalTransform] = Vector(CGEdgesTerminationTransform, ConstantPropagation)
-    if (config.checkOverflows) {
-      transformations :+= OverflowChecksTransform
-    }
+    val transformations: Vector[InternalTransform] = Vector(CGEdgesTerminationTransform, ConstantPropagation)
     val result = transformations.foldLeft(program)((prog, transf) => transf.transform(prog))
     logger.debug {
       val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
@@ -312,6 +310,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
 
   private def performViperEncoding(config: Config, pkgInfo: PackageInfo, program: Program)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, BackendVerifier.Task] = {
     if (config.shouldViperEncode) {
+      logger.info(s"Phase 5/6: Viper encoding [${LocalTime.now().format(timeFormatter)}]")
       val startMs = System.currentTimeMillis()
       val res = EitherT.fromEither[Future, Vector[VerifierError], BackendVerifier.Task](Future.successful(Translator.translate(program, pkgInfo)(config)))
       logger.debug {
@@ -328,6 +327,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     if (config.noVerify) {
       Future(VerifierResult.Success)(executor)
     } else {
+      logger.info(s"Phase 6/6: backend verification [${LocalTime.now().format(timeFormatter)}]")
       verifyAst(config, pkgInfo, ast, backtrack)(executor)
     }
   }

src/main/scala/viper/gobra/ast/internal/Program.scala

@@ -19,7 +19,7 @@ import viper.gobra.reporting.Source.Parser
 import viper.gobra.theory.Addressability
 import viper.gobra.translator.Names
 import viper.gobra.util.{BackendAnnotation, Decimal, GoString, NumBase, TypeBounds, Violation}
-import viper.gobra.util.TypeBounds.{IntegerKind, UnboundedInteger, UntypedConstInteger}
+import viper.gobra.util.TypeBounds.{IntegerKind, UnboundedInteger}
 import viper.gobra.util.Violation.violation
 
 import scala.collection.SortedSet
@@ -996,8 +996,8 @@ case class MapKeys(exp : Expr, expUnderlyingType: Type)(val info : Source.Parser
 
 case class MapValues(exp : Expr, expUnderlyingType: Type)(val info : Source.Parser.Info) extends Expr {
   override val typ : Type = expUnderlyingType match {
-    case t: MathMapT => SetT(t.keys, Addressability.mathDataStructureElement)
-    case t: MapT => SetT(t.keys, Addressability.rValue)
+    case t: MathMapT => SetT(t.values, Addressability.mathDataStructureElement)
+    case t: MapT => SetT(t.values, Addressability.rValue)
     case _ => violation(s"unexpected type ${exp.typ}")
   }
 }
@@ -1105,14 +1105,15 @@ sealed abstract class BinaryIntExpr(override val operator: String) extends Binar
     // "kinds IntegerKind(integer) and IntegerKind(int) cannot be merged".
     case (IntT(_, kind1), IntT(_, kind2)) => IntT(Addressability.Exclusive, TypeBounds.mergeLenient(kind1, kind2))
 
-    // A binary expression may have one operand of a defined type T and another operand that is an unbounded
-    // integer or an untyped integer constant.
+    // A binary expression may have one operand of a defined type T and another operand that is an integer
+    // (of any kind: a conversion like `AS(v)` yields the underlying bounded kind, an untyped constant may
+    // have been assigned a concrete kind by the type-checker, and internally synthesized nodes are unbounded).
     // If T's underlying type is an integer type, then the result of the expression should be of type T.
     // Here, the underlying type of a defined type is not checked, as the information is not available at this point.
     // However, this should not pose a problem assuming that the original program has been type-checked before the
     // translation to the internal language.
-    case (x, IntT(_, UnboundedInteger | UntypedConstInteger)) if x.isInstanceOf[DefinedT] => x.withAddressability(Addressability.Exclusive)
-    case (IntT(_, UnboundedInteger | UntypedConstInteger), y) if y.isInstanceOf[DefinedT] => y.withAddressability(Addressability.Exclusive)
+    case (x: DefinedT, _: IntT) => x.withAddressability(Addressability.Exclusive)
+    case (_: IntT, y: DefinedT) => y.withAddressability(Addressability.Exclusive)
     case (x, y) if x.equalsWithoutMod(y) => x.withAddressability(Addressability.Exclusive)
     case (l, r) => violation(s"cannot merge types $l and $r")
 
@@ -1153,7 +1154,13 @@ case class ShiftLeft(left: Expr, right: Expr)(val info: Source.Parser.Info) exte
 case class ShiftRight(left: Expr, right: Expr)(val info: Source.Parser.Info) extends BinaryIntExpr(">>") {
   override val typ: Type = left.typ
 }
-case class BitNeg(op: Expr)(val info: Source.Parser.Info) extends IntOperation
+case class BitNeg(op: Expr)(val info: Source.Parser.Info) extends IntOperation {
+  // ^x has its operand's type. The inherited unbounded-Int typ would misreport the
+  // complement of a bounded operand: the encoding produces a domain-typed value for it,
+  // and enclosing operations decide based on this typ whether the value still needs the
+  // domain-to-Int projection.
+  override def typ: Type = op.typ.withAddressability(Addressability.rValue)
+}
 
 /*
  * Convert 'expr' to non-interface type 'newType'. If 'newType' is