aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Deadcode.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2017-09-18 15:03:20 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2017-09-18 15:08:24 +0200
commit93d2fc9e3b23d69c0c97d229f9fa4ab36079f507 (patch)
tree3f54c9ecc6954ed51426c19db93097b6896431e6 /backend/Deadcode.v
parentc4dcf7c08016f175ba6c06d20c530ebaaad67749 (diff)
downloadcompcert-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/Deadcode.v')
-rw-r--r--backend/Deadcode.v5
1 files changed, 4 insertions, 1 deletions
diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index f491d678..9cbe5054 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -143,7 +143,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t)
| Some(Ibuiltin ef args res s) =>
transfer_builtin approx!!pc ef args res ne nm
| Some(Icond cond args s1 s2) =>
- (add_needs args (needs_of_condition cond) ne, nm)
+ if peq s1 s2 then after else
+ (add_needs args (needs_of_condition cond) ne, nm)
| Some(Ijumptable arg tbl) =>
(add_need_all arg ne, nm)
| Some(Ireturn optarg) =>
@@ -191,6 +192,8 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t)
if nmem_contains (snd an!!pc) (aaddr_arg approx!!pc dst) sz
then instr
else Inop s
+ | Icond cond args s1 s2 =>
+ if peq s1 s2 then Inop s1 else instr
| _ =>
instr
end.