diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-11 11:57:30 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-11 11:57:30 +0100 |
commit | 2231fe82a807cebab5cae495ed08cda17810efdc (patch) | |
tree | 76e59dd1e069ffac31f5cf9736e71db34f760a20 /backend | |
parent | 4dc9118a4578be8b869a8dd8fa98c15a0b592419 (diff) | |
download | compcert-kvx-2231fe82a807cebab5cae495ed08cda17810efdc.tar.gz compcert-kvx-2231fe82a807cebab5cae495ed08cda17810efdc.zip |
CSE3 ready to run?
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CSE3.v | 71 | ||||
-rw-r--r-- | backend/CSE3analysis.v | 18 |
2 files changed, 78 insertions, 11 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index 386591f1..d67a7a87 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -7,14 +7,81 @@ Axiom preanalysis : RTL.function -> analysis_hints. Definition run f := preanalysis f. +Section REWRITE. + Context {ctx : eq_context}. + +Definition find_op_in_fmap fmap pc op args := + match fmap with + | None => None + | Some map => + match PMap.get pc map with + | Some rel => rhs_find (ctx:=ctx) pc (SOp op) args rel + | None => None + end + end. + +Definition find_load_in_fmap fmap pc chunk addr args := + match fmap with + | None => None + | Some map => + match PMap.get pc map with + | Some rel => rhs_find (ctx:=ctx) pc (SLoad chunk addr) args rel + | None => None + end + end. + +Definition forward_move_b (rb : RB.t) (x : reg) := + match rb with + | None => x + | Some rel => forward_move (ctx := ctx) rel x + end. + +Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg := + match fmap with + | None => x + | Some inv => forward_move_b (PMap.get pc inv) x + end. + +Definition subst_args fmap pc := List.map (subst_arg fmap pc). + Definition transf_instr (fmap : option (PMap.t RB.t)) - (pc: node) (instr: instruction) := instr. + (pc: node) (instr: instruction) := + match instr with + | Iop op args dst s => + let args' := subst_args fmap pc args in + match find_op_in_fmap fmap pc op args' with + | None => Iop op args' dst s + | Some src => Iop Omove (src::nil) dst s + end + | Iload trap chunk addr args dst s => + let args' := subst_args fmap pc args in + match find_load_in_fmap fmap pc chunk addr args' with + | None => Iload trap chunk addr args' dst s + | Some src => Iop Omove (src::nil) dst s + end + | Istore chunk addr args src s => + Istore chunk addr (subst_args fmap pc args) src s + | Icall sig ros args dst s => + Icall sig ros (subst_args fmap pc args) dst s + | Itailcall sig ros args => + Itailcall sig ros (subst_args fmap pc args) + | Icond cond args s1 s2 => + Icond cond (subst_args fmap pc args) s1 s2 + | Ijumptable arg tbl => + Ijumptable (subst_arg fmap pc arg) tbl + | Ireturn (Some arg) => + Ireturn (Some (subst_arg fmap pc arg)) + | _ => instr + end. +End REWRITE. Definition transf_function (f: function) : function := + let ctx := context_from_hints (preanalysis f) in + let invariants := internal_analysis (ctx := ctx) f in {| fn_sig := f.(fn_sig); fn_params := f.(fn_params); fn_stacksize := f.(fn_stacksize); - fn_code := PTree.map (transf_instr (analysis (preanalysis f) f)) f.(fn_code); + fn_code := PTree.map (transf_instr (ctx := ctx) invariants) f.(fn_code); fn_entrypoint := f.(fn_entrypoint) |}. Definition transf_fundef (fd: fundef) : fundef := diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 140f2333..18aa33b1 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -303,16 +303,16 @@ Record analysis_hints := hint_eq_find_oracle : node -> equation -> option eq_id; hint_eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t }. -Definition analysis (hints : analysis_hints) := +Definition context_from_hints (hints : analysis_hints) := let eqs := hint_eq_catalog hints in let reg_kills := get_reg_kills eqs in let mem_kills := get_mem_kills eqs in let moves := get_moves eqs in - internal_analysis (ctx := {| - eq_catalog := fun eq_id => PTree.get eq_id eqs; - eq_find_oracle := hint_eq_find_oracle hints ; - eq_rhs_oracle := hint_eq_rhs_oracle hints; - eq_kill_reg := fun reg => PMap.get reg reg_kills; - eq_kill_mem := fun _ => mem_kills; - eq_moves := fun reg => PMap.get reg moves - |}). + {| + eq_catalog := fun eq_id => PTree.get eq_id eqs; + eq_find_oracle := hint_eq_find_oracle hints ; + eq_rhs_oracle := hint_eq_rhs_oracle hints; + eq_kill_reg := fun reg => PMap.get reg reg_kills; + eq_kill_mem := fun _ => mem_kills; + eq_moves := fun reg => PMap.get reg moves + |}. |