Merge pull request #1073 from utwente-fmt/resolve-javabip-warnings

Resolve javabip warnings

examples/concepts/javabip/casinoAdjusted/Operator.java

@@ -23,9 +23,9 @@ public class Operator {
     int amountToMove;
 
     //@ requires id != null;
+    //@ requires funds >= 0;
     Operator (Integer id, int funds) throws Exception {
         this.id = id;
-        if (funds < 0) throw new Exception("Cannot have negative funds");
         wallet = funds;
         amountToMove = 0;
         //@ ghost System.staticInvariant();

examples/concepts/javabip/casinoBroken/Operator.java

@@ -23,9 +23,9 @@ public class Operator {
     int amountToMove;
 
     //@ requires id != null;
+    //@ requires funds >= 0;
     Operator (Integer id, int funds) throws Exception {
         this.id = id;
-        if (funds < 0) throw new Exception("Cannot have negative funds");
         wallet = funds;
         amountToMove = 0;
         //@ ghost System.staticInvariant();

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]*/

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;
 }

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

@@ -1054,14 +1054,14 @@ sealed trait JavaGlobalDeclaration[G] extends GlobalDeclaration[G] with JavaGlob
 final class JavaNamespace[G](val pkg: Option[JavaName[G]], val imports: Seq[JavaImport[G]], val declarations: Seq[GlobalDeclaration[G]])(implicit val o: Origin) extends JavaGlobalDeclaration[G] with Declarator[G] with JavaNamespaceImpl[G]
 
 sealed trait JavaClassOrInterface[G] extends JavaGlobalDeclaration[G] with Declarator[G] with JavaClassOrInterfaceImpl[G]
-final class JavaClass[G](val name: String, val modifiers: Seq[JavaModifier[G]], val typeParams: Seq[Variable[G]], val intrinsicLockInvariant: Expr[G], val ext: Type[G], val imp: Seq[Type[G]], val decls: Seq[ClassDeclaration[G]])(implicit val o: Origin) extends JavaClassOrInterface[G] with JavaClassImpl[G]
+final class JavaClass[G](val name: String, val modifiers: Seq[JavaModifier[G]], val typeParams: Seq[Variable[G]], val intrinsicLockInvariant: Expr[G], val ext: Type[G], val imp: Seq[Type[G]], val decls: Seq[ClassDeclaration[G]])(val blame: Blame[JavaImplicitConstructorFailure])(implicit val o: Origin) extends JavaClassOrInterface[G] with JavaClassImpl[G]
 final class JavaInterface[G](val name: String, val modifiers: Seq[JavaModifier[G]], val typeParams: Seq[Variable[G]], val ext: Seq[Type[G]], val decls: Seq[ClassDeclaration[G]])(implicit val o: Origin) extends JavaClassOrInterface[G] with JavaInterfaceImpl[G]
 final class JavaAnnotationInterface[G](val name: String, val modifiers: Seq[JavaModifier[G]], val ext: Type[G], val decls: Seq[ClassDeclaration[G]])(implicit val o: Origin) extends JavaClassOrInterface[G] with JavaAnnotationInterfaceImpl[G]
 
 sealed trait JavaClassDeclaration[G] extends ClassDeclaration[G] with JavaClassDeclarationImpl[G]
 final class JavaSharedInitialization[G](val isStatic: Boolean, val initialization: Statement[G])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaSharedInitializationImpl[G]
 final class JavaFields[G](val modifiers: Seq[JavaModifier[G]], val t: Type[G], val decls: Seq[JavaVariableDeclaration[G]])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaFieldsImpl[G]
-final class JavaConstructor[G](val modifiers: Seq[JavaModifier[G]], val name: String, val parameters: Seq[JavaParam[G]], val typeParameters: Seq[Variable[G]], val signals: Seq[Type[G]], val body: Statement[G], val contract: ApplicableContract[G])(val blame: Blame[ConstructorFailure])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaConstructorImpl[G]
+final class JavaConstructor[G](val modifiers: Seq[JavaModifier[G]], val name: String, val parameters: Seq[JavaParam[G]], val typeParameters: Seq[Variable[G]], val signals: Seq[Type[G]], val body: Statement[G], val contract: ApplicableContract[G])(val blame: Blame[JavaConstructorFailure])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaConstructorImpl[G]
 final class JavaParam[G](val modifiers: Seq[JavaModifier[G]], val name: String, val t: Type[G])(implicit val o: Origin) extends Declaration[G] with JavaParamImpl[G]
 
 final class JavaMethod[G](val modifiers: Seq[JavaModifier[G]], val returnType: Type[G], val dims: Int, val name: String, val parameters: Seq[JavaParam[G]], val typeParameters: Seq[Variable[G]], val signals: Seq[Type[G]], val body: Option[Statement[G]], val contract: ApplicableContract[G])(val blame: Blame[CallableFailure])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaMethodImpl[G]
@@ -1120,7 +1120,7 @@ final case class BipGlueDataWire[G](dataOut: Ref[G, BipOutgoingData[G]], dataIn:
 
 sealed trait BipData[G] extends ClassDeclaration[G] with BipDataImpl[G]
 final class BipIncomingData[G](val t: Type[G])(implicit val o: Origin) extends BipData[G] with BipIncomingDataImpl[G]
-final class BipOutgoingData[G](val t: Type[G], val body: Statement[G], val pure: Boolean)(val blame: Blame[CallableFailure])(implicit val o: Origin) extends BipData[G] with BipOutgoingDataImpl[G]
+final class BipOutgoingData[G](val t: Type[G], val body: Statement[G], val pure: Boolean)(val blame: Blame[BipOutgoingDataPreconditionUnsatisfiable])(implicit val o: Origin) extends BipData[G] with BipOutgoingDataImpl[G]
 final case class BipLocalIncomingData[G](ref: Ref[G, BipIncomingData[G]])(implicit val o: Origin) extends Expr[G] with BipLocalIncomingDataImpl[G]
 
 final class BipStatePredicate[G](val expr: Expr[G])(implicit val o: Origin) extends ClassDeclaration[G] with BipStatePredicateImpl[G]
@@ -1131,10 +1131,10 @@ 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[BipGuardFailure])(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]
+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 requires: Expr[G])(val blame: Blame[BipConstructorFailure])(implicit val o: Origin) extends ClassDeclaration[G] with Declarator[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, Declaration, Type, Variable}
+
+trait BipConstructorImpl[G] { this: BipConstructor[G] =>
+  override def declarations: Seq[Declaration[G]] = args
+}

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 =
@@ -619,9 +619,11 @@ case class CoerceZFracFracFailed(node: Expr[_]) extends UnsafeCoercion {
 }
 
 sealed trait JavaAnnotationFailure extends VerificationFailure
+sealed trait JavaConstructorFailure extends VerificationFailure
+sealed trait JavaImplicitConstructorFailure extends VerificationFailure
 
-sealed trait BipConstructorFailure extends CallableFailure
-sealed trait BipTransitionFailure extends CallableFailure
+sealed trait BipConstructorFailure extends JavaConstructorFailure
+sealed trait BipTransitionFailure extends JavaAnnotationFailure
 
 sealed trait BipTransitionContractFailure extends BipTransitionFailure with WithContractFailure {
   def transition: BipTransition[_]
@@ -638,13 +640,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"
@@ -675,15 +677,14 @@ case class BipTransitionPreconditionUnsatisfiable(node: BipTransition[_]) extend
   override def inlineDescWithSource(source: String): String = s"Precondition unsatisfiable for transition `$source`"
 }
 
-case class BipOutgoingDataPreconditionUnsatisfiable(node: BipOutgoingData[_]) extends BipTransitionFailure with NodeVerificationFailure {
+case class BipOutgoingDataPreconditionUnsatisfiable(node: BipOutgoingData[_]) extends JavaAnnotationFailure with NodeVerificationFailure {
   override def code: String = "bipOutgoingDataPreconditionUnsatisfiable"
   override def descInContext: String = "The precondition of this outgoing data is unsatisfiable"
 
   override def inlineDescWithSource(source: String): String = s"Precondition unsatisfiable for outgoing data `$source`"
 }
 
-sealed trait BipGuardFailure extends CallableFailure
-case class BipGuardPreconditionUnsatisfiable(node: BipGuard[_]) extends BipGuardFailure with NodeVerificationFailure {
+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/ctx/Referrable.scala

@@ -70,6 +70,17 @@ sealed trait Referrable[G] {
     case RefLlvmFunctionDefinition(decl) => Referrable.originName(decl)
     case RefLlvmGlobal(decl) => Referrable.originName(decl)
     case RefLlvmSpecFunction(decl) => Referrable.originName(decl)
+    case RefBipComponent(decl) => Referrable.originName(decl)
+    case RefBipGlue(decl) => ""
+    case RefBipGuard(decl) => Referrable.originName(decl)
+    case RefBipIncomingData(decl) => Referrable.originName(decl)
+    case RefBipOutgoingData(decl) => Referrable.originName(decl)
+    case RefBipPort(decl) => Referrable.originName(decl)
+    case RefBipPortSynchronization(decl) => ""
+    case RefBipStatePredicate(decl) => Referrable.originName(decl)
+    case RefBipTransition(decl) => Referrable.originName(decl)
+    case RefBipTransitionSynchronization(decl) => ""
+    case RefBipConstructor(decl) => Referrable.originName(decl)
 
     case RefJavaBipGlueContainer() => ""
     case PVLBuiltinInstanceMethod(_) => ""
@@ -144,12 +155,23 @@ case object Referrable {
     case decl: PVLConstructor[G] => RefPVLConstructor(decl)
     case decl: VeyMontSeqProg[G] => RefSeqProg(decl)
     case decl: VeyMontThread[G] => RefVeyMontThread(decl)
-    case decl: JavaBipGlueContainer[G] => RefJavaBipGlueContainer()
     case decl: LlvmFunctionDefinition[G] => RefLlvmFunctionDefinition(decl)
     case decl: LlvmGlobal[G] => RefLlvmGlobal(decl)
     case decl: LlvmSpecFunction[G] => RefLlvmSpecFunction(decl)
     case decl: ProverType[G] => RefProverType(decl)
     case decl: ProverFunction[G] => RefProverFunction(decl)
+    case decl: JavaBipGlueContainer[G] => RefJavaBipGlueContainer()
+    case decl: BipComponent[G] => RefBipComponent(decl)
+    case decl: BipGlue[G] => RefBipGlue(decl)
+    case decl: BipGuard[G] => RefBipGuard(decl)
+    case decl: BipIncomingData[G] => RefBipIncomingData(decl)
+    case decl: BipOutgoingData[G] => RefBipOutgoingData(decl)
+    case decl: BipPort[G] => RefBipPort(decl)
+    case decl: BipPortSynchronization[G] => RefBipPortSynchronization(decl)
+    case decl: BipStatePredicate[G] => RefBipStatePredicate(decl)
+    case decl: BipTransition[G] => RefBipTransition(decl)
+    case decl: BipTransitionSynchronization[G] => RefBipTransitionSynchronization(decl)
+    case decl: BipConstructor[G] => RefBipConstructor(decl)
   })
 
   def originName(decl: Declaration[_]): String = decl.o match {
@@ -261,6 +283,17 @@ case class RefJavaBipGuard[G](decl: JavaMethod[G]) extends Referrable[G] with Ja
 case class RefJavaBipGlueContainer[G]() extends Referrable[G] // Bip glue jobs are not actually referrable
 case class RefLlvmFunctionDefinition[G](decl: LlvmFunctionDefinition[G]) extends Referrable[G] with LlvmInvocationTarget[G] with ResultTarget[G]
 case class RefLlvmGlobal[G](decl: LlvmGlobal[G]) extends Referrable[G]
+case class RefBipComponent[G](decl: BipComponent[G]) extends Referrable[G]
+case class RefBipGlue[G](decl: BipGlue[G]) extends Referrable[G]
+case class RefBipGuard[G](decl: BipGuard[G]) extends Referrable[G]
+case class RefBipIncomingData[G](decl: BipIncomingData[G]) extends Referrable[G]
+case class RefBipOutgoingData[G](decl: BipOutgoingData[G]) extends Referrable[G]
+case class RefBipPort[G](decl: BipPort[G]) extends Referrable[G]
+case class RefBipPortSynchronization[G](decl: BipPortSynchronization[G]) extends Referrable[G]
+case class RefBipStatePredicate[G](decl: BipStatePredicate[G]) extends Referrable[G]
+case class RefBipTransition[G](decl: BipTransition[G]) extends Referrable[G]
+case class RefBipTransitionSynchronization[G](decl: BipTransitionSynchronization[G]) extends Referrable[G]
+case class RefBipConstructor[G](decl: BipConstructor[G]) extends Referrable[G]
 
 case class RefLlvmSpecFunction[G](decl: LlvmSpecFunction[G]) extends Referrable[G] with SpecInvocationTarget[G] with ResultTarget[G]
 case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G]

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

@@ -549,10 +549,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/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,8 +1748,9 @@ 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.args, bc.body, bc.requires)(bc.blame)
       case bc: BipComponent[Pre] =>
-        new BipComponent(bc.fqn, bc.constructors, res(bc.invariant), bc.initial)
+        new BipComponent(bc.fqn, res(bc.invariant), bc.initial)
       case bsp: BipStatePredicate[Pre] =>
         new BipStatePredicate(bool(bsp.expr))
       case trans: BipTransition[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 {