diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index c5f396129..8122d9d50 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/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 diff --git a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala index 579b736ba..74f2dd9bb 100644 --- a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala +++ b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala @@ -112,6 +112,11 @@ 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) @@ -119,11 +124,6 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter "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,6 +761,8 @@ 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) @@ -766,8 +770,6 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter { "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) } } diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index d044058a1..493d67587 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/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) => diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala index 43d2a52a7..4f3ca0b4b 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala +++ b/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 + // `isGhostDef` returns true if a node is part of ghost code. However, implementation proofs are considered being + // non-ghost, independently of whether they are for a ghost or non-ghost method. Thus, implementation proofs for ghost + // and non-ghost methods are type-checked in the same way, which is unproblematic due to their syntactic restrictions. + 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 } } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala index a8fd70d43..d7c03e0f6 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala +++ b/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 = { diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MiscTyping.scala index c27b99fb9..b15f7b132 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MiscTyping.scala +++ b/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 = diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala index 5330c4cb4..70e0d7deb 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala @@ -8,8 +8,13 @@ package viper.gobra.frontend.info.implementation.typing import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} import viper.gobra.ast.frontend._ -import viper.gobra.frontend.info.base.Type.{BooleanT, ChannelModus, ChannelT, FunctionT, InterfaceT, InternalTupleT, Type, ArrayT, SliceT, MapT, SetT} +import viper.gobra.ast.frontend.{AstPattern => ap, _} +import viper.gobra.frontend.info.base.{SymbolTable => st} +import viper.gobra.frontend.info.base.Type.{ArrayT, BooleanT, ChannelModus, ChannelT, FunctionT, InterfaceT, InternalTupleT, MapT, SetT, SliceT, Type} import viper.gobra.frontend.info.implementation.TypeInfoImpl +import viper.gobra.util.Violation + +import scala.annotation.tailrec trait StmtTyping extends BaseTyping { this: TypeInfoImpl => @@ -198,6 +203,8 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl => } } + case p: PClosureImplProof => wellDefClosureImplProof(p) + case s => violation(s"$s was not handled") } @@ -217,4 +224,238 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl => res.get.result.outs map miscType zip res.get.result.outs } } + + private def nameFromParam(p: PParameter): Option[String] = p match { + case PNamedParameter(id, _) => Some(id.name) + case PExplicitGhostParameter(PNamedParameter(id, _)) => Some(id.name) + case _ => None + } + + private def wellDefClosureImplProof(p: PClosureImplProof): Messages = { + val PClosureImplProof(impl@PClosureImplements(closure, spec), b: PBlock) = p + + val func = resolve(spec.func) match { + case Some(ap.Function(_, f)) => f + case Some(ap.Closure(_, c)) => c + case _ => Violation.violation(s"expected a function or closure, but got ${spec.func}") + } + + val specArgs = if (spec.params.forall(_.key.isEmpty)) func.args.drop(spec.params.size) + else { + val paramSet = spec.paramKeys.toSet + func.args.filter(nameFromParam(_).fold(true)(!paramSet.contains(_))) + } + + val isPure = func match { + case f: st.Function => f.isPure + case c: st.Closure => c.isPure + } + + lazy val expectedCallArgs = specArgs.flatMap(nameFromParam).map(a => PNamedOperand(PIdnUse(a))) + + def isExpectedCall(i: PInvoke): Boolean = i.base == closure && i.args == expectedCallArgs + + lazy val expectedCallString: String = resolve(closure) match { + case Some(_: ap.LocalVariable) => s"$closure(${specArgs.flatMap(nameFromParam).mkString(",")}) as _" + case _ => s"$closure(${specArgs.flatMap(nameFromParam).mkString(",")}) [as _]" + } + + def wellDefIfNecessaryArgsNamed: Messages = error(spec, + s"cannot find a name for all arguments or results required by $spec", + cond = !specArgs.forall { + case _: PUnnamedParameter | PExplicitGhostParameter(_: PUnnamedParameter) => false + case _ => true + } + ) + + def wellDefIfArgNamesDoNotShadowClosure: Messages = { + val names = (func.args ++ func.result.outs).map(nameFromParam).filter(_.nonEmpty).map(_.get) + + def isShadowed(id: PIdnNode): Boolean = id match { + case _: PIdnUse | _: PIdnUnk => + val entityOutside = tryLookupAt(id, impl) + entityOutside.nonEmpty && tryLookupAt(id, id).fold(false)(_ eq entityOutside.get) && names.contains(id.name) + case _ => false + } + + def shadowedInside(n: PNode): Option[PIdnNode] = n match { + case id: PIdnNode => Some(id).filter(isShadowed) + case _ => tree.child(n).iterator.map(shadowedInside).find(_.nonEmpty).flatten + } + + val shadowed = shadowedInside(closure) + error(impl, + s"identifier ${shadowed.getOrElse("")} in $closure is shadowed by an argument or result with the same name in ${spec.func}", + shadowed.nonEmpty) + } + + def pureWellDefIfIsSinglePureReturnExpr: Messages = if (isPure) isPureBlock(b) else noMessages + + def pureWellDefIfRightShape: Messages = if (!isPure) { + noMessages + } else b.nonEmptyStmts match { + case Vector(PReturn(Vector(retExpr))) => + pureImplementationProofHasRightShape(retExpr, isExpectedCall, expectedCallString) + .asReason(retExpr, "invalid return expression of an implementation proof") + case _ => error(b, "invalid body of a pure implementation proof: expected a single return") + } + + def wellDefIfRightShape: Messages = + if (isPure) noMessages + else implementationProofBodyHasRightShape(b, isExpectedCall, expectedCallString, func.result) + .asReason(b, "invalid body of an implementation proof") + + def wellDefIfTerminationMeasuresConsistent: Messages = { + val specMeasures = func match { + case st.Function(decl, _, _) => decl.spec.terminationMeasures + case st.Closure(lit, _, _) => lit.spec.terminationMeasures + } + + lazy val callMeasures = terminationMeasuresForProofCall(p) + + // If the spec has termination measures, then the call inside the proof + // must be done with a spec that also has termination measures + if (specMeasures.isEmpty) noMessages + else error(p, s"spec ${p.impl.spec} has termination measures, so also ${closureImplProofCallAttr(p).base}" + + s"(used inside the proof) must", callMeasures.isEmpty) + } + + Seq(wellDefIfNecessaryArgsNamed, wellDefIfArgNamesDoNotShadowClosure, pureWellDefIfIsSinglePureReturnExpr, + pureWellDefIfRightShape, wellDefIfRightShape, wellDefIfTerminationMeasuresConsistent) + .iterator.find(_.nonEmpty).getOrElse(noMessages) + } + + private[typing] def pureImplementationProofHasRightShape(retExpr: PExpression, + isExpectedCall: PInvoke => Boolean, + expectedCall: String): PropertyResult = { + @tailrec + def validExpression(expr: PExpression): PropertyResult = expr match { + case invoke: PInvoke => failedProp(s"The call must be $expectedCall", !isExpectedCall(invoke)) + case f: PUnfolding => validExpression(f.op) + case _ => failedProp(s"only unfolding expressions and the call $expectedCall is allowed") + } + + validExpression(retExpr) + } + + // the body can only contain fold, unfold, and the call + private[typing] def implementationProofBodyHasRightShape(body: PBlock, + isExpectedCall: PInvoke => Boolean, + expectedCall: String, + result: PResult): PropertyResult = { + val expectedResults = result.outs.flatMap(nameFromParam).map(t => PNamedOperand(PIdnUse(t))) + + def isExpectedAssignment(ass: PAssignment): Boolean = ass match { + case PAssignment(Vector(i: PInvoke), left) => isExpectedCall(i) && expectedResults == left + case _ => false + } + + def isExpectedReturn(ret: PReturn): Boolean = ret match { + case PReturn(exps) => + if (result.outs.isEmpty) exps == Vector.empty + else if (result.outs.size != expectedResults.size) + exps == Vector.empty || (exps.size == 1 && exps.head.isInstanceOf[PInvoke] && isExpectedCall(exps.head.asInstanceOf[PInvoke])) + else exps == Vector.empty || exps == expectedResults || (exps.size == 1 && exps.head.isInstanceOf[PInvoke] && isExpectedCall(exps.head.asInstanceOf[PInvoke])) + } + + lazy val expectedReturns: Seq[String] = + if (result.outs.isEmpty) Seq("return") + else if (result.outs.size != expectedResults.size) Seq("return", s"return $expectedCall") + else Seq("return", PReturn(expectedResults).toString, s"return $expectedCall") + + lazy val expectedCallStatement = if (result.outs.isEmpty) expectedCall + else if (expectedResults.size != result.outs.size) s"return $expectedCall" + else s"${expectedResults.mkString(",")} = $expectedCall" + + lazy val lastStatement: PStatement = { + @tailrec + def aux(stmt: PStatement): PStatement = stmt match { + case seq: PSeq => aux(seq.nonEmptyStmts.last) + case block: PBlock => aux(block.nonEmptyStmts.last) + case s => s + } + + aux(body) + } + + var numOfImplemetationCalls = 0 + + def validStatements(stmts: Vector[PStatement]): PropertyResult = + PropertyResult.bigAnd(stmts.map { + case _: PUnfold | _: PFold | _: PAssert | _: PEmptyStmt => successProp + case _: PAssume | _: PInhale | _: PExhale => failedProp("Assume, inhale, and exhale are forbidden in implementation proofs") + + case b: PBlock => validStatements(b.nonEmptyStmts) + case seq: PSeq => validStatements(seq.nonEmptyStmts) + + case ass: PAssignment => + // Right now, we only allow assignments that are used for the one call + if (isExpectedAssignment(ass)) { + numOfImplemetationCalls += 1 + successProp + } else if (result.outs.isEmpty || expectedResults.size != result.outs.size) { + val reason = + if (result.outs.isEmpty) "Here, there are no out-parameters." + else "Here, not all out-parameters have a name, so they cannot be assigned to." + failedProp("An assignment must assign to all out-parameters. " + reason) + } else { + failedProp(s"The only allowed assignment is $expectedCallStatement") + } + + // A call alone can only occur if there are no result parameters + case PExpressionStmt(call: PInvoke) => + if (result.outs.nonEmpty) failedProp(s"The call '$call' is missing the out-parameters") + else if (!isExpectedCall(call)) failedProp(s"The only allowed call is $expectedCall") + else { + numOfImplemetationCalls += 1 + successProp + } + + case ret@PReturn(exps) => + // there has to be at most one return at the end of the block + if (lastStatement != ret) { + failedProp("A return must be the last statement") + } else if (isExpectedReturn(ret)) { + if (exps.size == 1 && exps.head.isInstanceOf[PInvoke] && isExpectedCall(exps.head.asInstanceOf[PInvoke])) numOfImplemetationCalls += 1 + successProp + } else failedProp(s"A return must be one of ${expectedReturns.mkString(", ")}") + + case _ => failedProp("Only fold, unfold, assert, and one call to the implementation are allowed") + }) + + val bodyHasRightShape = validStatements(body.nonEmptyStmts) + val notTooManyCalls = { + if (numOfImplemetationCalls != 1) { + failedProp(s"There must be exactly one call to the implementation " + + s"(with results and arguments in the right order '$expectedCallStatement')") + } else successProp + } + + bodyHasRightShape and notTooManyCalls + } + + /** Returns the termination measures of the spec used in the call within the body of the implementation proof */ + private def terminationMeasuresForProofCall(p: PClosureImplProof): Vector[PTerminationMeasure] = { + def measuresFromMethod(m: st.Method): Vector[PTerminationMeasure] = m match { + case st.MethodSpec(spec, _, _, _) => spec.spec.terminationMeasures + case st.MethodImpl(decl, _, _) => decl.spec.terminationMeasures + } + + resolve(closureImplProofCallAttr(p)) match { + case Some(ap.FunctionCall(callee, _)) => callee match { + case ap.Function(_, symb) => symb.decl.spec.terminationMeasures + case ap.Closure(_, symb) => symb.lit.spec.terminationMeasures + case ap.ReceivedMethod(_, _, _, symb) => measuresFromMethod(symb) + case ap.ImplicitlyReceivedInterfaceMethod(_, symb) => symb.spec.spec.terminationMeasures + case ap.MethodExpr(_, _, _, symb) => measuresFromMethod(symb) + case _ => Violation.violation("this case should be unreachable") + } + case Some(ap.ClosureCall(_, _, spec)) => resolve(spec.func) match { + case Some(ap.Function(_, f)) => f.decl.spec.terminationMeasures + case Some(ap.Closure(_, c)) => c.lit.spec.terminationMeasures + case _ => Violation.violation("this case should be unreachable") + } + case _ => Violation.violation("this case should be unreachable") + } + } } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala index 6fefc23d1..d25b98706 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala @@ -26,37 +26,6 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => body.fold(noMessages)(assignableToSpec) ++ isReceiverType.errors(miscType(receiver))(member) ++ nonVariadicArguments(args) - - 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[typing] def wellFoundedIfNeeded(member: PMember): Messages = { @@ -111,7 +80,7 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => } } - private[ghost] def isPureBlock(block: PBlock): Messages = { + private[typing] def isPureBlock(block: PBlock): Messages = { block.nonEmptyStmts match { case Vector(PReturn(Vector(ret))) => isPureExpr(ret) case b => error(block, s"For now, the body of a pure block is expected to be a single return with a pure expression, got $b instead") diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala index d2569a98c..198ce6433 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala @@ -9,7 +9,7 @@ package viper.gobra.frontend.info.implementation.typing.ghost import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, message, noMessages} import viper.gobra.ast.frontend._ import viper.gobra.frontend.info.base.SymbolTable -import viper.gobra.frontend.info.base.SymbolTable.{BuiltInMPredicate, GhostTypeMember, MPredicateImpl, MPredicateSpec, MethodSpec} +import viper.gobra.frontend.info.base.SymbolTable.{BuiltInMPredicate, GhostTypeMember, MPredicateImpl, MPredicateSpec} import viper.gobra.frontend.info.base.Type.{AdtClauseT, AssertionT, BooleanT, DeclaredT, FunctionT, PredT, Type, UnknownType} import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.frontend.info.implementation.typing.BaseTyping @@ -90,76 +90,6 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => case _ => violation("Encountered ill-formed program AST") } - 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") - } - } case _: PBackendAnnotation => noMessages } @@ -204,7 +134,6 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => case _: PMatchExpCase => UnknownType case _: PMatchExpDefault => UnknownType - case _: PMethodImplementationProof => UnknownType case _: PImplementationProofPredicateAlias => UnknownType case _: PBackendAnnotation => UnknownType } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala index 702adfbdf..995936ef6 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala @@ -6,14 +6,11 @@ package viper.gobra.frontend.info.implementation.typing.ghost -import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} +import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error} import viper.gobra.ast.frontend.{PClosureImplProof, AstPattern => ap, _} import viper.gobra.frontend.info.base.{SymbolTable => st} import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.frontend.info.implementation.typing.BaseTyping -import viper.gobra.util.Violation - -import scala.annotation.tailrec trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl => @@ -32,7 +29,6 @@ trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl => case p: PMatchAdt => assignableTo.errors(miscType(p), exprType(exp))(c) case _ => comparableTypes.errors((miscType(c.pattern), exprType(exp)))(c) }) ++ isPureExpr(exp) - case p: PClosureImplProof => wellDefClosureImplProof(p) } private[typing] def wellDefFoldable(acc: PPredicateAccess): Messages = { @@ -73,237 +69,5 @@ trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl => findCallDescendent(proof).get } - - private def wellDefClosureImplProof(p: PClosureImplProof): Messages = { - val PClosureImplProof(impl@PClosureImplements(closure, spec), b: PBlock) = p - - val func = resolve(spec.func) match { - case Some(ap.Function(_, f)) => f - case Some(ap.Closure(_, c)) => c - case _ => Violation.violation(s"expected a function or closure, but got ${spec.func}") - } - - val specArgs = if (spec.params.forall(_.key.isEmpty)) func.args.drop(spec.params.size) - else { - val paramSet = spec.paramKeys.toSet - func.args.filter(nameFromParam(_).fold(true)(!paramSet.contains(_))) - } - - val isPure = func match { - case f: st.Function => f.isPure - case c: st.Closure => c.isPure - } - - lazy val expectedCallArgs = specArgs.flatMap(nameFromParam).map(a => PNamedOperand(PIdnUse(a))) - - def isExpectedCall(i: PInvoke): Boolean = i.base == closure && i.args == expectedCallArgs - - lazy val expectedCallString: String = resolve(closure) match { - case Some(_: ap.LocalVariable) => s"$closure(${specArgs.flatMap(nameFromParam).mkString(",")}) as _" - case _ => s"$closure(${specArgs.flatMap(nameFromParam).mkString(",")}) [as _]" - } - - def wellDefIfNecessaryArgsNamed: Messages = error(spec, - s"cannot find a name for all arguments or results required by $spec", - cond = !specArgs.forall { - case _: PUnnamedParameter | PExplicitGhostParameter(_: PUnnamedParameter) => false - case _ => true - } - ) - - def wellDefIfArgNamesDoNotShadowClosure: Messages = { - val names = (func.args ++ func.result.outs).map(nameFromParam).filter(_.nonEmpty).map(_.get) - - def isShadowed(id: PIdnNode): Boolean = id match { - case _: PIdnUse | _: PIdnUnk => - val entityOutside = tryLookupAt(id, impl) - entityOutside.nonEmpty && tryLookupAt(id, id).fold(false)(_ eq entityOutside.get) && names.contains(id.name) - case _ => false - } - - def shadowedInside(n: PNode): Option[PIdnNode] = n match { - case id: PIdnNode => Some(id).filter(isShadowed) - case _ => tree.child(n).iterator.map(shadowedInside).find(_.nonEmpty).flatten - } - val shadowed = shadowedInside(closure) - error(impl, - s"identifier ${shadowed.getOrElse("")} in $closure is shadowed by an argument or result with the same name in ${spec.func}", - shadowed.nonEmpty) - } - - def pureWellDefIfIsSinglePureReturnExpr: Messages = if (isPure) isPureBlock(b) else noMessages - - def pureWellDefIfRightShape: Messages = if (!isPure) { - noMessages - } else b.nonEmptyStmts match { - case Vector(PReturn(Vector(retExpr))) => - pureImplementationProofHasRightShape(retExpr, isExpectedCall, expectedCallString) - .asReason(retExpr, "invalid return expression of an implementation proof") - case _ => error(b, "invalid body of a pure implementation proof: expected a single return") - } - - def wellDefIfRightShape: Messages = - if (isPure) noMessages - else implementationProofBodyHasRightShape(b, isExpectedCall, expectedCallString, func.result) - .asReason(b, "invalid body of an implementation proof") - - def wellDefIfTerminationMeasuresConsistent: Messages = { - val specMeasures = func match { - case st.Function(decl, _, _) => decl.spec.terminationMeasures - case st.Closure(lit, _, _) => lit.spec.terminationMeasures - } - - lazy val callMeasures = terminationMeasuresForProofCall(p) - - // If the spec has termination measures, then the call inside the proof - // must be done with a spec that also has termination measures - if (specMeasures.isEmpty) noMessages - else error(p, s"spec ${p.impl.spec} has termination measures, so also ${closureImplProofCallAttr(p).base}" + - s"(used inside the proof) must", callMeasures.isEmpty) - } - - Seq(wellDefIfNecessaryArgsNamed, wellDefIfArgNamesDoNotShadowClosure, pureWellDefIfIsSinglePureReturnExpr, - pureWellDefIfRightShape, wellDefIfRightShape, wellDefIfTerminationMeasuresConsistent) - .iterator.find(_.nonEmpty).getOrElse(noMessages) - } - - private def nameFromParam(p: PParameter): Option[String] = p match { - case PNamedParameter(id, _) => Some(id.name) - case PExplicitGhostParameter(PNamedParameter(id, _)) => Some(id.name) - case _ => None - } - - private [ghost] def pureImplementationProofHasRightShape(retExpr: PExpression, - isExpectedCall: PInvoke => Boolean, - expectedCall: String): PropertyResult = { - @tailrec - def validExpression(expr: PExpression): PropertyResult = expr match { - case invoke: PInvoke => failedProp(s"The call must be $expectedCall", !isExpectedCall(invoke)) - case f: PUnfolding => validExpression(f.op) - case _ => failedProp(s"only unfolding expressions and the call $expectedCall is allowed") - } - - validExpression(retExpr) - } - - // the body can only contain fold, unfold, and the call - private [ghost] def implementationProofBodyHasRightShape(body: PBlock, - isExpectedCall: PInvoke => Boolean, - expectedCall: String, - result: PResult): PropertyResult = { - val expectedResults = result.outs.flatMap(nameFromParam).map(t => PNamedOperand(PIdnUse(t))) - - def isExpectedAssignment(ass: PAssignment): Boolean = ass match{ - case PAssignment(Vector(i: PInvoke), left) if isExpectedCall(i) && expectedResults == left => true - case _ => false - } - - def isExpectedReturn(ret: PReturn): Boolean = ret match { - case PReturn(exps) => - if (result.outs.isEmpty) exps == Vector.empty - else if (result.outs.size != expectedResults.size) - exps == Vector.empty || (exps.size == 1 && exps.head.isInstanceOf[PInvoke] && isExpectedCall(exps.head.asInstanceOf[PInvoke])) - else exps == Vector.empty || exps == expectedResults || (exps.size == 1 && exps.head.isInstanceOf[PInvoke] && isExpectedCall(exps.head.asInstanceOf[PInvoke])) - } - - lazy val expectedReturns: Seq[String] = - if (result.outs.isEmpty) Seq("return") - else if (result.outs.size != expectedResults.size) Seq("return", s"return $expectedCall") - else Seq("return", PReturn(expectedResults).toString, s"return $expectedCall") - - lazy val expectedCallStatement = if (result.outs.isEmpty) expectedCall - else if (expectedResults.size != result.outs.size) s"return $expectedCall" - else s"${expectedResults.mkString(",")} = $expectedCall" - - lazy val lastStatement: PStatement = { - @tailrec - def aux(stmt: PStatement): PStatement = stmt match { - case seq: PSeq => aux(seq.nonEmptyStmts.last) - case block: PBlock => aux(block.nonEmptyStmts.last) - case s => s - } - aux(body) - } - - var numOfImplemetationCalls = 0 - - def validStatements(stmts: Vector[PStatement]): PropertyResult = - PropertyResult.bigAnd(stmts.map { - case _: PUnfold | _: PFold | _: PAssert | _: PEmptyStmt => successProp - case _: PAssume | _: PInhale | _: PExhale => failedProp("Assume, inhale, and exhale are forbidden in implementation proofs") - - case b: PBlock => validStatements(b.nonEmptyStmts) - case seq: PSeq => validStatements(seq.nonEmptyStmts) - - case ass: PAssignment => - // Right now, we only allow assignments that are used for the one call - if (isExpectedAssignment(ass)) { - numOfImplemetationCalls += 1 - successProp - } else if (result.outs.isEmpty || expectedResults.size != result.outs.size) { - val reason = - if (result.outs.isEmpty) "Here, there are no out-parameters." - else "Here, not all out-parameters have a name, so they cannot be assigned to." - failedProp("An assignment must assign to all out-parameters. " + reason) - } else { - failedProp(s"The only allowed assignment is $expectedCallStatement") - } - - // A call alone can only occur if there are no result parameters - case PExpressionStmt(call: PInvoke) => - if (result.outs.nonEmpty) failedProp(s"The call '$call' is missing the out-parameters") - else if (!isExpectedCall(call)) failedProp(s"The only allowed call is $expectedCall") - else { - numOfImplemetationCalls += 1 - successProp - } - - case ret@PReturn(exps) => - // there has to be at most one return at the end of the block - if (lastStatement != ret) { - failedProp("A return must be the last statement") - } else if (isExpectedReturn(ret)) { - if (exps.size == 1 && exps.head.isInstanceOf[PInvoke] && isExpectedCall(exps.head.asInstanceOf[PInvoke])) numOfImplemetationCalls += 1 - successProp - } else failedProp(s"A return must be one of ${expectedReturns.mkString(", ")}") - - case _ => failedProp("Only fold, unfold, assert, and one call to the implementation are allowed") - }) - - val bodyHasRightShape = validStatements(body.nonEmptyStmts) - val notTooManyCalls = { - if (numOfImplemetationCalls != 1) { - failedProp(s"There must be exactly one call to the implementation " + - s"(with results and arguments in the right order '$expectedCallStatement')") - } else successProp - } - - bodyHasRightShape and notTooManyCalls - } - - /** Returns the termination measures of the spec used in the call within the body of the implementation proof */ - private def terminationMeasuresForProofCall(p: PClosureImplProof): Vector[PTerminationMeasure] = { - def measuresFromMethod(m: st.Method): Vector[PTerminationMeasure] = m match { - case st.MethodSpec(spec, _, _, _) => spec.spec.terminationMeasures - case st.MethodImpl(decl, _, _) => decl.spec.terminationMeasures - } - resolve(closureImplProofCallAttr(p)) match { - case Some(ap.FunctionCall(callee, _)) => callee match { - case ap.Function(_, symb) => symb.decl.spec.terminationMeasures - case ap.Closure(_, symb) => symb.lit.spec.terminationMeasures - case ap.ReceivedMethod(_, _, _, symb) => measuresFromMethod(symb) - case ap.ImplicitlyReceivedInterfaceMethod(_, symb) => symb.spec.spec.terminationMeasures - case ap.MethodExpr(_, _, _, symb) => measuresFromMethod(symb) - case _ => Violation.violation("this case should be unreachable") - } - case Some(ap.ClosureCall(_, _, spec)) => resolve(spec.func) match { - case Some(ap.Function(_, f)) => f.decl.spec.terminationMeasures - case Some(ap.Closure(_, c)) => c.lit.spec.terminationMeasures - case _ => Violation.violation("this case should be unreachable") - } - case _ => Violation.violation("this case should be unreachable") - } - } - } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala index 039e9ea39..8670e27d9 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala @@ -70,6 +70,7 @@ class GhostLessPrinter(classifier: GhostClassifier) extends DefaultPrettyPrinter case n: PProofAnnotation => n match { case n: POutline => showStmt(n.body) + case _: PClosureImplProof => ghostToken } case s if classifier.isStmtGhost(s) => ghostToken diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostWellDef.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostWellDef.scala index 7c9f161d1..ad1b2d94f 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostWellDef.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostWellDef.scala @@ -11,7 +11,7 @@ import viper.gobra.ast.frontend._ import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.ast.frontend.{AstPattern => ap} import viper.gobra.frontend.info.base.SymbolTable.{Closure, Function, Regular, SingleLocalVariable} -import viper.gobra.frontend.info.base.Type.GhostPointerT +import viper.gobra.frontend.info.base.Type.{ActualPointerT, GhostPointerT} import viper.gobra.util.Violation import viper.gobra.util.Violation.violation @@ -102,15 +102,6 @@ trait GhostWellDef { this: TypeInfoImpl => private def exprGhostSeparation(expr: PExpression): Messages = expr match { case _: PGhostExpression => noMessages - case e if isEnclosingGhost(e) => - e match { - case PMake(_: PGhostSliceType, _) => noMessages - case _: PMake => error(e, "Allocating memory within ghost code is forbidden") - case _: PNew => - Violation.violation(exprType(e).isInstanceOf[GhostPointerT], s"All memory allocated within ghost code must be located on the ghost heap") - noMessages - case _ => noMessages - } case _: PDot | _: PDeref @@ -134,24 +125,38 @@ trait GhostWellDef { this: TypeInfoImpl => case n@ ( // these are just suggestions for now. We will have to adapt then, when we decide on proper ghost separation rules. _: PReceive - ) => error(n, "ghost error: Found ghost child expression, but expected none", !noGhostPropagationFromChildren(n)) + ) => error(n, "ghost error: Found ghost child expression, but expected none", !isEnclosingGhost(n) && !noGhostPropagationFromChildren(n)) case n: PInvoke => (exprOrType(n.base), resolve(n)) match { case (Right(_), Some(_: ap.Conversion)) => noMessages - case (Left(_), Some(call: ap.FunctionCall)) => ghostAssignableToCallExpr(call) + case (Left(_), Some(call: ap.FunctionCall)) => + error(n, "ghost error: Found call to non-ghost impure function in ghost code", + // call must be in a ghost context and callee must be actual and impure + isEnclosingGhost(n) && !calleeGhostTyping(call).isGhost && isPureExpr(n).nonEmpty) ++ + ghostAssignableToCallExpr(call) case (Left(_), Some(call: ap.ClosureCall)) => ghostAssignableToClosureCall(call) case (Left(_), Some(_: ap.PredicateCall)) => noMessages case (Left(_), Some(_: ap.PredExprInstance)) => noMessages case _ => violation("expected conversion, function call, or predicate call") } - case _: PNew => noMessages - - case n@PMake(_, args) => error( - n, - "ghost error: make expressions may not contain ghost expressions", - args exists (x => !noGhostPropagationFromChildren(x)) - ) + case e: PNew => + if (isEnclosingGhost(e)) { + Violation.violation(exprType(e).isInstanceOf[GhostPointerT], s"Cannot allocate non-ghost memory in ghost code.") + } else { + Violation.violation(exprType(e).isInstanceOf[ActualPointerT], s"Cannot allocate ghost memory in non-ghost code.") + } + noMessages + + case e: PMake => (e, isEnclosingGhost(e)) match { + case (PMake(_: PGhostSliceType, _), true) => noMessages + case (_, true) => error(e, "Allocating memory with make within ghost code is forbidden") + case (PMake(_, args), false) => error( + e, + "ghost error: make expressions may not contain ghost expressions", + args exists (x => !noGhostPropagationFromChildren(x)) + ) + } } private def typeGhostSeparation(typ: PType): Messages = typ match { diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala index a6606258a..8ec804f85 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala @@ -233,6 +233,7 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter { case n: PProofAnnotation => n match { case n: POutline => showSpec(n.spec) <> specComment <> "outline (" <> line <> showStmt(n.body) <> line <> specComment <> ")" <> line + case PClosureImplProof(impl, PBlock(stmts)) => blockSpecComment("proof" <+> showExpr(impl) <> block(showStmtList(stmts))) } case _ => super.showStmt(stmt) diff --git a/src/test/resources/regressions/features/closures/closures-fail5-proofs.gobra b/src/test/resources/regressions/features/closures/closures-fail5-proofs.gobra index e7329075c..0472c288d 100644 --- a/src/test/resources/regressions/features/closures/closures-fail5-proofs.gobra +++ b/src/test/resources/regressions/features/closures/closures-fail5-proofs.gobra @@ -66,8 +66,7 @@ func test4() { //:: ExpectedOutput(type_error) proof cl implements pspec { - //:: ExpectedOutput(type_error) - x = 2 // assignment in ghost code to a non-ghost variable + x = 2 y = cl1(x) as id1 } } diff --git a/src/test/resources/regressions/features/ghost_pointer/ghost-pointer-receiver-fail01.gobra b/src/test/resources/regressions/features/ghost_pointer/ghost-pointer-receiver-fail01.gobra new file mode 100644 index 000000000..534034884 --- /dev/null +++ b/src/test/resources/regressions/features/ghost_pointer/ghost-pointer-receiver-fail01.gobra @@ -0,0 +1,156 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostPointerReceiverFail01 + +type Foo struct { + field int +} + +decreases +func ActualFunc() { + p := &Foo{ 42 } + + p.ActualPointerReceiver() + (*p).ActualPointerReceiver() + (*Foo).ActualPointerReceiver(p) + //:: ExpectedOutput(type_error) + (Foo).ActualPointerReceiver(p) + + //:: ExpectedOutput(type_error) + p.GhostPointerReceiver() // fails because method expects a ghost pointer receiver + //:: ExpectedOutput(type_error) + (*p).GhostPointerReceiver() // fails because method expects a ghost pointer receiver + //:: ExpectedOutput(type_error) + (*Foo).GhostPointerReceiver(p) // fails because method expects a ghost pointer receiver + //:: ExpectedOutput(type_error) + (Foo).GhostPointerReceiver(p) // fails because method expects a ghost pointer receiver + // since `gpointer[Foo]` is a ghost type literal instead of a type literal, we currently do not support parsing the following line: + // (gpointer[Foo]).GhostPointerReceiver(p) + + p.ActualNonPointerReceiver() + (*p).ActualNonPointerReceiver() + (*Foo).ActualNonPointerReceiver(p) + //:: ExpectedOutput(type_error) + (Foo).ActualNonPointerReceiver(p) + (Foo).ActualNonPointerReceiver(*p) + + p.GhostNonPointerReceiver() // p is implicitly dereferenced + (*p).GhostNonPointerReceiver() + (*Foo).GhostNonPointerReceiver(p) + //:: ExpectedOutput(type_error) + (Foo).GhostNonPointerReceiver(p) + (Foo).GhostNonPointerReceiver(*p) +} + +ghost +decreases +requires acc(p) +func GhostFunc(p *Foo) { + gp := &Foo{ 42 } + + //:: ExpectedOutput(type_error) + p.ActualPointerReceiver() // actual calls not permitted in ghost code + //:: ExpectedOutput(type_error) + (*p).ActualPointerReceiver() // actual calls not permitted in ghost code + //:: ExpectedOutput(type_error) + (*Foo).ActualPointerReceiver(p) // actual calls not permitted in ghost code & p being ghost is not assignable to a non-ghost receiver + //:: ExpectedOutput(type_error) + (Foo).ActualPointerReceiver(p) // actual calls not permitted in ghost code + + //:: ExpectedOutput(type_error) + p.GhostPointerReceiver() // fails because method expects a ghost pointer receiver + gp.GhostPointerReceiver() + //:: ExpectedOutput(type_error) + (*p).GhostPointerReceiver() // fails because method expects a ghost pointer receiver + //:: ExpectedOutput(type_error) + (*gp).GhostPointerReceiver() // fails because we do not add `gpointer[T]` receivers to method set of T + //:: ExpectedOutput(type_error) + (*Foo).GhostPointerReceiver(p) // fails because method expects a ghost pointer receiver + //:: ExpectedOutput(type_error) + (*Foo).GhostPointerReceiver(gp) // fails because `gpointer[T]` receivers are not part of the method set of *T + //:: ExpectedOutput(type_error) + (Foo).GhostPointerReceiver(p) // fails because method expects a ghost pointer receiver + //:: ExpectedOutput(type_error) + (Foo).GhostPointerReceiver(gp) // fails because we do not add `gpointer[T]` receivers to method set of T + // since `gpointer[Foo]` is a ghost type literal instead of a type literal, we currently do not support parsing the following line: + // (gpointer[Foo]).GhostPointerReceiver(p) + + //:: ExpectedOutput(type_error) + p.ActualNonPointerReceiver() // actual calls not permitted in ghost code + //:: ExpectedOutput(type_error) + (*p).ActualNonPointerReceiver() // actual calls not permitted in ghost code + //:: ExpectedOutput(type_error) + (*Foo).ActualNonPointerReceiver(p) // actual calls not permitted in ghost code + //:: ExpectedOutput(type_error) + (Foo).ActualNonPointerReceiver(p) // actual calls not permitted in ghost code + //:: ExpectedOutput(type_error) + (Foo).ActualNonPointerReceiver(*p) // actual calls not permitted in ghost code + + p.GhostNonPointerReceiver() // p is implicitly dereferenced + gp.GhostNonPointerReceiver() // gp is implicitly dereferenced + (*p).GhostNonPointerReceiver() + (*gp).GhostNonPointerReceiver() + (*Foo).GhostNonPointerReceiver(p) + //:: ExpectedOutput(type_error) + (*Foo).GhostNonPointerReceiver(gp) // gp is not of type *Foo + //:: ExpectedOutput(type_error) + (*Foo).GhostNonPointerReceiver(*gp) // ghost Foo is not assignable to *Foo + //:: ExpectedOutput(type_error) + (Foo).GhostNonPointerReceiver(p) // *Foo is not assignable to Foo + //:: ExpectedOutput(type_error) + (Foo).GhostNonPointerReceiver(gp) // gpointer[Foo] is not assignable to Foo + (Foo).GhostNonPointerReceiver(*p) + (Foo).GhostNonPointerReceiver(*gp) +} + +ghost +decreases +preserves acc(r) +func (r gpointer[Foo]) GhostPointerReceiver() int { + r.field = 0 + return r.field +} + +decreases +preserves acc(r) +func (r *Foo) ActualPointerReceiver() int { + r.field = 0 + return r.field +} + +ghost +decreases +func (r Foo) GhostNonPointerReceiver() int { + r.field = 42 + return r.field +} + +decreases +func (r Foo) ActualNonPointerReceiver() int { + r.field = 42 + return r.field +} + +decreases +preserves acc(r) +//:: ExpectedOutput(type_error) +func (r gpointer[Foo]) ActualGhostPointerReceiver() int { // a receiver of type ghostpointer is only allowed for ghost methods + r.field = 0 + return r.field +} + +decreases +preserves acc(r) +func ActualMethodWithGhostPointerParam(ghost r gpointer[Foo]) (ghost res int) { // actual methods can take a ghostpointer as a ghost parameter + r.field = 0 + return r.field +} + +ghost +decreases +func (r *Foo) GhostActualPointerReceiver() int { + //:: ExpectedOutput(type_error) + r.field = 0 // fails since we're trying to modify actual memory + return r.field +} diff --git a/src/test/resources/regressions/features/ghost_pointer/ghost-write-fail02.gobra b/src/test/resources/regressions/features/ghost_pointer/ghost-write-fail02.gobra new file mode 100644 index 000000000..79b2cd1b5 --- /dev/null +++ b/src/test/resources/regressions/features/ghost_pointer/ghost-write-fail02.gobra @@ -0,0 +1,39 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package GhostWriteFail02 + +// this testcase checks that an actual method cannot be called within ghost code as this method might modify +// non-ghost memory. + +decreases +requires acc(x) +func foo(x *int) { + *x = 0 +} + +ghost +decreases +requires acc(x) +func bar(x *int) { + // the following two calls are type-checked in the same way as we are already in a ghost context. + // each call technically results in two type errors, i.e., (1) calling a non-ghost method in a ghost context and + // (2) assigning a ghost variable `x` to a non-ghost parameter. + + //:: ExpectedOutput(type_error) + ghost foo(x) + + //:: ExpectedOutput(type_error) + foo(x) +} + +decreases +requires acc(x) +func bar2(x *int) { + // the following call fails because we call a non-ghost method in a ghost context: + //:: ExpectedOutput(type_error) + ghost foo(x) + + // this is fine since we are in a non-ghost context: + foo(x) +} diff --git a/src/test/resources/regressions/features/interfaces/ghostnessOfImplementation-fail1.gobra b/src/test/resources/regressions/features/interfaces/ghostnessOfImplementation-fail1.gobra new file mode 100644 index 000000000..e9bc60d14 --- /dev/null +++ b/src/test/resources/regressions/features/interfaces/ghostnessOfImplementation-fail1.gobra @@ -0,0 +1,65 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// this test makes sure that a method's implementation has the same ghostness as specified in the interface + +package pkg + +type itfWithActualMethod interface { + decreases + actualMethod() int +} + +type itfWithActualPureMethod interface { + decreases + pure actualPureMethod() int +} + +type itfWithGhostMethod interface { + ghost + decreases + ghostMethod() int +} + +type itfWithGhostPureMethod interface { + ghost + decreases + pure ghostPureMethod() int +} + +type someImplementation struct { + value int +} + +// checks that `someImplementation` is indeed considered an implementation of each interface, i.e., that the ghost +// attribute in the interface and implementation is correctly handled. +//:: ExpectedOutput(type_error) +*someImplementation implements itfWithActualMethod +//:: ExpectedOutput(type_error) +*someImplementation implements itfWithActualPureMethod +//:: ExpectedOutput(type_error) +*someImplementation implements itfWithGhostMethod +//:: ExpectedOutput(type_error) +*someImplementation implements itfWithGhostPureMethod + +ghost +decreases +func (impl *someImplementation) actualMethod() int { + return 42 +} + +ghost +decreases +pure func (impl *someImplementation) actualPureMethod() int { + return 42 +} + +decreases +func (impl *someImplementation) ghostMethod() int { + return 42 +} + +decreases +pure func (impl *someImplementation) ghostPureMethod() int { + return 42 +} diff --git a/src/test/resources/regressions/features/options/options-simple3.gobra b/src/test/resources/regressions/features/options/options-simple3.gobra index 10336b9e3..ced533d84 100644 --- a/src/test/resources/regressions/features/options/options-simple3.gobra +++ b/src/test/resources/regressions/features/options/options-simple3.gobra @@ -13,15 +13,19 @@ func test2(b bool) { assert mset(some(b)) == mset[bool] { b } } +ghost +decreases requires opt != none[int] ensures set(opt) == set[int] { get(opt) } func lemma_set_some(ghost opt option[int]) { } +ghost +decreases requires set(opt) == set[int] { } ensures opt == none[int] func lemma_set_empty(ghost opt option[int]) { - ghost if (opt != none[int]) { + if (opt != none[int]) { lemma_set_some(opt) } } diff --git a/src/test/resources/regressions/issues/000037.gobra b/src/test/resources/regressions/issues/000037-1.gobra similarity index 62% rename from src/test/resources/regressions/issues/000037.gobra rename to src/test/resources/regressions/issues/000037-1.gobra index 6bdc8d3c7..d92838bb5 100644 --- a/src/test/resources/regressions/issues/000037.gobra +++ b/src/test/resources/regressions/issues/000037-1.gobra @@ -8,12 +8,17 @@ type Rectangle struct { } ghost +decreases pure func GetHeight(r Rectangle) (res int) { return r.Height } func main() { + someActualVariable := 42 r := Rectangle{Width: 2, Height: 5} h := GetHeight(r) assert h == GetHeight(r) && h == 5 -} \ No newline at end of file + // h is implicitly a ghost variable. Thus, the following assignment (to a non-ghost variable) should fail: + //:: ExpectedOutput(type_error) + someActualVariable = h +} diff --git a/src/test/resources/regressions/issues/000037-2.gobra b/src/test/resources/regressions/issues/000037-2.gobra new file mode 100644 index 000000000..b5025cc6d --- /dev/null +++ b/src/test/resources/regressions/issues/000037-2.gobra @@ -0,0 +1,29 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package main + +ghost +decreases x +pure func more(x int) int { + return x <= 0 ? 1 : more(x - 2) + 3 +} + +ghost /* lemma */ +decreases x +ensures x < more(x) +func increasing(x int) + +// returning b (a ghost variable) is not allowed as this is an actual function +//:: ExpectedOutput(type_error) +func exampleLemmaUse(a int) int { + increasing(a) + b := more(a) + c := more(b) + if a < 1000 { + increasing(more(a)) + assert 2 <= c - a + } + assert 2 <= c - a || 200 <= a + return b +} diff --git a/src/test/resources/regressions/issues/000420.gobra b/src/test/resources/regressions/issues/000420.gobra new file mode 100644 index 000000000..9310fc262 --- /dev/null +++ b/src/test/resources/regressions/issues/000420.gobra @@ -0,0 +1,17 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue420 + +func foo() int { + ghost bar := true + var baz int + ghost if bar { + //:: ExpectedOutput(type_error) + baz = 1 + } else { + //:: ExpectedOutput(type_error) + baz = 0 + } + return baz +}