Bool/Int type coercion

examples/technical/intBoolCoercion.c

@@ -0,0 +1,13 @@
+
+//@ requires i;
+void check(int i) {
+  if(!i) {
+    //@ assert false;
+  }
+}
+
+void main() {
+  check(5==5);
+  int *p;
+  if(!p) return;
+}

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

@@ -140,28 +140,30 @@ final case class TVar[G](ref: Ref[G, Variable[G]])(
     implicit val o: Origin = DiagnosticOrigin
 ) extends Type[G] with TVarImpl[G]
 final case class TConst[G](inner: Type[G])(
-  implicit val o: Origin = DiagnosticOrigin
+    implicit val o: Origin = DiagnosticOrigin
 ) extends Type[G] with TConstImpl[G]
 final case class TUnique[G](inner: Type[G], unique: BigInt)(
-  implicit val o: Origin = DiagnosticOrigin
+    implicit val o: Origin = DiagnosticOrigin
 ) extends Type[G] with TUniqueImpl[G]
-final case class CTStructUnique[G](inner: Type[G], pointerFieldRef: Ref[G, CStructMemberDeclarator[G]], unique: BigInt)(
-  implicit val o: Origin = DiagnosticOrigin
-) extends CType[G] with CTStructUniqueImpl[G]
-
+final case class CTStructUnique[G](
+    inner: Type[G],
+    pointerFieldRef: Ref[G, CStructMemberDeclarator[G]],
+    unique: BigInt,
+)(implicit val o: Origin = DiagnosticOrigin)
+    extends CType[G] with CTStructUniqueImpl[G]
 
 sealed trait PointerType[G] extends Type[G] with PointerTypeImpl[G]
 final case class TPointer[G](element: Type[G], unique: Option[BigInt])(
-  implicit val o: Origin = DiagnosticOrigin
+    implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TPointerImpl[G]
 final case class TNonNullPointer[G](element: Type[G], unique: Option[BigInt])(
-  implicit val o: Origin = DiagnosticOrigin
+    implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TNonNullPointerImpl[G]
 final case class TConstPointer[G](pureElement: Type[G])(
-  implicit val o: Origin = DiagnosticOrigin
+    implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TConstPointerImpl[G]
 final case class TNonNullConstPointer[G](pureElement: Type[G])(
-  implicit val o: Origin = DiagnosticOrigin
+    implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TNonNullConstPointerImpl[G]
 
 sealed trait CompositeType[G] extends Type[G] with CompositeTypeImpl[G]
@@ -256,9 +258,11 @@ final case class TByValueClass[G](
     typeArgs: Seq[Type[G]],
 )(implicit val o: Origin = DiagnosticOrigin)
     extends TClass[G] with TByValueClassImpl[G]
-final case class TClassUnique[G](inner: Type[G], uniqueMap: Seq[(Ref[G, InstanceField[G]], BigInt)])(
-  implicit val o: Origin = DiagnosticOrigin
-) extends TClass[G] with TClassUniqueImpl[G]
+final case class TClassUnique[G](
+    inner: Type[G],
+    uniqueMap: Seq[(Ref[G, InstanceField[G]], BigInt)],
+)(implicit val o: Origin = DiagnosticOrigin)
+    extends TClass[G] with TClassUniqueImpl[G]
 final case class TAnyClass[G]()(implicit val o: Origin = DiagnosticOrigin)
     extends DeclaredType[G] with TAnyClassImpl[G]
 final case class TAxiomatic[G](
@@ -371,15 +375,15 @@ final case class SpecIgnoreEnd[G]()(implicit val o: Origin)
 sealed trait NormallyCompletingStatement[G]
     extends Statement[G] with NormallyCompletingStatementImpl[G]
 sealed trait AssignStmt[G]
-  extends NormallyCompletingStatement[G] with AssignStmtImpl[G]
+    extends NormallyCompletingStatement[G] with AssignStmtImpl[G]
 final case class Assign[G](target: Expr[G], value: Expr[G])(
     val blame: Blame[AssignFailed]
 )(implicit val o: Origin)
     extends AssignStmt[G] with AssignImpl[G]
 final case class AssignInitial[G](target: Expr[G], value: Expr[G])(
-  val blame: Blame[AssignFailed]
+    val blame: Blame[AssignFailed]
 )(implicit val o: Origin)
-  extends AssignStmt[G] with AssignInitialImpl[G]
+    extends AssignStmt[G] with AssignInitialImpl[G]
 final case class Send[G](decl: SendDecl[G], delta: BigInt, res: Expr[G])(
     val blame: Blame[SendFailed]
 )(implicit val o: Origin)
@@ -999,40 +1003,43 @@ final case class CoercionSequence[G](coercions: Seq[Coercion[G]])(
     implicit val o: Origin
 ) extends Coercion[G] with CoercionSequenceImpl[G]
 
-final case class CoerceBetweenUnique[G](sourceId: BigInt, targetId: BigInt, innerCoercion: Coercion[G])(
-  implicit val o: Origin
-) extends Coercion[G] with CoerceBetweenUniqueImpl[G]
+final case class CoerceBetweenUnique[G](
+    sourceId: BigInt,
+    targetId: BigInt,
+    innerCoercion: Coercion[G],
+)(implicit val o: Origin)
+    extends Coercion[G] with CoerceBetweenUniqueImpl[G]
 final case class CoerceToUnique[G](source: Type[G], targetId: BigInt)(
-  implicit val o: Origin
+    implicit val o: Origin
 ) extends Coercion[G] with CoerceToUniqueImpl[G]
 final case class CoerceFromUnique[G](target: Type[G], sourceId: BigInt)(
-  implicit val o: Origin
+    implicit val o: Origin
 ) extends Coercion[G] with CoerceFromUniqueImpl[G]
 
 final case class CoerceToUniquePointer[G](source: Type[G], target: Type[G])(
-  implicit val o: Origin
+    implicit val o: Origin
 ) extends Coercion[G] with CoerceToUniquePointerImpl[G]
 final case class CoerceFromUniquePointer[G](source: Type[G], target: Type[G])(
-  implicit val o: Origin
+    implicit val o: Origin
 ) extends Coercion[G] with CoerceFromUniquePointerImpl[G]
-final case class CoerceBetweenUniquePointer[G](source: Type[G], target: Type[G])(
-  implicit val o: Origin
-) extends Coercion[G] with CoerceBetweenUniquePointerImpl[G]
+final case class CoerceBetweenUniquePointer[G](
+    source: Type[G],
+    target: Type[G],
+)(implicit val o: Origin)
+    extends Coercion[G] with CoerceBetweenUniquePointerImpl[G]
 
 final case class CoerceBetweenUniqueClass[G](source: Type[G], target: Type[G])(
-  implicit val o: Origin
+    implicit val o: Origin
 ) extends Coercion[G] with CoerceBetweenUniqueClassImpl[G]
 final case class CoerceBetweenUniqueStruct[G](source: Type[G], target: Type[G])(
-  implicit val o: Origin
+    implicit val o: Origin
 ) extends Coercion[G] with CoerceBetweenUniqueStructImpl[G]
 
-final case class CoerceToConst[G](source: Type[G])(
-  implicit val o: Origin
-) extends Coercion[G] with CoerceToConstImpl[G]
+final case class CoerceToConst[G](source: Type[G])(implicit val o: Origin)
+    extends Coercion[G] with CoerceToConstImpl[G]
 
-final case class CoerceFromConst[G](target: Type[G])(
-  implicit val o: Origin
-) extends Coercion[G] with CoerceFromConstImpl[G]
+final case class CoerceFromConst[G](target: Type[G])(implicit val o: Origin)
+    extends Coercion[G] with CoerceFromConstImpl[G]
 
 final case class CoerceNothingSomething[G](target: Type[G])(
     implicit val o: Origin
@@ -1080,9 +1087,8 @@ final case class CoerceNullJavaClass[G](
     extends Coercion[G] with CoerceNullJavaClassImpl[G]
 final case class CoerceNullAnyClass[G]()(implicit val o: Origin)
     extends Coercion[G] with CoerceNullAnyClassImpl[G]
-final case class CoerceNullPointer[G](target: Type[G])(
-    implicit val o: Origin
-) extends Coercion[G] with CoerceNullPointerImpl[G]
+final case class CoerceNullPointer[G](target: Type[G])(implicit val o: Origin)
+    extends Coercion[G] with CoerceNullPointerImpl[G]
 final case class CoerceNonNullPointer[G](target: Type[G])(
     implicit val o: Origin
 ) extends Coercion[G] with CoerceNonNullPointerImpl[G]
@@ -1121,6 +1127,13 @@ final case class CoerceCFloatFloat[G](source: Type[G], target: Type[G])(
 final case class CoerceIntRat[G]()(implicit val o: Origin)
     extends Coercion[G] with CoerceIntRatImpl[G]
 
+final case class CoerceBoolCInt[G]()(implicit val o: Origin)
+    extends Coercion[G] with CoerceBoolCIntImpl[G]
+final case class CoerceCIntBool[G]()(implicit val o: Origin)
+    extends Coercion[G] with CoerceCIntBoolImpl[G]
+final case class CoercePointerBool[G]()(implicit val o: Origin)
+    extends Coercion[G] with CoercePointerBoolImpl[G]
+
 final case class CoerceIncreasePrecision[G](source: Type[G], target: Type[G])(
     implicit val o: Origin
 ) extends Coercion[G] with CoerceIncreasePrecisionImpl[G]
@@ -2039,8 +2052,11 @@ final case class Select[G](
     extends Expr[G] with SelectImpl[G]
 final case class NewObject[G](cls: Ref[G, Class[G]])(implicit val o: Origin)
     extends Expr[G] with NewObjectImpl[G]
-final case class NewObjectUnique[G](cls: Ref[G, Class[G]], uniqueMap: Seq[(Ref[G, InstanceField[G]], BigInt)])(implicit val o: Origin)
-  extends Expr[G] with NewObjectUniqueImpl[G]
+final case class NewObjectUnique[G](
+    cls: Ref[G, Class[G]],
+    uniqueMap: Seq[(Ref[G, InstanceField[G]], BigInt)],
+)(implicit val o: Origin)
+    extends Expr[G] with NewObjectUniqueImpl[G]
 final case class NewArray[G](
     element: Type[G],
     dims: Seq[Expr[G]],
@@ -2049,25 +2065,30 @@ final case class NewArray[G](
 )(val blame: Blame[ArraySizeError])(implicit val o: Origin)
     extends Expr[G] with NewArrayImpl[G]
 sealed trait NewPointer[G] extends Expr[G] with NewPointerImpl[G]
-final case class NewPointerArray[G](element: Type[G], size: Expr[G], unique: Option[BigInt])(
-    val blame: Blame[ArraySizeError]
-)(implicit val o: Origin)
+final case class NewPointerArray[G](
+    element: Type[G],
+    size: Expr[G],
+    unique: Option[BigInt],
+)(val blame: Blame[ArraySizeError])(implicit val o: Origin)
     extends NewPointer[G] with NewPointerArrayImpl[G]
 final case class NewConstPointerArray[G](element: Type[G], size: Expr[G])(
-  val blame: Blame[ArraySizeError]
-)(implicit val o: Origin)
-  extends NewPointer[G] with NewConstPointerArrayImpl[G]
-final case class NewNonNullPointerArray[G](element: Type[G], size: Expr[G], unique: Option[BigInt])(
     val blame: Blame[ArraySizeError]
 )(implicit val o: Origin)
+    extends NewPointer[G] with NewConstPointerArrayImpl[G]
+final case class NewNonNullPointerArray[G](
+    element: Type[G],
+    size: Expr[G],
+    unique: Option[BigInt],
+)(val blame: Blame[ArraySizeError])(implicit val o: Origin)
     extends NewPointer[G] with NewNonNullPointerArrayImpl[G]
-final case class NewNonNullConstPointerArray[G](element: Type[G], size: Expr[G])(
-  val blame: Blame[ArraySizeError]
-)(implicit val o: Origin)
-  extends NewPointer[G] with NewNonNullConstPointerArrayImpl[G]
+final case class NewNonNullConstPointerArray[G](
+    element: Type[G],
+    size: Expr[G],
+)(val blame: Blame[ArraySizeError])(implicit val o: Origin)
+    extends NewPointer[G] with NewNonNullConstPointerArrayImpl[G]
 
 final case class UniquePointerCoercion[G](e: Expr[G], t: Type[G])(
-  implicit val o: Origin
+    implicit val o: Origin
 ) extends Expr[G] with UniquePointerCoercionImpl[G]
 final case class FreePointer[G](pointer: Expr[G])(
     val blame: Blame[PointerFreeError]
@@ -2839,9 +2860,10 @@ final case class CVolatile[G]()(implicit val o: Origin)
 final case class CAtomic[G]()(implicit val o: Origin)
     extends CTypeQualifier[G] with CAtomicImpl[G]
 final case class CUnique[G](i: BigInt)(implicit val o: Origin)
-  extends CTypeQualifier[G] with CUniqueImpl[G]
-final case class CUniquePointerField[G](name: String, i: BigInt)(implicit val o: Origin)
-  extends CTypeQualifier[G] with CUniquePointerFieldImpl[G] {
+    extends CTypeQualifier[G] with CUniqueImpl[G]
+final case class CUniquePointerField[G](name: String, i: BigInt)(
+    implicit val o: Origin
+) extends CTypeQualifier[G] with CUniquePointerFieldImpl[G] {
   var ref: Option[RefCStructField[G]] = None
 }
 

src/col/vct/col/ast/expr/heap/alloc/NewConstPointerArrayImpl.scala

@@ -4,7 +4,8 @@ import vct.col.ast.{NewConstPointerArray, TConstPointer, Type}
 import vct.col.ast.ops.NewConstPointerArrayOps
 import vct.col.print._
 
-trait NewConstPointerArrayImpl[G] extends NewConstPointerArrayOps[G] { this: NewConstPointerArray[G] =>
+trait NewConstPointerArrayImpl[G] extends NewConstPointerArrayOps[G] {
+  this: NewConstPointerArray[G] =>
   override lazy val t: Type[G] = TConstPointer[G](element)
 
   override def layout(implicit ctx: Ctx): Doc =

src/col/vct/col/ast/expr/heap/alloc/NewNonNullConstPointerArrayImpl.scala

@@ -4,7 +4,9 @@ import vct.col.ast.{NewNonNullConstPointerArray, Type, TNonNullConstPointer}
 import vct.col.ast.ops.NewNonNullConstPointerArrayOps
 import vct.col.print._
 
-trait NewNonNullConstPointerArrayImpl[G] extends NewNonNullConstPointerArrayOps[G] { this: NewNonNullConstPointerArray[G] =>
+trait NewNonNullConstPointerArrayImpl[G]
+    extends NewNonNullConstPointerArrayOps[G] {
+  this: NewNonNullConstPointerArray[G] =>
   override lazy val t: Type[G] = TNonNullConstPointer[G](element)
 
   override def layout(implicit ctx: Ctx): Doc =

src/col/vct/col/ast/expr/heap/alloc/NewNonNullPointerArrayImpl.scala

@@ -10,5 +10,8 @@ trait NewNonNullPointerArrayImpl[G] extends NewNonNullPointerArrayOps[G] {
 
   override def layout(implicit ctx: Ctx): Doc =
     Text("new") <>
-    (if(unique.nonEmpty) Text(" unique<" + unique.get.toString + ">") else Text("")) <+> element <> "[" <> size <> "]"
+      (if (unique.nonEmpty)
+         Text(" unique<" + unique.get.toString + ">")
+       else
+         Text("")) <+> element <> "[" <> size <> "]"
 }

src/col/vct/col/ast/expr/heap/alloc/NewObjectUniqueImpl.scala

@@ -6,9 +6,9 @@ import vct.col.ast.ops.NewObjectUniqueOps
 
 trait NewObjectUniqueImpl[G] extends NewObjectUniqueOps[G] {
   this: NewObjectUnique[G] =>
-  override def t: Type[G] = TClassUnique[G](cls.decl.classType(Seq()), uniqueMap)
+  override def t: Type[G] =
+    TClassUnique[G](cls.decl.classType(Seq()), uniqueMap)
 
   override def precedence: Int = Precedence.POSTFIX
-  override def layout(implicit ctx: Ctx): Doc =
-    Text("new") <+> t <> "()"
-    }
+  override def layout(implicit ctx: Ctx): Doc = Text("new") <+> t <> "()"
+}

src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala

@@ -10,5 +10,8 @@ trait NewPointerArrayImpl[G] extends NewPointerArrayOps[G] {
 
   override def layout(implicit ctx: Ctx): Doc =
     Text("new") <>
-      (if(unique.nonEmpty) Text(" unique<" + unique.get.toString + ">") else Text("")) <+> element <> "[" <> size <> "]"
+      (if (unique.nonEmpty)
+         Text(" unique<" + unique.get.toString + ">")
+       else
+         Text("")) <+> element <> "[" <> size <> "]"
 }

src/col/vct/col/ast/expr/heap/read/DerefImpl.scala

@@ -20,10 +20,13 @@ import vct.col.ast.ops.DerefOps
 
 trait DerefImpl[G] extends ExprImpl[G] with DerefOps[G] {
   this: Deref[G] =>
-  override def t: Type[G] = obj.t match {
-      case tc@TClassUnique(inner, uniqueMap) =>
-        uniqueMap.collectFirst {case (fieldRef, unique) if ref.decl == fieldRef.decl => addUniquePointer(inner, unique) }
-          .getOrElse(getT(tc))
+  override def t: Type[G] =
+    obj.t match {
+      case tc @ TClassUnique(inner, uniqueMap) =>
+        uniqueMap.collectFirst {
+          case (fieldRef, unique) if ref.decl == fieldRef.decl =>
+            addUniquePointer(inner, unique)
+        }.getOrElse(getT(tc))
       case t => getT(t)
     }
 

src/col/vct/col/ast/expr/misc/UniquePointerCoercionImpl.scala

@@ -4,6 +4,7 @@ import vct.col.ast.UniquePointerCoercion
 import vct.col.ast.ops.UniquePointerCoercionOps
 import vct.col.print._
 
-trait UniquePointerCoercionImpl[G] extends UniquePointerCoercionOps[G] { this: UniquePointerCoercion[G] =>
+trait UniquePointerCoercionImpl[G] extends UniquePointerCoercionOps[G] {
+  this: UniquePointerCoercion[G] =>
 
 }

src/col/vct/col/ast/family/coercion/CoerceBetweenUniqueClassImpl.scala

@@ -4,5 +4,6 @@ import vct.col.ast.CoerceBetweenUniqueClass
 import vct.col.ast.ops.CoerceBetweenUniqueClassOps
 import vct.col.print._
 
-trait CoerceBetweenUniqueClassImpl[G] extends CoerceBetweenUniqueClassOps[G] { this: CoerceBetweenUniqueClass[G] =>
+trait CoerceBetweenUniqueClassImpl[G] extends CoerceBetweenUniqueClassOps[G] {
+  this: CoerceBetweenUniqueClass[G] =>
 }

src/col/vct/col/ast/family/coercion/CoerceBetweenUniqueImpl.scala

@@ -4,6 +4,7 @@ import vct.col.ast.{CoerceBetweenUnique, TUnique}
 import vct.col.ast.ops.CoerceBetweenUniqueOps
 import vct.col.print._
 
-trait CoerceBetweenUniqueImpl[G] extends CoerceBetweenUniqueOps[G] { this: CoerceBetweenUnique[G] =>
+trait CoerceBetweenUniqueImpl[G] extends CoerceBetweenUniqueOps[G] {
+  this: CoerceBetweenUnique[G] =>
   override def target = TUnique(innerCoercion.target, targetId)
 }

src/col/vct/col/ast/family/coercion/CoerceBetweenUniquePointerImpl.scala

@@ -4,6 +4,8 @@ import vct.col.ast.CoerceBetweenUniquePointer
 import vct.col.ast.ops.CoerceBetweenUniquePointerOps
 import vct.col.print._
 
-trait CoerceBetweenUniquePointerImpl[G] extends CoerceBetweenUniquePointerOps[G] { this: CoerceBetweenUniquePointer[G] =>
+trait CoerceBetweenUniquePointerImpl[G]
+    extends CoerceBetweenUniquePointerOps[G] {
+  this: CoerceBetweenUniquePointer[G] =>
 
 }

src/col/vct/col/ast/family/coercion/CoerceBetweenUniqueStructImpl.scala

@@ -4,5 +4,6 @@ import vct.col.ast.CoerceBetweenUniqueStruct
 import vct.col.ast.ops.CoerceBetweenUniqueStructOps
 import vct.col.print._
 
-trait CoerceBetweenUniqueStructImpl[G] extends CoerceBetweenUniqueStructOps[G] { this: CoerceBetweenUniqueStruct[G] =>
+trait CoerceBetweenUniqueStructImpl[G] extends CoerceBetweenUniqueStructOps[G] {
+  this: CoerceBetweenUniqueStruct[G] =>
 }

src/col/vct/col/ast/family/coercion/CoerceBoolCIntImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceBoolCInt, TBool}
+import vct.col.ast.ops.CoerceBoolCIntOps
+
+trait CoerceBoolCIntImpl[G] extends CoerceBoolCIntOps[G] { this: CoerceBoolCInt[G] =>
+  override def target: TBool[G] = TBool()
+
+}

src/col/vct/col/ast/family/coercion/CoerceCIntBoolImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceCIntBool, TBool}
+import vct.col.ast.ops.CoerceCIntBoolOps
+
+trait CoerceCIntBoolImpl[G] extends CoerceCIntBoolOps[G] { this: CoerceCIntBool[G] =>
+  override def target: TBool[G] = TBool()
+
+}

src/col/vct/col/ast/family/coercion/CoerceFromConstImpl.scala

@@ -4,6 +4,7 @@ import vct.col.ast.{CoerceFromConst, TConst, Type}
 import vct.col.ast.ops.CoerceFromConstOps
 import vct.col.print._
 
-trait CoerceFromConstImpl[G] extends CoerceFromConstOps[G] { this: CoerceFromConst[G] =>
+trait CoerceFromConstImpl[G] extends CoerceFromConstOps[G] {
+  this: CoerceFromConst[G] =>
   val source: Type[G] = TConst[G](target)
 }