From 4192b5f46ff5dbe7a6ccc0929e2d339aaa0e7b71 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 23 Feb 2021 18:10:29 +0100 Subject: Separate target_op_simplify for riscV --- Makefile | 1 + riscV/RTLpathSE_simplify.v | 19 +++++++++++++++++++ scheduling/RTLpathSE_impl.v | 21 ++------------------- 3 files changed, 22 insertions(+), 19 deletions(-) create mode 100644 riscV/RTLpathSE_simplify.v 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. -- cgit