Generals lemmas for asmblockgenproof

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