diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | lib/OptionMonad.v | 21 | ||||
| -rw-r--r-- | scheduling/BTL.v | 835 | ||||
| -rw-r--r-- | scheduling/BTL_SEtheory.v | 1111 | ||||
| -rw-r--r-- | scheduling/BTLroadmap.md | 353 | ||||
| -rw-r--r-- | scheduling/BTLtoRTL.v | 23 | ||||
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 403 | ||||
| -rw-r--r-- | scheduling/RTLtoBTL.v | 23 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 744 |
10 files changed, 3518 insertions, 2 deletions
@@ -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,9 @@ 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 RTLtoBTL.v RTLtoBTLproof.v \ + BTL_SEtheory.v # C front-end modules (in cfrontend/) @@ -817,7 +817,7 @@ fi if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling cat >> Makefile.config <<EOF ARCHDIRS=$arch scheduling/abstractbb scheduling/postpass_lib -BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v \\ +BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v IterList.v \\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asm.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v\\ diff --git a/lib/OptionMonad.v b/lib/OptionMonad.v index 824a9c2f..18430e04 100644 --- a/lib/OptionMonad.v +++ b/lib/OptionMonad.v @@ -13,6 +13,27 @@ Local Open Scope option_monad_scope. (** Simple tactics for option-monad *) +Ltac deepest_match exp := + match exp with + | context f [match ?expr with | _ => _ end] => ltac: (deepest_match expr) + | _ => exp + end. + +Ltac autodestruct := + let EQ := fresh "EQ" in + match goal with + | |- context f [match ?expr with | _ => _ end] => + let t := ltac: (deepest_match expr) in + destruct t eqn:EQ; generalize EQ; clear EQ; congruence || trivial + end. + +(* deprecated version of "autodestruct". the new one seems a better replacement *) +Ltac dummy_autodestruct := + let EQ := fresh "EQ" in + match goal with + | |- context f [match ?expr with | _ => _ 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..10a000a8 --- /dev/null +++ b/scheduling/BTL.v @@ -0,0 +1,835 @@ +(** 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 := out { + _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. + +(* (* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *) + +Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := + | has_loaded_normal a trap + (EVAL: eval_addressing ge sp addr rs##args = Some a) + (LOAD: Mem.loadv chunk m a = Some v) + : has_loaded sp rs m chunk addr args v trap + | has_loaded_default + (LOAD: forall a, eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = None) + (DEFAULT: v = default_notrap_load_value chunk) + : has_loaded sp rs m chunk addr args v NOTRAP + . + +(* TODO: move this scheme in "Memory" module if this scheme is useful ! *) + +*) + +(** 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 +(* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above + | exec_load rs m trap chunk addr args dst v + (LOAD: has_loaded sp rs m chunk addr args v trap) + : 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 + (PC: (fn_code f)!pc = Some ib) + (STEP: 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 + (ALLOC: 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' + (EXTCALL: 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). + + +(** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) + +(** 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' m a lr r: + cfg!pc = Some (Iload TRAP m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bload TRAP 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 + . + +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. + +(** 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 Copied from duplicate, should we import ? *) +Lemma product_eq {A B: Type} : + (forall (a b: A), {a=b} + {a<>b}) -> + (forall (c d: B), {c=d} + {c<>d}) -> + forall (x y: A+B), {x=y} + {x<>y}. +Proof. + intros H H'. intros. decide equality. +Qed. + +(* TODO Copied from duplicate, should we import ? *) +(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application" + * error when doing so *) +Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}. +Proof. + intros. + apply (builtin_arg_eq Pos.eq_dec). +Defined. +Global Opaque builtin_arg_eq_pos. + +(* TODO Copied from duplicate, should we import ? *) +Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}. +Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed. +Global Opaque builtin_res_eq_pos. + +Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := + match ib with + | BF fi => + match fi with + | Bgoto pc1 => + do u <- verify_is_copy dupmap pc1 pc; + if negb isfst then + OK None + else Error (msg "verify_block: isfst is true Bgoto") + | Breturn or => + match cfg!pc with + | Some (Ireturn or') => + if option_eq Pos.eq_dec or or' then OK None + else Error (msg "verify_block: different opt reg in Breturn") + | _ => Error (msg "verify_block: incorrect cfg Breturn") + end + | Bcall s ri lr r pc1 => + match cfg!pc with + | Some (Icall s' ri' lr' r' pc2) => + do u <- verify_is_copy dupmap pc1 pc2; + if (signature_eq s s') then + if (product_eq Pos.eq_dec ident_eq ri ri') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK None + else Error (msg "verify_block: different r r' in Bcall") + else Error (msg "verify_block: different lr in Bcall") + else Error (msg "verify_block: different ri in Bcall") + else Error (msg "verify_block: different signatures in Bcall") + | _ => Error (msg "verify_block: incorrect cfg Bcall") + end + | Btailcall s ri lr => + match cfg!pc with + | Some (Itailcall s' ri' lr') => + if (signature_eq s s') then + if (product_eq Pos.eq_dec ident_eq ri ri') then + if (list_eq_dec Pos.eq_dec lr lr') then OK None + else Error (msg "verify_block: different lr in Btailcall") + else Error (msg "verify_block: different ri in Btailcall") + else Error (msg "verify_block: different signatures in Btailcall") + | _ => Error (msg "verify_block: incorrect cfg Btailcall") + end + | Bbuiltin ef la br pc1 => + match cfg!pc with + | Some (Ibuiltin ef' la' br' pc2) => + do u <- verify_is_copy dupmap pc1 pc2; + if (external_function_eq ef ef') then + if (list_eq_dec builtin_arg_eq_pos la la') then + if (builtin_res_eq_pos br br') then OK None + else Error (msg "verify_block: different brr in Bbuiltin") + else Error (msg "verify_block: different lbar in Bbuiltin") + else Error (msg "verify_block: different ef in Bbuiltin") + | _ => Error (msg "verify_block: incorrect cfg Bbuiltin") + end + | Bjumptable r ln => + match cfg!pc with + | Some (Ijumptable r' ln') => + do u <- verify_is_copy_list dupmap ln ln'; + if (Pos.eq_dec r r') then OK None + else Error (msg "verify_block: different r in Bjumptable") + | _ => Error (msg "verify_block: incorrect cfg Bjumptable") + end + end + | Bnop => + match cfg!pc with + | Some (Inop pc') => OK (Some pc') + | _ => Error (msg "verify_block: incorrect cfg Bnop") + end + | Bop op lr r => + match cfg!pc with + | Some (Iop op' lr' r' pc') => + if (eq_operation op op') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then + OK (Some pc') + else Error (msg "verify_block: different r in Bop") + else Error (msg "verify_block: different lr in Bop") + else Error (msg "verify_block: different operations in Bop") + | _ => Error (msg "verify_block: incorrect cfg Bop") + end + | Bload tm m a lr r => + match cfg!pc with + | Some (Iload tm' m' a' lr' r' pc') => + if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then + OK (Some pc') + else Error (msg "verify_block: different r in Bload") + else Error (msg "verify_block: different lr in Bload") + else Error (msg "verify_block: different addressing in Bload") + else Error (msg "verify_block: different mchunk in Bload") + else Error (msg "verify_block: NOTRAP trapping_mode unsupported in Bload") + | _ => Error (msg "verify_block: incorrect cfg Bload") + end + | Bstore m a lr r => + match cfg!pc with + | Some (Istore m' a' lr' r' pc') => + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK (Some pc') + else Error (msg "verify_block: different r in Bstore") + else Error (msg "verify_block: different lr in Bstore") + else Error (msg "verify_block: different addressing in Bstore") + else Error (msg "verify_block: different mchunk in Bstore") + | _ => Error (msg "verify_block: incorrect cfg Bstore") + end + | Bseq b1 b2 => + do opc <- verify_block dupmap cfg isfst pc b1; + match opc with + | Some pc' => + verify_block dupmap cfg false pc' b2 + | None => Error (msg "verify_block: None next pc in Bseq (deadcode)") + end + | Bcond c lr bso bnot i => + match cfg!pc with + | Some (Icond c' lr' pcso pcnot i') => + if (list_eq_dec Pos.eq_dec lr lr') then + if (eq_condition c c') then + do opc1 <- verify_block dupmap cfg false pcso bso; + do opc2 <- verify_block dupmap cfg false pcnot bnot; + match opc1, opc2 with + | None, o => OK o + | o, None => OK o + | Some x, Some x' => + if Pos.eq_dec x x' then OK (Some x) + else Error (msg "verify_block: is_join_opt incorrect for Bcond") + end + else Error (msg "verify_block: incompatible conditions in Bcond") + else Error (msg "verify_block: different lr in Bcond") + | _ => Error (msg "verify_block: incorrect cfg Bcond") + end + end. + +(* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *) +Lemma verify_block_correct dupmap cfg ib: forall pc isfst fin, + verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin. +Proof. + induction ib; intros; + try (unfold verify_block in H; destruct (cfg!pc) eqn:EQCFG; [ idtac | discriminate; fail ]). + - (* BF *) + destruct fi; unfold verify_block in H. + + (* Bgoto *) + monadInv H. + destruct (isfst); simpl in EQ0; inv EQ0. + eapply verify_is_copy_correct in EQ. + constructor; assumption. + + (* Breturn *) + destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. + destruct (option_eq _ _ _); try discriminate. inv H. + eapply mib_BF; eauto. constructor. + + (* Bcall *) + destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. + monadInv H. + eapply verify_is_copy_correct in EQ. + destruct (signature_eq _ _); try discriminate. + destruct (product_eq _ _ _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. subst. + inv EQ0. eapply mib_BF; eauto. constructor; assumption. + + (* Btailcall *) + destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. + destruct (signature_eq _ _); try discriminate. + destruct (product_eq _ _ _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. subst. + inv H. eapply mib_BF; eauto. constructor. + + (* Bbuiltin *) + destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. + monadInv H. + eapply verify_is_copy_correct in EQ. + destruct (external_function_eq _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (builtin_res_eq_pos _ _); try discriminate. subst. + inv EQ0. eapply mib_BF; eauto. constructor; assumption. + + (* Bjumptable *) + destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. + monadInv H. + eapply verify_is_copy_list_correct in EQ. + destruct (Pos.eq_dec _ _); try discriminate. subst. + inv EQ0. eapply mib_BF; eauto. constructor; assumption. + - (* Bnop *) + destruct i; inv H. + constructor; assumption. + - (* Bop *) + destruct i; try discriminate. + destruct (eq_operation _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. inv H. + constructor; assumption. + - (* Bload *) + destruct i; try discriminate. + do 2 (destruct (trapping_mode_eq _ _); try discriminate). + simpl in H. + destruct (chunk_eq _ _); try discriminate. + destruct (eq_addressing _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. inv H. + constructor; assumption. + - (* Bstore *) + destruct i; try discriminate. + destruct (chunk_eq _ _); try discriminate. + destruct (eq_addressing _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. inv H. + constructor; assumption. + - (* Bseq *) + monadInv H. + destruct x; try discriminate. + eapply mib_seq_Some. + eapply IHib1; eauto. + eapply IHib2; eauto. + - (* Bcond *) + destruct i; try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (eq_condition _ _); try discriminate. + fold (verify_block dupmap cfg false n ib1) in H. + fold (verify_block dupmap cfg false n0 ib2) in H. + monadInv H. + destruct x, x0; try destruct (Pos.eq_dec _ _); try discriminate. + all: inv EQ2; eapply mib_cond; eauto; econstructor. +Qed. +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'). + +Definition is_goto (ib: iblock): bool := + match ib with + | Bgoto _ => true + | _ => false + end. + +Definition is_atom (ib: iblock): bool := + match ib with + | Bseq _ _ | Bcond _ _ _ _ _ => false + | _ => true + end. + +(** Is expand property to only support atomic instructions on the left part of a Bseq *) +Inductive is_expand: iblock -> Prop := + | exp_Bseq ib1 ib2: + is_atom ib1 = true -> + is_expand ib2 -> + is_expand (Bseq ib1 ib2) + | exp_Bcond cond args ib1 ib2 i: + is_expand ib1 -> + is_expand ib2 -> + is_expand (Bcond cond args ib1 ib2 i) + | exp_others ib: + is_atom ib = true -> + is_expand ib + . +Local Hint Constructors is_expand: core. + +Fixpoint expand (ib: iblock) (k: option iblock): iblock := + match ib with + | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k)) + | Bcond cond args ib1 ib2 i => + Bcond cond args (expand ib1 k) (expand ib2 k) i + | BF fin => fin + | ib => + match k with + | None => ib + | Some rem => Bseq ib rem + end + end. + +Lemma expand_correct ib: forall k, + (match k with Some rem => is_expand rem | None => True end) + -> is_expand (expand ib k). +Proof. + induction ib; simpl; intros; try autodestruct; auto. +Qed. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v new file mode 100644 index 00000000..b9a05a8a --- /dev/null +++ b/scheduling/BTL_SEtheory.v @@ -0,0 +1,1111 @@ +(* A theory of symbolic execution on BTL + +NB: an efficient implementation with hash-consing will be defined in another file (some day) + +*) + +Require Import Coqlib Maps Floats. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL BTL OptionMonad. + +(* TODO remove this, when copy-paste of RTLpathSE_theory is clearly over... *) +Ltac inversion_SOME := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) +Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) + +Record iblock_exec_context := Bctx { + cge: BTL.genv; + cstk: list stackframe; + cf: function; + csp: val; + crs0: regset; + cm0: mem +}. + +(** * Syntax and semantics of symbolic values *) + +(* symbolic value *) +Inductive sval := + | Sinput (r: reg) + | Sop (op:operation) (lsv: list_sval) (sm: smem) + | 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 eval_sval ctx (sv: sval): option val := + match sv with + | Sinput r => Some ((crs0 ctx)#r) + | Sop op l sm => + SOME args <- eval_list_sval ctx l IN + SOME m <- eval_smem ctx sm IN + eval_operation (cge ctx) (csp ctx) op args m + | Sload sm trap chunk addr lsv => + match trap with + | TRAP => + SOME args <- eval_list_sval ctx lsv IN + SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN + SOME m <- eval_smem ctx sm IN + Mem.loadv chunk m a + | NOTRAP => + SOME args <- eval_list_sval ctx lsv IN + match (eval_addressing (cge ctx) (csp ctx) addr args) with + | None => Some (default_notrap_load_value chunk) + | Some a => + SOME m <- eval_smem ctx sm IN + match (Mem.loadv chunk m a) with + | None => Some (default_notrap_load_value chunk) + | Some val => Some val + end + end + end + end +with eval_list_sval ctx (lsv: list_sval): option (list val) := + match lsv with + | Snil => Some nil + | Scons sv lsv' => + SOME v <- eval_sval ctx sv IN + SOME lv <- eval_list_sval ctx lsv' IN + Some (v::lv) + end +with eval_smem ctx (sm: smem): option mem := + match sm with + | Sinit => Some (cm0 ctx) + | Sstore sm chunk addr lsv srce => + SOME args <- eval_list_sval ctx lsv IN + SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN + SOME m <- eval_smem ctx sm IN + SOME sv <- eval_sval ctx srce IN + Mem.storev chunk m a sv + end. + +Lemma eval_list_sval_inj ctx l (sreg: reg -> sval) rs: + (forall r : reg, eval_sval ctx (sreg r) = Some (rs # r)) -> + eval_list_sval ctx (list_sval_inj (map sreg l)) = Some (rs ## l). +Proof. + intros H; induction l as [|r l]; simpl; repeat autodestruct; auto. +Qed. + +Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : option bool := + SOME args <- eval_list_sval ctx lsv IN + SOME m <- eval_smem ctx sm IN + eval_condition cond args m. + + +(** * Auxiliary definitions on Builtins *) +(* TODO: clean this. Some (cge ctx)neric stuffs could be put in [AST.v] *) + +Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *) + +Variable ctx: iblock_exec_context. +Variable m: mem. + +Inductive seval_builtin_arg: builtin_arg sval -> val -> Prop := + | seval_BA: forall x v, + eval_sval ctx x = Some v -> + seval_builtin_arg (BA x) v + | seval_BA_int: forall n, + seval_builtin_arg (BA_int n) (Vint n) + | seval_BA_long: forall n, + seval_builtin_arg (BA_long n) (Vlong n) + | seval_BA_float: forall n, + seval_builtin_arg (BA_float n) (Vfloat n) + | seval_BA_single: forall n, + seval_builtin_arg (BA_single n) (Vsingle n) + | seval_BA_loadstack: forall chunk ofs v, + Mem.loadv chunk m (Val.offset_ptr (csp ctx) ofs) = Some v -> + seval_builtin_arg (BA_loadstack chunk ofs) v + | seval_BA_addrstack: forall ofs, + seval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs) + | seval_BA_loadglobal: forall chunk id ofs v, + Mem.loadv chunk m (Senv.symbol_address (cge ctx) id ofs) = Some v -> + seval_builtin_arg (BA_loadglobal chunk id ofs) v + | seval_BA_addrglobal: forall id ofs, + seval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address (cge ctx) id ofs) + | seval_BA_splitlong: forall hi lo vhi vlo, + seval_builtin_arg hi vhi -> seval_builtin_arg lo vlo -> + seval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo) + | seval_BA_addptr: forall a1 a2 v1 v2, + seval_builtin_arg a1 v1 -> seval_builtin_arg a2 v2 -> + seval_builtin_arg (BA_addptr a1 a2) + (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2) +. + +Definition seval_builtin_args (al: list (builtin_arg sval)) (vl: list val) : Prop := + list_forall2 seval_builtin_arg al vl. + +Lemma seval_builtin_arg_determ: + forall a v, seval_builtin_arg a v -> forall v', seval_builtin_arg a v' -> v' = v. +Proof. + induction 1; intros v' EV; inv EV; try congruence. + f_equal; eauto. + apply IHseval_builtin_arg1 in H3. apply IHseval_builtin_arg2 in H5. subst; auto. +Qed. + +Lemma eval_builtin_args_determ: + forall al vl, seval_builtin_args al vl -> forall vl', seval_builtin_args al vl' -> vl' = vl. +Proof. + induction 1; intros v' EV; inv EV; f_equal; eauto using seval_builtin_arg_determ. +Qed. + +End SEVAL_BUILTIN_ARG. + +(* NB: (cge ctx)neric function that could be put into [AST] file *) +Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B := + match arg with + | BA x => BA (f x) + | BA_int n => BA_int n + | BA_long n => BA_long n + | BA_float f => BA_float f + | BA_single s => BA_single s + | BA_loadstack chunk ptr => BA_loadstack chunk ptr + | BA_addrstack ptr => BA_addrstack ptr + | BA_loadglobal chunk id ptr => BA_loadglobal chunk id ptr + | BA_addrglobal id ptr => BA_addrglobal id ptr + | BA_splitlong ba1 ba2 => BA_splitlong (builtin_arg_map f ba1) (builtin_arg_map f ba2) + | BA_addptr ba1 ba2 => BA_addptr (builtin_arg_map f ba1) (builtin_arg_map f ba2) + end. + +Lemma seval_builtin_arg_correct ctx rs m sreg: forall arg varg, + (forall r, eval_sval ctx (sreg r) = Some rs # r) -> + eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg -> + seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg. +Proof. + induction arg. + all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence). + - intros varg SEVAL BARG. inv BARG. simpl. constructor. + eapply IHarg1; eauto. eapply IHarg2; eauto. + - intros varg SEVAL BARG. inv BARG. simpl. constructor. + eapply IHarg1; eauto. eapply IHarg2; eauto. +Qed. + +Lemma seval_builtin_args_correct ctx rs m sreg args vargs: + (forall r, eval_sval ctx (sreg r) = Some rs # r) -> + eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs -> + seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs. +Proof. + induction 2. + - constructor. + - simpl. constructor; [| assumption]. + eapply seval_builtin_arg_correct; eauto. +Qed. + +Lemma seval_builtin_arg_exact ctx rs m sreg: forall arg varg, + (forall r, eval_sval ctx (sreg r) = Some rs # r) -> + seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg -> + eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg. +Proof. + induction arg. + all: intros varg SEVAL BARG; try (inv BARG; constructor; congruence). + - inv BARG. rewrite SEVAL in H0. inv H0. constructor. + - inv BARG. simpl. constructor. + eapply IHarg1; eauto. eapply IHarg2; eauto. + - inv BARG. simpl. constructor. + eapply IHarg1; eauto. eapply IHarg2; eauto. +Qed. + +Lemma seval_builtin_args_exact ctx rs m sreg: forall args vargs, + (forall r, eval_sval ctx (sreg r) = Some rs # r) -> + seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs -> + eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs. +Proof. + induction args. + - simpl. intros. inv H0. constructor. + - intros vargs SEVAL BARG. simpl in BARG. inv BARG. + constructor; [| eapply IHargs; eauto]. + eapply seval_builtin_arg_exact; eauto. +Qed. + +Fixpoint seval_builtin_sval ctx bsv := + match bsv with + | BA sv => SOME v <- eval_sval ctx sv IN Some (BA v) + | BA_splitlong sv1 sv2 => + SOME v1 <- seval_builtin_sval ctx sv1 IN + SOME v2 <- seval_builtin_sval ctx sv2 IN + Some (BA_splitlong v1 v2) + | BA_addptr sv1 sv2 => + SOME v1 <- seval_builtin_sval ctx sv1 IN + SOME v2 <- seval_builtin_sval ctx sv2 IN + Some (BA_addptr v1 v2) + | BA_int i => Some (BA_int i) + | BA_long l => Some (BA_long l) + | BA_float f => Some (BA_float f) + | BA_single s => Some (BA_single s) + | BA_loadstack chk ptr => Some (BA_loadstack chk ptr) + | BA_addrstack ptr => Some (BA_addrstack ptr) + | BA_loadglobal chk id ptr => Some (BA_loadglobal chk id ptr) + | BA_addrglobal id ptr => Some (BA_addrglobal id ptr) + end. + +Fixpoint eval_list_builtin_sval ctx lbsv := + match lbsv with + | nil => Some nil + | bsv::lbsv => SOME v <- seval_builtin_sval ctx bsv IN + SOME lv <- eval_list_builtin_sval ctx lbsv IN + Some (v::lv) + end. + +Lemma eval_list_builtin_sval_nil ctx lbs2: + eval_list_builtin_sval ctx lbs2 = Some nil -> + lbs2 = nil. +Proof. + destruct lbs2; simpl; repeat autodestruct; congruence. +Qed. + +Lemma seval_builtin_sval_arg ctx bs: + forall ba m v, + seval_builtin_sval ctx bs = Some ba -> + eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> + seval_builtin_arg ctx m bs v. +Proof. + induction bs; simpl; + try (intros ba m v H; inversion H; subst; clear H; + intros H; inversion H; subst; + econstructor; auto; fail). + - intros ba m v; destruct (eval_sval _ _) eqn: SV; + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; auto. + - intros ba m v. + destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. + - intros ba m v. + destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. +Qed. + +Lemma seval_builtin_arg_sval ctx m v: forall bs, + seval_builtin_arg ctx m bs v -> + exists ba, + seval_builtin_sval ctx bs = Some ba + /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v. +Proof. + induction 1. + all: try (eexists; constructor; [simpl; reflexivity | constructor]). + 2-3: try assumption. + - eexists. constructor. + + simpl. rewrite H. reflexivity. + + constructor. + - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1). + destruct IHseval_builtin_arg2 as (ba2 & A2 & B2). + eexists. constructor. + + simpl. rewrite A1. rewrite A2. reflexivity. + + constructor; assumption. + - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1). + destruct IHseval_builtin_arg2 as (ba2 & A2 & B2). + eexists. constructor. + + simpl. rewrite A1. rewrite A2. reflexivity. + + constructor; assumption. +Qed. + +Lemma seval_builtin_sval_args ctx lbs: + forall lba m v, + eval_list_builtin_sval ctx lbs = Some lba -> + list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba v -> + seval_builtin_args ctx m lbs v. +Proof. + unfold seval_builtin_args; induction lbs; simpl; intros lba m v. + - intros H; inversion H; subst; clear H. + intros H; inversion H. econstructor. + - destruct (seval_builtin_sval _ _) eqn:SV; try congruence. + destruct (eval_list_builtin_sval _ _) eqn: SVL; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst; clear H. + econstructor; eauto. + eapply seval_builtin_sval_arg; eauto. +Qed. + +Lemma seval_builtin_args_sval ctx m lv: forall lbs, + seval_builtin_args ctx m lbs lv -> + exists lba, + eval_list_builtin_sval ctx lbs = Some lba + /\ list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba lv. +Proof. + induction 1. + - eexists. constructor. + + simpl. reflexivity. + + constructor. + - destruct IHlist_forall2 as (lba & A & B). + apply seval_builtin_arg_sval in H. destruct H as (ba & A' & B'). + eexists. constructor. + + simpl. rewrite A'. rewrite A. reflexivity. + + constructor; assumption. +Qed. + +Lemma seval_builtin_sval_correct ctx m: forall bs1 v bs2, + seval_builtin_arg ctx m bs1 v -> + (seval_builtin_sval ctx bs1) = (seval_builtin_sval ctx bs2) -> + seval_builtin_arg ctx m bs2 v. +Proof. + intros. exploit seval_builtin_arg_sval; eauto. + intros (ba & X1 & X2). + eapply seval_builtin_sval_arg; eauto. + congruence. +Qed. + +Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1, + seval_builtin_args ctx m lbs1 vargs -> + forall lbs2, (eval_list_builtin_sval ctx lbs1) = (eval_list_builtin_sval ctx lbs2) -> + seval_builtin_args ctx m lbs2 vargs. +Proof. + intros. exploit seval_builtin_args_sval; eauto. + intros (ba & X1 & X2). + eapply seval_builtin_sval_args; eauto. + congruence. +Qed. + +(** * Symbolic (final) value of a block *) + +Inductive sfval := + | Sgoto (pc: exit) + | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit) + (* NB: [res] the return register is hard-wired ! Is it restrictive ? *) + | Stailcall: signature -> sval + ident -> list_sval -> sfval + | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:exit) + | Sjumptable (sv: sval) (tbl: list exit) + | Sreturn: option sval -> sfval +. + +Definition sfind_function ctx (svos : sval + ident): option fundef := + match svos with + | inl sv => SOME v <- eval_sval ctx sv IN Genv.find_funct (cge ctx) v + | inr symb => SOME b <- Genv.find_symbol (cge ctx) symb IN Genv.find_funct_ptr (cge ctx) b + end +. + +Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop := + | exec_Sgoto pc rs m: + sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs m) + | exec_Sreturn stk osv rs m m' v: + (csp ctx) = (Vptr stk Ptrofs.zero) -> + Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' -> + match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v -> + sem_sfval ctx (Sreturn osv) rs m + E0 (Returnstate (cstk ctx) v m') + | exec_Scall rs m sig svos lsv args res pc fd: + sfind_function ctx svos = Some fd -> + funsig fd = sig -> + eval_list_sval ctx lsv = Some args -> + sem_sfval ctx (Scall sig svos lsv res pc) rs m + E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc rs :: (cstk ctx)) fd args m) + | exec_Stailcall stk rs m sig svos args fd m' lsv: + sfind_function ctx svos = Some fd -> + funsig fd = sig -> + (csp ctx) = Vptr stk Ptrofs.zero -> + Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' -> + eval_list_sval ctx lsv = Some args -> + sem_sfval ctx (Stailcall sig svos lsv) rs m + E0 (Callstate (cstk ctx) fd args m') + | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs: + seval_builtin_args ctx m sargs vargs -> + external_call ef (cge ctx) vargs m t vres m' -> + sem_sfval ctx (Sbuiltin ef sargs res pc) rs m + t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs) m') + | exec_Sjumptable sv tbl pc' n rs m: + eval_sval ctx sv = Some (Vint n) -> + list_nth_z tbl (Int.unsigned n) = Some pc' -> + sem_sfval ctx (Sjumptable sv tbl) rs m + E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m) +. + +(** * Preservation properties *) + +Section SymbValPreserved. + +Variable ge ge': BTL.genv. + +Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s. + +Hypothesis senv_preserved_BTL: Senv.equiv ge ge'. + +Lemma senv_find_symbol_preserved id: + Senv.find_symbol ge id = Senv.find_symbol ge' id. +Proof. + destruct senv_preserved_BTL as (A & B & C). congruence. +Qed. + +Lemma senv_symbol_address_preserved id ofs: + Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs. +Proof. + unfold Senv.symbol_address. rewrite senv_find_symbol_preserved. + reflexivity. +Qed. + +Variable stk stk': list stackframe. +Variable f f': function. +Variable sp: val. +Variable rs0: regset. +Variable m0: mem. + +Lemma eval_sval_preserved sv: + eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv. +Proof. + induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv) + (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto. + + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto. + rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto. + erewrite eval_operation_preserved; eauto. + + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsv; auto. + + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto. + rewrite IHsv0; auto. + + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto. + rewrite IHsv1; auto. +Qed. + +Lemma seval_builtin_arg_preserved m: forall bs varg, + seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg -> + seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg. +Proof. + induction 1; simpl. + all: try (constructor; auto). + - rewrite <- eval_sval_preserved. assumption. + - rewrite <- senv_symbol_address_preserved. assumption. + - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal. +Qed. + +Lemma seval_builtin_args_preserved m lbs vargs: + seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs -> + seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs. +Proof. + induction 1; constructor; eauto. + eapply seval_builtin_arg_preserved; auto. +Qed. + +Lemma list_sval_eval_preserved lsv: + eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv. +Proof. + induction lsv; simpl; auto. + rewrite eval_sval_preserved. destruct (eval_sval _ _); auto. + rewrite IHlsv; auto. +Qed. + +Lemma smem_eval_preserved sm: + eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm. +Proof. + induction sm; simpl; auto. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto. + rewrite eval_sval_preserved; auto. +Qed. + +Lemma seval_condition_preserved cond lsv sm: + seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm. +Proof. + unfold seval_condition. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. + rewrite smem_eval_preserved; auto. +Qed. + +End SymbValPreserved. + + +(* Syntax and Semantics of symbolic internal states *) +(* [si_pre] is a precondition on initial context *) +Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg: reg -> sval; si_smem: smem }. + +(* Predicate on which (rs, m) is a possible final state after evaluating [st] on ((crs0 ctx), (cm0 ctx)) *) +Definition sem_sistate ctx (st: sistate) (rs: regset) (m: mem): Prop := + st.(si_pre) ctx + /\ eval_smem ctx st.(si_smem) = Some m + /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r). + +(* Remark that we need to reason modulo "extensionality" wrt Regmap.get about regsets. + And, nothing in their representation as (val * PTree.t val) enforces that + (forall r, rs1#r = rs2#r) -> rs1 = rs2 +*) +Lemma sem_sistate_determ ctx st rs1 m1 rs2 m2: + sem_sistate ctx st rs1 m1 -> + sem_sistate ctx st rs2 m2 -> + (forall r, rs1#r = rs2#r) /\ m1 = m2. +Proof. + intros (_&MEM1®1) (_&MEM2®2). + intuition try congruence. + generalize (REG1 r); rewrite REG2; congruence. +Qed. + +(** * Symbolic execution of final step *) +Definition sexec_final_sfv (i: final) (sis: sistate): sfval := + match i with + | Bgoto pc => Sgoto pc + | Bcall sig ros args res pc => + let svos := sum_left_map sis.(si_sreg) ros in + let sargs := list_sval_inj (List.map sis.(si_sreg) args) in + Scall sig svos sargs res pc + | Btailcall sig ros args => + let svos := sum_left_map sis.(si_sreg) ros in + let sargs := list_sval_inj (List.map sis.(si_sreg) args) in + Stailcall sig svos sargs + | Bbuiltin ef args res pc => + let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in + Sbuiltin ef sargs res pc + | Breturn or => + let sor := SOME r <- or IN Some (sis.(si_sreg) r) in + Sreturn sor + | Bjumptable reg tbl => + let sv := sis.(si_sreg) reg in + Sjumptable sv tbl + end. + +Local Hint Constructors sem_sfval: core. + +Lemma sexec_final_svf_correct ctx i sis t rs m s: + sem_sistate ctx sis rs m -> + final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> + sem_sfval ctx (sexec_final_sfv i sis) rs m t s. +Proof. + intros (PRE&MEM®). + destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto. + + (* Bcall *) intros; eapply exec_Scall; auto. + - destruct ros; simpl in * |- *; auto. + rewrite REG; auto. + - erewrite eval_list_sval_inj; simpl; auto. + + (* Btailcall *) intros. eapply exec_Stailcall; eauto. + - destruct ros; simpl in * |- *; eauto. + rewrite REG; eauto. + - erewrite eval_list_sval_inj; simpl; auto. + + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto. + eapply seval_builtin_args_correct; eauto. + + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence. +Qed. + +Local Hint Constructors final_step: core. +Local Hint Resolve seval_builtin_args_exact: core. + +Lemma sexec_final_svf_exact ctx i sis t rs m s: + sem_sistate ctx sis rs m -> + sem_sfval ctx (sexec_final_sfv i sis) rs m t s + -> final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s. +Proof. + intros (PRE&MEM®). + destruct i; simpl; intros LAST; inv LAST; eauto. + + (* Breturn *) + enough (v=regmap_optget res Vundef rs) as ->; eauto. + destruct res; simpl in *; congruence. + + (* Bcall *) + erewrite eval_list_sval_inj in *; try_simplify_someHyps. + intros; eapply exec_Bcall; eauto. + destruct fn; simpl in * |- *; auto. + rewrite REG in * |- ; auto. + + (* Btailcall *) + erewrite eval_list_sval_inj in *; try_simplify_someHyps. + intros; eapply exec_Btailcall; eauto. + destruct fn; simpl in * |- *; auto. + rewrite REG in * |- ; auto. + + (* Bjumptable *) + eapply exec_Bjumptable; eauto. + congruence. +Qed. + + +(** * symbolic execution of basic instructions *) + +Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}. + +Lemma sis_init_correct ctx: + sem_sistate ctx sis_init (crs0 ctx) (cm0 ctx). +Proof. + unfold sis_init, sem_sistate; simpl; intuition eauto. +Qed. + +Definition set_sreg (r:reg) (sv:sval) (sis:sistate): sistate := + {| si_pre:=(fun ctx => eval_sval ctx (sis.(si_sreg) r) <> None /\ (sis.(si_pre) ctx)); + si_sreg:=fun y => if Pos.eq_dec r y then sv else sis.(si_sreg) y; + si_smem:= sis.(si_smem)|}. + +Lemma set_sreg_correct ctx dst sv sis (rs rs': regset) m: + sem_sistate ctx sis rs m -> + (eval_sval ctx sv = Some rs' # dst) -> + (forall r, r <> dst -> rs'#r = rs#r) -> + sem_sistate ctx (set_sreg dst sv sis) rs' m. +Proof. + intros (PRE&MEM®) NEW OLD. + unfold sem_sistate; simpl. + intuition. + - rewrite REG in *; congruence. + - destruct (Pos.eq_dec dst r); simpl; subst; eauto. + rewrite REG in *. rewrite OLD; eauto. +Qed. + +Definition set_smem (sm:smem) (sis:sistate): sistate := + {| si_pre:=(fun ctx => eval_smem ctx sis.(si_smem) <> None /\ (sis.(si_pre) ctx)); + si_sreg:= sis.(si_sreg); + si_smem:= sm |}. + +Lemma set_smem_correct ctx sm sis rs m m': + sem_sistate ctx sis rs m -> + eval_smem ctx sm = Some m' -> + sem_sistate ctx (set_smem sm sis) rs m'. +Proof. + intros (PRE&MEM®) NEW. + unfold sem_sistate; simpl. + intuition. + rewrite MEM in *; congruence. +Qed. + +Definition sexec_op op args dst sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + set_sreg dst (Sop op args sis.(si_smem)) sis. + +Lemma sexec_op_correct ctx op args dst sis rs m v + (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = Some v) + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_op op args dst sis) (rs#dst <- v) m). +Proof. + eapply set_sreg_correct; eauto. + - simpl. destruct SIS as (PRE&MEM®). + rewrite Regmap.gss; simpl; auto. + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + - intros; rewrite Regmap.gso; auto. +Qed. + +Definition sexec_load trap chunk addr args dst sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + set_sreg dst (Sload sis.(si_smem) trap chunk addr args) sis. + +Lemma sexec_load_TRAP_correct ctx chunk addr args dst sis rs m a v + (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a) + (LOAD: Mem.loadv chunk m a = Some v) + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_load TRAP chunk addr args dst sis) (rs#dst <- v) m). +Proof. + eapply set_sreg_correct; eauto. + - simpl. destruct SIS as (PRE&MEM®). + rewrite Regmap.gss; simpl; auto. + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + - intros; rewrite Regmap.gso; auto. +Qed. + +Definition sexec_store chunk addr args src sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + let src := sis.(si_sreg) src in + let sm := Sstore sis.(si_smem) chunk addr args src in + set_smem sm sis. + +Lemma sexec_store_correct ctx chunk addr args src sis rs m m' a + (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a) + (STORE: Mem.storev chunk m a (rs # src) = Some m') + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_store chunk addr args src sis) rs m'). +Proof. + eapply set_smem_correct; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + rewrite REG; auto. +Qed. + +Lemma seval_condition_eq ctx cond args sis rs m + (SIS : sem_sistate ctx sis rs m) + :seval_condition ctx cond (list_sval_inj (map (si_sreg sis) args)) (si_smem sis) = eval_condition cond rs ## args m. +Proof. + destruct SIS as (PRE&MEM®); unfold seval_condition; simpl. + erewrite eval_list_sval_inj; simpl; auto. + erewrite MEM; auto. +Qed. + +(** * symbolic execution of blocks *) + +(* symbolic state *) +Inductive sstate := + | Sfinal (sis: sistate) (sfv: sfval) + | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate) + | Sabort + . + +(* transition (t,s) produced by a sstate in initial context ctx *) +Inductive sem_sstate ctx t s: sstate -> Prop := + | sem_Sfinal sis sfv rs m + (SIS: sem_sistate ctx sis rs m) + (SFV: sem_sfval ctx sfv rs m t s) + : sem_sstate ctx t s (Sfinal sis sfv) + | sem_Scond b cond args sm ifso ifnot + (SEVAL: seval_condition ctx cond args sm = Some b) + (SELECT: sem_sstate ctx t s (if b then ifso else ifnot)) + : sem_sstate ctx t s (Scond cond args sm ifso ifnot) + (* NB: Sabort: fails to produce a transition *) + . + +(** * Idée de l'execution symbolique en Continuation Passing Style + +[k] ci-dessous est la continuation (c-a-d. la suite de la construction de l'arbre qu'on va appliquer dans chaque branche) + +Rem: si manipuler une telle continuation s'avère compliqué dans les preuves, +il faudra faire autrement dans le modèle -- par exemple avec une structure de donnée +pour représenter l'ensemble des chemins. +(même si on peut conserver le CPS dans l'implem finale, pour l'efficacité). + +*) + +Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := + match ib with + | BF fin => Sfinal sis (sexec_final_sfv fin sis) + (* basic instructions *) + | Bnop => k sis + | Bop op args res => k (sexec_op op args res sis) + | Bload TRAP chunk addr args dst => k (sexec_load TRAP chunk addr args dst sis) + | Bload NOTRAP chunk addr args dst => Sabort (* TODO *) + | Bstore chunk addr args src => k (sexec_store chunk addr args src sis) + (* composed instructions *) + | Bseq ib1 ib2 => + sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) + | Bcond cond args ifso ifnot _ => + let args := list_sval_inj (List.map sis.(si_sreg) args) in + let ifso := sexec_rec ifso sis k in + let ifnot := sexec_rec ifnot sis k in + Scond cond args sis.(si_smem) ifso ifnot + end + . + +Definition sexec ib := sexec_rec ib sis_init (fun _ => Sabort). + +Local Hint Constructors sem_sstate: core. +Local Hint Resolve sexec_op_correct sexec_final_svf_correct + sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core. + +Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin + (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): forall sis k + (SIS: sem_sistate ctx sis rs m) + (CONT: match ofin with + | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx t s (k sis') + | Some fin => final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s + end), + sem_sstate ctx t s (sexec_rec ib sis k). +Proof. + induction ISTEP; simpl; try autodestruct; eauto. + (* condition *) + all: intros; + eapply sem_Scond; eauto; [ + erewrite seval_condition_eq; eauto | + replace (if b then sexec_rec ifso sis k else sexec_rec ifnot sis k) with (sexec_rec (if b then ifso else ifnot) sis k); + try autodestruct; eauto ]. +Qed. + +(* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) + (sexec is a correct over-approximation) +*) +Theorem sexec_correct ctx ib t s: + iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s -> + sem_sstate ctx t s (sexec ib). +Proof. + destruct 1 as (rs' & m' & fin & ISTEP & FSTEP). + eapply sexec_rec_correct; simpl; eauto. +Qed. + + +(* TODO: déplacer les trucs sur equiv_stackframe -> regmap_setres_eq dans BTL! *) +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) + . + +Local Hint Constructors equiv_stackframe equiv_state: core. + +Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf. +Proof. + destruct stf; eauto. +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: core. + 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: core. + destruct 1; intros EQ; inv EQ; econstructor; eauto. + intros; eapply eq_trans; eauto. +Qed. + +Lemma regmap_setres_eq (rs rs': regset) res vres: + (forall r, rs # r = rs' # r) -> + forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r. +Proof. + intros RSEQ r. destruct res; simpl; try congruence. + destruct (peq x r). + - subst. repeat (rewrite Regmap.gss). reflexivity. + - repeat (rewrite Regmap.gso); auto. +Qed. + +Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s: + sem_sfval ctx sfv rs1 m t s -> + (forall r, rs1#r = rs2#r) -> + exists s', equiv_state s s' /\ sem_sfval ctx sfv rs2 m t s'. +Proof. + Local Hint Resolve equiv_stack_refl equiv_state_refl regmap_setres_eq: core. + Local Hint Constructors sem_sfval: core. + destruct 1; eexists; split; econstructor; eauto. + econstructor; eauto. +Qed. + +Local Hint Resolve sexec_final_svf_exact: core. + +Definition abort_sistate ctx (sis: sistate): Prop := + ~(sis.(si_pre) ctx) + \/ eval_smem ctx sis.(si_smem) = None + \/ exists (r: reg), eval_sval ctx (sis.(si_sreg) r) = None. + +Lemma sem_sistate_exclude_abort ctx sis rs m: + sem_sistate ctx sis rs m -> + abort_sistate ctx sis -> + False. +Proof. + intros SIS ABORT. inv SIS. destruct H0 as (H0 & H0'). + inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. +Qed. + +Local Hint Resolve sem_sistate_exclude_abort: core. + +Lemma set_sreg_preserves_abort ctx sv dst sis: + abort_sistate ctx sis -> + abort_sistate ctx (set_sreg dst sv sis). +Proof. + unfold abort_sistate; simpl; intros [PRE|[MEM|REG]]; try tauto. + destruct REG as [r REG]. + destruct (Pos.eq_dec dst r) as [TEST|TEST] eqn: HTEST. + - subst; rewrite REG; tauto. + - right. right. eexists; rewrite HTEST. auto. +Qed. + +Lemma sexec_op_preserves_abort ctx op args dest sis: + abort_sistate ctx sis + -> abort_sistate ctx (sexec_op op args dest sis). +Proof. + intros; eapply set_sreg_preserves_abort; eauto. +Qed. + +Lemma sexec_load_preserves_abort ctx chunk addr args dest sis: + abort_sistate ctx sis + -> abort_sistate ctx (sexec_load TRAP chunk addr args dest sis). +Proof. + intros; eapply set_sreg_preserves_abort; eauto. +Qed. + +Lemma set_smem_preserves_abort ctx sm sis: + abort_sistate ctx sis -> + abort_sistate ctx (set_smem sm sis). +Proof. + unfold abort_sistate; simpl; try tauto. +Qed. + +Lemma sexec_store_preserves_abort ctx chunk addr args src sis: + abort_sistate ctx sis + -> abort_sistate ctx (sexec_store chunk addr args src sis). +Proof. + intros; eapply set_smem_preserves_abort; eauto. +Qed. + +Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort + sexec_store_preserves_abort: core. + +Lemma sexec_exclude_abort ctx ib t s1: forall sis k + (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k)) + (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False) + (ABORT: abort_sistate ctx sis), + False. +Proof. + induction ib; simpl; intros; eauto. + - (* final *) inversion SEXEC; subst; eauto. + - (* load *) destruct trap; eauto. + inversion SEXEC. + - (* seq *) + eapply IHib1; eauto. + simpl. eauto. + - (* cond *) + inversion SEXEC; subst; eauto. clear SEXEC. + destruct b; eauto. +Qed. + +Lemma set_sreg_abort ctx dst sv sis rs m: + sem_sistate ctx sis rs m -> + (eval_sval ctx sv = None) -> + abort_sistate ctx (set_sreg dst sv sis). +Proof. + intros (PRE&MEM®) NEW. + unfold sem_sistate, abort_sistate; simpl. + right; right. + exists dst; destruct (Pos.eq_dec dst dst); simpl; try congruence. +Qed. + +Lemma sexec_op_abort ctx sis op args dest rs m + (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = None) + (SIS: sem_sistate ctx sis rs m) + : abort_sistate ctx (sexec_op op args dest sis). +Proof. + eapply set_sreg_abort; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. +Qed. + +Lemma sexec_load_TRAP_abort ctx chunk addr args dst sis rs m + (EVAL: forall a, eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a -> Mem.loadv chunk m a = None) + (SIS: sem_sistate ctx sis rs m) + : abort_sistate ctx (sexec_load TRAP chunk addr args dst sis). +Proof. + eapply set_sreg_abort; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + intros; autodestruct; try_simplify_someHyps. +Qed. + +Lemma set_smem_abort ctx sm sis rs m: + sem_sistate ctx sis rs m -> + eval_smem ctx sm = None -> + abort_sistate ctx (set_smem sm sis). +Proof. + intros (PRE&MEM®) NEW. + unfold abort_sistate; simpl. + tauto. +Qed. + +Lemma sexec_store_abort ctx chunk addr args src sis rs m + (EVAL: forall a, eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a -> Mem.storev chunk m a (rs # src) = None) + (SIS: sem_sistate ctx sis rs m) + :abort_sistate ctx (sexec_store chunk addr args src sis). +Proof. + eapply set_smem_abort; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + intros; rewrite REG; autodestruct; try_simplify_someHyps. +Qed. + +Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort: core. + +Lemma sexec_rec_exact ctx ib t s1: forall sis k + (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k)) + rs m + (SIS: sem_sistate ctx sis rs m) + (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False) + , + match iblock_istep_run (cge ctx) (csp ctx) ib rs m with + | Some (out rs' m' (Some fin)) => + exists s2, final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2 + | Some (out rs' m' None) => exists sis', (sem_sstate ctx t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m') + | None => False + end. +Proof. + induction ib; simpl; intros; eauto. + - (* final *) + inv SEXEC. + exploit (sem_sistate_determ ctx sis rs m rs0 m0); eauto. + intros (REG&MEM); subst. + exploit (sem_sfval_equiv rs0 rs); eauto. + intros (s2 & EQUIV & SFV'). + eexists; split; eauto. + - (* Bop *) autodestruct; eauto. + - destruct trap; [| inv SEXEC ]. + repeat autodestruct; eauto. + all: intros; eapply CONT; eauto; + eapply sexec_load_TRAP_abort; eauto; + intros; try_simplify_someHyps. + - repeat autodestruct; eauto. + all: intros; eapply CONT; eauto; + eapply sexec_store_abort; eauto; + intros; try_simplify_someHyps. + - (* Bseq *) + exploit IHib1; eauto. clear sis SEXEC SIS. + { simpl; intros; eapply sexec_exclude_abort; eauto. } + destruct (iblock_istep_run _ _ _ _ _) eqn: ISTEP; auto. + destruct o. + destruct _fin eqn: OFIN; simpl; eauto. + intros (sis1 & SEXEC1 & SIS1). + exploit IHib2; eauto. + - (* Bcond *) + inv SEXEC. + erewrite seval_condition_eq in SEVAL; eauto. + rewrite SEVAL. + destruct b. + + exploit IHib1; eauto. + + exploit IHib2; eauto. +Qed. + + +(* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution + (sexec is exact). +*) +Theorem sexec_exact ctx ib t s1: + sem_sstate ctx t s1 (sexec ib) -> + exists s2, iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2 + /\ equiv_state s1 s2. +Proof. + intros; exploit sexec_rec_exact; eauto. + { intros sis' SEXEC; inversion SEXEC. } + repeat autodestruct; simpl; try tauto. + - intros D1 D2 ISTEP (s2 & FSTEP & EQSTEP); subst. + eexists; split; eauto. + repeat eexists; eauto. + erewrite iblock_istep_run_equiv; eauto. + - intros D1 D2 ISTEP (sis & SEXEC & _); subst. + inversion SEXEC. +Qed. + diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md new file mode 100644 index 00000000..bd70e273 --- /dev/null +++ b/scheduling/BTLroadmap.md @@ -0,0 +1,353 @@ +# BTL Development Roadmap + +BTL aims to be an IR dedicated to defensive certification of middle-end optimizations (before register allocation). +It provides a CFG of "loop-free" blocks, where each block is run in one step emitting at most a single observational event. +The "local" optimizations (i.e. preserving "locally" the semantics of such blocks) would be checked by symbolic execution with rewriting rules. +The only info required from oracles: a "dupmap" mapping block entries. +In contrast, the "global" optimizations would require some invariants annotations at block entry (provided by oracles). + +Examples of optimizations that we aim to support: + + - instruction scheduling + - instruction rewritings (instruction selection) + - branch duplication, "if-lifting" (e.g. side-exit moved up in "traces"). + - strength-reduction + - SSA optimizations + +We sketch below the various kinds of supported optimizations in development order... + +## Introduction + +En gros la syntaxe d'un bloc BTL est définie par: + + Inductive iblock: Type := + | ... (* instructions basiques ou "finales" (call, return, goto, etc) *) + | Bseq (b1 b2: iblock) (* séquence de deux blocs *) + | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (* if-then-else *) + +Le modèle de base de l'exécution symbolique représente un tel bloc par un état symbolique de type: + + Inductive sstate := + | Sfinal (sis: sistate) (sfv: sfval) + | Scond (cond: condition) (args: list_sval) (ifso ifnot: sstate) + | Sabort + . + +où `sistate` est un PPA (preconditioned parallel assignment) des registres et `sfval` représente un branchement (call, return, goto, etc). + +Autrement dit, un état symbolique représente tous les chemins +d'exécution possibles par une sorte de gros BDD ayant sur les feuilles +un `Sfinal` (ou un `Sabort` s'il manque une instruction de branchement sur ce chemin). + +## Block boundaries, branch duplication or factorization + +Two possibility of branch duplications (e.g tail-duplication, loop unrolling, etc): + +- during RTL -> BTL (while "building" BTL blocks) +- during BTL -> BTL. Typically, the "if-lifting" à la Justus could be performed/verified in a single pass here ! + +Branch factorization should also be possible in BTL -> RTL pass. Example: revert "loop-unrolling". + +**IMPLEM NOTE:** in a first step a single verifier for RTL -> BTL and BTL -> RTL simulations, with a dupmap: BTL block-entries -> RTL nodes. + + +**CURRENT STATUS** + +- verifier: implemented and proved w.r.t match_iblock specification. +- Proof: + - BTL -> RTL: done. + - RTL -> BTL: done. +- Oracles: + - BTL -> RTL: TODO. + - RTL -> BTL: started. + +**TODO** + +- lien BTL/RTL: autoriser le BTL à avoir des Bnop en plus du RTL, e.g. pour autoriser des "if-then" sans else. +Pour faciliter le vérificateur, faire comme le Bgoto: les Bnop en "trop" ne sont autorisés que s'il y a eu une instruction RTL avant. +Ajouter aussi un booléen (positionné par l'oracle) sur le Bnop qui indique si le "nop" existe ou pas au niveau RTL. + +## Simulation modulo liveness and "Functional" semantics of BTL blocks + +L'approche suivie pour réaliser la simulation modulo liveness dans +RTLpath est compliquée à adapter sur BTL. En effet, un état +symbolique RTLpath correspond à un état symbolique BTL très +particulier: toutes les "feuilles" (les `Sfinal`) sont des `Sgoto` +sauf éventuellement une. Or, dans RTLpath, le traitement de l'info de liveness sur +cette feuille particulière est très adhoc et laborieux (cf. `pre_output_regs`). On +n'a pas envie de généraliser cette usine à gaz. + +On cherche donc une façon plus abstraite de faire... On a l'idée de +coder la "simulation modulo liveness" dans une "simulation +less_undef". Ça peut rendre le cadre du test de simulation plus +simple et plus général. + +L'idée de départ: "Extends BTL with the possibility of destroying a +set of registers at each exit (a destroyed register is simply set to +Vundef)" en prouvant une simulation "less_undef" n'est pas assez +générale! Ça n'autorise pas à introduire de "nouveaux" registres dans +le bloc transformé, juste à donner n'importe quelle valeur aux +registres "hors-liveout". + +**Idée corrigée** à côté de la sémantique "à la RTL" pour BTL, on +définit une nouvelle sémantique (basée sur la même sémantique à grand +pas dans les blocs), où c'est juste "l'entrée dans un bloc" qui change +de sémantique. Intuitivement, cette nouvelle sémantique considère +chaque bloc comme une sorte de fonction paramétrée par les `input_regs` +et appelée uniquement en "tailcall" (via les "goto"). C'est ce qu'on +va appeler la "functional semantics" de BTL (l'autre étant appelée +qqchose comme "CFG semantics" ?). + +Autrement dit, sur l'entrée dans un bloc pour un état (rs,m), on +remplace juste cet état par un nouvel état (rs0,m) où dans rs0, tous les registres +sont initialisés à Vundef sauf ceux du `input_regs` qui sont +initialisés comme une copie de "rs". In fine, on applique le +"iblock_step" sur cet état (rs0,m). + +**NOTE** cette idée de voir les blocs comme des "fonctions" correpond bien à la représentation "SSA" à la Appel/MLIR. +Donc cette sémantique peut servir de base pour un support de formes SSA (partielles ou totales) dans BTL. +Pour l'encodage de SSA, il suffira d'étendre le mécanisme d'initialisation du "rs0" d'un bloc avec un passage de paramètres. + +**IMPLEM PLAN** + +1. définir the "functional semantics" of BTL. +2. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep"). +3. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics. + en gros: on implémente un vérificateur des infos de liveness. + c'est la correction du "input_regs" qui garantit que la simulation est correct. + La preuve devrait normalement être très similaire à RTLpathLivegenproof. + + +## "Basic" symbolic execution / symbolic simulation + +We will implement a "basic" (e.g without rewriting rules) "less_undef" simulation test for BTL.FunctionalSemantics. + +**IMPLEM NOTE** + +- use Continuation Passing Style for an easy recursive generation of "all execution paths". +- pour implementer la "functional semantics", il faut changer + légèrement la sémantique du map qui associe une valeur symbolique à + chaque registre. En RTLpath, un registre "absent" de la map était considéré comme positionné à sa valeur initial. + Là, il faudra considérer qu'il vaut Vundef (il y a une valeur symbolique spéciale à ajouter !) + +**CURRENT STATUS** + +- model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms. +- next step: high-level specification of "symbolic simulation" + preservation proof w.r.t BTL.FunctionalSemantics +(dans une première étape, on peut laisser le "less_undef" de côté: ce sera facile à ajouter quand le cadre sera en place). + +## Port of RTLpath optimizations to BTL + +- Generalize superblock scheduling for a notion of "extended-blocks" such that each instruction of a block, except the block entry, has a single predecessor in the block. +- Port rewriting rules of RTLpath. +- Justus's "poor man SSA" + if-lifting. + +## Efficient comparison (guided by oracles) of "if-then-else" sequences. + +Le pb est complexe. Comparer des expressions booleennes contenant juste des variables booleennes est déjà NP-complet, avec "explosion exponentielle" dans le pire cas. + +Approche proposée: utiliser un mécanisme de vérification "simple", basée sur une comparaison par execution symbolique de "tous" les chemins d'execution (cf Intro ci-dessus). +Ça pète exponentiellement dans le pire cas: mais on pourra contrôler ce risque d'explosion par les oracles... + +Ci-dessous, on liste quelques "techniques" de collaboration oracle/vérificateur pour contrôler l'explosion des chemins. +Idée: les conditions comportent une liste d'annotations qui permet le guidage du vérificateur par l'oracle. + +### Contrôle des "joins internes" dans le bloc. + +Si dans le bloc, toute condition a au plus un "predecesseur" (au sens +du CFG RTL) dans le bloc: alors le nombre de "chemins sémantiques" +(explorés par l'exécution symbolique) est identique au nombre de +"branches syntaxiques" (présents dans le code). Une façon simple de +contrôler l'explosion de l'exécution symbolique est de fabriquer (avec +les oracles) des blocs avec un nombre borné (petit) de "joins +internes". + +**Exemple d'application: généralisation des superblocks** + +On considère le bloc BTL ci-dessous (où les `i*` sont des séquences d'instructions basiques sans branchement): + + i0; + if (c1) { i1 } else { i1'; goto pc1 } + if (c2) { i2; goto pc2 } else { i2' } + if (c3} { i3; goto pc3 } else { i3'; goto pc3' } + +Sur un tel bloc, il n'y a aucun "join interne" (l'exécution symbolique est donc linéaire). +Mais représenter en RTLpath un tel bloc nécessite au moins 4 blocks (1 superbloc et 3 basic-blocs): + + i0; c1; i1; c2; i2'; i3'; goto pc3' + i1'; goto pc1 + i2; goto pc2 + i3; goto pc3 + +La vérification BTL sur le gros bloc ne prendra à priori pas plus de +temps que la vérification RTLpath cumulée des 4 "petits" blocs. Mais +la vérification BTL sera plus *puissante*, puisque que quand on va +vérifier les chemins d'exécutions correspondant à ceux des 3 +basic-blocs, on aura le `i0` en plus dans l'état symbolique (i.e. un +"contexte d'exécution" plus précis). + +**Autre exemple d'application: le if-lifting à la Justus** + +Le superblock suivant: + + y1 = e1(x) + x = e2(a) + y2 = e3(x) + if (c[x]) { goto pc } else { i4; goto pc' } + +peut être directement montré équivalent à + + x' = e2(a) // x' un registre "frais" (pas dans les "liveout") + if (c[x']) { + y1 = e1(x); + x = x'; + y2 = e3(x); + goto pc + } else { + y1 = e1(x); + x = x'; + y2 = e3(x); + i4; + goto pc' + } + +Ici, la duplication de branche a donc lieu en BTL. + +L'exécution symbolique de ces deux blocs va produire deux BDD comparables (avec comparaison des feuilles modulo liveness). + +### Comparaison des BDD (modulo réordonnancement des conditions ?) + +On peut avoir envie de montrer que les deux blocs ci-dessous sont équivalents (si les dépendences sur les variables le permettent): + + if (c1) { i1 } else { i1' } + if (c2) { i2 } else { i2' } + +et + + if (c2) { i2 } else { i2' } + if (c1) { i1 } else { i1' } + +Ça revient (en gros) à comparer les BDD: + + if (c1) { if (c2) {i1;i2} else {i1;i2'} } else { if (c2) {i1';i2} else {i1';i2'} } + +et + + if (c2) { if (c1) {i2;i1} else {i2;i1'} } else { if (c1) {i2';i1} else {i2';i1'} } + +Pour gérer ça, on peut faire des "Ordered BDD": l'oracle du **bloc +transformé** annote (certaines) conditions avec des numéros de façon à +ce l'exécution symbolique du bloc transformé produise un "BDD" qui +correspond à celui du bloc d'origine (cf. "Principe" +ci-dessous). Cependant, il semble difficile d'appliquer complètement +les techniques de mémoïsation des BDD ayant des booléens sur les +feuilles. Car ici on veut effectuer une comparaison sur des feuilles +2 à 2 qui n'est pas une égalité, mais une inclusion ! + +**Principe du réordonnancement de BDD:** l'exécution symbolique du **bloc transformé** réordonne le BDD de +façon à respecter la numérotation: un pére doit avoir un numéro inférieur à +chacun de ses fils (en l'absence de numéro, on ignore les contraintes +de numérotation entre ce noeud est ses voisins). Exemple ci-dessous +avec trois conditions distinctes (pour order c1 < c2 < c3): + + if (c3) { if (c1) {f1} else {f1'} } else { if (c2} {f2} else {f2'} } + +est réordonné en + + if (c1) { if (c2) { if (c3) {f1} else {f2} } else { if (c3) {f1} else {f2'} } } + else { if (c2) { if (c3) {f1'} else {f2} } else { if (c3) {f1'} else {f2'} } } + +**rem:** on ajoute ici un undefined behavior potentiel à cause l'execution de c2 quand c3 est vrai. +Mais si le **bloc d'origine** est simulé par cet état symbolique réordonné, c'est correct. +Le bloc transformé a juste supprimé un test inutile... + +Bon, à voir si le principe ci-dessus est vraiment utile dans toute sa +généralité. Pour simplifier, on peut aussi restreindre le +réordonnancement du BDD aux cas où il n'y a pas de test redondant +inséré (comme dans l'exemple initial). + +**Version simplifiée: comparaison des BDD sans réordonnancement des conditions** + +Dans un premier temps (jusqu'à ce qu'on trouve une optimisation où ça pourrait être utile): pas de réordonnacement des BDD. +On autorise juste le BDD du bloc transformé à supprimer des conditions par rapport au bloc d'origine. +Autrement dit, dans la comparaison récursive de `{if (c) BDD1 BDD2}` avec `{if (c') BDD1' BDD2}'`: + +- soit `c=c'` et on compare récursivement `BDD1` avec `BDD1'` et `BDD2` avec `BDD2'`. +- soit `c<>c'` et on compare récursivement `BDD1` et `BDD2` avec `{if (c') BDD1' BDD2'}` + +Ce deuxième cas correspond au fait que le test sur `c` dans le bloc d'origine était inutile! + +### Propagation de valeurs symbolique de conditions (et élimination de condition) pendant l'execution symbolique + +L'exécution symbolique se propageant en "avant", on peut propager les valeurs des conditions symboliques, qu'on peut utiliser pour éliminer des conditions redondantes +(et donc limiter l'explosion du nombre de chemin). + +Pour rendre ce mécanisme efficace et puissant, on peut guider ce mécanisme de propagation/élimination avec des annotations introduites par les oracles. + +- une annotation "bind_to x" qui indique de mémoriser la valeur (soit "true" soit "false" suivant la branche) de la condition symbolique avec le nom "x" +- une annotation "eval_to b proof" qui indique que la condition s'évalue sur la constante "b", ce qui est prouvable avec la preuve "proof". + +Ici on peut imaginer un langage plus ou moins compliqué pour prouver l'évaluation des conditions. La version la plus simple: + +- "eq(x)" dit simplement que la condition symbolique est syntaxiquement égale celle appelée "x". +- "eqnot(x)" dit que c'est la négation. + +Dans le cas général, on peut introduire tout un système de réécriture pour éliminer les conditions. + +En fait, il serait sans doute intéressant de mettre en place un +"système de réécriture guidé par oracle" pour toutes les instructions +BTL. Ça permet de concilier "puissance" de l'exécution symbolique et +"efficacité". L'exécution symbolique va pouvoir éventuellement faire +des réécritures compliquées, mais uniquement quand c'est nécessaire. + +**Exemple: une "if-conversion" généralisée** +On aimerait montrer que le bloc d'origine: + + if (c) { + x1 = e1 + x2 = e2 + y = e + x3 = e3 + } else { + x3 = e3' + z = e' + x1 = e1' + x2 = e2' + } + +est simulable par le bloc transformé: + + x1 = (c?e1:e1') + x2 = (c?e2:e2') + x3 = (c?e3:e3') + if (c) { y = e } else { z = e' } + +une solution: ajouter une régle de réécriture `x = (c?e:e')` en `if (c) { x=e } else {x=e'}` +(attention, ce n'est pas une règle de réécriture sur les valeurs +symboliques, mais sur du code BTL lui-même, avant l'exécution +symbolique de ce code). + +L'exécution symbolique ouvre alors deux branches `c=true` et +`c=false` sur `x1 = (c?e1:e1')`, puis la propagation/élimination de la +condition symbolique `c` simplifie les conditionnelles sur `x2`, `x3` et `y`/`z`. +Au final, on obtient deux BDD identiques sur cet exemple (sans explosion combinatoire). + +**Rem** les mécanismes de propagation/réécritures décrits ci-dessus peuvent être aussi très utile pour la simulation symbolique modulo invariants (cf. ci-dessous) ! + +## Invariants at block entry + +Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. + +Case-study: support of strength-reduction. + +## Support of SSA-optimizations + +Extends BTL with "register renamings" at exits. + +This should enable to represent SSA-forms in BTL IR, more or less like in MLIR. + +## Alias analysis in the symbolic simulation + +A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf) + + 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..08a77ae4 --- /dev/null +++ b/scheduling/BTLtoRTLproof.v @@ -0,0 +1,403 @@ +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. + +Require Import Linking. + +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) + . + +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. + - eapply verify_is_copy_correct; eauto. +Qed. + +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. + +Lemma find_function_preserved ri rs0 fd + (FIND : find_function ge ri rs0 = Some fd) + : exists fd', RTL.find_function tge ri rs0 = Some fd' + /\ transf_fundef fd = OK fd'. +Proof. + pose symbols_preserved as SYMPRES. + destruct ri. + + simpl in FIND; apply functions_translated in FIND. + destruct FIND as (tf & cunit & TFUN & GFIND & LO). + eexists; split. eauto. assumption. + + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. + apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF). + eexists; split. simpl. rewrite symbols_preserved. + rewrite GFS. eassumption. assumption. +Qed. + +(* Inspired from Duplicateproof.v *) +Lemma list_nth_z_dupmap: + forall dupmap ln ln' (pc pc': node) val, + list_nth_z ln val = Some pc -> + list_forall2 (fun n n' => dupmap!n = Some n') ln ln' -> + exists (pc': node), + list_nth_z ln' val = Some pc' + /\ dupmap!pc = Some pc'. +Proof. + induction ln; intros until val; intros LNZ LFA. + - inv LNZ. + - inv LNZ. destruct (zeq val 0) eqn:ZEQ. + + inv H0. destruct ln'; inv LFA. + simpl. exists n. split; auto. + + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto. +Qed. + +(* variant of [star RTL.step] but requiring proposition [P] on the [refl] (stutttering) case. *) +Inductive cond_star_step (P: Prop): RTL.state -> trace -> RTL.state -> Prop := + | css_refl s: P -> cond_star_step P s E0 s + | css_plus s1 t s2: plus RTL.step tge s1 t s2 -> cond_star_step P s1 t s2 + . + +Lemma css_plus_trans P Q s0 s1 s2 t: + plus RTL.step tge s0 E0 s1 -> + cond_star_step P s1 t s2 -> + cond_star_step Q s0 t s2. +Proof. + intros PLUS STAR. + eapply css_plus. + inv STAR; auto. + eapply plus_trans; eauto. +Qed. + +Lemma css_star P s0 s1 t: + cond_star_step P s0 t s1 -> + star RTL.step tge s0 t s1. +Proof. + destruct 1. + - eapply star_refl; eauto. + - eapply plus_star; eauto. +Qed. + +Local Hint Constructors RTL.step match_states: core. +Local Hint Resolve css_refl plus_one transf_fundef_correct: core. + +Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin + (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin): + forall pc0 opc isfst + (MIB: match_iblock dupmap (RTL.fn_code f') isfst pc0 ib opc), + match ofin with + | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) + | Some fin => + exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin None + /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) + end. +Proof. + induction IBIS; simpl; intros. + - (* exec_final *) + assert (X: opc = None). { inv MIB; auto. } + subst. + repeat eexists; eauto. + - (* exec_nop *) + inv MIB. exists pc'; split; eauto. + - (* exec_op *) + inv MIB. exists pc'; split; auto. + apply plus_one. eapply exec_Iop; eauto. + erewrite <- eval_operation_preserved; eauto. + intros; rewrite symbols_preserved; trivial. + - (* exec_load *) + inv MIB. exists pc'; split; auto. + apply plus_one. eapply exec_Iload; eauto. + erewrite <- eval_addressing_preserved; eauto. + intros; rewrite symbols_preserved; trivial. + - (* exec_store *) + inv MIB. exists pc'; split; auto. + apply plus_one. eapply exec_Istore; eauto. + erewrite <- eval_addressing_preserved; eauto. + intros; rewrite symbols_preserved; trivial. + - (* exec_seq_stop *) + inv MIB; eauto. + - (* exec_seq_continue *) + inv MIB. + exploit IHIBIS1; eauto. + intros (pc1 & EQpc1 & STEP1); inv EQpc1. + exploit IHIBIS2; eauto. + destruct ofin; simpl. + + intros (ifst2 & pc2 & M2 & STEP2). + repeat eexists; eauto. + eapply css_plus_trans; eauto. + + intros (pc2 & EQpc2 & STEP2); inv EQpc2. + eexists; split; auto. + eapply plus_trans; eauto. + - (* exec_cond *) + inv MIB. + rename H10 into JOIN. (* is_join_opt opc1 opc2 opc *) + destruct b; exploit IHIBIS; eauto. + + (* taking ifso *) + destruct ofin; simpl. + * (* ofin is Some final *) + intros (isfst' & pc1 & MI & STAR). + repeat eexists; eauto. + eapply css_plus_trans; eauto. + * (* ofin is None *) + intros (pc1 & OPC & PLUS). inv OPC. + inv JOIN; eexists; split; eauto. + all: + eapply plus_trans; eauto. + + (* taking ifnot *) + destruct ofin; simpl. + * (* ofin is Some final *) + intros (isfst' & pc1 & MI & STAR). + repeat eexists; eauto. + eapply css_plus_trans; eauto. + * (* ofin is None *) + intros (pc1 & OPC & PLUS). subst. + inv JOIN; eexists; split; eauto. + all: + eapply plus_trans; eauto. +Qed. + +Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s + (STACKS : list_forall2 match_stackframes stack stack') + (TRANSF : match_function dupmap f f') + (FS : final_step ge stack f sp rs1 m1 fin t s) + (i : instruction) + (ATpc1 : (RTL.fn_code f') ! pc1 = Some i) + (MF : match_final_inst dupmap fin i) + : exists s', RTL.step tge (RTL.State stack' f' sp pc1 rs1 m1) t s' /\ match_states s s'. +Proof. + inv MF; inv FS. + - (* return *) + eexists; split. + eapply exec_Ireturn; eauto. + erewrite <- preserv_fnstacksize; eauto. + econstructor; eauto. + - (* call *) + rename H7 into FIND. + exploit find_function_preserved; eauto. + intros (fd' & FIND' & TRANSFU). + eexists; split. eapply exec_Icall; eauto. + apply function_sig_translated. assumption. + repeat (econstructor; eauto). + - (* tailcall *) + rename H2 into FIND. + exploit find_function_preserved; eauto. + intros (fd' & FIND' & TRANSFU). + eexists; split. eapply exec_Itailcall; eauto. + apply function_sig_translated. assumption. + erewrite <- preserv_fnstacksize; eauto. + repeat (econstructor; eauto). + - (* builtin *) + pose symbols_preserved as SYMPRES. + eexists. split. + eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + econstructor; eauto. + - (* jumptable *) + pose symbols_preserved as SYMPRES. + exploit list_nth_z_dupmap; eauto. intros (pc'1 & LNZ & REVM). + eexists. split. + eapply exec_Ijumptable; eauto. + econstructor; eauto. +Qed. + +Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s + (STACKS: list_forall2 match_stackframes stack stack') + (TRANSF: match_function dupmap f f') + (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin)) + (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None) + (FS : final_step ge stack f sp rs1 m1 fin t s) + : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'. +Proof. + intros; exploit iblock_istep_simulation; eauto. + simpl. intros (isfst' & pc1 & MI & STAR). clear IBIS MIB. + inv MI. + - (* final inst except goto *) + exploit final_simu_except_goto; eauto. + intros (s' & STEP & MS). eexists; split. + + eapply plus_right. + eapply css_star; eauto. + eapply STEP. econstructor. + + eapply MS. + - (* goto *) + inv FS. + inv STAR; try congruence. + eexists; split. eauto. + econstructor; eauto. +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'. +Proof. + destruct 1; intros; inv MS. + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (ib' & FNC & MIB). + try_simplify_someHyps. destruct STEP as (rs' & m' & fin & IBIS & FS). + intros; exploit iblock_step_simulation; eauto. + (* exec_function_internal *) + - inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split. + + eapply plus_one. apply RTL.exec_function_internal. + erewrite <- preserv_fnstacksize; eauto. + + erewrite <- preserv_fnparams; eauto. + eapply match_states_intro; eauto. + apply dupmap_entrypoint. assumption. + (* exec_function_external *) + - inversion TRANSF as [|]; subst. eexists. split. + + eapply plus_one. econstructor. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor. assumption. + (* exec_return *) + - inversion STACKS as [|a1 al b1 bl H1 HL]; subst. + destruct b1 as [res' f' sp' pc' rs']. + eexists. split. + + eapply plus_one. constructor. + + inv H1. econstructor; eauto. +Qed. + +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. diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v new file mode 100644 index 00000000..e9319315 --- /dev/null +++ b/scheduling/RTLtoBTL.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 rtl2btl: RTL.function -> BTL.code * node * (PTree.t node). + +Local Open Scope error_monad_scope. + +Definition transf_function (f: RTL.function) : res BTL.function := + let (tcte, dupmap) := rtl2btl f in + let (tc, te) := tcte in + let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) tc te in + do u <- verify_function dupmap f' f; + OK f'. + +Definition transf_fundef (f: RTL.fundef) : res fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: RTL.program) : res program := + transform_partial_program transf_fundef p. diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v new file mode 100644 index 00000000..633e1b8e --- /dev/null +++ b/scheduling/RTLtoBTLproof.v @@ -0,0 +1,744 @@ +Require Import Coqlib Maps Lia. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad BTL. + +Require Import Errors Linking RTLtoBTL. + +Require Import Linking. + +Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := { + dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f); + dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f); + preserv_fnsig: fn_sig tf = RTL.fn_sig f; + preserv_fnparams: fn_params tf = RTL.fn_params f; + preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f +}. + +Inductive match_fundef: RTL.fundef -> fundef -> Prop := + | match_Internal dupmap f tf: match_function dupmap f tf -> match_fundef (Internal f) (Internal tf) + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: RTL.stackframe -> 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 (RTL.Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs). + +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. + - eapply verify_is_copy_correct; eauto. +Qed. + +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: 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 BTL_SIMULATES_RTL. + +Variable prog: RTL.program. +Variable tprog: program. + +Hypothesis TRANSL: match_prog prog tprog. + +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Local Open Scope nat_scope. + +(** * Match relation from a RTL state to a BTL state + +The "option iblock" parameter represents the current BTL execution state. +Thus, each RTL single step is symbolized by a new BTL "option iblock" +starting at the equivalent PC. + +The simulation diagram for match_states_intro is as follows: + +<< + + RTL state match_states_intro BTL state + [pcR0,rs0,m0] --------------------------- [pcB0,rs0,m0] + | | + | | + RTL_RUN | *E0 | BTL_RUN + | | + | MIB | + [pcR1,rs1,m1] ------------------------------- [ib] + +>> +*) + +Inductive match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst: Prop := + | match_strong_state_intro + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function dupmap f f') + (ATpc0: (fn_code f')!pcB0 = Some ib0) + (DUPLIC: dupmap!pcB0 = Some pcR0) + (MIB: match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None) + (IS_EXPD: is_expand ib) + (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs1 m1)) + (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs1 m1) + : match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst + . + +Inductive match_states: (option iblock) -> RTL.state -> state -> Prop := + | match_states_intro + dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst + (MSTRONG: match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst) + (NGOTO: is_goto ib = false) + : match_states (Some ib) (RTL.State st f sp pcR1 rs1 m1) (State st' f' sp pcB0 rs0 m0) + | match_states_call + st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f') + : match_states None (RTL.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 None (RTL.Returnstate st v m) (Returnstate st' v m) + . + +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: RTL.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 -> funsig tf = RTL.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: + RTL.initial_state prog s1 -> + exists ib s2, initial_state tprog s2 /\ match_states ib s1 s2. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF). + eexists. 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 ib s1 s2 r: + match_states ib s1 s2 -> RTL.final_state s1 r -> final_state s2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Lemma find_function_preserved ri rs0 fd + (FIND : RTL.find_function ge ri rs0 = Some fd) + : exists fd', find_function tge ri rs0 = Some fd' + /\ transf_fundef fd = OK fd'. +Proof. + pose symbols_preserved as SYMPRES. + destruct ri. + + simpl in FIND; apply functions_translated in FIND. + destruct FIND as (tf & cunit & TFUN & GFIND & LO). + eexists; split. eauto. assumption. + + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. + apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF). + eexists; split. simpl. rewrite symbols_preserved. + rewrite GFS. eassumption. assumption. +Qed. + +(** Representing an intermediate BTL state + +We keep a measure of code that remains to be executed with the omeasure +type defined below. Intuitively, each RTL step corresponds to either + - a single BTL step if we are on the last instruction of the block + - no BTL step (as we use a "big step" semantics) but a change in + the measure which represents the new intermediate state of the BTL code + *) +Fixpoint measure ib: nat := + match ib with + | Bseq ib1 ib2 + | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2 + | ib => 1 + end. + +Definition omeasure (oib: option iblock): nat := + match oib with + | None => 0 + | Some ib => measure ib + end. + +Remark measure_pos: forall ib, + measure ib > 0. +Proof. + induction ib; simpl; auto; lia. +Qed. + +Lemma entry_isnt_goto dupmap f pc ib: + match_iblock dupmap (RTL.fn_code f) true pc (entry ib) None -> + is_goto (entry ib) = false. +Proof. + intros. + destruct (entry ib); trivial. + destruct fi; trivial. inv H. inv H4. +Qed. + +Lemma expand_entry_isnt_goto dupmap f pc ib: + match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None -> + is_goto (expand (entry ib) None) = false. +Proof. + destruct (is_goto (expand (entry ib) None))eqn:EQG. + - destruct (expand (entry ib) None); + try destruct fi; try discriminate; trivial. + intros; inv H; inv H4. + - destruct (expand (entry ib) None); + try destruct fi; try discriminate; trivial. +Qed. + +Lemma list_nth_z_rev_dupmap: + forall dupmap ln ln' (pc pc': node) val, + list_nth_z ln val = Some pc -> + list_forall2 (fun n' n => dupmap!n' = Some n) ln' ln -> + exists (pc': node), + list_nth_z ln' val = Some pc' + /\ dupmap!pc' = Some pc. +Proof. + induction ln; intros until val; intros LNZ LFA. + - inv LNZ. + - inv LNZ. destruct (zeq val 0) eqn:ZEQ. + + inv H0. destruct ln'; inv LFA. + simpl. exists p. split; auto. + + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto. + intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. +Qed. + +Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1: + forall (ISTEP: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin1) + k ofin2 rs2 m2 + (CONT: match ofin1 with + | None => + (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None) + \/ (exists rem, k = Some rem + /\ iblock_istep tge sp rs1 m1 rem rs2 m2 ofin2) + | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1 + end), + iblock_istep tge sp rs0 m0 (expand ib k) rs2 m2 ofin2. +Proof. + induction 1; simpl. + { (* BF *) + intros ? ? ? ? (HRS & HM & HOF); subst. + constructor. } + (*destruct k; intros. try inv CONT.*) + 1-4: (* Bnop, Bop, Bload, Bstore *) + destruct k; intros; destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; + subst; try (inv HK; fail); try (inv HR; fail); try (econstructor; eauto; fail); + inversion HR; subst; clear HR; + eapply exec_seq_continue; [ econstructor; eauto | assumption]. + - (* Bseq_stop *) + destruct k; intros; apply IHISTEP; eauto. + - (* Bseq_continue *) + destruct ofin; intros. + + destruct CONT as [HRS [HM HOF]]; subst. + eapply IHISTEP1; right. eexists; repeat split; eauto. + + destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; subst. + * eapply IHISTEP1; right. eexists; repeat split; eauto. + eapply IHISTEP2; left; simpl; auto. + * eapply IHISTEP1; right. eexists; repeat split; eauto. + - (* Bcond *) + destruct ofin; intros; + econstructor; eauto; + destruct b; eapply IHISTEP; eauto. +Qed. + +Lemma expand_iblock_istep_correct sp ib rs0 m0 rs1 m1 ofin: + iblock_istep tge sp rs0 m0 ib rs1 m1 ofin -> + iblock_istep tge sp rs0 m0 (expand ib None) rs1 m1 ofin. +Proof. + intros; eapply expand_iblock_istep_rec_correct; eauto. + destruct ofin; simpl; auto. +Qed. + +(* TODO useless? *) +Lemma expand_iblock_istep_run_Some_rec sp ib rs0 m0 rs1 m1 ofin1: + forall (ISTEP: iblock_istep_run tge sp ib rs0 m0 = + Some {| _rs := rs1; _m := m1; _fin := ofin1 |}) + k ofin2 rs2 m2 + (CONT: match ofin1 with + | None => + (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None) + \/ (exists rem, k = Some rem + /\ iblock_istep_run tge sp rem rs1 m1 = + Some {| _rs := rs2; _m := m2; _fin := ofin2 |}) + | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1 + end), + iblock_istep_run tge sp (expand ib k) rs0 m0 = + Some {| _rs := rs2; _m := m2; _fin := ofin2 |}. +Proof. + intros. destruct ofin1; + rewrite <- iblock_istep_run_equiv in *. + - destruct CONT as [HRS [HM HO]]; subst. + eapply expand_iblock_istep_rec_correct; eauto. + simpl; auto. + - eapply expand_iblock_istep_rec_correct; eauto. + simpl. destruct CONT as [HL | [rem [HR ISTEP']]]. + left; auto. rewrite <- iblock_istep_run_equiv in ISTEP'. + right; eexists; split; eauto. +Qed. + +Lemma expand_iblock_istep_run_None_rec sp ib: + forall rs0 m0 o k + (ISTEP: iblock_istep_run tge sp ib rs0 m0 = o) + (CONT: match o with + | Some (out rs1 m1 ofin) => + exists rem, + k = Some rem /\ ofin = None /\ + iblock_istep_run tge sp rem rs1 m1 = None + | _ => True + end), + iblock_istep_run tge sp (expand ib k) rs0 m0 = None. +Proof. + induction ib; simpl; + try discriminate. + - (* BF *) + intros; destruct o; try discriminate; simpl in *. + inv ISTEP. destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO. + - (* Bnop *) + intros; destruct o; inv ISTEP; destruct k; + destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + - (* Bop *) + intros; destruct o; + destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP; destruct k; + simpl; rewrite EVAL; auto; destruct CONT as [rem [HR [HO ISTEP]]]; + inv HR; inv HO; trivial. + - (* Bload *) + intros; destruct o; + destruct (trap) eqn:TRAP; + try destruct (eval_addressing _ _ _ _) eqn:EVAL; + try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; destruct k; + simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; + destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + - (* Bstore *) + intros; destruct o; + destruct (eval_addressing _ _ _ _) eqn:EVAL; + try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; destruct k; + simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; + destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + - (* Bseq *) + intros. + eapply IHib1; eauto. + destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:EQib1; try auto. + destruct o0. eexists; split; eauto. simpl in *. + destruct _fin; inv ISTEP. + + destruct CONT as [rem [_ [CONTRA _]]]; inv CONTRA. + + split; auto. eapply IHib2; eauto. + - (* Bcond *) + intros; destruct (eval_condition _ _ _); trivial. + destruct b. + + eapply IHib1; eauto. + + eapply IHib2; eauto. +Qed. + +Lemma expand_preserves_iblock_istep_run_None sp ib: + forall rs m, iblock_istep_run tge sp ib rs m = None + -> iblock_istep_run tge sp (expand ib None) rs m = None. +Proof. + intros; eapply expand_iblock_istep_run_None_rec; eauto. + simpl; auto. +Qed. + +Lemma expand_preserves_iblock_istep_run sp ib: + forall rs m, iblock_istep_run tge sp ib rs m = + iblock_istep_run tge sp (expand ib None) rs m. +Proof. + intros. + destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP. + - destruct o. symmetry. + rewrite <- iblock_istep_run_equiv in *. + apply expand_iblock_istep_correct; auto. + - symmetry. + apply expand_preserves_iblock_istep_run_None; auto. +Qed. + +Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst: + forall opc1 + (MIB: match_iblock dupmap cfg isfst pc ib opc1) k opc2 + (CONT: match opc1 with + | Some pc' => + k = None /\ opc2 = opc1 \/ + (exists rem, k = Some rem + /\ match_iblock dupmap cfg false pc' rem opc2) + | None => opc2=opc1 + end), + match_iblock dupmap cfg isfst pc (expand ib k) opc2. +Proof. + induction 1; simpl. + { (* BF *) + intros; inv CONT; econstructor; eauto. } + 1-4: (* Bnop *) + destruct k; intros; destruct CONT as [[HK HO] | [rem [HR MIB]]]; + try inv HK; try inv HO; try inv HR; repeat econstructor; eauto. + { (* Bgoto *) + intros; inv CONT; apply mib_exit; auto. } + { (* Bseq *) + intros. eapply IHMIB1. right. eexists; split; eauto. } + { (* Bcond *) + intros. inv H0; + econstructor; eauto; try econstructor. + destruct opc0; econstructor. } +Qed. + +Lemma expand_matchiblock_correct dupmap cfg ib pc isfst opc: + match_iblock dupmap cfg isfst pc ib opc -> + match_iblock dupmap cfg isfst pc (expand ib None) opc. +Proof. + intros. + eapply expand_matchiblock_rec_correct; eauto. + destruct opc; simpl; auto. +Qed. + +(** * Match strong state property + +Used when executing non-atomic instructions such as Bseq/Bcond(ib1,ib2). +Two possible executions: + +<< + + **ib2 is a Bgoto (left side):** + + RTL state MSS1 BTL state + [pcR1,rs1,m1] -------------------------- [ib1,pcB0,rs0,m0] + | | + | | + | | BTL_STEP + | | + | | + RTL_STEP | *E0 [ib2,pc=(Bgoto succ),rs2,m2] + | / | + | MSS2 / | + | _________________/ | BTL_GOTO + | / | + | / GOAL: match_states | + [pcR2,rs2,m2] ------------------------ [ib?,pc=succ,rs2,m2] + + + **ib2 is any other instruction (right side):** + +See explanations of opt_simu below. + +>> +*) + +Lemma match_strong_state_simu + dupmap st st' f f' sp rs2 m2 rs1 m1 rs0 m0 pcB0 pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 n + (STEP : RTL.step ge (RTL.State st f sp pcR1 rs1 m1) E0 (RTL.State st f sp pcR2 rs2 m2)) + (MSS1 : match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib1 ib0 isfst) + (MSS2 : match_strong_state dupmap st st' f f' sp rs2 m2 rs0 m0 pcB0 pcR0 pcR2 ib2 ib0 false) + (MES : measure ib2 < n) + : exists (oib' : option iblock), + (exists s2', step tge (State st' f' sp pcB0 rs0 m0) E0 s2' + /\ match_states oib' (RTL.State st f sp pcR2 rs2 m2) s2') + \/ (omeasure oib' < n /\ E0=E0 + /\ match_states oib' (RTL.State st f sp pcR2 rs2 m2) (State st' f' sp pcB0 rs0 m0)). +Proof. + destruct (is_goto ib2) eqn:GT. + destruct ib2; try destruct fi; try discriminate. + - (* Bgoto *) + inv MSS2. inversion MIB; subst; try inv H3. + remember H0 as ODUPLIC; clear HeqODUPLIC. + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + apply DMC in H0 as [ib [FNC MI]]; clear DMC. + eexists; left; eexists; split. + + repeat econstructor; eauto. + apply iblock_istep_run_equiv in BTL_RUN; eauto. + + econstructor; apply expand_matchiblock_correct in MI. + econstructor; eauto. apply expand_correct; trivial. + econstructor. apply expand_preserves_iblock_istep_run. + eapply expand_entry_isnt_goto; eauto. + - (* Others *) + exists (Some ib2); right; split. + simpl; auto. + split; auto. econstructor; eauto. +Qed. + +Lemma opt_simu_intro + dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst s1' t + (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1') + (MSTRONG : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst) + (NGOTO : is_goto ib = false) + : exists (oib' : option iblock), + (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2') + \/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)). +Proof. + inversion MSTRONG; subst. inv MIB. + - (* mib_BF *) + inv H0; + inversion STEP; subst; try_simplify_someHyps; intros. + + (* Breturn *) + eexists; left; eexists; split. + * econstructor; eauto. econstructor. + eexists; eexists; split. + eapply iblock_istep_run_equiv in BTL_RUN. + eapply BTL_RUN. econstructor; eauto. + erewrite preserv_fnstacksize; eauto. + * econstructor; eauto. + + (* Bcall *) + rename H10 into FIND. + eapply find_function_preserved in FIND. + destruct FIND as (fd' & FF & TRANSFUN). + eexists; left; eexists; split. + * econstructor; eauto. econstructor. + eexists; eexists; split. + eapply iblock_istep_run_equiv in BTL_RUN. + eapply BTL_RUN. econstructor; eauto. + eapply function_sig_translated; eauto. + * repeat (econstructor; eauto). + eapply transf_fundef_correct; eauto. + + (* Btailcall *) + rename H9 into FIND. + eapply find_function_preserved in FIND. + destruct FIND as (fd' & FF & TRANSFUN). + eexists; left; eexists; split. + * econstructor; eauto. econstructor. + eexists; eexists; split. + eapply iblock_istep_run_equiv in BTL_RUN. + eapply BTL_RUN. econstructor; eauto. + eapply function_sig_translated; eauto. + erewrite preserv_fnstacksize; eauto. + * repeat (econstructor; eauto). + eapply transf_fundef_correct; eauto. + + (* Bbuiltin *) + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + remember H1 as ODUPLIC; clear HeqODUPLIC. + apply DMC in H1 as [ib [FNC MI]]; clear DMC. + eexists; left; eexists; split. + * econstructor; eauto. econstructor. + eexists; eexists; split. + eapply iblock_istep_run_equiv in BTL_RUN. + eapply BTL_RUN. econstructor; eauto. + pose symbols_preserved as SYMPRES. + eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + * econstructor; eauto; apply expand_matchiblock_correct in MI. + { econstructor; eauto. apply expand_correct; trivial. + apply star_refl. apply expand_preserves_iblock_istep_run. } + eapply expand_entry_isnt_goto; eauto. + + (* Bjumptable *) + exploit list_nth_z_rev_dupmap; eauto. + intros (pc'0 & LNZ & DM). + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + remember DM as ODUPLIC; clear HeqODUPLIC. + apply DMC in DM as [ib [FNC MI]]; clear DMC. + eexists; left; eexists; split. + * econstructor; eauto. econstructor. + eexists; eexists; split. + eapply iblock_istep_run_equiv in BTL_RUN. + eapply BTL_RUN. econstructor; eauto. + * econstructor; eauto; apply expand_matchiblock_correct in MI. + { econstructor; eauto. apply expand_correct; trivial. + apply star_refl. apply expand_preserves_iblock_istep_run. } + eapply expand_entry_isnt_goto; eauto. + - (* mib_exit *) + discriminate. + - (* mib_seq *) + inversion H; subst; + try (inv IS_EXPD; try inv H5; discriminate; fail); + inversion STEP; subst; try_simplify_someHyps; intros. + + (* Bnop *) + eapply match_strong_state_simu. + 1,2: do 2 (econstructor; eauto). + econstructor; eauto. + inv IS_EXPD; eauto. simpl in *; discriminate. + eapply star_right; eauto. lia. + + (* Bop *) + eapply match_strong_state_simu. + 1,2: do 2 (econstructor; eauto). + econstructor; eauto. + inv IS_EXPD; eauto. simpl in *; discriminate. + eapply star_right; eauto. + erewrite eval_operation_preserved in H11. + erewrite H11 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. lia. + + (* Bload *) + eapply match_strong_state_simu. + 1,2: do 2 (econstructor; eauto). + econstructor; eauto. + inv IS_EXPD; eauto. simpl in *; discriminate. + eapply star_right; eauto. + erewrite eval_addressing_preserved in H11. + erewrite H11, H12 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. lia. + + (* Bstore *) + eapply match_strong_state_simu. + 1,2: do 2 (econstructor; eauto). + econstructor; eauto. + inv IS_EXPD; eauto. simpl in *; discriminate. + eapply star_right; eauto. + erewrite eval_addressing_preserved in H11. + erewrite H11, H12 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. lia. + - (* mib_cond *) + inversion STEP; subst; try_simplify_someHyps; intros. + intros; rewrite H12 in BTL_RUN. destruct b; + eapply match_strong_state_simu; eauto. + 1,3: inv H2; econstructor; eauto. + 1,3,5,7: inv IS_EXPD; auto; discriminate. + 1-4: eapply star_right; eauto. + assert (measure bnot > 0) by apply measure_pos; lia. + assert (measure bso > 0) by apply measure_pos; lia. +Qed. + +(** * Main RTL to BTL simulation theorem + +Two possible executions: + +<< + + **Last instruction (left side):** + + RTL state match_states BTL state + s1 ------------------------------------ s2 + | | + STEP | Classical lockstep simu | + | | + s1' ----------------------------------- s2' + + + **Middle instruction (right side):** + + RTL state match_states [oib] BTL state + s1 ------------------------------------ s2 + | _______/ + STEP | *E0 ___________________/ + | / match_states [oib'] + s1' ______/ + Where omeasure oib' < omeasure oib + +>> +*) + +Theorem opt_simu s1 t s1' oib s2: + RTL.step ge s1 t s1' -> + match_states oib s1 s2 -> + exists (oib' : option iblock), + (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2') + \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) + . +Proof. + inversion 2; subst; clear H0. + - (* State *) + exploit opt_simu_intro; eauto. + - (* Callstate *) + inv H. + + (* Internal function *) + inv TRANSF. + rename H0 into TRANSF. + eapply dupmap_entrypoint in TRANSF as ENTRY. + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + apply DMC in ENTRY as DMC'. + destruct DMC' as [ib [CENTRY MI]]; clear DMC. + eexists; left; eexists; split. + * eapply exec_function_internal. + erewrite preserv_fnstacksize; eauto. + * apply expand_matchiblock_correct in MI. + econstructor. econstructor; eauto. + apply expand_correct; trivial. + 3: eapply expand_entry_isnt_goto; eauto. + all: erewrite preserv_fnparams; eauto. + constructor. + apply expand_preserves_iblock_istep_run. + + (* External function *) + inv TRANSF. + eexists; left; eexists; split. + * eapply exec_function_external. + eapply external_call_symbols_preserved. + eapply senv_preserved. eauto. + * econstructor; eauto. + - (* Returnstate *) + inv H. inv STACKS. inv H1. + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + remember DUPLIC as ODUPLIC; clear HeqODUPLIC. + apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC. + eexists; left; eexists; split. + + eapply exec_return. + + apply expand_matchiblock_correct in MI. + econstructor. econstructor; eauto. + apply expand_correct; trivial. + constructor. apply expand_preserves_iblock_istep_run. + eapply expand_entry_isnt_goto; eauto. +Qed. + +Local Hint Resolve plus_one star_refl: core. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (BTL.semantics tprog). +Proof. + eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states). + constructor 1; simpl. + - apply well_founded_ltof. + - eapply transf_initial_states. + - eapply transf_final_states. + - intros s1 t s1' STEP i s2 MATCH. exploit opt_simu; eauto. clear MATCH STEP. + destruct 1 as (oib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]). + + repeat eexists; eauto. + + subst. repeat eexists; eauto. + - eapply senv_preserved. +Qed. + +End BTL_SIMULATES_RTL. |