diff options
Diffstat (limited to 'aarch64/Asmblockdeps.v')
-rw-r--r-- | aarch64/Asmblockdeps.v | 57 |
1 files changed, 30 insertions, 27 deletions
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 71b7c317..8ec862da 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -1485,27 +1485,26 @@ Ltac replace_regs_cond_force := try replace (2) with (#CN) in * by auto. Ltac validate_crbit_flags rr v1 v2 := - destruct (R.eq_dec 5 (#rr)) as [eCV|eCV]; subst; - [ destruct v1; destruct v2; simpl; - replace_regs_cond_force; apply ppos_equal in eCV; subst; - rewrite Pregmap.gss; auto | - destruct (R.eq_dec 4 (#rr)) as [eCC|eCC]; subst; - [ destruct v1; destruct v2; simpl; - replace_regs_cond_force; apply ppos_equal in eCC; subst; - rewrite Pregmap.gso, Pregmap.gss; auto; try discriminate | - destruct (R.eq_dec 3 (#rr)) as [eCZ|eCZ]; subst; - [ destruct v1; destruct v2; simpl; - replace_regs_cond_force; apply ppos_equal in eCZ; subst; - rewrite 2Pregmap.gso, Pregmap.gss; auto; try discriminate | - destruct (R.eq_dec 2 (#rr)) as [eCN|eCN]; subst; - [ destruct v1; destruct v2; simpl; - replace_regs_cond_force; apply ppos_equal in eCN; subst; - rewrite 3Pregmap.gso, Pregmap.gss; auto; try discriminate | - destruct v1; destruct v2; simpl; + destruct (R.eq_dec 5 (#rr)) as [e0|n0]; + destruct (R.eq_dec 4 (#rr)) as [e1|n1]; + destruct (R.eq_dec 3 (#rr)) as [e2|n2]; + destruct (R.eq_dec 2 (#rr)) as [e3|n3]; replace_regs_cond_force; - apply ppos_discr in eCV; apply ppos_discr in eCC; - apply ppos_discr in eCZ; apply ppos_discr in eCN; - rewrite 4Pregmap.gso; auto; try discriminate ]]]]. + try apply ppos_equal in e0; + try apply ppos_equal in e1; + try apply ppos_equal in e2; + try apply ppos_equal in e3; + try apply ppos_discr in n0; + try apply ppos_discr in n1; + try apply ppos_discr in n2; + try apply ppos_discr in n3; + subst. + +Ltac Simpl_flags := + try (rewrite Pregmap.gss; reflexivity); + try (rewrite Pregmap.gso, Pregmap.gss; [reflexivity|]; try auto); + try (rewrite Pregmap.gso; try auto); + try (rewrite !Pregmap.gso; try auto). Lemma compare_single_res: forall sr mr rsr rr v1 v2 (HMEM: sr pmem = Memstate mr) @@ -1519,6 +1518,7 @@ Val Proof. intros. unfold v_compare_single, compare_single, assign. validate_crbit_flags rr v1 v2. + all: destruct v1; destruct v2; Simpl_flags. Qed. Lemma compare_float_res: forall sr mr rsr rr v1 v2 @@ -1533,6 +1533,7 @@ Val Proof. intros. unfold v_compare_float, compare_float, assign. validate_crbit_flags rr v1 v2. + all: destruct v1; destruct v2; Simpl_flags. Qed. Lemma compare_long_res: forall sr mr rsr rr v1 v2 @@ -1547,6 +1548,7 @@ Val Proof. intros. unfold v_compare_long, compare_long, assign. validate_crbit_flags rr v1 v2. + all: Simpl_flags. Qed. Lemma compare_int_res: forall sr mr rsr rr v1 v2 @@ -1561,6 +1563,7 @@ Val Proof. intros. unfold v_compare_int, compare_int, assign. validate_crbit_flags rr v1 v2. + all: Simpl_flags. Qed. Section SECT_SEQ. @@ -1612,13 +1615,13 @@ Proof. try (eapply compare_long_res; eauto); try (eapply compare_float_res; eauto). - (* PArithComparisonR0R *) - simpl. destruct r1; ( - simpl; destruct i; - repeat Simpl_rep sr; Simpl_exists sr; - unfold arith_eval_comparison_r0r, arith_comparison_r0r_isize; destruct arith_prepare_comparison_r0r; destruct is; - simpl; intros rr; try destruct sz; - try (eapply compare_long_res; eauto); - try (eapply compare_int_res; eauto)). + simpl; destruct r1; simpl; destruct i; + repeat (replace_regs_cond_force; try fold (ppos r); try fold(ppos r2); + try rewrite !assign_diff; discriminate_ppos; try rewrite !H0); + Simpl sr; unfold arith_eval_comparison_r0r, arith_comparison_r0r_isize; + destruct arith_prepare_comparison_r0r; destruct is; + try (eapply compare_long_res; eauto); + try (eapply compare_int_res; eauto). - (* PArithComparisonP *) simpl; destruct i; unfold arith_eval_comparison_p, arith_prepare_comparison_p; simpl; |