Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bitfield Domain #1623

Draft
wants to merge 156 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
156 commits
Select commit Hold shift + click to select a range
9b0002f
initial tests
ManuelLerchner Oct 23, 2024
582630c
implement first bad solution
ManuelLerchner Oct 23, 2024
3042aae
begin int domain rewrite to include bitfield
ManuelLerchner Oct 27, 2024
a609f3d
fix bitfield domain
ManuelLerchner Oct 29, 2024
696c110
Draft of incredibly messy impls of bitfield shift operations that nee…
iC4rl0s Nov 4, 2024
0630662
some bug fixes
Nov 4, 2024
fd89907
implemented add, sub and mul
Nov 4, 2024
8a91829
reverted some changes due to incorrect implementations
Nov 5, 2024
5c0fdbb
optimized shifts that concretize the shifting constants from an abstr…
iC4rl0s Nov 5, 2024
087d4a9
minor bug in max_shift
iC4rl0s Nov 5, 2024
0116023
comparison bug in max_shift
iC4rl0s Nov 5, 2024
03961c0
begin overflow handling
ManuelLerchner Nov 7, 2024
d42b989
separation of break_down into break_down_to_const_bitfields and break…
iC4rl0s Nov 7, 2024
6a26669
clean up; begin other methods
ManuelLerchner Nov 7, 2024
05b3d8e
format
ManuelLerchner Nov 8, 2024
27c9876
make it more functional. untested
iC4rl0s Nov 8, 2024
ca7c040
bug fix: Bitfields with z set to zero missed
iC4rl0s Nov 8, 2024
1338d65
Implementation of arithmetic operators (including neg) (#8)
AdrianKrauss Nov 12, 2024
447db3d
fix comments
ManuelLerchner Nov 12, 2024
3a00c0b
Merge branch 'master' into overflow-handling
ManuelLerchner Nov 12, 2024
89294a9
delete bitfield ml
ManuelLerchner Nov 12, 2024
c78510b
fix
ManuelLerchner Nov 12, 2024
ec166cb
Merge pull request #5 from ManuelLerchner/overflow-handling
ManuelLerchner Nov 12, 2024
1adccde
hotfix refinements
ManuelLerchner Nov 12, 2024
2e05197
.
Draggon01 Nov 12, 2024
897d6a2
bitfield shifts pr ready
iC4rl0s Nov 12, 2024
7d5913a
Merge branch 'master' into bitfield-shifts. Doesnt compile yet
ManuelLerchner Nov 12, 2024
257cc5b
added norm to almost every function which usess ikind
Nov 12, 2024
24b3719
added correct fil and deleted test file
Nov 12, 2024
cbfbf28
bug fix: signedness with right shift considered
iC4rl0s Nov 12, 2024
87b0189
Merge branch 'bitfield-shifts' of github.com:ManuelLerchner/analyzer …
iC4rl0s Nov 12, 2024
ff8c4c7
refine hotfix2
ManuelLerchner Nov 14, 2024
d405853
Revert "refine hotfix2"
ManuelLerchner Nov 14, 2024
ffc7285
refine hotfix2
ManuelLerchner Nov 14, 2024
5ec64ad
restore refine with congruence, as it was lost during merging
ManuelLerchner Nov 14, 2024
8cd7e62
Merge branch 'master' into 10-extend-norm-to-arithmetic-operations
ManuelLerchner Nov 14, 2024
a31dc67
intDomain.ml is compilable
iC4rl0s Nov 15, 2024
28d9db0
Avoiding unnecessary computation when min{b} > ceil(log2 max{a}) in s…
iC4rl0s Nov 16, 2024
6177b13
begin first unit tests
ManuelLerchner Nov 18, 2024
8e8b9cb
add simple shift unit tests
Draggon01 Nov 18, 2024
ed56bd8
Merge branch 'master' into bitfield-shifts
Draggon01 Nov 18, 2024
9ae2b8f
base test impl
Draggon01 Nov 19, 2024
874e1ed
merge unit tests
Draggon01 Nov 19, 2024
5ce8db7
add simple tests
Draggon01 Nov 19, 2024
4170f7f
fix small bug in constant shifting expecting isSigned ik to check if …
Draggon01 Nov 19, 2024
cd1bd06
Merge pull request #14 from ManuelLerchner/unit-tests
ManuelLerchner Nov 19, 2024
5eafd97
Merge pull request #12 from ManuelLerchner/bitfield-shifts
ManuelLerchner Nov 19, 2024
811590d
added bitfield to quickcheck
Nov 19, 2024
6999a20
two bug fixes
Nov 19, 2024
9f72163
Merge branch 'master' into 10-extend-norm-to-arithmetic-operations
ManuelLerchner Nov 19, 2024
c660277
Merge pull request #13 from ManuelLerchner/10-extend-norm-to-arithmet…
ManuelLerchner Nov 19, 2024
146d858
hotfix compilationn
ManuelLerchner Nov 19, 2024
55bc2b3
Merge branch 'master' into Add-tests
AdrianKrauss Nov 19, 2024
90e1e99
Merge pull request #15 from ManuelLerchner/Add-tests
ManuelLerchner Nov 19, 2024
6a32e42
hotfix compilation again
ManuelLerchner Nov 19, 2024
47b7a56
hotfix name clash after merge
ManuelLerchner Nov 19, 2024
5606e67
logand fix
ManuelLerchner Nov 19, 2024
8b1fbfc
bug fixes for arith ops
Nov 19, 2024
4bf31cc
fixed norm
Nov 19, 2024
0b4b4a1
is_invalid and mul fix
Nov 19, 2024
15520a8
assertion function for shifts
iC4rl0s Nov 19, 2024
d55eab5
bug fix in get_bit and further tests that lead to fails
iC4rl0s Nov 19, 2024
6562161
clean up
ManuelLerchner Nov 19, 2024
2aa27f8
fix compile warnings
ManuelLerchner Nov 19, 2024
ad5f6f8
format
ManuelLerchner Nov 19, 2024
cfa0091
improve arbitrary
ManuelLerchner Nov 19, 2024
98a2d24
Merge branch 'quickcheck-fixes' of github.com:ManuelLerchner/analyzer…
ManuelLerchner Nov 19, 2024
5914695
fix bug after merge
ManuelLerchner Nov 19, 2024
4a542be
Merge branch 'goblint:master' into master
ManuelLerchner Nov 19, 2024
15f7abe
changed narrow and added unit tests for arith ops
Nov 21, 2024
f9f7fce
add some regression tests
ManuelLerchner Nov 24, 2024
1b6459d
reworked bitfield shifts, infix operators and some simple tests. sign…
iC4rl0s Nov 25, 2024
31def4b
shift a b = zero when min{b} >= ceil(log (Size.bit ik))
iC4rl0s Nov 25, 2024
2ba8f38
negative shifts are undefined
iC4rl0s Nov 25, 2024
b6762af
bugfix: zero bits for lsb bitmask
iC4rl0s Nov 25, 2024
b6ee7fa
refactored min and max
Nov 25, 2024
a933c4e
Merge remote-tracking branch 'refs/remotes/origin/quickcheck-fixes' i…
Nov 26, 2024
e2366ff
added infix to all functions
Nov 26, 2024
addda52
extract tuple 6 from intDomain file
Draggon01 Nov 26, 2024
29bcca1
bugfix: shift_right did not shift right
iC4rl0s Nov 26, 2024
7984a0a
to_pretty_bits displays concrete values for a small enough number of …
iC4rl0s Nov 26, 2024
ed1999a
small QoL improvements and bug fixes
iC4rl0s Nov 26, 2024
7fa0100
bugfix: certain zeros and uncertain ones
iC4rl0s Nov 26, 2024
96e5737
add regression test for refinement
ManuelLerchner Nov 27, 2024
90338a7
add more regression tests for refines
ManuelLerchner Nov 27, 2024
f25a578
improve refine with interval; add regression tests
ManuelLerchner Nov 28, 2024
e9286e7
fixed bitshifts
Draggon01 Dec 3, 2024
3e4928a
removed commmented code and old wrong testcases
Draggon01 Dec 3, 2024
9bcd884
fixed edge case where shift with 0 was done without zero in shifting bf
Draggon01 Dec 3, 2024
6fe1162
added of bitfield for refinements
Dec 3, 2024
5301322
Merge pull request #18 from ManuelLerchner/quickcheck-fixes
ManuelLerchner Dec 3, 2024
0fa8ca7
Merge branch 'master' of github.com:ManuelLerchner/analyzer into more…
ManuelLerchner Dec 3, 2024
bad0bb8
remove duplicate function
ManuelLerchner Dec 3, 2024
abde7e4
Revert "remove duplicate function"
ManuelLerchner Dec 3, 2024
937b341
Reapply "remove duplicate function"
ManuelLerchner Dec 3, 2024
ddfaace
fix bug
ManuelLerchner Dec 3, 2024
24f305f
add some more tests
ManuelLerchner Dec 4, 2024
7c4411d
add missing regression tests
ManuelLerchner Dec 4, 2024
6c2c570
simple refinements for base invariant with bitfields
Dec 7, 2024
f237a9e
shift_right and shift_left return bot when the result or the paramete…
iC4rl0s Dec 9, 2024
e4eefd9
added to_bitfield to refine base invariant further and regression test
Dec 9, 2024
8d4a4b8
Merge pull request #19 from ManuelLerchner/more-regression-tests
ManuelLerchner Dec 10, 2024
8d7faf9
Merge pull request #20 from ManuelLerchner/extract-tuple-six
ManuelLerchner Dec 10, 2024
e2568fd
Merge branch 'master' of github.com:ManuelLerchner/analyzer into inva…
ManuelLerchner Dec 10, 2024
ccb13c1
Merge pull request #21 from ManuelLerchner/invariant
ManuelLerchner Dec 10, 2024
88b0dfc
hotfix regression tests
ManuelLerchner Dec 10, 2024
86fdeb5
Merge branch 'goblint:master' into master
ManuelLerchner Dec 10, 2024
60fbbf5
improved property tests for bitshifts
iC4rl0s Dec 11, 2024
ed27d3d
fix show
ManuelLerchner Dec 11, 2024
58eeeb4
Merge branch 'master' of github.com:ManuelLerchner/analyzer
ManuelLerchner Dec 11, 2024
dbe2e00
some property tests failed as generators were not constrained to the ik
iC4rl0s Dec 11, 2024
810a966
fixed overflow in norm
Dec 11, 2024
d7b8755
renaming due to merge conflict
Dec 11, 2024
541a87d
Merge branch 'master' into overflow
AdrianKrauss Dec 11, 2024
686633a
two bug fixes
Dec 11, 2024
4b3a0f8
improved logging
iC4rl0s Dec 11, 2024
dee9036
overflow behavior cannot be checked by property tests
iC4rl0s Dec 11, 2024
d6e3f61
more robust tests with a found bug
iC4rl0s Dec 11, 2024
e3145ad
revert to basic unit tests
iC4rl0s Dec 11, 2024
6c720b8
Merge remote-tracking branch 'origin/overflow' into tests
iC4rl0s Dec 11, 2024
f09ead4
bug in exclude_undefined_bitshifts must be fixed or behavior defined
iC4rl0s Dec 12, 2024
8b53b08
Added distinction between invalid and undefined bitshifts. In the for…
iC4rl0s Dec 12, 2024
c682527
added pape rreferences and refined div
Dec 13, 2024
7a8b3ad
added some more cases
Draggon01 Dec 15, 2024
8cf7192
more tests and overflow bugs detected. comment out TODO fails to see
iC4rl0s Dec 16, 2024
79a859a
bugfix: zero shifted by anything should be zero
iC4rl0s Dec 16, 2024
bfe5dc6
Merge branch 'master' of github.com:goblint/analyzer into goblint-master
ManuelLerchner Dec 16, 2024
ed56056
Merge branch 'goblint-master'
ManuelLerchner Dec 16, 2024
f40fefb
refactored intDomain
Dec 17, 2024
e1d948d
Merge branch 'master' into tests
AdrianKrauss Dec 17, 2024
57ac94a
merge
Draggon01 Dec 17, 2024
6c7f899
exclude bitfield in modules python script as other intdomains
Draggon01 Dec 17, 2024
313adb8
changed to top_of
Dec 17, 2024
ee9f358
merge
Dec 17, 2024
288bf0d
Merge remote-tracking branch 'refs/remotes/origin/tests' into tests
Dec 17, 2024
306aa33
improved refinements with bitfield
Dec 17, 2024
3862f2e
added overflow checking
Draggon01 Dec 17, 2024
b683875
added missing bf in create
Draggon01 Dec 17, 2024
26a23f5
bugfixes for overflow errs
iC4rl0s Dec 17, 2024
f70838d
Merge branch 'tests' of github.com:ManuelLerchner/analyzer into tests
iC4rl0s Dec 17, 2024
2e85cc9
Merge pull request #22 from ManuelLerchner/tests
iC4rl0s Dec 17, 2024
898a68e
fixed all current ocp-indent failures
Draggon01 Dec 18, 2024
0cc16dc
added regression test
Draggon01 Dec 19, 2024
65237fd
fixed overflow handling
Dec 19, 2024
5cf4620
Merge pull request #26 from ManuelLerchner/precission
ManuelLerchner Dec 20, 2024
dc68f48
Merge pull request #25 from ManuelLerchner/indent-fixes
ManuelLerchner Dec 20, 2024
312b0c3
added adapted functions from interval domain to base
Jan 4, 2025
3034ad3
fixed bug in refine with congruence
Jan 6, 2025
1f08a87
fixed Div by zero exception
Jan 7, 2025
552c333
fixed overflow in bitshift
Jan 7, 2025
571cde3
removed test files
Jan 7, 2025
18ee9a9
removed unnecessary file
Jan 7, 2025
51c13e7
Merge branch 'goblint:master' into master
ManuelLerchner Jan 7, 2025
e7c3237
Merge branch 'master' into fixingBase
ManuelLerchner Jan 7, 2025
1376824
Merge pull request #27 from ManuelLerchner/fixingBase
ManuelLerchner Jan 7, 2025
abb48c4
canonize interval-sets after refine with bitfield
ManuelLerchner Jan 8, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
simple refinements for base invariant with bitfields
  • Loading branch information
Adrian Krauß committed Dec 7, 2024
commit 6c2c5708a9059790bcffa31e57dfcce2d6edeae7
32 changes: 13 additions & 19 deletions src/analyses/baseInvariant.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
166 changes: 100 additions & 66 deletions src/cdomain/value/cdomains/intDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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)

Expand Down Expand Up @@ -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";
Fixed Show fixed Hide fixed
Fixed Show fixed Hide fixed
Fixed Show fixed Hide fixed
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";
Fixed Show fixed Hide fixed
Fixed Show fixed Hide fixed
Fixed Show fixed Hide fixed
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 *)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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";
Fixed Show fixed Hide fixed
Fixed Show fixed Hide fixed
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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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? *)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/cdomain/value/cdomains/intDomain.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
19 changes: 19 additions & 0 deletions tests/regression/82-bitfield/10-refine-interval.c
Original file line number Diff line number Diff line change
@@ -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 <goblint.h>

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
}


}