path: root/abstract/constant_domain.ml

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 Bot else 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 = join        (* 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 a b = match a, b with
        | Int x, Int y -> Int (Z.mul x y)
        | Bot, _ | _, Bot -> Bot
        | Int x, _ when x = Z.zero -> Int Z.zero
        | _, Int x when x = Z.zero -> Int (Z.zero)
        | _ -> Top
    let div a b = match a, b with
        | Int x, Int y -> Int (Z.div x y)
        | Bot, _ | _, Bot -> Bot
        | Int x, _ when x = Z.zero -> Int Z.zero
        | _ -> Top
    let rem a b = match a, b with
        | Int x, Int y -> Int (Z.rem x y)
        | Bot, _ | _, Bot -> Bot
        | Int x, _ when x = Z.zero -> Int Z.zero
        | _ -> Top

    let leq a b =
        match a, b with
        | Int a, Int b ->
            if Z.leq a b
                then Int a, Int b
                else Bot, Bot
        | x, y -> x, y
    
    let to_string = function
        | Bot -> "bot"
        | Top -> "top"
        | Int i -> "{" ^ (Z.to_string i) ^ "}"
end