From 2231fe82a807cebab5cae495ed08cda17810efdc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 11 Mar 2020 11:57:30 +0100
Subject: CSE3 ready to run?

---
 backend/CSE3.v | 71 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 69 insertions(+), 2 deletions(-)

(limited to 'backend/CSE3.v')

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 386591f1..d67a7a87 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -7,14 +7,81 @@ Axiom preanalysis : RTL.function -> analysis_hints.
 
 Definition run f := preanalysis f.
 
+Section REWRITE.
+  Context {ctx : eq_context}.
+
+Definition find_op_in_fmap fmap pc op args :=
+  match fmap with
+  | 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
+  | 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) :=
+  match rb with
+  | None => x
+  | 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_args fmap pc := List.map (subst_arg fmap pc).
+
 Definition transf_instr (fmap : option (PMap.t RB.t))
-           (pc: node) (instr: instruction) := instr.
+           (pc: node) (instr: instruction) :=
+  match instr with
+  | Iop op args dst s =>
+    let args' := subst_args fmap pc args in
+    match find_op_in_fmap fmap pc op args' with
+    | None => Iop op args' dst s
+    | Some src => Iop Omove (src::nil) dst s
+    end
+  | Iload trap chunk addr args dst s =>
+    let args' := subst_args fmap pc args in
+    match find_load_in_fmap fmap pc chunk addr args' with
+    | None => Iload trap chunk addr args' dst s
+    | Some src => Iop Omove (src::nil) dst s
+    end
+  | Istore chunk addr args src s =>
+    Istore chunk addr (subst_args fmap pc args) src s
+  | Icall sig ros args dst s =>
+    Icall sig ros (subst_args fmap pc args) dst s
+  | Itailcall sig ros args =>
+    Itailcall sig ros (subst_args fmap pc args)
+  | Icond cond args s1 s2 =>
+    Icond cond (subst_args fmap pc args) s1 s2
+  | Ijumptable arg tbl =>
+    Ijumptable (subst_arg fmap pc arg) tbl
+  | Ireturn (Some arg) =>
+    Ireturn (Some (subst_arg fmap pc arg))
+  | _ => instr
+  end.
+End REWRITE.
 
 Definition transf_function (f: function) : function :=
+  let ctx := context_from_hints (preanalysis f) in
+  let invariants := internal_analysis (ctx := ctx) f in
   {| fn_sig := f.(fn_sig);
      fn_params := f.(fn_params);
      fn_stacksize := f.(fn_stacksize);
-     fn_code := PTree.map (transf_instr (analysis (preanalysis f) f)) f.(fn_code);
+     fn_code := PTree.map (transf_instr (ctx := ctx) invariants) f.(fn_code);
      fn_entrypoint := f.(fn_entrypoint) |}.
 
 Definition transf_fundef (fd: fundef) : fundef :=
-- 
cgit