diff options
Diffstat (limited to 'aarch64/Asmblockgenproof0.v')
-rw-r--r-- | aarch64/Asmblockgenproof0.v | 117 |
1 files changed, 116 insertions, 1 deletions
diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index 0187a494..69d6037c 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -42,6 +42,31 @@ Require Import Asmblockprops. Module MB:=Machblock. Module AB:=Asmblock. +(** * Agreement between Mach registers and processor registers *) + +Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree { + agree_sp: rs#SP = sp; + agree_sp_def: sp <> Vundef; + agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r)) +}. + +Lemma agree_exten: + forall ms sp rs rs', + agree ms sp rs -> + (forall r, data_preg r = true -> rs'#r = rs#r) -> + agree ms sp rs'. +Proof. + intros. destruct H. split; auto. + rewrite H0; auto. auto. + intros. rewrite H0; auto. apply preg_of_data. +Qed. + +Lemma preg_val: + forall ms sp rs r, agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r). +Proof. + intros. destruct H. auto. +Qed. + Inductive code_tail: Z -> bblocks -> bblocks -> Prop := | code_tail_0: forall c, code_tail 0 c c @@ -211,4 +236,94 @@ Proof. + exists Ptrofs.zero; red; intros. congruence. Qed. -End RETADDR_EXISTS.
\ No newline at end of file +End RETADDR_EXISTS. + +(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points + within the Asmblock code generated by translating Machblock function [f], + and [tc] is the tail of the generated code at the position corresponding + to the code pointer [pc]. *) + +Inductive transl_code_at_pc (ge: MB.genv): + val -> block -> MB.function -> MB.code -> bool -> AB.function -> AB.bblocks -> Prop := + transl_code_at_pc_intro: + forall b ofs f c ep tf tc, + Genv.find_funct_ptr ge b = Some(Internal f) -> + transf_function f = Errors.OK tf -> + transl_blocks f c ep = OK tc -> + code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc -> + transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc. + +Remark code_tail_no_bigger: + forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat. +Proof. + induction 1; simpl; omega. +Qed. + +Remark code_tail_unique: + forall fn c pos pos', + code_tail pos fn c -> code_tail pos' fn c -> pos = pos'. +Proof. + induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. + f_equal. eauto. +Qed. + +Lemma return_address_offset_correct: + forall ge b ofs fb f c tf tc ofs', + transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc -> + return_address_offset f c ofs' -> + ofs' = ofs. +Proof. + intros. inv H. red in H0. + exploit code_tail_unique. eexact H12. eapply H0; eauto. intro. + rewrite <- (Ptrofs.repr_unsigned ofs). + rewrite <- (Ptrofs.repr_unsigned ofs'). + congruence. +Qed. + +(** * Properties of the Machblock call stack *) + +Section MATCH_STACK. + +Variable ge: MB.genv. + +Inductive match_stack: list MB.stackframe -> Prop := + | match_stack_nil: + match_stack nil + | match_stack_cons: forall fb sp ra c s f tf tc, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transl_code_at_pc ge ra fb f c false tf tc -> + sp <> Vundef -> + match_stack s -> + match_stack (Stackframe fb sp ra c :: s). + +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 parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. +Proof. + induction 1; simpl. + unfold Vnullptr; destruct Archi.ptr64; congruence. + inv H0. congruence. +Qed. + +Lemma lessdef_parent_sp: + forall s v, + match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s. +Proof. + intros. inv H0. auto. exploit parent_sp_def; eauto. tauto. +Qed. + +Lemma lessdef_parent_ra: + forall s v, + match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s. +Proof. + intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. +Qed. + +End MATCH_STACK.
\ No newline at end of file |