json_parsert: construct with message handler

[tautschnig]

This both avoids an object of static lifetime as well as it fixes the (transitive) use of the deprecated messaget() constructor.

• Each commit message has a non-empty body, explaining why the change was made.
• 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.

[kroening]

The removal of the static object may create expectations that won't be met -- you can still only have one parser, given the state in the scanner.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (6438259) 79.09% compared to head (63e5910) 79.09%.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8137   +/-   ##
========================================
  Coverage    79.09%   79.09%           
========================================
  Files         1695     1695           
  Lines       196578   196583    +5     
========================================
+ Hits        155488   155493    +5     
  Misses       41090    41090           

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

[tautschnig]

The removal of the static object may create expectations that won't be met -- you can still only have one parser, given the state in the scanner.

Wouldn't the PRECONDITION in yyjsonlex(json_parsert &_json_parser) take care of these (misguided) expectations? We could also make the scanner reentrant, it would just require a bit of patching-up of the generated scanner implementation (yy_get_next_buffer would need to take a parameter, and for those scanners that have %option noinput this even is just a matter of not using YY_INPUT in the way we define it in src/util/parser.h at the moment).

[kroening]

Wouldn't the PRECONDITION in yyjsonlex(json_parsert &_json_parser) take care of these (misguided) expectations?

I don't seem to find that?

But yes, if we add such a PRECONDITION, it would be good to remove the static object.

[tautschnig]

Wouldn't the PRECONDITION in yyjsonlex(json_parsert &_json_parser) take care of these (misguided) expectations?

I don't seem to find that?

But yes, if we add such a PRECONDITION, it would be good to remove the static object.

Line 43 of json/scanner.l is what I am referring to.

[kroening]

Line 43 of json/scanner.l is what I am referring to.

Apologies, I looked at the current version, not the diff.

Yes, that precondition does the job.

[kroening]

Line 43 of json/scanner.l is what I am referring to.

Apologies, I looked at the current version, not the diff.

Yes, that precondition does the job.

Apologies, I think I want to take that back. I am afraid the precondition is too weak. Those scanners maintain internal state between calls to yylex, and the precondition wouldn't catch a user trying to simultaneously tokenise two files.

[kroening]

A solution would be to do that sort of check in the constructor of the parser object.

[tautschnig]

Apologies, I think I want to take that back. I am afraid the precondition is too weak. Those scanners maintain internal state between calls to yylex, and the precondition wouldn't catch a user trying to simultaneously tokenise two files.

I have now chosen to use Flex' support for reentrant scanners, making both the parser and the scanner reentrant. Pending completion of CI to make sure this is supported on all platforms.