#126 Switch-case simplification issue adds wrong cast

Bug
closed-fixed
nobody
5
2012-05-29
2012-01-29
Arie
No

We are using CIL in a concolic test generation tool in INTEL.
We use CIL library and API to instrument C source for producing traces for symbolic simulation of a C program.

I believe there is a bug in the switch case statement simplification in CIL (I don't use the trunk so it might been fixed already).
The issue is best explained by an example.
Here is a source snippet before simplification:

switch (x) {
case 33554432ull: …
And here is the simplified snippet:
if ((int ) x == 3554432ull){

Obviously CIL changes the semantics of the original code by introducing an unnecessary cast to “int”.
This is an unfortunate bug that breaks our entire simulation and the instrumented code correctness.

Discussion

  • Arie

    Arie - 2012-01-29

    Note; x is defined as unsigned long long

     
  • Jim Grundy

    Jim Grundy - 2012-02-03

    The bug here is not that the switch expression was cast to int, but that the case expression was not also cast to int. The C standard says that both expressions should be ints (Section 6.8.4.2 points 1 and 3). In casting only one expression to an int but not the other we get a situation where the case can't match, but if they were both cast to int they could.

     
  • Jim Grundy

    Jim Grundy - 2012-02-03

    The following patch to src/cil.ml seems like a fix:

    6549c6549
    < let make_eq exp = BinOp(Eq,e,exp,intType) in
    ---
    > let make_eq exp = BinOp(Eq, e, mkCast exp intType, intType) in

     
  • Gabriel Kerneis

    Gabriel Kerneis - 2012-05-29

    I believe this has been fixed in the git version (commit 64778b7). Please reopen the bug otherwise.

     
  • Gabriel Kerneis

    Gabriel Kerneis - 2012-05-29
    • status: open --> closed-fixed
     

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks