Index of types

We define a struct containing useful information for the algorithm: blk2id and id2blk are two maps from block ids to bitvector ids and the reverse, respectively;, A worklist in wl to be used with the round-robin fixpoint;, The corresponding cardinality in card;, In last_reg, the Coq positive corresponding to the last register id before executing the oracle (thus, for all n > last_reg, we know that n is a fresh variable);, A set sr_vauxs of fresh SR-variables from the oracle.

block_info [BTLtypes]

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

btr0 [StoreMotionOracle.Make]

btr1 [StoreMotionOracle.Make]

btr2 [StoreMotionOracle.Make]

btr3 [StoreMotionOracle.Make]

called_function [PrepassSchedulingOracleDeps]

cand [StoreMotionOracle]

cand_t [LazyCodeCore]

A candidate is a struct with: A map (block |-> offset set) of where the operation occurs in lhs;, The bitvector predicates in state;, A dedicated auxialiary variable to insert and replace the instruction;, A boolean indicating if the candidate depends on memory;, A boolean indicating if the candidate was strength-reduced;, A mutable list of arguments that is modified to permit substitution during the algorithm (a previous candidate can replace arguments of a future one). This list can also be emptied when the candidate was merged with another, so that it will be skipped by the algorithm;, The list of initial arguments before any substitution.

ci32 [LazyCodeCore]

ci64 [LazyCodeCore]

ckey_t [LazyCodeCore]

cm_ckey_t [LazyCodeCore]

const_t [LazyCodeCore]

Type for constants, were the Coq positive corresponds to the block in which the constant is.

eqclass [BTLtoRTLaux]

flattened_equation_or_condition [CSE3analysisaux]

function_info [BTLtypes]

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

ibtr0 [StoreMotionOracle.Make]

ibtr1 [StoreMotionOracle.Make]

ibtr2 [StoreMotionOracle.Make]

ibtr3 [StoreMotionOracle.Make]

icand [StoreMotionOracle.StPartial]

iflift_mode [PrepassSchedulingOracle]

innerLoop [Duplicateaux]

inst_info_shadow [BTLtypes]

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

inv_t [BTLtypes]

Type of invariants in oracles

join_res [StoreMotionOracle]

lct_predicate_t [LazyCodeCore]

lct_predicates [LazyCodeCore]

Each candidate for CM/SR have a list of bitvector predicates.

loc [PrepassSchedulingOracle]

mentions_element [BTL_BlockOptimizeraux]

mt_list [StoreMotionOracle.StPartial]

opweights [PrepassSchedulingOracleDeps]

pseudo_boolean_mapper [InstructionScheduler]

pseudo_boolean_problem_type [InstructionScheduler]

register_info [BTL_BlockOptimizeraux]

rel_loc [PrepassSchedulingOracle]

relsymbol [PrepassSchedulingOracle]

relvalue [PrepassSchedulingOracle]

s [StoreMotionOracle.St_type]

s [StoreMotionOracle.StPartial]

s [StoreMotionOracle.StTotal]

smash_t [StoreMotionOracle.St_type]

smash_t [StoreMotionOracle.StPartial]

smash_t [StoreMotionOracle.StTotal]

sr_size [LazyCodeCore]

sr_t [LazyCodeCore]

state [BTLtoRTLaux]

stores [StoreMotionOracle]

t [Bitv]

the type of bit vectors

t [StoreMotionOracle.St_type]

t [StoreMotionOracle.StPartial]

t [StoreMotionOracle.StTotal]

t_flags [LazyCodeCore]

t_lct_stats [LazyCodeCore]

A
abs_loc [PrepassSchedulingOracle]
address [StoreMotionOracle]
affine_form [LazyCodeCore]
analyse_node [StoreMotionOracle.Make]
analyze_result [StoreMotionOracle.Make]
analyze_stats [StoreMotionOracle]
B
bb_tf_event_t [LazyCodeOracle]
bblock_exit [StoreMotionOracle]
blk_tools_t [LazyCodeCore]	We define a struct containing useful information for the algorithm: `blk2id` and `id2blk` are two maps from block ids to bitvector ids and the reverse, respectively;, A worklist in `wl` to be used with the round-robin fixpoint;, The corresponding cardinality in `card`;, In `last_reg`, the Coq positive corresponding to the last register id before executing the oracle (thus, for all `n` > `last_reg`, we know that n is a fresh variable);, A set `sr_vauxs` of fresh SR-variables from the oracle.
block_info [BTLtypes]	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
btr0 [StoreMotionOracle.Make]
btr1 [StoreMotionOracle.Make]
btr2 [StoreMotionOracle.Make]
btr3 [StoreMotionOracle.Make]
C
called_function [PrepassSchedulingOracleDeps]
cand [StoreMotionOracle]
cand_t [LazyCodeCore]	A candidate is a struct with: A map (block \|-> offset set) of where the operation occurs in `lhs`;, The bitvector predicates in `state`;, A dedicated auxialiary variable to insert and replace the instruction;, A boolean indicating if the candidate depends on memory;, A boolean indicating if the candidate was strength-reduced;, A mutable list of arguments that is modified to permit substitution during the algorithm (a previous candidate can replace arguments of a future one). This list can also be emptied when the candidate was merged with another, so that it will be skipped by the algorithm;, The list of initial arguments before any substitution.
ci32 [LazyCodeCore]
ci64 [LazyCodeCore]
ckey_t [LazyCodeCore]
cm_ckey_t [LazyCodeCore]
const_t [LazyCodeCore]	Type for constants, were the Coq positive corresponds to the block in which the constant is.
E
eqclass [BTLtoRTLaux]
F
flattened_equation_or_condition [CSE3analysisaux]
function_info [BTLtypes]	Shadow field attached to each BTL function * typing: field transferring RTL typing information in BTL (used in regpres scheduling)
I
ibtr0 [StoreMotionOracle.Make]
ibtr1 [StoreMotionOracle.Make]
ibtr2 [StoreMotionOracle.Make]
ibtr3 [StoreMotionOracle.Make]
icand [StoreMotionOracle.StPartial]
iflift_mode [PrepassSchedulingOracle]
innerLoop [Duplicateaux]
inst_info_shadow [BTLtypes]	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
inv_t [BTLtypes]	Type of invariants in oracles
J
join_res [StoreMotionOracle]
L
lct_predicate_t [LazyCodeCore]
lct_predicates [LazyCodeCore]	Each candidate for CM/SR have a list of bitvector predicates.
loc [PrepassSchedulingOracle]
M
mentions_element [BTL_BlockOptimizeraux]
mt_list [StoreMotionOracle.StPartial]
O
opweights [PrepassSchedulingOracleDeps]
P
pseudo_boolean_mapper [InstructionScheduler]
pseudo_boolean_problem_type [InstructionScheduler]
R
register_info [BTL_BlockOptimizeraux]
rel_loc [PrepassSchedulingOracle]
relsymbol [PrepassSchedulingOracle]
relvalue [PrepassSchedulingOracle]
S
s [StoreMotionOracle.St_type]
s [StoreMotionOracle.StPartial]
s [StoreMotionOracle.StTotal]
smash_t [StoreMotionOracle.St_type]
smash_t [StoreMotionOracle.StPartial]
smash_t [StoreMotionOracle.StTotal]
sr_size [LazyCodeCore]
sr_t [LazyCodeCore]
state [BTLtoRTLaux]
stores [StoreMotionOracle]
T
t [Bitv]	the type of bit vectors
t [StoreMotionOracle.St_type]
t [StoreMotionOracle.StPartial]
t [StoreMotionOracle.StTotal]
t_flags [LazyCodeCore]
t_lct_stats [LazyCodeCore]