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 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