package jasmin

  1. Overview
  2. Docs

Module Jasmin.ProgSource

include module type of struct include CoreIdent end
Sourcemodule Name = CoreIdent.Name
Sourceval string_of_uid : uid -> string
Sourcetype base_ty = CoreIdent.base_ty =
  1. | Bool
  2. | Int
  3. | U of Wsize.wsize
Sourcetype 'len gty = 'len CoreIdent.gty =
  1. | Bty of base_ty
  2. | Arr of Wsize.wsize * 'len
Sourcetype 'len gety = 'len CoreIdent.gety =
  1. | ETbool
  2. | ETint
  3. | ETword of Wsize.signedness option * Wsize.wsize
  4. | ETarr of Wsize.wsize * 'len
Sourceval u8 : 'len gty
Sourceval u16 : 'len gty
Sourceval u32 : 'len gty
Sourceval u64 : 'len gty
Sourceval u128 : 'len gty
Sourceval u256 : 'len gty
Sourceval tu : Wsize.wsize -> 'len gty
Sourceval tbool : 'len gty
Sourceval tint : 'len gty
Sourceval etw : Wsize.wsize -> 'len gety
Sourceval etbool : 'len gety
Sourceval etint : 'len gety
Sourceval gty_of_gety : 'len gety -> 'len gty
Sourcetype +'len gvar = private 'len CoreIdent.gvar = {
  1. v_name : Name.t;
  2. v_id : uid;
  3. v_kind : Wsize.v_kind;
  4. v_ty : 'len gty;
  5. v_dloc : L.t;
  6. v_annot : Annotations.annotations;
}
Sourcemodule GV = CoreIdent.GV
Sourcemodule Cident = CoreIdent.Cident
Sourcetype funname = private CoreIdent.funname = {
  1. fn_name : Name.t;
  2. fn_id : uid;
}
Sourceval funname_tag : funname -> Uint63.t
Sourcemodule Sf = CoreIdent.Sf
Sourcemodule Mf = CoreIdent.Mf
Sourcemodule Hf = CoreIdent.Hf
module E = Expr
Sourcetype 'len gvar_i = 'len gvar L.located
Sourcetype 'len ggvar = {
  1. gv : 'len gvar_i;
  2. gs : E.v_scope;
}
Sourcetype 'len gexpr =
  1. | Pconst of Z.t
  2. | Pbool of bool
  3. | Parr_init of Wsize.wsize * 'len
  4. | Pvar of 'len ggvar
  5. | Pget of Memory_model.aligned * Warray_.arr_access * Wsize.wsize * 'len ggvar * 'len gexpr
  6. | Psub of Warray_.arr_access * Wsize.wsize * 'len * 'len ggvar * 'len gexpr
  7. | Pload of Memory_model.aligned * Wsize.wsize * 'len gexpr
  8. | Papp1 of Operators.sop1 * 'len gexpr
  9. | Papp2 of Operators.sop2 * 'len gexpr * 'len gexpr
  10. | PappN of Operators.opN * 'len gexpr list
  11. | Pif of 'len gty * 'len gexpr * 'len gexpr * 'len gexpr
Sourcetype 'len gexprs = 'len gexpr list
Sourcetype 'len gassert =
  1. | Pexpr of 'len gexpr
  2. | PappN_safety of Operators.opN_safety * 'len gexpr list
  3. | Pis_var_init of 'len gvar_i
  4. | Pis_mem_init of 'len gexpr * 'len gexpr
  5. | Pand of 'len gassert * 'len gassert
Sourceval is_stack_kind : Wsize.v_kind -> bool
Sourceval is_reg_kind : Wsize.v_kind -> bool
Sourceval is_ptr : Wsize.v_kind -> bool
Sourceval is_reg_ptr_kind : Wsize.v_kind -> bool
Sourceval is_stk_ptr_kind : Wsize.v_kind -> bool
Sourceval is_reg_direct_kind : Wsize.v_kind -> bool
Sourceval spill_to_mmx : int gvar -> bool
Sourcetype 'len glval =
  1. | Lnone of L.t * 'len gty
  2. | Lvar of 'len gvar_i
  3. | Lmem of Memory_model.aligned * Wsize.wsize * L.t * 'len gexpr
  4. | Laset of Memory_model.aligned * Warray_.arr_access * Wsize.wsize * 'len gvar_i * 'len gexpr
  5. | Lasub of Warray_.arr_access * Wsize.wsize * 'len * 'len gvar_i * 'len gexpr
Sourcetype 'len glvals = 'len glval list
Sourcetype 'len grange = E.dir * 'len gexpr * 'len gexpr
Sourcetype 'len assertion = string * 'len gassert
Sourcetype ('len, 'info, 'asm) ginstr_r =
  1. | Cassgn of 'len glval * E.assgn_tag * 'len gty * 'len gexpr
  2. | Copn of 'len glvals * E.assgn_tag * 'asm Sopn.sopn * 'len gexprs
  3. | Csyscall of 'len glvals * (Wsize.wsize * BinNums.coq_Z) Syscall_t.syscall_t * 'len gexprs
  4. | Cassert of 'len assertion
  5. | Cif of 'len gexpr * ('len, 'info, 'asm) gstmt * ('len, 'info, 'asm) gstmt
  6. | Cfor of 'len gvar_i * 'len grange * ('len, 'info, 'asm) gstmt
  7. | Cwhile of E.align * ('len, 'info, 'asm) gstmt * 'len gexpr * IInfo.t * 'info * ('len, 'info, 'asm) gstmt
  8. | Ccall of 'len glvals * funname * 'len gexprs
Sourceand ('len, 'info, 'asm) ginstr = {
  1. i_desc : ('len, 'info, 'asm) ginstr_r;
  2. i_loc : L.i_loc;
  3. i_info : 'info;
  4. i_annot : Annotations.annotations;
}
Sourceand ('len, 'info, 'asm) gstmt = ('len, 'info, 'asm) ginstr list
Sourcetype 'asm arch_info = {
  1. pd : Wsize.wsize;
  2. asmOp : 'asm Sopn.sopn Sopn.asmOp;
  3. zero_extend_op : 'asm -> Wsize.wsize -> 'asm option;
  4. known_implicits : (CoreIdent.Name.t * string) list;
  5. flagnames : CoreIdent.Name.t list;
}
Sourcetype 'len gfcontract = {
  1. f_iparams : 'len gvar_i list;
  2. f_ires : 'len gvar_i list;
  3. f_pre : 'len assertion list;
  4. f_post : 'len assertion list;
}
Sourcetype ('len, 'info, 'asm) gfunc = {
  1. f_loc : L.t;
  2. f_annot : FInfo.f_annot;
  3. f_info : 'info;
  4. f_contract : 'len gfcontract option;
  5. f_cc : FInfo.call_conv;
  6. f_name : funname;
  7. f_tyin : 'len gty list;
  8. f_args : 'len gvar list;
  9. f_body : ('len, 'info, 'asm) gstmt;
  10. f_tyout : 'len gty list;
  11. f_ret_info : FInfo.return_info;
  12. f_ret : 'len gvar_i list;
}
Sourcetype 'len ggexpr =
  1. | GEword of 'len gexpr
  2. | GEarray of 'len gexprs
Sourcetype ('len, 'info, 'asm) gmod_item =
  1. | MIfun of ('len, 'info, 'asm) gfunc
  2. | MIparam of 'len gvar * 'len gexpr
  3. | MIglobal of 'len gvar * 'len ggexpr
Sourcetype ('len, 'info, 'asm) gprog = ('len, 'info, 'asm) gmod_item list
Sourcetype pty = pexpr_ gty
Sourceand pvar = pexpr_ gvar
Sourceand pvar_i = pexpr_ gvar_i
Sourceand plval = pexpr_ glval
Sourceand plvals = pexpr_ glvals
Sourceand pexpr = pexpr_ gexpr
Sourceand pexpr_ =
  1. | PE of pexpr
Sourcetype epty = pexpr_ gety
Sourcetype ('info, 'asm) pinstr_r = (pexpr_, 'info, 'asm) ginstr_r
Sourcetype ('info, 'asm) pinstr = (pexpr_, 'info, 'asm) ginstr
Sourcetype ('info, 'asm) pstmt = (pexpr_, 'info, 'asm) gstmt
Sourcetype ('info, 'asm) pfunc = (pexpr_, 'info, 'asm) gfunc
Sourcetype ('info, 'asm) pmod_item = (pexpr_, 'info, 'asm) gmod_item
Sourcetype ('info, 'asm) pprog = (pexpr_, 'info, 'asm) gprog
Sourcemodule PV : sig ... end
Sourceval gkglob : 'len gvar_i -> 'len ggvar
Sourceval gkvar : 'len gvar_i -> 'len ggvar
Sourceval is_gkvar : 'len ggvar -> bool
Sourcemodule Mpv : Utils.Map.S with type key = pvar
Sourcemodule Spv : Utils.Set.S with type elt = pvar
Sourceval pty_equal : pty -> pty -> bool
Sourceval pexpr_equal : pexpr -> pexpr -> bool
Sourceval epty_equal : epty -> epty -> bool
Sourceval ws_of_ety : epty -> Wsize.wsize
Sourcetype ty = int gty
Sourcetype var = int gvar
Sourcetype var_i = int gvar_i
Sourcetype lval = int glval
Sourcetype lvals = int glval list
Sourcetype expr = int gexpr
Sourcetype exprs = int gexpr list
Sourcetype eassert = int gassert
Sourcetype range = int grange
Sourcetype ('info, 'asm) instr = (int, 'info, 'asm) ginstr
Sourcetype ('info, 'asm) instr_r = (int, 'info, 'asm) ginstr_r
Sourcetype ('info, 'asm) stmt = (int, 'info, 'asm) gstmt
Sourcetype ('info, 'asm) func = (int, 'info, 'asm) gfunc
Sourcetype ('info, 'asm) mod_item = (int, 'info, 'asm) gmod_item
Sourcetype global_decl = var * Global.glob_value
Sourcetype ('info, 'asm) prog = global_decl list * ('info, 'asm) func list
Sourceval var_of_ident : CoreIdent.var -> var
Sourceval ident_of_var : var -> CoreIdent.var
Sourcemodule V : sig ... end
Sourcemodule Sv : Utils.Set.S with type elt = var
Sourcemodule Mv : Utils.Map.S with type key = var
Sourcemodule Hv : Utils.Hash.S with type key = var
Sourceval is_regx : var -> bool
Sourceval kind_i : 'len gvar_i -> Wsize.v_kind
Sourceval ty_i : 'len gvar_i -> 'len gty
Sourceval fold_vars_ret : ('ty gvar -> 'acc -> 'acc) -> 'acc -> ('ty, 'info, 'asm) gfunc -> 'acc
Sourceval fold_vars_fc : ('ty gvar -> 'acc -> 'acc) -> 'acc -> ('ty, 'info, 'asm) gfunc -> 'acc
Sourceval vars_ret : ('info, 'asm) func -> Sv.t
Sourceval vars_lv : Sv.t -> lval -> Sv.t
Sourceval vars_e : expr -> Sv.t
Sourceval vars_es : expr list -> Sv.t
Sourceval vars_a : eassert -> Sv.t
Sourceval vars_i : ('info, 'asm) instr -> Sv.t
Sourceval vars_c : ('info, 'asm) stmt -> Sv.t
Sourceval pvars_c : ('info, 'asm) pstmt -> Spv.t
Sourceval vars_fc : ('info, 'asm) func -> Sv.t
Sourceval vars_fc_contract : ('info, 'asm) func -> Sv.t
Sourceval rvars_e : ('a gvar -> 'b -> 'b) -> 'b -> 'a gexpr -> 'b
Sourceval rvars_es : ('a gvar -> 'b -> 'b) -> 'b -> 'a gexprs -> 'b
Sourceval rvars_lv : ('a gvar -> 'b -> 'b) -> 'b -> 'a glval -> 'b
Sourceval rvars_lvs : ('a gvar -> 'b -> 'b) -> 'b -> 'a glvals -> 'b
Sourceval rvars_a : ('a gvar -> 'b -> 'b) -> 'b -> 'a gassert -> 'b
Sourceval rvars_as : ('a gvar -> 'b -> 'b) -> 'b -> 'a assertion list -> 'b
Sourceval locals : ('info, 'asm) func -> Sv.t
Sourceval spilled : ('info, 'asm) func -> Sv.t
Sourceval written_lv : Sv.t -> lval -> Sv.t

written_lv s x inserts x into s if x is a variable

Sourceval written_vars_fc : ('info, 'asm) func -> Sv.t * L.i_loc list Mf.t
Sourceval refresh_i_loc_i : ('info, 'asm) instr -> ('info, 'asm) instr
Sourceval refresh_i_loc_c : ('info, 'asm) stmt -> ('info, 'asm) stmt
Sourceval refresh_i_loc_f : ('info, 'asm) func -> ('info, 'asm) func
Sourceval refresh_i_loc_p : ('info, 'asm) prog -> ('info, 'asm) prog
Sourceval int_of_ws : Wsize.wsize -> int
Sourceval string_of_ws : Wsize.wsize -> string
Sourceval size_of_ws : Wsize.wsize -> int
Sourceval wsize_lt : Wsize.wsize -> Wsize.wsize -> bool
Sourceval wsize_le : Wsize.wsize -> Wsize.wsize -> bool
Sourceval int_of_pe : Wsize.pelem -> int
Sourceval int_of_velem : Wsize.velem -> int
Sourceval is_ty_arr : 'e gty -> bool
Sourceval array_kind : 'e gty -> Wsize.wsize * 'e
Sourceval ws_of_ty : 'e gty -> Wsize.wsize
Sourceval arr_size : Wsize.wsize -> int -> int
Sourceval size_of : ty -> int
Sourceval access_offset : Warray_.arr_access -> Wsize.wsize -> int -> int
Sourceval is_stack_var : var -> bool
Sourceval is_reg_arr : var -> bool
Sourceval is_stack_array : var_i -> bool
Sourceval (++) : 'len gexpr -> 'len gexpr -> 'len gexpr
Sourceval (**) : 'len gexpr -> 'len gexpr -> 'len gexpr
Sourceval cnst : Z.t -> 'len gexpr
Sourceval icnst : int -> 'len gexpr
Sourceval is_var : 'len gexpr -> bool
Sourceval get_ofs : Warray_.arr_access -> Wsize.wsize -> 'len gexpr -> int option
Sourceval expr_of_lval : 'len glval -> 'len gexpr option
Sourceval has_syscall : ('len, 'info, 'asm) gstmt -> bool
Sourceval has_call_or_syscall : ('len, 'info, 'asm) gstmt -> bool
Sourceval has_annot : Annotations.symbol -> ('len, 'info, 'asm) ginstr -> bool
Sourceval assigns : ('info, 'asm) instr_r -> Sv.t

Computes the set of variables that the given instruction writes to, if any. NB: control flow instructions (if, while, and for) do not write to any variable.

Sourceval has_effect : ('info, 'asm) instr_r -> bool

Whether the instruction has an “effect”. What is treated as an effect is:

  • a function call / system call;
  • a memory store.

Note that other control-flow constructions do not count as an effect (i.e., this function does not recurse within nested code blocks).

Sourceval iter_instr : (('len, 'info, 'asm) ginstr -> unit) -> ('len, 'info, 'asm) gstmt -> unit

iter_instr f c traverses statement c and applies function f to every instruction.

Sourceval clamp : Wsize.wsize -> Z.t -> Z.t
Sourcetype ('info, 'asm) sfundef = Expr.stk_fun_extra * ('info, 'asm) func
Sourcetype ('info, 'asm) sprog = ('info, 'asm) sfundef list * Expr.sprog_extra