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 108 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
108 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
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
ed27d3d
fix show
ManuelLerchner Dec 11, 2024
58eeeb4
Merge branch 'master' of github.com:ManuelLerchner/analyzer
ManuelLerchner Dec 11, 2024
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
Revert "remove duplicate function"
This reverts commit bad0bb8.
ManuelLerchner committed Dec 3, 2024
commit abde7e41b0174dd8ef12ca9ea2b4642c9a4710fd
3 changes: 2 additions & 1 deletion src/cdomain/value/cdomains/intDomain.ml
Original file line number Diff line number Diff line change
@@ -1500,7 +1500,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
let res = if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then (let tmp = z1 /: z2 in (!:tmp, tmp)) else top_of ik in
norm ik res

let is_power_of_two x = (x &: (x -: Ints_t.one) = Ints_t.zero)
let is_power_of_two x = Ints_t.(logand x (sub x one) = zero)

let rem ik x y =
if BArith.is_const x && BArith.is_const y then (
@@ -1556,6 +1556,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
of_interval ~suppress_ovwarn ik (Ints_t.of_bigint min_ik, n)

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 && m <> Ints_t.one ->
let congruenceMask = !:m in