AStat/domains/sign.ml

open Naked
open Abstract_syntax_tree

module Signs : NAKED_VALUE_DOMAIN = struct
	type t = N | Z | P (*Negative/Zero/Positive (signs include 0)*)
	let const z = if (Z.equal Z.zero z) then Z else
			(if Z.lt z Z.zero then N else P)
	let rand a b = if Z.leq b Z.zero then N
			else (if Z.geq a Z.zero then P else raise NeedTop) (*We know a < b*)
	let minus a = match a with
		| N -> P | Z -> Z | P -> N
	let rec binary a b op = match op with
		| AST_PLUS -> (match a, b with
				| P, P | P, Z | Z, P -> P
				| Z, Z -> Z
				| _ -> N)
		| AST_MINUS -> binary a (minus b) AST_PLUS
		| AST_MULTIPLY -> (match a, b with
					| P, P | N, N -> P
					| Z, _ | _, Z -> Z
					| _ -> N)
		| AST_DIVIDE -> (match a, b with
				| _, Z -> raise Absurd
				| _ -> binary a b AST_MULTIPLY)
		| AST_MODULO -> a
	let is_only_zero a = match a with
		| Z -> true | _ -> false
	let multiples_of a = match a with
		| Z -> Z | _ -> raise NeedTop
	let divisors_of a = match a with
		| Z -> Z | _ -> raise NeedTop
	let remainders a = a
	let convex_sym a = match a with
		| Z -> Z | _ -> raise NeedTop

	let compatible a op = match op with
		| AST_EQUAL -> a
		| AST_NOT_EQUAL -> raise NeedTop
		| AST_LESS | AST_LESS_EQUAL -> if a == P || a == Z then P else raise NeedTop
		| AST_GREATER | AST_GREATER_EQUAL -> if a == N || a == Z then N else raise NeedTop
	let rec compare a b op = match op with
		| AST_EQUAL 	-> if a <> b then Z, Z else a, b
		| AST_NOT_EQUAL -> if a == b && a == Z then raise Absurd else a, b
		| AST_LESS_EQUAL -> (match b with
					| Z -> (match a with | P -> Z | Z -> Z | N -> N), b
					| N -> (match a with
						| P -> Z,Z
						| N -> N,N
						| Z -> Z,Z)
					| P -> a,b)
		| AST_LESS -> (match b with
				| Z -> (match a with | P -> raise Absurd | Z -> raise Absurd | N -> N), b
				| N -> (match a with
					| P -> raise Absurd
					| N -> N,N
					| Z -> raise Absurd)
				| P -> a,b)
		| AST_GREATER_EQUAL | AST_GREATER -> let b',a' = compare b a (reverse op) in a', b'

	let meet x y = match x,y with
			|P, N | N, P -> raise Absurd
			|Z, _ | _, Z -> Z
			|N, N | P, P -> x

	let rec bwd_binary a b op r = match op with
		| AST_PLUS -> (match r with
				| P -> (if a <> P && b <> P then Z,Z else a,b)
				| N -> (if a <> N && b <> N then Z,Z else a,b)
				| Z -> if a == b then Z,Z else a,b)
		| AST_MINUS -> let a', nb' = bwd_binary a (minus b) AST_PLUS r in (a', minus nb')
		| AST_MULTIPLY -> (match r with
				| Z -> a,b (*all products must be zero, so one is Z, but we don't know which...*)
				| P -> (match a, b with
					| P, P | N, N -> a,b
					| Z, _ | _, Z -> a,b
					| N, P | P, N -> a,b) (*all products are 0, so at least one is Z, but...*)
				| N -> let a', nb' = bwd_binary a (minus b) AST_MULTIPLY (minus r) in (a', minus nb'))
		| AST_DIVIDE -> if b == Z then raise Absurd else (*Here zeros don't bother us!*)
					(match r with
					| Z -> Z,b
					| P -> b,b
					| N -> b, minus b)
		| AST_MODULO -> if b == Z then raise Absurd else
				(meet a r,b)
	let join x y = match x,y with
			| P, N | N, P -> raise NeedTop
			| Z, a | a, Z -> a
			| N, N | P, P -> x
	let widen x y = join x y
	let narrow x y = meet x y
	let subset x y = x == y || (x == Z)
	let print out x = match x with
		| Z -> Format.fprintf out "0"
		| N -> Format.fprintf out "<=0"
		| P -> Format.fprintf out ">=0"
end