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

[do not merge] work-in-progress dead code elimination #348

Open
wants to merge 15 commits into
base: master
Choose a base branch
from

Conversation

0adb
Copy link
Contributor

@0adb 0adb commented Apr 13, 2023

Work on implementing a compiler phase for replacing SSet's, SLit's and SOp's that target variables that are unread later in the function (or not live) with SSkip. Currently first pass of implementation is done, still need to work on proof of correctness.
Attached are screenshots of diffs of assembly code in compilerExamples/deadAssExample.v
img1
img2
img3

Copy link
Contributor

@samuelgruetter samuelgruetter left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks great 👍
Let me know if questions come up as you continue!

let deadAssignment' := deadAssignment used_after in
match s with
| SIf c s1 s2 => SIf c (deadAssignment' s1) (deadAssignment' s2)
| SLoop s1 c s2 => SLoop s1 c s2 (* loops are scary so skipping this case for now *)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hehe I agree that they are scary 😉 But they will also be important, because most loops contain something like i = i + 1, and UseImmediate will turn this into an Addi, creating an unused temporary for the value 1.
I would start by studying the SLoop case of live, and then try using a similar pattern as you used in the SSeq case of deadAssignment.

| SSeq s1 s2 =>
let s2' := deadAssignment' s2 in
let s1_used_after := live s2' used_after in
SSeq (deadAssignment s1_used_after s1) (s2')
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
SSeq (deadAssignment s1_used_after s1) (s2')
SSeq (deadAssignment s1_used_after s1) s2'

| CondNez x => [x]
end.

Fixpoint live(s: stmt var)(used_after: list var): list var :=
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This one should eventually go into its own file, abstract over the type of variables and their boolean equality, and be shared between this phase and the register allocator.

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

Successfully merging this pull request may close these issues.

2 participants