package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Linearization

module E : sig ... end
type 'asm_op linearization_params = {
  1. lip_tmp : Ident.Ident.ident;
  2. lip_tmp2 : Ident.Ident.ident;
  3. lip_not_saved_stack : Ident.Ident.ident list;
  4. lip_allocate_stack_frame : Expr.var_i -> Expr.var_i option -> BinNums.coq_Z -> ((Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list) list;
  5. lip_free_stack_frame : Expr.var_i -> Expr.var_i option -> BinNums.coq_Z -> ((Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list) list;
  6. lip_set_up_sp_register : Expr.var_i -> BinNums.coq_Z -> Wsize.wsize -> Expr.var_i -> Expr.var_i -> ((Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list) list;
  7. lip_lmove : Expr.var_i -> Expr.var_i -> (Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list;
  8. lip_check_ws : Wsize.wsize -> bool;
  9. lip_lstore : Expr.var_i -> BinNums.coq_Z -> Expr.var_i -> (Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list;
  10. lip_lload : Expr.var_i -> Expr.var_i -> BinNums.coq_Z -> (Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list;
  11. lip_lstores : Expr.var_i -> (Var0.Var.var * BinNums.coq_Z) list -> ((Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list) list;
  12. lip_lloads : Expr.var_i -> (Var0.Var.var * BinNums.coq_Z) list -> BinNums.coq_Z -> ((Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list) list;
}
val lstores_dfl : 'a1 Sopn.asmOp -> (Expr.var_i -> BinNums.coq_Z -> Expr.var_i -> (Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) -> Expr.var_i -> (Var0.Var.var * BinNums.coq_Z) list -> ((Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) list
val lstores_imm_dfl : Wsize.coq_PointerData -> 'a1 Sopn.asmOp -> Ident.Ident.ident -> (Expr.var_i -> BinNums.coq_Z -> Expr.var_i -> (Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) -> (Expr.var_i -> Expr.var_i -> BinNums.coq_Z -> ((Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) list) -> (BinNums.coq_Z -> bool) -> Expr.var_i -> (Var0.Var.var * BinNums.coq_Z) list -> ((Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) list
val lloads_aux : 'a1 Sopn.asmOp -> (Expr.var_i -> Expr.var_i -> BinNums.coq_Z -> (Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) -> Expr.var_i -> (Var0.Var.var * BinNums.coq_Z) list -> ((Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) list
val lloads_dfl : 'a1 Sopn.asmOp -> (Expr.var_i -> Expr.var_i -> BinNums.coq_Z -> (Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) -> Expr.var_i -> (Var0.Var.var * BinNums.coq_Z) list -> BinNums.coq_Z -> ((Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) list
val lloads_imm_dfl : Wsize.coq_PointerData -> 'a1 Sopn.asmOp -> Ident.Ident.ident -> (Expr.var_i -> Expr.var_i -> BinNums.coq_Z -> (Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) -> (Expr.var_i -> Expr.var_i -> BinNums.coq_Z -> ((Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) list) -> (BinNums.coq_Z -> bool) -> Expr.var_i -> (Var0.Var.var * BinNums.coq_Z) list -> BinNums.coq_Z -> ((Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) list
val check_Some : (string -> 'a1) -> ('a2 -> 'a3 option) -> string -> 'a2 -> ('a1, unit) Utils0.result
val to_fexpr : Expr.pexpr -> Fexpr.fexpr
val ovar_of_ra : Expr.return_address_location -> Var0.Var.var option
val ovari_of_ra : Expr.return_address_location -> Expr.var_i option
val tmp_of_ra : Expr.return_address_location -> Var0.Var.var option
val tmpi_of_ra : Expr.return_address_location -> Expr.var_i option
val stack_frame_allocation_size : Expr.stk_fun_extra -> BinNums.coq_Z
val frame_size : Expr.stk_fun_extra -> BinNums.coq_Z
val check_c : 'a1 Sopn.asmOp -> ('a1 Expr.instr -> unit Compiler_util.cexec) -> 'a1 Expr.instr list -> unit Compiler_util.cexec
val linear_c : 'a1 Sopn.asmOp -> ('a1 Expr.instr -> Label.label -> 'a1 Linear.lcmd -> Label.label * 'a1 Linear.lcmd) -> 'a1 Expr.instr list -> Label.label -> 'a1 Linear.lcmd -> Label.label * 'a1 Linear.lcmd
val add_align : 'a1 Sopn.asmOp -> Expr.instr_info -> Expr.align -> 'a1 Linear.lcmd -> 'a1 Linear.linstr list
val ov_type_ptr : Wsize.coq_PointerData -> Var0.Var.var option -> bool
val allocate_stack_frame : Wsize.coq_PointerData -> 'a1 Sopn.asmOp -> 'a1 linearization_params -> 'a1 Expr.sprog -> bool -> Expr.instr_info -> BinNums.coq_Z -> Expr.var_i option -> bool -> 'a1 Linear.lcmd
val is_RAstack_None_call : Expr.return_address_location -> bool
val is_RAstack_None_return : Expr.return_address_location -> bool
val linear_body : Wsize.coq_PointerData -> 'a1 Sopn.asmOp -> 'a1 linearization_params -> 'a1 Expr.sprog -> Var0.funname -> Expr.fun_info -> Expr.stk_fun_extra -> 'a1 Expr.instr list -> Label.label * 'a1 Linear.lcmd