Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

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

Proofs finished for expansion

parent 9d0ae473
......@@ -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 ]
......
......@@ -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.
......@@ -823,22 +823,6 @@ Proof.
Global Opaque hslocal_set_sreg.
Local Hint Resolve hslocal_set_sreg_correct: wlp.
(* TODO gourdinl MOVE ELSEWHERE Branch expansion *)
(* TODO gourdinl NOT SURE IF THIS DEF IS NEEDED
* SHOULD WE TAKE THE PREV STATE INTO ACCOUNT HERE?
Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) : ?? list_hsval :=
if is_inv then
hlist_args prev*)
(*
Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : ?? (condition * list_hsval) :=
*)
(** ** Execution of one instruction *)
(* TODO gourdinl
......@@ -871,13 +855,13 @@ Lemma cbranch_expanse_correct hst c l:
(OK: hsok_local ge sp rs0 m0 hst),
seval_condition ge sp (fst r) (hsval_list_proj (snd r)) (si_smem st) rs0 m0 =
seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
Proof. Admitted. (*
Proof.
unfold cbranch_expanse.
destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify.
+ destruct p as [c' l']; simpl.
exploit target_cbranch_expanse_correct; eauto.
+ unfold seval_condition; erewrite H; eauto.
Qed.*)
destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify;
unfold seval_condition; erewrite <- H; eauto.
destruct p as [c' l']; simpl.
exploit target_cbranch_expanse_correct; eauto.
Qed.
Local Hint Resolve cbranch_expanse_correct: wlp.
Global Opaque cbranch_expanse.
......
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