Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Forward-propagate assumptions/assertions (if possible) to strengthen the analysis #445

Open
danmatichuk opened this issue Sep 10, 2024 · 0 comments
Labels
enhancement New feature or request

Comments

@danmatichuk
Copy link
Collaborator

Generally the only information that is propagated forwards is equivalence domains and value domains. Neither of these are suitable for representing relational properties beyond simple equality (e.g. r1 (original) == r2 (patched)).

Often these relational properties are introduced in the form of equivalence conditions or assertions, but they are only available in exactly the CFAR where they are introduced. To carry this information forward, it needs to be asserted later and then propagated backwards in order to be used.

To recover this information in some cases, we can attempt to forward-propagate any conditions for a CFAR using the existing equivalence domain rescoping heuristics.

This is a simple change in lieu of a more invasive change to the equivalence/value domains in order to support more kinds of relations.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant