Refactor BipOutgoingDataUnsatisfiablePrecondition into JavaAnnotation…

…Error

src/col/vct/col/ast/Node.scala

@@ -1120,7 +1120,7 @@ final case class BipGlueDataWire[G](dataOut: Ref[G, BipOutgoingData[G]], dataIn:
 
 sealed trait BipData[G] extends ClassDeclaration[G] with BipDataImpl[G]
 final class BipIncomingData[G](val t: Type[G])(implicit val o: Origin) extends BipData[G] with BipIncomingDataImpl[G]
-final class BipOutgoingData[G](val t: Type[G], val body: Statement[G], val pure: Boolean)(val blame: Blame[CallableFailure])(implicit val o: Origin) extends BipData[G] with BipOutgoingDataImpl[G]
+final class BipOutgoingData[G](val t: Type[G], val body: Statement[G], val pure: Boolean)(val blame: Blame[BipOutgoingDataPreconditionUnsatisfiable])(implicit val o: Origin) extends BipData[G] with BipOutgoingDataImpl[G]
 final case class BipLocalIncomingData[G](ref: Ref[G, BipIncomingData[G]])(implicit val o: Origin) extends Expr[G] with BipLocalIncomingDataImpl[G]
 
 final class BipStatePredicate[G](val expr: Expr[G])(implicit val o: Origin) extends ClassDeclaration[G] with BipStatePredicateImpl[G]

src/col/vct/col/origin/Blame.scala

@@ -675,7 +675,7 @@ case class BipTransitionPreconditionUnsatisfiable(node: BipTransition[_]) extend
   override def inlineDescWithSource(source: String): String = s"Precondition unsatisfiable for transition `$source`"
 }
 
-case class BipOutgoingDataPreconditionUnsatisfiable(node: BipOutgoingData[_]) extends BipTransitionFailure with NodeVerificationFailure {
+case class BipOutgoingDataPreconditionUnsatisfiable(node: BipOutgoingData[_]) extends JavaAnnotationFailure with NodeVerificationFailure {
   override def code: String = "bipOutgoingDataPreconditionUnsatisfiable"
   override def descInContext: String = "The precondition of this outgoing data is unsatisfiable"
 

src/rewrite/vct/rewrite/bip/EncodeBip.scala

@@ -88,11 +88,11 @@ case object EncodeBip extends RewriterBuilderArg[VerificationResults] {
 
     override def blame(error: NontrivialUnsatisfiable): Unit = node match {
       case g: BipGuard[_] => g.blame.blame(BipGuardPreconditionUnsatisfiable(g))
-      case t: BipTransition[_] =>
-        results.reportPreconditionNotVerified(t)
-        results.report(t, UpdateFunctionFailure)
-        t.blame.blame(BipTransitionPreconditionUnsatisfiable(t))
-      case t: BipOutgoingData[_] => t.blame.blame(BipOutgoingDataPreconditionUnsatisfiable(t))
+      case transition: BipTransition[_] =>
+        results.reportPreconditionNotVerified(transition)
+        results.report(transition, UpdateFunctionFailure)
+        transition.blame.blame(BipTransitionPreconditionUnsatisfiable(transition))
+      case data: BipOutgoingData[_] => data.blame.blame(BipOutgoingDataPreconditionUnsatisfiable(data))
       case _ => throw Unreachable("This blame is not constructed for other types of node.")
     }
   }

src/rewrite/vct/rewrite/lang/LangBipToCol.scala

@@ -122,9 +122,7 @@ case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
     data.ref
   }
 
-  def rewriteTransition(m: JavaMethod[Pre]): Unit = jad.BipTransition.get(m).foreach(rewriteTransition(m, _))
-
-  def rewriteTransition(m: JavaMethod[Pre], transition: jad.BipTransition[Pre]): Unit = {
+  def rewriteTransition(m: JavaMethod[Pre], annotation: JavaAnnotation[Pre], transition: jad.BipTransition[Pre]): Unit = {
     val jad.BipTransition(portName, source, target, guardText, guard, requires, ensures) = transition
 
     if (m.returnType != TVoid[Pre]()) { throw WrongTransitionReturnType(m) }
@@ -163,32 +161,28 @@ case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
     BipLocalIncomingData(javaParamSucc.ref[Post, BipIncomingData[Post]](decl))(local.o)
   }
 
-  def rewriteGuard(m: JavaMethod[Pre]): Unit = {
-    val annotation = jad.BipGuard.get(m).get
-    val Some(jad.BipGuard(_)) = annotation.data
-
-    if (m.returnType != TBool[Pre]()) { throw LangBipToCol.WrongGuardReturnType(m) }
+  def rewriteGuard(method: JavaMethod[Pre], annotation: JavaAnnotation[Pre], guard: jad.BipGuard[Pre]): Unit = {
+    if (method.returnType != TBool[Pre]()) { throw LangBipToCol.WrongGuardReturnType(method) }
 
-    javaMethodSuccGuard(m) = rw.classDeclarations.declare(new BipGuard[Post](
-      m.parameters.map(rewriteParameter),
-      rw.dispatch(m.body.get),
+    javaMethodSuccGuard(method) = rw.classDeclarations.declare(new BipGuard[Post](
+      method.parameters.map(rewriteParameter),
+      rw.dispatch(method.body.get),
       true
-    )(annotation.blame)(SourceNameOrigin(m.name, m.o)))
+    )(annotation.blame)(SourceNameOrigin(method.name, method.o)))
   }
 
-  def rewriteOutgoingData(m: JavaMethod[Pre]): Unit = {
-    val data @ jad.BipData(name) = jad.BipData.get(m).get
-    if (!jad.BipPure.isPure(m)) {
-      throw ImpureData(m);
+  def rewriteOutgoingData(method: JavaMethod[Pre], annotation: JavaAnnotation[Pre], data: jad.BipData[Pre]): Unit = {
+    if (!jad.BipPure.isPure(method)) {
+      throw ImpureData(method);
     }
 
-    javaMethodSuccOutgoingData(m) = rw.classDeclarations.declare(
+    javaMethodSuccOutgoingData(method) = rw.classDeclarations.declare(
       new BipOutgoingData(
-        rw.dispatch(m.returnType),
-        rw.dispatch(m.body.get),
-        jad.BipPure.isPure(m)
-      )(m.blame)(BipDataOrigin(rw.java.namespace.top, currentClass(), data)))
-    dataOut((currentClass(), name)) = javaMethodSuccOutgoingData(m)
+        rw.dispatch(method.returnType),
+        rw.dispatch(method.body.get),
+        jad.BipPure.isPure(method)
+      )(annotation.blame)(BipDataOrigin(rw.java.namespace.top, currentClass(), data)))
+    dataOut((currentClass(), data.name)) = javaMethodSuccOutgoingData(method)
   }
 
   def generateComponent(cls: JavaClass[Pre], constructors: Seq[Ref[Post, Procedure[Post]]]): Unit = {

src/rewrite/vct/rewrite/lang/LangJavaToCol.scala

@@ -11,7 +11,8 @@ import vct.col.rewrite.{Generation, Rewritten}
 import vct.col.util.AstBuildHelpers._
 import vct.col.util.SuccessionMap
 import RewriteHelpers._
-import vct.col.resolve.lang.Java
+import vct.col.ast.lang.JavaAnnotationEx
+import vct.col.resolve.lang.{Java, JavaAnnotationData}
 import vct.col.resolve.lang.JavaAnnotationData.{BipComponent, BipData, BipGuard, BipTransition}
 import vct.result.VerificationError.{Unreachable, UserError}
 
@@ -245,13 +246,17 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends
           ))
         }
       case method: JavaMethod[Pre] =>
-        if (BipTransition.get(method).nonEmpty) {
-          rw.bip.rewriteTransition(method)
-        } else if (BipGuard.get(method).isDefined) {
-          rw.bip.rewriteGuard(method)
-        } else if (BipData.get(method).isDefined) {
-          rw.bip.rewriteOutgoingData(method)
-        } else {
+        // For each javabip annotation that we encounter, execute a rewrite
+        val results = method.modifiers.collect {
+          case annotation @ JavaAnnotationEx(_, _, guard @ JavaAnnotationData.BipGuard(_)) =>
+            rw.bip.rewriteGuard(method, annotation, guard)
+          case annotation @ JavaAnnotationEx(_, _, transition : JavaAnnotationData.BipTransition[Pre]) =>
+            rw.bip.rewriteTransition(method, annotation, transition)
+          case annotation @ JavaAnnotationEx(_, _, data: JavaAnnotationData.BipData[Pre]) =>
+            rw.bip.rewriteOutgoingData(method, annotation, data)
+        }
+        // If no rewrites were triggered, it must be a regular java method, so execute the default rewrite
+        if (results.isEmpty) {
           rw.dispatch(method)
         }