Factor bip guard precondition unsatisfiable error into a java annotat…

…ion error

examples/technical/javabip/BipGuardUnsatisfiablePrecondition.java → examples/technical/javabip/BipGuardPreconditionUnsatisfiable.java

@@ -20,11 +20,11 @@ public class GuardIsUsed {
     }
 
     @Pure
-    @Guard(name = GEQ_Y)
     /*[/expect bipGuardPreconditionUnsatisfiable]*/
+    @Guard(name = GEQ_Y)
+    /*[/end]*/
     public boolean geqZero() {
         return true;
     }
-    /*[/end]*/
 }
 /*[/end]*/

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

@@ -1131,7 +1131,7 @@ final class BipTransition[G](val signature: BipTransitionSignature[G],
                              val data: Seq[Ref[G, BipIncomingData[G]]], val guard: Expr[G],
                              val requires: Expr[G], val ensures: Expr[G], val body: Statement[G]
                             )(val blame: Blame[BipTransitionFailure])(implicit val o: Origin) extends ClassDeclaration[G] with BipTransitionImpl[G]
-final class BipGuard[G](val data: Seq[Ref[G, BipIncomingData[G]]], val body: Statement[G], val pure: Boolean)(val blame: Blame[BipGuardNontrivialUnsatisfiable])(implicit val o: Origin) extends ClassDeclaration[G] with BipGuardImpl[G]
+final class BipGuard[G](val data: Seq[Ref[G, BipIncomingData[G]]], val body: Statement[G], val pure: Boolean)(val blame: Blame[BipGuardPreconditionUnsatisfiable])(implicit val o: Origin) extends ClassDeclaration[G] with BipGuardImpl[G]
 final case class BipGuardInvocation[G](obj: Expr[G], guard: Ref[G, BipGuard[G]])(implicit val o: Origin) extends Expr[G] with BipGuardInvocationImpl[G]
 final class BipComponent[G](val fqn: Seq[String], val constructors: Seq[Ref[G, Procedure[G]]], val invariant: Expr[G],
                             val initial: Ref[G, BipStatePredicate[G]])(implicit val o: Origin) extends ClassDeclaration[G] with BipComponentImpl[G]

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

@@ -682,8 +682,8 @@ case class BipOutgoingDataPreconditionUnsatisfiable(node: BipOutgoingData[_]) ex
   override def inlineDescWithSource(source: String): String = s"Precondition unsatisfiable for outgoing data `$source`"
 }
 
-case class BipGuardNontrivialUnsatisfiable(node: BipGuard[_]) extends NodeVerificationFailure {
-  override def code: String = "bipGuardNontrivialUnsatisfiable"
+case class BipGuardPreconditionUnsatisfiable(node: BipGuard[_]) extends JavaAnnotationFailure with NodeVerificationFailure {
+  override def code: String = "bipGuardPreconditionUnsatisfiable"
   override def descInContext: String = "The precondition of this guard (consisting of only the component invariant) is unsatisfiable"
   override def inlineDescWithSource(source: String): String = s"Precondition unsatisfiable for guard `$source`"
 }

src/col/vct/col/resolve/lang/Java.scala

@@ -521,10 +521,10 @@ case object JavaAnnotationData {
   final case class BipData[G](name: String)(implicit val o: Origin) extends JavaAnnotationData[G]
 
   case object BipGuard {
-    def get[G](m: JavaMethod[G]): Option[BipGuard[G]] =
+    def get[G](m: JavaMethod[G]): Option[JavaAnnotation[G]] =
       m.modifiers
-        .collect { case ja @ JavaAnnotation(_, _) if ja.data.isDefined => ja.data.get }
-        .collectFirst { case b: BipGuard[G] => b }
+        .collect { case ja @ JavaAnnotation(_, _) => (ja, ja.data) }
+        .collectFirst { case (ja, Some(_: BipGuard[G])) => ja }
 
     def getName[G](method: JavaMethod[G]): Option[Expr[G]] =
       method.modifiers.collectFirst {

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

@@ -46,7 +46,7 @@ case object EncodeBip extends RewriterBuilderArg[VerificationResults] {
       }
       case ctx: SignalsFailed => PanicBlame("BIP transition does not have signals").blame(ctx)
       case ctx: ExceptionNotInSignals => PanicBlame("BIP transition does not have signals").blame(ctx)
-      case _: BipConstructorFailure | _: BipTransitionFailure | _: BipGuardFailure => PanicBlame("This error never occurs in the encoding, so why is it under CallableFailure?").blame(error)
+      case _: BipConstructorFailure | _: BipTransitionFailure => PanicBlame("This error never occurs in the encoding, so why is it under CallableFailure?").blame(error)
     }
   }
 
@@ -69,7 +69,7 @@ case object EncodeBip extends RewriterBuilderArg[VerificationResults] {
       }
       case ctx: SignalsFailed => proc.blame.blame(ctx)
       case ctx: ExceptionNotInSignals => proc.blame.blame(ctx)
-      case _: BipConstructorFailure | _: BipTransitionFailure | _: BipGuardFailure => PanicBlame("This error never occurs in the encoding, so why is it under CallableFailure?").blame(error)
+      case _: BipConstructorFailure | _: BipTransitionFailure =>PanicBlame("This error never occurs in the encoding, so why is it under CallableFailure?").blame(error)
     }
   }
 

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

@@ -164,15 +164,16 @@ case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
   }
 
   def rewriteGuard(m: JavaMethod[Pre]): Unit = {
-    val jad.BipGuard(_) = jad.BipGuard.get(m).get
+    val annotation = jad.BipGuard.get(m).get
+    val Some(jad.BipGuard(_)) = annotation.data
 
     if (m.returnType != TBool[Pre]()) { throw LangBipToCol.WrongGuardReturnType(m) }
 
     javaMethodSuccGuard(m) = rw.classDeclarations.declare(new BipGuard[Post](
       m.parameters.map(rewriteParameter),
       rw.dispatch(m.body.get),
       true
-    )(m.blame)(SourceNameOrigin(m.name, m.o)))
+    )(annotation.blame)(SourceNameOrigin(m.name, m.o)))
   }
 
   def rewriteOutgoingData(m: JavaMethod[Pre]): Unit = {

test/main/vct/test/integration/examples/TechnicalJavaBipSpec.scala

@@ -37,7 +37,7 @@ class TechnicalJavaBipSpec extends JavaBipSpecHelper {
     "technical/javabip/TransitionPostconditionFailed.java",
   )
 
-  vercors should verify using silicon example "technical/javabip/BipGuardUnsatisfiablePrecondition.java"
+  vercors should verify using silicon example "technical/javabip/BipGuardPreconditionUnsatisfiable.java"
   vercors should verify using silicon example "technical/javabip/BipGuardUsed.java"
   vercors should verify using silicon example "technical/javabip/BipGuardDataUsed.java"
 }