Fix issue 651 (#652)

* Add bug witness * Add fix * Reflect that the order of fields matter in the signature of AdtClauseT * use more general type
viperproject · May 14, 2023 · 178f985 · 178f985
1 parent 3ce34f3
commit 178f985
Show file tree

Hide file tree

Showing 6 changed files with 36 additions and 6 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/info/base/Type.scala b/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")
 

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
@@ -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 {

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala b/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

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/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")

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala b/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

diff --git a/src/test/resources/regressions/issues/000651.gobra b/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}
+}