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
|
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_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)
(* 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 = top (* TODO *)
let rem a b = top (* TODO *)
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
|
