Support for Ghost Fields

src/main/antlr4/GobraParser.g4

@@ -157,6 +157,12 @@ ghostSliceType: GHOST L_BRACKET R_BRACKET elementType;
 
 ghostPointerType: GPOINTER L_BRACKET elementType R_BRACKET;
 
+// copy of `fieldDecl` from GoParser.g4 extended with an optional `GHOST` modifier for fields and embedded fields:
+fieldDecl: GHOST? (
+		identifierList type_
+		| embeddedField
+	) tag = string_?;
+
 sqType: (kind=(SEQ | SET | MSET | OPT) L_BRACKET type_ R_BRACKET)
     | kind=DICT L_BRACKET type_ R_BRACKET type_;
 

src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java

@@ -369,6 +369,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitGhostPointerType(GobraParser.GhostPointerTypeContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitFieldDecl(GobraParser.FieldDeclContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -1531,13 +1538,6 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitStructType(GobraParser.StructTypeContext ctx) { return visitChildren(ctx); }
-	/**
-	 * {@inheritDoc}
-	 *
-	 * <p>The default implementation returns the result of calling
-	 * {@link #visitChildren} on {@code ctx}.</p>
-	 */
-	@Override public T visitFieldDecl(GobraParser.FieldDeclContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *

src/main/java/viper/gobra/frontend/GobraParserVisitor.java

@@ -320,6 +320,12 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitGhostPointerType(GobraParser.GhostPointerTypeContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#fieldDecl}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitFieldDecl(GobraParser.FieldDeclContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#sqType}.
 	 * @param ctx the parse tree
@@ -1350,12 +1356,6 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitStructType(GobraParser.StructTypeContext ctx);
-	/**
-	 * Visit a parse tree produced by {@link GobraParser#fieldDecl}.
-	 * @param ctx the parse tree
-	 * @return the visitor result
-	 */
-	T visitFieldDecl(GobraParser.FieldDeclContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#string_}.
 	 * @param ctx the parse tree

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

@@ -2938,7 +2938,7 @@ object Desugar extends LazyLogging {
         case MemberPath.Deref => in.Deref(e, underlyingType(e.typ))(pinfo)
         case MemberPath.Ref => in.Ref(e)(pinfo)
         case MemberPath.Next(g) =>
-          in.FieldRef(e, embeddedDeclD(g.decl, Addressability.fieldLookup(e.typ.addressability), g.context)(pinfo))(pinfo)
+          in.FieldRef(e, embeddedDeclD(g.decl, Addressability.fieldLookup(e.typ.addressability), g.ghost, g.context)(pinfo))(pinfo)
         case _: MemberPath.EmbeddedInterface => e
       }}
     }
@@ -4025,36 +4025,36 @@ object Desugar extends LazyLogging {
 
     def structD(struct: StructT, addrMod: Addressability)(src: Meta): Vector[in.Field] =
       struct.clauses.map {
-        case (name, (true, typ)) => fieldDeclD((name, typ), Addressability.field(addrMod), struct)(src)
-        case (name, (false, typ)) => embeddedDeclD((name, typ), Addressability.field(addrMod), struct)(src)
+        case (name, t: StructFieldT) => fieldDeclD((name, t), Addressability.field(addrMod), struct)(src)
+        case (name, t: StructEmbeddedT) => embeddedDeclD((name, t), Addressability.field(addrMod), struct)(src)
       }.toVector
 
     def structMemberD(m: st.StructMember, addrMod: Addressability)(src: Meta): in.Field = m match {
-      case st.Field(decl, _, context) => fieldDeclD(decl, addrMod, context)(src)
-      case st.Embbed(decl, _, context) => embeddedDeclD(decl, addrMod, context)(src)
+      case st.Field(decl, isGhost, context) => fieldDeclD(decl, addrMod, isGhost, context)(src)
+      case st.Embbed(decl, isGhost, context) => embeddedDeclD(decl, addrMod, isGhost, context)(src)
     }
 
-    def embeddedDeclD(embedded: (String, Type), fieldAddrMod: Addressability, struct: StructT)(src: Source.Parser.Info): in.Field = {
+    def embeddedDeclD(embedded: (String, StructEmbeddedT), fieldAddrMod: Addressability, struct: StructT)(src: Source.Parser.Info): in.Field = {
       val idname = nm.field(embedded._1, struct)
-      val td = typeD(embedded._2, fieldAddrMod)(src)
-      in.Field(idname, td, ghost = false)(src) // TODO: fix ghost attribute
+      val td = typeD(embedded._2.typ, fieldAddrMod)(src)
+      in.Field(idname, td, ghost = embedded._2.isGhost)(src)
     }
 
-    def embeddedDeclD(decl: PEmbeddedDecl, addrMod: Addressability, context: ExternalTypeInfo)(src: Meta): in.Field = {
+    def embeddedDeclD(decl: PEmbeddedDecl, addrMod: Addressability, isGhost: Boolean, context: ExternalTypeInfo)(src: Meta): in.Field = {
       val struct = context.struct(decl)
-      val embedded: (String, Type) = (decl.id.name, context.typ(decl.typ))
+      val embedded: (String, StructEmbeddedT) = (decl.id.name, StructEmbeddedT(context.typ(decl.typ), isGhost))
       embeddedDeclD(embedded, addrMod, struct.get)(src)
     }
 
-    def fieldDeclD(field: (String, Type), fieldAddrMod: Addressability, struct: StructT)(src: Source.Parser.Info): in.Field = {
+    def fieldDeclD(field: (String, StructFieldT), fieldAddrMod: Addressability, struct: StructT)(src: Source.Parser.Info): in.Field = {
       val idname = nm.field(field._1, struct)
-      val td = typeD(field._2, fieldAddrMod)(src)
-      in.Field(idname, td, ghost = false)(src) // TODO: fix ghost attribute
+      val td = typeD(field._2.typ, fieldAddrMod)(src)
+      in.Field(idname, td, ghost = field._2.isGhost)(src)
     }
 
-    def fieldDeclD(decl: PFieldDecl, addrMod: Addressability, context: ExternalTypeInfo)(src: Meta): in.Field = {
+    def fieldDeclD(decl: PFieldDecl, addrMod: Addressability, isGhost: Boolean, context: ExternalTypeInfo)(src: Meta): in.Field = {
       val struct = context.struct(decl)
-      val field: (String, Type) = (decl.id.name, context.symbType(decl.typ))
+      val field: (String, StructFieldT) = (decl.id.name, StructFieldT(context.symbType(decl.typ), isGhost))
       fieldDeclD(field, addrMod, struct.get)(src)
     }
 

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

@@ -301,14 +301,16 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     * {@link #visitChildren} on {@code ctx}.</p>
     */
   override def visitFieldDecl(ctx: FieldDeclContext): PStructClause = {
-    if (ctx.embeddedField() != null) {
+    val ghost = has(ctx.GHOST())
+    val actualDecl = if (ctx.embeddedField() != null) {
       val et = visitNode[PEmbeddedType](ctx.embeddedField())
       PEmbeddedDecl(et, PIdnDef(et.name).at(et))
     } else {
       val goIdnDefList(ids) = visitIdentifierList(ctx.identifierList())
       val t = visitNode[PType](ctx.type_())
       PFieldDecls(ids map (id => PFieldDecl(id, t.copy).at(id)))
     }
+    if (ghost) PExplicitGhostStructClause(actualDecl).at(ctx) else actualDecl
   }
 
   /**

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

@@ -99,15 +99,30 @@ object Type {
     case object Send extends ChannelModus("chan<-")
   }
 
-  case class StructT(clauses: ListMap[String, (Boolean, Type)], decl: PStructType, context: ExternalTypeInfo) extends ContextualType {
-    lazy val fieldsAndEmbedded: ListMap[String, Type] = clauses.map(removeFieldIndicator)
-    lazy val fields: ListMap[String, Type] = clauses.filter(isField).map(removeFieldIndicator)
-    lazy val embedded: ListMap[String, Type] = clauses.filterNot(isField).map(removeFieldIndicator)
-    private def isField(clause: (String, (Boolean, Type))): Boolean = clause._2._1
-    private def removeFieldIndicator(clause: (String, (Boolean, Type))): (String, Type) = (clause._1, clause._2._2)
+  trait StructClauseT {
+    def typ: Type
+    def isGhost: Boolean
+    override lazy val toString: String = typ.toString
+  }
+
+  case class StructFieldT(typ: Type, isGhost: Boolean) extends StructClauseT
+
+  case class StructEmbeddedT(typ: Type, isGhost: Boolean) extends StructClauseT
+
+  case class StructT(clauses: ListMap[String, StructClauseT], decl: PStructType, context: ExternalTypeInfo) extends ContextualType {
+    lazy val fieldsAndEmbedded: ListMap[String, Type] = clauses.map(extractTyp)
+    lazy val fields: ListMap[String, Type] = clauses.filter(isField).map(extractTyp)
+    lazy val embedded: ListMap[String, Type] = clauses.filterNot(isField).map(extractTyp)
+
+    private def isField(clause: (String, StructClauseT)): Boolean = clause._2 match {
+      case _: StructFieldT => true
+      case _ => false
+    }
+
+    private def extractTyp(clause: (String, StructClauseT)): (String, Type) = (clause._1, clause._2.typ)
 
     override lazy val toString: String = {
-      val fields = clauses.map{ case (n, (_, t)) => s"$n: $t" }
+      val fields = clauses.map { case (n, i) => s"$n: $i" }
       s"struct{ ${fields.mkString("; ")}}"
     }
   }

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

@@ -94,7 +94,7 @@ trait Implements { this: TypeInfoImpl =>
     failedProp(s"The type $t is not supported for interface", !isIdentityPreservingType(t))
   }
 
-  /** Returns whether values of type 't' satisfy that [x] == [y] in Viper implies x == y in Gobra. */
+  /** Returns whether values of type 't' satisfy that [x] == [y] in Viper (using `TypeEncoding.equal`) <==> x == y in Go (using Go equality). */
   private def isIdentityPreservingType(t: Type, encounteredTypes: Set[Type] = Set.empty): Boolean = {
     if (encounteredTypes contains t) {
       true
@@ -104,7 +104,9 @@ trait Implements { this: TypeInfoImpl =>
         case Type.NilType | Type.BooleanT | _: Type.IntT | Type.StringT => true
         case ut: Type.PointerT => go(ut.elem)
         case ut: Type.StructT =>
-          ut.clauses.forall{ case (_, (_, fieldType)) => go(fieldType) }
+          // a struct with ghost fields or ghost embeddings is not identity preserving.
+          // E.g., for `type S struct { val int, ghost gval int }`, `S{0, 0} == S{0, 42}` holds in Go (after erasing the ghost fields).
+          ut.clauses.forall{ case (_, info) => !info.isGhost && go(info.typ) }
         case ut: Type.ArrayT => go(ut.elem)
         case _: Type.SliceT => true
         case _: Type.MapT => true

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

@@ -42,7 +42,11 @@ trait TypeIdentity extends BaseProperty { this: TypeInfoImpl =>
 
       case (StructT(clausesL, _, contextL), StructT(clausesR, _, contextR)) =>
         contextL == contextR && clausesL.size == clausesR.size && clausesL.zip(clausesR).forall {
-          case (lm, rm) => lm._1 == rm._1 && lm._2._1 == rm._2._1 && identicalTypes(lm._2._2, rm._2._2)
+          case ((lId, lc), (rId, rc)) => lId == rId && identicalTypes(lc.typ, rc.typ) && ((lc, rc) match {
+            case (_: StructFieldT, _: StructFieldT) => true
+            case (_: StructEmbeddedT, _: StructEmbeddedT) => true
+            case _ => false
+          })
         }
 
       case (l: InterfaceT, r: InterfaceT) =>

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

@@ -65,6 +65,9 @@ class AdvancedMemberSet[M <: TypeMember] private(
   def forall(f: (String, (M, Vector[MemberPath])) => Boolean): Boolean =
     internal.forall{ case (s, (m, p, _)) => f(s, (m,p)) }
 
+  def exists(f: (String, (M, Vector[MemberPath])) => Boolean): Boolean =
+    internal.exists{ case (s, (m, p, _)) => f(s, (m,p)) }
+
   def map[T](f: (String, (M, Vector[MemberPath])) => T): Vector[T] = internal.map {
     case (s, (m, p, _)) => f(s, (m,p))
   }.toVector

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

@@ -11,6 +11,7 @@ import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages
 import scala.collection.immutable.ListMap
 import viper.gobra.ast.frontend._
 import viper.gobra.ast.frontend.{AstPattern => ap}
+import viper.gobra.frontend.info.base.SymbolTable.{Embbed, Field}
 import viper.gobra.frontend.info.base.Type.{StructT, _}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.property.UnderlyingType
@@ -55,7 +56,8 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
     case _: PPredType => noMessages // well definedness implied by well definedness of children
 
     case n@ PMapType(key, elem) => isType(key).out ++ isType(elem).out ++
-      error(n, s"map key $key is not comparable", !comparableType(typeSymbType(key)))
+      error(n, s"map key $key is not comparable", !comparableType(typeSymbType(key))) ++
+      error(n, s"map key $key cannot contain ghost fields", isStructTypeWithGhostFields(typeSymbType(key)))
 
     case t: PStructType =>
       t.embedded.flatMap(e => isNotPointerTypePE.errors(e.typ)(e)) ++
@@ -75,6 +77,20 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
     case t: PExpressionAndType => wellDefExprAndType(t).out ++ isType(t).out
   }
 
+  def isStructTypeWithGhostFields(t: Type): Boolean = t match {
+    case Single(st) => underlyingType(st) match {
+      case t: StructT =>
+        structMemberSet(t).exists {
+          case (_, (f: Field, _)) => f.ghost || isStructTypeWithGhostFields(f.context.symbType(f.decl.typ))
+          case (_, (e: Embbed, _)) => e.ghost || isStructTypeWithGhostFields(e.context.typ(e.decl.typ))
+          case _ => false
+        }
+
+      case _ => false
+    }
+    case _ => false
+  }
+
   lazy val typeSymbType: Typing[PType] = {
     // TODO: currently, this is required in order for Gobra to handle type alias to types from another package. This
     //       should be eventually generalized to all typing operations.
@@ -164,17 +180,19 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
   }
 
   private def structSymbType(t: PStructType): Type = {
-    def makeFields(x: PFieldDecls): ListMap[String, (Boolean, Type)] = {
-      x.fields.foldLeft(ListMap[String, (Boolean, Type)]()) { case (prev, f) => prev + (f.id.name -> (true, typeSymbType(f.typ))) }
+    def infoFromFieldDecl(f: PFieldDecl, isGhost: Boolean): StructFieldT = StructFieldT(typeSymbType(f.typ), isGhost)
+
+    def makeFields(x: PFieldDecls, isGhost: Boolean): ListMap[String, StructClauseT] = {
+      x.fields.foldLeft(ListMap[String, StructClauseT]()) { case (prev, f) => prev + (f.id.name -> infoFromFieldDecl(f, isGhost)) }
     }
-    def makeEmbedded(x: PEmbeddedDecl): ListMap[String, (Boolean, Type)] =
-      ListMap[String, (Boolean, Type)](x.id.name -> (false, miscType(x.typ)))
-
-    val clauses = t.clauses.foldLeft(ListMap[String, (Boolean, Type)]()) {
-      case (prev, x: PFieldDecls) => prev ++ makeFields(x)
-      case (prev, PExplicitGhostStructClause(x: PFieldDecls)) => prev ++ makeFields(x)
-      case (prev, x: PEmbeddedDecl) => prev ++ makeEmbedded(x)
-      case (prev, PExplicitGhostStructClause(x: PEmbeddedDecl)) => prev ++ makeEmbedded(x)
+    def makeEmbedded(x: PEmbeddedDecl, isGhost: Boolean): ListMap[String, StructClauseT] =
+      ListMap(x.id.name -> StructEmbeddedT(miscType(x.typ), isGhost))
+
+    val clauses = t.clauses.foldLeft(ListMap[String, StructClauseT]()) {
+      case (prev, x: PFieldDecls) => prev ++ makeFields(x, isGhost = false)
+      case (prev, PExplicitGhostStructClause(x: PFieldDecls)) => prev ++ makeFields(x, isGhost = true)
+      case (prev, x: PEmbeddedDecl) => prev ++ makeEmbedded(x, isGhost = false)
+      case (prev, PExplicitGhostStructClause(x: PEmbeddedDecl)) => prev ++ makeEmbedded(x, isGhost = true)
     }
     StructT(clauses, t, this)
   }

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

@@ -12,6 +12,7 @@ import viper.gobra.frontend.info.base.Type
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.ast.frontend.{AstPattern => ap}
 import viper.gobra.frontend.info.implementation.property.{AssignMode, StrictAssignMode}
+import viper.gobra.frontend.info.implementation.resolution.MemberPath
 import viper.gobra.util.Violation
 
 trait GhostTyping extends GhostClassifier { this: TypeInfoImpl =>
@@ -140,8 +141,12 @@ trait GhostTyping extends GhostClassifier { this: TypeInfoImpl =>
       case e: PDot => resolve(e) match {
         case Some(s: ap.FieldSelection) =>
           val isGhostField = ghostIdClassification(s.id)
-          (underlyingType(typ(s.base)), isGhostField) match {
-            case (_, true) => isGhost // ghost fields are always ghost memory
+          val isGhostEmbedding = s.path.exists {
+            case MemberPath.Next(decl) => decl.ghost
+            case _ => false
+          }
+          (underlyingType(typ(s.base)), isGhostField || isGhostEmbedding) match {
+            case (_, true) => isGhost // ghost fields and ghost embeddings are always ghost memory
             case (tb: Type.PointerT, _) => ghost(tb.isInstanceOf[Type.GhostPointerT]) // (implicitly) dereferencing a field of a ghost pointer leads to a ghost heap location
             case _ => ghostLocationTyping(s.base) // assignee is on the stack, recurse to find out if it's a ghost or actual variable
           }

src/main/scala/viper/gobra/translator/Names.scala

@@ -85,7 +85,7 @@ object Names {
   }
 
   def serializeFields(fields: Vector[in.Field]): String = {
-    val serializedFields = fields.map(f => s"${f.name}_${serializeType(f.typ)}").mkString("_")
+    val serializedFields = fields.map(f => s"${f.name}_${serializeType(f.typ)}_${if (f.ghost) "g" else "a"}").mkString("_")
     // we use a dollar sign to mark the beginning and end of the type list to avoid that `Tuple(Tuple(X), Y)` and `Tuple(Tuple(X, Y))` map to the same name:
     s"$$$serializedFields$$"
   }