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, 57 insertions, 8 deletions

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.