Separate target_op_simplify for riscV

3 files changed, 22 insertions, 19 deletions

diff --git a/Makefile b/Makefile
index 9adeb6db..fd0595d4 100644
--- a/Makefile
+++ b/Makefile
@@ -133,6 +133,7 @@ BACKEND=\
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
   Asm.v Asmgen.v Asmgenproof.v Asmaux.v \
+	RTLpathSE_simplify.v \
   $(BACKENDLIB)
 
 SCHEDULING= \
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
new file mode 100644
index 00000000..4fadcfdc
--- /dev/null
+++ b/riscV/RTLpathSE_simplify.v
@@ -0,0 +1,19 @@
+Require Import Op Registers.
+Require Import RTLpathSE_theory.
+Require Import RTLpathSE_simu_specs.
+
+Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
+  None.  (* default implementation *)
+
+Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
+   (H: target_op_simplify op lr hst = Some fsv)
+   (REF: hsilocal_refines ge sp rs0 m0 hst st)
+   (OK0: hsok_local ge sp rs0 m0 hst)
+   (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args)
+   (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m),
+   seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m.
+Proof.
+  unfold target_op_simplify; simpl. congruence.
+Qed.
+Global Opaque target_op_simplify.
+
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index bd7ae2ad..a7f1323d 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -6,7 +6,7 @@ Require Import Op Registers.
 Require Import RTL RTLpath.
 Require Import Errors.
 Require Import RTLpathSE_theory RTLpathLivegenproof.
-Require Import Axioms RTLpathSE_simu_specs.
+Require Import Axioms RTLpathSE_simu_specs RTLpathSE_simplify.
 
 Local Open Scope error_monad_scope.
 Local Open Scope option_monad_scope.
@@ -695,23 +695,6 @@ Proof.
     explore; try congruence.
 Qed.
 
-
-(* TODO: This function could be defined in a specific file for each target *)
-Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
-  None.  (* default implementation *)
-
-Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
-   (H: target_op_simplify op lr hst = Some fsv)
-   (REF: hsilocal_refines ge sp rs0 m0 hst st)
-   (OK0: hsok_local ge sp rs0 m0 hst)
-   (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args)
-   (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m),
-   seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m.
-Proof.
-  unfold target_op_simplify; simpl. congruence.
-Qed.
-Global Opaque target_op_simplify.
-
 (** simplify a symbolic value before assignment to a register *)
 Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
   match rsv with
@@ -1616,4 +1599,4 @@ Proof.
   destruct (unsafe_coerce (aux_simu_check dm f tf)) as [[|]|] eqn:Hres; simpl; try discriminate.
   intros; eapply aux_simu_check_correct; eauto.
   eapply unsafe_coerce_not_really_correct; eauto.
-Qed.
\ No newline at end of file
+Qed.