New parser based on new version of the Coq backend of Menhir #276

jhjourdan · 2019-02-26T07:46:23Z

This is the new version of the parser, based on recent updates of Menhir.

The corresponding changes in Menhir are not yet released: to test these changes, you should install the current master branch of Menhir. This is the reason why this PR is marked WIP. But apart from that (and updating configure), I think this PR is ready.

Changes include:

A rewrite of the Coq interpreter of Menhir automaton, with dependent types removing the need for runtime checks for the well-formedness of the LR stack. This seem to cause some speedup on the parsing time (~10% for lexing + parsing).
Thanks to 1., I was able to no longer use int31 for comparing symbols: Since this is only used for validation, positives are enough.
Speedup of Validation: on my machine, the time needed for compiling Parser.v goes from about 2 minutes to about 1 minute. I am not sure of the actual reason for this, but this seem to be related to a performance bug I detected in the completeness validator and to the use of positive instead of int31 (I used to use a weird hack for representing int31 constants for making sure they were evaluated efficiently after extraction... but this could actually be rather slow when executed with vm_compute).
Menhir now generates a dedicated inductive type for (semantic-value-carrying) tokens (in addition to the already existing inductive type for (non-semantic-value-carrying) terminals. The end result is that the OCaml support code for the parser no longer contain calls to Obj.magic. The bad side of this change is that the formal specification of the parser is perhaps harder to read.
The parser and its library are now free of axioms (I used to use axiom K and proof irrelevance for easing proofs involving dependent types).

jhjourdan · 2019-02-26T07:52:16Z

Note that I also updated the LICENSE file, reflecting that coq-menhirlib is under LGPLv3 (like Flocq), and that I moved it to the root of the repository.

xavierleroy · 2019-03-11T18:59:01Z

What about the use of streams? Cf. #231 . Will these changes to Menhir and its supporting library remove dependencies on the Stream library from Coq?

jhjourdan · 2019-03-11T21:17:35Z

You are right, I forgot about this. I need a bit more work to get rid of the Stream dependency.

jhjourdan · 2019-03-13T12:36:51Z

What about the use of streams? Cf. #231 . Will these changes to Menhir and its supporting library remove dependencies on the Stream library from Coq?

The dependency to the Stream library of Coq is now removed, Menhir now uses its own type for input buffer. This type is a negative coinductive type, so that it should not be affected by coq/coq#7536.

jhjourdan · 2019-03-21T15:03:05Z

I added another change: the fuel parameter is now specified using the logarithm (in base 2) of the maximum number of steps needed. In practice, we use the value 50, so that we are sure that we will not run out of fuel in reasonable computation time. From the perspective of CompCert, the advantage is that this prevents us from using the let rec inf = S inf hack.

xavierleroy

I didn't review everything line-by-line, but played with the branch, reviewed some of the diff, and had a look at some of the generated / extracted files.

Globally this looks fine to me. I'm very happy to see int31 gone. The cleaner and better typed interface with the handwritten OCaml code is welcome. I didn't see much difference in parsing time, but that's OK. I confirm that Parser.v now takes half as much time to check through Coq.

Below, a few cosmetic comments about the new Parser.vy, but nothing important.

I guess the next step is for you @jhjourdan and @fpottier to declare the Menhir side of things stable and make a Menhir release.

xavierleroy · 2019-03-27T15:01:35Z

configure

-        missingtools=true;;
-esac
+# TODO
+menhir_includes="-I `menhir --suggest-menhirLib`"


Remind me to fill in something there before I merge :-)

cparser/Lexer.mll

cparser/Parser.vy

The corresponding changes in Menhir have been released as part of version 20190613. The `MenhirLib` directory is identical to the content of the `src` directory of the corresponding `coq-menhirlib` opam package except that: - In order to try to make CompCert compatible with several Menhir versions without updates, we do not check the version of menhir is compatible with the version of coq-menhirlib. Hence the `Version.v` file is not present in CompCert's copy. - Build-system related files have been removed. More precisely, changes include: 1. A rewrite of the Coq interpreter of Menhir automaton, with dependent types removing the need for runtime checks for the well-formedness of the LR stack. This seem to cause some speedup on the parsing time (~10% for lexing + parsing). 2. Thanks to 1., it is now possible to avoid the use of int31 for comparing symbols: Since this is only used for validation, positives are enough. 3. Speedup of Validation: on my machine, the time needed for compiling Parser.v goes from about 2 minutes to about 1 minute. This seem to be related to a performance bug in the completeness validator and to the use of positive instead of int31. 3. Menhir now generates a dedicated inductive type for (semantic-value-carrying) tokens (in addition to the already existing inductive type for (non-semantic-value-carrying) terminals. The end result is that the OCaml support code for the parser no longer contain calls to Obj.magic. The bad side of this change is that the formal specification of the parser is perhaps harder to read. 4. The parser and its library are now free of axioms (I used to use axiom K and proof irrelevance for easing proofs involving dependent types). 5. Use of a dedicated custom negative coinductive type for the input stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a positive coinductive type, which are now deprecated by Coq. 6. The fuel of the parser is now specified using its logarithm instead of its actual value. This makes it possible to give large fuel values instead of using the `let rec fuel = S fuel` hack. 7. Some refactoring in the lexer, the parser and the Cabs syntax tree.

jhjourdan · 2019-06-18T08:27:04Z

The corresponding version of Menhir (20190613) have been released, I rebased/squashed the commits, and tested the whole thing.

As far as I can tell, this is now ready to merge.

xavierleroy · 2019-06-21T14:00:12Z

Thank you. I'm preparing the CI machines here at Inria so that they can test this new version.

xavierleroy · 2019-06-21T15:00:00Z

With Coq 8.7.2 under Cygwin, I get

16:54:35 File "./MenhirLib/Validator_complete.v", line 232, characters 6-62:
16:54:35 Error:
16:54:35 Anomaly
16:54:35 "File "plugins/ltac/tacinterp.ml", line 1157, characters 35-41: Assertion failed."

Will try other Coq versions.

jhjourdan · 2019-06-21T15:23:23Z

Thanks for the test. Let me look into this more in detail.

xavierleroy · 2019-06-21T17:29:13Z

After upgrading to Coq 8.9.1, still under Cygwin, I now get

COQC cparser/Parser.v
File "./cparser/Parser.v", line 217, characters 20-2939:
Error:
In environment
x : terminal
The term
 "match x with
  | ADD_ASSIGN't => 1
  | ALIGNAS't => 2
[...]
end" has type "nat" while it is expected to have type
"positive".

Coq 8.8.2 under Linux works fine, though.

I'll investigate on my side too.

jhjourdan · 2019-06-21T22:55:44Z

The compatibility issue with 8.7.2 is now fixed in this branch (and in upstream Menhir).

The compatibility issue with 8.9.1 required a change in Menhir itself (in the generator, not in the support library). The fix will be shipped with the next Menhir release:

https://gitlab.inria.fr/fpottier/menhir/commit/5f195649fda98fda58c83e4ce956b41a0db4fec6

I hope @fpottier will not mind too much doing yet another Menhir release :D Thanks, @fpottier!

jhjourdan · 2019-06-21T22:58:17Z

And sorry for still being a young Padawan too naive about compatibility between Cod versions! I should have checked that.

fpottier · 2019-06-24T08:40:18Z

I'll be happy to make a new release (now that the release scripts work again, it is reasonably easy).

@jhjourdan, could you modify the opam descriptions of the two versions that we have released already (20190613 and 20190620) so as to document their compatibility constraints? This will avoid problems if someone installs one of these versions. Thanks!

jhjourdan · 2019-07-01T22:08:45Z

This PR should now be fixed for both Coq 8.7 and Coq 8.9.

xavierleroy · 2019-07-05T13:14:09Z

The tests are OK, and we agreed to merge, so let's merge!

Thanks for all the hard work.

jhjourdan force-pushed the newparser branch from 0d80f98 to 0ae5901 Compare March 13, 2019 12:30

xavierleroy reviewed Mar 27, 2019

View reviewed changes

jhjourdan force-pushed the newparser branch from 3e97749 to fb4b653 Compare March 27, 2019 20:22

jhjourdan force-pushed the newparser branch 2 times, most recently from ab6338d to 4086284 Compare June 18, 2019 07:59

jhjourdan force-pushed the newparser branch from 4086284 to c29ae9d Compare June 18, 2019 08:24

jhjourdan changed the title ~~WIP : New parser based on new version of the Coq backend of Menhir~~ New parser based on new version of the Coq backend of Menhir Jun 18, 2019

New parser: fix compatibility with Coq 8.7.2.

cbf936a

Change MENHIR_REQUIRED for compatibility with Coq 8.9.

6872d33

jhjourdan mentioned this pull request Jul 3, 2019

Fix max menhir version for compcert.dev coq/opam#816

Merged

xavierleroy merged commit 998f3c5 into AbsInt:master Jul 5, 2019

xavierleroy mentioned this pull request Jul 8, 2019

Backporting the legacy Coq Stream library. #231

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New parser based on new version of the Coq backend of Menhir #276

New parser based on new version of the Coq backend of Menhir #276

jhjourdan commented Feb 26, 2019 •

edited

Loading

jhjourdan commented Feb 26, 2019

xavierleroy commented Mar 11, 2019

jhjourdan commented Mar 11, 2019

jhjourdan commented Mar 13, 2019

jhjourdan commented Mar 21, 2019

xavierleroy left a comment

xavierleroy Mar 27, 2019

jhjourdan commented Jun 18, 2019

xavierleroy commented Jun 21, 2019

xavierleroy commented Jun 21, 2019

jhjourdan commented Jun 21, 2019

xavierleroy commented Jun 21, 2019

jhjourdan commented Jun 21, 2019

jhjourdan commented Jun 21, 2019

fpottier commented Jun 24, 2019

jhjourdan commented Jul 1, 2019

xavierleroy commented Jul 5, 2019

New parser based on new version of the Coq backend of Menhir #276

New parser based on new version of the Coq backend of Menhir #276

Conversation

jhjourdan commented Feb 26, 2019 • edited Loading

jhjourdan commented Feb 26, 2019

xavierleroy commented Mar 11, 2019

jhjourdan commented Mar 11, 2019

jhjourdan commented Mar 13, 2019

jhjourdan commented Mar 21, 2019

xavierleroy left a comment

Choose a reason for hiding this comment

xavierleroy Mar 27, 2019

Choose a reason for hiding this comment

jhjourdan commented Jun 18, 2019

xavierleroy commented Jun 21, 2019

xavierleroy commented Jun 21, 2019

jhjourdan commented Jun 21, 2019

xavierleroy commented Jun 21, 2019

jhjourdan commented Jun 21, 2019

jhjourdan commented Jun 21, 2019

fpottier commented Jun 24, 2019

jhjourdan commented Jul 1, 2019

xavierleroy commented Jul 5, 2019

jhjourdan commented Feb 26, 2019 •

edited

Loading