From baa4c4fb81cbc56c787bd6b425b6fa024985be79 Mon Sep 17 00:00:00 2001 From: Jonas Date: Wed, 9 Feb 2022 11:13:04 +0100 Subject: [PATCH 1/3] Fix line positions --- .../viper/silver/parser/FastParser.scala | 34 +++++-------------- 1 file changed, 8 insertions(+), 26 deletions(-) diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index 2f8c1d839..41cf9a3b4 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -32,33 +32,15 @@ object FastParser { NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep) } - // As opposed to use Index ~ t ~ Index, this implementation is agnostic to white space specializations. - def FP[T](t: P[T])(implicit name: sourcecode.Name, ctx: P[_]): P[((FilePosition, FilePosition), T)] = { - t ~ Index map { - case (parsed: T, index) => - - // For some reason, LineCol(ctx.index) sometimes gives us the index of the _end_ of the parsed object (e.g., - // for methods). So, to avoid this in the cases we care about, we check if the parsed object consists - // of several parts and, if it does, use the start position of the first part. - val startPos = if (parsed.isInstanceOf[Product] && parsed.asInstanceOf[Product].productArity > 0) { - val sigh = parsed.asInstanceOf[Product].productElement(0) - sigh match { - case w: Where if w.pos._1.isInstanceOf[HasLineColumn] => { - val lc = w.pos._1.asInstanceOf[HasLineColumn] - (lc.line, lc.column) - } - case (lc: HasLineColumn, _) => { - (lc.line, lc.column) - } - case _ => LineCol(ctx.index) - } - }else{ - LineCol(ctx.index) - } - val finishPos = LineCol(index) - ((FilePosition(_file, startPos._1, startPos._2), FilePosition(_file, finishPos._1, finishPos._2)), parsed) - } + /** + * Function that wraps a parser to provide start and end positions if the wrapped parser succeeds. + */ + def FP[T](t: => P[T])(implicit ctx: P[_]): P[((FilePosition, FilePosition), T)] = { + val startPos = LineCol(ctx.index) + val res = t + val finishPos = LineCol(ctx.index) + res.map({ parsed => ((FilePosition(_file, startPos._1, startPos._2), FilePosition(_file, finishPos._1, finishPos._2)), parsed) }) } /* When importing a file from standard library, e.g. `include `, the file is expected From 4afc0c0803cf90733a501314b3f37dfba4c3e8fe Mon Sep 17 00:00:00 2001 From: Jonas Date: Wed, 9 Feb 2022 11:57:33 +0100 Subject: [PATCH 2/3] Improve positions test --- src/test/scala/AstPositionsTests.scala | 73 ++++++++++++++++++++++++-- 1 file changed, 70 insertions(+), 3 deletions(-) diff --git a/src/test/scala/AstPositionsTests.scala b/src/test/scala/AstPositionsTests.scala index b0321225e..23fe2cab3 100644 --- a/src/test/scala/AstPositionsTests.scala +++ b/src/test/scala/AstPositionsTests.scala @@ -62,11 +62,78 @@ class AstPositionsTests extends AnyFunSuite { |""".stripMargin val res: Program = generateViperAst(code).get - res.methods.map(m => m.pos match { + // Check position of field + assert(res.fields.length === 1) + res.fields(0).pos match { case spos: AbstractSourcePosition => - assert(spos.start !== spos.end.get) + assert(spos.start.line === 1 && spos.end.get.line === 1) + // Here it is unclear if we want to include the `field ` part in the pos + assert(spos.start.column === 1 || spos.start.column === 7) + assert( spos.end.get.column === 15) + case _ => + fail("fields must have start and end positions set") + } + // Check position of method + assert(res.methods.length === 1) + val m: Method = res.methods(0) + m.pos match { + case spos: AbstractSourcePosition => { + assert(spos.start.line === 2 && spos.end.get.line === 10) + assert(spos.start.column === 1 && spos.end.get.column === 2) + } case _ => fail("methods must have start and end positions set") - }) + } + // Check position of method arg + assert(m.formalArgs.length === 1) + val fa: LocalVarDecl = m.formalArgs(0) + fa.pos match { + case spos: AbstractSourcePosition => { + assert(spos.start.line === 2 && spos.end.get.line === 2) + assert(spos.start.column === 12 && spos.end.get.column === 13) + } + case _ => + fail("method args must have start and end positions set") + } + // Check position of method post + assert(m.posts.length === 1) + val post: Exp = m.posts(0) + post.pos match { + case spos: AbstractSourcePosition => { + assert(spos.start.line === 4 && spos.end.get.line === 4) + assert(spos.start.column === 11 && spos.end.get.column === 16) + } + case _ => + fail("method posts must have start and end positions set") + } + // Check position of body + if (m.body.get.ss.length == 1) { + val block: Stmt = m.body.get.ss(0) + block.pos match { + case spos: AbstractSourcePosition => { + assert(spos.start.line === 5 && spos.end.get.line === 10) + assert(spos.start.column === 1 && spos.end.get.column === 2) + } + case _ => + fail("statements must have start and end positions set") + } + if (block.isInstanceOf[Seqn]) { + // Check position of forall + assert(block.asInstanceOf[Seqn].ss.length === 4) + val forall: Stmt = block.asInstanceOf[Seqn].ss(0) + forall.pos match { + case spos: AbstractSourcePosition => { + assert(spos.start.line === 6 && spos.end.get.line === 6) + assert(spos.start.column === 3 && spos.end.get.column === 48) + } + case _ => + fail("forall must have start and end positions set") + } + } else { + fail("Failed to check position of statements in method body due to layout change") + } + } else { + fail("Failed to check position of statements in method body due to layout change") + } } } From 85f5b1306b43a22e8202c11d3d8b4a0ee16b8c8a Mon Sep 17 00:00:00 2001 From: Jonas Date: Wed, 9 Feb 2022 12:01:44 +0100 Subject: [PATCH 3/3] Clarify types and print stack-trace on exception in parser --- src/main/scala/viper/silver/parser/FastParser.scala | 2 +- src/main/scala/viper/silver/reporter/Reporter.scala | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index 41cf9a3b4..a8ec6327c 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -38,7 +38,7 @@ object FastParser { */ def FP[T](t: => P[T])(implicit ctx: P[_]): P[((FilePosition, FilePosition), T)] = { val startPos = LineCol(ctx.index) - val res = t + val res: P[T] = t val finishPos = LineCol(ctx.index) res.map({ parsed => ((FilePosition(_file, startPos._1, startPos._2), FilePosition(_file, finishPos._1, finishPos._2)), parsed) }) } diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala index ede6156cc..79d0efce8 100644 --- a/src/main/scala/viper/silver/reporter/Reporter.scala +++ b/src/main/scala/viper/silver/reporter/Reporter.scala @@ -112,8 +112,10 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t case ExceptionReport(e) => /** Theoretically, we may encounter an exceptional message that has - * not yet been reported via AbortedExceptionally. */ + * not yet been reported via AbortedExceptionally. This can happen + * if we encounter exeptions in e.g. the parser. */ println( s"Verification aborted exceptionally: ${e.toString}" ) + e.printStackTrace(System.out); Option(e.getCause) match { case Some(cause) => println( s" Cause: ${cause.toString}" ) case None =>