blob: 1ee7dac5f2492d3a735fc72325d2ed9a92b6987f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
Require Import Coqlib Floats Values Memory.
Require Import Integers.
Require Import Op Registers.
Require Import RTLpathSE_theory.
Require Import RTLpathSE_simu_specs.
(** Target op simplifications using "fake" values *)
Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
None.
Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
None.
(* Main proof of simplification *)
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.
intros H (LREF & SREF & SREG & SMEM) ? ? ?.
congruence.
Qed.
Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
(TARGET: target_cbranch_expanse hst c l = Some (c', l'))
(LREF : hsilocal_refines ge sp rs0 m0 hst st)
(OK: hsok_local ge sp rs0 m0 hst),
seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
Proof.
unfold target_cbranch_expanse, seval_condition; simpl.
intros H (LREF & SREF & SREG & SMEM) ?.
congruence.
Qed.
Global Opaque target_op_simplify.
Global Opaque target_cbranch_expanse.
|