From 6064bac57701ba0a12031d43acbe25cb0140730c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 4 Jun 2019 21:42:30 +0200 Subject: begin osel imm --- mppa_k1c/NeedOp.v | 12 ++++++++++++ mppa_k1c/Op.v | 42 +++++++++++++++++++++++++++++++++++++++--- mppa_k1c/ValueAOp.v | 6 ++++++ 3 files changed, 57 insertions(+), 3 deletions(-) diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 047c180a..4748f38b 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -133,6 +133,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oextfz _ _ | Oextfs _ _ | Oextfzl _ _ | Oextfsl _ _ => op1 (default nv) | Oinsf _ _ | Oinsfl _ _ => op2 (default nv) | Osel c ty => nv :: nv :: needs_of_condition0 c + | Oselimm c imm + | Osellimm c imm => nv :: needs_of_condition0 c end. Definition operation_is_redundant (op: operation) (nv: nval): bool := @@ -347,6 +349,16 @@ Proof. erewrite needs_of_condition0_sound by eauto. apply select_sound; auto. simpl; auto with na. + (* select imm *) +- destruct (eval_condition0 _ _ _) as [b|] eqn:EC. + { erewrite needs_of_condition0_sound by eauto. + apply select_sound; auto with na. } + simpl; auto with na. + (* select long imm *) +- destruct (eval_condition0 _ _ _) as [b|] eqn:EC. + { erewrite needs_of_condition0_sound by eauto. + apply select_sound; auto with na. } + simpl; auto with na. Qed. Lemma operation_is_redundant_sound: diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index be7ea812..1b3a839f 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -210,7 +210,9 @@ Inductive operation : Type := | Oextfsl (stop : Z) (start : Z) | Oinsf (stop : Z) (start : Z) | Oinsfl (stop : Z) (start : Z) - | Osel (c0 : condition0) (ty : typ). + | Osel (c0 : condition0) (ty : typ) + | Oselimm (c0 : condition0) (imm: int) + | Osellimm (c0 : condition0) (imm: int64). (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -454,6 +456,8 @@ Definition eval_operation | (Oinsf stop start), v0::v1::nil => Some (insf stop start v0 v1) | (Oinsfl stop start), v0::v1::nil => Some (insfl stop start v0 v1) | Osel c ty, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 v2 ty) + | Oselimm c imm, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vint imm) Tint) + | Osellimm c imm, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vlong imm) Tlong) | _, _ => None end. @@ -658,6 +662,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oinsf _ _ => (Tint :: Tint :: nil, Tint) | Oinsfl _ _ => (Tlong :: Tlong :: nil, Tlong) | Osel c ty => (ty :: ty :: arg_type_of_condition0 c :: nil, ty) + | Oselimm c ty => (Tint :: Tint :: arg_type_of_condition0 c :: nil, Tint) + | Osellimm c ty => (Tlong :: Tlong :: arg_type_of_condition0 c :: nil, Tlong) end. (* FIXME: two Tptr ?! *) @@ -971,6 +977,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - unfold Val.select. destruct (eval_condition0 _ _ m). + apply Val.normalize_type. + constructor. + (* Oselimm *) + - unfold Val.select. destruct (eval_condition0 _ _ m). + + apply Val.normalize_type. + + constructor. + (* Osellimm *) + - unfold Val.select. destruct (eval_condition0 _ _ m). + + apply Val.normalize_type. + + constructor. Qed. End SOUNDNESS. @@ -1132,8 +1146,8 @@ Definition op_depends_on_memory (op: operation) : bool := | Ocmp (Ccomplu _) => Archi.ptr64 | Ocmp (Ccompluimm _ _) => Archi.ptr64 - | Osel (Ccompu0 _) _ => negb Archi.ptr64 - | Osel (Ccomplu0 _) _ => Archi.ptr64 + | Osel (Ccompu0 _) _ | Oselimm (Ccompu0 _) _ | Osellimm (Ccompu0 _) _ => negb Archi.ptr64 + | Osel (Ccomplu0 _) _ | Oselimm (Ccomplu0 _) _ | Osellimm (Ccomplu0 _) _ => Archi.ptr64 | _ => false end. @@ -1150,6 +1164,12 @@ Proof. - destruct c0; simpl; try congruence; intros SF; auto; rewrite ? negb_false_iff in SF; unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. + - destruct c0; simpl; try congruence; + intros SF; auto; rewrite ? negb_false_iff in SF; + unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. + - destruct c0; simpl; try congruence; + intros SF; auto; rewrite ? negb_false_iff in SF; + unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. Qed. (** Global variables mentioned in an operation or addressing mode *) @@ -1591,6 +1611,22 @@ Proof. symmetry. eapply eval_condition0_inj; eassumption. + left. trivial. + + (* Oselimm *) + - apply Val.select_inject; trivial. + destruct (eval_condition0 c0 v2 m1) eqn:Hcond. + + right. + symmetry. + eapply eval_condition0_inj; eassumption. + + left. trivial. + + (* Osellimm *) + - apply Val.select_inject; trivial. + destruct (eval_condition0 c0 v2 m1) eqn:Hcond. + + right. + symmetry. + eapply eval_condition0_inj; eassumption. + + left. trivial. Qed. Lemma eval_addressing_inj: diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index d24cebcc..daceab8b 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -265,6 +265,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | (Oinsf stop start), v0::v1::nil => eval_static_insf stop start v0 v1 | (Oinsfl stop start), v0::v1::nil => eval_static_insfl stop start v0 v1 | Osel c ty, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 v2 + | Oselimm c imm, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 (I imm) + | Osellimm c imm, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 (L imm) | _, _ => Vbot end. @@ -421,6 +423,10 @@ Proof. + constructor. (* select *) - apply select_sound; auto. eapply eval_static_condition0_sound; eauto. + (* select imm *) + - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto. + (* select long imm *) + - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto. Qed. End SOUNDNESS. -- cgit