From e2ea45f5ba656254fa11bf3f355da67292c11f06 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 May 2019 23:37:07 +0200 Subject: more integer Op --- mppa_k1c/Machregs.v | 5 +- mppa_k1c/NeedOp.v | 60 ++++++++++++++++++++ mppa_k1c/Op.v | 159 ++++++++++++++++++++++++++++++++++++++++++++++++---- mppa_k1c/ValueAOp.v | 38 +++++++++++-- 4 files changed, 245 insertions(+), 17 deletions(-) diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index cd8c6606..6e0efe28 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -213,7 +213,10 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ + | Omadd | Omaddimm _ + | Omaddl | Omaddlimm _ + | Omsub | Omsubimm _ + | Omsubl | Omsublimm _ | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ | Oinsf _ _ | Oinsfl _ _ => true | _ => false diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index c10f5c56..ced31758 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -42,8 +42,13 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ocast16signed => op1 (sign_ext 16 nv) | Oadd => op2 (modarith nv) | Oaddimm n => op1 (modarith nv) + | Oaddx _ => op2 (default nv) + | Oaddximm _ _ => op1 (default nv) | Oneg => op1 (modarith nv) | Osub => op2 (default nv) + | Orevsubimm _ => op1 (default nv) + | Orevsubx _ => op2 (default nv) + | Orevsubximm _ _ => op1 (default nv) | Omul => op2 (modarith nv) | Omulimm _ => op1 (modarith nv) | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv) @@ -72,12 +77,19 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshrximm n => op1 (default nv) | Omadd => op3 (modarith nv) | Omaddimm n => op2 (modarith nv) + | Omsub => op3 (modarith nv) + | Omsubimm n => op2 (modarith nv) | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocast32signed => op1 (default nv) | Ocast32unsigned => op1 (default nv) | Oaddl => op2 (default nv) | Oaddlimm n => op1 (default nv) + | Oaddxl _ => op2 (default nv) + | Oaddxlimm _ _ => op1 (default nv) + | Orevsublimm _ => op1 (default nv) + | Orevsubxl _ => op2 (default nv) + | Orevsubxlimm _ _ => op1 (default nv) | Onegl => op1 (default nv) | Osubl => op2 (default nv) | Omull => op2 (default nv) @@ -107,6 +119,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshrxlimm n => op1 (default nv) | Omaddl => op3 (default nv) | Omaddlimm n => op2 (default nv) + | Omsubl => op3 (default nv) + | Omsublimm n => op2 (default nv) | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) | Onegfs | Oabsfs => op1 (default nv) @@ -229,6 +243,26 @@ Proof. - apply Val.addl_lessdef; trivial. Qed. +Lemma subl_lessdef: + forall v1 v1' v2 v2', + Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Val.lessdef (Val.subl v1 v2) (Val.subl v1' v2'). +Proof. + intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto. +Qed. + +Lemma subl_sound: + forall v1 w1 v2 w2 x, + vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> + vagree (Val.subl v1 v2) (Val.subl w1 w2) x. +Proof. + unfold default; intros. + destruct x; simpl in *; trivial. + - unfold Val.subl. + destruct v1; destruct v2; trivial; destruct Archi.ptr64; simpl; trivial. + destruct (eq_block _ _) ; simpl; trivial. + - apply subl_lessdef; trivial. +Qed. + Lemma mull_sound: forall v1 w1 v2 w2 x, @@ -424,6 +458,14 @@ Proof. destruct nv; simpl; trivial. Qed. +Remark sub_add_neg : + forall x y, Val.sub x y = Val.add x (Val.neg y). +Proof. + destruct x; destruct y; simpl; trivial. + f_equal. + apply Int.sub_add_opp. +Qed. + Lemma needs_of_operation_sound: forall op args v nv args', eval_operation ge (Vptr sp Ptrofs.zero) op args m1 = Some v -> @@ -466,8 +508,26 @@ 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. +- repeat rewrite sub_add_neg. + apply add_sound; trivial. + apply neg_sound; trivial. + rewrite modarith_idem. + apply mul_sound; + rewrite modarith_idem; trivial. +- repeat rewrite sub_add_neg. + apply add_sound; trivial. + apply neg_sound; trivial. + rewrite modarith_idem. + apply mul_sound; + rewrite modarith_idem; trivial. + apply vagree_same. (* maddl *) - apply addl_sound; trivial. + apply mull_sound; trivial. + rewrite default_idem; trivial. + rewrite default_idem; trivial. + (* msubl *) +- apply subl_sound; trivial. apply mull_sound; trivial. rewrite default_idem; trivial. rewrite default_idem; trivial. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 5e80589b..b93a9fc3 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -66,6 +66,20 @@ Definition arg_type_of_condition0 (cond: condition0) := (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) +Inductive shift1_4 : Type := +| SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4. + +Definition z_of_shift1_4 (x : shift1_4) := + match x with + | SHIFT1 => 1 + | SHIFT2 => 2 + | SHIFT3 => 3 + | SHIFT4 => 4 + end. + +Definition int_of_shift1_4 (x : shift1_4) := + Int.repr (z_of_shift1_4 x). + Inductive operation : Type := | Omove (**r [rd = r1] *) | Ointconst (n: int) (**r [rd] is set to the given integer constant *) @@ -79,8 +93,13 @@ Inductive operation : Type := | Ocast16signed (**r [rd] is 16-bit sign extension of [r1] *) | Oadd (**r [rd = r1 + r2] *) | Oaddimm (n: int) (**r [rd = r1 + n] *) + | Oaddx (shift: shift1_4) (**r [rd = r1 << shift + r2] *) + | Oaddximm (shift: shift1_4) (n: int) (**r [rd = r1 << shift + n] *) | Oneg (**r [rd = - r1] *) | Osub (**r [rd = r1 - r2] *) + | Orevsubimm (n: int) (**r [rd = n - r1] *) + | Orevsubx (shift: shift1_4) (**r [rd = r2 -r1 << shift] *) + | Orevsubximm (shift: shift1_4) (n: int) (**r [rd = n -r1 << shift] *) | Omul (**r [rd = r1 * r2] *) | Omulimm (n: int) (**r [rd = r1 * n] *) | Omulhs (**r [rd = high part of r1 * r2, signed] *) @@ -116,6 +135,8 @@ Inductive operation : Type := | Ororimm (n: int) (**r rotate right immediate *) | Omadd (**r [rd = rd + r1 * r2] *) | Omaddimm (n: int) (**r [rd = rd + r1 * imm] *) + | Omsub (**r [rd = rd - r1 * r2] *) + | Omsubimm (n: int) (**r [rd = rd - r1 * imm] *) (*c 64-bit integer arithmetic: *) | Omakelong (**r [rd = r1 << 32 | r2] *) | Olowlong (**r [rd = low-word(r1)] *) @@ -124,6 +145,11 @@ Inductive operation : Type := | Ocast32unsigned (**r [rd] is 32-bit zero extension of [r1] *) | Oaddl (**r [rd = r1 + r2] *) | Oaddlimm (n: int64) (**r [rd = r1 + n] *) + | Oaddxl (shift: shift1_4) (**r [rd = r1 << shift + r2] *) + | Oaddxlimm (shift: shift1_4) (n: int64) (**r [rd = r1 << shift + n] *) + | Orevsublimm (n: int64) (**r [rd = n - r1] *) + | Orevsubxl (shift: shift1_4) (**r [rd = r2 -r1 << shift] *) + | Orevsubxlimm (shift: shift1_4) (n: int64) (**r [rd = n -r1 << shift] *) | Onegl (**r [rd = - r1] *) | Osubl (**r [rd = r1 - r2] *) | Omull (**r [rd = r1 * r2] *) @@ -160,6 +186,8 @@ Inductive operation : Type := | Oshrxlimm (n: int) (**r [rd = r1 / 2^n] (signed) *) | Omaddl (**r [rd = rd + r1 * r2] *) | Omaddlimm (n: int64) (**r [rd = rd + r1 * imm] *) + | Omsubl (**r [rd = rd - r1 * r2] *) + | Omsublimm (n: int64) (**r [rd = rd - r1 * imm] *) (*c Floating-point arithmetic: *) | Onegf (**r [rd = - r1] *) | Oabsf (**r [rd = abs(r1)] *) @@ -235,9 +263,14 @@ Proof. decide equality. Defined. +Definition eq_shift1_4 (x y : shift1_4): {x=y} + {x<>y}. +Proof. + decide equality. +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 eq_condition0 Z.eq_dec; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0 Z.eq_dec eq_shift1_4; intros. decide equality. Defined. @@ -386,8 +419,13 @@ Definition eval_operation | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1) | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2) | Oaddimm n, v1 :: nil => Some (Val.add v1 (Vint n)) + | Oaddx shift, v1 :: v2 :: nil => Some (Val.add (Val.shl v1 (Vint (int_of_shift1_4 shift))) v2) + | Oaddximm shift n, v1 :: nil => Some (Val.add (Val.shl v1 (Vint (int_of_shift1_4 shift))) (Vint n)) | Oneg, v1 :: nil => Some (Val.neg v1) | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2) + | Orevsubimm n, v1 :: nil => Some (Val.sub (Vint n) v1) + | Orevsubx shift, v1 :: v2 :: nil => Some (Val.sub v2 (Val.shl v1 (Vint (int_of_shift1_4 shift)))) + | Orevsubximm shift n, v1 :: nil => Some (Val.sub (Vint n) (Val.shl v1 (Vint (int_of_shift1_4 shift)))) | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2) | Omulimm n, v1 :: nil => Some (Val.mul v1 (Vint n)) | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2) @@ -423,6 +461,8 @@ Definition eval_operation | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) | Omadd, v1::v2::v3::nil => Some (Val.add v1 (Val.mul v2 v3)) | (Omaddimm n), v1::v2::nil => Some (Val.add v1 (Val.mul v2 (Vint n))) + | Omsub, v1::v2::v3::nil => Some (Val.sub v1 (Val.mul v2 v3)) + | (Omsubimm n), v1::v2::nil => Some (Val.sub v1 (Val.mul v2 (Vint n))) | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2) | Olowlong, v1::nil => Some (Val.loword v1) @@ -431,8 +471,13 @@ Definition eval_operation | Ocast32unsigned, v1 :: nil => Some (Val.longofintu v1) | Oaddl, v1 :: v2 :: nil => Some (Val.addl v1 v2) | Oaddlimm n, v1::nil => Some (Val.addl v1 (Vlong n)) + | Oaddxl shift, v1 :: v2 :: nil => Some (Val.addl (Val.shll v1 (Vint (int_of_shift1_4 shift))) v2) + | Oaddxlimm shift n, v1 :: nil => Some (Val.addl (Val.shll v1 (Vint (int_of_shift1_4 shift))) (Vlong n)) | Onegl, v1::nil => Some (Val.negl v1) | Osubl, v1::v2::nil => Some (Val.subl v1 v2) + | Orevsublimm n, v1 :: nil => Some (Val.subl (Vlong n) v1) + | Orevsubxl shift, v1 :: v2 :: nil => Some (Val.subl v2 (Val.shll v1 (Vint (int_of_shift1_4 shift)))) + | Orevsubxlimm shift n, v1 :: nil => Some (Val.subl (Vlong n) (Val.shll v1 (Vint (int_of_shift1_4 shift)))) | Omull, v1::v2::nil => Some (Val.mull v1 v2) | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n)) | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2) @@ -467,6 +512,8 @@ Definition eval_operation | 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))) + | Omsubl, v1::v2::v3::nil => Some (Val.subl v1 (Val.mull v2 v3)) + | (Omsublimm n), v1::v2::nil => Some (Val.subl v1 (Val.mull v2 (Vlong n))) | Onegf, v1::nil => Some (Val.negf v1) | Oabsf, v1::nil => Some (Val.absf v1) @@ -583,8 +630,13 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ocast16signed => (Tint :: nil, Tint) | Oadd => (Tint :: Tint :: nil, Tint) | Oaddimm _ => (Tint :: nil, Tint) + | Oaddx _ => (Tint :: Tint :: nil, Tint) + | Oaddximm _ _ => (Tint :: nil, Tint) | Oneg => (Tint :: nil, Tint) | Osub => (Tint :: Tint :: nil, Tint) + | Orevsubimm _ => (Tint :: nil, Tint) + | Orevsubx _ => (Tint :: Tint :: nil, Tint) + | Orevsubximm _ _ => (Tint :: nil, Tint) | Omul => (Tint :: Tint :: nil, Tint) | Omulimm _ => (Tint :: nil, Tint) | Omulhs => (Tint :: Tint :: nil, Tint) @@ -620,6 +672,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ororimm _ => (Tint :: nil, Tint) | Omadd => (Tint :: Tint :: Tint :: nil, Tint) | Omaddimm _ => (Tint :: Tint :: nil, Tint) + | Omsub => (Tint :: Tint :: Tint :: nil, Tint) + | Omsubimm _ => (Tint :: Tint :: nil, Tint) | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) @@ -628,6 +682,11 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ocast32unsigned => (Tint :: nil, Tlong) | Oaddl => (Tlong :: Tlong :: nil, Tlong) | Oaddlimm _ => (Tlong :: nil, Tlong) + | Oaddxl _ => (Tlong :: Tlong :: nil, Tlong) + | Oaddxlimm _ _ => (Tlong :: nil, Tlong) + | Orevsublimm _ => (Tlong :: nil, Tlong) + | Orevsubxl _ => (Tlong :: Tlong :: nil, Tlong) + | Orevsubxlimm _ _ => (Tlong :: nil, Tlong) | Onegl => (Tlong :: nil, Tlong) | Osubl => (Tlong :: Tlong :: nil, Tlong) | Omull => (Tlong :: Tlong :: nil, Tlong) @@ -664,6 +723,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshrxlimm _ => (Tlong :: nil, Tlong) | Omaddl => (Tlong :: Tlong :: Tlong :: nil, Tlong) | Omaddlimm _ => (Tlong :: Tlong :: nil, Tlong) + | Omsubl => (Tlong :: Tlong :: Tlong :: nil, Tlong) + | Omsublimm _ => (Tlong :: Tlong :: nil, Tlong) | Onegf => (Tfloat :: nil, Tfloat) | Oabsf => (Tfloat :: nil, Tfloat) @@ -736,6 +797,32 @@ Proof. intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto. Qed. +Remark type_sub: + forall v1 v2, Val.has_type (Val.sub v1 v2) Tint. +Proof. + intros. unfold Val.has_type, Val.sub. destruct Archi.ptr64, v1, v2; simpl; auto. + destruct (eq_block _ _); auto. +Qed. + +Remark type_subl: + forall v1 v2, Val.has_type (Val.subl v1 v2) Tlong. +Proof. + intros. unfold Val.has_type, Val.subl. destruct Archi.ptr64, v1, v2; simpl; auto. + destruct (eq_block _ _); auto. +Qed. + +Remark type_shl: + forall v1 v2, Val.has_type (Val.shl v1 v2) Tint. +Proof. + destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial. +Qed. + +Remark type_shll: + forall v1 v2, Val.has_type (Val.shll v1 v2) Tlong. +Proof. + destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial. +Qed. + Lemma type_of_operation_sound: forall op vl sp v m, op <> Omove -> @@ -761,9 +848,17 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* add, addimm *) - apply type_add. - apply type_add. + (* addx, addximm *) + - apply type_add. + - apply type_add. (* neg, sub *) - destruct v0... - - unfold Val.sub. destruct v0; destruct v1... + - apply type_sub. + (* revsubimm, revsubx, revsubximm *) + - destruct v0... + - apply type_sub. + - destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* mul, mulimm, mulhs, mulhu *) - destruct v0; destruct v1... - destruct v0... @@ -819,8 +914,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* shrimm *) - destruct v0; simpl... (* madd *) - - destruct v0; destruct v1; destruct v2... - - destruct v0; destruct v1... + - apply type_add. + - apply type_add. + (* msub *) + - apply type_sub. + - apply type_sub. (* makelong, lowlong, highlong *) - destruct v0; destruct v1... - destruct v0... @@ -831,11 +929,16 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* addl, addlimm *) - apply type_addl. - apply type_addl. + (* addxl addxlimm *) + - apply type_addl. + - apply type_addl. (* negl, subl *) - destruct v0... - - unfold Val.subl. destruct v0; destruct v1... - unfold Val.has_type; destruct Archi.ptr64... - destruct (eq_block b b0)... + - apply type_subl. + - destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + - destruct v0... + - apply type_subl. (* mull, mullhs, mullhu *) - destruct v0; destruct v1... - destruct v0... @@ -889,10 +992,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* shrxl *) - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0... (* maddl, maddlim *) - - destruct v0; destruct v1; destruct v2; simpl; trivial. - destruct Archi.ptr64; simpl; trivial. - - destruct v0; destruct v1; simpl; trivial. - destruct Archi.ptr64; simpl; trivial. + - apply type_addl. + - apply type_addl. + (* msubl, msublim *) + - apply type_subl. + - apply type_subl. (* negf, absf *) - destruct v0... - destruct v0... @@ -1359,9 +1463,19 @@ Proof. (* add, addimm *) - apply Val.add_inject; auto. - apply Val.add_inject; auto. + (* addx, addximm *) + - apply Val.add_inject; trivial. + inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto. + - apply Val.add_inject; trivial. + inv H4; simpl; try destruct (Int.ltu _ _); simpl; auto. (* neg, sub *) - inv H4; simpl; auto. - apply Val.sub_inject; auto. + (* revsubimm, revsubx, revsubximm *) + - inv H4; simpl; trivial. + - apply Val.sub_inject; trivial. + inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto. + - inv H4; simpl; try destruct (Int.ltu _ _); simpl; auto. (* mul, mulimm, mulhs, mulhu *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1424,6 +1538,11 @@ Proof. (* madd, maddim *) - inv H2; inv H3; inv H4; simpl; auto. - inv H2; inv H4; simpl; auto. + (* msub *) + - apply Val.sub_inject; auto. + inv H3; inv H2; simpl; auto. + - apply Val.sub_inject; trivial. + inv H2; inv H4; simpl; auto. (* makelong, highlong, lowlong *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1434,8 +1553,21 @@ Proof. (* addl, addlimm *) - apply Val.addl_inject; auto. - apply Val.addl_inject; auto. + (* addxl, addxlimm *) + - apply Val.addl_inject; auto. + inv H4; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + - apply Val.addl_inject; auto. + inv H4; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* negl, subl *) - inv H4; simpl; auto. + - apply Val.subl_inject; auto. + inv H4; inv H2; simpl; trivial; + destruct (Int.ltu _ _); simpl; trivial. + - inv H4; simpl; trivial; + destruct (Int.ltu _ _); simpl; trivial. + - inv H4; simpl; auto. - apply Val.subl_inject; auto. (* mull, mullhs, mullhu *) - inv H4; inv H2; simpl; auto. @@ -1500,6 +1632,11 @@ Proof. inv H2; inv H3; inv H4; simpl; auto. - apply Val.addl_inject; auto. inv H4; inv H2; simpl; auto. + (* msubl, msublimm *) + - apply Val.subl_inject; auto. + inv H2; inv H3; inv H4; simpl; auto. + - apply Val.subl_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 643cca0c..27faa33c 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -161,8 +161,13 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ocast16signed, v1 :: nil => sign_ext 16 v1 | Oadd, v1::v2::nil => add v1 v2 | Oaddimm n, v1::nil => add v1 (I n) + | Oaddx shift, v1::v2::nil => add (shl v1 (I (int_of_shift1_4 shift))) v2 + | Oaddximm shift n, v1::nil => add (shl v1 (I (int_of_shift1_4 shift))) (I n) | Oneg, v1::nil => neg v1 | Osub, v1::v2::nil => sub v1 v2 + | Orevsubx shift, v1::v2::nil => sub v2 (shl v1 (I (int_of_shift1_4 shift))) + | Orevsubimm n, v1::nil => sub (I n) v1 + | Orevsubximm shift n, v1::nil => sub (I n) (shl v1 (I (int_of_shift1_4 shift))) | Omul, v1::v2::nil => mul v1 v2 | Omulimm n, v1::nil => mul v1 (I n) | Omulhs, v1::v2::nil => mulhs v1 v2 @@ -198,6 +203,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshrximm n, v1::nil => shrx v1 (I n) | Omadd, v1::v2::v3::nil => add v1 (mul v2 v3) | Omaddimm n, v1::v2::nil => add v1 (mul v2 (I n)) + | Omsub, v1::v2::v3::nil => sub v1 (mul v2 v3) + | Omsubimm n, v1::v2::nil => sub v1 (mul v2 (I n)) | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 | Ohighlong, v1::nil => hiword v1 @@ -205,8 +212,13 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ocast32unsigned, v1::nil => longofintu v1 | Oaddl, v1::v2::nil => addl v1 v2 | Oaddlimm n, v1::nil => addl v1 (L n) + | Oaddxl shift, v1::v2::nil => addl (shll v1 (I (int_of_shift1_4 shift))) v2 + | Oaddxlimm shift n, v1::nil => addl (shll v1 (I (int_of_shift1_4 shift))) (L n) | Onegl, v1::nil => negl v1 | Osubl, v1::v2::nil => subl v1 v2 + | Orevsubxl shift, v1::v2::nil => subl v2 (shll v1 (I (int_of_shift1_4 shift))) + | Orevsublimm n, v1::nil => subl (L n) v1 + | Orevsubxlimm shift n, v1::nil => subl (L n) (shll v1 (I (int_of_shift1_4 shift))) | Omull, v1::v2::nil => mull v1 v2 | Omullimm n, v1::nil => mull v1 (L n) | Omullhs, v1::v2::nil => mullhs v1 v2 @@ -241,6 +253,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | 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)) + | Omsubl, v1::v2::v3::nil => subl v1 (mull v2 v3) + | Omsublimm n, v1::v2::nil => subl v1 (mull v2 (L n)) | Onegf, v1::nil => negf v1 | Oabsf, v1::nil => absf v1 | Oaddf, v1::v2::nil => addf v1 v2 @@ -360,11 +374,25 @@ Theorem eval_static_operation_sound: vmatch bc vres (eval_static_operation op aargs). Proof. unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs; intros; - destruct op; InvHyps; eauto with va. - destruct (propagate_float_constants tt); constructor. - destruct (propagate_float_constants tt); constructor. - rewrite Ptrofs.add_zero_l; eauto with va. - apply of_optbool_sound. eapply eval_static_condition_sound; eauto. + destruct op; try (InvHyps; eauto with va). + - destruct (propagate_float_constants tt); constructor. + - destruct (propagate_float_constants tt); constructor. + - rewrite Ptrofs.add_zero_l; eauto with va. + - (*revsubimm*) inv H1; constructor. + - replace (match Val.shl a1 (Vint (int_of_shift1_4 shift)) with + | Vint n2 => Vint (Int.sub n n2) + | _ => Vundef + end) with (Val.sub (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))). + eauto with va. + destruct a1; destruct shift; reflexivity. + - inv H1; constructor. + - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with + | Vlong n2 => Vlong (Int64.sub n n2) + | _ => Vundef + end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))). + eauto with va. + destruct a1; destruct shift; reflexivity. + - apply of_optbool_sound. eapply eval_static_condition_sound; eauto. (* select *) - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption). rewrite eval_select_to2. -- cgit