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 (19)

Authors

  1. J
    Jasmin authors and contributors

Maintainers

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

Sources

jasmin-compiler-v2025.06.3.tar.bz2
sha256=e7aafd891eb54e89d41d9d7d1bbda9ddb1cddc5fdf0359d88c2b7b417ae4a39b

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