1
- (*
1
+ (* The meaning of keywords [strict] and [never_returns_normally] is defined in
2
+ terms of abstract values as follows:
2
3
3
- The meaning of keywords [strict] and [never_returns_normally]
4
- is defined in terms of abstract values as follows:
4
+ relaxed (default): nor = Safe and exn = Top and div = Top strict: nor = Safe
5
+ and exn = Safe and div = Safe never_returns_normally: nor = Bot and exn = Top
6
+ and div = Top
5
7
6
- relaxed (default): nor = Safe and exn = Top and div = Top
7
- strict: nor = Safe and exn = Safe and div = Safe
8
- never_returns_normally: nor = Bot and exn = Top and div = Top
8
+ where [nor] means normal return of the call, [ exn] means return via an
9
+ exception, [div] means diverging (non-terminating) executions, and the
10
+ meaning and order of elements is:
9
11
10
- where [nor] means normal return of the call, [exn] means return via an exception,
11
- [div] means diverging (non-terminating) executions,
12
- and the meaning and order of elements is:
12
+ Top may allocate Safe does not allocate on any execution paths Bot
13
+ unreachable
13
14
14
- Top may allocate
15
- Safe does not allocate on any execution paths
16
- Bot unreachable
17
-
18
- Using more than one keyword means intersection (i.e., meet of the elements,
15
+ Using more than one keyword means intersection (i.e., meet of the elements,
19
16
pointwise lifted to tuples), so we get the following:
20
17
21
- [@zero_alloc assume] nor = Safe and exn = Top and div = Top
22
- [@zero_alloc assume strict] nor = Safe and exn = Safe and div = Safe
23
- [@zero_alloc assume strict never_returns_normally] nor = Bot and exn = Safe and div = Safe
24
- [@zero_alloc assume never_returns_normally] nor = Bot and exn = Top and div = Top
18
+ [@zero_alloc assume] nor = Safe and exn = Top and div = Top [@zero_alloc
19
+ assume strict] nor = Safe and exn = Safe and div = Safe [@zero_alloc assume
20
+ strict never_returns_normally] nor = Bot and exn = Safe and div = Safe
21
+ [@zero_alloc assume never_returns_normally] nor = Bot and exn = Top and div =
22
+ Top
25
23
26
- See [Value] and [Annotation] in [backend/checkmach.ml].
27
- *)
28
- (* CR gyorsh: should we move [Value] and [Annotation] here or maybe "utils" and use them
29
- directly, instead of the weird compare function that abstracts them? Perhaps we
30
- should translate "strict" and "never_returns_normally" directly into (nor,exn,div)
31
- *)
24
+ See [Value] and [Annotation] in [backend/checkmach.ml]. *)
25
+ (* CR gyorsh: should we move [Value] and [Annotation] here or maybe "utils" and
26
+ use them directly, instead of the weird compare function that abstracts them?
27
+ Perhaps we should translate "strict" and "never_returns_normally" directly
28
+ into (nor,exn,div) *)
32
29
33
30
module Witnesses = struct
34
31
type t = unit
35
32
36
33
let join _ _ = ()
34
+
37
35
let lessequal _ _ = true
36
+
38
37
let meet _ _ = ()
38
+
39
39
let print _ _ = ()
40
+
40
41
let empty = ()
42
+
41
43
let compare _ _ = 0
42
44
end
43
45
44
46
include Zero_alloc_utils. Make (Witnesses )
45
47
46
- type t = No_assume | Assume of Value .t
48
+ type t =
49
+ | No_assume
50
+ | Assume of Value .t
47
51
48
52
let compare t1 t2 =
49
- match ( t1, t2) with
53
+ match t1, t2 with
50
54
| No_assume , No_assume -> 0
51
55
| Assume v1 , Assume v2 -> Value. compare v1 v2
52
56
| No_assume , Assume _ -> - 1
@@ -61,44 +65,24 @@ let print ppf = function
61
65
let to_string v = Format. asprintf " %a" print v
62
66
63
67
let join t1 t2 =
64
- match ( t1, t2) with
68
+ match t1, t2 with
65
69
| No_assume , No_assume -> No_assume
66
- | No_assume , Assume _
67
- | Assume _ , No_assume ->
68
- No_assume
70
+ | No_assume , Assume _ | Assume _ , No_assume -> No_assume
69
71
| Assume t1 , Assume t2 -> Assume (Value. join t1 t2)
70
72
71
73
let meet t1 t2 =
72
- match ( t1, t2) with
74
+ match t1, t2 with
73
75
| No_assume , No_assume -> No_assume
74
- | No_assume , (Assume _ as t)
75
- | (Assume _ as t ), No_assume ->
76
- t
76
+ | No_assume , (Assume _ as t ) | (Assume _ as t ), No_assume -> t
77
77
| Assume t1 , Assume t2 -> Assume (Value. meet t1 t2)
78
78
79
79
let none = No_assume
80
80
81
81
let create ~strict ~never_returns_normally =
82
- let res =
83
- if strict then
84
- Value. safe
85
- else
86
- Value. relaxed Witnesses. empty
87
- in
88
- let res =
89
- if never_returns_normally then
90
- { res with nor = V. Bot }
91
- else
92
- res
93
- in
82
+ let res = if strict then Value. safe else Value. relaxed Witnesses. empty in
83
+ let res = if never_returns_normally then { res with nor = V. Bot } else res in
94
84
Assume res
95
85
96
- let get_value t =
97
- match t with
98
- | No_assume -> None
99
- | Assume v -> Some v
86
+ let get_value t = match t with No_assume -> None | Assume v -> Some v
100
87
101
- let is_none t =
102
- match t with
103
- | No_assume -> true
104
- | Assume _ -> false
88
+ let is_none t = match t with No_assume -> true | Assume _ -> false
0 commit comments