From 077599f05fcc3e355b34b0f46dbe6643f7dfb29a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 21 Oct 2023 21:19:27 +0200 Subject: [PATCH 1/6] Experimental opaque functions via annotation --- src/main/scala/rules/Evaluator.scala | 11 ++++++++++- .../HeapAccessReplacingExpressionTranslator.scala | 12 +++++++++++- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index c7cf4dc80..43b46e5d3 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -768,7 +768,16 @@ object evaluator extends EvaluationRules { val snap1 = snap.convert(sorts.Snap) val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs) v3.decider.assume(preFApp) - val tFApp = App(v3.symbolConverter.toFunction(func), snap1 :: tArgs) + val funcAnn = func.info.getUniqueInfo[AnnotationInfo] + val tFApp = funcAnn match { + case Some(a) if a.values.contains("opaque") => + val funcAppAnn = fapp.info.getUniqueInfo[AnnotationInfo] + funcAppAnn match { + case Some(a) if a.values.contains("useDef") => App(v3.symbolConverter.toFunction(func), snap1 :: tArgs) + case _ => App(functionSupporter.limitedVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs) + } + case _ => App(v3.symbolConverter.toFunction(func), snap1 :: tArgs) + } val fr5 = s4.functionRecorder.changeDepthBy(-1) .recordSnapshot(fapp, v3.decider.pcs.branchConditions, snap1) diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala index 81aa923a1..8258879ea 100644 --- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala +++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala @@ -15,6 +15,7 @@ import viper.silicon.rules.functionSupporter import viper.silicon.state.{Identifier, SimpleIdentifier, SuffixedIdentifier, SymbolConverter} import viper.silicon.state.terms._ import viper.silicon.supporters.ExpressionTranslator +import viper.silver.ast.AnnotationInfo import viper.silver.reporter.{InternalWarningMessage, Reporter} class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter, @@ -127,7 +128,16 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter, case eFApp: ast.FuncApp => val silverFunc = program.findFunction(eFApp.funcname) - val fun = symbolConverter.toFunction(silverFunc) + val funcAnn = silverFunc.info.getUniqueInfo[AnnotationInfo] + val fun = funcAnn match { + case Some(a) if a.values.contains("opaque") => + val funcAppAnn = eFApp.info.getUniqueInfo[AnnotationInfo] + funcAppAnn match { + case Some(a) if a.values.contains("useDef") => symbolConverter.toFunction(silverFunc) + case _ => functionSupporter.limitedVersion(symbolConverter.toFunction(silverFunc)) + } + case _ => symbolConverter.toFunction(silverFunc) + } val args = eFApp.args map (arg => translate(arg)) val snap = getOrFail(data.fappToSnap, eFApp, sorts.Snap) val fapp = App(fun, snap +: args) From 7dd8a62c1c81bce4636f124ef32575eb3576778a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 21 Oct 2023 21:26:05 +0200 Subject: [PATCH 2/6] Omitting predicate triggers for opaque functions --- src/main/scala/supporters/functions/FunctionData.scala | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala index 7e0b3cab2..0ac3d6b48 100644 --- a/src/main/scala/supporters/functions/FunctionData.scala +++ b/src/main/scala/supporters/functions/FunctionData.scala @@ -259,9 +259,13 @@ class FunctionData(val programFunction: ast.Function, val pre = preconditionFunctionApplication val nestedDefinitionalAxioms = generateNestedDefinitionalAxioms val body = And(nestedDefinitionalAxioms ++ List(Implies(pre, And(functionApplication === translatedBody)))) + val funcAnn = programFunction.info.getUniqueInfo[ast.AnnotationInfo] + val actualPredicateTriggers = funcAnn match { + case Some(a) if a.values.contains("opaque") => Seq() + case _ => predicateTriggers.values.map(pt => Trigger(Seq(triggerFunctionApplication, pt))) + } val allTriggers = ( - Seq(Trigger(functionApplication)) - ++ predicateTriggers.values.map(pt => Trigger(Seq(triggerFunctionApplication, pt)))) + Seq(Trigger(functionApplication)) ++ actualPredicateTriggers) Forall(arguments, body, allTriggers)}) } From afa3f0886426b29d5ab5b70efab1b70cc06e3083 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 31 Oct 2023 13:27:24 +0100 Subject: [PATCH 3/6] Renamed @useDef() to @reveal() --- src/main/scala/rules/Evaluator.scala | 2 +- .../functions/HeapAccessReplacingExpressionTranslator.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 43b46e5d3..1797162c0 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -773,7 +773,7 @@ object evaluator extends EvaluationRules { case Some(a) if a.values.contains("opaque") => val funcAppAnn = fapp.info.getUniqueInfo[AnnotationInfo] funcAppAnn match { - case Some(a) if a.values.contains("useDef") => App(v3.symbolConverter.toFunction(func), snap1 :: tArgs) + case Some(a) if a.values.contains("reveal") => App(v3.symbolConverter.toFunction(func), snap1 :: tArgs) case _ => App(functionSupporter.limitedVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs) } case _ => App(v3.symbolConverter.toFunction(func), snap1 :: tArgs) diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala index 8258879ea..5235f31de 100644 --- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala +++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala @@ -133,7 +133,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter, case Some(a) if a.values.contains("opaque") => val funcAppAnn = eFApp.info.getUniqueInfo[AnnotationInfo] funcAppAnn match { - case Some(a) if a.values.contains("useDef") => symbolConverter.toFunction(silverFunc) + case Some(a) if a.values.contains("reveal") => symbolConverter.toFunction(silverFunc) case _ => functionSupporter.limitedVersion(symbolConverter.toFunction(silverFunc)) } case _ => symbolConverter.toFunction(silverFunc) From 44ec0fcf151e0b434f063d0dd787df956df5a486 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 31 Oct 2023 13:29:02 +0100 Subject: [PATCH 4/6] New test in silver repository --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index ce5523d0c..d43db152c 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit ce5523d0c902f5ff61c8af49f80cd180f758c5b5 +Subproject commit d43db152cf930e4e1c6b79fd1fc67837c93829b7 From 0148cb1e6774c89d69c924378cf357f006b965ab Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 1 Nov 2023 09:31:22 +0100 Subject: [PATCH 5/6] Updated silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index d43db152c..315fb2418 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit d43db152cf930e4e1c6b79fd1fc67837c93829b7 +Subproject commit 315fb2418b4776962ce99ce3469f5f3896ec787e From f0f8ee99f4e1a2cc76380d200fdfb1806ada0dc6 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 1 Nov 2023 16:13:52 +0100 Subject: [PATCH 6/6] Updated silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 315fb2418..62dacc0f7 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 315fb2418b4776962ce99ce3469f5f3896ec787e +Subproject commit 62dacc0f71d4204a6f6261ec12e008e40a13c91d