From 6a7280c9ff01f9f22eaa225fe9754c2c4cc603bc Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 13 Oct 2024 21:33:49 +0200 Subject: [PATCH 1/8] Assert-read-only function preconditions --- silver | 2 +- .../viper/carbon/modules/PermModule.scala | 4 + .../modules/impls/DefaultFuncPredModule.scala | 10 ++- .../modules/impls/DefaultMainModule.scala | 2 +- .../modules/impls/QuantifiedPermModule.scala | 82 +++++++++++++------ 5 files changed, 74 insertions(+), 26 deletions(-) diff --git a/silver b/silver index f649c0ba..4ea735d6 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit f649c0baf2fc133a5d99261dbb567b8a33732588 +Subproject commit 4ea735d6fdb47570d8b2105d9f051e76570f7b9d diff --git a/src/main/scala/viper/carbon/modules/PermModule.scala b/src/main/scala/viper/carbon/modules/PermModule.scala index 2c5bef1c..7806ed97 100644 --- a/src/main/scala/viper/carbon/modules/PermModule.scala +++ b/src/main/scala/viper/carbon/modules/PermModule.scala @@ -159,4 +159,8 @@ trait PermModule extends Module with CarbonStateComponent { // removes permission to w#ft (footprint of the magic wand) (See Heap module for w#ft description) def exhaleWandFt(w: sil.MagicWand): Stmt + def setCheckReadPermissionOnlyState(readOnly: Boolean): Boolean + + def assumePermUpperBounds: Stmt + } diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index 80aa2975..f4a60265 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -190,6 +190,8 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { override def translateFunction(f: sil.Function, names: Option[mutable.Map[String, String]]): Seq[Decl] = { env = Environment(verifier, f) ErrorMemberMapping.currentMember = f + + val oldPermOnlyState = permModule.setCheckReadPermissionOnlyState(true) val res = MaybeCommentedDecl(s"Translation of function ${f.name}", MaybeCommentedDecl("Uninterpreted function definitions", functionDefinitions(f), size = 1) ++ (if (f.isAbstract) Nil else @@ -207,6 +209,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { names.get ++= usedNames } + permModule.setCheckReadPermissionOnlyState(oldPermOnlyState) env = null ErrorMemberMapping.currentMember = null res @@ -871,12 +874,17 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { * contain permission introspection. */ val curState = stateModule.state + val oldReadState = permModule.setCheckReadPermissionOnlyState(true) defState.setDefState() val res = executeExhale() + permModule.setCheckReadPermissionOnlyState(oldReadState) stateModule.replaceState(curState) res case None => - executeExhale() + val oldReadState = permModule.setCheckReadPermissionOnlyState(true) + val res = executeExhale() + permModule.setCheckReadPermissionOnlyState(oldReadState) + res } } ) ++ diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala index 109942f0..28662a1f 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala @@ -137,7 +137,7 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles val initOldStateComment = "Initializing of old state" val ins: Seq[LocalVarDecl] = formalArgs map translateLocalVarDecl val outs: Seq[LocalVarDecl] = formalReturns map translateLocalVarDecl - val init = MaybeCommentBlock("Initializing the state", stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ stmtModule.initStmt(method.bodyOrAssumeFalse)) + val init = MaybeCommentBlock("Initializing the state", stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ permModule.assumePermUpperBounds ++ stmtModule.initStmt(method.bodyOrAssumeFalse)) val initOld = MaybeCommentBlock("Initializing the old state", stateModule.initOldState) val paramAssumptions = mWithLoopInfo.formalArgs map (a => allAssumptionsAboutValue(a.typ, translateLocalVarDecl(a), true)) val inhalePre = translateMethodDeclPre(pres) diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index 96a075e0..78ae7892 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -103,6 +103,9 @@ class QuantifiedPermModule(val verifier: Verifier) private val predicateMaskFieldName = Identifier("PredicateMaskField") private val wandMaskFieldName = Identifier("WandMaskField") + private val assumePermUpperBoundName = Identifier("AssumePermUpperBound") + private val assumePermUpperBound: Const = Const(assumePermUpperBoundName) + private val resultMask = LocalVarDecl(Identifier("ResultMask"),maskType) private val summandMask1 = LocalVarDecl(Identifier("SummandMask1"),maskType) @@ -122,6 +125,8 @@ class QuantifiedPermModule(val verifier: Verifier) private var rangeFuncs: ListBuffer[Func] = new ListBuffer[Func](); //list of inverse functions used for inhale/exhale qp private var triggerFuncs: ListBuffer[Func] = new ListBuffer[Func](); //list of inverse functions used for inhale/exhale qp + private var assertReadPermOnly: Boolean = false + private val readMaskName = Identifier("readMask") private val updateMaskName = Identifier("updMask") @@ -159,6 +164,7 @@ class QuantifiedPermModule(val verifier: Verifier) Seq(obj, field), Trigger(permInZeroPMask), permInZeroPMask === FalseLit())) :: + ConstDecl(assumePermUpperBoundName, Bool) :: // predicate mask function Func(predicateMaskFieldName, Seq(LocalVarDecl(Identifier("f"), predicateVersionFieldType())), @@ -195,7 +201,7 @@ class QuantifiedPermModule(val verifier: Verifier) Axiom(Forall(staticStateContributions(true, true) ++ obj ++ field, Trigger(Seq(staticGoodMask, perm)), // permissions are non-negative - (staticGoodMask ==> ( perm >= noPerm && + ((staticGoodMask && assumePermUpperBound) ==> ( perm >= noPerm && // permissions for fields which aren't predicates are smaller than 1 // permissions for fields which aren't predicates or wands are smaller than 1 ((staticGoodMask && heapModule.isPredicateField(field.l).not && heapModule.isWandField(field.l).not) ==> perm <= fullPerm ))) @@ -240,6 +246,10 @@ class QuantifiedPermModule(val verifier: Verifier) def permType = NamedType(permTypeName) + override def assumePermUpperBounds: Stmt = { + Assume(assumePermUpperBound) + } + def staticStateContributions(withHeap: Boolean, withPermissions: Boolean): Seq[LocalVarDecl] = if (withPermissions) Seq(LocalVarDecl(maskName, maskType)) else Seq() def currentStateContributions: Seq[LocalVarDecl] = Seq(LocalVarDecl(mask.name, maskType)) def currentStateVars : Seq[Var] = Seq(mask) @@ -259,6 +269,13 @@ class QuantifiedPermModule(val verifier: Verifier) inverseFuncs = new ListBuffer[Func](); rangeFuncs = new ListBuffer[Func](); triggerFuncs = new ListBuffer[Func](); + assertReadPermOnly = false + } + + override def setCheckReadPermissionOnlyState(readOnly: Boolean): Boolean = { + val oldState = assertReadPermOnly + assertReadPermOnly = readOnly + oldState } override def usingOldState = stateModuleIsUsingOldState @@ -367,15 +384,20 @@ class QuantifiedPermModule(val verifier: Verifier) (if (!usingOldState) currentMaskAssignUpdate(loc, permSub(curPerm, permToExhale)) else Nil) val permVar = LocalVar(Identifier("perm"), permType) - if (!p.isInstanceOf[sil.WildcardPerm]) { - val prmTranslated = translatePerm(p) - + if (assertReadPermOnly || !p.isInstanceOf[sil.WildcardPerm]) { + val prmTranslated = if (p.isInstanceOf[sil.WildcardPerm]) fullPerm else translatePerm(p) + if (assertReadPermOnly) { (permVar := prmTranslated) ++ Assert(permissionPositiveInternal(permVar, Some(p), true), error.dueTo(reasons.NegativePermission(p))) ++ - If(permVar !== noPerm, - Assert(permLe(permVar, curPerm), error.dueTo(reasons.InsufficientPermission(loc))), - Nil) ++ - subtractFromMask(permVar) + Assert(permLt(noPerm, permVar) ==> permLt(noPerm, curPerm), error.dueTo(reasons.InsufficientPermission(loc))) + } else { + (permVar := prmTranslated) ++ + Assert(permissionPositiveInternal(permVar, Some(p), true), error.dueTo(reasons.NegativePermission(p))) ++ + If(permVar !== noPerm, + Assert(permLe(permVar, curPerm), error.dueTo(reasons.InsufficientPermission(loc))), + Nil) ++ + subtractFromMask(permVar) + } } else { val curPerm = currentPermission(loc) val wildcard = LocalVar(Identifier("wildcard"), Real) @@ -389,9 +411,13 @@ class QuantifiedPermModule(val verifier: Verifier) case w@sil.MagicWand(_,_) => val wandRep = wandModule.getWandRepresentation(w) val curPerm = currentPermission(translateNull, wandRep) + val sufficientPermExp = if (assertReadPermOnly) + curPerm > noPerm + else + permLe(fullPerm, curPerm) Comment("permLe")++ - Assert(permLe(fullPerm, curPerm), error.dueTo(reasons.MagicWandChunkNotFound(w))) ++ - (if (!usingOldState) currentMaskAssignUpdate(translateNull, wandRep, permSub(curPerm, fullPerm)) else Nil) + Assert(sufficientPermExp, error.dueTo(reasons.MagicWandChunkNotFound(w))) ++ + (if (!usingOldState && !assertReadPermOnly) currentMaskAssignUpdate(translateNull, wandRep, permSub(curPerm, fullPerm)) else Nil) case fa@sil.Forall(v, cond, expr) => @@ -546,8 +572,10 @@ class QuantifiedPermModule(val verifier: Verifier) //define permission requirement val permNeeded = - if(isWildcard) { - currentPermission(translatedRecv, translatedLocation) > noPerm + if(assertReadPermOnly) { + translatedPerms > noPerm ==> currentPermission(translatedRecv, translatedLocation) > noPerm + } else if (isWildcard) { + currentPermission(translatedRecv, translatedLocation) > noPerm } else { currentPermission(translatedRecv, translatedLocation) >= translatedPerms } @@ -607,6 +635,11 @@ class QuantifiedPermModule(val verifier: Verifier) } val injectiveAssertion = Assert(is_injective, err) + val maskUpdateStmt = if (assertReadPermOnly) Nil else + CommentBlock("assume permission updates for field " + f.name, Assume(Forall(obj, triggersForPermissionUpdateAxiom, condTrueLocations && condFalseLocations))) ++ + CommentBlock("assume permission updates for independent locations", independentLocations) ++ + (mask := qpMask) + val res1 = Havoc(qpMask) ++ MaybeComment("wild card assumptions", stmts ++ wildcardAssms) ++ @@ -614,9 +647,7 @@ class QuantifiedPermModule(val verifier: Verifier) CommentBlock("check if receiver " + recv.toString + " is injective",injectiveAssertion) ++ CommentBlock("check if sufficient permission is held", enoughPerm) ++ CommentBlock("assumptions for inverse of receiver " + recv.toString, Assume(invAssm1)++ Assume(invAssm2)) ++ - CommentBlock("assume permission updates for field " + f.name, Assume(Forall(obj,triggersForPermissionUpdateAxiom, condTrueLocations && condFalseLocations ))) ++ - CommentBlock("assume permission updates for independent locations", independentLocations) ++ - (mask := qpMask) + maskUpdateStmt vsFresh.foreach(v => env.undefine(v.localVar)) @@ -711,8 +742,10 @@ class QuantifiedPermModule(val verifier: Verifier) //check that sufficient permission is held val permNeeded = - if(isWildcard) { - (currentPermission(translateNull, translatedResource) > RealLit(0)) + if(assertReadPermOnly) { + translatedPerms > noPerm ==> (currentPermission(translateNull, translatedResource) > noPerm) + } else if (isWildcard) { + (currentPermission(translateNull, translatedResource) > noPerm) } else { (currentPermission(translateNull, translatedResource) >= translatedPerms) } @@ -799,6 +832,12 @@ class QuantifiedPermModule(val verifier: Verifier) } val injectiveAssertion = Assert(Forall((translatedLocals ++ translatedLocals2), injectTrigger,injectiveCond ==> ineqExpr), err) + val maskUpdateStmts = if (assertReadPermOnly) Nil else + CommentBlock("assume permission updates", permissionsMap ++ + independentResource) ++ + CommentBlock("assume permission updates for independent locations ", independentLocations) ++ + (mask := qpMask) + val res1 = Havoc(qpMask) ++ MaybeComment("wildcard assumptions", stmts ++ wildcardAssms) ++ @@ -806,10 +845,7 @@ class QuantifiedPermModule(val verifier: Verifier) CommentBlock("check if receiver " + accPred.toString + " is injective",injectiveAssertion) ++ CommentBlock("check if sufficient permission is held", enoughPerm) ++ CommentBlock("assumptions for inverse of receiver " + accPred.toString, Assume(invAssm1)++ Assume(invAssm2)) ++ - CommentBlock("assume permission updates", permissionsMap ++ - independentResource) ++ - CommentBlock("assume permission updates for independent locations ", independentLocations) ++ - (mask := qpMask) + maskUpdateStmts vsFresh.foreach(vFresh => env.undefine(vFresh.localVar)) freshFormalDecls.foreach(x => env.undefine(x.localVar)) @@ -1009,7 +1045,7 @@ class QuantifiedPermModule(val verifier: Verifier) */ 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 + val vs = forall.variables val res = expr match { //Quantified Field Permission @@ -1171,7 +1207,7 @@ class QuantifiedPermModule(val verifier: Verifier) (if (!isWildcard) MaybeComment("Check that permission expression is non-negative for all fields", permPositive) else Nil) ++ CommentBlock("Assume set of fields is nonNull", nonNullAssumptions) ++ // CommentBlock("Assume injectivity", injectiveAssumption) ++ - CommentBlock("Define permissions", Assume(Forall(obj,triggerForPermissionUpdateAxiom, condTrueLocations&&condFalseLocations )) ++ + CommentBlock("Define permissions", Assume(Forall(obj, triggerForPermissionUpdateAxiom, condTrueLocations && condFalseLocations)) ++ independentLocations) ++ (mask := qpMask) From c999815ad286f0949a2e08248211953c1d855a38 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 13 Oct 2024 21:59:32 +0200 Subject: [PATCH 2/8] Update tests in silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 4ea735d6..89dce6fd 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 4ea735d6fdb47570d8b2105d9f051e76570f7b9d +Subproject commit 89dce6fde51d0a9bebf6db83c8968a5778be5a1f From 6048e9e2636c395ffdbd875509028536cfd936a0 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 15 Oct 2024 15:30:08 +0200 Subject: [PATCH 3/8] Fix assuming perm bounds in predicates, support flag to get old behavior --- silver | 2 +- src/main/scala/viper/carbon/CarbonVerifier.scala | 6 ++++++ .../viper/carbon/modules/impls/DefaultFuncPredModule.scala | 4 ++-- .../viper/carbon/modules/impls/QuantifiedPermModule.scala | 3 ++- src/main/scala/viper/carbon/verifier/Verifier.scala | 2 ++ 5 files changed, 13 insertions(+), 4 deletions(-) diff --git a/silver b/silver index 89dce6fd..626437b0 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 89dce6fde51d0a9bebf6db83c8968a5778be5a1f +Subproject commit 626437b04aaa354061246f8d07831ad8effdeb93 diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala index fc33d06a..8632851e 100644 --- a/src/main/scala/viper/carbon/CarbonVerifier.scala +++ b/src/main/scala/viper/carbon/CarbonVerifier.scala @@ -94,6 +94,12 @@ case class CarbonVerifier(override val reporter: Reporter, } else false + def respectFunctionPrecPermAmounts: Boolean = if (config != null) config.respectFunctionPrecPermAmounts.toOption match { + case Some(b) => b + case None => false + } + else false + override def usePolyMapsInEncoding = if (config != null) { config.desugarPolymorphicMaps.toOption match { diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index f4a60265..4b3dd2c8 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -191,7 +191,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { env = Environment(verifier, f) ErrorMemberMapping.currentMember = f - val oldPermOnlyState = permModule.setCheckReadPermissionOnlyState(true) + val oldPermOnlyState = permModule.setCheckReadPermissionOnlyState(!verifier.respectFunctionPrecPermAmounts) val res = MaybeCommentedDecl(s"Translation of function ${f.name}", MaybeCommentedDecl("Uninterpreted function definitions", functionDefinitions(f), size = 1) ++ (if (f.isAbstract) Nil else @@ -668,7 +668,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { val args = p.formalArgs map translateLocalVarDecl val init : Stmt = MaybeCommentBlock("Initializing the state", - stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true))) + stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ permModule.assumePermUpperBounds ++ (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true))) ) val predicateBody = p.body.get diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index 78ae7892..9af96186 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -198,10 +198,11 @@ class QuantifiedPermModule(val verifier: Verifier) Trigger(Seq(staticGoodState)), staticGoodState ==> staticGoodMask)) ++ { val perm = currentPermission(obj.l, field.l) + val shouldAssumePermUpperBound = if (verifier.respectFunctionPrecPermAmounts) TrueLit() else assumePermUpperBound Axiom(Forall(staticStateContributions(true, true) ++ obj ++ field, Trigger(Seq(staticGoodMask, perm)), // permissions are non-negative - ((staticGoodMask && assumePermUpperBound) ==> ( perm >= noPerm && + ((staticGoodMask && shouldAssumePermUpperBound) ==> ( perm >= noPerm && // permissions for fields which aren't predicates are smaller than 1 // permissions for fields which aren't predicates or wands are smaller than 1 ((staticGoodMask && heapModule.isPredicateField(field.l).not && heapModule.isWandField(field.l).not) ==> perm <= fullPerm ))) diff --git a/src/main/scala/viper/carbon/verifier/Verifier.scala b/src/main/scala/viper/carbon/verifier/Verifier.scala index ac28846b..9af97523 100644 --- a/src/main/scala/viper/carbon/verifier/Verifier.scala +++ b/src/main/scala/viper/carbon/verifier/Verifier.scala @@ -80,4 +80,6 @@ trait Verifier { def usePolyMapsInEncoding: Boolean + def respectFunctionPrecPermAmounts: Boolean + } From 232cf2d7d0cabf88aa8015ee2d73211bb6d58098 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 15 Oct 2024 17:54:42 +0200 Subject: [PATCH 4/8] Fixed good mask axiom --- .../viper/carbon/modules/impls/QuantifiedPermModule.scala | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index 9af96186..e1a8028b 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -202,10 +202,9 @@ class QuantifiedPermModule(val verifier: Verifier) Axiom(Forall(staticStateContributions(true, true) ++ obj ++ field, Trigger(Seq(staticGoodMask, perm)), // permissions are non-negative - ((staticGoodMask && shouldAssumePermUpperBound) ==> ( perm >= noPerm && - // permissions for fields which aren't predicates are smaller than 1 + (staticGoodMask ==> ( perm >= noPerm && // permissions for fields which aren't predicates or wands are smaller than 1 - ((staticGoodMask && heapModule.isPredicateField(field.l).not && heapModule.isWandField(field.l).not) ==> perm <= fullPerm ))) + ((staticGoodMask && shouldAssumePermUpperBound && heapModule.isPredicateField(field.l).not && heapModule.isWandField(field.l).not) ==> perm <= fullPerm ))) )) } ++ { val obj = LocalVarDecl(Identifier("o")(axiomNamespace), refType) val field = LocalVarDecl(Identifier("f")(axiomNamespace), fieldType) From 2dc9eba8cf447495328c0de0ba917291568f9b42 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 22 Oct 2024 17:06:54 +0200 Subject: [PATCH 5/8] Adapted to Silver changes, allowing compound expressions with wildcards in function preconditions --- silver | 2 +- src/main/scala/viper/carbon/CarbonVerifier.scala | 2 +- .../carbon/modules/impls/DefaultFuncPredModule.scala | 4 ++-- .../carbon/modules/impls/DefaultMainModule.scala | 4 ++-- .../carbon/modules/impls/QuantifiedPermModule.scala | 11 ++++++++--- 5 files changed, 14 insertions(+), 9 deletions(-) diff --git a/silver b/silver index 626437b0..aac52daa 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 626437b04aaa354061246f8d07831ad8effdeb93 +Subproject commit aac52daab393e3ce98148e30ed54808aedd3af54 diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala index 8632851e..f6c55489 100644 --- a/src/main/scala/viper/carbon/CarbonVerifier.scala +++ b/src/main/scala/viper/carbon/CarbonVerifier.scala @@ -94,7 +94,7 @@ case class CarbonVerifier(override val reporter: Reporter, } else false - def respectFunctionPrecPermAmounts: Boolean = if (config != null) config.respectFunctionPrecPermAmounts.toOption match { + def respectFunctionPrecPermAmounts: Boolean = if (config != null) config.respectFunctionPrePermAmounts.toOption match { case Some(b) => b case None => false } diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index 4b3dd2c8..0983ac2e 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -969,7 +969,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { wandModule.translatingStmtsInWandInit() } (checkDefinedness(acc, errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++ - checkDefinedness(perm, errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++ + checkDefinedness(perm.getOrElse(sil.FullPerm()()), errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++ foldFirst, foldLast) } } @@ -1006,7 +1006,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { unfold match { case sil.Unfold(acc@sil.PredicateAccessPredicate(pa@sil.PredicateAccess(_, _), perm)) => checkDefinedness(acc, errors.UnfoldFailed(unfold), insidePackageStmt = insidePackageStmt) ++ - checkDefinedness(perm, errors.UnfoldFailed(unfold)) ++ + checkDefinedness(perm.getOrElse(sil.FullPerm()()), errors.UnfoldFailed(unfold)) ++ unfoldPredicate(acc, errors.UnfoldFailed(unfold), false, statesStackForPackageStmt, insidePackageStmt) } } diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala index 28662a1f..f8b610cd 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala @@ -269,9 +269,9 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles val resourceCurPerm = q.exp match { case r : sil.FieldAccess => - sil.FieldAccessPredicate(r, curPermVar)() + sil.FieldAccessPredicate(r, Some(curPermVar))() case r: sil.PredicateAccess => - sil.PredicateAccessPredicate(r, curPermVar)() + sil.PredicateAccessPredicate(r, Some(curPermVar))() case _ => sys.error("Not supported resource in quasihavoc") } diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index e1a8028b..130da0a9 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -496,13 +496,14 @@ class QuantifiedPermModule(val verifier: Verifier) val vs = forall.variables val res = expr match { - case sil.FieldAccessPredicate(fieldAccess@sil.FieldAccess(recv, f), perms) => + case accPred@sil.FieldAccessPredicate(fieldAccess@sil.FieldAccess(recv, f), _) => // alpha renaming, to avoid clashes in context, use vFresh instead of v val vsFresh = vs.map(v => { val vFresh = env.makeUniquelyNamed(v) env.define(vFresh.localVar) vFresh }) + val perms = accPred.perm var isWildcard = false def renaming[E <: sil.Exp] = (e:E) => Expressions.renameVariables(e, vs.map(v => v.localVar), vsFresh.map(v => v.localVar)) @@ -1049,7 +1050,8 @@ class QuantifiedPermModule(val verifier: Verifier) val res = expr match { //Quantified Field Permission - case sil.FieldAccessPredicate(fieldAccess@sil.FieldAccess(recv, f), perms) => + case accPred@sil.FieldAccessPredicate(fieldAccess@sil.FieldAccess(recv, f), _) => + val perms = accPred.perm // alpha renaming, to avoid clashes in context, use vFresh instead of v var isWildcard = false val vsFresh = vs.map(v => env.makeUniquelyNamed(v)) @@ -1525,7 +1527,10 @@ class QuantifiedPermModule(val verifier: Verifier) case sil.FullPerm() => fullPerm case sil.WildcardPerm() => - sys.error("cannot translate wildcard at an arbitrary position (should only occur directly in an accessibility predicate)") + if (assertReadPermOnly) + fullPerm + else + sys.error("cannot translate wildcard at an arbitrary position (should only occur directly in an accessibility predicate)") case sil.EpsilonPerm() => sys.error("epsilon permissions are not supported by this permission module") case sil.CurrentPerm(res: ResourceAccess) => From 6e5ba478a7edef2e60eae834124298b27fae77f9 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 13 Nov 2024 16:46:47 +0100 Subject: [PATCH 6/8] Added comment to explain special case for wildcard translation --- .../viper/carbon/modules/impls/QuantifiedPermModule.scala | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index 130da0a9..aa32d443 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -1527,10 +1527,13 @@ class QuantifiedPermModule(val verifier: Verifier) case sil.FullPerm() => fullPerm case sil.WildcardPerm() => - if (assertReadPermOnly) + if (assertReadPermOnly) { + // We are in a context where permission amounts do not matter, so we can safely translate a wildcard to + // a full permission. fullPerm - else + } else { sys.error("cannot translate wildcard at an arbitrary position (should only occur directly in an accessibility predicate)") + } case sil.EpsilonPerm() => sys.error("epsilon permissions are not supported by this permission module") case sil.CurrentPerm(res: ResourceAccess) => From c82ff6bd24d58ce0d2f51aa8021cce4b92ed39f7 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 2 Dec 2024 12:15:08 +0100 Subject: [PATCH 7/8] Updating silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index aac52daa..cc7706f1 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit aac52daab393e3ce98148e30ed54808aedd3af54 +Subproject commit cc7706f131ea1932fafb7db2e2909750a222e6cf From 2280c325c4eb3aaa2ed729477353c60d00485c99 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 18 Dec 2024 14:12:00 +0100 Subject: [PATCH 8/8] Incorporating Gaurav's suggestions --- silver | 2 +- .../viper/carbon/modules/PermModule.scala | 5 ++-- .../modules/impls/DefaultFuncPredModule.scala | 25 +++++++++++------ .../modules/impls/DefaultMainModule.scala | 3 ++- .../modules/impls/QuantifiedPermModule.scala | 27 ++++++++++++------- 5 files changed, 39 insertions(+), 23 deletions(-) diff --git a/silver b/silver index cc7706f1..e771eee4 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit cc7706f131ea1932fafb7db2e2909750a222e6cf +Subproject commit e771eee40a5a55c2f9b4bea7c3252c756552f356 diff --git a/src/main/scala/viper/carbon/modules/PermModule.scala b/src/main/scala/viper/carbon/modules/PermModule.scala index 7806ed97..ef010516 100644 --- a/src/main/scala/viper/carbon/modules/PermModule.scala +++ b/src/main/scala/viper/carbon/modules/PermModule.scala @@ -8,7 +8,6 @@ package viper.carbon.modules import viper.carbon.boogie._ import viper.carbon.modules.components.CarbonStateComponent -import viper.carbon.utility.PolyMapRep import viper.silver.{ast => sil} case class PMaskDesugaredRep(selectId: Identifier, storeId: Identifier) @@ -159,8 +158,8 @@ trait PermModule extends Module with CarbonStateComponent { // removes permission to w#ft (footprint of the magic wand) (See Heap module for w#ft description) def exhaleWandFt(w: sil.MagicWand): Stmt - def setCheckReadPermissionOnlyState(readOnly: Boolean): Boolean + def setCheckReadPermissionOnly(readOnly: Boolean): Boolean - def assumePermUpperBounds: Stmt + def assumePermUpperBounds(doAssume: Boolean): Stmt } diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index 0983ac2e..b7203c12 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -191,7 +191,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { env = Environment(verifier, f) ErrorMemberMapping.currentMember = f - val oldPermOnlyState = permModule.setCheckReadPermissionOnlyState(!verifier.respectFunctionPrecPermAmounts) + val oldCheckReadPermOnly = permModule.setCheckReadPermissionOnly(!verifier.respectFunctionPrecPermAmounts) val res = MaybeCommentedDecl(s"Translation of function ${f.name}", MaybeCommentedDecl("Uninterpreted function definitions", functionDefinitions(f), size = 1) ++ (if (f.isAbstract) Nil else @@ -209,7 +209,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { names.get ++= usedNames } - permModule.setCheckReadPermissionOnlyState(oldPermOnlyState) + permModule.setCheckReadPermissionOnly(oldCheckReadPermOnly) env = null ErrorMemberMapping.currentMember = null res @@ -645,7 +645,8 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { val args = f.formalArgs map translateLocalVarDecl val res = sil.Result(f.typ)() val init : Stmt = MaybeCommentBlock("Initializing the state", - stateModule.initBoogieState ++ (f.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true))) ++ assumeFunctionsAt(heights(f.name))) + stateModule.initBoogieState ++ (if (verifier.respectFunctionPrecPermAmounts) Nil else permModule.assumePermUpperBounds(false)) ++ + (f.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true))) ++ assumeFunctionsAt(heights(f.name))) val checkPre : Stmt = checkFunctionPreconditionDefinedness(f) val checkExp : Stmt = if (f.isAbstract) MaybeCommentBlock("(no definition for abstract function)",Nil) else MaybeCommentBlock("Check definedness of function body", @@ -668,7 +669,9 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { val args = p.formalArgs map translateLocalVarDecl val init : Stmt = MaybeCommentBlock("Initializing the state", - stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ permModule.assumePermUpperBounds ++ (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true))) + stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ + (if (verifier.respectFunctionPrecPermAmounts) Nil else permModule.assumePermUpperBounds(true)) ++ + (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true))) ) val predicateBody = p.body.get @@ -874,16 +877,16 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { * contain permission introspection. */ val curState = stateModule.state - val oldReadState = permModule.setCheckReadPermissionOnlyState(true) + val oldCheckReadPermOnly = permModule.setCheckReadPermissionOnly(!verifier.respectFunctionPrecPermAmounts) defState.setDefState() val res = executeExhale() - permModule.setCheckReadPermissionOnlyState(oldReadState) + permModule.setCheckReadPermissionOnly(oldCheckReadPermOnly) stateModule.replaceState(curState) res case None => - val oldReadState = permModule.setCheckReadPermissionOnlyState(true) + val oldCheckReadPermOnly = permModule.setCheckReadPermissionOnly(!verifier.respectFunctionPrecPermAmounts) val res = executeExhale() - permModule.setCheckReadPermissionOnlyState(oldReadState) + permModule.setCheckReadPermissionOnly(oldCheckReadPermOnly) res } } @@ -969,6 +972,9 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { wandModule.translatingStmtsInWandInit() } (checkDefinedness(acc, errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++ + // If no permission amount is supplied explicitly, we always use the default FullPerm; this is + // okay even if we are inside a function and only want to check for some positive amount, because permission + // amounts do not matter in this context. checkDefinedness(perm.getOrElse(sil.FullPerm()()), errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++ foldFirst, foldLast) } @@ -1006,6 +1012,9 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { unfold match { case sil.Unfold(acc@sil.PredicateAccessPredicate(pa@sil.PredicateAccess(_, _), perm)) => checkDefinedness(acc, errors.UnfoldFailed(unfold), insidePackageStmt = insidePackageStmt) ++ + // If no permission amount is supplied explicitly, we always use the default FullPerm; this is + // okay even if we are inside a function and only want to check for some positive amount, because permission + // amounts do not matter in this context. checkDefinedness(perm.getOrElse(sil.FullPerm()()), errors.UnfoldFailed(unfold)) ++ unfoldPredicate(acc, errors.UnfoldFailed(unfold), false, statesStackForPackageStmt, insidePackageStmt) } diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala index f8b610cd..2a5cf608 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala @@ -137,7 +137,8 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles val initOldStateComment = "Initializing of old state" val ins: Seq[LocalVarDecl] = formalArgs map translateLocalVarDecl val outs: Seq[LocalVarDecl] = formalReturns map translateLocalVarDecl - val init = MaybeCommentBlock("Initializing the state", stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ permModule.assumePermUpperBounds ++ stmtModule.initStmt(method.bodyOrAssumeFalse)) + val init = MaybeCommentBlock("Initializing the state", stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ + (if (verifier.respectFunctionPrecPermAmounts) Nil else permModule.assumePermUpperBounds(true)) ++ stmtModule.initStmt(method.bodyOrAssumeFalse)) val initOld = MaybeCommentBlock("Initializing the old state", stateModule.initOldState) val paramAssumptions = mWithLoopInfo.formalArgs map (a => allAssumptionsAboutValue(a.typ, translateLocalVarDecl(a), true)) val inhalePre = translateMethodDeclPre(pres) diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index aa32d443..548cc095 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -32,7 +32,6 @@ import viper.carbon.boogie.Const import viper.carbon.boogie.LocalVar import viper.silver.ast.{LocationAccess, PermMul, PredicateAccess, PredicateAccessPredicate, ResourceAccess, WildcardPerm} import viper.carbon.boogie.Forall -import viper.carbon.boogie.Assign import viper.carbon.boogie.Func import viper.carbon.boogie.TypeAlias import viper.carbon.boogie.FuncApp @@ -164,7 +163,6 @@ class QuantifiedPermModule(val verifier: Verifier) Seq(obj, field), Trigger(permInZeroPMask), permInZeroPMask === FalseLit())) :: - ConstDecl(assumePermUpperBoundName, Bool) :: // predicate mask function Func(predicateMaskFieldName, Seq(LocalVarDecl(Identifier("f"), predicateVersionFieldType())), @@ -192,6 +190,7 @@ class QuantifiedPermModule(val verifier: Verifier) } else { Nil }) ++ + (if (verifier.respectFunctionPrecPermAmounts) Nil else ConstDecl(assumePermUpperBoundName, Bool)) ++ // good mask Func(goodMaskName, LocalVarDecl(maskName, maskType), Bool) ++ Axiom(Forall(stateModule.staticStateContributions(), @@ -246,8 +245,11 @@ class QuantifiedPermModule(val verifier: Verifier) def permType = NamedType(permTypeName) - override def assumePermUpperBounds: Stmt = { - Assume(assumePermUpperBound) + override def assumePermUpperBounds(doAssume: Boolean) : Stmt = { + if (doAssume) + Assume(assumePermUpperBound) + else + Assume(assumePermUpperBound.not) } def staticStateContributions(withHeap: Boolean, withPermissions: Boolean): Seq[LocalVarDecl] = if (withPermissions) Seq(LocalVarDecl(maskName, maskType)) else Seq() @@ -272,10 +274,10 @@ class QuantifiedPermModule(val verifier: Verifier) assertReadPermOnly = false } - override def setCheckReadPermissionOnlyState(readOnly: Boolean): Boolean = { - val oldState = assertReadPermOnly + override def setCheckReadPermissionOnly(readOnly: Boolean): Boolean = { + val oldValue = assertReadPermOnly assertReadPermOnly = readOnly - oldState + oldValue } override def usingOldState = stateModuleIsUsingOldState @@ -385,7 +387,13 @@ class QuantifiedPermModule(val verifier: Verifier) val permVar = LocalVar(Identifier("perm"), permType) if (assertReadPermOnly || !p.isInstanceOf[sil.WildcardPerm]) { - val prmTranslated = if (p.isInstanceOf[sil.WildcardPerm]) fullPerm else translatePerm(p) + val prmTranslated = if (p.isInstanceOf[sil.WildcardPerm]) { + // We are in a context where permission amounts do not matter, so we can safely translate a wildcard to + // a full permission. + fullPerm + } else { + translatePerm(p) + } if (assertReadPermOnly) { (permVar := prmTranslated) ++ Assert(permissionPositiveInternal(permVar, Some(p), true), error.dueTo(reasons.NegativePermission(p))) ++ @@ -834,8 +842,7 @@ class QuantifiedPermModule(val verifier: Verifier) val injectiveAssertion = Assert(Forall((translatedLocals ++ translatedLocals2), injectTrigger,injectiveCond ==> ineqExpr), err) val maskUpdateStmts = if (assertReadPermOnly) Nil else - CommentBlock("assume permission updates", permissionsMap ++ - independentResource) ++ + CommentBlock("assume permission updates", permissionsMap ++ independentResource) ++ CommentBlock("assume permission updates for independent locations ", independentLocations) ++ (mask := qpMask)