From 611e7b09253dbbb98e9cd4ca4e07a60b50e693fd Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 8 Jul 2008 12:04:42 +0000 Subject: Fusion partielle de la branche contsem: - semantiques a continuation pour Cminor et CminorSel - goto dans Cminor Suppression de backend/RTLbigstep.v, devenu inutile. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Cminor.v | 677 +++++++++++++++++++++++--- backend/CminorSel.v | 365 +++++++------- backend/RTLbigstep.v | 412 ---------------- backend/RTLgen.v | 193 +++++--- backend/RTLgenproof.v | 1126 +++++++++++++++++--------------------------- backend/RTLgenspec.v | 340 ++++++------- backend/Selection.v | 6 +- backend/Selectionproof.v | 265 ++++++----- cfrontend/Cminorgenproof.v | 2 +- common/Main.v | 4 +- common/Smallstep.v | 177 ++++--- 11 files changed, 1778 insertions(+), 1789 deletions(-) delete mode 100644 backend/RTLbigstep.v diff --git a/backend/Cminor.v b/backend/Cminor.v index f2eb84fd..910eaa44 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -95,11 +95,14 @@ Inductive expr : Set := [Sexit n] terminates prematurely the execution of the [n+1] enclosing [Sblock] statements. *) +Definition label := ident. + Inductive stmt : Set := | Sskip: stmt | Sassign : ident -> expr -> stmt | Sstore : memory_chunk -> expr -> expr -> stmt | Scall : option ident -> signature -> expr -> list expr -> stmt + | Stailcall: signature -> expr -> list expr -> stmt | Salloc : ident -> expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: expr -> stmt -> stmt -> stmt @@ -108,7 +111,8 @@ Inductive stmt : Set := | Sexit: nat -> stmt | Sswitch: expr -> list (int * nat) -> nat -> stmt | Sreturn: option expr -> stmt - | Stailcall: signature -> expr -> list expr -> stmt. + | Slabel: label -> stmt -> stmt + | Sgoto: label -> stmt. (** Functions are composed of a signature, a list of parameter names, a list of local variables, and a statement representing @@ -134,41 +138,7 @@ Definition funsig (fd: fundef) := | External ef => ef.(ef_sig) end. -(** * Operational semantics *) - -(** The operational semantics for Cminor is given in big-step operational - style. Expressions evaluate to values, and statements evaluate to - ``outcomes'' indicating how execution should proceed afterwards. *) - -Inductive outcome: Set := - | Out_normal: outcome (**r continue in sequence *) - | Out_exit: nat -> outcome (**r terminate [n+1] enclosing blocks *) - | Out_return: option val -> outcome (**r return immediately to caller *) - | Out_tailcall_return: val -> outcome. (**r already returned to caller via a tailcall *) - -Definition outcome_block (out: outcome) : outcome := - match out with - | Out_exit O => Out_normal - | Out_exit (S n) => Out_exit n - | out => out - end. - -Definition outcome_result_value - (out: outcome) (retsig: option typ) (vres: val) : Prop := - match out, retsig with - | Out_normal, None => vres = Vundef - | Out_return None, None => vres = Vundef - | Out_return (Some v), Some ty => vres = v - | Out_tailcall_return v, _ => vres = v - | _, _ => False - end. - -Definition outcome_free_mem - (out: outcome) (m: mem) (sp: block) : mem := - match out with - | Out_tailcall_return _ => m - | _ => Mem.free m sp - end. +(** * Operational semantics (small-step) *) (** Two kinds of evaluation environments are involved: - [genv]: global environments, define symbols and functions; @@ -201,6 +171,38 @@ Definition set_optvar (optid: option ident) (v: val) (e: env) : env := | Some id => PTree.set id v e end. +(** Continuations *) + +Inductive cont: Set := + | Kstop: cont (**r stop program execution *) + | Kseq: stmt -> cont -> cont (**r execute stmt, then cont *) + | Kblock: cont -> cont (**r exit a block, then do cont *) + | Kcall: option ident -> function -> val -> env -> cont -> cont. + (**r return to caller *) + +(** States *) + +Inductive state: Set := + | State: (**r Execution within a function *) + forall (f: function) (**r currently executing function *) + (s: stmt) (**r statement under consideration *) + (k: cont) (**r its continuation -- what to do next *) + (sp: val) (**r current stack pointer *) + (e: env) (**r current local environment *) + (m: mem), (**r current memory state *) + state + | Callstate: (**r Invocation of a function *) + forall (f: fundef) (**r function to invoke *) + (args: list val) (**r arguments provided by caller *) + (k: cont) (**r what to do next *) + (m: mem), (**r memory state *) + state + | Returnstate: (**r Return from a function *) + forall (v: val) (**r Return value *) + (k: cont) (**r what to do next *) + (m: mem), (**r memory state *) + state. + Section RELSEM. Variable ge: genv. @@ -351,6 +353,233 @@ Inductive eval_exprlist: list expr -> list val -> Prop := End EVAL_EXPR. +(** Pop continuation until a call or stop *) + +Fixpoint call_cont (k: cont) : cont := + match k with + | Kseq s k => call_cont k + | Kblock k => call_cont k + | _ => k + end. + +Definition is_call_cont (k: cont) : Prop := + match k with + | Kstop => True + | Kcall _ _ _ _ _ => True + | _ => False + end. + +(** Find the statement and manufacture the continuation + corresponding to a label *) + +Fixpoint find_label (lbl: label) (s: stmt) (k: cont) + {struct s}: option (stmt * cont) := + match s with + | Sseq s1 s2 => + match find_label lbl s1 (Kseq s2 k) with + | Some sk => Some sk + | None => find_label lbl s2 k + end + | Sifthenelse a s1 s2 => + match find_label lbl s1 k with + | Some sk => Some sk + | None => find_label lbl s2 k + end + | Sloop s1 => + find_label lbl s1 (Kseq (Sloop s1) k) + | Sblock s1 => + find_label lbl s1 (Kblock k) + | Slabel lbl' s' => + if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k + | _ => None + end. + +(** One step of execution *) + +Inductive step: state -> trace -> state -> Prop := + + | step_skip_seq: forall f s k sp e m, + step (State f Sskip (Kseq s k) sp e m) + E0 (State f s k sp e m) + | step_skip_block: forall f k sp e m, + step (State f Sskip (Kblock k) sp e m) + E0 (State f Sskip k sp e m) + | step_skip_call: forall f k sp e m, + is_call_cont k -> + f.(fn_sig).(sig_res) = None -> + step (State f Sskip k (Vptr sp Int.zero) e m) + E0 (Returnstate Vundef k (Mem.free m sp)) + + | step_assign: forall f id a k sp e m v, + eval_expr sp e m a v -> + step (State f (Sassign id a) k sp e m) + E0 (State f Sskip k sp (PTree.set id v e) m) + + | step_store: forall f chunk addr a k sp e m vaddr v m', + eval_expr sp e m addr vaddr -> + eval_expr sp e m a v -> + Mem.storev chunk m vaddr v = Some m' -> + step (State f (Sstore chunk addr a) k sp e m) + E0 (State f Sskip k sp e m') + + | step_call: forall f optid sig a bl k sp e m vf vargs fd, + eval_expr sp e m a vf -> + eval_exprlist sp e m bl vargs -> + Genv.find_funct ge vf = Some fd -> + funsig fd = sig -> + step (State f (Scall optid sig a bl) k sp e m) + E0 (Callstate fd vargs (Kcall optid f sp e k) m) + + | step_tailcall: forall f sig a bl k sp e m vf vargs fd, + eval_expr (Vptr sp Int.zero) e m a vf -> + eval_exprlist (Vptr sp Int.zero) e m bl vargs -> + Genv.find_funct ge vf = Some fd -> + funsig fd = sig -> + step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) + E0 (Callstate fd vargs (call_cont k) (Mem.free m sp)) + + | step_alloc: forall f id a k sp e m n m' b, + eval_expr sp e m a (Vint n) -> + Mem.alloc m 0 (Int.signed n) = (m', b) -> + step (State f (Salloc id a) k sp e m) + E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) 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) + + | step_ifthenelse: forall f a s1 s2 k sp e m v b, + eval_expr sp e m a v -> + Val.bool_of_val v b -> + step (State f (Sifthenelse a s1 s2) k sp e m) + E0 (State f (if b then s1 else s2) k sp e m) + + | step_loop: forall f s k sp e m, + step (State f (Sloop s) k sp e m) + E0 (State f s (Kseq (Sloop s) k) sp e m) + + | step_block: forall f s k sp e m, + step (State f (Sblock s) k sp e m) + E0 (State f s (Kblock k) sp e m) + + | step_exit_seq: forall f n s k sp e m, + step (State f (Sexit n) (Kseq s k) sp e m) + E0 (State f (Sexit n) k sp e m) + | step_exit_block_0: forall f k sp e m, + step (State f (Sexit O) (Kblock k) sp e m) + E0 (State f Sskip k sp e m) + | step_exit_block_S: forall f n k sp e m, + step (State f (Sexit (S n)) (Kblock k) sp e m) + E0 (State f (Sexit n) k sp e m) + + | step_switch: forall f a cases default k sp e m n, + eval_expr sp e m a (Vint n) -> + step (State f (Sswitch a cases default) k sp e m) + E0 (State f (Sexit (switch_target n default cases)) k sp e m) + + | step_return_0: forall f k sp e m, + f.(fn_sig).(sig_res) = None -> + step (State f (Sreturn None) k (Vptr sp Int.zero) e m) + E0 (Returnstate Vundef (call_cont k) (Mem.free m sp)) + | step_return_1: forall f a k sp e m v, + f.(fn_sig).(sig_res) <> None -> + eval_expr (Vptr sp Int.zero) e m a v -> + step (State f (Sreturn (Some a)) k (Vptr sp Int.zero) e m) + E0 (Returnstate v (call_cont k) (Mem.free m sp)) + + | step_label: forall f lbl s k sp e m, + step (State f (Slabel lbl s) k sp e m) + E0 (State f s k sp e m) + + | step_goto: forall f lbl k sp e m s' k', + find_label lbl f.(fn_body) (call_cont k) = Some(s', k') -> + step (State f (Sgoto lbl) k sp e m) + E0 (State f s' k' sp e m) + + | step_internal_function: forall f vargs k m m' sp e, + Mem.alloc m 0 f.(fn_stackspace) = (m', sp) -> + set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> + step (Callstate (Internal f) vargs k m) + E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m') + | step_external_function: forall ef vargs k m t vres, + event_match ef vargs t vres -> + step (Callstate (External ef) vargs k m) + t (Returnstate vres k m) + + | step_return: forall v optid f sp e k m, + step (Returnstate v (Kcall optid f sp e k) m) + E0 (State f Sskip k sp (set_optvar optid v e) m). + +End RELSEM. + +(** Execution of whole programs are described as sequences of transitions + from an initial state to a final state. An initial state is a [Callstate] + corresponding to the invocation of the ``main'' function of the program + without arguments and with an empty continuation. *) + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b f, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = mksignature nil (Some Tint) -> + initial_state p (Callstate f nil Kstop m0). + +(** A final state is a [Returnstate] with an empty continuation. *) + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall r m, + final_state (Returnstate (Vint r) Kstop m) r. + +(** Execution of a whole program: [exec_program p beh] + holds if the application of [p]'s main function to no arguments + in the initial memory state for [p] has [beh] as observable + behavior. *) + +Definition exec_program (p: program) (beh: program_behavior) : Prop := + program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. + +(** * Alternate operational semantics (big-step) *) + +(** In big-step style, just like expressions evaluate to values, + statements evaluate to``outcomes'' indicating how execution should + proceed afterwards. *) + +Inductive outcome: Set := + | Out_normal: outcome (**r continue in sequence *) + | Out_exit: nat -> outcome (**r terminate [n+1] enclosing blocks *) + | Out_return: option val -> outcome (**r return immediately to caller *) + | Out_tailcall_return: val -> outcome. (**r already returned to caller via a tailcall *) + +Definition outcome_block (out: outcome) : outcome := + match out with + | Out_exit O => Out_normal + | Out_exit (S n) => Out_exit n + | out => out + end. + +Definition outcome_result_value + (out: outcome) (retsig: option typ) (vres: val) : Prop := + match out, retsig with + | Out_normal, None => vres = Vundef + | Out_return None, None => vres = Vundef + | Out_return (Some v), Some ty => vres = v + | Out_tailcall_return v, _ => vres = v + | _, _ => False + end. + +Definition outcome_free_mem + (out: outcome) (m: mem) (sp: block) : mem := + match out with + | Out_tailcall_return _ => m + | _ => Mem.free m sp + end. + +Section NATURALSEM. + +Variable ge: genv. + (** Evaluation of a function invocation: [eval_funcall ge m f args t m' res] means that the function [f], applied to the arguments [args] in memory state [m], returns the value [res] in modified memory state [m']. @@ -389,18 +618,18 @@ with exec_stmt: exec_stmt sp e m Sskip E0 e m Out_normal | exec_Sassign: forall sp e m id a v, - eval_expr sp e m a v -> + eval_expr ge sp e m a v -> exec_stmt sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal | exec_Sstore: forall sp e m chunk addr a vaddr v m', - eval_expr sp e m addr vaddr -> - eval_expr sp e m a v -> + eval_expr ge sp e m addr vaddr -> + eval_expr ge sp e m a v -> Mem.storev chunk m vaddr v = Some m' -> exec_stmt sp e m (Sstore chunk addr a) E0 e m' Out_normal | exec_Scall: forall sp e m optid sig a bl vf vargs f t m' vres e', - eval_expr sp e m a vf -> - eval_exprlist sp e m bl vargs -> + eval_expr ge sp e m a vf -> + eval_exprlist ge sp e m bl vargs -> Genv.find_funct ge vf = Some f -> funsig f = sig -> eval_funcall m f vargs t m' vres -> @@ -408,13 +637,13 @@ with exec_stmt: exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal | exec_Salloc: forall sp e m id a n m' b, - eval_expr sp e m a (Vint n) -> + eval_expr ge sp e m a (Vint n) -> Mem.alloc m 0 (Int.signed n) = (m', b) -> exec_stmt sp e m (Salloc id a) E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal | exec_Sifthenelse: forall sp e m a s1 s2 v b t e' m' out, - eval_expr sp e m a v -> + eval_expr ge sp e m a v -> Val.bool_of_val v b -> exec_stmt sp e m (if b then s1 else s2) t e' m' out -> exec_stmt sp e m (Sifthenelse a s1 s2) t e' m' out @@ -449,7 +678,7 @@ with exec_stmt: exec_stmt sp e m (Sexit n) E0 e m (Out_exit n) | exec_Sswitch: forall sp e m a cases default n, - eval_expr sp e m a (Vint n) -> + eval_expr ge sp e m a (Vint n) -> exec_stmt sp e m (Sswitch a cases default) E0 e m (Out_exit (switch_target n default cases)) | exec_Sreturn_none: @@ -457,12 +686,12 @@ with exec_stmt: exec_stmt sp e m (Sreturn None) E0 e m (Out_return None) | exec_Sreturn_some: forall sp e m a v, - eval_expr sp e m a v -> + eval_expr ge sp e m a v -> exec_stmt sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v)) | exec_Stailcall: forall sp e m sig a bl vf vargs f t m' vres, - eval_expr (Vptr sp Int.zero) e m a vf -> - eval_exprlist (Vptr sp Int.zero) e m bl vargs -> + eval_expr ge (Vptr sp Int.zero) e m a vf -> + eval_exprlist ge (Vptr sp Int.zero) e m bl vargs -> Genv.find_funct ge vf = Some f -> funsig f = sig -> eval_funcall (Mem.free m sp) f vargs t m' vres -> @@ -495,15 +724,15 @@ with execinf_stmt: val -> env -> mem -> stmt -> traceinf -> Prop := | execinf_Scall: forall sp e m optid sig a bl vf vargs f t, - eval_expr sp e m a vf -> - eval_exprlist sp e m bl vargs -> + eval_expr ge sp e m a vf -> + eval_exprlist ge sp e m bl vargs -> Genv.find_funct ge vf = Some f -> funsig f = sig -> evalinf_funcall m f vargs t -> execinf_stmt sp e m (Scall optid sig a bl) t | execinf_Sifthenelse: forall sp e m a s1 s2 v b t, - eval_expr sp e m a v -> + eval_expr ge sp e m a v -> Val.bool_of_val v b -> execinf_stmt sp e m (if b then s1 else s2) t -> execinf_stmt sp e m (Sifthenelse a s1 s2) t @@ -533,21 +762,21 @@ with execinf_stmt: execinf_stmt sp e m (Sblock s) t | execinf_Stailcall: forall sp e m sig a bl vf vargs f t, - eval_expr (Vptr sp Int.zero) e m a vf -> - eval_exprlist (Vptr sp Int.zero) e m bl vargs -> + eval_expr ge (Vptr sp Int.zero) e m a vf -> + eval_exprlist ge (Vptr sp Int.zero) e m bl vargs -> Genv.find_funct ge vf = Some f -> funsig f = sig -> evalinf_funcall (Mem.free m sp) f vargs t -> execinf_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t. -End RELSEM. +End NATURALSEM. (** Execution of a whole program: [exec_program p beh] holds if the application of [p]'s main function to no arguments in the initial memory state for [p] has [beh] as observable behavior. *) -Inductive exec_program (p: program): program_behavior -> Prop := +Inductive exec_program_bigstep (p: program): program_behavior -> Prop := | program_terminates: forall b f t m r, let ge := Genv.globalenv p in @@ -556,7 +785,7 @@ Inductive exec_program (p: program): program_behavior -> Prop := Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> eval_funcall ge m0 f nil t m (Vint r) -> - exec_program p (Terminates t r) + exec_program_bigstep p (Terminates t r) | program_diverges: forall b f t, let ge := Genv.globalenv p in @@ -565,4 +794,340 @@ Inductive exec_program (p: program): program_behavior -> Prop := Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> evalinf_funcall ge m0 f nil t -> - exec_program p (Diverges t). + exec_program_bigstep p (Diverges t). + +(** ** Correctness of the big-step semantics with respect to the transition semantics *) + +Section BIGSTEP_TO_TRANSITION. + +Variable prog: program. +Let ge := Genv.globalenv prog. + +Definition eval_funcall_exec_stmt_ind2 + (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop) + (P2: val -> env -> mem -> stmt -> trace -> + env -> mem -> outcome -> Prop) := + fun a b c d e f g h i j k l m n o p q r => + conj + (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r) + (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r ). + +Inductive outcome_state_match + (sp: val) (e: env) (m: mem) (f: function) (k: cont): + outcome -> state -> Prop := + | osm_normal: + outcome_state_match sp e m f k + Out_normal + (State f Sskip k sp e m) + | osm_exit: forall n, + outcome_state_match sp e m f k + (Out_exit n) + (State f (Sexit n) k sp e m) + | osm_return_none: forall k', + call_cont k' = call_cont k -> + outcome_state_match sp e m f k + (Out_return None) + (State f (Sreturn None) k' sp e m) + | osm_return_some: forall k' a v, + call_cont k' = call_cont k -> + eval_expr ge sp e m a v -> + outcome_state_match sp e m f k + (Out_return (Some v)) + (State f (Sreturn (Some a)) k' sp e m) + | osm_tail: forall v, + outcome_state_match sp e m f k + (Out_tailcall_return v) + (Returnstate v (call_cont k) m). + +Remark is_call_cont_call_cont: + forall k, is_call_cont (call_cont k). +Proof. + induction k; simpl; auto. +Qed. + +Remark call_cont_is_call_cont: + forall k, is_call_cont k -> call_cont k = k. +Proof. + destruct k; simpl; intros; auto || contradiction. +Qed. + +Lemma eval_funcall_exec_stmt_steps: + (forall m fd args t m' res, + eval_funcall ge m fd args t m' res -> + forall k, + is_call_cont k -> + star step ge (Callstate fd args k m) + t (Returnstate res k m')) +/\(forall sp e m s t e' m' out, + exec_stmt ge sp e m s t e' m' out -> + forall f k, + exists S, + star step ge (State f s k sp e m) t S + /\ outcome_state_match sp e' m' f k out S). +Proof. + apply eval_funcall_exec_stmt_ind2; intros. + +(* funcall internal *) + destruct (H2 f k) as [S [A B]]. + assert (call_cont k = k) by (apply call_cont_is_call_cont; auto). + eapply star_left. econstructor; eauto. + eapply star_trans. eexact A. + inversion B; clear B; subst out; simpl in H3; simpl; try contradiction. + (* Out normal *) + assert (f.(fn_sig).(sig_res) = None /\ vres = Vundef). + destruct f.(fn_sig).(sig_res). contradiction. auto. + destruct H6. subst vres. + apply star_one. apply step_skip_call; auto. + (* Out_return None *) + assert (f.(fn_sig).(sig_res) = None /\ vres = Vundef). + destruct f.(fn_sig).(sig_res). contradiction. auto. + destruct H7. subst vres. + replace k with (call_cont k') by congruence. + apply star_one. apply step_return_0; auto. + (* Out_return Some *) + assert (f.(fn_sig).(sig_res) <> None /\ vres = v). + destruct f.(fn_sig).(sig_res). split; congruence. contradiction. + destruct H8. subst vres. + replace k with (call_cont k') by congruence. + apply star_one. eapply step_return_1; eauto. + (* Out_tailcall_return *) + subst vres. rewrite H5. apply star_refl. + + reflexivity. traceEq. + +(* funcall external *) + apply star_one. constructor; auto. + +(* skip *) + econstructor; split. + apply star_refl. + constructor. + +(* assign *) + exists (State f Sskip k sp (PTree.set id v e) m); split. + apply star_one. constructor. auto. + constructor. + +(* store *) + econstructor; split. + apply star_one. econstructor; eauto. + constructor. + +(* call *) + econstructor; split. + eapply star_left. econstructor; eauto. + eapply star_right. apply H4. red; auto. + constructor. reflexivity. traceEq. + subst e'. constructor. + +(* alloc *) + exists (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m'); split. + apply star_one. econstructor; eauto. + constructor. + +(* ifthenelse *) + destruct (H2 f k) as [S [A B]]. + exists S; split. + apply star_left with E0 (State f (if b then s1 else s2) k sp e m) t. + econstructor; eauto. exact A. + traceEq. + auto. + +(* seq continue *) + destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. + destruct (H2 f k) as [S2 [A2 B2]]. + inv B1. + exists S2; split. + eapply star_left. constructor. + eapply star_trans. eexact A1. + eapply star_left. constructor. eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* seq stop *) + destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. + set (S2 := + match out with + | Out_exit n => State f (Sexit n) k sp e1 m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. constructor. eapply star_trans. eexact A1. + unfold S2; destruct out; try (apply star_refl). + inv B1. apply star_one. constructor. + reflexivity. traceEq. + unfold S2; inv B1; congruence || simpl; constructor; auto. + +(* loop loop *) + destruct (H0 f (Kseq (Sloop s) k)) as [S1 [A1 B1]]. + destruct (H2 f k) as [S2 [A2 B2]]. + inv B1. + exists S2; split. + eapply star_left. constructor. + eapply star_trans. eexact A1. + eapply star_left. constructor. eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* loop stop *) + destruct (H0 f (Kseq (Sloop s) k)) as [S1 [A1 B1]]. + set (S2 := + match out with + | Out_exit n => State f (Sexit n) k sp e1 m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. constructor. eapply star_trans. eexact A1. + unfold S2; destruct out; try (apply star_refl). + inv B1. apply star_one. constructor. + reflexivity. traceEq. + unfold S2; inv B1; congruence || simpl; constructor; auto. + +(* block *) + destruct (H0 f (Kblock k)) as [S1 [A1 B1]]. + set (S2 := + match out with + | Out_normal => State f Sskip k sp e1 m1 + | Out_exit O => State f Sskip k sp e1 m1 + | Out_exit (S m) => State f (Sexit m) k sp e1 m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. constructor. eapply star_trans. eexact A1. + unfold S2; destruct out; try (apply star_refl). + inv B1. apply star_one. constructor. + inv B1. apply star_one. destruct n; constructor. + reflexivity. traceEq. + unfold S2; inv B1; simpl; try constructor; auto. + destruct n; constructor. + +(* exit *) + econstructor; split. apply star_refl. constructor. + +(* switch *) + econstructor; split. + apply star_one. econstructor; eauto. + constructor. + +(* return none *) + econstructor; split. apply star_refl. constructor; auto. + +(* return some *) + econstructor; split. apply star_refl. constructor; auto. + +(* tailcall *) + econstructor; split. + eapply star_left. econstructor; eauto. + apply H4. apply is_call_cont_call_cont. traceEq. + constructor. +Qed. + +Lemma eval_funcall_steps: + forall m fd args t m' res, + eval_funcall ge m fd args t m' res -> + forall k, + is_call_cont k -> + star step ge (Callstate fd args k m) + t (Returnstate res k m'). +Proof (proj1 eval_funcall_exec_stmt_steps). + +Lemma exec_stmt_steps: + forall sp e m s t e' m' out, + exec_stmt ge sp e m s t e' m' out -> + forall f k, + exists S, + star step ge (State f s k sp e m) t S + /\ outcome_state_match sp e' m' f k out S. +Proof (proj2 eval_funcall_exec_stmt_steps). + +Lemma evalinf_funcall_forever: + forall m fd args T k, + evalinf_funcall ge m fd args T -> + forever_plus step ge (Callstate fd args k m) T. +Proof. + cofix CIH_FUN. + assert (forall sp e m s T f k, + execinf_stmt ge sp e m s T -> + forever_plus step ge (State f s k sp e m) T). + cofix CIH_STMT. + intros. inv H. + +(* call *) + eapply forever_plus_intro. + apply plus_one. econstructor; eauto. + apply CIH_FUN. eauto. traceEq. + +(* ifthenelse *) + eapply forever_plus_intro with (s2 := State f (if b then s1 else s2) k sp e m). + apply plus_one. econstructor; eauto. + apply CIH_STMT. eauto. traceEq. + +(* seq 1 *) + eapply forever_plus_intro. + apply plus_one. constructor. + apply CIH_STMT. eauto. traceEq. + +(* seq 2 *) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kseq s2 k)) + as [S [A B]]. inv B. + eapply forever_plus_intro. + eapply plus_left. constructor. + eapply star_right. eexact A. constructor. + reflexivity. reflexivity. + apply CIH_STMT. eauto. traceEq. + +(* loop body *) + eapply forever_plus_intro. + apply plus_one. econstructor; eauto. + apply CIH_STMT. eauto. traceEq. + +(* loop loop *) + destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kseq (Sloop s0) k)) + as [S [A B]]. inv B. + eapply forever_plus_intro. + eapply plus_left. constructor. + eapply star_right. eexact A. constructor. + reflexivity. reflexivity. + apply CIH_STMT. eauto. traceEq. + +(* block *) + eapply forever_plus_intro. + apply plus_one. econstructor; eauto. + apply CIH_STMT. eauto. traceEq. + +(* tailcall *) + eapply forever_plus_intro. + apply plus_one. econstructor; eauto. + apply CIH_FUN. eauto. traceEq. + +(* function call *) + intros. inv H0. + eapply forever_plus_intro. + apply plus_one. econstructor; eauto. + apply H. eauto. + traceEq. +Qed. + +Theorem exec_program_bigstep_transition: + forall beh, + exec_program_bigstep prog beh -> + exec_program prog beh. +Proof. + intros. inv H. + (* termination *) + econstructor. + econstructor. eauto. eauto. auto. + apply eval_funcall_steps. eauto. red; auto. + econstructor. + (* divergence *) + econstructor. + econstructor. eauto. eauto. auto. + apply forever_plus_forever. + apply evalinf_funcall_forever. auto. +Qed. + +End BIGSTEP_TO_TRANSITION. + + + + diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 35788685..60c1d57a 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -67,6 +67,7 @@ Inductive stmt : Set := | Sassign : ident -> expr -> stmt | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt | Scall : option ident -> signature -> expr -> exprlist -> stmt + | Stailcall: signature -> expr -> exprlist -> stmt | Salloc : ident -> expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt @@ -75,7 +76,8 @@ Inductive stmt : Set := | Sexit: nat -> stmt | Sswitch: expr -> list (int * nat) -> nat -> stmt | Sreturn: option expr -> stmt - | Stailcall: signature -> expr -> exprlist -> stmt. + | Slabel: label -> stmt -> stmt + | Sgoto: label -> stmt. Record function : Set := mkfunction { fn_sig: signature; @@ -105,6 +107,38 @@ Definition funsig (fd: fundef) := Definition genv := Genv.t fundef. Definition letenv := list val. +(** Continuations *) + +Inductive cont: Set := + | Kstop: cont (**r stop program execution *) + | Kseq: stmt -> cont -> cont (**r execute stmt, then cont *) + | Kblock: cont -> cont (**r exit a block, then do cont *) + | Kcall: option ident -> function -> val -> env -> cont -> cont. + (**r return to caller *) + +(** States *) + +Inductive state: Set := + | State: (**r execution within a function *) + forall (f: function) (**r currently executing function *) + (s: stmt) (**r statement under consideration *) + (k: cont) (**r its continuation -- what to do next *) + (sp: val) (**r current stack pointer *) + (e: env) (**r current local environment *) + (m: mem), (**r current memory state *) + state + | Callstate: (**r invocation of a fundef *) + forall (f: fundef) (**r fundef to invoke *) + (args: list val) (**r arguments provided by caller *) + (k: cont) (**r what to do next *) + (m: mem), (**r memory state *) + state + | Returnstate: + forall (v: val) (**r return value *) + (k: cont) (**r what to do next *) + (m: mem), (**r memory state *) + state. + Section RELSEM. Variable ge: genv. @@ -174,198 +208,177 @@ Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop End EVAL_EXPR. -Inductive eval_funcall: - mem -> fundef -> list val -> trace -> - mem -> val -> Prop := - | eval_funcall_internal: - forall m f vargs m1 sp e t e2 m2 out vres, - Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) -> - set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> - exec_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t e2 m2 out -> - outcome_result_value out f.(fn_sig).(sig_res) vres -> - eval_funcall m (Internal f) vargs t (outcome_free_mem out m2 sp) vres - | eval_funcall_external: - forall ef m args t res, - event_match ef args t res -> - eval_funcall m (External ef) args t m res - -with exec_stmt: - val -> - env -> mem -> stmt -> trace -> - env -> mem -> outcome -> Prop := - | exec_Sskip: - forall sp e m, - exec_stmt sp e m Sskip E0 e m Out_normal - | exec_Sassign: - forall sp e m id a v, +(** Pop continuation until a call or stop *) + +Fixpoint call_cont (k: cont) : cont := + match k with + | Kseq s k => call_cont k + | Kblock k => call_cont k + | _ => k + end. + +Definition is_call_cont (k: cont) : Prop := + match k with + | Kstop => True + | Kcall _ _ _ _ _ => True + | _ => False + end. + +(** Find the statement and manufacture the continuation + corresponding to a label *) + +Fixpoint find_label (lbl: label) (s: stmt) (k: cont) + {struct s}: option (stmt * cont) := + match s with + | Sseq s1 s2 => + match find_label lbl s1 (Kseq s2 k) with + | Some sk => Some sk + | None => find_label lbl s2 k + end + | Sifthenelse a s1 s2 => + match find_label lbl s1 k with + | Some sk => Some sk + | None => find_label lbl s2 k + end + | Sloop s1 => + find_label lbl s1 (Kseq (Sloop s1) k) + | Sblock s1 => + find_label lbl s1 (Kblock k) + | Slabel lbl' s' => + if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k + | _ => None + end. + +(** One step of execution *) + +Inductive step: state -> trace -> state -> Prop := + + | step_skip_seq: forall f s k sp e m, + step (State f Sskip (Kseq s k) sp e m) + E0 (State f s k sp e m) + | step_skip_block: forall f k sp e m, + step (State f Sskip (Kblock k) sp e m) + E0 (State f Sskip k sp e m) + | step_skip_call: forall f k sp e m, + is_call_cont k -> + f.(fn_sig).(sig_res) = None -> + step (State f Sskip k (Vptr sp Int.zero) e m) + E0 (Returnstate Vundef k (Mem.free m sp)) + + | step_assign: forall f id a k sp e m v, eval_expr sp e m nil a v -> - exec_stmt sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal - | exec_Sstore: - forall sp e m chunk addr al b vl v vaddr m', + step (State f (Sassign id a) k sp e m) + E0 (State f Sskip k sp (PTree.set id v e) m) + + | step_store: forall f chunk addr al b k sp e m vl v vaddr m', eval_exprlist sp e m nil al vl -> eval_expr sp e m nil b v -> eval_addressing ge sp addr vl = Some vaddr -> Mem.storev chunk m vaddr v = Some m' -> - exec_stmt sp e m (Sstore chunk addr al b) E0 e m' Out_normal - | exec_Scall: - forall sp e m optid sig a bl vf vargs f t m' vres e', + step (State f (Sstore chunk addr al b) k sp e m) + E0 (State f Sskip k sp e m') + + | step_call: forall f optid sig a bl k sp e m vf vargs fd, eval_expr sp e m nil a vf -> eval_exprlist sp e m nil bl vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - eval_funcall m f vargs t m' vres -> - e' = set_optvar optid vres e -> - exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal - | exec_Salloc: - forall sp e m id a n m' b, - eval_expr sp e m nil a (Vint n) -> - Mem.alloc m 0 (Int.signed n) = (m', b) -> - exec_stmt sp e m (Salloc id a) - E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal - | exec_Sifthenelse: - forall sp e m a s1 s2 v t e' m' out, - eval_condexpr sp e m nil a v -> - exec_stmt sp e m (if v then s1 else s2) t e' m' out -> - exec_stmt sp e m (Sifthenelse a s1 s2) t e' m' out - | exec_Sseq_continue: - forall sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out, - exec_stmt sp e m s1 t1 e1 m1 Out_normal -> - exec_stmt sp e1 m1 s2 t2 e2 m2 out -> - t = t1 ** t2 -> - exec_stmt sp e m (Sseq s1 s2) t e2 m2 out - | exec_Sseq_stop: - forall sp e m t s1 s2 e1 m1 out, - exec_stmt sp e m s1 t e1 m1 out -> - out <> Out_normal -> - exec_stmt sp e m (Sseq s1 s2) t e1 m1 out - | exec_Sloop_loop: - forall sp e m s t t1 e1 m1 t2 e2 m2 out, - exec_stmt sp e m s t1 e1 m1 Out_normal -> - exec_stmt sp e1 m1 (Sloop s) t2 e2 m2 out -> - t = t1 ** t2 -> - exec_stmt sp e m (Sloop s) t e2 m2 out - | exec_Sloop_stop: - forall sp e m t s e1 m1 out, - exec_stmt sp e m s t e1 m1 out -> - out <> Out_normal -> - exec_stmt sp e m (Sloop s) t e1 m1 out - | exec_Sblock: - forall sp e m s t e1 m1 out, - exec_stmt sp e m s t e1 m1 out -> - exec_stmt sp e m (Sblock s) t e1 m1 (outcome_block out) - | exec_Sexit: - forall sp e m n, - exec_stmt sp e m (Sexit n) E0 e m (Out_exit n) - | exec_Sswitch: - forall sp e m a cases default n, - eval_expr sp e m nil a (Vint n) -> - exec_stmt sp e m (Sswitch a cases default) - E0 e m (Out_exit (switch_target n default cases)) - | exec_Sreturn_none: - forall sp e m, - exec_stmt sp e m (Sreturn None) E0 e m (Out_return None) - | exec_Sreturn_some: - forall sp e m a v, - eval_expr sp e m nil a v -> - exec_stmt sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v)) - | exec_Stailcall: - forall sp e m sig a bl vf vargs f t m' vres, + Genv.find_funct ge vf = Some fd -> + funsig fd = sig -> + step (State f (Scall optid sig a bl) k sp e m) + E0 (Callstate fd vargs (Kcall optid f sp e k) m) + + | step_tailcall: forall f sig a bl k sp e m vf vargs fd, eval_expr (Vptr sp Int.zero) e m nil a vf -> eval_exprlist (Vptr sp Int.zero) e m nil bl vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - eval_funcall (Mem.free m sp) f vargs t m' vres -> - exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m' (Out_tailcall_return vres). + Genv.find_funct ge vf = Some fd -> + funsig fd = sig -> + step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) + E0 (Callstate fd vargs (call_cont k) (Mem.free m sp)) -Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop - with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop. - -(** Coinductive semantics for divergence. *) - -CoInductive evalinf_funcall: - mem -> fundef -> list val -> traceinf -> Prop := - | evalinf_funcall_internal: - forall m f vargs m1 sp e t, - Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) -> + | step_alloc: forall f id a k sp e m n m' b, + eval_expr sp e m nil a (Vint n) -> + Mem.alloc m 0 (Int.signed n) = (m', b) -> + step (State f (Salloc id a) k sp e m) + E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) 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) + + | step_ifthenelse: forall f a s1 s2 k sp e m b, + eval_condexpr sp e m nil a b -> + step (State f (Sifthenelse a s1 s2) k sp e m) + E0 (State f (if b then s1 else s2) k sp e m) + + | step_loop: forall f s k sp e m, + step (State f (Sloop s) k sp e m) + E0 (State f s (Kseq (Sloop s) k) sp e m) + + | step_block: forall f s k sp e m, + step (State f (Sblock s) k sp e m) + E0 (State f s (Kblock k) sp e m) + + | step_exit_seq: forall f n s k sp e m, + step (State f (Sexit n) (Kseq s k) sp e m) + E0 (State f (Sexit n) k sp e m) + | step_exit_block_0: forall f k sp e m, + step (State f (Sexit O) (Kblock k) sp e m) + E0 (State f Sskip k sp e m) + | step_exit_block_S: forall f n k sp e m, + step (State f (Sexit (S n)) (Kblock k) sp e m) + E0 (State f (Sexit n) k sp e m) + + | step_switch: forall f a cases default k sp e m n, + eval_expr sp e m nil a (Vint n) -> + step (State f (Sswitch a cases default) k sp e m) + E0 (State f (Sexit (switch_target n default cases)) k sp e m) + + | step_return_0: forall f k sp e m, + f.(fn_sig).(sig_res) = None -> + step (State f (Sreturn None) k (Vptr sp Int.zero) e m) + E0 (Returnstate Vundef (call_cont k) (Mem.free m sp)) + | step_return_1: forall f a k sp e m v, + f.(fn_sig).(sig_res) <> None -> + eval_expr (Vptr sp Int.zero) e m nil a v -> + step (State f (Sreturn (Some a)) k (Vptr sp Int.zero) e m) + E0 (Returnstate v (call_cont k) (Mem.free m sp)) + + | step_label: forall f lbl s k sp e m, + step (State f (Slabel lbl s) k sp e m) + E0 (State f s k sp e m) + + | step_goto: forall f lbl k sp e m s' k', + find_label lbl f.(fn_body) (call_cont k) = Some(s', k') -> + step (State f (Sgoto lbl) k sp e m) + E0 (State f s' k' sp e m) + + | step_internal_function: forall f vargs k m m' sp e, + Mem.alloc m 0 f.(fn_stackspace) = (m', sp) -> set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> - execinf_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t -> - evalinf_funcall m (Internal f) vargs t + step (Callstate (Internal f) vargs k m) + E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m') + | step_external_function: forall ef vargs k m t vres, + event_match ef vargs t vres -> + step (Callstate (External ef) vargs k m) + t (Returnstate vres k m) -(** [execinf_stmt ge sp e m s t] means that statement [s] diverges. - [e] is the initial environment, [m] is the initial memory state, - and [t] the trace of observable events performed during the execution. *) - -with execinf_stmt: - val -> env -> mem -> stmt -> traceinf -> Prop := - | execinf_Scall: - forall sp e m optid sig a bl vf vargs f t, - eval_expr sp e m nil a vf -> - eval_exprlist sp e m nil bl vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - evalinf_funcall m f vargs t -> - execinf_stmt sp e m (Scall optid sig a bl) t - | execinf_Sifthenelse: - forall sp e m a s1 s2 v t, - eval_condexpr sp e m nil a v -> - execinf_stmt sp e m (if v then s1 else s2) t -> - execinf_stmt sp e m (Sifthenelse a s1 s2) t - | execinf_Sseq_1: - forall sp e m t s1 s2, - execinf_stmt sp e m s1 t -> - execinf_stmt sp e m (Sseq s1 s2) t - | execinf_Sseq_2: - forall sp e m t s1 t1 e1 m1 s2 t2, - exec_stmt sp e m s1 t1 e1 m1 Out_normal -> - execinf_stmt sp e1 m1 s2 t2 -> - t = t1 *** t2 -> - execinf_stmt sp e m (Sseq s1 s2) t - | execinf_Sloop_body: - forall sp e m s t, - execinf_stmt sp e m s t -> - execinf_stmt sp e m (Sloop s) t - | execinf_Sloop_loop: - forall sp e m s t t1 e1 m1 t2, - exec_stmt sp e m s t1 e1 m1 Out_normal -> - execinf_stmt sp e1 m1 (Sloop s) t2 -> - t = t1 *** t2 -> - execinf_stmt sp e m (Sloop s) t - | execinf_Sblock: - forall sp e m s t, - execinf_stmt sp e m s t -> - execinf_stmt sp e m (Sblock s) t - | execinf_Stailcall: - forall sp e m sig a bl vf vargs f t, - eval_expr (Vptr sp Int.zero) e m nil a vf -> - eval_exprlist (Vptr sp Int.zero) e m nil bl vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - evalinf_funcall (Mem.free m sp) f vargs t -> - execinf_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t. + | step_return: forall v optid f sp e k m, + step (Returnstate v (Kcall optid f sp e k) m) + E0 (State f Sskip k sp (set_optvar optid v e) m). End RELSEM. -(** Execution of a whole program: [exec_program p beh] - holds if the application of [p]'s main function to no arguments - in the initial memory state for [p] has [beh] as observable - behavior. *) - -Inductive exec_program (p: program): program_behavior -> Prop := - | program_terminates: - forall b f t m r, +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b f, let ge := Genv.globalenv p in let m0 := Genv.init_mem p in Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> - eval_funcall ge m0 f nil t m (Vint r) -> - exec_program p (Terminates t r) - | program_diverges: - forall b f t, - let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in - Genv.find_symbol ge p.(prog_main) = Some b -> - Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> - evalinf_funcall ge m0 f nil t -> - exec_program p (Diverges t). + initial_state p (Callstate f nil Kstop m0). + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall r m, + final_state (Returnstate (Vint r) Kstop m) r. + +Definition exec_program (p: program) (beh: program_behavior) : Prop := + program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. diff --git a/backend/RTLbigstep.v b/backend/RTLbigstep.v deleted file mode 100644 index 182f5935..00000000 --- a/backend/RTLbigstep.v +++ /dev/null @@ -1,412 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** An alternate, mixed-step semantics for the RTL intermediate language. *) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Events. -Require Import Mem. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Registers. -Require Import RTL. - -Section BIGSTEP. - -Variable ge: genv. - -(** The dynamic semantics of RTL is a combination of small-step (transition) - semantics and big-step semantics. Execution of an instruction performs - a single transition to the next instruction (small-step), except if - the instruction is a function call. In this case, the whole body of - the called function is executed at once and the transition terminates - on the instruction immediately following the call in the caller function. - Such ``mixed-step'' semantics is convenient for reasoning over - intra-procedural analyses and transformations. It also dispenses us - from making the call stack explicit in the semantics. - - The semantics is organized in three mutually inductive predicates. - The first is [exec_instr ge c sp pc rs m pc' rs' m']. [ge] is the - global environment (see module [Genv]), [c] the CFG for the current - function, and [sp] the pointer to the stack block for its - current activation (as in Cminor). [pc], [rs] and [m] is the - initial state of the transition: program point (CFG node) [pc], - register state (mapping of pseudo-registers to values) [rs], - and memory state [m]. The final state is [pc'], [rs'] and [m']. *) - -Inductive exec_instr: code -> val -> - node -> regset -> mem -> trace -> - node -> regset -> mem -> Prop := - | exec_Inop: - forall c sp pc rs m pc', - c!pc = Some(Inop pc') -> - exec_instr c sp pc rs m E0 pc' rs m - | exec_Iop: - forall c sp pc rs m op args res pc' v, - c!pc = Some(Iop op args res pc') -> - eval_operation ge sp op rs##args m = Some v -> - exec_instr c sp pc rs m E0 pc' (rs#res <- v) m - | exec_Iload: - forall c sp pc rs m chunk addr args dst pc' a v, - c!pc = Some(Iload chunk addr args dst pc') -> - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> - exec_instr c sp pc rs m E0 pc' (rs#dst <- v) m - | exec_Istore: - forall c sp pc rs m chunk addr args src pc' a m', - c!pc = Some(Istore chunk addr args src pc') -> - eval_addressing ge sp addr rs##args = Some a -> - Mem.storev chunk m a rs#src = Some m' -> - exec_instr c sp pc rs m E0 pc' rs m' - | exec_Icall: - forall c sp pc rs m sig ros args res pc' f vres m' t, - c!pc = Some(Icall sig ros args res pc') -> - find_function ge ros rs = Some f -> - funsig f = sig -> - exec_function f rs##args m t vres m' -> - exec_instr c sp pc rs m t pc' (rs#res <- vres) m' - | exec_Ialloc: - forall c sp pc rs m pc' arg res sz m' b, - c!pc = Some(Ialloc arg res pc') -> - rs#arg = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', b) -> - exec_instr c sp pc rs m E0 pc' (rs#res <- (Vptr b Int.zero)) m' - | exec_Icond_true: - forall c sp pc rs m cond args ifso ifnot, - c!pc = Some(Icond cond args ifso ifnot) -> - eval_condition cond rs##args m = Some true -> - exec_instr c sp pc rs m E0 ifso rs m - | exec_Icond_false: - forall c sp pc rs m cond args ifso ifnot, - c!pc = Some(Icond cond args ifso ifnot) -> - eval_condition cond rs##args m = Some false -> - exec_instr c sp pc rs m E0 ifnot rs m - -(** [exec_body ge c sp pc rs m res m'] repeatedly executes - instructions starting at [pc] in [c], until it - reaches a return or tailcall instruction. It performs - that instruction and sets [res] to the return value - and [m'] to the final memory state. *) - -with exec_body: code -> val -> - node -> regset -> mem -> trace -> - val -> mem -> Prop := - | exec_body_step: forall c sp pc rs m t1 pc1 rs1 m1 t2 t res m2, - exec_instr c sp pc rs m t1 pc1 rs1 m1 -> - exec_body c sp pc1 rs1 m1 t2 res m2 -> - t = t1 ** t2 -> - exec_body c sp pc rs m t res m2 - | exec_Ireturn: forall c stk pc rs m or res, - c!pc = Some(Ireturn or) -> - res = regmap_optget or Vundef rs -> - exec_body c (Vptr stk Int.zero) pc rs m E0 res (Mem.free m stk) - | exec_Itailcall: forall c stk pc rs m sig ros args f t res m', - c!pc = Some(Itailcall sig ros args) -> - find_function ge ros rs = Some f -> - funsig f = sig -> - exec_function f rs##args (Mem.free m stk) t res m' -> - exec_body c (Vptr stk Int.zero) pc rs m t res m' - -(** [exec_function ge f args m res m'] executes a function application. - [f] is the called function, [args] the values of its arguments, - and [m] the memory state at the beginning of the call. [res] is - the returned value: the value of [r] if the function terminates with - a [Ireturn (Some r)], or [Vundef] if it terminates with [Ireturn None]. - Evaluation proceeds by executing transitions from the function's entry - point to the first [Ireturn] instruction encountered. It is preceeded - by the allocation of the stack activation block and the binding - of register parameters to the provided arguments. - (Non-parameter registers are initialized to [Vundef].) Before returning, - the stack activation block is freed. *) - -with exec_function: fundef -> list val -> mem -> trace -> - val -> mem -> Prop := - | exec_funct_internal: - forall f m m1 stk args t m2 vres, - Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> - exec_body f.(fn_code) (Vptr stk Int.zero) - f.(fn_entrypoint) (init_regs args f.(fn_params)) m1 - t vres m2 -> - exec_function (Internal f) args m t vres m2 - | exec_funct_external: - forall ef args m t res, - event_match ef args t res -> - exec_function (External ef) args m t res m. - -Scheme exec_instr_ind_3 := Minimality for exec_instr Sort Prop - with exec_body_ind_3 := Minimality for exec_body Sort Prop - with exec_function_ind_3 := Minimality for exec_function Sort Prop. - -(** The reflexive transitive closure of [exec_instr]. *) - -Inductive exec_instrs: code -> val -> - node -> regset -> mem -> trace -> - node -> regset -> mem -> Prop := - | exec_refl: - forall c sp pc rs m, - exec_instrs c sp pc rs m E0 pc rs m - | exec_one: - forall c sp pc rs m t pc' rs' m', - exec_instr c sp pc rs m t pc' rs' m' -> - exec_instrs c sp pc rs m t pc' rs' m' - | exec_trans: - forall c sp pc1 rs1 m1 t1 pc2 rs2 m2 t2 pc3 rs3 m3 t3, - exec_instrs c sp pc1 rs1 m1 t1 pc2 rs2 m2 -> - exec_instrs c sp pc2 rs2 m2 t2 pc3 rs3 m3 -> - t3 = t1 ** t2 -> - exec_instrs c sp pc1 rs1 m1 t3 pc3 rs3 m3. - -(** Some derived execution rules. *) - -Lemma exec_instrs_exec_body: - forall c sp pc1 rs1 m1 t1 pc2 rs2 m2, - exec_instrs c sp pc1 rs1 m1 t1 pc2 rs2 m2 -> - forall res t2 m3 t3, - exec_body c sp pc2 rs2 m2 t2 res m3 -> - t3 = t1 ** t2 -> - exec_body c sp pc1 rs1 m1 t3 res m3. -Proof. - induction 1; intros. - subst t3. rewrite E0_left. auto. - eapply exec_body_step; eauto. - eapply IHexec_instrs1. eapply IHexec_instrs2. eauto. - eauto. traceEq. -Qed. - -Lemma exec_step: - forall c sp pc1 rs1 m1 t1 pc2 rs2 m2 t2 pc3 rs3 m3 t3, - exec_instr c sp pc1 rs1 m1 t1 pc2 rs2 m2 -> - exec_instrs c sp pc2 rs2 m2 t2 pc3 rs3 m3 -> - t3 = t1 ** t2 -> - exec_instrs c sp pc1 rs1 m1 t3 pc3 rs3 m3. -Proof. - intros. eapply exec_trans. apply exec_one. eauto. eauto. auto. -Qed. - -Lemma exec_Iop': - forall c sp pc rs m op args res pc' rs' v, - c!pc = Some(Iop op args res pc') -> - eval_operation ge sp op rs##args m = Some v -> - rs' = (rs#res <- v) -> - exec_instr c sp pc rs m E0 pc' rs' m. -Proof. - intros. subst rs'. eapply exec_Iop; eauto. -Qed. - -Lemma exec_Iload': - forall c sp pc rs m chunk addr args dst pc' rs' a v, - c!pc = Some(Iload chunk addr args dst pc') -> - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> - rs' = (rs#dst <- v) -> - exec_instr c sp pc rs m E0 pc' rs' m. -Proof. - intros. subst rs'. eapply exec_Iload; eauto. -Qed. - -(** Experimental: coinductive big-step semantics for divergence. *) - -CoInductive diverge_body: - code -> val -> node -> regset -> mem -> traceinf -> Prop := - | diverge_step: forall c sp pc rs m t1 pc1 rs1 m1 T2 T, - exec_instr c sp pc rs m t1 pc1 rs1 m1 -> - diverge_body c sp pc1 rs1 m1 T2 -> - T = t1 *** T2 -> - diverge_body c sp pc rs m T - | diverge_Icall: - forall c sp pc rs m sig ros args res pc' f T, - c!pc = Some(Icall sig ros args res pc') -> - find_function ge ros rs = Some f -> - funsig f = sig -> - diverge_function f rs##args m T -> - diverge_body c sp pc rs m T - | diverge_Itailcall: forall c stk pc rs m sig ros args f T, - c!pc = Some(Itailcall sig ros args) -> - find_function ge ros rs = Some f -> - funsig f = sig -> - diverge_function f rs##args (Mem.free m stk) T -> - diverge_body c (Vptr stk Int.zero) pc rs m T - -with diverge_function: fundef -> list val -> mem -> traceinf -> Prop := - | diverge_funct_internal: - forall f m m1 stk args T, - Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> - diverge_body f.(fn_code) (Vptr stk Int.zero) - f.(fn_entrypoint) (init_regs args f.(fn_params)) m1 - T -> - diverge_function (Internal f) args m T. - -End BIGSTEP. - -(** Execution of whole programs. *) - -Inductive exec_program (p: program): program_behavior -> Prop := - | exec_program_terminates: forall b f t r m, - let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in - Genv.find_symbol ge p.(prog_main) = Some b -> - Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> - exec_function ge f nil m0 t (Vint r) m -> - exec_program p (Terminates t r) - | exec_program_diverges: forall b f T, - let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in - Genv.find_symbol ge p.(prog_main) = Some b -> - Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> - diverge_function ge f nil m0 T -> - exec_program p (Diverges T). - -(** * Equivalence with the transition semantics. *) - -Section EQUIVALENCE. - -Variable ge: genv. - -Definition exec_instr_prop - (c: code) (sp: val) (pc1: node) (rs1: regset) (m1: mem) - (t: trace) (pc2: node) (rs2: regset) (m2: mem) : Prop := - forall s, - plus step ge (State s c sp pc1 rs1 m1) - t (State s c sp pc2 rs2 m2). - -Definition exec_body_prop - (c: code) (sp: val) (pc1: node) (rs1: regset) (m1: mem) - (t: trace) (res: val) (m2: mem) : Prop := - forall s, - plus step ge (State s c sp pc1 rs1 m1) - t (Returnstate s res m2). - -Definition exec_function_prop - (f: fundef) (args: list val) (m1: mem) - (t: trace) (res: val) (m2: mem) : Prop := - forall s, - plus step ge (Callstate s f args m1) - t (Returnstate s res m2). - -Lemma exec_steps: - (forall c sp pc1 rs1 m1 t pc2 rs2 m2, - exec_instr ge c sp pc1 rs1 m1 t pc2 rs2 m2 -> - exec_instr_prop c sp pc1 rs1 m1 t pc2 rs2 m2) /\ - (forall c sp pc1 rs1 m1 t res m2, - exec_body ge c sp pc1 rs1 m1 t res m2 -> - exec_body_prop c sp pc1 rs1 m1 t res m2) /\ - (forall f args m1 t res m2, - exec_function ge f args m1 t res m2 -> - exec_function_prop f args m1 t res m2). -Proof. - set (IND := fun a b c d e f g h i j k l m => - conj (exec_instr_ind_3 ge exec_instr_prop exec_body_prop exec_function_prop a b c d e f g h i j k l m) - (conj (exec_body_ind_3 ge exec_instr_prop exec_body_prop exec_function_prop a b c d e f g h i j k l m) - (exec_function_ind_3 ge exec_instr_prop exec_body_prop exec_function_prop a b c d e f g h i j k l m))). - apply IND; clear IND; - intros; red; intros. - (* nop *) - apply plus_one. eapply RTL.exec_Inop; eauto. - (* op *) - apply plus_one. eapply RTL.exec_Iop'; eauto. - (* load *) - apply plus_one. eapply RTL.exec_Iload'; eauto. - (* store *) - apply plus_one. eapply RTL.exec_Istore; eauto. - (* call *) - eapply plus_left'. eapply RTL.exec_Icall; eauto. - eapply plus_right'. apply H3. apply RTL.exec_return. - eauto. traceEq. - (* alloc *) - apply plus_one. eapply RTL.exec_Ialloc; eauto. - (* cond true *) - apply plus_one. eapply RTL.exec_Icond_true; eauto. - (* cond false *) - apply plus_one. eapply RTL.exec_Icond_false; eauto. - (* body step *) - eapply plus_trans. apply H0. apply H2. auto. - (* body return *) - apply plus_one. rewrite H0. eapply RTL.exec_Ireturn; eauto. - (* body tailcall *) - eapply plus_left'. eapply RTL.exec_Itailcall; eauto. - apply H3. traceEq. - (* internal function *) - eapply plus_left'. eapply RTL.exec_function_internal; eauto. - apply H1. traceEq. - (* external function *) - apply plus_one. eapply RTL.exec_function_external; eauto. -Qed. - -Lemma diverge_function_steps: - forall fd args m T s, - diverge_function ge fd args m T -> - forever step ge (Callstate s fd args m) T. -Proof. - assert (diverge_function_steps': - forall fd args m T s, - diverge_function ge fd args m T -> - forever_N step ge O (Callstate s fd args m) T). - cofix COINDHYP1. - assert (diverge_body_steps: forall c sp pc rs m T s, - diverge_body ge c sp pc rs m T -> - forever_N step ge O (State s c sp pc rs m) T). - cofix COINDHYP2; intros. - inv H. - (* step *) - apply forever_N_plus with (State s c sp pc1 rs1 m1) O. - destruct exec_steps as [E [F G]]. - apply E. assumption. - apply COINDHYP2. assumption. - (* call *) - change T with (E0 *** T). - apply forever_N_plus with (Callstate (Stackframe res c sp pc' rs :: s) - f rs##args m) O. - apply plus_one. eapply RTL.exec_Icall; eauto. - apply COINDHYP1. assumption. - (* tailcall *) - change T with (E0 *** T). - apply forever_N_plus with (Callstate s f rs##args (free m stk)) O. - apply plus_one. eapply RTL.exec_Itailcall; eauto. - apply COINDHYP1. assumption. - (* internal function *) - intros. inv H. - change T with (E0 *** T). - apply forever_N_plus with - (State s f.(fn_code) (Vptr stk Int.zero) - f.(fn_entrypoint) (init_regs args f.(fn_params)) m1) O. - apply plus_one. eapply RTL.exec_function_internal; eauto. - apply diverge_body_steps. assumption. - (* conclusion *) - intros. eapply forever_N_forever. eauto. -Qed. - -End EQUIVALENCE. - -Theorem exec_program_bigstep_smallstep: - forall p beh, - exec_program p beh -> - RTL.exec_program p beh. -Proof. - intros. unfold RTL.exec_program. inv H. - econstructor. - econstructor; eauto. - apply plus_star. - destruct (exec_steps (Genv.globalenv p)) as [E [F G]]. - apply (G _ _ _ _ _ _ H3). - constructor. - econstructor. - econstructor; eauto. - apply diverge_function_steps. auto. -Qed. - diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 3cc0eebf..5fde3d88 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -64,7 +64,8 @@ Inductive state_incr: state -> state -> Prop := forall (s1 s2: state), Ple s1.(st_nextnode) s2.(st_nextnode) -> Ple s1.(st_nextreg) s2.(st_nextreg) -> - (forall pc, Plt pc s1.(st_nextnode) -> s2.(st_code)!pc = s1.(st_code)!pc) -> + (forall pc, + s1.(st_code)!pc = None \/ s2.(st_code)!pc = s1.(st_code)!pc) -> state_incr s1 s2. Lemma state_incr_refl: @@ -73,19 +74,15 @@ Proof. intros. apply state_incr_intro. apply Ple_refl. apply Ple_refl. intros; auto. Qed. -Hint Resolve state_incr_refl: rtlg. Lemma state_incr_trans: forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3. Proof. - intros. inversion H. inversion H0. apply state_incr_intro. + intros. inv H; inv H0. apply state_incr_intro. apply Ple_trans with (st_nextnode s2); assumption. apply Ple_trans with (st_nextreg s2); assumption. - intros. transitivity (s2.(st_code)!pc). - apply H8. apply Plt_Ple_trans with s1.(st_nextnode); auto. - apply H3; auto. + intros. generalize (H3 pc) (H5 pc). intuition congruence. Qed. -Hint Resolve state_incr_trans: rtlg. (** ** The state and error monad *) @@ -148,6 +145,15 @@ Notation "'do' X <- A ; B" := (bind A (fun X => B)) Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) (at level 200, X ident, Y ident, A at level 100, B at level 200). +Definition handle_error (A: Set) (f g: mon A) : mon A := + fun (s: state) => + match f s with + | OK a s' i => OK a s' i + | Error _ => g s + end. + +Implicit Arguments handle_error [A]. + (** ** Operations on state *) (** The initial state (empty CFG). *) @@ -186,16 +192,14 @@ Proof. constructor; simpl. apply Ple_succ. apply Ple_refl. - intros. apply PTree.gso. apply Plt_ne; auto. + intros. destruct (st_wf s pc). right. apply PTree.gso. apply Plt_ne; auto. auto. Qed. Definition add_instr (i: instruction) : mon node := fun s => let n := s.(st_nextnode) in OK n - (mkstate s.(st_nextreg) - (Psucc n) - (PTree.set n i s.(st_code)) + (mkstate s.(st_nextreg) (Psucc n) (PTree.set n i s.(st_code)) (add_instr_wf s i)) (add_instr_incr s i). @@ -212,12 +216,26 @@ Proof. right; auto. Qed. -Definition reserve_instr (s: state): (node * state)%type := +Remark reserve_instr_incr: + forall s, + let n := s.(st_nextnode) in + state_incr s (mkstate s.(st_nextreg) + (Psucc n) + s.(st_code) + (reserve_instr_wf s)). +Proof. + intros; constructor; simpl. + apply Ple_succ. + apply Ple_refl. + auto. +Qed. + +Definition reserve_instr: mon node := + fun (s: state) => let n := s.(st_nextnode) in - (n, mkstate s.(st_nextreg) - (Psucc n) - s.(st_code) - (reserve_instr_wf s)). + OK n + (mkstate s.(st_nextreg) (Psucc n) s.(st_code) (reserve_instr_wf s)) + (reserve_instr_incr s). Remark update_instr_wf: forall s n i, @@ -231,44 +249,36 @@ Proof. rewrite PTree.gso; auto. exact (st_wf s pc). Qed. -Definition update_instr (n: node) (i: instruction) (s: state) : state := - match plt n s.(st_nextnode) with - | left PLT => - mkstate s.(st_nextreg) - s.(st_nextnode) - (PTree.set n i s.(st_code)) - (update_instr_wf s n i PLT) - | right _ => s (* never happens *) - end. - -Remark add_loop_incr: - forall s1 s3 i, - let n := fst (reserve_instr s1) in - let s2 := snd (reserve_instr s1) in - state_incr s2 s3 -> - state_incr s1 (update_instr n i s3). +Remark update_instr_incr: + forall s n i (LT: Plt n s.(st_nextnode)), + s.(st_code)!n = None -> + state_incr s + (mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set n i s.(st_code)) + (update_instr_wf s n i LT)). Proof. - intros. inv H. unfold update_instr. destruct (plt n (st_nextnode s3)). - constructor; simpl. - apply Ple_trans with (st_nextnode s2). - unfold s2; simpl. apply Ple_succ. auto. - assumption. - intros. rewrite PTree.gso. rewrite H2. reflexivity. - unfold s2; simpl. apply Plt_trans_succ. auto. - apply Plt_ne. assumption. - elim n0. apply Plt_Ple_trans with (st_nextnode s2). - unfold n, s2; simpl; apply Plt_succ. auto. + intros. + constructor; simpl; intros. + apply Ple_refl. + apply Ple_refl. + rewrite PTree.gsspec. destruct (peq pc n). left; congruence. right; auto. Qed. -Definition add_loop (body: node -> mon node) : mon node := - fun (s1: state) => - let nloop := fst(reserve_instr s1) in - let s2 := snd(reserve_instr s1) in - match body nloop s2 with - | Error msg => Error msg - | OK nbody s3 i => - OK nbody (update_instr nloop (Inop nbody) s3) - (add_loop_incr s1 s3 (Inop nbody) i) +Definition check_empty_node: + forall (s: state) (n: node), { s.(st_code)!n = None } + { True }. +Proof. + intros. case (s.(st_code)!n); intros. right; auto. left; auto. +Defined. + +Definition update_instr (n: node) (i: instruction) : mon unit := + fun s => + match plt n s.(st_nextnode), check_empty_node s n with + | left LT, left EMPTY => + OK tt + (mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set n i s.(st_code)) + (update_instr_wf s n i LT)) + (update_instr_incr s n i LT EMPTY) + | _, _ => + Error (Errors.msg "RTLgen.update_instr") end. (** Generate a fresh RTL register. *) @@ -284,8 +294,7 @@ Qed. Definition new_reg : mon reg := fun s => OK s.(st_nextreg) - (mkstate (Psucc s.(st_nextreg)) - s.(st_nextnode) s.(st_code) s.(st_wf)) + (mkstate (Psucc s.(st_nextreg)) s.(st_nextnode) s.(st_code) s.(st_wf)) (new_reg_incr s). (** ** Operations on mappings *) @@ -489,8 +498,10 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree) [nlist] if it terminates by an [exit n] construct. [rret] is the register where the return value of the function must be stored, if any. *) +Definition labelmap : Set := PTree.t node. + Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) - (nexits: list node) (nret: node) (rret: option reg) + (nexits: list node) (ngoto: labelmap) (nret: node) (rret: option reg) {struct s} : mon node := match s with | Sskip => @@ -513,6 +524,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do n2 <- add_instr (Icall sig (inl _ rf) rargs r n1); do n3 <- transl_exprlist map cl rargs n2; transl_expr map b rf n3 + | Stailcall sig b cl => + do rf <- alloc_reg map b; + do rargs <- alloc_regs map cl; + do n1 <- add_instr (Itailcall sig (inl _ rf) rargs); + do n2 <- transl_exprlist map cl rargs n1; + transl_expr map b rf n2 | Salloc id a => do ra <- alloc_reg map a; do rr <- new_reg; @@ -520,21 +537,24 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do n2 <- add_instr (Ialloc ra rr n1); transl_expr map a ra n2 | Sseq s1 s2 => - do ns <- transl_stmt map s2 nd nexits nret rret; - transl_stmt map s1 ns nexits nret rret + do ns <- transl_stmt map s2 nd nexits ngoto nret rret; + transl_stmt map s1 ns nexits ngoto nret rret | Sifthenelse a strue sfalse => if more_likely a strue sfalse then - do nfalse <- transl_stmt map sfalse nd nexits nret rret; - do ntrue <- transl_stmt map strue nd nexits nret rret; + do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret; + do ntrue <- transl_stmt map strue nd nexits ngoto nret rret; transl_condition map a ntrue nfalse else - do ntrue <- transl_stmt map strue nd nexits nret rret; - do nfalse <- transl_stmt map sfalse nd nexits nret rret; + do ntrue <- transl_stmt map strue nd nexits ngoto nret rret; + do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret; transl_condition map a ntrue nfalse | Sloop sbody => - add_loop (fun nloop => transl_stmt map sbody nloop nexits nret rret) + do n1 <- reserve_instr; + do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret; + do xx <- update_instr n1 (Inop n2); + ret n1 | Sblock sbody => - transl_stmt map sbody nd (nd :: nexits) nret rret + transl_stmt map sbody nd (nd :: nexits) ngoto nret rret | Sexit n => transl_exit nexits n | Sswitch a cases default => @@ -551,12 +571,42 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) | Some a, Some r => transl_expr map a r nret | _, _ => error (Errors.msg "RTLgen: type mismatch on return") end - | Stailcall sig b cl => - do rf <- alloc_reg map b; - do rargs <- alloc_regs map cl; - do n1 <- add_instr (Itailcall sig (inl _ rf) rargs); - do n2 <- transl_exprlist map cl rargs n1; - transl_expr map b rf n2 + | Slabel lbl s' => + do ns <- transl_stmt map s' nd nexits ngoto nret rret; + match ngoto!lbl with + | None => error (Errors.msg "RTLgen: unbound label") + | Some n => + do xx <- + (handle_error (update_instr n (Inop ns)) + (error (Errors.MSG "Multiply-defined label " :: + Errors.CTX lbl :: nil))); + ret ns + end + | Sgoto lbl => + match ngoto!lbl with + | None => error (Errors.MSG "Undefined defined label " :: + Errors.CTX lbl :: nil) + | Some n => ret n + end + end. + +(** Preallocate CFG nodes for each label defined in the function body. *) + +Definition alloc_label (lbl: Cminor.label) (maps: labelmap * state) : labelmap * state := + let (map, s) := maps in + let n := s.(st_nextnode) in + (PTree.set lbl n map, + mkstate s.(st_nextreg) (Psucc s.(st_nextnode)) s.(st_code) (reserve_instr_wf s)). + +Fixpoint reserve_labels (s: stmt) (ms: labelmap * state) + {struct s} : labelmap * state := + match s with + | Sseq s1 s2 => reserve_labels s1 (reserve_labels s2 ms) + | Sifthenelse c s1 s2 => reserve_labels s1 (reserve_labels s2 ms) + | Sloop s1 => reserve_labels s1 ms + | Sblock s1 => reserve_labels s1 ms + | Slabel lbl s1 => alloc_label lbl (reserve_labels s1 ms) + | _ => ms end. (** Translation of a CminorSel function. *) @@ -567,17 +617,18 @@ Definition ret_reg (sig: signature) (rd: reg) : option reg := | Some ty => Some rd end. -Definition transl_fun (f: CminorSel.function) : mon (node * list reg) := +Definition transl_fun (f: CminorSel.function) (ngoto: labelmap): mon (node * list reg) := do (rparams, map1) <- add_vars init_mapping f.(CminorSel.fn_params); do (rvars, map2) <- add_vars map1 f.(CminorSel.fn_vars); do rret <- new_reg; let orret := ret_reg f.(CminorSel.fn_sig) rret in do nret <- add_instr (Ireturn orret); - do nentry <- transl_stmt map2 f.(CminorSel.fn_body) nret nil nret orret; + do nentry <- transl_stmt map2 f.(CminorSel.fn_body) nret nil ngoto nret orret; ret (nentry, rparams). Definition transl_function (f: CminorSel.function) : Errors.res RTL.function := - match transl_fun f init_state with + let (ngoto, s0) := reserve_labels f.(fn_body) (PTree.empty node, init_state) in + match transl_fun f ngoto s0 with | Error msg => Errors.Error msg | OK (nentry, rparams) s i => Errors.OK (RTL.mkfunction diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index e02463a2..1074dddb 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -355,7 +355,8 @@ Proof. intros until tf. unfold transl_fundef, transf_partial_fundef. case f; intro. unfold transl_function. - case (transl_fun f0 init_state); simpl; intros. + destruct (reserve_labels (fn_body f0) (PTree.empty node, init_state)) as [ngoto s0]. + case (transl_fun f0 ngoto s0); simpl; intros. discriminate. destruct p. simpl in H. inversion H. reflexivity. intro. inversion H. reflexivity. @@ -415,6 +416,42 @@ Proof. exists rs; split. subst nd. apply star_refl. auto. Qed. +(** Correctness of the translation of [switch] statements *) + +Lemma transl_switch_correct: + forall cs sp rs m i code r nexits t ns, + tr_switch code r nexits t ns -> + rs#r = Vint i -> + exists nd, + star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs m) /\ + nth_error nexits (comptree_match i t) = Some nd. +Proof. + induction 1; intros; simpl. + exists n. split. apply star_refl. auto. + + caseEq (Int.eq i key); intros. + exists nfound; split. + apply star_one. eapply exec_Icond_true; eauto. + simpl. rewrite H2. congruence. auto. + exploit IHtr_switch; eauto. intros [nd [EX MATCH]]. + exists nd; split. + eapply star_step. eapply exec_Icond_false; eauto. + simpl. rewrite H2. congruence. eexact EX. traceEq. + auto. + + caseEq (Int.ltu i key); intros. + exploit IHtr_switch1; eauto. intros [nd [EX MATCH]]. + exists nd; split. + eapply star_step. eapply exec_Icond_true; eauto. + simpl. rewrite H2. congruence. eexact EX. traceEq. + auto. + exploit IHtr_switch2; eauto. intros [nd [EX MATCH]]. + exists nd; split. + eapply star_step. eapply exec_Icond_false; eauto. + simpl. rewrite H2. congruence. eexact EX. traceEq. + auto. +Qed. + (** ** Semantic preservation for the translation of expressions *) Section CORRECTNESS_EXPR. @@ -429,7 +466,7 @@ Variable m: mem. I /\ P e, le, m, a ------------- State cs code sp ns rs m || | - t|| t|* + || |* || | \/ v e, le, m', v ------------ State cs code sp nd rs' m' @@ -824,7 +861,73 @@ Proof End CORRECTNESS_EXPR. -(** ** Semantic preservation for the translation of terminating statements *) +(** ** Measure over CminorSel states *) + +Open Local Scope nat_scope. + +Fixpoint size_stmt (s: stmt) : nat := + match s with + | Sskip => 0 + | Sseq s1 s2 => (size_stmt s1 + size_stmt s2 + 1) + | Sifthenelse e s1 s2 => (size_stmt s1 + size_stmt s2 + 1) + | Sloop s1 => (size_stmt s1 + 1) + | Sblock s1 => (size_stmt s1 + 1) + | Sexit n => 0 + | Slabel lbl s1 => (size_stmt s1 + 1) + | _ => 1 + end. + +Fixpoint size_cont (k: cont) : nat := + match k with + | Kseq s k1 => (size_stmt s + size_cont k1 + 1) + | Kblock k1 => (size_cont k1 + 1) + | _ => 0%nat + end. + +Definition measure_state (S: CminorSel.state) := + match S with + | CminorSel.State _ s k _ _ _ => + existS (fun (x: nat) => nat) + (size_stmt s + size_cont k) + (size_stmt s) + | _ => + existS (fun (x: nat) => nat) 0 0 + end. + +Require Import Relations. +Require Import Wellfounded. + +Definition lt_state (S1 S2: CminorSel.state) := + lexprod nat (fun (x: nat) => nat) + lt (fun (x: nat) => lt) + (measure_state S1) (measure_state S2). + +Lemma lt_state_intro: + forall f1 s1 k1 sp1 e1 m1 f2 s2 k2 sp2 e2 m2, + size_stmt s1 + size_cont k1 < size_stmt s2 + size_cont k2 + \/ (size_stmt s1 + size_cont k1 = size_stmt s2 + size_cont k2 + /\ size_stmt s1 < size_stmt s2) -> + lt_state (CminorSel.State f1 s1 k1 sp1 e1 m1) + (CminorSel.State f2 s2 k2 sp2 e2 m2). +Proof. + intros. unfold lt_state. simpl. destruct H as [A | [A B]]. + apply left_lex. auto. + rewrite A. apply right_lex. auto. +Qed. + +Ltac Lt_state := + apply lt_state_intro; simpl; try omega. + +Require Import Wf_nat. + +Lemma lt_state_wf: + well_founded lt_state. +Proof. + unfold lt_state. apply wf_inverse_image with (f := measure_state). + apply wf_lexprod. apply lt_wf. intros. apply lt_wf. +Qed. + +(** ** Semantic preservation for the translation of statements *) (** The simulation diagram for the translation of statements is of the following form: @@ -854,718 +957,369 @@ End CORRECTNESS_EXPR. [e']. Moreover, the program point reached must correspond to the outcome [out]. This is captured by the following [state_for_outcome] predicate. *) -Inductive state_for_outcome - (ncont: node) (nexits: list node) (nret: node) (rret: option reg) - (cs: list stackframe) (c: code) (sp: val) (rs: regset) (m: mem): - outcome -> RTL.state -> Prop := - | state_for_normal: - state_for_outcome ncont nexits nret rret cs c sp rs m - Out_normal (State cs c sp ncont rs m) - | state_for_exit: forall n nexit, - nth_error nexits n = Some nexit -> - state_for_outcome ncont nexits nret rret cs c sp rs m - (Out_exit n) (State cs c sp nexit rs m) - | state_for_return_none: - rret = None -> - state_for_outcome ncont nexits nret rret cs c sp rs m - (Out_return None) (State cs c sp nret rs m) - | state_for_return_some: forall r v, - rret = Some r -> - rs#r = v -> - state_for_outcome ncont nexits nret rret cs c sp rs m - (Out_return (Some v)) (State cs c sp nret rs m) - | state_for_return_tail: forall v, - state_for_outcome ncont nexits nret rret cs c sp rs m - (Out_tailcall_return v) (Returnstate cs v m). - -Definition transl_stmt_prop - (sp: val) (e: env) (m: mem) (a: stmt) - (t: trace) (e': env) (m': mem) (out: outcome) : Prop := - forall cs code map ns ncont nexits nret rret rs - (MWF: map_wf map) - (TE: tr_stmt code map a ns ncont nexits nret rret) - (ME: match_env map e nil rs), - exists rs', exists st, - state_for_outcome ncont nexits nret rret cs code sp rs' m' out st - /\ star step tge (State cs code sp ns rs m) t st - /\ match_env map e' nil rs'. - -(** Finally, the correctness condition for the translation of functions - is that the translated RTL function, when applied to the same arguments - as the original Cminor function, returns the same value and performs - the same modifications on the memory state. *) - -Definition transl_function_prop - (m: mem) (f: CminorSel.fundef) (vargs: list val) - (t: trace) (m': mem) (vres: val) : Prop := - forall cs tf - (TE: transl_fundef f = OK tf), - star step tge (Callstate cs tf vargs m) t (Returnstate cs vres m'). - -Lemma transl_funcall_internal_correct: - forall (m : mem) (f : CminorSel.function) - (vargs : list val) (m1 : mem) (sp : block) (e : env) (t : trace) - (e2 : env) (m2 : mem) (out: outcome) (vres : val), - Mem.alloc m 0 (fn_stackspace f) = (m1, sp) -> - set_locals (fn_vars f) (set_params vargs (CminorSel.fn_params f)) = e -> - exec_stmt ge (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out -> - transl_stmt_prop (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out -> - outcome_result_value out f.(CminorSel.fn_sig).(sig_res) vres -> - transl_function_prop m (Internal f) vargs t - (outcome_free_mem out m2 sp) vres. +Inductive tr_funbody (c: code) (map: mapping) (f: CminorSel.function) + (ngoto: labelmap) (nret: node) (rret: option reg) : Prop := + | tr_funbody_intro: forall nentry r, + rret = ret_reg f.(CminorSel.fn_sig) r -> + tr_stmt c map f.(fn_body) nentry nret nil ngoto nret rret -> + tr_funbody c map f ngoto nret rret. + +Inductive tr_cont: RTL.code -> mapping -> + CminorSel.cont -> node -> list node -> labelmap -> node -> option reg -> + list RTL.stackframe -> Prop := + | tr_Kseq: forall c map s k nd nexits ngoto nret rret cs n, + tr_stmt c map s nd n nexits ngoto nret rret -> + tr_cont c map k n nexits ngoto nret rret cs -> + tr_cont c map (Kseq s k) nd nexits ngoto nret rret cs + | tr_Kblock: forall c map k nd nexits ngoto nret rret cs, + tr_cont c map k nd nexits ngoto nret rret cs -> + tr_cont c map (Kblock k) nd (nd :: nexits) ngoto nret rret cs + | tr_Kstop: forall c map ngoto nret rret cs, + c!nret = Some(Ireturn rret) -> + match_stacks Kstop cs -> + tr_cont c map Kstop nret nil ngoto nret rret cs + | tr_Kcall: forall c map optid f sp e k ngoto nret rret cs, + c!nret = Some(Ireturn rret) -> + match_stacks (Kcall optid f sp e k) cs -> + tr_cont c map (Kcall optid f sp e k) nret nil ngoto nret rret cs + +with match_stacks: CminorSel.cont -> list RTL.stackframe -> Prop := + | match_stacks_stop: + match_stacks Kstop nil + | match_stacks_call: forall optid f sp e k r c n rs cs map nexits ngoto nret rret n', + map_wf map -> + tr_funbody c map f ngoto nret rret -> + match_env map e nil rs -> + tr_store_optvar c map r optid n n' -> + ~reg_in_map map r -> + tr_cont c map k n' nexits ngoto nret rret cs -> + match_stacks (Kcall optid f sp e k) (Stackframe r c sp n rs :: cs). + +Inductive match_states: CminorSel.state -> RTL.state -> Prop := + | match_state: + forall f s k sp e m cs c ns rs map ncont nexits ngoto nret rret + (MWF: map_wf map) + (TS: tr_stmt c map s ns ncont nexits ngoto nret rret) + (TF: tr_funbody c map f ngoto nret rret) + (TK: tr_cont c map k ncont nexits ngoto nret rret cs) + (ME: match_env map e nil rs), + match_states (CminorSel.State f s k sp e m) + (RTL.State cs c sp ns rs m) + | match_callstate: + forall f args k m cs tf + (TF: transl_fundef f = OK tf) + (MS: match_stacks k cs), + match_states (CminorSel.Callstate f args k m) + (RTL.Callstate cs tf args m) + | match_returnstate: + forall v k m cs + (MS: match_stacks k cs), + match_states (CminorSel.Returnstate v k m) + (RTL.Returnstate cs v m). + +Lemma match_stacks_call_cont: + forall c map k ncont nexits ngoto nret rret cs, + tr_cont c map k ncont nexits ngoto nret rret cs -> + match_stacks (call_cont k) cs /\ c!nret = Some(Ireturn rret). Proof. - intros; red; intros. - generalize TE; simpl. caseEq (transl_function f); simpl. 2: congruence. - intros tfi EQ1 EQ2. injection EQ2; clear EQ2; intro EQ2. - assert (TR: tr_function f tfi). apply transl_function_charact; auto. - rewrite <- EQ2. inversion TR. subst f0. - - pose (rs := init_regs vargs rparams). - assert (ME: match_env map2 e nil rs). - rewrite <- H0. unfold rs. - eapply match_init_env_init_reg; eauto. - - assert (MWF: map_wf map2). - assert (map_valid init_mapping init_state) by apply init_mapping_valid. - exploit (add_vars_valid (CminorSel.fn_params f)); eauto. intros [A B]. - eapply add_vars_wf; eauto. eapply add_vars_wf; eauto. apply init_mapping_wf. - - exploit H2; eauto. intros [rs' [st [OUT [EX ME']]]]. - - eapply star_left. - eapply exec_function_internal; eauto. simpl. - inversion OUT; clear OUT; subst out st; simpl in H3; simpl. - - (* Out_normal *) - unfold ret_reg in H6. destruct (sig_res (CminorSel.fn_sig f)). contradiction. - subst vres orret. - eapply star_right. unfold rs in EX. eexact EX. - change Vundef with (regmap_optget None Vundef rs'). - apply exec_Ireturn. auto. reflexivity. - - (* Out_exit *) - contradiction. - - (* Out_return None *) - subst orret. - unfold ret_reg in H8. destruct (sig_res (CminorSel.fn_sig f)). contradiction. - subst vres. - eapply star_right. unfold rs in EX. eexact EX. - change Vundef with (regmap_optget None Vundef rs'). - apply exec_Ireturn. auto. - reflexivity. - - (* Out_return Some *) - subst orret. - unfold ret_reg in H8. unfold ret_reg in H9. - destruct (sig_res (CminorSel.fn_sig f)). inversion H9. - subst vres. - eapply star_right. unfold rs in EX. eexact EX. - replace v with (regmap_optget (Some rret) Vundef rs'). - apply exec_Ireturn. auto. - simpl. congruence. - reflexivity. - contradiction. - - (* a tail call *) - subst v. rewrite E0_right. auto. traceEq. + induction 1; simpl; auto. Qed. -Lemma transl_funcall_external_correct: - forall (ef : external_function) (m : mem) (args : list val) (t: trace) (res : val), - event_match ef args t res -> - transl_function_prop m (External ef) args t m res. +Lemma tr_cont_call_cont: + forall c map k ncont nexits ngoto nret rret cs, + tr_cont c map k ncont nexits ngoto nret rret cs -> + tr_cont c map (call_cont k) nret nil ngoto nret rret cs. Proof. - intros; red; intros. unfold transl_function in TE; simpl in TE. - inversion TE; subst tf. - apply star_one. apply exec_function_external. auto. + induction 1; simpl; auto; econstructor; eauto. Qed. -Lemma transl_stmt_Sskip_correct: - forall (sp: val) (e : env) (m : mem), - transl_stmt_prop sp e m Sskip E0 e m Out_normal. +Lemma tr_find_label: + forall c map lbl n (ngoto: labelmap) nret rret s' k' cs, + ngoto!lbl = Some n -> + forall s k ns1 nd1 nexits1, + find_label lbl s k = Some (s', k') -> + tr_stmt c map s ns1 nd1 nexits1 ngoto nret rret -> + tr_cont c map k nd1 nexits1 ngoto nret rret cs -> + exists ns2, exists nd2, exists nexits2, + c!n = Some(Inop ns2) + /\ tr_stmt c map s' ns2 nd2 nexits2 ngoto nret rret + /\ tr_cont c map k' nd2 nexits2 ngoto nret rret cs. Proof. - intros; red; intros; inv TE. - exists rs; econstructor. - split. constructor. - split. apply star_refl. - auto. -Qed. - -Remark state_for_outcome_stop: - forall ncont1 ncont2 nexits nret rret cs code sp rs m out st, - state_for_outcome ncont1 nexits nret rret cs code sp rs m out st -> - out <> Out_normal -> - state_for_outcome ncont2 nexits nret rret cs code sp rs m out st. -Proof. - intros. inv H; congruence || econstructor; eauto. -Qed. - -Lemma transl_stmt_Sseq_continue_correct: - forall (sp : val) (e : env) (m : mem) (t: trace) (s1 : stmt) - (t1: trace) (e1 : env) (m1 : mem) (s2 : stmt) (t2: trace) - (e2 : env) (m2 : mem) (out : outcome), - exec_stmt ge sp e m s1 t1 e1 m1 Out_normal -> - transl_stmt_prop sp e m s1 t1 e1 m1 Out_normal -> - exec_stmt ge sp e1 m1 s2 t2 e2 m2 out -> - transl_stmt_prop sp e1 m1 s2 t2 e2 m2 out -> - t = t1 ** t2 -> - transl_stmt_prop sp e m (Sseq s1 s2) t e2 m2 out. -Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. inv OUT1. - exploit H2; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]]. - exists rs2; exists st2. - split. eauto. - split. eapply star_trans; eauto. - auto. + induction s; intros until nexits1; simpl; try congruence. + (* seq *) + caseEq (find_label lbl s1 (Kseq s2 k)); intros. + inv H1. inv H2. eapply IHs1; eauto. econstructor; eauto. + inv H2. eapply IHs2; eauto. + (* ifthenelse *) + caseEq (find_label lbl s1 k); intros. + inv H1. inv H2. eapply IHs1; eauto. + inv H2. eapply IHs2; eauto. + (* loop *) + intros. inversion H1; subst. + eapply IHs; eauto. econstructor; eauto. + (* block *) + intros. inv H1. + eapply IHs; eauto. econstructor; eauto. + (* label *) + destruct (ident_eq lbl l); intros. + inv H0. inv H1. + assert (n0 = n). change positive with node in H4. congruence. subst n0. + exists ns1; exists nd1; exists nexits1; auto. + inv H1. eapply IHs; eauto. Qed. -Lemma transl_stmt_Sseq_stop_correct: - forall (sp : val) (e : env) (m : mem) (t: trace) (s1 s2 : stmt) (e1 : env) - (m1 : mem) (out : outcome), - exec_stmt ge sp e m s1 t e1 m1 out -> - transl_stmt_prop sp e m s1 t e1 m1 out -> - out <> Out_normal -> - transl_stmt_prop sp e m (Sseq s1 s2) t e1 m1 out. +Theorem transl_step_correct: + forall S1 t S2, CminorSel.step ge S1 t S2 -> + forall R1, match_states S1 R1 -> + exists R2, + (plus RTL.step tge R1 t R2 \/ (star RTL.step tge R1 t R2 /\ lt_state S2 S1)) + /\ match_states S2 R2. Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. - exists rs1; exists st1. - split. eapply state_for_outcome_stop; eauto. - auto. -Qed. - -Lemma transl_stmt_Sassign_correct: - forall (sp : val) (e : env) (m : mem) (id : ident) (a : expr) - (v : val), - eval_expr ge sp e m nil a v -> - transl_stmt_prop sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal. -Proof. - intros; red; intros; inv TE. + induction 1; intros R1 MSTATE; inv MSTATE. + + (* skip seq *) + inv TS. inv TK. econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. + + (* skip block *) + inv TS. inv TK. econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. constructor. + + (* skip return *) + inv TS. + assert (c!ncont = Some(Ireturn rret) /\ match_stacks k cs). + inv TK; simpl in H; try contradiction; auto. + destruct H1. + assert (rret = None). + inv TF. unfold ret_reg. rewrite H0. auto. + subst rret. + econstructor; split. + left; apply plus_one. eapply exec_Ireturn. eauto. + simpl. constructor; auto. + + (* assign *) + inv TS. + exploit transl_expr_correct; eauto. + intros [rs' [A [B [C D]]]]. + exploit tr_store_var_correct; eauto. + intros [rs'' [E F]]. + rewrite C in F. + econstructor; split. + right; split. eapply star_trans. eexact A. eexact E. traceEq. Lt_state. + econstructor; eauto. constructor. + + (* store *) + inv TS. + exploit transl_exprlist_correct; eauto. + intros [rs' [A [B [C D]]]]. exploit transl_expr_correct; eauto. - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit tr_store_var_correct; eauto. intros [rs2 [EX2 ME2]]. - exists rs2; econstructor. - split. constructor. - split. eapply star_trans. eexact EX1. eexact EX2. traceEq. - congruence. -Qed. - -Lemma transl_stmt_Sstore_correct: - forall (sp : val) (e : env) (m : mem) (chunk : memory_chunk) - (addr: addressing) (al: exprlist) (b: expr) - (vl: list val) (v: val) (vaddr: val) (m' : mem), - eval_exprlist ge sp e m nil al vl -> - eval_expr ge sp e m nil b v -> - eval_addressing ge sp addr vl = Some vaddr -> - storev chunk m vaddr v = Some m' -> - transl_stmt_prop sp e m (Sstore chunk addr al b) E0 e m' Out_normal. -Proof. - intros; red; intros; inv TE. - exploit transl_exprlist_correct; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit transl_expr_correct; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - exists rs2; econstructor. - (* Outcome *) - split. constructor. - (* Exec *) - split. eapply star_trans. eexact EX1. - eapply star_right. eexact EX2. - eapply exec_Istore; eauto. - assert (rs2##rl = rs1##rl). - apply list_map_exten. intros r' IN. symmetry. apply OTHER2. auto. - rewrite H3; rewrite RES1. - rewrite (@eval_addressing_preserved _ _ ge tge). eexact H1. - exact symbols_preserved. - rewrite RES2. auto. - reflexivity. traceEq. - (* Match-env *) - auto. -Qed. + intros [rs'' [E [F [G J]]]]. + assert (rs''##rl = vl). + rewrite <- C. apply list_map_exten. intros. symmetry. apply J. auto. + econstructor; split. + left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. + eapply exec_Istore with (a := vaddr); eauto. + rewrite H3. rewrite <- H1. apply eval_addressing_preserved. exact symbols_preserved. + rewrite G. eauto. + traceEq. + econstructor; eauto. constructor. -Lemma transl_stmt_Scall_correct: - forall (sp : val) (e : env) (m : mem) (optid : option ident) - (sig : signature) (a : expr) (bl : exprlist) (vf : val) - (vargs : list val) (f : CminorSel.fundef) (t : trace) (m' : mem) - (vres : val) (e' : env), - eval_expr ge sp e m nil a vf -> - eval_exprlist ge sp e m nil bl vargs -> - Genv.find_funct ge vf = Some f -> - CminorSel.funsig f = sig -> - eval_funcall ge m f vargs t m' vres -> - transl_function_prop m f vargs t m' vres -> - e' = set_optvar optid vres e -> - transl_stmt_prop sp e m (Scall optid sig a bl) t e' m' Out_normal. -Proof. - intros; red; intros; inv TE. + (* call *) + inv TS. exploit transl_expr_correct; eauto. - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. + intros [rs' [A [B [C D]]]]. exploit transl_exprlist_correct; eauto. - intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - exploit functions_translated; eauto. intros [tf [TFIND TF]]. - exploit H4; eauto. intro EXF. - exploit (tr_store_optvar_correct (rs2#rd <- vres)); eauto. - apply match_env_update_temp; eauto. - intros [rs3 [EX3 ME3]]. - exists rs3; econstructor. - (* Outcome *) - split. constructor. - (* Exec *) - split. eapply star_trans. eexact EX1. - eapply star_trans. eexact EX2. - eapply star_left. eapply exec_Icall; eauto. - simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. - eapply sig_transl_function; eauto. - eapply star_trans. rewrite RES2. eexact EXF. - eapply star_left. apply exec_return. - eexact EX3. - reflexivity. reflexivity. reflexivity. reflexivity. traceEq. - (* Match-env *) - rewrite Regmap.gss in ME3. auto. -Qed. - -Lemma transl_stmt_Salloc_correct: - forall (sp : val) (e : env) (m : mem) (id : ident) (a : expr) - (n : int) (m' : mem) (b : block), - eval_expr ge sp e m nil a (Vint n) -> - alloc m 0 (Int.signed n) = (m', b) -> - transl_stmt_prop sp e m (Salloc id a) E0 - (PTree.set id (Vptr b Int.zero) e) m' Out_normal. -Proof. - intros; red; intros; inv TE. - exploit transl_expr_correct; eauto. - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit (tr_store_var_correct (rs1#rd <- (Vptr b Int.zero))); eauto. - apply match_env_update_temp; eauto. - intros [rs2 [EX2 ME2]]. - exists rs2; econstructor. - (* Outcome *) - split. constructor. - (* Execution *) - split. eapply star_trans. eexact EX1. - eapply star_left. 2: eexact EX2. - eapply exec_Ialloc; eauto. - reflexivity. traceEq. - (* Match-env *) - rewrite Regmap.gss in ME2. auto. -Qed. - -Lemma transl_stmt_Sifthenelse_correct: - forall (sp : val) (e : env) (m : mem) (a : condexpr) (s1 s2 : stmt) - (v : bool) (t : trace) (e' : env) (m' : mem) (out : outcome), - eval_condexpr ge sp e m nil a v -> - exec_stmt ge sp e m (if v then s1 else s2) t e' m' out -> - transl_stmt_prop sp e m (if v then s1 else s2) t e' m' out -> - transl_stmt_prop sp e m (Sifthenelse a s1 s2) t e' m' out. -Proof. - intros; red; intros; inv TE. - exploit transl_condexpr_correct; eauto. - intros [rs1 [EX1 [ME1 OTHER1]]]. - assert (tr_stmt code map (if v then s1 else s2) (if v then ntrue else nfalse) - ncont nexits nret rret). - destruct v; auto. - exploit H1; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]]. - exists rs2; exists st2. - split. eauto. - split. eapply star_trans. eexact EX1. eexact EX2. auto. - auto. -Qed. - -Lemma transl_stmt_Sloop_loop_correct: - forall (sp: val) (e : env) (m : mem) (sl : stmt) (t t1: trace) - (e1 : env) (m1 : mem) (t2: trace) (e2 : env) (m2 : mem) - (out : outcome), - exec_stmt ge sp e m sl t1 e1 m1 Out_normal -> - transl_stmt_prop sp e m sl t1 e1 m1 Out_normal -> - exec_stmt ge sp e1 m1 (Sloop sl) t2 e2 m2 out -> - transl_stmt_prop sp e1 m1 (Sloop sl) t2 e2 m2 out -> - t = t1 ** t2 -> - transl_stmt_prop sp e m (Sloop sl) t e2 m2 out. -Proof. - intros; red; intros; inversion TE. subst. - exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. inv OUT1. - exploit H2; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]]. - exists rs2; exists st2. - split. eauto. - split. eapply star_trans. eexact EX1. - eapply star_left. apply exec_Inop; eauto. eexact EX2. - reflexivity. traceEq. - auto. -Qed. - -Lemma transl_stmt_Sloop_stop_correct: - forall (sp: val) (e : env) (m : mem) (t: trace) (sl : stmt) - (e1 : env) (m1 : mem) (out : outcome), - exec_stmt ge sp e m sl t e1 m1 out -> - transl_stmt_prop sp e m sl t e1 m1 out -> - out <> Out_normal -> - transl_stmt_prop sp e m (Sloop sl) t e1 m1 out. -Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. - exists rs1; exists st1. - split. eapply state_for_outcome_stop; eauto. - auto. -Qed. - -Lemma transl_stmt_Sblock_correct: - forall (sp: val) (e : env) (m : mem) (sl : stmt) (t: trace) - (e1 : env) (m1 : mem) (out : outcome), - exec_stmt ge sp e m sl t e1 m1 out -> - transl_stmt_prop sp e m sl t e1 m1 out -> - transl_stmt_prop sp e m (Sblock sl) t e1 m1 (outcome_block out). -Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. - exists rs1; exists st1. - split. inv OUT1; simpl; try (econstructor; eauto). - destruct n; simpl in H1. - inv H1. constructor. - constructor. auto. - auto. -Qed. - -Lemma transl_stmt_Sexit_correct: - forall (sp: val) (e : env) (m : mem) (n : nat), - transl_stmt_prop sp e m (Sexit n) E0 e m (Out_exit n). -Proof. - intros; red; intros; inv TE. - exists rs; econstructor. - split. econstructor; eauto. - split. apply star_refl. - auto. -Qed. - -Lemma transl_switch_correct: - forall cs sp rs m i code r nexits t ns, - tr_switch code r nexits t ns -> - rs#r = Vint i -> - exists nd, - star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs m) /\ - nth_error nexits (comptree_match i t) = Some nd. -Proof. - induction 1; intros; simpl. - exists n. split. apply star_refl. auto. - - caseEq (Int.eq i key); intros. - exists nfound; split. - apply star_one. eapply exec_Icond_true; eauto. - simpl. rewrite H2. congruence. auto. - exploit IHtr_switch; eauto. intros [nd [EX MATCH]]. - exists nd; split. - eapply star_step. eapply exec_Icond_false; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. - auto. + intros [rs'' [E [F [G J]]]]. + exploit functions_translated; eauto. intros [tf [P Q]]. + econstructor; split. + left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. + eapply exec_Icall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto. + apply sig_transl_function; auto. + traceEq. + rewrite G. constructor. auto. econstructor; eauto. - caseEq (Int.ltu i key); intros. - exploit IHtr_switch1; eauto. intros [nd [EX MATCH]]. - exists nd; split. - eapply star_step. eapply exec_Icond_true; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. - auto. - exploit IHtr_switch2; eauto. intros [nd [EX MATCH]]. - exists nd; split. - eapply star_step. eapply exec_Icond_false; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. - auto. -Qed. + (* tailcall *) + inv TS. + exploit transl_expr_correct; eauto. + intros [rs' [A [B [C D]]]]. + exploit transl_exprlist_correct; eauto. + intros [rs'' [E [F [G J]]]]. + exploit functions_translated; eauto. intros [tf [P Q]]. + exploit match_stacks_call_cont; eauto. intros [U V]. + econstructor; split. + left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. + eapply exec_Itailcall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto. + apply sig_transl_function; auto. + traceEq. + rewrite G. constructor; auto. -Lemma transl_stmt_Sswitch_correct: - forall (sp : val) (e : env) (m : mem) (a : expr) - (cases : list (int * nat)) (default : nat) (n : int), - eval_expr ge sp e m nil a (Vint n) -> - transl_stmt_prop sp e m (Sswitch a cases default) E0 e m - (Out_exit (switch_target n default cases)). -Proof. - intros; red; intros; inv TE. + (* alloc *) + inv TS. exploit transl_expr_correct; eauto. - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit transl_switch_correct; eauto. intros [nd [EX2 MO2]]. - exists rs1; econstructor. - split. econstructor. - rewrite (validate_switch_correct _ _ _ H3 n). eauto. - split. eapply star_trans. eexact EX1. eexact EX2. traceEq. - auto. -Qed. - -Lemma transl_stmt_Sreturn_none_correct: - forall (sp: val) (e : env) (m : mem), - transl_stmt_prop sp e m (Sreturn None) E0 e m (Out_return None). -Proof. - intros; red; intros; inv TE. - exists rs; econstructor. - split. constructor. auto. - split. apply star_refl. - auto. -Qed. - -Lemma transl_stmt_Sreturn_some_correct: - forall (sp : val) (e : env) (m : mem) (a : expr) (v : val), - eval_expr ge sp e m nil a v -> - transl_stmt_prop sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v)). -Proof. - intros; red; intros; inv TE. + intros [rs1 [A [B [C D]]]]. + set (rs2 := rs1#rd <- (Vptr b Int.zero)). + assert (match_env map e nil rs2). unfold rs2; eauto with rtlg. + exploit tr_store_var_correct. eauto. auto. eexact H1. + intros [rs3 [E F]]. + unfold rs2 in F. rewrite Regmap.gss in F. + econstructor; split. + left. apply plus_star_trans with E0 (State cs c sp n2 rs2 m') E0. + eapply plus_right. eexact A. unfold rs2. eapply exec_Ialloc; eauto. traceEq. + eexact E. traceEq. + econstructor; eauto. constructor. + + (* seq *) + inv TS. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. econstructor; eauto. + + (* ifthenelse *) + inv TS. + exploit transl_condexpr_correct; eauto. + intros [rs' [A [B C]]]. + econstructor; split. + right; split. eexact A. destruct b; Lt_state. + destruct b; econstructor; eauto. + + (* loop *) + inversion TS; subst. + econstructor; split. + left. apply plus_one. eapply exec_Inop; eauto. + econstructor; eauto. + econstructor; eauto. + + (* block *) + inv TS. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. econstructor; eauto. + + (* exit seq *) + inv TS. inv TK. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. econstructor; eauto. + + (* exit block 0 *) + inv TS. inv TK. simpl in H0. inv H0. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. econstructor; eauto. + + (* exit block n+1 *) + inv TS. inv TK. simpl in H0. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. econstructor; eauto. + + (* switch *) + inv TS. + exploit transl_expr_correct; eauto. + intros [rs' [A [B [C D]]]]. + exploit transl_switch_correct; eauto. + intros [nd [E F]]. + econstructor; split. + right; split. eapply star_trans. eexact A. eexact E. traceEq. Lt_state. + econstructor; eauto. + rewrite (validate_switch_correct _ _ _ H3 n). constructor. auto. + + (* return none *) + inv TS. + exploit match_stacks_call_cont; eauto. intros [U V]. + econstructor; split. + left; apply plus_one. eapply exec_Ireturn; eauto. + simpl. constructor; auto. + + (* return some *) + inv TS. exploit transl_expr_correct; eauto. - intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exists rs1; econstructor. - split. econstructor. reflexivity. auto. - eauto. -Qed. - -Lemma transl_stmt_Stailcall_correct: - forall (sp : block) (e : env) (m : mem) (sig : signature) (a : expr) - (bl : exprlist) (vf : val) (vargs : list val) (f : CminorSel.fundef) - (t : trace) (m' : mem) (vres : val), - eval_expr ge (Vptr sp Int.zero) e m nil a vf -> - eval_exprlist ge (Vptr sp Int.zero) e m nil bl vargs -> - Genv.find_funct ge vf = Some f -> - CminorSel.funsig f = sig -> - eval_funcall ge (free m sp) f vargs t m' vres -> - transl_function_prop (free m sp) f vargs t m' vres -> - transl_stmt_prop (Vptr sp Int.zero) e m (Stailcall sig a bl) t e - m' (Out_tailcall_return vres). -Proof. - intros; red; intros; inv TE. - exploit transl_expr_correct; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exploit transl_exprlist_correct; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - exploit functions_translated; eauto. intros [tf [TFIND TF]]. - exploit H4; eauto. intro EXF. - exists rs2; econstructor. - split. constructor. - split. - eapply star_trans. eexact EX1. - eapply star_trans. eexact EX2. - eapply star_step. - eapply exec_Itailcall; eauto. - simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. - eapply sig_transl_function; eauto. - rewrite RES2. eexact EXF. - reflexivity. reflexivity. traceEq. - auto. -Qed. - -(** The correctness of the translation then follows by application - of the mutual induction principle for Cminor evaluation derivations - to the lemmas above. *) - -Theorem transl_function_correct: - forall m f vargs t m' vres, - eval_funcall ge m f vargs t m' vres -> - transl_function_prop m f vargs t m' vres. -Proof - (eval_funcall_ind2 ge - transl_function_prop - transl_stmt_prop - - transl_funcall_internal_correct - transl_funcall_external_correct - transl_stmt_Sskip_correct - transl_stmt_Sassign_correct - transl_stmt_Sstore_correct - transl_stmt_Scall_correct - transl_stmt_Salloc_correct - transl_stmt_Sifthenelse_correct - transl_stmt_Sseq_continue_correct - transl_stmt_Sseq_stop_correct - transl_stmt_Sloop_loop_correct - transl_stmt_Sloop_stop_correct - transl_stmt_Sblock_correct - transl_stmt_Sexit_correct - transl_stmt_Sswitch_correct - transl_stmt_Sreturn_none_correct - transl_stmt_Sreturn_some_correct - transl_stmt_Stailcall_correct). - -Theorem transl_stmt_correct: - forall sp e m s t e' m' out, - exec_stmt ge sp e m s t e' m' out -> - transl_stmt_prop sp e m s t e' m' out. -Proof - (exec_stmt_ind2 ge - transl_function_prop - transl_stmt_prop - - transl_funcall_internal_correct - transl_funcall_external_correct - transl_stmt_Sskip_correct - transl_stmt_Sassign_correct - transl_stmt_Sstore_correct - transl_stmt_Scall_correct - transl_stmt_Salloc_correct - transl_stmt_Sifthenelse_correct - transl_stmt_Sseq_continue_correct - transl_stmt_Sseq_stop_correct - transl_stmt_Sloop_loop_correct - transl_stmt_Sloop_stop_correct - transl_stmt_Sblock_correct - transl_stmt_Sexit_correct - transl_stmt_Sswitch_correct - transl_stmt_Sreturn_none_correct - transl_stmt_Sreturn_some_correct - transl_stmt_Stailcall_correct). - -(** ** Semantic preservation for the translation of divering statements *) - -Fixpoint size_stmt (s: stmt) : nat := - match s with - | Sseq s1 s2 => (1 + size_stmt s1 + size_stmt s2)%nat - | Sifthenelse e s1 s2 => (1 + size_stmt s1 + size_stmt s2)%nat - | Sloop s1 => (1 + size_stmt s1)%nat - | Sblock s1 => (1 + size_stmt s1)%nat - | _ => 1%nat - end. - -Theorem transl_function_correct_divergence: - forall m fd vargs t tfd cs, - evalinf_funcall ge m fd vargs t -> - transl_fundef fd = OK tfd -> - forever_N step tge O (Callstate cs tfd vargs m) t. -Proof. - cofix FUNCALL. - assert (STMT: forall sp e m s t, - execinf_stmt ge sp e m s t -> - forall cs code map ns ncont nexits nret rret rs - (MWF: map_wf map) - (TE: tr_stmt code map s ns ncont nexits nret rret) - (ME: match_env map e nil rs), - forever_N step tge (size_stmt s) (State cs code sp ns rs m) t). - cofix STMT; intros. - inv H; inversion TE; subst. - (* Scall *) - destruct (transl_expr_correct _ _ _ _ _ _ H0 - cs _ _ _ _ _ _ _ MWF H7 ME) - as [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - destruct (transl_exprlist_correct _ _ _ _ _ _ H1 - cs _ _ _ _ _ _ _ MWF H8 ME1) - as [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - destruct (functions_translated _ _ H2) as [tf [TFIND TF]]. - eapply forever_N_star with (p := O). - eapply star_trans. eexact EX1. eexact EX2. reflexivity. - simpl; omega. - eapply forever_N_plus with (p := O). - apply plus_one. eapply exec_Icall; eauto. - simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. - eapply sig_transl_function; eauto. - eapply FUNCALL. rewrite RES2. eexact H4. assumption. - reflexivity. traceEq. - (* Sifthenelse *) - destruct (transl_condexpr_correct _ _ _ _ _ _ H0 - cs _ _ _ _ _ _ _ MWF H11 ME) - as [rs1 [EX1 [ME1 OTHER1]]]. - eapply forever_N_star with (p := size_stmt (if v then s1 else s2)). - eexact EX1. destruct v; simpl; omega. - eapply STMT. eexact H1. eauto. destruct v; eauto. eauto. - traceEq. - (* Sseq, 1 *) - eapply forever_N_star with (p := size_stmt s1). - apply star_refl. simpl; omega. - eapply STMT; eauto. - traceEq. - (* Sseq, 2 *) - destruct (transl_stmt_correct _ _ _ _ _ _ _ _ H0 - cs _ _ _ _ _ _ _ _ MWF H9 ME) - as [rs1 [st1 [OUT1 [EX1 ME1]]]]. - inv OUT1. - eapply forever_N_star with (p := size_stmt s2). - eexact EX1. simpl; omega. - eapply STMT; eauto. - traceEq. - (* Sloop, body *) - eapply forever_N_star with (p := size_stmt s0). - apply star_refl. simpl; omega. - eapply STMT; eauto. - traceEq. - (* Sloop, loop *) - destruct (transl_stmt_correct _ _ _ _ _ _ _ _ H0 - cs _ _ _ _ _ _ _ _ MWF H2 ME) - as [rs1 [st1 [OUT1 [EX1 ME1]]]]. - inv OUT1. - eapply forever_N_plus with (p := size_stmt (Sloop s0)). - eapply plus_right. eexact EX1. eapply exec_Inop; eauto. reflexivity. - eapply STMT; eauto. - traceEq. - (* Sblock *) - eapply forever_N_star with (p := size_stmt s0). - apply star_refl. simpl; omega. - eapply STMT; eauto. - traceEq. - (* Stailcall *) - destruct (transl_expr_correct _ _ _ _ _ _ H0 - cs _ _ _ _ _ _ _ MWF H6 ME) - as [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - destruct (transl_exprlist_correct _ _ _ _ _ _ H1 - cs _ _ _ _ _ _ _ MWF H12 ME1) - as [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. - destruct (functions_translated _ _ H2) as [tf [TFIND TF]]. - eapply forever_N_star with (p := O). - eapply star_trans. eexact EX1. eexact EX2. reflexivity. - simpl; omega. - eapply forever_N_plus with (p := O). - apply plus_one. eapply exec_Itailcall; eauto. - simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. - eapply sig_transl_function; eauto. - eapply FUNCALL. rewrite RES2. eexact H4. assumption. - reflexivity. traceEq. - (* funcall *) - intros. inversion H. subst m0 fd vargs0 t0. - generalize H0; simpl. caseEq (transl_function f); simpl. 2: congruence. - intros tfi EQ1 EQ2. injection EQ2; clear EQ2; intro EQ2. - assert (TR: tr_function f tfi). apply transl_function_charact; auto. - rewrite <- EQ2. inversion TR. subst f0. + intros [rs' [A [B [C D]]]]. + exploit match_stacks_call_cont; eauto. intros [U V]. + econstructor; split. + left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto. traceEq. + simpl. rewrite C. constructor; auto. + + (* label *) + inv TS. + econstructor; split. + right; split. apply star_refl. Lt_state. + econstructor; eauto. + + (* goto *) + inv TS. inversion TF; subst. + exploit tr_find_label; eauto. eapply tr_cont_call_cont; eauto. + intros [ns2 [nd2 [nexits2 [A [B C]]]]]. + econstructor; split. + left; apply plus_one. eapply exec_Inop; eauto. + econstructor; eauto. + + (* internal call *) + monadInv TF. exploit transl_function_charact; eauto. intro TRF. + inversion TRF. subst f0. + pose (e := set_locals (fn_vars f) (set_params vargs (CminorSel.fn_params f))). pose (rs := init_regs vargs rparams). assert (ME: match_env map2 e nil rs). - rewrite <- H2. unfold rs. - eapply match_init_env_init_reg; eauto. + unfold rs, e. eapply match_init_env_init_reg; eauto. assert (MWF: map_wf map2). - assert (map_valid init_mapping init_state) by apply init_mapping_valid. + assert (map_valid init_mapping s0) by apply init_mapping_valid. exploit (add_vars_valid (CminorSel.fn_params f)); eauto. intros [A B]. eapply add_vars_wf; eauto. eapply add_vars_wf; eauto. apply init_mapping_wf. - eapply forever_N_plus with (p := size_stmt (fn_body f)). - apply plus_one. eapply exec_function_internal; eauto. - simpl. eapply STMT; eauto. - traceEq. + econstructor; split. + left; apply plus_one. eapply exec_function_internal; simpl; eauto. + simpl. econstructor; eauto. + econstructor; eauto. + inversion MS; subst; econstructor; eauto. + + (* external call *) + monadInv TF. + econstructor; split. + left; apply plus_one. eapply exec_function_external; eauto. + constructor; auto. + + (* return *) + inv MS. + set (rs' := (rs#r <- v)). + assert (match_env map e nil rs'). unfold rs'; eauto with rtlg. + exploit tr_store_optvar_correct. eauto. eauto. eexact H. intros [rs'' [A B]]. + econstructor; split. + left; eapply plus_left. constructor. eexact A. traceEq. + econstructor; eauto. constructor. unfold rs' in B. rewrite Regmap.gss in B. auto. Qed. -(** ** Semantic preservation for whole programs. *) +Lemma transl_initial_states: + forall S, CminorSel.initial_state prog S -> + exists R, RTL.initial_state tprog R /\ match_states S R. +Proof. + induction 1. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + econstructor; split. + econstructor. rewrite (transform_partial_program_main _ _ TRANSL). fold tge. + rewrite symbols_preserved. eexact H. + eexact A. + rewrite <- H1. apply sig_transl_function; auto. + rewrite (Genv.init_mem_transf_partial _ _ TRANSL). constructor. auto. constructor. +Qed. -(** The correctness of the translation follows: - if the original Cminor program executes with observable behavior [beh], - then the generated RTL program executes with the same behavior. *) +Lemma transl_final_states: + forall S R r, + match_states S R -> CminorSel.final_state S r -> RTL.final_state R r. +Proof. + intros. inv H0. inv H. inv MS. constructor. +Qed. -Theorem transl_program_correct: +Theorem transf_program_correct: forall (beh: program_behavior), - CminorSel.exec_program prog beh -> - RTL.exec_program tprog beh. + CminorSel.exec_program prog beh -> RTL.exec_program tprog beh. Proof. - intros. inv H. - (* termination *) - exploit function_ptr_translated; eauto. intros [tf [TFIND TRANSLF]]. - exploit transl_function_correct; eauto. intro EX. - econstructor. - econstructor. - rewrite symbols_preserved. - replace (prog_main tprog) with (prog_main prog). eauto. - symmetry; apply transform_partial_program_main with transl_fundef. - exact TRANSL. - eexact TFIND. - generalize (sig_transl_function _ _ TRANSLF). congruence. - unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL). - eexact EX. - constructor. - (* divergence *) - exploit function_ptr_translated; eauto. intros [tf [TFIND TRANSLF]]. - exploit transl_function_correct_divergence; eauto. intro EX. - econstructor. - econstructor. - rewrite symbols_preserved. - replace (prog_main tprog) with (prog_main prog). eauto. - symmetry; apply transform_partial_program_main with transl_fundef. - exact TRANSL. - eexact TFIND. - generalize (sig_transl_function _ _ TRANSLF). congruence. - eapply forever_N_forever. - unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL). - eexact EX. + unfold CminorSel.exec_program, RTL.exec_program; intros. + eapply simulation_star_wf_preservation with (order := lt_state); eauto. + eexact transl_initial_states. + eexact transl_final_states. + apply lt_state_wf. + exact transl_step_correct. Qed. End CORRECTNESS. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index b8061a3f..59a5dd7e 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -136,39 +136,27 @@ Lemma instr_at_incr: forall s1 s2 n i, state_incr s1 s2 -> s1.(st_code)!n = Some i -> s2.(st_code)!n = Some i. Proof. - intros. inversion H. - rewrite H3. auto. elim (st_wf s1 n); intro. - assumption. congruence. + intros. inv H. + destruct (H3 n); congruence. Qed. Hint Resolve instr_at_incr: rtlg. -(** The following relation between two states is a weaker version of - [state_incr]. It permits changing the contents at an already reserved - graph node, but only from [None] to [Some i]. *) +(* +(** A useful tactic to reason over transitivity and reflexivity of [state_incr]. *) -Definition state_extends (s1 s2: state): Prop := - forall pc, - s1.(st_code)!pc = None \/ s2.(st_code)!pc = s1.(st_code)!pc. +Ltac Show_state_incr := + eauto; + match goal with + | |- (state_incr ?c ?c) => + apply state_incr_refl + | |- (state_incr ?c1 ?c2) => + eapply state_incr_trans; [eauto; fail | idtac]; Show_state_incr + end. -Lemma instr_at_extends: - forall s1 s2 pc i, - state_extends s1 s2 -> - s1.(st_code)!pc = Some i -> s2.(st_code)!pc = Some i. -Proof. - intros. elim (H pc); intro. congruence. congruence. -Qed. +Hint Extern 2 (state_incr _ _) => Show_state_incr : rtlg. +*) -Lemma state_incr_extends: - forall s1 s2, - state_incr s1 s2 -> state_extends s1 s2. -Proof. - unfold state_extends; intros. inversion H. - case (plt pc s1.(st_nextnode)); intro. - right; apply H2; auto. - left. elim (s1.(st_wf) pc); intro. - elim (n H5). auto. -Qed. -Hint Resolve state_incr_extends: rtlg. +Hint Resolve state_incr_refl state_incr_trans: rtlg. (** * Validity and freshness of registers *) @@ -273,70 +261,18 @@ Proof. Qed. Hint Resolve add_instr_at: rtlg. -(** Properties of [update_instr] and [add_loop]. The following diagram - shows the evolutions of the code component of the state during [add_loop]. - The vertical bar materializes the [st_nextnode] pointer. -<< - s1: I1 I2 ... In |None None None None None None None -reserve_instr - s2: I1 I2 ... In None|None None None None None None -body n - s3: I1 I2 ... In None Ip ... Iq |None None None -update_instr - s4: I1 I2 ... In Inop Ip ... Iq |None None None ->> - It is apparent that [state_incr s1 s2] and [state_incr s1 s4] hold. - Moreover, [state_extends s3 s4] holds but not [state_incr s3 s4]. -*) +(** Properties of [update_instr]. *) -Lemma update_instr_extends: - forall s1 s2 s3 i n, - reserve_instr s1 = (n, s2) -> - state_incr s2 s3 -> - state_extends s3 (update_instr n i s3). +Lemma update_instr_at: + forall n i s1 s2 incr u, + update_instr n i s1 = OK u s2 incr -> s2.(st_code)!n = Some i. Proof. - intros. injection H. intros EQ1 EQ2. - unfold update_instr. destruct (plt n (st_nextnode s3)). - red; simpl; intros. rewrite PTree.gsspec. - case (peq pc n); intro. - subst pc. left. inversion H0. subst s0 s4. rewrite H3. - rewrite <- EQ1; simpl. - destruct (s1.(st_wf) n). - rewrite <- EQ2 in H4. elim (Plt_strict _ H4). - auto. - rewrite <- EQ1; rewrite <- EQ2; simpl. apply Plt_succ. - auto. - red; intros; auto. -Qed. - -Lemma add_loop_inversion: - forall f s1 nbody s4 i, - add_loop f s1 = OK nbody s4 i -> - exists nloop, exists s2, exists s3, exists i', - state_incr s1 s2 - /\ f nloop s2 = OK nbody s3 i' - /\ state_extends s3 s4 - /\ s4.(st_code)!nloop = Some(Inop nbody). -Proof. - intros until i. unfold add_loop. - unfold reserve_instr; simpl. - set (s2 := mkstate (st_nextreg s1) (Psucc (st_nextnode s1)) (st_code s1) - (reserve_instr_wf s1)). - set (nloop := st_nextnode s1). - case_eq (f nloop s2). intros; discriminate. - intros n s3 i' EQ1 EQ2. inv EQ2. - exists nloop; exists s2; exists s3; exists i'. - split. - unfold s2; constructor; simpl. - apply Ple_succ. apply Ple_refl. auto. - split. auto. - split. apply update_instr_extends with s1 s2; auto. - unfold update_instr. destruct (plt nloop (st_nextnode s3)). - simpl. apply PTree.gss. - elim n. apply Plt_Ple_trans with (st_nextnode s2). - unfold nloop, s2; simpl; apply Plt_succ. - inversion i'; auto. + intros. unfold update_instr in H. + destruct (plt n (st_nextnode s1)); try discriminate. + destruct (check_empty_node s1 n); try discriminate. + inv H. simpl. apply PTree.gss. Qed. +Hint Resolve update_instr_at: rtlg. (** Properties of [new_reg]. *) @@ -819,76 +755,84 @@ Inductive tr_switch its value is deposited in register [rret]. *) Inductive tr_stmt (c: code) (map: mapping): - stmt -> node -> node -> list node -> node -> option reg -> Prop := - | tr_Sskip: forall ns nexits nret rret, - tr_stmt c map Sskip ns ns nexits nret rret - | tr_Sassign: forall id a ns nd nexits nret rret rt n, + stmt -> node -> node -> list node -> labelmap -> node -> option reg -> Prop := + | tr_Sskip: forall ns nexits ngoto nret rret, + tr_stmt c map Sskip ns ns nexits ngoto nret rret + | tr_Sassign: forall id a ns nd nexits ngoto nret rret rt n, tr_expr c map nil a ns n rt -> tr_store_var c map rt id n nd -> - tr_stmt c map (Sassign id a) ns nd nexits nret rret - | tr_Sstore: forall chunk addr al b ns nd nexits nret rret rd n1 rl n2, + tr_stmt c map (Sassign id a) ns nd nexits ngoto nret rret + | tr_Sstore: forall chunk addr al b ns nd nexits ngoto nret rret rd n1 rl n2, tr_exprlist c map nil al ns n1 rl -> tr_expr c map rl b n1 n2 rd -> c!n2 = Some (Istore chunk addr rl rd nd) -> - tr_stmt c map (Sstore chunk addr al b) ns nd nexits nret rret - | tr_Scall: forall optid sig b cl ns nd nexits nret rret rd n1 rf n2 n3 rargs, + tr_stmt c map (Sstore chunk addr al b) ns nd nexits ngoto nret rret + | tr_Scall: forall optid sig b cl ns nd nexits ngoto nret rret rd n1 rf n2 n3 rargs, tr_expr c map nil b ns n1 rf -> tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> c!n2 = Some (Icall sig (inl _ rf) rargs rd n3) -> tr_store_optvar c map rd optid n3 nd -> ~reg_in_map map rd -> - tr_stmt c map (Scall optid sig b cl) ns nd nexits nret rret - | tr_Salloc: forall id a ns nd nexits nret rret rd n1 n2 r, + tr_stmt c map (Scall optid sig b cl) ns nd nexits ngoto nret rret + | tr_Stailcall: forall sig b cl ns nd nexits ngoto nret rret n1 rf n2 rargs, + tr_expr c map nil b ns n1 rf -> + 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_Salloc: forall id a ns nd nexits ngoto nret rret rd n1 n2 r, tr_expr c map nil a ns n1 r -> c!n1 = Some (Ialloc r rd n2) -> tr_store_var c map rd id n2 nd -> ~reg_in_map map rd -> - tr_stmt c map (Salloc id a) ns nd nexits nret rret - | tr_Sseq: forall s1 s2 ns nd nexits nret rret n, - tr_stmt c map s2 n nd nexits nret rret -> - tr_stmt c map s1 ns n nexits nret rret -> - tr_stmt c map (Sseq s1 s2) ns nd nexits nret rret - | tr_Sifthenelse: forall a strue sfalse ns nd nexits nret rret ntrue nfalse, - tr_stmt c map strue ntrue nd nexits nret rret -> - tr_stmt c map sfalse nfalse nd nexits nret rret -> + tr_stmt c map (Salloc id a) 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 -> + tr_stmt c map (Sseq s1 s2) ns nd nexits ngoto nret rret + | tr_Sifthenelse: forall a strue sfalse ns nd nexits ngoto nret rret ntrue nfalse, + tr_stmt c map strue ntrue nd nexits ngoto nret rret -> + tr_stmt c map sfalse nfalse nd nexits ngoto nret rret -> tr_condition c map nil a ns ntrue nfalse -> - tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits nret rret - | tr_Sloop: forall sbody ns nd nexits nret rret nloop, - tr_stmt c map sbody ns nloop nexits nret rret -> - c!nloop = Some(Inop ns) -> - tr_stmt c map (Sloop sbody) ns nd nexits nret rret - | tr_Sblock: forall sbody ns nd nexits nret rret, - tr_stmt c map sbody ns nd (nd :: nexits) nret rret -> - tr_stmt c map (Sblock sbody) ns nd nexits nret rret - | tr_Sexit: forall n ns nd nexits nret rret, + tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret + | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop, + tr_stmt c map sbody nloop ns nexits ngoto nret rret -> + c!ns = Some(Inop nloop) -> + tr_stmt c map (Sloop sbody) ns nd nexits ngoto nret rret + | tr_Sblock: forall sbody ns nd nexits ngoto nret rret, + tr_stmt c map sbody ns nd (nd :: nexits) ngoto nret rret -> + tr_stmt c map (Sblock sbody) ns nd nexits ngoto nret rret + | tr_Sexit: forall n ns nd nexits ngoto nret rret, nth_error nexits n = Some ns -> - tr_stmt c map (Sexit n) ns nd nexits nret rret - | tr_Sswitch: forall a cases default ns nd nexits nret rret n r t, + tr_stmt c map (Sexit n) ns nd nexits ngoto nret rret + | tr_Sswitch: forall a cases default ns nd nexits ngoto nret rret n r t, validate_switch default cases t = true -> tr_expr c map nil a ns n r -> tr_switch c r nexits t n -> - tr_stmt c map (Sswitch a cases default) ns nd nexits nret rret - | tr_Sreturn_none: forall nret nd nexits, - tr_stmt c map (Sreturn None) nret nd nexits nret None - | tr_Sreturn_some: forall a ns nd nexits nret rret, + tr_stmt c map (Sswitch a cases default) ns nd nexits ngoto nret rret + | tr_Sreturn_none: forall nret nd nexits ngoto, + tr_stmt c map (Sreturn None) nret nd nexits ngoto nret None + | tr_Sreturn_some: forall a ns nd nexits ngoto nret rret, tr_expr c map nil a ns nret rret -> - tr_stmt c map (Sreturn (Some a)) ns nd nexits nret (Some rret) - | tr_Stailcall: forall sig b cl ns nd nexits nret rret n1 rf n2 rargs, - tr_expr c map nil b ns n1 rf -> - 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 nret rret. + tr_stmt c map (Sreturn (Some a)) ns nd nexits ngoto nret (Some rret) + | tr_Slabel: forall lbl s ns nd nexits ngoto nret rret n, + ngoto!lbl = Some n -> + c!n = Some (Inop ns) -> + tr_stmt c map s ns nd nexits ngoto nret rret -> + tr_stmt c map (Slabel lbl s) ns nd nexits ngoto nret rret + | tr_Sgoto: forall lbl ns nd nexits ngoto nret rret, + ngoto!lbl = Some ns -> + tr_stmt c map (Sgoto lbl) ns nd nexits ngoto nret rret. (** [tr_function f tf] specifies the RTL function [tf] that [RTLgen.transl_function] returns. *) Inductive tr_function: CminorSel.function -> RTL.function -> Prop := | tr_function_intro: - forall f code rparams map1 s1 i1 rvars map2 s2 i2 nentry nret rret orret nextnode wfcode, - add_vars init_mapping f.(CminorSel.fn_params) init_state = OK (rparams, map1) s1 i1 -> + forall f code rparams map1 s0 s1 i1 rvars map2 s2 i2 nentry ngoto nret rret orret nextnode wfcode, + add_vars init_mapping f.(CminorSel.fn_params) s0 = OK (rparams, map1) s1 i1 -> add_vars map1 f.(CminorSel.fn_vars) s1 = OK (rvars, map2) s2 i2 -> orret = ret_reg f.(CminorSel.fn_sig) rret -> - tr_stmt code map2 f.(CminorSel.fn_body) nentry nret nil nret orret -> + tr_stmt code map2 f.(CminorSel.fn_body) nentry nret nil ngoto nret orret -> code!nret = Some(Ireturn orret) -> tr_function f (RTL.mkfunction f.(CminorSel.fn_sig) @@ -918,18 +862,17 @@ Definition tr_expr_condition_exprlist_ind3 (conj (tr_condition_ind3 c P P0 P1 a b c' d e f g h i j k l) (tr_exprlist_ind3 c P P0 P1 a b c' d e f g h i j k l)). -Lemma tr_move_extends: - forall s1 s2, state_extends s1 s2 -> +Lemma tr_move_incr: + forall s1 s2, state_incr s1 s2 -> forall ns rs nd rd, tr_move s1.(st_code) ns rs nd rd -> tr_move s2.(st_code) ns rs nd rd. Proof. - induction 2; econstructor; eauto. - eapply instr_at_extends; eauto. + induction 2; econstructor; eauto with rtlg. Qed. -Lemma tr_expr_condition_exprlist_extends: - forall s1 s2, state_extends s1 s2 -> +Lemma tr_expr_condition_exprlist_incr: + forall s1 s2, state_incr s1 s2 -> (forall map pr a ns nd rd, tr_expr s1.(st_code) map pr a ns nd rd -> tr_expr s2.(st_code) map pr a ns nd rd) @@ -941,10 +884,10 @@ Lemma tr_expr_condition_exprlist_extends: tr_exprlist s2.(st_code) map pr al ns nd rl). Proof. intros s1 s2 EXT. - pose (AT := fun pc i => instr_at_extends s1 s2 pc i EXT). + pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). apply tr_expr_condition_exprlist_ind3; intros; econstructor; eauto. - eapply tr_move_extends; eauto. - eapply tr_move_extends; eauto. + eapply tr_move_incr; eauto. + eapply tr_move_incr; eauto. Qed. Lemma tr_expr_incr: @@ -954,8 +897,8 @@ Lemma tr_expr_incr: tr_expr s2.(st_code) map pr a ns nd rd. Proof. intros. - exploit tr_expr_condition_exprlist_extends. - apply state_incr_extends; eauto. intros [A [B C]]. eauto. + exploit tr_expr_condition_exprlist_incr; eauto. + intros [A [B C]]. eauto. Qed. Lemma tr_condition_incr: @@ -965,8 +908,8 @@ Lemma tr_condition_incr: tr_condition s2.(st_code) map pr a ns ntrue nfalse. Proof. intros. - exploit tr_expr_condition_exprlist_extends. - apply state_incr_extends; eauto. intros [A [B C]]. eauto. + exploit tr_expr_condition_exprlist_incr; eauto. + intros [A [B C]]. eauto. Qed. Lemma tr_exprlist_incr: @@ -976,8 +919,8 @@ Lemma tr_exprlist_incr: tr_exprlist s2.(st_code) map pr al ns nd rl. Proof. intros. - exploit tr_expr_condition_exprlist_extends. - apply state_incr_extends; eauto. intros [A [B C]]. eauto. + exploit tr_expr_condition_exprlist_incr; eauto. + intros [A [B C]]. eauto. Qed. Scheme expr_ind3 := Induction for expr Sort Prop @@ -1117,63 +1060,51 @@ Proof. intros. eapply B; eauto with rtlg. Qed. -Lemma tr_store_var_extends: - forall s1 s2, state_extends s1 s2 -> +Lemma tr_store_var_incr: + forall s1 s2, state_incr s1 s2 -> forall map rs id ns nd, tr_store_var s1.(st_code) map rs id ns nd -> tr_store_var s2.(st_code) map rs id ns nd. Proof. intros. destruct H0 as [rv [A B]]. - econstructor; split. eauto. eapply tr_move_extends; eauto. + econstructor; split. eauto. eapply tr_move_incr; eauto. Qed. -Lemma tr_store_optvar_extends: - forall s1 s2, state_extends s1 s2 -> +Lemma tr_store_optvar_incr: + forall s1 s2, state_incr s1 s2 -> forall map rs optid ns nd, tr_store_optvar s1.(st_code) map rs optid ns nd -> tr_store_optvar s2.(st_code) map rs optid ns nd. Proof. intros until nd. destruct optid; simpl. - apply tr_store_var_extends; auto. + apply tr_store_var_incr; auto. auto. Qed. -Lemma tr_switch_extends: - forall s1 s2, state_extends s1 s2 -> +Lemma tr_switch_incr: + forall s1 s2, state_incr s1 s2 -> forall r nexits t ns, tr_switch s1.(st_code) r nexits t ns -> tr_switch s2.(st_code) r nexits t ns. Proof. induction 2; econstructor; eauto with rtlg. - eapply instr_at_extends; eauto. - eapply instr_at_extends; eauto. -Qed. - -Lemma tr_stmt_extends: - forall s1 s2, state_extends s1 s2 -> - forall map s ns nd nexits nret rret, - tr_stmt s1.(st_code) map s ns nd nexits nret rret -> - tr_stmt s2.(st_code) map s ns nd nexits nret rret. -Proof. - intros s1 s2 EXT. - destruct (tr_expr_condition_exprlist_extends s1 s2 EXT) as [A [B C]]. - pose (AT := fun pc i => instr_at_extends s1 s2 pc i EXT). - pose (STV := tr_store_var_extends s1 s2 EXT). - pose (STOV := tr_store_optvar_extends s1 s2 EXT). - induction 1; econstructor; eauto. - eapply tr_switch_extends; eauto. Qed. Lemma tr_stmt_incr: forall s1 s2, state_incr s1 s2 -> - forall map s ns nd nexits nret rret, - tr_stmt s1.(st_code) map s ns nd nexits nret rret -> - tr_stmt s2.(st_code) map s ns nd nexits nret rret. + forall map s ns nd nexits ngoto nret rret, + tr_stmt s1.(st_code) map s ns nd nexits ngoto nret rret -> + tr_stmt s2.(st_code) map s ns nd nexits ngoto nret rret. Proof. - intros. eapply tr_stmt_extends; eauto with rtlg. + intros s1 s2 EXT. + destruct (tr_expr_condition_exprlist_incr s1 s2 EXT) as [A [B C]]. + pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). + pose (STV := tr_store_var_incr s1 s2 EXT). + pose (STOV := tr_store_optvar_incr s1 s2 EXT). + induction 1; econstructor; eauto. + eapply tr_switch_incr; eauto. Qed. - Lemma store_var_charact: forall map rs id nd s ns s' incr, store_var map rs id nd s = OK ns s' incr -> @@ -1215,27 +1146,27 @@ Proof. monadInv H. exploit transl_exit_charact; eauto. intros [A B]. subst s1. econstructor; eauto with rtlg. - apply tr_switch_extends with s0; eauto with rtlg. + apply tr_switch_incr with s0; eauto with rtlg. monadInv H. econstructor; eauto with rtlg. - apply tr_switch_extends with s1; eauto with rtlg. - apply tr_switch_extends with s0; eauto with rtlg. + apply tr_switch_incr with s1; eauto with rtlg. + apply tr_switch_incr with s0; eauto with rtlg. Qed. Lemma transl_stmt_charact: - forall map stmt nd nexits nret rret s ns s' INCR - (TR: transl_stmt map stmt nd nexits nret rret s = OK ns s' INCR) + forall map stmt nd nexits ngoto nret rret s ns s' INCR + (TR: transl_stmt map stmt nd nexits ngoto nret rret s = OK ns s' INCR) (WF: map_valid map s) (OK: return_reg_ok s map rret), - tr_stmt s'.(st_code) map stmt ns nd nexits nret rret. + tr_stmt s'.(st_code) map stmt ns nd nexits ngoto nret rret. Proof. induction stmt; intros; simpl in TR; try (monadInv TR). (* Sskip *) constructor. (* Sassign *) econstructor. eapply transl_expr_charact; eauto with rtlg. - apply tr_store_var_extends with s1; auto with rtlg. + apply tr_store_var_incr with s1; auto with rtlg. eapply store_var_charact; eauto. (* Sstore *) destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]]. @@ -1256,12 +1187,20 @@ Proof. apply regs_valid_incr with s1; eauto with rtlg. apply regs_valid_cons; eauto with rtlg. apply regs_valid_incr with s2; eauto with rtlg. - apply tr_store_optvar_extends with s4; eauto with rtlg. + apply tr_store_optvar_incr with s4; eauto with rtlg. eapply store_optvar_charact; eauto with rtlg. + (* Stailcall *) + destruct transl_expr_condexpr_list_charact as [A [B C]]. + assert (RV: regs_valid (x :: nil) s1). + apply regs_valid_cons; eauto with rtlg. + econstructor; eauto with rtlg. + eapply A; eauto with rtlg. + apply tr_exprlist_incr with s4; auto. + eapply C; eauto with rtlg. (* Salloc *) econstructor; eauto with rtlg. eapply transl_expr_charact; eauto with rtlg. - apply tr_store_var_extends with s2; eauto with rtlg. + apply tr_store_var_incr with s2; eauto with rtlg. eapply store_var_charact; eauto with rtlg. (* Sseq *) econstructor. @@ -1283,12 +1222,10 @@ Proof. eapply IHstmt2; eauto with rtlg. eapply transl_condexpr_charact; eauto with rtlg. (* Sloop *) - exploit add_loop_inversion; eauto. - intros [nloop [s2 [s3 [INCR23 [INCR02 [EQ [EXT CODEAT]]]]]]]. econstructor. - apply tr_stmt_extends with s3; auto. - eapply IHstmt; eauto with rtlg. - auto. + apply tr_stmt_incr with s1; auto. + eapply IHstmt; eauto with rtlg. + eauto with rtlg. (* Sblock *) econstructor. eapply IHstmt; eauto with rtlg. @@ -1302,7 +1239,7 @@ Proof. monadInv TR. econstructor; eauto with rtlg. eapply transl_expr_charact; eauto with rtlg. - apply tr_switch_extends with s1; auto with rtlg. + apply tr_switch_incr with s1; auto with rtlg. eapply transl_switch_charact; eauto with rtlg. monadInv TR. (* Sreturn *) @@ -1312,14 +1249,15 @@ Proof. eapply transl_expr_charact; eauto with rtlg. constructor. auto. simpl; tauto. constructor. - (* Stailcall *) - destruct transl_expr_condexpr_list_charact as [A [B C]]. - assert (RV: regs_valid (x :: nil) s1). - apply regs_valid_cons; eauto with rtlg. - econstructor; eauto with rtlg. - eapply A; eauto with rtlg. - apply tr_exprlist_incr with s4; auto. - eapply C; eauto with rtlg. + (* Slabel *) + generalize EQ0; clear EQ0. case_eq (ngoto!l); intros; monadInv EQ0. + generalize EQ1; clear EQ1. unfold handle_error. + case_eq (update_instr n (Inop ns) s0); intros; inv EQ1. + econstructor. eauto. eauto with rtlg. + eapply tr_stmt_incr with s0; eauto with rtlg. + (* Sgoto *) + generalize TR; clear TR. case_eq (ngoto!l); intros; monadInv TR. + econstructor. auto. Qed. Lemma transl_function_charact: @@ -1327,8 +1265,10 @@ Lemma transl_function_charact: transl_function f = Errors.OK tf -> tr_function f tf. Proof. - intros until tf. unfold transl_function. - caseEq (transl_fun f init_state). congruence. + intros until tf. unfold transl_function. + caseEq (reserve_labels (fn_body f) (PTree.empty node, init_state)). + intros ngoto s0 RESERVE. + caseEq (transl_fun f ngoto s0). congruence. intros [nentry rparams] sfinal INCR TR E. inv E. monadInv TR. exploit add_vars_valid. eexact EQ. apply init_mapping_valid. diff --git a/backend/Selection.v b/backend/Selection.v index a55b1918..6554e429 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -1153,6 +1153,8 @@ Fixpoint sel_stmt (s: Cminor.stmt) : stmt := | 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) + | Cminor.Stailcall sg fn args => + Stailcall sg (sel_expr fn) (sel_exprlist args) | Cminor.Salloc id b => Salloc id (sel_expr b) | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2) | Cminor.Sifthenelse e ifso ifnot => @@ -1164,8 +1166,8 @@ Fixpoint sel_stmt (s: Cminor.stmt) : stmt := | 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.Stailcall sg fn args => - Stailcall sg (sel_expr fn) (sel_exprlist args) + | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body) + | Cminor.Sgoto lbl => Sgoto lbl end. (** Conversion of functions and programs. *) diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 8b4713db..bd4dd233 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -21,6 +21,7 @@ Require Import Values. Require Import Mem. Require Import Events. Require Import Globalenvs. +Require Import Smallstep. Require Import Cminor. Require Import Op. Require Import CminorSel. @@ -1060,17 +1061,18 @@ Proof. Qed. Lemma eval_store: - forall chunk a1 a2 v1 v2 m', + forall chunk a1 a2 v1 v2 f k m', eval_expr ge sp e m nil a1 v1 -> eval_expr ge sp e m nil a2 v2 -> Mem.storev chunk m v1 v2 = Some m' -> - exec_stmt ge sp e m (store chunk a1 a2) E0 e m' Out_normal. + step ge (State f (store chunk a1 a2) k sp e m) + E0 (State f Sskip k sp e m'). Proof. intros. generalize H1; destruct v1; simpl; intro; try discriminate. unfold store. generalize (eval_addressing _ _ _ _ _ H (refl_equal _)). destruct (addressing a1). intros [vl [EV EQ]]. - eapply exec_Sstore; eauto. + eapply step_store; eauto. Qed. (** * Correctness of instruction selection for operators *) @@ -1241,144 +1243,149 @@ Hint Resolve sel_exprlist_correct: evalexpr. (** Semantic preservation for terminating function calls and statements. *) -Definition eval_funcall_exec_stmt_ind2 - (P1 : mem -> Cminor.fundef -> list val -> trace -> mem -> val -> Prop) - (P2 : val -> env -> mem -> Cminor.stmt -> trace -> env -> mem -> outcome -> Prop) := - fun a b c d e f g h i j k l m n o p q r => - conj (Cminor.eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r) - (Cminor.exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r). - -Lemma sel_function_stmt_correct: - (forall m fd vargs t m' vres, - Cminor.eval_funcall ge m fd vargs t m' vres -> - CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres) - /\ (forall sp e m s t e' m' out, - Cminor.exec_stmt ge sp e m s t e' m' out -> - CminorSel.exec_stmt tge sp e m (sel_stmt s) t e' m' out). +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.Kblock k1 => Kblock (sel_cont k1) + | Cminor.Kcall id f sp e k1 => + Kcall id (sel_function 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 -> + k' = sel_cont k -> + match_states + (Cminor.State f s k sp e m) + (State (sel_function 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) + | match_returnstate: forall v k k' m, + k' = sel_cont k -> + match_states + (Cminor.Returnstate v k m) + (Returnstate v k' m). + +Remark call_cont_commut: + forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k). Proof. - apply eval_funcall_exec_stmt_ind2; intros; simpl. - (* Internal function *) - econstructor; eauto. - (* External function *) - econstructor; eauto. - (* Sskip *) - constructor. - (* Sassign *) - econstructor; eauto with evalexpr. - (* Sstore *) - eapply eval_store; eauto with evalexpr. - (* Scall *) - econstructor; eauto with evalexpr. - apply functions_translated; auto. - rewrite <- H2. apply sig_function_translated. - (* Salloc *) - econstructor; eauto with evalexpr. - (* Sifthenelse *) - econstructor; eauto with evalexpr. - eapply eval_condition_of_expr; eauto with evalexpr. - destruct b; auto. - (* Sseq *) - eapply exec_Sseq_continue; eauto. - eapply exec_Sseq_stop; eauto. - (* Sloop *) - eapply exec_Sloop_loop; eauto. - eapply exec_Sloop_stop; eauto. - (* Sblock *) - econstructor; eauto. - (* Sexit *) - constructor. - (* Sswitch *) - econstructor; eauto with evalexpr. - (* Sreturn *) - constructor. - econstructor; eauto with evalexpr. - (* Stailcall *) - econstructor; eauto with evalexpr. - apply functions_translated; auto. - rewrite <- H2. apply sig_function_translated. + induction k; simpl; auto. Qed. -Lemma sel_function_correct: - forall m fd vargs t m' vres, - Cminor.eval_funcall ge m fd vargs t m' vres -> - CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres. -Proof (proj1 sel_function_stmt_correct). - -Lemma sel_stmt_correct: - forall sp e m s t e' m' out, - Cminor.exec_stmt ge sp e m s t e' m' out -> - CminorSel.exec_stmt tge sp e m (sel_stmt s) t e' m' out. -Proof (proj2 sel_function_stmt_correct). - -Hint Resolve sel_stmt_correct: evalexpr. - -(** Semantic preservation for diverging function calls and statements. *) +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))) + (Cminor.find_label lbl s k). +Proof. + induction s; intros; simpl; auto. + unfold store. destruct (addressing (sel_expr e)); auto. + change (Kseq (sel_stmt 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)) + with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)). + auto. + change (Kblock (sel_cont k)) + with (sel_cont (Cminor.Kblock k)). + auto. + destruct o; auto. + destruct (ident_eq lbl l); auto. +Qed. -Lemma sel_function_divergence_correct: - forall m fd vargs t, - Cminor.evalinf_funcall ge m fd vargs t -> - CminorSel.evalinf_funcall tge m (sel_fundef fd) vargs t. +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. Proof. - cofix FUNCALL. - assert (STMT: forall sp e m s t, - Cminor.execinf_stmt ge sp e m s t -> - CminorSel.execinf_stmt tge sp e m (sel_stmt s) t). - cofix STMT; intros. - inversion H; subst; simpl. - (* Call *) + induction 1; intros T1 ME; inv ME; simpl; + try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail). + + (* skip call *) + econstructor; split. + econstructor. destruct k; simpl in H; simpl; auto. + rewrite <- H0; reflexivity. + 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. + eapply eval_store; eauto with evalexpr. + constructor; auto. + (* Scall *) + econstructor; split. econstructor; eauto with evalexpr. - apply functions_translated; auto. + apply functions_translated; eauto. apply sig_function_translated. - (* Ifthenelse *) - econstructor; eauto with evalexpr. - eapply eval_condition_of_expr; eauto with evalexpr. - destruct b; eapply STMT; eauto. - (* Seq *) - apply execinf_Sseq_1; eauto. - eapply execinf_Sseq_2; eauto with evalexpr. - (* Loop *) - eapply execinf_Sloop_body; eauto. - eapply execinf_Sloop_loop; eauto with evalexpr. - change (Sloop (sel_stmt s0)) with (sel_stmt (Cminor.Sloop s0)). - apply STMT. auto. - (* Block *) - apply execinf_Sblock; eauto. - (* Tailcall *) + constructor; auto. + (* Stailcall *) + econstructor; split. econstructor; eauto with evalexpr. - apply functions_translated; auto. + apply functions_translated; eauto. apply sig_function_translated. - - intros. inv H; simpl. - (* Internal functions *) + constructor; auto. apply call_cont_commut. + (* Salloc *) + exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id (Vptr b Int.zero) e) m'); split. econstructor; eauto with evalexpr. - unfold sel_function; simpl. eapply STMT; eauto. -Qed. + constructor; auto. + (* Sifthenelse *) + exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt 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. + econstructor. rewrite <- H; reflexivity. + constructor; auto. apply call_cont_commut. + (* Sreturn Some *) + econstructor; split. + econstructor. simpl. auto. eauto with evalexpr. + constructor; auto. apply call_cont_commut. + (* Sgoto *) + econstructor; split. + econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut. + rewrite H. simpl. reflexivity. + constructor; auto. +Qed. -End PRESERVATION. +Lemma sel_initial_states: + forall S, Cminor.initial_state prog S -> + exists R, initial_state tprog R /\ match_states S R. +Proof. + induction 1. + econstructor; split. + econstructor. + simpl. fold tge. rewrite symbols_preserved. eexact H. + apply function_ptr_translated. eauto. + rewrite <- H1. apply sig_function_translated; auto. + unfold tprog, sel_program. rewrite Genv.init_mem_transf. + constructor; auto. +Qed. -(** As a corollary, instruction selection preserves the observable - behaviour of programs. *) +Lemma sel_final_states: + forall S R r, + match_states S R -> Cminor.final_state S r -> final_state R r. +Proof. + intros. inv H0. inv H. simpl. constructor. +Qed. -Theorem sel_program_correct: - forall prog beh, - Cminor.exec_program prog beh -> - CminorSel.exec_program (sel_program prog) beh. +Theorem transf_program_correct: + forall (beh: program_behavior), + Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. Proof. - intros. inv H. - (* Terminating *) - apply program_terminates with b (sel_fundef f) m. - simpl. rewrite <- H0. unfold ge. apply symbols_preserved. - apply function_ptr_translated. auto. - rewrite <- H2. apply sig_function_translated. - replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog). - apply sel_function_correct; auto. - symmetry. unfold sel_program. apply Genv.init_mem_transf. - (* Diverging *) - apply program_diverges with b (sel_fundef f). - simpl. rewrite <- H0. unfold ge. apply symbols_preserved. - apply function_ptr_translated. auto. - rewrite <- H2. apply sig_function_translated. - replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog). - apply sel_function_divergence_correct; auto. - symmetry. unfold sel_program. apply Genv.init_mem_transf. + unfold CminorSel.exec_program, Cminor.exec_program; intros. + eapply simulation_step_preservation; eauto. + eexact sel_initial_states. + eexact sel_final_states. + exact sel_step_correct. Qed. + +End PRESERVATION. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index a6038758..9dfb5732 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -2461,7 +2461,7 @@ Theorem transl_program_correct: Csharpminor.exec_program prog beh -> exec_program tprog beh. Proof. - intros. + intros. apply exec_program_bigstep_transition. set (m0 := Genv.init_mem prog) in *. set (f := meminj_init m0). assert (MINJ0: mem_inject f m0 m0). diff --git a/common/Main.v b/common/Main.v index e5f6280c..f50640ae 100644 --- a/common/Main.v +++ b/common/Main.v @@ -283,8 +283,8 @@ Proof. destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]]. generalize (transform_partial_program_identity _ _ _ _ H1). clear H1. intro. subst p1. apply transf_rtl_program_correct with p3. auto. - apply RTLgenproof.transl_program_correct with p2; auto. - rewrite <- P1. apply Selectionproof.sel_program_correct; auto. + apply RTLgenproof.transf_program_correct with p2; auto. + rewrite <- P1. apply Selectionproof.transf_program_correct; auto. Qed. Theorem transf_c_program_correct: diff --git a/common/Smallstep.v b/common/Smallstep.v index ec7a416d..a2634be1 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -19,6 +19,8 @@ the one-step transition relations that are used to specify operational semantics in small-step style. *) +Require Import Wf. +Require Import Wf_nat. Require Import Coqlib. Require Import AST. Require Import Events. @@ -157,7 +159,8 @@ Proof. Qed. Lemma plus_inv: - forall ge s1 t s2, plus ge s1 t s2 -> + forall ge s1 t s2, + plus ge s1 t s2 -> step ge s1 t s2 \/ exists s', exists t1, exists t2, step ge s1 t1 s' /\ plus ge s' t2 s2 /\ t = t1 ** t2. Proof. intros. inversion H; subst. inversion H1; subst. @@ -166,6 +169,14 @@ Proof. split. econstructor; eauto. auto. Qed. +Lemma star_inv: + forall ge s1 t s2, + star ge s1 t s2 -> + (s2 = s1 /\ t = E0) \/ plus ge s1 t s2. +Proof. + intros. inv H. left; auto. right; econstructor; eauto. +Qed. + (** Infinitely many transitions *) CoInductive forever (ge: genv): state -> traceinf -> Prop := @@ -186,61 +197,86 @@ Qed. (** An alternate, equivalent definition of [forever] that is useful for coinductive reasoning. *) -CoInductive forever_N (ge: genv): nat -> state -> traceinf -> Prop := - | forever_N_star: forall s1 t s2 p q T1 T2, +Variable A: Set. +Variable order: A -> A -> Prop. + +CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop := + | forever_N_star: forall s1 t s2 a1 a2 T1 T2, star ge s1 t s2 -> - (p < q)%nat -> - forever_N ge p s2 T2 -> + order a2 a1 -> + forever_N ge a2 s2 T2 -> T1 = t *** T2 -> - forever_N ge q s1 T1 - | forever_N_plus: forall s1 t s2 p q T1 T2, + forever_N ge a1 s1 T1 + | forever_N_plus: forall s1 t s2 a1 a2 T1 T2, plus ge s1 t s2 -> - forever_N ge p s2 T2 -> + forever_N ge a2 s2 T2 -> T1 = t *** T2 -> - forever_N ge q s1 T1. + forever_N ge a1 s1 T1. -Remark Peano_induction: - forall (P: nat -> Prop), - (forall p, (forall q, (q < p)%nat -> P q) -> P p) -> - forall p, P p. -Proof. - intros P IH. - assert (forall p, forall q, (q < p)%nat -> P q). - induction p; intros. elimtype False; omega. - apply IH. intros. apply IHp. omega. - intro. apply H with (S p). omega. -Qed. +Hypothesis order_wf: well_founded order. Lemma forever_N_inv: - forall ge p s T, - forever_N ge p s T -> - exists t, exists s', exists q, exists T', - step ge s t s' /\ forever_N ge q s' T' /\ T = t *** T'. + forall ge a s T, + forever_N ge a s T -> + exists t, exists s', exists a', exists T', + step ge s t s' /\ forever_N ge a' s' T' /\ T = t *** T'. Proof. - intros ge p. pattern p. apply Peano_induction; intros. - inv H0. + intros ge a0. pattern a0. apply (well_founded_ind order_wf). + intros. inv H0. (* star case *) inv H1. (* no transition *) - change (E0 *** T2) with T2. apply H with p1. auto. auto. + change (E0 *** T2) with T2. apply H with a2. auto. auto. (* at least one transition *) - exists t1; exists s0; exists p0; exists (t2 *** T2). + exists t1; exists s0; exists x; exists (t2 *** T2). split. auto. split. eapply forever_N_star; eauto. apply Eappinf_assoc. (* plus case *) inv H1. - exists t1; exists s0; exists (S p1); exists (t2 *** T2). - split. auto. split. eapply forever_N_star; eauto. + exists t1; exists s0; exists a2; exists (t2 *** T2). + split. auto. + split. inv H3. auto. + eapply forever_N_plus. econstructor; eauto. eauto. auto. apply Eappinf_assoc. Qed. Lemma forever_N_forever: - forall ge p s T, forever_N ge p s T -> forever ge s T. + forall ge a s T, forever_N ge a s T -> forever ge s T. Proof. cofix COINDHYP; intros. - destruct (forever_N_inv H) as [t [s' [q [T' [A [B C]]]]]]. - rewrite C. apply forever_intro with s'. auto. - apply COINDHYP with q; auto. + destruct (forever_N_inv H) as [t [s' [a' [T' [P [Q R]]]]]]. + rewrite R. apply forever_intro with s'. auto. + apply COINDHYP with a'; auto. +Qed. + +(** Yet another alternative definition of [forever]. *) + +CoInductive forever_plus (ge: genv) : state -> traceinf -> Prop := + | forever_plus_intro: forall s1 t s2 T1 T2, + plus ge s1 t s2 -> + forever_plus ge s2 T2 -> + T1 = t *** T2 -> + forever_plus ge s1 T1. + +Lemma forever_plus_inv: + forall ge s T, + forever_plus ge s T -> + exists s', exists t, exists T', + step ge s t s' /\ forever_plus ge s' T' /\ T = t *** T'. +Proof. + intros. inv H. inv H0. exists s0; exists t1; exists (t2 *** T2). + split. auto. + split. exploit star_inv; eauto. intros [[P Q] | R]. + subst. simpl. auto. econstructor; eauto. + traceEq. +Qed. + +Lemma forever_plus_forever: + forall ge s T, forever_plus ge s T -> forever ge s T. +Proof. + cofix COINDHYP; intros. + destruct (forever_plus_inv H) as [s' [t [T' [P [Q R]]]]]. + subst. econstructor; eauto. Qed. (** * Outcomes for program executions *) @@ -329,19 +365,21 @@ Hypothesis match_final_states: in the source program must correspond to infinitely many transitions in the second program. *) -Section SIMULATION_STAR. +Section SIMULATION_STAR_WF. -(** [measure] is a nonnegative integer associated with states - of the first semantics. It must decrease when we take - a stuttering step. *) +(** [order] is a well-founded ordering associated with states + of the first semantics. Stuttering steps must correspond + to states that decrease w.r.t. [order]. *) -Variable measure: state1 -> nat. +Variable order: state1 -> state1 -> Prop. +Hypothesis order_wf: well_founded order. Hypothesis simulation: forall st1 t st1', step1 ge1 st1 t st1' -> forall st2, match_states st1 st2 -> - (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') - \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat. + exists st2', + (plus step2 ge2 st2 t st2' \/ (star step2 ge2 st2 t st2' /\ order st1' st1)) + /\ match_states st1' st2'. Lemma simulation_star_star: forall st1 t st1', star step1 ge1 st1 t st1' -> @@ -350,12 +388,13 @@ Lemma simulation_star_star: Proof. induction 1; intros. exists st2; split. apply star_refl. auto. - elim (simulation H H2). - intros [st2' [A B]]. + destruct (simulation H H2) as [st2' [A B]]. destruct (IHstar _ B) as [st3' [C D]]. - exists st3'; split. apply star_trans with t1 st2' t2. - apply plus_star; auto. auto. auto. auto. - intros [A [B C]]. rewrite H1. rewrite B. simpl. apply IHstar; auto. + exists st3'; split; auto. + apply star_trans with t1 st2' t2; auto. + destruct A as [F | [F G]]. + apply plus_star; auto. + auto. Qed. Lemma simulation_star_forever: @@ -365,19 +404,19 @@ Lemma simulation_star_forever: Proof. assert (forall st1 st2 T, forever step1 ge1 st1 T -> match_states st1 st2 -> - forever_N step2 ge2 (measure st1) st2 T). + forever_N step2 order ge2 st1 st2 T). cofix COINDHYP; intros. - inversion H; subst. elim (simulation H1 H0). - intros [st2' [A B]]. apply forever_N_plus with t st2' (measure s2) T0. + inversion H; subst. + destruct (simulation H1 H0) as [st2' [A B]]. + destruct A as [C | [C D]]. + apply forever_N_plus with t st2' s2 T0. auto. apply COINDHYP. assumption. assumption. auto. - intros [A [B C]]. - apply forever_N_star with t st2 (measure s2) T0. - rewrite B. apply star_refl. auto. - apply COINDHYP. assumption. auto. auto. + apply forever_N_star with t st2' s2 T0. + auto. auto. apply COINDHYP. assumption. auto. auto. intros. eapply forever_N_forever; eauto. Qed. -Lemma simulation_star_preservation: +Lemma simulation_star_wf_preservation: forall beh, program_behaves step1 initial_state1 final_state1 ge1 beh -> program_behaves step2 initial_state2 final_state2 ge2 beh. @@ -391,6 +430,36 @@ Proof. eapply simulation_star_forever; eauto. Qed. +End SIMULATION_STAR_WF. + +Section SIMULATION_STAR. + +(** We now consider the case where we have a nonnegative integer measure + associated with states of the first semantics. It must decrease when we take + a stuttering step. *) + +Variable measure: state1 -> nat. + +Hypothesis simulation: + forall st1 t st1', step1 ge1 st1 t st1' -> + forall st2, match_states st1 st2 -> + (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') + \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat. + +Lemma simulation_star_preservation: + forall beh, + program_behaves step1 initial_state1 final_state1 ge1 beh -> + program_behaves step2 initial_state2 final_state2 ge2 beh. +Proof. + intros. + apply simulation_star_wf_preservation with (ltof _ measure). + apply well_founded_ltof. intros. + destruct (simulation H0 H1) as [[st2' [A B]] | [A [B C]]]. + exists st2'; auto. + exists st2; split. right; split. rewrite B. apply star_refl. auto. auto. + auto. +Qed. + End SIMULATION_STAR. (** Lock-step simulation: each transition in the first semantics -- cgit