Module LazyCodeCore

module LazyCodeCore: sig .. end

Core definitions for the LCT oracle

Types

module IM: Stdlib.Map.Make(Stdlib.Int)

type ci64 = Integers.Int64.int

Coq Int64 type

type lct_predicates = {

	`mutable transp : Bitv.t option;`
	`mutable ncomp : Bitv.t option;`
	`mutable xcomp : Bitv.t option;`
	`mutable injured : Bitv.t option;`
	`mutable update : Bitv.t option;`
	`mutable ndsafe : Bitv.t option;`
	`mutable xdsafe : Bitv.t option;`
	`mutable nusafe : Bitv.t option;`
	`mutable xusafe : Bitv.t option;`
	`mutable nearliest : Bitv.t option;`
	`mutable xearliest : Bitv.t option;`
	`mutable ndelayed : Bitv.t option;`
	`mutable xdelayed : Bitv.t option;`
	`mutable nlatest : Bitv.t option;`
	`mutable xlatest : Bitv.t option;`
	`mutable nisolated : Bitv.t option;`
	`mutable xisolated : Bitv.t option;`
	`mutable ninsert : Bitv.t option;`
	`mutable xinsert : Bitv.t option;`
	`mutable nreplace : Bitv.t option;`
	`mutable xreplace : Bitv.t option;`
	`mutable ncritical : Bitv.t option;`
	`mutable xcritical : Bitv.t option;`
	`mutable ncritinsert : Bitv.t option;`
	`mutable xcritinsert : Bitv.t option;`
	`mutable nsubstcrit : Bitv.t option;`
	`mutable xsubstcrit : Bitv.t option;`

}

Each candidate for CM/SR have a list of bitvector predicates. The six last ones are only used for SR.

type lct_predicate_t =

`\|`	`P_transp`
`\|`	`P_ncomp`
`\|`	`P_xcomp`
`\|`	`P_injured`
`\|`	`P_update`
`\|`	`P_ndsafe`
`\|`	`P_xdsafe`
`\|`	`P_nusafe`
`\|`	`P_xusafe`
`\|`	`P_nearliest`
`\|`	`P_xearliest`
`\|`	`P_ndelayed`
`\|`	`P_xdelayed`
`\|`	`P_nlatest`
`\|`	`P_xlatest`
`\|`	`P_nisolated`
`\|`	`P_xisolated`
`\|`	`P_ninsert`
`\|`	`P_xinsert`
`\|`	`P_nreplace`
`\|`	`P_xreplace`
`\|`	`P_ncritical`
`\|`	`P_xcritical`
`\|`	`P_ncritinsert`
`\|`	`P_xcritinsert`
`\|`	`P_nsubstcrit`
`\|`	`P_xsubstcrit`

type cm_ckey_t =

`\|`	`CMop of AST.trapping_mode * Op.operation * Camlcoq.P.t list`
`\|`	`CMload of AST.trapping_mode * AST.memory_chunk * Op.addressing * Camlcoq.P.t list * ValueDomain.aval option`

type sr_t =

`\|`	`SRmul`
`\|`	`SRadd`

type ckey_t =

`\|`	`CCM of cm_ckey_t`
`\|`	`CSR of sr_t * Op.operation * Camlcoq.P.t list`

Kind of candidates for CM/SR (splitted with the CCM|CSR type):

CMop: Code Motion candidate representing a BTL Op;
CMload: Code Motion candidate representing a BTL Load;
CSR: Strength-Reduction candidate, as for CMop but with one one less information as trapping_mode is not considered for SR (always non-trap). SR candidates also have two possible types :
- SRmul where we expect to insert an update operation;
- SRadd to represent potentially addition SR (SRadd candidates might be downgraded to CM ones if they do not contain an auxiliary variable in their argument when starting the LCT process. See the downgrade function in LazyCodeOracle module). SRadd candidates have an update operation computed using affine values Their injuring operation corresponds to the update operation of SRmul.

type cand_t = {

	`mutable lhs : BTLtypes.OrdIS.t IM.t;`
	`state : lct_predicates;`
	`mutable vaux : Camlcoq.P.t option;`
	`memdep : bool;`
	`mutable was_reduced : bool;`
	`mutable updated_args : Camlcoq.P.t list option;`
	`orig_args : Camlcoq.P.t list;`

}

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.

type blk_tools_t = {

	`blk2id : int Maps.PTree.t;`
	`id2blk : Camlcoq.P.t IM.t;`
	`wl : BTLtypes.OrdIS.t;`
	`card : int;`
	`last_reg : Camlcoq.P.t;`
	`mutable sr_vauxs : HashedSet.PSet.t;`

}

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.

type const_t = Op.operation * Camlcoq.P.t

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

type 'a affine_form =

`\|`	`Aff_term of 'a * Camlcoq.P.t * 'a affine_form`
`\|`	`Aff_const of 'a`

The above is a simple inductive polymorphic affine form, with 'a the type of constants, and Coq positive for registers.

Tools for managing variables and predicates

val constants : (Camlcoq.P.t, const_t) Stdlib.Hashtbl.t

Maps registers to immediate constant operation (if they are unchanged over the whole function).

val candidates : (ckey_t, cand_t) Stdlib.Hashtbl.t

Maps candidates keys to candidate type cand_t.

val affine_int64 : (Camlcoq.P.t * Camlcoq.P.t, ci64 affine_form)
       Stdlib.Hashtbl.t

Maps a tuple (block pc, register) to its int64 affine value, if applicable.

Affine operations: multiplication, addition, and accumulation of injuring amounts for a given set of variables.

val affine_mul : ('a -> 'a -> 'a) ->
       'a -> 'a affine_form -> 'a affine_form

Affine value times a constant of type 'a.

val affine_add : ('a -> 'a -> 'a) ->
       'a affine_form ->
       'a affine_form -> 'a affine_form

Addition over affine values with type 'a. We sort them by increasing order of registers in terms.

val affine_inj_const : 'a affine_form -> 'a

Wrappers to mul add, and inj_factor over affine_int64.

val aff_mul_int64 : ci64 ->
       Integers.Int64.int affine_form ->
       Integers.Int64.int affine_form

val aff_add_int64 : Integers.Int64.int affine_form ->
       Integers.Int64.int affine_form ->
       Integers.Int64.int affine_form

val aff_inj_const_int64 : Camlcoq.P.t * Camlcoq.P.t -> ci64

Grab the constant of affine form with key tup; Used for injuring operations.

val aff_inj_update_int64 : Camlcoq.P.t ->
       Camlcoq.P.t ->
       ci64 affine_form -> bool -> ci64

Compute the sum of all Aff_term(ci, ri, ...) with ci * (aff_inj_const_int64 (pc, ri)). The last constant Aff_const c is included only if arg is equal to at least one ri. This trick is needed to avoid adding the last constant of single term affine forms c * r + const when r = arg. Indeed, those constants are invariant so we don't need to compensate them.

val aff_find_update_int64 : Camlcoq.P.t list ->
       Camlcoq.P.t -> ci64 affine_form option

Finds the first defined affine form with key (pt, arg) for each pt in pts.

val aff_cargs_update_int64 : Camlcoq.P.t list -> Camlcoq.P.t -> Camlcoq.P.t list -> ci64

Fold computing the overall compensation value to add for a given list of arguments cargs, seeking for defined affine forms in block pc first, and in replace_pts otherwise (in case some values are out of the block's scope; it happens in practice).

val aff_may_replace_int64 : Camlcoq.P.t * Camlcoq.P.t ->
       ci64 affine_form -> bool -> unit

If force, replace the value at tup by aff, else, add it only if tup is not already defined.

val aff_mul_int64_uset : Camlcoq.P.t ->
       Camlcoq.P.t -> Camlcoq.P.t -> ci64 -> bool -> unit

Set a1 * l in (pc, dst) after eventually updating with the old value at (pc, a1).

val aff_add1_int64_uset : Camlcoq.P.t ->
       Camlcoq.P.t -> Camlcoq.P.t -> ci64 -> bool -> unit

Set a1 + l in (pc, dst) after eventually updating with the old value at (pc, a1).

val aff_add2_int64_uset : Camlcoq.P.t -> Camlcoq.P.t -> Camlcoq.P.t -> Camlcoq.P.t -> bool -> unit

Set a1 + a2 in (pc, dst) after eventually updating with the old values of {(pc, a1), (pc, a2)}.

Utility functions for candidates

val candidate_op_filter : Op.operation -> bool

val is_sr_ckey : ckey_t -> bool

val is_ld_ckey : ckey_t -> bool

val is_sr_mul_ckey : ckey_t -> bool

val is_constant_reg : Camlcoq.P.t -> bool

val is_trapping_ckey : ckey_t -> bool

val default_predicate_value : lct_predicate_t -> bool

Default predicate value, this setting is very important and quite touchy...

val is_fwd_predicate : lct_predicate_t -> bool

Is the predicate requiring a forward analysis?

val mk_def_df_predicates : unit -> lct_predicates

At the beginning, every predicate option is set to None.

val mk_cand : int -> BTLtypes.OrdIS.elt -> bool -> Camlcoq.P.t list -> cand_t

Initialize a new candidate appearing at pc, offset with _memdep, args and default values.

Read and write a predicate, or its values in cand.

val get_predicate_cand : cand_t -> lct_predicate_t -> Bitv.t

val get_predicate_value : cand_t -> int -> lct_predicate_t -> bool

val set_predicate_cand : cand_t -> Bitv.t -> lct_predicate_t -> unit

val set_predicate_value : cand_t -> int -> lct_predicate_t -> bool -> unit

val set_predicates_array : cand_t ->
       lct_predicate_t array -> Bitv.t array -> unit

Write an array of predicates preds with an array of solutions sols.

val is_really_sr_cand : cand_t -> bool

If a candidate for strength-reduction is never injured, then we can perform the code-motion dataflow analysis only.

val is_real_sr_mul_cand : ckey_t -> cand_t -> bool

Flags default values

type t_flags = {

	`mutable ok_sr : bool;`
	`mutable ok_trap : bool;`
	`mutable tlimit : int;`
	`mutable nlimit : int;`

}

val flags : t_flags

Logs and Statistics

val log_lvl : int

val llog : int -> ('a, Stdlib.out_channel, unit) Stdlib.format -> 'a

type t_lct_stats = {

	`mutable tstart : float;`
	`mutable tcounter : int;`
	`mutable nb_notrap : int;`
	`mutable nb_trap : int;`
	`mutable nb_nins_notrap : int;`
	`mutable nb_xins_notrap : int;`
	`mutable nb_nins_trap : int;`
	`mutable nb_xins_trap : int;`
	`mutable nb_nrep_notrap : int;`
	`mutable nb_xrep_notrap : int;`
	`mutable nb_nrep_trap : int;`
	`mutable nb_xrep_trap : int;`
	`mutable nb_sr : int;`
	`mutable nb_nins_sr : int;`
	`mutable nb_xins_sr : int;`
	`mutable nb_nrep_sr : int;`
	`mutable nb_xrep_sr : int;`
	`mutable nb_upd_sr : int;`
	`mutable nb_aseq_ginv : int;`
	`mutable nb_aseq_hinv : int;`
	`mutable lct_exec_time : float;`

}

val save_stats : bool

val stats : t_lct_stats

val reset_stats : unit -> unit

Below tools to limit the oracle in runtime.

exception TimeLimitReached

val has_timeout : unit -> bool

val check_time : unit -> unit

val filter_candidates : unit -> unit

Limit the number of candidates according to the user flag.

Debugging functions, and statistics.

val stat_code_motion : bool -> ckey_t -> bool -> unit

val fprint_stats_header : Stdlib.out_channel -> unit -> unit

val fprint_stats : Stdlib.out_channel -> unit -> unit

val write_stats : unit -> unit

val print_ordis : Stdlib.out_channel -> BTLtypes.OrdIS.t -> unit

val print_imap : Stdlib.out_channel -> BTLtypes.OrdIS.t IM.t -> unit

val print_sr_type : Stdlib.out_channel -> sr_t -> unit

val print_cand : Stdlib.out_channel -> ckey_t * cand_t -> unit

val print_predicates : BTLtypes.OrdIS.t -> int Maps.PTree.t -> unit

Print every predicates of every candidates in a CSV-like format separated with semicolumns.

val print_constants : unit -> unit

val print_candidates : unit -> unit

val print_affine_form : Stdlib.out_channel -> ('a -> int64) * 'a affine_form -> unit

val print_affine_map : (Camlcoq.P.t * Camlcoq.P.t, 'a affine_form) Stdlib.Hashtbl.t ->
       ('a -> int64) -> unit