diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala index c4d5f17cb..fa720e914 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/plugin/standard/reasoning/BeforeVerifyHelper.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/BeforeVerifyHelper.scala new file mode 100644 index 000000000..08050f7cd --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/BeforeVerifyHelper.scala @@ -0,0 +1,257 @@ +// 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 org.jgrapht.graph.DefaultEdge +import viper.silver.ast.utility.Expressions +import viper.silver.ast.{Apply, Exhale, Exp, FieldAssign, Fold, Inhale, LocalVar, LocalVarDecl, Method, MethodCall, Package, Position, Program, Seqn, Stmt, Unfold} +import viper.silver.plugin.standard.reasoning.analysis.VarAnalysisGraph +import viper.silver.plugin.standard.termination.{DecreasesSpecification, DecreasesStar, DecreasesTuple, DecreasesWildcard} +import viper.silver.verifier.{AbstractError, ConsistencyError} + +import scala.collection.mutable +import scala.jdk.CollectionConverters.CollectionHasAsScala + +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)) + } + + /** + * get all variables that are assigned to inside the block and take intersection with universal introduction + * variables. If they are contained throw error since these 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: Option[Set[LocalVarDecl]], quantified_vars: Seq[LocalVarDecl], reportError: AbstractError => Unit, u: UniversalIntro): Unit = { + if (modified_vars.isDefined) { + val reassigned_vars: Set[LocalVarDecl] = modified_vars.get.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)) + } + } + } + + private def specifiesLemma(m: Method): Boolean = (m.pres ++ m.posts).exists { + case _: Lemma => true + case _ => false + } + + /** check if isLemma precondition is correct */ + def checkLemma(input: Program, reportError: AbstractError => Unit): Unit = { + input.methods.foreach(method => { + val containsLemma = specifiesLemma(method) + var containsDecreases = false + if (containsLemma) { + /** check preconditions for decreases clause */ + method.pres.foreach { + case DecreasesTuple(_, _) => + containsDecreases = true + case DecreasesWildcard(_) => + containsDecreases = true + case DecreasesStar() => + reportError(ConsistencyError("decreases statement might not prove termination", method.pos)) + case _ => + () + } + /** check postconditions for decreases clause */ + method.posts.foreach { + case DecreasesTuple(_, _) => + containsDecreases = true + case DecreasesWildcard(_) => + containsDecreases = true + case DecreasesStar() => + reportError(ConsistencyError("decreases statement might not prove termination", method.pos)) + containsDecreases = true + case _ => () + } + + /** check info for decreases specification */ + method.meta._2 match { + case spec: DecreasesSpecification => + if (spec.star.isDefined) { + reportError(ConsistencyError("decreases statement might not prove termination", method.pos)) + containsDecreases = true + } else { + containsDecreases = true + } + case _ => + } + } + + /** report error if there is no decreases clause or specification */ + if (containsLemma && !containsDecreases) { + reportError(ConsistencyError(s"method ${method.name} marked lemma might not contain decreases clause", method.pos)) + } + + /** check method body for impure statements */ + if (containsLemma) { + checkBodyPure(method.body.getOrElse(Seqn(Seq(), Seq())()), method, input, reportError) + } + + }) + + } + + /** checks whether the body is pure, reports error if impure operation found */ + def checkBodyPure(stmt: Stmt, method: Method, prog: Program, reportError: AbstractError => Unit): Boolean = { + var pure: Boolean = true + stmt match { + case Seqn(ss, _) => + ss.foreach(s => { + pure = pure && checkBodyPure(s, method, prog, reportError) + }) + pure + + /** 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 containsLemma = specifiesLemma(mc) + + /** if called method is not a lemma report error */ + if (!containsLemma) { + reportError(ConsistencyError(s"method ${method.name} marked lemma might contain call to method ${m}", m.pos)) + false + } else { + pure + } + case _ => + pure + } + } + + /** check that influenced by expressions are exact or overapproximate the body of the method. */ + def checkInfluencedBy(input: Program, reportError: AbstractError => Unit): Unit = { + val body_graph_analysis: VarAnalysisGraph = VarAnalysisGraph(input, reportError) + input.methods.foreach(method => { + var return_vars = method.formalReturns.toSet ++ Seq(body_graph_analysis.heap_vertex) + val arg_vars = method.formalArgs.toSet ++ Seq(body_graph_analysis.heap_vertex) + + /** helper variable for error message, maps local variable to its position */ + var influenced_by_pos: Map[LocalVarDecl, Position] = Map() + + + val init_args_decl = method.formalArgs.map(a => body_graph_analysis.createInitialVertex(a)) + val init_rets_decl = method.formalReturns.map(r => body_graph_analysis.createInitialVertex(r)) + val method_vars: Map[LocalVarDecl, LocalVarDecl] = ((method.formalArgs zip init_args_decl) ++ (method.formalReturns zip init_rets_decl) ++ Seq((body_graph_analysis.heap_vertex, body_graph_analysis.createInitialVertex(body_graph_analysis.heap_vertex)))).toMap + val empty_body_graph = body_graph_analysis.createEmptyGraph(method_vars) + val heap_vert = LocalVarDecl(body_graph_analysis.heap_vertex.name, body_graph_analysis.heap_vertex.typ)() + + val influenced_graph = body_graph_analysis.copyGraph(empty_body_graph) + var influenced_exists: Boolean = false + /** iterate through method postconditions to find flow annotations */ + method.posts.foreach { + case v@FlowAnnotation(target, args) => + influenced_exists = true + + /** create target variable of flowannotation based on whether it is the heap or another return variable */ + val target_var: LocalVar = target match { + case value: Var => value.decl + case _ => body_graph_analysis.heap_vertex.localVar + } + val target_decl: LocalVarDecl = LocalVarDecl(target_var.name, target_var.typ)(v.pos) + + /** check whether the target variable is in fact a return variable */ + if (!return_vars.contains(target_decl)) { + reportError(ConsistencyError(s"Only return variables can be influenced and only one influenced by expression per return variable can exist. ${target_decl.name} may not be a return variable or might be used several times.", v.pos)) + } + /** keep track of which return variables have an influenced by annotation */ + return_vars -= target_decl + influenced_by_pos += (target_decl -> v.pos) + + + args.foreach(arg => { + + /** decide for each variable in the set of variables of the flow annotation whether they represent a normal variable or the heap */ + val arg_var: LocalVar = arg match { + case value: Var => value.decl + case _ => body_graph_analysis.heap_vertex.localVar + } + val arg_decl: LocalVarDecl = LocalVarDecl(arg_var.name, arg_var.typ)(arg_var.pos) + + /** check that each variable in the set is a method argument */ + if (!arg_vars.contains(arg_decl)) { + reportError(ConsistencyError(s"Only argument variables can be influencing the return variable. ${arg_decl.name} may not be an argument variable.", v.pos)) + } + + /** add corresponding edge from method argument to the target variable */ + influenced_graph.addEdge(method_vars(arg_decl), target_decl, new DefaultEdge) + }) + case _ => () + + } + /** for all remaining variables that didn't have an influenced by annotation create an edge from every method argument to the return variable + * to overapproximate the information flow + */ + return_vars.foreach(rv => { + (method.formalArgs ++ Seq(body_graph_analysis.heap_vertex)).foreach(a => { + if (!influenced_graph.containsVertex(method_vars(a))) { + influenced_graph.addVertex(method_vars(a)) + } + if (!influenced_graph.containsVertex(rv)) { + influenced_graph.addVertex(rv) + } + influenced_graph.addEdge(method_vars(a), rv, new DefaultEdge) + }) + }) + + /** for evaluation purposes if graph of method body should be created even though there is no influenced by annotation */ + //val body_graph = body_graph_analysis.compute_graph(method.body.getOrElse(Seqn(Seq(), Seq())()), method_vars) + + /** if influenced by annotation exists create graph of the method body and check whether the influenced by expression is correct */ + if (influenced_exists) { + val body_graph = body_graph_analysis.compute_graph(method.body.getOrElse(Seqn(Seq(), Seq())()), method_vars) + + /** ignore the edges from the .init_ret to the ret vertex since before the method there is no init value of a return variable. */ + method.formalReturns.foreach(r => { + body_graph.removeAllEdges(method_vars(r), r) + }) + + /** the set of all incoming edges to the return variables of the method body graph should be a subset of the set of the incoming edges of the influenced by graph */ + (method.formalReturns ++ Seq(heap_vert)).foreach(r => { + body_graph.incomingEdgesOf(r).forEach(e => { + if (!influenced_graph.containsEdge(body_graph.getEdgeSource(e), body_graph.getEdgeTarget(e))) { + val ret_sources: String = body_graph.incomingEdgesOf(r).asScala.map(e => body_graph.getEdgeSource(e).name).toList.sortWith(_ < _).mkString(", ").replace(".init_", "").replace(".", "") + reportError(ConsistencyError("influenced by expression may be incorrect. Possible influenced by expression: \n" + "influenced " + r.name.replace(".", "") + " by {" + ret_sources + "}", influenced_by_pos(r))) + } + }) + }) + } + }) + } +} 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..166e8d6a8 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningASTExtension.scala @@ -0,0 +1,148 @@ +// 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 quantifier must be of Bool type, but found ${exp.typ}", exp.pos)) else Seq()) ++ + (if (varList.isEmpty) Seq(ConsistencyError("Quantifier 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 space <> 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], exp1: Exp, exp2: 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 (!(exp1 isSubtype Bool)) Seq(ConsistencyError(s"Body of universal quantifier must be of Bool type, but found ${exp1.typ}", exp1.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(exp1) <+> + text("implies") <+> toParenDoc(exp2) <+> + showBlock(block) + } + + override val extensionSubnodes: Seq[Node] = varList ++ triggers ++ Seq(exp1, exp2, 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))) + } +} + +case class Heap()(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 = PHeapKeyword.keyword +} + +case class Var(decl: LocalVar)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends FlowVar { + override val extensionSubnodes: Seq[Node] = Seq(decl) + override def typ: Type = decl.typ + override def prettyPrint: PrettyPrintPrimitives#Cont = show(decl) +} + +case class FlowAnnotation(v: FlowVar, varList: Seq[FlowVar])(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, "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 _ => 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] = { + var s = Seq.empty[ConsistencyError] + if (!Consistency.noResult(this)) + s :+= ConsistencyError("Result variables are only allowed in postconditions of functions.", pos) + if (!Consistency.noDuplicates(rets)) + s :+= ConsistencyError("Targets are not allowed to have duplicates", rets.head.pos) + s ++= args.flatMap(Consistency.checkPure) + s + } + + 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..04088775e --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningErrors.scala @@ -0,0 +1,40 @@ +// 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 = " no witness could be found." + + 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 = " not true for all vars." + + 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 FlowAnalysisFailed(override val offendingNode: ErrorNode, override val reason: ErrorReason, override val cached: Boolean = false) extends ExtensionAbstractVerificationError { + override val id = "flow analysis.failed" + override val text = " ." + + override def withNode(offendingNode: errors.ErrorNode = this.offendingNode): FlowAnalysisFailed = + FlowAnalysisFailed(this.offendingNode, this.reason, this.cached) + + override def withReason(r: ErrorReason): FlowAnalysisFailed = FlowAnalysisFailed(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..cb1553576 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPASTExtension.scala @@ -0,0 +1,200 @@ +// 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.{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, 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 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 { + 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(e1)) + } +} + +case class PFlowAnnotation(v: PFlowVar, byKw: PReserved[PByKeyword.type], groupedVarList: PGrouped[PSym.Brace, Seq[PFlowVar]])(val pos: (Position,Position)) extends PExtender with PExp { + lazy val varList: Seq[PFlowVar] = groupedVarList.inner + + override def typeSubstitutions: Seq[PTypeSubstitution] = Seq(PTypeSubstitution.id) + + override def forceSubstitution(ts: PTypeSubstitution): Unit = {} + + //from here new + 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 = { + FlowAnnotation(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 = {} +} + +case class PHeap(heap: PReserved[PHeapKeyword.type])(val pos: (Position,Position)) extends PFlowVar { + override def translate(t: Translator): Heap = { + Heap()(t.liftPos(this)) + } + + override def pretty: String = PHeapKeyword.keyword +} + +case class PVar(decl: PIdnUseExp)(val pos: (Position,Position)) extends PFlowVar { + 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. + 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..0df3b9572 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala @@ -0,0 +1,368 @@ +// 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 org.jgrapht.Graph +import org.jgrapht.graph.{DefaultDirectedGraph, DefaultEdge} +import viper.silver.ast._ +import viper.silver.ast.utility.rewriter.{StrategyBuilder, Traverse} +import viper.silver.ast.utility.ViperStrategy +import viper.silver.parser.FastParserCompanion.whitespace +import viper.silver.parser._ +import viper.silver.plugin.standard.reasoning.analysis.{SetGraphComparison, VarAnalysisGraph} +import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} +import viper.silver.verifier._ + +import scala.annotation.unused +import scala.collection.mutable + +class ReasoningPlugin(@unused reporter: viper.silver.reporter.Reporter, + @unused logger: ch.qos.logback.classic.Logger, + @unused config: viper.silver.frontend.SilFrontendConfig, + fp: FastParser) extends SilverPlugin with ParserPluginTemplate with SetGraphComparison with BeforeVerifyHelper { + + import fp.{exp, ParserExtension, lineCol, _file} + import FastParserCompanion.{ExtendedParsing, PositionParsing, reservedKw, reservedSym} + + + override def reportErrorWithMsg(error: AbstractError): Unit = reportError(error) + + /** Parser for existential elimination statements. */ + def existential_elim[$: 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 universal_intro[$: 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) ~ influenced_by) map (PSpecification.apply _).tupled).pos + + def heap[$: P]: P[PHeap] = P(P(PHeapKeyword) map (PHeap(_) _)).pos // note that the parentheses are not redundant + + def singleVar[$: P]: P[PVar] = P(fp.idnuse map (PVar(_) _)).pos // note that the parentheses are not redundant + def vars_and_heap[$: P]: P[Seq[PFlowVar]] = (heap | singleVar).delimited(PSym.Comma).map(_.toSeq) + + def influenced_by[$: P]: P[PFlowAnnotation] = P(((heap | singleVar) ~ P(PByKeyword) ~/ vars_and_heap.braces) map { + case (v, byKw, groupedVarList) => PFlowAnnotation(v, byKw, groupedVarList)(_) + }).pos + + /** parser for lemma annotation */ + def lemma[$: P]: P[PSpecification[PIsLemmaKeyword.type]] = + P((P(PIsLemmaKeyword) ~ lemmaClause) map (PSpecification.apply _).tupled).pos + + // lemma clause is completely artificial and is created out of nowhere at the parser's current position + def lemmaClause[$: P]: P[PLemmaClause] = (Pass(()) map { _ => PLemmaClause()(_) }).pos + + /** 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)) + + /** 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(existential_elim(_)) + ParserExtension.addNewStmtAtEnd(universal_intro(_)) + + /** add influenced by flow annotation to as a postcondition */ + ParserExtension.addNewPostCondition(flowSpec(_)) + + /** 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) + } + + + override def beforeVerify(input: Program): Program = { + + /** for evaluation purposes */ + //val begin_time = System.currentTimeMillis() + + 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 */ + checkLemma(input, reportError) + + /** check that influenced by expressions are exact or overapproximate the body of the method. */ + checkInfluencedBy(input, reportError) + + + /** method call to compare the analysis of the set-approach vs. the graph approach */ + //compareGraphSet(input, reportError) + + + val newAst: Program = ViperStrategy.Slim({ + + /** remove the influenced by postconditions. + * remove isLemma */ + case m: Method => + + + var postconds: Seq[Exp] = Seq() + m.posts.foreach { + case _: FlowAnnotation => + postconds = postconds + case _: Lemma => + postconds = postconds + case s@_ => + postconds = postconds ++ Seq(s) + } + var preconds: Seq[Exp] = Seq() + m.pres.foreach { + case _: Lemma => + preconds = preconds + case s@_ => + preconds = preconds ++ Seq(s) + } + val newMethod = + if (postconds != m.posts || preconds != m.pres) { + m.copy(pres = preconds, posts = postconds)(m.pos, m.info, m.errT) + } else { + m + } + + newMethod + + case o@OldCall(methodName, args, rets, lbl) => + /** check whether called method is a lemma */ + val currmethod = input.findMethod(methodName) + val isLemma = (currmethod.pres ++ currmethod.posts).exists { + case _: Lemma => true + case _ => false + } + + if (!isLemma) { + reportError(ConsistencyError(s"method ${currmethod.name} called in old context must be lemma", o.pos)) + } + + var new_pres: Seq[Exp] = Seq() + var new_posts: Seq[Exp] = Seq() + var new_v_map: Seq[(LocalVarDecl, Exp)] = + (args zip currmethod.formalArgs).map(zipped => { + val formal_a: LocalVarDecl = zipped._2 + val arg_exp: Exp = zipped._1 + formal_a -> arg_exp + }) + new_v_map ++= + (rets zip currmethod.formalReturns).map(zipped => { + val formal_r: LocalVarDecl = zipped._2 + val r: LocalVar = zipped._1 + formal_r -> r + }) + /** replace all variables in precondition with fresh variables */ + currmethod.pres.foreach { + case Lemma() => () + case p => + new_pres ++= Seq(applySubstitutionWithExp(new_v_map, p)) + } + + /** replace all variables in postcondition with fresh variables */ + currmethod.posts.foreach { + case Lemma() => () + case p => + new_posts ++= Seq(applySubstitutionWithExp(new_v_map, p)) + } + + /** create new variable declarations to havoc the lhs of the oldCall */ + var new_v_decls: Seq[LocalVarDecl] = Seq() + var rTov: Map[LocalVar,LocalVarDecl] = Map() + for (r <- rets) { + val new_v = LocalVarDecl(uniqueName(".v", usedNames),r.typ)(r.pos) + new_v_decls = new_v_decls ++ Seq(new_v) + rTov += (r -> new_v) + } + + + Seqn( + new_pres.map(p => + Assert(LabelledOld(p, lbl)(p.pos))(o.pos) + ) + ++ + + rets.map(r => { + LocalVarAssign(r,rTov(r).localVar)(o.pos) + }) + ++ + + + new_posts.map(p => + Inhale(LabelledOld(p, lbl)(p.pos))(o.pos) + ), + new_v_decls + )(o.pos) + + + case e@ExistentialElim(v, trigs, exp) => + val (new_v_map, new_exp) = substituteWithFreshVars(v, exp, usedNames) + val new_trigs = trigs.map(t => Trigger(t.exps.map(e1 => applySubstitution(new_v_map, e1)))(t.pos)) + Seqn( + Seq( + Assert(Exists(new_v_map.map(_._2), new_trigs, new_exp)(e.pos, ReasoningInfo))(e.pos) + ) + ++ + v.map(variable => LocalVarDeclStmt(variable)(variable.pos)) //list of variables + ++ + Seq( + Inhale(exp)(e.pos) + ), + Seq() + )(e.pos) + + case u@UniversalIntro(v, trigs, exp1, exp2, blk) => + val boolvar = LocalVarDecl(uniqueName("b", usedNames), Bool)(exp1.pos) + + val vars_outside_blk: mutable.Set[Declaration] = mutable.Set() + + /** Get all variables that are in scope in the current method but not inside the block */ + input.methods.foreach(m => m.body.get.ss.foreach(s => { + if (s.contains(u)) { + vars_outside_blk ++= mutable.Set(m.transitiveScopedDecls: _*) + } + })) + + /** Qunatified variables in the universal introduction statement are tainted */ + val tainted: Set[LocalVarDecl] = v.toSet + + + /** + * GRAPH VERSION + */ + + val graph_analysis: VarAnalysisGraph = VarAnalysisGraph(input, reportError) + + + /** create graph with vars that are in scope only outside of the universal introduction code block including the qunatified variables*/ + vars_outside_blk --= mutable.Set(u.transitiveScopedDecls: _*) + vars_outside_blk ++= v + + val graph: Graph[LocalVarDecl, DefaultEdge] = new DefaultDirectedGraph[LocalVarDecl, DefaultEdge](classOf[DefaultEdge]) + + /** Map that contains all variables where the key is represents the variables final value and the value the variables initial value before a statement. */ + var allVertices: Map[LocalVarDecl, LocalVarDecl] = Map[LocalVarDecl, LocalVarDecl]() + + /** add heap variables to vertices */ + allVertices += (graph_analysis.heap_vertex -> graph_analysis.createInitialVertex(graph_analysis.heap_vertex)) + + vars_outside_blk.foreach { + case v_decl: LocalVarDecl => + val v_init = graph_analysis.createInitialVertex(v_decl) + allVertices += (v_decl -> v_init) + + /** add all variable to the graph */ + graph.addVertex(v_init) + graph.addVertex(v_decl) + case _ => + } + + /** + * 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 written_vars: Option[Set[LocalVarDecl]] = graph_analysis.getModifiedVars(allVertices ,blk) + checkReassigned(written_vars, v, reportError, u) + + /** execute modular flow analysis using graphs for the universal introduction statement */ + graph_analysis.executeTaintedGraphAnalysis(tainted, blk, allVertices, u) + + /** + * SET VERSION + */ + /* + val tainted_decls: Set[Declaration] = tainted.map(t => t.asInstanceOf[Declaration]) + executeTaintedSetAnalysis(tainted_decls, vars_outside_blk, blk, u, reportError) + */ + + /** Translate the new syntax into Viper language */ + val (new_v_map, new_exp1) = substituteWithFreshVars(v, exp1, usedNames) + val new_exp2 = applySubstitution(new_v_map, exp2) + val arb_vars = new_v_map.map(vars => vars._2) + val new_trigs = trigs.map(t => Trigger(t.exps.map(e1 => applySubstitution(new_v_map, e1)))(t.pos)) + val lbl = uniqueName("l", usedNames) + + Seqn( + Seq( + Label(lbl, Seq())(u.pos), + If(boolvar.localVar, + Seqn( + Seq( + Inhale(exp1)(exp1.pos) + ), + Seq())(exp1.pos), + Seqn(Seq(), Seq())(exp1.pos) + + )(exp1.pos), + blk, + Assert(Implies(boolvar.localVar, exp2)(exp2.pos))(exp2.pos), + Inhale(Forall(arb_vars, new_trigs, Implies(LabelledOld(new_exp1, lbl)(exp2.pos), new_exp2)(exp2.pos))(exp2.pos))(exp2.pos) + ), + Seq(boolvar) ++ v + )(exp1.pos) + + }, Traverse.TopDown).execute[Program](input) + /** for evaluation purposes */ + /* + val end_time = System.currentTimeMillis() + println("--------------------------------------------------------------------------") + println("beforeVerify time: " + (end_time - begin_time) + "ms") + println("--------------------------------------------------------------------------") + */ + newAst + } +} diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/SetGraphComparison.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/SetGraphComparison.scala new file mode 100644 index 000000000..2324b4789 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/SetGraphComparison.scala @@ -0,0 +1,152 @@ +// 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 org.jgrapht.Graph +import org.jgrapht.graph.DefaultEdge +import viper.silver.ast.{Declaration, LocalVarDecl, Program, Stmt} +import viper.silver.verifier.AbstractError + +import scala.jdk.CollectionConverters.CollectionHasAsScala + +trait SetGraphComparison extends VarAnalysisSet { + private def computeSet(v: Declaration, blk: Stmt): Set[LocalVarDecl] = { + get_tainted_vars_stmt(Set(v), blk).map(v => v.asInstanceOf[LocalVarDecl]) + } + + private def computeGraph(graph_analysis: VarAnalysisGraph, vars: Set[LocalVarDecl], blk: Stmt): (Graph[LocalVarDecl, DefaultEdge]/*, Map[LocalVarDecl,LocalVarDecl]*/) = { + + var allVertices: Map[LocalVarDecl, LocalVarDecl] = Map.empty + + /** add heap variables to vertices */ + allVertices += (graph_analysis.heap_vertex -> graph_analysis.createInitialVertex(graph_analysis.heap_vertex)) + + vars.foreach(v => { + val v_decl = v + val v_init = graph_analysis.createInitialVertex(v_decl) + allVertices += (v_decl -> v_init) + + }) + graph_analysis.compute_graph(blk, allVertices) + } + + def compareGraphSet(prog: Program, reportError: AbstractError => Unit): Unit = { + + /** + * SETS + */ + val beginTimeSets = System.currentTimeMillis() + var setForMethods: Map[String, Map[LocalVarDecl, Set[LocalVarDecl]]] = Map() + prog.methods.foreach(m => { + var vToSet: Map[LocalVarDecl, Set[LocalVarDecl]] = Map() + val allParameters: Set[LocalVarDecl] = m.formalArgs.toSet.concat(m.formalReturns.toSet) + m.formalArgs.foreach(arg => { + vToSet += (arg -> computeSet(arg,m.bodyOrAssumeFalse).intersect(allParameters)) + }) + setForMethods += (m.name -> vToSet) + + }) + + val endTimeSets = System.currentTimeMillis() + val totalTimeSets = endTimeSets - beginTimeSets + println("Time for Set analysis: " + totalTimeSets + "ms") + /* + val beginTimeSets = System.currentTimeMillis() + var vToSet: Map[LocalVarDecl,Set[LocalVarDecl]] = Map() + vars.foreach(v => { + vToSet += (v.asInstanceOf[LocalVarDecl] -> (computeSet(v,blk).intersect(vars.map(d => d.asInstanceOf[LocalVarDecl])))) + }) + val endTimeSets = System.currentTimeMillis() + val totalTimeSets = endTimeSets - beginTimeSets + + + println("Time for Set analysis: " + totalTimeSets + "ms") + + */ + + + /** + * GRAPHS + */ + + val beginTimeGraphs = System.currentTimeMillis() + val graph_analysis : VarAnalysisGraph = VarAnalysisGraph(prog, reportError) + var graphForMethods: Map[String, Graph[LocalVarDecl,DefaultEdge]] = Map[String, Graph[LocalVarDecl,DefaultEdge]]() + prog.methods.foreach(m => { + graphForMethods += (m.name -> computeGraph(graph_analysis, m.formalArgs.toSet.concat(m.formalReturns.toSet), m.bodyOrAssumeFalse)) + }) + + val endTimeGraphs = System.currentTimeMillis() + val totalTimeGraphs = endTimeGraphs - beginTimeGraphs + println("Time for Graph analysis: " + totalTimeGraphs + "ms") + println("--------------------------------------------------------------------------") + /* + val beginTimeGraphs = System.currentTimeMillis() + val graph_analysis: VarAnalysisGraph = VarAnalysisGraph(prog, reportError) + val (graph: Graph[LocalVarDecl,DefaultEdge],_) = computeGraph(graph_analysis, vars,blk,prog, reportError) + val endTimeGraphs = System.currentTimeMillis() + val totalTimeGraphs = endTimeGraphs - beginTimeGraphs + + println("Time for Graph analysis: " + totalTimeGraphs + "ms") + println("--------------------------------------------------------------------------") + + */ + + + /** compare for each variable */ + graphForMethods.foreach(mg => { + val methodname = mg._1 + val graph = mg._2 + + val set = setForMethods(methodname) + + prog.findMethod(methodname).formalArgs.foreach(arg => { + val out_edges = graph.outgoingEdgesOf(graph_analysis.createInitialVertex(arg)).asScala.toSet + + var graph_vars: Set[LocalVarDecl] = Set() + out_edges.foreach(e => { + graph_vars += graph.getEdgeTarget(e) + }) + + val set_vars: Set[LocalVarDecl] = set(arg) + + if ((graph_vars - arg).equals(set_vars - arg)) { + //println("SET AND GRAPH OF " + arg + " EQUAL") + } else { + println("SET AND GRAPH OF " + arg + " NOT EQUAL") + println("set: " + set_vars) + println("graph: " + graph_vars) + println(graph_analysis.createDOT(graph)) + println("method:\n" + methodname) + } + }) + }) + /* + vars.foreach(v => { + val out_edges = graph.outgoingEdgesOf(graph_analysis.createInitialVertex(v.asInstanceOf[LocalVarDecl])).asScala.toSet + + var graph_vars: Set[LocalVarDecl] = Set() + out_edges.foreach(e => { + graph_vars += graph.getEdgeTarget(e) + }) + + val set_vars: Set[LocalVarDecl] = vToSet(v.asInstanceOf[LocalVarDecl]) + + if ((graph_vars - v.asInstanceOf[LocalVarDecl]).equals(set_vars - v.asInstanceOf[LocalVarDecl])) { + println("SET AND GRAPH OF " + v + " EQUAL") + } else { + println("SET AND GRAPH OF " + v + " NOT EQUAL") + println("set: " + set_vars) + println("graph: " + graph_vars) + println(graph_analysis.createDOT(graph)) + println("method:\n" + m) + } + + }) + */ + } +} diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisGraph.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisGraph.scala new file mode 100644 index 000000000..68b6a2224 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisGraph.scala @@ -0,0 +1,692 @@ +// 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 org.jgrapht.Graph +import org.jgrapht.graph.{AbstractBaseGraph, DefaultDirectedGraph, DefaultEdge} +import viper.silver.ast.{AccessPredicate, Apply, Assert, Assume, BinExp, CurrentPerm, DomainFuncApp, Exhale, Exp, FieldAccess, FieldAssign, Fold, ForPerm, FuncApp, Goto, If, Inhale, Int, Label, LocalVar, LocalVarAssign, LocalVarDecl, MethodCall, Package, Program, Ref, Seqn, Stmt, UnExp, Unfold, While} +import viper.silver.plugin.standard.reasoning.{ExistentialElim, FlowAnnotation, Heap, OldCall, UniversalIntro, Var} +import viper.silver.verifier.{AbstractError, ConsistencyError} + +import java.io.StringWriter +import scala.jdk.CollectionConverters._ + + +case class VarAnalysisGraph(prog: Program, + reportErrorWithMsg: AbstractError => Unit) { + + val prefix: String = ".init_" + + val heap_vertex: LocalVarDecl = LocalVarDecl(".heap", Ref)() + + + /** execute the information flow analysis with graphs. + * When executed on the universal introduction statement the tainted variables are simply the quantified variables */ + def executeTaintedGraphAnalysis(tainted: Set[LocalVarDecl], blk: Seqn, allVertices: Map[LocalVarDecl, LocalVarDecl], u: UniversalIntro): Unit = { + + val graph = compute_graph(blk, allVertices) + + var noEdges: Boolean = true + var badEdges = Set[DefaultEdge]() + tainted.foreach(v => { + if (graph.edgesOf(createInitialVertex(v)).size() > 1) { + badEdges = badEdges ++ graph.edgesOf(createInitialVertex(v)).asScala.toSet[DefaultEdge] + noEdges = false + } + }) + if (!noEdges) { + var tainted_vars: Set[LocalVarDecl] = Set() + badEdges.foreach(e => { + val target = graph.getEdgeTarget(e) + if (!tainted.contains(target)) { + tainted_vars = tainted_vars + graph.getEdgeTarget(e) + } + }) + val tainted_vars_sorted: List[LocalVarDecl] = tainted_vars.toList.sortWith(_.name < _.name) + val problem_vars: String = tainted_vars_sorted.mkString(", ") + reportErrorWithMsg(ConsistencyError("Universal introduction variable might have been assigned to variable " + problem_vars + ", defined outside of the block", u.pos)) + } + } + + + /** + * Creates the Vertex that represents the initial value of the variable before the statement is executed + * @param variable Variable for which we want to create the Vertex which represents the initial value of the variable + * @return a LocalVariableDeclaration + */ + def createInitialVertex(variable:LocalVarDecl): LocalVarDecl = { + LocalVarDecl(prefix + variable.name, variable.typ)(variable.pos) + } + + /** + * creates a graph with no edges and only the vertices + * @param vertices represent the variables that are in scope + * @return an graph with only vertices + */ + def createEmptyGraph(vertices: Map[LocalVarDecl,LocalVarDecl]): Graph[LocalVarDecl, DefaultEdge] = { + val graph: Graph[LocalVarDecl,DefaultEdge] = new DefaultDirectedGraph[LocalVarDecl,DefaultEdge](classOf[DefaultEdge]) + for ((v,v_init)<-vertices) { + graph.addVertex(v_init) + graph.addVertex(v) + } + graph + } + + + /** + * create a Graph that contains all the vertices with an edge from edge vertex representing the initial value of the variable to the 'end'-value of the variable + * @param vertices represent the variables that are in scope + * @return an identity graph + */ + private def createIdentityGraph(vertices: Map[LocalVarDecl,LocalVarDecl]): Graph[LocalVarDecl, DefaultEdge] = { + val graph: Graph[LocalVarDecl, DefaultEdge] = createEmptyGraph(vertices) + for ((v,v_init)<-vertices) { + graph.addEdge(v_init, v) + } + graph + } + + /** + * add Edges from the vertices representing the initial value to the vertices representing its 'end'-values if they have no incoming edge yet + * @param graph existing graph + * @param vertices the vertices representing variables which should be checked + * @return graph + */ + private def addIdentityEdges(graph: Graph[LocalVarDecl,DefaultEdge], vertices:Map[LocalVarDecl,LocalVarDecl]): Graph[LocalVarDecl, DefaultEdge] = { + for ((v,v_init)<-vertices) { + if (graph.incomingEdgesOf(v).isEmpty) { + graph.addEdge(v_init, v, new DefaultEdge) + } + } + graph + } + + /** + * for debugging purposes + * @param graph graph that should be translated to DOT-language + * @return String that is the graph in DOT-language + * + */ + def createDOT(graph: Graph[LocalVarDecl, DefaultEdge]): String = { + val writer: StringWriter = new StringWriter() + writer.write("strict digraph G {\n") + graph.vertexSet().forEach(v => { + writer.write(" " + v.name.replace(".","") + ";\n") + }) + graph.edgeSet().forEach(e => { + writer.write(" " + graph.getEdgeSource(e).name.replace(".","") + " -> " + graph.getEdgeTarget(e).name.replace(".","") + ";\n") + }) + writer.write("}\n") + writer.toString + } + + /** + * returns all the variables inside an expression + * @param graph existing graph + * @param exp expressions from which all variables should be returned + * @return set of Variable declarations + */ + private def getVarsFromExpr(graph: Graph[LocalVarDecl, DefaultEdge], exp: Exp): Set[LocalVarDecl] = { + val vars: Set[LocalVarDecl] = Set() + exp match { + case l@LocalVar(_, _) => + var l_decl: LocalVarDecl = LocalVarDecl("", Int)() + graph.vertexSet().forEach(v => if (v.name == l.name) { + l_decl = v + }) + if (l_decl.name.isEmpty) { + l_decl = LocalVarDecl(l.name, l.typ)() + } + vars + l_decl + + case BinExp(exp1, exp2) => + getVarsFromExpr(graph, exp1) ++ getVarsFromExpr(graph, exp2) + + case UnExp(exp) => + getVarsFromExpr(graph, exp) + + case FuncApp(_, exps) => + var allVars = vars + if (!vars.contains(heap_vertex)) { + allVars += heap_vertex + } + exps.foreach(e => { + val exp_vars = getVarsFromExpr(graph, e) + exp_vars.foreach(v => { + if (v.typ != Ref) { + allVars += v + } + }) + }) + allVars + + case DomainFuncApp(_, exps, _) => + var allVars = vars + exps.foreach(e => { + val exp_vars = getVarsFromExpr(graph, e) + exp_vars.foreach(v => { + allVars += v + }) + }) + allVars + + case _: ForPerm | _: CurrentPerm => + if (!vars.contains(heap_vertex)) { + vars + heap_vertex + } else { + vars + } + + case FieldAccess(v, _) => + val allVars = vars ++ getVarsFromExpr(graph,v) + if(!allVars.contains(heap_vertex)) + allVars + heap_vertex + else + allVars + + case AccessPredicate(access, _) => + /** Should only be the case in e.g.an inhale or an exhale statement */ + var allVars = vars + val access_vars = getVarsFromExpr(graph, access) + access_vars.foreach(v => { + allVars += v + }) + allVars + + case _ => Set() + } + } + + /** + * returns a shallow copy of graph instance, neither Vertices nor Edges are cloned + * @param graph graph that should be copied. + * @return copied graph + */ + def copyGraph(graph: Graph[LocalVarDecl, DefaultEdge]): Graph[LocalVarDecl, DefaultEdge] = { + graph.asInstanceOf[AbstractBaseGraph[LocalVarDecl, DefaultEdge]].clone().asInstanceOf[DefaultDirectedGraph[LocalVarDecl, DefaultEdge]] + } + + /** + * takes two graphs and returns a new graph containing the union of the edges of both input graphs. Both graphs should contain the same vertices! + * @param graph1 + * @param graph2 + * @return graph + */ + private def unionEdges(graph1: Graph[LocalVarDecl, DefaultEdge], graph2: Graph[LocalVarDecl, DefaultEdge]): Graph[LocalVarDecl,DefaultEdge] = { + val new_graph = copyGraph(graph1) + if (graph1.vertexSet().equals(graph2.vertexSet())) { + for (e2: DefaultEdge <- graph2.edgeSet().asScala.toSet) { + if (!new_graph.containsEdge(e2)) { + val src = graph2.getEdgeSource(e2) + val trgt = graph2.getEdgeTarget(e2) + new_graph.addEdge(src, trgt, e2) + } + } + } else { + throw new AssertionError(s"cannot union edges since graphs have different vertex sets") + } + new_graph + } + + /** + * merges two graphs. Meaning: we create a new graph with all the init vertices from graph one and all 'end' vertices from graph two. + * We assume that all 'end' vertices from graph1 can be matched with an init vertex from graph2. E.g. v = .init_v + * We then add an edge from a to b if there is a path from a to b. + * @param graph1 + * @param graph2 + * @param vertices + * @return merged graph + */ + private def mergeGraphs(graph1: Graph[LocalVarDecl, DefaultEdge], graph2: Graph[LocalVarDecl, DefaultEdge], vertices: Map[LocalVarDecl, LocalVarDecl]): Graph[LocalVarDecl,DefaultEdge] = { + val new_graph = createEmptyGraph(vertices) + for (e1: DefaultEdge <- graph1.edgeSet().asScala.toSet) { + val src = graph1.getEdgeSource(e1) + val trgt = graph1.getEdgeTarget(e1) + val init_trgt = vertices.get(trgt) + if (init_trgt.isDefined) { + for (e2: DefaultEdge <- graph2.outgoingEdgesOf(init_trgt.get).asScala.toSet) { + new_graph.addEdge(src, graph2.getEdgeTarget(e2), new DefaultEdge) + } + } else { + throw new AssertionError(s"Vertex not found for declaration $trgt") + } + } + new_graph + } + + + /** creates a graph based on the statement + * edge is influenced by relation: source influences target + * vertices are all variables in scope*/ + def compute_graph(stmt: Stmt, vertices: Map[LocalVarDecl,LocalVarDecl]): Graph[LocalVarDecl,DefaultEdge] = { + stmt match { + case Seqn(ss, scopedSeqnDeclarations) => + var allVertices: Map[LocalVarDecl,LocalVarDecl] = vertices + for (d <- scopedSeqnDeclarations) { + d match { + case decl: LocalVarDecl => + val d_init = createInitialVertex(decl) + allVertices += (decl -> d_init) + } + } + var new_graph: Graph[LocalVarDecl, DefaultEdge] = createIdentityGraph(allVertices) + for (s <- ss) { + val comp_graph = compute_graph(s, allVertices) + new_graph = mergeGraphs(new_graph, comp_graph, allVertices) + } + + val final_graph: Graph[LocalVarDecl, DefaultEdge] = createEmptyGraph(vertices) + new_graph.edgeSet().forEach(e => { + val source: LocalVarDecl = new_graph.getEdgeSource(e) + val target: LocalVarDecl = new_graph.getEdgeTarget(e) + if (final_graph.containsVertex(source) && final_graph.containsVertex(target)) { + final_graph.addEdge(source, target, e) + } + }) + final_graph + + case If(cond, thn, els) => + val id_graph = createIdentityGraph(vertices) + val expr_vars = getVarsFromExpr(id_graph, cond) + val cond_graph = copyGraph(id_graph) + val thn_graph = compute_graph(thn, vertices) + val els_graph = compute_graph(els, vertices) + val writtenToThn = getModifiedVars(vertices, thn).getOrElse(Set.empty) + val writtenToEls = getModifiedVars(vertices, els).getOrElse(Set.empty) + val allWrittenTo = writtenToThn ++ writtenToEls + for (w <- allWrittenTo) { + if (cond_graph.containsVertex(w)) { + for (v <- expr_vars) { + val v_init = vertices(v) + cond_graph.addEdge(v_init, w, new DefaultEdge) + } + } + } + writtenToThn.intersect(writtenToEls).foreach(v => { + cond_graph.removeEdge(vertices(v),v) + }) + val thn_els_graph = unionEdges(thn_graph, els_graph) + unionEdges(cond_graph, thn_els_graph) + + case While(cond, _, body) => + /** analyse one iteration of the while loop */ + val one_iter_graph: Graph[LocalVarDecl, DefaultEdge] = compute_graph(If(cond, body, Seqn(Seq(), Seq())(body.pos))(body.pos), vertices) + var edges_equal: Boolean = false + var merge_graph = copyGraph(one_iter_graph) + while(!edges_equal) { + val last_iter_graph = copyGraph(merge_graph) + merge_graph = mergeGraphs(merge_graph, one_iter_graph, vertices) + val equal_size: Boolean = last_iter_graph.edgeSet().size().equals(merge_graph.edgeSet().size()) + if (equal_size && last_iter_graph.vertexSet().equals(merge_graph.vertexSet())) { + for (e1: DefaultEdge <- last_iter_graph.edgeSet().asScala.toSet) { + if (merge_graph.getEdge(last_iter_graph.getEdgeSource(e1), last_iter_graph.getEdgeTarget(e1)) == null) { + edges_equal = false + } else { + edges_equal = true + } + } + } + } + merge_graph + + case LocalVarAssign(lhs,rhs) => + var new_graph: Graph[LocalVarDecl,DefaultEdge] = createEmptyGraph(vertices) + val rhs_vars = getVarsFromExpr(new_graph, rhs) + val lhs_decl: LocalVarDecl = LocalVarDecl(lhs.name,lhs.typ)(lhs.pos) + for (v <- rhs_vars) { + /** if the variable on the right hand side is a field access */ + if (v.equals(heap_vertex)) { + val heap_init = vertices(heap_vertex) + new_graph.addEdge(heap_init, lhs_decl, new DefaultEdge) + } else { + val v_init = vertices(v) + new_graph.addEdge(v_init, lhs_decl, new DefaultEdge) + } + } + /** Since variables that are not assigned to should have an edge from their initial value to their 'end'-value */ + val vert_wout_lhs = vertices - lhs_decl + new_graph = addIdentityEdges(new_graph, vert_wout_lhs) + new_graph + + case Inhale(exp) => + val id_graph = createIdentityGraph(vertices) + expInfluencesAllVertices(exp, id_graph, vertices) + + /** same as inhale */ + case Assume(exp) => + val id_graph = createIdentityGraph(vertices) + expInfluencesAllVertices(exp, id_graph, vertices) + + case Exhale(exp) => + val id_graph = createIdentityGraph(vertices) + if (exp.isPure) { + id_graph + } else { + val exhale_vars = getVarsFromExpr(id_graph, exp) + exhale_vars.foreach(v => { + if (v.typ == Ref) { + val init_v = createInitialVertex(v) + id_graph.addEdge(init_v, heap_vertex, new DefaultEdge) + } + }) + id_graph + } + + case Assert(_) => createIdentityGraph(vertices) + + case Label(_, _) => createIdentityGraph(vertices) + + case MethodCall(methodName, args, targets) => + val met = prog.findMethod(methodName) + val methodcall_graph = createEmptyGraph(vertices) + createInfluencedByGraph(methodcall_graph,vertices,args,targets,met.formalArgs, met.formalReturns,met.posts) + + case FieldAssign(_, rhs) => + val id_graph = createIdentityGraph(vertices) + val rhs_vars = getVarsFromExpr(id_graph, rhs) + rhs_vars.foreach(v => { + /** Edge from .init_heap to heap does not have to be added since it exists anyways */ + if (v.equals(heap_vertex)) { + id_graph + } else { + val v_init = createInitialVertex(v) + id_graph.addEdge(v_init, heap_vertex, new DefaultEdge) + } + }) + id_graph + + /** TODO: technically not implemented correctly */ + case ExistentialElim(_,_,_) => createIdentityGraph(vertices) + + case UniversalIntro(varList,_,_,_,blk) => + val new_vertices: Map[LocalVarDecl, LocalVarDecl] = vertices ++ varList.map(v => (v -> createInitialVertex(v))) + val new_graph = compute_graph(blk,new_vertices) + varList.foreach(v => { + new_graph.removeVertex(v) + new_graph.removeVertex(new_vertices(v)) + }) + new_graph + + case Fold(acc) => + val id_graph = createIdentityGraph(vertices) + val vars = getVarsFromExpr(id_graph, acc) + vars.foreach(v => { + id_graph.addEdge(vertices(v), heap_vertex, new DefaultEdge) + }) + id_graph + + case Unfold(acc) => + val id_graph = createIdentityGraph(vertices) + val vars = getVarsFromExpr(id_graph, acc) + vars.foreach(v => { + id_graph.addEdge(vertices(v), heap_vertex, new DefaultEdge) + }) + id_graph + + case Apply(exp) => + val id_graph = createIdentityGraph(vertices) + val vars = getVarsFromExpr(id_graph, exp) + vars.foreach(v => { + id_graph.addEdge(vertices(v), heap_vertex, new DefaultEdge) + }) + id_graph + + case Package(wand, _) => + val id_graph = createIdentityGraph(vertices) + val vars = getVarsFromExpr(id_graph, wand) + vars.foreach(v => { + id_graph.addEdge(vertices(v), heap_vertex, new DefaultEdge) + }) + id_graph + + case g: Goto => + reportErrorWithMsg(ConsistencyError(s"$g is an undefined statement for the modular information flow analysis", g.pos)) + createEmptyGraph(vertices) + + case OldCall(methodName, args, targets, _) => + val met = prog.findMethod(methodName) + val methodcall_graph: Graph[LocalVarDecl, DefaultEdge] = createEmptyGraph(vertices) + + createInfluencedByGraph(methodcall_graph, vertices, args, targets, met.formalArgs, met.formalReturns, met.posts) + + case _ => + reportErrorWithMsg(ConsistencyError(s"$stmt is an undefined statement for the modular information flow analysis", stmt.pos)) + createEmptyGraph(vertices) + } + } + + /** + * creates an edge between every variable in the expression to every variable that is in scope and returns resulting graph + */ + private def expInfluencesAllVertices(exp:Exp, graph: Graph[LocalVarDecl, DefaultEdge], vertices: Map[LocalVarDecl,LocalVarDecl]) : Graph[LocalVarDecl, DefaultEdge] = { + val id_graph = createIdentityGraph(vertices) + val vars = getVarsFromExpr(graph, exp) + vars.foreach(v => { + val init_v = vertices(v) + vertices.keySet.foreach(k => { + id_graph.addEdge(init_v, k, new DefaultEdge) + }) + }) + id_graph + } + + /** creates graph for methodcall and oldcall. 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 createInfluencedByGraph(graph: Graph[LocalVarDecl, DefaultEdge], vertices: Map[LocalVarDecl,LocalVarDecl], arg_names: Seq[Exp], ret_names: Seq[LocalVar], method_arg_names: Seq[LocalVarDecl], method_ret_names: Seq[LocalVarDecl], posts: Seq[Exp]): Graph[LocalVarDecl, DefaultEdge] = { + /** set of all target variables that have not been included in the influenced by expression up until now */ + var retSet: Set[LocalVarDecl] = method_ret_names.toSet + heap_vertex + + var methodcall_graph = copyGraph(graph) + val method_arg_names_incl_heap = method_arg_names ++ Seq(heap_vertex) + + /** create .arg_ declaration for each argument */ + var method_args: Map[LocalVarDecl, LocalVarDecl] = Map.empty + var method_arg_counter: Int = 0 + method_arg_names_incl_heap.foreach(method_arg => { + method_args += (method_arg -> LocalVarDecl(".arg" + method_arg_counter, method_arg.typ)(method_arg.pos)) + method_arg_counter += 1 + }) + + /** create .ret_ declaration for each return variable */ + var method_rets: Map[LocalVarDecl, LocalVarDecl] = Map() + var method_ret_counter: Int = 0 + retSet.foreach(method_ret => { + method_rets += (method_ret -> LocalVarDecl(".ret" + method_ret_counter, method_ret.typ)(method_ret.pos)) + method_ret_counter += 1 + }) + + /** contains all variables that are passed to the method */ + var total_arg_decls: Set[LocalVarDecl] = Set(heap_vertex) + + /** add edges from method arguments to .arg variables */ + (arg_names zip method_arg_names).foreach(arg => { + /** extract all variables in expressions that are added to the method */ + val arg_decls: Set[LocalVarDecl] = getVarsFromExpr(graph, arg._1) + total_arg_decls ++= arg_decls + arg_decls.foreach(arg_decl => { + if (!methodcall_graph.containsVertex(vertices(arg_decl))) { + methodcall_graph.addVertex(vertices(arg_decl)) + } + if (!methodcall_graph.containsVertex(method_args(arg._2))) { + methodcall_graph.addVertex(method_args(arg._2)) + } + /** add edge from .init variable to .arg variable */ + methodcall_graph.addEdge(vertices(arg_decl), method_args(arg._2)) + }) + }) + + /** add heap and corresponding .arg variable as method argument */ + if(!methodcall_graph.containsVertex(heap_vertex)) { + methodcall_graph.addVertex(vertices(heap_vertex)) + } + if(!methodcall_graph.containsVertex(method_args(heap_vertex))) { + methodcall_graph.addVertex(method_args(heap_vertex)) + } + methodcall_graph.addEdge(vertices(heap_vertex),method_args(heap_vertex)) + + + /** need to add the edges from the influenced by expression */ + posts.foreach { + case FlowAnnotation(returned, arguments) => + + /** returned has to be instance of LocalVar */ + val returned_var: LocalVar = returned match { + case v: Var => v.decl + case _: Heap => heap_vertex.localVar + } + /** create LocalVarDecl such that it can be added in the graph */ + val return_decl = LocalVarDecl(returned_var.name, returned_var.typ)(returned_var.pos) + retSet -= return_decl + + if (!methodcall_graph.containsVertex(method_rets(return_decl))) { + methodcall_graph.addVertex(method_rets(return_decl)) + } + + arguments.foreach(argument => { + /** argument has to be instance of LocalVar */ + val argument_var: LocalVar = argument match { + case v: Var => v.decl + case _: Heap => heap_vertex.localVar + } + val argument_decl = LocalVarDecl(argument_var.name, argument_var.typ)(argument_var.pos) + /** get corresponding .arg variable and add edge from .arg to .ret vertex */ + val prov_decl = method_args(argument_decl) + methodcall_graph.addEdge(prov_decl, method_rets(return_decl), new DefaultEdge) + }) + + case _ => + } + + /** now need to add to graph the edges from the method return variables to the target variables */ + val targets_decl: Seq[LocalVarDecl] = ret_names.map(t => { + graph.vertexSet().asScala.filter(lvd => lvd.name == t.name).head + }) ++ Seq(heap_vertex) + ((method_ret_names ++ Seq(heap_vertex)) zip targets_decl).foreach(ret => { + if (!methodcall_graph.containsVertex(ret._2)) { + methodcall_graph.addVertex(ret._2) + } + if (!methodcall_graph.containsVertex(method_rets(ret._1))) { + methodcall_graph.addVertex(method_rets(ret._1)) + } + /** add edge from .ret variable to target variable */ + methodcall_graph.addEdge(method_rets(ret._1), ret._2) + }) + + + /** add edges from all method argument to each return variable that wasn't mentioned in the influenced by statement */ + retSet.foreach(r => { + method_arg_names_incl_heap.foreach(a => { + if (!methodcall_graph.containsVertex(method_args(a))) { + methodcall_graph.addVertex(method_args(a)) + } + if (!methodcall_graph.containsVertex(method_rets(r))) { + methodcall_graph.addVertex(method_rets(r)) + } + methodcall_graph.addEdge(method_args(a), method_rets(r), new DefaultEdge) + }) + }) + + + var copy_arg_graph = copyGraph(methodcall_graph) + + /** remove edge from .ret_ vertex to the final vertex */ + for (elem <- targets_decl) { + /** get all edges from target variables to .ret variables */ + copy_arg_graph.incomingEdgesOf(elem).forEach(inc_edge => { + //should only be one edge + val ret_vert = methodcall_graph.getEdgeSource(inc_edge) + /** get edges from .ret variable to .arg variable */ + copy_arg_graph.incomingEdgesOf(ret_vert).forEach(ret_inc_e => { + val arg_vert = methodcall_graph.getEdgeSource(ret_inc_e) + /** add edge from .arg variable to target variable */ + methodcall_graph.addEdge(arg_vert, elem) + }) + /** remove .ret variables */ + methodcall_graph.removeVertex(ret_vert) + }) + } + + /** remove rest of .ret variable incase no assigment */ + method_rets.values.foreach(ret_vert => { + methodcall_graph.removeVertex(ret_vert) + }) + + + + /** remove edge from the .arg_ to the .init vertex */ + copy_arg_graph = copyGraph(methodcall_graph) + /** go through .init variables */ + for (elem <- total_arg_decls + heap_vertex) { + /** go through all outgoing edges of .init variable */ + copy_arg_graph.outgoingEdgesOf(vertices(elem)).forEach(out_edge => { + /** get the .arg variable that edge leads to */ + val arg_vert = methodcall_graph.getEdgeTarget(out_edge) + /** get edges from .arg variable to the target variable */ + copy_arg_graph.outgoingEdgesOf(arg_vert).forEach(arg_out_e => { + val final_vert = methodcall_graph.getEdgeTarget(arg_out_e) + /** create edge from .init variable to target variable */ + methodcall_graph.addEdge(vertices(elem), final_vert) + }) + methodcall_graph.removeVertex(arg_vert) + }) + } + + /** Since variables that are not assigned to should have an edge from their initial value to their 'end'-value */ + val vert_wout_lhs = vertices.removedAll(targets_decl) + methodcall_graph = addIdentityEdges(methodcall_graph, vert_wout_lhs) + methodcall_graph + } + + + /** + * get the variables that were modified by the statement stmt + */ + def getModifiedVars(vertices: Map[LocalVarDecl,LocalVarDecl], stmt: Stmt): Option[Set[LocalVarDecl]] = { + var output: Option[Set[LocalVarDecl]] = None + stmt match { + case Seqn(ss, _) => + for (s <- ss) { + output match { + case None => output = getModifiedVars(vertices, s) + case Some(v) => output = Some(v ++ getModifiedVars(vertices, s).getOrElse(Set[LocalVarDecl]())) + } + } + output + + case LocalVarAssign(lhs, _) => + var res: Option[Set[LocalVarDecl]] = None + for (vs <- vertices) { + if (vs._1.name == lhs.name) { + res = Some(Set(vs._1)) + } else { + /** This is the case if the variable is in scope in e.g. a then or an else block. */ + res = Some(Set(LocalVarDecl(lhs.name, lhs.typ)(lhs.pos))) + } + } + res + + case If(_, thn, els) => + val writtenThn = getModifiedVars(vertices, thn) + val writtenEls = getModifiedVars(vertices, els) + (writtenThn, writtenEls) match { + case (None, None) => None + case (Some(_), None) => writtenThn + case (None, Some(_)) => writtenEls + case (Some(t), Some(e)) => Some(t ++ e) + } + + case While(_, _, body) => + getModifiedVars(vertices, body) + + case MethodCall(_, _, _) => None + case Inhale(_) => None + case Assume(_) => None + case Label(_, _) => None + case _ => None + } + } +} diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisSet.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisSet.scala new file mode 100644 index 000000000..46d930d66 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisSet.scala @@ -0,0 +1,177 @@ +// 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.{Assume, BinExp, Declaration, Exp, FieldAssign, If, Inhale, Label, LocalVar, LocalVarAssign, LocalVarDecl, MethodCall, Seqn, Stmt, UnExp, While} +import viper.silver.plugin.standard.reasoning.UniversalIntro +import viper.silver.verifier.{AbstractError, ConsistencyError} + +import scala.collection.mutable + +trait VarAnalysisSet { + + def reportErrorWithMsg(error: AbstractError): Unit + + def executeTaintedSetAnalysis(tainted: Set[Declaration], vars_outside_blk: mutable.Set[Declaration], blk: Seqn, u: UniversalIntro, reportError: AbstractError => Unit): Unit = { + /** check whether any additional variables are tainted inside of the block */ + var all_tainted = Set[Declaration]() + all_tainted = get_tainted_vars_stmt(tainted, blk) + + /** remove the variables that were tainted to begin with */ + vars_outside_blk --= mutable.Set(u.transitiveScopedDecls: _*) + + /** check whether any variables were tainted that are declared outside of our block */ + if (vars_outside_blk.intersect(all_tainted).nonEmpty) { + val tainted_vars: Set[Declaration] = all_tainted.intersect(vars_outside_blk) + val problem_vars: String = tainted_vars.mkString(", ") + reportError(ConsistencyError(s"Universal introduction variable might have been assigned to variable $problem_vars, defined outside of the block", u.pos)) + } + } + + /** + * check which arguments are influenced by universal introduction variables and add them to the tainted set. + * @param tainted + * @param stmt + * @return + */ + def get_tainted_vars_stmt(tainted: Set[Declaration], stmt: Stmt): Set[Declaration] = { + var output: Set[Declaration] = tainted + stmt match { + case Seqn(ss, _) => + for (s <- ss) { + output = get_tainted_vars_stmt(output, s) + } + output + + case LocalVarAssign(lhs, rhs) => + if (is_expr_tainted(tainted, rhs)) { + tainted ++ Set(LocalVarDecl(lhs.name, lhs.typ)(stmt.pos)) + } else { + tainted -- Set(LocalVarDecl(lhs.name, lhs.typ)(stmt.pos)) + } + + case If(cond, thn, els) => + if (is_expr_tainted(tainted, cond)) { + val written_vars_thn = writtenTo(thn) + val written_vars_els = writtenTo(els) + Set[Declaration]() ++ written_vars_thn.getOrElse(mutable.Set()) ++ written_vars_els.getOrElse(mutable.Set()) + } else { + get_tainted_vars_stmt(tainted, thn) ++ get_tainted_vars_stmt(tainted, els) + } + + case w@While(cond, _, body) => + val new_tainted = get_tainted_vars_stmt(tainted, If(cond,body,Seqn(Seq(), Seq())(body.pos))(body.pos)) + if (new_tainted.equals(tainted)) { + tainted + } else { + get_tainted_vars_stmt(new_tainted, w) + } + + case m@MethodCall(_, _, _) => + reportErrorWithMsg(ConsistencyError("Might be not allowed method call inside universal introduction block", m.pos)) + tainted + + case i@Inhale(exp) => + if(exp.isPure) { + tainted + } else { + reportErrorWithMsg(ConsistencyError("There might be an impure inhale expression inside universal introduction block", i.pos)) + tainted + } + + case Assume(_) => tainted + + case Label(_, _) => tainted + + /** TODO: Do not allow Heap assignments */ + case f@FieldAssign(_, _) => + reportErrorWithMsg(ConsistencyError("FieldAssign for modular flow analysis with sets", f.pos)) + tainted + + case s@_ => + reportErrorWithMsg(ConsistencyError("undefined statement for modular flow analysis with set", s.pos)) + tainted + } + } + + + /** + * expressions that should be added to tainted (e.g. for instance for inhale statements + * @param tainted + * @param exp + * @return + */ + private def addExprToTainted(tainted: Set[Declaration], exp: Exp) : Set[Declaration] = { + exp match { + case l@LocalVar(_, _) => tainted ++ Set(LocalVarDecl(l.name, l.typ)(exp.pos)) + case BinExp(exp1, exp2) => addExprToTainted(tainted, exp1) ++ addExprToTainted(tainted, exp2) + case UnExp(exp) => addExprToTainted(tainted, exp) + case _ => tainted + } + } + + /** + * check whether expression contains a tainted variable + * @param tainted + * @param exp + * @return + */ + private def is_expr_tainted(tainted:Set[Declaration], exp:Exp) : Boolean = { + exp match { + case l@LocalVar(_, _) => isTainted(LocalVarDecl(l.name, l.typ)(l.pos), tainted) + case BinExp(exp1, exp2) => is_expr_tainted(tainted, exp1) || is_expr_tainted(tainted, exp2) + case UnExp(exp) => is_expr_tainted(tainted, exp) + case _ => false + } + } + + private def isTainted(name:Declaration, tainted:Set[Declaration]): Boolean = { + tainted.contains(name) + } + + /** + * return variables that are assigned new values + * @param stmt + * @return + */ + def writtenTo(stmt: Stmt): Option[Set[LocalVarDecl]] = { + var output: Option[Set[LocalVarDecl]] = None + stmt match { + case Seqn(ss, _) => + for (s <- ss) { + output match { + case None => output = writtenTo(s) + case Some(v) => output = Some(v ++ writtenTo(s).getOrElse(Set[LocalVarDecl]())) + } + } + output + + case LocalVarAssign(lhs, _) => + val lhs_var = LocalVarDecl(lhs.name, lhs.typ)(lhs.pos) + Some(Set(lhs_var)) + + case If(_, thn, els) => + val writtenThn = writtenTo(thn) + val writtenEls = writtenTo(els) + (writtenThn, writtenEls) match { + case (None,None) => None + case (Some(_), None) => writtenThn + case (None, Some(_)) => writtenEls + case (Some(t), Some(e)) => Some(t++e) + } + + case While(_, _, body) => writtenTo(body) + + /** TODO */ + case MethodCall(_, _, _) => None + case Inhale(_) => None + case Assume(_) => None + case Label(_, _) => None + case _ => None + } + } +} 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.vpr b/src/test/resources/reasoning/existential_elim.vpr new file mode 100644 index 000000000..25e2ddeae --- /dev/null +++ b/src/test/resources/reasoning/existential_elim.vpr @@ -0,0 +1,34 @@ +// 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 +} + + +field f: Int + +method ex2() +{ + //:: ExpectedOutput(typechecker.error) + obtain x: Ref where {x.f} acc(x.f) +} + +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 +} 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.vpr b/src/test/resources/reasoning/old_call.vpr new file mode 100644 index 000000000..7ce7389d2 --- /dev/null +++ b/src/test/resources/reasoning/old_call.vpr @@ -0,0 +1,15 @@ +// 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 + x := oldCall[l](lemma()) + //:: ExpectedOutput(typechecker.error) + x := 42 + oldCall[l](lemma()) +} + +method lemma() returns (x: Int) +isLemma 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= -1) { + g := x + } else { + w := 4 + } + } +} + + + +method mWhileOK() +{ + var z: Int := 0 + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + 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() +{ + var z: Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + var y: Int := 0 + var x2: Int := 0 + var x1: Int := 0 + + while(y<100) { // will only be tainted after the 5th? iteration + 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() +{ + var z: Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + var y: Int := x + var x2: Int := 0 + var x1: Int := 0 + + while(y<100) { + z := x2 + x2 := x1 + y := y+1 + } + } +} + + + + +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 + } +} + +method mFieldAssignNOK2(y:Ref) +{ + var w: Int + //:: ExpectedOutput(consistency.error) + prove forall x: Int {P(x)} assuming P(x) implies Q(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 := y.f + } +} + + +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) + } +} + + +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 := 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 := func1(x) + } +} + + + +method example1(x:Int, y:Int) returns (res: Int) +influenced res by {x, y} +{ + res := x-y +} + +method mMethodCallNOK1() +{ + var z: Int + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + z := example1(x,x) + } +} + +//code without influenced by statement +method example2(x:Int, y:Int) returns (res: Int) +{ + res := 0 +} + +method mMethodCallNOK2() +{ + var z: Int + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + 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) { + var y:Int := 3 + z := example3(y,y) + } +} + +//method with several return values +method exampleMult(a0:Int, a1:Int) returns (r0:Int, r1:Int) +influenced r0 by {a0, a1} +influenced r1 by {a0} +{ + r0 := a0-a1 + r1 := a0 +} + +method mMethodCallNOK3() +{ + var z: Int + var w: Int + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + var v: Int := 3 + z,w := exampleMult(v,x) + } +} + + +method exampleIncomplete(b:Bool,c:Int) returns (z:Int, w:Int) +influenced w by {b} +{ + z := 3 + if (b) { + var y: Int := 2 + w := y + 1 + } +} + +method mMethodCallOK2() +{ + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + var y:Int + var v:Int + var bool:Bool := true + var count: Int := 16 + y,v := exampleIncomplete(bool,count) + } +} + +method exampleHeap(b:Int) returns (c:Int) +influenced heap by {heap} +influenced c by {} +{ + c := 3 +} + + +method mMethodCallOK3() +{ + var z: Int + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + z := exampleHeap(x) + } +} + + +method exampleincorrect(b:Bool,c:Int) returns (z:Int, w:Int) +//:: ExpectedOutput(consistency.error) +influenced w by {} +{ + z := 3 + if (b) { + var y: Int := 2 + w := y + 1 + } +} + +method exampleOverapprox(b:Bool,c:Int) returns (z:Int, w:Int) +influenced w by {b,c} +{ + z := 3 + if (b) { + var y: Int := 2 + w := y + 1 + } +} + + + + +method exampleHeapArg2(b:Ref) returns (c:Int) +requires acc(b.f) +influenced heap by { heap } +influenced c by { heap , b } +{ + c := b.f +} + +method exampleHeapArg3(b:Ref) returns (c:Int) +requires acc(b.f) +influenced heap by { b, heap } +influenced c by { b, heap } +{ + c := b.f +} + +method exampleHeapArg4(b:Ref) returns (c:Int) +requires acc(b.f) +influenced heap by { heap, b } +influenced c by { heap, b } +{ + c := b.f +} + +method exampleWrongInfluenced(a:Int) returns (c:Int) +//:: ExpectedOutput(consistency.error) +influenced c by {c} +{ + c := 0 +} + +//:: ExpectedOutput(consistency.error) +method l1() +isLemma +{ + var z:Int := 3 +} + +method l2() +decreases +isLemma +{ + var x:Int + //:: ExpectedOutput(consistency.error) + inhale(x == 0) +} + +//:: ExpectedOutput(consistency.error) +method l3() +isLemma +decreases * +{ + var x:Int := 0 + while (x>0) { + x := x+1 + } +} + +method l4() +isLemma +decreases +{ + var t: Int := 0 +} + +predicate foo(xs:Ref) +{ + acc(xs.f) +} + +method mFold() +{ + var z: Ref + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + assume acc(z.f) + fold foo(z) + } +} + +method mFoldNOK() +{ + var z: Ref + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + z.f := x + assume acc(z.f) + fold foo(z) + } +} + +method mOldCallOK() +{ + label l + oldCall[l](l3()) +} + +method mOldCallNOK() +{ + var x: Int := 0 + label l + x := 2 + //:: ExpectedOutput(consistency.error) + oldCall[l](exampleHeap(x)) +} + + + +method callLemma(x:Int) returns (y:Int, w:Int) + +isLemma +decreases +requires x > 0 +ensures y + w + x > 7 +ensures y == 3 +{ + y := 3 + w := 4 +} + +method mOldCallOK1() +{ + var x: Int := 5 + label l + var z: Int + var a: Int + z,a := oldCall[l](callLemma(x + 5)) +} + + +method exProjDesc() +{ + var k: Int + //:: ExpectedOutput(consistency.error) + prove forall x: Int assuming true implies x==k { + k := x + } +} + + +method mWhileCheck() +{ + var c:Bool + var e:Int + var d:Int + //:: ExpectedOutput(consistency.error) + prove forall a:Int {P(a)} assuming P(a) implies Q(a) { + while (c) + { + d:=e + e:=a + } + } +} + + +method m(a:Int, b:Int) +returns (d:Int) +influenced d by {a} +influenced heap by {heap} +{ + d:=a +} + +method m1() +{ + var b:Int + var d:Int + //:: ExpectedOutput(consistency.error) + prove forall a:Int {P(a)} assuming P(a) implies Q(a) { + d:=m(a,b) + } +} + +method mInhaleAccess() +{ + var d:Ref + //:: ExpectedOutput(consistency.error) + prove forall a:Int {P(a)} assuming P(a) implies Q(a) { + inhale acc(d.f) + d.f:=a + } +} + + +method mLiteralAssign() +{ + var d: Int + prove forall x:Int {P(x)} assuming P(x) implies Q(x) + { + d:=x + d:=3 + } +} + +method mUnivIntro() +{ + var d: Int + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) + { + prove forall y:Int {P(y)} assuming P(y) implies Q(y) + { + d:=x + } + } +} + +method dosomething(x: Int) +{ + var y:Int := x +} + +method xmcall() +{ + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + dosomething(x) + } +} diff --git a/src/test/resources/reasoning/test2.vpr b/src/test/resources/reasoning/test2.vpr new file mode 100644 index 000000000..19be7dfb7 --- /dev/null +++ b/src/test/resources/reasoning/test2.vpr @@ -0,0 +1,130 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +field f: Int + +// 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 +} + +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 +} + +// The annotation "influenced heap by {heap}" should be rejected, +// since test5 has no flow-annotation for the heap, thus it should be +// considered as influenced heap by {heap, x, y} +method test5_caller(x: Int, y: Int) returns (a: Int, b: Int) +//:: ExpectedOutput(consistency.error) + influenced heap by {heap} + influenced a by {y, x, heap} + influenced b by {x, heap, 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} + 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) + } +} \ No newline at end of file diff --git a/src/test/resources/reasoning/test3.vpr b/src/test/resources/reasoning/test3.vpr new file mode 100644 index 000000000..e050b8e21 --- /dev/null +++ b/src/test/resources/reasoning/test3.vpr @@ -0,0 +1,350 @@ +// 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 m0() +{ + var z:Int := 0 + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + var y:Int := x+1 + } + if (true) { var y:Int } // this should work -> two separate blocks + // var y:Int := 0 //here duplicate identifier +} +method mIndirect() +{ + var z:Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(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) { + 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) { + 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) { + 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) { + var l :Int := 0 + if (l >= -1) { + l := x + } else { + w := 4 // should be SAFE + } + } +} + +method mWhileCnd() +{ + var z: Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + while(x>5) { + z := z+3 + } + } +} + +method mWhileOK() +{ + var z: Int := 0 + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + 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) { + 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() +{ + var z: Int := 0 + //:: ExpectedOutput(consistency.error) + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + var y: Int := 0 + var x2: Int := 0 + var x1: Int := 0 + + while(y<100) { // will only be tainted after the 5th? iteration + 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) { + var y: Int := x + var x2: Int := 0 + var x1: Int := 0 + + while(y<100) { // will only be tainted after the 5th? iteration + z := x2 + x2 := x1 + y := y+1 + } + } +} + +method mcall() +{ + var y: Int := 0 + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + mWhileOK() + } +} + +method example1(x:Int, y:Int) returns (res: Int) +influenced res by {x, y} +{ + res := x-y +} + +method mMethodCallNOK1() +{ + var z: Int + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + z := example1(x,x) + } +} + +//code without influenced by statement +method example2(x:Int, y:Int) returns (res: Int) +{ + res := 0 +} + +method mMethodCallNOK2() +{ + var z: Int + //:: ExpectedOutput(consistency.error) + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + 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) { + 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) { + 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 mMethodCallOK2() +{ + prove forall x:Int {P(x)} assuming P(x) implies Q(x) { + var y:Int + var v:Int + var bool:Bool := true + var count: Int := 16 + y,v := exampleIncomplete(bool,count) + } +} + + +method mAssume() +{ + var m: Int := 0 + prove forall x: Int {P(x)} assuming P(x) implies Q(x) { + assume(m==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 + } +} + +method mFieldAssignNOK2(y:Ref) +{ + var w: Int + //:: ExpectedOutput(consistency.error) + prove forall x: Int {P(x)} assuming P(x) implies Q(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 := y.f + } +} + + +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 := 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 := func1(x) + } +} diff --git a/src/test/resources/reasoning/universal_intro.vpr b/src/test/resources/reasoning/universal_intro.vpr new file mode 100644 index 000000000..88e288b88 --- /dev/null +++ b/src/test/resources/reasoning/universal_intro.vpr @@ -0,0 +1,53 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +function greaterthanzero(x:Int) :Bool +{ + x > 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/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) }