From f8be99909b05e460a60d3300bc7d2f8822d748f4 Mon Sep 17 00:00:00 2001 From: Thibault Date: Fri, 9 Jul 2021 00:13:16 +0200 Subject: [PATCH 1/4] First version with negative permission treated as not well-defined --- .../viper/carbon/modules/InhaleModule.scala | 3 +- .../modules/components/InhaleComponent.scala | 3 +- .../modules/impls/DefaultExpModule.scala | 2 +- .../modules/impls/DefaultFuncPredModule.scala | 6 ++-- .../modules/impls/DefaultHeapModule.scala | 3 +- .../modules/impls/DefaultInhaleModule.scala | 23 ++++++++------- .../modules/impls/DefaultLoopModule.scala | 6 ++-- .../modules/impls/DefaultStmtModule.scala | 3 +- .../modules/impls/DefaultWandModule.scala | 4 +-- .../modules/impls/QuantifiedPermModule.scala | 29 +++++++++++++++---- 10 files changed, 52 insertions(+), 30 deletions(-) diff --git a/src/main/scala/viper/carbon/modules/InhaleModule.scala b/src/main/scala/viper/carbon/modules/InhaleModule.scala index 64e540ef..31045427 100644 --- a/src/main/scala/viper/carbon/modules/InhaleModule.scala +++ b/src/main/scala/viper/carbon/modules/InhaleModule.scala @@ -9,6 +9,7 @@ package viper.carbon.modules import components.{ComponentRegistry, InhaleComponent} import viper.silver.{ast => sil} import viper.carbon.boogie.Stmt +import viper.silver.verifier.PartialVerificationError /** * A module for translating inhale statements. The module takes care of the basic @@ -28,5 +29,5 @@ trait InhaleModule extends Module with InhaleComponent with ComponentRegistry[In * The 'statesStackForPackageStmt' and 'insidePackageStmt' are used when translating statements during packaging a wand. * For more details refer to the general note in 'wandModule'. */ - def inhale(exp: Seq[sil.Exp], statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt + def inhale(exp: Seq[(sil.Exp, PartialVerificationError)], statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt } diff --git a/src/main/scala/viper/carbon/modules/components/InhaleComponent.scala b/src/main/scala/viper/carbon/modules/components/InhaleComponent.scala index 3e92c52a..5f03e7c3 100644 --- a/src/main/scala/viper/carbon/modules/components/InhaleComponent.scala +++ b/src/main/scala/viper/carbon/modules/components/InhaleComponent.scala @@ -7,6 +7,7 @@ package viper.carbon.modules.components import viper.carbon.boogie.Stmt +import viper.silver.verifier.PartialVerificationError import viper.silver.{ast => sil} /** @@ -18,5 +19,5 @@ trait InhaleComponent extends Component { /** * Inhale a single expression. */ - def inhaleExp(exp: sil.Exp): Stmt + def inhaleExp(exp: sil.Exp, error: PartialVerificationError): Stmt } diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala index 6acc9ffe..cd5e6818 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala @@ -533,7 +533,7 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes // case fa@sil.Forall(vars, triggers, expr) => // NOTE: there's no need for a special case for QPs, since these are desugared, introducing conjunctions case _ => checkDefinedness(e, error, duringPackageStmt = duringPackageStmt) ++ - inhale(e, statesStack, duringPackageStmt) + inhale(Seq((e, error)), statesStack, duringPackageStmt) } } diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index d24da40a..928d1131 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -828,7 +828,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { foldInfo = acc val stmt = exhale(Seq((Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), error)), havocHeap = false, statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt) ++ - inhale(acc, statesStackForPackageStmt, insidePackageStmt) + inhale(Seq((acc, error)), statesStackForPackageStmt, insidePackageStmt) val stmtLast = Assume(predicateTrigger(heapModule.currentStateExps, acc.loc)) ++ { val location = acc.loc val predicate = verifier.program.findPredicate(location.predicateName) @@ -873,7 +873,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { } ++ (if(exhaleUnfoldedPredicate) exhale(Seq((acc, error)), havocHeap = false, statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt) - else Nil) ++ inhale(Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt) + else Nil) ++ inhale(Seq((Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), error)), statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt) unfoldInfo = oldUnfoldInfo duringUnfold = oldDuringUnfold duringFold = oldDuringFold @@ -937,7 +937,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { var exhaleTmpStateId = -1 var extraUnfolding = false - override def inhaleExp(e: sil.Exp): Stmt = { + override def inhaleExp(e: sil.Exp, error: PartialVerificationError): Stmt = { e match { case sil.Unfolding(acc, _) => if (duringUnfoldingExtraUnfold) Nil else // execute the unfolding, since this may gain information { diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala index ce831c5c..6d1b07dd 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala @@ -14,6 +14,7 @@ import viper.carbon.boogie._ import viper.carbon.boogie.Implicits._ import viper.carbon.verifier.Verifier import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion +import viper.silver.verifier.PartialVerificationError /** * The default implementation of a [[viper.carbon.modules.HeapModule]]. @@ -739,7 +740,7 @@ class DefaultHeapModule(val verifier: Verifier) else Nil } - override def inhaleExp(e: sil.Exp): Stmt = { + override def inhaleExp(e: sil.Exp, error: PartialVerificationError): Stmt = { e match { case sil.Unfolding(sil.PredicateAccessPredicate(loc, perm), exp) => addPermissionToPMask(loc) diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultInhaleModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultInhaleModule.scala index fbca1c60..8ed33fa6 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultInhaleModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultInhaleModule.scala @@ -11,6 +11,7 @@ import viper.silver.{ast => sil} import viper.carbon.boogie._ import viper.carbon.verifier.Verifier import viper.carbon.boogie.Implicits._ +import viper.silver.verifier.PartialVerificationError /** * The default implementation of a [[viper.carbon.modules.InhaleModule]]. @@ -29,7 +30,7 @@ class DefaultInhaleModule(val verifier: Verifier) extends InhaleModule with Stat register(this) } - override def inhale(exps: Seq[sil.Exp], statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt = { + override def inhale(exps: Seq[(sil.Exp, PartialVerificationError)], statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt = { val current_state = stateModule.state if(insidePackageStmt){ // replace currentState with the correct state in which the inhale occurs during packaging the wand stateModule.replaceState(statesStackForPackageStmt(0).asInstanceOf[StateRep].state) @@ -37,9 +38,9 @@ class DefaultInhaleModule(val verifier: Verifier) extends InhaleModule with Stat val stmt = - (exps map (e => inhaleConnective(e.whenInhaling))) ++ + (exps map (e => inhaleConnective(e._1.whenInhaling, e._2))) ++ MaybeCommentBlock("Free assumptions", - exps map (e => allFreeAssumptions(e))) ++ + exps map (e => allFreeAssumptions(e._1))) ++ assumeGoodState if(insidePackageStmt) { // all the assumption made during packaging a wand (except assumptions about the global state before the package statement) @@ -62,29 +63,29 @@ class DefaultInhaleModule(val verifier: Verifier) extends InhaleModule with Stat * Inhales Viper expression connectives (such as logical and/or) and forwards the * translation of other expressions to the inhale components. */ - private def inhaleConnective(e: sil.Exp): Stmt = { + private def inhaleConnective(e: sil.Exp, error: PartialVerificationError): Stmt = { e match { case sil.And(e1, e2) => - inhaleConnective(e1) :: - inhaleConnective(e2) :: + inhaleConnective(e1, error) :: + inhaleConnective(e2, error) :: Nil case sil.Implies(e1, e2) => - If(translateExp(e1), inhaleConnective(e2), Statements.EmptyStmt) + If(translateExp(e1), inhaleConnective(e2, error), Statements.EmptyStmt) case sil.CondExp(c, e1, e2) => - If(translateExp(c), inhaleConnective(e1), inhaleConnective(e2)) + If(translateExp(c), inhaleConnective(e1, error), inhaleConnective(e2, error)) case sil.Let(declared,boundTo,body) if !body.isPure => { val u = env.makeUniquelyNamed(declared) // choose a fresh binder env.define(u.localVar) Assign(translateLocalVar(u.localVar),translateExp(boundTo)) :: - inhaleConnective(body.replace(declared.localVar, u.localVar)) :: + inhaleConnective(body.replace(declared.localVar, u.localVar), error) :: { env.undefine(u.localVar) Nil } } case _ => - val stmt = components map (_.inhaleExp(e)) + val stmt = components map (_.inhaleExp(e, error)) if (stmt.children.isEmpty) sys.error(s"missing translation for inhaling of $e") val retStmt = (if (containsFunc(e)) Seq(assumeGoodState) else Seq()) ++ stmt ++ (if (e.isPure) Seq() else Seq(assumeGoodState)) @@ -95,7 +96,7 @@ class DefaultInhaleModule(val verifier: Verifier) extends InhaleModule with Stat } } - override def inhaleExp(e: sil.Exp): Stmt = { + override def inhaleExp(e: sil.Exp, error: PartialVerificationError): Stmt = { if (e.isPure) { Assume(translateExp(e)) } else { diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultLoopModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultLoopModule.scala index 843cc98c..0d068c65 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultLoopModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultLoopModule.scala @@ -437,7 +437,7 @@ class DefaultLoopModule(val verifier: Verifier) extends LoopModule with StmtComp MaybeCommentBlock("Check the loop body", NondetIf({ val (freshStateStmt, prevState) = stateModule.freshTempState("loop") val stmts = MaybeComment("Reset state", freshStateStmt ++ stateModule.initBoogieState) ++ - MaybeComment("Inhale invariant", inhale(invs) ++ executeUnfoldings(invs, (inv => errors.Internal(inv)))) ++ + MaybeComment("Inhale invariant", inhale(invs map (x => (x, errors.WhileFailed(x)))) ++ executeUnfoldings(invs, (inv => errors.Internal(inv)))) ++ Comment("Check and assume guard") ++ checkDefinedness(w.cond, errors.WhileFailed(w.cond)) ++ Assume(guard) ++ stateModule.assumeGoodState ++ @@ -450,7 +450,7 @@ class DefaultLoopModule(val verifier: Verifier) extends LoopModule with StmtComp )) ++ MaybeCommentBlock("Inhale loop invariant after loop, and assume guard", Assume(guard.not) ++ stateModule.assumeGoodState ++ - inhale(invs) ++ executeUnfoldings(invs, (inv => errors.Internal(inv))) + inhale(invs map (x => (x, errors.WhileFailed(x)))) ++ executeUnfoldings(invs, (inv => errors.Internal(inv))) ) } @@ -536,7 +536,7 @@ class DefaultLoopModule(val verifier: Verifier) extends LoopModule with StmtComp As long as modules the state at this point refers to the original state, this is fine. */ MaybeComment("Reset state", stateModule.initBoogieState) ++ - MaybeComment("Inhale invariant", inhale(invs) ++ executeUnfoldings(invs, (inv => errors.Internal(inv)))) ++ + MaybeComment("Inhale invariant", inhale(invs map (x => (x, errors.WhileFailed(x)))) ++ executeUnfoldings(invs, (inv => errors.Internal(inv)))) ++ stateModule.assumeGoodState ) ) diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala index 82780220..51c22529 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala @@ -189,7 +189,8 @@ class DefaultStmtModule(val verifier: Verifier) extends StmtModule with SimpleSt MaybeCommentBlock("Exhaling precondition", executeUnfoldings(pres, (pre => errors.PreconditionInCallFalse(mc).withReasonNodeTransformed(renamingArguments))) ++ exhale(pres map (e => (e, errors.PreconditionInCallFalse(mc).withReasonNodeTransformed(renamingArguments))), statesStackForPackageStmt = statesStack, insidePackageStmt = insidePackageStmt)) ++ { stateModule.replaceOldState(preCallState) - val res = MaybeCommentBlock("Inhaling postcondition", inhale(posts, statesStack, insidePackageStmt) ++ + val res = MaybeCommentBlock("Inhaling postcondition", + inhale(posts map (e => (e, errors.PostconditionInCallFalse(mc).withReasonNodeTransformed(renamingArguments))), statesStack, insidePackageStmt) ++ executeUnfoldings(posts, (post => errors.Internal(post).withReasonNodeTransformed(renamingArguments)))) stateModule.replaceOldState(oldState) toUndefine map mainModule.env.undefine diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala index 4b7c0503..289cd3a9 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala @@ -216,7 +216,7 @@ DefaultWandModule(val verifier: Verifier) extends WandModule with StmtComponent val oldOps = OPS currentWand = w - val addWand = inhaleModule.inhale(w, statesStack, inWand) + val addWand = inhaleModule.inhale(Seq((w, error)), statesStack, inWand) val currentState = stateModule.state @@ -692,7 +692,7 @@ case class PackageSetup(hypState: StateRep, usedState: StateRep, initStmt: Stmt) (if(inWand) exchangeAssumesWithBoolean(stateModule.assumeGoodState, OPS.boolVar) else stateModule.assumeGoodState) ++ CommentBlock("check if LHS holds and remove permissions ", exhaleModule.exhale((w.left, error), false, insidePackageStmt = inWand, statesStackForPackageStmt = statesStack)) ++ (if(inWand) exchangeAssumesWithBoolean(stateModule.assumeGoodState, OPS.boolVar) else stateModule.assumeGoodState) ++ - CommentBlock("inhale the RHS of the wand",inhaleModule.inhale(w.right, statesStackForPackageStmt = statesStack, insidePackageStmt = inWand)) ++ + CommentBlock("inhale the RHS of the wand",inhaleModule.inhale(Seq((w.right, error)), statesStackForPackageStmt = statesStack, insidePackageStmt = inWand)) ++ heapModule.beginExhale ++ heapModule.endExhale ++ (if(inWand) exchangeAssumesWithBoolean(stateModule.assumeGoodState, OPS.boolVar) else stateModule.assumeGoodState) //GP: using beginExhale, endExhale works now, but isn't intuitive, maybe should duplicate code to avoid this breaking diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index 3f8ccbd0..a33d4ae2 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -773,8 +773,8 @@ class QuantifiedPermModule(val verifier: Verifier) Nil } - override def inhaleExp(e: sil.Exp): Stmt = { - inhaleAux(e, Assume) + override def inhaleExp(e: sil.Exp, error: PartialVerificationError): Stmt = { + inhaleAux(e, Assume, error) } override def inhaleWandFt(w: sil.MagicWand): Stmt = { @@ -794,12 +794,25 @@ class QuantifiedPermModule(val verifier: Verifier) * Boogie program * Note: right now (05.04.15) inhale AND transferAdd both use this function */ - private def inhaleAux(e: sil.Exp, assmsToStmt: Exp => Stmt):Stmt = { + private def inhaleAux(e: sil.Exp, assmsToStmt: Exp => Stmt, error: PartialVerificationError):Stmt = { e match { case sil.AccessPredicate(loc: LocationAccess, prm) => val perm = PermissionSplitter.normalizePerm(prm) val curPerm = currentPermission(loc) val permVar = LocalVar(Identifier("perm"), permType) + + /* + case sil.AccessPredicate(loc: LocationAccess, prm) => + val p = PermissionSplitter.normalizePerm(prm) + val perms = PermissionSplitter.splitPerm(p) filter (x => x._1 - 1 == exhaleModule.currentPhaseId) + (if (exhaleModule.currentPhaseId == 0) + (if (!p.isInstanceOf[sil.WildcardPerm]) + Assert(permissionPositiveInternal(translatePerm(p), Some(p), true), error.dueTo(reasons.NegativePermission(p))) else Nil: Stmt) ++ Nil // check amount is non-negative + else Nil) ++ + */ + + + val (permVal, stmts): (Exp, Stmt) = if (perm.isInstanceOf[WildcardPerm]) { val w = LocalVar(Identifier("wildcard"), Real) @@ -808,9 +821,13 @@ class QuantifiedPermModule(val verifier: Verifier) (translatePerm(perm), Nil) } stmts ++ - (permVar := permVal) ++ - assmsToStmt(permissionPositiveInternal(permVar, Some(perm), true)) ++ - assmsToStmt(permissionPositiveInternal(permVar, Some(perm), false) ==> checkNonNullReceiver(loc)) ++ + (permVar := permVal) ++ + (if (perm.isInstanceOf[WildcardPerm]) + assmsToStmt(checkNonNullReceiver(loc)) + else + Assert(permissionPositiveInternal(permVar, Some(perm), true), error.dueTo(reasons.NegativePermission(perm))) ++ + assmsToStmt(permissionPositiveInternal(permVar, Some(perm), false) ==> checkNonNullReceiver(loc)) + ) ++ (if (!usingOldState) curPerm := permAdd(curPerm, permVar) else Nil) case w@sil.MagicWand(left,right) => val wandRep = wandModule.getWandRepresentation(w) From 118967459347de7814ebee9ed8d5b8bef5b897bb Mon Sep 17 00:00:00 2001 From: Thibault Date: Mon, 12 Jul 2021 19:22:49 +0200 Subject: [PATCH 2/4] Inhaling negative permission results in failure, inhaling QPs without injectivity also --- build.sbt | 2 + src/main/scala/viper/carbon/Carbon.scala | 6 + .../scala/viper/carbon/CarbonVerifier.scala | 3 + .../modules/impls/DefaultStmtModule.scala | 2 +- .../modules/impls/QuantifiedPermModule.scala | 128 +++++++++++++----- .../viper/carbon/verifier/Verifier.scala | 1 + src/test/scala/viper/carbon/AllTests.scala | 6 +- 7 files changed, 113 insertions(+), 35 deletions(-) diff --git a/build.sbt b/build.sbt index 53c59034..ece9c4bb 100644 --- a/build.sbt +++ b/build.sbt @@ -22,6 +22,8 @@ lazy val carbon = (project in file(".")) Test / fork := true, Test / testOptions += Tests.Argument(TestFrameworks.ScalaTest, "-u", "target/test-reports", "-oD"), + Compile / fork := true, + // Assembly settings assembly / assemblyJarName := "carbon.jar", // JAR filename assembly / mainClass := Some("viper.carbon.Carbon"), // Define JAR's entry point diff --git a/src/main/scala/viper/carbon/Carbon.scala b/src/main/scala/viper/carbon/Carbon.scala index f3283386..08a5a24a 100644 --- a/src/main/scala/viper/carbon/Carbon.scala +++ b/src/main/scala/viper/carbon/Carbon.scala @@ -95,5 +95,11 @@ class CarbonConfig(args: Seq[String]) extends SilFrontendConfig(args, "Carbon") noshort = true ) + val checkInjectivity = opt[Boolean]("checkInjectivity", + descr = "Check injectivity of the receiver for QPs instead of assuming it (default: disabled)", + default = None, + noshort = true + ) + verify() } diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala index 3704393f..0ad6c245 100644 --- a/src/main/scala/viper/carbon/CarbonVerifier.scala +++ b/src/main/scala/viper/carbon/CarbonVerifier.scala @@ -87,6 +87,9 @@ case class CarbonVerifier(override val reporter: Reporter, case None => z3Default } else z3Default + def checkInjectivity = if (config != null) config.checkInjectivity.isSupplied else false + + def name: String = "carbon" def version: String = "1.0" def buildVersion = version diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala index 51c22529..9bc0cf56 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala @@ -190,7 +190,7 @@ class DefaultStmtModule(val verifier: Verifier) extends StmtModule with SimpleSt exhale(pres map (e => (e, errors.PreconditionInCallFalse(mc).withReasonNodeTransformed(renamingArguments))), statesStackForPackageStmt = statesStack, insidePackageStmt = insidePackageStmt)) ++ { stateModule.replaceOldState(preCallState) val res = MaybeCommentBlock("Inhaling postcondition", - inhale(posts map (e => (e, errors.PostconditionInCallFalse(mc).withReasonNodeTransformed(renamingArguments))), statesStack, insidePackageStmt) ++ + inhale(posts map (e => (e, errors.CallFailed(mc).withReasonNodeTransformed(renamingArguments))), statesStack, insidePackageStmt) ++ executeUnfoldings(posts, (post => errors.Internal(post).withReasonNodeTransformed(renamingArguments)))) stateModule.replaceOldState(oldState) toUndefine map mainModule.env.undefine diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index a33d4ae2..71d1948a 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -840,7 +840,7 @@ class QuantifiedPermModule(val verifier: Verifier) Nil } else { //Quantified Permission - val stmt:Stmt = translateInhale(fa) + val stmt:Stmt = translateInhale(fa, error) stmt ++ Nil } case _ => Nil @@ -936,7 +936,7 @@ class QuantifiedPermModule(val verifier: Verifier) /* translate inhaling a forall expressions */ - def translateInhale(e: sil.Forall): Stmt = e match{ + def translateInhale(e: sil.Forall, error: PartialVerificationError): Stmt = e match{ case SourceQuantifiedPermissionAssertion(forall, Implies(cond, expr)) => val vs = forall.variables // TODO: Generalise to multiple quantified variables @@ -946,7 +946,9 @@ class QuantifiedPermModule(val verifier: Verifier) // alpha renaming, to avoid clashes in context, use vFresh instead of v val vsFresh = vs.map(v => env.makeUniquelyNamed(v)) vsFresh.foreach(vFresh => env.define(vFresh.localVar)) - def renaming[E <: sil.Exp] = (e:E) => Expressions.renameVariables(e, vs.map(v => v.localVar), vsFresh.map (vFresh => vFresh.localVar)) + + def renaming[E <: sil.Exp] = (e: E) => Expressions.renameVariables(e, vs.map(v => v.localVar), vsFresh.map(vFresh => vFresh.localVar)) + val (renamingCond, renamingRecv, renamingPerms, renamingFieldAccess) = (renaming(cond), renaming(recv), renaming(perms), renaming(fieldAccess)) val renamedTriggers = e.triggers.map(t => sil.Trigger(t.exps.map(x => renaming(x)))(t.pos, t.info)) @@ -963,15 +965,15 @@ class QuantifiedPermModule(val verifier: Verifier) } } val translatedTriggers = renamedTriggers.map(t => Trigger(t.exps.map(x => translateExp(x)))) - val translatedLocation = translateLocation(Expressions.instantiateVariables(fieldAccess, vs.map(v => v.localVar), vsFresh.map(vFresh => vFresh.localVar))) + val translatedLocation = translateLocation(Expressions.instantiateVariables(fieldAccess, vs.map(v => v.localVar), vsFresh.map(vFresh => vFresh.localVar))) //define inverse function and inverse terms val obj = LocalVarDecl(Identifier("o"), refType) val field = LocalVarDecl(Identifier("f"), fieldType) - val curPerm:Exp = currentPermission(obj.l,translatedLocation) + val curPerm: Exp = currentPermission(obj.l, translatedLocation) - val (invFuns,rangeFun,_) = addQPFunctions(translatedLocals) // for the moment, the injectivity check is not made on inhale, so we don't need the third (trigger) function - val invFunApps = invFuns.map(invFun => FuncApp(invFun.name, Seq(obj.l), invFun.typ )) + val (invFuns, rangeFun, triggerFun) = addQPFunctions(translatedLocals) // for the moment, the injectivity check is not made on inhale, so we don't need the third (trigger) function + val invFunApps = invFuns.map(invFun => FuncApp(invFun.name, Seq(obj.l), invFun.typ)) val rangeFunApp = FuncApp(rangeFun.name, Seq(obj.l), rangeFun.typ) // range(o): used to test whether an element of the mapped-to type is in the image of the QP's domain, projected by the receiver expression val rangeFunRecvApp = FuncApp(rangeFun.name, Seq(translatedRecv), rangeFun.typ) // range(e(v)) var condInv = translatedCond @@ -987,10 +989,10 @@ class QuantifiedPermModule(val verifier: Verifier) //Trigger for first inverse function. If user-defined triggers are provided, (only) these are used. Otherwise, those auto-generated + triggers corresponding to looking up the location are chosen val recvTrigger = Trigger(Seq(translatedRecv)) - lazy val candidateTriggers : Seq[Trigger] = if (validateTrigger(translatedLocals,recvTrigger).isEmpty) // if we can't use the receiver, maybe we can use H[recv,field] etc.. - validateTriggers(translatedLocals,Seq(Trigger(Seq(translateLocationAccess(translatedRecv, translatedLocation))),Trigger(Seq(currentPermission(qpMask,translatedRecv , translatedLocation))))) else Seq(recvTrigger) + lazy val candidateTriggers: Seq[Trigger] = if (validateTrigger(translatedLocals, recvTrigger).isEmpty) // if we can't use the receiver, maybe we can use H[recv,field] etc.. + validateTriggers(translatedLocals, Seq(Trigger(Seq(translateLocationAccess(translatedRecv, translatedLocation))), Trigger(Seq(currentPermission(qpMask, translatedRecv, translatedLocation))))) else Seq(recvTrigger) - val providedTriggers : Seq[Trigger] = validateTriggers(translatedLocals, translatedTriggers) + val providedTriggers: Seq[Trigger] = validateTriggers(translatedLocals, translatedTriggers) // add default trigger if triggers were generated automatically val tr1: Seq[Trigger] = /*if (e.info.getUniqueInfo[sil.AutoTriggered.type].isDefined)*/ candidateTriggers ++ providedTriggers /*else providedTriggers*/ @@ -998,46 +1000,75 @@ class QuantifiedPermModule(val verifier: Verifier) val assm1Rhs = (0 until invFuns.length).foldLeft(rangeFunRecvApp: Exp)((soFar, i) => BinExp(soFar, And, FuncApp(invFuns(i).name, Seq(translatedRecv), invFuns(i).typ) === translatedLocals(i).l)) val invAssm1 = (Forall(translatedLocals, tr1, (translatedCond && permGt(translatedPerms, noPerm)) ==> assm1Rhs)) - val invAssm2 = Forall(Seq(obj), Trigger(invFuns.map(invFun => FuncApp(invFun.name, Seq(obj.l), invFun.typ))), ((condInv && permGt(permInv, noPerm))&&rangeFunApp) ==> (rcvInv === obj.l) ) + val invAssm2 = Forall(Seq(obj), Trigger(invFuns.map(invFun => FuncApp(invFun.name, Seq(obj.l), invFun.typ))), ((condInv && permGt(permInv, noPerm)) && rangeFunApp) ==> (rcvInv === obj.l)) //Define non-null Assumptions: val nonNullAssumptions = - Assume(Forall(translatedLocals,tr1,(translatedCond && permissionPositiveInternal(translatedPerms, Some(renamingPerms), false)) ==> - (translatedRecv !== translateNull) )) + Assume(Forall(translatedLocals, tr1, (translatedCond && permissionPositiveInternal(translatedPerms, Some(renamingPerms), false)) ==> + (translatedRecv !== translateNull))) val translatedLocalVarDecl = vsFresh.map(vFresh => translateLocalVarDecl(vFresh)) //permission should be >= 0 if the condition is satisfied - val permPositive = Assume(Forall(translatedLocalVarDecl, tr1, translatedCond ==> permissionPositiveInternal(translatedPerms,None,true))) + + // TD: Positive permissions are not assumed anymore + // val permPositive = Assume(Forall(translatedLocalVarDecl, tr1, translatedCond ==> permissionPositiveInternal(translatedPerms,None,true))) + //check that given the condition, the permission held should be non-negative + val permPositive = Assert(Forall(translatedLocalVarDecl, tr1, translatedCond ==> permissionPositiveInternal(translatedPerms, None, true)), + error.dueTo(reasons.NegativePermission(perms))) + //Define Permission to all locations of field f for locations where condition applies: add permission defined - val condTrueLocations = (((condInv && permGt(permInv, noPerm))&&rangeFunApp) ==> ((permGt(permInv, noPerm) ==> (rcvInv === obj.l)) && ( + val condTrueLocations = (((condInv && permGt(permInv, noPerm)) && rangeFunApp) ==> ((permGt(permInv, noPerm) ==> (rcvInv === obj.l)) && ( (if (!usingOldState) { - ( currentPermission(qpMask,obj.l,translatedLocation) === curPerm + permInv ) + (currentPermission(qpMask, obj.l, translatedLocation) === curPerm + permInv) } else { - currentPermission(qpMask,obj.l,translatedLocation) === curPerm - } ) - )) ) + currentPermission(qpMask, obj.l, translatedLocation) === curPerm + }) + ))) //Define Permission to all locations of field f for locations where condition does not applies: no change - val condFalseLocations = (((condInv && permGt(permInv, noPerm))&&rangeFunApp).not ==> (currentPermission(qpMask,obj.l,translatedLocation) === curPerm)) + val condFalseLocations = (((condInv && permGt(permInv, noPerm)) && rangeFunApp).not ==> (currentPermission(qpMask, obj.l, translatedLocation) === curPerm)) - //Define Permissions to all independent locations: no change - val independentLocations = Assume(Forall(Seq(obj,field), Trigger(currentPermission(obj.l,field.l))++ - Trigger(currentPermission(qpMask,obj.l,field.l)),(field.l !== translatedLocation) ==> - (currentPermission(obj.l,field.l) === currentPermission(qpMask,obj.l,field.l))) ) + //Define Permissions to all independent locations: no change + val independentLocations = Assume(Forall(Seq(obj, field), Trigger(currentPermission(obj.l, field.l)) ++ + Trigger(currentPermission(qpMask, obj.l, field.l)), (field.l !== translatedLocation) ==> + (currentPermission(obj.l, field.l) === currentPermission(qpMask, obj.l, field.l)))) - val triggerForPermissionUpdateAxiom = Seq(/*Trigger(curPerm),*/Trigger(currentPermission(qpMask,obj.l,translatedLocation))/*,Trigger(invFunApp)*/) + val triggerForPermissionUpdateAxiom = Seq(/*Trigger(curPerm),*/ Trigger(currentPermission(qpMask, obj.l, translatedLocation)) /*,Trigger(invFunApp)*/) + /* val v2s = translatedLocals.map(translatedLocal => LocalVarDecl(Identifier("v2"),translatedLocal.typ)) val injectiveTrigger = tr1.map(trigger => Trigger(trigger.exps ++ trigger.exps.map(exp => replaceAll(exp, translatedLocals.map(translatedLocal => translatedLocal.l), v2s.map(v2 => v2.l))))) - //val injectiveAssumption = Assume(Forall( translatedLocal++v2,injectiveTrigger,((translatedLocal.l !== v2.l) && translatedCond && translatedCond.replace(translatedLocal.l, v2.l) ) ==> (translatedRecv !== translatedRecv.replace(translatedLocal.l, v2.l)))) + val injectiveCheck = Assert(Forall( translatedLocal++v2,injectiveTrigger,((translatedLocal.l !== v2.l) && translatedCond && translatedCond.replace(translatedLocal.l, v2.l) ) ==> (translatedRecv !== translatedRecv.replace(translatedLocal.l, v2.l))), + error.dueTo(reasons.ReceiverNotInjective(fieldAccess))) + */ + + + //injectivity assertion + val v2s = translatedLocals.map(translatedLocal => LocalVarDecl(Identifier(translatedLocal.name.name), translatedLocal.typ)) + var triggerFunApp2 = FuncApp(triggerFun.name, translatedLocals.map(v => LocalVar(v.name, v.typ)), triggerFun.typ) + var notEquals: Exp = TrueLit() + var translatedPerms2 = translatedPerms + var translatedCond2 = translatedCond + var translatedRecv2 = translatedRecv + for (i <- 0 until translatedLocals.length) { + triggerFunApp2 = triggerFunApp2.replace(translatedLocals(i).l, v2s(i).l) + translatedPerms2 = translatedPerms2.replace(translatedLocals(i).l, v2s(i).l) + translatedCond2 = translatedCond2.replace(translatedLocals(i).l, v2s(i).l) + translatedRecv2 = translatedRecv2.replace(translatedLocals(i).l, v2s(i).l) + notEquals = notEquals && (translatedLocals(i).l !== v2s(i).l) + } + val is_injective = Forall(translatedLocals ++ v2s, validateTriggers(translatedLocals ++ v2s, Seq(Trigger(Seq(triggerFunApp2)))), (notEquals && translatedCond && translatedCond2 && permGt(translatedPerms, noPerm) && permGt(translatedPerms2, noPerm)) ==> (translatedRecv !== translatedRecv2)) + val injectiveAssertion = Assert(is_injective, error.dueTo(reasons.ReceiverNotInjective(fieldAccess))) val res1 = Havoc(qpMask) ++ stmts ++ + (if (verifier.checkInjectivity) injectiveAssertion + else Nil) ++ CommentBlock("Define Inverse Function", Assume(invAssm1) ++ Assume(invAssm2)) ++ + MaybeComment("Check that permission expression is non-negative for all fields", permPositive) ++ CommentBlock("Assume set of fields is nonNull", nonNullAssumptions) ++ - MaybeComment("Assume permission expression is non-negative for all fields", permPositive) ++ // CommentBlock("Assume injectivity", injectiveAssumption) ++ CommentBlock("Define permissions", Assume(Forall(obj,triggerForPermissionUpdateAxiom, condTrueLocations&&condFalseLocations )) ++ independentLocations) ++ @@ -1081,7 +1112,7 @@ class QuantifiedPermModule(val verifier: Verifier) val translatedTriggers : Seq[Trigger] = renamedTriggers.map(trigger => Trigger(trigger.exps.map(x => translateExp(x)))) //define inverse function - val (invFuns,rangeFun,_) = addQPFunctions(translatedLocals, freshFormalBoogieDecls) // for the moment, the injectivity check is not made on inhale, so we don't need the third (trigger) function + val (invFuns,rangeFun,triggerFun) = addQPFunctions(translatedLocals, freshFormalBoogieDecls) // for the moment, the injectivity check is not made on inhale, so we don't need the third (trigger) function val funApps = invFuns.map(invFun => FuncApp(invFun.name, translatedArgs, invFun.typ)) val invFunApps = invFuns.map(invFun => FuncApp(invFun.name, freshFormalBoogieVars, invFun.typ)) @@ -1119,10 +1150,15 @@ class QuantifiedPermModule(val verifier: Verifier) //trigger for both map descriptions val triggerForPermissionUpdateAxioms = Seq(Trigger(currentPermission(qpMask,translateNull, general_location))/*, Trigger(invFunApp)*/) + // TD: We do not assume anymore that the permissions are non-negative, and we need to check them // permissions non-negative - val permPositive = Assume(Forall(translatedLocals, tr1, translatedCond ==> permissionPositiveInternal(translatedPerms,None,true))) + // val permPositive = Assume(Forall(translatedLocals, tr1, translatedCond ==> permissionPositiveInternal(translatedPerms,None,true))) + //check that given the condition, the permission held should be non-negative + val permPositive = Assert(Forall(translatedLocals, tr1, translatedCond ==> permissionPositiveInternal(translatedPerms,None,true)), + error.dueTo(reasons.NegativePermission(perms))) - //assumptions for predicates that gain permission + + //assumptions for predicates that gain permission val permissionsMap = Assume( { val exp = ((condInv && permGt(permInv, noPerm)) && rangeFunApp) ==> ((permGt(permInv, noPerm) ==> conjoinedInverseAssumptions) && (currentPermission(qpMask,translateNull, general_location) === currentPermission(translateNull, general_location) + permInv)) @@ -1153,16 +1189,44 @@ class QuantifiedPermModule(val verifier: Verifier) ((obj.l !== translateNull) || isPredicateField(fieldVar).not || (getPredicateId(fieldVar) !== IntLit(getPredicateId(predname)) )) ==> (currentPermission(obj.l,field.l) === currentPermission(qpMask,obj.l,field.l)))) - //assume injectivity of inverse function + //define second variable and other arguments needed to express injectivity val v2s = vs.map(v => env.makeUniquelyNamed(v)) v2s.foreach(v2 => env.define(v2.localVar)) + //assert injectivity of inverse function: + val translatedLocals2 = translatedLocals.map(translatedLocal => LocalVarDecl(Identifier(translatedLocal.name.name), translatedLocal.typ)) //new varible + + val triggerFunApp = FuncApp(triggerFun.name, translatedLocals.map(translatedLocal => LocalVar(translatedLocal.name, translatedLocal.typ)), triggerFun.typ) + + var unequalities : Exp = TrueLit() + var translatedCond2 = translatedCond + var translatedPerms2 = translatedPerms + var translatedArgs2 = translatedArgs + var triggerFunApp2 = triggerFunApp + for (i <- 0 until translatedLocals.length) { + unequalities = unequalities && (translatedLocals(i).l.!==(translatedLocals2(i).l)) + translatedCond2 = translatedCond2.replace(translatedLocals(i).l, translatedLocals2(i).l) + translatedPerms2 = translatedPerms2.replace(translatedLocals(i).l, translatedLocals2(i).l) + translatedArgs2 = translatedArgs2.map(a => a.replace(translatedLocals(i).l, translatedLocals2(i).l)) + triggerFunApp2 = triggerFunApp2.replace(translatedLocals(i).l, translatedLocals2(i).l) + } + + val injectiveCond = unequalities && translatedCond && translatedCond2 && permGt(translatedPerms, noPerm) && permGt(translatedPerms2, noPerm); + //val translatedArgs2= translatedArgs.map(x => x.replace(translatedLocal.l, translatedLocal2.l)) + val ineqs = (translatedArgs zip translatedArgs2).map(x => x._1 !== x._2) + val ineqExpr = ineqs.reduce((expr1, expr2) => (expr1) || (expr2)) + val injectTrigger = Seq(Trigger(Seq(triggerFunApp, triggerFunApp2))) + val injectiveAssertion = Assert(Forall((translatedLocals ++ translatedLocals2), injectTrigger,injectiveCond ==> ineqExpr), error.dueTo(reasons.ReceiverNotInjective(predAccPred.loc))) + + val res1 = Havoc(qpMask) ++ stmts ++ + (if (verifier.checkInjectivity) CommentBlock("check if receiver " + predAccPred.toString() + " is injective",injectiveAssertion) + else Nil) ++ CommentBlock("Define Inverse Function", Assume(invAssm1) ++ Assume(invAssm2)) ++ - MaybeComment("Assume permission expression is non-negative for all fields", permPositive) ++ + MaybeComment("Check that permission expression is non-negative for all fields", permPositive) ++ CommentBlock("Define updated permissions", permissionsMap) ++ CommentBlock("Define independent locations", (independentLocations ++ independentPredicate)) ++ diff --git a/src/main/scala/viper/carbon/verifier/Verifier.scala b/src/main/scala/viper/carbon/verifier/Verifier.scala index 5296eea9..ef9f59bf 100644 --- a/src/main/scala/viper/carbon/verifier/Verifier.scala +++ b/src/main/scala/viper/carbon/verifier/Verifier.scala @@ -76,5 +76,6 @@ trait Verifier { */ def replaceProgram(prog : sil.Program): Unit + def checkInjectivity: Boolean } diff --git a/src/test/scala/viper/carbon/AllTests.scala b/src/test/scala/viper/carbon/AllTests.scala index 3a132438..6b0d06d3 100644 --- a/src/test/scala/viper/carbon/AllTests.scala +++ b/src/test/scala/viper/carbon/AllTests.scala @@ -18,8 +18,10 @@ import viper.silver.reporter.{NoopReporter, StdIOReporter} */ class AllTests extends SilSuite { - override def testDirectories: Seq[String] = Vector("local", "all", "quantifiedpermissions", "quantifiedpredicates", "quantifiedcombinations", "wands", "examples", "termination" -// override def testDirectories: Seq[String] = Vector("wandsAhmed" + // override def testDirectories: Seq[String] = Vector("local", "all", "quantifiedpermissions", "quantifiedpredicates", "quantifiedcombinations", "wands", "examples", "termination" + override def testDirectories: Seq[String] = Vector("522" + + // override def testDirectories: Seq[String] = Vector("wandsAhmed" //, "generated" ) From e803e8ce4dc1ddf9a19a573dd6c94b766468a5a7 Mon Sep 17 00:00:00 2001 From: Thibault Date: Wed, 14 Jul 2021 21:24:24 +0200 Subject: [PATCH 3/4] Back to normal test --- src/test/scala/viper/carbon/AllTests.scala | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/test/scala/viper/carbon/AllTests.scala b/src/test/scala/viper/carbon/AllTests.scala index 6b0d06d3..15ce5976 100644 --- a/src/test/scala/viper/carbon/AllTests.scala +++ b/src/test/scala/viper/carbon/AllTests.scala @@ -18,9 +18,7 @@ import viper.silver.reporter.{NoopReporter, StdIOReporter} */ class AllTests extends SilSuite { - // override def testDirectories: Seq[String] = Vector("local", "all", "quantifiedpermissions", "quantifiedpredicates", "quantifiedcombinations", "wands", "examples", "termination" - override def testDirectories: Seq[String] = Vector("522" - + override def testDirectories: Seq[String] = Vector("local", "all", "quantifiedpermissions", "quantifiedpredicates", "quantifiedcombinations", "wands", "examples", "termination" // override def testDirectories: Seq[String] = Vector("wandsAhmed" //, "generated" ) From 4f42371f7e0919490421d749d67a15c3caa6fc92 Mon Sep 17 00:00:00 2001 From: Thibault Date: Thu, 15 Jul 2021 11:25:40 +0200 Subject: [PATCH 4/4] Moved --checkInjectivity flag from Carbon to Silver --- src/main/scala/viper/carbon/Carbon.scala | 6 ------ src/main/scala/viper/carbon/CarbonVerifier.scala | 6 +++++- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/main/scala/viper/carbon/Carbon.scala b/src/main/scala/viper/carbon/Carbon.scala index 08a5a24a..f3283386 100644 --- a/src/main/scala/viper/carbon/Carbon.scala +++ b/src/main/scala/viper/carbon/Carbon.scala @@ -95,11 +95,5 @@ class CarbonConfig(args: Seq[String]) extends SilFrontendConfig(args, "Carbon") noshort = true ) - val checkInjectivity = opt[Boolean]("checkInjectivity", - descr = "Check injectivity of the receiver for QPs instead of assuming it (default: disabled)", - default = None, - noshort = true - ) - verify() } diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala index 0ad6c245..d3101fc9 100644 --- a/src/main/scala/viper/carbon/CarbonVerifier.scala +++ b/src/main/scala/viper/carbon/CarbonVerifier.scala @@ -87,7 +87,11 @@ case class CarbonVerifier(override val reporter: Reporter, case None => z3Default } else z3Default - def checkInjectivity = if (config != null) config.checkInjectivity.isSupplied else false + def checkInjectivity = if (config != null) config.checkInjectivity.toOption match { + case Some(b) => b + case None => false + } + else false def name: String = "carbon"