Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1

7 files changed, 24 insertions, 31 deletions

diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v
index 0f303597..a4fce97e 100644
--- a/scheduling/RTLpath.v
+++ b/scheduling/RTLpath.v
@@ -28,8 +28,6 @@ Require Import Op Registers.
 Require Import RTL Linking.
 Require Import Lia.
 
-Declare Scope option_monad_scope.
-
 Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
          (at level 200, X ident, A at level 100, B at level 200)
          : option_monad_scope.
diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index 9b93bc32..2a20a15d 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -82,13 +82,15 @@ let get_path_map code entry join_points =
   let visited = ref (PTree.map (fun n i -> false) code) in
   let path_map = ref PTree.empty in
   let rec dig_path e =
-    let psize = ref (-1) in
-    let path_successors = ref [] in
-    let rec dig_path_rec n : (path_info * node list) option =
-      if not (get_some @@ PTree.get n !visited) then 
+    if (get_some @@ PTree.get e !visited) then
+      ()
+    else begin
+      visited := PTree.set e true !visited;
+      let psize = ref (-1) in
+      let path_successors = ref [] in
+      let rec dig_path_rec n : (path_info * node list) option =
         let inst = get_some @@ PTree.get n code in
         begin
-          visited := PTree.set n true !visited;
           psize := !psize + 1;
           let successor = match predicted_successor inst with
           | None -> None
@@ -102,15 +104,15 @@ let get_path_map code entry join_points =
                             input_regs = Regset.empty; pre_output_regs = Regset.empty; output_regs = Regset.empty },
                         !path_successors @ successors_inst inst)
         end
-      else None
-    in match dig_path_rec e with
-    | None -> ()
-    | Some ret ->
-        let (path_info, succs) = ret in
-        begin
-          path_map := PTree.set e path_info !path_map;
-          List.iter dig_path succs
-        end
+      in match dig_path_rec e with
+      | None -> ()
+      | Some ret ->
+          let (path_info, succs) = ret in
+          begin
+            path_map := PTree.set e path_info !path_map;
+            List.iter dig_path succs
+          end
+    end
   in begin
     dig_path entry;
     !path_map
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index 12aba56b..e21d7cd1 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -819,7 +819,7 @@ Proof.
     rewrite <- X, sok_local_set_sreg. intuition eauto.
     - destruct REF; intuition eauto.
     - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto.
-                    Qed.
+Qed.
 Global Opaque hslocal_set_sreg.
 Local Hint Resolve hslocal_set_sreg_correct: wlp.
 
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v
index 21f89f90..5051d805 100644
--- a/scheduling/RTLpathSE_simu_specs.v
+++ b/scheduling/RTLpathSE_simu_specs.v
@@ -106,13 +106,12 @@ with hsmem_proj hm :=
   | HSstore hm chk addr hl hv _ => Sstore (hsmem_proj hm) chk addr (hsval_list_proj hl) (hsval_proj hv)
   end.
 
-Declare Scope hse.
-Local Open Scope hse.
-
-
 (** We use a Notation instead a Definition, in order to get more automation "for free" *)
 Notation "'seval_hsval' ge sp hsv" := (seval_sval ge sp (hsval_proj hsv))
   (only parsing, at level 0, ge at next level, sp at next level, hsv at next level): hse.
+
+Local Open Scope hse.
+
 Notation "'seval_list_hsval' ge sp lhv" := (seval_list_sval ge sp (hsval_list_proj lhv))
   (only parsing, at level 0, ge at next level, sp at next level, lhv at next level): hse.
 Notation "'seval_hsmem' ge sp hsm" := (seval_smem ge sp (hsmem_proj hsm))
@@ -310,7 +309,6 @@ End HFINAL_REFINES.
 Section FAKE_HSVAL.
 (* BEGIN "fake" hsval without real hash-consing *)
 (* TODO: 
-  1) put these definitions elsewhere ? in RTLpathSE_simu_specs.v ? 
   2) reuse these definitions in hSinput, hSop, etc 
      in order to factorize proofs ?
 *)
diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v
index 1baf3fca..31680256 100644
--- a/scheduling/RTLpathScheduler.v
+++ b/scheduling/RTLpathScheduler.v
@@ -180,7 +180,7 @@ Proof.
     apply H in EQ2. rewrite EQ2. simpl.
   repeat (constructor; eauto).
   exploit function_equiv_checker_entrypoint. eapply EQ4. rewrite EQ2. intuition.
-Qed. 
+Qed.
 
 Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := {
   preserv_fnsig: fn_sig f1 = fn_sig f2;
diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml
index 378bf097..aeed39df 100644
--- a/scheduling/RTLpathScheduleraux.ml
+++ b/scheduling/RTLpathScheduleraux.ml
@@ -284,9 +284,7 @@ let rec do_schedule code pm = function
   | [] -> (code, pm)
   | sb :: lsb ->
       (*debug_flag := true;*)
-      let (code_exp, pm) =
-        if !Clflags.option_fexpanse_rtlcond then (expanse sb code pm)
-        else (code, pm) in
+      let (code_exp, pm) = expanse sb code pm in
       (*debug_flag := false;*)
       (* Trick: instead of turning loads into non trap as needed..
        * First, we turn them all into non-trap.
@@ -298,12 +296,12 @@ let rec do_schedule code pm = function
       let new_code = apply_schedule code' sb schedule in
       begin
         (*debug_flag := true;*)
+        if code != code_exp then (
         debug "Old Code: "; print_code code;
-        debug "Exp Code: "; print_code code_exp;
+        debug "Exp Code: "; print_code code_exp);
         debug "\nSchedule to apply: "; print_arrayp schedule;
         debug "\nNew Code: "; print_code new_code;
         debug "\n";
-        (*debug_flag := false; *)
         do_schedule new_code pm lsb
       end
 
@@ -321,7 +319,6 @@ let scheduler f =
     debug "Pathmap:\n"; debug "\n";
     print_path_map pm;
     debug "Superblocks:\n";
-    (*debug_flag := true; *)
     (*print_code code; flush stdout; flush stderr;*)
     (*debug_flag := false;*)
     (*print_superblocks lsb code; debug "\n";*)
diff --git a/scheduling/abstractbb/AbstractBasicBlocksDef.v b/scheduling/abstractbb/AbstractBasicBlocksDef.v
index 34d72de1..fec716c4 100644
--- a/scheduling/abstractbb/AbstractBasicBlocksDef.v
+++ b/scheduling/abstractbb/AbstractBasicBlocksDef.v
@@ -273,8 +273,6 @@ with list_term :=
 Scheme term_mut := Induction for term Sort Prop
 with list_term_mut := Induction for list_term Sort Prop.
 
-Declare Scope pattern_scope.
-Declare Scope term_scope.
 Bind Scope pattern_scope with term.
 Delimit Scope term_scope with term.
 Delimit Scope pattern_scope with pattern.