Skip to content

Opaque function annotation #474

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 5 commits into from
Nov 24, 2023
Merged

Opaque function annotation #474

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
42c8850
Support for @opaque() functions
marcoeilers Oct 31, 2023
b223000
Disable predicate triggers for opaque functions
marcoeilers Nov 1, 2023
96de23f
Added comment explaining assumption about limitedPostfix after code r…
marcoeilers Nov 24, 2023
1385ffc
Updated silver
marcoeilers Nov 24, 2023
27404f9
Merge
marcoeilers Nov 24, 2023
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
+337 −0 src/test/resources/all/annotation/opaque.vpr
41 changes: 30 additions & 11 deletions src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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
Expand Down Expand Up @@ -286,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))
))
Expand All @@ -302,10 +318,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) =>
Comment thread
marcoeilers marked this conversation as resolved.

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
Expand All @@ -319,9 +338,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)
Expand All @@ -334,7 +353,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
Expand Down Expand Up @@ -387,7 +406,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
Expand Down
⚡