Skip to content

Commit 1828cf8

Browse files
authored
Merge pull request #477 from viperproject/optimize-parser
Optimize parser on large Viper files
2 parents d000b35 + 8cc6f64 commit 1828cf8

2 files changed

Lines changed: 21 additions & 10 deletions

File tree

src/main/scala/viper/silver/parser/FastParser.scala

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,12 +34,21 @@ object FastParser extends PosParser[Char, String] {
3434
*/
3535
val standard_import_directory = "import"
3636

37-
var _lines: Array[Int] = null
37+
var _line_offset: Array[Int] = null
3838

3939
def parse(s: String, f: Path, plugins: Option[SilverPluginManager] = None) = {
4040
_file = f.toAbsolutePath
41+
42+
// Add an empty line at the end to make `computeFrom(s.length)` return `(lines.length, 1)`, as the old
43+
// implementation of `computeFrom` used to do.
4144
val lines = s.linesWithSeparators
42-
_lines = lines.map(_.length).toArray
45+
_line_offset = (lines.map(_.length) ++ Seq(0)).toArray
46+
var offset = 0
47+
for (i <- _line_offset.indices) {
48+
val line_length = _line_offset(i)
49+
_line_offset(i) = offset
50+
offset += line_length
51+
}
4352

4453
// Strategy to handle imports
4554
// Idea: Import every import reference and merge imported methods, functions, imports, .. into current program

src/main/scala/viper/silver/parser/ParserPositions.scala

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -30,15 +30,17 @@ case class FilePosition(file: Path, vline: Int, col: Int) extends util.parsing.i
3030

3131
trait PosComputer {
3232
def computeFrom(index: Int) : (Int, Int) = {
33-
var left = index
34-
var i = 0
35-
val arr = FastParser._lines
36-
while (i < arr.length && left >= arr(i)){
37-
left -= arr(i)
38-
i += 1
33+
val line_offset = FastParser._line_offset
34+
val result = java.util.Arrays.binarySearch(line_offset, index)
35+
if (result >= 0) {
36+
// Exact match
37+
val line = result
38+
(line + 1, index - line_offset(line) + 1)
39+
} else {
40+
// The binary search returned `- insertionPoint - 1`
41+
val line = - result - 2
42+
(line + 1, index - line_offset(line) + 1)
3943
}
40-
val r1 = (i + 1, left + 1)
41-
r1
4244
}
4345
}
4446
/**

0 commit comments

Comments
 (0)