Bitfield Domain #1623

ManuelLerchner · 2024-11-05T15:53:46Z

This pull request enhances the IntDomain by introducing a new BitfieldDomain capable of tracking bitwise operations.
Additionally, it adds all newly possible refinement directions to improve precision in the IntDomain.

This implementation is part of the Automated Bug Hunting and Beyond practical course at TUM.

…d some revision. Possible side-effects and runtime in O(n^2) while O(n) should be possible.

github-advanced-security

Semgrep OSS found more than 20 potential problems in the proposed changes. Check the Files changed tab for more details.

…act bitfield by eliminating constants that would result in a shift to zero beforehand

…_down_to_consts

* implemented modulo * current changes * implementation of add, sub, mul based on paper * implemented neg * bug fixes for arith operators --------- Co-authored-by: Adrian Krauß <[email protected]>

Overflow and wrapping

Bugfixes from benchmarking

…gfixes

michael-schwarz · 2025-01-22T09:24:22Z

src/analyses/baseInvariant.ml

+          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


Should most of these computations not be moved inside your domain? (After getting the bitfields).

This works on the internal representation of these bitfield things, so maybe should be in there. Granted, the intervals also leak outside of their domain,but people intuitively understand how they work.

Also, please leave some comment here about what happens. One can puzzle it together, but it took @DrMichaelPetter and me about 10 mins yesterday to do so.

michael-schwarz · 2025-01-22T09:25:10Z

src/analyses/baseInvariant.ml

+             | None -> a)
+          | _ -> a


The tracing output should still be produced if bitfield is off.

michael-schwarz · 2025-01-22T09:26:09Z

src/analyses/baseInvariant.ml

+          let a' = ID.meet a (ID.logxor c b)
+          in let b' = ID.meet b (ID.logxor a c)          


Please change to use standard indentation.

let ... = ... in

michael-schwarz · 2025-01-22T09:26:27Z

src/analyses/baseInvariant.ml

+        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


Same as above.

michael-schwarz · 2025-01-22T09:29:49Z

src/cdomain/value/cdomains/int/congruenceDomain.ml

+    match x with None -> (Z.zero, Z.zero) | Some (c,m) ->
+      if m = Z.zero then (Z.lognot c, c)


Please indent as done in other places in Goblint.

michael-schwarz · 2025-01-22T09:32:10Z

src/cdomain/value/cdomains/int/congruenceDomain.ml

+      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)


Does one need to consider the signedness here?

I'm unsure whether you mean the signedess of c and m or of the returned bitfield. But in both cases, we do not have to consider it explicitly. normalize always returns positive values for c and m if m is unequal to zero. Additionally, a possible sign bit is set to top in the returned bitfield representation.

michael-schwarz · 2025-01-22T09:34:14Z

src/cdomain/value/cdomains/int/congruenceDomain.ml

+  let refine_with_bitfield ik a (z,o) = 
+    if Z.lognot z = o then meet ik a (Some (o, Z.zero))
+    else a


Is this the only case where we can benefit? Naively, one thinks we should be able to benefit along the reasoning of the to_bitfield above?

We benefit along the reasoning of the to_bitfield in the refine_with_congruence of the bitfield domain because we transform a value from the congruence into the bitfield domain. Unfortunately, I don't see how we can use similar tricks for the converse direction.

Naively I would think that knowing that the last k bits are must-zero would give rise to a
congruence of the type z mod 2^(k) = 0, at least in the case where we also know that the values are positive (because of the ik, or because the MSB is not set)?
But maybe that's wrong?

michael-schwarz · 2025-01-22T09:35:02Z

src/cdomain/value/cdomains/int/defExcDomain.ml

+  let to_bitfield ik x = 
+    match x with 
+      `Definite c -> (Z.lognot c, c) |
+      _ -> let one_mask = Z.lognot Z.zero 
+      in (one_mask, one_mask)


Indentation

michael-schwarz · 2025-01-22T09:36:01Z

src/cdomain/value/cdomains/int/defExcDomain.ml

+  let refine_with_bitfield ik x (z,o) = 
+    if Z.lognot z = o then meet ik x (`Definite o)
+    else x


Do you not need to consider the ik here?

michael-schwarz · 2025-01-22T09:37:01Z

src/cdomain/value/cdomains/int/enumsDomain.ml

+  let to_bitfield ik x = 
+    match x with 
+      Inc i when BISet.is_empty i -> (Z.zero, Z.zero) |
+      Inc i when BISet.is_singleton i -> 
+      let o = BISet.choose i 
+      in (Z.lognot o, o) |
+      Inc i -> BISet.fold (fun o (az, ao) -> (Z.logor (Z.lognot o) az, Z.logor o ao)) i (Z.zero, Z.zero) |
+      _ -> let one_mask = Z.lognot Z.zero     
+      in (one_mask, one_mask)
+


With this indentation it is near impossible to review!

michael-schwarz · 2025-01-22T09:38:18Z

src/cdomain/value/cdomains/int/intervalDomain.ml

@@ -1,4 +1,5 @@
 open IntDomain0
+open GoblintCil


Where are you using this? If it's only very few places, one may not want to open it.

We use it for the isSigned function of ikinds.

Ok, since it's only used three times (and only in one function), I think i would personally prefer getting rid of the open and qualifying those references with GoblintCil.isSigned or using a local open in that function.

michael-schwarz · 2025-01-22T09:40:16Z

src/cdomain/value/cdomains/int/intervalSetDomain.ml

+    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)


Is this not just a fold?

michael-schwarz · 2025-01-22T09:44:15Z

src/cdomain/value/cdomains/int/intervalDomain.ml

+              `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


where do these polymorphic variants now come from?

michael-schwarz · 2025-01-22T09:46:24Z

src/cdomain/value/util/precisionUtil.ml

+  annotation_int_enabled := None;
+  bitfield := None


Please swap

michael-schwarz · 2025-01-22T09:47:55Z

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


Why verbose?

I'm curious if you've actually used this and found anything with this. Domain tests for individual integer domains are part of unit tests where they are directly triggered. This attempts to test the full domain used by the configured analysis, but I suspect this doesn't have arbitrary-s defined all the way down to the integer domains through all the functors. For that reason I've even considered removing this feature altogether, but if it has actually been useful then let me know.

michael-schwarz · 2025-01-22T09:49:43Z

tests/regression/82-bitfield/00-simple-demo.c

@@ -0,0 +1,29 @@
+// PARAM: --enable ana.int.bitfield


In general it seems very few of your pograms tests actually test the join of your domain. That would be something that probably should be added.

michael-schwarz · 2025-01-22T09:53:20Z

src/cdomain/value/cdomains/int/intDomTuple.ml

+    | (_, _, _, _, _, Some true) 
+      -> true 


Please stick with the normal indentation.

michael-schwarz · 2025-01-22T09:56:35Z

src/cdomain/value/cdomains/int/bitfieldDomain.ml

+  let rec concretize (z,o) = (* O(2^n) *)
+    if is_const (z,o) then [o]
+    else
+      let bit = o &: Ints_t.one in
+      let bf_bit = nth_bf_bit (z,o) 0 in
+      concretize (z >>. 1, o >>: 1) |>
+      if bf_bit = `Undetermined then
+        List.concat_map (fun c -> [c <<: 1; (c <<: 1) |: Ints_t.one])
+      else if bf_bit = `Invalid then
+        failwith "Should not have happened: Invalid bit during concretization of a bitfield."
+      else
+        List.map (fun c -> c <<: 1 |: bit)
+
+  let concretize bf = List.map Ints_t.to_int (concretize bf)


Where is this used?

The 'concretize' method is used inside the shift operations (shift_left, shift_right) as it returns the values which needs to be shifted.

Fully concretizing an abstract value is not something that should be done lightly, as you have noted yourself. If you do a shift and know nothing about the operand (which can happen), this operation alone will completely kill the chance of ever terminating, already from constructing this list of length 2^64.

Does your domain not have an efficient way of computing $$| \gamma (x) |$$ by counting the number n of zero bits in z xor x (size 2^n)? In this case, you should only do something for small n (maybe up to 3) to stay tractable.

Ah, I see you actually bound the argument in all calls with the bitwidth, so it is not too problematic. Probably you should make a comment here as well then that the function is not a reasonable shift function for any arguments, but only for second arguments with small(!) concretizations.

Sure that makes sense, I will add comments that make this more obvious.

michael-schwarz · 2025-01-22T10:12:28Z

src/cdomain/value/cdomains/int/bitfieldDomain.ml

+  let bot () = (BArith.zero_mask, BArith.zero_mask)
+
+  let top_of ik = 
+    if isSigned ik then top () 


I don't think i understand how you handle ikinds in general here.

Do you norm the upper bits?

If not do you not risk having values that are semantically equal but syntactically not?

What happens for ikinds that are wider than the BArith.one_mask?

Why can this not work for signed types? And does this not mean you find out nothing as soon as any computations happen in the program (even for unsigned types)?

C99 6.3.1.

If an int can represent all values of the original type, the value is converted to an int; otherwise, it is converted to an unsigned int. These are called the integer
promotions. All other types are unchanged by the integer promotions.

michael-schwarz · 2025-01-22T10:32:49Z

src/cdomain/value/cdomains/int/bitfieldDomain.ml

+    let o_mask = ref o in
+    let z_mask = ref z in


It was not necessary to use references in this case, therefore the code was changed and the ref removed.

michael-schwarz · 2025-01-22T10:35:07Z

src/cdomain/value/cdomains/int/bitfieldDomain.ml

+  let range ik bf = (BArith.min ik bf, BArith.max ik bf)
+
+  let maximal (z,o) =     
+    if (z < Ints_t.zero) <> (o < Ints_t.zero) then Some o


Can you explain this?

We basically check whether the sign bit is clear, i.e., whether we only represent positive or negative numbers. Under such a condition, the maximal represented number is just the number with the maximal number of ones.

Hmm, that works if the ikind and the type of Ints_t coincide. But what if you have, e.g., the ikind of signed char? There you would need to check the 7th bit right?

I wasn't there for the first couple of meetings, so maybe you'll need to enlighten us tomorrow how you deal with different ikinds in your domain in general 😃

michael-schwarz

Thanks for the PR! I left some first comments in some places, but have not worked through the entire thing.

bug fix in to_bitfield()

jerhard

Thank you for the PR! I left some comments below.

jerhard · 2025-01-23T03:14:10Z

src/cdomain/value/cdomains/int/intervalDomain.ml

+  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


Can you make this function easier to read?
A comment about what is done here overall may help. Possibly one may also find a more telling name for the helper function analyze_bits?

jerhard · 2025-01-23T03:16:25Z

src/cdomain/value/cdomains/int/intervalSetDomain.ml

+      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) =


Indentation.

jerhard · 2025-01-23T03:18:09Z

src/cdomain/value/cdomains/int/intervalSetDomain.ml

+      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


signBit and signMask only seem to depend on ik. Can one extract them from min and max, so they don't have to be defined twice?

jerhard · 2025-01-23T03:21:23Z

tests/unit/cdomains/intDomainTest.ml

+        assert_shift_right ~rev_cond:true ik (`I [max_of ik]) top top; (* the sign bit shouldn't be set with right shifts if its unset *)
+
+        assert_shift_right ik (`I [2]) (`I [-1]) top; (* Negative shifts are undefined behavior *)
+        (*assert_shift_right ik (`I [min_of ik]) top top;*) (*TODO implementation-defined sign-bit handling *)


What is this todo about?

This test case could be removed if you agree with our design choice to handle right shifts as arithmetic ones.
Given the C standard's definition of right shifts on signed integers, it might be better to leave the upper bits undetermined. In that case this test case should pass.

jerhard · 2025-01-23T03:26:27Z

src/cdomain/value/cdomains/int/bitfieldDomain.ml

+    | true, true -> `Undetermined
+    | false, false -> `Invalid
+    | true, false -> `Zero
+    | false, true -> `One


Is there a specific reason you are using polymorphic variants? If not, it would be preferable to define a variant type. See also here.

No, they were naively chosen to be used for readability purposes here but not necessary in any way. This part will be removed.

jerhard · 2025-01-23T03:33:11Z

src/cdomain/value/cdomains/int/bitfieldDomain.ml

+    else None
+
+  let minimal (z,o) =     
+    if (z < Ints_t.zero) <> (o < Ints_t.zero) then Some (!:z)


Using the polymorphic compare < here probably works, but the compare on Ints_t is probably still the better choice?

jerhard · 2025-01-23T03:34:18Z

src/cdomain/value/cdomains/int/bitfieldDomain.ml

+        (* (M.warn ~category:M.Category.Integer.overflow "Bitfield: Value was outside of range, indicating overflow, but 'sem.int.signed_overflow' is 'assume_none' -> Returned Top"; *)
+        (* (bot (), overflow_info)) *)


Commented out code should be removed in the final version.

jerhard · 2025-01-23T03:37:02Z

src/cdomain/value/cdomains/int/bitfieldDomain.ml

+
+  (* Conversions *)
+
+  let of_interval ?(suppress_ovwarn=false) ik (x,y) =


Does this function share code with the to_bitfield function in the interval domain? If so, could this be deduplicated?

jerhard · 2025-01-23T03:39:43Z

src/cdomain/value/cdomains/int/bitfieldDomain.ml

+          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


Here, one could also define a variant type, instead of using a polymorphic variant type.

jerhard · 2025-01-23T03:41:48Z

src/cdomain/value/cdomains/int/bitfieldDomain.ml

+  (* Unit Tests *)
+
+  let arbitrary ik = 


arbitrary is used for unit tests, indeed; still the comment may be a bit misleading, since there are no unit tests following the comment.

ManuelLerchner and others added 8 commits October 23, 2024 15:11

initial tests

9b0002f

implement first bad solution

582630c

begin int domain rewrite to include bitfield

3042aae

fix bitfield domain

a609f3d

Draft of incredibly messy impls of bitfield shift operations that nee…

696c110

…d some revision. Possible side-effects and runtime in O(n^2) while O(n) should be possible.

some bug fixes

0630662

implemented add, sub and mul

fd89907

reverted some changes due to incorrect implementations

8a91829

michael-schwarz added student-job feature labels Nov 5, 2024

github-advanced-security bot found potential problems Nov 5, 2024

View reviewed changes

iC4rl0s added 3 commits November 5, 2024 22:17

optimized shifts that concretize the shifting constants from an abstr…

5c0fdbb

…act bitfield by eliminating constants that would result in a shift to zero beforehand

minor bug in max_shift

087d4a9

comparison bug in max_shift

0116023

sim642 added in progress precision practical-course Practical Course at TUM labels Nov 6, 2024

ManuelLerchner and others added 13 commits November 7, 2024 04:43

begin overflow handling

03961c0

separation of break_down into break_down_to_const_bitfields and break…

d42b989

…_down_to_consts

clean up; begin other methods

6a26669

format

05b3d8e

make it more functional. untested

27c9876

bug fix: Bitfields with z set to zero missed

ca7c040

Implementation of arithmetic operators (including neg) (#8)

1338d65

* implemented modulo * current changes * implementation of add, sub, mul based on paper * implemented neg * bug fixes for arith operators --------- Co-authored-by: Adrian Krauß <[email protected]>

fix comments

447db3d

Merge branch 'master' into overflow-handling

3a00c0b

delete bitfield ml

89294a9

fix

c78510b

Merge pull request #5 from ManuelLerchner/overflow-handling

ec166cb

Overflow and wrapping

hotfix refinements

1adccde

ManuelLerchner added 2 commits January 18, 2025 16:58

Merge pull request #28 from ManuelLerchner/bugfixes

1d78b29

Bugfixes from benchmarking

Merge branch 'goblint:master' into master

4fe0097

ManuelLerchner marked this pull request as ready for review January 20, 2025 17:32

Adrian Krauß and others added 3 commits January 21, 2025 15:46

bug fix in to_bitfield()

767f998

bugfix: underflow handling

821be43

Merge branch 'bugfixes' of github.com:ManuelLerchner/analyzer into bu…

a1807b6

…gfixes

michael-schwarz reviewed Jan 22, 2025

View reviewed changes

Merge pull request #29 from ManuelLerchner/bugfixes

0a55d08

bug fix in to_bitfield()

jerhard reviewed Jan 23, 2025

View reviewed changes

		let a' = ID.meet a (ID.logxor c b)
		in let b' = ID.meet b (ID.logxor a c)

		match x with None -> (Z.zero, Z.zero) \| Some (c,m) ->
		if m = Z.zero then (Z.lognot c, c)

		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

		(* (M.warn ~category:M.Category.Integer.overflow "Bitfield: Value was outside of range, indicating overflow, but 'sem.int.signed_overflow' is 'assume_none' -> Returned Top"; *)
		(* (bot (), overflow_info)) *)


		(* Conversions *)

		let of_interval ?(suppress_ovwarn=false) ik (x,y) =

Bitfield Domain #1623

Are you sure you want to change the base?

Bitfield Domain #1623

Conversation

ManuelLerchner commented Nov 5, 2024 • edited Loading

github-advanced-security bot left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

michael-schwarz left a comment

Choose a reason for hiding this comment

jerhard left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jerhard Jan 23, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jerhard Jan 23, 2025 • edited Loading

Choose a reason for hiding this comment

ManuelLerchner commented Nov 5, 2024 •

edited

Loading

jerhard Jan 23, 2025 •

edited

Loading

jerhard Jan 23, 2025 •

edited

Loading