Skip to content

Fixing invalid Boogie code for quantified predicates without parameters #541

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
marcoeilers merged 2 commits into from
Dec 30, 2024
Merged

Fixing invalid Boogie code for quantified predicates without parameters #541

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0ef49ad
Fixing invalid Boogie code for quantified predicates without parameters
marcoeilers Dec 28, 2024
8746032
Update silver
marcoeilers Dec 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion silver
Open in desktop
Submodule silver updated 1 files
+18 −0 src/test/resources/all/issues/carbon/0391.vpr
20 changes: 7 additions & 13 deletions src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand All @@ -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
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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)
})

/*
Expand Down
⚡