Commit 4192b5f4 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Separate target_op_simplify for riscV

parent 9cddf911
......@@ -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= \
......
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.
......@@ -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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment