Module LazyCodeBackend

module LazyCodeBackend: sig .. end

Backend specific functions for the LCT algorithm

Functions of the LCT oracle that are specific to the underlying architecture. We only define SR-related functions here.

val is_constant_op : Op.operation -> bool

Constant operation that the oracle should consider.

val get_const_from_reg : Camlcoq.P.t -> LazyCodeCore.ci64

val match_injuring_op : Op.operation ->
       Camlcoq.P.t list ->
       Camlcoq.P.t -> Camlcoq.P.t list -> (Camlcoq.P.t * LazyCodeCore.ci64) option

Matching "injuring" operations, which slightly modify the value of a variable with a constant argument: for now, we only target immediate additions and additions whose at least one argument was detected as a constant by the is_constant_op function above. Only on long (not int).

val is_sr_candidate_op : Op.operation ->
       Camlcoq.P.t list ->
       Camlcoq.P.t -> Camlcoq.P.t option -> LazyCodeCore.ckey_t option

Auxiliary function for candidate detection. The o_pc_dst parameter must be defined when calling from the detection procedure, as we use the destination register to initialize affine forms. Otherwise, it may be None when the call comes from the forward replace function. Currently, we target immediate left shifts, multiplications, and additions (immediate or not). Only on long (not int).

val is_immediate_sr_op : Op.operation -> bool

Returns true for multiplicative SR operations working with immediates.

val extract_ckey_const : LazyCodeCore.ckey_t -> LazyCodeCore.ci64

val mk_sr_update_op : LazyCodeCore.ci64 -> Op.operation

val is_sr_update_op : Op.operation -> bool

val is_affine_op : Op.operation -> bool