package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa
doc/jasmin.jasmin/Jasmin/Compile/index.html
Module Jasmin.CompileSource
Source
val preprocess :
Wsize.wsize ->
'asm Sopn.asmOp ->
(unit, 'asm) Prog.pprog ->
(unit, 'asm) Prog.progPreprocessing 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`.
Source
val 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.pprogramParsing 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`.
Source
val do_spill_unspill :
'asm Sopn.asmOp ->
?debug:bool ->
(unit, 'asm) Prog.prog ->
((unit, 'asm) Prog.prog, Utils.hierror) resultRemoves (aka implements) #spill and #unspill instructions.
Source
val 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.progSource
val 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