Introduce ghost equality (===) and inequality (!==)

src/main/antlr4/GobraLexer.g4

@@ -83,3 +83,5 @@ OUTLINE     : 'outline';
 INIT_POST   : 'initEnsures';
 IMPORT_PRE  : 'importRequires';
 PROOF       : 'proof';
+GHOST_EQUALS     : '===';
+GHOST_NOT_EQUALS : '!==';

src/main/antlr4/GobraParser.g4

@@ -275,6 +275,8 @@ expression:
     | LESS_OR_EQUALS
     | GREATER
     | GREATER_OR_EQUALS
+    | GHOST_EQUALS
+    | GHOST_NOT_EQUALS
   ) expression #relExpr
   | expression IMPL closureSpecInstance #closureImplSpecExpr
   | expression LOGICAL_AND expression #andExpr

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

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.9.2
+// Generated from /Users/joao/Code/gobraHome/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.9.2
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 

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

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.9.2
+// Generated from /Users/joao/Code/gobraHome/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.9.2
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -525,6 +525,10 @@ case class PEquals(left: PExpressionOrType, right: PExpressionOrType) extends PB
 
 case class PUnequals(left: PExpressionOrType, right: PExpressionOrType) extends PBinaryExp[PExpressionOrType, PExpressionOrType]
 
+case class PGhostEquals(left: PExpression, right: PExpression) extends PBinaryGhostExp
+
+case class PGhostUnequals(left: PExpression, right: PExpression) extends PBinaryGhostExp
+
 case class PAnd(left: PExpression, right: PExpression) extends PBinaryExp[PExpression, PExpression]
 
 case class POr(left: PExpression, right: PExpression) extends PBinaryExp[PExpression, PExpression]

src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala

@@ -471,6 +471,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PIota() => "iota"
     }
     case expr: PGhostExpression => expr match {
+      case PGhostEquals(l, r) => showExpr(l) <+> "===" <+> showExpr(r)
+      case PGhostUnequals(l, r) => showExpr(l) <+> "!==" <+> showExpr(r)
       case POld(e) => "old" <> parens(showExpr(e))
       case PLabeledOld(l, e) => "old" <> brackets(l.name) <> parens(showExpr(e))
       case PBefore(e) => "before" <> parens(showExpr(e))

src/main/scala/viper/gobra/ast/internal/Program.scala

@@ -1036,6 +1036,8 @@ object BinaryExpr {
 
 case class EqCmp(left: Expr, right: Expr)(val info: Source.Parser.Info)      extends BinaryExpr("==") with BoolOperation
 case class UneqCmp(left: Expr, right: Expr)(val info: Source.Parser.Info)    extends BinaryExpr("!=") with BoolOperation
+case class GhostEqCmp(left: Expr, right: Expr)(val info: Source.Parser.Info)   extends BinaryExpr("===") with BoolOperation
+case class GhostUneqCmp(left: Expr, right: Expr)(val info: Source.Parser.Info) extends BinaryExpr("!==") with BoolOperation
 case class LessCmp(left: Expr, right: Expr)(val info: Source.Parser.Info)    extends BinaryExpr("<" ) with BoolOperation
 case class AtMostCmp(left: Expr, right: Expr)(val info: Source.Parser.Info)  extends BinaryExpr("<=") with BoolOperation
 case class GreaterCmp(left: Expr, right: Expr)(val info: Source.Parser.Info) extends BinaryExpr(">" ) with BoolOperation

src/main/scala/viper/gobra/ast/internal/utility/GobraStrategy.scala

@@ -119,6 +119,8 @@ object GobraStrategy {
       case (_: BitNeg, Seq(op: Expr)) => BitNeg(op)(meta)
       case (_: EqCmp, Seq(l: Expr, r: Expr)) => EqCmp(l, r)(meta)
       case (_: UneqCmp, Seq(l: Expr, r: Expr)) => UneqCmp(l, r)(meta)
+      case (_: GhostEqCmp, Seq(l: Expr, r: Expr)) => GhostEqCmp(l, r)(meta)
+      case (_: GhostUneqCmp, Seq(l: Expr, r: Expr)) => GhostUneqCmp(l, r)(meta)
       case (_: LessCmp, Seq(l: Expr, r: Expr)) => LessCmp(l, r)(meta)
       case (_: AtMostCmp, Seq(l: Expr, r: Expr)) => AtMostCmp(l, r)(meta)
       case (_: GreaterCmp, Seq(l: Expr, r: Expr)) => GreaterCmp(l, r)(meta)

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

@@ -2239,6 +2239,11 @@ object Desugar {
 
           case PEquals(left, right) =>
             if (info.typOfExprOrType(left) == PermissionT || info.typOfExprOrType(right) == PermissionT) {
+              // When at least one of the operands has type 'perm', both operands are treated as permissions.
+              // This ensures that comparisons between a perm and a literal are handled consistently with the design of Go.
+              // E.g. the right-hand side of perm(1/2) == 1/2 is treated as a permission.
+              // TODO: maybe it would be preferable to not have this implicit cast for 'perm', and instead require
+              //       the user to always annotate literals of type 'perm' with a conversion.
               for {
                 l <- permissionD(ctx, info)(left.asInstanceOf[PExpression])
                 r <- permissionD(ctx, info)(right.asInstanceOf[PExpression])
@@ -2252,6 +2257,9 @@ object Desugar {
 
           case PUnequals(left, right) =>
             if (info.typOfExprOrType(left) == PermissionT || info.typOfExprOrType(right) == PermissionT) {
+              // When at least one of the operands has type 'perm', both operands are treated as permissions.
+              // This ensures that comparisons between a perm and a literal are handled consistently with the design of Go.
+              // E.g. the right-hand side of perm(1/2) == 1/2 is treated as a permission.
               for {
                 l <- permissionD(ctx, info)(left.asInstanceOf[PExpression])
                 r <- permissionD(ctx, info)(right.asInstanceOf[PExpression])
@@ -2263,6 +2271,26 @@ object Desugar {
               } yield in.UneqCmp(l, r)(src)
             }
 
+          case PGhostEquals(left, right) =>
+            if (info.typ(left) == PermissionT || info.typ(right) == PermissionT) {
+              // When at least one of the operands has type 'perm', both operands are treated as permissions.
+              // This ensures that comparisons between a perm and a literal are handled consistently with the design of Go.
+              // E.g. the right-hand side of perm(1/2) == 1/2 is treated as a permission.
+              for { l <- permissionD(ctx, info)(left); r <- permissionD(ctx, info)(right) } yield in.GhostEqCmp(l, r)(src)
+            } else {
+              for { l <- exprD(ctx, info)(left); r <- exprD(ctx, info)(right) } yield in.GhostEqCmp(l, r)(src)
+            }
+
+          case PGhostUnequals(left, right) =>
+            if (info.typ(left) == PermissionT || info.typ(right) == PermissionT) {
+              // When at least one of the operands has type 'perm', both operands are treated as permissions.
+              // This ensures that comparisons between a perm and a literal are handled consistently with the design of Go.
+              // E.g. the right-hand side of perm(1/2) == 1/2 is treated as a permission.
+              for { l <- permissionD(ctx, info)(left); r <- permissionD(ctx, info)(right) } yield in.GhostUneqCmp(l, r)(src)
+            } else {
+              for { l <- exprD(ctx, info)(left); r <- exprD(ctx, info)(right) } yield in.GhostUneqCmp(l, r)(src)
+            }
+
           case PLess(left, right) =>
             if (info.typ(left) == PermissionT || info.typ(right) == PermissionT) {
               for {l <- permissionD(ctx, info)(left); r <- permissionD(ctx, info)(right)} yield in.PermLtCmp(l, r)(src)

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

@@ -14,6 +14,8 @@ object TranslationHelpers {
   val binOp: Map[String, (PExpression, PExpression) => PExpression] = Map(
     VOCABULARY.getLiteralName(GobraParser.EQUALS) -> PEquals,
     VOCABULARY.getLiteralName(GobraParser.NOT_EQUALS) -> PUnequals,
+    VOCABULARY.getLiteralName(GobraParser.GHOST_EQUALS) -> PGhostEquals,
+    VOCABULARY.getLiteralName(GobraParser.GHOST_NOT_EQUALS) -> PGhostUnequals,
     VOCABULARY.getLiteralName(GobraParser.LESS) -> PLess,
     VOCABULARY.getLiteralName(GobraParser.LESS_OR_EQUALS) -> PAtMost,
     VOCABULARY.getLiteralName(GobraParser.GREATER) -> PGreater,

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

@@ -93,6 +93,8 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl =>
       case _: PNegation => AddrMod.rValue
       case _: PBitNegation => AddrMod.rValue
       case _: PBinaryExp[_,_] => AddrMod.rValue
+      case _: PGhostEquals => AddrMod.rValue
+      case _: PGhostUnequals => AddrMod.rValue
       case _: PPermission => AddrMod.rValue
       case _: PPredConstructor => AddrMod.rValue
       case n: PUnfolding => AddrMod.unfolding(addressability(n.op))

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

@@ -411,9 +411,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
 
     case n: PBinaryExp[_,_] =>
         (n, exprOrTypeType(n.left), exprOrTypeType(n.right)) match {
-          case (_: PEquals | _: PUnequals, l, r) =>
-            if (isEnclosingGhost(n)) ghostComparableTypes.errors(l, r)(n)
-            else comparableTypes.errors(l, r)(n)
+          case (_: PEquals | _: PUnequals, l, r) => comparableTypes.errors(l, r)(n)
           case (_: PAnd | _: POr, l, r) => assignableTo.errors(l, AssertionT)(n) ++ assignableTo.errors(r, AssertionT)(n)
           case (_: PLess | _: PAtMost | _: PGreater | _: PAtLeast, l, r) => (l,r) match {
             case (StringT, StringT) => noMessages

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

@@ -105,6 +105,16 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case t =>  error(n, s"expected interface or type, but got an expression of type $t")
     }
 
+    case n: PGhostEquals =>
+      val lType = typ(n.left)
+      val rType = typ(n.right)
+      ghostComparableTypes.errors(lType, rType)(n)
+
+    case n: PGhostUnequals =>
+      val lType = typ(n.left)
+      val rType = typ(n.right)
+      ghostComparableTypes.errors(lType, rType)(n)
+
     case POptionNone(t) => isType(t).out
     case POptionSome(e) => isExpr(e).out
     case POptionGet(e) => isExpr(e).out ++ {
@@ -222,6 +232,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
     case _: PTypeOf => SortT
     case _: PTypeExpr => SortT
     case _: PIsComparable => BooleanT
+    case _: PGhostEquals | _: PGhostUnequals => BooleanT
 
     case POptionNone(t) => OptionT(typeSymbType(t))
     case POptionSome(e) => OptionT(exprType(e))
@@ -401,6 +412,9 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case PLength(op) => go(op)
       case PCapacity(op) => go(op)
 
+      case PGhostEquals(l, r) => go(l) && go(r)
+      case PGhostUnequals(l, r) => go(l) && go(r)
+
       case expr: PGhostCollectionExp => expr match {
         case n: PBinaryGhostExp => go(n.left) && go(n.right)
         case PSequenceConversion(op) => go(op)

src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala

@@ -19,7 +19,8 @@ class MemoryEncoding extends Encoding {
     case r: in.Ref => ctx.reference(r.ref.op)
     case x@ in.EqCmp(l, r) => ctx.goEqual(l, r)(x)
     case x@ in.UneqCmp(l, r) => ctx.goEqual(l, r)(x).map(v => withSrc(vpr.Not(v), x))
-
+    case x@ in.GhostEqCmp(l, r) => ctx.equal(l, r)(x)
+    case x@ in.GhostUneqCmp(l, r) => ctx.equal(l, r)(x).map(v => withSrc(vpr.Not(v), x))
     case n@ in.LessCmp(l, r) => for {vl <- ctx.expression(l); vr <- ctx.expression(r)}    yield withSrc(vpr.LtCmp(vl, vr), n)
     case n@ in.AtMostCmp(l, r) => for {vl <- ctx.expression(l); vr <- ctx.expression(r)}  yield withSrc(vpr.LeCmp(vl, vr), n)
     case n@ in.GreaterCmp(l, r) => for {vl <- ctx.expression(l); vr <- ctx.expression(r)} yield withSrc(vpr.GtCmp(vl, vr), n)

src/test/resources/regressions/features/closures/closures-recursion1-simple.gobra

@@ -12,7 +12,7 @@ pure func fact(n int)int {
 func main() {
     var c@ func(int)int
     c = requires n >= 0
-        preserves acc(&c, 1/2) && c == factorial
+        preserves acc(&c, 1/2) && c === factorial
         ensures r == fact(n)
         decreases n
         func factorial(n int) (r int) {

src/test/resources/regressions/features/closures/closures-termination.gobra

@@ -6,7 +6,7 @@ package closuresTermination
 func test1() {
     var c@ func(int)int
     c = requires n >= 0
-        preserves acc(&c, 1/2) && c == factorial
+        preserves acc(&c, 1/2) && c === factorial
         decreases n
         func factorial(n int) int {
             if n == 0 {
@@ -21,7 +21,7 @@ func test2() {
     var c@ func(int, int)int
     c = requires m >= 0
         requires n >= 0
-        preserves acc(&c, 1/2) && c == ack
+        preserves acc(&c, 1/2) && c === ack
         ensures result >= 0
         decreases m, n
         func ack(m int, n int) (result int) {
@@ -51,7 +51,7 @@ func test3() {
 func test4() {
     var c@ func(int)int
     c = requires 1 <= n
-        preserves acc(&c, 1/2) && c == collatz
+        preserves acc(&c, 1/2) && c === collatz
         decreases _
         func collatz(n int)int {
             if n == 1 {

src/test/resources/regressions/features/slices/slice-type-fail1.gobra

@@ -0,0 +1,10 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+// property error: slice types are always incomparable using go equality (==), except for 'nil'
+//:: ExpectedOutput(type_error)
+requires s == t
+func foo(s []int, t []int) { 
+}

src/test/resources/regressions/features/slices/slice-type-fail5.gobra

@@ -0,0 +1,11 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+requires s == nil
+func foo(s []int) {
+	var a@ [0]int
+	//:: ExpectedOutput(type_error)
+	assert s[:] == a[:] // slices can only be compared when using ghost equality (===)
+}

src/test/resources/regressions/features/slices/slice-type-simple3.gobra

@@ -0,0 +1,26 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+// slices can be compared with ghost equality (===)
+requires s === t
+func foo(s []int, t []int) { 
+}
+
+type Comp interface{
+	m() int
+}
+
+// interfaces can also be compared with ghost equality (===)
+ghost
+requires c1 === c2
+func bar1(c1, c2 Comp) bool {
+	return c1 === c2
+}
+
+ghost
+requires c1 !== c2 // ghost disequality
+func bar2(c1, c2 Comp) bool {
+	return c1 !== c2
+}

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

@@ -5,14 +5,14 @@ package test
 
 func foo(x []int) {
 	z := x
-	assert x == z
+	assert x === z
 }
 
-requires s == t
+requires s === t
 func bar(s []int, t []int) { }
 
 requires s == nil
 func foobar(s []int) {
 	var a@ [0]int
-	assert s[:] != a[:]
+	assert s[:] !== a[:]
 }