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

Authors

  1. J
    Jasmin authors and contributors

Maintainers

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

Sources

jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa

doc/src/jasmin.jasmin/checkAnnot.ml.html

Source file checkAnnot.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
open Utils
open Glob_options
open Prog

let check_stack_size fds =
  List.iter
    (fun ( { Expr.sf_stk_sz; Expr.sf_stk_extra_sz; Expr.sf_align; Expr.sf_max_call_depth },
           { f_loc; f_annot; f_name } ) ->
      let hierror fmt =
        hierror ~loc:(Lone f_loc) ~funname:f_name.fn_name
          ~kind:"compilation error" ~sub_kind:"stack allocation" fmt
      in
      (match f_annot.stack_size with
      | None -> ()
      | Some expected ->
          let actual = Conv.z_of_cz sf_stk_sz in
          if Z.equal actual expected then (
            if !debug then
              Format.eprintf "INFO: %s has the expected stack size (%a)@."
                f_name.fn_name Z.pp_print expected)
          else
            hierror "the stack has size %a (expected: %a)" Z.pp_print actual
              Z.pp_print expected);
      (match f_annot.stack_allocation_size with
      | None -> ()
      | Some expected ->
          let actual =
            Conv.z_of_cz
              (Memory_model.round_ws sf_align
                 (BinInt.Z.add sf_stk_sz sf_stk_extra_sz))
          in
          if Z.equal actual expected then (
            if !debug then
              Format.eprintf "INFO: %s has the expected stack size (%a)@."
                f_name.fn_name Z.pp_print expected)
          else
            hierror "the stack has size %a (expected: %a)" Z.pp_print actual
              Z.pp_print expected);
      (match f_annot.stack_align with
      | None -> ()
      | Some expected ->
          let actual = sf_align in
          if actual = expected then (
            if !debug then
              Format.eprintf "INFO: %s has the expected stack alignment (%s)@."
                f_name.fn_name (string_of_ws expected))
          else
            hierror "the stack has alignment %s (expected: %s)"
              (string_of_ws actual) (string_of_ws expected));
      match f_annot.max_call_depth with
      | None -> ()
      | Some expected ->
          let actual = Conv.z_of_cz sf_max_call_depth in
          if actual = expected then (
            if !debug then
              Format.eprintf "INFO: %s has the expected max call depth (%a)@."
                f_name.fn_name Z.pp_print expected)
            else
              hierror "the maximum call depth is %a (expected: %a)"
                Z.pp_print actual Z.pp_print expected)
    fds