From 95dc0730b9fa0f7d60222f53d7cdc3aed14206da Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 17 Dec 2020 15:25:31 +0100 Subject: Some progress in Asmblockgenproof --- aarch64/Asmblockgenproof1.v | 223 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 211 insertions(+), 12 deletions(-) (limited to 'aarch64/Asmblockgenproof1.v') diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v index bc4302ca..870211b8 100644 --- a/aarch64/Asmblockgenproof1.v +++ b/aarch64/Asmblockgenproof1.v @@ -1121,32 +1121,213 @@ Proof. destruct r; try contradiction; destruct v1; auto; destruct v2; auto. Qed. -Lemma transl_cbranch_correct: - forall cond args lbl k c m ms b sp rs m' bdy t ofs, - transl_cond_branch cond args lbl k = OK (bdy, c) -> +Lemma cmpu_bool_some_b: forall n x rs m0 b tbb, + Int.eq n Int.zero = true -> + Val.cmp_bool Ceq (rs (preg_of m0)) (Vint n) = Some b -> + ireg_of m0 = OK x -> + Val_cmpu_bool Ceq (incrPC (Ptrofs.repr (size tbb)) rs x) (Vint Int.zero) = Some b. +Proof. + intros. + replace (Vint Int.zero) with (Vint n). + 2: { apply f_equal. apply Int.same_if_eq; auto. } + unfold incrPC. Simpl. replace (rs (preg_of m0)) with (rs x) in H0. auto. + apply f_equal. symmetry. apply ireg_of_eq; auto. +Qed. + +Lemma transl_cbranch_correct_1: + forall cond args lbl c k b m ms sp rs m' tbb bdy, + transl_cond_branch cond args lbl k = OK (bdy,c) -> eval_condition cond (List.map ms args) m = Some b -> agree ms sp rs -> Mem.extends m m' -> - exists rs' m' rs'' m'', - exec_body lk ge bdy rs m = Next rs' m' - /\ exec_exit ge fn ofs rs' m' (Some c) t rs'' m'' + exists rs', + exec_straight_opt ge lk bdy rs m' k rs' m' + /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = eval_branch fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m' (Some b) /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. + intros until bdy; intros TR EC AG MEMX. + set (vl' := map rs (map preg_of args)). + assert (EVAL': eval_condition cond vl' m' = Some b). + { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. } + destruct cond; unfold transl_cond_branch in TR; + try unfold transl_cond_branch_default in TR; + simpl in TR; destruct args; ArgsInv. +- (* Ccomp *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_signed_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_sint; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccompu *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_uint; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccompimm *) +admit. +(* destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]; + destruct c0; try destruct (Int.eq n Int.zero) eqn:IEQ; + monadInv TR; try monadInv EQ; econstructor; split; + try (econstructor; try apply exec_straight_one); + simpl in *; eauto; try (split; intros; auto). + all: try (erewrite (cmpu_bool_some_b n x rs m0 b tbb); eauto; assumption). + unfold incrPC; Simpl. + try (rewrite (cmpu_bool_some_b n x rs m0 b tbb); auto). + + monadInv TR; try monadInv EQ. econstructor; split. econstructor; apply exec_straight_one. simpl in *; eauto. + split; intros; auto. unfold compare_int, incrPC. Simpl. auto. + assert (Val_cmpu_bool Ceq (incrPC (Ptrofs.repr (size tbb)) rs x) (Vint Int.zero) = Some b). + { replace (Vint Int.zero) with (Vint n). + 2: { apply f_equal. apply Int.same_if_eq; auto. } + unfold incrPC. Simpl. replace (rs (preg_of m0)) with (rs x) in EVAL'. auto. + apply f_equal. symmetry. apply ireg_of_eq; auto. } + rewrite H; auto. + inv EQ. + split; intros; auto. assert (eval_testcond (cond_for_unsigned_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_uint; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. + + destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. ++ econstructor; split. + apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. + split; intros. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. ++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply eval_testcond_compare_sint; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. *) +- (* Ccompuimm *) + admit. +- (* Ccompshift *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_signed_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) + (compare_int rs (rs x) (eval_shift_op_int (rs x0) (transl_shift s a)))) = Some b). + { apply eval_testcond_compare_sint; auto. rewrite transl_eval_shift; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccompushift *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) + (compare_int rs (rs x) (eval_shift_op_int (rs x0) (transl_shift s a)))) = Some b). + { apply eval_testcond_compare_uint; auto. rewrite transl_eval_shift; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Cmaskzero *) admit. +- (* Cmasknotzero *) admit. +- (* Ccompl *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_signed_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_long rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_slong; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccomplu *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_long rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_ulong; auto. eapply Val_cmplu_bool_correct; eauto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccomplimm *) admit. +- (* Ccompluimm *) admit. +- (* Ccomplshift *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_signed_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) + (compare_long rs (rs x) (eval_shift_op_long (rs x0) (transl_shift s a)))) = Some b). + { apply eval_testcond_compare_slong; auto. rewrite transl_eval_shiftl; auto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Ccomplushift *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) + (compare_long rs (rs x) (eval_shift_op_long (rs x0) (transl_shift s a)))) = Some b). + { apply eval_testcond_compare_ulong; auto. rewrite transl_eval_shiftl; auto. + eapply Val_cmplu_bool_correct; eauto. } rewrite H. auto. + destruct r; reflexivity || discriminate. +- (* Cmasklzero *) admit. +- (* Cmasknotzero *) admit. +- (* Ccompf *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_float; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Cnotcompf *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_not_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_not_float; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Ccompfzero *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (Vfloat Float.zero))) = Some b). + { apply eval_testcond_compare_float; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Cnotcompfzero *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_not_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (Vfloat Float.zero))) = Some b). + { apply eval_testcond_compare_not_float; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Ccompfs *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_single; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_single_inv; auto. +- (* Cnotcompfs *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_not_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (rs x0))) = Some b). + { apply eval_testcond_compare_not_single; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_single_inv; auto. +- (* Ccompfszero *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (Vsingle Float32.zero))) = Some b). + { apply eval_testcond_compare_single; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_single_inv; auto. +- (* Cnotcompfszero *) + econstructor; split. econstructor; apply exec_straight_one. simpl; eauto. + split; intros. assert (eval_testcond (cond_for_float_not_cmp c0) + (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (Vsingle Float32.zero))) = Some b). + { apply eval_testcond_compare_not_single; auto. } rewrite H. auto. + destruct r; discriminate || rewrite compare_single_inv; auto. Admitted. -(* Lemma transl_cbranch_correct_true: - forall cond args lbl k c m ms sp rs m' bdy, - transl_cond_branch cond args lbl k = OK (bdy, c) -> +Lemma transl_cbranch_correct_true: + forall cond args lbl k c m ms sp rs m' tbb bdy, + transl_cond_branch cond args lbl k = OK (bdy,c) -> eval_condition cond (List.map ms args) m = Some true -> agree ms sp rs -> Mem.extends m m' -> - exists rs', exists insn, + exists rs', exec_straight_opt ge lk bdy rs m' k rs' m' - /\ exec_cfi ge fn insn (nextinstr rs') m' = goto_label fn lbl (nextinstr rs') m' + /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = goto_label fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m' /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. intros. eapply transl_cbranch_correct_1 with (b := true); eauto. -Qed. *) +Qed. + +Lemma transl_cbranch_correct_false: + forall cond args lbl k c m ms sp rs m' tbb bdy, + transl_cond_branch cond args lbl k = OK (bdy,c) -> + eval_condition cond (List.map ms args) m = Some false -> + agree ms sp rs -> + Mem.extends m m' -> + exists rs', + exec_straight_opt ge lk bdy rs m' k rs' m' + /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = Next (incrPC (Ptrofs.repr (size tbb)) rs') m' + /\ forall r, data_preg r = true -> rs'#r = rs#r. +Proof. + intros. exploit transl_cbranch_correct_1. all: eauto. +Qed. Lemma transl_cond_correct: forall cond args k c rs m, @@ -1727,6 +1908,24 @@ Proof. split. Simpl. intros; Simpl. Qed. +Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset), + Mem.storev Mint64 m (Val.offset_ptr rs#base ofs) rs#src = Some m' -> + preg_of_iregsp base <> IR X16 -> + (DR (IR (RR1 src))) <> (DR (IR (RR1 X16))) -> + exists rs', + exec_straight ge lk (storeptr_bc src base ofs k) rs m k rs' m' + /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r. +Proof. + intros. + destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. + exploit indexed_memory_access_correct; eauto. intros (ad & rs' & A & B & C). + econstructor; split. + eapply exec_straight_opt_right. eexact A. + apply exec_straight_one. simpl. unfold exec_store_rs_a. rewrite B, C, H. eauto. + discriminate. auto. + intros; Simpl. rewrite C; auto. +Qed. + Lemma loadind_correct: forall (base: iregsp) ofs ty dst k c (rs: regset) m v, loadind base ofs ty dst k = OK c -> -- cgit