Module BTL_BlockOptimizer.StoreMotionOracle2

module StoreMotionOracle2: StoreMotionOracle.Make(StoreMotionOracle.StPartial)

type btr3 = unit -> St.t * BTL.iblock

type btr2 = St.s -> btr3

type btr1 = unit -> St.t * btr2

type btr0 = St.t -> btr1

type ibtr3 = unit -> BTL.iblock

type ibtr2 = St.s -> St.s * ibtr3

type ibtr1 = unit -> ibtr2

type ibtr0 = St.t ->
       (St.t, St.t) StoreMotionOracle.bblock_exit * ibtr1

type analyse_node = {

	`mutable an_Delayable : St.t option;`
	`mutable an_tr1 : btr1 option;`
	`mutable an_Delayable_exit : St.t option;`
	`mutable an_tr2 : btr2;`
	`mutable an_Used : St.s option;`
	`mutable an_tr3 : btr3 option;`

}

type analyze_result = {

	`aux_tbl : (StoreMotionOracle.address, Registers.reg) Stdlib.Hashtbl.t;`
	`an_nds : analyse_node Maps.PTree.t;`
	`stats : StoreMotionOracle.analyze_stats;`

}

val transfer_core : BTL.coq_function ->
       BTL.code * BTL_Invariants.gluemap * analyze_result

val print_analysis : Stdlib.out_channel ->
       BTL.coq_function * analyze_result -> unit

val transfer : BTL.coq_function -> BTL.code * BTL_Invariants.gluemap