From acb41b1af6e5e4c933e3be1b17f6e5012eca794d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sat, 6 Feb 2021 16:53:46 +0100 Subject: cond and branches expanded --- riscV/Asmgenproof1.v | 81 +++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 71 insertions(+), 10 deletions(-) (limited to 'riscV/Asmgenproof1.v') diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 49635ebd..429c5fec 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -292,7 +292,7 @@ Qed. (** Translation of conditional branches *) -Lemma transl_cbranch_int32s_correct: +(* TODO REMOVE 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,16 +375,16 @@ 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.*) -Remark branch_on_X31: +(* TODO UNUSUED ? Remark branch_on_X31: forall normal lbl (rs: regset) m b, rs#X31 = Val.of_bool (eqb normal b) -> exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m = eval_branch fn lbl rs m (Some b). Proof. intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. -Qed. + Qed.*) Ltac ArgsInv := repeat (match goal with @@ -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. -- exists rs, (transl_cbranch_int32s c0 x x0 lbl). + (* TODO REMOVE - 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,68 @@ 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 *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. Qed. Lemma transl_cbranch_correct_true: @@ -528,7 +589,7 @@ Qed. (** Translation of condition operators *) -Lemma transl_cond_int32s_correct: +(* TODO REMOVE 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 @@ -830,9 +891,9 @@ Proof. + apply DFL. + apply DFL. + apply DFL. -Qed. + Qed. -(* TODO Lemma transl_cond_op_correct: +Lemma transl_cond_op_correct: forall cond rd args k c rs m, transl_cond_op cond rd args k = OK c -> exists rs', @@ -1134,7 +1195,7 @@ Opaque Int.eq. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } (* cond *) - (* TODO { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). + (* TODO REMOVE { 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; -- cgit