diff options
-rw-r--r-- | scheduling/BTL.v | 88 | ||||
-rw-r--r-- | scheduling/BTL_SEtheory.v | 292 | ||||
-rw-r--r-- | scheduling/RTLtoBTL.v | 3 | ||||
-rw-r--r-- | scheduling/RTLtoBTLproof.v | 2 |
4 files changed, 372 insertions, 13 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index c8dfa0af..d7ffa118 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -175,6 +175,23 @@ Definition find_function (ros: reg + ident) (rs: regset) : option fundef := Local Open Scope option_monad_scope. +(* (* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *) + +Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := + | has_loaded_normal a trap + (EVAL: eval_addressing ge sp addr rs##args = Some a) + (LOAD: Mem.loadv chunk m a = Some v) + : has_loaded sp rs m chunk addr args v trap + | has_loaded_default + (LOAD: forall a, eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = None) + (DEFAULT: v = default_notrap_load_value chunk) + : has_loaded sp rs m chunk addr args v NOTRAP + . + +(* TODO: move this scheme in "Memory" module if this scheme is useful ! *) + +*) + (** internal big-step execution of one iblock *) Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := | exec_final rs m fin: iblock_istep sp rs m (BF fin) rs m (Some fin) @@ -186,6 +203,11 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi (EVAL: eval_addressing ge sp addr rs##args = Some a) (LOAD: Mem.loadv chunk m a = Some v) : iblock_istep sp rs m (Bload TRAP chunk addr args dst) (rs#dst <- v) m None +(* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above + | exec_load rs m trap chunk addr args dst v + (LOAD: has_loaded sp rs m chunk addr args v trap) + : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None +*) | exec_store rs m chunk addr args src a m' (EVAL: eval_addressing ge sp addr rs##args = Some a) (STORE: Mem.storev chunk m a rs#src = Some m') @@ -764,11 +786,6 @@ Definition verify_function dupmap f f' : res unit := do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); verify_cfg dupmap (fn_code f) (RTL.fn_code f'). -Definition is_seq (ib: iblock): bool := - match ib with - | Bseq _ _ => true - | _ => false - end. Definition is_atom (ib: iblock): bool := match ib with @@ -776,6 +793,67 @@ Definition is_atom (ib: iblock): bool := | _ => true end. +Inductive is_expand: iblock -> Prop := + | exp_Bseq ib1 ib2: + is_atom ib1 = true -> + is_expand ib2 -> + is_expand (Bseq ib1 ib2) + | exp_Bcond cond args ib1 ib2 i: + is_expand ib1 -> + is_expand ib2 -> + is_expand (Bcond cond args ib1 ib2 i) + | exp_others ib: + is_atom ib = true -> + is_expand ib + . +Local Hint Constructors is_expand: core. + +Fixpoint expand (ib: iblock) (k: option iblock): iblock := + match ib with + | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k)) + | Bcond cond args ib1 ib2 i => + Bcond cond args (expand ib1 k) (expand ib2 k) i + | ib => + match k with + | None => ib + | Some rem => Bseq ib rem + end + end. + +Lemma expand_correct ib: forall k, + (match k with Some rem => is_expand rem | None => True end) + -> is_expand (expand ib k). +Proof. + induction ib; simpl; intros; try autodestruct; auto. +Qed. + +Lemma expand_None_correct ib: + is_expand (expand ib None). +Proof. + apply expand_correct; simpl; auto. +Qed. + +Definition expand_code (cfg: code): code := + (PTree.map (fun _ ib => {| entry:=expand ib.(entry) None; input_regs := ib.(input_regs) |}) cfg). + +Lemma expand_code_correct cfg pc ib : + (expand_code cfg)!pc=Some ib -> is_expand (ib.(entry)). +Proof. + unfold expand_code. + rewrite PTree.gmap. + destruct (cfg!pc); simpl; intros; try_simplify_someHyps. + apply expand_None_correct; auto. +Qed. + + +(* TODO: eliminer toute la suite quand "right_assoc" sera remplace par "expand" *) + +Definition is_seq (ib: iblock): bool := + match ib with + | Bseq _ _ => true + | _ => false + end. + Inductive is_right_assoc: iblock -> Prop := | ira_Bseq ib1 ib2: diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 7025b90c..0a2c0a04 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -13,12 +13,11 @@ Require Import RTL BTL OptionMonad. 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 := { +Record iblock_exec_context := Bctx { cge: BTL.genv; - csp: val; cstk: list stackframe; cf: function; + csp: val; crs0: regset; cm0: mem }. @@ -431,6 +430,103 @@ Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop := E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' 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 *) @@ -521,19 +617,199 @@ 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 |}. + +Lemma sis_init_correct ctx: + sem_sistate ctx sis_init (crs0 ctx) (cm0 ctx). +Proof. + unfold sis_init, sem_sistate; simpl; intuition eauto. +Qed. + +Definition set_sreg (r:reg) (sv:sval) (sis:sistate): sistate := + {| si_pre:=(fun ctx => eval_sval ctx (sis.(si_sreg) r) <> None /\ (sis.(si_pre) ctx)); + si_sreg:=fun y => if Pos.eq_dec r y then sv else sis.(si_sreg) y; + si_smem:= sis.(si_smem)|}. + +Lemma set_sreg_correct ctx dst sv sis (rs rs': regset) m: + sem_sistate ctx sis rs m -> + (eval_sval ctx sv = Some rs' # dst) -> + (forall r, r <> dst -> rs'#r = rs#r) -> + sem_sistate ctx (set_sreg dst sv sis) rs' m. +Proof. + intros (PRE&MEM®) NEW OLD. + unfold sem_sistate, set_sreg; simpl. + intuition. + - rewrite REG in *; congruence. + - destruct (Pos.eq_dec dst r); simpl; subst; eauto. + rewrite REG in *. rewrite OLD; eauto. +Qed. + +Definition set_smem (sm:smem) (sis:sistate): sistate := + {| si_pre:=(fun ctx => eval_smem ctx sis.(si_smem) <> None /\ (sis.(si_pre) ctx)); + si_sreg:= sis.(si_sreg); + si_smem:= sm |}. + +Lemma set_smem_correct ctx sm sis rs m m': + sem_sistate ctx sis rs m -> + eval_smem ctx sm = Some m' -> + sem_sistate ctx (set_smem sm sis) rs m'. +Proof. + intros (PRE&MEM®) NEW. + unfold sem_sistate, set_smem; simpl. + intuition. + rewrite MEM in *; congruence. +Qed. + +Definition sexec_op op args dst sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + set_sreg dst (Sop op args sis.(si_smem)) sis. + +Lemma sexec_op_correct ctx op args dst sis rs m v + (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = Some v) + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_op op args dst sis) (rs#dst <- v) m). +Proof. + eapply set_sreg_correct; eauto. + - simpl. destruct SIS as (PRE&MEM®). + rewrite Regmap.gss; simpl; auto. + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + - intros; rewrite Regmap.gso; auto. +Qed. + +Definition sexec_load trap chunk addr args dst sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + set_sreg dst (Sload sis.(si_smem) trap chunk addr args) sis. + +Lemma sexec_load_TRAP_correct ctx chunk addr args dst sis rs m a v + (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a) + (LOAD: Mem.loadv chunk m a = Some v) + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_load TRAP chunk addr args dst sis) (rs#dst <- v) m). +Proof. + eapply set_sreg_correct; eauto. + - simpl. destruct SIS as (PRE&MEM®). + rewrite Regmap.gss; simpl; auto. + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + - intros; rewrite Regmap.gso; auto. +Qed. + +Definition sexec_store chunk addr args src sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + let src := sis.(si_sreg) src in + let sm := Sstore sis.(si_smem) chunk addr args src in + set_smem sm sis. + +Lemma sexec_store_correct ctx chunk addr args src sis rs m m' a + (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a) + (STORE: Mem.storev chunk m a (rs # src) = Some m') + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_store chunk addr args src sis) rs m'). +Proof. + eapply set_smem_correct; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + rewrite REG; auto. +Qed. + +Lemma seval_condition_eq ctx cond args sis rs m + (SIS : sem_sistate ctx sis rs m) + :seval_condition ctx cond (list_sval_inj (map (si_sreg sis) args)) (si_smem sis) = eval_condition cond rs ## args m. +Proof. + destruct SIS as (PRE&MEM®); unfold seval_condition; simpl. + erewrite eval_list_sval_inj; simpl; auto. + erewrite MEM; auto. +Qed. + +(** * symbolic execution of blocks *) + (* symbolic state *) Inductive sstate := | Sfinal (sis: sistate) (sfv: sfval) | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate) + | Sabort . -Inductive sem_internal_sstate ctx rs m t s: sstate -> Prop := - | sem_Sfinal sis sfv +(* 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_internal_sstate ctx rs m t s (Sfinal sis sfv) + : 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) - (SELECT: sem_internal_sstate ctx rs m t s (if b then ifso else ifnot)) - : sem_internal_sstate ctx rs m t s (Scond cond args sm ifso ifnot) + (SELECT: sem_sstate ctx t s (if b then ifso else ifnot)) + : sem_sstate ctx t s (Scond cond args sm ifso ifnot) + (* NB: Sabort: fails to produce a transition *) + . + +(** * Idée de l'execution symbolique en Continuation Passing Style + +[k] ci-dessous est la continuation (c-a-d. la suite de la construction de l'arbre qu'on va appliquer dans chaque branche) + +Rem: si manipuler une telle continuation s'avère compliqué dans les preuves, +il faudra faire autrement dans le modèle -- par exemple avec une structure de donnée +pour représenter l'ensemble des chemins. +(même si on peut conserver le CPS dans l'implem finale, pour l'efficacité). + +*) + +Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := + match ib with + | BF fin => Sfinal sis (sexec_final_sfv fin sis) + (* basic instructions *) + | Bnop => k sis + | Bop op args res => k (sexec_op op args res sis) + | Bload TRAP chunk addr args dst => k (sexec_load TRAP chunk addr args dst sis) + | Bload NOTRAP chunk addr args dst => Sabort (* TODO *) + | 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) + | 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 + Scond cond args sis.(si_smem) ifso ifnot + end . + +Definition sexec ib := sexec_rec ib sis_init (fun _ => Sabort). + +Local Hint Constructors sem_sstate: core. +Local Hint Resolve sexec_op_correct sexec_final_svf_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 + (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): forall sis k + (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 + end), + sem_sstate ctx t s (sexec_rec 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); + 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). +Proof. + destruct 1 as (rs' & m' & fin & ISTEP & FSTEP). + eapply sexec_rec_correct; simpl; eauto. +Qed. diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v index 14aecb21..2b2bd15c 100644 --- a/scheduling/RTLtoBTL.v +++ b/scheduling/RTLtoBTL.v @@ -12,6 +12,9 @@ Local Open Scope error_monad_scope. Definition transf_function (f: RTL.function) : res BTL.function := let (tcte, dupmap) := rtl2btl f in let (tc, te) := tcte in + (* TODO, pour finir la preuve: remplacer ci-dessous "right_assoc_code" par "expand_code" + on s'arrangera pour éliminer cette transformation "coûteuse" à la fin ! + *) let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) (right_assoc_code tc) te in do u <- verify_function dupmap f' f; OK f'. diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 1db088d2..efc22eb6 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -6,6 +6,8 @@ Require Import Errors Linking RTLtoBTL. Require Import Linking. +(* TODO: remplacer "right_assoc" par "expand" ci-dessous *) + Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := { dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f); dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f); |