Hmm

utwente-fmt · Oct 11, 2023 · ab40e3a · ab40e3a
1 parent 41b209c
commit ab40e3a
Show file tree

Hide file tree

Showing 3 changed files with 32 additions and 27 deletions.
diff --git a/examples/technical/javabip/ComponentInvariantNotEstablished.java b/examples/technical/javabip/ComponentInvariantNotEstablished.java
@@ -9,7 +9,7 @@ public class ComponentInvariantNotEstablished {
     public static final String INIT = "initialState";
     public static final String NAME = "oneComponentOneTransition";
 
-    OneComponentOneTransition() { }
+    ComponentInvariantNotEstablished() { }
 
     private int x;
 }

diff --git a/src/rewrite/vct/rewrite/lang/LangBipToCol.scala b/src/rewrite/vct/rewrite/lang/LangBipToCol.scala
@@ -3,7 +3,7 @@ package vct.col.lang
 import com.typesafe.scalalogging.LazyLogging
 import vct.col.ast._
 import vct.col.lang.LangBipToCol._
-import vct.col.origin.{DiagnosticOrigin, Origin, PanicBlame, SourceNameOrigin}
+import vct.col.origin.{BipComponentInvariantNotEstablished, BipConstructorFailure, BipStateInvariantNotEstablished, Blame, DiagnosticOrigin, NontrivialUnsatisfiable, Origin, PanicBlame, SourceNameOrigin}
 import vct.col.ref.Ref
 import vct.col.resolve.ctx.{ImplicitDefaultJavaBipStatePredicate, JavaBipStatePredicateTarget, RefJavaBipGuard, RefJavaBipStatePredicate}
 import vct.col.resolve.lang.{JavaAnnotationData => jad}
@@ -78,13 +78,21 @@ case object LangBipToCol {
     override def shortPosition: String = data.o.shortPosition
   }
 
-  case class BipConstructorOrigin(cls: JavaClass[_], c: JavaConstructor[_]) extends Origin {
+  case class BipConstructorOrigin(cls: JavaClassOrInterface[_], c: JavaConstructor[_]) extends Origin {
     override def preferredName: String = s"${cls.o.preferredName}_constructor"
 
     override def context: String = c.o.context
     override def inlineContext: String = c.o.inlineContext
     override def shortPosition: String = c.o.shortPosition
   }
+
+  case class UntangleBipConstructorFailure(constructor: JavaConstructor[_]) extends Blame[BipConstructorFailure] {
+    override def blame(error: BipConstructorFailure): Unit = error match {
+      case err: NontrivialUnsatisfiable => constructor.contract.blame.blame(err)
+      case err: BipComponentInvariantNotEstablished => constructor.blame.blame(err)
+      case err: BipStateInvariantNotEstablished => constructor.blame.blame(err)
+    }
+  }
 }
 
 case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging {
@@ -192,7 +200,7 @@ case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
               generateInit(rw.currentThis.top),
               rw.dispatch(constructor.body))),
             requires = foldStar(rw.dispatch(constructor.contract.requires))
-          )(constructor.blame /* TODO: Account for extra postcondition */)(BipConstructorOrigin(rw.java.currentJavaClass.top.asInstanceOf, constructor))
+          )(UntangleBipConstructorFailure(constructor))(BipConstructorOrigin(rw.java.currentJavaClass.top, constructor))
         )
       }
     }

diff --git a/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala b/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala
@@ -227,34 +227,31 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends
           case annotation@JavaAnnotationEx(_, _, component@JavaAnnotationData.BipComponent(_, _)) =>
             rw.bip.rewriteConstructor(cons, annotation, component, diz => Block[Post](Seq(fieldInit(diz), sharedInit(diz))))
         }
-        if (results.nonEmpty) return
-
-        rw.labelDecls.scope {
-          javaConstructor(cons) = rw.globalDeclarations.declare(withResult((result: Result[Post]) =>
-            new Procedure(
-              returnType = t,
-              args = rw.variables.collect { cons.parameters.map(rw.dispatch) }._1,
-              outArgs = Nil, typeArgs = Nil,
-              body = Some(rw.currentThis.having(res) {
-                Scope(Seq(resVar), Block(Seq(
+        if (results.isEmpty) { // We didn't execute the bip rewrite, so we do the normal one
+          rw.labelDecls.scope {
+            javaConstructor(cons) = rw.globalDeclarations.declare(withResult((result: Result[Post]) =>
+              new Procedure(
+                returnType = t,
+                args = rw.variables.collect { cons.parameters.map(rw.dispatch) }._1,
+                outArgs = Nil, typeArgs = Nil,
+                body = rw.currentThis.having(res) { Some(Scope(Seq(resVar), Block(Seq(
                   assignLocal(res, NewObject(ref)),
                   fieldInit(res),
                   sharedInit(res),
                   rw.dispatch(cons.body),
                   Return(res),
-                )))
-              }),
-              contract = rw.currentThis.having(result) { cons.contract.rewrite(
-                ensures = SplitAccountedPredicate(
-                  left = UnitAccountedPredicate((result !== Null()) && (TypeOf(result) === TypeValue(t))),
-                  right = rw.dispatch(cons.contract.ensures),
-                ),
-                signals = cons.contract.signals.map(rw.dispatch) ++
-                  cons.signals.map(t => SignalsClause(new Variable(rw.dispatch(t)), tt)),
-              ) },
-            )(PostBlameSplit.left[CallableFailure](PanicBlame("Constructor cannot return null value or value of wrong type."),
-                cons.blame))(JavaConstructorOrigin(cons))
-          ))
+                )))) },
+                contract = rw.currentThis.having(result) { cons.contract.rewrite(
+                  ensures = SplitAccountedPredicate(
+                    left = UnitAccountedPredicate((result !== Null()) && (TypeOf(result) === TypeValue(t))),
+                    right = rw.dispatch(cons.contract.ensures),
+                  ),
+                  signals = cons.contract.signals.map(rw.dispatch) ++
+                    cons.signals.map(t => SignalsClause(new Variable(rw.dispatch(t)), tt)),
+                ) },
+              )(PostBlameSplit.left(PanicBlame("Constructor cannot return null value or value of wrong type."), cons.blame))(JavaConstructorOrigin(cons))
+            ))
+          }
         }
       case method: JavaMethod[Pre] =>
         // For each javabip annotation that we encounter, execute a rewrite