Code

Bitfield Domain#1623

Code

Draft

ManuelLerchner wants to merge 156 commits intogoblint:mastergoblint/analyzer:masterfrom ManuelLerchner:masterManuelLerchner/analyzer:masterCopy head branch name to clipboard

+2,152-87

Commits

Commits on Oct 23, 2024

• initial tests

  ManuelLerchner

  committed
  9b0002f

• implement first bad solution

  ManuelLerchner

  committed
  582630c

Commits on Oct 27, 2024

• begin int domain rewrite to include bitfield

  ManuelLerchner

  committed
  3042aae

Commits on Oct 29, 2024

• fix bitfield domain

  ManuelLerchner

  committed
  a609f3d

Commits on Nov 4, 2024

• Draft of incredibly messy impls of bitfield shift operations that need some revision. Possible side-effects and runtime in O(n^2) while O(n) should be possible.

  iC4rl0s

  committed
  696c110

• some bug fixes

  

  Adrian Krauß

  committed
  0630662

• implemented add, sub and mul

  

  Adrian Krauß

  committed
  fd89907

Commits on Nov 5, 2024

• reverted some changes due to incorrect implementations

  

  Adrian Krauß

  committed
  8a91829

• optimized shifts that concretize the shifting constants from an abstract bitfield by eliminating constants that would result in a shift to zero beforehand

  iC4rl0s

  committed
  5c0fdbb

• minor bug in max_shift

  iC4rl0s

  committed
  087d4a9

• comparison bug in max_shift

  iC4rl0s

  committed
  0116023

Commits on Nov 7, 2024

• begin overflow handling

  ManuelLerchner

  committed
  03961c0

• separation of break_down into break_down_to_const_bitfields and break_down_to_consts

  iC4rl0s

  committed
  d42b989

• clean up; begin other methods

  ManuelLerchner

  committed
  6a26669

Commits on Nov 8, 2024

• format

  ManuelLerchner

  committed
  05b3d8e

• make it more functional. untested

  iC4rl0s

  committed
  27c9876

• bug fix: Bitfields with z set to zero missed

  iC4rl0s

  committed
  ca7c040

Commits on Nov 12, 2024

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

  Show description for 1338d65
  

  AdrianKrauss

  and

  Adrian Krauß

  authored
  1338d65

• fix comments

  ManuelLerchner

  committed
  447db3d

• Merge branch 'master' into overflow-handling

  ManuelLerchner

  committed
  3a00c0b

• delete bitfield ml

  ManuelLerchner

  committed
  89294a9

• fix

  ManuelLerchner

  committed
  c78510b

• Merge pull request #5 from ManuelLerchner/overflow-handling

  Show description for ec166cb
  ManuelLerchner

  authored
  ec166cb

• hotfix refinements

  ManuelLerchner

  committed
  1adccde

• .

  Draggon01

  committed
  2e05197

• bitfield shifts pr ready

  iC4rl0s

  committed
  897d6a2

• Merge branch 'master' into bitfield-shifts. Doesnt compile yet

  ManuelLerchner

  committed
  7d5913a

• added norm to almost every function which usess ikind

  

  Adrian Krauß

  committed
  257cc5b

• added correct fil and deleted test file

  

  Adrian Krauß

  committed
  24b3719

• bug fix: signedness with right shift considered

  iC4rl0s

  committed
  cbfbf28

• Merge branch 'bitfield-shifts' of github.com:ManuelLerchner/analyzer into bitfield-shifts

  iC4rl0s

  committed
  87b0189

Commits on Nov 14, 2024

• refine hotfix2

  ManuelLerchner

  committed
  ff8c4c7

• Revert "refine hotfix2"

  Show description for d405853
  ManuelLerchner

  committed
  d405853

• refine hotfix2

  ManuelLerchner

  committed
  ffc7285

• restore refine with congruence, as it was lost during merging

  ManuelLerchner

  committed
  5ec64ad

• Merge branch 'master' into 10-extend-norm-to-arithmetic-operations

  ManuelLerchner

  authored
  8cd7e62

Commits on Nov 15, 2024

• intDomain.ml is compilable

  iC4rl0s

  committed
  a31dc67

Commits on Nov 16, 2024

• Avoiding unnecessary computation when min{b} > ceil(log2 max{a}) in shift a b since in that case shift a b = zero always.

  iC4rl0s

  committed
  28d9db0

Commits on Nov 18, 2024

• begin first unit tests

  ManuelLerchner

  committed
  6177b13

• add simple shift unit tests

  Draggon01

  committed
  8e8b9cb

• Merge branch 'master' into bitfield-shifts

  Draggon01

  authored
  ed56bd8

Commits on Nov 19, 2024

• base test impl

  Draggon01

  committed
  9ae2b8f

• merge unit tests

  Draggon01

  committed
  874e1ed

• add simple tests

  Draggon01

  committed
  5ce8db7

• fix small bug in constant shifting expecting isSigned ik to check if the value is signed

  Draggon01

  committed
  4170f7f

• Merge pull request #14 from ManuelLerchner/unit-tests

  Show description for cd1bd06
  ManuelLerchner

  authored
  cd1bd06

• Merge pull request #12 from ManuelLerchner/bitfield-shifts

  Show description for 5eafd97
  ManuelLerchner

  authored
  5eafd97

• added bitfield to quickcheck

  

  Adrian Krauß

  committed
  811590d

• two bug fixes

  

  Adrian Krauß

  committed
  6999a20

• Merge branch 'master' into 10-extend-norm-to-arithmetic-operations

  ManuelLerchner

  authored
  9f72163

• Merge pull request #13 from ManuelLerchner/10-extend-norm-to-arithmetic-operations

  Show description for c660277
  ManuelLerchner

  authored
  c660277

• hotfix compilationn

  ManuelLerchner

  committed
  146d858

• Merge branch 'master' into Add-tests

  AdrianKrauss

  authored
  55bc2b3

• Merge pull request #15 from ManuelLerchner/Add-tests

  Show description for 90e1e99
  ManuelLerchner

  authored
  90e1e99

• hotfix compilation again

  ManuelLerchner

  committed
  6a32e42

• hotfix name clash after merge

  ManuelLerchner

  committed
  47b7a56

• logand fix

  ManuelLerchner

  committed
  5606e67

• bug fixes for arith ops

  

  Adrian Krauß

  committed
  8b1fbfc

• fixed norm

  

  Adrian Krauß

  committed
  4bf31cc

• is_invalid and mul fix

  

  Adrian Krauß

  committed
  0b4b4a1

• assertion function for shifts

  iC4rl0s

  committed
  15520a8

• bug fix in get_bit and further tests that lead to fails

  iC4rl0s

  committed
  d55eab5

• clean up

  ManuelLerchner

  committed
  6562161

• fix compile warnings

  ManuelLerchner

  committed
  2aa27f8

• format

  ManuelLerchner

  committed
  ad5f6f8

• improve arbitrary

  ManuelLerchner

  committed
  cfa0091

• Merge branch 'quickcheck-fixes' of github.com:ManuelLerchner/analyzer into quickcheck-fixes

  ManuelLerchner

  committed
  98a2d24

• fix bug after merge

  ManuelLerchner

  committed
  5914695

• Merge branch 'goblint:master' into master

  ManuelLerchner

  authored
  4a542be

Commits on Nov 21, 2024

• changed narrow and added unit tests for arith ops

  

  Adrian Krauß

  committed
  15f7abe

Commits on Nov 24, 2024

• add some regression tests

  ManuelLerchner

  committed
  f9f7fce

Commits on Nov 25, 2024

• reworked bitfield shifts, infix operators and some simple tests. signedness info in type necessary for maximal and minimal func?

  iC4rl0s

  committed
  1b6459d

• shift a b = zero when min{b} >= ceil(log (Size.bit ik))

  iC4rl0s

  committed
  31def4b

• negative shifts are undefined

  iC4rl0s

  committed
  2ba8f38

• bugfix: zero bits for lsb bitmask

  iC4rl0s

  committed
  b6762af

• refactored min and max

  

  Adrian Krauß

  committed
  b6ee7fa

Commits on Nov 26, 2024

• Merge remote-tracking branch 'refs/remotes/origin/quickcheck-fixes' into quickcheck-fixes

  

  Adrian Krauß

  committed
  a933c4e

• added infix to all functions

  

  Adrian Krauß

  committed
  e2366ff

• extract tuple 6 from intDomain file

  Draggon01

  committed
  addda52

• bugfix: shift_right did not shift right

  iC4rl0s

  committed
  29bcca1

• to_pretty_bits displays concrete values for a small enough number of unknown bits and introduced module for infix ops on bitfields

  iC4rl0s

  committed
  7984a0a

• small QoL improvements and bug fixes

  iC4rl0s

  committed
  ed1999a

• bugfix: certain zeros and uncertain ones

  iC4rl0s

  committed
  7fa0100

Commits on Nov 27, 2024

• add regression test for refinement

  ManuelLerchner

  committed
  96e5737

• add more regression tests for refines

  ManuelLerchner

  committed
  90338a7

Commits on Nov 28, 2024

• improve refine with interval; add regression tests

  ManuelLerchner

  committed
  f25a578

Commits on Dec 3, 2024

• fixed bitshifts

  Draggon01

  committed
  e9286e7

• removed commmented code and old wrong testcases

  Draggon01

  committed
  3e4928a

• fixed edge case where shift with 0 was done without zero in shifting bf

  Draggon01

  committed
  9bcd884

• added of bitfield for refinements

  

  Adrian Krauß

  committed
  6fe1162

• Merge pull request #18 from ManuelLerchner/quickcheck-fixes

  Show description for 5301322
  ManuelLerchner

  authored
  5301322

• Merge branch 'master' of github.com:ManuelLerchner/analyzer into more-regression-tests

  ManuelLerchner

  committed
  0fa8ca7

• remove duplicate function

  ManuelLerchner

  committed
  bad0bb8

• Revert "remove duplicate function"

  Show description for abde7e4
  ManuelLerchner

  committed
  abde7e4

• Reapply "remove duplicate function"

  Show description for 937b341
  ManuelLerchner

  committed
  937b341

• fix bug

  ManuelLerchner

  committed
  ddfaace

Commits on Dec 4, 2024

• add some more tests

  ManuelLerchner

  committed
  24f305f

• add missing regression tests

  ManuelLerchner

  committed
  7c4411d

Commits on Dec 7, 2024

• simple refinements for base invariant with bitfields

  

  Adrian Krauß

  committed
  6c2c570

Commits on Dec 9, 2024

• shift_right and shift_left return bot when the result or the parameters are undefined + qcheck tests for bitshifts: https://wiki.sei.cmu.edu/confluence/display/c/INT34-C.+Do+not+shift+an+expression…

  Show description for f237a9e
  iC4rl0s

  committed
  f237a9e

• added to_bitfield to refine base invariant further and regression test

  

  Adrian Krauß

  committed
  e4eefd9

Commits on Dec 10, 2024

• Merge pull request #19 from ManuelLerchner/more-regression-tests

  Show description for 8d4a4b8
  ManuelLerchner

  authored
  8d4a4b8

• Merge pull request #20 from ManuelLerchner/extract-tuple-six

  Show description for 8d7faf9
  ManuelLerchner

  authored
  8d7faf9

• Merge branch 'master' of github.com:ManuelLerchner/analyzer into invariant

  ManuelLerchner

  committed
  e2568fd

• Merge pull request #21 from ManuelLerchner/invariant

  Show description for ccb13c1
  ManuelLerchner

  authored
  ccb13c1

• hotfix regression tests

  ManuelLerchner

  committed
  88b0dfc

• Merge branch 'goblint:master' into master

  ManuelLerchner

  authored
  86fdeb5

Commits on Dec 11, 2024

• improved property tests for bitshifts

  iC4rl0s

  committed
  60fbbf5

• fix show

  ManuelLerchner

  committed
  ed27d3d

• Merge branch 'master' of github.com:ManuelLerchner/analyzer

  ManuelLerchner

  committed
  58eeeb4

• some property tests failed as generators were not constrained to the ik

  iC4rl0s

  committed
  dbe2e00

• fixed overflow in norm

  

  Adrian Krauß

  committed
  810a966

• renaming due to merge conflict

  

  Adrian Krauß

  committed
  d7b8755

• Merge branch 'master' into overflow

  AdrianKrauss

  authored
  541a87d

• two bug fixes

  

  Adrian Krauß

  committed
  686633a

• improved logging

  iC4rl0s

  committed
  4b3a0f8

• overflow behavior cannot be checked by property tests

  iC4rl0s

  committed
  dee9036

• more robust tests with a found bug

  iC4rl0s

  committed
  d6e3f61

• revert to basic unit tests

  iC4rl0s

  committed
  e3145ad

• Merge remote-tracking branch 'origin/overflow' into tests

  iC4rl0s

  committed
  6c720b8

Commits on Dec 12, 2024

• bug in exclude_undefined_bitshifts must be fixed or behavior defined

  iC4rl0s

  committed
  f09ead4

• Added distinction between invalid and undefined bitshifts. In the former case bot is returned and in the latter top.

  iC4rl0s

  committed
  8b53b08

Commits on Dec 13, 2024

• added pape rreferences and refined div

  

  Adrian Krauß

  committed
  c682527

Commits on Dec 15, 2024

• added some more cases

  Draggon01

  committed
  7a8b3ad

Commits on Dec 16, 2024

• more tests and overflow bugs detected. comment out TODO fails to see

  iC4rl0s

  committed
  8cf7192

• bugfix: zero shifted by anything should be zero

  iC4rl0s

  committed
  79a859a

• Merge branch 'master' of github.com:goblint/analyzer into goblint-master

  ManuelLerchner

  committed
  bfe5dc6

• Merge branch 'goblint-master'

  ManuelLerchner

  committed
  ed56056

Commits on Dec 17, 2024

• refactored intDomain

  

  Adrian Krauß

  committed
  f40fefb

• Merge branch 'master' into tests

  AdrianKrauss

  authored
  e1d948d

• merge

  Draggon01

  committed
  57ac94a

• exclude bitfield in modules python script as other intdomains

  Draggon01

  committed
  6c7f899

• changed to top_of

  

  Adrian Krauß

  committed
  313adb8

• merge

  

  Adrian Krauß

  committed
  ee9f358

• Merge remote-tracking branch 'refs/remotes/origin/tests' into tests

  

  Adrian Krauß

  committed
  288bf0d

• improved refinements with bitfield

  

  Adrian Krauß

  committed
  306aa33

• added overflow checking

  Draggon01

  committed
  3862f2e

• added missing bf in create

  Draggon01

  committed
  b683875

• bugfixes for overflow errs

  iC4rl0s

  committed
  26a23f5

• Merge branch 'tests' of github.com:ManuelLerchner/analyzer into tests

  iC4rl0s

  committed
  f70838d

• Merge pull request #22 from ManuelLerchner/tests

  Show description for 2e85cc9
  iC4rl0s

  authored
  2e85cc9

Commits on Dec 18, 2024

• fixed all current ocp-indent failures

  Draggon01

  committed
  898a68e

Commits on Dec 19, 2024

• added regression test

  Draggon01

  committed
  0cc16dc

• fixed overflow handling

  

  Adrian Krauß

  committed
  65237fd

Commits on Dec 20, 2024

• Merge pull request #26 from ManuelLerchner/precission

  Show description for 5cf4620
  ManuelLerchner

  authored
  5cf4620

• Merge pull request #25 from ManuelLerchner/indent-fixes

  Show description for dc68f48
  ManuelLerchner

  authored
  dc68f48

Commits on Jan 4, 2025

• added adapted functions from interval domain to base

  

  Adrian Krauß

  committed
  312b0c3

Commits on Jan 6, 2025

• fixed bug in refine with congruence

  

  Adrian Krauß

  committed
  3034ad3

Commits on Jan 7, 2025

• fixed Div by zero exception

  

  Adrian Krauß

  committed
  1f08a87

• fixed overflow in bitshift

  

  Adrian Krauß

  committed
  552c333

• removed test files

  

  Adrian Krauß

  committed
  571cde3

• removed unnecessary file

  

  Adrian Krauß

  committed
  18ee9a9

• Merge branch 'goblint:master' into master

  ManuelLerchner

  authored
  51c13e7

• Merge branch 'master' into fixingBase

  ManuelLerchner

  authored
  e7c3237

• Merge pull request #27 from ManuelLerchner/fixingBase

  Show description for 1376824
  ManuelLerchner

  authored
  1376824

Commits on Jan 8, 2025

• canonize interval-sets after refine with bitfield

  ManuelLerchner

  committed
  abb48c4