summaryrefslogtreecommitdiff
path: root/backend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-07-08 12:04:42 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-07-08 12:04:42 +0000
commit611e7b09253dbbb98e9cd4ca4e07a60b50e693fd (patch)
treed784e293ec226fec40c12399816824e24a921899 /backend
parent0290650b7463088bb228bc96d3143941590b54dd (diff)
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
Diffstat (limited to 'backend')
-rw-r--r--backend/Cminor.v677
-rw-r--r--backend/CminorSel.v365
-rw-r--r--backend/RTLbigstep.v412
-rw-r--r--backend/RTLgen.v193
-rw-r--r--backend/RTLgenproof.v1126
-rw-r--r--backend/RTLgenspec.v340
-rw-r--r--backend/Selection.v6
-rw-r--r--backend/Selectionproof.v265
8 files changed, 1652 insertions, 1732 deletions
diff --git a/backend/Cminor.v b/backend/Cminor.v
index f2eb84f..910eaa4 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 3578868..60c1d57 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 182f593..0000000
--- 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 3cc0eeb..5fde3d8 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 e02463a..1074ddd 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 b8061a3..59a5dd7 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 a55b191..6554e42 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 8b4713d..bd4dd23 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.