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. --- cfrontend/Cminorgenproof.v | 174 ++++++++++++++++++++++++--------------------- 1 file changed, 92 insertions(+), 82 deletions(-) (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 2f551d68..ea1bc89c 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -76,7 +76,7 @@ Lemma sig_preserved: Proof. intros until tf; destruct f; simpl. unfold transl_function. destruct (build_compilenv f). - case (zle z Int.max_unsigned); simpl bind; try congruence. + case (zle z Ptrofs.max_unsigned); simpl bind; try congruence. intros. monadInv H. simpl. eapply sig_preserved_body; eauto. intro. inv H. reflexivity. Qed. @@ -190,7 +190,7 @@ Qed. Inductive match_var (f: meminj) (sp: block): option (block * Z) -> option Z -> Prop := | match_var_local: forall b sz ofs, - Val.inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> + Val.inject f (Vptr b Ptrofs.zero) (Vptr sp (Ptrofs.repr ofs)) -> match_var f sp (Some(b, sz)) (Some ofs) | match_var_global: match_var f sp None None. @@ -311,7 +311,7 @@ Proof. intros. rewrite PTree.gsspec. destruct (peq id0 id). (* the new var *) subst id0. rewrite CENV. constructor. econstructor. eauto. - rewrite Int.add_commut; rewrite Int.add_zero; auto. + rewrite Ptrofs.add_commut; rewrite Ptrofs.add_zero; auto. (* old vars *) generalize (me_vars0 id0). rewrite PTree.gro; auto. intros M; inv M. constructor; eauto. @@ -794,7 +794,7 @@ Definition cenv_mem_separated (cenv: compilenv) (vars: list (ident * Z)) (f: mem Lemma match_callstack_alloc_variables_rec: forall tm sp tf cenv le te lo cs, Mem.valid_block tm sp -> - fn_stackspace tf <= Int.max_unsigned -> + fn_stackspace tf <= Ptrofs.max_unsigned -> (forall ofs k p, Mem.perm tm sp ofs k p -> 0 <= ofs < fn_stackspace tf) -> (forall ofs k p, 0 <= ofs < fn_stackspace tf -> Mem.perm tm sp ofs k p) -> forall e1 m1 vars e2 m2, @@ -854,7 +854,7 @@ Qed. Lemma match_callstack_alloc_variables: forall tm1 sp tm2 m1 vars e m2 cenv f1 cs fn le te, Mem.alloc tm1 0 (fn_stackspace fn) = (tm2, sp) -> - fn_stackspace fn <= Int.max_unsigned -> + fn_stackspace fn <= Ptrofs.max_unsigned -> alloc_variables empty_env m1 vars e m2 -> list_norepet (map fst vars) -> cenv_compat cenv vars (fn_stackspace fn) -> @@ -1225,7 +1225,7 @@ Qed. Theorem match_callstack_function_entry: forall fn cenv tf m e m' tm tm' sp f cs args targs le, build_compilenv fn = (cenv, tf.(fn_stackspace)) -> - tf.(fn_stackspace) <= Int.max_unsigned -> + tf.(fn_stackspace) <= Ptrofs.max_unsigned -> list_norepet (map fst (Csharpminor.fn_vars fn)) -> list_norepet (Csharpminor.fn_params fn) -> list_disjoint (Csharpminor.fn_params fn) (Csharpminor.fn_temps fn) -> @@ -1334,82 +1334,91 @@ Lemma eval_binop_compat: eval_binop op tv1 tv2 tm = Some tv /\ Val.inject f v tv. Proof. - destruct op; simpl; intros. - inv H; inv H0; inv H1; TrivialExists. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - inv H; inv H0; inv H1; TrivialExists. - apply Int.sub_add_l. - simpl. destruct (eq_block b1 b0); auto. - subst b1. rewrite H in H0; inv H0. - rewrite dec_eq_true. rewrite Int.sub_shifted. auto. - inv H; inv H0; inv H1; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct op; simpl; intros; inv H. +- TrivialExists. apply Val.add_inject; auto. +- TrivialExists. apply Val.sub_inject; auto. +- TrivialExists. inv H0; inv H1; constructor. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. destruct (Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. - destruct (Int.eq i0 Int.zero); inv H. TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. + || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H4; TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int.eq i0 Int.zero); inv H4. TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. destruct (Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. - destruct (Int.eq i0 Int.zero); inv H. TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. + || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H4; TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int.eq i0 Int.zero); inv H4. TrivialExists. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int.iwordsize); constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int.iwordsize); constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int.iwordsize); constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists. apply Val.addl_inject; auto. +- TrivialExists. apply Val.subl_inject; auto. +- TrivialExists. inv H0; inv H1; constructor. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. destruct (Int64.eq i0 Int64.zero - || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. - destruct (Int64.eq i0 Int64.zero); inv H. TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H4; TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int64.eq i0 Int64.zero); inv H4. TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. destruct (Int64.eq i0 Int64.zero - || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists. - inv H0; try discriminate; inv H1; try discriminate. simpl in *. - destruct (Int64.eq i0 Int64.zero); inv H. TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. -(* cmpu *) - inv H. econstructor; split; eauto. - unfold Val.cmpu. + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H4; TrivialExists. +- inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int64.eq i0 Int64.zero); inv H4. TrivialExists. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int64.iwordsize'); constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int64.iwordsize'); constructor. +- TrivialExists; inv H0; inv H1; simpl; auto. + destruct (Int.ltu i0 Int64.iwordsize'); constructor. +- (* cmp *) + TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool. +- (* cmpu *) + TrivialExists. unfold Val.cmpu. destruct (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E. replace (Val.cmpu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b). - destruct b; simpl; constructor. + apply val_inject_val_of_optbool. symmetry. eapply Val.cmpu_bool_inject; eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. simpl; auto. -(* cmpf *) - inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. -(* cmpfs *) - inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. -(* cmpl *) - unfold Val.cmpl in *. inv H0; inv H1; simpl in H; inv H. +- (* cmpf *) + TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool. +- (* cmpfs *) + TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool. +- (* cmpl *) + unfold Val.cmpl in *. inv H0; inv H1; simpl in H4; inv H4. econstructor; split. simpl; eauto. apply val_inject_val_of_bool. -(* cmplu *) - unfold Val.cmplu in *. inv H0; inv H1; simpl in H; inv H. +- (* cmplu *) + unfold Val.cmplu in *. + destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E. + simpl in H4; inv H4. + replace (Val.cmplu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b). econstructor; split. simpl; eauto. apply val_inject_val_of_bool. + symmetry. eapply Val.cmplu_bool_inject; eauto. + intros; eapply Mem.valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. + intros; eapply Mem.different_pointers_inject; eauto. + discriminate. Qed. (** * Correctness of Cminor construction functions *) @@ -1421,21 +1430,22 @@ Lemma var_addr_correct: match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) -> eval_var_addr ge e id b -> exists tv, - eval_expr tge (Vptr sp Int.zero) te tm (var_addr cenv id) tv - /\ Val.inject f (Vptr b Int.zero) tv. + eval_expr tge (Vptr sp Ptrofs.zero) te tm (var_addr cenv id) tv + /\ Val.inject f (Vptr b Ptrofs.zero) tv. Proof. unfold var_addr; intros. assert (match_var f sp e!id cenv!id). inv H. inv MENV. auto. inv H1; inv H0; try congruence. (* local *) - exists (Vptr sp (Int.repr ofs)); split. - constructor. simpl. rewrite Int.add_zero_l; auto. + exists (Vptr sp (Ptrofs.repr ofs)); split. + constructor. simpl. rewrite Ptrofs.add_zero_l; auto. congruence. (* global *) exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG. - exists (Vptr b Int.zero); split. - constructor. simpl. rewrite symbols_preserved. rewrite H2. auto. + exists (Vptr b Ptrofs.zero); split. + constructor. simpl. unfold Genv.symbol_address. + rewrite symbols_preserved. rewrite H2. auto. econstructor; eauto. Qed. @@ -1497,7 +1507,7 @@ Lemma transl_expr_correct: forall ta (TR: transl_expr cenv a = OK ta), exists tv, - eval_expr tge (Vptr sp Int.zero) te tm ta tv + eval_expr tge (Vptr sp Ptrofs.zero) te tm ta tv /\ Val.inject f v tv. Proof. induction 3; intros; simpl in TR; try (monadInv TR). @@ -1535,7 +1545,7 @@ Lemma transl_exprlist_correct: forall ta (TR: transl_exprlist cenv a = OK ta), exists tv, - eval_exprlist tge (Vptr sp Int.zero) te tm ta tv + eval_exprlist tge (Vptr sp Ptrofs.zero) te tm ta tv /\ Val.inject_list f v tv. Proof. induction 3; intros; monadInv TR. @@ -1569,7 +1579,7 @@ Inductive match_cont: Csharpminor.cont -> Cminor.cont -> compilenv -> exit_env - transl_funbody cenv sz fn = OK tfn -> match_cont k tk cenv xenv cs -> match_cont (Csharpminor.Kcall optid fn e le k) - (Kcall optid tfn (Vptr sp Int.zero) te tk) + (Kcall optid tfn (Vptr sp Ptrofs.zero) te tk) cenv' nil (Frame cenv tfn e le te sp lo hi :: cs). @@ -1584,7 +1594,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := (Mem.nextblock m) (Mem.nextblock tm)) (MK: match_cont k tk cenv xenv cs), match_states (Csharpminor.State fn s k e le m) - (State tfn ts tk (Vptr sp Int.zero) te tm) + (State tfn ts tk (Vptr sp Ptrofs.zero) te tm) | match_state_seq: forall fn s1 s2 k e le m tfn ts1 tk sp te tm cenv xenv f lo hi cs sz (TRF: transl_funbody cenv sz fn = OK tfn) @@ -1595,7 +1605,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := (Mem.nextblock m) (Mem.nextblock tm)) (MK: match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs), match_states (Csharpminor.State fn (Csharpminor.Sseq s1 s2) k e le m) - (State tfn ts1 tk (Vptr sp Int.zero) te tm) + (State tfn ts1 tk (Vptr sp Ptrofs.zero) te tm) | match_callstate: forall fd args k m tfd targs tk tm f cs cenv (TR: transl_fundef fd = OK tfd) @@ -1789,7 +1799,7 @@ Lemma switch_match_states: (MK: match_cont k tk cenv xenv cs) (TK: transl_lblstmt_cont cenv xenv ls tk tk'), exists S, - plus step tge (State tfn (Sexit O) tk' (Vptr sp Int.zero) te tm) E0 S + plus step tge (State tfn (Sexit O) tk' (Vptr sp Ptrofs.zero) te tm) E0 S /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e le m) S. Proof. intros. inv TK. @@ -2050,7 +2060,7 @@ Opaque PTree.set. (* ifthenelse *) monadInv TR. exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. - left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Int.zero) te tm); split. + left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Ptrofs.zero) te tm); split. apply plus_one. eapply step_ifthenelse; eauto. eapply bool_of_val_inject; eauto. econstructor; eauto. destruct b; auto. @@ -2152,7 +2162,7 @@ Opaque PTree.set. (* internal call *) monadInv TR. generalize EQ; clear EQ; unfold transl_function. caseEq (build_compilenv f). intros ce sz BC. - destruct (zle sz Int.max_unsigned); try congruence. + destruct (zle sz Ptrofs.max_unsigned); try congruence. intro TRBODY. generalize TRBODY; intro TMP. monadInv TMP. set (tf := mkfunction (Csharpminor.fn_sig f) -- cgit