From 5606e678cc4dc3390639e69a7a31a02230d4f77e Mon Sep 17 00:00:00 2001 From: ManuelLerchner Date: Tue, 19 Nov 2024 17:20:26 +0100 Subject: [PATCH 01/25] logand fix --- src/cdomain/value/cdomains/intDomain.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 9eddc9767e..7648e83083 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1340,6 +1340,9 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let range ik bf = (BArith.min ik bf, BArith.max ik bf) let norm ?(suppress_ovwarn=false) ik (z,o) = + if BArith.is_undef (z,o) then + ((z,o), {underflow=false; overflow=false}) + else let (min_ik, max_ik) = Size.range ik in let (min,max) = range ik (z,o) in @@ -1399,9 +1402,9 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let of_interval ?(suppress_ovwarn=false) ik (x,y) = (* naive implentation -> horrible O(n) runtime *) let (min_ik, max_ik) = Size.range ik in - let current = ref (min_ik) in + let current = ref (Z.of_int (Ints_t.to_int x)) in let bf = ref (bot ()) in - while Z.leq !current max_ik do + while Z.leq !current (Z.of_int (Ints_t.to_int y)) do bf := BArith.join !bf (BArith.of_int (Ints_t.of_bigint !current)); current := Z.add !current Z.one done; @@ -1423,14 +1426,16 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int | None -> top_of ik | Some x -> of_bool ik (f x) - let log2 f ik i1 i2 = match (to_bool i1, to_bool i2) with - | None, None -> top_of ik - | None, Some x | Some x, None -> of_bool ik x + let log2 f ~annihilator ik i1 i2 = match to_bool i1, to_bool i2 with + | Some x, _ when x = annihilator -> of_bool ik annihilator + | _, Some y when y = annihilator -> of_bool ik annihilator | Some x, Some y -> of_bool ik (f x y) - let c_logor ik i1 i2 = log2 (||) ik i1 i2 + | _ -> top_of ik - let c_logand ik i1 i2 = log2 (&&) ik i1 i2 + let c_logor = log2 (||) ~annihilator:true + let c_logand = log2 (&&) ~annihilator:false + let c_lognot ik i1 = log1 not ik i1 From 8b1fbfc9ced84077ffe718114165558217c16d21 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adrian=20Krau=C3=9F?= Date: Tue, 19 Nov 2024 17:25:07 +0100 Subject: [PATCH 02/25] bug fixes for arith ops --- src/cdomain/value/cdomains/intDomain.ml | 63 +++++++++++++------------ 1 file changed, 32 insertions(+), 31 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 7648e83083..c85e20e5f8 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1465,11 +1465,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int of Vishwanathan et al. *) - let add ?no_ov ik (z1, o1) (z2, o2) = - let pv = Ints_t.logand o1 (Ints_t.lognot z1) in - let pm = Ints_t.logand o1 z1 in - let qv = Ints_t.logand o2 (Ints_t.lognot z2) in - let qm = Ints_t.logand o2 z2 in + let add_paper pv pm qv qm = let sv = Ints_t.add pv qv in let sm = Ints_t.add pm qm in let sigma = Ints_t.add sv sm in @@ -1477,6 +1473,14 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let mu = Ints_t.logor (Ints_t.logor pm qm) chi in let rv = Ints_t.logand sv (Ints_t.lognot mu) in let rm = mu in + (rv, rm) + + let add ?no_ov ik (z1, o1) (z2, o2) = + let pv = Ints_t.logand o1 (Ints_t.lognot z1) in + let pm = Ints_t.logand o1 z1 in + let qv = Ints_t.logand o2 (Ints_t.lognot z2) in + let qm = Ints_t.logand o2 z2 in + let (rv, rm) = add_paper pv pm qv qm in let o3 = Ints_t.logor rv rm in let z3 = Ints_t.logor (Ints_t.lognot rv) rm in norm ik (z3, o3) @@ -1502,42 +1506,39 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int sub ?no_ov ik BArith.zero x let mul ?no_ov ik (z1, o1) (z2, o2) = - let z1 = ref z1 in - let o1 = ref o1 in - let z2 = ref z2 in - let o2 = ref o2 in - let z3 = ref BArith.one_mask in - let o3 = ref BArith.zero_mask in + let pm = ref (Ints_t.logand z1 o1) in + let pv = ref (Ints_t.logand o1 (Ints_t.lognot z1)) in + let qm = ref (Ints_t.logand z2 o2) in + let qv = ref (Ints_t.logand o2 (Ints_t.lognot z2)) in + let accv = ref BArith.zero_mask in + let accm = ref BArith.zero_mask in let size = if isSigned ik then Size.bit ik - 1 else Size.bit ik in let bitmask = Ints_t.of_int(Z.to_int(Z.lognot (fst (Size.range ik)))) in - let signBitUndef1 = Ints_t.logand (Ints_t.logand !z1 !o1) bitmask in - let signBitUndef2 = Ints_t.logand (Ints_t.logand !z2 !o2) bitmask in + let signBitUndef1 = Ints_t.logand (Ints_t.logand z1 o1) bitmask in + let signBitUndef2 = Ints_t.logand (Ints_t.logand z2 o2) bitmask in let signBitUndef = Ints_t.logor signBitUndef1 signBitUndef2 in - let signBitDefO = Ints_t.logand (Ints_t.logxor !o1 !o2) bitmask in - let signBitDefZ = Ints_t.logand (Ints_t.lognot (Ints_t.logxor !o1 !o2)) bitmask in + let signBitDefO = Ints_t.logand (Ints_t.logxor o1 o2) bitmask in + let signBitDefZ = Ints_t.logand (Ints_t.lognot (Ints_t.logxor o1 o2)) bitmask in for i = size downto 0 do - (if Ints_t.logand !o1 Ints_t.one == Ints_t.one then - if Ints_t.logand !z1 Ints_t.one == Ints_t.one then - let tmp = Ints_t.add (Ints_t.logand !z3 !o3) !o2 in - z3 := Ints_t.logor !z3 tmp; - o3 := Ints_t.logor !o3 tmp - else - let tmp = fst (add ik (!z3, !o3) (!z2, !o2)) in - z3 := fst tmp; - o3 := snd tmp;); - - z1 := Ints_t.shift_right !z1 1; - o1 := Ints_t.shift_right !o1 1; - z2 := Ints_t.shift_left !z2 1; - o2 := Ints_t.shift_left !o2 1; + (if Ints_t.logand !pm Ints_t.one == Ints_t.one then + accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (Ints_t.logor !qv !qm)) + else if Ints_t.logand !pv Ints_t.one == Ints_t.one then + accv := fst(add_paper !accv Ints_t.zero !qv Ints_t.zero); + accm := snd(add_paper Ints_t.zero !accm Ints_t.zero !qm)); + + pv := Ints_t.shift_right !pv 1; + pm := Ints_t.shift_right !pm 1; + qv := Ints_t.shift_left !qv 1; + qm := Ints_t.shift_left !qm 1; done; + let o3 = ref(Ints_t.logor !accv !accm) in + let z3 = ref(Ints_t.logor (Ints_t.lognot !accv) !accm) in if isSigned ik then z3 := Ints_t.logor signBitUndef (Ints_t.logor signBitDefZ !z3); if isSigned ik then o3 := Ints_t.logor signBitUndef (Ints_t.logor signBitDefO !o3); - norm ik (!z3, !o3) let rec div ?no_ov ik (z1, o1) (z2, o2) = - let res = if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then (let tmp = Ints_t.div z1 z2 in (tmp, Ints_t.lognot tmp)) else top_of ik in + let res = if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then (let tmp = Ints_t.div z1 z2 in (Ints_t.lognot tmp, tmp)) else top_of ik in norm ik res let rem ik x y = From 4bf31cc004d9064f2e7f98e8d7f378442afcbdfe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adrian=20Krau=C3=9F?= Date: Tue, 19 Nov 2024 17:31:12 +0100 Subject: [PATCH 03/25] fixed norm --- src/cdomain/value/cdomains/intDomain.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index c85e20e5f8..f6e44eff5e 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1211,7 +1211,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let bits_undef (z,o) = Ints_t.lognot (Ints_t.logxor z o) let is_const (z,o) = (Ints_t.logxor z o) = one_mask - let is_undef (z,o) = Ints_t.compare (bits_undef (z,o)) Ints_t.zero != 0 + let is_invalid (z,o) = Ints_t.compare (Ints_t.lognot (Ints_t.logand z o)) Ints_t.zero != 0 let nabla x y= if x = Ints_t.logor x y then x else one_mask @@ -1246,7 +1246,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct in aux n 0 in ilog2 (Size.bit ik) - let break_down_lsb ik (z,o) : (Ints_t.t * Ints_t.t) list option = if is_undef (z,o) then None + let break_down_lsb ik (z,o) : (Ints_t.t * Ints_t.t) list option = if is_invalid (z,o) then None else let rec break_down c_lst i = if i < 0 then c_lst else @@ -1340,7 +1340,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let range ik bf = (BArith.min ik bf, BArith.max ik bf) let norm ?(suppress_ovwarn=false) ik (z,o) = - if BArith.is_undef (z,o) then + if BArith.is_invalid (z,o) then ((z,o), {underflow=false; overflow=false}) else let (min_ik, max_ik) = Size.range ik in From 0b4b4a10a7b5446309ba36c0e9147fddc61adf69 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adrian=20Krau=C3=9F?= Date: Tue, 19 Nov 2024 19:25:40 +0100 Subject: [PATCH 04/25] is_invalid and mul fix --- src/cdomain/value/cdomains/intDomain.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index f6e44eff5e..a97c5f055b 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1211,7 +1211,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let bits_undef (z,o) = Ints_t.lognot (Ints_t.logxor z o) let is_const (z,o) = (Ints_t.logxor z o) = one_mask - let is_invalid (z,o) = Ints_t.compare (Ints_t.lognot (Ints_t.logand z o)) Ints_t.zero != 0 + let is_invalid (z,o) = Ints_t.compare (Ints_t.lognot (Ints_t.logor z o)) Ints_t.zero != 0 let nabla x y= if x = Ints_t.logor x y then x else one_mask @@ -1513,13 +1513,13 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let accv = ref BArith.zero_mask in let accm = ref BArith.zero_mask in let size = if isSigned ik then Size.bit ik - 1 else Size.bit ik in - let bitmask = Ints_t.of_int(Z.to_int(Z.lognot (fst (Size.range ik)))) in + let bitmask = Ints_t.of_bigint (fst (Size.range ik)) in let signBitUndef1 = Ints_t.logand (Ints_t.logand z1 o1) bitmask in let signBitUndef2 = Ints_t.logand (Ints_t.logand z2 o2) bitmask in let signBitUndef = Ints_t.logor signBitUndef1 signBitUndef2 in let signBitDefO = Ints_t.logand (Ints_t.logxor o1 o2) bitmask in let signBitDefZ = Ints_t.logand (Ints_t.lognot (Ints_t.logxor o1 o2)) bitmask in - for i = size downto 0 do + for i = size downto 0 do (if Ints_t.logand !pm Ints_t.one == Ints_t.one then accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (Ints_t.logor !qv !qm)) else if Ints_t.logand !pv Ints_t.one == Ints_t.one then @@ -1530,9 +1530,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int pm := Ints_t.shift_right !pm 1; qv := Ints_t.shift_left !qv 1; qm := Ints_t.shift_left !qm 1; - done; - let o3 = ref(Ints_t.logor !accv !accm) in - let z3 = ref(Ints_t.logor (Ints_t.lognot !accv) !accm) in + done; + let (rv, rm) = add_paper !accv Ints_t.zero Ints_t.zero !accm in + let o3 = ref(Ints_t.logor rv rm) in + let z3 = ref(Ints_t.logor (Ints_t.lognot rv) rm) in if isSigned ik then z3 := Ints_t.logor signBitUndef (Ints_t.logor signBitDefZ !z3); if isSigned ik then o3 := Ints_t.logor signBitUndef (Ints_t.logor signBitDefO !o3); norm ik (!z3, !o3) From 15520a86696026603d50bc96193ac3d3a13e4e47 Mon Sep 17 00:00:00 2001 From: giaca Date: Tue, 19 Nov 2024 20:43:22 +0100 Subject: [PATCH 05/25] assertion function for shifts --- tests/unit/cdomains/intDomainTest.ml | 41 ++++++++++++---------------- 1 file changed, 17 insertions(+), 24 deletions(-) diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index ce72deded0..992480a6be 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -460,33 +460,26 @@ module I = IntDomain.SOverflowUnlifter (I) assert_bool "-13 ?= not (4 | 12)" (I.equal_to (of_int (-13)) (I.lognot ik b12) = `Top); assert_bool "-5 ?= not (4 | 12)" (I.equal_to (of_int (-5)) (I.lognot ik b12) = `Top) - let test_shift_left _ = - let stat1 = I.of_int ik (of_int 2) in - let stat2 = I.of_int ik (of_int 1) in - let eval = (I.shift_left ik stat1 stat2) in - let eq = (of_int(4)) in - assert_bool ("2 << 1 should be: \"4\" but was: \"" ^ I.show eval ^ "\"") (I.equal_to eq eval = `Eq); - - let stat1 = I.of_int ik (of_int (-2)) in - let stat2 = I.of_int ik (of_int 1) in - let eval = (I.shift_left ik stat1 stat2) in - let eq = (of_int(-4)) in - assert_bool ("2 << 1 should be: \"4\" but was: \"" ^ I.show eval ^ "\"") (I.equal_to eq eval = `Eq) + (* TODO assumes join to be correct *) + let assert_shift shift symb ik a b res = + let lst2bf lst = List.map (fun x -> I.of_int ik @@ of_int x) lst |> List.fold_left (I.join ik) (I.bot ()) in + let stat1 = lst2bf a in + let stat2 = lst2bf b in + let eval = (shift ik stat1 stat2) in + let eq = lst2bf res in + let out_string = I.show stat1 ^ symb ^ I.show stat2 ^ " should be : \"" ^ I.show eq ^ "\" but was \"" ^ I.show eval ^ "\"" in + OUnit2.assert_equal ~cmp:(fun x y -> Option.value ~default:false @@ I.to_bool @@ I.eq ik x y) ~msg:out_string eq eval (* TODO msg *) + + let assert_shift_left ik a b res = assert_shift I.shift_left "<<" ik a b res + let assert_shift_right ik a b res = assert_shift I.shift_right ">>" ik a b res + let test_shift_left _ = + assert_shift_left ik [2] [1] [4]; + assert_shift_left ik [-2] [1] [-4] let test_shift_right _ = - let stat1 = I.of_int ik (of_int (4)) in - let stat2 = I.of_int ik (of_int 1) in - let eval = (I.shift_right ik stat1 stat2) in - let eq = (of_int (2)) in - assert_bool ("4 >> 1 should be: \"2\" but was: \"" ^ I.show eval ^ "\"" ^ I.show stat1) (I.equal_to eq eval = `Eq); - - let stat1 = I.of_int ik (of_int (-4)) in - let stat2 = I.of_int ik (of_int 1) in - let eval = (I.shift_right ik stat1 stat2) in - let eq = (of_int (-2)) in - assert_bool ("4 >> 1 should be: \"2\" but was: \"" ^ I.show eval ^ "\"" ^ I.show stat1) (I.equal_to eq eval = `Eq) - + assert_shift_right ik [4] [1] [2]; + assert_shift_right ik [-4] [1] [-2] (* Arith *) From d55eab5f9035dc07d9dcf9d252f16ec31a829bd3 Mon Sep 17 00:00:00 2001 From: giaca Date: Tue, 19 Nov 2024 21:14:26 +0100 Subject: [PATCH 06/25] bug fix in get_bit and further tests that lead to fails --- src/cdomain/value/cdomains/intDomain.ml | 2 +- tests/unit/cdomains/intDomainTest.ml | 8 ++++++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index a97c5f055b..e31a31183a 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1231,7 +1231,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let make_lsb_bitmask pos = Ints_t.sub (make_bitone_msk pos) Ints_t.one let make_msb_bitmask pos = Ints_t.lognot @@ make_lsb_bitmask pos - let get_bit bf pos = Ints_t.logand Ints_t.one @@ Ints_t.shift_right bf (pos-1) + let get_bit bf pos = Ints_t.logand Ints_t.one @@ Ints_t.shift_right bf pos let set_bit ?(zero=false) bf pos = if zero then Ints_t.logand bf @@ make_bitzero_msk pos diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index 992480a6be..6fdd1c0dc3 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -475,11 +475,15 @@ module I = IntDomain.SOverflowUnlifter (I) let test_shift_left _ = assert_shift_left ik [2] [1] [4]; - assert_shift_left ik [-2] [1] [-4] + assert_shift_left ik [-2] [1] [-4]; + assert_shift_left ik [1; 8; 16] [1; 2] [2; 4; 16; 32; 64]; + assert_shift_left ik [1; 16] [28; 31; 32; 33] [0; 1 lsr 28; 1 lsr 32; 1 lsr 32] let test_shift_right _ = assert_shift_right ik [4] [1] [2]; - assert_shift_right ik [-4] [1] [-2] + assert_shift_right ik [-4] [1] [-2]; + assert_shift_right ik [1; 8; 16] [1; 2] [0; 2; 4; 8]; + assert_shift_right ik [1; 16; Int.max_int] [16; 32; 64; 128] [0; 16; Sys.word_size] (* TODO *) (* Arith *) From 65621615440cbcb147fb9ec979dff5249413626a Mon Sep 17 00:00:00 2001 From: ManuelLerchner Date: Tue, 19 Nov 2024 23:27:28 +0100 Subject: [PATCH 07/25] clean up --- src/cdomain/value/cdomains/intDomain.ml | 158 ++++++++++++------------ src/framework/control.ml | 2 +- tests/unit/cdomains/intDomainTest.ml | 14 +-- 3 files changed, 87 insertions(+), 87 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index a97c5f055b..c1efa08802 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1199,7 +1199,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let zero_mask = Ints_t.zero let one_mask = Ints_t.lognot zero_mask - + let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2) let meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2) @@ -1249,7 +1249,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let break_down_lsb ik (z,o) : (Ints_t.t * Ints_t.t) list option = if is_invalid (z,o) then None else let rec break_down c_lst i = if i < 0 then c_lst - else + else if get_bit z i = get_bit o i then List.fold_left2 ( fun acc (z1,o1) (z2,o2) -> (set_bit z1 i, set_bit ~zero:true o1 i) :: (set_bit ~zero:true z2 i, o2) :: acc @@ -1263,8 +1263,8 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let sufx_msk = make_lsb_bitmask lsb_bitcnt_log_ik in let msb_msk = Ints_t.logand (bits_set (z,o)) pfx_msk in (* shift a b = zero when min{b} > ceil(ilog2 a) *) if Ints_t.compare msb_msk Ints_t.zero = 0 - then break_down [(Ints_t.logand z pfx_msk, Ints_t.logand o sufx_msk)] (lsb_bitcnt_log_ik - 1) |> Option.some - else Some ([of_int @@ Ints_t.of_int (lsb_bitcnt_log_ik)]) + then break_down [(Ints_t.logand z pfx_msk, Ints_t.logand o sufx_msk)] (lsb_bitcnt_log_ik - 1) |> Option.some + else Some ([of_int @@ Ints_t.of_int (lsb_bitcnt_log_ik)]) let break_down ik bf = Option.map (fun c_bf_lst -> List.map snd c_bf_lst |> List.map Ints_t.to_int) (break_down_lsb ik bf) @@ -1281,53 +1281,53 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let shift_left ik bf n_bf = let shift_left (z,o) c = - let z_msk = Ints_t.sub (Ints_t.shift_left Ints_t.one c) Ints_t.one in - (Ints_t.logor (Ints_t.shift_left z c) z_msk, Ints_t.shift_left o c) + let z_msk = Ints_t.sub (Ints_t.shift_left Ints_t.one c) Ints_t.one in + (Ints_t.logor (Ints_t.shift_left z c) z_msk, Ints_t.shift_left o c) in if is_const n_bf then Some (shift_left bf (Ints_t.to_int @@ snd n_bf)) else Option.map (fun c_lst -> List.map (shift_left bf) c_lst |> List.fold_left join zero) (break_down ik n_bf) - - let min ik (z,o) = - let knownBitMask = Ints_t.logxor z o in - let unknownBitMask = Ints_t.lognot knownBitMask in - let impossibleBitMask = Ints_t.lognot (Ints_t.logor z o) in - let guaranteedBits = Ints_t.logand o knownBitMask in - - if impossibleBitMask <> zero_mask then - failwith "Impossible bitfield" - else - - if isSigned ik then - let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in - let worstPossibleUnknownBits = Ints_t.logand unknownBitMask signBitMask in - Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) - else - let worstPossibleUnknownBits = Ints_t.logand unknownBitMask zero_mask in - Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) - - let max ik (z,o) = - let knownBitMask = Ints_t.logxor z o in - let unknownBitMask = Ints_t.lognot knownBitMask in - let impossibleBitMask = Ints_t.lognot (Ints_t.logor z o) in - let guaranteedBits = Ints_t.logand o knownBitMask in - - if impossibleBitMask <> zero_mask then - failwith "Impossible bitfield" - else - + + let min ik (z,o) = + let knownBitMask = Ints_t.logxor z o in + let unknownBitMask = Ints_t.lognot knownBitMask in + let impossibleBitMask = Ints_t.lognot (Ints_t.logor z o) in + let guaranteedBits = Ints_t.logand o knownBitMask in + + if impossibleBitMask <> zero_mask then + failwith "Impossible bitfield" + else + + if isSigned ik then + let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in + let worstPossibleUnknownBits = Ints_t.logand unknownBitMask signBitMask in + Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) + else + let worstPossibleUnknownBits = Ints_t.logand unknownBitMask zero_mask in + Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) + + let max ik (z,o) = + let knownBitMask = Ints_t.logxor z o in + let unknownBitMask = Ints_t.lognot knownBitMask in + let impossibleBitMask = Ints_t.lognot (Ints_t.logor z o) in + let guaranteedBits = Ints_t.logand o knownBitMask in + + if impossibleBitMask <> zero_mask then + failwith "Impossible bitfield" + else + let (_,fullMask) = Size.range ik in let worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in - + if isSigned ik then Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) else Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) - - - let one = of_int Ints_t.one - let zero = of_int Ints_t.zero - let top_bool = join one zero - + + + let one = of_int Ints_t.one + let zero = of_int Ints_t.zero + let top_bool = join one zero + end module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) = struct @@ -1343,24 +1343,24 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int if BArith.is_invalid (z,o) then ((z,o), {underflow=false; overflow=false}) else - let (min_ik, max_ik) = Size.range ik in + let (min_ik, max_ik) = Size.range ik in - let (min,max) = range ik (z,o) in - let underflow = Z.compare min min_ik < 0 in - let overflow = Z.compare max max_ik > 0 in - - let new_bitfield= - (if isSigned ik then - let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit z (Size.bit ik))) in - let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit o (Size.bit ik))) in - (newz,newo) - else - let newz = Ints_t.logor z (Ints_t.lognot (Ints_t.of_bigint max_ik)) in - let newo = Ints_t.logand o (Ints_t.of_bigint max_ik) in - (newz,newo)) - in - if suppress_ovwarn then (new_bitfield, {underflow=false; overflow=false}) - else (new_bitfield, {underflow=underflow; overflow=overflow}) + let (min,max) = range ik (z,o) in + let underflow = Z.compare min min_ik < 0 in + let overflow = Z.compare max max_ik > 0 in + + let new_bitfield= + (if isSigned ik then + let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit z (Size.bit ik))) in + let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit o (Size.bit ik))) in + (newz,newo) + else + let newz = Ints_t.logor z (Ints_t.lognot (Ints_t.of_bigint max_ik)) in + let newo = Ints_t.logand o (Ints_t.of_bigint max_ik) in + (newz,newo)) + in + if suppress_ovwarn then (new_bitfield, {underflow=false; overflow=false}) + else (new_bitfield, {underflow=underflow; overflow=overflow}) let top () = (BArith.one_mask, BArith.one_mask) let bot () = (BArith.zero_mask, BArith.zero_mask) @@ -1391,8 +1391,8 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let of_int ik (x: int_t) = (norm ik @@ BArith.of_int x) let to_int (z,o) = if is_bot (z,o) then None else - if BArith.is_const (z,o) then Some o - else None + if BArith.is_const (z,o) then Some o + else None let equal_to i bf = if BArith.of_int i = bf then `Eq @@ -1435,7 +1435,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let c_logor = log2 (||) ~annihilator:true let c_logand = log2 (&&) ~annihilator:false - + let c_lognot ik i1 = log1 not ik i1 @@ -1521,10 +1521,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let signBitDefZ = Ints_t.logand (Ints_t.lognot (Ints_t.logxor o1 o2)) bitmask in for i = size downto 0 do (if Ints_t.logand !pm Ints_t.one == Ints_t.one then - accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (Ints_t.logor !qv !qm)) - else if Ints_t.logand !pv Ints_t.one == Ints_t.one then - accv := fst(add_paper !accv Ints_t.zero !qv Ints_t.zero); - accm := snd(add_paper Ints_t.zero !accm Ints_t.zero !qm)); + accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (Ints_t.logor !qv !qm)) + else if Ints_t.logand !pv Ints_t.one == Ints_t.one then + accv := fst(add_paper !accv Ints_t.zero !qv Ints_t.zero); + accm := snd(add_paper Ints_t.zero !accm Ints_t.zero !qm)); pv := Ints_t.shift_right !pv 1; pm := Ints_t.shift_right !pm 1; @@ -1545,10 +1545,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let rem ik x y = M.trace "bitfield" "rem"; if BArith.is_const x && BArith.is_const y then ( - (* x % y = x - (x / y) * y *) - let tmp = fst (div ik x y) in - let tmp = fst (mul ik tmp y) in - fst (sub ik x tmp)) + (* x % y = x - (x / y) * y *) + let tmp = fst (div ik x y) in + let tmp = fst (mul ik tmp y) in + fst (sub ik x tmp)) else top_of ik let eq ik x y = @@ -1625,10 +1625,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let is_power_of_two x = Ints_t.(logand x (sub x one) = zero) in match bf, cong with | (z,o), Some (c, m) when is_power_of_two m -> - let congruenceMask = Ints_t.lognot m in - let newz = Ints_t.logor (Ints_t.logand (Ints_t.lognot congruenceMask) z) (Ints_t.logand congruenceMask (Ints_t.lognot c)) in - let newo = Ints_t.logor (Ints_t.logand (Ints_t.lognot congruenceMask) o) (Ints_t.logand congruenceMask c) in - norm ik (newz, newo) |> fst + let congruenceMask = Ints_t.lognot m in + let newz = Ints_t.logor (Ints_t.logand (Ints_t.lognot congruenceMask) z) (Ints_t.logand congruenceMask (Ints_t.lognot c)) in + let newo = Ints_t.logor (Ints_t.logand (Ints_t.lognot congruenceMask) o) (Ints_t.logand congruenceMask c) in + norm ik (newz, newo) |> fst | _ -> norm ik bf |> fst let refine_with_interval ik bf (int: (int_t * int_t) option) : t = @@ -1641,12 +1641,12 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let refine_with_incl_list ik t (incl : (int_t list) option) : t = let joined =match incl with - | None -> top_of ik - | Some ls -> - List.fold_left (fun acc i -> BArith.join acc (BArith.of_int i)) (bot_of ik) ls + | None -> top_of ik + | Some ls -> + List.fold_left (fun acc i -> BArith.join acc (BArith.of_int i)) (bot_of ik) ls in meet ik t joined - + let arbitrary ik = let open QCheck.Iter in let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in @@ -1655,7 +1655,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int | (z, o) -> (GobQCheck.shrink int_arb z >|= fun z -> (z, o)) <+> (GobQCheck.shrink int_arb o >|= fun o -> (z, o)) in QCheck.(set_shrink shrink @@ set_print show @@ map (fun i -> of_int ik i |> fst ) int_arb) - (* QCheck.(set_shrink shrink @@ set_print show @@ map (fun (i1,i2) -> norm ik (join ik (fst (of_int ik i1)) (fst (of_int ik i2))) |> fst ) pair_arb)*) + (* QCheck.(set_shrink shrink @@ set_print show @@ map (fun (i1,i2) -> norm ik (join ik (fst (of_int ik i1)) (fst (of_int ik i2))) |> fst ) pair_arb)*) let project ik p t = t end diff --git a/src/framework/control.ml b/src/framework/control.ml index 1d0ebb869b..82c197273c 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -380,7 +380,7 @@ struct let test_domain (module D: Lattice.S): unit = let module DP = DomainProperties.All (D) in Logs.debug "domain testing...: %s" (D.name ()); - let errcode = QCheck_base_runner.run_tests DP.tests in + let errcode = QCheck_base_runner.run_tests DP.tests ~verbose:true in if (errcode <> 0) then failwith "domain tests failed" in diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index 992480a6be..5b56e433d4 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -252,7 +252,7 @@ end module BitfieldTest (I : IntDomain.SOverflow with type int_t = Z.t) = struct -module I = IntDomain.SOverflowUnlifter (I) + module I = IntDomain.SOverflowUnlifter (I) let ik = Cil.IInt @@ -407,7 +407,7 @@ module I = IntDomain.SOverflowUnlifter (I) let test_cast_to _ = let b1 = I.of_int ik (of_int 1234) in - + assert_equal (I.of_int IChar (of_int (210))) (I.cast_to IChar b1); assert_equal (I.of_int ISChar (of_int (-46))) (I.cast_to ISChar b1); @@ -449,7 +449,7 @@ module I = IntDomain.SOverflowUnlifter (I) assert_bool "13 ?= 13 or (5 | 17)" (I.equal_to (of_int 13) (I.logor ik b12 b3) = `Top); assert_bool "29 ?= 13 or (5 | 17)" (I.equal_to (of_int 29) (I.logor ik b12 b3) = `Top) - let test_lognot _ = + let test_lognot _ = let b1 = I.of_int ik (of_int 4) in let b2 = I.of_int ik (of_int 12) in @@ -528,7 +528,7 @@ module I = IntDomain.SOverflowUnlifter (I) let b6 = I.of_int ik (of_int 4) in assert_bool "4 <= (5 | 14)" (I.le ik b6 b12 = I.of_bool ik true) - + let test_ge _ = let b1 = I.of_int ik (of_int 5) in let b2 = I.of_int ik (of_int 14) in @@ -671,7 +671,7 @@ module I = IntDomain.SOverflowUnlifter (I) "test_refine_with_congruence" >:: test_refine_with_congruence; "test_refine_with_inclusion_list" >:: test_refine_with_inclusion_list; - ] + ] end @@ -752,7 +752,7 @@ struct module B = IntDomain.SOverflowUnlifter (B) let ik = Cil.IUChar - let of_list ik is = List.fold_left (fun acc x -> B.join ik acc (B.of_int ik x)) (B.bot ()) is + let of_list ik is = List.fold_left (fun acc x -> B.join ik acc (B.of_int ik x)) (B.bot ()) is let v1 = Z.of_int 0 let v2 = Z.of_int 13 @@ -769,7 +769,7 @@ struct let test () = [ "test_add" >:: test_add; - ] + ] end module TEMPDEBUG_TODO_REMOVE = TEMPDEBUG_TODO_REMOVE_TEST(IntDomain.Bitfield) From 2aa27f8e76faaa5b7bcab146dd31acfcc06e0778 Mon Sep 17 00:00:00 2001 From: ManuelLerchner Date: Wed, 20 Nov 2024 00:31:52 +0100 Subject: [PATCH 08/25] fix compile warnings --- src/cdomain/value/cdomains/intDomain.ml | 202 ++++-------------------- 1 file changed, 30 insertions(+), 172 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index c1efa08802..d7ea336042 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -17,11 +17,7 @@ exception ArithmeticOnIntegerBot of string (* Custom Tuple6 as Batteries only provides up to Tuple5 *) module Tuple6 = struct - type ('a,'b,'c,'d,'e,'f) t = 'a * 'b * 'c * 'd * 'e * 'f - type 'a enumerable = 'a * 'a * 'a * 'a * 'a * 'a - - let make a b c d e f= (a, b, c, d, e, f) let first (a,_,_,_,_, _) = a let second (_,b,_,_,_, _) = b @@ -30,23 +26,7 @@ module Tuple6 = struct let fifth (_,_,_,_,e, _) = e let sixth (_,_,_,_,_, f) = f - let map f1 f2 f3 f4 f5 f6 (a,b,c,d,e,f) = - let a = f1 a in - let b = f2 b in - let c = f3 c in - let d = f4 d in - let e = f5 e in - let f = f6 f in - (a, b, c, d, e, f) - - let mapn fn (a,b,c,d,e,f) = - let a = fn a in - let b = fn b in - let c = fn c in - let d = fn d in - let e = fn e in - let f = fn f in - (a, b, c, d, e, f) + let map1 fn (a, b, c, d, e, f) = (fn a, b, c, d, e, f) let map2 fn (a, b, c, d, e, f) = (a, fn b, c, d, e, f) @@ -56,106 +36,24 @@ module Tuple6 = struct let map6 fn (a, b, c, d, e, f) = (a, b, c, d, e, fn f) - - - let curry fn a b c d e f= fn (a,b,c,d,e,f) - let uncurry fn (a,b,c,d,e,f) = fn a b c d e f - let enum (a,b,c,d,e,f) = BatList.enum [a;b;c;d;e;f] (* Make efficient? *) - let of_enum e = match BatEnum.get e with - None -> failwith "Tuple6.of_enum: not enough elements" - | Some a -> match BatEnum.get e with - None -> failwith "Tuple6.of_enum: not enough elements" - | Some b -> match BatEnum.get e with - None -> failwith "Tuple6.of_enum: not enough elements" - | Some c -> match BatEnum.get e with - None -> failwith "Tuple6.of_enum: not enough elements" - | Some d -> match BatEnum.get e with - None -> failwith "Tuple6.of_enum: not enough elements" - | Some e -> match BatEnum.get e with - None -> failwith "Tuple6.of_enum: not enough elements" - | Some f -> (a,b,c,d,e,f) - - let print ?(first="(") ?(sep=",") ?(last=")") print_a print_b print_c print_d print_e print_f out (a,b,c,d,e,f) = - BatIO.nwrite out first; - print_a out a; - BatIO.nwrite out sep; - print_b out b; - BatIO.nwrite out sep; - print_c out c; - BatIO.nwrite out sep; - print_d out d; - BatIO.nwrite out sep; - print_e out e; - BatIO.nwrite out sep; - print_f out f - BatIO.nwrite out last - - - let printn ?(first="(") ?(sep=",") ?(last=")") printer out pair = - print ~first ~sep ~last printer printer printer printer printer out pair - - let compare ?(cmp1=Pervasives.compare) ?(cmp2=Pervasives.compare) ?(cmp3=Pervasives.compare) ?(cmp4=Pervasives.compare) ?(cmp5=Pervasives.compare) ?(cmp6=Pervasives.compare) (a1,a2,a3,a4,a5,a6) (b1,b2,b3,b4,b5,b6) = - let c1 = cmp1 a1 b1 in - if c1 <> 0 then c1 else - let c2 = cmp2 a2 b2 in - if c2 <> 0 then c2 else - let c3 = cmp3 a3 b3 in - if c3 <> 0 then c3 else - let c4 = cmp4 a4 b4 in - if c4 <> 0 then c4 else - let c5 = cmp5 a5 b5 in - if c5 <> 0 then c5 else - cmp5 a6 b6 - - open BatOrd - let eq eq1 eq2 eq3 eq4 eq5 eq6 = - fun (t1, t2, t3, t4, t5,t6) (t1', t2', t3', t4', t5',t6') -> - bin_eq eq1 t1 t1' - (bin_eq eq2 t2 t2' - (bin_eq eq3 t3 t3' - (bin_eq eq4 t4 t4' - (bin_eq eq5 t5 t5' eq6)))) t6 t6' - - let ord ord1 ord2 ord3 ord4 ord5 ord6 = - fun (t1, t2, t3, t4, t5,t6) (t1', t2', t3', t4', t5',t6') -> - bin_ord ord1 t1 t1' - (bin_ord ord2 t2 t2' - (bin_ord ord3 t3 t3' - (bin_ord ord4 t4 t4' - (bin_ord ord5 t5 t5' ord6)))) t6 t6' - - let comp comp1 comp2 comp3 comp4 comp5 comp6 = - fun (t1, t2, t3, t4, t5,t6) (t1', t2', t3', t4', t5',t6') -> - let c1 = comp1 t1 t1' in - if c1 <> 0 then c1 else - let c2 = comp2 t2 t2' in - if c2 <> 0 then c2 else - let c3 = comp3 t3 t3' in - if c3 <> 0 then c3 else - let c4 = comp4 t4 t4' in - if c4 <> 0 then c4 else - let c5 = comp5 t5 t5' in - if c5 <> 0 then c5 else - comp6 t6 t6' - - module Eq (A : Eq) (B : Eq) (C : Eq) (D : Eq) (E : Eq) (F : Eq) = struct - type t = A.t * B.t * C.t * D.t * E.t * F.t - let eq = eq A.eq B.eq C.eq D.eq E.eq F.eq - end - - module Ord (A : Ord) (B : Ord) (C : Ord) (D : Ord) (E : Ord ) (F : Ord) = struct - type t = A.t * B.t * C.t * D.t * E.t * F.t - let ord = ord A.ord B.ord C.ord D.ord E.ord F.ord - end - - module Comp (A : Comp) (B : Comp) (C : Comp) (D : Comp) (E : Comp ) (F : Comp) = struct - type t = A.t * B.t * C.t * D.t * E.t * F.t - let compare = comp A.compare B.compare C.compare D.compare E.compare F.compare - end end +(* Prevent compile warnings *) +let _ = Tuple6.first +let _ = Tuple6.second +let _ = Tuple6.third +let _ = Tuple6.fourth +let _ = Tuple6.fifth +let _ = Tuple6.sixth + +let _ = Tuple6.map1 +let _ = Tuple6.map2 +let _ = Tuple6.map3 +let _ = Tuple6.map4 +let _ = Tuple6.map5 +let _ = Tuple6.map6 (** Define records that hold mutable variables representing different Configuration values. @@ -1194,8 +1092,6 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let of_int x = (Ints_t.lognot x, x) - let one = of_int Ints_t.one - let zero = of_int Ints_t.zero let zero_mask = Ints_t.zero let one_mask = Ints_t.lognot zero_mask @@ -1203,12 +1099,14 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2) let meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2) + let one = of_int Ints_t.one + let zero = of_int Ints_t.zero + let top_bool = join one zero let bits_known (z,o) = Ints_t.logxor z o let bits_unknown bf = Ints_t.lognot @@ bits_known bf let bits_set bf = Ints_t.logand (snd bf) @@ bits_known bf - let bits_undef (z,o) = Ints_t.lognot (Ints_t.logxor z o) let is_const (z,o) = (Ints_t.logxor z o) = one_mask let is_invalid (z,o) = Ints_t.compare (Ints_t.lognot (Ints_t.logor z o)) Ints_t.zero != 0 @@ -1288,45 +1186,28 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct else Option.map (fun c_lst -> List.map (shift_left bf) c_lst |> List.fold_left join zero) (break_down ik n_bf) let min ik (z,o) = - let knownBitMask = Ints_t.logxor z o in - let unknownBitMask = Ints_t.lognot knownBitMask in - let impossibleBitMask = Ints_t.lognot (Ints_t.logor z o) in - let guaranteedBits = Ints_t.logand o knownBitMask in + let unknownBitMask = bits_unknown (z,o) in + let guaranteedBits = bits_set (z,o) in - if impossibleBitMask <> zero_mask then - failwith "Impossible bitfield" - else if isSigned ik then let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in let worstPossibleUnknownBits = Ints_t.logand unknownBitMask signBitMask in Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) else - let worstPossibleUnknownBits = Ints_t.logand unknownBitMask zero_mask in - Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) + Size.cast ik (Ints_t.to_bigint guaranteedBits ) let max ik (z,o) = - let knownBitMask = Ints_t.logxor z o in - let unknownBitMask = Ints_t.lognot knownBitMask in - let impossibleBitMask = Ints_t.lognot (Ints_t.logor z o) in - let guaranteedBits = Ints_t.logand o knownBitMask in - - if impossibleBitMask <> zero_mask then - failwith "Impossible bitfield" - else + let unknownBitMask = bits_unknown (z,o) in + let guaranteedBits = bits_set (z,o) in let (_,fullMask) = Size.range ik in let worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in - if isSigned ik then - Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) - else Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) - let one = of_int Ints_t.one - let zero = of_int Ints_t.zero - let top_bool = join one zero + end @@ -1402,9 +1283,9 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let of_interval ?(suppress_ovwarn=false) ik (x,y) = (* naive implentation -> horrible O(n) runtime *) let (min_ik, max_ik) = Size.range ik in - let current = ref (Z.of_int (Ints_t.to_int x)) in + let current = ref (Z.max (Z.of_int (Ints_t.to_int x)) min_ik) in let bf = ref (bot ()) in - while Z.leq !current (Z.of_int (Ints_t.to_int y)) do + while Z.leq !current (Z.min (Z.of_int (Ints_t.to_int y)) max_ik) do bf := BArith.join !bf (BArith.of_int (Ints_t.of_bigint !current)); current := Z.add !current Z.one done; @@ -1519,7 +1400,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let signBitUndef = Ints_t.logor signBitUndef1 signBitUndef2 in let signBitDefO = Ints_t.logand (Ints_t.logxor o1 o2) bitmask in let signBitDefZ = Ints_t.logand (Ints_t.lognot (Ints_t.logxor o1 o2)) bitmask in - for i = size downto 0 do + for _ = size downto 0 do (if Ints_t.logand !pm Ints_t.one == Ints_t.one then accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (Ints_t.logor !qv !qm)) else if Ints_t.logand !pv Ints_t.one == Ints_t.one then @@ -1538,7 +1419,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int if isSigned ik then o3 := Ints_t.logor signBitUndef (Ints_t.logor signBitDefO !o3); norm ik (!z3, !o3) - let rec div ?no_ov ik (z1, o1) (z2, o2) = + let div ?no_ov ik (z1, o1) (z2, o2) = let res = if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then (let tmp = Ints_t.div z1 z2 in (Ints_t.lognot tmp, tmp)) else top_of ik in norm ik res @@ -1600,26 +1481,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int (norm ~suppress_ovwarn ik @@ (top ())) - let refine_with_congruence ik (intv : t) ((cong) : (int_t * int_t ) option) : t = - let is_power_of_two x = Ints_t.(logand x (sub x one) = zero) in - match intv, cong with - | (z,o), Some (c, m) -> - if is_power_of_two m then - let congruenceMask = Ints_t.lognot m in - let newz = Ints_t.logor (Ints_t.logand (Ints_t.lognot congruenceMask) z) (Ints_t.logand congruenceMask (Ints_t.lognot c)) in - let newo = Ints_t.logor (Ints_t.logand (Ints_t.lognot congruenceMask) o) (Ints_t.logand congruenceMask c) in - norm ik (newz, newo) |> fst - else - top_of ik - | _ -> top_of ik - - let refine_with_interval ik t i = norm ik t |> fst - - let refine_with_excl_list ik t (excl : (int_t list * (int64 * int64)) option) : t = norm ik t |> fst - let invariant_ikind e ik = - M.trace "bitfield" "invariant_ikind"; - failwith "Not implemented" let refine_with_congruence ik bf ((cong) : (int_t * int_t ) option) : t = let is_power_of_two x = Ints_t.(logand x (sub x one) = zero) in @@ -1631,13 +1493,9 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int norm ik (newz, newo) |> fst | _ -> norm ik bf |> fst - let refine_with_interval ik bf (int: (int_t * int_t) option) : t = - M.trace "bitfield" "refine_with_interval"; - norm ik bf |> fst + let refine_with_interval ik t i = norm ik t |> fst - let refine_with_excl_list ik bf (excl : (int_t list * (int64 * int64)) option) : t = - M.trace "bitfield" "refine_with_excl_list"; - norm ik bf |> fst + let refine_with_excl_list ik t (excl : (int_t list * (int64 * int64)) option) : t = norm ik t |> fst let refine_with_incl_list ik t (incl : (int_t list) option) : t = let joined =match incl with From ad5f6f8ca89f5bdeb07a6cb61e9d2b022cfcb71a Mon Sep 17 00:00:00 2001 From: ManuelLerchner Date: Wed, 20 Nov 2024 00:33:30 +0100 Subject: [PATCH 09/25] format --- src/cdomain/value/cdomains/intDomain.ml | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index d7ea336042..4a9b803788 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1,5 +1,5 @@ -open GobConfig open GoblintCil +open GobConfig open Pretty open PrecisionUtil @@ -18,7 +18,6 @@ exception ArithmeticOnIntegerBot of string (* Custom Tuple6 as Batteries only provides up to Tuple5 *) module Tuple6 = struct - let first (a,_,_,_,_, _) = a let second (_,b,_,_,_, _) = b let third (_,_,c,_,_, _) = c @@ -26,8 +25,6 @@ module Tuple6 = struct let fifth (_,_,_,_,e, _) = e let sixth (_,_,_,_,_, f) = f - - let map1 fn (a, b, c, d, e, f) = (fn a, b, c, d, e, f) let map2 fn (a, b, c, d, e, f) = (a, fn b, c, d, e, f) let map3 fn (a, b, c, d, e, f) = (a, b, fn c, d, e, f) @@ -35,7 +32,6 @@ module Tuple6 = struct let map5 fn (a, b, c, d, e, f) = (a, b, c, d, fn e, f) let map6 fn (a, b, c, d, e, f) = (a, b, c, d, e, fn f) - let enum (a,b,c,d,e,f) = BatList.enum [a;b;c;d;e;f] (* Make efficient? *) end @@ -1186,10 +1182,9 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct else Option.map (fun c_lst -> List.map (shift_left bf) c_lst |> List.fold_left join zero) (break_down ik n_bf) let min ik (z,o) = - let unknownBitMask = bits_unknown (z,o) in + let unknownBitMask = bits_unknown (z,o) in let guaranteedBits = bits_set (z,o) in - if isSigned ik then let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in let worstPossibleUnknownBits = Ints_t.logand unknownBitMask signBitMask in @@ -1201,13 +1196,10 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let unknownBitMask = bits_unknown (z,o) in let guaranteedBits = bits_set (z,o) in - let (_,fullMask) = Size.range ik in - let worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in - - Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) - - + let (_,fullMask) = Size.range ik in + let worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in + Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) end From cfa009193ca358708ef2ac51164f855b7dd1dccb Mon Sep 17 00:00:00 2001 From: ManuelLerchner Date: Wed, 20 Nov 2024 00:36:48 +0100 Subject: [PATCH 10/25] improve arbitrary --- src/cdomain/value/cdomains/intDomain.ml | 59 ++++++++++++++----------- 1 file changed, 33 insertions(+), 26 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 4a9b803788..751171eb92 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1086,12 +1086,11 @@ end (* Bitfield arithmetic, without any overflow handling etc. *) module BitfieldArith (Ints_t : IntOps.IntOps) = struct - let of_int x = (Ints_t.lognot x, x) - - let zero_mask = Ints_t.zero let one_mask = Ints_t.lognot zero_mask + let of_int x = (Ints_t.lognot x, x) + let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2) let meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2) @@ -1210,11 +1209,27 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int module BArith = BitfieldArith (Ints_t) + let top () = (BArith.one_mask, BArith.one_mask) + let bot () = (BArith.zero_mask, BArith.zero_mask) + let top_of ik = top () + let bot_of ik = bot () + + let show t = + if t = bot () then "bot" else + if t = top () then "top" else + let (z,o) = t in + if BArith.is_const t then + Format.sprintf "{%08X, %08X} (unique: %d)" (Ints_t.to_int z) (Ints_t.to_int o) (Ints_t.to_int o) + else + Format.sprintf "{%08X, %08X}" (Ints_t.to_int z) (Ints_t.to_int o) + + include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end) + let range ik bf = (BArith.min ik bf, BArith.max ik bf) let norm ?(suppress_ovwarn=false) ik (z,o) = if BArith.is_invalid (z,o) then - ((z,o), {underflow=false; overflow=false}) + (bot (), {underflow=false; overflow=false}) else let (min_ik, max_ik) = Size.range ik in @@ -1235,21 +1250,6 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int if suppress_ovwarn then (new_bitfield, {underflow=false; overflow=false}) else (new_bitfield, {underflow=underflow; overflow=overflow}) - let top () = (BArith.one_mask, BArith.one_mask) - let bot () = (BArith.zero_mask, BArith.zero_mask) - let top_of ik = (norm ik (top ())) |> fst - let bot_of ik = bot () - - let show t = - if t = bot () then "bot" else - if t = top () then "top" else - let (z,o) = t in - if BArith.is_const t then - Format.sprintf "{%08X, %08X} (unique: %d)" (Ints_t.to_int z) (Ints_t.to_int o) (Ints_t.to_int o) - else - Format.sprintf "{%08X, %08X}" (Ints_t.to_int z) (Ints_t.to_int o) - - include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end) let join ik b1 b2 = (norm ik @@ (BArith.join b1 b2) ) |> fst @@ -1473,8 +1473,6 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int (norm ~suppress_ovwarn ik @@ (top ())) - - let refine_with_congruence ik bf ((cong) : (int_t * int_t ) option) : t = let is_power_of_two x = Ints_t.(logand x (sub x one) = zero) in match bf, cong with @@ -1500,12 +1498,21 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let arbitrary ik = let open QCheck.Iter in let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in - (*let pair_arb = QCheck.pair int_arb int_arb in*) - let shrink = function - | (z, o) -> (GobQCheck.shrink int_arb z >|= fun z -> (z, o)) <+> (GobQCheck.shrink int_arb o >|= fun o -> (z, o)) + let pair_arb = QCheck.pair int_arb int_arb in + let shrink (z, o) = + (GobQCheck.shrink pair_arb (z, o) + >|= (fun (new_z, new_o) -> + (* Randomly flip bits to be opposite *) + let random_mask = Ints_t.of_int64 (Random.int64 (Int64.of_int (Size.bits ik |> snd))) in + let unsure_bitmask= Ints_t.logand new_z new_o in + let canceled_bits=Ints_t.logand unsure_bitmask random_mask in + let flipped_z = Ints_t.logor new_z canceled_bits in + let flipped_o = Ints_t.logand new_o (Ints_t.lognot canceled_bits) in + norm ik (flipped_z, flipped_o) |> fst + )) in - QCheck.(set_shrink shrink @@ set_print show @@ map (fun i -> of_int ik i |> fst ) int_arb) - (* QCheck.(set_shrink shrink @@ set_print show @@ map (fun (i1,i2) -> norm ik (join ik (fst (of_int ik i1)) (fst (of_int ik i2))) |> fst ) pair_arb)*) + + QCheck.(set_shrink shrink @@ set_print show @@ map (fun (i1,i2) -> norm ik (i1,i2) |> fst ) pair_arb) let project ik p t = t end From 59146952bb60503bd463910e8707d64b74ba20e3 Mon Sep 17 00:00:00 2001 From: ManuelLerchner Date: Wed, 20 Nov 2024 00:45:54 +0100 Subject: [PATCH 11/25] fix bug after merge --- src/cdomain/value/cdomains/intDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 730a156257..18eebd968f 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1239,8 +1239,8 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let new_bitfield= (if isSigned ik then - let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit z (Size.bit ik))) in - let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit o (Size.bit ik))) in + let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit z (Size.bit ik - 1))) in + let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit o (Size.bit ik - 1))) in (newz,newo) else let newz = Ints_t.logor z (Ints_t.lognot (Ints_t.of_bigint max_ik)) in From 15f7abeb9e2188b501fab73c3ab3fd7022c7502b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adrian=20Krau=C3=9F?= Date: Thu, 21 Nov 2024 22:19:00 +0100 Subject: [PATCH 12/25] changed narrow and added unit tests for arith ops --- src/cdomain/value/cdomains/intDomain.ml | 2 +- tests/unit/cdomains/intDomainTest.ml | 86 +++++++++++++++++++++++++ 2 files changed, 87 insertions(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 18eebd968f..de5f437696 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1259,7 +1259,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let widen ik x y = (norm ik @@ BArith.widen x y) |> fst - let narrow ik x y = norm ik x |> fst + let narrow ik x y = meet ik x y let of_int ik (x: int_t) = (norm ik @@ BArith.of_int x) diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index 9a4392548d..795c1be9d9 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -487,6 +487,85 @@ struct (* Arith *) + let print_err_message bf1 bf2 bfr = + I.show bfr ^ " on input " ^ I.show bf1 ^ " and " ^ I.show bf2 + + let ik_arithu = Cil.IUChar + + let ik_ariths = Cil.IChar + + let of_list ik is = List.fold_left (fun acc x -> I.join ik acc (I.of_int ik x)) (I.bot ()) is + + let result_list op is1 is2 = List.concat (List.map (fun x -> List.map (op x) is2) is1) + + let generate_test ?(debug=false) opc opa ik is1 is2 = + let zs1 = List.map Z.of_int is1 in + let zs2 = List.map Z.of_int is2 in + let res = of_list ik (result_list opc zs1 zs2) in + let bs1 = of_list ik zs1 in + let bs2 = of_list ik zs2 in + let bsr = opa ik bs1 bs2 in + OUnit2.assert_equal ~cmp:I.leq ~printer:(print_err_message bs1 bs2) res bsr + + let c1 = [99] + let c2 = [186] + let c3 = [-64] + let c4 = [-104] + + let is1 = [8; 45; 89; 128] + let is2 = [5; 69; 72; 192] + let is3 = [-11; -42; -99; -120] + let is4 = [-16; -64; -87; -111] + let is5 = [-64; -14; 22; 86] + + let testsuite = [c1;c2;c3;c4;is1;is2;is3;is4] + let testsuite_unsigned = [c1;c2;is1;is2] + + let arith_testsuite ?(debug=false) opc opa ts ik = + List.map (fun x -> List.map (generate_test opc opa ik x) ts) ts + + let test_add _ = + let _ = arith_testsuite Z.add I.add testsuite ik_arithu in + let _ = arith_testsuite Z.add I.add testsuite ik_ariths in + () + + let test_sub _ = + let _ = arith_testsuite Z.sub I.sub testsuite ik_arithu in + let _ = arith_testsuite Z.sub I.sub testsuite ik_ariths in + () + + let test_mul _ = + let _ = arith_testsuite Z.mul I.mul testsuite ik_arithu in + let _ = arith_testsuite Z.mul I.mul testsuite ik_ariths in + () + + let test_div _ = + let _ = arith_testsuite Z.div I.div testsuite_unsigned ik_arithu in + let _ = arith_testsuite Z.div I.div testsuite IShort in + () + + let test_rem _ = + let _ = arith_testsuite Z.rem I.rem testsuite_unsigned ik_arithu in + let _ = arith_testsuite Z.rem I.rem testsuite IShort in + () + + let test_neg _ = + let print_neg_err_message bfi bfr = + I.show bfr ^ " on input " ^ I.show bfi + in + let generate_test_neg opc opa ik is = + let zs = List.map Z.of_int is in + let res = of_list ik (List.map opc zs) in + let bs = of_list ik zs in + OUnit2.assert_equal ~cmp:I.leq ~printer:(print_neg_err_message bs) res (opa ik bs) + in + let neg_testsuite opc opa ik = + let testsuite = [c1;c2;c3;c4;is1;is2;is3;is4] in + List.map (generate_test_neg opc opa ik) testsuite + in + let _ = neg_testsuite Z.neg I.neg ik_arithu in + let _ = neg_testsuite Z.neg I.neg ik_ariths in + () (* Comparisons *) @@ -663,6 +742,13 @@ struct "test_shift_left" >:: test_shift_left; "test_shift_right" >:: test_shift_right; + "test_add" >:: test_add; + "test_sub" >:: test_sub; + "test_mul" >:: test_mul; + "test_div" >:: test_div; + "test_rem" >:: test_rem; + + "test_eq" >:: test_eq; "test_ne" >:: test_ne; "test_le" >:: test_le; From f9f7fce57400618a0d9701e93b015abc96a2b32c Mon Sep 17 00:00:00 2001 From: ManuelLerchner Date: Sun, 24 Nov 2024 15:40:00 +0100 Subject: [PATCH 13/25] add some regression tests --- src/cdomain/value/cdomains/intDomain.ml | 24 ++++++- tests/regression/01-cpa/76-bitfield.c | 36 ----------- .../82-bitfield/00-simple-mask-bitfield.c | 29 +++++++++ .../regression/82-bitfield/01-simple-arith.c | 13 ++++ .../regression/82-bitfield/02-complex-arith.c | 62 +++++++++++++++++++ .../82-bitfield/03-simple-bitwise.c | 14 +++++ 6 files changed, 140 insertions(+), 38 deletions(-) delete mode 100644 tests/regression/01-cpa/76-bitfield.c create mode 100644 tests/regression/82-bitfield/00-simple-mask-bitfield.c create mode 100644 tests/regression/82-bitfield/01-simple-arith.c create mode 100644 tests/regression/82-bitfield/02-complex-arith.c create mode 100644 tests/regression/82-bitfield/03-simple-bitwise.c diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index de5f437696..283724e096 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1101,6 +1101,9 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let bits_known (z,o) = Ints_t.logxor z o let bits_unknown bf = Ints_t.lognot @@ bits_known bf + + let bits_impossible (z,o) = Ints_t.lognot @@ Ints_t.logor z o + let bits_set bf = Ints_t.logand (snd bf) @@ bits_known bf let is_const (z,o) = (Ints_t.logxor z o) = one_mask @@ -1214,14 +1217,31 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let top_of ik = top () let bot_of ik = bot () + let to_pretty_bits (z,o) = + let known = BArith.bits_known (z,o) in + let impossible = BArith.bits_impossible (z,o) in + + let max_bits = 16 in + + let rec to_pretty_bits' known_mask impossible_mask o_mask max_bits acc = + if max_bits < 0 || o_mask = Ints_t.zero then acc + else + let current_bit_known = Ints_t.logand known_mask Ints_t.one in + let current_bit_impossible = Ints_t.logand impossible_mask Ints_t.one in + let value = Ints_t.logand o_mask Ints_t.one in + let acc' = (if current_bit_impossible = Ints_t.one then "⊥" else if current_bit_known = Ints_t.one then string_of_int (Ints_t.to_int value) else "⊤") ^ acc in + to_pretty_bits' (Ints_t.shift_right known_mask 1) (Ints_t.shift_right impossible_mask 1) (Ints_t.shift_right o_mask 1) (max_bits - 1) acc' + in + to_pretty_bits' known impossible o max_bits "" + let show t = if t = bot () then "bot" else if t = top () then "top" else let (z,o) = t in if BArith.is_const t then - Format.sprintf "{%08X, %08X} (unique: %d)" (Ints_t.to_int z) (Ints_t.to_int o) (Ints_t.to_int o) + Format.sprintf "{%d, %d} {%s} (unique: %d)" (Ints_t.to_int z) (Ints_t.to_int o) (to_pretty_bits t) (Ints_t.to_int o) else - Format.sprintf "{%08X, %08X}" (Ints_t.to_int z) (Ints_t.to_int o) + Format.sprintf "{%d, %d} {%s}" (Ints_t.to_int z) (Ints_t.to_int o) (to_pretty_bits t) include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end) diff --git a/tests/regression/01-cpa/76-bitfield.c b/tests/regression/01-cpa/76-bitfield.c deleted file mode 100644 index 2125895d18..0000000000 --- a/tests/regression/01-cpa/76-bitfield.c +++ /dev/null @@ -1,36 +0,0 @@ -//PARAM: --enable ana.int.bitfield -#include -#include -#include - -#define ANY_ERROR 5 // 5 -int main() { - int testvar = 235; - - int state; - int r = rand() % 3; // {r 7→ [0; 2],state 7→ [MIN INT; MAX INT]} - switch (r) { - case 0: - state = 0; /* 0 */ - testvar = 1; - break; - case 1: - state = 8; /* 8 */ - testvar = 1; - break; - default: - state = 10; /* 10 */ - testvar = 1; - break; - } - - if(state & ANY_ERROR == 0) { - printf("Error\n"); - } else { - printf("No error\n"); - } - - // {r 7→ [0; 2],state 7→ [0; 10]} - assert((state & ANY_ERROR) == 0); - __goblint_check((state & ANY_ERROR) == 0); -} diff --git a/tests/regression/82-bitfield/00-simple-mask-bitfield.c b/tests/regression/82-bitfield/00-simple-mask-bitfield.c new file mode 100644 index 0000000000..f5ea8dd79f --- /dev/null +++ b/tests/regression/82-bitfield/00-simple-mask-bitfield.c @@ -0,0 +1,29 @@ +// PARAM: --enable ana.int.bitfield +#include +#include +#include + +#define ANY_ERROR 5 // 0b0101 + +int main() { + int testvar = 235; + + int state; + int r = rand() % 3; + switch (r) { + case 0: + state = 0; /* 0b000 */ + testvar = 1; + break; + case 1: + state = 8; /* 0b1000 */ + testvar = 1; + break; + default: + state = 10; /* 0b1010 */ + testvar = 1; + break; + } + + __goblint_check((state & ANY_ERROR) == 0); +} diff --git a/tests/regression/82-bitfield/01-simple-arith.c b/tests/regression/82-bitfield/01-simple-arith.c new file mode 100644 index 0000000000..4fa963eb51 --- /dev/null +++ b/tests/regression/82-bitfield/01-simple-arith.c @@ -0,0 +1,13 @@ +// PARAM: --disable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield +#include + +int main() { + int a = 19; + int b = 23; + + __goblint_check(a + b == 42); + __goblint_check(a - b == -4); + __goblint_check(a * b == 437); + __goblint_check(a / b == 0); + __goblint_check(a % b == 19); +} diff --git a/tests/regression/82-bitfield/02-complex-arith.c b/tests/regression/82-bitfield/02-complex-arith.c new file mode 100644 index 0000000000..b6de6028b7 --- /dev/null +++ b/tests/regression/82-bitfield/02-complex-arith.c @@ -0,0 +1,62 @@ +// PARAM: --disable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield +#include + +int main() { + int a; + int b = 23; + + int r = rand() % 2; + switch (r) { + case 0: + a = 19; + printf("a = 19\n"); + break; + default: + a = 17; + printf("a = 17\n"); + break; + } + + // PLUS + + int c_add = a + b; + + if (c_add == 40) { + __goblint_check(1); // reachable + } + if (c_add == 42) { + __goblint_check(1); // reachable + } + if (c_add > 42 || c_add < 40) { + __goblint_check(0); // NOWARN (unreachable) + } + + // MINUS + + int c_minus = b - a; + + if (c_minus == 6) { + __goblint_check(1); // reachable + } + if (c_minus == 4) { + __goblint_check(1); // reachable + } + if (c_minus > 6 || c_minus < 4) { + __goblint_check(0); // NOWARN (unreachable) + } + + // MULT + + int c_mult = a * b; + + if (c_mult == 391) { + __goblint_check(1); // reachable + } + if (c_mult == 437) { + __goblint_check(1); // reachable + } + + // DIV + + // Div on non-unique bitfields is not supported +} diff --git a/tests/regression/82-bitfield/03-simple-bitwise.c b/tests/regression/82-bitfield/03-simple-bitwise.c new file mode 100644 index 0000000000..8f4f809ba2 --- /dev/null +++ b/tests/regression/82-bitfield/03-simple-bitwise.c @@ -0,0 +1,14 @@ +// PARAM: --disable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield +#include + +int main() { + int a = 19; + int b = 14; + + __goblint_check((a & b) == 2); + __goblint_check((a | b) == 31); + __goblint_check((a ^ b) == 29); + __goblint_check((~a) == -20); + __goblint_check((a << 2) == 76); + __goblint_check((a >> 2) == 4); +} From 1b6459d441345aa315f0e0fcb90b60a08e49ed3d Mon Sep 17 00:00:00 2001 From: giaca Date: Mon, 25 Nov 2024 07:34:25 +0100 Subject: [PATCH 14/25] reworked bitfield shifts, infix operators and some simple tests. signedness info in type necessary for maximal and minimal func? --- src/cdomain/value/cdomains/intDomain.ml | 188 ++++++++++++------------ tests/unit/cdomains/intDomainTest.ml | 65 ++++---- 2 files changed, 134 insertions(+), 119 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index de5f437696..75f61f6253 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1086,104 +1086,104 @@ end (* Bitfield arithmetic, without any overflow handling etc. *) module BitfieldArith (Ints_t : IntOps.IntOps) = struct + let (&:) = Ints_t.logand + let (|:) = Ints_t.logor + let (^:) = Ints_t.logxor + let (!:) = Ints_t.lognot + let (<<:) = Ints_t.shift_left + let (>>:) = Ints_t.shift_right + (* Shift-in ones *) + let ( >>. ) = fun a b -> Ints_t.shift_right a b |: !:(Ints_t.sub (Ints_t.one <<: b) Ints_t.one) + let (<:) = fun a b -> Ints_t.compare a b < 0 + let (=:) = fun a b -> Ints_t.compare a b = 0 + let zero_mask = Ints_t.zero - let one_mask = Ints_t.lognot zero_mask + let one_mask = !:zero_mask - let of_int x = (Ints_t.lognot x, x) + let of_int x = (!:x, x) - let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2) - let meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2) + let join (z1,o1) (z2,o2) = (z1 |: z2, o1 |: o2) + let meet (z1,o1) (z2,o2) = (z1 &: z2, o1 &: o2) let one = of_int Ints_t.one let zero = of_int Ints_t.zero - let top_bool = join one zero - let bits_known (z,o) = Ints_t.logxor z o - let bits_unknown bf = Ints_t.lognot @@ bits_known bf - let bits_set bf = Ints_t.logand (snd bf) @@ bits_known bf + let bits_known (z,o) = z ^: o + let bits_unknown bf = !:(bits_known bf) + let bits_set bf = snd bf &: bits_known bf - let is_const (z,o) = (Ints_t.logxor z o) = one_mask - let is_invalid (z,o) = Ints_t.compare (Ints_t.lognot (Ints_t.logor z o)) Ints_t.zero != 0 + let is_const (z,o) = (z ^: o) =: one_mask + let is_invalid (z,o) = not ((!:(z |: o)) =: Ints_t.zero) - let nabla x y= if x = Ints_t.logor x y then x else one_mask + let nabla x y= if x =: (x |: y) then x else one_mask let widen (z1,o1) (z2,o2) = (nabla z1 z2, nabla o1 o2) let lognot (z,o) = (o,z) - let logxor (z1,o1) (z2,o2) = (Ints_t.logor (Ints_t.logand z1 z2) (Ints_t.logand o1 o2), - Ints_t.logor (Ints_t.logand z1 o2) (Ints_t.logand o1 z2)) + let logxor (z1,o1) (z2,o2) = ((z1 &: z2) |: (o1 &: o2), + (z1 &: o2) |: (o1 &: z2)) - let logand (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logand o1 o2) + let logand (z1,o1) (z2,o2) = (z1 |: z2, o1 &: o2) - let logor (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logor o1 o2) + let logor (z1,o1) (z2,o2) = (z1 &: z2, o1 |: o2) - let make_bitone_msk pos = Ints_t.shift_left Ints_t.one pos - let make_bitzero_msk pos = Ints_t.lognot @@ make_bitone_msk pos - let make_lsb_bitmask pos = Ints_t.sub (make_bitone_msk pos) Ints_t.one - let make_msb_bitmask pos = Ints_t.lognot @@ make_lsb_bitmask pos + let make_bitone_msk pos = Ints_t.one <<: pos + let make_bitzero_msk pos = !:(make_bitone_msk pos) + let make_lsb_bitmask pos = + let bitmsk = make_bitone_msk pos in + if bitmsk =: Ints_t.zero then Ints_t.zero + else Ints_t.sub bitmsk Ints_t.one + let make_msb_bitmask pos = !:(make_lsb_bitmask pos) - let get_bit bf pos = Ints_t.logand Ints_t.one @@ Ints_t.shift_right bf pos - let set_bit ?(zero=false) bf pos = - if zero then - Ints_t.logand bf @@ make_bitzero_msk pos + let get_bit bf pos = Ints_t.one &: (bf <<: pos) + + (* Worst Case asymptotic runtime: O(2^n). *) + let rec concretize (z,o) = + if is_const (z,o) then [o] else - Ints_t.logor bf @@ make_bitone_msk pos + let arbitrary_bit = (z ^: o) &: (z |: o) &: Ints_t.one in + let bit = o &: Ints_t.one in + let shifted_z, shifted_o = (z >>. 1, o >>: 1) in + if not (arbitrary_bit =: Ints_t.zero) + then concretize (shifted_z, shifted_o) |> List.concat_map (fun c -> [c <<: 1; (c <<: 1) |: Ints_t.one]) + else concretize (shifted_z, shifted_o) |> List.map (fun c -> c <<: 1 |: bit) + + let concretize bf = List.map Ints_t.to_int (concretize bf) - let log2_bitcnt ik = - let ilog2 n = - let rec aux n acc = - if n <= 1 then acc - else aux (n lsr 1) (acc + 1) - in aux n 0 - in ilog2 (Size.bit ik) + let get_c (_,o) = Ints_t.to_int o - let break_down_lsb ik (z,o) : (Ints_t.t * Ints_t.t) list option = if is_invalid (z,o) then None + let shift_right ik (z,o) c = + let sign_msk = make_msb_bitmask (Size.bit ik - c) in + if (isSigned ik) && (o <: Ints_t.zero) then + (z <<: c, (o <<: c) |: sign_msk) else - let rec break_down c_lst i = if i < 0 then c_lst - else - if get_bit z i = get_bit o i then - List.fold_left2 ( - fun acc (z1,o1) (z2,o2) -> (set_bit z1 i, set_bit ~zero:true o1 i) :: (set_bit ~zero:true z2 i, o2) :: acc - ) [] c_lst c_lst - |> fun c_lst -> break_down c_lst (i-1) - else - break_down c_lst (i-1) - in - let lsb_bitcnt_log_ik = log2_bitcnt ik + 1 in (* ilog2 bitcnt of ik ceiled *) - let pfx_msk = make_msb_bitmask lsb_bitcnt_log_ik in - let sufx_msk = make_lsb_bitmask lsb_bitcnt_log_ik in - let msb_msk = Ints_t.logand (bits_set (z,o)) pfx_msk in (* shift a b = zero when min{b} > ceil(ilog2 a) *) - if Ints_t.compare msb_msk Ints_t.zero = 0 - then break_down [(Ints_t.logand z pfx_msk, Ints_t.logand o sufx_msk)] (lsb_bitcnt_log_ik - 1) |> Option.some - else Some ([of_int @@ Ints_t.of_int (lsb_bitcnt_log_ik)]) - - let break_down ik bf = Option.map (fun c_bf_lst -> List.map snd c_bf_lst |> List.map Ints_t.to_int) (break_down_lsb ik bf) - - let shift_right ik bf n_bf = - let shift_right (z,o) c = - let sign_msk = Ints_t.shift_left one_mask (Size.bit ik - c) in - if (isSigned ik) && ((Ints_t.to_int o) < 0) then - (Ints_t.shift_right z c, Ints_t.logor (Ints_t.shift_right o c) sign_msk) - else - (Ints_t.logor (Ints_t.shift_right z c) sign_msk, Ints_t.shift_right o c) - in - if is_const n_bf then Some (shift_right bf (Ints_t.to_int @@ snd n_bf)) - else Option.map (fun c_lst -> List.map (shift_right bf) c_lst |> List.fold_left join zero) (break_down ik n_bf) + ((z <<: c) |: sign_msk, o <<: c) - let shift_left ik bf n_bf = - let shift_left (z,o) c = - let z_msk = Ints_t.sub (Ints_t.shift_left Ints_t.one c) Ints_t.one in - (Ints_t.logor (Ints_t.shift_left z c) z_msk, Ints_t.shift_left o c) - in - if is_const n_bf then Some (shift_left bf (Ints_t.to_int @@ snd n_bf)) - else Option.map (fun c_lst -> List.map (shift_left bf) c_lst |> List.fold_left join zero) (break_down ik n_bf) + let shift_right ik bf possible_shifts = + if is_const possible_shifts then shift_right ik bf (get_c possible_shifts) + else + let join_shrs c_lst = List.map (shift_right ik bf) c_lst |> List.fold_left join zero in + let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in + concretize (fst bf &: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) + |> join_shrs + + let shift_left _ (z,o) c = + let z_msk = make_lsb_bitmask c in + ((z <<: c) |: z_msk, o <<: c) + + let shift_left ik bf possible_shifts = + if is_const possible_shifts then shift_left ik bf (get_c possible_shifts) + else + let join_shls c_lst = List.map (shift_left ik bf) c_lst |> List.fold_left join zero in + let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in + concretize (fst bf &: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) + |> join_shls let min ik (z,o) = let unknownBitMask = bits_unknown (z,o) in let guaranteedBits = bits_set (z,o) in - if isSigned ik then let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in let worstPossibleUnknownBits = Ints_t.logand unknownBitMask signBitMask in @@ -1194,10 +1194,8 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let max ik (z,o) = let unknownBitMask = bits_unknown (z,o) in let guaranteedBits = bits_set (z,o) in - let (_,fullMask) = Size.range ik in let worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in - Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) end @@ -1226,26 +1224,28 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end) let range ik bf = (BArith.min ik bf, BArith.max ik bf) + let minimal bf = Option.some (BArith.bits_known bf) (* TODO signedness info in type? No ik here! *) + let maximal bf = BArith.(bits_known bf |: bits_unknown bf) |> Option.some (* TODO signedness info in type? No ik here! *) let norm ?(suppress_ovwarn=false) ik (z,o) = if BArith.is_invalid (z,o) then (bot (), {underflow=false; overflow=false}) else let (min_ik, max_ik) = Size.range ik in - + let wrap ik (z,o) = + if isSigned ik then + let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit z (Size.bit ik - 1))) in + let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit o (Size.bit ik - 1))) in + (newz,newo) + else + let newz = Ints_t.logor z (Ints_t.lognot (Ints_t.of_bigint max_ik)) in + let newo = Ints_t.logand o (Ints_t.of_bigint max_ik) in + (newz,newo) + in let (min,max) = range ik (z,o) in let underflow = Z.compare min min_ik < 0 in let overflow = Z.compare max max_ik > 0 in - - let new_bitfield= - (if isSigned ik then - let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit z (Size.bit ik - 1))) in - let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit o (Size.bit ik - 1))) in - (newz,newo) - else - let newz = Ints_t.logor z (Ints_t.lognot (Ints_t.of_bigint max_ik)) in - let newo = Ints_t.logand o (Ints_t.of_bigint max_ik) in - (newz,newo)) + let new_bitfield = wrap ik (z,o) in if suppress_ovwarn then (new_bitfield, {underflow=false; overflow=false}) else (new_bitfield, {underflow=underflow; overflow=overflow}) @@ -1273,12 +1273,11 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int else `Neq let of_interval ?(suppress_ovwarn=false) ik (x,y) = - (* naive implentation -> horrible O(n) runtime *) let (min_ik, max_ik) = Size.range ik in - let current = ref (Z.max (Z.of_int (Ints_t.to_int x)) min_ik) in - let bf = ref (bot ()) in - while Z.leq !current (Z.min (Z.of_int (Ints_t.to_int y)) max_ik) do - bf := BArith.join !bf (BArith.of_int (Ints_t.of_bigint !current)); + let current = ref (Z.max (Ints_t.to_bigint x) min_ik) in + let bf = ref (bot ()) in + while Z.leq !current (Z.min (Ints_t.to_bigint y) max_ik) do + bf := BArith.join !bf (BArith.of_int @@ Ints_t.of_bigint !current); current := Z.add !current Z.one done; norm ~suppress_ovwarn ik !bf @@ -1324,11 +1323,13 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let shift_right ik a b = M.trace "bitfield" "shift_right"; - norm ik @@ (BArith.shift_right ik a b |> Option.value ~default: (bot ())) + if BArith.is_invalid b || BArith.is_invalid a then (bot (), {underflow=false; overflow=false}) + else norm ik (BArith.shift_right ik a b) let shift_left ik a b = M.trace "bitfield" "shift_left"; - norm ik @@ (BArith.shift_left ik a b |> Option.value ~default: (bot ())) + if BArith.is_invalid b || BArith.is_invalid a then (bot (), {underflow=false; overflow=false}) + else norm ik (BArith.shift_left ik a b) (* Arith *) @@ -1424,7 +1425,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int fst (sub ik x tmp)) else top_of ik - let eq ik x y = + let eq ik x y = if (BArith.max ik x) <= (BArith.min ik y) && (BArith.min ik x) >= (BArith.max ik y) then of_bool ik true else if (BArith.min ik x) > (BArith.max ik y) || (BArith.max ik x) < (BArith.min ik y) then of_bool ik false else BArith.top_bool @@ -1455,7 +1456,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let starting ?(suppress_ovwarn=false) ik n = if Ints_t.compare n Ints_t.zero >= 0 then (* sign bit can only be 0, as all numbers will be positive *) - let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in + let signBitMask = BArith.make_bitone_msk (Size.bit ik - 1) in let zs = BArith.one_mask in let os = Ints_t.logand (Ints_t.lognot signBitMask) BArith.one_mask in (norm ~suppress_ovwarn ik @@ (zs,os)) @@ -1465,7 +1466,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let ending ?(suppress_ovwarn=false) ik n = if isSigned ik && Ints_t.compare n Ints_t.zero <= 0 then (* sign bit can only be 1, as all numbers will be negative *) - let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in + let signBitMask = BArith.make_bitone_msk (Size.bit ik - 1) in let zs = Ints_t.logand (Ints_t.lognot signBitMask) BArith.one_mask in let os = BArith.one_mask in (norm ~suppress_ovwarn ik @@ (zs,os)) @@ -1511,7 +1512,6 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int norm ik (flipped_z, flipped_o) |> fst )) in - QCheck.(set_shrink shrink @@ set_print show @@ map (fun (i1,i2) -> norm ik (i1,i2) |> fst ) pair_arb) let project ik p t = t diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index 795c1be9d9..7acccbccd9 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -289,10 +289,10 @@ struct let b1 = I.of_int ik (of_int 9) in let b2 = I.of_int ik (of_int 2) in let bjoin = I.join ik b1 b2 in + assert_bool "num1 leq join" (I.leq b1 bjoin); assert_bool "num2 leq join" (I.leq b2 bjoin); - OUnit.assert_equal `Top (I.equal_to (Z.of_int 9) bjoin); OUnit.assert_equal `Top (I.equal_to (Z.of_int 2) bjoin); OUnit.assert_equal `Top (I.equal_to (Z.of_int 11) bjoin) @@ -373,14 +373,20 @@ struct (* no widening needed *) assert_bool "join leq widen" (I.leq (I.join ik b1 b2) (I.widen ik b1 b2)) - let test_of_interval _ = - let intvl= (of_int 3, of_int 17) in - let b1 = I.of_interval ik intvl in - - for i = 3 to 17 do - assert_bool (string_of_int i) (I.equal_to (of_int i) b1 = `Top) + let assert_of_interval lb ub = + let intvl = (of_int lb, of_int ub) in + let bf = I.of_interval ik intvl in + let print_err_message i = "Missing value: " ^ string_of_int i ^ " in [" ^ string_of_int lb ^ ", " ^ string_of_int ub ^ "]" in + for i = lb to ub do + assert_bool (print_err_message i) (I.equal_to (of_int i) bf = `Top) done + let test_of_interval _ = + assert_of_interval 3 17; + assert_of_interval (-17) (-3); + assert_of_interval (-3) 17; + assert_of_interval (-17) 3 + let test_of_bool _ = let b1 = I.of_bool ik true in let b2 = I.of_bool ik false in @@ -460,30 +466,37 @@ struct assert_bool "-13 ?= not (4 | 12)" (I.equal_to (of_int (-13)) (I.lognot ik b12) = `Top); assert_bool "-5 ?= not (4 | 12)" (I.equal_to (of_int (-5)) (I.lognot ik b12) = `Top) - (* TODO assumes join to be correct *) + let of_list ik is = List.fold_left (fun acc x -> I.join ik acc (I.of_int ik x)) (I.bot ()) is + let assert_shift shift symb ik a b res = - let lst2bf lst = List.map (fun x -> I.of_int ik @@ of_int x) lst |> List.fold_left (I.join ik) (I.bot ()) in - let stat1 = lst2bf a in - let stat2 = lst2bf b in - let eval = (shift ik stat1 stat2) in - let eq = lst2bf res in - let out_string = I.show stat1 ^ symb ^ I.show stat2 ^ " should be : \"" ^ I.show eq ^ "\" but was \"" ^ I.show eval ^ "\"" in - OUnit2.assert_equal ~cmp:(fun x y -> Option.value ~default:false @@ I.to_bool @@ I.eq ik x y) ~msg:out_string eq eval (* TODO msg *) + let bs1 = of_list ik (List.map of_int a) in + let bs2 = of_list ik (List.map of_int b) in + let bsr = of_list ik (List.map of_int res) in + let res = (shift ik bs1 bs2) in + let test_case_str = I.show bs1 ^ symb ^ I.show bs2 in + OUnit.assert_equal ~cmp:I.leq ~printer:I.show ~msg:test_case_str bsr res (*bsr <= res!*) - let assert_shift_left ik a b res = assert_shift I.shift_left "<<" ik a b res - let assert_shift_right ik a b res = assert_shift I.shift_right ">>" ik a b res + let assert_shift_left ik a b res = assert_shift I.shift_left " << " ik a b res + let assert_shift_right ik a b res = assert_shift I.shift_right " >> " ik a b res let test_shift_left _ = assert_shift_left ik [2] [1] [4]; assert_shift_left ik [-2] [1] [-4]; - assert_shift_left ik [1; 8; 16] [1; 2] [2; 4; 16; 32; 64]; - assert_shift_left ik [1; 16] [28; 31; 32; 33] [0; 1 lsr 28; 1 lsr 32; 1 lsr 32] + assert_shift_left ik [2; 16] [1; 2] [4; 8; 32; 64]; + assert_shift_left ik [-2; 16] [1; 2] [-8; -4; 32; 64]; + assert_shift_left ik [2; -16] [1; 2] [-64; -32; 4; 8]; + assert_shift_left ik [-2; -16] [1; 2] [-64; -32; -8; -4]; + assert_shift_left ik [-3; 5; -7; 11] [2; 5] [-224; -96; -28; -12; 20; 44; 160; 352] let test_shift_right _ = assert_shift_right ik [4] [1] [2]; assert_shift_right ik [-4] [1] [-2]; - assert_shift_right ik [1; 8; 16] [1; 2] [0; 2; 4; 8]; - assert_shift_right ik [1; 16; Int.max_int] [16; 32; 64; 128] [0; 16; Sys.word_size] (* TODO *) + assert_shift_right ik [8; 64] [3; 5] [0; 1; 2; 8]; + assert_shift_right ik [-2; 16] [1; 2] [-1; 0; 4; 8]; + assert_shift_right ik [2; -16] [1; 2] [-8; -4; 0; 1]; + assert_shift_right ik [-2; -16] [1; 2] [-8; -4; -1; 0]; + assert_shift_right ik [-53; 17; -24; 48] [3; 7] [-6; -3; 0; 2; 9] + (* Arith *) @@ -494,8 +507,6 @@ struct let ik_ariths = Cil.IChar - let of_list ik is = List.fold_left (fun acc x -> I.join ik acc (I.of_int ik x)) (I.bot ()) is - let result_list op is1 is2 = List.concat (List.map (fun x -> List.map (op x) is2) is1) let generate_test ?(debug=false) opc opa ik is1 is2 = @@ -522,7 +533,7 @@ struct let testsuite_unsigned = [c1;c2;is1;is2] let arith_testsuite ?(debug=false) opc opa ts ik = - List.map (fun x -> List.map (generate_test opc opa ik x) ts) ts + List.iter (fun x -> List.iter (generate_test opc opa ik x) ts) ts let test_add _ = let _ = arith_testsuite Z.add I.add testsuite ik_arithu in @@ -649,7 +660,6 @@ struct let b1 = I.of_int ik (of_int 5) in let b2 = I.of_int ik (of_int 14) in - assert_bool "5 > 5" (I.gt ik b1 b1 = I.of_bool ik false); assert_bool "5 > 14" (I.gt ik b1 b2 = I.of_bool ik false); assert_bool "14 > 5" (I.gt ik b2 b1 = I.of_bool ik true); @@ -713,6 +723,10 @@ struct List.iter (fun i -> assert_bool (Z.to_string i) (I.equal_to i bf_refined = `Top)) list + (* + let test_refine_with_exclusion_list _ = failwith "TODO" + *) + let test () =[ "test_of_int_to_int" >:: test_of_int_to_int; "test_to_int_of_int" >:: test_to_int_of_int; @@ -761,6 +775,7 @@ struct "test_refine_with_congruence" >:: test_refine_with_congruence; "test_refine_with_inclusion_list" >:: test_refine_with_inclusion_list; + (*"test_refine_with_exclusion_list" >:: test_refine_with_exclusion_list;*) ] end From 31def4bf221b4ef454c5e1279c3f5d95ca31c7bb Mon Sep 17 00:00:00 2001 From: giaca Date: Mon, 25 Nov 2024 07:59:46 +0100 Subject: [PATCH 15/25] shift a b = zero when min{b} >= ceil(log (Size.bit ik)) --- src/cdomain/value/cdomains/intDomain.ml | 41 +++++++++++++------------ 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 75f61f6253..fe1534077b 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1139,6 +1139,24 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let get_bit bf pos = Ints_t.one &: (bf <<: pos) + let min ik (z,o) = + let unknownBitMask = bits_unknown (z,o) in + let guaranteedBits = bits_set (z,o) in + if isSigned ik then + let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in + let worstPossibleUnknownBits = Ints_t.logand unknownBitMask signBitMask in + Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) + else + Size.cast ik (Ints_t.to_bigint guaranteedBits ) + + let max ik (z,o) = + let unknownBitMask = bits_unknown (z,o) in + let guaranteedBits = bits_set (z,o) in + let (_,fullMask) = Size.range ik in + let worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in + Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) + + (* Worst Case asymptotic runtime: O(2^n). *) let rec concretize (z,o) = if is_const (z,o) then [o] @@ -1166,7 +1184,8 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct else let join_shrs c_lst = List.map (shift_right ik bf) c_lst |> List.fold_left join zero in let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in - concretize (fst bf &: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) + if Z.to_int (min ik bf) >= max_bit then zero + else concretize (make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) |> join_shrs let shift_left _ (z,o) c = @@ -1178,26 +1197,10 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct else let join_shls c_lst = List.map (shift_left ik bf) c_lst |> List.fold_left join zero in let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in - concretize (fst bf &: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) + if Z.to_int (min ik bf) >= max_bit then zero + else concretize (make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) |> join_shls - let min ik (z,o) = - let unknownBitMask = bits_unknown (z,o) in - let guaranteedBits = bits_set (z,o) in - if isSigned ik then - let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in - let worstPossibleUnknownBits = Ints_t.logand unknownBitMask signBitMask in - Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) - else - Size.cast ik (Ints_t.to_bigint guaranteedBits ) - - let max ik (z,o) = - let unknownBitMask = bits_unknown (z,o) in - let guaranteedBits = bits_set (z,o) in - let (_,fullMask) = Size.range ik in - let worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in - Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) - end module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) = struct From 2ba8f386ac03c228f5042c0243a8fcc025003b01 Mon Sep 17 00:00:00 2001 From: giaca Date: Mon, 25 Nov 2024 08:14:50 +0100 Subject: [PATCH 16/25] negative shifts are undefined --- src/cdomain/value/cdomains/intDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index fe1534077b..f9ed4d0dbc 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1326,12 +1326,12 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let shift_right ik a b = M.trace "bitfield" "shift_right"; - if BArith.is_invalid b || BArith.is_invalid a then (bot (), {underflow=false; overflow=false}) + if BArith.is_invalid b || BArith.is_invalid a || BArith.(min ik b < Z.zero) then (bot (), {underflow=false; overflow=false}) else norm ik (BArith.shift_right ik a b) let shift_left ik a b = M.trace "bitfield" "shift_left"; - if BArith.is_invalid b || BArith.is_invalid a then (bot (), {underflow=false; overflow=false}) + if BArith.is_invalid b || BArith.is_invalid a || BArith.(min ik b < Z.zero) then (bot (), {underflow=false; overflow=false}) else norm ik (BArith.shift_left ik a b) (* Arith *) From b6762af8d59976d9d82cb9bcba2acf5489e77068 Mon Sep 17 00:00:00 2001 From: giaca Date: Mon, 25 Nov 2024 08:18:31 +0100 Subject: [PATCH 17/25] bugfix: zero bits for lsb bitmask --- src/cdomain/value/cdomains/intDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index f9ed4d0dbc..61b80dd843 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1185,7 +1185,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let join_shrs c_lst = List.map (shift_right ik bf) c_lst |> List.fold_left join zero in let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in if Z.to_int (min ik bf) >= max_bit then zero - else concretize (make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) + else concretize (make_msb_bitmask max_bit |: fst bf, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) |> join_shrs let shift_left _ (z,o) c = @@ -1198,7 +1198,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let join_shls c_lst = List.map (shift_left ik bf) c_lst |> List.fold_left join zero in let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in if Z.to_int (min ik bf) >= max_bit then zero - else concretize (make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) + else concretize (make_msb_bitmask max_bit |: fst bf, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) |> join_shls end From b6ee7fa64fa49834d4bb83e79a2c266ceacc17c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adrian=20Krau=C3=9F?= Date: Mon, 25 Nov 2024 21:34:28 +0100 Subject: [PATCH 18/25] refactored min and max --- src/cdomain/value/cdomains/intDomain.ml | 36 +++++++++++-------------- tests/unit/cdomains/intDomainTest.ml | 8 +++--- 2 files changed, 20 insertions(+), 24 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index de5f437696..a9a96e3a35 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1181,24 +1181,18 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct else Option.map (fun c_lst -> List.map (shift_left bf) c_lst |> List.fold_left join zero) (break_down ik n_bf) let min ik (z,o) = - let unknownBitMask = bits_unknown (z,o) in - let guaranteedBits = bits_set (z,o) in - - if isSigned ik then - let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in - let worstPossibleUnknownBits = Ints_t.logand unknownBitMask signBitMask in - Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) - else - Size.cast ik (Ints_t.to_bigint guaranteedBits ) + let signBit = Ints_t.shift_left Ints_t.one ((Size.bit ik) - 1) in + let signMask = Ints_t.lognot (Ints_t.of_bigint (snd (Size.range ik))) in + let isNegative = Ints_t.logand signBit o <> Ints_t.zero in + if isSigned ik && isNegative then Ints_t.to_bigint(Ints_t.logor signMask (Ints_t.lognot z)) + else Ints_t.to_bigint(Ints_t.lognot z) let max ik (z,o) = - let unknownBitMask = bits_unknown (z,o) in - let guaranteedBits = bits_set (z,o) in - - let (_,fullMask) = Size.range ik in - let worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in - - Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits)) + let signBit = Ints_t.shift_left Ints_t.one ((Size.bit ik) - 1) in + let signMask = Ints_t.of_bigint (snd (Size.range ik)) in + let isPositive = Ints_t.logand signBit z <> Ints_t.zero in + if isSigned ik && isPositive then Ints_t.to_bigint(Ints_t.logand signMask o) + else Ints_t.to_bigint o end @@ -1336,6 +1330,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int add, sub and mul based on the paper "Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers" of Vishwanathan et al. + https://doi.org/10.1109/CGO53902.2022.9741267 *) let add_paper pv pm qv qm = @@ -1394,10 +1389,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let signBitDefZ = Ints_t.logand (Ints_t.lognot (Ints_t.logxor o1 o2)) bitmask in for _ = size downto 0 do (if Ints_t.logand !pm Ints_t.one == Ints_t.one then - accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (Ints_t.logor !qv !qm)) - else if Ints_t.logand !pv Ints_t.one == Ints_t.one then - accv := fst(add_paper !accv Ints_t.zero !qv Ints_t.zero); - accm := snd(add_paper Ints_t.zero !accm Ints_t.zero !qm)); + accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (Ints_t.logor !qv !qm)) + else if Ints_t.logand !pv Ints_t.one == Ints_t.one then + accv := fst(add_paper !accv Ints_t.zero !qv Ints_t.zero); + accm := snd(add_paper Ints_t.zero !accm Ints_t.zero !qm)); pv := Ints_t.shift_right !pv 1; pm := Ints_t.shift_right !pm 1; @@ -1445,7 +1440,6 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int else if (BArith.min ik x) >= (BArith.max ik y) then of_bool ik false else BArith.top_bool - let gt ik x y = lt ik y x let invariant_ikind e ik (z,o) = diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index 795c1be9d9..1f5602e897 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -845,10 +845,10 @@ struct let of_list ik is = List.fold_left (fun acc x -> B.join ik acc (B.of_int ik x)) (B.bot ()) is let v1 = Z.of_int 0 - let v2 = Z.of_int 13 + let v2 = Z.of_int 2 let vr = Z.mul v1 v2 - let is = [0;1;2;3;4;5;6;7] + let is = [-3;3] let res = [0;13;26;39;52;65;78;91] let b1 = of_list ik (List.map Z.of_int is) @@ -857,8 +857,10 @@ struct let test_add _ = assert_equal ~cmp:B.leq ~printer:B.show br (B.mul ik b2 b1) + let test_lt _ = assert_equal ~cmp:B.leq ~printer:B.show (B.join ik (B.of_int ik Z.zero) (B.of_int ik Z.one)) (B.lt ik b1 b2) + let test () = [ - "test_add" >:: test_add; + "test_lt" >:: test_lt; ] end From e2366ffa58c4a4059058389effcf8a9ccf78ba40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adrian=20Krau=C3=9F?= Date: Tue, 26 Nov 2024 11:54:49 +0100 Subject: [PATCH 19/25] added infix to all functions --- src/cdomain/value/cdomains/intDomain.ml | 150 +++++++++++++----------- 1 file changed, 83 insertions(+), 67 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 5baf8c92b3..cc4e4c4310 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1138,17 +1138,17 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let get_bit bf pos = Ints_t.one &: (bf >>: pos) let min ik (z,o) = - let signBit = Ints_t.shift_left Ints_t.one ((Size.bit ik) - 1) in - let signMask = Ints_t.lognot (Ints_t.of_bigint (snd (Size.range ik))) in - let isNegative = Ints_t.logand signBit o <> Ints_t.zero in - if isSigned ik && isNegative then Ints_t.to_bigint(Ints_t.logor signMask (Ints_t.lognot z)) - else Ints_t.to_bigint(Ints_t.lognot z) + let signBit = Ints_t.one <<: ((Size.bit ik) - 1) in + let signMask = !: (Ints_t.of_bigint (snd (Size.range ik))) in + let isNegative = signBit &: o <> Ints_t.zero in + if isSigned ik && isNegative then Ints_t.to_bigint(signMask |: (!: z)) + else Ints_t.to_bigint(!: z) let max ik (z,o) = - let signBit = Ints_t.shift_left Ints_t.one ((Size.bit ik) - 1) in + let signBit = Ints_t.one <<: ((Size.bit ik) - 1) in let signMask = Ints_t.of_bigint (snd (Size.range ik)) in - let isPositive = Ints_t.logand signBit z <> Ints_t.zero in - if isSigned ik && isPositive then Ints_t.to_bigint(Ints_t.logand signMask o) + let isPositive = signBit &: z <> Ints_t.zero in + if isSigned ik && isPositive then Ints_t.to_bigint(signMask &: o) else Ints_t.to_bigint o (* Worst Case asymptotic runtime: O(2^n). *) @@ -1202,6 +1202,22 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int module BArith = BitfieldArith (Ints_t) + let (+:) = Ints_t.add + let (-:) = Ints_t.sub + let ( *: ) = Ints_t.mul + let (/:) = Ints_t.div + let (%:) = Ints_t.rem + let (&:) = Ints_t.logand + let (|:) = Ints_t.logor + let (^:) = Ints_t.logxor + let (!:) = Ints_t.lognot + let (<<:) = Ints_t.shift_left + let (>>:) = Ints_t.shift_right + (* Shift-in ones *) + let ( >>. ) = fun a b -> Ints_t.shift_right a b |: !:(Ints_t.sub (Ints_t.one <<: b) Ints_t.one) + let (<:) = fun a b -> Ints_t.compare a b < 0 + let (=:) = fun a b -> Ints_t.compare a b = 0 + let top () = (BArith.one_mask, BArith.one_mask) let bot () = (BArith.zero_mask, BArith.zero_mask) let top_of ik = top () @@ -1229,12 +1245,12 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let (min_ik, max_ik) = Size.range ik in let wrap ik (z,o) = if isSigned ik then - let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit z (Size.bit ik - 1))) in - let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit o (Size.bit ik - 1))) in + let newz = (z &: (Ints_t.of_bigint max_ik)) |: ((Ints_t.of_bigint min_ik) *: (BArith.get_bit z (Size.bit ik - 1))) in + let newo = (o &: (Ints_t.of_bigint max_ik)) |: ((Ints_t.of_bigint min_ik) *: (BArith.get_bit o (Size.bit ik - 1))) in (newz,newo) else - let newz = Ints_t.logor z (Ints_t.lognot (Ints_t.of_bigint max_ik)) in - let newo = Ints_t.logand o (Ints_t.of_bigint max_ik) in + let newz = z |: !:(Ints_t.of_bigint max_ik) in + let newo = o &: (Ints_t.of_bigint max_ik) in (newz,newo) in let (min,max) = range ik (z,o) in @@ -1336,39 +1352,39 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int *) let add_paper pv pm qv qm = - let sv = Ints_t.add pv qv in - let sm = Ints_t.add pm qm in - let sigma = Ints_t.add sv sm in - let chi = Ints_t.logxor sigma sv in - let mu = Ints_t.logor (Ints_t.logor pm qm) chi in - let rv = Ints_t.logand sv (Ints_t.lognot mu) in + let sv = pv +: qv in + let sm = pm +: qm in + let sigma = sv +: sm in + let chi = sigma ^: sv in + let mu = pm |: qm |: chi in + let rv = sv &: !:mu in let rm = mu in (rv, rm) let add ?no_ov ik (z1, o1) (z2, o2) = - let pv = Ints_t.logand o1 (Ints_t.lognot z1) in - let pm = Ints_t.logand o1 z1 in - let qv = Ints_t.logand o2 (Ints_t.lognot z2) in - let qm = Ints_t.logand o2 z2 in + let pv = o1 &: !:z1 in + let pm = o1 &: z1 in + let qv = o2 &: !:z2 in + let qm = o2 &: z2 in let (rv, rm) = add_paper pv pm qv qm in - let o3 = Ints_t.logor rv rm in - let z3 = Ints_t.logor (Ints_t.lognot rv) rm in + let o3 = rv |: rm in + let z3 = !:rv |: rm in norm ik (z3, o3) let sub ?no_ov ik (z1, o1) (z2, o2) = - let pv = Ints_t.logand o1 (Ints_t.lognot z1) in - let pm = Ints_t.logand o1 z1 in - let qv = Ints_t.logand o2 (Ints_t.lognot z2) in - let qm = Ints_t.logand o2 z2 in - let dv = Ints_t.sub pv qv in - let alpha = Ints_t.add dv pm in - let beta = Ints_t.sub dv qm in - let chi = Ints_t.logxor alpha beta in - let mu = Ints_t.logor (Ints_t.logor pm qm) chi in - let rv = Ints_t.logand dv (Ints_t.lognot mu) in + let pv = o1 &: !:z1 in + let pm = o1 &: z1 in + let qv = o2 &: !:z2 in + let qm = o2 &: z2 in + let dv = pv -: qv in + let alpha = dv +: pm in + let beta = dv -: qm in + let chi = alpha ^: beta in + let mu = pm |: qm |: chi in + let rv = dv &: !:mu in let rm = mu in - let o3 = Ints_t.logor rv rm in - let z3 = Ints_t.logor (Ints_t.lognot rv) rm in + let o3 = rv |: rm in + let z3 = !:rv |: rm in norm ik (z3, o3) let neg ?no_ov ik x = @@ -1376,40 +1392,40 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int sub ?no_ov ik BArith.zero x let mul ?no_ov ik (z1, o1) (z2, o2) = - let pm = ref (Ints_t.logand z1 o1) in - let pv = ref (Ints_t.logand o1 (Ints_t.lognot z1)) in - let qm = ref (Ints_t.logand z2 o2) in - let qv = ref (Ints_t.logand o2 (Ints_t.lognot z2)) in + let pm = ref (z1 &: o1) in + let pv = ref (o1 &: !:z1) in + let qm = ref (z2 &: o2) in + let qv = ref (o2 &: !:z2) in let accv = ref BArith.zero_mask in let accm = ref BArith.zero_mask in let size = if isSigned ik then Size.bit ik - 1 else Size.bit ik in let bitmask = Ints_t.of_bigint (fst (Size.range ik)) in - let signBitUndef1 = Ints_t.logand (Ints_t.logand z1 o1) bitmask in - let signBitUndef2 = Ints_t.logand (Ints_t.logand z2 o2) bitmask in - let signBitUndef = Ints_t.logor signBitUndef1 signBitUndef2 in - let signBitDefO = Ints_t.logand (Ints_t.logxor o1 o2) bitmask in - let signBitDefZ = Ints_t.logand (Ints_t.lognot (Ints_t.logxor o1 o2)) bitmask in + let signBitUndef1 = z1 &: o1 &: bitmask in + let signBitUndef2 = z2 &: o2 &: bitmask in + let signBitUndef = signBitUndef1 |: signBitUndef2 in + let signBitDefO = (o1 ^: o2) &: bitmask in + let signBitDefZ = !:(o1 ^: o2) &: bitmask in for _ = size downto 0 do - (if Ints_t.logand !pm Ints_t.one == Ints_t.one then - accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (Ints_t.logor !qv !qm)) - else if Ints_t.logand !pv Ints_t.one == Ints_t.one then + (if !pm &: Ints_t.one == Ints_t.one then + accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (!qv |: !qm)) + else if !pv &: Ints_t.one == Ints_t.one then accv := fst(add_paper !accv Ints_t.zero !qv Ints_t.zero); accm := snd(add_paper Ints_t.zero !accm Ints_t.zero !qm)); - pv := Ints_t.shift_right !pv 1; - pm := Ints_t.shift_right !pm 1; - qv := Ints_t.shift_left !qv 1; - qm := Ints_t.shift_left !qm 1; + pv := !pv >>: 1; + pm := !pm >>: 1; + qv := !qv <<: 1; + qm := !qm <<: 1; done; let (rv, rm) = add_paper !accv Ints_t.zero Ints_t.zero !accm in - let o3 = ref(Ints_t.logor rv rm) in - let z3 = ref(Ints_t.logor (Ints_t.lognot rv) rm) in - if isSigned ik then z3 := Ints_t.logor signBitUndef (Ints_t.logor signBitDefZ !z3); - if isSigned ik then o3 := Ints_t.logor signBitUndef (Ints_t.logor signBitDefO !o3); + let o3 = ref(rv |: rm) in + let z3 = ref(!:rv |: rm) in + if isSigned ik then z3 := signBitUndef |: signBitDefZ |: !z3; + if isSigned ik then o3 := signBitUndef |: signBitDefO |: !o3; norm ik (!z3, !o3) let div ?no_ov ik (z1, o1) (z2, o2) = - let res = if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then (let tmp = Ints_t.div z1 z2 in (Ints_t.lognot tmp, tmp)) else top_of ik in + let res = if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then (let tmp = z1 /: z2 in (!:tmp, tmp)) else top_of ik in norm ik res let rem ik x y = @@ -1453,7 +1469,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int (* sign bit can only be 0, as all numbers will be positive *) let signBitMask = BArith.make_bitone_msk (Size.bit ik - 1) in let zs = BArith.one_mask in - let os = Ints_t.logand (Ints_t.lognot signBitMask) BArith.one_mask in + let os = !:signBitMask &: BArith.one_mask in (norm ~suppress_ovwarn ik @@ (zs,os)) else (norm ~suppress_ovwarn ik @@ (top ())) @@ -1462,7 +1478,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int if isSigned ik && Ints_t.compare n Ints_t.zero <= 0 then (* sign bit can only be 1, as all numbers will be negative *) let signBitMask = BArith.make_bitone_msk (Size.bit ik - 1) in - let zs = Ints_t.logand (Ints_t.lognot signBitMask) BArith.one_mask in + let zs = !:signBitMask &: BArith.one_mask in let os = BArith.one_mask in (norm ~suppress_ovwarn ik @@ (zs,os)) else @@ -1470,12 +1486,12 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let refine_with_congruence ik bf ((cong) : (int_t * int_t ) option) : t = - let is_power_of_two x = Ints_t.(logand x (sub x one) = zero) in + let is_power_of_two x = (x &: (x -: Ints_t.one) = Ints_t.zero) in match bf, cong with | (z,o), Some (c, m) when is_power_of_two m -> - let congruenceMask = Ints_t.lognot m in - let newz = Ints_t.logor (Ints_t.logand (Ints_t.lognot congruenceMask) z) (Ints_t.logand congruenceMask (Ints_t.lognot c)) in - let newo = Ints_t.logor (Ints_t.logand (Ints_t.lognot congruenceMask) o) (Ints_t.logand congruenceMask c) in + let congruenceMask = !:m in + let newz = (!:congruenceMask &: z) |: (congruenceMask &: !:c) in + let newo = (!:congruenceMask &: o) |: (congruenceMask &: c) in norm ik (newz, newo) |> fst | _ -> norm ik bf |> fst @@ -1500,10 +1516,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int >|= (fun (new_z, new_o) -> (* Randomly flip bits to be opposite *) let random_mask = Ints_t.of_int64 (Random.int64 (Int64.of_int (Size.bits ik |> snd))) in - let unsure_bitmask= Ints_t.logand new_z new_o in - let canceled_bits=Ints_t.logand unsure_bitmask random_mask in - let flipped_z = Ints_t.logor new_z canceled_bits in - let flipped_o = Ints_t.logand new_o (Ints_t.lognot canceled_bits) in + let unsure_bitmask= new_z &: new_o in + let canceled_bits= unsure_bitmask &: random_mask in + let flipped_z = new_z |: canceled_bits in + let flipped_o = new_o &: !:canceled_bits in norm ik (flipped_z, flipped_o) |> fst )) in From 29bcca16c833515f1b70e6f30c7821541ba0a3a0 Mon Sep 17 00:00:00 2001 From: giaca Date: Tue, 26 Nov 2024 13:01:32 +0100 Subject: [PATCH 20/25] bugfix: shift_right did not shift right --- src/cdomain/value/cdomains/intDomain.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index cc4e4c4310..08d0c75bf4 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1092,7 +1092,6 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let (!:) = Ints_t.lognot let (<<:) = Ints_t.shift_left let (>>:) = Ints_t.shift_right - (* Shift-in ones *) let ( >>. ) = fun a b -> Ints_t.shift_right a b |: !:(Ints_t.sub (Ints_t.one <<: b) Ints_t.one) let (<:) = fun a b -> Ints_t.compare a b < 0 let (=:) = fun a b -> Ints_t.compare a b = 0 @@ -1111,6 +1110,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let bits_known (z,o) = z ^: o let bits_unknown bf = !:(bits_known bf) + let bits_set bf = (snd bf) &: (bits_known bf) let is_const (z,o) = (z ^: o) =: one_mask let is_invalid (z,o) = not ((!:(z |: o)) =: Ints_t.zero) @@ -1169,9 +1169,9 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let shift_right ik (z,o) c = let sign_msk = make_msb_bitmask (Size.bit ik - c) in if (isSigned ik) && (o <: Ints_t.zero) then - (z <<: c, (o <<: c) |: sign_msk) + (z >>: c, (o >>: c) |: sign_msk) else - ((z <<: c) |: sign_msk, o <<: c) + ((z >>: c) |: sign_msk, o >>: c) let shift_right ik bf possible_shifts = if is_const possible_shifts then shift_right ik bf (get_c possible_shifts) From ed1999a14abd21b50fc5b8d597f7cc00d18b5b91 Mon Sep 17 00:00:00 2001 From: giaca Date: Tue, 26 Nov 2024 22:07:58 +0100 Subject: [PATCH 21/25] small QoL improvements and bug fixes --- src/cdomain/value/cdomains/intDomain.ml | 37 +++++++++++++++---------- tests/unit/cdomains/intDomainTest.ml | 22 +++++---------- 2 files changed, 29 insertions(+), 30 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 1535eee09a..8723dc25dd 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1090,15 +1090,17 @@ module BitfieldInfixOps (Ints_t : IntOps.IntOps) = struct let (!:) = Ints_t.lognot let (<<:) = Ints_t.shift_left let (>>:) = Ints_t.shift_right - let ( >>. ) = fun a b -> Ints_t.shift_right a b |: !:(Ints_t.sub (Ints_t.one <<: b) Ints_t.one) let (<:) = fun a b -> Ints_t.compare a b < 0 let (=:) = fun a b -> Ints_t.compare a b = 0 + let (>:) = fun a b -> Ints_t.compare a b > 0 let (+:) = Ints_t.add let (-:) = Ints_t.sub let ( *: ) = Ints_t.mul let (/:) = Ints_t.div let (%:) = Ints_t.rem + + let (>>.) = fun a b -> a >>: b |: !:((Ints_t.one <<: b) -: Ints_t.one) end (* Bitfield arithmetic, without any overflow handling etc. *) @@ -1119,7 +1121,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let top_bool = join one zero let bits_known (z,o) = z ^: o - let bits_unknown bf = !:(bits_known bf) + let bits_unknown (z,o) = z &: o let bits_set bf = (snd bf) &: (bits_known bf) let bits_invalid (z,o) = !:(z |: o) @@ -1166,16 +1168,16 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let rec concretize (z,o) = if is_const (z,o) then [o] else - let arbitrary_bit = (z ^: o) &: (z |: o) &: Ints_t.one in + let is_bit_unknown = not ((bits_unknown (z,o) &: Ints_t.one) =: Ints_t.zero) in let bit = o &: Ints_t.one in let shifted_z, shifted_o = (z >>. 1, o >>: 1) in - if not (arbitrary_bit =: Ints_t.zero) + if is_bit_unknown then concretize (shifted_z, shifted_o) |> List.concat_map (fun c -> [c <<: 1; (c <<: 1) |: Ints_t.one]) else concretize (shifted_z, shifted_o) |> List.map (fun c -> c <<: 1 |: bit) let concretize bf = List.map Ints_t.to_int (concretize bf) - let get_c (_,o) = Ints_t.to_int o + let get_o (_,o) = Ints_t.to_int o let shift_right ik (z,o) c = let sign_msk = make_msb_bitmask (Size.bit ik - c) in @@ -1185,11 +1187,12 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct ((z >>: c) |: sign_msk, o >>: c) let shift_right ik bf possible_shifts = - if is_const possible_shifts then shift_right ik bf (get_c possible_shifts) + if is_const possible_shifts then shift_right ik bf (get_o possible_shifts) else let join_shrs c_lst = List.map (shift_right ik bf) c_lst |> List.fold_left join zero in let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in - concretize (fst bf &: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) + if Z.to_int (min ik bf) >= max_bit then zero + else concretize (fst bf &: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) |> join_shrs let shift_left _ (z,o) c = @@ -1197,11 +1200,12 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct ((z <<: c) |: z_msk, o <<: c) let shift_left ik bf possible_shifts = - if is_const possible_shifts then shift_left ik bf (get_c possible_shifts) + if is_const possible_shifts then shift_left ik bf (get_o possible_shifts) else let join_shls c_lst = List.map (shift_left ik bf) c_lst |> List.fold_left join zero in let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in - concretize (fst bf &: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) + if Z.to_int (min ik bf) >= max_bit then zero + else concretize (fst bf &: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) |> join_shls end @@ -1224,9 +1228,12 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let to_pretty_bits (z,o) = let known_bits = BArith.bits_known (z,o) in let invalid_bits = BArith.bits_invalid (z,o) in - let num_bits_to_print = 8 in + let num_bits_to_print = Sys.word_size in let rec to_pretty_bits' known_mask impossible_mask o_mask max_bits acc = - if o_mask = Ints_t.zero then "0" + if max_bits < 0 then + if o_mask = Ints_t.zero && String.empty = acc + then "0" else acc + else if o_mask = Ints_t.zero then acc else let current_bit_known = known_mask &: Ints_t.one in let current_bit_impossible = impossible_mask &: Ints_t.one in @@ -1236,7 +1243,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int then "⊥" else if current_bit_known = Ints_t.one || current_bit_known = Ints_t.zero then string_of_int (Ints_t.to_int bit_value) else "⊤" in - to_pretty_bits' (known_mask <<: 1) (impossible_mask <<: 1) (o_mask <<: 1) (max_bits - 1) (next_bit_string ^ acc) + to_pretty_bits' (known_mask >>: 1) (impossible_mask >>: 1) (o_mask >>: 1) (max_bits - 1) (next_bit_string ^ acc) in to_pretty_bits' known_bits invalid_bits o num_bits_to_print "" @@ -1251,7 +1258,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int with Z.Overflow -> max_num_unknown_bits_to_concretize + 1 in if num_bits_unknown > max_num_unknown_bits_to_concretize then - Format.sprintf "(%08X, %08X)" (Ints_t.to_int z) (Ints_t.to_int o) + Format.sprintf "(%016X, %016X)" (Ints_t.to_int z) (Ints_t.to_int o) else (* TODO: Might be a source of long running tests.*) BArith.concretize (z,o) |> List.map string_of_int |> String.concat "; " @@ -1365,12 +1372,12 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let shift_right ik a b = M.trace "bitfield" "shift_right"; - if BArith.is_invalid b || BArith.is_invalid a then (bot (), {underflow=false; overflow=false}) + if BArith.is_invalid b || BArith.is_invalid a || (isSigned ik && BArith.min ik b < Z.zero) then (bot (), {underflow=false; overflow=false}) else norm ik (BArith.shift_right ik a b) let shift_left ik a b = M.trace "bitfield" "shift_left"; - if BArith.is_invalid b || BArith.is_invalid a then (bot (), {underflow=false; overflow=false}) + if BArith.is_invalid b || BArith.is_invalid a || (isSigned ik && BArith.min ik b < Z.zero) then (bot (), {underflow=false; overflow=false}) else norm ik (BArith.shift_left ik a b) (* Arith *) diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index 03d930ed19..7f9be62dbe 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -468,13 +468,13 @@ struct let of_list ik is = List.fold_left (fun acc x -> I.join ik acc (I.of_int ik x)) (I.bot ()) is - let assert_shift shift symb ik a b res = + let assert_shift shift symb ik a b expected_values = let bs1 = of_list ik (List.map of_int a) in let bs2 = of_list ik (List.map of_int b) in - let bsr = of_list ik (List.map of_int res) in - let res = (shift ik bs1 bs2) in - let test_case_str = I.show bs1 ^ symb ^ I.show bs2 in - OUnit.assert_equal ~cmp:I.leq ~printer:I.show ~msg:test_case_str bsr res (*bsr <= res!*) + let bf_shift_res = (shift ik bs1 bs2) in + let output_string = I.show bs1 ^ symb ^ I.show bs2 in + let output_string elm = "Test shift (bf" ^ symb ^ string_of_int elm ^ ") failed: " ^ output_string in + List.iter (fun v -> assert_bool (output_string v) (let test_result = I.equal_to (of_int v) bf_shift_res in test_result = `Top || test_result = `Eq)) expected_values let assert_shift_left ik a b res = assert_shift I.shift_left " << " ik a b res let assert_shift_right ik a b res = assert_shift I.shift_right " >> " ik a b res @@ -482,20 +482,12 @@ struct let test_shift_left _ = assert_shift_left ik [2] [1] [4]; assert_shift_left ik [-2] [1] [-4]; - assert_shift_left ik [2; 16] [1; 2] [4; 8; 32; 64]; - assert_shift_left ik [-2; 16] [1; 2] [-8; -4; 32; 64]; - assert_shift_left ik [2; -16] [1; 2] [-64; -32; 4; 8]; - assert_shift_left ik [-2; -16] [1; 2] [-64; -32; -8; -4]; - assert_shift_left ik [-3; 5; -7; 11] [2; 5] [-224; -96; -28; -12; 20; 44; 160; 352] + assert_shift_left ik [2; 16] [1; 2] [4; 8; 32; 64] let test_shift_right _ = assert_shift_right ik [4] [1] [2]; assert_shift_right ik [-4] [1] [-2]; - assert_shift_right ik [8; 64] [3; 5] [0; 1; 2; 8]; - assert_shift_right ik [-2; 16] [1; 2] [-1; 0; 4; 8]; - assert_shift_right ik [2; -16] [1; 2] [-8; -4; 0; 1]; - assert_shift_right ik [-2; -16] [1; 2] [-8; -4; -1; 0]; - assert_shift_right ik [-53; 17; -24; 48] [3; 7] [-6; -3; 0; 2; 9] + assert_shift_right ik [8; 64] [3; 5] [0; 1; 2; 8] (* Arith *) From 7fa010084dbfa7e19b5ce799cb9d6a816d79f59c Mon Sep 17 00:00:00 2001 From: giaca Date: Tue, 26 Nov 2024 22:13:44 +0100 Subject: [PATCH 22/25] bugfix: certain zeros and uncertain ones --- src/cdomain/value/cdomains/intDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 8723dc25dd..5859b86f11 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1192,7 +1192,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let join_shrs c_lst = List.map (shift_right ik bf) c_lst |> List.fold_left join zero in let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in if Z.to_int (min ik bf) >= max_bit then zero - else concretize (fst bf &: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) + else concretize (fst bf |: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) |> join_shrs let shift_left _ (z,o) c = @@ -1205,7 +1205,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let join_shls c_lst = List.map (shift_left ik bf) c_lst |> List.fold_left join zero in let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in if Z.to_int (min ik bf) >= max_bit then zero - else concretize (fst bf &: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) + else concretize (fst bf |: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) |> join_shls end From e9286e798d8f6c159d03dc2d00811ca3e92d1db7 Mon Sep 17 00:00:00 2001 From: leon Date: Tue, 3 Dec 2024 09:54:26 +0100 Subject: [PATCH 23/25] fixed bitshifts --- src/cdomain/value/cdomains/intDomain.ml | 65 ++++++++++++++++++------- tests/unit/cdomains/intDomainTest.ml | 45 +++++++++++++++-- 2 files changed, 87 insertions(+), 23 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 5859b86f11..c82ab8f549 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1179,7 +1179,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let get_o (_,o) = Ints_t.to_int o - let shift_right ik (z,o) c = + (* let shift_right ik (z,o) c = let sign_msk = make_msb_bitmask (Size.bit ik - c) in if (isSigned ik) && (o <: Ints_t.zero) then (z >>: c, (o >>: c) |: sign_msk) @@ -1206,7 +1206,50 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in if Z.to_int (min ik bf) >= max_bit then zero else concretize (fst bf |: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) - |> join_shls + |> join_shls *) + + + let shift_right_action ik (z,o) c = + let sign_msk = make_msb_bitmask (Size.bit ik - c) in + if (isSigned ik) && (o <: Ints_t.zero) then + (z >>: c, (o >>: c) |: sign_msk) + else + ((z >>: c) |: sign_msk, o >>: c) + + let shift_right ik (z1, o1) (z2, o2) = + if is_const (z2, o2) then shift_right_action ik (z1, o1) (Ints_t.to_int o2) + else + let max_bit = Z.log2up (Z.of_int (Size.bit ik)) in + let mask = !:(one_mask<<:max_bit) in + let concrete_values = concretize ((z2 &: mask), (o2 &: mask)) in + if (List.length concrete_values) == 0 then (one_mask, zero_mask) + else + let (v1, v2) = (ref zero_mask, ref zero_mask) in + List.iter (fun x -> let (a, b) = (shift_right_action ik (z1, o1) x) in + v1 := !v1 |: a; + v2 := !v2 |: b + ) concrete_values; + (!v1, !v2) + + let shift_left_action _ (z,o) c = + let z_msk = make_lsb_bitmask c in + ((z <<: c) |: z_msk, o <<: c) + + let shift_left ik (z1, o1) (z2, o2) = + (* (one_mask, Ints_t.of_int (Size.bit ik)) *) + if is_const (z2, o2) then shift_left_action ik (z1, o1) (Ints_t.to_int o2) + else + let max_bit = Z.log2up (Z.of_int (Size.bit ik)) in + let mask = !:(one_mask<<:max_bit) in + let concrete_values = concretize ((z2 &: mask), (o2 &: mask)) in + if (List.length concrete_values) == 0 then (one_mask, zero_mask) + else + let (v1, v2) = (ref zero_mask, ref zero_mask) in + List.iter (fun x -> let (a, b) = (shift_left_action ik (z1, o1) x) in + v1 := !v1 |: a; + v2 := !v2 |: b + ) concrete_values; + (!v1, !v2) end @@ -1250,25 +1293,11 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let show t = if t = bot () then "bot" else if t = top () then "top" else - let string_of_bitfield (z,o) = - let max_num_unknown_bits_to_concretize = Z.log2 @@ Z.of_int (Sys.word_size) |> fun x -> x lsr 2 in - let num_bits_unknown = - try - BArith.bits_unknown (z,o) |> fun i -> Z.popcount @@ Z.of_int @@ Ints_t.to_int i - with Z.Overflow -> max_num_unknown_bits_to_concretize + 1 - in - if num_bits_unknown > max_num_unknown_bits_to_concretize then - Format.sprintf "(%016X, %016X)" (Ints_t.to_int z) (Ints_t.to_int o) - else - (* TODO: Might be a source of long running tests.*) - BArith.concretize (z,o) |> List.map string_of_int |> String.concat "; " - |> fun s -> "{" ^ s ^ "}" - in let (z,o) = t in if BArith.is_const t then - Format.sprintf "%s | %s (unique: %d)" (string_of_bitfield (z,o)) (to_pretty_bits t) (Ints_t.to_int o) + Format.sprintf "{%08X, %08X} (unique: %d)" (Ints_t.to_int z) (Ints_t.to_int o) (Ints_t.to_int o) else - Format.sprintf "%s | %s" (string_of_bitfield (z,o)) (to_pretty_bits t) + Format.sprintf "{%08X, %08X}" (Ints_t.to_int z) (Ints_t.to_int o) include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end) diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index 7f9be62dbe..2470ebf8ea 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -255,6 +255,7 @@ struct module I = IntDomain.SOverflowUnlifter (I) let ik = Cil.IInt + let ik_char = Cil.IChar let assert_equal x y = OUnit.assert_equal ~printer:I.show x y @@ -468,7 +469,7 @@ struct let of_list ik is = List.fold_left (fun acc x -> I.join ik acc (I.of_int ik x)) (I.bot ()) is - let assert_shift shift symb ik a b expected_values = + let assert_shift_xx shift symb ik a b expected_values = let bs1 = of_list ik (List.map of_int a) in let bs2 = of_list ik (List.map of_int b) in let bf_shift_res = (shift ik bs1 bs2) in @@ -476,19 +477,51 @@ struct let output_string elm = "Test shift (bf" ^ symb ^ string_of_int elm ^ ") failed: " ^ output_string in List.iter (fun v -> assert_bool (output_string v) (let test_result = I.equal_to (of_int v) bf_shift_res in test_result = `Top || test_result = `Eq)) expected_values + let assert_shift shift symb ik a b expected_values = + let bf1 = of_list ik (List.map of_int a) in + let bf2 = of_list ik (List.map of_int b) in + let bf_shift_resolution = (shift ik bf1 bf2) in + let x = of_list ik (List.map of_int expected_values) in + let output_string = I.show bf1 ^ symb ^ I.show bf2 ^ " was: " ^ I.show bf_shift_resolution ^ " but should be: " ^ I.show x in + let output = "Test shift ("^ I.show bf1 ^ symb ^ I.show bf2 ^ ") failed: " ^ output_string in + assert_bool (output) (I.equal bf_shift_resolution x) + let assert_shift_left ik a b res = assert_shift I.shift_left " << " ik a b res let assert_shift_right ik a b res = assert_shift I.shift_right " >> " ik a b res let test_shift_left _ = - assert_shift_left ik [2] [1] [4]; - assert_shift_left ik [-2] [1] [-4]; - assert_shift_left ik [2; 16] [1; 2] [4; 8; 32; 64] + assert_shift_left ik_char [-3] [7] [-128]; + assert_shift_left ik [-3] [7] [-384]; + assert_shift_left ik [2] [1; 2] [2; 4; 8; 16]; + assert_shift_left ik [1; 2] [1] [2; 4]; + assert_shift_left ik [-1; 1] [1] [-2; 2]; + assert_shift_left ik [-1] [4] [-16]; + assert_shift_left ik [-1] [1] [-2]; + assert_shift_left ik [-1] [2] [-4]; + assert_shift_left ik [-1] [3] [-8]; + assert_shift_left ik [-2] [1; 2] [-2; -4; -8; -16]; + assert_shift_left ik [-1] [1; 2] [-1; -2; -4; -8] + + + (* assert_shift_left ik [1] [64] [0]; + assert_shift_left ik [1] [64; 128] [0] *) let test_shift_right _ = assert_shift_right ik [4] [1] [2]; assert_shift_right ik [-4] [1] [-2]; - assert_shift_right ik [8; 64] [3; 5] [0; 1; 2; 8] + assert_shift_right ik [1] [1] [0]; + assert_shift_right ik [1] [1; 2] [0; 1]; + assert_shift_right ik [1; 2] [1; 2] [0; 1; 2; 3] + + + (* assert_shift_right ik [8; 64] [3; 5] [0; 1; 2; 8]; + assert_shift_right ik [8; 64] [1] [4; 32]; + assert_shift_right ik [8; 64] [3; 5] [0; 1; 2; 4; 8; 32]; + assert_shift_right ik [-2; 16] [1; 2] [-1; 0; 4; 8]; + assert_shift_right ik [2; -16] [1; 2] [-8; -4; 0; 1]; + assert_shift_right ik [-2; -16] [1; 2] [-8; -4; -1; 0]; + assert_shift_right ik [-53; 17; -24; 48] [3; 7] [-6; -3; 0; 2; 9] *) (* Arith *) @@ -736,6 +769,7 @@ struct "test_widen_1" >:: test_widen_1; "test_widen_2" >:: test_widen_2; + "test_of_interval" >:: test_of_interval; "test_of_bool" >:: test_of_bool; "test_to_bool" >:: test_to_bool; @@ -745,6 +779,7 @@ struct "test_logand" >:: test_logand; "test_logor" >:: test_logor; "test_lognot" >:: test_lognot; + "test_shift_left" >:: test_shift_left; "test_shift_right" >:: test_shift_right; From 3e4928ae5a87ae16c730014b69724d228b052e00 Mon Sep 17 00:00:00 2001 From: leon Date: Tue, 3 Dec 2024 09:56:14 +0100 Subject: [PATCH 24/25] removed commmented code and old wrong testcases --- src/cdomain/value/cdomains/intDomain.ml | 30 ------------------------- tests/unit/cdomains/intDomainTest.ml | 20 ----------------- 2 files changed, 50 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index c82ab8f549..6ac8985615 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1179,36 +1179,6 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let get_o (_,o) = Ints_t.to_int o - (* let shift_right ik (z,o) c = - let sign_msk = make_msb_bitmask (Size.bit ik - c) in - if (isSigned ik) && (o <: Ints_t.zero) then - (z >>: c, (o >>: c) |: sign_msk) - else - ((z >>: c) |: sign_msk, o >>: c) - - let shift_right ik bf possible_shifts = - if is_const possible_shifts then shift_right ik bf (get_o possible_shifts) - else - let join_shrs c_lst = List.map (shift_right ik bf) c_lst |> List.fold_left join zero in - let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in - if Z.to_int (min ik bf) >= max_bit then zero - else concretize (fst bf |: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) - |> join_shrs - - let shift_left _ (z,o) c = - let z_msk = make_lsb_bitmask c in - ((z <<: c) |: z_msk, o <<: c) - - let shift_left ik bf possible_shifts = - if is_const possible_shifts then shift_left ik bf (get_o possible_shifts) - else - let join_shls c_lst = List.map (shift_left ik bf) c_lst |> List.fold_left join zero in - let max_bit = Z.log2up (Z.of_int @@ Size.bit ik) in - if Z.to_int (min ik bf) >= max_bit then zero - else concretize (fst bf |: make_msb_bitmask max_bit, snd bf &: make_lsb_bitmask max_bit) (* O( 2^(log(n)) ) *) - |> join_shls *) - - let shift_right_action ik (z,o) c = let sign_msk = make_msb_bitmask (Size.bit ik - c) in if (isSigned ik) && (o <: Ints_t.zero) then diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index 2470ebf8ea..e8b9ae809f 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -469,14 +469,6 @@ struct let of_list ik is = List.fold_left (fun acc x -> I.join ik acc (I.of_int ik x)) (I.bot ()) is - let assert_shift_xx shift symb ik a b expected_values = - let bs1 = of_list ik (List.map of_int a) in - let bs2 = of_list ik (List.map of_int b) in - let bf_shift_res = (shift ik bs1 bs2) in - let output_string = I.show bs1 ^ symb ^ I.show bs2 in - let output_string elm = "Test shift (bf" ^ symb ^ string_of_int elm ^ ") failed: " ^ output_string in - List.iter (fun v -> assert_bool (output_string v) (let test_result = I.equal_to (of_int v) bf_shift_res in test_result = `Top || test_result = `Eq)) expected_values - let assert_shift shift symb ik a b expected_values = let bf1 = of_list ik (List.map of_int a) in let bf2 = of_list ik (List.map of_int b) in @@ -503,25 +495,13 @@ struct assert_shift_left ik [-1] [1; 2] [-1; -2; -4; -8] - (* assert_shift_left ik [1] [64] [0]; - assert_shift_left ik [1] [64; 128] [0] *) - let test_shift_right _ = assert_shift_right ik [4] [1] [2]; assert_shift_right ik [-4] [1] [-2]; assert_shift_right ik [1] [1] [0]; assert_shift_right ik [1] [1; 2] [0; 1]; assert_shift_right ik [1; 2] [1; 2] [0; 1; 2; 3] - - - (* assert_shift_right ik [8; 64] [3; 5] [0; 1; 2; 8]; - assert_shift_right ik [8; 64] [1] [4; 32]; - assert_shift_right ik [8; 64] [3; 5] [0; 1; 2; 4; 8; 32]; - assert_shift_right ik [-2; 16] [1; 2] [-1; 0; 4; 8]; - assert_shift_right ik [2; -16] [1; 2] [-8; -4; 0; 1]; - assert_shift_right ik [-2; -16] [1; 2] [-8; -4; -1; 0]; - assert_shift_right ik [-53; 17; -24; 48] [3; 7] [-6; -3; 0; 2; 9] *) (* Arith *) From 9bcd884ad3530558ae3a2f73cc23212d7b33a405 Mon Sep 17 00:00:00 2001 From: leon Date: Tue, 3 Dec 2024 15:32:09 +0100 Subject: [PATCH 25/25] fixed edge case where shift with 0 was done without zero in shifting bf --- src/cdomain/value/cdomains/intDomain.ml | 24 ++++++++++++++++-------- tests/unit/cdomains/intDomainTest.ml | 9 ++++++--- 2 files changed, 22 insertions(+), 11 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 6ac8985615..09d40084e4 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1187,12 +1187,16 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct ((z >>: c) |: sign_msk, o >>: c) let shift_right ik (z1, o1) (z2, o2) = - if is_const (z2, o2) then shift_right_action ik (z1, o1) (Ints_t.to_int o2) + if is_const (z2, o2) + then + shift_right_action ik (z1, o1) (Ints_t.to_int o2) else let max_bit = Z.log2up (Z.of_int (Size.bit ik)) in - let mask = !:(one_mask<<:max_bit) in - let concrete_values = concretize ((z2 &: mask), (o2 &: mask)) in - if (List.length concrete_values) == 0 then (one_mask, zero_mask) + let mask_usefull_bits = !:(one_mask<<:max_bit) in + let concrete_values = concretize ((z2 &: mask_usefull_bits), (o2 &: mask_usefull_bits)) in + if (((o2 &: mask_usefull_bits) == Ints_t.of_int 0) && (z2 != one_mask)) || (List.length concrete_values) == 0 + then + (one_mask, zero_mask) else let (v1, v2) = (ref zero_mask, ref zero_mask) in List.iter (fun x -> let (a, b) = (shift_right_action ik (z1, o1) x) in @@ -1207,12 +1211,16 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let shift_left ik (z1, o1) (z2, o2) = (* (one_mask, Ints_t.of_int (Size.bit ik)) *) - if is_const (z2, o2) then shift_left_action ik (z1, o1) (Ints_t.to_int o2) + if is_const (z2, o2) + then + shift_left_action ik (z1, o1) (Ints_t.to_int o2) else let max_bit = Z.log2up (Z.of_int (Size.bit ik)) in - let mask = !:(one_mask<<:max_bit) in - let concrete_values = concretize ((z2 &: mask), (o2 &: mask)) in - if (List.length concrete_values) == 0 then (one_mask, zero_mask) + let mask_usefull_bits = !:(one_mask <<: max_bit) in + let concrete_values = concretize ((z2 &: mask_usefull_bits), (o2 &: mask_usefull_bits)) in + if (((o2 &: mask_usefull_bits) == Ints_t.of_int 0) && (z2 != one_mask)) || (List.length concrete_values) == 0 + then + (one_mask, zero_mask) else let (v1, v2) = (ref zero_mask, ref zero_mask) in List.iter (fun x -> let (a, b) = (shift_left_action ik (z1, o1) x) in diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index e8b9ae809f..b3de4fe99f 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -492,15 +492,18 @@ struct assert_shift_left ik [-1] [2] [-4]; assert_shift_left ik [-1] [3] [-8]; assert_shift_left ik [-2] [1; 2] [-2; -4; -8; -16]; - assert_shift_left ik [-1] [1; 2] [-1; -2; -4; -8] - + assert_shift_left ik [-1] [1; 2] [-1; -2; -4; -8]; + assert_shift_left ik [1073741824] [128; 384] [0]; + assert_shift_left ik [1073741824] [0; 128; 384] [1073741824] let test_shift_right _ = assert_shift_right ik [4] [1] [2]; assert_shift_right ik [-4] [1] [-2]; assert_shift_right ik [1] [1] [0]; assert_shift_right ik [1] [1; 2] [0; 1]; - assert_shift_right ik [1; 2] [1; 2] [0; 1; 2; 3] + assert_shift_right ik [1; 2] [1; 2] [0; 1; 2; 3]; + assert_shift_right ik [32] [64; 2] [8; 32]; + assert_shift_right ik [32] [128; 384] [0] (* Arith *)