From: Christopher L. Conway Date: Sat, 27 Feb 2010 18:34:44 +0000 (+0000) Subject: Adding --mmap option to use memory-mapped file input, which provides a marginal impro... X-Git-Tag: cvc5-1.0.0~9215 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e56c41f47d43103a6e8bf744e12229ed6e5a8f19;p=cvc5.git Adding --mmap option to use memory-mapped file input, which provides a marginal improvement (<5%) on big benchmarks. --- 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, ""); + } 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 +#include +#include + +#include +#include +#include +#include + +#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 #include #include +#include #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 */