From 0ef49ad68d96a44c5057fb0034ef1cde7660f7b8 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Sat, 28 Dec 2024 17:52:51 +0100 Subject: [PATCH] Fixing invalid Boogie code for quantified predicates without parameters --- silver | 2 +- .../modules/impls/QuantifiedPermModule.scala | 20 +++++++------------ 2 files changed, 8 insertions(+), 14 deletions(-) diff --git a/silver b/silver index b9f72722..007f3454 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit b9f7272234d6c2a2b84e140979d1b282c74ecba1 +Subproject commit 007f3454b21cb081de0383d4bdd615211e044aae diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index 548cc095..de2a38f3 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -743,10 +743,10 @@ class QuantifiedPermModule(val verifier: Verifier) //for each argument, define the second inverse function val eqExpr = (argsInv zip freshFormalBoogieVars).map(x => x._1 === x._2) val conjoinedInverseAssumptions = eqExpr.foldLeft(TrueLit():Exp)((soFar,exp) => BinExp(soFar,And,exp)) - val invAssm2 = Forall(freshFormalBoogieDecls, Trigger(invFunApps), ((condInv && permGt(permInv, noPerm)) && rangeFunApp) ==> conjoinedInverseAssumptions) + val invAssm2 = MaybeForall(freshFormalBoogieDecls, Trigger(invFunApps), ((condInv && permGt(permInv, noPerm)) && rangeFunApp) ==> conjoinedInverseAssumptions) //check that the permission expression is non-negative for all predicates/wands satisfying the condition - val permPositive = Assert(Forall(freshFormalBoogieDecls, Trigger(invFunApps), (condInv && rangeFunApp) ==> permissionPositive(permInv, true)), + val permPositive = Assert(MaybeForall(freshFormalBoogieDecls, Trigger(invFunApps), (condInv && rangeFunApp) ==> permissionPositive(permInv, true)), error.dueTo(reasons.NegativePermission(perms))) //check that sufficient permission is held @@ -788,7 +788,7 @@ class QuantifiedPermModule(val verifier: Verifier) //trigger: val triggerForPermissionUpdateAxioms = Seq(Trigger(currentPermission(qpMask,translateNull, general_location)) /*,Trigger(currentPermission(mask, translateNull, general_location)),Trigger(invFunApp)*/ ) - val permissionsMap = Assume(Forall(freshFormalBoogieDecls,triggerForPermissionUpdateAxioms, ((condInv && (permGt(permInv, noPerm)) && rangeFunApp) ==> (conjoinedInverseAssumptions && (currentPermission(qpMask,translateNull, general_location) === currentPermission(translateNull, general_location) - permInv))))) + val permissionsMap = Assume(MaybeForall(freshFormalBoogieDecls,triggerForPermissionUpdateAxioms, ((condInv && (permGt(permInv, noPerm)) && rangeFunApp) ==> (conjoinedInverseAssumptions && (currentPermission(qpMask,translateNull, general_location) === currentPermission(translateNull, general_location) - permInv))))) //Assume no change for independent locations: different predicate/wand or different resource type val obj = LocalVarDecl(Identifier("o"), refType) @@ -804,7 +804,7 @@ class QuantifiedPermModule(val verifier: Verifier) ((obj.l !== translateNull) || isDifferentFieldType || hasWrongId) ==> (currentPermission(obj.l,field.l) === currentPermission(qpMask,obj.l,field.l)))) //same resource, but not satisfying the condition - val independentResource = Assume(Forall(freshFormalBoogieDecls, triggerForPermissionUpdateAxioms, ((condInv && (permGt(permInv, noPerm)) && rangeFunApp).not) ==> (currentPermission(qpMask,translateNull, general_location) === currentPermission(translateNull, general_location)))) + val independentResource = Assume(MaybeForall(freshFormalBoogieDecls, triggerForPermissionUpdateAxioms, ((condInv && (permGt(permInv, noPerm)) && rangeFunApp).not) ==> (currentPermission(qpMask,translateNull, general_location) === currentPermission(translateNull, general_location)))) //AS: TODO: it would be better to use the Boogie representation of a predicate/wand instance as the canonical representation here (i.e. the function mapping to a field in the Boogie heap); this would avoid the disjunction of arguments used below. In addition, this could be used as a candidate trigger in tr1 code above. See issue 242 @@ -1295,7 +1295,7 @@ class QuantifiedPermModule(val verifier: Verifier) //for each argument, define the second inverse function val eqExpr = (argsInv zip freshFormalBoogieVars).map(x => x._1 === x._2) val conjoinedInverseAssumptions = eqExpr.foldLeft(TrueLit():Exp)((soFar,exp) => BinExp(soFar,And,exp)) - val invAssm2 = Forall(freshFormalBoogieDecls, Trigger(invFunApps), ((condInv && permGt(permInv, noPerm)) && rangeFunApp) ==> conjoinedInverseAssumptions) + val invAssm2 = MaybeForall(freshFormalBoogieDecls, Trigger(invFunApps), ((condInv && permGt(permInv, noPerm)) && rangeFunApp) ==> conjoinedInverseAssumptions) //define arguments needed to describe map updates val general_location = accPred match { @@ -1323,19 +1323,13 @@ class QuantifiedPermModule(val verifier: Verifier) val permissionsMap = Assume( { val exp = ((condInv && permGt(permInv, noPerm)) && rangeFunApp) ==> ((permGt(permInv, noPerm) ==> conjoinedInverseAssumptions) && (currentPermission(qpMask,translateNull, general_location) === currentPermission(translateNull, general_location) + permInv)) - if (freshFormalBoogieDecls.isEmpty) - exp - else - Forall(freshFormalBoogieDecls,triggerForPermissionUpdateAxioms, exp) + MaybeForall(freshFormalBoogieDecls,triggerForPermissionUpdateAxioms, exp) }) //assumptions for predicates/wands of the same type which do not gain permission val independentResource = Assume( { val exp = (((condInv && permGt(permInv, noPerm)) && rangeFunApp).not) ==> (currentPermission(qpMask,translateNull, general_location) === currentPermission(translateNull, general_location)) - if (freshFormalBoogieDecls.isEmpty) - exp - else - Forall(freshFormalBoogieDecls, triggerForPermissionUpdateAxioms, exp) + MaybeForall(freshFormalBoogieDecls, triggerForPermissionUpdateAxioms, exp) }) /*