As discussed with Michael, a final change would be to rename the Rmtmps CIL module, since it removes much more than temporaries. I would suggest merging this first, then refactoring to the new CIL API in a separate PR.

There should be no more material changes to this pull request.

@sim642 any comments before we merge?

How does this handle the fact that there isn't a one-to-one correspondence between our CFG nodes (which we compute liveness for) and CIL statements?

Edit: Looks like I still had some misunderstandings about CFG construction. The current implementation kind of gets lucky; if statements and while loops have a location that corresponds to the condition node in the CFG, and are thus kept if the condition node is live, and single Instr and Return statements do all directly map to nodes in the CFG for which liveness can be checked.

All other CIL statements, which are not in the CFG at all, are always kept. This includes plain Block statements.
This also means though that e.g. Goto statements are not removed, since they don't appear as nodes in the CFG.

To do things properly, it looks like it is necessary to traverse through CIL statements in the same way as CFG construction. Then, liveness of If, Loop and Instr/Return can be checked as before, but liveness of anything else would be decided by liveness of the preceding CFG node.

Original comment:

CIL statements are put in three categories by this transformation:

• in the (solver) result, dead in all contexts
• in the result, but live in some contexts
• not in the result

Only the first category is removed. Block statements fall under the third category, and are not removed.

(By "result" I mean the lh hashtable of solver results by CFG node and context.)

which are left into the default true case here

The case distinction only handles the recursion. A dead Instr is removed above:

CIL transformations working at the level of statements and locations instead of our CFG nodes has been an issue in the past

Yes, it's not the prettiest. But ultimately the transformation must occur on a syntax level on the original CIL file, short of regenerating the C code from scratch out of the CFG. From my understanding, other transformations need a bit of a hack because they go through the query system. This transformation sort of gets around that with the new Transform.queries must_be_dead parameter, which directly looks up a statement/location in the map of results joined by statement/location. As long as each CFG node corresponds to one CIL statement, this should work.

Edit: it would probably make sense for transformations to work on statements/function declarations (i.e., pass those to ask), which makes things slightly better by not conflating e.g. a statement and a block containing only that statement.

To do things properly, it looks like it is necessary to traverse through CIL statements in the same way as CFG construction. Then, liveness of If, Loop and Instr/Return can be checked as before, but liveness of anything else would be decided by liveness of the preceding CFG node.

This is essentially what I've implemented now. Statements that are skipped during CFG construction are tracked directly. Then, a statement between two nodes is considered dead if the preceding or following node is dead (with appropriate handling for statements on multiple such paths).

Integrated review (ff9aa70...just-max:goblint-analyzer:deadcode_removal).

The regression cram tests are currently failing because apparently cram only sees an empty stdout. Probably some part of file redirection trickery in transform.sh not working right.

Of course it comes down to bash not waiting for processes inside process substitution. Fixed by using temp file instead.

Also, it probably never makes sense for cram tests to have backtraces enabled (in CI), since those are very fragile.

Edit: Making this work on Mac without having such a system locally is quite frustrating. The /bin/bash in the image is version 3.2, well on its way to being 20 years old!

Edit: Making this work on Mac without having such a system locally is quite frustrating.

I feel you, I have the same issue all the time myself too!

As Simmo suggested, I've used a string constant in dead conditions. Everything should be ready now.