diff options
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 252 |
1 files changed, 115 insertions, 137 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 389d8d93..2be4fcac 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -26,6 +26,14 @@ Import ListNotations. Definition exit := node. (* we may generalize this with register renamings at exit, like in "phi" nodes of SSA-form *) +(* inst_info is a ghost record to provide instruction information through oracles *) +Parameter inst_info: Set. +Extract Constant inst_info => "BTLtypes.inst_info". + +(* block_info is a ghost record to provide block information through oracles *) +Parameter block_info: Set. +Extract Constant block_info => "BTLtypes.block_info". + (** final instructions (that stops block execution) *) Inductive final: Type := | Bgoto (succ:exit) (** No operation -- just branch to [succ]. *) @@ -51,16 +59,16 @@ Inductive final: Type := (* instruction block *) Inductive iblock: Type := (* final instructions that stops block execution *) - | BF (fi: final) + | BF (fi: final) (iinfo: inst_info) (* basic instructions that continues block execution, except when aborting *) - | Bnop (* nop instruction *) - | Bop (op:operation) (args:list reg) (dest:reg) + | Bnop (oiinfo: option inst_info) (* nop instruction *) + | Bop (op:operation) (args:list reg) (dest:reg) (iinfo: inst_info) (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *) - | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) + | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) (iinfo: inst_info) (** loads a [chunk] quantity from the address determined by the addressing mode [addr] and the values of the [args] registers, stores the quantity just read into [dest]. If trap=NOTRAP, then failures lead to a default value written to [dest]. *) - | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) + | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) (iinfo: inst_info) (** stores the value of register [src] in the [chunk] quantity at the the address determined by the addressing mode [addr] and the values of the [args] registers. *) @@ -68,13 +76,13 @@ Inductive iblock: Type := | Bseq (b1 b2: iblock) (** starts by running [b1] and stops here if execution of [b1] has reached a final instruction or aborted or continue with [b2] otherwise *) - | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (info:option bool) + | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (iinfo: inst_info) (** evaluates the boolean condition [cond] over the values of registers [args]. If the condition is true, it continues on [ifso]. If the condition is false, it continues on [ifnot]. [info] is a ghost field there to provide information relative to branch prediction. *) . -Coercion BF: final >-> iblock. +Coercion BF: final >-> Funclass. (** NB: - a RTL [(Inop pc)] ending a branch of block is encoded by [(Bseq Bnop (Bgoto pc))]. @@ -87,6 +95,7 @@ Coercion BF: final >-> iblock. Record iblock_info := { entry: iblock; input_regs: Regset.t (* extra liveness information for BTL functional semantics *) + binfo: block_info (* Ghost field used in oracles *) }. Definition code: Type := PTree.t iblock_info. @@ -215,24 +224,24 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := (** 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) - | exec_nop rs m: iblock_istep sp rs m Bnop rs m None - | exec_op rs m op args res v + | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin) +| exec_nop rs m oiinfo: iblock_istep sp rs m (Bnop oiinfo) rs m None + | 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) (rs#res <- v) m None - | exec_load_TRAP rs m chunk addr args dst a 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) (rs#dst <- v) m None + : 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 (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' + | 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') - : iblock_istep sp rs m (Bstore chunk addr args src) rs m' None + : iblock_istep sp rs m (Bstore chunk addr args src iinfo) rs m' None | exec_seq_stop rs m b1 b2 rs' m' fin (EXEC: iblock_istep sp rs m b1 rs' m' (Some fin)) : iblock_istep sp rs m (Bseq b1 b2) rs' m' (Some fin) @@ -240,10 +249,10 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi (EXEC1: iblock_istep sp rs m b1 rs1 m1 None) (EXEC2: iblock_istep sp rs1 m1 b2 rs' m' ofin) : iblock_istep sp rs m (Bseq b1 b2) rs' m' ofin - | exec_cond rs m cond args ifso ifnot i b rs' m' ofin + | exec_cond rs m cond args ifso ifnot b rs' m' ofin iinfo (EVAL: eval_condition cond rs##args m = Some b) (EXEC: iblock_istep sp rs m (if b then ifso else ifnot) rs' m' ofin) - : iblock_istep sp rs m (Bcond cond args ifso ifnot i) rs' m' ofin + : iblock_istep sp rs m (Bcond cond args ifso ifnot iinfo) rs' m' ofin . Local Hint Constructors iblock_istep: core. @@ -252,21 +261,21 @@ Lemma [iblock_istep_run_equiv] below provides a proof that "relation" [iblock_is *) Fixpoint iblock_istep_run sp ib rs m: option outcome := match ib with - | BF fin => + | BF fin _ => Some {| _rs := rs; _m := m; _fin := Some fin |} (* basic instructions *) - | Bnop => + | Bnop _ => Some {| _rs := rs; _m:= m; _fin := None |} - | Bop op args res => + | Bop op args res _ => SOME v <- eval_operation ge sp op rs##args m IN Some {| _rs := rs#res <- v; _m:= m; _fin := None |} - | Bload TRAP chunk addr args dst => + | Bload TRAP chunk addr args dst _ => SOME a <- eval_addressing ge sp addr rs##args IN SOME v <- Mem.loadv chunk m a IN Some {| _rs := rs#dst <- v; _m:= m; _fin := None |} - | Bload NOTRAP chunk addr args dst => + | Bload NOTRAP chunk addr args dst _ => None (* TODO *) - | Bstore chunk addr args src => + | 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 Some {| _rs := rs; _m:= m'; _fin := None |} @@ -887,25 +896,27 @@ Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop := - if [opc] is [Some pc'], this means that all branches of the block that do not exit, join on [pc']. *) Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> iblock -> (option node) -> Prop := - | mib_BF isfst fi pc i: + | mib_BF isfst fi pc i iinfo: cfg!pc = Some i -> match_final_inst dupmap fi i -> - match_iblock dupmap cfg isfst pc (BF fi) None - | mib_nop isfst pc pc': + match_iblock dupmap cfg isfst pc (BF fi iinfo) None + | mib_nop_on_rtl isfst pc pc' iinfo: cfg!pc = Some (Inop pc') -> - match_iblock dupmap cfg isfst pc Bnop (Some pc') - | mib_op isfst pc pc' op lr r: + match_iblock dupmap cfg isfst pc (Bnop (Some iinfo)) (Some pc') + | mib_nop_skip pc: + match_iblock dupmap cfg false pc (Bnop None) (Some pc) + | mib_op isfst pc pc' op lr r iinfo: cfg!pc = Some (Iop op lr r pc') -> - match_iblock dupmap cfg isfst pc (Bop op lr r) (Some pc') - | mib_load isfst pc pc' m a lr r: + match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc') + | mib_load isfst pc pc' m a lr r iinfo: cfg!pc = Some (Iload TRAP m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r) (Some pc') - | mib_store isfst pc pc' m a lr r: + match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc') + | mib_store isfst pc pc' m a lr r iinfo: cfg!pc = Some (Istore m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bstore m a lr r) (Some pc') - | mib_exit pc pc': + match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc') + | mib_exit pc pc' iinfo: dupmap!pc = (Some pc') -> - match_iblock dupmap cfg false pc' (Bgoto pc) None + match_iblock dupmap cfg false pc' (BF (Bgoto pc) iinfo) None (* NB: on RTL side, we exit the block by a "basic" instruction (or Icond). Thus some step should have been executed before [pc'] in the RTL code *) | mib_seq_Some isfst b1 b2 pc1 pc2 opc: @@ -920,12 +931,12 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i And the verifier could fail if there is such dead code! *) *) - | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i i': - cfg!pc = Some (Icond c lr pcso pcnot i') -> + | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i iinfo: + cfg!pc = Some (Icond c lr pcso pcnot i) -> match_iblock dupmap cfg false pcso bso opc1 -> match_iblock dupmap cfg false pcnot bnot opc2 -> is_join_opt opc1 opc2 opc -> - match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i) opc + match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot iinfo) opc . Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := @@ -938,8 +949,8 @@ Local Open Scope error_monad_scope. Definition verify_is_copy dupmap n n' := match dupmap!n with - | None => Error(msg "verify_is_copy None") - | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end + | None => Error(msg "BTL.verify_is_copy None") + | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "BTL.verify_is_copy invalid map") end end. Fixpoint verify_is_copy_list dupmap ln ln' := @@ -947,9 +958,9 @@ Fixpoint verify_is_copy_list dupmap ln ln' := | n::ln => match ln' with | n'::ln' => do _ <- verify_is_copy dupmap n n'; verify_is_copy_list dupmap ln ln' - | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end + | nil => Error (msg "BTL.verify_is_copy_list: ln' bigger than ln") end | nil => match ln' with - | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") + | n :: ln' => Error (msg "BTL.verify_is_copy_list: ln bigger than ln'") | nil => OK tt end end. @@ -998,19 +1009,19 @@ Global Opaque builtin_res_eq_pos. Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := match ib with - | BF fi => + | BF fi _ => match fi with | Bgoto pc1 => do u <- verify_is_copy dupmap pc1 pc; if negb isfst then OK None - else Error (msg "verify_block: isfst is true Bgoto") + else Error (msg "BTL.verify_block: isfst is true Bgoto") | Breturn or => match cfg!pc with | Some (Ireturn or') => if option_eq Pos.eq_dec or or' then OK None - else Error (msg "verify_block: different opt reg in Breturn") - | _ => Error (msg "verify_block: incorrect cfg Breturn") + else Error (msg "BTL.verify_block: different opt reg in Breturn") + | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn") end | Bcall s ri lr r pc1 => match cfg!pc with @@ -1020,11 +1031,11 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (product_eq Pos.eq_dec ident_eq ri ri') then if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK None - else Error (msg "verify_block: different r r' in Bcall") - else Error (msg "verify_block: different lr in Bcall") - else Error (msg "verify_block: different ri in Bcall") - else Error (msg "verify_block: different signatures in Bcall") - | _ => Error (msg "verify_block: incorrect cfg Bcall") + else Error (msg "BTL.verify_block: different r r' in Bcall") + else Error (msg "BTL.verify_block: different lr in Bcall") + else Error (msg "BTL.verify_block: different ri in Bcall") + else Error (msg "BTL.verify_block: different signatures in Bcall") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall") end | Btailcall s ri lr => match cfg!pc with @@ -1032,10 +1043,10 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (signature_eq s s') then if (product_eq Pos.eq_dec ident_eq ri ri') then if (list_eq_dec Pos.eq_dec lr lr') then OK None - else Error (msg "verify_block: different lr in Btailcall") - else Error (msg "verify_block: different ri in Btailcall") - else Error (msg "verify_block: different signatures in Btailcall") - | _ => Error (msg "verify_block: incorrect cfg Btailcall") + else Error (msg "BTL.verify_block: different lr in Btailcall") + else Error (msg "BTL.verify_block: different ri in Btailcall") + else Error (msg "BTL.verify_block: different signatures in Btailcall") + | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall") end | Bbuiltin ef la br pc1 => match cfg!pc with @@ -1044,38 +1055,44 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (external_function_eq ef ef') then if (list_eq_dec builtin_arg_eq_pos la la') then if (builtin_res_eq_pos br br') then OK None - else Error (msg "verify_block: different brr in Bbuiltin") - else Error (msg "verify_block: different lbar in Bbuiltin") - else Error (msg "verify_block: different ef in Bbuiltin") - | _ => Error (msg "verify_block: incorrect cfg Bbuiltin") + else Error (msg "BTL.verify_block: different brr in Bbuiltin") + else Error (msg "BTL.verify_block: different lbar in Bbuiltin") + else Error (msg "BTL.verify_block: different ef in Bbuiltin") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin") end | Bjumptable r ln => match cfg!pc with | Some (Ijumptable r' ln') => do u <- verify_is_copy_list dupmap ln ln'; if (Pos.eq_dec r r') then OK None - else Error (msg "verify_block: different r in Bjumptable") - | _ => Error (msg "verify_block: incorrect cfg Bjumptable") + else Error (msg "BTL.verify_block: different r in Bjumptable") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable") end end - | Bnop => - match cfg!pc with - | Some (Inop pc') => OK (Some pc') - | _ => Error (msg "verify_block: incorrect cfg Bnop") + | Bnop oiinfo => + match oiinfo with + | Some _ => + match cfg!pc with + | Some (Inop pc') => OK (Some pc') + | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop") + end + | None => + if negb isfst then OK (Some pc) + else Error (msg "BTL.verify_block: isfst is true Bnop (on_rtl is false)") end - | Bop op lr r => + | Bop op lr r _ => match cfg!pc with | Some (Iop op' lr' r' pc') => if (eq_operation op op') then if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK (Some pc') - else Error (msg "verify_block: different r in Bop") - else Error (msg "verify_block: different lr in Bop") - else Error (msg "verify_block: different operations in Bop") - | _ => Error (msg "verify_block: incorrect cfg Bop") + else Error (msg "BTL.verify_block: different r in Bop") + else Error (msg "BTL.verify_block: different lr in Bop") + else Error (msg "BTL.verify_block: different operations in Bop") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bop") end - | Bload tm m a lr r => + | Bload tm m a lr r _ => match cfg!pc with | Some (Iload tm' m' a' lr' r' pc') => if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then @@ -1084,34 +1101,34 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK (Some pc') - else Error (msg "verify_block: different r in Bload") - else Error (msg "verify_block: different lr in Bload") - else Error (msg "verify_block: different addressing in Bload") - else Error (msg "verify_block: different mchunk in Bload") - else Error (msg "verify_block: NOTRAP trapping_mode unsupported in Bload") - | _ => Error (msg "verify_block: incorrect cfg Bload") + else Error (msg "BTL.verify_block: different r in Bload") + else Error (msg "BTL.verify_block: different lr in Bload") + else Error (msg "BTL.verify_block: different addressing in Bload") + else Error (msg "BTL.verify_block: different mchunk in Bload") + else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bload") end - | Bstore m a lr r => + | Bstore m a lr r _ => match cfg!pc with | Some (Istore m' a' lr' r' pc') => if (chunk_eq m m') then if (eq_addressing a a') then if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK (Some pc') - else Error (msg "verify_block: different r in Bstore") - else Error (msg "verify_block: different lr in Bstore") - else Error (msg "verify_block: different addressing in Bstore") - else Error (msg "verify_block: different mchunk in Bstore") - | _ => Error (msg "verify_block: incorrect cfg Bstore") + else Error (msg "BTL.verify_block: different r in Bstore") + else Error (msg "BTL.verify_block: different lr in Bstore") + else Error (msg "BTL.verify_block: different addressing in Bstore") + else Error (msg "BTL.verify_block: different mchunk in Bstore") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bstore") end | Bseq b1 b2 => do opc <- verify_block dupmap cfg isfst pc b1; match opc with | Some pc' => verify_block dupmap cfg false pc' b2 - | None => Error (msg "verify_block: None next pc in Bseq (deadcode)") + | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)") end - | Bcond c lr bso bnot i => + | Bcond c lr bso bnot _ => match cfg!pc with | Some (Icond c' lr' pcso pcnot i') => if (list_eq_dec Pos.eq_dec lr lr') then @@ -1123,11 +1140,11 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | o, None => OK o | Some x, Some x' => if Pos.eq_dec x x' then OK (Some x) - else Error (msg "verify_block: is_join_opt incorrect for Bcond") + else Error (msg "BTL.verify_block: is_join_opt incorrect for Bcond") end - else Error (msg "verify_block: incompatible conditions in Bcond") - else Error (msg "verify_block: different lr in Bcond") - | _ => Error (msg "verify_block: incorrect cfg Bcond") + else Error (msg "BTL.verify_block: incompatible conditions in Bcond") + else Error (msg "BTL.verify_block: different lr in Bcond") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bcond") end end. @@ -1178,8 +1195,11 @@ Proof. destruct (Pos.eq_dec _ _); try discriminate. subst. inv EQ0. eapply mib_BF; eauto. constructor; assumption. - (* Bnop *) - destruct i; inv H. - constructor; assumption. + destruct oiinfo; simpl in *. + + destruct (cfg!pc) eqn:EQCFG; try discriminate. + destruct i0; inv H. constructor; assumption. + + destruct isfst; try discriminate. inv H. + constructor; assumption. - (* Bop *) destruct i; try discriminate. destruct (eq_operation _ _); try discriminate. @@ -1228,9 +1248,9 @@ Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit := | Some ib => do o <- verify_block dupmap cfg' true pc' ib.(entry); match o with | None => verify_blocks dupmap cfg cfg' l - | _ => Error(msg "verify_blocks.end") + | _ => Error(msg "BTL.verify_blocks.end") end - | _ => Error(msg "verify_blocks.entry") + | _ => Error(msg "BTL.verify_blocks.entry") end end. @@ -1263,48 +1283,6 @@ Definition verify_function dupmap f f' : res unit := Definition is_goto (ib: iblock): bool := match ib with - | Bgoto _ => true + | BF (Bgoto _) _ => true | _ => false - end. - -Definition is_atom (ib: iblock): bool := - match ib with - | Bseq _ _ | Bcond _ _ _ _ _ => false - | _ => true - end. - -(** Is expand property to only support atomic instructions on the left part of a Bseq *) -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 - | BF fin => fin - | 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. + end.
\ No newline at end of file |