Also added ForbiddenInTrigger functionality to extension expressions

Author: marcoeilers

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

@@ -1290,13 +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
 }

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

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

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

@@ -295,6 +295,11 @@ object Expressions {
     leftConds ++ guardedRightConds
   }
 
+  def isForbiddenInTrigger: PartialFunction[Node, Unit] = {
+    case _: ForbiddenInTrigger =>
+    case ee: ExtensionExp if ee.extensionIsForbiddenInTrigger() =>
+  }
+
   /** 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)

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

@@ -39,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.isDefinedAt(e) => true
       case _ => false
     }: PartialFunction[Exp, Boolean])(e)
 

Diff for: 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}
 
 /**
@@ -207,7 +207,9 @@ case class AdtConstructorApp(name: String, args: Seq[Exp], typVarMap: Map[TypeVa
     }
   }
 
-  override def extensionIsValidTrigger(): Boolean = args.forall(a => !a.existsDefined {case _: ForbiddenInTrigger => })
+  override def extensionIsValidTrigger(): Boolean = args.forall(a => !a.existsDefined(Expressions.isForbiddenInTrigger))
+
+  override def extensionIsForbiddenInTrigger(): Boolean = false
 }
 
 object AdtConstructorApp {
@@ -256,7 +258,9 @@ case class AdtDestructorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type
     }
   }
 
-  override def extensionIsValidTrigger(): Boolean = !rcv.existsDefined {case _: ForbiddenInTrigger => }
+  override def extensionIsValidTrigger(): Boolean = !rcv.existsDefined(Expressions.isForbiddenInTrigger)
+
+  override def extensionIsForbiddenInTrigger(): Boolean = false
 }
 
 object AdtDestructorApp {
@@ -310,7 +314,9 @@ case class AdtDiscriminatorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, T
     }
   }
 
-  override def extensionIsValidTrigger(): Boolean = !rcv.existsDefined {case _: ForbiddenInTrigger => }
+  override def extensionIsValidTrigger(): Boolean = !rcv.existsDefined(Expressions.isForbiddenInTrigger)
+
+  override def extensionIsForbiddenInTrigger(): Boolean = false
 }
 
 object AdtDiscriminatorApp {