Module BTLtypes

module BTLtypes: sig .. end

Common type definitions for BTL: oracles' types and shadow fields

type inst_info_shadow = {

	`mutable inumb : int;`
	`mutable opt_info : bool option;`
	`mutable visited : bool;`
	`mutable liveins : Registers.Regset.t;`

}

This struct is a shadow field attached to each BTL instruction * inumb: int field used for remembering the original numbering of CFG * opt_info: option bool used for various tests: * - On Bcond, stores the prediction information * - On Bload, stores the trapping information (if Some false, the load was * initially non-trapping, and the opposite if some true) * visited: boolean used to tag instructions * liveins: set of lives registers

type block_info = {

	`mutable bnumb : int;`
	`mutable visited : bool;`
	`mutable input_regs : Registers.Regset.t;`
	`mutable s_output_regs : Registers.Regset.t;`
	`mutable successors : Camlcoq.P.t list;`
	`mutable predecessors : Camlcoq.P.t list;`

}

Shadow field attached to each BTL iblock_info type * bnumb: int representing the block id in the BTL CFG * visited: boolean used to tag blocks * input_regs: set of input (live) registers * s_output_regs: set of output (live) registers * successors and predecessors: list of them

type function_info = {

	`typing : RTLtyping.regenv;`
	`bb_mode : bool;`

}

Shadow field attached to each BTL function * typing: field transferring RTL typing information in BTL (used in regpres scheduling)

module OrdIS: Stdlib.Set.Make(Stdlib.Int)

Notations for Ordered sets of integers

val ($?) : OrdIS.elt -> OrdIS.t -> bool

val ($+) : OrdIS.elt -> OrdIS.t -> OrdIS.t

val ($-) : OrdIS.elt -> OrdIS.t -> OrdIS.t

val ($|$) : OrdIS.t -> OrdIS.t -> OrdIS.t

val ($&$) : OrdIS.t -> OrdIS.t -> OrdIS.t

val (~$) : OrdIS.elt -> OrdIS.t

val (!$-) : OrdIS.t -> OrdIS.elt

val (!$+) : OrdIS.t -> OrdIS.elt

type inv_t =

`\|`	`Gluing`
`\|`	`History`

Type of invariants in oracles