search

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 coercion for C is incomplete #1187

Open ArmborstL opened 5 months ago

ArmborstL commented 5 months ago

The PR #1170 started implementing a coercion between boolean and integer values in C, since booleans are a type of integer there. It works for simple examples like https://github.com/utwente-fmt/vercors/blob/9b74fd74a18ad232784329ba78fab55d623a1511/examples/technical/intBoolCoercion.c. But for the program below, it still fails on the comparison:

//@ ensures 0 <= \result ;
_Bool __VERIFIER_nondet_bool();

To type-check the AmbiguousLessEq operation, the CoercingRewriter tries to convert both sides to int. Here, \result has the type CPrimitiveType, which wraps a TBool. So I tried extending the coercion to this specific combination of types. However, it seems that at some point in the process, the node is assigned the simple type TBool. Afterwards, a NopCoercingRewriter tries to cast this TBool into an int, and fails.

I'm not sure what the solution here is. I think if we simply allow coercing TBool to int, then this would also enable the coercion in non-C cases, which we probably don't want. But how do we recognise for a specific case that we are working in C and should allow this coercion?

ArmborstL commented 5 months ago

Another option is to have _Bool be a TCInt rather than a TBool. Given that PR #1170 allows coercion from int to boolean, this should not cause too many problems, right? It would be closer to the C semantics, but probably further from the user's intentions.

ArmborstL commented 5 months ago

this should not cause too many problems, right?

So I tried it, and the CI fails in a few cases, e.g. https://github.com/utwente-fmt/vercors/actions/runs/8803794962/job/24163164935. It seems that coercing the boolean expression of the return statement into _Bool fails. I think it's because this https://github.com/utwente-fmt/vercors/blob/aef15a47cc9b77cd9a25da59dd08e6419873597e/src/rewrite/vct/rewrite/CFloatIntCoercion.scala#L24 turns the TCInt into TInt, preventing any further coercion to/from TBool. I'm not sure why this coercion is done, maybe @sakehl can explain it. For now, I'm not sure whether having _Bool be a TCInt is worth it, or whether it breaks more than it fixes 😕

sakehl commented 5 months ago

A few thought

But how do we recognise for a specific case that we are working in C and should allow this coercion?

This is exactly why I introduced TCInt. So we recognize when we come from a C program, and we want C like coercions between types. So you could make the type TCBool if you want.

The file CFloatIntCoercion.scala removes all 'C' types here, and adds the specific cast needed (only cast between integer types and floats here).

So if you want to coerce from TCInt to TBool, that is fine. But then you need to add the explicit cast. Probably with

CoerceCIntBool()? Or something?

Does that help?