aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--driver/Clflags.ml3
-rw-r--r--driver/Compopts.v9
-rw-r--r--driver/Driver.ml3
-rw-r--r--extraction/extraction.v10
-rw-r--r--mppa_k1c/SelectLong.vp22
-rw-r--r--mppa_k1c/SelectLongproof.v19
-rw-r--r--mppa_k1c/SelectOp.vp29
-rw-r--r--mppa_k1c/SelectOpproof.v31
8 files changed, 97 insertions, 29 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index b1afab6f..651d644e 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -70,4 +70,5 @@ let use_standard_headers = ref Configuration.has_standard_headers
let option_fglobaladdrtmp = ref false
let option_fglobaladdroffset = ref false
let option_fxsaddr = ref true
-let option_coalesce_mem = ref true
+let option_faddx = ref false
+let option_fcoalesce_mem = ref true
diff --git a/driver/Compopts.v b/driver/Compopts.v
index f7de596c..9c6448b7 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -43,17 +43,20 @@ Parameter optim_redundancy: unit -> bool.
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.
+Parameter optim_globaladdrtmp: unit -> bool.
(** FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses (default false) *)
-Parameter optim_fglobaladdroffset: unit -> bool.
+Parameter optim_globaladdroffset: unit -> bool.
(** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *)
-Parameter optim_fxsaddr: unit -> bool.
+Parameter optim_xsaddr: unit -> bool.
(** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *)
Parameter optim_coalesce_mem: unit -> bool.
+(** FIXME TEMPORARY Flag -faddx. Fuse (default false) *)
+Parameter optim_addx: unit -> bool.
+
(** Flag -fthumb. For the ARM back-end. *)
Parameter thumb: unit -> bool.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index cfafcaa3..74e7ae77 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -375,7 +375,8 @@ let cmdline_actions =
@ f_opt "globaladdrtmp" option_fglobaladdrtmp
@ f_opt "globaladdroffset" option_fglobaladdroffset
@ f_opt "xsaddr" option_fxsaddr
- @ f_opt "coalesce-mem" option_coalesce_mem
+ @ f_opt "addx" option_faddx
+ @ f_opt "coalesce-mem" option_fcoalesce_mem
(* Code generation options *)
@ f_opt "fpu" option_ffpu
@ f_opt "sse" option_ffpu (* backward compatibility *)
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 979e1d49..e2ffd65d 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -117,14 +117,16 @@ Extract Constant Compopts.thumb =>
"fun _ -> !Clflags.option_mthumb".
Extract Constant Compopts.debug =>
"fun _ -> !Clflags.option_g".
-Extract Constant Compopts.optim_fglobaladdrtmp =>
+Extract Constant Compopts.optim_globaladdrtmp =>
"fun _ -> !Clflags.option_fglobaladdrtmp".
-Extract Constant Compopts.optim_fglobaladdroffset =>
+Extract Constant Compopts.optim_globaladdroffset =>
"fun _ -> !Clflags.option_fglobaladdroffset".
-Extract Constant Compopts.optim_fxsaddr =>
+Extract Constant Compopts.optim_xsaddr =>
"fun _ -> !Clflags.option_fxsaddr".
+Extract Constant Compopts.optim_addx =>
+ "fun _ -> !Clflags.option_faddx".
Extract Constant Compopts.optim_coalesce_mem =>
- "fun _ -> !Clflags.option_coalesce_mem".
+ "fun _ -> !Clflags.option_fcoalesce_mem".
(* Compiler *)
Extract Constant Compiler.print_Clight => "PrintClight.print_if".
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index fe739a01..2450ab97 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -67,10 +67,13 @@ Definition longofintu (e: expr) :=
(** ** Integer addition and pointer addition *)
Definition addlimm_shllimm sh k2 e1 :=
- match shift1_4_of_z (Int.unsigned sh) with
- | Some s14 => Eop (Oaddxlimm s14 k2) (e1:::Enil)
- | None => Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil)
- end.
+ if Compopts.optim_faddx tt
+ then
+ match shift1_4_of_z (Int.unsigned sh) with
+ | Some s14 => Eop (Oaddxlimm s14 k2) (e1:::Enil)
+ | None => Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil)
+ end
+ else Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil).
Nondetfunction addlimm (n: int64) (e: expr) :=
if Int64.eq n Int64.zero then e else
@@ -87,10 +90,13 @@ Nondetfunction addlimm (n: int64) (e: expr) :=
end.
Definition addl_shllimm n e1 e2 :=
- match shift1_4_of_z (Int.unsigned n) with
- | Some s14 => Eop (Oaddxl s14) (e1:::e2:::Enil)
- | None => Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil)
- end.
+ if Compopts.optim_faddx tt
+ then
+ match shift1_4_of_z (Int.unsigned n) with
+ | Some s14 => Eop (Oaddxl s14) (e1:::e2:::Enil)
+ | None => Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil)
+ end
+ else Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil).
Nondetfunction addl (e1: expr) (e2: expr) :=
if Archi.splitlong then SplitLong.addl e1 e2 else
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 3c9f64d5..58a4c39a 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -124,6 +124,8 @@ Theorem eval_addlimm_shllimm:
forall sh k2, unary_constructor_sound (addlimm_shllimm sh k2) (fun x => ExtValues.addxl sh x (Vlong k2)).
Proof.
red; unfold addlimm_shllimm; intros.
+ destruct (Compopts.optim_addx tt).
+ {
destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT.
- TrivialExists. simpl.
f_equal.
@@ -178,6 +180,13 @@ Proof.
repeat (try eassumption; try econstructor).
simpl.
reflexivity.
+ }
+ { unfold addxl. rewrite Val.addl_commut.
+ TrivialExists.
+ repeat (try eassumption; try econstructor).
+ simpl.
+ reflexivity.
+ }
Qed.
Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)).
@@ -188,7 +197,7 @@ Proof.
destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto.
destruct (addlimm_match a); InvEval.
- econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto.
-- destruct (Compopts.optim_fglobaladdroffset _).
+- destruct (Compopts.optim_globaladdroffset _).
+ econstructor; split. EvalOp. simpl; eauto.
unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto.
destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto.
@@ -211,6 +220,8 @@ Proof.
red.
intros.
unfold addl_shllimm.
+ destruct (Compopts.optim_addx tt).
+ {
destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT.
- TrivialExists.
simpl.
@@ -235,7 +246,11 @@ Proof.
discriminate.
(* Oaddxl *)
- TrivialExists;
- repeat econstructor; eassumption.
+ repeat econstructor; eassumption.
+ }
+ { TrivialExists;
+ repeat econstructor; eassumption.
+ }
Qed.
Theorem eval_addl: binary_constructor_sound addl Val.addl.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 3427dda3..4d2a948d 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -105,10 +105,13 @@ Definition addrstack (ofs: ptrofs) :=
(** ** Integer addition and pointer addition *)
Definition addimm_shlimm sh k2 e1 :=
- match shift1_4_of_z (Int.unsigned sh) with
- | Some s14 => Eop (Oaddximm s14 k2) (e1:::Enil)
- | None => Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil)
- end.
+ if Compopts.optim_faddx tt
+ then
+ match shift1_4_of_z (Int.unsigned sh) with
+ | Some s14 => Eop (Oaddximm s14 k2) (e1:::Enil)
+ | None => Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil)
+ end
+ else Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil).
Nondetfunction addimm (n: int) (e: expr) :=
if Int.eq n Int.zero then e else
@@ -123,10 +126,13 @@ Nondetfunction addimm (n: int) (e: expr) :=
end.
Definition add_shlimm n e1 e2 :=
- match shift1_4_of_z (Int.unsigned n) with
- | Some s14 => Eop (Oaddx s14) (e1:::e2:::Enil)
- | None => Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil)
- end.
+ if Compopts.optim_faddx tt
+ then
+ match shift1_4_of_z (Int.unsigned n) with
+ | Some s14 => Eop (Oaddx s14) (e1:::e2:::Enil)
+ | None => Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil)
+ end
+ else Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil).
Nondetfunction add (e1: expr) (e2: expr) :=
match e1, e2 with
@@ -611,6 +617,13 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
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 (Oaddxl sh) (e1:::e2:::Enil) =>
let zscale := ExtValues.z_of_shift1_4 sh in
let scale := Int.repr zscale in
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 8e1812c6..f5a90803 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -187,6 +187,8 @@ Theorem eval_addimm_shlimm:
forall sh k2, unary_constructor_sound (addimm_shlimm sh k2) (fun x => ExtValues.addx sh x (Vint k2)).
Proof.
red; unfold addimm_shlimm; intros.
+ destruct (Compopts.optim_addx tt).
+ {
destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT.
- TrivialExists. simpl.
f_equal.
@@ -241,6 +243,13 @@ Proof.
repeat (try eassumption; try econstructor).
simpl.
reflexivity.
+ }
+ { unfold addx. rewrite Val.add_commut.
+ TrivialExists.
+ repeat (try eassumption; try econstructor).
+ simpl.
+ reflexivity.
+ }
Qed.
Theorem eval_addimm:
@@ -272,6 +281,8 @@ Proof.
red.
intros.
unfold add_shlimm.
+ destruct (Compopts.optim_addx tt).
+ {
destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT.
- TrivialExists.
simpl.
@@ -295,7 +306,11 @@ Proof.
apply Int.repr_unsigned. }
discriminate.
- TrivialExists;
- repeat econstructor; eassumption.
+ repeat econstructor; eassumption.
+ }
+ { TrivialExists;
+ repeat econstructor; eassumption.
+ }
Qed.
Theorem eval_add: binary_constructor_sound add Val.add.
@@ -1377,8 +1392,20 @@ 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_xsaddr 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.
- unfold addxl in *.
- destruct (Compopts.optim_fxsaddr tt).
+ destruct (Compopts.optim_xsaddr tt).
+ unfold int_of_shift1_4 in *.
destruct (Z.eq_dec _ _).
* exists (v0 :: v1 :: nil); split.
generated by cgit (git 2.34.1) at 2024-06-02 22:07:09 +0000