From 9c7c84cc40eaacc1e2c13091165785cddecba5ad Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jun 2010 08:27:14 +0000 Subject: Support for inlined built-ins. AST: add ef_inline flag to external functions. Selection: recognize calls to inlined built-ins and inline them as Sbuiltin. CminorSel to Asm: added Sbuiltin/Ibuiltin instruction. PrintAsm: adapted expansion of builtins. C2Clight: adapted detection of builtins. Conventions: refactored in a machine-independent part (backend/Conventions) and a machine-dependent part (ARCH/SYS/Conventions1). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Allocation.v | 4 ++ backend/Allocproof.v | 15 +++++- backend/Alloctyping.v | 2 + backend/Bounds.v | 2 + backend/CMparser.mly | 4 +- backend/CSE.v | 4 +- backend/CSEproof.v | 32 +++++++----- backend/Cminor.v | 4 +- backend/CminorSel.v | 11 +++- backend/Coloring.v | 2 + backend/Coloringaux.ml | 10 ++-- backend/Coloringproof.v | 70 +++++++++++--------------- backend/Constprop.v | 2 + backend/Constpropproof.v | 11 ++++ backend/LTL.v | 16 ++++-- backend/LTLin.v | 10 +++- backend/LTLintyping.v | 9 +++- backend/LTLtyping.v | 10 +++- backend/Linear.v | 20 +++++--- backend/Linearize.v | 2 + backend/Linearizeaux.ml | 1 + backend/Linearizeproof.v | 17 +++++++ backend/Linearizetyping.v | 1 + backend/Lineartyping.v | 6 +++ backend/Locations.v | 23 +++++++++ backend/Mach.v | 5 +- backend/Machabstr.v | 15 ++++-- backend/Machabstr2concr.v | 15 +++++- backend/Machconcr.v | 15 ++++-- backend/Machtyping.v | 13 +++-- backend/RTL.v | 15 +++++- backend/RTLgen.v | 6 +++ backend/RTLgenproof.v | 16 ++++++ backend/RTLgenspec.v | 11 ++++ backend/RTLtyping.v | 30 +++++++++-- backend/RTLtypingaux.ml | 11 ++++ backend/Reload.v | 5 ++ backend/Reloadproof.v | 106 ++++++++++++++++++++------------------- backend/Reloadtyping.v | 9 +++- backend/Selection.v | 51 ++++++++++++++----- backend/Selectionproof.v | 125 +++++++++++++++++++++++++++++++++------------- backend/Stacking.v | 2 + backend/Stackingproof.v | 14 +++++- backend/Stackingtyping.v | 3 ++ backend/Tailcall.v | 4 +- backend/Tailcallproof.v | 15 +++++- backend/Tunneling.v | 2 + backend/Tunnelingproof.v | 8 +++ 48 files changed, 574 insertions(+), 210 deletions(-) (limited to 'backend') diff --git a/backend/Allocation.v b/backend/Allocation.v index b802f4ac..69fb32fa 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -101,6 +101,8 @@ Definition transfer (reg_sum_live ros (reg_dead res after)) | Itailcall sig ros args => reg_list_live args (reg_sum_live ros Regset.empty) + | Ibuiltin ef args res s => + reg_list_live args (reg_dead res after) | Icond cond args ifso ifnot => reg_list_live args after | Ijumptable arg tbl => @@ -167,6 +169,8 @@ Definition transf_instr (assign res) s | Itailcall sig ros args => Ltailcall sig (sum_left_map assign ros) (List.map assign args) + | Ibuiltin ef args res s => + Lbuiltin ef (List.map assign args) (assign res) s | Icond cond args ifso ifnot => Lcond cond (List.map assign args) ifso ifnot | Ijumptable arg tbl => diff --git a/backend/Allocproof.v b/backend/Allocproof.v index c5d6adc3..d06c26fa 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -330,7 +330,7 @@ Lemma agree_postcall: forall live args ros res rs v (ls: locset), (forall r, Regset.In r live -> r <> res -> - ~(In (assign r) Conventions.destroyed_at_call)) -> + ~(In (assign r) destroyed_at_call)) -> (forall r, Regset.In r live -> r <> res -> assign r <> assign res) -> agree (reg_list_live args (reg_sum_live ros (reg_dead res live))) rs ls -> @@ -676,6 +676,19 @@ Proof. rewrite (sig_function_translated _ _ TF). eauto. rewrite H1. econstructor; eauto. + (* Ibuiltin *) + econstructor; split. + eapply exec_Lbuiltin; eauto. TranslInstr. + replace (map ls (@map reg loc assign args)) with (rs##args). + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + eapply agree_eval_regs; eauto. + generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). + unfold correct_alloc_instr. intro CORR. + MatchStates. + eapply agree_assign_live; eauto. + eapply agree_reg_list_live; eauto. + (* Icond, true *) assert (COND: eval_condition cond (map ls (map assign args)) = Some true). replace (map ls (map assign args)) with (rs##args). auto. diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index 260297f2..a6536831 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -139,6 +139,8 @@ Proof. split. autorewrite with allocty; auto. split. auto with allocty. auto. rewrite transf_unroll; auto. + (* builtin *) + WT. (* cond *) WT. (* jumptable *) diff --git a/backend/Bounds.v b/backend/Bounds.v index 15468c57..514895be 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -72,6 +72,7 @@ Definition instr_within_bounds (i: instruction) := | Lop op args res => mreg_within_bounds res | Lload chunk addr args dst => mreg_within_bounds dst | Lcall sig ros => size_arguments sig <= bound_outgoing b + | Lbuiltin ef args res => mreg_within_bounds res | _ => True end. @@ -103,6 +104,7 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil + | Lbuiltin ef args res => res :: nil | Llabel lbl => nil | Lgoto lbl => nil | Lcond cond args lbl => nil diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 84202096..1cd245ec 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -352,9 +352,7 @@ proc: fn_stackspace = $8; fn_body = $10 }) } | EXTERN STRINGLIT COLON signature - { Coq_pair($2, - External { ef_id = $2; - ef_sig = $4 }) } + { Coq_pair($2, External({ef_id = $2; ef_sig = $4; ef_inline = false})) } ; signature: diff --git a/backend/CSE.v b/backend/CSE.v index ff79be54..dab8fc31 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -189,7 +189,7 @@ Definition add_load (n: numbering) (rd: reg) (** [add_unknown n rd] returns a numbering where [rd] is mapped to a fresh value number, and no equations are added. This is useful - to model instructions with unpredictable results such as [Ialloc]. *) + to model instructions with unpredictable results such as [Ibuiltin]. *) Definition add_unknown (n: numbering) (rd: reg) := mknumbering (Psucc n.(num_next)) @@ -348,6 +348,8 @@ Definition transfer (f: function) (pc: node) (before: numbering) := empty_numbering | Itailcall sig ros args => empty_numbering + | Ibuiltin ef args res s => + add_unknown (kill_loads before) res | Icond cond args ifso ifnot => before | Ijumptable arg tbl => diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 445c1af9..c5670e8d 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -232,7 +232,7 @@ Proof. apply wf_kill_loads; auto. apply wf_empty_numbering. apply wf_empty_numbering. -(* apply wf_add_unknown; auto. *) + apply wf_add_unknown. apply wf_kill_loads; auto. Qed. (** As a consequence, the numberings computed by the static analysis @@ -582,21 +582,16 @@ Proof. Qed. Lemma kill_load_satisfiable: - forall n rs chunk addr v m', - Mem.storev chunk m addr v = Some m' -> + forall n rs m', numbering_satisfiable ge sp rs m n -> numbering_satisfiable ge sp rs m' (kill_loads n). Proof. - intros. inversion H0. inversion H1. - generalize (kill_load_eqs_incl n.(num_eqs)). intro. + intros. inv H. destruct H0. generalize (kill_load_eqs_incl n.(num_eqs)). intro. exists x. split; intros. - generalize (H2 _ _ (H4 _ H5)). - generalize (kill_load_eqs_ops _ _ _ H5). - destruct rh; simpl. - intros. destruct addr; simpl in H; try discriminate. - auto. - tauto. - apply H3. assumption. + generalize (H _ _ (H1 _ H2)). + generalize (kill_load_eqs_ops _ _ _ H2). + destruct rh; simpl; tauto. + apply H0. auto. Qed. (** Correctness of [reg_valnum]: if it returns a register [r], @@ -902,7 +897,18 @@ Proof. econstructor; split. eapply exec_Itailcall; eauto. apply sig_preserved. - econstructor; eauto. + econstructor; eauto. + + (* Ibuiltin *) + econstructor; split. + eapply exec_Ibuiltin; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + apply add_unknown_satisfiable. apply wf_kill_loads. apply wf_analyze. + eapply kill_load_satisfiable; eauto. (* Icond true *) econstructor; split. diff --git a/backend/Cminor.v b/backend/Cminor.v index bdfb379a..4e57d3ce 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -133,8 +133,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. (** * Operational semantics (small-step) *) diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 1e87419f..29f7178e 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -70,6 +70,7 @@ Inductive stmt : Type := | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt | Scall : option ident -> signature -> expr -> exprlist -> stmt | Stailcall: signature -> expr -> exprlist -> stmt + | Sbuiltin : option ident -> external_function -> exprlist -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -93,8 +94,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. (** * Operational semantics *) @@ -297,6 +298,12 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) m') + | step_builtin: forall f optid ef al k sp e m vl t v m', + eval_exprlist sp e m nil al vl -> + external_call ef ge vl m t v m' -> + step (State f (Sbuiltin optid ef al) k sp e m) + t (State f Sskip k sp (set_optvar optid v e) m') + | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) diff --git a/backend/Coloring.v b/backend/Coloring.v index 67824ae3..28626cba 100644 --- a/backend/Coloring.v +++ b/backend/Coloring.v @@ -183,6 +183,8 @@ Definition add_edges_instr let largs := loc_arguments sig in add_prefs_call args largs (add_interf_call ros largs g) + | Ibuiltin ef args res s => + add_interf_op res live g | Ireturn (Some r) => add_pref_mreg r (loc_result sig) g | _ => g diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml index d17229ea..63f21906 100644 --- a/backend/Coloringaux.ml +++ b/backend/Coloringaux.ml @@ -22,6 +22,7 @@ open Locations open RTL open RTLtyping open InterfGraph +open Conventions1 open Conventions (* George-Appel graph coloring *) @@ -202,13 +203,13 @@ let rec remove_reserved = function let init_regs() = caller_save_registers.(0) <- - Array.of_list (remove_reserved Conventions.int_caller_save_regs); + Array.of_list (remove_reserved int_caller_save_regs); caller_save_registers.(1) <- - Array.of_list (remove_reserved Conventions.float_caller_save_regs); + Array.of_list (remove_reserved float_caller_save_regs); callee_save_registers.(0) <- - Array.of_list (remove_reserved Conventions.int_callee_save_regs); + Array.of_list (remove_reserved int_callee_save_regs); callee_save_registers.(1) <- - Array.of_list (remove_reserved Conventions.float_callee_save_regs); + Array.of_list (remove_reserved float_callee_save_regs); for i = 0 to num_register_classes - 1 do num_available_registers.(i) <- Array.length caller_save_registers.(i) @@ -789,6 +790,7 @@ let spill_costs f = | Istore(chunk, addr, args, src, _) -> incr_list args; incr src | Icall(sg, ros, args, res, _) -> incr_ros ros; incr_list args; incr res | Itailcall(sg, ros, args) -> incr_ros ros; incr_list args + | Ibuiltin(ef, args, res, _) -> incr_list args; incr res | Icond(cond, args, _, _) -> incr_list args | Ijumptable(arg, _) -> incr arg | Ireturn(Some r) -> incr r diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index 92ac0676..5f035b40 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -384,6 +384,7 @@ Proof. apply add_interf_destroyed_incl. eapply graph_incl_trans; [idtac|apply add_prefs_call_incl]. apply add_interfs_call_incl. + apply add_interf_op_incl. destruct o. apply add_pref_mreg_incl. apply graph_incl_refl. @@ -433,6 +434,10 @@ Definition correct_interf_instr interfere_mreg rfun mr g | inr idfun => True end + | Ibuiltin ef args res s => + forall r, + Regset.In r live -> + r <> res -> interfere r res g | _ => True end. @@ -453,7 +458,8 @@ Proof. split. intros. eapply interfere_mreg_incl; eauto. split. intros. eapply interfere_incl; eauto. destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. - destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. + destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. + intros. eapply interfere_incl; eauto. Qed. Lemma add_edges_instr_correct: @@ -500,38 +506,9 @@ Proof. eapply interfere_mreg_incl. apply add_prefs_call_incl. apply add_interfs_call_correct. auto. -Qed. - -Lemma add_edges_instrs_incl_aux: - forall sig live instrs g, - graph_incl g - (fold_left - (fun (a : graph) (p : positive * instruction) => - add_edges_instr sig (snd p) live !! (fst p) a) - instrs g). -Proof. - induction instrs; simpl; intros. - apply graph_incl_refl. - eapply graph_incl_trans; [idtac|eauto]. - apply add_edges_instr_incl. -Qed. -Lemma add_edges_instrs_correct_aux: - forall sig live instrs g pc i, - In (pc, i) instrs -> - correct_interf_instr live!!pc i - (fold_left - (fun (a : graph) (p : positive * instruction) => - add_edges_instr sig (snd p) live !! (fst p) a) - instrs g). -Proof. - induction instrs; simpl; intros. - elim H. - elim H; intro. - subst a; simpl. eapply correct_interf_instr_incl. - apply add_edges_instrs_incl_aux. - apply add_edges_instr_correct. - auto. + (* Ibuiltin *) + intros. apply add_interf_op_correct; auto. Qed. Lemma add_edges_instrs_correct: @@ -539,11 +516,20 @@ Lemma add_edges_instrs_correct: f.(fn_code)!pc = Some i -> correct_interf_instr live!!pc i (add_edges_instrs f live). Proof. - intros. - unfold add_edges_instrs. - rewrite PTree.fold_spec. - apply add_edges_instrs_correct_aux. - apply PTree.elements_correct. auto. + intros f live. + set (P := fun (c: code) g => + forall pc i, c!pc = Some i -> correct_interf_instr live#pc i g). + set (F := (fun (g : graph) (pc0 : positive) (i0 : instruction) => + add_edges_instr (fn_sig f) i0 live # pc0 g)). + change (P f.(fn_code) (PTree.fold F f.(fn_code) empty_graph)). + apply PTree_Properties.fold_rec; unfold P; intros. + apply H0. rewrite H. auto. + rewrite PTree.gempty in H. congruence. + rewrite PTree.gsspec in H2. destruct (peq pc k). + inv H2. unfold F. apply add_edges_instr_correct. + apply correct_interf_instr_incl with a. + unfold F; apply add_edges_instr_incl. + apply H1; auto. Qed. (** Here are the three correctness properties of the generated @@ -783,7 +769,7 @@ Definition correct_alloc_instr (forall r, Regset.In r live!!pc -> r <> res -> - ~(In (alloc r) Conventions.destroyed_at_call)) + ~(In (alloc r) destroyed_at_call)) /\ (forall r, Regset.In r live!!pc -> r <> res -> alloc r <> alloc res) @@ -796,6 +782,10 @@ Definition correct_alloc_instr | inl rfun => ~(In (alloc rfun) (loc_arguments sig)) | inr idfun => True end) + | Ibuiltin ef args res s => + forall r, + Regset.In r live!!pc -> + r <> res -> alloc r <> alloc res | _ => True end. @@ -877,14 +867,14 @@ Proof. generalize (ALL2 _ _ H2). contradiction. split. auto. destruct s0; auto. red; intros. - generalize (ALL3 r0). generalize (Conventions.loc_arguments_acceptable _ _ H). + generalize (ALL3 r0). generalize (loc_arguments_acceptable _ _ H). unfold loc_argument_acceptable, loc_acceptable. caseEq (alloc r0). intros. elim (ALL2 r0 m). apply C; auto. congruence. auto. destruct s0; auto. (* Itailcall *) destruct s0; auto. red; intros. - generalize (ALL3 r). generalize (Conventions.loc_arguments_acceptable _ _ H0). + generalize (ALL3 r). generalize (loc_arguments_acceptable _ _ H0). unfold loc_argument_acceptable, loc_acceptable. caseEq (alloc r). intros. elim (ALL2 r m). apply H; auto. congruence. auto. diff --git a/backend/Constprop.v b/backend/Constprop.v index e1ab2e9c..03966cdd 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -128,6 +128,8 @@ Definition transfer (f: function) (pc: node) (before: D.t) := D.set dst Unknown before | Icall sig ros args res s => D.set res Unknown before + | Ibuiltin ef args res s => + D.set res Unknown before | _ => before end diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 16f839fc..714468aa 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -355,6 +355,17 @@ Proof. eapply exec_Itailcall; eauto. apply sig_function_translated; auto. constructor; auto. + (* Ibuiltin *) + TransfInstr. intro. + exists (State s' (transf_function f) sp pc' (rs#res <- v) m'); split. + eapply exec_Ibuiltin; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. + eapply analyze_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. simpl; auto. + (* Icond, true *) exists (State s' (transf_function f) sp ifso rs m); split. caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); diff --git a/backend/LTL.v b/backend/LTL.v index a44f3fa4..e1222a52 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -41,6 +41,7 @@ Inductive instruction: Type := | Lstore: memory_chunk -> addressing -> list loc -> loc -> node -> instruction | Lcall: signature -> loc + ident -> list loc -> loc -> node -> instruction | Ltailcall: signature -> loc + ident -> list loc -> instruction + | Lbuiltin: external_function -> list loc -> loc -> node -> instruction | Lcond: condition -> list loc -> node -> node -> instruction | Ljumptable: loc -> list node -> instruction | Lreturn: option loc -> instruction. @@ -61,8 +62,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. (** * Operational semantics *) @@ -91,9 +92,9 @@ Definition postcall_locs (ls: locset) : locset := fun (l: loc) => match l with | R r => - if In_dec Loc.eq (R r) Conventions.temporaries then + if In_dec Loc.eq (R r) temporaries then Vundef - else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then + else if In_dec Loc.eq (R r) destroyed_at_call then Vundef else ls (R r) @@ -196,6 +197,12 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) pc rs m) E0 (Callstate s f' (List.map rs args) m') + | exec_Lbuiltin: + forall s f sp pc rs m ef args res pc' t v m', + (fn_code f)!pc = Some(Lbuiltin ef args res pc') -> + external_call ef ge (map rs args) m t v m' -> + step (State s f sp pc rs m) + t (State s f sp pc' (Locmap.set res v rs) m') | exec_Lcond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> @@ -272,6 +279,7 @@ Definition successors_instr (i: instruction) : list node := | Lstore chunk addr args src s => s :: nil | Lcall sig ros args res s => s :: nil | Ltailcall sig ros args => nil + | Lbuiltin ef args res s => s :: nil | Lcond cond args ifso ifnot => ifso :: ifnot :: nil | Ljumptable arg tbl => tbl | Lreturn optarg => nil diff --git a/backend/LTLin.v b/backend/LTLin.v index 806a7aa9..ee4cb943 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -47,6 +47,7 @@ Inductive instruction: Type := | Lstore: memory_chunk -> addressing -> list loc -> loc -> instruction | Lcall: signature -> loc + ident -> list loc -> loc -> instruction | Ltailcall: signature -> loc + ident -> list loc -> instruction + | Lbuiltin: external_function -> list loc -> loc -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list loc -> label -> instruction @@ -68,8 +69,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. Definition genv := Genv.t fundef unit. @@ -186,6 +187,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m) E0 (Callstate s f' (List.map rs args) m') + | exec_Lbuiltin: + forall s f sp rs m ef args res b t v m', + external_call ef ge (map rs args) m t v m' -> + step (State s f sp (Lbuiltin ef args res :: b) rs m) + t (State s f sp b (Locmap.set res v rs) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 69422e0c..ad3ad644 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -67,8 +67,15 @@ Inductive wt_instr : instruction -> Prop := LTLtyping.call_loc_acceptable sig ros -> locs_acceptable args -> sig.(sig_res) = funsig.(sig_res) -> - Conventions.tailcall_possible sig -> + tailcall_possible sig -> wt_instr (Ltailcall sig ros args) + | wt_Lbuiltin: + forall ef args res, + List.map Loc.type args = (ef_sig ef).(sig_args) -> + Loc.type res = proj_sig_res (ef_sig ef) -> + arity_ok (ef_sig ef).(sig_args) = true -> + locs_acceptable args -> loc_acceptable res -> + wt_instr (Lbuiltin ef args res) | wt_Llabel: forall lbl, wt_instr (Llabel lbl) | wt_Lgoto: forall lbl, diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index e1e43f56..7afae2db 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -88,8 +88,16 @@ Inductive wt_instr : instruction -> Prop := call_loc_acceptable sig ros -> locs_acceptable args -> sig.(sig_res) = funct.(fn_sig).(sig_res) -> - Conventions.tailcall_possible sig -> + tailcall_possible sig -> wt_instr (Ltailcall sig ros args) + | wt_Lbuiltin: + forall ef args res s, + List.map Loc.type args = (ef_sig ef).(sig_args) -> + Loc.type res = proj_sig_res (ef_sig ef) -> + arity_ok (ef_sig ef).(sig_args) = true -> + locs_acceptable args -> loc_acceptable res -> + valid_successor s -> + wt_instr (Lbuiltin ef args res s) | wt_Lcond: forall cond args s1 s2, List.map Loc.type args = type_of_condition cond -> diff --git a/backend/Linear.v b/backend/Linear.v index 71310a97..0f44206d 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -43,6 +43,7 @@ Inductive instruction: Type := | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Lcall: signature -> mreg + ident -> instruction | Ltailcall: signature -> mreg + ident -> instruction + | Lbuiltin: external_function -> list mreg -> mreg -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list mreg -> label -> instruction @@ -63,8 +64,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. Definition genv := Genv.t fundef unit. @@ -153,9 +154,9 @@ Definition return_regs (caller callee: locset) : locset := fun (l: loc) => match l with | R r => - if In_dec Loc.eq (R r) Conventions.temporaries then + if In_dec Loc.eq (R r) temporaries then callee (R r) - else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then + else if In_dec Loc.eq (R r) destroyed_at_call then callee (R r) else caller (R r) @@ -275,6 +276,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m) E0 (Callstate s f' (return_regs (parent_locset s) rs) m') + | exec_Lbuiltin: + forall s f sp rs m ef args res b t v m', + external_call ef ge (reglist rs args) m t v m' -> + step (State s f sp (Lbuiltin ef args res :: b) rs m) + t (State s f sp b (Locmap.set (R res) v rs) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -315,8 +321,8 @@ Inductive step: state -> trace -> state -> Prop := | exec_function_external: forall s ef args res rs1 rs2 m t m', external_call ef ge args m t res m' -> - args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) -> - rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 -> + args = List.map rs1 (loc_arguments (ef_sig ef)) -> + rs2 = Locmap.set (R (loc_result (ef_sig ef))) res rs1 -> step (Callstate s (External ef) rs1 m) t (Returnstate s rs2 m') | exec_return: @@ -337,7 +343,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs (R (Conventions.loc_result (mksignature nil (Some Tint)))) = Vint r -> + rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r -> final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := diff --git a/backend/Linearize.v b/backend/Linearize.v index 31d0318c..fd350c71 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -185,6 +185,8 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code := Lcall sig ros args res :: add_branch s k | LTL.Ltailcall sig ros args => Ltailcall sig ros args :: k + | LTL.Lbuiltin ef args res s => + Lbuiltin ef args res :: add_branch s k | LTL.Lcond cond args s1 s2 => if starts_with s1 k then Lcond (negate_condition cond) args s2 :: add_branch s1 k diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 1f4e5fac..ce7788f4 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -94,6 +94,7 @@ let basic_blocks f joins = | Lstore (chunk, addr, args, src, s) -> next_in_block blk minpc s | Lcall (sig0, ros, args, res, s) -> next_in_block blk minpc s | Ltailcall (sig0, ros, args) -> end_block blk minpc + | Lbuiltin (ef, args, res, s) -> next_in_block blk minpc s | Lcond (cond, args, ifso, ifnot) -> end_block blk minpc; start_block ifso; start_block ifnot | Ljumptable(arg, tbl) -> diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 5f0a2a4e..df750008 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -612,6 +612,23 @@ Proof. destruct (Genv.find_symbol ge i); try discriminate. eapply Genv.find_funct_ptr_prop; eauto. + (* Lbuiltin *) + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + assert (REACH': (reachable f)!!pc' = true). + eapply reachable_successors; eauto. simpl; auto. + exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. + econstructor; split. + eapply plus_left'. + eapply exec_Lbuiltin. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + eapply add_branch_correct; eauto. + eapply is_tail_add_branch. eapply is_tail_cons_left. + eapply is_tail_find_label. eauto. + traceEq. + econstructor; eauto. + (* Lcond true *) destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index 716b66f1..7393535d 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -55,6 +55,7 @@ Proof. apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. apply wt_add_instr. constructor; auto. auto. + apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. destruct (starts_with s1 k); apply wt_add_instr. constructor; auto. rewrite H. destruct cond; auto. apply wt_add_branch; auto. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 028e1200..4ea2ea95 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -87,6 +87,12 @@ Inductive wt_instr : instruction -> Prop := tailcall_possible sig -> match ros with inl r => r = IT1 | _ => True end -> wt_instr (Ltailcall sig ros) + | wt_Lbuiltin: + forall ef args res, + List.map mreg_type args = (ef_sig ef).(sig_args) -> + mreg_type res = proj_sig_res (ef_sig ef) -> + arity_ok (ef_sig ef).(sig_args) = true -> + wt_instr (Lbuiltin ef args res) | wt_Llabel: forall lbl, wt_instr (Llabel lbl) diff --git a/backend/Locations.v b/backend/Locations.v index 295df281..c2fda9c2 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -173,6 +173,18 @@ Module Loc. destruct s; destruct s0; intuition auto. Qed. + Lemma diff_reg_right: + forall l r, l <> R r -> diff (R r) l. + Proof. + intros. simpl. destruct l. congruence. auto. + Qed. + + Lemma diff_reg_left: + forall l r, l <> R r -> diff l (R r). + Proof. + intros. apply diff_sym. apply diff_reg_right. auto. + Qed. + (** [Loc.overlap l1 l2] returns [false] if [l1] and [l2] are different and non-overlapping, and [true] otherwise: either [l1 = l2] or they partially overlap. *) @@ -290,6 +302,14 @@ Module Loc. auto. Qed. + Lemma reg_notin: + forall r ll, ~(In (R r) ll) -> notin (R r) ll. + Proof. + induction ll; simpl; intros. auto. + split. destruct a; auto. intuition congruence. + apply IHll. intuition. + Qed. + (** [Loc.disjoint l1 l2] is true if the locations in list [l1] are different from all locations in list [l2]. *) @@ -352,6 +372,9 @@ Module Loc. | norepet_cons: forall hd tl, notin hd tl -> norepet tl -> norepet (hd :: tl). +(** [Loc.no_overlap l1 l2] holds if elements of [l1] never overlap partially + with elements of [l2]. *) + Definition no_overlap (l1 l2 : list loc) := forall r, In r l1 -> forall s, In s l2 -> r = s \/ Loc.diff r s. diff --git a/backend/Mach.v b/backend/Mach.v index e89ff3b1..2ec312e4 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -58,6 +58,7 @@ Inductive instruction: Type := | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Mcall: signature -> mreg + ident -> instruction | Mtailcall: signature -> mreg + ident -> instruction + | Mbuiltin: external_function -> list mreg -> mreg -> instruction | Mlabel: label -> instruction | Mgoto: label -> instruction | Mcond: condition -> list mreg -> label -> instruction @@ -80,8 +81,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. Definition genv := Genv.t fundef unit. diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 060c6c2b..291a4682 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -24,7 +24,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Op. Require Import Locations. -Require Conventions. +Require Import Conventions. Require Import Mach. Require Stacklayout. @@ -148,7 +148,7 @@ Inductive extcall_args: regset -> frame -> list loc -> list val -> Prop := Definition extcall_arguments (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop := - extcall_args rs fr (Conventions.loc_arguments sg) args. + extcall_args rs fr (loc_arguments sg) args. End FRAME_ACCESSES. @@ -267,6 +267,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs fr m) E0 (Callstate s f' rs m') + | exec_Mbuiltin: + forall s f sp rs fr m ef args res b t v m', + external_call ef ge rs##args m t v m' -> + step (State s f sp (Mbuiltin ef args res :: b) rs fr m) + t (State s f sp b (rs#res <- v) fr m') | exec_Mgoto: forall s f sp lbl c rs fr m c', find_label lbl f.(fn_code) = Some c' -> @@ -304,8 +309,8 @@ Inductive step: state -> trace -> state -> Prop := | exec_function_external: forall s ef args res rs1 rs2 m t m', external_call ef ge args m t res m' -> - extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args -> - rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> + extcall_arguments (parent_function s) rs1 (parent_frame s) (ef_sig ef) args -> + rs2 = (rs1#(loc_result (ef_sig ef)) <- res) -> step (Callstate s (External ef) rs1 m) t (Returnstate s rs2 m') | exec_return: @@ -325,7 +330,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs (Conventions.loc_result (mksignature nil (Some Tint))) = Vint r -> + rs (loc_result (mksignature nil (Some Tint))) = Vint r -> final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 125cd57a..1a97dda5 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -28,6 +28,7 @@ Require Import Mach. Require Import Machtyping. Require Import Machabstr. Require Import Machconcr. +Require Import Conventions. Require Import Asmgenretaddr. (** Two semantics were defined for the Mach intermediate language: @@ -911,7 +912,7 @@ Lemma transl_extcall_arguments: /\ Val.lessdef_list args targs. Proof. unfold Machabstr.extcall_arguments, extcall_arguments; intros. - generalize (Conventions.loc_arguments sg) args H. + generalize (loc_arguments sg) args H. induction l; intros; inv H2. exists (@nil val); split; constructor. exploit IHl; eauto. intros [targs [A B]]. @@ -1023,6 +1024,16 @@ Proof. eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto. econstructor; eauto. eapply match_stacks_free; eauto. + (* Mbuiltin *) + exploit external_call_mem_extends; eauto. eapply regset_lessdef_list; eauto. + intros [v' [ms' [A [B [C D]]]]]. + econstructor; split. + eapply exec_Mbuiltin. eauto. + econstructor; eauto with coqlib. + eapply match_stacks_external_call; eauto. + eapply frame_match_external_call; eauto. + apply regset_lessdef_set; eauto. + (* Mgoto *) econstructor; split. eapply exec_Mgoto; eauto. @@ -1104,7 +1115,7 @@ Lemma equiv_final_states: Proof. intros. inv H0. destruct H. inv H. inv STACKS. constructor. - generalize (RLD (Conventions.loc_result (mksignature nil (Some Tint)))). + generalize (RLD (loc_result (mksignature nil (Some Tint)))). rewrite H1. intro LD. inv LD. auto. Qed. diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 5b63fa8f..b736c8f7 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -23,7 +23,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Op. Require Import Locations. -Require Conventions. +Require Import Conventions. Require Import Mach. Require Stacklayout. Require Asmgenretaddr. @@ -82,7 +82,7 @@ Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop := Definition extcall_arguments (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := - extcall_args rs m sp (Conventions.loc_arguments sg) args. + extcall_args rs m sp (loc_arguments sg) args. (** Mach execution states. *) @@ -187,6 +187,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) E0 (Callstate s f' rs m') + | exec_Mbuiltin: + forall s f sp rs m ef args res b t v m', + external_call ef ge rs##args m t v m' -> + step (State s f sp (Mbuiltin ef args res :: b) rs m) + t (State s f sp b (rs#res <- v) m') | exec_Mgoto: forall s fb f sp lbl c rs m c', Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -234,8 +239,8 @@ Inductive step: state -> trace -> state -> Prop := forall s fb rs m t rs' ef args res m', Genv.find_funct_ptr ge fb = Some (External ef) -> external_call ef ge args m t res m' -> - extcall_arguments rs m (parent_sp s) ef.(ef_sig) args -> - rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) -> + extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> + rs' = (rs#(loc_result (ef_sig ef)) <- res) -> step (Callstate s fb rs m) t (Returnstate s rs' m') | exec_return: @@ -254,7 +259,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs (Conventions.loc_result (mksignature nil (Some Tint))) = Vint r -> + rs (loc_result (mksignature nil (Some Tint))) = Vint r -> final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := diff --git a/backend/Machtyping.v b/backend/Machtyping.v index b0673ca8..7013e296 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -23,7 +23,7 @@ Require Import Events. Require Import Globalenvs. Require Import Op. Require Import Locations. -Require Conventions. +Require Import Conventions. Require Import Mach. (** * Typing rules *) @@ -69,9 +69,14 @@ Inductive wt_instr : instruction -> Prop := wt_instr (Mcall sig ros) | wt_Mtailcall: forall sig ros, - Conventions.tailcall_possible sig -> + tailcall_possible sig -> match ros with inl r => mreg_type r = Tint | inr s => True end -> wt_instr (Mtailcall sig ros) + | wt_Mbuiltin: + forall ef args res, + List.map mreg_type args = (ef_sig ef).(sig_args) -> + mreg_type res = proj_sig_res (ef_sig ef) -> + wt_instr (Mbuiltin ef args res) | wt_Mgoto: forall lbl, wt_instr (Mgoto lbl) @@ -273,7 +278,7 @@ Proof. apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H). econstructor; eauto. -(* apply wt_setreg; auto. exact I. *) + inv H0. apply wt_setreg; auto. rewrite H5. eapply external_call_well_typed; eauto. apply is_tail_find_label with lbl; congruence. apply is_tail_find_label with lbl; congruence. @@ -286,7 +291,7 @@ Proof. econstructor; eauto. apply wt_setreg; auto. generalize (external_call_well_typed _ _ _ _ _ _ _ H). - unfold proj_sig_res, Conventions.loc_result. + unfold proj_sig_res, loc_result. destruct (sig_res (ef_sig ef)). destruct t0; simpl; auto. simpl; auto. diff --git a/backend/RTL.v b/backend/RTL.v index a17c74ee..1c309a0c 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -70,6 +70,10 @@ Inductive instruction: Type := | Itailcall: signature -> reg + ident -> list reg -> instruction (** [Itailcall sig fn args] performs a function invocation in tail-call position. *) + | Ibuiltin: external_function -> list reg -> reg -> node -> instruction + (** [Ibuiltin ef args dest succ] calls the built-in function + identified by [ef], giving it the values of [args] as arguments. + It stores the return value in [dest] and branches to [succ]. *) | Icond: condition -> list reg -> node -> node -> instruction (** [Icond cond args ifso ifnot] evaluates the boolean condition [cond] over the values of registers [args]. If the condition @@ -109,8 +113,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. (** * Operational semantics *) @@ -245,6 +249,12 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) pc rs m) E0 (Callstate s fd rs##args m') + | exec_Ibuiltin: + forall s f sp pc rs m ef args res pc' t v m', + (fn_code f)!pc = Some(Ibuiltin ef args res pc') -> + external_call ef ge rs##args m t v m' -> + step (State s f sp pc rs m) + t (State s f sp pc' (rs#res <- v) m') | exec_Icond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> @@ -351,6 +361,7 @@ Definition successors_instr (i: instruction) : list node := | Istore chunk addr args src s => s :: nil | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil + | Ibuiltin ef args res s => s :: nil | Icond cond args ifso ifnot => ifso :: ifnot :: nil | Ijumptable arg tbl => tbl | Ireturn optarg => nil diff --git a/backend/RTLgen.v b/backend/RTLgen.v index ff4f81c5..aec2c867 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -546,6 +546,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do n1 <- add_instr (Itailcall sig (inl _ rf) rargs); do n2 <- transl_exprlist map cl rargs n1; transl_expr map b rf n2 + | Sbuiltin optid ef al => + do rargs <- alloc_regs map al; + do r <- new_reg; + do n1 <- store_optvar map r optid nd; + do n2 <- add_instr (Ibuiltin ef rargs r n1); + transl_exprlist map al rargs n2 | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index a96dfbfd..a1bd6618 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1213,6 +1213,22 @@ Proof. rewrite H2; eauto. traceEq. rewrite G. constructor; auto. + + (* builtin *) + inv TS. + exploit transl_exprlist_correct; eauto. + intros [rs' [E [F [G J]]]]. + exploit tr_store_optvar_correct. eauto. eauto. + apply match_env_update_temp. eexact F. eauto. + intros [rs'' [A B]]. + econstructor; split. + left. eapply star_plus_trans. eexact E. eapply plus_left. + eapply exec_Ibuiltin. eauto. rewrite G. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + eexact A. reflexivity. traceEq. + econstructor; eauto. constructor. rewrite Regmap.gss in B. auto. + (* seq *) inv TS. econstructor; split. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 5690bb29..0b18a99b 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -816,6 +816,12 @@ Inductive tr_stmt (c: code) (map: mapping): tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> c!n2 = Some (Itailcall sig (inl _ rf) rargs) -> tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret + | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 n2 rargs, + tr_exprlist c map nil al ns n1 rargs -> + c!n1 = Some (Ibuiltin ef rargs rd n2) -> + tr_store_optvar c map rd optid n2 nd -> + ~reg_in_map map rd -> + tr_stmt c map (Sbuiltin optid ef al) ns nd nexits ngoto nret rret | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n, tr_stmt c map s2 n nd nexits ngoto nret rret -> tr_stmt c map s1 ns n nexits ngoto nret rret -> @@ -1228,6 +1234,11 @@ Proof. eapply transl_expr_charact; eauto 3 with rtlg. apply tr_exprlist_incr with s4; auto. eapply transl_exprlist_charact; eauto 4 with rtlg. + (* Sbuiltin *) + econstructor; eauto 4 with rtlg. + eapply transl_exprlist_charact; eauto 3 with rtlg. + apply tr_store_optvar_incr with s2; auto. + eapply store_optvar_charact; eauto with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 68f38c0d..533c47a9 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -25,7 +25,7 @@ Require Import Integers. Require Import Events. Require Import Smallstep. Require Import RTL. -Require Conventions. +Require Import Conventions. (** * The type system *) @@ -104,8 +104,15 @@ Inductive wt_instr : instruction -> Prop := match ros with inl r => env r = Tint | inr s => True end -> sig.(sig_res) = funct.(fn_sig).(sig_res) -> List.map env args = sig.(sig_args) -> - Conventions.tailcall_possible sig -> + tailcall_possible sig -> wt_instr (Itailcall sig ros args) + | wt_Ibuiltin: + forall ef args res s, + List.map env args = (ef_sig ef).(sig_args) -> + env res = proj_sig_res (ef_sig ef) -> + arity_ok (ef_sig ef).(sig_args) = true -> + valid_successor s -> + wt_instr (Ibuiltin ef args res s) | wt_Icond: forall cond args s1 s2, List.map env args = type_of_condition cond -> @@ -225,7 +232,12 @@ Definition check_instr (i: instruction) : bool := match ros with inl r => check_reg r Tint | inr s => true end && check_regs args sig.(sig_args) && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res) - && Conventions.tailcall_is_possible sig + && tailcall_is_possible sig + | Ibuiltin ef args res s => + check_regs args (ef_sig ef).(sig_args) + && check_reg res (proj_sig_res (ef_sig ef)) + && arity_ok (ef_sig ef).(sig_args) + && check_successor s | Icond cond args s1 s2 => check_regs args (type_of_condition cond) && check_successor s1 @@ -331,7 +343,13 @@ Proof. destruct s0; auto. apply check_reg_correct; auto. eapply proj_sumbool_true; eauto. apply check_regs_correct; auto. - apply Conventions.tailcall_is_possible_correct; auto. + apply tailcall_is_possible_correct; auto. + (* builtin *) + constructor. + apply check_regs_correct; auto. + apply check_reg_correct; auto. + auto. + apply check_successor_correct; auto. (* cond *) constructor. apply check_regs_correct; auto. apply check_successor_correct; auto. @@ -541,6 +559,10 @@ Proof. econstructor; eauto. rewrite H6; auto. rewrite <- H7. apply wt_regset_list. auto. + (* Ibuiltin *) + econstructor; eauto. + apply wt_regset_assign. auto. + rewrite H6. eapply external_call_well_typed; eauto. (* Icond *) econstructor; eauto. econstructor; eauto. diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml index 868fb8df..657c4daa 100644 --- a/backend/RTLtypingaux.ml +++ b/backend/RTLtypingaux.ml @@ -86,6 +86,17 @@ let type_instr retty (Coq_pair(pc, i)) = raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s" name msg)) end + | Ibuiltin(ef, args, res, _) -> + begin try + let sg = ef_sig ef in + set_types args sg.sig_args; + set_type res (match sg.sig_res with None -> Tint | Some ty -> ty); + if not (Conventions.arity_ok sg.sig_args) then + raise(Type_error "wrong arity") + with Type_error msg -> + raise(Type_error (Printf.sprintf "type mismatch in Ibuiltin(%s): %s" + (extern_atom ef.ef_id) msg)) + end | Icond(cond, args, _, _) -> set_types args (type_of_condition cond) | Ijumptable(arg, _) -> diff --git a/backend/Reload.v b/backend/Reload.v index 5728a628..81b61998 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -235,6 +235,11 @@ Definition transf_instr parallel_move args largs (Ltailcall sig (inr _ id) :: k) end + | LTLin.Lbuiltin ef args dst => + let rargs := regs_for args in + let rdst := reg_for dst in + add_reloads args rargs + (Lbuiltin ef rargs rdst :: add_spill rdst dst k) | LTLin.Llabel lbl => Llabel lbl :: k | LTLin.Lgoto lbl => diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 155f7b1b..286a266d 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -25,6 +25,7 @@ Require Import Op. Require Import Locations. Require Import Conventions. Require Import Allocproof. +Require Import RTLtyping. Require Import LTLin. Require Import LTLintyping. Require Import Linear. @@ -33,33 +34,10 @@ Require Import Reload. (** * Exploitation of the typing hypothesis *) -(** Reloading is applied to LTLin code that is well-typed in - the sense of [LTLintyping]. We exploit this hypothesis to obtain information on - the number of temporaries required for reloading the arguments. *) - -Fixpoint temporaries_ok_rec (tys: list typ) (itmps ftmps: list mreg) - {struct tys} : bool := - match tys with - | nil => true - | Tint :: ts => - match itmps with - | nil => false - | it1 :: its => temporaries_ok_rec ts its ftmps - end - | Tfloat :: ts => - match ftmps with - | nil => false - | ft1 :: fts => temporaries_ok_rec ts itmps fts - end - end. - -Definition temporaries_ok (tys: list typ) := - temporaries_ok_rec tys int_temporaries float_temporaries. - -Remark temporaries_ok_rec_incr_1: +Remark arity_ok_rec_incr_1: forall tys it itmps ftmps, - temporaries_ok_rec tys itmps ftmps = true -> - temporaries_ok_rec tys (it :: itmps) ftmps = true. + arity_ok_rec tys itmps ftmps = true -> + arity_ok_rec tys (it :: itmps) ftmps = true. Proof. induction tys; intros until ftmps; simpl. tauto. @@ -68,10 +46,10 @@ Proof. destruct ftmps. congruence. auto. Qed. -Remark temporaries_ok_rec_incr_2: +Remark arity_ok_rec_incr_2: forall tys ft itmps ftmps, - temporaries_ok_rec tys itmps ftmps = true -> - temporaries_ok_rec tys itmps (ft :: ftmps) = true. + arity_ok_rec tys itmps ftmps = true -> + arity_ok_rec tys itmps (ft :: ftmps) = true. Proof. induction tys; intros until ftmps; simpl. tauto. @@ -80,37 +58,37 @@ Proof. destruct ftmps. congruence. auto. Qed. -Remark temporaries_ok_rec_decr: +Remark arity_ok_rec_decr: forall tys ty itmps ftmps, - temporaries_ok_rec (ty :: tys) itmps ftmps = true -> - temporaries_ok_rec tys itmps ftmps = true. + arity_ok_rec (ty :: tys) itmps ftmps = true -> + arity_ok_rec tys itmps ftmps = true. Proof. intros until ftmps. simpl. destruct ty. - destruct itmps. congruence. intros. apply temporaries_ok_rec_incr_1; auto. - destruct ftmps. congruence. intros. apply temporaries_ok_rec_incr_2; auto. + destruct itmps. congruence. intros. apply arity_ok_rec_incr_1; auto. + destruct ftmps. congruence. intros. apply arity_ok_rec_incr_2; auto. Qed. -Lemma temporaries_ok_enough_rec: +Lemma arity_ok_enough_rec: forall locs itmps ftmps, - temporaries_ok_rec (List.map Loc.type locs) itmps ftmps = true -> + arity_ok_rec (List.map Loc.type locs) itmps ftmps = true -> enough_temporaries_rec locs itmps ftmps = true. Proof. induction locs; intros until ftmps. simpl. auto. simpl enough_temporaries_rec. simpl map. - destruct a. intros. apply IHlocs. eapply temporaries_ok_rec_decr; eauto. + destruct a. intros. apply IHlocs. eapply arity_ok_rec_decr; eauto. simpl. destruct (slot_type s). destruct itmps; auto. destruct ftmps; auto. Qed. -Lemma temporaries_ok_enough: +Lemma arity_ok_enough: forall locs, - temporaries_ok (List.map Loc.type locs) = true -> + arity_ok (List.map Loc.type locs) = true -> enough_temporaries locs = true. Proof. - unfold temporaries_ok, enough_temporaries. intros. - apply temporaries_ok_enough_rec; auto. + unfold arity_ok, enough_temporaries. intros. + apply arity_ok_enough_rec; auto. Qed. Lemma enough_temporaries_op_args: @@ -118,7 +96,7 @@ Lemma enough_temporaries_op_args: (List.map Loc.type args, Loc.type res) = type_of_operation op -> enough_temporaries args = true. Proof. - intros. apply temporaries_ok_enough. + intros. apply arity_ok_enough. replace (map Loc.type args) with (fst (type_of_operation op)). destruct op; try (destruct c); compute; reflexivity. rewrite <- H. auto. @@ -129,7 +107,7 @@ Lemma enough_temporaries_cond: List.map Loc.type args = type_of_condition cond -> enough_temporaries args = true. Proof. - intros. apply temporaries_ok_enough. rewrite H. + intros. apply arity_ok_enough. rewrite H. destruct cond; compute; reflexivity. Qed. @@ -138,15 +116,15 @@ Lemma enough_temporaries_addr: List.map Loc.type args = type_of_addressing addr -> enough_temporaries args = true. Proof. - intros. apply temporaries_ok_enough. rewrite H. + intros. apply arity_ok_enough. rewrite H. destruct addr; compute; reflexivity. Qed. -Lemma temporaries_ok_rec_length: +Lemma arity_ok_rec_length: forall tys itmps ftmps, (length tys <= length itmps)%nat -> (length tys <= length ftmps)%nat -> - temporaries_ok_rec tys itmps ftmps = true. + arity_ok_rec tys itmps ftmps = true. Proof. induction tys; intros until ftmps; simpl. auto. @@ -159,8 +137,8 @@ Lemma enough_temporaries_length: forall args, (length args <= 2)%nat -> enough_temporaries args = true. Proof. - intros. apply temporaries_ok_enough. unfold temporaries_ok. - apply temporaries_ok_rec_length. + intros. apply arity_ok_enough. unfold arity_ok. + apply arity_ok_rec_length. rewrite list_length_map. simpl. omega. rewrite list_length_map. simpl. omega. Qed. @@ -690,7 +668,7 @@ Proof. intros. unfold return_regs. destruct (In_dec Loc.eq (R (loc_result sig)) temporaries). auto. destruct (In_dec Loc.eq (R (loc_result sig)) destroyed_at_call). auto. - elim n0. apply loc_result_caller_save. + generalize (loc_result_caller_save sig). tauto. Qed. (** * Preservation of labels and gotos *) @@ -885,7 +863,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop := | match_states_call: forall s f args m s' ls tm (STACKS: match_stackframes s s' (LTLin.funsig f)) - (AG: Val.lessdef_list args (map ls (Conventions.loc_arguments (LTLin.funsig f)))) + (AG: Val.lessdef_list args (map ls (loc_arguments (LTLin.funsig f)))) (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call -> ls l = parent_locset s' l) (WT: wt_fundef f) @@ -895,7 +873,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop := | match_states_return: forall s res m s' ls tm sig (STACKS: match_stackframes s s' sig) - (AG: Val.lessdef res (ls (R (Conventions.loc_result sig)))) + (AG: Val.lessdef res (ls (R (loc_result sig)))) (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call -> ls l = parent_locset s' l) (MMD: Mem.extends m tm), @@ -1216,6 +1194,29 @@ Proof. rewrite return_regs_arguments; auto. congruence. exact (return_regs_preserve (parent_locset s') ls3). + (* Lbuiltin *) + ExploitWT; inv WTI. + exploit add_reloads_correct. + instantiate (1 := args). apply arity_ok_enough. rewrite H3. auto. + apply locs_acceptable_disj_temporaries; auto. + intros [ls2 [A [B C]]]. + exploit external_call_mem_extends; eauto. + apply agree_locs; eauto. + intros [v' [tm' [P [Q [R S]]]]]. + exploit add_spill_correct. + intros [ls3 [D [E F]]]. + left; econstructor; split. + eapply star_plus_trans. eauto. + eapply plus_left. eapply exec_Lbuiltin. rewrite B. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + eauto. reflexivity. traceEq. + econstructor; eauto with coqlib. + apply agree_set with ls; auto. + rewrite E. rewrite Locmap.gss. auto. + intros. rewrite F; auto. rewrite Locmap.gso. auto. + apply reg_for_diff; auto. + (* Llabel *) left; econstructor; split. apply plus_one. apply exec_Llabel. @@ -1319,7 +1320,8 @@ Proof. econstructor; eauto. simpl. rewrite Locmap.gss. auto. intros. rewrite Locmap.gso. auto. - simpl. destruct l; auto. red; intro. elim H1. subst m0. apply loc_result_caller_save. + simpl. destruct l; auto. red; intro. elim H1. subst m0. + generalize (loc_result_caller_save (ef_sig ef)). tauto. (* return *) inv STACKS. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index df0715ee..1bb462dc 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -34,7 +34,7 @@ Require Import Reloadproof. given sufficient typing and well-formedness hypotheses over the locations involved. *) Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove - wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall + wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lbuiltin wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty. Remark wt_code_cons: @@ -291,6 +291,13 @@ Proof. destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. auto 10 with reloadty. + assert (map mreg_type (regs_for args) = map Loc.type args). + apply wt_regs_for. apply arity_ok_enough. congruence. + assert (mreg_type (reg_for res) = Loc.type res). eauto with reloadty. + auto with reloadty. + + + assert (map mreg_type (regs_for args) = map Loc.type args). eauto with reloadty. auto with reloadty. diff --git a/backend/Selection.v b/backend/Selection.v index e822fdf7..ebdad8a2 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -167,46 +167,73 @@ Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist := | a :: bl => Econs (sel_expr a) (sel_exprlist bl) end. +(** Recognition of calls to built-in functions that should be inlined *) + +Definition expr_is_addrof_ident (e: Cminor.expr) : option ident := + match e with + | Cminor.Econst (Cminor.Oaddrsymbol id ofs) => + if Int.eq ofs Int.zero then Some id else None + | _ => None + end. + +Definition expr_is_addrof_builtin (ge: Cminor.genv) (e: Cminor.expr) : option external_function := + match expr_is_addrof_ident e with + | None => None + | Some id => + match Genv.find_symbol ge id with + | None => None + | Some b => + match Genv.find_funct_ptr ge b with + | Some(External ef) => if ef.(ef_inline) then Some ef else None + | _ => None + end + end + end. + (** Conversion from Cminor statements to Cminorsel statements. *) -Fixpoint sel_stmt (s: Cminor.stmt) : stmt := +Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt := match s with | Cminor.Sskip => Sskip | Cminor.Sassign id e => Sassign id (sel_expr e) | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs) | Cminor.Scall optid sg fn args => - Scall optid sg (sel_expr fn) (sel_exprlist args) + match expr_is_addrof_builtin ge fn with + | None => Scall optid sg (sel_expr fn) (sel_exprlist args) + | Some ef => Sbuiltin optid ef (sel_exprlist args) + end | Cminor.Stailcall sg fn args => Stailcall sg (sel_expr fn) (sel_exprlist args) - | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2) + | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2) | Cminor.Sifthenelse e ifso ifnot => Sifthenelse (condexpr_of_expr (sel_expr e)) - (sel_stmt ifso) (sel_stmt ifnot) - | Cminor.Sloop body => Sloop (sel_stmt body) - | Cminor.Sblock body => Sblock (sel_stmt body) + (sel_stmt ge ifso) (sel_stmt ge ifnot) + | Cminor.Sloop body => Sloop (sel_stmt ge body) + | Cminor.Sblock body => Sblock (sel_stmt ge body) | Cminor.Sexit n => Sexit n | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl | Cminor.Sreturn None => Sreturn None | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e)) - | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body) + | Cminor.Slabel lbl body => Slabel lbl (sel_stmt ge body) | Cminor.Sgoto lbl => Sgoto lbl end. (** Conversion of functions and programs. *) -Definition sel_function (f: Cminor.function) : function := +Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : function := mkfunction f.(Cminor.fn_sig) f.(Cminor.fn_params) f.(Cminor.fn_vars) f.(Cminor.fn_stackspace) - (sel_stmt f.(Cminor.fn_body)). + (sel_stmt ge f.(Cminor.fn_body)). -Definition sel_fundef (f: Cminor.fundef) : fundef := - transf_fundef sel_function f. +Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : fundef := + transf_fundef (sel_function ge) f. Definition sel_program (p: Cminor.program) : program := - transform_program sel_fundef p. + let ge := Genv.globalenv p in + transform_program (sel_fundef ge) p. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index e03085a9..cb9f4fc5 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -275,6 +275,36 @@ Qed. End CMCONSTR. +(** Recognition of calls to built-in functions *) + +Lemma expr_is_addrof_ident_correct: + forall e id, + expr_is_addrof_ident e = Some id -> + e = Cminor.Econst (Cminor.Oaddrsymbol id Int.zero). +Proof. + intros e id. unfold expr_is_addrof_ident. + destruct e; try congruence. + destruct c; try congruence. + predSpec Int.eq Int.eq_spec i0 Int.zero; congruence. +Qed. + +Lemma expr_is_addrof_builtin_correct: + forall ge sp e m a v ef fd, + expr_is_addrof_builtin ge a = Some ef -> + Cminor.eval_expr ge sp e m a v -> + Genv.find_funct ge v = Some fd -> + fd = External ef. +Proof. + intros until fd; unfold expr_is_addrof_builtin. + case_eq (expr_is_addrof_ident a); intros; try congruence. + exploit expr_is_addrof_ident_correct; eauto. intro EQ; subst a. + inv H1. inv H4. + destruct (Genv.find_symbol ge i); try congruence. + inv H3. rewrite Genv.find_funct_find_funct_ptr in H2. rewrite H2 in H0. + destruct fd; try congruence. + destruct (ef_inline e0); congruence. +Qed. + (** * Semantic preservation for instruction selection. *) Section PRESERVATION. @@ -297,24 +327,24 @@ Qed. Lemma functions_translated: forall (v: val) (f: Cminor.fundef), Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (sel_fundef f). + Genv.find_funct tge v = Some (sel_fundef ge f). Proof. intros. - exact (Genv.find_funct_transf sel_fundef _ _ H). + exact (Genv.find_funct_transf (sel_fundef ge) _ _ H). Qed. Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (sel_fundef f). + Genv.find_funct_ptr tge b = Some (sel_fundef ge f). Proof. intros. - exact (Genv.find_funct_ptr_transf sel_fundef _ _ H). + exact (Genv.find_funct_ptr_transf (sel_fundef ge) _ _ H). Qed. Lemma sig_function_translated: forall f, - funsig (sel_fundef f) = Cminor.funsig f. + funsig (sel_fundef ge f) = Cminor.funsig f. Proof. intros. destruct f; reflexivity. Qed. @@ -369,29 +399,40 @@ Hint Resolve sel_exprlist_correct: evalexpr. Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont := match k with | Cminor.Kstop => Kstop - | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1) + | Cminor.Kseq s1 k1 => Kseq (sel_stmt ge s1) (sel_cont k1) | Cminor.Kblock k1 => Kblock (sel_cont k1) | Cminor.Kcall id f sp e k1 => - Kcall id (sel_function f) sp e (sel_cont k1) + Kcall id (sel_function ge f) sp e (sel_cont k1) end. Inductive match_states: Cminor.state -> CminorSel.state -> Prop := | match_state: forall f s k s' k' sp e m, - s' = sel_stmt s -> + s' = sel_stmt ge s -> k' = sel_cont k -> match_states (Cminor.State f s k sp e m) - (State (sel_function f) s' k' sp e m) + (State (sel_function ge f) s' k' sp e m) | match_callstate: forall f args k k' m, k' = sel_cont k -> match_states (Cminor.Callstate f args k m) - (Callstate (sel_fundef f) args k' m) + (Callstate (sel_fundef ge f) args k' m) | match_returnstate: forall v k k' m, k' = sel_cont k -> match_states (Cminor.Returnstate v k m) - (Returnstate v k' m). + (Returnstate v k' m) + | match_builtin_1: forall ef args optid f sp e k m al k', + k' = sel_cont k -> + eval_exprlist tge sp e m nil al args -> + match_states + (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) + (State (sel_function ge f) (Sbuiltin optid ef al) k' sp e m) + | match_builtin_2: forall v optid f sp e k m k', + k' = sel_cont k -> + match_states + (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m) + (State (sel_function ge f) Sskip k' sp (set_optvar optid v e) m). Remark call_cont_commut: forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k). @@ -401,19 +442,20 @@ Qed. Remark find_label_commut: forall lbl s k, - find_label lbl (sel_stmt s) (sel_cont k) = - option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk))) + find_label lbl (sel_stmt ge s) (sel_cont k) = + option_map (fun sk => (sel_stmt ge (fst sk), sel_cont (snd sk))) (Cminor.find_label lbl s k). Proof. induction s; intros; simpl; auto. unfold store. destruct (addressing m (sel_expr e)); auto. - change (Kseq (sel_stmt s2) (sel_cont k)) + destruct (expr_is_addrof_builtin ge e); auto. + change (Kseq (sel_stmt ge s2) (sel_cont k)) with (sel_cont (Cminor.Kseq s2 k)). rewrite IHs1. rewrite IHs2. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto. rewrite IHs1. rewrite IHs2. destruct (Cminor.find_label lbl s1 k); auto. - change (Kseq (Sloop (sel_stmt s)) (sel_cont k)) + change (Kseq (Sloop (sel_stmt ge s)) (sel_cont k)) with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)). auto. change (Kblock (sel_cont k)) @@ -423,64 +465,79 @@ Proof. destruct (ident_eq lbl l); auto. Qed. +Definition measure (s: Cminor.state) : nat := + match s with + | Cminor.Callstate _ _ _ _ => 0%nat + | Cminor.State _ _ _ _ _ _ => 1%nat + | Cminor.Returnstate _ _ _ => 2%nat + end. + Lemma sel_step_correct: forall S1 t S2, Cminor.step ge S1 t S2 -> forall T1, match_states S1 T1 -> - exists T2, step tge T1 t T2 /\ match_states S2 T2. + (exists T2, step tge T1 t T2 /\ match_states S2 T2) + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat. Proof. induction 1; intros T1 ME; inv ME; simpl; - try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail). + try (left; econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail). (* skip call *) - econstructor; split. + left; econstructor; split. econstructor. destruct k; simpl in H; simpl; auto. rewrite <- H0; reflexivity. simpl. eauto. constructor; auto. -(* - (* assign *) - exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split. - constructor. auto with evalexpr. - constructor; auto. -*) (* store *) - econstructor; split. + left; econstructor; split. eapply eval_store; eauto with evalexpr. constructor; auto. (* Scall *) - econstructor; split. + case_eq (expr_is_addrof_builtin ge a). + (* Scall turned into Sbuiltin *) + intros ef EQ. exploit expr_is_addrof_builtin_correct; eauto. intro EQ1. subst fd. + right; split. omega. split. auto. + econstructor; eauto with evalexpr. + (* Scall preserved *) + intro EQ. left; econstructor; split. econstructor; eauto with evalexpr. apply functions_translated; eauto. apply sig_function_translated. constructor; auto. (* Stailcall *) - econstructor; split. + left; econstructor; split. econstructor; eauto with evalexpr. apply functions_translated; eauto. apply sig_function_translated. constructor; auto. apply call_cont_commut. (* Sifthenelse *) - exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split. + left; exists (State (sel_function ge f) (if b then sel_stmt ge s1 else sel_stmt ge s2) (sel_cont k) sp e m); split. constructor. eapply eval_condition_of_expr; eauto with evalexpr. constructor; auto. destruct b; auto. (* Sreturn None *) - econstructor; split. + left; econstructor; split. econstructor. simpl; eauto. constructor; auto. apply call_cont_commut. (* Sreturn Some *) - econstructor; split. + left; econstructor; split. econstructor. simpl. eauto with evalexpr. simpl; eauto. constructor; auto. apply call_cont_commut. (* Sgoto *) - econstructor; split. + left; econstructor; split. econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut. rewrite H. simpl. reflexivity. constructor; auto. (* external call *) - econstructor; split. + left; econstructor; split. econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. constructor; auto. + (* external call turned into a Sbuiltin *) + left; econstructor; split. + econstructor. eauto. eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + constructor; auto. + (* return of an external call turned into a Sbuiltin *) + right; split. omega. split. auto. constructor; auto. Qed. Lemma sel_initial_states: @@ -509,10 +566,10 @@ Theorem transf_program_correct: Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. Proof. unfold CminorSel.exec_program, Cminor.exec_program; intros. - eapply simulation_step_preservation; eauto. + eapply simulation_opt_preservation; eauto. eexact sel_initial_states. eexact sel_final_states. - exact sel_step_correct. + eexact sel_step_correct. Qed. End PRESERVATION. diff --git a/backend/Stacking.v b/backend/Stacking.v index 5d9cf374..f289793e 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -179,6 +179,8 @@ Definition transl_instr | Ltailcall sig ros => restore_callee_save fe (Mtailcall sig ros :: k) + | Lbuiltin ef args dst => + Mbuiltin ef args dst :: k | Llabel lbl => Mlabel lbl :: k | Lgoto lbl => diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 4406187f..68d179a6 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -650,7 +650,7 @@ Qed. Lemma agree_callee_save_set_result: forall ls1 ls2 v sg, agree_callee_save ls1 ls2 -> - agree_callee_save (Locmap.set (R (Conventions.loc_result sg)) v ls1) ls2. + agree_callee_save (Locmap.set (R (loc_result sg)) v ls1) ls2. Proof. intros; red; intros. rewrite H; auto. symmetry; apply Locmap.gso. destruct l; simpl; auto. @@ -1501,7 +1501,17 @@ Proof. econstructor; eauto. intros; symmetry; eapply agree_return_regs; eauto. intros. inv WTI. generalize (H4 _ H0). tauto. - apply agree_callee_save_return_regs. + apply agree_callee_save_return_regs. + + (* Lbuiltin *) + exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) (rs0#res <- v) fr m'); split. + apply plus_one. apply exec_Mbuiltin. + change mreg with RegEq.t. + rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto with coqlib. + apply agree_set_reg; auto. (* Llabel *) econstructor; split. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index 8ba5caed..6ef86690 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -176,6 +176,9 @@ Proof. apply wt_restore_callee_save. apply wt_instrs_cons; auto. constructor; auto. destruct s0; auto. rewrite H5; auto. + (* builtin *) + apply wt_instrs_cons; auto. + constructor; auto. (* label *) apply wt_instrs_cons; auto. constructor. diff --git a/backend/Tailcall.v b/backend/Tailcall.v index 809a6a13..158002e8 100644 --- a/backend/Tailcall.v +++ b/backend/Tailcall.v @@ -19,7 +19,7 @@ Require Import Globalenvs. Require Import Registers. Require Import Op. Require Import RTL. -Require Conventions. +Require Import Conventions. (** An [Icall] instruction that stores its result in register [rreg] can be turned into a tail call if: @@ -88,7 +88,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) := match instr with | Icall sig ros args res s => if is_return niter f s res - && Conventions.tailcall_is_possible sig + && tailcall_is_possible sig && opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then Itailcall sig ros args else instr diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 2eed6e8d..11e6be20 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -24,7 +24,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Registers. Require Import RTL. -Require Conventions. +Require Import Conventions. Require Import Tailcall. (** * Syntactic properties of the code transformation *) @@ -168,7 +168,7 @@ Lemma transf_instr_charact: transf_instr_spec f instr (transf_instr f pc instr). Proof. intros. unfold transf_instr. destruct instr; try constructor. - caseEq (is_return niter f n r && Conventions.tailcall_is_possible s && + caseEq (is_return niter f n r && tailcall_is_possible s && opt_typ_eq (sig_res s) (sig_res (fn_sig f))); intros. destruct (andb_prop _ _ H0). destruct (andb_prop _ _ H1). eapply transf_instr_tailcall; eauto. @@ -497,6 +497,17 @@ Proof. rewrite stacksize_preserved; auto. constructor. auto. apply regset_get_list; auto. auto. +(* builtin *) + TransfInstr. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. + exploit external_call_mem_extends; eauto. + intros [v' [m'1 [A [B [C D]]]]]. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'1); split. + eapply exec_Ibuiltin; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. apply regset_set; auto. + (* cond true *) TransfInstr. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifso rs' m'); split. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 3ad8c4d0..6646f11f 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -104,6 +104,8 @@ Definition tunnel_instr (uf: U.t) (b: instruction) : instruction := Lcall sig ros args res (U.repr uf s) | Ltailcall sig ros args => Ltailcall sig ros args + | Lbuiltin ef args res s => + Lbuiltin ef args res (U.repr uf s) | Lcond cond args s1 s2 => Lcond cond args (U.repr uf s1) (U.repr uf s2) | Ljumptable arg tbl => diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 774ce853..9a14158f 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -308,6 +308,14 @@ Proof. rewrite sig_preserved. auto. apply find_function_translated; auto. econstructor; eauto. + (* Lbuiltin *) + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. + left; econstructor; split. + eapply exec_Lbuiltin; eauto. + rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. (* cond *) generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. -- cgit