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 /src/parser | |
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 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 5 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 5 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 5 |
3 files changed, 12 insertions, 3 deletions
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" |