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

1 files changed, 14 insertions, 0 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