diff options
| -rw-r--r-- | common/Values.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/NeedOp.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 29 | ||||
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 16 | ||||
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 64 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 40 |
6 files changed, 149 insertions, 6 deletions
diff --git a/common/Values.v b/common/Values.v index 45774913..ecc1c458 100644 --- a/common/Values.v +++ b/common/Values.v @@ -802,7 +802,7 @@ Definition extfzl stop start v := let stop' := Z.add stop Z.one in match v with | Vlong w => - Vlong (Int64.shru (Int64.shl w (Int64.repr (Z.sub Int64.zwordsize stop'))) (Int64.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) + Vlong (Int64.shru' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) | _ => Vundef end else Vundef. @@ -816,7 +816,7 @@ Definition extfsl stop start v := let stop' := Z.add stop Z.one in match v with | Vlong w => - Vlong (Int64.shr (Int64.shl w (Int64.repr (Z.sub Int64.zwordsize stop'))) (Int64.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) + Vlong (Int64.shr' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) | _ => Vundef end else Vundef. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 3a27df6a..53c9c117 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -118,7 +118,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) | Ocmp c => needs_of_condition c | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => op3 (default nv) - | Oextfz _ _ | Oextfs _ _ => op1 (default nv) + | Oextfz _ _ | Oextfs _ _ | Oextfzl _ _ | Oextfsl _ _ => op1 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index f6433f90..99625f5c 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -199,7 +199,9 @@ Inductive operation : Type := | Oselectf (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) | Oselectfs (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) | Oextfz (stop : Z) (start : Z) - | Oextfs (stop : Z) (start : Z). + | Oextfs (stop : Z) (start : Z) + | Oextfzl (stop : Z) (start : Z) + | Oextfsl (stop : Z) (start : Z). (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -502,6 +504,8 @@ Definition eval_operation | (Oselectfs cond), v0::v1::vselect::nil => Some (eval_selectfs cond v0 v1 vselect m) | (Oextfz stop start), v0::nil => Some (Val.extfz stop start v0) | (Oextfs stop start), v0::nil => Some (Val.extfs stop start v0) + | (Oextfzl stop start), v0::nil => Some (Val.extfzl stop start v0) + | (Oextfsl stop start), v0::nil => Some (Val.extfsl stop start v0) | _, _ => None end. @@ -696,6 +700,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oselectf cond => (Tfloat :: Tfloat :: (arg_type_of_condition0 cond) :: nil, Tfloat) | Oselectfs cond => (Tsingle :: Tsingle :: (arg_type_of_condition0 cond) :: nil, Tsingle) | Oextfz _ _ | Oextfs _ _ => (Tint :: nil, Tint) + | Oextfzl _ _ | Oextfsl _ _ => (Tlong :: nil, Tlong) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -978,6 +983,16 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). destruct (_ && _ && _). + destruct v0; simpl; trivial. + constructor. + (* extfzl *) + - unfold Val.extfzl. + destruct (_ && _ && _). + + destruct v0; simpl; trivial. + + constructor. + (* extfsl *) + - unfold Val.extfsl. + destruct (_ && _ && _). + + destruct v0; simpl; trivial. + + constructor. Qed. End SOUNDNESS. @@ -1599,6 +1614,18 @@ Proof. destruct (_ && _ && _). + inv H4; trivial. + trivial. + + (* extfzl *) + - unfold Val.extfzl. + destruct (_ && _ && _). + + inv H4; trivial. + + trivial. + + (* extfsl *) + - unfold Val.extfsl. + destruct (_ && _ && _). + + inv H4; trivial. + + trivial. Qed. Lemma eval_addressing_inj: diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 811a8ab1..90901e04 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -155,6 +155,14 @@ Nondetfunction shrluimm (e1: expr) (n: int) := if Int.ltu (Int.add n n1) Int64.iwordsize' then Eop (Oshrluimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrluimm n) (e1:::Enil) + | Eop (Oshllimm n1) (t1:::Enil) => + let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in + let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in + if (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int64.zwordsize) + then Eop (Oextfzl stop start) (t1:::Enil) + else Eop (Oshrluimm n) (e1:::Enil) | _ => Eop (Oshrluimm n) (e1:::Enil) end. @@ -172,6 +180,14 @@ Nondetfunction shrlimm (e1: expr) (n: int) := if Int.ltu (Int.add n n1) Int64.iwordsize' then Eop (Oshrlimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrlimm n) (e1:::Enil) + | Eop (Oshllimm n1) (t1:::Enil) => + let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in + let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in + if (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int64.zwordsize) + then Eop (Oextfsl stop start) (t1:::Enil) + else Eop (Oshrlimm n) (e1:::Enil) | _ => Eop (Oshrlimm n) (e1:::Enil) end. diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 3fa35331..451bded7 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -238,7 +238,7 @@ Proof. exists x; split; auto. subst n; destruct x; simpl; auto. destruct (Int.ltu Int.zero Int64.iwordsize'); auto. change (Int64.shru' i Int.zero) with (Int64.shru i Int64.zero). rewrite Int64.shru_zero; auto. - destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. + destruct (Int.ltu n Int64.iwordsize') eqn:LT. assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop (Oshrluimm n) (a:::Enil)) v /\ Val.lessdef (Val.shrlu x (Vint n)) v) by TrivialExists. destruct (shrluimm_match a); InvEval. @@ -248,6 +248,36 @@ Proof. destruct v1; simpl; auto. rewrite LT'. destruct (Int.ltu n1 Int64.iwordsize') eqn:LT1; auto. simpl; rewrite LT. rewrite Int.add_commut, Int64.shru'_shru'; auto. rewrite Int.add_commut; auto. +- subst x. + simpl negb. + cbn iota. + destruct (_ && _ && _) eqn:BOUNDS. + + exists (Val.extfzl (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) + (Z.sub + (Z.add + (Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one))) + Z.one) Int64.zwordsize) v1). + split. + ++ EvalOp. + ++ unfold Val.extfzl. + rewrite BOUNDS. + destruct v1; try (simpl; apply Val.lessdef_undef). + replace (Z.sub Int64.zwordsize + (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega. + replace (Z.sub Int64.zwordsize + (Z.sub + (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one) + (Z.sub + (Z.add + (Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one))) + Z.one) Int64.zwordsize))) with (Int.unsigned n) by omega. + simpl. + destruct (Int.ltu n1 Int64.iwordsize') eqn:Hltu_n1; simpl; trivial. + destruct (Int.ltu n Int64.iwordsize') eqn:Hltu_n; simpl; trivial. + rewrite Int.repr_unsigned. + rewrite Int.repr_unsigned. + constructor. + + TrivialExists. constructor. econstructor. constructor. eassumption. constructor. simpl. reflexivity. constructor. simpl. reflexivity. - apply DEFAULT. - TrivialExists. constructor; eauto. constructor. EvalOp. simpl; eauto. constructor. auto. Qed. @@ -260,7 +290,7 @@ Proof. exists x; split; auto. subst n; destruct x; simpl; auto. destruct (Int.ltu Int.zero Int64.iwordsize'); auto. change (Int64.shr' i Int.zero) with (Int64.shr i Int64.zero). rewrite Int64.shr_zero; auto. - destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. + destruct (Int.ltu n Int64.iwordsize') eqn:LT. assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop (Oshrlimm n) (a:::Enil)) v /\ Val.lessdef (Val.shrl x (Vint n)) v) by TrivialExists. destruct (shrlimm_match a); InvEval. @@ -270,6 +300,36 @@ Proof. destruct v1; simpl; auto. rewrite LT'. destruct (Int.ltu n1 Int64.iwordsize') eqn:LT1; auto. simpl; rewrite LT. rewrite Int.add_commut, Int64.shr'_shr'; auto. rewrite Int.add_commut; auto. +- subst x. + simpl negb. + cbn iota. + destruct (_ && _ && _) eqn:BOUNDS. + + exists (Val.extfsl (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) + (Z.sub + (Z.add + (Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one))) + Z.one) Int64.zwordsize) v1). + split. + ++ EvalOp. + ++ unfold Val.extfsl. + rewrite BOUNDS. + destruct v1; try (simpl; apply Val.lessdef_undef). + replace (Z.sub Int64.zwordsize + (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega. + replace (Z.sub Int64.zwordsize + (Z.sub + (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one) + (Z.sub + (Z.add + (Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one))) + Z.one) Int64.zwordsize))) with (Int.unsigned n) by omega. + simpl. + destruct (Int.ltu n1 Int64.iwordsize') eqn:Hltu_n1; simpl; trivial. + destruct (Int.ltu n Int64.iwordsize') eqn:Hltu_n; simpl; trivial. + rewrite Int.repr_unsigned. + rewrite Int.repr_unsigned. + constructor. + + TrivialExists. constructor. econstructor. constructor. eassumption. constructor. simpl. reflexivity. constructor. simpl. reflexivity. - apply DEFAULT. - TrivialExists. constructor; eauto. constructor. EvalOp. simpl; eauto. constructor. auto. Qed. diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 23514d21..e9269213 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -101,6 +101,32 @@ Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) := end else Vtop. +Definition eval_static_extfsl (stop : Z) (start : Z) (v : aval) := + if (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int64.zwordsize) + then + let stop' := Z.add stop Z.one in + match v with + | L w => + L (Int64.shr' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) + | _ => Vtop + end + else Vtop. + +Definition eval_static_extfzl (stop : Z) (start : Z) (v : aval) := + if (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int64.zwordsize) + then + let stop' := Z.add stop Z.one in + match v with + | L w => + L (Int64.shru' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) + | _ => Vtop + end + else Vtop. + Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -231,6 +257,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | (Oselectfs cond), v0::v1::vselect::nil => eval_static_selectfs cond v0 v1 vselect | (Oextfz stop start), v0::nil => eval_static_extfz stop start v0 | (Oextfs stop start), v0::nil => eval_static_extfs stop start v0 + | (Oextfzl stop start), v0::nil => eval_static_extfzl stop start v0 + | (Oextfsl stop start), v0::nil => eval_static_extfsl stop start v0 | _, _ => Vbot end. @@ -368,6 +396,18 @@ Proof. destruct (_ && _ && _). + inv H1; constructor. + constructor. + + (* extfzl *) + - unfold Val.extfzl, eval_static_extfzl. + destruct (_ && _ && _). + + inv H1; constructor. + + constructor. + + (* extfsl *) + - unfold Val.extfsl, eval_static_extfsl. + destruct (_ && _ && _). + + inv H1; constructor. + + constructor. Qed. End SOUNDNESS. |