diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-23 18:13:28 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-23 18:13:28 +0100 |
commit | a78fe0efa4b114d7c5ae11d0bed8cd17d55fd89c (patch) | |
tree | c8a59f14c27caf63241c507e7a7ff023c55c4c8a /riscV | |
parent | 3ce99d1f53b24704b45b6984d0fd0bc156016309 (diff) | |
parent | 91699fd379eb4087eb4088af77a5eb918552dc5e (diff) | |
download | compcert-kvx-a78fe0efa4b114d7c5ae11d0bed8cd17d55fd89c.tar.gz compcert-kvx-a78fe0efa4b114d7c5ae11d0bed8cd17d55fd89c.zip |
Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work
Diffstat (limited to 'riscV')
-rw-r--r-- | riscV/RTLpathSE_simplify.v | 19 |
1 files changed, 19 insertions, 0 deletions
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. + |