diff options
35 files changed, 534 insertions, 237 deletions
@@ -22,7 +22,7 @@ common/Memory.vo common/Memory.glob common/Memory.v.beautified: common/Memory.v common/Values.vo common/Values.glob common/Values.v.beautified: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Smallstep.vo common/Smallstep.glob common/Smallstep.v.beautified: common/Smallstep.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Behaviors.vo common/Behaviors.glob common/Behaviors.v.beautified: common/Behaviors.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Smallstep.vo -common/Switch.vo common/Switch.glob common/Switch.v.beautified: common/Switch.v lib/Coqlib.vo lib/Integers.vo lib/Ordered.vo +common/Switch.vo common/Switch.glob common/Switch.v.beautified: common/Switch.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo common/Determinism.vo common/Determinism.glob common/Determinism.v.beautified: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo backend/Cminor.vo backend/Cminor.glob backend/Cminor.v.beautified: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo $(ARCH)/Op.vo $(ARCH)/Op.glob $(ARCH)/Op.v.beautified: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo @@ -45,10 +45,11 @@ backend/Renumber.vo backend/Renumber.glob backend/Renumber.v.beautified: backend backend/Renumberproof.vo backend/Renumberproof.glob backend/Renumberproof.v.beautified: backend/Renumberproof.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Renumber.vo backend/RTLtyping.vo backend/RTLtyping.glob backend/RTLtyping.v.beautified: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo lib/Integers.vo common/Events.vo backend/RTL.vo backend/Conventions.vo backend/Kildall.vo backend/Kildall.glob backend/Kildall.v.beautified: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo +backend/Liveness.vo backend/Liveness.glob backend/Liveness.v.beautified: backend/Liveness.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob $(ARCH)/ConstpropOp.v.beautified: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo -backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo +backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo -backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo +backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob $(ARCH)/CombineOp.v.beautified: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo $(ARCH)/SelectOp.vo backend/CSE.vo backend/CSE.glob backend/CSE.v.beautified: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/RTL.vo $(ARCH)/CombineOp.vo backend/CSE.vo @@ -62,8 +63,8 @@ backend/LTLtyping.vo backend/LTLtyping.glob backend/LTLtyping.v.beautified: back backend/InterfGraph.vo backend/InterfGraph.glob backend/InterfGraph.v.beautified: backend/InterfGraph.v lib/Coqlib.vo lib/Ordered.vo backend/Registers.vo backend/Locations.vo backend/Coloring.vo backend/Coloring.glob backend/Coloring.v.beautified: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloringproof.vo backend/Coloringproof.glob backend/Coloringproof.v.beautified: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo -backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Coloring.vo backend/LTL.vo -backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/LTL.vo +backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Liveness.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo +backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Liveness.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Alloctyping.vo backend/Alloctyping.glob backend/Alloctyping.v.beautified: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Conventions.vo backend/Tunneling.vo backend/Tunneling.glob backend/Tunneling.v.beautified: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo backend/LTL.vo backend/Tunnelingproof.vo backend/Tunnelingproof.glob backend/Tunnelingproof.v.beautified: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo @@ -1,3 +1,11 @@ +Development version + +- Reduced stack usage of the compiler by rewriting some key functions + in tail-recursive style. +- Reduced memory requirements of constant propagation pass by forgetting + compile-time approximations of dead variables. + + Release 1.13, 2013-03-12 ======================== @@ -73,7 +73,7 @@ BACKEND=\ Inlining.v Inliningspec.v Inliningproof.v \ Renumber.v Renumberproof.v \ RTLtyping.v \ - Kildall.v \ + Kildall.v Liveness.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v LTLtyping.v \ diff --git a/arm/Asmgen.v b/arm/Asmgen.v index c7d7712..d158c77 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -593,7 +593,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (** Translation of a code sequence *) -Definition r10_is_parent (before: bool) (i: Mach.instruction) : bool := +Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool := match i with | Msetstack src ofs ty => before | Mgetparam ofs ty dst => negb (mreg_eq dst IT1) @@ -601,14 +601,32 @@ Definition r10_is_parent (before: bool) (i: Mach.instruction) : bool := | _ => false end. -Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (r10p: bool) := +(** This is the naive definition that we no longer use because it + is not tail-recursive. It is kept as specification. *) + +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := match il with | nil => OK nil | i1 :: il' => - do k <- transl_code f il' (r10_is_parent r10p i1); - transl_instr f i1 r10p k + do k <- transl_code f il' (it1_is_parent it1p i1); + transl_instr f i1 it1p k end. +(** This is an equivalent definition in continuation-passing style + that runs in constant stack space. *) + +Fixpoint transl_code_rec (f: Mach.function) (il: list Mach.instruction) + (it1p: bool) (k: code -> res code) := + match il with + | nil => k nil + | i1 :: il' => + transl_code_rec f il' (it1_is_parent it1p i1) + (fun c1 => do c2 <- transl_instr f i1 it1p c1; k c2) + end. + +Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := + transl_code_rec f il it1p (fun c => OK c). + (** Translation of a whole function. Note that we must check that the generated code contains less than [2^32] instructions, otherwise the offset part of the [PC] code pointer could wrap diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 0760eb0..986d474 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -451,7 +451,7 @@ Lemma exec_straight_steps: exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' /\ agree ms2 sp rs2 - /\ (r10_is_parent ep i = true -> rs2#IR10 = parent_sp s)) -> + /\ (it1_is_parent ep i = true -> rs2#IR10 = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ match_states (Mach.State s fb sp c ms2 m2) st'. @@ -470,7 +470,7 @@ Lemma exec_straight_steps_goto: Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl f.(Mach.fn_code) = Some c' -> transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> - r10_is_parent ep i = false -> + it1_is_parent ep i = false -> (forall k c (TR: transl_instr f i ep k = OK c), exists jmp, exists k', exists rs2, exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' diff --git a/backend/Allocation.v b/backend/Allocation.v index 4a4c219..caaf09d 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -21,107 +21,13 @@ Require Import Op. Require Import Registers. Require Import RTL. Require Import RTLtyping. -Require Import Kildall. +Require Import Liveness. Require Import Locations. +Require Import LTL. Require Import Coloring. -(** * Liveness analysis over RTL *) - -(** A register [r] is live at a point [p] if there exists a path - from [p] to some instruction that uses [r] as argument, - and [r] is not redefined along this path. - Liveness can be computed by a backward dataflow analysis. - The analysis operates over sets of (live) pseudo-registers. *) - -Notation reg_live := Regset.add. -Notation reg_dead := Regset.remove. - -Definition reg_option_live (or: option reg) (lv: Regset.t) := - match or with None => lv | Some r => reg_live r lv end. - -Definition reg_sum_live (ros: reg + ident) (lv: Regset.t) := - match ros with inl r => reg_live r lv | inr s => lv end. - -Fixpoint reg_list_live - (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t := - match rl with - | nil => lv - | r1 :: rs => reg_list_live rs (reg_live r1 lv) - end. - -Fixpoint reg_list_dead - (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t := - match rl with - | nil => lv - | r1 :: rs => reg_list_dead rs (reg_dead r1 lv) - end. - -(** Here is the transfer function for the dataflow analysis. - Since this is a backward dataflow analysis, it takes as argument - the abstract register set ``after'' the given instruction, - i.e. the registers that are live after; and it returns as result - the abstract register set ``before'' the given instruction, - i.e. the registers that must be live before. - The general relation between ``live before'' and ``live after'' - an instruction is that a register is live before if either - it is one of the arguments of the instruction, or it is not the result - of the instruction and it is live after. - However, if the result of a side-effect-free instruction is not - live ``after'', the whole instruction will be removed later - (since it computes a useless result), thus its arguments need not - be live ``before''. *) - -Definition transfer - (f: RTL.function) (pc: node) (after: Regset.t) : Regset.t := - match f.(fn_code)!pc with - | None => - Regset.empty - | Some i => - match i with - | Inop s => - after - | Iop op args res s => - if Regset.mem res after then - reg_list_live args (reg_dead res after) - else - after - | Iload chunk addr args dst s => - if Regset.mem dst after then - reg_list_live args (reg_dead dst after) - else - after - | Istore chunk addr args src s => - reg_list_live args (reg_live src after) - | Icall sig ros args res s => - reg_list_live args - (reg_sum_live ros (reg_dead res after)) - | Itailcall sig ros args => - reg_list_live args (reg_sum_live ros Regset.empty) - | Ibuiltin ef args res s => - reg_list_live args (reg_dead res after) - | Icond cond args ifso ifnot => - reg_list_live args after - | Ijumptable arg tbl => - reg_live arg after - | Ireturn optarg => - reg_option_live optarg Regset.empty - end - end. - -(** The liveness analysis is then obtained by instantiating the - general framework for backward dataflow analysis provided by - module [Kildall]. *) - -Module RegsetLat := LFSet(Regset). -Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward). - -Definition analyze (f: RTL.function): option (PMap.t Regset.t) := - DS.fixpoint (successors f) (transfer f) nil. - (** * Translation from RTL to LTL *) -Require Import LTL. - (** Each [RTL] instruction translates to an [LTL] instruction. The register assignment [assign] returned by register allocation is applied to the arguments and results of the RTL diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 2011485..8dfa2d4 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -28,7 +28,9 @@ Require Import Op. Require Import Registers. Require Import RTL. Require Import RTLtyping. +Require Import Liveness. Require Import Locations. +Require Import LTL. Require Import Conventions. Require Import Coloring. Require Import Coloringproof. @@ -42,7 +44,7 @@ Require Import Allocation. Section REGALLOC_PROPERTIES. -Variable f: function. +Variable f: RTL.function. Variable env: regenv. Variable live: PMap.t Regset.t. Variable alloc: reg -> loc. @@ -145,7 +147,7 @@ Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop := Lemma agree_increasing: forall live1 live2 rs ls, - RegsetLat.ge live1 live2 -> agree live1 rs ls -> + Regset.Subset live2 live1 -> agree live1 rs ls -> agree live2 rs ls. Proof. unfold agree; intros. @@ -162,9 +164,7 @@ Lemma agree_succ: Proof. intros. apply agree_increasing with (live!!n). - eapply DS.fixpoint_solution. unfold analyze in H; eauto. - unfold RTL.successors, Kildall.successors_list. - rewrite PTree.gmap1. rewrite H0. simpl. auto. + eapply Liveness.analyze_solution; eauto. auto. Qed. diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index a653683..59bf621 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -19,6 +19,7 @@ Require Import AST. Require Import Op. Require Import Registers. Require Import RTL. +Require Import Liveness. Require Import Locations. Require Import LTL. Require Import Coloring. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index e1a3abc..72de80a 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -452,6 +452,28 @@ Inductive transl_code_at_pc (ge: Mach.genv): code_tail (Int.unsigned ofs) (fn_code tf) tc -> transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc. +(** Equivalence between [transl_code] and [transl_code']. *) + +Local Open Scope error_monad_scope. + +Lemma transl_code_rec_transl_code: + forall f il ep k, + transl_code_rec f il ep k = (do c <- transl_code f il ep; k c). +Proof. + induction il; simpl; intros. + auto. + rewrite IHil. + destruct (transl_code f il (it1_is_parent ep a)); simpl; auto. +Qed. + +Lemma transl_code'_transl_code: + forall f il ep, + transl_code' f il ep = transl_code f il ep. +Proof. + intros. unfold transl_code'. rewrite transl_code_rec_transl_code. + destruct (transl_code f il ep); auto. +Qed. + (** Predictor for return addresses in generated Asm code. The [return_address_offset] predicate defined here is used in the diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v index 0ed2be1..8db871e 100644 --- a/backend/CleanupLabels.v +++ b/backend/CleanupLabels.v @@ -44,17 +44,17 @@ Definition labels_branched_to (c: code) : Labelset.t := (** Remove label declarations for labels that are not in the [bto] (branched-to) set. *) -Fixpoint remove_unused_labels (bto: Labelset.t) (c: code) : code := - match c with - | nil => nil - | Llabel lbl :: c' => - if Labelset.mem lbl bto - then Llabel lbl :: remove_unused_labels bto c' - else remove_unused_labels bto c' - | i :: c' => - i :: remove_unused_labels bto c' +Definition remove_unused (bto: Labelset.t) (i: instruction) (k: code) : code := + match i with + | Llabel lbl => + if Labelset.mem lbl bto then i :: k else k + | _ => + i :: k end. +Definition remove_unused_labels (bto: Labelset.t) (c: code) : code := + list_fold_right (remove_unused bto) c nil. + Definition cleanup_labels (c: code) := remove_unused_labels (labels_branched_to c) c. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index dbd33c1..70f0eb3 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -143,6 +143,20 @@ Qed. (** Commutation with [find_label]. *) +Lemma remove_unused_labels_cons: + forall bto i c, + remove_unused_labels bto (i :: c) = + match i with + | Llabel lbl => + if Labelset.mem lbl bto then i :: remove_unused_labels bto c else remove_unused_labels bto c + | _ => + i :: remove_unused_labels bto c + end. +Proof. + unfold remove_unused_labels; intros. rewrite list_fold_right_eq. auto. +Qed. + + Lemma find_label_commut: forall lbl bto, Labelset.In lbl bto -> @@ -152,6 +166,7 @@ Lemma find_label_commut: Proof. induction c; simpl; intros. congruence. + rewrite remove_unused_labels_cons. unfold is_label in H0. destruct a; simpl; auto. destruct (peq lbl l). subst l. inv H0. rewrite Labelset.mem_1; auto. @@ -222,7 +237,7 @@ Theorem transf_step_correct: (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; simpl. + induction 1; intros; inv MS; try rewrite remove_unused_labels_cons. (* Lop *) left; econstructor; split. econstructor; eauto. instantiate (1 := v). rewrite <- H. @@ -263,7 +278,7 @@ Proof. constructor. econstructor; eauto with coqlib. (* eliminated *) - right. split. omega. split. auto. econstructor; eauto with coqlib. + right. split. simpl. omega. split. auto. econstructor; eauto with coqlib. (* Lgoto *) left; econstructor; split. econstructor. eapply find_label_translated; eauto. red; auto. diff --git a/backend/CleanupLabelstyping.v b/backend/CleanupLabelstyping.v index f58a910..11b516f 100644 --- a/backend/CleanupLabelstyping.v +++ b/backend/CleanupLabelstyping.v @@ -24,9 +24,9 @@ Require Import LTLintyping. Lemma in_remove_unused_labels: forall bto i c, In i (remove_unused_labels bto c) -> In i c. Proof. - induction c; simpl. + unfold remove_unused_labels, remove_unused. induction c; simpl. auto. - destruct a; simpl; intuition. + rewrite list_fold_right_eq. destruct a; simpl; intuition. destruct (Labelset.mem l bto); simpl in H; intuition. Qed. diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml index ddd3094..09ffb8e 100644 --- a/backend/Coloringaux.ml +++ b/backend/Coloringaux.ml @@ -91,7 +91,7 @@ let name_of_node n = | Some s -> s end | Some(S _), _ -> "fixed-slot" - | None, Some r -> Printf.sprintf "x%ld" (camlint_of_positive r) + | None, Some r -> Printf.sprintf "x%ld" (P.to_int32 r) | None, None -> "unknown-reg" *) @@ -602,12 +602,15 @@ let rec getAlias n = (* Combine two nodes *) let combine u v = - (*i Printf.printf "Combining %s and %s\n" (name_of_node u) (name_of_node v);*) + (*i Printf.printf "Combining %s and %s\n" (name_of_node u) (name_of_node v); *) if v.nstate = FreezeWorklist then DLinkNode.move v freezeWorklist coalescedNodes else DLinkNode.move v spillWorklist coalescedNodes; v.alias <- Some u; - u.movelist <- u.movelist @ v.movelist; + (* Precolored nodes often have big movelists, and if one of [u] and [v] + is precolored, it is []u. So, append [v.movelist] to [u.movelist] + instead of the other way around. *) + u.movelist <- List.rev_append v.movelist u.movelist; u.spillcost <- u.spillcost +. v.spillcost; iterAdjacent (combineEdge u) v; (*r original code using [decrementDegree] is buggy *) enableMoves v; (*r added as per Appel's book erratum *) diff --git a/backend/Constprop.v b/backend/Constprop.v index 2f3123f..f85405d 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -24,6 +24,7 @@ Require Import Registers. Require Import RTL. Require Import Lattice. Require Import Kildall. +Require Import Liveness. Require Import ConstpropOp. (** * Static analysis *) @@ -211,6 +212,18 @@ Definition transfer (gapp: global_approx) (f: function) (pc: node) (before: D.t) end end. +(** To reduce the size of approximations, we preventively set to [Top] + the approximations of registers used for the last time in the + current instruction. *) + +Definition transfer' (gapp: global_approx) (f: function) (lastuses: PTree.t (list reg)) + (pc: node) (before: D.t) := + let after := transfer gapp f pc before in + match lastuses!pc with + | None => after + | Some regs => List.fold_left (fun a r => D.set r Unknown a) regs after + end. + (** The static analysis itself is then an instantiation of Kildall's generic solver for forward dataflow inequations. [analyze f] returns a mapping from program points to mappings of pseudo-registers @@ -221,7 +234,8 @@ Definition transfer (gapp: global_approx) (f: function) (pc: node) (before: D.t) Module DS := Dataflow_Solver(D)(NodeSetForward). Definition analyze (gapp: global_approx) (f: RTL.function): PMap.t D.t := - match DS.fixpoint (successors f) (transfer gapp f) + let lu := Liveness.last_uses f in + match DS.fixpoint (successors f) (transfer' gapp f lu) ((f.(fn_entrypoint), D.top) :: nil) with | None => PMap.init D.top | Some res => res diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index b223e89..580d551 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -26,6 +26,7 @@ Require Import Registers. Require Import RTL. Require Import Lattice. Require Import Kildall. +Require Import Liveness. Require Import ConstpropOp. Require Import Constprop. Require Import ConstpropOpproof. @@ -95,6 +96,18 @@ Proof. constructor. apply H. auto. Qed. +Lemma regs_match_approx_forget: + forall rs rl ra, + regs_match_approx ra rs -> + regs_match_approx (List.fold_left (fun a r => D.set r Unknown a) rl ra) rs. +Proof. + induction rl; simpl; intros. + auto. + apply IHrl. red; intros. destruct (peq r a). + subst a. rewrite D.gss. constructor. + rewrite D.gso; auto. +Qed. + (** The correctness of the static analysis follows from the results of module [ConstpropOpproof] and the fact that the result of the static analysis is a solution of the forward dataflow inequations. *) @@ -106,13 +119,15 @@ Lemma analyze_correct_1: regs_match_approx (transfer gapp f pc (analyze gapp f)!!pc) rs -> regs_match_approx (analyze gapp f)!!pc' rs. Proof. - intros until i. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer gapp f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. - apply regs_match_approx_increasing with (transfer gapp f pc approxs!!pc). + unfold analyze; intros. + set (lu := last_uses f) in *. + destruct (DS.fixpoint (successors f) (transfer' gapp f lu) + ((fn_entrypoint f, D.top) :: nil)) as [approxs|] eqn:FIX. + apply regs_match_approx_increasing with (transfer' gapp f lu pc approxs!!pc). eapply DS.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto. + unfold successors_list, successors. rewrite PTree.gmap1. rewrite H. auto. + unfold transfer'. destruct (lu!pc) as [regs|]. + apply regs_match_approx_forget; auto. auto. intros. rewrite PMap.gi. apply regs_match_approx_top. Qed. @@ -122,9 +137,9 @@ Lemma analyze_correct_3: regs_match_approx (analyze gapp f)!!(f.(fn_entrypoint)) rs. Proof. intros. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer gapp f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. + set (lu := last_uses f) in *. + destruct (DS.fixpoint (successors f) (transfer' gapp f lu) + ((fn_entrypoint f, D.top) :: nil)) as [approxs|] eqn:FIX. apply regs_match_approx_increasing with D.top. eapply DS.fixpoint_entry; eauto. auto with coqlib. apply regs_match_approx_top. diff --git a/backend/Linearize.v b/backend/Linearize.v index 636cb22..6fc8e48 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -198,17 +198,15 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code := (** Linearize a function body according to an enumeration of its nodes. *) -Fixpoint linearize_body (f: LTL.function) (enum: list node) - {struct enum} : code := - match enum with - | nil => nil - | pc :: rem => - match f.(LTL.fn_code)!pc with - | None => linearize_body f rem - | Some b => Llabel pc :: linearize_instr b (linearize_body f rem) - end +Definition linearize_node (f: LTL.function) (pc: node) (k: code) : code := + match f.(LTL.fn_code)!pc with + | None => k + | Some b => Llabel pc :: linearize_instr b k end. +Definition linearize_body (f: LTL.function) (enum: list node) : code := + list_fold_right (linearize_node f) enum nil. + (** * Entry points for code linearization *) Definition transf_function (f: LTL.function) : res LTLin.function := diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index b72268a..d368311 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -293,6 +293,18 @@ Proof. case (starts_with n k); simpl; auto. Qed. +Remark linearize_body_cons: + forall f pc enum, + linearize_body f (pc :: enum) = + match f.(LTL.fn_code)!pc with + | None => linearize_body f enum + | Some b => Llabel pc :: linearize_instr b (linearize_body f enum) + end. +Proof. + intros. unfold linearize_body. rewrite list_fold_right_eq. + unfold linearize_node. destruct (LTL.fn_code f)!pc; auto. +Qed. + Lemma find_label_lin_rec: forall f enum pc b, In pc enum -> @@ -301,12 +313,13 @@ Lemma find_label_lin_rec: Proof. induction enum; intros. elim H. - case (peq a pc); intro. + rewrite linearize_body_cons. + destruct (peq a pc). subst a. exists (linearize_body f enum). - simpl. rewrite H0. simpl. rewrite peq_true. auto. + rewrite H0. simpl. rewrite peq_true. auto. assert (In pc enum). simpl in H. tauto. - elim (IHenum pc b H1 H0). intros k FIND. - exists k. simpl. destruct (LTL.fn_code f)!a. + destruct (IHenum pc b H1 H0) as [k FIND]. + exists k. destruct (LTL.fn_code f)!a. simpl. rewrite peq_false. rewrite find_label_lin_instr. auto. auto. auto. Qed. @@ -377,7 +390,7 @@ Lemma label_in_lin_rec: Proof. induction enum. simpl; auto. - simpl. destruct (LTL.fn_code f)!a. + rewrite linearize_body_cons. destruct (LTL.fn_code f)!a. simpl. intros [A|B]. left; congruence. right. apply IHenum. eapply label_in_lin_instr; eauto. intro; right; auto. @@ -406,7 +419,8 @@ Lemma unique_labels_lin_rec: Proof. induction enum. simpl; auto. - intro. simpl. destruct (LTL.fn_code f)!a. + rewrite linearize_body_cons. + intro. destruct (LTL.fn_code f)!a. simpl. split. red. intro. inversion H. elim H3. apply label_in_lin_rec with f. apply label_in_lin_instr with i. auto. diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index 7393535..b4e25de 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -71,9 +71,9 @@ Lemma wt_linearize_body: forall enum, wt_code f.(LTL.fn_sig) (linearize_body f enum). Proof. - induction enum; simpl. + unfold linearize_body; induction enum; rewrite list_fold_right_eq. red; simpl; intros; contradiction. - caseEq ((LTL.fn_code f)!a); intros. + unfold linearize_node. caseEq ((LTL.fn_code f)!a); intros. apply wt_add_instr. constructor. apply wt_linearize_instr; eauto with coqlib. auto. Qed. diff --git a/backend/Liveness.v b/backend/Liveness.v new file mode 100644 index 0000000..b97455f --- /dev/null +++ b/backend/Liveness.v @@ -0,0 +1,147 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Liveness analysis over RTL *) + +Require Import Coqlib. +Require Import Maps. +Require Import Lattice. +Require Import AST. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import Kildall. + +(** A register [r] is live at a point [p] if there exists a path + from [p] to some instruction that uses [r] as argument, + and [r] is not redefined along this path. + Liveness can be computed by a backward dataflow analysis. + The analysis operates over sets of (live) pseudo-registers. *) + +Notation reg_live := Regset.add. +Notation reg_dead := Regset.remove. + +Definition reg_option_live (or: option reg) (lv: Regset.t) := + match or with None => lv | Some r => reg_live r lv end. + +Definition reg_sum_live (ros: reg + ident) (lv: Regset.t) := + match ros with inl r => reg_live r lv | inr s => lv end. + +Fixpoint reg_list_live + (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t := + match rl with + | nil => lv + | r1 :: rs => reg_list_live rs (reg_live r1 lv) + end. + +Fixpoint reg_list_dead + (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t := + match rl with + | nil => lv + | r1 :: rs => reg_list_dead rs (reg_dead r1 lv) + end. + +(** Here is the transfer function for the dataflow analysis. + Since this is a backward dataflow analysis, it takes as argument + the abstract register set ``after'' the given instruction, + i.e. the registers that are live after; and it returns as result + the abstract register set ``before'' the given instruction, + i.e. the registers that must be live before. + The general relation between ``live before'' and ``live after'' + an instruction is that a register is live before if either + it is one of the arguments of the instruction, or it is not the result + of the instruction and it is live after. + However, if the result of a side-effect-free instruction is not + live ``after'', the whole instruction will be removed later + (since it computes a useless result), thus its arguments need not + be live ``before''. *) + +Definition transfer + (f: function) (pc: node) (after: Regset.t) : Regset.t := + match f.(fn_code)!pc with + | None => + Regset.empty + | Some i => + match i with + | Inop s => + after + | Iop op args res s => + if Regset.mem res after then + reg_list_live args (reg_dead res after) + else + after + | Iload chunk addr args dst s => + if Regset.mem dst after then + reg_list_live args (reg_dead dst after) + else + after + | Istore chunk addr args src s => + reg_list_live args (reg_live src after) + | Icall sig ros args res s => + reg_list_live args + (reg_sum_live ros (reg_dead res after)) + | Itailcall sig ros args => + reg_list_live args (reg_sum_live ros Regset.empty) + | Ibuiltin ef args res s => + reg_list_live args (reg_dead res after) + | Icond cond args ifso ifnot => + reg_list_live args after + | Ijumptable arg tbl => + reg_live arg after + | Ireturn optarg => + reg_option_live optarg Regset.empty + end + end. + +(** The liveness analysis is then obtained by instantiating the + general framework for backward dataflow analysis provided by + module [Kildall]. *) + +Module RegsetLat := LFSet(Regset). +Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward). + +Definition analyze (f: function): option (PMap.t Regset.t) := + DS.fixpoint (successors f) (transfer f) nil. + +(** Basic property of the liveness information computed by [analyze]. *) + +Lemma analyze_solution: + forall f live n i s, + analyze f = Some live -> + f.(fn_code)!n = Some i -> + In s (successors_instr i) -> + Regset.Subset (transfer f s live!!s) live!!n. +Proof. + unfold analyze; intros. eapply DS.fixpoint_solution; eauto. + unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. simpl. auto. +Qed. + +(** Given an RTL function, compute (for every PC) the list of + pseudo-registers that are used for the last time in the instruction + at PC. These are the registers that are used or defined by the instruction + and dead afterwards. *) + +Definition last_uses_at (live: PMap.t Regset.t) (pc: node) (i: instruction) : list reg := + let l := live!!pc in + let lu := List.filter (fun r => negb (Regset.mem r l)) (instr_uses i) in + match instr_defs i with + | None => lu + | Some r => if Regset.mem r l then lu else r :: lu + end. + +Definition last_uses (f: function) : PTree.t (list reg) := + match analyze f with + | None => PTree.empty (list reg) + | Some live => PTree.map (last_uses_at live) f.(fn_code) + end. + + diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index ef6ba1d..01ea1e6 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -255,7 +255,7 @@ let print_function p id f = fprintf p "@;<0 -2>}@]@ " let print_extfun p id ef = - fprintf p "@[<v 0>extern @[<hov 2>\"%s\" =@ %s :@ %a@]@ " + fprintf p "@[<v 0>extern @[<hov 2>\"%s\" =@ %s :@ %a@]@]@ " (extern_atom id) (name_of_external ef) print_sig (ef_sig ef) let print_init_data p = function diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 0bafcde..0cdf505 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -95,7 +95,7 @@ let print_function pp id f = let instrs = List.sort (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) - (List.map + (List.rev_map (fun (pc, i) -> (P.to_int32 pc, i)) (PTree.elements f.fn_code)) in print_succ pp f.fn_entrypoint diff --git a/backend/RRE.v b/backend/RRE.v index b8409e3..bee57f6 100644 --- a/backend/RRE.v +++ b/backend/RRE.v @@ -109,57 +109,61 @@ Fixpoint safe_move_insertion (c: code) : bool := into register-to-register move whenever possible. Simultaneously, it propagates valid (register, slot) equations across basic blocks. *) -Fixpoint transf_code (eqs: equations) (c: code) : code := +(** [transf_code] is written in accumulator-passing style so that it runs + in constant stack space. The [k] parameter accumulates the instructions + to be generated, in reverse order, and is then reversed at the end *) + +Fixpoint transf_code (eqs: equations) (c: code) (k: code) : code := match c with - | nil => nil + | nil => List.rev' k | Lgetstack s r :: c => if is_incoming s then - Lgetstack s r :: transf_code (kill_loc (R r) (kill_loc (R IT1) eqs)) c + transf_code (kill_loc (R r) (kill_loc (R IT1) eqs)) c (Lgetstack s r :: k) else if contains_equation s r eqs then - transf_code eqs c + transf_code eqs c k else match find_reg_containing s eqs with | Some r' => if safe_move_insertion c then - Lop Omove (r' :: nil) r :: transf_code (kill_at_move (mkeq r s :: kill_loc (R r) eqs)) c + transf_code (kill_at_move (mkeq r s :: kill_loc (R r) eqs)) c (Lop Omove (r' :: nil) r :: k) else - Lgetstack s r:: transf_code (mkeq r s :: kill_loc (R r) eqs) c + transf_code (mkeq r s :: kill_loc (R r) eqs) c (Lgetstack s r :: k) | None => - Lgetstack s r:: transf_code (mkeq r s :: kill_loc (R r) eqs) c + transf_code (mkeq r s :: kill_loc (R r) eqs) c (Lgetstack s r :: k) end | Lsetstack r s :: c => - Lsetstack r s :: transf_code (kill_at_move (mkeq r s :: kill_loc (S s) eqs)) c + transf_code (kill_at_move (mkeq r s :: kill_loc (S s) eqs)) c (Lsetstack r s :: k) | Lop op args res :: c => - Lop op args res :: transf_code (kill_loc (R res) (kill_op op eqs)) c + transf_code (kill_loc (R res) (kill_op op eqs)) c (Lop op args res :: k) | Lload chunk addr args res :: c => - Lload chunk addr args res :: transf_code (kill_loc (R res) (kill_temps eqs)) c + transf_code (kill_loc (R res) (kill_temps eqs)) c (Lload chunk addr args res :: k) | Lstore chunk addr args src :: c => - Lstore chunk addr args src :: transf_code (kill_temps eqs) c + transf_code (kill_temps eqs) c (Lstore chunk addr args src :: k) | Lcall sg ros :: c => - Lcall sg ros :: transf_code nil c + transf_code nil c (Lcall sg ros :: k) | Ltailcall sg ros :: c => - Ltailcall sg ros :: transf_code nil c + transf_code nil c (Ltailcall sg ros :: k) | Lbuiltin ef args res :: c => - Lbuiltin ef args res :: transf_code (kill_loc (R res) (kill_temps eqs)) c + transf_code (kill_loc (R res) (kill_temps eqs)) c (Lbuiltin ef args res :: k) | Lannot ef args :: c => - Lannot ef args :: transf_code eqs c + transf_code eqs c (Lannot ef args :: k) | Llabel lbl :: c => - Llabel lbl :: transf_code nil c + transf_code nil c (Llabel lbl :: k) | Lgoto lbl :: c => - Lgoto lbl :: transf_code nil c + transf_code nil c (Lgoto lbl :: k) | Lcond cond args lbl :: c => - Lcond cond args lbl :: transf_code (kill_temps eqs) c + transf_code (kill_temps eqs) c (Lcond cond args lbl :: k) | Ljumptable arg lbls :: c => - Ljumptable arg lbls :: transf_code nil c + transf_code nil c (Ljumptable arg lbls :: k) | Lreturn :: c => - Lreturn :: transf_code nil c + transf_code nil c (Lreturn :: k) end. Definition transf_function (f: function) : function := mkfunction (fn_sig f) (fn_stacksize f) - (transf_code nil (fn_code f)). + (transf_code nil (fn_code f) nil). Definition transf_fundef (fd: fundef) : fundef := transf_fundef transf_function fd. diff --git a/backend/RREproof.v b/backend/RREproof.v index 40632f7..98de7a8 100644 --- a/backend/RREproof.v +++ b/backend/RREproof.v @@ -280,18 +280,44 @@ Proof. destruct op; exact agree_undef_temps || exact agree_undef_move_2. Qed. +Lemma transf_code_cont: + forall c eqs k1 k2, + transf_code eqs c (k1 ++ k2) = List.rev k2 ++ transf_code eqs c k1. +Proof. + induction c; simpl; intros. + unfold rev'; rewrite <- ! rev_alt; apply rev_app_distr. + destruct a; try (rewrite <- IHc; reflexivity). + destruct (is_incoming s). + rewrite <- IHc; reflexivity. + destruct (contains_equation s m eqs). + auto. + destruct (find_reg_containing s eqs). + destruct (safe_move_insertion c). + rewrite <- IHc; reflexivity. + rewrite <- IHc; reflexivity. + rewrite <- IHc; reflexivity. +Qed. + +Corollary transf_code_eq: + forall eqs c i, transf_code eqs c (i :: nil) = i :: transf_code eqs c nil. +Proof. + intros. change (i :: nil) with (nil ++ (i :: nil)). + rewrite transf_code_cont. auto. +Qed. + Lemma transl_find_label: forall lbl c eqs, - find_label lbl (transf_code eqs c) = - option_map (transf_code nil) (find_label lbl c). + find_label lbl (transf_code eqs c nil) = + option_map (fun c => transf_code nil c nil) (find_label lbl c). Proof. - induction c; simpl; intros. + induction c; intros. auto. - destruct a; simpl; auto. + destruct a; simpl; try (rewrite transf_code_eq; simpl; auto). destruct (is_incoming s); simpl; auto. - destruct (contains_equation s m eqs); auto. - destruct (find_reg_containing s eqs); simpl; auto. - destruct (safe_move_insertion c); simpl; auto. + destruct (contains_equation s m eqs). auto. + destruct (find_reg_containing s eqs); rewrite !transf_code_eq. + destruct (safe_move_insertion c); simpl; auto. + simpl; auto. destruct (peq lbl l); simpl; auto. Qed. @@ -348,7 +374,7 @@ Inductive match_frames: stackframe -> stackframe -> Prop := | match_frames_intro: forall f sp rs c, match_frames (Stackframe f sp rs c) - (Stackframe (transf_function f) sp rs (transf_code nil c)). + (Stackframe (transf_function f) sp rs (transf_code nil c nil)). Inductive match_states: state -> state -> Prop := | match_states_regular: @@ -358,7 +384,7 @@ Inductive match_states: state -> state -> Prop := (AG: agree sm rs rs') (SAFE: sm = false \/ safe_move_insertion c = true), match_states (State stk f sp c rs m) - (State stk' (transf_function f) sp (transf_code eqs c) rs' m) + (State stk' (transf_function f) sp (transf_code eqs c nil) rs' m) | match_states_call: forall stk f rs m stk' (STK: list_forall2 match_frames stk stk'), @@ -400,7 +426,8 @@ Opaque destroyed_at_move_regs. (* incoming, stays as getstack *) assert (UGS: forall rs, undef_getstack sl rs = Locmap.set (R IT1) Vundef rs). destruct sl; simpl in Heqb0; discriminate || auto. - left; econstructor; split. constructor. + left; econstructor; split. + rewrite transf_code_eq; constructor. repeat rewrite UGS. apply match_states_regular with sm. auto. apply kill_loc_hold. apply kill_loc_hold; auto. @@ -424,20 +451,23 @@ Opaque destroyed_at_move_regs. simpl; intro EQ. (* turned into a move *) destruct (safe_move_insertion b) eqn:?. - left; econstructor; split. constructor. simpl; eauto. + left; econstructor; split. + rewrite transf_code_eq. constructor. simpl; eauto. rewrite UGS. rewrite <- EQ. apply match_states_regular with true; auto. apply eqs_movestack_hold; auto. rewrite (agree_slot _ _ _ sl AG). apply agree_set. eapply agree_undef_move_1; eauto. (* left as a getstack *) - left; econstructor; split. constructor. + left; econstructor; split. + rewrite transf_code_eq. constructor. repeat rewrite UGS. apply match_states_regular with sm. auto. apply eqs_getstack_hold; auto. rewrite (agree_slot _ _ _ sl AG). apply agree_set. auto. intuition congruence. (* no equation, left as a getstack *) - left; econstructor; split. constructor. + left; econstructor; split. + rewrite transf_code_eq; constructor. repeat rewrite UGS. apply match_states_regular with sm. auto. apply eqs_getstack_hold; auto. @@ -445,14 +475,14 @@ Opaque destroyed_at_move_regs. tauto. (* setstack *) - left; econstructor; split. constructor. + left; econstructor; split. rewrite transf_code_eq; constructor. apply match_states_regular with false; auto. apply eqs_setstack_hold; auto. rewrite (agree_reg _ _ _ r AG). apply agree_set. eapply agree_undef_move_2; eauto. simpl in SAFE. destruct (in_dec mreg_eq r destroyed_at_move_regs); simpl in SAFE; intuition congruence. (* op *) - left; econstructor; split. constructor. + left; econstructor; split. rewrite transf_code_eq; constructor. instantiate (1 := v). rewrite <- H. rewrite (agree_regs _ _ _ args AG). apply eval_operation_preserved. exact symbols_preserved. @@ -463,7 +493,7 @@ Opaque destroyed_at_move_regs. (* load *) left; econstructor; split. - econstructor. instantiate (1 := a). rewrite <- H. + rewrite transf_code_eq; econstructor. instantiate (1 := a). rewrite <- H. rewrite (agree_regs _ _ _ args AG). apply eval_addressing_preserved. exact symbols_preserved. simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence. @@ -480,7 +510,7 @@ Opaque list_disjoint_dec. destruct (list_disjoint_dec mreg_eq (src :: args) destroyed_at_move_regs); try discriminate. split. eapply list_disjoint_notin; eauto with coqlib. eapply list_disjoint_cons_left; eauto. left; econstructor; split. - econstructor. instantiate (1 := a). rewrite <- H. + rewrite transf_code_eq; econstructor. instantiate (1 := a). rewrite <- H. rewrite (agree_regs _ _ _ args AG). apply eval_addressing_preserved. exact symbols_preserved. tauto. @@ -495,7 +525,7 @@ Opaque list_disjoint_dec. simpl in SAFE. assert (sm = false) by intuition congruence. subst sm. rewrite agree_false in AG. subst rs'. left; econstructor; split. - constructor. eapply find_function_translated; eauto. + rewrite transf_code_eq; constructor. eapply find_function_translated; eauto. symmetry; apply sig_preserved. constructor. constructor; auto. constructor. @@ -503,13 +533,13 @@ Opaque list_disjoint_dec. simpl in SAFE. assert (sm = false) by intuition congruence. subst sm. rewrite agree_false in AG. subst rs'. left; econstructor; split. - constructor. eapply find_function_translated; eauto. + rewrite transf_code_eq; constructor. eapply find_function_translated; eauto. symmetry; apply sig_preserved. eauto. rewrite (match_parent_locset _ _ STK). constructor; auto. (* builtin *) left; econstructor; split. - constructor. + rewrite transf_code_eq; constructor. rewrite (agree_regs _ _ _ args AG). eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. @@ -522,20 +552,20 @@ Opaque list_disjoint_dec. simpl in SAFE. assert (sm = false) by intuition congruence. subst sm. rewrite agree_false in AG. subst rs'. left; econstructor; split. - econstructor. eapply external_call_symbols_preserved; eauto. + rewrite transf_code_eq; econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. apply match_states_regular with false; auto. rewrite agree_false; auto. (* label *) - left; econstructor; split. constructor. + left; econstructor; split. rewrite transf_code_eq; constructor. apply match_states_regular with false; auto. apply nil_hold. simpl in SAFE. destruct SAFE. subst sm. auto. congruence. (* goto *) generalize (transl_find_label lbl (fn_code f) nil). rewrite H. simpl. intros. - left; econstructor; split. constructor; eauto. + left; econstructor; split. rewrite transf_code_eq; constructor; eauto. apply match_states_regular with false; auto. apply nil_hold. simpl in SAFE. destruct SAFE. subst sm. auto. congruence. @@ -543,7 +573,7 @@ Opaque list_disjoint_dec. (* cond true *) generalize (transl_find_label lbl (fn_code f) nil). rewrite H0. simpl. intros. left; econstructor; split. - apply exec_Lcond_true; auto. + rewrite transf_code_eq; apply exec_Lcond_true; auto. rewrite (agree_regs _ _ _ args AG). auto. simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence. eauto. @@ -552,7 +582,7 @@ Opaque list_disjoint_dec. eapply agree_undef_temps; eauto. (* cond false *) - left; econstructor; split. apply exec_Lcond_false; auto. + left; econstructor; split. rewrite transf_code_eq; apply exec_Lcond_false; auto. rewrite (agree_regs _ _ _ args AG). auto. simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence. apply match_states_regular with false; auto. @@ -561,7 +591,7 @@ Opaque list_disjoint_dec. (* jumptable *) generalize (transl_find_label lbl (fn_code f) nil). rewrite H1. simpl. intros. - left; econstructor; split. econstructor; eauto. + left; econstructor; split. rewrite transf_code_eq; econstructor; eauto. rewrite (agree_reg _ _ _ arg AG). auto. simpl in SAFE. destruct (in_dec mreg_eq arg destroyed_at_move_regs); simpl in SAFE; intuition congruence. apply match_states_regular with false; auto. @@ -571,7 +601,7 @@ Opaque list_disjoint_dec. (* return *) simpl in SAFE. destruct SAFE; try discriminate. subst sm. rewrite agree_false in AG. subst rs'. left; econstructor; split. - constructor. simpl. eauto. + rewrite transf_code_eq; constructor. simpl. eauto. rewrite (match_parent_locset _ _ STK). constructor; auto. diff --git a/backend/RREtyping.v b/backend/RREtyping.v index 539fb20..170d8ad 100644 --- a/backend/RREtyping.v +++ b/backend/RREtyping.v @@ -83,19 +83,20 @@ Hint Resolve wt_kill_op: linearty. Lemma wt_transf_code: forall f c eqs, wt_code f c -> wt_eqs eqs -> - wt_code (transf_function f) (transf_code eqs c). + wt_code (transf_function f) (transf_code eqs c nil). Proof. induction c; intros; simpl. red; simpl; tauto. assert (WI: wt_instr f a) by auto with coqlib. assert (WC: wt_code f c) by (red; auto with coqlib). clear H. - inv WI; auto 10 with linearty. + inv WI; rewrite ? transf_code_eq; auto 10 with linearty. destruct (is_incoming s) eqn:?. auto with linearty. destruct (contains_equation s r eqs). auto with linearty. destruct (find_reg_containing s eqs) as [r'|] eqn:?; auto with linearty. assert (mreg_type r' = mreg_type r). exploit H0. eapply find_reg_containing_sound; eauto. simpl. congruence. + rewrite ! transf_code_eq. destruct (safe_move_insertion c); auto 10 with linearty. Qed. diff --git a/backend/Reload.v b/backend/Reload.v index 31bddcd..be844b3 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -257,7 +257,7 @@ Definition transf_instr end. Definition transf_code (f: LTLin.function) (c: LTLin.code) : code := - List.fold_right (transf_instr f) nil c. + list_fold_right (transf_instr f) c nil. Definition transf_function (f: LTLin.function) : function := mkfunction diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 6402237..fe6e475 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -837,6 +837,12 @@ Proof. destruct o; FL. Qed. +Lemma transf_code_cons: + forall f i c, transf_code f (i :: c) = transf_instr f i (transf_code f c). +Proof. + unfold transf_code; intros. rewrite list_fold_right_eq; auto. +Qed. + Lemma find_label_transf_code: forall sg lbl c, find_label lbl (transf_code sg c) = @@ -844,6 +850,7 @@ Lemma find_label_transf_code: Proof. induction c; simpl. auto. + rewrite transf_code_cons. rewrite find_label_transf_instr. destruct (LTLin.is_label lbl a); auto. Qed. @@ -1022,7 +1029,7 @@ Theorem transf_step_correct: \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat. Proof. Opaque regs_for. Opaque add_reloads. - induction 1; intros; try inv MS; simpl. + induction 1; intros; try inv MS; try rewrite transf_code_cons; simpl. (* Lop *) ExploitWT. inv WTI. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index c005139..70d79bc 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -317,6 +317,7 @@ Lemma wt_transf_code: Proof. induction c; simpl; intros. red; simpl; tauto. + rewrite transf_code_cons. apply wt_transf_instr; auto with coqlib. apply IHc. red; auto with coqlib. Qed. diff --git a/backend/Stacking.v b/backend/Stacking.v index 732443b..03e882e 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -207,7 +207,7 @@ Definition transl_instr Definition transl_code (fe: frame_env) (il: list Linear.instruction) : Mach.code := - List.fold_right (transl_instr fe) nil il. + list_fold_right (transl_instr fe) il nil. Definition transl_body (f: Linear.function) (fe: frame_env) := save_callee_save fe (transl_code fe f.(Linear.fn_code)). diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d97ec93..a73f0aa 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1997,6 +1997,12 @@ Proof. intro; reflexivity. Qed. +Lemma transl_code_eq: + forall fe i c, transl_code fe (i :: c) = transl_instr fe i (transl_code fe c). +Proof. + unfold transl_code; intros. rewrite list_fold_right_eq. auto. +Qed. + Lemma find_label_transl_code: forall fe lbl c, Mach.find_label lbl (transl_code fe c) = @@ -2004,6 +2010,7 @@ Lemma find_label_transl_code: Proof. induction c; simpl; intros. auto. + rewrite transl_code_eq. destruct a; unfold transl_instr; auto. destruct s; simpl; auto. destruct s; simpl; auto. @@ -2089,7 +2096,8 @@ Qed. Lemma is_tail_transl_code: forall fe c1 c2, is_tail c1 c2 -> is_tail (transl_code fe c1) (transl_code fe c2). Proof. - induction 1; simpl. auto with coqlib. + induction 1; simpl. auto with coqlib. + rewrite transl_code_eq. eapply is_tail_trans. eauto. apply is_tail_transl_instr. Qed. @@ -2364,14 +2372,9 @@ Theorem transf_step_correct: forall s1' (MS: match_states s1 s1'), exists s2', plus step tge s1' t s2' /\ match_states s2 s2'. Proof. - assert (RED: forall f i c, - transl_code (make_env (function_bounds f)) (i :: c) = - transl_instr (make_env (function_bounds f)) i - (transl_code (make_env (function_bounds f)) c)). - intros. reflexivity. induction 1; intros; try inv MS; - try rewrite RED; + try rewrite transl_code_eq; try (generalize (WTF _ (is_tail_in TAIL)); intro WTI); try (generalize (function_is_within_bounds f WTF _ (is_tail_in TAIL)); intro BOUND; simpl in BOUND); @@ -2512,7 +2515,8 @@ Proof. (* Lcall *) exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. - exploit is_tail_transf_function; eauto. intros IST. simpl in IST. + exploit is_tail_transf_function; eauto. intros IST. + rewrite transl_code_eq in IST. simpl in IST. exploit return_address_offset_exists. eexact IST. intros [ra D]. econstructor; split. diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index a7a629b..6e3ccf8 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -528,28 +528,46 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (** Translation of a code sequence *) -Definition edx_preserved (before: bool) (i: Mach.instruction) : bool := +Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool := match i with | Msetstack src ofs ty => before | Mgetparam ofs ty dst => negb (mreg_eq dst IT1) | _ => false end. -Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (edx_is_parent: bool) := +(** This is the naive definition that we no longer use because it + is not tail-recursive. It is kept as specification. *) + +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := match il with | nil => OK nil | i1 :: il' => - do k <- transl_code f il' (edx_preserved edx_is_parent i1); - transl_instr f i1 edx_is_parent k + do k <- transl_code f il' (it1_is_parent it1p i1); + transl_instr f i1 it1p k end. +(** This is an equivalent definition in continuation-passing style + that runs in constant stack space. *) + +Fixpoint transl_code_rec (f: Mach.function) (il: list Mach.instruction) + (it1p: bool) (k: code -> res code) := + match il with + | nil => k nil + | i1 :: il' => + transl_code_rec f il' (it1_is_parent it1p i1) + (fun c1 => do c2 <- transl_instr f i1 it1p c1; k c2) + end. + +Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := + transl_code_rec f il it1p (fun c => OK c). + (** Translation of a whole function. Note that we must check that the generated code contains less than [2^32] instructions, otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions. *) Definition transf_function (f: Mach.function) : res Asm.code := - do c <- transl_code f f.(Mach.fn_code) true; + do c <- transl_code' f f.(Mach.fn_code) true; if zlt (list_length_z c) Int.max_unsigned then OK (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c) else Error (msg "code size exceeded"). diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 060d018..e43392a 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -332,7 +332,7 @@ Lemma transl_find_label: end. Proof. intros. monadInv H. destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0. - simpl. eapply transl_code_label; eauto. + simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ; eauto. Qed. End TRANSL_LABEL. @@ -375,6 +375,7 @@ Proof. destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. - intros. monadInv H0. destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0. + rewrite transl_code'_transl_code in EQ. exists x; exists true; split; auto. unfold fn_code. repeat constructor. - exact transf_function_no_overflow. Qed. @@ -436,7 +437,7 @@ Lemma exec_straight_steps: exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' /\ agree ms2 sp rs2 - /\ (edx_preserved ep i = true -> rs2#EDX = parent_sp s)) -> + /\ (it1_is_parent ep i = true -> rs2#EDX = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ match_states (Mach.State s fb sp c ms2 m2) st'. @@ -455,7 +456,7 @@ Lemma exec_straight_steps_goto: Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl f.(Mach.fn_code) = Some c' -> transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> - edx_preserved ep i = false -> + it1_is_parent ep i = false -> (forall k c (TR: transl_instr f i ep k = OK c), exists jmp, exists k', exists rs2, exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' @@ -868,7 +869,7 @@ Opaque loadind. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. - generalize EQ; intros EQ'. monadInv EQ'. + generalize EQ; intros EQ'. monadInv EQ'. rewrite transl_code'_transl_code in EQ0. destruct (zlt (list_length_z x0) Int.max_unsigned); inversion EQ1. clear EQ1. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. diff --git a/ia32/PrintOp.ml b/ia32/PrintOp.ml index f76416a..7ddf42f 100644 --- a/ia32/PrintOp.ml +++ b/ia32/PrintOp.ml @@ -64,6 +64,7 @@ let print_operation reg pp = function | Omove, [r1] -> reg pp r1 | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n) | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n) + | Oindirectsymbol id, [] -> fprintf pp "&%s" (extern_atom id) | Ocast8signed, [r1] -> fprintf pp "int8signed(%a)" reg r1 | Ocast8unsigned, [r1] -> fprintf pp "int8unsigned(%a)" reg r1 | Ocast16signed, [r1] -> fprintf pp "int16signed(%a)" reg r1 diff --git a/lib/Coqlib.v b/lib/Coqlib.v index f58a894..b936b9b 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -854,6 +854,54 @@ Proof. exists (a0 :: l1); exists l2; intuition. simpl; congruence. Qed. +(** Folding a function over a list *) + +Section LIST_FOLD. + +Variables A B: Type. +Variable f: A -> B -> B. + +(** This is exactly [List.fold_left] from Coq's standard library, + with [f] taking arguments in a different order. *) + +Fixpoint list_fold_left (accu: B) (l: list A) : B := + match l with nil => accu | x :: l' => list_fold_left (f x accu) l' end. + +(** This is exactly [List.fold_right] from Coq's standard library, + except that it runs in constant stack space. *) + +Definition list_fold_right (l: list A) (base: B) : B := + list_fold_left base (List.rev' l). + +Remark list_fold_left_app: + forall l1 l2 accu, + list_fold_left accu (l1 ++ l2) = list_fold_left (list_fold_left accu l1) l2. +Proof. + induction l1; simpl; intros. + auto. + rewrite IHl1. auto. +Qed. + +Lemma list_fold_right_eq: + forall l base, + list_fold_right l base = + match l with nil => base | x :: l' => f x (list_fold_right l' base) end. +Proof. + unfold list_fold_right; intros. + destruct l. + auto. + unfold rev'. rewrite <- ! rev_alt. simpl. + rewrite list_fold_left_app. simpl. auto. +Qed. + +Lemma list_fold_right_spec: + forall l base, list_fold_right l base = List.fold_right f base l. +Proof. + induction l; simpl; intros; rewrite list_fold_right_eq; congruence. +Qed. + +End LIST_FOLD. + (** Properties of list membership. *) Lemma in_cns: diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 0035dff..39b84e0 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -621,7 +621,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (** Translation of a code sequence *) -Definition r11_is_parent (before: bool) (i: Mach.instruction) : bool := +Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool := match i with | Msetstack src ofs ty => before | Mgetparam ofs ty dst => negb (mreg_eq dst IT1) @@ -629,21 +629,39 @@ Definition r11_is_parent (before: bool) (i: Mach.instruction) : bool := | _ => false end. -Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (r11p: bool) := +(** This is the naive definition that we no longer use because it + is not tail-recursive. It is kept as specification. *) + +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := match il with | nil => OK nil | i1 :: il' => - do k <- transl_code f il' (r11_is_parent r11p i1); - transl_instr f i1 r11p k + do k <- transl_code f il' (it1_is_parent it1p i1); + transl_instr f i1 it1p k end. +(** This is an equivalent definition in continuation-passing style + that runs in constant stack space. *) + +Fixpoint transl_code_rec (f: Mach.function) (il: list Mach.instruction) + (it1p: bool) (k: code -> res code) := + match il with + | nil => k nil + | i1 :: il' => + transl_code_rec f il' (it1_is_parent it1p i1) + (fun c1 => do c2 <- transl_instr f i1 it1p c1; k c2) + end. + +Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := + transl_code_rec f il it1p (fun c => OK c). + (** Translation of a whole function. Note that we must check that the generated code contains less than [2^32] instructions, otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - do c <- transl_code f f.(Mach.fn_code) false; + do c <- transl_code' f f.(Mach.fn_code) false; OK (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: Pmflr GPR0 :: Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: c). diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 658653f..07e66cf 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -317,7 +317,8 @@ Lemma transl_find_label: end. Proof. intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. - monadInv EQ. simpl. eapply transl_code_label; eauto. + monadInv EQ. rewrite transl_code'_transl_code in EQ0. + simpl. eapply transl_code_label; eauto. Qed. End TRANSL_LABEL. @@ -360,6 +361,7 @@ Proof. destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. - intros. monadInv H0. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. monadInv EQ. + rewrite transl_code'_transl_code in EQ0. exists x; exists false; split; auto. unfold fn_code. repeat constructor. - exact transf_function_no_overflow. Qed. @@ -421,7 +423,7 @@ Lemma exec_straight_steps: exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' /\ agree ms2 sp rs2 - /\ (r11_is_parent ep i = true -> rs2#GPR11 = parent_sp s)) -> + /\ (it1_is_parent ep i = true -> rs2#GPR11 = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ match_states (Mach.State s fb sp c ms2 m2) st'. @@ -440,7 +442,7 @@ Lemma exec_straight_steps_goto: Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl f.(Mach.fn_code) = Some c' -> transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> - r11_is_parent ep i = false -> + it1_is_parent ep i = false -> (forall k c (TR: transl_instr f i ep k = OK c), exists jmp, exists k', exists rs2, exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' @@ -897,7 +899,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. intros [m3' [P Q]]. (* Execution of function prologue *) - monadInv EQ0. + monadInv EQ0. rewrite transl_code'_transl_code in EQ1. set (rs2 := nextinstr (rs0#GPR1 <- sp #GPR0 <- Vundef)). set (rs3 := nextinstr (rs2#GPR0 <- (rs0#LR))). set (rs4 := nextinstr rs3). |