Dead Code Elimination Transformation

[just-max]

Dead code elimination transformation as suggested by Simmo in #850. The implementation in its current state is still quite messy, but all the important bits should be there.

The transformation:

• removes dead code (statements) within functions
• removes functions that are entirely dead
• using CIL Rmtmps/RmUnused, tracks references between globals (functions, variables, named types, struct/union types, enums), then removes any that aren't referenced (possibly transitively) by live code

This PR also makes small changes to the transformation subsystem:

• expand query/ask for access to liveness information
• streamline output to file

Merging will close #850.

TODO:

• Clean up code, move all to own module
• Put transformation behind appropriate option and clean up output to file

[just-max]

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.

[michael-schwarz]

As soon as you have convinced yourself that the issue with gotos mentioned above is a non-issue, I think this is ready to merge!

[michael-schwarz]

@sim642 any comments before we merge?

[sim642]

How does this handle the fact that there isn't a one-to-one correspondance between our CFG nodes (which we compute liveness for) and CIL statements?
That is, our CFG construction skips over many CIL statements, so we don't compute liveness for many of them. Evene moreso, CfgTools never puts Block statements into nodes (which are handled here), but instead Instr statements (which are left into the default true case here).

It would be good to have (e.g. cram) tests for this that really show all aspects working, because I'm not entirely convinced right now.
CIL transformations working at the level of statements and locations instead of our CFG nodes has been an issue in the past (other transformations have a bunch of hackery regarding this), so it's odd that this transformation can get away with not needing any such special treatment.

[just-max]

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:

analyzer/src/transform/deadCode.ml

Lines 15 to 18 in 8d86284

	and impl_stmt stmt =
	if not (f stmt) then false
	else
	match stmt.skind with

---

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.

[just-max]

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).

[just-max]

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!

[michael-schwarz]

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!

[just-max]

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