Upgrade the ARM port to the new builtins.

1 files changed, 11 insertions, 9 deletions

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index fea99ef5..aec737ad 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -489,16 +489,18 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | _ => (Aindexed Int.zero, e:::Enil)
   end.
 
-(** ** Arguments of annotations *)
+(** ** Arguments of builtins *)
 
-Nondetfunction annot_arg (e: expr) :=
+Nondetfunction builtin_arg (e: expr) :=
   match e with
-  | Eop (Ointconst n) Enil => AA_int n
-  | Eop (Oaddrsymbol id ofs) Enil => AA_addrglobal id ofs
-  | Eop (Oaddrstack ofs) Enil => AA_addrstack ofs
+  | Eop (Ointconst n) Enil => BA_int n
+  | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs
+  | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs
   | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
-        AA_long (Int64.ofwords h l)
-  | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l)
-  | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs
-  | _ => AA_base e
+        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
+  | Eload chunk (Aindexed ofs1) (Eop (Oaddrsymbol id ofs) Enil ::: Enil) =>
+       BA_loadglobal chunk id (Int.add ofs ofs1)
+  | _ => BA e
   end.