Use access events in MemOutOfBounds analysis#2027
Open
karoliineh wants to merge 15 commits into
Open
Conversation
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
Use access events instead of recursively traversing expressions in memOutOfBounds. This follows the same direction as the useAfterFree refactoring #1864: accessAnalysis determines what is accessed, while memOutOfBounds only checks the reported access. This avoids duplicating access traversal logic and removes the need to distinguish implicit from explicit dereferences in the analysis itself. Keep the initial refactor close to the previous implementation to make the behavioral diff easier to review. Further cleanup of now-obsolete helpers is left for a follow-up commit.
…nto cases that use them
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
karoliineh
added
cleanup
| collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed"; | ||
| let activated = get_string_list "ana.activated" in | ||
| emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *) | ||
| emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated || List.mem (MemOutOfBounds.Spec.name ()) activated (* TODO: some of these don't have access as dependency *) |
Member
There was a problem hiding this comment.
Can we do this TODO here? Seems simple.
Contributor
There was a problem hiding this comment.
Pull request overview
Refactors the memOutOfBounds analysis to consume shared Events.Access emitted by accessAnalysis instead of locally traversing expressions/lvalues, aligning it with the access-event-based infrastructure used by other analyses (e.g., useAfterFree).
Changes:
- Register
memOutOfBoundsas depending onaccessand add an event handler to processEvents.Access. - Rework OOB checking logic into clearer cases (deref checks, pointer-value checks, counted library accesses) and add stored-pointer-offset handling for dereferences.
- Update regression tests/expected outputs for changed diagnostics and add a one-past-pointer dereference regression.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
src/analyses/memOutOfBounds.ml |
Main refactor: switch to access events, new OOB reporting helper, new offset handling and event-based checking logic. |
src/analyses/accessAnalysis.ml |
Enable single-threaded access event emission when memOutOfBounds is activated. |
tests/regression/74-invalid_deref/36-one-past-pointer.c |
Add explicit one-past dereference to ensure a warning is produced. |
tests/regression/74-invalid_deref/01-oob-heap-simple.t |
Update expected warning text to match refactored diagnostics. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| | _ -> () | ||
| (* Actual dereference/access through a pointer. *) | ||
| | AddrOf (Mem e, o) when not (ptr_only_has_str_addr e) -> | ||
| check_ptr_deref_access man e o |
Comment on lines
+269
to
+271
| (* Pointer arithmetic / pointer value access. *) | ||
| | _ when isPointerType (typeOf exp) && not (ptr_only_has_str_addr exp) -> | ||
| check_ptr_value_access man exp (get_addr_offs_from_ad man exp ad) |
Comment on lines
+315
to
+317
| | AddrOf lval | ||
| | StartOf lval -> | ||
| let ptr_exp = Lval lval in |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR refactors
memOutOfBoundsto use access events, similarly to theuseAfterFreerefactoring in #1864.Instead of recursively traversing expressions inside
memOutOfBoundsto rediscover what is accessed, the analysis now consumesEvents.Accessemitted byaccessAnalysis. This makes the analysis depend on the shared access infrastructure and removes the local implicit/explicit dereference traversal logic. It also refactors and simplifies the code in other aspects.This PR replaces #2024. The stored-pointer-offset dereference fix (#2017 (comment)) from #2024 is included here as part of the event-based cleanup instead of being merged separately.
Changes:
memOutOfBoundsas depending onaccess.memOutOfBoundsis active.memOutOfBoundswith handling ofEvents.Access.memset/memcpy(kept close to as was originally)I ran the portfolio on 074e4d7 for
memsafetytasks with 15s timeouts (as there were only 5 tasks that took > 12s to solve in the C.MemSafety category from SV-COMP 2026). The results were sound.Open questions
check_ptr_value_accesscase is even needed to get rid of theltandlethings (FixmemOutOfBoundshandling of negative pointer offsets #2017 (comment))PreValueDomain.Offs.to_indexwithout losing precision. Currently, the index case is less precise in the versionOffsets.to_indexand using this, some OOB tests start to fail due to lack of precision, but adding a case ofin between the
makes some other (unrelated) tests fail
I also didn't resolve the TODOs that were already there about deduplicating some functions with base, namely:
get_size_of_ptr_target(* TODO: deduplicate with base *)convert_offset(* TODO: Some duplication with convert_offset in base.ml, unclear how to immediately get more reuse *)