op simplify BTL intro

8 files changed, 56 insertions, 10 deletions

diff --git a/Makefile b/Makefile
index c4c45291..c9255fdb 100644
--- a/Makefile
+++ b/Makefile
@@ -152,7 +152,7 @@ BACKEND=\
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
   Asm.v Asmgen.v Asmgenproof.v Asmaux.v \
-	RTLpathSE_simplify.v \
+	RTLpathSE_simplify.v BTL_SEsimplify.v \
   $(BACKENDLIB)
 
 SCHEDULING= \
diff --git a/aarch64/BTL_SEsimplify.v b/aarch64/BTL_SEsimplify.v
new file mode 100644
index 00000000..34b41eee
--- /dev/null
+++ b/aarch64/BTL_SEsimplify.v
@@ -0,0 +1,43 @@
+Require Import Coqlib Floats Values Memory.
+Require Import Integers.
+Require Import Op Registers.
+Require Import BTL_SEtheory.
+Require Import BTL_SEsimuref.
+
+(** Target op simplifications using "fake" values *)
+
+Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval :=
+  None.
+
+Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) :=
+  None.
+
+(* Main proof of simplification *)
+
+(*
+Lemma target_op_simplify_correct ge sp ctx op lr hrs fsv st args m: forall
+   (H: target_op_simplify op lr hrs = Some fsv)
+   (REF: ris_refines ctx hrs st)
+   (OK0: ris_ok ctx hrs)
+   (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args)
+   (OK2: eval_smem ctx (si_smem st) = Some m),
+   eval_sval ctx fsv = eval_operation ge sp op args m.
+Proof.
+  unfold target_op_simplify; simpl.
+  intros H (LREF & SREF & SREG & SMEM) ? ? ?.
+  congruence.
+Qed.
+
+Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
+  (TARGET: target_cbranch_expanse hst c l = Some (c', l'))
+  (LREF : hsilocal_refines ge sp rs0 m0 hst st)
+  (OK: hsok_local ge sp rs0 m0 hst),
+  seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
+  seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
+Proof.
+  unfold target_cbranch_expanse, seval_condition; simpl.
+  intros H (LREF & SREF & SREG & SMEM) ?.
+  congruence.
+Qed.
+Global Opaque target_op_simplify.
+   Global Opaque target_cbranch_expanse.*)
diff --git a/arm/BTL_SEsimplify.v b/arm/BTL_SEsimplify.v
new file mode 120000
index 00000000..f190e6d5
--- /dev/null
+++ b/arm/BTL_SEsimplify.v
@@ -0,0 +1 @@
+../aarch64/BTL_SEsimplify.v
\ No newline at end of file
diff --git a/kvx/BTL_SEsimplify.v b/kvx/BTL_SEsimplify.v
new file mode 120000
index 00000000..f190e6d5
--- /dev/null
+++ b/kvx/BTL_SEsimplify.v
@@ -0,0 +1 @@
+../aarch64/BTL_SEsimplify.v
\ No newline at end of file
diff --git a/powerpc/BTL_SEsimplify.v b/powerpc/BTL_SEsimplify.v
new file mode 120000
index 00000000..f190e6d5
--- /dev/null
+++ b/powerpc/BTL_SEsimplify.v
@@ -0,0 +1 @@
+../aarch64/BTL_SEsimplify.v
\ No newline at end of file
diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v
new file mode 120000
index 00000000..f190e6d5
--- /dev/null
+++ b/riscV/BTL_SEsimplify.v
@@ -0,0 +1 @@
+../aarch64/BTL_SEsimplify.v
\ No newline at end of file
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index d6cdff59..3050f2e2 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -2,6 +2,7 @@ Require Import Coqlib AST Maps.
 Require Import Op Registers.
 Require Import RTL BTL Errors.
 Require Import BTL_SEsimuref BTL_SEtheory OptionMonad.
+Require Import BTL_SEsimplify.
 
 Require Import Impure.ImpHCons.
 Import Notations.
@@ -587,14 +588,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :=
      match is_move_operation op lr with
      | Some arg => hrs_sreg_get hrs arg (* optimization of Omove *)
      | None =>
-         DO lsv <~ hlist_args hrs lr;;
-         hSop op lsv
-        (* TODO gourdinl
        match target_op_simplify op lr hrs with
        | Some fsv => fsval_proj fsv
        | None =>
-         hSop op lhsv
-           end*)
+        DO lhsv <~ hlist_args hrs lr;;
+        hSop op lhsv
+        end
      end
   | Rload _ chunk addr => 
        DO lsv <~ hlist_args hrs lr;;
@@ -665,15 +664,14 @@ Proof.
 Qed.
 
 Definition cbranch_expanse (prev: ristate) (cond: condition) (args: list reg): ?? (condition * list_sval) :=
-  (* TODO gourdinl  
   match target_cbranch_expanse prev cond args with
     | Some (cond', vargs) => 
       DO vargs' <~ fsval_list_proj vargs;;
       RET (cond', vargs')
-     | None =>*)
+     | None =>
       DO vargs <~ hlist_args prev args ;;
-      RET (cond, vargs).
-    (*end.*)
+      RET (cond, vargs)
+  end.
 
 Lemma cbranch_expanse_correct hrs c l:
  WHEN cbranch_expanse hrs c l ~> r THEN forall ctx sis
diff --git a/x86/BTL_SEsimplify.v b/x86/BTL_SEsimplify.v
new file mode 120000
index 00000000..f190e6d5
--- /dev/null
+++ b/x86/BTL_SEsimplify.v
@@ -0,0 +1 @@
+../aarch64/BTL_SEsimplify.v
\ No newline at end of file