diff options
-rw-r--r-- | scheduling/BTL.v | 491 | ||||
-rw-r--r-- | scheduling/BTL_SEtheory.v | 541 | ||||
-rw-r--r-- | scheduling/BTLroadmap.md | 64 | ||||
-rw-r--r-- | scheduling/BTLtoRTLproof.v | 18 | ||||
-rw-r--r-- | scheduling/RTLtoBTLproof.v | 10 |
5 files changed, 840 insertions, 284 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index caa48920..2be4fcac 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -17,6 +17,9 @@ 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 *) @@ -91,7 +94,7 @@ Coercion BF: final >-> Funclass. Record iblock_info := { entry: iblock; - input_regs: Regset.t; (* extra liveness information ignored by BTL semantics *) + input_regs: Regset.t (* extra liveness information for BTL functional semantics *) binfo: block_info (* Ghost field used in oracles *) }. @@ -168,8 +171,26 @@ Record outcome := out { _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 := @@ -280,10 +301,12 @@ Proof. 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 rs m) + (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' -> @@ -293,7 +316,7 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := find_function ros rs = Some fd -> funsig fd = sig -> final_step stack f sp rs m (Bcall sig ros args res pc') - E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m) + 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 -> @@ -305,12 +328,12 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> final_step stack f sp rs m (Bbuiltin ef args res pc') - t (State stack f sp pc' (regmap_setres res vres rs) m') + 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' rs m) + E0 (State stack f sp pc' (tr_exit f tbl None rs) m) . (** big-step execution of one iblock *) @@ -367,11 +390,463 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate nil (Vint r) m) r. -(** The small-step semantics for a program. *) +(** 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. -Definition semantics (p: program) := - Semantics step (initial_state p) final_state (Genv.globalenv p). +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" ? *) diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index cd69cd37..cea69f55 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1,7 +1,12 @@ -(* A theory of symbolic execution on BTL +(** 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. @@ -9,10 +14,6 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import Op Registers. Require Import RTL BTL OptionMonad. -(* TODO remove this, when copy-paste of RTLpathSE_theory is clearly over... *) -Ltac inversion_SOME := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) -Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) - Record iblock_exec_context := Bctx { cge: BTL.genv; cstk: list stackframe; @@ -26,6 +27,7 @@ Record iblock_exec_context := Bctx { (* symbolic value *) Inductive sval := + | Sundef | Sinput (r: reg) | Sop (op:operation) (lsv: list_sval) (sm: smem) | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) @@ -51,6 +53,7 @@ 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 sm => SOME args <- eval_list_sval ctx l IN @@ -109,7 +112,7 @@ Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : o (** * Auxiliary definitions on Builtins *) -(* TODO: clean this. Some (cge ctx)neric stuffs could be put in [AST.v] *) +(* TODO: clean this. Some generic stuffs could be put in [AST.v] *) Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *) @@ -166,7 +169,7 @@ Qed. End SEVAL_BUILTIN_ARG. -(* NB: (cge ctx)neric function that could be put into [AST] file *) +(* 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) @@ -381,7 +384,6 @@ Qed. Inductive sfval := | Sgoto (pc: exit) | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit) - (* NB: [res] the return register is hard-wired ! Is it restrictive ? *) | Stailcall: signature -> sval + ident -> list_sval -> sfval | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:exit) | Sjumptable (sv: sval) (tbl: list exit) @@ -395,21 +397,24 @@ Definition sfind_function ctx (svos : sval + ident): option fundef := end . +Import ListNotations. +Local Open Scope list_scope. + Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop := | exec_Sgoto pc rs m: - sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs m) + sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] None rs) m) | exec_Sreturn stk osv rs m m' v: (csp ctx) = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' -> match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v -> - sem_sfval ctx (Sreturn osv) rs m + sem_sfval ctx (Sreturn osv) rs m E0 (Returnstate (cstk ctx) v m') | exec_Scall rs m sig svos lsv args res pc fd: sfind_function ctx svos = Some fd -> funsig fd = sig -> eval_list_sval ctx lsv = Some args -> sem_sfval ctx (Scall sig svos lsv res pc) rs m - E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc rs :: (cstk ctx)) fd args m) + E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] (Some res) rs)::cstk ctx) fd args m) | exec_Stailcall stk rs m sig svos args fd m' lsv: sfind_function ctx svos = Some fd -> funsig fd = sig -> @@ -422,136 +427,23 @@ Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop := seval_builtin_args ctx m sargs vargs -> external_call ef (cge ctx) vargs m t vres m' -> sem_sfval ctx (Sbuiltin ef sargs res pc) rs m - t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs) m') + t (State (cstk ctx) (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 (Sjumptable sv tbl) rs m - E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m) + E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' (tr_inputs ctx.(cf) tbl None rs) m) . -(** * Preservation properties *) - -Section SymbValPreserved. - -Variable ge ge': BTL.genv. - -Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s. - -Hypothesis senv_preserved_BTL: Senv.equiv ge ge'. - -Lemma senv_find_symbol_preserved id: - Senv.find_symbol ge id = Senv.find_symbol ge' id. -Proof. - destruct senv_preserved_BTL as (A & B & C). congruence. -Qed. - -Lemma senv_symbol_address_preserved id ofs: - Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs. -Proof. - unfold Senv.symbol_address. rewrite senv_find_symbol_preserved. - reflexivity. -Qed. - -Variable stk stk': list stackframe. -Variable f f': function. -Variable sp: val. -Variable rs0: regset. -Variable m0: mem. - -Lemma eval_sval_preserved sv: - eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv. -Proof. - induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv) - (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto. - + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto. - rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto. - erewrite eval_operation_preserved; eauto. - + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. - erewrite <- eval_addressing_preserved; eauto. - destruct (eval_addressing _ sp _ _); auto. - rewrite IHsv; auto. - + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto. - rewrite IHsv0; auto. - + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. - erewrite <- eval_addressing_preserved; eauto. - destruct (eval_addressing _ sp _ _); auto. - rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto. - rewrite IHsv1; auto. -Qed. - -Lemma seval_builtin_arg_preserved m: forall bs varg, - seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg -> - seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg. -Proof. - induction 1; simpl. - all: try (constructor; auto). - - rewrite <- eval_sval_preserved. assumption. - - rewrite <- senv_symbol_address_preserved. assumption. - - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal. -Qed. - -Lemma seval_builtin_args_preserved m lbs vargs: - seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs -> - seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs. -Proof. - induction 1; constructor; eauto. - eapply seval_builtin_arg_preserved; auto. -Qed. - -Lemma list_sval_eval_preserved lsv: - eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv. -Proof. - induction lsv; simpl; auto. - rewrite eval_sval_preserved. destruct (eval_sval _ _); auto. - rewrite IHlsv; auto. -Qed. - -Lemma smem_eval_preserved sm: - eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm. -Proof. - induction sm; simpl; auto. - rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. - erewrite <- eval_addressing_preserved; eauto. - destruct (eval_addressing _ sp _ _); auto. - rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto. - rewrite eval_sval_preserved; auto. -Qed. - -Lemma seval_condition_preserved cond lsv sm: - seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm. -Proof. - unfold seval_condition. - rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. - rewrite smem_eval_preserved; auto. -Qed. - -End SymbValPreserved. - - (* Syntax and Semantics of symbolic internal states *) (* [si_pre] is a precondition on initial context *) Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg: reg -> sval; si_smem: smem }. (* Predicate on which (rs, m) is a possible final state after evaluating [st] on ((crs0 ctx), (cm0 ctx)) *) -Definition sem_sistate ctx (st: sistate) (rs: regset) (m: mem): Prop := - st.(si_pre) ctx - /\ eval_smem ctx st.(si_smem) = Some m - /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r). - -(* Remark that we need to reason modulo "extensionality" wrt Regmap.get about regsets. - And, nothing in their representation as (val * PTree.t val) enforces that - (forall r, rs1#r = rs2#r) -> rs1 = rs2 -*) -Lemma sem_sistate_determ ctx st rs1 m1 rs2 m2: - sem_sistate ctx st rs1 m1 -> - sem_sistate ctx st rs2 m2 -> - (forall r, rs1#r = rs2#r) /\ m1 = m2. -Proof. - intros (_&MEM1®1) (_&MEM2®2). - intuition try congruence. - generalize (REG1 r); rewrite REG2; congruence. -Qed. +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) (sis: sistate): sfval := @@ -580,10 +472,10 @@ Local Hint Constructors sem_sfval: core. Lemma sexec_final_svf_correct ctx i sis t rs m s: sem_sistate ctx sis rs m -> - final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> + final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> sem_sfval ctx (sexec_final_sfv i sis) rs m t s. Proof. - intros (PRE&MEM®). + 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. @@ -604,7 +496,7 @@ Local Hint Resolve seval_builtin_args_exact: core. Lemma sexec_final_svf_exact ctx i sis t rs m s: sem_sistate ctx sis rs m -> sem_sfval ctx (sexec_final_sfv i sis) rs m t s - -> final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s. + -> final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s. Proof. intros (PRE&MEM®). destruct i; simpl; intros LAST; inv LAST; eauto. @@ -626,7 +518,6 @@ Proof. congruence. Qed. - (** * symbolic execution of basic instructions *) Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}. @@ -735,6 +626,76 @@ Proof. erewrite MEM; auto. 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 r r1 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) |}. + +Definition sreg_eval ctx (sis: sistate) (r: reg): option val := + eval_sval ctx (sis.(si_sreg) r). + +Lemma tr_sis_regs_correct_aux ctx fin sis rs m: + sem_sistate ctx sis rs m -> + (forall r, sreg_eval ctx (tr_sis (cf ctx) fin sis) r = Some (tr_regs (cf ctx) fin rs) # r). +Proof. + Local Opaque str_inputs. + unfold sreg_eval; 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 (svf: sfval): A := + match svf 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 *) @@ -746,8 +707,8 @@ Inductive sstate := (* transition (t,s) produced by a sstate in initial context ctx *) Inductive sem_sstate ctx t s: sstate -> Prop := - | sem_Sfinal sis sfv rs m - (SIS: sem_sistate ctx sis rs m) + | sem_Sfinal sis sfv rs m + (SIS: sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m) (SFV: sem_sfval ctx sfv rs m t s) : sem_sstate ctx t s (Sfinal sis sfv) | sem_Scond b cond args sm ifso ifnot @@ -768,9 +729,9 @@ pour représenter l'ensemble des chemins. *) -Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := +Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := match ib with - | BF fin _ => Sfinal sis (sexec_final_sfv fin sis) + | 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) @@ -779,19 +740,19 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := | Bstore chunk addr args src _ => k (sexec_store chunk addr args src sis) (* composed instructions *) | Bseq ib1 ib2 => - sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) + 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 ifso sis k in - let ifnot := sexec_rec ifnot sis k in + let ifso := sexec_rec f ifso sis k in + let ifnot := sexec_rec f ifnot sis k in Scond cond args sis.(si_smem) ifso ifnot end . -Definition sexec ib := sexec_rec ib sis_init (fun _ => Sabort). +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_svf_correct +Local Hint Resolve sexec_op_correct sexec_final_svf_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 t s ib rs m rs1 m1 ofin @@ -799,131 +760,72 @@ Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin (SIS: sem_sistate ctx sis rs m) (CONT: match ofin with | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx t s (k sis') - | Some fin => final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s + | Some fin => final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s end), - sem_sstate ctx t s (sexec_rec ib sis k). + sem_sstate ctx 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 ifso sis k else sexec_rec ifnot sis k) with (sexec_rec (if b then ifso else ifnot) sis k); + 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 ib t s: - iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s -> - sem_sstate ctx t s (sexec ib). + iblock_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s -> + sem_sstate ctx t s (sexec (cf ctx) ib). Proof. destruct 1 as (rs' & m' & fin & ISTEP & FSTEP). eapply sexec_rec_correct; simpl; eauto. Qed. - -(* TODO: déplacer les trucs sur equiv_stackframe -> regmap_setres_eq dans BTL! *) -Inductive equiv_stackframe: stackframe -> stackframe -> Prop := - | equiv_stackframe_intro res f sp pc rs1 rs2 - (EQUIV: forall r : positive, rs1 !! r = rs2 !! r): - equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2) - . - -Inductive equiv_state: state -> state -> Prop := - | State_equiv stack f sp pc rs1 m rs2 - (EQUIV: forall r, rs1#r = rs2#r): - equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m) - | Call_equiv stk stk' f args m - (STACKS: list_forall2 equiv_stackframe stk stk'): - equiv_state (Callstate stk f args m) (Callstate stk' f args m) - | Return_equiv stk stk' v m - (STACKS: list_forall2 equiv_stackframe stk stk'): - equiv_state (Returnstate stk v m) (Returnstate stk' v m) - . - -Local Hint Constructors equiv_stackframe equiv_state: core. - -Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf. -Proof. - destruct stf; eauto. -Qed. - -Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk. -Proof. - Local Hint Resolve equiv_stackframe_refl: core. - induction stk; simpl; constructor; auto. -Qed. - -Lemma equiv_state_refl s: equiv_state s s. -Proof. - Local Hint Resolve equiv_stack_refl: core. - induction s; simpl; constructor; auto. -Qed. - -Lemma equiv_stackframe_trans stf1 stf2 stf3: - equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3. -Proof. - destruct 1; intros EQ; inv EQ; try econstructor; eauto. - intros; eapply eq_trans; eauto. -Qed. - -Lemma equiv_stack_trans stk1 stk2: - list_forall2 equiv_stackframe stk1 stk2 -> - forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> - list_forall2 equiv_stackframe stk1 stk3. -Proof. - Local Hint Resolve equiv_stackframe_trans: core. - induction 1; intros stk3 EQ; inv EQ; econstructor; eauto. -Qed. - -Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3. +(* 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. - Local Hint Resolve equiv_stack_trans: core. - destruct 1; intros EQ; inv EQ; econstructor; eauto. - intros; eapply eq_trans; eauto. + intros H1 H2. + lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto. + unfold sreg_eval; 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. -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. +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 sfv m t s: sem_sfval ctx sfv rs1 m t s -> - (forall r, rs1#r = rs2#r) -> - exists s', equiv_state s s' /\ sem_sfval ctx sfv rs2 m t s'. -Proof. - Local Hint Resolve equiv_stack_refl equiv_state_refl regmap_setres_eq: core. - Local Hint Constructors sem_sfval: core. - destruct 1; eexists; split; econstructor; eauto. - econstructor; eauto. + (forall r, (str_regs (cf ctx) sfv rs1)#r = (str_regs (cf ctx) sfv rs2)#r) -> + exists s', sem_sfval ctx 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. -Local Hint Resolve sexec_final_svf_exact: core. - Definition abort_sistate ctx (sis: sistate): Prop := ~(sis.(si_pre) ctx) \/ eval_smem ctx sis.(si_smem) = None \/ exists (r: reg), eval_sval ctx (sis.(si_sreg) r) = None. -Lemma sem_sistate_exclude_abort ctx sis rs m: - sem_sistate ctx sis rs m -> - abort_sistate ctx sis -> - False. -Proof. - intros SIS ABORT. inv SIS. destruct H0 as (H0 & H0'). - inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. -Qed. - -Local Hint Resolve sem_sistate_exclude_abort: core. - Lemma set_sreg_preserves_abort ctx sv dst sis: abort_sistate ctx sis -> abort_sistate ctx (set_sreg dst sv sis). @@ -963,11 +865,20 @@ 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: core. + sexec_store_preserves_abort sem_sistate_tr_sis_exclude_abort: core. Lemma sexec_exclude_abort ctx ib t s1: forall sis k - (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k)) + (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k)) (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False) (ABORT: abort_sistate ctx sis), False. @@ -1039,17 +950,17 @@ Proof. intros; rewrite REG; autodestruct; try_simplify_someHyps. Qed. -Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort: core. +Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort sexec_final_svf_exact: core. Lemma sexec_rec_exact ctx ib t s1: forall sis k - (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k)) + (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k)) rs m (SIS: sem_sistate ctx sis rs m) (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False) , match iblock_istep_run (cge ctx) (csp ctx) ib rs m with | Some (out rs' m' (Some fin)) => - exists s2, final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2 + exists s2, final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2 | Some (out rs' m' None) => exists sis', (sem_sstate ctx t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m') | None => False end. @@ -1057,11 +968,11 @@ Proof. induction ib; simpl; intros; eauto. - (* final *) inv SEXEC. - exploit (sem_sistate_determ ctx sis rs m rs0 m0); eauto. + exploit (sem_sistate_tr_sis_determ ctx sis rs m fi); eauto. intros (REG&MEM); subst. exploit (sem_sfval_equiv rs0 rs); eauto. - intros (s2 & EQUIV & SFV'). - eexists; split; eauto. + * intros; rewrite REG, str_tr_regs_equiv; auto. + * intros (s2 & EQUIV & SFV'); eauto. - (* Bop *) autodestruct; eauto. - destruct trap; [| inv SEXEC ]. repeat autodestruct; eauto. @@ -1094,8 +1005,8 @@ Qed. (sexec is exact). *) Theorem sexec_exact ctx ib t s1: - sem_sstate ctx t s1 (sexec ib) -> - exists s2, iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2 + sem_sstate ctx t s1 (sexec (cf ctx) ib) -> + exists s2, iblock_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2 /\ equiv_state s1 s2. Proof. intros; exploit sexec_rec_exact; eauto. @@ -1109,3 +1020,141 @@ Proof. inversion SEXEC. Qed. +(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) + +Record simu_proof_context := Sctx { + sge1: BTL.genv; + sge2: BTL.genv; + sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s; + sstk1: list BTL.stackframe; + sstk2: list BTL.stackframe; + sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2; + sf1: BTL.function; + sf2: BTL.function; + ssp: val; + srs0: regset; + sm0: mem +}. + +Definition bctx1 (ctx: simu_proof_context):= Bctx ctx.(sge1) ctx.(sstk1) ctx.(sf1) ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx2 (ctx: simu_proof_context):= Bctx ctx.(sge2) ctx.(sstk2) ctx.(sf2) ctx.(ssp) ctx.(srs0) ctx.(sm0). + +Definition sstate_simu (ctx: simu_proof_context) (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 ctx ib1 ib2: Prop := sstate_simu ctx (sexec (sf1 ctx) ib1) (sexec (sf2 ctx) ib2). + +Theorem symbolic_simu_correct ctx ib1 ib2: + symbolic_simu ctx ib1 ib2 -> + forall t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) (sf1 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> + exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) (sf2 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2. +Proof. + unfold symbolic_simu, sstate_simu. + intros SIMU 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 *) + +Section SymbValPreserved. + +Variable ge ge': BTL.genv. + +Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s. + +Hypothesis senv_preserved_BTL: Senv.equiv ge ge'. + +Lemma senv_find_symbol_preserved id: + Senv.find_symbol ge id = Senv.find_symbol ge' id. +Proof. + destruct senv_preserved_BTL as (A & B & C). congruence. +Qed. + +Lemma senv_symbol_address_preserved id ofs: + Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs. +Proof. + unfold Senv.symbol_address. rewrite senv_find_symbol_preserved. + reflexivity. +Qed. + +Variable stk stk': list stackframe. +Variable f f': function. +Variable sp: val. +Variable rs0: regset. +Variable m0: mem. + +Lemma eval_sval_preserved sv: + eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv. +Proof. + induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv) + (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto. + + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto. + rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto. + erewrite eval_operation_preserved; eauto. + + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsv; auto. + + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto. + rewrite IHsv0; auto. + + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto. + rewrite IHsv1; auto. +Qed. + +Lemma seval_builtin_arg_preserved m: forall bs varg, + seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg -> + seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg. +Proof. + induction 1; simpl. + all: try (constructor; auto). + - rewrite <- eval_sval_preserved. assumption. + - rewrite <- senv_symbol_address_preserved. assumption. + - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal. +Qed. + +Lemma seval_builtin_args_preserved m lbs vargs: + seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs -> + seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs. +Proof. + induction 1; constructor; eauto. + eapply seval_builtin_arg_preserved; auto. +Qed. + +Lemma list_sval_eval_preserved lsv: + eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv. +Proof. + induction lsv; simpl; auto. + rewrite eval_sval_preserved. destruct (eval_sval _ _); auto. + rewrite IHlsv; auto. +Qed. + +Lemma smem_eval_preserved sm: + eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm. +Proof. + induction sm; simpl; auto. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto. + rewrite eval_sval_preserved; auto. +Qed. + +Lemma seval_condition_preserved cond lsv sm: + seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm. +Proof. + unfold seval_condition. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. + rewrite smem_eval_preserved; auto. +Qed. + +End SymbValPreserved. diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index 39ea12d0..0cbcd7d6 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -3,8 +3,8 @@ BTL aims to be an IR dedicated to defensive certification of middle-end optimizations (before register allocation). It provides a CFG of "loop-free" blocks, where each block is run in one step emitting at most a single observational event. The "local" optimizations (i.e. preserving "locally" the semantics of such blocks) would be checked by symbolic execution with rewriting rules. -The only info required from oracles: a "dupmap" mapping block entries. -In contrast, the "global" optimizations would require some invariants annotations at block entry (provided by oracles). +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: @@ -16,6 +16,9 @@ Examples of optimizations that we aim to support: 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: @@ -83,7 +86,7 @@ coder la "simulation modulo liveness" dans une "simulation less_undef". Ça peut rendre le cadre du test de simulation plus simple et plus général. -**Idée** à côté de la sémantique "à la RTL" pour BTL, on pourrait +**Idée_Informelle** à côté de la sémantique "à la RTL" pour BTL, on pourrait définir une nouvelle sémantique (basée sur la même sémantique à grand pas dans les blocs), où c'est juste "l'entrée dans un bloc" qui change de sémantique. Intuitivement, cette nouvelle sémantique considèrerait @@ -102,30 +105,49 @@ 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. -En fait, pour le test d'exécution symbolique, il semble plus simple de mettre les Vundef à la fin de la transition... +**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). On pourrait aussi 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 "functional semantics" 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. -**IMPLEM PLAN** +**STATUS** + +1. See [BTL.fsem] (Pour l'instant CFGSemantics => BTL.semantics et FunctionalSemantics => BTL.fsem) + +**TODO** -1. définir the "functional semantics" of BTL. -2. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep"). -3. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics. +1. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep"). +2. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics. en gros: on implémente un vérificateur des infos de liveness. c'est la correction du "input_regs" qui garantit que la simulation est correct. La preuve devrait normalement être très similaire à RTLpathLivegenproof. - ## "Basic" symbolic execution / symbolic simulation -We will implement a "basic" (e.g without rewriting rules) "less_undef" simulation test for BTL.FunctionalSemantics. +We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.FunctionalSemantics. +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é. -**IMPLEM NOTE** +**STATUS** -- use Continuation Passing Style for an easy recursive generation of "all execution paths". +- 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). -**CURRENT STATUS** +**TODO** -- model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms. -- next step: high-level specification of "symbolic simulation" + preservation proof w.r.t BTL.FunctionalSemantics. +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 @@ -327,9 +349,13 @@ Au final, on obtient deux BDD identiques sur cet exemple (sans explosion combina ## Invariants at block entry -Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. +Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. Case-study: support of strength-reduction. + +**IDEAS** -Case-study: support of strength-reduction. +- En pratique, il faudra peut-être 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. + +- 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). ## Support of SSA-optimizations @@ -339,6 +365,4 @@ This should enable to represent SSA-forms in BTL IR, more or less like in MLIR. ## Alias analysis in the symbolic simulation -A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf) - - +A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf) diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 7b62a844..46f360c5 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -303,7 +303,7 @@ Qed. Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s (STACKS : list_forall2 match_stackframes stack stack') (TRANSF : match_function dupmap f f') - (FS : final_step ge stack f sp rs1 m1 fin t s) + (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) @@ -349,7 +349,7 @@ Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fi (TRANSF: match_function dupmap f f') (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin)) (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None) - (FS : final_step ge stack f sp rs1 m1 fin t s) + (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. @@ -370,7 +370,7 @@ Proof. Qed. Theorem plus_simulation s1 t s1': - step ge 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' @@ -401,8 +401,8 @@ Proof. + inv H1. econstructor; eauto. Qed. -Theorem transf_program_correct: - forward_simulation (semantics prog) (RTL.semantics tprog). +Theorem transf_program_correct_cfg: + forward_simulation (BTL.cfgsem prog) (RTL.semantics tprog). Proof. eapply forward_simulation_plus with match_states. - eapply senv_preserved. @@ -411,4 +411,12 @@ Proof. - 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/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index f561ee7a..7d83931b 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -538,7 +538,7 @@ Lemma match_strong_state_simu (MSS2 : match_strong_state dupmap st st' f f' sp rs2 m2 rs0 m0 pcB0 pcR0 pcR2 ib2 ib0 false) (MES : measure ib2 < n) : exists (oib' : option iblock), - (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' + (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)). @@ -566,7 +566,7 @@ Lemma opt_simu_intro (MSTRONG : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst) (NGOTO : is_goto ib = false) : exists (oib' : option iblock), - (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2') + (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. @@ -699,7 +699,7 @@ Theorem opt_simu s1 t s1' oib s2: RTL.step ge s1 t s1' -> match_states oib s1 s2 -> exists (oib' : option iblock), - (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2') + (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. @@ -738,9 +738,9 @@ Qed. Local Hint Resolve plus_one star_refl: core. Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (BTL.semantics tprog). + forward_simulation (RTL.semantics prog) (BTL.cfgsem tprog). Proof. - eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states). + 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. |