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. --- Makefile | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 369fd4cd..1e578006 100644 --- a/Makefile +++ b/Makefile @@ -23,9 +23,10 @@ endif DIRS=lib common $(ARCHDIRS) backend cfrontend driver \ flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \ - exportclight cparser cparser/MenhirLib + exportclight MenhirLib cparser -RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight cparser +RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ + MenhirLib cparser COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) @@ -103,16 +104,16 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \ Cshmgen.v Cshmgenproof.v \ Csharpminor.v Cminorgen.v Cminorgenproof.v -# LR(1) parser validator - -PARSERVALIDATOR=Alphabet.v Interpreter_complete.v Interpreter.v \ - Validator_complete.v Automaton.v Interpreter_correct.v Main.v \ - Validator_safe.v Grammar.v Interpreter_safe.v Tuples.v - # Parser PARSER=Cabs.v Parser.v +# MenhirLib + +MENHIRLIB=Alphabet.v Automaton.v Grammar.v Interpreter_complete.v \ + Interpreter_correct.v Interpreter.v Main.v Validator_complete.v \ + Validator_safe.v Validator_classes.v + # Putting everything together (in driver/) DRIVER=Compopts.v Compiler.v Complements.v @@ -120,7 +121,7 @@ DRIVER=Compopts.v Compiler.v Complements.v # All source files FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ - $(PARSERVALIDATOR) $(PARSER) + $(MENHIRLIB) $(PARSER) # Generated source files @@ -141,7 +142,6 @@ ifeq ($(CLIGHTGEN),true) $(MAKE) clightgen endif - proof: $(FILES:.v=.vo) # Turn off some warnings for compiling Flocq @@ -225,7 +225,7 @@ driver/Version.ml: VERSION cparser/Parser.v: cparser/Parser.vy @rm -f $@ - $(MENHIR) $(MENHIR_FLAGS) --coq cparser/Parser.vy + $(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy @chmod a-w $@ depend: $(GENERATED) depend1 -- cgit From d08b080747225160b80c3f04bdfd9cd67550b425 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 2 Jul 2019 16:25:40 +0200 Subject: Give formal semantics to some built-in functions and run-time functions This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 1e578006..ae19225a 100644 --- a/Makefile +++ b/Makefile @@ -63,7 +63,7 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ COMMON=Errors.v AST.v Linking.v \ Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \ Values.v Smallstep.v Behaviors.v Switch.v Determinism.v Unityping.v \ - Separation.v + Separation.v Builtins0.v Builtins1.v Builtins.v # Back-end modules (in backend/, $(ARCH)/) -- cgit