diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 06:35:31 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 06:35:31 +0200 |
| commit | d336d31434602b786bcaa89c8d91d2472d9cb3f5 (patch) | |
| tree | e315eb52c474ea628b066c1108556abaad838453 /mppa_k1c/Op.v | |
| parent | d8d22519bff9414f973a1310cb32eb60e6695796 (diff) | |
| download | compcert-kvx-d336d31434602b786bcaa89c8d91d2472d9cb3f5.tar.gz compcert-kvx-d336d31434602b786bcaa89c8d91d2472d9cb3f5.zip | |
Oaddx -> P
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 20 |
1 files changed, 10 insertions, 10 deletions
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. |