diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-18 15:03:20 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-18 15:08:24 +0200 |
| commit | 93d2fc9e3b23d69c0c97d229f9fa4ab36079f507 (patch) | |
| tree | 3f54c9ecc6954ed51426c19db93097b6896431e6 /backend/Deadcodeproof.v | |
| parent | c4dcf7c08016f175ba6c06d20c530ebaaad67749 (diff) | |
| download | compcert-kvx-93d2fc9e3b23d69c0c97d229f9fa4ab36079f507.tar.gz compcert-kvx-93d2fc9e3b23d69c0c97d229f9fa4ab36079f507.zip | |
Deadcode: eliminate trivial Icond instructions
These are conditionals where the "ifso" and the "ifnot" successors are the same. By eliminating them here and not later, we can also eliminate the instructions that compute the arguments to the condition, if any.
There is another, later point where these trivial conditional instructions are eliminated: in the Tunneling phase. The elimination done in Tunneling is more powerful in that it works not just for conditionals whose two successors are the same, but also for conditionals whose two successors lead to the same point after a series of nops. The elimination done in Deadcode is more powerful in that it eliminates the instructions that compute the arguments to the condition. Hence it is worth having both eliminations.
Diffstat (limited to 'backend/Deadcodeproof.v')
| -rw-r--r-- | backend/Deadcodeproof.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 07c3f84a..e23fdfd3 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -1046,8 +1046,12 @@ Ltac UseTransfer := eapply mextends_agree; eauto. - (* conditional *) - TransfInstr; UseTransfer. + TransfInstr; UseTransfer. destruct (peq ifso ifnot). ++ replace (if b then ifso else ifnot) with ifso by (destruct b; congruence). econstructor; split. + eapply exec_Inop; eauto. + eapply match_succ_states; eauto. simpl; auto. ++ econstructor; split. eapply exec_Icond; eauto. eapply needs_of_condition_sound. eapply ma_perm; eauto. eauto. eauto with na. eapply match_succ_states; eauto 2 with na. |