Skip to content

Commit

Permalink
make GTIRB input optional instead of replacing the BAP input
Browse files Browse the repository at this point in the history
  • Loading branch information
l-kent committed Feb 5, 2024
1 parent 0d344f0 commit d45fed6
Show file tree
Hide file tree
Showing 6 changed files with 45 additions and 50 deletions.
6 changes: 3 additions & 3 deletions src/main/scala/Main.scala
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,8 @@ object Main {

@main(name = "BASIL")
case class Config(
@arg(name = "adt", short = 'a', doc = "BAP ADT file name.")
adtFileName: String,
@arg(name = "input", short = 'i', doc = "BAP .adt file or Gtirb/ASLi .gts file")
inputFileName: 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.")
Expand Down Expand Up @@ -67,7 +67,7 @@ object Main {
}

val q = BASILConfig(
loading = ILLoadingConfig(conf.adtFileName, conf.relfFileName, conf.specFileName, conf.dumpIL, conf.mainProcedureName, conf.procedureDepth),
loading = ILLoadingConfig(conf.inputFileName, conf.relfFileName, conf.specFileName, conf.dumpIL, conf.mainProcedureName, conf.procedureDepth),
runInterpret = conf.interpret.value,
staticAnalysis = if conf.analyse.value then Some(StaticAnalysisConfig(conf.dumpIL, conf.analysisResults, conf.analysisResultsDot)) else None,
boogieTranslation = BoogieGeneratorConfig(if conf.lambdaStores.value then BoogieMemoryAccessMode.LambdaStoreSelect else BoogieMemoryAccessMode.SuccessiveStoreSelect),
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/util/BASILConfig.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package util

case class ILLoadingConfig(adtFile: String, relfFile: String, specFile: Option[String] = None, dumpIL: Option[String] = None, mainProcedureName: String = "main", procedureTrimDepth: Int = Int.MaxValue)
case class ILLoadingConfig(inputFile: String, relfFile: String, specFile: Option[String] = None, dumpIL: Option[String] = None, mainProcedureName: String = "main", procedureTrimDepth: Int = Int.MaxValue)
case class BoogieGeneratorConfig(memoryFunctionType: BoogieMemoryAccessMode = BoogieMemoryAccessMode.SuccessiveStoreSelect, coalesceConstantMemory: Boolean = true)
case class StaticAnalysisConfig(dumpILToPath: Option[String] = None, analysisResultsPath: Option[String] = None, analysisDotPath: Option[String] = None)
enum BoogieMemoryAccessMode:
Expand Down
63 changes: 30 additions & 33 deletions src/main/scala/util/RunUtils.scala
Original file line number Diff line number Diff line change
Expand Up @@ -44,45 +44,43 @@ object RunUtils {
// constants
private val exitRegister: Variable = Register("R30", BitVecType(64))

def loadBAP(fileName: String, mainAddress: Int): Program = {
// // BAP LOGIC
// val ADTLexer = BAP_ADTLexer(CharStreams.fromFileName(fileName))
// val tokens = CommonTokenStream(ADTLexer)
// val parser = BAP_ADTParser(tokens)
def loadBAP(fileName: String): BAPProgram = {
val ADTLexer = BAP_ADTLexer(CharStreams.fromFileName(fileName))
val tokens = CommonTokenStream(ADTLexer)
val parser = BAP_ADTParser(tokens)

// parser.setBuildParseTree(true)

// BAPLoader.visitProject(parser.project())
parser.setBuildParseTree(true)

BAPLoader.visitProject(parser.project())
}

// GTIRB LOGIC
var fIn = new FileInputStream(fileName)
def loadGtirb(fileName: String, mainAddress: Int): Program = {
val fIn = FileInputStream(fileName)
val ir = IR.parseFrom(fIn)
val mods = ir.modules
val cfg = ir.cfg.get

val semantics = mods.map(_.auxData("ast").data.toStringUtf8.parseJson.convertTo[Map[String, Array[Array[String]]]]);
val semantics = mods.map(_.auxData("ast").data.toStringUtf8.parseJson.convertTo[Map[String, Array[Array[String]]]])

def parse_insn (f: String) : StmtContext = {
def parse_insn(f: String): StmtContext = {
try {
val semanticsLexer = SemanticsLexer(CharStreams.fromString(f))
val tokens = CommonTokenStream(semanticsLexer)
val parser = SemanticsParser(tokens)
parser.setErrorHandler(new BailErrorStrategy())
parser.setBuildParseTree(true)
return parser.stmt()
parser.setErrorHandler(BailErrorStrategy())
parser.setBuildParseTree(true)
parser.stmt()
} catch {
case e: org.antlr.v4.runtime.misc.ParseCancellationException =>
println(f)
throw new RuntimeException(e)
Logger.error(f)
throw RuntimeException(e)
}
}

val parserMap = semantics.map(_.map(((k: String,v: Array[Array[String]]) => (k, v.map(_.map(parse_insn(_)))))))
val parserMap = semantics.map(_.map((k: String, v: Array[Array[String]]) => (k, v.map(_.map(parse_insn)))))

val GtirbConverter = new GtirbToIR(mods, parserMap.flatten.toMap, cfg, mainAddress)
val program = GtirbConverter.createIR()
return program
val GtirbConverter = GtirbToIR(mods, parserMap.flatten.toMap, cfg, mainAddress)
GtirbConverter.createIR()
}

def loadReadELF(fileName: String, config: ILLoadingConfig): (Set[ExternalFunction], Set[SpecGlobal], Map[BigInt, BigInt], Int) = {
Expand Down Expand Up @@ -116,21 +114,20 @@ object RunUtils {
}

def loadAndTranslate(q: BASILConfig): BProgram = {

/** Loading phase
*/
val (externalFunctions, globals, globalOffsets, mainAddress) = loadReadELF(q.loading.relfFile, q.loading)

var IRProgram: Program = if (q.loading.inputFile.endsWith(".adt")) {
val bapProgram = loadBAP(q.loading.inputFile)
val IRTranslator = BAPToIR(bapProgram, mainAddress)
IRTranslator.translate
} else if (q.loading.inputFile.endsWith(".gts")) {
loadGtirb(q.loading.inputFile, mainAddress)
} else {
throw Exception(s"input file name ${q.loading.inputFile} must be an .adt or .gst file")
}


// GTIRB LOGIC
val (externalFunctions, globals, globalOffsets, mainAddress) = loadReadELF(q.loading.relfFile, q.loading)
var IRProgram = loadBAP(q.loading.adtFile, mainAddress)

// // BAP LOGIC
// val bapProgram = loadBAP(q.loading.adtFile, 12121)
// val (externalFunctions, globals, globalOffsets, mainAddress) = loadReadELF(q.loading.relfFile, q.loading)
// val IRTranslator = BAPToIR(bapProgram, mainAddress)
// var IRProgram = IRTranslator.translate

val specification = loadSpecification(q.loading.specFile, IRProgram, globals)

/** Analysis Phase
Expand Down
2 changes: 1 addition & 1 deletion src/test/scala/MemoryRegionAnalysisMiscTest.scala
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ class MemoryRegionAnalysisMiscTest extends AnyFunSuite with OneInstancePerTest {
RunUtils.loadAndTranslate(
BASILConfig(
loading = ILLoadingConfig(
adtFile = examplesPath + s"$name/$name.adt",
inputFile = examplesPath + s"$name/$name.adt",
relfFile = examplesPath + s"$name/$name.relf",
specFile = None,
dumpIL = None,
Expand Down
11 changes: 5 additions & 6 deletions src/test/scala/SystemTests.scala
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ class SystemTests extends AnyFunSuite {
val variations = getSubdirectories(path)
variations.foreach(t =>
test("correct/" + p + "/" + t) {
runTest(correctPath, p, t, true)
runTest(correctPath, p, t, true, true)
}
)
}
Expand All @@ -44,7 +44,7 @@ class SystemTests extends AnyFunSuite {
val variations = getSubdirectories(path)
variations.foreach(t =>
test("incorrect/" + p + "/" + t) {
runTest(incorrectPath, p, t, false)
runTest(incorrectPath, p, t, false, true)
}
)
}
Expand Down Expand Up @@ -72,18 +72,17 @@ class SystemTests extends AnyFunSuite {
log(summaryHeader + System.lineSeparator() + summaryRow, testPath + "summary.csv")
}


def runTest(path: String, name: String, variation: String, shouldVerify: Boolean): Unit= {
def runTest(path: String, name: String, variation: String, shouldVerify: Boolean, useADT: Boolean): Unit= {
val directoryPath = path + "/" + name + "/"
val variationPath = directoryPath + variation + "/" + name
val specPath = directoryPath + name + ".spec"
val outPath = variationPath + ".bpl"
val ADTPath = variationPath + ".gts"
val inputPath = if useADT then variationPath + ".adt" else variationPath + ".gts"
val RELFPath = variationPath + ".relf"
Logger.info(outPath)
val timer = PerformanceTimer(s"test $name/$variation")

val args = mutable.ArrayBuffer("--adt", ADTPath, "--relf", RELFPath, "--output", outPath)
val args = mutable.ArrayBuffer("--input", inputPath, "--relf", RELFPath, "--output", outPath)
if (File(specPath).exists) args ++= Seq("--spec", specPath)

Main.main(args.toArray)
Expand Down
11 changes: 5 additions & 6 deletions src/test/scala/ir/InterpreterTests.scala
Original file line number Diff line number Diff line change
Expand Up @@ -18,17 +18,16 @@ class InterpreterTests extends AnyFunSuite with BeforeAndAfter {


val loading = ILLoadingConfig(
adtFile = s"examples/$name/$name.adt",
inputFile = s"examples/$name/$name.adt",
relfFile = s"examples/$name/$name.relf",
specFile = None,
dumpIL = None,
mainProcedureName = "main",
dumpIL = None
)

val bapProgram = loadBAP(loading.inputFile)
val (externalFunctions, globals, _, mainAddress) = loadReadELF(loading.relfFile, loading)
var IRProgram = loadBAP(loading.adtFile, mainAddress)
// val IRTranslator = BAPToIR(bapProgram, mainAddress)
// var IRProgram = IRTranslator.translate
val IRTranslator = BAPToIR(bapProgram, mainAddress)
var IRProgram = IRTranslator.translate
IRProgram = ExternalRemover(externalFunctions.map(e => e.name)).visitProgram(IRProgram)
IRProgram = Renamer(Set("free")).visitProgram(IRProgram)
IRProgram.stripUnreachableFunctions()
Expand Down

0 comments on commit d45fed6

Please sign in to comment.