From 7f8ccba038ce9bf7665341c05b89bb5d9b9b536b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 3 Feb 2021 12:29:11 +0100 Subject: Ccomp for long --- riscV/Asmgenproof1.v | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'riscV/Asmgenproof1.v') 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 *) -- cgit