Improve int domain bitwise operators, support struct bitfields #1739
Conversation
sim642
added
feature
student-job
sv-comp
| let logor ik x y = norm ik (match x,y with | ||
| | `Excluded (_, r), `Definite i | ||
| | `Definite i, `Excluded (_, r) -> | ||
| if Z.compare i Z.zero >= 0 then | ||
| `Excluded (S.empty (), R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i))) | ||
| else | ||
| (match R.minimal r, R.maximal r with | ||
| | None, _ | _, None -> top_of ik | ||
| | Some r1, Some r2 -> let b = Int.max (Z.numbits i) (Int64.to_int(Int64.max (Int64.abs r1) (Int64.abs r2))) in | ||
| `Excluded (S.empty (), R.of_interval range_ikind (Int64.of_int @@ -b, Int64.of_int b)) | ||
| ) | ||
| | `Excluded (_, r1), `Excluded (_, r2) -> `Excluded (S.empty (), R.join r1 r2) | ||
| | `Definite x, `Definite y -> | ||
| (try `Definite (Z.logor x y) with | Division_by_zero -> top_of ik) | ||
| | `Bot, `Bot -> `Bot | ||
| | _ -> | ||
| (* If only one of them is bottom, we raise an exception that eval_rv will catch *) | ||
| raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))) | ||
|
|
||
| let logor = lift2 Z.logor | ||
| let logxor = lift2 Z.logxor | ||
| let logxor ik x y = norm ik (match x,y with | ||
| | `Definite i, `Excluded (_, r) | ||
| | `Excluded (_, r), `Definite i -> begin | ||
| if Z.compare i Z.zero >= 0 then | ||
| `Excluded (S.empty (), R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i))) | ||
| else | ||
| match R.minimal r, R.maximal r with | ||
| | None, _ | _, None -> top_of ik | ||
| | Some r1, Some r2 -> let b = Int.max (Z.numbits i) (Int64.to_int(Int64.max (Int64.abs r1) (Int64.abs r2))) in | ||
| `Excluded (S.empty (), R.of_interval range_ikind (Int64.of_int @@ -b, Int64.of_int b)) | ||
| end | ||
| | `Excluded (_, r1), `Excluded (_, r2) -> `Excluded (S.empty (), R.join r1 r2) | ||
| (* The good case: *) | ||
| | `Definite x, `Definite y -> | ||
| (try `Definite (Z.logxor x y) with | Division_by_zero -> top_of ik) | ||
| | `Bot, `Bot -> `Bot | ||
| | _ -> | ||
| (* If only one of them is bottom, we raise an exception that eval_rv will catch *) | ||
| raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))) |
There was a problem hiding this comment.
This looks a little like copy pasta 🍝
| let logand ikind u v = | ||
| handle_bot u v (fun () -> | ||
| norm ikind @@ match u, v with | ||
| | Inc x,Inc y when BISet.is_singleton x && BISet.is_singleton y -> Inc (BISet.singleton (Z.logand (BISet.choose x) (BISet.choose y))) | ||
| | Inc x, Exc (s,r) | ||
| | Exc (s,r), Inc x -> | ||
| let f = fun i -> | ||
| if Z.compare i Z.zero >= 0 then | ||
| R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i)) | ||
| else | ||
| (match R.minimal r, R.maximal r with | ||
| | None, _ | _, None -> R.top () | ||
| | Some r1, Some r2 -> let b = Int.max (Z.numbits i) (Int64.to_int(Int64.max (Int64.abs r1) (Int64.abs r2))) in | ||
| R.of_interval range_ikind (Int64.of_int @@ -b, Int64.of_int b) | ||
| ) in | ||
| let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in | ||
| Exc (BISet.empty (), r') | ||
| | Exc (_, r1), Exc (_, r2) -> Exc (BISet.empty (), R.meet r1 r2) | ||
| | _,_ -> top_of ikind) | ||
|
|
||
| let logor ikind u v = handle_bot u v (fun () -> | ||
| norm ikind @@ match u, v with | ||
| | Inc x,Inc y when BISet.is_singleton x && BISet.is_singleton y -> Inc (BISet.singleton (Z.logor (BISet.choose x) (BISet.choose y))) | ||
| | Inc x, Exc (_,r) | ||
| | Exc (_,r), Inc x -> | ||
| let f = fun i -> | ||
| if Z.compare i Z.zero >= 0 then | ||
| R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i)) | ||
| else | ||
| (match R.minimal r, R.maximal r with | ||
| | None, _ | _, None -> R.top () | ||
| | Some r1, Some r2 -> let b = Int.max (Z.numbits i) (Int64.to_int(Int64.max (Int64.abs r1) (Int64.abs r2))) in | ||
| R.of_interval range_ikind (Int64.of_int @@ -b, Int64.of_int b) | ||
| ) in | ||
| let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in | ||
| Exc (BISet.empty (), r') | ||
| | Exc (_, r1), Exc (_, r2) -> Exc (BISet.empty (), R.join r1 r2) | ||
| | _ -> top_of ikind) | ||
|
|
||
| let logxor ikind u v = handle_bot u v (fun () -> | ||
| norm ikind @@ match u, v with | ||
| | Inc x,Inc y when BISet.is_singleton x && BISet.is_singleton y -> Inc (BISet.singleton (Z.logxor (BISet.choose x) (BISet.choose y))) | ||
| | Inc x, Exc (_,r) | ||
| | Exc (_,r), Inc x -> | ||
| let f = fun i -> | ||
| if Z.compare i Z.zero >= 0 then | ||
| R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i)) | ||
| else | ||
| match R.minimal r, R.maximal r with | ||
| | None, _ | _, None -> R.top () | ||
| | Some r1, Some r2 -> let b = Int.max (Z.numbits i) (Int64.to_int(Int64.max (Int64.abs r1) (Int64.abs r2))) in | ||
| R.of_interval range_ikind (Int64.of_int @@ -b, Int64.of_int b) | ||
| in | ||
| let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in | ||
| Exc (BISet.empty (), r') | ||
| | Exc (_, r1), Exc (_, r2) -> Exc (BISet.empty (), R.join r1 r2) | ||
| | _ -> top_of ikind) |
There was a problem hiding this comment.
These three functions look very similar?
sim642
changed the title
|
There seems to be a bug: the regression test 83/07 refine-with-interval crashes. It looks like I also did a 60s sv-benchmarks run, which revealed 10 unsound unreach-call results:
|
sim642
force-pushed
the
bit-operation-additions
branch
from
27d26c4 to
fc50485
Compare
…analyzer-thesis into bit-operation-additions
|
I did a new 60s sv-benchmarks run with the latest fixes. All of the unsoundness is now fixed! |
|
I saw the commit message
and got curious. What exactly are you proving here and how are you going about it? Are these manual proofs or some sort of mechanized approach? If yes, can we use it for our other domains too? |
Since the thesis will be in Estonian, I can't say "wait a week". Various cases of each bitwise operation are formulated as Z3 (instead of OCaml code) queries over the bitvector SMT theory by bitblasting or whatever Z3 decides to do. One probably could do this more widely, but the manual re-encoding is still error prone, so the guarantees aren't super strong. Nevertheless, I'm wondering if we should have these Z3 proof scripts added into this repository for the sake of it? |
|
Interesting!
Not sure if we want to add it to the repo as it may go out of sync, but I'm definitely curious what they look like! |
All the proofs are in this repo: https://github.com/H-Innos/Z3 |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| if Ints_t.equal n Ints_t.zero then | ||
| Ints_t.neg Ints_t.one | ||
| else | ||
| Ints_t.neg @@ Ints_t.shift_left Ints_t.one (Z.numbits (Z.sub (Z.abs @@ Ints_t.to_bigint n) Z.one)) |
Check warning
Code scanning / Semgrep OSS
Semgrep Finding: semgrep.z-sub-one Warning
| if Ints_t.equal n Ints_t.zero then | ||
| Ints_t.neg Ints_t.one | ||
| else | ||
| Ints_t.neg @@ Ints_t.shift_left Ints_t.one (Z.numbits (Z.sub (Z.abs @@ Ints_t.to_bigint n) Z.one)) |
Check warning
Code scanning / Semgrep OSS
Semgrep Finding: semgrep.z-sub-one Warning
Additions for my BSc thesis "Improving Bitwise Operation Analysis in Goblint", supervised by Simmo Saan. This includes making the logand, logor, logxor, lognot, and shift_right abstractions more precise in the interval, interval sets, defexc, and enums domains. Additionally, I added support for the analysis of bit-fields.