From c571c8c4b1d6a8f90ab60d3411cf2c03a61ea457 Mon Sep 17 00:00:00 2001
From: Alistair Michael <alistair.michael@uq.edu.au>
Date: Fri, 13 Oct 2023 15:02:48 +1000
Subject: [PATCH] add sbt-git-versioning, buildinfo, and version flag

---
 build.sbt                 |  5 +++--
 project/plugins.sbt       |  5 +++++
 src/main/scala/Main.scala | 23 ++++++++++++++++++++---
 3 files changed, 28 insertions(+), 5 deletions(-)

diff --git a/build.sbt b/build.sbt
index a331e7743..b13c36527 100644
--- a/build.sbt
+++ b/build.sbt
@@ -1,7 +1,7 @@
 import scala.io.Source
 
+import scala.sys.process.*
 ThisBuild / scalaVersion := "3.1.0"
-ThisBuild / version := "0.0.1"
 ThisBuild / organization := "uq.pac"
 
 val javaTests = "com.novocode" % "junit-interface" % "0.11" % "test"
@@ -13,9 +13,10 @@ val mainArgs = "com.lihaoyi" %% "mainargs" % "0.5.1"
 
 lazy val root = project
   .in(file("."))
-  .enablePlugins(Antlr4Plugin)
+  .enablePlugins(Antlr4Plugin, BuildInfoPlugin)
   .settings(
     name := "wptool-boogie",
+    buildInfoKeys := Seq[BuildInfoKey](name, version, scalaVersion, sbtVersion),
     Antlr4 / antlr4Version := "4.9.3",
     Antlr4 / antlr4GenVisitor := true,
     Antlr4 / antlr4PackageName := Some("Parsers"),
diff --git a/project/plugins.sbt b/project/plugins.sbt
index 01970cd71..a7a03448f 100644
--- a/project/plugins.sbt
+++ b/project/plugins.sbt
@@ -1,2 +1,7 @@
 addSbtPlugin("com.simplytyped" % "sbt-antlr4" % "0.8.3")
 addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "1.2.0")
+
+resolvers += Resolver.bintrayIvyRepo("rallyhealth", "sbt-plugins")
+
+addSbtPlugin("com.rallyhealth.sbt" % "sbt-git-versioning" % "1.6.0")
+addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.11.0")
diff --git a/src/main/scala/Main.scala b/src/main/scala/Main.scala
index f64f60cff..879389f0c 100644
--- a/src/main/scala/Main.scala
+++ b/src/main/scala/Main.scala
@@ -4,6 +4,7 @@ import bap._
 import boogie._
 import translating._
 import util.RunUtils
+import buildinfo.* 
 
 import scala.collection.mutable.{ArrayBuffer, Set}
 import scala.collection.{immutable, mutable}
@@ -14,18 +15,20 @@ import mainargs.{main, arg, ParserForClass, Flag}
 
 object Main {
 
-  @main(name = "BASIL")
+  @main(name = f"${BuildInfo.name} ${BuildInfo.version}")
   case class Config(
       @arg(name = "adt", short = 'a', doc = "BAP ADT file name.")
-      adtFileName: String,
+      adtFileName: String = "",
       @arg(name = "relf", short = 'r', doc = "Name of the file containing the output of 'readelf -s -r -W'.")
-      relfFileName: String,
+      relfFileName: String = "",
       @arg(name = "spec", short = 's', doc = "BASIL specification file.")
       specFileName: Option[String],
       @arg(name = "output", short = 'o', doc = "Boogie output destination file.")
       outFileName: String = "boogie_out.bpl",
       @arg(name = "verbose", short = 'v', doc = "Show extra debugging logs.")
       verbose: Flag,
+      @arg(name = "version", doc = "Show version.")
+      version: Flag,
       @arg(name = "analyse", doc = "Run static analysis pass.")
       analyse: Flag,
       @arg(name = "interpret", doc = "Run BASIL IL interpreter.")
@@ -48,15 +51,29 @@ object Main {
       }
     }
 
+
     if (conf.help.value) {
       println(parser.helpText(sorted = false));
+      return;
+    }
+
+    if (conf.version.value) {
+      println(f"${BuildInfo.name} ${BuildInfo.version}")
+      return;
     }
 
+
     Logger.setLevel(LogLevel.INFO)
     if (conf.verbose.value) {
       Logger.setLevel(LogLevel.DEBUG)
     }
 
+    if (conf.adtFileName == "" || conf.relfFileName == "") {
+      println("Must specify adt and relf.")
+      println(parser.helpText(sorted = false));
+      return;
+    }
+
     val program: BProgram = RunUtils.loadAndTranslate(
       conf.adtFileName,
       conf.relfFileName,