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.

18 files changed, 95 insertions, 10 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 3dd4cb09..3ac99a47 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -808,6 +808,9 @@ Fixpoint add_equations_builtin_arg
   | BA_splitlong hi lo, BA_splitlong hi' lo' =>
       do e1 <- add_equations_builtin_arg env hi hi' e;
       add_equations_builtin_arg env lo lo' e1
+  | BA_addptr a1 a2, BA_addptr a1' a2' =>
+      do e1 <- add_equations_builtin_arg env a1 a1' e;
+      add_equations_builtin_arg env a2 a2' e1
   | _, _ =>
       None
   end.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 3b2ecd35..6c10d27f 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1560,6 +1560,11 @@ Proof.
   intros (v1 & A & B).
   exploit IHeval_builtin_arg2; eauto. intros (v2 & C & D).
   exists (Val.longofwords v1 v2); split; auto with barg. apply Val.longofwords_lessdef; auto.
+- exploit IHeval_builtin_arg1; eauto. eapply add_equations_builtin_arg_satisf; eauto.
+  intros (v1' & A & B).
+  exploit IHeval_builtin_arg2; eauto. intros (v2' & C & D).
+  econstructor; split. eauto with barg.
+  destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef.
 Qed.
 
 Lemma add_equations_builtin_args_satisf:
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 13aa71d2..07e33efa 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -82,7 +82,8 @@ let translate_annot sp preg_to_dwarf annot =
     | BA_single _
     | BA_loadglobal _
     | BA_addrglobal _
-    | BA_loadstack _ -> None
+    | BA_loadstack _
+    | BA_addptr _ -> None
     | BA_addrstack ofs -> Some (sp,BA_addrstack ofs)
     | BA_splitlong (hi,lo) ->
         begin
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 9439c269..96cb8ae6 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -272,7 +272,11 @@ Inductive eval_builtin_arg: builtin_arg expr -> val -> Prop :=
       eval_builtin_arg (BA_addrglobal id ofs) (Genv.symbol_address ge id ofs)
   | eval_BA_splitlong: forall a1 a2 v1 v2,
       eval_expr nil a1 v1 -> eval_expr nil a2 v2 ->
-      eval_builtin_arg (BA_splitlong (BA a1) (BA a2)) (Val.longofwords v1 v2).
+      eval_builtin_arg (BA_splitlong (BA a1) (BA a2)) (Val.longofwords v1 v2)
+  | eval_BA_addptr: forall a1 v1 a2 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).
 
 End EVAL_EXPR.
 
diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index e5b2ce3a..f491d678 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -68,6 +68,8 @@ Fixpoint transfer_builtin_arg (nv: nval) (na: NA.t) (a: builtin_arg reg) : NA.t
   | BA_loadglobal chunk id ofs => (ne, nmem_add nm (Gl id ofs) (size_chunk chunk))
   | BA_splitlong hi lo =>
       transfer_builtin_arg All (transfer_builtin_arg All na hi) lo
+  | BA_addptr hi lo =>
+      transfer_builtin_arg All (transfer_builtin_arg All na hi) lo
   end.
 
 Definition transfer_builtin_args (na: NA.t) (al: list (builtin_arg reg)) : NA.t :=
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 3f0c5a4c..07c3f84a 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -609,6 +609,12 @@ Proof.
   constructor; auto.
   apply vagree_lessdef.
   apply Val.longofwords_lessdef; apply lessdef_vagree; auto.
+- destruct (transfer_builtin_arg All (ne1, nm1) a1) as [ne' nm'] eqn:TR.
+  exploit IHeval_builtin_arg2; eauto. intros (v2' & A & B & C & D).
+  exploit IHeval_builtin_arg1; eauto. intros (v1' & P & Q & R & S).
+  econstructor; intuition auto.
+  econstructor; eauto.
+  destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef, vagree_lessdef, lessdef_vagree.
 Qed.
 
 Lemma transfer_builtin_args_sound:
@@ -657,6 +663,9 @@ Proof.
 - destruct IHeval_builtin_arg1 as (v1' & A1).
   destruct IHeval_builtin_arg2 as (v2' & A2).
   exists (Val.longofwords v1' v2'); constructor; auto.
+- destruct IHeval_builtin_arg1 as (v1' & A1).
+  destruct IHeval_builtin_arg2 as (v2' & A2).
+  econstructor; econstructor; eauto.
 Qed.
 
 Lemma can_eval_builtin_args:
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 61776743..17139dbd 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -203,6 +203,7 @@ Fixpoint sbuiltinarg (ctx: context) (a: builtin_arg reg) : builtin_arg reg :=
   | BA_loadstack chunk ofs => BA_loadstack chunk (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk)))
   | BA_addrstack ofs => BA_addrstack (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk)))
   | BA_splitlong hi lo => BA_splitlong (sbuiltinarg ctx hi) (sbuiltinarg ctx lo)
+  | BA_addptr a1 a2 => BA_addptr (sbuiltinarg ctx a1) (sbuiltinarg ctx a2)
   | _ => a
   end.
 
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index bc991f0f..c3b0cfc3 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -436,9 +436,13 @@ Proof.
   unfold Senv.symbol_address; simpl; unfold Genv.symbol_address.
   rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
   inv MG. econstructor. eauto. rewrite Ptrofs.add_zero; auto.
-- destruct IHeval_builtin_arg1 as (v1 & A1 & B1).
-  destruct IHeval_builtin_arg2 as (v2 & A2 & B2).
+- destruct IHeval_builtin_arg1 as (v1' & A1 & B1).
+  destruct IHeval_builtin_arg2 as (v2' & A2 & B2).
   econstructor; split. eauto with barg. apply Val.longofwords_inject; auto.
+- destruct IHeval_builtin_arg1 as (v1' & A1 & B1).
+  destruct IHeval_builtin_arg2 as (v2' & A2 & B2).
+  econstructor; split. eauto with barg.
+  destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject.
 Qed.
 
 Lemma tr_builtin_args:
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index c8f8ea82..f54c8698 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -178,6 +178,10 @@ let rec print_annot print_preg sp_reg_name oc = function
       fprintf oc "(%a * 0x100000000 + %a)"
         (print_annot print_preg sp_reg_name) hi
         (print_annot print_preg sp_reg_name) lo
+  | BA_addptr(a1, a2) ->
+      fprintf oc "(%a + %a)"
+        (print_annot print_preg sp_reg_name) a1
+        (print_annot print_preg sp_reg_name) a2
 
 let print_annot_text print_preg sp_reg_name oc txt args =
   let print_fragment = function
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index cfbf57d6..6d81f84b 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -396,6 +396,10 @@ Fixpoint convert_builtin_arg {A: Type} (a: builtin_arg expr) (rl: list A) : buil
       let (hi', rl1) := convert_builtin_arg hi rl in
       let (lo', rl2) := convert_builtin_arg lo rl1 in
       (BA_splitlong hi' lo', rl2)
+  | BA_addptr a1 a2 =>
+      let (a1', rl1) := convert_builtin_arg a1 rl in
+      let (a2', rl2) := convert_builtin_arg a2 rl1 in
+      (BA_addptr a1' a2', rl2)
   end.
 
 Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list A) : list (builtin_arg A) :=
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index b635fd58..93f209b7 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -1010,10 +1010,18 @@ Lemma invert_eval_builtin_arg:
   /\ Events.eval_builtin_arg ge (fun v => v) sp m (fst (convert_builtin_arg a vl)) v
   /\ (forall vl', convert_builtin_arg a (vl ++ vl') = (fst (convert_builtin_arg a vl), vl')).
 Proof.
-  induction 1; simpl; econstructor; intuition eauto with evalexpr barg.
-  constructor.
-  constructor.
-  repeat constructor.
+  induction 1; simpl; try (econstructor; intuition eauto with evalexpr barg; fail).
+- econstructor; split; eauto with evalexpr. split. constructor. auto. 
+- econstructor; split; eauto with evalexpr. split. constructor. auto. 
+- econstructor; split; eauto with evalexpr. split. repeat constructor. auto. 
+- destruct IHeval_builtin_arg1 as (vl1 & A1 & B1 & C1).
+  destruct IHeval_builtin_arg2 as (vl2 & A2 & B2 & C2).
+  destruct (convert_builtin_arg a1 vl1) as [a1' rl1] eqn:E1; simpl in *.
+  destruct (convert_builtin_arg a2 vl2) as [a2' rl2] eqn:E2; simpl in *.
+  exists (vl1 ++ vl2); split.
+  apply eval_exprlist_append; auto.
+  split. rewrite C1, E2. constructor; auto. 
+  intros. rewrite app_ass, !C1, C2, E2. auto.
 Qed.
 
 Lemma invert_eval_builtin_args:
@@ -1057,6 +1065,17 @@ Proof.
   rewrite CV2, CV4; simpl. intros (v2' & A2 & B2 & C2).
   exists (Val.longofwords v1' v2'); split. constructor; auto.
   split; auto. apply Val.longofwords_lessdef; auto.
+- destruct (convert_builtin_arg a1 vl) as [a1' vl1] eqn:CV1; simpl in *.
+  destruct (convert_builtin_arg a2 vl1) as [a2' vl2] eqn:CV2; simpl in *.
+  destruct (convert_builtin_arg a1 rl) as [a1'' rl1] eqn:CV3; simpl in *.
+  destruct (convert_builtin_arg a2 rl1) as [a2'' rl2] eqn:CV4; simpl in *.
+  inv EV.
+  exploit IHa1; eauto. rewrite CV1; simpl; eauto.
+  rewrite CV1, CV3; simpl. intros (v1' & A1 & B1 & C1).
+  exploit IHa2. eexact C1. rewrite CV2; simpl; eauto.
+  rewrite CV2, CV4; simpl. intros (v2' & A2 & B2 & C2).
+  econstructor; split. constructor; eauto.
+  split; auto. destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef.
 Qed.
 
 Lemma transl_eval_builtin_args:
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 9992ab79..fef74706 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -77,6 +77,7 @@ Definition type_of_builtin_arg (a: builtin_arg reg) : typ :=
   | BA_loadglobal chunk id ofs => type_of_chunk chunk
   | BA_addrglobal id ofs => Tptr
   | BA_splitlong hi lo => Tlong
+  | BA_addptr a1 a2 => Tptr
   end.
 
 Definition type_of_builtin_res (r: builtin_res reg) : typ :=
@@ -249,6 +250,7 @@ Definition type_builtin_arg (e: S.typenv) (a: builtin_arg reg) (ty: typ) : res S
   | BA_loadglobal chunk id ofs => type_expect e ty (type_of_chunk chunk)
   | BA_addrglobal id ofs => type_expect e ty Tptr
   | BA_splitlong hi lo => type_expect e ty Tlong
+  | BA_addptr a1 a2 => type_expect e ty Tptr
   end.
 
 Fixpoint type_builtin_args (e: S.typenv) (al: list (builtin_arg reg)) (tyl: list typ) : res S.typenv :=
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index c14852f4..d4d7362d 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -167,6 +167,8 @@ let rec convert_builtin_arg tyenv = function
   | BA_addrglobal(id, ofs) -> BA_addrglobal(id, ofs)
   | BA_splitlong(hi, lo) ->
       BA_splitlong(convert_builtin_arg tyenv hi, convert_builtin_arg tyenv lo)
+  | BA_addptr(a1, a2) ->
+      BA_addptr(convert_builtin_arg tyenv a1, convert_builtin_arg tyenv a2)
 
 let convert_builtin_res tyenv = function
   | BR r ->
@@ -185,6 +187,10 @@ let rec constrain_builtin_arg a cl =
       let (hi', cl1) = constrain_builtin_arg hi cl in
       let (lo', cl2) = constrain_builtin_arg lo cl1 in
       (BA_splitlong(hi', lo'), cl2)
+  | BA_addptr(a1, a2), _ ->
+      let (a1', cl1) = constrain_builtin_arg a1 cl in
+      let (a2', cl2) = constrain_builtin_arg a2 cl1 in
+      (BA_addptr(a1', a2'), cl2)
   | _, _ -> (a, cl)
 
 let rec constrain_builtin_args al cl =
@@ -335,6 +341,7 @@ let rec vset_addarg a after =
   match a with
   | BA v -> VSet.add v after
   | BA_splitlong(hi, lo) -> vset_addarg hi (vset_addarg lo after)
+  | BA_addptr(a1, a2) -> vset_addarg a1 (vset_addarg a2 after)
   | _ -> after
 
 let vset_addargs al after = List.fold_right vset_addarg al after
@@ -432,8 +439,8 @@ let rec dce_parmove srcs dsts after =
 
 let rec keep_builtin_arg after = function
   | BA v -> VSet.mem v after
-  | BA_splitlong(hi, lo) ->
-      keep_builtin_arg after hi && keep_builtin_arg after lo
+  | BA_splitlong(a1, a2) | BA_addptr(a1, a2) ->
+      keep_builtin_arg after a1 && keep_builtin_arg after a2
   | _ -> true
 
 let dce_instr instr after k =
@@ -855,6 +862,10 @@ let rec reload_arg tospill eqs = function
       let (hi', c1, eqs1) = reload_arg tospill eqs hi in
       let (lo', c2, eqs2) = reload_arg tospill eqs1 lo in
       (BA_splitlong(hi', lo'), c1 @ c2, eqs2)
+  | BA_addptr(a1, a2) ->
+      let (a1', c1, eqs1) = reload_arg tospill eqs a1 in
+      let (a2', c2, eqs2) = reload_arg tospill eqs1 a2 in
+      (BA_addptr(a1', a2'), c1 @ c2, eqs2)
   | a -> (a, [], eqs)
 
 let rec reload_args tospill eqs = function
diff --git a/backend/Stacking.v b/backend/Stacking.v
index f51848f2..7b382d05 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -97,6 +97,8 @@ Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg m
   | BA_addrglobal id ofs => BA_addrglobal id ofs
   | BA_splitlong hi lo =>
       BA_splitlong (transl_builtin_arg fe hi) (transl_builtin_arg fe lo)
+  | BA_addptr a1 a2 =>
+      BA_addptr (transl_builtin_arg fe a1) (transl_builtin_arg fe a2)
   end.
 
 (** Translation of a Linear instruction.  Prepends the corresponding
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index b885d22c..d3d901b6 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1744,6 +1744,10 @@ Local Opaque fe.
   destruct IHeval_builtin_arg2 as (v2 & A2 & B2); auto using in_or_app.
   exists (Val.longofwords v1 v2); split; auto with barg.
   apply Val.longofwords_inject; auto.
+- destruct IHeval_builtin_arg1 as (v1' & A1 & B1); auto using in_or_app.
+  destruct IHeval_builtin_arg2 as (v2' & A2 & B2); auto using in_or_app.
+  econstructor; split. eauto with barg.
+  destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject.
 Qed.
 
 Lemma transl_builtin_args_correct:
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index db03d0b3..446ffb7f 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -853,6 +853,10 @@ Proof.
   destruct IHeval_builtin_arg2 as (v2' & A2 & B2); eauto using in_or_app.
   exists (Val.longofwords v1' v2'); split; auto with barg.
   apply Val.longofwords_inject; auto.
+- destruct IHeval_builtin_arg1 as (v1' & A1 & B1); eauto using in_or_app.
+  destruct IHeval_builtin_arg2 as (v2' & A2 & B2); eauto using in_or_app.
+  econstructor; split; eauto with barg.
+  destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject.
 Qed.
 
 Lemma eval_builtin_args_inject:
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 17a518cd..7c4c0525 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -59,6 +59,10 @@ Fixpoint abuiltin_arg (ae: aenv) (am: amem) (rm: romem) (ba: builtin_arg reg) :
   | BA_loadglobal chunk id ofs => loadv chunk rm am (Ptr (Gl id ofs))
   | BA_addrglobal id ofs => Ptr (Gl id ofs)
   | BA_splitlong hi lo => longofwords (abuiltin_arg ae am rm hi) (abuiltin_arg ae am rm lo)
+  | BA_addptr ba1 ba2 =>
+      let v1 := abuiltin_arg ae am rm ba1 in
+      let v2 := abuiltin_arg ae am rm ba2 in
+      if Archi.ptr64 then addl v1 v2 else add v1 v2
   end.
 
 Definition set_builtin_res (br: builtin_res reg) (av: aval) (ae: aenv) : aenv :=
@@ -338,6 +342,7 @@ Proof.
 - simpl. rewrite Ptrofs.add_zero_l. auto with va.
 - eapply loadv_sound; eauto. apply symbol_address_sound; auto.
 - apply symbol_address_sound; auto.
+- destruct Archi.ptr64; auto with va.
 Qed.
 
 Lemma abuiltin_args_sound:
diff --git a/backend/XTL.ml b/backend/XTL.ml
index a1b7f23b..f10efeed 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -133,6 +133,7 @@ let rec type_builtin_arg a ty =
   match a with
   | BA v -> set_var_type v ty
   | BA_splitlong(a1, a2) -> type_builtin_arg a1 Tint; type_builtin_arg a2 Tint
+  | BA_addptr(a1, a2) -> type_builtin_arg a1 coq_Tptr; type_builtin_arg a2 coq_Tptr
   | _ -> ()
 
 let rec type_builtin_args al tyl =