diff options
Diffstat (limited to 'riscV/Asmgenproof1.v')
| -rw-r--r-- | riscV/Asmgenproof1.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index ee203da4..49635ebd 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -832,7 +832,7 @@ Proof. + apply DFL. Qed. -Lemma transl_cond_op_correct: +(* TODO Lemma transl_cond_op_correct: forall cond rd args k c rs m, transl_cond_op cond rd args k = OK c -> exists rs', @@ -844,7 +844,7 @@ Proof. { destruct ob as [[]|]; reflexivity. } intros until m; intros TR. destruct cond; simpl in TR; ArgsInv. -(* TODO + (* cmp *) ++ (* 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). @@ -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)). @@ -923,7 +923,7 @@ Proof. * econstructor; split. apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto. split; intros; Simpl. -Qed. + Qed.*) (** Some arithmetic properties. *) @@ -1134,8 +1134,8 @@ Opaque Int.eq. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } (* cond *) - { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). - exists rs'; split. eexact A. eauto with asmgen. } + (* TODO { 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; split; intros; Simpl; rewrite Int.add_commut; auto. |