diff options
Diffstat (limited to 'scheduling/RTLpath.v')
| -rw-r--r-- | scheduling/RTLpath.v | 1067 |
1 files changed, 1067 insertions, 0 deletions
diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v new file mode 100644 index 00000000..35512652 --- /dev/null +++ b/scheduling/RTLpath.v @@ -0,0 +1,1067 @@ +(** We introduce a data-structure extending the RTL CFG into a control-flow graph over "traces" (in the sense of "trace-scheduling") + Here, we use the word "path" instead of "trace" because "trace" has already a meaning in CompCert: + a "path" is simply a list of successive nodes in the CFG (modulo some additional wellformness conditions). + + Actually, we extend syntactically the notion of RTL programs with a structure of "path_map": + this gives an alternative view of the CFG -- where "nodes" are paths instead of simple instructions. + Our wellformness condition on paths express that: + - the CFG on paths is wellformed: any successor of a given path points to another path (possibly the same). + - execution of a paths only emit single events. + + We represent each path only by a natural: the number of nodes in the path. These nodes are recovered from a static notion of "default successor". + This notion of path is thus incomplete. For example, if a path contains a whole loop (and for example, unrools it several times), + then this loop must be a suffix of the path. + + However: it is sufficient in order to represent superblocks (each superblock being represented as a path). + A superblock decomposition of the CFG exactly corresponds to the case where each node is in at most one path. + + Our goal is to provide two bisimulable semantics: + - one is simply the RTL semantics + - the other is based on a notion of "path-step": each path is executed in a single step. + + Remark that all analyses on RTL programs should thus be appliable for "free" also for RTLpath programs ! +*) + +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL Linking. + +Declare Scope option_monad_scope. + +Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end) + (at level 200, X ident, A at level 100, B at level 200) + : option_monad_scope. + +Notation "'ASSERT' A 'IN' B" := (if A then B else None) + (at level 200, A at level 100, B at level 200) + : option_monad_scope. + +Local Open Scope option_monad_scope. + +(** * Syntax of RTLpath programs *) + +(** Internal instruction = instruction with a default successor in a path. *) + +Definition default_succ (i: instruction): option node := + match i with + | Inop s => Some s + | Iop op args res s => Some s + | Iload _ chunk addr args dst s => Some s + | Istore chunk addr args src s => Some s + | Icond cond args ifso ifnot _ => Some ifnot + | _ => None (* TODO: we could choose a successor for jumptable ? *) + end. + +Definition early_exit (i: instruction): option node := (* FIXME: for jumptable, replace [node] by [list node] *) + match i with + | Icond cond args ifso ifnot _ => Some ifso + | _ => None + end. + +(** Our notion of path. + + We do not formally require that the set of path is a partition of the CFG. + path may have intersections ! + + Moreover, we do not formally require that path have a single entry-point (a superblock structure) + + But, in practice, these properties are probably necessary in order to ensure the success of dynamic verification of scheduling. + + Here: we only require that each exit-point of a path is the entry-point of a path + (and that internal node of a path are internal instructions) +*) + + +(* By convention, we say that node [n] is the entry-point of a path if it is a key of the path_map. + + Such a path of entry [n] is defined from a natural [path] representing the [path] default-successors of [n]. + + Remark: a path can loop several times in the CFG. + +*) + +Record path_info := { + psize: nat; (* number minus 1 of instructions in the path *) + input_regs: Regset.t; + (** Registers that are used (as input_regs) by the "fallthrough successors" of the path *) + (** This field is not used by the verificator, but is helpful for the superblock scheduler *) + output_regs: Regset.t +}. + +Definition path_map: Type := PTree.t path_info. + +Definition path_entry (*c:code*) (pm: path_map) (n: node): Prop + := pm!n <> None (*/\ c!n <> None*). + +Inductive wellformed_path (c:code) (pm: path_map): nat -> node -> Prop := + | wf_last_node i pc: + c!pc = Some i -> + (forall n, List.In n (successors_instr i) -> path_entry (*c*) pm n) -> + wellformed_path c pm 0 pc + | wf_internal_node path i pc pc': + c!pc = Some i -> + default_succ i = Some pc' -> + (forall n, early_exit i = Some n -> path_entry (*c*) pm n) -> + wellformed_path c pm path pc' -> + wellformed_path c pm (S path) pc. + +(* all paths defined from the path_map are wellformed *) +Definition wellformed_path_map (c:code) (pm: path_map): Prop := + forall n path, pm!n = Some path -> wellformed_path c pm path.(psize) n. + +(** We "extend" the notion of RTL program with the additional structure for path. + + There is thus a trivial "forgetful functor" from RTLpath programs to RTL ones. +*) + +Record function : Type := + { fn_RTL:> RTL.function; + fn_path: path_map; + (* condition 1 below: the entry-point of the code is an entry-point of a path *) + fn_entry_point_wf: path_entry (*fn_RTL.(fn_code)*) fn_path fn_RTL.(fn_entrypoint); + (* condition 2 below: the path_map is well-formed *) + fn_path_wf: wellformed_path_map fn_RTL.(fn_code) fn_path + }. + +Definition fundef := AST.fundef function. +Definition program := AST.program fundef unit. +Definition genv := Genv.t fundef unit. + +Definition fundef_RTL (fu: fundef) : RTL.fundef := + match fu with + | Internal f => Internal f.(fn_RTL) + | External ef => External ef + end. +Coercion fundef_RTL: fundef >-> RTL.fundef. + +Definition transf_program (p: program) : RTL.program := transform_program fundef_RTL p. +Coercion transf_program: program >-> RTL.program. + +(** * Path-step semantics of RTLpath programs *) + +(* Semantics of internal instructions (mimicking RTL semantics) *) + +Record istate := mk_istate { icontinue: bool; ipc: node; irs: regset; imem: mem }. + +(* FIXME - prediction *) +(* Internal step through the path *) +Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem): option istate := + match i with + | Inop pc' => Some (mk_istate true pc' rs m) + | Iop op args res pc' => + SOME v <- eval_operation ge sp op rs##args m IN + Some (mk_istate true pc' (rs#res <- v) m) + | Iload TRAP chunk addr args dst pc' => + SOME a <- eval_addressing ge sp addr rs##args IN + SOME v <- Mem.loadv chunk m a IN + Some (mk_istate true pc' (rs#dst <- v) m) + | Iload NOTRAP chunk addr args dst pc' => + let default_state := mk_istate true pc' rs#dst <- (default_notrap_load_value chunk) m in + match (eval_addressing ge sp addr rs##args) with + | None => Some default_state + | Some a => match (Mem.loadv chunk m a) with + | None => Some default_state + | Some v => Some (mk_istate true pc' (rs#dst <- v) m) + end + end + | Istore chunk addr args src pc' => + SOME a <- eval_addressing ge sp addr rs##args IN + SOME m' <- Mem.storev chunk m a rs#src IN + Some (mk_istate true pc' rs m') + | Icond cond args ifso ifnot _ => + SOME b <- eval_condition cond rs##args m IN + Some (mk_istate (negb b) (if b then ifso else ifnot) rs m) + | _ => None (* TODO jumptable ? *) + end. + +(** Execution of a path in a single step *) + +(* Executes until a state [st] is reached where st.(continue) is false *) +Fixpoint isteps ge (path:nat) (f: function) sp rs m pc: option istate := + match path with + | O => Some (mk_istate true pc rs m) + | S p => + SOME i <- (fn_code f)!pc IN + SOME st <- istep ge i sp rs m IN + if (icontinue st) then + isteps ge p f sp (irs st) (imem st) (ipc st) + else + Some st + end. + +Definition find_function (pge: genv) (ros: reg + ident) (rs: regset) : option fundef := + match ros with + | inl r => Genv.find_funct pge rs#r + | inr symb => + match Genv.find_symbol pge symb with + | None => None + | Some b => Genv.find_funct_ptr pge b + end + end. + +Inductive stackframe : Type := + | Stackframe + (res: reg) (**r where to store the result *) + (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (pc: node) (**r program point in calling function *) + (rs: regset) (**r register state in calling function *) + . + +Definition stf_RTL (st: stackframe): RTL.stackframe := + match st with + | Stackframe res f sp pc rs => RTL.Stackframe res f sp pc rs + end. + +Fixpoint stack_RTL (stack: list stackframe): list RTL.stackframe := + match stack with + | nil => nil + | cons stf stack' => cons (stf_RTL stf) (stack_RTL stack') + end. + +Inductive state : Type := + | State + (stack: list stackframe) (**r call stack *) + (f: function) (**r current function *) + (sp: val) (**r stack pointer *) + (pc: node) (**r current program point in [c] *) + (rs: regset) (**r register state *) + (m: mem) (**r memory state *) + | Callstate + (stack: list stackframe) (**r call stack *) + (f: fundef) (**r function to call *) + (args: list val) (**r arguments to the call *) + (m: mem) (**r memory state *) + | Returnstate + (stack: list stackframe) (**r call stack *) + (v: val) (**r return value for the call *) + (m: mem) (**r memory state *) + . + +Definition state_RTL (s: state): RTL.state := + match s with + | State stack f sp pc rs m => RTL.State (stack_RTL stack) f sp pc rs m + | Callstate stack f args m => RTL.Callstate (stack_RTL stack) f args m + | Returnstate stack v m => RTL.Returnstate (stack_RTL stack) v m + end. +Coercion state_RTL: state >-> RTL.state. + +(* Used to execute the last instruction of a path (isteps is only in charge of executing the instructions before the last) *) +Inductive path_last_step ge pge stack (f: function): val -> node -> regset -> mem -> trace -> state -> Prop := + | exec_istate i sp pc rs m st: + (fn_code f)!pc = Some i -> + istep ge i sp rs m = Some st -> + path_last_step ge pge stack f sp pc rs m + E0 (State stack f sp (ipc st) (irs st) (imem st)) + | exec_Icall sp pc rs m sig ros args res pc' fd: + (fn_code f)!pc = Some(Icall sig ros args res pc') -> + find_function pge ros rs = Some fd -> + funsig fd = sig -> + path_last_step ge pge stack f sp pc rs m + E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m) + | exec_Itailcall stk pc rs m sig ros args fd m': + (fn_code f)!pc = Some(Itailcall sig ros args) -> + find_function pge ros rs = Some fd -> + funsig fd = sig -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + path_last_step ge pge stack f (Vptr stk Ptrofs.zero) pc rs m + E0 (Callstate stack fd rs##args m') + | exec_Ibuiltin sp pc rs m ef args res pc' vargs t vres m': + (fn_code f)!pc = Some(Ibuiltin ef args res pc') -> + eval_builtin_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + path_last_step ge pge stack f sp pc rs m + t (State stack f sp pc' (regmap_setres res vres rs) m') + | exec_Ijumptable sp pc rs m arg tbl n pc': (* TODO remove jumptable from here ? *) + (fn_code f)!pc = Some(Ijumptable arg tbl) -> + rs#arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some pc' -> + path_last_step ge pge stack f sp pc rs m + E0 (State stack f sp pc' rs m) + | exec_Ireturn stk pc rs m or m': + (fn_code f)!pc = Some(Ireturn or) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + path_last_step ge pge stack f (Vptr stk Ptrofs.zero) pc rs m + E0 (Returnstate stack (regmap_optget or Vundef rs) m'). + +(* Executes an entire path *) +Inductive path_step ge pge (path:nat) stack f sp rs m pc: trace -> state -> Prop := + | exec_early_exit st: + isteps ge path f sp rs m pc = Some st -> + (icontinue st) = false -> + path_step ge pge path stack f sp rs m pc E0 (State stack f sp (ipc st) (irs st) (imem st)) + | exec_normal_exit st t s: + isteps ge path f sp rs m pc = Some st -> + (icontinue st) = true -> + path_last_step ge pge stack f sp (ipc st) (irs st) (imem st) t s -> + path_step ge pge path stack f sp rs m pc t s. + +(* Either internal path execution, or the usual exec_function / exec_return borrowed from RTL *) +Inductive step ge pge: state -> trace -> state -> Prop := + | exec_path path stack f sp rs m pc t s: + (fn_path f)!pc = Some path -> + path_step ge pge path.(psize) stack f sp rs m pc t s -> + step ge pge (State stack f sp pc rs m) t s + | exec_function_internal s f args m m' stk: + Mem.alloc m 0 (fn_RTL f).(fn_stacksize) = (m', stk) -> + step ge pge (Callstate s (Internal f) args m) + E0 (State s + f + (Vptr stk Ptrofs.zero) + f.(fn_entrypoint) + (init_regs args f.(fn_params)) + m') + | exec_function_external s ef args res t m m': + external_call ef ge args m t res m' -> + step ge pge (Callstate s (External ef) args m) + t (Returnstate s res m') + | exec_return res f sp pc rs s vres m: + step ge pge (Returnstate (Stackframe res f sp pc rs :: s) vres m) + E0 (State s f sp pc (rs#res <- vres) m). + +Inductive initial_state (p:program) : state -> Prop := + initial_state_intro (b : block) (f : fundef) (m0 : mem): + Genv.init_mem p = Some m0 -> + Genv.find_symbol (Genv.globalenv p) (prog_main p) = Some b -> + Genv.find_funct_ptr (Genv.globalenv p) b = Some f -> + funsig f = signature_main -> initial_state p (Callstate nil f nil m0). + +Definition final_state (st: state) (i:int): Prop + := RTL.final_state st i. + +Definition semantics (p: program) := + Semantics (step (Genv.globalenv (transf_program p))) (initial_state p) final_state (Genv.globalenv p). + +(** * Proving the bisimulation between (semantics p) and (RTL.semantics p). *) + +(** ** Preliminaries: simple tactics for option-monad *) + +Lemma destruct_SOME A B (P: option B -> Prop) (e: option A) (f: A -> option B): + (forall x, e = Some x -> P (f x)) -> (e = None -> P None) -> (P (SOME x <- e IN f x)). +Proof. + intros; destruct e; simpl; auto. +Qed. + +Lemma destruct_ASSERT B (P: option B -> Prop) (e: bool) (x: option B): + (e = true -> P x) -> (e = false -> P None) -> (P (ASSERT e IN x)). +Proof. + intros; destruct e; simpl; auto. +Qed. + +Ltac inversion_SOME x := + try (eapply destruct_SOME; [ let x := fresh x in intro x | simpl; try congruence ]). + +Ltac inversion_ASSERT := + try (eapply destruct_ASSERT; [ idtac | simpl; try congruence ]). + +Ltac simplify_someHyp := + match goal with + | H: None = Some _ |- _ => inversion H; clear H; subst + | H: Some _ = None |- _ => inversion H; clear H; subst + | H: ?t = ?t |- _ => clear H + | H: Some _ = Some _ |- _ => inversion H; clear H; subst + | H: Some _ <> None |- _ => clear H + | H: None <> Some _ |- _ => clear H + | H: _ = Some _ |- _ => (try rewrite !H in * |- *); generalize H; clear H + | H: _ = None |- _ => (try rewrite !H in * |- *); generalize H; clear H + end. + +Ltac explore_destruct := + repeat (match goal with + | [H: ?expr = ?val |- context[match ?expr with | _ => _ end]] => rewrite H + | [H: match ?var with | _ => _ end |- _] => destruct var + | [ |- context[match ?m with | _ => _ end] ] => destruct m + | _ => discriminate + end). + +Ltac simplify_someHyps := + repeat (simplify_someHyp; simpl in * |- *). + +Ltac try_simplify_someHyps := + try (intros; simplify_someHyps; eauto). + +(* TODO: try to improve this tactic with a better control over names and inversion *) +Ltac simplify_SOME x := + (repeat inversion_SOME x); try_simplify_someHyps. + +(** ** The easy way: Forward simulation of RTLpath by RTL + +This way can be viewed as a correctness property: all transitions in RTLpath are valid RTL transitions ! + +*) + +Local Hint Resolve RTL.exec_Inop RTL.exec_Iop RTL.exec_Iload RTL.exec_Istore RTL.exec_Icond RTL.exec_Iload_notrap1 RTL.exec_Iload_notrap2: core. + +(* istep reflects RTL.step *) +Lemma istep_correct ge i stack (f:function) sp rs m st : + istep ge i sp rs m = Some st -> + forall pc, (fn_code f)!pc = Some i -> + RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(ipc) st.(irs) st.(imem)). +Proof. + destruct i; simpl; try congruence; simplify_SOME x. + 1-3: explore_destruct; simplify_SOME x. +Qed. + +Local Hint Resolve star_refl: core. + +(* isteps reflects a star relation on RTL.step *) +Lemma isteps_correct ge path stack f sp: forall rs m pc st, + isteps ge path f sp rs m pc = Some st -> + star RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(ipc) st.(irs) st.(imem)). +Proof. + induction path; simpl; try_simplify_someHyps. + inversion_SOME i; intros Hi. + inversion_SOME st0; intros Hst0. + destruct (icontinue st0) eqn:cont. + + intros; eapply star_step. + - eapply istep_correct; eauto. + - simpl; eauto. + - auto. + + intros; simplify_someHyp; eapply star_step. + - eapply istep_correct; eauto. + - simpl; eauto. + - auto. +Qed. + +Lemma isteps_correct_early_exit ge path stack f sp: forall rs m pc st, + isteps ge path f sp rs m pc = Some st -> + st.(icontinue) = false -> + plus RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(ipc) st.(irs) st.(imem)). +Proof. + destruct path; simpl; try_simplify_someHyps; try congruence. + inversion_SOME i; intros Hi. + inversion_SOME st0; intros Hst0. + destruct (icontinue st0) eqn:cont. + + intros; eapply plus_left. + - eapply istep_correct; eauto. + - eapply isteps_correct; eauto. + - auto. + + intros X; inversion X; subst. + eapply plus_one. + eapply istep_correct; eauto. +Qed. + +Local Hint Resolve list_forall2_nil match_globdef_fun linkorder_refl match_globvar_intro: core. + +Section CORRECTNESS. + +Variable p: program. + +Lemma match_prog_RTL: match_program (fun _ f tf => tf = fundef_RTL f) eq p (transf_program p). +Proof. + eapply match_transform_program; eauto. +Qed. + +Let pge := Genv.globalenv p. +Let ge := Genv.globalenv (transf_program p). + +Lemma senv_preserved: Senv.equiv pge ge. +Proof (Genv.senv_match match_prog_RTL). + +Lemma symbols_preserved s: Genv.find_symbol ge s = Genv.find_symbol pge s. +Proof (Genv.find_symbol_match match_prog_RTL s). + +Lemma find_function_RTL_match ros rs fd: + find_function pge ros rs = Some fd -> RTL.find_function ge ros rs = Some (fundef_RTL fd). +Proof. + destruct ros; simpl. + + intro; exploit (Genv.find_funct_match match_prog_RTL); eauto. + intros (cuint & tf & H1 & H2 & H3); subst; auto. + + rewrite symbols_preserved. + destruct (Genv.find_symbol pge i); simpl; try congruence. + intro; exploit (Genv.find_funct_ptr_match match_prog_RTL); eauto. + intros (cuint & tf & H1 & H2 & H3); subst; auto. +Qed. + +Local Hint Resolve istep_correct RTL.exec_Ibuiltin RTL.exec_Ijumptable RTL.exec_Ireturn RTL.exec_Icall RTL.exec_Itailcall find_function_RTL_match: core. + +Lemma path_last_step_correct stack f sp pc rs m t s: + path_last_step ge pge stack f sp pc rs m t s -> + RTL.step ge (State stack f sp pc rs m) t s. +Proof. + destruct 1; try (eapply istep_correct); simpl; eauto. +Qed. + +Lemma path_step_correct path stack f sp pc rs m t s: + path_step ge pge path stack f sp rs m pc t s -> + plus RTL.step ge (State stack f sp pc rs m) t s. +Proof. + destruct 1. + + eapply isteps_correct_early_exit; eauto. + + eapply plus_right. + eapply isteps_correct; eauto. + eapply path_last_step_correct; eauto. + auto. +Qed. + +Local Hint Resolve plus_one RTL.exec_function_internal RTL.exec_function_external RTL.exec_return: core. + +Lemma step_correct s t s': step ge pge s t s' -> plus RTL.step ge s t s'. +Proof. + destruct 1; try (eapply path_step_correct); simpl; eauto. +Qed. + +Theorem RTLpath_correct: forward_simulation (semantics p) (RTL.semantics p). +Proof. + eapply forward_simulation_plus with (match_states := fun s1 s2 => s2 = state_RTL s1); simpl; auto. + - apply senv_preserved. + - destruct 1; intros; eexists; intuition eauto. econstructor; eauto. + + apply (Genv.init_mem_match match_prog_RTL); auto. + + rewrite (Genv.find_symbol_match match_prog_RTL). + rewrite (match_program_main match_prog_RTL); eauto. + + exploit (Genv.find_funct_ptr_match match_prog_RTL); eauto. + intros (cunit & tf0 & XX); intuition subst; eauto. + - unfold final_state; intros; subst; eauto. + - intros; subst. eexists; intuition. + eapply step_correct; eauto. +Qed. + +End CORRECTNESS. + +Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B), + prog_defs p1 = prog_defs p2 -> + prog_public p1 = prog_public p2 -> + prog_main p1 = prog_main p2 -> + p1 = p2. +Proof. + intros. destruct p1. destruct p2. simpl in *. subst. auto. +Qed. + +Lemma cons_extract {A: Type} : forall (l: list A) a b, a = b -> a::l = b::l. +Proof. + intros. congruence. +Qed. + +(* Definition transf_program : RTLpath.program -> RTL.program := transform_program fundef_RTL. + +Lemma transf_program_proj: forall p, transf_program (transf_program p) = p. +Proof. + intros p. destruct p as [defs pub main]. unfold program_proj. simpl. + apply program_equals; simpl; auto. + induction defs. + - simpl; auto. + - simpl. rewrite IHdefs. + destruct a as [id gd]; simpl. + destruct gd as [f|v]; simpl; auto. + rewrite transf_fundef_proj. auto. +Qed. *) + + +(** The hard way: Forward simulation of RTL by RTLpath + +This way can be viewed as a completeness property: all transitions in RTL can be represented as RTLpath transitions ! + +*) + +(* This lemma is probably needed to compose a pass from RTL -> RTLpath with other passes.*) +Lemma match_RTL_prog {LA: Linker fundef} {LV: Linker unit} p: match_program (fun _ f tf => f = fundef_RTL tf) eq (transf_program p) p. +Proof. + unfold match_program, match_program_gen; intuition. + unfold transf_program at 2; simpl. + generalize (prog_defs p). + induction l as [|a l]; simpl; eauto. + destruct a; simpl. + intros; eapply list_forall2_cons; eauto. + unfold match_ident_globdef; simpl; intuition; destruct g as [f|v]; simpl; eauto. + eapply match_globdef_var. destruct v; eauto. +Qed. + +(* Theory of wellformed paths *) + +Fixpoint nth_default_succ (c: code) (path:nat) (pc: node): option node := + match path with + | O => Some pc + | S path' => + SOME i <- c!pc IN + SOME pc' <- default_succ i IN + nth_default_succ c path' pc' + end. + +Lemma wellformed_suffix_path c pm path path': + (path' <= path)%nat -> + forall pc, wellformed_path c pm path pc -> + exists pc', nth_default_succ c (path-path') pc = Some pc' /\ wellformed_path c pm path' pc'. +Proof. + induction 1 as [|m]. + + intros. enough (path'-path'=0)%nat as ->; [simpl;eauto|omega]. + + intros pc WF; enough (S m-path'=S (m-path'))%nat as ->; [simpl;eauto|omega]. + inversion WF; subst; clear WF; intros; simplify_someHyps. + intros; simplify_someHyps; eauto. +Qed. + +Definition nth_default_succ_inst (c: code) (path:nat) pc: option instruction := + SOME pc <- nth_default_succ c path pc IN + c!pc. + +Lemma final_node_path f path pc: + (fn_path f)!pc = Some path -> + exists i, nth_default_succ_inst (fn_code f) path.(psize) pc = Some i + /\ (forall n, List.In n (successors_instr i) -> path_entry (*fn_code f*) (fn_path f) n). +Proof. + intros; exploit fn_path_wf; eauto. + intro WF. + set (ps:=path.(psize)). + exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps O); omega || eauto. + destruct 1 as (pc' & NTH_SUCC & WF'); auto. + assert (ps - 0 = ps)%nat as HH by omega. rewrite HH in NTH_SUCC. clear HH. + unfold nth_default_succ_inst. + inversion WF'; clear WF'; subst. simplify_someHyps; eauto. +Qed. + +Lemma internal_node_path path f path0 pc: + (fn_path f)!pc = (Some path0) -> + (path < path0.(psize))%nat -> + exists i pc', + nth_default_succ_inst (fn_code f) path pc = Some i /\ + default_succ i = Some pc' /\ + (forall n, early_exit i = Some n -> path_entry (*fn_code f*) (fn_path f) n). +Proof. + intros; exploit fn_path_wf; eauto. + set (ps:=path0.(psize)). + intro WF; exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps (ps-path)); eauto. { omega. } + destruct 1 as (pc' & NTH_SUCC & WF'). + assert (ps - (ps - path) = path)%nat as HH by omega. rewrite HH in NTH_SUCC. clear HH. + unfold nth_default_succ_inst. + inversion WF'; clear WF'; subst. { omega. } + simplify_someHyps; eauto. +Qed. + +Lemma initialize_path (*c*) pm n: path_entry (*c*) pm n -> exists path, pm!n = Some path. +Proof. + unfold path_entry; destruct pm!n; eauto. intuition congruence. +Qed. +Local Hint Resolve fn_entry_point_wf: core. +Local Opaque path_entry. + +Lemma istep_successors ge i sp rs m st: + istep ge i sp rs m = Some st -> + In (ipc st) (successors_instr i). +Proof. + destruct i; simpl; try congruence; simplify_SOME x. + all: explore_destruct; simplify_SOME x. +Qed. + +Lemma istep_normal_exit ge i sp rs m st: + istep ge i sp rs m = Some st -> + st.(icontinue) = true -> + default_succ i = Some st.(ipc). +Proof. + destruct i; simpl; try congruence; simplify_SOME x. + all: explore_destruct; simplify_SOME x. +Qed. + +Lemma isteps_normal_exit ge path f sp: forall rs m pc st, + st.(icontinue) = true -> + isteps ge path f sp rs m pc = Some st -> + nth_default_succ (fn_code f) path pc = Some st.(ipc). +Proof. + induction path; simpl. { try_simplify_someHyps. } + intros rs m pc st CONT; try_simplify_someHyps. + inversion_SOME i; intros Hi. + inversion_SOME st0; intros Hst0. + destruct (icontinue st0) eqn:X; try congruence. + try_simplify_someHyps. + intros; erewrite istep_normal_exit; eauto. +Qed. + + +(* TODO: the three following lemmas could maybe simplified by introducing an auxiliary + left-recursive definition equivalent to isteps ? +*) +Lemma isteps_step_right ge path f sp: forall rs m pc st i, + isteps ge path f sp rs m pc = Some st -> + st.(icontinue) = true -> + (fn_code f)!(st.(ipc)) = Some i -> + istep ge i sp st.(irs) st.(imem) = isteps ge (S path) f sp rs m pc. +Proof. + induction path. + + simpl; intros; try_simplify_someHyps. simplify_SOME st. + destruct st as [b]; destruct b; simpl; auto. + + intros rs m pc st i H. + simpl in H. + generalize H; clear H; simplify_SOME xx. + destruct (icontinue xx0) eqn: CONTxx0. + * intros; erewrite IHpath; eauto. + * intros; congruence. +Qed. + +Lemma isteps_inversion_early ge path f sp: forall rs m pc st, + isteps ge path f sp rs m pc = Some st -> + (icontinue st)=false -> + exists st0 i path0, + (path > path0)%nat /\ + isteps ge path0 f sp rs m pc = Some st0 /\ + st0.(icontinue) = true /\ + (fn_code f)!(st0.(ipc)) = Some i /\ + istep ge i sp st0.(irs) st0.(imem) = Some st. +Proof. + induction path as [|path]; simpl. + - intros; try_simplify_someHyps; try congruence. + - intros rs m pc st; inversion_SOME i; inversion_SOME st0. + destruct (icontinue st0) eqn: CONT. + + intros STEP PC STEPS CONT0. exploit IHpath; eauto. + clear STEPS. + intros (st1 & i0 & path0 & BOUND & STEP1 & CONT1 & X1 & X2); auto. + exists st1. exists i0. exists (S path0). intuition. + simpl; try_simplify_someHyps. + rewrite CONT. auto. + + intros; try_simplify_someHyps; try congruence. + eexists. exists i. exists O; simpl. intuition eauto. + omega. +Qed. + +Lemma isteps_resize ge path0 path1 f sp rs m pc st: + (path0 <= path1)%nat -> + isteps ge path0 f sp rs m pc = Some st -> + (icontinue st)=false -> + isteps ge path1 f sp rs m pc = Some st. +Proof. + induction 1 as [|path1]; simpl; auto. + intros PSTEP CONT. exploit IHle; auto. clear PSTEP IHle H path0. + generalize rs m pc st CONT; clear rs m pc st CONT. + induction path1 as [|path]; simpl; auto. + - intros; try_simplify_someHyps; try congruence. + - intros rs m pc st; inversion_SOME i; inversion_SOME st0; intros; try_simplify_someHyps. + destruct (icontinue st0) eqn: CONT0; eauto. +Qed. + +(* FIXME - add prediction *) +Inductive is_early_exit pc: instruction -> Prop := + | Icond_early_exit cond args ifnot predict: + is_early_exit pc (Icond cond args pc ifnot predict) + . (* TODO add jumptable here ? *) + +Lemma istep_early_exit ge i sp rs m st : + istep ge i sp rs m = Some st -> + st.(icontinue) = false -> + st.(irs) = rs /\ st.(imem) = m /\ is_early_exit st.(ipc) i. +Proof. + Local Hint Resolve Icond_early_exit: core. + destruct i; simpl; try congruence; simplify_SOME b; simpl; try congruence. + all: explore_destruct; simplify_SOME b; try discriminate. +Qed. + +Section COMPLETENESS. + +Variable p: program. + +Let pge := Genv.globalenv p. +Let ge := Genv.globalenv (transf_program p). + +Lemma find_funct_ptr_RTL_preserv b f: + Genv.find_funct_ptr ge b = Some f -> (exists f0, Genv.find_funct_ptr pge b = Some f0 /\ f = f0). +Proof. + intros; exploit (Genv.find_funct_ptr_match (match_RTL_prog p)); eauto. + destruct 1 as (cunit & tf & X & Y & Z); subst. + eauto. +Qed. + +Lemma find_RTL_function_match ros rs fd: + RTL.find_function ge ros rs = Some fd -> exists fd', fd = fundef_RTL fd' /\ find_function pge ros rs = Some fd'. +Proof. + destruct ros; simpl. + + intro; exploit (Genv.find_funct_match (match_RTL_prog p)); eauto. + intros (cuint & tf & H1 & H2 & H3); subst; eauto. + + rewrite (symbols_preserved p); unfold pge. + destruct (Genv.find_symbol (Genv.globalenv p) i); simpl; try congruence. + intro; exploit find_funct_ptr_RTL_preserv; eauto. + intros (tf & H1 & H2); subst; eauto. +Qed. + + +(** *** Definition of well-formed stacks and of match_states *) +Definition wf_stf (st: stackframe): Prop := + match st with + | Stackframe res f sp pc rs => path_entry (*f.(fn_code)*) f.(fn_path) pc + end. + +Definition wf_stackframe (stack: list stackframe): Prop := + forall st, List.In st stack -> wf_stf st. + +Lemma wf_stackframe_nil: wf_stackframe nil. +Proof. + unfold wf_stackframe; simpl. tauto. +Qed. +Local Hint Resolve wf_stackframe_nil: core. + +Lemma wf_stackframe_cons st stack: + wf_stackframe (st::stack) <-> (wf_stf st) /\ wf_stackframe stack. +Proof. + unfold wf_stackframe; simpl; intuition (subst; auto). +Qed. + +Definition stack_of (s: state): list stackframe := + match s with + | State stack f sp pc rs m => stack + | Callstate stack f args m => stack + | Returnstate stack v m => stack + end. + +Definition is_inst (s: RTL.state): bool := + match s with + | RTL.State stack f sp pc rs m => true + | _ => false + end. + +Inductive match_inst_states_goal (idx: nat) (s1:RTL.state): state -> Prop := + | State_match path stack f sp pc rs m s2: + (fn_path f)!pc = Some path -> + (idx <= path.(psize))%nat -> + isteps ge (path.(psize)-idx) f sp rs m pc = Some s2 -> + s1 = State stack f sp s2.(ipc) s2.(irs) s2.(imem) -> + match_inst_states_goal idx s1 (State stack f sp pc rs m). + +Definition match_inst_states (idx: nat) (s1:RTL.state) (s2:state): Prop := + if is_inst s1 then match_inst_states_goal idx s1 s2 else s1 = state_RTL s2. + +Definition match_states (idx: nat) (s1:RTL.state) (s2:state): Prop := + match_inst_states idx s1 s2 + /\ wf_stackframe (stack_of s2). + +(** *** Auxiliary lemmas of completeness *) +Lemma istep_complete t i stack f sp rs m pc s': + RTL.step ge (State stack f sp pc rs m) t s' -> + (fn_code f)!pc = Some i -> + default_succ i <> None -> + t = E0 /\ exists st, istep ge i sp rs m = Some st /\ s'=(State stack f sp st.(ipc) st.(irs) st.(imem)). +Proof. + intros H X; inversion H; simpl; subst; try rewrite X in * |-; clear X; simplify_someHyps; try congruence; + (split; auto); simplify_someHyps; eexists; split; simplify_someHyps; eauto. + all: explore_destruct; simplify_SOME a. +Qed. + +Lemma stuttering path idx stack f sp rs m pc st t s1': + isteps ge (path.(psize)-(S idx)) f sp rs m pc = Some st -> + (fn_path f)!pc = Some path -> + (S idx <= path.(psize))%nat -> + st.(icontinue) = true -> + RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' -> + t = E0 /\ match_inst_states idx s1' (State stack f sp pc rs m). +Proof. + intros PSTEP PATH BOUND CONT RSTEP; exploit (internal_node_path (path.(psize)-(S idx))); omega || eauto. + intros (i & pc' & Hi & Hpc & DUM). + unfold nth_default_succ_inst in Hi. + erewrite isteps_normal_exit in Hi; eauto. + exploit istep_complete; congruence || eauto. + intros (SILENT & st0 & STEP0 & EQ). + intuition; subst; unfold match_inst_states; simpl. + intros; refine (State_match _ _ path stack f sp pc rs m _ PATH _ _ _); simpl; omega || eauto. + set (ps:=path.(psize)). enough (ps - idx = S (ps - (S idx)))%nat as ->; try omega. + erewrite <- isteps_step_right; eauto. +Qed. + +Lemma normal_exit path stack f sp rs m pc st t s1': + isteps ge path.(psize) f sp rs m pc = Some st -> + (fn_path f)!pc = Some path -> + st.(icontinue) = true -> + RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' -> + wf_stackframe stack -> + exists s2', + (path_last_step ge pge stack f sp st.(ipc) st.(irs) st.(imem)) t s2' + /\ (exists idx', match_states idx' s1' s2'). +Proof. + Local Hint Resolve istep_successors list_nth_z_in: core. (* Hint for path_entry proofs *) + intros PSTEP PATH CONT RSTEP WF; exploit (final_node_path f path); eauto. + intros (i & Hi & SUCCS). + unfold nth_default_succ_inst in Hi. + erewrite isteps_normal_exit in Hi; eauto. + destruct (default_succ i) eqn:Hn0. + + (* exec_istate *) + exploit istep_complete; congruence || eauto. + intros (SILENT & st0 & STEP0 & EQ); subst. + exploit (exec_istate ge pge); eauto. + eexists; intuition eauto. + unfold match_states, match_inst_states; simpl. + destruct (initialize_path (*fn_code f*) (fn_path f) (ipc st0)) as (path0 & Hpath0); eauto. + exists (path0.(psize)); intuition eauto. + econstructor; eauto. + * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega. + * simpl; eauto. + + generalize Hi; inversion RSTEP; clear RSTEP; subst; (repeat (simplify_someHyp; simpl in * |- * )); try congruence; eauto. + - (* Icall *) + intros; exploit find_RTL_function_match; eauto. + intros (fd' & MATCHfd & Hfd'); subst. + exploit (exec_Icall ge pge); eauto. + eexists; intuition eauto. + eexists O; unfold match_states, match_inst_states; simpl; intuition eauto. + rewrite wf_stackframe_cons; intuition simpl; eauto. + - (* Itailcall *) + intros; exploit find_RTL_function_match; eauto. + intros (fd' & MATCHfd & Hfd'); subst. + exploit (exec_Itailcall ge pge); eauto. + eexists; intuition eauto. + eexists O; unfold match_states, match_inst_states; simpl; intuition eauto. + - (* Ibuiltin *) + intros; exploit exec_Ibuiltin; eauto. + eexists; intuition eauto. + unfold match_states, match_inst_states; simpl. + destruct (initialize_path (*fn_code f*) (fn_path f) pc') as (path0 & Hpath0); eauto. + exists path0.(psize); intuition eauto. + econstructor; eauto. + * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega. + * simpl; eauto. + - (* Ijumptable *) + intros; exploit exec_Ijumptable; eauto. + eexists; intuition eauto. + unfold match_states, match_inst_states; simpl. + destruct (initialize_path (*fn_code f*) (fn_path f) pc') as (path0 & Hpath0); eauto. + exists path0.(psize); intuition eauto. + econstructor; eauto. + * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega. + * simpl; eauto. + - (* Ireturn *) + intros; exploit exec_Ireturn; eauto. + eexists; intuition eauto. + eexists O; unfold match_states, match_inst_states; simpl; intuition eauto. +Qed. + +Lemma path_step_complete stack f sp rs m pc t s1' idx path st: + isteps ge (path.(psize)-idx) f sp rs m pc = Some st -> + (fn_path f)!pc = Some path -> + (idx <= path.(psize))%nat -> + RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' -> + wf_stackframe stack -> + exists idx' s2', + (path_step ge pge path.(psize) stack f sp rs m pc t s2' + \/ (t = E0 /\ s2'=(State stack f sp pc rs m) /\ (idx' < idx)%nat) + \/ (exists path', path_step ge pge path.(psize) stack f sp rs m pc E0 (State stack f sp st.(ipc) st.(irs) st.(imem)) + /\ (fn_path f)!(ipc st) = Some path' /\ path'.(psize) = O + /\ path_step ge pge path'.(psize) stack f sp st.(irs) st.(imem) st.(ipc) t s2') + ) + /\ match_states idx' s1' s2'. +Proof. + Local Hint Resolve exec_early_exit exec_normal_exit: core. + intros PSTEP PATH BOUND RSTEP WF; destruct (st.(icontinue)) eqn: CONT. + destruct idx as [ | idx]. + + (* path_step on normal_exit *) + assert (path.(psize)-0=path.(psize))%nat as HH by omega. rewrite HH in PSTEP. clear HH. + exploit normal_exit; eauto. + intros (s2' & LSTEP & (idx' & MATCH)). + exists idx'; exists s2'; intuition eauto. + + (* stuttering step *) + exploit stuttering; eauto. + unfold match_states; exists idx; exists (State stack f sp pc rs m); + intuition. + + (* one or two path_step on early_exit *) + exploit (isteps_resize ge (path.(psize) - idx)%nat path.(psize)); eauto; try omega. + clear PSTEP; intros PSTEP. + (* TODO for clarification: move the assert below into a separate lemma *) + assert (HPATH0: exists path0, (fn_path f)!(ipc st) = Some path0). + { clear RSTEP. + exploit isteps_inversion_early; eauto. + intros (st0 & i & path0 & BOUND0 & PSTEP0 & CONT0 & PC0 & STEP0). + exploit istep_early_exit; eauto. + intros (X1 & X2 & EARLY_EXIT). + destruct st as [cont pc0 rs0 m0]; simpl in * |- *; intuition subst. + exploit (internal_node_path path0); omega || eauto. + intros (i' & pc' & Hi' & Hpc' & ENTRY). + unfold nth_default_succ_inst in Hi'. + erewrite isteps_normal_exit in Hi'; eauto. + clear pc' Hpc' STEP0 PSTEP0 BOUND0; try_simplify_someHyps; intros. + destruct EARLY_EXIT as [cond args ifnot]; simpl in ENTRY; + destruct (initialize_path (*fn_code f*) (fn_path f) pc0); eauto. + } + destruct HPATH0 as (path1 & Hpath1). + destruct (path1.(psize)) as [|ps] eqn:Hpath1size. + * (* two step case *) + exploit (normal_exit path1); try rewrite Hpath1size; simpl; eauto. + simpl; intros (s2' & LSTEP & (idx' & MATCH)). + exists idx'. exists s2'. constructor; auto. + right. right. eexists; intuition eauto. + (* now, prove the last step *) + rewrite Hpath1size; exploit exec_normal_exit. 4:{ eauto. } + - simpl; eauto. + - simpl; eauto. + - simpl; eauto. + * (* single step case *) + exploit (stuttering path1 ps stack f sp (irs st) (imem st) (ipc st)); simpl; auto. + - { rewrite Hpath1size; enough (S ps-S ps=0)%nat as ->; try omega. simpl; eauto. } + - omega. + - simpl; eauto. + - simpl; eauto. + - intuition subst. + repeat eexists; intuition eauto. +Qed. + +Lemma step_noninst_complete s1 t s1' s2: + is_inst s1 = false -> + s1 = state_RTL s2 -> + RTL.step ge s1 t s1' -> + wf_stackframe (stack_of s2) -> + exists s2', step ge pge s2 t s2' /\ exists idx, match_states idx s1' s2'. +Proof. + intros H0 H1 H2 WFSTACK; destruct s2; subst; simpl in * |- *; try congruence; + inversion H2; clear H2; subst; try_simplify_someHyps; try congruence. + + (* exec_function_internal *) + destruct f; simpl in H3; inversion H3; subst; clear H3. + eexists; constructor 1. + * eapply exec_function_internal; eauto. + * unfold match_states, match_inst_states; simpl. + destruct (initialize_path (*fn_code f*) (fn_path f) (fn_entrypoint (fn_RTL f))) as (path & Hpath); eauto. + exists path.(psize). constructor; auto. + econstructor; eauto. + - set (ps:=path.(psize)). enough (ps-ps=O)%nat as ->; simpl; eauto. + omega. + - simpl; auto. + + (* exec_function_external *) + destruct f; simpl in H3 |-; inversion H3; subst; clear H3. + eexists; constructor 1. + * apply exec_function_external; eauto. + * unfold match_states, match_inst_states; simpl. exists O; auto. + + (* exec_return *) + destruct stack eqn: Hstack; simpl in H1; inversion H1; clear H1; subst. + destruct s0 eqn: Hs0; simpl in H0; inversion H0; clear H0; subst. + eexists; constructor 1. + * apply exec_return. + * unfold match_states, match_inst_states; simpl. + rewrite wf_stackframe_cons in WFSTACK. + destruct WFSTACK as (H0 & H1); simpl in H0. + destruct (initialize_path (*fn_code f0*) (fn_path f0) pc0) as (path & Hpath); eauto. + exists path.(psize). constructor; auto. + econstructor; eauto. + - set (ps:=path.(psize)). enough (ps-ps=O)%nat as ->; simpl; eauto. + omega. + - simpl; auto. +Qed. + +(** *** The main completeness lemma and the simulation theorem...*) +Lemma step_complete s1 t s1' idx s2: + match_states idx s1 s2 -> + RTL.step ge s1 t s1' -> + exists idx' s2', (plus (step ge) pge s2 t s2' \/ (t = E0 /\ s2=s2' /\ (idx' < idx)%nat)) /\ match_states idx' s1' s2'. +Proof. + Local Hint Resolve plus_one plus_two exec_path: core. + unfold match_states at 1, match_inst_states. intros (IS_INST & WFSTACK). destruct (is_inst s1) eqn: His1. + - clear His1; destruct IS_INST as [path stack f sp pc rs m s2 X X0 X1 X2]; auto; subst; simpl in * |- *. + intros STEP; exploit path_step_complete; eauto. + intros (idx' & s2' & H0 & H1). + eexists; eexists; eauto. + destruct H0 as [H0|[H0|(path'&H0)]]; intuition subst; eauto. + - intros; exploit step_noninst_complete; eauto. + intros (s2' & STEP & (idx0 & MATCH)). + exists idx0; exists s2'; intuition auto. +Qed. + +Theorem RTLpath_complete: forward_simulation (RTL.semantics p) (semantics p). +Proof. + eapply (Forward_simulation (L1:=RTL.semantics p) (L2:=semantics p) lt match_states). + constructor 1; simpl. + - apply lt_wf. + - unfold match_states, match_inst_states. destruct 1; simpl; exists O. + destruct (find_funct_ptr_RTL_preserv b f) as (f0 & X1 & X2); subst; eauto. + exists (Callstate nil f0 nil m0). simpl; split; try econstructor; eauto. + + apply (Genv.init_mem_match (match_RTL_prog p)); auto. + + rewrite (Genv.find_symbol_match (match_RTL_prog p)). + rewrite (match_program_main (match_RTL_prog p)); eauto. + - unfold final_state, match_states, match_inst_states. intros i s1 s2 r (H0 & H1) H2; destruct H2. + destruct s2; simpl in * |- *; inversion H0; subst. + constructor. + - Local Hint Resolve star_refl: core. + intros; exploit step_complete; eauto. + destruct 1 as (idx' & s2' & X). + exists idx'. exists s2'. intuition (subst; eauto). + - intros id; destruct (senv_preserved p); simpl in * |-. intuition. +Qed. + +End COMPLETENESS. |