cil icon indicating copy to clipboard operation
cil copied to clipboard

`Formatcil` doesn't insert implicit casts

Open sim642 opened this issue 2 years ago • 0 comments

Formatcil can parse the following expression (from Goblint's Apron analysis): 2147483647LL - (long long )top >= 0. When Goblint evaluates the parsed expression, it crashes with:

exception IntDomain.IncompatibleIKinds("ikinds long long and int are incompatible. Values: (Unknown int([0,32])) and (0)")

Turns out Formatcil doesn't insert implicit casts on both sides of the comparison to make the types same: https://github.com/goblint/cil/blob/56f5f9ad58e71908ff66e179e056a22ea71693a2/src/formatparse.mly#L87-L92 Even worse, it uses the type of the left argument as the type of any binary operator expression, which is also blatantly incorrect.

Meanwhile Frontc does the appropriate conversion to deduce the result type and inserts the necessary casts: https://github.com/goblint/cil/blob/56f5f9ad58e71908ff66e179e056a22ea71693a2/src/frontc/cabs2cil.ml#L4915-L4920

It's starting to look more and more unlikely that we can keep abusing Formatcil to parse individual expressions.

sim642 avatar May 24 '22 14:05 sim642