diff options
| -rw-r--r-- | backend/CSE3.v | 4 | ||||
| -rw-r--r-- | backend/CSE3analysis.v | 5 |
2 files changed, 5 insertions, 4 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index f4d75c51..386591f1 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -7,14 +7,14 @@ Axiom preanalysis : RTL.function -> analysis_hints. Definition run f := preanalysis f. -Definition transf_instr (fmap : analysis_hints) +Definition transf_instr (fmap : option (PMap.t RB.t)) (pc: node) (instr: instruction) := instr. Definition transf_function (f: function) : function := {| fn_sig := f.(fn_sig); fn_params := f.(fn_params); fn_stacksize := f.(fn_stacksize); - fn_code := PTree.map (transf_instr (preanalysis f)) f.(fn_code); + fn_code := PTree.map (transf_instr (analysis (preanalysis f) f)) 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 ded31270..140f2333 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -303,12 +303,13 @@ 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 (eqs : PTree.t equation) (hints : analysis_hints) := +Definition analysis (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 (hint_eq_catalog hints); + 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; |