From 29e0c9b2c99a437fc9dfab66e1abdd546a5308d6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Jan 2014 15:59:11 +0000 Subject: Updated ARM backend wrt new static analyses and optimizations. NeedOp, Deadcode: must have distinct needs per argument of an operator. This change remains to be propagated to IA32 and PPC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Deadcode.v | 53 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 33 insertions(+), 20 deletions(-) (limited to 'backend/Deadcode.v') diff --git a/backend/Deadcode.v b/backend/Deadcode.v index 9efeca1a..98bc14a8 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -31,24 +31,34 @@ Require Import NeedOp. (** * Part 1: the static analysis *) +Definition add_need_all (r: reg) (ne: nenv) : nenv := + NE.set r All ne. + 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 := +Fixpoint add_needs_all (rl: list reg) (ne: nenv) : nenv := match rl with | nil => ne - | r1 :: rs => add_need r1 nv (add_needs rs nv ne) + | r1 :: rs => add_need_all r1 (add_needs_all rs ne) + end. + +Fixpoint add_needs (rl: list reg) (nvl: list nval) (ne: nenv) : nenv := + match rl, nvl with + | nil, _ => ne + | r1 :: rs, nil => add_needs_all rl ne + | r1 :: rs, nv1 :: nvs => add_need r1 nv1 (add_needs rs nvs ne) end. -Definition add_ros_need (ros: reg + ident) (ne: nenv) : nenv := +Definition add_ros_need_all (ros: reg + ident) (ne: nenv) : nenv := match ros with - | inl r => add_need r All ne + | inl r => add_need_all r ne | inr s => ne end. -Definition add_opt_need (or: option reg) (ne: nenv) : nenv := +Definition add_opt_need_all (or: option reg) (ne: nenv) : nenv := match or with - | Some r => add_need r All ne + | Some r => add_need_all r ne | None => ne end. @@ -64,26 +74,26 @@ Function transfer_builtin (app: VA.t) (ef: external_function) (args: list reg) ( (ne: NE.t) (nm: nmem) : NA.t := match ef, args with | EF_vload chunk, a1::nil => - (add_needs args All (kill res ne), + (add_needs_all args (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), + (add_needs_all args (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) + (add_need_all a1 (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), + (add_needs_all args (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) + (add_needs_all args (kill res ne), nm) | EF_annot_val txt targ, _ => - (add_needs args All (kill res ne), nm) + (add_needs_all args (kill res ne), nm) | _, _ => - (add_needs args All (kill res ne), nmem_all) + (add_needs_all args (kill res ne), nmem_all) end. Definition transfer (f: function) (approx: PMap.t VA.t) @@ -103,27 +113,27 @@ Definition transfer (f: function) (approx: PMap.t VA.t) 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), + else (add_needs_all args (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), + then (add_needs_all args (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) + (add_needs_all args (add_ros_need_all ros (kill res ne)), nmem_all) | Some(Itailcall sig ros args) => - (add_needs args All (add_ros_need ros NE.bot), + (add_needs_all args (add_ros_need_all 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) + (add_need_all arg ne, nm) | Some(Ireturn optarg) => - (add_opt_need optarg ne, nmem_dead_stack f.(fn_stacksize)) + (add_opt_need_all optarg ne, nmem_dead_stack f.(fn_stacksize)) end. Module DS := Backward_Dataflow_Solver(NA)(NodeSetBackward). @@ -144,7 +154,10 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t) 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 + match args with + | arg :: _ => Iop Omove (arg :: nil) res s + | nil => instr + end else instr | Iload chunk addr args dst s => -- cgit