diff options
Diffstat (limited to 'riscV/Asmgenproof1.v')
| -rw-r--r-- | riscV/Asmgenproof1.v | 56 |
1 files changed, 46 insertions, 10 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 1e17c4e2..cbe68577 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -529,31 +529,37 @@ Proof. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; @@ -591,31 +597,37 @@ Proof. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. Qed. @@ -1262,12 +1274,7 @@ Opaque Int.eq. { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) - { unfold get_opimmR0; destruct opi; simpl; - econstructor; split; try apply exec_straight_one; simpl; eauto; - split; intros; Simpl. - try rewrite Int.add_commut; auto. - try rewrite Int64.add_commut; auto. } - 7,8,9,16,17,18: + 8,9,17,18: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; try destruct (rs x0); try rewrite Int64.add_commut; @@ -1276,12 +1283,41 @@ Opaque Int.eq. try rewrite Int.and_commut; auto; try rewrite Int64.or_commut; try rewrite Int.or_commut; auto. - 1-12: - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; inv EQ3; + 1-14: + destruct optR as [[]|]; try discriminate; + try (ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl); + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; try inv EQ3; try inv EQ2; + try destruct (Int.eq _ _) eqn:A; try inv H0; + try destruct (Int64.eq _ _) eqn:A; try inv H1; econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; - destruct (rs x0); auto; - destruct (rs x1); auto. + try apply Int.same_if_eq in A; subst; + try apply Int64.same_if_eq in A; subst; + unfold get_sp; + try destruct (rs x0); auto; + try destruct (rs x1); auto; + try destruct (rs X2); auto; + try destruct Archi.ptr64 eqn:B; + try fold (Val.add (Vint Int.zero) (get_sp (rs X2))); + try fold (Val.addl (Vlong Int64.zero) (get_sp (rs X2))); + try rewrite Val.add_commut; auto; + try rewrite Val.addl_commut; auto; + try rewrite Int.add_commut; auto; + try rewrite Int64.add_commut; auto; + replace (Ptrofs.of_int Int.zero) with (Ptrofs.zero) by auto; + replace (Ptrofs.of_int64 Int64.zero) with (Ptrofs.zero) by auto; + try rewrite Ptrofs.add_zero; auto. + (* mayundef *) + { destruct (ireg_eq x x0); inv EQ2; + econstructor; split; + try apply exec_straight_one; simpl; eauto; + split; unfold eval_may_undef; + destruct mu eqn:EQMU; simpl; intros; Simpl; auto. + all: + destruct (rs (preg_of m0)) eqn:EQM0; simpl; auto; + destruct (rs x0); simpl; auto; Simpl; + try destruct (Int.ltu _ _); simpl; + Simpl; auto. } (* select *) { econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. |