diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-27 18:34:44 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-27 18:34:44 +0000 |
commit | e56c41f47d43103a6e8bf744e12229ed6e5a8f19 (patch) | |
tree | 39be4124610edf8072206aa85b178b8fe3eab2e2 /src/parser/memory_mapped_input_buffer.h | |
parent | 14c22833d05f632eb40eb68cc3c68345d891005c (diff) |
Adding --mmap option to use memory-mapped file input, which provides a marginal improvement (<5%) on big benchmarks.
Diffstat (limited to 'src/parser/memory_mapped_input_buffer.h')
-rw-r--r-- | src/parser/memory_mapped_input_buffer.h | 78 |
1 files changed, 78 insertions, 0 deletions
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_ */ |