AStat/domains/naked.ml

open Abstract_syntax_tree
open Value_domain
exception NeedTop
exception Absurd

module type NAKED_VALUE_DOMAIN =
sig
	type t

	val const: Z.t -> t
	val rand: Z.t -> Z.t -> t
	val minus: t -> t
	val binary: t -> t -> int_binary_op -> t
	
	val is_only_zero: t -> bool
	val multiples_of: t -> t
	val divisors_of:  t -> t
	val remainders:   t -> t
	val convex_sym:   t -> t

	val compatible: t -> compare_op -> t (* returns the arguments possibly on the right of a comp w t*)
	val compare: t -> t -> compare_op -> (t*t)
	val bwd_binary: t -> t -> int_binary_op -> t -> (t*t)
	
	val join: t -> t -> t
	val meet: t -> t -> t

	val widen: t -> t -> t
	val narrow: t -> t -> t
	val subset: t -> t -> bool

	val print: Format.formatter -> t -> unit
end

module AddTopBot (N : NAKED_VALUE_DOMAIN) : VALUE_DOMAIN = 
struct
	type t = Bot | Top | V of N.t
	
	let top = Top
	let bottom = Bot

	let is_bottom a = match a with
		| Bot -> true
		| _   -> false

	let is_top a = match a with
		| Top -> true
		| _   -> false

	let const c = try V (N.const c) with NeedTop -> Top
	let rand a b = try (if Z.equal a b then
			V (N.const a)
		else (if Z.leq a b then V (N.rand a b) else Bot)) with NeedTop -> Top

	let unary a op = try (match op with
		| AST_UNARY_PLUS -> a
		| AST_UNARY_MINUS -> (match a with
			| Top -> Top
			| Bot -> Bot
			| V t -> V (N.minus t)) ) with NeedTop -> Top

	let binary a b op = try( if (is_bottom a || is_bottom b) then (Bot)
		else match op with
		| AST_PLUS -> if (is_top a || is_top b) then Top else
				let V a', V b' = a, b in V (N.binary a' b' AST_PLUS)
		| AST_MINUS -> if (is_top a || is_top b) then Top else
				let V a', V b' = a, b in V (N.binary a' b' AST_MINUS)
		| AST_MULTIPLY -> (match a, b with
				| Top, Top -> Top
				| Top, V x | V x, Top -> V (N.multiples_of x)
				| V x, V y -> V(N.binary x y AST_MULTIPLY))
		| AST_DIVIDE -> (match a, b with
				| Top, Top -> Top
				| Top, V x -> if N.is_only_zero x then Bot else Top
				| V x, Top -> V(N.divisors_of x)
				| V x, V y -> if N.is_only_zero y then Bot else V(N.binary x y AST_DIVIDE))
		| AST_MODULO -> (match a, b with
				| Top, Top -> Top
				| Top, V x -> if N.is_only_zero x then Bot else V(N.convex_sym x) (* convex symetric hull *)
				| V x, Top -> V(N.remainders x)
				| V x, V y -> if N.is_only_zero y then Bot else V(N.binary x y AST_MODULO)) ) with NeedTop -> Top

	let compare a b op = match a, b with
		| Bot, _ | _, Bot -> Bot, Bot
		| Top, Top -> Top, Top (* We are non-relational ! *)
		| V x, Top -> V x, (try(V (N.compatible x op))with NeedTop->Top)(*We can't learn anything comparing to Top*)
		| Top, V x -> (try(V (N.compatible x (reverse op)))with NeedTop->Top), V x
		| V x, V y -> try( let a', b' = (N.compare x y op) in V a', V b' )with Absurd -> Bot,Bot

	let bwd_unary x op r =
		match r with
		| Top -> Top
		| Bot -> Bot
		| V r' -> (match x with
			| Top -> (match op with
					| AST_UNARY_PLUS  -> r
					| AST_UNARY_MINUS -> V(N.minus r'))
			| Bot -> Bot
			| V x' -> (match op with
					| AST_UNARY_PLUS -> (try(V (N.meet x' r') )with Absurd -> Bot)
					| AST_UNARY_MINUS -> try( V(N.meet x' (N.minus r')))with Absurd->Bot))
	let bwd_binary x y op r =
		match r with
		| Top -> x, y
		| Bot -> (match op with
				| AST_DIVIDE | AST_MODULO -> x, (try (V (N.const Z.zero) )with NeedTop->Top)
				| _ -> x, y (* This can only happen if one of x or y was already Bot *)
			)
		| V r' -> (match x, y with
			| Bot, _| _, Bot -> x,y
			| Top, Top -> x, y (*TODO: add some trivialities like a / b = 0 implies a == 0 *)
			| V a, Top -> (match op with
					| AST_PLUS     -> (V a, V (N.binary r' a  AST_MINUS))
					| AST_MINUS    -> (V a, V (N.binary a  r' AST_MINUS))
					(*
					If a can't be null, the values described by b are exactly the values taken by r'/a
					(there aren't any rounding issues because r' = ab IMPLIES b = r'/a.)
					If a and r' can be null, we can't deduce anything.
					If a can be null but r' can't, then b can take any value r'/a can (when a != 0)
					*)
					| AST_MULTIPLY -> let an, rn = N.subset (N.const Z.zero) a, N.subset (N.const Z.zero) r' in
						(match an, rn with
						| false, _    -> (V a, V (N.binary r' a AST_DIVIDE))
						| true, false -> if N.is_only_zero a then (V a, Bot) else V a, V (N.binary r' a AST_DIVIDE)
						| true, true  -> (V a, Top))
					| AST_DIVIDE | AST_MODULO -> x,y) (* divide has rounding issues, modulo makes my head hurt *)
			| Top, V a -> (match op with
					| AST_PLUS  -> (V (N.binary r' a AST_MINUS), V a)
					| AST_MINUS -> (V (N.binary r' a AST_PLUS),  V a)
					| AST_MULTIPLY -> let an, rn = N.subset (N.const Z.zero) a, N.subset (N.const Z.zero) r' in
						(match an, rn with
						| false, _    -> (V a, V (N.binary r' a AST_DIVIDE))
						| true, false -> if N.is_only_zero a then (V a, Bot) else V a, V (N.binary r' a AST_DIVIDE)
						| true, true  -> (V a, Top))
					| AST_DIVIDE | AST_MODULO -> x,y)
			| V a, V b -> try( let a',b' = (N.bwd_binary a b op r') in V a', V b' )with Absurd->(Bot,Bot) )

	let join a b = try (match a, b with
		| Top, x | x, Top -> Top
		| Bot, x | x, Bot -> x
		| V a', V b' -> V(N.join a' b') )with NeedTop -> Top
	let meet a b = match a, b with
		| Bot, x | x, Bot -> Bot
		| Top, x | x, Top -> x
		| V a', V b' -> try( V(N.meet a' b') )with Absurd -> Bot

	let widen a b = try( match a, b with
		| Bot, x | x, Bot -> x
		| Top, x | x, Top -> Top
		| V a', V b' -> V(N.widen a' b') )with NeedTop->Top

	let narrow a b = match a, b with
		| Bot, x | x, Bot -> Bot
		| Top, x | x, Top -> x
		| V a', V b' -> try( V(N.narrow a' b') )with Absurd -> Bot

	let subset a b = match a, b with
		| Bot, b -> true
		| b, Bot -> false
		| b, Top -> true
		| Top, b -> false
		| V a', V b' -> (N.subset a' b')
	let print out a =
		match a with
		| Top -> Format.fprintf out "T"
		| Bot -> Format.fprintf out "B"
		| V a' -> N.print out a'
end