From 42c88501cccc8eee777c91e9e08364b102827ca1 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 31 Oct 2023 13:52:54 +0100 Subject: [PATCH 1/4] Support for @opaque() functions --- silver | 2 +- .../modules/impls/DefaultFuncPredModule.scala | 34 +++++++++++++------ 2 files changed, 25 insertions(+), 11 deletions(-) diff --git a/silver b/silver index 31c94df4..315fb241 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 31c94df4f9792046618d9b4db52444ffe9c7c988 +Subproject commit 315fb2418b4776962ce99ce3469f5f3896ec787e diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index 5ee2ee82..f47a235e 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -226,10 +226,21 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { override def dummyFuncApp(e: Exp): Exp = FuncApp(dummyTriggerName, Seq(e), Bool) override def translateFuncApp(fa: sil.FuncApp) = { - translateFuncApp(fa.funcname, heapModule.currentStateExps ++ (fa.args map translateExp), fa.typ) + val forceNonLimited = fa.info.getUniqueInfo[sil.AnnotationInfo] match { + case Some(ai) if ai.values.contains("reveal") => true + case _ => false + } + translateFuncApp(fa.funcname, heapModule.currentStateExps ++ (fa.args map translateExp), fa.typ, forceNonLimited) } - def translateFuncApp(fname : String, args: Seq[Exp], typ: sil.Type) = { - FuncApp(Identifier(fname), args, translateType(typ)) + + def translateFuncApp(fname : String, args: Seq[Exp], typ: sil.Type, forceNonLimited: Boolean) = { + val func = verifier.program.findFunction(fname) + val useLimited = !forceNonLimited && (func.info.getUniqueInfo[sil.AnnotationInfo] match { + case Some(ai) if ai.values.contains("opaque") => true + case _ => false + }) + val ident = if (useLimited) Identifier(fname + limitedPostfix) else Identifier(fname) + FuncApp(ident, args, translateType(typ)) } private def assumeFunctionsAbove(i: Int): Exp = @@ -247,7 +258,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { val height = heights(f.name) val heap = heapModule.staticStateContributions(true, true) val args = f.formalArgs map translateLocalVarDecl - val fapp = translateFuncApp(f.name, (heap ++ args) map (_.l), f.typ) + val fapp = translateFuncApp(f.name, (heap ++ args) map (_.l), f.typ, true) val precondition : Exp = f.pres.map(p => translateExp(Expressions.asBooleanExp(p).whenExhaling)) match { case Seq() => TrueLit() case Seq(p) => p @@ -302,10 +313,13 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { */ private def transformFuncAppsToLimitedOrTriggerForm(exp: Exp, heightToSkip : Int = -1, triggerForm: Boolean = false): Exp = { def transformer: PartialFunction[Exp, Option[Exp]] = { - case FuncApp(recf, recargs, t) if recf.namespace == fpNamespace && (heightToSkip == -1 || heights(recf.name) <= heightToSkip) => + case FuncApp(recf, recargs, t) if recf.namespace == fpNamespace && + (heightToSkip == -1 || heights(if (recf.name.endsWith(limitedPostfix)) recf.name.dropRight(limitedPostfix.length) else recf.name) <= heightToSkip) => + + val baseName = if (recf.name.endsWith(limitedPostfix)) recf.name.dropRight(limitedPostfix.length) else recf.name // change all function applications to use the limited form, and still go through all arguments if (triggerForm) - {val func = verifier.program.findFunction(recf.name) + {val func = verifier.program.findFunction(baseName) // This was an attempt to make triggering functions heap-independent. // But the problem is that, for soundness such a function cannot be equated with/substituted for // the original function application, and if nested inside further structure in a trigger, the @@ -319,9 +333,9 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { val frameExp : Exp = { getFunctionFrame(func, recargs)._1 // the declarations will be taken care of when the function is translated } - Some(FuncApp(Identifier(func.name + framePostfix), Seq(frameExp) ++ (recargs.tail /* drop Heap argument */ map (_.transform(transformer))), t)) + Some(FuncApp(Identifier(baseName + framePostfix), Seq(frameExp) ++ (recargs.tail /* drop Heap argument */ map (_.transform(transformer))), t)) - } else Some(FuncApp(Identifier(recf.name + limitedPostfix), recargs map (_.transform(transformer)), t)) + } else Some(FuncApp(Identifier(baseName + limitedPostfix), recargs map (_.transform(transformer)), t)) case Forall(vs,ts,e,tvs,w) => Some(Forall(vs,ts,e.transform(transformer),tvs,w)) // avoid recursing into the triggers of nested foralls (which will typically get translated via another call to this anyway) case Exists(vs,ts,e,w) => Some(Exists(vs,ts,e.transform(transformer),w)) // avoid recursing into the triggers of nested exists (which will typically get translated via another call to this anyway) @@ -334,7 +348,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { val height = heights(f.name) val heap = heapModule.staticStateContributions(true, true) val args = f.formalArgs map translateLocalVarDecl - val fapp = translateFuncApp(f.name, (heap ++ args) map (_.l), f.typ) + val fapp = translateFuncApp(f.name, (heap ++ args) map (_.l), f.typ, true) val precondition : Exp = f.pres.map(p => translateExp(Expressions.asBooleanExp(p).whenExhaling)) match { case Seq() => TrueLit() case Seq(p) => p @@ -387,7 +401,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { val func = Func(name, LocalVarDecl(Identifier("frame"), frameType) ++ realArgs, typ) val funcFrameInfo = getFunctionFrame(f, args map (_.l)) val funcApp = FuncApp(name, funcFrameInfo._1 ++ (realArgs map (_.l)), typ) - val funcApp2 = translateFuncApp(f.name, args map (_.l), f.typ) + val funcApp2 = translateFuncApp(f.name, args map (_.l), f.typ, true) val outerUnfoldings : Seq[Unfolding] = Functions.recursiveCallsAndSurroundingUnfoldings(f).map((pair) => pair._2.headOption).flatten //only include predicate accesses that do not refer to bound variables From b2230000f7364ea23cbb1ce16cb16fc130e3f6fe Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 1 Nov 2023 16:13:11 +0100 Subject: [PATCH 2/4] Disable predicate triggers for opaque functions --- silver | 2 +- .../viper/carbon/modules/impls/DefaultFuncPredModule.scala | 7 ++++++- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/silver b/silver index 315fb241..62dacc0f 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 315fb2418b4776962ce99ce3469f5f3896ec787e +Subproject commit 62dacc0f71d4204a6f6261ec12e008e40a13c91d diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index f47a235e..eab2c6c7 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -297,10 +297,15 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { case _ => None}.flatten } + // Do not use predicate triggers if the function is annotated as opaque + val usePredicateTriggers = f.info.getUniqueInfo[sil.AnnotationInfo] match { + case Some(ai) if ai.values.contains("opaque") => false + case _ => true + } Axiom(Forall( stateModule.staticStateContributions() ++ args, - Seq(Trigger(Seq(staticGoodState,fapp))) ++ (if (predicateTriggers.isEmpty) Seq() else Seq(Trigger(Seq(staticGoodState, triggerFuncStatelessApp(f,args map (_.l))) ++ predicateTriggers))), + Seq(Trigger(Seq(staticGoodState,fapp))) ++ (if (!usePredicateTriggers || predicateTriggers.isEmpty) Seq() else Seq(Trigger(Seq(staticGoodState, triggerFuncStatelessApp(f,args map (_.l))) ++ predicateTriggers))), (staticGoodState && assumeFunctionsAbove(height)) ==> (precondition ==> (fapp === body)) )) From 96de23fa1a8c14210bee56da0b44bea06b0529cd Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 24 Nov 2023 17:18:01 +0100 Subject: [PATCH 3/4] Added comment explaining assumption about limitedPostfix after code review. --- .../carbon/modules/impls/DefaultFuncPredModule.scala | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index eab2c6c7..863bff2d 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -55,6 +55,11 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { private val assumeFunctionsAbove: Const = Const(assumeFunctionsAboveName) private val specialRefName = Identifier("special_ref") private val specialRef = Const(specialRefName) + + /* limitedPostfix is appended to the actual function name to get the name of the limited function. + * It must be a string that cannot appear in Viper identifiers to ensure that we can easily check if a given identifier + * refers to the limited version of a function or not. + */ private val limitedPostfix = "'" private val triggerFuncPostfix = "#trigger" private val triggerFuncNoHeapPostfix = "#triggerStateless" @@ -319,6 +324,9 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { private def transformFuncAppsToLimitedOrTriggerForm(exp: Exp, heightToSkip : Int = -1, triggerForm: Boolean = false): Exp = { def transformer: PartialFunction[Exp, Option[Exp]] = { case FuncApp(recf, recargs, t) if recf.namespace == fpNamespace && + // recf might refer to a limited function already if the function was marked as opaque. + // In that case, we have to drop the limited postfix, since heights contains only the original function names. + // We assume that any name that ends with limitedPostfix refers to a limited function (see limitedPostfix above). (heightToSkip == -1 || heights(if (recf.name.endsWith(limitedPostfix)) recf.name.dropRight(limitedPostfix.length) else recf.name) <= heightToSkip) => val baseName = if (recf.name.endsWith(limitedPostfix)) recf.name.dropRight(limitedPostfix.length) else recf.name From 1385ffc9e4431bf7e55d72076024575fc02071c6 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 24 Nov 2023 17:19:39 +0100 Subject: [PATCH 4/4] Updated silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 62dacc0f..11ab30d8 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 62dacc0f71d4204a6f6261ec12e008e40a13c91d +Subproject commit 11ab30d8402a51fca41846ab88f514af6fb53170