From bf1173b1609d04b8c99d1bdbcda4fffbb3745578 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 25 Mar 2019 12:58:26 +0100 Subject: more on cmove --- mppa_k1c/Asmblockgenproof1.v | 87 ++++++++++++-------------------------------- 1 file changed, 24 insertions(+), 63 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 5486a497..6239ed4a 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1558,6 +1558,16 @@ Ltac TranslOpSimpl := [ apply exec_straight_one; reflexivity | split; [ apply Val.lessdef_same; simpl; Simpl; fail | intros; simpl; Simpl; fail ] ]. +Lemma int_eq_comm: + forall (x y: int), + (Int.eq x y) = (Int.eq y x). +Proof. + intros. + unfold Int.eq. + unfold zeq. + destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence. +Qed. + Lemma transl_op_correct: forall op args res k (rs: regset) m v c, transl_op op args res k = OK c -> @@ -1645,69 +1655,20 @@ Opaque Int.eq. - (* Ocmp *) exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. -(* -- (* intconst *) - exploit loadimm32_correct; eauto. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* longconst *) - exploit loadimm64_correct; eauto. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* floatconst *) - destruct (Float.eq_dec n Float.zero). -+ subst n. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -+ econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -- (* singleconst *) - destruct (Float32.eq_dec n Float32.zero). -+ subst n. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -+ econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -- (* stackoffset *) - exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C). - exists rs'; split; eauto. auto with asmgen. -- (* addimm *) - exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* andimm *) - exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* orimm *) - exploit (opimm32_correct Porw Poriw Val.or); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* xorimm *) - exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. - - - -- (* addlimm *) - exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. - -- (* andimm *) - exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* orimm *) - exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* xorimm *) - exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -*) +- (* Oselect *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold select. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. Qed. (** Memory accesses *) -- cgit From e6a14b52554819995fed85c85a4acfedbb6ee3bc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 25 Mar 2019 13:23:43 +0100 Subject: selectl --- mppa_k1c/Asmblockgenproof1.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 6239ed4a..a1bd7124 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1669,6 +1669,20 @@ Opaque Int.eq. destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. +- (* Oselectl *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold select. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. Qed. (** Memory accesses *) -- cgit From 3750a2ad965b4959f6535aeeb9075dbd1a7c0527 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 26 Mar 2019 22:44:31 +0100 Subject: selectl generation --- mppa_k1c/Asmblockgenproof1.v | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index a1bd7124..16663522 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1568,6 +1568,16 @@ Proof. destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence. Qed. +Lemma int64_eq_comm: + forall (x y: int64), + (Int64.eq x y) = (Int64.eq y x). +Proof. + intros. + unfold Int64.eq. + unfold zeq. + destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence. +Qed. + Lemma transl_op_correct: forall op args res k (rs: regset) m v c, transl_op op args res k = OK c -> @@ -1674,13 +1684,13 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold select. + * unfold selectl. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. simpl. - rewrite int_eq_comm. - destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + rewrite int64_eq_comm. + destruct (Int64.eq i Int64.zero); simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. Qed. -- cgit From 4518486a771055e633aa050141d9721353d542d7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 21:59:22 +0200 Subject: ternary ops in AES and TEA --- mppa_k1c/Asmblockgenproof1.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index d90b73e2..99ab1b91 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1661,8 +1661,8 @@ Opaque Int.eq. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. simpl. - rewrite int64_eq_comm. - destruct (Int64.eq i Int64.zero); simpl; rewrite Pregmap.gss; constructor. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. Qed. -- cgit From ca34ea47f863c074a9d0ca890097786c5829267c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 22:36:22 +0200 Subject: ternary ops for float/double --- mppa_k1c/Asmblockgenproof1.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 99ab1b91..f75f0bd3 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1665,6 +1665,34 @@ Opaque Int.eq. destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. +- (* Oselectf *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold selectl. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. +- (* Oselectfs *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold selectl. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. Qed. (** Memory accesses *) -- cgit From 70db0c8a5cd5fb21e92de32cc4eb5774baf60610 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 4 Apr 2019 06:07:00 +0200 Subject: prepare for conditions in cmove --- mppa_k1c/Asmblockgenproof1.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index f75f0bd3..698d64d6 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1642,7 +1642,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold select. + * unfold eval_select. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. @@ -1656,7 +1656,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold selectl. + * unfold eval_selectl. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. @@ -1670,7 +1670,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold selectl. + * unfold eval_selectf. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. @@ -1684,7 +1684,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold selectl. + * unfold eval_selectfs. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. -- cgit From 71c38724bee43fe1a2ce67ee51f09478cd167929 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 4 Apr 2019 21:31:36 +0200 Subject: Oselect --- mppa_k1c/Asmblockgenproof1.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 698d64d6..e8e04019 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1638,17 +1638,18 @@ Opaque Int.eq. exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. - (* Oselect *) + destruct cond in *; simpl in *; try congruence; injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in *. econstructor; split. + + eapply exec_straight_one. simpl; reflexivity. + split. * unfold eval_select. - destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. - simpl. - rewrite int_eq_comm. - destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + destruct c0 in *; simpl; + destruct (Val.cmp_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. - (* Oselectl *) -- cgit From a4f081bd7972c9007104942bdf90a4042397e167 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 4 Apr 2019 23:54:54 +0200 Subject: some more Oselect comparisons --- mppa_k1c/Asmblockgenproof1.v | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index e8e04019..e58c7f0c 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1638,7 +1638,7 @@ Opaque Int.eq. exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. - (* Oselect *) - destruct cond in *; simpl in *; try congruence; injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in *. + destruct cond in *; simpl in *; try congruence; injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in *; econstructor; split. + eapply exec_straight_one. @@ -1652,6 +1652,17 @@ Opaque Int.eq. destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmpl_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. - (* Oselectl *) econstructor; split. + eapply exec_straight_one. -- cgit From b27d386185527d1ee9d0bb77ebe3bacffc2bf05a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 5 Apr 2019 00:12:45 +0200 Subject: factor out some proofs --- mppa_k1c/Asmblockgenproof1.v | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index e58c7f0c..7da86de4 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1639,10 +1639,9 @@ Opaque Int.eq. exists rs'; split. eexact A. eauto with asmgen. - (* Oselect *) destruct cond in *; simpl in *; try congruence; injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in *; - econstructor; split. - - + eapply exec_straight_one. - simpl; reflexivity. + econstructor; split; + try ( eapply exec_straight_one; + simpl; reflexivity ). + split. * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. @@ -1652,8 +1651,6 @@ Opaque Int.eq. destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. - + eapply exec_straight_one. - simpl; reflexivity. + split. * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. -- cgit From 53b6eb437c7988b44e881c7b7a9df2e735ded0ea Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 5 Apr 2019 06:03:21 +0200 Subject: select cmpu --- mppa_k1c/Asmblockgenproof1.v | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 7da86de4..75f2005c 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1638,10 +1638,12 @@ Opaque Int.eq. exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. - (* Oselect *) - destruct cond in *; simpl in *; try congruence; injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in *; + destruct cond in *; simpl in *; try congruence; + try monadInv EQ3; + try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew); econstructor; split; - try ( eapply exec_straight_one; - simpl; reflexivity ). + try ( eapply exec_straight_one; simpl; reflexivity ). + (* Cmp *) + split. * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. @@ -1651,6 +1653,24 @@ Opaque Int.eq. destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. + (* Cmpu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmpl *) + split. * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. -- cgit From 483d0e37880dbe44af3dafdcac9b1110a37139c4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 5 Apr 2019 06:15:28 +0200 Subject: Select cmplu --- mppa_k1c/Asmblockgenproof1.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 75f2005c..1cb75c4c 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1680,6 +1680,24 @@ Opaque Int.eq. destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. + + (* Cmplu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + - (* Oselectl *) econstructor; split. + eapply exec_straight_one. -- cgit From 57925286e8ba6055534cd0acbcf2b411366d3e0b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 5 Apr 2019 09:40:45 +0200 Subject: selectl with condition --- mppa_k1c/Asmblockgenproof1.v | 65 ++++++++++++++++++++++++++++++++++++++------ 1 file changed, 56 insertions(+), 9 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 1cb75c4c..874e40a8 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1698,20 +1698,67 @@ Opaque Int.eq. * intros. rewrite Pregmap.gso; congruence. -- (* Oselectl *) - econstructor; split. - + eapply exec_straight_one. - simpl; reflexivity. +- (* Oselect *) + destruct cond in *; simpl in *; try congruence; + try monadInv EQ3; + try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew); + econstructor; split; + try ( eapply exec_straight_one; simpl; reflexivity ). + (* Cmp *) + split. - * unfold eval_selectl. - destruct (rs x1) eqn:eqX1; try constructor. + * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. - simpl. - rewrite int_eq_comm. - destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + destruct c0 in *; simpl; + destruct (Val.cmp_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. + (* Cmpu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmpl *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmpl_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmplu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + - (* Oselectf *) econstructor; split. + eapply exec_straight_one. -- cgit From e4bc9aa604977ee168c2f580d3fc3c3521f6c25c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 5 Apr 2019 13:36:56 +0200 Subject: Oselectf, Oselectfs with condition --- mppa_k1c/Asmblockgenproof1.v | 128 +++++++++++++++++++++++++++++++++++++------ 1 file changed, 111 insertions(+), 17 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 874e40a8..6cf5c60c 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1698,7 +1698,7 @@ Opaque Int.eq. * intros. rewrite Pregmap.gso; congruence. -- (* Oselect *) +- (* Oselectl *) destruct cond in *; simpl in *; try congruence; try monadInv EQ3; try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew); @@ -1760,31 +1760,125 @@ Opaque Int.eq. rewrite Pregmap.gso; congruence. - (* Oselectf *) - econstructor; split. - + eapply exec_straight_one. - simpl; reflexivity. + destruct cond in *; simpl in *; try congruence; + try monadInv EQ3; + try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew); + econstructor; split; + try ( eapply exec_straight_one; simpl; reflexivity ). + (* Cmp *) + split. - * unfold eval_selectf. - destruct (rs x1) eqn:eqX1; try constructor. + * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. - simpl. - rewrite int_eq_comm. - destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + destruct c0 in *; simpl; + destruct (Val.cmp_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. + (* Cmpu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmpl *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmpl_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmplu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + - (* Oselectfs *) - econstructor; split. - + eapply exec_straight_one. - simpl; reflexivity. + destruct cond in *; simpl in *; try congruence; + try monadInv EQ3; + try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew); + econstructor; split; + try ( eapply exec_straight_one; simpl; reflexivity ). + (* Cmp *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmp_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + (* Cmpu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmpl *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmpl_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmplu *) + split. - * unfold eval_selectfs. - destruct (rs x1) eqn:eqX1; try constructor. + * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. - simpl. - rewrite int_eq_comm. - destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. Qed. -- cgit