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/Asmblockgen.v | 12 +--- mppa_k1c/Asmblockgenproof1.v | 128 ++++++++++++++++++++++++++++++++------ mppa_k1c/Machregs.v | 2 +- mppa_k1c/NeedOp.v | 98 +++++++++++++++++++++-------- mppa_k1c/Op.v | 142 +++++++++++++++++++++++++++++-------------- mppa_k1c/SelectOp.vp | 14 +++++ mppa_k1c/ValueAOp.v | 50 +++++++-------- 7 files changed, 323 insertions(+), 123 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index b3478a9a..392b7953 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -752,7 +752,9 @@ Definition transl_op transl_cond_op cmp rd args k | Oselect cond, a0 :: a1 :: aS :: nil - | Oselectl cond, a0 :: a1 :: aS :: nil => + | Oselectl cond, a0 :: a1 :: aS :: nil + | Oselectf cond, a0 :: a1 :: aS :: nil + | Oselectfs cond, a0 :: a1 :: aS :: nil => assertion (mreg_eq a0 res); do r0 <- ireg_of a0; do r1 <- ireg_of a1; @@ -769,14 +771,6 @@ Definition transl_op do bt <- btest_for_cmpudz cmp; OK (Pcmoveu bt r0 rS r1 ::i k) end) - - | Oselectf, a0 :: a1 :: aS :: nil - | Oselectfs, a0 :: a1 :: aS :: nil => - assertion (mreg_eq a0 res); - do r0 <- ireg_of a0; - do r1 <- ireg_of a1; - do rS <- ireg_of aS; - OK (Pcmove BTwnez r0 rS r1 ::i k) | _, _ => Error(msg "Asmgenblock.transl_op") 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. diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index ddf730a9..f36962f3 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -209,7 +209,7 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl _ | Oselectf | Oselectfs => true + | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => true | _ => false end. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index a276cda1..ba051c90 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -117,7 +117,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) | Ocmp c => needs_of_condition c - | Oselect _ | Oselectl _ | Oselectf | Oselectfs => op3 (default nv) + | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => op3 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := @@ -332,41 +332,89 @@ Proof. Qed. Lemma selectf_sound: - forall v0 w0 v1 w1 v2 w2 x, + forall cond v0 w0 v1 w1 v2 w2 x, vagree v0 w0 (default x) -> vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> - vagree (eval_selectf v0 v1 v2) (eval_selectf w0 w1 w2) x. + vagree (eval_selectf cond v0 v1 v2 m1) (eval_selectf cond w0 w1 w2 m2) x. Proof. - unfold default; intros. - destruct x; trivial. - - destruct v2; simpl; trivial. - destruct v0; simpl; trivial. - destruct v1; simpl; trivial. - - destruct v2; simpl; trivial. - destruct v0; simpl; trivial. - destruct v1; simpl; trivial. - inv H. inv H0. inv H1. simpl. - constructor. + intros. + destruct x; simpl in *; trivial. + - rewrite eval_selectf_to2. + rewrite eval_selectf_to2. + unfold eval_selectf2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + - rewrite eval_selectf_to2. + rewrite eval_selectf_to2. + unfold eval_selectf2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. Qed. Lemma selectfs_sound: - forall v0 w0 v1 w1 v2 w2 x, + forall cond v0 w0 v1 w1 v2 w2 x, vagree v0 w0 (default x) -> vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> - vagree (eval_selectfs v0 v1 v2) (eval_selectfs w0 w1 w2) x. + vagree (eval_selectfs cond v0 v1 v2 m1) (eval_selectfs cond w0 w1 w2 m2) x. Proof. - unfold default; intros. - destruct x; trivial. - - destruct v2; simpl; trivial. - destruct v0; simpl; trivial. - destruct v1; simpl; trivial. - - destruct v2; simpl; trivial. - destruct v0; simpl; trivial. - destruct v1; simpl; trivial. - inv H. inv H0. inv H1. simpl. - constructor. + intros. + destruct x; simpl in *; trivial. + - rewrite eval_selectfs_to2. + rewrite eval_selectfs_to2. + unfold eval_selectfs2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + - rewrite eval_selectfs_to2. + rewrite eval_selectfs_to2. + unfold eval_selectfs2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. Qed. Remark default_idem: forall nv, default (default nv) = default nv. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 045946fd..14758bee 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -194,10 +194,10 @@ Inductive operation : Type := | Osingleoflongu (**r [rd = float32_of_unsigned_int(r1)] *) (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) - | Oselect (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) - | Oselectl (cond: condition0)(**r [rd = if cond r3 then r2 else r1] *) - | Oselectf (**r [rd = if r3 then r2 else r1] *) - | Oselectfs. (**r [rd = if r3 then r2 else r1] *) + | Oselect (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) + | Oselectl (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) + | Oselectf (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) + | Oselectfs (cond: condition0). (**r [rd = if cond r3 then r2 else r1] *) (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -324,40 +324,48 @@ Proof. destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity. Qed. -Definition eval_selectf (v0 : val) (v1 : val) (vselect : val) : val := - match vselect with - | Vint iselect => - match v0 with - | Vfloat i0 => - match v1 with - | Vfloat i1 => - Vfloat (if Int.cmp Ceq Int.zero iselect - then i0 - else i1) - | _ => Vundef - end - | _ => Vundef - end - | _ => Vundef +Definition eval_selectf (cond: condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := + match v0, v1, (eval_condition0 cond vselect m) with + | Vfloat i0, Vfloat i1, Some bval => Vfloat (if bval then i1 else i0) + | _,_,_ => Vundef + end. + +Definition eval_selectf2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := + match (eval_condition0 cond vselect m), v0, v1 with + | Some bval, Vfloat i0, Vfloat i1 => Vfloat (if bval then i1 else i0) + | _,_,_ => Vundef + end. + +Lemma eval_selectf_to2: forall cond v0 v1 vselect m, + (eval_selectf cond v0 v1 vselect m) = + (eval_selectf2 cond v0 v1 vselect m). +Proof. + intros. + unfold eval_selectf2. + destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity. +Qed. + +Definition eval_selectfs (cond: condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := + match v0, v1, (eval_condition0 cond vselect m) with + | Vsingle i0, Vsingle i1, Some bval => Vsingle (if bval then i1 else i0) + | _,_,_ => Vundef end. -Definition eval_selectfs (v0 : val) (v1 : val) (vselect : val) : val := - match vselect with - | Vint iselect => - match v0 with - | Vsingle i0 => - match v1 with - | Vsingle i1 => - Vsingle (if Int.cmp Ceq Int.zero iselect - then i0 - else i1) - | _ => Vundef - end - | _ => Vundef - end - | _ => Vundef +Definition eval_selectfs2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := + match (eval_condition0 cond vselect m), v0, v1 with + | Some bval, Vsingle i0, Vsingle i1 => Vsingle (if bval then i1 else i0) + | _,_,_ => Vundef end. +Lemma eval_selectfs_to2: forall cond v0 v1 vselect m, + (eval_selectfs cond v0 v1 vselect m) = + (eval_selectfs2 cond v0 v1 vselect m). +Proof. + intros. + unfold eval_selectfs2. + destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity. +Qed. + Definition eval_operation (F V: Type) (genv: Genv.t F V) (sp: val) (op: operation) (vl: list val) (m: mem): option val := @@ -488,8 +496,8 @@ Definition eval_operation | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) | (Oselect cond), v0::v1::vselect::nil => Some (eval_select cond v0 v1 vselect m) | (Oselectl cond), v0::v1::vselect::nil => Some (eval_selectl cond v0 v1 vselect m) - | Oselectf, v0::v1::vselect::nil => Some (eval_selectf v0 v1 vselect) - | Oselectfs, v0::v1::vselect::nil => Some (eval_selectfs v0 v1 vselect) + | (Oselectf cond), v0::v1::vselect::nil => Some (eval_selectf cond v0 v1 vselect m) + | (Oselectfs cond), v0::v1::vselect::nil => Some (eval_selectfs cond v0 v1 vselect m) | _, _ => None end. @@ -681,8 +689,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oselect cond => (Tint :: Tint :: (arg_type_of_condition0 cond) :: nil, Tint) | Oselectl cond => (Tlong :: Tlong :: (arg_type_of_condition0 cond) :: nil, Tlong) - | Oselectf => (Tfloat :: Tfloat :: Tint :: nil, Tfloat) - | Oselectfs => (Tsingle :: Tsingle :: Tint :: nil, Tsingle) + | Oselectf cond => (Tfloat :: Tfloat :: (arg_type_of_condition0 cond) :: nil, Tfloat) + | Oselectfs cond => (Tsingle :: Tsingle :: (arg_type_of_condition0 cond) :: nil, Tsingle) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -938,9 +946,23 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). destruct (Val.cmp_different_blocks _); simpl; trivial. (* selectf *) - - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial. + - destruct v0; destruct v1; simpl in *; try discriminate; trivial. + destruct cond; destruct v2; simpl in *; trivial. + + destruct Archi.ptr64; simpl; trivial. + destruct (_ && _); simpl; trivial. + destruct (Val.cmp_different_blocks _); simpl; trivial. + + destruct Archi.ptr64; simpl; trivial. + destruct (_ && _); simpl; trivial. + destruct (Val.cmp_different_blocks _); simpl; trivial. (* selectfs *) - - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial. + - destruct v0; destruct v1; simpl in *; try discriminate; trivial. + destruct cond; destruct v2; simpl in *; trivial. + + destruct Archi.ptr64; simpl; trivial. + destruct (_ && _); simpl; trivial. + destruct (Val.cmp_different_blocks _); simpl; trivial. + + destruct Archi.ptr64; simpl; trivial. + destruct (_ && _); simpl; trivial. + destruct (Val.cmp_different_blocks _); simpl; trivial. Qed. End SOUNDNESS. @@ -1107,6 +1129,12 @@ Definition op_depends_on_memory (op: operation) : bool := | Oselectl (Ccompu0 _) => negb Archi.ptr64 | Oselectl (Ccomplu0 _) => Archi.ptr64 + + | Oselectf (Ccompu0 _) => negb Archi.ptr64 + | Oselectf (Ccomplu0 _) => Archi.ptr64 + + | Oselectfs (Ccompu0 _) => negb Archi.ptr64 + | Oselectfs (Ccomplu0 _) => Archi.ptr64 | _ => false end. @@ -1119,7 +1147,7 @@ Proof. intros until m2. destruct op; simpl; try congruence; destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF; - unfold eval_select, eval_selectl, eval_condition0, Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. + unfold eval_select, eval_selectl, eval_selectf, eval_selectfs, eval_condition0, Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. Qed. (** Global variables mentioned in an operation or addressing mode *) @@ -1517,13 +1545,33 @@ Proof. assumption. * rewrite Hcond'. constructor. (* selectf *) - - inv H3; simpl; try constructor. - inv H4; simpl; try constructor. - inv H2; simpl; constructor. + - unfold eval_selectf. + inv H4; trivial. + inv H2; trivial. + inv H3; trivial; + try (destruct cond; simpl; trivial; fail). + destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial. + eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b). + * eapply eval_condition0_inj. + eapply Val.inject_ptr. + eassumption. + reflexivity. + assumption. + * rewrite Hcond'. constructor. (* selectfs *) - - inv H3; simpl; try constructor. - inv H4; simpl; try constructor. - inv H2; simpl; constructor. + - unfold eval_selectfs. + inv H4; trivial. + inv H2; trivial. + inv H3; trivial; + try (destruct cond; simpl; trivial; fail). + destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial. + eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b). + * eapply eval_condition0_inj. + eapply Val.inject_ptr. + eassumption. + reflexivity. + assumption. + * rewrite Hcond'. constructor. Qed. Lemma eval_addressing_inj: diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index eeb3ffae..71e0eff3 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -76,6 +76,20 @@ Definition selectl_base o0 o1 oselect := Definition selectl o0 o1 oselect := selectl_base o0 o1 oselect. +Definition selectf_base o0 o1 oselect := + Eop (Oselectf (Ccomp0 Cne)) + (o0:::o1:::oselect:::Enil). + +Definition selectf o0 o1 oselect := + selectf_base o0 o1 oselect. + +Definition selectfs_base o0 o1 oselect := + Eop (Oselectfs (Ccomp0 Cne)) + (o0:::o1:::oselect:::Enil). + +Definition selectfs o0 o1 oselect := + selectfs_base o0 o1 oselect. + (** ** Constants **) Definition addrsymbol (id: ident) (ofs: ptrofs) := diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 62cfa85e..f17bd765 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -62,21 +62,15 @@ Definition eval_static_selectl (cond : condition0) (v0 v1 vselect : aval) : aval | _ => Vtop end. -Definition eval_static_selectf (v0 v1 vselect : aval) : aval := - match vselect with - | I iselect => - if Int.eq Int.zero iselect - then binop_float (fun x0 x1 => x0) v0 v1 - else binop_float (fun x0 x1 => x1) v0 v1 +Definition eval_static_selectf (cond : condition0) (v0 v1 vselect : aval) : aval := + match eval_static_condition0 cond vselect with + | Just b => binop_float (fun x0 x1 => if b then x1 else x0) v0 v1 | _ => Vtop end. -Definition eval_static_selectfs (v0 v1 vselect : aval) : aval := - match vselect with - | I iselect => - if Int.eq Int.zero iselect - then binop_single (fun x0 x1 => x0) v0 v1 - else binop_single (fun x0 x1 => x1) v0 v1 +Definition eval_static_selectfs (cond : condition0) (v0 v1 vselect : aval) : aval := + match eval_static_condition0 cond vselect with + | Just b => binop_single (fun x0 x1 => if b then x1 else x0) v0 v1 | _ => Vtop end. @@ -206,8 +200,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ocmp c, _ => of_optbool (eval_static_condition c vl) | (Oselect cond), v0::v1::vselect::nil => eval_static_select cond v0 v1 vselect | (Oselectl cond), v0::v1::vselect::nil => eval_static_selectl cond v0 v1 vselect - | Oselectf, v0::v1::vselect::nil => eval_static_selectf v0 v1 vselect - | Oselectfs, v0::v1::vselect::nil => eval_static_selectfs v0 v1 vselect + | (Oselectf cond), v0::v1::vselect::nil => eval_static_selectf cond v0 v1 vselect + | (Oselectfs cond), v0::v1::vselect::nil => eval_static_selectfs cond v0 v1 vselect | _, _ => Vbot end. @@ -314,17 +308,25 @@ Proof. + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef. apply vmatch_ifptr_l. (* selectf *) - - inv H2; simpl; try constructor. - + destruct (Int.eq _ _); apply binop_float_sound; trivial. - + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption). + rewrite eval_selectf_to2. + unfold eval_selectf2. + inv Hcond; trivial; try constructor. + + apply binop_float_sound; assumption. + + destruct a1; destruct a0; try apply vmatch_ifptr_undef. + constructor. + + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef. + constructor. (* selectfs *) - - inv H2; simpl; try constructor. - + destruct (Int.eq _ _); apply binop_single_sound; trivial. - + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption). + rewrite eval_selectfs_to2. + unfold eval_selectfs2. + inv Hcond; trivial; try constructor. + + apply binop_single_sound; assumption. + + destruct a1; destruct a0; try apply vmatch_ifptr_undef. + constructor. + + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef. + constructor. Qed. End SOUNDNESS. -- cgit