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. --- backend/Allocation.v | 3 +++ backend/Allocproof.v | 5 +++++ backend/Asmexpandaux.ml | 3 ++- backend/CminorSel.v | 6 +++++- backend/Deadcode.v | 2 ++ backend/Deadcodeproof.v | 9 +++++++++ backend/Inlining.v | 1 + backend/Inliningproof.v | 8 ++++++-- backend/PrintAsmaux.ml | 4 ++++ backend/RTLgen.v | 4 ++++ backend/RTLgenproof.v | 27 +++++++++++++++++++++++---- backend/RTLtyping.v | 2 ++ backend/Regalloc.ml | 15 +++++++++++++-- backend/Stacking.v | 2 ++ backend/Stackingproof.v | 4 ++++ backend/Unusedglobproof.v | 4 ++++ backend/ValueAnalysis.v | 5 +++++ backend/XTL.ml | 1 + common/AST.v | 21 +++++++-------------- common/Events.v | 11 ++++++++++- common/PrintAST.ml | 3 +++ test/regression/Makefile | 2 +- test/regression/Results/volatile4 | 5 +++++ test/regression/volatile4.c | 29 +++++++++++++++++++++++++++++ x86/Asmexpand.ml | 2 ++ x86/Machregs.v | 6 +++--- x86/Op.v | 21 +++++++++++++++++++++ x86/SelectOp.vp | 17 +++++++++++++---- x86/SelectOpproof.v | 26 ++++++++++++++++++++++---- 29 files changed, 211 insertions(+), 37 deletions(-) create mode 100644 test/regression/Results/volatile4 create mode 100644 test/regression/volatile4.c 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 = 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 | [] -> () diff --git a/test/regression/Makefile b/test/regression/Makefile index 54745863..25b47c7e 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -10,7 +10,7 @@ LIBS=$(LIBMATH) TESTS=int32 int64 floats floats-basics \ expr1 expr6 funptr2 initializers initializers2 initializers3 \ - volatile1 volatile2 volatile3 \ + volatile1 volatile2 volatile3 volatile4 \ funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \ sizeof1 sizeof2 binops bool for1 switch switch2 compound \ decl1 interop1 bitfields9 ptrs3 \ diff --git a/test/regression/Results/volatile4 b/test/regression/Results/volatile4 new file mode 100644 index 00000000..e650a8e5 --- /dev/null +++ b/test/regression/Results/volatile4 @@ -0,0 +1,5 @@ +l = 42 +a[5] = 255 +g = 3 +b[2] = -1 +p[1] = 80 diff --git a/test/regression/volatile4.c b/test/regression/volatile4.c new file mode 100644 index 00000000..b72e1bb9 --- /dev/null +++ b/test/regression/volatile4.c @@ -0,0 +1,29 @@ +/* Addressing modes in volatiles */ + +#include + +volatile int g = 1; +volatile int b[10]; + +void test1(volatile int * p) +{ + volatile int l; + volatile int a[10]; + + l = 42; + printf ("l = %d\n", l); + a[5] = 0xff; + printf ("a[5] = %d\n", a[5]); + g = 3; + printf ("g = %d\n", g); + b[2] = -1; + printf ("b[2] = %d\n", b[2]); + p[1] = 80; + printf ("p[1] = %d\n", p[1]); +} + +int main() +{ + test1(&b[0]); + return 0; +} 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