diff options
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 758 |
1 files changed, 758 insertions, 0 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v new file mode 100644 index 00000000..f832085c --- /dev/null +++ b/scheduling/BTL.v @@ -0,0 +1,758 @@ +(** 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 = Vundef) + : has_loaded sp rs m chunk addr args v NOTRAP + . +Local Hint Constructors has_loaded: core. + +(* 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 rs m trap chunk addr args dst v iinfo + (LOAD: has_loaded sp rs m chunk addr args v trap) + : iblock_istep sp rs m (Bload trap chunk addr args dst iinfo) (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 _ => + match eval_addressing ge sp addr rs##args with + | Some a => + match Mem.loadv chunk m a with + | Some v => Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + | None => + Some {| _rs := rs#dst <- Vundef; _m:= m; _fin := None |} + end + | None => + Some {| _rs := rs#dst <- Vundef; _m:= m; _fin := None |} + end + | 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_load sp ib v rs rs' m trap chunk addr args dst iinfo ofin: + ib = (Bload trap chunk addr args dst iinfo) -> + rs' = rs # dst <- v -> + has_loaded sp rs m chunk addr args v trap -> + iblock_istep sp rs m ib rs' m ofin <-> + iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m := m; _fin := ofin |}. +Proof. + split; subst; inv H1; simpl in *; intros. + - destruct trap; inv H; simpl in *; repeat autodestruct. + - inv H; autodestruct; rewrite LOAD; auto. + - destruct trap; inv H; simpl in *; + rewrite EVAL, LOAD in H1; inv H1; repeat econstructor; eauto. + - generalize H; autodestruct. + + rewrite LOAD in *; inv H; auto; constructor. + eapply has_loaded_default; eauto; try_simplify_someHyps. + + inv H; constructor. eapply has_loaded_default; eauto; try_simplify_someHyps. +Qed. +Local Hint Resolve iblock_istep_run_equiv_load: core. + +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; try (eapply iblock_istep_run_equiv_load; eauto; fail); + 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). + 1,2: constructor; eapply has_loaded_default; 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. + |