From dff22ef6d855973e0e0f05c7203a6bfa9a4cf01a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 15 Jun 2017 15:11:26 +0200 Subject: 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. --- x86/Asmexpand.ml | 2 ++ x86/Machregs.v | 6 +++--- x86/Op.v | 21 +++++++++++++++++++++ x86/SelectOp.vp | 17 +++++++++++++---- x86/SelectOpproof.v | 26 ++++++++++++++++++++++---- 5 files changed, 61 insertions(+), 11 deletions(-) (limited to 'x86') 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. -- cgit