Extend builtin arguments with a pointer addition operator

This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses.

Current status: x86 port only, the only new addressing mode handled is reg + offset.

5 files changed, 61 insertions, 11 deletions

diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 8e69061e..1b716165 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -108,6 +108,8 @@ let addressing_of_builtin_arg = function
   | BA (IR r) -> linear_addr r Z.zero
   | BA_addrstack ofs -> linear_addr RSP (Integers.Ptrofs.unsigned ofs)
   | BA_addrglobal(id, ofs) -> global_addr id ofs
+  | BA_addptr(BA (IR r), BA_int n) -> linear_addr r (Integers.Int.signed n)
+  | BA_addptr(BA (IR r), BA_long n) -> linear_addr r (Integers.Int64.signed n)
   | _ -> assert false
 
 (* Handling of memcpy *)
diff --git a/x86/Machregs.v b/x86/Machregs.v
index ffaf2531..5d1b4515 100644
--- a/x86/Machregs.v
+++ b/x86/Machregs.v
@@ -358,9 +358,9 @@ Definition two_address_op (op: operation) : bool :=
 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_memcpy _ _ => OK_addrany :: OK_addrany :: 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
   | _ => nil
diff --git a/x86/Op.v b/x86/Op.v
index 8ace5067..136c900b 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -1455,3 +1455,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_addrglobal _ _ => true
+  | OK_addressing, BA_addptr (BA _) (BA_int _ | 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/x86/SelectOp.vp b/x86/SelectOp.vp
index 1200c3d7..a1583600 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -516,14 +516,23 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
 
 (** ** Arguments of builtins *)
 
+Nondetfunction builtin_arg_addr (addr: Op.addressing) (el: exprlist) :=
+  match addr, el with
+  | Aindexed n, e1 ::: Enil =>
+      BA_addptr (BA e1) (if Archi.ptr64 then BA_long (Int64.repr n) else BA_int (Int.repr n))
+  | Aglobal id ofs, Enil => BA_addrglobal id ofs
+  | Ainstack ofs, Enil => BA_addrstack ofs
+  | _, _ => BA (Eop (Olea_ptr addr) el)
+  end.
+
 Nondetfunction builtin_arg (e: expr) :=
   match e with
   | Eop (Ointconst n) Enil => BA_int n
   | Eop (Olongconst n) Enil => BA_long n
-  | Eop (Olea (Aglobal id ofs)) Enil => if Archi.ptr64 then BA e else BA_addrglobal id ofs
-  | Eop (Olea (Ainstack ofs)) Enil => if Archi.ptr64 then BA e else BA_addrstack ofs
-  | Eop (Oleal (Aglobal id ofs)) Enil => if Archi.ptr64 then BA_addrglobal id ofs else BA e
-  | Eop (Oleal (Ainstack ofs)) Enil => if Archi.ptr64 then BA_addrstack ofs else BA e
+  | Eop (Olea addr) el =>
+      if Archi.ptr64 then BA e else builtin_arg_addr addr el
+  | Eop (Oleal addr) el =>
+      if Archi.ptr64 then builtin_arg_addr addr el else BA e
   | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
         BA_long (Int64.ofwords h l)
   | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index e2e0b830..fdbadaa8 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -947,6 +947,22 @@ Proof.
 - apply D; auto.
 Qed.
 
+Theorem eval_builtin_arg_addr:
+  forall addr al vl v,
+  eval_exprlist ge sp e m nil al vl ->
+  Op.eval_addressing ge sp addr vl = Some v ->
+  CminorSel.eval_builtin_arg ge sp e m (builtin_arg_addr addr al) v.
+Proof.
+  intros until v. unfold builtin_arg_addr; case (builtin_arg_addr_match addr al); intros; InvEval.
+- set (v2 := if Archi.ptr64 then Vlong (Int64.repr n) else Vint (Int.repr n)).
+  assert (EQ: v = if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2).
+  { unfold Op.eval_addressing in H0; unfold v2; destruct Archi.ptr64; simpl in H0; inv H0; auto. }
+  rewrite EQ. constructor. constructor; auto. unfold v2; destruct Archi.ptr64; constructor.
+- rewrite eval_addressing_Aglobal in H0. inv H0. constructor.
+- rewrite eval_addressing_Ainstack in H0. inv H0. constructor.
+- constructor. econstructor. eauto. rewrite eval_Olea_ptr. auto. 
+Qed. 
+
 Theorem eval_builtin_arg:
   forall a v,
   eval_expr ge sp e m nil a v ->
@@ -955,10 +971,12 @@ Proof.
   intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval.
 - constructor.
 - constructor.
-- constructor.
-- constructor.
-- constructor.
-- constructor.
+- destruct Archi.ptr64 eqn:SF. 
++ constructor; auto.
++ inv H. eapply eval_builtin_arg_addr. eauto. unfold Op.eval_addressing; rewrite SF; assumption.
+- destruct Archi.ptr64 eqn:SF. 
++ inv H. eapply eval_builtin_arg_addr. eauto. unfold Op.eval_addressing; rewrite SF; assumption.
++ constructor; auto.
 - simpl in H5. inv H5. constructor.
 - constructor; auto.
 - inv H. InvEval. rewrite eval_addressing_Aglobal in H6. inv H6. constructor; auto.