diff options
Diffstat (limited to 'scheduling/RTLpath.v')
| -rw-r--r-- | scheduling/RTLpath.v | 1066 |
1 files changed, 0 insertions, 1066 deletions
diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v deleted file mode 100644 index b29a7759..00000000 --- a/scheduling/RTLpath.v +++ /dev/null @@ -1,1066 +0,0 @@ -(** 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. -Require Import Lia. - -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 *) - pre_output_regs: Regset.t; - (** 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 (pm: path_map) (n: node): Prop := pm!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_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 <- Vundef 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|lia]. - + intros pc WF; enough (S m-path'=S (m-path'))%nat as ->; [simpl;eauto|lia]. - 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); lia || eauto. - destruct 1 as (pc' & NTH_SUCC & WF'); auto. - assert (ps - 0 = ps)%nat as HH by lia. 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. { lia. } - destruct 1 as (pc' & NTH_SUCC & WF'). - assert (ps - (ps - path) = path)%nat as HH by lia. rewrite HH in NTH_SUCC. clear HH. - unfold nth_default_succ_inst. - inversion WF'; clear WF'; subst. { lia. } - 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. - lia. -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))); lia || 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; lia || eauto. - set (ps:=path.(psize)). enough (ps - idx = S (ps - (S idx)))%nat as ->; try lia. - 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 || lia. - * 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 || lia. - * 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 || lia. - * 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 lia. 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 lia. - 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); lia || 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 lia. simpl; eauto. } - - lia. - - 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. - lia. - - 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. - lia. - - 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. |