diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asm.v | 25 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 28 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 49 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 53 | ||||
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 39 | ||||
| -rw-r--r-- | mppa_k1c/DecBoolOps.v | 15 | ||||
| -rw-r--r-- | mppa_k1c/ExtValues.v | 119 | ||||
| -rw-r--r-- | mppa_k1c/Machregs.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/NeedOp.v | 5 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 97 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 43 | ||||
| -rw-r--r-- | mppa_k1c/PrintOp.ml | 2 | ||||
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 43 | ||||
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 122 | ||||
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 43 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 105 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 18 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 97 | ||||
| -rwxr-xr-x | mppa_k1c/bitmasks.py | 12 |
19 files changed, 759 insertions, 160 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 1e1f6e36..d1ac8a67 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -23,6 +23,7 @@ Require Import AST. Require Import Integers.
Require Import Floats.
Require Import Values.
+Require Import ExtValues.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
@@ -133,6 +134,12 @@ Inductive instruction : Type := | Pextfz (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *)
| Pextfs (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields signed *)
+ | Pextfzl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *)
+ | Pextfsl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields signed *)
+
+ | Pinsf (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r insert bitfield *)
+ | Pinsfl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r insert bitfield *)
+
| Pfabsd (rd rs: ireg) (**r float absolute double *)
| Pfabsw (rd rs: ireg) (**r float absolute word *)
| Pfnegd (rd rs: ireg) (**r float negate double *)
@@ -142,9 +149,7 @@ Inductive instruction : Type := | Pfloatwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (32 -> 32) *)
| Pfloatuwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (u32 -> 32) *)
| Pfloatudrnsz (rd rs: ireg) (**r Floating Point Conversion from unsigned integer (64 bits) *)
- | Pfloatudrnsz_i32 (rd rs: ireg) (**r Floating Point Conversion from unsigned integer (32 bits) *)
| Pfloatdrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (64 bits) *)
- | Pfloatdrnsz_i32 (rd rs: ireg) (**r Floating Point Conversion from integer (32 bits) *)
| Pfixedwrzz (rd rs: ireg) (**r Integer conversion from floating point *)
| Pfixeduwrzz (rd rs: ireg) (**r Integer conversion from floating point (f32 -> 32 bits unsigned *)
| Pfixeddrzz (rd rs: ireg) (**r Integer conversion from floating point (i64 -> 64 bits) *)
@@ -182,6 +187,7 @@ Inductive instruction : Type := | Pandnw (rd rs1 rs2: ireg) (**r andn word *)
| Pornw (rd rs1 rs2: ireg) (**r orn word *)
| Psraw (rd rs1 rs2: ireg) (**r shift right arithmetic word *)
+ | Psrxw (rd rs1 rs2: ireg) (**r shift right arithmetic word round to 0*)
| Psrlw (rd rs1 rs2: ireg) (**r shift right logical word *)
| Psllw (rd rs1 rs2: ireg) (**r shift left logical word *)
| Pmaddw (rd rs1 rs2: ireg) (**r multiply-add words *)
@@ -200,6 +206,7 @@ Inductive instruction : Type := | Pslll (rd rs1 rs2: ireg) (**r shift left logical long *)
| Psrll (rd rs1 rs2: ireg) (**r shift right logical long *)
| Psral (rd rs1 rs2: ireg) (**r shift right arithmetic long *)
+ | Psrxl (rd rs1 rs2: ireg) (**r shift right arithmetic long round to 0*)
| Pmaddl (rd rs1 rs2: ireg) (**r multiply-add long *)
| Pfaddd (rd rs1 rs2: ireg) (**r Float addition double *)
@@ -223,11 +230,13 @@ Inductive instruction : Type := | Pandniw (rd rs: ireg) (imm: int) (**r andn imm word *)
| Porniw (rd rs: ireg) (imm: int) (**r orn imm word *)
| Psraiw (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word *)
+ | Psrxiw (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word round to 0*)
| Psrliw (rd rs: ireg) (imm: int) (**r shift right logical imm word *)
| Pslliw (rd rs: ireg) (imm: int) (**r shift left logical imm word *)
| Proriw (rd rs: ireg) (imm: int) (**r rotate right imm word *)
| Pmaddiw (rd rs: ireg) (imm: int) (**r multiply add imm word *)
| Psllil (rd rs: ireg) (imm: int) (**r shift left logical immediate long *)
+ | Psrxil (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word round to 0*)
| Psrlil (rd rs: ireg) (imm: int) (**r shift right logical immediate long *)
| Psrail (rd rs: ireg) (imm: int) (**r shift right arithmetic immediate long *)
@@ -286,6 +295,8 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmvliw.Pzxwd rd rs => Pzxwd rd rs
| PArithRR (Asmvliw.Pextfz stop start) rd rs => Pextfz rd rs stop start
| PArithRR (Asmvliw.Pextfs stop start) rd rs => Pextfs rd rs stop start
+ | PArithRR (Asmvliw.Pextfzl stop start) rd rs => Pextfzl rd rs stop start
+ | PArithRR (Asmvliw.Pextfsl stop start) rd rs => Pextfsl rd rs stop start
| PArithRR Asmvliw.Pfabsd rd rs => Pfabsd rd rs
| PArithRR Asmvliw.Pfabsw rd rs => Pfabsw rd rs
| PArithRR Asmvliw.Pfnegd rd rs => Pfnegd rd rs
@@ -296,8 +307,6 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmvliw.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs
| PArithRR Asmvliw.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs
| PArithRR Asmvliw.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs
- | PArithRR Asmvliw.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs
- | PArithRR Asmvliw.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs
| PArithRR Asmvliw.Pfixedwrzz rd rs => Pfixedwrzz rd rs
| PArithRR Asmvliw.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs
| PArithRR Asmvliw.Pfixeddrzz rd rs => Pfixeddrzz rd rs
@@ -334,6 +343,7 @@ Definition basic_to_instruction (b: basic) := | PArithRRR Asmvliw.Pandnw rd rs1 rs2 => Pandnw rd rs1 rs2
| PArithRRR Asmvliw.Pornw rd rs1 rs2 => Pornw rd rs1 rs2
| PArithRRR Asmvliw.Psraw rd rs1 rs2 => Psraw rd rs1 rs2
+ | PArithRRR Asmvliw.Psrxw rd rs1 rs2 => Psrxw rd rs1 rs2
| PArithRRR Asmvliw.Psrlw rd rs1 rs2 => Psrlw rd rs1 rs2
| PArithRRR Asmvliw.Psllw rd rs1 rs2 => Psllw rd rs1 rs2
@@ -351,6 +361,7 @@ Definition basic_to_instruction (b: basic) := | PArithRRR Asmvliw.Pslll rd rs1 rs2 => Pslll rd rs1 rs2
| PArithRRR Asmvliw.Psrll rd rs1 rs2 => Psrll rd rs1 rs2
| PArithRRR Asmvliw.Psral rd rs1 rs2 => Psral rd rs1 rs2
+ | PArithRRR Asmvliw.Psrxl rd rs1 rs2 => Psrxl rd rs1 rs2
| PArithRRR Asmvliw.Pfaddd rd rs1 rs2 => Pfaddd rd rs1 rs2
| PArithRRR Asmvliw.Pfaddw rd rs1 rs2 => Pfaddw rd rs1 rs2
@@ -372,11 +383,13 @@ Definition basic_to_instruction (b: basic) := | PArithRRI32 Asmvliw.Pandniw rd rs imm => Pandniw rd rs imm
| PArithRRI32 Asmvliw.Porniw rd rs imm => Porniw rd rs imm
| PArithRRI32 Asmvliw.Psraiw rd rs imm => Psraiw rd rs imm
+ | PArithRRI32 Asmvliw.Psrxiw rd rs imm => Psrxiw rd rs imm
| PArithRRI32 Asmvliw.Psrliw rd rs imm => Psrliw rd rs imm
| PArithRRI32 Asmvliw.Pslliw rd rs imm => Pslliw rd rs imm
| PArithRRI32 Asmvliw.Proriw rd rs imm => Proriw rd rs imm
| PArithRRI32 Asmvliw.Psllil rd rs imm => Psllil rd rs imm
| PArithRRI32 Asmvliw.Psrlil rd rs imm => Psrlil rd rs imm
+ | PArithRRI32 Asmvliw.Psrxil rd rs imm => Psrxil rd rs imm
| PArithRRI32 Asmvliw.Psrail rd rs imm => Psrail rd rs imm
(* RRI64 *)
@@ -398,6 +411,10 @@ Definition basic_to_instruction (b: basic) := | PArithARRR (Asmvliw.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2
| PArithARRR (Asmvliw.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2
+ (** ARR *)
+ | PArithARR (Asmvliw.Pinsf stop start) rd rs => Pinsf rd rs stop start
+ | PArithARR (Asmvliw.Pinsfl stop start) rd rs => Pinsfl rd rs stop start
+
(** ARRI32 *)
| PArithARRI32 Asmvliw.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index b3a72517..2e83fb44 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -57,6 +57,7 @@ Inductive arith_op := | OArithRRI32 (n: arith_name_rri32) (imm: int) | OArithRRI64 (n: arith_name_rri64) (imm: int64) | OArithARRR (n: arith_name_arrr) + | OArithARR (n: arith_name_arr) | OArithARRI32 (n: arith_name_arri32) (imm: int) | OArithARRI64 (n: arith_name_arri64) (imm: int64) . @@ -121,6 +122,7 @@ Definition arith_eval (ao: arith_op) (l: list value) := | OArithRRI32 n i, [Val v] => Some (Val (arith_eval_rri32 n v i)) | OArithRRI64 n i, [Val v] => Some (Val (arith_eval_rri64 n v i)) + | OArithARR n, [Val v1; Val v2] => Some (Val (arith_eval_arr n v1 v2)) | OArithARRR n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrr n v1 v2 v3)) | OArithARRI32 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri32 n v1 v2 i)) | OArithARRI64 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri64 n v1 v2 i)) @@ -329,6 +331,8 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool := match o2 with OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end | OArithARRR n1 => match o2 with OArithARRR n2 => phys_eq n1 n2 | _ => RET false end + | OArithARR n1 => + match o2 with OArithARR n2 => phys_eq n1 n2 | _ => RET false end | OArithARRI32 n1 i1 => match o2 with OArithARRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end | OArithARRI64 n1 i1 => @@ -597,6 +601,7 @@ Definition trans_arith (ai: ar_instruction) : inst := | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (PReg(#s) @ Enil))] | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (PReg(#s) @ Enil))] | PArithARRR n d s1 s2 => [(#d, Op (Arith (OArithARRR n)) (PReg(#d) @ PReg(#s1) @ PReg(#s2) @ Enil))] + | PArithARR n d s => [(#d, Op (Arith (OArithARR n)) (PReg(#d) @ PReg(#s) @ Enil))] | PArithARRI32 n d s i => [(#d, Op (Arith (OArithARRI32 n i)) (PReg(#d) @ PReg(#s) @ Enil))] | PArithARRI64 n d s i => [(#d, Op (Arith (OArithARRI64 n i)) (PReg(#d) @ PReg(#s) @ Enil))] end. @@ -776,6 +781,12 @@ Proof. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. +(* PArithARR *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. (* PArithARRI32 *) - eexists; split; [|split]. * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. @@ -1215,6 +1226,8 @@ Definition string_of_name_rr (n: arith_name_rr): pstring := | Pzxwd => "Pzxwd" | Pextfz _ _ => "Pextfz" | Pextfs _ _ => "Pextfs" + | Pextfzl _ _ => "Pextfzl" + | Pextfsl _ _ => "Pextfsl" | Pfabsd => "Pfabsd" | Pfabsw => "Pfabsw" | Pfnegd => "Pfnegd" @@ -1224,9 +1237,7 @@ Definition string_of_name_rr (n: arith_name_rr): pstring := | Pfloatwrnsz => "Pfloatwrnsz" | Pfloatuwrnsz => "Pfloatuwrnsz" | Pfloatudrnsz => "Pfloatudrnsz" - | Pfloatudrnsz_i32 => "Pfloatudrnsz_i32" | Pfloatdrnsz => "Pfloatdrnsz" - | Pfloatdrnsz_i32 => "Pfloatdrnsz_i32" | Pfixedwrzz => "Pfixedwrzz" | Pfixeduwrzz => "Pfixeduwrzz" | Pfixeddrzz => "Pfixeddrzz" @@ -1274,6 +1285,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pornw => "Pornw" | Psraw => "Psraw" | Psrlw => "Psrlw" + | Psrxw => "Psrxw" | Psllw => "Psllw" | Paddl => "Paddl" | Psubl => "Psubl" @@ -1288,6 +1300,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pmull => "Pmull" | Pslll => "Pslll" | Psrll => "Psrll" + | Psrxl => "Psrxl" | Psral => "Psral" | Pfaddd => "Pfaddd" | Pfaddw => "Pfaddw" @@ -1312,11 +1325,13 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Porniw => "Porniw" | Psraiw => "Psraiw" | Psrliw => "Psrliw" + | Psrxiw => "Psrxiw" | Pslliw => "Pslliw" | Proriw => "Proriw" | Psllil => "Psllil" | Psrlil => "Psrlil" | Psrail => "Psrail" + | Psrxil => "Psrxil" end. Definition string_of_name_rri64 (n: arith_name_rri64): pstring := @@ -1342,6 +1357,12 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring := | Pcmoveu _ => "Pcmoveu" end. +Definition string_of_name_arr (n: arith_name_arr): pstring := + match n with + | Pinsf _ _ => "Pinsf" + | Pinsfl _ _ => "Pinsfl" + end. + Definition string_of_name_arri32 (n: arith_name_arri32): pstring := match n with | Pmaddiw => "Pmaddw" @@ -1364,6 +1385,7 @@ Definition string_of_arith (op: arith_op): pstring := | OArithRRI32 n _ => string_of_name_rri32 n | OArithRRI64 n _ => string_of_name_rri64 n | OArithARRR n => string_of_name_arrr n + | OArithARR n => string_of_name_arr n | OArithARRI32 n _ => string_of_name_arri32 n | OArithARRI64 n _ => string_of_name_arri64 n end. @@ -1468,5 +1490,3 @@ Definition bblock_equiv_eq := pure_bblock_eq_test_correct true. End SECT_BBLOCK_EQUIV. - - diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 6af18178..6cd31468 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -21,6 +21,7 @@ Require Archi. Require Import Coqlib Errors. Require Import AST Integers Floats Memdata. Require Import Op Locations Machblock Asmblock. +Require ExtValues. Local Open Scope string_scope. Local Open Scope error_monad_scope. @@ -518,11 +519,7 @@ Definition transl_op OK (Psrliw rd rs n ::i k) | Oshrximm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (if Int.eq n Int.zero then Pmv rd rs ::i k else - Psraiw RTMP rs (Int.repr 31) ::i - Psrliw RTMP RTMP (Int.sub Int.iwordsize n) ::i - Paddw RTMP rs RTMP ::i - Psraiw rd RTMP n ::i k) + OK (Psrxiw rd rs n ::i k) | Ororimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Proriw rd rs n ::i k) @@ -644,11 +641,7 @@ Definition transl_op OK (Psrlil rd rs n ::i k) | Oshrxlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (if Int.eq n Int.zero then Pmv rd rs ::i k else - Psrail RTMP rs (Int.repr 63) ::i - Psrlil RTMP RTMP (Int.sub Int64.iwordsize' n) ::i - Paddl RTMP rs RTMP ::i - Psrail rd RTMP n ::i k) + OK (Psrxil rd rs n ::i k) | Omaddl, a1 :: a2 :: a3 :: nil => assertion (mreg_eq a1 res); do r1 <- ireg_of a1; @@ -703,12 +696,6 @@ Definition transl_op | Ofloatoflongu, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfloatudrnsz rd rs ::i k) - | Ofloatofint, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pfloatdrnsz_i32 rd rs ::i k) - | Ofloatofintu, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pfloatudrnsz_i32 rd rs ::i k) | Ointofsingle, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; OK (Pfixedwrzz rd rs ::i k) @@ -773,19 +760,37 @@ Definition transl_op end) | Oextfz stop start, a1 :: nil => - assertion ((Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize)); + assertion (ExtValues.is_bitfield stop start); do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pextfz stop start rd rs ::i k) | Oextfs stop start, a1 :: nil => - assertion ((Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize)); + assertion (ExtValues.is_bitfield stop start); do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pextfs stop start rd rs ::i k) + + | Oextfzl stop start, a1 :: nil => + assertion (ExtValues.is_bitfieldl stop start); + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pextfzl stop start rd rs ::i k) + + | Oextfsl stop start, a1 :: nil => + assertion (ExtValues.is_bitfieldl stop start); + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pextfsl stop start rd rs ::i k) + | Oinsf stop start, a0 :: a1 :: nil => + assertion (ExtValues.is_bitfield stop start); + assertion (mreg_eq a0 res); + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pinsf stop start rd rs ::i k) + + | Oinsfl stop start, a0 :: a1 :: nil => + assertion (ExtValues.is_bitfieldl stop start); + assertion (mreg_eq a0 res); + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pinsfl stop start rd rs ::i k) + | _, _ => Error(msg "Asmgenblock.transl_op") end. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index bbcffbe2..40f9f08b 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1593,44 +1593,27 @@ Opaque Int.eq. 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. - (* Oshrximm *) - clear H. exploit Val.shrx_shr_2; eauto. intros E; subst v; clear EV. - destruct (Int.eq n Int.zero). -+ econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros; Simpl. -+ change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. - eapply exec_straight_step. simpl; reflexivity. - eapply exec_straight_step. simpl; reflexivity. - apply exec_straight_one. simpl; reflexivity. - split; intros; Simpl. -(* - (* Ocast32signed *) - exploit cast32signed_correct; eauto. intros (rs' & A & B & C). - exists rs'; split; eauto. split. apply B. - intros. assert (r <> PC). { destruct r; auto; contradict H; discriminate. } - apply C; auto. - *)(* - (* longofintu *) econstructor; split. - eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. - split; intros; Simpl. (* unfold Pregmap.set; Simpl. *) destruct (PregEq.eq x0 x0). - + destruct (rs x0); auto. simpl. - assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto. - rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal. - rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. - + contradict n. auto. *) + + apply exec_straight_one. simpl. eauto. + + split. + * rewrite Pregmap.gss. + subst v. + destruct (rs x0); simpl; trivial. + unfold Val.maketotal. + destruct (Int.ltu _ _); simpl; trivial. + * intros. + rewrite Pregmap.gso; trivial. - (* Oshrxlimm *) - clear H. exploit Val.shrxl_shrl_2; eauto. intros E; subst v; clear EV. - destruct (Int.eq n Int.zero). -+ econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros; Simpl. -+ change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). econstructor; split. - eapply exec_straight_step. simpl; reflexivity. - eapply exec_straight_step. simpl; reflexivity. - eapply exec_straight_step. simpl; reflexivity. - apply exec_straight_one. simpl; reflexivity. - - split; intros; Simpl. + + apply exec_straight_one. simpl. eauto. + + split. + * rewrite Pregmap.gss. + subst v. + destruct (rs x0); simpl; trivial. + unfold Val.maketotal. + destruct (Int.ltu _ _); simpl; trivial. + * intros. + rewrite Pregmap.gso; trivial. - (* Ocmp *) exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 13ff5422..cf827818 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -25,6 +25,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. +Require Import ExtValues. Require Import Memory. Require Import Events. Require Import Globalenvs. @@ -309,7 +310,9 @@ Inductive arith_name_rr : Type := (* | Pextfs (stop : int) (start : int) (**r extract bit field, signed *) *) | Pextfz (stop : Z) (start : Z) (**r extract bit field, unsigned *) | Pextfs (stop : Z) (start : Z) (**r extract bit field, signed *) - + | Pextfzl (stop : Z) (start : Z) (**r extract bit field, unsigned *) + | Pextfsl (stop : Z) (start : Z) (**r extract bit field, signed *) + | Pfabsd (**r float absolute double *) | Pfabsw (**r float absolute word *) | Pfnegd (**r float negate double *) @@ -319,9 +322,7 @@ Inductive arith_name_rr : Type := | Pfloatwrnsz (**r Floating Point conversion from integer (int -> SINGLE) *) | Pfloatuwrnsz (**r Floating Point conversion from integer (unsigned int -> SINGLE) *) | Pfloatudrnsz (**r Floating Point Conversion from integer (unsigned long -> float) *) - | Pfloatudrnsz_i32 (**r Floating Point Conversion from integer (unsigned int -> float) *) | Pfloatdrnsz (**r Floating Point Conversion from integer (long -> float) *) - | Pfloatdrnsz_i32 (**r Floating Point Conversion from integer (int -> float) *) | Pfixedwrzz (**r Integer conversion from floating point (single -> int) *) | Pfixeduwrzz (**r Integer conversion from floating point (single -> unsigned int) *) | Pfixeddrzz (**r Integer conversion from floating point (float -> long) *) @@ -364,6 +365,7 @@ Inductive arith_name_rrr : Type := | Pandnw (**r andn word *) | Pornw (**r orn word *) | Psraw (**r shift right arithmetic word *) + | Psrxw (**r shift right arithmetic word round to 0*) | Psrlw (**r shift right logical word *) | Psllw (**r shift left logical word *) @@ -380,6 +382,7 @@ Inductive arith_name_rrr : Type := | Pmull (**r mul long (low part) *) | Pslll (**r shift left logical long *) | Psrll (**r shift right logical long *) + | Psrxl (**r shift right logical long round to 0*) | Psral (**r shift right arithmetic long *) | Pfaddd (**r float add double *) @@ -404,12 +407,14 @@ Inductive arith_name_rri32 : Type := | Pandniw (**r andn word *) | Porniw (**r orn word *) | Psraiw (**r shift right arithmetic imm word *) + | Psrxiw (**r shift right arithmetic imm word round to 0*) | Psrliw (**r shift right logical imm word *) | Pslliw (**r shift left logical imm word *) | Proriw (**r rotate right imm word *) | Psllil (**r shift left logical immediate long *) | Psrlil (**r shift right logical immediate long *) | Psrail (**r shift right arithmetic immediate long *) + | Psrxil (**r shift right arithmetic immediate long round to 0*) . Inductive arith_name_rri64 : Type := @@ -441,6 +446,11 @@ Inductive arith_name_arri64 : Type := | Pmaddil (**r multiply add long *) . +Inductive arith_name_arr : Type := + | Pinsf (stop : Z) (start : Z) (**r insert bit field *) + | Pinsfl (stop : Z) (start : Z) (**r insert bit field *) +. + Inductive ar_instruction : Type := | PArithR (i: arith_name_r) (rd: ireg) | PArithRR (i: arith_name_rr) (rd rs: ireg) @@ -452,6 +462,7 @@ Inductive ar_instruction : Type := | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int) | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64) | PArithARRR (i: arith_name_arrr) (rd rs1 rs2: ireg) + | PArithARR (i: arith_name_arr) (rd rs: ireg) | PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int) | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64) . @@ -465,7 +476,8 @@ Coercion PArithRF64: arith_name_rf64 >-> Funclass. Coercion PArithRRR: arith_name_rrr >-> Funclass. Coercion PArithRRI32: arith_name_rri32 >-> Funclass. Coercion PArithRRI64: arith_name_rri64 >-> Funclass. -Coercion PArithARRR: arith_name_arrr >-> Funclass. +Coercion PArithARRR: arith_name_arrr >-> Funclass. +Coercion PArithARR: arith_name_arr >-> Funclass. Coercion PArithARRI32: arith_name_arri32 >-> Funclass. Coercion PArithARRI64: arith_name_arri64 >-> Funclass. @@ -881,8 +893,10 @@ Definition arith_eval_rr n v := | Pcvtl2w => Val.loword v | Psxwd => Val.longofint v | Pzxwd => Val.longofintu v - | Pextfz stop start => Val.extfz stop start v - | Pextfs stop start => Val.extfs stop start v + | Pextfz stop start => extfz stop start v + | Pextfs stop start => extfs stop start v + | Pextfzl stop start => extfzl stop start v + | Pextfsl stop start => extfsl stop start v | Pfnegd => Val.negf v | Pfnegw => Val.negfs v | Pfabsd => Val.absf v @@ -893,8 +907,6 @@ Definition arith_eval_rr n v := | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end - | Pfloatudrnsz_i32 => match Val.floatofintu v with Some f => f | _ => Vundef end - | Pfloatdrnsz_i32 => match Val.floatofint v with Some f => f | _ => Vundef end | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end @@ -944,6 +956,7 @@ Definition arith_eval_rrr n v1 v2 := | Psrlw => Val.shru v1 v2 | Psraw => Val.shr v1 v2 | Psllw => Val.shl v1 v2 + | Psrxw => ExtValues.val_shrx v1 v2 | Paddl => Val.addl v1 v2 | Psubl => Val.subl v1 v2 @@ -959,6 +972,7 @@ Definition arith_eval_rrr n v1 v2 := | Pslll => Val.shll v1 v2 | Psrll => Val.shrlu v1 v2 | Psral => Val.shrl v1 v2 + | Psrxl => ExtValues.val_shrxl v1 v2 | Pfaddd => Val.addf v1 v2 | Pfaddw => Val.addfs v1 v2 @@ -982,10 +996,12 @@ Definition arith_eval_rri32 n v i := | Pandniw => Val.and (Val.notint v) (Vint i) | Porniw => Val.or (Val.notint v) (Vint i) | Psraiw => Val.shr v (Vint i) + | Psrxiw => ExtValues.val_shrx v (Vint i) | Psrliw => Val.shru v (Vint i) | Pslliw => Val.shl v (Vint i) | Proriw => Val.ror v (Vint i) | Psllil => Val.shll v (Vint i) + | Psrxil => ExtValues.val_shrxl v (Vint i) | Psrlil => Val.shrlu v (Vint i) | Psrail => Val.shrl v (Vint i) end. @@ -1043,6 +1059,12 @@ Definition arith_eval_arrr n v1 v2 v3 := end end. +Definition arith_eval_arr n v1 v2 := + match n with + | Pinsf stop start => ExtValues.insf stop start v1 v2 + | Pinsfl stop start => ExtValues.insfl stop start v1 v2 + end. + Definition arith_eval_arri32 n v1 v2 v3 := match n with | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3)) @@ -1069,6 +1091,7 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset := | PArithRRI64 n d s i => rsw#d <- (arith_eval_rri64 n rsr#s i) | PArithARRR n d s1 s2 => rsw#d <- (arith_eval_arrr n rsr#d rsr#s1 rsr#s2) + | PArithARR n d s => rsw#d <- (arith_eval_arr n rsr#d rsr#s) | PArithARRI32 n d s i => rsw#d <- (arith_eval_arri32 n rsr#d rsr#s i) | PArithARRI64 n d s i => rsw#d <- (arith_eval_arri64 n rsr#d rsr#s i) end. diff --git a/mppa_k1c/DecBoolOps.v b/mppa_k1c/DecBoolOps.v new file mode 100644 index 00000000..7f6f7c87 --- /dev/null +++ b/mppa_k1c/DecBoolOps.v @@ -0,0 +1,15 @@ +Set Implicit Arguments. + +Theorem and_dec : forall A B C D : Prop, + { A } + { B } -> { C } + { D } -> + { A /\ C } + { (B /\ C) \/ (B /\ D) \/ (A /\ D) }. +Proof. + intros A B C D AB CD. + destruct AB; destruct CD. + - left. tauto. + - right. tauto. + - right. tauto. + - right. tauto. +Qed. + +
\ No newline at end of file diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v new file mode 100644 index 00000000..5d16b79c --- /dev/null +++ b/mppa_k1c/ExtValues.v @@ -0,0 +1,119 @@ +Require Import Coqlib. +Require Import Integers. +Require Import Values. + +Definition is_bitfield stop start := + (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int.zwordsize). + +Definition extfz stop start v := + if is_bitfield stop start + then + let stop' := Z.add stop Z.one in + match v with + | Vint w => + Vint (Int.shru (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start)))) + | _ => Vundef + end + else Vundef. + + +Definition extfs stop start v := + if is_bitfield stop start + then + let stop' := Z.add stop Z.one in + match v with + | Vint w => + Vint (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start)))) + | _ => Vundef + end + else Vundef. + +Definition zbitfield_mask stop start := + (Z.shiftl 1 (Z.succ stop)) - (Z.shiftl 1 start). + +Definition bitfield_mask stop start := + Vint(Int.repr (zbitfield_mask stop start)). + +Definition bitfield_maskl stop start := + Vlong(Int64.repr (zbitfield_mask stop start)). + +Definition insf stop start prev fld := + let mask := bitfield_mask stop start in + if is_bitfield stop start + then + Val.or (Val.and prev (Val.notint mask)) + (Val.and (Val.shl fld (Vint (Int.repr start))) mask) + else Vundef. + +Definition is_bitfieldl stop start := + (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int64.zwordsize). + +Definition extfzl stop start v := + if is_bitfieldl stop start + then + let stop' := Z.add stop Z.one in + match v with + | Vlong w => + 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. + + +Definition extfsl stop start v := + if is_bitfieldl stop start + then + let stop' := Z.add stop Z.one in + match v with + | Vlong w => + 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. + +Definition insfl stop start prev fld := + let mask := bitfield_maskl stop start in + if is_bitfieldl stop start + then + Val.orl (Val.andl prev (Val.notl mask)) + (Val.andl (Val.shll fld (Vint (Int.repr start))) mask) + else Vundef. + +Fixpoint highest_bit (x : Z) (n : nat) : Z := + match n with + | O => 0 + | S n1 => + let n' := Z.of_N (N_of_nat n) in + if Z.testbit x n' + then n' + else highest_bit x n1 + end. + +Definition int_highest_bit (x : int) : Z := + highest_bit (Int.unsigned x) (31%nat). + + +Definition int64_highest_bit (x : int64) : Z := + highest_bit (Int64.unsigned x) (63%nat). + +Definition val_shrx (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 31) + then Vint(Int.shrx n1 n2) + else Vundef + | _, _ => Vundef + end. + +Definition val_shrxl (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vint n2 => + if Int.ltu n2 (Int.repr 63) + then Vlong(Int64.shrx' n1 n2) + else Vundef + | _, _ => Vundef + end. diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 06758756..ee85fb1c 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -210,7 +210,9 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => true + | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ + | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ + | Oinsf _ _ | Oinsfl _ _ => true | _ => false end. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 3a27df6a..c10f5c56 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -112,13 +112,14 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Onegfs | Oabsfs => op1 (default nv) | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) | Ofloatofsingle | Osingleoffloat => op1 (default nv) - | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv) + | Ointoffloat | Ointuoffloat => op1 (default nv) | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => op1 (default nv) | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | 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) + | Oinsf _ _ | Oinsfl _ _ => op2 (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..baf17cc0 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -31,7 +31,7 @@ Require Import BoolEqual Coqlib. Require Import AST Integers Floats. -Require Import Values Memory Globalenvs Events. +Require Import Values ExtValues Memory Globalenvs Events. Set Implicit Arguments. @@ -178,8 +178,6 @@ Inductive operation : Type := (*c Conversions between int and float: *) | Ointoffloat (**r [rd = signed_int_of_float64(r1)] *) | Ointuoffloat (**r [rd = unsigned_int_of_float64(r1)] *) - | Ofloatofint (**r [rd = float64_of_signed_int(r1)] *) - | Ofloatofintu (**r [rd = float64_of_unsigned_int(r1)] *) | Ointofsingle (**r [rd = signed_int_of_float32(r1)] *) | Ointuofsingle (**r [rd = unsigned_int_of_float32(r1)] *) | Osingleofint (**r [rd = float32_of_signed_int(r1)] *) @@ -199,7 +197,11 @@ 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) + | Oinsf (stop : Z) (start : Z) + | Oinsfl (stop : Z) (start : Z). (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -481,8 +483,6 @@ Definition eval_operation | Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1) | Ointoffloat, v1::nil => Val.intoffloat v1 | Ointuoffloat, v1::nil => Val.intuoffloat v1 - | Ofloatofint, v1::nil => Val.floatofint v1 - | Ofloatofintu, v1::nil => Val.floatofintu v1 | Ointofsingle, v1::nil => Val.intofsingle v1 | Ointuofsingle, v1::nil => Val.intuofsingle v1 | Osingleofint, v1::nil => Val.singleofint v1 @@ -500,8 +500,12 @@ Definition eval_operation | (Oselectl cond), v0::v1::vselect::nil => Some (eval_selectl cond v0 v1 vselect m) | (Oselectf cond), v0::v1::vselect::nil => Some (eval_selectf cond v0 v1 vselect m) | (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) + | (Oextfz stop start), v0::nil => Some (extfz stop start v0) + | (Oextfs stop start), v0::nil => Some (extfs stop start v0) + | (Oextfzl stop start), v0::nil => Some (extfzl stop start v0) + | (Oextfsl stop start), v0::nil => Some (extfsl stop start v0) + | (Oinsf stop start), v0::v1::nil => Some (insf stop start v0 v1) + | (Oinsfl stop start), v0::v1::nil => Some (insfl stop start v0 v1) | _, _ => None end. @@ -675,8 +679,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ofloatofsingle => (Tsingle :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) | Ointuoffloat => (Tfloat :: nil, Tint) - | Ofloatofint => (Tint :: nil, Tfloat) - | Ofloatofintu => (Tint :: nil, Tfloat) | Ointofsingle => (Tsingle :: nil, Tint) | Ointuofsingle => (Tsingle :: nil, Tint) | Osingleofint => (Tint :: nil, Tsingle) @@ -696,6 +698,9 @@ 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) + | Oinsf _ _ => (Tint :: Tint :: nil, Tint) + | Oinsfl _ _ => (Tlong :: Tlong :: nil, Tlong) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -908,9 +913,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* intoffloat, intuoffloat *) - destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2... - destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2... - (* floatofint, floatofintu *) - - destruct v0; simpl in H0; inv H0... - - destruct v0; simpl in H0; inv H0... (* intofsingle, intuofsingle *) - destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); inv H2... - destruct v0; simpl in H0; inv H0. destruct (Float32.to_intu f); inv H2... @@ -969,15 +971,37 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). destruct (_ && _); simpl; trivial. destruct (Val.cmp_different_blocks _); simpl; trivial. (* extfz *) - - unfold Val.extfz. - destruct (_ && _ && _). + - unfold extfz. + destruct (is_bitfield _ _). + destruct v0; simpl; trivial. + constructor. (* extfs *) - - unfold Val.extfs. - destruct (_ && _ && _). + - unfold extfs. + destruct (is_bitfield _ _). + + destruct v0; simpl; trivial. + + constructor. + (* extfzl *) + - unfold extfzl. + destruct (is_bitfieldl _ _). + + destruct v0; simpl; trivial. + + constructor. + (* extfsl *) + - unfold extfsl. + destruct (is_bitfieldl _ _). + destruct v0; simpl; trivial. + constructor. + (* insf *) + - unfold insf, bitfield_mask. + destruct (is_bitfield _ _). + + destruct v0; destruct v1; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + + constructor. + (* insf *) + - unfold insfl, bitfield_mask. + destruct (is_bitfieldl _ _). + + destruct v0; destruct v1; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + + constructor. Qed. End SOUNDNESS. @@ -1499,9 +1523,6 @@ Proof. exists (Vint i); auto. - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2. exists (Vint i); auto. - (* floatofint, floatofintu *) - - inv H4; simpl in H1; inv H1. simpl. TrivialExists. - - inv H4; simpl in H1; inv H1. simpl. TrivialExists. (* intofsingle, intuofsingle *) - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2. exists (Vint i); auto. @@ -1589,16 +1610,44 @@ Proof. * rewrite Hcond'. constructor. (* extfz *) - - unfold Val.extfz. - destruct (_ && _ && _). + - unfold extfz. + destruct (is_bitfield _ _). + inv H4; trivial. + trivial. (* extfs *) - - unfold Val.extfs. - destruct (_ && _ && _). + - unfold extfs. + destruct (is_bitfield _ _). + inv H4; trivial. + trivial. + + (* extfzl *) + - unfold extfzl. + destruct (is_bitfieldl _ _). + + inv H4; trivial. + + trivial. + + (* extfsl *) + - unfold extfsl. + destruct (is_bitfieldl _ _). + + inv H4; trivial. + + trivial. + + (* insf *) + - unfold insf. + destruct (is_bitfield _ _). + + inv H4; inv H2; trivial. + simpl. destruct (Int.ltu _ _); trivial. + simpl. trivial. + + trivial. + + (* insfl *) + - unfold insfl. + destruct (is_bitfieldl _ _). + + inv H4; inv H2; trivial. + simpl. destruct (Int.ltu _ _); trivial. + simpl. trivial. + + trivial. Qed. Lemma eval_addressing_inj: diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 41a5454b..b63dcb6c 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -36,6 +36,8 @@ let arith_rr_str = function | Pzxwd -> "Pzxwd" | Pextfz(_,_) -> "Pextfz" | Pextfs(_,_) -> "Pextfs" + | Pextfzl(_,_) -> "Pextfzl" + | Pextfsl(_,_) -> "Pextfsl" | Pfabsw -> "Pfabsw" | Pfabsd -> "Pfabsd" | Pfnegw -> "Pfnegw" @@ -44,10 +46,8 @@ let arith_rr_str = function | Pfwidenlwd -> "Pfwidenlwd" | Pfloatwrnsz -> "Pfloatwrnsz" | Pfloatuwrnsz -> "Pfloatuwrnsz" - | Pfloatudrnsz_i32 -> "Pfloatudrnsz_i32" | Pfloatudrnsz -> "Pfloatudrnsz" | Pfloatdrnsz -> "Pfloatdrnsz" - | Pfloatdrnsz_i32 -> "Pfloatdrnsz_i32" | Pfixedwrzz -> "Pfixedwrzz" | Pfixeduwrzz -> "Pfixeduwrzz" | Pfixeddrzz -> "Pfixeddrzz" @@ -73,6 +73,7 @@ let arith_rrr_str = function | Pornw -> "Pornw" | Psraw -> "Psraw" | Psrlw -> "Psrlw" + | Psrxw -> "Psrxw" | Psllw -> "Psllw" | Paddl -> "Paddl" | Psubl -> "Psubl" @@ -87,6 +88,7 @@ let arith_rrr_str = function | Pmull -> "Pmull" | Pslll -> "Pslll" | Psrll -> "Psrll" + | Psrxl -> "Psrxl" | Psral -> "Psral" | Pfaddd -> "Pfaddd" | Pfaddw -> "Pfaddw" @@ -108,12 +110,14 @@ let arith_rri32_str = function | Pandniw -> "Pandniw" | Porniw -> "Porniw" | Psraiw -> "Psraiw" + | Psrxiw -> "Psrxiw" | Psrliw -> "Psrliw" | Pslliw -> "Pslliw" | Proriw -> "Proriw" | Psllil -> "Psllil" | Psrlil -> "Psrlil" | Psrail -> "Psrail" + | Psrxil -> "Psrxil" let arith_rri64_str = function | Pcompil it -> "Pcompil" @@ -128,6 +132,11 @@ let arith_rri64_str = function | Pandnil -> "Pandnil" | Pornil -> "Pornil" + +let arith_arr_str = function + | Pinsf (_, _) -> "Pinsf" + | Pinsfl (_, _) -> "Pinsfl" + let arith_arrr_str = function | Pmaddw -> "Pmaddw" | Pmaddl -> "Pmaddl" @@ -177,6 +186,8 @@ let arith_arri32_rec i rd rs imm32 = { inst = "Pmaddiw"; write_locs = [Reg rd]; let arith_arri64_rec i rd rs imm64 = { inst = "Pmaddil"; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm64; is_control = false } +let arith_arr_rec i rd rs = { inst = arith_arr_str i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = None; is_control = false} + let arith_arrr_rec i rd rs1 rs2 = { inst = arith_arrr_str i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs1; Reg rs2]; imm = None; is_control = false} let arith_rr_rec i rd rs = { inst = arith_rr_str i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = None; is_control = false} @@ -190,6 +201,7 @@ let arith_rec i = | PArithRRI32 (i, rd, rs, imm32) -> arith_rri32_rec i (IR rd) (IR rs) (Some (I32 imm32)) | PArithRRI64 (i, rd, rs, imm64) -> arith_rri64_rec i (IR rd) (IR rs) (Some (I64 imm64)) | PArithRRR (i, rd, rs1, rs2) -> arith_rrr_rec i (IR rd) (IR rs1) (IR rs2) + | PArithARR (i, rd, rs) -> arith_arr_rec i (IR rd) (IR rs) (* Seems like single constant constructor types are elided *) | PArithARRI32 ((* i,*) rd, rs, imm32) -> arith_arri32_rec () (IR rd) (IR rs) (Some (I32 imm32)) | PArithARRI64 ((* i,*) rd, rs, imm64) -> arith_arri64_rec () (IR rd) (IR rs) (Some (I64 imm64)) @@ -422,11 +434,11 @@ let lsu_data_y : int array = let resmap = fun r -> match r with type real_instruction = (* ALU *) - | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw - | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord + | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Srsw | Rorw | Xorw + | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Srsd | Xord | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd | Maddw | Maddd | Cmoved - | Make | Nop | Extfz | Extfs + | Make | Nop | Extfz | Extfs | Insf (* LSU *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Sb | Sh | Sw | Sd @@ -459,6 +471,8 @@ let ab_inst_to_real = function | "Psubl" | "Pnegl" -> Sbfd | "Psraw" | "Psraiw" -> Sraw | "Psral" | "Psrail" -> Srad + | "Psrxw" | "Psrxiw" -> Srsw + | "Psrxl" | "Psrxil" -> Srsd | "Psrlw" | "Psrliw" -> Srlw | "Psrll" | "Psrlil" -> Srld | "Psllw" | "Pslliw" -> Sllw @@ -476,18 +490,15 @@ let ab_inst_to_real = function | "Pmaddl" -> Maddd | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make | "Pnop" | "Pcvtw2l" -> Nop - | "Psxwd" -> Extfs - | "Pzxwd" -> Extfz - | "Pextfz" -> Extfz - | "Pextfs" -> Extfs + | "Pextfz" | "Pextfzl" | "Pzxwd" -> Extfz + | "Pextfs" | "Pextfsl" | "Psxwd" -> Extfs + | "Pinsf" | "Pinsfl" -> Insf | "Pfnarrowdw" -> Fnarrowdw | "Pfwidenlwd" -> Fwidenlwd | "Pfloatwrnsz" -> Floatwz | "Pfloatuwrnsz" -> Floatuwz | "Pfloatdrnsz" -> Floatdz - | "Pfloatdrnsz_i32" -> Floatdz | "Pfloatudrnsz" -> Floatudz - | "Pfloatudrnsz_i32" -> Floatudz | "Pfixedwrzz" -> Fixedwz | "Pfixeduwrzz" -> Fixeduwz | "Pfixeddrzz" -> Fixeddz @@ -571,10 +582,10 @@ let rec_to_usage r = | Some U27L5 | Some U27L10 -> mau_x | Some E27U27L10 -> mau_y) | Nop -> alu_nop - | Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding) + | Sraw | Srlw | Srsw | Sllw | Srad | Srld | Slld | Srsd -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding) (* TODO: check *) | Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding) - | Extfz | Extfs -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding) + | Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding) | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> (match encoding with None | Some U6 | Some S10 -> lsu_data @@ -592,12 +603,12 @@ let rec_to_usage r = let real_inst_to_latency = function | Nop -> 0 (* Only goes through ID *) - | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw + | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srsw | Srlw | Sllw | Xorw (* TODO check rorw *) | Rorw | Nandw | Norw | Nxorw | Ornw | Andnw | Nandd | Nord | Nxord | Ornd | Andnd - | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make - | Extfs | Extfz | Fcompw | Fcompd | Cmoved + | Addd | Andd | Compd | Ord | Sbfd | Srad | Srsd | Srld | Slld | Xord | Make + | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved -> 1 | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) diff --git a/mppa_k1c/PrintOp.ml b/mppa_k1c/PrintOp.ml index 5ac00404..4b833014 100644 --- a/mppa_k1c/PrintOp.ml +++ b/mppa_k1c/PrintOp.ml @@ -141,8 +141,6 @@ let print_operation reg pp = function | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1 - | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 - | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1 | Olongoffloat, [r1] -> fprintf pp "longoffloat(%a)" reg r1 | Olonguoffloat, [r1] -> fprintf pp "longuoffloat(%a)" reg r1 | Ofloatoflong, [r1] -> fprintf pp "floatoflong(%a)" reg r1 diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 811a8ab1..3b9e5bf9 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -23,6 +23,8 @@ Require Import AST Integers Floats. Require Import Op CminorSel. Require Import OpHelpers. Require Import SelectOp SplitLong. +Require Import ExtValues. +Require Import DecBoolOps. Local Open Scope cminorsel_scope. Local Open Scope string_scope. @@ -155,6 +157,12 @@ 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 is_bitfieldl stop start + then Eop (Oextfzl stop start) (t1:::Enil) + else Eop (Oshrluimm n) (e1:::Enil) | _ => Eop (Oshrluimm n) (e1:::Enil) end. @@ -172,6 +180,12 @@ 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 is_bitfieldl stop start + then Eop (Oextfsl stop start) (t1:::Enil) + else Eop (Oshrlimm n) (e1:::Enil) | _ => Eop (Oshrlimm n) (e1:::Enil) end. @@ -298,6 +312,31 @@ Nondetfunction orl (e1: expr) (e2: expr) := && Int64.eq zero1 Int64.zero then Eop (Oselectl (Ccompl0 Cne)) (v0:::v1:::y0:::Enil) else Eop Oorl (e1:::e2:::Enil) + | (Eop (Oandlimm nmask) (prev:::Enil)), + (Eop (Oandlimm mask) + ((Eop (Oshllimm start) (fld:::Enil)):::Enil)) => + let zstart := Int.unsigned start in + let zstop := int64_highest_bit mask in + if is_bitfieldl zstop zstart + then + let mask' := Int64.repr (zbitfield_mask zstop zstart) in + if and_dec (Int64.eq_dec mask mask') + (Int64.eq_dec nmask (Int64.not mask')) + then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil) + else Eop Oorl (e1:::e2:::Enil) + else Eop Oorl (e1:::e2:::Enil) + | (Eop (Oandlimm nmask) (prev:::Enil)), + (Eop (Oandlimm mask) (fld:::Enil)) => + let zstart := 0 in + let zstop := int64_highest_bit mask in + if is_bitfieldl zstop zstart + then + let mask' := Int64.repr (zbitfield_mask zstop zstart) in + if and_dec (Int64.eq_dec mask mask') + (Int64.eq_dec nmask (Int64.not mask')) + then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil) + else Eop Oorl (e1:::e2:::Enil) + else Eop Oorl (e1:::e2:::Enil) | _, _ => Eop Oorl (e1:::e2:::Enil) end. @@ -408,3 +447,7 @@ Definition singleoflong (e: expr) := SplitLong.singleoflong e. Definition singleoflongu (e: expr) := SplitLong.singleoflongu e. End SELECT. + +(* Local Variables: *) +(* mode: coq *) +(* End: *)
\ No newline at end of file diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 3fa35331..cf8eed2b 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -19,11 +19,12 @@ Require Import String Coqlib Maps Integers Floats Errors. Require Archi. -Require Import AST Values Memory Globalenvs Events. +Require Import AST Values ExtValues Memory Globalenvs Events. Require Import Cminor Op CminorSel. Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. +Require Import DecBoolOps. Local Open Scope cminorsel_scope. Local Open Scope string_scope. @@ -238,7 +239,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 +249,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 (is_bitfieldl _ _) eqn:BOUNDS. + + exists (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 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 +291,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 +301,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 (is_bitfieldl _ _) eqn:BOUNDS. + + exists (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 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. @@ -528,6 +589,61 @@ Proof. rewrite Int64.and_zero. rewrite Int64.or_zero. reflexivity. + + - (*insfl first case*) + destruct (is_bitfieldl _ _) eqn:Risbitfield. + + destruct (and_dec _ _) as [[Rmask Rnmask] | ]. + * rewrite Rnmask in *. + inv H. inv H0. inv H4. inv H3. inv H9. inv H8. + simpl in H6, H7. + inv H6. inv H7. + inv H4. inv H3. inv H7. + simpl in H6. + inv H6. + set (zstop := (int64_highest_bit mask)) in *. + set (zstart := (Int.unsigned start)) in *. + + TrivialExists. + simpl. f_equal. + + unfold insfl. + rewrite Risbitfield. + rewrite Rmask. + simpl. + unfold bitfield_maskl. + subst zstart. + rewrite Int.repr_unsigned. + reflexivity. + * TrivialExists. + + TrivialExists. + - destruct (is_bitfieldl _ _) eqn:Risbitfield. + + destruct (and_dec _ _) as [[Rmask Rnmask] | ]. + * rewrite Rnmask in *. + inv H. inv H0. inv H4. inv H6. inv H8. inv H3. inv H8. + inv H0. simpl in H7. inv H7. + set (zstop := (int64_highest_bit mask)) in *. + set (zstart := 0) in *. + + TrivialExists. simpl. f_equal. + unfold insfl. + rewrite Risbitfield. + rewrite Rmask. + simpl. + subst zstart. + f_equal. + destruct v0; simpl; trivial. + unfold Int.ltu, Int64.iwordsize', Int64.zwordsize, Int64.wordsize. + rewrite Int.unsigned_repr. + ** rewrite Int.unsigned_repr. + *** simpl. + rewrite Int64.shl'_zero. + reflexivity. + *** simpl. unfold Int.max_unsigned. unfold Int.modulus. + simpl. omega. + ** unfold Int.max_unsigned. unfold Int.modulus. + simpl. omega. + * TrivialExists. + + TrivialExists. - TrivialExists. Qed. diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 6bb5ee56..25f09e2e 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -51,6 +51,8 @@ Require Import Floats. Require Import Op. Require Import CminorSel. Require Import OpHelpers. +Require Import ExtValues. +Require Import DecBoolOps. Local Open Scope cminorsel_scope. @@ -189,9 +191,7 @@ Nondetfunction shruimm (e1: expr) (n: int) := | Eop (Oshlimm n1) (t1:::Enil) => let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) + if is_bitfield stop start then Eop (Oextfz stop start) (t1:::Enil) else Eop (Oshruimm n) (e1:::Enil) | _ => @@ -213,9 +213,7 @@ Nondetfunction shrimm (e1: expr) (n: int) := | Eop (Oshlimm n1) (t1:::Enil) => let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) + if is_bitfield stop start then Eop (Oextfs stop start) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil) | _ => @@ -339,6 +337,31 @@ Nondetfunction or (e1: expr) (e2: expr) := && Int.eq zero1 Int.zero then select_base v0 v1 y0 else Eop Oor (e1:::e2:::Enil) + | (Eop (Oandimm nmask) (prev:::Enil)), + (Eop (Oandimm mask) + ((Eop (Oshlimm start) (fld:::Enil)):::Enil)) => + let zstart := Int.unsigned start in + let zstop := int_highest_bit mask in + if is_bitfield zstop zstart + then + let mask' := Int.repr (zbitfield_mask zstop zstart) in + if and_dec (Int.eq_dec mask mask') + (Int.eq_dec nmask (Int.not mask')) + then Eop (Oinsf zstop zstart) (prev:::fld:::Enil) + else Eop Oor (e1:::e2:::Enil) + else Eop Oor (e1:::e2:::Enil) + | (Eop (Oandimm nmask) (prev:::Enil)), + (Eop (Oandimm mask) (fld:::Enil)) => + let zstart := 0 in + let zstop := int_highest_bit mask in + if is_bitfield zstop zstart + then + let mask' := Int.repr (zbitfield_mask zstop zstart) in + if and_dec (Int.eq_dec mask mask') + (Int.eq_dec nmask (Int.not mask')) + then Eop (Oinsf zstop zstart) (prev:::fld:::Enil) + else Eop Oor (e1:::e2:::Enil) + else Eop Oor (e1:::e2:::Enil) | _, _ => Eop Oor (e1:::e2:::Enil) end. @@ -535,13 +558,13 @@ Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). Nondetfunction floatofintu (e: expr) := match e with | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil - | _ => Eop Ofloatofintu (e ::: Enil) + | _ => Eop Ofloatoflongu ((Eop Ocast32unsigned (e ::: Enil)) ::: Enil) end. Nondetfunction floatofint (e: expr) := match e with | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil - | _ => Eop Ofloatofint (e ::: Enil) + | _ => Eop Ofloatoflong ((Eop Ocast32signed (e ::: Enil)) ::: Enil) end. Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil). @@ -593,3 +616,7 @@ Definition divfs_base (e1: expr) (e2: expr) := (* Eop Odivf (e1 ::: e2 ::: Enil). *) Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil). End SELECT. + +(* Local Variables: *) +(* mode: coq *) +(* End: *)
\ No newline at end of file diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 4df87bea..6fa93fd8 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -23,6 +23,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. +Require Import ExtValues. Require Import Memory. Require Import Globalenvs. Require Import Cminor. @@ -32,6 +33,7 @@ Require Import SelectOp. Require Import Events. Require Import OpHelpers. Require Import OpHelpersproof. +Require Import DecBoolOps. Local Open Scope cminorsel_scope. Local Open Scope string_scope. @@ -310,15 +312,15 @@ Proof. - subst x. simpl negb. cbn iota. - destruct (_ && _ && _) eqn:BOUNDS. - + exists (Val.extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) + destruct (is_bitfield _ _) eqn:BOUNDS. + + exists (extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) (Z.sub (Z.add (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))) Z.one) Int.zwordsize) v1). split. ++ EvalOp. - ++ unfold Val.extfz. + ++ unfold extfz. rewrite BOUNDS. destruct v1; try (simpl; apply Val.lessdef_undef). replace (Z.sub Int.zwordsize @@ -367,15 +369,15 @@ Proof. - subst x. simpl negb. cbn iota. - destruct (_ && _ && _) eqn:BOUNDS. - + exists (Val.extfs (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) + destruct (is_bitfield _ _) eqn:BOUNDS. + + exists (extfs (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) (Z.sub (Z.add (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))) Z.one) Int.zwordsize) v1). split. ++ EvalOp. - ++ unfold Val.extfs. + ++ unfold extfs. rewrite BOUNDS. destruct v1; try (simpl; apply Val.lessdef_undef). replace (Z.sub Int.zwordsize @@ -699,6 +701,58 @@ Proof. rewrite Int.or_commut. rewrite Int.or_zero. reflexivity. + - set (zstop := (int_highest_bit mask)). + set (zstart := (Int.unsigned start)). + destruct (is_bitfield _ _) eqn:Risbitfield. + + destruct (and_dec _ _) as [[Rmask Rnmask] | ]. + * simpl in H6. + injection H6. + clear H6. + intro. subst y. subst x. + TrivialExists. simpl. f_equal. + unfold insf. + rewrite Risbitfield. + rewrite Rmask. + rewrite Rnmask. + simpl. + unfold bitfield_mask. + subst v0. + subst zstart. + rewrite Int.repr_unsigned. + reflexivity. + * apply DEFAULT. + + apply DEFAULT. + - set (zstop := (int_highest_bit mask)). + set (zstart := 0). + destruct (is_bitfield _ _) eqn:Risbitfield. + + destruct (and_dec _ _) as [[Rmask Rnmask] | ]. + * subst y. subst x. + TrivialExists. simpl. f_equal. + unfold insf. + rewrite Risbitfield. + rewrite Rmask. + rewrite Rnmask. + simpl. + unfold bitfield_mask. + subst zstart. + rewrite (Val.or_commut (Val.and v1 _)). + rewrite (Val.or_commut (Val.and v1 _)). + destruct v0; simpl; trivial. + unfold Int.ltu, Int.iwordsize, Int.zwordsize. + rewrite Int.unsigned_repr. + ** rewrite Int.unsigned_repr. + *** simpl. + rewrite Int.shl_zero. + reflexivity. + *** simpl. + unfold Int.max_unsigned, Int.modulus. + simpl. + omega. + ** unfold Int.max_unsigned, Int.modulus. + simpl. + omega. + * apply DEFAULT. + + apply DEFAULT. - apply DEFAULT. Qed. @@ -1101,9 +1155,23 @@ Theorem eval_floatofintu: Val.floatofintu x = Some y -> exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v. Proof. - intros until y; unfold floatofintu. case (floatofintu_match a); intros. - InvEval. simpl in H0. TrivialExists. - TrivialExists. + intros. + unfold Val.floatofintu in *. + unfold floatofintu. + destruct (floatofintu_match a). + - InvEval. + TrivialExists. + - InvEval. + TrivialExists. + constructor. econstructor. constructor. eassumption. constructor. + simpl. f_equal. constructor. + simpl. + destruct x; simpl; trivial. + f_equal. + inv H0. + f_equal. + rewrite Float.of_intu_of_longu. + reflexivity. Qed. Theorem eval_floatofint: @@ -1112,9 +1180,22 @@ Theorem eval_floatofint: Val.floatofint x = Some y -> exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v. Proof. - intros until y; unfold floatofint. case (floatofint_match a); intros. - InvEval. simpl in H0. TrivialExists. - TrivialExists. + intros. + unfold floatofint. + destruct (floatofint_match a). + - InvEval. + TrivialExists. + - InvEval. + TrivialExists. + constructor. econstructor. constructor. eassumption. constructor. + simpl. f_equal. constructor. + simpl. + destruct x; simpl; trivial. + f_equal. + inv H0. + f_equal. + rewrite Float.of_int_of_long. + reflexivity. Qed. Theorem eval_intofsingle: diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 8826e6a2..506faa1c 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -377,10 +377,12 @@ module Target (*: TARGET*) = fprintf oc " sxwd %a = %a\n" ireg rd ireg rs | Pzxwd(rd, rs) -> fprintf oc " zxwd %a = %a\n" ireg rd ireg rs - | Pextfz(rd, rs, stop, start) -> + | Pextfz(rd, rs, stop, start) | Pextfzl(rd, rs, stop, start) -> fprintf oc " extfz %a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start) - | Pextfs(rd, rs, stop, start) -> + | Pextfs(rd, rs, stop, start) | Pextfsl(rd, rs, stop, start) -> fprintf oc " extfs %a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start) + | Pinsf(rd, rs, stop, start) | Pinsfl(rd, rs, stop, start) -> + fprintf oc " insf %a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start) | Pfabsd(rd, rs) -> fprintf oc " fabsd %a = %a\n" ireg rd ireg rs | Pfabsw(rd, rs) -> @@ -399,12 +401,8 @@ module Target (*: TARGET*) = fprintf oc " floatw.rn.s %a = %a, 0\n" ireg rd ireg rs | Pfloatudrnsz(rd, rs) -> fprintf oc " floatud.rn.s %a = %a, 0\n" ireg rd ireg rs - | Pfloatudrnsz_i32(rd, rs) -> - fprintf oc " zxwd %a = %a\n # FIXME\n ;;\n floatud.rn.s %a = %a, 0\n" ireg rd ireg rs ireg rd ireg rd | Pfloatdrnsz(rd, rs) -> fprintf oc " floatd.rn.s %a = %a, 0\n" ireg rd ireg rs - | Pfloatdrnsz_i32(rd, rs) -> - fprintf oc " sxwd %a = %a\n # FIXME\n ;;\n floatd.rn.s %a = %a, 0\n" ireg rd ireg rs ireg rd ireg rd | Pfixedwrzz(rd, rs) -> fprintf oc " fixedw.rz %a = %a, 0\n" ireg rd ireg rs | Pfixeduwrzz(rd, rs) -> @@ -469,6 +467,8 @@ module Target (*: TARGET*) = fprintf oc " ornw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psraw (rd, rs1, rs2) -> fprintf oc " sraw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Psrxw (rd, rs1, rs2) -> + fprintf oc " srsw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psrlw (rd, rs1, rs2) -> fprintf oc " srlw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psllw (rd, rs1, rs2) -> @@ -502,6 +502,8 @@ module Target (*: TARGET*) = fprintf oc " slld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psrll (rd, rs1, rs2) -> fprintf oc " srld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Psrxl (rd, rs1, rs2) -> + fprintf oc " srsd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psral (rd, rs1, rs2) -> fprintf oc " srad %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pmaddl (rd, rs1, rs2) -> @@ -545,6 +547,8 @@ module Target (*: TARGET*) = fprintf oc " ornw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psraiw (rd, rs, imm) -> fprintf oc " sraw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Psrxiw (rd, rs, imm) -> + fprintf oc " srsw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psrliw (rd, rs, imm) -> fprintf oc " srlw %a = %a, %a\n" ireg rd ireg rs coqint imm | Pslliw (rd, rs, imm) -> @@ -560,6 +564,8 @@ module Target (*: TARGET*) = fprintf oc " srld %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Psrail (rd, rs, imm) -> fprintf oc " srad %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Psrxil (rd, rs, imm) -> + fprintf oc " srsd %a = %a, %a\n" ireg rd ireg rs coqint64 imm (* Arith RRI64 instructions *) | Pcompil (it, rd, rs, imm) -> diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 23514d21..064686cc 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -12,7 +12,7 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. -Require Import Op RTL ValueDomain. +Require Import Op ExtValues RTL ValueDomain. (** Value analysis for RISC V operators *) @@ -76,9 +76,7 @@ Definition eval_static_selectfs (cond : condition0) (v0 v1 vselect : aval) : ava Definition eval_static_extfs (stop : Z) (start : Z) (v : aval) := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) + if is_bitfield stop start then let stop' := Z.add stop Z.one in match v with @@ -89,9 +87,7 @@ Definition eval_static_extfs (stop : Z) (start : Z) (v : aval) := else Vtop. Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) + if is_bitfield stop start then let stop' := Z.add stop Z.one in match v with @@ -101,6 +97,56 @@ Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) := end else Vtop. +Definition eval_static_extfsl (stop : Z) (start : Z) (v : aval) := + if is_bitfieldl stop start + 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 is_bitfieldl stop start + 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_insf stop start prev fld := + let mask := Int.repr (zbitfield_mask stop start) in + if is_bitfield stop start + then + match prev, fld with + | (I prevI), (I fldI) => + if Int.ltu (Int.repr start) Int.iwordsize + then I (Int.or (Int.and prevI (Int.not mask)) + (Int.and (Int.shl fldI (Int.repr start)) mask)) + else Vtop + | _, _ => Vtop + end + else Vtop. + +Definition eval_static_insfl stop start prev fld := + let mask := Int64.repr (zbitfield_mask stop start) in + if is_bitfieldl stop start + then + match prev, fld with + | (L prevL), (L fldL) => + if Int.ltu (Int.repr start) Int64.iwordsize' + then L (Int64.or (Int64.and prevL (Int64.not mask)) + (Int64.and (Int64.shl' fldL (Int.repr start)) mask)) + else Vtop + | _,_ => Vtop + end + else Vtop. + Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -210,8 +256,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 | Ointuoffloat, v1::nil => intuoffloat v1 - | Ofloatofint, v1::nil => floatofint v1 - | Ofloatofintu, v1::nil => floatofintu v1 | Ointofsingle, v1::nil => intofsingle v1 | Ointuofsingle, v1::nil => intuofsingle v1 | Osingleofint, v1::nil => singleofint v1 @@ -231,6 +275,10 @@ 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 + | (Oinsf stop start), v0::v1::nil => eval_static_insf stop start v0 v1 + | (Oinsfl stop start), v0::v1::nil => eval_static_insfl stop start v0 v1 | _, _ => Vbot end. @@ -358,16 +406,39 @@ Proof. constructor. (* extfz *) - - unfold Val.extfz, eval_static_extfz. - destruct (_ && _ && _). + - unfold extfz, eval_static_extfz. + destruct (is_bitfield _ _). + inv H1; constructor. + constructor. (* extfs *) - - unfold Val.extfs, eval_static_extfs. - destruct (_ && _ && _). + - unfold extfs, eval_static_extfs. + destruct (is_bitfield _ _). + inv H1; constructor. + constructor. + + (* extfzl *) + - unfold extfzl, eval_static_extfzl. + destruct (is_bitfieldl _ _). + + inv H1; constructor. + + constructor. + + (* extfsl *) + - unfold extfsl, eval_static_extfsl. + destruct (is_bitfieldl _ _). + + inv H1; constructor. + + constructor. + + (* insf *) + - unfold insf, eval_static_insf. + destruct (is_bitfield _ _). + + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + constructor. + (* insfl *) + - unfold insfl, eval_static_insfl. + destruct (is_bitfieldl _ _). + + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + constructor. Qed. End SOUNDNESS. diff --git a/mppa_k1c/bitmasks.py b/mppa_k1c/bitmasks.py new file mode 100755 index 00000000..9f6987d6 --- /dev/null +++ b/mppa_k1c/bitmasks.py @@ -0,0 +1,12 @@ +#!/usr/bin/env python3 +def bitmask(to, fr): + bit_to = 1<<to + return (bit_to | (bit_to - 1)) & ~((1<<fr)-1) + +def bitmask2(to, fr): + bit_to = 1<<to + return bit_to + (bit_to - (1 << fr)) + +for stop in range(32): + for start in range(stop+1): + assert(bitmask(stop, start) == bitmask2(stop, start)) |