diff options
Diffstat (limited to 'backend/Deadcode.v')
-rw-r--r-- | backend/Deadcode.v | 192 |
1 files changed, 192 insertions, 0 deletions
diff --git a/backend/Deadcode.v b/backend/Deadcode.v new file mode 100644 index 00000000..9efeca1a --- /dev/null +++ b/backend/Deadcode.v @@ -0,0 +1,192 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Elimination of unneeded computations over RTL. *) + +Require Import Coqlib. +Require Import Errors. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Memory. +Require Import Registers. +Require Import Op. +Require Import RTL. +Require Import Lattice. +Require Import Kildall. +Require Import ValueDomain. +Require Import ValueAnalysis. +Require Import NeedDomain. +Require Import NeedOp. + +(** * Part 1: the static analysis *) + +Definition add_need (r: reg) (nv: nval) (ne: nenv) : nenv := + NE.set r (nlub nv (NE.get r ne)) ne. + +Fixpoint add_needs (rl: list reg) (nv: nval) (ne: nenv) : nenv := + match rl with + | nil => ne + | r1 :: rs => add_need r1 nv (add_needs rs nv ne) + end. + +Definition add_ros_need (ros: reg + ident) (ne: nenv) : nenv := + match ros with + | inl r => add_need r All ne + | inr s => ne + end. + +Definition add_opt_need (or: option reg) (ne: nenv) : nenv := + match or with + | Some r => add_need r All ne + | None => ne + end. + +Definition kill (r: reg) (ne: nenv) : nenv := NE.set r Nothing ne. + +Definition is_dead (v: nval) := + match v with Nothing => true | _ => false end. + +Definition is_int_zero (v: nval) := + match v with I n => Int.eq n Int.zero | _ => false end. + +Function transfer_builtin (app: VA.t) (ef: external_function) (args: list reg) (res: reg) + (ne: NE.t) (nm: nmem) : NA.t := + match ef, args with + | EF_vload chunk, a1::nil => + (add_needs args All (kill res ne), + nmem_add nm (aaddr app a1) (size_chunk chunk)) + | EF_vload_global chunk id ofs, nil => + (add_needs args All (kill res ne), + nmem_add nm (Gl id ofs) (size_chunk chunk)) + | EF_vstore chunk, a1::a2::nil => + (add_need a1 All (add_need a2 (store_argument chunk) (kill res ne)), nm) + | EF_vstore_global chunk id ofs, a1::nil => + (add_need a1 (store_argument chunk) (kill res ne), nm) + | EF_memcpy sz al, dst::src::nil => + if nmem_contains nm (aaddr app dst) sz then + (add_needs args All (kill res ne), + nmem_add (nmem_remove nm (aaddr app dst) sz) (aaddr app src) sz) + else (ne, nm) + | EF_annot txt targs, _ => + (add_needs args All (kill res ne), nm) + | EF_annot_val txt targ, _ => + (add_needs args All (kill res ne), nm) + | _, _ => + (add_needs args All (kill res ne), nmem_all) + end. + +Definition transfer (f: function) (approx: PMap.t VA.t) + (pc: node) (after: NA.t) : NA.t := + let (ne, nm) := after in + match f.(fn_code)!pc with + | None => + NA.bot + | Some (Inop s) => + after + | Some (Iop op args res s) => + let nres := nreg ne res in + if is_dead nres then after + else if is_int_zero nres then (kill res ne, nm) + else (add_needs args (needs_of_operation op nres) (kill res ne), nm) + | Some (Iload chunk addr args dst s) => + let ndst := nreg ne dst in + if is_dead ndst then after + else if is_int_zero ndst then (kill dst ne, nm) + else (add_needs args All (kill dst ne), + nmem_add nm (aaddressing approx!!pc addr args) (size_chunk chunk)) + | Some (Istore chunk addr args src s) => + let p := aaddressing approx!!pc addr args in + if nmem_contains nm p (size_chunk chunk) + then (add_needs args All (add_need src (store_argument chunk) ne), + nmem_remove nm p (size_chunk chunk)) + else after + | Some(Icall sig ros args res s) => + (add_needs args All (add_ros_need ros (kill res ne)), nmem_all) + | Some(Itailcall sig ros args) => + (add_needs args All (add_ros_need ros NE.bot), + nmem_dead_stack f.(fn_stacksize)) + | 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) + | Some(Ijumptable arg tbl) => + (add_need arg All ne, nm) + | Some(Ireturn optarg) => + (add_opt_need optarg ne, nmem_dead_stack f.(fn_stacksize)) + end. + +Module DS := Backward_Dataflow_Solver(NA)(NodeSetBackward). + +Definition analyze (approx: PMap.t VA.t) (f: function): option (PMap.t NA.t) := + DS.fixpoint f.(fn_code) successors_instr + (transfer f approx). + +(** * Part 2: the code transformation *) + +Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t) + (pc: node) (instr: instruction) := + match instr with + | Iop op args res s => + let nres := nreg (fst an!!pc) res in + if is_dead nres then + Inop s + else if is_int_zero nres then + Iop (Ointconst Int.zero) nil res s + else if operation_is_redundant op nres then + match args with arg :: _ => Iop Omove (arg :: nil) res s | nil => instr end + else + instr + | Iload chunk addr args dst s => + let ndst := nreg (fst an!!pc) dst in + if is_dead ndst then + Inop s + else if is_int_zero ndst then + Iop (Ointconst Int.zero) nil dst s + else + instr + | Istore chunk addr args src s => + let p := aaddressing approx!!pc addr args in + if nmem_contains (snd an!!pc) p (size_chunk chunk) + then instr + else Inop s + | Ibuiltin (EF_memcpy sz al) (dst :: src :: nil) res s => + if nmem_contains (snd an!!pc) (aaddr approx!!pc dst) sz + then instr + else Inop s + | _ => + instr + end. + +Definition vanalyze := ValueAnalysis.analyze. + +Definition transf_function (rm: romem) (f: function) : res function := + let approx := vanalyze rm f in + match analyze approx f with + | Some an => + OK {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := PTree.map (transf_instr approx an) f.(fn_code); + fn_entrypoint := f.(fn_entrypoint) |} + | None => + Error (msg "Neededness analysis failed") + end. + + +Definition transf_fundef (rm: romem) (fd: fundef) : res fundef := + AST.transf_partial_fundef (transf_function rm) fd. + +Definition transf_program (p: program) : res program := + transform_partial_program (transf_fundef (romem_for_program p)) p. + |