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

@@ -393,6 +393,9 @@ final case class CoerceCIntCFloat[G](target: Type[G])(implicit val o: Origin) ex
 final case class CoerceCIntInt[G]()(implicit val o: Origin) extends Coercion[G] with CoerceCIntIntImpl[G]
 final case class CoerceCFloatFloat[G](source: Type[G], target: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceCFloatFloatImpl[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]
 final case class CoerceDecreasePrecision[G](source: Type[G], target: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceDecreasePrecisionImpl[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/CoercePointerBoolImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.ops.CoercePointerBoolOps
+import vct.col.ast.{CoercePointerBool, TBool}
+
+trait CoercePointerBoolImpl[G] extends CoercePointerBoolOps[G] {
+  this: CoercePointerBool[G] =>
+  // override def layout(implicit ctx: Ctx): Doc = ???
+  override def target: TBool[G] = TBool()
+}

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

@@ -79,5 +79,8 @@ trait CoercionImpl[G] extends CoercionFamilyOps[G] { this: Coercion[G] =>
     case CoerceCFloatFloat(_, _) => true
     case CoerceDecreasePrecision(_, _) => false
     case CoerceCFloatCInt(_) => false
+    case CoerceBoolCInt() => true
+    case CoerceCIntBool() => false
+    case CoercePointerBool() => false
   }
 }

src/col/vct/col/feature/FeatureRainbow.scala

@@ -120,6 +120,9 @@ class FeatureRainbow[G] {
     case node: CoerceIdentity[G] => Coercions
     case node: CoerceIncreasePrecision[G] => Coercions
     case node: CoerceIntRat[G] => Coercions
+    case node: CoerceBoolCInt[G] => Coercions
+    case node: CoerceCIntBool[G] => Coercions
+    case node: CoercePointerBool[G] => Coercions
     case node: CoerceJavaClassAnyClass[G] => Coercions
     case node: CoerceJavaSupports[G] => Coercions
     case node: CoerceJoinUnion[G] => Coercions

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -206,6 +206,9 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
       case CoerceRatZFrac() => e
       case CoerceZFracFrac() => e
 
+      case CoerceBoolCInt() => e
+      case CoerceCIntBool() => e
+      case CoercePointerBool() => e
       case CoerceDecreasePrecision(_, _) => e
       case CoerceCFloatCInt(_) => e
       case CoerceCIntCFloat(_) => e

src/col/vct/col/typerules/CoercionUtils.scala

@@ -90,6 +90,11 @@ case object CoercionUtils {
       case (TFraction(), TRational()) => CoercionSequence(Seq(CoerceFracZFrac(), CoerceZFracRat()))
       case (TZFraction(), TRational()) => CoerceZFracRat()
       case (source: FloatType[G], TRational()) => CoerceFloatRat(source)
+      case (TBool(), TCInt()) => CoerceBoolCInt()
+      case (TCInt(), TBool()) => CoerceCIntBool()
+      case (TCInt(), TResource()) => CoerceCIntBool()
+      case (TPointer(_), TBool()) => CoercePointerBool()
+      case (CTPointer(_), TBool()) => CoercePointerBool()
 
       case (source @ TFloat(exponentL, mantissaL), target @ TFloat(exponentR, mantissaR)) if exponentL <= exponentR && mantissaL <= mantissaR =>
         CoerceIncreasePrecision(source, target)

src/main/vct/main/stages/Transformation.scala

@@ -177,6 +177,7 @@ case class SilverTransformation
 ) extends Transformation(onBeforePassKey, onAfterPassKey, Seq(
     // Replace leftover SYCL types
     ReplaceSYCLTypes,
+    CIntBoolCoercion,
     CFloatIntCoercion,
 
     ComputeBipGlue,

src/rewrite/vct/rewrite/CIntBoolCoercion.scala

@@ -0,0 +1,27 @@
+package vct.col.rewrite
+
+import vct.col.ast._
+import vct.col.origin.Origin
+import vct.col.typerules.CoercingRewriter
+
+case object CIntBoolCoercion extends RewriterBuilder {
+  override def key: String = "CIntBool"
+  override def desc: String = "Introduce an explicit node to convert integers to boolean and vice versa for C."
+}
+
+case class CIntBoolCoercion[Pre <: Generation]() extends CoercingRewriter[Pre] {
+  override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])(implicit o: Origin): Expr[Post] = coercion match {
+    case CoerceBoolCInt() =>
+      val zero = new CIntegerValue[Post](0)
+      val one = new CIntegerValue[Post](1)
+      new Select[Post](e, one, zero)
+    case CoerceCIntBool() =>
+      val zero = new CIntegerValue[Post](0)
+      new Neq[Post](e, zero)
+    case CoercePointerBool() =>
+      val ptr = new Null[Post]()
+      new Neq[Post](e, ptr)
+    case other => super.applyCoercion(e, other)
+  }
+
+}

test/main/vct/test/integration/examples/TechnicalSpec.scala

@@ -434,6 +434,8 @@ vercors should verify using silicon in "example using string primitive" pvl
 
   vercors should verify using anyBackend example "technical/labeledEmbeddedStatement.c"
 
+  vercors should verify using anyBackend example "technical/intBoolCoercion.c"
+
   vercors should verify using anyBackend in "usage of given/yields in C" c """
     /*@
     given int x;