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.

3 files changed, 20 insertions, 15 deletions

diff --git a/common/AST.v b/common/AST.v
index 8a46a153..9eeca5b1 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -627,7 +627,8 @@ Inductive builtin_arg (A: Type) : Type :=
   | BA_addrstack (ofs: ptrofs)
   | BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: ptrofs)
   | BA_addrglobal (id: ident) (ofs: ptrofs)
-  | BA_splitlong (hi lo: builtin_arg A).
+  | BA_splitlong (hi lo: builtin_arg A)
+  | BA_addptr (a1 a2: builtin_arg A).
 
 Inductive builtin_res (A: Type) : Type :=
   | BR (x: A)
@@ -639,6 +640,7 @@ Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident :=
   | BA_loadglobal chunk id ofs => id :: nil
   | BA_addrglobal id ofs => id :: nil
   | BA_splitlong hi lo => globals_of_builtin_arg hi ++ globals_of_builtin_arg lo
+  | BA_addptr a1 a2 => globals_of_builtin_arg a1 ++ globals_of_builtin_arg a2
   | _ => nil
   end.
 
@@ -649,6 +651,7 @@ Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A :=
   match a with
   | BA x => x :: nil
   | BA_splitlong hi lo => params_of_builtin_arg hi ++ params_of_builtin_arg lo
+  | BA_addptr a1 a2 => params_of_builtin_arg a1 ++ params_of_builtin_arg a2
   | _ => nil
   end.
 
@@ -675,6 +678,8 @@ Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_ar
   | BA_addrglobal id ofs => BA_addrglobal id ofs
   | BA_splitlong hi lo =>
       BA_splitlong (map_builtin_arg f hi) (map_builtin_arg f lo)
+  | BA_addptr a1 a2 =>
+      BA_addptr (map_builtin_arg f a1) (map_builtin_arg f a2)
   end.
 
 Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B :=
@@ -691,17 +696,5 @@ Inductive builtin_arg_constraint : Type :=
   | OK_default
   | OK_const
   | OK_addrstack
-  | OK_addrglobal
-  | OK_addrany
+  | OK_addressing
   | OK_all.
-
-Definition builtin_arg_ok
-       (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
-  match ba, c with
-  | (BA _ | BA_splitlong (BA _) (BA _)), _ => true
-  | (BA_int _ | BA_long _ | BA_float _ | BA_single _), OK_const => true
-  | BA_addrstack _, (OK_addrstack | OK_addrany) => true
-  | BA_addrglobal _ _, (OK_addrglobal | OK_addrany) => true
-  | _, OK_all => true
-  | _, _ => false
-  end.
diff --git a/common/Events.v b/common/Events.v
index 14cd27c5..ab804aa7 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1555,7 +1555,11 @@ Inductive eval_builtin_arg: builtin_arg A -> val -> Prop :=
       eval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address ge id ofs)
   | eval_BA_splitlong: forall hi lo vhi vlo,
       eval_builtin_arg hi vhi -> eval_builtin_arg lo vlo ->
-      eval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo).
+      eval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo)
+  | eval_BA_addptr: forall a1 a2 v1 v2,
+      eval_builtin_arg a1 v1 -> eval_builtin_arg a2 v2 ->
+      eval_builtin_arg (BA_addptr a1 a2)
+                       (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2).
 
 Definition eval_builtin_args (al: list (builtin_arg A)) (vl: list val) : Prop :=
   list_forall2 eval_builtin_arg al vl.
@@ -1565,6 +1569,7 @@ Lemma eval_builtin_arg_determ:
 Proof.
   induction 1; intros v' EV; inv EV; try congruence.
   f_equal; eauto.
+  apply IHeval_builtin_arg1 in H3. apply IHeval_builtin_arg2 in H5. subst; auto. 
 Qed.
 
 Lemma eval_builtin_args_determ:
@@ -1637,6 +1642,10 @@ Proof.
 - destruct IHeval_builtin_arg1 as (vhi' & P & Q).
   destruct IHeval_builtin_arg2 as (vlo' & R & S).
   econstructor; split; eauto with barg. apply Val.longofwords_lessdef; auto.
+- destruct IHeval_builtin_arg1 as (vhi' & P & Q).
+  destruct IHeval_builtin_arg2 as (vlo' & R & S).
+  econstructor; split; eauto with barg. 
+  destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef.
 Qed.
 
 Lemma eval_builtin_args_lessdef:
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 48172dfd..ac7d2276 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -70,6 +70,9 @@ let rec print_builtin_arg px oc = function
   | BA_splitlong(hi, lo) ->
       fprintf oc "splitlong(%a, %a)"
                  (print_builtin_arg px) hi (print_builtin_arg px) lo
+  | BA_addptr(a1, a2) ->
+      fprintf oc "addptr(%a, %a)"
+                 (print_builtin_arg px) a1 (print_builtin_arg px) a2
 
 let rec print_builtin_args px oc = function
   | [] -> ()