aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--driver/Clflags.ml4
-rw-r--r--driver/Compopts.v9
-rw-r--r--driver/Driver.ml3
-rw-r--r--extraction/extraction.v6
-rw-r--r--mppa_k1c/Asm.v21
-rw-r--r--mppa_k1c/Asmblock.v4
-rw-r--r--mppa_k1c/Asmblockdeps.v41
-rw-r--r--mppa_k1c/Asmblockgen.v54
-rw-r--r--mppa_k1c/Asmblockgenproof.v4
-rw-r--r--mppa_k1c/Asmblockgenproof1.v175
-rw-r--r--mppa_k1c/Asmvliw.v23
-rw-r--r--mppa_k1c/Chunks.v20
-rw-r--r--mppa_k1c/ConstpropOp.vp2
-rw-r--r--mppa_k1c/ConstpropOpproof.v2
-rw-r--r--mppa_k1c/Op.v13
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml10
-rw-r--r--mppa_k1c/PostpassSchedulingproof.v24
-rw-r--r--mppa_k1c/SelectOp.vp14
-rw-r--r--mppa_k1c/SelectOpproof.v14
-rw-r--r--mppa_k1c/TargetPrinter.ml26
-rw-r--r--mppa_k1c/ValueAOp.v1
-rw-r--r--mppa_k1c/lib/Asmblockgenproof0.v2
-rw-r--r--test/monniaux/ocaml/config/Makefile2
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
generated by cgit (git 2.34.1) at 2024-07-02 11:50:48 +0000