From 4b3ce37b3d5245d8827d04e4f459c32631083613 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 13 Jun 2012 19:50:35 +0000 Subject: [PATCH] Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow condition when reading from stdin. This should completely resolve bug #319. However, on large inputs especially (like the stp/testcase benchmarks), this inlining feature can speed parsing by 5-10%, at the cost of not supporting interactive sessions on stdin (like in the SMT-COMP application track). So I updated the submission script and competition build so that * a competition build with antlr-inlining is built for the main and parallel tracks * a competition build without antlr-inlining is built for the application track Again, the effect is only when reading the stdin stream (but that's how SMT-COMP works). For normal (non-competition) builds, we need to support interactive sessions (from e.g. KIND) on stdin, so this inlining is off for all builds except main- and parallel-track competition builds. Also added a "get-antlr-3.4" script that automatically downloads and locally installs a copy of libantlr3c and the antlr parser generator inside the CVC4 source tree. Closing bug #319. --- Makefile | 15 ++++++++++- config/antlr.m4 | 14 +++++++++++ contrib/Makefile.am | 1 + contrib/get-antlr-3.4 | 47 +++++++++++++++++++++++++++++++++++ src/main/driver.cpp | 8 ++++-- src/main/driver_portfolio.cpp | 8 ++++-- src/parser/cvc/Cvc.g | 5 +++- src/parser/smt/Smt.g | 5 +++- src/parser/smt2/Smt2.g | 5 +++- 9 files changed, 100 insertions(+), 8 deletions(-) create mode 100755 contrib/get-antlr-3.4 diff --git a/Makefile b/Makefile index 8a6d80607..7f0dc916d 100644 --- a/Makefile +++ b/Makefile @@ -43,6 +43,12 @@ examples: all YEAR := $(shell date +%Y) submission: + @if [ -n "`ls src/parser/*/generated`" ]; then \ + echo 'ERROR:' >&2; \ + echo 'ERROR: Please make maintainer-clean first.' >&2; \ + echo 'ERROR:' >&2; \ + exit 1; \ + fi if [ ! -e configure ]; then ./autogen.sh; fi ./configure competition --disable-shared --enable-static-binary --with-cln --with-portfolio $(MAKE) @@ -64,7 +70,14 @@ submission: echo 'exec ./pcvc4 -L smt2 --no-interactive' ) > cvc4-parallel-smtcomp-$(YEAR)/run chmod 755 cvc4-parallel-smtcomp-$(YEAR)/run tar cf cvc4-parallel-smtcomp-$(YEAR).tar cvc4-parallel-smtcomp-$(YEAR) - # application track + # application track is a separate build + make maintainer-clean + if [ ! -e configure ]; then ./autogen.sh; fi + ./configure competition --disable-shared --enable-static-binary --with-cln CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK + $(MAKE) + strip builds/bin/cvc4 + $(MAKE) regress1 + # package the application track tarball mkdir -p cvc4-application-smtcomp-$(YEAR) cp -p builds/bin/cvc4 cvc4-application-smtcomp-$(YEAR)/cvc4 ( echo '#!/bin/sh'; \ diff --git a/config/antlr.m4 b/config/antlr.m4 index 18b2eff73..674feaed6 100644 --- a/config/antlr.m4 +++ b/config/antlr.m4 @@ -25,6 +25,14 @@ AC_DEFUN([AC_PROG_ANTLR], [ [No usable antlr3 script found. Make sure that the parser code has been generated already. To obtain ANTLR see .] ) + ANTLR_VERSION= + else + ANTLR_VERSION="`$ANTLR -version 2>&1 | sed 's,.*\&2 + echo "but apparently:" >&2 + echo >&2 + echo " $(pwd)" >&2 + echo >&2 + echo "is not a CVC4 source tree ?!" >&2 + exit 1 +fi + +set -x +mkdir -p antlr-3.4/share/java +mkdir -p antlr-3.4/bin +mkdir -p antlr-3.4/src +cd antlr-3.4 +wget -c -O share/java/antlr-3.4-complete.jar http://antlr.org/download/antlr-3.4-complete.jar +wget -c -O src/libantlr3c-3.4.tar.gz http://antlr.org/download/C/libantlr3c-3.4.tar.gz +tee bin/antlr3 < Makefile +make +make install +set +x +cd ../../.. + +echo +echo Invalidating generated parsers.. +touch src/parser/*/*.g + +echo +echo ===================== Now configure CVC4 with ===================== +echo ./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3 diff --git a/src/main/driver.cpp b/src/main/driver.cpp index 042a8ef1d..00072d6d9 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -115,7 +115,7 @@ int runCvc4(int argc, char* argv[], Options& options) { // If in competition mode, set output stream option to flush immediately #ifdef CVC4_COMPETITION_MODE *options.out << unitbuf; -#endif +#endif /* CVC4_COMPETITION_MODE */ // We only accept one input file if(argc > firstArgIndex + 1) { @@ -268,7 +268,11 @@ int runCvc4(int argc, char* argv[], Options& options) { ParserBuilder parserBuilder(&exprMgr, filename, options); if( inputFromStdin ) { +#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) + parserBuilder.withStreamInput(cin); +#else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ parserBuilder.withLineBufferedStreamInput(cin); +#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ } Parser *parser = parserBuilder.build(); @@ -311,7 +315,7 @@ int runCvc4(int argc, char* argv[], Options& options) { // exit, don't return // (don't want destructors to run) exit(returnValue); -#endif +#endif /* CVC4_COMPETITION_MODE */ ReferenceStat< Result > s_statSatResult("sat/unsat", result); RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult); diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp index c1c3f699b..1908d3e90 100644 --- a/src/main/driver_portfolio.cpp +++ b/src/main/driver_portfolio.cpp @@ -232,7 +232,7 @@ int runCvc4(int argc, char *argv[], Options& options) { // If in competition mode, set output stream option to flush immediately #ifdef CVC4_COMPETITION_MODE *options.out << unitbuf; -#endif +#endif /* CVC4_COMPETITION_MODE */ // We only accept one input file if(argc > firstArgIndex + 1) { @@ -429,7 +429,11 @@ int runCvc4(int argc, char *argv[], Options& options) { withOptions(options); if( inputFromStdin ) { +#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) + parserBuilder.withStreamInput(cin); +#else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ parserBuilder.withLineBufferedStreamInput(cin); +#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ } Parser *parser = parserBuilder.build(); @@ -567,7 +571,7 @@ int runCvc4(int argc, char *argv[], Options& options) { // exit, don't return // (don't want destructors to run) exit(returnValue); -#endif +#endif /* CVC4_COMPETITION_MODE */ // ReferenceStat< Result > s_statSatResult("sat/unsat", result); // RegisterStatistic statSatResultReg(*exprMgr, &s_statSatResult); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 2988ae4ef..21f82f638 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -430,12 +430,15 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { * the lexer headers for two grammars AND (b) uses the token symbol definitions. */ #pragma GCC system_header +#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) /* This improves performance by ~10 percent on big inputs. * This option is only valid if we know the input is ASCII (or some 8-bit encoding). * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. * Otherwise, we have to let the lexer detect the encoding at runtime. */ -#define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_8BIT +#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ #include "parser/antlr_tracing.h" #include "util/integer.h" diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 568f3bb92..9f1f458c9 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -50,12 +50,15 @@ options { */ #pragma GCC system_header +#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) /* This improves performance by ~10 percent on big inputs. * This option is only valid if we know the input is ASCII (or some 8-bit encoding). * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. * Otherwise, we have to let the lexer detect the encoding at runtime. */ -#define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_8BIT +#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ #include "parser/antlr_tracing.h" }/* @lexer::includes */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 59b6715b9..07998b58f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -51,12 +51,15 @@ options { */ #pragma GCC system_header +#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) /* This improves performance by ~10 percent on big inputs. * This option is only valid if we know the input is ASCII (or some 8-bit encoding). * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. * Otherwise, we have to let the lexer detect the encoding at runtime. */ -#define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_8BIT +#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ #include "parser/antlr_tracing.h" -- 2.30.2