Forward Solvers: Split local unknowns by digests #1971
Open
jerhard wants to merge 43 commits intofwd_constrsys_newfrom
Open
Forward Solvers: Split local unknowns by digests #1971jerhard wants to merge 43 commits intofwd_constrsys_newfrom
jerhard wants to merge 43 commits intofwd_constrsys_newfrom
Conversation
This breaks comparing constraint systems for the backward constraint systems (for now).
…, context, original- and current digest.
Handle man.split with the digest system for the foward-propagating constraint system. Handling of procedure calls still needs some work. When defaulting to "bu" as the default solver this commit increases the number of failing sanity tests to 38.
…hin called function.
This introduces makes the domain for function return nodes a mapping from unknowns to abstract values. The unknowns that are used as keys may differ by digest, in particular.
This will allow to have the globals defined by the analyses, globals for returns split by current digest, and globals for returns joined over current digests.
…gests at global return unknowns.
…ction is applicable works.
…ues from dead digests not being pruned
…on call pollute results. Also a problem without digests.
In fwdConstraints, in case that the callee does not return, introduce a return path with bottom for the longjmpLifter to do its work.
…viely. This implementation using man.split should work when using digests and when using pathsensitivity. The event list passed to man.split is empty, since there is nothing further to do.
…onal path-sensitivity with option solvers.fwd.digests.
Member
|
I just realized that this isn't merging into master. That's why there's no forward solver in the diff here. |
Contributor
There was a problem hiding this comment.
Pull request overview
This PR introduces digest-based splitting of local unknowns in the forward constraint system to realize path-sensitivity via analysis-spec P digests (configurable via solvers.fwd.digests). It also adapts result aggregation and the XSLT report output to present results grouped by (context, calling digest, current digest, abstract state).
Changes:
- Add digest-aware local variables and forward constraint generation that propagates/updates digests and supports splitting via
man.split. - Extend the framework with
Spec'/LVarSetsupport and a new 3-way lifted global lattice (Lift3/GVar3) to represent spec globals + per-return-node globals + return-node sets. - Update XSLT/XML result output and add new regression tests under
tests/regression/90-digests.
Reviewed changes
Copilot reviewed 19 out of 20 changed files in this pull request and generated 9 comments.
Show a summary per file
| File | Description |
|---|---|
xslt/node.xsl |
Render node results as grouped <tuple> entries with optional digest sections. |
tests/regression/90-digests/01-function-call.c |
New regression test for digest-sensitive behavior across function calls. |
tests/regression/90-digests/02-mutex-lock-split.c |
New regression test for digest-sensitive mutex locking. |
tests/regression/90-digests/03-function-call-split.c |
New regression test for digest changes during a function call. |
tests/regression/90-digests/04-garbage-digest.c |
New regression test for digest “garbage collection” expectations. |
tests/regression/90-digests/05-garbage-call.c |
New regression test involving calls/precision; currently has a C11 declaration-order concern. |
tests/regression/90-digests/06-longjmp-return.c |
New regression test for longjmp/setjmp interactions with the solver. |
src/solver/td_simplified_ref_improved.ml |
Formatting-only adjustments. |
src/lifters/noDigestLifter.ml |
New lifter to expose unit digests when solvers.fwd.digests is disabled. |
src/lifters/longjmpLifter.ml |
Adjust setjmp handling to use man.split for separating normal vs longjmp return flows. |
src/framework/fwdControl.ml |
Switch forward analysis to Spec', integrate digest-aware result type, and wire in the new comparator. |
src/framework/fwdConstraints.ml |
Core change: digest-aware locals (VarDigestF), digest propagation/update, and return handling via return-node sets. |
src/framework/fwdCompareConstraints.ml |
New forward comparator adapted to digest-aware locals and the new forward globals. |
src/framework/control.ml |
Switch to Spec' in the (non-forward) control pipeline for shared infrastructure. |
src/framework/compareConstraints.ml |
Refactor comparator to work against SpecSys and adjust local-joining logic structure. |
src/framework/analysisResult.ml |
Change XML printing to emit <tuple> entries and add a digest-aware result entry type. |
src/framework/analyses.ml |
Introduce VarDigestF, GVarFCNW return variants, GVar3, Spec', and Spec2Spec'. |
src/domain/lattice.ml |
Add Lift3 lattice combinator to support 3-way lifted globals. |
src/config/options.schema.json |
Add new option solvers.fwd.digests (default false). |
src/common/domains/printable.ml |
Add Lift3Conf printable and Prod4 printable used by new result/global types. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
Member
michael-schwarz
left a comment
michael-schwarz
left a comment
There was a problem hiding this comment.
Nice! I was wondering if now that you have understood all the details may be a good idea to leave some more comments in these modules. I think if someone comes back to this in a few years, it will all be very hard to understand.
Also: Maybe establishing some kind of terminology for the return variable where occuring digests are accumulated may be helpful?
|
|
||
| module V = | ||
| struct | ||
| (* TODO: Consider splitting unknowns by digest for constraint system in [FwdConstraints] *) |
Member
There was a problem hiding this comment.
Does this mean that here we still have the set construction? Which is fine, I'm just worried whether this will work together nicely.
Member
There was a problem hiding this comment.
And in particular whether such sets will then leak to places they are not supposed to be in, i.e., non-longjumpy unknowns.
Member
Author
There was a problem hiding this comment.
@michael-schwarz What do you mean with set construction here?
Member
There was a problem hiding this comment.
The reduced cardinal powerset mechanism that we used for path-sensitivity before.
Member
|
@arkocal Can you have a look if the test failures as you would expect them to be? |
…the XML when the lifter is used.
…point is needed for the result view.
…e accurately what it does.
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
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 splits the local unknowns by digests for the forward constraint systems. It uses the module
Pof the analysis specifications that was previously used for pathsensitivity.Local unknowns now are four-tuples, consisting of the node, the calling context, the calling digest (called original_digest in the implementation) and the current digest.
After the application of a transfer function, when the new abstract state is computed, the new current digest is derived from the abstract state via the function
P.of_elt. In case a transfer function should introduce some splitting, it can useman.split, which is the same mechanism as for pathsensitivity.The pathsensitivity (without splitting of unknowns) is used when
solvers.fwd.digestsisfalse, and the digests are used otherwise.Additionally, there are changes to the XSLT-output, now grouping result entries consisting of context, calling digest, current digest and abstract state together.