(** 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. *) 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 "raw" CFG small-step semantics for a BTL program (e.g. close to RTL semantics) *) (* 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). (** 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. (* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation. We start by extending the previous [equiv_*] stuff for [Val.lessdef]: 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. Local Hint Resolve init_regs_lessdef_preserv: core. 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: core. 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. Local Hint Resolve find_function_lessdef regs_lessdef_regs: core. Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of) 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. Admitted. Local Hint Constructors final_step list_forall2: core. Local Hint Unfold regs_lessdef: 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. (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) (** Matching BTL and RTL code We should be able to define a single verifier able to prove a bisimulation between BTL and RTL code. NB 1: the proof of BTL -> RTL (plus simulation) should be much easier than RTL -> BTL (star simulation). NB 2: our scheme allows the BTL to duplicate some RTL code. - in other words: RTL -> BTL allows tail duplication, loop unrolling, etc. Exactly like "Duplicate" on RTL. - BTL -> RTL allows to "undo" some duplications (e.g. remove duplications that have not enabled interesting optimizations) ! Hence, in a sense, our verifier imitates the approach of Duplicate, where [dupmap] maps the BTL nodes to the RTL nodes. The [match_*] definitions gives a "relational" specification of the verifier... *) Require Import Errors. Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop := (* TODO: it may be simplify the oracle for BTL -> RTL, but may makes the verifier more complex ? | mfi_goto pc pc': dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc') *) | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or) | mfi_call pc pc' s ri lr r: dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc') | mfi_tailcall s ri lr: match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr) | mfi_builtin pc pc' ef la br: dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc') | mfi_jumptable ln ln' r: list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' -> match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln') . Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop := | ijo_None_left o: is_join_opt None o o | ijo_None_right o: is_join_opt o None o | ijo_Some x: is_join_opt (Some x) (Some x) (Some x) . (* [match_iblock dupmap cfg isfst pc ib opc] means that [ib] match a block in a RTL code starting at [pc], with: - [isfst] (in "input") indicates that no step in the surrounding block has been executed before entering [pc] - if [opc] (in "ouput") is [None], this means that all branches of the block ends on a final instruction - if [opc] is [Some pc'], this means that all branches of the block that do not exit, join on [pc']. *) Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> iblock -> (option node) -> Prop := | mib_BF isfst fi pc i 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 (* TODO: here [b2] is dead code ! Is this case really useful ? The oracle could remove this dead code. And the verifier could fail if there is such dead code! *) *) | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i 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: code) (cfg':RTL.code): Prop := forall pc pc', dupmap!pc = Some pc' -> exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None. (** Shared verifier between RTL -> BTL and BTL -> RTL *) Local Open Scope error_monad_scope. Definition verify_is_copy dupmap n n' := match dupmap!n with | None => Error(msg "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'). Definition is_goto (ib: iblock): bool := match ib with | BF (Bgoto _) _ => true | _ => false end.