diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-06-13 19:50:35 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-06-13 19:50:35 +0000 |
| commit | 4b3ce37b3d5245d8827d04e4f459c32631083613 (patch) | |
| tree | 61a4ab0e9c0d39656b02f668bfed4217b088ecb0 /contrib | |
| parent | 0f0f135f98372e32dafb0e70aa918f92b57ae8c7 (diff) | |
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.
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/Makefile.am | 1 | ||||
| -rwxr-xr-x | contrib/get-antlr-3.4 | 47 |
2 files changed, 48 insertions, 0 deletions
diff --git a/contrib/Makefile.am b/contrib/Makefile.am index 1439a1117..815c3377d 100644 --- 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 index 000000000..c5211474a --- /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 |