Module LazyCodeOracle

module LazyCodeOracle: sig .. end

LCT Oracle implementation

Detection, construction and insertion of candidates

val lhs_blk_add : LazyCodeCore.cand_t -> int -> BTLtypes.OrdIS.elt -> unit

val lhs_blk_rem : LazyCodeCore.cand_t -> int -> BTLtypes.OrdIS.elt -> unit

val insert_cand : LazyCodeCore.ckey_t ->
       BTLtypes.OrdIS.elt -> Camlcoq.P.t -> bool -> Camlcoq.P.t list -> unit

If the ckey already exist, we check if the candidate was already seen in block pc, ifso, we add it to the offset set, ifnot, we create a singleton.

val erase_latest_cand : LazyCodeCore.ckey_t ->
       LazyCodeCore.cand_t ->
       LazyCodeCore.cand_t -> BTLtypes.OrdIS.t LazyCodeCore.IM.t -> unit

Compare both cand and old_cand according to their position, update the lhs field of the earlier, and and erase the last one by emptying lhs.

val merge_cand : LazyCodeCore.ckey_t -> LazyCodeCore.cand_t -> unit

Merge an eventually existing candidate at ckey with cand, and erase the latest one.

val make_op_ckey : BTLtypes.OrdIS.elt ->
       Camlcoq.P.t ->
       AST.trapping_mode -> Op.operation -> Camlcoq.P.t list -> Camlcoq.P.t -> unit

Build a candidate from a btl operation.

val make_load_ckey : BTLtypes.OrdIS.elt ->
       Camlcoq.P.t ->
       AST.trapping_mode ->
       AST.memory_chunk ->
       Op.addressing -> Camlcoq.P.t list -> ValueDomain.aval option -> unit

val detect_constants : (Camlcoq.P.t * BTL.iblock_info) list -> unit

Detect constants over the whole function (never erased) A constant that is defined multiple times is still a constant, and in this case we keep the oldest (former) one.

val detect_candidates : Camlcoq.P.t -> BTL.iblock_info -> unit

Detect candidates (transfer function to be used with apply_over_function).

Match and extraction functions for candidates

val match_op_ckey : Op.operation -> Camlcoq.P.t list -> LazyCodeCore.ckey_t -> bool

val match_load_ckey : AST.trapping_mode ->
       AST.memory_chunk ->
       Op.addressing ->
       Camlcoq.P.t list -> ValueDomain.aval option -> LazyCodeCore.ckey_t -> bool

val extract_ckey_args : LazyCodeCore.ckey_t -> Camlcoq.P.t list

val extract_ckey_chk_aaddr : LazyCodeCore.ckey_t -> AST.memory_chunk * ValueDomain.aval option

Local analysis part

val initialize_nonrec_predicates : int -> LazyCodeCore.ckey_t -> LazyCodeCore.cand_t -> unit

Initialize local and non-recursive predicates.

type bb_tf_event_t =

`\|`	`E_matchN`
`\|`	`E_matchX`
`\|`	`E_smash`
`\|`	`E_injure`
`\|`	`E_end`

val bb_analysis : LazyCodeCore.ckey_t ->
       LazyCodeCore.cand_t ->
       (int -> int -> int -> bb_tf_event_t -> unit) ->
       BTL.iblock -> unit

This function performs an analysis over a single basic-block ib. It has currently two main purposes:

Computing the transp, injure, ncomp, and xcomp predicates (which are local);
Computing insertion points. A transfer function tf must be given as an argument, with the following expected signature: tf : (offset: int) -> (border: int) -> (first_smash: int) -> bb_tf_event_t -> unit where:
offset: current position in the block; it is equal to the number of BTL instruction at the end;
border: indicates the point separating the entry part from the exit part;
first_smash: contains the offset of the first instruction smashing the given candidate dependencies;
bb_tf_event_t: sum type given to tf to indicate one of five cases:
- E_matchN: we matched the candidate in the entry part;
- E_matchX: we matched the candidate in the exit part;
- E_smash: one of the candidate dependencies was smashed;
- E_injure: one of the candidate dependencies was injured;
- E_end: we reached the end of the basic-block.

val local_predicates_for_cand : int Maps.PTree.t ->
       LazyCodeCore.ckey_t ->
       LazyCodeCore.cand_t -> Camlcoq.P.t -> BTL.iblock -> unit

Computes transp, injure, ncomp and xcomp predicates.

val init_and_local_analysis : BTL.code ->
       LazyCodeCore.blk_tools_t ->
       LazyCodeCore.ckey_t -> LazyCodeCore.cand_t -> unit

Init non-recursive predicates and computes local ones for a whole function.

Predicates transfer functions (to be used with round-robin algorithm)

val d_safe_tf : int Maps.PTree.t ->
       Camlcoq.P.t list ->
       LazyCodeCore.cand_t -> Camlcoq.P.t -> int -> Bitv.t array -> bool array

D_Safe transfer function sols.(0) should be xdsafe and sols.(1) should be ndsafe.

val u_safe_tf : int Maps.PTree.t ->
       Camlcoq.P.t list ->
       LazyCodeCore.cand_t -> Camlcoq.P.t -> int -> Bitv.t array -> bool array

U_Safe transfer function sols.(0) should be nusafe and sols.(1) should be xusafe.

val delayed_tf : int Maps.PTree.t ->
       Camlcoq.P.t list ->
       LazyCodeCore.cand_t -> Camlcoq.P.t -> int -> Bitv.t array -> bool array

Delayed transfer function sols.(0) should be ndelayed and sols.(1) should be xdelayed.

val isolated_tf : int Maps.PTree.t ->
       Camlcoq.P.t list ->
       LazyCodeCore.cand_t -> Camlcoq.P.t -> int -> Bitv.t array -> bool array

Isolated transfer function sols.(0) should be xisolated and sols.(1) should be nisolated.

val critical_tf : int Maps.PTree.t ->
       Camlcoq.P.t list ->
       LazyCodeCore.cand_t -> Camlcoq.P.t -> int -> Bitv.t array -> bool array

Critical transfer function sols.(0) should be xcritical and sols.(1) should be ncritical.

val substcrit_tf : int Maps.PTree.t ->
       Camlcoq.P.t list ->
       LazyCodeCore.cand_t -> Camlcoq.P.t -> int -> Bitv.t array -> bool array

Subst-Crit transfer function sols.(0) should be nsubstcrit and sols.(1) should be xsubstcrit.

Update transfer function with two equations sols.(0) should be xupdate and sols.(1) should be nupdate let update_tf (blk2id: int PTree.t) (succs_list : P.t list) (cand : cand_t) (pc : P.t) (bitvi : int) (sols : Bitv.t array) : bool array = llog 3 "Update analyzing %d\n" (p2i pc); let xupdate = let xcomp = get_predicate_value cand bitvi P_xcomp in if xcomp then xcomp else List.exists (fun succ -> let succi = pget succ blk2id in let ninsert = get_predicate_value cand succi P_ninsert in let nupdate = Bitv.get sols.(1) succi in llog 3 "ninsert is %b and nupdate is %b\n" ninsert nupdate; (not ninsert) && nupdate) succs_list in llog 3 "xupdate is %b\n" xupdate; let nupdate = let ncomp = get_predicate_value cand bitvi P_ncomp in if ncomp then ncomp else let xinsert = get_predicate_value cand bitvi P_xinsert in if xinsert then not xinsert else xupdate in llog 3 "nupdate is %b\n" nupdate; | xupdate; nupdate |

val update_tf : int Maps.PTree.t ->
       Camlcoq.P.t list ->
       LazyCodeCore.cand_t -> Camlcoq.P.t -> int -> Bitv.t array -> bool array

Update transfer function sols contains the single equation.

Dataflow analysis part

val round_robin : BTL.code ->
       LazyCodeCore.blk_tools_t ->
       (int Maps.PTree.t ->
        Camlcoq.P.t list ->
        LazyCodeCore.cand_t -> Camlcoq.P.t -> int -> Bitv.t array -> bool array) ->
       LazyCodeCore.lct_predicate_t array -> LazyCodeCore.cand_t -> Bitv.t array

Main dataflow function: a unidirectionnal round-robin worklist (in wl) based dataflow algorithm taking a transfer function tf as parameter, and working on a single candidate cand at a time. The predicates parameter is an array containing the system of equations to evaluate.

Computation of predicates from dataflow equations

val compute_earliestness : BTL.code -> LazyCodeCore.blk_tools_t -> LazyCodeCore.cand_t -> unit

val compute_latestness : BTL.code -> LazyCodeCore.blk_tools_t -> LazyCodeCore.cand_t -> unit

Insertion points predicates and related functions

val compute_critical_insertion : LazyCodeCore.cand_t -> unit

val set_lct_targets : LazyCodeCore.cand_t -> Bitv.t -> Bitv.t -> Bitv.t -> Bitv.t -> unit

Set insertion and replacement points in the candidate record.

val find_substcrit_targets : BTL.code -> LazyCodeCore.blk_tools_t -> LazyCodeCore.cand_t -> unit

Push critical insertion points forward to the first non critical but substitution critical point, in the direction of the control-flow.

val compute_lcm_targets_notrap : LazyCodeCore.cand_t -> unit

Non-trapping insertion points: Insert(n) = Latest(n) /\ not Isolated(n)

val compute_lcm_targets_trap : BTL.code ->
       Camlcoq.P.t -> LazyCodeCore.blk_tools_t -> LazyCodeCore.cand_t -> unit

Trapping insertion points:

First computes a set P =
For each pc_p, build the set I = /\ (N-Comp(pc_i) \/ X-Comp(pc_i)) /\ exists (p : path), p = (pc_i, pc_p) /\ forall n, n in p /\ n > pc_i /\ n < pc_p -> Transp(n) Then, it applies the below rules: |I| > 0 -> N-Replace(pc_p) <- true X-Comp(pc_p) = true -> X-Insert(pc_p) <- true /\ X-replace(pc_p) <- true For each pc_i,
- N-Comp(pc_i) -> N-Insert(pc_i) <- true /\ N-Replace(pc_i) <- true
- X-Comp(pc_i) -> X-Insert(pc_i) <- true /\ X-Replace(pc_i) <- true

val dataflow_analysis : BTL.code ->
       Camlcoq.P.t ->
       LazyCodeCore.blk_tools_t ->
       LazyCodeCore.ckey_t -> LazyCodeCore.cand_t -> unit

Main dataflow analysis.

Rewriting part (modifying the CFG once analysis is done)

val insert_node : BTL.iblock -> int -> BTL.iblock -> BTL.iblock

Insert inst in ib at offset_target, using offset as iterator.

val commit_new_block : BTL.code Stdlib.ref -> Camlcoq.P.t -> BTL.iblock -> BTL.iblock_info -> unit

val update_args_ckey : LazyCodeCore.ckey_t -> Camlcoq.P.t list -> LazyCodeCore.ckey_t

val mark_updated_ckey : LazyCodeCore.ckey_t -> Camlcoq.P.t list -> unit

val mark_updated_op : Op.operation -> Camlcoq.P.t list -> Camlcoq.P.t list -> Camlcoq.P.t -> unit

val mark_updated_load : AST.trapping_mode ->
       AST.memory_chunk ->
       Op.addressing ->
       Camlcoq.P.t list -> Camlcoq.P.t list -> ValueDomain.aval option -> unit

val subst_arg : Camlcoq.P.t -> Camlcoq.P.t -> Camlcoq.P.t -> Camlcoq.P.t

val subst_arg_list : Camlcoq.P.t -> Camlcoq.P.t -> Camlcoq.P.t list -> Camlcoq.P.t list

val forward_replace : Camlcoq.P.t ->
       int -> LazyCodeCore.ckey_t -> Camlcoq.P.t -> BTL.iblock -> BTL.iblock

Forward substitution of auxiliary variables, and candidate replacement procedure. This function takes the target block pc, the target offset offset_target, and recurses through the basic-block ib. It bases its behavior on the comparison between the current offset offset and offset_target:

if offset < offset_target: continue and increment offset;
if offset = offset_target: ensure a match between the current instruction and the candidate to replace, replace it by a nop (rather than directly by a move), and continue. At this point, we also update the tables of affine values and constants by copying the previous mapping (if existing) to a new one bound to the auxiliary variable of the candidate. The algorithm saves the original destination of the replaced instruction;
if offset > offset_target: (meaning the candidate was already replaced by a nop), there are two possible subcases:
- A final case when either (i) the auxiliary variable or the original destination of the candidate is rewritten; (ii) the current instruction is another occurrence of the candidate or an injuring operation; (iii) we are reaching the end of the block. If so, we insert the move from the auxiliary variable and stop the substitution algorithm;
- A recursive case otherwise, where we substitute the previously saved original destination in the updated_args field of the current candidate by its auxiliary variable.

val compute_insertion_point : LazyCodeCore.ckey_t -> LazyCodeCore.cand_t -> BTL.iblock -> bool -> int

Compute the insertion point for a given basic-block and candidate.

val build_inst_from_ckey : Camlcoq.P.t -> LazyCodeCore.ckey_t -> BTL.iblock

Translate a virtual candidate to a concrete BTL instruction.

val sr_update_mul : Camlcoq.P.t list -> Camlcoq.P.t -> Camlcoq.P.t -> BTL.iblock -> BTL.iblock

val sr_update_add : Camlcoq.P.t list ->
       Camlcoq.P.t list -> Camlcoq.P.t -> Camlcoq.P.t -> BTL.iblock -> BTL.iblock

val strength_reduce_update : LazyCodeCore.blk_tools_t ->
       Camlcoq.P.t list ->
       Camlcoq.P.t ->
       LazyCodeCore.ckey_t -> LazyCodeCore.cand_t -> BTL.iblock -> BTL.iblock

Insert update assignments for strength reduction candidates

val code_motion : BTL.code Stdlib.ref ->
       Camlcoq.P.t LazyCodeCore.IM.t ->
       LazyCodeCore.ckey_t ->
       LazyCodeCore.cand_t -> Bitv.t -> Bitv.t -> bool -> unit

Applies code motion using the information in insert_pred and replace_pred.

val strength_reduction : BTL.code Stdlib.ref ->
       LazyCodeCore.blk_tools_t ->
       Camlcoq.P.t list -> LazyCodeCore.ckey_t -> LazyCodeCore.cand_t -> unit

val rewrite_graph : BTL.code Stdlib.ref ->
       LazyCodeCore.blk_tools_t ->
       LazyCodeCore.ckey_t -> LazyCodeCore.cand_t -> unit

Invariant construction part

val build_ival_from_ckey : bool -> LazyCodeCore.ckey_t -> BTL_Invariants.ival

val build_invariants : BTL.code ->
       BTL_Invariants.gluemap ->
       Camlcoq.P.t ->
       LazyCodeCore.blk_tools_t ->
       (LazyCodeCore.ckey_t * LazyCodeCore.cand_t) list -> BTL_Invariants.gluemap

Build all the needed invariants for LCT: for each candidate in the list, with a defined vaux: g1 = (N-REPLACE /\ not N-INSERT) \/ (X-REPLACE /\ not X-INSERT) g2 = (not N-ISOLATED /\ not X-ISOLATED) g3 = (not N-DELAYED /\ not X-DELAYED) pp = g1 \/ (g2 /\ g3) if the candidate is trapping: pp = pp /\ N-U-SAFE for blk_pc in CFG if blk_pc <> entry: if candidate is a SRmul && candidate is not immediate SR op && candidate was reduced: r = constant_reg of candidate cop, cpc = obtain the constant operation and first appearance block pc if blk_pc < cpc && r <= last_reg (ie is not a fresh variable) && (blk_pc in pp || r live in blk_pc) add an history invariant based on the constant operation, along with a corresponding liveness entry. if blk_pc in pp: add a gluing invariant based on the candidate operation in ckey

Main part

val identify_blocks : BTL.code -> int Maps.PTree.t * Camlcoq.P.t LazyCodeCore.IM.t

This function builds two mappings from block ids to bitvector ids and its reverse, to facilitate bitvector manipulation.

val initialize : unit -> unit

val prepare_data : BTL.code ->
       Camlcoq.P.t ->
       BTL.code * BTL_Invariants.gluemap * LazyCodeCore.blk_tools_t *
       (LazyCodeCore.ckey_t * LazyCodeCore.cand_t) list

val may_downgrade_ckey : BTL.code ->
       LazyCodeCore.blk_tools_t ->
       LazyCodeCore.ckey_t -> LazyCodeCore.cand_t -> LazyCodeCore.ckey_t

Downgrading an SRadd candidate to a LCM one. The candidate is downgraded if none of the arguments are strength-reduction auxiliary variables.

val update_ckey : BTL.code ->
       LazyCodeCore.blk_tools_t ->
       LazyCodeCore.ckey_t -> LazyCodeCore.cand_t -> LazyCodeCore.ckey_t

val lazy_optim : BTL.code Stdlib.ref ->
       Camlcoq.P.t ->
       LazyCodeCore.blk_tools_t ->
       (LazyCodeCore.ckey_t * LazyCodeCore.cand_t) list ->
       (LazyCodeCore.ckey_t * LazyCodeCore.cand_t) list

val liveness_and_dce : BTL.code -> BTL.code

val lazy_code_oracle : BTL.code -> Camlcoq.P.t -> BTL.code * BTL_Invariants.gluemap

Launch according to cli args.