Merge branch 'argparsing-refactor'

# Conflicts:
#	readme.md

build.sbt

@@ -9,6 +9,7 @@ val scalaTests = "org.scalatest" %% "scalatest" % "3.2.10" % "test"
 val scalactic = "org.scalactic" %% "scalactic" % "3.2.10"
 val antlrRuntime = "org.antlr" % "antlr4-runtime" % "4.9.3"
 val sourceCode = "com.lihaoyi" %% "sourcecode" % "0.3.0" 
+val mainArgs = "com.lihaoyi" %% "mainargs" % "0.5.1" 
 
 lazy val root = project
   .in(file("."))
@@ -18,12 +19,13 @@ lazy val root = project
     Antlr4 / antlr4Version := "4.9.3",
     Antlr4 / antlr4GenVisitor := true,
     Antlr4 / antlr4PackageName := Some("BilParser"),
-    Compile / run / mainClass := Some("main"),
+    Compile / run / mainClass := Some("Main"),
     libraryDependencies += javaTests,
     libraryDependencies += antlrRuntime,
     libraryDependencies += scalactic,
     libraryDependencies += scalaTests,
-    libraryDependencies += sourceCode
+    libraryDependencies += sourceCode,
+    libraryDependencies += mainArgs 
   )
 
 lazy val updateExpected = taskKey[Unit]("updates .expected for test cases")

readme.md

@@ -79,24 +79,35 @@ The tool takes as inputs a BAP ADT file (here denoted with `.adt`) and a file co
 
 To build and run the tool using sbt, use the following command:
 
-`sbt "run file.adt file.relf [file.spec] [output.bpl] [-analyse]"` where the output filename is optional and specification filenames are optional. The specification filename must end in `.spec`.
+`sbt "run --adt file.adt --relf file.relf [--spec file.spec] [--output output.bpl] [--analyse] [--interpret]"` where the output filename is optional and specification filenames are optional. The specification filename must end in `.spec`.
 
-The `-analyse` flag is optional and enables the static analysis functionality.
+The `--analyse` flag is optional and enables the static analysis functionality.
+
+
+```
+BASIL
+  -a --adt <str>     BAP ADT file name.
+  -r --relf <str>    Output of 'readelf -s -r -W'.
+  -s --spec <str>    BASIL specification file.
+  -o --output <str>  Boogie output destination file.
+  -v --verbose       Show extra debugging logs.
+  --analyse          Run static analysis pass.
+  --interpret        Run BASIL IL interpreter.
+  -h --help          Show this help message.
+```
 
 The sbt shell can also be used for multiple tasks with less overhead by executing `sbt` and then the relevant sbt commands.
 
 To build a standalone `.jar` file, use the following command:
 
 `sbt assembly`
 
+This is located at `target/scala-3.1.0/wptool-boogie-assembly-0.0.1.jar`.
+
 To compile the source without running it - this helps IntelliJ highlight things properly:
 
 `sbt compile`
 
-The standalone `.jar` can then be executed with the following command:
-
-`./run.sh file.adt file.relf [file.spec] [output.bpl] [-analyse]`
-
 ## Generating inputs
 The tool takes a `.adt` and a `.relf` file as inputs, which are produced by BAP and readelf, respectively.
 

src/main/scala/Main.scala

@@ -10,32 +10,53 @@ import scala.collection.{immutable, mutable}
 import scala.language.postfixOps
 import scala.sys.process._
 import util.*
+import mainargs.{main, arg, ParserForClass, Flag}
 
-@main def main(fileName: String, elfFileName: String, options: String*): Unit = {
+object Main {
 
-  Logger.setLevel(LogLevel.DEBUG)
+  @main(name= "BASIL")
+  case class Config(
+    @arg(name="adt", short='a', doc="BAP ADT file name.")
+      adtFileName: String, 
+    @arg(name="relf", short='r', doc="Name of the file containing the output of 'readelf -s -r -W'.")
+      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="analyse", doc="Run static analysis pass.")  
+      analyse: Flag,
+    @arg(name="interpret", doc="Run BASIL IL interpreter.")
+      interpret: Flag,
+    @arg(name="help", short='h', doc="Show this help message.")
+      help: Flag 
+    )
 
+  def main(args: Array[String]): Unit = {
+    val parser = ParserForClass[Config]
+    val parsed = parser.constructEither(args)
 
-  val specFileName: Option[String] = if (options.nonEmpty && options.head.endsWith(".spec")) {
-    Some(options.head)
-  } else {
-    None
-  }
-  val outFileName = if (specFileName.isEmpty) {
-    if (options.isEmpty) {
-      "boogie_out.bpl"
-    } else {
-      options.head
+    val conf = parsed match {
+      case  Right(r) => r
+      case Left(l) => {
+        println(l)
+        return
+      }
     }
-  } else {
-    if (options.tail.isEmpty) {
-      "boogie_out.bpl"
-    } else {
-      options.tail.head
+
+    if (conf.help.value) {
+      println(parser.helpText(sorted=false));
+    }
+
+    Logger.setLevel(LogLevel.WARN)
+    if (conf.verbose.value) {
+      Logger.setLevel(LogLevel.DEBUG)
     }
-  }
-  val performAnalysis = options.nonEmpty && options.contains("-analyse")
-  val performInterpret = options.nonEmpty && options.contains("-interpret")
-  val program: BProgram = RunUtils.loadAndTranslate(fileName, elfFileName, specFileName, performAnalysis, performInterpret)
-  RunUtils.writeToFile(program, outFileName)
+
+    val program: BProgram = RunUtils.loadAndTranslate(conf.adtFileName, conf.relfFileName, conf.specFileName, conf.analyse.value, conf.interpret.value)
+    RunUtils.writeToFile(program, conf.outFileName)
+  } 
+
 }

src/test/scala/SystemTests.scala

@@ -39,9 +39,9 @@ class SystemTests extends AnyFunSuite {
     val ADTPath = variationPath + ".adt"
     val RELFPath = variationPath + ".relf"
     if (File(specPath).exists) {
-      main(ADTPath, RELFPath, specPath, outPath)
+      Main.main(Array("--adt", ADTPath, "--relf", RELFPath, "--spec", specPath, "--output", outPath))
     } else {
-      main(ADTPath, RELFPath, outPath)
+      Main.main(Array("--adt", ADTPath, "--relf", RELFPath, "--output", outPath))
     }
     val boogieResult = Seq("boogie", "/printVerifiedProceduresCount:0", outPath).!!
     val resultPath = variationPath + "_result.txt"