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/backend/ViperBackends.scala

@@ -41,9 +41,7 @@ object ViperBackends {
       if (config.unsafeWildcardOptimization) {
         options ++= Vector(s"--unsafeWildcardOptimization")
       }
-      if (config.enableMoreJoins) {
-        options ++= Vector(s"--moreJoins")
-      }
+      options ++= Vector(s"--moreJoins=${config.moreJoins.viperValue}")
       val mceSiliconOpt = config.mceMode match {
         case MCE.Disabled => "0"
         case MCE.Enabled  => "1"
@@ -149,9 +147,7 @@ object ViperBackends {
       if (config.unsafeWildcardOptimization) {
         options ++= Vector(s"--unsafeWildcardOptimization")
       }
-      if (config.enableMoreJoins) {
-        options ++= Vector(s"--moreJoins")
-      }
+      options ++= Vector(s"--moreJoins=${config.moreJoins.viperValue}")
       val mceSiliconOpt = config.mceMode match {
         case MCE.Disabled => "0"
         case MCE.Enabled  => "1"

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

@@ -76,7 +76,7 @@ object ConfigDefaults {
   val DefaultDisableSetAxiomatization: Boolean = false
   val DefaultDisableCheckTerminationPureFns: Boolean = false
   val DefaultUnsafeWildcardOptimization: Boolean = false
-  val DefaultEnableMoreJoins: Boolean = false
+  val DefaultMoreJoins: MoreJoins.Mode = MoreJoins.Disabled
 }
 
 // More-complete exhale modes
@@ -89,6 +89,31 @@ object MCE {
   object Enabled extends Mode
 }
 
+object MoreJoins {
+  sealed trait Mode {
+    // Option number used by Viper, as described in
+    // https://github.com/viperproject/silicon/pull/823
+    def viperValue: Int
+  }
+  object Disabled extends Mode {
+    override val viperValue = 0
+  }
+  object Impure extends Mode {
+    override val viperValue = 1
+  }
+  object All extends Mode {
+    override val viperValue = 2
+  }
+
+  def merge(m1: Mode, m2: Mode): Mode = {
+    (m1, m2) match  {
+      case (All, _) | (_, All) => All
+      case (Impure, _) | (_, Impure) => Impure
+      case _ => Disabled
+    }
+  }
+}
+
 case class Config(
                    gobraDirectory: Path = ConfigDefaults.DefaultGobraDirectory,
                    // Used as an identifier of a verification task, ideally it shouldn't change between verifications
@@ -146,7 +171,7 @@ case class Config(
                    disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization,
                    disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
                    unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
-                   enableMoreJoins: Boolean = ConfigDefaults.DefaultEnableMoreJoins,
+                   moreJoins: MoreJoins.Mode = ConfigDefaults.DefaultMoreJoins,
 
 ) {
 
@@ -201,7 +226,7 @@ case class Config(
       disableSetAxiomatization = disableSetAxiomatization || other.disableSetAxiomatization,
       disableCheckTerminationPureFns = disableCheckTerminationPureFns || other.disableCheckTerminationPureFns,
       unsafeWildcardOptimization = unsafeWildcardOptimization && other.unsafeWildcardOptimization,
-      enableMoreJoins = enableMoreJoins || other.enableMoreJoins,
+      moreJoins = MoreJoins.merge(moreJoins, other.moreJoins),
     )
   }
 
@@ -259,7 +284,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization,
                       disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
                       unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
-                      enableMoreJoins: Boolean = ConfigDefaults.DefaultEnableMoreJoins,
+                      moreJoins: MoreJoins.Mode = ConfigDefaults.DefaultMoreJoins,
                      ) {
   def shouldParse: Boolean = true
   def shouldTypeCheck: Boolean = !shouldParseOnly
@@ -321,7 +346,7 @@ trait RawConfig {
     disableSetAxiomatization = baseConfig.disableSetAxiomatization,
     disableCheckTerminationPureFns = baseConfig.disableCheckTerminationPureFns,
     unsafeWildcardOptimization = baseConfig.unsafeWildcardOptimization,
-    enableMoreJoins = baseConfig.enableMoreJoins,
+    moreJoins = baseConfig.moreJoins,
   )
 }
 
@@ -686,12 +711,23 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     noshort = true
   )
 
-  val enableMoreJoins: ScallopOption[Boolean] = opt[Boolean](
-    name = "moreJoins",
-    descr = "Enable more joins using a more complete implementation of state merging.",
-    default = Some(false),
-    noshort = true
-  )
+  val moreJoins: ScallopOption[MoreJoins.Mode] = {
+    val all = "all"
+    val impure = "impure"
+    val off = "off"
+    choice(
+      choices = Seq("all", "impure", "off"),
+      name = "moreJoins",
+      descr = s"Specifies if silicon should be run with more joins completely enabled ($all), disabled ($off), or only for impure conditionals ($impure).",
+      default = Some(off),
+      noshort = true
+    ).map {
+      case `all` => MoreJoins.All
+      case `off` => MoreJoins.Disabled
+      case `impure` => MoreJoins.Impure
+      case s => Violation.violation(s"Unexpected mode for moreJoins: $s")
+    }
+  }
 
   val mceMode: ScallopOption[MCE.Mode] = {
     val on = "on"
@@ -840,8 +876,8 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
   }
 
   addValidation {
-    val enableMoreJoinsOptSupplied = enableMoreJoins.isSupplied
-    if (enableMoreJoinsOptSupplied  && !isSiliconBasedBackend) {
+    val moreJoinsOptSupplied = moreJoins.isSupplied
+    if (moreJoinsOptSupplied  && !isSiliconBasedBackend) {
       Left("The flag --moreJoins can only be used with Silicon or ViperServer with Silicon")
     } else {
       Right(())
@@ -965,6 +1001,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     disableSetAxiomatization = disableSetAxiomatization(),
     disableCheckTerminationPureFns = disableCheckTerminationPureFns(),
     unsafeWildcardOptimization = unsafeWildcardOptimization(),
-    enableMoreJoins = enableMoreJoins(),
+    moreJoins = moreJoins(),
   )
 }

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