Disallows impure non-ghost calls in ghost code

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

@@ -465,7 +465,9 @@ case class PClosureSpecInstance(func: PNameOrDot, params: Vector[PKeyedElement])
 
 case class PClosureImplements(closure: PExpression, spec: PClosureSpecInstance) extends PGhostExpression
 
-case class PClosureImplProof(impl: PClosureImplements, block: PBlock) extends PGhostStatement with PScope
+case class PClosureImplProof(impl: PClosureImplements, block: PBlock) extends PActualStatement with PScope with PProofAnnotation {
+  override def nonGhostChildren: Vector[PBlock] = Vector(block)
+}
 
 case class PInvoke(base: PExpressionOrType, args: Vector[PExpression], spec: Option[PClosureSpecInstance], reveal: Boolean = false) extends PActualExpression {
   require(base.isInstanceOf[PExpression] || spec.isEmpty) // `base` is a type for conversions only, for which `spec` is empty
@@ -938,7 +940,9 @@ case class PImplementationProof(
                                  subT: PType, superT: PType,
                                  alias: Vector[PImplementationProofPredicateAlias],
                                  memberProofs: Vector[PMethodImplementationProof]
-                               ) extends PGhostMember
+                               ) extends PActualMember with PProofAnnotation {
+  override def nonGhostChildren: Vector[PNode] = memberProofs
+}
 
 case class PMethodImplementationProof(
                                        id: PIdnUse, // references the method definition of the super type
@@ -947,7 +951,9 @@ case class PMethodImplementationProof(
                                        result: PResult,
                                        isPure: Boolean,
                                        body: Option[(PBodyParameterInfo, PBlock)]
-                                     ) extends PGhostMisc with PScope with PCodeRootWithResult with PWithBody
+                                     ) extends PActualMisc with PScope with PCodeRootWithResult with PWithBody with PProofAnnotation {
+  override def nonGhostChildren: Vector[PNode] = Vector(receiver, result) ++ args ++ body.map(_._2).toVector
+}
 
 case class PImplementationProofPredicateAlias(left: PIdnUse, right: PNameOrDot) extends PGhostMisc
 

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

@@ -112,18 +112,18 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PMethodDecl(id, rec, args, res, spec, body) =>
         showSpec(spec) <> "func" <+> showReceiver(rec) <+> showId(id) <> parens(showParameterList(args)) <> showResult(res) <>
         opt(body)(b => space <> showBodyParameterInfoWithBlock(b._1, b._2))
+      case ip: PImplementationProof =>
+        showType(ip.subT) <+> "implements" <+> showType(ip.superT) <> (
+          if (ip.alias.isEmpty && ip.memberProofs.isEmpty) emptyDoc
+          else block(ssep(ip.alias map showMisc, line) <> line <> ssep(ip.memberProofs map showMisc, line))
+          )
     }
     case member: PGhostMember => member match {
       case PExplicitGhostMember(m) => "ghost" <+> showMember(m)
       case PFPredicateDecl(id, args, body) =>
         "pred" <+> showId(id) <> parens(showParameterList(args)) <> opt(body)(b => space <> block(showExpr(b)))
       case PMPredicateDecl(id, recv, args, body) =>
         "pred" <+> showReceiver(recv) <+> showId(id) <> parens(showParameterList(args)) <> opt(body)(b => space <> block(showExpr(b)))
-      case ip: PImplementationProof =>
-        showType(ip.subT) <+> "implements" <+> showType(ip.superT) <> (
-            if (ip.alias.isEmpty && ip.memberProofs.isEmpty) emptyDoc
-            else block(ssep(ip.alias map showMisc, line) <> line <> ssep(ip.memberProofs map showMisc, line))
-          )
     }
   }
 
@@ -279,6 +279,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PBlock(stmts) => block(showStmtList(stmts))
       case PSeq(stmts) => showStmtList(stmts)
       case POutline(body, spec) => showSpec(spec) <> "outline" <> parens(nest(line <> showStmt(body)) <> line)
+      case PClosureImplProof(impl, PBlock(stmts)) => "proof" <+> showExpr(impl) <> block(showStmtList(stmts))
     }
     case statement: PGhostStatement => statement match {
       case PExplicitGhostStatement(actual) => "ghost" <+> showStmt(actual)
@@ -292,7 +293,6 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PApplyWand(wand) => "apply" <+> showExpr(wand)
       case PMatchStatement(exp, clauses, _) => "match" <+>
         showExpr(exp) <+> block(ssep(clauses map showMatchClauseStatement, line))
-      case PClosureImplProof(impl, PBlock(stmts)) => "proof" <+> showExpr(impl) <> block(showStmtList(stmts))
     }
   }
 
@@ -703,15 +703,21 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   // misc
 
   def showMisc(id: PMisc): Doc = id match {
-    case n: PRange => showRange(n)
-    case receiver: PReceiver => showReceiver(receiver)
-    case result: PResult => showResult(result)
-    case embeddedType: PEmbeddedType => showEmbeddedType(embeddedType)
-    case parameter: PParameter => showParameter(parameter)
-    case literalValue: PLiteralValue => showLiteralValue(literalValue)
-    case keyedElement: PKeyedElement => showKeyedElement(keyedElement)
-    case compositeVal: PCompositeVal => showCompositeVal(compositeVal)
-    case closureDecl: PClosureDecl => showFunctionLit(PFunctionLit(None, closureDecl))
+    case misc: PActualMisc => misc match {
+      case n: PRange => showRange(n)
+      case receiver: PReceiver => showReceiver(receiver)
+      case result: PResult => showResult(result)
+      case embeddedType: PEmbeddedType => showEmbeddedType(embeddedType)
+      case parameter: PParameter => showParameter(parameter)
+      case literalValue: PLiteralValue => showLiteralValue(literalValue)
+      case keyedElement: PKeyedElement => showKeyedElement(keyedElement)
+      case compositeVal: PCompositeVal => showCompositeVal(compositeVal)
+      case closureDecl: PClosureDecl => showFunctionLit(PFunctionLit(None, closureDecl))
+      case mip: PMethodImplementationProof =>
+        (if (mip.isPure) "pure ": Doc else emptyDoc) <>
+          parens(showParameter(mip.receiver)) <+> showId(mip.id) <> parens(showParameterList(mip.args)) <> showResult(mip.result) <>
+          opt(mip.body)(b => space <> showBodyParameterInfoWithBlock(b._1, b._2))
+    }
     case misc: PGhostMisc => misc match {
       case s: PClosureSpecInstance => showExprOrType(s.func) <> braces(ssep(s.params map showMisc, comma <> space))
       case PFPredBase(id) => showId(id)
@@ -722,10 +728,6 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PDomainFunction(id, args, res) =>
         "func" <+> showId(id) <> parens(showParameterList(args)) <> showResult(res)
       case PDomainAxiom(exp) => "axiom" <+> block(showExpr(exp))
-      case mip: PMethodImplementationProof =>
-        (if (mip.isPure) "pure ": Doc else emptyDoc) <>
-          parens(showParameter(mip.receiver)) <+> showId(mip.id) <> parens(showParameterList(mip.args)) <> showResult(mip.result) <>
-          opt(mip.body)(b => space <> showBodyParameterInfoWithBlock(b._1, b._2))
       case ipa: PImplementationProofPredicateAlias =>
         "pred" <+> showId(ipa.left) <+> ":=" <+> showExprOrType(ipa.right)
       case PAdtClause(id, args) =>
@@ -759,15 +761,15 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
         showSpec(spec) <> "func" <+> showId(id) <> parens(showParameterList(args)) <> showResult(res)
       case PMethodDecl(id, rec, args, res, spec, _) =>
         showSpec(spec) <> "func" <+> showReceiver(rec) <+> showId(id) <> parens(showParameterList(args)) <> showResult(res)
+      case ip: PImplementationProof =>
+        showType(ip.subT) <+> "implements" <+> showType(ip.superT)
     }
     case member: PGhostMember => member match {
       case PExplicitGhostMember(m) => "ghost" <+> showMember(m)
       case PFPredicateDecl(id, args, _) =>
         "pred" <+> showId(id) <> parens(showParameterList(args))
       case PMPredicateDecl(id, recv, args, _) =>
         "pred" <+> showReceiver(recv) <+> showId(id) <> parens(showParameterList(args))
-      case ip: PImplementationProof =>
-        showType(ip.subT) <+> "implements" <+> showType(ip.superT)
     }
   }
 

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

@@ -1914,6 +1914,8 @@ object Desugar extends LazyLogging {
               case t => violation(s"Type $t not supported as a range expression")
             }
 
+          case p: PClosureImplProof => closureImplProofD(ctx)(p)
+
           case _ => ???
         }
       }
@@ -4108,7 +4110,6 @@ object Desugar extends LazyLogging {
             case w: in.MagicWand => in.ApplyWand(w)(src)
             case e => Violation.violation(s"Expected a magic wand, but got $e")
           }
-        case p: PClosureImplProof => closureImplProofD(ctx)(p)
         case PExplicitGhostStatement(actual) => stmtD(ctx, info)(actual)
 
         case PMatchStatement(exp, clauses, strict) =>

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

@@ -144,7 +144,10 @@ trait NameResolution {
       case _ => violation("PIdnUnk always has a parent")
     }
 
-  private[resolution] lazy val isGhostDef: PNode => Boolean = isEnclosingGhost
+  // technically, `isGhostDef` should consider for implementation proofs whether the method getting implemented is ghost
+  // however, since implementation proofs are syntactically restricted, we assume for now that definitions in all
+  // implementation proofs are non-ghost.
+  private[resolution] lazy val isGhostDef: PNode => Boolean = n => isEnclosingGhost(n)
 
   private[resolution] def serialize(id: PIdnNode): String = id.name
 
@@ -260,11 +263,13 @@ trait NameResolution {
         case d: PFunctionDecl => Vector(d.id)
         case d: PTypeDecl => Vector(d.left) ++ leakingIdentifier(d.right)
         case d: PMethodDecl => Vector(d.id)
+        case _: PImplementationProof => Vector.empty
+      }
+      case g: PGhostMember => g match {
+        case PExplicitGhostMember(a) => packageLevelDefinitions(a)
+        case p: PMPredicateDecl => Vector(p.id)
+        case p: PFPredicateDecl => Vector(p.id)
       }
-      case PExplicitGhostMember(a) => packageLevelDefinitions(a)
-      case p: PMPredicateDecl => Vector(p.id)
-      case p: PFPredicateDecl => Vector(p.id)
-      case _: PImplementationProof => Vector.empty
     }
   }
 

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

@@ -10,6 +10,7 @@ import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages
 import viper.gobra.GoVerifier
 import viper.gobra.ast.frontend._
 import viper.gobra.frontend.Config
+import viper.gobra.frontend.info.base.SymbolTable.MPredicateSpec
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.util.Constants
 
@@ -55,6 +56,37 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl =>
       }
     case s: PActualStatement =>
       wellDefStmt(s).out
+
+    case ip: PImplementationProof =>
+      val subType = symbType(ip.subT)
+      val superType = symbType(ip.superT)
+
+      val syntaxImplementsMsgs = syntaxImplements(subType, superType).asReason(ip, s"${ip.subT} does not implement the interface ${ip.superT}")
+      if (syntaxImplementsMsgs.nonEmpty) syntaxImplementsMsgs
+      else {
+        addDemandedImplements(subType, superType)
+
+        {
+          val badReceiverTypes = ip.memberProofs.map(m => miscType(m.receiver))
+            .filter(t => !identicalTypes(t, subType))
+          error(ip, s"The receiver of all methods included in the implementation proof must be $subType, " +
+            s"but encountered: ${badReceiverTypes.distinct.mkString(", ")}", cond = badReceiverTypes.nonEmpty)
+        } ++ {
+          val superPredNames = memberSet(superType).collect { case (n, m: MPredicateSpec) => (n, m) }
+          val allPredicatesDefined = PropertyResult.bigAnd(superPredNames.map { case (name, symb) =>
+            val valid = tryMethodLikeLookup(subType, PIdnUse(name)).isDefined ||
+              ip.alias.exists(al => al.left.name == name)
+            failedProp({
+              val argTypes = symb.args map symb.context.typ
+
+              s"predicate $name is not defined for type $subType. " +
+                s"Either declare a predicate 'pred ($subType) $name(${argTypes.mkString(", ")})' " +
+                s"or declare a predicate 'pred p($subType${if (argTypes.isEmpty) "" else ", "}${argTypes.mkString(", ")})' with some name p and add 'pred $name := p' to the implementation proof."
+            }, !valid)
+          })
+          allPredicatesDefined.asReason(ip, "Some predicate definitions are missing")
+        }
+      }
   }
 
   private def wellDefConstSpec(spec: PConstSpec): Messages = {

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

@@ -41,6 +41,77 @@ trait MiscTyping extends BaseTyping { this: TypeInfoImpl =>
     case _: PLiteralValue | _: PKeyedElement | _: PCompositeVal => noMessages // these are checked at the level of the composite literal
 
     case _: PClosureDecl => noMessages // checks are done at the PFunctionLit level
+
+    case n: PMethodImplementationProof =>
+      val validPureCheck = wellDefIfPureMethodImplementationProof(n)
+      if (validPureCheck.nonEmpty) validPureCheck
+      else {
+        entity(n.id) match {
+          case spec: MethodSpec =>
+            // check that the signatures match
+            val matchingSignature = {
+              val implSig = FunctionT(n.args map miscType, miscType(n.result))
+              val specSig = memberType(spec)
+              failedProp(
+                s"implementation proof and interface member have a different signature (should be '$specSig', but is $implSig nad ${implSig == specSig})",
+                cond = !identicalTypes(implSig, specSig)
+              )
+            }
+            // check that pure annotations match
+            val matchingPure = failedProp(
+              s"The pure annotation does not match with the pure annotation of the interface member",
+              cond = n.isPure != spec.isPure
+            )
+            // check that the receiver has the method
+            val receiverHasMethod = failedProp(
+              s"The type ${n.receiver.typ} does not have member ${n.id}",
+              cond = tryMethodLikeLookup(miscType(n.receiver), n.id).isEmpty
+            )
+            // check that the body has the right shape
+            val rightShape = {
+              n.body match {
+                case None => failedProp("A method in an implementation proof must not be abstract")
+                case Some((_, block)) =>
+
+                  val expectedReceiverOpt = n.receiver match {
+                    case _: PUnnamedParameter => None
+                    case p: PNamedParameter => Some(PNamedOperand(PIdnUse(p.id.name)))
+                    case PExplicitGhostParameter(_: PUnnamedParameter) => None
+                    case PExplicitGhostParameter(p: PNamedParameter) => Some(PNamedOperand(PIdnUse(p.id.name)))
+                  }
+
+                  val expectedArgs = n.args.flatMap {
+                    case p: PNamedParameter => Some(PNamedOperand(PIdnUse(p.id.name)))
+                    case PExplicitGhostParameter(p: PNamedParameter) => Some(PNamedOperand(PIdnUse(p.id.name)))
+                    case _ => None
+                  }
+
+                  if (expectedReceiverOpt.isEmpty || expectedArgs.size != n.args.size) {
+                    failedProp("Receiver and arguments must be named so that they can be used in a call")
+                  } else {
+                    val expectedReceiver = expectedReceiverOpt.getOrElse(violation(""))
+                    val expectedInvoke = PInvoke(PDot(expectedReceiver, n.id), expectedArgs, None)
+
+                    if (n.isPure) {
+                      block.nonEmptyStmts match {
+                        case Vector(PReturn(Vector(ret))) =>
+                          pureImplementationProofHasRightShape(ret, _ == expectedInvoke, expectedInvoke.toString)
+
+                        case _ => successProp // already checked before
+                      }
+                    } else {
+                      implementationProofBodyHasRightShape(block, _ == expectedInvoke, expectedInvoke.toString, n.result)
+                    }
+                  }
+              }
+            }
+
+            (matchingSignature and matchingPure and receiverHasMethod and rightShape)
+              .asReason(n, "invalid method of an implementation proof")
+
+          case e => Violation.violation(s"expected a method signature of an interface, but got $e")
+        }
+      }
   }
 
   lazy val miscType: Typing[PMisc] = createTyping {
@@ -74,6 +145,8 @@ trait MiscTyping extends BaseTyping { this: TypeInfoImpl =>
     case l: PKeyedElement => miscType(l.exp)
     case l: PExpCompositeVal => exprType(l.exp)
     case l: PLitCompositeVal => expectedMiscType(l)
+
+    case _: PMethodImplementationProof => UnknownType
   }
 
   lazy val expectedMiscType: PShortCircuitMisc => Type =