Making java constructor errors first class

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 with JavaConstructorFailure
+sealed trait CallableFailure extends ConstructorFailure
 sealed trait ContractedFailure extends CallableFailure
 case class PostconditionFailed(path: Seq[AccountedDirection], failure: ContractFailure, node: ContractApplicable[_]) extends ContractedFailure with WithContractFailure {
   override def baseCode: String = "postFailed"
@@ -622,6 +622,12 @@ 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
 
@@ -640,13 +646,13 @@ sealed trait BipTransitionContractFailure extends BipTransitionFailure with With
     ))
 }
 
-case class BipComponentInvariantNotEstablished(failure: ContractFailure, node: Procedure[_]) extends BipConstructorFailure with WithContractFailure {
+case class BipComponentInvariantNotEstablished(failure: ContractFailure, node: BipConstructor[_]) extends BipConstructorFailure with WithContractFailure {
   override def baseCode: String = "bipComponentInvariantNotEstablished"
   override def descInContext: String = "In this constructor the component invariant is not established, since"
   override def inlineDescWithSource(node: String, failure: String): String = s"The component invariant cannot be established in $node, since $failure"
 }
 
-case class BipStateInvariantNotEstablished(failure: ContractFailure, node: Procedure[_]) extends BipConstructorFailure with WithContractFailure {
+case class BipStateInvariantNotEstablished(failure: ContractFailure, node: BipConstructor[_]) extends BipConstructorFailure with WithContractFailure {
   override def baseCode: String = "bipStateInvariantNotEstablished"
   override def descInContext: String = "In this constructor the invariant of the state is not established, since"
   override def inlineDescWithSource(node: String, failure: String): String = s"The state invariant is not established in $node, since $failure"

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

@@ -50,25 +50,25 @@ case object EncodeBip extends RewriterBuilderArg[VerificationResults] {
     }
   }
 
-  case class ConstructorPostconditionFailed(results: VerificationResults, component: BipComponent[_], proc: Procedure[_]) extends Blame[CallableFailure] {
+  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)
-          proc.blame.blame(BipComponentInvariantNotEstablished(failure, proc))
+          constructor.blame.blame(BipComponentInvariantNotEstablished(failure, constructor))
         case PostconditionFailed(Seq(FailRight, FailLeft), failure, _) => // Failed establishing state invariant
           results.report(component, StateInvariantNotMaintained)
-          proc.blame.blame(BipStateInvariantNotEstablished(failure, proc))
-        case PostconditionFailed(FailRight +: FailRight +: path, failure, node) => // Failed postcondition
+          constructor.blame.blame(BipStateInvariantNotEstablished(failure, constructor))
+        case ctx@PostconditionFailed(FailRight +: FailRight +: path, failure, node) => // Failed postcondition
           results.report(component, PostconditionNotVerified)
-          proc.blame.blame(PostconditionFailed(path, failure, node))
+          PanicBlame("BIP constructor should not have non-trivial post-condition").blame(ctx)
         case PostconditionFailed(_, _, _) =>
           throw BlamePathError
-        case ctx: TerminationMeasureFailed => proc.blame.blame(ctx)
-        case ctx: ContextEverywhereFailedInPost => proc.blame.blame(ctx)
+        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 => proc.blame.blame(ctx)
-      case ctx: ExceptionNotInSignals => proc.blame.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)
     }
   }
 

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

@@ -175,12 +175,13 @@ case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
   }
 
   def rewriteConstructor(constructor: JavaConstructor[Pre], annotation: JavaAnnotation[Pre], data: jad.BipComponent[Pre]): Unit = {
-    if (constructor.contract.nonEmpty) {
-      throw ImproperConstructor(constructor, "Non-trivial contract is not allowed on JavaBIP component constructors")
+    implicit val o: Origin = constructor.o
+    val contractWithoutRequires = constructor.contract.copy(requires = UnitAccountedPredicate(tt))()
+    if (contractWithoutRequires.nonEmpty) {
+      throw ImproperConstructor(constructor, "Only precondition is allowed on JavaBIP component constructors")
     }
 
     logger.debug(s"JavaBIP component constructor for ${constructor.o.context}")
-    implicit val o: Origin = constructor.o
     rw.labelDecls.scope {
       rw.classDeclarations.declare(
         new BipConstructor(

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

@@ -4,14 +4,15 @@ import com.typesafe.scalalogging.LazyLogging
 import hre.util.{FuncTools, ScopedStack}
 import vct.col.ast._
 import vct.col.rewrite.lang.LangSpecificToCol.{NotAValue, ThisVar}
-import vct.col.origin.{AbstractApplicable, DerefPerm, JavaArrayInitializerBlame, Origin, PanicBlame, PostBlameSplit, SourceNameOrigin, TrueSatisfiable}
+import vct.col.origin.{AbstractApplicable, Blame, CallableFailure, ContextEverywhereFailedInPost, ContractedFailure, DerefPerm, ExceptionNotInSignals, JavaArrayInitializerBlame, JavaConstructorPostconditionFailed, Origin, PanicBlame, PostBlameSplit, SignalsFailed, SourceNameOrigin, TerminationMeasureFailed, TrueSatisfiable}
 import vct.col.ref.{LazyRef, Ref}
 import vct.col.resolve.ctx._
 import vct.col.rewrite.{Generation, Rewritten}
 import vct.col.util.AstBuildHelpers._
 import vct.col.util.SuccessionMap
 import RewriteHelpers._
 import vct.col.ast.lang.JavaAnnotationEx
+import vct.col.origin
 import vct.col.resolve.lang.{Java, JavaAnnotationData}
 import vct.col.resolve.lang.JavaAnnotationData.{BipComponent, BipData, BipGuard, BipTransition}
 import vct.result.VerificationError.{Unreachable, UserError}
@@ -91,6 +92,18 @@ case object LangJavaToCol {
     override def code: String = decl.o.messageInContext("This declaration is not supported in the java.lang.String class")
     override def text: String = "notSupportedInStringClass"
   }
+
+  case class TransformCallableError(constructor: JavaConstructor[_]) extends Blame[CallableFailure] {
+    override def blame(error: CallableFailure): Unit = error match {
+      case failure: ContractedFailure => failure match {
+        case PostconditionFailed(path, failure, node) => JavaConstructorPostconditionFailed(path, failure, node)
+        case TerminationMeasureFailed(applicable, apply, measure) => ??? // JavaConstructorTerminationMeasureFailed(applicable, apply, measure)
+        case ContextEverywhereFailedInPost(failure, node) => ???
+      }
+      case SignalsFailed(failure, node) => ???
+      case ExceptionNotInSignals(node) => ???
+    }
+  }
 }
 
 case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging {
@@ -248,7 +261,8 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends
                 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))
+            )(PostBlameSplit.left(PanicBlame("Constructor cannot return null value or value of wrong type."),
+                TransformCallableError(cons)))(JavaConstructorOrigin(cons))
           ))
         }
       case method: JavaMethod[Pre] =>