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

sem: remove float analysis from sem/guards #1240

Merged
merged 2 commits into from
Mar 15, 2024

Conversation

Clyybber
Copy link
Contributor

@Clyybber Clyybber commented Mar 14, 2024

Summary

Remove float analysis from sem/guards since it's currently unsound.

Details

sem/guards is only used for static bounds checking (
--staticBoundChecks ), not nil checking, warning for checked field
accesses ( --warning:ProveField ) and field accesses of fields
annotated with {.guard: ...} .
Since object variants with a float discriminator are invalid and
bound checks only concern integers, only conversions to float range
types would be affected under --staticBoundChecks .

It's not clear whether the analysis method here can work with floats
without special treatment in a lot of cases, due to float equality
lacking the subsitution and reflexivity property or the comparison
relations not being total.

@Clyybber Clyybber changed the title Remove float analysis from sem/guards Remove float analysis from sem/guards Mar 14, 2024
Copy link
Collaborator

@saem saem left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One minor typo.

So now we're using very simple symbol equality during tree equivalence checks in guards. Are we relying on guards outside of things like checked arithmetic which might be impacted?

compiler/sem/guards.nim Outdated Show resolved Hide resolved
@saem saem changed the title Remove float analysis from sem/guards sem: remove float analysis from sem/guards Mar 14, 2024
@saem
Copy link
Collaborator

saem commented Mar 14, 2024

For the summary, the impact here would be not removing floating point operation checks in certain cases?

@Clyybber
Copy link
Contributor Author

Clyybber commented Mar 14, 2024

So now we're using very simple symbol equality during tree equivalence checks in guards. Are we relying on guards outside of things like checked arithmetic which might be impacted?
For the summary, the impact here would be not removing floating point operation checks in certain cases?

sem/guards is only used for static bounds checking (--staticBoundChecks), not nil checking and warning for checked field accesses (--warning:ProveField) and field accesses of fields annotated with {.guard: ...}, so it isn't actually used for optimization/removing checks.
Since object variants with a float kind are invalid and bound checks concern integers, only float range checks would be affected under --staticBoundChecks.
This PR doesn't actually change to use bit equality for floats (leaving that for #1238), but it does make it so that it shouldn't matter. (Although there are AFAICT other soundness issues in sem/guards so there might be cases where it does still matter)

@saem
Copy link
Collaborator

saem commented Mar 14, 2024

I moved the extra info into details, guards stuff seems so broken.

@saem
Copy link
Collaborator

saem commented Mar 14, 2024

/merge

Copy link

Merge requested by: @saem

Contents after the first section break of the PR description has been removed and preserved below:


Notes for Reviewers

@chore-runner chore-runner bot added this pull request to the merge queue Mar 14, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 14, 2024
@zerbina zerbina added the compiler/sem Related to semantic-analysis system of the compiler label Mar 14, 2024
@Clyybber Clyybber added this pull request to the merge queue Mar 14, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 14, 2024
@saem
Copy link
Collaborator

saem commented Mar 15, 2024

/merge

@chore-runner chore-runner bot added this pull request to the merge queue Mar 15, 2024
Merged via the queue into nim-works:devel with commit 87e282a Mar 15, 2024
31 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
compiler/sem Related to semantic-analysis system of the compiler
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants