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

Avoid concatenating Text values in termToPat. #1272

Merged
merged 1 commit into from
Sep 15, 2021
Merged

Avoid concatenating Text values in termToPat. #1272

merged 1 commit into from
Sep 15, 2021

Conversation

brianhuffman
Copy link
Contributor

Fixes #1263.

We now use identBaseName instead of identText in the termToPat
definition. While identText concatenates the module name and base
name, identBaseName just returns the base name directly.

Using only the base name means that there is a chance of name collisions
between constants that differ only by module name. However, term nets
are only used as an approximate filter prior to term matching; it is
not a problem if a few extra hits are returned from time to time.

Ultimately it might be better to replace the use of Text in the term
net Atom constructor with a more specialized key type; for example
with ExtCns names we could use the VarIndex for matching. However,
this would require modifying the term net library.

Copy link
Contributor

@robdockins robdockins left a comment

Choose a reason for hiding this comment

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

Seems OK to me, although maybe we are better off precomputing and caching the identText when building an Ident. Using VarIndex to match with also seems like a better idea, but I don't think this will be a problem.

@robdockins
Copy link
Contributor

This is going to interact somewhat with #1298. I'm not sure what is the best order for them to land.

@brianhuffman
Copy link
Contributor Author

I was holding off on merging this because I wasn't sure that this was the best solution to the problem, so I was thinking about making further changes. Go ahead and merge #1298 first.

Fixes #1263.

We now use `identBaseName` instead of `identText` in the `termToPat`
definition. While `identText` concatenates the module name and base
name, `identBaseName` just returns the base name directly.

Using only the base name means that there is a chance of name collisions
between constants that differ only by module name. However, term nets
are only used as an approximate filter prior to term matching; it is
not a problem if a few extra hits are returned from time to time.

Ultimately it might be better to replace the use of `Text` in the term
net `Atom` constructor with a more specialized key type; for example
with `ExtCns` names we could use the `VarIndex` for matching. However,
this would require modifying the term net library.
@brianhuffman brianhuffman added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Sep 14, 2021
@atomb atomb added this to the 0.9 milestone Sep 14, 2021
@brianhuffman
Copy link
Contributor Author

brianhuffman commented Sep 15, 2021

heapster-tests is failing with this message:

"heapster_assume_fun" (/home/runner/work/saw-script/saw-script/heapster-saw/examples/mbox.saw:44:1-44:20):
Could not find symbol: llvm.objectsize.i64.p0i8

later it says

make[1]: *** No rule to make target 'mbox_gen.v', needed by 'mbox_gen.vo'.  Stop.

@mergify mergify bot merged commit 58ca144 into master Sep 15, 2021
@mergify mergify bot deleted the issue1263 branch September 15, 2021 04:13
@brianhuffman
Copy link
Contributor Author

I guess that was a transient failure, since it worked after a restart without any changes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Avoid using toAbsoluteName so much in rewriter
3 participants