From 056658bd2986d9e12ac07a54d25c08eb8a62ff60 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 28 Jul 2021 10:32:09 +0200 Subject: remove todos, clean --- scheduling/BTLScheduleraux.ml | 70 +++++++++++++---------------------------- scheduling/BTL_SEimpl.v | 20 +----------- scheduling/BTL_Scheduler.v | 46 +++++++++++++++++++++++++++ scheduling/BTL_Schedulerproof.v | 47 --------------------------- scheduling/PrintBTL.ml | 13 -------- scheduling/RTLpathSE_impl.v | 14 --------- scheduling/RTLtoBTLaux.ml | 2 -- 7 files changed, 69 insertions(+), 143 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml index 5ebc4144..c8c4e0d3 100644 --- a/scheduling/BTLScheduleraux.ml +++ b/scheduling/BTLScheduleraux.ml @@ -47,61 +47,45 @@ let find_array arr n = get_some @@ !index let count_cbs bseq olast indexes = - debug "count_cbs\n"; let current_cbs = ref SI.empty in let cbs_above = Hashtbl.create 100 in let update_cbs n ib = print_btl_inst stderr ib; - if is_a_cb ib then ( - debug "n is %d, add cb at: %d\n" n indexes.(n); - current_cbs := SI.add indexes.(n) !current_cbs) - else if is_a_load ib then ( - debug "n is %d, add load at: %d\n" n indexes.(n); - Hashtbl.add cbs_above indexes.(n) !current_cbs) + if is_a_cb ib then current_cbs := SI.add indexes.(n) !current_cbs + else if is_a_load ib then Hashtbl.add cbs_above indexes.(n) !current_cbs in Array.iteri (fun n ib -> update_cbs n ib) bseq; (match olast with - | Some last -> - debug "last\n"; - update_cbs (Array.length bseq) last + | Some last -> update_cbs (Array.length bseq) last | None -> ()); cbs_above let apply_schedule bseq olast positions = - let fmap n = find_array positions n in - let seq = (Array.init (Array.length positions) (fun i -> i)) in - let fseq = Array.map fmap seq in - (*debug_flag := true;*) - Array.iter (fun i -> debug "%d " i) positions; - debug "\n"; - Array.iter (fun i -> debug "%d " i) fseq; - debug "\n"; - Array.iter - (fun i -> debug "%d " i) - (Array.init (Array.length positions) (fun i -> i)); - debug "\n"; - let cbs_above_old = count_cbs bseq olast fseq in let bseq_new = Array.map (fun i -> bseq.(i)) positions in - let cbs_above_new = count_cbs bseq_new olast seq in - Array.iteri - (fun n ib -> - let n' = fseq.(n) in - match ib with - | Bload (t, a, b, c, d, e) -> - let set_old = Hashtbl.find cbs_above_old n' in - let set_new = Hashtbl.find cbs_above_new n' in - if SI.subset set_old set_new then - bseq_new.(n') <- Bload (AST.TRAP, a, b, c, d, e) - else (Printf.eprintf "\nTEST_GOURDINL_OK\n"; assert !config.has_non_trapping_loads) - | _ -> ()) - bseq; + (if !config.has_non_trapping_loads then + let fmap n = find_array positions n in + let seq = Array.init (Array.length positions) (fun i -> i) in + let fseq = Array.map fmap seq in + let cbs_above_old = count_cbs bseq olast fseq in + let cbs_above_new = count_cbs bseq_new olast seq in + Array.iteri + (fun n ib -> + let n' = fseq.(n) in + match ib with + | Bload (t, a, b, c, d, e) -> + let set_old = Hashtbl.find cbs_above_old n' in + let set_new = Hashtbl.find cbs_above_new n' in + if SI.subset set_old set_new then + bseq_new.(n') <- Bload (AST.TRAP, a, b, c, d, e) + else assert !config.has_non_trapping_loads + | _ -> ()) + bseq); let ibl = Array.to_list bseq_new in let rec build_iblock = function | [] -> failwith "build_iblock: empty list" | [ ib ] -> ( match olast with Some last -> Bseq (ib, last) | None -> ib) | ib1 :: ib2 :: k -> Bseq (ib1, build_iblock (ib2 :: k)) in - (*debug_flag := false;*) build_iblock ibl let schedule_blk n ibf btl = @@ -110,9 +94,6 @@ let schedule_blk n ibf btl = let bseq, olast = flatten_blk_basics ibf in match schedule_sequence bseq btl with | Some positions -> - debug "%d," (p2i n); - Array.iter (fun p -> debug "%d " p) positions; - debug "\n"; let new_ib = apply_schedule bseq olast positions in let new_ibf = { entry = new_ib; binfo = ibf.binfo; input_regs = ibf.input_regs } @@ -139,15 +120,8 @@ let rec do_schedule btl = function | [] -> btl | (n, ibf) :: blks -> let code_exp = expanse n ibf btl in - let code_nt = turn_all_loads_nontrap n ibf btl in + let code_nt = turn_all_loads_nontrap n ibf code_exp in let btl' = schedule_blk n ibf code_nt in - (*debug_flag := true;*) - if btl != code_exp then ( - debug "#######################################################\n"; - print_btl_code stderr btl; - debug "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n"; - print_btl_code stderr code_exp); - (*debug_flag := false;*) do_schedule btl' blks let btl_scheduler f = diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index aa27bd19..65d16d01 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -745,7 +745,6 @@ Proof. rewrite Heq; eauto. Qed. -(* TODO gourdinl move this in BTL_SEtheory? *) Lemma eval_list_sval_inj_not_none ctx st: forall l, (forall r, List.In r l -> eval_sval ctx (si_sreg st r) = None -> False) -> eval_list_sval ctx (list_sval_inj (map (si_sreg st) l)) = None -> False. @@ -853,23 +852,6 @@ Proof. split; destruct 1; econstructor; simpl in *; eauto. Qed. -(* TODO useless? -Lemma hrset_red_reg_correct ctx r rsv sv hrs sis: - ris_refines ctx hrs sis -> - (ris_ok ctx hrs -> eval_sval ctx rsv <> None) -> - (ris_ok ctx hrs -> eval_sval ctx rsv = eval_sval ctx sv) -> - ris_refines ctx (ris_sreg_set hrs (red_PTree_set r rsv hrs)) (set_sreg r sv sis). -Proof. - destruct 1; intros. - econstructor; eauto. - + rewrite ok_set_sreg, ok_hrset_red_sreg; intuition congruence. - + rewrite ok_hrset_red_sreg; intuition eauto. - + rewrite ok_hrset_red_sreg. intros; unfold set_sreg; simpl; - erewrite red_PTree_set_refines; eauto. - econstructor; eauto. -Qed. - *) - Fixpoint transfer_hrs (inputs: list reg) (hrs: ristate): ?? ristate := match inputs with | nil => RET {| ris_smem := hrs.(ris_smem); @@ -1474,7 +1456,7 @@ Definition simu_check_single (f1 f2: function) (ibf1 ibf2: iblock_info): ?? unit Lemma simu_check_single_correct (f1 f2: function) (ibf1 ibf2: iblock_info): WHEN simu_check_single f1 f2 ibf1 ibf2 ~> _ THEN symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). -Proof. (* TODO *) +Proof. unfold symbolic_simu; wlp_simplify. eapply rst_simu_correct; eauto. + intros; eapply hrexec_correct1; eauto; wlp_simplify. diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index 0662a357..78c597e0 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -46,6 +46,52 @@ Record match_function (f1 f2: BTL.function): Prop := { exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2); }. +Inductive match_fundef: fundef -> fundef -> Prop := + | match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f') + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + | match_stackframe_intro + res f sp pc rs rs' f' + (EQREGS: forall r, rs # r = rs' # r) + (TRANSF: match_function f f') + : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs'). + +Inductive match_states: state -> state -> Prop := + | match_states_intro + st f sp pc rs rs' m st' f' + (EQREGS: forall r, rs # r = rs' # r) + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function f f') + : match_states (State st f sp pc rs m) (State st' f' sp pc rs' m) + | match_states_call + st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f') + : match_states (Callstate st f args m) (Callstate st' f' args m) + | match_states_return + st st' v m + (STACKS: list_forall2 match_stackframes st st') + : match_states (Returnstate st v m) (Returnstate st' v m) + . + +Lemma match_stack_equiv stk1 stk2: + list_forall2 match_stackframes stk1 stk2 -> + forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> + list_forall2 match_stackframes stk1 stk3. +Proof. + induction 1; intros stk3 EQ; inv EQ; constructor; eauto. + inv H3; inv H; econstructor; eauto. + intros; rewrite <- EQUIV; auto. +Qed. + +Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3. +Proof. + Local Hint Resolve match_stack_equiv: core. + destruct 1; intros EQ; inv EQ; econstructor; eauto. + intros; rewrite <- EQUIV; auto. +Qed. + Local Open Scope error_monad_scope. Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res unit := diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index 40ad0d88..9a73d278 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -45,53 +45,6 @@ Proof. + eapply linkorder_refl. Qed. -(* TODO gourdinl move this to BTL_Scheduler.v? *) -Inductive match_fundef: fundef -> fundef -> Prop := - | match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f') - | match_External ef: match_fundef (External ef) (External ef). - -Inductive match_stackframes: stackframe -> stackframe -> Prop := - | match_stackframe_intro - res f sp pc rs rs' f' - (EQREGS: forall r, rs # r = rs' # r) - (TRANSF: match_function f f') - : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs'). - -Inductive match_states: state -> state -> Prop := - | match_states_intro - st f sp pc rs rs' m st' f' - (EQREGS: forall r, rs # r = rs' # r) - (STACKS: list_forall2 match_stackframes st st') - (TRANSF: match_function f f') - : match_states (State st f sp pc rs m) (State st' f' sp pc rs' m) - | match_states_call - st st' f f' args m - (STACKS: list_forall2 match_stackframes st st') - (TRANSF: match_fundef f f') - : match_states (Callstate st f args m) (Callstate st' f' args m) - | match_states_return - st st' v m - (STACKS: list_forall2 match_stackframes st st') - : match_states (Returnstate st v m) (Returnstate st' v m) - . - -Lemma match_stack_equiv stk1 stk2: - list_forall2 match_stackframes stk1 stk2 -> - forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> - list_forall2 match_stackframes stk1 stk3. -Proof. - induction 1; intros stk3 EQ; inv EQ; constructor; eauto. - inv H3; inv H; econstructor; eauto. - intros; rewrite <- EQUIV; auto. -Qed. - -Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3. -Proof. - Local Hint Resolve match_stack_equiv: core. - destruct 1; intros EQ; inv EQ; econstructor; eauto. - intros; rewrite <- EQUIV; auto. -Qed. - Lemma transf_function_correct f f': transf_function f = OK f' -> match_function f f'. Proof. diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml index 52178064..89254301 100644 --- a/scheduling/PrintBTL.ml +++ b/scheduling/PrintBTL.ml @@ -116,16 +116,3 @@ let print_btl_code pp btl = (PTree.elements btl); fprintf pp "\n") else () - -(* TODO gourdinl remove or adapt this? -let print_function pp id f = - fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; - let instrs = List.map (fun (n, i) -> i.entry) (PTree.elements f.fn_code) in - List.iter (print_iblock pp true "") instrs; - fprintf pp "}\n\n" - -let print_globdef pp (id, gd) = - match gd with Gfun (Internal f) -> print_function pp id f | _ -> () - -let print_program pp (prog : BTL.program) = - List.iter (print_globdef pp) prog.prog_defs*) diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index e21d7cd1..cda1c079 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -825,20 +825,6 @@ Local Hint Resolve hslocal_set_sreg_correct: wlp. (** ** Execution of one instruction *) -(* TODO gourdinl - * This is just useful for debugging fake values hashcode projection *) -Fixpoint check_no_uhid lhsv := - match lhsv with - | HSnil hc => - DO b <~ phys_eq hc unknown_hid;; - assert_b (negb b) "fail no uhid";; - RET tt - | HScons hsv lhsv' hc => - DO b <~ phys_eq hc unknown_hid;; - assert_b (negb b) "fail no uhid";; - check_no_uhid lhsv' - end. - Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) := match target_cbranch_expanse prev cond args with | Some (cond', vargs) => diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index 3de82d96..d544e87f 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -67,7 +67,6 @@ let translate_function code entry join_points liveness = | Some s -> ( match inst with | Icond (cond, lr, ifso, ifnot, info) -> - (* TODO gourdinl remove this *) assert (s = ifnot); next_nodes := !next_nodes @ non_predicted_successors inst psucc; iinfo.pcond <- info; @@ -100,7 +99,6 @@ let rtl2btl (f : RTL.coq_function) = let liveness = analyze f in let btl = translate_function code entry join_points liveness in let dm = PTree.map (fun n i -> n) btl in - (* TODO gourdinl move elsewhere *) (*debug_flag := true;*) debug "Entry %d\n" (p2i entry); debug "RTL Code: "; -- cgit