From af2c82cfd7f2318fcd81da2ea4cf3fd695db3b40 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 28 Apr 2021 18:14:53 +0200 Subject: start the new "BTL" IR. --- Makefile | 4 +- configure | 2 +- lib/OptionMonad.v | 6 + scheduling/BTL.v | 575 +++++++++++++++++++++++++++++++++++++++++++++ scheduling/BTLtoRTL.v | 23 ++ scheduling/BTLtoRTLproof.v | 127 ++++++++++ 6 files changed, 735 insertions(+), 2 deletions(-) create mode 100644 scheduling/BTL.v create mode 100644 scheduling/BTLtoRTL.v create mode 100644 scheduling/BTLtoRTLproof.v diff --git a/Makefile b/Makefile index 62635d70..90c39907 100644 --- a/Makefile +++ b/Makefile @@ -82,6 +82,7 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ Iteration.v Zbits.v Integers.v Archi.v IEEE754_extra.v Floats.v \ Parmov.v UnionFind.v Wfsimpl.v \ Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v \ + OptionMonad.v \ ImpConfig.v ImpExtern.v ImpIO.v ImpMonads.v \ ImpCore.v ImpHCons.v ImpLoops.v ImpPrelude.v @@ -141,7 +142,8 @@ SCHEDULING= \ RTLpathLivegen.v RTLpathSE_impl.v \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ - RTLpathScheduler.v RTLpathWFcheck.v + RTLpathScheduler.v RTLpathWFcheck.v \ + BTL.v BTLtoRTL.v BTLtoRTLproof.v \ # C front-end modules (in cfrontend/) diff --git a/configure b/configure index e8ebb6f8..1ec6d210 100755 --- a/configure +++ b/configure @@ -817,7 +817,7 @@ fi if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling cat >> Makefile.config < _ end] => destruct expr eqn:EQ; generalize EQ; clear EQ; congruence || trivial + end. + 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. diff --git a/scheduling/BTL.v b/scheduling/BTL.v new file mode 100644 index 00000000..8bdafb89 --- /dev/null +++ b/scheduling/BTL.v @@ -0,0 +1,575 @@ +(** The BTL intermediate language: abstract syntax and semantics. + + BTL stands for "Block Transfer Language". + + Informally, a block is a piece of "loop-free" code, with a single entry-point, + hence, such that transformation preserving locally the semantics of each block, + preserve also globally the semantics of the function. + + a BTL function is a CFG where each node is such a block, represented by structured code. + + BTL gives a structured view of RTL code. + It is dedicated to optimizations validated by "symbolic simulation" over blocks. + + +*) + +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad. + +(** * Abstract syntax *) + +Definition exit := node. (* we may generalize this with register renamings at exit, + like in "phi" nodes of SSA-form *) + +(** final instructions (that stops block execution) *) +Inductive final: Type := + | Bgoto (succ:exit) (** No operation -- just branch to [succ]. *) + | Breturn (res: option reg) + (** terminates the execution of the current function. It returns the value of the given + register, or [Vundef] if none is given. *) + | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit) + (** invokes the function determined by [fn] (either a function pointer found in a register or a + function name), giving it the values of registers [args] as arguments. + It stores the return value in [dest] and branches to [succ]. *) + | Btailcall (sig:signature) (fn: reg + ident) (args: list reg) + (** performs a function invocation in tail-call position + (the current function terminates after the call, returning the result of the callee) + *) + | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit) + (** calls the built-in function identified by [ef], giving it the values of [args] as arguments. + It stores the return value in [dest] and branches to [succ]. *) + | Bjumptable (arg:reg) (tbl:list exit) + (** [Bjumptable arg tbl] transitions to the node that is the [n]-th + element of the list [tbl], where [n] is the unsigned integer value of register [arg]. *) + . + +(* instruction block *) +Inductive iblock: Type := +(* final instructions that stops block execution *) + | BF (fi: final) +(* basic instructions that continues block execution, except when aborting *) + | Bnop (* nop instruction *) + | Bop (op:operation) (args:list reg) (dest:reg) + (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *) + | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) + (** loads a [chunk] quantity from the address determined by the addressing mode [addr] + and the values of the [args] registers, stores the quantity just read into [dest]. + If trap=NOTRAP, then failures lead to a default value written to [dest]. *) + | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) + (** stores the value of register [src] in the [chunk] quantity at the + the address determined by the addressing mode [addr] and the + values of the [args] registers. *) +(* composed instructions *) + | Bseq (b1 b2: iblock) + (** starts by running [b1] and stops here if execution of [b1] has reached a final instruction or aborted + or continue with [b2] otherwise *) + | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (info:option bool) + (** evaluates the boolean condition [cond] over the values of registers [args]. + If the condition is true, it continues on [ifso]. + If the condition is false, it continues on [ifnot]. + [info] is a ghost field there to provide information relative to branch prediction. *) + . +Coercion BF: final >-> iblock. + + +(** NB: - a RTL [(Inop pc)] ending a branch of block is encoded by [(Bseq Bnop (Bgoto pc))]. + - a RTL [(Inop pc)] in the middle of a branch is simply encoded by [Bnop]. + - the same trick appears for all "basic" instructions and [Icond]. +*) + + + +Record iblock_info := { + entry: iblock; + input_regs: Regset.t (* extra liveness information ignored by BTL semantics *) +}. + +Definition code: Type := PTree.t iblock_info. + +Record function: Type := mkfunction { + fn_sig: signature; + fn_params: list reg; + fn_stacksize: Z; + fn_code: code; + fn_entrypoint: node +}. + +(** A function description comprises a control-flow graph (CFG) [fn_code] + (a partial finite mapping from nodes to instructions). As in Cminor, + [fn_sig] is the function signature and [fn_stacksize] the number of bytes + for its stack-allocated activation record. [fn_params] is the list + of registers that are bound to the values of arguments at call time. + [fn_entrypoint] is the node of the first instruction of the function + in the CFG. *) + +Definition fundef := AST.fundef function. + +Definition program := AST.program fundef unit. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => fn_sig f + | External ef => ef_sig ef + end. + +(** * Operational semantics *) + +Definition genv := Genv.t fundef unit. + +(** The dynamic semantics of BTL is similar to RTL, + except that the step of one instruction is generalized into the run of one [iblock]. +*) + +Inductive stackframe : Type := + | Stackframe: + forall (res: reg) (**r where to store the result *) + (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (succ: exit) (**r program point in calling function *) + (rs: regset), (**r register state in calling function *) + stackframe. + +Inductive state : Type := + | State: + forall (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 *) + state + | Callstate: + forall (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 *) + state + | Returnstate: + forall (stack: list stackframe) (**r call stack *) + (v: val) (**r return value for the call *) + (m: mem), (**r memory state *) + state. + +(** outcome of a block execution *) +Record outcome := { + _rs: regset; + _m: mem; + _fin: option final +}. + +Section RELSEM. + +Variable ge: genv. + +Definition find_function (ros: reg + ident) (rs: regset) : option fundef := + match ros with + | inl r => Genv.find_funct ge rs#r + | inr symb => + match Genv.find_symbol ge symb with + | None => None + | Some b => Genv.find_funct_ptr ge b + end + end. + +Local Open Scope option_monad_scope. + +(** internal big-step execution of one iblock *) +Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := + | exec_final rs m fin: iblock_istep sp rs m (BF fin) rs m (Some fin) + | exec_nop rs m: iblock_istep sp rs m Bnop rs m None + | exec_op rs m op args res v + (EVAL: eval_operation ge sp op rs##args m = Some v) + : iblock_istep sp rs m (Bop op args res) (rs#res <- v) m None + | exec_load_TRAP rs m chunk addr args dst a v + (EVAL: eval_addressing ge sp addr rs##args = Some a) + (LOAD: Mem.loadv chunk m a = Some v) + : iblock_istep sp rs m (Bload TRAP chunk addr args dst) (rs#dst <- v) m None + | exec_store rs m chunk addr args src a m' + (EVAL: eval_addressing ge sp addr rs##args = Some a) + (STORE: Mem.storev chunk m a rs#src = Some m') + : iblock_istep sp rs m (Bstore chunk addr args src) rs m' None + | exec_seq_stop rs m b1 b2 rs' m' fin + (EXEC: iblock_istep sp rs m b1 rs' m' (Some fin)) + : iblock_istep sp rs m (Bseq b1 b2) rs' m' (Some fin) + | exec_seq_continue rs m b1 b2 rs1 m1 rs' m' ofin + (EXEC1: iblock_istep sp rs m b1 rs1 m1 None) + (EXEC2: iblock_istep sp rs1 m1 b2 rs' m' ofin) + : iblock_istep sp rs m (Bseq b1 b2) rs' m' ofin + | exec_cond rs m cond args ifso ifnot i b rs' m' ofin + (EVAL: eval_condition cond rs##args m = Some b) + (EXEC: iblock_istep sp rs m (if b then ifso else ifnot) rs' m' ofin) + : iblock_istep sp rs m (Bcond cond args ifso ifnot i) rs' m' ofin + . +Local Hint Constructors iblock_istep: core. + +(** A functional variant of [iblock_istep_run] of [iblock_istep]. +Lemma [iblock_istep_run_equiv] below provides a proof that "relation" [iblock_istep] is a "partial function". +*) +Fixpoint iblock_istep_run sp ib rs m: option outcome := + match ib with + | BF fin => + Some {| _rs := rs; _m := m; _fin := Some fin |} + (* basic instructions *) + | Bnop => + Some {| _rs := rs; _m:= m; _fin := None |} + | Bop op args res => + SOME v <- eval_operation ge sp op rs##args m IN + Some {| _rs := rs#res <- v; _m:= m; _fin := None |} + | Bload TRAP chunk addr args dst => + SOME a <- eval_addressing ge sp addr rs##args IN + SOME v <- Mem.loadv chunk m a IN + Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + | Bload NOTRAP chunk addr args dst => + None (* TODO *) + | Bstore chunk addr args src => + SOME a <- eval_addressing ge sp addr rs##args IN + SOME m' <- Mem.storev chunk m a rs#src IN + Some {| _rs := rs; _m:= m'; _fin := None |} + (* composed instructions *) + | Bseq b1 b2 => + SOME out1 <- iblock_istep_run sp b1 rs m IN + match out1.(_fin) with + | None => iblock_istep_run sp b2 out1.(_rs) out1.(_m) + | _ => Some out1 (* stop execution on the 1st final instruction *) + end + | Bcond cond args ifso ifnot _ => + SOME b <- eval_condition cond rs##args m IN + iblock_istep_run sp (if b then ifso else ifnot) rs m + end. + +Lemma iblock_istep_run_equiv sp rs m ib rs' m' ofin: + iblock_istep sp rs m ib rs' m' ofin <-> iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m:= m'; _fin := ofin |}. +Proof. + constructor. + - induction 1; simpl; try autodestruct; try_simplify_someHyps. + - generalize rs m rs' m' ofin; clear rs m rs' m' ofin. + induction ib; simpl; repeat (try autodestruct; try_simplify_someHyps). + destruct o; try_simplify_someHyps; subst; eauto. +Qed. + +Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := + | exec_Bgoto pc: + final_step stack f sp rs m (Bgoto pc) E0 + (State stack f sp pc rs m) + | exec_Breturn or stk m': + sp = (Vptr stk Ptrofs.zero) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + final_step stack f sp rs m (Breturn or) + E0 (Returnstate stack (regmap_optget or Vundef rs) m') + | exec_Bcall sig ros args res pc' fd: + find_function ros rs = Some fd -> + funsig fd = sig -> + final_step stack f sp rs m (Bcall sig ros args res pc') + E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m) + | exec_Btailcall sig ros args stk m' fd: + find_function ros rs = Some fd -> + funsig fd = sig -> + sp = (Vptr stk Ptrofs.zero) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + final_step stack f sp rs m (Btailcall sig ros args) + E0 (Callstate stack fd rs##args m') + | exec_Bbuiltin ef args res pc' vargs t vres m': + eval_builtin_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + final_step stack f sp rs m (Bbuiltin ef args res pc') + t (State stack f sp pc' (regmap_setres res vres rs) m') + | exec_Bjumptable arg tbl n pc': + rs#arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some pc' -> + final_step stack f sp rs m (Bjumptable arg tbl) + E0 (State stack f sp pc' rs m) +. + +(** big-step execution of one iblock *) +Definition iblock_step stack f sp rs m ib t s: Prop := + exists rs' m' fin, iblock_istep sp rs m ib rs' m' (Some fin) /\ final_step stack f sp rs' m' fin t s. + +(** The transitions are presented as an inductive predicate + [step ge st1 t st2], where [ge] is the global environment, + [st1] the initial state, [st2] the final state, and [t] the trace + of system calls performed during this transition. *) + +Inductive step: state -> trace -> state -> Prop := + | exec_iblock stack ib f sp pc rs m t s: + (fn_code f)!pc = Some ib -> + iblock_step stack f sp rs m ib.(entry) t s -> + step (State stack f sp pc rs m) t s + | exec_function_internal stack f args m m' stk: + Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> + step (Callstate stack (Internal f) args m) + E0 (State stack + f + (Vptr stk Ptrofs.zero) + f.(fn_entrypoint) + (init_regs args f.(fn_params)) + m') + | exec_function_external stack ef args res t m m': + external_call ef ge args m t res m' -> + step (Callstate stack (External ef) args m) + t (Returnstate stack res m') + | exec_return stack res f sp pc rs vres m: + step (Returnstate (Stackframe res f sp pc rs :: stack) vres m) + E0 (State stack f sp pc (rs#res <- vres) m) +. + +End RELSEM. + +(** Execution of whole programs are described as sequences of transitions + from an initial state to a final state. An initial state is a [Callstate] + corresponding to the invocation of the ``main'' function of the program + without arguments and with an empty call stack. *) + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b f m0, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = signature_main -> + initial_state p (Callstate nil f nil m0). + +(** A final state is a [Returnstate] with an empty call stack. *) + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall r m, + final_state (Returnstate nil (Vint r) m) r. + +(** The small-step semantics for a program. *) + +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). + + +(** Matching BTL and RTL code + +We should be able to define a single verifier able to prove a bisimulation between BTL and RTL code. + +NB 1: the proof of BTL -> RTL (plus simulation) should be much easier than RTL -> BTL (star simulation). + +NB 2: our scheme allows the BTL to duplicate some RTL code. +- in other words: RTL -> BTL allows tail duplication, loop unrolling, etc. Exactly like "Duplicate" on RTL. +- BTL -> RTL allows to "undo" some duplications (e.g. remove duplications that have not enabled interesting optimizations) ! + +Hence, in a sense, our verifier imitates the approach of Duplicate, where [dupmap] maps the BTL nodes to the RTL nodes. + +The [match_*] definitions gives a "relational" specification of the verifier... +*) + +Require Import Errors. + +Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop := +(* TODO: it may be simplify the oracle for BTL -> RTL, but may makes the verifier more complex ? + | mfi_goto pc pc': + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc') +*) + | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or) + | mfi_call pc pc' s ri lr r: + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc') + | mfi_tailcall s ri lr: + match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr) + | mfi_builtin pc pc' ef la br: + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc') + | mfi_jumptable ln ln' r: + list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' -> + match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln') +. + +Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop := + | ijo_None_left o: is_join_opt None o o + | ijo_None_right o: is_join_opt o None o + | ijo_Some x: is_join_opt (Some x) (Some x) (Some x) + . + +(* [match_iblock dupmap cfg isfst pc ib opc] means that [ib] match a block in a RTL code starting at [pc], with: + - [isfst] (in "input") indicates that no step in the surrounding block has been executed before entering [pc] + - if [opc] (in "ouput") is [None], this means that all branches of the block ends on a final instruction + - if [opc] is [Some pc'], this means that all branches of the block that do not exit, join on [pc']. +*) +Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> iblock -> (option node) -> Prop := + | mib_BF isfst fi pc i: + cfg!pc = Some i -> + match_final_inst dupmap fi i -> + match_iblock dupmap cfg isfst pc (BF fi) None + | mib_nop isfst pc pc': + cfg!pc = Some (Inop pc') -> + match_iblock dupmap cfg isfst pc Bnop (Some pc') + | mib_op isfst pc pc' op lr r: + cfg!pc = Some (Iop op lr r pc') -> + match_iblock dupmap cfg isfst pc (Bop op lr r) (Some pc') + | mib_load isfst pc pc' tm m a lr r: + cfg!pc = Some (Iload tm m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bload tm m a lr r) (Some pc') + | mib_store isfst pc pc' m a lr r: + cfg!pc = Some (Istore m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bstore m a lr r) (Some pc') + | mib_exit pc pc': + dupmap!pc = (Some pc') -> + match_iblock dupmap cfg false pc' (Bgoto pc) None + (* NB: on RTL side, we exit the block by a "basic" instruction (or Icond). + Thus some step should have been executed before [pc'] in the RTL code *) + | mib_seq_Some isfst b1 b2 pc1 pc2 opc: + match_iblock dupmap cfg isfst pc1 b1 (Some pc2) -> + match_iblock dupmap cfg false pc2 b2 opc -> + match_iblock dupmap cfg isfst pc1 (Bseq b1 b2) opc +(* | mib_seq_None isfst b1 b2 pc: + match_iblock dupmap cfg isfst pc b1 None -> + match_iblock dupmap cfg isfst (Bseq b1 b2) pc None + (* TODO: here [b2] is dead code ! Is this case really useful ? + The oracle could remove this dead code. + And the verifier could fail if there is such dead code! + *) +*) + | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i i': + cfg!pc = Some (Icond c lr pcso pcnot i') -> + match_iblock dupmap cfg false pcso bso opc1 -> + match_iblock dupmap cfg false pcnot bnot opc2 -> + is_join_opt opc1 opc2 opc -> + match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i) opc + . + +(* Partial copy of Duplicate and Duplicateproof. *) + +Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := + forall pc pc', dupmap!pc = Some pc' -> + exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None. + +Record match_function dupmap f f': Prop := { + dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f'); + dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f'); + preserv_fnsig: fn_sig f = RTL.fn_sig f'; + preserv_fnparams: fn_params f = RTL.fn_params f'; + preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f' +}. + +Inductive match_fundef: fundef -> RTL.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 -> RTL.stackframe -> Prop := + | match_stackframe_intro + dupmap res f sp pc rs f' pc' + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc' = Some pc) + : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). + +Inductive match_states: state -> RTL.state -> Prop := + | match_states_intro + dupmap st f sp pc rs m st' f' pc' + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc' = Some pc) + : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m) + | match_states_call + st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f') + : match_states (Callstate st f args m) (RTL.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) (RTL.Returnstate st' v m) + . + +(** Shared verifier between RTL -> BTL and BTL -> RTL *) + +Local Open Scope error_monad_scope. + +Definition verify_is_copy dupmap n n' := + match dupmap!n with + | None => Error(msg "verify_is_copy None") + | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end + end. + +Fixpoint verify_is_copy_list dupmap ln ln' := + match ln with + | n::ln => match ln' with + | n'::ln' => do _ <- verify_is_copy dupmap n n'; + verify_is_copy_list dupmap ln ln' + | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end + | nil => match ln' with + | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") + | nil => OK tt end + end. + +Lemma verify_is_copy_correct dupmap n n' tt: + verify_is_copy dupmap n n' = OK tt -> + dupmap ! n = Some n'. +Proof. + unfold verify_is_copy; repeat autodestruct. + intros NP H; destruct (_ ! n) eqn:REVM; [|inversion H]. + eapply Pos.compare_eq in NP. congruence. +Qed. +Local Hint Resolve verify_is_copy_correct: core. + +Lemma verify_is_copy_list_correct dupmap ln: forall ln' tt, + verify_is_copy_list dupmap ln ln' = OK tt -> + list_forall2 (fun n n' => dupmap ! n = Some n') ln ln'. +Proof. + induction ln. + - intros. destruct ln'; monadInv H. constructor. + - intros. destruct ln'; monadInv H. constructor; eauto. +Qed. + +(* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *) +Parameter verify_block: PTree.t node -> RTL.code -> bool -> node -> iblock -> res (option node). + +(* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *) +Lemma verify_block_correct: forall dupmap cfg isfst pc ib fin, + verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin. +Admitted. +Local Hint Resolve verify_block_correct: core. + +Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit := + match l with + | nil => OK tt + | (pc, pc')::l => + match cfg!pc with + | Some ib => do o <- verify_block dupmap cfg' true pc' ib.(entry); + match o with + | None => verify_blocks dupmap cfg cfg' l + | _ => Error(msg "verify_blocks.end") + end + | _ => Error(msg "verify_blocks.entry") + end + end. + +Definition verify_cfg dupmap (cfg: code) (cfg':RTL.code): res unit := + verify_blocks dupmap cfg cfg' (PTree.elements dupmap). + +Lemma verify_cfg_correct dupmap cfg cfg' tt: + verify_cfg dupmap cfg cfg' = OK tt -> + match_cfg dupmap cfg cfg'. +Proof. + unfold verify_cfg. + intros X pc pc' H; generalize X; clear X. + exploit PTree.elements_correct; eauto. + generalize tt pc pc' H; clear tt pc pc' H. + generalize (PTree.elements dupmap). + induction l as [|[pc1 pc1']l]; simpl. + - tauto. + - intros pc pc' DUP u H. + unfold bind. + repeat autodestruct. + intros; subst. + destruct H as [H|H]; eauto. + inversion H; subst. + eexists; split; eauto. +Qed. + +Definition verify_function dupmap f f' : res unit := + do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); + verify_cfg dupmap (fn_code f) (RTL.fn_code f'). + +Lemma verify_function_correct dupmap f f' tt: + verify_function dupmap f f' = OK tt -> + fn_sig f = RTL.fn_sig f' -> + fn_params f = RTL.fn_params f' -> + fn_stacksize f = RTL.fn_stacksize f' -> + match_function dupmap f f'. +Proof. + unfold verify_function; intro VERIF. monadInv VERIF. + constructor; eauto. + eapply verify_cfg_correct; eauto. +Qed. diff --git a/scheduling/BTLtoRTL.v b/scheduling/BTLtoRTL.v new file mode 100644 index 00000000..b64fd87a --- /dev/null +++ b/scheduling/BTLtoRTL.v @@ -0,0 +1,23 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad BTL. + +Require Import Errors Linking. + +(** External oracle *) +Parameter btl2rtl: function -> RTL.code * node * (PTree.t node). + +Local Open Scope error_monad_scope. + +Definition transf_function (f: function) : res RTL.function := + let (tcte, dupmap) := btl2rtl f in + let (tc, te) := tcte in + let f' := RTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in + do u <- verify_function dupmap f f'; + OK f'. + +Definition transf_fundef (f: fundef) : res RTL.fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: program) : res RTL.program := + transform_partial_program transf_fundef p. diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v new file mode 100644 index 00000000..26b5bae6 --- /dev/null +++ b/scheduling/BTLtoRTLproof.v @@ -0,0 +1,127 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad BTL. + +Require Import Errors Linking BTLtoRTL. + + +(*****************************) +(* Put this in an other file *) + +Require Import Linking. + +Lemma transf_function_correct f f': + transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. +Proof. + unfold transf_function; unfold bind. repeat autodestruct. + intros H _ _ X. inversion X; subst; clear X. + eexists; eapply verify_function_correct; simpl; 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. + +Definition match_prog (p: program) (tp: RTL.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 RTL_SIMULATES_BTL. + +Variable prog: program. +Variable tprog: RTL.program. + +Hypothesis TRANSL: match_prog prog tprog. + +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + rewrite <- (Genv.find_symbol_match TRANSL). reflexivity. +Qed. + +Lemma senv_preserved: Senv.equiv ge tge. +Proof. + eapply (Genv.senv_match TRANSL). +Qed. + +Lemma functions_translated (v: val) (f: fundef): + Genv.find_funct ge v = Some f -> + exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge 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_translated v f: + Genv.find_funct_ptr ge v = Some f -> + exists tf, + Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. +Proof. + intros. + exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto. +Qed. + +Lemma function_sig_translated f tf: transf_fundef f = OK tf -> RTL.funsig tf = funsig f. +Proof. + intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto. + erewrite preserv_fnsig; eauto. +Qed. + +Lemma transf_initial_states s1: + initial_state prog s1 -> + exists s2, RTL.initial_state tprog s2 /\ match_states s1 s2. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF). + eexists. split. + - econstructor; eauto. + + eapply (Genv.init_mem_transf_partial TRANSL); eauto. + + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main. eauto. + + erewrite function_sig_translated; eauto. + - constructor; eauto. + constructor. + apply transf_fundef_correct; auto. +Qed. + +Lemma transf_final_states s1 s2 r: + match_states s1 s2 -> final_state s1 r -> RTL.final_state s2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem plus_simulation s1 t s1': + step ge s1 t s1' -> + forall s2 (MS: match_states s1 s2), + exists s2', + plus RTL.step tge s2 t s2' + /\ match_states s1' s2'. +Admitted. (* TODO: première étape *) + +Theorem transf_program_correct: + forward_simulation (semantics prog) (RTL.semantics tprog). +Proof. + eapply forward_simulation_plus with match_states. + - eapply senv_preserved. + - eapply transf_initial_states. + - eapply transf_final_states. + - eapply plus_simulation. +Qed. + +End RTL_SIMULATES_BTL. -- cgit