Recursively traverse let expressions when inferring triggers, not just once (#890)

* Recursively traverse let expressions when inferring triggers, not just once

* Filter out triggers that become invalid because of let-replacement

* Made check to discard invalid triggers slightly more precise

Author: marcoeilers

src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala

@@ -167,10 +167,15 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
       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
+      var currentRelevantVars = vs
+      var varFinder = additionalRelevantVariables(currentRelevantVars, nestedBoundVars)
+      visit(toSearch){
+        case n if varFinder.isDefinedAt(n) =>
+          val newVars = varFinder.apply(n)
+          currentRelevantVars = (currentRelevantVars ++ newVars).distinct
+          varFinder = additionalRelevantVariables(currentRelevantVars, nestedBoundVars)
+      }
+      currentRelevantVars
     }
     val allRelevantVars = (vs ++ additionalRelevantVars).distinct
     val modifyTriggers = modifyPossibleTriggers(allRelevantVars)

src/main/scala/viper/silver/ast/utility/Triggers.scala

@@ -75,11 +75,16 @@ object Triggers {
           (ast.LabelledOld(exp, l)(exp.pos, exp.info, exp.errT), t._2, t._3)
         })
       case ast.Let(v, e, body) => results =>
-        results.flatten.map(t => {
+        results.flatten.flatMap(t => {
           val exp = t._1
+          val varIsUsed = body.contains(v.localVar)
           val coveredVars = t._2.filter(cv => cv != v.localVar) ++
-            (if (body.contains(v.localVar)) relevantVars.filter(rv => e.contains(rv)) else Seq())
-          (exp.replace(v.localVar, e), coveredVars, t._3)
+            (if (varIsUsed) relevantVars.filter(rv => e.contains(rv)) else Seq())
+          if (varIsUsed && isForbiddenInTrigger(e)) {
+            None
+          } else {
+            Some((exp.replace(v.localVar, e), coveredVars, t._3))
+          }
         })
     }
 

src/test/resources/all/issues/silicon/0926.vpr

@@ -1,3 +1,6 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 
 function fn(x: Ref, y: Ref): Int