Add BipConstructor node

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

@@ -1135,7 +1135,7 @@ final class BipGuard[G](val data: Seq[Ref[G, BipIncomingData[G]]], val body: Sta
 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]
-final class BipConstructor[G](val parameters: Seq[Variable[G]], val body: Statement[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 blame: Blame[BipConstructorFailure])(implicit val o: Origin) extends ClassDeclaration[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/typerules/CoercingRewriter.scala

@@ -1673,7 +1673,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case namespace: JavaNamespace[Pre] =>
         namespace
       case clazz: JavaClass[Pre] =>
-        new JavaClass[Pre](clazz.name, clazz.modifiers, clazz.typeParams, res(clazz.intrinsicLockInvariant), clazz.ext, clazz.imp, clazz.decls)
+        new JavaClass[Pre](clazz.name, clazz.modifiers, clazz.typeParams, res(clazz.intrinsicLockInvariant), clazz.ext, clazz.imp, clazz.decls)(clazz.blame)
       case interface: JavaInterface[Pre] =>
         interface
       case interface: JavaAnnotationInterface[Pre] =>
@@ -1748,7 +1748,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         })
       case seqProg: VeyMontSeqProg[Pre] => seqProg
       case thread: VeyMontThread[Pre] => thread
-      case bc: BipConstructor[Pre] => new BipConstructor(bc.parameters, bc.body)(bc.blame)
+      case bc: BipConstructor[Pre] => new BipConstructor(bc.args, bc.body)(bc.blame)
       case bc: BipComponent[Pre] =>
         new BipComponent(bc.fqn, bc.constructors, res(bc.invariant), bc.initial)
       case bsp: BipStatePredicate[Pre] =>

src/parsers/vct/parsers/transform/JavaToCol.scala

@@ -39,7 +39,7 @@ case class JavaToCol[G](override val originProvider: OriginProvider, override va
         Seq(new JavaClass(convert(name), mods.map(convert(_)), args.map(convert(_)).getOrElse(Nil),
           AstBuildHelpers.foldStar(contract.consume(contract.lock_invariant)),
           ext.map(convert(_)).getOrElse(Java.JAVA_LANG_OBJECT),
-          imp.map(convert(_)).getOrElse(Nil), decls.flatMap(convert(_))))
+          imp.map(convert(_)).getOrElse(Nil), decls.flatMap(convert(_)))(blame(decl)))
       })
     case TypeDeclaration1(mods, EnumDeclaration0(_, name, None, _, Some(constants), _, None | Some(EnumBodyDeclarations0(_, Seq())), _)) =>
       mods.map(convert(_)).foreach {

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

@@ -36,6 +36,11 @@ case object LangBipToCol {
     override def text: String = m.o.messageInContext("This data method should be marked pure with `@Pure`")
   }
 
+  case class ImproperConstructor(c: JavaConstructor[_], msg: String) extends UserError {
+    override def code: String = "bipImproperConstructor"
+    override def text: String = c.o.messageInContext(msg)
+  }
+
   case class BipIncomingDataInconsistentType(data: BipData[_], param: JavaParam[_]) extends UserError {
     override def code: String = "bipInconsistentDataType"
     override def text: String = Origin.messagesInContext(Seq(
@@ -72,6 +77,14 @@ case object LangBipToCol {
     override def inlineContext: String = data.o.inlineContext
     override def shortPosition: String = data.o.shortPosition
   }
+
+  case class BipConstructorOrigin(cls: JavaClass[_], 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 LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging {
@@ -161,6 +174,23 @@ 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]): Unit = {
+    if (constructor.contract.nonEmpty) {
+      throw ImproperConstructor(constructor, "Non-trivial contract is not 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(
+          args = rw.variables.collect { constructor.parameters.map(rw.dispatch) }._1,
+          body = rw.dispatch(constructor.body),
+        )(constructor.blame)(BipConstructorOrigin(rw.java.currentJavaClass.top.asInstanceOf, constructor))
+      )
+    }
+  }
+
   def rewriteGuard(method: JavaMethod[Pre], annotation: JavaAnnotation[Pre], guard: jad.BipGuard[Pre]): Unit = {
     if (method.returnType != TBool[Pre]()) { throw LangBipToCol.WrongGuardReturnType(method) }
 

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

@@ -216,6 +216,12 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends
 
     declsDefault.foreach {
       case cons: JavaConstructor[Pre] =>
+        val results = currentJavaClass.top.modifiers.collect {
+          case annotation@JavaAnnotationEx(_, _, component@JavaAnnotationData.BipComponent(_, _)) =>
+            rw.bip.rewriteConstructor(cons, annotation, component)
+        }
+        if (results.nonEmpty) return
+
         logger.debug(s"Constructor for ${cons.o.context}")
         implicit val o: Origin = cons.o
         val t = TClass(ref)