From c6ebd73465ef895c6ea5e240f9c784463a6a0fe5 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 12 Mar 2020 16:46:06 +0100
Subject: removed second analysis phase

---
 backend/CSE3.v | 33 ++++++++++-----------------------
 1 file changed, 10 insertions(+), 23 deletions(-)

(limited to 'backend/CSE3.v')

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);
-- 
cgit