Fixing issue #849 by letting extension expressions declare whether they are valid triggers

Author: marcoeilers

src/main/scala/viper/silver/ast/Expression.scala

@@ -1290,10 +1290,20 @@ sealed trait Lhs extends Exp
   * reach the backend verifiers. */
 trait ExtensionExp extends Exp {
   def extensionIsPure: Boolean
+
   def extensionSubnodes: Seq[Node]
+
   def typ: Type
+
   def verifyExtExp(): VerificationResult
+
   /** Pretty printing functionality as defined for other nodes in class FastPrettyPrinter.
-    * Sample implementation would be text("old") <> parens(show(e)) for pretty-printing an old-expression.*/
+    * Sample implementation would be text("old") <> parens(show(e)) for pretty-printing an old-expression. */
   def prettyPrint: PrettyPrintPrimitives#Cont
+
+  /** Defines whether this expression can be used as a trigger. Defaults to false. */
+  def extensionIsValidTrigger(): Boolean = false
+
+  /** Defines whether this expression is forbidden from occurring *anywhere* in a trigger. Defaults to true.  */
+  def extensionIsForbiddenInTrigger(): Boolean = true
 }

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

@@ -269,8 +269,9 @@ object Consistency {
     e match {
       case Old(nested) => validTrigger(nested, program) // case corresponds to OldTrigger node
       case LabelledOld(nested, _) => validTrigger(nested, program)
-      case wand: MagicWand => wand.subexpressionsToEvaluate(program).forall(e => !e.existsDefined {case _: ForbiddenInTrigger => })
-      case _ : PossibleTrigger | _: FieldAccess | _: PredicateAccess => !e.existsDefined { case _: ForbiddenInTrigger => }
+      case ee: ExtensionExp => ee.extensionIsValidTrigger()
+      case wand: MagicWand => wand.subexpressionsToEvaluate(program).forall(e => !e.exists(Expressions.isForbiddenInTrigger))
+      case _ : PossibleTrigger | _: FieldAccess | _: PredicateAccess => !e.exists(Expressions.isForbiddenInTrigger)
       case _ => false
     }
   }

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

@@ -295,6 +295,12 @@ object Expressions {
     leftConds ++ guardedRightConds
   }
 
+  def isForbiddenInTrigger(n: Node): Boolean = n match {
+    case _: ForbiddenInTrigger => true
+    case ee: ExtensionExp => ee.extensionIsForbiddenInTrigger()
+    case _ => false
+  }
+
   /** See [[viper.silver.ast.utility.Triggers.TriggerGeneration.generateTriggerSetGroups]] */
   def generateTriggerGroups(exp: QuantifiedExp, tg: TriggerGeneration = DefaultTriggerGeneration): Seq[(Seq[tg.TriggerSet], Seq[LocalVarDecl])] = {
     tg.generateTriggerSetGroups(exp.variables map (_.localVar), exp.exp)

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

@@ -30,6 +30,7 @@ object Triggers {
     /* True iff the given node is a possible trigger */
     protected def isPossibleTrigger(e: Exp): Boolean = (customIsPossibleTrigger orElse {
       case _: PossibleTrigger => true
+      case ee: ExtensionExp => ee.extensionIsValidTrigger()
       case Old(_: PossibleTrigger) => true
       case LabelledOld(_: PossibleTrigger, _) => true
       case _ => false
@@ -38,7 +39,7 @@ object Triggers {
     /* Note: If Add and Sub were type arguments of GenericTriggerGenerator, the latter
      *       could implement isForbiddenInTrigger already */
     def isForbiddenInTrigger(e: Exp) = (customIsForbiddenInTrigger orElse {
-      case _: ForbiddenInTrigger => true
+      case e if Expressions.isForbiddenInTrigger(e) => true
       case _ => false
     }: PartialFunction[Exp, Boolean])(e)
 

src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala

@@ -9,7 +9,7 @@ package viper.silver.plugin.standard.adt
 import viper.silver.ast._
 import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, braces, brackets, char, defaultIndent, line, nest, nil, parens, show, showType, showVars, space, ssep, text}
 import viper.silver.ast.pretty.PrettyPrintPrimitives
-import viper.silver.ast.utility.Consistency
+import viper.silver.ast.utility.{Consistency, Expressions}
 import viper.silver.verifier.{ConsistencyError, Failure, VerificationResult}
 
 /**
@@ -206,6 +206,10 @@ case class AdtConstructorApp(name: String, args: Seq[Exp], typVarMap: Map[TypeVa
       AdtConstructorApp(first, second, third)(this.pos, this.info, this.typ, this.adtName, this.errT).asInstanceOf[this.type]
     }
   }
+
+  override def extensionIsValidTrigger(): Boolean = args.forall(a => !a.exists(Expressions.isForbiddenInTrigger))
+
+  override def extensionIsForbiddenInTrigger(): Boolean = false
 }
 
 object AdtConstructorApp {
@@ -253,6 +257,10 @@ case class AdtDestructorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type
       AdtDestructorApp(first, second, third)(this.pos, this.info, this.typ, this.adtName, this.errT).asInstanceOf[this.type]
     }
   }
+
+  override def extensionIsValidTrigger(): Boolean = !rcv.exists(Expressions.isForbiddenInTrigger)
+
+  override def extensionIsForbiddenInTrigger(): Boolean = false
 }
 
 object AdtDestructorApp {
@@ -306,6 +314,11 @@ case class AdtDiscriminatorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, T
     }
   }
 
+  // Since a discriminator desugars to ADT_tag(rcv) == name_tag, which contains an equality,
+  // it cannot be used anywhere inside a trigger.
+  override def extensionIsValidTrigger(): Boolean = false
+
+  override def extensionIsForbiddenInTrigger(): Boolean = true
 }
 
 object AdtDiscriminatorApp {

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

@@ -0,0 +1,54 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+adt Term {
+  Const(n: Int)
+}
+
+domain theory {
+  function foo(t: Term): Bool
+
+  axiom ax1 { forall n: Int ::
+    {Const(n)}      // Type checker error
+    {foo(Const(n))} // OK
+    foo(Const(n))
+  }
+}
+
+method testConstr(s: Set[Int], j: Int) {
+  assume j in s
+  assume forall i: Int :: {Const(i)} i in s ==> i > 0
+  var t: Term := Const(j)
+  assert j > 0
+}
+
+method testConstrF(s: Set[Int], j: Int) {
+  assume j in s
+  assume forall i: Int :: {Const(i)} i in s ==> i > 0
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert j > 0
+}
+
+method testDestr(s: Set[Term], c: Term) {
+  assume c in s
+  assume forall i: Term :: {i.n} i in s ==> foo(i)
+  var t: Int := c.n
+  assert foo(c)
+}
+
+method testDestr2(s: Set[Term], c: Term) {
+  assume c in s
+  assume forall i: Term :: {i.n} i in s ==> foo(i)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert foo(c)
+}
+
+method testDiscr(s: Set[Term], c: Term) {
+  assume c in s
+  // i.isConst must not be picked as a trigger, otherwise the backends may crash
+  assume forall i: Term :: i.isConst ==> foo(i)
+  var t: Bool := c.isConst
+  assert foo(c)
+}
+

src/test/resources/all/issues/silver/0849_2.vpr

@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+adt Term {
+  Const(n: Int)
+}
+
+domain theory {
+  function foo(t: Term): Bool
+
+  axiom ax1 { forall n: Int ::
+    {Const(n)}      // Type checker error
+    {foo(Const(n))} // OK
+    foo(Const(n))
+  }
+}
+
+
+method testDiscr(s: Set[Term], c: Term) {
+  assume c in s
+  //:: ExpectedOutput(typechecker.error)
+  assume forall i: Term :: {i.isConst} i in s ==> foo(i)
+  assert foo(c)
+}