diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 09:32:49 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 09:32:49 +0200 |
commit | 9f256a4ad30c93749e6c1192a84f996feac3b023 (patch) | |
tree | 81b381e5651e34474a133f012927442f64d51c56 | |
parent | 053cfa54205575ceb984f5922f51f4fce5980604 (diff) | |
download | compcert-kvx-9f256a4ad30c93749e6c1192a84f996feac3b023.tar.gz compcert-kvx-9f256a4ad30c93749e6c1192a84f996feac3b023.zip |
command line options (still incomplete)
-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/SelectOp.vp | 16 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 19 |
6 files changed, 46 insertions, 11 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 4d70d350..76afa4b4 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 c68c066a..505a1d35 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -367,6 +367,9 @@ let cmdline_actions = @ f_opt "postpass-ilp" option_fpostpass_ilp @ 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/SelectOp.vp b/mppa_k1c/SelectOp.vp index 28b91728..6adcebe5 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -54,6 +54,7 @@ Require Import OpHelpers. Require Import ExtValues. Require Import DecBoolOps. Require Import Chunks. +Require Compopts. Local Open Scope cminorsel_scope. @@ -582,14 +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) => - 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) + (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 a92ed572..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,11 +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 (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. + - 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. |