Add a version of get_or_create_string_literal_symbol that takes a string parameter #4509
Conversation
Following the new coding standard.
antlechner
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
| /// global symbols will be added. | ||
| /// \param string_refinement_enabled: if true, string refinement's string data | ||
| /// structure will also be initialised and added to the symbol table. | ||
| /// \return a symbol_expr corresponding to the new or existing literal symbol. | ||
| symbol_exprt get_or_create_string_literal_symbol( | ||
| const exprt &string_expr, |
There was a problem hiding this comment.
Are there any users of this overload left?
There was a problem hiding this comment.
Only one:
There was a problem hiding this comment.
In that case it would be a very welcome addition to this PR to make java_string_literal_exprt rather than directly twiddling operands / named subexpressions -- fair enough though if you think that's out of scope.
There was a problem hiding this comment.
It looks like there aren't any java[\w_]+exprt types yet. Should such a type go into jbmc/src/java_bytecode/java_types.h or a new file, e.g. something like jbmc/src/java_bytecode/java_expressions.h or similar?
Or does it make more sense to create a new folder jbmc/src/util? In that case I would definitely make a new PR for that.
There was a problem hiding this comment.
Does symex have to handle these expressions in a specific way? If it's the case then they shouldn't be defined in a jbmc subdirectory. Otherwise java_expr.h would be clearer for showing the class inherits from exprt and I'd prefer one class per file, so java_string_literal_expr.h would be better.
There was a problem hiding this comment.
Hearing about language-specific expressions makes me panic a bit. You will need to make sure all of these are gone by the time the code leaves the Java front-end.
There was a problem hiding this comment.
They are; these are just descriptions of the exprts produced by the bytecode parser. The only other example I'm aware of now, and which I suggest we emulate, is fieldref_exprt, which is defined in java_bytecode_parse_tree.h.
There was a problem hiding this comment.
(that expression is also local to the parser and becomes member_exprt later once we have more information about what it's referring to)
There was a problem hiding this comment.
I added the new class as you suggested, in a new commit.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 78d181a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107812797
antlechner
force-pushed
the
antonia/refactor-constant-string-symbol
branch
2 times, most recently
from
bcc3f91 to
50ee969
Compare
antlechner
force-pushed
the
antonia/refactor-constant-string-symbol
branch
from
50ee969 to
f6db991
Compare
antlechner
force-pushed
the
antonia/refactor-constant-string-symbol
branch
from
f6db991 to
ef2e5fe
Compare
This simplifies the code in a few places, since we don't have to repeat the same lines of constructing the string literal exprt every time.
With this new class, we can avoid directly accessing named subexpressions of exprts with id() == ID_java_string_literal.
antlechner
force-pushed
the
antonia/refactor-constant-string-symbol
branch
from
ef2e5fe to
9e499d5
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 9e499d5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108126079
No functional change, only refactoring.