diff options
-rw-r--r-- | arm/Asmexpand.ml | 14 | ||||
-rw-r--r-- | arm/Machregs.v | 4 | ||||
-rw-r--r-- | arm/Op.v | 19 | ||||
-rw-r--r-- | arm/SelectOp.vp | 1 | ||||
-rw-r--r-- | arm/SelectOpproof.v | 1 | ||||
-rw-r--r-- | backend/Constprop.v | 2 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 233 | ||||
-rw-r--r-- | powerpc/Machregs.v | 4 | ||||
-rw-r--r-- | powerpc/Op.v | 23 | ||||
-rw-r--r-- | powerpc/SelectOp.vp | 3 | ||||
-rw-r--r-- | powerpc/SelectOpproof.v | 3 | ||||
-rw-r--r-- | riscV/Asmexpand.ml | 14 | ||||
-rw-r--r-- | riscV/Machregs.v | 4 | ||||
-rw-r--r-- | riscV/Op.v | 21 | ||||
-rw-r--r-- | riscV/SelectOp.vp | 4 | ||||
-rw-r--r-- | riscV/SelectOpproof.v | 22 | ||||
-rw-r--r-- | test/regression/Results/volatile4 | 2 | ||||
-rw-r--r-- | test/regression/volatile4.c | 8 |
18 files changed, 283 insertions, 99 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 8761e666..a32b0e8b 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -215,6 +215,13 @@ let expand_builtin_vload chunk args res = | [BA_addrglobal(id, ofs)] -> emit (Ploadsymbol (IR14,id,ofs)); expand_builtin_vload_common chunk IR14 _0 res + | [BA_addptr(BA(IR addr), BA_int ofs)] -> + if offset_in_range (Int.add ofs (Memdata.size_chunk chunk)) then + expand_builtin_vload_common chunk addr ofs res + else begin + expand_addimm IR14 addr ofs; + expand_builtin_vload_common chunk IR14 _0 res + end | _ -> assert false @@ -252,6 +259,13 @@ let expand_builtin_vstore chunk args = | [BA_addrglobal(id, ofs); src] -> emit (Ploadsymbol (IR14,id,ofs)); expand_builtin_vstore_common chunk IR14 _0 src + | [BA_addptr(BA(IR addr), BA_int ofs); src] -> + if offset_in_range (Int.add ofs (Memdata.size_chunk chunk)) then + expand_builtin_vstore_common chunk addr ofs src + else begin + expand_addimm IR14 addr ofs; + expand_builtin_vstore_common chunk IR14 _0 src + end | _ -> assert false diff --git a/arm/Machregs.v b/arm/Machregs.v index e97df790..ba3bda7c 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -197,8 +197,8 @@ Global Opaque two_address_op. Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := match ef with - | EF_vload _ => OK_addrany :: nil - | EF_vstore _ => OK_addrany :: OK_default :: nil + | EF_vload _ => OK_addressing :: nil + | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil | EF_annot txt targs => map (fun _ => OK_all) targs | EF_debug kind txt targs => map (fun _ => OK_all) targs @@ -1127,3 +1127,22 @@ Qed. End EVAL_INJECT. +(** * Handling of builtin arguments *) + +Definition builtin_arg_ok_1 + (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := + match c, ba with + | OK_all, _ => true + | OK_const, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => true + | OK_addrstack, BA_addrstack _ => true + | OK_addressing, BA_addrstack _ => true + | OK_addressing, BA_addptr (BA _) (BA_int _) => true + | _, _ => false + end. + +Definition builtin_arg_ok + (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := + match ba with + | (BA _ | BA_splitlong (BA _) (BA _)) => true + | _ => builtin_arg_ok_1 ba c + end. diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index fc2fbe6b..c361df65 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -505,5 +505,6 @@ Nondetfunction builtin_arg (e: expr) := | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs | Eload chunk (Aindexed ofs1) (Eop (Oaddrsymbol id ofs) Enil ::: Enil) => BA_loadglobal chunk id (Ptrofs.add ofs (Ptrofs.of_int ofs1)) + | Eop (Oaddimm n) (e1:::Enil) => BA_addptr (BA e1) (BA_int n) | _ => BA e end. diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index f025e345..d4aac9b6 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -889,6 +889,7 @@ Proof. - inv H. InvEval. simpl in H6; inv H6. constructor; auto. - inv H. InvEval. simpl in H6. rewrite <- Genv.shift_symbol_address_32 in H6 by auto. inv H6. constructor; auto. +- inv H. repeat constructor; auto. - constructor; auto. Qed. diff --git a/backend/Constprop.v b/backend/Constprop.v index 151f8418..d8211ffe 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -98,6 +98,8 @@ Fixpoint builtin_arg_reduction (ae: AE.t) (a: builtin_arg reg) := | BA_int nhi, BA_int nlo => BA_long (Int64.ofwords nhi nlo) | hi', lo' => BA_splitlong hi' lo' end + | BA_addptr a1 a2 => + BA_addptr (builtin_arg_reduction ae a1) (builtin_arg_reduction ae a2) | _ => a end. diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index fc787a35..deab7703 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -165,6 +165,56 @@ 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) + 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) + else begin + emit (Paddis(temp, GPR1, Cint (Asmgen.high_s ofs))); + mk1 temp (Cint (Asmgen.low_s ofs)) + end + | BA_addrglobal(id, ofs) -> + if symbol_is_small_data id ofs then + mk1 GPR0 (Csymbol_sda(id, ofs)) + 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 + emit (Paddis(temp, GPR0, Csymbol_high(id, ofs))); + mk1 temp (Csymbol_low(id, ofs)) + end + | BA_addptr(BA(IR r), BA_int n) -> + 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 + | 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 begin + emit (Paddis(temp, r, Csymbol_high(id, ofs))); + mk1 temp (Csymbol_low(id, ofs)) + end + | BA_addptr(BA(IR r1), BA(IR r2)) -> + mk2 r1 r2 + | _ -> + assert false + let offset_constant cst delta = match cst with | Cint n -> @@ -174,65 +224,76 @@ let offset_constant cst delta = Some (Csymbol_sda(id, Int.add ofs delta)) | _ -> None -let rec expand_builtin_vload_common chunk base offset res = +let expand_load_int64 hi lo base ofs_hi ofs_lo = + if hi <> base then begin + emit (Plwz(hi, ofs_hi, base)); + emit (Plwz(lo, ofs_lo, base)) + end else begin + emit (Plwz(lo, ofs_lo, base)); + emit (Plwz(hi, ofs_hi, base)) + end + +let expand_builtin_vload_1 chunk addr res = match chunk, res with | Mint8unsigned, BR(IR res) -> - emit (Plbz(res, offset, base)) + expand_volatile_access + (fun r c -> emit (Plbz(res, c, r))) + (fun r1 r2 -> emit (Plbzx(res, r1, r2))) + addr GPR11 | Mint8signed, BR(IR res) -> - emit (Plbz(res, offset, base)); - emit (Pextsb(res, 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))) + addr GPR11 | Mint16unsigned, BR(IR res) -> - emit (Plhz(res, offset, base)) + expand_volatile_access + (fun r c -> emit (Plhz(res, c, r))) + (fun r1 r2 -> emit (Plhzx(res, r1, r2))) + addr GPR11 | Mint16signed, BR(IR res) -> - emit (Plha(res, offset, base)) + expand_volatile_access + (fun r c -> emit (Plha(res, c, r))) + (fun r1 r2 -> emit (Plhax(res, r1, r2))) + addr GPR11 | (Mint32 | Many32), BR(IR res) -> - emit (Plwz(res, offset, base)) + expand_volatile_access + (fun r c -> emit (Plwz(res, c, r))) + (fun r1 r2 -> emit (Plwzx(res, r1, r2))) + addr GPR11 | Mfloat32, BR(FR res) -> - emit (Plfs(res, offset, base)) + expand_volatile_access + (fun r c -> emit (Plfs(res, c, r))) + (fun r1 r2 -> emit (Plfsx(res, r1, r2))) + addr GPR11 | (Mfloat64 | Many64), BR(FR res) -> - emit (Plfd(res, offset, base)) + expand_volatile_access + (fun r c -> emit (Plfd(res, c, r))) + (fun r1 r2 -> emit (Plfdx(res, r1, r2))) + addr GPR11 | (Mint64 | Many64), BR(IR res) -> - emit (Pld(res, offset, base)) + expand_volatile_access + (fun r c -> emit (Pld(res, c, r))) + (fun r1 r2 -> emit (Pldx(res, r1, r2))) + addr GPR11 | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) -> - begin match offset_constant offset _4 with - | Some offset' -> - if hi <> base then begin - emit (Plwz(hi, offset, base)); - emit (Plwz(lo, offset', base)) - end else begin - emit (Plwz(lo, offset', base)); - emit (Plwz(hi, offset, base)) - end - | None -> - emit (Paddi(GPR11, base, offset)); - expand_builtin_vload_common chunk GPR11 (Cint _0) res - end + expand_volatile_access + (fun r c -> + match offset_constant c _4 with + | Some c' -> expand_load_int64 hi lo r c c' + | 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)) + addr GPR11 | _, _ -> assert false let expand_builtin_vload chunk args res = match args with - | [BA(IR addr)] -> - expand_builtin_vload_common chunk addr (Cint _0) res - | [BA_addrstack ofs] -> - if offset_in_range ofs then - expand_builtin_vload_common chunk GPR1 (Cint ofs) res - else begin - emit_addimm GPR11 GPR1 ofs; - expand_builtin_vload_common chunk GPR11 (Cint _0) res - end - | [BA_addrglobal(id, ofs)] -> - if symbol_is_small_data id ofs then - expand_builtin_vload_common chunk GPR0 (Csymbol_sda(id, ofs)) res - else if symbol_is_rel_data id ofs then begin - emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs))); - expand_builtin_vload_common chunk GPR11 (Csymbol_rel_low(id, ofs)) res - end else begin - emit (Paddis(GPR11, GPR0, Csymbol_high(id, ofs))); - expand_builtin_vload_common chunk GPR11 (Csymbol_low(id, ofs)) res - end - | _ -> - assert false + | [addr] -> expand_builtin_vload_1 chunk addr res + | _ -> assert false let temp_for_vstore src = let rl = AST.params_of_builtin_arg src in @@ -240,60 +301,62 @@ let temp_for_vstore src = else if not (List.mem (IR GPR12) rl) then GPR12 else GPR10 -let expand_builtin_vstore_common chunk base offset src = +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_builtin_vstore_1 chunk addr src = + let temp = temp_for_vstore src in match chunk, src with | (Mint8signed | Mint8unsigned), BA(IR src) -> - emit (Pstb(src, offset, base)) + expand_volatile_access + (fun r c -> emit (Pstb(src, c, r))) + (fun r1 r2 -> emit (Pstbx(src, r1, r2))) + addr temp | (Mint16signed | Mint16unsigned), BA(IR src) -> - emit (Psth(src, offset, base)) + expand_volatile_access + (fun r c -> emit (Psth(src, c, r))) + (fun r1 r2 -> emit (Psthx(src, r1, r2))) + addr temp | (Mint32 | Many32), BA(IR src) -> - emit (Pstw(src, offset, base)) + expand_volatile_access + (fun r c -> emit (Pstw(src, c, r))) + (fun r1 r2 -> emit (Pstwx(src, r1, r2))) + addr temp | Mfloat32, BA(FR src) -> - emit (Pstfs(src, offset, base)) + expand_volatile_access + (fun r c -> emit (Pstfs(src, c, r))) + (fun r1 r2 -> emit (Pstfsx(src, r1, r2))) + addr temp | (Mfloat64 | Many64), BA(FR src) -> - emit (Pstfd(src, offset, base)) + expand_volatile_access + (fun r c -> emit (Pstfd(src, c, r))) + (fun r1 r2 -> emit (Pstfdx(src, r1, r2))) + addr temp | (Mint64 | Many64), BA(IR src) -> - emit (Pstd(src, offset, base)) + expand_volatile_access + (fun r c -> emit (Pstd(src, c, r))) + (fun r1 r2 -> emit (Pstdx(src, r1, r2))) + addr temp | Mint64, BA_splitlong(BA(IR hi), BA(IR lo)) -> - begin match offset_constant offset _4 with - | Some offset' -> - emit (Pstw(hi, offset, base)); - emit (Pstw(lo, offset', base)) - | None -> - let tmp = temp_for_vstore src in - emit (Paddi(tmp, base, offset)); - emit (Pstw(hi, Cint _0, tmp)); - emit (Pstw(lo, Cint _4, tmp)) - end + expand_volatile_access + (fun r c -> + match offset_constant c _4 with + | Some c' -> expand_store_int64 hi lo r c c' + | 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_load_int64 hi lo temp (Cint _0) (Cint _4)) + addr temp | _, _ -> assert false let expand_builtin_vstore chunk args = match args with - | [BA(IR addr); src] -> - expand_builtin_vstore_common chunk addr (Cint _0) src - | [BA_addrstack ofs; src] -> - if offset_in_range ofs then - expand_builtin_vstore_common chunk GPR1 (Cint ofs) src - else begin - let tmp = temp_for_vstore src in - emit_addimm tmp GPR1 ofs; - expand_builtin_vstore_common chunk tmp (Cint _0) src - end - | [BA_addrglobal(id, ofs); src] -> - if symbol_is_small_data id ofs then - expand_builtin_vstore_common chunk GPR0 (Csymbol_sda(id, ofs)) src - else if symbol_is_rel_data id ofs then begin - let tmp = temp_for_vstore src in - emit (Paddis(tmp, GPR0, Csymbol_rel_high(id, ofs))); - expand_builtin_vstore_common chunk tmp (Csymbol_rel_low(id, ofs)) src - end else begin - let tmp = temp_for_vstore src in - emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs))); - expand_builtin_vstore_common chunk tmp (Csymbol_low(id, ofs)) src - end - | _ -> - assert false + | [addr; src] -> expand_builtin_vstore_1 chunk addr src + | _ -> assert false (* Handling of varargs *) let linkregister_offset = ref _0 diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 6f2c6a03..8442bb52 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -276,8 +276,8 @@ Definition builtin_constraints (ef: external_function) : else if string_dec id "__builtin_mbar" then OK_const :: nil else if string_dec id "__builtin_mr" then OK_const :: OK_const :: nil else nil - | EF_vload _ => OK_addrany :: nil - | EF_vstore _ => OK_addrany :: OK_default :: nil + | EF_vload _ => OK_addressing :: nil + | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil | EF_annot txt targs => map (fun _ => OK_all) targs | EF_debug kind txt targs => map (fun _ => OK_all) targs diff --git a/powerpc/Op.v b/powerpc/Op.v index de4eee48..263c1bd8 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -1318,3 +1318,26 @@ Definition is_rldl_mask (x: int64) : bool := (*r 0s in the high bits, 1s in t Definition is_rldr_mask (x: int64) : bool := (*r 1s in the high bits, 0s in the low bits *) is_mask_rec rlr_transition rlr_accepting Int64.wordsize RLR_S0 (Int64.unsigned x). + +(** * Handling of builtin arguments *) + +Definition builtin_arg_ok_1 + (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := + match c, ba with + | OK_all, _ => true + | OK_const, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => true + | OK_addrstack, BA_addrstack _ => true + | OK_addressing, BA_addrstack _ => true + | OK_addressing, BA_addrglobal _ _ => true + | OK_addressing, BA_addptr (BA _) (BA_int _) => true + | OK_addressing, BA_addptr (BA_addrglobal _ _) (BA _) => true + | OK_addressing, BA_addptr (BA _) (BA _) => true + | _, _ => false + end. + +Definition builtin_arg_ok + (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := + match ba with + | (BA _ | BA_splitlong (BA _) (BA _)) => true + | _ => builtin_arg_ok_1 ba c + end. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 2d9ae7a5..d2ca408a 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -547,5 +547,8 @@ Nondetfunction builtin_arg (e: expr) := | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) | Eload chunk (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs + | Eop (Oaddimm n) (e1:::Enil) => BA_addptr (BA e1) (BA_int n) + | Eop (Oaddsymbol id ofs) (e1:::Enil) => BA_addptr (BA_addrglobal id ofs) (BA e1) + | Eop Oadd (e1:::e2:::Enil) => BA_addptr (BA e1) (BA e2) | _ => BA e end. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 31ddf304..5f87d9b9 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -1038,6 +1038,9 @@ Proof. - subst v. constructor; auto. - inv H. InvEval. simpl in H6; inv H6. constructor; auto. - inv H. InvEval. simpl in H6. inv H6. constructor; auto. +- inv H. repeat constructor; auto. +- inv H. repeat constructor; auto. +- inv H. repeat constructor; auto. - constructor; auto. Qed. diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 02e573fc..d42f4d13 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -251,6 +251,13 @@ let expand_builtin_vload chunk args res = expand_addptrofs X31 X2 ofs; (* X31 <- sp + ofs *) expand_builtin_vload_common chunk X31 _0 res end + | [BA_addptr(BA(IR addr), (BA_int ofs | BA_long ofs))] -> + if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then + expand_builtin_vload_common chunk addr ofs res + else begin + expand_addptrofs X31 addr ofs; (* X31 <- addr + ofs *) + expand_builtin_vload_common chunk X31 _0 res + end | _ -> assert false @@ -286,6 +293,13 @@ let expand_builtin_vstore chunk args = expand_addptrofs X31 X2 ofs; (* X31 <- sp + ofs *) expand_builtin_vstore_common chunk X31 _0 src end + | [BA_addptr(BA(IR addr), (BA_int ofs | BA_long ofs)); src] -> + if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then + expand_builtin_vstore_common chunk addr ofs src + else begin + expand_addptrofs X31 addr ofs; (* X31 <- addr + ofs *) + expand_builtin_vstore_common chunk X31 _0 src + end | _ -> assert false diff --git a/riscV/Machregs.v b/riscV/Machregs.v index e286bbad..c7d558ed 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -244,8 +244,8 @@ Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := match ef with | EF_builtin id sg => nil - | EF_vload _ => OK_addrstack :: nil - | EF_vstore _ => OK_addrstack :: OK_default :: nil + | EF_vload _ => OK_addressing :: nil + | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil | EF_annot txt targs => map (fun _ => OK_all) targs | EF_debug kind txt targs => map (fun _ => OK_all) targs @@ -1338,3 +1338,24 @@ Proof. Qed. End EVAL_INJECT. + +(** * Handling of builtin arguments *) + +Definition builtin_arg_ok_1 + (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := + match c, ba with + | OK_all, _ => true + | OK_const, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => true + | OK_addrstack, BA_addrstack _ => true + | OK_addressing, BA_addrstack _ => true + | OK_addressing, BA_addptr (BA _) (BA_int _) => true + | OK_addressing, BA_addptr (BA _) (BA_long _) => true + | _, _ => false + end. + +Definition builtin_arg_ok + (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := + match ba with + | (BA _ | BA_splitlong (BA _) (BA _)) => true + | _ => builtin_arg_ok_1 ba c + end. diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index b38b7b4d..bb8af2ed 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -442,5 +442,9 @@ Nondetfunction builtin_arg (e: expr) := BA_long (Int64.ofwords h l) | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs + | Eop (Oaddimm n) (e1:::Enil) => + if Archi.ptr64 then BA e else BA_addptr (BA e1) (BA_int n) + | Eop (Oaddlimm n) (e1:::Enil) => + if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e | _ => BA e end. diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index b9652b34..90f077db 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -902,13 +902,23 @@ Theorem eval_builtin_arg: eval_expr ge sp e m nil a v -> CminorSel.eval_builtin_arg ge sp e m (builtin_arg a) v. Proof. - intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval. -- constructor. -- constructor. -- constructor. -- simpl in H5. inv H5. constructor. -- subst v. constructor; auto. + intros until v. unfold builtin_arg; case (builtin_arg_match a); intros. +- InvEval. constructor. +- InvEval. constructor. +- InvEval. constructor. +- InvEval. simpl in H5. inv H5. constructor. +- InvEval. subst v. constructor; auto. - inv H. InvEval. simpl in H6; inv H6. constructor; auto. +- destruct Archi.ptr64 eqn:SF. ++ constructor; auto. ++ InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vint n) else Val.add v1 (Vint n)). + repeat constructor; auto. + rewrite SF; auto. +- destruct Archi.ptr64 eqn:SF. ++ InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vlong n) else Val.add v1 (Vlong n)). + repeat constructor; auto. + rewrite SF; auto. ++ constructor; auto. - constructor; auto. Qed. diff --git a/test/regression/Results/volatile4 b/test/regression/Results/volatile4 index e650a8e5..e00651de 100644 --- a/test/regression/Results/volatile4 +++ b/test/regression/Results/volatile4 @@ -2,4 +2,6 @@ l = 42 a[5] = 255 g = 3 b[2] = -1 +b[i] = -2 p[1] = 80 +p[i] = 81 diff --git a/test/regression/volatile4.c b/test/regression/volatile4.c index b72e1bb9..e363c04c 100644 --- a/test/regression/volatile4.c +++ b/test/regression/volatile4.c @@ -5,7 +5,7 @@ volatile int g = 1; volatile int b[10]; -void test1(volatile int * p) +void test1(volatile int * p, int i) { volatile int l; volatile int a[10]; @@ -18,12 +18,16 @@ void test1(volatile int * p) printf ("g = %d\n", g); b[2] = -1; printf ("b[2] = %d\n", b[2]); + b[i] = -2; + printf ("b[i] = %d\n", b[i]); p[1] = 80; printf ("p[1] = %d\n", p[1]); + p[i] = 81; + printf ("p[i] = %d\n", p[i]); } int main() { - test1(&b[0]); + test1(&b[0], 3); return 0; } |