diff options
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/BTL.v | 735 | ||||
| -rw-r--r-- | scheduling/BTLRenumber.ml | 112 | ||||
| -rw-r--r-- | scheduling/BTLScheduleraux.ml | 254 | ||||
| -rw-r--r-- | scheduling/BTL_Livecheck.v | 689 | ||||
| -rw-r--r-- | scheduling/BTL_SEsimuref.v | 807 | ||||
| -rw-r--r-- | scheduling/BTL_SEtheory.v | 1311 | ||||
| -rw-r--r-- | scheduling/BTL_Scheduler.v | 70 | ||||
| -rw-r--r-- | scheduling/BTL_Schedulerproof.v | 31 | ||||
| -rw-r--r-- | scheduling/BTLcommonaux.ml | 70 | ||||
| -rw-r--r-- | scheduling/BTLmatchRTL.v | 603 | ||||
| -rw-r--r-- | scheduling/BTLroadmap.md | 408 | ||||
| -rw-r--r-- | scheduling/BTLtoRTL.v | 26 | ||||
| -rw-r--r-- | scheduling/BTLtoRTLaux.ml | 88 | ||||
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 402 | ||||
| -rw-r--r-- | scheduling/BTLtypes.ml | 7 | ||||
| -rw-r--r-- | scheduling/PrintBTL.ml | 131 | ||||
| -rw-r--r-- | scheduling/RTLpathLivegenaux.ml | 85 | ||||
| -rw-r--r-- | scheduling/RTLpathScheduleraux.ml | 1 | ||||
| -rw-r--r-- | scheduling/RTLtoBTL.v | 27 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLaux.ml | 116 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 749 |
21 files changed, 6641 insertions, 81 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v new file mode 100644 index 00000000..6536addb --- /dev/null +++ b/scheduling/BTL.v @@ -0,0 +1,735 @@ +(** 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. +Require Import Lia. + +Import ListNotations. + +(** * Abstract syntax *) + +Definition exit := node. (* we may generalize this with register renamings at exit, + like in "phi" nodes of SSA-form *) + +(* inst_info is a ghost record to provide instruction information through oracles *) +Parameter inst_info: Set. +Extract Constant inst_info => "BTLtypes.inst_info". + +(* block_info is a ghost record to provide block information through oracles *) +Parameter block_info: Set. +Extract Constant block_info => "BTLtypes.block_info". + +(** 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) (iinfo: inst_info) +(* basic instructions that continues block execution, except when aborting *) + | Bnop (oiinfo: option inst_info) (* nop instruction *) + | Bop (op:operation) (args:list reg) (dest:reg) (iinfo: inst_info) + (** 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) (iinfo: inst_info) + (** 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) (iinfo: inst_info) + (** 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) (iinfo: inst_info) + (** 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 >-> Funclass. + + +(** 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 for BTL functional semantics *) + binfo: block_info (* Ghost field used in oracles *) +}. + +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 +}. + +(* follows RTL semantics to set the result of builtin *) +Definition reg_builtin_res (res: builtin_res reg): option reg := + match res with + | BR r => Some r + | _ => None + end. + +Section RELSEM. + +(** [step] (and in particular [final_step]) is parametrized by function [tr_exit] to transfer registers on each iblock exit. + + In particular, [tr_exit f lpc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [lpc] in [f] may start. + + Here, [or] is an optional register that will be assigned after exiting the iblock, but before entering in [pc]: e.g. the register set by a function call + before entering in return address. + + See [tr_inputs] implementation below. + +*) + +Variable tr_exit: function -> list exit -> option reg -> regset -> regset. + +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 iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin) +| exec_nop rs m oiinfo: iblock_istep sp rs m (Bnop oiinfo) rs m None + | exec_op rs m op args res v iinfo + (EVAL: eval_operation ge sp op rs##args m = Some v) + : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None + | exec_load_TRAP rs m chunk addr args dst a v iinfo + (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 iinfo) (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' iinfo + (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 iinfo) 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 b rs' m' ofin iinfo + (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 iinfo) 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. + +Local Open Scope list_scope. + +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 (tr_exit f [pc] None 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' (tr_exit f [pc'] (Some res) 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 (tr_exit f [pc'] (reg_builtin_res res) 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' (tr_exit f tbl None 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 full "functional" small-step semantics for a BTL program. + at each exit, we only transfer register in "input_regs" (i.e. "alive" registers). +*) +Definition transfer_regs (inputs: list reg) (rs: regset): regset := + init_regs (rs##inputs) inputs. + +Lemma transfer_regs_inputs inputs rs r: + List.In r inputs -> (transfer_regs inputs rs)#r = rs#r. +Proof. + unfold transfer_regs; induction inputs; simpl; intuition subst. + - rewrite Regmap.gss; auto. + - destruct (Pos.eq_dec a r). + + subst; rewrite Regmap.gss; auto. + + rewrite Regmap.gso; auto. +Qed. + +Lemma transfer_regs_dead inputs rs r: + ~List.In r inputs -> (transfer_regs inputs rs)#r = Vundef. +Proof. + unfold transfer_regs; induction inputs; simpl; intuition subst. + - rewrite Regmap.gi; auto. + - rewrite Regmap.gso; auto. +Qed. + +Fixpoint union_inputs (f:function) (tbl: list exit): Regset.t := + match tbl with + | nil => Regset.empty + | pc::l => let rs:= union_inputs f l in + match f.(fn_code)!pc with + | None => rs + | Some ib => Regset.union rs ib.(input_regs) + end + end. + +(* TODO: lemma not yet used + +Lemma union_inputs_In f tbl r: + Regset.In r (union_inputs f tbl) -> (exists pc, List.In pc tbl /\ exists ib, f.(fn_code)!pc = Some ib /\ Regset.In r ib.(input_regs)). +Proof. + induction tbl as [|pc l]; simpl; intros. + - exploit Regset.empty_1; eauto. intuition. + - destruct ((fn_code f) ! pc) eqn:ATpc. + + exploit Regset.union_1; eauto. + destruct 1 as [X1|X1]. + * destruct IHl as (pc' & H1 & H2); eauto. + * eexists; intuition eauto. + + destruct IHl as (pc' & H1 & H2); eauto. +Qed. + +Lemma union_inputs_notIn f tbl r: + (forall pc ib, List.In pc tbl -> f.(fn_code)!pc = Some ib -> ~Regset.In r ib.(input_regs)) + -> ~Regset.In r (union_inputs f tbl). +Proof. + induction tbl as [|pc l]; simpl; intuition eauto. + - exploit Regset.empty_1; eauto. + - destruct ((fn_code f) ! pc) eqn:ATpc; intuition eauto. + exploit Regset.union_1; intuition eauto. +Qed. +*) + +(* This function computes the union of the inputs associated to the exits + minus the optional register in [or] (typically the result of a call or a builtin). + i.e. similar to [pre_output_regs] in RTLpath. +*) +Definition pre_inputs (f:function) (tbl: list exit) (or: option reg): Regset.t := + let rs := union_inputs f tbl in + match or with + | Some r => Regset.remove r rs + | None => rs + end + . + +(* TODO: lemma pre_inputs_In + pre_inputs_notIn ? *) + +Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset + := transfer_regs (Regset.elements (pre_inputs f tbl or)). + + +(* TODO: move this elsewhere *) +Lemma SetoidList_InA_eq_equiv A (l: list A): forall x, + SetoidList.InA (fun x y => x = y) x l <-> List.In x l. +Proof. + intros x; split. + - induction 1; simpl; eauto. + - induction l; simpl; intuition. +Qed. + +Lemma tr_pre_inputs f tbl or rs r: + Regset.In r (pre_inputs f tbl or) -> (tr_inputs f tbl or rs)#r = rs#r. +Proof. + intros; eapply transfer_regs_inputs. + rewrite <- SetoidList_InA_eq_equiv. + eapply Regset.elements_1; eauto. +Qed. + +Lemma tr_inputs_dead f tbl or rs r: + ~(Regset.In r (pre_inputs f tbl or)) -> (tr_inputs f tbl or rs)#r = Vundef. +Proof. + intros X; eapply transfer_regs_dead; intuition eauto. + eapply X. eapply Regset.elements_2. + rewrite -> SetoidList_InA_eq_equiv; eauto. +Qed. + +Local Hint Resolve tr_pre_inputs Regset.mem_2 Regset.mem_1: core. + +Lemma tr_inputs_get f tbl or rs r: + (tr_inputs f tbl or rs)#r = if Regset.mem r (pre_inputs f tbl or) then rs#r else Vundef. +Proof. + autodestruct; eauto. + intros; apply tr_inputs_dead; eauto. + intro X; exploit Regset.mem_1; eauto. + congruence. +Qed. + +(* TODO: not yet used +Lemma tr_inputs_ext f tbl or rs1 rs2: + (forall r, Regset.In r (pre_inputs f tbl or) -> rs1#r = rs2#r) -> + (forall r, (tr_inputs f tbl or rs1)#r = (tr_inputs f tbl or rs2)#r). +Proof. + intros EQ r. rewrite !tr_inputs_get. + autodestruct; auto. +Qed. +*) + +Definition fsem (p: program) := + Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p). + +Local Open Scope list_scope. + +Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: final): A := + match i with + | Bgoto pc => tr f [pc] None + | Bcall _ _ _ res pc => tr f [pc] (Some res) + | Btailcall _ _ args => tr f [] None + | Bbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res) + | Breturn _ => tr f [] None + | Bjumptable _ tbl => tr f tbl None + end. + +Definition tr_regs: function -> final -> regset -> regset := + poly_tr tr_inputs. + +(* TODO: NOT USEFUL ? +Definition liveout: function -> final -> Regset.t := + poly_tr pre_inputs. + +Lemma tr_regs_liveout_equiv f fi : tr_regs f fi = transfer_regs (Regset.elements (liveout f fi)). +Proof. + destruct fi; simpl; auto. +Qed. + +Local Hint Resolve tr_inputs_get: core. + +Lemma tr_regs_get f fi rs r: (tr_regs f fi rs)#r = if Regset.mem r (liveout f fi) then rs#r else Vundef. +Proof. + Local Opaque pre_inputs. + destruct fi; simpl; auto. +Qed. +*) + +(* * Comparing BTL semantics modulo extensionality of [regset]. + +NB: This is at least used in BTL_SEtheory (and probably in the future BTL_SchedulerProof). + +*) +Inductive equiv_stackframe: stackframe -> stackframe -> Prop := + | equiv_stackframe_intro res f sp pc (rs1 rs2: regset) + (EQUIV: forall r, 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 stk1 stk2 f sp pc rs1 m rs2 + (STACKS: list_forall2 equiv_stackframe stk1 stk2) + (EQUIV: forall r, rs1#r = rs2#r) + :equiv_state (State stk1 f sp pc rs1 m) (State stk2 f sp pc rs2 m) + | Call_equiv stk1 stk2 f args m + (STACKS: list_forall2 equiv_stackframe stk1 stk2) + :equiv_state (Callstate stk1 f args m) (Callstate stk2 f args m) + | Return_equiv stk1 stk2 v m + (STACKS: list_forall2 equiv_stackframe stk1 stk2) + :equiv_state (Returnstate stk1 v m) (Returnstate stk2 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. +Local Hint Resolve equiv_stack_refl: core. + +Lemma equiv_state_refl s: equiv_state s s. +Proof. + 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. +Local Hint Resolve equiv_stackframe_trans: core. + +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. + 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. + +(* * Comparing BTL semantics modulo [regs_lessdef]. + +This extends the previous [equiv_*] stuff for [Val.lessdef]. Here, we need to also compare memories +for Mem.extends, because Vundef values are propagated in memory through stores, allocation, etc. + +*) + +Inductive lessdef_stackframe: stackframe -> stackframe -> Prop := + | lessdef_stackframe_intro res f sp pc rs1 rs2 + (REGS: forall r, Val.lessdef rs1#r rs2#r) + :lessdef_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2) + . + +Inductive lessdef_state: state -> state -> Prop := + | State_lessdef stk1 stk2 f sp pc rs1 m1 rs2 m2 + (STACKS: list_forall2 lessdef_stackframe stk1 stk2) + (REGS: forall r, Val.lessdef rs1#r rs2#r) + (MEMS: Mem.extends m1 m2) + :lessdef_state (State stk1 f sp pc rs1 m1) (State stk2 f sp pc rs2 m2) + | Call_lessdef stk1 stk2 f args1 args2 m1 m2 + (STACKS: list_forall2 lessdef_stackframe stk1 stk2) + (ARGS: Val.lessdef_list args1 args2) + (MEMS: Mem.extends m1 m2) + :lessdef_state (Callstate stk1 f args1 m1) (Callstate stk2 f args2 m2) + | Return_lessdef stk1 stk2 v1 v2 m1 m2 + (STACKS: list_forall2 lessdef_stackframe stk1 stk2) + (REGS: Val.lessdef v1 v2) + (MEMS: Mem.extends m1 m2) + :lessdef_state (Returnstate stk1 v1 m1) (Returnstate stk2 v2 m2) + . +Local Hint Constructors lessdef_stackframe lessdef_state: core. + +Lemma lessdef_stackframe_refl stf: lessdef_stackframe stf stf. +Proof. + destruct stf; eauto. +Qed. + +Local Hint Resolve lessdef_stackframe_refl: core. +Lemma lessdef_stack_refl stk: list_forall2 lessdef_stackframe stk stk. +Proof. + induction stk; simpl; constructor; auto. +Qed. + +Local Hint Resolve lessdef_stack_refl: core. + +Lemma lessdef_list_refl args: Val.lessdef_list args args. +Proof. + induction args; simpl; auto. +Qed. + +Local Hint Resolve lessdef_list_refl Mem.extends_refl: core. + +Lemma lessdef_state_refl s: lessdef_state s s. +Proof. + induction s; simpl; constructor; auto. +Qed. + +Local Hint Resolve Val.lessdef_trans: core. +Lemma lessdef_stackframe_trans stf1 stf2 stf3: + lessdef_stackframe stf1 stf2 -> lessdef_stackframe stf2 stf3 -> lessdef_stackframe stf1 stf3. +Proof. + destruct 1. intros LD; inv LD; try econstructor; eauto. +Qed. + +Local Hint Resolve lessdef_stackframe_trans: core. +Lemma lessdef_stack_trans stk1 stk2: + list_forall2 lessdef_stackframe stk1 stk2 -> + forall stk3, list_forall2 lessdef_stackframe stk2 stk3 -> + list_forall2 lessdef_stackframe stk1 stk3. +Proof. + induction 1; intros stk3 LD; inv LD; econstructor; eauto. +Qed. + +Local Hint Resolve lessdef_stack_trans Mem.extends_extends_compose Val.lessdef_list_trans: core. +Lemma lessdef_state_trans s1 s2 s3: lessdef_state s1 s2 -> lessdef_state s2 s3 -> lessdef_state s1 s3. +Proof. + destruct 1; intros LD; inv LD; econstructor; eauto. +Qed. + +Lemma init_regs_lessdef_preserv args1 args2 + (ARGS : Val.lessdef_list args1 args2) + : forall rl r, Val.lessdef (init_regs args1 rl)#r (init_regs args2 rl)#r. +Proof. + induction ARGS; simpl; auto. + intros rl r1; destruct rl; simpl in *; auto. + eapply set_reg_lessdef; eauto. + intros r2; eauto. +Qed. + +Lemma find_function_lessdef ge ros rs1 rs2 fd + (FIND: find_function ge ros rs1 = Some fd) + (REGS: forall r, Val.lessdef rs1#r rs2#r) + : find_function ge ros rs2 = Some fd. +Proof. + destruct ros; simpl in *; auto. + exploit Genv.find_funct_inv; eauto. + intros (b & EQ). + destruct (REGS r); try congruence. +Qed. + +(** * Auxiliary general purpose functions on BTL *) + +Definition is_goto (ib: iblock): bool := + match ib with + | BF (Bgoto _) _ => true + | _ => false + end. + diff --git a/scheduling/BTLRenumber.ml b/scheduling/BTLRenumber.ml new file mode 100644 index 00000000..6ff42a27 --- /dev/null +++ b/scheduling/BTLRenumber.ml @@ -0,0 +1,112 @@ +open Maps +open BTL +open RTLcommonaux +open BTLcommonaux +open BTLtypes +open DebugPrint +open PrintBTL + +let recompute_inumbs btl entry = + let btl = reset_visited_ib (reset_visited_ibf btl) in + let last_used = ref 0 in + let ibf = get_some @@ PTree.get entry btl in + let ipos () = + last_used := !last_used + 1; + !last_used + in + let rec walk ib k = + (* heuristic: try to explore the lower numbered branch first *) + let walk_smallest_child s1 s2 ib1 ib2 = + if s1 < s2 then ( + walk ib1 None; + walk ib2 None) + else ( + walk ib2 None; + walk ib1 None) + in + if jump_visit ib then () + else + match ib with + | BF (Bcall (_, _, _, _, s), iinfo) | BF (Bbuiltin (_, _, _, s), iinfo) -> + let ib' = (get_some @@ PTree.get s btl).entry in + walk ib' None; + iinfo.inumb <- ipos () + | BF (Bgoto s, _) -> + let ib' = (get_some @@ PTree.get s btl).entry in + walk ib' None + | BF (Bjumptable (_, tbl), iinfo) -> + List.iter + (fun s -> + let ib' = (get_some @@ PTree.get s btl).entry in + walk ib' None) + tbl; + iinfo.inumb <- ipos () + | BF (Btailcall (_, _, _), iinfo) | BF (Breturn _, iinfo) -> + iinfo.inumb <- ipos () + | Bnop None -> + failwith + "recompute_inumbs: Bnop None can only be in the right child of \ + Bcond" + | Bnop (Some iinfo) + | Bop (_, _, _, iinfo) + | Bload (_, _, _, _, _, iinfo) + | Bstore (_, _, _, _, iinfo) -> + let succ = get_some @@ k in + walk succ None; + iinfo.inumb <- ipos () + | Bseq (ib1, ib2) -> walk ib1 (Some ib2) + | Bcond (_, _, BF (Bgoto s1, iinfoL), Bnop None, iinfoF) -> + iinfoL.visited <- true; + let ib1 = get_some @@ PTree.get s1 btl in + let ib2 = get_some @@ k in + walk_smallest_child (p2i s1) (get_inumb_or_next ib2) ib1.entry ib2; + iinfoF.inumb <- ipos () + | Bcond (_, _, _, _, _) -> failwith "recompute_inumbs: unsupported Bcond" + in + walk ibf.entry None; + btl + +let regenerate_btl_tree btl entry = + let new_entry = ref entry in + let rec renumber_iblock ib = + let get_new_succ s = + let sentry = get_some @@ PTree.get s btl in + i2p (get_inumb_or_next sentry.entry) + in + match ib with + | BF (Bcall (sign, fn, lr, rd, s), iinfo) -> + BF (Bcall (sign, fn, lr, rd, get_new_succ s), iinfo) + | BF (Bbuiltin (sign, fn, lr, s), iinfo) -> + BF (Bbuiltin (sign, fn, lr, get_new_succ s), iinfo) + | BF (Bgoto s, iinfo) -> BF (Bgoto (get_new_succ s), iinfo) + | BF (Bjumptable (arg, tbl), iinfo) -> + let tbl' = List.map (fun s -> get_new_succ s) tbl in + BF (Bjumptable (arg, tbl'), iinfo) + | Bcond (cond, lr, ib1, ib2, iinfo) -> + Bcond (cond, lr, renumber_iblock ib1, renumber_iblock ib2, iinfo) + | Bseq (ib1, ib2) -> Bseq (renumber_iblock ib1, renumber_iblock ib2) + | _ -> ib + in + let dm = ref PTree.empty in + let ord_btl = + PTree.fold + (fun ord_btl old_n old_ibf -> + let ib = renumber_iblock old_ibf.entry in + let n = get_inumb_or_next ib in + let n_pos = i2p n in + let bi = mk_binfo n in + let ibf = { entry = ib; input_regs = old_ibf.input_regs; binfo = bi } in + if old_n = entry then new_entry := n_pos; + dm := PTree.set old_n n_pos !dm; + PTree.set n_pos ibf ord_btl) + btl PTree.empty + in + debug "Renumbered BTL with new_entry=%d:\n" (p2i !new_entry); + print_btl_code stderr ord_btl; + ((ord_btl, !new_entry), !dm) + +let renumber btl entry = + (*debug_flag := true;*) + let btl' = recompute_inumbs btl entry in + (*debug_flag := false;*) + regenerate_btl_tree btl' entry diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml new file mode 100644 index 00000000..b87636e1 --- /dev/null +++ b/scheduling/BTLScheduleraux.ml @@ -0,0 +1,254 @@ +open AST +open Maps +open Registers +open BTL +open BTLtypes +open DebugPrint +open PrintBTL +open RTLcommonaux +open InstructionScheduler +open PrepassSchedulingOracleDeps + +let use_alias_analysis () = false + +let build_constraints_and_resources (opweights : opweights) insts btl = + let last_reg_reads : int list PTree.t ref = ref PTree.empty + and last_reg_write : (int * int) PTree.t ref = ref PTree.empty + and last_mem_reads : int list ref = ref [] + and last_mem_write : int option ref = ref None + and last_branch : int option ref = ref None + and last_non_pipelined_op : int array = + Array.make opweights.nr_non_pipelined_units (-1) + and latency_constraints : latency_constraint list ref = ref [] + and resources = ref [] in + let add_constraint instr_from instr_to latency = + assert (instr_from <= instr_to); + assert (latency >= 0); + if instr_from = instr_to then + if latency = 0 then () + else + failwith "PrepassSchedulingOracle.get_dependencies: negative self-loop" + else + latency_constraints := + { instr_from; instr_to; latency } :: !latency_constraints + and get_last_reads reg = + match PTree.get reg !last_reg_reads with Some l -> l | None -> [] + in + let add_input_mem i = + if not (use_alias_analysis ()) then ( + (* Read after write *) + (match !last_mem_write with None -> () | Some j -> add_constraint j i 1); + last_mem_reads := i :: !last_mem_reads) + and add_output_mem i = + if not (use_alias_analysis ()) then ( + (* Write after write *) + (match !last_mem_write with None -> () | Some j -> add_constraint j i 1); + (* Write after read *) + List.iter (fun j -> add_constraint j i 0) !last_mem_reads; + last_mem_write := Some i; + last_mem_reads := []) + and add_input_reg i reg = + (* Read after write *) + (match PTree.get reg !last_reg_write with + | None -> () + | Some (j, latency) -> add_constraint j i latency); + last_reg_reads := PTree.set reg (i :: get_last_reads reg) !last_reg_reads + and add_output_reg i latency reg = + (* Write after write *) + (match PTree.get reg !last_reg_write with + | None -> () + | Some (j, _) -> add_constraint j i 1); + (* Write after read *) + List.iter (fun j -> add_constraint j i 0) (get_last_reads reg); + last_reg_write := PTree.set reg (i, latency) !last_reg_write; + last_reg_reads := PTree.remove reg !last_reg_reads + in + let add_input_regs i regs = List.iter (add_input_reg i) regs + and irreversible_action i = + match !last_branch with None -> () | Some j -> add_constraint j i 1 + in + let set_branch i = + irreversible_action i; + last_branch := Some i + and add_non_pipelined_resources i resources = + Array.iter2 + (fun latency last -> + if latency >= 0 && last >= 0 then add_constraint last i latency) + resources last_non_pipelined_op; + Array.iteri + (fun rsc latency -> if latency >= 0 then last_non_pipelined_op.(rsc) <- i) + resources + in + Array.iteri + (fun i inst -> + match inst with + | Bnop _ -> + let rs = Array.map (fun _ -> 0) opweights.pipelined_resource_bounds in + resources := rs :: !resources + | Bop (op, lr, rd, _) -> + add_non_pipelined_resources i + (opweights.non_pipelined_resources_of_op op (List.length lr)); + if Op.is_trapping_op op then irreversible_action i; + add_input_regs i lr; + add_output_reg i (opweights.latency_of_op op (List.length lr)) rd; + let rs = opweights.resources_of_op op (List.length lr) in + resources := rs :: !resources + | Bload (trap, chk, addr, lr, rd, _) -> + if trap = TRAP then irreversible_action i; + add_input_mem i; + add_input_regs i lr; + add_output_reg i + (opweights.latency_of_load trap chk addr (List.length lr)) + rd; + let rs = opweights.resources_of_load trap chk addr (List.length lr) in + resources := rs :: !resources + | Bstore (chk, addr, lr, src, _) -> + irreversible_action i; + add_input_regs i lr; + add_input_reg i src; + add_output_mem i; + let rs = opweights.resources_of_store chk addr (List.length lr) in + resources := rs :: !resources + | Bcond (cond, lr, BF (Bgoto s, _), ibnot, _) -> + (* TODO gourdinl test with/out this line *) + let live = (get_some @@ PTree.get s btl).input_regs in + add_input_regs i (Regset.elements live); + set_branch i; + add_input_mem i; + add_input_regs i lr; + let rs = opweights.resources_of_cond cond (List.length lr) in + resources := rs :: !resources + | Bcond (_, _, _, _, _) -> + failwith "get_simple_dependencies: invalid Bcond" + | BF (_, _) -> failwith "get_simple_dependencies: BF" + | Bseq (_, _) -> failwith "get_simple_dependencies: Bseq") + insts; + (!latency_constraints, Array.of_list (List.rev !resources)) + +let define_problem (opweights : opweights) ibf btl = + let simple_deps, resources = + build_constraints_and_resources opweights ibf btl + in + { + max_latency = -1; + resource_bounds = opweights.pipelined_resource_bounds; + instruction_usages = resources; + latency_constraints = simple_deps; + } + +let zigzag_scheduler problem early_ones = + let nr_instructions = get_nr_instructions problem in + assert (nr_instructions = Array.length early_ones); + match list_scheduler problem with + | Some fwd_schedule -> + let fwd_makespan = fwd_schedule.(Array.length fwd_schedule - 1) in + let constraints' = ref problem.latency_constraints in + Array.iteri + (fun i is_early -> + if is_early then + constraints' := + { + instr_from = i; + instr_to = nr_instructions; + latency = fwd_makespan - fwd_schedule.(i); + } + :: !constraints') + early_ones; + validated_scheduler reverse_list_scheduler + { problem with latency_constraints = !constraints' } + | None -> None + +let prepass_scheduler_by_name name problem insts = + match name with + | "zigzag" -> + let early_ones = + Array.map + (fun inst -> + match inst with Bcond (_, _, _, _, _) -> true | _ -> false) + insts + in + zigzag_scheduler problem early_ones + | _ -> scheduler_by_name name problem + +let schedule_sequence insts btl = + let opweights = OpWeights.get_opweights () in + try + if Array.length insts <= 1 then None + else + let nr_instructions = Array.length insts in + let problem = define_problem opweights insts btl in + match + prepass_scheduler_by_name !Clflags.option_fprepass_sched problem insts + with + | None -> + Printf.printf "no solution in prepass scheduling\n"; + None + | Some solution -> + let positions = Array.init nr_instructions (fun i -> i) in + Array.sort + (fun i j -> + let si = solution.(i) and sj = solution.(j) in + if si < sj then -1 else if si > sj then 1 else i - j) + positions; + Some positions + with Failure s -> + Printf.printf "failure in prepass scheduling: %s\n" s; + None + +let flatten_blk_basics ibf = + let ib = ibf.entry in + let last = ref None in + let rec traverse_blk ib = + match ib with + | BF (_, _) -> + last := Some ib; + [] + | Bseq ((Bcond (_, _, _, _, iinfo) as ib1), ib2) -> ( + match iinfo.pcond with + | Some _ -> [ ib1 ] @ traverse_blk ib2 + | None -> + last := Some ib; + []) + | Bseq (ib1, ib2) -> traverse_blk ib1 @ traverse_blk ib2 + | _ -> [ ib ] + in + let ibl = traverse_blk ib in + (Array.of_list ibl, !last) + +let apply_schedule bseq olast positions = + let ibl = Array.to_list (Array.map (fun i -> bseq.(i)) positions) in + let rec build_iblock = function + | [] -> failwith "build_iblock: empty list" + | [ ib ] -> ( match olast with Some last -> Bseq (ib, last) | None -> ib) + | ib1 :: ib2 :: k -> Bseq (ib1, build_iblock (ib2 :: k)) + in + build_iblock ibl + +let schedule_blk n ibf btl = + let bseq, olast = flatten_blk_basics ibf in + match schedule_sequence bseq btl with + | Some positions -> + debug "%d," (p2i n); + Array.iter (fun p -> debug "%d " p) positions; + debug "\n"; + let new_ib = apply_schedule bseq olast positions in + let new_ibf = + { entry = new_ib; binfo = ibf.binfo; input_regs = ibf.input_regs } + in + PTree.set n new_ibf btl + | None -> btl + +let rec do_schedule btl = function + | [] -> btl + | (n, ibf) :: blks -> + let btl' = schedule_blk n ibf btl in + do_schedule btl' blks + +let btl_scheduler f = + let btl = f.fn_code in + (*debug_flag := true;*) + let btl' = do_schedule btl (PTree.elements btl) in + debug "Scheduled BTL Code:\n"; + print_btl_code stderr btl'; + (*debug_flag := false;*) + btl' diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v new file mode 100644 index 00000000..25a1c545 --- /dev/null +++ b/scheduling/BTL_Livecheck.v @@ -0,0 +1,689 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep Op Registers OptionMonad. +Require Import Errors RTL BTL BTLmatchRTL. + + +Local Open Scope lazy_bool_scope. + +Local Open Scope option_monad_scope. + +Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool := + match rl with + | nil => true + | r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive + end. + +Definition reg_option_mem (or: option reg) (alive: Regset.t) := + match or with None => true | Some r => Regset.mem r alive end. + +Definition reg_sum_mem (ros: reg + ident) (alive: Regset.t) := + match ros with inl r => Regset.mem r alive | inr s => true end. + +(* NB: definition following [regmap_setres] in [RTL.step] semantics *) +Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t := + match res with + | BR r => Regset.add r alive + | _ => alive + end. + +Definition exit_checker (btl: code) (alive: Regset.t) (s: node): option unit := + SOME next <- btl!s IN + ASSERT Regset.subset next.(input_regs) alive IN + Some tt. + +Fixpoint exit_list_checker (btl: code) (alive: Regset.t) (l: list node): bool := + match l with + | nil => true + | s :: l' => exit_checker btl alive s &&& exit_list_checker btl alive l' + end. + +Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option unit := + match fin with + | Bgoto s => + exit_checker btl alive s + | Breturn oreg => + ASSERT reg_option_mem oreg alive IN Some tt + | Bcall _ ros args res s => + ASSERT list_mem args alive IN + ASSERT reg_sum_mem ros alive IN + exit_checker btl (Regset.add res alive) s + | Btailcall _ ros args => + ASSERT list_mem args alive IN + ASSERT reg_sum_mem ros alive IN Some tt + | Bbuiltin _ args res s => + ASSERT list_mem (params_of_builtin_args args) alive IN + exit_checker btl (reg_builtin_res res alive) s + | Bjumptable arg tbl => + ASSERT Regset.mem arg alive IN + ASSERT exit_list_checker btl alive tbl IN Some tt + end. + +(* This definition is the meet (infimum) subset of alive registers, + used for conditions by the below checker. + A None argument represents the neutral element for intersection. *) +Definition meet (o1 o2: option Regset.t): option Regset.t := + match o1, o2 with + | None, _ => o2 + | _, None => o1 + | Some alive1, Some alive2 => Some (Regset.inter alive1 alive2) + end. + +Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option (option Regset.t) := + match ib with + | Bseq ib1 ib2 => + SOME oalive1 <- body_checker btl ib1 alive IN + SOME alive1 <- oalive1 IN + body_checker btl ib2 alive1 + | Bnop _ => Some (Some alive) + | Bop _ args dest _ => + ASSERT list_mem args alive IN + Some (Some (Regset.add dest alive)) + | Bload _ _ _ args dest _ => + ASSERT list_mem args alive IN + Some (Some (Regset.add dest alive)) + | Bstore _ _ args src _ => + ASSERT Regset.mem src alive IN + ASSERT list_mem args alive IN + Some (Some alive) + | Bcond _ args ib1 ib2 _ => + ASSERT list_mem args alive IN + SOME oalive1 <- body_checker btl ib1 alive IN + SOME oalive2 <- body_checker btl ib2 alive IN + Some (meet oalive1 oalive2) + | BF fin _ => + SOME _ <- final_inst_checker btl alive fin IN + Some None + end. + +(* This definition simply convert the result in an option unit *) +Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t): option unit := + SOME _ <- body_checker btl ib alive IN Some tt. + +Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool := + match l with + | nil => true + | (_, ibf) :: l' => iblock_checker btl ibf.(entry) ibf.(input_regs) &&& list_iblock_checker btl l' + end. + +Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true. +Proof. + destruct o; simpl; intuition. + - eauto. + - firstorder. try_simplify_someHyps. +Qed. + +Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true. +Proof. + intros; rewrite lazy_and_Some_true; firstorder. + destruct x; auto. +Qed. + +Lemma list_iblock_checker_correct btl l: + list_iblock_checker btl l = true -> + forall e, List.In e l -> iblock_checker btl (snd e).(entry) (snd e).(input_regs) = Some tt. +Proof. + intros CHECKER e H; induction l as [|(n & ibf) l]; intuition. + simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto). +Qed. + +Definition liveness_checker_bool (f: BTL.function): bool := + f.(fn_code)!(f.(fn_entrypoint)) &&& list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)). + +Definition liveness_checker (f: BTL.function): res unit := + match liveness_checker_bool f with + | true => OK tt + | false => Error (msg "BTL_Livecheck: liveness_checker failed") + end. + +Lemma decomp_liveness_checker f: + liveness_checker f = OK tt -> + exists ibf, f.(fn_code)!(f.(fn_entrypoint)) = Some ibf /\ + list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) = true. +Proof. + intros LIVE; unfold liveness_checker in LIVE. + destruct liveness_checker_bool eqn:EQL; try congruence. + clear LIVE. unfold liveness_checker_bool in EQL. + rewrite lazy_and_Some_true in EQL; destruct EQL as [[ibf ENTRY] LIST]. + eexists; split; eauto. +Qed. + +Lemma liveness_checker_correct f n ibf: + liveness_checker f = OK tt -> + f.(fn_code)!n = Some ibf -> + iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) = Some tt. +Proof. + intros LIVE PC. + apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]]. + exploit list_iblock_checker_correct; eauto. + - eapply PTree.elements_correct; eauto. + - simpl; auto. +Qed. + +Lemma liveness_checker_entrypoint f: + liveness_checker f = OK tt -> + f.(fn_code)!(f.(fn_entrypoint)) <> None. +Proof. + intros LIVE; apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]]. + unfold not; intros CONTRA. congruence. +Qed. + +Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt. + +Inductive liveness_ok_fundef: fundef -> Prop := + | liveness_ok_Internal f: liveness_ok_function f -> liveness_ok_fundef (Internal f) + | liveness_ok_External ef: liveness_ok_fundef (External ef). + + +Local Notation ext alive := (fun r => Regset.In r alive). + +Definition ext_opt (oalive: option Regset.t): Regset.elt -> Prop := + match oalive with + | Some alive => ext alive + | None => fun _ => True + end. + +Lemma ext_opt_meet: forall r oalive1 oalive2, + ext_opt (meet oalive1 oalive2) r -> + ext_opt oalive1 r /\ ext_opt oalive2 r. +Proof. + intros. destruct oalive1, oalive2; + simpl in *; intuition. + eapply Regset.inter_1; eauto. + eapply Regset.inter_2; eauto. +Qed. + +Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live). +Proof. + destruct (Pos.eq_dec r1 r2). + - subst. intuition; eapply Regset.add_1; auto. + - intuition. + * right. eapply Regset.add_3; eauto. + * eapply Regset.add_2; auto. +Qed. + +Local Hint Resolve Regset.mem_2 Regset.subset_2: core. + +Lemma lazy_and_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true. +Proof. + destruct b1; simpl; intuition. +Qed. + +Lemma list_mem_correct (rl: list reg) (alive: Regset.t): + list_mem rl alive = true -> forall r, List.In r rl -> ext alive r. +Proof. + induction rl; simpl; try rewrite lazy_and_true; intuition subst; auto. +Qed. + +Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop := + forall r, (alive r) -> rs1#r = rs2#r. + +Lemma eqlive_reg_update (alive: Regset.elt -> Prop) rs1 rs2 r v: eqlive_reg (fun r1 => r1 <> r /\ alive r1) rs1 rs2 -> eqlive_reg alive (rs1 # r <- v) (rs2 # r <- v). +Proof. + unfold eqlive_reg; intros EQLIVE r0 ALIVE. + destruct (Pos.eq_dec r r0) as [H|H]. + - subst. rewrite! Regmap.gss. auto. + - rewrite! Regmap.gso; auto. +Qed. + +Lemma eqlive_reg_monotonic (alive1 alive2: Regset.elt -> Prop) rs1 rs2: eqlive_reg alive2 rs1 rs2 -> (forall r, alive1 r -> alive2 r) -> eqlive_reg alive1 rs1 rs2. +Proof. + unfold eqlive_reg; intuition. +Qed. + +Lemma eqlive_reg_list (alive: Regset.elt -> Prop) args rs1 rs2: eqlive_reg alive rs1 rs2 -> (forall r, List.In r args -> (alive r)) -> rs1##args = rs2##args. +Proof. + induction args; simpl; auto. + intros EQLIVE ALIVE; rewrite IHargs; auto. + unfold eqlive_reg in EQLIVE. + rewrite EQLIVE; auto. +Qed. + +Lemma eqlive_reg_listmem (alive: Regset.t) args rs1 rs2: eqlive_reg (ext alive) rs1 rs2 -> list_mem args alive = true -> rs1##args = rs2##args. +Proof. + intros; eapply eqlive_reg_list; eauto. + intros; eapply list_mem_correct; eauto. +Qed. + +Inductive eqlive_stackframes: stackframe -> stackframe -> Prop := + | eqlive_stackframes_intro ibf res f sp pc rs1 rs2 + (LIVE: liveness_ok_function f) + (ENTRY: f.(fn_code)!pc = Some ibf) + (EQUIV: forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # res <- v) (rs2 # res <- v)): + eqlive_stackframes (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2). + +Inductive eqlive_states: state -> state -> Prop := + | eqlive_states_intro + ibf st1 st2 f sp pc rs1 rs2 m + (STACKS: list_forall2 eqlive_stackframes st1 st2) + (LIVE: liveness_ok_function f) + (PATH: f.(fn_code)!pc = Some ibf) + (EQUIV: eqlive_reg (ext ibf.(input_regs)) rs1 rs2): + eqlive_states (State st1 f sp pc rs1 m) (State st2 f sp pc rs2 m) + | eqlive_states_call st1 st2 f args m + (LIVE: liveness_ok_fundef f) + (STACKS: list_forall2 eqlive_stackframes st1 st2): + eqlive_states (Callstate st1 f args m) (Callstate st2 f args m) + | eqlive_states_return st1 st2 v m + (STACKS: list_forall2 eqlive_stackframes st1 st2): + eqlive_states (Returnstate st1 v m) (Returnstate st2 v m). + +Section FSEM_SIMULATES_CFGSEM. + +Variable prog: BTL.program. + +Let ge := Genv.globalenv prog. + +Hypothesis all_fundef_liveness_ok: forall b f, Genv.find_funct_ptr ge b = Some f -> liveness_ok_fundef f. + +Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core. + +Lemma eqlive_reg_update_gso alive rs1 rs2 res r: forall v : val, + eqlive_reg (ext alive) rs1 # res <- v rs2 # res <- v -> + res <> r -> Regset.In r alive -> + rs1 # r = rs2 # r. +Proof. + intros v REGS NRES INR. unfold eqlive_reg in REGS. + specialize REGS with r. apply REGS in INR. + rewrite !Regmap.gso in INR; auto. +Qed. + +Lemma find_funct_liveness_ok v fd: + Genv.find_funct ge v = Some fd -> liveness_ok_fundef fd. +Proof. + unfold Genv.find_funct. + destruct v; try congruence. + destruct (Integers.Ptrofs.eq_dec _ _); try congruence. + eapply all_fundef_liveness_ok; eauto. +Qed. + +Lemma find_function_liveness_ok ros rs f: + find_function ge ros rs = Some f -> liveness_ok_fundef f. +Proof. + destruct ros as [r|i]; simpl. + - intros; eapply find_funct_liveness_ok; eauto. + - destruct (Genv.find_symbol ge i); try congruence. + eapply all_fundef_liveness_ok; eauto. +Qed. + +Lemma find_function_eqlive alive ros rs1 rs2: + eqlive_reg (ext alive) rs1 rs2 -> + reg_sum_mem ros alive = true -> + find_function ge ros rs1 = find_function ge ros rs2. +Proof. + intros EQLIVE. + destruct ros; simpl; auto. + intros H; erewrite (EQLIVE r); eauto. +Qed. + +Lemma exit_checker_eqlive (btl: code) (alive: Regset.t) (pc: node) rs1 rs2: + exit_checker btl alive pc = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists ibf, btl!pc = Some ibf /\ eqlive_reg (ext ibf.(input_regs)) rs1 rs2. +Proof. + unfold exit_checker. + inversion_SOME next. + inversion_ASSERT. try_simplify_someHyps. + repeat (econstructor; eauto). + intros; eapply eqlive_reg_monotonic; eauto. + intros; exploit Regset.subset_2; eauto. +Qed. + +Lemma exit_list_checker_eqlive (btl: code) (alive: Regset.t) (tbl: list node) rs1 rs2 pc: forall n, + exit_list_checker btl alive tbl = true -> + eqlive_reg (ext alive) rs1 rs2 -> + list_nth_z tbl n = Some pc -> + exists ibf, btl!pc = Some ibf /\ eqlive_reg (ext ibf.(input_regs)) rs1 rs2. +Proof. + induction tbl; simpl. + - intros; try congruence. + - intros n; rewrite lazy_and_Some_tt_true; destruct (zeq n 0) eqn: Hn. + * try_simplify_someHyps; intuition. + exploit exit_checker_eqlive; eauto. + * intuition. eapply IHtbl; eauto. +Qed. + +Lemma exit_checker_eqlive_update (btl: code) (alive: Regset.t) (pc: node) r rs1 rs2: + exit_checker btl (Regset.add r alive) pc = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists ibf, btl!pc = Some ibf /\ (forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # r <- v) (rs2 # r <- v)). +Proof. + unfold exit_checker. + inversion_SOME next. + inversion_ASSERT. try_simplify_someHyps. + repeat (econstructor; eauto). + intros; eapply eqlive_reg_update; eauto. + eapply eqlive_reg_monotonic; eauto. + intros r0 [X1 X2]; exploit Regset.subset_2; eauto. + rewrite regset_add_spec. intuition subst. +Qed. + +Lemma exit_checker_eqlive_builtin_res (btl: code) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg): + exit_checker btl (reg_builtin_res res alive) pc = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists ibf, btl!pc = Some ibf /\ (forall vres, eqlive_reg (ext ibf.(input_regs)) (regmap_setres res vres rs1) (regmap_setres res vres rs2)). +Proof. + destruct res; simpl. + - intros; exploit exit_checker_eqlive_update; eauto. + - intros; exploit exit_checker_eqlive; eauto. + intros (ibf & PC & REGS). + eexists; intuition eauto. + - intros; exploit exit_checker_eqlive; eauto. + intros (ibf & PC & REGS). + eexists; intuition eauto. +Qed. + +Local Hint Resolve in_or_app: local. +Lemma eqlive_eval_builtin_args alive rs1 rs2 sp m args vargs: + eqlive_reg alive rs1 rs2 -> + Events.eval_builtin_args ge (fun r => rs1 # r) sp m args vargs -> + (forall r, List.In r (params_of_builtin_args args) -> alive r) -> + Events.eval_builtin_args ge (fun r => rs2 # r) sp m args vargs. +Proof. + unfold Events.eval_builtin_args. + intros EQLIVE; induction 1 as [|a1 al b1 bl EVAL1 EVALL]; simpl. + { econstructor; eauto. } + intro X. + assert (X1: eqlive_reg (fun r => In r (params_of_builtin_arg a1)) rs1 rs2). + { eapply eqlive_reg_monotonic; eauto with local. } + lapply IHEVALL; eauto with local. + clear X IHEVALL; intro X. econstructor; eauto. + generalize X1; clear EVALL X1 X. + induction EVAL1; simpl; try (econstructor; eauto; fail). + - intros X1; erewrite X1; [ econstructor; eauto | eauto ]. + - intros; econstructor. + + eapply IHEVAL1_1; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + + eapply IHEVAL1_2; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + - intros; econstructor. + + eapply IHEVAL1_1; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + + eapply IHEVAL1_2; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. +Qed. + +Lemma tr_inputs_eqlive_None f pc tbl ibf rs1 rs2 + (PC: (fn_code f) ! pc = Some ibf) + (REGS: eqlive_reg (ext (input_regs ibf)) rs1 rs2) + :eqlive_reg (ext (input_regs ibf)) (tid f (pc :: tbl) None rs1) + (tr_inputs f (pc :: tbl) None rs2). +Proof. + unfold eqlive_reg. intros r INR. + unfold tid. rewrite tr_inputs_get. + simpl. rewrite PC. + exploit Regset.union_3. eapply INR. + intros INRU. eapply Regset.mem_1 in INRU. + erewrite INRU; eauto. +Qed. + +Lemma tr_inputs_eqlive_list_None tbl: forall f pc n alive ibf rs1 rs2 + (REGS1: eqlive_reg (ext alive) rs1 rs2) + (EXIT_LIST: exit_list_checker (fn_code f) alive tbl = true) + (LIST: list_nth_z tbl n = Some pc) + (PC: (fn_code f) ! pc = Some ibf) + (REGS2: eqlive_reg (ext (input_regs ibf)) rs1 rs2), + eqlive_reg (ext (input_regs ibf)) (tid f tbl None rs1) + (tr_inputs f tbl None rs2). +Proof. + induction tbl as [| pc' tbl IHtbl]; try_simplify_someHyps. + autodestruct; try_simplify_someHyps. + - intros; eapply tr_inputs_eqlive_None; eauto. + - rewrite lazy_and_Some_tt_true in EXIT_LIST. + destruct EXIT_LIST as [EXIT EXIT_REM]. + intros. unfold eqlive_reg. intros r INR. + exploit (IHtbl f pc (Z.pred n) alive ibf rs1 rs2); eauto. + unfold tid. rewrite !tr_inputs_get. + exploit exit_checker_eqlive; eauto. + intros (ibf' & PC' & REGS3). + simpl; rewrite PC'. autodestruct. + + intro INRU. apply Regset.mem_2 in INRU. + intros EQR. eapply Regset.union_2 in INRU. + eapply Regset.mem_1 in INRU. erewrite INRU; auto. + + intros. autodestruct. + rewrite (REGS2 r); auto. +Qed. + +Lemma tr_inputs_eqlive_update f pc ibf rs1 rs2 res + (PC: (fn_code f) ! pc = Some ibf) + :forall (v: val) + (REGS: eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v), + eqlive_reg (ext (input_regs ibf)) + (tid f (pc :: nil) (Some res) rs1) # res <- v + (tr_inputs f (pc :: nil) (Some res) rs2) # res <- v. +Proof. + intros. apply eqlive_reg_update. + unfold eqlive_reg. intros r (NRES & INR). + unfold tid. rewrite tr_inputs_get. + simpl. rewrite PC. assert (NRES': res <> r) by auto. + clear NRES. exploit Regset.union_3. eapply INR. + intros INRU. exploit Regset.remove_2; eauto. + intros INRU_RES. eapply Regset.mem_1 in INRU_RES. + erewrite INRU_RES. eapply eqlive_reg_update_gso; eauto. +Qed. + +Local Hint Resolve tr_inputs_eqlive_None tr_inputs_eqlive_update: core. +Lemma cfgsem2fsem_finalstep_simu sp f stk1 stk2 s t fin alive rs1 m rs2 + (FSTEP: final_step tid ge stk1 f sp rs1 m fin t s) + (LIVE: liveness_ok_function f) + (REGS: eqlive_reg (ext alive) rs1 rs2) + (FCHK: final_inst_checker (fn_code f) alive fin = Some tt) + (STACKS: list_forall2 eqlive_stackframes stk1 stk2) + :exists s', + final_step tr_inputs ge stk2 f sp rs2 m fin t s' + /\ eqlive_states s s'. +Proof. + destruct FSTEP; try_simplify_someHyps; repeat inversion_ASSERT; intros. + - (* Bgoto *) + eexists; split. + + econstructor; eauto. + + exploit exit_checker_eqlive; eauto. + intros (ibf & PC & REGS'). + econstructor; eauto. + - (* Breturn *) + eexists; split. econstructor; eauto. + destruct or; simpl in *; + try erewrite (REGS r); eauto. + - (* Bcall *) + exploit exit_checker_eqlive_update; eauto. + intros (ibf & PC & REGS'). + eexists; split. + + econstructor; eauto. + erewrite <- find_function_eqlive; eauto. + + erewrite eqlive_reg_listmem; eauto. + eapply eqlive_states_call; eauto. + eapply find_function_liveness_ok; eauto. + - (* Btailcall *) + eexists; split. + + econstructor; eauto. + erewrite <- find_function_eqlive; eauto. + + erewrite eqlive_reg_listmem; eauto. + eapply eqlive_states_call; eauto. + eapply find_function_liveness_ok; eauto. + - (* Bbuiltin *) + exploit exit_checker_eqlive_builtin_res; eauto. + intros (ibf & PC & REGS'). + eexists; split. + + econstructor; eauto. + eapply eqlive_eval_builtin_args; eauto. + intros; eapply list_mem_correct; eauto. + + repeat (econstructor; simpl; eauto). + unfold regmap_setres. destruct res; simpl in *; eauto. + - (* Bjumptable *) + exploit exit_list_checker_eqlive; eauto. + intros (ibf & PC & REGS'). + eexists; split. + + econstructor; eauto. + erewrite <- REGS; eauto. + + repeat (econstructor; simpl; eauto). + apply (tr_inputs_eqlive_list_None tbl f pc' (Int.unsigned n) alive ibf rs1 rs2); + auto. +Qed. + +Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m' + (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' None) + alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2) + (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2)), + exists rs2', + iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' None) + /\ eqlive_reg (ext_opt oalive2) rs1' rs2'. +Proof. + induction ib; intros; try_simplify_someHyps; + repeat inversion_ASSERT; intros; inv ISTEP. + - (* Bnop *) + inv BDY; eauto. + - (* Bop *) + erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps; intros. + repeat econstructor. + apply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + intros r0; rewrite regset_add_spec. + intuition. + - (* Bload *) + erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps; intros. + rewrite LOAD; eauto. + repeat econstructor. + apply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + intros r0; rewrite regset_add_spec. + intuition. + - (* Bstore *) + erewrite <- eqlive_reg_listmem; eauto. + rewrite <- (REGS src); auto. + try_simplify_someHyps; intros. + rewrite STORE; eauto. + - (* Bseq continue *) + destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate. + generalize BDY; clear BDY. + inversion_SOME aliveMid; intros OALIVE BDY2. inv OALIVE. + exploit IHib1; eauto. + intros (rs2' & ISTEP1 & REGS1). rewrite ISTEP1; simpl. + eapply IHib2; eauto. + - (* Bcond *) + generalize BDY; clear BDY. + inversion_SOME oaliveSo; inversion_SOME oaliveNot; intros BDY1 BDY2 JOIN. + erewrite <- eqlive_reg_listmem; eauto. + rewrite EVAL. + destruct b; [ exploit IHib1; eauto | exploit IHib2; eauto]. + all: + intros (rs2' & ISTEP1 & REGS1); + econstructor; split; eauto; inv JOIN; + eapply eqlive_reg_monotonic; eauto; + intros r EXTM; apply ext_opt_meet in EXTM; intuition. +Qed. + +Lemma cfgsem2fsem_ibistep_simu_Some sp f stk1 stk2 ib: forall s t rs1 m rs1' m' fin + (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' (Some fin)) + (FSTEP: final_step tid ge stk1 f sp rs1' m' fin t s) + alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2) + (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2)) + (LIVE: liveness_ok_function f) + (*(PC : (fn_code f) ! pc = Some ibf)*) + (STACKS: list_forall2 eqlive_stackframes stk1 stk2), + exists rs2' s', + iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' (Some fin)) + /\ final_step tr_inputs ge stk2 f sp rs2' m' fin t s' + /\ eqlive_states s s'. +Proof. + induction ib; simpl; try_simplify_someHyps; + repeat inversion_ASSERT; intros; inv ISTEP. + - (* BF *) + generalize BDY; clear BDY. + inversion_SOME x; try_simplify_someHyps; intros FCHK. + destruct x; exploit cfgsem2fsem_finalstep_simu; eauto. + intros (s2 & FSTEP' & STATES); eauto. + - (* Bseq stop *) + destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate. + generalize BDY; clear BDY. + inversion_SOME aliveMid. intros OALIVE BDY2. inv OALIVE. + exploit IHib1; eauto. intros (rs2' & s' & ISTEP1 & FSTEP1 & STATES). + rewrite ISTEP1; simpl. + do 2 eexists; intuition eauto. + - (* Bseq continue *) + destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate. + generalize BDY; clear BDY. + inversion_SOME aliveMid; intros OALIVE BDY2. inv OALIVE. + exploit cfgsem2fsem_ibistep_simu_None; eauto. + intros (rs2' & ISTEP1 & REGS'). rewrite ISTEP1; simpl; eauto. + - (* Bcond *) + generalize BDY; clear BDY. + inversion_SOME oaliveSo; inversion_SOME oaliveNot; intros BDY1 BDY2 JOIN. + erewrite <- eqlive_reg_listmem; eauto. rewrite EVAL. + destruct b; eauto. +Qed. + +Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t: + iblock_step tid (Genv.globalenv prog) stk1 f sp rs1 m ibf.(entry) t s1 -> + list_forall2 eqlive_stackframes stk1 stk2 -> + eqlive_reg (ext (input_regs ibf)) rs1 rs2 -> + liveness_ok_function f -> + (fn_code f) ! pc = Some ibf -> + exists s2 : state, + iblock_step tr_inputs (Genv.globalenv prog) stk2 f sp rs2 m ibf.(entry) t s2 /\ + eqlive_states s1 s2. +Proof. + intros STEP STACKS EQLIVE LIVE PC. + assert (CHECKER: liveness_ok_function f) by auto. + unfold liveness_ok_function in CHECKER. + apply decomp_liveness_checker in CHECKER; destruct CHECKER as [ibf' [ENTRY LIST]]. + eapply PTree.elements_correct in PC as PCIN. + eapply list_iblock_checker_correct in LIST as IBC; eauto. + unfold iblock_checker in IBC. generalize IBC; clear IBC. + inversion_SOME alive; intros BODY _. + destruct STEP as (rs1' & m1' & fin' & ISTEP & FSTEP). + exploit cfgsem2fsem_ibistep_simu_Some; eauto. + intros (rs2' & s' & ISTEP' & FSTEP' & REGS). + rewrite <- iblock_istep_run_equiv in ISTEP'. clear ISTEP. + unfold iblock_step. repeat eexists; eauto. +Qed. + +Local Hint Constructors step: core. + +Lemma cfgsem2fsem_step_simu s1 s1' t s2: + step tid (Genv.globalenv prog) s1 t s1' -> + eqlive_states s1 s2 -> + exists s2' : state, + step tr_inputs (Genv.globalenv prog) s2 t s2' /\ + eqlive_states s1' s2'. +Proof. + destruct 1 as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; intros STATES. + - (* iblock *) + inv STATES; simplify_someHyps. + intros. + exploit cfgsem2fsem_ibstep_simu; eauto. + intros (s2 & STEP2 & EQUIV2). + eexists; split; eauto. + - (* function internal *) + inv STATES; inv LIVE. + apply liveness_checker_entrypoint in H0 as ENTRY. + destruct ((fn_code f) ! (fn_entrypoint f)) eqn:EQENTRY; try congruence; eauto. + eexists; split; repeat econstructor; eauto. + - (* function external *) + inv STATES; inv LIVE; eexists; split; econstructor; eauto. + - (* return *) + inv STATES. + inversion STACKS as [|s1 st1 s' s2 STACK STACKS']; subst; clear STACKS. + inv STACK. + exists (State s2 f sp pc (rs2 # res <- vres) m); split. + * apply exec_return. + * eapply eqlive_states_intro; eauto. +Qed. + +Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog). +Proof. + eapply forward_simulation_step with eqlive_states; simpl; eauto. + - destruct 1, f; intros; eexists; intuition eauto; + repeat (econstructor; eauto). + - intros s1 s2 r STATES FINAL; destruct FINAL. + inv STATES; inv STACKS; constructor. + - intros. eapply cfgsem2fsem_step_simu; eauto. +Qed. + +End FSEM_SIMULATES_CFGSEM. + + diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v new file mode 100644 index 00000000..852bced0 --- /dev/null +++ b/scheduling/BTL_SEsimuref.v @@ -0,0 +1,807 @@ +(** Refinement of BTL_SEtheory data-structures + in order to introduce (and prove correct) a lower-level specification of the simulation test. + + Ceci est un "bac à sable". + + - On introduit une représentation plus concrète pour les types d'état symbolique [sistate] et [sstate]. + - Etant donné une spécification intuitive "*_simu" pour tester la simulation sur cette représentation des états symboliques, + on essaye déjà de trouver les bonnes notions de raffinement "*_refines" qui permette de prouver les lemmes "*_simu_correct". + - Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement ! + +*) + +Require Import Coqlib Maps Floats. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL BTL OptionMonad BTL_SEtheory. + + +Local Open Scope option_monad_scope. + +(** * Refinement of data-structures and of the specification of the simulation test *) + +Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core. +Local Hint Constructors si_ok: core. + +(* NB: refinement of (symbolic) internal state *) +Record ristate := + { + (** [ris_smem] represents the current smem symbolic evaluations. + (we also recover the history of smem in ris_smem) *) + ris_smem: smem; + (** For the values in registers: + 1) we store a list of sval evaluations + 2) we encode the symbolic regset by a PTree + a boolean indicating the default sval *) + ris_input_init: bool; + ok_rsval: list sval; + ris_sreg:> PTree.t sval + }. + +Definition ris_sreg_get (ris: ristate) r: sval := + match PTree.get r ris with + | None => if ris_input_init ris then Sinput r else Sundef + | Some sv => sv + end. +Coercion ris_sreg_get: ristate >-> Funclass. + +Record ris_ok ctx (ris: ristate) : Prop := { + OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None; + OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None +}. +Local Hint Resolve OK_RMEM OK_RREG: core. +Local Hint Constructors ris_ok: core. + +(* TODO: Is it useful ? +Definition ris_abs (ris: ristate) : sistate := {| + si_pre := fun ctx => ris_ok ctx ris; + si_sreg := ris_sreg_get ris; + si_smem := ris.(ris_smem) +|}. +*) + +Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := { + OK_EQUIV: si_ok ctx sis <-> ris_ok ctx ris; + MEM_EQ: ris_ok ctx ris -> eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(si_smem); + REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r) +}. +Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ: core. +Local Hint Constructors ris_refines: core. + +Record ris_simu ris1 ris2: Prop := { + SIMU_FAILS: forall sv, List.In sv ris2.(ok_rsval) -> List.In sv ris1.(ok_rsval); + SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem); + SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r +}. +Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core. +Local Hint Constructors ris_simu: core. +Local Hint Resolve sge_match: core. + +Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2): + ris_simu ris1 ris2 -> ris_ok (bctx1 ctx) ris1 -> ris_ok (bctx2 ctx) ris2. +Proof. + intros SIMU OK; econstructor; eauto. + - erewrite <- SIMU_MEM; eauto. + erewrite <- smem_eval_preserved; eauto. + - intros; erewrite <- eval_sval_preserved; eauto. +Qed. + +Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2: + ris_simu ris1 ris2 -> + ris_refines (bctx1 ctx) ris1 sis1 -> + ris_refines (bctx2 ctx) ris2 sis2 -> + sistate_simu ctx sis1 sis2. +Proof. + intros RIS REF1 REF2 rs m SEM. + exploit sem_si_ok; eauto. + erewrite OK_EQUIV; eauto. + intros ROK1. + exploit ris_simu_ok_preserv; eauto. + intros ROK2. generalize ROK2; erewrite <- OK_EQUIV; eauto. + intros SOK2. + destruct SEM as (PRE & SMEM & SREG). + unfold sem_sistate; intuition eauto. + + erewrite <- MEM_EQ, <- SIMU_MEM; eauto. + erewrite <- smem_eval_preserved; eauto. + erewrite MEM_EQ; eauto. + + erewrite <- REG_EQ, <- SIMU_REG; eauto. + erewrite <- eval_sval_preserved; eauto. + erewrite REG_EQ; eauto. +Qed. + +Inductive optrsv_refines ctx: (option sval) -> (option sval) -> Prop := + | RefSome rsv sv + (REF:eval_sval ctx rsv = eval_sval ctx sv) + :optrsv_refines ctx (Some rsv) (Some sv) + | RefNone: optrsv_refines ctx None None + . + +Inductive rsvident_refines ctx: (sval + ident) -> (sval + ident) -> Prop := + | RefLeft rsv sv + (REF:eval_sval ctx rsv = eval_sval ctx sv) + :rsvident_refines ctx (inl rsv) (inl sv) + | RefRight id1 id2 + (IDSIMU: id1 = id2) + :rsvident_refines ctx (inr id1) (inr id2) + . + +Definition bargs_refines ctx (rargs: list (builtin_arg sval)) (args: list (builtin_arg sval)): Prop := + eval_list_builtin_sval ctx rargs = eval_list_builtin_sval ctx args. + +Inductive rfv_refines ctx: sfval -> sfval -> Prop := + | RefGoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc) + | RefCall sig rvos ros rargs args r pc + (SV:rsvident_refines ctx rvos ros) + (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args) + :rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc) + | RefTailcall sig rvos ros rargs args + (SV:rsvident_refines ctx rvos ros) + (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args) + :rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args) + | RefBuiltin ef lbra lba br pc + (BARGS: bargs_refines ctx lbra lba) + :rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc) + | RefJumptable rsv sv lpc + (VAL: eval_sval ctx rsv = eval_sval ctx sv) + :rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc) + | RefReturn orsv osv + (OPT:optrsv_refines ctx orsv osv) + :rfv_refines ctx (Sreturn orsv) (Sreturn osv) +. + +Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2. + +Local Hint Resolve eval_sval_preserved list_sval_eval_preserved smem_eval_preserved eval_list_builtin_sval_preserved: core. + +Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2: + rfv_simu rfv1 rfv2 -> + rfv_refines (bctx1 ctx) rfv1 sfv1 -> + rfv_refines (bctx2 ctx) rfv2 sfv2 -> + sfv_simu ctx sfv1 sfv2. +Proof. + unfold rfv_simu; intros X REF1 REF2. subst. + unfold bctx2; destruct REF1; inv REF2; simpl; econstructor; eauto. + - (* call svid *) + inv SV; inv SV0; econstructor; eauto. + rewrite <- REF, <- REF0; eauto. + - (* call args *) + rewrite <- LIST, <- LIST0; eauto. + - (* taillcall svid *) + inv SV; inv SV0; econstructor; eauto. + rewrite <- REF, <- REF0; eauto. + - (* tailcall args *) + rewrite <- LIST, <- LIST0; eauto. + - (* builtin args *) + unfold bargs_refines, bargs_simu in *. + rewrite <- BARGS, <- BARGS0; eauto. + - rewrite <- VAL, <- VAL0; eauto. + - (* return *) + inv OPT; inv OPT0; econstructor; eauto. + rewrite <- REF, <- REF0; eauto. +Qed. + +(* refinement of (symbolic) state *) +Inductive rstate := + | Rfinal (ris: ristate) (rfv: sfval) + | Rcond (cond: condition) (rargs: list_sval) (rifso rifnot: rstate) + | Rabort + . + + +Record routcome := rout { + _ris: ristate; + _rfv: sfval; +}. + +Fixpoint get_routcome ctx (rst:rstate): option routcome := + match rst with + | Rfinal ris rfv => Some (rout ris rfv) + | Rcond cond args ifso ifnot => + SOME b <- seval_condition ctx cond args IN + get_routcome ctx (if b then ifso else ifnot) + | Rabort => None + end. + +Inductive rst_simu: rstate -> rstate -> Prop := + | Rfinal_simu ris1 ris2 rfv1 rfv2 + (RIS: ris_simu ris1 ris2) + (RFV: rfv_simu rfv1 rfv2) + : rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2) + | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2 + (IFSO: rst_simu rifso1 rifso2) + (IFNOT: rst_simu rifnot1 rifnot2) + : rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2) + | Rabort_simu: rst_simu Rabort Rabort +(* TODO: extension à voir dans un second temps ! + | Rcond_skip cond rargs rifso1 rifnot1 rst: + rst_simu rifso1 rst -> + rst_simu rifnot1 rst -> + rst_simu (Rcond cond rargs rifso1 rifnot1) rst +*) + . + +Lemma rst_simu_lroutcome rst1 rst2: + rst_simu rst1 rst2 -> + forall f1 f2 (ctx: simu_proof_context f1 f2) ris1 rfv1, + get_routcome (bctx1 ctx) rst1 = Some (rout ris1 rfv1) -> + exists ris2 rfv2, get_routcome (bctx2 ctx) rst2 = Some (rout ris2 rfv2) /\ ris_simu ris1 ris2 /\ rfv_simu rfv1 rfv2. +Proof. + induction 1; simpl; intros f1 f2 ctx lris1 lrfv1 ROUT; try_simplify_someHyps. + erewrite <- seval_condition_preserved. + autodestruct. + destruct b; simpl; auto. +Qed. + +Inductive rst_refines ctx: rstate -> sstate -> Prop := + | Reffinal ris sis rfv sfv + (RIS: ris_refines ctx ris sis) + (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv) + : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv) + | Refcond cond rargs args rifso rifnot ifso ifnot + (RCOND: seval_condition ctx cond rargs = seval_condition ctx cond args) + (REFso: seval_condition ctx cond rargs = Some true -> rst_refines ctx rifso ifso) + (REFnot: seval_condition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot) + : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args ifso ifnot) + | Refabort + : rst_refines ctx Rabort Sabort + . + +Lemma rst_refines_outcome_up ctx rst st: + rst_refines ctx rst st -> + forall ris rfv, + get_routcome ctx rst = Some (rout ris rfv) -> + exists sis sfv, get_soutcome ctx st = Some (sout sis sfv) /\ ris_refines ctx ris sis /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv). +Proof. + induction 1; simpl; intros lris lrfv ROUT; try_simplify_someHyps. + rewrite RCOND. + autodestruct. + destruct b; simpl; auto. +Qed. + +Lemma rst_refines_outcome_down ctx rst st: + rst_refines ctx rst st -> + forall sis sfv, + get_soutcome ctx st = Some (sout sis sfv) -> + exists ris rfv, get_routcome ctx rst = Some (rout ris rfv) /\ ris_refines ctx ris sis /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv). +Proof. + induction 1; simpl; intros lris lrfv ROUT; try_simplify_someHyps. + rewrite RCOND. + autodestruct. + destruct b; simpl; auto. +Qed. + +Local Hint Resolve ris_simu_correct rvf_simu_correct: core. + +Lemma rst_simu_correct f1 f2 (ctx: simu_proof_context f1 f2) rst1 rst2 st1 st2 + (SIMU: rst_simu rst1 rst2) + (REF1: forall sis sfv, get_soutcome (bctx1 ctx) st1 = Some (sout sis sfv) -> si_ok (bctx1 ctx) sis -> rst_refines (bctx1 ctx) rst1 st1) + (REF2: forall ris rfv, get_routcome (bctx2 ctx) rst2 = Some (rout ris rfv) -> ris_ok (bctx2 ctx) ris -> rst_refines (bctx2 ctx) rst2 st2) + :sstate_simu ctx st1 st2. +Proof. + intros sis1 sfv1 SOUT OK1. + exploit REF1; eauto. + clear REF1; intros REF1. + exploit rst_refines_outcome_down; eauto. clear REF1 SOUT. + intros (ris1 & rfv1 & ROUT1 & REFI1 & REFF1). + rewrite OK_EQUIV in OK1; eauto. + exploit REFF1; eauto. clear REFF1; intros REFF1. + exploit rst_simu_lroutcome; eauto. + intros (ris2 & rfv2 & ROUT2 & SIMUI & SIMUF). clear ROUT1. + exploit ris_simu_ok_preserv; eauto. + clear OK1. intros OK2. + exploit REF2; eauto. clear REF2; intros REF2. + exploit rst_refines_outcome_up; eauto. + intros (sis2 & sfv2 & SOUT & REFI2 & REFF2). + do 2 eexists; split; eauto. +Qed. + +(** * Refinement of the symbolic execution *) + +Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core. + +Lemma eval_list_sval_refpreserv ctx args ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + eval_list_sval ctx (list_sval_inj (map ris args)) = + eval_list_sval ctx (list_sval_inj (map (si_sreg sis) args)). +Proof. + intros REF OK. + induction args; simpl; eauto. + intros; erewrite REG_EQ, IHargs; eauto. +Qed. + +Local Hint Resolve eval_list_sval_refpreserv: core. + +Lemma eval_builtin_sval_refpreserv ctx arg ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + eval_builtin_sval ctx (builtin_arg_map ris arg) = eval_builtin_sval ctx (builtin_arg_map sis arg). +Proof. + intros REF OK; induction arg; simpl; eauto. + + erewrite REG_EQ; eauto. + + erewrite IHarg1, IHarg2; eauto. + + erewrite IHarg1, IHarg2; eauto. +Qed. + +Lemma bargs_refpreserv ctx args ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + bargs_refines ctx (map (builtin_arg_map ris) args) (map (builtin_arg_map sis) args). +Proof. + unfold bargs_refines. intros REF OK. + induction args; simpl; eauto. + erewrite eval_builtin_sval_refpreserv, IHargs; eauto. +Qed. + +Local Hint Resolve bargs_refpreserv: core. + +Lemma exec_final_refpreserv ctx i ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + rfv_refines ctx (sexec_final_sfv i ris) (sexec_final_sfv i sis). +Proof. + destruct i; simpl; unfold sum_left_map; try autodestruct; eauto. +Qed. + +Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ok_rsval := nil; ris_sreg := PTree.empty _ |}. + +Lemma ris_init_correct ctx: + ris_refines ctx ris_init sis_init. +Proof. + unfold ris_init, sis_init; econstructor; simpl in *; eauto. + + split; destruct 1; econstructor; simpl in *; eauto. + congruence. + + destruct 1; simpl in *. unfold ris_sreg_get; simpl. + intros; rewrite PTree.gempty; eauto. +Qed. + +Definition rset_smem rm (ris:ristate): ristate := + {| ris_smem := rm; + ris_input_init := ris.(ris_input_init); + ok_rsval := ris.(ok_rsval); + ris_sreg:= ris.(ris_sreg) + |}. + +Lemma ok_set_mem ctx sm sis: + si_ok ctx (set_smem sm sis) + <-> (si_ok ctx sis /\ eval_smem ctx sm <> None). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. + intuition eauto. +Qed. + +Lemma ok_rset_mem ctx rm (ris: ristate): + (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) -> + ris_ok ctx (rset_smem rm ris) + <-> (ris_ok ctx ris /\ eval_smem ctx rm <> None). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. +Qed. + +Lemma rset_mem_correct ctx rm sm ris sis: + (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) -> + ris_refines ctx ris sis -> + (ris_ok ctx ris -> eval_smem ctx rm = eval_smem ctx sm) -> + ris_refines ctx (rset_smem rm ris) (set_smem sm sis). +Proof. + destruct 2; intros. + econstructor; eauto. + + rewrite ok_set_mem, ok_rset_mem; intuition congruence. + + rewrite ok_rset_mem; intuition eauto. + + rewrite ok_rset_mem; intuition eauto. +Qed. + +Definition rexec_store chunk addr args src ris: ristate := + let args := list_sval_inj (List.map (ris_sreg_get ris) args) in + let src := ris_sreg_get ris src in + let rm := Sstore ris.(ris_smem) chunk addr args src in + rset_smem rm ris. + +Lemma rexec_store_correct ctx chunk addr args src ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (rexec_store chunk addr args src ris) (sexec_store chunk addr args src sis). +Proof. + intros REF; eapply rset_mem_correct; simpl; eauto. + + intros X; rewrite X. repeat autodestruct; eauto. + + intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ, REG_EQ; eauto. +Qed. + +(* TODO: reintroduire le "root_apply" ? *) + +Definition rset_sreg r rsv (ris:ristate): ristate := + {| ris_smem := ris.(ris_smem); + ris_input_init := ris.(ris_input_init); + ok_rsval := rsv::ris.(ok_rsval); (* TODO: A CHANGER ? *) + ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *) + |}. + +Lemma ok_set_sreg ctx r sv sis: + si_ok ctx (set_sreg r sv sis) + <-> (si_ok ctx sis /\ eval_sval ctx sv <> None). +Proof. + unfold set_sreg; split. + + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split. + - econstructor; eauto. + intros r0; generalize (SREG r0); destruct (Pos.eq_dec r r0); try congruence. + - generalize (SREG r); destruct (Pos.eq_dec r r); try congruence. + + intros ([PRE SMEM SREG] & SVAL). + econstructor; simpl; eauto. + intros r0; destruct (Pos.eq_dec r r0); try congruence. +Qed. + +Lemma ok_rset_sreg ctx r rsv ris: + ris_ok ctx (rset_sreg r rsv ris) + <-> (ris_ok ctx ris /\ eval_sval ctx rsv <> None). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. + intuition subst; eauto. + exploit OK_RREG; eauto. +Qed. + +Lemma rset_reg_correct ctx r rsv sv ris sis: + ris_refines ctx ris sis -> + (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) -> + ris_refines ctx (rset_sreg r rsv ris) (set_sreg r sv sis). +Proof. + destruct 1; intros. + econstructor; eauto. + + rewrite ok_set_sreg, ok_rset_sreg; intuition congruence. + + rewrite ok_rset_sreg; intuition eauto. + + rewrite ok_rset_sreg. intros; unfold rset_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto. + destruct (Pos.eq_dec _ _). + * subst; rewrite PTree.gss; eauto. + * rewrite PTree.gso; eauto. +Qed. + +Definition rexec_op op args dst (ris:ristate): ristate := + let args := list_sval_inj (List.map ris args) in + rset_sreg dst (Sop op args) ris. + +Lemma rexec_op_correct ctx op args dst ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (rexec_op op args dst ris) (sexec_op op args dst sis). +Proof. + intros REF; eapply rset_reg_correct; simpl; eauto. + intros OK; erewrite eval_list_sval_refpreserv; eauto. +Qed. + +Definition rexec_load trap chunk addr args dst (ris:ristate): ristate := + let args := list_sval_inj (List.map ris args) in + rset_sreg dst (Sload ris.(ris_smem) trap chunk addr args) ris. + +Lemma rexec_load_correct ctx trap chunk addr args dst ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (rexec_load trap chunk addr args dst ris) (sexec_load trap chunk addr args dst sis). +Proof. + intros REF; eapply rset_reg_correct; simpl; eauto. + intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ; eauto. +Qed. + +Lemma seval_condition_refpreserv ctx cond args ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + seval_condition ctx cond (list_sval_inj (map ris args)) = seval_condition ctx cond (list_sval_inj (map sis args)). +Proof. + intros; unfold seval_condition. + erewrite eval_list_sval_refpreserv; eauto. +Qed. + + +(* transfer *) + +Definition rseto_sreg r rsv (ris:ristate): ristate := + {| ris_smem := ris.(ris_smem); + ris_input_init := ris.(ris_input_init); + ok_rsval := ris.(ok_rsval); + ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *) + |}. + +Lemma ok_rseto_sreg ctx r rsv ris: + ris_ok ctx (rseto_sreg r rsv ris) + <-> (ris_ok ctx ris). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. +Qed. + +Lemma rseto_reg_correct ctx r rsv sv ris sis: + ris_refines ctx ris sis -> + (ris_ok ctx ris -> eval_sval ctx rsv <> None) -> + (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) -> + ris_refines ctx (rseto_sreg r rsv ris) (set_sreg r sv sis). +Proof. + destruct 1; intros. + econstructor; eauto. + + rewrite ok_set_sreg, ok_rseto_sreg; intuition congruence. + + rewrite ok_rseto_sreg; intuition eauto. + + rewrite ok_rseto_sreg. intros; unfold rseto_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto. + destruct (Pos.eq_dec _ _). + * subst; rewrite PTree.gss; eauto. + * rewrite PTree.gso; eauto. +Qed. + +Fixpoint transfer_ris (inputs: list reg) (ris:ristate): ristate := + match inputs with + | nil => {| ris_smem := ris.(ris_smem); + ris_input_init := false; + ok_rsval := ris.(ok_rsval); + ris_sreg:= PTree.empty _ + |} + | r::l => rseto_sreg r (ris_sreg_get ris r) (transfer_ris l ris) + end. + +Definition transfer_sis (inputs: list reg) (sis:sistate): sistate := + {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None); + si_sreg := transfer_sreg inputs sis; + si_smem := sis.(si_smem) |}. + +Lemma ok_transfer_sis ctx inputs sis: + si_ok ctx (transfer_sis inputs sis) + <-> (si_ok ctx sis). +Proof. + unfold transfer_sis. induction inputs as [|r l]; simpl. + + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence. + + split. + * destruct 1; econstructor; simpl in *; intuition eauto. + * intros X; generalize X. rewrite <- IHl in X; clear IHl. + intros [PRE SMEM SREG]. + econstructor; simpl; eauto. + intros r0; destruct (Pos.eq_dec r r0); try congruence. + intros H; eapply OK_SREG; eauto. +Qed. + +Lemma ok_transfer_ris ctx inputs ris: + ris_ok ctx (transfer_ris inputs ris) + <-> (ris_ok ctx ris). +Proof. + induction inputs as [|r l]; simpl. + + split; destruct 1; econstructor; simpl in *; intuition eauto. + + rewrite ok_rseto_sreg. auto. +Qed. + +Lemma transfer_ris_correct ctx inputs ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (transfer_ris inputs ris) (transfer_sis inputs sis). +Proof. + destruct 1; intros. + induction inputs as [|r l]. + + econstructor; eauto. + * erewrite ok_transfer_sis, ok_transfer_ris; eauto. + * erewrite ok_transfer_ris; eauto. + * erewrite ok_transfer_ris; simpl; unfold ris_sreg_get; simpl; eauto. + intros; rewrite PTree.gempty. simpl; auto. + + econstructor; eauto. + * erewrite ok_transfer_sis, ok_transfer_ris; eauto. + * erewrite ok_transfer_ris; simpl. + intros; erewrite MEM_EQ. 2: eauto. + - unfold transfer_sis; simpl; eauto. + - rewrite ok_transfer_ris; simpl; eauto. + * erewrite ok_transfer_ris; simpl. + intros H r0. + erewrite REG_EQ. 2: eapply rseto_reg_correct; eauto. + - unfold set_sreg; simpl; auto. + destruct (Pos.eq_dec _ _); simpl; auto. + - intros. rewrite REG_EQ0; auto. apply OK_SREG; tauto. + - rewrite ok_rseto_sreg, ok_transfer_ris. auto. +Qed. + +Definition alt_tr_sis := poly_tr (fun f tbl or => transfer_sis (Regset.elements (pre_inputs f tbl or))). + +Lemma tr_sis_alt_def f fi sis: + alt_tr_sis f fi sis = tr_sis f fi sis. +Proof. + unfold tr_sis, str_inputs. destruct fi; simpl; auto. +Qed. + +Definition tr_ris := poly_tr (fun f tbl or => transfer_ris (Regset.elements (pre_inputs f tbl or))). + +Local Hint Resolve transfer_ris_correct ok_transfer_ris: core. +Local Opaque transfer_ris. + +Lemma ok_tr_ris ctx fi ris: + ris_ok ctx (tr_ris (cf ctx) fi ris) + <-> (ris_ok ctx ris). +Proof. + destruct fi; simpl; eauto. +Qed. + +Lemma ok_tr_ris_imp ctx fi ris: + ris_ok ctx (tr_ris (cf ctx) fi ris) + -> (ris_ok ctx ris). +Proof. + rewrite ok_tr_ris; auto. +Qed. + + +Lemma tr_ris_correct ctx fi ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (tr_ris (cf ctx) fi ris) (tr_sis (cf ctx) fi sis). +Proof. + intros REF. rewrite <- tr_sis_alt_def. + destruct fi; simpl; eauto. +Qed. + +Lemma si_ok_tr_down ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis. +Admitted. + +Lemma si_ok_op_down ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis. +Admitted. + +Lemma si_ok_trap_down ctx chunk addr args dest sis: si_ok ctx (sexec_load TRAP chunk addr args dest sis) -> si_ok ctx sis. +Admitted. + +Lemma si_ok_store_down ctx chunk addr args src sis: si_ok ctx (sexec_store chunk addr args src sis) -> si_ok ctx sis. +Admitted. + +(* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *) +Local Hint Resolve si_ok_tr_down si_ok_op_down si_ok_trap_down si_ok_store_down: core. + +Lemma sexec_rec_down ctx ib: + forall k + (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) + sis lsis sfv + (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv)) + (OK: si_ok ctx lsis) + ,si_ok ctx sis. +Proof. + induction ib; simpl; try (autodestruct; simpl). + 1-6: try_simplify_someHyps. + - intros. eapply IHib1. 2-3: eauto. + eapply IHib2; eauto. + - intros k CONT sis lsis sfv. + do 2 autodestruct. + + intros; eapply IHib1; eauto. + + intros; eapply IHib2; eauto. +Qed. + + +(** RAFFINEMENT EXEC SYMBOLIQUE **) + +Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := + match ib with + | BF fin _ => Rfinal (tr_ris f fin ris) (sexec_final_sfv fin ris) + (* basic instructions *) + | Bnop _ => k ris + | Bop op args res _ => k (rexec_op op args res ris) + | Bload TRAP chunk addr args dst _ => k (rexec_load TRAP chunk addr args dst ris) + | Bload NOTRAP chunk addr args dst _ => Rabort + | Bstore chunk addr args src _ => k (rexec_store chunk addr args src ris) + (* composed instructions *) + | Bseq ib1 ib2 => + rexec_rec f ib1 ris (fun ris2 => rexec_rec f ib2 ris2 k) + | Bcond cond args ifso ifnot _ => + let args := list_sval_inj (List.map ris args) in + let ifso := rexec_rec f ifso ris k in + let ifnot := rexec_rec f ifnot ris k in + Rcond cond args ifso ifnot + end + . + +Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort). + + +Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ok_tr_ris_imp + rexec_op_correct rexec_load_correct rexec_store_correct: core. + +Local Hint Constructors rst_refines: core. + +Lemma rexec_rec_correct1 ctx ib: + forall rk k + (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) + (CONT: forall ris sis lsis sfv st, ris_refines ctx ris sis -> k sis = st -> get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> rst_refines ctx (rk ris) (k sis)) + ris sis lsis sfv st + (REF: ris_refines ctx ris sis) + (EXEC: sexec_rec (cf ctx) ib sis k = st) + (SOUT: get_soutcome ctx st = Some (sout lsis sfv)) + (OK: si_ok ctx lsis) + , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st. +Proof. + induction ib; simpl; try (intros; subst; eauto; fail). + - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. + - (* seq *) + intros; subst. + eapply IHib1. 3-6: eauto. + + simpl. eapply sexec_rec_down; eauto. + + intros; subst. eapply IHib2; eauto. + - (* cond *) + intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst. + assert (rOK: ris_ok ctx ris). { + erewrite <- OK_EQUIV. 2: eauto. + eapply sexec_rec_down with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. + } + generalize OUT; clear OUT; simpl. + autodestruct. + intros COND; generalize COND. + erewrite <- seval_condition_refpreserv; eauto. + econstructor; try_simplify_someHyps. +Qed. + +Lemma rexec_correct1 ctx ib sis sfv: + get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) -> + (si_ok ctx sis) -> + rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib). +Proof. + unfold sexec; intros; eapply rexec_rec_correct1; eauto; simpl; congruence. +Qed. + + +(** COPIER-COLLER ... Y a-t-il moyen de l'eviter ? **) + +Lemma ris_ok_tr_down ctx fi ris: ris_ok ctx (tr_ris (cf ctx) fi ris) -> ris_ok ctx ris. +Admitted. + +Lemma ris_ok_op_down ctx op args dest ris: ris_ok ctx (rexec_op op args dest ris) -> ris_ok ctx ris. +Admitted. + +Lemma ris_ok_trap_down ctx chunk addr args dest ris: ris_ok ctx (rexec_load TRAP chunk addr args dest ris) -> ris_ok ctx ris. +Admitted. + +Lemma ris_ok_store_down ctx chunk addr args src ris: ris_ok ctx (rexec_store chunk addr args src ris) -> ris_ok ctx ris. +Admitted. + +(* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *) +Local Hint Resolve ris_ok_tr_down ris_ok_op_down ris_ok_trap_down ris_ok_store_down: core. + +Lemma rexec_rec_down ctx ib: + forall k + (CONT: forall ris lris rfv, get_routcome ctx (k ris) = Some (rout lris rfv) -> ris_ok ctx lris -> ris_ok ctx ris) + ris lris rfv + (ROUT: get_routcome ctx (rexec_rec (cf ctx) ib ris k) = Some (rout lris rfv)) + (OK: ris_ok ctx lris) + ,ris_ok ctx ris. +Proof. + induction ib; simpl; try (autodestruct; simpl). + 1-6: try_simplify_someHyps. + - intros. eapply IHib1. 2-3: eauto. + eapply IHib2; eauto. + - intros k CONT sis lsis sfv. + do 2 autodestruct. + + intros; eapply IHib1; eauto. + + intros; eapply IHib2; eauto. +Qed. + +Lemma rexec_rec_correct2 ctx ib: + forall rk k + (CONTh: forall ris lris rfv, get_routcome ctx (rk ris) = Some (rout lris rfv) -> ris_ok ctx lris -> ris_ok ctx ris) + (CONT: forall ris sis lris rfv st, ris_refines ctx ris sis -> rk ris = st -> get_routcome ctx (rk ris) = Some (rout lris rfv) -> ris_ok ctx lris -> rst_refines ctx (rk ris) (k sis)) + ris sis lris rfv st + (REF: ris_refines ctx ris sis) + (EXEC: rexec_rec (cf ctx) ib ris rk = st) + (SOUT: get_routcome ctx st = Some (rout lris rfv)) + (OK: ris_ok ctx lris) + , rst_refines ctx st (sexec_rec (cf ctx) ib sis k). +Proof. + induction ib; simpl; try (intros; subst; eauto; fail). + - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. + - (* seq *) + intros; subst. + eapply IHib1. 3-6: eauto. + + simpl. eapply rexec_rec_down; eauto. + + intros; subst. eapply IHib2; eauto. + - (* cond *) + intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst. + assert (OK0: ris_ok ctx ris). { + eapply rexec_rec_down with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. + } + generalize OUT; clear OUT; simpl. + autodestruct. + intros COND; generalize COND. + erewrite seval_condition_refpreserv; eauto. + econstructor; try_simplify_someHyps. +Qed. + +Lemma rexec_correct2 ctx ib ris rfv: + get_routcome ctx (rexec (cf ctx) ib) = Some (rout ris rfv) -> + (ris_ok ctx ris) -> + rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib). +Proof. + unfold rexec; intros; eapply rexec_rec_correct2; eauto; simpl; congruence. +Qed. + +Theorem rexec_simu_correct f1 f2 ib1 ib2: + rst_simu (rexec f1 ib1) (rexec f2 ib2) -> + symbolic_simu f1 f2 ib1 ib2. +Proof. + intros SIMU ctx. + eapply rst_simu_correct; eauto. + + intros; eapply rexec_correct1; eauto. + + intros; eapply rexec_correct2; eauto. +Qed. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v new file mode 100644 index 00000000..5a94b235 --- /dev/null +++ b/scheduling/BTL_SEtheory.v @@ -0,0 +1,1311 @@ +(** A theory of symbolic simulation (i.e. simulation of symbolic executions) on BTL blocks. + +NB: an efficient implementation with hash-consing will be defined in another file (some day) + +The main theorem of this file is [symbolic_simu_correct] stating +that the abstract definition of symbolic simulation of two BTL blocks +implies the simulation for BTL.fsem block-steps. + + +*) + +Require Import Coqlib Maps Floats. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL BTL OptionMonad. + +Record iblock_exec_context := Bctx { + cge: BTL.genv; + (* cstk: list stackframe; *) (* having the stack here does seem not a good idea *) + cf: function; + csp: val; + crs0: regset; + cm0: mem +}. + +(** * Syntax and semantics of symbolic values *) + +(* TODO: introduire les hash-code directement ici - avec les "fake" smart constructors qui mettent un unknown_hid ? *) + +(* symbolic value *) +Inductive sval := + | Sundef + | Sinput (r: reg) + | Sop (op:operation) (lsv: list_sval) + | 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 + | Sundef => Some Vundef + | Sinput r => Some ((crs0 ctx)#r) + | Sop op l => + SOME args <- eval_list_sval ctx l IN + eval_operation (cge ctx) (csp ctx) op args (cm0 ctx) + | 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 valid_pointer_preserv ctx sm: + forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs. +Proof. + induction sm; simpl; intros; try_simplify_someHyps; auto. + repeat autodestruct; intros; erewrite IHsm by reflexivity. + eapply Mem.storev_preserv_valid; eauto. +Qed. +Local Hint Resolve valid_pointer_preserv: core. + +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): option bool := + SOME args <- eval_list_sval ctx lsv IN + eval_condition cond args (cm0 ctx). + + +(** * Auxiliary definitions on Builtins *) +(* TODO: clean this. Some generic 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: generic 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 eval_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 <- eval_builtin_sval ctx sv1 IN + SOME v2 <- eval_builtin_sval ctx sv2 IN + Some (BA_splitlong v1 v2) + | BA_addptr sv1 sv2 => + SOME v1 <- eval_builtin_sval ctx sv1 IN + SOME v2 <- eval_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 <- eval_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 eval_builtin_sval_arg ctx bs: + forall ba m v, + eval_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 (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_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 (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_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, + eval_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 eval_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 (eval_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 eval_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 eval_builtin_sval_correct ctx m: forall bs1 v bs2, + seval_builtin_arg ctx m bs1 v -> + (eval_builtin_sval ctx bs1) = (eval_builtin_sval ctx bs2) -> + seval_builtin_arg ctx m bs2 v. +Proof. + intros. exploit seval_builtin_arg_sval; eauto. + intros (ba & X1 & X2). + eapply eval_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 eval_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) + | 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 +. + +Import ListNotations. +Local Open Scope list_scope. + +Inductive sem_sfval ctx stk: sfval -> regset -> mem -> trace -> state -> Prop := + | exec_Sgoto pc rs m: + sem_sfval ctx stk (Sgoto pc) rs m E0 (State stk (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] None rs) m) + | exec_Sreturn pstk osv rs m m' v: + (csp ctx) = (Vptr pstk Ptrofs.zero) -> + Mem.free m pstk 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 stk (Sreturn osv) rs m + E0 (Returnstate stk 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 stk (Scall sig svos lsv res pc) rs m + E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] (Some res) rs)::stk) fd args m) + | exec_Stailcall pstk rs m sig svos args fd m' lsv: + sfind_function ctx svos = Some fd -> + funsig fd = sig -> + (csp ctx) = Vptr pstk Ptrofs.zero -> + Mem.free m pstk 0 (cf ctx).(fn_stacksize) = Some m' -> + eval_list_sval ctx lsv = Some args -> + sem_sfval ctx stk (Stailcall sig svos lsv) rs m + E0 (Callstate stk 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 stk (Sbuiltin ef sargs res pc) rs m + t (State stk (cf ctx) (csp ctx) pc (regmap_setres res vres (tr_inputs (cf ctx) [pc] (reg_builtin_res res) 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 stk (Sjumptable sv tbl) rs m + E0 (State stk (cf ctx) (csp ctx) pc' (tr_inputs ctx.(cf) tbl None rs) m) +. + +(* 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 (sis: sistate) (rs: regset) (m: mem): Prop := + sis.(si_pre) ctx + /\ eval_smem ctx sis.(si_smem) = Some m + /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r). + +(** * Symbolic execution of final step *) +Definition sexec_final_sfv (i: final) (sreg: reg -> sval): sfval := + match i with + | Bgoto pc => Sgoto pc + | Bcall sig ros args res pc => + let svos := sum_left_map sreg ros in + let sargs := list_sval_inj (List.map sreg args) in + Scall sig svos sargs res pc + | Btailcall sig ros args => + let svos := sum_left_map sreg ros in + let sargs := list_sval_inj (List.map sreg args) in + Stailcall sig svos sargs + | Bbuiltin ef args res pc => + let sargs := List.map (builtin_arg_map sreg) args in + Sbuiltin ef sargs res pc + | Breturn or => + let sor := SOME r <- or IN Some (sreg r) in + Sreturn sor + | Bjumptable reg tbl => + let sv := sreg reg in + Sjumptable sv tbl + end. + +Local Hint Constructors sem_sfval: core. + +Lemma sexec_final_sfv_correct ctx stk i sis t rs m s: + sem_sistate ctx sis rs m -> + final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs m i t s -> + sem_sfval ctx stk (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_sfv_exact ctx stk i sis t rs m s: + sem_sistate ctx sis rs m -> + sem_sfval ctx stk (sexec_final_sfv i sis) rs m t s + -> final_step tr_inputs (cge ctx) stk (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. + +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; erewrite op_valid_pointer_eq; eauto. + - 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)) = eval_condition cond rs ## args m. +Proof. + destruct SIS as (PRE&MEM®); unfold seval_condition; simpl. + erewrite eval_list_sval_inj; simpl; auto. + eapply cond_valid_pointer_eq; eauto. +Qed. + +(** * Compute sistate associated to final values *) +Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval := + match inputs with + | nil => fun r => Sundef + | r1::l => fun r => if Pos.eq_dec r1 r then sreg r1 else transfer_sreg l sreg r + end. + +Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (pre_inputs f tbl or)). + +Lemma str_inputs_correct ctx sis rs tbl or r: + (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) -> + eval_sval ctx (str_inputs (cf ctx) tbl or (si_sreg sis) r) = Some (tr_inputs (cf ctx) tbl or rs) # r. +Proof. + intros H. + unfold str_inputs, tr_inputs, transfer_regs. + induction (Regset.elements _) as [|x l]; simpl. + + rewrite Regmap.gi; auto. + + autodestruct; intros; subst. + * rewrite Regmap.gss; auto. + * rewrite Regmap.gso; eauto. +Qed. + +Local Hint Resolve str_inputs_correct: core. + +Definition tr_sis f (fi: final) (sis: sistate) := + {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None); + si_sreg := poly_tr str_inputs f fi sis.(si_sreg); + si_smem := sis.(si_smem) |}. + +Lemma tr_sis_regs_correct_aux ctx fin sis rs m: + sem_sistate ctx sis rs m -> + (forall r, eval_sval ctx (tr_sis (cf ctx) fin sis r) = Some (tr_regs (cf ctx) fin rs) # r). +Proof. + Local Opaque str_inputs. + simpl. destruct 1 as (_ & _ & REG). + destruct fin; simpl; eauto. +Qed. + +Lemma tr_sis_regs_correct ctx fin sis rs m: + sem_sistate ctx sis rs m -> + sem_sistate ctx (tr_sis (cf ctx) fin sis) (tr_regs (cf ctx) fin rs) m. +Proof. + intros H. + generalize (tr_sis_regs_correct_aux _ fin _ _ _ H). + destruct H as (PRE & MEM & REG). + econstructor; simpl; intuition eauto || congruence. +Qed. + +Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f (sfv: sfval): A := + match sfv with + | Sgoto pc => tr f [pc] None + | Scall _ _ _ res pc => tr f [pc] (Some res) + | Stailcall _ _ args => tr f [] None + | Sbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res) + | Sreturn _ => tr f [] None + | Sjumptable _ tbl => tr f tbl None + end. + +Definition str_regs: function -> sfval -> regset -> regset := + poly_str tr_inputs. + +Lemma str_tr_regs_equiv f fin sis: + str_regs f (sexec_final_sfv fin sis) = tr_regs f fin. +Proof. + destruct fin; simpl; auto. +Qed. + +(** * symbolic execution of blocks *) + +(* symbolic state *) +Inductive sstate := + | Sfinal (sis: sistate) (sfv: sfval) + | Scond (cond: condition) (args: list_sval) (ifso ifnot: sstate) + | Sabort + . + +(* outcome of a symbolic execution path *) +Record soutcome := sout { + _sis: sistate; + _sfv: sfval; +}. + +Fixpoint get_soutcome ctx (st:sstate): option soutcome := + match st with + | Sfinal sis sfv => Some (sout sis sfv) + | Scond cond args ifso ifnot => + SOME b <- seval_condition ctx cond args IN + get_soutcome ctx (if b then ifso else ifnot) + | Sabort => None + end. + +(* transition (t,s) produced by a sstate in initial context ctx *) +Inductive sem_sstate ctx stk t s: sstate -> Prop := + | sem_Sfinal sis sfv rs m + (SIS: sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m) + (SFV: sem_sfval ctx stk sfv rs m t s) + : sem_sstate ctx stk t s (Sfinal sis sfv) + | sem_Scond b cond args ifso ifnot + (SEVAL: seval_condition ctx cond args = Some b) + (SELECT: sem_sstate ctx stk t s (if b then ifso else ifnot)) + : sem_sstate ctx stk t s (Scond cond args ifso ifnot) + (* NB: Sabort: fails to produce a transition *) + . + +Lemma sem_sstate_run ctx stk st t s: + sem_sstate ctx stk t s st -> + exists sis sfv rs m, + get_soutcome ctx st = Some (sout sis sfv) + /\ sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m + /\ sem_sfval ctx stk sfv rs m t s + . +Proof. + induction 1; simpl; try_simplify_someHyps; do 4 eexists; intuition eauto. +Qed. + +Local Hint Resolve sem_Sfinal: core. + +Lemma run_sem_sstate ctx st sis sfv: + get_soutcome ctx st = Some (sout sis sfv) -> + forall rs m stk s t, + sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m -> + sem_sfval ctx stk sfv rs m t s -> + sem_sstate ctx stk t s st + . +Proof. + induction st; simpl; try_simplify_someHyps. + autodestruct; intros; econstructor; eauto. + autodestruct; eauto. +Qed. + + +(** * 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 f ib sis (k: sistate -> sstate): sstate := + match ib with + | BF fin _ => Sfinal (tr_sis f fin 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 f ib1 sis (fun sis2 => sexec_rec f ib2 sis2 k) + | Bcond cond args ifso ifnot _ => + let args := list_sval_inj (List.map sis.(si_sreg) args) in + let ifso := sexec_rec f ifso sis k in + let ifnot := sexec_rec f ifnot sis k in + Scond cond args ifso ifnot + end + . + +Definition sexec f ib := sexec_rec f ib sis_init (fun _ => Sabort). + +Local Hint Constructors sem_sstate: core. +Local Hint Resolve sexec_op_correct sexec_final_sfv_correct tr_sis_regs_correct_aux tr_sis_regs_correct + sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core. + +Lemma sexec_rec_correct ctx stk 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 stk t s (k sis') + | Some fin => final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs1 m1 fin t s + end), + sem_sstate ctx stk t s (sexec_rec (cf ctx) ib sis k). +Proof. + induction ISTEP; simpl; try autodestruct; eauto. + (* final value *) + intros; econstructor; eauto. + rewrite str_tr_regs_equiv; eauto. + (* condition *) + all: intros; + eapply sem_Scond; eauto; [ + erewrite seval_condition_eq; eauto | + replace (if b then sexec_rec (cf ctx) ifso sis k else sexec_rec (cf ctx) ifnot sis k) with (sexec_rec (cf ctx) (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 stk ib t s: + iblock_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s -> + sem_sstate ctx stk t s (sexec (cf ctx) ib). +Proof. + destruct 1 as (rs' & m' & fin & ISTEP & FSTEP). + eapply sexec_rec_correct; simpl; eauto. +Qed. + +(* Remark that we want 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_tr_sis_determ ctx sis rs1 m1 fi rs2 m2: + sem_sistate ctx sis rs1 m1 -> + sem_sistate ctx (tr_sis (cf ctx) fi sis) rs2 m2 -> + (forall r, rs2#r = (tr_regs (cf ctx) fi rs1)#r) + /\ m1 = m2. +Proof. + intros H1 H2. + lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto. + intros X. + destruct H1 as (_&MEM1®1). + destruct H2 as (_&MEM2®2); simpl in *. + intuition try congruence. + cut (Some rs2 # r = Some (tr_regs (cf ctx) fi rs1)#r). + { congruence. } + rewrite <- REG2, X. auto. +Qed. + +Local Hint Constructors equiv_stackframe list_forall2: core. +Local Hint Resolve regmap_setres_eq equiv_stack_refl equiv_stack_refl: core. + +Lemma sem_sfval_equiv rs1 rs2 ctx stk sfv m t s: + sem_sfval ctx stk sfv rs1 m t s -> + (forall r, (str_regs (cf ctx) sfv rs1)#r = (str_regs (cf ctx) sfv rs2)#r) -> + exists s', sem_sfval ctx stk sfv rs2 m t s' /\ equiv_state s s'. +Proof. + unfold str_regs. + destruct 1; simpl in *; intros; subst; eexists; split; econstructor; eauto; try congruence. +Qed. + +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 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. + +Lemma sem_sistate_tr_sis_exclude_abort ctx sis fi rs m: + sem_sistate ctx (tr_sis (cf ctx) fi sis) rs m -> + abort_sistate ctx sis -> + False. +Proof. + intros ((PRE1 & PRE2) & MEM & REG); simpl in *. + intros [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; try congruence. +Qed. + +Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort + sexec_store_preserves_abort sem_sistate_tr_sis_exclude_abort: core. + +Lemma sexec_exclude_abort ctx stk ib t s1: forall sis k + (SEXEC: sem_sstate ctx stk t s1 (sexec_rec (cf ctx) ib sis k)) + (CONT: forall sis', sem_sstate ctx stk 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. + intros; erewrite op_valid_pointer_eq; eauto. +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 sexec_final_sfv_exact: core. + +Lemma sexec_rec_exact ctx stk ib t s1: forall sis k + (SEXEC: sem_sstate ctx stk t s1 (sexec_rec (cf ctx) ib sis k)) + rs m + (SIS: sem_sistate ctx sis rs m) + (CONT: forall sis', sem_sstate ctx stk 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 tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2 + | Some (out rs' m' None) => exists sis', (sem_sstate ctx stk 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_tr_sis_determ ctx sis rs m fi); eauto. + intros (REG&MEM); subst. + exploit (sem_sfval_equiv rs0 rs); eauto. + * intros; rewrite REG, str_tr_regs_equiv; auto. + * intros (s2 & EQUIV & SFV'); 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 stk ib t s1: + sem_sstate ctx stk t s1 (sexec (cf ctx) ib) -> + exists s2, iblock_step tr_inputs (cge ctx) stk (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. + +(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) + +Record simu_proof_context {f1 f2: BTL.function} := Sctx { + sge1: BTL.genv; + sge2: BTL.genv; + sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s; + ssp: val; + srs0: regset; + sm0: mem +}. +Arguments simu_proof_context: clear implicits. + +Definition bctx1 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx2 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0). + +(* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract + the [match_states] of BTL_Schedulerproof. + + Indeed, the [match_states] involves [match_function] in [match_stackframe]. + And, here, we aim to define a notion of simulation for defining [match_function]. + + A syntactic definition of the simulation on [sfval] avoids the circularity issue. + +*) + +Inductive optsv_simu {f1 f2: function} (ctx: simu_proof_context f1 f2): (option sval) -> (option sval) -> Prop := + | Ssome_simu sv1 sv2 + (SIMU:eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2) + :optsv_simu ctx (Some sv1) (Some sv2) + | Snone_simu: optsv_simu ctx None None + . + +Inductive svident_simu {f1 f2: function} (ctx: simu_proof_context f1 f2): (sval + ident) -> (sval + ident) -> Prop := + | Sleft_simu sv1 sv2 + (SIMU:eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2) + :svident_simu ctx (inl sv1) (inl sv2) + | Sright_simu id1 id2 + (IDSIMU: id1 = id2) + :svident_simu ctx (inr id1) (inr id2) + . + +Definition bargs_simu {f1 f2: function} (ctx: simu_proof_context f1 f2) (args1 args2: list (builtin_arg sval)): Prop := + eval_list_builtin_sval (bctx1 ctx) args1 = eval_list_builtin_sval (bctx2 ctx) args2. + +Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Prop := + | Sgoto_simu pc: sfv_simu ctx (Sgoto pc) (Sgoto pc) + | Scall_simu sig ros1 ros2 args1 args2 r pc + (SVID: svident_simu ctx ros1 ros2) + (ARGS:eval_list_sval (bctx1 ctx) args1 = eval_list_sval (bctx2 ctx) args2) + :sfv_simu ctx (Scall sig ros1 args1 r pc) (Scall sig ros2 args2 r pc) + | Stailcall_simu sig ros1 ros2 args1 args2 + (SVID: svident_simu ctx ros1 ros2) + (ARGS:eval_list_sval (bctx1 ctx) args1 = eval_list_sval (bctx2 ctx) args2) + :sfv_simu ctx (Stailcall sig ros1 args1) (Stailcall sig ros2 args2) + | Sbuiltin_simu ef lba1 lba2 br pc + (BARGS: bargs_simu ctx lba1 lba2) + :sfv_simu ctx (Sbuiltin ef lba1 br pc) (Sbuiltin ef lba2 br pc) + | Sjumptable_simu sv1 sv2 lpc + (VAL: eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2) + :sfv_simu ctx (Sjumptable sv1 lpc) (Sjumptable sv2 lpc) + | simu_Sreturn osv1 osv2 + (OPT:optsv_simu ctx osv1 osv2) + :sfv_simu ctx (Sreturn osv1) (Sreturn osv2) +. + +Definition sistate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (sis1 sis2:sistate): Prop := + forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sem_sistate (bctx2 ctx) sis2 rs m. + + +Record si_ok ctx (sis: sistate): Prop := { + OK_PRE: (sis.(si_pre) ctx); + OK_SMEM: eval_smem ctx sis.(si_smem) <> None; + OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None +}. + +Lemma sem_si_ok ctx sis rs m: + sem_sistate ctx sis rs m -> si_ok ctx sis. +Proof. + unfold sem_sistate; + econstructor; + intuition congruence. +Qed. + + +Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): Prop := + forall sis1 sfv1, get_soutcome (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> si_ok (bctx1 ctx) sis1 -> + exists sis2 sfv2, get_soutcome (bctx2 ctx) st2 = Some (sout sis2 sfv2) + /\ sistate_simu ctx sis1 sis2 + /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sfv_simu ctx sfv1 sfv2) + . + +Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2). + +(* REM. L'approche suivie initialement ne marche pas !!! +*) +(* +Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2: sstate) := + forall t s1, sem_sstate (bctx1 ctx) t s1 st1 -> + exists s2, sem_sstate (bctx2 ctx) t s2 st2 /\ equiv_state s1 s2. + +Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2). + +Theorem symbolic_simu_correct f1 f2 ib1 ib2: + symbolic_simu f1 f2 ib1 ib2 -> + forall (ctx: simu_proof_context f1 f2) t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> + exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2. +Proof. + unfold symbolic_simu, sstate_simu. + intros SIMU ctx t s1 STEP1. + exploit (sexec_correct (bctx1 ctx)); simpl; eauto. + intros; exploit SIMU; eauto. + intros (s2 & SEM1 & EQ1). + exploit (sexec_exact (bctx2 ctx)); simpl; eauto. + intros (s3 & STEP2 & EQ2). + clear STEP1; eexists; split; eauto. + eapply equiv_state_trans; eauto. +Qed. +*) + +(** * Preservation properties under a [simu_proof_context] *) + +Section SymbValPreserved. + +Variable f1 f2: function. + +Hypothesis ctx: simu_proof_context f1 f2. +Local Hint Resolve sge_match: core. + +Lemma eval_sval_preserved sv: + eval_sval (bctx1 ctx) sv = eval_sval (bctx2 ctx) sv. +Proof. + induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (bctx1 ctx) lsv = eval_list_sval (bctx2 ctx) lsv) + (P1 := fun sm => eval_smem (bctx1 ctx) sm = eval_smem (bctx2 ctx) sm); simpl; auto. + + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto. + erewrite eval_operation_preserved; eauto. + + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. + erewrite eval_addressing_preserved; eauto. + destruct (eval_addressing _ _ _ _); 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 _ _ _ _); auto. + rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto. + rewrite IHsv1; auto. +Qed. + +Lemma list_sval_eval_preserved lsv: + eval_list_sval (bctx1 ctx) lsv = eval_list_sval (bctx2 ctx) 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 (bctx1 ctx) sm = eval_smem (bctx2 ctx) sm. +Proof. + induction sm; simpl; auto. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. + erewrite eval_addressing_preserved; eauto. + destruct (eval_addressing _ _ _ _); auto. + rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto. + rewrite eval_sval_preserved; auto. +Qed. + +Lemma eval_builtin_sval_preserved sv: + eval_builtin_sval (bctx1 ctx) sv = eval_builtin_sval (bctx2 ctx) sv. +Proof. + induction sv; simpl; auto. + all: try (erewrite eval_sval_preserved by eauto); trivial. + all: erewrite IHsv1 by eauto; erewrite IHsv2 by eauto; reflexivity. +Qed. + +Lemma eval_list_builtin_sval_preserved lsv: + eval_list_builtin_sval (bctx1 ctx) lsv = eval_list_builtin_sval (bctx2 ctx) lsv. +Proof. + induction lsv; simpl; auto. + erewrite eval_builtin_sval_preserved by eauto. + erewrite IHlsv by eauto. + reflexivity. +Qed. + +Lemma seval_condition_preserved cond lsv: + seval_condition (bctx1 ctx) cond lsv = seval_condition (bctx2 ctx) cond lsv. +Proof. + unfold seval_condition. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. +Qed. + +(* TODO: useless ? +Lemma get_soutcome_preserved sis: + get_soutcome (bctx1 ctx) sis = get_soutcome (bctx2 ctx) sis. +Proof. + induction sis; simpl; eauto. + erewrite seval_condition_preserved. + repeat (autodestruct; auto). +Qed. +*) + +(* additional preservation properties under this additional hypothesis *) +Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx). + +Lemma senv_find_symbol_preserved id: + Senv.find_symbol (sge1 ctx) id = Senv.find_symbol (sge2 ctx) id. +Proof. + destruct senv_preserved_BTL as (A & B & C). congruence. +Qed. + +Lemma senv_symbol_address_preserved id ofs: + Senv.symbol_address (sge1 ctx) id ofs = Senv.symbol_address (sge2 ctx) id ofs. +Proof. + unfold Senv.symbol_address. rewrite senv_find_symbol_preserved. + reflexivity. +Qed. + +Lemma seval_builtin_arg_preserved m: forall bs varg, + seval_builtin_arg (bctx1 ctx) m bs varg -> + seval_builtin_arg (bctx2 ctx) 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 (bctx1 ctx) m lbs vargs -> + seval_builtin_args (bctx2 ctx) m lbs vargs. +Proof. + induction 1; constructor; eauto. + eapply seval_builtin_arg_preserved; auto. +Qed. + +End SymbValPreserved. + diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v new file mode 100644 index 00000000..ec83b3c1 --- /dev/null +++ b/scheduling/BTL_Scheduler.v @@ -0,0 +1,70 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad BTL. + +Require Import Errors Linking BTL_SEtheory. + +(** External oracle *) +Axiom scheduler: BTL.function -> BTL.code. + +Extract Constant scheduler => "BTLScheduleraux.btl_scheduler". + +(* TODO: could be useful ? +Definition equiv_input_regs (f1 f2: BTL.function): Prop := + (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) + /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)). + +Lemma equiv_input_regs_union f1 f2: + equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl. +Proof. + intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto. + generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS. + do 2 autodestruct; intuition; try_simplify_someHyps. + intros; exploit EQS; eauto; clear EQS. congruence. +Qed. + +Lemma equiv_input_regs_pre f1 f2 tbl or: + equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or. +Proof. + intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto. +Qed. +*) + + +(* a specification of the verification to do on each function *) +Record match_function (f1 f2: BTL.function): Prop := { + preserv_fnsig: fn_sig f1 = fn_sig f2; + preserv_fnparams: fn_params f1 = fn_params f2; + preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2; + preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2; + (* preserv_inputs: equiv_input_regs f1 f2; TODO: a-t-on besoin de ça ? *) + symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 -> + exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2); +}. + +Local Open Scope error_monad_scope. + +Definition check_symbolic_simu (f tf: BTL.function): res unit := OK tt. (* TODO: fixme *) + +(* TODO: a-t-on besoin de ça ? +Lemma check_symbolic_simu_input_equiv x f1 f2: + check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2. +Admitted. +*) + +Lemma check_symbolic_simu_correct x f1 f2: + check_symbolic_simu f1 f2 = OK x -> + forall pc ib1, (fn_code f1)!pc = Some ib1 -> + exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2). +Admitted. + +Definition transf_function (f: BTL.function) := + let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f) in + do _ <- check_symbolic_simu f tf; + OK tf. + +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef (fun f => transf_function f) f. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v new file mode 100644 index 00000000..c8c2a76f --- /dev/null +++ b/scheduling/BTL_Schedulerproof.v @@ -0,0 +1,31 @@ +Require Import AST Linking Values Maps Globalenvs Smallstep Registers. +Require Import Coqlib Maps Events Errors Op. +Require Import RTL BTL BTL_SEtheory. +Require Import BTL_Scheduler. + +Definition match_prog (p tp: program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. + +Section PRESERVATION. + +Variable prog: program. +Variable tprog: program. + +Hypothesis TRANSL: match_prog prog tprog. + +Let pge := Genv.globalenv prog. +Let tpge := Genv.globalenv tprog. + +Theorem transf_program_correct: + forward_simulation (fsem prog) (fsem tprog). +Proof. + eapply forward_simulation_step with equiv_state. (* lock-step with respect to equiv_states *) +Admitted. + +End PRESERVATION. diff --git a/scheduling/BTLcommonaux.ml b/scheduling/BTLcommonaux.ml new file mode 100644 index 00000000..4605d613 --- /dev/null +++ b/scheduling/BTLcommonaux.ml @@ -0,0 +1,70 @@ +open Maps +open BTL +open BTLtypes +open RTLcommonaux + +let undef_node = -1 + +let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond; visited = false } + +let def_iinfo () = { inumb = undef_node; pcond = None; visited = false } + +let mk_binfo _bnumb = { bnumb = _bnumb; visited = false } + +let reset_visited_ibf btl = + PTree.map + (fun n ibf -> + ibf.binfo.visited <- false; + ibf) + btl + +let reset_visited_ib btl = + List.iter + (fun (n, ibf) -> + let ib = ibf.entry in + let rec reset_visited_ib_rec ib = + match ib with + | Bseq (ib1, ib2) -> + reset_visited_ib_rec ib1; + reset_visited_ib_rec ib2 + | Bcond (_, _, ib1, ib2, iinfo) -> + reset_visited_ib_rec ib1; + reset_visited_ib_rec ib2; + iinfo.visited <- false + | Bnop (Some iinfo) + | Bop (_, _, _, iinfo) + | Bload (_, _, _, _, _, iinfo) + | Bstore (_, _, _, _, iinfo) + | BF (_, iinfo) -> + iinfo.visited <- false + | _ -> () + in + reset_visited_ib_rec ib) + (PTree.elements btl); + btl + +let jump_visit = function + | Bcond (_, _, _, _, iinfo) + | Bnop (Some iinfo) + | Bop (_, _, _, iinfo) + | Bload (_, _, _, _, _, iinfo) + | Bstore (_, _, _, _, iinfo) + | BF (_, iinfo) -> + if iinfo.visited then true + else ( + iinfo.visited <- true; + false) + | Bseq (_, _) -> false + | Bnop None -> true + +let rec get_inumb_or_next = function + | BF (Bgoto s, _) -> p2i s + | BF (_, iinfo) + | Bnop (Some iinfo) + | Bop (_, _, _, iinfo) + | Bload (_, _, _, _, _, iinfo) + | Bstore (_, _, _, _, iinfo) + | Bcond (_, _, _, _, iinfo) -> + iinfo.inumb + | Bseq (ib1, _) -> get_inumb_or_next ib1 + | _ -> failwith "get_inumb_or_next: Bnop None" diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v new file mode 100644 index 00000000..439ba9cc --- /dev/null +++ b/scheduling/BTLmatchRTL.v @@ -0,0 +1,603 @@ +(** General notions about the bisimulation BTL <-> RTL. + +This bisimulation is proved on the "CFG semantics" of BTL called [cfgsem] defined below, +such that the full state of registers is preserved when exiting blocks. + +*) + +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad Lia. +Require Export BTL. + +(* tid = transfer_identity *) +Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs. + +Definition cfgsem (p: program) := + Semantics (step tid) (initial_state p) final_state (Genv.globalenv p). + +(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation. +*) + + +Lemma tr_inputs_lessdef f rs1 rs2 tbl or r + (REGS: forall r, Val.lessdef rs1#r rs2#r) + :Val.lessdef (tr_inputs f tbl or rs1)#r (tid f tbl or rs2)#r. +Proof. + unfold tid; rewrite tr_inputs_get. + autodestruct. +Qed. + +Local Hint Resolve tr_inputs_lessdef init_regs_lessdef_preserv find_function_lessdef regs_lessdef_regs + lessdef_state_refl: core. +Local Hint Unfold regs_lessdef: core. + +Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 rs1' m1' of ib + (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of): forall + rs2 m2 + (REGS: forall r, Val.lessdef rs1#r rs2#r) + (MEMS: Mem.extends m1 m2), + exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) + /\ (forall r, Val.lessdef rs1'#r rs2'#r) + /\ (Mem.extends m1' m2'). +Proof. + induction ISTEP; simpl; try_simplify_someHyps; intros. + - (* Bop *) + exploit (@eval_operation_lessdef _ _ ge sp op (rs ## args)); eauto. + intros (v1 & EVAL' & LESSDEF). + do 2 eexists; rewrite EVAL'. repeat (split; eauto). + eapply set_reg_lessdef; eauto. + - (* Bload *) + exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto. + intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto. + intros (v3 & LOAD' & LESSDEF'). + do 2 eexists; rewrite EVAL', LOAD'. repeat (split; eauto). + eapply set_reg_lessdef; eauto. + - (* Bstore *) + exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto. + intros (v2 & EVAL' & LESSDEF). exploit Mem.storev_extends; eauto. + intros (v3 & STORE' & LESSDEF'). + do 2 eexists; rewrite EVAL', STORE'. repeat (split; eauto). + - (* Bseq stop *) + exploit IHISTEP; eauto. intros (rs2' & m2' & IBIS & REGS' & MEMS'). + destruct (iblock_istep_run _ _ _ _ _); try congruence. + destruct o, _fin; simpl in *; try congruence. eauto. + - (* Bseq continue *) + exploit IHISTEP1; eauto. + clear ISTEP1 REGS MEMS. + intros (rs3 & m3 & ISTEP3 & REGS3 & MEMS3). + rewrite ISTEP3; simpl. rewrite iblock_istep_run_equiv in ISTEP2. + exploit IHISTEP2; eauto. + - (* Bcond *) + erewrite (@eval_condition_lessdef cond (rs ## args)); eauto. +Qed. + +Local Hint Constructors lessdef_stackframe lessdef_state final_step list_forall2 step: core. + +Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2 + (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1) + (STACKS: list_forall2 lessdef_stackframe stk1 stk2) + (REGS: forall r, Val.lessdef rs1#r rs2#r) + (MEMS: Mem.extends m1 m2) + : exists s2, final_step tid ge stk2 f sp rs2 m2 fin t s2 + /\ lessdef_state s1 s2. +Proof. + destruct FSTEP; try (eexists; split; simpl; econstructor; eauto; fail). + - (* return *) + exploit Mem.free_parallel_extends; eauto. + intros (m2' & FREE & MEMS2). + eexists; split; simpl; econstructor; eauto. + destruct or; simpl; auto. + - (* tailcall *) + exploit Mem.free_parallel_extends; eauto. + intros (m2' & FREE & MEMS2). + eexists; split; simpl; econstructor; eauto. + - (* builtin *) + exploit (eval_builtin_args_lessdef (ge:=ge) (e1:=(fun r => rs1 # r)) (fun r => rs2 # r)); eauto. + intros (vl2' & BARGS & VARGS). + exploit external_call_mem_extends; eauto. + intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). + eexists; split; simpl; econstructor; eauto. + intros; apply set_res_lessdef; eauto. + - (* jumptable *) + eexists; split; simpl; econstructor; eauto. + destruct (REGS arg); try congruence. +Qed. + +Lemma fsem2cfgsem_ibstep_simu ge stk1 stk2 f sp rs1 m1 ib t s1 rs2 m2 + (STEP: iblock_step tr_inputs ge stk1 f sp rs1 m1 ib t s1) + (STACKS : list_forall2 lessdef_stackframe stk1 stk2) + (REGS: forall r, Val.lessdef rs1#r rs2#r) + (MEMS : Mem.extends m1 m2) + : exists s2, iblock_step tid ge stk2 f sp rs2 m2 ib t s2 + /\ lessdef_state s1 s2. +Proof. + destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP). + exploit fsem2cfgsem_ibistep_simu; eauto. + intros (rs2' & m2' & ISTEP2 & REGS2 & MEMS2). + rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP REGS MEMS. + exploit fsem2cfgsem_finalstep_simu; eauto. + intros (s2 & FSTEP2 & LESSDEF). clear FSTEP. + unfold iblock_step; eexists; split; eauto. +Qed. + +Local Hint Constructors step: core. + +Lemma fsem2cfgsem_step_simu ge s1 t s1' s2 + (STEP: step tr_inputs ge s1 t s1') + (REGS: lessdef_state s1 s2) + :exists s2' : state, + step tid ge s2 t s2' /\ + lessdef_state s1' s2'. +Proof. + destruct STEP; inv REGS. + - (* iblock *) + intros; exploit fsem2cfgsem_ibstep_simu; eauto. clear STEP. + intros (s2 & STEP2 & REGS2). + eexists; split; eauto. + - (* internal call *) + exploit (Mem.alloc_extends m m2 0 (fn_stacksize f) stk m' 0 (fn_stacksize f)); eauto. + 1-2: lia. + intros (m2' & ALLOC2 & MEMS2). clear ALLOC MEMS. + eexists; split; econstructor; eauto. + - (* external call *) + exploit external_call_mem_extends; eauto. + intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). clear EXTCALL MEMS. + eexists; split; econstructor; eauto. + - (* return *) + inversion STACKS as [|d1 d2 d3 d4 STF2 STK2]. subst. + inv STF2. + eexists; split; econstructor; eauto. + intros; eapply set_reg_lessdef; eauto. +Qed. + +Theorem fsem2cfgsem prog: + forward_simulation (fsem prog) (cfgsem prog). +Proof. + eapply forward_simulation_step with lessdef_state; simpl; auto. + - destruct 1; intros; eexists; intuition eauto. econstructor; eauto. + - intros s1 s2 r REGS FINAL; destruct FINAL. + inv REGS; inv STACKS; inv REGS0. + econstructor; eauto. + - intros; eapply fsem2cfgsem_step_simu; eauto. +Qed. + +(** * Matching BTL (for cfgsem) and RTL code + +We define a single verifier able to prove a bisimulation between BTL and RTL code. + +Hence, in a sense, our verifier imitates the approach of Duplicate, where [dupmap] maps the BTL nodes to the RTL nodes. + +The [match_function] definition gives a "relational" specification of the verifier... +*) + +Require Import Errors. + +Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop := + | 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 iinfo: + cfg!pc = Some i -> + match_final_inst dupmap fi i -> + match_iblock dupmap cfg isfst pc (BF fi iinfo) None + | mib_nop_on_rtl isfst pc pc' iinfo: + cfg!pc = Some (Inop pc') -> + match_iblock dupmap cfg isfst pc (Bnop (Some iinfo)) (Some pc') + | mib_nop_skip pc: + match_iblock dupmap cfg false pc (Bnop None) (Some pc) + | mib_op isfst pc pc' op lr r iinfo: + cfg!pc = Some (Iop op lr r pc') -> + match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc') + | mib_load isfst pc pc' m a lr r iinfo: + cfg!pc = Some (Iload TRAP m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc') + | mib_store isfst pc pc' m a lr r iinfo: + cfg!pc = Some (Istore m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc') + | mib_exit pc pc' iinfo: + dupmap!pc = (Some pc') -> + match_iblock dupmap cfg false pc' (BF (Bgoto pc) iinfo) 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 + (* here [b2] is dead code ! Our verifier rejects such dead code! + *) +*) + | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i iinfo: + 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 iinfo) opc + . + +Definition match_cfg dupmap (cfg: BTL.code) (cfg':RTL.code): Prop := + forall pc pc', dupmap!pc = Some pc' -> + exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None. + +Record match_function dupmap f f': Prop := { + dupmap_correct: match_cfg dupmap (BTL.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' +}. + +(** * 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 "BTL.verify_is_copy None") + | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "BTL.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 "BTL.verify_is_copy_list: ln' bigger than ln") end + | nil => match ln' with + | n :: ln' => Error (msg "BTL.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 "BTL.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 "BTL.verify_block: different opt reg in Breturn") + | _ => Error (msg "BTL.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 "BTL.verify_block: different r r' in Bcall") + else Error (msg "BTL.verify_block: different lr in Bcall") + else Error (msg "BTL.verify_block: different ri in Bcall") + else Error (msg "BTL.verify_block: different signatures in Bcall") + | _ => Error (msg "BTL.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 "BTL.verify_block: different lr in Btailcall") + else Error (msg "BTL.verify_block: different ri in Btailcall") + else Error (msg "BTL.verify_block: different signatures in Btailcall") + | _ => Error (msg "BTL.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 "BTL.verify_block: different brr in Bbuiltin") + else Error (msg "BTL.verify_block: different lbar in Bbuiltin") + else Error (msg "BTL.verify_block: different ef in Bbuiltin") + | _ => Error (msg "BTL.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 "BTL.verify_block: different r in Bjumptable") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable") + end + end + | Bnop oiinfo => + match oiinfo with + | Some _ => + match cfg!pc with + | Some (Inop pc') => OK (Some pc') + | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop") + end + | None => + if negb isfst then OK (Some pc) + else Error (msg "BTL.verify_block: isfst is true Bnop (on_rtl is false)") + 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 "BTL.verify_block: different r in Bop") + else Error (msg "BTL.verify_block: different lr in Bop") + else Error (msg "BTL.verify_block: different operations in Bop") + | _ => Error (msg "BTL.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 "BTL.verify_block: different r in Bload") + else Error (msg "BTL.verify_block: different lr in Bload") + else Error (msg "BTL.verify_block: different addressing in Bload") + else Error (msg "BTL.verify_block: different mchunk in Bload") + else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload") + | _ => Error (msg "BTL.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 "BTL.verify_block: different r in Bstore") + else Error (msg "BTL.verify_block: different lr in Bstore") + else Error (msg "BTL.verify_block: different addressing in Bstore") + else Error (msg "BTL.verify_block: different mchunk in Bstore") + | _ => Error (msg "BTL.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 "BTL.verify_block: None next pc in Bseq (deadcode)") + end + | Bcond c lr bso bnot _ => + 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 "BTL.verify_block: is_join_opt incorrect for Bcond") + end + else Error (msg "BTL.verify_block: incompatible conditions in Bcond") + else Error (msg "BTL.verify_block: different lr in Bcond") + | _ => Error (msg "BTL.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 oiinfo; simpl in *. + + destruct (cfg!pc) eqn:EQCFG; try discriminate. + destruct i0; inv H. constructor; assumption. + + destruct isfst; try discriminate. 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 "BTL.verify_blocks.end") + end + | _ => Error(msg "BTL.verify_blocks.entry") + end + end. + +Definition verify_cfg dupmap (cfg: code) (cfg':RTL.code): res unit := + verify_blocks dupmap cfg cfg' (PTree.elements dupmap). + +Lemma verify_cfg_correct dupmap cfg cfg' tt: + verify_cfg dupmap cfg cfg' = OK tt -> + match_cfg dupmap cfg cfg'. +Proof. + unfold verify_cfg. + intros X pc pc' H; generalize X; clear X. + exploit PTree.elements_correct; eauto. + generalize tt pc pc' H; clear tt pc pc' H. + generalize (PTree.elements dupmap). + induction l as [|[pc1 pc1']l]; simpl. + - tauto. + - intros pc pc' DUP u H. + unfold bind. + repeat autodestruct. + intros; subst. + destruct H as [H|H]; eauto. + inversion H; subst. + eexists; split; eauto. +Qed. + +Definition verify_function dupmap f f' : res unit := + do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); + verify_cfg dupmap (fn_code f) (RTL.fn_code f'). + +Lemma verify_function_correct dupmap f f' tt: + verify_function dupmap f f' = OK tt -> + fn_sig f = RTL.fn_sig f' -> + fn_params f = RTL.fn_params f' -> + fn_stacksize f = RTL.fn_stacksize f' -> + match_function dupmap f f'. +Proof. + unfold verify_function; intro VERIF. monadInv VERIF. + constructor; eauto. + eapply verify_cfg_correct; eauto. +Qed. + diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md new file mode 100644 index 00000000..9dd21be9 --- /dev/null +++ b/scheduling/BTLroadmap.md @@ -0,0 +1,408 @@ +# 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 main info required from oracles: a "dupmap" mapping block entries (and maybe strategies for controlling path explosion during symbolic execution -- see below). +Moreover, 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... + +Remark that we may port most of the current optimizations from RTL to BTL (even maybe, register allocation). +However, RTL will probably remain useful for "fine-tuned" duplication that crosses block boundaries (e.g. Duplicate module). + +## 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:** 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. + +## 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. le traitement de `pre_output_regs` dans RTLpathScheduler, etc). +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_def". Ça peut rendre le cadre du test de simulation plus +simple et plus général. + +**Idée_Informelle** à côté de la sémantique "à la RTL" pour BTL +[BTLmatch.cfgsem], on définit une sémantique [BTL.fsem], où c'est +juste "l'entrée dans un bloc" qui change de sémantique. Intuitivement, +cette 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 pourrait moralement +commencer par mettre à Vundef tous les registres qui ne sont pas dans l'`input_regs`. + +**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. + +**REM** pour le test d'exécution symbolique, il semble plus adapté de +mettre les Vundef juste à la fin de la transition (précédente) plutôt +qu'au début (de la suivante): c'est d'ailleurs plus proche de la vision SSA. + +En fait, on pourrait faire les deux (dans le détail, ça ne ferait pas +exactement deux fois la même chose: par exemple, quand on sort sur un +call ou un builtin, le résultat du call/builtin n'est jamais dans le +liveout puisqu'il va être écrasé de toute façon pendant la transition, +mais il peut être -- ou pas -- dans le livein de la transition +suivante dans ce même bloc). + +Avoir une initialisation à Vundef en début de bloc permettrait de +faire une analyse des expressions mal initialisées - par exemple à +partir du bloc d'entrée de la fonction. Ça semble complémentaire de +l'analyse de "liveout". Mais utilisable uniquement dans le cadre d'une +combinaison "exécution symbolique"+"value analysis" (donc pas tout de suite). + +Donc, dans un premier temps, la BTL.fsem encode/abstrait la notion de +"liveout" pour le test d'exécution symbolique. Les définitions des +deux sémantiques (symbolique et "functional") se font donc en +simultanée. + +**STATUS** + +1. See [BTL.fsem] +2. fsem -> cfgsem: fait (ou presque). +3. cfgsem -> fsem: a faire (via verif de liveness). + +## "Basic" symbolic execution / symbolic simulation + +We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.fsem. +Dans un premier temps: pas besoin de "less_undef lockstep", on peut se contenter de tester l'égalité des registres de chaque côté: les registres hors liveout seront égaux à Vundef de chaque côté. + +**STATUS** + +- BTL_SEtheory: DONE + - model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.fsem + - high-level specification [sstate_simu] of "symbolic simulation" over iblocks (wrt BTL.fsem). + +**TODO** + +1. Verif du "scheduling" (aka analogue de RTLpathScheduler & RTLSchedulerproof). +2. raffinement intermediaire avant le hash-consing ? ça permettrait de décomposer encore davantage la preuve ? +Y a-t-il un moyen simple de faire le tests d'inclusion des fails potentiels à coût linéaire plutôt que quadratique (contrairement à RTLpath) ? + +## 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. + +**PRELIMINARY IDEAS** + +- En pratique, il faudrait affiner la sémantique symbolique des "jumptable" pour que ça marche bien: avec un "état symbolique interne" par sortie (au lieu d'un état symbolique interne global dans la sémantique actuelle). Ça semble nécessaire pour gérer les invariants de renommage par exemple: en effet, il y a potentiellement un renommage différent pour chaque sortie. +Une solution possible: calquer Bjumptable sur Bcond (c-a-d autoriser les Bjumptable en milieu de blocs). On pourrait étendre la prédiction de branchement par profiling aux jumptables (par exemple, avoir des superblocks avec des jumptables au milieu). Un autre intérêt: simplifier (un peu) le support pour des formes SSA partielles (cf. ci-dessous). Ceci dit, ça compliquerait les choses à plein d'endroits (type Coq [iblock] mutuellement inductif avec [list_iblock] pour avoir les bons principes d'inductions, etc) pour des gains minimes en pratiques ? + +- Est-ce qu'il ne faut pas envisager une combinaison "execution symbolique + value analysis" ? La value analysis pourrait se faire directement sur la sémantique symbolique (donc en sortie de l'exécution symbolique), avec un mécanisme de mémoïsation (pour éviter les calculs redondants dus à la duplication de termes dans l'état symbolique). Intérêts: la value analysis ne se ferait que sur les registres live. Elle serait aussi plus sans doute un peu simple (par exemple inutile d'avoir un "join": on peut se contenter d'un test d'inclusion sur chacun des chemins). + +**EXAMPLE OF STRENGTH REDUCTION** + +On veut passer du code C1: + + init: // inputs: int *t, int n, int s + int i=0; + loop: // inputs: int *t, int n, int s, int i + if (i >= n) goto exit; + s += t[i]; + i += 1; + goto loop; + exit: // inputs: int *t, int s + +au code C2: + + init: // inputs: int *t, int n, int s + int *ti = t; + int *tn = t+n; + loop: // inputs: int *t, int s, int *ti, int *tn + if (ti >= tn) goto exit; + s += *ti; + ti += 4; + goto loop; + exit; // inputs: int *t, int s + +Pour donner la correspondance entre les variables des 2 blocs, pour chaque entrée "pc", on introduit une "fonction" de C1@pc.(inputs) -> C2@pc.(inputs). + +Typiquement, cette fonction est codable comme un map associant une valeur symbolique sur les C1@pc.(inputs) aux variables de C2@pc.(inputs). Exemple: + + init: // map vide (identité) + loop: + ti = t+i + tn = t+n + exit: // map vide (identité) + +Si on note `TRANSFER` cette fonction, alors la vérification par +exécution symbolique que le bloc `ib1` est simulé par `ib2` modulo +`TRANSFER` sur l'entrée `pc` se ramène à montrer `ib1[TRANSFER]` avec +`TRANSFER(pc); ib2` pour la simulation symbolique usuelle. + +Ci-dessus `ib1[TRANSFER]` dit qu'on a appliqué `TRANSFER(pc')` sur chacune des sorties `pc'` de `ib1`. + +**REM** pour que ce soit correct, il faut sans doute vérifier une condition du style `ok(ib1) => ok(ib1[TRANSFER])`... + +## Support of SSA-optimizations + +Minimum feature: extends BTL with "register renamings" at exits. This should enable to represent SSA-forms in BTL IR, more or less like in MLIR. + +Maximum feature: add a basic instruction that performs parallel renaming of registers. If we also support Bjumptable in the middle of a block (see above), this simple feature would suffice to represent a very general notion of "partial SSA forms": since they could appear in the middle of a block, or just before an exit (such a parallel assignment would be forbidden in BTL<->RTL matching). + +## 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..fc58533d --- /dev/null +++ b/scheduling/BTLtoRTL.v @@ -0,0 +1,26 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad BTL. +Require Export BTLmatchRTL. + +Require Import Errors Linking. + +(** External oracle *) +Axiom btl2rtl: BTL.function -> RTL.code * node * (PTree.t node). + +Extract Constant btl2rtl => "BTLtoRTLaux.btl2rtl". + +Local Open Scope error_monad_scope. + +Definition transf_function (f: BTL.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/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml new file mode 100644 index 00000000..ddec991d --- /dev/null +++ b/scheduling/BTLtoRTLaux.ml @@ -0,0 +1,88 @@ +open Maps +open BTL +open RTL +open Camlcoq +open RTLcommonaux +open DebugPrint +open PrintBTL +open BTLcommonaux +open BTLtypes +open BTLRenumber + +let get_inumb iinfo = P.of_int iinfo.inumb + +let get_ib_num ib = P.of_int (get_inumb_or_next ib) + +let translate_function btl entry = + let rtl_code = ref PTree.empty in + let rec translate_btl_block ib k = + debug "Entering translate_btl_block...\n"; + print_btl_inst stderr ib; + let rtli = + match ib with + | Bcond (cond, lr, BF (Bgoto s1, _), Bnop None, iinfo) -> + Some + ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.pcond), + get_inumb iinfo ) + | Bcond (_, _, _, _, _) -> + failwith "translate_function: unsupported Bcond" + | Bseq (ib1, ib2) -> + translate_btl_block ib1 (Some ib2); + translate_btl_block ib2 None; + None + | Bnop (Some iinfo) -> + Some (Inop (get_ib_num (get_some k)), get_inumb iinfo) + | Bnop None -> + failwith + "translate_function: Bnop None can only be in the right child of \ + Bcond" + | Bop (op, lr, rd, iinfo) -> + Some (Iop (op, lr, rd, get_ib_num (get_some k)), get_inumb iinfo) + | Bload (trap, chk, addr, lr, rd, iinfo) -> + Some + ( Iload (trap, chk, addr, lr, rd, get_ib_num (get_some k)), + get_inumb iinfo ) + | Bstore (chk, addr, lr, src, iinfo) -> + Some + ( Istore (chk, addr, lr, src, get_ib_num (get_some k)), + get_inumb iinfo ) + | BF (Bcall (sign, fn, lr, rd, s), iinfo) -> + Some (Icall (sign, fn, lr, rd, s), get_inumb iinfo) + | BF (Btailcall (sign, fn, lr), iinfo) -> + Some (Itailcall (sign, fn, lr), get_inumb iinfo) + | BF (Bbuiltin (ef, lr, rd, s), iinfo) -> + Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo) + | BF (Bjumptable (arg, tbl), iinfo) -> + Some (Ijumptable (arg, tbl), get_inumb iinfo) + | BF (Breturn oreg, iinfo) -> Some (Ireturn oreg, get_inumb iinfo) + | BF (Bgoto s, iinfo) -> None + in + match rtli with + | Some (inst, inumb) -> rtl_code := PTree.set inumb inst !rtl_code + | None -> () + in + List.iter + (fun (n, ibf) -> + ibf.binfo.visited <- true; + let ib = ibf.entry in + translate_btl_block ib None) + (PTree.elements btl); + !rtl_code + +let btl2rtl (f : BTL.coq_function) = + (*debug_flag := true;*) + let btl = f.fn_code in + let entry = f.fn_entrypoint in + let obne, dm = renumber btl entry in + let ordered_btl, new_entry = obne in + let rtl = translate_function ordered_btl new_entry in + debug "Entry %d\n" (p2i new_entry); + debug "BTL Code:\n"; + print_btl_code stderr ordered_btl; + debug "RTL Code: "; + print_code rtl; + debug "Dupmap:\n"; + print_ptree print_pint dm; + debug "\n"; + (*debug_flag := false;*) + ((rtl, new_entry), dm) diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v new file mode 100644 index 00000000..75f67d51 --- /dev/null +++ b/scheduling/BTLtoRTLproof.v @@ -0,0 +1,402 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad. + +Require Import Errors Linking BTLtoRTL. + +Require Import Linking. + + +Inductive match_fundef: BTL.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: BTL.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 (BTL.Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). + +Inductive match_states: BTL.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 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_E0_trans isfst isfst' s0 s1 s2: + cond_star_step (isfst=false) s0 E0 s1 -> + cond_star_step (false=isfst') s1 E0 s2 -> + cond_star_step (isfst=isfst') s0 E0 s2. +Proof. + intros S1 S2. + inversion S1; subst; eauto. + inversion S2; subst; eauto. + eapply css_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) /\ cond_star_step (isfst = false) (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) + | Some fin => + exists isfst' pc1 iinfo, match_iblock dupmap (RTL.fn_code f') isfst' pc1 (BF fin iinfo) 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; eexists; split; econstructor; eauto. + - (* exec_op *) + inv MIB. exists pc'; split; auto; constructor. + 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; constructor. + 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; constructor. + 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 & iinfo & M2 & STEP2). + repeat eexists; eauto. + eapply css_E0_trans; eauto. + + intros (pc2 & EQpc2 & STEP2); inv EQpc2. + eexists; split; auto. + eapply css_E0_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 & iinfo' & 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 css_plus_trans; eauto. + + (* taking ifnot *) + destruct ofin; simpl. + * (* ofin is Some final *) + intros (isfst' & pc1 & iinfo' & 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 css_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 tid 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 tid 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 & iinfo & 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 tid 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_cfg: + forward_simulation (BTLmatchRTL.cfgsem 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. + +Theorem transf_program_correct: + forward_simulation (BTL.fsem prog) (RTL.semantics tprog). +Proof. + eapply compose_forward_simulations. + - eapply fsem2cfgsem. + - eapply transf_program_correct_cfg. +Qed. + +End RTL_SIMULATES_BTL. diff --git a/scheduling/BTLtypes.ml b/scheduling/BTLtypes.ml new file mode 100644 index 00000000..3972fd6b --- /dev/null +++ b/scheduling/BTLtypes.ml @@ -0,0 +1,7 @@ +type inst_info = { + mutable inumb : int; + mutable pcond : bool option; + mutable visited : bool; +} + +type block_info = { mutable bnumb : int; mutable visited : bool } diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml new file mode 100644 index 00000000..52178064 --- /dev/null +++ b/scheduling/PrintBTL.ml @@ -0,0 +1,131 @@ +open Printf +open Camlcoq +open Datatypes +open Maps +open BTL +open PrintAST +open DebugPrint +open BTLtypes + +(* Printing of BTL code *) + +let reg pp r = fprintf pp "x%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [ r ] -> reg pp r + | r1 :: rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_succ pp s = fprintf pp "\tsucc %d\n" (P.to_int s) + +let print_pref pp pref = fprintf pp "%s" pref + +let rec print_iblock pp is_rec pref ib = + match ib with + | Bnop None -> + print_pref pp pref; + fprintf pp "??: Bnop None\n" + | Bnop (Some iinfo) -> + print_pref pp pref; + fprintf pp "%d: Bnop\n" iinfo.inumb + | Bop (op, args, res, iinfo) -> + print_pref pp pref; + fprintf pp "%d: Bop: %a = %a\n" iinfo.inumb reg res + (PrintOp.print_operation reg) + (op, args) + | Bload (trap, chunk, addr, args, dst, iinfo) -> + print_pref pp pref; + fprintf pp "%d: Bload: %a = %s[%a]%a\n" iinfo.inumb reg dst + (name_of_chunk chunk) + (PrintOp.print_addressing reg) + (addr, args) print_trapping_mode trap + | Bstore (chunk, addr, args, src, iinfo) -> + print_pref pp pref; + fprintf pp "%d: Bstore: %s[%a] = %a\n" iinfo.inumb (name_of_chunk chunk) + (PrintOp.print_addressing reg) + (addr, args) reg src + | BF (Bcall (sg, fn, args, res, s), iinfo) -> + print_pref pp pref; + fprintf pp "%d: Bcall: %a = %a(%a)\n" iinfo.inumb reg res ros fn regs args; + print_succ pp s + | BF (Btailcall (sg, fn, args), iinfo) -> + print_pref pp pref; + fprintf pp "%d: Btailcall: %a(%a)\n" iinfo.inumb ros fn regs args + | BF (Bbuiltin (ef, args, res, s), iinfo) -> + print_pref pp pref; + fprintf pp "%d: Bbuiltin: %a = %s(%a)\n" iinfo.inumb + (print_builtin_res reg) res (name_of_external ef) + (print_builtin_args reg) args; + print_succ pp s + | Bcond (cond, args, ib1, ib2, iinfo) -> + print_pref pp pref; + fprintf pp "%d: Bcond: (%a) (prediction: %s)\n" iinfo.inumb + (PrintOp.print_condition reg) + (cond, args) + (match iinfo.pcond with + | None -> "none" + | Some true -> "branch" + | Some false -> "fallthrough"); + let pref' = pref ^ " " in + fprintf pp "%sifso = [\n" pref; + if is_rec then print_iblock pp is_rec pref' ib1 else fprintf pp "...\n"; + fprintf pp "%s]\n" pref; + fprintf pp "%sifnot = [\n" pref; + if is_rec then print_iblock pp is_rec pref' ib2 else fprintf pp "...\n"; + fprintf pp "%s]\n" pref + | BF (Bjumptable (arg, tbl), iinfo) -> + let tbl = Array.of_list tbl in + print_pref pp pref; + fprintf pp "%d: Bjumptable: (%a)\n" iinfo.inumb reg arg; + for i = 0 to Array.length tbl - 1 do + fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i)) + done + | BF (Breturn None, iinfo) -> + print_pref pp pref; + fprintf pp "%d: Breturn\n" iinfo.inumb + | BF (Breturn (Some arg), iinfo) -> + print_pref pp pref; + fprintf pp "%d: Breturn: %a\n" iinfo.inumb reg arg + | BF (Bgoto s, iinfo) -> + print_pref pp pref; + fprintf pp "%d: Bgoto: %d\n" iinfo.inumb (P.to_int s) + | Bseq (ib1, ib2) -> + if is_rec then ( + print_iblock pp is_rec pref ib1; + print_iblock pp is_rec pref ib2) + else fprintf pp "Bseq...\n" + +let print_btl_inst pp ib = + if !debug_flag then print_iblock pp false " " ib else () + +let print_btl_code pp btl = + if !debug_flag then ( + fprintf pp "\n"; + List.iter + (fun (n, ibf) -> + fprintf pp "[BTL Liveness] "; + print_regset ibf.input_regs; + fprintf pp "\n"; + fprintf pp "[BTL block %d with inumb %d]\n" (P.to_int n) ibf.binfo.bnumb; + print_iblock pp true " " ibf.entry; + fprintf pp "\n") + (PTree.elements btl); + fprintf pp "\n") + else () + +(* TODO gourdinl remove or adapt this? +let print_function pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; + let instrs = List.map (fun (n, i) -> i.entry) (PTree.elements f.fn_code) in + List.iter (print_iblock pp true "") instrs; + fprintf pp "}\n\n" + +let print_globdef pp (id, gd) = + match gd with Gfun (Internal f) -> print_function pp id f | _ -> () + +let print_program pp (prog : BTL.program) = + List.iter (print_globdef pp) prog.prog_defs*) diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml index 2a20a15d..976ddc16 100644 --- a/scheduling/RTLpathLivegenaux.ml +++ b/scheduling/RTLpathLivegenaux.ml @@ -4,34 +4,8 @@ open Registers open Maps open Camlcoq open Datatypes -open Kildall -open Lattice open DebugPrint - -let get_some = function -| None -> failwith "Got None instead of Some _" -| Some thing -> thing - -let successors_inst = function -| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) | Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> [n] -| Icond (_,_,n1,n2,_) -> [n1; n2] -| Ijumptable (_,l) -> l -| Itailcall _ | Ireturn _ -> [] - -let predicted_successor = function -| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> Some n -| Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> None -| Icond (_,_,n1,n2,p) -> ( - match p with - | Some true -> Some n1 - | Some false -> Some n2 - | None -> None ) -| Ijumptable _ | Itailcall _ | Ireturn _ -> None - -let non_predicted_successors i = - match predicted_successor i with - | None -> successors_inst i - | Some n -> List.filter (fun n' -> n != n') (successors_inst i) +open RTLcommonaux let rec list_to_regset = function | [] -> Regset.empty @@ -59,24 +33,6 @@ let get_output_reg i = | Iop (_, _, r, _) | Iload (_, _, _, _, r, _) | Icall (_, _, _, r, _) -> Some r | Ibuiltin (_, _, brr, _) -> (match brr with AST.BR r -> Some r | _ -> None) -(* adapted from Linearizeaux.get_join_points *) -let get_join_points code entry = - let reached = ref (PTree.map (fun n i -> false) code) in - let reached_twice = ref (PTree.map (fun n i -> false) code) in - let rec traverse pc = - if get_some @@ PTree.get pc !reached then begin - if not (get_some @@ PTree.get pc !reached_twice) then - reached_twice := PTree.set pc true !reached_twice - end else begin - reached := PTree.set pc true !reached; - traverse_succs (successors_inst @@ get_some @@ PTree.get pc code) - end - and traverse_succs = function - | [] -> () - | [pc] -> traverse pc - | pc :: l -> traverse pc; traverse_succs l - in traverse entry; !reached_twice - (* Does not set the input_regs and liveouts field *) let get_path_map code entry join_points = let visited = ref (PTree.map (fun n i -> false) code) in @@ -92,12 +48,13 @@ let get_path_map code entry join_points = let inst = get_some @@ PTree.get n code in begin psize := !psize + 1; - let successor = match predicted_successor inst with + let psucc = predicted_successor inst in + let successor = match psucc with | None -> None | Some n' -> if get_some @@ PTree.get n' join_points then None else Some n' in match successor with | Some n' -> begin - path_successors := !path_successors @ non_predicted_successors inst; + path_successors := !path_successors @ non_predicted_successors inst psucc; dig_path_rec n' end | None -> Some ({ psize = (Camlcoq.Nat.of_int !psize); @@ -118,40 +75,6 @@ let get_path_map code entry join_points = !path_map end -let transfer f pc after = let open Liveness in - match PTree.get pc f.fn_code with - | Some i -> - (match i with - | Inop _ -> after - | Iop (_, args, res, _) -> - reg_list_live args (Regset.remove res after) - | Iload (_, _, _, args, dst, _) -> - reg_list_live args (Regset.remove dst after) - | Istore (_, _, args, src, _) -> - reg_list_live args (Regset.add src after) - | Icall (_, ros, args, res, _) -> - reg_list_live args (reg_sum_live ros (Regset.remove res after)) - | Itailcall (_, ros, args) -> - reg_list_live args (reg_sum_live ros Regset.empty) - | Ibuiltin (_, args, res, _) -> - reg_list_live (AST.params_of_builtin_args args) - (reg_list_dead (AST.params_of_builtin_res res) after) - | Icond (_, args, _, _, _) -> - reg_list_live args after - | Ijumptable (arg, _) -> - Regset.add arg after - | Ireturn optarg -> - reg_option_live optarg Regset.empty) - | None -> Regset.empty - -module RegsetLat = LFSet(Regset) - -module DS = Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward) - -let analyze f = - let liveouts = get_some @@ DS.fixpoint f.fn_code successors_instr (transfer f) in - PTree.map (fun n _ -> let lo = PMap.get n liveouts in transfer f n lo) f.fn_code - (** OLD CODE - If needed to have our own kildall let transfer after = let open Liveness in function diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml index aeed39df..3db25d82 100644 --- a/scheduling/RTLpathScheduleraux.ml +++ b/scheduling/RTLpathScheduleraux.ml @@ -7,6 +7,7 @@ open RTL open Maps open Registers open ExpansionOracle +open RTLcommonaux let config = Machine.config diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v new file mode 100644 index 00000000..309c616e --- /dev/null +++ b/scheduling/RTLtoBTL.v @@ -0,0 +1,27 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad BTL. +Require Export BTLmatchRTL BTL_Livecheck. + +Require Import Errors Linking. + +(** External oracle *) +Axiom rtl2btl: RTL.function -> BTL.code * node * (PTree.t node). + +Extract Constant rtl2btl => "RTLtoBTLaux.rtl2btl". + +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; + do u <- liveness_checker 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/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml new file mode 100644 index 00000000..3de82d96 --- /dev/null +++ b/scheduling/RTLtoBTLaux.ml @@ -0,0 +1,116 @@ +open Maps +open RTL +open BTL +open PrintBTL +open RTLcommonaux +open DebugPrint +open BTLtypes +open BTLcommonaux + +let encaps_final inst osucc = + match inst with + | BF _ -> inst + | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo ())) + +let translate_inst (iinfo : BTL.inst_info) inst is_final = + let osucc = ref None in + let btli = + match inst with + | Inop s -> + osucc := Some s; + Bnop (Some iinfo) + | Iop (op, lr, rd, s) -> + osucc := Some s; + Bop (op, lr, rd, iinfo) + | Iload (trap, chk, addr, lr, rd, s) -> + osucc := Some s; + Bload (trap, chk, addr, lr, rd, iinfo) + | Istore (chk, addr, lr, src, s) -> + osucc := Some s; + Bstore (chk, addr, lr, src, iinfo) + | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s), iinfo) + | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr), iinfo) + | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo) + | Icond (cond, lr, ifso, ifnot, info) -> + osucc := Some ifnot; + iinfo.pcond <- info; + Bcond + ( cond, + lr, + BF (Bgoto ifso, def_iinfo ()), + Bnop None, + iinfo ) + | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl), iinfo) + | Ireturn oreg -> BF (Breturn oreg, iinfo) + in + if is_final then encaps_final btli !osucc else btli + +let translate_function code entry join_points liveness = + let reached = ref (PTree.map (fun n i -> false) code) in + let btl_code = ref PTree.empty in + let rec build_btl_tree e = + if get_some @@ PTree.get e !reached then () + else ( + reached := PTree.set e true !reached; + let next_nodes = ref [] in + let rec build_btl_block n = + let inst = get_some @@ PTree.get n code in + let psucc = predicted_successor inst in + let iinfo = mk_iinfo (p2i n) None in + let succ = + match psucc with + | Some ps -> + if get_some @@ PTree.get ps join_points then None else Some ps + | None -> None + in + match succ with + | Some s -> ( + match inst with + | Icond (cond, lr, ifso, ifnot, info) -> + (* TODO gourdinl remove this *) + assert (s = ifnot); + next_nodes := !next_nodes @ non_predicted_successors inst psucc; + iinfo.pcond <- info; + Bseq + ( Bcond + (cond, lr, BF (Bgoto ifso, def_iinfo ()), Bnop None, iinfo), + build_btl_block s ) + | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s)) + | None -> + debug "BLOCK END.\n"; + next_nodes := !next_nodes @ successors_inst inst; + translate_inst iinfo inst true + in + let ib = build_btl_block e in + let succs = !next_nodes in + + let inputs = get_some @@ PTree.get e liveness in + let bi = mk_binfo (p2i e) in + let ibf = { entry = ib; input_regs = inputs; binfo = bi } in + btl_code := PTree.set e ibf !btl_code; + List.iter build_btl_tree succs) + in + build_btl_tree entry; + !btl_code + +let rtl2btl (f : RTL.coq_function) = + let code = f.fn_code in + let entry = f.fn_entrypoint in + let join_points = get_join_points code entry in + let liveness = analyze f in + let btl = translate_function code entry join_points liveness in + let dm = PTree.map (fun n i -> n) btl in + (* TODO gourdinl move elsewhere *) + (*debug_flag := true;*) + debug "Entry %d\n" (p2i entry); + debug "RTL Code: "; + print_code code; + debug "BTL Code:\n"; + print_btl_code stderr btl; + (*debug_flag := false;*) + debug "Dupmap:\n"; + print_ptree print_pint dm; + debug "Join points: "; + print_true_nodes join_points; + debug "\n"; + ((btl, entry), dm) diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v new file mode 100644 index 00000000..18ff8d5f --- /dev/null +++ b/scheduling/RTLtoBTLproof.v @@ -0,0 +1,749 @@ +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. + +(** * Normalization of BTL iblock for simulation of RTL + +Below [normRTL] normalizes the representation of BTL blocks, +in order to represent as sequences of RTL instructions. + +This eases the + +*) + +Definition is_RTLatom (ib: iblock): bool := + match ib with + | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false + | _ => true + end. + +Definition is_RTLbasic (ib: iblock): bool := + match ib with + | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None | BF _ _ => false + | _ => true + end. + +(** The strict [is_normRTL] property specifying the ouput of [normRTL] below *) +Inductive is_normRTL: iblock -> Prop := + | norm_Bseq ib1 ib2: + is_RTLbasic ib1 = true -> + is_normRTL ib2 -> + is_normRTL (Bseq ib1 ib2) + | norm_Bcond cond args ib1 ib2 i: + is_normRTL ib1 -> + is_normRTL ib2 -> + is_normRTL (Bcond cond args ib1 ib2 i) + | norm_others ib: + is_RTLatom ib = true -> + is_normRTL ib + . +Local Hint Constructors is_normRTL: core. + +(** Weaker version allowing for trailing [Bnop None]. *) +Inductive is_wnormRTL: iblock -> Prop := + | wnorm_Bseq ib1 ib2: + is_RTLbasic ib1 = true -> + (ib2 <> Bnop None -> is_wnormRTL ib2) -> + is_wnormRTL (Bseq ib1 ib2) + | wnorm_Bcond cond args ib1 ib2 iinfo: + (ib1 <> Bnop None -> is_wnormRTL ib1) -> + (ib2 <> Bnop None -> is_wnormRTL ib2) -> + is_wnormRTL (Bcond cond args ib1 ib2 iinfo) + | wnorm_others ib: + is_RTLatom ib = true -> + is_wnormRTL ib + . +Local Hint Constructors is_wnormRTL: core. + +(* NB: [k] is a "continuation" (e.g. semantically [normRTLrec ib k] is like [Bseq ib k]) *) +Fixpoint normRTLrec (ib: iblock) (k: iblock): iblock := + match ib with + | Bseq ib1 ib2 => normRTLrec ib1 (normRTLrec ib2 k) + | Bcond cond args ib1 ib2 iinfo => + Bcond cond args (normRTLrec ib1 k) (normRTLrec ib2 k) iinfo + | BF fin iinfo => BF fin iinfo + | Bnop None => k + | ib => Bseq ib k + end. + +Definition normRTL ib := normRTLrec ib (Bnop None). + +Lemma normRTLrec_wcorrect ib: forall k, + (k <> (Bnop None) -> is_wnormRTL k) -> + (normRTLrec ib k) <> Bnop None -> + is_wnormRTL (normRTLrec ib k). +Proof. + induction ib; simpl; intros; repeat autodestruct; auto. +Qed. + +Lemma normRTL_wcorrect ib: + (normRTL ib) <> Bnop None -> + is_wnormRTL (normRTL ib). +Proof. + intros; eapply normRTLrec_wcorrect; eauto. +Qed. + +Lemma is_join_opt_None {A} (opc1 opc2: option A): + is_join_opt opc1 opc2 None -> opc1 = None /\ opc2 = None. +Proof. + intros X. inv X; auto. +Qed. + +Lemma match_iblock_None_not_Bnop dupmap cfg isfst pc ib: + match_iblock dupmap cfg isfst pc ib None -> ib <> Bnop None. +Proof. + intros X; inv X; try congruence. +Qed. +Local Hint Resolve match_iblock_None_not_Bnop: core. + +Lemma is_wnormRTL_normRTL dupmap cfg ib: + is_wnormRTL ib -> + forall isfst pc + (MIB: match_iblock dupmap cfg isfst pc ib None), + is_normRTL ib. +Proof. + induction 1; simpl; intros; auto; try (inv MIB); eauto. + (* Bcond *) + destruct (is_join_opt_None opc1 opc2); subst; eauto. + econstructor; eauto. +Qed. + +Local Hint Constructors iblock_istep: core. +Lemma normRTLrec_iblock_istep_correct tge 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 => iblock_istep tge sp rs1 m1 k rs2 m2 ofin2 + | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1 + end), + iblock_istep tge sp rs0 m0 (normRTLrec ib k) rs2 m2 ofin2. +Proof. + induction 1; simpl; intuition subst; eauto. + { (* Bnop *) autodestruct; eauto. } + 1-3: (* Bop, Bload, Bstore *) + intros; repeat econstructor; eauto. + (* Bcond *) + destruct ofin; intuition subst; + destruct b; eapply IHISTEP; eauto. +Qed. + +Lemma normRTL_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin: + iblock_istep tge sp rs0 m0 ib rs1 m1 ofin -> + iblock_istep tge sp rs0 m0 (normRTL ib) rs1 m1 ofin. +Proof. + intros; eapply normRTLrec_iblock_istep_correct; eauto. + destruct ofin; simpl; auto. +Qed. + +Lemma normRTLrec_iblock_istep_run_None tge sp ib: + forall rs0 m0 k + (CONT: match iblock_istep_run tge sp ib rs0 m0 with + | Some (out rs1 m1 ofin) => + ofin = None /\ + iblock_istep_run tge sp k rs1 m1 = None + | _ => True + end), + iblock_istep_run tge sp (normRTLrec ib k) rs0 m0 = None. +Proof. + induction ib; simpl; intros; subst; intuition (try discriminate). + - (* Bnop *) + intros. autodestruct; auto. + - (* Bop *) + intros; repeat autodestruct; simpl; intuition congruence. + - (* Bload *) + intros; repeat autodestruct; simpl; intuition congruence. + - (* Bstore *) + intros; repeat autodestruct; simpl; intuition congruence. + - (* Bseq *) + intros. + eapply IHib1; eauto. + autodestruct; simpl in *; destruct o; simpl in *; intuition eauto. + + destruct _fin; intuition eauto. + + destruct _fin; intuition congruence || eauto. + - (* Bcond *) + intros; repeat autodestruct; simpl; intuition congruence || eauto. +Qed. + +Lemma normRTL_preserves_iblock_istep_run_None tge sp ib: + forall rs m, iblock_istep_run tge sp ib rs m = None + -> iblock_istep_run tge sp (normRTL ib) rs m = None. +Proof. + intros; eapply normRTLrec_iblock_istep_run_None; eauto. + rewrite H; simpl; auto. +Qed. + +Lemma normRTL_preserves_iblock_istep_run tge sp ib: + forall rs m, iblock_istep_run tge sp ib rs m = + iblock_istep_run tge sp (normRTL ib) 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 normRTL_iblock_istep_correct; auto. + - symmetry. + apply normRTL_preserves_iblock_istep_run_None; auto. +Qed. + +Local Hint Constructors match_iblock: core. +Lemma normRTLrec_matchiblock_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' => + match_iblock dupmap cfg false pc' k opc2 + | None => opc2=opc1 + end), + match_iblock dupmap cfg isfst pc (normRTLrec ib k) opc2. +Proof. + induction 1; simpl; intros; subst; eauto. + (* Bcond *) + intros. inv H0; + econstructor; eauto; try econstructor. + destruct opc0; econstructor. +Qed. + +Lemma normRTL_matchiblock_correct dupmap cfg ib pc isfst opc: + match_iblock dupmap cfg isfst pc ib opc -> + match_iblock dupmap cfg isfst pc (normRTL ib) opc. +Proof. + intros. + eapply normRTLrec_matchiblock_correct; eauto. + destruct opc; simpl; auto. +Qed. + +Lemma is_normRTL_correct dupmap cfg ib pc + (MI : match_iblock dupmap cfg true pc ib None): + is_normRTL (normRTL ib). +Proof. + exploit normRTL_matchiblock_correct; eauto. + intros MI2. + eapply is_wnormRTL_normRTL; eauto. + apply normRTL_wcorrect; try congruence. + inv MI2; discriminate. +Qed. + +(** * Matching relation on functions *) + +(* we simply switch [f] and [tf] in the usual way *) +Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := { + matchRTL:> BTLmatchRTL.match_function dupmap tf f; + liveness_ok: liveness_ok_function tf; +}. + +Local Hint Resolve matchRTL: core. + +Inductive match_fundef: RTL.fundef -> BTL.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: RTL.stackframe -> BTL.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) (BTL.Stackframe res f' sp pc' rs). + +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. +*) +Admitted. + +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_normRTL 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. +Admitted. + +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 match_iblock_true_isnt_goto dupmap cfg pc ib opc: + match_iblock dupmap cfg true pc ib opc -> + is_goto ib = false. +Proof. + intros MIB; inversion MIB as [d1 d2 d3 d4 d5 H H0| | | | | | | |]; subst; simpl; try congruence. + inv H0; congruence. +Qed. + +Local Hint Resolve match_iblock_true_isnt_goto normRTL_preserves_iblock_istep_run star_refl star_right: core. +Local Hint Constructors match_strong_state RTL.step: core. + +(** At entry in a block: we init [match_states] on [normRTL] to normalize the block *) +Lemma match_states_entry dupmap st f sp pc ib rs m st' f' pc' + (STACKS : list_forall2 match_stackframes st st') + (TRANSF : match_function dupmap f f') + (FN : (fn_code f') ! pc' = Some ib) + (MI : match_iblock dupmap (RTL.fn_code f) true pc (entry ib) None) + (DUP : dupmap ! pc' = Some pc): + match_states (Some (normRTL (entry ib))) (RTL.State st f sp pc rs m) (State st' f' sp pc' rs m). +Proof. + exploit is_normRTL_correct; eauto. + econstructor; eauto; apply normRTL_matchiblock_correct in MI; eauto. +Qed. +Local Hint Resolve match_states_entry: core. + +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. + + +(** * 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 t s1' + (EQt: t=E0) + (EQs1': s1'=(RTL.State st f sp pcR2 rs2 m2)) + (STEP : RTL.step ge (RTL.State st f sp pcR1 rs1 m1) t s1') + (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 tid tge (State st' f' sp pcB0 rs0 m0) E0 s2' + /\ match_states oib' s1' s2') + \/ (omeasure oib' < n /\ t=E0 + /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)). +Proof. + subst. + destruct (is_goto ib2) eqn:GT. + destruct ib2; try destruct fi; try discriminate. + - (* Bgoto *) + inv MSS2. inversion MIB; subst; try inv H4. + remember H2 as ODUPLIC; clear HeqODUPLIC. + exploit dupmap_correct; eauto. + intros [ib [FNC MI]]. + eexists; left; eexists; split; eauto. + repeat econstructor; eauto. + apply iblock_istep_run_equiv in BTL_RUN; eauto. + econstructor. + - (* 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 tid 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. + inv 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 *) + exploit dupmap_correct; eauto. + intros [ib [FNC MI]]. + exists (Some (normRTL (entry ib))); left; eexists; split; eauto. + 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. + + (* Bjumptable *) + exploit list_nth_z_rev_dupmap; eauto. + intros (pc'0 & LNZ & DM). + exploit dupmap_correct; eauto. + intros [ib [FNC MI]]. + exists (Some (normRTL (entry ib))); left; eexists; split; eauto. + econstructor; eauto. econstructor. + eexists; eexists; split. + eapply iblock_istep_run_equiv in BTL_RUN. + eapply BTL_RUN. econstructor; eauto. + - (* mib_exit *) + discriminate. + - (* mib_seq *) + inv IS_EXPD; try discriminate. + inv H; simpl in *; try congruence; + inv STEP; try_simplify_someHyps; eauto. + + (* Bnop is_rtl *) + intros; eapply match_strong_state_simu; eauto. + + (* Bop *) + intros; eapply match_strong_state_simu; eauto. + econstructor; eauto. + erewrite eval_operation_preserved in H12. + erewrite H12 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. + + (* Bload *) + intros; eapply match_strong_state_simu; eauto. + econstructor; eauto. + erewrite eval_addressing_preserved in H12. + erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. + + (* Bstore *) + intros; eapply match_strong_state_simu; eauto. + econstructor; eauto. + erewrite eval_addressing_preserved in H12. + erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. + - (* mib_cond *) + inv IS_EXPD; try discriminate. + inversion STEP; subst; try_simplify_someHyps; intros. + destruct (is_join_opt_None opc1 opc2); eauto. subst. + eapply match_strong_state_simu with (ib1:=Bcond c lr bso bnot iinfo) (ib2:=(if b then bso else bnot)); eauto. + + intros; rewrite H14 in BTL_RUN; destruct b; econstructor; eauto. + + assert (measure (if b then bnot else bso) > 0) by apply measure_pos; destruct b; simpl; lia. + Unshelve. + all: eauto. +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 tid 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. + exploit dupmap_entrypoint; eauto. intros ENTRY. + exploit dupmap_correct; eauto. + intros [ib [CENTRY MI]]. + exists (Some (normRTL (entry ib))); left; eexists; split. + * eapply exec_function_internal. + erewrite preserv_fnstacksize; eauto. + * erewrite preserv_fnparams; eauto. + + (* 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. + exploit dupmap_correct; eauto. + intros [ib [FNC MI]]. + eexists; left; eexists; split; eauto. + eapply exec_return. +Qed. + +Local Hint Resolve plus_one star_refl: core. + +Theorem transf_program_correct_cfg: + forward_simulation (RTL.semantics prog) (BTLmatchRTL.cfgsem tprog). +Proof. + eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem 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. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (BTL.fsem tprog). +Proof. + eapply compose_forward_simulations. + - eapply transf_program_correct_cfg. + - eapply cfgsem2fsem. +Admitted. + +End BTL_SIMULATES_RTL. |