diff options
| -rw-r--r-- | backend/AuxTools.ml (renamed from common/AuxTools.ml) | 3 | ||||
| -rw-r--r-- | riscV/ExpansionOracle.ml | 3 | ||||
| -rw-r--r-- | scheduling/BTL.v | 158 | ||||
| -rw-r--r-- | scheduling/BTL_SEtheory.v | 14 | ||||
| -rw-r--r-- | scheduling/BTLaux.ml | 3 | ||||
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 16 | ||||
| -rw-r--r-- | scheduling/PrintBTL.ml | 19 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLaux.ml | 44 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 12 |
9 files changed, 145 insertions, 127 deletions
diff --git a/common/AuxTools.ml b/backend/AuxTools.ml index a667044f..1e334524 100644 --- a/common/AuxTools.ml +++ b/backend/AuxTools.ml @@ -1,5 +1,8 @@ open RTL open Maps +open Camlcoq + +let p2i r = P.to_int r let get_some = function | None -> failwith "Got None instead of Some _" diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 1384b9b3..735f5cf5 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -23,6 +23,7 @@ open Camlcoq open Option open AST open DebugPrint +open AuxTools (** Mini CSE (a dynamic numbering is applied during expansion. The CSE algorithm is inspired by the "static" one used in backend/CSE.v *) @@ -33,8 +34,6 @@ let reg = ref 1 let node = ref 1 -let p2i r = P.to_int r - let r2p () = P.of_int !reg let n2p () = P.of_int !node diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 44c25b75..ca727f82 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -23,29 +23,32 @@ Require Import RTL Op Registers OptionMonad. Definition exit := node. (* we may generalize this with register renamings at exit, like in "phi" nodes of SSA-form *) -(* node_info is a ghost record to provide and transfert information through oracles *) -Record node_info := { - _pos: node -}. +(* inst_info is a ghost record to provide instruction information through oracles *) +Parameter inst_info: Set. +Extract Constant inst_info => "BTLaux.inst_info". + +(* block_info is a ghost record to provide block information through oracles *) +Parameter block_info: Set. +Extract Constant block_info => "BTLaux.block_info". (** final instructions (that stops block execution) *) Inductive final: Type := | Bgoto (succ:exit) (** No operation -- just branch to [succ]. *) - | Breturn (res: option reg) (ni: node_info) + | Breturn (res: option reg) (** terminates the execution of the current function. It returns the value of the given register, or [Vundef] if none is given. *) - | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit) (ni: node_info) + | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit) (** invokes the function determined by [fn] (either a function pointer found in a register or a function name), giving it the values of registers [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) - | Btailcall (sig:signature) (fn: reg + ident) (args: list reg) (ni: node_info) + | Btailcall (sig:signature) (fn: reg + ident) (args: list reg) (** performs a function invocation in tail-call position (the current function terminates after the call, returning the result of the callee) *) - | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit) (ni: node_info) + | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit) (** calls the built-in function identified by [ef], giving it the values of [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) - | Bjumptable (arg:reg) (tbl:list exit) (ni: node_info) + | Bjumptable (arg:reg) (tbl:list exit) (** [Bjumptable arg tbl] transitions to the node that is the [n]-th element of the list [tbl], where [n] is the unsigned integer value of register [arg]. *) . @@ -53,16 +56,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 (ni: node_info) (* nop instruction *) - | Bop (op:operation) (args:list reg) (dest:reg) (ni: node_info) + | Bnop (iinfo: 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) (ni: node_info) + | 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) (ni: node_info) + | 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. *) @@ -70,13 +73,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) (ni: node_info) + | 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))]. @@ -88,7 +91,8 @@ Coercion BF: final >-> iblock. Record iblock_info := { entry: iblock; - input_regs: Regset.t (* extra liveness information ignored by BTL semantics *) + input_regs: Regset.t; (* extra liveness information ignored by BTL semantics *) + binfo: block_info (* Ghost field used in oracles *) }. Definition code: Type := PTree.t iblock_info. @@ -199,24 +203,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 ni: iblock_istep sp rs m (Bnop ni) rs m None - | exec_op rs m op args res v ni + | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin) + | exec_nop rs m iinfo: iblock_istep sp rs m (Bnop iinfo) 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 ni) (rs#res <- v) m None - | exec_load_TRAP rs m chunk addr args dst a v ni + : 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 ni) (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' ni + | 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 ni) 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) @@ -224,10 +228,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 ni + | 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 ni) rs' m' ofin + : iblock_istep sp rs m (Bcond cond args ifso ifnot iinfo) rs' m' ofin . Local Hint Constructors iblock_istep: core. @@ -236,7 +240,7 @@ 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 _ => @@ -261,7 +265,7 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome := | None => iblock_istep_run sp b2 out1.(_rs) out1.(_m) | _ => Some out1 (* stop execution on the 1st final instruction *) end - | Bcond cond args ifso ifnot _ _ => + | Bcond cond args ifso ifnot _ => SOME b <- eval_condition cond rs##args m IN iblock_istep_run sp (if b then ifso else ifnot) rs m end. @@ -280,32 +284,32 @@ 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 rs m) - | exec_Breturn or stk m' ni: + | exec_Breturn or stk m': sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - final_step stack f sp rs m (Breturn or ni) + final_step stack f sp rs m (Breturn or) E0 (Returnstate stack (regmap_optget or Vundef rs) m') - | exec_Bcall sig ros args res pc' fd ni: + | exec_Bcall sig ros args res pc' fd: find_function ros rs = Some fd -> funsig fd = sig -> - final_step stack f sp rs m (Bcall sig ros args res pc' ni) + final_step stack f sp rs m (Bcall sig ros args res pc') E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m) - | exec_Btailcall sig ros args stk m' fd ni: + | exec_Btailcall sig ros args stk m' fd: find_function ros rs = Some fd -> funsig fd = sig -> sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - final_step stack f sp rs m (Btailcall sig ros args ni) + final_step stack f sp rs m (Btailcall sig ros args) E0 (Callstate stack fd rs##args m') - | exec_Bbuiltin ef args res pc' vargs t vres m' ni: + | exec_Bbuiltin ef args res pc' vargs t vres m': eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> - final_step stack f sp rs m (Bbuiltin ef args res pc' ni) + final_step stack f sp rs m (Bbuiltin ef args res pc') t (State stack f sp pc' (regmap_setres res vres rs) m') - | exec_Bjumptable arg tbl n pc' ni: + | 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 ni) + final_step stack f sp rs m (Bjumptable arg tbl) E0 (State stack f sp pc' rs m) . @@ -393,16 +397,16 @@ Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop | mfi_goto pc pc': dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc') *) - | mfi_return or ni: match_final_inst dupmap (Breturn or ni) (Ireturn or) - | mfi_call pc pc' s ri lr r ni: - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc ni) (Icall s ri lr r pc') - | mfi_tailcall s ri lr ni: - match_final_inst dupmap (Btailcall s ri lr ni) (Itailcall s ri lr) - | mfi_builtin pc pc' ef la br ni: - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc ni) (Ibuiltin ef la br pc') - | mfi_jumptable ln ln' r ni: + | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or) + | mfi_call pc pc' s ri lr r: + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc') + | mfi_tailcall s ri lr: + match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr) + | mfi_builtin pc pc' ef la br: + dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc') + | mfi_jumptable ln ln' r: list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' -> - match_final_inst dupmap (Bjumptable r ln ni) (Ijumptable r ln') + match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln') . Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop := @@ -417,25 +421,25 @@ 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' ni: + match_iblock dupmap cfg isfst pc (BF fi iinfo) None + | mib_nop isfst pc pc' iinfo: cfg!pc = Some (Inop pc') -> - match_iblock dupmap cfg isfst pc (Bnop ni) (Some pc') - | mib_op isfst pc pc' op lr r ni: + match_iblock dupmap cfg isfst pc (Bnop iinfo) (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 ni) (Some pc') - | mib_load isfst pc pc' m a lr r ni: + 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 ni) (Some pc') - | mib_store isfst pc pc' m a lr r ni: + 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 ni) (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: @@ -450,12 +454,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' ni: - 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 ni) opc + match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot iinfo) opc . Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := @@ -528,21 +532,21 @@ 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 "BTL.verify_block: isfst is true Bgoto") - | Breturn or _ => + | Breturn or => match cfg!pc with | Some (Ireturn or') => if option_eq Pos.eq_dec or or' then OK None 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 _ => + | Bcall s ri lr r pc1 => match cfg!pc with | Some (Icall s' ri' lr' r' pc2) => do u <- verify_is_copy dupmap pc1 pc2; @@ -556,7 +560,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different signatures in Bcall") | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall") end - | Btailcall s ri lr _ => + | Btailcall s ri lr => match cfg!pc with | Some (Itailcall s' ri' lr') => if (signature_eq s s') then @@ -567,7 +571,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different signatures in Btailcall") | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall") end - | Bbuiltin ef la br pc1 _ => + | Bbuiltin ef la br pc1 => match cfg!pc with | Some (Ibuiltin ef' la' br' pc2) => do u <- verify_is_copy dupmap pc1 pc2; @@ -579,7 +583,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different ef in Bbuiltin") | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin") end - | Bjumptable r ln _ => + | Bjumptable r ln => match cfg!pc with | Some (Ijumptable r' ln') => do u <- verify_is_copy_list dupmap ln ln'; @@ -641,7 +645,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) verify_block dupmap cfg false pc' b2 | 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 @@ -793,13 +797,13 @@ 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 + | Bseq _ _ | Bcond _ _ _ _ _ => false | _ => true end. @@ -809,10 +813,10 @@ Inductive is_expand: iblock -> Prop := is_atom ib1 = true -> is_expand ib2 -> is_expand (Bseq ib1 ib2) - | exp_Bcond cond args ib1 ib2 i ni: + | exp_Bcond cond args ib1 ib2 iinfo: is_expand ib1 -> is_expand ib2 -> - is_expand (Bcond cond args ib1 ib2 i ni) + is_expand (Bcond cond args ib1 ib2 iinfo) | exp_others ib: is_atom ib = true -> is_expand ib @@ -822,9 +826,9 @@ 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 ni => - Bcond cond args (expand ib1 k) (expand ib2 k) i ni - | BF fin => fin + | Bcond cond args ib1 ib2 iinfo => + Bcond cond args (expand ib1 k) (expand ib2 k) iinfo + | BF fin iinfo => BF fin iinfo | ib => match k with | None => ib diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 94d299e7..cd69cd37 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -557,21 +557,21 @@ Qed. Definition sexec_final_sfv (i: final) (sis: sistate): sfval := match i with | Bgoto pc => Sgoto pc - | Bcall sig ros args res pc _ => + | Bcall sig ros args res pc => let svos := sum_left_map sis.(si_sreg) ros in let sargs := list_sval_inj (List.map sis.(si_sreg) args) in Scall sig svos sargs res pc - | Btailcall sig ros args _ => + | Btailcall sig ros args => let svos := sum_left_map sis.(si_sreg) ros in let sargs := list_sval_inj (List.map sis.(si_sreg) args) in Stailcall sig svos sargs - | Bbuiltin ef args res pc _ => + | Bbuiltin ef args res pc => let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in Sbuiltin ef sargs res pc - | Breturn or _ => + | Breturn or => let sor := SOME r <- or IN Some (sis.(si_sreg) r) in Sreturn sor - | Bjumptable reg tbl _ => + | Bjumptable reg tbl => let sv := sis.(si_sreg) reg in Sjumptable sv tbl end. @@ -770,7 +770,7 @@ pour représenter l'ensemble des chemins. Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := match ib with - | BF fin => Sfinal sis (sexec_final_sfv fin sis) + | 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) @@ -780,7 +780,7 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := (* composed instructions *) | Bseq ib1 ib2 => sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) - | Bcond cond args ifso ifnot _ _ => + | 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 diff --git a/scheduling/BTLaux.ml b/scheduling/BTLaux.ml new file mode 100644 index 00000000..e8e355b1 --- /dev/null +++ b/scheduling/BTLaux.ml @@ -0,0 +1,3 @@ +type inst_info = { mutable inumb : int; mutable pcond : bool option } + +type block_info = { mutable bnumb : int } diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 6c894b78..9b37d8fa 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -221,7 +221,7 @@ Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin match ofin with | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) | Some fin => - exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin None + exists isfst' pc1 iinfo, match_iblock dupmap (RTL.fn_code f') isfst' pc1 (BF fin iinfo) None /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) end. Proof. @@ -255,7 +255,7 @@ Proof. intros (pc1 & EQpc1 & STEP1); inv EQpc1. exploit IHIBIS2; eauto. destruct ofin; simpl. - + intros (ifst2 & pc2 & M2 & STEP2). + + intros (ifst2 & pc2 & iinfo & M2 & STEP2). repeat eexists; eauto. eapply css_plus_trans; eauto. + intros (pc2 & EQpc2 & STEP2); inv EQpc2. @@ -263,12 +263,12 @@ Proof. eapply plus_trans; eauto. - (* exec_cond *) inv MIB. - rename H11 into JOIN. (* is_join_opt opc1 opc2 opc *) + rename H10 into JOIN. (* is_join_opt opc1 opc2 opc *) destruct b; exploit IHIBIS; eauto. + (* taking ifso *) destruct ofin; simpl. * (* ofin is Some final *) - intros (isfst' & pc1 & MI & STAR). + intros (isfst' & pc1 & iinfo' & MI & STAR). repeat eexists; eauto. eapply css_plus_trans; eauto. * (* ofin is None *) @@ -279,7 +279,7 @@ Proof. + (* taking ifnot *) destruct ofin; simpl. * (* ofin is Some final *) - intros (isfst' & pc1 & MI & STAR). + intros (isfst' & pc1 & iinfo' & MI & STAR). repeat eexists; eauto. eapply css_plus_trans; eauto. * (* ofin is None *) @@ -305,14 +305,14 @@ Proof. erewrite <- preserv_fnstacksize; eauto. econstructor; eauto. - (* call *) - rename H8 into FIND. + rename H7 into FIND. exploit find_function_preserved; eauto. intros (fd' & FIND' & TRANSFU). eexists; split. eapply exec_Icall; eauto. apply function_sig_translated. assumption. repeat (econstructor; eauto). - (* tailcall *) - rename H3 into FIND. + rename H2 into FIND. exploit find_function_preserved; eauto. intros (fd' & FIND' & TRANSFU). eexists; split. eapply exec_Itailcall; eauto. @@ -342,7 +342,7 @@ Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fi : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'. Proof. intros; exploit iblock_istep_simulation; eauto. - simpl. intros (isfst' & pc1 & MI & STAR). clear IBIS MIB. + simpl. intros (isfst' & pc1 & iinfo & MI & STAR). clear IBIS MIB. inv MI. - (* final inst except goto *) exploit final_simu_except_goto; eauto. diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml index 4b14d28e..23ad91f6 100644 --- a/scheduling/PrintBTL.ml +++ b/scheduling/PrintBTL.ml @@ -5,6 +5,7 @@ open Maps open AST open BTL open PrintAST +open BTLaux (* Printing of BTL code *) @@ -43,24 +44,24 @@ let rec print_iblock pp is_rec pref ib = fprintf pp "Bstore: %s[%a] = %a\n" (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) reg src - | BF (Bcall (sg, fn, args, res, s, _)) -> + | BF (Bcall (sg, fn, args, res, s), _) -> print_pref pp pref; fprintf pp "Bcall: %a = %a(%a)\n" reg res ros fn regs args; print_succ pp s - | BF (Btailcall (sg, fn, args, _)) -> + | BF (Btailcall (sg, fn, args), _) -> print_pref pp pref; fprintf pp "Btailcall: %a(%a)\n" ros fn regs args - | BF (Bbuiltin (ef, args, res, s, _)) -> + | BF (Bbuiltin (ef, args, res, s), _) -> print_pref pp pref; fprintf pp "Bbuiltin: %a = %s(%a)\n" (print_builtin_res reg) res (name_of_external ef) (print_builtin_args reg) args; print_succ pp s - | Bcond (cond, args, ib1, ib2, info, _) -> + | Bcond (cond, args, ib1, ib2, iinfo) -> print_pref pp pref; fprintf pp "Bcond: (%a) (prediction: %s)\n" (PrintOp.print_condition reg) (cond, args) - (match info with + (match iinfo.pcond with | None -> "none" | Some true -> "branch" | Some false -> "fallthrough"); @@ -71,20 +72,20 @@ let rec print_iblock pp is_rec pref ib = fprintf pp "%sifnot = [\n" pref; if is_rec then print_iblock pp is_rec pref' ib2 else fprintf pp "...\n"; fprintf pp "%s]\n" pref - | BF (Bjumptable (arg, tbl, _)) -> + | BF (Bjumptable (arg, tbl), _) -> let tbl = Array.of_list tbl in print_pref pp pref; fprintf pp "Bjumptable: (%a)\n" reg arg; for i = 0 to Array.length tbl - 1 do fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i)) done - | BF (Breturn (None, _)) -> + | BF (Breturn None, _) -> print_pref pp pref; fprintf pp "Breturn\n" - | BF (Breturn (Some arg, _)) -> + | BF (Breturn (Some arg), _) -> print_pref pp pref; fprintf pp "Breturn: %a\n" reg arg - | BF (Bgoto s) -> + | BF (Bgoto s, _) -> print_pref pp pref; fprintf pp "Bgoto: %d\n" (P.to_int s) | Bseq (ib1, ib2) -> diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index 859bbf07..d4fd2643 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -6,37 +6,43 @@ open DebugPrint open PrintBTL open Camlcoq open AuxTools +open BTLaux -let mk_ni n = n +let undef_node = -1 +let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond } +let def_iinfo = { inumb = undef_node; pcond = None } + +let mk_binfo _bnumb = { bnumb = _bnumb } let encaps_final inst osucc = match inst with | BF _ | Bcond _ -> inst - | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc))) + | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo)) -let translate_inst ni inst is_final = +let translate_inst iinfo inst is_final = let osucc = ref None in let btli = match inst with | Inop s -> osucc := Some s; - Bnop ni + Bnop iinfo | Iop (op, lr, rd, s) -> osucc := Some s; - Bop (op, lr, rd, ni) + Bop (op, lr, rd, iinfo) | Iload (trap, chk, addr, lr, rd, s) -> osucc := Some s; - Bload (trap, chk, addr, lr, rd, ni) + Bload (trap, chk, addr, lr, rd, iinfo) | Istore (chk, addr, lr, rd, s) -> osucc := Some s; - Bstore (chk, addr, lr, rd, ni) - | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s, ni)) - | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr, ni)) - | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s, ni)) + Bstore (chk, addr, lr, rd, iinfo) + | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s), iinfo) + | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr), iinfo) + | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo) | Icond (cond, lr, ifso, ifnot, info) -> - Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info, ni) - | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl, ni)) - | Ireturn oreg -> BF (Breturn (oreg, ni)) + iinfo.pcond <- info; + Bcond (cond, lr, BF (Bgoto ifso, def_iinfo), BF (Bgoto ifnot, def_iinfo), iinfo) + | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl), iinfo) + | Ireturn oreg -> BF (Breturn (oreg), iinfo) in if is_final then encaps_final btli !osucc else btli @@ -52,7 +58,7 @@ let translate_function code entry join_points = let rec build_btl_block n = let inst = get_some @@ PTree.get n code in let psucc = predicted_successor inst in - let ni = mk_ni n in + let iinfo = mk_iinfo (p2i n) None in let succ = match psucc with | Some ps -> @@ -70,16 +76,18 @@ let translate_function code entry join_points = (* TODO gourdinl remove this *) assert (s = ifnot); next_nodes := !next_nodes @ non_predicted_successors inst psucc; - Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info, ni) - | _ -> Bseq (translate_inst ni inst false, build_btl_block s)) + iinfo.pcond <- info; + Bcond (cond, lr, BF (Bgoto ifso, def_iinfo), build_btl_block s, iinfo) + | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s)) | None -> debug "BLOCK END.\n"; next_nodes := !next_nodes @ successors_inst inst; - translate_inst ni inst true + translate_inst iinfo inst true in let ib = build_btl_block e in let succs = !next_nodes in - let ibf = { entry = ib; input_regs = Regset.empty } in + let bi = mk_binfo (p2i e) in + let ibf = { entry = ib; input_regs = Regset.empty; binfo = bi } in btl_code := PTree.set e ibf !btl_code; List.iter build_btl_tree succs) in diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 6681d691..7ad1472b 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -215,7 +215,7 @@ type defined below. Intuitively, each RTL step corresponds to either Fixpoint measure ib: nat := match ib with | Bseq ib1 ib2 - | Bcond _ _ ib1 ib2 _ _ => measure ib1 + measure ib2 + | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2 | ib => 1 end. @@ -238,7 +238,7 @@ Lemma entry_isnt_goto dupmap f pc ib: Proof. intros. destruct (entry ib); trivial. - destruct fi; trivial. inv H. inv H4. + destruct fi; trivial. inv H. inv H5. Qed. Lemma expand_entry_isnt_goto dupmap f pc ib: @@ -248,7 +248,7 @@ Proof. destruct (is_goto (expand (entry ib) None))eqn:EQG; destruct (expand (entry ib) None); try destruct fi; try discriminate; trivial. - intros; inv H; inv H4. + intros; inv H; inv H5. Qed. Lemma list_nth_z_rev_dupmap: @@ -499,10 +499,10 @@ Proof. destruct (is_goto ib2) eqn:GT. destruct ib2; try destruct fi; try discriminate. - (* Bgoto *) - inv MSS2. inversion MIB; subst; try inv H3. - remember H0 as ODUPLIC; clear HeqODUPLIC. + inv MSS2. inversion MIB; subst; try inv H4. + remember H2 as ODUPLIC; clear HeqODUPLIC. eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. - apply DMC in H0 as [ib [FNC MI]]; clear DMC. + apply DMC in H2 as [ib [FNC MI]]; clear DMC. eexists; left; eexists; split. + repeat econstructor; eauto. apply iblock_istep_run_equiv in BTL_RUN; eauto. |