Generate parser (#848)

* integrates parser generation into build file and changes parser generation script to optionally download the necessary ANTLR JAR

* fixes CI by providing access to genparser.sh

* simplifies parser generator script as we no longer need to make the paths in the comments relative

* cleanup

Author: ArquintL

.gitignore

@@ -28,3 +28,10 @@ project/
 
 # genparser script
 genparser.config
+.genparser/
+
+# generated parser files
+src/main/java/viper/gobra/frontend/GobraLexer.java
+src/main/java/viper/gobra/frontend/GobraParser.java
+src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java
+src/main/java/viper/gobra/frontend/GobraParserVisitor.java

build.sbt

@@ -4,13 +4,21 @@
 //
 // Copyright (c) 2011-2020 ETH Zurich.
 
-import scala.sys.process.Process
+import scala.sys.process._
 import scala.util.Try
 
 // Import general settings from viperserver and, transitively, from carbon, silicon and silver.
 // we assume that carbon/silver and silicon/silver point to the same version of the silver repo
 lazy val server = project in file("viperserver")
 
+lazy val genParser = taskKey[Unit]("Generate Gobra's parser")
+genParser := {
+  val res: Int = ("./genparser.sh --download" !) // parentheses are not optional despite what IntelliJ suggests
+  if (res != 0) {
+    sys.error(s"genparser.sh exited with the non-zero exit code $res")
+  }
+}
+
 // Gobra specific project settings
 lazy val gobra = (project in file("."))
   .dependsOn(server % "compile->compile;test->test")
@@ -44,6 +52,9 @@ lazy val gobra = (project in file("."))
 
     javacOptions := Seq("-encoding", "UTF-8"),
 
+    // overwrite `compile` task to depend on the `genParser` task such that the parser is generated first:
+    Compile / compile := (Compile / compile).dependsOn(genParser).value,
+
     // Run settings
     run / javaOptions ++= Seq(
       "-Xss128m",

genparser.sh

@@ -7,6 +7,8 @@
 
 # This script generates a new parser from the antlr4 files stored in this repository.
 # This script MUST NOT be run from a symlink.
+# '--download' can optionally be passed as a parameter to download ANTLR and automatically create the config file
+# if a config file does not exist yet.
 
 ##### Constants #####
 RED='\033[0;31m'
@@ -18,8 +20,17 @@ RESET='\033[0m'
 # https://stackoverflow.com/questions/24112727/relative-paths-based-on-file-location-instead-of-current-working-directory
 SCRIPT_DIR=$( cd "$(dirname "${BASH_SOURCE[0]}")" || exit 1; pwd -P )
 
-##### Configure if it is the first execution #####
 CONFIGFILE="$SCRIPT_DIR/genparser.config"
+
+##### Download and configure ANTLR if config file does not exist yet #####
+if ! test -f "$CONFIGFILE" && [ "$1" = "--download" ]; then
+  mkdir -p "$SCRIPT_DIR/.genparser"
+  DESTINATION="$SCRIPT_DIR/.genparser/antlr-4.13.1-complete.jar"
+  curl --fail --show-error -L "https://www.antlr.org/download/antlr-4.13.1-complete.jar" --output "$DESTINATION"
+  echo "$DESTINATION" > "$CONFIGFILE"
+fi
+
+##### Configure if it is the first execution #####
 if ! test -f "$CONFIGFILE"; then
   echo -e "What is the ${RED}ABSOLUTE${RESET} path to the antlr4 .jar file?"
   read -r ANSWER
@@ -39,11 +50,5 @@ java -jar "$ANTLR4_PATH" "$SCRIPT_DIR"/src/main/antlr4/GobraLexer.g4 -package vi
 echo -e "${GREEN}Generating the parser:${RESET}"
 java -jar "$ANTLR4_PATH" "$SCRIPT_DIR"/src/main/antlr4/GobraParser.g4 -package viper.gobra.frontend -visitor -no-listener || { echo -e "${RED}Error while generating the parser.${RESET}"; exit 3; }
 
-echo -e "${GREEN}Making path in comments relative:${RESET}"
-sed -i '' 's/\/\/ Generated from .*src\/main\/antlr4\/GobraLexer\.g4/\/\/ Generated from src\/main\/antlr4\/GobraLexer\.g4/g' "$SCRIPT_DIR"/src/main/antlr4/GobraLexer.java
-sed -i '' 's/\/\/ Generated from .*src\/main\/antlr4\/GobraParser\.g4/\/\/ Generated from src\/main\/antlr4\/GobraParser\.g4/g' "$SCRIPT_DIR"/src/main/antlr4/GobraParser.java
-sed -i '' 's/\/\/ Generated from .*src\/main\/antlr4\/GobraParser\.g4/\/\/ Generated from src\/main\/antlr4\/GobraParser\.g4/g' "$SCRIPT_DIR"/src/main/antlr4/GobraParserBaseVisitor.java
-sed -i '' 's/\/\/ Generated from .*src\/main\/antlr4\/GobraParser\.g4/\/\/ Generated from src\/main\/antlr4\/GobraParser\.g4/g' "$SCRIPT_DIR"/src/main/antlr4/GobraParserVisitor.java
-
 echo -e "${GREEN}Moving the generated files:${RESET}"
 mv -v "$SCRIPT_DIR"/src/main/antlr4/*.java "$SCRIPT_DIR"/src/main/java/viper/gobra/frontend/