From 31db34d7a722c695e0b2087d48804bc6b056677c Mon Sep 17 00:00:00 2001 From: ArmborstL Date: Thu, 21 Mar 2024 21:02:59 +0100 Subject: [PATCH 1/4] add type coercion between int and bool for C. Also coerce pointers to bool. --- examples/technical/intBoolCoercion.c | 13 +++++++++ src/col/vct/col/ast/Node.scala | 3 +++ .../family/coercion/CoerceBoolCIntImpl.scala | 9 +++++++ .../family/coercion/CoerceCIntBoolImpl.scala | 9 +++++++ .../coercion/CoercePointerBoolImpl.scala | 10 +++++++ .../ast/family/coercion/CoercionImpl.scala | 3 +++ src/col/vct/col/feature/FeatureRainbow.scala | 3 +++ .../vct/col/typerules/CoercingRewriter.scala | 3 +++ src/col/vct/col/typerules/CoercionUtils.scala | 5 ++++ src/main/vct/main/stages/Transformation.scala | 1 + .../vct/rewrite/CIntBoolCoercion.scala | 27 +++++++++++++++++++ .../integration/examples/TechnicalSpec.scala | 2 ++ 12 files changed, 88 insertions(+) create mode 100644 examples/technical/intBoolCoercion.c create mode 100644 src/col/vct/col/ast/family/coercion/CoerceBoolCIntImpl.scala create mode 100644 src/col/vct/col/ast/family/coercion/CoerceCIntBoolImpl.scala create mode 100644 src/col/vct/col/ast/family/coercion/CoercePointerBoolImpl.scala create mode 100644 src/rewrite/vct/rewrite/CIntBoolCoercion.scala diff --git a/examples/technical/intBoolCoercion.c b/examples/technical/intBoolCoercion.c new file mode 100644 index 0000000000..83db38b739 --- /dev/null +++ b/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; +} \ No newline at end of file diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index df74796728..ea6a227db1 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/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] diff --git a/src/col/vct/col/ast/family/coercion/CoerceBoolCIntImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceBoolCIntImpl.scala new file mode 100644 index 0000000000..2265c591c5 --- /dev/null +++ b/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() + +} diff --git a/src/col/vct/col/ast/family/coercion/CoerceCIntBoolImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceCIntBoolImpl.scala new file mode 100644 index 0000000000..65950fb7b4 --- /dev/null +++ b/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() + +} diff --git a/src/col/vct/col/ast/family/coercion/CoercePointerBoolImpl.scala b/src/col/vct/col/ast/family/coercion/CoercePointerBoolImpl.scala new file mode 100644 index 0000000000..83aacdf24c --- /dev/null +++ b/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() +} diff --git a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala index 4d077bad02..8e09c6f068 100644 --- a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala +++ b/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 } } \ No newline at end of file diff --git a/src/col/vct/col/feature/FeatureRainbow.scala b/src/col/vct/col/feature/FeatureRainbow.scala index 0c6dfeb276..1b9f544789 100644 --- a/src/col/vct/col/feature/FeatureRainbow.scala +++ b/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 diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index e3e15c9150..651cb1f4ad 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/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 diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index e28cb832b5..4aadccbccf 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/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) diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index 4f3c8036b5..097dae3203 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/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, diff --git a/src/rewrite/vct/rewrite/CIntBoolCoercion.scala b/src/rewrite/vct/rewrite/CIntBoolCoercion.scala new file mode 100644 index 0000000000..056b724e3b --- /dev/null +++ b/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) + } + +} diff --git a/test/main/vct/test/integration/examples/TechnicalSpec.scala b/test/main/vct/test/integration/examples/TechnicalSpec.scala index 16289ba940..04e16d6900 100644 --- a/test/main/vct/test/integration/examples/TechnicalSpec.scala +++ b/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; From 18ffaaf0387bd9f907a318a7d4335e36d90a7036 Mon Sep 17 00:00:00 2001 From: ArmborstL Date: Fri, 22 Mar 2024 14:10:07 +0100 Subject: [PATCH 2/4] int/bool coercion: incorporated PR feedback --- src/col/vct/col/ast/family/coercion/CoercionImpl.scala | 4 ++-- src/col/vct/col/typerules/CoercionUtils.scala | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala index 8e09c6f068..d12ee7301b 100644 --- a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala @@ -10,8 +10,8 @@ trait CoercionImpl[G] extends CoercionFamilyOps[G] { this: Coercion[G] => case CoerceDecreasePrecision(_, _) => false case CoerceCFloatCInt(_) => false case CoercionSequence(coercions) => coercions.forall(_.isCPromoting) - case CoerceJoinUnion(inner, _, _) => inner.forall(_.isPromoting) - case CoerceSelectUnion(inner, _, _, _) => inner.isPromoting + case CoerceJoinUnion(inner, _, _) => inner.forall(_.isCPromoting) + case CoerceSelectUnion(inner, _, _, _) => inner.isCPromoting case CoerceMapOption(inner, _, _) => inner.isCPromoting case CoerceMapTuple(inner, _, _) => inner.forall(_.isCPromoting) case CoerceMapEither(inner, _, _) => inner._1.isCPromoting && inner._2.isCPromoting diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 4aadccbccf..589c269782 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -92,7 +92,7 @@ case object CoercionUtils { case (source: FloatType[G], TRational()) => CoerceFloatRat(source) case (TBool(), TCInt()) => CoerceBoolCInt() case (TCInt(), TBool()) => CoerceCIntBool() - case (TCInt(), TResource()) => CoerceCIntBool() + case (TCInt(), TResource()) => CoercionSequence(Seq(CoerceCIntBool(), CoerceBoolResource())) case (TPointer(_), TBool()) => CoercePointerBool() case (CTPointer(_), TBool()) => CoercePointerBool() From d9402ac0b70b02141119700147b6312d86478324 Mon Sep 17 00:00:00 2001 From: Armborst Date: Tue, 23 Apr 2024 17:27:55 +0200 Subject: [PATCH 3/4] allow explicit cast from int to boolean and vice versa --- src/rewrite/vct/rewrite/lang/LangCToCol.scala | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index 5718d5f263..4e7f1f9516 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -309,6 +309,13 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz NewPointerArray(rw.dispatch(t1), size)(ArrayMallocFailed(inv))(c.o) case CCast(CInvocation(CLocal("__vercors_malloc"), _, _, _), _) => throw UnsupportedMalloc(c) case CCast(n@Null(), t) if t.asPointer.isDefined => rw.dispatch(n) + case CCast(e, t) if getBaseType(e.t)==TBool[Pre]() && getBaseType(t)==TCInt[Pre]() => + val zero = new CIntegerValue[Post](0)(e.o) + val one = new CIntegerValue[Post](1)(e.o) + new Select[Post](rw.dispatch(e), one, zero)(e.o) + case CCast(e, t) if getBaseType(t)==TBool[Pre]() && getBaseType(e.t)==TCInt[Pre]() => + val zero = new CIntegerValue[Post](0)(e.o) + new Neq[Post](rw.dispatch(e), zero)(e.o) case _ => throw UnsupportedCast(c) } From 0e8d8a5a10952127bc264a087d4d2343aecd54a1 Mon Sep 17 00:00:00 2001 From: Armborst Date: Tue, 23 Apr 2024 18:17:59 +0200 Subject: [PATCH 4/4] Try having _Bool be an integer internally. Let's see what the CI says... --- src/col/vct/col/resolve/lang/C.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/col/vct/col/resolve/lang/C.scala b/src/col/vct/col/resolve/lang/C.scala index 60eb22603c..836d0bf34f 100644 --- a/src/col/vct/col/resolve/lang/C.scala +++ b/src/col/vct/col/resolve/lang/C.scala @@ -72,7 +72,7 @@ case object C { case Seq(CFloat()) => C_ieee754_32bit() case Seq(CDouble()) => C_ieee754_64bit() case Seq(CLong(), CDouble()) => C_ieee754_64bit() - case Seq(CBool()) => TBool() + case Seq(CBool()) => TCInt() case Seq(defn @ CTypedefName(_)) => Types.notAValue(defn.ref.get) case Seq(CSpecificationType(typ)) => typ case Seq(defn @ CStructSpecifier(_)) => CTStruct(defn.ref.get.decl.ref)