Merge branch 'master' into aggressive_chop

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/frontend/info/base/Type.scala

@@ -13,7 +13,7 @@ import viper.gobra.frontend.info.ExternalTypeInfo
 import viper.gobra.util.TypeBounds
 
 import scala.annotation.tailrec
-import scala.collection.immutable.ListMap
+import scala.collection.immutable.{ListMap, SeqMap}
 
 object Type {
 
@@ -58,7 +58,7 @@ 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(fields: SeqMap[String, Type], decl: PAdtClause, adtT: PAdtType, context: ExternalTypeInfo) extends Type
 
   case class MapT(key: Type, elem: Type) extends PrettyType(s"map[$key]$elem")
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

@@ -14,6 +14,8 @@ import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.util.TypeBounds.{BoundedIntegerKind, UnboundedInteger}
 import viper.gobra.util.{Constants, TypeBounds, Violation}
 
+import scala.collection.immutable.ListMap
+
 trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
 
   import viper.gobra.util.Violation._
@@ -145,7 +147,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
         case Some(p: ap.DomainFunction) => FunctionT(p.symb.args map p.symb.context.typ, p.symb.context.typ(p.symb.result))
 
         case Some(p: ap.AdtClause) =>
-          val fields = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)).toMap
+          val fields = ListMap.from(p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)))
           AdtClauseT(fields, p.symb.decl, p.symb.adtDecl, this)
         case Some(p: ap.AdtField) =>
           p.symb match {

src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala

@@ -14,6 +14,8 @@ import viper.gobra.frontend.info.base.Type._
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.property.{AssignMode, StrictAssignMode}
 
+import scala.collection.immutable.ListMap
+
 trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
 
   import viper.gobra.util.Violation._
@@ -157,7 +159,7 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
 
       // ADT clause is special since it is a type with a name that is not a named type
       case a: AdtClause =>
-        val types = a.fields.map(f => f.id.name -> a.context.symbType(f.typ)).toMap
+        val types = ListMap.from(a.fields.map(f => f.id.name -> a.context.symbType(f.typ)))
         AdtClauseT(types, a.decl, a.adtDecl, this)
 
       case BuiltInType(tag, _, _) => tag.typ

src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala

@@ -155,7 +155,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
 
         // ADT clause is special since it is a type with a name that is not a named type
         case Some(p: ap.AdtClause) =>
-          val types = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)).toMap
+          val types = ListMap.from(p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)))
           AdtClauseT(types, p.symb.decl, p.symb.adtDecl, p.symb.context)
 
         case _ => violation(s"expected type, but got $n")

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala

@@ -14,6 +14,7 @@ import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.util.Violation.violation
 
 import scala.annotation.unused
+import scala.collection.immutable.ListMap
 
 trait GhostIdTyping { this: TypeInfoImpl =>
 
@@ -42,7 +43,7 @@ trait GhostIdTyping { this: TypeInfoImpl =>
 
     case AdtClause(decl, adtDecl, context) =>
       AdtClauseT(
-        decl.args.flatMap(_.fields).map(f => f.id.name -> context.symbType(f.typ)).toMap,
+        ListMap.from(decl.args.flatMap(_.fields).map(f => f.id.name -> context.symbType(f.typ))),
         decl,
         adtDecl,
         context

src/test/resources/regressions/issues/000651.gobra

@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package test
+
+type A adt {
+	A_ {
+		a uint
+		b set[int]
+		c bool
+		d bool
+		e seq[int]
+	}
+}
+
+ghost
+decreases
+pure func f(x A) A {
+	return A_ {
+	a: x.a,
+	b: x.b,
+	c: x.c,
+	d: x.d,
+	e: x.e}
+}