Merge pull request #424 from viperproject/parser-fixes

Parser Fixes

src/main/java/viper/gobra/frontend/GobraParserBase.java

@@ -1,9 +1,7 @@
 // Imported to Gobra from https://github.com/antlr/grammars-v4/blob/4c06ad8cc8130931c75ca0b17cbc1453f3830cd2/golang
 
 package viper.gobra.frontend;
-import java.util.List;
 import org.antlr.v4.runtime.*;
-import viper.gobra.frontend.GobraLexer;
 
 /**
  * All parser methods that are used in grammar (p, prev, notLineTerminator, etc.)
@@ -16,7 +14,7 @@ protected GobraParserBase(TokenStream input) {
     }
 
     /**
-     * Returns true if the current Token is a closing bracket (")" or "}")
+     * Returns true if the current Token is a closing bracket (")", "}" or "!>")
      */
     protected boolean closingBracket()
     {

src/main/scala/viper/gobra/Gobra.scala

@@ -26,7 +26,7 @@ import scala.concurrent.{Await, Future, TimeoutException}
 
 object GoVerifier {
 
-  val copyright = "(c) Copyright ETH Zurich 2012 - 2021"
+  val copyright = "(c) Copyright ETH Zurich 2012 - 2022"
 
   val name = "Gobra"
 

src/main/scala/viper/gobra/frontend/InformativeErrorListener.scala

@@ -70,10 +70,10 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
 
 
   /**
-    * Failed predicate errors are emitted when the no viable alternatives remain, as all conflict with the input
+    * Failed predicate errors are emitted when no viable alternatives remain, as all alternatives conflict with the input
     * or contain a semantic predicate that evaluated to false. Because the only predicate present in Gobra's grammar
-    * is responsible for inducing semicolons, we know that we are at a point where a statement could have ended, but
-    * another token was discovered.
+    * is responsible for inducing semicolons, we know that if a predicate failed, we are at a point where a statement
+    * could have ended, but another token was discovered.
     *
     * @see [[FailedPredicateException]]
     * @param context
@@ -116,7 +116,7 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
   }
 
   /**
-    * The input did not match the expecte tokens. This one of the most common exceptions.
+    * The input did not match the expected tokens. This is one of the most common exceptions.
     *
     * @see [[InputMismatchException]]
     * @param context The context of the error
@@ -196,7 +196,6 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
   /**
     * Return the display name associated with a specific rule
     * @param index
-    * @param context
     * @return
     */
   def getRuleDisplay(index : Int): String = {

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -2172,8 +2172,8 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
   implicit class PositionableTerminalNode[T <: TerminalNode](term: T) extends PositionableToken(term.getSymbol)
 
   implicit class PositionableToken[T <: Token](tok: T) extends NamedPositionable {
-    val startPos : Position = Position(tok.getLine, tok.getCharPositionInLine + 1, source)
-    val endPos : Position = Position(tok.getLine, tok.getCharPositionInLine + 1 +(tok.getStopIndex -tok.getStartIndex), source)
+    val startPos: Position = source.offsetToPosition(tok.getStartIndex)
+    val endPos: Position = source.offsetToPosition(tok.getStopIndex + 1)
     val name : String = GobraParser.VOCABULARY.getDisplayName(tok.getType)
     val text : String = tok.getText
   }

src/main/scala/viper/gobra/frontend/ReportFirstErrorStrategy.scala

@@ -7,7 +7,7 @@
 package viper.gobra.frontend
 
 import org.antlr.v4.runtime.misc.ParseCancellationException
-import org.antlr.v4.runtime.{BailErrorStrategy, DefaultErrorStrategy, FailedPredicateException, InputMismatchException, Parser, RecognitionException, Token}
+import org.antlr.v4.runtime.{DefaultErrorStrategy, FailedPredicateException, InputMismatchException, Parser, RecognitionException, Token}
 import viper.gobra.frontend.GobraParser.{BlockContext, ExprSwitchStmtContext}
 
 /**
@@ -33,6 +33,8 @@ class ReportFirstErrorStrategy extends DefaultErrorStrategy {
     */
   override def recover(recognizer: Parser, e: RecognitionException): Unit = {
     var context = recognizer.getContext
+    // First, report the error
+    reportError(recognizer, e)
     // For blocks that could be interpreted as struct literals (like `if a == b { }` or `switch tag := 0; tag { }`)
     // Cast a wide net to catch every case, but still allow faster parsing if the error can't be an ambiguity.
     // Thee rest of recover and recoverInline is the same as in the superclass.
@@ -56,6 +58,8 @@ class ReportFirstErrorStrategy extends DefaultErrorStrategy {
 
   override def recoverInline(recognizer: Parser): Token = {
     val e = new InputMismatchException(recognizer)
+    // First report the error
+    reportError(recognizer, e)
     // This performs the same analysis as the recover function above.
     var context = recognizer.getContext
     context match {