Merges branch 'master' into 'pre-parse-unit-tests'

README.md

@@ -45,6 +45,28 @@ More information about the available options in Gobra can be found by running `r
 ### Running the Tests
 In the `gobra` directory, run the command `sbt test`.
 
+### Debugging
+By default, Gobra runs in sbt on a forked JVM. This means that simply attaching a debugger to sbt will not work. There
+are two workarounds:
+
+- Run Gobra in a non-forked JVM by first running `set fork := false` in sbt. This will allow you to attach a debugger to
+  sbt normally. However, for unknown reasons, this causes issues with class resolution in the Viper backend, so actually
+  only the parsing can really be debugged.
+- Attach the debugger to the forked JVM.
+  - Create a debug configuration in IntelliJ and specify to `Attach to remote JVM`, set `localhost` as host, and 
+     a port (e.g. 5005).
+  - Run `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=5005"`
+     in sbt (use any port you like, just make sure to use the same one in the debugger). Now, the forked JVM can be
+    debugged instead of the sbt JVM. This requires starting the debugger again every time a new VM is created,
+    e.g. for every `run`.
+- Let the debugger listen to the forked JVM.
+  - Create a debug configuration in IntelliJ and specify to `Listen to remote JVM`, enable auto restart, set
+    `localhost` as host, and a port (e.g. 5005).
+  - Run `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=n,address=localhost:5005,suspend=y"` in sbt.
+    Thanks to auto restart, the debugger keeps listening even when the JVM is restarted, e.g. for every `run`.
+    Note however that the debugger must be running/listening as otherwise the JVM will emit a connection 
+    refused error.
+
 ## Licensing
 Most Gobra sources are licensed under the Mozilla Public License Version 2.0.
 The [LICENSE](./LICENSE) lists the exceptions to this rule.

docs/tutorial.md

@@ -401,7 +401,7 @@ pure func toSeq(s []int) (res seq[int]) {
 
 Gobra supports many of Go's native types, namely integers (`int`, `int8`, `int16`, `int32`, `int64`, `byte`, `uint8`, `rune`, `uint16`, `uint32`, `uint64`, `uintptr`), strings, structs, pointers, arrays, slices, interfaces, and channels. Note that currently the support for strings and specific types of integers such as `rune` is very limited. 
 
-In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`|set1|`). 
+In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`len(set1)`). 
 
 
 ## Interfaces
@@ -680,4 +680,4 @@ java -Xss128m -jar gobra.jar -i [FILES_TO_VERIFY]
 To check the full list of flags available in Gobra, run the command
 ```bash
 java -jar gobra.jar -h
-```
+```

src/main/scala/viper/gobra/backend/ViperBackends.scala

@@ -6,7 +6,7 @@
 
 package viper.gobra.backend
 
-import viper.gobra.frontend.Config
+import viper.gobra.frontend.{Config, MCE}
 import viper.gobra.util.GobraExecutionContext
 import viper.server.ViperConfig
 import viper.server.core.ViperCoreServer
@@ -27,9 +27,12 @@ object ViperBackends {
       if (config.conditionalizePermissions) {
         options ++= Vector("--conditionalizePermissions")
       }
-      if (!config.disableMoreCompleteExhale) {
-        options ++= Vector("--enableMoreCompleteExhale")
+      val mceSiliconOpt = config.mceMode match {
+        case MCE.Disabled => "0"
+        case MCE.Enabled  => "1"
+        case MCE.OnDemand => "2"
       }
+      options ++= Vector(s"--exhaleMode=$mceSiliconOpt")
       if (config.assumeInjectivityOnInhale) {
         options ++= Vector("--assumeInjectivityOnInhale")
       }
@@ -78,7 +81,7 @@ object ViperBackends {
     /** returns an existing ViperCoreServer instance or otherwise creates a new one */
     protected def getOrCreateServer(config: Config)(executionContext: GobraExecutionContext): ViperCoreServer = {
       server.getOrElse({
-        var serverConfig = List("--logLevel", config.logLevel.levelStr)
+        var serverConfig = List("--disablePlugins", "--logLevel", config.logLevel.levelStr)
         if(config.cacheFile.isDefined) {
           serverConfig = serverConfig.appendedAll(List("--cacheFile", config.cacheFile.get.toString))
         }
@@ -100,9 +103,12 @@ object ViperBackends {
       var options: Vector[String] = Vector.empty
       options ++= Vector("--logLevel", "ERROR")
       options ++= Vector("--disableCatchingExceptions")
-      if (!config.disableMoreCompleteExhale) {
-        options ++= Vector("--enableMoreCompleteExhale")
+      val mceSiliconOpt = config.mceMode match {
+        case MCE.Disabled => "0"
+        case MCE.Enabled  => "1"
+        case MCE.OnDemand => "2"
       }
+      options ++= Vector(s"--exhaleMode=$mceSiliconOpt")
       if (config.assumeInjectivityOnInhale) {
         options ++= Vector("--assumeInjectivityOnInhale")
       }

src/main/scala/viper/gobra/frontend/Config.scala

@@ -65,13 +65,23 @@ object ConfigDefaults {
   lazy val DefaultAssumeInjectivityOnInhale: Boolean = true
   lazy val DefaultParallelizeBranches: Boolean = false
   lazy val DefaultConditionalizePermissions: Boolean = false
-  lazy val DefaultDisableMoreCompleteExhale: Boolean = false
+  lazy val DefaultMCEMode: MCE.Mode = MCE.Enabled
   lazy val DefaultEnableLazyImports: Boolean = false
   lazy val DefaultNoVerify: Boolean = false
   lazy val DefaultNoStreamErrors: Boolean = false
   lazy val DefaultParseAndTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel
 }
 
+// More-complete exhale modes
+object MCE {
+  sealed trait Mode
+  object Disabled extends Mode
+  // When running in `OnDemand`, mce will only be enabled when silicon retries a query.
+  // More information can be found in https://github.com/viperproject/silicon/pull/682.
+  object OnDemand extends Mode
+  object Enabled extends Mode
+}
+
 case class Config(
                    gobraDirectory: Path = ConfigDefaults.DefaultGobraDirectory,
                    // Used as an identifier of a verification task, ideally it shouldn't change between verifications
@@ -117,7 +127,7 @@ case class Config(
                    // branches will be verified in parallel
                    parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches,
                    conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions,
-                   disableMoreCompleteExhale: Boolean = ConfigDefaults.DefaultDisableMoreCompleteExhale,
+                   mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode,
                    enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                    noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
                    noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
@@ -164,7 +174,7 @@ case class Config(
       assumeInjectivityOnInhale = assumeInjectivityOnInhale || other.assumeInjectivityOnInhale,
       parallelizeBranches = parallelizeBranches,
       conditionalizePermissions = conditionalizePermissions,
-      disableMoreCompleteExhale = disableMoreCompleteExhale,
+      mceMode = mceMode,
       enableLazyImports = enableLazyImports || other.enableLazyImports,
       noVerify = noVerify || other.noVerify,
       noStreamErrors = noStreamErrors || other.noStreamErrors,
@@ -215,7 +225,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       assumeInjectivityOnInhale: Boolean = ConfigDefaults.DefaultAssumeInjectivityOnInhale,
                       parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches,
                       conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions,
-                      disableMoreCompleteExhale: Boolean = ConfigDefaults.DefaultDisableMoreCompleteExhale,
+                      mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode,
                       enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                       noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
                       noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
@@ -270,7 +280,7 @@ trait RawConfig {
     assumeInjectivityOnInhale = baseConfig.assumeInjectivityOnInhale,
     parallelizeBranches = baseConfig.parallelizeBranches,
     conditionalizePermissions = baseConfig.conditionalizePermissions,
-    disableMoreCompleteExhale = baseConfig.disableMoreCompleteExhale,
+    mceMode = baseConfig.mceMode,
     enableLazyImports = baseConfig.enableLazyImports,
     noVerify = baseConfig.noVerify,
     noStreamErrors = baseConfig.noStreamErrors,
@@ -618,12 +628,23 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     short = 'c',
   )
 
-  val disableMoreCompleteExhale: ScallopOption[Boolean] = opt[Boolean](
-    name = "disableMoreCompleteExhale",
-    descr = "Disables the flag --enableMoreCompleteExhale passed by default to Silicon",
-    default = Some(ConfigDefaults.DefaultDisableMoreCompleteExhale),
-    noshort = true,
-  )
+  val mceMode: ScallopOption[MCE.Mode] = {
+    val on = "on"
+    val off = "off"
+    val od = "od"
+    choice(
+      choices = Seq("on", "off", "od"),
+      name = "mceMode",
+      descr = s"Specifies if silicon should be run with more complete exhale enabled ($on), disabled ($off), or enabled on demand ($od).",
+      default = Some(on),
+      noshort = true
+    ).map{
+      case `on` => MCE.Enabled
+      case `off` => MCE.Disabled
+      case `od` => MCE.OnDemand
+      case s => Violation.violation(s"Unexpected mode for more complete exhale: $s")
+    }
+  }
 
   val enableLazyImports: ScallopOption[Boolean] = opt[Boolean](
     name = Config.enableLazyImportOptionName,
@@ -705,11 +726,11 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     }
   }
 
-  // `disableMoreCompleteExhale` can only be enabled when using a silicon-based backend
+  // `mceMode` can only be provided when using a silicon-based backend
   addValidation {
-    val disableMoreCompleteExh = disableMoreCompleteExhale.toOption.contains(true)
-    if (disableMoreCompleteExh && !isSiliconBasedBackend) {
-      Left("The flag --disableMoreCompleteExhale can only be used with Silicon and ViperServer with Silicon")
+    val mceModeSupplied = mceMode.isSupplied
+    if (mceModeSupplied && !isSiliconBasedBackend) {
+      Left("The flag --mceMode can only be used with Silicon or ViperServer with Silicon")
     } else {
       Right(())
     }
@@ -801,7 +822,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     assumeInjectivityOnInhale = assumeInjectivityOnInhale(),
     parallelizeBranches = parallelizeBranches(),
     conditionalizePermissions = conditionalizePermissions(),
-    disableMoreCompleteExhale = disableMoreCompleteExhale(),
+    mceMode = mceMode(),
     enableLazyImports = enableLazyImports(),
     noVerify = noVerify(),
     noStreamErrors = noStreamErrors(),

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -1838,7 +1838,7 @@ object Desugar extends LazyLogging {
             } yield in.Seqn(Vector(dPre, exprAss, clauseBody))(src)
 
           case n: POutline =>
-            val name = s"${rootName(n, info)}$$${nm.relativeId(n, info)}"
+            val name = s"${rootName(n, info)}$$${nm.relativeIdEnclosingFuncOrMethodDecl(n, info)}"
             val pres = (n.spec.pres ++ n.spec.preserves) map preconditionD(ctx, info)
             val posts = (n.spec.preserves ++ n.spec.posts) map postconditionD(ctx, info)
             val terminationMeasures = sequence(n.spec.terminationMeasures map terminationMeasureD(ctx, info)).res
@@ -3768,7 +3768,7 @@ object Desugar extends LazyLogging {
       case t: Type.AdtClauseT =>
         val tAdt = Type.AdtT(t.adtT, t.context)
         val adt: in.AdtT = in.AdtT(nm.adt(tAdt), addrMod)
-        val fields: Vector[in.Field] = (t.fields map { case (key: String, typ: Type) =>
+        val fields: Vector[in.Field] = (t.fieldsWithTypes map { case (key: String, typ: Type) =>
           in.Field(nm.adtField(key, tAdt), typeD(typ, Addressability.mathDataStructureElement)(src), true)(src)
         }).toVector
         in.AdtClauseT(idName(t.decl.id, t.context.getTypeInfo), adt, fields, addrMod)
@@ -3840,6 +3840,13 @@ object Desugar extends LazyLogging {
         case decl: PMethodSig      => idName(decl.id, context)
         case decl: PMPredicateSig  => idName(decl.id, context)
         case decl: PDomainFunction => idName(decl.id, context)
+        case decl: PClosureDecl =>
+          // closure declarations do not have an associated name and may be arbitrarily nested.
+          // to simplify, we just return the enclosing function or method's name
+          info.enclosingFunctionOrMethod(decl) match {
+            case Some(d) => idName(d.id, context)
+            case None => violation(s"Could not find a function or method declaration enclosing the closure declaration.")
+          }
         case _ => ??? // axiom and method-implementation-proof
       }
     }
@@ -4884,7 +4891,7 @@ object Desugar extends LazyLogging {
       * The id is of the form 'L$<a>$<b>' where a is the difference of the lines
       * of the node with the code root and b is the difference of the columns
       * of the node with the code root.
-      * If a differce is negative, the '-' character is replaced with '_'.
+      * If the difference is negative, the '-' character is replaced with '_'.
       *
       * @param node the node we are interested in
       * @param info type info to get position information
@@ -4897,6 +4904,25 @@ object Desugar extends LazyLogging {
       ("L$" + (lpos.line - rpos.line) + "$" + (lpos.column - rpos.column)).replace("-", "_")
     }
 
+    /**
+      * Returns an id for a node with respect to its enclosing function or method declaration.
+      * The id is of the form 'L$<a>$<b>' where a is the difference of the lines
+      * of the node with the enclosing declaration and b is the difference of the columns
+      * of the node with the enclosing declaration.
+      * If the difference is negative, the '-' character is replaced with '_'.
+      *
+      * @param node the node we are interested in
+      * @param info type info to get position information
+      * @return     string
+      */
+    def relativeIdEnclosingFuncOrMethodDecl(node: PNode, info: TypeInfo) : String = {
+      val pom = info.getTypeInfo.tree.originalRoot.positions
+      val lpos = pom.positions.getStart(node).get
+      val enclosingMember = info.enclosingFunctionOrMethod(node).get
+      val rpos = pom.positions.getStart(enclosingMember).get
+      ("L$" + (lpos.line - rpos.line) + "$" + (lpos.column - rpos.column)).replace("-", "_")
+    }
+
     /** returns the relativeId with the CONTINUE_LABEL_SUFFIX appended */
     def continueLabel(loop: PGeneralForStmt, info: TypeInfo) : String = relativeId(loop, info) + CONTINUE_LABEL_SUFFIX
 

src/main/scala/viper/gobra/frontend/info/base/Type.scala

@@ -58,7 +58,17 @@ object Type {
 
   case class AdtT(decl: PAdtType, context: ExternalTypeInfo) extends Type
 
-  case class AdtClauseT(fields: Map[String, Type], decl: PAdtClause, adtT: PAdtType, context: ExternalTypeInfo) extends Type
+  case class AdtClauseT(fieldsToTypes: Map[String, Type], fields: Vector[String], decl: PAdtClause, adtT: PAdtType, context: ExternalTypeInfo) extends Type {
+    require(fields.forall(fieldsToTypes.isDefinedAt), "there must be a type for each key")
+
+    def typeAt(idx: Int): Type = {
+      require(0 <= idx && idx < fields.size, s"index $idx is not within range of ADT fields (size ${fields.size})")
+      fieldsToTypes(fields(idx))
+    }
+
+    lazy val fieldsWithTypes: Vector[(String, Type)] = fields.map(f => (f, fieldsToTypes(f)))
+    lazy val fieldTypes: Vector[Type] = fieldsWithTypes.map(_._2)
+  }
 
   case class MapT(key: Type, elem: Type) extends PrettyType(s"map[$key]$elem")
 

src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala

@@ -184,7 +184,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl =>
           if (elems.isEmpty) {
             successProp
           } else if (elems.exists(_.key.nonEmpty)) {
-            val tmap: Map[String, Type] = a.fields
+            val tmap: Map[String, Type] = a.fieldsToTypes
 
             failedProp("for adt literals either all or none elements must be keyed",
               !elems.forall(_.key.nonEmpty)) and
@@ -198,7 +198,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl =>
               })
           } else if (elems.size == a.fields.size) {
             propForall(
-              elems.map(_.exp).zip(a.fields.values),
+              elems.map(_.exp).zip(a.fieldTypes),
               compositeValAssignableTo
             )
           } else {

src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala

@@ -20,6 +20,8 @@ trait Convertibility extends BaseProperty { this: TypeInfoImpl =>
       case (left, right) if assignableTo(left, right) => true
       case (IntT(_), Float32T) => true
       case (IntT(_), Float64T) => true
+      case (Float32T, IntT(_)) => true
+      case (Float64T, IntT(_)) => true
       case (IntT(_), IntT(_)) => true
       case (SliceT(IntT(config.typeBounds.Byte)), StringT) => true
       case (StringT, SliceT(IntT(config.typeBounds.Byte))) => true

src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala

@@ -6,6 +6,7 @@
 
 package viper.gobra.frontend.info.implementation.property
 
+import viper.gobra.ast.internal.{Float32T, Float64T}
 import viper.gobra.frontend.info.base.Type.{AdtClauseT, AdtT, ArrayT, ChannelT, GhostSliceT, IntT, InternalSingleMulti, InternalTupleT, MapT, MultisetT, PermissionT, PointerT, SequenceT, SetT, Single, SliceT, Type}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
@@ -23,6 +24,10 @@ trait TypeMerging extends BaseProperty { this: TypeInfoImpl =>
           (lst, rst) match {
             case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[IntT] => Some(a)
             case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[IntT] => Some(b)
+            case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[Float64T] => Some(a)
+            case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[Float64T] => Some(b)
+            case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[Float32T] => Some(a)
+            case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[Float32T] => Some(b)
             case (IntT(_), PermissionT) => Some(PermissionT)
             case (PermissionT, IntT(_)) => Some(PermissionT)
             case (SequenceT(l), SequenceT(r)) => typeMerge(l,r) map SequenceT

src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala

@@ -94,9 +94,12 @@ trait NameResolution {
 
           case tree.parent.pair(decl: PAdtClause, adtDecl: PAdtType) => AdtClause(decl, adtDecl, this)
 
-          case tree.parent.pair(decl: PMatchBindVar, adt: PMatchAdt) => MatchVariable(decl, adt, this)
           case tree.parent.pair(decl: PMatchBindVar, tree.parent.pair(_: PMatchStmtCase, matchE: PMatchStatement)) =>
-            MatchVariable(decl, matchE.exp, this)
+            MatchVariable(decl, matchE.exp, this) // match full expression of match statement
+          case tree.parent.pair(decl: PMatchBindVar, tree.parent.pair(_: PMatchExpCase, matchE: PMatchExp)) =>
+            MatchVariable(decl, matchE.exp, this) // match full expression of match expression
+          case tree.parent.pair(decl: PMatchBindVar, adt: PMatchAdt) =>
+            MatchVariable(decl, adt, this) // match part of subexpression
 
           case c => Violation.violation(s"This case should be unreachable, but got $c")
         }