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](element: Type[G])(
-  implicit val o: Origin = DiagnosticOrigin
+    implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TConstPointerImpl[G]
 final case class TNonNullConstPointer[G](element: 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)
@@ -692,8 +696,9 @@ final case class ModelDo[G](
 @family
 sealed trait GlobalDeclaration[G]
     extends Declaration[G] with GlobalDeclarationImpl[G]
-final class HeapVariable[G](val t: Type[G], val init: Option[Expr[G]])(implicit val o: Origin)
-    extends GlobalDeclaration[G] with HeapVariableImpl[G]
+final class HeapVariable[G](val t: Type[G], val init: Option[Expr[G]])(
+    implicit val o: Origin
+) extends GlobalDeclaration[G] with HeapVariableImpl[G]
 final class SimplificationRule[G](val axiom: Expr[G])(implicit val o: Origin)
     extends GlobalDeclaration[G] with SimplificationRuleImpl[G]
 @scopes[Variable]
@@ -999,40 +1004,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 +1088,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 +1128,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]
@@ -1485,7 +1499,7 @@ final case class PointerAdd[G](pointer: Expr[G], offset: Expr[G])(
 final case class AddrOf[G](e: Expr[G])(implicit val o: Origin)
     extends Expr[G] with AddrOfImpl[G]
 final case class AddrOfConstCast[G](e: Expr[G])(implicit val o: Origin)
-  extends Expr[G] with AddrOfConstCastImpl[G]
+    extends Expr[G] with AddrOfConstCastImpl[G]
 final case class FunctionOf[G](
     binding: Ref[G, Variable[G]],
     vars: Seq[Ref[G, Variable[G]]],
@@ -2041,8 +2055,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]],
@@ -2051,25 +2068,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]
@@ -2841,9 +2863,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/declaration/global/HeapVariableImpl.scala

@@ -7,13 +7,14 @@ import vct.col.ast.ops.HeapVariableOps
 trait HeapVariableImpl[G] extends HeapVariableOps[G] {
   this: HeapVariable[G] =>
   override def layout(implicit ctx: Ctx): Doc = {
-    val decl: Doc = ctx.syntax match {
-      case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP =>
-        val (spec, decl) = t.layoutSplitDeclarator
-        spec <+> decl <> ctx.name(this)
-      case _ => t.show <+> ctx.name(this)
+    val decl: Doc =
+      ctx.syntax match {
+        case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP =>
+          val (spec, decl) = t.layoutSplitDeclarator
+          spec <+> decl <> ctx.name(this)
+        case _ => t.show <+> ctx.name(this)
 
-    }
+      }
     decl <> init.map(i => Text(" = ") <> i).getOrElse(Text("")) <> ";"
   }
 }

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/AddrOfConstCastImpl.scala

@@ -4,7 +4,8 @@ import vct.col.ast.{AddrOfConstCast, TConst}
 import vct.col.ast.ops.AddrOfConstCastOps
 import vct.col.print._
 
-trait AddrOfConstCastImpl[G] extends AddrOfConstCastOps[G] { this: AddrOfConstCast[G] =>
+trait AddrOfConstCastImpl[G] extends AddrOfConstCastOps[G] {
+  this: AddrOfConstCast[G] =>
   override lazy val t = TConst(e.t)
 
   override def layout(implicit ctx: Ctx): Doc = Text("constCast(") <> e <> ")"

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

@@ -1,6 +1,14 @@
 package vct.col.ast.expr.heap.read
 
-import vct.col.ast.{AddrOf, AddrOfConstCast, TPointer, TConstPointer, Type, DerefPointer, AmbiguousSubscript}
+import vct.col.ast.{
+  AddrOf,
+  AddrOfConstCast,
+  TPointer,
+  TConstPointer,
+  Type,
+  DerefPointer,
+  AmbiguousSubscript,
+}
 import vct.col.print._
 import vct.col.ast.ops.AddrOfOps
 

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] =>
 
 }