From bf443e2f2bf38c30c9b68020c7c43cd7b3e10549 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 17 May 2021 23:19:16 +0200 Subject: preparing compiler passes and ml oracles --- driver/Compiler.vexpand | 8 ++------ scheduling/BTL.v | 8 ++++---- scheduling/BTLtoRTL.v | 4 +++- scheduling/BTLtoRTLaux.ml | 5 +++++ scheduling/RTLtoBTL.v | 4 +++- scheduling/RTLtoBTLaux.ml | 17 +++++++++++++++++ scheduling/RTLtoBTLproof.v | 11 +++++------ tools/compiler_expand.ml | 6 +++--- 8 files changed, 42 insertions(+), 21 deletions(-) create mode 100644 scheduling/BTLtoRTLaux.ml create mode 100644 scheduling/RTLtoBTLaux.ml diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index a751b232..40ea0d68 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -298,13 +298,9 @@ EXPAND_ASM_SEMANTICS eapply RTLgenproof.transf_program_correct; eassumption. EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. - eapply RTLpathLivegenproof.transf_program_correct; eassumption. - pose proof RTLpathLivegenproof.all_fundef_liveness_ok as X. - refine (modusponens _ _ (X _ _ _) _); eauto. intro. + eapply RTLtoBTLproof.transf_program_correct; eassumption. eapply compose_forward_simulations. - eapply RTLpathSchedulerproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply RTLpathproof.transf_program_correct; eassumption. + eapply BTLtoRTLproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 10a000a8..9fdf39be 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -463,8 +463,8 @@ Local Open Scope error_monad_scope. Definition verify_is_copy dupmap n n' := match dupmap!n with - | None => Error(msg "verify_is_copy None") - | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end + | None => Error(msg "BTL.verify_is_copy None") + | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "BTL.verify_is_copy invalid map") end end. Fixpoint verify_is_copy_list dupmap ln ln' := @@ -472,9 +472,9 @@ Fixpoint verify_is_copy_list dupmap ln ln' := | n::ln => match ln' with | n'::ln' => do _ <- verify_is_copy dupmap n n'; verify_is_copy_list dupmap ln ln' - | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end + | nil => Error (msg "BTL.verify_is_copy_list: ln' bigger than ln") end | nil => match ln' with - | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") + | n :: ln' => Error (msg "BTL.verify_is_copy_list: ln bigger than ln'") | nil => OK tt end end. diff --git a/scheduling/BTLtoRTL.v b/scheduling/BTLtoRTL.v index b64fd87a..82ad47b1 100644 --- a/scheduling/BTLtoRTL.v +++ b/scheduling/BTLtoRTL.v @@ -5,7 +5,9 @@ Require Import RTL Op Registers OptionMonad BTL. Require Import Errors Linking. (** External oracle *) -Parameter btl2rtl: function -> RTL.code * node * (PTree.t node). +Axiom btl2rtl: function -> RTL.code * node * (PTree.t node). + +Extract Constant btl2rtl => "BTLtoRTLaux.btl2rtl". Local Open Scope error_monad_scope. diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml new file mode 100644 index 00000000..3d8d44d0 --- /dev/null +++ b/scheduling/BTLtoRTLaux.ml @@ -0,0 +1,5 @@ +open Maps +open BinNums + +let btl2rtl f = + ((PTree.empty, Coq_xH), PTree.empty) diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v index e9319315..b3585157 100644 --- a/scheduling/RTLtoBTL.v +++ b/scheduling/RTLtoBTL.v @@ -5,7 +5,9 @@ Require Import RTL Op Registers OptionMonad BTL. Require Import Errors Linking. (** External oracle *) -Parameter rtl2btl: RTL.function -> BTL.code * node * (PTree.t node). +Axiom rtl2btl: RTL.function -> BTL.code * node * (PTree.t node). + +Extract Constant rtl2btl => "RTLtoBTLaux.rtl2btl". Local Open Scope error_monad_scope. diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml new file mode 100644 index 00000000..8ace6e2a --- /dev/null +++ b/scheduling/RTLtoBTLaux.ml @@ -0,0 +1,17 @@ +open RTLpathLivegenaux +open Maps +open RTL +open BinNums +open DebugPrint + +let rtl2btl (f: RTL.coq_function) = + let code = f.fn_code in + let entry = f.fn_entrypoint in + let join_points = get_join_points code entry in + Printf.eprintf "test"; + debug_flag := true; + debug "Join points: "; + print_true_nodes join_points; + debug "\n"; + debug_flag := false; + ((PTree.empty, Coq_xH), PTree.empty) diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 633e1b8e..5cebd33c 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -231,6 +231,7 @@ Proof. induction ib; simpl; auto; lia. Qed. +(* TODO gourdinl remove useless lemma? *) Lemma entry_isnt_goto dupmap f pc ib: match_iblock dupmap (RTL.fn_code f) true pc (entry ib) None -> is_goto (entry ib) = false. @@ -244,12 +245,10 @@ Lemma expand_entry_isnt_goto dupmap f pc ib: match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None -> is_goto (expand (entry ib) None) = false. Proof. - destruct (is_goto (expand (entry ib) None))eqn:EQG. - - destruct (expand (entry ib) None); - try destruct fi; try discriminate; trivial. - intros; inv H; inv H4. - - destruct (expand (entry ib) None); - try destruct fi; try discriminate; trivial. + destruct (is_goto (expand (entry ib) None))eqn:EQG; + destruct (expand (entry ib) None); + try destruct fi; try discriminate; trivial. + intros; inv H; inv H4. Qed. Lemma list_nth_z_rev_dupmap: diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index ddb3c21a..be3c6e19 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -51,9 +51,9 @@ PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob" let post_rtl_passes = [| - PARTIAL, Always, Require, (Some "RTLpath generation"), "RTLpathLivegen", Noprint; - PARTIAL, Always, Require, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint; - TOTAL, Always, Require, (Some "Projection to RTL"), "RTLpath", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1))); + PARTIAL, Always, Require, (Some "BTL generation"), "RTLtoBTL", Noprint; + (*PARTIAL, Always, Require, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint;*) + PARTIAL, Always, Require, (Some "Projection to RTL"), "BTLtoRTL", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1))); PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL 1"); PARTIAL, Always, Require, (Some "Branch tunneling"), "Tunneling", (Print "LTL 2"); PARTIAL, Always, Require, (Some "CFG linearization"), "Linearize", Noprint; -- cgit