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