From c77420f1cf6eecb86472c45b2b1cfbe9f5fe91e8 Mon Sep 17 00:00:00 2001 From: Nick Date: Tue, 4 May 2021 12:23:33 +0200 Subject: [PATCH 1/2] Fixed wildcard encoding issue for QP --- .../modules/impls/QuantifiedPermModule.scala | 59 ++++++++++++++----- 1 file changed, 43 insertions(+), 16 deletions(-) diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala index 9707003e..d7ea6088 100644 --- a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala @@ -924,6 +924,7 @@ class QuantifiedPermModule(val verifier: Verifier) //Quantified Field Permission case sil.FieldAccessPredicate(fieldAccess@sil.FieldAccess(recv, f), perms) => // alpha renaming, to avoid clashes in context, use vFresh instead of v + var isWildcard = false val vsFresh = vs.map(v => env.makeUniquelyNamed(v)) vsFresh.foreach(vFresh => env.define(vFresh.localVar)) def renaming[E <: sil.Exp] = (e:E) => Expressions.renameVariables(e, vs.map(v => v.localVar), vsFresh.map (vFresh => vFresh.localVar)) @@ -936,8 +937,12 @@ class QuantifiedPermModule(val verifier: Verifier) val (translatedPerms, stmts) = { //define wildcard if necessary if (conservativeIsWildcardPermission(perms)) { + // Wildcards over quantified permissions should not be represented as a single existential fraction > 0. + // Representig them this way implies that all quantified fields have the same amount of permission which is not the + // correct abstraction + isWildcard = true; val w = LocalVar(Identifier("wildcard"), Real) - (w, LocalVarWhereDecl(w.name, w > noPerm) :: Havoc(w) :: Nil) + (w, Nil) } else { (translateExp(renamingPerms), Nil) } @@ -977,8 +982,15 @@ class QuantifiedPermModule(val verifier: Verifier) val assm1Rhs = (0 until invFuns.length).foldLeft(rangeFunRecvApp: Exp)((soFar, i) => BinExp(soFar, And, FuncApp(invFuns(i).name, Seq(translatedRecv), invFuns(i).typ) === translatedLocals(i).l)) - val invAssm1 = (Forall(translatedLocals, tr1, (translatedCond && permGt(translatedPerms, noPerm)) ==> assm1Rhs)) - val invAssm2 = Forall(Seq(obj), Trigger(invFuns.map(invFun => FuncApp(invFun.name, Seq(obj.l), invFun.typ))), ((condInv && permGt(permInv, noPerm))&&rangeFunApp) ==> (rcvInv === obj.l) ) + // wildcards are per definition positive, thus no need to check for positivity + val invAssm1 = + if (isWildcard) + (Forall(translatedLocals, tr1, translatedCond ==> assm1Rhs)) + else (Forall(translatedLocals, tr1, (translatedCond && permGt(translatedPerms, noPerm)) ==> assm1Rhs)) + val invAssm2 = + if (isWildcard) + Forall(Seq(obj), Trigger(invFuns.map(invFun => FuncApp(invFun.name, Seq(obj.l), invFun.typ))), (condInv && rangeFunApp) ==> (rcvInv === obj.l) ) + else Forall(Seq(obj), Trigger(invFuns.map(invFun => FuncApp(invFun.name, Seq(obj.l), invFun.typ))), ((condInv && permGt(permInv, noPerm))&&rangeFunApp) ==> (rcvInv === obj.l) ) //Define non-null Assumptions: val nonNullAssumptions = @@ -986,20 +998,37 @@ class QuantifiedPermModule(val verifier: Verifier) (translatedRecv !== translateNull) )) val translatedLocalVarDecl = vsFresh.map(vFresh => translateLocalVarDecl(vFresh)) - //permission should be >= 0 if the condition is satisfied + //permission should be >= 0 if the condition is satisfied val permPositive = Assume(Forall(translatedLocalVarDecl, tr1, translatedCond ==> permissionPositiveInternal(translatedPerms,None,true))) - //Define Permission to all locations of field f for locations where condition applies: add permission defined - val condTrueLocations = (((condInv && permGt(permInv, noPerm))&&rangeFunApp) ==> ((permGt(permInv, noPerm) ==> (rcvInv === obj.l)) && ( - (if (!usingOldState) { - ( currentPermission(qpMask,obj.l,translatedLocation) === curPerm + permInv ) - } else { - currentPermission(qpMask,obj.l,translatedLocation) === curPerm - } ) - )) ) - + //Define Permission to all locations of field f for locations where condition applies: add permission defined + val condTrueLocations = + if (isWildcard) ( + // for wildcards + (condInv && rangeFunApp) ==> + ((rcvInv === obj.l) && ( + if (!usingOldState) + permGt(currentPermission(qpMask,obj.l,translatedLocation), curPerm) + else + (currentPermission(qpMask,obj.l,translatedLocation) === curPerm) + )) + ) + else ( + // for non wildcards + ((condInv && permGt(permInv, noPerm))&&rangeFunApp) ==> + ((permGt(permInv, noPerm) ==> (rcvInv === obj.l)) && ( + if (!usingOldState) + (currentPermission(qpMask,obj.l,translatedLocation) === curPerm + permInv) + else + (currentPermission(qpMask,obj.l,translatedLocation) === curPerm) + )) + ) //Define Permission to all locations of field f for locations where condition does not applies: no change - val condFalseLocations = (((condInv && permGt(permInv, noPerm))&&rangeFunApp).not ==> (currentPermission(qpMask,obj.l,translatedLocation) === curPerm)) + val condFalseLocations = + if (isWildcard) + ((condInv && rangeFunApp).not ==> (currentPermission(qpMask,obj.l,translatedLocation) === curPerm)) + else + (((condInv && permGt(permInv, noPerm))&&rangeFunApp).not ==> (currentPermission(qpMask,obj.l,translatedLocation) === curPerm)) //Define Permissions to all independent locations: no change val independentLocations = Assume(Forall(Seq(obj,field), Trigger(currentPermission(obj.l,field.l))++ @@ -1090,8 +1119,6 @@ class QuantifiedPermModule(val verifier: Verifier) val conjoinedInverseAssumptions = eqExpr.foldLeft(TrueLit():Exp)((soFar,exp) => BinExp(soFar,And,exp)) val invAssm2 = Forall(freshFormalBoogieDecls, Trigger(invFunApps), ((condInv && permGt(permInv, noPerm)) && rangeFunApp) ==> conjoinedInverseAssumptions) - - //define arguments needed to describe map updates val formalPredicate = new PredicateAccess(freshFormalVars, predname) (predicate.pos, predicate.info, predicate.errT) val general_location = translateLocation(formalPredicate) From a311464c9e2c04fee0b74f8456784d8a71b6c6bc Mon Sep 17 00:00:00 2001 From: Thibault Date: Thu, 15 Jul 2021 17:58:14 +0200 Subject: [PATCH 2/2] Removed a trigger to solve incompleteness of known-folded permissions --- .../scala/viper/carbon/modules/impls/DefaultHeapModule.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala index ce831c5c..1afe532c 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala @@ -305,7 +305,8 @@ class DefaultHeapModule(val verifier: Verifier) MaybeCommentedDecl("Frame all locations with known folded permissions", Axiom(Forall( vars ++ Seq(predField), //Trigger(Seq(identicalFuncApp, lookup(h.l, nullLit, predicateMaskField(predField.l)), isPredicateField(predField.l))) ++ - Trigger(Seq(identicalFuncApp, lookup(eh.l, nullLit, predField.l), isPredicateField(predField.l))) /*++ + // Trigger(Seq(identicalFuncApp, lookup(eh.l, nullLit, predField.l), isPredicateField(predField.l))) /*++ + Trigger(Seq(identicalFuncApp, isPredicateField(predField.l))) /*++ Trigger(Seq(identicalFuncApp, lookup(eh.l, nullLit, predicateMaskField(predField.l)), isPredicateField(predField.l))) ++ (verifier.program.predicates map (pred => Trigger(Seq(identicalFuncApp, predicateTriggerAnyState(pred, predField.l), isPredicateField(predField.l))))