From e8322076875090a68fc6ca3607ddde8e5717a8b5 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 23 Feb 2021 10:03:28 +0100 Subject: Some more proofs on branch expansion, using make_immed32_sound --- scheduling/RTLpathSE_impl.v | 280 ++++++++++++++++++++++++++++++++++---------- 1 file changed, 221 insertions(+), 59 deletions(-) (limited to 'scheduling') diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 32761c6e..a5f6cf46 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -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 -- cgit