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

More precise value analysis for "known integer or Vundef" results #520

Merged
merged 2 commits into from
Aug 22, 2024

Conversation

xavierleroy
Copy link
Contributor

This PR introduces a new abstract value IU n, standing for "either Vint n or Vundef".

It enables more precise value analysis of comparison and selection operators, which in turn enables more compile-time evaluation of these operators.

Example:

struct s { char c[4]; char d[2]; };

int f(void)
{ struct s x; return (x.c + 6 == x.d); }

int g(void)
{ struct s x; if (x.c + 6 == x.d) return 1; else return 0; }

The current CompCert optimizes g into return 0, but fails to optimize f, as the result of the pointer comparison can be Vundef, so its abstract value cannot be I Int.zero.

With this PR, the expression x.c + 6 == x.d is analyzed as IU Int.zero, and constant-propagated to the constant 0. Hence, f and g produce the same return 0; code.

This improves analysis precision for comparisons and selections.
Results that analyze to `IU n` are turned into
`load-integer-immediate(n)` operations.

This is semantically safe, and enables compile-time evaluation of some
pointer comparisons (e.g. `&x == &x` where `x` is a global variable or
a stack-allocated variable).
@xavierleroy
Copy link
Contributor Author

Note: we could further reduce Uns p 0 to IU Int.zero, since 0 is the only 0-bit unsigned integer. But this needs a bit of work on the lub operator. I'll look into this later.

@xavierleroy xavierleroy merged commit d351f4b into master Aug 22, 2024
7 checks passed
@xavierleroy xavierleroy deleted the value-analysis-IU branch August 26, 2024 14:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant