1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andres Noetzli, Mathias Preiner, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* The LineBuffer class stores lines from an input stream |
14 |
|
* |
15 |
|
* Each line is guaranteed to be consecutive in memory. The content in |
16 |
|
* the line buffer can be addressed using line number and the position |
17 |
|
* |
18 |
|
* For each line, the class allocates a separate buffer. |
19 |
|
*/ |
20 |
|
|
21 |
|
#include "parser/line_buffer.h" |
22 |
|
|
23 |
|
#include <cstring> |
24 |
|
#include <iostream> |
25 |
|
#include <string> |
26 |
|
|
27 |
|
#include "base/check.h" |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace parser { |
31 |
|
|
32 |
4 |
LineBuffer::LineBuffer(std::istream* stream) : d_stream(stream) {} |
33 |
|
|
34 |
8 |
LineBuffer::~LineBuffer() { |
35 |
10 |
for (size_t i = 0; i < d_lines.size(); i++) { |
36 |
6 |
delete[] d_lines[i]; |
37 |
|
} |
38 |
4 |
} |
39 |
|
|
40 |
42 |
uint8_t* LineBuffer::getPtr(size_t line, size_t pos_in_line) { |
41 |
42 |
if (!readToLine(line)) { |
42 |
8 |
return NULL; |
43 |
|
} |
44 |
34 |
Assert(pos_in_line < d_sizes[line]); |
45 |
34 |
return d_lines[line] + pos_in_line; |
46 |
|
} |
47 |
|
|
48 |
54 |
uint8_t* LineBuffer::getPtrWithOffset(size_t line, size_t pos_in_line, |
49 |
|
size_t offset) { |
50 |
54 |
if (!readToLine(line)) { |
51 |
8 |
return NULL; |
52 |
|
} |
53 |
46 |
if (pos_in_line + offset >= d_sizes[line]) { |
54 |
|
return getPtrWithOffset(line + 1, 0, |
55 |
|
offset - (d_sizes[line] - pos_in_line - 1)); |
56 |
|
} |
57 |
46 |
Assert(pos_in_line + offset < d_sizes[line]); |
58 |
46 |
return d_lines[line] + pos_in_line + offset; |
59 |
|
} |
60 |
|
|
61 |
|
bool LineBuffer::isPtrBefore(uint8_t* ptr, size_t line, size_t pos_in_line) { |
62 |
|
for (size_t j = 0; j < line; j++) |
63 |
|
{ |
64 |
|
// NOTE: std::less is guaranteed to give consistent results when comparing |
65 |
|
// pointers of different arrays (in contrast to built-in comparison |
66 |
|
// operators). |
67 |
|
size_t i = line - j; |
68 |
|
uint8_t* end = d_lines[i] + ((i == line) ? pos_in_line : d_sizes[i]); |
69 |
|
if (std::less<uint8_t*>()(d_lines[i] - 1, ptr) && |
70 |
|
std::less<uint8_t*>()(ptr, end)) { |
71 |
|
return true; |
72 |
|
} |
73 |
|
} |
74 |
|
return false; |
75 |
|
} |
76 |
|
|
77 |
102 |
bool LineBuffer::readToLine(size_t line_size) |
78 |
|
{ |
79 |
108 |
while (line_size >= d_lines.size()) |
80 |
|
{ |
81 |
22 |
if (!(*d_stream)) { |
82 |
16 |
return false; |
83 |
|
} |
84 |
|
|
85 |
12 |
std::string line; |
86 |
6 |
std::getline(*d_stream, line); |
87 |
6 |
uint8_t* segment = new uint8_t[line.size() + 1]; |
88 |
6 |
std::memcpy(segment, line.c_str(), line.size()); |
89 |
6 |
segment[line.size()] = LineBuffer::NewLineChar; |
90 |
6 |
d_lines.push_back(segment); |
91 |
6 |
d_sizes.push_back(line.size() + 1); |
92 |
|
} |
93 |
80 |
return true; |
94 |
|
} |
95 |
|
|
96 |
|
} // namespace parser |
97 |
29307 |
} // namespace cvc5 |