Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Formatcil doesn't insert implicit casts #95

Open
sim642 opened this issue May 24, 2022 · 0 comments
Open

Formatcil doesn't insert implicit casts #95

sim642 opened this issue May 24, 2022 · 0 comments
Labels

Comments

@sim642
Copy link
Member

sim642 commented May 24, 2022

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:

cil/src/formatparse.mly

Lines 87 to 92 in 56f5f9a

let doBinop bop e1t e2t =
((fun args ->
let e1 = (fst e1t) args in
let e2 = (fst e2t) args in
let t1 = typeOf e1 in
BinOp(bop, e1, e2, t1)),

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:

cil/src/frontc/cabs2cil.ml

Lines 4915 to 4920 in 56f5f9a

let doArithmeticComp () =
let tres = arithmeticConversion t1 t2 in
(* Keep the operator since it is arithmetic *)
intType,
optConstFoldBinOp false bop
(makeCastT ~e:e1 ~oldt:t1 ~newt:tres) (makeCastT ~e:e2 ~oldt:t2 ~newt:tres) intType

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant