Fix #861 (#862)

* adapts type-checker to correctly consider the fact that we are implicitly treating a call to an actual pure function as being ghost * adds a ghost erasure testcase * Update src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostAssignability.scala Co-authored-by: João Pereira <[email protected]> * implements CR suggestions by Joao --------- Co-authored-by: João Pereira <[email protected]>
viperproject · Feb 26, 2025 · 9470b55 · 9470b55
1 parent d2bc4f8
commit 9470b55
Show file tree

Hide file tree

Showing 6 changed files with 153 additions and 42 deletions.
diff --git a/src/main/scala/viper/gobra/ast/frontend/AstPattern.scala b/src/main/scala/viper/gobra/ast/frontend/AstPattern.scala
@@ -51,28 +51,49 @@ object AstPattern {
   case class IndexedExp(base : PExpression, index : PExpression) extends Expr
   case class BlankIdentifier(decl: PBlankIdentifier) extends Expr
 
-  sealed trait FunctionKind extends Expr {
+  sealed trait FunctionKind extends Expr with Symbolic {
     def id: PIdnUse
+    def ghost: Boolean = symb.ghost
+    def isPure: Boolean
   }
 
-  case class Function(id: PIdnUse, symb: st.Function) extends FunctionKind with Symbolic
-  case class Closure(id: PIdnUse, symb: st.Closure) extends FunctionKind with Symbolic
-  case class DomainFunction(id: PIdnUse, symb: st.DomainFunction) extends FunctionKind with Symbolic
-  case class ReceivedMethod(recv: PExpression, id: PIdnUse, path: Vector[MemberPath], symb: st.Method) extends FunctionKind with Symbolic
-  case class ImplicitlyReceivedInterfaceMethod(id: PIdnUse, symb: st.MethodSpec) extends FunctionKind with Symbolic // for method references withing an interface definition
-  case class MethodExpr(typ: PType, id: PIdnUse, path: Vector[MemberPath], symb: st.Method) extends FunctionKind with Symbolic
+  case class Function(id: PIdnUse, symb: st.Function) extends FunctionKind {
+    override val isPure: Boolean = symb.isPure
+  }
+  case class Closure(id: PIdnUse, symb: st.Closure) extends FunctionKind {
+    override val isPure: Boolean = symb.isPure
+  }
+  case class DomainFunction(id: PIdnUse, symb: st.DomainFunction) extends FunctionKind {
+    override val isPure: Boolean = true
+  }
+  case class ReceivedMethod(recv: PExpression, id: PIdnUse, path: Vector[MemberPath], symb: st.Method) extends FunctionKind {
+    override val isPure: Boolean = symb.isPure
+  }
+  /** for method references withing an interface definition */
+  case class ImplicitlyReceivedInterfaceMethod(id: PIdnUse, symb: st.MethodSpec) extends FunctionKind {
+    override val isPure: Boolean = symb.isPure
+  }
+  case class MethodExpr(typ: PType, id: PIdnUse, path: Vector[MemberPath], symb: st.Method) extends FunctionKind {
+    override val isPure: Boolean = symb.isPure
+  }
 
-  sealed trait BuiltInFunctionKind extends FunctionKind with Symbolic {
+  sealed trait BuiltInFunctionKind extends FunctionKind {
     def symb: st.BuiltInActualEntity
   }
   sealed trait BuiltInMethodKind extends BuiltInFunctionKind {
     def path: Vector[MemberPath]
     def symb: st.BuiltInMethod
   }
 
-  case class BuiltInFunction(id: PIdnUse, symb: st.BuiltInFunction) extends BuiltInFunctionKind with Symbolic
-  case class BuiltInReceivedMethod(recv: PExpression, id: PIdnUse, path: Vector[MemberPath], symb: st.BuiltInMethod) extends BuiltInMethodKind
-  case class BuiltInMethodExpr(typ: PType, id: PIdnUse, path: Vector[MemberPath], symb: st.BuiltInMethod) extends BuiltInMethodKind
+  case class BuiltInFunction(id: PIdnUse, symb: st.BuiltInFunction) extends BuiltInFunctionKind with Symbolic {
+    override val isPure: Boolean = symb.isPure
+  }
+  case class BuiltInReceivedMethod(recv: PExpression, id: PIdnUse, path: Vector[MemberPath], symb: st.BuiltInMethod) extends BuiltInMethodKind {
+    override val isPure: Boolean = symb.isPure
+  }
+  case class BuiltInMethodExpr(typ: PType, id: PIdnUse, path: Vector[MemberPath], symb: st.BuiltInMethod) extends BuiltInMethodKind {
+    override val isPure: Boolean = symb.isPure
+  }
 
   sealed trait Assertion extends Pattern
 

diff --git a/...viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostAssignability.scala b/...viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostAssignability.scala
@@ -20,27 +20,14 @@ trait GhostAssignability {
 
   /** checks that ghost arguments are not assigned to non-ghost arguments  */
   private[separation] def ghostAssignableToCallExpr(call: ap.FunctionCall): Messages = {
-
-    val isPure = call.callee match {
-      case p: ap.Function => p.symb.isPure
-      case p: ap.Closure => p.symb.isPure
-      case p: ap.MethodExpr => p.symb.isPure
-      case p: ap.ReceivedMethod => p.symb.isPure
-      case p: ap.BuiltInFunction => p.symb.isPure
-      case p: ap.BuiltInMethodExpr => p.symb.isPure
-      case p: ap.BuiltInReceivedMethod => p.symb.isPure
-      case p: ap.ImplicitlyReceivedInterfaceMethod => p.symb.isPure
-      case _: ap.DomainFunction => true
-      case _ => false
-    }
-    if (isPure) {return noMessages}
-
     val argTyping = calleeArgGhostTyping(call).toTuple
-    generalGhostAssignableTo[PExpression, Boolean](ghostExprResultTyping){
-      case (g, l) => error(call.callee.id, "ghost error: ghost cannot be assigned to non-ghost", g && !l)
-    }(call.args: _*)(argTyping: _*)
+    argsAssignable(call, argTyping)
   }
 
+  private def argsAssignable(call: ap.FunctionCall, argTyping: Vector[Boolean]): Messages = generalGhostAssignableTo[PExpression, Boolean](ghostExprResultTyping){
+    case (g, l) => error(call.callee.id, "ghost error: ghost cannot be assigned to non-ghost", g && !l)
+  }(call.args: _*)(argTyping: _*)
+
   /** checks that ghost arguments are not assigned to non-ghost arguments in a call with spec  */
   private[separation] def ghostAssignableToClosureCall(call: ap.ClosureCall): Messages = {
     val isPure = resolve(call.maybeSpec.get.func) match {
@@ -125,9 +112,8 @@ trait GhostAssignability {
     generalGhostAssignableTo(ghostExprResultTyping)(dfltGhostAssignableMsg[PIdnNode](wellGhostSeparated)(ghostIdClassification))(exprs: _*)(lefts: _*)
 
   /** conservative ghost separation assignment check */
-  private[separation] def ghostAssignableToParam(exprs: PExpression*)(lefts: PParameter*): Messages = {
+  private[separation] def ghostAssignableToParam(exprs: PExpression*)(lefts: PParameter*): Messages =
     generalGhostAssignableTo(ghostExprResultTyping)(dfltGhostAssignableMsg[PParameter](wellGhostSeparated)(ghostParameterClassification))(exprs: _*)(lefts: _*)
-  }
 
   /**
     * default factory for producing messages that a ghost right-hand side cannot be assigned to a non-ghost left-hand side
@@ -175,6 +161,20 @@ trait GhostAssignability {
 
   /** ghost type of the arguments of a callee */
   private[separation] def calleeArgGhostTyping(call: ap.FunctionCall): GhostType = {
+    val explicitGhostType = explicitCalleeArgGhostTyping(call)
+    val isImplicitlyGhost = isCallImplicitlyGhost(call)
+    // preserve the amount of entries in `explicitGhostType` but set all to true
+    // if the call is implicitly ghost. In case there are no entries (i.e., it's not ghost),
+    // simply return `isGhost`:
+    if (isImplicitlyGhost && explicitGhostType.toTuple.isEmpty) {
+      GhostType.isGhost
+    } else if (isImplicitlyGhost) {
+      GhostType.ghostTuple(Seq.fill(explicitGhostType.length)(true).toVector)
+    } else explicitGhostType
+  }
+
+  /** ghost type of the arguments of a callee based on explicit annotations of the parameter or callee */
+  private def explicitCalleeArgGhostTyping(call: ap.FunctionCall): GhostType = {
     // a parameter of a ghost member is ghost (even if such a explicit declaration is missing)
     def argTyping(args: Vector[PParameter], isMemberGhost: Boolean, context: ExternalTypeInfo): GhostType =
       GhostType.ghostTuple(args.map(p => isMemberGhost || context.isParamGhost(p)))
@@ -197,23 +197,16 @@ trait GhostAssignability {
   }
 
   /* ghost type of the callee itself (not considering its arguments or results) */
-  private[separation] def calleeGhostTyping(call: ap.FunctionCall): GhostType = call.callee match {
-    case p: ap.Function => ghost(p.symb.ghost)
-    case p: ap.ReceivedMethod => ghost(p.symb.ghost)
-    case p: ap.MethodExpr => ghost(p.symb.ghost)
-    case _: ap.PredicateKind => GhostType.isGhost
-    case _: ap.DomainFunction => GhostType.isGhost
-    case p: ap.BuiltInFunction => ghost(p.symb.ghost)
-    case p: ap.BuiltInReceivedMethod => ghost(p.symb.ghost)
-    case p: ap.BuiltInMethodExpr => ghost(p.symb.ghost)
-    case _ => GhostType.isGhost // conservative choice
+  private[separation] def calleeGhostTyping(call: ap.FunctionCall): GhostType = {
+    val isExplicitlyGhost = call.callee.ghost
+    ghost(isExplicitlyGhost || isCallImplicitlyGhost(call))
   }
 
   /** ghost type of the result of a callee */
   private[separation] def calleeReturnGhostTyping(call: ap.FunctionCall): GhostType = {
     // a result of a ghost member is ghost (even if such a explicit declaration is missing)
     def resultTyping(result: PResult, isMemberGhost: Boolean, context: ExternalTypeInfo): GhostType = {
-      GhostType.ghostTuple(result.outs.map(p => isMemberGhost || context.isParamGhost(p)))
+      GhostType.ghostTuple(result.outs.map(p => isMemberGhost || context.isParamGhost(p) || isCallImplicitlyGhost(call)))
     }
 
     call.callee match {
@@ -230,6 +223,20 @@ trait GhostAssignability {
     }
   }
 
+  /** returns true if `call` should be treated as being ghost because it is not explicitly
+    * annotated as being ghost _and_ one of the arguments is ghost even though the corresponding
+    * parameter is not explicitly annotated as being ghost.
+    */
+  private def isCallImplicitlyGhost(call: ap.FunctionCall): Boolean = {
+    // we only do this special treatment for calls to pure functions as the call
+    // can be erased without losing any side-effects. Furthermore, we have to do
+    // this implicit treatment only if assignability of arguments to parameters
+    // would otherwise fail:
+    val argTyping = explicitCalleeArgGhostTyping(call).toTuple
+    val assignable = argsAssignable(call, argTyping)
+    call.callee.isPure && assignable.nonEmpty
+  }
+
   /* If a closure is not ghost, the arguments and results of all the specs it can be called with must have
    * the same ghostness, so that removing ghost arguments yields a consistent result.
    * To ensure this, we make sure, for all spec implementation proofs, that the ghostness of the arguments and result

diff --git a/src/test/resources/regressions/issues/000861-1.gobra b/src/test/resources/regressions/issues/000861-1.gobra
@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue0008611
+
+//:: ExpectedOutput(type_error)
+func test() bool {
+    ghost var x = 42
+    ghost var y = 0
+    return isEqual(x, y)
+}
+
+decreases
+pure func isEqual(x, y int) bool {
+    return x == y
+}
diff --git a/src/test/resources/regressions/issues/000861-2.gobra b/src/test/resources/regressions/issues/000861-2.gobra
@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue0008612
+
+func test() (res bool) {
+    ghost var x = 42
+    ghost var y = 0
+    tmp := isEqual(x, y)
+    //:: ExpectedOutput(type_error)
+    res = tmp
+    return
+}
+
+decreases
+pure func isEqual(x, y int) bool {
+    return x == y
+}
diff --git a/src/test/resources/regressions/issues/000861-3.gobra b/src/test/resources/regressions/issues/000861-3.gobra
@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue0008613
+
+func test() (ghost res bool) {
+    ghost var x = 42
+    ghost var y = 0
+    tmp := isEqual(x, y)
+    res = tmp
+    //:: ExpectedOutput(assert_error:assertion_error)
+    assert false
+    return
+}
+
+decreases
+pure func isEqual(x, y int) bool {
+    return x == y
+}
diff --git a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala
@@ -339,6 +339,36 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
     frontend.testProg(input, expected)
   }
 
+  test("Ghost Erasure: ghost calls to non-ghost pure functions should be erased") {
+    // this corresponds to the program in "issues/000861-3.gobra"
+    val input =
+      s"""
+         |package pkg
+         |func test() (ghost res bool) {
+         |    ghost var x = 42
+         |    ghost var y = 0
+         |    tmp := isEqual(x, y)
+         |    res = tmp
+         |    return
+         |}
+         |decreases
+         |pure func isEqual(x, y int) bool {
+         |    return x == y
+         |}
+         |""".stripMargin
+    val expected =
+      s"""
+         |package pkg
+         |func test() {
+         |  return
+         |}
+         |func isEqual(x, y int) bool {
+         |  return x == y
+         |}
+         |""".stripMargin
+    frontend.testProg(input, expected)
+  }
+
   /* ** Stubs, mocks, and other test setup  */
 
   class TestFrontend {