diff options
| -rw-r--r-- | mppa_k1c/NeedOp.v | 40 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 27 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 2 |
3 files changed, 52 insertions, 17 deletions
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 68f43894..2577370c 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -105,6 +105,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshrlimm n => op1 (default nv) | Oshrluimm n => op1 (default nv) | Oshrxlimm n => op1 (default nv) + | Omaddl => op3 (default nv) + | Omaddlimm n => op2 (default nv) | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) | Onegfs | Oabsfs => op1 (default nv) @@ -156,6 +158,39 @@ Proof. eapply default_needs_of_condition_sound; eauto. Qed. +Lemma addl_sound: + forall v1 w1 v2 w2 x, + vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> + vagree (Val.addl v1 v2) (Val.addl w1 w2) x. +Proof. + unfold default; intros. + destruct x; simpl in *; trivial. + - unfold Val.addl. + destruct v1; destruct v2; trivial; destruct Archi.ptr64; trivial. + - apply Val.addl_lessdef; trivial. +Qed. + + +Lemma mull_sound: + forall v1 w1 v2 w2 x, + vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> + vagree (Val.mull v1 v2) (Val.mull w1 w2) x. +Proof. + unfold default; intros. + destruct x; simpl in *; trivial. + - unfold Val.mull. + destruct v1; destruct v2; trivial. + - unfold Val.mull. + destruct v1; destruct v2; trivial. + inv H. inv H0. + trivial. +Qed. + +Remark default_idem: forall nv, default (default nv) = default nv. +Proof. + destruct nv; simpl; trivial. +Qed. + Lemma needs_of_operation_sound: forall op args v nv args', eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v -> @@ -198,6 +233,11 @@ Proof. (* madd *) - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. + (* maddl *) +- apply addl_sound; trivial. + apply mull_sound; trivial. + rewrite default_idem; trivial. + rewrite default_idem; trivial. Qed. Lemma operation_is_redundant_sound: diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 0e9a7af9..c4338857 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -146,10 +146,8 @@ Inductive operation : Type := | Oshrlu (**r [rd = r1 >> r2] (unsigned) *) | Oshrluimm (n: int) (**r [rd = r1 >> n] (unsigned) *) | Oshrxlimm (n: int) (**r [rd = r1 / 2^n] (signed) *) - (* FIXME | Omaddl (**r [rd = rd + r1 * r2] *) | Omaddlimm (n: int64) (**r [rd = rd + r1 * imm] *) -*) (*c Floating-point arithmetic: *) | Onegf (**r [rd = - r1] *) | Oabsf (**r [rd = abs(r1)] *) @@ -346,11 +344,8 @@ Definition eval_operation | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2) | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n)) | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n) - - (* | Omaddl, v1::v2::v3::nil => Some (Val.addl v1 (Val.mull v2 v3)) | (Omaddlimm n), v1::v2::nil => Some (Val.addl v1 (Val.mull v2 (Vlong n))) - *) | Onegf, v1::nil => Some (Val.negf v1) | Oabsf, v1::nil => Some (Val.absf v1) @@ -536,10 +531,9 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshrlu => (Tlong :: Tint :: nil, Tlong) | Oshrluimm _ => (Tlong :: nil, Tlong) | Oshrxlimm _ => (Tlong :: nil, Tlong) - (* FIXME | Omaddl => (Tlong :: Tlong :: Tlong :: nil, Tlong) | Omaddlimm _ => (Tlong :: Tlong :: nil, Tlong) -*) + | Onegf => (Tfloat :: nil, Tfloat) | Oabsf => (Tfloat :: nil, Tfloat) | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat) @@ -753,10 +747,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... (* shrxl *) - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0... - (* FIXME (* maddl, maddlim *) - - destruct v0; destruct v1; destruct v2... - - destruct v0; destruct v1... *) + - destruct v0; destruct v1; destruct v2; simpl; trivial. + destruct Archi.ptr64; simpl; trivial. + - destruct v0; destruct v1; simpl; trivial. + destruct Archi.ptr64; simpl; trivial. (* negf, absf *) - destruct v0... - destruct v0... @@ -1265,13 +1260,11 @@ Proof. - inv H4; simpl in H1; try discriminate. simpl. destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists. - (* - (* maddl, maddlim *) - - inv H2; inv H3; inv H4; simpl; auto; simpl. - destruct Archi.ptr64; trivial. - s - - inv H2; inv H4; simpl; auto. - *) + (* maddl, maddlimm *) + - apply Val.addl_inject; auto. + inv H2; inv H3; inv H4; simpl; auto. + - apply Val.addl_inject; auto. + inv H4; inv H2; simpl; auto. (* negf, absf *) - inv H4; simpl; auto. diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index b43c4d78..fb1977ea 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -132,6 +132,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshrlu, v1::v2::nil => shrlu v1 v2 | Oshrluimm n, v1::nil => shrlu v1 (I n) | Oshrxlimm n, v1::nil => shrxl v1 (I n) + | Omaddl, v1::v2::v3::nil => addl v1 (mull v2 v3) + | Omaddlimm n, v1::v2::nil => addl v1 (mull v2 (L n)) | Onegf, v1::nil => negf v1 | Oabsf, v1::nil => absf v1 | Oaddf, v1::v2::nil => addf v1 v2 |