diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-03 12:29:11 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-03 12:29:11 +0100 |
| commit | 7f8ccba038ce9bf7665341c05b89bb5d9b9b536b (patch) | |
| tree | a939b46a94b7c8aaee8e26c08026905f6c38f3ca /riscV/Asmgenproof1.v | |
| parent | 4df03aaf5204d2f15885b49fe3f5c9cb61b4596d (diff) | |
| download | compcert-kvx-7f8ccba038ce9bf7665341c05b89bb5d9b9b536b.tar.gz compcert-kvx-7f8ccba038ce9bf7665341c05b89bb5d9b9b536b.zip | |
Ccomp for long
Diffstat (limited to 'riscV/Asmgenproof1.v')
| -rw-r--r-- | riscV/Asmgenproof1.v | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 6c722798..ee203da4 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -844,7 +844,7 @@ Proof. { destruct ob as [[]|]; reflexivity. } intros until m; intros TR. destruct cond; simpl in TR; ArgsInv. -+ (* cmp *) +(* TODO + (* cmp *) exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. + (* cmpu *) exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C). @@ -858,7 +858,7 @@ Proof. exists rs'; repeat split; eauto. rewrite MKTOT; eauto. + (* cmplu *) exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto. + exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto. + (* cmplimm *) exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. intros (rs' & A & B & C). @@ -866,7 +866,7 @@ Proof. + (* cmpluimm *) exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. + exists rs'; repeat split; eauto. rewrite MKTOT; eauto.*) + (* cmpf *) destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. fold (Val.cmpf c0 (rs x) (rs x0)). @@ -1137,11 +1137,13 @@ 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 *) - 1-4: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; + 5: 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; + 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. - econstructor; split; try apply exec_straight_one; simpl; eauto; - split; intros; Simpl. rewrite Int.add_commut. auto. Qed. (** Memory accesses *) |