From 7e8e3efdd69cee4412817f2e29f9ef687bec019b Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 11 Aug 2021 15:21:57 +0200 Subject: Share code for memory access for PowerPC Instead of duplicating the memory access code in `Asmexpand.ml` we move the code for each of the different addressings in `Asmgen.v` into separate functions that then can be reused in `Asmexpand.ml`. --- powerpc/Asmexpand.ml | 186 +++++++++++++++++++------------------------------ powerpc/Asmgen.v | 131 +++++++++++++++++++++------------- powerpc/Asmgenproof.v | 2 +- powerpc/Asmgenproof1.v | 6 +- 4 files changed, 159 insertions(+), 166 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index e663226f..7efa80a6 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -58,6 +58,20 @@ let emit_loadimm r n = let emit_addimm rd rs n = List.iter emit (Asmgen.addimm rd rs n []) +let emit_aindexed mk1 mk2 unaligned r1 temp ofs = + List.iter emit (Asmgen.aindexed mk1 mk2 unaligned r1 temp ofs []) + +let emit_aindexed2 mk r1 r2 = + List.iter emit (Asmgen.aindexed2 mk r1 r2 []) + +let emit_aglobal mk1 mk2 unaligned temp symb ofs = + List.iter emit (Asmgen.aglobal mk1 mk2 unaligned temp symb ofs []) + +let emit_abased mk1 mk2 unaligned r1 temp symb ofs = + List.iter emit (Asmgen.abased mk1 mk2 unaligned r1 temp symb ofs []) + +let emit_ainstack mk1 mk2 unaligned temp ofs = + List.iter emit (Asmgen.ainstack mk1 mk2 unaligned temp ofs []) (* Numbering of bits in the CR register *) let num_crbit = function @@ -175,79 +189,23 @@ let expand_builtin_memcpy sz al args = (* Handling of volatile reads and writes *) let expand_volatile_access - (mk1: ireg -> constant -> unit) - (mk2: ireg -> ireg -> unit) + (mk1: constant -> ireg -> instruction list -> instruction list) + (mk2: ireg -> ireg -> instruction list -> instruction list) ?(ofs_unaligned = true) addr temp = match addr with | BA(IR r) -> - mk1 r (Cint _0) + List.iter emit (mk1 (Cint _0) r []) | BA_addrstack 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))); - emit (Paddi (temp, temp, Cint (Asmgen.low_s ofs))); - mk1 temp (Cint _0) - end + emit_ainstack mk1 mk2 ofs_unaligned temp ofs | BA_addrglobal(id, ofs) -> - if symbol_is_small_data id ofs then - 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 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 + emit_aglobal mk1 mk2 ofs_unaligned temp id ofs | BA_addptr(BA(IR r), BA_int 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))); - emit (Paddi (temp, temp, Cint (Asmgen.low_s n))); - mk1 temp (Cint _0) - end + emit_aindexed mk1 mk2 ofs_unaligned r temp n | BA_addptr(BA_addrglobal(id, ofs), BA(IR r)) -> - if symbol_is_small_data id ofs then begin - emit (Paddi(GPR0, GPR0, Csymbol_sda(id, ofs))); - mk2 r GPR0 - end else if symbol_is_rel_data id ofs then begin - emit (Pmr(GPR0, r)); - emit (Paddis(temp, GPR0, Csymbol_rel_high(id, ofs))); - emit (Paddi(temp, temp, Csymbol_rel_low(id, ofs))); - mk2 temp GPR0 - 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 + emit_abased mk1 mk2 ofs_unaligned r temp id ofs | BA_addptr(BA(IR r1), BA(IR r2)) -> - mk2 r1 r2 + emit_aindexed2 mk2 r1 r2 | _ -> assert false @@ -260,69 +218,69 @@ let offset_constant cst delta = Some (Csymbol_sda(id, Int.add ofs delta)) | _ -> None -let expand_load_int64 hi lo base ofs_hi ofs_lo = +let expand_load_int64 hi lo base ofs_hi ofs_lo k = if hi <> base then begin - emit (Plwz(hi, ofs_hi, base)); - emit (Plwz(lo, ofs_lo, base)) + Plwz(hi, ofs_hi, base) :: + Plwz(lo, ofs_lo, base) :: k end else begin - emit (Plwz(lo, ofs_lo, base)); - emit (Plwz(hi, ofs_hi, base)) + Plwz(lo, ofs_lo, base) :: + Plwz(hi, ofs_hi, base) :: k end let expand_builtin_vload_1 chunk addr res = match chunk, res with | Mint8unsigned, BR(IR res) -> expand_volatile_access - (fun r c -> emit (Plbz(res, c, r))) - (fun r1 r2 -> emit (Plbzx(res, r1, r2))) + (fun c r k -> Plbz(res, c, r) :: k) + (fun r1 r2 k -> Plbzx(res, r1, r2) :: k) addr GPR11 | Mint8signed, BR(IR res) -> expand_volatile_access - (fun r c -> emit (Plbz(res, c, r)); emit (Pextsb(res, res))) - (fun r1 r2 -> emit (Plbzx(res, r1, r2)); emit (Pextsb(res, res))) + (fun c r k-> Plbz(res, c, r) :: Pextsb(res, res) :: k) + (fun r1 r2 k -> Plbzx(res, r1, r2) :: Pextsb(res, res) :: k) addr GPR11 | Mint16unsigned, BR(IR res) -> expand_volatile_access - (fun r c -> emit (Plhz(res, c, r))) - (fun r1 r2 -> emit (Plhzx(res, r1, r2))) + (fun c r k -> Plhz(res, c, r) :: k) + (fun r1 r2 k -> Plhzx(res, r1, r2) :: k) addr GPR11 | Mint16signed, BR(IR res) -> expand_volatile_access - (fun r c -> emit (Plha(res, c, r))) - (fun r1 r2 -> emit (Plhax(res, r1, r2))) + (fun c r k-> Plha(res, c, r) :: k) + (fun r1 r2 k -> Plhax(res, r1, r2) :: k) addr GPR11 | (Mint32 | Many32), BR(IR res) -> expand_volatile_access - (fun r c -> emit (Plwz(res, c, r))) - (fun r1 r2 -> emit (Plwzx(res, r1, r2))) + (fun c r k-> Plwz(res, c, r) :: k) + (fun r1 r2 k -> Plwzx(res, r1, r2) :: k) addr GPR11 | Mfloat32, BR(FR res) -> expand_volatile_access - (fun r c -> emit (Plfs(res, c, r))) - (fun r1 r2 -> emit (Plfsx(res, r1, r2))) + (fun c r k-> Plfs(res, c, r) :: k) + (fun r1 r2 k -> Plfsx(res, r1, r2) :: k) addr GPR11 | (Mfloat64 | Many64), BR(FR res) -> expand_volatile_access - (fun r c -> emit (Plfd(res, c, r))) - (fun r1 r2 -> emit (Plfdx(res, r1, r2))) + (fun c r k-> Plfd(res, c, r) :: k) + (fun r1 r2 k -> Plfdx(res, r1, r2) :: k) addr GPR11 | (Mint64 | Many64), BR(IR res) -> expand_volatile_access - (fun r c -> emit (Pld(res, c, r))) - (fun r1 r2 -> emit (Pldx(res, r1, r2))) + (fun c r k-> Pld(res, c, r) :: k) + (fun r1 r2 k -> Pldx(res, r1, r2) :: k) ~ofs_unaligned:false addr GPR11 | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) -> expand_volatile_access - (fun r c -> + (fun c r k-> match offset_constant c _4 with - | Some c' -> expand_load_int64 hi lo r c c' + | Some c' -> expand_load_int64 hi lo r c c' k | None -> - emit (Paddi(GPR11, r, c)); - expand_load_int64 hi lo GPR11 (Cint _0) (Cint _4)) - (fun r1 r2 -> - emit (Padd(GPR11, r1, r2)); - expand_load_int64 hi lo GPR11 (Cint _0) (Cint _4)) + Paddi(GPR11, r, c) :: + expand_load_int64 hi lo GPR11 (Cint _0) (Cint _4) k) + (fun r1 r2 k -> + Padd(GPR11, r1, r2) :: + expand_load_int64 hi lo GPR11 (Cint _0) (Cint _4) k) addr GPR11 | _, _ -> assert false @@ -338,55 +296,55 @@ let temp_for_vstore src = else if not (List.mem (IR GPR12) rl) then GPR12 else GPR10 -let expand_store_int64 hi lo base ofs_hi ofs_lo = - emit (Pstw(hi, ofs_hi, base)); - emit (Pstw(lo, ofs_lo, base)) +let expand_store_int64 hi lo base ofs_hi ofs_lo k = + Pstw(hi, ofs_hi, base) :: + Pstw(lo, ofs_lo, base) :: k let expand_builtin_vstore_1 chunk addr src = let temp = temp_for_vstore src in match chunk, src with | (Mint8signed | Mint8unsigned), BA(IR src) -> expand_volatile_access - (fun r c -> emit (Pstb(src, c, r))) - (fun r1 r2 -> emit (Pstbx(src, r1, r2))) + (fun c r k-> Pstb(src, c, r) :: k) + (fun r1 r2 k -> Pstbx(src, r1, r2) :: k) addr temp | (Mint16signed | Mint16unsigned), BA(IR src) -> expand_volatile_access - (fun r c -> emit (Psth(src, c, r))) - (fun r1 r2 -> emit (Psthx(src, r1, r2))) + (fun c r k-> Psth(src, c, r) :: k) + (fun r1 r2 k -> Psthx(src, r1, r2) :: k) addr temp | (Mint32 | Many32), BA(IR src) -> expand_volatile_access - (fun r c -> emit (Pstw(src, c, r))) - (fun r1 r2 -> emit (Pstwx(src, r1, r2))) + (fun c r k-> Pstw(src, c, r) :: k) + (fun r1 r2 k -> Pstwx(src, r1, r2) :: k) addr temp | Mfloat32, BA(FR src) -> expand_volatile_access - (fun r c -> emit (Pstfs(src, c, r))) - (fun r1 r2 -> emit (Pstfsx(src, r1, r2))) + (fun c r k-> Pstfs(src, c, r) :: k) + (fun r1 r2 k -> Pstfsx(src, r1, r2) :: k) addr temp | (Mfloat64 | Many64), BA(FR src) -> expand_volatile_access - (fun r c -> emit (Pstfd(src, c, r))) - (fun r1 r2 -> emit (Pstfdx(src, r1, r2))) + (fun c r k-> Pstfd(src, c, r) :: k) + (fun r1 r2 k -> Pstfdx(src, r1, r2) :: k) addr temp | (Mint64 | Many64), BA(IR src) -> expand_volatile_access - (fun r c -> emit (Pstd(src, c, r))) - (fun r1 r2 -> emit (Pstdx(src, r1, r2))) + (fun c r k-> Pstd(src, c, r) :: k) + (fun r1 r2 k -> Pstdx(src, r1, r2) :: k) ~ofs_unaligned:false addr temp | Mint64, BA_splitlong(BA(IR hi), BA(IR lo)) -> expand_volatile_access - (fun r c -> + (fun c r k -> match offset_constant c _4 with - | Some c' -> expand_store_int64 hi lo r c c' + | Some c' -> expand_store_int64 hi lo r c c' k | None -> - emit (Paddi(temp, r, c)); - expand_store_int64 hi lo temp (Cint _0) (Cint _4)) - (fun r1 r2 -> - emit (Padd(temp, r1, r2)); - expand_store_int64 hi lo temp (Cint _0) (Cint _4)) + Paddi(temp, r, c) :: + expand_store_int64 hi lo temp (Cint _0) (Cint _4) k) + (fun r1 r2 k -> + Padd(temp, r1, r2) :: + expand_store_int64 hi lo temp (Cint _0) (Cint _4) k) addr temp | _, _ -> assert false diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 0a75ad58..7b6ac9af 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -730,6 +730,82 @@ 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 aindexed + (mk1: constant -> ireg -> code -> code) + (mk2: ireg -> ireg -> code -> code) + (unaligned : bool) (r1 temp: ireg) (ofs: int) (k: code) := + 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)). + +Definition aindexed2 + (mk: ireg -> ireg -> code -> code) + (r1 r2: ireg) (k: code) := + mk r1 r2 k. + +Definition aglobal + (mk1: constant -> ireg -> code -> code) + (mk2: ireg -> ireg -> code -> code) + (unaligned : bool) (temp: ireg) + symb ofs k := + 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) :: + Paddi temp temp (Csymbol_low symb ofs) :: + mk1 (Cint Int.zero) temp k. + +Definition abased + (mk1: constant -> ireg -> code -> code) + (mk2: ireg -> ireg -> code -> code) + (unaligned : bool) (r1 temp: ireg) + symb ofs k := + if symbol_is_small_data symb ofs then + Paddi GPR0 GPR0 (Csymbol_sda symb ofs) :: + mk2 r1 GPR0 k + else if symbol_is_rel_data symb ofs then + Pmr GPR0 r1 :: + Paddis temp GPR0 (Csymbol_rel_high symb ofs) :: + Paddi temp temp (Csymbol_rel_low symb ofs) :: + mk2 temp GPR0 k + else if unaligned || symbol_ofs_word_aligned symb ofs then + Paddis temp r1 (Csymbol_high symb ofs) :: + 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. + +Definition ainstack + (mk1 : constant -> ireg -> code -> code) + (mk2 : ireg -> ireg -> code -> code) + (unaligned : bool) (temp: ireg) ofs k := + 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). + Definition transl_memory_access (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) @@ -739,63 +815,18 @@ Definition transl_memory_access match addr, args with | Aindexed ofs, a1 :: nil => do r1 <- ireg_of a1; - 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))) + OK (aindexed (fun c r k => mk1 c r :: k) (fun r1 r2 k => mk2 r1 r2 :: k) unaligned r1 temp ofs k) | Aindexed2, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (mk2 r1 r2 :: k) + OK (aindexed2 (fun r1 r2 k => mk2 r1 r2 :: k) r1 r2 k) | Aglobal symb ofs, nil => - 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) :: - Paddi temp temp (Csymbol_low symb ofs) :: - mk1 (Cint Int.zero) temp :: k) + OK (aglobal (fun c r k => mk1 c r :: k) (fun r1 r2 k => mk2 r1 r2 :: k) unaligned temp symb ofs k) | Abased symb ofs, a1 :: nil => do r1 <- ireg_of a1; - OK (if symbol_is_small_data symb ofs then - Paddi GPR0 GPR0 (Csymbol_sda symb ofs) :: - mk2 r1 GPR0 :: k - else if symbol_is_rel_data symb ofs then - Pmr GPR0 r1 :: - Paddis temp GPR0 (Csymbol_rel_high symb ofs) :: - Paddi temp temp (Csymbol_rel_low symb ofs) :: - mk2 temp GPR0 :: k - else if unaligned || symbol_ofs_word_aligned symb ofs then - Paddis temp r1 (Csymbol_high symb ofs) :: - 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) + OK (abased (fun c r k => mk1 c r :: k) (fun r1 r2 k => mk2 r1 r2 :: k) unaligned r1 temp symb ofs k) | Ainstack ofs, nil => let ofs := Ptrofs.to_int ofs in - 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)) + OK (ainstack (fun c r k => mk1 c r :: k) (fun r1 r2 k => mk2 r1 r2 :: k) unaligned temp ofs k) | _, _ => Error(msg "Asmgen.transl_memory_access") end. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 2730e3d6..85541118 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -310,7 +310,7 @@ Remark transl_memory_access_label: (forall r1 r2, nolabel (mk2 r1 r2)) -> tail_nolabel k c. Proof. - unfold transl_memory_access; intros; destruct addr; TailNoLabel. + unfold transl_memory_access, aindexed, aindexed2, aglobal, abased, ainstack; intros; destruct addr; 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. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 7268b407..6ae520ef 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1564,6 +1564,7 @@ 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 *) + unfold 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. @@ -1590,6 +1591,7 @@ Proof. - (* Aindexed2 *) apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. - (* Aglobal *) + unfold aglobal in *. 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). @@ -1643,7 +1645,8 @@ Proof. 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 *) + - (* Abased *) + unfold abased in *. 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))). @@ -1700,6 +1703,7 @@ Proof. unfold rs2; Simpl. apply low_high_half_zero. eexact EX'. auto. - (* Ainstack *) + unfold ainstack in *. 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. } -- cgit From 9e30fa95607cf357ab7c18a4773edf6b6f84c7d7 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 6 Sep 2021 18:03:41 +0200 Subject: Fix the type and the semantics of BI_bsel The return type is Tint8unsigned (i.e. _Bool), not Tint. --- powerpc/Builtins1.v | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v index b3fdebd0..f212f141 100644 --- a/powerpc/Builtins1.v +++ b/powerpc/Builtins1.v @@ -47,22 +47,35 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with - | BI_isel | BI_uisel | BI_bsel => + | BI_isel | BI_uisel => mksignature (Tint :: Tint :: Tint :: nil) Tint cc_default | BI_isel64 | BI_uisel64 => mksignature (Tint :: Tlong :: Tlong :: nil) Tlong cc_default + | BI_bsel => + mksignature (Tint :: Tint :: Tint :: nil) Tint8unsigned cc_default | BI_mulhw | BI_mulhwu => mksignature (Tint :: Tint :: nil) Tint cc_default | BI_mulhd | BI_mulhdu => mksignature (Tlong :: Tlong :: nil) Tlong cc_default end. +Definition isel {A: Type} (c: int) (n1 n2: A) : A := + if Int.eq c Int.zero then n2 else n1. + +Program Definition bsel (c n1 n2: int) : { n : int | n = Int.zero_ext 8 n } := + Int.zero_ext 8 (isel c n1 n2). +Next Obligation. + symmetry. apply Int.zero_ext_idem. lia. +Qed. + Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with - | BI_isel | BI_uisel | BI_bsel => - mkbuiltin_n3t Tint Tint Tint Tint (fun c n1 n2 => if Int.eq c Int.zero then n2 else n1) + | BI_isel | BI_uisel => + mkbuiltin_n3t Tint Tint Tint Tint isel | BI_isel64 | BI_uisel64 => - mkbuiltin_n3t Tint Tlong Tlong Tlong (fun c n1 n2 => if Int.eq c Int.zero then n2 else n1) + mkbuiltin_n3t Tint Tlong Tlong Tlong isel + | BI_bsel => + mkbuiltin_n3t Tint Tint Tint Tint8unsigned bsel | BI_mulhw => mkbuiltin_n2t Tint Tint Tint Int.mulhs | BI_mulhwu => -- cgit From c34d25e011402aedad62b3fe9b7b04989df4522e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 23 Sep 2021 12:52:11 +0200 Subject: Fix wrong expansion of __builtin_memcpy_aligned In the "small" case, there was an error in the choice of temporary registers to use when one argument is a stack location and the other is a register. The chosen temporary could conflict with the argument that resides in a register. Fixes: #412 --- powerpc/Asmexpand.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 7efa80a6..45b3f708 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -118,8 +118,8 @@ let memcpy_small_arg sz arg tmp = assert false let expand_builtin_memcpy_small sz al src dst = - let (tsrc, tdst) = - if dst <> BA (IR GPR11) then (GPR11, GPR12) else (GPR12, GPR11) in + let tsrc = if dst <> BA (IR GPR11) then GPR11 else GPR12 in + let tdst = if dst <> BA (IR GPR12) then GPR12 else GPR11 in let (rsrc, osrc) = memcpy_small_arg sz src tsrc in let (rdst, odst) = memcpy_small_arg sz dst tdst in let rec copy osrc odst sz = -- cgit