summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/main/getopt.cpp6
-rw-r--r--src/main/main.cpp14
-rw-r--r--src/main/usage.h2
-rw-r--r--src/parser/Makefile.am3
-rw-r--r--src/parser/memory_mapped_input_buffer.h78
-rw-r--r--src/parser/parser.cpp51
-rw-r--r--src/parser/parser.h13
-rw-r--r--src/util/options.h6
8 files changed, 137 insertions, 36 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 7ca889592..baad6fe31 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -67,6 +67,7 @@ enum OptionValue {
SEGV_NOSPIN,
PARSE_ONLY,
NO_CHECKING,
+ USE_MMAP,
SHOW_CONFIG
};/* enum OptionValue */
@@ -103,6 +104,7 @@ static struct option cmdlineOptions[] = {
{ "segv-nospin", no_argument , NULL, SEGV_NOSPIN },
{ "parse-only" , no_argument , NULL, PARSE_ONLY },
{ "no-checking", no_argument , NULL, NO_CHECKING },
+ { "mmap", no_argument , NULL, USE_MMAP },
{ "show-config", no_argument , NULL, SHOW_CONFIG }
};/* if you add things to the above, please remember to update usage.h! */
@@ -219,6 +221,10 @@ throw(OptionException) {
opts->semanticChecks = false;
break;
+ case USE_MMAP:
+ opts->memoryMap = true;
+ break;
+
case SHOW_CONFIG:
fputs(Configuration::about().c_str(), stdout);
printf("\n");
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 745fa30e9..2eea56947 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -142,10 +142,19 @@ int runCvc4(int argc, char *argv[]) {
// Create the parser
Parser* parser;
+ istream* input = NULL;
+
if(inputFromStdin) {
- parser = Parser::getNewParser(&exprMgr, options.lang, cin);
+ parser = Parser::getNewParser(&exprMgr, options.lang, cin, "<stdin>");
+ } else if( options.memoryMap ) {
+ parser = Parser::getMemoryMappedParser(&exprMgr, options.lang, argv[firstArgIndex]);
} else {
- parser = Parser::getNewParser(&exprMgr, options.lang, argv[firstArgIndex]);
+ string filename = argv[firstArgIndex];
+ input = new ifstream(filename.c_str());
+ if(input == NULL) {
+ throw Exception("file does not exist or is unreadable: " + filename);
+ }
+ parser = Parser::getNewParser(&exprMgr, options.lang, *input, filename);
}
if(!options.semanticChecks) {
@@ -163,6 +172,7 @@ int runCvc4(int argc, char *argv[]) {
// Remove the parser
delete parser;
+ delete input;
switch(lastResult.asSatisfiabilityResult().isSAT()) {
diff --git a/src/main/usage.h b/src/main/usage.h
index 6c44fef5a..3a609d2ec 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -37,6 +37,8 @@ CVC4 options:\n\
--stats give statistics on exit\n\
--segv-nospin (debug builds only) don't spin on segfault waiting for gdb\n\
--parse-only exit after parsing input\n\
+ --no-checking disable semantic checks in the parser\n\
+ --mmap memory map file input\n\
--show-config show CVC4 static configuration\n\
";
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 3ecde0169..5ac1c9e35 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -39,4 +39,5 @@ libcvc4parser_noinst_la_SOURCES = \
parser_exception.h \
symbol_table.h \
antlr_parser.h \
- antlr_parser.cpp
+ antlr_parser.cpp \
+ memory_mapped_input_buffer.h
diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h
new file mode 100644
index 000000000..c92e62524
--- /dev/null
+++ b/src/parser/memory_mapped_input_buffer.h
@@ -0,0 +1,78 @@
+/********************* */
+/** memory_mapped_input_buffer.cpp
+ ** Original author: cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** ANTLR input buffer from a memory-mapped file.
+ **/
+
+#ifndef MEMORY_MAPPED_INPUT_BUFFER_H_
+#define MEMORY_MAPPED_INPUT_BUFFER_H_
+
+#include <fcntl.h>
+#include <stdio.h>
+#include <stdint.h>
+
+#include <sys/errno.h>
+#include <sys/mman.h>
+#include <sys/stat.h>
+#include <antlr/InputBuffer.hpp>
+
+#include "util/Assert.h"
+#include "util/exception.h"
+
+namespace CVC4 {
+namespace parser {
+
+class MemoryMappedInputBuffer : public antlr::InputBuffer {
+
+public:
+ MemoryMappedInputBuffer(const std::string& filename) {
+ errno = 0;
+ struct stat st;
+ if( stat(filename.c_str(), &st) == -1 ) {
+ throw Exception("unable to stat() file");
+// throw Exception( "unable to stat() file " << filename << " errno " << errno );
+ }
+ d_size = st.st_size;
+
+ int fd = open(filename.c_str(), O_RDONLY);
+ if( fd == -1 ) {
+ throw Exception("unable to fopen() file");
+ }
+
+ d_start = static_cast< const char * >(
+ mmap( 0, d_size, PROT_READ, MAP_FILE | MAP_PRIVATE, fd, 0 ) );
+ errno = 0;
+ if( intptr_t( d_start ) == -1 ) {
+ throw Exception("unable to mmap() file");
+// throw Exception( "unable to mmap() file " << filename << " errno " << errno );
+ }
+ d_cur = d_start;
+ d_end = d_start + d_size;
+ }
+
+ ~MemoryMappedInputBuffer() {
+ munmap((void*)d_start,d_size);
+ }
+
+ inline int getChar() {
+ Assert( d_cur >= d_start && d_cur <= d_end );
+ return d_cur == d_end ? EOF : *d_cur++;
+ }
+
+private:
+ unsigned long int d_size;
+ const char *d_start, *d_end, *d_cur;
+};
+
+}
+}
+
+
+#endif /* MEMORY_MAPPED_INPUT_BUFFER_H_ */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 85b6c9865..852eda595 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -16,8 +16,10 @@
#include <iostream>
#include <fstream>
#include <antlr/CharScanner.hpp>
+#include <antlr/CharBuffer.hpp>
#include "parser.h"
+#include "memory_mapped_input_buffer.h"
#include "expr/command.h"
#include "util/output.h"
#include "util/Assert.h"
@@ -80,59 +82,56 @@ Expr Parser::parseNextExpression() throw (ParserException, AssertionException) {
Parser::~Parser() {
delete d_antlrParser;
delete d_antlrLexer;
- if(d_deleteInput) {
- delete d_input;
- }
+ delete d_inputBuffer;
}
-Parser::Parser(istream* input, AntlrParser* antlrParser,
- CharScanner* antlrLexer, bool deleteInput) :
- d_done(false), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer),
- d_input(input), d_deleteInput(deleteInput) {
+Parser::Parser(InputBuffer* inputBuffer, AntlrParser* antlrParser,
+ CharScanner* antlrLexer) :
+ d_done(false),
+ d_antlrParser(antlrParser),
+ d_antlrLexer(antlrLexer),
+ d_inputBuffer(inputBuffer) {
}
Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
- istream* input, string filename, bool deleteInput) {
+ InputBuffer* inputBuffer, string filename) {
AntlrParser* antlrParser = 0;
antlr::CharScanner* antlrLexer = 0;
switch(lang) {
case LANG_CVC4: {
- antlrLexer = new AntlrCvcLexer(*input);
- antlrLexer->setFilename(filename);
+ antlrLexer = new AntlrCvcLexer(*inputBuffer);
antlrParser = new AntlrCvcParser(*antlrLexer);
- antlrParser->setFilename(filename);
- antlrParser->setExpressionManager(em);
break;
}
case LANG_SMTLIB: {
- antlrLexer = new AntlrSmtLexer(*input);
- antlrLexer->setFilename(filename);
+// MemoryMappedInputBuffer inputBuffer(filename);
+// antlrLexer = new AntlrSmtLexer(inputBuffer);
+ antlrLexer = new AntlrSmtLexer(*inputBuffer);
antlrParser = new AntlrSmtParser(*antlrLexer);
- antlrParser->setFilename(filename);
- antlrParser->setExpressionManager(em);
break;
}
default:
Unhandled("Unknown Input language!");
}
- return new Parser(input, antlrParser, antlrLexer, deleteInput);
+ antlrLexer->setFilename(filename);
+ antlrParser->setFilename(filename);
+ antlrParser->setExpressionManager(em);
+
+ return new Parser(inputBuffer, antlrParser, antlrLexer);
}
-Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
- string filename) {
- istream* input = new ifstream(filename.c_str());
- if(!*input) {
- throw Exception("file does not exist or is unreadable: " + filename);
- }
- return getNewParser(em, lang, input, filename, true);
+Parser* Parser::getMemoryMappedParser(ExprManager* em, InputLanguage lang, string filename) {
+ MemoryMappedInputBuffer* inputBuffer = new MemoryMappedInputBuffer(filename);
+ return getNewParser(em,lang,inputBuffer,filename);
}
Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
- istream& input) {
- return getNewParser(em, lang, &input, "", false);
+ istream& input, string filename) {
+ antlr::CharBuffer* inputBuffer = new CharBuffer(input);
+ return getNewParser(em, lang, inputBuffer, filename);
}
void Parser::disableChecks() {
diff --git a/src/parser/parser.h b/src/parser/parser.h
index da2c630ca..d482b7907 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -25,6 +25,7 @@
namespace antlr {
class CharScanner;
+ class InputBuffer;
}
namespace CVC4 {
@@ -56,8 +57,8 @@ public:
LANG_AUTO
};
- static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::string filename);
- static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::istream& input);
+ static Parser* getMemoryMappedParser(ExprManager* em, InputLanguage lang, std::string filename);
+ static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::istream& input, std::string filename);
/**
* Destructor.
@@ -96,18 +97,18 @@ private:
* Create a new parser.
* @param em the expression manager to usee
* @param lang the language to parse
- * @param input the input stream to parse
+ * @param inputBuffer the input buffer to parse
* @param filename the filename to attach to the stream
* @param deleteInput wheather to delete the input
* @return the parser
*/
- static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::istream* input, std::string filename, bool deleteInput);
+ static Parser* getNewParser(ExprManager* em, InputLanguage lang, antlr::InputBuffer* inputBuffer, std::string filename);
/**
* Create a new parser given the actual antlr parser.
* @param antlrParser the antlr parser to user
*/
- Parser(std::istream* input, AntlrParser* antlrParser, antlr::CharScanner* antlrLexer, bool deleteInput);
+ Parser(antlr::InputBuffer* inputBuffer, AntlrParser* antlrParser, antlr::CharScanner* antlrLexer);
/** Sets the done flag */
void setDone(bool done = true);
@@ -122,7 +123,7 @@ private:
antlr::CharScanner* d_antlrLexer;
/** The input stream we are using */
- std::istream* d_input;
+ antlr::InputBuffer* d_inputBuffer;
/** Wherther to de-allocate the input */
bool d_deleteInput;
diff --git a/src/util/options.h b/src/util/options.h
index d2b19a20b..676dc0059 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -51,6 +51,9 @@ struct CVC4_PUBLIC Options {
/** Should the parser do semantic checks? */
bool semanticChecks;
+ /** Should the parser memory-map file input? */
+ bool memoryMap;
+
Options() : binary_name(),
smtcomp_mode(false),
statistics(false),
@@ -60,7 +63,8 @@ struct CVC4_PUBLIC Options {
lang(parser::Parser::LANG_AUTO),
d_cnfConversion(CVC4::CNF_VAR_INTRODUCTION),
parseOnly(false),
- semanticChecks(true)
+ semanticChecks(true),
+ memoryMap(false)
{}
};/* struct Options */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback