diff options
| -rw-r--r-- | backend/Cmconstr.v | 2 | ||||
| -rw-r--r-- | backend/Cmconstrproof.v | 4 | ||||
| -rw-r--r-- | backend/Cminor.v | 85 | ||||
| -rw-r--r-- | backend/Cminorgen.v | 60 | ||||
| -rw-r--r-- | backend/Cminorgenproof.v | 173 | ||||
| -rw-r--r-- | backend/Csharpminor.v | 2 | ||||
| -rw-r--r-- | backend/RTLgen.v | 33 | ||||
| -rw-r--r-- | backend/RTLgenproof.v | 177 | ||||
| -rw-r--r-- | backend/RTLgenproof1.v | 60 |
9 files changed, 247 insertions, 349 deletions
diff --git a/backend/Cmconstr.v b/backend/Cmconstr.v index cd50e38..da642f8 100644 --- a/backend/Cmconstr.v +++ b/backend/Cmconstr.v @@ -907,5 +907,5 @@ Definition store (chunk: memory_chunk) (e1 e2: expr) := (** ** If-then-else statement *) -Definition ifthenelse (e: expr) (ifso ifnot: stmtlist) : stmt := +Definition ifthenelse (e: expr) (ifso ifnot: stmt) : stmt := Sifthenelse (condexpr_of_expr e) ifso ifnot. diff --git a/backend/Cmconstrproof.v b/backend/Cmconstrproof.v index 19b7473..b7469be 100644 --- a/backend/Cmconstrproof.v +++ b/backend/Cmconstrproof.v @@ -1128,7 +1128,7 @@ Theorem exec_ifthenelse_true: forall sp e1 m1 a e2 m2 v ifso ifnot e3 m3 out, eval_expr ge sp nil e1 m1 a e2 m2 v -> Val.is_true v -> - exec_stmtlist ge sp e2 m2 ifso e3 m3 out -> + exec_stmt ge sp e2 m2 ifso e3 m3 out -> exec_stmt ge sp e1 m1 (ifthenelse a ifso ifnot) e3 m3 out. Proof. intros. unfold ifthenelse. @@ -1141,7 +1141,7 @@ Theorem exec_ifthenelse_false: forall sp e1 m1 a e2 m2 v ifso ifnot e3 m3 out, eval_expr ge sp nil e1 m1 a e2 m2 v -> Val.is_false v -> - exec_stmtlist ge sp e2 m2 ifnot e3 m3 out -> + exec_stmt ge sp e2 m2 ifnot e3 m3 out -> exec_stmt ge sp e1 m1 (ifthenelse a ifso ifnot) e3 m3 out. Proof. intros. unfold ifthenelse. diff --git a/backend/Cminor.v b/backend/Cminor.v index f08d927..54d5552 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -52,19 +52,17 @@ with exprlist : Set := [Sblock] statements. *) Inductive stmt : Set := + | Sskip: stmt | Sexpr: expr -> stmt - | Sifthenelse: condexpr -> stmtlist -> stmtlist -> stmt - | Sloop: stmtlist -> stmt - | Sblock: stmtlist -> stmt + | Sseq: stmt -> stmt -> stmt + | Sifthenelse: condexpr -> stmt -> stmt -> stmt + | Sloop: stmt -> stmt + | Sblock: stmt -> stmt | Sexit: nat -> stmt - | Sreturn: option expr -> stmt - -with stmtlist : Set := - | Snil: stmtlist - | Scons: stmt -> stmtlist -> stmtlist. + | Sreturn: option expr -> stmt. (** Functions are composed of a signature, a list of parameter names, - a list of local variables, and a list of statements representing + a list of local variables, and a statement representing the function body. Each function can allocate a memory block of size [fn_stackspace] on entrance. This block will be deallocated automatically before the function returns. Pointers into this block @@ -75,7 +73,7 @@ Record function : Set := mkfunction { fn_params: list ident; fn_vars: list ident; fn_stackspace: Z; - fn_body: stmtlist + fn_body: stmt }. Definition program := AST.program function. @@ -261,7 +259,7 @@ with eval_funcall: forall m f vargs m1 sp e 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_stmtlist (Vptr sp Int.zero) e m1 f.(fn_body) e2 m2 out -> + exec_stmt (Vptr sp Int.zero) e m1 f.(fn_body) e2 m2 out -> outcome_result_value out f.(fn_sig).(sig_res) vres -> eval_funcall m f vargs (Mem.free m2 sp) vres @@ -273,29 +271,42 @@ with exec_stmt: val -> env -> mem -> stmt -> env -> mem -> outcome -> Prop := + | exec_Sskip: + forall sp e m, + exec_stmt sp e m Sskip e m Out_normal | exec_Sexpr: forall sp e m a e1 m1 v, eval_expr sp nil e m a e1 m1 v -> exec_stmt sp e m (Sexpr a) e1 m1 Out_normal | exec_Sifthenelse: - forall sp e m a sl1 sl2 e1 m1 v1 e2 m2 out, + forall sp e m a s1 s2 e1 m1 v1 e2 m2 out, eval_condexpr sp nil e m a e1 m1 v1 -> - exec_stmtlist sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out -> - exec_stmt sp e m (Sifthenelse a sl1 sl2) e2 m2 out + exec_stmt sp e1 m1 (if v1 then s1 else s2) e2 m2 out -> + exec_stmt sp e m (Sifthenelse a s1 s2) e2 m2 out + | exec_Sseq_continue: + forall sp e m s1 e1 m1 s2 e2 m2 out, + exec_stmt sp e m s1 e1 m1 Out_normal -> + exec_stmt sp e1 m1 s2 e2 m2 out -> + exec_stmt sp e m (Sseq s1 s2) e2 m2 out + | exec_Sseq_stop: + forall sp e m s1 s2 e1 m1 out, + exec_stmt sp e m s1 e1 m1 out -> + out <> Out_normal -> + exec_stmt sp e m (Sseq s1 s2) e1 m1 out | exec_Sloop_loop: - forall sp e m sl e1 m1 e2 m2 out, - exec_stmtlist sp e m sl e1 m1 Out_normal -> - exec_stmt sp e1 m1 (Sloop sl) e2 m2 out -> - exec_stmt sp e m (Sloop sl) e2 m2 out + forall sp e m s e1 m1 e2 m2 out, + exec_stmt sp e m s e1 m1 Out_normal -> + exec_stmt sp e1 m1 (Sloop s) e2 m2 out -> + exec_stmt sp e m (Sloop s) e2 m2 out | exec_Sloop_stop: - forall sp e m sl e1 m1 out, - exec_stmtlist sp e m sl e1 m1 out -> + forall sp e m s e1 m1 out, + exec_stmt sp e m s e1 m1 out -> out <> Out_normal -> - exec_stmt sp e m (Sloop sl) e1 m1 out + exec_stmt sp e m (Sloop s) e1 m1 out | exec_Sblock: - forall sp e m sl e1 m1 out, - exec_stmtlist sp e m sl e1 m1 out -> - exec_stmt sp e m (Sblock sl) e1 m1 (outcome_block out) + forall sp e m s e1 m1 out, + exec_stmt sp e m s e1 m1 out -> + exec_stmt sp e m (Sblock s) e1 m1 (outcome_block out) | exec_Sexit: forall sp e m n, exec_stmt sp e m (Sexit n) e m (Out_exit n) @@ -305,31 +316,7 @@ with exec_stmt: | exec_Sreturn_some: forall sp e m a e1 m1 v, eval_expr sp nil e m a e1 m1 v -> - exec_stmt sp e m (Sreturn (Some a)) e1 m1 (Out_return (Some v)) - -(** Execution of a list of statements: [exec_stmtlist ge sp e m sl e' m' out] - means that the list [sl] of statements executes sequentially - with outcome [out]. Execution stops at the first statement that - leads an outcome different from [Out_normal]. - The other parameters are as in [eval_expr]. *) - -with exec_stmtlist: - val -> - env -> mem -> stmtlist -> - env -> mem -> outcome -> Prop := - | exec_Snil: - forall sp e m, - exec_stmtlist sp e m Snil e m Out_normal - | exec_Scons_continue: - forall sp e m s sl e1 m1 e2 m2 out, - exec_stmt sp e m s e1 m1 Out_normal -> - exec_stmtlist sp e1 m1 sl e2 m2 out -> - exec_stmtlist sp e m (Scons s sl) e2 m2 out - | exec_Scons_stop: - forall sp e m s sl e1 m1 out, - exec_stmt sp e m s e1 m1 out -> - out <> Out_normal -> - exec_stmtlist sp e m (Scons s sl) e1 m1 out. + exec_stmt sp e m (Sreturn (Some a)) e1 m1 (Out_return (Some v)). End RELSEM. diff --git a/backend/Cminorgen.v b/backend/Cminorgen.v index 6af5260..032b287 100644 --- a/backend/Cminorgen.v +++ b/backend/Cminorgen.v @@ -231,18 +231,24 @@ with transl_exprlist (cenv: compilenv) (el: Csharpminor.exprlist) Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) {struct s}: option stmt := match s with + | Csharpminor.Sskip => + Some Sskip | Csharpminor.Sexpr e => do te <- transl_expr cenv e; Some(Sexpr te) + | Csharpminor.Sseq s1 s2 => + do ts1 <- transl_stmt cenv s1; + do ts2 <- transl_stmt cenv s2; + Some (Sseq ts1 ts2) | Csharpminor.Sifthenelse e s1 s2 => do te <- transl_expr cenv e; - do ts1 <- transl_stmtlist cenv s1; - do ts2 <- transl_stmtlist cenv s2; + do ts1 <- transl_stmt cenv s1; + do ts2 <- transl_stmt cenv s2; Some (Cmconstr.ifthenelse te ts1 ts2) | Csharpminor.Sloop s => - do ts <- transl_stmtlist cenv s; + do ts <- transl_stmt cenv s; Some (Sloop ts) | Csharpminor.Sblock s => - do ts <- transl_stmtlist cenv s; + do ts <- transl_stmt cenv s; Some (Sblock ts) | Csharpminor.Sexit n => Some (Sexit n) @@ -251,16 +257,6 @@ Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) | Csharpminor.Sreturn (Some e) => do te <- transl_expr cenv e; Some (Sreturn (Some te)) - end - -with transl_stmtlist (cenv: compilenv) (s: Csharpminor.stmtlist) - {struct s}: option stmtlist := - match s with - | Csharpminor.Snil => Some Snil - | Csharpminor.Scons s1 s2 => - do ts1 <- transl_stmt cenv s1; - do ts2 <- transl_stmtlist cenv s2; - Some (Scons ts1 ts2) end. (** Computation of the set of variables whose address is taken in @@ -296,22 +292,18 @@ with addr_taken_exprlist (e: Csharpminor.exprlist): Identset.t := Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := match s with + | Csharpminor.Sskip => Identset.empty | Csharpminor.Sexpr e => addr_taken_expr e + | Csharpminor.Sseq s1 s2 => + Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2) | Csharpminor.Sifthenelse e s1 s2 => Identset.union (addr_taken_expr e) - (Identset.union (addr_taken_stmtlist s1) (addr_taken_stmtlist s2)) - | Csharpminor.Sloop s => addr_taken_stmtlist s - | Csharpminor.Sblock s => addr_taken_stmtlist s + (Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2)) + | Csharpminor.Sloop s => addr_taken_stmt s + | Csharpminor.Sblock s => addr_taken_stmt s | Csharpminor.Sexit n => Identset.empty | Csharpminor.Sreturn None => Identset.empty | Csharpminor.Sreturn (Some e) => addr_taken_expr e - end - -with addr_taken_stmtlist (s: Csharpminor.stmtlist): Identset.t := - match s with - | Csharpminor.Snil => Identset.empty - | Csharpminor.Scons s1 s2 => - Identset.union (addr_taken_stmt s1) (addr_taken_stmtlist s2) end. (** Layout of the Cminor stack data block and construction of the @@ -351,7 +343,7 @@ Fixpoint assign_variables Definition build_compilenv (f: Csharpminor.function) : compilenv * Z := assign_variables - (addr_taken_stmtlist f.(Csharpminor.fn_body)) + (addr_taken_stmt f.(Csharpminor.fn_body)) (fn_variables f) (PMap.init Var_global, 0). @@ -361,19 +353,19 @@ Definition build_compilenv (f: Csharpminor.function) : compilenv * Z := Fixpoint store_parameters (cenv: compilenv) (params: list (ident * memory_chunk)) - {struct params} : stmtlist := + {struct params} : stmt := match params with - | nil => Snil + | nil => Sskip | (id, chunk) :: rem => match PMap.get id cenv with | Var_local chunk => - Scons (Sexpr (Eassign id (make_cast chunk (Evar id)))) - (store_parameters cenv rem) + Sseq (Sexpr (Eassign id (make_cast chunk (Evar id)))) + (store_parameters cenv rem) | Var_stack_scalar chunk ofs => - Scons (Sexpr (make_store chunk (make_stackaddr ofs) (Evar id))) - (store_parameters cenv rem) + Sseq (Sexpr (make_store chunk (make_stackaddr ofs) (Evar id))) + (store_parameters cenv rem) | _ => - Snil (* should never happen *) + Sskip (* should never happen *) end end. @@ -385,13 +377,13 @@ Fixpoint store_parameters Definition transl_function (f: Csharpminor.function): option function := let (cenv, stacksize) := build_compilenv f in if zle stacksize Int.max_signed then - do tbody <- transl_stmtlist cenv f.(Csharpminor.fn_body); + do tbody <- transl_stmt cenv f.(Csharpminor.fn_body); Some (mkfunction (Csharpminor.fn_sig f) (Csharpminor.fn_params_names f) (Csharpminor.fn_vars_names f) stacksize - (Scons (Sblock (store_parameters cenv f.(Csharpminor.fn_params))) tbody)) + (Sseq (store_parameters cenv f.(Csharpminor.fn_params)) tbody)) else None. Definition transl_program (p: Csharpminor.program) : option program := diff --git a/backend/Cminorgenproof.v b/backend/Cminorgenproof.v index b7c7884..cefe432 100644 --- a/backend/Cminorgenproof.v +++ b/backend/Cminorgenproof.v @@ -1390,7 +1390,7 @@ Lemma store_parameters_correct: mem_inject f m1 tm1 -> match_callstack f (mkframe cenv e te1 sp lo hi :: cs) m1.(nextblock) tm1.(nextblock) m1 -> exists te2, exists tm2, - exec_stmtlist tge (Vptr sp Int.zero) + exec_stmt tge (Vptr sp Int.zero) te1 tm1 (store_parameters cenv params) te2 tm2 Out_normal /\ mem_inject f m2 tm2 @@ -1430,7 +1430,7 @@ Proof. as [te3 [tm3 [EXEC3 [MINJ3 MATCH3]]]]. exists te3; exists tm3. (* execution *) - split. apply exec_Scons_continue with te2 tm1. + split. apply exec_Sseq_continue with te2 tm1. econstructor. unfold te2. constructor. assumption. assumption. (* meminj & match_callstack *) @@ -1453,7 +1453,7 @@ Proof. H12 H6 MINJ2 MATCH2) as [te3 [tm3 [EVAL4 [MINJ3 MATCH3]]]]. exists te3; exists tm3. (* execution *) - split. apply exec_Scons_continue with te1 tm2. + split. apply exec_Sseq_continue with te1 tm2. econstructor. eauto. assumption. (* meminj & match_callstack *) @@ -1537,9 +1537,9 @@ Lemma function_entry_ok: mem_inject f m tm -> list_norepet (fn_params_names fn ++ fn_vars_names fn) -> exists f2, exists te2, exists tm2, - exec_stmtlist tge (Vptr sp Int.zero) - te tm1 (store_parameters cenv fn.(Csharpminor.fn_params)) - te2 tm2 Out_normal + exec_stmt tge (Vptr sp Int.zero) + te tm1 (store_parameters cenv fn.(Csharpminor.fn_params)) + te2 tm2 Out_normal /\ mem_inject f2 m2 tm2 /\ inject_incr f f2 /\ match_callstack f2 @@ -1713,22 +1713,11 @@ Definition exec_stmt_prop (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2. -Definition exec_stmtlist_prop - (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmtlist) (m2: mem) (out: Csharpminor.outcome): Prop := - forall cenv ts f1 te1 tm1 sp lo hi cs - (TR: transl_stmtlist cenv s = Some ts) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 - (mkframe cenv e te1 sp lo hi :: cs) - m1.(nextblock) tm1.(nextblock) m1), - exists f2, exists te2, exists tm2, exists tout, - exec_stmtlist tge (Vptr sp Int.zero) te1 tm1 ts te2 tm2 tout - /\ outcome_inject f2 out tout - /\ mem_inject f2 m2 tm2 - /\ inject_incr f1 f2 - /\ match_callstack f2 - (mkframe cenv e te2 sp lo hi :: cs) - m2.(nextblock) tm2.(nextblock) m2. +Check (eval_funcall_ind4 ge + eval_expr_prop + eval_exprlist_prop + eval_funcall_prop + exec_stmt_prop). (** There are as many cases in the inductive proof as there are evaluation rules in the Csharpminor semantics. We treat each case as a separate @@ -2051,8 +2040,8 @@ Lemma transl_funcall_correct: list_norepet (fn_params_names f ++ fn_vars_names f) -> alloc_variables empty_env m (fn_variables f) e m1 lb -> bind_parameters e m1 (Csharpminor.fn_params f) vargs m2 -> - Csharpminor.exec_stmtlist ge e m2 (Csharpminor.fn_body f) m3 out -> - exec_stmtlist_prop e m2 (Csharpminor.fn_body f) m3 out -> + Csharpminor.exec_stmt ge e m2 (Csharpminor.fn_body f) m3 out -> + exec_stmt_prop e m2 (Csharpminor.fn_body f) m3 out -> Csharpminor.outcome_result_value out (sig_res (Csharpminor.fn_sig f)) vres -> eval_funcall_prop m f vargs (free_list m3 lb) vres. Proof. @@ -2085,9 +2074,8 @@ Proof. exists f3; exists (Mem.free tm3 sp); exists tvres. (* execution *) split. rewrite <- H6; econstructor; simpl; eauto. - apply exec_Scons_continue with te2 tm2. - change Out_normal with (outcome_block Out_normal). - apply exec_Sblock. exact STOREPARAM. + apply exec_Sseq_continue with te2 tm2. + exact STOREPARAM. eexact EXECBODY. (* val_inject *) split. assumption. @@ -2105,6 +2093,15 @@ Proof. intros. elim (BLOCKS b); intros B1 B2. generalize (B2 H7). omega. Qed. +Lemma transl_stmt_Sskip_correct: + forall (e : Csharpminor.env) (m : mem), + exec_stmt_prop e m Csharpminor.Sskip m Csharpminor.Out_normal. +Proof. + intros; red; intros. monadInv TR. + exists f1; exists te1; exists tm1; exists Out_normal. + intuition. subst ts; constructor. constructor. +Qed. + Lemma transl_stmt_Sexpr_correct: forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) (m1 : mem) (v : val), @@ -2120,15 +2117,51 @@ Proof. constructor. Qed. +Lemma transl_stmt_Sseq_continue_correct: + forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt) + (m1 m2 : mem) (out : Csharpminor.outcome), + Csharpminor.exec_stmt ge e m s1 m1 Csharpminor.Out_normal -> + exec_stmt_prop e m s1 m1 Csharpminor.Out_normal -> + Csharpminor.exec_stmt ge e m1 s2 m2 out -> + exec_stmt_prop e m1 s2 m2 out -> + exec_stmt_prop e m (Csharpminor.Sseq s1 s2) m2 out. +Proof. + intros; red; intros; monadInv TR. + destruct (H0 _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) + as [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + destruct (H2 _ _ _ _ _ _ _ _ _ EQ0 MINJ2 MATCH2) + as [f3 [te3 [tm3 [tout2 [EXEC2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. + exists f3; exists te3; exists tm3; exists tout2. + intuition. subst ts; eapply exec_Sseq_continue; eauto. + inversion OINJ1. subst tout1. auto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_stmt_Sseq_stop_correct: + forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt) + (m1 : mem) (out : Csharpminor.outcome), + Csharpminor.exec_stmt ge e m s1 m1 out -> + exec_stmt_prop e m s1 m1 out -> + out <> Csharpminor.Out_normal -> + exec_stmt_prop e m (Csharpminor.Sseq s1 s2) m1 out. +Proof. + intros; red; intros; monadInv TR. + destruct (H0 _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) + as [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; exists tout1. + intuition. subst ts; eapply exec_Sseq_stop; eauto. + inversion OINJ1; subst out tout1; congruence. +Qed. + Lemma transl_stmt_Sifthenelse_true_correct: forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (sl1 sl2 : Csharpminor.stmtlist) (m1 : mem) (v1 : val) (m2 : mem) + (sl1 sl2 : Csharpminor.stmt) (m1 : mem) (v1 : val) (m2 : mem) (out : Csharpminor.outcome), Csharpminor.eval_expr ge nil e m a m1 v1 -> eval_expr_prop nil e m a m1 v1 -> Val.is_true v1 -> - Csharpminor.exec_stmtlist ge e m1 sl1 m2 out -> - exec_stmtlist_prop e m1 sl1 m2 out -> + Csharpminor.exec_stmt ge e m1 sl1 m2 out -> + exec_stmt_prop e m1 sl1 m2 out -> exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) m2 out. Proof. intros; red; intros. monadInv TR. @@ -2145,13 +2178,13 @@ Qed. Lemma transl_stmt_Sifthenelse_false_correct: forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (sl1 sl2 : Csharpminor.stmtlist) (m1 : mem) (v1 : val) (m2 : mem) + (sl1 sl2 : Csharpminor.stmt) (m1 : mem) (v1 : val) (m2 : mem) (out : Csharpminor.outcome), Csharpminor.eval_expr ge nil e m a m1 v1 -> eval_expr_prop nil e m a m1 v1 -> Val.is_false v1 -> - Csharpminor.exec_stmtlist ge e m1 sl2 m2 out -> - exec_stmtlist_prop e m1 sl2 m2 out -> + Csharpminor.exec_stmt ge e m1 sl2 m2 out -> + exec_stmt_prop e m1 sl2 m2 out -> exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) m2 out. Proof. intros; red; intros. monadInv TR. @@ -2167,10 +2200,10 @@ Proof. Qed. Lemma transl_stmt_Sloop_loop_correct: - forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmtlist) + forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) (m1 m2 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmtlist ge e m sl m1 Csharpminor.Out_normal -> - exec_stmtlist_prop e m sl m1 Csharpminor.Out_normal -> + Csharpminor.exec_stmt ge e m sl m1 Csharpminor.Out_normal -> + exec_stmt_prop e m sl m1 Csharpminor.Out_normal -> Csharpminor.exec_stmt ge e m1 (Csharpminor.Sloop sl) m2 out -> exec_stmt_prop e m1 (Csharpminor.Sloop sl) m2 out -> exec_stmt_prop e m (Csharpminor.Sloop sl) m2 out. @@ -2189,10 +2222,10 @@ Qed. Lemma transl_stmt_Sloop_exit_correct: - forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmtlist) + forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmtlist ge e m sl m1 out -> - exec_stmtlist_prop e m sl m1 out -> + Csharpminor.exec_stmt ge e m sl m1 out -> + exec_stmt_prop e m sl m1 out -> out <> Csharpminor.Out_normal -> exec_stmt_prop e m (Csharpminor.Sloop sl) m1 out. Proof. @@ -2205,10 +2238,10 @@ Proof. Qed. Lemma transl_stmt_Sblock_correct: - forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmtlist) + forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmtlist ge e m sl m1 out -> - exec_stmtlist_prop e m sl m1 out -> + Csharpminor.exec_stmt ge e m sl m1 out -> + exec_stmt_prop e m sl m1 out -> exec_stmt_prop e m (Csharpminor.Sblock sl) m1 (Csharpminor.outcome_block out). Proof. @@ -2258,51 +2291,6 @@ Proof. intuition. subst ts; econstructor; eauto. constructor; auto. Qed. -Lemma transl_stmtlist_Snil_correct: - forall (e : Csharpminor.env) (m : mem), - exec_stmtlist_prop e m Csharpminor.Snil m Csharpminor.Out_normal. -Proof. - intros; red; intros; monadInv TR. - exists f1; exists te1; exists tm1; exists Out_normal. - intuition. subst ts; constructor. constructor. -Qed. - -Lemma transl_stmtlist_Scons_2_correct: - forall (e : Csharpminor.env) (m : mem) (s : Csharpminor.stmt) - (sl : Csharpminor.stmtlist) (m1 m2 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt ge e m s m1 Csharpminor.Out_normal -> - exec_stmt_prop e m s m1 Csharpminor.Out_normal -> - Csharpminor.exec_stmtlist ge e m1 sl m2 out -> - exec_stmtlist_prop e m1 sl m2 out -> - exec_stmtlist_prop e m (Csharpminor.Scons s sl) m2 out. -Proof. - intros; red; intros; monadInv TR. - destruct (H0 _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - destruct (H2 _ _ _ _ _ _ _ _ _ EQ0 MINJ2 MATCH2) - as [f3 [te3 [tm3 [tout2 [EXEC2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. - exists f3; exists te3; exists tm3; exists tout2. - intuition. subst ts; eapply exec_Scons_continue; eauto. - inversion OINJ1. subst tout1. auto. - eapply inject_incr_trans; eauto. -Qed. - -Lemma transl_stmtlist_Scons_1_correct: - forall (e : Csharpminor.env) (m : mem) (s : Csharpminor.stmt) - (sl : Csharpminor.stmtlist) (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt ge e m s m1 out -> - exec_stmt_prop e m s m1 out -> - out <> Csharpminor.Out_normal -> - exec_stmtlist_prop e m (Csharpminor.Scons s sl) m1 out. -Proof. - intros; red; intros; monadInv TR. - destruct (H0 _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exists f2; exists te2; exists tm2; exists tout1. - intuition. subst ts; eapply exec_Scons_stop; eauto. - inversion OINJ1; subst out tout1; congruence. -Qed. - (** We conclude by an induction over the structure of the Csharpminor evaluation derivation, using the lemmas above for each case. *) @@ -2311,12 +2299,11 @@ Lemma transl_function_correct: Csharpminor.eval_funcall ge m1 f vargs m2 vres -> eval_funcall_prop m1 f vargs m2 vres. Proof - (eval_funcall_ind5 ge + (eval_funcall_ind4 ge eval_expr_prop eval_exprlist_prop eval_funcall_prop exec_stmt_prop - exec_stmtlist_prop transl_expr_Evar_correct transl_expr_Eassign_correct @@ -2333,7 +2320,10 @@ Proof transl_exprlist_Enil_correct transl_exprlist_Econs_correct transl_funcall_correct + transl_stmt_Sskip_correct transl_stmt_Sexpr_correct + transl_stmt_Sseq_continue_correct + transl_stmt_Sseq_stop_correct transl_stmt_Sifthenelse_true_correct transl_stmt_Sifthenelse_false_correct transl_stmt_Sloop_loop_correct @@ -2341,10 +2331,7 @@ Proof transl_stmt_Sblock_correct transl_stmt_Sexit_correct transl_stmt_Sreturn_none_correct - transl_stmt_Sreturn_some_correct - transl_stmtlist_Snil_correct - transl_stmtlist_Scons_2_correct - transl_stmtlist_Scons_1_correct). + transl_stmt_Sreturn_some_correct). (** The [match_globalenvs] relation holds for the global environments of the source program and the transformed program. *) diff --git a/backend/Csharpminor.v b/backend/Csharpminor.v index da73646..dee3032 100644 --- a/backend/Csharpminor.v +++ b/backend/Csharpminor.v @@ -107,7 +107,7 @@ Inductive local_variable : Set := (** Functions are composed of a signature, a list of parameter names with associated memory chunks (parameters must be scalar), a list of local variables with associated [local_variable] description, and a - list of statements representing the function body. *) + statement representing the function body. *) Record function : Set := mkfunction { fn_sig: signature; diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 9dc9660..32dd2cf 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -376,7 +376,7 @@ with transl_exprlist (map: mapping) (mut: list ident) no impact on program correctness. We delegate the choice to an external heuristic (written in OCaml), declared below. *) -Parameter more_likely: condexpr -> stmtlist -> stmtlist -> bool. +Parameter more_likely: condexpr -> stmt -> stmt -> bool. (** Translation of statements. [transl_stmt map s nd nexits nret rret] enriches the current CFG with the RTL instructions necessary to @@ -391,26 +391,31 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) (nexits: list node) (nret: node) (rret: option reg) {struct s} : mon node := match s with + | Sskip => + ret nd | Sexpr a => let mut := mutated_expr a in do r <- alloc_reg map mut a; transl_expr map mut a r nd + | Sseq s1 s2 => + do ns <- transl_stmt map s2 nd nexits nret rret; + transl_stmt map s1 ns nexits nret rret | Sifthenelse a strue sfalse => let mut := mutated_condexpr a in (if more_likely a strue sfalse then - do nfalse <- transl_stmtlist map sfalse nd nexits nret rret; - do ntrue <- transl_stmtlist map strue nd nexits nret rret; + do nfalse <- transl_stmt map sfalse nd nexits nret rret; + do ntrue <- transl_stmt map strue nd nexits nret rret; transl_condition map mut a ntrue nfalse else - do ntrue <- transl_stmtlist map strue nd nexits nret rret; - do nfalse <- transl_stmtlist map sfalse nd nexits nret rret; + do ntrue <- transl_stmt map strue nd nexits nret rret; + do nfalse <- transl_stmt map sfalse nd nexits nret rret; transl_condition map mut a ntrue nfalse) | Sloop sbody => do nloop <- reserve_instr; - do nbody <- transl_stmtlist map sbody nloop nexits nret rret; + do nbody <- transl_stmt map sbody nloop nexits nret rret; do x <- update_instr nloop (Inop nbody); ret nbody | Sblock sbody => - transl_stmtlist map sbody nd (nd :: nexits) nret rret + transl_stmt map sbody nd (nd :: nexits) nret rret | Sexit n => match nth_error nexits n with | None => error node @@ -422,18 +427,6 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) | Some a, Some r => transl_expr map (mutated_expr a) a r nret | _, _ => error node end - end - -(** Translation of lists of statements. *) - -with transl_stmtlist (map: mapping) (sl: stmtlist) (nd: node) - (nexits: list node) (nret: node) (rret: option reg) - {struct sl} : mon node := - match sl with - | Snil => ret nd - | Scons s1 ss => - do ns <- transl_stmtlist map ss nd nexits nret rret; - transl_stmt map s1 ns nexits nret rret end. (** Translation of a Cminor function. *) @@ -450,7 +443,7 @@ Definition transl_fun (f: Cminor.function) : mon (node * list reg) := do rret <- new_reg; let orret := ret_reg f.(Cminor.fn_sig) rret in do nret <- add_instr (Ireturn orret); - do nentry <- transl_stmtlist map2 f.(Cminor.fn_body) nret nil nret orret; + do nentry <- transl_stmt map2 f.(Cminor.fn_body) nret nil nret orret; ret (nentry, rparams). Definition transl_function (f: Cminor.function) : option RTL.function := diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 98462d2..e6ab2c2 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -203,8 +203,8 @@ Definition match_return_outcome end end. -(** The simulation diagram for the translation of statements and - lists of statements is of the following form: +(** The simulation diagram for the translation of statements + is of the following form: << I /\ P e, m, a ------------- ns, rs, m @@ -245,20 +245,6 @@ Definition transl_stmt_correct /\ match_env map e' nil rs' /\ match_return_outcome out rret rs'. -Definition transl_stmtlist_correct - (sp: val) (e: env) (m: mem) (al: stmtlist) - (e': env) (m': mem) (out: outcome) : Prop := - forall map ncont nexits nret rret s ns s' nd rs - (MWF: map_wf map s) - (TE: transl_stmtlist map al ncont nexits nret rret s = OK ns s') - (ME: match_env map e nil rs) - (OUT: outcome_node out ncont nexits nret nd) - (RRG: return_reg_ok s map rret), - exists rs', - exec_instrs tge s'.(st_code) sp ns rs m nd rs' m' - /\ match_env map e' nil rs' - /\ match_return_outcome out rret 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 @@ -917,8 +903,8 @@ Lemma transl_funcall_correct: (out : outcome) (vres : val), Mem.alloc m 0 (fn_stackspace f) = (m1, sp) -> set_locals (Cminor.fn_vars f) (set_params vargs (Cminor.fn_params f)) = e -> - exec_stmtlist ge (Vptr sp Int.zero) e m1 (fn_body f) e2 m2 out -> - transl_stmtlist_correct (Vptr sp Int.zero) e m1 (fn_body f) e2 m2 out -> + exec_stmt ge (Vptr sp Int.zero) e m1 (fn_body f) e2 m2 out -> + transl_stmt_correct (Vptr sp Int.zero) e m1 (fn_body f) e2 m2 out -> outcome_result_value out f.(Cminor.fn_sig).(sig_res) vres -> transl_function_correct m f vargs (Mem.free m2 sp) vres. Proof. @@ -969,6 +955,60 @@ Proof. destruct o; contradiction||auto. Qed. +Lemma transl_stmt_Sskip_correct: + forall (sp: val) (e : env) (m : mem), + transl_stmt_correct sp e m Sskip e m Out_normal. +Proof. + intros; red; intros. simpl in TE. monadInv TE. + subst s'; subst ns. + simpl in OUT. subst ncont. + exists rs. simpl. intuition. apply exec_refl. +Qed. + +Lemma transl_stmt_Sseq_continue_correct: + forall (sp : val) (e : env) (m : mem) (s1 : stmt) (e1 : env) + (m1 : mem) (s2 : stmt) (e2 : env) (m2 : mem) (out : outcome), + exec_stmt ge sp e m s1 e1 m1 Out_normal -> + transl_stmt_correct sp e m s1 e1 m1 Out_normal -> + exec_stmt ge sp e1 m1 s2 e2 m2 out -> + transl_stmt_correct sp e1 m1 s2 e2 m2 out -> + transl_stmt_correct sp e m (Sseq s1 s2) e2 m2 out. +Proof. + intros; red; intros. simpl in TE; monadInv TE. intro EQ0. + assert (MWF1: map_wf map s0). eauto with rtlg. + assert (OUTs: outcome_node Out_normal n nexits nret n). + simpl. auto. + assert (RRG1: return_reg_ok s0 map rret). eauto with rtlg. + generalize (H0 _ _ _ _ _ _ _ _ _ _ MWF1 EQ0 ME OUTs RRG1). + intros [rs1 [EX1 [ME1 MR1]]]. + generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG). + intros [rs2 [EX2 [ME2 MR2]]]. + exists rs2. +(* Exec *) + split. eapply exec_trans. eexact EX1. + apply exec_instrs_incr with s0. eauto with rtlg. + exact EX2. +(* Match-env + return *) + tauto. +Qed. + +Lemma transl_stmt_Sseq_stop_correct: + forall (sp : val) (e : env) (m : mem) (s1 s2 : stmt) (e1 : env) + (m1 : mem) (out : outcome), + exec_stmt ge sp e m s1 e1 m1 out -> + transl_stmt_correct sp e m s1 e1 m1 out -> + out <> Out_normal -> + transl_stmt_correct sp e m (Sseq s1 s2) e1 m1 out. +Proof. + intros; red; intros. + simpl in TE; monadInv TE. intro EQ0; clear TE. + assert (MWF1: map_wf map s0). eauto with rtlg. + assert (OUTs: outcome_node out n nexits nret nd). + destruct out; simpl; auto. tauto. + assert (RRG1: return_reg_ok s0 map rret). eauto with rtlg. + exact (H0 _ _ _ _ _ _ _ _ _ _ MWF1 EQ0 ME OUTs RRG1). +Qed. + Lemma transl_stmt_Sexpr_correct: forall (sp: val) (e : env) (m : mem) (a : expr) (e1 : env) (m1 : mem) (v : val), @@ -988,12 +1028,12 @@ Qed. Lemma transl_stmt_Sifthenelse_correct: forall (sp: val) (e : env) (m : mem) (a : condexpr) - (sl1 sl2 : stmtlist) (e1 : env) (m1 : mem) + (sl1 sl2 : stmt) (e1 : env) (m1 : mem) (v1 : bool) (e2 : env) (m2 : mem) (out : outcome), eval_condexpr ge sp nil e m a e1 m1 v1 -> transl_condition_correct sp nil e m a e1 m1 v1 -> - exec_stmtlist ge sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out -> - transl_stmtlist_correct sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out -> + exec_stmt ge sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out -> + transl_stmt_correct sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out -> transl_stmt_correct sp e m (Sifthenelse a sl1 sl2) e2 m2 out. Proof. intros; red; intros until rs; intro MWF. @@ -1038,11 +1078,11 @@ Proof. Qed. Lemma transl_stmt_Sloop_loop_correct: - forall (sp: val) (e : env) (m : mem) (sl : stmtlist) + forall (sp: val) (e : env) (m : mem) (sl : stmt) (e1 : env) (m1 : mem) (e2 : env) (m2 : mem) (out : outcome), - exec_stmtlist ge sp e m sl e1 m1 Out_normal -> - transl_stmtlist_correct sp e m sl e1 m1 Out_normal -> + exec_stmt ge sp e m sl e1 m1 Out_normal -> + transl_stmt_correct sp e m sl e1 m1 Out_normal -> exec_stmt ge sp e1 m1 (Sloop sl) e2 m2 out -> transl_stmt_correct sp e1 m1 (Sloop sl) e2 m2 out -> transl_stmt_correct sp e m (Sloop sl) e2 m2 out. @@ -1077,10 +1117,10 @@ Proof. Qed. Lemma transl_stmt_Sloop_stop_correct: - forall (sp: val) (e : env) (m : mem) (sl : stmtlist) + forall (sp: val) (e : env) (m : mem) (sl : stmt) (e1 : env) (m1 : mem) (out : outcome), - exec_stmtlist ge sp e m sl e1 m1 out -> - transl_stmtlist_correct sp e m sl e1 m1 out -> + exec_stmt ge sp e m sl e1 m1 out -> + transl_stmt_correct sp e m sl e1 m1 out -> out <> Out_normal -> transl_stmt_correct sp e m (Sloop sl) e1 m1 out. Proof. @@ -1105,10 +1145,10 @@ Proof. Qed. Lemma transl_stmt_Sblock_correct: - forall (sp: val) (e : env) (m : mem) (sl : stmtlist) + forall (sp: val) (e : env) (m : mem) (sl : stmt) (e1 : env) (m1 : mem) (out : outcome), - exec_stmtlist ge sp e m sl e1 m1 out -> - transl_stmtlist_correct sp e m sl e1 m1 out -> + exec_stmt ge sp e m sl e1 m1 out -> + transl_stmt_correct sp e m sl e1 m1 out -> transl_stmt_correct sp e m (Sblock sl) e1 m1 (outcome_block out). Proof. intros; red; intros. simpl in TE. @@ -1168,85 +1208,28 @@ Proof. monadSimpl. Qed. - -Lemma transl_stmtlist_Snil_correct: - forall (sp: val) (e : env) (m : mem), - transl_stmtlist_correct sp e m Snil e m Out_normal. -Proof. - intros; red; intros. simpl in TE. monadInv TE. - subst s'; subst ns. - simpl in OUT. subst ncont. - exists rs. simpl. intuition. apply exec_refl. -Qed. - -Lemma transl_stmtlist_Scons_continue_correct: - forall (sp: val) (e : env) (m : mem) (s : stmt) - (sl : stmtlist) (e1 : env) (m1 : mem) (e2 : env) - (m2 : mem) (out : outcome), - exec_stmt ge sp e m s e1 m1 Out_normal -> - transl_stmt_correct sp e m s e1 m1 Out_normal -> - exec_stmtlist ge sp e1 m1 sl e2 m2 out -> - transl_stmtlist_correct sp e1 m1 sl e2 m2 out -> - transl_stmtlist_correct sp e m (Scons s sl) e2 m2 out. -Proof. - intros; red; intros. simpl in TE; monadInv TE. intro EQ0. - assert (MWF1: map_wf map s1). eauto with rtlg. - assert (OUTs: outcome_node Out_normal n nexits nret n). - simpl. auto. - assert (RRG1: return_reg_ok s1 map rret). eauto with rtlg. - generalize (H0 _ _ _ _ _ _ _ _ _ _ MWF1 EQ0 ME OUTs RRG1). - intros [rs1 [EX1 [ME1 MR1]]]. - generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG). - intros [rs2 [EX2 [ME2 MR2]]]. - exists rs2. -(* Exec *) - split. eapply exec_trans. eexact EX1. - apply exec_instrs_incr with s1. eauto with rtlg. - exact EX2. -(* Match-env + return *) - tauto. -Qed. - -Lemma transl_stmtlist_Scons_stop_correct: - forall (sp: val) (e : env) (m : mem) (s : stmt) - (sl : stmtlist) (e1 : env) (m1 : mem) (out : outcome), - exec_stmt ge sp e m s e1 m1 out -> - transl_stmt_correct sp e m s e1 m1 out -> - out <> Out_normal -> - transl_stmtlist_correct sp e m (Scons s sl) e1 m1 out. -Proof. - intros; red; intros. - simpl in TE; monadInv TE. intro EQ0; clear TE. - assert (MWF1: map_wf map s1). eauto with rtlg. - assert (OUTs: outcome_node out n nexits nret nd). - destruct out; simpl; auto. tauto. - assert (RRG1: return_reg_ok s1 map rret). eauto with rtlg. - exact (H0 _ _ _ _ _ _ _ _ _ _ MWF1 EQ0 ME OUTs RRG1). -Qed. (** The correctness of the translation then follows by application of the mutual induction principle for Cminor evaluation derivations to the lemmas above. *) -Scheme eval_expr_ind_6 := Minimality for eval_expr Sort Prop - with eval_condexpr_ind_6 := Minimality for eval_condexpr Sort Prop - with eval_exprlist_ind_6 := Minimality for eval_exprlist Sort Prop - with eval_funcall_ind_6 := Minimality for eval_funcall Sort Prop - with exec_stmt_ind_6 := Minimality for exec_stmt Sort Prop - with exec_stmtlist_ind_6 := Minimality for exec_stmtlist Sort Prop. +Scheme eval_expr_ind_5 := Minimality for eval_expr Sort Prop + with eval_condexpr_ind_5 := Minimality for eval_condexpr Sort Prop + with eval_exprlist_ind_5 := Minimality for eval_exprlist Sort Prop + with eval_funcall_ind_5 := Minimality for eval_funcall Sort Prop + with exec_stmt_ind_5 := Minimality for exec_stmt Sort Prop. Theorem transl_function_correctness: forall m f vargs m' vres, eval_funcall ge m f vargs m' vres -> transl_function_correct m f vargs m' vres. Proof - (eval_funcall_ind_6 ge + (eval_funcall_ind_5 ge transl_expr_correct transl_condition_correct transl_exprlist_correct transl_function_correct transl_stmt_correct - transl_stmtlist_correct transl_expr_Evar_correct transl_expr_Eassign_correct @@ -1264,17 +1247,17 @@ Proof transl_exprlist_Enil_correct transl_exprlist_Econs_correct transl_funcall_correct + transl_stmt_Sskip_correct transl_stmt_Sexpr_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_Sreturn_none_correct - transl_stmt_Sreturn_some_correct - transl_stmtlist_Snil_correct - transl_stmtlist_Scons_continue_correct - transl_stmtlist_Scons_stop_correct). + transl_stmt_Sreturn_some_correct). Theorem transl_program_correct: forall (r: val), diff --git a/backend/RTLgenproof1.v b/backend/RTLgenproof1.v index 4a8ad43..a928a3d 100644 --- a/backend/RTLgenproof1.v +++ b/backend/RTLgenproof1.v @@ -1390,52 +1390,21 @@ Proof (proj2 (proj2 transl_expr_condition_exprlist_incr)). Hint Resolve transl_expr_incr transl_condition_incr transl_exprlist_incr: rtlg. -Scheme stmt_ind2 := Induction for stmt Sort Prop - with stmtlist_ind2 := Induction for stmtlist Sort Prop. - -Lemma stmt_stmtlist_ind: -forall (P : stmt -> Prop) (P0 : stmtlist -> Prop), - (forall e : expr, P (Sexpr e)) -> - (forall (c : condexpr) (s : stmtlist), - P0 s -> forall s0 : stmtlist, P0 s0 -> P (Sifthenelse c s s0)) -> - (forall s : stmtlist, P0 s -> P (Sloop s)) -> - (forall s : stmtlist, P0 s -> P (Sblock s)) -> - (forall n : nat, P (Sexit n)) -> - (forall o : option expr, P (Sreturn o)) -> - P0 Snil -> - (forall s : stmt, - P s -> forall s0 : stmtlist, P0 s0 -> P0 (Scons s s0)) -> - (forall s : stmt, P s) /\ - (forall sl : stmtlist, P0 sl). -Proof. - intros. split. apply (stmt_ind2 P P0); assumption. - apply (stmtlist_ind2 P P0); assumption. -Qed. - -Definition transl_stmt_incr_pred (a: stmt) : Prop := - forall map nd nexits nret rret s ns s', +Lemma transl_stmt_incr: + forall a map nd nexits nret rret s ns s', transl_stmt map a nd nexits nret rret s = OK ns s' -> state_incr s s'. -Definition transl_stmtlist_incr_pred (al: stmtlist) : Prop := - forall map nd nexits nret rret s ns s', - transl_stmtlist map al nd nexits nret rret s = OK ns s' -> - state_incr s s'. - -Lemma transl_stmt_stmtlist_incr: - (forall a, transl_stmt_incr_pred a) /\ - (forall al, transl_stmtlist_incr_pred al). Proof. - apply stmt_stmtlist_ind; - unfold transl_stmt_incr_pred, - transl_stmtlist_incr_pred; - simpl; intros; + induction a; simpl; intros; try (monadInv H); try (monadInv H0); try (monadInv H1); try (monadInv H2); eauto 6 with rtlg. - generalize H1. case (more_likely c s s0); monadSimpl; eauto 6 with rtlg. + subst s'; auto with rtlg. + + generalize H. case (more_likely c a1 a2); monadSimpl; eauto 6 with rtlg. - subst s'. apply update_instr_incr with s1 s2 (Inop n0) n u; + subst s' s5. apply update_instr_incr with s3 s4 (Inop n2) n1 u0; eauto with rtlg. generalize H; destruct (nth_error nexits n); monadSimpl. @@ -1444,20 +1413,7 @@ Proof. generalize H. destruct o; destruct rret; try monadSimpl. eauto with rtlg. subst s'; auto with rtlg. - subst s'; auto with rtlg. Qed. -Lemma transl_stmt_incr: - forall a map nd nexits nret rret s ns s', - transl_stmt map a nd nexits nret rret s = OK ns s' -> - state_incr s s'. -Proof (proj1 transl_stmt_stmtlist_incr). - -Lemma transl_stmtlist_incr: - forall al map nd nexits nret rret s ns s', - transl_stmtlist map al nd nexits nret rret s = OK ns s' -> - state_incr s s'. -Proof (proj2 transl_stmt_stmtlist_incr). - -Hint Resolve transl_stmt_incr transl_stmtlist_incr: rtlg. +Hint Resolve transl_stmt_incr: rtlg. |