package jasmin

  1. Overview
  2. Docs
Compiler for High-Assurance and High-Speed Cryptography

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (18)

Authors

  1. J
    Jasmin authors and contributors

Maintainers

  1. J
    Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Sources

jasmin-compiler-v2025.06.2.tar.bz2
sha256=aa0d21f532c1560a0939244cfd1c8414ba2b42c9d1403960f458500446cb1ebb

doc/jasmin.linter/Linter/BackwardAnalyser/module-type-Logic/index.html

Module type BackwardAnalyser.Logic

module type Logic : Abstract interface for the logic of the forward analysis. The user must provides :

  • domain type
  • functions to modify the domain (intialisation, pretty printing, inclusion test, merge, spliting)
  • function to handle atomic instructions (assign, function call, syscall, opn)

Control flow is handled by the Make functor (user don't have to implement it).

type domain

Type of the domain used for the analysis

val initialize : ('info, 'asm) Jasmin.Prog.func -> domain Annotation.annotation

Build the initial value of the domain using the function passed as argument.

args :

  • ('info,'asm) Prog.func (function to analyse)

returns :

  • domain (intial domain)

Pretty printer for the domain.

args :

  • Format.formatter (formatter to use)
  • domain (domain to print)
val included : domain -> domain -> bool

Inclusion test for the domain. included a b test if a is included in b

args :

  • domain (first domain)
  • domain (second domain)

returns :

  • bool (true if first domain is included in the second one)

Control flow function used to handle conditionnal branches. assume build an annotation such that : for all A1, A2, e, s ; s in I(account e A1 A2) => s in I(if es then A1 else A2)

Function to remove a variable from a domain. This function is needed because of the way we handle for loops. args :

  • Jasmin.Prog.var_i (variable to remove)
  • domain (domain to update)

returns :

  • domain Annotation.annotation (updated domain wrap with annotation type)

Function to handle function call instruction

Function to handle syscall instruction

Function to handle assign instruction

Function to handle opn instruction