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 e8322076 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Some more proofs on branch expansion, using make_immed32_sound

parent fb6325b4
......@@ -7,7 +7,7 @@ Require Import RTL RTLpath.
Require Import Errors.
Require Import RTLpathSE_theory RTLpathLivegenproof.
Require Import Axioms RTLpathSE_simu_specs.
Require Import Asmgen.
Require Import Asmgen Asmgenproof1.
Local Open Scope error_monad_scope.
Local Open Scope option_monad_scope.
......@@ -936,20 +936,20 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
end.
Lemma simplify_nothing lr (hst: hsistate_local) op:
WHEN DO lhsv <~ hlist_args hst lr;; hSop op lhsv ~> hv
THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset)
(m0 : mem) (st : sistate_local),
hsilocal_refines ge sp rs0 m0 hst st ->
hsok_local ge sp rs0 m0 hst ->
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp op args m) <> None ->
seval_sval ge sp (hsval_proj hv) rs0 m0 =
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp op args m)).
WHEN DO lhsv <~ hlist_args hst lr;; hSop op lhsv ~> hv
THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset)
(m0 : mem) (st : sistate_local),
hsilocal_refines ge sp rs0 m0 hst st ->
hsok_local ge sp rs0 m0 hst ->
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp op args m) <> None ->
seval_sval ge sp (hsval_proj hv) rs0 m0 =
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp op args m)).
Proof.
wlp_simplify.
generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0.
......@@ -979,6 +979,18 @@ Proof.
destruct b; simpl; auto.
Qed.
Lemma xor_ceq_zero: forall v n cmp,
cmp = Ceq \/ cmp = Cne ->
Some
(Val.of_optbool (Val.cmp_bool cmp (Val.xor v (Vint n)) (Vint Int.zero))) =
Some (Val.of_optbool (Val.cmp_bool cmp v (Vint n))).
Proof.
intros; destruct v; unfold Val.xor; simpl; auto.
destruct cmp, H; try discriminate; simpl;
destruct (Int.eq (Int.xor i n) Int.zero) eqn:EQ;
rewrite Int.xor_is_zero in EQ; rewrite EQ; trivial.
Qed.
(* TODO gourdinl Lemma xor_neg_ltge_cmp: forall v1 v2,
Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
Some (Val.of_optbool (Val.cmp_bool Cge v1 v2)).
......@@ -1221,6 +1233,31 @@ Proof.
destruct (Float.cmp _ _ _); simpl; auto.
Qed.
Lemma cmp_ltle_add_one: forall v n,
Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) =
Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))).
Proof.
intros. unfold Val.cmp_bool; destruct 6; simpl; auto.
unfold Int.lt. replace (Int.signed (Int.add imm Int.one)) with (Int.signed imm + 1).
destruct (zlt (Int.signed imm) (Int.signed i)).
rewrite zlt_false by omega. auto.
rewrite zlt_true by omega. auto.
rewrite Int.add_signed. symmetry; apply Int.signed_repr.
specialize (Int.eq_spec imm (Int.repr Int.max_signed)).
rewrite EQMAX; simpl; intros.
assert (Int.signed imm <> Int.max_signed).
{ red; intros E. elim H2. rewrite <- (Int.repr_signed imm). rewrite E. auto. }
generalize (Int.signed_range imm); omega.
(*Lemma cmp_le_max: forall v*)
(*(CONTRA: Some*)
(*(Val.of_optbool (Val.cmp_bool Cle v (Vint (Int.repr Int.max_signed)))) =*)
(*None -> False),*)
(*Some (Vint Int.one) =*)
(*Some (Val.of_optbool (Val.cmp_bool Cle v (Vint (Int.repr Int.max_signed)))).*)
(*Proof.*)
(*intros; destruct v. simpl in *; try discriminate CONTRA; auto.*)
Lemma simplify_ccomp_correct: forall c r r0 (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;;
DO hv2 <~ hsi_sreg_get hst r0;;
......@@ -1305,6 +1342,16 @@ Proof.
destruct (Int.eq _ _); inv H; auto.
Qed.
Lemma mkimm_pair_equal: forall n hi lo,
make_immed32 n = Imm32_pair hi lo ->
hi = (Int.shru (Int.sub n (Int.sign_ext 12 n)) (Int.repr 12)) /\
lo = (Int.sign_ext 12 n).
Proof.
intros. unfold make_immed32 in H.
destruct (Int.eq _ _) in H; try congruence.
inv H. auto.
Qed.
(* TODO gourdinl Lemma mkimm_pair_lo_zero_equal: forall n hi lo,
make_immed32 n = Imm32_pair hi lo ->
Int.eq n Int.zero = false ->
......@@ -1317,8 +1364,8 @@ Proof.
rewrite Int.sub_zero_l. unfold Int.shru, Int.shl.
*)
Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32u c hv1 n ~> hv
Lemma simplify_ccompimm_correct: forall c n r (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32s c hv1 n ~> hv
THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset)
(m0 : mem) (st : sistate_local),
hsilocal_refines ge sp rs0 m0 hst st ->
......@@ -1326,66 +1373,180 @@ Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local),
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m) <> None ->
IN eval_operation ge sp (Ocmp (Ccompimm c n)) args m) <> None ->
seval_sval ge sp (hsval_proj hv) rs0 m0 =
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m)).
IN eval_operation ge sp (Ocmp (Ccompimm c n)) args m)).
Proof.
unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl.
- wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail).
unfold expanse_condimm_int32s, cond_int32s in *; destruct c;
intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32.
1,3,5,7,9,11:
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence;
try (simplify_SOME z; contradiction; fail);
try erewrite H9; eauto; try erewrite H8; eauto;
try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
apply Int.same_if_eq in EQIMM; subst. trivial.
- unfold loadimm32. destruct (make_immed32 n) eqn:EQMKI;
4: rewrite <- xor_neg_ltle_cmp; unfold Val.cmp.
5: intros; replace (Clt) with (swap_comparison Cgt) by auto;
unfold Val.cmp; rewrite Val.swap_cmp_bool; trivial.
6: intros; replace (Clt) with (negate_comparison Cge) by auto;
unfold Val.cmp; rewrite Val.negate_cmp_bool; rewrite xor_neg_optb.
1,2,3,4,5,6: apply Int.same_if_eq in EQIMM; subst; trivial.
all:
specialize make_immed32_sound with n;
destruct (make_immed32 n) eqn:EQMKI;
try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX;
try destruct (Int.eq lo Int.zero) eqn:EQLO.
19,21,22:
specialize make_immed32_sound with (Int.one);
destruct (make_immed32 Int.one) eqn:EQMKI_A1.
25,26,27:
specialize make_immed32_sound with (Int.add n Int.one);
destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2.
all:
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail);
try erewrite H9; eauto; try erewrite H8; eauto;
all: try (simplify_SOME z; contradiction; fail).
all:
try erewrite H12; eauto; try erewrite H11; eauto;
try erewrite H10; eauto; try erewrite H9; eauto; try erewrite H8; eauto;
try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
+ apply mkimm_single_equal in EQMKI; subst.
rewrite Int.add_commut, Int.add_zero_l. trivial.
+ admit.
+ admit.
- (* TODO gourdinl same as first goal *)
simplify_SOME z; unfold Val.cmp, zero32; intros; try contradiction.
all: try apply Int.same_if_eq in H1; subst.
all: try apply Int.same_if_eq in EQLO; subst.
all: try apply Int.same_if_eq in EQMAX; subst.
all: try rewrite Int.add_commut, Int.add_zero_l; trivial.
all: try apply xor_ceq_zero; auto.
(* Problème d'implémentation lié au addiwr0 ?
--> On dirait que comme l'instruction n'a pas d'argument une fois expansée,
un cas spécial se produit si l'argument de départ n'est pas un entier :
L'instruction addiwr0 est configurée pour toujours renvoyer Int.one,
mais si le premier argument de la comparaison originelle n'est pas un
Vint, alors on se retrouve avec :
Some (Vint Int.one) = Some (Val.of_optbool None)
<-> Some (Vint Int.zero) = Some (Vundef)
Il faudrait peut-être modifier la sémantique dans Op pour éliminer ce cas. *)
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
{ unfold Val.cmp_bool; destruct z0; simpl; auto.
unfold Int.lt. replace (Int.signed (Int.add imm Int.one)) with (Int.signed imm + 1).
destruct (zlt (Int.signed imm) (Int.signed i)).
rewrite zlt_false by omega. auto.
rewrite zlt_true by omega. auto.
rewrite Int.add_signed. symmetry; apply Int.signed_repr.
specialize (Int.eq_spec imm (Int.repr Int.max_signed)).
rewrite EQMAX; simpl; intros.
assert (Int.signed imm <> Int.max_signed).
{ red; intros E. elim H8. rewrite <- (Int.repr_signed imm). rewrite E. auto. }
generalize (Int.signed_range imm); omega. }
{ apply Int.same_if_eq in H2; subst.
rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in H.
rewrite Int.add_zero_l in H. rewrite <- H.
unfold Val.cmp_bool; destruct z6; simpl; auto.
unfold Int.lt. replace (Int.signed (Int.add imm Int.one)) with (Int.signed imm + 1).
destruct (zlt (Int.signed imm) (Int.signed i)).
rewrite zlt_false by omega. auto.
rewrite zlt_true by omega. auto.
rewrite Int.add_signed. symmetry; apply Int.signed_repr.
specialize (Int.eq_spec imm (Int.repr Int.max_signed)).
rewrite EQMAX; simpl; intros.
assert (Int.signed imm <> Int.max_signed).
{ red; intros E. elim H2. rewrite <- (Int.repr_signed imm). rewrite E. auto. }
generalize (Int.signed_range imm); omega. }
rewrite Int.not_lt. destruct (Int.eq i imm) eqn:EQ.
- apply Int.same_if_eq in EQ; subst.
rewrite orb_true_r. rewrite Int.lt_not.
assert ((Int.eq (Int.add imm Int.one) imm) = false).
{ apply Int.eq_false. unfold Int.add.
erewrite Int.translate_lt; eauto.
destruct (Int.lt _ _) eqn:CONTRA; auto.
unfold Int.lt in CONTRA.
assert ((Int.signed imm) < (Int.signed (Int.add imm Int.one))).
{
apply xor_ceq_zero.
all: try rewrite <- xor_neg_ltle_cmp; unfold Val.cmp; trivial.
all: intros; replace (Clt) with (negate_comparison Cge) by auto;
rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb; trivial.
Qed.
Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32u c hv1 n ~> hv
THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset)
(m0 : mem) (st : sistate_local),
hsilocal_refines ge sp rs0 m0 hst st ->
hsok_local ge sp rs0 m0 hst ->
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m) <> None ->
seval_sval ge sp (hsval_proj hv) rs0 m0 =
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m)).
Proof.
unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
unfold loadimm32, sltuimm32, opimm32, load_hilo32.
1,3,5,7,9,11:
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail).
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence;
try (simplify_SOME z; contradiction; fail);
try erewrite H9; eauto; try erewrite H8; eauto;
try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
apply Int.same_if_eq in EQIMM; subst. trivial.
- admit.
- (* TODO gourdinl same as first goal *)
4: rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu.
5: intros; replace (Clt) with (swap_comparison Cgt) by auto;
rewrite Val.swap_cmpu_bool; trivial.
6: intros; replace (Clt) with (negate_comparison Cge) by auto;
rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb.
1,2,3,4,5,6: apply Int.same_if_eq in EQIMM; subst; trivial.
all:
specialize make_immed32_sound with n;
destruct (make_immed32 n) eqn:EQMKI;
try destruct (Int.eq lo Int.zero) eqn:EQLO.
all:
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail).
try erewrite H9; eauto; try erewrite H8; eauto;
all: try (simplify_SOME z; contradiction; fail).
all:
try erewrite H11; eauto;
try erewrite H10; eauto; try erewrite H9; eauto; try erewrite H8; eauto;
try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
apply Int.same_if_eq in EQIMM; subst. trivial.
- (* same *) admit.
- (* same *) admit.
- (* same *) admit.
- (* same *) admit.
- (* same *) admit.
- (* same *) admit.
- (* same *) admit.
Admitted.
all: try apply Int.same_if_eq in H1; subst.
all: try apply Int.same_if_eq in EQLO; subst.
all: try rewrite Int.add_commut, Int.add_zero_l; trivial.
all: try rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu; trivial.
all: intros; replace (Clt) with (negate_comparison Cge) by auto;
rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb; trivial.
Qed.
Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;;
......@@ -2046,7 +2207,7 @@ Lemma hsiexec_inst_correct i hst:
exists st', siexec_inst i st = Some st'
/\ (forall (REF:hsistate_refines_stat hst st), hsistate_refines_stat hst' st')
/\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st').
Proof. Admitted. (*
Proof.
destruct i; simpl;
try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail).
- (* refines_dyn Iop *)
......@@ -2086,7 +2247,7 @@ Proof. Admitted. (*
destruct (Int.eq _ _) eqn:EQIMM; simpl.
1: admit.
unfold loadimm32; destruct make_immed32.
unfold loadimm32; destruct make_immed32 eqn:EQMKI.
{
wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
* unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
......@@ -2098,13 +2259,14 @@ Proof. Admitted. (*
intros; erewrite seval_condition_refines; eauto.
destruct c0; simpl; unfold seval_condition.
{ simpl in *.
erewrite H4; eauto.
erewrite H3; eauto; erewrite H2; eauto.
simpl.
erewrite H1; eauto. try erewrite H0; eauto;
try erewrite H; eauto; simplify_SOME z.
{ simpl in *. apply mkimm_single_equal in EQMKI; subst.
destruct (seval_smem _ _ _ _ _) eqn:EQSM; try congruence.
- erewrite H4; eauto; erewrite H3; eauto;
erewrite H2; eauto; erewrite H1; eauto;
try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z. rewrite Int.add_zero. trivial.
- simplify_SOME x.
}
2: {
generalize (sok_local_set_sreg_simp (Rop (OEaddiwr0 imm))); simpl; eauto.
intros.j
......
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