Extend builtin arguments with a pointer addition operator, continued

- Add support for PowerPC, with all addressing modes.
- Add support for ARM, with "reg + ofs" addressing mode.
- Add support for RISC-V, with the one addressing mode.
- Constprop.v: forgot to recurse in BA_addptr
- volatile4 test: more tests

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
diff --git a/arm/Op.v b/arm/Op.v
index 2e919758..9515557d 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -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
diff --git a/riscV/Op.v b/riscV/Op.v
index ce90ebee..ae5a1017 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -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;
 }