From 6fe1162b96d9376181533f078f7769080470c812 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adrian=20Krau=C3=9F?= Date: Tue, 3 Dec 2024 16:20:45 +0100 Subject: [PATCH 1/3] added of bitfield for refinements --- src/analyses/baseInvariant.ml | 20 ++++++++- src/cdomain/value/cdomains/intDomain.ml | 53 +++++++++++++++++++++++- src/cdomain/value/cdomains/intDomain.mli | 4 ++ 3 files changed, 73 insertions(+), 4 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 51a27e19f8..661fd481fa 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -395,10 +395,26 @@ struct | Le, Some false -> meet_bin (ID.starting ikind (Z.succ l2)) (ID.ending ikind (Z.pred u1)) | _, _ -> a, b) | _ -> a, b) - | BOr | BXor as op-> - if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op; + | BOr as op-> + if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op; (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *) a, b + | BXor as op -> + if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op; + let a' = match ID.to_int b, ID.to_int c with + Some b, Some c -> (let res = IntDomain.Bitfield.to_int (IntDomain.Bitfield.logxor ikind (fst (IntDomain.Bitfield.of_int ikind b)) (fst (IntDomain.Bitfield.of_int ikind c))) in + match res with + Some r -> ID.meet a (ID.of_int ikind r) | + None -> a) | + _, _ -> a + in let b' = match ID.to_int a, ID.to_int c with + Some a, Some c -> (let res = IntDomain.Bitfield.to_int (IntDomain.Bitfield.logxor ikind (fst (IntDomain.Bitfield.of_int ikind a)) (fst (IntDomain.Bitfield.of_int ikind c))) in + match res with + Some r -> ID.meet b (ID.of_int ikind r) | + None -> b) | + _, _ -> b + (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *) + in a', b' | LAnd -> if ID.to_bool c = Some true then meet_bin c c diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 5859b86f11..1983d601d8 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -233,6 +233,7 @@ sig val of_bool: bool -> t val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t val of_congruence: Cil.ikind -> int_t * int_t -> t + val of_bitfield: Cil.ikind -> int_t * int_t -> t val arbitrary: unit -> t QCheck.arbitrary val invariant: Cil.exp -> t -> Invariant.t end @@ -260,6 +261,7 @@ sig val of_bool: Cil.ikind -> bool -> t val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t val of_congruence: Cil.ikind -> int_t * int_t -> t + val of_bitfield: Cil.ikind -> int_t * int_t -> t val is_top_of: Cil.ikind -> t -> bool val invariant_ikind : Cil.exp -> Cil.ikind -> t -> Invariant.t @@ -310,6 +312,7 @@ sig val of_bool: Cil.ikind -> bool -> t val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t val of_congruence: Cil.ikind -> int_t * int_t -> t + val of_bitfield: Cil.ikind -> int_t * int_t -> t val starting : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t val ending : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t @@ -388,6 +391,8 @@ struct let to_incl_list x = I.to_incl_list x.v let of_interval ?(suppress_ovwarn=false) ikind (lb,ub) = {v = I.of_interval ~suppress_ovwarn ikind (lb,ub); ikind} let of_congruence ikind (c,m) = {v = I.of_congruence ikind (c,m); ikind} + let of_bitfield ikind (z,o) = {v = I.of_bitfield ikind (z,o); ikind} + let starting ?(suppress_ovwarn=false) ikind i = {v = I.starting ~suppress_ovwarn ikind i; ikind} let ending ?(suppress_ovwarn=false) ikind i = {v = I.ending ~suppress_ovwarn ikind i; ikind} let maximal x = I.maximal x.v @@ -522,6 +527,7 @@ module StdTop (B: sig type t val top_of: Cil.ikind -> t end) = struct let to_incl_list x = None let of_interval ?(suppress_ovwarn=false) ik x = top_of ik let of_congruence ik x = top_of ik + let of_bitfield ik x = top_of ik let starting ?(suppress_ovwarn=false) ik x = top_of ik let ending ?(suppress_ovwarn=false) ik x = top_of ik let maximal x = None @@ -748,7 +754,25 @@ struct (* TODO: change to_int signature so it returns a big_int *) let to_int x = Option.bind x (IArith.to_int) + let to_excl_list x = None + let of_excl_list ik x = top_of ik + let is_excl_list x = false + let to_incl_list x = None let of_interval ?(suppress_ovwarn=false) ik (x,y) = norm ~suppress_ovwarn ik @@ Some (x,y) + let of_bitfield ik x = + 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.logor signMask (Ints_t.lognot z) + else Ints_t.lognot z + in let max ik (z,o) = + 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.logand signMask o + else o + in fst (norm ik (Some (min ik x, max ik x))) let of_int ik (x: int_t) = of_interval ik (x,x) let zero = Some IArith.zero let one = Some IArith.one @@ -1273,8 +1297,13 @@ 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 maximal (z,o) = let isPositive = z < Ints_t.zero in + if o < Ints_t.zero && isPositive then (match Ints_t.upper_bound with Some maxVal -> Some (maxVal &: o) | None -> None ) + else Some o + + let minimal (z,o) = let isNegative = o < Ints_t.zero in + if z < Ints_t.zero && isNegative then (match Ints_t.lower_bound with Some minVal -> Some (minVal |: (!:z)) | None -> None ) + else Some (!:z) let norm ?(suppress_ovwarn=false) ik (z,o) = if BArith.is_invalid (z,o) then @@ -1331,6 +1360,8 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int done; norm ~suppress_ovwarn ik !bf + let of_congruence ik (c,m) = (if m = Ints_t.zero then fst (of_int ik c) else top_of ik) + let of_bool _ik = function true -> BArith.one | false -> BArith.zero let to_bool d = @@ -1564,6 +1595,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int 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 @@ -1800,6 +1832,21 @@ struct let of_interval ?(suppress_ovwarn=false) ik (x,y) = norm_interval ~suppress_ovwarn ~cast:false ik (x,y) + let of_bitfield ik x = + 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.logor signMask (Ints_t.lognot z) + else Ints_t.lognot z + in let max ik (z,o) = + 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.logand signMask o + else o + in fst (norm_interval ik (min ik x, max ik x)) + let of_int ik (x: int_t) = of_interval ik (x, x) let lt ik x y = @@ -2241,6 +2288,7 @@ struct let to_incl_list x = None let of_interval ?(suppress_ovwarn=false) ik x = top_of ik let of_congruence ik x = top_of ik + let of_bitfield ik x = top_of ik let starting ?(suppress_ovwarn=false) ikind x = top_of ikind let ending ?(suppress_ovwarn=false) ikind x = top_of ikind let maximal x = None @@ -3912,6 +3960,7 @@ module IntDomTupleImpl = struct let ending ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.ending ~suppress_ovwarn ik } let of_interval ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_interval ~suppress_ovwarn ik } let of_congruence ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_congruence ik } + let of_bitfield ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_bitfield ik } let refine_with_congruence ik ((a, b, c, d, e, f) : t) (cong : (int_t * int_t) option) : t= let opt f a = diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli index d6bb233aee..401ba84e94 100644 --- a/src/cdomain/value/cdomains/intDomain.mli +++ b/src/cdomain/value/cdomains/intDomain.mli @@ -228,6 +228,7 @@ sig val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t val of_congruence: Cil.ikind -> int_t * int_t -> t + val of_bitfield: Cil.ikind -> int_t * int_t -> t val arbitrary: unit -> t QCheck.arbitrary val invariant: Cil.exp -> t -> Invariant.t end @@ -262,6 +263,7 @@ sig val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t val of_congruence: Cil.ikind -> int_t * int_t -> t + val of_bitfield: Cil.ikind -> int_t * int_t -> t val is_top_of: Cil.ikind -> t -> bool val invariant_ikind : Cil.exp -> Cil.ikind -> t -> Invariant.t @@ -325,6 +327,8 @@ sig val of_congruence: Cil.ikind -> int_t * int_t -> t + val of_bitfield: Cil.ikind -> int_t * int_t -> t + val starting : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t val ending : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t From 6c2c5708a9059790bcffa31e57dfcce2d6edeae7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adrian=20Krau=C3=9F?= Date: Sat, 7 Dec 2024 17:02:36 +0100 Subject: [PATCH 2/3] simple refinements for base invariant with bitfields --- src/analyses/baseInvariant.ml | 32 ++-- src/cdomain/value/cdomains/intDomain.ml | 166 +++++++++++------- src/cdomain/value/cdomains/intDomain.mli | 1 + .../82-bitfield/10-refine-interval.c | 19 ++ 4 files changed, 133 insertions(+), 85 deletions(-) create mode 100644 tests/regression/82-bitfield/10-refine-interval.c diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 661fd481fa..950fd6f236 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -395,26 +395,18 @@ struct | Le, Some false -> meet_bin (ID.starting ikind (Z.succ l2)) (ID.ending ikind (Z.pred u1)) | _, _ -> a, b) | _ -> a, b) - | BOr as op-> - if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op; + | BOr -> (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *) - a, b - | BXor as op -> - if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op; - let a' = match ID.to_int b, ID.to_int c with - Some b, Some c -> (let res = IntDomain.Bitfield.to_int (IntDomain.Bitfield.logxor ikind (fst (IntDomain.Bitfield.of_int ikind b)) (fst (IntDomain.Bitfield.of_int ikind c))) in - match res with - Some r -> ID.meet a (ID.of_int ikind r) | - None -> a) | - _, _ -> a - in let b' = match ID.to_int a, ID.to_int c with - Some a, Some c -> (let res = IntDomain.Bitfield.to_int (IntDomain.Bitfield.logxor ikind (fst (IntDomain.Bitfield.of_int ikind a)) (fst (IntDomain.Bitfield.of_int ikind c))) in - match res with - Some r -> ID.meet b (ID.of_int ikind r) | - None -> b) | - _, _ -> b + if PrecisionUtil.get_bitfield () then + ID.meet a (ID.logand a c), ID.meet b (ID.logand b c) + else a, b + | BXor -> (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *) - in a', b' + if PrecisionUtil.get_bitfield () then + let a' = ID.meet a (ID.logxor c b) + in let b' = ID.meet b (ID.logxor a c) + in a', b' + else a,b | LAnd -> if ID.to_bool c = Some true then meet_bin c c @@ -431,7 +423,9 @@ struct | None -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a 1 = %a" d_binop op ID.pretty c; a) | _ -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a %a = %a" d_binop op ID.pretty b ID.pretty c; a in - a, b + if PrecisionUtil.get_bitfield () then + ID.meet a (ID.logor a c), ID.meet b (ID.logor b c) + else a, b | op -> if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op; a, b diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 1983d601d8..2a9ae32562 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -267,6 +267,7 @@ sig val refine_with_congruence: Cil.ikind -> t -> (int_t * int_t) option -> t val refine_with_interval: Cil.ikind -> t -> (int_t * int_t) option -> t + val refine_with_bitfield: Cil.ikind -> t -> (int_t * int_t) -> t val refine_with_excl_list: Cil.ikind -> t -> (int_t list * (int64 * int64)) option -> t val refine_with_incl_list: Cil.ikind -> t -> int_t list option -> t @@ -1077,6 +1078,10 @@ struct let refine_with_interval ik a b = meet ik a b + let refine_with_bitfield ik a b = + let interv = of_bitfield ik b in + meet ik a interv + let refine_with_excl_list ik (intv : t) (excl : (int_t list * (int64 * int64)) option) : t = match intv, excl with | None, _ | _, None -> intv @@ -1150,7 +1155,9 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct let bits_invalid (z,o) = !:(z |: o) let is_const (z,o) = (z ^: o) =: one_mask - let is_invalid (z,o) = not ((!:(z |: o)) =: Ints_t.zero) + let is_invalid ik (z,o) = + let mask = !:(Ints_t.of_bigint (snd (Size.range ik))) in + not ((!:(z |: o |: mask)) = Ints_t.zero) let nabla x y= if x =: (x |: y) then x else one_mask @@ -1265,38 +1272,22 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let next_bit_string = if current_bit_impossible = Ints_t.one then "⊥" - else if current_bit_known = Ints_t.one || current_bit_known = Ints_t.zero + else if current_bit_known = Ints_t.one 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) in - to_pretty_bits' known_bits invalid_bits o num_bits_to_print "" - - 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) - else - Format.sprintf "%s | %s" (string_of_bitfield (z,o)) (to_pretty_bits t) + "0b" ^ to_pretty_bits' known_bits invalid_bits o num_bits_to_print "" + + let show t = + if t = bot () then "bot" else + if t = top () then "top" else + let (z,o) = t in + Format.sprintf "{zs:%d, os:%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) let range ik bf = (BArith.min ik bf, BArith.max ik bf) + let maximal (z,o) = let isPositive = z < Ints_t.zero in if o < Ints_t.zero && isPositive then (match Ints_t.upper_bound with Some maxVal -> Some (maxVal &: o) | None -> None ) else Some o @@ -1305,10 +1296,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int if z < Ints_t.zero && isNegative then (match Ints_t.lower_bound with Some minVal -> Some (minVal |: (!:z)) | None -> None ) else Some (!:z) - let norm ?(suppress_ovwarn=false) ik (z,o) = - if BArith.is_invalid (z,o) then + let norm ?(debug=false) ?(suppress_ovwarn=false) ik (z,o) = + if BArith.is_invalid ik (z,o) then (bot (), {underflow=false; overflow=false}) - else + else let (min_ik, max_ik) = Size.range ik in let wrap ik (z,o) = if isSigned ik then @@ -1352,13 +1343,41 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let of_interval ?(suppress_ovwarn=false) ik (x,y) = let (min_ik, max_ik) = Size.range ik in - 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 + let startv = Ints_t.max x (Ints_t.of_bigint min_ik) in + let endv= Ints_t.min y (Ints_t.of_bigint max_ik) in + + let rec analyze_bits pos (acc_z, acc_o) = + if pos < 0 then (acc_z, acc_o) + else + let position = Ints_t.shift_left Ints_t.one pos in + let mask = Ints_t.sub position Ints_t.one in + let remainder = Ints_t.logand startv mask in + + let without_remainder = Ints_t.sub startv remainder in + let bigger_number = Ints_t.add without_remainder position in + + let bit_status = + if Ints_t.compare bigger_number endv <= 0 then + `top + else + if Ints_t.equal (Ints_t.logand (Ints_t.shift_right startv pos) Ints_t.one) Ints_t.one then + `one + else + `zero + in + + let new_acc = + match bit_status with + | `top -> (Ints_t.logor position acc_z, Ints_t.logor position acc_o) + | `one -> (Ints_t.logand (Ints_t.lognot position) acc_z, Ints_t.logor position acc_o) + | `zero -> (Ints_t.logor position acc_z, Ints_t.logand (Ints_t.lognot position) acc_o) + + in + analyze_bits (pos - 1) new_acc + in + let result = analyze_bits (Size.bit ik - 1) (bot()) in + let casted = (Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (fst result)))), Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (snd result))))) + in norm ~debug:true ~suppress_ovwarn ik casted let of_congruence ik (c,m) = (if m = Ints_t.zero then fst (of_int ik c) else top_of ik) @@ -1403,12 +1422,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 || (isSigned ik && BArith.min ik b < Z.zero) then (bot (), {underflow=false; overflow=false}) + if BArith.is_invalid ik b || BArith.is_invalid ik 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 || (isSigned ik && BArith.min ik b < Z.zero) then (bot (), {underflow=false; overflow=false}) + if BArith.is_invalid ik b || BArith.is_invalid ik 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 *) @@ -1438,7 +1457,11 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let (rv, rm) = add_paper pv pm qv qm in let o3 = rv |: rm in let z3 = !:rv |: rm in - norm ik (z3, o3) + (* let _ = print_endline (show (z3, o3)) in + let _ = (match maximal (z3,o3) with Some k -> print_endline (Ints_t.to_string k) | None -> print_endline "None") in + let _ = (match minimal (z3,o3) with Some k -> print_endline (Ints_t.to_string k) | None -> print_endline "None") in + let _ = (match Size.range ik with (a,b) -> print_endline ("(" ^ Z.to_string a ^ "; " ^ Z.to_string b ^ ")")) in *) + norm ik (z3,o3) let sub ?no_ov ik (z1, o1) (z2, o2) = let pv = o1 &: !:z1 in @@ -1499,12 +1522,9 @@ 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)) - else top_of ik + match to_int x, to_int y with + Some a, Some b -> fst (of_int ik (Ints_t.rem a b)) | + _, _ -> top_of ik 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 @@ -1534,37 +1554,30 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int IntInvariant.of_interval e ik range 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 = BArith.make_bitone_msk (Size.bit ik - 1) in - let zs = BArith.one_mask in - let os = !:signBitMask &: BArith.one_mask in - (norm ~suppress_ovwarn ik @@ (zs,os)) - else - (norm ~suppress_ovwarn ik @@ (top ())) + let (min_ik, max_ik) = Size.range ik in + of_interval ~suppress_ovwarn ik (n, Ints_t.of_bigint max_ik) 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 = BArith.make_bitone_msk (Size.bit ik - 1) in - let zs = !:signBitMask &: BArith.one_mask in - let os = BArith.one_mask in - (norm ~suppress_ovwarn ik @@ (zs,os)) - else - (norm ~suppress_ovwarn ik @@ (top ())) + let (min_ik, max_ik) = Size.range ik in + of_interval ~suppress_ovwarn ik (Ints_t.of_bigint min_ik, n) + let is_power_of_two x = (x &: (x -: Ints_t.one) = Ints_t.zero) let refine_with_congruence ik bf ((cong) : (int_t * int_t ) option) : t = - 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 -> + | (z,o), Some (c, m) when is_power_of_two m && m <> Ints_t.one -> 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 - let refine_with_interval ik t i = norm ik t |> fst + let refine_with_interval ik t itv = + match itv with + | None -> norm ik t |> fst + | Some (l, u) -> meet ik t (of_interval ik (l, u) |> fst) + + let refine_with_bitfield ik x y = meet ik x y let refine_with_excl_list ik t (excl : (int_t list * (int64 * int64)) option) : t = norm ik t |> fst @@ -2112,6 +2125,10 @@ struct let refine_with_interval ik xs = function None -> [] | Some (a,b) -> meet ik xs [(a,b)] + let refine_with_bitfield ik x y = + let interv = of_bitfield ik y in + meet ik x interv + let refine_with_incl_list ik intvs = function | None -> intvs | Some xs -> meet ik intvs (List.map (fun x -> (x,x)) xs) @@ -2937,6 +2954,7 @@ struct let refine_with_interval ik a b = match a, b with | x, Some(i) -> meet ik x (of_interval ik i) | _ -> a + let refine_with_bitfield ik x y = x let refine_with_excl_list ik a b = match a, b with | `Excluded (s, r), Some(ls, _) -> meet ik (`Excluded (s, r)) (of_excl_list ik ls) (* TODO: refine with excl range? *) | _ -> a @@ -3299,6 +3317,8 @@ module Enums : S with type int_t = Z.t = struct let refine_with_interval ik a b = a (* TODO: refine inclusion (exclusion?) set *) + let refine_with_bitfield ik x y = x + let refine_with_excl_list ik a b = match b with | Some (ls, _) -> meet ik a (of_excl_list ik ls) (* TODO: refine with excl range? *) @@ -3798,6 +3818,8 @@ struct if M.tracing then M.trace "refine" "cong_refine_with_interval %a %a -> %a" pretty cong pretty_intv intv pretty refn; refn + let refine_with_bitfield ik a b = a + let refine_with_congruence ik a b = meet ik a b let refine_with_excl_list ik a b = a let refine_with_incl_list ik a b = a @@ -3985,6 +4007,17 @@ module IntDomTupleImpl = struct , opt I5.refine_with_interval ik e intv , opt I6.refine_with_interval ik f intv ) + let refine_with_bitfield ik (a, b, c, d, e,f) bf = + let opt f a = + curry @@ function Some x, y -> Some (f a x y) | _ -> None + in + ( opt I1.refine_with_bitfield ik a bf + , opt I2.refine_with_bitfield ik b bf + , opt I3.refine_with_bitfield ik c bf + , opt I4.refine_with_bitfield ik d bf + , opt I5.refine_with_bitfield ik e bf + , opt I6.refine_with_bitfield ik f bf ) + let refine_with_excl_list ik (a, b, c, d, e,f) excl = let opt f a = curry @@ function Some x, y -> Some (f a x y) | _ -> None @@ -4096,8 +4129,9 @@ module IntDomTupleImpl = struct in [(fun (a, b, c, d, e, f) -> refine_with_excl_list ik (a, b, c, d, e,f) (to_excl_list (a, b, c, d, e,f))); (fun (a, b, c, d, e, f) -> refine_with_incl_list ik (a, b, c, d, e,f) (to_incl_list (a, b, c, d, e,f))); - (fun (a, b, c, d, e, f) -> maybe refine_with_interval ik (a, b, c, d, e,f) b); (* TODO: get interval across all domains with minimal and maximal *) - (fun (a, b, c, d, e, f) -> maybe refine_with_congruence ik (a, b, c, d, e,f) d)] + (fun (a, b, c, d, e, f) -> maybe refine_with_interval ik (a, b, c, d, e, f) b); (* TODO: get interval across all domains with minimal and maximal *) + (fun (a, b, c, d, e, f) -> maybe refine_with_congruence ik (a, b, c, d, e, f) d); + (fun (a, b, c, d, e, f) -> maybe refine_with_bitfield ik (a, b, c, d, e, f) f)] let refine ik ((a, b, c, d, e,f) : t ) : t = let dt = ref (a, b, c, d, e,f) in diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli index 401ba84e94..55149cdb54 100644 --- a/src/cdomain/value/cdomains/intDomain.mli +++ b/src/cdomain/value/cdomains/intDomain.mli @@ -269,6 +269,7 @@ sig val refine_with_congruence: Cil.ikind -> t -> (int_t * int_t) option -> t val refine_with_interval: Cil.ikind -> t -> (int_t * int_t) option -> t + val refine_with_bitfield: Cil.ikind -> t -> (int_t * int_t) -> t val refine_with_excl_list: Cil.ikind -> t -> (int_t list * (int64 * int64)) option -> t val refine_with_incl_list: Cil.ikind -> t -> int_t list option -> t diff --git a/tests/regression/82-bitfield/10-refine-interval.c b/tests/regression/82-bitfield/10-refine-interval.c new file mode 100644 index 0000000000..d49e9937de --- /dev/null +++ b/tests/regression/82-bitfield/10-refine-interval.c @@ -0,0 +1,19 @@ +// PARAM: --enable ana.int.interval --enable ana.int.bitfield --set ana.int.refinement fixpoint --trace inv --trace branch --trace invariant +#include + +int main() { + unsigned char r; // non-neg rand + char x = r % 64; + + if ((r | x) == 0) { + __goblint_check(r == 0); // SUCCESS + __goblint_check(x == 0); // SUCCESS + } + + if ((r & x) == 63) { + __goblint_check(r & 63 == 63); // SUCCESS + __goblint_check(x == 63); // SUCCESS + } + + +} From e4eefd93cbc24e8cb4fda0fe04d566d060d33950 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adrian=20Krau=C3=9F?= Date: Mon, 9 Dec 2024 18:45:05 +0100 Subject: [PATCH 3/3] added to_bitfield to refine base invariant further and regression test --- src/analyses/baseInvariant.ml | 30 ++++-- src/cdomain/value/cdomains/intDomain.ml | 94 ++++++++++++++++++- src/cdomain/value/cdomains/intDomain.mli | 2 + .../82-bitfield/10-refine-interval.c | 3 + .../82-bitfield/11-refine-interval2.c | 17 ++++ 5 files changed, 136 insertions(+), 10 deletions(-) create mode 100644 tests/regression/82-bitfield/11-refine-interval2.c diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 950fd6f236..08f96a6185 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -398,7 +398,16 @@ struct | BOr -> (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *) if PrecisionUtil.get_bitfield () then - ID.meet a (ID.logand a c), ID.meet b (ID.logand b c) + let a', b' = ID.meet a (ID.logand a c), ID.meet b (ID.logand b c) in + let (cz, co) = ID.to_bitfield ikind c in + let (az, ao) = ID.to_bitfield ikind a' in + let (bz, bo) = ID.to_bitfield ikind b' in + let cDef1 = Z.logand co (Z.lognot cz) in + let aDef0 = Z.logand az (Z.lognot ao) in + let bDef0 = Z.logand bz (Z.lognot bo) in + let az = Z.logand az (Z.lognot (Z.logand bDef0 cDef1)) in + let bz = Z.logand bz (Z.lognot (Z.logand aDef0 cDef1)) in + ID.meet a' (ID.of_bitfield ikind (az, ao)), ID.meet b' (ID.of_bitfield ikind (bz, bo)) else a, b | BXor -> (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *) @@ -412,7 +421,7 @@ struct meet_bin c c else a, b - | BAnd as op -> + | BAnd -> (* we only attempt to refine a here *) let a = match ID.to_int b with @@ -420,11 +429,20 @@ struct (match ID.to_bool c with | Some true -> ID.meet a (ID.of_congruence ikind (Z.one, Z.of_int 2)) | Some false -> ID.meet a (ID.of_congruence ikind (Z.zero, Z.of_int 2)) - | None -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a 1 = %a" d_binop op ID.pretty c; a) - | _ -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a %a = %a" d_binop op ID.pretty b ID.pretty c; a + | None -> a) + | _ -> a in - if PrecisionUtil.get_bitfield () then - ID.meet a (ID.logor a c), ID.meet b (ID.logor b c) + if PrecisionUtil.get_bitfield () then + let a', b' = ID.meet a (ID.logor a c), ID.meet b (ID.logor b c) in + let (cz, co) = ID.to_bitfield ikind c in + let (az, ao) = ID.to_bitfield ikind a' in + let (bz, bo) = ID.to_bitfield ikind b' in + let cDef0 = Z.logand cz (Z.lognot co) in + let aDef1 = Z.logand ao (Z.lognot az) in + let bDef1 = Z.logand bo (Z.lognot bz) in + let ao = Z.logand ao (Z.lognot (Z.logand bDef1 cDef0)) in + let bo = Z.logand bo (Z.lognot (Z.logand aDef1 cDef0)) in + ID.meet a' (ID.of_bitfield ikind (az, ao)), ID.meet b' (ID.of_bitfield ikind (bz, bo)) else a, b | op -> if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op; diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 2a9ae32562..d2c92415ff 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -262,6 +262,7 @@ sig val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t val of_congruence: Cil.ikind -> int_t * int_t -> t val of_bitfield: Cil.ikind -> int_t * int_t -> t + val to_bitfield: Cil.ikind -> t -> int_t * int_t val is_top_of: Cil.ikind -> t -> bool val invariant_ikind : Cil.exp -> Cil.ikind -> t -> Invariant.t @@ -314,6 +315,7 @@ sig val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t val of_congruence: Cil.ikind -> int_t * int_t -> t val of_bitfield: Cil.ikind -> int_t * int_t -> t + val to_bitfield: Cil.ikind -> t -> int_t * int_t val starting : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t val ending : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t @@ -393,6 +395,7 @@ struct let of_interval ?(suppress_ovwarn=false) ikind (lb,ub) = {v = I.of_interval ~suppress_ovwarn ikind (lb,ub); ikind} let of_congruence ikind (c,m) = {v = I.of_congruence ikind (c,m); ikind} let of_bitfield ikind (z,o) = {v = I.of_bitfield ikind (z,o); ikind} + let to_bitfield ikind x = I.to_bitfield ikind x.v let starting ?(suppress_ovwarn=false) ikind i = {v = I.starting ~suppress_ovwarn ikind i; ikind} let ending ?(suppress_ovwarn=false) ikind i = {v = I.ending ~suppress_ovwarn ikind i; ikind} @@ -779,6 +782,45 @@ struct let one = Some IArith.one let top_bool = Some IArith.top_bool + let to_bitfield ik z = + match z with None -> (Ints_t.lognot Ints_t.zero, Ints_t.lognot Ints_t.zero) | Some (x,y) -> + let (min_ik, max_ik) = Size.range ik in + let startv = Ints_t.max x (Ints_t.of_bigint min_ik) in + let endv= Ints_t.min y (Ints_t.of_bigint max_ik) in + + let rec analyze_bits pos (acc_z, acc_o) = + if pos < 0 then (acc_z, acc_o) + else + let position = Ints_t.shift_left Ints_t.one pos in + let mask = Ints_t.sub position Ints_t.one in + let remainder = Ints_t.logand startv mask in + + let without_remainder = Ints_t.sub startv remainder in + let bigger_number = Ints_t.add without_remainder position in + + let bit_status = + if Ints_t.compare bigger_number endv <= 0 then + `top + else + if Ints_t.equal (Ints_t.logand (Ints_t.shift_right startv pos) Ints_t.one) Ints_t.one then + `one + else + `zero + in + + let new_acc = + match bit_status with + | `top -> (Ints_t.logor position acc_z, Ints_t.logor position acc_o) + | `one -> (Ints_t.logand (Ints_t.lognot position) acc_z, Ints_t.logor position acc_o) + | `zero -> (Ints_t.logor position acc_z, Ints_t.logand (Ints_t.lognot position) acc_o) + + in + analyze_bits (pos - 1) new_acc + in + let result = analyze_bits (Size.bit ik - 1) (Ints_t.zero, Ints_t.zero) in + let casted = (Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (fst result)))), Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (snd result))))) + in casted + let of_bool _ik = function true -> one | false -> zero let to_bool (a: t) = match a with | None -> None @@ -1379,7 +1421,20 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let casted = (Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (fst result)))), Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (snd result))))) in norm ~debug:true ~suppress_ovwarn ik casted - let of_congruence ik (c,m) = (if m = Ints_t.zero then fst (of_int ik c) else top_of ik) + let of_bitfield ik x = norm ik x |> fst + + let to_bitfield ik x = norm ik x |> fst + + let is_power_of_two x = (x &: (x -: Ints_t.one) = Ints_t.zero) + + let of_congruence ik (c,m) = + if m = Ints_t.zero then of_int ik c |> fst + else if is_power_of_two m then + let mod_mask = m -: Ints_t.one in + let z = !: c in + let o = !:mod_mask |: c in + norm ik (z,o) |> fst + else top_of ik let of_bool _ik = function true -> BArith.one | false -> BArith.zero @@ -1561,11 +1616,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int let (min_ik, max_ik) = Size.range ik in of_interval ~suppress_ovwarn ik (Ints_t.of_bigint min_ik, n) - let is_power_of_two x = (x &: (x -: Ints_t.one) = Ints_t.zero) - let refine_with_congruence ik bf ((cong) : (int_t * int_t ) option) : t = match bf, cong with - | (z,o), Some (c, m) when is_power_of_two m && m <> Ints_t.one -> + | (z,o), Some (c,m) when m = Ints_t.zero -> norm ik (!: c, c) |> fst + | (z,o), Some (c,m) when is_power_of_two m && m <> Ints_t.one -> let congruenceMask = !:m in let newz = (!:congruenceMask &: z) |: (congruenceMask &: !:c) in let newo = (!:congruenceMask &: o) |: (congruenceMask &: c) in @@ -1860,6 +1914,13 @@ struct else o in fst (norm_interval ik (min ik x, max ik x)) + let to_bitfield ik x = + let joinbf (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2) in + let rec from_list is acc = match is with + [] -> acc | + j::js -> from_list js (joinbf acc (Interval.to_bitfield ik (Some j))) + in from_list x (Ints_t.zero, Ints_t.zero) + let of_int ik (x: int_t) = of_interval ik (x, x) let lt ik x y = @@ -2720,6 +2781,10 @@ struct let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in norm ik @@ (`Excluded (ex, r)) + let to_bitfield ik x = + let one_mask = Z.lognot Z.zero + in (one_mask, one_mask) + let starting ?(suppress_ovwarn=false) ikind x = let _,u_ik = Size.range ikind in of_interval ~suppress_ovwarn ikind (x, u_ik) @@ -3209,6 +3274,10 @@ module Enums : S with type int_t = Z.t = struct let is_excl_list = BatOption.is_some % to_excl_list let to_incl_list = function Inc s when not (BISet.is_empty s) -> Some (BISet.elements s) | _ -> None + let to_bitfield ik x = + let one_mask = Z.lognot Z.zero + in (one_mask, one_mask) + let starting ?(suppress_ovwarn=false) ikind x = let _,u_ik = Size.range ikind in of_interval ~suppress_ovwarn ikind (x, u_ik) @@ -3469,6 +3538,17 @@ struct let of_congruence ik (c,m) = normalize ik @@ Some(c,m) + let to_bitfield ik x = + let is_power_of_two x = (Z.logand x (x -: Z.one) = Z.zero) in + match x with None -> (Z.zero, Z.zero) | Some (c,m) -> + if m = Z.zero then (Z.lognot c, c) + else if is_power_of_two m then + let mod_mask = m -: Z.one in + let z = Z.lognot c in + let o = Z.logor (Z.lognot mod_mask) c in + (z,o) + else (Z.lognot Z.zero, Z.lognot Z.zero) + let maximal t = match t with | Some (x, y) when y =: Z.zero -> Some x | _ -> None @@ -4101,6 +4181,12 @@ module IntDomTupleImpl = struct in mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_incl_list } x |> flat merge + let to_bitfield ik x = + let bf_meet (z1,o1) (z2,o2) = (Z.logand z1 z2, Z.logand o1 o2) in + let bf_top = (Z.lognot Z.zero, Z.lognot Z.zero) in + let res_tup = mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_bitfield ik } x + in List.fold bf_meet bf_top (to_list res_tup) + let same show x = let xs = to_list_some x in let us = List.unique xs in let n = List.length us in if n = 1 then Some (List.hd xs) else ( diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli index 55149cdb54..6c68724cc5 100644 --- a/src/cdomain/value/cdomains/intDomain.mli +++ b/src/cdomain/value/cdomains/intDomain.mli @@ -264,6 +264,7 @@ sig val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t val of_congruence: Cil.ikind -> int_t * int_t -> t val of_bitfield: Cil.ikind -> int_t * int_t -> t + val to_bitfield: Cil.ikind -> t -> int_t * int_t val is_top_of: Cil.ikind -> t -> bool val invariant_ikind : Cil.exp -> Cil.ikind -> t -> Invariant.t @@ -329,6 +330,7 @@ sig val of_congruence: Cil.ikind -> int_t * int_t -> t val of_bitfield: Cil.ikind -> int_t * int_t -> t + val to_bitfield: Cil.ikind -> t -> int_t * int_t val starting : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t val ending : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t diff --git a/tests/regression/82-bitfield/10-refine-interval.c b/tests/regression/82-bitfield/10-refine-interval.c index d49e9937de..d9441f05e9 100644 --- a/tests/regression/82-bitfield/10-refine-interval.c +++ b/tests/regression/82-bitfield/10-refine-interval.c @@ -15,5 +15,8 @@ int main() { __goblint_check(x == 63); // SUCCESS } + if ((x ^ 3) == 5) { + __goblint_check(x == 6); // SUCCESS + } } diff --git a/tests/regression/82-bitfield/11-refine-interval2.c b/tests/regression/82-bitfield/11-refine-interval2.c new file mode 100644 index 0000000000..4abaac9b89 --- /dev/null +++ b/tests/regression/82-bitfield/11-refine-interval2.c @@ -0,0 +1,17 @@ +// PARAM: --enable ana.int.interval --enable ana.int.bitfield --set ana.int.refinement fixpoint --trace inv --trace branch --trace invariant +#include + +int main() { + unsigned char r; // non-neg rand + char x = r % 64; + + if ((x | 0) == 63) { + __goblint_check(x == 63); // SUCCESS + } + + if ((x & 63) == 0) { + __goblint_check(x == 0); // SUCCESS + } + + +}