From e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:25:18 +0200 Subject: Support for 64-bit architectures: generic support - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly. --- backend/Selectionproof.v | 157 +++++++++++++++++------------------------------ 1 file changed, 57 insertions(+), 100 deletions(-) (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index a57e5ea6..34157553 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -12,28 +12,11 @@ (** Correctness of instruction selection *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Linking. -Require Import Errors. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Switch. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. -Require Import SelectOp. -Require Import SelectDiv. -Require Import SelectLong. -Require Import Selection. -Require Import SelectOpproof. -Require Import SelectDivproof. -Require Import SelectLongproof. +Require Import Coqlib Maps. +Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep. +Require Import Switch Cminor Op CminorSel. +Require Import SelectOp SelectDiv SplitLong SelectLong Selection. +Require Import SelectOpproof SelectDivproof SplitLongproof SelectLongproof. Local Open Scope cminorsel_scope. Local Open Scope error_monad_scope. @@ -252,8 +235,7 @@ Lemma eval_sel_unop: forall le op a1 v1 v, eval_expr tge sp e m le a1 v1 -> eval_unop op v1 = Some v -> - - exists v', eval_expr tge sp e m le (sel_unop hf op a1) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_cast8unsigned; auto. @@ -296,7 +278,7 @@ Lemma eval_sel_binop: eval_expr tge sp e m le a1 v1 -> eval_expr tge sp e m le a2 v2 -> eval_binop op v1 v2 m = Some v -> - exists v', eval_expr tge sp e m le (sel_binop hf op a1 a2) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_add; auto. @@ -348,12 +330,12 @@ End CMCONSTR. Lemma expr_is_addrof_ident_correct: forall e id, expr_is_addrof_ident e = Some id -> - e = Cminor.Econst (Cminor.Oaddrsymbol id Int.zero). + e = Cminor.Econst (Cminor.Oaddrsymbol id Ptrofs.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. + predSpec Ptrofs.eq Ptrofs.eq_spec i0 Ptrofs.zero; congruence. Qed. Lemma classify_call_correct: @@ -363,17 +345,17 @@ Lemma classify_call_correct: Genv.find_funct ge v = Some fd -> match classify_call (prog_defmap unit) a with | Call_default => True - | Call_imm id => exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b Int.zero + | Call_imm id => exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b Ptrofs.zero | Call_builtin ef => fd = External ef end. Proof. unfold classify_call; intros. destruct (expr_is_addrof_ident a) as [id|] eqn:EA; auto. exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a. - inv H0. inv H3. + inv H0. inv H3. unfold Genv.symbol_address in *. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. rewrite Genv.find_funct_find_funct_ptr in H1. - assert (DFL: exists b1, Genv.find_symbol ge id = Some b1 /\ Vptr b Int.zero = Vptr b1 Int.zero) by (exists b; auto). + assert (DFL: exists b1, Genv.find_symbol ge id = Some b1 /\ Vptr b Ptrofs.zero = Vptr b1 Ptrofs.zero) by (exists b; auto). unfold globdef; destruct (prog_defmap unit)!id as [[[f|ef] |gv] |] eqn:G; auto. destruct (ef_inline ef) eqn:INLINE; auto. destruct (prog_defmap_linkorder _ _ _ _ H G) as (gd & P & Q). @@ -530,12 +512,12 @@ Proof. rewrite Int64.unsigned_repr. destruct (zeq (Int64.unsigned n0) n); auto. unfold Int64.max_unsigned; omega. - intros until n; intros EVAL R RANGE. - eapply eval_cmplu. eexact EVAL. apply eval_longconst with (n := Int64.repr n). + eapply eval_cmplu; auto. eexact EVAL. apply eval_longconst with (n := Int64.repr n). inv R. unfold Val.cmplu. simpl. f_equal; f_equal. unfold Int64.ltu. rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. unfold Int64.max_unsigned; omega. - intros until n; intros EVAL R RANGE. - exploit eval_subl. eexact EVAL. apply eval_longconst with (n := Int64.repr n). + exploit eval_subl; auto. eexact EVAL. apply eval_longconst with (n := Int64.repr n). intros (vb & A & B). inv R. simpl in B. inv B. econstructor; split; eauto. replace ((Int64.unsigned n0 - n) mod Int64.modulus) @@ -579,13 +561,25 @@ Lemma eval_binop_lessdef: Proof. intros until m'; intros EV LD1 LD2 ME. assert (exists v', eval_binop op v1' v2' m = Some v' /\ Val.lessdef v v'). - inv LD1. inv LD2. exists v; auto. - destruct op; destruct v1'; simpl in *; inv EV; TrivialExists. - destruct op; simpl in *; inv EV; TrivialExists. - destruct op; try (exact H). - simpl in *. TrivialExists. inv EV. apply Val.of_optbool_lessdef. - intros. apply Val.cmpu_bool_lessdef with (Mem.valid_pointer m) v1 v2; auto. - intros; eapply Mem.valid_pointer_extends; eauto. + { inv LD1. inv LD2. exists v; auto. + destruct op; destruct v1'; simpl in *; inv EV; TrivialExists. + destruct op; simpl in *; inv EV; TrivialExists. } + assert (CMPU: forall c, + eval_binop (Ocmpu c) v1 v2 m = Some v -> + exists v' : val, eval_binop (Ocmpu c) v1' v2' m' = Some v' /\ Val.lessdef v v'). + { intros c A. simpl in *. inv A. econstructor; split. eauto. + apply Val.of_optbool_lessdef. + intros. apply Val.cmpu_bool_lessdef with (Mem.valid_pointer m) v1 v2; auto. + intros; eapply Mem.valid_pointer_extends; eauto. } + assert (CMPLU: forall c, + eval_binop (Ocmplu c) v1 v2 m = Some v -> + exists v' : val, eval_binop (Ocmplu c) v1' v2' m' = Some v' /\ Val.lessdef v v'). + { intros c A. simpl in *. unfold Val.cmplu in *. + destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:C; simpl in A; inv A. + eapply Val.cmplu_bool_lessdef with (valid_ptr' := (Mem.valid_pointer m')) in C; + eauto using Mem.valid_pointer_extends. + rewrite C. exists (Val.of_bool b); auto. } + destruct op; auto. Qed. (** * Semantic preservation for instruction selection. *) @@ -644,7 +638,7 @@ Lemma sel_expr_correct: Cminor.eval_expr ge sp e m a v -> forall e' le m', env_lessdef e e' -> Mem.extends m m' -> - exists v', eval_expr tge sp e' m' le (sel_expr hf a) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'. Proof. induction 1; intros; simpl. (* Evar *) @@ -654,10 +648,8 @@ Proof. exists (Vint i); split; auto. econstructor. constructor. auto. exists (Vfloat f); split; auto. econstructor. constructor. auto. exists (Vsingle f); split; auto. econstructor. constructor. auto. - exists (Val.longofwords (Vint (Int64.hiword i)) (Vint (Int64.loword i))); split. - eapply eval_Eop. constructor. EvalOp. simpl; eauto. constructor. EvalOp. simpl; eauto. constructor. auto. - simpl. rewrite Int64.ofwords_recompose. auto. - rewrite <- symbols_preserved. fold (Genv.symbol_address tge i i0). apply eval_addrsymbol. + exists (Vlong i); split; auto. apply eval_longconst. + unfold Genv.symbol_address; rewrite <- symbols_preserved; fold (Genv.symbol_address tge i i0). apply eval_addrsymbol. apply eval_addrstack. (* Eunop *) exploit IHeval_expr; eauto. intros [v1' [A B]]. @@ -668,7 +660,9 @@ Proof. exploit IHeval_expr1; eauto. intros [v1' [A B]]. exploit IHeval_expr2; eauto. intros [v2' [C D]]. exploit eval_binop_lessdef; eauto. intros [v' [E F]]. - exploit eval_sel_binop. eexact LINK. eexact HF. eexact A. eexact C. eauto. intros [v'' [P Q]]. + assert (G: exists v'', eval_expr tge sp e' m' le (sel_binop op (sel_expr a1) (sel_expr a2)) v'' /\ Val.lessdef v' v'') + by (eapply eval_sel_binop; eauto). + destruct G as [v'' [P Q]]. exists v''; split; eauto. eapply Val.lessdef_trans; eauto. (* Eload *) exploit IHeval_expr; eauto. intros [vaddr' [A B]]. @@ -681,7 +675,7 @@ Lemma sel_exprlist_correct: Cminor.eval_exprlist ge sp e m a v -> forall e' le m', env_lessdef e e' -> Mem.extends m m' -> - exists v', eval_exprlist tge sp e' m' le (sel_exprlist hf a) v' /\ Val.lessdef_list v v'. + exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'. Proof. induction 1; intros; simpl. exists (@nil val); split; auto. constructor. @@ -695,13 +689,13 @@ Lemma sel_builtin_arg_correct: env_lessdef e e' -> Mem.extends m m' -> Cminor.eval_expr ge sp e m a v -> exists v', - CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg hf a c) v' + CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg a c) v' /\ Val.lessdef v v'. Proof. intros. unfold sel_builtin_arg. exploit sel_expr_correct; eauto. intros (v1 & A & B). exists v1; split; auto. - destruct (builtin_arg_ok (builtin_arg (sel_expr hf a)) c). + destruct (builtin_arg_ok (builtin_arg (sel_expr a)) c). apply eval_builtin_arg; eauto. constructor; auto. Qed. @@ -714,7 +708,7 @@ Lemma sel_builtin_args_correct: forall cl, exists vl', list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') - (sel_builtin_args hf al cl) + (sel_builtin_args al cl) vl' /\ Val.lessdef_list vl vl'. Proof. @@ -737,37 +731,11 @@ End EXPRESSIONS. (** Semantic preservation for functions and statements. *) -(* -Inductive match_call_cont: Cminor.cont -> CminorSel.cont -> Prop := - | match_call_cont_stop: - match_call_cont Cminor.Kstop Kstop - | match_call_cont_call: forall cunit hf id f sp e k f' e' k', - linkorder cunit prog -> - helper_functions_declared cunit hf -> - sel_function (prog_defmap cunit) hf f = OK f' -> - match_cont cunit hf k k' -> env_lessdef e e' -> - match_call_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k') - -with match_cont: Cminor.program -> helper_functions -> Cminor.cont -> CminorSel.cont -> Prop := - | match_cont_stop: forall cunit hf, - match_cont cunit hf Cminor.Kstop Kstop - | match_cont_seq: forall cunit hf s s' k k', - sel_stmt (prog_defmap cunit) hf s = OK s' -> - match_cont cunit hf k k' -> - match_cont cunit hf (Cminor.Kseq s k) (Kseq s' k') - | match_cont_block: forall cunit hf k k', - match_cont cunit hf k k' -> - match_cont cunit hf (Cminor.Kblock k) (Kblock k') - | match_cont_call: forall cunit hf id f sp e k f' e' k', - match_call_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k') -> - match_cont cunit hf (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k'). -*) - Inductive match_cont: Cminor.program -> helper_functions -> Cminor.cont -> CminorSel.cont -> Prop := | match_cont_stop: forall cunit hf, match_cont cunit hf Cminor.Kstop Kstop | match_cont_seq: forall cunit hf s s' k k', - sel_stmt (prog_defmap cunit) hf s = OK s' -> + sel_stmt (prog_defmap cunit) s = OK s' -> match_cont cunit hf k k' -> match_cont cunit hf (Cminor.Kseq s k) (Kseq s' k') | match_cont_block: forall cunit hf k k', @@ -788,7 +756,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (LINK: linkorder cunit prog) (HF: helper_functions_declared cunit hf) (TF: sel_function (prog_defmap cunit) hf f = OK f') - (TS: sel_stmt (prog_defmap cunit) hf s = OK s') + (TS: sel_stmt (prog_defmap cunit) s = OK s') (MC: match_cont cunit hf k k') (LD: env_lessdef e e') (ME: Mem.extends m m'), @@ -835,31 +803,20 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m) (State f' Sskip k' sp (set_builtin_res (sel_builtin_res optid) v' e') m'). -(* -Remark call_cont_commut_1: - forall cunit hf k k', match_cont cunit hf k k' -> - forall cunit' hf', match_cont cunit' hf' (Cminor.call_cont k) (call_cont k'). -Proof. - induction 1; simpl; auto; intros; econstructor; eauto. -Qed. - -Remark call_cont_commut_2: - forall cunit hf k k', match_cont cunit hf k k' -> match_cont cunit hf (Cminor.call_cont k) (call_cont k'). -Proof. - intros. eapply call_cont_commut_1; eauto. -Qed. -*) - Remark call_cont_commut: forall cunit hf k k', match_cont cunit hf k k' -> match_call_cont (Cminor.call_cont k) (call_cont k'). Proof. - induction 1; simpl; auto; red; intros; econstructor; eauto. + induction 1; simpl; auto; red; intros. +- constructor. +- eapply match_cont_call with (hf := hf); eauto. Qed. Remark match_is_call_cont: forall cunit hf k k', match_cont cunit hf k k' -> Cminor.is_call_cont k -> match_call_cont k k'. Proof. - destruct 1; intros; try contradiction; red; intros; econstructor; eauto. + destruct 1; intros; try contradiction; red; intros. +- constructor. +- eapply match_cont_call with (hf := hf); eauto. Qed. Remark match_call_cont_cont: @@ -875,16 +832,16 @@ Qed. Remark find_label_commut: forall cunit hf lbl s k s' k', match_cont cunit hf k k' -> - sel_stmt (prog_defmap cunit) hf s = OK s' -> + sel_stmt (prog_defmap cunit) s = OK s' -> match Cminor.find_label lbl s k, find_label lbl s' k' with | None, None => True - | Some(s1, k1), Some(s1', k1') => sel_stmt (prog_defmap cunit) hf s1 = OK s1' /\ match_cont cunit hf k1 k1' + | Some(s1, k1), Some(s1', k1') => sel_stmt (prog_defmap cunit) s1 = OK s1' /\ match_cont cunit hf k1 k1' | _, _ => False end. Proof. induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto. (* store *) - unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto. + unfold store. destruct (addressing m (sel_expr e)); simpl; auto. (* call *) destruct (classify_call (prog_defmap cunit) e); simpl; auto. (* tailcall *) @@ -963,7 +920,7 @@ Proof. econstructor; eauto. econstructor; eauto. eapply sig_function_translated; eauto. eapply match_callstate with (cunit := cunit'); eauto. - red; intros. eapply match_cont_call with (cunit := cunit); eauto. + red; intros. eapply match_cont_call with (cunit := cunit) (hf := hf); eauto. + (* direct *) intros [b [U V]]. exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. @@ -973,7 +930,7 @@ Proof. subst vf. econstructor; eauto. rewrite symbols_preserved; eauto. eapply sig_function_translated; eauto. eapply match_callstate with (cunit := cunit'); eauto. - red; intros; eapply match_cont_call with (cunit := cunit); eauto. + red; intros; eapply match_cont_call with (cunit := cunit) (hf := hf); eauto. + (* turned into Sbuiltin *) intros EQ. subst fd. exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]]. @@ -1052,7 +1009,7 @@ Proof. - (* Slabel *) left; econstructor; split. constructor. econstructor; eauto. - (* Sgoto *) - assert (sel_stmt (prog_defmap cunit) hf (Cminor.fn_body f) = OK (fn_body f')). + assert (sel_stmt (prog_defmap cunit) (Cminor.fn_body f) = OK (fn_body f')). { monadInv TF; simpl; auto. } exploit (find_label_commut cunit hf lbl (Cminor.fn_body f) (Cminor.call_cont k)). eapply call_cont_commut; eauto. eauto. -- cgit