diff --git a/build.sbt b/build.sbt index 3a833b25f..535704cfe 100644 --- a/build.sbt +++ b/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") diff --git a/readme.md b/readme.md index 1d977f567..16c994e2d 100644 --- a/readme.md +++ b/readme.md @@ -79,9 +79,22 @@ 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 BAP ADT file name. + -r --relf Output of 'readelf -s -r -W'. + -s --spec BASIL specification file. + -o --output 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. @@ -89,14 +102,12 @@ 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. diff --git a/src/main/scala/Main.scala b/src/main/scala/Main.scala index b21807345..86d347557 100644 --- a/src/main/scala/Main.scala +++ b/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) + } + } diff --git a/src/test/scala/SystemTests.scala b/src/test/scala/SystemTests.scala index b6b3cdeee..99daaeaac 100644 --- a/src/test/scala/SystemTests.scala +++ b/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"