diff options
| -rw-r--r-- | .depend | 4 | ||||
| -rw-r--r-- | Changelog | 3 | ||||
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | backend/RTLtyping.v | 6 | ||||
| -rw-r--r-- | backend/Tailcall.v | 110 | ||||
| -rw-r--r-- | backend/Tailcallproof.v | 737 | ||||
| -rw-r--r-- | common/AST.v | 6 | ||||
| -rw-r--r-- | common/Mem.v | 20 | ||||
| -rw-r--r-- | driver/Compiler.v | 11 |
9 files changed, 889 insertions, 9 deletions
@@ -68,6 +68,8 @@ backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Intege backend/Stackingproof.vo: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machabstr.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingtyping.vo: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingproof.vo backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo +backend/Tailcallproof.vo: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Tailcall.vo +backend/Tailcall.vo: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Globalenvs.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo @@ -81,5 +83,5 @@ cfrontend/Cshmgenproof3.vo: cfrontend/Cshmgenproof3.v lib/Coqlib.vo common/Error cfrontend/Cshmgen.vo: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csyntax.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Csyntax.vo: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Ctyping.vo: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo cfrontend/Csyntax.vo -driver/Compiler.vo: driver/Compiler.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo $(ARCH)/Selection.vo backend/RTLgen.vo $(ARCH)/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/Ctyping.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/Cshmgenproof3.vo cfrontend/Cminorgenproof.vo $(ARCH)/Selectionproof.vo backend/RTLgenproof.vo $(ARCH)/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2concr.vo $(ARCH)/Asmgenproof.vo +driver/Compiler.vo: driver/Compiler.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo $(ARCH)/Selection.vo backend/RTLgen.vo backend/Tailcall.vo $(ARCH)/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/Ctyping.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/Cshmgenproof3.vo cfrontend/Cminorgenproof.vo $(ARCH)/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo $(ARCH)/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2concr.vo $(ARCH)/Asmgenproof.vo driver/Complements.vo: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo @@ -1,3 +1,6 @@ +- New optimization over RTL: turning calls into tail calls when possible. + + Release 1.3, 2008-08-11 ======================= @@ -48,6 +48,7 @@ BACKEND=\ Selection.v Selectionproof.v \ Registers.v RTL.v \ RTLgen.v RTLgenspec.v RTLgenproof.v \ + Tailcall.v Tailcallproof.v \ RTLtyping.v \ Kildall.v \ Constprop.v Constpropproof.v \ diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 60b1d72c..f466a90c 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -167,12 +167,6 @@ Section TYPECHECKING. Variable funct: function. Variable env: regenv. -Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}. -Proof. decide equality. Qed. - -Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}. -Proof. decide equality. apply typ_eq. Qed. - Definition check_reg (r: reg) (ty: typ): bool := if typ_eq (env r) ty then true else false. diff --git a/backend/Tailcall.v b/backend/Tailcall.v new file mode 100644 index 00000000..809a6a13 --- /dev/null +++ b/backend/Tailcall.v @@ -0,0 +1,110 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Recognition of tail calls. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Globalenvs. +Require Import Registers. +Require Import Op. +Require Import RTL. +Require Conventions. + +(** An [Icall] instruction that stores its result in register [rreg] + can be turned into a tail call if: +- its successor is a [Ireturn None] or [Ireturn (Some rreg)] instruction; +- the stack block of the current function is empty: [stacksize = 0]. + +If the current function had a non-empty stack block, it could be that +the called function accesses it, for instance if a pointer into the +stack block is passed as an argument. In this case, it would be +semantically incorrect to deallocate the stack block before the call, +as [Itailcall] does. Therefore, the optimization can only be performed if +the stack block of the current function is empty, in which case it makes +no semantic difference to deallocate it before or after the call. + +Another complication is that the [Ireturn] instruction does not, in general, +follow immediately the [Icall] instruction: the RTL code generator +can have inserted moves and no-ops between these instructions. +The general pattern we recognize is therefore: +<< + r1 <- call(....) + nop + r2 <- r1 + r3 <- r2 + return r3 +>> +The [is_return] function below recognizes this pattern. +*) + +Fixpoint is_return (n: nat) (f: function) (pc: node) (rret: reg) + {struct n}: bool := + match n with + | O => false + | S n' => + match f.(fn_code)!pc with + | Some(Ireturn None) => true + | Some(Ireturn (Some r)) => Reg.eq r rret + | Some(Inop s) => is_return n' f s rret + | Some(Iop op args dst s) => + match is_move_operation op args with + | None => false + | Some src => + if Reg.eq rret src + then is_return n' f s dst + else false + end + | _ => false + end + end. + +(** To ensure termination, we bound arbitrarily the number of iterations +of the [is_return] function: we look ahead for a nop/move/return of length +at most [niter] instructions. *) + +Definition niter := 5%nat. + +(** The code transformation is straightforward: call instructions + followed by an appropriate nop/move/return sequence become + tail calls; other instructions are unchanged. + + To ensure that the resulting RTL code is well typed, we + restrict the transformation to the cases where a tail call is + allowed by the calling conventions, and where the result signatures + match. *) + +Definition transf_instr (f: function) (pc: node) (instr: instruction) := + match instr with + | Icall sig ros args res s => + if is_return niter f s res + && Conventions.tailcall_is_possible sig + && opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) + then Itailcall sig ros args + else instr + | _ => instr + end. + +(** A function is transformed only if its stack block is empty, + as explained above. *) + +Definition transf_function (f: function) : function := + if zeq f.(fn_stacksize) 0 + then RTL.transf_function (transf_instr f) f + else f. + +Definition transf_fundef (fd: fundef) : fundef := + AST.transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v new file mode 100644 index 00000000..8e97e1a4 --- /dev/null +++ b/backend/Tailcallproof.v @@ -0,0 +1,737 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Recognition of tail calls: correctness proof *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Mem. +Require Import Op. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Registers. +Require Import RTL. +Require Conventions. +Require Import Tailcall. + +(** * Syntactic properties of the code transformation *) + +(** ** Measuring the number of instructions eliminated *) + +(** The [return_measure c pc] function counts the number of instructions + eliminated by the code transformation, where [pc] is the successor + of a call turned into a tailcall. This is the length of the + move/nop/return sequence recognized by the [is_return] boolean function. +*) + +Fixpoint return_measure_rec (n: nat) (c: code) (pc: node) + {struct n}: nat := + match n with + | O => O + | S n' => + match c!pc with + | Some(Inop s) => S(return_measure_rec n' c s) + | Some(Iop op args dst s) => S(return_measure_rec n' c s) + | _ => O + end + end. + +Definition return_measure (c: code) (pc: node) := + return_measure_rec niter c pc. + +Lemma return_measure_bounds: + forall f pc, (return_measure f pc <= niter)%nat. +Proof. + intro f. + assert (forall n pc, (return_measure_rec n f pc <= n)%nat). + induction n; intros; simpl. + omega. + destruct (f!pc); try omega. + destruct i; try omega. + generalize (IHn n0). omega. + generalize (IHn n0). omega. + intros. unfold return_measure. apply H. +Qed. + +Remark return_measure_rec_incr: + forall f n1 n2 pc, + (n1 <= n2)%nat -> + (return_measure_rec n1 f pc <= return_measure_rec n2 f pc)%nat. +Proof. + induction n1; intros; simpl. + omega. + destruct n2. omegaContradiction. assert (n1 <= n2)%nat by omega. + simpl. destruct f!pc; try omega. destruct i; try omega. + generalize (IHn1 n2 n H0). omega. + generalize (IHn1 n2 n H0). omega. +Qed. + +Lemma is_return_measure_rec: + forall f n n' pc r, + is_return n f pc r = true -> (n <= n')%nat -> + return_measure_rec n f.(fn_code) pc = return_measure_rec n' f.(fn_code) pc. +Proof. + induction n; simpl; intros. + congruence. + destruct n'. omegaContradiction. simpl. + destruct (fn_code f)!pc; try congruence. + destruct i; try congruence. + decEq. apply IHn with r. auto. omega. + destruct (is_move_operation o l); try congruence. + destruct (Reg.eq r r1); try congruence. + decEq. apply IHn with r0. auto. omega. +Qed. + +(** ** Relational characterization of the code transformation *) + +(** The [is_return_spec] characterizes the instruction sequences + recognized by the [is_return] boolean function. *) + +Inductive is_return_spec (f:function): node -> reg -> Prop := + | is_return_none: forall pc r, + f.(fn_code)!pc = Some(Ireturn None) -> + is_return_spec f pc r + | is_return_some: forall pc r, + f.(fn_code)!pc = Some(Ireturn (Some r)) -> + is_return_spec f pc r + | is_return_nop: forall pc r s, + f.(fn_code)!pc = Some(Inop s) -> + is_return_spec f s r -> + (return_measure f.(fn_code) s < return_measure f.(fn_code) pc)%nat -> + is_return_spec f pc r + | is_return_move: forall pc r r' s, + f.(fn_code)!pc = Some(Iop Omove (r::nil) r' s) -> + is_return_spec f s r' -> + (return_measure f.(fn_code) s < return_measure f.(fn_code) pc)%nat -> + is_return_spec f pc r. + +Lemma is_return_charact: + forall f n pc rret, + is_return n f pc rret = true -> (n <= niter)%nat -> + is_return_spec f pc rret. +Proof. + induction n; intros. + simpl in H. congruence. + generalize H. simpl. + caseEq ((fn_code f)!pc); try congruence. + intro i. caseEq i; try congruence. + intros s; intros. eapply is_return_nop; eauto. eapply IHn; eauto. omega. + unfold return_measure. + rewrite <- (is_return_measure_rec f (S n) niter pc rret); auto. + rewrite <- (is_return_measure_rec f n niter s rret); auto. + simpl. rewrite H2. omega. omega. + + intros op args dst s EQ1 EQ2. + caseEq (is_move_operation op args); try congruence. + intros src IMO. destruct (Reg.eq rret src); try congruence. + subst rret. intro. + exploit is_move_operation_correct; eauto. intros [A B]. subst. + eapply is_return_move; eauto. eapply IHn; eauto. omega. + unfold return_measure. + rewrite <- (is_return_measure_rec f (S n) niter pc src); auto. + rewrite <- (is_return_measure_rec f n niter s dst); auto. + simpl. rewrite EQ2. omega. omega. + + intros or EQ1 EQ2. destruct or; intros. + assert (r = rret). eapply proj_sumbool_true; eauto. subst r. + apply is_return_some; auto. + apply is_return_none; auto. +Qed. + +(** The [transf_instr_spec] predicate relates one instruction in the + initial code with its possible transformations in the optimized code. *) + +Inductive transf_instr_spec (f: function): instruction -> instruction -> Prop := + | transf_instr_tailcall: forall sig ros args res s, + f.(fn_stacksize) = 0 -> + is_return_spec f s res -> + transf_instr_spec f (Icall sig ros args res s) (Itailcall sig ros args) + | transf_instr_default: forall i, + transf_instr_spec f i i. + +Lemma transf_instr_charact: + forall f pc instr, + f.(fn_stacksize) = 0 -> + transf_instr_spec f instr (transf_instr f pc instr). +Proof. + intros. unfold transf_instr. destruct instr; try constructor. + caseEq (is_return niter f n r && Conventions.tailcall_is_possible s && + opt_typ_eq (sig_res s) (sig_res (fn_sig f))); intros. + destruct (andb_prop _ _ H0). destruct (andb_prop _ _ H1). + eapply transf_instr_tailcall; eauto. + eapply is_return_charact; eauto. + constructor. +Qed. + +Lemma transf_instr_lookup: + forall f pc i, + f.(fn_code)!pc = Some i -> + exists i', (transf_function f).(fn_code)!pc = Some i' /\ transf_instr_spec f i i'. +Proof. + intros. unfold transf_function. destruct (zeq (fn_stacksize f) 0). + simpl. rewrite PTree.gmap. rewrite H. simpl. + exists (transf_instr f pc i); split. auto. apply transf_instr_charact; auto. + exists i; split. auto. constructor. +Qed. + +(** * Semantic properties of the code transformation *) + +(** ** The ``less defined than'' relation between register states *) + +(** A call followed by a return without an argument can be turned + into a tail call. In this case, the original function returns + [Vundef], while the transformed function can return any value. + We account for this situation by using the ``less defined than'' + relation between values and between memory states. We need to + extend it pointwise to register states. *) + +Definition regset_lessdef (rs rs': regset) : Prop := + forall r, Val.lessdef (rs#r) (rs'#r). + +Lemma regset_get_list: + forall rs rs' l, + regset_lessdef rs rs' -> Val.lessdef_list (rs##l) (rs'##l). +Proof. + induction l; simpl; intros; constructor; auto. +Qed. + +Lemma regset_set: + forall rs rs' v v' r, + regset_lessdef rs rs' -> Val.lessdef v v' -> + regset_lessdef (rs#r <- v) (rs'#r <- v'). +Proof. + intros; red; intros. repeat rewrite PMap.gsspec. destruct (peq r0 r); auto. +Qed. + +Lemma regset_init_regs: + forall params vl vl', + Val.lessdef_list vl vl' -> + regset_lessdef (init_regs vl params) (init_regs vl' params). +Proof. + induction params; intros. + simpl. red; intros. rewrite Regmap.gi. constructor. + simpl. inv H. red; intros. rewrite Regmap.gi. constructor. + apply regset_set. auto. auto. +Qed. + +(** ** Agreement between the size of a stack block and a function *) + +(** To reason over deallocation of empty stack blocks, we need to + maintain the invariant that the bounds of a stack block + for function [f] are always [0, f.(fn_stacksize)]. *) + +Inductive match_stacksize: function -> block -> mem -> Z -> Prop := + | match_stacksize_intro: forall f sp m bound, + sp < bound -> + low_bound m sp = 0 -> + high_bound m sp = f.(fn_stacksize) -> + match_stacksize f sp m bound. + +Lemma match_stacksize_store: + forall m m' chunk b ofs v f sp bound, + store chunk m b ofs v = Some m' -> + match_stacksize f sp m bound -> + match_stacksize f sp m' bound. +Proof. + intros. inv H0. constructor. auto. + rewrite <- H2. eapply Mem.low_bound_store; eauto. + rewrite <- H3. eapply Mem.high_bound_store; eauto. +Qed. + +Lemma match_stacksize_alloc_other: + forall m m' lo hi b f sp bound, + alloc m lo hi = (m', b) -> + match_stacksize f sp m bound -> + bound <= m.(nextblock) -> + match_stacksize f sp m' bound. +Proof. + intros. inv H0. + assert (valid_block m sp). red. omega. + constructor. auto. + rewrite <- H3. eapply low_bound_alloc_other; eauto. + rewrite <- H4. eapply high_bound_alloc_other; eauto. +Qed. + +Lemma match_stacksize_alloc_same: + forall m f m' sp, + alloc m 0 f.(fn_stacksize) = (m', sp) -> + match_stacksize f sp m' m'.(nextblock). +Proof. + intros. constructor. + unfold alloc in H. inv H. simpl. omega. + eapply low_bound_alloc_same; eauto. + eapply high_bound_alloc_same; eauto. +Qed. + +Lemma match_stacksize_free: + forall f sp m b bound, + match_stacksize f sp m bound -> + bound <= b -> + match_stacksize f sp (free m b) bound. +Proof. + intros. inv H. constructor. auto. + rewrite <- H2. apply low_bound_free. unfold block; omega. + rewrite <- H3. apply high_bound_free. unfold block; omega. +Qed. + +(** * Proof of semantic preservation *) + +Section PRESERVATION. + +Variable prog: program. +Let tprog := transf_program prog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof (Genv.find_symbol_transf transf_fundef prog). + +Lemma functions_translated: + forall (v: val) (f: RTL.fundef), + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog). + +Lemma funct_ptr_translated: + forall (b: block) (f: RTL.fundef), + Genv.find_funct_ptr ge b = Some f -> + Genv.find_funct_ptr tge b = Some (transf_fundef f). +Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog). + +Lemma sig_preserved: + forall f, funsig (transf_fundef f) = funsig f. +Proof. + destruct f; auto. simpl. unfold transf_function. + destruct (zeq (fn_stacksize f) 0); auto. +Qed. + +Lemma find_function_translated: + forall ros rs rs' f, + find_function ge ros rs = Some f -> + regset_lessdef rs rs' -> + find_function tge ros rs' = Some (transf_fundef f). +Proof. + intros until f; destruct ros; simpl. + intros. + assert (rs'#r = rs#r). + exploit Genv.find_funct_inv; eauto. intros [b EQ]. + generalize (H0 r). rewrite EQ. intro LD. inv LD. auto. + rewrite H1. apply functions_translated; auto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge i); intros. + apply funct_ptr_translated; auto. + discriminate. +Qed. + +(** Consider an execution of a call/move/nop/return sequence in the + original code and the corresponding tailcall in the transformed code. + The transition sequences are of the following form + (left: original code, right: transformed code). + [f] is the calling function and [fd] the called function. +<< + State stk f (Icall instruction) State stk' f' (Itailcall) + + Callstate (frame::stk) fd args Callstate stk' fd' args' + . . + . . + . . + Returnstate (frame::stk) res Returnstate stk' res' + + State stk f (move/nop/return seq) + . + . + . + State stk f (return instr) + + Returnstate stk res +>> +The simulation invariant must therefore account for two kinds of +mismatches between the transition sequences: +- The call stack of the original program can contain more frames + than that of the transformed program (e.g. [frame] in the example above). +- The regular states corresponding to executing the move/nop/return + sequence must all correspond to the single [Returnstate stk' res'] + state of the transformed program. + +We first define the simulation invariant between call stacks. +The first two cases are standard, but the third case corresponds +to a frame that was eliminated by the transformation. *) + +Inductive match_stackframes: mem -> Z -> list stackframe -> list stackframe -> Prop := + | match_stackframes_nil: forall m bound, + match_stackframes m bound nil nil + | match_stackframes_normal: forall m bound stk stk' res sp pc rs rs' f, + match_stackframes m sp stk stk' -> + match_stacksize f sp m bound -> + regset_lessdef rs rs' -> + match_stackframes m bound + (Stackframe res f.(fn_code) (Vptr sp Int.zero) pc rs :: stk) + (Stackframe res (transf_function f).(fn_code) (Vptr sp Int.zero) pc rs' :: stk') + | match_stackframes_tail: forall m bound stk stk' res sp pc rs f, + match_stackframes m sp stk stk' -> + match_stacksize f sp m bound -> + is_return_spec f pc res -> + f.(fn_stacksize) = 0 -> + match_stackframes m bound + (Stackframe res f.(fn_code) (Vptr sp Int.zero) pc rs :: stk) + stk'. + +(** In [match_stackframes m bound s s'], the memory state [m] is used + to check that the sizes of the stack blocks agree with what was + declared by the corresponding functions. The [bound] parameter + is used to enforce separation between the stack blocks. *) + +Lemma match_stackframes_incr: + forall m bound s s' bound', + match_stackframes m bound s s' -> + bound <= bound' -> + match_stackframes m bound' s s'. +Proof. + intros. inv H; econstructor; eauto. + inv H2. constructor; auto. omega. + inv H2. constructor; auto. omega. +Qed. + +Lemma match_stackframes_store: + forall m bound s s', + match_stackframes m bound s s' -> + forall chunk b ofs v m', + store chunk m b ofs v = Some m' -> + match_stackframes m' bound s s'. +Proof. + induction 1; intros. + constructor. + econstructor; eauto. eapply match_stacksize_store; eauto. + econstructor; eauto. eapply match_stacksize_store; eauto. +Qed. + +Lemma match_stackframes_alloc: + forall m lo hi m' sp s s', + match_stackframes m (nextblock m) s s' -> + alloc m lo hi = (m', sp) -> + match_stackframes m' sp s s'. +Proof. + intros. + assert (forall bound s s', + match_stackframes m bound s s' -> + bound <= m.(nextblock) -> + match_stackframes m' bound s s'). + induction 1; intros. constructor. + constructor; auto. apply IHmatch_stackframes; auto. inv H2. omega. + eapply match_stacksize_alloc_other; eauto. + econstructor; eauto. apply IHmatch_stackframes; auto. inv H2. omega. + eapply match_stacksize_alloc_other; eauto. + exploit alloc_result; eauto. intro. rewrite H2. + eapply H1; eauto. omega. +Qed. + +Lemma match_stackframes_free: + forall f sp m s s', + match_stacksize f sp m (nextblock m) -> + match_stackframes m sp s s' -> + match_stackframes (free m sp) (nextblock (free m sp)) s s'. +Proof. + intros. simpl. + assert (forall bound s s', + match_stackframes m bound s s' -> + bound <= sp -> + match_stackframes (free m sp) bound s s'). + induction 1; intros. constructor. + constructor; auto. apply IHmatch_stackframes; auto. inv H2; omega. + apply match_stacksize_free; auto. + econstructor; eauto. apply IHmatch_stackframes; auto. inv H2; omega. + apply match_stacksize_free; auto. + + apply match_stackframes_incr with sp. apply H1; auto. omega. + inv H. omega. +Qed. + +(** Here is the invariant relating two states. The first three + cases are standard. Note the ``less defined than'' conditions + over values, register states, and memory states. *) + +Inductive match_states: state -> state -> Prop := + | match_states_normal: + forall s sp pc rs m s' rs' m' f + (STKSZ: match_stacksize f sp m m.(nextblock)) + (STACKS: match_stackframes m sp s s') + (RLD: regset_lessdef rs rs') + (MLD: Mem.lessdef m m'), + match_states (State s f.(fn_code) (Vptr sp Int.zero) pc rs m) + (State s' (transf_function f).(fn_code) (Vptr sp Int.zero) pc rs' m') + | match_states_call: + forall s f args m s' args' m', + match_stackframes m m.(nextblock) s s' -> + Val.lessdef_list args args' -> + Mem.lessdef m m' -> + match_states (Callstate s f args m) + (Callstate s' (transf_fundef f) args' m') + | match_states_return: + forall s v m s' v' m', + match_stackframes m m.(nextblock) s s' -> + Val.lessdef v v' -> + Mem.lessdef m m' -> + match_states (Returnstate s v m) + (Returnstate s' v' m') + | match_states_interm: + forall s sp pc rs m s' m' f r v' + (STKSZ: match_stacksize f sp m m.(nextblock)) + (STACKS: match_stackframes m sp s s') + (MLD: Mem.lessdef m m'), + is_return_spec f pc r -> + f.(fn_stacksize) = 0 -> + Val.lessdef (rs#r) v' -> + match_states (State s f.(fn_code) (Vptr sp Int.zero) pc rs m) + (Returnstate s' v' m'). + +(** The last case of [match_states] corresponds to the execution + of a move/nop/return sequence in the original code that was + eliminated by the transformation: +<< + State stk f (move/nop/return seq) ~~ Returnstate stk' res' + . + . + . + State stk f (return instr) ~~ Returnstate stk' res' +>> + To preserve non-terminating behaviors, we need to make sure + that the execution of this sequence in the original code cannot + diverge. For this, we introduce the following complicated + measure over states, which will decrease strictly whenever + the original code makes a transition but the transformed code + does not. *) + +Definition measure (st: state) : nat := + match st with + | State s c sp pc rs m => (List.length s * (niter + 2) + return_measure c pc + 1)%nat + | Callstate s f args m => 0%nat + | Returnstate s v m => (List.length s * (niter + 2))%nat + end. + +Ltac TransfInstr := + match goal with + | H: (PTree.get _ (fn_code _) = _) |- _ => + destruct (transf_instr_lookup _ _ _ H) as [i' [TINSTR TSPEC]]; inv TSPEC + end. + +Ltac EliminatedInstr := + match goal with + | H: (is_return_spec _ _ _) |- _ => inv H; try congruence + | _ => idtac + end. + +(** The proof of semantic preservation, then, is a simulation diagram + of the ``option'' kind. *) + +Lemma transf_step_correct: + forall s1 t s2, step ge s1 t s2 -> + forall s1' (MS: match_states s1 s1'), + (exists s2', step tge s1' t s2' /\ match_states s2 s2') + \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat. +Proof. + induction 1; intros; inv MS; EliminatedInstr. + +(* nop *) + TransfInstr. left. econstructor; split. + eapply exec_Inop; eauto. constructor; auto. +(* eliminated nop *) + assert (s0 = pc') by congruence. subst s0. + right. split. simpl. omega. split. auto. + econstructor; eauto. + +(* op *) + TransfInstr. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. + exploit eval_operation_lessdef; eauto. + intros [v' [EVAL' VLD]]. + left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'); split. + eapply exec_Iop; eauto. rewrite <- EVAL'. + apply eval_operation_preserved. exact symbols_preserved. + econstructor; eauto. apply regset_set; auto. +(* eliminated move *) + rewrite H1 in H. clear H1. inv H. + right. split. simpl. omega. split. auto. + econstructor; eauto. simpl in H0. rewrite PMap.gss. congruence. + +(* load *) + TransfInstr. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. + exploit eval_addressing_lessdef; eauto. + intros [a' [ADDR' ALD]]. + exploit loadv_lessdef; eauto. + intros [v' [LOAD' VLD]]. + left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split. + eapply exec_Iload; eauto. rewrite <- ADDR'. + apply eval_addressing_preserved. exact symbols_preserved. + econstructor; eauto. apply regset_set; auto. + +(* store *) + TransfInstr. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. + exploit eval_addressing_lessdef; eauto. + intros [a' [ADDR' ALD]]. + exploit storev_lessdef. 4: eexact H1. eauto. eauto. apply RLD. + intros [m'1 [STORE' MLD']]. + left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'1); split. + eapply exec_Istore; eauto. rewrite <- ADDR'. + apply eval_addressing_preserved. exact symbols_preserved. + destruct a; simpl in H1; try discriminate. + econstructor; eauto. + eapply match_stacksize_store; eauto. + rewrite (nextblock_store _ _ _ _ _ _ H1). auto. + eapply match_stackframes_store; eauto. + +(* call *) + exploit find_function_translated; eauto. intro FIND'. + TransfInstr. +(* call turned tailcall *) + left. exists (Callstate s' (transf_fundef f) (rs'##args) (Mem.free m' sp0)); split. + eapply exec_Itailcall; eauto. apply sig_preserved. + constructor. eapply match_stackframes_tail; eauto. apply regset_get_list; auto. + apply Mem.free_right_lessdef; auto. inv STKSZ. omega. +(* call that remains a call *) + left. exists (Callstate (Stackframe res (fn_code (transf_function f0)) (Vptr sp0 Int.zero) pc' rs' :: s') + (transf_fundef f) (rs'##args) m'); split. + eapply exec_Icall; eauto. apply sig_preserved. + constructor. constructor; auto. apply regset_get_list; auto. auto. + +(* tailcall *) + exploit find_function_translated; eauto. intro FIND'. + TransfInstr. + left. exists (Callstate s' (transf_fundef f) (rs'##args) (Mem.free m' stk)); split. + eapply exec_Itailcall; eauto. apply sig_preserved. + constructor. eapply match_stackframes_free; eauto. + apply regset_get_list; auto. apply Mem.free_lessdef; auto. + +(* cond true *) + TransfInstr. + left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) ifso rs' m'); split. + eapply exec_Icond_true; eauto. + apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto. + constructor; auto. + +(* cond false *) + TransfInstr. + left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) ifnot rs' m'); split. + eapply exec_Icond_false; eauto. + apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto. + constructor; auto. + +(* return *) + TransfInstr. + left. exists (Returnstate s' (regmap_optget or Vundef rs') (free m' stk)); split. + apply exec_Ireturn; auto. + constructor. + eapply match_stackframes_free; eauto. + destruct or; simpl. apply RLD. constructor. + apply Mem.free_lessdef; auto. + +(* eliminated return None *) + assert (or = None) by congruence. subst or. + right. split. simpl. omega. split. auto. + constructor. + eapply match_stackframes_free; eauto. + simpl. constructor. + apply Mem.free_left_lessdef; auto. + +(* eliminated return Some *) + assert (or = Some r) by congruence. subst or. + right. split. simpl. omega. split. auto. + constructor. + eapply match_stackframes_free; eauto. + simpl. auto. + apply Mem.free_left_lessdef; auto. + +(* internal call *) + caseEq (alloc m'0 0 (fn_stacksize f)). intros m'1 stk' ALLOC'. + exploit alloc_lessdef; eauto. intros [EQ1 LD']. subst stk'. + assert (fn_stacksize (transf_function f) = fn_stacksize f /\ + fn_entrypoint (transf_function f) = fn_entrypoint f /\ + fn_params (transf_function f) = fn_params f). + unfold transf_function. destruct (zeq (fn_stacksize f) 0); auto. + destruct H0 as [EQ1 [EQ2 EQ3]]. + left. econstructor; split. + simpl. eapply exec_function_internal; eauto. rewrite EQ1; eauto. + rewrite EQ2. rewrite EQ3. constructor; auto. + eapply match_stacksize_alloc_same; eauto. + eapply match_stackframes_alloc; eauto. + apply regset_init_regs. auto. + +(* external call *) + exploit event_match_lessdef; eauto. intros [res' [EVM' VLD']]. + left. exists (Returnstate s' res' m'); split. + simpl. econstructor; eauto. + constructor; auto. + +(* returnstate *) + inv H2. +(* synchronous return in both programs *) + left. econstructor; split. + apply exec_return. + constructor; auto. apply regset_set; auto. +(* return instr in source program, eliminated because of tailcall *) + right. split. unfold measure. simpl length. + change (S (length s) * (niter + 2))%nat + with ((niter + 2) + (length s) * (niter + 2))%nat. + generalize (return_measure_bounds (fn_code f) pc). omega. + split. auto. + econstructor; eauto. + rewrite Regmap.gss. auto. +Qed. + +Lemma transf_initial_states: + forall st1, initial_state prog st1 -> + exists st2, initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inv H. + exploit funct_ptr_translated; eauto. intro FIND. + exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. + econstructor; eauto. + replace (prog_main tprog) with (prog_main prog). + rewrite symbols_preserved. eauto. + reflexivity. + rewrite <- H2. apply sig_preserved. + replace (Genv.init_mem tprog) with (Genv.init_mem prog). + constructor. constructor. constructor. apply lessdef_refl. + symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> final_state st1 r -> final_state st2 r. +Proof. + intros. inv H0. inv H. inv H5. inv H3. constructor. +Qed. + + +(** The preservation of the observable behavior of the program then + follows, using the generic preservation theorem + [Smallstep.simulation_opt_preservation]. *) + +Theorem transf_program_correct: + forall (beh: program_behavior), + exec_program prog beh -> exec_program tprog beh. +Proof. + unfold exec_program; intros. + eapply simulation_opt_preservation with (measure := measure); eauto. + eexact transf_initial_states. + eexact transf_final_states. + exact transf_step_correct. +Qed. + +End PRESERVATION. + + diff --git a/common/AST.v b/common/AST.v index eab1adf1..ec8053d4 100644 --- a/common/AST.v +++ b/common/AST.v @@ -46,6 +46,12 @@ Definition typesize (ty: typ) : Z := Lemma typesize_pos: forall ty, typesize ty > 0. Proof. destruct ty; simpl; omega. Qed. +Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}. +Proof. decide equality. Qed. + +Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}. +Proof. decide equality. apply typ_eq. Qed. + (** Additionally, function definitions and function calls are annotated by function signatures indicating the number and types of arguments, as well as the type of the returned value if any. These signatures diff --git a/common/Mem.v b/common/Mem.v index de3e8c94..e169dfc7 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -1796,6 +1796,26 @@ Proof. unfold inject_id; intros. congruence. Qed. +Lemma free_left_lessdef: + forall m1 m2 b, + lessdef m1 m2 -> lessdef (free m1 b) m2. +Proof. + intros. destruct H. split. + rewrite <- H. auto. + apply free_left_inj; auto. +Qed. + +Lemma free_right_lessdef: + forall m1 m2 b, + lessdef m1 m2 -> low_bound m1 b >= high_bound m1 b -> + lessdef m1 (free m2 b). +Proof. + intros. destruct H. unfold lessdef. split. + rewrite H. auto. + apply free_right_inj; auto. intros. unfold inject_id in H2. inv H2. + red; intro. inv H2. generalize (size_chunk_pos chunk); intro. omega. +Qed. + Lemma valid_block_lessdef: forall m1 m2 b, lessdef m1 m2 -> valid_block m1 b -> valid_block m2 b. Proof. diff --git a/driver/Compiler.v b/driver/Compiler.v index 219fcae3..bce0dab0 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -36,6 +36,7 @@ Require Cshmgen. Require Cminorgen. Require Selection. Require RTLgen. +Require Tailcall. Require Constprop. Require CSE. Require Allocation. @@ -56,6 +57,7 @@ Require Cshmgenproof3. Require Cminorgenproof. Require Selectionproof. Require RTLgenproof. +Require Tailcallproof. Require Constpropproof. Require CSEproof. Require Allocproof. @@ -108,6 +110,7 @@ Notation "a @@ b" := Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := OK f + @@ Tailcall.transf_fundef @@ Constprop.transf_fundef @@ CSE.transf_fundef @@@ Allocation.transf_fundef @@ -245,7 +248,9 @@ Proof. clear H2. destruct (transform_program_compose _ _ _ _ _ _ _ _ H1) as [p0 [H00 P0]]. clear H1. - generalize (transform_partial_program_identity _ _ _ _ H00). clear H00. intro. subst p0. + destruct (transform_program_compose _ _ _ _ _ _ _ _ H00) as [p00 [H000 P00]]. + clear H00. + generalize (transform_partial_program_identity _ _ _ _ H000). clear H000. intro. subst p00. assert (WT3 : LTLtyping.wt_program p3). apply Alloctyping.program_typing_preserved with p2. auto. @@ -266,7 +271,9 @@ Proof. subst p4; apply Tunnelingproof.transf_program_correct. apply Allocproof.transf_program_correct with p2; auto. subst p2; apply CSEproof.transf_program_correct. - subst p1; apply Constpropproof.transf_program_correct. auto. + subst p1; apply Constpropproof.transf_program_correct. + subst p0; apply Tailcallproof.transf_program_correct. + auto. Qed. Theorem transf_cminor_program_correct: |