diff options
| -rw-r--r-- | Makefile.extr | 3 | ||||
| -rw-r--r-- | backend/Lineartyping.v | 1 | ||||
| -rwxr-xr-x | configure | 1 | ||||
| -rw-r--r-- | driver/Compiler.vexpand | 6 | ||||
| -rw-r--r-- | kvx/SelectOpproof.v | 1 | ||||
| -rw-r--r-- | kvx/lib/RTLpath.v | 1063 | ||||
| -rw-r--r-- | kvx/lib/RTLpathLivegen.v | 290 | ||||
| -rw-r--r-- | kvx/lib/RTLpathLivegenaux.ml | 287 | ||||
| -rw-r--r-- | kvx/lib/RTLpathLivegenproof.v | 736 | ||||
| -rw-r--r-- | kvx/lib/RTLpathSE_theory.v | 1336 | ||||
| -rw-r--r-- | kvx/lib/RTLpathScheduler.v | 190 | ||||
| -rw-r--r-- | kvx/lib/RTLpathScheduleraux.ml | 8 | ||||
| -rw-r--r-- | kvx/lib/RTLpathSchedulerproof.v | 303 | ||||
| -rw-r--r-- | kvx/lib/RTLpathproof.v | 50 | ||||
| -rw-r--r-- | tools/compiler_expand.ml | 5 |
15 files changed, 4276 insertions, 4 deletions
diff --git a/Makefile.extr b/Makefile.extr index 1f5e6aeb..59cc6c1d 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -43,7 +43,8 @@ cparser/pre_parser_messages.ml: DIRS=extraction \ lib common $(ARCH) backend cfrontend cparser driver \ - exportclight debug kvx/unittest kvx/abstractbb/Impure/ocaml + exportclight debug kvx/unittest kvx/abstractbb/Impure/ocaml \ + kvx/lib INCLUDES=$(patsubst %,-I %, $(DIRS)) diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 3fe61470..22658fb7 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -324,7 +324,6 @@ Local Opaque mreg_type. apply wt_setreg; auto; try (apply wt_undef_regs; auto). eapply Val.has_subtype; eauto. - change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. red; intros; subst op. simpl in ISMOVE. destruct args; try discriminate. destruct args; discriminate. @@ -845,6 +845,7 @@ EXECUTE=kvx-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __KVX_COS__ SIMU=kvx-cluster -- BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ + RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathScheduler.v RTLpathSchedulerproof.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 0f59aab7..3285a012 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -297,6 +297,12 @@ EXPAND_ASM_SEMANTICS eapply RTLgenproof.transf_program_correct; eassumption. EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. + eapply RTLpathLivegenproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLpathSchedulerproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLpathproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Tunnelingproof.transf_program_correct; eassumption. diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index d1d0b95c..c23ed601 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1199,7 +1199,6 @@ Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate. Qed. diff --git a/kvx/lib/RTLpath.v b/kvx/lib/RTLpath.v new file mode 100644 index 00000000..64f3917e --- /dev/null +++ b/kvx/lib/RTLpath.v @@ -0,0 +1,1063 @@ +(** 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 +}. + +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 + 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. diff --git a/kvx/lib/RTLpathLivegen.v b/kvx/lib/RTLpathLivegen.v new file mode 100644 index 00000000..1f0ebe3c --- /dev/null +++ b/kvx/lib/RTLpathLivegen.v @@ -0,0 +1,290 @@ +(** Building a RTLpath program with liveness annotation. +*) + + +Require Import Coqlib. +Require Import Maps. +Require Import Lattice. +Require Import AST. +Require Import Op. +Require Import Registers. +Require Import Globalenvs Smallstep RTL RTLpath. +Require Import Bool Errors. +Require Import Program. + +Local Open Scope lazy_bool_scope. + +Local Open Scope option_monad_scope. + +Axiom build_path_map: RTL.function -> path_map. + +Extract Constant build_path_map => "RTLpathLivegenaux.build_path_map". + +Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool := + match rl with + | nil => true + | r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive + end. + +Definition exit_checker {A} (pm: path_map) (alive: Regset.t) (pc: node) (v:A): option A := + SOME path <- pm!pc IN + ASSERT Regset.subset path.(input_regs) alive IN + Some v. + +Lemma exit_checker_path_entry A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res: + exit_checker pm alive pc v = Some res -> path_entry pm pc. +Proof. + unfold exit_checker, path_entry. + inversion_SOME path; simpl; congruence. +Qed. + +Lemma exit_checker_res A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res: + exit_checker pm alive pc v = Some res -> v=res. +Proof. + unfold exit_checker, path_entry. + inversion_SOME path; try_simplify_someHyps. + inversion_ASSERT; try_simplify_someHyps. +Qed. + +(* FIXME - what about trap? *) +Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option (Regset.t * node) := + match i with + | Inop pc' => Some (alive, pc') + | Iop op args dst pc' => + ASSERT list_mem args alive IN + Some (Regset.add dst alive, pc') + | Iload _ chunk addr args dst pc' => + ASSERT list_mem args alive IN + Some (Regset.add dst alive, pc') + | Istore chunk addr args src pc' => + ASSERT Regset.mem src alive IN + ASSERT list_mem args alive IN + Some (alive, pc') + | Icond cond args ifso ifnot _ => + ASSERT list_mem args alive IN + exit_checker pm alive ifso (alive, ifnot) + | _ => None (* TODO jumptable ? *) + end. + + +Local Hint Resolve exit_checker_path_entry: core. + +Lemma iinst_checker_path_entry (pm: path_map) (alive: Regset.t) (i: instruction) res pc: + iinst_checker pm alive i = Some res -> + early_exit i = Some pc -> path_entry pm pc. +Proof. + destruct i; simpl; try_simplify_someHyps; subst. + inversion_ASSERT; try_simplify_someHyps. +Qed. + +Lemma iinst_checker_default_succ (pm: path_map) (alive: Regset.t) (i: instruction) res pc: + iinst_checker pm alive i = Some res -> + pc = snd res -> + default_succ i = Some pc. +Proof. + destruct i; simpl; try_simplify_someHyps; subst; + repeat (inversion_ASSERT); try_simplify_someHyps. + intros; exploit exit_checker_res; eauto. + intros; subst. simpl; auto. +Qed. + +Fixpoint ipath_checker (ps:nat) (f: RTL.function) (pm: path_map) (alive: Regset.t) (pc:node): option (Regset.t * node) := + match ps with + | O => Some (alive, pc) + | S p => + SOME i <- f.(fn_code)!pc IN + SOME res <- iinst_checker pm alive i IN + ipath_checker p f pm (fst res) (snd res) + end. + +Lemma ipath_checker_wellformed f pm ps: forall alive pc res, + ipath_checker ps f pm alive pc = Some res -> + wellformed_path f.(fn_code) pm 0 (snd res) -> + wellformed_path f.(fn_code) pm ps pc. +Proof. + induction ps; simpl; try_simplify_someHyps. + inversion_SOME i; inversion_SOME res'. + intros. eapply wf_internal_node; eauto. + * eapply iinst_checker_default_succ; eauto. + * intros; eapply iinst_checker_path_entry; eauto. +Qed. + +Definition reg_option_mem (or: option reg) (alive: Regset.t) := + match or with None => true | Some r => Regset.mem r alive end. + +Definition reg_sum_mem (ros: reg + ident) (alive: Regset.t) := + match ros with inl r => Regset.mem r alive | inr s => true end. + +(* NB: definition following [regmap_setres] in [RTL.step] semantics *) +Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t := + match res with + | BR r => Regset.add r alive + | _ => alive + end. + +Fixpoint exit_list_checker (pm: path_map) (alive: Regset.t) (l: list node): bool := + match l with + | nil => true + | pc::l' => exit_checker pm alive pc tt &&& exit_list_checker pm alive l' + end. + +Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true. +Proof. + destruct o; simpl; intuition. + - eauto. + - firstorder. try_simplify_someHyps. +Qed. + +Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true. +Proof. + intros; rewrite lazy_and_Some_true; firstorder. + destruct x; auto. +Qed. + + +Lemma exit_list_checker_correct pm alive l pc: + exit_list_checker pm alive l = true -> List.In pc l -> exit_checker pm alive pc tt = Some tt. +Proof. + intros EXIT PC; induction l; intuition. + simpl in * |-. rewrite lazy_and_Some_tt_true in EXIT. + firstorder (subst; eauto). +Qed. + +Local Hint Resolve exit_list_checker_correct: core. + +Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit := + match i with + | Icall sig ros args res pc' => + ASSERT list_mem args alive IN + ASSERT reg_sum_mem ros alive IN + exit_checker pm (Regset.add res alive) pc' tt + | Itailcall sig ros args => + ASSERT list_mem args alive IN + ASSERT reg_sum_mem ros alive IN + Some tt + | Ibuiltin ef args res pc' => + ASSERT list_mem (params_of_builtin_args args) alive IN + exit_checker pm (reg_builtin_res res alive) pc' tt + | Ijumptable arg tbl => + ASSERT Regset.mem arg alive IN + ASSERT exit_list_checker pm alive tbl IN + Some tt + | Ireturn optarg => + ASSERT (reg_option_mem optarg) alive IN + Some tt + | _ => + SOME res <- iinst_checker pm alive i IN + exit_checker pm (fst res) (snd res) tt + end. + +Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction): + inst_checker pm alive i = Some tt -> + c!pc = Some i -> wellformed_path c pm 0 pc. +Proof. + intros CHECK PC. eapply wf_last_node; eauto. + clear c pc PC. intros pc PC. + destruct i; simpl in * |- *; intuition (subst; eauto); + try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps). + intros X; exploit exit_checker_res; eauto. + clear X. intros; subst; eauto. +Qed. + +Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit := + SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc IN + SOME i <- f.(fn_code)!(snd res) IN + inst_checker pm (fst res) i. + +Lemma path_checker_wellformed f pm pc path: + path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc. +Proof. + unfold path_checker. + inversion_SOME res. + inversion_SOME i. + intros; eapply ipath_checker_wellformed; eauto. + eapply inst_checker_wellformed; eauto. +Qed. + +Fixpoint list_path_checker f pm (l:list (node*path_info)): bool := + match l with + | nil => true + | (pc, path)::l' => + path_checker f pm pc path &&& list_path_checker f pm l' + end. + +Lemma list_path_checker_correct f pm l: + list_path_checker f pm l = true -> forall e, List.In e l -> path_checker f pm (fst e) (snd e) = Some tt. +Proof. + intros CHECKER e H; induction l as [|(pc & path) l]; intuition. + simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto). +Qed. + +Definition function_checker (f: RTL.function) pm: bool := + pm!(f.(fn_entrypoint)) &&& list_path_checker f pm (PTree.elements pm). + +Lemma function_checker_correct f pm pc path: + function_checker f pm = true -> + pm!pc = Some path -> + path_checker f pm pc path = Some tt. +Proof. + unfold function_checker; rewrite lazy_and_Some_true. + intros (ENTRY & PATH) PC. + exploit list_path_checker_correct; eauto. + - eapply PTree.elements_correct; eauto. + - simpl; auto. +Qed. + +Lemma function_checker_wellformed_path_map f pm: + function_checker f pm = true -> wellformed_path_map f.(fn_code) pm. +Proof. + unfold wellformed_path_map. + intros; eapply path_checker_wellformed; eauto. + intros; eapply function_checker_correct; eauto. +Qed. + +Lemma function_checker_path_entry f pm: + function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)). +Proof. + unfold function_checker; rewrite lazy_and_Some_true; + unfold path_entry. firstorder congruence. +Qed. + +Definition liveness_ok_function (f: function): Prop := + forall pc path, f.(fn_path)!pc = Some path -> path_checker f f.(fn_path) pc path = Some tt. + +Program Definition transf_function (f: RTL.function): { r: res function | forall f', r = OK f' -> liveness_ok_function f' /\ f'.(fn_RTL) = f } := + let pm := build_path_map f in + match function_checker f pm with + | true => OK {| fn_RTL := f; fn_path := pm |} + | false => Error(msg "RTLpathGen: function_checker failed") + end. +Obligation 1. + apply function_checker_path_entry; auto. +Qed. +Obligation 2. + apply function_checker_wellformed_path_map; auto. +Qed. +Obligation 3. + unfold liveness_ok_function; simpl; intros; intuition. + apply function_checker_correct; auto. +Qed. + +Definition transf_fundef (f: RTL.fundef) : res fundef := + transf_partial_fundef (fun f => ` (transf_function f)) f. + +Inductive liveness_ok_fundef: fundef -> Prop := + | liveness_ok_Internal f: liveness_ok_function f -> liveness_ok_fundef (Internal f) + | liveness_ok_External ef: liveness_ok_fundef (External ef). + +Lemma transf_fundef_correct f f': + transf_fundef f = OK f' -> (liveness_ok_fundef f') /\ fundef_RTL f' = f. +Proof. + intros TRANSF; destruct f; simpl; monadInv TRANSF. + - destruct (transf_function f) as [res H]; simpl in * |- *; auto. + destruct (H _ EQ). + intuition subst; auto. apply liveness_ok_Internal; auto. + - intuition. apply liveness_ok_External; auto. +Qed. + +Definition transf_program (p: RTL.program) : res program := + transform_partial_program transf_fundef p. + diff --git a/kvx/lib/RTLpathLivegenaux.ml b/kvx/lib/RTLpathLivegenaux.ml new file mode 100644 index 00000000..09684f22 --- /dev/null +++ b/kvx/lib/RTLpathLivegenaux.ml @@ -0,0 +1,287 @@ +open RTL +open RTLpath +open Registers +open Maps +open Camlcoq +open Datatypes +open Kildall +open Lattice + +let debug_flag = ref false + +let dprintf fmt = let open Printf in + match !debug_flag with + | true -> printf fmt + | false -> ifprintf stdout fmt + +let get_some = function +| None -> failwith "Got None instead of Some _" +| Some thing -> thing + +let successors_inst = function +| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) | Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> [n] +| Icond (_,_,n1,n2,_) -> [n1; n2] +| Ijumptable (_,l) -> l +| Itailcall _ | Ireturn _ -> [] + +let predicted_successor = function +| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> Some n +| Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> None +| Icond (_,_,n1,n2,p) -> ( + match p with + | Some true -> Some n1 + | Some false -> Some n2 + | None -> None ) +| Ijumptable _ | Itailcall _ | Ireturn _ -> None + +let non_predicted_successors i = + match predicted_successor i with + | None -> successors_inst i + | Some n -> List.filter (fun n' -> n != n') (successors_inst i) + +let rec list_to_regset = function + | [] -> Regset.empty + | r::l -> Regset.add r (list_to_regset l) + +let get_input_regs i = + let empty = Regset.empty in + match i with + | Inop _ -> empty + | Iop (_,lr,_,_) | Iload (_,_,_,lr,_,_) | Icond (_,lr,_,_,_) -> list_to_regset lr + | Istore (_,_,lr,r,_) -> Regset.add r (list_to_regset lr) + | Icall (_, ri, lr, _, _) | Itailcall (_, ri, lr) -> begin + let rs = list_to_regset lr in + match ri with + | Coq_inr _ -> rs + | Coq_inl r -> Regset.add r rs + end + | Ibuiltin (_, lbr, _, _) -> list_to_regset @@ AST.params_of_builtin_args lbr + | Ijumptable (r, _) -> Regset.add r empty + | Ireturn opr -> (match opr with Some r -> Regset.add r empty | None -> empty) + +let get_output_reg i = + match i with + | Inop _ | Istore _ | Icond _ | Itailcall _ | Ijumptable _ | Ireturn _ -> None + | Iop (_, _, r, _) | Iload (_, _, _, _, r, _) | Icall (_, _, _, r, _) -> Some r + | Ibuiltin (_, _, brr, _) -> (match brr with AST.BR r -> Some r | _ -> None) + +(* adapted from Linearizeaux.get_join_points *) +let get_join_points code entry = + let reached = ref (PTree.map (fun n i -> false) code) in + let reached_twice = ref (PTree.map (fun n i -> false) code) in + let rec traverse pc = + if get_some @@ PTree.get pc !reached then begin + if not (get_some @@ PTree.get pc !reached_twice) then + reached_twice := PTree.set pc true !reached_twice + end else begin + reached := PTree.set pc true !reached; + traverse_succs (successors_inst @@ get_some @@ PTree.get pc code) + end + and traverse_succs = function + | [] -> () + | [pc] -> traverse pc + | pc :: l -> traverse pc; traverse_succs l + in traverse entry; !reached_twice + +(* Does not set the input_regs field *) +let get_path_map code entry join_points = + let visited = ref (PTree.map (fun n i -> false) code) in + let path_map = ref PTree.empty in + let rec dig_path e = + let psize = ref (-1) in + let path_successors = ref [] in + let rec dig_path_rec n : (path_info * node list) option = + if not (get_some @@ PTree.get n !visited) then + let inst = get_some @@ PTree.get n code in + begin + visited := PTree.set n true !visited; + psize := !psize + 1; + let successor = match predicted_successor inst with + | None -> None + | Some n' -> if get_some @@ PTree.get n' join_points then None else Some n' + in match successor with + | Some n' -> begin + path_successors := !path_successors @ non_predicted_successors inst; + dig_path_rec n' + end + | None -> Some ({ psize = (Camlcoq.Nat.of_int !psize); input_regs = Regset.empty }, !path_successors @ successors_inst inst) + end + else None + in match dig_path_rec e with + | None -> () + | Some ret -> + let (path_info, succs) = ret in + begin + path_map := PTree.set e path_info !path_map; + List.iter dig_path succs + end + in begin + dig_path entry; + !path_map + end + +let print_regset rs = begin + dprintf "["; + List.iter (fun n -> dprintf "%d " (P.to_int n)) (Regset.elements rs); + dprintf "]" +end + +let print_ptree_regset pt = begin + dprintf "["; + List.iter (fun (n, rs) -> + dprintf "\n\t"; + dprintf "%d: " (P.to_int n); + print_regset rs + ) (PTree.elements pt); + dprintf "]" +end + +let transfer f pc after = let open Liveness in + match PTree.get pc f.fn_code with + | Some i -> + (match i with + | Inop _ -> after + | Iop (_, args, res, _) -> + reg_list_live args (Regset.remove res after) + | Iload (_, _, _, args, dst, _) -> + reg_list_live args (Regset.remove dst after) + | Istore (_, _, args, src, _) -> + reg_list_live args (Regset.add src after) + | Icall (_, ros, args, res, _) -> + reg_list_live args (reg_sum_live ros (Regset.remove res after)) + | Itailcall (_, ros, args) -> + reg_list_live args (reg_sum_live ros Regset.empty) + | Ibuiltin (_, args, res, _) -> + reg_list_live (AST.params_of_builtin_args args) + (reg_list_dead (AST.params_of_builtin_res res) after) + | Icond (_, args, _, _, _) -> + reg_list_live args after + | Ijumptable (arg, _) -> + Regset.add arg after + | Ireturn optarg -> + reg_option_live optarg Regset.empty) + | None -> Regset.empty + +module RegsetLat = LFSet(Regset) + +module DS = Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward) + +let analyze f = + let liveouts = get_some @@ DS.fixpoint f.fn_code successors_instr (transfer f) in + PTree.map (fun n _ -> let lo = PMap.get n liveouts in transfer f n lo) f.fn_code + +(** OLD CODE - If needed to have our own kildall + +let transfer after = let open Liveness in function + | Inop _ -> after + | Iop (_, args, res, _) -> + reg_list_live args (Regset.remove res after) + | Iload (_, _, _, args, dst, _) -> + reg_list_live args (Regset.remove dst after) + | Istore (_, _, args, src, _) -> + reg_list_live args (Regset.add src after) + | Icall (_, ros, args, res, _) -> + reg_list_live args (reg_sum_live ros (Regset.remove res after)) + | Itailcall (_, ros, args) -> + reg_list_live args (reg_sum_live ros Regset.empty) + | Ibuiltin (_, args, res, _) -> + reg_list_live (AST.params_of_builtin_args args) + (reg_list_dead (AST.params_of_builtin_res res) after) + | Icond (_, args, _, _, _) -> + reg_list_live args after + | Ijumptable (arg, _) -> + Regset.add arg after + | Ireturn optarg -> + reg_option_live optarg Regset.empty + +let get_last_nodes f = + let visited = ref (PTree.map (fun n i -> false) f.fn_code) in + let rec step n = + let inst = get_some @@ PTree.get n f.fn_code in + let successors = successors_inst inst in + if get_some @@ PTree.get n !visited then [] + else begin + +let analyze f = + let liveness = ref (PTree.map (fun n i -> None) f.fn_code) in + let predecessors = Duplicateaux.get_predecessors_rtl f.fn_code in + let last_nodes = get_last_nodes f in + let rec step liveout n = (* liveout is the input_regs from the successor *) + let inst = get_some @@ PTree.get n f.fn_code in + let continue = ref true in + let alive = match get_some @@ PTree.get n !liveness with + | None -> transfer liveout inst + | Some pre_alive -> begin + let union = Regset.union pre_alive liveout in + let new_alive = transfer union inst in + (if Regset.equal pre_alive new_alive then continue := false); + new_alive + end + in begin + liveness := PTree.set n (Some alive) !liveness; + if !continue then + let preds = get_some @@ PTree.get n predecessors in + List.iter (step alive) preds + end + in begin + List.iter (step Regset.empty) last_nodes; + let liveness_noopt = PTree.map (fun n i -> get_some i) !liveness in + begin + debug_flag := true; + dprintf "Liveness: "; print_ptree_regset liveness_noopt; dprintf "\n"; + debug_flag := false; + liveness_noopt + end + end +*) + +let set_pathmap_liveness f pm = + let liveness = analyze f in + let new_pm = ref PTree.empty in + begin + dprintf "Liveness: "; print_ptree_regset liveness; dprintf "\n"; + List.iter (fun (n, pi) -> + let rs = get_some @@ PTree.get n liveness in + new_pm := PTree.set n {psize=pi.psize; input_regs=rs} !new_pm + ) (PTree.elements pm); + !new_pm + end + +let print_true_nodes booltree = begin + dprintf "["; + List.iter (fun (n,b) -> + if b then dprintf "%d " (P.to_int n) + ) (PTree.elements booltree); + dprintf "]"; +end + +let print_path_info pi = begin + dprintf "(psize=%d; " (Camlcoq.Nat.to_int pi.psize); + dprintf "input_regs="; + print_regset pi.input_regs; + dprintf ")" +end + +let print_path_map path_map = begin + dprintf "["; + List.iter (fun (n,pi) -> + dprintf "\n\t"; + dprintf "%d: " (P.to_int n); + print_path_info pi + ) (PTree.elements path_map); + dprintf "]" +end + +let build_path_map f = + let code = f.fn_code in + let entry = f.fn_entrypoint in + let join_points = get_join_points code entry in + let path_map = set_pathmap_liveness f @@ get_path_map code entry join_points in + begin + dprintf "Join points: "; + print_true_nodes join_points; + dprintf "\nPath map: "; + print_path_map path_map; + dprintf "\n"; + path_map + end diff --git a/kvx/lib/RTLpathLivegenproof.v b/kvx/lib/RTLpathLivegenproof.v new file mode 100644 index 00000000..0ba5ed44 --- /dev/null +++ b/kvx/lib/RTLpathLivegenproof.v @@ -0,0 +1,736 @@ +(** Proofs of the liveness properties from the liveness checker of RTLpathLivengen. +*) + + +Require Import Coqlib. +Require Import Maps. +Require Import Lattice. +Require Import AST. +Require Import Op. +Require Import Registers. +Require Import Globalenvs Smallstep RTL RTLpath RTLpathLivegen. +Require Import Bool Errors Linking Values Events. +Require Import Program. + +Definition match_prog (p: RTL.program) (tp: program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. + +Section PRESERVATION. + +Variables prog: RTL.program. +Variables tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tpge := Genv.globalenv tprog. +Let tge := Genv.globalenv (RTLpath.transf_program tprog). + +Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + rewrite <- (Genv.find_symbol_match TRANSL). + apply (Genv.find_symbol_match (match_prog_RTL tprog)). +Qed. + +Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z. +Proof. + unfold Senv.equiv. intuition congruence. +Qed. + +Lemma senv_preserved: Senv.equiv ge tge. +Proof. + eapply senv_transitivity. { eapply (Genv.senv_match TRANSL). } + eapply RTLpath.senv_preserved. +Qed. + +Lemma function_ptr_preserved v f: Genv.find_funct_ptr ge v = Some f -> + exists tf, Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf. +Proof. + intros; apply (Genv.find_funct_ptr_transf_partial TRANSL); eauto. +Qed. + + +Lemma function_ptr_RTL_preserved v f: Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some f. +Proof. + intros; exploit function_ptr_preserved; eauto. + intros (tf & Htf & TRANS). + exploit (Genv.find_funct_ptr_match (match_prog_RTL tprog)); eauto. + intros (cunit & tf0 & X & Y & DUM); subst. + unfold tge. rewrite X. + exploit transf_fundef_correct; eauto. + intuition subst; auto. +Qed. + +Lemma find_function_preserved ros rs fd: + RTL.find_function ge ros rs = Some fd -> RTL.find_function tge ros rs = Some fd. +Proof. + intros H; assert (X: exists tfd, find_function tpge ros rs = Some tfd /\ fd = fundef_RTL tfd). + * destruct ros; simpl in * |- *. + + intros; exploit (Genv.find_funct_match TRANSL); eauto. + intros (cuint & tf & H1 & H2 & H3); subst; repeat econstructor; eauto. + exploit transf_fundef_correct; eauto. + intuition auto. + + rewrite <- (Genv.find_symbol_match TRANSL) in H. + unfold tpge. destruct (Genv.find_symbol _ i); simpl; try congruence. + exploit function_ptr_preserved; eauto. + intros (tf & H1 & H2); subst; repeat econstructor; eauto. + exploit transf_fundef_correct; eauto. + intuition auto. + * destruct X as (tf & X1 & X2); subst. + eapply find_function_RTL_match; eauto. +Qed. + + +Local Hint Resolve symbols_preserved senv_preserved: core. + +Lemma transf_program_RTL_correct: + forward_simulation (RTL.semantics prog) (RTL.semantics (RTLpath.transf_program tprog)). +Proof. + eapply forward_simulation_step with (match_states:=fun (s1 s2:RTL.state) => s1=s2); simpl; eauto. + - eapply senv_preserved. + - (* initial states *) + intros s1 INIT. destruct INIT as [b f m0 ge0 INIT SYMB PTR SIG]. eexists; intuition eauto. + econstructor; eauto. + + intros; eapply (Genv.init_mem_match (match_prog_RTL tprog)). apply (Genv.init_mem_match TRANSL); auto. + + rewrite symbols_preserved. + replace (prog_main (RTLpath.transf_program tprog)) with (prog_main prog). + * eapply SYMB. + * erewrite (match_program_main (match_prog_RTL tprog)). erewrite (match_program_main TRANSL); auto. + + exploit function_ptr_RTL_preserved; eauto. + - intros; subst; auto. + - intros s t s2 STEP s1 H; subst. + eexists; intuition. + destruct STEP. + + (* Inop *) eapply exec_Inop; eauto. + + (* Iop *) eapply exec_Iop; eauto. + erewrite eval_operation_preserved; eauto. + + (* Iload *) eapply exec_Iload; eauto. + erewrite eval_addressing_preserved; eauto. + + (* Iload notrap1 *) eapply exec_Iload_notrap1; eauto. + erewrite eval_addressing_preserved; eauto. + + (* Iload notrap2 *) eapply exec_Iload_notrap2; eauto. + erewrite eval_addressing_preserved; eauto. + + (* Istore *) eapply exec_Istore; eauto. + erewrite eval_addressing_preserved; eauto. + + (* Icall *) + eapply RTL.exec_Icall; eauto. + eapply find_function_preserved; eauto. + + (* Itailcall *) + eapply RTL.exec_Itailcall; eauto. + eapply find_function_preserved; eauto. + + (* Ibuiltin *) + eapply RTL.exec_Ibuiltin; eauto. + * eapply eval_builtin_args_preserved; eauto. + * eapply external_call_symbols_preserved; eauto. + + (* Icond *) + eapply exec_Icond; eauto. + + (* Ijumptable *) + eapply RTL.exec_Ijumptable; eauto. + + (* Ireturn *) + eapply RTL.exec_Ireturn; eauto. + + (* exec_function_internal *) + eapply RTL.exec_function_internal; eauto. + + (* exec_function_external *) + eapply RTL.exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. + + (* exec_return *) + eapply RTL.exec_return; eauto. +Qed. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (RTLpath.semantics tprog). +Proof. + eapply compose_forward_simulations. + + eapply transf_program_RTL_correct. + + eapply RTLpath_complete. +Qed. + + +(* Properties used in hypothesis of [RTLpathLiveproofs.step_eqlive] theorem *) +Theorem all_fundef_liveness_ok b f: + Genv.find_funct_ptr tpge b = Some f -> liveness_ok_fundef f. +Proof. + unfold match_prog, match_program in TRANSL. + unfold Genv.find_funct_ptr, tpge; simpl; intro X. + destruct (Genv.find_def_match_2 TRANSL b) as [|f0 y H]; try congruence. + destruct y as [tf0|]; try congruence. + inversion X as [H1]. subst. clear X. + remember (@Gfun fundef unit f) as f2. + destruct H as [ctx' f1 f2 H0|]; try congruence. + inversion Heqf2 as [H2]. subst; clear Heqf2. + exploit transf_fundef_correct; eauto. + intuition. +Qed. + +End PRESERVATION. + +Local Open Scope lazy_bool_scope. +Local Open Scope option_monad_scope. + +Local Notation ext alive := (fun r => Regset.In r alive). + +Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live). +Proof. + destruct (Pos.eq_dec r1 r2). + - subst. intuition; eapply Regset.add_1; auto. + - intuition. + * right. eapply Regset.add_3; eauto. + * eapply Regset.add_2; auto. +Qed. + +Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop := + forall r, (alive r) -> rs1#r = rs2#r. + +Lemma eqlive_reg_refl alive rs: eqlive_reg alive rs rs. +Proof. + unfold eqlive_reg; auto. +Qed. + +Lemma eqlive_reg_symmetry alive rs1 rs2: eqlive_reg alive rs1 rs2 -> eqlive_reg alive rs2 rs1. +Proof. + unfold eqlive_reg; intros; symmetry; auto. +Qed. + +Lemma eqlive_reg_trans alive rs1 rs2 rs3: eqlive_reg alive rs1 rs2 -> eqlive_reg alive rs2 rs3 -> eqlive_reg alive rs1 rs3. +Proof. + unfold eqlive_reg; intros H0 H1 r H. rewrite H0; eauto. +Qed. + +Lemma eqlive_reg_update (alive: Regset.elt -> Prop) rs1 rs2 r v: eqlive_reg (fun r1 => r1 <> r /\ alive r1) rs1 rs2 -> eqlive_reg alive (rs1 # r <- v) (rs2 # r <- v). +Proof. + unfold eqlive_reg; intros EQLIVE r0 ALIVE. + destruct (Pos.eq_dec r r0) as [H|H]. + - subst. rewrite! Regmap.gss. auto. + - rewrite! Regmap.gso; auto. +Qed. + +Lemma eqlive_reg_monotonic (alive1 alive2: Regset.elt -> Prop) rs1 rs2: eqlive_reg alive2 rs1 rs2 -> (forall r, alive1 r -> alive2 r) -> eqlive_reg alive1 rs1 rs2. +Proof. + unfold eqlive_reg; intuition. +Qed. + +Lemma eqlive_reg_triv rs1 rs2: (forall r, rs1#r = rs2#r) <-> eqlive_reg (fun _ => True) rs1 rs2. +Proof. + unfold eqlive_reg; intuition. +Qed. + +Lemma eqlive_reg_triv_trans alive rs1 rs2 rs3: eqlive_reg alive rs1 rs2 -> (forall r, rs2#r = rs3#r) -> eqlive_reg alive rs1 rs3. +Proof. + rewrite eqlive_reg_triv; intros; eapply eqlive_reg_trans; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; eauto. +Qed. + +Local Hint Resolve Regset.mem_2 Regset.subset_2. + +Lemma lazy_and_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true. +Proof. + destruct b1; simpl; intuition. +Qed. + +Lemma list_mem_correct (rl: list reg) (alive: Regset.t): + list_mem rl alive = true -> forall r, List.In r rl -> ext alive r. +Proof. + induction rl; simpl; try rewrite lazy_and_true; intuition subst; auto. +Qed. + +Lemma eqlive_reg_list (alive: Regset.elt -> Prop) args rs1 rs2: eqlive_reg alive rs1 rs2 -> (forall r, List.In r args -> (alive r)) -> rs1##args = rs2##args. +Proof. + induction args; simpl; auto. + intros EQLIVE ALIVE; rewrite IHargs; auto. + unfold eqlive_reg in EQLIVE. + rewrite EQLIVE; auto. +Qed. + +Lemma eqlive_reg_listmem (alive: Regset.t) args rs1 rs2: eqlive_reg (ext alive) rs1 rs2 -> list_mem args alive = true -> rs1##args = rs2##args. +Proof. + intros; eapply eqlive_reg_list; eauto. + intros; eapply list_mem_correct; eauto. +Qed. + +Record eqlive_istate alive (st1 st2: istate): Prop := + { eqlive_continue: icontinue st1 = icontinue st2; + eqlive_ipc: ipc st1 = ipc st2; + eqlive_irs: eqlive_reg alive (irs st1) (irs st2); + eqlive_imem: (imem st1) = (imem st2) }. + +Lemma iinst_checker_eqlive ge sp pm alive i res rs1 rs2 m st1: + eqlive_reg (ext alive) rs1 rs2 -> + iinst_checker pm alive i = Some res -> + istep ge i sp rs1 m = Some st1 -> + exists st2, istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2. +Proof. + intros EQLIVE. + destruct i; simpl; try_simplify_someHyps. + - (* Inop *) + repeat (econstructor; eauto). + - (* Iop *) + inversion_ASSERT; try_simplify_someHyps. + inversion_SOME v. intros EVAL. + erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps. + repeat (econstructor; simpl; eauto). + eapply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + intros r0; rewrite regset_add_spec. + intuition. + - (* Iload *) + inversion_ASSERT; try_simplify_someHyps. + destruct t. (* TODO - simplify that proof ? *) + + inversion_SOME a0. intros EVAL. + erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps. + inversion_SOME v; try_simplify_someHyps. + repeat (econstructor; simpl; eauto). + eapply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + intros r0; rewrite regset_add_spec. + intuition. + + erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto. + destruct (eval_addressing _ _ _ _). + * destruct (Memory.Mem.loadv _ _ _). + ** intros. inv H1. repeat (econstructor; simpl; eauto). + eapply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + intros r0; rewrite regset_add_spec. + intuition. + ** intros. inv H1. repeat (econstructor; simpl; eauto). + eapply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + intros r0; rewrite regset_add_spec. + intuition. + * intros. inv H1. repeat (econstructor; simpl; eauto). + eapply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + intros r0; rewrite regset_add_spec. + intuition. + - (* Istore *) + (repeat inversion_ASSERT); try_simplify_someHyps. + inversion_SOME a0. intros EVAL. + erewrite <- eqlive_reg_listmem; eauto. + rewrite <- (EQLIVE r); auto. + inversion_SOME v; try_simplify_someHyps. + try_simplify_someHyps. + repeat (econstructor; simpl; eauto). + - (* Icond *) + inversion_ASSERT. + inversion_SOME b. intros EVAL. + intros ARGS; erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps. + repeat (econstructor; simpl; eauto). + exploit exit_checker_res; eauto. + intro; subst; simpl. auto. +Qed. + +Lemma iinst_checker_istep_continue ge sp pm alive i res rs m st: + iinst_checker pm alive i = Some res -> + istep ge i sp rs m = Some st -> + icontinue st = true -> + (snd res)=(ipc st). +Proof. + intros; exploit iinst_checker_default_succ; eauto. + erewrite istep_normal_exit; eauto. + congruence. +Qed. + +Lemma exit_checker_eqlive A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res rs1 rs2: + exit_checker pm alive pc v = Some res -> + eqlive_reg (ext alive) rs1 rs2 -> + exists path, pm!pc = Some path /\ eqlive_reg (ext path.(input_regs)) rs1 rs2. +Proof. + unfold exit_checker. + inversion_SOME path. + inversion_ASSERT. try_simplify_someHyps. + repeat (econstructor; eauto). + intros; eapply eqlive_reg_monotonic; eauto. + intros; exploit Regset.subset_2; eauto. +Qed. + +Lemma iinst_checker_eqlive_stopped ge sp pm alive i res rs1 rs2 m st1: + eqlive_reg (ext alive) rs1 rs2 -> + istep ge i sp rs1 m = Some st1 -> + iinst_checker pm alive i = Some res -> + icontinue st1 = false -> + exists path st2, pm!(ipc st1) = Some path /\ istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2. +Proof. + intros EQLIVE. + set (tmp := istep ge i sp rs2). + destruct i; simpl; try_simplify_someHyps; repeat (inversion_ASSERT || inversion_SOME b); try_simplify_someHyps; try congruence. + 1-3: explore_destruct; simpl; try_simplify_someHyps; repeat (inversion_ASSERT || inversion_SOME b); try_simplify_someHyps; try congruence. + (* Icond *) + unfold tmp; clear tmp; simpl. + intros EVAL; erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps. + destruct b eqn:EQb; simpl in * |-; try congruence. + intros; exploit exit_checker_eqlive; eauto. + intros (path & PATH & EQLIVE2). + repeat (econstructor; simpl; eauto). +Qed. + +Lemma ipath_checker_eqlive_normal ge ps (f:function) sp pm: forall alive pc res rs1 rs2 m st1, + eqlive_reg (ext alive) rs1 rs2 -> + ipath_checker ps f pm alive pc = Some res -> + isteps ge ps f sp rs1 m pc = Some st1 -> + icontinue st1 = true -> + exists st2, isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2. +Proof. + induction ps as [|ps]; simpl; try_simplify_someHyps. + - repeat (econstructor; simpl; eauto). + - inversion_SOME i; try_simplify_someHyps. + inversion_SOME res0. + inversion_SOME st0. + intros. + exploit iinst_checker_eqlive; eauto. + destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]). + try_simplify_someHyps. + rewrite <- CONT, <- MEM, <- PC. + destruct (icontinue st0) eqn:CONT'. + * intros; exploit iinst_checker_istep_continue; eauto. + rewrite <- PC; intros X; rewrite X in * |-. eauto. + * try_simplify_someHyps. + congruence. +Qed. + +Lemma ipath_checker_isteps_continue ge ps (f:function) sp pm: forall alive pc res rs m st, + ipath_checker ps f pm alive pc = Some res -> + isteps ge ps f sp rs m pc = Some st -> + icontinue st = true -> + (snd res)=(ipc st). +Proof. + induction ps as [|ps]; simpl; try_simplify_someHyps. + inversion_SOME i; try_simplify_someHyps. + inversion_SOME res0. + inversion_SOME st0. + destruct (icontinue st0) eqn:CONT'. + - intros; exploit iinst_checker_istep_continue; eauto. + intros EQ; rewrite EQ in * |-; clear EQ; eauto. + - try_simplify_someHyps; congruence. +Qed. + +Lemma ipath_checker_eqlive_stopped ge ps (f:function) sp pm: forall alive pc res rs1 rs2 m st1, + eqlive_reg (ext alive) rs1 rs2 -> + ipath_checker ps f pm alive pc = Some res -> + isteps ge ps f sp rs1 m pc = Some st1 -> + icontinue st1 = false -> + exists path st2, pm!(ipc st1) = Some path /\ isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2. +Proof. + induction ps as [|ps]; simpl; try_simplify_someHyps; try congruence. + inversion_SOME i; try_simplify_someHyps. + inversion_SOME res0. + inversion_SOME st0. + intros. + destruct (icontinue st0) eqn:CONT'; try_simplify_someHyps; intros. + * intros; exploit iinst_checker_eqlive; eauto. + destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]). + exploit iinst_checker_istep_continue; eauto. + intros PC'. + try_simplify_someHyps. + rewrite PC', <- CONT, <- MEM, <- PC, CONT'. + eauto. + * intros; exploit iinst_checker_eqlive_stopped; eauto. + intros EQLIVE; generalize EQLIVE; destruct 1 as (path & st2 & PATH & ISTEP & [CONT PC RS MEM]). + try_simplify_someHyps. + rewrite <- CONT, <- MEM, <- PC, CONT'. + try_simplify_someHyps. +Qed. + +Inductive eqlive_stackframes: stackframe -> stackframe -> Prop := + | eqlive_stackframes_intro path res f sp pc rs1 rs2 + (LIVE: liveness_ok_function f) + (PATH: f.(fn_path)!pc = Some path) + (EQUIV: forall v, eqlive_reg (ext path.(input_regs)) (rs1 # res <- v) (rs2 # res <- v)): + eqlive_stackframes (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2). + +Inductive eqlive_states: state -> state -> Prop := + | eqlive_states_intro + path st1 st2 f sp pc rs1 rs2 m + (STACKS: list_forall2 eqlive_stackframes st1 st2) + (LIVE: liveness_ok_function f) + (PATH: f.(fn_path)!pc = Some path) + (EQUIV: eqlive_reg (ext path.(input_regs)) rs1 rs2): + eqlive_states (State st1 f sp pc rs1 m) (State st2 f sp pc rs2 m) + | eqlive_states_call st1 st2 f args m + (LIVE: liveness_ok_fundef f) + (STACKS: list_forall2 eqlive_stackframes st1 st2): + eqlive_states (Callstate st1 f args m) (Callstate st2 f args m) + | eqlive_states_return st1 st2 v m + (STACKS: list_forall2 eqlive_stackframes st1 st2): + eqlive_states (Returnstate st1 v m) (Returnstate st2 v m). + + +Section LivenessProperties. + +Variable prog: program. + +Let pge := Genv.globalenv prog. +Let ge := Genv.globalenv (RTLpath.transf_program prog). + +Hypothesis all_fundef_liveness_ok: forall b f, + Genv.find_funct_ptr pge b = Some f -> + liveness_ok_fundef f. + +Lemma find_funct_liveness_ok v fd: + Genv.find_funct pge v = Some fd -> liveness_ok_fundef fd. +Proof. + unfold Genv.find_funct. + destruct v; try congruence. + destruct (Integers.Ptrofs.eq_dec _ _); try congruence. + eapply all_fundef_liveness_ok; eauto. +Qed. + +Lemma find_function_liveness_ok ros rs f: + find_function pge ros rs = Some f -> liveness_ok_fundef f. +Proof. + destruct ros as [r|i]; simpl. + - intros; eapply find_funct_liveness_ok; eauto. + - destruct (Genv.find_symbol pge i); try congruence. + eapply all_fundef_liveness_ok; eauto. +Qed. + +Lemma find_function_eqlive alive ros rs1 rs2: + eqlive_reg (ext alive) rs1 rs2 -> + reg_sum_mem ros alive = true -> + find_function pge ros rs1 = find_function pge ros rs2. +Proof. + intros EQLIVE. + destruct ros; simpl; auto. + intros H; erewrite (EQLIVE r); eauto. +Qed. + +Lemma inst_checker_from_iinst_checker i sp rs m st pm alive: + istep ge i sp rs m = Some st -> + inst_checker pm alive i = (SOME res <- iinst_checker pm alive i IN exit_checker pm (fst res) (snd res) tt). +Proof. + destruct i; simpl; try congruence. +Qed. + +Lemma exit_checker_eqlive_ext1 (pm: path_map) (alive: Regset.t) (pc: node) r rs1 rs2: + exit_checker pm (Regset.add r alive) pc tt = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists path, pm!pc = Some path /\ (forall v, eqlive_reg (ext path.(input_regs)) (rs1 # r <- v) (rs2 # r <- v)). +Proof. + unfold exit_checker. + inversion_SOME path. + inversion_ASSERT. try_simplify_someHyps. + repeat (econstructor; eauto). + intros; eapply eqlive_reg_update; eauto. + eapply eqlive_reg_monotonic; eauto. + intros r0 [X1 X2]; exploit Regset.subset_2; eauto. + rewrite regset_add_spec. intuition subst. +Qed. + +Local Hint Resolve in_or_app: local. +Lemma eqlive_eval_builtin_args alive rs1 rs2 sp m args vargs: + eqlive_reg alive rs1 rs2 -> + Events.eval_builtin_args ge (fun r => rs1 # r) sp m args vargs -> + (forall r, List.In r (params_of_builtin_args args) -> alive r) -> + Events.eval_builtin_args ge (fun r => rs2 # r) sp m args vargs. +Proof. + unfold Events.eval_builtin_args. + intros EQLIVE; induction 1 as [|a1 al b1 bl EVAL1 EVALL]; simpl. + { econstructor; eauto. } + intro X. + assert (X1: eqlive_reg (fun r => In r (params_of_builtin_arg a1)) rs1 rs2). + { eapply eqlive_reg_monotonic; eauto with local. } + lapply IHEVALL; eauto with local. + clear X IHEVALL; intro X. econstructor; eauto. + generalize X1; clear EVALL X1 X. + induction EVAL1; simpl; try (econstructor; eauto; fail). + - intros X1; erewrite X1; [ econstructor; eauto | eauto ]. + - intros; econstructor. + + eapply IHEVAL1_1; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + + eapply IHEVAL1_2; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + - intros; econstructor. + + eapply IHEVAL1_1; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + + eapply IHEVAL1_2; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. +Qed. + +Lemma exit_checker_eqlive_builtin_res (pm: path_map) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg): + exit_checker pm (reg_builtin_res res alive) pc tt = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists path, pm!pc = Some path /\ (forall vres, eqlive_reg (ext path.(input_regs)) (regmap_setres res vres rs1) (regmap_setres res vres rs2)). +Proof. + destruct res; simpl. + - intros; exploit exit_checker_eqlive_ext1; eauto. + - intros; exploit exit_checker_eqlive; eauto. + intros (path & PATH & EQLIVE). + eexists; intuition eauto. + - intros; exploit exit_checker_eqlive; eauto. + intros (path & PATH & EQLIVE). + eexists; intuition eauto. +Qed. + +Lemma exit_list_checker_eqlive (pm: path_map) (alive: Regset.t) (tbl: list node) rs1 rs2 pc: forall n, + exit_list_checker pm alive tbl = true -> + eqlive_reg (ext alive) rs1 rs2 -> + list_nth_z tbl n = Some pc -> + exists path, pm!pc = Some path /\ eqlive_reg (ext path.(input_regs)) rs1 rs2. +Proof. + induction tbl; simpl. + - intros; try congruence. + - intros n; rewrite lazy_and_Some_tt_true; destruct (zeq n 0) eqn: Hn. + * try_simplify_someHyps; intuition. + exploit exit_checker_eqlive; eauto. + * intuition. eapply IHtbl; eauto. +Qed. + +Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1: + list_forall2 eqlive_stackframes stk1 stk2 -> + eqlive_reg (ext alive) rs1 rs2 -> + liveness_ok_function f -> + (fn_code f) ! pc = Some i -> + path_last_step ge pge stk1 f sp pc rs1 m t s1 -> + inst_checker (fn_path f) alive i = Some tt -> + exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2. +Proof. + intros STACKS EQLIVE LIVENESS PC; + destruct 1 as [i' sp pc rs1 m st1| + sp pc rs1 m sig ros args res pc' fd| + st1 pc rs1 m sig ros args fd m'| + sp pc rs1 m ef args res pc' vargs t vres m'| + sp pc rs1 m arg tbl n pc' | + st1 pc rs1 m optr m']; + try_simplify_someHyps. + + (* istate *) + intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto. + inversion_SOME res. + intros. + destruct (icontinue st1) eqn: CONT. + - (* CONT => true *) + exploit iinst_checker_eqlive; eauto. + destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]). + repeat (econstructor; simpl; eauto). + rewrite <- MEM, <- PC2. + exploit exit_checker_eqlive; eauto. + intros (path & PATH & EQLIVE2). + eapply eqlive_states_intro; eauto. + erewrite <- iinst_checker_istep_continue; eauto. + - (* CONT => false *) + intros; exploit iinst_checker_eqlive_stopped; eauto. + destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]). + repeat (econstructor; simpl; eauto). + rewrite <- MEM, <- PC2. + eapply eqlive_states_intro; eauto. + + (* Icall *) + repeat inversion_ASSERT. intros. + exploit exit_checker_eqlive_ext1; eauto. + intros (path & PATH & EQLIVE2). + eexists; split. + - eapply exec_Icall; eauto. + erewrite <- find_function_eqlive; eauto. + - erewrite eqlive_reg_listmem; eauto. + eapply eqlive_states_call; eauto. + eapply find_function_liveness_ok; eauto. + repeat (econstructor; eauto). + + (* Itailcall *) + repeat inversion_ASSERT. intros. + eexists; split. + - eapply exec_Itailcall; eauto. + erewrite <- find_function_eqlive; eauto. + - erewrite eqlive_reg_listmem; eauto. + eapply eqlive_states_call; eauto. + eapply find_function_liveness_ok; eauto. + + (* Ibuiltin *) + repeat inversion_ASSERT. intros. + exploit exit_checker_eqlive_builtin_res; eauto. + intros (path & PATH & EQLIVE2). + eexists; split. + - eapply exec_Ibuiltin; eauto. + eapply eqlive_eval_builtin_args; eauto. + intros; eapply list_mem_correct; eauto. + - repeat (econstructor; simpl; eauto). + + (* Ijumptable *) + repeat inversion_ASSERT. intros. + exploit exit_list_checker_eqlive; eauto. + intros (path & PATH & EQLIVE2). + eexists; split. + - eapply exec_Ijumptable; eauto. + erewrite <- EQLIVE; eauto. + - repeat (econstructor; simpl; eauto). + + (* Ireturn *) + repeat inversion_ASSERT. intros. + eexists; split. + - eapply exec_Ireturn; eauto. + - destruct optr; simpl in * |- *. + * erewrite (EQLIVE r); eauto. + eapply eqlive_states_return; eauto. + * eapply eqlive_states_return; eauto. +Qed. + +Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2: + path_step ge pge (psize path) stk1 f sp rs1 m pc t s1 -> + list_forall2 eqlive_stackframes stk1 stk2 -> + eqlive_reg (ext (input_regs path)) rs1 rs2 -> + liveness_ok_function f -> + (fn_path f) ! pc = Some path -> + exists s2, path_step ge pge (psize path) stk2 f sp rs2 m pc t s2 /\ eqlive_states s1 s2. +Proof. + intros STEP STACKS EQLIVE LIVE PC. + unfold liveness_ok_function in LIVE. + exploit LIVE; eauto. + unfold path_checker. + inversion_SOME res; (* destruct res as [alive pc']. *) intros ICHECK. (* simpl. *) + inversion_SOME i; intros PC'. + destruct STEP as [st ISTEPS CONT|]. + - (* early_exit *) + intros; exploit ipath_checker_eqlive_stopped; eauto. + destruct 1 as (path2 & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]). + repeat (econstructor; simpl; eauto). + rewrite <- MEM, <- PC2. + eapply eqlive_states_intro; eauto. + - (* normal_exit *) + intros; exploit ipath_checker_eqlive_normal; eauto. + destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]). + exploit ipath_checker_isteps_continue; eauto. + intros PC3; rewrite <- PC3, <- PC2 in * |-. + exploit inst_checker_eqlive; eauto. + intros (s2 & LAST_STEP & EQLIVE2). + eexists; split; eauto. + eapply exec_normal_exit; eauto. + rewrite <- PC3, <- MEM; auto. +Qed. + +Theorem step_eqlive t s1 s1' s2: + step ge pge s1 t s1' -> + eqlive_states s1 s2 -> + exists s2', step ge pge s2 t s2' /\ eqlive_states s1' s2'. +Proof. + destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ]. + - intros EQLIVE; inv EQLIVE; simplify_someHyps. + intro PATH. + exploit path_step_eqlive; eauto. + intros (s2 & STEP2 & EQUIV2). + eexists; split; eauto. + eapply exec_path; eauto. + - intros EQLIVE; inv EQLIVE; inv LIVE. + exploit initialize_path. { eapply fn_entry_point_wf. } + intros (path & Hpath). + eexists; split. + * eapply exec_function_internal; eauto. + * eapply eqlive_states_intro; eauto. + eapply eqlive_reg_refl. + - intros EQLIVE; inv EQLIVE. + eexists; split. + * eapply exec_function_external; eauto. + * eapply eqlive_states_return; eauto. + - intros EQLIVE; inv EQLIVE. + inversion STACKS as [|s1 st1 s' s2 STACK STACKS']; subst; clear STACKS. + inv STACK. + exists (State s2 f sp pc (rs2 # res <- vres) m); split. + * apply exec_return. + * eapply eqlive_states_intro; eauto. +Qed. + +End LivenessProperties. diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v new file mode 100644 index 00000000..b0dcbe80 --- /dev/null +++ b/kvx/lib/RTLpathSE_theory.v @@ -0,0 +1,1336 @@ +(* A theory of symbolic execution on RTLpath + +NB: an efficient implementation with hash-consing will be defined in ... + +*) + +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL RTLpath. + +(* NOTE for the implementation of the symbolic execution. + It is important to remove dependency of Op on memory. + Here is an way to formalize this + +Parameter mem_irrel: operation -> bool. +Hypothesis eval_operation_mem_irrel: forall (ge: RTL.genv) sp o args m1 m2, mem_irrel o = true -> eval_operation ge sp o args m1 = eval_operation ge sp o args m2. + +*) + +(** * Syntax and semantics of symbolic values *) + +(* FIXME - might have to add non trapping loads *) +(* symbolic value *) +Inductive sval := + | Sinput (r: reg) + | Sop (op:operation) (lsv: list_sval) (sm: smem) (* TODO for the implementation: add an additionnal case without dependency on sm*) + | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) +with list_sval := + | Snil + | Scons (sv: sval) (lsv: list_sval) +(* symbolic memory *) +with smem := + | Sinit + | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval). + +Scheme sval_mut := Induction for sval Sort Prop +with list_sval_mut := Induction for list_sval Sort Prop +with smem_mut := Induction for smem Sort Prop. + +Fixpoint list_sval_inj (l: list sval): list_sval := + match l with + | nil => Snil + | v::l => Scons v (list_sval_inj l) + end. + +Local Open Scope option_monad_scope. + +Fixpoint seval_sval (ge: RTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): option val := + match sv with + | Sinput r => Some (rs0#r) + | Sop op l sm => + SOME args <- seval_list_sval ge sp l rs0 m0 IN + SOME m <- seval_smem ge sp sm rs0 m0 IN + eval_operation ge sp op args m + | Sload sm trap chunk addr lsv => + match trap with + | TRAP => + SOME args <- seval_list_sval ge sp lsv rs0 m0 IN + SOME a <- eval_addressing ge sp addr args IN + SOME m <- seval_smem ge sp sm rs0 m0 IN + Mem.loadv chunk m a + | NOTRAP => + SOME args <- seval_list_sval ge sp lsv rs0 m0 IN + match (eval_addressing ge sp addr args) with + | None => Some (default_notrap_load_value chunk) + | Some a => + SOME m <- seval_smem ge sp sm rs0 m0 IN + match (Mem.loadv chunk m a) with + | None => Some (default_notrap_load_value chunk) + | Some val => Some val + end + end + end + end +with seval_list_sval (ge: RTL.genv) (sp:val) (lsv: list_sval) (rs0: regset) (m0: mem): option (list val) := + match lsv with + | Snil => Some nil + | Scons sv lsv' => + SOME v <- seval_sval ge sp sv rs0 m0 IN + SOME lv <- seval_list_sval ge sp lsv' rs0 m0 IN + Some (v::lv) + end +with seval_smem (ge: RTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): option mem := + match sm with + | Sinit => Some m0 + | Sstore sm chunk addr lsv srce => + SOME args <- seval_list_sval ge sp lsv rs0 m0 IN + SOME a <- eval_addressing ge sp addr args IN + SOME m <- seval_smem ge sp sm rs0 m0 IN + SOME sv <- seval_sval ge sp srce rs0 m0 IN + Mem.storev chunk m a sv + end. + +(* Syntax and Semantics of local symbolic internal states *) +(* [si_pre] is a precondition on initial ge, sp, rs0, m0 *) +Record sistate_local := { si_pre: RTL.genv -> val -> regset -> mem -> Prop; si_sreg: reg -> sval; si_smem: smem }. + +(* Predicate on which (rs, m) is a possible final state after evaluating [st] on (rs0, m0) *) +Definition ssem_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop := + st.(si_pre) ge sp rs0 m0 + /\ seval_smem ge sp st.(si_smem) rs0 m0 = Some m + /\ forall (r:reg), seval_sval ge sp (st.(si_sreg) r) rs0 m0 = Some (rs#r). + +Definition sabort_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem): Prop := + ~(st.(si_pre) ge sp rs0 m0) + \/ seval_smem ge sp st.(si_smem) rs0 m0 = None + \/ exists (r: reg), seval_sval ge sp (st.(si_sreg) r) rs0 m0 = None. + +(* Syntax and semantics of symbolic exit states *) +Record sistate_exit := mk_sistate_exit + { si_cond: condition; si_scondargs: list_sval; si_elocal: sistate_local; si_ifso: node }. + +Definition seval_condition ge sp (cond: condition) (lsv: list_sval) (sm: smem) rs0 m0 : option bool := + SOME args <- seval_list_sval ge sp lsv rs0 m0 IN + SOME m <- seval_smem ge sp sm rs0 m0 IN + eval_condition cond args m. + +Definition all_fallthrough ge sp (lx: list sistate_exit) rs0 m0: Prop := + forall ext, List.In ext lx -> + seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some false. + +(** Semantic of an exit in pseudo code: + if si_cond (si_condargs) + si_elocal; goto if_so + else () +*) + +Definition ssem_exit (ge: RTL.genv) (sp: val) (ext: sistate_exit) (rs: regset) (m: mem) rs' m' (pc': node) : Prop := + seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = Some true + /\ ssem_local ge sp (si_elocal ext) rs m rs' m' + /\ (si_ifso ext) = pc'. + +(* Either an abort on the condition evaluation OR an abort on the sistate_local IF the condition was true *) +Definition sabort_exit (ge: RTL.genv) (sp: val) (ext: sistate_exit) (rs: regset) (m: mem) : Prop := + let sev_cond := seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m in + sev_cond = None + \/ (sev_cond = Some true /\ sabort_local ge sp ext.(si_elocal) rs m). + +(** * Syntax and Semantics of symbolic internal state *) +Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. + +Definition all_fallthrough_upto_exit ge sp ext lx' lx rs m : Prop := + is_tail (ext::lx') lx /\ all_fallthrough ge sp lx' rs m. + +(** Semantic of a sistate in pseudo code: + si_exit1; si_exit2; ...; si_exitn; + si_local; goto si_pc *) + +(* Note: in RTLpath, is.(icontinue) = false iff we took an early exit *) + +Definition ssem (ge: RTL.genv) (sp:val) (st: sistate) (rs: regset) (m: mem) (is: istate): Prop := + if (is.(icontinue)) + then + ssem_local ge sp st.(si_local) rs m is.(irs) is.(imem) + /\ st.(si_pc) = is.(ipc) + /\ all_fallthrough ge sp st.(si_exits) rs m + else exists ext lx, + ssem_exit ge sp ext rs m is.(irs) is.(imem) is.(ipc) + /\ all_fallthrough_upto_exit ge sp ext lx st.(si_exits) rs m. + +Definition sabort (ge: RTL.genv) (sp: val) (st: sistate) (rs: regset) (m: mem): Prop := + (* No early exit was met but we aborted on the si_local *) + (all_fallthrough ge sp st.(si_exits) rs m /\ sabort_local ge sp st.(si_local) rs m) + (* OR we aborted on an evaluation of one of the early exits *) + \/ (exists ext lx, all_fallthrough_upto_exit ge sp ext lx st.(si_exits) rs m /\ sabort_exit ge sp ext rs m). + +Definition ssem_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop := + match ois with + | Some is => ssem ge sp st rs0 m0 is + | None => sabort ge sp st rs0 m0 + end. + +Definition ssem_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop := + match ost with + | Some st => ssem_opt ge sp st rs0 m0 ois + | None => ois=None + end. + +(** * An internal state represents a parallel program ! + + We prove below that the semantics [ssem_opt] is deterministic. + + *) + +Definition istate_eq ist1 ist2 := + ist1.(icontinue) = ist2.(icontinue) /\ + ist1.(ipc) = ist2.(ipc) /\ + (forall r, (ist1.(irs)#r) = ist2.(irs)#r) /\ + ist1.(imem) = ist2.(imem). + +Lemma all_fallthrough_noexit ge sp ext lx rs0 m0 rs m pc: + ssem_exit ge sp ext rs0 m0 rs m pc -> + In ext lx -> + all_fallthrough ge sp lx rs0 m0 -> + False. +Proof. + Local Hint Resolve is_tail_in: core. + intros SSEM INE ALLF. + destruct SSEM as (SSEM & SSEM'). + unfold all_fallthrough in ALLF. rewrite ALLF in SSEM; eauto. + discriminate. +Qed. + +Lemma ssem_exclude_incompatible_continue ge sp st rs m is1 is2: + is1.(icontinue) = true -> + is2.(icontinue) = false -> + ssem ge sp st rs m is1 -> + ssem ge sp st rs m is2 -> + False. +Proof. + Local Hint Resolve all_fallthrough_noexit: core. + unfold ssem. + intros CONT1 CONT2. + rewrite CONT1, CONT2; simpl. + intuition eauto. + destruct H0 as (ext & lx & SSEME & ALLFU). + destruct ALLFU as (ALLFU & ALLFU'). + eapply all_fallthrough_noexit; eauto. +Qed. + +Lemma ssem_determ_continue ge sp st rs m is1 is2: + ssem ge sp st rs m is1 -> + ssem ge sp st rs m is2 -> + is1.(icontinue) = is2.(icontinue). +Proof. + Local Hint Resolve ssem_exclude_incompatible_continue: core. + destruct (Bool.bool_dec is1.(icontinue) is2.(icontinue)) as [|H]; auto. + intros H1 H2. assert (absurd: False); intuition. + destruct (icontinue is1) eqn: His1, (icontinue is2) eqn: His2; eauto. +Qed. + +Lemma ssem_local_determ ge sp st rs0 m0 rs1 m1 rs2 m2: + ssem_local ge sp st rs0 m0 rs1 m1 -> + ssem_local ge sp st rs0 m0 rs2 m2 -> + (forall r, rs1#r = rs2#r) /\ m1 = m2. +Proof. + unfold ssem_local. intuition try congruence. + generalize (H5 r); rewrite H4; congruence. +Qed. + +(* TODO: lemma to move in Coqlib *) +Lemma is_tail_bounded_total {A} (l1 l2 l3: list A): is_tail l1 l3 -> is_tail l2 l3 + -> is_tail l1 l2 \/ is_tail l2 l1. +Proof. + Local Hint Resolve is_tail_cons: core. + induction 1 as [|i l1 l3 T1 IND]; simpl; auto. + intros T2; inversion T2; subst; auto. +Qed. + +Lemma exit_cond_determ ge sp rs0 m0 l1 l2: + is_tail l1 l2 -> forall ext1 lx1 ext2 lx2, + l1=(ext1 :: lx1) -> + l2=(ext2 :: lx2) -> + all_fallthrough ge sp lx1 rs0 m0 -> + seval_condition ge sp (si_cond ext1) (si_scondargs ext1) (si_smem (si_elocal ext1)) rs0 m0 = Some true -> + all_fallthrough ge sp lx2 rs0 m0 -> + ext1=ext2. +Proof. + destruct 1 as [l1|i l1 l3 T1]; intros ext1 lx1 ext2 lx2 EQ1 EQ2; subst; + inversion EQ2; subst; auto. + intros D1 EVAL NYE. + Local Hint Resolve is_tail_in: core. + unfold all_fallthrough in NYE. + rewrite NYE in EVAL; eauto. + try congruence. +Qed. + +Lemma ssem_exit_determ ge sp ext rs0 m0 rs1 m1 pc1 rs2 m2 pc2: + ssem_exit ge sp ext rs0 m0 rs1 m1 pc1 -> + ssem_exit ge sp ext rs0 m0 rs2 m2 pc2 -> + pc1 = pc2 /\ (forall r, rs1#r = rs2#r) /\ m1 = m2. +Proof. + Local Hint Resolve exit_cond_determ eq_sym: core. + intros SSEM1 SSEM2. destruct SSEM1 as (SEVAL1 & SLOC1 & PCEQ1). destruct SSEM2 as (SEVAL2 & SLOC2 & PCEQ2). subst. + destruct (ssem_local_determ ge sp (si_elocal ext) rs0 m0 rs1 m1 rs2 m2); auto. +Qed. + +Remark is_tail_inv_left {A: Type} (a a': A) l l': + is_tail (a::l) (a'::l') -> + (a = a' /\ l = l') \/ (In a l' /\ is_tail l (a'::l')). +Proof. + intros. inv H. + - left. eauto. + - right. econstructor. + + eapply is_tail_in; eauto. + + eapply is_tail_cons_left; eauto. +Qed. + +Lemma ssem_determ ge sp st rs m is1 is2: + ssem ge sp st rs m is1 -> + ssem ge sp st rs m is2 -> + istate_eq is1 is2. +Proof. + unfold istate_eq. + intros SEM1 SEM2. + exploit (ssem_determ_continue ge sp st rs m is1 is2); eauto. + intros CONTEQ. unfold ssem in * |-. rewrite CONTEQ in * |- *. + destruct (icontinue is2). + - destruct (ssem_local_determ ge sp (si_local st) rs m (irs is1) (imem is1) (irs is2) (imem is2)); + intuition (try congruence). + - destruct SEM1 as (ext1 & lx1 & SSEME1 & ALLFU1). destruct SEM2 as (ext2 & lx2 & SSEME2 & ALLFU2). + destruct ALLFU1 as (ALLFU1 & ALLFU1'). destruct ALLFU2 as (ALLFU2 & ALLFU2'). + destruct SSEME1 as (SSEME1 & SSEME1' & SSEME1''). destruct SSEME2 as (SSEME2 & SSEME2' & SSEME2''). + assert (X:ext1=ext2). + { destruct (is_tail_bounded_total (ext1 :: lx1) (ext2 :: lx2) (si_exits st)) as [TAIL|TAIL]; eauto. } + subst. destruct (ssem_local_determ ge sp (si_elocal ext2) rs m (irs is1) (imem is1) (irs is2) (imem is2)); auto. + intuition. congruence. +Qed. + +Lemma ssem_local_exclude_sabort_local ge sp loc rs m rs' m': + ssem_local ge sp loc rs m rs' m' -> +(* all_fallthrough ge sp (si_exits st) rs m -> *) + sabort_local ge sp loc rs m -> + False. +Proof. + intros SIML (* ALLF *) ABORT. inv SIML. destruct H0 as (H0 & H0'). + inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. +Qed. + +Lemma ssem_local_exclude_sabort_exit ge sp st ext lx rs m rs' m': + ssem_local ge sp (si_local st) rs m rs' m' -> + all_fallthrough ge sp (si_exits st) rs m -> + is_tail (ext :: lx) (si_exits st) -> + sabort_exit ge sp ext rs m -> + False. +Proof. + intros SSEML ALLF TAIL ABORT. + inv ABORT. + - exploit ALLF; eauto. congruence. + - (* FIXME Problem : if we have a ssem_local, this means we ONLY evaluated the conditions, + but we NEVER actually evaluated the si_elocal from the sistate_exit ! So we cannot prove + a lack of abort on the si_elocal.. We must change the definitions *) +Abort. + +Lemma ssem_local_exclude_sabort ge sp st rs m rs' m': + ssem_local ge sp (si_local st) rs m rs' m' -> + all_fallthrough ge sp (si_exits st) rs m -> + sabort ge sp st rs m -> + False. +Proof. + intros SIML ALLF ABORT. + inv ABORT. + - intuition; eapply ssem_local_exclude_sabort_local; eauto. + - destruct H as (ext & lx & ALLFU & SABORT). + destruct ALLFU as (TAIL & _). eapply is_tail_in in TAIL. + eapply ALLF in TAIL. + destruct SABORT as [CONDFAIL | (CONDTRUE & ABORTL)]; congruence. +Qed. + +Lemma ssem_exit_fallthrough_upto_exit ge sp ext ext' lx lx' exits rs m rs' m' pc': + ssem_exit ge sp ext rs m rs' m' pc' -> + all_fallthrough_upto_exit ge sp ext lx exits rs m -> + all_fallthrough_upto_exit ge sp ext' lx' exits rs m -> + is_tail (ext'::lx') (ext::lx). +Proof. + intros SSEME ALLFU ALLFU'. + destruct ALLFU as (ISTAIL & ALLFU). destruct ALLFU' as (ISTAIL' & ALLFU'). + destruct (is_tail_bounded_total (ext::lx) (ext'::lx') exits); eauto. + inv H. + - econstructor; eauto. + - eapply is_tail_in in H2. eapply ALLFU' in H2. + destruct SSEME as (SEVAL & _). congruence. +Qed. + +Lemma ssem_exit_exclude_sabort_exit ge sp ext rs m rs' m' pc': + ssem_exit ge sp ext rs m rs' m' pc' -> + sabort_exit ge sp ext rs m -> + False. +Proof. + intros A B. destruct A as (A & A' & A''). inv B. + - congruence. + - destruct H as (_ & H). eapply ssem_local_exclude_sabort_local; eauto. +Qed. + +Lemma ssem_exit_exclude_sabort ge sp ext st lx rs m rs' m' pc': + ssem_exit ge sp ext rs m rs' m' pc' -> + all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs m -> + sabort ge sp st rs m -> + False. +Proof. + intros SSEM ALLFU ABORT. + inv ABORT. + - destruct H as (ALLF & _). destruct ALLFU as (TAIL & _). + eapply is_tail_in in TAIL. + destruct SSEM as (SEVAL & _ & _). + eapply ALLF in TAIL. congruence. + - destruct H as (ext' & lx' & ALLFU' & ABORT). + exploit ssem_exit_fallthrough_upto_exit; eauto. intros ITAIL. + destruct ALLFU as (ALLFU1 & ALLFU2). destruct ALLFU' as (ALLFU1' & ALLFU2'). + exploit (is_tail_inv_left ext' ext lx' lx); eauto. intro. inv H. + + inv H0. eapply ssem_exit_exclude_sabort_exit; eauto. + + destruct H0 as (INE & TAIL). eapply ALLFU2 in INE. destruct ABORT as [ABORT | (ABORT & ABORT')]; congruence. +Qed. + +Lemma ssem_exclude_sabort ge sp st rs m is: + sabort ge sp st rs m -> + ssem ge sp st rs m is -> False. +Proof. + intros ABORT SEM. + unfold ssem in SEM. destruct icontinue. + - destruct SEM as (SEM1 & SEM2 & SEM3). + eapply ssem_local_exclude_sabort; eauto. + - destruct SEM as (ext & lx & SEM1 & SEM2). eapply ssem_exit_exclude_sabort; eauto. +Qed. + +Definition istate_eq_opt ist1 oist := + exists ist2, oist = Some ist2 /\ istate_eq ist1 ist2. + +Lemma ssem_opt_determ ge sp st rs m ois is: + ssem_opt ge sp st rs m ois -> + ssem ge sp st rs m is -> + istate_eq_opt is ois. +Proof. + destruct ois as [is1|]; simpl; eauto. + - intros; eexists; intuition; eapply ssem_determ; eauto. + - intros; exploit ssem_exclude_sabort; eauto. destruct 1. +Qed. + +(** * Symbolic execution of one internal step *) + +Definition slocal_set_sreg (st:sistate_local) (r:reg) (sv:sval) := + {| si_pre:=(fun ge sp rs m => seval_sval ge sp (st.(si_sreg) r) rs m <> None /\ (st.(si_pre) ge sp rs m)); + si_sreg:=fun y => if Pos.eq_dec r y then sv else st.(si_sreg) y; + si_smem:= st.(si_smem)|}. + +Definition slocal_set_smem (st:sistate_local) (sm:smem) := + {| si_pre:=(fun ge sp rs m => seval_smem ge sp st.(si_smem) rs m <> None /\ (st.(si_pre) ge sp rs m)); + si_sreg:= st.(si_sreg); + si_smem:= sm |}. + +Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): option sistate := + Some {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}. + + +Definition sistep (i: instruction) (st: sistate): option sistate := + match i with + | Inop pc' => + sist_set_local st pc' st.(si_local) + | Iop op args dst pc' => + let prev := st.(si_local) in + let vargs := list_sval_inj (List.map prev.(si_sreg) args) in + let next := slocal_set_sreg prev dst (Sop op vargs prev.(si_smem)) in + sist_set_local st pc' next + | Iload trap chunk addr args dst pc' => + let prev := st.(si_local) in + let vargs := list_sval_inj (List.map prev.(si_sreg) args) in + let next := slocal_set_sreg prev dst (Sload prev.(si_smem) trap chunk addr vargs) in + sist_set_local st pc' next + | Istore chunk addr args src pc' => + let prev := st.(si_local) in + let vargs := list_sval_inj (List.map prev.(si_sreg) args) in + let next := slocal_set_smem prev (Sstore prev.(si_smem) chunk addr vargs (prev.(si_sreg) src)) in + sist_set_local st pc' next + | Icond cond args ifso ifnot _ => + let prev := st.(si_local) in + let vargs := list_sval_inj (List.map prev.(si_sreg) args) in + let ex := {| si_cond:=cond; si_scondargs:=vargs; si_elocal := prev; si_ifso := ifso |} in + Some {| si_pc := ifnot; si_exits := ex::st.(si_exits); si_local := prev |} + | _ => None (* TODO jumptable ? *) + end. + + +Lemma seval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: + (forall r : reg, seval_sval ge sp (sreg r) rs0 m0 = Some (rs # r)) -> + seval_list_sval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l). +Proof. + intros H; induction l as [|r l]; simpl; auto. + inversion_SOME v. + inversion_SOME lv. + generalize (H r). + try_simplify_someHyps. +Qed. + +(* TODO - continue updating the rest *) + +Lemma slocal_set_sreg_preserves_sabort_local ge sp st rs0 m0 r sv: + sabort_local ge sp st rs0 m0 -> + sabort_local ge sp (slocal_set_sreg st r sv) rs0 m0. +Proof. + unfold sabort_local. simpl; intuition. + destruct H as [r1 H]. destruct (Pos.eq_dec r r1) as [TEST|TEST] eqn: HTEST. + - subst; rewrite H; intuition. + - right. right. exists r1. rewrite HTEST. auto. +Qed. + +Lemma slocal_set_smem_preserves_sabort_local ge sp st rs0 m0 m: + sabort_local ge sp st rs0 m0 -> + sabort_local ge sp (slocal_set_smem st m) rs0 m0. +Proof. + unfold sabort_local. simpl; intuition. +Qed. + +Lemma sist_set_local_preserves_sabort ge sp rs0 m0 st st' loc' pc': + sist_set_local st pc' loc' = Some st' -> + sabort ge sp st rs0 m0 -> + sabort ge sp st' rs0 m0. +Proof. + intros SSL ABORT. inv SSL. unfold sabort. simpl. + destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. + - +Abort. + +Lemma all_fallthrough_upto_exit_cons ge sp ext lx ext' exits rs m: + all_fallthrough_upto_exit ge sp ext lx exits rs m -> + all_fallthrough_upto_exit ge sp ext lx (ext'::exits) rs m. +Proof. + intros. inv H. econstructor; eauto. +Qed. + +Lemma all_fallthrough_cons ge sp exits rs m ext: + all_fallthrough ge sp exits rs m -> + seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs m = Some false -> + all_fallthrough ge sp (ext::exits) rs m. +Proof. + intros. unfold all_fallthrough in *. intros. + inv H1; eauto. +Qed. + +Lemma sistep_preserves_sabort i ge sp rs m st st': + sistep i st = Some st' -> + sabort ge sp st rs m -> sabort ge sp st' rs m. +Proof. + intros SISTEP ABORT. + destruct i; simpl in SISTEP; try discriminate; inv SISTEP; unfold sabort; simpl. + (* NOP *) + * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. + - left. constructor; eauto. + - right. exists ext0, lx0. constructor; eauto. + (* OP *) + * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. + - left. constructor; eauto. eapply slocal_set_sreg_preserves_sabort_local; eauto. + - right. exists ext0, lx0. constructor; eauto. + (* LOAD *) + * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. + - left. constructor; eauto. eapply slocal_set_sreg_preserves_sabort_local; eauto. + - right. exists ext0, lx0. constructor; eauto. + (* STORE *) + * destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. + - left. constructor; eauto. eapply slocal_set_smem_preserves_sabort_local; eauto. + - right. exists ext0, lx0. constructor; eauto. + (* COND *) + * remember ({| si_cond := _; si_scondargs := _; si_elocal := _; si_ifso := _ |}) as ext. + destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. + - destruct (seval_condition ge sp (si_cond ext) (si_scondargs ext) + (si_smem (si_elocal ext)) rs m) eqn:SEVAL; [destruct b|]. + (* case true *) + + right. exists ext, (si_exits st). + constructor. + ++ constructor. econstructor; eauto. eauto. + ++ unfold sabort_exit. right. constructor; eauto. + subst. simpl. eauto. + (* case false *) + + left. constructor; eauto. eapply all_fallthrough_cons; eauto. + (* case None *) + + right. exists ext, (si_exits st). constructor. + ++ constructor. econstructor; eauto. eauto. + ++ unfold sabort_exit. left. eauto. + - right. exists ext0, lx0. constructor; eauto. eapply all_fallthrough_upto_exit_cons; eauto. +Qed. + +Lemma sistep_WF i st: + sistep i st = None -> default_succ i = None. +Proof. + destruct i; simpl; unfold sist_set_local; simpl; congruence. +Qed. + +Lemma sistep_default_succ i st st': + sistep i st = Some st' -> default_succ i = Some (st'.(si_pc)). +Proof. + destruct i; simpl; unfold sist_set_local; simpl; try congruence; + intro H; inversion_clear H; simpl; auto. +Qed. + + +Lemma seval_list_sval_inj_not_none ge sp st rs0 m0 rs: forall l, + (forall r, List.In r l -> seval_sval ge sp (si_sreg (si_local st) r) rs0 m0 = Some rs # r) -> + seval_list_sval ge sp (list_sval_inj (map (si_sreg (si_local st)) l)) rs0 m0 = None -> + False. +Proof. + induction l. + - intros. simpl in H0. discriminate. + - intros ALLR. simpl. + inversion_SOME v. + + intro SVAL. inversion_SOME lv; [discriminate|]. + assert (forall r : reg, In r l -> seval_sval ge sp (si_sreg (si_local st) r) rs0 m0 = Some rs # r). + { intros r INR. eapply ALLR. right. assumption. } + intro SVALLIST. intro. eapply IHl; eauto. + + intros. exploit (ALLR a); [constructor; eauto|]. congruence. +Qed. + +Lemma sistep_correct ge sp i st rs0 m0 rs m: + ssem_local ge sp st.(si_local) rs0 m0 rs m -> + all_fallthrough ge sp st.(si_exits) rs0 m0 -> + ssem_opt2 ge sp (sistep i st) rs0 m0 (istep ge i sp rs m). +Proof. + intros (PRE & MEM & REG) NYE. + destruct i; simpl; auto. + + (* Nop *) + constructor; [|constructor]; simpl; auto. + constructor; auto. + + (* Op *) + inversion_SOME v; intros OP; simpl. + - constructor; [|constructor]; simpl; auto. + constructor; simpl; auto. + * constructor; auto. congruence. + * constructor; auto. + intro r0. destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. + subst. rewrite Regmap.gss; simpl; auto. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + - left. constructor; simpl; auto. + unfold sabort_local. right. right. + simpl. exists r. destruct (Pos.eq_dec r r); try congruence. + simpl. erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + + (* LOAD *) + inversion_SOME a0; intro ADD. + { inversion_SOME v; intros LOAD; simpl. + - explore_destruct; unfold ssem, ssem_local; simpl; intuition. + * unfold ssem. simpl. constructor; [|constructor]; auto. + constructor; constructor; simpl; auto. congruence. intro r0. + destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. + subst; rewrite Regmap.gss; simpl. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + * unfold ssem. simpl. constructor; [|constructor]; auto. + constructor; constructor; simpl; auto. congruence. intro r0. + destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. + subst; rewrite Regmap.gss; simpl. + inversion_SOME args; intros ARGS; [|exploit seval_list_sval_inj_not_none; eauto; contradiction]. + exploit seval_list_sval_inj; eauto. intro ARGS'. erewrite ARGS in ARGS'. inv ARGS'. rewrite ADD. + inversion_SOME m2. intro SMEM. + assert (m = m2) by congruence. subst. rewrite LOAD. reflexivity. + - explore_destruct; unfold sabort, sabort_local; simpl. + * unfold sabort. simpl. left. constructor; auto. + right. right. exists r. simpl. destruct (Pos.eq_dec r r); try congruence. + simpl. erewrite seval_list_sval_inj; simpl; auto. + rewrite ADD; simpl; auto. try_simplify_someHyps. + * unfold ssem. simpl. constructor; [|constructor]; auto. + constructor; constructor; simpl; auto. congruence. intro r0. + destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. + subst; rewrite Regmap.gss; simpl. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. intros SMEM SEVAL. + rewrite LOAD. reflexivity. + } { rewrite ADD. destruct t. + - simpl. left; eauto. simpl. econstructor; eauto. + right. right. simpl. exists r. destruct (Pos.eq_dec r r); [|contradiction]. + simpl. inversion_SOME args. intro SLS. + eapply seval_list_sval_inj in REG. rewrite REG in SLS. inv SLS. + rewrite ADD. reflexivity. + - simpl. constructor; [|constructor]; simpl; auto. + constructor; simpl; constructor; auto; [congruence|]. + intro r0. destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. + subst. simpl. rewrite Regmap.gss. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. intro SMEM. rewrite ADD. reflexivity. + } + + (* STORE *) + inversion_SOME a0; intros ADD. + { inversion_SOME m'; intros STORE; simpl. + - unfold ssem, ssem_local; simpl; intuition. + * congruence. + * erewrite seval_list_sval_inj; simpl; auto. + erewrite REG. + try_simplify_someHyps. + - unfold sabort, sabort_local; simpl. + left. constructor; auto. right. left. + erewrite seval_list_sval_inj; simpl; auto. + erewrite REG. + try_simplify_someHyps. } + { unfold sabort, sabort_local; simpl. + left. constructor; auto. right. left. + erewrite seval_list_sval_inj; simpl; auto. + erewrite ADD; simpl; auto. } + + (* COND *) + Local Hint Resolve is_tail_refl: core. + Local Hint Unfold ssem_local: core. + inversion_SOME b; intros COND. + { destruct b; simpl; unfold ssem, ssem_local; simpl. + - remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st). + constructor; constructor; subst; simpl; auto. + unfold seval_condition. subst; simpl. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + - intuition. unfold all_fallthrough in * |- *. simpl. + intuition. subst. simpl. + unfold seval_condition. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. } + { unfold sabort. simpl. right. + remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st). + constructor; [constructor; subst; simpl; auto|]. + left. subst; simpl; auto. + unfold seval_condition. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. } +Qed. + + +Lemma sistep_correct_None ge sp i st rs0 m0 rs m: + ssem_local ge sp (st.(si_local)) rs0 m0 rs m -> + sistep i st = None -> + istep ge i sp rs m = None. +Proof. + intros (PRE & MEM & REG). + destruct i; simpl; unfold sist_set_local, ssem, ssem_local; simpl; try_simplify_someHyps. +Qed. + +(** * Symbolic execution of the internal steps of a path *) +Fixpoint sisteps (path:nat) (f: function) (st: sistate): option sistate := + match path with + | O => Some st + | S p => + SOME i <- (fn_code f)!(st.(si_pc)) IN + SOME st1 <- sistep i st IN + sisteps p f st1 + end. + +Lemma sist_set_local_preserves_si_exits st pc loc st': + sist_set_local st pc loc = Some st' -> + si_exits st' = si_exits st. +Proof. + intros. inv H. simpl. reflexivity. +Qed. + +Lemma sistep_preserves_allfu ge sp ext lx rs0 m0 st st' i: + all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs0 m0 -> + sistep i st = Some st' -> + all_fallthrough_upto_exit ge sp ext lx (si_exits st') rs0 m0. +Proof. + intros ALLFU SISTEP. destruct ALLFU as (ISTAIL & ALLF). + constructor; eauto. + destruct i; try discriminate; simpl in SISTEP; try (erewrite sist_set_local_preserves_si_exits; eauto; fail). + inv SISTEP. simpl. constructor. assumption. +Qed. + +Lemma sisteps_correct_false ge sp f rs0 m0 st' is: + forall path, + is.(icontinue)=false -> + forall st, ssem ge sp st rs0 m0 is -> + sisteps path f st = Some st' -> + ssem ge sp st' rs0 m0 is. +Proof. + induction path; simpl. + - intros. congruence. + - intros ICF st SSEM STEQ'. + destruct ((fn_code f) ! (si_pc st)) eqn:FIC; [|discriminate]. + destruct (sistep _ _) eqn:SISTEP; [|discriminate]. + eapply IHpath. 3: eapply STEQ'. eauto. + unfold ssem in SSEM. rewrite ICF in SSEM. + destruct SSEM as (ext & lx & SEXIT & ALLFU). + unfold ssem. rewrite ICF. exists ext, lx. + constructor; auto. eapply sistep_preserves_allfu; eauto. +Qed. + +Lemma sisteps_preserves_sabort ge sp path f rs0 m0 st': forall st, + sisteps path f st = Some st' -> + sabort ge sp st rs0 m0 -> sabort ge sp st' rs0 m0. +Proof. + Local Hint Resolve sistep_preserves_sabort: core. + induction path; simpl. + + unfold sist_set_local; try_simplify_someHyps. + + intros st; inversion_SOME i. + inversion_SOME st1; eauto. +Qed. + +Lemma sisteps_WF path f: forall st, + sisteps path f st = None -> nth_default_succ (fn_code f) path st.(si_pc) = None. +Proof. + induction path; simpl. + + unfold sist_set_local. intuition congruence. + + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try tauto. + destruct (sistep i st) as [st1|] eqn: Hst1; simpl. + - intros; erewrite sistep_default_succ; eauto. + - intros; erewrite sistep_WF; eauto. +Qed. + +Lemma sisteps_default_succ path f st': forall st, + sisteps path f st = Some st' -> nth_default_succ (fn_code f) path st.(si_pc) = Some st'.(si_pc). +Proof. + induction path; simpl. + + unfold sist_set_local. intros st H. inversion_clear H; simpl; try congruence. + + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try congruence. + destruct (sistep i st) as [st1|] eqn: Hst1; simpl; try congruence. + intros; erewrite sistep_default_succ; eauto. +Qed. + +Lemma sisteps_correct_true ge sp path (f:function) rs0 m0: forall st is, + is.(icontinue)=true -> + ssem ge sp st rs0 m0 is -> + nth_default_succ (fn_code f) path st.(si_pc) <> None -> + ssem_opt2 ge sp (sisteps path f st) rs0 m0 + (isteps ge path f sp is.(irs) is.(imem) is.(ipc)) + . +Proof. + Local Hint Resolve sisteps_correct_false sisteps_preserves_sabort sisteps_WF: core. + induction path; simpl. + + intros st is CONT INV WF; + unfold ssem, sist_set_local in * |- *; + try_simplify_someHyps. simpl. + destruct is; simpl in * |- *; subst; intuition auto. + + intros st is CONT; unfold ssem at 1; rewrite CONT. + intros (LOCAL & PC & NYE) WF. + rewrite <- PC. + inversion_SOME i; intro Hi; rewrite Hi in WF |- *; simpl; auto. + exploit sistep_correct; eauto. + inversion_SOME st1; intros Hst1; erewrite Hst1; simpl. + - inversion_SOME is1; intros His1;rewrite His1; simpl. + * destruct (icontinue is1) eqn:CONT1. + (* icontinue is0 = true *) + intros; eapply IHpath; eauto. + destruct i; simpl in * |- *; unfold sist_set_local in * |- *; try_simplify_someHyps. + (* icontinue is0 = false -> EARLY EXIT *) + destruct (sisteps path f st1) as [st2|] eqn: Hst2; simpl; eauto. + destruct WF. erewrite sistep_default_succ; eauto. + (* try_simplify_someHyps; eauto. *) + * destruct (sisteps path f st1) as [st2|] eqn: Hst2; simpl; eauto. + - intros His1;rewrite His1; simpl; auto. +Qed. + +(** REM: in the following two unused lemmas *) + +Lemma sisteps_right_assoc_decompose f path: forall st st', + sisteps (S path) f st = Some st' -> + exists st0, sisteps path f st = Some st0 /\ sisteps 1%nat f st0 = Some st'. +Proof. + induction path; simpl; eauto. + intros st st'. + inversion_SOME i1. + inversion_SOME st1. + try_simplify_someHyps; eauto. +Qed. + +Lemma sisteps_right_assoc_compose f path: forall st st0 st', + sisteps path f st = Some st0 -> + sisteps 1%nat f st0 = Some st' -> + sisteps (S path) f st = Some st'. +Proof. + induction path. + + intros st st0 st' H. simpl in H. + try_simplify_someHyps; auto. + + intros st st0 st'. + assert (X:exists x, x=(S path)); eauto. + destruct X as [x X]. + intros H1 H2. rewrite <- X. + generalize H1; clear H1. simpl. + inversion_SOME i1. intros Hi1; rewrite Hi1. + inversion_SOME st1. intros Hst1; rewrite Hst1. + subst; eauto. +Qed. + +(** * Symbolic (final) value of a path *) +Inductive sfval := + | Snone + | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:node) + (* NB: [res] the return register is hard-wired ! Is it restrictive ? *) + | Stailcall: signature -> sval + ident -> list_sval -> sfval +(* + | Sbuiltin: external_function -> list (builtin_arg sval) -> builtin_res sval -> sfval + | Sjumptable: sval -> list node -> sfval +*) + | Sreturn: option sval -> sfval +. + +Definition sfind_function (pge: RTLpath.genv) (ge: RTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): option fundef := + match svos with + | inl sv => SOME v <- seval_sval ge sp sv rs0 m0 IN Genv.find_funct pge v + | inr symb => SOME b <- Genv.find_symbol pge symb IN Genv.find_funct_ptr pge b + end. + +Inductive sfmatch (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: sistate) stack (f: function) (rs0: regset) (m0: mem): sfval -> regset -> mem -> trace -> state -> Prop := + | exec_Snone rs m: + sfmatch pge ge sp st stack f rs0 m0 Snone rs m E0 (State stack f sp st.(si_pc) rs m) + | exec_Scall rs m sig svos lsv args res pc fd: + sfind_function pge ge sp svos rs0 m0 = Some fd -> + funsig fd = sig -> + seval_list_sval ge sp lsv rs0 m0 = Some args -> + sfmatch pge ge sp st stack f rs0 m0 (Scall sig svos lsv res pc) rs m + E0 (Callstate (Stackframe res f sp pc rs :: stack) fd args m) + | exec_Stailcall stk rs m sig svos args fd m' lsv: + sfind_function pge ge sp svos rs0 m0 = Some fd -> + funsig fd = sig -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + seval_list_sval ge sp lsv rs0 m0 = Some args -> + sfmatch pge ge sp st stack f rs0 m0 (Stailcall sig svos lsv) rs m + E0 (Callstate stack fd args 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') *) +(* TODO: + | 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_Sreturn stk osv rs m m' v: + sp = (Vptr stk Ptrofs.zero) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + match osv with Some sv => seval_sval ge sp sv rs0 m0 | None => Some Vundef end = Some v -> + sfmatch pge ge sp st stack f rs0 m0 (Sreturn osv) rs m + E0 (Returnstate stack v m') +. + +Record sstate := { internal:> sistate; final: sfval }. + +Inductive smatch pge (ge: RTL.genv) (sp:val) (st: sstate) stack f (rs0: regset) (m0: mem): trace -> state -> Prop := + | smatch_early is: + is.(icontinue) = false -> + ssem ge sp st rs0 m0 is -> + smatch pge ge sp st stack f rs0 m0 E0 (State stack f sp is.(ipc) is.(irs) is.(imem)) + | smatch_normal is t s: + is.(icontinue) = true -> + ssem ge sp st rs0 m0 is -> + sfmatch pge ge sp st stack f rs0 m0 st.(final) is.(irs) is.(imem) t s -> + smatch pge ge sp st stack f rs0 m0 t s + . + +(** * Symbolic execution of final step *) +Definition sfstep (i: instruction) (prev: sistate_local): sfval := + match i with + | Icall sig ros args res pc => + let svos := sum_left_map prev.(si_sreg) ros in + let sargs := list_sval_inj (List.map prev.(si_sreg) args) in + Scall sig svos sargs res pc + | Itailcall sig ros args => + let svos := sum_left_map prev.(si_sreg) ros in + let sargs := list_sval_inj (List.map prev.(si_sreg) args) in + Stailcall sig svos sargs + | Ireturn or => + let sor := SOME r <- or IN Some (prev.(si_sreg) r) in + Sreturn sor + | _ => Snone + end. + +Lemma sfstep_correct pge ge sp i (f:function) pc st stack rs0 m0 t rs m s: + (fn_code f) ! pc = Some i -> + pc = st.(si_pc) -> + ssem_local ge sp (si_local st) rs0 m0 rs m -> + path_last_step ge pge stack f sp pc rs m t s -> + sistep i st = None -> + sfmatch pge ge sp st stack f rs0 m0 (sfstep i (si_local st)) rs m t s. +Proof. + intros PC1 PC2 (PRE&MEM®) LAST Hi. destruct LAST; subst; try_simplify_someHyps; simpl. + + (* Snone *) destruct i; simpl in Hi |- *; unfold sist_set_local in Hi; try congruence. + + (* Icall *) intros; eapply exec_Scall; auto. + - destruct ros; simpl in * |- *; auto. + rewrite REG; auto. + - erewrite seval_list_sval_inj; simpl; auto. + + (* Itailcall *) intros. eapply exec_Stailcall; auto. + - destruct ros; simpl in * |- *; auto. + rewrite REG; auto. + - eauto. + - erewrite seval_list_sval_inj; simpl; auto. + + (* Ibuiltin *) admit. + + (* Ijumptable *) admit. + + (* Ireturn *) intros; eapply exec_Sreturn; simpl; eauto. + destruct or; simpl; auto. +Admitted. + +Lemma sfstep_complete i (f:function) pc st ge pge sp stack rs0 m0 t rs m s: + (fn_code f) ! pc = Some i -> + pc = st.(si_pc) -> + ssem_local ge sp (si_local st) rs0 m0 rs m -> + sfmatch pge ge sp st stack f rs0 m0 (sfstep i (si_local st)) rs m t s -> + sistep i st = None -> + path_last_step ge pge stack f sp pc rs m t s. +Proof. + intros PC1 PC2 (PRE&MEM®) LAST Hi. + destruct i as [ | | | |(*Icall*)sig ros args res pc'| | | | |(*Ireturn*)or]; + subst; try_simplify_someHyps; try (unfold sist_set_local in Hi; try congruence); inversion LAST; subst; clear LAST; simpl in * |- *. + + (* Icall *) + erewrite seval_list_sval_inj in * |- ; simpl; try_simplify_someHyps; auto. + intros; eapply exec_Icall; eauto. + destruct ros; simpl in * |- *; auto. + rewrite REG in * |- ; auto. + + (* Itaillcall *) admit. + + (* Ibuiltin *) admit. + + (* Ijumptable *) admit. + + (* Ireturn *) + intros; subst. enough (v=regmap_optget or Vundef rs) as ->. + * eapply exec_Ireturn; eauto. + * intros; destruct or; simpl; congruence. +Admitted. + + +(** * Main function of the symbolic execution *) + +Definition init_sistate_local := {| si_pre:= fun _ _ _ _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}. + +Definition init_sistate pc := {| si_pc:= pc; si_exits:=nil; si_local:= init_sistate_local |}. + +Lemma init_ssem ge sp pc rs m: ssem ge sp (init_sistate pc) rs m (mk_istate true pc rs m). +Proof. + unfold ssem, ssem_local, all_fallthrough; simpl. intuition. +Qed. + +Definition sstep (f: function) (pc:node): option sstate := + SOME path <- (fn_path f)!pc IN + SOME st <- sisteps path.(psize) f (init_sistate pc) IN + SOME i <- (fn_code f)!(st.(si_pc)) IN + Some (match sistep i st with + | Some st' => {| internal := st'; final := Snone |} + | None => {| internal := st; final := sfstep i st.(si_local) |} + end). + +Lemma final_node_path_simpl f path pc: + (fn_path f)!pc = Some path -> nth_default_succ_inst (fn_code f) path.(psize) pc <> None. +Proof. + intros; exploit final_node_path; eauto. + intros (i & NTH & DUM). + congruence. +Qed. + +Lemma symb_path_last_step i st st' ge pge stack (f:function) sp pc rs m t s: + (fn_code f) ! pc = Some i -> + pc = st.(si_pc) -> + sistep i st = Some st' -> + path_last_step ge pge stack f sp pc rs m t s -> + exists mk_istate, + istep ge i sp rs m = Some mk_istate + /\ t = E0 + /\ s = (State stack f sp mk_istate.(ipc) mk_istate.(RTLpath.irs) mk_istate.(imem)). +Proof. + intros PC1 PC2 Hst' LAST; destruct LAST; subst; try_simplify_someHyps; simpl. +Qed. + +(* NB: each concrete execution can be executed on the symbolic state (produced from [sstep]) +(sstep is a correct over-approximation) +*) +Theorem sstep_correct f pc pge ge sp path stack rs m t s: + (fn_path f)!pc = Some path -> + path_step ge pge path.(psize) stack f sp rs m pc t s -> + exists st, sstep f pc = Some st /\ smatch pge ge sp st stack f rs m t s. +Proof. +(* Local Hint Resolve init_ssem sistep_preserves_ssem_exits: core. + intros PATH STEP; unfold sstep; rewrite PATH; simpl. + lapply (final_node_path_simpl f path pc); eauto. intro WF. + exploit (sisteps_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto. + { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. } + (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]). + destruct STEP as [sti STEPS CONT|sti t s STEPS CONT LAST]; + (* intro Hst *) + (rewrite STEPS; unfold ssem_opt2; destruct (sisteps _ _ _) as [st|] eqn: Hst; try congruence); + (* intro SEM *) + (simpl; unfold ssem; simpl; rewrite CONT; intro SEM); + (* intro Hi' *) + ( assert (Hi': (fn_code f) ! (si_pc st) = Some i); + [ unfold nth_default_succ_inst in Hi; + exploit sisteps_default_succ; eauto; simpl; + intros DEF; rewrite DEF in Hi; auto + | clear Hi; rewrite Hi' ]); + (* eexists *) + (eexists; constructor; eauto). + - (* early *) + eapply smatch_early; eauto. + unfold ssem; simpl; rewrite CONT. + destruct (sistep i st) as [st'|] eqn: Hst'; simpl; eauto. + - destruct SEM as (SEM & PC & HNYE). + destruct (sistep i st) as [st'|] eqn: Hst'; simpl. + + (* normal on Snone *) + rewrite <- PC in LAST. + exploit symb_path_last_step; eauto; simpl. + intros (mk_istate & ISTEP & Ht & Hs); subst. + exploit sistep_correct; eauto. simpl. + erewrite Hst', ISTEP; simpl. + clear LAST CONT STEPS PC SEM HNYE Hst Hi' Hst' ISTEP st sti i. + intro SEM; destruct (mk_istate.(icontinue)) eqn: CONT. + { (* icontinue mk_istate = true *) + eapply smatch_normal; simpl; eauto. + unfold ssem in SEM. + rewrite CONT in SEM. + destruct SEM as (SEM & PC & HNYE). + rewrite <- PC. + eapply exec_Snone. } + { eapply smatch_early; eauto. } + + (* normal non-Snone instruction *) + eapply smatch_normal; eauto. + * unfold ssem; simpl; rewrite CONT; intuition. + * simpl. eapply sfstep_correct; eauto. + rewrite PC; auto. *) +Admitted. + +(* TODO: déplacer les trucs sur equiv_stackframe dans RTLpath ? *) +Inductive equiv_stackframe: stackframe -> stackframe -> Prop := + | equiv_stackframe_intro res f sp pc rs1 rs2 + (EQUIV: forall r : positive, rs1 !! r = rs2 !! r): + equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2). + +Inductive equiv_state: state -> state -> Prop := + | State_equiv stack f sp pc rs1 m rs2 + (EQUIV: forall r, rs1#r = rs2#r): + equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m) + | Call_equiv stk stk' f args m + (STACKS: list_forall2 equiv_stackframe stk stk'): + equiv_state (Callstate stk f args m) (Callstate stk' f args m) + | Return_equiv stk stk' v m + (STACKS: list_forall2 equiv_stackframe stk stk'): + equiv_state (Returnstate stk v m) (Returnstate stk' v m). + +Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf. +Proof. + destruct stf. constructor; auto. +Qed. + +Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk. +Proof. + Local Hint Resolve equiv_stackframe_refl: core. + induction stk; simpl; constructor; auto. +Qed. + +Lemma equiv_state_refl s: equiv_state s s. +Proof. + Local Hint Resolve equiv_stack_refl: core. + induction s; simpl; constructor; auto. +Qed. + +(* +Lemma equiv_stackframe_trans stf1 stf2 stf3: + equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3. +Proof. + destruct 1; intros EQ; inv EQ; try econstructor; eauto. + intros; eapply eq_trans; eauto. +Qed. + +Lemma equiv_stack_trans stk1 stk2: + list_forall2 equiv_stackframe stk1 stk2 -> + forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> + list_forall2 equiv_stackframe stk1 stk3. +Proof. + Local Hint Resolve equiv_stackframe_trans. + induction 1; intros stk3 EQ; inv EQ; econstructor; eauto. +Qed. + +Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3. +Proof. + Local Hint Resolve equiv_stack_trans. + destruct 1; intros EQ; inv EQ; econstructor; eauto. + intros; eapply eq_trans; eauto. +Qed. +*) + +Lemma sfmatch_equiv pge ge sp (f:function) st sv stack rs0 m0 t rs1 rs2 m s: + sfmatch pge ge sp st stack f rs0 m0 sv rs1 m t s -> + (forall r, rs1#r = rs2#r) -> + exists s', equiv_state s s' /\ sfmatch pge ge sp st stack f rs0 m0 sv rs2 m t s'. +Proof. + Local Hint Resolve equiv_stack_refl: core. + destruct 1. + - (* Snone *) intros; eexists; econstructor. + + eapply State_equiv; eauto. + + eapply exec_Snone. + - (* Scall *) intros; eexists; econstructor. + 2: { eapply exec_Scall; eauto. } + apply Call_equiv; auto. + repeat (constructor; auto). + - (* Sreturn *) intros; eexists; econstructor. + + eapply equiv_state_refl; eauto. + + (* eapply exec_Sreturn; eauto. *) admit. +Admitted. + +(* NB: each execution of a symbolic state (produced from [sstep]) represents a concrete execution + (sstep is exact). +*) +Theorem sstep_exact f pc pge ge sp path stack st rs m t s1: + (fn_path f)!pc = Some path -> + sstep f pc = Some st -> + smatch pge ge sp st stack f rs m t s1 -> + exists s2, path_step ge pge path.(psize) stack f sp rs m pc t s2 /\ + equiv_state s1 s2. +Proof. + Local Hint Resolve init_ssem: core. + unfold sstep; intros PATH SSTEP SEM; rewrite PATH in SSTEP. + lapply (final_node_path_simpl f path pc); eauto. intro WF. + exploit (sisteps_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto. + { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. } + (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]). + unfold nth_default_succ_inst in Hi. + destruct (sisteps path.(psize) f (init_sistate pc)) as [st0|] eqn: Hst0; simpl. + 2:{ (* absurd case *) + exploit sisteps_WF; eauto. + simpl; intros NDS; rewrite NDS in Hi; congruence. } + exploit sisteps_default_succ; eauto; simpl. + intros NDS; rewrite NDS in Hi. + rewrite Hi in SSTEP. + intros ISTEPS. try_simplify_someHyps. + destruct (sistep i st0) as [st'|] eqn: Hst'; simpl. + + (* normal exit on Snone instruction *) + admit. + + destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *. + - (* early exit *) + intros. + exploit ssem_opt_determ; eauto. + destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4). + eexists. econstructor 1. + * eapply exec_early_exit; eauto. + * rewrite EQ2, EQ4; eapply State_equiv. auto. + - (* normal exit non-Snone instruction *) + intros. + exploit ssem_opt_determ; eauto. + destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4). + unfold ssem in SEM1. + rewrite CONT in SEM1. destruct SEM1 as (SEM1 & PC0 & NYE0). + exploit sfmatch_equiv; eauto. + clear SEM2; destruct 1 as (s' & Ms' & SEM2). + rewrite ! EQ4 in * |-; clear EQ4. + rewrite ! EQ2 in * |-; clear EQ2. + exists s'; intuition. + eapply exec_normal_exit; eauto. + eapply sfstep_complete; eauto. + * congruence. + * unfold ssem_local in * |- *. intuition try congruence. +Admitted. + +(** * Simulation of RTLpath code w.r.t symbolic execution *) + +Section SymbValPreserved. + +Variable ge ge': RTL.genv. + +Hypothesis symbols_preserved_RTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s. + +Lemma seval_preserved sp sv rs0 m0: + seval_sval ge sp sv rs0 m0 = seval_sval ge' sp sv rs0 m0. +Proof. + Local Hint Resolve symbols_preserved_RTL: core. + induction sv using sval_mut with (P0 := fun lsv => seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv rs0 m0) + (P1 := fun sm => seval_smem ge sp sm rs0 m0 = seval_smem ge' sp sm rs0 m0); simpl; auto. + + rewrite IHsv; clear IHsv. destruct (seval_list_sval _ _ _ _); auto. + rewrite IHsv0; clear IHsv0. destruct (seval_smem _ _ _ _); auto. + erewrite eval_operation_preserved; eauto. + + rewrite IHsv0; clear IHsv0. destruct (seval_list_sval _ _ _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsv; auto. + + rewrite IHsv; clear IHsv. destruct (seval_sval _ _ _ _); auto. + rewrite IHsv0; auto. + + rewrite IHsv0; clear IHsv0. destruct (seval_list_sval _ _ _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsv; clear IHsv. destruct (seval_smem _ _ _ _); auto. + rewrite IHsv1; auto. +Qed. + +Lemma list_sval_eval_preserved sp lsv rs0 m0: + seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv rs0 m0. +Proof. + induction lsv; simpl; auto. + rewrite seval_preserved. destruct (seval_sval _ _ _ _); auto. + rewrite IHlsv; auto. +Qed. + +Lemma smem_eval_preserved sp sm rs0 m0: + seval_smem ge sp sm rs0 m0 = seval_smem ge' sp sm rs0 m0. +Proof. + induction sm; simpl; auto. + rewrite list_sval_eval_preserved. destruct (seval_list_sval _ _ _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsm; clear IHsm. destruct (seval_smem _ _ _ _); auto. + rewrite seval_preserved; auto. +Qed. + +Lemma seval_condition_preserved sp cond lsv sm rs0 m0: + seval_condition ge sp cond lsv sm rs0 m0 = seval_condition ge' sp cond lsv sm rs0 m0. +Proof. + unfold seval_condition. + rewrite list_sval_eval_preserved. destruct (seval_list_sval _ _ _ _); auto. + rewrite smem_eval_preserved; auto. +Qed. + +End SymbValPreserved. + +Require Import RTLpathLivegen RTLpathLivegenproof. + +Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop := + is1.(icontinue) = is2.(icontinue) + /\ eqlive_reg alive is1.(irs) is2.(irs) + /\ is1.(imem) = is2.(imem). + +Definition istate_simu f (srce: PTree.t node) is1 is2: Prop := + if is1.(icontinue) then + (* TODO: il faudra raffiner le (fun _ => True) si on veut autoriser l'oracle à + ajouter du "code mort" sur des registres non utilisés (loop invariant code motion à la David) + Typiquement, pour connaître la frame des registres vivants, il faudra faire une propagation en arrière + sur la dernière instruction du superblock. *) + istate_simulive (fun _ => True) srce is1 is2 + else + exists path, f.(fn_path)!(is1.(ipc)) = Some path + /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2 + /\ srce!(is2.(ipc)) = Some is1.(ipc). + +(* NOTE: a pure semantic definition on [sistate], for a total freedom in refinements *) +Definition sistate_simu (f: RTLpath.function) (srce: PTree.t node) (st1 st2: sistate): Prop := + forall sp ge1 ge2, + (forall s, Genv.find_symbol ge2 s = Genv.find_symbol ge1 s) -> + liveness_ok_function f -> + forall rs m is1, ssem ge1 sp st1 rs m is1 -> + exists is2, ssem ge2 sp st2 rs m is2 /\ istate_simu f srce is1 is2. + +(* NOTE: a syntactic definition on [sfval] in order to abstract the [match_states] *) +Inductive sfval_simu (f: RTLpath.function) (srce: PTree.t node) (opc1 opc2: node): sfval -> sfval -> Prop := + | Snone_simu: + srce!opc2 = Some opc1 -> + sfval_simu f srce opc1 opc2 Snone Snone + | Scall_simu sig svos lsv res pc1 pc2: + srce!pc2 = Some pc1 -> + sfval_simu f srce opc1 opc2 (Scall sig svos lsv res pc1) (Scall sig svos lsv res pc2) + | Sreturn_simu os: + sfval_simu f srce opc1 opc2 (Sreturn os) (Sreturn os). + +Definition sstate_simu f srce (s1 s2: sstate): Prop := + sistate_simu f srce s1.(internal) s2.(internal) + /\ sfval_simu f srce s1.(si_pc) s2.(si_pc) s1.(final) s2.(final). + +Definition sstep_simu srce (f1 f2: RTLpath.function) pc1 pc2: Prop := + forall st1, sstep f1 pc1 = Some st1 -> + exists st2, sstep f2 pc2 = Some st2 /\ sstate_simu f1 srce st1 st2. + +(* IDEA: we will provide an efficient test for checking "sstep_simu" property, by hash-consing. + See usage of [sstep_simu] in [RTLpathScheduler]. +*) diff --git a/kvx/lib/RTLpathScheduler.v b/kvx/lib/RTLpathScheduler.v new file mode 100644 index 00000000..57ae6c7f --- /dev/null +++ b/kvx/lib/RTLpathScheduler.v @@ -0,0 +1,190 @@ +(** RTLpath Scheduling from an external oracle. + +This module is inspired from [Duplicate] and [Duplicateproof] + +*) + +Require Import AST Linking Values Maps Globalenvs Smallstep Registers. +Require Import Coqlib Maps Events Errors Op. +Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory. + + +Local Open Scope error_monad_scope. +Local Open Scope positive_scope. + + + +(** External oracle returning the new RTLpath function and a mapping of new path_entries to old path_entries + +NB: the new RTLpath function is generated from the fn_code, the fn_entrypoint and the fn_path +It requires to check that the path structure is wf ! + +*) +(* Axiom untrusted_scheduler: RTLpath.function -> code * node * path_map * (PTree.t node). *) + +Axiom untrusted_scheduler: RTLpath.function -> code * (PTree.t node). + +Extract Constant untrusted_scheduler => "RTLpathScheduleraux.scheduler". + +Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := { + preserv_fnsig: fn_sig f1 = fn_sig f2; + preserv_fnparams: fn_params f1 = fn_params f2; + preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2; + preserv_entrypoint: dupmap!(f2.(fn_entrypoint)) = Some f1.(fn_entrypoint); + dupmap_path_entry1: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f1) pc1; + dupmap_path_entry2: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f2) pc2; + dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> sstep_simu dupmap f1 f2 pc1 pc2 +}. + +(* TODO - perform appropriate checks on tc and dupmap *) +Definition verified_scheduler (f: RTLpath.function) : res (code * (PTree.t node)) := + let (tc, dupmap) := untrusted_scheduler f in OK (tc, dupmap). + +Lemma verified_scheduler_wellformed_pm f tc pm dm: + fn_path f = pm -> + verified_scheduler f = OK (tc, dm) -> + wellformed_path_map tc pm. +Proof. +Admitted. + +Program Definition transf_function (f: RTLpath.function): res RTLpath.function := + match (verified_scheduler f) with + | Error e => Error e + | OK (tc, dupmap) => + let rtl_tf := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc (fn_entrypoint f) in + OK {| fn_RTL := rtl_tf; fn_path := (fn_path f) |} + end. +Next Obligation. + destruct f as [rtl_f pm EP_WF PATH_WF]. assumption. +Qed. Next Obligation. + destruct f as [rtl_f pm EP_WF PATH_WF]. simpl. + eapply verified_scheduler_wellformed_pm; eauto. simpl. reflexivity. +Qed. + +Parameter transf_function_correct: + forall f f', transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. + +Theorem transf_function_preserves: + forall f f', + transf_function f = OK f' -> + fn_sig f = fn_sig f' /\ fn_params f = fn_params f' /\ fn_stacksize f = fn_stacksize f'. +Proof. + intros. exploit transf_function_correct; eauto. + destruct 1 as (dupmap & [SIG PARAM SIZE ENTRY CORRECT]). + intuition. +Qed. + +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. + +(** * Preservation proof *) + +Local Notation ext alive := (fun r => Regset.In r alive). + +Inductive match_fundef: RTLpath.fundef -> RTLpath.fundef -> Prop := + | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + | match_stackframe_intro dupmap res f sp pc rs1 rs2 f' pc' path + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc' = Some pc) + (LIVE: liveness_ok_function f) + (PATH: f.(fn_path)!pc = Some path) + (EQUIV: forall v, eqlive_reg (ext path.(input_regs)) (rs1 # res <- v) (rs2 # res <- v)): + match_stackframes (Stackframe res f sp pc rs1) (Stackframe res f' sp pc' rs2). + +Inductive match_states: state -> state -> Prop := + | match_states_intro dupmap st f sp pc rs1 rs2 m st' f' pc' path + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc' = Some pc) + (LIVE: liveness_ok_function f) + (PATH: f.(fn_path)!pc = Some path) + (EQUIV: eqlive_reg (ext path.(input_regs)) rs1 rs2): + match_states (State st f sp pc rs1 m) (State st' f' sp pc' rs2 m) + | match_states_call st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f') + (LIVE: liveness_ok_fundef f): + match_states (Callstate st f args m) (Callstate st' f' args m) + | match_states_return st st' v m + (STACKS: list_forall2 match_stackframes st st'): + match_states (Returnstate st v m) (Returnstate st' v m). + +Lemma match_stackframes_equiv stf1 stf2 stf3: + match_stackframes stf1 stf2 -> equiv_stackframe stf2 stf3 -> match_stackframes stf1 stf3. +Proof. + destruct 1; intros EQ; inv EQ; try econstructor; eauto. + intros; eapply eqlive_reg_trans; eauto. + rewrite eqlive_reg_triv in * |-. + eapply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + simpl; auto. +Qed. + +Lemma match_stack_equiv stk1 stk2: + list_forall2 match_stackframes stk1 stk2 -> + forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> + list_forall2 match_stackframes stk1 stk3. +Proof. + Local Hint Resolve match_stackframes_equiv: core. + induction 1; intros stk3 EQ; inv EQ; econstructor; eauto. +Qed. + +Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3. +Proof. + Local Hint Resolve match_stack_equiv: core. + destruct 1; intros EQ; inv EQ; econstructor; eauto. + intros; eapply eqlive_reg_triv_trans; eauto. +Qed. + +Lemma eqlive_match_stackframes stf1 stf2 stf3: + eqlive_stackframes stf1 stf2 -> match_stackframes stf2 stf3 -> match_stackframes stf1 stf3. +Proof. + destruct 1; intros MS; inv MS; try econstructor; eauto. + try_simplify_someHyps. intros; eapply eqlive_reg_trans; eauto. +Qed. + +Lemma eqlive_match_stack stk1 stk2: + list_forall2 eqlive_stackframes stk1 stk2 -> + forall stk3, list_forall2 match_stackframes stk2 stk3 -> + list_forall2 match_stackframes stk1 stk3. +Proof. + induction 1; intros stk3 MS; inv MS; econstructor; eauto. + eapply eqlive_match_stackframes; eauto. +Qed. + +Lemma eqlive_match_states s1 s2 s3: eqlive_states s1 s2 -> match_states s2 s3 -> match_states s1 s3. +Proof. + Local Hint Resolve eqlive_match_stack: core. + destruct 1; intros MS; inv MS; try_simplify_someHyps; econstructor; eauto. + eapply eqlive_reg_trans; eauto. +Qed. + +Lemma eqlive_stackframes_refl stf1 stf2: match_stackframes stf1 stf2 -> eqlive_stackframes stf1 stf1. +Proof. + destruct 1; econstructor; eauto. + intros; eapply eqlive_reg_refl; eauto. +Qed. + +Lemma eqlive_stacks_refl stk1 stk2: + list_forall2 match_stackframes stk1 stk2 -> list_forall2 eqlive_stackframes stk1 stk1. +Proof. + induction 1; simpl; econstructor; eauto. + eapply eqlive_stackframes_refl; eauto. +Qed. + +Lemma transf_fundef_correct f f': + transf_fundef f = OK f' -> match_fundef f f'. +Proof. + intros TRANSF; destruct f; simpl; monadInv TRANSF. + + exploit transf_function_correct; eauto. + intros (dupmap & MATCH_F). + eapply match_Internal; eauto. + + eapply match_External. +Qed. + diff --git a/kvx/lib/RTLpathScheduleraux.ml b/kvx/lib/RTLpathScheduleraux.ml new file mode 100644 index 00000000..1017cf63 --- /dev/null +++ b/kvx/lib/RTLpathScheduleraux.ml @@ -0,0 +1,8 @@ +open RTLpath +open RTL +open Maps + +let scheduler f = + let code = f.fn_RTL.fn_code in + let id_ptree = PTree.map (fun n i -> n) code in + (code, id_ptree) diff --git a/kvx/lib/RTLpathSchedulerproof.v b/kvx/lib/RTLpathSchedulerproof.v new file mode 100644 index 00000000..db1f6be7 --- /dev/null +++ b/kvx/lib/RTLpathSchedulerproof.v @@ -0,0 +1,303 @@ +Require Import AST Linking Values Maps Globalenvs Smallstep Registers. +Require Import Coqlib Maps Events Errors Op. +Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory. +Require Import RTLpathScheduler. + +Definition match_prog (p tp: program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. + +Section PRESERVATION. + +Variable prog: program. +Variable tprog: program. + +Hypothesis TRANSL: match_prog prog tprog. + +Let pge := Genv.globalenv prog. +Let tpge := Genv.globalenv tprog. + +(* Was a Hypothesis *) +Theorem all_fundef_liveness_ok: forall b fd, + Genv.find_funct_ptr pge b = Some fd -> liveness_ok_fundef fd. +Proof. +Admitted. + +Lemma symbols_preserved s: Genv.find_symbol tpge s = Genv.find_symbol pge s. +Proof. + rewrite <- (Genv.find_symbol_match TRANSL). reflexivity. +Qed. + +Lemma senv_preserved: + Senv.equiv pge tpge. +Proof. + eapply (Genv.senv_match TRANSL). +Qed. + +Lemma functions_preserved: + forall (v: val) (f: fundef), + Genv.find_funct pge v = Some f -> + exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tpge v = Some tf /\ linkorder cunit prog. +Proof. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & A & B & C). + repeat eexists; intuition eauto. + + unfold incl; auto. + + eapply linkorder_refl. +Qed. + +Lemma function_ptr_preserved: + forall v f, + Genv.find_funct_ptr pge v = Some f -> + exists tf, + Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf. +Proof. + intros. + exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto. +Qed. + +Lemma function_sig_preserved: + forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f. +Proof. + intros. destruct f. + - simpl in H. monadInv H. simpl. symmetry. + eapply transf_function_preserves. + assumption. + - simpl in H. monadInv H. reflexivity. +Qed. + +Theorem transf_initial_states: + forall s1, initial_state prog s1 -> + exists s2, initial_state tprog s2 /\ match_states s1 s2. +Proof. + intros. inv H. + exploit function_ptr_preserved; eauto. intros (tf & FIND & TRANSF). + exists (Callstate nil tf nil m0). + split. + - econstructor; eauto. + + intros; apply (Genv.init_mem_match TRANSL); assumption. + + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main. eauto. + + destruct f. + * monadInv TRANSF. rewrite <- H3. symmetry; eapply transf_function_preserves. assumption. + * monadInv TRANSF. assumption. + - constructor; eauto. + + constructor. + + apply transf_fundef_correct; auto. + + eapply all_fundef_liveness_ok; eauto. +Qed. + +Theorem transf_final_states s1 s2 r: + final_state s1 r -> match_states s1 s2 -> final_state s2 r. +Proof. + unfold final_state. + intros H; inv H. + intros H; inv H; simpl in * |- *; try congruence. + inv H1. + destruct st; simpl in * |- *; try congruence. + inv STACKS. constructor. +Qed. + + +Let ge := Genv.globalenv (RTLpath.transf_program prog). +Let tge := Genv.globalenv (RTLpath.transf_program tprog). + +Lemma senv_sym x y: Senv.equiv x y -> Senv.equiv y x. +Proof. + unfold Senv.equiv. intuition congruence. +Qed. + +Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z. +Proof. + unfold Senv.equiv. intuition congruence. +Qed. + +Lemma senv_preserved_RTL: + Senv.equiv ge tge. +Proof. + eapply senv_transitivity. { eapply senv_sym; eapply RTLpath.senv_preserved. } + eapply senv_transitivity. { eapply senv_preserved. } + eapply RTLpath.senv_preserved. +Qed. + +Lemma symbols_preserved_RTL s: Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + unfold tge, ge. erewrite RTLpath.symbols_preserved; eauto. + rewrite symbols_preserved. + erewrite RTLpath.symbols_preserved; eauto. +Qed. + +Lemma s_find_function_preserved sp svos rs0 m0 fd: + sfind_function pge ge sp svos rs0 m0 = Some fd -> + exists fd', sfind_function tpge tge sp svos rs0 m0 = Some fd' + /\ transf_fundef fd = OK fd' + /\ liveness_ok_fundef fd. +Proof. + Local Hint Resolve symbols_preserved_RTL: core. + unfold sfind_function. destruct svos; simpl. + + rewrite (seval_preserved ge tge); auto. + destruct (seval_sval _ _ _ _); try congruence. + intros; exploit functions_preserved; eauto. + intros (fd' & cunit & X). eexists. intuition eauto. + eapply find_funct_liveness_ok; eauto. + intros. eapply all_fundef_liveness_ok; eauto. + + rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence. + intros; exploit function_ptr_preserved; eauto. + intros (fd' & X). eexists. intuition eauto. + intros. eapply all_fundef_liveness_ok; eauto. +Qed. + +Lemma sistate_simu f dupmap sp st st' rs m is: + ssem ge sp st rs m is -> + liveness_ok_function f -> + sistate_simu f dupmap st st' -> + exists is', + ssem tge sp st' rs m is' /\ istate_simu f dupmap is is'. +Proof. + intros SEM LIVE X; eapply X; eauto. +Qed. + + +Lemma sfmatch_simu dupmap f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s: + match_function dupmap f f' -> + liveness_ok_function f -> + list_forall2 match_stackframes stk stk' -> + (* s_istate_simu f dupmap st st' -> *) + sfval_simu f dupmap st.(si_pc) st'.(si_pc) sv sv' -> + sfmatch pge ge sp st stk f rs0 m0 sv rs m t s -> + exists s', sfmatch tpge tge sp st' stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'. +Proof. + Local Hint Resolve transf_fundef_correct: core. + intros FUN LIVE STK (* SIS *) SFV. destruct SFV; intros SEM; inv SEM; simpl. + - (* Snone *) + exploit initialize_path. { eapply dupmap_path_entry1; eauto. } + intros (path & PATH). + eexists; split; econstructor; eauto. + eapply eqlive_reg_refl. + - (* Scall *) + exploit s_find_function_preserved; eauto. + intros (fd' & FIND & TRANSF & LIVE'). + erewrite <- function_sig_preserved; eauto. + exploit initialize_path. { eapply dupmap_path_entry1; eauto. } + intros (path & PATH). + eexists; split; econstructor; eauto. + + erewrite <- (list_sval_eval_preserved ge tge); auto. + + simpl. repeat (econstructor; eauto). + - (* Sreturn *) + eexists; split; econstructor; eauto. + + erewrite <- preserv_fnstacksize; eauto. + + destruct os; auto. + erewrite <- seval_preserved; eauto. +Qed. + +(* The main theorem on simulation of symbolic states ! *) +Theorem smatch_sstate_simu dupmap f f' stk stk' sp st st' rs m t s: + match_function dupmap f f' -> + liveness_ok_function f -> + list_forall2 match_stackframes stk stk' -> + smatch pge ge sp st stk f rs m t s -> + sstate_simu f dupmap st st' -> + exists s', smatch tpge tge sp st' stk' f' rs m t s' /\ match_states s s'. +Proof. + intros MFUNC LIVE STACKS SEM (SIMU1 & SIMU2). destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl. + - (* sem_early *) + exploit sistate_simu; eauto. + unfold istate_simu; rewrite CONT. + intros (is' & SEM' & (path & PATH & (CONT' & RS' & M') & PC')). + exists (State stk' f' sp (ipc is') (irs is') (imem is')). + split. + + eapply smatch_early; auto. congruence. + + rewrite M'. econstructor; eauto. + - (* sem_normal *) + exploit sistate_simu; eauto. + unfold istate_simu; rewrite CONT. + intros (is' & SEM' & (CONT' & RS' & M')). + rewrite <- eqlive_reg_triv in RS'. + exploit sfmatch_simu; eauto. + clear SEM2; intros (s0 & SEM2 & MATCH0). + exploit sfmatch_equiv; eauto. + clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s1 & EQ & SEM2). + exists s1; split. + + eapply smatch_normal; eauto. + + eapply match_states_equiv; eauto. +Qed. + +Lemma exec_path_simulation dupmap path stk stk' f f' sp rs m pc pc' t s: + (fn_path f)!pc = Some path -> + path_step ge pge path.(psize) stk f sp rs m pc t s -> + list_forall2 match_stackframes stk stk' -> + dupmap ! pc' = Some pc -> + match_function dupmap f f' -> + liveness_ok_function f -> + exists path' s', (fn_path f')!pc' = Some path' /\ path_step tge tpge path'.(psize) stk' f' sp rs m pc' t s' /\ match_states s s'. +Proof. + intros PATH STEP STACKS DUPPC MATCHF LIVE. + exploit initialize_path. { eapply dupmap_path_entry2; eauto. } + intros (path' & PATH'). + exists path'. + exploit (sstep_correct f pc pge ge sp path stk rs m t s); eauto. + intros (st & SYMB & SEM); clear STEP. + exploit dupmap_correct; eauto. + clear SYMB; intros (st' & SYMB & SIMU). + exploit smatch_sstate_simu; eauto. + intros (s0 & SEM0 & MATCH). + exploit sstep_exact; eauto. + intros (s' & STEP' & EQ). + exists s'; intuition. + eapply match_states_equiv; eauto. +Qed. + +Lemma step_simulation s1 t s1' s2: + step ge pge s1 t s1' -> + match_states s1 s2 -> + exists s2', + step tge tpge s2 t s2' + /\ match_states s1' s2'. +Proof. + Local Hint Resolve eqlive_stacks_refl transf_fundef_correct: core. + destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ]; intros MS; inv MS. +(* exec_path *) + - try_simplify_someHyps. intros. + exploit path_step_eqlive; eauto. { intros. eapply all_fundef_liveness_ok; eauto. } + clear STEP EQUIV rs; intros (s2 & STEP & EQLIVE). + exploit exec_path_simulation; eauto. + clear STEP; intros (path' & s' & PATH' & STEP' & MATCH'). + exists s'; split. + + eapply exec_path; eauto. + + eapply eqlive_match_states; eauto. +(* exec_function_internal *) + - inv LIVE. + exploit initialize_path. { eapply (fn_entry_point_wf f). } + destruct 1 as (path & PATH). + inversion TRANSF as [f0 xf tf MATCHF|]; subst. eexists. split. + + eapply exec_function_internal. erewrite <- preserv_fnstacksize; eauto. + + erewrite preserv_fnparams; eauto. + econstructor; eauto. + { apply preserv_entrypoint; auto. } + { apply eqlive_reg_refl. } +(* exec_function_external *) + - inversion TRANSF as [|]; subst. eexists. split. + + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved_RTL. + + constructor. assumption. +(* exec_return *) + - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split. + + constructor. + + inv H1. econstructor; eauto. +Qed. + +Theorem transf_program_correct: + forward_simulation (semantics prog) (semantics tprog). +Proof. + eapply forward_simulation_step with match_states. + - eapply senv_preserved. + - eapply transf_initial_states. + - intros; eapply transf_final_states; eauto. + - intros; eapply step_simulation; eauto. +Qed. + +End PRESERVATION. diff --git a/kvx/lib/RTLpathproof.v b/kvx/lib/RTLpathproof.v new file mode 100644 index 00000000..20eded97 --- /dev/null +++ b/kvx/lib/RTLpathproof.v @@ -0,0 +1,50 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL Linking. +Require Import RTLpath. + +Definition match_prog (p: RTLpath.program) (tp: RTL.program) := + match_program (fun ctx f tf => tf = fundef_RTL f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. + +Lemma match_program_transf: + forall p tp, match_prog p tp -> transf_program p = tp. +Proof. + intros p tp H. inversion_clear H. inv H1. + destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. simpl in *. + subst. unfold transf_program. unfold transform_program. simpl. + apply program_equals; simpl; auto. + induction H0; simpl; auto. + rewrite IHlist_forall2. apply cons_extract. + destruct a1 as [ida gda]. destruct b1 as [idb gdb]. + simpl in *. + inv H. inv H2. + - simpl in *. subst. auto. + - simpl in *. subst. inv H. auto. +Qed. + + +Section PRESERVATION. + +Variable prog: RTLpath.program. +Variable tprog: RTL.program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Theorem transf_program_correct: + forward_simulation (RTLpath.semantics prog) (RTL.semantics tprog). +Proof. + pose proof (match_program_transf prog tprog TRANSF) as TR. subst. + eapply RTLpath_correct. +Qed. + +End PRESERVATION. + + diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 1fa5ad28..c37880d5 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -34,11 +34,14 @@ TOTAL, (Option "optim_move_loop_invariants"), (Some "Renumbering for LICM"), "Re PARTIAL, (Option "optim_move_loop_invariants"), (Some "CSE3 for LICM"), "CSE3"; PARTIAL, (Option "optim_move_loop_invariants"), (Some "Redundancy elimination for LICM"), "Deadcode"; TOTAL, (Option "all_loads_nontrap"), None, "Allnontrap"; -PARTIAL, Always, (Some "Unused globals"), "Unusedglob" +PARTIAL, Always, (Some "Unused globals"), "Unusedglob"; |];; let post_rtl_passes = [| + PARTIAL, Always, (Some "RTLpath generation"), "RTLpathLivegen", Noprint; + PARTIAL, Always, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint; + TOTAL, Always, (Some "Projection to RTL"), "RTLpath", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1))); PARTIAL, Always, (Some "Register allocation"), "Allocation", (Print "LTL"); TOTAL, Always, (Some "Branch tunneling"), "Tunneling", Noprint; PARTIAL, Always, (Some "CFG linearization"), "Linearize", Noprint; |