Review and simplify unrollType uses#2019
Conversation
VD.top_value already includes on-demand unrolling. It also needs non-unrolled type because it checks for mutex, etc. types.
VD.bot_value already includes on-demand unrolling. It also needs non-unrolled type because it checks for mutex, etc. types.
There was a problem hiding this comment.
Pull request overview
This PR refactors several call sites to rely less on explicit Cil.unrollType calls by centralizing struct-type checks in Cilfacade and passing more original typ values through to ValueDomain. In the analyzer, that mostly affects value initialization/top-value fallback paths and a small memLeak helper.
Changes:
- Added
Cilfacade.isStructTypeand reused shared type predicates. - Replaced several explicit
unrollTypecalls inbase.mlandvalueDomain.mlwith directtypforwarding. - Simplified memLeak/global-struct filtering and union-find struct-type detection.
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 6 comments.
Show a summary per file
| File | Description |
|---|---|
src/common/util/cilfacade.ml |
Adds a new helper for identifying struct (not union) types. |
src/cdomains/unionFind.ml |
Reuses a shared struct/union predicate instead of a local helper. |
src/cdomain/value/cdomains/valueDomain.ml |
Simplifies TNamed handling in bot_value. |
src/analyses/memLeak.ml |
Replaces manual global-struct filtering with the new facade helper. |
src/analyses/base.ml |
Removes explicit unrollType calls in several VD.top_value fallback paths. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.bot ()) | ||
| | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.Bufs.empty (), false) | ||
| | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t) | ||
| | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr t |
There was a problem hiding this comment.
bot_value was an odd one out that had this unrollType for the TNamed case, others didn't so I removed it from here as well.
Technically, unrollType does propagate the attributes but these functions haven't done that before so I'm not sure if it's actually needed for anything. I left TODOs about this just in case.
See individual commits.