From f59c540aa7cf85c89ee0cb07c20374c8ad76a46c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 27 Oct 2020 15:21:11 +0100
Subject: new CSE3

---
 backend/CSE3analysisaux.ml | 57 +++++++++++++++++++++++++++++++++++++---------
 1 file changed, 46 insertions(+), 11 deletions(-)

(limited to 'backend/CSE3analysisaux.ml')

diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 3990b765..8c83dc2e 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -39,12 +39,12 @@ let print_reg channel i =
 let print_eq channel (lhs, sop, args) =
   match sop with
   | SOp op ->
-     Printf.printf "%a = %a\n" print_reg lhs (PrintOp.print_operation print_reg) (op, args)
+     Printf.printf "%a = %a" print_reg lhs (PrintOp.print_operation print_reg) (op, args)
   | SLoad(chunk, addr) ->
-     Printf.printf "%a = %s @ %a\n" print_reg lhs (string_of_chunk chunk)
+     Printf.printf "%a = %s @ %a" print_reg lhs (string_of_chunk chunk)
        (PrintOp.print_addressing print_reg) (addr, args);;
 
-let pp_set oc s =
+let pp_intset oc s =
   Printf.fprintf oc "{ ";
   List.iter (fun i -> Printf.fprintf oc "%d; " (P.to_int i)) (PSet.elements s);
   Printf.fprintf oc "}";;
@@ -70,6 +70,38 @@ let pp_option pp oc = function
 let is_trivial eq =
   (eq.eq_op = SOp Op.Omove) && (eq.eq_args = [eq.eq_lhs]);;
 
+let rec pp_list separator pp_item chan = function
+  | [] -> ()
+  | [h] -> pp_item chan h
+  | h::t ->
+     pp_item chan h;
+     output_string chan separator;
+     pp_list separator pp_item chan t;;
+
+let pp_set separator pp_item chan s =
+  pp_list separator pp_item chan (PSet.elements s);;
+
+let pp_equation hints chan x =
+  match PTree.get x hints.hint_eq_catalog with
+  | None -> output_string chan "???"
+  | Some eq ->
+     print_eq chan  (P.to_int eq.eq_lhs, eq.eq_op, List.map P.to_int eq.eq_args);;
+
+let pp_relation hints chan rel =
+  pp_set "; " (pp_equation hints) chan rel;;
+
+let pp_relation_b hints chan = function
+  | None -> output_string chan "bot"
+  | Some rel -> pp_relation hints chan rel;;
+
+let pp_results f (invariants : RB.t PMap.t) hints chan =
+  let max_pc = P.to_int (RTL.max_pc_function f) in
+  for pc=max_pc downto 1
+  do
+    Printf.fprintf chan "%d: %a\n" pc
+      (pp_relation_b hints) (PMap.get (P.of_int pc) invariants)
+  done
+
 let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   let cur_eq_id = ref 0
   and cur_catalog = ref PTree.empty
@@ -81,7 +113,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   let eq_find_oracle node eq =
     assert (not (is_trivial eq));
     let o = Hashtbl.find_opt eq_table (flatten_eq eq) in
-    (if !Clflags.option_debug_compcert > 1
+    (if !Clflags.option_debug_compcert > 5
      then Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node)
             pp_eq eq (pp_option pp_P) o);
     o
@@ -90,9 +122,9 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
       match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with
       | None -> PSet.empty
       | Some s -> s in
-    (if !Clflags.option_debug_compcert > 1
+    (if !Clflags.option_debug_compcert > 5
      then Printf.printf "@%d: rhs_find %a = %a\n"
-            (P.to_int node) pp_rhs (sop, args) pp_set o);
+            (P.to_int node) pp_rhs (sop, args) pp_intset o);
     o in
   let mutating_eq_find_oracle node eq : P.t option =
     let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in
@@ -124,7 +156,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
          Some coq_id
        end
     in
-    (if !Clflags.option_debug_compcert > 1
+    (if !Clflags.option_debug_compcert > 5
      then Printf.printf "@%d: mutating_eq_find %a -> %a\n" (P.to_int node)
       pp_eq eq (pp_option pp_P) o);    
     o
@@ -140,7 +172,10 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
       } tenv f
   with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3"
      | Some invariants ->
-        invariants,
-        { hint_eq_catalog    = !cur_catalog;
-          hint_eq_find_oracle= eq_find_oracle;
-          hint_eq_rhs_oracle = rhs_find_oracle };;
+        let hints = { hint_eq_catalog    = !cur_catalog;
+                      hint_eq_find_oracle= eq_find_oracle;
+                      hint_eq_rhs_oracle = rhs_find_oracle } in
+        (if !Clflags.option_debug_compcert > 1
+         then pp_results f invariants hints stdout);
+        invariants, hints
+;;
-- 
cgit