Compiles since a long while

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

@@ -1134,7 +1134,7 @@ final class BipTransition[G](val signature: BipTransitionSignature[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 invariant: Expr[G], val initial: Ref[G, BipStatePredicate[G]])(implicit val o: Origin) extends ClassDeclaration[G] with BipComponentImpl[G]
-final class BipConstructor[G](val args: Seq[Variable[G]], val body: Statement[G], val contract: ApplicableContract[G])(val blame: Blame[BipConstructorFailure])(implicit val o: Origin) extends ClassDeclaration[G]
+final class BipConstructor[G](val args: Seq[Variable[G]], val body: Statement[G], val requires: Expr[G])(val blame: Blame[BipConstructorFailure])(implicit val o: Origin) extends ClassDeclaration[G] with BipConstructorImpl[G]
 
 final class BipPort[G](val t: BipPortType[G])(implicit val o: Origin) extends ClassDeclaration[G] with BipPortImpl[G]
 sealed trait BipPortType[G] extends NodeFamily[G]

src/col/vct/col/ast/declaration/cls/BipConstructorImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.declaration.cls
+
+import vct.col.ast.{BipConstructor, Type, Variable}
+
+trait BipConstructorImpl[G] { this: BipConstructor[G] =>
+
+}

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

@@ -208,7 +208,7 @@ case class ContextEverywhereFailedInPre(failure: ContractFailure, node: Invoking
   override def inlineDescWithSource(node: String, failure: String): String = s"Context of `$node` may not hold in the precondition, since $failure."
 }
 
-sealed trait CallableFailure extends ConstructorFailure
+sealed trait CallableFailure extends ConstructorFailure with JavaConstructorFailure
 sealed trait ContractedFailure extends CallableFailure
 case class PostconditionFailed(path: Seq[AccountedDirection], failure: ContractFailure, node: ContractApplicable[_]) extends ContractedFailure with WithContractFailure {
   override def baseCode: String = "postFailed"
@@ -594,7 +594,7 @@ case class ScaleNegative(node: Scale[_]) extends NodeVerificationFailure {
   override def inlineDescWithSource(source: String): String = s"The scale in `$source` may be negative."
 }
 
-case class NontrivialUnsatisfiable(node: ApplicableContract[_]) extends NodeVerificationFailure {
+case class NontrivialUnsatisfiable(node: ApplicableContract[_]) extends NodeVerificationFailure with BipConstructorFailure {
   override def code: String = "unsatisfiable"
   override def descInContext: String = "The precondition of this contract may be unsatisfiable. If this is intentional, replace it with `requires false`."
   override def inlineDescWithSource(source: String): String =
@@ -622,12 +622,6 @@ sealed trait JavaAnnotationFailure extends VerificationFailure
 sealed trait JavaConstructorFailure extends VerificationFailure
 sealed trait JavaImplicitConstructorFailure extends VerificationFailure
 
-case class JavaConstructorPostconditionFailed(path: Seq[AccountedDirection], failure: ContractFailure, node: ContractApplicable[_]) extends JavaConstructorFailure with WithContractFailure {
-  override def baseCode: String = "javaConstructorPostFailed"
-  override def descInContext: String = "The postcondition of this constructor may not hold, since"
-  override def inlineDescWithSource(node: String, failure: String): String = s"Postcondition of `$node` may not hold, since $failure."
-}
-
 sealed trait BipConstructorFailure extends JavaConstructorFailure
 sealed trait BipTransitionFailure extends JavaAnnotationFailure
 

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

@@ -46,29 +46,20 @@ 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 => PanicBlame("This error never occurs in the encoding, so why is it under CallableFailure?").blame(error)
     }
   }
 
-  case class ConstructorPostconditionFailed(results: VerificationResults, component: BipComponent[_], constructor: BipConstructor[_]) extends Blame[CallableFailure] {
-    override def blame(error: CallableFailure): Unit = error match {
-      case cf: ContractedFailure => cf match {
-        case PostconditionFailed(Seq(FailLeft), failure, _) => // Failed establishing component invariant
-          results.report(component, ComponentInvariantNotMaintained)
-          constructor.blame.blame(BipComponentInvariantNotEstablished(failure, constructor))
-        case PostconditionFailed(Seq(FailRight, FailLeft), failure, _) => // Failed establishing state invariant
-          results.report(component, StateInvariantNotMaintained)
-          constructor.blame.blame(BipStateInvariantNotEstablished(failure, constructor))
-        case ctx@PostconditionFailed(FailRight +: FailRight +: path, failure, node) => // Failed postcondition
-          results.report(component, PostconditionNotVerified)
-          PanicBlame("BIP constructor should not have non-trivial post-condition").blame(ctx)
-        case PostconditionFailed(_, _, _) =>
-          throw BlamePathError
-        case ctx: TerminationMeasureFailed => PanicBlame("BIP constructor should not do termination checking").blame(ctx)
-        case ctx: ContextEverywhereFailedInPost => PanicBlame("BIP constructor should not have context everywhere clauses").blame(ctx)
-      }
-      case ctx: SignalsFailed => PanicBlame("BIP constructor should not have signals").blame(ctx)
-      case ctx: ExceptionNotInSignals => PanicBlame("BIP constructor should not have signals").blame(ctx)
+  case class ForwardComponentInvariantFailed(results: VerificationResults, component: BipComponent[_], constructor: BipConstructor[_]) extends Blame[ExhaleFailed] {
+    override def blame(error: ExhaleFailed): Unit = {
+      results.report(component, ComponentInvariantNotMaintained)
+      constructor.blame.blame(BipComponentInvariantNotEstablished(error.failure, constructor))
+    }
+  }
+
+  case class ForwardStateInvariantFailed(results: VerificationResults, component: BipComponent[_], constructor: BipConstructor[_]) extends Blame[ExhaleFailed] {
+    override def blame(error: ExhaleFailed): Unit = {
+      results.report(component, StateInvariantNotMaintained)
+      constructor.blame.blame(BipStateInvariantNotEstablished(error.failure, constructor))
     }
   }
 
@@ -310,46 +301,30 @@ case class EncodeBip[Pre <: Generation](results: VerificationResults) extends Re
       val component = componentOf(constructor)
       results.declare(component)
       implicit val o = DiagnosticOrigin
-      val t = TClass(succ[Class[Post]](classOf(constructor)))
+      val ref = succ[Class[Post]](classOf(constructor))
+      val t = TClass[Post](ref)
       rewritingBipConstructorBody.having(component) {
-        withResult { res: Result[Post] =>
-          val ensures =
-            // Establish component invariant
-            SplitAccountedPredicate(UnitAccountedPredicate(currentThis.having(res) {
-              dispatch(component.invariant)
-            }),
-            // Establish state invariant
-            UnitAccountedPredicate(currentThis.having(res) {
-              dispatch(component.initial.decl.expr)
-            }))
-
-          constructorSucc(constructor) = globalDeclarations.declare(
-            new Procedure[Post](
-              returnType = t,
-              args = variables.collect { constructor.args.map(dispatch) }._1,
-              outArgs = Nil, typeArgs = Nil,
-              body = {
-                val resVar = new Variable[Post](t)
-                val res = Local[Post](resVar.ref)
-                currentThis.having(res) {
-                  Some(Scope(Seq(resVar), Block(Seq(
-                    assignLocal(res, NewObject(ref)),
-                    fieldInit(res),
-                    sharedInit(res),
-                    dispatch(constructor.body),
-                    Return(res),
-                  ))))
-                }
+        constructorSucc(constructor) = globalDeclarations.declare(
+          new Procedure[Post](
+            returnType = TVoid(),
+            args = variables.collect { constructor.args.map(dispatch) }._1,
+            outArgs = Nil, typeArgs = Nil,
+            body = {
+              val resVar = new Variable[Post](t)
+              val res = Local[Post](resVar.ref)
+              currentThis.having(res) {
+                Some(Scope(Seq(resVar), Block(Seq(
+                  assignLocal(res, NewObject(ref)),
+                  dispatch(constructor.body),
+                  Exhale(dispatch(component.initial.decl.expr))(ForwardStateInvariantFailed(results, component, constructor)),
+                  Exhale(dispatch(component.invariant))(ForwardComponentInvariantFailed(results, component, constructor))
+                ))))
               }
-              ???,
-              ???,
-              ???
-            )(ConstructorPostconditionFailed(results, component, constructor))
-          )
-//          globalDeclarations.succeed(proc,
-//            proc.rewrite(contract = contract,
-//              blame = ConstructorPostconditionFailed(results, component, proc)))
-        }
+            },
+            contract(requires = UnitAccountedPredicate(dispatch(constructor.requires)),
+              blame = constructor.blame)
+          )(PanicBlame("Unexpected error, failing precondition on JavaBIP constructor should not happen"))
+        )
       }
 
     case transition: BipTransition[Pre] =>
@@ -418,9 +393,7 @@ case class EncodeBip[Pre <: Generation](results: VerificationResults) extends Re
              - Guard (done further down)
         */
       val preconditionComponents: Expr[Post] = foldStar(synchronization.transitions.map { case Ref(transition) =>
-        val clsThisSubst = (ThisObject[Pre](classOf(transition).ref)(DiagnosticOrigin), varOf(transition))
-
-        currentThis.having(clsThisSubst) {
+        currentThis.having(varOf(transition)) {
           (varOf(transition) !== Null()) &**
             dispatch(componentOf(transition).invariant) &**
             dispatch(transition.source.decl.expr)
@@ -436,8 +409,7 @@ case class EncodeBip[Pre <: Generation](results: VerificationResults) extends Re
       })
 
       val preconditionGuards: Expr[Post] = foldStar(synchronization.transitions.map { case Ref(transition) =>
-        val clsThisSubst = (ThisObject[Pre](classOf(transition).ref)(DiagnosticOrigin), varOf(transition))
-        currentThis.having(clsThisSubst) {
+        currentThis.having(varOf(transition)) {
           incomingDataContext.having(RewriteToOutgoingDataContext(incomingDataTranslation)) {
             dispatch(transition.guard)
           }
@@ -465,10 +437,8 @@ case class EncodeBip[Pre <: Generation](results: VerificationResults) extends Re
           - Separate so we can detect the error easily
       */
       val exhales: Seq[Exhale[Post]] = synchronization.transitions.flatMap { case Ref(transition) =>
-        val clsThisSubst = (ThisObject[Pre](classOf(transition).ref)(DiagnosticOrigin), varOf(transition))
-
         incomingDataContext.having(RewriteToVariableContext(incomingDataToVariableContext)) {
-          val componentStateGuardExhale = Exhale(currentThis.having(clsThisSubst) { foldStar(
+          val componentStateGuardExhale = Exhale(currentThis.having(varOf(transition)) { foldStar(
             Seq(dispatch(componentOf(transition).invariant), dispatch(transition.source.decl.expr)) :+
                 dispatch(transition.guard)
           )})(PanicBlame("Component invariant, state invariant, and transition guard should hold"))
@@ -490,7 +460,7 @@ case class EncodeBip[Pre <: Generation](results: VerificationResults) extends Re
              We don't have to split up the component, state, guard, any further, because those are always implied
              by the precondition of the synchron.
            */
-          val preconditionExhale = Exhale(currentThis.having(clsThisSubst) {
+          val preconditionExhale = Exhale(currentThis.having(varOf(transition)) {
                 dispatch(transition.requires)
             })(ExhalingTransitionPreconditionFailed(results, synchronization, transition))
 
@@ -505,9 +475,7 @@ case class EncodeBip[Pre <: Generation](results: VerificationResults) extends Re
           - postcondition
       */
       val inhales: Seq[Inhale[Post]] = synchronization.transitions.map { case Ref(transition) =>
-        val clsThisSubst = (ThisObject[Pre](classOf(transition).ref)(DiagnosticOrigin), varOf(transition))
-
-        Inhale(currentThis.having(clsThisSubst) {
+        Inhale(currentThis.having(varOf(transition)) {
           dispatch(componentOf(transition).invariant) &**
             dispatch(transition.target.decl.expr) &**
             dispatch(transition.ensures)
@@ -521,9 +489,8 @@ case class EncodeBip[Pre <: Generation](results: VerificationResults) extends Re
           - New state invariant
       */
       val postcondition: Expr[Post] = foldStar(synchronization.transitions.map { case Ref(transition) =>
-        val clsThisSubst = (ThisObject[Pre](classOf(transition).ref)(DiagnosticOrigin), varOf(transition))
 
-        currentThis.having(clsThisSubst) {
+        currentThis.having(varOf(transition)) {
           dispatch(componentOf(transition).invariant) &**
           dispatch(transition.target.decl.expr)
         }

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

@@ -174,7 +174,7 @@ case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
     BipLocalIncomingData(javaParamSucc.ref[Post, BipIncomingData[Post]](decl))(local.o)
   }
 
-  def rewriteConstructor(constructor: JavaConstructor[Pre], annotation: JavaAnnotation[Pre], data: jad.BipComponent[Pre], generateBody: Statement[Pre] => Statement[Post]): Unit = {
+  def rewriteConstructor(constructor: JavaConstructor[Pre], annotation: JavaAnnotation[Pre], data: jad.BipComponent[Pre], generateInit: Expr[Post] => Statement[Post]): Unit = {
     implicit val o: Origin = constructor.o
     val contractWithoutRequires = constructor.contract.copy(requires = UnitAccountedPredicate[Pre](tt))(
       blame = constructor.contract.blame)(o = constructor.o)
@@ -183,17 +183,18 @@ case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
     }
 
     logger.debug(s"JavaBIP component constructor for ${constructor.o.context}")
-    rw.labelDecls.scope {
-      rw.classDeclarations.declare(withResult((result: Result[Post]]) =>
-        val t = TClass(rw.java.javaInstanceClassSuccessor.ref(rw.java.currentJavaClass.top))
-        new BipConstructor(
-          args = rw.variables.collect { constructor.parameters.map(rw.dispatch) }._1,
-          body = generateBody(constructor.body),
-          contract = rw.currentThis.having(result) { constructor.contract.rewrite(
-            ensures = UnitAccountedPredicate((result !== Null()) && (TypeOf(result) === TypeValue(t)))
-          ) }
-        )(constructor.blame /* TODO: Account for extra postcondition */)(BipConstructorOrigin(rw.java.currentJavaClass.top.asInstanceOf, constructor))
-      ))
+    rw.currentThis.having(ThisObject(rw.java.javaInstanceClassSuccessor.ref(rw.java.currentJavaClass.top))) {
+      rw.labelDecls.scope {
+        rw.classDeclarations.declare(
+          new BipConstructor(
+            args = rw.variables.collect { constructor.parameters.map(rw.dispatch) }._1,
+            body = Block(Seq(
+              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))
+        )
+      }
     }
   }