From 5a632954c85e8b2b5afea124e4fc83f39c5d3598 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 1 Jun 2021 14:37:07 +0200 Subject: [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend/C2C.ml --- powerpc/Archi.v | 9 +- powerpc/Asm.v | 2 + powerpc/Asmexpand.ml | 54 +++++++-- powerpc/Asmgen.v | 114 ++++++++++++------- powerpc/Asmgenproof.v | 23 +++- powerpc/Asmgenproof1.v | 271 +++++++++++++++++++++++++++----------------- powerpc/Builtins1.v | 9 +- powerpc/CBuiltins.ml | 9 +- powerpc/extractionMachdep.v | 10 +- 9 files changed, 322 insertions(+), 179 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 5b9d67cc..5b0af3b6 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -7,10 +7,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 93bc31b8..6b1f2232 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -538,6 +538,8 @@ Axiom small_data_area_addressing: Parameter symbol_is_rel_data: ident -> ptrofs -> bool. +Parameter symbol_is_aligned: ident -> Z -> bool. + (** Armed with the [low_half] and [high_half] functions, we can define the evaluation of a symbolic constant. Note that for [const_high], integer constants diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index df712b9d..e663226f 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -177,34 +177,56 @@ let expand_builtin_memcpy sz al args = let expand_volatile_access (mk1: ireg -> constant -> unit) (mk2: ireg -> ireg -> unit) + ?(ofs_unaligned = true) addr temp = match addr with | BA(IR r) -> mk1 r (Cint _0) | BA_addrstack ofs -> - if offset_in_range ofs then - mk1 GPR1 (Cint ofs) + if ofs_unaligned || Int.eq (Int.mods ofs _4) _0 then + if offset_in_range ofs then + mk1 GPR1 (Cint ofs) + else begin + emit (Paddis(temp, GPR1, Cint (Asmgen.high_s ofs))); + mk1 temp (Cint (Asmgen.low_s ofs)) + end else begin - emit (Paddis(temp, GPR1, Cint (Asmgen.high_s ofs))); - mk1 temp (Cint (Asmgen.low_s ofs)) + emit (Paddis (temp, GPR1, Cint (Asmgen.high_s ofs))); + emit (Paddi (temp, temp, Cint (Asmgen.low_s ofs))); + mk1 temp (Cint _0) end | BA_addrglobal(id, ofs) -> if symbol_is_small_data id ofs then - mk1 GPR0 (Csymbol_sda(id, ofs)) + if ofs_unaligned || Asmgen.symbol_ofs_word_aligned id ofs then + mk1 GPR0 (Csymbol_sda(id, ofs)) + else begin + emit (Paddi (temp, GPR0, (Csymbol_sda (id,ofs)))); + mk1 temp (Cint _0) + end else if symbol_is_rel_data id ofs then begin emit (Paddis(temp, GPR0, Csymbol_rel_high(id, ofs))); emit (Paddi(temp, temp, Csymbol_rel_low(id, ofs))); mk1 temp (Cint _0) - end else begin + end else if ofs_unaligned || Asmgen.symbol_ofs_word_aligned id ofs then begin emit (Paddis(temp, GPR0, Csymbol_high(id, ofs))); mk1 temp (Csymbol_low(id, ofs)) + end else begin + emit (Paddis (temp, GPR0, (Csymbol_high (id, ofs)))); + emit (Paddi (temp, temp, (Csymbol_low (id, ofs)))); + mk1 temp (Cint _0) end | BA_addptr(BA(IR r), BA_int n) -> - if offset_in_range n then - mk1 r (Cint n) + if ofs_unaligned || Int.eq (Int.mods n _4) _0 then + if offset_in_range n then + mk1 r (Cint n) + else begin + emit (Paddis(temp, r, Cint (Asmgen.high_s n))); + mk1 temp (Cint (Asmgen.low_s n)) + end else begin - emit (Paddis(temp, r, Cint (Asmgen.high_s n))); - mk1 temp (Cint (Asmgen.low_s n)) + emit (Paddis (temp, r, Cint (Asmgen.high_s n))); + emit (Paddi (temp, temp, Cint (Asmgen.low_s n))); + mk1 temp (Cint _0) end | BA_addptr(BA_addrglobal(id, ofs), BA(IR r)) -> if symbol_is_small_data id ofs then begin @@ -215,9 +237,14 @@ let expand_volatile_access emit (Paddis(temp, GPR0, Csymbol_rel_high(id, ofs))); emit (Paddi(temp, temp, Csymbol_rel_low(id, ofs))); mk2 temp GPR0 - end else begin + end else if ofs_unaligned || Asmgen.symbol_ofs_word_aligned id ofs then begin emit (Paddis(temp, r, Csymbol_high(id, ofs))); mk1 temp (Csymbol_low(id, ofs)) + end else begin + emit (Pmr (GPR0, r)); + emit (Paddis(temp, GPR0, Csymbol_high(id, ofs))); + emit (Paddi(temp, temp, Csymbol_low(id, ofs))); + mk2 temp GPR0 end | BA_addptr(BA(IR r1), BA(IR r2)) -> mk2 r1 r2 @@ -283,6 +310,7 @@ let expand_builtin_vload_1 chunk addr res = expand_volatile_access (fun r c -> emit (Pld(res, c, r))) (fun r1 r2 -> emit (Pldx(res, r1, r2))) + ~ofs_unaligned:false addr GPR11 | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) -> expand_volatile_access @@ -346,6 +374,7 @@ let expand_builtin_vstore_1 chunk addr src = expand_volatile_access (fun r c -> emit (Pstd(src, c, r))) (fun r1 r2 -> emit (Pstdx(src, r1, r2))) + ~ofs_unaligned:false addr temp | Mint64, BA_splitlong(BA(IR hi), BA(IR lo)) -> expand_volatile_access @@ -764,6 +793,9 @@ let expand_builtin_inline name args res = (* no operation *) | "__builtin_nop", [], _ -> emit (Pori (GPR0, GPR0, Cint _0)) + (* Optimization hint *) + | "__builtin_unreachable", [], _ -> + () (* atomic operations *) | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ -> (* Register constraints imposed by Machregs.v *) diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index d0c44f08..ec7242bb 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -190,36 +190,38 @@ Definition rolm64 (r1 r2: ireg) (amount: int) (mask: int64) (k: code) := (** Accessing slots in the stack frame. *) +(* For 64 bit load and store the offset needs to be a multiple of word size *) Definition accessind {A: Type} (instr1: A -> constant -> ireg -> instruction) (instr2: A -> ireg -> ireg -> instruction) + (unaligned : bool) (base: ireg) (ofs: ptrofs) (r: A) (k: code) := let ofs := Ptrofs.to_int ofs in - if Int.eq (high_s ofs) Int.zero + if Int.eq (high_s ofs) Int.zero && (unaligned || (Int.eq (Int.mods ofs (Int.repr 4)) Int.zero)) then instr1 r (Cint ofs) base :: k else loadimm GPR0 ofs (instr2 r base GPR0 :: k). Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := match ty, preg_of dst with - | Tint, IR r => OK(accessind Plwz Plwzx base ofs r k) - | Tany32, IR r => OK(accessind Plwz_a Plwzx_a base ofs r k) - | Tsingle, FR r => OK(accessind Plfs Plfsx base ofs r k) - | Tlong, IR r => OK(accessind Pld Pldx base ofs r k) - | Tfloat, FR r => OK(accessind Plfd Plfdx base ofs r k) - | Tany64, IR r => OK(accessind Pld_a Pldx_a base ofs r k) - | Tany64, FR r => OK(accessind Plfd_a Plfdx_a base ofs r k) + | Tint, IR r => OK(accessind Plwz Plwzx true base ofs r k) + | Tany32, IR r => OK(accessind Plwz_a Plwzx_a true base ofs r k) + | Tsingle, FR r => OK(accessind Plfs Plfsx true base ofs r k) + | Tlong, IR r => OK(accessind Pld Pldx false base ofs r k) + | Tfloat, FR r => OK(accessind Plfd Plfdx true base ofs r k) + | Tany64, IR r => OK(accessind Pld_a Pldx_a false base ofs r k) + | Tany64, FR r => OK(accessind Plfd_a Plfdx_a true base ofs r k) | _, _ => Error (msg "Asmgen.loadind") end. Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) := match ty, preg_of src with - | Tint, IR r => OK(accessind Pstw Pstwx base ofs r k) - | Tany32, IR r => OK(accessind Pstw_a Pstwx_a base ofs r k) - | Tsingle, FR r => OK(accessind Pstfs Pstfsx base ofs r k) - | Tlong, IR r => OK(accessind Pstd Pstdx base ofs r k) - | Tfloat, FR r => OK(accessind Pstfd Pstfdx base ofs r k) - | Tany64, IR r => OK(accessind Pstd_a Pstdx_a base ofs r k) - | Tany64, FR r => OK(accessind Pstfd_a Pstfdx_a base ofs r k) + | Tint, IR r => OK(accessind Pstw Pstwx true base ofs r k) + | Tany32, IR r => OK(accessind Pstw_a Pstwx_a true base ofs r k) + | Tsingle, FR r => OK(accessind Pstfs Pstfsx true base ofs r k) + | Tlong, IR r => OK(accessind Pstd Pstdx false base ofs r k) + | Tfloat, FR r => OK(accessind Pstfd Pstfdx true base ofs r k) + | Tany64, IR r => OK(accessind Pstd_a Pstdx_a false base ofs r k) + | Tany64, FR r => OK(accessind Pstfd_a Pstfdx_a true base ofs r k) | _, _ => Error (msg "Asmgen.storeind") end. @@ -724,32 +726,48 @@ Definition transl_op Definition int_temp_for (r: mreg) := if mreg_eq r R12 then GPR11 else GPR12. +Definition symbol_ofs_word_aligned symb ofs := + let ofs := Ptrofs.to_int ofs in + symbol_is_aligned symb 4 && (Int.eq (Int.mods ofs (Int.repr 4)) Int.zero). + Definition transl_memory_access (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) + (unaligned : bool) (addr: addressing) (args: list mreg) (temp: ireg) (k: code) := match addr, args with | Aindexed ofs, a1 :: nil => do r1 <- ireg_of a1; - OK (if Int.eq (high_s ofs) Int.zero then - mk1 (Cint ofs) r1 :: k - else - Paddis temp r1 (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) temp :: k) + OK (if unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero then + if Int.eq (high_s ofs) Int.zero then + mk1 (Cint ofs) r1 :: k + else + Paddis temp r1 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) temp :: k + else + (loadimm GPR0 ofs (mk2 r1 GPR0 :: k))) | Aindexed2, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (mk2 r1 r2 :: k) | Aglobal symb ofs, nil => - OK (if symbol_is_small_data symb ofs then - mk1 (Csymbol_sda symb ofs) GPR0 :: k + OK (if symbol_is_small_data symb ofs then + if unaligned || symbol_ofs_word_aligned symb ofs then + mk1 (Csymbol_sda symb ofs) GPR0 :: k + else + Paddi temp GPR0 (Csymbol_sda symb ofs) :: + mk1 (Cint Int.zero) temp :: k else if symbol_is_rel_data symb ofs then Paddis temp GPR0 (Csymbol_rel_high symb ofs) :: Paddi temp temp (Csymbol_rel_low symb ofs) :: mk1 (Cint Int.zero) temp :: k + else if unaligned || symbol_ofs_word_aligned symb ofs then + Paddis temp GPR0 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) temp :: k else Paddis temp GPR0 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) temp :: k) + Paddi temp temp (Csymbol_low symb ofs) :: + mk1 (Cint Int.zero) temp :: k) | Abased symb ofs, a1 :: nil => do r1 <- ireg_of a1; OK (if symbol_is_small_data symb ofs then @@ -760,16 +778,24 @@ Definition transl_memory_access Paddis temp GPR0 (Csymbol_rel_high symb ofs) :: Paddi temp temp (Csymbol_rel_low symb ofs) :: mk2 temp GPR0 :: k - else + else if unaligned || symbol_ofs_word_aligned symb ofs then Paddis temp r1 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) temp :: k) + mk1 (Csymbol_low symb ofs) temp :: k + else + Pmr GPR0 r1 :: + Paddis temp GPR0 (Csymbol_high symb ofs) :: + Paddi temp temp (Csymbol_low symb ofs) :: + mk2 temp GPR0 :: k) | Ainstack ofs, nil => let ofs := Ptrofs.to_int ofs in - OK (if Int.eq (high_s ofs) Int.zero then - mk1 (Cint ofs) GPR1 :: k - else - Paddis temp GPR1 (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) temp :: k) + OK (if unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero then + if Int.eq (high_s ofs) Int.zero then + mk1 (Cint ofs) GPR1 :: k + else + Paddis temp GPR1 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) temp :: k + else + addimm temp GPR1 ofs (mk1 (Cint Int.zero) temp :: k)) | _, _ => Error(msg "Asmgen.transl_memory_access") end. @@ -784,28 +810,28 @@ Definition transl_load match chunk with | Mint8signed => do r <- ireg_of dst; - transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 (Pextsb r r :: k) + transl_memory_access (Plbz r) (Plbzx r) true addr args GPR12 (Pextsb r r :: k) | Mint8unsigned => do r <- ireg_of dst; - transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 k + transl_memory_access (Plbz r) (Plbzx r) true addr args GPR12 k | Mint16signed => do r <- ireg_of dst; - transl_memory_access (Plha r) (Plhax r) addr args GPR12 k + transl_memory_access (Plha r) (Plhax r) true addr args GPR12 k | Mint16unsigned => do r <- ireg_of dst; - transl_memory_access (Plhz r) (Plhzx r) addr args GPR12 k + transl_memory_access (Plhz r) (Plhzx r) true addr args GPR12 k | Mint32 => do r <- ireg_of dst; - transl_memory_access (Plwz r) (Plwzx r) addr args GPR12 k + transl_memory_access (Plwz r) (Plwzx r) true addr args GPR12 k | Mint64 => do r <- ireg_of dst; - transl_memory_access (Pld r) (Pldx r) addr args GPR12 k + transl_memory_access (Pld r) (Pldx r) false addr args GPR12 k | Mfloat32 => do r <- freg_of dst; - transl_memory_access (Plfs r) (Plfsx r) addr args GPR12 k + transl_memory_access (Plfs r) (Plfsx r) true addr args GPR12 k | Mfloat64 => do r <- freg_of dst; - transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k + transl_memory_access (Plfd r) (Plfdx r) true addr args GPR12 k | _ => Error (msg "Asmgen.transl_load") end @@ -817,22 +843,22 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) match chunk with | Mint8signed | Mint8unsigned => do r <- ireg_of src; - transl_memory_access (Pstb r) (Pstbx r) addr args temp k + transl_memory_access (Pstb r) (Pstbx r) true addr args temp k | Mint16signed | Mint16unsigned => do r <- ireg_of src; - transl_memory_access (Psth r) (Psthx r) addr args temp k + transl_memory_access (Psth r) (Psthx r) true addr args temp k | Mint32 => do r <- ireg_of src; - transl_memory_access (Pstw r) (Pstwx r) addr args temp k + transl_memory_access (Pstw r) (Pstwx r) true addr args temp k | Mint64 => do r <- ireg_of src; - transl_memory_access (Pstd r) (Pstdx r) addr args temp k + transl_memory_access (Pstd r) (Pstdx r) false addr args temp k | Mfloat32 => do r <- freg_of src; - transl_memory_access (Pstfs r) (Pstfsx r) addr args temp k + transl_memory_access (Pstfs r) (Pstfsx r) true addr args temp k | Mfloat64 => do r <- freg_of src; - transl_memory_access (Pstfd r) (Pstfdx r) addr args temp k + transl_memory_access (Pstfd r) (Pstfdx r) true addr args temp k | _ => Error (msg "Asmgen.transl_store") end. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 2fab6d57..e30ca9ed 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -205,10 +205,13 @@ Remark loadind_label: forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> tail_nolabel k c. Proof. - unfold loadind, accessind; intros. set (ofs' := Ptrofs.to_int ofs) in *. + unfold loadind, accessind ; intros. + set (ofs' := Ptrofs.to_int ofs) in *. + set (ofs_mod := Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *. destruct ty; try discriminate; destruct (preg_of dst); try discriminate; destruct (Int.eq (high_s ofs') Int.zero); + destruct ofs_mod; TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. Qed. @@ -216,10 +219,13 @@ Remark storeind_label: forall base ofs ty src k c, storeind src base ofs ty k = OK c -> tail_nolabel k c. Proof. - unfold storeind, accessind; intros. set (ofs' := Ptrofs.to_int ofs) in *. + unfold storeind, accessind; + intros. set (ofs' := Ptrofs.to_int ofs) in *. + set (ofs_mod := Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *. destruct ty; try discriminate; destruct (preg_of src); try discriminate; destruct (Int.eq (high_s ofs') Int.zero); + destruct ofs_mod; TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. Qed. @@ -298,17 +304,22 @@ Qed. Remark transl_memory_access_label: forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - addr args temp k c, - transl_memory_access mk1 mk2 addr args temp k = OK c -> + unaligned addr args temp k c, + transl_memory_access mk1 mk2 unaligned addr args temp k = OK c -> (forall c r, nolabel (mk1 c r)) -> (forall r1 r2, nolabel (mk2 r1 r2)) -> tail_nolabel k c. Proof. unfold transl_memory_access; intros; destruct addr; TailNoLabel. - destruct (Int.eq (high_s i) Int.zero); TailNoLabel. - destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. + destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero). destruct (Int.eq (high_s i) Int.zero); TailNoLabel. + eapply tail_nolabel_trans. apply loadimm_label. TailNoLabel. + destruct (symbol_is_small_data i i0). destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. + destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel. destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. + destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel. + destruct (unaligned || Int.eq (Int.mods (Ptrofs.to_int i) (Int.repr 4)) Int.zero). destruct (Int.eq (high_s (Ptrofs.to_int i)) Int.zero); TailNoLabel. + eapply tail_nolabel_trans. eapply addimm_label. TailNoLabel. Qed. Remark transl_epilogue_label: diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 9f928ff8..7b0c6266 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -805,6 +805,7 @@ Lemma accessind_load_correct: forall (A: Type) (inj: A -> preg) (instr1: A -> constant -> ireg -> instruction) (instr2: A -> ireg -> ireg -> instruction) + (unaligned: bool) (base: ireg) ofs rx chunk v (rs: regset) m k, (forall rs m r1 cst r2, exec_instr ge fn (instr1 r1 cst r2) rs m = load1 ge chunk (inj r1) cst r2 rs m) -> @@ -813,14 +814,15 @@ Lemma accessind_load_correct: Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v -> base <> GPR0 -> inj rx <> PC -> exists rs', - exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m + exec_straight ge fn (accessind instr1 instr2 unaligned base ofs rx k) rs m k rs' m /\ rs'#(inj rx) = v /\ forall r, r <> PC -> r <> inj rx -> r <> GPR0 -> rs'#r = rs#r. Proof. intros. unfold accessind. set (ofs' := Ptrofs.to_int ofs) in *. + set (ofs_mod := unaligned || Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *. assert (LD: Mem.loadv chunk m (Val.add (rs base) (Vint ofs')) = Some v) by (apply loadv_offset_ptr; auto). - destruct (Int.eq (high_s ofs') Int.zero). + destruct (Int.eq (high_s ofs') Int.zero && ofs_mod). - econstructor; split. apply exec_straight_one. rewrite H. unfold load1. rewrite gpr_or_zero_not_zero by auto. simpl. rewrite LD. eauto. unfold nextinstr. repeat Simplif. @@ -862,6 +864,7 @@ Lemma accessind_store_correct: forall (A: Type) (inj: A -> preg) (instr1: A -> constant -> ireg -> instruction) (instr2: A -> ireg -> ireg -> instruction) + (unaligned: bool) (base: ireg) ofs rx chunk (rs: regset) m m' k, (forall rs m r1 cst r2, exec_instr ge fn (instr1 r1 cst r2) rs m = store1 ge chunk (inj r1) cst r2 rs m) -> @@ -870,13 +873,14 @@ Lemma accessind_store_correct: Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs (inj rx)) = Some m' -> base <> GPR0 -> inj rx <> PC -> inj rx <> GPR0 -> exists rs', - exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m' + exec_straight ge fn (accessind instr1 instr2 unaligned base ofs rx k) rs m k rs' m' /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r. Proof. intros. unfold accessind. set (ofs' := Ptrofs.to_int ofs) in *. + set (ofs_mod := unaligned || Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *. assert (ST: Mem.storev chunk m (Val.add (rs base) (Vint ofs')) (rs (inj rx)) = Some m') by (apply storev_offset_ptr; auto). - destruct (Int.eq (high_s ofs') Int.zero). + destruct (Int.eq (high_s ofs') Int.zero && ofs_mod). - econstructor; split. apply exec_straight_one. rewrite H. unfold store1. rewrite gpr_or_zero_not_zero by auto. simpl. rewrite ST. eauto. unfold nextinstr. repeat Simplif. @@ -1540,8 +1544,8 @@ Qed. (** Translation of memory accesses *) Lemma transl_memory_access_correct: - forall (P: regset -> Prop) mk1 mk2 addr args temp k c (rs: regset) a m m', - transl_memory_access mk1 mk2 addr args temp k = OK c -> + forall (P: regset -> Prop) mk1 mk2 unaligned addr args temp k c (rs: regset) a m m', + transl_memory_access mk1 mk2 unaligned addr args temp k = OK c -> eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a -> temp <> GPR0 -> (forall cst (r1: ireg) (rs1: regset) k, @@ -1559,111 +1563,174 @@ Lemma transl_memory_access_correct: Proof. intros until m'; intros TR ADDR TEMP MK1 MK2. unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in ADDR; inv ADDR. - (* Aindexed *) - case (Int.eq (high_s i) Int.zero). - (* Aindexed short *) - apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. - (* Aindexed long *) - set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))). - exploit (MK1 (Cint (low_s i)) temp rs1 k). - simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. - unfold rs1; Simpl. rewrite Val.add_assoc. -Transparent Val.add. - simpl. rewrite low_high_s. auto. - intros; unfold rs1; Simpl. - intros [rs' [EX' AG']]. - exists rs'. split. apply exec_straight_step with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. - auto. auto. - (* Aindexed2 *) - apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. - (* Aglobal *) - destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR. - (* Aglobal from small data *) - apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. - rewrite add_zero_symbol_address. auto. - auto. - (* Aglobal from relative data *) - set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). - set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))). - exploit (MK1 (Cint Int.zero) temp rs2). - simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. - unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address. auto. - intros; unfold rs2, rs1; Simpl. - intros [rs' [EX' AG']]. - exists rs'; split. apply exec_straight_step with rs1 m; auto. - apply exec_straight_step with rs2 m; auto. simpl. unfold rs2. - rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal. - unfold rs1; Simpl. apply low_high_half_zero. - eexact EX'. auto. - (* Aglobal from absolute data *) - set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). - exploit (MK1 (Csymbol_low i i0) temp rs1). - simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. - unfold rs1. Simpl. rewrite low_high_half_zero. auto. - intros; unfold rs1; Simpl. - intros [rs' [EX' AG']]. - exists rs'; split. apply exec_straight_step with rs1 m; auto. - eexact EX'. auto. - (* Abased *) + - (* Aindexed *) + destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero); [destruct (Int.eq (high_s i) Int.zero) |]. + + (* Aindexed 4 aligned short *) + apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. + (* Aindexed 4 aligned long *) + + set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))). + exploit (MK1 (Cint (low_s i)) temp rs1 k). + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. + unfold rs1; Simpl. rewrite Val.add_assoc. + Transparent Val.add. + simpl. rewrite low_high_s. auto. + intros; unfold rs1; Simpl. + intros [rs' [EX' AG']]. + exists rs'. split. apply exec_straight_step with rs1 m. + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. + auto. auto. + + (* Aindexed non 4 aligned *) + exploit (loadimm_correct GPR0 i (mk2 x GPR0 :: k) rs). + intros (rs' & A & B & C). + exploit (MK2 x GPR0 rs'). + rewrite gpr_or_zero_not_zero; eauto with asmgen. + rewrite B. rewrite C; eauto with asmgen. auto. + intros. destruct H as [rs'' [A1 B1]]. exists rs''. + split. eapply exec_straight_trans. exact A. exact A1. auto. + - (* Aindexed2 *) + apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. + - (* Aglobal *) + destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR. + + (* Aglobal from small data 4 aligned *) + case (unaligned || symbol_ofs_word_aligned i i0). + apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. + rewrite add_zero_symbol_address. auto. auto. + (* Aglobal from small data not aligned *) + set (rs1 := nextinstr (rs#temp <- (Val.add (gpr_or_zero rs GPR0) (const_low ge (Csymbol_sda i i0))))). + exploit (MK1 (Cint Int.zero) temp rs1). rewrite gpr_or_zero_not_zero; auto. + unfold const_low. unfold rs1. Simpl. + rewrite gpr_or_zero_zero. unfold const_low. + rewrite small_data_area_addressing by auto. + rewrite add_zero_symbol_address. rewrite Val.add_commut. + rewrite add_zero_symbol_address. auto. + intros. unfold rs1. Simpl. + intros. destruct H as [rs2 [A B]]. + exists rs2. split. eapply exec_straight_step. reflexivity. + reflexivity. eexact A. apply B. + + (* relative data *) + set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). + set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))). + exploit (MK1 (Cint Int.zero) temp rs2). + simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. + unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address. auto. + intros; unfold rs2, rs1; Simpl. + intros [rs' [EX' AG']]. + exists rs'; split. apply exec_straight_step with rs1 m; auto. + apply exec_straight_step with rs2 m; auto. simpl. unfold rs2. + rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal. + unfold rs1; Simpl. apply low_high_half_zero. + eexact EX'. auto. + + (* Aglobal from absolute data *) + destruct (unaligned || symbol_ofs_word_aligned i i0). + (* Aglobal 4 aligned *) + set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). + exploit (MK1 (Csymbol_low i i0) temp rs1). + simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. + unfold rs1. Simpl. rewrite low_high_half_zero. auto. + intros; unfold rs1; Simpl. + intros [rs' [EX' AG']]. + exists rs'; split. apply exec_straight_step with rs1 m; auto. + eexact EX'. auto. + (* Aglobal non aligned *) + set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). + set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))). + exploit (MK1 (Cint Int.zero) temp rs2). + simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. + unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address. + auto. intros; unfold rs2, rs1; Simpl. + intros [rs' [EX' AG']]. + exists rs'; split. apply exec_straight_step with rs1 m; auto. + apply exec_straight_step with rs2 m; auto. simpl. unfold rs2. + rewrite gpr_or_zero_not_zero; auto. f_equal. f_equal. f_equal. + unfold rs1; Simpl. apply low_high_half_zero. eexact EX'. auto. + -(* Abased *) destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]. - (* Abased from small data *) - set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))). - exploit (MK2 x GPR0 rs1 k). + + (* Abased from small data *) + set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))). + exploit (MK2 x GPR0 rs1 k). simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. unfold rs1; Simpl. rewrite Val.add_commut. auto. intros. unfold rs1; Simpl. - intros [rs' [EX' AG']]. - exists rs'; split. apply exec_straight_step with rs1 m. - unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal. - unfold const_low. rewrite small_data_area_addressing; auto. - apply add_zero_symbol_address. - reflexivity. - assumption. assumption. - (* Abased from relative data *) - set (rs1 := nextinstr (rs#GPR0 <- (rs#x))). - set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))). - set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))). - exploit (MK2 temp GPR0 rs3). + intros [rs' [EX' AG']]. + exists rs'; split. apply exec_straight_step with rs1 m. + unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal. + unfold const_low. rewrite small_data_area_addressing; auto. + apply add_zero_symbol_address. + reflexivity. + assumption. assumption. + + (* Abased from relative data *) + set (rs1 := nextinstr (rs#GPR0 <- (rs#x))). + set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))). + set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))). + exploit (MK2 temp GPR0 rs3). rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl. intros. unfold rs3, rs2, rs1; Simpl. - intros [rs' [EX' AG']]. - exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m). - apply exec_straight_three with rs1 m rs2 m; auto. - simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto. - unfold rs2; Simpl. apply low_high_half_zero. - eexact EX'. auto. - (* Abased absolute *) - set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))). - exploit (MK1 (Csymbol_low i i0) temp rs1 k). + intros [rs' [EX' AG']]. + exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m). + apply exec_straight_three with rs1 m rs2 m; auto. + simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto. + unfold rs2; Simpl. apply low_high_half_zero. + eexact EX'. auto. + + (* Abased absolute *) + destruct (unaligned || symbol_ofs_word_aligned i i0). + (* Abased absolute 4 aligned *) + set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))). + exploit (MK1 (Csymbol_low i i0) temp rs1 k). simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. unfold rs1. Simpl. rewrite Val.add_assoc. rewrite low_high_half. rewrite Val.add_commut. auto. intros; unfold rs1; Simpl. - intros [rs' [EX' AG']]. - exists rs'. split. apply exec_straight_step with rs1 m. - unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. - assumption. assumption. - (* Ainstack *) - set (ofs := Ptrofs.to_int i) in *. - assert (L: Val.lessdef (Val.offset_ptr (rs GPR1) i) (Val.add (rs GPR1) (Vint ofs))). - { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. } - destruct (Int.eq (high_s ofs) Int.zero); inv TR. - apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. - set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). - exploit (MK1 (Cint (low_s ofs)) temp rs1 k). - simpl. rewrite gpr_or_zero_not_zero; auto. - unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. - rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. - congruence. - intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - intros [rs' [EX' AG']]. - exists rs'. split. apply exec_straight_step with rs1 m. - unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. - assumption. assumption. + intros [rs' [EX' AG']]. + exists rs'. split. apply exec_straight_step with rs1 m. + unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. + assumption. assumption. + (* Abased absolute non aligned *) + set (rs1 := nextinstr (rs#GPR0 <- (rs#x))). + set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))). + set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))). + exploit (MK2 temp GPR0 rs3). + rewrite gpr_or_zero_not_zero by eauto with asmgen. + f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl. + intros. unfold rs3, rs2, rs1; Simpl. + intros [rs' [EX' AG']]. + exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m). + apply exec_straight_three with rs1 m rs2 m; auto. + simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto. + unfold rs2; Simpl. apply low_high_half_zero. + eexact EX'. auto. + - (* Ainstack *) + set (ofs := Ptrofs.to_int i) in *. + assert (L: Val.lessdef (Val.offset_ptr (rs GPR1) i) (Val.add (rs GPR1) (Vint ofs))). + { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. } + destruct (unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero); [destruct (Int.eq (high_s ofs) Int.zero)|]; inv TR. + + (* Ainstack short *) + apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. + + (* Ainstack non short *) + set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). + exploit (MK1 (Cint (low_s ofs)) temp rs1 k). + simpl. rewrite gpr_or_zero_not_zero; auto. + unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. + rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. + congruence. + intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + intros [rs' [EX' AG']]. + exists rs'. split. apply exec_straight_step with rs1 m. + unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. + assumption. assumption. + + (* Ainstack non aligned *) + exploit (addimm_correct temp GPR1 ofs (mk1 (Cint Int.zero) temp :: k) rs); eauto with asmgen. + intros [rs1 [A [B C]]]. + exploit (MK1 (Cint Int.zero) temp rs1 k). + rewrite gpr_or_zero_not_zero; auto. rewrite B. simpl. + destruct (rs GPR1); auto. simpl. rewrite Ptrofs.add_zero. + unfold ofs. rewrite Ptrofs.of_int_to_int. auto. auto. + intros. rewrite C; auto. intros [rs2 [EX' AG']]. + exists rs2. split; auto. + eapply exec_straight_trans. eexact A. assumption. Qed. + (** Translation of loads *) Lemma transl_load_correct: @@ -1680,8 +1747,8 @@ Proof. destruct trap; try discriminate. assert (LD: forall v, Val.lessdef a v -> v = a). { intros. inv H2; auto. discriminate H1. } - assert (BASE: forall mk1 mk2 k' chunk' v', - transl_memory_access mk1 mk2 addr args GPR12 k' = OK c -> + assert (BASE: forall mk1 mk2 unaligned k' chunk' v', + transl_memory_access mk1 mk2 unaligned addr args GPR12 k' = OK c -> Mem.loadv chunk' m a = Some v' -> (forall cst (r1: ireg) (rs1: regset), exec_instr ge fn (mk1 cst r1) rs1 m = @@ -1759,8 +1826,8 @@ Local Transparent destroyed_by_store. subst src; simpl; congruence. change (IR GPR12) with (preg_of R12). red; intros; elim n. eapply preg_of_injective; eauto. - assert (BASE: forall mk1 mk2 chunk', - transl_memory_access mk1 mk2 addr args (int_temp_for src) k = OK c -> + assert (BASE: forall mk1 mk2 unaligned chunk', + transl_memory_access mk1 mk2 unaligned addr args (int_temp_for src) k = OK c -> Mem.storev chunk' m a (rs (preg_of src)) = Some m' -> (forall cst (r1: ireg) (rs1: regset), exec_instr ge fn (mk1 cst r1) rs1 m = diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v index 9d7aadd9..b3fdebd0 100644 --- a/powerpc/Builtins1.v +++ b/powerpc/Builtins1.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index e0826877..dc8aa73a 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index a3e945bf..202f4436 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -21,6 +22,7 @@ Extract Constant Asm.high_half => "fun _ _ _ -> assert false". Extract Constant Asm.symbol_is_small_data => "C2C.atom_is_small_data". Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false". Extract Constant Asm.symbol_is_rel_data => "C2C.atom_is_rel_data". +Extract Constant Asm.symbol_is_aligned => "C2C.atom_is_aligned". (* Suppression of stupidly big equality functions *) Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y". -- cgit