diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 07:43:38 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 07:43:38 +0200 |
commit | 4e17c25f7d6d3c5d7fb13dc0d0c3dacf3fb2830b (patch) | |
tree | f2d11986cdd646baa4da20d7366ba2bb70fb85cc | |
parent | 70db0c8a5cd5fb21e92de32cc4eb5774baf60610 (diff) | |
download | compcert-kvx-4e17c25f7d6d3c5d7fb13dc0d0c3dacf3fb2830b.tar.gz compcert-kvx-4e17c25f7d6d3c5d7fb13dc0d0c3dacf3fb2830b.zip |
working on select
-rw-r--r-- | mppa_k1c/Op.v | 86 |
1 files changed, 58 insertions, 28 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 551d2dfb..15e3eda4 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -57,6 +57,12 @@ Inductive condition0 : Type := | Ccompl0 (c: comparison) (**r signed 64-bit integer comparison with 0 *) | Ccomplu0 (c: comparison). (**r unsigned 64-bit integer comparison with 0 *) +Definition arg_type_of_condition0 (cond: condition0) := + match cond with + | Ccomp0 _ | Ccompu0 _ => Tint + | Ccompl0 _ | Ccomplu0 _ => Tlong + end. + (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -188,7 +194,7 @@ 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 (**r [rd = if r3 then r2 else r1] *) + | Oselect (cond: condition0) (**r [rd = if r3 then r2 else r1] *) | Oselectl (**r [rd = if r3 then r2 else r1] *) | Oselectf (**r [rd = if r3 then r2 else r1] *) | Oselectfs. (**r [rd = if r3 then r2 else r1] *) @@ -211,6 +217,13 @@ Proof. decide equality. Defined. +Definition eq_condition0 (x y: condition0) : {x=y} + {x<>y}. +Proof. + generalize Int.eq_dec Int64.eq_dec; intro. + assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. + decide equality. +Defined. + Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. generalize ident_eq Ptrofs.eq_dec; intros. @@ -219,7 +232,7 @@ Defined. Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0; intros. decide equality. Defined. @@ -261,26 +274,23 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | _, _ => None end. -Definition eval_condition0 (cond: condition0) (vl: list val) (m: mem): option bool := - match cond, vl with - | Ccomp0 c, v1 :: nil => Val.cmp_bool c v1 (Vint Int.zero) - | Ccompu0 c, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint Int.zero) - | Ccompl0 c, v1 :: nil => Val.cmpl_bool c v1 (Vlong Int64.zero) - | Ccomplu0 c, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong Int64.zero) - | _, _ => None +Definition eval_condition0 (cond: condition0) (v1: val) (m: mem): option bool := + match cond with + | Ccomp0 c => Val.cmp_bool c v1 (Vint Int.zero) + | Ccompu0 c => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint Int.zero) + | Ccompl0 c => Val.cmpl_bool c v1 (Vlong Int64.zero) + | Ccomplu0 c => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong Int64.zero) end. -Definition eval_select (v0 : val) (v1 : val) (vselect : val) : val := - match vselect with - | Vint iselect => - match v0 with - | Vint i0 => - match v1 with - | Vint i1 => - Vint (if Int.cmp Ceq Int.zero iselect - then i0 - else i1) - | _ => Vundef +Definition eval_select (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := + match v0 with + | Vint i0 => + match v1 with + | Vint i1 => + match (eval_condition0 cond vselect m) with + | Some bval => + Vint (if bval then i1 else i0) + | None => Vundef end | _ => Vundef end @@ -466,7 +476,7 @@ Definition eval_operation | Osingleoflong, v1::nil => Val.singleoflong v1 | Osingleoflongu, v1::nil => Val.singleoflongu v1 | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) - | Oselect, v0::v1::vselect::nil => Some (eval_select v0 v1 vselect) + | (Oselect cond), v0::v1::vselect::nil => Some (eval_select cond v0 v1 vselect m) | Oselectl, v0::v1::vselect::nil => Some (eval_selectl v0 v1 vselect) | Oselectf, v0::v1::vselect::nil => Some (eval_selectf v0 v1 vselect) | Oselectfs, v0::v1::vselect::nil => Some (eval_selectfs v0 v1 vselect) @@ -659,7 +669,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoflongu => (Tlong :: nil, Tsingle) | Ocmp c => (type_of_condition c, Tint) - | Oselect => (Tint :: Tint :: Tint :: nil, Tint) + | Oselect cond => (Tint :: Tint :: (arg_type_of_condition0 cond) :: nil, Tint) | Oselectl => (Tlong :: Tlong :: Tint :: nil, Tlong) | Oselectf => (Tfloat :: Tfloat :: Tint :: nil, Tfloat) | Oselectfs => (Tsingle :: Tsingle :: Tint :: nil, Tsingle) @@ -899,7 +909,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* cmp *) - destruct (eval_condition cond vl m)... destruct b... (* select *) - - 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. (* selectl *) - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial. (* selectf *) @@ -1066,6 +1083,10 @@ Definition op_depends_on_memory (op: operation) : bool := | Ocmp (Ccompuimm _ _) => negb Archi.ptr64 | Ocmp (Ccomplu _) => Archi.ptr64 | Ocmp (Ccompluimm _ _) => Archi.ptr64 + + | Oselect (Ccompu0 _) => negb Archi.ptr64 + | Oselect (Ccomplu0 _) => Archi.ptr64 + | _ => false end. @@ -1074,9 +1095,10 @@ Lemma op_depends_on_memory_correct: op_depends_on_memory op = false -> eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. - intros until m2. destruct op; simpl; try congruence. + intros until m2. destruct op; simpl; try congruence; + destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF; - unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. + unfold eval_select, eval_condition0, Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. Qed. (** Global variables mentioned in an operation or addressing mode *) @@ -1204,6 +1226,14 @@ Proof. - inv H3; inv H2; simpl in H0; inv H0; auto. Qed. +Lemma eval_condition0_inj: + forall cond v1 v2 b, + Val.inject f v1 v2 -> + eval_condition0 cond v1 m1 = Some b -> + eval_condition0 cond v2 m2 = Some b. +Proof. + intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. + Ltac TrivialExists := match goal with | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] => @@ -1433,9 +1463,9 @@ Proof. destruct b; simpl; constructor. simpl; constructor. (* select *) - - inv H3; simpl; try constructor. - inv H4; simpl; try constructor. - inv H2; simpl; constructor. + - inv H4; simpl; try constructor. + inv H2; simpl; try constructor. + inv H3; simpl; try constructor. (* selectl *) - inv H3; simpl; try constructor. inv H4; simpl; try constructor. |