diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-11 20:03:49 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-11 20:03:49 +0100 |
| commit | adf1bbcd5c356a0cb75c412357a3b7af23795f47 (patch) | |
| tree | 2e6a75bbee70c0377868861fc85976fccf017547 /riscV/Asmgenproof1.v | |
| parent | c40646559461154e5190a4c887f9992f35eedb9f (diff) | |
| download | compcert-kvx-adf1bbcd5c356a0cb75c412357a3b7af23795f47.tar.gz compcert-kvx-adf1bbcd5c356a0cb75c412357a3b7af23795f47.zip | |
[Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof
Diffstat (limited to 'riscV/Asmgenproof1.v')
| -rw-r--r-- | riscV/Asmgenproof1.v | 69 |
1 files changed, 64 insertions, 5 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 57d281ec..0b1abe2a 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -497,6 +497,36 @@ Proof. - destruct optR0 as [[]|]; unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; auto; + simpl in *. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int.eq Int.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int.eq i Int.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + 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 *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; auto; + simpl in *. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int.eq Int.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int.eq i Int.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + 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 *; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR0 as [[]|]; @@ -528,6 +558,36 @@ Proof. unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; unfold zero64, Op.zero64 in *; eexists; eexists; eauto; split; constructor; + simpl in *; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int64.eq Int64.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int64.eq i Int64.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + 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 *; + eexists; eexists; eauto; split; constructor; + simpl in *; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + 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 *; + eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR0 as [[]|]; unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; @@ -1198,13 +1258,15 @@ 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 *) - 5: econstructor; split; try apply exec_straight_one; simpl; eauto; + 7: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; rewrite Int.add_commut; auto. - 9: econstructor; split; try apply exec_straight_one; simpl; eauto; + 13: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; rewrite Int64.add_commut; auto. all: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl. + all: destruct (rs x0); auto. + all: destruct (rs x1); auto. Qed. (** Memory accesses *) @@ -1512,6 +1574,3 @@ Proof. Qed. End CONSTRUCTORS. - - - |