Implements CR suggestions by Felix

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

@@ -89,18 +89,12 @@ trait Implements { this: TypeInfoImpl =>
     case _ => failedProp(s"$r is not an interface")
   }
 
-  /** Returns true if the type is supported for interfaces. All finite types are supported except for structs with ghost fields. */
+  /** Returns true if the type is supported for interfaces. All finite types are supported. */
   def supportedSortForInterfaces(t: Type): PropertyResult = {
-    failedProp(s"The type $t is not supported for interface", !isIdentityPreservingType(t)) and
-    // the following restriction is in place because Go considers two struct values under an interface to be equal if
-    // they agree on their struct fields. I.e., for `type S struct { val int, ghost gval int }`, `any(S{0, 0}) == any(S{0, 42})` holds
-    // in Go (after erasing the ghost fields). While we could extend the interface encoding to permit structs with ghost fields
-    // to implement an interface, we currently reject such cases. However, note that we already support a _pointer_ to a struct with
-    // ghost fields implementing an interface.
-    failedProp(s"Structs containing ghost fields are not supported for interface", isStructTypeWithGhostFields(t))
+    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
@@ -110,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 (_, info) => go(info.typ) }
+          // 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/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

@@ -80,10 +80,11 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
   def isStructTypeWithGhostFields(t: Type): Boolean = t match {
     case Single(st) => underlyingType(st) match {
       case t: StructT =>
-        structMemberSet(t).collect {
-          case (_, f: Field) => f.ghost
-          case (_, e: Embbed) => e.ghost || isStructTypeWithGhostFields(e.context.typ(e.decl.typ))
-        }.exists(identity)
+        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
     }

src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala

@@ -131,19 +131,7 @@ class StructEncoding extends TypeEncoding {
     * [(lhs: *Struct{}°) == rhs: *Struct{}] -> unknown()
     * [(lhs: *Struct{F}°) == rhs: *Struct{_}] -> [lhs] == [rhs]
     */
-  override def equal(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = {
-    case (lhs :: ctx.Struct(lhsFs), rhs :: ctx.Struct(rhsFs), src) =>
-      val (pos, info, errT) = src.vprMeta
-      pure(
-        for {
-          x <- bind(lhs)(ctx)
-          y <- bind(rhs)(ctx)
-          lhsFAccs = fieldAccesses(x, lhsFs)
-          rhsFAccs = fieldAccesses(y, rhsFs)
-          equalFields <- sequence((lhsFAccs zip rhsFAccs).map { case (lhsFA, rhsFA) => ctx.equal(lhsFA, rhsFA)(src) })
-        } yield VU.bigAnd(equalFields)(pos, info, errT)
-      )(ctx)
-
+  override def equal(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = structEqual(ctx, useGoEquality = false) orElse {
     case (lhs :: ctx.*(ctx.Struct(lhsFs)) / Exclusive, rhs :: ctx.*(ctx.Struct(_)), src) =>
       if (lhsFs.isEmpty) {
         unit(withSrc(if (lhs == rhs) vpr.TrueLit() else ctx.unknownValue.unkownValue(vpr.Bool), src))
@@ -160,17 +148,30 @@ class StructEncoding extends TypeEncoding {
     *
     * [(lhs: Struct{F}) == rhs: Struct{_}] -> AND f in actual(F): [lhs.f == rhs.f] (NOTE: f ranges only over actual fields since `goEqual` corresponds to actual comparison)
     */
-  override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = default(super.goEqual(ctx)) {
+  override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = default(super.goEqual(ctx))(structEqual(ctx, useGoEquality = true))
+
+  /**
+    * Encodes equality of two struct values under consideration of either the Go or Gobra/ghost semantics
+    *
+    * useGoEquality:
+    * [(lhs: Struct{F}) == rhs: Struct{_}] -> AND f in actual(F): [lhs.f == rhs.f] (NOTE: f ranges only over actual fields)
+    *
+    * !useGoEquality:
+    * [(lhs: Struct{F}) == rhs: Struct{_}] -> AND f in F: [lhs.f == rhs.f] (NOTE: f ranges over actual & ghost fields)
+    */
+  private def structEqual(ctx: Context, useGoEquality: Boolean): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = {
     case (lhs :: ctx.Struct(lhsFs), rhs :: ctx.Struct(rhsFs), src) =>
       val (pos, info, errT) = src.vprMeta
-      val actualFieldFilter: in.FieldRef => Boolean = fr => !fr.field.ghost
+      // keep all fields if we are NOT using Go's equality. Otherwise, only keep actual fields:
+      val fieldFilter: in.FieldRef => Boolean = fr => !useGoEquality || !fr.field.ghost
+      val equalFn = (l: in.Expr, r: in.Expr) => if (useGoEquality) ctx.goEqual(l, r)(src) else ctx.equal(l, r)(src)
       pure(
         for {
           x <- bind(lhs)(ctx)
           y <- bind(rhs)(ctx)
-          lhsFAccs = fieldAccesses(x, lhsFs).filter(actualFieldFilter)
-          rhsFAccs = fieldAccesses(y, rhsFs).filter(actualFieldFilter)
-          equalFields <- sequence((lhsFAccs zip rhsFAccs).map { case (lhsFA, rhsFA) => ctx.equal(lhsFA, rhsFA)(src) })
+          lhsFAccs = fieldAccesses(x, lhsFs).filter(fieldFilter)
+          rhsFAccs = fieldAccesses(y, rhsFs).filter(fieldFilter)
+          equalFields <- sequence((lhsFAccs zip rhsFAccs).map { case (lhsFA, rhsFA) => equalFn(lhsFA, rhsFA) })
         } yield VU.bigAnd(equalFields)(pos, info, errT)
       )(ctx)
   }

src/test/resources/regressions/features/ghost_field/ghost-field-comparison-simple02.gobra

@@ -0,0 +1,43 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// tests that Gobra correctly excludes ghost fields of nested structs when comparing structs using the standard Go comparison
+
+package GhostFieldComparisonSimple02
+
+type Test struct {
+    n NestedStruct
+}
+
+type NestedStruct struct {
+    actualField int
+    ghost ghostField int
+}
+
+decreases
+func foo() {
+    t1 := Test{NestedStruct{0, 0}}
+    t2 := Test{NestedStruct{0, 42}}
+    t3 := Test{NestedStruct{0, 42}}
+    assert t1 == t2 // actual comparison, i.e., ghost fields are ignored
+    assert t2 === t3 // ghost comparison
+    assert t1 !== t2 // ghost comparison
+
+    //:: ExpectedOutput(assert_error:assertion_error)
+    assert false
+}
+
+// behavior is the same independent of ghost/actual context
+ghost
+decreases
+func ghostFoo() {
+    t1 := Test{NestedStruct{0, 0}}
+    t2 := Test{NestedStruct{0, 42}}
+    t3 := Test{NestedStruct{0, 42}}
+    assert t1 == t2 // actual comparison, i.e., ghost fields are ignored
+    assert t2 === t3 // ghost comparison
+    assert t1 !== t2 // ghost comparison
+
+    //:: ExpectedOutput(assert_error:assertion_error)
+    assert false
+}