diff options
| -rw-r--r-- | backend/RTLTunneling.v | 1 | ||||
| -rw-r--r-- | backend/RTLTunnelingproof.v | 5 | ||||
| -rw-r--r-- | tools/compiler_expand.ml | 3 |
3 files changed, 8 insertions, 1 deletions
diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v index e6901a9f..049160fd 100644 --- a/backend/RTLTunneling.v +++ b/backend/RTLTunneling.v @@ -25,6 +25,7 @@ Definition UF := PTree.t (node * Z). (* The oracle returns a map of "nop" node to their target with a distance (ie the number of the "nop" node on the path) to the target. *) Axiom branch_target: RTL.function -> UF. +Extract Constant branch_target => "RTLTunnelingaux.branch_target". (* TODO: add an extraction command to link branch_target with its implementation *) Local Open Scope error_monad_scope. diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 7f6696ad..14a2c037 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -149,6 +149,11 @@ Definition match_prog (p tp: program) := * `p` et `tp` sont les programmes donc on doit dire s'ils match *) + (**) Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. Section PRESERVATION. diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index ddb3c21a..265d0bcf 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -46,7 +46,8 @@ TOTAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Renumbering for PARTIAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "CSE3 for LICM"), "CSE3"; PARTIAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Redundancy elimination for LICM"), "Deadcode"; TOTAL, (Option "all_loads_nontrap"), Require, None, "Allnontrap"; -PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob" +PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob"; +PARTIAL, Always, Require, (Some "RTL Branch Tunneling"), "RTLTunneling" |];; let post_rtl_passes = |