diff --git a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala index 39381eb8b..df062080c 100644 --- a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala +++ b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala @@ -133,7 +133,7 @@ object ImpureAssumeRewriter { assert(conds.isEmpty) assert(cond.isEmpty) - PermGeCmp(permLoc, perm)() + PermGeCmp(permLoc, perm)(permLoc.pos, permLoc.info, permLoc.errT) } else { val perms: Seq[Exp] = (contextWithoutRcv map (_._2)) :+ perm @@ -146,7 +146,7 @@ object ImpureAssumeRewriter { val func = funcs(contextWithoutRcv.length-1) val funcApp = DomainFuncApp(func, conds ++ perms, Map[TypeVar, Type]())() - PermGeCmp(permLoc, funcApp)() + PermGeCmp(permLoc, funcApp)(permLoc.pos, permLoc.info, permLoc.errT) } } diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala index 68eafdb55..3ed93527f 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontend.scala +++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala @@ -107,6 +107,7 @@ trait SilFrontend extends DefaultFrontend { "viper.silver.plugin.standard.adt.AdtPlugin", "viper.silver.plugin.standard.termination.TerminationPlugin", "viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin", + "viper.silver.plugin.standard.reasoning.ReasoningPlugin", refutePlugin ) diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala index 539a80fa8..614548a5e 100644 --- a/src/main/scala/viper/silver/parser/ParseAst.scala +++ b/src/main/scala/viper/silver/parser/ParseAst.scala @@ -1467,7 +1467,7 @@ case class PNewExp(keyword: PKw.New, fields: PGrouped.Paren[Either[PSym.Star, PD def forceSubstitution(ts: PTypeSubstitution) = {} } -sealed trait PScope extends PNode { +trait PScope extends PNode { val scopeId = PScope.uniqueId() } diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/BeforeVerifyHelper.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/BeforeVerifyHelper.scala new file mode 100644 index 000000000..1a268c33c --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/BeforeVerifyHelper.scala @@ -0,0 +1,163 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2024 ETH Zurich. + +package viper.silver.plugin.standard.reasoning + + +import viper.silver.ast.utility.Expressions +import viper.silver.ast.{Apply, Exhale, Exp, FieldAssign, Fold, Inhale, LocalVarDecl, Method, MethodCall, Package, Program, Seqn, Stmt, Unfold} +import viper.silver.verifier.{AbstractError, ConsistencyError} +import viper.silver.plugin.standard.reasoning.analysis.AnalysisUtils +import viper.silver.plugin.standard.reasoning.analysis.AnalysisUtils.{AssumeInfluenceSink, InfluenceSink} + +import scala.collection.mutable + +trait BeforeVerifyHelper { + /** methods to rename variables for the encoding of the new syntax */ + def uniqueName(name: String, usedNames: mutable.Set[String]): String = { + var i = 1 + var newName = name + while (usedNames.contains(newName)) { + newName = name + i + i += 1 + } + usedNames.add(newName) + newName + } + + def substituteWithFreshVars[E <: Exp](vars: Seq[LocalVarDecl], exp: E, usedNames: mutable.Set[String]): (Seq[(LocalVarDecl, LocalVarDecl)], E) = { + val declMapping = vars.map(oldDecl => + oldDecl -> LocalVarDecl(uniqueName(oldDecl.name, usedNames), oldDecl.typ)(oldDecl.pos, oldDecl.info, oldDecl.errT)) + val transformedExp = applySubstitution(declMapping, exp) + (declMapping, transformedExp) + } + + def applySubstitution[E <: Exp](mapping: Seq[(LocalVarDecl, LocalVarDecl)], exp: E): E = { + Expressions.instantiateVariables(exp, mapping.map(_._1.localVar), mapping.map(_._2.localVar)) + } + + def applySubstitutionWithExp[E <: Exp](mapping: Seq[(LocalVarDecl, Exp)], exp: E): E = { + Expressions.instantiateVariables(exp, mapping.map(_._1.localVar), mapping.map(_._2)) + } + + /** + * check that all variables (`modified_vars`) that are assigned to inside a universal introduction `u`'s block are + * distinct from the universal introduction `u`'s quantified variables `quantified_vars`. Otherwise, an error is + * reported via `reportError` since these quantified variables should be immutable. + * + * @param modified_vars: set of variables that were modified in a given statement + * @param quantified_vars: set of quantified variables in the universal introduction statement. + * @param reportError: Method to report the error when a qunatified variable was modified + * @param u: universal introduction statement, used for details in error message + */ + def checkReassigned(modified_vars: Set[LocalVarDecl], quantified_vars: Seq[LocalVarDecl], reportError: AbstractError => Unit, u: UniversalIntro): Unit = { + val reassigned_vars: Set[LocalVarDecl] = modified_vars.intersect(quantified_vars.toSet) + if (reassigned_vars.nonEmpty) { + val reassigned_names: String = reassigned_vars.mkString(", ") + val reassigned_pos: String = reassigned_vars.map(_.pos).mkString(", ") + reportError(ConsistencyError("Universal Introduction variable(s) (" + reassigned_names + ") might have been reassigned at position(s) (" + reassigned_pos + ")", u.pos)) + } + } + + /** returns true if method `m` is annotated to be a lemma */ + def specifiesLemma(m: Method): Boolean = (m.pres ++ m.posts).exists { + case _: Lemma => true + case _ => false + } + + /** Checks that all lemmas in `input` satisfy the syntactical restrictions and, otherwise, reports errors by invoking `reportError`. */ + def checkLemmas(input: Program, reportError: AbstractError => Unit): Unit = { + input.methods.foreach(method => { + val containsLemma = specifiesLemma(method) + val terminationSpecState = AnalysisUtils.specifiesTermination(method) + + if (containsLemma) { + // lemmas must terminate. We report slightly different errors depending on the cause: + if (!terminationSpecState.guaranteesTermination) { + if (terminationSpecState.noTerminationSpec) { + reportError(ConsistencyError(s"Lemmas must terminate but method ${method.name} marked lemma does not specify any termination measures", method.pos)) + } else { + reportError(ConsistencyError(s"Lemmas must terminate but the specification of method ${method.name} might not guarantee termination", method.pos)) + } + } + + /** check method body for impure statements */ + checkStmtPure(method.body.getOrElse(Seqn(Seq.empty, Seq.empty)()), method, input, reportError) + } + }) + } + + /** checks whether a statement `stmt` is pure, reports error if impure operation found */ + def checkStmtPure(stmt: Stmt, method: Method, prog: Program, reportError: AbstractError => Unit): Boolean = { + stmt match { + case Seqn(ss, _) => + ss.forall(s => checkStmtPure(s, method, prog, reportError)) + + /** case for statements considered impure */ + case ie@(Inhale(_) | Exhale(_) | FieldAssign(_, _) | Fold(_) | Unfold(_) | Apply(_) | Package(_, _)) => + reportError(ConsistencyError(s"method ${method.name} marked lemma might contain impure statement $ie", ie.pos)) + false + case m@MethodCall(methodName, _, _) => + val mc = prog.findMethod(methodName) + val isLemmaCall = specifiesLemma(mc) + + /** if called method is not a lemma report error */ + if (!isLemmaCall) { + reportError(ConsistencyError(s"method ${method.name} marked lemma might contain call to method $m", m.pos)) + } + isLemmaCall + case _ => true + } + } + + /** checks that all influences by annotations in `input` are used correctly. */ + def checkInfluencedBy(input: Program, reportError: AbstractError => Unit): Unit = { + input.methods.foreach(method => { + val argSources = method.formalArgs.map(AnalysisUtils.getSourceFromVarDecl).toSet + AnalysisUtils.HeapSource + val retSinks = method.formalReturns.map(AnalysisUtils.getSinkFromVarDecl).toSet + AnalysisUtils.HeapSink + AnalysisUtils.AssumeMethodInfluenceSink(method) + + val seenSinks: mutable.Set[InfluenceSink] = mutable.Set.empty + /** iterate through method postconditions to find flow annotations */ + method.posts.foreach { + case v@InfluencedBy(target, args) => + val declaredSink = AnalysisUtils.getSinkFromFlowVar(target, method) + + if (!retSinks.contains(declaredSink)) { + reportError(ConsistencyError(s"Only return parameters, the heap or assumes can be influenced but not ${declaredSink.name}.", v.pos)) + } + if (seenSinks.contains(declaredSink)) { + reportError(ConsistencyError(s"Only one influenced-by specification per return parameter, heap or assume is allowed. ${declaredSink.name} is used several times.", v.pos)) + } + seenSinks.add(declaredSink) + + args.foreach(arg => { + val declaredSource = AnalysisUtils.getSourceFromFlowVar(arg) + if (!argSources.contains(declaredSource)) { + reportError(ConsistencyError(s"Only method input parameters or the heap can be sources of influenced-by specifications but not ${declaredSource.name}.", v.pos)) + } + }) + case _ => + } + + // checks that "assume influeced by" and "assumesNothing" are mutually exclusive: + val assumeNothings = method.posts.collect { + // case InfluencedBy(_: Assumes, _) => + case a: AssumesNothing => a + } + val hasAssumeInfluenceSink = seenSinks.exists { + case _: AssumeInfluenceSink => true + case _ => false + } + if (assumeNothings.length > 1) { + assumeNothings.foreach(a => + reportError(ConsistencyError(s"At most one '${PNothingKeyword.keyword}' permitted per method specification.", a.pos))) + } else if (assumeNothings.nonEmpty && hasAssumeInfluenceSink) { + assumeNothings.foreach(a => + reportError(ConsistencyError(s"'${PNothingKeyword.keyword}' and '${PInfluencedKeyword.keyword} ${PAssumesKeyword.keyword} ${PByKeyword.keyword} ...' are mutually exclusive.", a.pos))) + } + }) + } +} diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningASTExtension.scala new file mode 100644 index 000000000..41cae3162 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningASTExtension.scala @@ -0,0 +1,175 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2024 ETH Zurich. + +package viper.silver.plugin.standard.reasoning + +import viper.silver.ast._ +import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, brackets, char, defaultIndent, group, line, nest, nil, parens, show, showBlock, showVars, space, ssep, text, toParenDoc} +import viper.silver.ast.pretty.PrettyPrintPrimitives +import viper.silver.ast.utility.Consistency +import viper.silver.verifier.{ConsistencyError, Failure, VerificationResult} + + +case object ReasoningInfo extends FailureExpectedInfo + +case class ExistentialElim(varList: Seq[LocalVarDecl], trigs: Seq[Trigger], exp: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt { + override lazy val check: Seq[ConsistencyError] = Consistency.checkPure(exp) ++ + (if (!(exp isSubtype Bool)) Seq(ConsistencyError(s"Body of existential elimination must be of Bool type, but found ${exp.typ}", exp.pos)) else Seq()) ++ + (if (varList.isEmpty) Seq(ConsistencyError("Existential elimination must have at least one quantified variable.", pos)) else Seq()) + + override lazy val prettyPrint: PrettyPrintPrimitives#Cont = { + text("obtain") <+> showVars(varList) <+> + text("where") <+> (if (trigs.isEmpty) nil else ssep(trigs map show, space)) <+> + toParenDoc(exp) + } + + override val extensionSubnodes: Seq[Node] = varList ++ trigs ++ Seq(exp) + + /** declarations contributed by this statement that should be added to the parent scope */ + override def declarationsInParentScope: Seq[Declaration] = varList +} + +case class UniversalIntro(varList: Seq[LocalVarDecl], triggers: Seq[Trigger], assumingExp: Exp, implyingExp: Exp, block: Seqn)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt with Scope { + // See also Expression Line 566 + override lazy val check: Seq[ConsistencyError] = + (if (!(assumingExp isSubtype Bool)) Seq(ConsistencyError(s"Assume expression of universal introduction must be of Bool type, but found ${assumingExp.typ}", assumingExp.pos)) else Seq()) ++ + (if (!(implyingExp isSubtype Bool)) Seq(ConsistencyError(s"Implies expression of universal introduction must be of Bool type, but found ${implyingExp.typ}", implyingExp.pos)) else Seq()) ++ + (if (varList.isEmpty) Seq(ConsistencyError("Quantifier must have at least one quantified variable.", pos)) else Seq()) ++ + Consistency.checkAllVarsMentionedInTriggers(varList, triggers) + + override val scopedDecls: Seq[Declaration] = varList + + override lazy val prettyPrint: PrettyPrintPrimitives#Cont = { + text("prove forall") <+> showVars(varList) <+> + text("assuming") <+> + toParenDoc(assumingExp) <+> + text("implies") <+> toParenDoc(implyingExp) <+> + showBlock(block) + } + + override val extensionSubnodes: Seq[Node] = varList ++ triggers ++ Seq(assumingExp, implyingExp, block) +} + +sealed trait FlowVar extends ExtensionExp { + override def extensionIsPure: Boolean = true + + override def verifyExtExp(): VerificationResult = { + assert(assertion = false, "FlowAnalysis: verifyExtExp has not been implemented.") + Failure(Seq(ConsistencyError("FlowAnalysis: verifyExtExp has not been implemented.", pos))) + } +} + +trait FlowVarOrHeap extends FlowVar + +case class Assumes()(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends FlowVar { + override val extensionSubnodes: Seq[Node] = Seq.empty + override def typ: Type = InternalType + override def prettyPrint: PrettyPrintPrimitives#Cont = PAssumesKeyword.keyword +} + +case class Heap()(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends FlowVarOrHeap { + override val extensionSubnodes: Seq[Node] = Seq.empty + override def typ: Type = InternalType + override def prettyPrint: PrettyPrintPrimitives#Cont = PHeapKeyword.keyword +} + +case class Var(decl: LocalVar)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends FlowVarOrHeap { + override val extensionSubnodes: Seq[Node] = Seq(decl) + override def typ: Type = decl.typ + override def prettyPrint: PrettyPrintPrimitives#Cont = show(decl) +} + +trait FlowAnnotation extends ExtensionExp with Node + +case class AssumesNothing()(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends FlowAnnotation { + override def extensionIsPure: Boolean = true + + override def extensionSubnodes: Seq[Node] = Seq() + + override def typ: Type = Bool + + override def verifyExtExp(): VerificationResult = { + assert(assertion = false, "FlowAnalysis: verifyExtExp has not been implemented.") + Failure(Seq(ConsistencyError("FlowAnalysis: verifyExtExp has not been implemented.", pos))) + } + + /** Pretty printing functionality as defined for other nodes in class FastPrettyPrinter. + * Sample implementation would be text("old") <> parens(show(e)) for pretty-printing an old-expression. */ + override def prettyPrint: PrettyPrintPrimitives#Cont = { + text(PNothingKeyword.keyword) + } +} + +case class InfluencedBy(v: FlowVar, varList: Seq[FlowVarOrHeap])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends FlowAnnotation with Scope { + override def extensionIsPure: Boolean = true + + override val scopedDecls: Seq[Declaration] = Seq() + + override def typ: Type = Bool + + override def verifyExtExp(): VerificationResult = { + assert(assertion = false, "FlowAnalysis: verifyExtExp has not been implemented.") + Failure(Seq(ConsistencyError("FlowAnalysis: verifyExtExp has not been implemented.", pos))) + } + + override def extensionSubnodes: Seq[Node] = Seq(v) ++ varList + + /** Pretty printing functionality as defined for other nodes in class FastPrettyPrinter. + * Sample implementation would be text("old") <> parens(show(e)) for pretty-printing an old-expression. */ + override def prettyPrint: PrettyPrintPrimitives#Cont = { + text("influenced") <+> (v match { + case value: Var => show(value.decl) + case _: Assumes => text("assumes") + case _: Heap => text("heap") + }) <+> + text("by") <+> + ssep(varList.map { + case value: Var => show(value.decl) + case _ => text("heap") + }, group(char(',') <> line(" "))) + } +} + +case class Lemma()(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionExp with Node with Scope { + override def extensionIsPure: Boolean = true + + override val scopedDecls: Seq[Declaration] = Seq() + + override def typ: Type = Bool + + override def verifyExtExp(): VerificationResult = { + assert(assertion = false, "Lemma: verifyExtExp has not been implemented.") + Failure(Seq(ConsistencyError("Lemma: verifyExtExp has not been implemented.", pos))) + } + + override def extensionSubnodes: Seq[Node] = Seq() + + /** Pretty printing functionality as defined for other nodes in class FastPrettyPrinter. + * Sample implementation would be text("old") <> parens(show(e)) for pretty-printing an old-expression. */ + override def prettyPrint: PrettyPrintPrimitives#Cont = { + text("isLemma") + } +} + +case class OldCall(methodName: String, args: Seq[Exp], rets: Seq[LocalVar], oldLabel: String)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt with Scope { + override val scopedDecls: Seq[Declaration] = Seq() + + override lazy val check: Seq[ConsistencyError] = { + (if (Consistency.noResult(this)) Seq.empty else Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", pos))) ++ + (if (Consistency.noDuplicates(rets)) Seq.empty else Seq(ConsistencyError("Targets are not allowed to have duplicates", rets.head.pos))) ++ + args.flatMap(Consistency.checkPure) + } + + override lazy val prettyPrint: PrettyPrintPrimitives#Cont = { + val call = text("oldCall") <> brackets(text(oldLabel)) <> text(methodName) <> nest(defaultIndent, parens(ssep(args map show, group(char(',') <> line)))) + rets match { + case Nil => call + case _ => ssep(rets map show, char(',') <> space) <+> ":=" <+> call + } + } + + override val extensionSubnodes: Seq[Node] = args ++ rets +} diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningErrors.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningErrors.scala new file mode 100644 index 000000000..6eea6012e --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningErrors.scala @@ -0,0 +1,39 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2024 ETH Zurich. + +package viper.silver.plugin.standard.reasoning + +import viper.silver.verifier._ +import viper.silver.verifier.reasons.ErrorNode + +case class ExistentialElimFailed(override val offendingNode: ErrorNode, override val reason: ErrorReason, override val cached: Boolean = false) extends ExtensionAbstractVerificationError { + override val id = "existential.elimination.failed" + override val text = "Existentially quantified formula might not hold." + + override def withNode(offendingNode: errors.ErrorNode = this.offendingNode): ExistentialElimFailed = + ExistentialElimFailed(this.offendingNode, this.reason, this.cached) + + override def withReason(r: ErrorReason): ExistentialElimFailed = ExistentialElimFailed(offendingNode, r, cached) +} + +case class UniversalIntroFailed(override val offendingNode: ErrorNode, override val reason: ErrorReason, override val cached: Boolean = false) extends ExtensionAbstractVerificationError { + override val id = "universal.introduction.failed" + override val text = "Specified property might not hold." + + override def withNode(offendingNode: errors.ErrorNode = this.offendingNode): UniversalIntroFailed = + UniversalIntroFailed(this.offendingNode, this.reason, this.cached) + + override def withReason(r: ErrorReason): UniversalIntroFailed = UniversalIntroFailed(offendingNode, r, cached) +} + +case class PreconditionInLemmaCallFalse(offendingNode: OldCall, reason: ErrorReason, override val cached: Boolean = false) extends ExtensionAbstractVerificationError { + val id = "lemma.call.precondition" + val text = s"The precondition of lemma ${offendingNode.methodName} might not hold." + + def withNode(offendingNode: errors.ErrorNode = this.offendingNode): PreconditionInLemmaCallFalse = PreconditionInLemmaCallFalse(offendingNode.asInstanceOf[OldCall], this.reason, this.cached) + + def withReason(r: ErrorReason): PreconditionInLemmaCallFalse = PreconditionInLemmaCallFalse(offendingNode, r, cached) +} diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPASTExtension.scala new file mode 100644 index 000000000..063f5a2e3 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPASTExtension.scala @@ -0,0 +1,234 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2024 ETH Zurich. + +package viper.silver.plugin.standard.reasoning + +import viper.silver.FastMessaging +import viper.silver.ast.{Exp, ExtensionExp, LocalVar, LocalVarDecl, Position, Seqn, Stmt, Trigger} +import viper.silver.parser.TypeHelper.Bool +import viper.silver.parser.{NameAnalyser, PAssignTarget, PCall, PCallable, PDelimited, PExp, PExtender, PGrouped, PIdnRef, PIdnUseExp, PKeywordLang, PKeywordStmt, PKw, PLabel, PLocalVarDecl, PReserved, PScope, PSeqn, PStmt, PSym, PSymOp, PTrigger, PType, PTypeSubstitution, Translator, TypeChecker} + +case object PObtainKeyword extends PKw("obtain") with PKeywordLang with PKeywordStmt +case object PWhereKeyword extends PKw("where") with PKeywordLang +case object PProveKeyword extends PKw("prove") with PKeywordLang with PKeywordStmt +case object PAssumingKeyword extends PKw("assuming") with PKeywordLang +case object PImpliesKeyword extends PKw("implies") with PKeywordLang +case object PInfluencedKeyword extends PKw("influenced") with PKeywordLang with PKw.PostSpec +case object PByKeyword extends PKw("by") with PKeywordLang +case object PHeapKeyword extends PKw("heap") with PKeywordLang +case object PAssumesKeyword extends PKw("assumes") with PKeywordLang +case object PNothingKeyword extends PKw("assumesNothing") with PKeywordLang with PKw.PostSpec +case object PIsLemmaKeyword extends PKw("isLemma") with PKeywordLang with PKw.PreSpec with PKw.PostSpec +case object POldCallKeyword extends PKw("oldCall") with PKeywordLang with PKeywordStmt + +case class PExistentialElim(obtainKw: PReserved[PObtainKeyword.type], delimitedVarDecls: PDelimited[PLocalVarDecl, PSym.Comma], whereKw: PReserved[PWhereKeyword.type], trig: Seq[PTrigger], e: PExp)(val pos: (Position, Position)) extends PExtender with PStmt { + lazy val varDecls: Seq[PLocalVarDecl] = delimitedVarDecls.toSeq + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + varDecls foreach (v => t.check(v.typ)) + trig foreach (_.exp.inner.toSeq foreach (tpe => t.checkTopTyped(tpe, None))) + t.check(e, Bool) + None + } + + override def translateStmt(t: Translator): Stmt = { + ExistentialElim( + varDecls.map { variable => LocalVarDecl(variable.idndef.name, t.ttyp(variable.typ))(t.liftPos(variable)) }, + trig.map { t1 => Trigger(t1.exp.inner.toSeq.map { t2 => t.exp(t2) })(t.liftPos(t1)) }, + t.exp(e))(t.liftPos(e)) + } +} + +case class PUniversalIntro(proveKw: PReserved[PProveKeyword.type], forallKw: PKw.Forall, delimitedVarDecls: PDelimited[PLocalVarDecl, PSym.Comma], triggers: Seq[PTrigger], assumingKw: PReserved[PAssumingKeyword.type], e1: PExp, impliesKw: PReserved[PImpliesKeyword.type], e2: PExp, block: PSeqn)(val pos: (Position, Position)) extends PExtender with PStmt with PScope { + lazy val varDecls: Seq[PLocalVarDecl] = delimitedVarDecls.toSeq + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + varDecls foreach (v => t.check(v.typ)) + triggers foreach (_.exp.inner.toSeq foreach (tpe => t.checkTopTyped(tpe, None))) + t.check(e1, Bool) + t.check(e2, Bool) + t.check(block) + None + } + + override def translateStmt(t: Translator): Stmt = { + UniversalIntro( + varDecls.map { variable => LocalVarDecl(variable.idndef.name, t.ttyp(variable.typ))(t.liftPos(variable)) }, + triggers.map { t1 => Trigger(t1.exp.inner.toSeq.map { t2 => t.exp(t2) })(t.liftPos(t1)) }, + t.exp(e1), + t.exp(e2), + t.stmt(block).asInstanceOf[Seqn])(t.liftPos(block)) + } +} + +trait PFlowAnnotation extends PExp with PExtender { + val pos: (Position,Position) +} + +case class PInfluencedBy(v: PFlowVar, byKw: PReserved[PByKeyword.type], groupedVarList: PGrouped[PSym.Brace, Seq[PFlowVarOrHeap]])(val pos: (Position,Position)) extends PFlowAnnotation { + lazy val varList: Seq[PFlowVarOrHeap] = groupedVarList.inner + + override def typeSubstitutions: Seq[PTypeSubstitution] = Seq(PTypeSubstitution.id) + + override def forceSubstitution(ts: PTypeSubstitution): Unit = {} + + override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = { + + varList.foreach { + case c: PVar => + t.checkTopTyped(c.decl, None) + case _ => + } + v match { + case c: PVar => + t.checkTopTyped(c.decl, None) + case _ => + } + + None + } + + override def translateExp(t: Translator): ExtensionExp = { + InfluencedBy(v.translate(t), varList.map { variable => variable.translate(t) })(t.liftPos(this)) + } +} + +sealed trait PFlowVar extends PExtender with PExp { + override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = typecheck(t, n) + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = None + + def translate(t: Translator): FlowVar + + override def typeSubstitutions: Seq[PTypeSubstitution] = Seq(PTypeSubstitution.id) + + override def forceSubstitution(ts: PTypeSubstitution): Unit = {} +} + +trait PFlowVarOrHeap extends PFlowVar { + + override def translate(t: Translator): FlowVarOrHeap +} + +case class PHeap(heap: PReserved[PHeapKeyword.type])(val pos: (Position,Position)) extends PFlowVarOrHeap { + override def translate(t: Translator): Heap = { + Heap()(t.liftPos(this)) + } + + override def pretty: String = PHeapKeyword.keyword +} + +case class PAssumes(assumes: PReserved[PAssumesKeyword.type])(val pos: (Position,Position)) extends PFlowVar { + override def translate(t: Translator): Assumes = { + Assumes()(t.liftPos(this)) + } + + override def pretty: String = PAssumesKeyword.keyword +} + +case class PAssumesNothing()(val pos: (Position,Position)) extends PFlowAnnotation { + def translate(t: Translator): AssumesNothing = { + AssumesNothing()(t.liftPos(this)) + } + + override def pretty: String = PNothingKeyword.keyword + override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = None + + override def translateExp(t: Translator): Exp = AssumesNothing()(t.liftPos(this)) + + override def typeSubstitutions: collection.Seq[PTypeSubstitution] = Seq(PTypeSubstitution.id) + + override def forceSubstitution(ts: PTypeSubstitution): Unit = {} +} + +case class PVar(decl: PIdnUseExp)(val pos: (Position,Position)) extends PFlowVarOrHeap { + override def translate(t: Translator): Var = { + // due to the implementation of `t.exp`, a LocalVar should be returned + Var(t.exp(decl).asInstanceOf[LocalVar])(t.liftPos(this)) + } + + override def pretty: String = decl.pretty +} + +case class PLemmaClause()(val pos: (Position,Position)) extends PExtender with PExp { + override def typeSubstitutions: Seq[PTypeSubstitution] = Seq(PTypeSubstitution.id) + + override def forceSubstitution(ts: PTypeSubstitution): Unit = {} + + override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = typecheck(t, n) + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = None + + override def translateExp(t: Translator): ExtensionExp = { + Lemma()(t.liftPos(this)) + } +} + +case class POldCall(lhs: PDelimited[PExp with PAssignTarget, PSym.Comma], op: Option[PSymOp.Assign], oldCallKw: PReserved[POldCallKeyword.type], lbl: PGrouped[PSym.Bracket, Either[PKw.Lhs, PIdnRef[PLabel]]], call: PGrouped[PSym.Paren, PCall])(val pos: (Position, Position)) extends PExtender with PStmt { + lazy val targets: Seq[PExp with PAssignTarget] = lhs.toSeq + lazy val idnref: PIdnRef[PCallable] = call.inner.idnref + lazy val args: Seq[PExp] = call.inner.args + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + args.foreach(a => + t.checkTopTyped(a, None) + ) + targets.foreach(r => + t.checkTopTyped(r, None)) + targets filter { + case _: PIdnUseExp => false + case _ => true + } foreach(target => t.messages ++= FastMessaging.message(target, s"expected an identifier but got $target")) + None + } + + override def translateStmt(t: Translator): Stmt = { + val labelName = lbl.inner.fold(_.rs.keyword, _.name) + val translatedTargets = targets.map(target => t.exp(target).asInstanceOf[LocalVar]) // due to the typecheck and the implementation of `t.exp`, a LocalVar should be returned + OldCall(idnref.name, args map t.exp, translatedTargets, labelName)(t.liftPos(this)) + } +} + +/** + * oldCall that does not assign any return parameters. + * Note that this node is only used for parsing and is translated to `POldCall` before typechecking + */ +case class POldCallStmt(oldCallKw: PReserved[POldCallKeyword.type], lbl: PGrouped[PSym.Bracket, Either[PKw.Lhs, PIdnRef[PLabel]]], funcApp: PGrouped[PSym.Paren, PCall])(val pos: (Position, Position)) extends PExtender with PStmt { + lazy val call: PCall = funcApp.inner + lazy val idnref: PIdnRef[PCallable] = call.idnref + lazy val args: Seq[PExp] = call.args + + // POldCallStmt are always transformed by `beforeResolve` in `ReasoningPlugin`. Thus, calling `typecheck` indicates a logical error + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = throw new AssertionError(s"POldCallStmt '$this' should have been transformed before typechecking") + + // we do not translate this expression but `POldCall` which is created before resolution + override def translateStmt(t: Translator): Stmt = throw new AssertionError(s"POldCallStmt '$this' should have been transformed before typechecking") +} + +/** + * Note that this node is only used for parsing and is translated to `POldCall` before typechecking + */ +case class POldCallExp(oldCallKw: PReserved[POldCallKeyword.type], lbl: PGrouped[PSym.Bracket, Either[PKw.Lhs, PIdnRef[PLabel]]], call: PGrouped[PSym.Paren, PCall])(val pos: (Position, Position)) extends PExtender with PExp { + lazy val idnref: PIdnRef[PCallable] = call.inner.idnref + lazy val args: Seq[PExp] = call.inner.args + + override def typeSubstitutions: Seq[PTypeSubstitution] = Seq(PTypeSubstitution.id) + + override def forceSubstitution(ts: PTypeSubstitution): Unit = {} + + override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = typecheck(t, n) + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + // this node should get translated to `POldCall` but `beforeResolve` in `ReasoningPlugin` performs this translation + // only if its parent node is a PAssign. Thus, an invocation of this function indicates that this expression occurs + // at an unsupported location within the AST. + // TODO check that label is valid + Some(Seq(s"oldCalls are only supported as statements or as the right-hand side of an assignment")) + } + + // we do not translate this expression but `POldCall` which is created before resolution + override def translateExp(t: Translator): ExtensionExp = throw new AssertionError(s"POldCallExp '$this' should have been transformed before typechecking") +} diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala new file mode 100644 index 000000000..ef5114531 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala @@ -0,0 +1,296 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2024 ETH Zurich. + +package viper.silver.plugin.standard.reasoning + +import fastparse._ +import viper.silver.ast._ +import viper.silver.ast.utility.rewriter.{StrategyBuilder, Traverse} +import viper.silver.ast.utility.ViperStrategy +import viper.silver.parser.FastParserCompanion.{Pos, whitespace} +import viper.silver.parser._ +import viper.silver.plugin.standard.reasoning.analysis.AnalysisUtils.{LocalVarSink, NonAssumeInfluenceSink} +import viper.silver.plugin.standard.reasoning.analysis.VarAnalysisGraphMap +import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} +import viper.silver.verifier._ +import viper.silver.verifier.errors.AssertFailed + +import scala.annotation.unused +import scala.collection.mutable + +class ReasoningPlugin(@unused reporter: viper.silver.reporter.Reporter, + logger: ch.qos.logback.classic.Logger, + @unused config: viper.silver.frontend.SilFrontendConfig, + fp: FastParser) extends SilverPlugin with ParserPluginTemplate with BeforeVerifyHelper { + + import fp.{exp, ParserExtension, lineCol, _file} + import FastParserCompanion.{ExtendedParsing, PositionParsing, reservedKw, reservedSym} + + /** Parser for existential elimination statements. */ + def existentialElim[$: P]: P[PExistentialElim] = + P((P(PObtainKeyword) ~/ fp.nonEmptyIdnTypeList(PLocalVarDecl(_)) ~/ P(PWhereKeyword) ~/ fp.trigger.rep ~ exp).map { + case (obtainKw, varDecls, whereKw, triggers, e) => PExistentialElim(obtainKw, varDecls, whereKw, triggers, e)(_) + }).pos + + /** Parser for universal introduction statements. */ + def universalIntro[$: P]: P[PUniversalIntro] = + P((P(PProveKeyword) ~/ PKw.Forall ~/ fp.nonEmptyIdnTypeList(PLocalVarDecl(_)) ~/ fp.trigger.rep ~/ P(PAssumingKeyword) ~/ exp ~/ P(PImpliesKeyword) ~/ exp ~/ fp.stmtBlock()).map { + case (proveKw, forallKw, varDecls, triggers, assumingKw, p, impliesKw, q, b) => PUniversalIntro(proveKw, forallKw, varDecls, triggers, assumingKw, p, impliesKw, q, b)(_) + }).pos + + /** Parser for new influence by condition */ + def flowSpec[$: P]: P[PSpecification[PInfluencedKeyword.type]] = + P((P(PInfluencedKeyword) ~ influencedBy) map (PSpecification.apply _).tupled).pos + + def heap[$: P]: P[PHeap] = P(P(PHeapKeyword) map (PHeap(_) _)).pos // note that the parentheses are not redundant + + def assumes[$: P]: P[PAssumes] = P(P(PAssumesKeyword) map (PAssumes(_) _)).pos // note that the parentheses are not redundant + + def assumesNothingSpec[$: P]: P[PSpecification[PNothingKeyword.type]] = + P((P(PNothingKeyword) ~ assumesNothingClause) map { case (kw, clauseFn) => pos: Pos => PSpecification(kw, clauseFn(pos))(pos) }).pos + + // assumes nothing clause is completely artificial and is created out of nowhere. Instead of taking the parser's current position, + // we parameterize this parser by `Pos` such that the caller can pass in the position of, e.g., the corresponding keyword. + def assumesNothingClause[$: P]: P[Pos => PAssumesNothing] = Pass(()) map { _ => PAssumesNothing()(_) } + def singleVar[$: P]: P[PVar] = P(fp.idnuse map (PVar(_) _)).pos // note that the parentheses are not redundant + def varsAndHeap[$: P]: P[Seq[PFlowVarOrHeap]] = (heap | singleVar).delimited(PSym.Comma).map(_.toSeq) + + def influencedBy[$: P]: P[PInfluencedBy] = P(((heap | assumes | singleVar) ~ P(PByKeyword) ~/ varsAndHeap.braces) map { + case (v, byKw, groupedVarList) => PInfluencedBy(v, byKw, groupedVarList)(_) + }).pos + + /** parser for lemma annotation */ + def lemma[$: P]: P[PSpecification[PIsLemmaKeyword.type]] = + P((P(PIsLemmaKeyword) ~ lemmaClause) map { case (kw, clauseFn) => pos: Pos => PSpecification(kw, clauseFn(pos))(pos) }).pos + + // lemma clause is completely artificial and is created out of nowhere. Instead of taking the parser's current position, + // we parameterize this parser by `Pos` such that the caller can pass in the position of, e.g., the corresponding keyword. + def lemmaClause[$: P]: P[Pos => PLemmaClause] = Pass(()) map { _ => PLemmaClause()(_) } + + /** parsers for oldCall statement */ + /* + Note that the following definition of old call, i.e., `a, b := oldCall[L](lemma())` causes issues with backtracking + because depending on whether `oldCall` is added at the beginning and end of the list of statement parsers, the parser + has to backtrack to parse assignments and old calls, resp. + def oldCall[$: P]: P[POldCall] = + P(((fp.idnuse.delimited(PSym.Comma) ~ P(PSymOp.Assign)).? ~ P(POldCallKeyword) ~ fp.oldLabel.brackets ~ fp.funcApp.parens) map { + case (lhs, oldCallKw, lbl, call) => POldCall(lhs, oldCallKw, lbl, call)(_) + }).pos + */ + def oldCallStmt[$: P]: P[POldCallStmt] = + P((P(POldCallKeyword) ~/ fp.oldLabel.brackets ~/ fp.funcApp.parens) map { + case (oldCallKw, lbl, funcApp) => POldCallStmt(oldCallKw, lbl, funcApp)(_) + }).pos + + def oldCallExp[$: P]: P[POldCallExp] = + P((P(POldCallKeyword) ~ fp.oldLabel.brackets ~ fp.funcApp.parens) map { + case (oldCallKw, lbl, call) => POldCallExp(oldCallKw, lbl, call)(_) + }).pos + + /** Add existential elimination and universal introduction to the parser. */ + override def beforeParse(input: String, isImported: Boolean): String = { + /** keywords for existential elimination and universal introduction */ + ParserExtension.addNewKeywords(Set(PObtainKeyword, PWhereKeyword, PProveKeyword, PAssumingKeyword, PImpliesKeyword)) + + /** keywords for flow annotation and therefore modular flow analysis */ + ParserExtension.addNewKeywords(Set(PInfluencedKeyword, PByKeyword, PHeapKeyword, PNothingKeyword, PAssumesKeyword)) + + /** keyword to declare a lemma and to call the lemma in an old context*/ + ParserExtension.addNewKeywords(Set(PIsLemmaKeyword)) + ParserExtension.addNewKeywords(Set(POldCallKeyword)) + + /** adding existential elimination and universal introduction to the parser */ + ParserExtension.addNewStmtAtEnd(existentialElim(_)) + ParserExtension.addNewStmtAtEnd(universalIntro(_)) + + /** add influenced by flow annotation to as a postcondition */ + ParserExtension.addNewPostCondition(flowSpec(_)) + ParserExtension.addNewPostCondition(assumesNothingSpec(_)) + + /** add lemma as an annotation either as a pre- or a postcondition */ + ParserExtension.addNewPreCondition(lemma(_)) + ParserExtension.addNewPostCondition(lemma(_)) + + /** add the oldCall as a new stmt */ + ParserExtension.addNewStmtAtEnd(oldCallStmt(_)) + ParserExtension.addNewExpAtEnd(oldCallExp(_)) + + input + } + + + override def beforeResolve(input: PProgram): PProgram = { + // we change `oldCallExp` and `oldCallStmt` (which made parsing easier) to `oldCall`, which makes the translation easier + def transformStrategy[T <: PNode](input: T): T = StrategyBuilder.Slim[PNode]({ + case a@PAssign(delimitedTargets, op, c: POldCallExp) => POldCall(delimitedTargets, op, c.oldCallKw, c.lbl, c.call)(a.pos) + case o@POldCallStmt(oldCallKw, lbl, call) => POldCall(PDelimited(None, Nil, None)(oldCallKw.pos), None, oldCallKw, lbl, call)(o.pos) + }).recurseFunc({ + // only visit statements + case _: PExp => Seq() + case n: PNode => n.children collect { case ar: AnyRef => ar } + }).execute(input) + + transformStrategy(input) + } + + + private def removeReasoningAnnotations(m: Method): Method = { + val flowAnnotationAndLemmaFilter: Exp => Boolean = { + case _: InfluencedBy | _: Lemma | _: AssumesNothing => false + case _ => true + } + val postconds = m.posts.filter(flowAnnotationAndLemmaFilter) + val preconds = m.pres.filter(flowAnnotationAndLemmaFilter) + m.copy(pres = preconds, posts = postconds)(m.pos, m.info, m.errT) + } + + private def translateOldCall(o: OldCall, method: Method, usedNames: mutable.Set[String]): Stmt = { + val new_v_map: Seq[(LocalVarDecl, Exp)] = ((method.formalArgs ++ method.formalReturns) zip (o.args ++ o.rets)).map(zipped => { + val formal_a: LocalVarDecl = zipped._1 + val arg_exp: Exp = zipped._2 + formal_a -> arg_exp + }) + + /** replace all input parameters in preconditions with the corresponding argument */ + val new_pres = method.pres.flatMap { + case Lemma() => Seq.empty + case p => Seq(applySubstitutionWithExp(new_v_map, p)) + } + + /** replace all input & output parameters in postconditions with the corresponding argument / result */ + val new_posts = method.posts.flatMap { + case Lemma() => Seq.empty + case p => Seq(applySubstitutionWithExp(new_v_map, p)) + } + + /** create new variable declarations to havoc the lhs of the oldCall */ + val rToV = o.rets.map(r => { + val new_v = LocalVarDecl(uniqueName(".v", usedNames), r.typ)(r.pos) + r -> new_v + }).toMap + + val errTransformer = ErrTrafo({ + case AssertFailed(_, r, c) => PreconditionInLemmaCallFalse(o, r, c) + case d => d + }) + + Seqn( + // assert precondition(s) + new_pres.map(p => + Assert(LabelledOld(p, o.oldLabel)(p.pos))(o.pos, errT = errTransformer) + ) ++ + // havoc return args by assigning an unconstrained value + o.rets.map(r => { + LocalVarAssign(r, rToV(r).localVar)(o.pos) + }) ++ + // inhale postcondition(s) + new_posts.map(p => + Inhale(LabelledOld(p, o.oldLabel)(p.pos))(o.pos) + ), + rToV.values.toSeq + )(o.pos) + } + + private def translateExistentialElim(e: ExistentialElim, usedNames: mutable.Set[String]): Stmt = { + val (new_v_map, new_exp) = substituteWithFreshVars(e.varList, e.exp, usedNames) + val new_trigs = e.trigs.map(t => Trigger(t.exps.map(e1 => applySubstitution(new_v_map, e1)))(t.pos)) + val errTransformer = ErrTrafo({ + case AssertFailed(_, r, c) => ExistentialElimFailed(e, r, c) + case d => d + }) + Seqn( + Seq( + Assert(Exists(new_v_map.map(_._2), new_trigs, new_exp)(e.pos, errT = errTransformer))(e.pos) + ) + ++ + e.varList.map(variable => LocalVarDeclStmt(variable)(variable.pos)) //list of variables + ++ + Seq( + Inhale(e.exp)(e.pos) + ), + Seq() + )(e.pos) + } + + private def translateUniversalIntroduction(u: UniversalIntro, usedNames: mutable.Set[String]): Stmt = { + /** Translate the new syntax into Viper language */ + val (newVarMap, newExp1) = substituteWithFreshVars(u.varList, u.assumingExp, usedNames) + val newExp2 = applySubstitution(newVarMap, u.implyingExp) + val quantifiedVars = newVarMap.map(vars => vars._2) + val newTrigs = u.triggers.map(t => Trigger(t.exps.map(e1 => applySubstitution(newVarMap, e1)))(t.pos)) + val lbl = uniqueName("l", usedNames) + val errTransformer = ErrTrafo({ + case AssertFailed(_, r, c) => UniversalIntroFailed(u, r, c) + case d => d + }) + + val boolvar = LocalVarDecl(uniqueName("b", usedNames), Bool)(u.assumingExp.pos) + Seqn( + Seq( + Label(lbl, Seq.empty)(u.pos), + // conditionally inhale assume expression + If(boolvar.localVar, + Seqn( + Seq(Inhale(u.assumingExp)(u.assumingExp.pos)), + Seq.empty)(u.assumingExp.pos), + Seqn(Seq.empty, Seq.empty)(u.assumingExp.pos) + )(u.pos), + // execute block + u.block, + // conditionally assert imply expression + Assert(Implies(boolvar.localVar, u.implyingExp)(u.implyingExp.pos))(u.implyingExp.pos, errT = errTransformer), + Inhale(Forall(quantifiedVars, newTrigs, Implies(LabelledOld(newExp1, lbl)(u.implyingExp.pos), newExp2)(u.implyingExp.pos))(u.implyingExp.pos))(u.implyingExp.pos) + ), + Seq(boolvar) ++ u.varList + )(u.pos) + } + + override def beforeVerify(input: Program): Program = { + val usedNames: mutable.Set[String] = collection.mutable.Set(input.transitiveScopedDecls.map(_.name): _*) + + /** check that lemma terminates (has a decreases clause) and that it is pure */ + checkLemmas(input, reportError) + /** create graph with vars that are in scope only outside of the universal introduction code block including the quantified variables */ + val analysis: VarAnalysisGraphMap = VarAnalysisGraphMap(input, logger, reportError) + + /** Run taint analysis for all methods annotated with influences */ + analysis.checkUserProvidedInfluencesSpec() + + ViperStrategy.Slim({ + /** remove the influenced by postconditions. + * remove isLemma */ + case m: Method => removeReasoningAnnotations(m) + case o: OldCall => + /** check whether called method is a lemma */ + val currmethod = input.findMethod(o.methodName) + if (!specifiesLemma(currmethod)) { + reportError(ConsistencyError(s"method ${currmethod.name} called in old context must be lemma", o.pos)) + } + translateOldCall(o, currmethod, usedNames) + case e: ExistentialElim => translateExistentialElim(e, usedNames) + case u@UniversalIntro(v, _, exp1, exp2, blk) => + /** + * get all variables that are assigned to inside the block and take intersection with universal introduction + * variables. If they are contained throw error since quantified variables should be immutable + */ + val writtenVars: Set[LocalVarDecl] = analysis.getModifiedVars(blk).collect({ case v: LocalVarDecl => v}) + checkReassigned(writtenVars, v, reportError, u) + checkInfluencedBy(input, reportError) + + /** Get all variables that are in scope in the current method */ + val tainted: Set[LocalVarDecl] = v.toSet + val varsOutside = (input.methods + .filter(m => m.body.isDefined) + .flatMap(m => m.body.get.ss.filter(s => s.contains(u)).flatMap(_ => Set(m.transitiveScopedDecls: _*))).toSet -- Set(u.transitiveScopedDecls: _*)) ++ tainted + + /** Contains all variables that must not be tainted */ + val volatileVars: Set[NonAssumeInfluenceSink] = analysis.getSinksFromExpr(exp1) ++ analysis.getSinksFromExpr(exp2) -- v.map(decl => LocalVarSink(decl.localVar)).toSet + /** execute modular flow analysis using graph maps for the universal introduction statement */ + analysis.executeTaintedGraphAnalysis(varsOutside.collect({ case v:LocalVarDecl => v }), tainted, blk, volatileVars, u) + translateUniversalIntroduction(u, usedNames); + }, Traverse.TopDown).execute[Program](input) + } +} diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisGraphMap.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisGraphMap.scala new file mode 100644 index 000000000..8f4766583 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisGraphMap.scala @@ -0,0 +1,514 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2024 ETH Zurich. + +package viper.silver.plugin.standard.reasoning.analysis + +import viper.silver.ast.utility.Expressions +import viper.silver.ast.{AccessPredicate, Apply, Assert, Assume, BinExp, CurrentPerm, Declaration, DomainFuncApp, Exhale, Exp, FieldAccess, FieldAssign, Fold, ForPerm, FuncApp, Goto, If, Info, Inhale, Label, LocalVar, LocalVarAssign, LocalVarDecl, Method, MethodCall, NoPosition, Package, Position, Program, Quasihavoc, Quasihavocall, Scope, Seqn, Stmt, UnExp, Unfold, While} +import viper.silver.plugin.standard.reasoning.analysis.AnalysisUtils.{AssumeInfluenceSink, AssumeMethodInfluenceSink, AssumeStmtInfluenceSink, AssumeWhileInfluenceSink, HeapSink, HeapSource, InfluenceSink, InfluenceSource, LocalVarSink, LocalVarSource, NonAssumeInfluenceSink, getLocalVarDeclFromLocalVar, getSinkFromVarDecl, getSourceFromVarDecl} +import viper.silver.plugin.standard.reasoning.{Assumes, AssumesNothing, ExistentialElim, FlowAnnotation, FlowVar, FlowVarOrHeap, Heap, InfluencedBy, OldCall, UniversalIntro, Var} +import viper.silver.plugin.standard.termination.{DecreasesClause, DecreasesSpecification, DecreasesTuple, DecreasesWildcard} +import viper.silver.verifier.{AbstractError, ConsistencyError} + +import scala.collection.mutable + +object AnalysisUtils { + trait InfluenceSource extends Declaration + + case object HeapSource extends InfluenceSource { + override def name: String = ".heap" + override def pos: Position = NoPosition + } + + /** This is either a local variable or a method's input parameter */ + case class LocalVarSource(v: LocalVar) extends InfluenceSource { + override def name: String = v.name + + override def pos: Position = v.pos + } + + def getSourceFromFlowVar(f: FlowVarOrHeap): InfluenceSource = f match { + case v: Var => LocalVarSource(v.decl) + case _: Heap => HeapSource + } + + def getSourceFromVarDecl(v: LocalVarDecl): InfluenceSource = LocalVarSource(v.localVar) + + /** presence of an InfluenceSink indicates that assume stmts are potentially (transitively) present.This sink might + * map to an emtpy set of sources in case these assume stmts are not influenced by any variables. Note that we use + * the absence of these sinks in the GraphMap to indicate that no assume stmts are (transitively) present. + */ + trait InfluenceSink extends Declaration + + trait AssumeInfluenceSink extends InfluenceSink { + override def name: String = ".assume" + def pretty: String + } + + /** Declaration that method might contain assume stmts, which is used for the analysis of the callers of this method */ + case class AssumeMethodInfluenceSink(m: Method) extends AssumeInfluenceSink { + lazy val pretty = s"Method called at $pos" + override def pos: Position = m.pos + } + /** Declaration that the while loop behaves like an assume stmt, which is used for the analysis of the surrounding method */ + case class AssumeWhileInfluenceSink(w: While) extends AssumeInfluenceSink { + lazy val pretty = s"Loop at $pos" + override def pos: Position = w.pos + } + /** Declaration that there's an assume or inhale stmt at `pos`, which is used for the analysis of the surrounding method */ + case class AssumeStmtInfluenceSink(i: Inhale) extends AssumeInfluenceSink { + lazy val pretty = s"Assume or inhale at $pos" + override def pos: Position = i.pos + } + + trait NonAssumeInfluenceSink extends InfluenceSink + + case object HeapSink extends NonAssumeInfluenceSink { + override def name: String = ".heap" + override def pos: Position = NoPosition + } + + /** This is either a local variable or a method's output parameter */ + case class LocalVarSink(v: LocalVar) extends NonAssumeInfluenceSink { + override def name: String = v.name + override def pos: Position = v.pos + } + + def getSinkFromFlowVar(f: FlowVar, m: Method): InfluenceSink = f match { + case f: FlowVarOrHeap => f match { + case v: Var => LocalVarSink(v.decl) + case _: Heap => HeapSink + } + case _: Assumes => AssumeMethodInfluenceSink(m) + } + + def getSinkFromVarDecl(v: LocalVarDecl): InfluenceSink = LocalVarSink(v.localVar) + + def isAssumeSink(sink: InfluenceSink): Boolean = sink match { + case _: AssumeInfluenceSink => true + case _: NonAssumeInfluenceSink => false + } + + def getLocalVarDeclFromLocalVar(l: LocalVar): LocalVarDecl = { + LocalVarDecl(l.name, l.typ)() + } + + case class TerminationSpecState(guaranteesTermination: Boolean, noTerminationSpec: Boolean) + + private def specifiesTermination(spec: Seq[Exp], info: Info): TerminationSpecState = { + // we do not analyze whether the conditions cover all cases but are conservative. + val noTerminationSpec = spec.forall { + case _: DecreasesClause => false + case _ => true + } + + val allInfos = info.getAllInfos[Info] + val noTerminationInfo = allInfos.forall { + case _: DecreasesSpecification => false + case _ => true + } + + def specifiesCompleteTermination(e: Exp): Boolean = e match { + case DecreasesTuple(_, None) => true + case DecreasesWildcard(None) => true + case _ => false + } + + val isTerminationSpecComplete = spec.exists(specifiesCompleteTermination) + + val isTerminationInfoComplete = allInfos.exists { + case DecreasesSpecification(optTuple, optWildcard, _) => + optTuple.exists(specifiesCompleteTermination) || optWildcard.exists(specifiesCompleteTermination) + case _ => false + } + + TerminationSpecState( + guaranteesTermination = isTerminationSpecComplete || isTerminationInfoComplete, + noTerminationSpec = noTerminationSpec && noTerminationInfo + ) + } + + def specifiesTermination(m: Method): TerminationSpecState = specifiesTermination(m.pres ++ m.posts, m.info) + def specifiesTermination(w: While): TerminationSpecState = specifiesTermination(w.invs, w.info) +} + +case class VarAnalysisGraphMap(prog: Program, + logger: ch.qos.logback.classic.Logger, + reportErrorWithMsg: AbstractError => Unit) { + + // Maps all influences for a given variable + private type GraphMap = Map[InfluenceSink, Set[InfluenceSource]] + + // Storage for method analysis + private val methodAnalysisMap: mutable.Map[Method, GraphMap] = mutable.Map() + private val methodAnalysisStarted: mutable.ListBuffer[Method] = mutable.ListBuffer() + + + def checkUserProvidedInfluencesSpec(): Unit = { + val methodsWithFlowAnnotations = prog.methods.filter(_.posts.exists { + case _: FlowAnnotation => true + case _ => false + }) + methodsWithFlowAnnotations.foreach(executeTaintedGraphMethodAnalysis) + } + + /** execute the information flow analysis with graphs. + * When executed on the universal introduction statement the tainted variables are simply the quantified variables */ + def executeTaintedGraphAnalysis(allVars: Set[LocalVarDecl], tainted: Set[LocalVarDecl], blk: Seqn, volatileSinks: Set[NonAssumeInfluenceSink], u: UniversalIntro): Unit = { + // Build initial graph where every variable and the heap influences itself + val initialGraph: GraphMap = allVars.map(k => getSinkFromVarDecl(k) -> Set[InfluenceSource](LocalVarSource(k.localVar))).toMap + (AnalysisUtils.HeapSink -> Set[InfluenceSource](AnalysisUtils.HeapSource)) + val graph = computeInfluenceMap(blk, initialGraph) + val taintedSources: Set[InfluenceSource] = tainted.map(decl => LocalVarSource(decl.localVar)) + val taintedNonAssumeSinks = volatileSinks.filter(v => graph(v).intersect(taintedSources).nonEmpty) + taintedNonAssumeSinks.foreach { + case AnalysisUtils.HeapSink => reportErrorWithMsg(ConsistencyError("Universally introduced variables might influence the heap", u.pos)) + case LocalVarSink(v) => reportErrorWithMsg(ConsistencyError(s"Universally introduced variables might influence variable $v", u.pos)) + } + + val assumeSinks = graph.keySet.collect { case s: AssumeInfluenceSink => s } + val taintedAssumes = assumeSinks.filter(assumeSink => graph(assumeSink).intersect(taintedSources).nonEmpty) + taintedAssumes.foreach { + case AssumeMethodInfluenceSink(p) => reportErrorWithMsg(ConsistencyError(s"Universal introduction variable might influence the method's termination or assume statements in the method's body", p.pos)) + case AssumeStmtInfluenceSink(p) => reportErrorWithMsg(ConsistencyError(s"Universal introduction variable might influence assume statement", p.pos)) + case AssumeWhileInfluenceSink(p) => reportErrorWithMsg(ConsistencyError(s"Universal introduction variable might influence loop termination", p.pos)) + } + } + + /** + * Executes the taint analysis for a method and stores the resulting graph map in methodAnalysisMap and the resulting + * assume analysis in the methodAssumeAnalysisMap. + * + * If a recursive method is encountered, we fall back to the specified influences or a over approximation for the graph map + * and an over approximation for the assume analysis + */ + def executeTaintedGraphMethodAnalysis(method: Method): Unit = { + if (methodAnalysisStarted.contains(method)) { + // Case for recursive methods + if (!methodReturnInfluencesFullySpecified(method)) { + logger.info(s"Taint analysis encountered an incomplete flow annotation and conservatively over-approximates information flows. (${method.name} ${method.pos})") + } + methodAnalysisMap.put(method, getGraphForRecursiveOrAbstractMethod(method)) + } else { + method.body match { + case None => + // Case for abstract methods + val map = getGraphForRecursiveOrAbstractMethod(method) + methodAnalysisMap.put(method, map) + case Some(seqn) => + // Default case + methodAnalysisStarted.addOne(method) + val initialGraph: GraphMap = + method.formalArgs.map(k => getSinkFromVarDecl(k) -> Set(getSourceFromVarDecl(k))).toMap ++ + method.formalReturns.map(k => getSinkFromVarDecl(k) -> Set.empty[InfluenceSource]).toMap + + (HeapSink -> Set(HeapSource)) + + val stmt = seqn.copy(scopedSeqnDeclarations = seqn.scopedSeqnDeclarations.filter({ + case l: LocalVarDecl => !initialGraph.contains(LocalVarSink(l.localVar)) + case _ => true + }))(seqn.pos, seqn.info, seqn.errT) + + var map = computeInfluenceMap(stmt, initialGraph) + val assumeVars = map.keySet.collect { + case v: AssumeInfluenceSink => v + } + + // Remove all assume nodes and save them as a single assume node for the whole method + if (assumeVars.nonEmpty) { + map = map.removedAll(assumeVars) + (AssumeMethodInfluenceSink(method) -> assumeVars.flatMap(v => map(v))) + + // we enter this branch if there are any assume statements in this method's or any callees' body + // check that user-provided spec did not specify that there are none + val assumesNothings = method.posts.collect { case n: AssumesNothing => n } + assumesNothings.foreach { + n => reportErrorWithMsg(ConsistencyError(s"Contradicting flow annotation: Method might assume or inhale, which is caused by ${assumeVars.map(_.pretty).mkString(", ")}", n.pos)) + } + } + + // Remove sources corresponding to local variables (as opposed to parameters) such that only sources concerned with method arguments and the heap remain: + val formalVars = method.formalArgs.map(_.localVar) + map = map.map { + case (sink, sources) => sink -> sources.filter { + case LocalVarSource(v) => formalVars.contains(v) + case _ => true + } + } + + // Check calculated value against the provided influencedBy annotations if there are any + val influencedBys = method.posts.collect { case f: InfluencedBy => f } + influencedBys.foreach(f => { + val returnVar = AnalysisUtils.getSinkFromFlowVar(f.v, method) + val specifiedInfluences = f.varList.map(v => AnalysisUtils.getSourceFromFlowVar(v)).toSet + val calculatedInfluences = lookupVar(returnVar, map) + + if (!calculatedInfluences.subsetOf(specifiedInfluences)) { + reportErrorWithMsg(ConsistencyError(s"Specified influence on return variable $returnVar is missing some potential influences. Specified: $specifiedInfluences Calculated: $calculatedInfluences", f.pos)) + } + + if (calculatedInfluences.intersect(specifiedInfluences).size < calculatedInfluences.size) { + logger.warn(s"Specified influence on return variable $returnVar potentially assumes too many influences. Specified: $specifiedInfluences Calculated: $calculatedInfluences, (${f.pos})") + } + + map = map + (returnVar -> specifiedInfluences) + }) + methodAnalysisMap.put(method, map) + } + } + + methodAnalysisStarted -= method + } + + private def methodReturnInfluencesFullySpecified(method: Method): Boolean = { + val allVars = method.posts.collect({ case f: InfluencedBy => f.v }) + val vars = allVars.collect({ case Var(localVar) => getLocalVarDeclFromLocalVar(localVar)}) + method.formalReturns.forall(v => vars.contains(v)) && allVars.exists(v => v.isInstanceOf[Heap]) && allVars.exists(v => v.isInstanceOf[Assumes]) + } + + /** + * Returns the graph map for invocations of a recursive or abstract method. + * In the case of a recursive method, the returned graph map is used as a summary of the recursive call and the caller's + * analysis continues. The returned graph contains all user-provided influenced-by annotations, which means that the + * caller's analysis checks that these annotations form a (over-approximating) fixed point. All return variables (and + * the heap) for which the user did _not_ provide influenced-by annotations, we over-approximate and treat them as + * being influenced by all input parameters and the heap. + * While the graph for an abstract method is computed in the very same way, the user-provided annotations is effectively + * trusted because we cannot use the method's body to check that these annotations represent a valid fixed point. + * AssumeNothing and "influence assume by" annotations are treated in a similar way, i.e., are included in the returned + * graph map if specified. If both of these annotations are missing, we over-approximate for possibly non-terminating + * methods, i.e., the returned graph map specifies that assumes are (potentially) influenced by all input parameters + * and the heap. If a method is guaranteed to terminate (according to its termination measures), we treat the method + * as if `AssumeNothing` has been specified. + */ + private def getGraphForRecursiveOrAbstractMethod(method: Method): GraphMap = { + // We ignore the assume vertex on purpose here, as a missing assume vertex is treated as if no assume statement appears in the method + val retSet: Set[InfluenceSink] = method.formalReturns.map(decl => LocalVarSink(decl.localVar)).toSet + HeapSink + val allMethodArgsSet: Set[InfluenceSource] = method.formalArgs.map(decl => LocalVarSource(decl.localVar)).toSet + HeapSource + + val annotatedInfluencedBys = method.posts.collect({ case a: InfluencedBy => a }).map(a => { + AnalysisUtils.getSinkFromFlowVar(a.v, method) -> a.varList.map(f => AnalysisUtils.getSourceFromFlowVar(f)).toSet + }).toMap + /** influence all return variables, not mentioned by annotation, by every method argument */ + val unannotatedInfluencedBys = (retSet -- annotatedInfluencedBys.keySet).map(retVar => { + retVar -> allMethodArgsSet + }).toMap + val terminates = AnalysisUtils.specifiesTermination(method).guaranteesTermination + val noAssumes = method.posts.exists { + case _: AssumesNothing => true + case _ => false + } + + // add information about assume statements. We distinguish two cases: (1) Either the user specified which variables + // influence an assume, that no assume statement occurs or the method terminates and (2) otherwise. + // In the first case, we do not have to add any influenced by annotations and in the second case, we over-approximate and + // add an annotation stating that all input parameters and the heap possibly influence a possibly existing assume statements. + if(annotatedInfluencedBys.contains(AssumeMethodInfluenceSink(method)) || terminates || noAssumes) { + annotatedInfluencedBys ++ unannotatedInfluencedBys + } else { + val assumeInfluence: GraphMap = Map(AssumeMethodInfluenceSink(method) -> allMethodArgsSet) + annotatedInfluencedBys ++ unannotatedInfluencedBys ++ assumeInfluence + } + } + + private def computeInfluenceMap(stmt: Stmt, graphMap: GraphMap): GraphMap = { + /** extends heap influences by all sources of `exp` and returns the updated graph */ + def addExpSourcesToHeap(graphMap: GraphMap, exp: Exp): GraphMap = { + val vars = getResolvedVarsFromExp(exp, graphMap) + graphMap + (HeapSink -> (lookupVar(HeapSink, graphMap) ++ vars)) + } + + stmt match { + case s: Scope => + // Temporarily add the scoped declarations to the graph and remove them afterwards + val declarations = s.scopedDecls.collect({ case l: LocalVarDecl => l }) + val scopedGraph = graphMap ++ declarations.map(decl => LocalVarSink(decl.localVar) -> Set[InfluenceSource](LocalVarSource(decl.localVar))).toMap + val graph: GraphMap = s match { + case Seqn(ss, _) => + ss.foldLeft(scopedGraph) { (graph, subStmt) => computeInfluenceMap(subStmt, graph) } + case u: UniversalIntro => computeInfluenceMap(u.block, scopedGraph) + case o: OldCall => + val met = prog.findMethod(o.methodName) + computeMethodInfluenceMap(graphMap, met, o.args, o.rets) + // The quantified variables of the Quasihavocall statement are ignored because they are untainted by definition + case Quasihavocall(_, lhs, _) => + val vars = lhs.map(e => getResolvedVarsFromExp(e, graphMap)).getOrElse(Set.empty) + graphMap + (HeapSink -> (lookupVar(HeapSink, graphMap) ++ vars)) + } + graph.removedAll(declarations.map(decl => LocalVarSink(decl.localVar))) + case LocalVarAssign(lhs, rhs) => + val influences = getResolvedVarsFromExp(rhs, graphMap) + graphMap + (LocalVarSink(lhs) -> influences) + case If(cond, thn, els) => + val conditionVars = getResolvedVarsFromExp(cond, graphMap) + // For the condition influences, we only care for variables that are declared outside of the if block and for assume annotations + val writesInIfBlocks = (getModifiedVars(thn) ++ getModifiedVars(els)).filter(v => AnalysisUtils.isAssumeSink(v) || graphMap.contains(v)) + val conditionInfluences = writesInIfBlocks.map(v => v -> (lookupVar(v, graphMap) ++ conditionVars)).toMap + + val thenGraph = computeInfluenceMap(thn, graphMap) + val elseGraph = computeInfluenceMap(els, graphMap) + (thenGraph.keySet ++ elseGraph.keySet).map( + v => v -> (thenGraph.getOrElse(v, Set.empty) ++ elseGraph.getOrElse(v, Set.empty) ++ conditionInfluences.getOrElse(v, Set.empty)) + ).toMap + case s@ While(cond, _, body) => + val unrolledLoop = If(cond, body, Seqn(Seq.empty, Seq.empty)())(body.pos, body.info, body.errT) + var edgesEqual: Boolean = false + var mergedGraph = computeInfluenceMap(unrolledLoop, graphMap) + while (!edgesEqual) { + val iterationGraph = computeInfluenceMap(unrolledLoop, mergedGraph) + if(iterationGraph.equals(mergedGraph)) { + edgesEqual = true + } else { + mergedGraph = iterationGraph + } + } + + val loopTerminates = AnalysisUtils.specifiesTermination(s).guaranteesTermination + if(loopTerminates) { + mergedGraph + } else { + mergedGraph + (AssumeWhileInfluenceSink(s) -> getResolvedVarsFromExp(cond, mergedGraph)) + } + case m: MethodCall => + val met = prog.findMethod(m.methodName) + computeMethodInfluenceMap(graphMap, met, m.args, m.targets) + case FieldAssign(_, rhs) => + // after the assignment, the heap is influenced by everything that influences `rhs` (i.e. `vars`) and all things + // that influenced the heap before the assignment + addExpSourcesToHeap(graphMap, rhs) + case Exhale(exp) => + if (exp.isPure) { + graphMap + } else { + addExpSourcesToHeap(graphMap, exp) + } + case Fold(acc) => + addExpSourcesToHeap(graphMap, acc) + case Unfold(acc) => + addExpSourcesToHeap(graphMap, acc) + case Apply(exp) => + addExpSourcesToHeap(graphMap, exp) + case Package(wand, _) => + addExpSourcesToHeap(graphMap, wand) + case Quasihavoc(lhs, _) => + lhs.map(exp => addExpSourcesToHeap(graphMap, exp)).getOrElse(graphMap) + case Assert(_) => graphMap + case Label(_, _) => graphMap + // Assume analysis + case a: Inhale => + val assumeVars = lookupVar(AssumeStmtInfluenceSink(a), graphMap) ++ getResolvedVarsFromExp(a.exp, graphMap) + graphMap + (AssumeStmtInfluenceSink(a) -> assumeVars) + case ExistentialElim(vars, _, exp) => graphMap ++ vars.map(v => LocalVarSink(v.localVar) -> getResolvedVarsFromExp(exp, graphMap)) + // Non handled cases + case a: Assume => + reportErrorWithMsg(ConsistencyError("Unexpected assume statement in the modular information flow analysis", a.pos)) + graphMap + case g: Goto => + reportErrorWithMsg(ConsistencyError(s"$g is an undefined statement for the modular information flow analysis", g.pos)) + graphMap + case _ => + reportErrorWithMsg(ConsistencyError(s"$stmt is an undefined statement for the modular information flow analysis", stmt.pos)) + graphMap + } + } + + /** creates graph for method call and old call. maps expressions passed to methods to the method arguments, computes the graph based on the flow annotation, + * and finally maps the return variables to the variables that the method is assigned to. */ + private def computeMethodInfluenceMap(graphMap: GraphMap, method: Method, callArgs: Seq[Exp], callTargets: Seq[LocalVar]): GraphMap = { + /** maps formal arguments to the influence sources of the corresponding call arguments */ + val methodArgExpMapping: Map[InfluenceSource, Set[InfluenceSource]] = (method.formalArgs zip callArgs).map { + case (formalArg, callArg) => + getSourceFromVarDecl(formalArg) -> getResolvedVarsFromExp(callArg, graphMap) + }.toMap + (HeapSource -> lookupVar(HeapSink, graphMap)) + + /** maps formal returns, heap, and assume sink to call targets, heap, and assume */ + val retVarMapping: Map[InfluenceSink, InfluenceSink] = + (method.formalReturns zip callTargets).map { + case (formalRet, callTarget) => getSinkFromVarDecl(formalRet) -> LocalVarSink(callTarget) + }.toMap + + (HeapSink -> HeapSink) + + // we set the position to the method call instead of the assume statement, so potential error are more readable: + (AssumeMethodInfluenceSink(method) -> AssumeMethodInfluenceSink(method)) + + val resolvedMethodMap = getMethodAnalysisMap(method) + .filter(v => retVarMapping.contains(v._1)) + .map { + // extend the method analysis graph by transitivity via the method's arguments: + case (sink, sources) => retVarMapping(sink) -> sources.flatMap(methodArgExpMapping) + } + + graphMap ++ resolvedMethodMap + } + + private def getMethodAnalysisMap(method: Method): GraphMap = { + if (!methodAnalysisMap.contains(method)) { + executeTaintedGraphMethodAnalysis(method) + } + methodAnalysisMap(method) + } + + /** + * get the variables that were modified by the statement stmt + */ + def getModifiedVars(stmt: Stmt): Set[InfluenceSink] = { + stmt match { + case Seqn(ss, _) => ss.flatMap(s => getModifiedVars(s)).toSet + case LocalVarAssign(l, _) => Set(LocalVarSink(l)) + case If(_, thn, els) => getModifiedVars(thn) ++ getModifiedVars(els) + case While(_, _, body) => getModifiedVars(body) + case MethodCall(name, _, targets) => + val method = prog.methodsByName(name) + val methodInfluences = getMethodAnalysisMap(method) + val mightContainAssumeStmts = methodInfluences.keySet.exists(AnalysisUtils.isAssumeSink) + val targetSinks: Set[InfluenceSink] = targets.map(target => LocalVarSink(target)).toSet + if (mightContainAssumeStmts) { + targetSinks + AssumeMethodInfluenceSink(method) + } else { + targetSinks + } + case i: Inhale => Set(AssumeStmtInfluenceSink(i)) + case _: Assume => + assert(assertion = false, "Assume statements should have been replaced by inhale statements") + ??? + case Label(_, _) => Set.empty + case Quasihavoc(_, _) => Set(HeapSink) + case Quasihavocall(_, _, _) => Set(HeapSink) + case ExistentialElim(vars, _, _) => vars.map(v => LocalVarSink(v.localVar)).toSet + case _ => Set.empty + } + } + + private def lookupVar(variable: InfluenceSink, graphMap: GraphMap): Set[InfluenceSource] = { + // Assume Nodes are added when they are first encountered(can be a method call or a assume / inhale statement), so they might not exist when looked up + variable match { + case _: AssumeInfluenceSink => graphMap.getOrElse(variable, Set.empty) + case _ => + assert(graphMap.contains(variable), "Variable " + variable + " not found in graph analysis") + graphMap(variable) + } + } + + /** + * Gets all variables used in a given expressions and maps them to their influences specified in given graph map + */ + private def getResolvedVarsFromExp(exp: Exp, graphMap: GraphMap): Set[InfluenceSource] = { + getSinksFromExpr(exp).flatMap(v => lookupVar(v, graphMap)) + } + + /** returns all the sinks inside an expression */ + def getSinksFromExpr(exp: Exp): Set[NonAssumeInfluenceSink] = { + exp match { + case l: LocalVar => Set(LocalVarSink(l)) + case BinExp(exp1, exp2) => getSinksFromExpr(exp1) ++ getSinksFromExpr(exp2) + case UnExp(exp) => getSinksFromExpr(exp) + case f: FuncApp => + val isHeapDependent = Expressions.couldBeHeapDependent(f.func(prog), prog) + f.args.flatMap(e => getSinksFromExpr(e)).toSet ++ (if (isHeapDependent) Set(HeapSink) else Set.empty) + case DomainFuncApp(_, exps, _) => exps.flatMap(e => getSinksFromExpr(e)).toSet + case _: ForPerm | _: CurrentPerm => Set(HeapSink) + case FieldAccess(v, _) => getSinksFromExpr(v) + HeapSink + case AccessPredicate(access, _) => getSinksFromExpr(access) + HeapSink + case _ => Set.empty + } + } +} diff --git a/src/test/resources/all/basic/many_conjuncts.vpr b/src/test/resources/all/basic/many_conjuncts.vpr index 3fde77a99..9951e9cc0 100644 --- a/src/test/resources/all/basic/many_conjuncts.vpr +++ b/src/test/resources/all/basic/many_conjuncts.vpr @@ -15,7 +15,7 @@ field acq: Bool predicate AcqConjunct(x: Ref, idx: Int) domain parallelHeaps { - function heap(x: Ref) : Int + function heap_lookup(x: Ref) : Int function is_ghost(x:Ref) : Bool } @@ -28,25 +28,25 @@ domain reads { method read(data: Ref, count: Ref, ghost: Ref) returns (v: Int) - requires heap(data) == 0 && (heap(count) == 0 && (heap(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) - ensures heap(data) == 0 && (heap(count) == 0 && (heap(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) && (data.val == v && [true, perm(data.val) == none]) + requires heap_lookup(data) == 0 && (heap_lookup(count) == 0 && (heap_lookup(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) + ensures heap_lookup(data) == 0 && (heap_lookup(count) == 0 && (heap_lookup(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) && (data.val == v && [true, perm(data.val) == none]) { v := data.val } method read_erroneous(data: Ref, count: Ref, ghost: Ref) returns (v: Int) - requires heap(data) == 0 && (heap(count) == 0 && (heap(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) + requires heap_lookup(data) == 0 && (heap_lookup(count) == 0 && (heap_lookup(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) //:: ExpectedOutput(postcondition.violated:assertion.false) - ensures heap(data) == 0 && (heap(count) == 0 && (heap(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) && (data.val == v && [true, perm(data.val) == none] && false) + ensures heap_lookup(data) == 0 && (heap_lookup(count) == 0 && (heap_lookup(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) && (data.val == v && [true, perm(data.val) == none] && false) { v := data.val } method read2(data: Ref, count: Ref, ghost: Ref) returns (v: Int) requires - heap(data) == 0 && - heap(count) == 0 && - heap(ghost) == 0 && + heap_lookup(data) == 0 && + heap_lookup(count) == 0 && + heap_lookup(ghost) == 0 && is_ghost(ghost) && acc(data.val, rd()) && acc(ghost.val, rd()) && @@ -58,9 +58,9 @@ method read2(data: Ref, count: Ref, ghost: Ref) returns (v: Int) acc(count.init, wildcard) ensures - heap(data) == 0 && - heap(count) == 0 && - heap(ghost) == 0 && + heap_lookup(data) == 0 && + heap_lookup(count) == 0 && + heap_lookup(ghost) == 0 && is_ghost(ghost) && acc(data.val, rd()) && acc(ghost.val, rd()) && @@ -78,9 +78,9 @@ method read2(data: Ref, count: Ref, ghost: Ref) returns (v: Int) method read2_erroneous(data: Ref, count: Ref, ghost: Ref) returns (v: Int) requires - heap(data) == 0 && - heap(count) == 0 && - heap(ghost) == 0 && + heap_lookup(data) == 0 && + heap_lookup(count) == 0 && + heap_lookup(ghost) == 0 && is_ghost(ghost) && acc(data.val, rd()) && acc(ghost.val, rd()) && @@ -93,9 +93,9 @@ method read2_erroneous(data: Ref, count: Ref, ghost: Ref) returns (v: Int) ensures //:: ExpectedOutput(postcondition.violated:assertion.false) - heap(data) == 0 && - heap(count) == 0 && - heap(ghost) == 0 && + heap_lookup(data) == 0 && + heap_lookup(count) == 0 && + heap_lookup(ghost) == 0 && is_ghost(ghost) && acc(data.val, rd()) && acc(ghost.val, rd()) && diff --git a/src/test/resources/all/issues/silicon/0365.vpr b/src/test/resources/all/issues/silicon/0365.vpr index 9a086ced6..5800688ec 100644 --- a/src/test/resources/all/issues/silicon/0365.vpr +++ b/src/test/resources/all/issues/silicon/0365.vpr @@ -16,15 +16,15 @@ function tokCountRef(r:Ref): Ref domain parallelHeaps { function temp(x: Ref): Ref function temp_inv(x: Ref): Ref - function heap(x: Ref): Int + function heap_lookup(x: Ref): Int function is_ghost(x: Ref): Bool // WARNING: The two axioms can cause a matching loop axiom inv_temp { - (forall r: Ref :: { temp(r) } temp_inv(temp(r)) == r && (is_ghost(r) ? temp(r) == r : heap(temp(r)) == heap(r) - 3)) + (forall r: Ref :: { temp(r) } temp_inv(temp(r)) == r && (is_ghost(r) ? temp(r) == r : heap_lookup(temp(r)) == heap_lookup(r) - 3)) } axiom inv_temp_inv { - (forall r: Ref :: { temp_inv(r) } temp(temp_inv(r)) == r && (is_ghost(r) ? temp_inv(r) == r : heap(temp_inv(r)) == heap(r) + 3)) + (forall r: Ref :: { temp_inv(r) } temp(temp_inv(r)) == r && (is_ghost(r) ? temp_inv(r) == r : heap_lookup(temp_inv(r)) == heap_lookup(r) + 3)) } } diff --git a/src/test/resources/quantifiedpermissions/misc/misc1.vpr b/src/test/resources/quantifiedpermissions/misc/misc1.vpr index d30d18644..fff21de5e 100644 --- a/src/test/resources/quantifiedpermissions/misc/misc1.vpr +++ b/src/test/resources/quantifiedpermissions/misc/misc1.vpr @@ -1,6 +1,6 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + field val : Int domain parallelHeaps { @@ -12,10 +12,10 @@ domain parallelHeaps { function temp(x: Ref) : Ref function temp_inv(x: Ref) : Ref - function heap(x: Ref) : Int + function heap_lookup(x: Ref) : Int function is_ghost(x:Ref) : Bool - axiom inv_temp { forall r:Ref :: {temp(r)} temp_inv(temp(r)) == r && (is_ghost(r) ? temp(r) == r : heap(temp(r)) == -3) } + axiom inv_temp { forall r:Ref :: {temp(r)} temp_inv(temp(r)) == r && (is_ghost(r) ? temp(r) == r : heap_lookup(temp(r)) == -3) } } domain reads { @@ -31,9 +31,9 @@ domain reads { method clone(data: Ref, count: Ref, ghost: Ref) - requires heap(data) == 0 - && heap(count) == 0 - && heap(ghost) == 0 + requires heap_lookup(data) == 0 + && heap_lookup(count) == 0 + && heap_lookup(ghost) == 0 && is_ghost(ghost) && acc(data.val, rd()) && acc(ghost.val, rd()) diff --git a/src/test/resources/reasoning/existential_elim_fail1.vpr b/src/test/resources/reasoning/existential_elim_fail1.vpr new file mode 100644 index 000000000..8811d6472 --- /dev/null +++ b/src/test/resources/reasoning/existential_elim_fail1.vpr @@ -0,0 +1,11 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + + +field f: Int + +method ex2() +{ + //:: ExpectedOutput(typechecker.error) + obtain x: Ref where {x.f} acc(x.f) // impure expressions are disallowed +} diff --git a/src/test/resources/reasoning/existential_elim_success1.vpr b/src/test/resources/reasoning/existential_elim_success1.vpr new file mode 100644 index 000000000..4e54d8ee0 --- /dev/null +++ b/src/test/resources/reasoning/existential_elim_success1.vpr @@ -0,0 +1,29 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function eq(x: Int, y: Int): Bool { + x == y +} + +method ex1() + requires exists x: Int :: { eq(x, 42) } eq(x, 42) +{ + obtain x:Int where eq(x, 42) + assert x == 42 + //:: ExpectedOutput(assert.failed:assertion.false) + assert false +} + +function geq(x:Int, y:Int) : Bool +{ + x>=y +} + +method ex3() +{ + assert geq(3, 0) + obtain x:Int, y:Int where {geq(x,y)} geq(x,y) + assert x>=y + //:: ExpectedOutput(assert.failed:assertion.false) + assert false +} diff --git a/src/test/resources/reasoning/immutableVar.vpr b/src/test/resources/reasoning/immutableVar.vpr new file mode 100644 index 000000000..38fa6f70f --- /dev/null +++ b/src/test/resources/reasoning/immutableVar.vpr @@ -0,0 +1,59 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function P(x: Int) : Bool { + x == 0 +} + +function Q(x: Int) : Bool { + x == 0 +} + +method xassigned() +{ + var z:Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + var y:Int := x+1 + x:=2 + } +} + +method xwhile() +{ + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + while (x<0) { + x := x+1 + } + } +} + +method xif() +{ + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + var y: Int := 2 + if (y==2) { + y:= y-1 + } else { + x := x+1 + } + } +} + +method xmultOK() +{ + prove forall x:Int, y:Int {P(x),P(y)} assuming P(x) implies Q(x) { + var z: Int := 5 + } +} + +method xmult() +{ + //:: ExpectedOutput(consistency.error) + prove forall x:Int, y:Int {P(x),P(y)} assuming P(x) implies Q(x) { + x:=y + y:=3 + } +} \ No newline at end of file diff --git a/src/test/resources/reasoning/influenced_heap.vpr b/src/test/resources/reasoning/influenced_heap.vpr new file mode 100644 index 000000000..a207ad563 --- /dev/null +++ b/src/test/resources/reasoning/influenced_heap.vpr @@ -0,0 +1,23 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +field f:Int + + +method exampleHeapArg(b:Ref) returns (c:Int) +requires acc(b.f) +influenced heap by {heap,b} +//:: ExpectedOutput(consistency.error) +influenced c by { b } +{ + + c := b.f +} + + +method exampleHeap(b:Int) returns (c:Int) +influenced heap by {heap} +influenced c by {} +{ + c := 3 +} \ No newline at end of file diff --git a/src/test/resources/reasoning/old_call_fail1.vpr b/src/test/resources/reasoning/old_call_fail1.vpr new file mode 100644 index 000000000..69c314d6f --- /dev/null +++ b/src/test/resources/reasoning/old_call_fail1.vpr @@ -0,0 +1,17 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +method foo() +//:: ExpectedOutput(typechecker.error) +requires oldCall[l](lemma()) +{ + var x: Int + //:: ExpectedOutput(typechecker.error) + x := oldCall[l](lemma()) // label l does not yet exist + label l + //:: ExpectedOutput(typechecker.error) + x := 42 + oldCall[l](lemma()) +} + +method lemma() returns (x: Int) +isLemma diff --git a/src/test/resources/reasoning/old_call_fail2.vpr b/src/test/resources/reasoning/old_call_fail2.vpr new file mode 100644 index 000000000..51ddd1389 --- /dev/null +++ b/src/test/resources/reasoning/old_call_fail2.vpr @@ -0,0 +1,12 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +method foo() +{ + var x: Int + label l + //:: ExpectedOutput(typechecker.error) + x := oldCall[l](nonlemma()) // only lemmas can be called +} + +method nonlemma() returns (x: Int) diff --git a/src/test/resources/reasoning/old_call_success1.vpr b/src/test/resources/reasoning/old_call_success1.vpr new file mode 100644 index 000000000..79b37dba2 --- /dev/null +++ b/src/test/resources/reasoning/old_call_success1.vpr @@ -0,0 +1,23 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +method foo() +{ + label l + + oldCall[l](lemma(42)) + + var y: Int + y := lemma(42) + y := oldCall[l](lemma(42)) + + y := oldCall[l](lemma(42)) +} + +method foo(x: Int) returns (y: Int) +isLemma +// decreases // is necessary for lemma +ensures x == y +{ + y := x +} diff --git a/src/test/resources/reasoning/set_vs_graph.vpr b/src/test/resources/reasoning/set_vs_graph.vpr new file mode 100644 index 000000000..4c905c149 --- /dev/null +++ b/src/test/resources/reasoning/set_vs_graph.vpr @@ -0,0 +1,173 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function P(x: Int) : Bool { + x == 0 +} + +function Q(x: Int) : Bool { + x == 0 +} + +method simple(x: Int) returns (z:Int) +{ + z := x +} + + +method mIfOK1(x:Int) returns (w:Int) +{ + w := 0 + var l :Int := 0 + var g: Int := 0 + if (l >= -1) { + g := x + } else { + w := 4 + } +} + + + +method mWhileOK(x:Int) returns (z:Int) +{ + var y: Int := 0 + while(y<100) { // will only be tainted after the 5th? iteration + var x4: Int := 0 + var x3: Int := 0 + var x2: Int := 0 + var x1: Int := 0 + z := x4 + x4 := x3 + x3 := x2 + x2 := x1 + x1 := x + y := y+1 + } +} + + +method mWhileNOK(x:Int) returns (z:Int) +{ + var y: Int := 0 + var x2: Int := 0 + var x1: Int := 0 + + while(y<100) { + z := x2 + x2 := x1 + x1 := x + y := y+1 + } +} + + +//graph at the end such that z is influenced by .init_z and .init_x +//correct because if loop not executed then z is influenced by .init_z? +method mWhileNOK2(x:Int) returns (z:Int) +{ + var y: Int := x + var x2: Int := 0 + var x1: Int := 0 + + while(y<100) { + z := x2 + x2 := x1 + y := y+1 + } +} + +method m0(x: Int) returns (z:Int) +{ + var y: Int := x+1 + if (true) { var w:Int } // this should work -> two separate blocks + // var y:Int := 0 //here duplicate identifier +} +method mIndirect(x:Int) returns (z:Int) +{ + var y:Int := x+1 + z := y + // problem if here var y:Int := 0 -> this will also be in tainted set + if (true) { var w:Int } +} + +method mIfCnd(x: Int) returns (z:Int, y:Int) +{ + if(x>5) { + z := 3 + } else { + y := 5 + } +} + + +method mIfOK2(x:Int) returns (w:Int) +{ + var l :Int := 0 + if (l >= -1) { + l := x + } else { + w := 4 // should be SAFE + } +} + +method mAssignOK2(x:Int) returns (r:Int) +{ + r:=x + r:=1 + +} + +method mAssignOK3(x:Int) returns (r:Int) +{ + r:=x + var y: Int + r:= y +} + +method m(a:Int,c:Bool) returns (d:Int,e:Int) +{ + while(c) { + d:=e + e:=a + } +} + +method mMany(a:Int,b:Int,c:Int,d:Int,e:Int,f:Int,g:Int,h:Int,i:Int,j:Int,k:Int,l:Int,m1:Int,n:Int,o:Int,p:Int,q:Int,r:Int,s:Int) returns (r1:Int,r2:Int,r3:Int,r4:Int,r5:Int,r6:Int) +requires p!=0 +{ + if(a 0 +} + +method ex1() +{ + var y: Int + prove forall x:Int {greaterthanzero(x)} assuming x>0 implies x>0 { + var z: Int := x+1 + } +} + + + +function g_zero(x:Int) : Bool { + x>0 +} +function greater(x:Int, y:Int) :Bool { + x>y +} +method ex2() +{ + var i:Int := 10 + var j:Int := 5 + prove forall x:Int, y:Int {g_zero(y),greater(x,y)} assuming (g_zero(y) && greater(x,y)) implies g_zero(x) { + var z: Bool := x>y + } + assert greater(i,j) +} + + +function P(k: Int) : Bool +{ + false +} + +function Q(k: Int) : Bool +{ + k==2 +} + +//assuming false +method m1() +{ + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + var y:Int := x+1 + } +} + diff --git a/src/test/resources/reasoning/universal_introduction/ui_assume.vpr b/src/test/resources/reasoning/universal_introduction/ui_assume.vpr new file mode 100644 index 000000000..0683d4398 --- /dev/null +++ b/src/test/resources/reasoning/universal_introduction/ui_assume.vpr @@ -0,0 +1,214 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function P(x: Int) : Bool { + x == 0 +} + +function Q(x: Int) : Bool { + x == 0 +} + +method assumeF() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + //:: ExpectedOutput(consistency.error) + assume(x==0) + + //:: ExpectedOutput(consistency.error) + assume(P(x) && Q(10)) + if(x==0) { + //:: ExpectedOutput(consistency.error) + assume(true) + } + while(x > 0) { + //:: ExpectedOutput(consistency.error) + assume(true) + } + } +} + +method assumeAssignF() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + var y: Int := x + //:: ExpectedOutput(consistency.error) + assume(y==0) + + if(y==0) { + //:: ExpectedOutput(consistency.error) + assume(true) + } + while(y > 0) { + //:: ExpectedOutput(consistency.error) + assume(true) + } + } +} + +method assumeMultipleF() +{ + prove forall x: Int, y: Int {P(x), P(y)} assuming P(x) && P(y) implies Q(x) && Q(y) { + //:: ExpectedOutput(consistency.error) + assume(y==x) + + if(y==x) { + //:: ExpectedOutput(consistency.error) + assume(true) + } + while(y > x) { + //:: ExpectedOutput(consistency.error) + assume(true) + } + } +} + + +method assumeMultipleNestedF() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + prove forall y: Int {P(y)} assuming P(y) implies Q(y) { + //:: ExpectedOutput(consistency.error) + assume(y==x) + + if(y==x) { + //:: ExpectedOutput(consistency.error) + assume(true) + } + while(y > x) { + //:: ExpectedOutput(consistency.error) + assume(true) + } + } + } +} + +method assumeMultipleNestedOuterInfluenceF() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + prove forall y: Int {P(y)} assuming P(y) implies Q(y) { + //:: ExpectedOutput(consistency.error) + assume(1==x) + + if(1==x) { + //:: ExpectedOutput(consistency.error) + assume(true) + } + while(1 > x) { + //:: ExpectedOutput(consistency.error) + assume(true) + } + } + } +} + +method assumeS() +{ + var y: Int := 0 + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + assume(y==0) + if(y==0) { + assume(true) + } + while(y > 0) { + assume(true) + } + } +} + +method assumeMethodCallF() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + //:: ExpectedOutput(consistency.error) + assumeSomething(x, x) + if(x > 0) { + //:: ExpectedOutput(consistency.error) + assumeSomething(10, 0) + } + while(x > 0) { + //:: ExpectedOutput(consistency.error) + assumeSomething(10, 0) + } + } +} + +method assumeMethodCallTaintedVarF() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + var y: Int := x + 1 + //:: ExpectedOutput(consistency.error) + assumeSomething(y, y) + if(y > 0) { + //:: ExpectedOutput(consistency.error) + assumeSomething(10, 0) + } + while(y > 0) { + //:: ExpectedOutput(consistency.error) + assumeSomething(10, 0) + } + } +} + +method assumeRecMethodCallF() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + //:: ExpectedOutput(consistency.error) + assumeRec1(x) + + if(x > 0) { + //:: ExpectedOutput(consistency.error) + assumeRec1(10) + } + while(x > 0) { + //:: ExpectedOutput(consistency.error) + assumeRec1(10) + } + } +} + +method assumeDeepRecMethodCallF() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + //:: ExpectedOutput(consistency.error) + assumeRec2(x) + if(x > 0) { + //:: ExpectedOutput(consistency.error) + assumeRec2(10) + } + while(x > 0) { + //:: ExpectedOutput(consistency.error) + assumeRec2(10) + } + } +} + +method assumeDeepRecMethodCall1S() +{ + var y: Int := 0 + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + assumeRec2(y) + } +} + +method assumeRec1(x: Int) { + assumeRec1(x - 1) + assumeSomething(x, x) +} + +method assumeRec2(x: Int) { + assumeRec3(x - 1) +} + +method assumeRec3(x: Int) { + assumeRec4(x - 1) +} + +method assumeRec4(x: Int) { + assumeRec2(x - 1) + assumeSomething(x, x) +} + +method assumeSomething(x: Int, y: Int) +{ + assume(x >= y) +} \ No newline at end of file diff --git a/src/test/resources/reasoning/universal_introduction/ui_assume_methods.vpr b/src/test/resources/reasoning/universal_introduction/ui_assume_methods.vpr new file mode 100644 index 000000000..9100fe685 --- /dev/null +++ b/src/test/resources/reasoning/universal_introduction/ui_assume_methods.vpr @@ -0,0 +1,167 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function P(x: Int) : Bool { + x == 0 +} + +function Q(x: Int) : Bool { + x == 0 +} + +method assumeMethodCall1() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + abstractNonTermImpl(10) + if(x > 0) { + //:: ExpectedOutput(consistency.error) + abstractNonTermImpl(10) + } + while(x > 0) + decreases x + { + //:: ExpectedOutput(consistency.error) + abstractNonTermImpl(10) + } + } +} + + +method assumeMethodCall2() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + //:: ExpectedOutput(consistency.error) + abstractNonTermImpl(x) + if(x > 0) { + //:: ExpectedOutput(consistency.error) + abstractNonTermImpl(x) + } + while(x > 0) + decreases x + { + //:: ExpectedOutput(consistency.error) + abstractNonTermImpl(x) + } + } +} + +method assumeMethodCall3() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + //:: ExpectedOutput(consistency.error) + abstractNonTermExpl(x) + if(x > 0) { + //:: ExpectedOutput(consistency.error) + abstractNonTermExpl(x) + } + while(x > 0) + decreases x + { + //:: ExpectedOutput(consistency.error) + abstractNonTermExpl(x) + } + } +} + +method assumeMethodCall4() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + abstractNonTermImplSpec(x) + if(x > 0) { + //:: ExpectedOutput(consistency.error) + abstractNonTermImplSpec(x) + } + while(x > 0) + decreases x + { + //:: ExpectedOutput(consistency.error) + abstractNonTermImplSpec(x) + } + } +} + +method assumeMethodCall5() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + abstractNonTermExplSpec(x) + if(x > 0) { + //:: ExpectedOutput(consistency.error) + abstractNonTermExplSpec(x) + } + //:: ExpectedOutput(consistency.error) + while(x > 0) { + //:: ExpectedOutput(consistency.error) + abstractNonTermExplSpec(x) + } + } +} + +method assumeMethodCall6() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + abstractNonTermImplNoAssumesSpec(x) + if(x > 0) { + abstractNonTermImplNoAssumesSpec(x) + } + while(x > 0) + decreases x + { + abstractNonTermImplNoAssumesSpec(x) + } + } +} + +method assumeMethodCall7() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + abstractNonTermExplNoAssumesSpec(x) + if(x > 0) { + abstractNonTermExplNoAssumesSpec(x) + } + while(x > 0) + decreases x + { + abstractNonTermExplNoAssumesSpec(x) + } + } +} + +method assumeMethodCall8() +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + abstractTerm(x) + if(x > 0) { + abstractTerm(x) + } + while(x > 0) + decreases x + { + abstractTerm(x) + } + } +} + + +method abstractNonTermImpl(x: Int) + +method abstractNonTermImplSpec(x: Int) + influenced assumes by {} + +method abstractNonTermExpl(x: Int) + decreases * + +method abstractNonTermExplSpec(x: Int) + decreases * + influenced assumes by {} + +method abstractNonTermImplNoAssumesSpec(x: Int) + assumesNothing + +method abstractNonTermExplNoAssumesSpec(x: Int) + decreases * + assumesNothing + +method abstractTerm(x: Int) + decreases x + + diff --git a/src/test/resources/reasoning/universal_introduction/ui_func.vpr b/src/test/resources/reasoning/universal_introduction/ui_func.vpr new file mode 100644 index 000000000..58ae73f0f --- /dev/null +++ b/src/test/resources/reasoning/universal_introduction/ui_func.vpr @@ -0,0 +1,45 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function P(x: Int) : Bool { + x == 0 +} + +function Q(x: Int) : Bool { + x == 0 +} + +function func1(x:Int) : Int +{ + x +} + +method mFunctionOK() +{ + var z: Int := 3 + var y: Int + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && y == z { + y := func1(z) + } +} + +method mFunctionNOK() +{ + var z: Int := 3 + var y: Int + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && y >= 0 || y < 0 { + y := func1(x) + } +} + +function func2(e: Ref): Ref { + e +} + +method mFunction2NOK() { + var x: Ref + prove forall i:Ref assuming true implies i == x { + x := test(i) + } +} \ No newline at end of file diff --git a/src/test/resources/reasoning/universal_introduction/ui_heap.vpr b/src/test/resources/reasoning/universal_introduction/ui_heap.vpr new file mode 100644 index 000000000..97be70cde --- /dev/null +++ b/src/test/resources/reasoning/universal_introduction/ui_heap.vpr @@ -0,0 +1,92 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function P(x: Int) : Bool { + x == 0 +} + +function Q(x: Int) : Bool { + x == 0 +} + +method mInhalingOK() +{ + var m: Int := 0 + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + var y: Int := 0 + inhale (y==0) + } +} + +field f: Int + +method mInhaleOK2(y: Ref) +{ + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + inhale (acc(y.f)) + } +} + +method mExhaleOK(y:Ref) +requires acc(y.f) +{ + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + exhale acc(y.f) + } +} + + +method mFieldAssignNOK1(y:Ref) +requires acc(y.f) +{ + //:: ExpectedOutput(consistency.error) + prove forall x: Int {P(x)} assuming P(x) implies Q(x) && y.f == x { + y.f := x + } +} + +method mFieldAssignNOK2(y:Ref) +{ + var w: Int + //:: ExpectedOutput(consistency.error) + prove forall x: Int {P(x)} assuming P(x) implies Q(x) && w == x { + var z: Int := x + w := z + } +} + + +method mFieldAssignOK1(y:Ref) +requires acc(y.f) +{ + var z: Int := 0 + prove forall x: Int {P(x)} assuming P(x) implies Q(x) && z >= 0 || z < 0 { + z := y.f + } +} + +method quasiHavocOk1(y:Ref) +{ + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && (y.f > 0 || y.f <= 0) { + quasihavoc y.f + } +} + + +method quasiHavocNOk1(y:Ref) +{ + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && (y.f > 0 || y.f <= 0) { + quasihavoc x == 10 ==> y.f + } +} + +method quasiHavocNOk2(y:Ref) +{ + //:: ExpectedOutput(consistency.error) + prove forall x:Idecreases xnt {P(x)} assuming P(x) implies Q(x) && (y.f > 0 || y.f <= 0) { + if(x == 100) { + quasihavoc y.f + } + } +} \ No newline at end of file diff --git a/src/test/resources/reasoning/universal_introduction/ui_if.vpr b/src/test/resources/reasoning/universal_introduction/ui_if.vpr new file mode 100644 index 000000000..283672851 --- /dev/null +++ b/src/test/resources/reasoning/universal_introduction/ui_if.vpr @@ -0,0 +1,77 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function P(x: Int) : Bool { + x == 0 +} + +function Q(x: Int) : Bool { + x == 0 +} + +method mIndirect() +{ + var z:Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && z == x { + var y:Int := x+1 + z := y // Consistency error + } + // problem if here var y:Int := 0 -> this will also be in tainted set + if (true) { var y:Int } +} + +method mIfCnd() +{ + var z: Int := 0 + var y: Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && y == 5 { + if(x>5) { + z := 3 + } else { + y := 5 + } + } +} + +method mIfNOK() +{ + var w :Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && w == x { + var l :Int := 0 + if (l >= -1) { + l := x + } else { + w := x + } + } +} + +method mIfOK1() +{ + var w :Int := 0 + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && w == 4 { + var l :Int := 0 + var g: Int := 0 + if (l >= -1) { + g := x + } else { + w := 4 + } + } +} + +method mIfOK2() +{ + var w :Int := 0 + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && w == 4 { + var l :Int := 0 + if (l >= -1) { + l := x + } else { + w := 4 // should be SAFE + } + } +} \ No newline at end of file diff --git a/src/test/resources/reasoning/universal_introduction/ui_methods.vpr b/src/test/resources/reasoning/universal_introduction/ui_methods.vpr new file mode 100644 index 000000000..e81705444 --- /dev/null +++ b/src/test/resources/reasoning/universal_introduction/ui_methods.vpr @@ -0,0 +1,304 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function P(x: Int) : Bool { + x == 0 +} + +function Q(x: Int) : Bool { + x == 0 +} + +method example1(x:Int, y:Int) returns (res: Int) +influenced res by {x, y} +{ + res := x-y +} + +method example2(x:Int, y:Int) returns (res: Int) +{ + res := 0 +} + +method mMethodCallNOK1() +{ + var z: Int + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && z == 0 { + z := example1(x,x) + } +} + +method mMethodCallNOK2() +{ + var z: Int + // This should be OK, since the return value in example2 does not depend on its arguments + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && z == 0 { + z := example2(x,x) + } +} + +//code with influenced by statement +method example3(x:Int, y:Int) returns (res: Int) +influenced res by {} +{ + res := 0 +} + +method mMethodCallOK1() +{ + var z: Int + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && z == 0 { + var y:Int := 3 + z := example3(y,y) + } +} + +//method with several return values +method exampleMult(x:Int, y:Int) returns (diff:Int, id:Int) +influenced diff by {x, y} +influenced id by {x} +{ + diff := x-y + id := x +} + +method mMethodCallNOK3() +{ + var z: Int + var w: Int + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && z == x - 3 && w == x { + var y: Int := 3 + z,w := exampleMult(y,x) + } +} + +method exampleIncomplete(b:Bool,c:Int) returns (z:Int, w:Int) +influenced w by {b} +{ + z := 3 + if (b) { + w := w + 1 + } +} + +method mMethodCallNOK4() +{ + var y:Int + var v:Int + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && y == 3 && v == x + 1 { + var bool:Bool := true + y,v := exampleIncomplete(bool,x) + } +} + +method exampleCompleteInfluence(b:Bool,c:Int) returns (z:Int, w:Int) +influenced w by {b} +influenced z by {} +{ + z := 3 + if (b) { + w := 13 + } +} + +method mMethodCallOK4() +{ + var y:Int + var v:Int + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && y == 3 && v == x + 1 { + var bool:Bool := true + y,v := exampleCompleteInfluence(bool,x) + } +} + + + +field f: Int + +method test() +{ + var r: Ref + var p: Perm + var i: Int + var j: Int + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + r := test1(r) + r := test2(r) + p := test3(p) + p := test4(p) + j, i := test5(i, j) + j, i := test5_equivalent(i, j) + j, i := test5_caller(i, j) + j, i := test6(i, j) + j, i := test7(i, j) + j, i := caller_test6(i, j, r) + j, i := caller_test6(i, j, r) + caller_caller_test6(i, j, r) + test8(r, j) + test9(r, i) + } +} + + +// Should be accepted +method test1(x: Ref) returns (z: Ref) + influenced z by {x} +{ + z := x +} + +// Should be rejected +method test2(x: Ref) returns (z: Ref) +//:: ExpectedOutput(consistency.error) + influenced z by {heap} +{ + z := x +} + +// Should be accepted +method test3(x: Perm) returns (y: Perm) + influenced y by {x} +{ + y := x +} + +// Should be rejected +method test4(x: Perm) returns (y: Perm) +//:: ExpectedOutput(consistency.error) + influenced y by {heap} +{ + y := x +} + +// Should be accepted (we interpret absence of influenced by as influenced by everything, as shown below) +method test5(x: Int, y: Int) returns (a: Int, b: Int) +{ + a := x + y + b := x + y +} + +// Both specifications are over approximated, the heap is not needed. An error is not expected, but a warning is logged +method test5_equivalent(x: Int, y: Int) returns (a: Int, b: Int) + influenced a by {y, x, heap} + influenced b by {x, heap, y} +{ + a := x + y + b := x + y +} + +method test5_caller(x: Int, y: Int) returns (a: Int, b: Int) + influenced heap by {heap} + influenced a by {y, x} + influenced b by {x, y} +{ + a, b := test5(x, y) +} + +// should be rejected (at most 1 line per return variable) +method test6(x: Int, y: Int) returns (a: Int, b: Int) + influenced a by {y, x} +//:: ExpectedOutput(consistency.error) + influenced b by { } +//:: ExpectedOutput(consistency.error) + influenced b by {x, y} +{ + a := x + y + b := x + y +} + +// should be rejected: x cannot be influenced by anything, since it's a formal argument +method test7(x: Int, y: Int) returns (a: Int, b: Int) + influenced a by {y, x} + influenced b by {x, y} +//:: ExpectedOutput(consistency.error) + influenced x by {x} +{ + a := x + y + b := x + y +} + +// The most precise annotation for this test is +// influenced a by {x, y} +// influenced b by {x, y} +// influenced heap by {heap, x} +method caller_test6(x: Int, y: Int, r: Ref) returns (a: Int, b: Int) + requires acc(r.f) + influenced b by {x, y} + influenced a by {x, y} +{ + a, b := test6(x, y) + r.f := x +} + +// Should be rejected: the heap (r.f in this case) +// is influenced by x in caller_test6 +method caller_caller_test6(x: Int, y: Int, r: Ref) + requires acc(r.f) +//:: ExpectedOutput(consistency.error) + influenced heap by {heap} +{ + var a: Int + var b: Int + a, b := caller_test6(x, y, r) +} + +// Should be rejected: The heap (x.f in this case) +// is influenced by y +method test8(x: Ref, y: Int) + requires acc(x.f) +//:: ExpectedOutput(consistency.error) + influenced heap by {heap} +{ + x.f := y +} + +// Should be rejected: The heap (permission to x.f in this case) +// is influenced by y +method test9(x: Ref, y: Int) + requires acc(x.f) +//:: ExpectedOutput(consistency.error) + influenced heap by {heap} +{ + if (y == 0) { + exhale acc(x.f) + } +} + + +method testRec1(x: Ref) + requires acc(x.f) + influenced heap by {heap, x} +{ + if (x.f == 0) { + exhale acc(x.f) + } +} + + +method testRec2(x: Ref) + requires acc(x.f) + influenced heap by {heap, x} +{ + testAssumesAbstract(x) + testRec1(x) +} + +method testAssumesAbstract(x: Ref) + influenced assumes by {x} + +function f1(i1: Int, i2: Int): Int + +method test_local_var_resolve(i2: Int) returns (ret: Int) +influenced ret by {i2} +{ + var i1: Int + ret := f1(i1, i2) +} + +method test_local_var_resolve_caller() { + prove forall x: Int assuming x != 0 implies x == 1 { + var i: Int := test_local_var_resolve(x) + } +} \ No newline at end of file diff --git a/src/test/resources/reasoning/universal_introduction/ui_while.vpr b/src/test/resources/reasoning/universal_introduction/ui_while.vpr new file mode 100644 index 000000000..2c12f8c60 --- /dev/null +++ b/src/test/resources/reasoning/universal_introduction/ui_while.vpr @@ -0,0 +1,107 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function P(x: Int) : Bool { + x == 0 +} + +function Q(x: Int) : Bool { + x == 0 +} + +method mWhileCnd() +{ + var z: Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && z >= 0 { + while(x>5) { + z := z+3 + } + } +} + +method mWhileOK() +{ + var z: Int := 0 + prove forall x:Int {P(x)} assuming P(x) implies Q(x) && z >= 0 { + var y: Int := 0 + while(y<5) { + z := z+3 + y := y+1 + } + } +} + +method mWhileOK2() +{ + var z: Int := 0 + prove forall x: Int {P(x)} assuming P(x) implies Q(x) && z == 0 { + var y: Int := 0 + while(y<100) { // will never be tainted as the variables are local + var x4: Int := 0 + var x3: Int := 0 + var x2: Int := 0 + var x1: Int := 0 + z := x4 + x4 := x3 + x3 := x2 + x2 := x1 + x1 := x + y := y+1 + } + } +} + +method mWhileNOK() +{ + var z: Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x: Int {P(x)} assuming P(x) implies Q(x) && z == x { + var y: Int := 0 + var x2: Int := 0 + var x1: Int := 0 + + while(y<100) { + z := x2 + x2 := x1 + x1 := x + y := y+1 + } + } +} + +method mWhileNOK2() +{ + var z: Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x: Int {P(x)} assuming P(x) implies Q(x) && z == 0 { + var y: Int := x + var x2: Int := 0 + var x1: Int := 0 + + //:: ExpectedOutput(consistency.error) + while(y<100) { + z := x2 + x2 := x1 + y := y+1 + } + } +} + +method mWhileOK3() +{ + var z: Int := 0 + prove forall x: Int {P(x)} assuming P(x) implies Q(x) && z == 0 { + var y: Int := 0 + var x2: Int := 0 + var x1: Int := 0 + + while(y<100) + decreases y + { + z := x2 + x2 := x1 + y := y+1 + } + } +} \ No newline at end of file diff --git a/src/test/resources/transformations/Performance/BinomialHeap.vpr b/src/test/resources/transformations/Performance/BinomialHeap.vpr index d8c17c505..c969f44aa 100644 --- a/src/test/resources/transformations/Performance/BinomialHeap.vpr +++ b/src/test/resources/transformations/Performance/BinomialHeap.vpr @@ -234,7 +234,7 @@ method findMinNode(arg: Ref) returns (res: Ref) field Nodes: Ref // BinomialHeapNode field size: Int // not read in the code, so we can omit it and simplify the predicates -predicate heap(this: Ref){ +predicate binheap(this: Ref){ acc(this.Nodes) && heapseg(this.Nodes, null) && sorted(this.Nodes, null) && (this.Nodes != null ==> segParent(this.Nodes, null) == null) && @@ -526,10 +526,10 @@ heapseg(this.Nodes, null) && sorted(this.Nodes, null) // in the callee method union or because it affects the fields we did // not model so far, namely size and parent. method extractMin(this: Ref) returns (res: Ref) - requires heap(this) - ensures heap(this) + requires binheap(this) + ensures binheap(this) { - unfold heap(this) + unfold binheap(this) var nodes: Ref := this.Nodes if(nodes == null){ res := null @@ -554,8 +554,8 @@ method extractMin(this: Ref) returns (res: Ref) invariant prevTemp != null && temp != minNode ==> treeDegree(prevTemp) < segDegree(temp, minNode, 0) invariant prevTemp != null && temp == minNode ==> treeDegree(prevTemp) < segDegree(minNode, null, 0) invariant temp != minNode ==> segDegree(temp, minNode, segLength(temp, minNode) - 1) < segDegree(minNode, null, 0) - invariant prevTemp != null ==> segSize(nodes, prevTemp) + treeSize(prevTemp) + segSize(temp, minNode) + segSize(minNode, null) == old(unfolding heap(this) in segSize(this.Nodes, null)) - invariant prevTemp == null ==> segSize(temp, minNode) + segSize(minNode, null) == old(unfolding heap(this) in segSize(this.Nodes, null)) + invariant prevTemp != null ==> segSize(nodes, prevTemp) + treeSize(prevTemp) + segSize(temp, minNode) + segSize(minNode, null) == old(unfolding binheap(this) in segSize(this.Nodes, null)) + invariant prevTemp == null ==> segSize(temp, minNode) + segSize(minNode, null) == old(unfolding binheap(this) in segSize(this.Nodes, null)) invariant temp != minNode ==> segParent(temp, minNode) == null invariant minNode != null ==> segParent(minNode, null) == null invariant prevTemp != null && nodes != prevTemp ==> segParent(nodes, prevTemp) == null @@ -637,5 +637,5 @@ method extractMin(this: Ref) returns (res: Ref) res := minNode } - fold heap(this) + fold binheap(this) }