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
|
open Value_domain
module VD : VALUE_DOMAIN = struct
type t = itv
(* utilities *)
let bound_leq a b = (* a <= b ? *)
match a, b with
| MInf, _ | _, PInf -> true
| Int a, Int b -> 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 (a + b)
| _ -> assert false
let bound_mul a b =
match a, b with
| PInf, Int(x) | Int(x), PInf ->
if x > 0 then PInf
else if x < 0 then MInf
else Int 0
| MInf, Int(x) | Int(x), MInf ->
if x < 0 then PInf
else if x > 0 then MInf
else Int 0
| Int(x), Int(y) -> Int(x * y)
| MInf, PInf | PInf, MInf -> MInf
| MInf, MInf | PInf, PInf -> PInf
let bound_div a b =
match a, b with
| _, PInf | _, MInf -> Int 0
| PInf, Int i ->
if i < 0 then MInf
else PInf
| MInf, Int i ->
if i < 0 then PInf
else MInf
| Int i, Int j ->
assert (j != 0);
Int (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 (- 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 i <= j then Itv(Int i, Int j) else Bot
let to_itv x = x
let as_const = function
| Itv(Int i, Int j) when i = j -> Some i
| _ -> None
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
(if bound_leq (Int 0) c then Int 0 else MInf)
else a),
(if not (bound_leq d b) then
(if bound_leq d (Int 0) then Int 0 else 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 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 (-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 0,
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 to_string = string_of_itv
end
|
