From 165d0bf89b0bdfa535f15a9b6407c5f671752698 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 8 Nov 2023 21:28:39 +0100 Subject: [PATCH 1/2] Properly treating let-expressions when generating triggers (in a hopefully generic way) --- .../ast/utility/GenericTriggerGenerator.scala | 20 ++++++++++++++++--- .../viper/silver/ast/utility/Triggers.scala | 13 +++++++++++- src/test/resources/all/issues/silver/0751.vpr | 15 ++++++++++++++ 3 files changed, 44 insertions(+), 4 deletions(-) create mode 100644 src/test/resources/all/issues/silver/0751.vpr diff --git a/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala b/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala index 35f98c242..ec75b7c5e 100644 --- a/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala +++ b/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala @@ -165,6 +165,15 @@ abstract class GenericTriggerGenerator[Node <: AnyRef, val nestedBoundVars: Seq[Var] = deepCollect(toSearch){ case qe: Quantification => Quantification_vars(qe)}.flatten + val additionalRelevantVars: Seq[Var] = { + val additionalVarFinder = additionalRelevantVariables(vs, nestedBoundVars) + deepCollect(toSearch){ + case n if additionalVarFinder.isDefinedAt(n) => additionalVarFinder(n) + }.flatten + } + val allRelevantVars = (vs ++ additionalRelevantVars).distinct + val modifyTriggers = modifyPossibleTriggers(allRelevantVars) + /* Get all function applications */ reduceTree(toSearch)((node: Node, results: Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]]) => node match { case possibleTrigger: PossibleTrigger if isPossibleTrigger(possibleTrigger) => @@ -187,7 +196,7 @@ abstract class GenericTriggerGenerator[Node <: AnyRef, processedArgs foreach (arg => visit(arg) { case v: Var => if (nestedBoundVars.contains(v)) containsNestedBoundVars = true - if (vs.contains(v)) containedVars +:= v + if (allRelevantVars.contains(v)) containedVars +:= v }) if (!containsNestedBoundVars && containedVars.nonEmpty) @@ -195,7 +204,7 @@ abstract class GenericTriggerGenerator[Node <: AnyRef, else results.flatten - case e if modifyPossibleTriggers.isDefinedAt(e) => modifyPossibleTriggers.apply(e)(results) + case e if modifyTriggers.isDefinedAt(e) => modifyTriggers.apply(e)(results) case _ => results.flatten }) @@ -205,9 +214,14 @@ abstract class GenericTriggerGenerator[Node <: AnyRef, * Hook for clients to add more cases to getFunctionAppsContaining to modify the found possible triggers. * Used e.g. to wrap trigger expressions inferred from inside old-expression into old() */ - def modifyPossibleTriggers: PartialFunction[Node, Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] => + def modifyPossibleTriggers(relevantVars: Seq[Var]): PartialFunction[Node, Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] => Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] = PartialFunction.empty + /* + * Hook for clients to identify additional variables which can be covered by triggers. + */ + def additionalRelevantVariables(relevantVars: Seq[Var], varsToAvoid: Seq[Var]): PartialFunction[Node, Seq[Var]] = PartialFunction.empty + /* Precondition: if vars is non-empty then every (f,vs) pair in functs * satisfies the property that vars and vs are not disjoint. * diff --git a/src/main/scala/viper/silver/ast/utility/Triggers.scala b/src/main/scala/viper/silver/ast/utility/Triggers.scala index 93b89e609..0516b0ffb 100644 --- a/src/main/scala/viper/silver/ast/utility/Triggers.scala +++ b/src/main/scala/viper/silver/ast/utility/Triggers.scala @@ -58,7 +58,7 @@ object Triggers { case _ => sys.error(s"Unexpected expression $e") } - override def modifyPossibleTriggers = { + override def modifyPossibleTriggers(relevantVars: Seq[LocalVar]) = { case ast.Old(_) => results => results.flatten.map(t => { val exp = t._1 @@ -69,6 +69,17 @@ object Triggers { val exp = t._1 (ast.LabelledOld(exp, l)(exp.pos, exp.info, exp.errT), t._2, t._3) }) + case ast.Let(v, e, _) => results => + results.flatten.map(t => { + val exp = t._1 + val coveredVars = t._2.filter(cv => cv != v.localVar) ++ relevantVars.filter(rv => e.contains(rv)) + (exp.replace(v.localVar, e), coveredVars, t._3) + }) + } + + override def additionalRelevantVariables(relevantVars: Seq[LocalVar], varsToAvoid: Seq[LocalVar]): PartialFunction[Node, Seq[LocalVar]] = { + case ast.Let(v, e, _) if relevantVars.exists(v => e.contains(v)) && varsToAvoid.forall(v => !e.contains(v)) => + Seq(v.localVar) } } diff --git a/src/test/resources/all/issues/silver/0751.vpr b/src/test/resources/all/issues/silver/0751.vpr new file mode 100644 index 000000000..a5c8bb0cd --- /dev/null +++ b/src/test/resources/all/issues/silver/0751.vpr @@ -0,0 +1,15 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +method main() { + assume forall qvar: Int :: + let alias == (qvar) in + f_get(alias) == f_clamp() + assert f_get(10) == 0 +} + +function f_get(idx: Int): Int + + +function f_clamp(): Int + ensures result == 0 \ No newline at end of file From c7ed3b916279e27f50433e226b0f9ee64372d1c0 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 8 Nov 2023 21:42:31 +0100 Subject: [PATCH 2/2] Slightly extended test to cover a case that needs an adjustment in Silicon --- src/test/resources/all/issues/silver/0751.vpr | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/test/resources/all/issues/silver/0751.vpr b/src/test/resources/all/issues/silver/0751.vpr index a5c8bb0cd..b5469d8bb 100644 --- a/src/test/resources/all/issues/silver/0751.vpr +++ b/src/test/resources/all/issues/silver/0751.vpr @@ -4,12 +4,23 @@ method main() { assume forall qvar: Int :: let alias == (qvar) in - f_get(alias) == f_clamp() + f_get(alias) == f_clamp() assert f_get(10) == 0 } function f_get(idx: Int): Int +method main2() { + assume forall qvar: Int :: qvar > 0 ==> + let alias == (qvar) in + f_get2(alias) == f_clamp() + assert f_get2(10) == 0 +} + +function f_get2(idx: Int): Int + requires idx > -5 + + function f_clamp(): Int ensures result == 0 \ No newline at end of file