utwente-fmt / vercors

The VerCors verification toolset for verifying parallel and concurrent software
https://utwente.nl/vercors
Mozilla Public License 2.0
55 stars 26 forks source link

Bool/Int type coercion #1170

Open ArmborstL opened 6 months ago

ArmborstL commented 6 months ago

Before merging this PR, please check the following:

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 commented 6 months ago

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 https://github.com/utwente-fmt/vercors/blob/9ad14fc3ba0c637eb79275df16d279044fcee850/src/col/vct/col/ast/lang/sycl/SYCLTBufferImpl.scala#L24, 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 https://github.com/utwente-fmt/vercors/blob/9ad14fc3ba0c637eb79275df16d279044fcee850/src/col/vct/col/typerules/CoercionUtils.scala#L74, 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?