removed second analysis phase

5 files changed, 25 insertions, 31 deletions

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 2ef16376..e82b7cdb 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -6,31 +6,21 @@ Require Import RTLtyping.
 
 Local Open Scope error_monad_scope.
 
-Axiom preanalysis : typing_env -> RTL.function -> analysis_hints.
-
-Definition run f := preanalysis f.
+Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints.
 
 Section REWRITE.
   Context {ctx : eq_context}.
 
 Definition find_op_in_fmap fmap pc op args :=
-  match fmap with
+  match PMap.get pc fmap with
+  | Some rel => rhs_find (ctx:=ctx) pc (SOp op) args rel
   | None => None
-  | Some map =>
-    match PMap.get pc map with
-    | Some rel => rhs_find (ctx:=ctx) pc (SOp op) args rel
-    | None => None
-    end
   end.
 
 Definition find_load_in_fmap fmap pc chunk addr args :=
-  match fmap with
+  match PMap.get pc fmap with
+  | Some rel => rhs_find (ctx:=ctx) pc (SLoad chunk addr) args rel
   | None => None
-  | Some map =>
-    match PMap.get pc map with
-    | Some rel => rhs_find (ctx:=ctx) pc (SLoad chunk addr) args rel
-    | None => None
-    end
   end.
 
 Definition forward_move_b (rb : RB.t) (x : reg) :=
@@ -39,15 +29,12 @@ Definition forward_move_b (rb : RB.t) (x : reg) :=
   | Some rel => forward_move (ctx := ctx) rel x
   end.
 
-Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg :=
-  match fmap with
-  | None => x
-  | Some inv => forward_move_b (PMap.get pc inv) x
-  end.
+Definition subst_arg (fmap : PMap.t RB.t) (pc : node) (x : reg) : reg :=
+  forward_move_b (PMap.get pc fmap) x.
 
 Definition subst_args fmap pc := List.map (subst_arg fmap pc).
 
-Definition transf_instr (fmap : option (PMap.t RB.t))
+Definition transf_instr (fmap : PMap.t RB.t)
            (pc: node) (instr: instruction) :=
   match instr with
   | Iop op args dst s =>
@@ -80,8 +67,8 @@ End REWRITE.
 
 Definition transf_function (f: function) : res function :=
   do tenv <- type_function f;
-    let ctx := context_from_hints (preanalysis tenv f) in
-    let invariants := internal_analysis (ctx := ctx) tenv f in
+  let (invariants, hints) := preanalysis tenv f in 
+  let ctx := context_from_hints hints in
     OK {| fn_sig := f.(fn_sig);
           fn_params := f.(fn_params);
           fn_stacksize := f.(fn_stacksize);
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 643b752a..69c21113 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -329,9 +329,11 @@ Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t
     end
   end.
 
+Definition invariants := PMap.t RB.t.
+
 Definition internal_analysis
   (tenv : typing_env)
-  (f : RTL.function) := DS.fixpoint
+  (f : RTL.function) : option invariants := DS.fixpoint
   (RTL.fn_code f) RTL.successors_instr
   (apply_instr' tenv (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
 
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 392fd13f..23e20ea8 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -80,15 +80,18 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
          Some coq_id
        end
   in
-  ignore 
-    (internal_analysis
+  match
+    internal_analysis
       { eq_catalog     = (fun eq_id -> PTree.get eq_id !cur_catalog);
         eq_find_oracle = mutating_eq_find_oracle;
         eq_rhs_oracle  = rhs_find_oracle ;
         eq_kill_reg    = (fun reg -> PMap.get reg !cur_kill_reg);
         eq_kill_mem    = (fun () -> !cur_kill_mem);
         eq_moves       = (fun reg -> PMap.get reg !cur_moves)
-      } tenv f);
-  { hint_eq_catalog    = !cur_catalog;
-    hint_eq_find_oracle= eq_find_oracle;
-    hint_eq_rhs_oracle = rhs_find_oracle };;
+      } 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 };;
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index c7a882b6..72b3e7e1 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -76,6 +76,8 @@ Proof.
   destruct f; simpl; intros.
   - monadInv H.
     monadInv EQ.
+    destruct preanalysis.
+    inv EQ1.
     reflexivity.
   - monadInv H.
     reflexivity.
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 79393cf8..9b47b203 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -191,7 +191,7 @@ Set Extraction AccessOpaque.
 Cd "extraction".
 
 Separate Extraction
-   CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem CSE3.run
+   CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
    Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env