JSIL front-end: no need for parser reentrancy

[tautschnig]

Just make sure it isn't used in a reentrant manner.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: 7 lines in your changes are missing coverage. Please review.

Comparison is base (69bb2b6) 79.09% compared to head (6682802) 79.09%.

Files	Patch %	Lines
src/jsil/jsil_parser.h	0.00%	7 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8153      +/-   ##
===========================================
- Coverage    79.09%   79.09%   -0.01%     
===========================================
  Files         1695     1695              
  Lines       196583   196589       +6     
===========================================
- Hits        155496   155493       -3     
- Misses       41087    41096       +9     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[kroening]

Where does the bison state go?

[tautschnig]

Where does the bison state go?

Good call, this is now fixed (by using %pure-parser -- see comments and commit messages for more on this choice).

[kroening]

Good call, this is now fixed (by using %pure-parser -- see comments and commit messages for more on this choice).

Sure this is worth it? We currently don't need reentrant parsing, and if all you want is to remove set_message_handler call, you could achieve that with a simple precondition in the constructor.

[tautschnig]

Good call, this is now fixed (by using %pure-parser -- see comments and commit messages for more on this choice).

Sure this is worth it? We currently don't need reentrant parsing, and if all you want is to remove set_message_handler call, you could achieve that with a simple precondition in the constructor.

Added commits to just do the precondition. The overall change should now accomplish the simpler approach, while the individual commits could be reverted in case we ever wish to use full reentrancy.

[kroening]

There are still lots of changes to the scanner left, which are probably not needed?

[tautschnig]

There are still lots of changes to the scanner left, which are probably not needed?

We can stick with the existing jsil_scanner_init and the file-local global pointer, in which case we indeed don't need those changes as we aren't going for a reentrant setup anyway. We could then just have the new PRECONDITION as about the only change for added safety.

I believe the reentrant lexer makes for cleaner code, but I acknowledge that we don't actually need that capability and it might just be seen as unnecessary code churn. So I am ok producing a (much simpler) variant of this PR that just introduces the additional safety check. Just let me know.

Edit: and I will use the outcome of this PR to inform how to proceed with #8135, #8138, #8141.

[kroening]

I believe the reentrant lexer makes for cleaner code, but I acknowledge that we don't actually need that capability and it might just be seen as unnecessary code churn. So I am ok producing a (much simpler) variant of this PR that just introduces the additional safety check. Just let me know.

For reentrant lexing, we should consider generating C++ lexers, which would be possibly easier to understand.

The flex-generated C++ code seems to be sensible. However, attempts to have bison generate C++ have apparently been abandoned.

[tautschnig]

The changes in this PR are now limited to just guarding against attempts of reentrant parser use.

[martin-cs]

I'm a bit late to the party do the following exist or are there plans for them to exist?

• A maintained tool the produces JSIL.
• A documented process of how to use that tool with CBMC.

Because if not, I could suggest a much more radical PR which would also solve this problem. Last I spoke to Philippa I got the impression that she and her group had stopped working on this.

[tautschnig]

I'm a bit late to the party do the following exist or are there plans for them to exist?

* A maintained tool the produces JSIL.

* A documented process of how to use that tool with CBMC.

Because if not, I could suggest a much more radical PR which would also solve this problem. Last I spoke to Philippa I got the impression that she and her group had stopped working on this.

#8158