From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Archi.v | 18 ++- arm/Asm.v | 79 ++++++++++++-- arm/Asmgen.v | 95 ++++++++++++---- arm/Asmgenproof.v | 9 +- arm/Asmgenproof1.v | 255 +++++++++++++++++++++++++++++++------------ arm/ConstpropOp.vp | 30 ++++- arm/ConstpropOpproof.v | 68 ++++++++---- arm/Machregs.v | 28 ++--- arm/NeedOp.v | 9 +- arm/Op.v | 112 ++++++++++++++++--- arm/PrintAsm.ml | 121 +++++++++++++------- arm/SelectOp.vp | 34 +++++- arm/SelectOpproof.v | 76 +++++++++++++ arm/ValueAOp.v | 17 +++ arm/eabi/Conventions1.v | 52 +++++++-- arm/hardfloat/Conventions1.v | 97 +++++++++++++--- 16 files changed, 864 insertions(+), 236 deletions(-) (limited to 'arm') diff --git a/arm/Archi.v b/arm/Archi.v index e693541..5657f31 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -25,12 +25,24 @@ Definition big_endian := false. Notation align_int64 := 8%Z (only parsing). Notation align_float64 := 8%Z (only parsing). -Program Definition default_pl : bool * nan_pl 53 := (false, nat_iter 51 xO xH). +Program Definition default_pl_64 : bool * nan_pl 53 := + (false, nat_iter 51 xO xH). -Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := +Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := (** Choose second NaN if pl2 is sNaN but pl1 is qNan. In all other cases, choose first NaN *) (Pos.testbit (proj1_sig pl1) 51 && negb (Pos.testbit (proj1_sig pl2) 51))%bool. -Global Opaque big_endian default_pl choose_binop_pl. +Program Definition default_pl_32 : bool * nan_pl 24 := + (false, nat_iter 22 xO xH). + +Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) := + (** Choose second NaN if pl2 is sNaN but pl1 is qNan. + In all other cases, choose first NaN *) + (Pos.testbit (proj1_sig pl1) 22 && + negb (Pos.testbit (proj1_sig pl2) 22))%bool. + +Global Opaque big_endian + default_pl_64 choose_binop_pl_64 + default_pl_32 choose_binop_pl_32. diff --git a/arm/Asm.v b/arm/Asm.v index 9d3ba5b..f054db0 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -143,6 +143,7 @@ Inductive instruction : Type := | Pcmp: ireg -> shift_op -> instruction (**r integer comparison *) | Peor: ireg -> ireg -> shift_op -> instruction (**r bitwise exclusive or *) | Pldr: ireg -> ireg -> shift_addr -> instruction (**r int32 load *) + | Pldr_a: ireg -> ireg -> shift_addr -> instruction (**r any32 load to int register *) | Pldrb: ireg -> ireg -> shift_addr -> instruction (**r unsigned int8 load *) | Pldrh: ireg -> ireg -> shift_addr -> instruction (**r unsigned int16 load *) | Pldrsb: ireg -> ireg -> shift_addr -> instruction (**r signed int8 load *) @@ -155,6 +156,7 @@ Inductive instruction : Type := | Porr: ireg -> ireg -> shift_op -> instruction (**r bitwise or *) | Prsb: ireg -> ireg -> shift_op -> instruction (**r integer reverse subtraction *) | Pstr: ireg -> ireg -> shift_addr -> instruction (**r int32 store *) + | Pstr_a: ireg -> ireg -> shift_addr -> instruction (**r any32 store from int register *) | Pstrb: ireg -> ireg -> shift_addr -> instruction (**r int8 store *) | Pstrh: ireg -> ireg -> shift_addr -> instruction (**r int16 store *) | Psdiv: instruction (**r signed division *) @@ -172,15 +174,31 @@ Inductive instruction : Type := | Pfsubd: freg -> freg -> freg -> instruction (**r float subtraction *) | Pflid: freg -> float -> instruction (**r load float constant *) | Pfcmpd: freg -> freg -> instruction (**r float comparison *) - | Pfcmpzd: freg -> instruction (**r float comparison with 0.0 *) + | Pfcmpzd: freg -> instruction (**r float comparison with 0.0 *) | Pfsitod: freg -> ireg -> instruction (**r signed int to float *) | Pfuitod: freg -> ireg -> instruction (**r unsigned int to float *) | Pftosizd: ireg -> freg -> instruction (**r float to signed int *) | Pftouizd: ireg -> freg -> instruction (**r float to unsigned int *) - | Pfcvtsd: freg -> freg -> instruction (**r round to singled precision *) + | Pfabss: freg -> freg -> instruction (**r float absolute value *) + | Pfnegs: freg -> freg -> instruction (**r float opposite *) + | Pfadds: freg -> freg -> freg -> instruction (**r float addition *) + | Pfdivs: freg -> freg -> freg -> instruction (**r float division *) + | Pfmuls: freg -> freg -> freg -> instruction (**r float multiplication *) + | Pfsubs: freg -> freg -> freg -> instruction (**r float subtraction *) + | Pflis: freg -> float32 -> instruction (**r load float constant *) + | Pfcmps: freg -> freg -> instruction (**r float comparison *) + | Pfcmpzs: freg -> instruction (**r float comparison with 0.0 *) + | Pfsitos: freg -> ireg -> instruction (**r signed int to float *) + | Pfuitos: freg -> ireg -> instruction (**r unsigned int to float *) + | Pftosizs: ireg -> freg -> instruction (**r float to signed int *) + | Pftouizs: ireg -> freg -> instruction (**r float to unsigned int *) + | Pfcvtsd: freg -> freg -> instruction (**r round to single precision *) + | Pfcvtds: freg -> freg -> instruction (**r expand to double precision *) | Pfldd: freg -> ireg -> int -> instruction (**r float64 load *) + | Pfldd_a: freg -> ireg -> int -> instruction (**r any64 load to FP reg *) | Pflds: freg -> ireg -> int -> instruction (**r float32 load *) | Pfstd: freg -> ireg -> int -> instruction (**r float64 store *) + | Pfstd_a: freg -> ireg -> int -> instruction (**r any64 store from FP reg *) | Pfsts: freg -> ireg -> int -> instruction (**r float32 store *) (* Pseudo-instructions *) @@ -392,7 +410,7 @@ Definition compare_int (rs: regset) (v1 v2: val) (m: mem) := #CC <- (Val.cmpu (Mem.valid_pointer m) Cge v1 v2) #CV <- (Val.sub_overflow v1 v2). -(** Semantics of [fcmpd] instruction: +(** Semantics of [fcmp] instructions: << == N=0 Z=1 C=1 V=0 < N=1 Z=0 C=0 V=0 @@ -415,6 +433,20 @@ Definition compare_float (rs: regset) (v1 v2: val) := #CV <- Vundef end. +Definition compare_float32 (rs: regset) (v1 v2: val) := + match v1, v2 with + | Vsingle f1, Vsingle f2 => + rs#CN <- (Val.of_bool (Float32.cmp Clt f1 f2)) + #CZ <- (Val.of_bool (Float32.cmp Ceq f1 f2)) + #CC <- (Val.of_bool (negb (Float32.cmp Clt f1 f2))) + #CV <- (Val.of_bool (negb (Float32.cmp Ceq f1 f2 || Float32.cmp Clt f1 f2 || Float32.cmp Cgt f1 f2))) + | _, _ => + rs#CN <- Vundef + #CZ <- Vundef + #CC <- Vundef + #CV <- Vundef + end. + (** Testing a condition *) Definition eval_testcond (c: testcond) (rs: regset) : option bool := @@ -523,6 +555,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#r1 <- (Val.xor rs#r2 (eval_shift_op so rs)))) m | Pldr r1 r2 sa => exec_load Mint32 (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Pldr_a r1 r2 sa => + exec_load Many32 (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m | Pldrb r1 r2 sa => exec_load Mint8unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m | Pldrh r1 r2 sa => @@ -551,6 +585,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#r1 <- (Val.sub (eval_shift_op so rs) rs#r2))) m | Pstr r1 r2 sa => exec_store Mint32 (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Pstr_a r1 r2 sa => + exec_store Many32 (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m | Pstrb r1 r2 sa => exec_store Mint8unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m | Pstrh r1 r2 sa => @@ -606,19 +642,48 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs #FR6 <- Vundef #r1 <- (Val.maketotal (Val.intoffloat rs#r2)))) m | Pftouizd r1 r2 => Next (nextinstr (rs #FR6 <- Vundef #r1 <- (Val.maketotal (Val.intuoffloat rs#r2)))) m + | Pfabss r1 r2 => + Next (nextinstr (rs#r1 <- (Val.absfs rs#r2))) m + | Pfnegs r1 r2 => + Next (nextinstr (rs#r1 <- (Val.negfs rs#r2))) m + | Pfadds r1 r2 r3 => + Next (nextinstr (rs#r1 <- (Val.addfs rs#r2 rs#r3))) m + | Pfdivs r1 r2 r3 => + Next (nextinstr (rs#r1 <- (Val.divfs rs#r2 rs#r3))) m + | Pfmuls r1 r2 r3 => + Next (nextinstr (rs#r1 <- (Val.mulfs rs#r2 rs#r3))) m + | Pfsubs r1 r2 r3 => + Next (nextinstr (rs#r1 <- (Val.subfs rs#r2 rs#r3))) m + | Pflis r1 f => + Next (nextinstr (rs#r1 <- (Vsingle f))) m + | Pfcmps r1 r2 => + Next (nextinstr (compare_float32 rs rs#r1 rs#r2)) m + | Pfcmpzs r1 => + Next (nextinstr (compare_float32 rs rs#r1 (Vsingle Float32.zero))) m + | Pfsitos r1 r2 => + Next (nextinstr (rs#r1 <- (Val.maketotal (Val.singleofint rs#r2)))) m + | Pfuitos r1 r2 => + Next (nextinstr (rs#r1 <- (Val.maketotal (Val.singleofintu rs#r2)))) m + | Pftosizs r1 r2 => + Next (nextinstr (rs #FR6 <- Vundef #r1 <- (Val.maketotal (Val.intofsingle rs#r2)))) m + | Pftouizs r1 r2 => + Next (nextinstr (rs #FR6 <- Vundef #r1 <- (Val.maketotal (Val.intuofsingle rs#r2)))) m | Pfcvtsd r1 r2 => Next (nextinstr (rs#r1 <- (Val.singleoffloat rs#r2))) m + | Pfcvtds r1 r2 => + Next (nextinstr (rs#r1 <- (Val.floatofsingle rs#r2))) m | Pfldd r1 r2 n => exec_load Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m + | Pfldd_a r1 r2 n => + exec_load Many64 (Val.add rs#r2 (Vint n)) r1 rs m | Pflds r1 r2 n => exec_load Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m | Pfstd r1 r2 n => exec_store Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m + | Pfstd_a r1 r2 n => + exec_store Many64 (Val.add rs#r2 (Vint n)) r1 rs m | Pfsts r1 r2 n => - match exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m with - | Next rs' m' => Next (rs'#FR6 <- Vundef) m' - | Stuck => Stuck - end + exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m (* Pseudo-instructions *) | Pallocframe sz pos => let (m1, stk) := Mem.alloc m 0 sz in diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 2513a5e..fa4faa6 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -185,6 +185,18 @@ Definition transl_cond | Cnotcompfzero cmp, a1 :: nil => do r1 <- freg_of a1; OK (Pfcmpzd r1 :: k) + | Ccompfs cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmps r1 r2 :: k) + | Cnotcompfs cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmps r1 r2 :: k) + | Ccompfszero cmp, a1 :: nil => + do r1 <- freg_of a1; + OK (Pfcmpzs r1 :: k) + | Cnotcompfszero cmp, a1 :: nil => + do r1 <- freg_of a1; + OK (Pfcmpzs r1 :: k) | _, _ => Error(msg "Asmgen.transl_cond") end. @@ -241,6 +253,10 @@ Definition cond_for_cond (cond: condition) := | Cnotcompf cmp => cond_for_float_not_cmp cmp | Ccompfzero cmp => cond_for_float_cmp cmp | Cnotcompfzero cmp => cond_for_float_not_cmp cmp + | Ccompfs cmp => cond_for_float_cmp cmp + | Cnotcompfs cmp => cond_for_float_not_cmp cmp + | Ccompfszero cmp => cond_for_float_cmp cmp + | Cnotcompfszero cmp => cond_for_float_not_cmp cmp end. (** Translation of the arithmetic operation [r <- op(args)]. @@ -261,6 +277,9 @@ Definition transl_op | Ofloatconst f, nil => do r <- freg_of res; OK (Pflid r f :: k) + | Osingleconst f, nil => + do r <- freg_of res; + OK (Pflis r f :: k) | Oaddrsymbol s ofs, nil => do r <- ireg_of res; OK (Ploadsymbol r s ofs :: k) @@ -400,9 +419,30 @@ Definition transl_op | Odivf, a1 :: a2 :: nil => do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; OK (Pfdivd r r1 r2 :: k) + | Onegfs, a1 :: nil => + do r <- freg_of res; do r1 <- freg_of a1; + OK (Pfnegs r r1 :: k) + | Oabsfs, a1 :: nil => + do r <- freg_of res; do r1 <- freg_of a1; + OK (Pfabss r r1 :: k) + | Oaddfs, a1 :: a2 :: nil => + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfadds r r1 r2 :: k) + | Osubfs, a1 :: a2 :: nil => + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfsubs r r1 r2 :: k) + | Omulfs, a1 :: a2 :: nil => + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfmuls r r1 r2 :: k) + | Odivfs, a1 :: a2 :: nil => + do r <- freg_of res; do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfdivs r r1 r2 :: k) | Osingleoffloat, a1 :: nil => do r <- freg_of res; do r1 <- freg_of a1; OK (Pfcvtsd r r1 :: k) + | Ofloatofsingle, a1 :: nil => + do r <- freg_of res; do r1 <- freg_of a1; + OK (Pfcvtds r r1 :: k) | Ointoffloat, a1 :: nil => do r <- ireg_of res; do r1 <- freg_of a1; OK (Pftosizd r r1 :: k) @@ -415,6 +455,18 @@ Definition transl_op | Ofloatofintu, a1 :: nil => do r <- freg_of res; do r1 <- ireg_of a1; OK (Pfuitod r r1 :: k) + | Ointofsingle, a1 :: nil => + do r <- ireg_of res; do r1 <- freg_of a1; + OK (Pftosizs r r1 :: k) + | Ointuofsingle, a1 :: nil => + do r <- ireg_of res; do r1 <- freg_of a1; + OK (Pftouizs r r1 :: k) + | Osingleofint, a1 :: nil => + do r <- freg_of res; do r1 <- ireg_of a1; + OK (Pfsitos r r1 :: k) + | Osingleofintu, a1 :: nil => + do r <- freg_of res; do r1 <- ireg_of a1; + OK (Pfuitos r r1 :: k) | Ocmp cmp, _ => do r <- ireg_of res; transl_cond cmp args @@ -440,31 +492,34 @@ Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) := indexed_memory_access (fun base n => Pldr dst base (SAimm n)) mk_immed_mem_word base ofs k. Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := - match ty with - | Tint => - do r <- ireg_of dst; OK (loadind_int base ofs r k) - | Tfloat => - do r <- freg_of dst; - OK (indexed_memory_access (Pfldd r) mk_immed_mem_float base ofs k) - | Tsingle => - do r <- freg_of dst; + match ty, preg_of dst with + | Tint, IR r => + OK (indexed_memory_access (fun base n => Pldr r base (SAimm n)) mk_immed_mem_word base ofs k) + | Tany32, IR r => + OK (indexed_memory_access (fun base n => Pldr_a r base (SAimm n)) mk_immed_mem_word base ofs k) + | Tsingle, FR r => OK (indexed_memory_access (Pflds r) mk_immed_mem_float base ofs k) - | Tlong => + | Tfloat, FR r => + OK (indexed_memory_access (Pfldd r) mk_immed_mem_float base ofs k) + | Tany64, FR r => + OK (indexed_memory_access (Pfldd_a r) mk_immed_mem_float base ofs k) + | _, _ => Error (msg "Asmgen.loadind") end. Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := - match ty with - | Tint => - do r <- ireg_of src; + match ty, preg_of src with + | Tint, IR r => OK (indexed_memory_access (fun base n => Pstr r base (SAimm n)) mk_immed_mem_word base ofs k) - | Tfloat => - do r <- freg_of src; - OK (indexed_memory_access (Pfstd r) mk_immed_mem_float base ofs k) - | Tsingle => - do r <- freg_of src; + | Tany32, IR r => + OK (indexed_memory_access (fun base n => Pstr_a r base (SAimm n)) mk_immed_mem_word base ofs k) + | Tsingle, FR r => OK (indexed_memory_access (Pfsts r) mk_immed_mem_float base ofs k) - | Tlong => + | Tfloat, FR r => + OK (indexed_memory_access (Pfstd r) mk_immed_mem_float base ofs k) + | Tany64, FR r => + OK (indexed_memory_access (Pfstd_a r) mk_immed_mem_float base ofs k) + | _, _ => Error (msg "Asmgen.storeind") end. @@ -546,7 +601,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access_float Pflds mk_immed_mem_float dst addr args k | Mfloat64 => transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k - | Mint64 => + | _ => Error (msg "Asmgen.transl_load") end. @@ -567,7 +622,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) transl_memory_access_float Pfsts mk_immed_mem_float src addr args k | Mfloat64 => transl_memory_access_float Pfstd mk_immed_mem_float src addr args k - | Mint64 => + | _ => Error (msg "Asmgen.transl_store") end. diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index cfe4f54..341f6a0 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -237,16 +237,15 @@ Hint Resolve indexed_memory_access_label. Remark loadind_label: forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> tail_nolabel k c. Proof. - intros. destruct ty; monadInv H. - unfold loadind_int; TailNoLabel. - TailNoLabel. - TailNoLabel. + unfold loadind, loadind_int; intros; + destruct ty, (preg_of dst); inv H; TailNoLabel. Qed. Remark storeind_label: forall base ofs ty src k c, storeind src base ofs ty k = OK c -> tail_nolabel k c. Proof. - intros. destruct ty; monadInv H; TailNoLabel. + unfold storeind; intros; + destruct ty, (preg_of src); inv H; TailNoLabel. Qed. Remark transl_cond_label: diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 3e00217..a0d6752 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -405,22 +405,6 @@ Proof. split. Simpl. intros; Simpl. Qed. -(* -Lemma loadind_float_correct: - forall (base: ireg) ofs dst (rs: regset) m v k, - Mem.loadv Mfloat64al32 m (Val.add rs#base (Vint ofs)) = Some v -> - exists rs', - exec_straight ge fn (loadind_float base ofs dst k) rs m k rs' m - /\ rs'#dst = v - /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. -Proof. - intros; unfold loadind_float. apply indexed_memory_access_correct; intros. - econstructor; split. - apply exec_straight_one. simpl. unfold exec_load. rewrite H0; rewrite H; eauto. auto. - split. Simpl. intros; Simpl. -Qed. -*) - Lemma loadind_correct: forall (base: ireg) ofs ty dst k c (rs: regset) m v, loadind base ofs ty dst k = OK c -> @@ -430,56 +414,32 @@ Lemma loadind_correct: /\ rs'#(preg_of dst) = v /\ forall r, r <> PC -> r <> IR14 -> r <> preg_of dst -> rs'#r = rs#r. Proof. - unfold loadind; intros. - destruct ty; monadInv H. + unfold loadind; intros. destruct ty; destruct (preg_of dst); inv H; simpl in H0. - (* int *) - erewrite ireg_of_eq by eauto. apply loadind_int_correct; auto. + apply loadind_int_correct; auto. - (* float *) - erewrite freg_of_eq by eauto. simpl in H0. apply indexed_memory_access_correct; intros. econstructor; split. apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. split. Simpl. intros; Simpl. - (* single *) - erewrite freg_of_eq by eauto. simpl in H0. apply indexed_memory_access_correct; intros. econstructor; split. apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. split. Simpl. intros; Simpl. -Qed. - -(** Indexed memory stores. *) - -(* -Lemma storeind_int_correct: - forall (base: ireg) ofs (src: ireg) (rs: regset) m m' k, - Mem.storev Mint32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' -> - src <> IR14 -> - exists rs', - exec_straight ge fn (storeind_int src base ofs k) rs m k rs' m' - /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. -Proof. - intros; unfold storeind_int. apply indexed_memory_access_correct; intros. +- (* any32 *) + apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. - rewrite H1. rewrite H2; auto with asmgen. rewrite H; eauto. auto. - intros; Simpl. -Qed. - -Lemma storeind_float_correct: - forall (base: ireg) ofs (src: freg) (rs: regset) m m' k, - Mem.storev Mfloat64al32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' -> - exists rs', - exec_straight ge fn (storeind_float src base ofs k) rs m k rs' m' - /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. -Proof. - intros; unfold storeind_float. apply indexed_memory_access_correct; intros. + apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. + split. Simpl. intros; Simpl. +- (* any64 *) + apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. - rewrite H0. rewrite H1; auto with asmgen. rewrite H; eauto. auto. - intros; Simpl. + apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. + split. Simpl. intros; Simpl. Qed. -*) + +(** Indexed memory stores. *) Lemma storeind_correct: forall (base: ireg) ofs ty src k c (rs: regset) m m', @@ -490,29 +450,38 @@ Lemma storeind_correct: /\ forall r, r <> PC -> r <> IR14 -> preg_notin r (destroyed_by_setstack ty) -> rs'#r = rs#r. Proof. unfold storeind; intros. - destruct ty; monadInv H; simpl in H0. + assert (NOT14: preg_of src <> IR IR14) by eauto with asmgen. + destruct ty; destruct (preg_of src); inv H; simpl in H0. - (* int *) - erewrite ireg_of_eq in H0 by eauto. apply indexed_memory_access_correct; intros. econstructor; split. apply exec_straight_one. simpl. unfold exec_store. - rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. - assert (IR x <> IR IR14) by eauto with asmgen. congruence. - auto. intros; Simpl. + rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. + intros; Simpl. - (* float *) - erewrite freg_of_eq in H0 by eauto. apply indexed_memory_access_correct; intros. econstructor; split. apply exec_straight_one. simpl. unfold exec_store. - rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. - auto. intros; Simpl. + rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. + intros; Simpl. - (* single *) - erewrite freg_of_eq in H0 by eauto. apply indexed_memory_access_correct; intros. econstructor; split. apply exec_straight_one. simpl. unfold exec_store. - rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. - auto. intros; Simpl. + rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. + intros; Simpl. +- (* any32 *) + apply indexed_memory_access_correct; intros. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. + rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. + intros; Simpl. +- (* any64 *) + apply indexed_memory_access_correct; intros. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. + rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. + intros; Simpl. Qed. (** Translation of shift immediates *) @@ -775,6 +744,112 @@ Proof. exfalso; eapply Float.cmp_lt_gt_false; eauto. Qed. +Lemma compare_float32_spec: + forall rs f1 f2, + let rs1 := nextinstr (compare_float32 rs (Vsingle f1) (Vsingle f2)) in + rs1#CN = Val.of_bool (Float32.cmp Clt f1 f2) + /\ rs1#CZ = Val.of_bool (Float32.cmp Ceq f1 f2) + /\ rs1#CC = Val.of_bool (negb (Float32.cmp Clt f1 f2)) + /\ rs1#CV = Val.of_bool (negb (Float32.cmp Ceq f1 f2 || Float32.cmp Clt f1 f2 || Float32.cmp Cgt f1 f2)). +Proof. + intros. intuition. +Qed. + +Lemma compare_float32_inv: + forall rs v1 v2, + let rs1 := nextinstr (compare_float32 rs v1 v2) in + forall r', data_preg r' = true -> rs1#r' = rs#r'. +Proof. + intros. unfold rs1, compare_float32. + assert (nextinstr (rs#CN <- Vundef #CZ <- Vundef #CC <- Vundef #CV <- Vundef) r' = rs r'). + { repeat Simplif. } + destruct v1; destruct v2; auto. + repeat Simplif. +Qed. + +Lemma compare_float32_nextpc: + forall rs v1 v2, + nextinstr (compare_float32 rs v1 v2) PC = Val.add (rs PC) Vone. +Proof. + intros. unfold compare_float32. destruct v1; destruct v2; reflexivity. +Qed. + +Lemma cond_for_float32_cmp_correct: + forall c n1 n2 rs, + eval_testcond (cond_for_float_cmp c) + (nextinstr (compare_float32 rs (Vsingle n1) (Vsingle n2))) = + Some(Float32.cmp c n1 n2). +Proof. + intros. + generalize (compare_float32_spec rs n1 n2). + set (rs' := nextinstr (compare_float32 rs (Vsingle n1) (Vsingle n2))). + intros [A [B [C D]]]. + unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. + destruct c; simpl. +(* eq *) + destruct (Float32.cmp Ceq n1 n2); auto. +(* ne *) + rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq n1 n2); auto. +(* lt *) + destruct (Float32.cmp Clt n1 n2); auto. +(* le *) + rewrite Float32.cmp_le_lt_eq. + destruct (Float32.cmp Clt n1 n2); destruct (Float32.cmp Ceq n1 n2); auto. +(* gt *) + destruct (Float32.cmp Ceq n1 n2) eqn:EQ; + destruct (Float32.cmp Clt n1 n2) eqn:LT; + destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float32.cmp_lt_gt_false; eauto. + exfalso; eapply Float32.cmp_gt_eq_false; eauto. + exfalso; eapply Float32.cmp_lt_gt_false; eauto. +(* ge *) + rewrite Float32.cmp_ge_gt_eq. + destruct (Float32.cmp Ceq n1 n2) eqn:EQ; + destruct (Float32.cmp Clt n1 n2) eqn:LT; + destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float32.cmp_lt_eq_false; eauto. + exfalso; eapply Float32.cmp_lt_eq_false; eauto. + exfalso; eapply Float32.cmp_lt_gt_false; eauto. +Qed. + +Lemma cond_for_float32_not_cmp_correct: + forall c n1 n2 rs, + eval_testcond (cond_for_float_not_cmp c) + (nextinstr (compare_float32 rs (Vsingle n1) (Vsingle n2)))= + Some(negb(Float32.cmp c n1 n2)). +Proof. + intros. + generalize (compare_float32_spec rs n1 n2). + set (rs' := nextinstr (compare_float32 rs (Vsingle n1) (Vsingle n2))). + intros [A [B [C D]]]. + unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. + destruct c; simpl. +(* eq *) + destruct (Float32.cmp Ceq n1 n2); auto. +(* ne *) + rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq n1 n2); auto. +(* lt *) + destruct (Float32.cmp Clt n1 n2); auto. +(* le *) + rewrite Float32.cmp_le_lt_eq. + destruct (Float32.cmp Clt n1 n2) eqn:LT; destruct (Float32.cmp Ceq n1 n2) eqn:EQ; auto. +(* gt *) + destruct (Float32.cmp Ceq n1 n2) eqn:EQ; + destruct (Float32.cmp Clt n1 n2) eqn:LT; + destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float32.cmp_lt_gt_false; eauto. + exfalso; eapply Float32.cmp_gt_eq_false; eauto. + exfalso; eapply Float32.cmp_lt_gt_false; eauto. +(* ge *) + rewrite Float32.cmp_ge_gt_eq. + destruct (Float32.cmp Ceq n1 n2) eqn:EQ; + destruct (Float32.cmp Clt n1 n2) eqn:LT; + destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float32.cmp_lt_eq_false; eauto. + exfalso; eapply Float32.cmp_lt_eq_false; eauto. + exfalso; eapply Float32.cmp_lt_gt_false; eauto. +Qed. + Ltac ArgsInv := repeat (match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -881,6 +956,37 @@ Local Opaque compare_float. simpl. apply cond_for_float_not_cmp_correct. Local Opaque compare_float. simpl. apply cond_for_float_not_cmp_correct. exact I. apply compare_float_inv. +- (* Ccompfs *) + econstructor. + split. apply exec_straight_one. simpl. eauto. apply compare_float32_nextpc. + split. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) eqn:CMP; auto. + destruct (rs x); try discriminate. destruct (rs x0); try discriminate. + simpl in CMP. inv CMP. apply cond_for_float32_cmp_correct. + apply compare_float32_inv. +- (* Cnotcompfs *) + econstructor. + split. apply exec_straight_one. simpl. eauto. apply compare_float32_nextpc. + split. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) eqn:CMP; auto. + destruct (rs x); try discriminate. destruct (rs x0); try discriminate. + simpl in CMP. inv CMP. +Local Opaque compare_float32. simpl. apply cond_for_float32_not_cmp_correct. + exact I. + apply compare_float32_inv. +- (* Ccompfszero *) + econstructor. + split. apply exec_straight_one. simpl. eauto. apply compare_float32_nextpc. + split. destruct (Val.cmpfs_bool c0 (rs x) (Vsingle Float32.zero)) eqn:CMP; auto. + destruct (rs x); try discriminate. + simpl in CMP. inv CMP. apply cond_for_float32_cmp_correct. + apply compare_float32_inv. +- (* Cnotcompfzero *) + econstructor. + split. apply exec_straight_one. simpl. eauto. apply compare_float32_nextpc. + split. destruct (Val.cmpfs_bool c0 (rs x) (Vsingle Float32.zero)) eqn:CMP; auto. + destruct (rs x); try discriminate. simpl in CMP. inv CMP. + simpl. apply cond_for_float32_not_cmp_correct. + exact I. + apply compare_float32_inv. Qed. (** Translation of arithmetic operations. *) @@ -1039,6 +1145,18 @@ Transparent destroyed_by_op. (* floatofintu *) econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. intuition Simpl. + (* intofsingle *) + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + simpl. intuition Simpl. + (* intuofsingle *) + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + simpl. intuition Simpl. + (* singleofint *) + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + intuition Simpl. + (* singleofintu *) + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + intuition Simpl. (* Ocmp *) contradiction. Qed. @@ -1234,6 +1352,8 @@ Proof. discriminate. eapply transl_load_float_correct; eauto. eapply transl_load_float_correct; eauto. + discriminate. + discriminate. Qed. Lemma transl_store_correct: @@ -1256,13 +1376,10 @@ Proof. - eapply transl_store_int_correct; eauto. - eapply transl_store_int_correct; eauto. - discriminate. -- unfold transl_memory_access_float in H. monadInv H. rewrite (freg_of_eq _ _ EQ) in *. - eapply transl_memory_access_correct; eauto. - intros. econstructor; split. apply exec_straight_one. - simpl. unfold exec_store. rewrite H. rewrite H2; eauto with asmgen. - rewrite H1. eauto. auto. intros. Simpl. - simpl; auto. - eapply transl_store_float_correct; eauto. +- eapply transl_store_float_correct; eauto. +- discriminate. +- discriminate. Qed. End CONSTRUCTORS. diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 2b658a4..4f4bf5a 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -70,6 +70,22 @@ Nondetfunction cond_strength_reduction if Float.eq_dec n2 Float.zero then (Cnotcompfzero c, r1 :: nil) else (cond, args) + | Ccompfs c, r1 :: r2 :: nil, FS n1 :: v2 :: nil => + if Float32.eq_dec n1 Float32.zero + then (Ccompfszero (swap_comparison c), r2 :: nil) + else (cond, args) + | Ccompfs c, r1 :: r2 :: nil, v1 :: FS n2 :: nil => + if Float32.eq_dec n2 Float32.zero + then (Ccompfszero c, r1 :: nil) + else (cond, args) + | Cnotcompfs c, r1 :: r2 :: nil, FS n1 :: v2 :: nil => + if Float32.eq_dec n1 Float32.zero + then (Cnotcompfszero (swap_comparison c), r2 :: nil) + else (cond, args) + | Cnotcompfs c, r1 :: r2 :: nil, v1 :: FS n2 :: nil => + if Float32.eq_dec n2 Float32.zero + then (Cnotcompfszero c, r1 :: nil) + else (cond, args) | _, _, _ => (cond, args) end. @@ -164,18 +180,19 @@ Definition make_xorimm (n: int) (r: reg) := else (Oxorimm n, r :: nil). Definition make_mulfimm (n: float) (r r1 r2: reg) := - if Float.eq_dec n (Float.floatofint (Int.repr 2)) + if Float.eq_dec n (Float.of_int (Int.repr 2)) then (Oaddf, r :: r :: nil) else (Omulf, r1 :: r2 :: nil). +Definition make_mulfsimm (n: float32) (r r1 r2: reg) := + if Float32.eq_dec n (Float32.of_int (Int.repr 2)) + then (Oaddfs, r :: r :: nil) + else (Omulfs, r1 :: r2 :: nil). + Definition make_cast8signed (r: reg) (a: aval) := if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). Definition make_cast16signed (r: reg) (a: aval) := if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). -Definition make_singleoffloat (r: reg) (a: aval) := - if vincl a Fsingle && generate_float_constants tt - then (Omove, r :: nil) - else (Osingleoffloat, r :: nil). Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := @@ -207,10 +224,11 @@ Nondetfunction op_strength_reduction | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2 | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2 | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2 - | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1 | Ocmp c, args, vl => make_cmp c args vl | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2 | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2 + | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => make_mulfsimm n2 r1 r1 r2 + | Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil => make_mulfsimm n1 r2 r1 r2 | _, _, _ => (op, args) end. diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 00ea8bc..597c960 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -80,6 +80,10 @@ Ltac SimplVM := let E := fresh in assert (E: v = Vfloat n) by (inversion H; auto); rewrite E in *; clear H; SimplVM + | [ H: vmatch _ ?v (FS ?n) |- _ ] => + let E := fresh in + assert (E: v = Vsingle n) by (inversion H; auto); + rewrite E in *; clear H; SimplVM | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] => let E := fresh in assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); @@ -123,6 +127,18 @@ Proof. - destruct (Float.eq_dec n2 Float.zero); simpl; auto. subst n2; auto. rewrite H1; auto. +- destruct (Float32.eq_dec n1 Float32.zero). + subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float32.cmp_swap. auto. + simpl. rewrite H1; auto. +- destruct (Float32.eq_dec n2 Float32.zero). + subst n2. simpl. auto. + simpl. rewrite H1; auto. +- destruct (Float32.eq_dec n1 Float32.zero). + subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float32.cmp_swap. auto. + simpl. rewrite H1; auto. +- destruct (Float32.eq_dec n2 Float32.zero); simpl; auto. + subst n2; auto. + rewrite H1; auto. - auto. Qed. @@ -335,7 +351,7 @@ Lemma make_mulfimm_correct: exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. - destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. + destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. simpl. econstructor; split. eauto. rewrite H; subst n. destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto. simpl. econstructor; split; eauto. @@ -348,13 +364,40 @@ Lemma make_mulfimm_correct_2: exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. - destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. + destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. simpl. econstructor; split. eauto. rewrite H; subst n. destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto. rewrite Float.mul_commut; auto. simpl. econstructor; split; eauto. Qed. +Lemma make_mulfsimm_correct: + forall n r1 r2, + rs#r2 = Vsingle n -> + let (op, args) := make_mulfsimm n r1 r1 r2 in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. +Proof. + intros; unfold make_mulfsimm. + destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. + simpl. econstructor; split. eauto. rewrite H; subst n. + destruct (rs#r1); simpl; auto. rewrite Float32.mul2_add; auto. + simpl. econstructor; split; eauto. +Qed. + +Lemma make_mulfsimm_correct_2: + forall n r1 r2, + rs#r1 = Vsingle n -> + let (op, args) := make_mulfsimm n r2 r1 r2 in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. +Proof. + intros; unfold make_mulfsimm. + destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. + simpl. econstructor; split. eauto. rewrite H; subst n. + destruct (rs#r2); simpl; auto. rewrite Float32.mul2_add; auto. + rewrite Float32.mul_commut; auto. + simpl. econstructor; split; eauto. +Qed. + Lemma make_cast8signed_correct: forall r x, vmatch bc rs#r x -> @@ -383,21 +426,6 @@ Proof. econstructor; split; simpl; eauto. Qed. -Lemma make_singleoffloat_correct: - forall r x, - vmatch bc rs#r x -> - let (op, args) := make_singleoffloat r x in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.singleoffloat rs#r) v. -Proof. - intros; unfold make_singleoffloat. - destruct (vincl x Fsingle && generate_float_constants tt) eqn:INCL. - InvBooleans. exists rs#r; split; auto. - assert (V: vmatch bc rs#r Fsingle). - { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite Float.singleoffloat_of_single by auto. auto. - econstructor; split; simpl; eauto. -Qed. - Lemma op_strength_reduction_correct: forall op args vl v, vl = map (fun r => AE.get r ae) args -> @@ -459,14 +487,16 @@ Proof. InvApproxRegs; SimplVM. inv H0. apply make_shrimm_correct; auto. (* shru *) InvApproxRegs; SimplVM. inv H0. apply make_shruimm_correct; auto. -(* singleoffloat *) - InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto. (* cmp *) inv H0. apply make_cmp_correct; auto. (* mulf *) InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto. InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2). rewrite <- H2. apply make_mulfimm_correct_2; auto. +(* mulfs *) + InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfsimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. fold (Val.mulfs (Vsingle n1) rs#r2). + rewrite <- H2. apply make_mulfsimm_correct_2; auto. (* default *) exists v; auto. Qed. diff --git a/arm/Machregs.v b/arm/Machregs.v index b55259b..791ccbb 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -44,14 +44,10 @@ Global Opaque mreg_eq. Definition mreg_type (r: mreg): typ := match r with - | R0 => Tint | R1 => Tint | R2 => Tint | R3 => Tint - | R4 => Tint | R5 => Tint | R6 => Tint | R7 => Tint - | R8 => Tint | R9 => Tint | R10 => Tint | R11 => Tint - | R12 => Tint - | F0 => Tfloat | F1 => Tfloat | F2 => Tfloat | F3 => Tfloat - | F4 => Tfloat| F5 => Tfloat | F6 => Tfloat | F7 => Tfloat - | F8 => Tfloat | F9 => Tfloat | F10 => Tfloat | F11 => Tfloat - | F12 => Tfloat | F13 => Tfloat | F14 => Tfloat | F15 => Tfloat + | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 + | R8 | R9 | R10 | R11 | R12 => Tany32 + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 + | F8 | F9 | F10 | F11 | F12 | F13 | F14 | F15 => Tany64 end. Open Scope positive_scope. @@ -84,18 +80,14 @@ Definition is_stack_reg (r: mreg) : bool := false. Definition destroyed_by_op (op: operation): list mreg := match op with | Odiv | Odivu => R0 :: R1 :: R2 :: R3 :: R12 :: nil - | Ointoffloat | Ointuoffloat => F6 :: nil + | Ointoffloat | Ointuoffloat | Ointofsingle | Ointuofsingle => F6 :: nil | _ => nil end. Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg := nil. -Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg := - match chunk with - | Mfloat32 => F6 :: nil - | _ => nil - end. +Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg := nil. Definition destroyed_by_cond (cond: condition): list mreg := nil. @@ -106,16 +98,10 @@ Definition destroyed_by_jumptable: list mreg := Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_memcpy sz al => if zle sz 32 then nil else R2 :: R3 :: R12 :: nil - | EF_vstore Mfloat32 => F6 :: nil - | EF_vstore_global Mfloat32 _ _ => F6 :: nil | _ => nil end. -Definition destroyed_by_setstack (ty: typ): list mreg := - match ty with - | Tsingle => F6 :: nil - | _ => nil - end. +Definition destroyed_by_setstack (ty: typ): list mreg := nil. Definition destroyed_at_function_entry: list mreg := R12 :: nil. diff --git a/arm/NeedOp.v b/arm/NeedOp.v index 3fb0d72..e91ea64 100644 --- a/arm/NeedOp.v +++ b/arm/NeedOp.v @@ -42,6 +42,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Omove => nv::nil | Ointconst n => nil | Ofloatconst n => nil + | Osingleconst n => nil | Oaddrsymbol id ofs => nil | Oaddrstack ofs => nil | Ocast8signed => op1 (sign_ext 8 nv) @@ -74,8 +75,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshrximm _ => op1 (default nv) | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) - | Osingleoffloat => op1 (singleoffloat nv) + | Onegfs | Oabsfs => op1 (default nv) + | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) + | Ofloatofsingle | Osingleoffloat => op1 (default nv) | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv) + | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocmp c => needs_of_condition c @@ -87,7 +91,6 @@ Definition operation_is_redundant (op: operation) (nv: nval): bool := | Ocast16signed => sign_ext_redundant 16 nv | Oandimm n => andimm_redundant nv n | Oorimm n => orimm_redundant nv n - | Osingleoffloat => singleoffloat_redundant nv | _ => false end. @@ -180,7 +183,6 @@ Proof. - apply notint_sound; auto. - apply notint_sound. apply needs_of_shift_sound; auto. - apply needs_of_shift_sound; auto. -- apply singleoffloat_sound; auto. Qed. Lemma operation_is_redundant_sound: @@ -195,7 +197,6 @@ Proof. - apply sign_ext_redundant_sound; auto. omega. - apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. -- apply singleoffloat_redundant_sound; auto. Qed. End SOUNDNESS. diff --git a/arm/Op.v b/arm/Op.v index b50a7b0..e7971f0 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -57,11 +57,14 @@ Inductive condition : Type := | Ccompushift: comparison -> shift -> condition (**r unsigned integer comparison *) | Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *) | Ccompuimm: comparison -> int -> condition (**r unsigned integer comparison with a constant *) - | Ccompf: comparison -> condition (**r floating-point comparison *) + | Ccompf: comparison -> condition (**r 64-bit floating-point comparison *) | Cnotcompf: comparison -> condition (**r negation of a floating-point comparison *) | Ccompfzero: comparison -> condition (**r floating-point comparison with 0.0 *) - | Cnotcompfzero: comparison -> condition. (**r negation of a floating-point comparison with 0.0 *) - + | Cnotcompfzero: comparison -> condition (**r negation of a floating-point comparison with 0.0 *) + | Ccompfs: comparison -> condition (**r 32-bit floating-point comparison *) + | Cnotcompfs: comparison -> condition (**r negation of a floating-point comparison *) + | Ccompfszero: comparison -> condition (**r floating-point comparison with 0.0 *) + | Cnotcompfszero: comparison -> condition. (**r negation of a floating-point comparison with 0.0 *) (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -69,7 +72,8 @@ Inductive condition : Type := Inductive operation : Type := | Omove: operation (**r [rd = r1] *) | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) - | Ofloatconst: float -> operation (**r [rd] is set to the given float constant *) + | Ofloatconst: float -> operation (**r [rd] is set to the given 64-bit float constant *) + | Osingleconst: float32 -> operation (**r [rd] is set to the given 32-bit float constant *) | Oaddrsymbol: ident -> int -> operation (**r [rd] is set to the the address of the symbol plus the offset *) | Oaddrstack: int -> operation (**r [rd] is set to the stack pointer plus the given offset *) (*c Integer arithmetic: *) @@ -113,12 +117,23 @@ Inductive operation : Type := | Osubf: operation (**r [rd = r1 - r2] *) | Omulf: operation (**r [rd = r1 * r2] *) | Odivf: operation (**r [rd = r1 / r2] *) + | Onegfs: operation (**r [rd = - r1] *) + | Oabsfs: operation (**r [rd = abs(r1)] *) + | Oaddfs: operation (**r [rd = r1 + r2] *) + | Osubfs: operation (**r [rd = r1 - r2] *) + | Omulfs: operation (**r [rd = r1 * r2] *) + | Odivfs: operation (**r [rd = r1 / r2] *) | Osingleoffloat: operation (**r [rd] is [r1] truncated to single-precision float *) + | Ofloatofsingle: operation (**r [rd] is [r1] expanded to double-precision float *) (*c Conversions between int and float: *) | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *) | Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] *) | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] *) | Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] *) + | Ointofsingle: operation (**r [rd = signed_int_of_single(r1)] *) + | Ointuofsingle: operation (**r [rd = unsigned_int_of_single(r1)] *) + | Osingleofint: operation (**r [rd = single_of_signed_int(r1)] *) + | Osingleofintu: operation (**r [rd = single_of_unsigned_int(r1)] *) (*c Manipulating 64-bit integers: *) | Omakelong: operation (**r [rd = r1 << 32 | r2] *) | Olowlong: operation (**r [rd = low-word(r1)] *) @@ -160,6 +175,7 @@ Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. generalize Int.eq_dec; intro. generalize Float.eq_dec; intro. + generalize Float32.eq_dec; intro. assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. generalize eq_shift; intro. generalize eq_condition; intro. @@ -203,6 +219,10 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | Ccompfzero c, v1 :: nil => Val.cmpf_bool c v1 (Vfloat Float.zero) | Cnotcompfzero c, v1 :: nil => option_map negb (Val.cmpf_bool c v1 (Vfloat Float.zero)) + | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 + | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) + | Ccompfszero c, v1 :: nil => Val.cmpfs_bool c v1 (Vsingle Float32.zero) + | Cnotcompfszero c, v1 :: nil => option_map negb (Val.cmpfs_bool c v1 (Vsingle Float32.zero)) | _, _ => None end. @@ -213,6 +233,7 @@ Definition eval_operation | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) | Ofloatconst n, nil => Some (Vfloat n) + | Osingleconst n, nil => Some (Vsingle n) | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs)) | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1) @@ -254,11 +275,22 @@ Definition eval_operation | Osubf, v1::v2::nil => Some(Val.subf v1 v2) | Omulf, v1::v2::nil => Some(Val.mulf v1 v2) | Odivf, v1::v2::nil => Some(Val.divf v1 v2) + | Onegfs, v1::nil => Some(Val.negfs v1) + | Oabsfs, v1::nil => Some(Val.absfs v1) + | Oaddfs, v1::v2::nil => Some(Val.addfs v1 v2) + | Osubfs, v1::v2::nil => Some(Val.subfs v1 v2) + | Omulfs, v1::v2::nil => Some(Val.mulfs v1 v2) + | Odivfs, v1::v2::nil => Some(Val.divfs v1 v2) | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1) + | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1) | Ointoffloat, v1::nil => Val.intoffloat v1 | Ointuoffloat, v1::nil => Val.intuoffloat v1 | Ofloatofint, v1::nil => Val.floatofint v1 | Ofloatofintu, v1::nil => Val.floatofintu v1 + | Ointofsingle, v1::nil => Val.intofsingle v1 + | Ointuofsingle, v1::nil => Val.intuofsingle v1 + | Osingleofint, v1::nil => Val.singleofint v1 + | Osingleofintu, v1::nil => Val.singleofintu v1 | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2) | Olowlong, v1::nil => Some(Val.loword v1) | Ohighlong, v1::nil => Some(Val.hiword v1) @@ -281,8 +313,6 @@ Ltac FuncInv := match goal with | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => destruct x; simpl in H; try discriminate; FuncInv - | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ => - destruct v; simpl in H; try discriminate; FuncInv | H: (Some _ = Some _) |- _ => injection H; intros; clear H; FuncInv | _ => @@ -303,13 +333,18 @@ Definition type_of_condition (c: condition) : list typ := | Cnotcompf _ => Tfloat :: Tfloat :: nil | Ccompfzero _ => Tfloat :: nil | Cnotcompfzero _ => Tfloat :: nil + | Ccompfs _ => Tsingle :: Tsingle :: nil + | Cnotcompfs _ => Tsingle :: Tsingle :: nil + | Ccompfszero _ => Tsingle :: nil + | Cnotcompfszero _ => Tsingle :: nil end. Definition type_of_operation (op: operation) : list typ * typ := match op with | Omove => (nil, Tint) (* treated specially *) | Ointconst _ => (nil, Tint) - | Ofloatconst f => (nil, if Float.is_single_dec f then Tsingle else Tfloat) + | Ofloatconst f => (nil, Tfloat) + | Osingleconst f => (nil, Tsingle) | Oaddrsymbol _ _ => (nil, Tint) | Oaddrstack _ => (nil, Tint) | Ocast8signed => (Tint :: nil, Tint) @@ -351,11 +386,22 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osubf => (Tfloat :: Tfloat :: nil, Tfloat) | Omulf => (Tfloat :: Tfloat :: nil, Tfloat) | Odivf => (Tfloat :: Tfloat :: nil, Tfloat) + | Onegfs => (Tsingle :: nil, Tsingle) + | Oabsfs => (Tsingle :: nil, Tsingle) + | Oaddfs => (Tsingle :: Tsingle :: nil, Tsingle) + | Osubfs => (Tsingle :: Tsingle :: nil, Tsingle) + | Omulfs => (Tsingle :: Tsingle :: nil, Tsingle) + | Odivfs => (Tsingle :: Tsingle :: nil, Tsingle) | Osingleoffloat => (Tfloat :: nil, Tsingle) + | Ofloatofsingle => (Tsingle :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) | Ointuoffloat => (Tfloat :: nil, Tint) | Ofloatofint => (Tint :: nil, Tfloat) | Ofloatofintu => (Tint :: nil, Tfloat) + | Ointofsingle => (Tsingle :: nil, Tint) + | Ointuofsingle => (Tsingle :: nil, Tint) + | Osingleofint => (Tint :: nil, Tsingle) + | Osingleofintu => (Tint :: nil, Tsingle) | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) | Ohighlong => (Tlong :: nil, Tint) @@ -390,7 +436,6 @@ Proof with (try exact I). intros. destruct op; simpl; simpl in H0; FuncInv; try subst v... congruence. - destruct (Float.is_single_dec f); red; auto. unfold Genv.symbol_address. destruct (Genv.find_symbol genv i)... destruct sp... destruct v0... @@ -433,9 +478,20 @@ Proof with (try exact I). destruct v0; destruct v1... destruct v0; destruct v1... destruct v0; destruct v1... - destruct v0... simpl. apply Float.singleoffloat_is_single. - destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); simpl in H2; inv H2... - destruct v0; simpl in H0; inv H0. destruct (Float.intuoffloat f); simpl in H2; inv H2... + destruct v0... + destruct v0... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0... + destruct v0... + destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); simpl in H2; inv H2... + destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); simpl in H2; inv H2... + destruct v0; simpl in H0; inv H0... + destruct v0; simpl in H0; inv H0... + destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); simpl in H2; inv H2... + destruct v0; simpl in H0; inv H0. destruct (Float32.to_intu f); simpl in H2; inv H2... destruct v0; simpl in H0; inv H0... destruct v0; simpl in H0; inv H0... destruct v0; destruct v1... @@ -503,6 +559,10 @@ Definition negate_condition (cond: condition): condition := | Cnotcompf c => Ccompf c | Ccompfzero c => Cnotcompfzero c | Cnotcompfzero c => Ccompfzero c + | Ccompfs c => Cnotcompfs c + | Cnotcompfs c => Ccompfs c + | Ccompfszero c => Cnotcompfszero c + | Cnotcompfszero c => Ccompfszero c end. Lemma eval_negate_condition: @@ -520,6 +580,10 @@ Proof. repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto. repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.cmpf_bool c v (Vfloat Float.zero)); auto. destruct b; auto. + repeat (destruct vl; auto). + repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0); auto. destruct b; auto. + repeat (destruct vl; auto). + repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v (Vsingle Float32.zero)); auto. destruct b; auto. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) @@ -772,6 +836,8 @@ Ltac InvInject := inv H; InvInject | [ H: val_inject _ (Vfloat _) _ |- _ ] => inv H; InvInject + | [ H: val_inject _ (Vsingle _) _ |- _ ] => + inv H; InvInject | [ H: val_inject _ (Vptr _ _) _ |- _ ] => inv H; InvInject | [ H: val_list_inject _ nil _ |- _ ] => @@ -804,6 +870,10 @@ Proof. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; simpl in H0; inv H0; auto. inv H3; simpl in H0; inv H0; auto. + inv H3; inv H2; simpl in H0; inv H0; auto. + inv H3; inv H2; simpl in H0; inv H0; auto. + inv H3; simpl in H0; inv H0; auto. + inv H3; simpl in H0; inv H0; auto. Qed. Ltac TrivialExists := @@ -869,11 +939,27 @@ Proof. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. + + inv H4; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; simpl; auto. + + inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2. + exists (Vint i); auto. + inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2. + exists (Vint i); auto. + inv H4; simpl in *; inv H1. TrivialExists. + inv H4; simpl in *; inv H1. TrivialExists. - inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2. + inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2. exists (Vint i); auto. - inv H4; simpl in H1; inv H1. simpl. destruct (Float.intuoffloat f0); simpl in H2; inv H2. + inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_intu f0); simpl in H2; inv H2. exists (Vint i); auto. inv H4; simpl in *; inv H1. TrivialExists. inv H4; simpl in *; inv H1. TrivialExists. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 7e6827e..2ad9114 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -161,9 +161,10 @@ let distance_to_emit_constants () = (* Associate labels to floating-point constants and to symbols *) let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t) +let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t) let label_float f = - let bf = camlint64_of_coqint(Floats.Float.bits_of_double f) in + let bf = camlint64_of_coqint(Floats.Float.to_bits f) in try Hashtbl.find float_labels bf with Not_found -> @@ -173,6 +174,17 @@ let label_float f = max_pos_constants := min !max_pos_constants (!currpos + 1024); lbl' +let label_float32 f = + let bf = camlint_of_coqint(Floats.Float32.to_bits f) in + try + Hashtbl.find float32_labels bf + with Not_found -> + let lbl' = new_label() in + Hashtbl.add float32_labels bf lbl'; + size_constants := !size_constants + 4; + max_pos_constants := min !max_pos_constants (!currpos + 1024); + lbl' + let symbol_labels = (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t) @@ -188,6 +200,7 @@ let label_symbol id ofs = let reset_constants () = Hashtbl.clear float_labels; + Hashtbl.clear float32_labels; Hashtbl.clear symbol_labels; size_constants := 0; max_pos_constants := max_int @@ -200,6 +213,10 @@ let emit_constants oc = and bflo = Int64.logand bf 0xFFFF_FFFFL in fprintf oc ".L%d: .word 0x%Lx, 0x%Lx\n" lbl bflo bfhi) float_labels; + Hashtbl.iter + (fun bf lbl -> + fprintf oc ".L%d: .word 0x%lx\n" lbl bf) + float32_labels; Hashtbl.iter (fun (id, ofs) lbl -> fprintf oc ".L%d: .word %a\n" @@ -348,8 +365,7 @@ let print_builtin_vload_common oc chunk args res = fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr end; 2 | Mfloat32, [IR addr], [FR res] -> - fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr; - fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2 + fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr; 1 | Mfloat64, [IR addr], [FR res] -> fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1 | _ -> @@ -379,8 +395,7 @@ let print_builtin_vstore_common oc chunk args = fprintf oc " str %a, [%a, #0]\n" ireg src2 ireg addr; fprintf oc " str %a, [%a, #4]\n" ireg src1 ireg addr; 2 | Mfloat32, [IR addr; FR src] -> - fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src; - fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2 + fprintf oc " fsts %a, [%a, #0]\n" freg_single src ireg addr; 1 | Mfloat64, [IR addr; FR src] -> fprintf oc " fstd %a, [%a, #0]\n" freg src ireg addr; 1 | _ -> @@ -409,11 +424,11 @@ let align n a = (n + a - 1) land (-a) let rec next_arg_location ir ofs = function | [] -> Int32.of_int (ir * 4 + ofs) - | (Tint | Tsingle) :: l -> + | (Tint | Tsingle | Tany32) :: l -> if ir < 4 then next_arg_location (ir + 1) ofs l else next_arg_location ir (ofs + 4) l - | (Tfloat | Tlong) :: l -> + | (Tfloat | Tlong | Tany64) :: l -> if ir < 3 then next_arg_location (align ir 2 + 2) ofs l else next_arg_location ir (align ofs 8 + 8) l @@ -525,11 +540,9 @@ module FixupEABI = struct let fixup_single oc dir f i = match dir with - | Incoming -> (* f <- i; f <- double_of_single f *) - fprintf oc " fmsr %a, %a\n" freg_single f ireg i; - fprintf oc " fcvtds %a, %a\n" freg f freg_single f - | Outgoing -> (* f <- single_of_double f; i <- f *) - fprintf oc " fcvtsd %a, %a\n" freg_single f freg f; + | Incoming -> (* f <- i *) + fprintf oc " fmsr %a, %a\n" freg_single f ireg i + | Outgoing -> (* i <- f *) fprintf oc " fmrs %a, %a\n" ireg i freg_single f let fixup_conventions oc dir tyl = @@ -537,11 +550,11 @@ module FixupEABI = struct if i >= 4 then 0 else match tyl with | [] -> 0 - | Tint :: tyl' -> + | (Tint | Tany32) :: tyl' -> fixup (i+1) tyl' | Tlong :: tyl' -> fixup (((i + 1) land (-2)) + 2) tyl' - | Tfloat :: tyl' -> + | (Tfloat | Tany64) :: tyl' -> let i = (i + 1) land (-2) in if i >= 4 then 0 else begin fixup_double oc dir (freg_param i) (ireg_param i) (ireg_param (i+1)); @@ -549,7 +562,7 @@ module FixupEABI = struct end | Tsingle :: tyl' -> fixup_single oc dir (freg_param i) (ireg_param i); - 2 + fixup (i+1) tyl' + 1 + fixup (i+1) tyl' in fixup 0 tyl let fixup_arguments oc dir sg = @@ -577,8 +590,8 @@ module FixupHF = struct let rec fixup_actions used fr tyl = match tyl with | [] -> [] - | (Tint | Tlong) :: tyl' -> fixup_actions used fr tyl' - | Tfloat :: tyl' -> + | (Tint | Tlong | Tany32) :: tyl' -> fixup_actions used fr tyl' + | (Tfloat | Tany64) :: tyl' -> if fr >= 8 then [] else begin let dr = find_double used 0 in assert (dr < 8); @@ -599,7 +612,7 @@ module FixupHF = struct 1 + fixup_outgoing oc act end | (fr, Single, sr) :: act -> - fprintf oc " fcvtsd s%d, d%d\n" sr fr; + fprintf oc " fcpys s%d, s%d\n" sr (2*fr); 1 + fixup_outgoing oc act let rec fixup_incoming oc = function @@ -612,8 +625,10 @@ module FixupHF = struct end | (fr, Single, sr) :: act -> let n = fixup_incoming oc act in - fprintf oc " fcvtds d%d, s%d\n" fr sr; + if fr = sr then n else begin + fprintf oc " fcpys s%d, s%d\n" (2*fr) sr; 1 + n + end let fixup_arguments oc dir sg = if sg.sig_cc.cc_vararg then @@ -628,14 +643,8 @@ module FixupHF = struct let fixup_result oc dir sg = if sg.sig_cc.cc_vararg then FixupEABI.fixup_result oc dir sg - else begin - match proj_sig_res sg, dir with - | Tsingle, Outgoing -> - fprintf oc " fcvtsd s0, d0\n"; 1 - | Tsingle, Incoming -> - fprintf oc " fcvtds d0, s0\n"; 1 - | _ -> 0 - end + else + 0 end let (fixup_arguments, fixup_result) = @@ -703,7 +712,7 @@ let print_instruction oc = function fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1 | Peor(r1, r2, so) -> fprintf oc " eor %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 - | Pldr(r1, r2, sa) -> + | Pldr(r1, r2, sa) | Pldr_a(r1, r2, sa) -> fprintf oc " ldr %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 | Pldrb(r1, r2, sa) -> fprintf oc " ldrb %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 @@ -727,7 +736,7 @@ let print_instruction oc = function fprintf oc " orr %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 | Prsb(r1, r2, so) -> fprintf oc " rsb %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 - | Pstr(r1, r2, sa) -> + | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) -> fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; begin match r1, r2, sa with | IR14, IR13, SAimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n) @@ -786,19 +795,53 @@ let print_instruction oc = function | Pftouizd(r1, r2) -> fprintf oc " ftouizd %a, %a\n" freg_single FR6 freg r2; fprintf oc " fmrs %a, %a\n" ireg r1 freg_single FR6; 2 + | Pfabss(r1, r2) -> + fprintf oc " fabss %a, %a\n" freg_single r1 freg_single r2; 1 + | Pfnegs(r1, r2) -> + fprintf oc " fnegs %a, %a\n" freg_single r1 freg_single r2; 1 + | Pfadds(r1, r2, r3) -> + fprintf oc " fadds %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + | Pfdivs(r1, r2, r3) -> + fprintf oc " fdivs %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + | Pfmuls(r1, r2, r3) -> + fprintf oc " fmuls %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + | Pfsubs(r1, r2, r3) -> + fprintf oc " fsubs %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + | Pflis(r1, f) -> + (* We could make good use of the fconsts instruction, but it's available + in VFD v3 and up, not in v1 nor v2 *) + let lbl = label_float32 f in + fprintf oc " flds %a, .L%d @ %.12g\n" freg_single r1 lbl (camlfloat_of_coqfloat32 f); 1 + | Pfcmps(r1, r2) -> + fprintf oc " fcmps %a, %a\n" freg_single r1 freg_single r2; + fprintf oc " fmstat\n"; 2 + | Pfcmpzs(r1) -> + fprintf oc " fcmpzs %a\n" freg_single r1; + fprintf oc " fmstat\n"; 2 + | Pfsitos(r1, r2) -> + fprintf oc " fmsr %a, %a\n" freg_single r1 ireg r2; + fprintf oc " fsitos %a, %a\n" freg_single r1 freg_single r1; 2 + | Pfuitos(r1, r2) -> + fprintf oc " fmsr %a, %a\n" freg_single r1 ireg r2; + fprintf oc " fuitos %a, %a\n" freg_single r1 freg_single r1; 2 + | Pftosizs(r1, r2) -> + fprintf oc " ftosizs %a, %a\n" freg_single FR6 freg_single r2; + fprintf oc " fmrs %a, %a\n" ireg r1 freg_single FR6; 2 + | Pftouizs(r1, r2) -> + fprintf oc " ftouizs %a, %a\n" freg_single FR6 freg_single r2; + fprintf oc " fmrs %a, %a\n" ireg r1 freg_single FR6; 2 | Pfcvtsd(r1, r2) -> - fprintf oc " fcvtsd %a, %a\n" freg_single r1 freg r2; - fprintf oc " fcvtds %a, %a\n" freg r1 freg_single r1; 2 - | Pfldd(r1, r2, n) -> + fprintf oc " fcvtsd %a, %a\n" freg_single r1 freg r2; 1 + | Pfcvtds(r1, r2) -> + fprintf oc " fcvtds %a, %a\n" freg r1 freg_single r2; 1 + | Pfldd(r1, r2, n) | Pfldd_a(r1, r2, n) -> fprintf oc " fldd %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 | Pflds(r1, r2, n) -> - fprintf oc " flds %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; - fprintf oc " fcvtds %a, %a\n" freg r1 freg_single r1; 2 - | Pfstd(r1, r2, n) -> + fprintf oc " flds %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1 + | Pfstd(r1, r2, n) | Pfstd_a(r1, r2, n) -> fprintf oc " fstd %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 | Pfsts(r1, r2, n) -> - fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg r1; - fprintf oc " fsts %a, [%a, #%a]\n" freg_single FR6 ireg r2 coqint n; 2 + fprintf oc " fsts %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1 (* Pseudo-instructions *) | Pallocframe(sz, ofs) -> fprintf oc " mov r12, sp\n"; @@ -927,10 +970,10 @@ let print_init oc = function | Init_int64 n -> fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) | Init_float32 n -> - fprintf oc " .word 0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float.bits_of_single n)) + fprintf oc " .word 0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float32.to_bits n)) comment (camlfloat_of_coqfloat n) | Init_float64 n -> - fprintf oc " .quad %Ld %s %.18g\n" (camlint64_of_coqint (Floats.Float.bits_of_double n)) + fprintf oc " .quad %Ld %s %.18g\n" (camlint64_of_coqint (Floats.Float.to_bits n)) comment (camlfloat_of_coqfloat n) | Init_space n -> if Z.gt n Z.zero then diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index e4005c9..ad8a945 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -321,6 +321,12 @@ Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). +Definition negfs (e: expr) := Eop Onegfs (e ::: Enil). +Definition absfs (e: expr) := Eop Oabsfs (e ::: Enil). +Definition addfs (e1 e2: expr) := Eop Oaddfs (e1 ::: e2 ::: Enil). +Definition subfs (e1 e2: expr) := Eop Osubfs (e1 ::: e2 ::: Enil). +Definition mulfs (e1 e2: expr) := Eop Omulfs (e1 ::: e2 ::: Enil). + (** ** Comparisons *) Nondetfunction compimm (default: comparison -> int -> condition) @@ -370,6 +376,9 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := Definition compf (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). +Definition compfs (c: comparison) (e1: expr) (e2: expr) := + Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). + (** ** Integer conversions *) Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. @@ -391,21 +400,38 @@ Nondetfunction cast16signed (e: expr) := (** ** Floating-point conversions *) Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). +Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). + Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). Nondetfunction floatofint (e: expr) := match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofint n)) Enil + | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil | _ => Eop Ofloatofint (e ::: Enil) end. Nondetfunction floatofintu (e: expr) := match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofintu n)) Enil + | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil | _ => Eop Ofloatofintu (e ::: Enil) end. +Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil). +Definition intuofsingle (e: expr) := Eop Ointuofsingle (e ::: Enil). + +Nondetfunction singleofint (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_int n)) Enil + | _ => Eop Osingleofint (e ::: Enil) + end. + +Nondetfunction singleofintu (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_intu n)) Enil + | _ => Eop Osingleofintu (e ::: Enil) + end. + (** ** Recognition of addressing modes for load and store operations *) (** We do not recognize the [Aindexed2] and [Aindexed2shift] modes @@ -424,6 +450,8 @@ Definition can_use_Aindexed2 (chunk: memory_chunk): bool := | Mint64 => false | Mfloat32 => false | Mfloat64 => false + | Many32 => true + | Many64 => false end. Definition can_use_Aindexed2shift (chunk: memory_chunk): bool := @@ -436,6 +464,8 @@ Definition can_use_Aindexed2shift (chunk: memory_chunk): bool := | Mint64 => false | Mfloat32 => false | Mfloat64 => false + | Many32 => true + | Many64 => false end. Nondetfunction addressing (chunk: memory_chunk) (e: expr) := diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 1dd2c20..c68d227 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -598,6 +598,31 @@ Proof. red; intros; TrivialExists. Qed. +Theorem eval_negfs: unary_constructor_sound negfs Val.negfs. +Proof. + red; intros. TrivialExists. +Qed. + +Theorem eval_absfs: unary_constructor_sound absfs Val.absfs. +Proof. + red; intros. TrivialExists. +Qed. + +Theorem eval_addfs: binary_constructor_sound addfs Val.addfs. +Proof. + red; intros; TrivialExists. +Qed. + +Theorem eval_subfs: binary_constructor_sound subfs Val.subfs. +Proof. + red; intros; TrivialExists. +Qed. + +Theorem eval_mulfs: binary_constructor_sound mulfs Val.mulfs. +Proof. + red; intros; TrivialExists. +Qed. + Section COMP_IMM. Variable default: comparison -> int -> condition. @@ -693,6 +718,12 @@ Proof. intros; red; intros. unfold compf. TrivialExists. Qed. +Theorem eval_compfs: + forall c, binary_constructor_sound (compfs c) (Val.cmpfs c). +Proof. + intros; red; intros. unfold compfs. TrivialExists. +Qed. + Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). Proof. red; intros until x. unfold cast8signed; case (cast8signed_match a); intros. @@ -724,6 +755,11 @@ Proof. red; intros. unfold singleoffloat. TrivialExists. Qed. +Theorem eval_floatofsingle: unary_constructor_sound floatofsingle Val.floatofsingle. +Proof. + red; intros. unfold floatofsingle. TrivialExists. +Qed. + Theorem eval_intoffloat: forall le a x y, eval_expr ge sp e m le a x -> @@ -764,6 +800,46 @@ Proof. TrivialExists. Qed. +Theorem eval_intofsingle: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.intofsingle x = Some y -> + exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v. +Proof. + intros; unfold intofsingle. TrivialExists. +Qed. + +Theorem eval_singleofint: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.singleofint x = Some y -> + exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v. +Proof. + intros until y; unfold singleofint. case (singleofint_match a); intros. + InvEval. simpl in H0. TrivialExists. + TrivialExists. +Qed. + +Theorem eval_intuofsingle: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.intuofsingle x = Some y -> + exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v. +Proof. + intros; unfold intuofsingle. TrivialExists. +Qed. + +Theorem eval_singleofintu: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.singleofintu x = Some y -> + exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v. +Proof. + intros until y; unfold singleofintu. case (singleofintu_match a); intros. + InvEval. simpl in H0. TrivialExists. + TrivialExists. +Qed. + Theorem eval_addressing: forall le chunk a v b ofs, eval_expr ge sp e m le a v -> diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v index b312361..a14d6b9 100644 --- a/arm/ValueAOp.v +++ b/arm/ValueAOp.v @@ -44,6 +44,10 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfzero c, v1 :: nil => cmpf_bool c v1 (F Float.zero) | Cnotcompfzero c, v1 :: nil => cnot (cmpf_bool c v1 (F Float.zero)) + | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 + | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) + | Ccompfszero c, v1 :: nil => cmpfs_bool c v1 (FS Float32.zero) + | Cnotcompfszero c, v1 :: nil => cnot (cmpfs_bool c v1 (FS Float32.zero)) | _, _ => Bnone end. @@ -61,6 +65,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omove, v1::nil => v1 | Ointconst n, nil => I n | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop + | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) | Oaddrstack ofs, nil => Ptr (Stk ofs) | Ocast8signed, v1 :: nil => sign_ext 8 v1 @@ -102,11 +107,22 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osubf, v1::v2::nil => subf v1 v2 | Omulf, v1::v2::nil => mulf v1 v2 | Odivf, v1::v2::nil => divf v1 v2 + | Onegfs, v1::nil => negfs v1 + | Oabsfs, v1::nil => absfs v1 + | Oaddfs, v1::v2::nil => addfs v1 v2 + | Osubfs, v1::v2::nil => subfs v1 v2 + | Omulfs, v1::v2::nil => mulfs v1 v2 + | Odivfs, v1::v2::nil => divfs v1 v2 | Osingleoffloat, v1::nil => singleoffloat v1 + | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 | Ointuoffloat, v1::nil => intuoffloat v1 | Ofloatofint, v1::nil => floatofint v1 | Ofloatofintu, v1::nil => floatofintu v1 + | Ointofsingle, v1::nil => intofsingle v1 + | Ointuofsingle, v1::nil => intuofsingle v1 + | Osingleofint, v1::nil => singleofint v1 + | Osingleofintu, v1::nil => singleofintu v1 | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 | Ohighlong, v1::nil => hiword v1 @@ -185,6 +201,7 @@ Proof. unfold eval_operation, eval_static_operation; intros; destruct op; InvHyps; eauto with va. destruct (propagate_float_constants tt); constructor. + destruct (propagate_float_constants tt); constructor. rewrite Int.add_zero_l; eauto with va. fold (Val.sub (Vint i) a1). auto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. diff --git a/arm/eabi/Conventions1.v b/arm/eabi/Conventions1.v index c02af1a..c26d29e 100644 --- a/arm/eabi/Conventions1.v +++ b/arm/eabi/Conventions1.v @@ -15,6 +15,7 @@ Require Import Coqlib. Require Import AST. +Require Import Events. Require Import Locations. (** * Classification of machine registers *) @@ -178,13 +179,13 @@ Proof. Qed. Lemma int_callee_save_type: - forall r, In r int_callee_save_regs -> mreg_type r = Tint. + forall r, In r int_callee_save_regs -> mreg_type r = Tany32. Proof. intro. simpl; ElimOrEq; reflexivity. Qed. Lemma float_callee_save_type: - forall r, In r float_callee_save_regs -> mreg_type r = Tfloat. + forall r, In r float_callee_save_regs -> mreg_type r = Tany64. Proof. intro. simpl; ElimOrEq; reflexivity. Qed. @@ -235,12 +236,21 @@ Qed. Definition loc_result (s: signature) : list mreg := match s.(sig_res) with | None => R0 :: nil - | Some Tint => R0 :: nil - | Some (Tfloat | Tsingle) => F0 :: nil + | Some (Tint | Tany32) => R0 :: nil + | Some (Tfloat | Tsingle | Tany64) => F0 :: nil | Some Tlong => R1 :: R0 :: nil end. -(** The result location is a caller-save register or a temporary *) +(** The result registers have types compatible with that given in the signature. *) + +Lemma loc_result_type: + forall sig, + subtype_list (proj_sig_res' sig) (map mreg_type (loc_result sig)) = true. +Proof. + intros. unfold proj_sig_res', loc_result. destruct (sig_res sig) as [[]|]; auto. +Qed. + +(** The result locations are caller-save registers *) Lemma loc_result_caller_save: forall (s: signature) (r: mreg), @@ -292,12 +302,12 @@ Definition sreg_param (n: Z) : mreg := Fixpoint loc_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : list loc := match tyl with | nil => nil - | Tint :: tys => - (if zle 0 ofs then S Outgoing ofs Tint else R (ireg_param ofs)) + | (Tint | Tany32) as ty :: tys => + (if zle 0 ofs then S Outgoing ofs ty else R (ireg_param ofs)) :: loc_arguments_rec tys (ofs + 1) - | Tfloat :: tys => + | (Tfloat | Tany64) as ty :: tys => let ofs := align ofs 2 in - (if zle 0 ofs then S Outgoing ofs Tfloat else R (freg_param ofs)) + (if zle 0 ofs then S Outgoing ofs ty else R (freg_param ofs)) :: loc_arguments_rec tys (ofs + 2) | Tsingle :: tys => (if zle 0 ofs then S Outgoing ofs Tsingle else R (sreg_param ofs)) @@ -321,8 +331,8 @@ Definition loc_arguments (s: signature) : list loc := Fixpoint size_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : Z := match tyl with | nil => ofs - | (Tint | Tsingle) :: tys => size_arguments_rec tys (ofs + 1) - | (Tfloat | Tlong) :: tys => size_arguments_rec tys (align ofs 2 + 2) + | (Tint | Tsingle | Tany32) :: tys => size_arguments_rec tys (ofs + 1) + | (Tfloat | Tlong | Tany64) :: tys => size_arguments_rec tys (align ofs 2 + 2) end. Definition size_arguments (s: signature) : Z := @@ -404,6 +414,19 @@ Proof. split. omega. split. omega. congruence. apply sreg_param_caller_save. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. +- (* Tany32 *) + destruct H. + subst l. destruct (zle 0 ofs). + split. omega. split. omega. congruence. + apply ireg_param_caller_save. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. +- (* Tany64 *) + assert (ofs <= align ofs 2) by (apply align_le; omega). + destruct H. + subst l. destruct (zle 0 (align ofs 2)). + split. omega. split. auto. congruence. + apply freg_param_caller_save. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. Qed. Lemma loc_arguments_acceptable: @@ -433,6 +456,9 @@ Proof. assert (ofs <= align ofs 2) by (apply align_le; omega). apply Zle_trans with (align ofs 2 + 2); auto; omega. apply Zle_trans with (ofs + 1); auto; omega. + apply Zle_trans with (ofs + 1); auto; omega. + assert (ofs <= align ofs 2) by (apply align_le; omega). + apply Zle_trans with (align ofs 2 + 2); auto; omega. Qed. Lemma size_arguments_above: @@ -474,6 +500,10 @@ Proof. eapply Zle_trans. 2: apply H0. simpl typesize; omega. omega. - (* Tsingle *) destruct H1; auto. destruct (zle 0 ofs0); inv H1. apply H0. omega. + - (* Tany32 *) + destruct H1; auto. destruct (zle 0 ofs0); inv H1. apply H0. omega. + - (* Tany64 *) + destruct H1; auto. destruct (zle 0 (align ofs0 2)); inv H1. apply H0. omega. } unfold size_arguments. apply H1. auto. Qed. diff --git a/arm/hardfloat/Conventions1.v b/arm/hardfloat/Conventions1.v index e3875e7..40a761c 100644 --- a/arm/hardfloat/Conventions1.v +++ b/arm/hardfloat/Conventions1.v @@ -15,6 +15,7 @@ Require Import Coqlib. Require Import AST. +Require Import Events. Require Import Locations. (** * Classification of machine registers *) @@ -178,13 +179,13 @@ Proof. Qed. Lemma int_callee_save_type: - forall r, In r int_callee_save_regs -> mreg_type r = Tint. + forall r, In r int_callee_save_regs -> mreg_type r = Tany32. Proof. intro. simpl; ElimOrEq; reflexivity. Qed. Lemma float_callee_save_type: - forall r, In r float_callee_save_regs -> mreg_type r = Tfloat. + forall r, In r float_callee_save_regs -> mreg_type r = Tany64. Proof. intro. simpl; ElimOrEq; reflexivity. Qed. @@ -235,12 +236,21 @@ Qed. Definition loc_result (s: signature) : list mreg := match s.(sig_res) with | None => R0 :: nil - | Some Tint => R0 :: nil - | Some (Tfloat | Tsingle) => F0 :: nil + | Some (Tint | Tany32) => R0 :: nil + | Some (Tfloat | Tsingle | Tany64) => F0 :: nil | Some Tlong => R1 :: R0 :: nil end. -(** The result location is a caller-save register or a temporary *) +(** The result registers have types compatible with that given in the signature. *) + +Lemma loc_result_type: + forall sig, + subtype_list (proj_sig_res' sig) (map mreg_type (loc_result sig)) = true. +Proof. + intros. unfold proj_sig_res', loc_result. destruct (sig_res sig) as [[]|]; auto. +Qed. + +(** The result locations are caller-save registers *) Lemma loc_result_caller_save: forall (s: signature) (r: mreg), @@ -286,15 +296,15 @@ Fixpoint loc_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list loc := match tyl with | nil => nil - | Tint :: tys => + | (Tint | Tany32) as ty :: tys => if zlt ir 4 then R (ireg_param ir) :: loc_arguments_rec tys (ir + 1) fr ofs - else S Outgoing ofs Tint :: loc_arguments_rec tys ir fr (ofs + 1) - | Tfloat :: tys => + else S Outgoing ofs ty :: loc_arguments_rec tys ir fr (ofs + 1) + | (Tfloat | Tany64) as ty :: tys => if zlt fr 8 then R (freg_param fr) :: loc_arguments_rec tys ir (fr + 1) ofs else let ofs := align ofs 2 in - S Outgoing ofs Tfloat :: loc_arguments_rec tys ir fr (ofs + 2) + S Outgoing ofs ty :: loc_arguments_rec tys ir fr (ofs + 2) | Tsingle :: tys => if zlt fr 8 then R (freg_param fr) :: loc_arguments_rec tys ir (fr + 1) ofs @@ -325,12 +335,12 @@ Fixpoint loc_arguments_vararg (tyl: list typ) (ofs: Z) {struct tyl} : list loc := match tyl with | nil => nil - | Tint :: tys => - (if zlt ofs 0 then R (ireg_param (ofs + 4)) else S Outgoing ofs Tint) + | (Tint|Tany32) as ty :: tys => + (if zlt ofs 0 then R (ireg_param (ofs + 4)) else S Outgoing ofs ty) :: loc_arguments_vararg tys (ofs + 1) - | Tfloat :: tys => + | (Tfloat|Tany64) as ty :: tys => let ofs := align ofs 2 in - (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tfloat) + (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs ty) :: loc_arguments_vararg tys (ofs + 2) | Tsingle :: tys => (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tsingle) @@ -356,11 +366,11 @@ Definition loc_arguments (s: signature) : list loc := Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := match tyl with | nil => ofs - | Tint :: tys => + | (Tint|Tany32) :: tys => if zlt ir 4 then size_arguments_rec tys (ir + 1) fr ofs else size_arguments_rec tys ir fr (ofs + 1) - | Tfloat :: tys => + | (Tfloat|Tany64) :: tys => if zlt fr 8 then size_arguments_rec tys ir (fr + 1) ofs else size_arguments_rec tys ir fr (align ofs 2 + 2) @@ -378,8 +388,8 @@ Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := Fixpoint size_arguments_vararg (tyl: list typ) (ofs: Z) {struct tyl} : Z := match tyl with | nil => Zmax 0 ofs - | (Tint | Tsingle) :: tys => size_arguments_vararg tys (ofs + 1) - | (Tfloat | Tlong) :: tys => size_arguments_vararg tys (align ofs 2 + 2) + | (Tint | Tsingle | Tany32) :: tys => size_arguments_vararg tys (ofs + 1) + | (Tfloat | Tlong | Tany64) :: tys => size_arguments_vararg tys (align ofs 2 + 2) end. Definition size_arguments (s: signature) : Z := @@ -469,6 +479,19 @@ Proof. eapply IHtyl; eauto. subst. split; [omega | congruence]. eapply INCR. eapply IHtyl; eauto. omega. +- (* any32 *) + destruct (zlt ir 4); destruct H. + subst. left; apply ireg_param_in_params. + eapply IHtyl; eauto. + subst. split; [omega | congruence]. + eapply INCR. eapply IHtyl; eauto. omega. +- (* any64 *) + destruct (zlt fr 8); destruct H. + subst. right; apply freg_param_in_params. + eapply IHtyl; eauto. + subst. split. apply Zle_ge. apply align_le. omega. congruence. + eapply INCR. eapply IHtyl; eauto. + apply Zle_trans with (align ofs 2). apply align_le; omega. omega. Qed. Remark loc_arguments_vararg_charact: @@ -530,6 +553,20 @@ Proof. right; apply freg_param_in_params. split. xomega. congruence. eapply INCR. eapply IHtyl; eauto. omega. +- (* any32 *) + destruct H. + destruct (zlt ofs 0); subst l. + left; apply ireg_param_in_params. + split. xomega. congruence. + eapply INCR. eapply IHtyl; eauto. omega. +- (* any64 *) + set (ofs' := align ofs 2) in *. + assert (ofs <= ofs') by (apply align_le; omega). + destruct H. + destruct (zlt ofs' 0); subst l. + right; apply freg_param_in_params. + split. xomega. congruence. + eapply INCR. eapply IHtyl; eauto. omega. Qed. Lemma loc_arguments_acceptable: @@ -569,6 +606,10 @@ Proof. apply Zle_trans with (align ofs0 2 + 2); auto; omega. destruct (zlt fr 8); eauto. apply Zle_trans with (ofs0 + 1); eauto. omega. + destruct (zlt ir 4); eauto. apply Zle_trans with (ofs0 + 1); auto; omega. + destruct (zlt fr 8); eauto. + apply Zle_trans with (align ofs0 2). apply align_le; omega. + apply Zle_trans with (align ofs0 2 + 2); auto; omega. Qed. Remark size_arguments_vararg_above: @@ -582,6 +623,8 @@ Proof. assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. xomega. + xomega. + assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. Qed. Lemma size_arguments_above: @@ -626,6 +669,18 @@ Proof. eauto. inv H. apply size_arguments_rec_above. eauto. +- (* any32 *) + destruct (zlt ir 4); destruct H. + discriminate. + eauto. + inv H. apply size_arguments_rec_above. + eauto. +- (* any64 *) + destruct (zlt fr 8); destruct H. + discriminate. + eauto. + inv H. apply size_arguments_rec_above. + eauto. Qed. Lemma loc_arguments_vararg_bounded: @@ -656,6 +711,14 @@ Proof. destruct H. destruct (zlt ofs0 0); inv H. apply size_arguments_vararg_above. eauto. +- (* any32 *) + destruct H. + destruct (zlt ofs0 0); inv H. apply size_arguments_vararg_above. + eauto. +- (* any64 *) + destruct H. + destruct (zlt (align ofs0 2) 0); inv H. apply size_arguments_vararg_above. + eauto. Qed. Lemma loc_arguments_bounded: -- cgit v1.2.3