From df9aab806ae8d20393b56e4175e210ed6cff1ef1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 30 Mar 2021 12:48:51 +0200 Subject: a more general way to manage special registers before introducing SP --- riscV/Asmgenproof1.v | 142 ++++++++++++++++++++++++++------------------------- 1 file changed, 73 insertions(+), 69 deletions(-) (limited to 'riscV/Asmgenproof1.v') diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 6e5cc531..1e17c4e2 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -494,124 +494,128 @@ Proof. split. rewrite V; destruct normal, b; reflexivity. intros; Simpl. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; - eexists; eexists; eauto; split; constructor; auto; + destruct (rs x) eqn:EQRS; simpl in *; try congruence; + inv EQ2; eexists; eexists; eauto; split; constructor; auto; simpl in *. - + destruct (rs x); simpl in *; try congruence. + + rewrite EQRS; assert (HB: (Int.eq Int.zero i) = b) by congruence. rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. + + rewrite EQRS; assert (HB: (Int.eq i Int.zero) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. + rewrite <- HB; destruct b; simpl; auto. + + rewrite EQRS; destruct (rs x0); try congruence. assert (HB: (Int.eq i i0) = b) by congruence. - rewrite HB; destruct b; simpl; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + rewrite <- HB; destruct b; simpl; auto. +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; - eexists; eexists; eauto; split; constructor; auto; + destruct (rs x) eqn:EQRS; simpl in *; try congruence; + inv EQ2; eexists; eexists; eauto; split; constructor; auto; simpl in *. - + destruct (rs x); simpl in *; try congruence. + + rewrite EQRS; assert (HB: negb (Int.eq Int.zero i) = b) by congruence. rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. + + rewrite EQRS; assert (HB: negb (Int.eq i Int.zero) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. + rewrite <- HB; destruct b; simpl; auto. + + rewrite EQRS; destruct (rs x0); try congruence. assert (HB: negb (Int.eq i i0) = b) by congruence. - rewrite HB; destruct b; simpl; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; + rewrite <- HB; destruct b; simpl; auto. +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32 in *; inv EQ2; + destruct (rs x) eqn:EQRS; simpl in *; try congruence; eexists; eexists; eauto; split; constructor; simpl in *; auto. - + destruct (rs x); simpl in *; try congruence. + + rewrite EQRS; assert (HB: (Int64.eq Int64.zero i) = b) by congruence. rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. + + rewrite EQRS; assert (HB: (Int64.eq i Int64.zero) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. + rewrite <- HB; destruct b; simpl; auto. + + rewrite EQRS; destruct (rs x0); try congruence. assert (HB: (Int64.eq i i0) = b) by congruence. - rewrite HB; destruct b; simpl; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; + rewrite <- HB; destruct b; simpl; auto. +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32 in *; inv EQ2; + destruct (rs x) eqn:EQRS; simpl in *; try congruence; eexists; eexists; eauto; split; constructor; simpl in *; auto. - + destruct (rs x); simpl in *; try congruence. + + rewrite EQRS; assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. + + rewrite EQRS; assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. + rewrite <- HB; destruct b; simpl; auto. + + rewrite EQRS; destruct (rs x0); try congruence. assert (HB: negb (Int64.eq i i0) = b) by congruence. - rewrite HB; destruct b; simpl; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; + rewrite <- HB; destruct b; simpl; auto. +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; +- destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. Qed. @@ -1273,7 +1277,7 @@ Opaque Int.eq. try rewrite Int64.or_commut; try rewrite Int.or_commut; auto. 1-12: - destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; + destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; inv EQ3; econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; destruct (rs x0); auto; -- cgit