diff --git a/silver b/silver index 10b1b26a..aac52daa 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 10b1b26a20957e5f000bf1bbcd4017145148afd7 +Subproject commit aac52daab393e3ce98148e30ed54808aedd3af54 diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala index fc33d06a..f6c55489 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.respectFunctionPrePermAmounts.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/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/DefaultExpModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala index 73c7a296..ff81c55a 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala @@ -79,6 +79,7 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes case sil.Unfolding(_, exp) => translateExp(exp) case sil.Applying(_, exp) => translateExp(exp) + case sil.Asserting(_, exp) => translateExp(exp) case sil.Old(exp) => val prevState = stateModule.state stateModule.replaceState(stateModule.oldState) @@ -378,6 +379,13 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes checkDefinednessImpl(e1, error, makeChecks = makeChecks, definednessStateOpt) :: // short-circuiting evaluation: If(UnExp(Not, translateExp(e1)), checkDefinednessImpl(e2, error, makeChecks = makeChecks, definednessStateOpt), Statements.EmptyStmt) :: Nil + case sil.Asserting(assertion, e) => + val checkAssDefined = checkDefinedness(assertion, error, makeChecks = makeChecks) + val (stateStmt, state) = stateModule.freshTempState("asserting") + val checkAssHolds = MaybeComment("Exhale assertion of asserting", exhale(Seq((assertion, error, Some(error))))) + stateModule.replaceState(state) + val checkEDefined = checkDefinedness(e, error, makeChecks = makeChecks) + checkAssDefined :: stateStmt :: checkAssHolds :: checkEDefined :: Nil case w@sil.MagicWand(_, _) => checkDefinednessWand(w, error, makeChecks = makeChecks) case sil.Let(v, e, body) => diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index 80aa2975..0983ac2e 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(!verifier.respectFunctionPrecPermAmounts) 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 @@ -665,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 @@ -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 } } ) ++ @@ -961,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) } } @@ -998,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 109942f0..f8b610cd 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) @@ -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 96a075e0..130da0a9 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())), @@ -192,13 +198,13 @@ 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 ==> ( 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 ))) + ((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) @@ -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) => @@ -470,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)) @@ -546,8 +573,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 +636,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 +648,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 +743,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 +833,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 +846,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,11 +1046,12 @@ 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 - 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)) @@ -1171,7 +1209,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) @@ -1489,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) => 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 + }