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_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