From e9c1871c4df7e0612dc0edc7654fed267cc0bd83 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 5 Oct 2023 16:28:28 +0200 Subject: [PATCH 1/3] Alternative implementation of positive permission check for fold/unfold --- .../viper/carbon/modules/PermModule.scala | 2 ++ .../modules/impls/DefaultFuncPredModule.scala | 5 +++- .../modules/impls/QuantifiedPermModule.scala | 26 ++++++++++++------- 3 files changed, 22 insertions(+), 11 deletions(-) diff --git a/src/main/scala/viper/carbon/modules/PermModule.scala b/src/main/scala/viper/carbon/modules/PermModule.scala index d65603ec..b2fa90f0 100644 --- a/src/main/scala/viper/carbon/modules/PermModule.scala +++ b/src/main/scala/viper/carbon/modules/PermModule.scala @@ -45,6 +45,8 @@ trait PermModule extends Module with CarbonStateComponent { def conservativeIsPositivePerm(e: sil.Exp): Boolean + def isStrictlyPositivePerm(e: sil.Exp): Exp + /** * The current mask. */ diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index f274f655..49e5c2d1 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -20,6 +20,7 @@ import viper.silver.verifier.{NullPartialVerificationError, PartialVerificationE import scala.collection.mutable.ListBuffer import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion +import viper.silver.verifier.reasons.NonPositivePermission import scala.collection.mutable @@ -927,7 +928,8 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { , statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): (Stmt,Stmt) = { duringFold = true foldInfo = acc - val stmt = exhaleSingleWithoutDefinedness(Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), error, havocHeap = false, + val stmt = Assert(permModule.isStrictlyPositivePerm(acc.perm), error.dueTo(NonPositivePermission(acc.perm))) ++ + exhaleSingleWithoutDefinedness(Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), error, havocHeap = false, statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt) ++ inhale(Seq((acc, error)), addDefinednessChecks = false, statesStackForPackageStmt, insidePackageStmt) val stmtLast = Assume(predicateTrigger(heapModule.currentStateExps, acc.loc)) ++ { @@ -972,6 +974,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { val translatedArgs = location.args map translateExp Assume(translateLocationAccess(location) === getPredicateFrame(predicate,translatedArgs)._1) } ++ + Assert(permModule.isStrictlyPositivePerm(acc.perm), error.dueTo(NonPositivePermission(acc.perm))) ++ (if(exhaleUnfoldedPredicate) exhaleSingleWithoutDefinedness(acc, error, havocHeap = false, statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt) else Nil) ++ inhale(Seq((Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), error)), addDefinednessChecks = false, statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt) diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index dd9ac0b9..9fdc1a19 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -1601,26 +1601,30 @@ class QuantifiedPermModule(val verifier: Verifier) override def conservativeIsPositivePerm(e: sil.Exp): Boolean = PermissionHelper.conservativeStaticIsStrictlyPositivePerm(e) + override def isStrictlyPositivePerm(e: sil.Exp): Exp = PermissionHelper.isStrictlyPositivePerm(e) + object PermissionHelper { def isStrictlyPositivePerm(e: sil.Exp): Exp = { require(e isSubtype sil.Perm, s"found ${e.typ} ($e), but required Perm") - val backup = permissionPositiveInternal(translatePerm(e), Some(e)) + // Use backup lazily when needed only. This allows the function to work on WildcardPerms for which + // translatePerm would throw an exception. + val backup = () => permissionPositiveInternal(translatePerm(e), Some(e)) e match { case sil.NoPerm() => FalseLit() case sil.FullPerm() => TrueLit() case sil.WildcardPerm() => TrueLit() case sil.EpsilonPerm() => sys.error("epsilon permissions are not supported by this permission module") case x: sil.LocalVar if isAbstractRead(x) => TrueLit() - case sil.CurrentPerm(loc) => backup + case sil.CurrentPerm(loc) => backup() case sil.FractionalPerm(left, right) => val (l, r) = (translateExp(left), translateExp(right)) ((l > IntLit(0)) && (r > IntLit(0))) || ((l < IntLit(0)) && (r < IntLit(0))) case sil.PermMinus(a) => isStrictlyNegativePerm(a) case sil.PermAdd(left, right) => - (isStrictlyPositivePerm(left) && isStrictlyPositivePerm(right)) || backup - case sil.PermSub(left, right) => backup + (isStrictlyPositivePerm(left) && isStrictlyPositivePerm(right)) || backup() + case sil.PermSub(left, right) => backup() case sil.PermMul(a, b) => (isStrictlyPositivePerm(a) && isStrictlyPositivePerm(b)) || (isStrictlyNegativePerm(a) && isStrictlyNegativePerm(b)) case sil.PermDiv(a, b) => @@ -1633,7 +1637,7 @@ class QuantifiedPermModule(val verifier: Verifier) ((n > IntLit(0)) && isStrictlyPositivePerm(b)) || ((n < IntLit(0)) && isStrictlyNegativePerm(b)) case sil.CondExp(cond, thn, els) => CondExp(translateExp(cond), isStrictlyPositivePerm(thn), isStrictlyPositivePerm(els)) - case _ => backup + case _ => backup() } } @@ -1705,22 +1709,24 @@ class QuantifiedPermModule(val verifier: Verifier) def isStrictlyNegativePerm(e: sil.Exp): Exp = { require(e isSubtype sil.Perm) - val backup = UnExp(Not,permissionPositiveInternal(translatePerm(e), Some(e), true)) + // Use backup lazily when needed only. This allows the function to work on WildcardPerms for which + // translatePerm would throw an exception. + val backup = () => UnExp(Not,permissionPositiveInternal(translatePerm(e), Some(e), true)) e match { case sil.NoPerm() => FalseLit() // strictly negative case sil.FullPerm() => FalseLit() case sil.WildcardPerm() => FalseLit() case sil.EpsilonPerm() => sys.error("epsilon permissions are not supported by this permission module") case x: sil.LocalVar if isAbstractRead(x) => FalseLit() - case sil.CurrentPerm(loc) => backup + case sil.CurrentPerm(loc) => backup() case sil.FractionalPerm(left, right) => val (l, r) = (translateExp(left), translateExp(right)) ((l < IntLit(0)) && (r > IntLit(0))) || ((l > IntLit(0)) && (r < IntLit(0))) case sil.PermMinus(a) => isStrictlyPositivePerm(a) case sil.PermAdd(left, right) => - (isStrictlyNegativePerm(left) && isStrictlyNegativePerm(right)) || backup - case sil.PermSub(left, right) => backup + (isStrictlyNegativePerm(left) && isStrictlyNegativePerm(right)) || backup() + case sil.PermSub(left, right) => backup() case sil.PermMul(a, b) => (isStrictlyPositivePerm(a) && isStrictlyNegativePerm(b)) || (isStrictlyNegativePerm(a) && isStrictlyPositivePerm(b)) case sil.PermDiv(a, b) => @@ -1733,7 +1739,7 @@ class QuantifiedPermModule(val verifier: Verifier) ((n > IntLit(0)) && isStrictlyNegativePerm(b)) || ((n < IntLit(0)) && isStrictlyPositivePerm(b)) case sil.CondExp(cond, thn, els) => CondExp(translateExp(cond), isStrictlyNegativePerm(thn), isStrictlyNegativePerm(els)) - case _ => backup + case _ => backup() } } From db6587f7777f3ff10bf144f99dc818b30d528b86 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 6 Oct 2023 09:49:31 +0200 Subject: [PATCH 2/3] Updated silver version --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 07dce2bf..820db76e 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 07dce2bf8a90f6be9443ece6d1697b0e2767fb48 +Subproject commit 820db76e92646c57b180c7ccdc8dee0465118e62 From 1a90800d538f40e8f2cec45c51d01567760983ca Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 9 Oct 2023 16:59:34 +0200 Subject: [PATCH 3/3] Addressed review comments --- src/main/scala/viper/carbon/modules/PermModule.scala | 8 ++++++++ .../carbon/modules/impls/DefaultFuncPredModule.scala | 4 ++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/carbon/modules/PermModule.scala b/src/main/scala/viper/carbon/modules/PermModule.scala index b2fa90f0..fa3b4518 100644 --- a/src/main/scala/viper/carbon/modules/PermModule.scala +++ b/src/main/scala/viper/carbon/modules/PermModule.scala @@ -45,6 +45,14 @@ trait PermModule extends Module with CarbonStateComponent { def conservativeIsPositivePerm(e: sil.Exp): Boolean + /** + * Returns an expression representing that a permission amount is positive. + * Similar to [[permissionPositive]], but works directly on Viper expressions, *including* ones containing + * wildcards, and performs more aggressive simplifications. + * + * @param e the permission amount to be checked + * @return the expression representing the fact that the permission is positive + */ def isStrictlyPositivePerm(e: sil.Exp): Exp /** diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index 49e5c2d1..5ee2ee82 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -967,14 +967,14 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { duringUnfold = true duringUnfolding = isUnfolding unfoldInfo = acc - val stmt = Assume(predicateTrigger(heapModule.currentStateExps, acc.loc)) ++ + val stmt = Assert(permModule.isStrictlyPositivePerm(acc.perm), error.dueTo(NonPositivePermission(acc.perm))) ++ + Assume(predicateTrigger(heapModule.currentStateExps, acc.loc)) ++ { val location = acc.loc val predicate = verifier.program.findPredicate(location.predicateName) val translatedArgs = location.args map translateExp Assume(translateLocationAccess(location) === getPredicateFrame(predicate,translatedArgs)._1) } ++ - Assert(permModule.isStrictlyPositivePerm(acc.perm), error.dueTo(NonPositivePermission(acc.perm))) ++ (if(exhaleUnfoldedPredicate) exhaleSingleWithoutDefinedness(acc, error, havocHeap = false, statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt) else Nil) ++ inhale(Seq((Permissions.multiplyExpByPerm(acc.loc.predicateBody(verifier.program, env.allDefinedNames(program)).get,acc.perm), error)), addDefinednessChecks = false, statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt)