diff options
Diffstat (limited to 'scheduling/PseudoAsmblockproof.v')
| -rw-r--r-- | scheduling/PseudoAsmblockproof.v | 1173 |
1 files changed, 1173 insertions, 0 deletions
diff --git a/scheduling/PseudoAsmblockproof.v b/scheduling/PseudoAsmblockproof.v new file mode 100644 index 00000000..67308278 --- /dev/null +++ b/scheduling/PseudoAsmblockproof.v @@ -0,0 +1,1173 @@ +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. |