diff options
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 51 |
1 files changed, 38 insertions, 13 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 6536addb..96377943 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -205,7 +205,7 @@ 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 *) +(* 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 @@ -217,11 +217,10 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := (DEFAULT: v = default_notrap_load_value chunk) : has_loaded sp rs m chunk addr args v NOTRAP . +Local Hint Constructors has_loaded: core. (* TODO: move this scheme in "Memory" module if this scheme is useful ! *) -*) - (** internal big-step execution of one iblock *) Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin) @@ -229,15 +228,9 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi | exec_op rs m op args res v iinfo (EVAL: eval_operation ge sp op rs##args m = Some v) : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None - | exec_load_TRAP rs m chunk addr args dst a v iinfo - (EVAL: eval_addressing ge sp addr rs##args = Some a) - (LOAD: Mem.loadv chunk m a = Some v) - : iblock_istep sp rs m (Bload TRAP chunk addr args dst iinfo) (rs#dst <- v) m None -(* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above - | exec_load rs m trap chunk addr args dst v + | exec_load rs m trap chunk addr args dst v iinfo (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 -*) + : iblock_istep sp rs m (Bload trap chunk addr args dst iinfo) (rs#dst <- v) m None | exec_store rs m chunk addr args src a m' iinfo (EVAL: eval_addressing ge sp addr rs##args = Some a) (STORE: Mem.storev chunk m a rs#src = Some m') @@ -274,7 +267,18 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome := SOME v <- Mem.loadv chunk m a IN Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} | Bload NOTRAP chunk addr args dst _ => - None (* TODO *) + match eval_addressing ge sp addr rs##args with + | Some a => + match Mem.loadv chunk m a with + | Some v => Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + | None => + let v := default_notrap_load_value chunk in + Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + end + | None => + let v := default_notrap_load_value chunk in + Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} + end | Bstore chunk addr args src _ => SOME a <- eval_addressing ge sp addr rs##args IN SOME m' <- Mem.storev chunk m a rs#src IN @@ -291,13 +295,34 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome := iblock_istep_run sp (if b then ifso else ifnot) rs m end. +Lemma iblock_istep_run_equiv_load sp ib v rs rs' m trap chunk addr args dst iinfo ofin: + ib = (Bload trap chunk addr args dst iinfo) -> + rs' = rs # dst <- v -> + has_loaded sp rs m chunk addr args v trap -> + iblock_istep sp rs m ib rs' m ofin <-> + iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m := m; _fin := ofin |}. +Proof. + split; subst; inv H1; simpl in *; intros. + - destruct trap; inv H; simpl in *; repeat autodestruct. + - inv H; autodestruct; rewrite LOAD; auto. + - destruct trap; inv H; simpl in *; + rewrite EVAL, LOAD in H1; inv H1; repeat econstructor; eauto. + - generalize H; autodestruct. + + rewrite LOAD in *; inv H; auto; constructor. + eapply has_loaded_default; eauto; try_simplify_someHyps. + + inv H; constructor. eapply has_loaded_default; eauto; try_simplify_someHyps. +Qed. +Local Hint Resolve iblock_istep_run_equiv_load: core. + Lemma iblock_istep_run_equiv sp rs m ib rs' m' ofin: iblock_istep sp rs m ib rs' m' ofin <-> iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m:= m'; _fin := ofin |}. Proof. constructor. - - induction 1; simpl; try autodestruct; try_simplify_someHyps. + - induction 1; try (eapply iblock_istep_run_equiv_load; eauto; fail); + simpl; try autodestruct; try_simplify_someHyps. - generalize rs m rs' m' ofin; clear rs m rs' m' ofin. induction ib; simpl; repeat (try autodestruct; try_simplify_someHyps). + 1,2: constructor; eapply has_loaded_default; try_simplify_someHyps. destruct o; try_simplify_someHyps; subst; eauto. Qed. |