From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Machtyping.v | 245 +-------------------------------------------------- 1 file changed, 2 insertions(+), 243 deletions(-) (limited to 'backend/Machtyping.v') diff --git a/backend/Machtyping.v b/backend/Machtyping.v index 93ac00cd..95ceafe6 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -87,7 +87,7 @@ Inductive wt_instr : instruction -> Prop := | wt_Mjumptable: forall arg tbl, mreg_type arg = Tint -> - list_length_z tbl * 4 <= Int.max_signed -> + list_length_z tbl * 4 <= Int.max_unsigned -> wt_instr (Mjumptable arg tbl) | wt_Mreturn: wt_instr Mreturn. @@ -96,24 +96,7 @@ Record wt_function (f: function) : Prop := mk_wt_function { wt_function_instrs: forall instr, In instr f.(fn_code) -> wt_instr instr; wt_function_stacksize: - f.(fn_stacksize) >= 0; - wt_function_framesize: - 0 <= f.(fn_framesize) <= -Int.min_signed; - wt_function_framesize_aligned: - (4 | f.(fn_framesize)); - wt_function_link: - 0 <= Int.signed f.(fn_link_ofs) - /\ Int.signed f.(fn_link_ofs) + 4 <= f.(fn_framesize); - wt_function_link_aligned: - (4 | Int.signed f.(fn_link_ofs)); - wt_function_retaddr: - 0 <= Int.signed f.(fn_retaddr_ofs) - /\ Int.signed f.(fn_retaddr_ofs) + 4 <= f.(fn_framesize); - wt_function_retaddr_aligned: - (4 | Int.signed f.(fn_retaddr_ofs)); - wt_function_link_retaddr: - Int.signed f.(fn_retaddr_ofs) + 4 <= Int.signed f.(fn_link_ofs) - \/ Int.signed f.(fn_link_ofs) + 4 <= Int.signed f.(fn_retaddr_ofs) + 0 <= f.(fn_stacksize) <= Int.max_unsigned }. Inductive wt_fundef: fundef -> Prop := @@ -125,227 +108,3 @@ Inductive wt_fundef: fundef -> Prop := Definition wt_program (p: program) : Prop := forall i f, In (i, f) (prog_funct p) -> wt_fundef f. - -(** * Type soundness *) - -Require Import Machabstr. - -(** We show a weak type soundness result for the abstract semantics - of Mach: for a well-typed Mach program, if a transition is taken - from a state where registers hold values of their static types, - registers in the final state hold values of their static types - as well. This is a subject reduction theorem for our type system. - It is used in the proof of implication from the abstract Mach - semantics to the concrete Mach semantics (file [Machabstr2concr]). -*) - -Definition wt_regset (rs: regset) : Prop := - forall r, Val.has_type (rs r) (mreg_type r). - -Definition wt_frame (fr: frame) : Prop := - forall ty ofs, Val.has_type (fr ty ofs) ty. - -Lemma wt_setreg: - forall (rs: regset) (r: mreg) (v: val), - Val.has_type v (mreg_type r) -> - wt_regset rs -> wt_regset (rs#r <- v). -Proof. - intros; red; intros. unfold Regmap.set. - case (RegEq.eq r0 r); intro. - subst r0; assumption. - apply H0. -Qed. - -Lemma wt_undef_temps: - forall rs, wt_regset rs -> wt_regset (undef_temps rs). -Proof. - unfold undef_temps. - generalize (int_temporaries ++ float_temporaries). - induction l; simpl; intros. auto. - apply IHl. red; intros. unfold Regmap.set. - destruct (RegEq.eq r a). constructor. auto. -Qed. - -Lemma wt_undef_op: - forall op rs, wt_regset rs -> wt_regset (undef_op op rs). -Proof. - intros. set (W := wt_undef_temps rs H). - destruct op; simpl; auto. -Qed. - -Lemma wt_undef_getparam: - forall rs, wt_regset rs -> wt_regset (rs#IT1 <- Vundef). -Proof. - intros; red; intros. unfold Regmap.set. - destruct (RegEq.eq r IT1). constructor. auto. -Qed. - -Lemma wt_get_slot: - forall f fr ty ofs v, - get_slot f fr ty ofs v -> - wt_frame fr -> - Val.has_type v ty. -Proof. - induction 1; intros. - subst v. apply H1. -Qed. - -Lemma wt_set_slot: - forall f fr ty ofs v fr', - set_slot f fr ty ofs v fr' -> - wt_frame fr -> - Val.has_type v ty -> - wt_frame fr'. -Proof. - intros. induction H. subst fr'; red; intros. unfold update. - destruct (zeq (ofs - f.(fn_framesize)) ofs0). - destruct (typ_eq ty ty0). congruence. exact I. - destruct (zle (ofs0 + AST.typesize ty0) (ofs - f.(fn_framesize))). - apply H0. - destruct (zle (ofs - f.(fn_framesize) + AST.typesize ty) ofs0). - apply H0. - exact I. -Qed. - -Lemma wt_empty_frame: - wt_frame empty_frame. -Proof. - intros; red; intros; exact I. -Qed. - -Lemma is_tail_find_label: - forall lbl c c', find_label lbl c = Some c' -> is_tail c' c. -Proof. - induction c; simpl. - intros; discriminate. - case (is_label lbl a); intros. - injection H; intro; subst c'. constructor. constructor. - constructor; auto. -Qed. - -Section SUBJECT_REDUCTION. - -Inductive wt_stackframe: stackframe -> Prop := - | wt_stackframe_intro: forall f sp c fr, - wt_function f -> - Val.has_type sp Tint -> - is_tail c f.(fn_code) -> - wt_frame fr -> - wt_stackframe (Stackframe f sp c fr). - -Inductive wt_state: state -> Prop := - | wt_state_intro: forall stk f sp c rs fr m - (STK: forall s, In s stk -> wt_stackframe s) - (WTF: wt_function f) - (WTSP: Val.has_type sp Tint) - (TAIL: is_tail c f.(fn_code)) - (WTRS: wt_regset rs) - (WTFR: wt_frame fr), - wt_state (State stk f sp c rs fr m) - | wt_state_call: forall stk f rs m, - (forall s, In s stk -> wt_stackframe s) -> - wt_fundef f -> - wt_regset rs -> - wt_state (Callstate stk f rs m) - | wt_state_return: forall stk rs m, - (forall s, In s stk -> wt_stackframe s) -> - wt_regset rs -> - wt_state (Returnstate stk rs m). - -Variable p: program. -Hypothesis wt_p: wt_program p. -Let ge := Genv.globalenv p. - -Lemma subject_reduction: - forall s1 t s2, step ge s1 t s2 -> - forall (WTS: wt_state s1), wt_state s2. -Proof. - induction 1; intros; inv WTS; - try (generalize (wt_function_instrs _ WTF _ (is_tail_in TAIL)); intro WTI; - eapply wt_state_intro; eauto with coqlib). - - apply wt_setreg; auto. inv WTI. eapply wt_get_slot; eauto. - - eapply wt_set_slot; eauto. inv WTI; auto. - - assert (mreg_type dst = ty). - inv WTI; auto. - assert (wt_frame (parent_frame s)). - destruct s; simpl. apply wt_empty_frame. - generalize (STK s (in_eq _ _)); intro. inv H1. auto. - apply wt_setreg; auto. - rewrite H0. eapply wt_get_slot; eauto. - apply wt_undef_getparam; auto. - -(* op *) - apply wt_setreg; auto. - inv WTI. - (* move *) - simpl in H. inv H. rewrite <- H1. apply WTRS. - (* not move *) - replace (mreg_type res) with (snd (type_of_operation op)). - apply type_of_operation_sound with fundef unit ge rs##args sp; auto. - rewrite <- H4; reflexivity. - apply wt_undef_op; auto. - -(* load *) - apply wt_setreg; auto. inv WTI. rewrite H6. eapply type_of_chunk_correct; eauto. - apply wt_undef_temps; auto. - -(* store *) - apply wt_undef_temps; auto. - -(* call *) - assert (WTFD: wt_fundef f'). - destruct ros; simpl in H. - apply (Genv.find_funct_prop wt_fundef _ _ wt_p H). - destruct (Genv.find_symbol ge i); try discriminate. - apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H). - econstructor; eauto. - intros. elim H0; intro. subst s0. econstructor; eauto with coqlib. - auto. - -(* tailcall *) - assert (WTFD: wt_fundef f'). - destruct ros; simpl in H. - apply (Genv.find_funct_prop wt_fundef _ _ wt_p H). - destruct (Genv.find_symbol ge i); try discriminate. - apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H). - econstructor; eauto. - -(* extcall *) - apply wt_setreg; auto. - inv WTI. rewrite H4. eapply external_call_well_typed; eauto. - apply wt_undef_temps; auto. - -(* goto *) - apply is_tail_find_label with lbl; congruence. -(* cond *) - apply is_tail_find_label with lbl; congruence. apply wt_undef_temps; auto. - apply wt_undef_temps; auto. -(* jumptable *) - apply is_tail_find_label with lbl; congruence. apply wt_undef_temps; auto. - -(* return *) - econstructor; eauto. - -(* internal function *) - econstructor; eauto with coqlib. inv H5; auto. exact I. - apply wt_empty_frame. - -(* external function *) - econstructor; eauto. apply wt_setreg; auto. - generalize (external_call_well_typed _ _ _ _ _ _ _ H). - unfold proj_sig_res, loc_result. - destruct (sig_res (ef_sig ef)). - destruct t0; simpl; auto. - simpl; auto. - -(* returnstate *) - generalize (H1 _ (in_eq _ _)); intro. inv H. - econstructor; eauto. - eauto with coqlib. -Qed. - -End SUBJECT_REDUCTION. - -- cgit