Commit 21f6353c authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Generals lemmas for asmblockgenproof

parent ffc27e40
......@@ -41,6 +41,8 @@ Require Export Asm.
Local Open Scope option_monad_scope.
Notation regset := Asm.regset.
(** * Abstract syntax *)
(* First task: splitting the big [instruction] type below into CFI and basic instructions.
......
......@@ -1159,11 +1159,11 @@ Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
| _ => false
end.
Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode):=
Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
match il with
| nil => OK (k)
| nil => OK (nil)
| i1 :: il' =>
do k1 <- transl_basic_code f il' (it1_is_parent it1p i1) k;
do k1 <- transl_basic_code f il' (it1_is_parent it1p i1);
transl_instr_basic f i1 it1p k1
end.
......@@ -1196,12 +1196,29 @@ Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instructio
(* XXX: the simulation proof may be complex with this pattern. We may fix this later *)
Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks :=
match non_empty_bblockb bdy ex with
| true => {| header := ll; body:= bdy; exit := ex |} :: nil
| false => {| header := ll; body:= Pnop::nil; exit := None |} :: nil
match ex with
| None =>
match bdy with
| nil => {| header := ll; body:= Pnop::nil; exit := None |} :: nil
| _ => {| header := ll; body:= bdy; exit := None |} :: nil
end
| _ =>
match bdy with
| nil => {| header := ll; body:= nil; exit := ex |} :: nil
| _ => {| header := ll; body:= bdy; exit := ex |} :: nil
end
end.
Obligation 1.
rewrite <- Heq_anonymous. constructor.
Next Obligation.
induction bdy. congruence.
simpl. auto.
Qed.
Next Obligation.
destruct ex. simpl. auto.
congruence.
Qed.
Next Obligation.
induction bdy. congruence.
simpl. auto.
Qed.
Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res (bcode*control) :=
......@@ -1227,10 +1244,9 @@ Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) :
end.
Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
let stub := false in
do (bdy, ex) <- transl_exit f fb.(Machblock.exit);
do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy;
OK (cons_bblocks fb.(Machblock.header) bdy' ex)
do (bdy2, ex) <- transl_exit f fb.(Machblock.exit);
do bdy1 <- transl_basic_code f fb.(Machblock.body) ep;
OK (cons_bblocks fb.(Machblock.header) (bdy1 @@ bdy2) ex)
.
Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) :=
......
This diff is collapsed.
......@@ -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
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment