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
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
open Value_domain
module Intervals : VALUE_DOMAIN = struct
type bound = Int of Z.t | PInf | MInf
type t = Itv of bound * bound | Bot
(* utilities *)
let bound_leq a b = (* a <= b ? *)
match a, b with
| MInf, _ | _, PInf -> true
| Int a, Int b -> Z.leq a b
| x, y -> x = y
let bound_add a b =
match a, b with
| MInf, Int a | Int a, MInf -> MInf
| PInf, Int a | Int a, PInf -> PInf
| MInf, MInf -> MInf
| PInf, PInf -> PInf
| Int a, Int b -> Int (Z.add a b)
| _ -> assert false
let bound_mul a b =
match a, b with
| PInf, Int(x) | Int(x), PInf ->
if x > Z.zero then PInf
else if x < Z.zero then MInf
else Int Z.zero
| MInf, Int(x) | Int(x), MInf ->
if x < Z.zero then PInf
else if x > Z.zero then MInf
else Int Z.zero
| Int(x), Int(y) -> Int(Z.mul x y)
| MInf, PInf | PInf, MInf -> MInf
| MInf, MInf | PInf, PInf -> PInf
let bound_div a b =
match a, b with
| _, PInf | _, MInf -> Int Z.zero
| PInf, Int i ->
if i < Z.zero then MInf
else PInf
| MInf, Int i ->
if i < Z.zero then PInf
else MInf
| Int i, Int j ->
if j = Z.zero then
if i < Z.zero then MInf
else PInf
else Int (Z.div i j)
let bound_min a b = match a, b with
| MInf, _ | _, MInf -> MInf
| Int a, Int b -> Int (min a b)
| Int a, PInf -> Int a
| PInf, Int a -> Int a
| PInf, PInf -> PInf
let bound_max a b = match a, b with
| PInf, _ | _, PInf -> PInf
| Int a, Int b -> Int (max a b)
| Int a, MInf | MInf, Int a -> Int a
| MInf, MInf -> MInf
let bound_neg = function
| PInf -> MInf
| MInf -> PInf
| Int i -> Int (Z.neg i)
let bound_abs a = bound_max a (bound_neg a)
(* implementation *)
let top = Itv(MInf, PInf)
let bottom = Bot
let const i = Itv(Int i, Int i)
let rand i j =
if Z.leq i j then Itv(Int i, Int j) else Bot
let subset a b = match a, b with
| Bot, _ -> true
| _, Bot -> false
| Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
let join a b = match a, b with
| Bot, x | x, Bot -> x
| Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)
let meet a b = match a, b with
| Bot, x | x, Bot -> Bot
| Itv(a, b), Itv(c, d) ->
let u, v = bound_max a c, bound_min b d in
if bound_leq u v
then Itv(u, v)
else Bot
let widen a b = match a, b with
| x, Bot | Bot, x -> x
| Itv(a, b), Itv(c, d) ->
Itv(
(if not (bound_leq a c) then MInf else a),
(if not (bound_leq d b) then PInf else b))
let neg = function
| Bot -> Bot
| Itv(a, b) -> Itv(bound_neg b, bound_neg a)
let add a b = match a, b with
| Bot, _ | _, Bot -> Bot
| Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
let sub a b = match a, b with
| Bot, _ | _, Bot -> Bot
| Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
let mul a b = match a, b with
| Bot, _ | _, Bot -> Bot
| Itv(a, b), Itv(c, d) ->
Itv(
(bound_min (bound_min (bound_mul a c) (bound_mul a d))
(bound_min (bound_mul b c) (bound_mul b d))),
(bound_max (bound_max (bound_mul a c) (bound_mul a d))
(bound_max (bound_mul b c) (bound_mul b d))))
let div a b = match a, b with
| Bot, _ -> Bot
| Itv(a, b), q ->
let p1 = match meet q (Itv(Int (Z.of_int 1), PInf)) with
| Bot -> Bot
| Itv(c, d) ->
Itv(min (bound_div a c) (bound_div a d), max (bound_div b c) (bound_div b d))
in
let p2 = match meet q (Itv(MInf, Int (Z.of_int (-1)))) with
| Bot -> Bot
| Itv(c, d) ->
Itv(min (bound_div b c) (bound_div b d), max (bound_div a c) (bound_div a d))
in
join p1 p2
let rem a b = match a, b with
| Bot, _ | _, Bot -> Bot
| Itv(a, b), Itv(c, d) ->
Itv(
Int Z.zero,
bound_max (bound_abs c) (bound_abs d)
)
let leq a b = match a, b with
| Bot, _ | _, Bot -> Bot, Bot
| Itv(a, b), Itv(c, d) ->
if not (bound_leq a d)
then Bot, Bot
else Itv(a, bound_min b d), Itv(bound_max a c, d)
let bound_str = function
| MInf -> "-oo"
| PInf -> "+oo"
| Int i -> Z.to_string i
let to_string = function
| Bot -> "bot"
| Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
end
|
