fixes fresh variable generation #1376
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.
This PR is a cherry pick from a big effort on reducing the number of calls to
Toplevel.exec
, with the end goal to forbid any nesting calls. The amount of work turned to be much greater than expected as we still rely very much on the old abstractions (spoiler: the main issue is with how we encode CPU exceptions). The problem with nested calls, is that they have inconsistent views on the knowledge base and that the outer calls undo the knowledge of the inner calls. The real impact is not that tragic but there are some number of annoying artifacts with which we would like to deal.In this PR we will deal with the way how fresh variables are generated. So far they were using the knowledge base to store the number of generated variables and since
Bap.Std.Var.create
is having non-monadic type we had to useToplevel.exec
to evaluate the creation of a fresh variable in the knowledge base. This function is still heavily used, especially by the old lifters, which in turn are run during disassembly, which is a knowledge computation by itself, so we have the nested call toToplevel.exec
every time we create a new variable in the legacy lifters. As a result we have intersecting variables, on targets that use both new and old lifters, e.g., ARM. The semantics is still correct, because the variables have non-intersecting scopes, although this argument could be discarded by using a different definition of a variable scope. To remove this nuisance, we no longer use the knowledge base to generate fresh identifiers for variables in Bap.Std.Var but instead use the good old reference counter, which is set to a high value that shouldn't intersect with the theory fresh variables, which occupy the lower spectrum of the variable numbers. Of course, theoretically they can still clash, but in practice such a possibility could be safely ignored, especially since they still will have non-intersecting scopes.Note, that in the future, we will define the scope more precisely and will reuse variable identifiers more aggressively. So it is better not to rely on the current behavior that each fresh variable has indefinite scope and never changes its type.