Skip to content

Commit

Permalink
Merge pull request #79 from UQ-PAC/serialise-il
Browse files Browse the repository at this point in the history
Serialise IL
  • Loading branch information
l-kent authored Sep 22, 2023
2 parents ecc244f + c20c1ba commit 50c80a6
Show file tree
Hide file tree
Showing 6 changed files with 298 additions and 5 deletions.
5 changes: 4 additions & 1 deletion src/main/scala/Main.scala
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@ object Main {
analyse: Flag,
@arg(name="interpret", doc="Run BASIL IL interpreter.")
interpret: Flag,
@arg(name="dump-il", doc="Dump the Intermediate Language to text.")
dumpIL: Flag,
@arg(name="help", short='h', doc="Show this help message.")
help: Flag
)
Expand All @@ -55,7 +57,8 @@ object Main {
Logger.setLevel(LogLevel.DEBUG)
}

val program: BProgram = RunUtils.loadAndTranslate(conf.adtFileName, conf.relfFileName, conf.specFileName, conf.analyse.value, conf.interpret.value)

val program: BProgram = RunUtils.loadAndTranslate(conf.adtFileName, conf.relfFileName, conf.specFileName, conf.analyse.value, conf.interpret.value, conf.dumpIL.value)
RunUtils.writeToFile(program, conf.outFileName)
}

Expand Down
5 changes: 4 additions & 1 deletion src/main/scala/ir/Expr.scala
Original file line number Diff line number Diff line change
Expand Up @@ -356,6 +356,9 @@ sealed trait Variable extends Expr {
case b: BitVecType => b.size
case _ => throw new Exception("tried to get size of non-bitvector")
}

override def toString: String = s"Variable($name, $irType)"

override def acceptVisit(visitor: Visitor): Variable =
throw new Exception("visitor " + visitor + " unimplemented for: " + this)
}
Expand All @@ -372,4 +375,4 @@ case class LocalVar(override val name: String, override val irType: IRType) exte
override def toBoogie: BVar = BVariable(s"$name", irType.toBoogie, Scope.Local)
override def toString: String = s"LocalVar($name, $irType)"
override def acceptVisit(visitor: Visitor): Variable = visitor.visitLocalVar(this)
}
}
4 changes: 3 additions & 1 deletion src/main/scala/ir/Program.scala
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,8 @@ class Program(var procedures: ArrayBuffer[Procedure], var initialMemory: ArrayBu
p.stackIdentification()
}
}


}

class Procedure(var name: String, var address: Option[Int], var blocks: ArrayBuffer[Block], var in: ArrayBuffer[Parameter], var out: ArrayBuffer[Parameter]) {
Expand Down Expand Up @@ -179,4 +181,4 @@ class Parameter(var name: String, var size: Int, var value: Register) {
def toGamma: BVariable = BParam(s"Gamma_$name", BoolBType)
}

case class MemorySection(name: String, address: Int, size: Int, bytes: Seq[Literal])
case class MemorySection(name: String, address: Int, size: Int, bytes: Seq[Literal])
276 changes: 276 additions & 0 deletions src/main/scala/translating/ILtoIL.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,276 @@
package translating
import ir._


private class ILSerialiser extends ReadOnlyVisitor {
var program: StringBuilder = StringBuilder()

var indentLevel = 0

def getIndent(): String = {
" " * indentLevel
}

def blockIdentifier(block: Block) : String = {
val i = block.address match {
case Some(addr) => f"${addr}:${block.label}"
case None => f"?:${block.label}"
}
'"' + i + '"'
}

def procedureIdentifier(proc: Procedure): String = {
val i = proc.address match {
case Some(addr) => f"${addr}:${proc.name}"
case None => f"?:${proc.name}"
}
'"' + i + '"'
}


override def visitExpr(node: Expr): Expr = {
node.acceptVisit(this)
}

override def visitStatement(node: Statement): Statement = node.acceptVisit(this)

override def visitLocalAssign(node: LocalAssign): Statement = {
program ++= "LocalAssign("
visitVariable(node.lhs)
program ++= " := "
visitExpr(node.rhs)
program ++= ")"
node
}

override def visitMemoryAssign(node: MemoryAssign): Statement = {
program ++= "MemoryAssign("
visitMemoryStore(node.rhs)
program ++= ")"
node
}

override def visitAssert(node: Assert): Statement = {
program ++= "Assert("
visitExpr(node.body)
program ++= ")"
node
}

override def visitJump(node: Jump): Jump = {
node.acceptVisit(this)
node
}

override def visitGoTo(node: GoTo): Jump = {
program ++= "GoTo("
// TODO
program ++= blockIdentifier(node.target)
program ++= ", "
program ++= "condition("
node.condition.map(visitExpr)
program ++= ")" // Condition
program ++= ")" // GoTo
node
}

override def visitDirectCall(node: DirectCall): Jump = {
program ++= "DirectCall("
program ++= procedureIdentifier(node.target)
program ++= ", "
program ++= "condition("
node.condition.map(visitExpr)
program ++= ")" // Condition
program ++= ")" // DirectCall
node
}

override def visitIndirectCall(node: IndirectCall): Jump = {
program ++= "IndirectCall("
visitVariable(node.target)
program ++= ", "
program ++= "condition("
node.condition.map(visitExpr)
program ++= ")" // Condition
program ++= ")" // IndirectCall
node
}

override def visitBlock(node: Block): Block = {
program ++= getIndent()
program ++= "Block(" + blockIdentifier(node) + ",\n"
indentLevel += 1
program ++= getIndent()
program ++= "statements(\n"
indentLevel += 1

for (i <- node.statements.indices) {
program ++= getIndent()
visitStatement(node.statements(i))
program ++= "\n"
}
indentLevel -= 1
program ++= getIndent() + "),\n"
program ++= getIndent() + "jumps(\n"
indentLevel += 1
for (j <- node.jumps) {
program ++= getIndent()
visitJump(j)
program ++= "\n"
}
indentLevel -= 1
program ++= getIndent() + ")\n"
indentLevel -= 1
program ++= getIndent()
program ++= ")\n"
node
}

override def visitProcedure(node: Procedure): Procedure = {
program ++= "Procedure(" + procedureIdentifier(node) + ", "
indentLevel += 1

program ++= "in("
for (i <- node.in.indices) {
visitParameter(node.in(i))
if (i != node.in.size - 1) {
program ++= ", "
}
}
program ++= "), "
program ++= "out("
for (i <- node.out.indices) {
visitParameter(node.out(i))
if (i != node.out.size - 1)
program ++= ", "
}
program ++= "), "
program ++= "blocks(\n"
for (i <- node.blocks.indices) {
visitBlock(node.blocks(i))
}
program ++= ")),\n"
indentLevel -= 1
node
}

override def visitParameter(node: Parameter): Parameter = {
program ++= "Parameter("
visitRegister(node.value)
program ++= ")"
node
}

override def visitProgram(node: Program): Program = {
for (i <- node.procedures) {
visitProcedure(i)
}
node
}

override def visitExtract(node: Extract): Expr = {
program ++= "Extract("
visitExpr(node.body)
program ++= f"[${node.end}:${node.start}]"
program ++= ")"
node
}

override def visitRepeat(node: Repeat): Expr = {
program ++= "Repeat("
visitExpr(node.body)
program ++= f", ${node.repeats}"
program ++= ")"
node
}

override def visitZeroExtend(node: ZeroExtend): Expr = {
program ++= "ZeroExtend("
visitExpr(node.body)
program ++= f", ${node.extension}"
program ++= ")"
node
}

override def visitSignExtend(node: SignExtend): Expr = {
program ++= "SignExtend("
visitExpr(node.body)
program ++= f", ${node.extension}"
program ++= ")"
node
}

override def visitUnaryExpr(node: UnaryExpr): Expr = {
program ++= "UnaryExpr("
program ++= '"' + f"${node.op}" + '"' + ", "
visitExpr(node.arg)
program ++= ")"
node
}

override def visitBinaryExpr(node: BinaryExpr): Expr = {
program ++= "BinaryExpr("
program ++= "\"" + node.op + '"' + ", "
visitExpr(node.arg1)
program ++= ", "
visitExpr(node.arg2)
program ++= ")"
node
}

override def visitMemoryStore(node: MemoryStore): MemoryStore = {
program ++= "MemoryStore("
visitMemory(node.mem)
program ++= "["
visitExpr(node.index)
program ++= "] := "
visitExpr(node.value)
program ++= ")"
node
}

override def visitMemoryLoad(node: MemoryLoad): Expr = {
program ++= "MemoryLoad("
visitMemory(node.mem)
program ++= ", ["
visitExpr(node.index)
program ++= "])"
node
}

override def visitMemory(node: Memory): Memory = {
program ++= "Memory("
program ++= '"' + node.name + '"'
program ++= f", ${node.addressSize}, ${node.valueSize})"
node
}

override def visitVariable(node: Variable): Variable = {
program ++= node.toString()
node
}

override def visitRegister(node: Register): Register = {
program ++= node.toString()
node
}

override def visitLocalVar(node: LocalVar): LocalVar = {
program ++= node.toString()
node
}

override def visitLiteral(node: Literal): Literal = {
program ++= node.toString()
node
}


}

def serialiseIL(p: Program): String = {
val s = ILSerialiser()
s.visitProgram(p)
s.program.toString()
}

11 changes: 10 additions & 1 deletion src/main/scala/util/RunUtils.scala
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ object RunUtils {
}
}

def loadAndTranslate(BAPFileName: String, readELFFileName: String, specFileName: Option[String], performAnalysis: Boolean, performInterpret: Boolean): BProgram = {
def loadAndTranslate(BAPFileName: String, readELFFileName: String, specFileName: Option[String], performAnalysis: Boolean, performInterpret: Boolean, dumpIL: Boolean): BProgram = {
val bapProgram = loadBAP(BAPFileName)

val (externalFunctions, globals, globalOffsets, mainAddress) = loadReadELF(readELFFileName)
Expand All @@ -74,10 +74,19 @@ object RunUtils {
IRProgram = externalRemover.visitProgram(IRProgram)
IRProgram = renamer.visitProgram(IRProgram)

if (dumpIL) {
dump_file(serialiseIL(IRProgram), "before-analysis.il")
}

if (performAnalysis) {
analyse(IRProgram, externalFunctions, globals, globalOffsets)
if (dumpIL) {
dump_file(serialiseIL(IRProgram), "after-analysis.il")
}
}



IRProgram.stripUnreachableFunctions()
IRProgram.stackIdentification()
IRProgram.setModifies()
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 @@ -14,7 +14,7 @@ class MemoryRegionAnalysisMiscTest extends AnyFunSuite with OneInstancePerTest {
var expected = ""
var actual = ""
var output: Option[Map[analysis.CfgNode, ?]] = None
RunUtils.loadAndTranslate(examplesPath + s"${name}/${name}.adt", examplesPath + s"${name}/${name}.relf", None, true, false)
RunUtils.loadAndTranslate(examplesPath + s"${name}/${name}.adt", examplesPath + s"${name}/${name}.relf", None, true, false, false)
try {
// create dump folder if it does not exist
val dumpFolder = File(tempPath)
Expand Down

0 comments on commit 50c80a6

Please sign in to comment.