diff options
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/PseudoAsmblock.v | 267 | ||||
-rw-r--r-- | scheduling/PseudoAsmblockproof.v | 1173 |
2 files changed, 0 insertions, 1440 deletions
diff --git a/scheduling/PseudoAsmblock.v b/scheduling/PseudoAsmblock.v deleted file mode 100644 index b33ea1bd..00000000 --- a/scheduling/PseudoAsmblock.v +++ /dev/null @@ -1,267 +0,0 @@ -Require Import Coqlib Maps AST Integers Values Memory Events Globalenvs Smallstep. -Require Import Op Machregs Locations Stacklayout Conventions. -Require Import Mach Machblock OptionMonad. - - -(** Registers and States *) - -Inductive preg: Type := - | PC: preg (* program counter *) - | RA: preg (* return-address *) - | SP: preg (* stack-pointer *) - | preg_of: mreg -> preg. -Coercion preg_of: mreg >-> preg. - -Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. - decide equality. - apply mreg_eq. -Defined. - -Module PregEq. - Definition t := preg. - Definition eq := preg_eq. -End PregEq. - -Module Pregmap := EMap(PregEq). - -Definition regset := Pregmap.t val. - -Module AsmNotations. - -(* Declare Scope asm. *) -Notation "a # b" := (a b) (at level 1, only parsing) : asm. -Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. -Open Scope asm. - -End AsmNotations. - -Import AsmNotations. - -Definition to_Machrs (rs: regset): Mach.regset := - fun (r:mreg) => rs r. -Coercion to_Machrs: regset >-> Mach.regset. - -Definition set_from_Machrs (mrs: Mach.regset) (rs: regset): regset := - fun (r:preg) => - match r with - | preg_of mr => mrs mr - | _ => rs r - end. - -Local Open Scope option_monad_scope. - -Record state: Type := State { _rs: regset; _m: mem }. -Definition outcome := option state. -Definition Next rs m: outcome := Some (State rs m). -Definition Stuck: outcome := None. - -(* Asm semantic on Mach *) - -Section RELSEM. - -(** "oracle" stating the successive position (ie offset) of each block in the final assembly function *) -Variable next: function -> Z -> Z. - -Inductive is_pos (f: function): Z -> code -> Prop := - | First_pos: is_pos f 0 (fn_code f) - | Next_pos pos b c: is_pos f pos (b::c) -> is_pos f (next f pos) c. - -Fixpoint label_pos (f: function) (lbl: label) (pos: Z) (c: code) {struct c} : option Z := - match c with - | nil => None - | b :: c' => - if is_label lbl b then Some pos else label_pos f lbl (next f pos) c' - end. - -Definition goto_label (f: function) (lbl: label) (rs: regset) : option val := - SOME pos <- label_pos f lbl 0 (fn_code f) IN - match rs#PC with - | Vptr b _ => Some (Vptr b (Ptrofs.repr pos)) - | _ => None - end. - -Definition next_addr (f: function) (rs: regset): option val := - match rs#PC with - | Vptr b ofs => Some (Vptr b (Ptrofs.repr (next f (Ptrofs.unsigned ofs)))) - | _ => None - end. - -Variable ge:genv. - -Inductive basic_step (f: function) (rs: regset) (m:mem): basic_inst -> regset -> mem -> Prop := - | exec_MBgetstack: - forall ofs ty dst v, - load_stack m (rs#SP) ty ofs = Some v -> - basic_step f rs m (MBgetstack ofs ty dst) (rs#dst <- v) m - | exec_MBsetstack: - forall (src: mreg) ofs ty m' rs', - store_stack m (rs#SP) ty ofs (rs src) = Some m' -> - rs' = set_from_Machrs (undef_regs (destroyed_by_setstack ty) rs) rs -> - basic_step f rs m (MBsetstack src ofs ty) rs' m' - | exec_MBgetparam: - forall ofs ty (dst: mreg) v rs' psp, - load_stack m (rs#SP) Tptr f.(fn_link_ofs) = Some psp -> - load_stack m psp ty ofs = Some v -> - rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) -> - basic_step f rs m (MBgetparam ofs ty dst) rs' m - | exec_MBop: - forall op args v rs' (res: mreg), - eval_operation ge (rs#SP) op (to_Machrs rs)##args m = Some v -> - rs' = (set_from_Machrs (undef_regs (destroyed_by_op op) rs) rs)#res <- v -> - basic_step f rs m (MBop op args res) rs' m - | exec_MBload: - forall addr args a v rs' trap chunk (dst: mreg), - eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a -> - Mem.loadv chunk m a = Some v -> - rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- v -> - basic_step f rs m (MBload trap chunk addr args dst) rs' m - | exec_MBload_notrap1: - forall addr args rs' chunk (dst: mreg), - eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = None -> - rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- (default_notrap_load_value chunk) -> - basic_step f rs m (MBload NOTRAP chunk addr args dst) rs' m - | exec_MBload_notrap2: - forall addr args a rs' chunk (dst: mreg), - eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a -> - Mem.loadv chunk m a = None -> - rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- (default_notrap_load_value chunk) -> - basic_step f rs m (MBload NOTRAP chunk addr args dst) rs' m - | exec_MBstore: - forall chunk addr args (src: mreg) m' a rs', - eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a -> - Mem.storev chunk m a (rs src) = Some m' -> - rs' = set_from_Machrs (undef_regs (destroyed_by_store chunk addr) rs) rs -> - basic_step f rs m (MBstore chunk addr args src) rs' m' - . - - -Inductive body_step (f: function) : bblock_body -> regset -> mem -> regset -> mem -> Prop := - | exec_nil_body rs m: - body_step f nil rs m rs m - | exec_cons_body rs m bi p rs' m' rs'' m'': - basic_step f rs m bi rs' m' -> - body_step f p rs' m' rs'' m'' -> - body_step f (bi::p) rs m rs'' m'' - . - - -Definition find_function_ptr (ros: mreg + ident) (rs: regset) : option val := - match ros with - | inl r => Some (rs#r) - | inr symb => - SOME b <- Genv.find_symbol ge symb IN - Some (Vptr b Ptrofs.zero) - end. - -Definition exec_epilogue (f: function) (rs: regset) (m: mem) : outcome := - SOME sp <- load_stack m rs#SP Tptr f.(fn_link_ofs) IN - SOME ra <- load_stack m rs#SP Tptr f.(fn_retaddr_ofs) IN - match rs#SP with - | Vptr stk ofs => - SOME m' <- Mem.free m stk 0 f.(fn_stacksize) IN - Next (rs#SP <- sp #RA <- ra) m' - | _ => Stuck - end. - -Inductive cfi_step (f: function): control_flow_inst -> regset -> mem -> trace -> regset -> mem -> Prop := - | exec_MBcall sig ros rs m pc: - find_function_ptr ros rs = Some pc -> - cfi_step f (MBcall sig ros) rs m E0 ((rs#RA <- (rs#PC))#PC <- pc) m - | exec_MBtailcall sig ros rs m rs' m' pc: - find_function_ptr ros rs = Some pc -> - exec_epilogue f rs m = Next rs' m' -> - cfi_step f (MBtailcall sig ros) rs m E0 (rs'#PC <- pc) m' - | exec_MBreturn rs m rs' m': - exec_epilogue f rs m = Next rs' m' -> - cfi_step f MBreturn rs m E0 (rs'#PC <- (rs'#RA)) m' - | exec_MBgoto lbl rs m pc: - goto_label f lbl rs = Some pc -> - cfi_step f (MBgoto lbl) rs m E0 (rs#PC <- pc) m - | exec_MBcond_true cond args lbl rs m pc rs': - eval_condition cond (to_Machrs rs)##args m = Some true -> - goto_label f lbl rs = Some pc -> - rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs -> - cfi_step f (MBcond cond args lbl) rs m E0 (rs'#PC <- pc) m - | exec_MBcond_false cond args lbl rs m rs': - eval_condition cond (to_Machrs rs)##args m = Some false -> - rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs -> - cfi_step f (MBcond cond args lbl) rs m E0 rs' m - | exec_MBjumptable arg tbl rs m index lbl pc rs': - to_Machrs rs arg = Vint index -> - 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 - | 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_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': - cfi_step f ctl rs m t rs' m' -> - exit_step f (Some ctl) rs m t rs' m' - | exec_None_exit rs m: - exit_step f None rs m E0 rs m - . - -Inductive exec_bblock f: bblock -> regset -> mem -> trace -> regset -> mem -> Prop := - | exec_bblock_all (bb: bblock) rs0 m0 rs1 m1 pc t rs2 m2: - body_step f (body bb) rs0 m0 rs1 m1 -> - next_addr f rs1 = Some pc -> - exit_step f (exit bb) (rs1#PC <- pc) m1 t rs2 m2 -> - exec_bblock f bb rs0 m0 t rs2 m2. - -Definition exec_prologue f (pos:Z) (rs: regset) (m:mem) : option state := - if Z.eq_dec pos 0 then - let (m1, stk) := Mem.alloc m 0 f.(fn_stacksize) in - let sp := Vptr stk Ptrofs.zero in - SOME m2 <- store_stack m1 sp Tptr f.(fn_link_ofs) rs#SP IN - SOME m3 <- store_stack m2 sp Tptr f.(fn_retaddr_ofs) rs#RA IN - Next ((set_from_Machrs (undef_regs destroyed_at_function_entry rs) rs)#SP <- sp) m3 - else - Next rs m. - - -Inductive step: state -> trace -> state -> Prop := - | exec_step_internal b ofs f bb c rs0 m0 rs1 m1 t rs2 m2: - rs0 PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal f) -> - is_pos f (Ptrofs.unsigned ofs) (bb::c) -> - exec_prologue f (Ptrofs.unsigned ofs) rs0 m0 = Next rs1 m1 -> - exec_bblock f bb rs1 m1 t rs2 m2 -> - step (State rs0 m0) t (State rs2 m2) - | exec_step_external: - 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 (to_Machrs rs) m (rs#SP) (ef_sig ef) args -> - external_call ef ge args m t res m' -> - 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. - -Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall m0, - let ge := Genv.globalenv p in - Genv.init_mem p = Some m0 -> - let rs0 := - (Pregmap.init Vundef) - # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero) - # SP <- Vnullptr - # RA <- Vnullptr in - initial_state p (State rs0 m0). - -Inductive final_state: state -> int -> Prop := - | final_state_intro: forall rs m r retcode, - loc_result signature_main = One r -> - rs PC = Vnullptr -> - rs r = Vint retcode -> - final_state (State rs m) retcode. - -Definition semantics (next: function -> Z -> Z) (p: program) := - Semantics (step next) (initial_state p) final_state (Genv.globalenv p). diff --git a/scheduling/PseudoAsmblockproof.v b/scheduling/PseudoAsmblockproof.v deleted file mode 100644 index 67308278..00000000 --- a/scheduling/PseudoAsmblockproof.v +++ /dev/null @@ -1,1173 +0,0 @@ -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 IterList. - -(** Tiny translation from Machblock semantics to PseudoAsmblock semantics (needs additional checks) -*) - -Section TRANSLATION. - -(* 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. -*) - -Definition has_header (c: code) : bool := - match c with - | nil => false - | bb::_ => match header bb with - | nil => false - | _ => true - end - end. - -Definition insert_implicit_prologue c := - if has_header c then {| header := nil; body := nil; exit := None |}::c else c. - -Definition transl_function (f: function) : function := - {| fn_sig:=fn_sig f; - fn_code:=insert_implicit_prologue (fn_code f); - fn_stacksize := fn_stacksize f; - fn_link_ofs := fn_link_ofs f; - fn_retaddr_ofs := fn_retaddr_ofs f - |}. - -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. - -Definition transf_fundef (f: fundef) : res fundef := - transf_partial_fundef transf_function f. - -Definition transf_program (p: program) : res program := - transform_partial_program transf_fundef p. - -End TRANSLATION. - -(** Proof of the translation -*) - -Require Import Linking. -Import PseudoAsmblock.AsmNotations. - -Section PRESERVATION. - -Definition match_prog (p: program) (tp: program) := - match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. - -Lemma transf_program_match: - forall p tp, transf_program p = OK tp -> match_prog p tp. -Proof. - intros. eapply match_transform_partial_program; eauto. -Qed. - -Local Open Scope Z_scope. -Local Open Scope option_monad_scope. - -Variable prog: program. -Variable tprog: program. - -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; - agree_sp_def: sp <> Vundef; - agree_mregs: forall r: mreg, (ms r)=(rs#r) -}. - -(** [transl_code_at_pc pc fb f tf c] holds if the code pointer [pc] points - within the code generated by Machblock function (originally [f] -- but translated as [tf]), - and [c] is the tail of the code at the position corresponding to the code pointer [pc]. -*) -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 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 *) - is_pos next tf (Ptrofs.unsigned ofs) c -> - transl_code_at_pc b f tf c (Vptr b ofs). - -Inductive match_stack: list stackframe -> Prop := - | match_stack_nil: - match_stack nil - | match_stack_cons: forall fb sp ra c s f tf, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - transl_code_at_pc fb f tf c ra -> - sp <> Vundef -> - match_stack s -> - match_stack (Stackframe fb sp ra c :: s). - -(** Semantic preservation is proved using simulation diagrams - of the following form. -<< - s1 ---------------- s2 - | | - t| *|t - | | - v v - s1'---------------- s2' ->> - The invariant is the [match_states] predicate below... - -*) - -Inductive match_states: Machblock.state -> state -> Prop := - | match_states_internal s fb sp c ms m rs f tf - (STACKS: match_stack s) - (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) - (AT: transl_code_at_pc fb f tf c (rs PC)) - (AG: agree ms sp rs): - match_states (Machblock.State s fb sp c ms m) - (State rs m) - | match_states_prologue s sp fb ms rs0 m0 f rs1 m1 - (STACKS: match_stack s) - (AG: agree ms sp rs1) - (ATPC: rs0 PC = Vptr fb Ptrofs.zero) - (ATLR: rs0 RA = parent_ra s) - (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) - (PROL: exec_prologue f 0 rs0 m0 = Next rs1 m1): - match_states (Machblock.State s fb sp (fn_code f) ms m1) - (State rs0 m0) - | match_states_call s fb ms m rs - (STACKS: match_stack s) - (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = Vptr fb Ptrofs.zero) - (ATLR: rs RA = parent_ra s): - match_states (Machblock.Callstate s fb ms m) - (State rs m) - | match_states_return s ms m rs - (STACKS: match_stack s) - (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = parent_ra s): - match_states (Machblock.Returnstate s ms m) - (State rs m). - -Definition measure (s: Machblock.state) : nat := - match s with - | Machblock.State _ _ _ _ _ _ => 0%nat - | Machblock.Callstate _ _ _ _ => 1%nat - | Machblock.Returnstate _ _ _ => 1%nat - end. - -Definition rao (f: function) (c: code) (ofs: ptrofs) : Prop := - forall tf, - transf_function f = OK tf -> - is_pos next tf (Ptrofs.unsigned ofs) c. - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_match TRANSF). - -Lemma senv_preserved: - Senv.equiv ge tge. -Proof (Genv.senv_match TRANSF). - -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 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 f = OK tf -> - Genv.find_funct_ptr tge fb = Some (Internal tf). -Proof. - intros. exploit functions_translated; eauto. intros [tf' [A B]]. - monadInv B. inv H0; auto. -Qed. - -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. - intros; eapply functions_bound_max_pos; eauto. - eapply functions_transl; eauto. -Qed. - -Lemma transf_function_def f tf: - transf_function f = OK tf -> tf.(fn_code) = insert_implicit_prologue f.(fn_code). -Proof. - unfold transf_function. - intros EQ; inv EQ. - auto. -Qed. - -Lemma stackinfo_preserved f 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. - intros EQ0; inv EQ0. simpl; intuition. -Qed. - -Lemma transf_initial_states st1: Machblock.initial_state prog st1 -> - exists st2, initial_state tprog st2 /\ match_states st1 st2. -Proof. - intro H. inversion H. unfold ge0 in *. - econstructor; split. - - econstructor. - eapply (Genv.init_mem_transf_partial TRANSF); eauto. - - replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero) - with (Vptr fb Ptrofs.zero). - + econstructor; eauto. - * constructor. - * split; auto; simpl; unfold Vnullptr; destruct Archi.ptr64; congruence. - + unfold Genv.symbol_address. - rewrite (match_program_main TRANSF). - rewrite symbols_preserved. - unfold ge. simplify_someHyp. auto. -Qed. - -Lemma transf_final_states st1 st2 r: - match_states st1 st2 -> Machblock.final_state st1 r -> final_state st2 r. -Proof. - intros H H0. inv H0. inv H. - econstructor; eauto. - exploit agree_mregs; eauto. - erewrite H2. intro H3; inversion H3. - auto. -Qed. - -(** Lemma on [is_pos]. *) - -Lemma is_pos_alt_def f pos code: is_pos next f pos code -> - exists n, (n <= List.length (fn_code f))%nat /\ pos = (iter n (next f) 0) /\ code = iter_tail n (fn_code f). -Proof. - induction 1. - - unfold iter_tail; exists O; simpl; intuition. - - destruct IHis_pos as (n & H0 & H1 & H2). - exists (S n). repeat split. - + rewrite (length_iter_tail n); eauto. - rewrite <- H2; simpl; omega. - + rewrite iter_S; congruence. - + unfold iter_tail in *; rewrite iter_S, <- H2; auto. -Qed. - -Local Hint Resolve First_pos Next_pos: core. - -Lemma is_pos_alt_def_recip f n: (n <= List.length (fn_code f))%nat -> - is_pos next f (iter n (next f) 0) (iter_tail n (fn_code f)). -Proof. - induction n. - - unfold iter_tail; simpl; eauto. - - 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. - -Lemma is_pos_inject1 f pos1 pos2 code: - is_pos next f pos1 code -> is_pos next f pos2 code -> pos1=pos2. -Proof. - intros H1 H2. - destruct (is_pos_alt_def f pos1 code) as (n1 & B1 & POS1 & CODE1); eauto. - destruct (is_pos_alt_def f pos2 code) as (n2 & B2 & POS2 & CODE2); eauto. - clear H1 H2; subst. - erewrite (iter_tail_inject1 n1 n2); eauto. -Qed. - -Lemma iter_next_strict_monotonic f n m x: (n < m)%nat -> iter n (next f) x < iter m (next f) x. -Proof. - induction 1; rewrite iter_S; auto. - generalize (next_progress f (iter m (next f) x)). - omega. -Qed. - -Lemma iter_next_monotonic f n m x: (n <= m)%nat -> iter n (next f) x <= iter m (next f) x. -Proof. - destruct 1. - - omega. - - generalize (iter_next_strict_monotonic f n (S m) x). omega. -Qed. - -Lemma is_pos_bound_pos f pos code: - is_pos next f pos code -> 0 <= pos <= max_pos f. -Proof. - intros H; exploit is_pos_alt_def; eauto. - intros (n & H1 & H2 & H3). - rewrite H2. unfold max_pos. split. - - cutrewrite (0 = iter O (next f) 0); auto. - apply iter_next_monotonic; omega. - - apply iter_next_monotonic; omega. -Qed. - -Lemma is_pos_unsigned_repr f pos code: - is_pos next f pos code -> - max_pos f <= Ptrofs.max_unsigned -> - Ptrofs.unsigned (Ptrofs.repr pos) = pos. -Proof. - intros; eapply Ptrofs.unsigned_repr. - exploit is_pos_bound_pos; eauto. - omega. -Qed. - -Lemma is_pos_simplify f pos code: - is_pos next f pos code -> - max_pos f <= Ptrofs.max_unsigned -> - is_pos next f (Ptrofs.unsigned (Ptrofs.repr pos)) code. -Proof. - intros; erewrite is_pos_unsigned_repr; eauto. -Qed. - -Lemma find_label_label_pos f lbl c: forall pos c', - find_label lbl c = Some c' -> - exists n, - label_pos next f lbl pos c = Some (iter n (next f) pos) - /\ c' = iter_tail n c - /\ (n <= List.length c)%nat. -Proof. - induction c. - - simpl; intros. discriminate. - - simpl; intros pos c'. - destruct (is_label lbl a). - + intro EQ; injection EQ; intro; subst c'. - exists O; simpl; intuition. - + intros. generalize (IHc (next f pos) c' H). intros (n' & A & B & C). - exists (S n'). intuition. -Qed. - -Lemma find_label_insert_implicit_prologue lbl c: - find_label lbl c = find_label lbl (insert_implicit_prologue c). -Proof. - unfold insert_implicit_prologue. - destruct (has_header c); simpl; auto. - unfold is_label; simpl. - destruct (in_dec lbl nil); auto. - simpl in *. tauto. -Qed. - -Lemma no_header_insert_implicit_prologue c: - has_header (insert_implicit_prologue c) = false. -Proof. - unfold insert_implicit_prologue. - destruct (has_header c) eqn: H; simpl; auto. -Qed. - -Lemma find_label_has_header lbl c c': - find_label lbl c = Some c' -> - has_header c' = true. -Proof. - induction c; simpl; try congruence. - destruct (is_label lbl a) eqn:LAB; auto. - intros X; inv X; simpl. - unfold is_label in LAB. - destruct (in_dec lbl (header a)); try congruence. - destruct (header a); try congruence. - simpl in *; tauto. -Qed. - -Lemma find_label_label_pos_no_header f lbl c pos c': - (has_header c) = false -> - find_label lbl c = Some c' -> - exists n, - label_pos next f lbl pos c = Some (iter (S n) (next f) pos) - /\ c' = iter_tail (S n) c - /\ ((S n) <= List.length c)%nat. -Proof. - intros H H0; exploit find_label_label_pos; eauto. - intros ([|n] & H1 & H2 & H3); try (exists n; intuition eauto). - unfold iter_tail in *; simpl in *; subst. - erewrite find_label_has_header in H; eauto. - congruence. -Qed. - -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 f = OK tf -> - Vptr b ofs = rs PC -> - find_label lbl f.(fn_code) = Some c' -> - exists pc, - goto_label next tf lbl rs = Some pc - /\ transl_code_at_pc b f tf c' pc. -Proof. - intros FINDF T HPC FINDL. - erewrite find_label_insert_implicit_prologue, <- transf_function_def in FINDL; eauto. - exploit find_label_label_pos_no_header; eauto. - { erewrite transf_function_def; eauto. - apply no_header_insert_implicit_prologue. - } - intros (n & LAB & CODE & BOUND); subst. - exists (Vptr b (Ptrofs.repr (iter (S n) (next tf) 0))). - unfold goto_label; intuition. - - simplify_someHyps; rewrite <- HPC. auto. - - econstructor; eauto. - erewrite is_pos_unsigned_repr; eauto. - generalize (iter_next_strict_monotonic tf O (S n) 0); simpl. - omega. -Qed. - -(** Preservation of register agreement under various assignments. *) - -Lemma agree_mregs_list ms sp rs: - agree ms sp rs -> - forall l, (ms##l)=(to_Machrs rs)##l. -Proof. - unfold to_Machrs. intros AG; induction l; simpl; eauto. - erewrite agree_mregs; eauto. - congruence. -Qed. - -Lemma agree_set_mreg ms sp rs r v rs': - agree ms sp rs -> - v=(rs'#(preg_of r)) -> - (forall r', r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros H H0 H1. destruct H. split; auto. - - rewrite H1; auto. destruct r; simpl; congruence. - - intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. - rewrite H1; auto. destruct r; simpl; congruence. -Qed. - -Corollary agree_set_mreg_parallel: - forall ms sp rs r v, - agree ms sp 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 - | _ => false - end. - -Lemma agree_exten ms sp rs rs': - agree ms sp rs -> - (forall r, data_preg r = true -> rs'#r = rs#r) -> - agree ms sp rs'. -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 -> - agree ms sp (rs#r <- v). -Proof. - intros; apply agree_exten with rs; auto. - intros. apply Pregmap.gso. congruence. -Qed. - - -Lemma agree_next_addr f ms sp b pos rs: - agree ms sp rs -> - agree ms sp (rs#PC <- (Vptr b (Ptrofs.repr (next f pos)))). -Proof. - intros. apply agree_set_other; auto. -Qed. - -Local Hint Resolve agree_set_mreg_parallel2: core. - -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 H; destruct p; simpl; auto. -Qed. - -Lemma agree_undef_caller_save_regs: - 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 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': - agree ms sp rs -> sp' <> Vundef -> - agree ms sp' (rs#SP <- sp'). -Proof. - intros H H0. inv H. split; auto. -Qed. - -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. destruct H; subst. split; auto. - intros. destruct (In_dec mreg_eq r rl). - + 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: - agree ms sp rs -> - Machblock.find_function_ptr ge ros ms = Some b -> - find_function_ptr tge ros rs = Some (Vptr b Ptrofs.zero). -Proof. - intros AG; unfold Mach.find_function_ptr; destruct ros as [r|s]; simpl; auto. - - generalize (agree_mregs _ _ _ AG r). destruct (ms r); simpl; try congruence. - intros H; inv H; try congruence. - inversion_ASSERT. intros H; rewrite (Ptrofs.same_if_eq _ _ H); eauto. - try_simplify_someHyps. - - intros H; rewrite symbols_preserved, H. auto. -Qed. - -Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. -Proof. - induction 1; simpl. - unfold Vnullptr; destruct Archi.ptr64; congruence. - auto. -Qed. - -Lemma extcall_arg_match ms sp rs m l v: - agree ms sp rs -> - extcall_arg ms m sp l v -> - extcall_arg rs m (rs#SP) l v. -Proof. - destruct 2. - - erewrite agree_mregs; eauto. constructor. - - unfold load_stack in *. econstructor; eauto. - erewrite agree_sp; eauto. -Qed. - -Local Hint Resolve extcall_arg_match: core. - -Lemma extcall_arg_pair_match: - forall ms sp rs m p v, - agree ms sp rs -> - extcall_arg_pair ms m sp p v -> - extcall_arg_pair rs m (rs#SP) p v. -Proof. - destruct 2; constructor; eauto. -Qed. - -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 (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. - -Lemma extcall_arguments_match: - forall ms m sp rs sg args, - agree ms sp rs -> - extcall_arguments ms m sp sg args -> - extcall_arguments rs m (rs#SP) sg args. -Proof. - unfold extcall_arguments, extcall_arguments; intros. - eapply extcall_args_match; eauto. -Qed. - -(** A few tactics *) - -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_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)). - -Ltac simplify_next_addr := - match goal with - | [ HPC: Vptr _ _ = _ PC |- _ ] => try (unfold next_addr, Val.offset_ptr); simplify_regmap; try (rewrite <- HPC) - end. - -Ltac discharge_match_states := - econstructor; eauto; try ( simplify_next_addr; econstructor; eauto ). - - -(** Instruction step simulation lemma: the simulation lemma for stepping one instruction - -<< - s1 ---------------- s2 - | | - t| +|t - | | - v v - s1'---------------- s2' ->> - -*) - -Lemma trivial_exec_prologue: - forall tf ofs rs m, - 0 < Ptrofs.unsigned ofs -> - exec_prologue tf (Ptrofs.unsigned ofs) rs m = Next rs m. -Proof. - unfold exec_prologue. intros. - destruct (Z.eq_dec); eauto. omega. -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 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. -Proof. - destruct 5. - (* MBgetstack *) - - eexists; split. - + econstructor; eauto. erewrite agree_sp; eauto. - + eauto. - (* MBsetstack *) - - eexists; split. - + econstructor; eauto. - erewrite agree_sp; eauto. - erewrite <- agree_mregs; eauto. - + rewrite H4; split; eauto. - (* MBgetparam *) - - eexists; split. - + econstructor; eauto. - erewrite agree_sp; eauto. - assert (f = f0). { rewrite H2 in H3. inversion H3. reflexivity. } - assert (fn_link_ofs tf = fn_link_ofs f0). { - rewrite <- H7. - eapply stackinfo_preserved. eauto. - } - rewrite H8. eauto. - + rewrite H6; split; eauto. - (* MBop *) - - eexists; split. - + econstructor; eauto. - erewrite agree_sp; eauto. - erewrite agree_mregs_list in H3. - * erewrite <- H3. - eapply eval_operation_preserved; trivial. - * eauto. - + rewrite H4; split; eauto. - (* MBload *) - - eexists; split. - + econstructor; eauto. - erewrite agree_sp; eauto. erewrite <- agree_mregs_list; eauto. - erewrite <- H3. - eapply eval_addressing_preserved; trivial. - + rewrite H5; split; eauto. - (* MBload notrap1 *) - - eexists; split. - + eapply exec_MBload_notrap1; eauto. - erewrite agree_sp; eauto. - erewrite agree_mregs_list in H3; eauto. - * erewrite eval_addressing_preserved; eauto. - + rewrite H4; eauto. - (* MBload notrap2 *) - - eexists; split. - + eapply exec_MBload_notrap2; eauto. - erewrite agree_sp; eauto. - erewrite agree_mregs_list in H3; eauto. - * erewrite eval_addressing_preserved; eauto. - + rewrite H5; eauto. - (* MBstore *) - - eexists; split. - + econstructor; eauto. - * erewrite agree_sp; eauto. - erewrite agree_mregs_list in H3. - erewrite eval_addressing_preserved; eauto. - eauto. - * erewrite <- agree_mregs; eauto. - + rewrite H5; eauto. -Qed. - -Lemma body_step_simulation: forall ms sp s f tf fb ms' bb m m', - match_stack s -> - 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 -> - exists rs', body_step tge tf bb rs m rs' m' /\ agree ms' sp rs' /\ rs' PC = rs PC. -Proof. - induction 4. - - repeat (econstructor; eauto). - - intros. exploit basic_step_simulation; eauto. - intros (rs'0 & BASIC & AG1' & AGPC1). - exploit IHbody_step; eauto. - intros (rs'1 & BODY & AG2' & AGPC2). - repeat (econstructor; eauto). - congruence. -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') - (STACKS: match_stack s) - (AG: agree ms sp rs) - (NXT: next_addr next tf rs = Some pc) - (AT: transl_code_at_pc fb f tf c pc): - exists rs' m', exit_step next tge tf (exit bb) (rs#PC <- pc) m t rs' m' /\ match_states s1' (State rs' m'). -Proof. - inv AT. - inv STEP. - (* cfi_step currently only defined for exec_MBcall, exec_MBreturn, and exec_MBgoto *) - - inversion H4; subst. clear H4. (* inversion_clear H4 does not work so well: it clears an important hypothesis about "sp" in the Mreturn case *) - (* MBcall *) - + eexists. eexists. split. - * apply exec_Some_exit. - apply exec_MBcall. - eapply find_function_ptr_agree; eauto. - * assert (f0 = f). { congruence. } subst. - assert (Ptrofs.unsigned ra = Ptrofs.unsigned ofs). { - eapply is_pos_inject1; eauto. - } - assert (ofs = ra). { - apply Ptrofs.same_if_eq. unfold Ptrofs.eq. - rewrite H4. rewrite zeq_true. reflexivity. - } - repeat econstructor; eauto. - -- unfold rao in *. congruence. - -- simpl. simplify_regmap. - erewrite agree_sp; eauto. - -- simpl. simplify_regmap. auto. - (* MBtailcall *) - + assert (f0 = f). { congruence. } subst. - eexists. eexists. split. - * repeat econstructor. - -- eapply find_function_ptr_agree; eauto. - -- unfold exec_epilogue. erewrite agree_sp; eauto. - apply stackinfo_preserved in H0 as ( SS & RA & LO ). - rewrite SS, RA, LO. - try_simplify_someHyps. - * repeat econstructor; eauto. - intros r. - eapply agree_mregs; eapply agree_set_other; eauto. - (* MBbuiltin *) - +eexists. eexists. split. - * repeat econstructor. - -- simplify_regmap. erewrite agree_sp; eauto. - eapply eval_builtin_args_preserved; eauto. - -- eapply external_call_symbols_preserved; eauto. - exact senv_preserved. - * repeat econstructor; eauto. - -- assert (transl_function f = tf). { - unfold transf_function in *. congruence. - } - erewrite H5. assumption. - -- eapply agree_sp. eapply agree_set_res. eapply agree_undef_regs. - eapply agree_set_from_Machrs; eauto. - -- intros; simpl. - eapply agree_set_res. eapply agree_undef_regs. - eapply agree_set_from_Machrs; eauto. - (* MBgoto *) - + simplify_someHyps. intros. - assert ((rs # PC <- (Vptr fb ofs)) PC = Vptr fb ofs). { - rewrite Pregmap.gss. reflexivity. - } - eassert (exists pc, goto_label next tf lbl rs # PC <- (Vptr fb ofs) = Some pc - /\ transl_code_at_pc fb f tf c' pc) as (pc & GOTO_LABEL & _). { - eapply find_label_goto_label; eauto. - } - eexists. eexists. split. - * apply exec_Some_exit. - apply exec_MBgoto. - rewrite GOTO_LABEL. trivial. - * repeat econstructor; eauto. - -- simplify_regmap. - exploit find_label_goto_label; eauto. intros (pc' & GOTO_LABEL' & TRANSL). - assert(pc' = pc). { congruence. } subst. eauto. - -- simplify_regmap. erewrite agree_sp; eauto. - (* MBcond true *) - (* Mostly copy and paste from MBgoto *) - + simplify_someHyps. intros. - assert ((rs # PC <- (Vptr fb ofs)) PC = Vptr fb ofs). { - rewrite Pregmap.gss. reflexivity. - } - eassert (exists pc, goto_label next tf lbl rs # PC <- (Vptr fb ofs) = Some pc - /\ transl_code_at_pc fb f tf c' pc) as (pc & GOTO_LABEL & _). { - eapply find_label_goto_label; eauto. - } - eexists. eexists. split. - * apply exec_Some_exit. eapply exec_MBcond_true; eauto. - erewrite agree_mregs_list in H14; eauto. - * repeat econstructor; eauto. - -- simplify_regmap. - exploit find_label_goto_label; eauto. intros (pc' & GOTO_LABEL' & TRANSL). - assert(pc' = pc). { congruence. } subst. eauto. - -- simplify_regmap. erewrite agree_sp; eauto. - (* MBcond false *) - + inv H0. eexists. eexists. split. - * apply exec_Some_exit. apply exec_MBcond_false. - -- erewrite agree_mregs_list in H15; eauto. - -- trivial. - * repeat econstructor; eauto. erewrite agree_sp; eauto. - (* MBjumptable *) - + simplify_someHyps. intros. - assert ((rs # PC <- (Vptr fb ofs)) PC = Vptr fb ofs). { - rewrite Pregmap.gss. reflexivity. - } - eassert (exists pc, goto_label next tf lbl rs # PC <- (Vptr fb ofs) = Some pc - /\ transl_code_at_pc fb f tf c' pc) as (pc & GOTO_LABEL & _). { - eapply find_label_goto_label; eauto. - } - eexists. eexists. split. - * repeat econstructor; eauto. - rewrite <- H14. - symmetry. eapply agree_mregs. eapply agree_set_other; eauto. - * repeat econstructor; eauto. - (* copy paste from MBgoto *) - -- simplify_regmap. - 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. - * apply exec_Some_exit. - apply exec_MBreturn. - unfold exec_epilogue. - erewrite agree_sp; eauto. - apply stackinfo_preserved in H0 as ( SS & RA & LO ). - rewrite SS, RA, LO. - try_simplify_someHyps. - * repeat econstructor; eauto. intros r. - simplify_regmap. eapply agree_mregs; eauto. - - inv H0; repeat econstructor; eauto. - erewrite agree_sp; eauto. -Qed. - -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) - (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'. -Proof. - inv STEP. - inv AT. - exploit body_step_simulation; eauto. intros (rs0' & BODY & AG0 & AGPC). - assert (NXT: next_addr next tf rs0' = Some (Vptr fb (Ptrofs.repr (next tf (Ptrofs.unsigned ofs))))). - { unfold next_addr; rewrite AGPC, <- H; simpl; eauto. } - exploit exit_step_simulation; eauto. - { econstructor; eauto. - erewrite is_pos_unsigned_repr; eauto. - generalize (next_progress tf (Ptrofs.unsigned ofs)); omega. } - intros (rs2 & m2 & STEP & MS). - eexists. - split; eauto. - eapply plus_one. - eapply exec_step_internal; eauto. - econstructor; eauto. -Qed. - -Lemma prologue_preserves_pc: forall f rs0 m0 rs1 m1, - exec_prologue f 0 rs0 m0 = Next rs1 m1 -> - rs1 PC = rs0 PC. -Proof. - unfold exec_prologue; simpl; - intros f rs0 m0 rs1 m1 H. - destruct (Mem.alloc m0 0 (fn_stacksize f)) in H; unfold Next in H. - simplify_someHyps; inversion_SOME ignored; inversion_SOME ignored'; - intros ? ? H'; inversion H'; trivial. -Qed. - -Lemma is_pos_next_zero bb c fb f - (FIND : Genv.find_funct_ptr ge fb = Some (Internal f)) - (FN_HEAD : bb :: c = fn_code f): - is_pos next (transl_function f) (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)) (if has_header (fn_code f) then bb::c else c). -Proof. - exploit (transf_function_def f). unfold transf_function; auto. - unfold insert_implicit_prologue. - intros fn_code_tf; destruct (has_header (fn_code f)); - eapply Next_pos; rewrite Ptrofs.unsigned_zero; - rewrite FN_HEAD; rewrite <- fn_code_tf; apply First_pos. -Qed. - -Lemma prologue_simulation_no_header_step t s1' s sp fb ms f m1 rs0 m0 rs1 - (STACKS : match_stack s) - (AG : agree ms sp rs1) - (ATPC : rs0 PC = Vptr fb Ptrofs.zero) - (ATLR : rs0 RA = parent_ra s) - (FIND : Genv.find_funct_ptr ge fb = Some (Internal f)) - (PROL : exec_prologue f 0 rs0 m0 = Next rs1 m1) - (STEP : Machblock.step rao ge (Machblock.State s fb sp (fn_code f) ms m1) t s1') - (NO_HEADER: has_header (fn_code f) = false): - exists s2' : state, step next tge {| _rs := rs0; _m := m0 |} t s2' /\ match_states s1' s2'. -Proof. - inv STEP. - - exploit functions_translated; eauto; - intros (tf & FINDtf & TRANSf); monadInv TRANSf. - assert (fn_code f = fn_code (transl_function f)) as TF_CODE. { - unfold transl_function; simpl; unfold insert_implicit_prologue; - rewrite NO_HEADER; trivial. - } - - exploit body_step_simulation; eauto; unfold transf_function; auto. - intros (rs0' & BODY & AG0 & AGPC). - - exploit prologue_preserves_pc; eauto. - intros AGPC'. - - exploit is_pos_next_zero; eauto; rewrite NO_HEADER. - intros IS_POS. - - exploit transl_code_at_pc_intro; eauto; unfold transf_function; auto. { - rewrite Ptrofs.unsigned_zero; erewrite is_pos_unsigned_repr; eauto. - } intros TRANSL_CODE. - - assert (next_addr next (transl_function f) rs0' = - Some (Vptr fb (Ptrofs.repr (next (transl_function f) - (Ptrofs.unsigned Ptrofs.zero))))) as NEXT_ADDR. { - unfold next_addr; rewrite AGPC; rewrite AGPC'; rewrite ATPC; reflexivity. - } - - exploit exit_step_simulation; eauto. - intros (? & ? & EXIT_STEP & MATCH_EXIT). - - exploit exec_bblock_all; eauto. - intros EXEC_BBLOCK. - - exploit exec_step_internal; eauto. - apply is_pos_simplify; eauto. rewrite H3; rewrite TF_CODE; apply First_pos. -Qed. - -Lemma prologue_simulation_header_step t s1' s sp fb ms f m1 rs0 m0 rs1 - (STACKS : match_stack s) - (AG : agree ms sp rs1) - (ATPC : rs0 PC = Vptr fb Ptrofs.zero) - (ATLR : rs0 RA = parent_ra s) - (FIND : Genv.find_funct_ptr ge fb = Some (Internal f)) - (PROL : exec_prologue f 0 rs0 m0 = Next rs1 m1) - (STEP : Machblock.step rao ge (Machblock.State s fb sp (fn_code f) ms m1) t s1') - (HEADER: has_header (fn_code f) = true): - exists s2' : state, plus (step next) tge {| _rs := rs0; _m := m0 |} t s2' /\ match_states s1' s2'. -Proof. - inv STEP. - - (* FIRST STEP *) - exploit functions_translated; eauto; - intros (tf & FINDtf & TRANSf); monadInv TRANSf. - exploit transf_function_def; eauto; unfold transf_function; auto; - unfold insert_implicit_prologue; rewrite HEADER; intros TF_CODE. - - exploit is_pos_next_zero; eauto; rewrite HEADER; rewrite H3; - intros IS_POS. - - exploit prologue_preserves_pc; eauto. - intros AGPC'. - - assert ( next_addr next (transl_function f) rs1 - = Some (Vptr fb (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)))) - ) as NEXT_ADDR0. { unfold next_addr; rewrite AGPC'; rewrite ATPC; trivial. } - - exploit exec_nil_body; intros BODY0. - assert ((body {| header := nil; body := nil; exit := None |}) = nil) as NIL; auto. - rewrite <- NIL in BODY0. - - exploit exec_None_exit; intros EXIT0. - assert ((exit {| header := nil; body := nil; exit := None |}) = None) as NONE; auto. - rewrite <- NONE in EXIT0. - - exploit exec_bblock_all; eauto; - intros BBLOCK0. - - exploit exec_step_internal; eauto. rewrite <- TF_CODE; apply First_pos. - intros STEP0. - - clear BODY0 BBLOCK0 EXIT0. - - (* SECOND step *) - - exploit (mkagree ms sp - (rs1 # PC <- (Vptr fb (Ptrofs.repr (next (transl_function f) - (Ptrofs.unsigned Ptrofs.zero)))))); eauto. - apply (agree_sp ms); apply agree_set_other; eauto. - intros AG'. - - exploit body_step_simulation; eauto; unfold transf_function; auto. - intros (rs1' & BODY1 & AGRS1' & AGPC). - - assert ( next_addr next (transl_function f) rs1' - = Some (Vptr fb (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned - (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero))))))) - ) as NEXT_ADDR1. { unfold next_addr; rewrite AGPC; reflexivity. } - - assert (IS_POS' := IS_POS). - rewrite <- H3 in IS_POS'; apply Next_pos in IS_POS'. - exploit transl_code_at_pc_intro; eauto; unfold transf_function; auto. { - rewrite Ptrofs.unsigned_zero; erewrite is_pos_unsigned_repr; eauto. - assert (0 < next (transl_function f) 0) as Z0. { apply next_progress. } - assert ( next (transl_function f) 0 - < next (transl_function f) (next (transl_function f) 0) - ) as Z1. { apply next_progress. } - rewrite <- Z1. exact Z0. - } intros TRANSL_CODE1. - - exploit exit_step_simulation; eauto. - rewrite Ptrofs.unsigned_repr. - 2: { - assert(max_pos (transl_function f) <= Ptrofs.max_unsigned) as MAX_POS. { - eapply functions_bound_max_pos; eauto. - } - rewrite <- MAX_POS. - eapply is_pos_bound_pos; eauto. - } - exact TRANSL_CODE1. - intros (? & ? & EXIT_STEP & MATCH_EXIT). - - exploit (trivial_exec_prologue (transl_function f) (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)))). { - rewrite Ptrofs.unsigned_zero; erewrite is_pos_unsigned_repr; eauto. - } intros NO_PROL. - - exploit exec_bblock_all; eauto; intros BBLOCK1. - - clear AGPC. - rewrite <- H3 in IS_POS. - exploit (exec_step_internal next tge fb - (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero))) - (transl_function f) - bb c); simplify_regmap; eauto. - - intros STEP1. - - eexists; split. - + eapply plus_two. - * exact STEP0. - * exact STEP1. - * trivial. - + assumption. -Qed. - -Lemma step_simulation s1 t s1': - Machblock.step rao ge s1 t s1' -> - forall s2, match_states s1 s2 -> - (exists s2', plus (step next) tge s2 t s2' /\ match_states s1' s2') \/ ((measure s1' < measure s1)%nat /\ t = E0 /\ match_states s1' s2). -Proof. - intros STEP s2 MATCH; destruct MATCH. - - exploit inst_step_simulation; eauto. - - left. - destruct (has_header (fn_code f)) eqn:NO_HEADER. - + eapply prologue_simulation_header_step; eauto. - + exploit prologue_simulation_no_header_step; eauto; - intros (s2' & NO_HEADER_STEP & MATCH_STATES). - eexists; split; eauto. - apply plus_one; eauto. - - inv STEP; simpl; exploit functions_translated; eauto; - intros (tf0 & FINDtf & TRANSf); - monadInv TRANSf. - * (* internal calls *) - right. - intuition. - econstructor; eauto. - -- exploit - (mkagree (undef_regs destroyed_at_function_entry ms) - sp - (set_from_Machrs (undef_regs destroyed_at_function_entry rs) rs) # SP <- sp - ); eauto. - ++ unfold sp; discriminate. - ++ intros mr; unfold undef_regs; - induction destroyed_at_function_entry as [ | ? ? IH]. - ** inversion AG as [_ _ AG_MREGS]; apply AG_MREGS. - ** fold undef_regs in *; - unfold Regmap.set; simpl; rewrite IH; reflexivity. - -- unfold exec_prologue; - inversion AG as (RS_SP & ?); rewrite RS_SP; fold sp; - rewrite H4; fold sp; rewrite H7; rewrite ATLR; rewrite H8; eauto. - * (* external calls *) - left. - exploit extcall_arguments_match; eauto. - eexists; split. - + eapply plus_one. - eapply exec_step_external; eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - + econstructor; eauto. - - (* Returnstate *) - inv STEP; simpl; right. - inv STACKS; simpl in *; subst. - repeat (econstructor; eauto). -Qed. - -(** * The main simulation theorem *) - -Theorem transf_program_correct: - forward_simulation (Machblock.semantics rao prog) (semantics next tprog). -Proof. - eapply forward_simulation_star with (measure := measure). - apply senv_preserved. - - eexact transf_initial_states. - - eexact transf_final_states. - - eexact step_simulation. -Qed. - -End PRESERVATION. |