diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-01 21:52:27 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-01 21:52:27 +0100 |
commit | dae202e121342b691585a78caaec8f4100c3123d (patch) | |
tree | 3b5e333a0e5fa81794cbd6c2254ae87fcfeafdcd /riscV | |
parent | 9d0ae4730abbad616991c5df5813bd1e8a981f5e (diff) | |
download | compcert-kvx-dae202e121342b691585a78caaec8f4100c3123d.tar.gz compcert-kvx-dae202e121342b691585a78caaec8f4100c3123d.zip |
Proofs finished for expansion
Diffstat (limited to 'riscV')
-rw-r--r-- | riscV/ExpansionOracle.ml | 2 | ||||
-rw-r--r-- | riscV/RTLpathSE_simplify.v | 79 |
2 files changed, 62 insertions, 19 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 39b8f367..41a2227b 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -327,7 +327,7 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = insn :: (if normal' then Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info) - else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO gourdinl Maybe incorrect *) + else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) :: k let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index f6d96d06..6a0297e9 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -1249,32 +1249,75 @@ Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall 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. + unfold target_cbranch_expanse, seval_condition; simpl. intros H (LREF & SREF & SREG & SMEM) ?. - destruct c; try congruence. - all: - repeat (destruct l; simpl in H; try congruence). - inv H; simpl. - try erewrite !fsi_sreg_get_correct; eauto. - - - simpl. - destruct c; inv H; simpl. + destruct c; try congruence; + repeat (destruct l; simpl in H; try congruence). + 1,2,5,6: + destruct c; inv H; simpl; try erewrite !fsi_sreg_get_correct; eauto; + try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence); try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); - try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence). - - try destruct (Int.eq n Int.zero) eqn: EQIMM; - try apply Int.same_if_eq in EQIMM; - all: try replace (Cle) with (swap_comparison Cge) by auto; try replace (Clt) with (swap_comparison Cgt) by auto; try rewrite Val.swap_cmp_bool; trivial; try rewrite Val.swap_cmpu_bool; trivial; try rewrite Val.swap_cmpl_bool; trivial; - try rewrite Val.swap_cmplu_bool; trivial.*) - all:admit. -Admitted. -(*Qed.*) + try rewrite Val.swap_cmplu_bool; trivial. + 1,2,3,4: + try destruct (Int.eq n Int.zero) eqn: EQIMM; + try apply Int.same_if_eq in EQIMM; + try destruct (Int64.eq n Int64.zero) eqn: EQIMM; + try apply Int64.same_if_eq in EQIMM; + destruct c; inv H; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); + unfold loadimm32, load_hilo32, Val.cmp, Val.cmpu, zero32; + unfold loadimm64, load_hilo64, Val.cmpl, Val.cmplu, zero64; + intros; try (specialize make_immed32_sound with (n); + destruct (make_immed32 n) eqn:EQMKI); intros; simpl; + intros; try (specialize make_immed64_sound with (n); + destruct (make_immed64 n) eqn:EQMKI); intros; simpl; + try rewrite EQLO; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; + try apply Int.same_if_eq in EQLO; simpl; trivial; + try apply Int64.same_if_eq in EQLO; simpl; trivial; + unfold may_undef_int, may_undef_luil; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; simpl; trivial; + try destruct v; try rewrite H; + try rewrite ltu_12_wordsize; try rewrite EQLO; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite Int64.add_commut, Int64.add_zero_l; + auto; simpl; + try rewrite H in EQIMM; + try rewrite EQLO in EQIMM; + try rewrite Int.add_commut, Int.add_zero_l in EQIMM; + try rewrite Int64.add_commut, Int64.add_zero_l in EQIMM; + try rewrite EQIMM; simpl; + try destruct (Archi.ptr64); trivial. + + 1,2,3,4: + destruct c; inv H; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); + unfold zero32, zero64, Val.cmpf, Val.cmpfs; + destruct v, v0; simpl; trivial; + try rewrite Float.cmp_ne_eq; + try rewrite Float32.cmp_ne_eq; + try rewrite <- Float.cmp_swap; simpl; + try rewrite <- Float32.cmp_swap; simpl; + try destruct (Float.cmp _ _); simpl; + try destruct (Float32.cmp _ _); simpl; + try rewrite Int.eq_true; simpl; + try rewrite Int.eq_false; try apply Int.one_not_zero; + simpl; trivial. +Qed. Global Opaque target_op_simplify. Global Opaque target_cbranch_expanse. |