diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-03 17:14:23 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-03 17:14:23 +0100 |
| commit | 29ba37cc21cedc09b20bbd8adfa0ec52c48365c0 (patch) | |
| tree | 673c5cdb7b99756c4c6880e7ef0b14bed7544bc2 /riscV/Asmgenproof1.v | |
| parent | 7f8ccba038ce9bf7665341c05b89bb5d9b9b536b (diff) | |
| download | compcert-kvx-29ba37cc21cedc09b20bbd8adfa0ec52c48365c0.tar.gz compcert-kvx-29ba37cc21cedc09b20bbd8adfa0ec52c48365c0.zip | |
All Ocmp expanded in RTL
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. |