Fix unsound var_eq unknown function invalidation #694
Merged
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.
Initially this came up in #618, where a TODO test and commented out possible fix were added. Since those benchmarks ended up not being relevant, we put off fixing the issue.
While analyzing zstd with var_eq I found that the same unsoundness occurs there, making all locking in files other than
pool.c
dead. This applies the commented out fix from #618 and a couple of others where zstd caused crashes due to the change.This changes the unknown function invalidation to just use
remove
like all the other var_eq invalidation. The old algorithm did something weirder: it checked each expression in the local state whether it's reachable from the lvalues reachable from the invalidated variables. I don't recall any more why it was done so, but the change doesn't cause any regressions.Or is the new invalidation unsound in some different untested way? The extreme solution would be to apply both invalidations in sequence to ensure removal by both, but I'm not sure if we have to go that far.