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