riscV/RTLpathSE_simplify.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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.