From e30376ce891d0710757c65e85a24e7d2550a37ed Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 27 May 2021 13:49:35 +0200 Subject: cleaning BTL_SEtheory --- scheduling/BTL_SEtheory.v | 304 +++++++++++++++++----------------------------- 1 file changed, 114 insertions(+), 190 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index d6b4e741..79db99c8 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1,20 +1,19 @@ -(* 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. + -(* TODO: A REVOIR - remplacer les [tid] par [tr_inputs] pour montrer la bisimulation avec [fsem] plutôt. *) +*) Require Import Coqlib Maps Floats. 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; @@ -113,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 *) @@ -170,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) @@ -436,105 +435,6 @@ Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop := 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 }. @@ -909,80 +809,8 @@ Proof. rewrite <- REG2, X. auto. 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. -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. - -(* Local Hint Resolve tr_inputs_ext: core. *) -Local Hint Resolve regmap_setres_eq: core. +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 -> @@ -991,11 +819,8 @@ Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s: Proof. unfold str_regs. destruct 1; simpl in *; intros; subst; eexists; split; econstructor; eauto; try congruence. - constructor; eauto. 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 @@ -1125,7 +950,7 @@ 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 (cf ctx) ib sis k)) @@ -1195,7 +1020,7 @@ Proof. inversion SEXEC. Qed. -(** * High-Level specification of the symbolic simulation test as predicate [sstate_simu] *) +(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) Record simu_proof_context := Sctx { sge1: BTL.genv; @@ -1218,12 +1043,14 @@ 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. -Theorem sstate_simu_correct ctx ib1 ib2: - sstate_simu ctx (sexec (sf1 ctx) ib1) (sexec (sf2 ctx) ib2) -> +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 sstate_simu. + unfold symbolic_simu, sstate_simu. intros SIMU t s1 STEP1. exploit (sexec_correct (bctx1 ctx)); simpl; eauto. intros; exploit SIMU; eauto. @@ -1234,3 +1061,100 @@ Proof. 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. -- cgit