From 998f3c5ff90f6230b722b6094761f5989beea0a5 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Fri, 5 Jul 2019 15:15:42 +0200 Subject: New parser based on new version of the Coq backend of Menhir (#276) What's new: 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. The corresponding changes in Menhir have been released as part of version 20190626. 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. --- cparser/Parser.vy | 595 ++++++++++++++++++++++++++++-------------------------- 1 file changed, 306 insertions(+), 289 deletions(-) (limited to 'cparser/Parser.vy') diff --git a/cparser/Parser.vy b/cparser/Parser.vy index 79e3793d..03bfa590 100644 --- a/cparser/Parser.vy +++ b/cparser/Parser.vy @@ -15,96 +15,99 @@ %{ -Require Import Cabs. Require Import List. +Require Cabs. %} -%token VAR_NAME TYPEDEF_NAME OTHER_NAME -%token PRAGMA -%token STRING_LITERAL -%token CONSTANT -%token SIZEOF PTR INC DEC LEFT RIGHT LEQ GEQ EQEQ EQ NEQ LT GT +%token VAR_NAME TYPEDEF_NAME OTHER_NAME +%token PRAGMA +%token STRING_LITERAL +%token CONSTANT +%token SIZEOF PTR INC DEC LEFT RIGHT LEQ GEQ EQEQ EQ NEQ LT GT ANDAND BARBAR PLUS MINUS STAR TILDE BANG SLASH PERCENT HAT BAR QUESTION COLON AND ALIGNOF -%token MUL_ASSIGN DIV_ASSIGN MOD_ASSIGN ADD_ASSIGN SUB_ASSIGN +%token MUL_ASSIGN DIV_ASSIGN MOD_ASSIGN ADD_ASSIGN SUB_ASSIGN LEFT_ASSIGN RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN -%token LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA - SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE NORETURN - CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE CONST VOLATILE VOID +%token LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA + SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE + NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE CONST VOLATILE VOID STRUCT UNION ENUM UNDERSCORE_BOOL PACKED ALIGNAS ATTRIBUTE ASM -%token CASE DEFAULT IF ELSE SWITCH WHILE DO FOR GOTO CONTINUE BREAK +%token CASE DEFAULT IF_ ELSE SWITCH WHILE DO FOR GOTO CONTINUE BREAK RETURN BUILTIN_VA_ARG BUILTIN_OFFSETOF %token EOF -%type primary_expression postfix_expression +%type primary_expression postfix_expression unary_expression cast_expression multiplicative_expression additive_expression shift_expression relational_expression equality_expression AND_expression exclusive_OR_expression inclusive_OR_expression logical_AND_expression logical_OR_expression conditional_expression assignment_expression constant_expression expression -%type unary_operator -%type assignment_operator -%type argument_expression_list -%type declaration -%type declaration_specifiers -%type declaration_specifiers_typespec_opt -%type init_declarator_list -%type init_declarator -%type storage_class_specifier -%type type_specifier struct_or_union_specifier enum_specifier -%type struct_or_union -%type struct_declaration_list -%type struct_declaration -%type specifier_qualifier_list -%type struct_declarator_list -%type