diff options
Diffstat (limited to 'backend/CSE3.v')
| -rw-r--r-- | backend/CSE3.v | 38 |
1 files changed, 29 insertions, 9 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index 746ba399..2f73a1a7 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -15,11 +15,22 @@ Require Import AST Linking. Require Import Memory Registers Op RTL Maps CSE2deps. Require Import CSE3analysis HashedSet. Require Import RTLtyping. +Require Compopts. Local Open Scope error_monad_scope. Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints. +Record cse3params : Type := + mkcse3params + { cse3_conditions : bool; + cse3_operations : bool; + cse3_trivial_ops: bool; + }. + +Section PARAMS. + Variable params : cse3params. + Section REWRITE. Context {ctx : eq_context}. @@ -54,7 +65,7 @@ Definition subst_args fmap pc xl := forward_move_l_b (PMap.get pc fmap) xl. Definition find_cond_in_fmap fmap pc cond args := - if Compopts.optim_CSE3_conditions tt + if params.(cse3_conditions) then match PMap.get pc fmap with | Some rel => @@ -74,12 +85,12 @@ Definition find_cond_in_fmap fmap pc cond args := end else None. -Definition transf_instr (fmap : PMap.t RB.t) +Definition param_transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) := match instr with | Iop op args dst s => let args' := subst_args fmap pc args in - match (if (negb (Compopts.optim_CSE3_trivial_ops tt)) && (is_trivial_op op) + match (if (negb params.(cse3_operations) || ((negb params.(cse3_trivial_ops)) && (is_trivial_op op))) then None else find_op_in_fmap fmap pc op args') with | None => Iop op args' dst s | Some src => Iop Omove (src::nil) dst s @@ -110,7 +121,7 @@ Definition transf_instr (fmap : PMap.t RB.t) end. End REWRITE. -Definition transf_function (f: function) : res function := +Definition param_transf_function (f: function) : res function := do tenv <- type_function f; let (invariants, hints) := preanalysis tenv f in let ctx := context_from_hints hints in @@ -119,13 +130,22 @@ Definition transf_function (f: function) : res function := OK {| fn_sig := f.(fn_sig); fn_params := f.(fn_params); fn_stacksize := f.(fn_stacksize); - fn_code := PTree.map (transf_instr (ctx := ctx) invariants) + fn_code := PTree.map (param_transf_instr (ctx := ctx) invariants) f.(fn_code); fn_entrypoint := f.(fn_entrypoint) |} else Error (msg "cse3: not inductive"). -Definition transf_fundef (fd: fundef) : res fundef := - AST.transf_partial_fundef transf_function fd. +Definition param_transf_fundef (fd: fundef) : res fundef := + AST.transf_partial_fundef param_transf_function fd. + +Definition param_transf_program (p: program) : res program := + transform_partial_program param_transf_fundef p. + +End PARAMS. + +Definition cmdline_params (_ : unit) := + {| cse3_conditions := Compopts.optim_CSE3_conditions tt; + cse3_operations := true; + cse3_trivial_ops:= Compopts.optim_CSE3_trivial_ops tt |}. -Definition transf_program (p: program) : res program := - transform_partial_program transf_fundef p. +Definition transf_program p := param_transf_program (cmdline_params tt) p. |