Bool/Int type coercion

[ArmborstL]

Before merging this PR, please check the following:

• I made sure the wiki is updated in accordance with the changes in this PR. For example, syntax changes, semantics changes, VerCors flags changes, etc.

PR description

Add type coercion between int and bool for C. Also coerce pointers to bool.

In C, integers can act as booleans (e.g. in if(myInt)), and booleans are just integers internally and can be passed as such, e.g. in

void check(int i) {}
void main() {
  check(0==0);
}

Therefore, implicit casting between those types should work.

Pointers are basically integers, so the same applies for them. E.g. after p=malloc(...), we might write if(!p)return;, treating the pointer as a boolean. This PR also covers that case.

[ArmborstL]

@sakehl I'm not sure what isCPromoting does. Should I add one of the coercions as a case there? In principle, I want all coercions to work in C code, so I'm reluctant to add e.g. CoerceCIntBool as false here, but it is not injective and thus not promoting...
Also, is it correct that some cases, like CoerceJoinUnion, call the regular isPromoting instead of the special C version isCPromoting? or is that just a copy-paste error?

[sakehl]

What I wanted to capture here is that float/double can only be demoted to int (and double to float) in:

• an assignment
• an argument of a function call
  I based this mostly on this reference and here

This is called demotion, and is only valid in those cases. More specifically it is not valid with arithmetic conversions. (so 5 % 4.0 is not a valid statement, since 4.0 cannot be demoted to an int here, and % does not work on floating point numbers).

Anyway it seems that boolean is a bit harder. When looking specifically at if-statements and logical and/or statements of C:
https://en.cppreference.com/w/c/language/operator_logical

They work for an expression of any scalar type. Which is of course not how we defined this internally in VerCors.

I think we can then best encode this to always allow demoting pointers and integers to booleans.

So in that case, I'd say that we put:

case CoerceCIntBool() => false
    case CoercePointerBool() => false
  }

both to true.

(.... what is C a messy language)

Also, is it correct that some cases, like CoerceJoinUnion, call the regular isPromoting instead of the special C version isCPromoting? or is that just a copy-paste error?

This is definitely a copy paste error, thanks for spotting it.

[ArmborstL]

I think we can then best encode this to always allow demoting pointers and integers to booleans.

Ok, then I leave it as-is and let the default case handle it.

This is definitely a copy paste error

Ok, I'll fix it :)

[ArmborstL]

A SYCL test (https://github.com/utwente-fmt/vercors/blob/9ad14fc3ba0c637eb79275df16d279044fcee850/examples/concepts/sycl/buffers/WrongGenericArgumentForConstructorHostdataType.cpp) fails in the CI. It is a negative test that tries to instantiate an int buffer with a bool array, which should fail. It still does, but now with a different error. @OmerSakar says it should still raise the original error, not the new one.

The problem occurs, because at

vercors/src/col/vct/col/ast/lang/sycl/SYCLTBufferImpl.scala

Line 24 in 9ad14fc

CPP.getBaseTypeFromSpecs[G](Seq(typeSpec)).superTypeOf(args.head.t.asPointer.get.element) && Util.compatTypes[G](args.tail, Seq(SYCLTRange[G](1))) =>

, we explicitly check "superTypeOf" of the pointed type, which used to fail, but now with the CInt/bool coercion, it succeeds. That's why the original error is no longer raised. However, at some later stage, we simply check coercion, and there it does not coerce the inner type (I'm guessing it's this one

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

Line 74 in 9ad14fc

case (CPPTArray(_, innerType), TArray(element)) if element == innerType =>

, but I'm not sure).

I suspect that the SYCLTBufferImpl should not check the contained type of the array, but maybe @OmerSakar or @pieter-bos disagree?