diff options
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 6 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Asmvliw.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Op.v | 20 | ||||
-rw-r--r-- | mppa_k1c/ValueAOp.v | 37 |
5 files changed, 48 insertions, 21 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 839d444d..ef980894 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -443,6 +443,12 @@ Definition transl_op | Oaddimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (addimm32 rd rs n ::i k) + | Oaddx shift, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Paddxw shift rd rs1 rs2 ::i k) + | Oaddximm shift n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Paddxiw shift rd rs n ::i k) | Oneg, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pnegw rd rs ::i k) diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 1569aedf..86a0ff88 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1693,7 +1693,7 @@ Opaque Int.eq. split; intros; Simpl. assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. + apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. - (* Oshrximm *) econstructor; split. + apply exec_straight_one. simpl. eauto. diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 2bf9115e..c1f21f8d 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -1068,8 +1068,8 @@ Definition arith_eval_rrr n v1 v2 := | Pfmuld => Val.mulf v1 v2 | Pfmulw => Val.mulfs v1 v2 - | Paddxw shift => Val.add v1 (Val.shl v2 (Vint (int_of_shift1_4 shift))) - | Paddxl shift => Val.addl v1 (Val.shll v2 (Vint (int_of_shift1_4 shift))) + | Paddxw shift => Val.add v2 (Val.shl v1 (Vint (int_of_shift1_4 shift))) + | Paddxl shift => Val.addl v1 (Val.shll v1 (Vint (int_of_shift1_4 shift))) | Prevsubxw shift => Val.sub v2 (Val.shl v1 (Vint (int_of_shift1_4 shift))) diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 4abd104e..fb6c454c 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -405,8 +405,8 @@ 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)) + | Oaddx shift, v1 :: v2 :: nil => Some (Val.add v2 (Val.shl v1 (Vint (int_of_shift1_4 shift)))) + | Oaddximm shift n, v1 :: nil => Some (Val.add (Vint n) (Val.shl v1 (Vint (int_of_shift1_4 shift)))) | 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) @@ -457,8 +457,8 @@ 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)) + | Oaddxl shift, v1 :: v2 :: nil => Some (Val.addl v2 (Val.shll v1 (Vint (int_of_shift1_4 shift)))) + | Oaddxlimm shift n, v1 :: nil => Some (Val.addl (Vlong n) (Val.shll v1 (Vint (int_of_shift1_4 shift)))) | 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) @@ -836,7 +836,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - apply type_add. (* addx, addximm *) - apply type_add. - - apply type_add. + - destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* neg, sub *) - destruct v0... - apply type_sub. @@ -917,7 +918,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - apply type_addl. (* addxl addxlimm *) - apply type_addl. - - apply type_addl. + - destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* negl, subl *) - destruct v0... - apply type_subl. @@ -1452,8 +1454,7 @@ Proof. (* 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. + - inv H4; simpl; trivial. try destruct (Int.ltu _ _); simpl; auto. (* neg, sub *) - inv H4; simpl; auto. - apply Val.sub_inject; auto. @@ -1543,8 +1544,7 @@ Proof. - apply Val.addl_inject; auto. inv H4; simpl; trivial. destruct (Int.ltu _ _); simpl; trivial. - - apply Val.addl_inject; auto. - inv H4; simpl; trivial. + - inv H4; simpl; trivial. destruct (Int.ltu _ _); simpl; trivial. (* negl, subl *) - inv H4; simpl; auto. diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 27faa33c..00e8a1d8 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -161,8 +161,8 @@ 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) + | Oaddx shift, v1::v2::nil => add v2 (shl v1 (I (int_of_shift1_4 shift))) + | Oaddximm shift n, v1::nil => add (I n) (shl v1 (I (int_of_shift1_4 shift))) | 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))) @@ -212,8 +212,8 @@ 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) + | Oaddxl shift, v1::v2::nil => addl v2 (shll v1 (I (int_of_shift1_4 shift))) + | Oaddxlimm shift n, v1::nil => addl (L n) (shll v1 (I (int_of_shift1_4 shift))) | 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))) @@ -378,20 +378,41 @@ Proof. - destruct (propagate_float_constants tt); constructor. - destruct (propagate_float_constants tt); constructor. - rewrite Ptrofs.add_zero_l; eauto with va. + - replace (match Val.shl a1 (Vint (int_of_shift1_4 shift)) with + | Vint n2 => Vint (Int.add n n2) + | Vptr b2 ofs2 => + if Archi.ptr64 + then Vundef + else Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int n)) + | _ => Vundef + end) with (Val.add (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))). + + eauto with va. + + destruct a1; destruct shift; reflexivity. - (*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. + + eauto with va. + + destruct a1; destruct shift; reflexivity. + - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with + | Vlong n2 => Vlong (Int64.add n n2) + | Vptr b2 ofs2 => + if Archi.ptr64 + then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n)) + else Vundef + | _ => Vundef + end) with + (Val.addl (Vlong n) (Val.shll 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. + + 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). |