From cf8ff0b0407cd0b4981f363418fde7f96e95d6a5 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 9 Dec 2020 08:46:25 +0100
Subject: CSE3 compiles again, but some admitted lemmas

---
 backend/CSE3analysisaux.ml | 18 ++++++++----------
 driver/Clflags.ml          |  2 +-
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index b8f98b0d..efe6b600 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -137,8 +137,7 @@ let rb_glb (x : RB.t) (y : RB.t) : RB.t =
 let compute_invariants
       (nodes : RTL.node list)
       (entrypoint : RTL.node)
-      (successors : RTL.node -> RTL.node list)
-      (tfr : RTL.node -> RB.t -> RB.t) =
+      (tfr : RTL.node -> RB.t -> (RTL.node * RB.t) list) =
   let todo = ref IntSet.empty
   and invariants = ref (PMap.set entrypoint (Some RELATION.top) (PMap.init RB.bot)) in  
   let add_todo (pc : RTL.node) =
@@ -147,13 +146,13 @@ let compute_invariants
     (if !Clflags.option_debug_compcert > 9
      then Printf.printf "UP updating node %d\n" (P.to_int pc));
     let cur = PMap.get pc !invariants in
-    List.iter (fun next_pc ->
+    List.iter (fun (next_pc, next_contrib) ->
         let previous = PMap.get next_pc !invariants in
-        let next = RB.lub previous (tfr pc cur) in
+        let next = RB.lub previous next_contrib in
         if not (RB.beq previous next)
         then (
           invariants := PMap.set next_pc next !invariants;
-          add_todo next_pc)) (successors pc) in
+          add_todo next_pc)) (tfr pc cur) in
   add_todo entrypoint;
   while not (IntSet.is_empty !todo) do
     let nxt = IntSet.max_elt !todo in
@@ -167,7 +166,8 @@ let refine_invariants
       (entrypoint : RTL.node)
       (successors : RTL.node -> RTL.node list)
       (predecessors : RTL.node -> RTL.node list)
-      (tfr : RTL.node -> RB.t -> RB.t) (invariants0 : RB.t PMap.t) =
+      (tfr : RTL.node -> RB.t -> (RTL.node * RB.t) list)
+      (invariants0 : RB.t PMap.t) =
   let todo = ref IntSet.empty
   and invariants = ref invariants0 in  
   let add_todo (pc : RTL.node) =
@@ -182,7 +182,7 @@ let refine_invariants
                   (List.map
                      (fun pred_pc->
                        rb_glb cur
-                         (tfr pred_pc (PMap.get pred_pc !invariants)))
+                         (List.assoc pc (tfr pred_pc (PMap.get pred_pc !invariants))))
                      (predecessors pc)) in
       if not (RB.beq cur nxt)
       then
@@ -205,12 +205,10 @@ let get_default default x ptree =
   | Some y -> y;;
 
 let initial_analysis ctx tenv (f : RTL.coq_function) =
-  let succ_map = RTL.successors_map f in
-  let succ_f x = get_default [] x succ_map in
   let tfr = apply_instr' ctx tenv f.RTL.fn_code in
   compute_invariants
     (List.map fst (PTree.elements f.RTL.fn_code))
-    f.RTL.fn_entrypoint succ_f tfr;;
+    f.RTL.fn_entrypoint tfr;;
 
 let refine_analysis ctx tenv
       (f : RTL.coq_function) (invariants0 : RB.t PMap.t) =
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index eebc170a..991720bf 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -34,7 +34,7 @@ let option_fcse3_across_calls = ref false
 let option_fcse3_across_merges = ref true
 let option_fcse3_glb = ref true
 let option_fcse3_trivial_ops = ref false
-let option_fcse3_refine = ref false (* DM *)
+let option_fcse3_refine = ref true
 let option_fredundancy = ref true
 
 (** Options relative to superblock scheduling *)
-- 
cgit