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

5 files changed, 37 insertions, 2 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.