Remove type argument from do_update_offset, fix calls with incorrect offset type#1984
Open
Remove type argument from do_update_offset, fix calls with incorrect offset type#1984
do_update_offset, fix calls with incorrect offset type#1984Conversation
Makes it consistent with do_eval_offset. This breaks a lot of tests.
The bot_value is constructed for the variable, but update_offset goes deeper into fields.
to_cil_offset is specific for partitioned arrays and drops indices. Thus, it can compute an incorrect type which doesn't match the actual offset.
The entire var is refined, but update_offset goes deeper into fields.
Contributor
There was a problem hiding this comment.
Pull request overview
This PR removes the recursive “type” parameter from do_update_offset to align its recursion behavior with do_eval_offset, and fixes VD.update_offset call sites that were passing a type that didn’t correspond to the offset being updated.
Changes:
- Simplified
ValueDomain.update_offsetinternals by removing the recursivet: typargument fromdo_update_offset. - Updated Base analysis write paths to compute the updated lvalue type via
Offs.type_of ~base:x.vtype offs(with fallback) instead ofCilfacade.typeOfLvalon an index-dropping offset. - Updated BaseInvariant refinement to pass
Cilfacade.typeOfLval x(lval-with-offset type) instead ofvar.vtype.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
src/cdomain/value/cdomains/valueDomain.ml |
Removes recursive t threading in do_update_offset, keeping type usage consistent with do_eval_offset. |
src/analyses/baseInvariant.ml |
Passes the correct offset-specific lval type into VD.update_offset during whole-variable refinement. |
src/analyses/base.ml |
Computes the type for VD.update_offset using Offs.type_of (and improves debug/tracing output accordingly). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
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 is a continuation of #1914.
There I noticed that
do_update_offsetrecursively may change the type, whereasdo_eval_offsetdid not. This mismatch of strange because both should recurse into base value domain abstractions in the same manner.Thus, this PR removes that argument to make things more consistent.
Simply removing the argument breaks a lot of tests. Turns out that
VD.update_offsetis being called in multiple places with the incorrect type which isn't the one corresponding to the offset being updated.By fixing these (explanations in commit messages), all tests again pass.
The type-changing aspect of
do_update_offsetwas just covering up these root issues by managing to get the type from somewhere else.TODO
ana.base.branch.refine-pointer-by-pointee#1982 (comment).