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/Op.v | 42 +++++++++++++++++++++++++++++++++++++++--- 1 file changed, 39 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/Op.v') 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: -- cgit