diff --git a/silver b/silver index 07dce2bf..820db76e 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 07dce2bf8a90f6be9443ece6d1697b0e2767fb48 +Subproject commit 820db76e92646c57b180c7ccdc8dee0465118e62 diff --git a/src/main/scala/viper/carbon/modules/PermModule.scala b/src/main/scala/viper/carbon/modules/PermModule.scala index d65603ec..fa3b4518 100644 --- a/src/main/scala/viper/carbon/modules/PermModule.scala +++ b/src/main/scala/viper/carbon/modules/PermModule.scala @@ -45,6 +45,16 @@ 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 + /** * 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..5ee2ee82 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)) ++ { @@ -965,7 +967,8 @@ 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) 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() } }