Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow conditio...

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.

diff --git a/Makefile b/Makefile
index 8a6d8060768853a7cf166606c3bb902ca863c9eb..7f0dc916da4c9ce241437531219d152d1482994b 100644 (file)
--- 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 18b2eff733000d0fdc0545fde64769754f210d64..674feaed68640147d8054586e7ebfb0d317323a9 100644 (file)
--- 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 <http://www.antlr.org/>.]
     )
+    ANTLR_VERSION=
+  else
+    ANTLR_VERSION="`$ANTLR -version 2>&1 | sed 's,.*\<Version  *\([[0-9.]]*\).*,\1,'`"
+    case "$ANTLR_VERSION" in
+      3.2|3.2.*) ANTLR_VERSION=3.2 ;;
+      3.4|3.4.*) ANTLR_VERSION=3.4 ;;
+      *) AC_MSG_WARN([unknown version of antlr: $ANTLR_VERSION]);;
+    esac
   fi
 ])
 
@@ -94,6 +102,9 @@ AC_DEFUN([AC_LIB_ANTLR],[
     ])],
     [
       AC_MSG_RESULT([found it (must be antlr3 3.2 or similar)])
+      if test -n "$ANTLR_VERSION" -a "$ANTLR_VERSION" != 3.2; then
+        AC_MSG_WARN([your antlr parser generator is version $ANTLR_VERSION, which doesn't match the library!])
+      fi
       CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ANTLR3_OLD_INPUT_STREAM"
     ],
         [
@@ -111,6 +122,9 @@ AC_DEFUN([AC_LIB_ANTLR],[
             ])],
             [
               AC_MSG_RESULT([found it (must be antlr3 3.4 or similar)])
+              if test -n "$ANTLR_VERSION" -a "$ANTLR_VERSION" != 3.4; then
+                AC_MSG_WARN([your antlr parser generator is version $ANTLR_VERSION, which doesn't match the library!])
+              fi
             ],
                 [
                   AC_MSG_ERROR([cannot figure out how to create an antlr3 input stream, bailing..])

diff --git a/contrib/Makefile.am b/contrib/Makefile.am
index 1439a11172d991838acc34863901b3a038e34512..815c3377d913cc8855b647f73a88795f39a72be6 100644 (file)
--- a/contrib/Makefile.am
+++ b/contrib/Makefile.am
@@ -10,6 +10,7 @@ EXTRA_DIST = \
        new-theory \
        configure-in-place \
        depgraph \
+       get-antlr-3.4 \
        theoryskel/kinds \
        theoryskel/Makefile \
        theoryskel/Makefile.am \

diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
new file mode 100755 (executable)
index 0000000..c521147
--- /dev/null
+++ b/contrib/get-antlr-3.4
@@ -0,0 +1,47 @@
+#!/bin/bash
+#
+set -e
+
+cd "$(dirname "$0")/.."
+
+if ! [ -e src/parser/cvc/Cvc.g ]; then
+  echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&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 <<EOF
+#!/bin/sh
+export CLASSPATH=/usr/share/java/stringtemplate.jar:`pwd`/share/java/antlr-3.4-complete.jar:\$CLASSPATH
+exec java org.antlr.Tool "\$@"
+EOF
+chmod a+x bin/antlr3
+cd src
+tar xfzv libantlr3c-3.4.tar.gz
+cd libantlr3c-3.4
+./configure --enable-64bit --prefix=`pwd`/../..
+cp Makefile Makefile.orig
+sed 's,^CFLAGS = .*,\0 -fexceptions,' Makefile.orig > 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 042a8ef1d403397c47ade4da10327d86af96cf77..00072d6d9fbb47b1b626232b0a7987e4df712692 100644 (file)
--- 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 c1c3f699bcfc8715276bcaf2422573d5c5838cbe..1908d3e90fe32e39e7ce4ba421cab47cc45c7ef2 100644 (file)
--- 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 2988ae4ef7ac9075864cfe64f29196e199c49332..21f82f6388c5805f0efcf6158ced73e1d3e36648 100644 (file)
--- 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 568f3bb92ad6d448c51a178a97999363120edeed..9f1f458c95f72b6a65d9b9321c88fcb9d3a4de62 100644 (file)
--- 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 59b6715b9d46a801e63b5c38634875bcee395c63..07998b58f700717df2fc284b14e33de006059894 100644 (file)
--- 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"