diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-25 13:36:57 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-25 16:00:55 +0200 |
commit | 6938945d80bf16a6de4986e2815113e938bff6c3 (patch) | |
tree | 3ed60831a5f68a677f682224c577a5c777a8f910 | |
parent | 25a4620c95aaa6b017443da29fcf3d033a44a86f (diff) | |
download | compcert-kvx-6938945d80bf16a6de4986e2815113e938bff6c3.tar.gz compcert-kvx-6938945d80bf16a6de4986e2815113e938bff6c3.zip |
starting to experiment SE of fsem
-rw-r--r-- | scheduling/BTL.v | 91 | ||||
-rw-r--r-- | scheduling/BTL_SEtheory.v | 213 |
2 files changed, 232 insertions, 72 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index fb6d5cea..4ae7a6dd 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -159,18 +159,22 @@ Record outcome := out { _fin: option final }. + + + 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 pc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [f] will start. + 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 -> exit -> option reg -> regset -> regset. +Variable tr_exit: function -> list exit -> option reg -> regset -> regset. Variable ge: genv. @@ -282,10 +286,13 @@ Proof. destruct o; try_simplify_someHyps; subst; eauto. Qed. +Import ListNotations. +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) + (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' -> @@ -295,7 +302,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' (tr_exit f pc' (Some res) 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 -> @@ -308,14 +315,14 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop := external_call ef ge vargs m t vres m' -> final_step stack f sp rs m (Bbuiltin ef args res pc') (* TODO: not clear that this is the better choice ! - we coud also do something like [regmap_setres res vres (tr_exit f pc' (reg_builtin_res res) rs)] + we coud also do something like [regmap_setres res vres (tr_exit f [pc'] (reg_builtin_res res) rs)] *) - t (State stack f sp pc' (tr_exit f pc' None (regmap_setres res vres rs)) m') + t (State stack f sp pc' (tr_exit f [pc'] None (regmap_setres res vres rs)) m') | exec_Bjumptable arg tbl n pc': rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> final_step stack f sp rs m (Bjumptable arg tbl) - E0 (State stack f sp pc' (tr_exit f pc' None rs) m) + E0 (State stack f sp pc' (tr_exit f tbl None rs) m) . (** big-step execution of one iblock *) @@ -375,7 +382,7 @@ Inductive final_state: state -> int -> Prop := (** The basic small-step semantics for a BTL program. *) (* tid = transfer_identity *) -Definition tid (_:function) (_:exit) (_: option reg) (rs:regset) := rs. +Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs. Definition semantics (p: program) := Semantics (step tid) (initial_state p) final_state (Genv.globalenv p). @@ -405,19 +412,51 @@ Proof. - rewrite Regmap.gso; auto. Qed. -Definition inputs_exit (f:function) (pc: exit) (or:option reg): Regset.t := - match f.(fn_code)!pc with - | None => Regset.empty - | Some ib => - match or with - | Some r => Regset.remove r ib.(input_regs) - | None => ib.(input_regs) - end +Fixpoint inputs_exitrec (f:function) (tbl: list exit): Regset.t := + match tbl with + | nil => Regset.empty + | pc::l => let rs:= inputs_exitrec f l in + match f.(fn_code)!pc with + | None => rs + | Some ib => Regset.union rs ib.(input_regs) + end end. -Definition tr_inputs (f:function) (pc: exit) (or:option reg): regset -> regset +Lemma inputs_exitrec_In f tbl r: + Regset.In r (inputs_exitrec 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 inputs_exitrec_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 (inputs_exitrec 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. + +Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t := + let rs := inputs_exitrec f tbl in + match or with + | Some r => Regset.remove r rs + | None => rs + end. + +Definition tr_inputs (f:function) (pc: list exit) (or:option reg): regset -> regset := transfer_regs (Regset.elements (inputs_exit f pc 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. @@ -443,6 +482,24 @@ Proof. rewrite -> SetoidList_InA_eq_equiv; eauto. Qed. +Definition Regset_In_dec r rs: + { Regset.In r rs } + { ~(Regset.In r rs)}. +Proof. + destruct (Regset.mem r rs) eqn: IsIN. + + left. abstract (eapply Regset.mem_2; auto). + + right. + abstract (intro H; exploit Regset.mem_1; eauto; congruence). +Defined. + +Lemma tr_inputs_ext f pc or rs1 rs2: + (forall r, Regset.In r (inputs_exit f pc or) -> rs1#r = rs2#r) -> + (forall r, (tr_inputs f pc or rs1)#r = (tr_inputs f pc or rs2)#r). +Proof. + intros EQ r. destruct (Regset_In_dec r (inputs_exit f pc or)). + + rewrite! tr_inputs_exit; eauto. + + rewrite! tr_inputs_dead; eauto. +Qed. + Definition fsem (p: program) := Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p). diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 5125ea3c..fb7c650f 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -28,6 +28,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) @@ -53,6 +54,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 @@ -383,7 +385,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) @@ -397,39 +398,60 @@ Definition sfind_function ctx (svos : sval + ident): option fundef := end . -Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop := - | exec_Sgoto pc rs m: - sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs m) +Import ListNotations. +Local Open Scope list_scope. + +(** [sem_sfval] corresponds to [final_step tr_inputs] for symbolic final value. + + A main difference comes from [rsx] which observes the registers saved in the stackframe + of the returned state. + + Intuitively, only liveout registers are stored in the stack + (others will be associated to [Vundef] value). +*) +Inductive sem_sfval ctx (rsx: reg -> option val): sfval -> regset -> mem -> trace -> state -> Prop := + | exec_Sgoto pc rs rs' m: + rs' = tr_inputs ctx.(cf) [pc] None rs -> + (forall r, rsx r = Some rs'#r) -> + sem_sfval ctx rsx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs' m) | exec_Sreturn stk osv rs m m' v: (csp ctx) = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' -> match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v -> - sem_sfval ctx (Sreturn osv) rs m + (forall r, rsx r = Some Vundef) -> + sem_sfval ctx rsx (Sreturn osv) rs m E0 (Returnstate (cstk ctx) v m') - | exec_Scall rs m sig svos lsv args res pc fd: + | exec_Scall rs m sig svos lsv args res pc fd rs': 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) + rs' = tr_inputs ctx.(cf) [pc] (Some res) rs -> + (forall r, rsx r = Some rs'#r) -> + sem_sfval ctx rsx (Scall sig svos lsv res pc) rs m + E0 (Callstate ((Stackframe res (cf ctx) (csp ctx) pc rs')::cstk ctx) fd args m) | exec_Stailcall stk rs m sig svos args fd m' lsv: sfind_function ctx svos = Some fd -> funsig fd = sig -> (csp ctx) = Vptr stk Ptrofs.zero -> Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' -> eval_list_sval ctx lsv = Some args -> - sem_sfval ctx (Stailcall sig svos lsv) rs m + (forall r, rsx r = Some Vundef) -> + sem_sfval ctx rsx (Stailcall sig svos lsv) rs m E0 (Callstate (cstk ctx) fd args m') - | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs: + | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs rs': seval_builtin_args ctx m sargs vargs -> external_call ef (cge ctx) vargs m t vres m' -> - sem_sfval ctx (Sbuiltin ef sargs res pc) rs m - t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs) m') - | exec_Sjumptable sv tbl pc' n rs m: + rs' = tr_inputs ctx.(cf) [pc] None (regmap_setres res vres rs) -> + (forall r, rsx r = Some rs'#r) -> + sem_sfval ctx rsx (Sbuiltin ef sargs res pc) rs m + t (State (cstk ctx) (cf ctx) (csp ctx) pc rs' m') + | exec_Sjumptable sv tbl pc' n rs m rs': 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) + rs' = tr_inputs ctx.(cf) tbl None rs -> + (forall r, rsx r = Some rs'#r) -> + sem_sfval ctx rsx (Sjumptable sv tbl) rs m + E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs' m) . (** * Preservation properties *) @@ -536,18 +558,18 @@ End SymbValPreserved. 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). +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). (* 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 -> +Lemma sem_sistate_determ ctx sis rs1 m1 rs2 m2: + sem_sistate ctx sis rs1 m1 -> + sem_sistate ctx sis rs2 m2 -> (forall r, rs1#r = rs2#r) /\ m1 = m2. Proof. intros (_&MEM1®1) (_&MEM2®2). @@ -556,6 +578,82 @@ Proof. Qed. (** * Symbolic execution of final step *) +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. + +Lemma transfer_sreg_inputs inputs sreg r: + List.In r inputs -> transfer_sreg inputs sreg r = sreg r. +Proof. + induction inputs; simpl; try autodestruct; intuition congruence. +Qed. + +Lemma transfer_sreg_dead inputs sreg r: + ~List.In r inputs -> transfer_sreg inputs sreg r = Sundef. +Proof. + induction inputs; simpl; try autodestruct; intuition congruence. +Qed. + +Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (inputs_exit f tbl or)). + +Definition transfer_sis (f:function) (tbl: list exit) (or:option reg) (sis: sistate) := + {| si_pre := sis.(si_pre); si_sreg := str_inputs f tbl or 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 transfer_sis_correct ctx sis rs tbl or r: + (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) -> + sreg_eval ctx (transfer_sis (cf ctx) tbl or sis) r = Some (tr_inputs (cf ctx) tbl or rs) # r. +Admitted. + +Local Hint Resolve transfer_sis_correct: core. + +(* TODO: move the 3 below functions in [BTL] ? + Could be reused for liveness checking ? +*) +Definition reg_builtin_res (res: builtin_res reg): option reg := + match res with + | BR r => Some r + | _ => None + end. + +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 sig ros args res pc => tr f [pc] (Some res) + | Btailcall sig ros args => tr f [] None + | Bbuiltin ef args res pc => tr f [pc] (reg_builtin_res res) + | Breturn or => tr f [] None + | Bjumptable reg tbl => tr f tbl None + end. + +Definition tr_regs: function -> final -> regset -> regset := + poly_tr tr_inputs. + +Definition tr_sis: function -> final -> sistate -> sistate := + poly_tr transfer_sis. + +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. + 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). + destruct fin; simpl; econstructor; simpl; intuition eauto. +Qed. + Definition sexec_final_sfv (i: final) (sis: sistate): sfval := match i with | Bgoto pc => Sgoto pc @@ -582,10 +680,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 tid (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. + final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> + sem_sfval ctx (sreg_eval ctx (tr_sis (cf ctx) i sis)) (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. @@ -597,21 +695,20 @@ Proof. - erewrite eval_list_sval_inj; simpl; auto. + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto. eapply seval_builtin_args_correct; eauto. + admit. + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence. -Qed. +Admitted. Local Hint Constructors final_step: core. Local Hint Resolve seval_builtin_args_exact: core. Lemma sexec_final_svf_exact ctx i sis t rs m s: sem_sistate ctx sis rs m -> - sem_sfval ctx (sexec_final_sfv i sis) rs m t s - -> final_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s. + sem_sfval ctx (sreg_eval ctx (tr_sis (cf ctx) i sis)) (sexec_final_sfv i sis) rs m 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. - + (* Bgoto *) - econstructor. + (* Breturn *) enough (v=regmap_optget res Vundef rs) as ->; eauto. destruct res; simpl in *; congruence. @@ -625,8 +722,6 @@ Proof. intros; eapply exec_Btailcall; eauto. destruct fn; simpl in * |- *; auto. rewrite REG in * |- ; auto. - + (* Bbuiltin *) - eapply (exec_Bbuiltin tid); eauto. + (* Bjumptable *) eapply exec_Bjumptable; eauto. congruence. @@ -752,9 +847,10 @@ 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) - (SFV: sem_sfval ctx sfv rs m t s) + | sem_Sfinal sis sfv rs rs' rsx m + (SIS: sem_sistate ctx sis rs' m) + (EXT: forall r, rsx r = Some (rs'#r)) + (SFV: sem_sfval ctx rsx sfv rs m t s) : sem_sstate ctx t s (Sfinal sis sfv) | sem_Scond b cond args sm ifso ifnot (SEVAL: seval_condition ctx cond args sm = Some b) @@ -774,9 +870,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) @@ -785,19 +881,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 @@ -805,16 +901,16 @@ 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 tid (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. (* 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. @@ -822,8 +918,8 @@ Qed. (sexec is a correct over-approximation) *) Theorem sexec_correct ctx ib t s: - iblock_step tid (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. @@ -901,6 +997,9 @@ Proof. - repeat (rewrite Regmap.gso); auto. Qed. +Local Hint Resolve tr_inputs_ext: core. + +(* TODO 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) -> @@ -911,6 +1010,7 @@ Proof. destruct 1; eexists; split; econstructor; eauto. econstructor; eauto. Qed. +*) Local Hint Resolve sexec_final_svf_exact: core. @@ -973,13 +1073,14 @@ Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort sexec_store_preserves_abort: core. Lemma sexec_exclude_abort ctx ib t s1: forall sis k - (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k)) + (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. Proof. induction ib; simpl; intros; eauto. - (* final *) inversion SEXEC; subst; eauto. + admit. - (* load *) destruct trap; eauto. inversion SEXEC. - (* seq *) @@ -988,7 +1089,7 @@ Proof. - (* cond *) inversion SEXEC; subst; eauto. clear SEXEC. destruct b; eauto. -Qed. +Admitted. Lemma set_sreg_abort ctx dst sv sis rs m: sem_sistate ctx sis rs m -> @@ -1048,14 +1149,14 @@ Qed. Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort: core. Lemma sexec_rec_exact ctx ib t s1: forall sis k - (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k)) + (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 tid (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. @@ -1063,11 +1164,13 @@ Proof. induction ib; simpl; intros; eauto. - (* final *) inv SEXEC. + admit. + (* TODO exploit (sem_sistate_determ ctx sis rs m rs0 m0); eauto. intros (REG&MEM); subst. exploit (sem_sfval_equiv rs0 rs); eauto. intros (s2 & EQUIV & SFV'). - eexists; split; eauto. + eexists; split; eauto. *) - (* Bop *) autodestruct; eauto. - destruct trap; [| inv SEXEC ]. repeat autodestruct; eauto. @@ -1093,15 +1196,15 @@ Proof. destruct b. + exploit IHib1; eauto. + exploit IHib2; eauto. -Qed. +Admitted. (* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution (sexec is exact). *) Theorem sexec_exact ctx ib t s1: - sem_sstate ctx t s1 (sexec ib) -> - exists s2, iblock_step tid (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. |