Add a model for String.intern #22
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
romainbrenguier
added a commit
to romainbrenguier/cbmc
that referenced
this pull request
Apr 30, 2019
This contains a model for String.intern diffblue/java-models-library#22
romainbrenguier
force-pushed
the
romain/intern
branch
from
59a2dbf to
2568c36
Compare
peterschrammel
approved these changes
Apr 30, 2019
antlechner
reviewed
Apr 30, 2019
src/main/java/java/lang/String.java
Outdated
| static String[] cproverInternPool = null; | ||
|
|
||
| /** | ||
| * Number of element stored in the pool for {@code String.intern} pool. |
src/main/java/java/lang/String.java
Outdated
|
|
||
| /** | ||
| * Number of element stored in the pool for {@code String.intern} pool. | ||
| * This can be smaller than {@code cproverInternPoll.length} which |
src/main/java/java/lang/String.java
Outdated
| CProver.notModelled(); | ||
| return CProver.nondetWithoutNullForNotModelled(); | ||
| // Initialize the pool if needed | ||
| if(cproverInternPool == null) { |
src/main/java/java/lang/String.java
Outdated
| return this; | ||
| } | ||
| // Look for an entry in the pool equal to `this` | ||
| for(int i = 0; i < cproverInternPoolSize; ++i) { |
There was a problem hiding this comment.
🍵 (here and in the line just below)
| if(cproverInternPool == null) { | ||
| int capacity = CProver.nondetInt(); | ||
| CProver.assume(capacity > 0); | ||
| cproverInternPool = new String[capacity]; |
There was a problem hiding this comment.
❓ Why isn't this done as part of the initialisation of cproverInternPool? Is this to avoid the static initialiser getting too complicated? If that is not a problem, it would be good to avoid this null check.
There was a problem hiding this comment.
yes I don't expect String.intern to be used often so I prefer to keep the String static initialiser simple (which is called all the time). The null check is relatively simple compared to the loop that follows, it could also be replaced by if(cproverInternPoolSize == 0) but I don't know if there is an advantage in that.
This uses a custom static pool of strings, through which we look-up strings on which intern was already called.
romainbrenguier
force-pushed
the
romain/intern
branch
from
2568c36 to
1d879b0
Compare
antlechner
approved these changes
Apr 30, 2019
romainbrenguier
added a commit
to romainbrenguier/cbmc
that referenced
this pull request
Apr 30, 2019
This contains a model for String.intern diffblue/java-models-library#22
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 uses a custom static pool of strings, through which we look-up
strings on which intern was already called.
This is in preparation for removing the special handling of
internin JBMC: diffblue/cbmc#4554