package jasmin

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

Module Jasmin.CompileSource

Sourceval preprocess : Wsize.wsize -> 'asm Sopn.asmOp -> (unit, 'asm) Prog.pprog -> (unit, 'asm) Prog.prog

Preprocessing before translation to Coq representation:

  • substitution of parameters;
  • inserts `#copy` operators where needed;
  • fixes the length information in `Ocopy` operations;
  • typechecks the result.

Raises `Typing.TyError`.

Sourceval parse_file : ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Pretyping.arch_info -> ?idirs:(string * string) list -> string -> ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Arch_extra.extended_op Pretyping.Env.env * (unit, ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Arch_extra.extended_op) Prog.pmod_item list * Syntax.pprogram

Parsing and pre-typing of a complete file. Require directives are resolved using named path given through the idirs argument and the JASMINPATH environment variable.

Raises `Pretyping.TyError` and `Syntax.ParseError`.

Sourceval do_spill_unspill : 'asm Sopn.asmOp -> ?debug:bool -> (unit, 'asm) Prog.prog -> ((unit, 'asm) Prog.prog, Utils.hierror) result

Removes (aka implements) #spill and #unspill instructions.

Sourceval do_wint_int : (module Arch_full.Arch with type asm_op = 'asm_op and type cond = 'cond and type extra_op = 'extra_op and type reg = 'reg and type regx = 'regx and type rflag = 'rflag and type xreg = 'xreg) -> (unit, ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Arch_extra.extended_op Sopn.asm_op_t) Prog.prog -> (unit, ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Arch_extra.extended_op Sopn.asm_op_t) Prog.prog
Sourceval compile : (module Arch_full.Arch with type asm_op = 'asm_op and type cond = 'cond and type extra_op = 'extra_op and type reg = 'reg and type regx = 'regx and type rflag = 'rflag and type xreg = 'xreg) -> (debug:bool -> Compiler.compiler_step -> (unit, ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Arch_extra.extended_op Sopn.asm_op_t) Prog.prog -> unit) -> (_, _) Prog.prog -> ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Arch_extra.extended_op Expr._uprog -> ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) Arch_decl.asm_prog Compiler_util.cexec