diff options
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | mppa_k1c/lib/PseudoAsmblock.v | 60 | ||||
| -rw-r--r-- | mppa_k1c/lib/PseudoAsmblockproof.v | 263 |
3 files changed, 128 insertions, 197 deletions
@@ -844,7 +844,7 @@ ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure EXECUTE=k1-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __K1C_COS__ SIMU=k1-cluster -- -BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v PseudoAsmblock.v PseudoAsmblockproof.v\\ +BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ diff --git a/mppa_k1c/lib/PseudoAsmblock.v b/mppa_k1c/lib/PseudoAsmblock.v index 22cc643d..336e315c 100644 --- a/mppa_k1c/lib/PseudoAsmblock.v +++ b/mppa_k1c/lib/PseudoAsmblock.v @@ -187,18 +187,13 @@ Inductive cfi_step (f: function): control_flow_inst -> regset -> mem -> trace -> list_nth_z tbl (Int.unsigned index) = Some lbl -> goto_label f lbl rs = Some pc -> rs' = set_from_Machrs (undef_regs destroyed_by_jumptable rs) rs -> - cfi_step f (MBjumptable arg tbl) rs m E0 (rs'#PC <- pc) m. - -(* TODO à finir... - | exec_MBbuiltin: - forall s f sp rs m ef args res b c vargs t vres rs' m', - eval_builtin_args ge rs sp m args vargs -> + cfi_step f (MBjumptable arg tbl) rs m E0 (rs'#PC <- pc) m + | exec_MBbuiltin rs m ef args res vargs t vres rs' m': + eval_builtin_args ge (to_Machrs rs) (rs#SP) m args vargs -> external_call ef ge vargs m t vres m' -> - rs' = set_res res vres (undef_regs (destroyed_by_builtin ef) rs) -> - cfi_step (MBbuiltin ef args res) (State s f sp (b :: c) rs m) - t (State s f sp c rs' m') + rs' = set_from_Machrs (set_res res vres (undef_regs (destroyed_by_builtin ef) rs)) rs -> + cfi_step f (MBbuiltin ef args res) rs m t rs' m' . -*) Inductive exit_step f : option control_flow_inst -> regset -> mem -> trace -> regset -> mem -> Prop := | exec_Some_exit ctl rs m t rs' m': @@ -225,47 +220,6 @@ Definition exec_prologue f (pos:Z) (rs: regset) (m:mem) : option state := else Next rs m. -(** Extract the values of the arguments of an external call. - We exploit the calling conventions from module [Conventions], except that - we use machine registers instead of locations. *) -Definition undef_caller_save_regs (rs: regset) : regset := - fun r => - if preg_eq r SP - || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs)) - then rs r - else Vundef. - -Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := - | extcall_arg_reg: forall r, - extcall_arg rs m (R r) (rs (preg_of r)) - | extcall_arg_stack: forall ofs ty bofs v, - bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> - Mem.loadv (chunk_of_type ty) m - (Val.offset_ptr (rs SP) (Ptrofs.repr bofs)) = Some v -> - extcall_arg rs m (S Outgoing ofs ty) v. - -Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop := - | extcall_arg_one: forall l v, - extcall_arg rs m l v -> - extcall_arg_pair rs m (One l) v - | extcall_arg_twolong: forall hi lo vhi vlo, - extcall_arg rs m hi vhi -> - extcall_arg rs m lo vlo -> - extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo). - -Definition extcall_arguments - (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := - list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args. - -Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset := - match p with - | One r => rs#r <- v - | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v) - end. - -Definition loc_external_result (sg: signature) : rpair preg := - map_rpair preg_of (loc_result sg). - Inductive step: state -> trace -> state -> Prop := | exec_step_internal b ofs f bb c rs0 m0 rs1 m1 t rs2 m2: @@ -279,9 +233,9 @@ Inductive step: state -> trace -> state -> Prop := forall b ef args res rs m t rs' m', rs PC = Vptr b Ptrofs.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> - extcall_arguments rs m (ef_sig ef) args -> + extcall_arguments (to_Machrs rs) m (rs#SP) (ef_sig ef) args -> external_call ef ge args m t res m' -> - rs' = (set_pair (loc_external_result (ef_sig ef)) res (undef_caller_save_regs rs)) #PC <- (rs RA) -> + rs' = (set_from_Machrs (set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs)) rs) #PC <- (rs RA) -> step (State rs m) t (State rs' m'). End RELSEM. diff --git a/mppa_k1c/lib/PseudoAsmblockproof.v b/mppa_k1c/lib/PseudoAsmblockproof.v index cdb46202..59a7e62a 100644 --- a/mppa_k1c/lib/PseudoAsmblockproof.v +++ b/mppa_k1c/lib/PseudoAsmblockproof.v @@ -1,16 +1,13 @@ Require Import Coqlib Maps AST Integers Values Memory Events Globalenvs Smallstep. Require Import Op Machregs Locations Stacklayout Conventions. Require Import Mach Machblock OptionMonad. -Require Import Errors Datatypes PseudoAsmblock. +Require Import Errors Datatypes PseudoAsmblock IterList. (** Tiny translation from Machblock semantics to PseudoAsmblock semantics (needs additional checks) *) Section TRANSLATION. -(** "oracle" returning the last offset of the final assembly function in memory *) -Variable max_pos: function -> Z. - (* In the actual Asmblock code, the prologue will be inserted in the first block of the function. But, this block should have an empty header. *) @@ -37,9 +34,11 @@ Definition transl_function (f: function) : function := Definition transf_function (f: function) : res function := let tf := transl_function f in + (* removed because it is simpler or/and more efficient to perform this test in Asmblockgen ! if zlt Ptrofs.max_unsigned (max_pos tf) then Error (msg "code size exceeded") - else OK tf. + else *) + OK tf. Definition transf_fundef (f: fundef) : res fundef := transf_partial_fundef transf_function f. @@ -49,51 +48,6 @@ Definition transf_program (p: program) : res program := End TRANSLATION. -(** TODO: are these def and lemma already defined in the standard library ? - -In this case, it should be better to reuse those of the standard library ! - -*) - -Fixpoint iter {A} (n:nat) (f: A -> A) (x: A) {struct n}: A := - match n with - | O => x - | S n0 => iter n0 f (f x) - end. - -Lemma iter_S A (n:nat) (f: A -> A): forall x, iter (S n) f x = f (iter n f x). -Proof. - induction n; simpl; auto. - intros; erewrite <- IHn; simpl; auto. -Qed. - -Definition iter_tail {A} (n:nat) (l: list A) := iter n (@tl A) l. - -Lemma length_iter_tail {A} (n:nat): forall (l: list A), (n <= List.length l)%nat -> (List.length l = n + List.length (iter_tail n l))%nat. -Proof. - unfold iter_tail; induction n; auto. - intros l; destruct l. { simpl; omega. } - intros; simpl. erewrite IHn; eauto. - simpl in *; omega. -Qed. - -Lemma iter_tail_S {A} (n:nat): forall (l: list A), (n < length l)%nat -> exists x, iter_tail n l = x::(iter_tail (S n) l). -Proof. - unfold iter_tail; induction n; simpl. - - intros l; destruct l; simpl; omega || eauto. - - intros l H; destruct (IHn (tl l)) as (x & H1). - + destruct l; simpl in *; try omega. - + rewrite H1; eauto. -Qed. - -Lemma iter_tail_inject1 {A} (n1 n2:nat) (l: list A): (n1 <= List.length l)%nat -> (n2 <= List.length l)%nat -> iter_tail n1 l = iter_tail n2 l -> n1=n2. -Proof. - intros H1 H2 EQ; exploit (length_iter_tail n1 l); eauto. - rewrite EQ. - rewrite (length_iter_tail n2 l); eauto. - omega. -Qed. - (** Proof of the translation *) @@ -101,19 +55,11 @@ Require Import Linking. Section PRESERVATION. -Variable next: function -> Z -> Z. - -Hypothesis next_progress: forall (f:function) (pos:Z), (pos < (next f pos))%Z. - -Variable max_pos: function -> Z. - -Hypothesis max_pos_def: forall (f:function), max_pos f = iter (length f.(fn_code)) (next f) 0. - Definition match_prog (p: program) (tp: program) := - match_program (fun _ f tf => transf_fundef max_pos f = OK tf) eq p tp. + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. Lemma transf_program_match: - forall p tp, transf_program max_pos p = OK tp -> match_prog p tp. + forall p tp, transf_program p = OK tp -> match_prog p tp. Proof. intros. eapply match_transform_partial_program; eauto. Qed. @@ -129,6 +75,19 @@ Hypothesis TRANSF: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. +Variable next: function -> Z -> Z. + +Hypothesis next_progress: forall (f:function) (pos:Z), (pos < (next f pos))%Z. + +Definition max_pos (f:function) := iter (S (length f.(fn_code))) (next f) 0. + +(* This hypothesis expresses that Asmgen checks for each tf + that (max_pos tf) represents a valid address +*) +Hypothesis functions_bound_max_pos: forall fb tf, + Genv.find_funct_ptr tge fb = Some (Internal tf) -> + (max_pos tf) <= Ptrofs.max_unsigned. + (** * Agreement between Mach registers and PseudoAsm registers *) Record agree (ms: Mach.regset) (sp: val) (rs: regset) : Prop := mkagree { agree_sp: rs#SP = sp; @@ -143,7 +102,7 @@ Record agree (ms: Mach.regset) (sp: val) (rs: regset) : Prop := mkagree { Inductive transl_code_at_pc (b:block) (f:function) (tf:function) (c:code): val -> Prop := transl_code_at_pc_intro ofs: Genv.find_funct_ptr ge b = Some (Internal f) -> - transf_function max_pos f = OK tf -> + transf_function f = OK tf -> (* we have passed the first block containing the prologue *) (0 < (Ptrofs.unsigned ofs))%Z -> (* the code is identical in the two functions *) @@ -214,7 +173,7 @@ Definition measure (s: Machblock.state) : nat := Definition rao (f: function) (c: code) (ofs: ptrofs) : Prop := forall tf, - transf_function max_pos f = OK tf -> + transf_function f = OK tf -> is_pos next tf (Ptrofs.unsigned ofs) c. Lemma symbols_preserved: @@ -229,45 +188,40 @@ Lemma functions_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transf_fundef max_pos f = OK tf. + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. Proof (Genv.find_funct_ptr_transf_partial TRANSF). Lemma functions_transl fb f tf: Genv.find_funct_ptr ge fb = Some (Internal f) -> - transf_function max_pos f = OK tf -> + transf_function f = OK tf -> Genv.find_funct_ptr tge fb = Some (Internal tf). Proof. intros. exploit functions_translated; eauto. intros [tf' [A B]]. - monadInv B. rewrite H0 in EQ; inv EQ; auto. + monadInv B. inv H0; auto. Qed. -Lemma function_bound f tf: - transf_function max_pos f = OK tf -> (max_pos tf) <= Ptrofs.max_unsigned. +Lemma function_bound fb f tf: + Genv.find_funct_ptr ge fb = Some (Internal f) -> transf_function f = OK tf -> (max_pos tf) <= Ptrofs.max_unsigned. Proof. - unfold transf_function. - destruct (zlt _ _); try congruence. - intros EQ; inv EQ. - omega. + intros; eapply functions_bound_max_pos; eauto. + eapply functions_transl; eauto. Qed. - Lemma transf_function_def f tf: - transf_function max_pos f = OK tf -> tf.(fn_code) = insert_implicit_prologue f.(fn_code). + transf_function f = OK tf -> tf.(fn_code) = insert_implicit_prologue f.(fn_code). Proof. unfold transf_function. - destruct (zlt _ _); try congruence. intros EQ; inv EQ. auto. Qed. Lemma stackinfo_preserved f tf: - transf_function max_pos f = OK tf -> + transf_function f = OK tf -> tf.(fn_stacksize) = f.(fn_stacksize) /\ tf.(fn_retaddr_ofs) = f.(fn_retaddr_ofs) /\ tf.(fn_link_ofs) = f.(fn_link_ofs). Proof. unfold transf_function. - destruct (zlt _ _); try congruence. intros EQ0; inv EQ0. simpl; intuition. Qed. @@ -321,7 +275,7 @@ Lemma is_pos_alt_def_recip f n: (n <= List.length (fn_code f))%nat -> Proof. induction n. - unfold iter_tail; simpl; eauto. - - intros H; destruct (iter_tail_S n (fn_code f)) as (x & H1); try omega. + - intros H; destruct (iter_tail_S_ex n (fn_code f)) as (x & H1); try omega. rewrite iter_S; lapply IHn; try omega. rewrite H1; eauto. Qed. @@ -355,7 +309,7 @@ Lemma is_pos_bound_pos f pos code: Proof. intros H; exploit is_pos_alt_def; eauto. intros (n & H1 & H2 & H3). - rewrite H2, max_pos_def. split. + rewrite H2. unfold max_pos. split. - cutrewrite (0 = iter O (next f) 0); auto. apply iter_next_monotonic; omega. - apply iter_next_monotonic; omega. @@ -445,7 +399,7 @@ Hint Resolve is_pos_simplify is_pos_alt_def_recip function_bound: core. Lemma find_label_goto_label f tf lbl rs c' b ofs: Genv.find_funct_ptr ge b = Some (Internal f) -> - transf_function max_pos f = OK tf -> + transf_function f = OK tf -> Vptr b ofs = rs PC -> find_label lbl f.(fn_code) = Some c' -> exists pc, @@ -492,16 +446,25 @@ Proof. Qed. Corollary agree_set_mreg_parallel: - forall ms sp rs r v v', + forall ms sp rs r v, agree ms sp rs -> - v=v' -> - agree (Regmap.set r v ms) sp (Pregmap.set (preg_of r) v' rs). + agree (Regmap.set r v ms) sp (Pregmap.set (preg_of r) v rs). Proof. intros. eapply agree_set_mreg; eauto. - rewrite Pregmap.gss; auto. - intros; apply Pregmap.gso; auto. Qed. +Corollary agree_set_mreg_parallel2: + forall ms sp rs r v ms', + agree ms sp (set_from_Machrs ms' rs)-> + agree (Regmap.set r v ms) sp (set_from_Machrs (Regmap.set r v ms') rs). +Proof. + intros. unfold set_from_Machrs in *. eapply agree_set_mreg; eauto. + - rewrite Regmap.gss; auto. + - intros r' X. destruct r'; try congruence. rewrite Regmap.gso; try congruence. +Qed. + Definition data_preg (r: preg) : bool := match r with | preg_of _ | SP => true @@ -516,6 +479,16 @@ Proof. intros H H0. destruct H. split; intros; try rewrite H0; auto. Qed. +Lemma agree_set_from_Machrs ms sp ms' rs: + agree ms sp rs -> + (forall (r:mreg), (ms' r) = rs#r) -> + agree ms sp (set_from_Machrs ms' rs). +Proof. + unfold set_from_Machrs; intros. + eapply agree_exten; eauto. + intros r; destruct r; simpl; try congruence. +Qed. + Lemma agree_set_other ms sp rs r v: agree ms sp rs -> data_preg r = false -> @@ -525,13 +498,6 @@ Proof. intros. apply Pregmap.gso. congruence. Qed. -(* TODO: à revoir ! -Lemma agree_next_addr f ms sp b pos rs: - agree ms sp rs -> agree ms sp (next_addr next f b pos rs). -Proof. - intros. unfold next_addr. apply agree_set_other; auto. -Qed. -*) Lemma agree_next_addr f ms sp b pos rs: agree ms sp rs -> @@ -540,40 +506,24 @@ Proof. intros. apply agree_set_other; auto. Qed. -Lemma agree_set_pair sp p v v' ms rs: - agree ms sp rs -> - v=v' -> - agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs). -Proof. - intros H H0; subst; destruct p; simpl; repeat (apply agree_set_mreg_parallel; auto). -Qed. - -Lemma preg_of_injective r1 r2: preg_of r1 = preg_of r2 -> r1 = r2. -Proof. - intros H; inversion H. auto. -Qed. +Local Hint Resolve agree_set_mreg_parallel2: core. -Lemma preg_of_not_SP: - forall r, preg_of r <> SP. +Lemma agree_set_pair sp p v ms ms' rs: + agree ms sp (set_from_Machrs ms' rs) -> + agree (set_pair p v ms) sp (set_from_Machrs (set_pair p v ms') rs). Proof. - intros. destruct r; simpl; congruence. + intros H; destruct p; simpl; auto. Qed. Lemma agree_undef_caller_save_regs: - forall ms sp rs, - agree ms sp rs -> - agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs). + forall ms sp ms' rs, + agree ms sp (set_from_Machrs ms' rs) -> + agree (undef_caller_save_regs ms) sp (set_from_Machrs (undef_caller_save_regs ms') rs). Proof. - intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split. -- unfold proj_sumbool; rewrite dec_eq_true. auto. -- auto. -- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). - destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter Conventions1.is_callee_save all_mregs))); simpl. -+ apply list_in_map_inv in i. destruct i as (mr & A & B). - assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. - apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. -+ destruct (Conventions1.is_callee_save r) eqn:CS; auto. - elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. + intros. destruct H as [H0 H1 H2]. unfold undef_caller_save_regs. split; auto. + intros. + unfold set_from_Machrs in * |- *. + rewrite H2. auto. Qed. Lemma agree_change_sp ms sp rs sp': @@ -583,16 +533,45 @@ Proof. intros H H0. inv H. split; auto. Qed. -Lemma agree_undef_regs ms sp rl ms' (rs: regset): - agree ms sp rs -> - (forall (r:mreg), (ms' r) = rs#r) -> +Lemma agree_undef_regs ms sp rl ms' rs: + agree ms sp (set_from_Machrs ms' rs) -> agree (Mach.undef_regs rl ms) sp (set_from_Machrs (Mach.undef_regs rl ms') rs). Proof. - unfold set_from_Machrs; intros H H0. destruct H; subst. split; auto. + unfold set_from_Machrs; intros H. destruct H; subst. split; auto. intros. destruct (In_dec mreg_eq r rl). - + rewrite! Mach.undef_regs_same; auto. - + rewrite! Mach.undef_regs_other; auto. - rewrite agree_mregs0; auto. + + rewrite! undef_regs_same; auto. + + rewrite! undef_regs_other; auto. +Qed. + +(** Translation of arguments and results to builtins. *) + +Remark builtin_arg_match: + forall ms rs sp m a v, + agree ms sp rs -> + eval_builtin_arg ge ms sp m a v -> + eval_builtin_arg ge (to_Machrs rs) sp m a v. +Proof. + induction 2; simpl; eauto with barg. + unfold to_Machrs; erewrite agree_mregs; eauto. + econstructor. +Qed. + +Lemma builtin_args_match: + forall ms sp rs m, + agree ms sp rs -> + forall al vl, eval_builtin_args ge ms sp m al vl -> + eval_builtin_args ge (to_Machrs rs) sp m al vl. +Proof. + induction 2; intros; simpl; try (constructor; auto). + eapply eval_builtin_arg_preserved; eauto. + eapply builtin_arg_match; eauto. +Qed. + +Lemma agree_set_res res: forall ms sp rs v ms', + agree ms sp (set_from_Machrs ms' rs) -> + agree (set_res res v ms) sp (set_from_Machrs (set_res res v ms') rs). +Proof. + induction res; simpl; auto. Qed. Lemma find_function_ptr_agree ros ms rs sp b: @@ -617,8 +596,8 @@ Qed. Lemma extcall_arg_match ms sp rs m l v: agree ms sp rs -> - Mach.extcall_arg ms m sp l v -> - extcall_arg rs m l v. + extcall_arg ms m sp l v -> + extcall_arg rs m (rs#SP) l v. Proof. destruct 2. - erewrite agree_mregs; eauto. constructor. @@ -631,8 +610,8 @@ Local Hint Resolve extcall_arg_match: core. Lemma extcall_arg_pair_match: forall ms sp rs m p v, agree ms sp rs -> - Mach.extcall_arg_pair ms m sp p v -> - extcall_arg_pair rs m p v. + extcall_arg_pair ms m sp p v -> + extcall_arg_pair rs m (rs#SP) p v. Proof. destruct 2; constructor; eauto. Qed. @@ -642,8 +621,8 @@ Local Hint Resolve extcall_arg_pair_match: core. Lemma extcall_args_match: forall ms sp rs m, agree ms sp rs -> forall ll vl, - list_forall2 (Mach.extcall_arg_pair ms m sp) ll vl -> - list_forall2 (extcall_arg_pair rs m) ll vl. + list_forall2 (extcall_arg_pair ms m sp) ll vl -> + list_forall2 (extcall_arg_pair rs m rs#SP) ll vl. Proof. induction 2; constructor; eauto. Qed. @@ -651,10 +630,10 @@ Qed. Lemma extcall_arguments_match: forall ms m sp rs sg args, agree ms sp rs -> - Mach.extcall_arguments ms m sp sg args -> - extcall_arguments rs m sg args. + extcall_arguments ms m sp sg args -> + extcall_arguments rs m (rs#SP) sg args. Proof. - unfold Mach.extcall_arguments, extcall_arguments; intros. + unfold extcall_arguments, extcall_arguments; intros. eapply extcall_args_match; eauto. Qed. @@ -662,7 +641,8 @@ Qed. Local Hint Resolve functions_transl symbols_preserved (* agree_next_addr *) agree_mregs agree_set_mreg_parallel agree_undef_regs agree_set_other agree_change_sp - agree_sp_def agree_set_pair agree_undef_caller_save_regs f_equal Ptrofs.repr_unsigned parent_sp_def: core. + agree_sp_def agree_set_from_Machrs agree_set_pair agree_undef_caller_save_regs agree_set_res f_equal Ptrofs.repr_unsigned parent_sp_def + builtin_args_match external_call_symbols_preserved: core. Ltac simplify_regmap := repeat (rewrite ?Pregmap.gss; try (rewrite Pregmap.gso; try congruence)). @@ -701,7 +681,7 @@ Qed. Lemma basic_step_simulation: forall ms sp rs s f tf fb ms' bi m m', agree ms sp rs -> match_stack s -> - transf_function max_pos f = OK tf -> + transf_function f = OK tf -> Genv.find_funct_ptr ge fb = Some (Internal f) -> Machblock.basic_step ge s fb sp ms m bi ms' m' -> exists rs', basic_step tge tf rs m bi rs' m' /\ agree ms' sp rs' /\ rs' PC = rs PC. @@ -771,7 +751,7 @@ Qed. Lemma body_step_simulation: forall ms sp s f tf fb ms' bb m m', match_stack s -> - transf_function max_pos f = OK tf -> + transf_function f = OK tf -> Genv.find_funct_ptr ge fb = Some (Internal f) -> Machblock.body_step ge s fb sp bb ms m ms' m' -> forall rs, agree ms sp rs -> @@ -790,7 +770,7 @@ Qed. Local Hint Resolve trivial_exec_prologue: core. Lemma exit_step_simulation s fb f sp c t bb ms m s1' tf rs pc - (STEP:Machblock.exit_step rao ge (exit bb) (Machblock.State s fb sp (bb :: c) ms m) t s1') + (STEP: Machblock.exit_step rao ge (exit bb) (Machblock.State s fb sp (bb :: c) ms m) t s1') (STACKS: match_stack s) (AG: agree ms sp rs) (NXT: next_addr next tf rs = Some pc) @@ -869,7 +849,7 @@ Proof. assert(pc' = pc). { congruence. } subst. eauto. -- simplify_regmap. erewrite agree_sp; eauto. (* MBcond false *) - + eexists. eexists. split. + + inv H0. eexists. eexists. split. * apply exec_Some_exit. apply exec_MBcond_false. -- erewrite agree_mregs_list in H15; eauto. -- trivial. @@ -893,6 +873,7 @@ Proof. exploit find_label_goto_label; eauto. intros (pc' & GOTO_LABEL' & TRANSL). assert(pc' = pc). { congruence. } subst. eauto. -- simplify_regmap. erewrite agree_sp; eauto. + -- intros; simplify_regmap. eauto. + (* MBreturn *) try_simplify_someHyps. eexists. eexists. split. @@ -905,14 +886,13 @@ Proof. try_simplify_someHyps. * repeat econstructor; eauto. intros r. simplify_regmap. eapply agree_mregs; eauto. - - repeat econstructor; eauto. + - inv H0; repeat econstructor; eauto. erewrite agree_sp; eauto. Admitted. Lemma inst_step_simulation s fb f sp c t ms m s1' tf rs (STEP: Machblock.step rao ge (Machblock.State s fb sp c ms m) t s1') (STACKS: match_stack s) - (*FIND: Genv.find_funct_ptr ge fb = Some (Internal f)*) (* already in AT *) (AT: transl_code_at_pc fb f tf c (rs PC)) (AG: agree ms sp rs): exists s2' : state, plus (step next) tge (State rs m) t s2' /\ match_states s1' s2'. @@ -947,8 +927,6 @@ Proof. monadInv TRANSf. * (* internal calls *) right. - unfold transf_function in EQ. - destruct (zlt _ _); simpl in *; inv EQ. intuition. admit. (* TODO *) @@ -960,7 +938,6 @@ Proof. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. + econstructor; eauto. - unfold loc_external_result; eauto. - (* Returnstate *) inv STEP; simpl; right. inv STACKS; simpl in *; subst. |