Source file l2lCheckMemSafe.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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
(** Time-stamp: <modified the 29/08/2019 (at 15:40) by Erwan Jahier> *)
open Lxm
open Lic
let _dbg = (Lv6Verbose.get_flag "check-mem")
let (is_memoryless_val_exp : LicPrg.t -> Lic.val_exp -> bool) =
fun licprg ve ->
let rec (aux_val_exp : Lic.val_exp -> bool) =
fun ve -> aux_val_exp_core ve.ve_core
and aux_val_exp_core ve_core =
match ve_core with
| CallByPosLic(op, vel) -> (
(List.for_all aux_val_exp vel) && aux_pos_op op.it
)
| CallByNameLic(_,cl) -> (
let vel = (snd (List.split cl)) in
List.for_all aux_val_exp vel
)
| Merge(ve,cl) -> (
let vel = ve::(snd (List.split cl)) in
List.for_all aux_val_exp vel
)
and (aux_pos_op: Lic.by_pos_op -> bool) =
function
| CALL({it=nk;_}) | PREDEF_CALL({it=nk;_}) -> (
match LicPrg.find_node licprg nk with
| None -> true
| Some node_exp -> not node_exp.has_mem_eff
)
| CURRENT _ | PRE | ARROW | FBY
-> false
| HAT (_) | ARRAY| ARRAY_SLICE(_) | ARRAY_ACCES(_) | STRUCT_ACCESS(_)
| WHEN _ | TUPLE | CONCAT | CONST _ | CONST_REF _ | VAR_REF _
-> true
in
aux_val_exp ve
let (check_memory : LicPrg.t -> bool -> val_exp -> Lxm.t -> bool -> bool) =
fun licprg should_have_mem ve lxm warning ->
match should_have_mem, not (is_memoryless_val_exp licprg ve) with
| false, false
| true, true -> false
| false, true ->
let msg = "Error: this call uses memory from a function." in
raise (Lv6errors.Compile_error(lxm,msg))
| true, false -> warning
let (is_safe_val_exp : LicPrg.t -> Lic.val_exp -> bool) =
fun licprg ve ->
let rec (aux_val_exp : Lic.val_exp -> bool) =
fun ve -> aux_val_exp_core ve.ve_core
and aux_val_exp_core ve_core =
match ve_core with
| CallByPosLic(op, vel) -> (
(List.for_all aux_val_exp vel) && aux_pos_op op.it
)
| CallByNameLic(_,cl) -> (
let vel = (snd (List.split cl)) in
List.for_all aux_val_exp vel
)
| Merge(ve,cl) -> (
let vel = ve::(snd (List.split cl)) in
List.for_all aux_val_exp vel
)
and (aux_pos_op: Lic.by_pos_op -> bool) =
function
| CALL({it=nk;_}) | PREDEF_CALL({it=nk;_}) -> (
match LicPrg.find_node licprg nk with
| None -> true
| Some node_exp -> node_exp.is_safe_eff
)
| CURRENT _ | PRE | ARROW | FBY
| HAT (_) | ARRAY| ARRAY_SLICE(_) | ARRAY_ACCES(_) | STRUCT_ACCESS(_)
| WHEN _ | TUPLE | CONCAT | CONST _ | CONST_REF _ | VAR_REF _
-> true
in
aux_val_exp ve
let (check_safety : LicPrg.t -> bool -> val_exp -> Lxm.t -> bool -> bool) =
fun licprg should_be_safe ve lxm warning ->
match should_be_safe, is_safe_val_exp licprg ve with
| false, false
| true, true -> false
| true, false ->
let msg = "Error: calling an unsafe node from a safe one." in
raise (Lv6errors.Compile_error(lxm,msg))
| false, true -> warning
let (check_node : LicPrg.t -> Lic.node_exp -> unit) =
fun licprg node ->
match node.def_eff with
| ExternLic | MetaOpLic | AbstractLic _ -> ()
| BodyLic{ eqs_eff = eql ; asserts_eff = vel } ->
let warning = true in
let warning = List.fold_left
(fun warn eq -> check_memory licprg node.has_mem_eff (snd eq.it) eq.src warn)
warning eql
in
let warning = List.fold_left
(fun warn eq -> check_memory licprg node.has_mem_eff eq.it eq.src warn)
warning vel
in
if warning then (
let id = Lic.string_of_node_key node.node_key_eff in
let msg = Printf.sprintf
"%s is declared as a node, but it uses no memory (i.e., it is a function)."
id
in
Lv6errors.warning node.lxm msg;
);
let warning = true in
let warning = List.fold_left
(fun warn eq -> check_safety licprg node.is_safe_eff (snd eq.it) eq.src warn)
warning eql
in
let warning = List.fold_left
(fun warn eq -> check_safety licprg node.is_safe_eff eq.it eq.src warn)
warning vel
in
if warning then (
let id = Lic.string_of_node_key node.node_key_eff in
let msg = Printf.sprintf "%s is declared as unsafe, but is safe." id in
Lv6errors.warning node.lxm msg
)
let (doit : LicPrg.t -> unit) =
fun inprg ->
let (do_node : Lic.node_key -> Lic.node_exp -> unit) =
fun _nk ne -> check_node inprg ne
in
LicPrg.iter_nodes do_node inprg