From f0a218800bf0b8a94da35fd8a0553184294f6368 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sat, 19 Dec 2020 18:01:10 +0100 Subject: Asmblockgenproof finished ! --- aarch64/Asmblockgenproof.v | 9 +- aarch64/Asmblockgenproof1.v | 338 +++++++++++++++++--------------------------- 2 files changed, 132 insertions(+), 215 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index 586286bd..1abcb570 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -77,11 +77,6 @@ Qed. Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs. -(*Lemma functions_bound_max_pos: forall fb f, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - (max_pos next f) <= Ptrofs.max_unsigned. -Admitted.*) - (** * Proof of semantic preservation *) (** Semantic preservation is proved using a complex simulation diagram @@ -881,7 +876,7 @@ exploit builtin_args_match; eauto. intros [vargs' [P Q]]. eapply preg_vals; eauto. all: eauto. intros EC. - exploit transl_cbranch_correct_true; eauto. intros (rs', H). + exploit transl_cbranch_correct_1; eauto. intros (rs', H). destruct H as [ES [ECFI]]. exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC). assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. } @@ -909,7 +904,7 @@ exploit builtin_args_match; eauto. intros [vargs' [P Q]]. all: eauto. intros EC. - exploit transl_cbranch_correct_false; eauto. intros (rs', H). + exploit transl_cbranch_correct_1; eauto. intros (rs', H). destruct H as [ES [ECFI]]. exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC). assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. } diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v index 870211b8..dd7803cd 100644 --- a/aarch64/Asmblockgenproof1.v +++ b/aarch64/Asmblockgenproof1.v @@ -1121,214 +1121,6 @@ Proof. destruct r; try contradiction; destruct v1; auto; destruct v2; auto. Qed. -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', - 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' 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', - exec_straight_opt ge lk bdy rs m' k 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. - -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, transl_cond cond args k = OK c -> @@ -1515,6 +1307,136 @@ Proof. destruct r; discriminate || rewrite compare_single_inv; auto. Qed. +Lemma transl_cond_correct': + forall cond args k c tbb rs m, + transl_cond cond args k = OK c -> + exists rs', + exec_straight ge lk c rs m k rs' m + /\ (forall b, + eval_condition cond (map rs (map preg_of args)) m = Some b -> + eval_testcond (cond_for_cond cond) (incrPC (Ptrofs.repr (size tbb)) rs') = Some b) + /\ forall r, data_preg r = true -> rs'#r = rs#r. +Proof. + intros until m; intros TR. + eapply transl_cond_correct; eauto. +Qed. + +Lemma transl_cbranch_correct_1: + forall cond args lbl c k b m rs tbb bdy, + transl_cond_branch cond args lbl k = OK (bdy,c) -> + eval_condition cond (map rs (map preg_of args)) m = Some b -> + 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 = + (if b then goto_label fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m else + Next (incrPC (Ptrofs.repr (size tbb)) rs') m) + /\ forall r, data_preg r = true -> rs'#r = rs#r. +Proof. +intros until bdy; intros TR EV. + assert (Archi.ptr64 = true) as SF; auto. + assert (DFL: + transl_cond_branch_default cond args lbl k = OK (bdy,c) -> + 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). + { + unfold transl_cond_branch_default; intros. monadInv H. + exploit transl_cond_correct'; eauto. intros (rs' & A & B & C). + eexists; split. + apply exec_straight_opt_intro. eexact A. + split; auto. simpl. rewrite (B b) by auto. auto. + } +Local Opaque transl_cond transl_cond_branch_default. + destruct args as [ | a1 args]; simpl in TR; auto. + destruct args as [ | a2 args]; simpl in TR; auto. + destruct cond; simpl in TR; auto. +- (* Ccompimm *) + destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; + apply Int.same_if_eq in N0; subst n; ArgsInv. ++ (* Ccompimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. + unfold incrPC. Simpl. rewrite EQRSX. simpl. auto. ++ (* Ccompimm Ceq 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + destruct (Int.eq i Int.zero); auto. +- (* Ccompuimm *) + destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto. + apply Int.same_if_eq in N0; subst n; ArgsInv. ++ (* Ccompuimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. apply Val_cmpu_bool_correct in EV. + unfold incrPC. Simpl. rewrite EV. auto. ++ (* Ccompuimm Ceq 0 *) + monadInv TR. ArgsInv. simpl in *. + econstructor; split. econstructor. + split; auto. simpl. unfold incrPC. Simpl. + apply Int.same_if_eq in N0; subst. + rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cne), EV. + destruct b; auto. +- (* Cmaskzero *) + destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. simpl. + erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. + unfold incrPC. Simpl. + rewrite (Val.negate_cmp_bool Ceq), EV. destruct b; auto. +- (* Cmasknotzero *) + destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. simpl. + erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. + unfold incrPC. Simpl. + rewrite EV. auto. +- (* Ccomplimm *) + destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; + apply Int64.same_if_eq in N0; subst n; ArgsInv. ++ (* Ccomplimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. + unfold incrPC. Simpl. rewrite EQRSX. simpl. auto. ++ (* Ccomplimm Ceq 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + destruct (Int64.eq i Int64.zero); auto. +- (* Ccompluimm *) + destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; + apply Int64.same_if_eq in N0; subst n; ArgsInv. ++ (* Ccompluimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. apply Val_cmplu_bool_correct in EV. + unfold incrPC. Simpl. rewrite EV. auto. ++ (* Ccompluimm Ceq 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + destruct (Int64.eq i Int64.zero); auto. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + rewrite SF in *; simpl in *. + rewrite Int64.eq_true in *. + destruct ((Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); simpl in *. + assert (b = true). { destruct b; try congruence. } + rewrite H; auto. discriminate. +- (* Cmasklzero *) + destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. + erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. + unfold incrPC. Simpl. + rewrite (Val.negate_cmpl_bool Ceq), EV. destruct b; auto. +- (* Cmasklnotzero *) + destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. + erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. + unfold incrPC. Simpl. + rewrite EV. auto. +Qed. + Lemma transl_op_correct: forall op args res k (rs: regset) m v c, transl_op op args res k = OK c -> -- cgit