diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-05-24 15:06:18 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:58:30 +0200 |
commit | 0236781c3ff798b60c5c8171a0f9b6cd569f7995 (patch) | |
tree | 117e80f627ac331c066db3140a14040603118424 | |
parent | 265fdd4f703b0310fbcf5ad448c29dc34f7ff33a (diff) | |
download | compcert-kvx-0236781c3ff798b60c5c8171a0f9b6cd569f7995.tar.gz compcert-kvx-0236781c3ff798b60c5c8171a0f9b6cd569f7995.zip |
Machblock: Mach language with basic blocks
-rw-r--r-- | Makefile | 3 | ||||
-rw-r--r-- | driver/ForwardSimulationBlock.v | 236 | ||||
-rw-r--r-- | lib/Coqlib.v | 7 | ||||
-rw-r--r-- | mppa_k1c/Machblock.v | 354 | ||||
-rw-r--r-- | mppa_k1c/Machblockgen.v | 749 | ||||
-rw-r--r-- | mppa_k1c/Machblockgenproof.v | 638 |
6 files changed, 1986 insertions, 1 deletions
@@ -95,6 +95,7 @@ BACKEND=\ Debugvar.v Debugvarproof.v \ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ + Machblock.v Machblockgen.v Machblockgenproof.v \ Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v # C front-end modules (in cfrontend/) @@ -118,7 +119,7 @@ PARSER=Cabs.v Parser.v # Putting everything together (in driver/) -DRIVER=Compopts.v Compiler.v Complements.v +DRIVER=Compopts.v Compiler.v Complements.v ForwardSimulationBlock.v # All source files diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v new file mode 100644 index 00000000..43cf58c3 --- /dev/null +++ b/driver/ForwardSimulationBlock.v @@ -0,0 +1,236 @@ +(*** + +Variante de Forward Simulation pour les blocks. + +***) + +Require Import Relations. +Require Import Wellfounded. +Require Import Coqlib. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. + + +Local Open Scope nat_scope. + + +Section ForwardSimuBlock. + +Variable L1 L2: semantics. + +Local Hint Resolve starN_refl starN_step. + + +(* TODO: faut-il se baser sur [starN] ou un type inductif équivalent + (qui ferait les step dans l'ordre ci-dessous) ? + + => Voir ce qui est le plus facile pour prouver l'hypothèse [simu_end_block] ci-dessous... +*) + +Lemma starN_last_step n s t1 s': + starN (step L1) (globalenv L1) n s t1 s' -> + forall (t t2:trace) s'', + Step L1 s' t2 s'' -> t = t1 ** t2 -> starN (step L1) (globalenv L1) (S n) s t s''. +Proof. + induction 1; simpl. + + intros t t1 s0; autorewrite with trace_rewrite. + intros; subst; eapply starN_step; eauto. + autorewrite with trace_rewrite; auto. + + intros. eapply starN_step; eauto. + intros; subst; autorewrite with trace_rewrite; auto. +Qed. + +(** Hypothèses de la preuve *) + +Variable dist_end_block: state L1 -> nat. + +Hypothesis simu_mid_block: + forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). + +Hypothesis public_preserved: + forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. + +Variable build_block: state L1 -> state L2. + +Hypothesis match_initial_states: + forall s1, initial_state L1 s1 -> initial_state L2 (build_block s1). + +Hypothesis match_final_states: + forall s1 r, final_state L1 s1 r -> final_state L2 (build_block s1) r. + +Hypothesis final_states_end_block: + forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. + +Hypothesis simu_end_block: + forall s1 t s1', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> Step L2 (build_block s1) t (build_block s1'). + + +(** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) + +Definition star_in_block (head current: state L1): Prop := + dist_end_block head >= dist_end_block current + /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. + +Lemma star_in_block_step (head previous next: state L1): + forall t, star_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> star_in_block head next. +Proof. + intros t [H1 H2] H3 H4. + destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. + constructor 1. + + omega. + + cutrewrite (dist_end_block head - dist_end_block next = S (dist_end_block head - dist_end_block previous)). + - eapply starN_last_step; eauto. + - omega. +Qed. + +Lemma star_in_block_init (head current: state L1): + forall t, Step L1 head t current -> (dist_end_block head)<>0 -> star_in_block head current. +Proof. + intros t H3 H4. + destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. + constructor 1. + + omega. + + cutrewrite (dist_end_block head - dist_end_block current = 1). + - eapply starN_last_step; eauto. + - omega. +Qed. + + +Record memostate := { + real: state L1; + memorized: option (state L1); + memo_star: forall head, memorized = Some head -> star_in_block head real; + memo_final: forall r, final_state L1 real r -> memorized = None +}. + +Definition head (s: memostate): state L1 := + match memorized s with + | None => real s + | Some s' => s' + end. + +Lemma head_star (s: memostate): star_in_block (head s) (real s). +Proof. + destruct s as [rs ms Hs]. simpl. + destruct ms as [ms|]; unfold head; simpl; auto. + constructor 1. + omega. + cutrewrite ((dist_end_block rs - dist_end_block rs)%nat=O). + + apply starN_refl; auto. + + omega. +Qed. + +Inductive is_well_memorized (s s': memostate): Prop := + | StartBloc: + dist_end_block (real s) <> O -> + memorized s = None -> + memorized s' = Some (real s) -> + is_well_memorized s s' + | MidBloc: + dist_end_block (real s) <> O -> + memorized s <> None -> + memorized s' = memorized s -> + is_well_memorized s s' + | ExitBloc: + dist_end_block (real s) = O -> + memorized s' = None -> + is_well_memorized s s'. + +Local Hint Resolve StartBloc MidBloc ExitBloc. + +Definition memoL1 := {| + state := memostate; + genvtype := genvtype L1; + step := fun ge s t s' => + step L1 ge (real s) t (real s') + /\ is_well_memorized s s' ; + initial_state := fun s => initial_state L1 (real s) /\ memorized s = None; + final_state := fun s r => final_state L1 (real s) r; + globalenv:= globalenv L1; + symbolenv:= symbolenv L1 +|}. + + +(** Preuve des 2 forward simulations: L1 -> memoL1 et memoL1 -> L2 *) + +Lemma discr_dist_end s: + {dist_end_block s = O} + {dist_end_block s <> O}. +Proof. + destruct (dist_end_block s); simpl; intuition. +Qed. + +Lemma memo_simulation_step: + forall s1 t s1', Step L1 s1 t s1' -> + forall s2, s1 = (real s2) -> exists s2', Step memoL1 s2 t s2' /\ s1' = (real s2'). +Proof. + intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. simpl in H2; subst. + destruct (discr_dist_end rs2) as [H3 | H3]. + + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); simpl. + intuition. + + destruct ms2 as [s|]. + - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); simpl. + intuition. + - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); simpl. + intuition. + Unshelve. + * intros; discriminate. + * intros; auto. + * intros head X; injection X; clear X; intros; subst. + eapply star_in_block_step; eauto. + * intros r X; erewrite final_states_end_block in H3; intuition eauto. + * intros head X; injection X; clear X; intros; subst. + eapply star_in_block_init; eauto. + * intros r X; erewrite final_states_end_block in H3; intuition eauto. +Qed. + +Lemma forward_memo_simulation_1: forward_simulation L1 memoL1. +Proof. + apply forward_simulation_step with (match_states:=fun s1 s2 => s1 = (real s2)); auto. + + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); simpl. + intuition. + + intros; subst; auto. + + intros; exploit memo_simulation_step; eauto. + Unshelve. + * intros; discriminate. + * auto. +Qed. + +Lemma forward_memo_simulation_2: forward_simulation memoL1 L2. +Proof. + apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => s2 = (build_block (head s1))); auto. + + unfold memoL1; simpl. intros s1 [H0 H1]; eapply ex_intro with (x:=(build_block (real s1))). + unfold head. rewrite H1. intuition. + + intros s1 s2 r X H0. subst. unfold head. + erewrite memo_final; eauto. + eapply H0. + + unfold memoL1; simpl. + intros s1 t s1' [H1 H2] s H; subst. + destruct H2. + - (* StartBloc *) + constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H3 H4]; auto. + unfold head. rewrite H0. rewrite H2. rewrite H4. intuition. + - (* MidBloc *) + constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H3 H4]; auto. + unfold head. rewrite H2. rewrite H4. intuition. + destruct (memorized s1); simpl; auto. destruct H0; auto. + - (* EndBloc *) + constructor 1. + eapply ex_intro; intuition eauto. + apply simu_end_block. + destruct (head_star s1) as [H2 H3]. + cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3. + unfold head; rewrite H0; simpl. + eapply starN_last_step; eauto. + omega. +Qed. + +Lemma forward_simulation_block: forward_simulation L1 L2. +Proof. + eapply compose_forward_simulations. + eapply forward_memo_simulation_1. + apply forward_memo_simulation_2. +Qed. + + +End ForwardSimuBlock.
\ No newline at end of file diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 3fe1ea2e..86bfa248 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -90,6 +90,13 @@ Ltac exploit x := || refine (modusponens _ _ (x _ _) _) || refine (modusponens _ _ (x _) _). +Ltac totologize H := + match type of H with + | ( ?id = _ ) => + let Hassert := fresh "Htoto" in ( + assert (id = id) as Hassert; auto; rewrite H in Hassert at 2; simpl in Hassert; rewrite H in Hassert) + end. + (** * Definitions and theorems over the type [positive] *) Definition peq: forall (x y: positive), {x = y} + {x <> y} := Pos.eq_dec. diff --git a/mppa_k1c/Machblock.v b/mppa_k1c/Machblock.v new file mode 100644 index 00000000..9b36fc43 --- /dev/null +++ b/mppa_k1c/Machblock.v @@ -0,0 +1,354 @@ +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. +Require Import Op. +Require Import Locations. +Require Import Conventions. +Require Stacklayout. +Require Import Mach. +Require Import Linking. + +(** instructions "basiques" (ie non control-flow) *) +Inductive basic_inst: Type := + | MBgetstack: ptrofs -> typ -> mreg -> basic_inst + | MBsetstack: mreg -> ptrofs -> typ -> basic_inst + | MBgetparam: ptrofs -> typ -> mreg -> basic_inst + | MBop: operation -> list mreg -> mreg -> basic_inst + | MBload: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst + | MBstore: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst + . + +Definition bblock_body := list basic_inst. + +(** instructions de control flow *) +Inductive control_flow_inst: Type := + | MBcall: signature -> mreg + ident -> control_flow_inst + | MBtailcall: signature -> mreg + ident -> control_flow_inst + | MBbuiltin: external_function -> list (builtin_arg mreg) -> builtin_res mreg -> control_flow_inst + | MBgoto: label -> control_flow_inst + | MBcond: condition -> list mreg -> label -> control_flow_inst + | MBjumptable: mreg -> list label -> control_flow_inst + | MBreturn: control_flow_inst + . + +Record bblock := mk_bblock { + header: option label; + body: bblock_body; + exit: option control_flow_inst +}. + +Lemma bblock_eq: + forall b1 b2, + header b1 = header b2 -> + body b1 = body b2 -> + exit b1 = exit b2 -> + b1 = b2. +Proof. + intros. destruct b1. destruct b2. + simpl in *. subst. auto. +Qed. + +Definition length_opt {A} (o: option A) : nat := + match o with + | Some o => 1 + | None => 0 + end. + +Definition size (b:bblock): nat := (length_opt (header b))+(length (body b))+(length_opt (exit b)). + +Lemma size_null b: + size b = 0%nat -> + header b = None /\ body b = nil /\ exit b = None. +Proof. + destruct b as [h b e]. simpl. unfold size. simpl. + intros H. + assert (length_opt h = 0%nat) as Hh; [ omega |]. + assert (length b = 0%nat) as Hb; [ omega |]. + assert (length_opt e = 0%nat) as He; [ omega|]. + repeat split. + destruct h; try (simpl in Hh; discriminate); auto. + destruct b; try (simpl in Hb; discriminate); auto. + destruct e; try (simpl in He; discriminate); auto. +Qed. + +Definition code := list bblock. + +Record function: Type := mkfunction + { fn_sig: signature; + fn_code: code; + fn_stacksize: Z; + fn_link_ofs: ptrofs; + fn_retaddr_ofs: ptrofs }. + +Definition fundef := AST.fundef function. + +Definition program := AST.program fundef unit. + +Definition genv := Genv.t fundef unit. + +(*** sémantique ***) + +Definition is_label (lbl: label) (bb: bblock) : bool := + match header bb with + | Some lbl' => if peq lbl lbl' then true else false + | _ => false + end. + +Lemma is_label_correct: + forall lbl bb, + if is_label lbl bb then (header bb) = Some lbl else (header bb) <> Some lbl. +Proof. + intros. unfold is_label. destruct (header bb) as [lbl'|]; simpl; try discriminate. + case (peq lbl lbl'); intro; congruence. +Qed. + +Local Open Scope nat_scope. + +Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := + match c with + | nil => None + | bb1 :: bbl => if is_label lbl bb1 + then let bb' := {| header := None ; body := body bb1 ; exit := exit bb1 |} in ( + Some (match size bb' with + | O => bbl + | Datatypes.S _ => bb' :: bbl + end) + ) + else find_label lbl bbl + end. + +Section RELSEM. + +Variable rao:function -> code -> ptrofs -> Prop. +Variable ge:genv. + +Definition find_function_ptr + (ge: genv) (ros: mreg + ident) (rs: regset) : option block := + match ros with + | inl r => + match rs r with + | Vptr b ofs => if Ptrofs.eq ofs Ptrofs.zero then Some b else None + | _ => None + end + | inr symb => + Genv.find_symbol ge symb + end. + +(** Machblock execution states. *) + +Inductive stackframe: Type := + | Stackframe: + forall (f: block) (**r pointer to calling function *) + (sp: val) (**r stack pointer in calling function *) + (retaddr: val) (**r Asm return address in calling function *) + (c: code), (**r program point in calling function *) + stackframe. + +Inductive state: Type := + | State: + forall (stack: list stackframe) (**r call stack *) + (f: block) (**r pointer to current function *) + (sp: val) (**r stack pointer *) + (c: code) (**r current program point *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Callstate: + forall (stack: list stackframe) (**r call stack *) + (f: block) (**r pointer to function to call *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Returnstate: + forall (stack: list stackframe) (**r call stack *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state. + +Definition parent_sp (s: list stackframe) : val := + match s with + | nil => Vnullptr + | Stackframe f sp ra c :: s' => sp + end. + +Definition parent_ra (s: list stackframe) : val := + match s with + | nil => Vnullptr + | Stackframe f sp ra c :: s' => ra + end. + +Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m:mem): basic_inst -> regset -> mem -> Prop := + | exec_MBgetstack: + forall ofs ty dst v, + load_stack m sp ty ofs = Some v -> + basic_step s fb sp rs m (MBgetstack ofs ty dst) (rs#dst <- v) m + | exec_MBsetstack: + forall src ofs ty m' rs', + store_stack m sp ty ofs (rs src) = Some m' -> + rs' = undef_regs (destroyed_by_setstack ty) rs -> + basic_step s fb sp rs m (MBsetstack src ofs ty) rs' m' + | exec_MBgetparam: + forall ofs ty dst v rs' f, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m sp Tptr f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (parent_sp s) ty ofs = Some v -> + rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) -> + basic_step s fb sp rs m (MBgetparam ofs ty dst) rs' m + | exec_MBop: + forall op args v rs' res, + eval_operation ge sp op rs##args m = Some v -> + rs' = ((undef_regs (destroyed_by_op op) rs)#res <- v) -> + basic_step s fb sp rs m (MBop op args res) rs' m + | exec_MBload: + forall addr args a v rs' chunk dst, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) -> + basic_step s fb sp rs m (MBload chunk addr args dst) rs' m + | exec_MBstore: + forall chunk addr args src m' a rs', + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a (rs src) = Some m' -> + rs' = undef_regs (destroyed_by_store chunk addr) rs -> + basic_step s fb sp rs m (MBstore chunk addr args src) rs' m' + . + + +Inductive body_step (s: list stackframe) (f: block) (sp: val): bblock_body -> regset -> mem -> regset -> mem -> Prop := + | exec_nil_body: + forall rs m, + body_step s f sp nil rs m rs m + | exec_cons_body: + forall rs m bi p rs' m' rs'' m'', + basic_step s f sp rs m bi rs' m' -> + body_step s f sp p rs' m' rs'' m'' -> + body_step s f sp (bi::p) rs m rs'' m'' + . + +Inductive cfi_step: control_flow_inst -> state -> trace -> state -> Prop := + | exec_MBcall: + forall s fb sp sig ros c b rs m f f' ra, + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + rao f c ra -> + cfi_step (MBcall sig ros) (State s fb sp (b::c) rs m) + E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) + f' rs m) + | exec_MBtailcall: + forall s fb stk soff sig ros c rs m f f' m', + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + cfi_step (MBtailcall sig ros) (State s fb (Vptr stk soff) c rs m) + E0 (Callstate s f' rs m') + | exec_MBbuiltin: + forall s f sp rs m ef args res b c vargs t vres rs' m', + eval_builtin_args ge rs sp m args vargs -> + external_call ef ge vargs m t vres m' -> + rs' = set_res res vres (undef_regs (destroyed_by_builtin ef) rs) -> + cfi_step (MBbuiltin ef args res) (State s f sp (b :: c) rs m) + t (State s f sp c rs' m') + | exec_MBgoto: + forall s fb f sp lbl c rs m c', + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + cfi_step (MBgoto lbl) (State s fb sp c rs m) + E0 (State s fb sp c' rs m) + | exec_MBcond_true: + forall s fb f sp cond args lbl c rs m c' rs', + eval_condition cond rs##args m = Some true -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + rs' = undef_regs (destroyed_by_cond cond) rs -> + cfi_step (MBcond cond args lbl) (State s fb sp c rs m) + E0 (State s fb sp c' rs' m) + | exec_MBcond_false: + forall s f sp cond args lbl b c rs m rs', + eval_condition cond rs##args m = Some false -> + rs' = undef_regs (destroyed_by_cond cond) rs -> + cfi_step (MBcond cond args lbl) (State s f sp (b :: c) rs m) + E0 (State s f sp c rs' m) + | exec_MBjumptable: + forall s fb f sp arg tbl c rs m n lbl c' rs', + rs arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some lbl -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + rs' = undef_regs destroyed_by_jumptable rs -> + cfi_step (MBjumptable arg tbl) (State s fb sp c rs m) + E0 (State s fb sp c' rs' m) + | exec_MBreturn: + forall s fb stk soff c rs m f m', + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + cfi_step MBreturn (State s fb (Vptr stk soff) c rs m) + E0 (Returnstate s rs m') + . + +Inductive exit_step: option control_flow_inst -> state -> trace -> state -> Prop := + | exec_Some_exit: + forall ctl s t s', + cfi_step ctl s t s' -> + exit_step (Some ctl) s t s' + | exec_None_exit: + forall stk f sp b lb rs m, + exit_step None (State stk f sp (b::lb) rs m) E0 (State stk f sp lb rs m) + . + +Inductive step: state -> trace -> state -> Prop := + | exec_bblock: + forall sf f sp bb c rs m rs' m' t s', + body_step sf f sp (body bb) rs m rs' m' -> + exit_step (exit bb) (State sf f sp (bb::c) rs' m') t s' -> + step (State sf f sp (bb::c) rs m) t s' + | exec_function_internal: + forall s fb rs m f m1 m2 m3 stk rs', + Genv.find_funct_ptr ge fb = Some (Internal f) -> + Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> + let sp := Vptr stk Ptrofs.zero in + store_stack m1 sp Tptr f.(fn_link_ofs) (parent_sp s) = Some m2 -> + store_stack m2 sp Tptr f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> + rs' = undef_regs destroyed_at_function_entry rs -> + step (Callstate s fb rs m) + E0 (State s fb sp f.(fn_code) rs' m3) + | exec_function_external: + forall s fb rs m t rs' ef args res m', + Genv.find_funct_ptr ge fb = Some (External ef) -> + extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> + external_call ef ge args m t res m' -> + rs' = set_pair (loc_result (ef_sig ef)) res rs -> + step (Callstate s fb rs m) + t (Returnstate s rs' m') + | exec_return: + forall s f sp ra c rs m, + step (Returnstate (Stackframe f sp ra c :: s) rs m) + E0 (State s f sp c rs m) + . + +End RELSEM. + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall fb m0, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some fb -> + initial_state p (Callstate nil fb (Regmap.init Vundef) m0). + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall rs m r retcode, + loc_result signature_main = One r -> + rs r = Vint retcode -> + final_state (Returnstate nil rs m) retcode. + +Definition semantics (rao: function -> code -> ptrofs -> Prop) (p: program) := + Semantics (step rao) (initial_state p) final_state (Genv.globalenv p). diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v new file mode 100644 index 00000000..93284b0b --- /dev/null +++ b/mppa_k1c/Machblockgen.v @@ -0,0 +1,749 @@ +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. +Require Import Op. +Require Import Locations. +Require Import Conventions. +Require Stacklayout. +Require Import Mach. +Require Import Linking. +Require Import Machblock. + +Definition to_basic_inst(i: Mach.instruction): option basic_inst := + match i with + | Mgetstack ofs ty dst => Some (MBgetstack ofs ty dst) + | Msetstack src ofs ty => Some (MBsetstack src ofs ty) + | Mgetparam ofs ty dst => Some (MBgetparam ofs ty dst) + | Mop op args res => Some (MBop op args res) + | Mload chunk addr args dst => Some (MBload chunk addr args dst) + | Mstore chunk addr args src => Some (MBstore chunk addr args src) + | _ => None + end. + +(* version pas récursive terminale, mais plus facile pour la preuve *) +Fixpoint to_bblock_body(c: Mach.code): bblock_body * Mach.code := + match c with + | nil => (nil,nil) + | i::c' => + match to_basic_inst i with + | Some bi => + let (p,c'') := to_bblock_body c' in + (bi::p, c'') + | None => (nil, c) + end + end. + +Definition to_bblock_header (c: Mach.code): option label * Mach.code := + match c with + | (Mlabel l)::c' => (Some l, c') + | _ => (None, c) + end. + + +Definition to_cfi (i: Mach.instruction): option control_flow_inst := + match i with + | Mcall sig ros => Some (MBcall sig ros) + | Mtailcall sig ros => Some (MBtailcall sig ros) + | Mbuiltin ef args res => Some (MBbuiltin ef args res) + | Mgoto lbl => Some (MBgoto lbl) + | Mcond cond args lbl => Some (MBcond cond args lbl) + | Mjumptable arg tbl => Some (MBjumptable arg tbl) + | Mreturn => Some (MBreturn) + | _ => None + end. + +Definition to_bblock_exit (c: Mach.code): option control_flow_inst * Mach.code := + match c with + | nil => (None,nil) + | i::c' => + match to_cfi i with + | Some bi as o => (o, c') + | None => (None, c) + end + end. + +Inductive code_nature: Set := IsEmpty | IsLabel | IsBasicInst | IsCFI. + +Definition get_code_nature (c: Mach.code): code_nature := + match c with + | nil => IsEmpty + | (Mlabel _)::_ => IsLabel + | i::_ => match to_basic_inst i with + | Some _ => IsBasicInst + | None => IsCFI + end + end. + +Ltac Discriminate := + match goal with + | [ H: ?a <> ?a |- _ ] => contradict H; auto + | _ => discriminate + end. + + +Lemma cn_eqdec (cn1 cn2: code_nature): { cn1=cn2 } + {cn1 <> cn2}. +Proof. + decide equality. +Qed. + +Lemma get_code_nature_nil c: c<>nil -> get_code_nature c <> IsEmpty. +Proof. + intro. unfold get_code_nature. destruct c; try Discriminate. + destruct i; discriminate. +Qed. + +Lemma get_code_nature_nil_contra c: get_code_nature c = IsEmpty -> c = nil. +Proof. + intro. destruct c; auto. exploit (get_code_nature_nil (i::c)); discriminate || auto. + intro. contradict H0. +Qed. + +Lemma get_code_nature_basic_inst: + forall c a c0, + c = a :: c0 -> + get_code_nature c = IsBasicInst -> + to_basic_inst a <> None. +Proof. + intros. destruct a; discriminate || contradict H0; subst; simpl; discriminate. +Qed. + +Lemma to_bblock_header_not_IsLabel: + forall c b c0, + get_code_nature c <> IsLabel -> + to_bblock_header c = (b, c0) -> + c = c0 /\ b=None. +Proof. + intros. destruct c. + - simpl in H0; inversion H0; auto. + - destruct i; unfold to_bblock_header in H0; inversion H0; auto. + simpl in H; contradict H; auto. +Qed. + + +Lemma to_bblock_header_eq: + forall c b c0, + get_code_nature c <> IsLabel -> + to_bblock_header c = (b, c0) -> + c = c0. +Proof. + intros; exploit to_bblock_header_not_IsLabel; intuition eauto. +Qed. + +Lemma to_bblock_header_IsLabel: + forall c c0 b, + get_code_nature c = IsLabel -> + to_bblock_header c = (b, c0) -> + exists l, c = (Mlabel l)::c0. +Proof. + intros. destruct c; try discriminate. + destruct i; try discriminate. + unfold to_bblock_header in H0; inversion H0; eauto. +Qed. + +Lemma to_bblock_header_wf: + forall c b c0, + get_code_nature c = IsLabel -> + to_bblock_header c = (b, c0) -> + (length c > length c0)%nat. +Proof. + intros; exploit to_bblock_header_IsLabel; eauto. + intros [l H1]; subst; simpl; auto. +Qed. + +Ltac ExploitHeaderEq := + match goal with + | [ H: to_bblock_header (?i0 :: ?c) = (?b, ?c0) |- _ ] => + exploit (to_bblock_header_eq (i0::c) b c0); [subst; simpl; discriminate | auto | intro; subst; auto] + | _ => idtac + end. + +Lemma to_bblock_header_wfe: + forall c b c0, + to_bblock_header c = (b, c0) -> + (length c >= length c0)%nat. +Proof. + intros c b c0; destruct (cn_eqdec (get_code_nature c) IsLabel). + - intros; exploit to_bblock_header_wf; eauto; omega. + - intros; exploit to_bblock_header_eq; eauto. intros; subst; auto. +Qed. + +Lemma to_bblock_body_eq: + forall c b c0, + get_code_nature c <> IsBasicInst -> + to_bblock_body c = (b, c0) -> + c = c0. +Proof. + intros. destruct c. + - simpl in H0. inversion H0. auto. + - destruct i; simpl in *; try Discriminate || inversion H0; subst; auto. +Qed. + +Lemma to_bblock_body_wfe: + forall c b c0, + to_bblock_body c = (b, c0) -> + (length c >= length c0)%nat. +Proof. + induction c. + - intros. simpl in H. inversion H. subst. auto. + - intros. simpl in H. destruct (to_basic_inst a). + + remember (to_bblock_body c) as tbbc. destruct tbbc as [p c'']. + exploit (IHc p c''); auto. inversion H. subst. simpl. omega. + + inversion H; subst; auto. +Qed. + + +Inductive cons_to_bblock_body c0: Mach.code -> bblock_body -> Prop := + Cons_to_bbloc_body i bi c' b': + to_basic_inst i = Some bi + -> to_bblock_body c' = (b', c0) + -> cons_to_bblock_body c0 (i::c') (bi::b'). + +Lemma to_bblock_body_IsBasicInst: + forall c b c0, + get_code_nature c = IsBasicInst -> + to_bblock_body c = (b, c0) -> + cons_to_bblock_body c0 c b. +Proof. + intros. destruct c; [ contradict H; simpl; discriminate | ]. + remember (to_basic_inst i) as tbii. destruct tbii. + - simpl in H0. rewrite <- Heqtbii in H0. + remember (to_bblock_body c) as tbbc. destruct tbbc as [p1 c1]. + inversion H0. subst. eapply Cons_to_bbloc_body; eauto. + - destruct i; try discriminate. +Qed. + +Lemma to_bblock_body_wf: + forall c b c0, + get_code_nature c = IsBasicInst -> + to_bblock_body c = (b, c0) -> + (length c > length c0)%nat. +Proof. + intros; exploit to_bblock_body_IsBasicInst; eauto. + intros H1; destruct H1. + exploit to_bblock_body_wfe; eauto. + simpl; omega. +Qed. + +Lemma to_bblock_exit_eq: + forall c b c0, + get_code_nature c <> IsCFI -> + to_bblock_exit c = (b, c0) -> + c = c0. +Proof. + intros. destruct c. + - simpl in H0; inversion H0; auto. + - destruct i; unfold to_bblock_header in H0; inversion H0; auto; + simpl in H; contradict H; auto. +Qed. + +Lemma to_bblock_exit_wf: + forall c b c0, + get_code_nature c = IsCFI -> + to_bblock_exit c = (b, c0) -> + (length c > length c0)%nat. +Proof. + intros. destruct c; try discriminate. + destruct i; try discriminate; + unfold to_bblock_header in H0; inversion H0; auto. +Qed. + +Ltac ExploitExitEq := + match goal with + | [ H: to_bblock_exit (?i0 :: ?c) = (?b, ?c0) |- _ ] => + exploit (to_bblock_exit_eq (i0::c) b c0); [subst; simpl; discriminate | auto | intro; subst; auto] + | _ => idtac + end. + +Lemma to_bblock_exit_wfe: + forall c b c0, + to_bblock_exit c = (b, c0) -> + (length c >= length c0)%nat. +Proof. + intros. destruct c. unfold to_bblock_exit in H; inversion H; auto. + remember i as i0. + destruct i; try ExploitExitEq. + all: exploit (to_bblock_exit_wf (i0::c) b c0); [subst; simpl; auto | auto | try omega]. +Qed. + +Definition to_bblock(c: Mach.code): bblock * Mach.code := + let (h,c0) := to_bblock_header c in + let (bdy, c1) := to_bblock_body c0 in + let (ext, c2) := to_bblock_exit c1 in + ({| header := h; body := bdy; exit := ext |}, c2) + . + +Lemma to_bblock_double_label: + forall c l, + get_code_nature c = IsLabel -> + to_bblock (Mlabel l :: c) = ({| header := Some l; body := nil; exit := None |}, c). +Proof. + intros. + destruct c; try (contradict H; simpl; discriminate). + destruct i; try (contradict H; simpl; discriminate). + simpl. auto. +Qed. + +Lemma to_bblock_basic_inst_then_label: + forall i c bi, + get_code_nature (i::c) = IsBasicInst -> + get_code_nature c = IsLabel -> + to_basic_inst i = Some bi -> + fst (to_bblock (i::c)) = {| header := None; body := bi::nil; exit := None |}. +Proof. + intros. + destruct c; try (contradict H; simpl; discriminate). + destruct i0; try (contradict H; simpl; discriminate). + destruct i; simpl in *; inversion H1; subst; auto. +Qed. + +Lemma to_bblock_cf_inst_then_label: + forall i c cfi, + get_code_nature (i::c) = IsCFI -> + get_code_nature c = IsLabel -> + to_cfi i = Some cfi -> + fst (to_bblock (i::c)) = {| header := None; body := nil; exit := Some cfi |}. +Proof. + intros. + destruct c; try (contradict H; simpl; discriminate). + destruct i0; try (contradict H; simpl; discriminate). + destruct i; simpl in *; inversion H1; subst; auto. +Qed. + +Lemma to_bblock_single_label: + forall c l, + get_code_nature c <> IsLabel -> + fst (to_bblock (Mlabel l :: c)) = {| + header := Some l; + body := body (fst (to_bblock c)); + exit := exit (fst (to_bblock c)) + |}. +Proof. + intros. + destruct c; simpl; auto. + apply bblock_eq; simpl. +(* header *) + + destruct i; try ( + remember (to_bblock _) as bb; + unfold to_bblock in *; + remember (to_bblock_header _) as tbh; + destruct tbh; + destruct (to_bblock_body _); + destruct (to_bblock_exit _); + subst; simpl; inversion Heqtbh; auto; fail + ). +(* body *) + + remember i as i0; destruct i0; try ( + remember (to_bblock _) as bb; + unfold to_bblock in *; + remember (to_bblock_header _) as tbh; rewrite Heqi0; + remember (to_bblock_header (i :: _)) as tbh'; rewrite <- Heqi0 in *; + destruct tbh; destruct tbh'; + inversion Heqtbh; inversion Heqtbh'; subst; + destruct (to_bblock_body _); + destruct (to_bblock_exit _); auto; fail + ). contradict H; simpl; auto. +(* exit (same proof as body) *) + + remember i as i0; destruct i0; try ( + remember (to_bblock _) as bb; + unfold to_bblock in *; + remember (to_bblock_header _) as tbh; rewrite Heqi0; + remember (to_bblock_header (i :: _)) as tbh'; rewrite <- Heqi0 in *; + destruct tbh; destruct tbh'; + inversion Heqtbh; inversion Heqtbh'; subst; + destruct (to_bblock_body _); + destruct (to_bblock_exit _); auto; fail + ). contradict H; simpl; auto. +Qed. + +Lemma to_bblock_no_label: + forall c, + get_code_nature c <> IsLabel -> + fst (to_bblock c) = {| + header := None; + body := body (fst (to_bblock c)); + exit := exit (fst (to_bblock c)) + |}. +Proof. + intros. + destruct c; simpl; auto. + apply bblock_eq; simpl; + destruct i; ( + try ( + remember (to_bblock _) as bb; + unfold to_bblock in *; + remember (to_bblock_header _) as tbh; + destruct tbh; + destruct (to_bblock_body _); + destruct (to_bblock_exit _); + subst; simpl; inversion Heqtbh; auto; fail + ) + || contradict H; simpl; auto ). +Qed. + +Lemma to_bblock_body_nil c c': + to_bblock_body c = (nil, c') -> + c = c'. +Proof. + intros H. + destruct c; [ simpl in *; inversion H; auto |]. + destruct i; try ( simpl in *; remember (to_bblock_body c) as tbc; destruct tbc as [p c'']; inversion H ). + all: auto. +Qed. + +Lemma to_bblock_exit_nil c c': + to_bblock_exit c = (None, c') -> + c = c'. +Proof. + intros H. + destruct c; [ simpl in *; inversion H; auto |]. + destruct i; try ( simpl in *; remember (to_bblock_exit c) as tbe; destruct tbe as [p c'']; inversion H ). + all: auto. +Qed. + +Lemma to_bblock_label b l c c': + to_bblock (Mlabel l :: c) = (b, c') -> + exists bdy c1, to_bblock_body c = (bdy, c1) /\ + header b = Some l /\ body b = bdy /\ exit b = fst (to_bblock_exit c1). +Proof. + intros H. + (* destruct b as [bhd bbd bex]. simpl. *) + unfold to_bblock in H; simpl in H. + remember (to_bblock_body c) as tbbc; destruct tbbc as [bdy' c1']. + remember (to_bblock_exit c1') as tbbe; destruct tbbe as [ext c2]. + esplit; eauto. esplit; eauto. esplit; eauto. + inversion H; subst; clear H. simpl. + apply (f_equal fst) in Heqtbbe. simpl in Heqtbbe. auto. +Qed. + +Lemma to_bblock_label_then_nil b l c c': + to_bblock (Mlabel l :: c) = (b, c') -> + body b = nil -> + exit b = None -> + c = c'. +Proof. + intros TOB BB EB. + unfold to_bblock in TOB. + remember (to_bblock_header _) as tbh; destruct tbh as [h c0]. + remember (to_bblock_body _) as tbb; destruct tbb as [bdy c1]. + remember (to_bblock_exit _) as tbe; destruct tbe as [ext c2]. + inversion TOB; subst. simpl in *. clear TOB. + inversion Heqtbh; subst. clear Heqtbh. + exploit to_bblock_body_nil; eauto. intros; subst. clear Heqtbb. + exploit to_bblock_exit_nil; eauto. +Qed. + +Lemma to_bblock_basic_inst: + forall c i bi, + get_code_nature (i::c) = IsBasicInst -> + to_basic_inst i = Some bi -> + get_code_nature c <> IsLabel -> + fst (to_bblock (i::c)) = {| + header := None; + body := bi :: body (fst (to_bblock c)); + exit := exit (fst (to_bblock c)) + |}. +Proof. + intros. + destruct c; try (destruct i; inversion H0; subst; simpl; auto; fail). + apply bblock_eq; simpl. +(* header *) + + destruct i; simpl; auto; ( + exploit to_bblock_no_label; [rewrite H; discriminate | intro; rewrite H2; simpl; auto]). +(* body *) +(* FIXME - the proof takes some time to prove.. N² complexity :( *) + + destruct i; inversion H0; try ( + destruct i0; try ( + subst; unfold to_bblock; + remember (to_bblock_header _) as tbh; destruct tbh; + remember (to_bblock_header (_::c)) as tbh'; destruct tbh'; + inversion Heqtbh; inversion Heqtbh'; subst; + + remember (to_bblock_body _) as tbb; destruct tbb; + remember (to_bblock_body (_::c)) as tbb'; destruct tbb'; + inversion Heqtbb; inversion Heqtbb'; destruct (to_bblock_body c); + inversion H3; inversion H4; subst; + + remember (to_bblock_exit _) as tbc; destruct tbc; + simpl; auto ); + contradict H1; simpl; auto ). +(* exit - same as body *) + + destruct i; inversion H0; try ( + destruct i0; try ( + subst; unfold to_bblock; + remember (to_bblock_header _) as tbh; destruct tbh; + remember (to_bblock_header (_::c)) as tbh'; destruct tbh'; + inversion Heqtbh; inversion Heqtbh'; subst; + + remember (to_bblock_body _) as tbb; destruct tbb; + remember (to_bblock_body (_::c)) as tbb'; destruct tbb'; + inversion Heqtbb; inversion Heqtbb'; destruct (to_bblock_body c); + inversion H3; inversion H4; subst; + + remember (to_bblock_exit _) as tbc; destruct tbc; + simpl; auto ); + contradict H1; simpl; auto ). +Qed. + +Lemma to_bblock_size_single_label: + forall c i, + get_code_nature (i::c) = IsLabel -> + get_code_nature c <> IsLabel -> + size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))). +Proof. + intros. + destruct i; try (contradict H; simpl; discriminate). + destruct c; simpl; auto. + destruct i; try ( + exploit to_bblock_single_label; eauto; intro; rewrite H1; + exploit to_bblock_no_label; eauto; intro; rewrite H2; + simpl; auto; fail ). + Unshelve. all: auto. +Qed. + +Lemma to_bblock_size_label_neqz: + forall c, + get_code_nature c = IsLabel -> + size (fst (to_bblock c)) <> 0%nat. +Proof. + intros. destruct c; try (contradict H; auto; simpl; discriminate). + destruct i; try (contradict H; simpl; discriminate). + destruct (get_code_nature c) eqn:gcnc. + (* Case gcnc is not IsLabel *) + all: try (rewrite to_bblock_size_single_label; auto; rewrite gcnc; discriminate). + (* Case gcnc is IsLabel *) + rewrite to_bblock_double_label; auto; unfold size; simpl; auto. +Qed. + +Lemma to_bblock_size_basicinst_neqz: + forall c, + get_code_nature c = IsBasicInst -> + size (fst (to_bblock c)) <> 0%nat. +Proof. + intros. destruct c; try (contradict H; auto; simpl; discriminate). + destruct i; try (contradict H; simpl; discriminate); + ( + destruct (get_code_nature c) eqn:gcnc; + (* Case gcnc is not IsLabel *) + try (erewrite to_bblock_basic_inst; eauto; [ + unfold size; simpl; auto + | simpl; auto + | rewrite gcnc; discriminate + ]); + erewrite to_bblock_basic_inst_then_label; eauto; [ + unfold size; simpl; auto + | simpl; auto + ] + ). +Qed. + +Lemma to_bblock_size_cfi_neqz: + forall c, + get_code_nature c = IsCFI -> + size (fst (to_bblock c)) <> 0%nat. +Proof. + intros. destruct c; try (contradict H; auto; simpl; discriminate). + destruct i; discriminate. +Qed. + +Lemma to_bblock_size_single_basicinst: + forall c i, + get_code_nature (i::c) = IsBasicInst -> + get_code_nature c <> IsLabel -> + size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))). +Proof. + intros. + destruct i; try (contradict H; simpl; discriminate); try ( + (exploit to_bblock_basic_inst; eauto); + [remember (to_basic_inst _) as tbi; destruct tbi; eauto |]; + intro; rewrite H1; unfold size; simpl; + assert ((length_opt (header (fst (to_bblock c)))) = 0%nat); + exploit to_bblock_no_label; eauto; intro; rewrite H2; simpl; auto; + rewrite H2; auto + ). +Qed. + +Lemma to_bblock_wf c b c0: + c <> nil -> + to_bblock c = (b, c0) -> + (length c > length c0)%nat. +Proof. + intro H; lapply (get_code_nature_nil c); eauto. + intro H'; remember (get_code_nature c) as gcn. + unfold to_bblock. + remember (to_bblock_header c) as p1; eauto. + destruct p1 as [h c1]. + intro H0. + destruct gcn. + - contradict H'; auto. + - exploit to_bblock_header_wf; eauto. + remember (to_bblock_body c1) as p2; eauto. + destruct p2 as [h2 c2]. + exploit to_bblock_body_wfe; eauto. + remember (to_bblock_exit c2) as p3; eauto. + destruct p3 as [h3 c3]. + exploit to_bblock_exit_wfe; eauto. + inversion H0. omega. + - exploit to_bblock_header_eq; eauto. rewrite <- Heqgcn. discriminate. + intro; subst. + remember (to_bblock_body c1) as p2; eauto. + destruct p2 as [h2 c2]. + exploit to_bblock_body_wf; eauto. + remember (to_bblock_exit c2) as p3; eauto. + destruct p3 as [h3 c3]. + exploit to_bblock_exit_wfe; eauto. + inversion H0. omega. + - exploit to_bblock_header_eq; eauto. rewrite <- Heqgcn. discriminate. + intro; subst. + remember (to_bblock_body c1) as p2; eauto. + destruct p2 as [h2 c2]. + exploit (to_bblock_body_eq c1 h2 c2); eauto. rewrite <- Heqgcn. discriminate. + intro; subst. + remember (to_bblock_exit c2) as p3; eauto. + destruct p3 as [h3 c3]. + exploit (to_bblock_exit_wf c2 h3 c3); eauto. + inversion H0. omega. +Qed. + +Lemma to_bblock_nonil: + forall c i c0, + c = i :: c0 -> + size (fst (to_bblock c)) <> 0%nat. +Proof. + intros. remember (get_code_nature c) as gcnc. destruct gcnc. + - contradict Heqgcnc. subst. simpl. destruct i; discriminate. + - eapply to_bblock_size_label_neqz; auto. + - eapply to_bblock_size_basicinst_neqz; auto. + - eapply to_bblock_size_cfi_neqz; auto. +Qed. + +Lemma to_bblock_islabel: + forall c l, + is_label l (fst (to_bblock (Mlabel l :: c))) = true. +Proof. + intros. unfold to_bblock. + remember (to_bblock_header _) as tbh; destruct tbh as [h c0]. + remember (to_bblock_body _) as tbc; destruct tbc as [bdy c1]. + remember (to_bblock_exit _) as tbe; destruct tbe as [ext c2]. + simpl. inversion Heqtbh. unfold is_label. simpl. + apply peq_true. +Qed. + +Lemma body_fst_to_bblock_label: + forall l c, + body (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_body c). +Proof. + intros. destruct c as [|i c']; simpl; auto. + destruct i; simpl; auto. + all: ( + remember (to_bblock_body c') as tbbc; destruct tbbc as [tc c'']; simpl; + unfold to_bblock; + remember (to_bblock_header _) as tbh; destruct tbh as [h c0]; + remember (to_bblock_body c0) as tbc; destruct tbc as [bdy c1]; + remember (to_bblock_exit c1) as tbe; destruct tbe as [ext c2]; + simpl; simpl in Heqtbh; inversion Heqtbh; subst c0; + simpl in Heqtbc; remember (to_bblock_body c') as tbc'; destruct tbc' as [tc' osef]; + inversion Heqtbc; inversion Heqtbbc; auto + ). +Qed. + +Lemma exit_fst_to_bblock_label: + forall c c' l, + snd (to_bblock_body c) = c' -> + exit (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_exit c'). +Proof. + intros. destruct c as [|i c]; [simpl in *; subst; auto |]. + unfold to_bblock. + remember (to_bblock_header _) as tbh; destruct tbh as [h c0]. + remember (to_bblock_body c0) as tbc; destruct tbc as [bdy c1]. + remember (to_bblock_exit c1) as tbe; destruct tbe as [ext c2]. + simpl in *. inversion Heqtbh; subst. + destruct (to_basic_inst i) eqn:TBI. + - remember (to_bblock_body c) as tbbc; destruct tbbc as [p c'']. + simpl. simpl in Heqtbc. rewrite TBI in Heqtbc. rewrite <- Heqtbbc in Heqtbc. + inversion Heqtbc; subst. apply (f_equal fst) in Heqtbe; auto. + - simpl. simpl in Heqtbc. rewrite TBI in Heqtbc. + inversion Heqtbc; subst. clear Heqtbh Heqtbc. unfold to_bblock_exit in Heqtbe. + apply (f_equal fst) in Heqtbe; auto. +Qed. + +Function trans_code (c: Mach.code) { measure length c }: code := + match c with + | nil => nil + | _ => + let (b, c0) := to_bblock c in + b::(trans_code c0) + end. +Proof. + intros; eapply to_bblock_wf; eauto. discriminate. +Qed. + +(* +Functional Scheme trans_code_ind := Induction for trans_code Sort Prop. +*) + +Definition hd_code (bc: code) := (hd {| header := None; body := nil; exit := None |} bc). + +Lemma trans_code_nonil: + forall c, + c <> nil -> trans_code c <> nil. +Proof. + intros. + induction c, (trans_code c) using trans_code_ind; simpl; auto. discriminate. +Qed. + +Lemma trans_code_step: + forall c b lb0 hb c1 bb c2 eb c3, + trans_code c = b :: lb0 -> + to_bblock_header c = (hb, c1) -> + to_bblock_body c1 = (bb, c2) -> + to_bblock_exit c2 = (eb, c3) -> + hb = header b /\ bb = body b /\ eb = exit b /\ trans_code c3 = lb0. +Proof. + intros. + induction c, (trans_code c) using trans_code_ind. discriminate. clear IHc0. + subst. destruct _x as [|i c]; try (contradict y; auto; fail). + inversion H; subst. clear H. unfold to_bblock in e0. + remember (to_bblock_header (i::c)) as hd. destruct hd as [hb' c1']. + remember (to_bblock_body c1') as bd. destruct bd as [bb' c2']. + remember (to_bblock_exit c2') as be. destruct be as [eb' c3']. + inversion e0. simpl. + inversion H0. subst. + rewrite <- Heqbd in H1. inversion H1. subst. + rewrite <- Heqbe in H2. inversion H2. subst. + auto. +Qed. + +Lemma trans_code_cfi: + forall i c cfi, + to_cfi i = Some cfi -> + trans_code (i :: c) = {| header := None ; body := nil ; exit := Some cfi |} :: trans_code c. +Proof. + intros. rewrite trans_code_equation. remember (to_bblock _) as tb; destruct tb as [b c0]. + destruct i; try (contradict H; discriminate). + all: unfold to_bblock in Heqtb; remember (to_bblock_header _) as tbh; destruct tbh as [h c0']; + remember (to_bblock_body c0') as tbb; destruct tbb as [bdy c1']; + remember (to_bblock_exit c1') as tbe; destruct tbe as [ext c2]; simpl in *; + inversion Heqtbh; subst; inversion Heqtbb; subst; inversion Heqtbe; subst; + inversion Heqtb; subst; rewrite H; auto. +Qed. + +(* à finir pour passer des Mach.function au function, etc. *) +Definition trans_function (f: Mach.function) : function := + {| fn_sig:=Mach.fn_sig f; + fn_code:=trans_code (Mach.fn_code f); + fn_stacksize := Mach.fn_stacksize f; + fn_link_ofs := Mach.fn_link_ofs f; + fn_retaddr_ofs := Mach.fn_retaddr_ofs f + |}. + +Definition trans_fundef (f: Mach.fundef) : fundef := + transf_fundef trans_function f. + +Definition trans_prog (src: Mach.program) : program := + transform_program trans_fundef src. diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v new file mode 100644 index 00000000..838f7977 --- /dev/null +++ b/mppa_k1c/Machblockgenproof.v @@ -0,0 +1,638 @@ +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. +Require Import Op. +Require Import Locations. +Require Import Conventions. +Require Stacklayout. +Require Import Mach. +Require Import Linking. +Require Import Machblock. +Require Import Machblockgen. +Require Import ForwardSimulationBlock. + +(* FIXME: put this section somewhere else. + In "Smallstep" ? + +TODO: also move "starN_last_step" in the same section ? + +*) + +Section starN_lemma. +(* Auxiliary Lemma on starN *) + +Import Smallstep. +Local Open Scope nat_scope. + + +Variable L: semantics. + +Local Hint Resolve starN_refl starN_step Eapp_assoc. + +Lemma starN_split n s t s': + starN (step L) (globalenv L) n s t s' -> + forall m k, n=m+k -> + exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. +Proof. + induction 1; simpl. + + intros m k H; assert (X: m=0); try omega. + assert (X0: k=0); try omega. + subst; repeat (eapply ex_intro); intuition eauto. + + intros m; destruct m as [| m']; simpl. + - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. + - intros k H2. inversion H2. + exploit (IHstarN m' k); eauto. intro. + destruct H3 as (t5 & t6 & s0 & H5 & H6 & H7). + repeat (eapply ex_intro). + instantiate (1 := t6); instantiate (1 := t1 ** t5); instantiate (1 := s0). + intuition eauto. subst. auto. +Qed. + +End starN_lemma. + + +Definition inv_trans_rao (rao: function -> code -> ptrofs -> Prop) (f: Mach.function) (c: Mach.code) := + rao (trans_function f) (trans_code c). + +Definition match_prog (p: Mach.program) (tp: Machblock.program) := + match_program (fun _ f tf => tf = trans_fundef f) eq p tp. + +Lemma trans_program_match: forall p, match_prog p (trans_prog p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. + +Definition trans_stackframe (msf: Mach.stackframe) : stackframe := + match msf with + | Mach.Stackframe f sp retaddr c => Stackframe f sp retaddr (trans_code c) + end. + +Fixpoint trans_stack (mst: list Mach.stackframe) : list stackframe := + match mst with + | nil => nil + | msf :: mst0 => (trans_stackframe msf) :: (trans_stack mst0) + end. + +Definition trans_state (ms: Mach.state) : state := + match ms with + | Mach.State s f sp c rs m => State (trans_stack s) f sp (trans_code c) rs m + | Mach.Callstate s f rs m => Callstate (trans_stack s) f rs m + | Mach.Returnstate s rs m => Returnstate (trans_stack s) rs m + end. + +Section PRESERVATION. + +Variable prog: Mach.program. +Variable tprog: Machblock.program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +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 init_mem_preserved: + forall m, + Genv.init_mem prog = Some m -> + Genv.init_mem tprog = Some m. +Proof (Genv.init_mem_transf TRANSF). + +Lemma prog_main_preserved: + prog_main tprog = prog_main prog. +Proof (match_program_main 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 /\ trans_fundef f = tf. +Proof. + intros. + exploit (Genv.find_funct_ptr_match TRANSF); eauto. intro. + destruct H0 as (cunit & tf & A & B & C). + eapply ex_intro. intuition; eauto. subst. eapply A. +Qed. + +Lemma find_function_ptr_same: + forall s rs, + Mach.find_function_ptr ge s rs = find_function_ptr tge s rs. +Proof. + intros. unfold Mach.find_function_ptr. unfold find_function_ptr. + destruct s; auto. + rewrite symbols_preserved; auto. +Qed. + +Lemma find_funct_ptr_same: + forall f f0, + Genv.find_funct_ptr ge f = Some (Internal f0) -> + Genv.find_funct_ptr tge f = Some (Internal (trans_function f0)). +Proof. + intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto. +Qed. + +Lemma find_funct_ptr_same_external: + forall f f0, + Genv.find_funct_ptr ge f = Some (External f0) -> + Genv.find_funct_ptr tge f = Some (External f0). +Proof. + intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto. +Qed. + +Lemma parent_sp_preserved: + forall s, + Mach.parent_sp s = parent_sp (trans_stack s). +Proof. + unfold parent_sp. unfold Mach.parent_sp. destruct s; simpl; auto. + unfold trans_stackframe. destruct s; simpl; auto. +Qed. + +Lemma parent_ra_preserved: + forall s, + Mach.parent_ra s = parent_ra (trans_stack s). +Proof. + unfold parent_ra. unfold Mach.parent_ra. destruct s; simpl; auto. + unfold trans_stackframe. destruct s; simpl; auto. +Qed. + +Lemma external_call_preserved: + forall ef args m t res m', + external_call ef ge args m t res m' -> + external_call ef tge args m t res m'. +Proof. + intros. eapply external_call_symbols_preserved; eauto. + apply senv_preserved. +Qed. + +Lemma Mach_find_label_split l i c c': + Mach.find_label l (i :: c) = Some c' -> + (i=Mlabel l /\ c' = c) \/ (i <> Mlabel l /\ Mach.find_label l c = Some c'). +Proof. + intros H. + destruct i; try (constructor 2; split; auto; discriminate ). + destruct (peq l0 l) as [P|P]. + - constructor. subst l0; split; auto. + revert H. unfold Mach.find_label. simpl. rewrite peq_true. + intros H; injection H; auto. + - constructor 2. split. + + intro F. injection F. intros. contradict P; auto. + + revert H. unfold Mach.find_label. simpl. rewrite peq_false; auto. +Qed. + +Lemma find_label_stop l b c c0: + to_bblock (Mlabel l :: c) = (b, c0) -> find_label l (b :: trans_code c0) = Some (trans_code c). +Proof. + intros H. + unfold find_label. + assert (X: b=(fst (to_bblock (Mlabel l :: c)))). + { rewrite H; simpl; auto. } + subst b; rewrite to_bblock_islabel. + remember ({| header := None; body := _ ; exit := _ |}) as b'. + remember (fst (to_bblock _)) as b. + destruct (size b') eqn:SIZE. + - destruct (size_null b') as (Hh & Hb & He); auto. + subst b'; simpl in *. clear Hh SIZE. + erewrite <- (to_bblock_label_then_nil b l c c0); eauto. + - assert (X: exists b0 lb0, trans_code c = b0::lb0 /\ c <> nil). + { induction c, (trans_code c) using trans_code_ind. + + subst. simpl in * |-. inversion SIZE. + + (repeat econstructor 1). intro; subst; try tauto. + } + destruct X as (b0 & lb0 & X0 & X1). + unfold to_bblock in * |-. + remember (to_bblock_header _) as bh; destruct bh as [h c1]. + remember (to_bblock_body _) as bb; destruct bb as [bdy c2]. + remember (to_bblock_exit _) as be; destruct be as [ext c3]. + unfold size in SIZE; subst b b'; simpl in * |-. + injection H; clear H; intro; subst c3. + injection Heqbh; clear Heqbh; intros; subst. + cut (to_bblock_header c = (None, c)). + * intros X2; exploit trans_code_step; eauto. + simpl; rewrite X0; clear X0. + intros (Y1 & Y2 & Y3 & Y4). subst. + rewrite Y1; clear X1; destruct b0; simpl; auto. + * destruct (cn_eqdec (get_code_nature c) IsLabel) as [ Y | Y ]. + + destruct c; simpl; try discriminate. + destruct i; simpl; try discriminate. + simpl in * |-. + inversion Heqbb; subst. simpl in * |-. + inversion Heqbe; subst; simpl in * |-. + discriminate. + + destruct c; simpl; discriminate || auto. + destruct i; simpl; auto. + destruct Y. simpl; auto. +Qed. + +Lemma find_label_next l i b c c': + to_bblock (i :: c) = (b, c') -> i <> Mlabel l -> find_label l (b :: trans_code c') = find_label l (trans_code c'). +Proof. + intros H H1. + destruct b as [hd bd ex]. + destruct (cn_eqdec (get_code_nature (i::c)) IsLabel) as [ X | X ]. + - destruct i; try discriminate. + exploit to_bblock_label; eauto. + intros (bdy & c1 & Y1 & Y2 & Y3 & Y4). + simpl in *|-. subst. clear X. + simpl. unfold is_label; simpl. + assert (l0 <> l); [ intro; subst; contradict H1; auto |]. + rewrite peq_false; auto. + - exploit to_bblock_no_label; eauto. + intro Y. apply (f_equal fst) in H as Y1. simpl in Y1. rewrite Y in Y1. clear Y. + inversion Y1; subst; clear Y1. + simpl. auto. +Qed. + +Lemma to_bblock_header_split i c h c1: + to_bblock_header (i::c)=(h, c1) + -> (exists l, i=Mlabel l /\ h=Some l /\ c1=c) \/ (forall l, i<>Mlabel l /\ h=None /\ c1=(i::c)). +Proof. + destruct i; simpl; intros H; inversion H; try (constructor 2; intuition auto; discriminate). + constructor 1; eapply ex_intro; intuition eauto. +Qed. + +Lemma to_bblock_header_find_label i c1 l c h: + i <> Mlabel l + -> to_bblock_header (i :: c) = (h, c1) -> Mach.find_label l c = Mach.find_label l c1. +Proof. + intros H1 H2; exploit to_bblock_header_split; eauto. + intros [ ( l0 & X1 & X2 & X3 ) | X ]. + - subst. auto. + - destruct (X l) as (X1 & X2 & X3). subst. clear X X1. + symmetry. destruct i; try (simpl; auto). + assert (l0 <> l); [ intro; subst; contradict H1; auto |]. + rewrite peq_false; auto. +Qed. + +Lemma to_bblock_body_find_label c2 bdy l c1: + (bdy, c2) = to_bblock_body c1 -> + Mach.find_label l c1 = Mach.find_label l c2. +Proof. + generalize bdy c2. + induction c1 as [|i c1]. + - intros bdy0 c0 H. simpl in H. inversion H; subst; clear H. auto. + - intros bdy' c2' H. simpl in H. destruct i; try ( + simpl in H; remember (to_bblock_body c1) as tbb; destruct tbb as [p c'']; + inversion H; subst; clear H; simpl; erewrite IHc1; eauto; fail). +Qed. + +Lemma to_bblock_exit_find_label c2 ext l c1: + (ext, c2) = to_bblock_exit c1 + -> Mach.find_label l c1 = Mach.find_label l c2. +Proof. + intros H. destruct c1 as [|i c1]. + - simpl in H. inversion H; subst; clear H. auto. + - destruct i; try ( + simpl in H; inversion H; subst; clear H; auto; fail). +Qed. + +Lemma Mach_find_label_to_bblock i c l b c0: + i <> Mlabel l + -> to_bblock (i :: c) = (b, c0) + -> Mach.find_label l c = Mach.find_label l c0. +Proof. + intro H. + unfold to_bblock. + remember (to_bblock_header _) as bh; destruct bh as [h c1]. + remember (to_bblock_body _) as bb; destruct bb as [bdy c2]. + remember (to_bblock_exit _) as be; destruct be as [ext c3]. + intros X; injection X. clear X; intros; subst. + erewrite (to_bblock_header_find_label i c1); eauto. + erewrite (to_bblock_body_find_label c2); eauto. + erewrite to_bblock_exit_find_label; eauto. +Qed. + +Local Hint Resolve find_label_next. + +Lemma find_label_transcode_preserved: + forall l c c', + Mach.find_label l c = Some c' -> + find_label l (trans_code c) = Some (trans_code c'). +Proof. + intros l c; induction c, (trans_code c) using trans_code_ind. + - intros c' H; inversion H. + - intros c' H. subst _x. destruct c as [| i c]; try tauto. + exploit Mach_find_label_split; eauto. clear H. + intros [ [H1 H2] | [H1 H2] ]. + + subst. erewrite find_label_stop; eauto. + + rewrite <- IHc0. eauto. + erewrite <- (Mach_find_label_to_bblock i c); eauto. +Qed. + +Lemma find_label_preserved: + forall l f c, + Mach.find_label l (Mach.fn_code f) = Some c -> + find_label l (fn_code (trans_function f)) = Some (trans_code c). +Proof. + intros. cutrewrite ((fn_code (trans_function f)) = trans_code (Mach.fn_code f)); eauto. + apply find_label_transcode_preserved; auto. +Qed. + +Lemma mem_free_preserved: + forall m stk f, + Mem.free m stk 0 (Mach.fn_stacksize f) = Mem.free m stk 0 (fn_stacksize (trans_function f)). +Proof. + intros. auto. +Qed. + +Local Hint Resolve symbols_preserved senv_preserved init_mem_preserved prog_main_preserved functions_translated + parent_sp_preserved. + +Definition dist_end_block_code (c: Mach.code) := (size (fst (to_bblock c))-1)%nat. + + +Definition dist_end_block (s: Mach.state): nat := + match s with + | Mach.State _ _ _ c _ _ => dist_end_block_code c + | _ => 0 + end. + +Local Hint Resolve exec_nil_body exec_cons_body. +Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore. + +Variable rao: function -> code -> ptrofs -> Prop. + +(* +Lemma minus_diff_0 n: (n-1<>0)%nat -> (n >= 2)%nat. +Proof. + omega. +Qed. +*) + +Ltac ExploitDistEndBlockCode := + match goal with + | [ H : dist_end_block_code (Mlabel ?l :: ?c) <> 0%nat |- _ ] => + exploit (to_bblock_size_single_label c (Mlabel l)); eauto + | [ H : dist_end_block_code (?i0 :: ?c) <> 0%nat |- _ ] => + exploit (to_bblock_size_single_basicinst c i0); eauto + | _ => idtac + end. + +(* FIXME - refactoriser avec get_code_nature pour que ce soit plus joli *) +Lemma dist_end_block_code_simu_mid_block i c: + dist_end_block_code (i::c) <> 0%nat -> + (dist_end_block_code (i::c) = Datatypes.S (dist_end_block_code c))%nat. +Proof. + intros. + remember (get_code_nature c) as gcnc; destruct gcnc. + (* when c is nil *) + - contradict H. rewrite get_code_nature_nil_contra with (c := c); auto. destruct i; simpl; auto. + (* when c is IsLabel *) + - remember i as i0; remember (to_basic_inst i) as sbi; remember (to_cfi i) as scfi; + remember (get_code_nature (i::c)) as gcnic; + destruct i. + (* when i is a basic instruction *) + 1-6: try (( contradict H; unfold dist_end_block_code; exploit to_bblock_basic_inst_then_label; eauto; + [ totologize Heqgcnic; eapply Htoto + | totologize Heqsbi; try eapply Htoto + | intro; subst; rewrite H; simpl; auto + ] ); fail). + (* when i is a control flow instruction *) + 1-8: try (( contradict H; unfold dist_end_block_code; exploit to_bblock_cf_inst_then_label; eauto; + [ totologize Heqgcnic; eapply Htoto + | totologize Heqscfi; try eapply Htoto + | intro; subst; rewrite H; simpl; auto + ] ); fail). + (* when i is a label *) + contradict H. unfold dist_end_block_code. exploit to_bblock_double_label; eauto. + intro. subst. rewrite H. simpl. auto. + (* when c is IsBasicInst or IsCFI *) + - destruct i; try (contradict H; auto; fail); (* getting rid of the non basic inst *) + ( ExploitDistEndBlockCode; [ rewrite <- Heqgcnc; discriminate | + unfold dist_end_block_code in *; intro; rewrite H0 in *; omega ] ). + - destruct i; try (contradict H; auto; fail); (* getting rid of the non basic inst *) + ( ExploitDistEndBlockCode; [ rewrite <- Heqgcnc; discriminate | + unfold dist_end_block_code in *; intro; rewrite H0 in *; omega ] ). +Qed. + +Local Hint Resolve dist_end_block_code_simu_mid_block. + +Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) s f sp rs m (t:trace) (s':Mach.state): + to_basic_inst i = Some bi -> + Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' -> + exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'. +Proof. + destruct i; simpl in * |-; + (discriminate + || (intro H; inversion_clear H; intro X; inversion_clear X; eapply ex_intro; eapply ex_intro; intuition eauto)). + - eapply exec_MBgetparam; eauto. exploit (functions_translated); eauto. intro. + destruct H3 as (tf & A & B). subst. eapply A. + all: simpl; rewrite <- parent_sp_preserved; auto. + - eapply exec_MBop; eauto. rewrite <- H. destruct o; simpl; auto. destruct (rs ## l); simpl; auto. + unfold Genv.symbol_address; rewrite symbols_preserved; auto. + - eapply exec_MBload; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + unfold Genv.symbol_address; rewrite symbols_preserved; auto. + - eapply exec_MBstore; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + unfold Genv.symbol_address; rewrite symbols_preserved; auto. +Qed. + + +Lemma star_step_simu_body_step s f sp c: + forall (p:bblock_body) c' rs m t s', + to_bblock_body c = (p, c') -> + starN (Mach.step (inv_trans_rao rao)) ge (length p) (Mach.State s f sp c rs m) t s' -> + exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp p rs m rs' m'. +Proof. + induction c as [ | i0 c0 Hc0]; simpl; intros p c' rs m t s' H. + * (* nil *) + inversion_clear H; simpl; intros X; inversion_clear X. + eapply ex_intro; eapply ex_intro; intuition eauto. + * (* cons *) + remember (to_basic_inst i0) as o eqn:Ho. + destruct o as [bi |]. + + (* to_basic_inst i0 = Some bi *) + remember (to_bblock_body c0) as r eqn:Hr. + destruct r as [p1 c1]; inversion H; simpl; subst; clear H. + intros X; inversion_clear X. + exploit step_simu_basic_step; eauto. + intros [rs' [m' [H2 [H3 H4]]]]; subst. + exploit Hc0; eauto. + intros [rs'' [m'' [H5 [H6 H7]]]]; subst. + refine (ex_intro _ rs'' (ex_intro _ m'' _)); intuition eauto. + + (* to_basic_inst i0 = None *) + inversion_clear H; simpl. + intros X; inversion_clear X. intuition eauto. +Qed. + +Lemma step_simu_cfi_step: + forall c e c' stk f sp rs m t s' b lb', + to_bblock_exit c = (Some e, c') -> + trans_code c' = lb' -> + Mach.step (inv_trans_rao rao) ge (Mach.State stk f sp c rs m) t s' -> + cfi_step rao tge e (State (trans_stack stk) f sp (b::lb') rs m) t (trans_state s'). +Proof. + intros c e c' stk f sp rs m t s' b lb'. + intros Hexit Htc Hstep. + destruct c as [|ei c]; try (contradict Hexit; discriminate). + destruct ei; (contradict Hexit; discriminate) || ( + inversion Hexit; subst; inversion Hstep; subst; simpl + ). + * unfold inv_trans_rao in H11. + apply exec_MBcall with (f := (trans_function f0)); auto. + rewrite find_function_ptr_same in H9; auto. + apply find_funct_ptr_same. auto. + * apply exec_MBtailcall with (f := (trans_function f0)); auto. + rewrite find_function_ptr_same in H9; auto. + apply find_funct_ptr_same; auto. + rewrite parent_sp_preserved in H11; subst; auto. + rewrite parent_ra_preserved in H12; subst; auto. + * eapply exec_MBbuiltin; eauto. + eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. + * eapply exec_MBgoto; eauto. + apply find_funct_ptr_same; eauto. + apply find_label_preserved; auto. + * eapply exec_MBcond_true; eauto. + erewrite find_funct_ptr_same; eauto. + apply find_label_preserved; auto. + * eapply exec_MBcond_false; eauto. + * eapply exec_MBjumptable; eauto. + erewrite find_funct_ptr_same; eauto. + apply find_label_preserved; auto. + * eapply exec_MBreturn; eauto. + apply find_funct_ptr_same; eauto. + rewrite parent_sp_preserved in H8; subst; auto. + rewrite parent_ra_preserved in H9; subst; auto. + rewrite mem_free_preserved in H10; subst; auto. +Qed. + +Lemma simu_end_block: + forall s1 t s1', + starN (Mach.step (inv_trans_rao rao)) ge (Datatypes.S (dist_end_block s1)) s1 t s1' -> + step rao tge (trans_state s1) t (trans_state s1'). +Proof. + destruct s1; simpl. + + (* State *) + (* c cannot be nil *) + destruct c as [|i c]; simpl; try ( (* nil => absurd *) + unfold dist_end_block_code; simpl; + intros t s1' H; inversion_clear H; + inversion_clear H0; fail + ). + + intros t s1' H. + remember (_::_) as c0. remember (trans_code c0) as tc0. + + (* tc0 cannot be nil *) + destruct tc0; try + ( exploit (trans_code_nonil c0); subst; auto; try discriminate; intro H0; contradict H0 ). + + assert (X: Datatypes.S (dist_end_block_code c0) = (size (fst (to_bblock c0)))). + { + unfold dist_end_block_code. remember (size _) as siz. + assert (siz <> 0%nat). rewrite Heqsiz; apply to_bblock_nonil with (c0 := c) (i := i) (c := c0); auto. + omega. + } + + (* decomposition of starN in 3 parts: header + body + exit *) + rewrite X in H; unfold size in H. + destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H _ _ refl_equal) as [t3 [t4 [s1 [H0 [H3 H4]]]]]. + subst t; clear X H. + destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H0 _ _ refl_equal) as [t1 [t2 [s0 [H [H1 H2]]]]]. + subst t3; clear H0. + + (* Making the hypothesis more readable *) + remember (Smallstep.step _) as Machstep. remember (globalenv _) as mge. + remember (Mach.State _ _ _ _ _ _) as si. + + unfold to_bblock in * |- *. + (* naming parts of block "b" *) + remember (to_bblock_header c0) as hd. destruct hd as [hb c1]. + remember (to_bblock_body c1) as bb. destruct bb as [bb c2]. + remember (to_bblock_exit c2) as exb. destruct exb as [exb c3]. + simpl in * |- *. + + exploit trans_code_step; eauto. intro EQ. destruct EQ as (EQH & EQB & EQE & EQTB0). + subst hb bb exb. + + (* header opt step *) + assert (X: s0 = (Mach.State stack f sp c1 rs m) /\ t1 = E0). + { + destruct (header b) eqn:EQHB. + - inversion_clear H. inversion H2. subst. + destruct i; try (contradict EQHB; inversion Heqhd; fail). + inversion H0. subst. inversion Heqhd. auto. + - simpl in H. inversion H. subst. + destruct i; try (inversion Heqhd; auto; fail). + } + clear H; destruct X as [X1 X2]; subst s0 t1. + autorewrite with trace_rewrite. + + (* body steps *) + subst mge Machstep. + exploit (star_step_simu_body_step); eauto. + clear H1; intros [rs' [m' [H0 [H1 H2]]]]. + subst s1 t2. autorewrite with trace_rewrite. + (* preparing exit step *) + eapply exec_bblock; eauto. + clear H2. + + (* exit step *) + destruct (exit b) as [e|] eqn:EQEB. + - constructor. + simpl in H3. inversion H3. subst. clear H3. + inversion H1. subst. clear H1. + destruct c2 as [|ei c2']; try (contradict Heqexb; discriminate). + rewrite E0_right. + destruct ei; try (contradict Heqexb; discriminate). + all: eapply step_simu_cfi_step; eauto. + - simpl in H3. inversion H3; subst. simpl. + destruct c2 as [|ei c2']; inversion Heqexb; subst; try eapply exec_None_exit. + clear H3. destruct (to_cfi ei) as [cfi|] eqn:TOCFI; inversion H0. + subst. eapply exec_None_exit. + + + (* Callstate *) + intros t s1' H; inversion_clear H. + inversion H1; subst; clear H1. + inversion_clear H0; simpl. + - (* function_internal*) + cutrewrite (trans_code (Mach.fn_code f0) = fn_code (trans_function f0)); eauto. + eapply exec_function_internal; eauto. + apply find_funct_ptr_same; auto. + rewrite <- parent_sp_preserved; eauto. + rewrite <- parent_ra_preserved; eauto. + - (* function_external *) + autorewrite with trace_rewrite. + eapply exec_function_external; eauto. + apply find_funct_ptr_same_external; auto. + rewrite <- parent_sp_preserved; eauto. + apply external_call_preserved; auto. + + (* Returnstate *) + intros t s1' H; inversion_clear H. + inversion H1; subst; clear H1. + inversion_clear H0; simpl. + eapply exec_return. +Qed. + +Theorem simulation: forward_simulation (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog). +Proof. + apply forward_simulation_block with (dist_end_block := dist_end_block) (build_block := trans_state). +(* simu_mid_block *) + - intros s1 t s1' H1. + destruct H1; simpl; omega || (intuition auto). +(* public_preserved *) + - apply senv_preserved. +(* match_initial_states *) + - intros. simpl. destruct H. split. + apply init_mem_preserved; auto. + rewrite prog_main_preserved. rewrite <- H0. apply symbols_preserved. +(* match_final_states *) + - intros. simpl. destruct H. split with (r := r); auto. +(* final_states_end_block *) + - intros. simpl in H0. inversion H0. + inversion H; simpl; auto. + (* the remaining instructions cannot lead to a Returnstate *) + all: subst; discriminate. +(* simu_end_block *) + - apply simu_end_block. +Qed. + +End PRESERVATION. |