Module `Jasmin.Linearization`

module E : sig ... end

type 'asm_op linearization_params = {

lip_tmp : Ident.Ident.ident;
lip_tmp2 : Ident.Ident.ident;
lip_not_saved_stack : Ident.Ident.ident list;
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;
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;
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;
lip_lmove : Expr.var_i -> Expr.var_i -> (Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list;
lip_check_ws : Wsize.wsize -> bool;
lip_lstore : Expr.var_i -> BinNums.coq_Z -> Expr.var_i -> (Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list;
lip_lload : Expr.var_i -> Expr.var_i -> BinNums.coq_Z -> (Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list;
lip_lstores : Expr.var_i -> (Var0.Var.var * BinNums.coq_Z) list -> ((Fexpr.lexpr list * 'asm_op Sopn.sopn) * Fexpr.rexpr list) list;
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 lmove : 
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  Expr.instr_info ->
  Expr.var_i ->
  Expr.var_i ->
  'a1 Linear.linstr

val lload : 
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  Expr.instr_info ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  'a1 Linear.linstr

val lstore : 
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  Expr.instr_info ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Expr.var_i ->
  'a1 Linear.linstr

val set_up_sp_register : 
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  Expr.instr_info ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Wsize.wsize ->
  Expr.var_i ->
  Expr.var_i ->
  'a1 Linear.lcmd

val check_Some : 
  (string -> 'a1) ->
  ('a2 -> 'a3 option) ->
  string ->
  'a2 ->
  ('a1, unit) Utils0.result

val to_fexpr : Expr.pexpr -> Fexpr.fexpr

val check_fexpr : 
  Expr.instr_info ->
  Expr.pexpr ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

val check_rexpr : 
  Expr.instr_info ->
  Expr.pexpr ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

val check_lexpr : 
  Expr.instr_info ->
  Expr.lval ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

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 push_to_save : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  'a1 Expr.sprog ->
  Expr.instr_info ->
  (Var0.Var.var * BinNums.coq_Z) list ->
  (Var0.Var.var * BinNums.coq_Z) ->
  'a1 Linear.lcmd

val pop_to_save : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  'a1 Expr.sprog ->
  Expr.instr_info ->
  (Var0.Var.var * BinNums.coq_Z) list ->
  BinNums.coq_Z ->
  'a1 Linear.lcmd

val check_c : 
  'a1 Sopn.asmOp ->
  ('a1 Expr.instr -> unit Compiler_util.cexec) ->
  'a1 Expr.instr list ->
  unit Compiler_util.cexec

val check_i : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 Expr.sprog ->
  Var0.funname ->
  Expr.stk_fun_extra ->
  'a1 Expr.instr ->
  unit Compiler_util.cexec

val check_to_save_slot : 
  (Var0.Var.var * BinNums.coq_Z) ->
  (BinNums.coq_Z * Wsize.wsize) Compiler_util.cexec

val all_disjoint_aligned_between : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  BinNums.coq_Z ->
  BinNums.coq_Z ->
  Wsize.wsize ->
  (Var0.Var.var * BinNums.coq_Z) list ->
  unit Compiler_util.cexec

val check_to_save : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  Expr.stk_fun_extra ->
  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 align : 
  'a1 Sopn.asmOp ->
  Expr.instr_info ->
  Expr.align ->
  (Label.label * 'a1 Linear.lcmd) ->
  Label.label * 'a1 Linear.lcmd

val ov_type_ptr : Wsize.coq_PointerData -> Var0.Var.var option -> bool

val check_fd : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  'a1 Expr.sprog ->
  Var0.funname ->
  'a1 Expr.sfundef ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

val check_prog : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  'a1 Expr.sprog ->
  (Compiler_util.pp_error_loc, unit) Utils0.result

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_i : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  'a1 Expr.sprog ->
  Var0.funname ->
  'a1 Expr.instr ->
  Label.label ->
  'a1 Linear.lcmd ->
  Label.label * 'a1 Linear.lcmd

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

val linear_fd : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  'a1 Expr.sprog ->
  Var0.funname ->
  'a1 Expr.sfundef ->
  Label.label * 'a1 Linear.lfundef

val linear_prog : 
  Wsize.coq_PointerData ->
  'a1 Sopn.asmOp ->
  'a1 linearization_params ->
  'a1 Expr.sprog ->
  'a1 Linear.lprog Compiler_util.cexec

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/Linearization/index.html

Module `Jasmin.Linearization`

package jasmin

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/Linearization/index.html

Module Jasmin.Linearization

dune-project
Dependency

Module `Jasmin.Linearization`