summaryrefslogtreecommitdiffstats
path: root/abstract/constant_domain.ml
blob: 4bd5cf21253566efdcc547abef2bf2ecee874649 (plain) (blame)
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

open Value_domain

module Constants : VALUE_DOMAIN = struct
    type t =
        | Top
        | Int of Z.t
        | Bot
    
    let top = Top
    let bottom = Bot
    let const i = Int i
    let rand i j = if i <> j then Top else Int i

    let subset a b = match a, b with
        | _, Top -> true
        | Bot, _ -> true
        | Int a, Int b -> a = b
        | _, _ -> false
    
    let join a b = match a, b with
        | Bot, x | x, Bot -> x
        | Int a, Int b when a = b -> Int a
        | _ -> Top
    
    let meet a b = match a, b with
        | Top, x | x, Top -> x
        | Int a, Int b when a = b -> Int a
        | _ -> Bot
    
    let widen = meet        (* pas besoin d'accélerer la convergence au-delà *)

    let neg = function
        | Int a -> Int (Z.neg a)
        | x -> x
    
    let b_aux op a b = match a, b with
        | Int x, Int y -> Int (op x y)
        | Bot, _ | _, Bot -> Bot
        | _ -> Top
    let add = b_aux Z.add
    let sub = b_aux Z.sub
    let mul = b_aux Z.mul
    let div = b_aux Z.div
    let rem = b_aux Z.rem

    let leq a b =
        match a, b with
        | Int a, Int b when Z.leq a b ->
            if Z.leq a b
                then Int a, Int b
                else Bot, Bot
        | x, y -> x, y
end