From f37a87e35850e57febba0a39ce3cb526e7886c10 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 28 Mar 2014 08:08:46 +0000 Subject: Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping): the new Lineartyping can't keep track of single floats that were spilled. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Lineartyping.v | 708 +++++-------------------------------------------- 1 file changed, 66 insertions(+), 642 deletions(-) (limited to 'backend/Lineartyping.v') diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index f1e3d41b..73c54538 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -10,26 +10,20 @@ (* *) (* *********************************************************************) -(** Type-checking Linear code. *) +(** Typing rules for Linear. *) -Require Import FSets. -Require FSetAVL. Require Import Coqlib. -Require Import Ordered. -Require Import Maps. -Require Import Iteration. Require Import AST. Require Import Integers. Require Import Values. Require Import Events. Require Import Op. -Require Import Machregs. Require Import Locations. Require Import Conventions. Require Import LTL. Require Import Linear. -(** The typechecker for Linear enforce several properties useful for +(** The typing rules for Linear enforce several properties useful for the proof of the [Stacking] pass: - for each instruction, the type of the result register or slot agrees with the type of values produced by the instruction; @@ -37,120 +31,13 @@ Require Import Linear. accessed through [Lgetstack] and [Lsetstack] Linear instructions. *) -(** * Tracking the flow of single-precision floats *) - -(** At each program point, we infer a set of machine registers - that are guaranteed to contain single-precision floats. - The inference is a simple forward dataflow analysis, iterating on the - list of instructions until a fixpoint is reached. The result of - the analysis is a map from labels to sets of machine registers - containing single-precision floats. *) - -Module OrderedMreg := OrderedIndexed(IndexedMreg). -Module Regset := FSetAVL.Make(OrderedMreg). - -Definition setreg (fs: Regset.t) (r: mreg) (t: typ) := - if typ_eq t Tsingle then Regset.add r fs else Regset.remove r fs. - -Fixpoint setregs (fs: Regset.t) (rl: list mreg) (tl: list typ) := - match rl, tl with - | nil, nil => fs - | r1 :: rs, t1 :: ts => setregs (setreg fs r1 t1) rs ts - | _, _ => fs - end. - -Definition copyreg (fs: Regset.t) (rd rs: mreg) := - if Regset.mem rs fs then Regset.add rd fs else Regset.remove rd fs. - -Definition allregs := - List.fold_right Regset.add Regset.empty - (float_caller_save_regs ++ float_callee_save_regs). - -Definition destroyed_at_call_regs := - List.fold_right Regset.add Regset.empty destroyed_at_call. - -Definition callregs (fs: Regset.t) := - Regset.diff fs destroyed_at_call_regs. - -Definition labelmap := PMap.t Regset.t. - -Definition update_label (lbl: label) (fs: Regset.t) (lm: labelmap) : Regset.t * labelmap * bool := - let fs1 := PMap.get lbl lm in - if Regset.subset fs1 fs - then (fs1, lm, false) - else let fs2 := Regset.inter fs fs1 in (fs2, PMap.set lbl fs2 lm, true). - -Fixpoint update_labels (lbls: list label) (fs: Regset.t) (lm: labelmap): labelmap * bool := - match lbls with - | nil => (lm, false) - | lbl1 :: lbls => - let '(fs1, lm1, changed1) := update_label lbl1 fs lm in - let '(lm2, changed2) := update_labels lbls fs lm1 in - (lm2, changed1 || changed2) - end. - -Fixpoint ana_code (lm: labelmap) (ch: bool) (fs: Regset.t) (c: code) : labelmap * bool := - match c with - | nil => (lm, ch) - | Lgetstack sl ofs ty rd :: c => - ana_code lm ch (setreg fs rd ty) c - | Lsetstack rs sl ofs ty :: c => - ana_code lm ch fs c - | Lop op args dst :: c => - match is_move_operation op args with - | Some src => ana_code lm ch (copyreg fs dst src) c - | None => ana_code lm ch (setreg fs dst (snd (type_of_operation op))) c - end - | Lload chunk addr args dst :: c => - ana_code lm ch (setreg fs dst (type_of_chunk chunk)) c - | Lstore chunk addr args src :: c => - ana_code lm ch fs c - | Lcall sg ros :: c => - ana_code lm ch (callregs fs) c - | Ltailcall sg ros :: c => - ana_code lm ch allregs c - | Lbuiltin ef args res :: c => - ana_code lm ch (setregs fs res (proj_sig_res' (ef_sig ef))) c - | Lannot ef args :: c => - ana_code lm ch fs c - | Llabel lbl :: c => - let '(fs1, lm1, ch1) := update_label lbl fs lm in - ana_code lm1 (ch || ch1) fs1 c - | Lgoto lbl :: c => - let '(fs1, lm1, ch1) := update_label lbl fs lm in - ana_code lm1 (ch || ch1) allregs c - | Lcond cond args lbl :: c => - let '(fs1, lm1, ch1) := update_label lbl fs lm in - ana_code lm1 (ch || ch1) fs c - | Ljumptable r lbls :: c => - let '(lm1, ch1) := update_labels lbls fs lm in - ana_code lm1 (ch || ch1) allregs c - | Lreturn :: c => - ana_code lm ch allregs c - end. - -Definition ana_iter (c: code) (lm: labelmap) : labelmap + labelmap := - let '(lm1, ch) := ana_code lm false Regset.empty c in - if ch then inr _ lm1 else inl _ lm. - -Definition ana_function (f: function): option (PMap.t Regset.t) := - PrimIter.iterate _ _ (ana_iter f.(fn_code)) (PMap.init allregs). - -(** * The type-checker *) - -(** The typing rules are presented as boolean-valued functions so that we +(** The rules are presented as boolean-valued functions so that we get an executable type-checker for free. *) Section WT_INSTR. Variable funct: function. -Variable lm: labelmap. - -Definition reg_type (fs: Regset.t) (r: mreg) := - let ty := mreg_type r in - if typ_eq ty Tfloat && Regset.mem r fs then Tsingle else ty. - Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool := match sl with | Local => zle 0 ofs @@ -176,579 +63,116 @@ Definition loc_valid (l: loc) : bool := | S _ _ _ => false end. -Fixpoint wt_code (fs: Regset.t) (c: code) : bool := - match c with - | nil => true - | Lgetstack sl ofs ty rd :: c => - subtype ty (mreg_type rd) && slot_valid sl ofs ty && - wt_code (setreg fs rd ty) c - | Lsetstack rs sl ofs ty :: c => - subtype (reg_type fs rs) ty && - slot_valid sl ofs ty && slot_writable sl && - wt_code fs c - | Lop op args dst :: c => +Definition wt_instr (i: instruction) : bool := + match i with + | Lgetstack sl ofs ty r => + subtype ty (mreg_type r) && slot_valid sl ofs ty + | Lsetstack r sl ofs ty => + slot_valid sl ofs ty && slot_writable sl + | Lop op args res => match is_move_operation op args with - | Some src => - typ_eq (mreg_type src) (mreg_type dst) && - wt_code (copyreg fs dst src) c - | None => - let (ty_args, ty_res) := type_of_operation op in - subtype ty_res (mreg_type dst) && - wt_code (setreg fs dst ty_res) c + | Some arg => + subtype (mreg_type arg) (mreg_type res) + | None => + let (targs, tres) := type_of_operation op in + subtype tres (mreg_type res) end - | Lload chunk addr args dst :: c => - subtype (type_of_chunk chunk) (mreg_type dst) && - wt_code (setreg fs dst (type_of_chunk chunk)) c - | Lstore chunk addr args src :: c => - wt_code fs c - | Lcall sg ros :: c => - wt_code (callregs fs) c - | Ltailcall sg ros :: c => - zeq (size_arguments sg) 0 && - wt_code allregs c - | Lbuiltin ef args res :: c => - let ty_res := proj_sig_res' (ef_sig ef) in - subtype_list ty_res (map mreg_type res) && - wt_code (setregs fs res ty_res) c - | Lannot ef args :: c => - forallb loc_valid args && - wt_code fs c - | Llabel lbl :: c => - let fs1 := PMap.get lbl lm in - Regset.subset fs1 fs && wt_code fs1 c - | Lgoto lbl :: c => - let fs1 := PMap.get lbl lm in - Regset.subset fs1 fs && wt_code allregs c - | Lcond cond args lbl :: c => - let fs1 := PMap.get lbl lm in - Regset.subset fs1 fs && wt_code fs c - | Ljumptable r lbls :: c => - forallb (fun lbl => Regset.subset (PMap.get lbl lm) fs) lbls && - wt_code allregs c - | Lreturn :: c => - wt_code allregs c + | Lload chunk addr args dst => + subtype (type_of_chunk chunk) (mreg_type dst) + | Ltailcall sg ros => + zeq (size_arguments sg) 0 + | Lbuiltin ef args res => + subtype_list (proj_sig_res' (ef_sig ef)) (map mreg_type res) + | Lannot ef args => + forallb loc_valid args + | _ => + true end. -Remark wt_code_cons: - forall fs i c, - wt_code fs (i :: c) = true -> exists fs', wt_code fs' c = true. -Proof. - simpl; intros. destruct i; InvBooleans; try (econstructor; eassumption). - destruct (is_move_operation o l). - InvBooleans; econstructor; eassumption. - destruct (type_of_operation o). InvBooleans; econstructor; eassumption. -Qed. - -Lemma wt_find_label: - forall lbl c' c fs, - find_label lbl c = Some c' -> - wt_code fs c = true -> - wt_code (PMap.get lbl lm) c' = true. -Proof. - induction c; intros. -- discriminate. -- simpl in H. specialize (is_label_correct lbl a). destruct (is_label lbl a); intros IL. - + subst a. simpl in H0. inv H. InvBooleans. auto. - + destruct (wt_code_cons _ _ _ H0) as [fs' WT]. eauto. -Qed. - End WT_INSTR. -Definition wt_funcode (f: function) (lm: labelmap) : bool := - wt_code f lm Regset.empty f.(fn_code). +Definition wt_code (f: function) (c: code) : bool := + forallb (wt_instr f) c. Definition wt_function (f: function) : bool := - match ana_function f with - | None => false - | Some lm => wt_funcode f lm - end. + wt_code f f.(fn_code). -(** * Soundness of the type system *) +(** Typing the run-time state. These definitions are used in [Stackingproof]. *) Require Import Values. -Require Import Globalenvs. -Require Import Memory. -Module RSF := FSetFacts.Facts(Regset). - -(** ** Typing the run-time state *) - -Definition loc_type (fs: Regset.t) (l: loc): typ := - match l with - | R r => reg_type fs r - | S sl ofs ty => ty - end. - -Definition wt_locset (fs: Regset.t) (ls: locset) : Prop := - forall l, Val.has_type (ls l) (loc_type fs l). - -Remark subtype_refl: - forall ty, subtype ty ty = true. -Proof. - destruct ty; reflexivity. -Qed. - -Remark reg_type_sub: - forall fs r, subtype (reg_type fs r) (mreg_type r) = true. -Proof. - intros. unfold reg_type. destruct (typ_eq (mreg_type r) Tfloat); simpl. - rewrite e. destruct (Regset.mem r fs); auto. - apply subtype_refl. -Qed. - -Lemma wt_mreg: - forall fs ls r, wt_locset fs ls -> Val.has_type (ls (R r)) (mreg_type r). -Proof. - intros. eapply Val.has_subtype. apply reg_type_sub with (fs := fs). apply H. -Qed. - -Lemma wt_locset_empty: - forall ls, - (forall l, Val.has_type (ls l) (Loc.type l)) -> - wt_locset Regset.empty ls. -Proof. - intros; red; intros. destruct l; simpl. -- unfold reg_type. change (Regset.mem r Regset.empty) with false. - rewrite andb_false_r. apply H. -- apply H. -Qed. - -Remark reg_type_mon: - forall fs1 fs2 r, Regset.Subset fs2 fs1 -> subtype (reg_type fs1 r) (reg_type fs2 r) = true. -Proof. - intros. unfold reg_type. destruct (typ_eq (mreg_type r) Tfloat); simpl. - rewrite e. destruct (Regset.mem r fs2) eqn:E. - rewrite Regset.mem_1. auto. apply H. apply Regset.mem_2; auto. - destruct (Regset.mem r fs1); auto. - apply subtype_refl. -Qed. - -Lemma wt_locset_mon: - forall fs1 fs2 ls, - Regset.Subset fs2 fs1 -> wt_locset fs1 ls -> wt_locset fs2 ls. -Proof. - intros; red; intros. apply Val.has_subtype with (loc_type fs1 l); auto. - unfold loc_type. destruct l. apply reg_type_mon; auto. apply subtype_refl. -Qed. +Definition wt_locset (ls: locset) : Prop := + forall l, Val.has_type (ls l) (Loc.type l). Lemma wt_setreg: - forall fs ls r v ty, - Val.has_type v ty -> subtype ty (mreg_type r) = true -> wt_locset fs ls -> - wt_locset (setreg fs r ty) (Locmap.set (R r) v ls). + forall ls r v, + Val.has_type v (mreg_type r) -> wt_locset ls -> wt_locset (Locmap.set (R r) v ls). Proof. intros; red; intros. - unfold Locmap.set. destruct (Loc.eq (R r) l). -- subst l. simpl. unfold reg_type, setreg. - destruct (typ_eq (mreg_type r) Tfloat && - Regset.mem r - (if typ_eq ty Tsingle then Regset.add r fs else Regset.remove r fs)) eqn:E. -+ InvBooleans. destruct (typ_eq ty Tsingle). - congruence. - rewrite RSF.remove_b in H3. unfold RSF.eqb in H3. rewrite dec_eq_true in H3. - simpl in H3. rewrite andb_false_r in H3. discriminate. -+ eapply Val.has_subtype; eauto. -- destruct (Loc.diff_dec (R r) l). -+ replace (loc_type (setreg fs r ty) l) with (loc_type fs l). - apply H1. - unfold loc_type, setreg. destruct l; auto. destruct (typ_eq ty Tsingle). - unfold reg_type. rewrite RSF.add_neq_b. auto. congruence. - unfold reg_type. rewrite RSF.remove_neq_b. auto. congruence. -+ red; auto. -Qed. - -Lemma wt_copyreg: - forall fs ls src dst v, - mreg_type src = mreg_type dst -> - wt_locset fs ls -> - Val.has_type v (reg_type fs src) -> - wt_locset (copyreg fs dst src) (Locmap.set (R dst) v ls). -Proof. - intros; red; intros. - unfold Locmap.set. destruct (Loc.eq (R dst) l). -- subst l. simpl. unfold reg_type, copyreg. - unfold reg_type in H1. rewrite H in H1. - destruct (Regset.mem src fs) eqn:SRC. - rewrite RSF.add_b. unfold RSF.eqb. rewrite dec_eq_true. simpl. auto. - rewrite RSF.remove_b. unfold RSF.eqb. rewrite dec_eq_true. simpl. rewrite ! andb_false_r. - rewrite andb_false_r in H1. auto. -- destruct (Loc.diff_dec (R dst) l). -+ replace (loc_type (copyreg fs dst src) l) with (loc_type fs l). - apply H0. - unfold loc_type, copyreg. destruct l; auto. destruct (Regset.mem src fs). - unfold reg_type. rewrite RSF.add_neq_b. auto. congruence. - unfold reg_type. rewrite RSF.remove_neq_b. auto. congruence. -+ red; auto. + unfold Locmap.set. + destruct (Loc.eq (R r) l). + subst l; auto. + destruct (Loc.diff_dec (R r) l). auto. red. auto. Qed. Lemma wt_setstack: - forall fs ls sl ofs ty v, - Val.has_type v ty -> wt_locset fs ls -> - wt_locset fs (Locmap.set (S sl ofs ty) v ls). + forall ls sl ofs ty v, + wt_locset ls -> wt_locset (Locmap.set (S sl ofs ty) v ls). Proof. intros; red; intros. unfold Locmap.set. destruct (Loc.eq (S sl ofs ty) l). - subst l. simpl. auto. + subst l. simpl. + generalize (Val.load_result_type (chunk_of_type ty) v). + replace (type_of_chunk (chunk_of_type ty)) with ty. auto. + destruct ty; reflexivity. destruct (Loc.diff_dec (S sl ofs ty) l). auto. red. auto. Qed. -Lemma wt_undef: - forall fs ls l, wt_locset fs ls -> wt_locset fs (Locmap.set l Vundef ls). -Proof. - intros; red; intros. unfold Locmap.set. - destruct (Loc.eq l l0). red; auto. - destruct (Loc.diff_dec l l0); auto. red; auto. -Qed. - Lemma wt_undef_regs: - forall fs rs ls, wt_locset fs ls -> wt_locset fs (undef_regs rs ls). + forall rs ls, wt_locset ls -> wt_locset (undef_regs rs ls). Proof. - induction rs; simpl; intros. auto. apply wt_undef; auto. + induction rs; simpl; intros. auto. apply wt_setreg; auto. red; auto. Qed. Lemma wt_call_regs: - forall fs ls, wt_locset fs ls -> wt_locset Regset.empty (call_regs ls). + forall ls, wt_locset ls -> wt_locset (call_regs ls). Proof. - intros; red; intros. unfold call_regs. destruct l. - eapply Val.has_subtype; eauto. unfold loc_type. apply reg_type_mon. - red; intros. eelim Regset.empty_1; eauto. + intros; red; intros. unfold call_regs. destruct l. auto. destruct sl. red; auto. - change (loc_type Regset.empty (S Incoming pos ty)) - with (loc_type fs (S Outgoing pos ty)). auto. + change (Loc.type (S Incoming pos ty)) with (Loc.type (S Outgoing pos ty)). auto. red; auto. Qed. -Remark set_from_list: - forall r l, Regset.In r (List.fold_right Regset.add Regset.empty l) <-> In r l. -Proof. - induction l; simpl. -- rewrite RSF.empty_iff. tauto. -- rewrite RSF.add_iff. rewrite IHl. tauto. -Qed. - Lemma wt_return_regs: - forall fs caller callee, - wt_locset fs caller -> wt_locset Regset.empty callee -> - wt_locset (callregs fs) (return_regs caller callee). + forall caller callee, + wt_locset caller -> wt_locset callee -> wt_locset (return_regs caller callee). Proof. intros; red; intros. - unfold return_regs. destruct l. -- destruct (in_dec mreg_eq r destroyed_at_call). -+ unfold loc_type. replace (reg_type (callregs fs) r) with (mreg_type r). - eapply Val.has_subtype. eapply reg_type_sub. apply (H0 (R r)). - unfold reg_type, callregs. rewrite RSF.diff_b. - rewrite (@Regset.mem_1 destroyed_at_call_regs). - rewrite ! andb_false_r. auto. - unfold destroyed_at_call_regs; apply set_from_list; auto. -+ unfold loc_type, reg_type, callregs. rewrite RSF.diff_b. - destruct (Regset.mem r destroyed_at_call_regs) eqn:E. - elim n. apply set_from_list. apply Regset.mem_2; auto. - rewrite andb_true_r. apply H. -- unfold loc_type. apply H. + unfold return_regs. destruct l; auto. + destruct (in_dec mreg_eq r destroyed_at_call); auto. Qed. Lemma wt_init: - forall fs, wt_locset fs (Locmap.init Vundef). + wt_locset (Locmap.init Vundef). Proof. red; intros. unfold Locmap.init. red; auto. Qed. -Lemma wt_setregs: - forall vl tyl rl fs rs, - Val.has_type_list vl tyl -> - subtype_list tyl (map mreg_type rl) = true -> - wt_locset fs rs -> - wt_locset (setregs fs rl tyl) (Locmap.setlist (map R rl) vl rs). -Proof. - induction vl; simpl; intros. -- destruct tyl; try contradiction. destruct rl; try discriminate. - simpl. auto. -- destruct tyl as [ | ty tyl]; try contradiction. destruct H. - destruct rl as [ | r rl]; simpl in H0; try discriminate. InvBooleans. - simpl. eapply IHvl; eauto. eapply wt_setreg; eauto. -Qed. - -Lemma wt_setregs_result: - forall sg fs v rl rs, +Lemma wt_setlist_result: + forall sg v rs, Val.has_type v (proj_sig_res sg) -> - subtype_list (proj_sig_res' sg) (map mreg_type rl) = true -> - wt_locset fs rs -> - wt_locset (setregs fs rl (proj_sig_res' sg)) - (Locmap.setlist (map R rl) (encode_long (sig_res sg) v) rs). -Proof. - intros. eapply wt_setregs; eauto. - unfold proj_sig_res in H. unfold encode_long, proj_sig_res'. - destruct (sig_res sg) as [[] | ]; simpl; intuition. - destruct v; simpl; auto. - destruct v; simpl; auto. -Qed. - -Remark in_setreg_other: - forall fs r ty r', - r' <> r -> (Regset.In r' (setreg fs r ty) <-> Regset.In r' fs). -Proof. - intros. unfold setreg. destruct (typ_eq ty Tsingle). - rewrite RSF.add_iff. intuition. - rewrite RSF.remove_iff. intuition. -Qed. - -Remark in_setregs_other: - forall r rl fs tyl, - ~In r rl -> (Regset.In r (setregs fs rl tyl) <-> Regset.In r fs). -Proof. - induction rl; simpl; intros. -- destruct tyl; tauto. -- destruct tyl. tauto. rewrite IHrl by tauto. apply in_setreg_other. intuition. -Qed. - -Remark callregs_setregs_result: - forall sg fs, - Regset.Subset (callregs fs) (setregs fs (loc_result sg) (proj_sig_res' sg)). -Proof. - red; unfold callregs; intros. rewrite RSF.diff_iff in H. destruct H. - apply in_setregs_other; auto. - red; intros; elim H0. apply set_from_list. eapply loc_result_caller_save; eauto. -Qed. - -Definition wt_fundef (fd: fundef) := - match fd with - | Internal f => wt_function f = true - | External ef => True - end. - -Inductive wt_callstack: list stackframe -> Regset.t -> Prop := - | wt_callstack_nil: forall fs, - wt_callstack nil fs - | wt_callstack_cons: forall f sp rs c s fs lm fs0 fs1 - (WTSTK: wt_callstack s fs0) - (WTF: wt_funcode f lm = true) - (WTC: wt_code f lm (callregs fs1) c = true) - (WTRS: wt_locset fs rs) - (INCL: Regset.Subset (callregs fs1) (callregs fs)), - wt_callstack (Stackframe f sp rs c :: s) fs. - -Lemma wt_parent_locset: - forall s fs, wt_callstack s fs -> wt_locset fs (parent_locset s). -Proof. - induction 1; simpl. -- apply wt_init. -- auto. -Qed. - -Lemma wt_callstack_change_fs: - forall s fs, wt_callstack s fs -> wt_callstack s (callregs fs). -Proof. - induction 1. -- constructor. -- econstructor; eauto. - apply wt_locset_mon with fs; auto. - unfold callregs; red; intros. eapply Regset.diff_1; eauto. - red; intros. exploit INCL; eauto. unfold callregs. rewrite ! RSF.diff_iff. - tauto. -Qed. - -Inductive wt_state: state -> Prop := - | wt_regular_state: forall s f sp c rs m lm fs fs0 - (WTSTK: wt_callstack s fs0) - (WTF: wt_funcode f lm = true) - (WTC: wt_code f lm fs c = true) - (WTRS: wt_locset fs rs), - wt_state (State s f sp c rs m) - | wt_call_state: forall s fd rs m fs - (WTSTK: wt_callstack s fs) - (WTFD: wt_fundef fd) - (WTRS: wt_locset fs rs), - wt_state (Callstate s fd rs m) - | wt_return_state: forall s rs m fs - (WTSTK: wt_callstack s fs) - (WTRS: wt_locset (callregs fs) rs), - wt_state (Returnstate s rs m). - -(** ** Preservation of state typing by transitions *) - -Section SOUNDNESS. - -Variable prog: program. -Let ge := Genv.globalenv prog. - -Hypothesis wt_prog: - forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd. - -Lemma wt_find_function: - forall ros rs f, find_function ge ros rs = Some f -> wt_fundef f. -Proof. - intros. - assert (X: exists i, In (i, Gfun f) prog.(prog_defs)). - { - destruct ros as [r | s]; simpl in H. - eapply Genv.find_funct_inversion; eauto. - destruct (Genv.find_symbol ge s) as [b|]; try discriminate. - eapply Genv.find_funct_ptr_inversion; eauto. - } - destruct X as [i IN]. eapply wt_prog; eauto. -Qed. - -Theorem step_type_preservation: - forall S1 t S2, step ge S1 t S2 -> wt_state S1 -> wt_state S2. -Proof. - induction 1; intros WTS; inv WTS. -- (* getstack *) - simpl in WTC; InvBooleans. - econstructor; eauto. - apply wt_setreg; auto. apply (WTRS (S sl ofs ty)). apply wt_undef_regs; auto. -- (* setstack *) - simpl in WTC; InvBooleans. - econstructor; eauto. - apply wt_setstack; auto. eapply Val.has_subtype; eauto. apply WTRS. - apply wt_undef_regs; auto. -- (* op *) - simpl in WTC. destruct (is_move_operation op args) as [src | ] eqn:ISMOVE. - + (* move *) - InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst. - simpl in H. inv H. - econstructor; eauto. - apply wt_copyreg. auto. apply wt_undef_regs; auto. apply WTRS. - + (* other ops *) - destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans. - econstructor; eauto. - apply wt_setreg; auto. - change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. - eapply type_of_operation_sound; eauto. - red; intros; subst op. simpl in ISMOVE. - destruct args; try discriminate. destruct args; discriminate. - apply wt_undef_regs; auto. -- (* load *) - simpl in WTC; InvBooleans. - econstructor; eauto. - apply wt_setreg. - destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto. - auto. - apply wt_undef_regs; auto. -- (* store *) - simpl in WTC; InvBooleans. - econstructor; eauto. - apply wt_undef_regs; auto. -- (* call *) - simpl in WTC; InvBooleans. - econstructor; eauto. econstructor; eauto. - red; auto. - eapply wt_find_function; eauto. -- (* tailcall *) - simpl in WTC; InvBooleans. - econstructor. apply wt_callstack_change_fs; eauto. - eapply wt_find_function; eauto. - apply wt_return_regs. apply wt_parent_locset; auto. - eapply wt_locset_mon; eauto. red; intros. eelim Regset.empty_1; eauto. -- (* builtin *) - simpl in WTC; InvBooleans. inv H. - econstructor; eauto. - apply wt_setregs_result; auto. - eapply external_call_well_typed; eauto. - apply wt_undef_regs; auto. -- (* annot *) - simpl in WTC; InvBooleans. - econstructor; eauto. -- (* label *) - simpl in WTC; InvBooleans. - econstructor; eauto. - eapply wt_locset_mon; eauto. apply Regset.subset_2; auto. -- (* goto *) - simpl in WTC; InvBooleans. - econstructor. eauto. eauto. - eapply wt_find_label; eauto. - eapply wt_locset_mon; eauto. apply Regset.subset_2; auto. -- (* cond branch, taken *) - simpl in WTC; InvBooleans. - econstructor. eauto. eauto. - eapply wt_find_label; eauto. - eapply wt_locset_mon. apply Regset.subset_2; eauto. - apply wt_undef_regs; auto. -- (* cond branch, not taken *) - simpl in WTC; InvBooleans. - econstructor. eauto. eauto. eauto. - apply wt_undef_regs; auto. -- (* jumptable *) - simpl in WTC; InvBooleans. - econstructor. eauto. eauto. - eapply wt_find_label; eauto. - apply wt_locset_mon with fs. - apply Regset.subset_2. rewrite List.forallb_forall in H2. apply H2. - eapply list_nth_z_in; eauto. - apply wt_undef_regs; auto. -- (* return *) - econstructor. eauto. - apply wt_return_regs. - apply wt_parent_locset; auto. - apply wt_locset_mon with fs; auto. red; intros. eelim Regset.empty_1; eauto. -- (* internal function *) - simpl in WTFD. unfold wt_function in WTFD. destruct (ana_function f) as [lm|]; try discriminate. - econstructor. eauto. eauto. eexact WTFD. - apply wt_undef_regs. eapply wt_call_regs; eauto. -- (* external function *) - inv H0. - econstructor. eauto. - eapply wt_locset_mon. 2: eapply wt_setregs_result; eauto. - apply callregs_setregs_result. - eapply external_call_well_typed; eauto. - unfold proj_sig_res', loc_result. destruct (sig_res (ef_sig ef) )as [[] | ]; auto. -- (* return *) - inv WTSTK. econstructor; eauto. - apply wt_locset_mon with (callregs fs); auto. -Qed. - -Theorem wt_initial_state: - forall S, initial_state prog S -> wt_state S. -Proof. - induction 1. econstructor. - apply wt_callstack_nil with (fs := Regset.empty). - unfold ge0 in H1. exploit Genv.find_funct_ptr_inversion; eauto. - intros [id IN]. eapply wt_prog; eauto. - apply wt_init. -Qed. - -End SOUNDNESS. - -(** Properties of well-typed states that are used in [Stackingproof]. *) - -Lemma wt_state_getstack: - forall s f sp sl ofs ty rd c rs m, - wt_state (State s f sp (Lgetstack sl ofs ty rd :: c) rs m) -> - slot_valid f sl ofs ty = true. -Proof. - intros. inv H. simpl in WTC; InvBooleans. auto. -Qed. - -Lemma wt_state_setstack: - forall s f sp sl ofs ty r c rs m, - wt_state (State s f sp (Lsetstack r sl ofs ty :: c) rs m) -> - Val.has_type (rs (R r)) ty /\ slot_valid f sl ofs ty = true /\ slot_writable sl = true. -Proof. - intros. inv H. simpl in WTC; InvBooleans. intuition. - eapply Val.has_subtype; eauto. apply WTRS. -Qed. - -Lemma wt_state_tailcall: - forall s f sp sg ros c rs m, - wt_state (State s f sp (Ltailcall sg ros :: c) rs m) -> - size_arguments sg = 0. -Proof. - intros. inv H. simpl in WTC; InvBooleans. auto. -Qed. - -Lemma wt_state_annot: - forall s f sp ef args c rs m, - wt_state (State s f sp (Lannot ef args :: c) rs m) -> - forallb (loc_valid f) args = true. -Proof. - intros. inv H. simpl in WTC; InvBooleans. auto. -Qed. - -Lemma wt_callstate_wt_locset: - forall s f rs m, - wt_state (Callstate s f rs m) -> wt_locset Regset.empty rs. -Proof. - intros. inv H. apply wt_locset_mon with fs; auto. - red; intros; eelim Regset.empty_1; eauto. + wt_locset rs -> + wt_locset (Locmap.setlist (map R (loc_result sg)) (encode_long (sig_res sg) v) rs). +Proof. + unfold loc_result, encode_long, proj_sig_res; intros. + destruct (sig_res sg) as [[] | ]; simpl. +- apply wt_setreg; auto. +- apply wt_setreg; auto. +- destruct v; simpl in H; try contradiction; + simpl; apply wt_setreg; auto; apply wt_setreg; auto. +- apply wt_setreg; auto. apply Val.has_subtype with Tsingle; auto. +- apply wt_setreg; auto. Qed. -- cgit