Quickcheck int domain abstract operation properties

[sim642]

For example, def_exc domain implements logand in a non-commutative way:

analyzer/src/cdomain/value/cdomains/intDomain.ml

Lines 2280 to 2291 in 9a8dd4e

	let logand ik x y = norm ik (match x,y with
	(* We don't bother with exclusion sets: *)
	| `Excluded _, `Definite i ->
	(* Except in two special cases *)
	if Z.equal i Z.zero then
	`Definite Z.zero
	else if Z.equal i Z.one then
	of_interval IBool (Z.zero, Z.one)
	else
	top ()
	| `Definite _, `Excluded _
	| `Excluded _, `Excluded _ -> top ()

Same for intervals:

analyzer/src/cdomain/value/cdomains/intDomain.ml

Lines 826 to 835 in 9a8dd4e

	let logand ik i1 i2 =
	match is_bot i1, is_bot i2 with
	| true, true -> bot_of ik
	| true, _
	| _ , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show i1) (show i2)))
	| _ ->
	match to_int i1, to_int i2 with
	| Some x, Some y -> (try of_int ik (Ints_t.logand x y) |> fst with Division_by_zero -> top_of ik)
	| _, Some y when Ints_t.equal y Ints_t.zero -> of_int ik Ints_t.zero |> fst
	| _, Some y when Ints_t.equal y Ints_t.one -> of_interval ik (Ints_t.zero, Ints_t.one) |> fst

And congruences:

analyzer/src/cdomain/value/cdomains/intDomain.ml

Lines 3094 to 3104 in 9a8dd4e

	let logand ik x y = match x, y with
	| None, None -> None
	| None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
	| Some (c, m), Some (c', m') ->
	if m =: Z.zero && m' =: Z.zero then
	(* both arguments constant *)
	Some (Z.logand c c', Z.zero)
	else if m' =: Z.zero && c' =: Z.one && Z.rem m (Z.of_int 2) =: Z.zero then
	(* x & 1 and x == c (mod 2*z) *)
	(* Value is equal to LSB of c *)
	Some (Z.logand c c', Z.zero)

The int domain property-based tests check lattice properties (like commutativity of join) and abstraction properties (like abstract logand overapproximates concrete logand) but not properties like commutativity of logand. Such property-based tests could be added for many int domain abstract operations for commutativity, associativity, etc.