diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-10 10:34:38 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-10 10:34:38 +0100 |
| commit | 84cb4939653e5355c2039ed62a140aa392e21162 (patch) | |
| tree | 156a6a78208983cf7fca540899313144f36687e0 /riscV/Asmgenproof1.v | |
| parent | 3104e551bf87abeab9a257c955cf9b180769dc64 (diff) | |
| download | compcert-kvx-84cb4939653e5355c2039ed62a140aa392e21162.tar.gz compcert-kvx-84cb4939653e5355c2039ed62a140aa392e21162.zip | |
[Admitted checker] Checker expansion for reg Ocmp (without scratch)
Diffstat (limited to 'riscV/Asmgenproof1.v')
| -rw-r--r-- | riscV/Asmgenproof1.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 429c5fec..57d281ec 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -292,7 +292,7 @@ Qed. (** Translation of conditional branches *) -(* TODO REMOVE Lemma transl_cbranch_int32s_correct: +Lemma transl_cbranch_int32s_correct: forall cmp r1 r2 lbl (rs: regset) m b, Val.cmp_bool cmp rs##r1 rs##r2 = Some b -> exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m = @@ -375,7 +375,7 @@ Proof. rewrite <- Float32.cmp_swap. auto. - simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. rewrite <- Float32.cmp_swap. auto. - Qed.*) + Qed. (* TODO UNUSUED ? Remark branch_on_X31: forall normal lbl (rs: regset) m b, @@ -417,7 +417,7 @@ Proof. { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. } clear EVAL MEXT AG. destruct cond; simpl in TRANSL; ArgsInv. - (* TODO REMOVE - exists rs, (transl_cbranch_int32s c0 x x0 lbl). + - exists rs, (transl_cbranch_int32s c0 x x0 lbl). intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. - exists rs, (transl_cbranch_int32u c0 x x0 lbl). intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. @@ -492,7 +492,7 @@ Proof. econstructor; econstructor. split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl.*) + intros; Simpl. - destruct optR0 as [[]|]; unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; @@ -589,7 +589,7 @@ Qed. (** Translation of condition operators *) -(* TODO REMOVE Lemma transl_cond_int32s_correct: +Lemma transl_cond_int32s_correct: forall cmp rd r1 r2 k rs m, exists rs', exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m @@ -984,7 +984,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. *) @@ -1195,8 +1195,8 @@ Opaque Int.eq. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } (* cond *) - (* TODO REMOVE { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). - exists rs'; split. eexact A. eauto with asmgen. }*) + { 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. |