remove todos, clean

7 files changed, 69 insertions, 143 deletions

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: ";