Skip to content

Improve memOutOfBounds precision for points-to sets which mix allocs with others#2030

Draft
sim642 wants to merge 2 commits into
masterfrom
memOutOfBounds-blobsize
Draft

Improve memOutOfBounds precision for points-to sets which mix allocs with others#2030
sim642 wants to merge 2 commits into
masterfrom
memOutOfBounds-blobsize

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented May 13, 2026

This is on top of #2029.

Pointer may point to either allocated blob or static array.
Currently memOutOfBounds only uses BlobSize query for points-to sets which are definitely alloc, but not a mix.

This moves the decision to be made per-pointee basis, not on the basis of the whole points-to set.
The diff probably looks much nicer with whitespace ignored.

TODO

  • sv-benchmarks
  • Look into TopValue exceptions from sv-benchmarks.

sim642 added 2 commits May 13, 2026 15:44
Pointer may point to either allocated blob or static array.
Currently memOutOfBounds only uses BlobSize query for points-to sets which are definitely alloc, but not a mix.
@sim642 sim642 added this to the SV-COMP 2027 milestone May 13, 2026
@sim642 sim642 self-assigned this May 13, 2026
@sim642 sim642 added sv-comp SV-COMP (analyses, results), witnesses precision labels May 13, 2026
Base automatically changed from memOutOfBounds-one-past-end to master May 13, 2026 17:21
@sim642
Copy link
Copy Markdown
Member Author

sim642 commented May 14, 2026

According to an sv-benchmarks run with level01, 60s and 1GB, this doesn't improve any verdicts: https://goblint.cs.ut.ee/results/335-all-level01-pr-2030-after/table-generator-cmp.diff.html#/table.

However, there is a regression on

  • ldv-challenges/linux-3.14_linux-kernel-locking-mutex_drivers-net-ethernet-chelsio-cxgb4-cxgb4.cil
  • ldv-challenges/linux-3.14_linux-kernel-locking-spinlock_drivers-net-ethernet-chelsio-cxgb4-cxgb4.cil

where TIMEOUT goes to exception Lattice.TopValue. That's with unreach-call not valid-memsafety. This changes base just to keep the function in sync with memOutOfBounds.
For reference, in SV-COMP we output true after >400s for these but get no points because the witness isn't validated.

Somehow it's coming from the Fake lattice used for ZeroInit of blobs.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

precision sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant