diff options
-rw-r--r-- | driver/Clflags.ml | 4 | ||||
-rw-r--r-- | driver/Compopts.v | 9 | ||||
-rw-r--r-- | driver/Driver.ml | 3 | ||||
-rw-r--r-- | extraction/extraction.v | 6 | ||||
-rw-r--r-- | mppa_k1c/Asm.v | 21 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 41 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 54 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 175 | ||||
-rw-r--r-- | mppa_k1c/Asmvliw.v | 23 | ||||
-rw-r--r-- | mppa_k1c/Chunks.v | 20 | ||||
-rw-r--r-- | mppa_k1c/ConstpropOp.vp | 2 | ||||
-rw-r--r-- | mppa_k1c/ConstpropOpproof.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Op.v | 13 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 10 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 24 | ||||
-rw-r--r-- | mppa_k1c/SelectOp.vp | 14 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 14 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 26 | ||||
-rw-r--r-- | mppa_k1c/ValueAOp.v | 1 | ||||
-rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 2 | ||||
-rw-r--r-- | test/monniaux/ocaml/config/Makefile | 2 |
23 files changed, 419 insertions, 55 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 5b8ad443..46f19dcf 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -66,3 +66,7 @@ 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 diff --git a/driver/Compopts.v b/driver/Compopts.v index e6eecc9b..3bb7a474 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -42,6 +42,15 @@ 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. + (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 2672ed99..35b5db86 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -372,6 +372,9 @@ let cmdline_actions = @ 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 (* 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..0f336916 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -117,6 +117,12 @@ 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". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d1ac8a67..d73d00c7 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -42,6 +42,7 @@ Definition preg := preg. Inductive addressing : Type :=
| AOff (ofs: offset)
| AReg (ro: ireg)
+ | ARegXS (ro: ireg)
.
(** Syntax *)
@@ -444,6 +445,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)
@@ -463,6 +475,15 @@ 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)
+
end.
Section RELSEM.
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index ed145f21..1988813f 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -268,10 +268,14 @@ Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ir 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_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 ge chunk 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 2e83fb44..1ee5002c 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. @@ -75,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. @@ -82,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. @@ -146,10 +149,17 @@ 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. @@ -169,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. @@ -355,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: @@ -363,6 +382,7 @@ Proof. destruct o1, o2; wlp_simplify; try discriminate. - congruence. - congruence. + - congruence. Qed. Hint Resolve load_op_eq_correct: wlp. Opaque load_op_eq_correct. @@ -374,6 +394,8 @@ Definition store_op_eq (o1 o2: store_op): ?? bool := match o2 with OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_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: @@ -382,6 +404,7 @@ Proof. destruct o1, o2; wlp_simplify; try discriminate. - congruence. - congruence. + - congruence. Qed. Hint Resolve store_op_eq_correct: wlp. Opaque store_op_eq_correct. @@ -612,8 +635,10 @@ 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))] | 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)); @@ -828,6 +853,13 @@ 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 *) @@ -845,6 +877,13 @@ Proof. eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. + (* 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. + (* Allocframe *) - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. * eexists; repeat split. @@ -1408,6 +1447,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 := @@ -1426,6 +1466,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 := diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 6cd31468..ca7094da 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -22,6 +22,7 @@ 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. @@ -807,31 +808,31 @@ 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. *) @@ -846,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 := @@ -885,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. @@ -914,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 40f9f08b..b265f221 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. *) @@ -2110,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 -> @@ -2133,6 +2154,32 @@ 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, @@ -2156,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 -> @@ -2199,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 -> @@ -2210,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: @@ -2241,6 +2317,33 @@ 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, @@ -2280,7 +2383,7 @@ 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' -> @@ -2327,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 -> @@ -2352,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 -> @@ -2362,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/Asmvliw.v b/mppa_k1c/Asmvliw.v index cf827818..e460727c 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -35,6 +35,7 @@ Require Stacklayout. Require Import Conventions. Require Import Errors. Require Import Sorting.Permutation. +Require Import Chunks. (** * Abstract syntax *) @@ -270,11 +271,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 *) @@ -290,11 +289,9 @@ 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) . -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 *) @@ -1123,6 +1120,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 @@ -1138,6 +1141,12 @@ 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 load_chunk n := match n with | Plb => Mint8signed @@ -1172,9 +1181,11 @@ 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 | Pallocframe sz pos => let (mw, stk) := Mem.alloc mr 0 sz in diff --git a/mppa_k1c/Chunks.v b/mppa_k1c/Chunks.v new file mode 100644 index 00000000..833f8116 --- /dev/null +++ b/mppa_k1c/Chunks.v @@ -0,0 +1,20 @@ +Require Import AST. +Require Import Values. +Require Import Integers. + +Local Open Scope Z_scope. + +Definition zscale_of_chunk (chunk: memory_chunk) := + 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/Op.v b/mppa_k1c/Op.v index baf17cc0..5e80589b 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -207,7 +207,8 @@ Inductive operation : Type := 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] *) @@ -230,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. @@ -513,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) @@ -703,8 +705,10 @@ Definition type_of_operation (op: operation) : list typ * typ := | 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 @@ -1117,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))) @@ -1661,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/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index b63dcb6c..abc3dcb6 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -216,15 +216,15 @@ 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)) ; 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 + | 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 } diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index bc90dd4c..43c8acb8 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -117,6 +117,17 @@ 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' -> @@ -140,6 +151,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 +177,11 @@ 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. - 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. diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 25f09e2e..6adcebe5 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -53,6 +53,8 @@ Require Import CminorSel. Require Import OpHelpers. Require Import ExtValues. Require Import DecBoolOps. +Require Import Chunks. +Require Compopts. Local Open Scope cminorsel_scope. @@ -581,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. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 6fa93fd8..9e2eec8b 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -1256,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. @@ -1265,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 506faa1c..62b02f58 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -166,7 +166,11 @@ module Target (*: TARGET*) = 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" @@ -342,26 +346,26 @@ 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 (* Arith R instructions *) diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 064686cc..643cca0c 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -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 diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index eb336edc..0a83a903 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -946,8 +946,10 @@ Proof. 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_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | 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 ge 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. - 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/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 |