Merge pull request #753 from viperproject/meilers_fix_751

Properly treating let-expressions when generating triggers

Author: marcoeilers

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,15 +196,15 @@ 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)
           results.flatten ++ Seq((withArgs(possibleTrigger, processedArgs), containedVars, extraVars))
         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.
    *

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)
     }
   }
 

src/test/resources/all/issues/silver/0751.vpr

@@ -0,0 +1,26 @@
+// 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
+
+
+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