diff options
Diffstat (limited to 'backend')
38 files changed, 137 insertions, 537 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 3a5960b..2389a33 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -101,8 +101,6 @@ Definition transfer (reg_sum_live ros (reg_dead res after)) | Itailcall sig ros args => reg_list_live args (reg_sum_live ros Regset.empty) - | Ialloc arg res s => - reg_live arg (reg_dead res after) | Icond cond args ifso ifnot => reg_list_live args after | Ireturn optarg => @@ -167,8 +165,6 @@ Definition transf_instr (assign res) s | Itailcall sig ros args => Ltailcall sig (sum_left_map assign ros) (List.map assign args) - | Ialloc arg res s => - Lalloc (assign arg) (assign res) s | Icond cond args ifso ifnot => Lcond cond (List.map assign args) ifso ifnot | Ireturn optarg => diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 5e38934..3971fb6 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -601,7 +601,7 @@ Proof. rewrite <- H1. eapply agree_move_live; eauto. (* Not a move *) intros INMO CORR CODE. - assert (eval_operation tge sp op (map ls (map assign args)) m = Some v). + assert (eval_operation tge sp op (map ls (map assign args)) = Some v). replace (map ls (map assign args)) with (rs##args). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. eapply agree_eval_regs; eauto. @@ -671,25 +671,15 @@ Proof. rewrite (sig_function_translated _ _ TF). eauto. rewrite H1. econstructor; eauto. - (* Ialloc *) - assert (ls (assign arg) = Vint sz). - rewrite <- H0. symmetry. eapply agree_eval_reg; eauto. - econstructor; split. - eapply exec_Lalloc; eauto. TranslInstr. - generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). - unfold correct_alloc_instr. intros [CORR1 CORR2]. - MatchStates. - eapply agree_postcall with (args := arg :: nil) (ros := inr reg 1%positive); eauto. - (* Icond, true *) - assert (COND: eval_condition cond (map ls (map assign args)) m = Some true). + assert (COND: eval_condition cond (map ls (map assign args)) = Some true). replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Lcond_true; eauto. TranslInstr. MatchStates. eapply agree_reg_list_live. eauto. (* Icond, false *) - assert (COND: eval_condition cond (map ls (map assign args)) m = Some false). + assert (COND: eval_condition cond (map ls (map assign args)) = Some false). replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index d9ab17b..aba9660 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -139,8 +139,6 @@ Proof. split. autorewrite with allocty; auto. split. auto with allocty. auto. rewrite transf_unroll; auto. - (* alloc *) - WT. (* cond *) WT. (* return *) diff --git a/backend/Bounds.v b/backend/Bounds.v index e598245..d1ed28d 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -26,8 +26,7 @@ Require Import Conventions. (** The [bounds] record capture how many local and outgoing stack slots and callee-save registers are used by a function. *) -(** We demand that all bounds are positive or null, - and moreover [bound_outgoing] is greater or equal to 6. +(** We demand that all bounds are positive or null. These properties are used later to reason about the layout of the activation record. *) @@ -104,7 +103,6 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil - | Lalloc => nil | Llabel lbl => nil | Lgoto lbl => nil | Lcond cond args lbl => nil diff --git a/backend/CSE.v b/backend/CSE.v index 49b8489..13e9be8 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -260,7 +260,7 @@ Definition equation_holds (vres: valnum) (rh: rhs) : Prop := match rh with | Op op vl => - eval_operation ge sp op (List.map valuation vl) m = + eval_operation ge sp op (List.map valuation vl) = Some (valuation vres) | Load chunk addr vl => exists a, @@ -348,8 +348,6 @@ Definition transfer (f: function) (pc: node) (before: numbering) := empty_numbering | Itailcall sig ros args => empty_numbering - | Ialloc arg res s => - add_unknown before res | Icond cond args ifso ifnot => before | Ireturn optarg => diff --git a/backend/CSEproof.v b/backend/CSEproof.v index a87cd75..265bb20 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -232,7 +232,7 @@ Proof. apply wf_kill_loads; auto. apply wf_empty_numbering. apply wf_empty_numbering. - apply wf_add_unknown; auto. +(* apply wf_add_unknown; auto. *) Qed. (** As a consequence, the numberings computed by the static analysis @@ -401,7 +401,7 @@ Definition rhs_evals_to (valu: valnum -> val) (rh: rhs) (v: val) : Prop := match rh with | Op op vl => - eval_operation ge sp op (List.map valu vl) m = Some v + eval_operation ge sp op (List.map valu vl) = Some v | Load chunk addr vl => exists a, eval_addressing ge sp addr (List.map valu vl) = Some a /\ @@ -482,7 +482,7 @@ Lemma add_op_satisfiable: forall n rs op args dst v, wf_numbering n -> numbering_satisfiable ge sp rs m n -> - eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op rs##args = Some v -> numbering_satisfiable ge sp (rs#dst <- v) m (add_op n dst op args). Proof. intros. inversion H0. @@ -559,7 +559,7 @@ Proof. intros. destruct H0 as [valu [A B]]. exists valu; split; intros. generalize (A _ _ H0). destruct rh; simpl. - intro. eapply eval_operation_alloc; eauto. + auto. intros [addr [C D]]. exists addr; split. auto. destruct addr; simpl in *; try discriminate. eapply Mem.load_alloc_other; eauto. @@ -595,7 +595,7 @@ Proof. generalize (kill_load_eqs_ops _ _ _ H5). destruct rh; simpl. intros. destruct addr; simpl in H; try discriminate. - eapply eval_operation_store; eauto. + auto. tauto. apply H3. assumption. Qed. @@ -651,7 +651,7 @@ Lemma find_op_correct: wf_numbering n -> numbering_satisfiable ge sp rs m n -> find_op n op args = Some r -> - eval_operation ge sp op rs##args m = Some rs#r. + eval_operation ge sp op rs##args = Some rs#r. Proof. intros until r. intros WF [valu NH]. unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND. @@ -841,14 +841,14 @@ Proof. (* Iop *) exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. - assert (eval_operation tge sp op rs##args m = Some v). + assert (eval_operation tge sp op rs##args = Some v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. generalize C; clear C. case (is_trivial_op op). intro. eapply exec_Iop'; eauto. caseEq (find_op (analyze f)!!pc op args). intros r FIND CODE. eapply exec_Iop'; eauto. simpl. - assert (eval_operation ge sp op rs##args m = Some rs#r). + assert (eval_operation ge sp op rs##args = Some rs#r). eapply find_op_correct; eauto. eapply wf_analyze; eauto. congruence. @@ -910,16 +910,6 @@ Proof. apply sig_preserved. econstructor; eauto. - (* Ialloc *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- (Vptr b Int.zero)) m'); split. - eapply exec_Ialloc; eauto. - econstructor; eauto. - apply analysis_correct_1 with pc. - unfold successors; rewrite H; auto with coqlib. - unfold transfer; rewrite H. - apply add_unknown_satisfiable. apply wf_analyze; auto. - eapply alloc_satisfiable; eauto. - (* Icond true *) econstructor; split. eapply exec_Icond_true; eauto. diff --git a/backend/Cminor.v b/backend/Cminor.v index 16f7c3d..35bf391 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -103,7 +103,6 @@ Inductive stmt : Set := | Sstore : memory_chunk -> expr -> expr -> stmt | Scall : option ident -> signature -> expr -> list expr -> stmt | Stailcall: signature -> expr -> list expr -> stmt - | Salloc : ident -> expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: expr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -251,8 +250,11 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := Definition eval_compare_mismatch (c: comparison) : option val := match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end. +Definition eval_compare_null (c: comparison) (n: int) : option val := + if Int.eq n Int.zero then eval_compare_mismatch c else None. + Definition eval_binop - (op: binary_operation) (arg1 arg2: val) (m: mem): option val := + (op: binary_operation) (arg1 arg2: val): option val := match op, arg1, arg2 with | Oadd, Vint n1, Vint n2 => Some (Vint (Int.add n1 n2)) | Oadd, Vint n1, Vptr b2 n2 => Some (Vptr b2 (Int.add n2 n1)) @@ -286,17 +288,13 @@ Definition eval_binop | Ocmp c, Vint n1, Vint n2 => Some (Val.of_bool(Int.cmp c n1 n2)) | Ocmp c, Vptr b1 n1, Vptr b2 n2 => - if valid_pointer m b1 (Int.signed n1) - && valid_pointer m b2 (Int.signed n2) then - if eq_block b1 b2 - then Some(Val.of_bool(Int.cmp c n1 n2)) - else eval_compare_mismatch c - else - None + if eq_block b1 b2 + then Some(Val.of_bool(Int.cmp c n1 n2)) + else eval_compare_mismatch c | Ocmp c, Vptr b1 n1, Vint n2 => - if Int.eq n2 Int.zero then eval_compare_mismatch c else None + eval_compare_null c n2 | Ocmp c, Vint n1, Vptr b2 n2 => - if Int.eq n1 Int.zero then eval_compare_mismatch c else None + eval_compare_null c n1 | Ocmpu c, Vint n1, Vint n2 => Some (Val.of_bool(Int.cmpu c n1 n2)) | Ocmpf c, Vfloat f1, Vfloat f2 => @@ -332,7 +330,7 @@ Inductive eval_expr: expr -> val -> Prop := | eval_Ebinop: forall op a1 a2 v1 v2 v, eval_expr a1 v1 -> eval_expr a2 v2 -> - eval_binop op v1 v2 m = Some v -> + eval_binop op v1 v2 = Some v -> eval_expr (Ebinop op a1 a2) v | eval_Eload: forall chunk addr vaddr v, eval_expr addr vaddr -> @@ -438,12 +436,6 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) (Mem.free m sp)) - | step_alloc: forall f id a k sp e m n m' b, - eval_expr sp e m a (Vint n) -> - Mem.alloc m 0 (Int.signed n) = (m', b) -> - step (State f (Salloc id a) k sp e m) - E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m') - | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) @@ -633,12 +625,6 @@ with exec_stmt: eval_funcall m f vargs t m' vres -> e' = set_optvar optid vres e -> exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal - | exec_Salloc: - forall sp e m id a n m' b, - eval_expr ge sp e m a (Vint n) -> - Mem.alloc m 0 (Int.signed n) = (m', b) -> - exec_stmt sp e m (Salloc id a) - E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal | exec_Sifthenelse: forall sp e m a s1 s2 v b t e' m' out, eval_expr ge sp e m a v -> @@ -805,10 +791,10 @@ Definition eval_funcall_exec_stmt_ind2 (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop) (P2: val -> env -> mem -> stmt -> trace -> env -> mem -> outcome -> Prop) := - fun a b c d e f g h i j k l m n o p q r => + fun a b c d e f g h i j k l m n o p q => conj - (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r) - (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r ). + (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q) + (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q). Inductive outcome_state_match (sp: val) (e: env) (m: mem) (f: function) (k: cont): @@ -918,11 +904,6 @@ Proof. constructor. reflexivity. traceEq. subst e'. constructor. -(* alloc *) - exists (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m'); split. - apply star_one. econstructor; eauto. - constructor. - (* ifthenelse *) destruct (H2 f k) as [S [A B]]. exists S; split. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 1d5c8c0..bfe92a4 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -68,7 +68,6 @@ Inductive stmt : Set := | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt | Scall : option ident -> signature -> expr -> exprlist -> stmt | Stailcall: signature -> expr -> exprlist -> stmt - | Salloc : ident -> expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -162,7 +161,7 @@ Inductive eval_expr: letenv -> expr -> val -> Prop := eval_expr le (Evar id) v | eval_Eop: forall le op al vl v, eval_exprlist le al vl -> - eval_operation ge sp op vl m = Some v -> + eval_operation ge sp op vl = Some v -> eval_expr le (Eop op al) v | eval_Eload: forall le chunk addr al vl vaddr v, eval_exprlist le al vl -> @@ -188,7 +187,7 @@ with eval_condexpr: letenv -> condexpr -> bool -> Prop := eval_condexpr le CEfalse false | eval_CEcond: forall le cond al vl b, eval_exprlist le al vl -> - eval_condition cond vl m = Some b -> + eval_condition cond vl = Some b -> eval_condexpr le (CEcond cond al) b | eval_CEcondition: forall le a b c vb1 vb2, eval_condexpr le a vb1 -> @@ -294,12 +293,6 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) (Mem.free m sp)) - | step_alloc: forall f id a k sp e m n m' b, - eval_expr sp e m nil a (Vint n) -> - Mem.alloc m 0 (Int.signed n) = (m', b) -> - step (State f (Salloc id a) k sp e m) - E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m') - | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) diff --git a/backend/Coloring.v b/backend/Coloring.v index 056aaa5..7204bc7 100644 --- a/backend/Coloring.v +++ b/backend/Coloring.v @@ -183,12 +183,6 @@ Definition add_edges_instr let largs := loc_arguments sig in add_prefs_call args largs (add_interf_call ros largs g) - | Ialloc arg res s => - add_pref_mreg arg loc_alloc_argument - (add_pref_mreg res loc_alloc_result - (add_interf_op res live - (add_interf_destroyed - (Regset.remove res live) destroyed_at_call_regs g))) | Ireturn (Some r) => add_pref_mreg r (loc_result sig) g | _ => g diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index ea31a29..c86652a 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -384,10 +384,6 @@ Proof. apply add_interf_destroyed_incl. eapply graph_incl_trans; [idtac|apply add_prefs_call_incl]. apply add_interfs_call_incl. - eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. - eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. - eapply graph_incl_trans; [idtac|apply add_interf_op_incl]. - apply add_interf_destroyed_incl. destruct o. apply add_pref_mreg_incl. apply graph_incl_refl. @@ -437,15 +433,6 @@ Definition correct_interf_instr interfere_mreg rfun mr g | inr idfun => True end - | Ialloc arg res s => - (forall r mr, - Regset.In r live -> - In mr destroyed_at_call_regs -> - r <> res -> - interfere_mreg r mr g) - /\ (forall r, - Regset.In r live -> - r <> res -> interfere r res g) | _ => True end. @@ -467,9 +454,6 @@ Proof. split. intros. eapply interfere_incl; eauto. destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. - intros [A B]. split. - intros. eapply interfere_mreg_incl; eauto. - intros. eapply interfere_incl; eauto. Qed. Lemma add_edges_instr_correct: @@ -516,20 +500,6 @@ Proof. eapply interfere_mreg_incl. apply add_prefs_call_incl. apply add_interfs_call_correct. auto. - - (* Ialloc *) - split; intros. - apply interfere_mreg_incl with - (add_interf_destroyed (Regset.remove r0 live) destroyed_at_call_regs g). - eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. - eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. - apply add_interf_op_incl. - apply add_interf_destroyed_correct; auto. - apply Regset.remove_2; auto. - - eapply interfere_incl. - eapply graph_incl_trans; apply add_pref_mreg_incl. - apply add_interf_op_correct; auto. Qed. Lemma add_edges_instrs_incl_aux: @@ -826,14 +796,6 @@ Definition correct_alloc_instr | inl rfun => ~(In (alloc rfun) (loc_arguments sig)) | inr idfun => True end) - | Ialloc arg res s => - (forall r, - Regset.In r live!!pc -> - r <> res -> - ~(In (alloc r) Conventions.destroyed_at_call)) - /\ (forall r, - Regset.In r live!!pc -> - r <> res -> alloc r <> alloc res) | _ => True end. @@ -927,15 +889,6 @@ Proof. caseEq (alloc r). intros. elim (ALL2 r m). apply H; auto. congruence. auto. destruct s0; auto. - (* Ialloc *) - intros [A B]. split. - intros; red; intros. - unfold destroyed_at_call in H1. - generalize (list_in_map_inv R _ _ H1). - intros [mr [EQ IN]]. - generalize (A r1 mr H IN H0). intro. - generalize (ALL2 _ _ H2). contradiction. - auto. Qed. Lemma regalloc_correct_1: diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index c9891c2..433c074 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -52,12 +52,6 @@ Module OrderedRegReg := OrderedPair(OrderedReg)(OrderedReg). Module OrderedMreg := OrderedIndexed(IndexedMreg). Module OrderedRegMreg := OrderedPair(OrderedReg)(OrderedMreg). -(* -Module SetDepRegReg := FSetAVL.Make(OrderedRegReg). -Module SetRegReg := NodepOfDep(SetDepRegReg). -Module SetDepRegMreg := FSetAVL.Make(OrderedRegMreg). -Module SetRegMreg := NodepOfDep(SetDepRegMreg). -*) Module SetRegReg := FSetAVL.Make(OrderedRegReg). Module SetRegMreg := FSetAVL.Make(OrderedRegMreg). @@ -226,16 +220,6 @@ Definition all_interf_regs (g: graph) : Regset.t := g.(interf_reg_mreg) Regset.empty). -(* -Lemma mem_add_tail: - forall r r' u, - Regset.mem r u = true -> Regset.mem r (Regset.add r' u) = true. -Proof. - intros. case (Reg.eq r r'); intro. - subst r'. apply Regset.mem_add_same. - rewrite Regset.mem_add_other; auto. -Qed. -*) Lemma in_setregreg_fold: forall g r1 r2 u, SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u -> diff --git a/backend/LTL.v b/backend/LTL.v index 6ee07f7..0db5495 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -41,7 +41,6 @@ Inductive instruction: Set := | Lstore: memory_chunk -> addressing -> list loc -> loc -> node -> instruction | Lcall: signature -> loc + ident -> list loc -> loc -> node -> instruction | Ltailcall: signature -> loc + ident -> list loc -> instruction - | Lalloc: loc -> loc -> node -> instruction | Lcond: condition -> list loc -> node -> node -> instruction | Lreturn: option loc -> instruction. @@ -165,7 +164,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_Lop: forall s f sp pc rs m op args res pc' v, (fn_code f)!pc = Some(Lop op args res pc') -> - eval_operation ge sp op (map rs args) m = Some v -> + eval_operation ge sp op (map rs args) = Some v -> step (State s f sp pc rs m) E0 (State s f sp pc' (Locmap.set res v rs) m) | exec_Lload: @@ -197,23 +196,16 @@ Inductive step: state -> trace -> state -> Prop := funsig f' = sig -> step (State s f (Vptr stk Int.zero) pc rs m) E0 (Callstate s f' (List.map rs args) (Mem.free m stk)) - | exec_Lalloc: - forall s f sp pc rs m pc' arg res sz m' b, - (fn_code f)!pc = Some(Lalloc arg res pc') -> - rs arg = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', b) -> - step (State s f sp pc rs m) - E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_locs rs)) m') | exec_Lcond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> - eval_condition cond (map rs args) m = Some true -> + eval_condition cond (map rs args) = Some true -> step (State s f sp pc rs m) E0 (State s f sp ifso rs m) | exec_Lcond_false: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> - eval_condition cond (map rs args) m = Some false -> + eval_condition cond (map rs args) = Some false -> step (State s f sp pc rs m) E0 (State s f sp ifnot rs m) | exec_Lreturn: @@ -275,7 +267,6 @@ Definition successors (f: function) (pc: node) : list node := | Lstore chunk addr args src s => s :: nil | Lcall sig ros args res s => s :: nil | Ltailcall sig ros args => nil - | Lalloc arg res s => s :: nil | Lcond cond args ifso ifnot => ifso :: ifnot :: nil | Lreturn optarg => nil end diff --git a/backend/LTLin.v b/backend/LTLin.v index fae6417..4c87c0d 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -47,7 +47,6 @@ Inductive instruction: Set := | Lstore: memory_chunk -> addressing -> list loc -> loc -> instruction | Lcall: signature -> loc + ident -> list loc -> loc -> instruction | Ltailcall: signature -> loc + ident -> list loc -> instruction - | Lalloc: loc -> loc -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list loc -> label -> instruction @@ -157,7 +156,7 @@ Definition find_function (ros: loc + ident) (rs: locset) : option fundef := Inductive step: state -> trace -> state -> Prop := | exec_Lop: forall s f sp op args res b rs m v, - eval_operation ge sp op (map rs args) m = Some v -> + eval_operation ge sp op (map rs args) = Some v -> step (State s f sp (Lop op args res :: b) rs m) E0 (State s f sp b (Locmap.set res v rs) m) | exec_Lload: @@ -185,12 +184,6 @@ Inductive step: state -> trace -> state -> Prop := sig = funsig f' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m) E0 (Callstate s f' (List.map rs args) (Mem.free m stk)) - | exec_Lalloc: - forall s f sp arg res b rs m sz m' blk, - rs arg = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - step (State s f sp (Lalloc arg res :: b) rs m) - E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_locs rs)) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -202,13 +195,13 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp b' rs m) | exec_Lcond_true: forall s f sp cond args lbl b rs m b', - eval_condition cond (map rs args) m = Some true -> + eval_condition cond (map rs args) = Some true -> find_label lbl f.(fn_code) = Some b' -> step (State s f sp (Lcond cond args lbl :: b) rs m) E0 (State s f sp b' rs m) | exec_Lcond_false: forall s f sp cond args lbl b rs m, - eval_condition cond (map rs args) m = Some false -> + eval_condition cond (map rs args) = Some false -> step (State s f sp (Lcond cond args lbl :: b) rs m) E0 (State s f sp b rs m) | exec_Lreturn: diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 26ec066..9f3f589 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -67,11 +67,6 @@ Inductive wt_instr : instruction -> Prop := sig.(sig_res) = funsig.(sig_res) -> Conventions.tailcall_possible sig -> wt_instr (Ltailcall sig ros args) - | wt_Lalloc: - forall arg res, - Loc.type arg = Tint -> Loc.type res = Tint -> - loc_acceptable arg -> loc_acceptable res -> - wt_instr (Lalloc arg res) | wt_Llabel: forall lbl, wt_instr (Llabel lbl) | wt_Lgoto: forall lbl, diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 950154a..0461c9a 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -88,12 +88,6 @@ Inductive wt_instr : instruction -> Prop := sig.(sig_res) = funct.(fn_sig).(sig_res) -> Conventions.tailcall_possible sig -> wt_instr (Ltailcall sig ros args) - | wt_Lalloc: - forall arg res s, - Loc.type arg = Tint -> Loc.type res = Tint -> - loc_acceptable arg -> loc_acceptable res -> - valid_successor s -> - wt_instr (Lalloc arg res s) | wt_Lcond: forall cond args s1 s2, List.map Loc.type args = type_of_condition cond -> diff --git a/backend/Linear.v b/backend/Linear.v index 629dcc5..34d6e5c 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -43,7 +43,6 @@ Inductive instruction: Set := | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Lcall: signature -> mreg + ident -> instruction | Ltailcall: signature -> mreg + ident -> instruction - | Lalloc: instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list mreg -> label -> instruction @@ -247,7 +246,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp b (Locmap.set (S sl) (rs (R r)) rs) m) | exec_Lop: forall s f sp op args res b rs m v, - eval_operation ge sp op (reglist rs args) m = Some v -> + eval_operation ge sp op (reglist rs args) = Some v -> step (State s f sp (Lop op args res :: b) rs m) E0 (State s f sp b (Locmap.set (R res) v rs) m) | exec_Lload: @@ -274,15 +273,6 @@ Inductive step: state -> trace -> state -> Prop := sig = funsig f' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m) E0 (Callstate s f' (return_regs (parent_locset s) rs) (Mem.free m stk)) - | exec_Lalloc: - forall s f sp b rs m sz m' blk, - rs (R Conventions.loc_alloc_argument) = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - step (State s f sp (Lalloc :: b) rs m) - E0 (State s f sp b - (Locmap.set (R Conventions.loc_alloc_result) - (Vptr blk Int.zero) rs) - m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -294,13 +284,13 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp b' rs m) | exec_Lcond_true: forall s f sp cond args lbl b rs m b', - eval_condition cond (reglist rs args) m = Some true -> + eval_condition cond (reglist rs args) = Some true -> find_label lbl f.(fn_code) = Some b' -> step (State s f sp (Lcond cond args lbl :: b) rs m) E0 (State s f sp b' rs m) | exec_Lcond_false: forall s f sp cond args lbl b rs m, - eval_condition cond (reglist rs args) m = Some false -> + eval_condition cond (reglist rs args) = Some false -> step (State s f sp (Lcond cond args lbl :: b) rs m) E0 (State s f sp b rs m) | exec_Lreturn: diff --git a/backend/Linearize.v b/backend/Linearize.v index de372cc..866d05b 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -186,8 +186,6 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code := Lcall sig ros args res :: add_branch s k | LTL.Ltailcall sig ros args => Ltailcall sig ros args :: k - | LTL.Lalloc arg res s => - Lalloc arg res :: add_branch s k | LTL.Lcond cond args s1 s2 => if starts_with s1 k then Lcond (negate_condition cond) args s2 :: add_branch s1 k diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 8378332..b385429 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -604,22 +604,6 @@ Proof. destruct (Genv.find_symbol ge i); try discriminate. eapply Genv.find_funct_ptr_prop; eauto. - (* Lalloc *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - assert (REACH': (reachable f)!!pc' = true). - eapply reachable_successors; eauto. - unfold successors; rewrite H; auto with coqlib. - exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. - econstructor; split. - eapply plus_left'. - eapply exec_Lalloc; eauto. - eapply add_branch_correct; eauto. - eapply is_tail_add_branch. eapply is_tail_cons_left. - eapply is_tail_find_label. eauto. - traceEq. - econstructor; eauto. - (* Lcond true *) destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index ba54723..627c878 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -55,7 +55,6 @@ Proof. apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. apply wt_add_instr. constructor; auto. auto. - apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. destruct (starts_with s1 k); apply wt_add_instr. constructor; auto. rewrite H. destruct cond; auto. apply wt_add_branch; auto. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 9ef6e31..33b570b 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -85,8 +85,6 @@ Inductive wt_instr : instruction -> Prop := tailcall_possible sig -> match ros with inl r => r = IT1 | _ => True end -> wt_instr (Ltailcall sig ros) - | wt_Lalloc: - wt_instr Lalloc | wt_Llabel: forall lbl, wt_instr (Llabel lbl) diff --git a/backend/Mach.v b/backend/Mach.v index c64903b..3f25137 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -58,7 +58,6 @@ Inductive instruction: Set := | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Mcall: signature -> mreg + ident -> instruction | Mtailcall: signature -> mreg + ident -> instruction - | Malloc: instruction | Mlabel: label -> instruction | Mgoto: label -> instruction | Mcond: condition -> list mreg -> label -> instruction diff --git a/backend/Machabstr.v b/backend/Machabstr.v index e145c89..25819f7 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -94,8 +94,9 @@ Section FRAME_ACCESSES. Variable f: function. (** A slot [(ty, ofs)] within a frame is valid in function [f] if it lies - within the bounds of [f]'s frame, and it does not overlap with - the slots reserved for the return address and the back link. *) + within the bounds of [f]'s frame, it does not overlap with + the slots reserved for the return address and the back link, + and it is aligned on a 4-byte boundary. *) Inductive slot_valid: typ -> Z -> Prop := slot_valid_intro: @@ -106,6 +107,7 @@ Inductive slot_valid: typ -> Z -> Prop := \/ Int.signed f.(fn_link_ofs) + 4 <= ofs) -> (ofs + AST.typesize ty <= Int.signed f.(fn_retaddr_ofs) \/ Int.signed f.(fn_retaddr_ofs) + 4 <= ofs) -> + (4 | ofs) -> slot_valid ty ofs. (** [get_slot f fr ty ofs v] holds if the frame [fr] contains value [v] @@ -239,7 +241,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp c (rs#dst <- v) fr m) | exec_Mop: forall s f sp op args res c rs fr m v, - eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op rs##args = Some v -> step (State s f sp (Mop op args res :: c) rs fr m) E0 (State s f sp c (rs#res <- v) fr m) | exec_Mload: @@ -264,15 +266,6 @@ Inductive step: state -> trace -> state -> Prop := find_function ros rs = Some f' -> step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs fr m) E0 (Callstate s f' rs (Mem.free m stk)) - - | exec_Malloc: - forall s f sp c rs fr m sz m' blk, - rs (Conventions.loc_alloc_argument) = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - step (State s f sp (Malloc :: c) rs fr m) - E0 (State s f sp c - (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero)) - fr m') | exec_Mgoto: forall s f sp lbl c rs fr m c', find_label lbl f.(fn_code) = Some c' -> @@ -280,13 +273,13 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp c' rs fr m) | exec_Mcond_true: forall s f sp cond args lbl c rs fr m c', - eval_condition cond rs##args m = Some true -> + eval_condition cond rs##args = Some true -> find_label lbl f.(fn_code) = Some c' -> step (State s f sp (Mcond cond args lbl :: c) rs fr m) E0 (State s f sp c' rs fr m) | exec_Mcond_false: forall s f sp cond args lbl c rs fr m, - eval_condition cond rs##args m = Some false -> + eval_condition cond rs##args = Some false -> step (State s f sp (Mcond cond args lbl :: c) rs fr m) E0 (State s f sp c rs fr m) | exec_Mreturn: diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 7eae610..6e331f3 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -84,7 +84,7 @@ Inductive frame_match (fr: frame) high_bound ms sp >= 0 -> base = Int.repr (-f.(fn_framesize)) -> (forall ty ofs, - -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> + -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) -> load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) -> frame_match fr sp base mm ms. @@ -126,15 +126,16 @@ Lemma frame_match_load_stack: forall fr sp base mm ms ty ofs, frame_match fr sp base mm ms -> 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> + (4 | Int.signed ofs) -> load_stack ms (Vptr sp base) ty ofs = Some (fr ty (Int.signed ofs - f.(fn_framesize))). Proof. - intros. inv H. + intros. inv H. inv wt_f. unfold load_stack, Val.add, loadv. replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs)) with (Int.signed ofs - fn_framesize f). - apply H6. omega. omega. - inv wt_f. + apply H7. omega. omega. + apply Zdivide_minus_l; auto. assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f). apply Int.signed_repr. assert (0 <= Int.max_signed). compute; congruence. omega. @@ -150,8 +151,7 @@ Lemma frame_match_get_slot: get_slot f fr ty (Int.signed ofs) v -> load_stack ms (Vptr sp base) ty ofs = Some v. Proof. - intros. inversion H. inv H0. eapply frame_match_load_stack; eauto. - inv H7. auto. + intros. inversion H. inv H0. inv H7. eapply frame_match_load_stack; eauto. Qed. (** Assigning a value to a frame slot (in the abstract semantics) @@ -163,6 +163,7 @@ Lemma frame_match_store_stack: forall fr sp base mm ms ty ofs v, frame_match fr sp base mm ms -> 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> + (4 | Int.signed ofs) -> Val.has_type v ty -> Mem.extends mm ms -> exists ms', @@ -186,7 +187,10 @@ Proof. apply valid_access_store. constructor. auto. omega. rewrite size_type_chunk. omega. - destruct H7 as [ms' STORE]. + replace (align_chunk (chunk_of_type ty)) with 4. + apply Zdivide_minus_l; auto. + destruct ty; auto. + destruct H8 as [ms' STORE]. generalize (low_bound_store _ _ _ _ _ _ STORE sp). intro LB. generalize (high_bound_store _ _ _ _ _ _ STORE sp). intro HB. exists ms'. @@ -205,10 +209,10 @@ Proof. destruct ty; destruct ty0; simpl; congruence. destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)). (* disjoint *) - rewrite <- H8; auto. eapply load_store_other; eauto. + rewrite <- H9; auto. eapply load_store_other; eauto. right; left. rewrite size_type_chunk; auto. destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)). - rewrite <- H8; auto. eapply load_store_other; eauto. + rewrite <- H9; auto. eapply load_store_other; eauto. right; right. rewrite size_type_chunk; auto. (* overlap *) eapply load_store_overlap'; eauto with mem. @@ -230,8 +234,7 @@ Lemma frame_match_set_slot: frame_match fr' sp base mm ms' /\ Mem.extends mm ms'. Proof. - intros. inv H0. eapply frame_match_store_stack; eauto. - inv H3. auto. + intros. inv H0. inv H3. eapply frame_match_store_stack; eauto. Qed. (** Agreement is preserved by stores within blocks other than the @@ -277,7 +280,7 @@ Proof. destruct (zeq sp b). subst b. right. rewrite size_type_chunk. assert (valid_access mm chunk sp ofs) by eauto with mem. - inv H8. left. omega. + inv H9. left. omega. auto. Qed. @@ -310,6 +313,7 @@ Proof. intros. eapply load_alloc_same'; eauto. rewrite size_type_chunk. omega. + replace (align_chunk (chunk_of_type ty)) with 4; auto. destruct ty; auto. Qed. Lemma frame_match_alloc: @@ -435,6 +439,7 @@ Proof. replace (parent_sp cs) with (extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))). eapply frame_match_load_stack; eauto. + unfold extend_frame. rewrite update_other. apply update_same. simpl. omega. Qed. @@ -470,10 +475,10 @@ Proof. exploit frame_match_new. eauto. inv H. eexact H4. eauto. eauto. eauto. fold base. intros [C FM0]. destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ - FM0 wt_function_link H2 EXT0) + FM0 wt_function_link wt_function_link_aligned H2 EXT0) as [ms2 [STORE1 [FM1 EXT1]]]. destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ - FM1 wt_function_retaddr H3 EXT1) + FM1 wt_function_retaddr wt_function_retaddr_aligned H3 EXT1) as [ms3 [STORE2 [FM3 EXT3]]]. exists ms2; exists ms3; auto. Qed. @@ -783,8 +788,6 @@ Proof. (* Mop *) exists (State ts fb (Vptr sp0 base) c (rs#res <- v) ms); split. apply exec_Mop; auto. - eapply eval_operation_change_mem with (m := m); eauto. - intros. eapply Mem.valid_pointer_extends; eauto. econstructor; eauto with coqlib. (* Mload *) @@ -826,15 +829,6 @@ Proof. econstructor; eauto. eapply match_stacks_free; auto. apply free_extends; auto. - (* Malloc *) - caseEq (alloc ms 0 (Int.signed sz)). intros ms' blk' ALLOC. - exploit alloc_extends; eauto. omega. omega. intros [EQ MEXT']. subst blk'. - exists (State ts fb (Vptr sp0 base) c (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero)) ms'); split. - eapply exec_Malloc; eauto. - econstructor; eauto. - eapply match_stacks_alloc; eauto. inv MEXT; auto. - eapply frame_match_alloc with (mm := m) (ms := ms); eauto. inv MEXT; auto. - (* Mgoto *) econstructor; split. eapply exec_Mgoto; eauto. @@ -843,13 +837,9 @@ Proof. (* Mcond *) econstructor; split. eapply exec_Mcond_true; eauto. - eapply eval_condition_change_mem with (m := m); eauto. - intros. eapply Mem.valid_pointer_extends; eauto. econstructor; eauto. econstructor; split. eapply exec_Mcond_false; eauto. - eapply eval_condition_change_mem with (m := m); eauto. - intros. eapply Mem.valid_pointer_extends; eauto. econstructor; eauto. (* Mreturn *) diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 41216d2..4417cc6 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -155,7 +155,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s fb sp c (rs#dst <- v) m) | exec_Mop: forall s f sp op args res c rs m v, - eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op rs##args = Some v -> step (State s f sp (Mop op args res :: c) rs m) E0 (State s f sp c (rs#res <- v) m) | exec_Mload: @@ -186,14 +186,6 @@ Inductive step: state -> trace -> state -> Prop := load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) E0 (Callstate s f' rs (Mem.free m stk)) - | exec_Malloc: - forall s f sp c rs m sz m' blk, - rs (Conventions.loc_alloc_argument) = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - step (State s f sp (Malloc :: c) rs m) - E0 (State s f sp c - (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero)) - m') | exec_Mgoto: forall s fb f sp lbl c rs m c', Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -202,14 +194,14 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s fb sp c' rs m) | exec_Mcond_true: forall s fb f sp cond args lbl c rs m c', - eval_condition cond rs##args m = Some true -> + eval_condition cond rs##args = Some true -> Genv.find_funct_ptr ge fb = Some (Internal f) -> find_label lbl f.(fn_code) = Some c' -> step (State s fb sp (Mcond cond args lbl :: c) rs m) E0 (State s fb sp c' rs m) | exec_Mcond_false: forall s f sp cond args lbl c rs m, - eval_condition cond rs##args m = Some false -> + eval_condition cond rs##args = Some false -> step (State s f sp (Mcond cond args lbl :: c) rs m) E0 (State s f sp c rs m) | exec_Mreturn: diff --git a/backend/Machtyping.v b/backend/Machtyping.v index f9f76d8..ef59e6f 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -72,8 +72,6 @@ Inductive wt_instr : instruction -> Prop := Conventions.tailcall_possible sig -> match ros with inl r => mreg_type r = Tint | inr s => True end -> wt_instr (Mtailcall sig ros) - | wt_Malloc: - wt_instr Malloc | wt_Mgoto: forall lbl, wt_instr (Mgoto lbl) @@ -91,12 +89,18 @@ Record wt_function (f: function) : Prop := mk_wt_function { f.(fn_stacksize) >= 0; wt_function_framesize: 0 <= f.(fn_framesize) <= -Int.min_signed; + wt_function_framesize_aligned: + (4 | f.(fn_framesize)); wt_function_link: 0 <= Int.signed f.(fn_link_ofs) /\ Int.signed f.(fn_link_ofs) + 4 <= f.(fn_framesize); + wt_function_link_aligned: + (4 | Int.signed f.(fn_link_ofs)); wt_function_retaddr: 0 <= Int.signed f.(fn_retaddr_ofs) /\ Int.signed f.(fn_retaddr_ofs) + 4 <= f.(fn_framesize); + wt_function_retaddr_aligned: + (4 | Int.signed f.(fn_retaddr_ofs)); wt_function_link_retaddr: Int.signed f.(fn_retaddr_ofs) + 4 <= Int.signed f.(fn_link_ofs) \/ Int.signed f.(fn_link_ofs) + 4 <= Int.signed f.(fn_retaddr_ofs) @@ -250,7 +254,7 @@ Proof. simpl in H. rewrite <- H2. replace v with (rs r1). apply WTRS. congruence. replace (mreg_type res) with (snd (type_of_operation op)). - apply type_of_operation_sound with fundef ge rs##args sp m; auto. + apply type_of_operation_sound with fundef ge rs##args sp; auto. rewrite <- H5; reflexivity. apply wt_setreg; auto. inversion H1. rewrite H7. @@ -272,7 +276,7 @@ Proof. apply (Genv.find_funct_ptr_prop wt_fundef wt_p H). econstructor; eauto. - apply wt_setreg; auto. exact I. +(* apply wt_setreg; auto. exact I. *) apply is_tail_find_label with lbl; congruence. apply is_tail_find_label with lbl; congruence. @@ -293,17 +297,6 @@ Proof. econstructor; eauto. eauto with coqlib. Qed. -(* -Lemma subject_reduction_2: - forall s1 t s2, step ge s1 t s2 -> - forall (WTS: wt_state s1), wt_state s2. -Proof. - induction 1; intros. - auto. - eapply subject_reduction; eauto. - auto. -Qed. -*) End SUBJECT_REDUCTION. diff --git a/backend/RTL.v b/backend/RTL.v index abecd4a..5fad2f2 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -68,10 +68,8 @@ Inductive instruction: Set := as arguments. It stores the return value in [dest] and branches to [succ]. *) | Itailcall: signature -> reg + ident -> list reg -> instruction - | Ialloc: reg -> reg -> node -> instruction - (** [Ialloc arg dest succ] allocates a fresh block of size - the contents of register [arg], stores a pointer to this - block in [dest], and branches to [succ]. *) + (** [Itailcall sig fn args] performs a function invocation + in tail-call position. *) | Icond: condition -> list reg -> node -> node -> instruction (** [Icond cond args ifso ifnot] evaluates the boolean condition [cond] over the values of registers [args]. If the condition @@ -213,7 +211,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_Iop: forall s c sp pc rs m op args res pc' v, c!pc = Some(Iop op args res pc') -> - eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op rs##args = Some v -> step (State s c sp pc rs m) E0 (State s c sp pc' (rs#res <- v) m) | exec_Iload: @@ -244,23 +242,16 @@ Inductive step: state -> trace -> state -> Prop := funsig f = sig -> step (State s c (Vptr stk Int.zero) pc rs m) E0 (Callstate s f rs##args (Mem.free m stk)) - | exec_Ialloc: - forall s c sp pc rs m pc' arg res sz m' b, - c!pc = Some(Ialloc arg res pc') -> - rs#arg = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', b) -> - step (State s c sp pc rs m) - E0 (State s c sp pc' (rs#res <- (Vptr b Int.zero)) m') | exec_Icond_true: forall s c sp pc rs m cond args ifso ifnot, c!pc = Some(Icond cond args ifso ifnot) -> - eval_condition cond rs##args m = Some true -> + eval_condition cond rs##args = Some true -> step (State s c sp pc rs m) E0 (State s c sp ifso rs m) | exec_Icond_false: forall s c sp pc rs m cond args ifso ifnot, c!pc = Some(Icond cond args ifso ifnot) -> - eval_condition cond rs##args m = Some false -> + eval_condition cond rs##args = Some false -> step (State s c sp pc rs m) E0 (State s c sp ifnot rs m) | exec_Ireturn: @@ -291,7 +282,7 @@ Inductive step: state -> trace -> state -> Prop := Lemma exec_Iop': forall s c sp pc rs m op args res pc' rs' v, c!pc = Some(Iop op args res pc') -> - eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op rs##args = Some v -> rs' = (rs#res <- v) -> step (State s c sp pc rs m) E0 (State s c sp pc' rs' m). @@ -352,7 +343,6 @@ Definition successors (f: function) (pc: node) : list node := | Istore chunk addr args src s => s :: nil | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil - | Ialloc arg res s => s :: nil | Icond cond args ifso ifnot => ifso :: ifnot :: nil | Ireturn optarg => nil end diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 5fde3d8..709dc78 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -530,12 +530,6 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do n1 <- add_instr (Itailcall sig (inl _ rf) rargs); do n2 <- transl_exprlist map cl rargs n1; transl_expr map b rf n2 - | Salloc id a => - do ra <- alloc_reg map a; - do rr <- new_reg; - do n1 <- store_var map rr id nd; - do n2 <- add_instr (Ialloc ra rr n1); - transl_expr map a ra n2 | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 1074ddd..6d5cd8e 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -568,7 +568,7 @@ Lemma transl_expr_Eop_correct: (vargs : list val) (v : val), eval_exprlist ge sp e m le args vargs -> transl_exprlist_prop le args vargs -> - eval_operation ge sp op vargs m = Some v -> + eval_operation ge sp op vargs = Some v -> transl_expr_prop le (Eop op args) v. Proof. intros; red; intros. inv TE. @@ -711,7 +711,7 @@ Lemma transl_condition_CEcond_correct: (vargs : list val) (b : bool), eval_exprlist ge sp e m le args vargs -> transl_exprlist_prop le args vargs -> - eval_condition cond vargs m = Some b -> + eval_condition cond vargs = Some b -> transl_condition_prop le (CEcond cond args) b. Proof. intros; red; intros; inv TE. @@ -1154,22 +1154,6 @@ Proof. apply sig_transl_function; auto. traceEq. rewrite G. constructor; auto. - - (* alloc *) - inv TS. - exploit transl_expr_correct; eauto. - intros [rs1 [A [B [C D]]]]. - set (rs2 := rs1#rd <- (Vptr b Int.zero)). - assert (match_env map e nil rs2). unfold rs2; eauto with rtlg. - exploit tr_store_var_correct. eauto. auto. eexact H1. - intros [rs3 [E F]]. - unfold rs2 in F. rewrite Regmap.gss in F. - econstructor; split. - left. apply plus_star_trans with E0 (State cs c sp n2 rs2 m') E0. - eapply plus_right. eexact A. unfold rs2. eapply exec_Ialloc; eauto. traceEq. - eexact E. traceEq. - econstructor; eauto. constructor. - (* seq *) inv TS. econstructor; split. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 59a5dd7..e6adeb0 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -141,21 +141,6 @@ Proof. Qed. Hint Resolve instr_at_incr: rtlg. -(* -(** A useful tactic to reason over transitivity and reflexivity of [state_incr]. *) - -Ltac Show_state_incr := - eauto; - match goal with - | |- (state_incr ?c ?c) => - apply state_incr_refl - | |- (state_incr ?c1 ?c2) => - eapply state_incr_trans; [eauto; fail | idtac]; Show_state_incr - end. - -Hint Extern 2 (state_incr _ _) => Show_state_incr : rtlg. -*) - Hint Resolve state_incr_refl state_incr_trans: rtlg. (** * Validity and freshness of registers *) @@ -779,12 +764,6 @@ Inductive tr_stmt (c: code) (map: mapping): tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> c!n2 = Some (Itailcall sig (inl _ rf) rargs) -> tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret - | tr_Salloc: forall id a ns nd nexits ngoto nret rret rd n1 n2 r, - tr_expr c map nil a ns n1 r -> - c!n1 = Some (Ialloc r rd n2) -> - tr_store_var c map rd id n2 nd -> - ~reg_in_map map rd -> - tr_stmt c map (Salloc id a) ns nd nexits ngoto nret rret | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n, tr_stmt c map s2 n nd nexits ngoto nret rret -> tr_stmt c map s1 ns n nexits ngoto nret rret -> @@ -1197,11 +1176,6 @@ Proof. eapply A; eauto with rtlg. apply tr_exprlist_incr with s4; auto. eapply C; eauto with rtlg. - (* Salloc *) - econstructor; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. - apply tr_store_var_incr with s2; eauto with rtlg. - eapply store_var_charact; eauto with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index fa9dd21..60b1d72 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -100,11 +100,6 @@ Inductive wt_instr : instruction -> Prop := List.map env args = sig.(sig_args) -> Conventions.tailcall_possible sig -> wt_instr (Itailcall sig ros args) - | wt_Ialloc: - forall arg res s, - env arg = Tint -> env res = Tint -> - valid_successor s -> - wt_instr (Ialloc arg res s) | wt_Icond: forall cond args s1 s2, List.map env args = type_of_condition cond -> @@ -225,10 +220,6 @@ Definition check_instr (i: instruction) : bool := && check_regs args sig.(sig_args) && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res) && Conventions.tailcall_is_possible sig - | Ialloc arg res s => - check_reg arg Tint - && check_reg res Tint - && check_successor s | Icond cond args s1 s2 => check_regs args (type_of_condition cond) && check_successor s1 @@ -331,11 +322,6 @@ Proof. eapply proj_sumbool_true; eauto. apply check_regs_correct; auto. apply Conventions.tailcall_is_possible_correct; auto. - (* alloc *) - constructor. - apply check_reg_correct; auto. - apply check_reg_correct; auto. - apply check_successor_correct; auto. (* cond *) constructor. apply check_regs_correct; auto. apply check_successor_correct; auto. @@ -524,7 +510,7 @@ Proof. econstructor; eauto. apply wt_regset_assign. auto. replace (env res) with (snd (type_of_operation op)). - apply type_of_operation_sound with fundef ge rs##args sp m; auto. + apply type_of_operation_sound with fundef ge rs##args sp; auto. rewrite <- H6. reflexivity. (* Iload *) econstructor; eauto. @@ -556,9 +542,6 @@ Proof. econstructor; eauto. rewrite H5; auto. rewrite <- H6. apply wt_regset_list. auto. - (* Ialloc *) - econstructor; eauto. - apply wt_regset_assign. auto. rewrite H6; exact I. (* Icond *) econstructor; eauto. econstructor; eauto. diff --git a/backend/Reload.v b/backend/Reload.v index 17664b6..621e75b 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -235,9 +235,6 @@ Definition transf_instr parallel_move args largs (Ltailcall sig (inr _ id) :: k) end - | LTLin.Lalloc arg res => - add_reload arg loc_alloc_argument - (Lalloc :: add_spill loc_alloc_result res k) | LTLin.Llabel lbl => Llabel lbl :: k | LTLin.Lgoto lbl => diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 5a3acd3..ea7c5d1 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -178,10 +178,10 @@ Proof. Qed. Lemma not_enough_temporaries_addr: - forall (ge: genv) sp addr src args ls m v, + forall (ge: genv) sp addr src args ls v, enough_temporaries (src :: args) = false -> eval_addressing ge sp addr (List.map ls args) = Some v -> - eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) m = Some v. + eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) = Some v. Proof. intros. apply eval_op_for_binary_addressing; auto. @@ -631,21 +631,6 @@ Proof. apply temporaries_not_acceptable; auto. Qed. -Lemma agree_postcall_alloc: - forall rs ls ls2 v, - agree rs ls -> - (forall l, Loc.diff (R loc_alloc_argument) l -> ls2 l = ls l) -> - agree (LTL.postcall_locs rs) (Locmap.set (R loc_alloc_result) v ls2). -Proof. - intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto. - intros. destruct (Loc.eq l (R loc_alloc_result)). - subst l. elim H2. simpl. tauto. - rewrite Locmap.gso. apply H0. - red. destruct l; auto. red; intro. subst m. elim H2. - simpl. tauto. - apply Loc.diff_sym. apply loc_acceptable_noteq_diff; auto. -Qed. - Lemma agree_init_locs: forall ls dsts vl, locs_acceptable dsts -> @@ -991,9 +976,9 @@ Proof. eapply enough_temporaries_op_args; eauto. apply locs_acceptable_disj_temporaries; auto. intros [ls2 [A [B C]]]. instantiate (1 := ls) in B. - assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) tm = Some tv + assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) = Some tv /\ Val.lessdef v tv). - apply eval_operation_lessdef with m (map rs args); auto. + apply eval_operation_lessdef with (map rs args); auto. rewrite B. eapply agree_locs; eauto. rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. destruct H1 as [tv [P Q]]. @@ -1231,28 +1216,6 @@ Proof. exact (return_regs_preserve (parent_locset s') ls3). apply Mem.free_lessdef; auto. - (* Lalloc *) - ExploitWT; inv WTI. - caseEq (alloc tm 0 (Int.signed sz)). intros tm' blk' TALLOC. - assert (blk = blk' /\ Mem.lessdef m' tm'). - eapply Mem.alloc_lessdef; eauto. - exploit add_reload_correct. intros [ls2 [A [B C]]]. - exploit add_spill_correct. intros [ls3 [D [E F]]]. - destruct H1 as [P Q]. subst blk'. - assert (ls arg = Vint sz). - assert (Val.lessdef (rs arg) (ls arg)). eapply agree_loc; eauto. - rewrite H in H1; inversion H1; auto. - left; econstructor; split. - eapply star_plus_trans. eauto. - eapply plus_left. eapply exec_Lalloc; eauto. - rewrite B. eauto. - eauto. eauto. traceEq. - econstructor; eauto with coqlib. - apply agree_set with (Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) ls2). - auto. rewrite E. rewrite Locmap.gss. constructor. - auto. - apply agree_postcall_alloc with ls; auto. - (* Llabel *) left; econstructor; split. apply plus_one. apply exec_Llabel. @@ -1272,7 +1235,7 @@ Proof. intros [ls2 [A [B C]]]. left; econstructor; split. eapply plus_right. eauto. eapply exec_Lcond_true; eauto. - rewrite B. apply eval_condition_lessdef with m (map rs args); auto. + rewrite B. apply eval_condition_lessdef with (map rs args); auto. eapply agree_locs; eauto. apply find_label_transf_function; eauto. traceEq. @@ -1288,7 +1251,7 @@ Proof. intros [ls2 [A [B C]]]. left; econstructor; split. eapply plus_right. eauto. eapply exec_Lcond_false; eauto. - rewrite B. apply eval_condition_lessdef with m (map rs args); auto. + rewrite B. apply eval_condition_lessdef with (map rs args); auto. eapply agree_locs; eauto. traceEq. econstructor; eauto with coqlib. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index e531c54..375bbfd 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -34,7 +34,7 @@ Require Import Reloadproof. given sufficient typing and well-formedness hypotheses over the locations involved. *) Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove - wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lalloc + wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Llabel wt_Lgoto wt_Lcond wt_Lreturn: reloadty. Remark wt_code_cons: diff --git a/backend/Stacking.v b/backend/Stacking.v index 1cf010b..158af8f 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -179,8 +179,6 @@ Definition transl_instr | Ltailcall sig ros => restore_callee_save fe (Mtailcall sig ros :: k) - | Lalloc => - Malloc :: k | Llabel lbl => Mlabel lbl :: k | Lgoto lbl => diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index e17f67a..a7560d0 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -172,6 +172,45 @@ Proof. assert (z <> z0). intuition auto. omega. Qed. +Remark aligned_4_4x: forall x, (4 | 4 * x). +Proof. intro. exists x; ring. Qed. + +Remark aligned_4_8x: forall x, (4 | 8 * x). +Proof. intro. exists (x * 2); ring. Qed. + +Remark aligned_4_align8: forall x, (4 | align x 8). +Proof. + intro. apply Zdivides_trans with 8. exists 2; auto. apply align_divides. omega. +Qed. + +Hint Resolve Zdivide_0 Zdivide_refl Zdivide_plus_r + aligned_4_4x aligned_4_8x aligned_4_align8: align_4. + +Hint Extern 4 (?X | ?Y) => (exists (Y/X); reflexivity) : align_4. + +Lemma offset_of_index_aligned: + forall idx, (4 | offset_of_index fe idx). +Proof. + intros. + destruct idx; + unfold offset_of_index, fe, make_env, + fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, + fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg; + auto with align_4. + destruct t; auto with align_4. +Qed. + +Lemma frame_size_aligned: + (4 | fe_size fe). +Proof. + unfold offset_of_index, fe, make_env, + fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, + fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg; + auto with align_4. +Qed. + (** The following lemmas give sufficient conditions for indices of various kinds to be valid. *) @@ -232,7 +271,7 @@ Proof. fe_ofs_float_local, fe_ofs_float_callee_save, fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg, type_of_index, typesize; - simpl in H5; + unfold index_valid in H5; simpl typesize in H5; omega. Qed. @@ -287,6 +326,7 @@ Proof. auto. exact I. red. destruct idx; auto || congruence. intro. rewrite typesize_typesize. assumption. exact I. + apply offset_of_index_aligned. Qed. Lemma get_slot_index: @@ -535,96 +575,6 @@ Proof. intros. rewrite get_set_index_val_other; eauto with stacking. red; auto. Qed. -(* -Lemma agree_set_int_callee_save: - forall ls ls0 rs fr r v, - agree ls ls0 rs fr -> - In r int_callee_save_regs -> - index_int_callee_save r < fe.(fe_num_int_callee_save) -> - exists fr', - set_slot tf fr Tint - (Int.signed (Int.repr - (offset_of_index fe (FI_saved_int (index_int_callee_save r))))) - v fr' /\ - agree ls (Locmap.set (R r) v ls0) rs fr'. -Proof. - intros. - set (idx := FI_saved_int (index_int_callee_save r)). - exists (set_index_val idx v fr); split. - change Tint with (type_of_index idx). - apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. - constructor; eauto with stacking. - (* agree_unused_reg *) - intros. rewrite Locmap.gso. eauto with stacking. - red; red; intro. subst r0. elim H2. red. - rewrite (int_callee_save_type r H0). auto. - (* agree_local *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_outgoing *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_incoming *) - intros. rewrite Locmap.gso. eauto with stacking. red. auto. - (* saved ints *) - intros. destruct (mreg_eq r r0). - subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. - rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking. - unfold idx. auto with stacking. auto with stacking. - unfold idx; red. apply index_int_callee_save_inj; auto. - red; auto. - (* saved floats *) - intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. - unfold idx. auto with stacking. - unfold idx; red; auto. - red. apply int_float_callee_save_disjoint; auto. -Qed. - -Lemma agree_set_float_callee_save: - forall ls ls0 rs fr r v, - agree ls ls0 rs fr -> - In r float_callee_save_regs -> - index_float_callee_save r < fe.(fe_num_float_callee_save) -> - exists fr', - set_slot tf fr Tfloat - (Int.signed (Int.repr - (offset_of_index fe (FI_saved_float (index_float_callee_save r))))) - v fr' /\ - agree ls (Locmap.set (R r) v ls0) rs fr'. -Proof. - intros. - set (idx := FI_saved_float (index_float_callee_save r)). - exists (set_index_val idx v fr); split. - change Tfloat with (type_of_index idx). - apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. - constructor; eauto with stacking. - (* agree_unused_reg *) - intros. rewrite Locmap.gso. eauto with stacking. - red; red; intro. subst r0. elim H2. red. - rewrite (float_callee_save_type r H0). auto. - (* agree_local *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_outgoing *) - intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_incoming *) - intros. rewrite Locmap.gso. eauto with stacking. red. auto. - (* saved ints *) - intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. - unfold idx. auto with stacking. - unfold idx; red; auto. - red. apply sym_not_equal. apply int_float_callee_save_disjoint; auto. - (* saved floats *) - intros. destruct (mreg_eq r r0). - subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. - rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking. - unfold idx. auto with stacking. auto with stacking. - unfold idx; red. apply index_float_callee_save_inj; auto. - red; auto. -Qed. -*) - Lemma agree_return_regs: forall ls ls0 rs fr cs rs', agree ls ls0 rs fr cs -> @@ -1270,12 +1220,11 @@ Proof. Qed. Lemma shift_eval_operation: - forall f tf sp op args m v, + forall f tf sp op args v, transf_function f = OK tf -> - eval_operation ge sp op args m = Some v -> + eval_operation ge sp op args = Some v -> eval_operation tge (shift_sp tf sp) - (transl_op (make_env (function_bounds f)) op) args m = - Some v. + (transl_op (make_env (function_bounds f)) op) args = Some v. Proof. intros until v. destruct op; intros; auto. simpl in *. rewrite symbols_preserved. auto. @@ -1535,15 +1484,6 @@ Proof. intros. inv WTI. generalize (H3 _ H0). tauto. apply agree_callee_save_return_regs. - (* Lalloc *) - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) - (rs0#loc_alloc_result <- (Vptr blk Int.zero)) fr m'); split. - apply plus_one; eapply exec_Malloc; eauto. - rewrite (agree_eval_reg _ _ _ _ _ _ _ loc_alloc_argument AG). auto. - econstructor; eauto with coqlib. - apply agree_set_reg; auto. - red. simpl. generalize (max_over_regs_of_funct_pos f int_callee_save). omega. - (* Llabel *) econstructor; split. apply plus_one; apply exec_Mlabel. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index f1fe2cf..b88dd50 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -176,8 +176,6 @@ Proof. apply wt_restore_callee_save. apply wt_instrs_cons; auto. constructor; auto. destruct s0; auto. rewrite H5; auto. - (* alloc *) - apply wt_instrs_cons; auto. constructor. (* label *) apply wt_instrs_cons; auto. constructor. @@ -227,10 +225,13 @@ Proof. red; intros. elim H5. subst tf; simpl; auto. rewrite H2. generalize (size_pos f). fold b; fold fe; omega. + rewrite H1. change (4 | fe_size fe). unfold fe, b. apply frame_size_aligned. rewrite H3; rewrite H2. change 4 with (4 * typesize (type_of_index FI_link)). unfold fe, b; apply offset_of_index_valid. red; auto. + rewrite H3. unfold fe,b; apply offset_of_index_aligned. rewrite H4; rewrite H2. change 4 with (4 * typesize (type_of_index FI_retaddr)). unfold fe, b; apply offset_of_index_valid. red; auto. + rewrite H4. unfold fe,b; apply offset_of_index_aligned. rewrite H3; rewrite H4. apply (offset_of_index_disj f FI_retaddr FI_link); red; auto. Qed. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 2f520c6..32d1b59 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -112,8 +112,6 @@ Definition tunnel_instr (f: LTL.function) (b: instruction) : instruction := Lcall sig ros args res (branch_target f s) | Ltailcall sig ros args => Ltailcall sig ros args - | Lalloc arg res s => - Lalloc arg res (branch_target f s) | Lcond cond args s1 s2 => Lcond cond args (branch_target f s1) (branch_target f s2) | Lreturn or => diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 7ad75ba..49bf894 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -297,12 +297,6 @@ Proof. rewrite sig_preserved. auto. apply find_function_translated; auto. econstructor; eauto. - (* Lalloc *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. - left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_locs rs)) m'); split. - eapply exec_Lalloc; eauto. - rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. - econstructor; eauto. (* cond *) rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. left; econstructor; split. |