Fix reserved parser keyword error reporting (#869)

* adds bug witness

* fixes InformativeErrorListener to report 'proof' as a reserved word

Author: ArquintL

src/main/antlr4/GobraLexer.g4

@@ -17,6 +17,7 @@ DECIMAL_FLOAT_LIT      : DECIMALS ('.'{_input.LA(1) != '.'}? DECIMALS? EXPONENT?
 // ->mode(NLSEMI) means line breaks directly after this token
 // emit a semicolon. (just like after identifiers, literals, ')}]' etc in base Go)
 
+// NOTE: if you prepend a new token, do not forget to update InformativeErrorListener.FIRST_GOBRA_TOKEN
 TRUE        : 'true' -> mode(NLSEMI);
 FALSE       : 'false' -> mode(NLSEMI);
 ASSERT      : 'assert';
@@ -93,4 +94,5 @@ GHOST_NOT_EQUALS : '!==';
 WITH        : 'with';
 OPAQUE      : 'opaque' -> mode(NLSEMI);
 REVEAL      : 'reveal';
-BACKEND     : '#backend';
+BACKEND     : '#backend';
+// NOTE: if you append a new token, do not forget to update InformativeErrorListener.LAST_GOBRA_TOKEN

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

@@ -20,6 +20,19 @@ import scala.collection.mutable.ListBuffer
 
 class InformativeErrorListener(val messages: ListBuffer[ParserError], val source: Source) extends BaseErrorListener {
 
+  /**
+    * First token that Gobra introduces that is not present in Go.
+    * First refers to the order of token declarations in GobraLexer.g4
+    * as this order is preserved by ANTLR4 when generating GobraParser.java
+    */
+  private val FIRST_GOBRA_TOKEN = GobraParser.TRUE
+  /**
+    * Last token that Gobra introduces that is not present in Go.
+    * Last refers to the order of token declarations in GobraLexer.g4
+    * this order is preserved by ANTLR4 when generating GobraParser.java
+    */
+  private val LAST_GOBRA_TOKEN = GobraParser.BACKEND
+
   /**
     *
     * @param recognizer The recognizer that encountered the error
@@ -314,5 +327,5 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
   }
 
   // All tokens reserved by gobra, but not by Go
-  val new_reserved = IntervalSet.of(GobraParser.TRUE, GobraParser.TRUSTED)
+  val new_reserved = IntervalSet.of(FIRST_GOBRA_TOKEN, LAST_GOBRA_TOKEN)
 }

src/test/scala/viper/gobra/parsing/ParserUnitTests.scala

@@ -11,6 +11,7 @@ import org.scalatest.exceptions.TestFailedException
 import org.scalatest.funsuite.AnyFunSuite
 import org.scalatest.matchers.should.Matchers
 import viper.gobra.ast.frontend._
+import viper.gobra.reporting.ParserError
 import viper.gobra.util.{Decimal, Hexadecimal}
 
 class ParserUnitTests extends AnyFunSuite with Matchers with Inside {
@@ -2721,4 +2722,10 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside {
       case Vector(PExplicitGhostMember(PTypeDef(PExplicitGhostStructType(PStructType(Vector(PFieldDecls(Vector(PFieldDecl(PIdnDef("Value"), PIntType())))))), PIdnDef("MyStruct")))) =>
     }
   }
+
+  test("Parser: should point out that 'proof' is a reserved word") {
+    frontend.parseMember("func test(proof ProofType)") should matchPattern {
+      case Left(Vector(ParserError(msg, _))) if msg contains "Unexpected reserved word proof" =>
+    }
+  }
 }