diff options
Diffstat (limited to 'backend/CSE3.v')
-rw-r--r-- | backend/CSE3.v | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index d67a7a87..2ef16376 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -2,8 +2,11 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps CSE2deps. Require Import CSE3analysis HashedSet. +Require Import RTLtyping. -Axiom preanalysis : RTL.function -> analysis_hints. +Local Open Scope error_monad_scope. + +Axiom preanalysis : typing_env -> RTL.function -> analysis_hints. Definition run f := preanalysis f. @@ -75,20 +78,19 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) 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 (ctx := ctx) invariants) f.(fn_code); - fn_entrypoint := f.(fn_entrypoint) |}. - -Definition transf_fundef (fd: fundef) : fundef := - AST.transf_fundef transf_function fd. +Definition transf_function (f: function) : res function := + do tenv <- type_function f; + let ctx := context_from_hints (preanalysis tenv f) in + let invariants := internal_analysis (ctx := ctx) tenv f in + 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) + f.(fn_code); + fn_entrypoint := f.(fn_entrypoint) |}. -Definition transf_program (p: program) : program := - transform_program transf_fundef p. +Definition transf_fundef (fd: fundef) : res fundef := + AST.transf_partial_fundef transf_function fd. -Definition match_prog (p tp: RTL.program) := - match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. |