1 files changed, 151 insertions, 0 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v
new file mode 100644
index 00000000..2f73a1a7
--- /dev/null
+++ b/backend/CSE3.v
@@ -0,0 +1,151 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*                                                             *)
+(*  Copyright VERIMAG. All rights reserved.                    *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps CSE2deps.
+Require Import CSE3analysis HashedSet.
+Require Import RTLtyping.
+Require Compopts.
+
+Local Open Scope error_monad_scope.
+
+Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints.
+
+Record cse3params : Type :=
+  mkcse3params
+    { cse3_conditions : bool;
+      cse3_operations : bool;
+      cse3_trivial_ops: bool;
+    }.
+
+Section PARAMS.
+  Variable params : cse3params.
+
+Section REWRITE.
+  Context {ctx : eq_context}.
+
+Definition find_op_in_fmap fmap pc op args :=
+  match PMap.get pc fmap with
+  | Some rel => rhs_find (ctx:=ctx) pc (SOp op) args rel
+  | None => None
+  end.
+
+Definition find_load_in_fmap fmap pc chunk addr args :=
+  match PMap.get pc fmap with
+  | Some rel => rhs_find (ctx:=ctx) pc (SLoad chunk addr) args rel
+  | None => None
+  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 : PMap.t RB.t) (pc : node) (x : reg) : reg :=
+  forward_move_b (PMap.get pc fmap) x.
+
+Definition forward_move_l_b (rb : RB.t) (xl : list reg) :=
+  match rb with
+  | None => xl
+  | Some rel => forward_move_l (ctx := ctx) rel xl
+  end.
+
+Definition subst_args fmap pc xl :=
+  forward_move_l_b (PMap.get pc fmap) xl.
+
+Definition find_cond_in_fmap fmap pc cond args :=
+  if params.(cse3_conditions)
+  then
+    match PMap.get pc fmap with
+    | Some rel =>
+      if is_condition_present (ctx:=ctx) pc rel cond args
+      then Some true
+      else
+        let ncond := negate_condition cond in
+        if is_condition_present (ctx:=ctx) pc rel ncond args
+        then Some false
+        else let args' := subst_args fmap pc args in
+             if is_condition_present (ctx:=ctx) pc rel cond args'
+             then Some true
+             else if is_condition_present (ctx:=ctx) pc rel ncond args'
+                  then Some false
+                  else None
+    | None => None
+    end
+  else None.
+
+Definition param_transf_instr (fmap : PMap.t RB.t)
+           (pc: node) (instr: instruction) :=
+  match instr with
+  | Iop op args dst s =>
+    let args' := subst_args fmap pc args in
+    match (if (negb params.(cse3_operations) || ((negb params.(cse3_trivial_ops)) && (is_trivial_op op)))
+           then None else 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) (subst_arg fmap pc 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 expected =>
+    let args' := subst_args fmap pc args in
+    match find_cond_in_fmap fmap pc cond args with
+    | None => Icond cond args' s1 s2 expected
+    | Some b => Inop (if b then s1 else s2)
+    end
+  | 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 param_transf_function (f: function) : res function :=
+  do tenv <- type_function f;
+  let (invariants, hints) := preanalysis tenv f in
+  let ctx := context_from_hints hints in
+  if check_inductiveness (ctx:=ctx) f tenv invariants
+  then
+    OK {| fn_sig := f.(fn_sig);
+          fn_params := f.(fn_params);
+          fn_stacksize := f.(fn_stacksize);
+          fn_code := PTree.map (param_transf_instr (ctx := ctx) invariants)
+                               f.(fn_code);
+          fn_entrypoint := f.(fn_entrypoint) |}
+  else Error (msg "cse3: not inductive").
+
+Definition param_transf_fundef (fd: fundef) : res fundef :=
+  AST.transf_partial_fundef param_transf_function fd.
+
+Definition param_transf_program (p: program) : res program :=
+  transform_partial_program param_transf_fundef p.
+
+End PARAMS.
+
+Definition cmdline_params (_ : unit) :=
+  {| cse3_conditions := Compopts.optim_CSE3_conditions tt;
+     cse3_operations := true;
+     cse3_trivial_ops:= Compopts.optim_CSE3_trivial_ops tt |}.
+
+Definition transf_program p := param_transf_program (cmdline_params tt) p.