Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work

4 files changed, 13 insertions, 92 deletions

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index 7dea752b..40db4e45 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -203,8 +203,7 @@ Fixpoint verify_mapping_mn_rec dupmap f f' lm :=
   match lm with
   | nil => OK tt
   | m :: lm => do u <- verify_mapping_mn dupmap f f' m;
-               do u2 <- verify_mapping_mn_rec dupmap f f' lm;
-               OK tt
+               verify_mapping_mn_rec dupmap f f' lm
   end.
 
 Definition verify_mapping_match_nodes dupmap (f f': function): res unit :=
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 861df3cd..b3635527 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -22,9 +22,8 @@
 open RTL
 open Maps
 open Camlcoq
+open DebugPrint
 
-let debug_flag = LICMaux.debug_flag
-let debug = LICMaux.debug
 let get_loop_headers = LICMaux.get_loop_headers
 let get_some = LICMaux.get_some
 let rtl_successors = LICMaux.rtl_successors
@@ -87,8 +86,6 @@ end
 
 module PSet = Set.Make(PInt)
 
-let print_intlist = LICMaux.print_intlist
-
 let print_intset s =
   let seq = PSet.to_seq s
   in begin
@@ -101,18 +98,6 @@ let print_intset s =
     end
   end
 
-let ptree_printbool pt =
-  let elements = PTree.elements pt
-  in begin
-    if !debug_flag then begin
-      Printf.printf "[";
-      List.iter (fun (n, b) ->
-        if b then Printf.printf "%d, " (P.to_int n) else ()
-      ) elements;
-      Printf.printf "]"
-    end
-  end
-
 (* Looks ahead (until a branch) to see if a node further down verifies
  * the given predicate *)
 let rec look_ahead_gen (successors: RTL.instruction -> P.t list) code node is_loop_header predicate =
@@ -215,16 +200,6 @@ type innerLoop = {
 
 let print_pset = LICMaux.pp_pset
 
-let print_ptree printer pt =
-  let elements = PTree.elements pt in
-  begin
-    debug "[\n";
-    List.iter (fun (n, elt) ->
-      debug "\t%d: %a\n" (P.to_int n) printer elt
-    ) elements;
-    debug "]\n"
-  end
-
 let rtl_successors_pref = function
 | Itailcall _ | Ireturn _ -> []
 | Icall(_,_,_,_,n) | Ibuiltin(_,_,_,n) | Inop n | Iop (_,_,_,n)
@@ -458,21 +433,21 @@ let update_direction direction = function
     | Some _ -> Icond (cond, lr, n, n', pred) )
 | i -> i
 
-let rec update_direction_rec directions = function
-| [] -> PTree.empty
-| m::lm -> let (n, i) = m
-    in let direction = get_some @@ PTree.get n directions
-    in PTree.set n (update_direction direction i) (update_direction_rec directions lm)
-
 (* Uses branch prediction to write prediction annotations in Icond *)
 let update_directions f code entrypoint = begin
   debug "Update_directions\n";
-  let directions = get_directions f code entrypoint
-  in begin
+  let directions = get_directions f code entrypoint in
+  let code' = ref code in
+  begin
+    debug "Get Directions done, now proceeding to update all direction information..\n";
     (* debug "Ifso directions: ";
     ptree_printbool directions;
     debug "\n"; *)
-    update_direction_rec directions (PTree.elements code)
+    List.iter (fun (n, i) ->
+      let direction = get_some @@ PTree.get n directions in
+      code' := PTree.set n (update_direction direction i) !code'
+    ) (PTree.elements code);
+    !code'
   end
 end
 
@@ -554,8 +529,6 @@ let print_traces oc traces =
       Printf.fprintf oc "Traces: {%a}\n" f traces
   end
 
-let print_code code = LICMaux.print_code code
-
 (* Dumb (but linear) trace selection *)
 let select_traces_linear code entrypoint =
   let is_visited = ref (PTree.map (fun n i -> false) code) in
@@ -770,14 +743,6 @@ let invert_iconds code =
  * cyclic dependencies between LICMaux and Duplicateaux
  *)
 
-
-
-let print_option_pint oc o =
-  if !debug_flag then
-    match o with
-    | None -> Printf.fprintf oc "None"
-    | Some n -> Printf.fprintf oc "Some %d" (P.to_int n)
-
 let print_inner_loop iloop =
   debug "{preds: %a, body: %a, head: %d, finals: %a, sb_final: %a}\n"
     print_intlist iloop.preds
@@ -794,8 +759,6 @@ let rec print_inner_loops = function
     print_inner_loops iloops
   end
 
-let print_pint oc i = if !debug_flag then Printf.fprintf oc "%d" (P.to_int i) else ()
-
 let cb_exit_node = function
   | Icond (_,_,n1,n2,p) -> begin match p with
       | Some true -> Some n2
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index 2480ccf0..cc24104f 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -111,7 +111,7 @@ Proof.
   - monadInv H0. inversion H.
   - inversion H.
     + subst. monadInv H0. destruct x. assumption.
-    + monadInv H0. destruct x0. eapply IHlb; assumption.
+    + monadInv H0. destruct x. eapply IHlb; assumption.
 Qed.
 
 Lemma verify_is_copy_correct:
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml
index df98077b..1f6b8817 100644
--- a/backend/LICMaux.ml
+++ b/backend/LICMaux.ml
@@ -16,16 +16,11 @@ open Maps;;
 open Kildall;;
 open HashedSet;;
 open Inject;;
+open DebugPrint;;
 
 type reg = P.t;;
 
 (** get_loop_headers moved from Duplicateaux.ml to LICMaux.ml to prevent cycle dependencies *)
-let debug_flag = ref false
-
-let debug fmt =
-  if !debug_flag then (flush stderr; Printf.eprintf fmt)
-  else Printf.ifprintf stderr fmt
-
 type vstate = Unvisited | Processed | Visited
 
 let get_some = function
@@ -39,42 +34,6 @@ let rtl_successors = function
 | Icond (_,_,n1,n2,_) -> [n1; n2]
 | Ijumptable (_,ln) -> ln
 
-let print_ptree_bool oc pt =
-  if !debug_flag then
-    let elements = PTree.elements pt in
-    begin
-      Printf.fprintf oc "[";
-      List.iter (fun (n, b) ->
-        if b then Printf.fprintf oc "%d, " (P.to_int n)
-      ) elements;
-      Printf.fprintf oc "]\n"
-    end
-  else ()
-
-let print_intlist oc l =
-  let rec f oc = function
-  | [] -> ()
-  | n::ln -> (Printf.fprintf oc "%d %a" (P.to_int n) f ln)
-  in begin
-    if !debug_flag then begin
-      Printf.fprintf oc "[%a]" f l
-    end
-  end
-
-(* Adapted from backend/PrintRTL.ml: print_function *)
-let print_code code = let open PrintRTL in let open Printf in
-  if (!debug_flag) then begin
-    fprintf stdout "{\n";
-    let instrs =
-      List.sort
-        (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
-        (List.rev_map
-          (fun (pc, i) -> (P.to_int pc, i))
-          (PTree.elements code)) in
-    List.iter (print_instruction stdout) instrs;
-    fprintf stdout "}"
-  end
-
 (** Getting loop branches with a DFS visit :
   * Each node is either Unvisited, Visited, or Processed
   * pre-order: node becomes Processed