diff options
42 files changed, 1684 insertions, 379 deletions
diff --git a/common/Values.v b/common/Values.v index 059a72d9..127d1085 100644 --- a/common/Values.v +++ b/common/Values.v @@ -767,34 +767,6 @@ Definition rolml (v: val) (amount: int) (mask: int64): val := end. -Definition extfz stop start v := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) - 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 (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) - 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. - - (** Comparisons *) Section COMPARISONS. @@ -806,7 +806,7 @@ ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ - Asmblockdeps.v\\ + Asmblockdeps.v Chunks.v Peephole.v ExtValues.v\\ AbstractBasicBlocksDef.v DepTreeTheory.v ImpDep.v Parallelizability.v\\ ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v EOF diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 4d70d350..b1afab6f 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,7 +28,7 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true let option_fpostpass = ref true -let option_fpostpass_ilp = ref false +let option_fpostpass_sched = ref "list" let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 @@ -66,3 +66,8 @@ let option_small_const = ref (!option_small_data) let option_timings = ref false let stdlib_path = ref Configuration.stdlib_path let use_standard_headers = ref Configuration.has_standard_headers + +let option_fglobaladdrtmp = ref false +let option_fglobaladdroffset = ref false +let option_fxsaddr = ref true +let option_coalesce_mem = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index e6eecc9b..f7de596c 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -42,6 +42,18 @@ Parameter optim_redundancy: unit -> bool. (** Flag -fpostpass. Postpass scheduling for K1 architecture *) Parameter optim_postpass: unit -> bool. +(** FIXME TEMPORARY Flag -fglobaladdrtmp. Use a temporary register for loading the address of global variables (default false) *) +Parameter optim_fglobaladdrtmp: unit -> bool. + +(** FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses (default false) *) +Parameter optim_fglobaladdroffset: unit -> bool. + +(** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *) +Parameter optim_fxsaddr: unit -> bool. + +(** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *) +Parameter optim_coalesce_mem: unit -> bool. + (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index c68c066a..cfafcaa3 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,7 +194,8 @@ Processing options: -fcse Perform common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] - -fpostpass-ilp Use integer linear programming for postpass scheduling [off] + -fpostpass= <optim> Perform postpass scheduling with the specified optimization [list] + (<optim>=list: list scheduling, <optim>=ilp: ILP, <optim>=greedy: just packing bundles) -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] @@ -264,6 +265,10 @@ let num_input_files = ref 0 let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in + let f_opt_str name ref strref = + [Exact("-f" ^ name ^ "="), String + (fun s -> (strref := (if s == "" then "list" else s)); ref := true) + ] in [ (* Getting help *) Exact "-help", Unit print_usage_and_exit; @@ -364,9 +369,13 @@ let cmdline_actions = @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass - @ f_opt "postpass-ilp" option_fpostpass_ilp + @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once + @ f_opt "globaladdrtmp" option_fglobaladdrtmp + @ f_opt "globaladdroffset" option_fglobaladdroffset + @ f_opt "xsaddr" option_fxsaddr + @ f_opt "coalesce-mem" option_coalesce_mem (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) diff --git a/extraction/extraction.v b/extraction/extraction.v index f58991aa..979e1d49 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -117,6 +117,14 @@ Extract Constant Compopts.thumb => "fun _ -> !Clflags.option_mthumb". Extract Constant Compopts.debug => "fun _ -> !Clflags.option_g". +Extract Constant Compopts.optim_fglobaladdrtmp => + "fun _ -> !Clflags.option_fglobaladdrtmp". +Extract Constant Compopts.optim_fglobaladdroffset => + "fun _ -> !Clflags.option_fglobaladdroffset". +Extract Constant Compopts.optim_fxsaddr => + "fun _ -> !Clflags.option_fxsaddr". +Extract Constant Compopts.optim_coalesce_mem => + "fun _ -> !Clflags.option_coalesce_mem". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 1e1f6e36..8b1c9a81 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.
@@ -41,6 +42,7 @@ Definition preg := preg. Inductive addressing : Type :=
| AOff (ofs: offset)
| AReg (ro: ireg)
+ | ARegXS (ro: ireg)
.
(** Syntax *)
@@ -120,7 +122,9 @@ Inductive instruction : Type := | Psd (rs: ireg) (ra: ireg) (ofs: addressing) (**r store int64 *)
| Psd_a (rs: ireg) (ra: ireg) (ofs: addressing) (**r store any64 *)
| Pfss (rs: freg) (ra: ireg) (ofs: addressing) (**r store float *)
- | Pfsd (rd: freg) (ra: ireg) (ofs: addressing) (**r store 64-bit float *)
+ | Pfsd (rs: freg) (ra: ireg) (ofs: addressing) (**r store 64-bit float *)
+
+ | Psq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r store 64-bit float *)
(** Arith RR *)
| Pmv (rd rs: ireg) (**r register move *)
@@ -133,6 +137,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 +152,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 +190,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 +209,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 +233,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 +298,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 +310,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 +346,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 +364,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 +386,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 +414,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
@@ -427,6 +447,17 @@ Definition basic_to_instruction (b: basic) := | PLoadRRR Asmvliw.Pfls rd ra ro => Pfls rd ra (AReg ro)
| PLoadRRR Asmvliw.Pfld rd ra ro => Pfld rd ra (AReg ro)
+ | PLoadRRRXS Asmvliw.Plb rd ra ro => Plb rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Plbu rd ra ro => Plbu rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Plh rd ra ro => Plh rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Plhu rd ra ro => Plhu rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Plw rd ra ro => Plw rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Plw_a rd ra ro => Plw_a rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Pld rd ra ro => Pld rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Pld_a rd ra ro => Pld_a rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Pfls rd ra ro => Pfls rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Pfld rd ra ro => Pfld rd ra (ARegXS ro)
+
(** Store *)
| PStoreRRO Asmvliw.Psb rd ra ofs => Psb rd ra (AOff ofs)
| PStoreRRO Asmvliw.Psh rd ra ofs => Psh rd ra (AOff ofs)
@@ -446,6 +477,16 @@ Definition basic_to_instruction (b: basic) := | PStoreRRR Asmvliw.Pfss rd ra ro => Pfss rd ra (AReg ro)
| PStoreRRR Asmvliw.Pfsd rd ra ro => Pfsd rd ra (AReg ro)
+ | PStoreRRRXS Asmvliw.Psb rd ra ro => Psb rd ra (ARegXS ro)
+ | PStoreRRRXS Asmvliw.Psh rd ra ro => Psh rd ra (ARegXS ro)
+ | PStoreRRRXS Asmvliw.Psw rd ra ro => Psw rd ra (ARegXS ro)
+ | PStoreRRRXS Asmvliw.Psw_a rd ra ro => Psw_a rd ra (ARegXS ro)
+ | PStoreRRRXS Asmvliw.Psd rd ra ro => Psd rd ra (ARegXS ro)
+ | PStoreRRRXS Asmvliw.Psd_a rd ra ro => Psd_a rd ra (ARegXS ro)
+ | PStoreRRRXS Asmvliw.Pfss rd ra ro => Pfss rd ra (ARegXS ro)
+ | PStoreRRRXS Asmvliw.Pfsd rd ra ro => Pfsd rd ra (ARegXS ro)
+
+ | PStoreQRRO qrs ra ofs => Psq qrs ra (AOff ofs)
end.
Section RELSEM.
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index ed145f21..f2c4a382 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -264,14 +264,20 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := parexec (** Auxiliaries for memory accesses *) -Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := parexec_load_offset ge chunk rs rs m m d a ofs. +Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := parexec_load_offset chunk rs rs m m d a ofs. Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_reg chunk rs rs m m d a ro. -Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset ge chunk rs rs m m s a ofs. +Definition exec_load_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_regxs chunk rs rs m m d a ro. + +Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset chunk rs rs m m s a ofs. + +Definition exec_store_q_offset (rs: regset) (m: mem) (s : gpreg_q) (a: ireg) (ofs: offset) := parexec_store_q_offset rs rs m m s a ofs. Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_reg chunk rs rs m m s a ro. +Definition exec_store_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_regxs chunk rs rs m m s a ro. + (** * basic instructions *) Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := parexec_basic_instr ge bi rs rs m m. diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index b3a72517..52af8cdf 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -13,6 +13,7 @@ Require Import ImpDep. Require Import Axioms. Require Import Parallelizability. Require Import Asmvliw Permutation. +Require Import Chunks. Open Scope impure. @@ -57,6 +58,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) . @@ -74,6 +76,7 @@ Coercion OArithRRI64: arith_name_rri64 >-> Funclass. Inductive load_op := | OLoadRRO (n: load_name) (ofs: offset) | OLoadRRR (n: load_name) + | OLoadRRRXS (n: load_name) . Coercion OLoadRRO: load_name >-> Funclass. @@ -81,6 +84,7 @@ Coercion OLoadRRO: load_name >-> Funclass. Inductive store_op := | OStoreRRO (n: store_name) (ofs: offset) | OStoreRRR (n: store_name) + | OStoreRRRXS (n: store_name) . Coercion OStoreRRO: store_name >-> Funclass. @@ -121,6 +125,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)) @@ -130,7 +135,7 @@ Definition arith_eval (ao: arith_op) (l: list value) := Definition exec_load_deps_offset (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) := let (ge, fn) := Ge in - match (eval_offset ge ofs) with + match (eval_offset ofs) with | OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with | None => None | Some vl => Some (Val vl) @@ -144,16 +149,23 @@ Definition exec_load_deps_reg (chunk: memory_chunk) (m: mem) (v vo: val) := | Some vl => Some (Val vl) end. +Definition exec_load_deps_regxs (chunk: memory_chunk) (m: mem) (v vo: val) := + match Mem.loadv chunk m (Val.addl v (Val.shll vo (scale_of_chunk chunk))) with + | None => None + | Some vl => Some (Val vl) + end. + Definition load_eval (lo: load_op) (l: list value) := match lo, l with | OLoadRRO n ofs, [Val v; Memstate m] => exec_load_deps_offset (load_chunk n) m v ofs | OLoadRRR n, [Val v; Val vo; Memstate m] => exec_load_deps_reg (load_chunk n) m v vo + | OLoadRRRXS n, [Val v; Val vo; Memstate m] => exec_load_deps_regxs (load_chunk n) m v vo | _, _ => None end. Definition exec_store_deps_offset (chunk: memory_chunk) (m: mem) (vs va: val) (ofs: offset) := let (ge, fn) := Ge in - match (eval_offset ge ofs) with + match (eval_offset ofs) with | OK ptr => match Mem.storev chunk m (Val.offset_ptr va ptr) vs with | None => None | Some m' => Some (Memstate m') @@ -167,10 +179,17 @@ Definition exec_store_deps_reg (chunk: memory_chunk) (m: mem) (vs va vo: val) := | Some m' => Some (Memstate m') end. +Definition exec_store_deps_regxs (chunk: memory_chunk) (m: mem) (vs va vo: val) := + match Mem.storev chunk m (Val.addl va (Val.shll vo (scale_of_chunk chunk))) vs with + | None => None + | Some m' => Some (Memstate m') + end. + Definition store_eval (so: store_op) (l: list value) := match so, l with | OStoreRRO n ofs, [Val vs; Val va; Memstate m] => exec_store_deps_offset (store_chunk n) m vs va ofs | OStoreRRR n, [Val vs; Val va; Val vo; Memstate m] => exec_store_deps_reg (store_chunk n) m vs va vo + | OStoreRRRXS n, [Val vs; Val va; Val vo; Memstate m] => exec_store_deps_regxs (store_chunk n) m vs va vo | _, _ => None end. @@ -329,6 +348,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 => @@ -351,6 +372,8 @@ Definition load_op_eq (o1 o2: load_op): ?? bool := match o2 with OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end | OLoadRRR n1 => match o2 with OLoadRRR n2 => phys_eq n1 n2 | _ => RET false end + | OLoadRRRXS n1 => + match o2 with OLoadRRRXS n2 => phys_eq n1 n2 | _ => RET false end end. Lemma load_op_eq_correct o1 o2: @@ -359,23 +382,40 @@ Proof. destruct o1, o2; wlp_simplify; try discriminate. - congruence. - congruence. + - congruence. Qed. Hint Resolve load_op_eq_correct: wlp. Opaque load_op_eq_correct. +Definition offset_eq (ofs1 ofs2 : offset): ?? bool := + RET (Ptrofs.eq ofs1 ofs2). + +Lemma offset_eq_correct ofs1 ofs2: + WHEN offset_eq ofs1 ofs2 ~> b THEN b = true -> ofs1 = ofs2. +Proof. + wlp_simplify. + pose (Ptrofs.eq_spec ofs1 ofs2). + rewrite H in *. + trivial. +Qed. +Hint Resolve offset_eq_correct: wlp. Definition store_op_eq (o1 o2: store_op): ?? bool := match o1 with | OStoreRRO n1 ofs1 => - match o2 with OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end + match o2 with OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (offset_eq ofs1 ofs2) | _ => RET false end | OStoreRRR n1 => match o2 with OStoreRRR n2 => phys_eq n1 n2 | _ => RET false end + | OStoreRRRXS n1 => + match o2 with OStoreRRRXS n2 => phys_eq n1 n2 | _ => RET false end end. Lemma store_op_eq_correct o1 o2: WHEN store_op_eq o1 o2 ~> b THEN b = true -> o1 = o2. Proof. destruct o1, o2; wlp_simplify; try discriminate. + - f_equal. pose (Ptrofs.eq_spec ofs ofs0). + rewrite H in *. trivial. - congruence. - congruence. Qed. @@ -597,6 +637,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. @@ -607,8 +648,14 @@ Definition trans_basic (b: basic) : inst := | PArith ai => trans_arith ai | PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (PReg (#a) @ PReg pmem @ Enil))] | PLoadRRR n d a ro => [(#d, Op (Load (OLoadRRR n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PLoadRRRXS n d a ro => [(#d, Op (Load (OLoadRRRXS n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))] | PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PStoreQRRO qs a ofs => + let (s0, s1) := gpreg_q_expand qs in + [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil)); + (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil))] | Pallocframe sz pos => [(#FP, PReg (#SP)); (#SP, Op (Allocframe2 sz pos) (PReg (#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil); (pmem, Op (Allocframe sz pos) (Old (PReg (#SP)) @ PReg pmem @ Enil))] | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (PReg (#SP) @ PReg pmem @ Enil)); @@ -776,6 +823,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. @@ -805,7 +858,8 @@ Proof. (* Load Offset *) + destruct i; simpl load_chunk. all: unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0; - destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; + unfold eval_offset; + simpl; auto; destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. @@ -817,12 +871,19 @@ Proof. eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + (* Load Reg XS *) + + destruct i; simpl load_chunk. all: + unfold parexec_load_regxs; simpl; unfold exec_load_deps_regxs; rewrite H, H0; rewrite (H0 rofs); + destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + (* Store *) - destruct i. (* Store Offset *) + destruct i; simpl store_chunk. all: unfold parexec_store_offset; simpl; unfold exec_store_deps_offset; erewrite GENV, H, H0; rewrite (H0 ra); - destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; + unfold eval_offset; simpl; auto; destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. @@ -834,7 +895,44 @@ Proof. eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. -(* Allocframe *) + (* Store Reg XS *) + + destruct i; simpl store_chunk. all: + unfold parexec_store_regxs; simpl; unfold exec_store_deps_regxs; rewrite H, H0; rewrite (H0 ra); rewrite (H0 rofs); + destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl. + + + unfold parexec_store_q_offset. + simpl. + destruct (gpreg_q_expand rs) as [s0 s1]. + simpl. + unfold exec_store_deps_offset. + repeat rewrite H0. + repeat rewrite H. + destruct Ge. + destruct (Mem.storev _ _ _ (rsr s0)) as [mem0 | ] eqn:MEML0; simpl. + ++ rewrite MEML0. + destruct (Mem.storev _ _ _ (rsr s1)) as [mem1 | ] eqn:MEML1; simpl. + * rewrite (assign_diff sr _ (# s1)) by apply ppos_pmem_discr. + rewrite (assign_diff sr _ (# ra)) by apply ppos_pmem_discr. + repeat rewrite H0. + rewrite MEML1. + eexists; split. + reflexivity. + rewrite (assign_eq _ pmem). + split; trivial. + intro r. + rewrite (assign_diff _ _ (# r)) by apply ppos_pmem_discr. + rewrite (assign_diff _ _ (# r)) by apply ppos_pmem_discr. + congruence. + * rewrite (assign_diff sr pmem (# s1)) by apply ppos_pmem_discr. + rewrite (assign_diff sr pmem (# ra)) by apply ppos_pmem_discr. + repeat rewrite H0. + rewrite MEML1. + reflexivity. + ++ rewrite MEML0. + reflexivity. + (* Allocframe *) - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. * eexists; repeat split. { Simpl. erewrite !H0, H, MEMAL, MEMS. Simpl. @@ -1215,6 +1313,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 +1324,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 +1372,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 +1387,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 +1412,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 +1444,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 +1472,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. @@ -1386,6 +1495,7 @@ Definition string_of_load (op: load_op): pstring := match op with | OLoadRRO n _ => string_of_load_name n | OLoadRRR n => string_of_load_name n + | OLoadRRRXS n => string_of_load_name n end. Definition string_of_store_name (n: store_name) : pstring := @@ -1404,6 +1514,7 @@ Definition string_of_store (op: store_op) : pstring := match op with | OStoreRRO n _ => string_of_store_name n | OStoreRRR n => string_of_store_name n + | OStoreRRRXS n => string_of_store_name n end. Definition string_of_control (op: control_op) : pstring := @@ -1466,7 +1577,3 @@ Definition bblock_equivb: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bbloc 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..dc55715a 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -21,6 +21,8 @@ Require Archi. Require Import Coqlib Errors. Require Import AST Integers Floats Memdata. Require Import Op Locations Machblock Asmblock. +Require ExtValues. +Require Import Chunks. Local Open Scope string_scope. Local Open Scope error_monad_scope. @@ -518,11 +520,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 +642,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 +697,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 +761,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. @@ -797,36 +803,36 @@ Definition indexed_memory_access (base: ireg) (ofs: ptrofs) := match make_immed64 (Ptrofs.to_int64 ofs) with | Imm64_single imm => - mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) + mk_instr base (Ptrofs.of_int64 imm) end. Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := match ty, preg_of dst with - | Tint, IR rd => OK (indexed_memory_access (Plw rd) base ofs ::i k) - | Tlong, IR rd => OK (indexed_memory_access (Pld rd) base ofs ::i k) - | Tsingle, IR rd => OK (indexed_memory_access (Pfls rd) base ofs ::i k) - | Tfloat, IR rd => OK (indexed_memory_access (Pfld rd) base ofs ::i k) - | Tany32, IR rd => OK (indexed_memory_access (Plw_a rd) base ofs ::i k) - | Tany64, IR rd => OK (indexed_memory_access (Pld_a rd) base ofs ::i k) + | Tint, IR rd => OK (indexed_memory_access (PLoadRRO Plw rd) base ofs ::i k) + | Tlong, IR rd => OK (indexed_memory_access (PLoadRRO Pld rd) base ofs ::i k) + | Tsingle, IR rd => OK (indexed_memory_access (PLoadRRO Pfls rd) base ofs ::i k) + | Tfloat, IR rd => OK (indexed_memory_access (PLoadRRO Pfld rd) base ofs ::i k) + | Tany32, IR rd => OK (indexed_memory_access (PLoadRRO Plw_a rd) base ofs ::i k) + | Tany64, IR rd => OK (indexed_memory_access (PLoadRRO Pld_a rd) base ofs ::i k) | _, _ => Error (msg "Asmblockgen.loadind") end. Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: bcode) := match ty, preg_of src with - | Tint, IR rd => OK (indexed_memory_access (Psw rd) base ofs ::i k) - | Tlong, IR rd => OK (indexed_memory_access (Psd rd) base ofs ::i k) - | Tsingle, IR rd => OK (indexed_memory_access (Pfss rd) base ofs ::i k) - | Tfloat, IR rd => OK (indexed_memory_access (Pfsd rd) base ofs ::i k) - | Tany32, IR rd => OK (indexed_memory_access (Psw_a rd) base ofs ::i k) - | Tany64, IR rd => OK (indexed_memory_access (Psd_a rd) base ofs ::i k) + | Tint, IR rd => OK (indexed_memory_access (PStoreRRO Psw rd) base ofs ::i k) + | Tlong, IR rd => OK (indexed_memory_access (PStoreRRO Psd rd) base ofs ::i k) + | Tsingle, IR rd => OK (indexed_memory_access (PStoreRRO Pfss rd) base ofs ::i k) + | Tfloat, IR rd => OK (indexed_memory_access (PStoreRRO Pfsd rd) base ofs ::i k) + | Tany32, IR rd => OK (indexed_memory_access (PStoreRRO Psw_a rd) base ofs ::i k) + | Tany64, IR rd => OK (indexed_memory_access (PStoreRRO Psd_a rd) base ofs ::i k) | _, _ => Error (msg "Asmblockgen.storeind") end. Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) := - indexed_memory_access (Pld dst) base ofs. + indexed_memory_access (PLoadRRO Pld dst) base ofs. Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) := - indexed_memory_access (Psd src) base ofs. + indexed_memory_access (PStoreRRO Psd src) base ofs. (** Translation of memory accesses: loads, and stores. *) @@ -841,6 +847,19 @@ Definition transl_memory_access2 | _, _ => Error (msg "Asmblockgen.transl_memory_access2") end. +Definition transl_memory_access2XS + (chunk: memory_chunk) + (mk_instr: ireg -> ireg -> basic) + scale (args: list mreg) (k: bcode) : res bcode := + match args with + | (a1 :: a2 :: nil) => + assertion (Z.eqb (zscale_of_chunk chunk) scale); + do rs1 <- ireg_of a1; + do rs2 <- ireg_of a2; + OK (mk_instr rs1 rs2 ::i k) + | _ => Error (msg "Asmblockgen.transl_memory_access2XS") + end. + Definition transl_memory_access (mk_instr: ireg -> offset -> basic) (addr: addressing) (args: list mreg) (k: bcode) : res bcode := @@ -849,7 +868,7 @@ Definition transl_memory_access do rs <- ireg_of a1; OK (indexed_memory_access mk_instr rs ofs ::i k) | Aglobal id ofs, nil => - OK (Ploadsymbol id ofs RTMP ::i (mk_instr RTMP (Ofsimm Ptrofs.zero) ::i k)) + OK (Ploadsymbol id ofs RTMP ::i (mk_instr RTMP Ptrofs.zero ::i k)) | Ainstack ofs, nil => OK (indexed_memory_access mk_instr SP ofs ::i k) | _, _ => @@ -880,9 +899,15 @@ Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing) do r <- ireg_of dst; transl_memory_access2 (PLoadRRR (chunk2load chunk) r) addr args k. +Definition transl_load_rrrXS (chunk: memory_chunk) (scale : Z) + (args: list mreg) (dst: mreg) (k: bcode) : res bcode := + do r <- ireg_of dst; + transl_memory_access2XS chunk (PLoadRRRXS (chunk2load chunk) r) scale args k. + Definition transl_load (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := match addr with + | Aindexed2XS scale => transl_load_rrrXS chunk scale args dst k | Aindexed2 => transl_load_rrr chunk addr args dst k | _ => transl_load_rro chunk addr args dst k end. @@ -909,10 +934,16 @@ Definition transl_store_rrr (chunk: memory_chunk) (addr: addressing) do r <- ireg_of src; transl_memory_access2 (PStoreRRR (chunk2store chunk) r) addr args k. +Definition transl_store_rrrxs (chunk: memory_chunk) (scale: Z) + (args: list mreg) (src: mreg) (k: bcode) : res bcode := + do r <- ireg_of src; + transl_memory_access2XS chunk (PStoreRRRXS (chunk2store chunk) r) scale args k. + Definition transl_store (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg) (k: bcode) : res bcode := match addr with | Aindexed2 => transl_store_rrr chunk addr args src k + | Aindexed2XS scale => transl_store_rrrxs chunk scale args src k | _ => transl_store_rro chunk addr args src k end. diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index c6c88681..0233a3dc 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -521,9 +521,9 @@ Proof. unfold transl_cond_float32. exploreInst; try discriminate.
unfold transl_cond_notfloat32. exploreInst; try discriminate.
- simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate.
- all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; exploreInst; try discriminate.
+ all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; unfold transl_memory_access2XS in EQ0; exploreInst; try discriminate.
- simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate.
- all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; exploreInst; try discriminate.
+ all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; unfold transl_memory_access2XS in EQ0; exploreInst; try discriminate.
Qed.
Lemma transl_basic_code_nonil:
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index bbcffbe2..c3ee28f1 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -19,6 +19,7 @@ Require Import Coqlib Errors Maps. Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op Locations Machblock Conventions. Require Import Asmblock Asmblockgen Asmblockgenproof0. +Require Import Chunks. (** Decomposition of integer constants. *) @@ -1593,44 +1594,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. @@ -1888,7 +1872,7 @@ Lemma indexed_memory_access_correct: exists base' ofs' rs' ptr', exec_straight_opt (indexed_memory_access mk_instr base ofs ::g k) rs m (mk_instr base' ofs' ::g k) rs' m - /\ eval_offset ge ofs' = OK ptr' + /\ eval_offset ofs' = OK ptr' /\ Val.offset_ptr rs'#base' ptr' = Val.offset_ptr rs#base ofs /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. Proof. @@ -1933,7 +1917,7 @@ Qed. Lemma indexed_load_access_correct: forall chunk (mk_instr: ireg -> offset -> basic) rd m, (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs) -> forall (base: ireg) ofs k (rs: regset) v, Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v -> base <> RTMP -> @@ -1954,7 +1938,7 @@ Qed. Lemma indexed_store_access_correct: forall chunk (mk_instr: ireg -> offset -> basic) r1 m, (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk rs m r1 base ofs) -> forall (base: ireg) ofs k (rs: regset) m', Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' -> base <> RTMP -> r1 <> RTMP -> @@ -1990,7 +1974,7 @@ Proof. /\ c = indexed_memory_access mk_instr base ofs :: k /\ forall base' ofs' rs', exec_basic_instr ge (mk_instr base' ofs') rs' m = - exec_load_offset ge (chunk_of_type ty) rs' m rd base' ofs'). + exec_load_offset (chunk_of_type ty) rs' m rd base' ofs'). { unfold loadind in TR. destruct ty, (preg_of dst); inv TR; econstructor; esplit; eauto. } destruct A as (mk_instr & rd & rdEq & B & C). subst c. rewrite rdEq. @@ -2012,7 +1996,7 @@ Proof. /\ c = indexed_memory_access mk_instr base ofs :: k /\ forall base' ofs' rs', exec_basic_instr ge (mk_instr base' ofs') rs' m = - exec_store_offset ge (chunk_of_type ty) rs' m rr base' ofs'). + exec_store_offset (chunk_of_type ty) rs' m rr base' ofs'). { unfold storeind in TR. destruct ty, (preg_of src); inv TR; econstructor; esplit; eauto. } destruct A as (mk_instr & rr & rsEq & B & C). subst c. eapply indexed_store_access_correct; eauto with asmgen. @@ -2082,7 +2066,7 @@ Lemma transl_memory_access_correct: eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> exists base ofs rs' ptr, exec_straight_opt (basics_to_code c) rs m (mk_instr base ofs ::g (basics_to_code k)) rs' m - /\ eval_offset ge ofs = OK ptr + /\ eval_offset ofs = OK ptr /\ Val.offset_ptr rs'#base ptr = v /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. Proof. @@ -2127,6 +2111,26 @@ Proof. inv EV. repeat eexists. eassumption. econstructor; eauto. Qed. +Lemma transl_memory_access2XS_correct: + forall chunk mk_instr (scale : Z) args k c (rs: regset) m v, + transl_memory_access2XS chunk mk_instr scale args k = OK c -> + eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v -> + exists base ro mro mr1 rs', + args = mr1 :: mro :: nil + /\ ireg_of mro = OK ro + /\ exec_straight_opt (basics_to_code c) rs m (mk_instr base ro ::g (basics_to_code k)) rs' m + /\ Val.addl rs'#base (Val.shll rs'#ro (Vint (Int.repr scale))) = v + /\ (forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r) + /\ scale = (zscale_of_chunk chunk). +Proof. + intros until v; intros TR EV. + unfold transl_memory_access2XS in TR; ArgsInv. + inv EV. repeat eexists. eassumption. econstructor; eauto. + symmetry. + apply Z.eqb_eq. + assumption. +Qed. + Lemma transl_load_access2_correct: forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro v', args = mr1 :: mro :: nil -> @@ -2150,10 +2154,36 @@ Proof. split; intros; Simpl. auto. Qed. +Lemma transl_load_access2XS_correct: + forall chunk (mk_instr: ireg -> ireg -> basic) (scale : Z) args k c rd (rs: regset) m v mro mr1 ro v', + args = mr1 :: mro :: nil -> + ireg_of mro = OK ro -> + (forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs chunk rs m rd base ro) -> + transl_memory_access2XS chunk mk_instr scale args k = OK c -> + eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v -> + Mem.loadv chunk m v = Some v' -> + exists rs', + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m + /\ rs'#rd = v' + /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r. +Proof. + intros until v'; intros ARGS IREGE INSTR TR EV LOAD. + exploit transl_memory_access2XS_correct; eauto. + intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C & D). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS. + econstructor; split. + eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2. + rewrite INSTR. unfold exec_load_regxs. unfold parexec_load_regxs. + unfold scale_of_chunk. + subst scale. + rewrite B, LOAD. reflexivity. Simpl. + split; intros; Simpl. auto. +Qed. + Lemma transl_load_access_correct: forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v', (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs) -> transl_memory_access mk_instr addr args k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> Mem.loadv chunk m v = Some v' -> @@ -2173,7 +2203,7 @@ Qed. Lemma transl_load_memory_access_ok: forall addr chunk args dst k c rs a v m, - addr <> Aindexed2 -> + (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) -> transl_load chunk addr args dst k = OK c -> eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> @@ -2181,7 +2211,7 @@ Lemma transl_load_memory_access_ok: preg_of dst = IR rd /\ transl_memory_access mk_instr addr args k = OK c /\ forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs. + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs. Proof. intros until m. intros ADDR TR ? ?. unfold transl_load in TR. destruct addr; try contradiction. @@ -2216,6 +2246,27 @@ Proof. | eauto]. Qed. +Lemma transl_load_memory_access2XS_ok: + forall scale chunk args dst k c rs a v m, + transl_load chunk (Aindexed2XS scale) args dst k = OK c -> + eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a -> + Mem.loadv chunk m a = Some v -> + exists mk_instr mr0 mro rd ro, + args = mr0 :: mro :: nil + /\ preg_of dst = IR rd + /\ preg_of mro = IR ro + /\ transl_memory_access2XS chunk mk_instr scale args k = OK c + /\ forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs chunk rs m rd base ro. +Proof. + intros until m. intros TR ? ?. + unfold transl_load in TR. subst. monadInv TR. destruct chunk. all: + unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists; + [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity + | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRRXS _ x)); simpl; rewrite Heqb; eauto + | eauto]. +Qed. + Lemma transl_load_correct: forall chunk addr args dst k c (rs: regset) m a v, transl_load chunk addr args dst k = OK c -> @@ -2227,11 +2278,19 @@ Lemma transl_load_correct: /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r. Proof. intros until v; intros TR EV LOAD. destruct addr. - 2-4: exploit transl_load_memory_access_ok; eauto; try discriminate; - intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq; - eapply transl_load_access_correct; eauto with asmgen. + - exploit transl_load_memory_access2XS_ok; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C). + rewrite rdEq. eapply transl_load_access2XS_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. - exploit transl_load_memory_access2_ok; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C). rewrite rdEq. eapply transl_load_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. + - exploit transl_load_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity). + intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq; + eapply transl_load_access_correct; eauto with asmgen. + - exploit transl_load_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity). + intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq; + eapply transl_load_access_correct; eauto with asmgen. + - exploit transl_load_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity). + intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq; + eapply transl_load_access_correct; eauto with asmgen. Qed. Lemma transl_store_access2_correct: @@ -2258,10 +2317,37 @@ Proof. auto. Qed. +Lemma transl_store_access2XS_correct: + forall chunk (mk_instr: ireg -> ireg -> basic) scale args k c r1 (rs: regset) m v mr1 mro ro m', + args = mr1 :: mro :: nil -> + ireg_of mro = OK ro -> + (forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_store_regxs chunk rs m r1 base ro) -> + transl_memory_access2XS chunk mk_instr scale args k = OK c -> + eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v -> + Mem.storev chunk m v rs#r1 = Some m' -> + r1 <> RTMP -> + exists rs', + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m' + /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. +Proof. + intros until m'; intros ARGS IREG INSTR TR EV STORE NOT31. + exploit transl_memory_access2XS_correct; eauto. + intros (base & ro2 & mr2 & mro2 & rs' & ARGSS & IREGG & A & B & C & D). rewrite ARGSS in ARGS. inversion ARGS. subst mro2 mr2. clear ARGS. + econstructor; split. + eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2. + rewrite INSTR. unfold exec_store_regxs. unfold parexec_store_regxs. + unfold scale_of_chunk. + subst scale. + rewrite B. rewrite C; try discriminate. rewrite STORE. auto. + intro. inv H. contradiction. + auto. +Qed. + Lemma transl_store_access_correct: forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m', (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk rs m r1 base ofs) -> transl_memory_access mk_instr addr args k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> Mem.storev chunk m v rs#r1 = Some m' -> @@ -2282,22 +2368,22 @@ Qed. Remark exec_store_offset_8_sign rs m x base ofs: - exec_store_offset ge Mint8unsigned rs m x base ofs = exec_store_offset ge Mint8signed rs m x base ofs. + exec_store_offset Mint8unsigned rs m x base ofs = exec_store_offset Mint8signed rs m x base ofs. Proof. - unfold exec_store_offset. unfold parexec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev. + unfold exec_store_offset. unfold parexec_store_offset. unfold eval_offset; auto. unfold Mem.storev. destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_8. reflexivity. Qed. Remark exec_store_offset_16_sign rs m x base ofs: - exec_store_offset ge Mint16unsigned rs m x base ofs = exec_store_offset ge Mint16signed rs m x base ofs. + exec_store_offset Mint16unsigned rs m x base ofs = exec_store_offset Mint16signed rs m x base ofs. Proof. - unfold exec_store_offset. unfold parexec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev. + unfold exec_store_offset. unfold parexec_store_offset. unfold eval_offset; auto. unfold Mem.storev. destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_16. reflexivity. Qed. Lemma transl_store_memory_access_ok: forall addr chunk args src k c rs a m m', - addr <> Aindexed2 -> + (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) -> transl_store chunk addr args src k = OK c -> eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a -> Mem.storev chunk m a (rs (preg_of src)) = Some m' -> @@ -2305,7 +2391,7 @@ Lemma transl_store_memory_access_ok: preg_of src = IR rr /\ transl_memory_access mk_instr addr args k = OK c /\ (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk' rs m rr base ofs) + exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk' rs m rr base ofs) /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src). Proof. intros until m'. intros ? TR ? ?. @@ -2344,6 +2430,20 @@ Proof. erewrite <- Mem.store_signed_unsigned_16. reflexivity. Qed. +Remark exec_store_regxs_8_sign rs m x base ofs: + exec_store_regxs Mint8unsigned rs m x base ofs = exec_store_regxs Mint8signed rs m x base ofs. +Proof. + unfold exec_store_regxs. unfold parexec_store_regxs. unfold Mem.storev. destruct (Val.addl _ _); auto. + erewrite <- Mem.store_signed_unsigned_8. reflexivity. +Qed. + +Remark exec_store_regxs_16_sign rs m x base ofs: + exec_store_regxs Mint16unsigned rs m x base ofs = exec_store_regxs Mint16signed rs m x base ofs. +Proof. + unfold exec_store_regxs. unfold parexec_store_regxs. unfold Mem.storev. destruct (Val.addl _ _); auto. + erewrite <- Mem.store_signed_unsigned_16. reflexivity. +Qed. + Lemma transl_store_memory_access2_ok: forall addr chunk args src k c rs a m m', addr = Aindexed2 -> @@ -2369,6 +2469,30 @@ Proof. - simpl. intros. eapply exec_store_reg_16_sign. Qed. +Lemma transl_store_memory_access2XS_ok: + forall scale chunk args src k c rs a m m', + transl_store chunk (Aindexed2XS scale) args src k = OK c -> + eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a -> + Mem.storev chunk m a (rs (preg_of src)) = Some m' -> + exists mk_instr chunk' rr mr0 mro ro, + args = mr0 :: mro :: nil + /\ preg_of mro = IR ro + /\ preg_of src = IR rr + /\ transl_memory_access2XS chunk' mk_instr scale args k = OK c + /\ (forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_store_regxs chunk' rs m rr base ro) + /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src). +Proof. + intros until m'. intros TR ? ?. + unfold transl_store in TR. monadInv TR. destruct chunk. all: + unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists; + [ ArgsInv; reflexivity + | rewrite EQ1; rewrite EQ0; instantiate (1 := (PStoreRRRXS _ x)); simpl; rewrite Heqb; eauto + | eauto ]. + - simpl. intros. eapply exec_store_regxs_8_sign. + - simpl. intros. eapply exec_store_regxs_16_sign. +Qed. + Lemma transl_store_correct: forall chunk addr args src k c (rs: regset) m a m', transl_store chunk addr args src k = OK c -> @@ -2379,14 +2503,30 @@ Lemma transl_store_correct: /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. Proof. intros until m'; intros TR EV STORE. destruct addr. - 2-4: exploit transl_store_memory_access_ok; eauto; try discriminate; intro A; + - exploit transl_store_memory_access2XS_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C). + eapply transl_store_access2XS_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence. + destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate. + - exploit transl_store_memory_access2_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C). + eapply transl_store_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence. + destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate. + - exploit transl_store_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity). + intro A; + destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D); + rewrite D in STORE; clear D; + eapply transl_store_access_correct; eauto with asmgen; try congruence; + destruct rr; try discriminate; destruct src; try discriminate. + - exploit transl_store_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity). + intro A; + destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D); + rewrite D in STORE; clear D; + eapply transl_store_access_correct; eauto with asmgen; try congruence; + destruct rr; try discriminate; destruct src; try discriminate. + - exploit transl_store_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity). + intro A; destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D); rewrite D in STORE; clear D; eapply transl_store_access_correct; eauto with asmgen; try congruence; destruct rr; try discriminate; destruct src; try discriminate. - - exploit transl_store_memory_access2_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C). - eapply transl_store_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence. - destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate. Qed. Lemma make_epilogue_correct: diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index ba771bcb..c49cfbd5 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -154,10 +154,10 @@ let expand_builtin_memcpy_big sz al src dst = let lbl = new_label() in emit (Ploopdo (tmpbuf, lbl)); emit Psemi; - emit (Plb (tmpbuf, srcptr, AOff (Asmvliw.Ofsimm Z.zero))); + emit (Plb (tmpbuf, srcptr, AOff Z.zero)); emit (Paddil (srcptr, srcptr, Z.one)); emit Psemi; - emit (Psb (tmpbuf, dstptr, AOff (Asmvliw.Ofsimm Z.zero))); + emit (Psb (tmpbuf, dstptr, AOff Z.zero)); emit (Paddil (dstptr, dstptr, Z.one)); emit Psemi; emit (Plabel lbl);; @@ -173,30 +173,30 @@ let expand_builtin_memcpy sz al args = let expand_builtin_vload_common chunk base ofs res = match chunk, res with | Mint8unsigned, BR(Asmvliw.IR res) -> - emit (Plbu (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plbu (res, base, AOff ofs)) | Mint8signed, BR(Asmvliw.IR res) -> - emit (Plb (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plb (res, base, AOff ofs)) | Mint16unsigned, BR(Asmvliw.IR res) -> - emit (Plhu (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plhu (res, base, AOff ofs)) | Mint16signed, BR(Asmvliw.IR res) -> - emit (Plh (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plh (res, base, AOff ofs)) | Mint32, BR(Asmvliw.IR res) -> - emit (Plw (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plw (res, base, AOff ofs)) | Mint64, BR(Asmvliw.IR res) -> - emit (Pld (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Pld (res, base, AOff ofs)) | Mint64, BR_splitlong(BR(Asmvliw.IR res1), BR(Asmvliw.IR res2)) -> let ofs' = Ptrofs.add ofs _4 in if base <> res2 then begin - emit (Plw (res2, base, AOff (Asmvliw.Ofsimm ofs))); - emit (Plw (res1, base, AOff (Asmvliw.Ofsimm ofs'))) + emit (Plw (res2, base, AOff ofs)); + emit (Plw (res1, base, AOff ofs')) end else begin - emit (Plw (res1, base, AOff (Asmvliw.Ofsimm ofs'))); - emit (Plw (res2, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plw (res1, base, AOff ofs')); + emit (Plw (res2, base, AOff ofs)) end | Mfloat32, BR(Asmvliw.IR res) -> - emit (Pfls (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Pfls (res, base, AOff ofs)) | Mfloat64, BR(Asmvliw.IR res) -> - emit (Pfld (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Pfld (res, base, AOff ofs)) | _ -> assert false @@ -215,21 +215,21 @@ let expand_builtin_vload chunk args res = let expand_builtin_vstore_common chunk base ofs src = match chunk, src with | (Mint8signed | Mint8unsigned), BA(Asmvliw.IR src) -> - emit (Psb (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Psb (src, base, AOff ofs)) | (Mint16signed | Mint16unsigned), BA(Asmvliw.IR src) -> - emit (Psh (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Psh (src, base, AOff ofs)) | Mint32, BA(Asmvliw.IR src) -> - emit (Psw (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Psw (src, base, AOff ofs)) | Mint64, BA(Asmvliw.IR src) -> - emit (Psd (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Psd (src, base, AOff ofs)) | Mint64, BA_splitlong(BA(Asmvliw.IR src1), BA(Asmvliw.IR src2)) -> let ofs' = Ptrofs.add ofs _4 in - emit (Psw (src2, base, AOff (Asmvliw.Ofsimm ofs))); - emit (Psw (src1, base, AOff (Asmvliw.Ofsimm ofs'))) + emit (Psw (src2, base, AOff ofs)); + emit (Psw (src1, base, AOff ofs')) | Mfloat32, BA(Asmvliw.IR src) -> - emit (Pfss (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Pfss (src, base, AOff ofs)) | Mfloat64, BA(Asmvliw.IR src) -> - emit (Pfsd (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Pfsd (src, base, AOff ofs)) | _ -> assert false diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 13ff5422..6ebc8340 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. @@ -34,6 +35,7 @@ Require Stacklayout. Require Import Conventions. Require Import Errors. Require Import Sorting.Permutation. +Require Import Chunks. (** * Abstract syntax *) @@ -64,12 +66,63 @@ Inductive gpreg: Type := Definition ireg := gpreg. Definition freg := gpreg. +Lemma gpreg_eq: forall (x y: gpreg), {x=y} + {x<>y}. +Proof. decide equality. Defined. + Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. Proof. decide equality. Defined. Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. Proof. decide equality. Defined. +Inductive gpreg_q : Type := +| R0R1 | R2R3 | R4R5 | R6R7 | R8R9 +| R10R11 | R12R13 | R14R15 | R16R17 | R18R19 +| R20R21 | R22R23 | R24R25 | R26R27 | R28R29 +| R30R31 | R32R33 | R34R35 | R36R37 | R38R39 +| R40R41 | R42R43 | R44R45 | R46R47 | R48R49 +| R50R51 | R52R53 | R54R55 | R56R57 | R58R59 +| R60R61 | R62R63. + +Lemma gpreg_q_eq : forall (x y : gpreg_q), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +Definition gpreg_q_expand (x : gpreg_q) : gpreg * gpreg := + match x with + | R0R1 => (GPR0, GPR1) + | R2R3 => (GPR2, GPR3) + | R4R5 => (GPR4, GPR5) + | R6R7 => (GPR6, GPR7) + | R8R9 => (GPR8, GPR9) + | R10R11 => (GPR10, GPR11) + | R12R13 => (GPR12, GPR13) + | R14R15 => (GPR14, GPR15) + | R16R17 => (GPR16, GPR17) + | R18R19 => (GPR18, GPR19) + | R20R21 => (GPR20, GPR21) + | R22R23 => (GPR22, GPR23) + | R24R25 => (GPR24, GPR25) + | R26R27 => (GPR26, GPR27) + | R28R29 => (GPR28, GPR29) + | R30R31 => (GPR30, GPR31) + | R32R33 => (GPR32, GPR33) + | R34R35 => (GPR34, GPR35) + | R36R37 => (GPR36, GPR37) + | R38R39 => (GPR38, GPR39) + | R40R41 => (GPR40, GPR41) + | R42R43 => (GPR42, GPR43) + | R44R45 => (GPR44, GPR45) + | R46R47 => (GPR46, GPR47) + | R48R49 => (GPR48, GPR49) + | R50R51 => (GPR50, GPR51) + | R52R53 => (GPR52, GPR53) + | R54R55 => (GPR54, GPR55) + | R56R57 => (GPR56, GPR57) + | R58R59 => (GPR58, GPR59) + | R60R61 => (GPR60, GPR61) + | R62R63 => (GPR62, GPR63) + end. + (** We model the following registers of the RISC-V architecture. *) (** basic register *) @@ -150,9 +203,7 @@ Inductive ftest: Type := (** Offsets for load and store instructions. An offset is either an immediate integer or the low part of a symbol. *) -Inductive offset : Type := - | Ofsimm (ofs: ptrofs) - | Ofslow (id: ident) (ofs: ptrofs). +Definition offset : Type := ptrofs. (** We model a subset of the K1c instruction set. In particular, we do not support floats yet. @@ -183,9 +234,6 @@ Definition label := positive. *) Inductive ex_instruction : Type := (* Pseudo-instructions *) -(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *) - | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) *) - | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *) . @@ -269,11 +317,9 @@ Inductive load_name : Type := Inductive ld_instruction : Type := | PLoadRRO (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset) | PLoadRRR (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) + | PLoadRRRXS (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) . -Coercion PLoadRRO: load_name >-> Funclass. -Coercion PLoadRRR: load_name >-> Funclass. - (** Stores **) Inductive store_name : Type := | Psb (**r store byte *) @@ -289,11 +335,10 @@ Inductive store_name : Type := Inductive st_instruction : Type := | PStoreRRO (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset) | PStoreRRR (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg) + | PStoreRRRXS(i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg) + | PStoreQRRO (rs: gpreg_q) (ra: ireg) (ofs: offset) . -Coercion PStoreRRO: store_name >-> Funclass. -Coercion PStoreRRR: store_name >-> Funclass. - (** Arithmetic instructions **) Inductive arith_name_r : Type := | Ploadsymbol (id: ident) (ofs: ptrofs) (**r load the address of a symbol *) @@ -306,10 +351,11 @@ Inductive arith_name_rr : Type := | Pcvtl2w (**r Convert Long to Word *) | Psxwd (**r Sign Extend Word to Double Word *) | Pzxwd (**r Zero Extend Word to Double Word *) -(* | 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 +365,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 +408,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 +425,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 +450,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 +489,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 +505,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 +519,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. @@ -633,7 +688,7 @@ Variable ge: genv. from the current state (a register set + a memory state) to either [Next rs' m'] where [rs'] and [m'] are the updated register set and memory state after execution of the instruction at [rs#PC], or [Stuck] if the processor is stuck. - + The parallel semantics of each instructions handles two states in input: - the actual input state of the bundle which is only read - and the other on which every "write" is performed: @@ -881,8 +936,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 +950,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 +999,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 +1015,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 +1039,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 +1102,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,19 +1134,12 @@ 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. -Definition eval_offset (ofs: offset) : res ptrofs := - match ofs with - | Ofsimm n => OK n - | Ofslow id delta => - match (Genv.symbol_address ge id delta) with - | Vptr b ofs => OK ofs - | _ => Error (msg "Asmblock.eval_offset") - end - end. +Definition eval_offset (ofs: offset) : res ptrofs := OK ofs. (** * load/store *) @@ -1100,6 +1158,12 @@ Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) | Some v => Next (rsw#d <- v) mw end. +Definition parexec_load_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) := + match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with + | None => Stuck + | Some v => Next (rsw#d <- v) mw + end. + Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a: ireg) (ofs: offset) := match (eval_offset ofs) with | OK ptr => match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with @@ -1115,6 +1179,28 @@ Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem | Some m' => Next rsw m' end. +Definition parexec_store_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) := + match Mem.storev chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) (rsr s) with + | None => Stuck + | Some m' => Next rsw m' + end. + +Definition parexec_store_q_offset (rsr rsw: regset) (mr mw: mem) (s : gpreg_q) (a: ireg) (ofs: offset) := + let (s0, s1) := gpreg_q_expand s in + match eval_offset ofs with + | OK eofs => + match Mem.storev Many64 mr (Val.offset_ptr (rsr a) eofs) (rsr s0) with + | None => Stuck + | Some m1 => + match Mem.storev Many64 m1 (Val.offset_ptr (rsr a) (Ptrofs.add eofs (Ptrofs.repr 8))) (rsr s1) with + | None => Stuck + | Some m2 => Next rsw m2 + end + end + | _ => Stuck + end. + + Definition load_chunk n := match n with | Plb => Mint8signed @@ -1149,10 +1235,13 @@ Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) := | PLoadRRO n d a ofs => parexec_load_offset (load_chunk n) rsr rsw mr mw d a ofs | PLoadRRR n d a ro => parexec_load_reg (load_chunk n) rsr rsw mr mw d a ro + | PLoadRRRXS n d a ro => parexec_load_regxs (load_chunk n) rsr rsw mr mw d a ro | PStoreRRO n s a ofs => parexec_store_offset (store_chunk n) rsr rsw mr mw s a ofs | PStoreRRR n s a ro => parexec_store_reg (store_chunk n) rsr rsw mr mw s a ro - + | PStoreRRRXS n s a ro => parexec_store_regxs (store_chunk n) rsr rsw mr mw s a ro + | PStoreQRRO s a ofs => + parexec_store_q_offset rsr rsw mr mw s a ofs | Pallocframe sz pos => let (mw, stk) := Mem.alloc mr 0 sz in let sp := (Vptr stk Ptrofs.zero) in diff --git a/mppa_k1c/Chunks.v b/mppa_k1c/Chunks.v new file mode 100644 index 00000000..40778877 --- /dev/null +++ b/mppa_k1c/Chunks.v @@ -0,0 +1,22 @@ +Require Import AST. +Require Import Values. +Require Import Integers. +Require Import Coq.ZArith.BinIntDef. +Require Import BinNums. + +Local Open Scope Z_scope. + +Definition zscale_of_chunk (chunk: memory_chunk) : Z := + match chunk with + | Mint8signed => 0 + | Mint8unsigned => 0 + | Mint16signed => 1 + | Mint16unsigned => 1 + | Mint32 => 2 + | Mint64 => 3 + | Mfloat32 => 2 + | Mfloat64 => 3 + | Many32 => 2 + | Many64 => 3 + end. +Definition scale_of_chunk chunk := Vint (Int.repr (zscale_of_chunk chunk)). diff --git a/mppa_k1c/ConstpropOp.vp b/mppa_k1c/ConstpropOp.vp index aab2424d..b5128357 100644 --- a/mppa_k1c/ConstpropOp.vp +++ b/mppa_k1c/ConstpropOp.vp @@ -298,7 +298,7 @@ Nondetfunction addr_strength_reduction (addr: addressing) (args: list reg) (vl: list aval) := match addr, args, vl with | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil => - if Archi.pic_code tt + if (orb (Archi.pic_code tt) (negb (Compopts.optim_fglobaladdrtmp tt))) then (addr, args) else (Aglobal symb (Ptrofs.add n1 n), nil) | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil => diff --git a/mppa_k1c/ConstpropOpproof.v b/mppa_k1c/ConstpropOpproof.v index b6c73281..ae11a220 100644 --- a/mppa_k1c/ConstpropOpproof.v +++ b/mppa_k1c/ConstpropOpproof.v @@ -730,7 +730,7 @@ Proof. intros until res. unfold addr_strength_reduction. destruct (addr_strength_reduction_match addr args vl); simpl; intros VL EA; InvApproxRegs; SimplVM; try (inv EA). -- destruct (Archi.pic_code tt). +- destruct (orb _ _). + exists (Val.offset_ptr e#r1 n); auto. + simpl. rewrite Genv.shift_symbol_address. econstructor; split; eauto. inv H0; simpl; auto. 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/InstructionScheduler.ml b/mppa_k1c/InstructionScheduler.ml index dca4b8ff..1fa55c9b 100644 --- a/mppa_k1c/InstructionScheduler.ml +++ b/mppa_k1c/InstructionScheduler.ml @@ -307,10 +307,67 @@ let priority_list_scheduler (order : list_scheduler_order) let list_scheduler = priority_list_scheduler CRITICAL_PATH_ORDER;; -(* FIXME DUMMY CODE to placate warnings - *) +(** FIXME - warning fix *) let _ = priority_list_scheduler INSTRUCTION_ORDER;; +type bundle = int list;; + +let rec extract_deps_to index = function + | [] -> [] + | dep :: deps -> let extracts = extract_deps_to index deps in + if (dep.instr_to == index) then + dep :: extracts + else + extracts + +exception InvalidBundle;; + +let dependency_check problem bundle index = + let index_deps = extract_deps_to index problem.latency_constraints in + List.iter (fun i -> + List.iter (fun dep -> + if (dep.instr_from == i) then raise InvalidBundle + ) index_deps + ) bundle;; + +let rec make_bundle problem resources bundle index = + let resources_copy = Array.copy resources in + let nr_instructions = get_nr_instructions problem in + if (index >= nr_instructions) then (bundle, index+1) else + let inst_usage = problem.instruction_usages.(index) in + try match vector_less_equal inst_usage resources with + | false -> raise InvalidBundle + | true -> ( + dependency_check problem bundle index; + vector_subtract problem.instruction_usages.(index) resources_copy; + make_bundle problem resources_copy (index::bundle) (index+1) + ) + with InvalidBundle -> (bundle, index);; + +let rec make_bundles problem index : bundle list = + if index >= get_nr_instructions problem then + [] + else + let (bundle, new_index) = make_bundle problem problem.resource_bounds [] index in + bundle :: (make_bundles problem new_index);; + +let bundles_to_schedule problem bundles : solution = + let nr_instructions = get_nr_instructions problem in + let schedule = Array.make (nr_instructions+1) (nr_instructions+4) in + let time = ref 0 in + List.iter (fun bundle -> + begin + List.iter (fun i -> + schedule.(i) <- !time + ) bundle; + time := !time + 1 + end + ) bundles; schedule;; + +let greedy_scheduler (problem : problem) : solution option = + let bundles = make_bundles problem 0 in + Some (bundles_to_schedule problem bundles);; + (* alternate implementation let swap_array_elements a i j = let x = a.(i) in diff --git a/mppa_k1c/InstructionScheduler.mli b/mppa_k1c/InstructionScheduler.mli index 629664f9..f91c2d06 100644 --- a/mppa_k1c/InstructionScheduler.mli +++ b/mppa_k1c/InstructionScheduler.mli @@ -62,6 +62,9 @@ Once a clock tick is full go to the next. @return [Some solution] when a solution is found, [None] if not. *) val list_scheduler : problem -> solution option +(** Schedule the problem using the order of instructions without any reordering *) +val greedy_scheduler : problem -> solution option + (** Schedule a problem using a scheduler applied in the opposite direction, e.g. for list scheduling from the end instead of the start. BUGGY *) val schedule_reversed : scheduler -> problem -> int array option 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..5e80589b 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,13 +197,18 @@ 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. *) Inductive addressing: Type := - | Aindexed2: addressing (**r Address is [r1 + r2] *) + | Aindexed2XS (scale : Z) : addressing (**r Address is [r1 + r2 << scale] *) + | Aindexed2 : addressing (**r Address is [r1 + r2] *) | Aindexed: ptrofs -> addressing (**r Address is [r1 + offset] *) | Aglobal: ident -> ptrofs -> addressing (**r Address is global plus offset *) | Ainstack: ptrofs -> addressing. (**r Address is [stack_pointer + offset] *) @@ -228,7 +231,7 @@ Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. - generalize ident_eq Ptrofs.eq_dec; intros. + generalize ident_eq Ptrofs.eq_dec Z.eq_dec; intros. decide equality. Defined. @@ -481,8 +484,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 +501,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. @@ -509,6 +514,7 @@ Definition eval_addressing (F V: Type) (genv: Genv.t F V) (sp: val) (addr: addressing) (vl: list val) : option val := match addr, vl with + | Aindexed2XS scale, v1 :: v2 :: nil => Some (Val.addl v1 (Val.shll v2 (Vint (Int.repr scale)))) | Aindexed2, v1 :: v2 :: nil => Some (Val.addl v1 v2) | Aindexed n, v1 :: nil => Some (Val.offset_ptr v1 n) | Aglobal s ofs, nil => Some (Genv.symbol_address genv s ofs) @@ -675,8 +681,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,10 +700,15 @@ 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. +(* FIXME: two Tptr ?! *) Definition type_of_addressing (addr: addressing) : list typ := match addr with + | Aindexed2XS _ => Tptr :: Tptr :: nil | Aindexed2 => Tptr :: Tptr :: nil | Aindexed _ => Tptr :: nil | Aglobal _ _ => nil @@ -908,9 +917,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 +975,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. @@ -1093,7 +1121,7 @@ Qed. Definition offset_addressing (addr: addressing) (delta: Z) : option addressing := match addr with - | Aindexed2 => None + | Aindexed2 | Aindexed2XS _ => None | Aindexed n => Some(Aindexed (Ptrofs.add n (Ptrofs.repr delta))) | Aglobal id n => Some(Aglobal id (Ptrofs.add n (Ptrofs.repr delta))) | Ainstack n => Some(Ainstack (Ptrofs.add n (Ptrofs.repr delta))) @@ -1499,9 +1527,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 +1614,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: @@ -1612,6 +1665,9 @@ Lemma eval_addressing_inj: exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. + - apply Val.addl_inject; trivial. + destruct v0; destruct v'0; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial; inv H3. + apply Val.inject_long. - apply Val.addl_inject; auto. - apply Val.offset_ptr_inject; auto. - apply H; simpl; auto. diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v new file mode 100644 index 00000000..6e06e7ea --- /dev/null +++ b/mppa_k1c/Peephole.v @@ -0,0 +1,70 @@ +Require Import Coqlib. +Require Import Asmvliw. +Require Import Values. +Require Import Integers. +Require Compopts. + +Definition gpreg_q_list : list gpreg_q := +R0R1 :: R2R3 :: R4R5 :: R6R7 :: R8R9 +:: R10R11 :: R12R13 :: R14R15 :: R16R17 :: R18R19 +:: R20R21 :: R22R23 :: R24R25 :: R26R27 :: R28R29 +:: R30R31 :: R32R33 :: R34R35 :: R36R37 :: R38R39 +:: R40R41 :: R42R43 :: R44R45 :: R46R47 :: R48R49 +:: R50R51 :: R52R53 :: R54R55 :: R56R57 :: R58R59 +:: R60R61 :: R62R63 :: nil. + +Fixpoint gpreg_q_search_rec r0 r1 l := + match l with + | h :: t => + let (s0, s1) := gpreg_q_expand h in + if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) + then Some h + else gpreg_q_search_rec r0 r1 t + | nil => None + end. + +Definition gpreg_q_search (r0 : gpreg) (r1 : gpreg) : option gpreg_q := + gpreg_q_search_rec r0 r1 gpreg_q_list. + +Parameter print_found_store: forall A, Z -> A -> A. + +Fixpoint coalesce_mem (insns : list basic) : list basic := + match insns with + | nil => nil + | h0 :: t0 => + match t0 with + | h1 :: t1 => + match h0, h1 with + | (PStoreRRO Psd_a rs0 ra0 ofs0), + (PStoreRRO Psd_a rs1 ra1 ofs1) => + match gpreg_q_search rs0 rs1 with + | Some rs0rs1 => + let zofs0 := Ptrofs.signed ofs0 in + let zofs1 := Ptrofs.signed ofs1 in + if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1) + then (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + else h0 :: (coalesce_mem t0) + | None => h0 :: (coalesce_mem t0) + end + | _, _ => h0 :: (coalesce_mem t0) + end + | nil => h0 :: nil + end + end. + +Definition optimize_body (insns : list basic) := + if Compopts.optim_coalesce_mem tt + then coalesce_mem insns + else insns. + +Program Definition optimize_bblock (bb : bblock) := + let optimized := optimize_body (body bb) in + let wf_ok := wf_bblockb optimized (exit bb) in + {| header := header bb; + body := if wf_ok then optimized else (body bb); + exit := exit bb |}. +Next Obligation. + destruct (wf_bblockb (optimize_body (body bb))) eqn:Rwf. + - rewrite Rwf. simpl. trivial. + - exact (correct bb). +Qed. diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index ab4bc9c9..ecd40f5c 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -13,6 +13,7 @@ Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. Require Import Asmblockdeps Asmblockgenproof0. +Require Peephole. Local Open Scope error_monad_scope. @@ -347,8 +348,9 @@ Fixpoint verify_par (lbb: list bblock) := end. Definition verified_schedule_nob (bb : bblock) : res (list bblock) := - let bb' := no_header bb in - let lbb := do_schedule bb' in + let bb' := no_header bb in + let bb'' := Peephole.optimize_bblock bb' in + let lbb := do_schedule bb'' in do tbb <- concat_all lbb; do sizecheck <- verify_size bb lbb; do schedcheck <- verify_schedule bb' tbb; diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 87f34ee6..327e6c4b 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)) @@ -204,15 +216,20 @@ let arith_rec i = | PArithR (i, rd) -> arith_r_rec i (IR rd) let load_rec i = match i with - | PLoadRRO (i, rs1, rs2, imm) -> { inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2)]; imm = (Some (Off imm)) - ; is_control = false} - | PLoadRRR (i, rs1, rs2, rs3) -> { inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2); Reg (IR rs3)]; imm = None - ; is_control = false} + | PLoadRRO (i, rs1, rs2, imm) -> + { inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2)]; imm = (Some (Off imm)) ; is_control = false} + | PLoadRRR (i, rs1, rs2, rs3) | PLoadRRRXS (i, rs1, rs2, rs3) -> + { inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2); Reg (IR rs3)]; imm = None ; is_control = false} let store_rec i = match i with - | PStoreRRO (i, rs1, rs2, imm) -> { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2)]; imm = (Some (Off imm)) + | PStoreRRO (i, rs1, rs2, imm) -> + { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2)]; imm = (Some (Off imm)) ; is_control = false} - | PStoreRRR (i, rs1, rs2, rs3) -> { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; imm = None + | PStoreQRRO (rs, ra, imm) -> + let (rs0, rs1) = gpreg_q_expand rs in + { inst = "Psq"; write_locs = [Mem]; read_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR ra)]; imm = (Some (Off imm)) + ; is_control = false} + | PStoreRRR (i, rs1, rs2, rs3) | PStoreRRRXS (i, rs1, rs2, rs3) -> { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; imm = None ; is_control = false} let get_rec (rd:gpreg) rs = { inst = get_str; write_locs = [Reg (IR rd)]; read_locs = [Reg rs]; imm = None; is_control = false } @@ -422,14 +439,14 @@ 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 + | Sb | Sh | Sw | Sd | Sq (* BCU *) | Icall | Call | Cb | Igoto | Goto | Ret | Get | Set (* FPU *) @@ -459,6 +476,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 +495,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 @@ -507,6 +523,7 @@ let ab_inst_to_real = function | "Psh" -> Sh | "Psw" | "Psw_a" | "Pfss" -> Sw | "Psd" | "Psd_a" | "Pfsd" -> Sd + | "Psq" -> Sq | "Pcb" | "Pcbu" -> Cb | "Pcall" | "Pdiv" | "Pdivu" -> Call @@ -527,15 +544,17 @@ let ab_inst_to_real = function | "Pfsbfw" -> Fsbfw | "Pfmuld" -> Fmuld | "Pfmulw" -> Fmulw + + | "nop" -> Nop + | s -> failwith @@ sprintf "ab_inst_to_real: unrecognized instruction: %s" s exception InvalidEncoding let rec_to_usage r = let encoding = match r.imm with None -> None | Some (I32 i) | Some (I64 i) -> Some (encode_imm @@ Z.to_int64 i) - | Some (Off (Ofsimm ptr)) -> Some (encode_imm @@ camlint64_of_ptrofs ptr) - | Some (Off (Ofslow (_, _))) -> Some E27U27L10 (* FIXME *) - (* I do not know yet in which context Ofslow can be used by CompCert *) + | Some (Off ptr) -> Some (encode_imm @@ camlint64_of_ptrofs ptr) + and real_inst = ab_inst_to_real r.inst in match real_inst with | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw @@ -571,16 +590,16 @@ 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 | Some U27L5 | Some U27L10 -> lsu_data_x | Some E27U27L10 -> lsu_data_y) - | Sb | Sh | Sw | Sd -> + | Sb | Sh | Sw | Sd | Sq -> (match encoding with None | Some U6 | Some S10 -> lsu_acc | Some U27L5 | Some U27L10 -> lsu_acc_x | Some E27U27L10 -> lsu_acc_y) @@ -592,17 +611,17 @@ 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 *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> 3 - | Sb | Sh | Sw | Sd -> 1 (* See k1c-Optimization.pdf page 19 *) + | Sb | Sh | Sw | Sd | Sq -> 1 (* See k1c-Optimization.pdf page 19 *) | Get -> 1 | Set -> 4 (* According to the manual should be 3, but I measured 4 *) | Icall | Call | Cb | Igoto | Goto | Ret -> 42 (* Should not matter since it's the final instruction of the basic block *) @@ -756,10 +775,12 @@ let print_bb oc bb = let do_schedule bb = let problem = build_problem bb - in let solution = validated_scheduler - (if !Clflags.option_fpostpass_ilp - then cascaded_scheduler - else list_scheduler) problem + in let solution = (if !Clflags.option_fpostpass_sched = "ilp" then + validated_scheduler cascaded_scheduler + else if !Clflags.option_fpostpass_sched = "list" then + validated_scheduler list_scheduler + else if !Clflags.option_fpostpass_sched = "greedy" then + greedy_scheduler else failwith ("Invalid scheduler:" ^ !Clflags.option_fpostpass_sched)) problem in match solution with | None -> failwith "Could not find a valid schedule" | Some sol -> let bundles = bundlize_solution bb sol in @@ -802,19 +823,25 @@ let is_opaque = function | PBasic (Pallocframe _) | PBasic (Pfreeframe _) | PControl (PExpand (Pbuiltin _)) -> true | _ -> false +(* Returns : (accumulated instructions, remaining instructions, opaque instruction if found) *) let rec biggest_wo_opaque = function - | [] -> ([], []) - | [i] -> ([i], []) - | i1 :: i2 :: li -> if is_opaque i2 || is_opaque i1 then ([i1], i2::li) - else let big, rem = biggest_wo_opaque li in (i1 :: i2 :: big, rem) + | [] -> ([], [], None) + | i :: li -> if is_opaque i then ([], li, Some i) + else let big, rem, opaque = biggest_wo_opaque li in (i :: big, rem, opaque);; let separate_opaque bb = let instrs = bb_to_instrs bb - in let rec f hd = function - | [] -> [] - | li -> - let sub_li, li = biggest_wo_opaque li - in (bundlize sub_li hd) :: (f [] li) + in let rec f hd li = + match li with + | [] -> [] + | li -> let big, rem, opaque = biggest_wo_opaque li in + match opaque with + | Some i -> + (match big with + | [] -> (bundlize [i] hd) :: (f [] rem) + | big -> (bundlize big hd) :: (bundlize [i] []) :: (f [] rem) + ) + | None -> (bundlize big hd) :: (f [] rem) in f bb.header instrs let smart_schedule bb = diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index bc90dd4c..da64c41d 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -96,11 +96,11 @@ Proof. Qed. Lemma exec_load_offset_pc_var: - forall ge t rs m rd ra ofs rs' m' v, - exec_load_offset ge t rs m rd ra ofs = Next rs' m' -> - exec_load_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. + forall t rs m rd ra ofs rs' m' v, + exec_load_offset t rs m rd ra ofs = Next rs' m' -> + exec_load_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. - intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. + intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - discriminate. @@ -117,18 +117,42 @@ Proof. - discriminate. Qed. +Lemma exec_load_regxs_pc_var: + forall t rs m rd ra ro rs' m' v, + exec_load_regxs t rs m rd ra ro = Next rs' m' -> + exec_load_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate. + destruct (Mem.loadv _ _ _). + - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. + - discriminate. +Qed. + Lemma exec_store_offset_pc_var: - forall ge t rs m rd ra ofs rs' m' v, - exec_store_offset ge t rs m rd ra ofs = Next rs' m' -> - exec_store_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. + forall t rs m rd ra ofs rs' m' v, + exec_store_offset t rs m rd ra ofs = Next rs' m' -> + exec_store_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate. - destruct (eval_offset ge ofs); try discriminate. + destruct (eval_offset ofs); try discriminate. destruct (Mem.storev _ _ _). - inv H. apply next_eq; auto. - discriminate. Qed. +Lemma exec_store_q_offset_pc_var: + forall rs m rd ra ofs rs' m' v, + exec_store_q_offset rs m rd ra ofs = Next rs' m' -> + exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate. + simpl in *. + destruct (gpreg_q_expand _) as [s0 s1]. + destruct (Mem.storev _ _ _); try discriminate. + destruct (Mem.storev _ _ _); try discriminate. + inv H. apply next_eq; auto. +Qed. + Lemma exec_store_reg_pc_var: forall t rs m rd ra ro rs' m' v, exec_store_reg t rs m rd ra ro = Next rs' m' -> @@ -140,6 +164,17 @@ Proof. - discriminate. Qed. +Lemma exec_store_regxs_pc_var: + forall t rs m rd ra ro rs' m' v, + exec_store_regxs t rs m rd ra ro = Next rs' m' -> + exec_store_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_store_regxs in *. unfold parexec_store_regxs in *. rewrite Pregmap.gso; try discriminate. + destruct (Mem.storev _ _ _). + - inv H. apply next_eq; auto. + - discriminate. +Qed. + Lemma exec_basic_instr_pc_var: forall ge i rs m rs' m' v, exec_basic_instr ge i rs m = Next rs' m' -> @@ -155,9 +190,12 @@ Proof. - destruct i. + exploreInst; apply exec_load_offset_pc_var; auto. + exploreInst; apply exec_load_reg_pc_var; auto. + + exploreInst; apply exec_load_regxs_pc_var; auto. - destruct i. + exploreInst; apply exec_store_offset_pc_var; auto. + exploreInst; apply exec_store_reg_pc_var; auto. + + exploreInst; apply exec_store_regxs_pc_var; auto. + + apply exec_store_q_offset_pc_var; auto. - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate). destruct (Mem.storev _ _ _ _); try discriminate. inv H. apply next_eq; auto. apply functional_extensionality. intros. @@ -576,32 +614,12 @@ Proof. unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto. Qed. -Lemma eval_offset_preserved: - forall ofs, eval_offset ge ofs = eval_offset tge ofs. -Proof. - intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto. -Qed. - -Lemma transf_exec_load_offset: - forall t rs m rd ra ofs, exec_load_offset ge t rs m rd ra ofs = exec_load_offset tge t rs m rd ra ofs. -Proof. - intros. unfold exec_load_offset. unfold parexec_load_offset. rewrite eval_offset_preserved. reflexivity. -Qed. - -Lemma transf_exec_store_offset: - forall t rs m rs0 ra ofs, exec_store_offset ge t rs m rs0 ra ofs = exec_store_offset tge t rs m rs0 ra ofs. -Proof. - intros. unfold exec_store_offset. unfold parexec_store_offset. rewrite eval_offset_preserved. reflexivity. -Qed. - Lemma transf_exec_basic_instr: forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m. Proof. intros. pose symbol_address_preserved. unfold exec_basic_instr. unfold parexec_basic_instr. exploreInst; simpl; auto; try congruence. - - unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. - - apply transf_exec_load_offset. - - apply transf_exec_store_offset. + unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. Qed. Lemma transf_exec_body: 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..717b0120 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. @@ -68,7 +70,10 @@ Nondetfunction addlimm (n: int64) (e: expr) := if Int64.eq n Int64.zero then e else match e with | Eop (Olongconst m) Enil => longconst (Int64.add n m) - | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil + | Eop (Oaddrsymbol s m) Enil => + (if Compopts.optim_fglobaladdroffset tt + then Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil + else Eop (Oaddlimm n) (e ::: Enil)) | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil | Eop (Oaddlimm m) (t ::: Enil) => Eop (Oaddlimm(Int64.add n m)) (t ::: Enil) | _ => Eop (Oaddlimm n) (e ::: Enil) @@ -155,6 +160,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 +183,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 +315,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 +450,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..3b724c01 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. @@ -126,9 +127,11 @@ Proof. destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto. destruct (addlimm_match a); InvEval. - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto. -- econstructor; split. EvalOp. simpl; eauto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. - destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto. +- destruct (Compopts.optim_fglobaladdroffset _). + + econstructor; split. EvalOp. simpl; eauto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. + destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto. + + TrivialExists. repeat econstructor. simpl. trivial. - econstructor; split. EvalOp. simpl; eauto. destruct sp; simpl; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_assoc, (Ptrofs.add_commut m0). auto. @@ -238,7 +241,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 +251,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 +293,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 +303,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 +591,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..6adcebe5 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -51,6 +51,10 @@ Require Import Floats. Require Import Op. Require Import CminorSel. Require Import OpHelpers. +Require Import ExtValues. +Require Import DecBoolOps. +Require Import Chunks. +Require Compopts. Local Open Scope cminorsel_scope. @@ -189,9 +193,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 +215,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 +339,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 +560,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). @@ -558,9 +583,19 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). Nondetfunction addressing (chunk: memory_chunk) (e: expr) := match e with | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) - | Eop (Oaddrsymbol id ofs) Enil => if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil) + | Eop (Oaddrsymbol id ofs) Enil => + (if (orb (Archi.pic_code tt) (negb (Compopts.optim_fglobaladdrtmp tt))) + then (Aindexed Ptrofs.zero, e:::Enil) + else (Aglobal id ofs, Enil)) | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil) | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil) + | Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) => + (if Compopts.optim_fxsaddr tt + then let zscale := Int.unsigned scale in + if Z.eq_dec zscale (zscale_of_chunk chunk) + then (Aindexed2XS zscale, e1:::e2:::Enil) + else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) + else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil)) | Eop Oaddl (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) | _ => (Aindexed Ptrofs.zero, e:::Enil) end. @@ -593,3 +628,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..9e2eec8b 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: @@ -1175,7 +1256,7 @@ Theorem eval_addressing: Proof. intros until v. unfold addressing; case (addressing_match a); intros; InvEval. - exists (@nil val); split. eauto with evalexpr. simpl. auto. - - destruct (Archi.pic_code tt). + - destruct (orb _ _). + exists (Vptr b ofs0 :: nil); split. constructor. EvalOp. simpl. congruence. constructor. simpl. rewrite Ptrofs.add_zero. congruence. + exists (@nil val); split. constructor. simpl; auto. @@ -1184,6 +1265,18 @@ Proof. - exists (v1 :: nil); split. eauto with evalexpr. simpl. destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. simpl. auto. + - destruct (Compopts.optim_fxsaddr tt). + + destruct (Z.eq_dec _ _). + * exists (v1 :: v2 :: nil); split. + repeat (constructor; auto). simpl. rewrite Int.repr_unsigned. destruct v2; simpl in *; congruence. + * exists (v1 :: v0 :: nil); split. + repeat (constructor; auto). econstructor. + repeat (constructor; auto). eassumption. simpl. congruence. + simpl. congruence. + + exists (v1 :: v0 :: nil); split. + repeat (constructor; auto). econstructor. + repeat (constructor; auto). eassumption. simpl. congruence. + simpl. congruence. - exists (v1 :: v0 :: nil); split. repeat (constructor; auto). simpl. congruence. - exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto. Qed. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 8826e6a2..9d42169a 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -41,6 +41,7 @@ module Target (*: TARGET*) = let print_label oc lbl = label oc (transl_label lbl) let int_reg_name = let open Asmvliw in function + | GPR0 -> "$r0" | GPR1 -> "$r1" | GPR2 -> "$r2" | GPR3 -> "$r3" | GPR4 -> "$r4" | GPR5 -> "$r5" | GPR6 -> "$r6" | GPR7 -> "$r7" | GPR8 -> "$r8" | GPR9 -> "$r9" | GPR10 -> "$r10" | GPR11 -> "$r11" @@ -60,7 +61,43 @@ module Target (*: TARGET*) = let ireg oc r = output_string oc (int_reg_name r) - let ireg = ireg + let int_gpreg_q_name = + let open Asmvliw in + function + | R0R1 -> "$r0r1" + | R2R3 -> "$r2r3" + | R4R5 -> "$r4r5" + | R6R7 -> "$r6r7" + | R8R9 -> "$r8r9" + | R10R11 -> "$r10r11" + | R12R13 -> "$r12r13" + | R14R15 -> "$r14r15" + | R16R17 -> "$r16r17" + | R18R19 -> "$r18r19" + | R20R21 -> "$r20r21" + | R22R23 -> "$r22r23" + | R24R25 -> "$r24r25" + | R26R27 -> "$r26r27" + | R28R29 -> "$r28r29" + | R30R31 -> "$r30r31" + | R32R33 -> "$r32r33" + | R34R35 -> "$r34r35" + | R36R37 -> "$r36r37" + | R38R39 -> "$r38r39" + | R40R41 -> "$r40r41" + | R42R43 -> "$r42r43" + | R44R45 -> "$r44r45" + | R46R47 -> "$r46r47" + | R48R49 -> "$r48r49" + | R50R51 -> "$r50r51" + | R52R53 -> "$r52r53" + | R54R55 -> "$r54r55" + | R56R57 -> "$r56r57" + | R58R59 -> "$r58r59" + | R60R61 -> "$r60r61" + | R62R63 -> "$r62r63" + + let gpreg_q oc r = output_string oc (int_gpreg_q_name r) let preg oc = let open Asmvliw in function | IR r -> ireg oc r @@ -160,13 +197,15 @@ module Target (*: TARGET*) = *) (* Offset part of a load or store *) - let offset oc = let open Asmvliw in function - | Ofsimm n -> ptrofs oc n - | Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs) + let offset oc n = ptrofs oc n let addressing oc = function | AOff ofs -> offset oc ofs - | AReg ro -> ireg oc ro + | AReg ro | ARegXS ro -> ireg oc ro + + let xscale oc = function + | ARegXS _ -> fprintf oc ".xs" + | _ -> () let icond_name = let open Asmvliw in function | ITne | ITneu -> "ne" @@ -248,7 +287,7 @@ module Target (*: TARGET*) = | _ -> assert false end - | Pnop -> fprintf oc " nop\n" + | Pnop -> (* FIXME fprintf oc " nop\n" *) () | Psemi -> fprintf oc ";;\n" | Pclzll (rd, rs) -> fprintf oc " clzd %a = %a\n" ireg rd ireg rs @@ -342,27 +381,29 @@ module Target (*: TARGET*) = (* Load/Store instructions *) | Plb(rd, ra, adr) -> - fprintf oc " lbs %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " lbs%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Plbu(rd, ra, adr) -> - fprintf oc " lbz %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " lbz%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Plh(rd, ra, adr) -> - fprintf oc " lhs %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " lhs%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Plhu(rd, ra, adr) -> - fprintf oc " lhz %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " lhz%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Plw(rd, ra, adr) | Plw_a(rd, ra, adr) | Pfls(rd, ra, adr) -> - fprintf oc " lws %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " lws%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Pld(rd, ra, adr) | Pfld(rd, ra, adr) | Pld_a(rd, ra, adr) -> assert Archi.ptr64; - fprintf oc " ld %a = %a[%a]\n" ireg rd addressing adr ireg ra + fprintf oc " ld%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Psb(rd, ra, adr) -> - fprintf oc " sb %a[%a] = %a\n" addressing adr ireg ra ireg rd + fprintf oc " sb%a %a[%a] = %a\n" xscale adr addressing adr ireg ra ireg rd | Psh(rd, ra, adr) -> - fprintf oc " sh %a[%a] = %a\n" addressing adr ireg ra ireg rd + fprintf oc " sh%a %a[%a] = %a\n" xscale adr addressing adr ireg ra ireg rd | Psw(rd, ra, adr) | Psw_a(rd, ra, adr) | Pfss(rd, ra, adr) -> - fprintf oc " sw %a[%a] = %a\n" addressing adr ireg ra ireg rd + fprintf oc " sw%a %a[%a] = %a\n" xscale adr addressing adr ireg ra ireg rd | Psd(rd, ra, adr) | Psd_a(rd, ra, adr) | Pfsd(rd, ra, adr) -> assert Archi.ptr64; - fprintf oc " sd %a[%a] = %a\n" addressing adr ireg ra ireg rd - + fprintf oc " sd%a %a[%a] = %a\n" xscale adr addressing adr ireg ra ireg rd + | Psq(rd, ra, adr) -> + fprintf oc " sq%a %a[%a] = %a\n" xscale adr addressing adr ireg ra gpreg_q rd + (* Arith R instructions *) (* Arith RR instructions *) @@ -377,10 +418,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 +442,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 +508,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 +543,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 +588,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 +605,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..643cca0c 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 *) @@ -37,6 +37,7 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval := match addr, vl with | Aindexed n, v1::nil => offset_ptr v1 n | Aindexed2, v1::v2::nil => addl v1 v2 + | Aindexed2XS scale, v1::v2::nil => addl v1 (shll v2 (I (Int.repr scale))) | Aglobal s ofs, nil => Ptr (Gl s ofs) | Ainstack ofs, nil => Ptr (Stk ofs) | _, _ => Vbot @@ -76,9 +77,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 +88,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 +98,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 +257,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 +276,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 +407,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)) diff --git a/mppa_k1c/extractionMachdep.v b/mppa_k1c/extractionMachdep.v index e70f51de..fdecd2a3 100644 --- a/mppa_k1c/extractionMachdep.v +++ b/mppa_k1c/extractionMachdep.v @@ -22,6 +22,9 @@ Require Archi Asm. Extract Constant Archi.ptr64 => " Configuration.model = ""64"" ". Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *) +Extract Constant Peephole.print_found_store => +"fun offset x -> Printf.printf ""found offset = %ld\n"" (Camlcoq.camlint_of_coqint offset); x". + (* Asm *) (* Extract Constant Asm.low_half => "fun _ _ _ -> assert false". diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index eb336edc..3bca6629 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -944,10 +944,19 @@ Lemma exec_basic_instr_pc: Proof. intros. destruct b; try destruct i; try destruct i. all: try (inv H; Simpl). - 1-10: try (unfold parexec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + 1-10: try (unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). 1-10: try (unfold parexec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - 1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). + 1-10: try (unfold parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + 1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). 1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. + 1-10: try (unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. + - (* PStoreQRRO *) + unfold parexec_store_q_offset in H1. + destruct (gpreg_q_expand _) as [r0 r1] in H1. + unfold eval_offset in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + inv H1. Simpl. reflexivity. - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. diff --git a/test/monniaux/bitfields/bitfields.c b/test/monniaux/bitfields/bitfields.c index 868d7483..16ad5a61 100644 --- a/test/monniaux/bitfields/bitfields.c +++ b/test/monniaux/bitfields/bitfields.c @@ -4,8 +4,18 @@ struct fields { unsigned f0 : 3; unsigned f1 : 5; signed f2 : 3; + unsigned toto1: 16; + unsigned toto2: 16; }; +unsigned get_toto1(struct fields x) { + return x.toto1; +} + +unsigned get_toto2(struct fields x) { + return x.toto2; +} + int get_f1(struct fields x) { return x.f1; } @@ -14,7 +24,13 @@ int get_f2(struct fields x) { return x.f2; } +void set_f1(struct fields *x, unsigned v) { + x->f1 = v; +} + int main() { struct fields x = {1, 2, -1}; printf("%d %d\n", get_f1(x), get_f2(x)); + set_f1(&x, 4); + printf("%d %d\n", get_f1(x), get_f2(x)); } diff --git a/test/monniaux/bitfields/bitfields_long.c b/test/monniaux/bitfields/bitfields_long.c new file mode 100644 index 00000000..93bba8d0 --- /dev/null +++ b/test/monniaux/bitfields/bitfields_long.c @@ -0,0 +1,19 @@ +#include <stdio.h> +#include <stdint.h> + +#define GET_FIELD_L(x, stop, start) (((x) << (63-(stop))) >> (63-(stop)+(start))) +#define FIELD_MASK(stop, start) ((1ULL<<(stop)) - (1ULL<<(start)) + (1ULL<<(stop))) + +#define SET_FIELD_L(x, stop, start, y) (((x) & ~FIELD_MASK(stop, start)) | ((y << start) & FIELD_MASK(stop, start))) + +uint64_t get_f2(uint64_t x) { + return GET_FIELD_L(x, 47, 16); +} + +uint64_t set_f2(uint64_t x, uint64_t y) { + return SET_FIELD_L(x, 47, 16, y); +} + +int main() { + printf("%lx %lx\n", FIELD_MASK(47, 16), set_f2(0x12345678ABCD1234ULL, 0x11112222ULL)); +} diff --git a/test/monniaux/ocaml/config/Makefile b/test/monniaux/ocaml/config/Makefile index 8fa72626..26b14670 100644 --- a/test/monniaux/ocaml/config/Makefile +++ b/test/monniaux/ocaml/config/Makefile @@ -22,7 +22,7 @@ X11_LINK=-lX11 LIBBFD_LINK= LIBBFD_INCLUDE= # DM CC=k1-mbr-gcc -CC=/home/monniaux/work/Kalray/CompCert/ccomp +CC=/home/monniaux/work/Kalray/mppa-xsaddr/ccomp CPP=$(CC) -E CFLAGS=-O -Wall -fall # DM CFLAGS=-O3 -Wall diff --git a/test/monniaux/regalloc/bigspill.c b/test/monniaux/regalloc/bigspill.c new file mode 100644 index 00000000..6191e018 --- /dev/null +++ b/test/monniaux/regalloc/bigspill.c @@ -0,0 +1,21 @@ +extern void callee(void); + +void bigspill(int *t) { + int t0 = t[0]; + int t1 = t[1]; + int t2 = t[2]; + int t3 = t[3]; + int t4 = t[4]; + int t5 = t[5]; + int t6 = t[6]; + int t7 = t[7]; + callee(); + t[0] = t0; + t[1] = t1; + t[2] = t2; + t[3] = t3; + t[4] = t4; + t[5] = t5; + t[6] = t6; + t[7] = t7; +} |