Fixing several issues with malformed triggers (#827)

Author: marcoeilers

Diff for: src/main/scala/viper/silver/ast/Expression.scala

@@ -73,12 +73,12 @@ case class GtCmp(left: Exp, right: Exp)(val pos: Position = NoPosition, val info
 case class GeCmp(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(GeOp) with ForbiddenInTrigger
 
 // Equality and non-equality (defined for all types)
-case class EqCmp(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends EqualityCmp("==") {
+case class EqCmp(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends EqualityCmp("==") with ForbiddenInTrigger {
   override lazy val check : Seq[ConsistencyError] =
     Seq(left, right).flatMap(Consistency.checkPure) ++
     (if(left.typ != right.typ) Seq(ConsistencyError(s"expected the same type, but got ${left.typ} and ${right.typ}", left.pos)) else Seq())
 }
-case class NeCmp(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends EqualityCmp("!=") {
+case class NeCmp(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends EqualityCmp("!=") with ForbiddenInTrigger {
   override lazy val check : Seq[ConsistencyError] =
     Seq(left, right).flatMap(Consistency.checkPure) ++
     (if(left.typ != right.typ) Seq(ConsistencyError(s"expected the same type, but got ${left.typ} and ${right.typ}", left.pos)) else Seq())

Diff for: src/main/scala/viper/silver/ast/utility/Consistency.scala

@@ -235,8 +235,8 @@ object Consistency {
   /** checks that all quantified variables appear in all triggers */
   def checkAllVarsMentionedInTriggers(variables: Seq[LocalVarDecl], triggers: Seq[Trigger]) : Seq[ConsistencyError] = {
     var s = Seq.empty[ConsistencyError]
-    val varsInTriggers : Seq[Seq[LocalVar]] = triggers map(t=>{
-      t.deepCollect({case lv: LocalVar => lv})
+    val varsInTriggers : Seq[Set[LocalVar]] = triggers map(t=>{
+      Expressions.getContainedVariablesExcludingLet(t)
     })
     variables.foreach(v=>{
       varsInTriggers.foreach(varList=>{

Diff for: src/main/scala/viper/silver/ast/utility/Expressions.scala

@@ -136,6 +136,23 @@ object Expressions {
     }.flatten.toSet
   }
 
+  /** Collects all variables that are actually contained in the given node, filtering out let-variables
+    * as well as variables used in expressions bound to let-variables which are not used in the let body.  */
+  def getContainedVariablesExcludingLet(e: Node): Set[LocalVar] = {
+    Visitor.deepCollect[Node, Set[LocalVar]](Seq(e), {
+      case _: Let => Seq()
+      case n => Nodes.subnodes(n)
+    }) {
+      case lv: LocalVar => Set(lv)
+      case Let(v, e, body) =>
+        val bodyVars = getContainedVariablesExcludingLet(body)
+        if (bodyVars.contains(v.localVar))
+          bodyVars - v.localVar ++ getContainedVariablesExcludingLet(e)
+        else
+          bodyVars - v.localVar
+    }.flatten.toSet
+  }
+
   /** In an expression, rename a list (domain) of variables with given (range) variables. */
   def renameVariables[E <: Exp]
                      (exp: E, domain: Seq[AbstractLocalVar], range: Seq[AbstractLocalVar])

Diff for: src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala

@@ -8,6 +8,7 @@ package viper.silver.ast.utility
 
 import java.util.concurrent.atomic.AtomicInteger
 import reflect.ClassTag
+import scala.annotation.unused
 
 object GenericTriggerGenerator {
   case class TriggerSet[E](exps: Seq[E])
@@ -193,7 +194,7 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
         })
 
         /* Collect all the sought (vs) variables in the function application */
-        processedArgs foreach (arg => visit(arg) {
+        processedArgs foreach (arg => getVarsInExp(arg) foreach {
           case v: Var =>
             if (nestedBoundVars.contains(v)) containsNestedBoundVars = true
             if (allRelevantVars.contains(v)) containedVars +:= v
@@ -210,17 +211,25 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
     })
   }
 
+  def getVarsInExp(e: Exp): Set[Var] = {
+    var result: Set[Var] = Set()
+    visit(e) {
+      case v: Var => result += v
+    }
+    result
+  }
+
   /*
    * 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(relevantVars: Seq[Var]): PartialFunction[Node, Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] =>
+  def modifyPossibleTriggers(@unused 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
+  def additionalRelevantVariables(@unused relevantVars: Seq[Var], @unused 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 for: src/main/scala/viper/silver/ast/utility/Triggers.scala

@@ -58,6 +58,10 @@ object Triggers {
       case _ => sys.error(s"Unexpected expression $e")
     }
 
+    override def getVarsInExp(e: Exp): Set[LocalVar] = {
+      Expressions.getContainedVariablesExcludingLet(e)
+    }
+
     override def modifyPossibleTriggers(relevantVars: Seq[LocalVar]) = {
       case ast.Old(_) => results =>
         results.flatten.map(t => {
@@ -69,16 +73,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 =>
+      case ast.Let(v, e, body) => results =>
         results.flatten.map(t => {
           val exp = t._1
-          val coveredVars = t._2.filter(cv => cv != v.localVar) ++ relevantVars.filter(rv => e.contains(rv))
+          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)
         })
     }
 
     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)) =>
+      case ast.Let(v, e, body) if body.contains(v.localVar) && relevantVars.exists(v => e.contains(v)) && varsToAvoid.forall(v => !e.contains(v)) =>
         Seq(v.localVar)
     }
   }

Diff for: src/test/resources/all/issues/carbon/0406.vpr

@@ -1,3 +1,6 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Ref
 
 method m1() {

Diff for: src/test/resources/all/issues/carbon/0422.vpr

@@ -1,3 +1,6 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 method m1() {
   while (true) {
       goto bubble

Diff for: src/test/resources/all/issues/carbon/0489.vpr

@@ -0,0 +1,13 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+method test1()
+    ensures (forall q: Bool :: id(q == q))
+{}
+
+function id(a : Bool): Bool { a }
+
+
+method test3()
+  ensures (forall q: Int ::  id(let x == (q) in (true)))
+{}

Diff for: src/test/scala/ConsistencyTests.scala

@@ -263,6 +263,7 @@ class ConsistencyTests extends AnyFunSuite with Matchers {
     val f = Function("f", Seq(LocalVarDecl("i", Int)()), Int, Seq(), Seq(), None)()
     val forallNoVar = Forall(Seq(), Seq(), TrueLit()())()
     val forallUnusedVar = Forall(Seq(LocalVarDecl("i", Int)(), LocalVarDecl("j", Int)()), Seq(Trigger(Seq(FuncApp(f, Seq(LocalVar("j", Int)()))()))()), TrueLit()())()
+    val forallUnusedVarLet = Forall(Seq(LocalVarDecl("i", Int)()), Seq(Trigger(Seq(FuncApp(f, Seq(Let(LocalVarDecl("j", Int)(), LocalVar("i", Int)(), TrueLit()())()))()))()), TrueLit()())()
     val forallNoVarTrigger = Forall(Seq(LocalVarDecl("i", Int)()), Seq(Trigger(Seq(FuncApp(f, Seq(LocalVar("i", Int)()))(), FuncApp(f, Seq(IntLit(0)()))()))()), TrueLit()())()
 
     forallNoVar.checkTransitively shouldBe Seq(
@@ -273,6 +274,10 @@ class ConsistencyTests extends AnyFunSuite with Matchers {
       ConsistencyError("Variable i is not mentioned in one or more triggers.", NoPosition)
     )
 
+    forallUnusedVarLet.checkTransitively shouldBe Seq(
+      ConsistencyError("Variable i is not mentioned in one or more triggers.", NoPosition)
+    )
+
     forallNoVarTrigger.checkTransitively shouldBe Seq(
       ConsistencyError("Trigger expression f(0) does not contain any quantified variable.", NoPosition)
     )