From a452165707a53525d2aee18b596ff0a3e4a3d701 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Fri, 29 Nov 2024 16:49:28 +1000 Subject: [PATCH] work on adding param support to interpreter --- src/main/scala/ir/Expr.scala | 2 +- src/main/scala/ir/eval/InterpretBasilIR.scala | 95 +++++++++++++++---- src/main/scala/ir/eval/Interpreter.scala | 2 + src/main/scala/util/RunUtils.scala | 1 - .../State.scala} | 0 ...s.scala => DifferentialAnalysisTest.scala} | 84 +++++++--------- 6 files changed, 115 insertions(+), 69 deletions(-) rename src/main/scala/util/{functional.scala => functional/State.scala} (100%) rename src/test/scala/{DifferentialAnalysis.scala => DifferentialAnalysisTest.scala} (70%) diff --git a/src/main/scala/ir/Expr.scala b/src/main/scala/ir/Expr.scala index 447ed82a6..6ab939a4b 100644 --- a/src/main/scala/ir/Expr.scala +++ b/src/main/scala/ir/Expr.scala @@ -42,7 +42,7 @@ case object FalseLiteral extends BoolLit { } case class BitVecLiteral(value: BigInt, size: Int) extends Literal { - assert(size > 0) + assert(size >= 0) override def toBoogie: BitVecBLiteral = BitVecBLiteral(value, size) override def getType: IRType = BitVecType(size) override def toString: String = s"${value}bv$size" diff --git a/src/main/scala/ir/eval/InterpretBasilIR.scala b/src/main/scala/ir/eval/InterpretBasilIR.scala index 2c0697e77..24a274fd8 100644 --- a/src/main/scala/ir/eval/InterpretBasilIR.scala +++ b/src/main/scala/ir/eval/InterpretBasilIR.scala @@ -70,6 +70,16 @@ case object Eval { } yield (res) } + def evalLiteral[S, T <: Effects[S, InterpreterError]](f: T)(e: Expr): State[S, Literal, InterpreterError] = { + for { + res <- evalExpr(f)(e) + r <- State.pureE(res match { + case l: Literal => Right(l) + case _ => Left((Errored(s"Eval BV residual $e"))) + }) + } yield (r) + } + def evalBV[S, T <: Effects[S, InterpreterError]](f: T)(e: Expr): State[S, BitVecLiteral, InterpreterError] = { for { res <- evalExpr(f)(e) @@ -228,12 +238,11 @@ case object Eval { /** Helper functions * */ - /** - * Load all memory cells from pointer until reaching cell containing 0. - * Ptr -> List[Bitvector] - */ - def getNullTerminatedString[S, T <: Effects[S, InterpreterError]](f: T) - (rgn: String, src: BasilValue, acc: List[BitVecLiteral] = List()): State[S, List[BitVecLiteral], InterpreterError] = + /** Load all memory cells from pointer until reaching cell containing 0. Ptr -> List[Bitvector] + */ + def getNullTerminatedString[S, T <: Effects[S, InterpreterError]]( + f: T + )(rgn: String, src: BasilValue, acc: List[BitVecLiteral] = List()): State[S, List[BitVecLiteral], InterpreterError] = for { srv: BitVecLiteral <- src match { case Scalar(b: BitVecLiteral) => State.pure(b) @@ -262,6 +271,7 @@ class BASILInterpreter[S](f: Effects[S, InterpreterError]) extends Interpreter[S r: Boolean <- (next match { case Intrinsic(tgt) => LibcIntrinsic.intrinsics(tgt)(f).map(_ => true) case Run(c: Statement) => interpretStatement(f)(c).map(_ => true) + case ReturnTo(c) => interpretReturn(f)(c).map(_ => true) case Run(c: Jump) => interpretJump(f)(c).map(_ => true) case Stopped() => State.pure(false) case ErrorStop(e) => State.pure(false) @@ -297,16 +307,45 @@ class BASILInterpreter[S](f: Effects[S, InterpreterError]) extends Interpreter[S case h :: tl => State.setError(Errored(s"More than one jump guard satisfied $gt")) } } yield (res) - case r: Return => f.doReturn() + case r: Return => { + // eval return values, return to caller, then bind return values to formal out params + for { + outs <- State.mapM( + ((bindout: (LocalVar, Expr)) => { + for { + rhs <- Eval.evalLiteral(f)(bindout._2) + } yield (bindout._1, rhs) + }), + r.outParams + ) + _ <- f.doReturn() + _ <- State.sequence(State.pure(()), outs.map(m => f.storeVar(m._1.name, m._1.toBoogie.scope, Scalar(m._2)))) + } yield () + } case h: Unreachable => State.setError(EscapedControlFlow(h)) } } + def interpretReturn[S, T <: Effects[S, InterpreterError]](f: T)(s: DirectCall): State[S, Unit, InterpreterError] = { + for { + outs <- State.mapM( + ((bindout: (LocalVar, Variable)) => { + for { + rhs <- Eval.evalLiteral(f)(bindout._1) + } yield (bindout._2, rhs) + }), + s.outParams + ) + c <- State.sequence(State.pure(()), outs.map(m => f.storeVar(m._1.name, m._1.toBoogie.scope, Scalar(m._2)))) + _ <- f.setNext(Run(s.successor)) + } yield (c) + } + def interpretStatement[S, T <: Effects[S, InterpreterError]](f: T)(s: Statement): State[S, Unit, InterpreterError] = { s match { case assign: LocalAssign => { for { - rhs <- Eval.evalBV(f)(assign.rhs) + rhs <- Eval.evalLiteral(f)(assign.rhs) st <- f.storeVar(assign.lhs.name, assign.lhs.toBoogie.scope, Scalar(rhs)) n <- f.setNext(Run(s.successor)) } yield (st) @@ -347,14 +386,29 @@ class BASILInterpreter[S](f: Effects[S, InterpreterError]) extends Interpreter[S }) } yield (n) case dc: DirectCall => { - if (dc.target.entryBlock.isDefined) { - val block = dc.target.entryBlock.get - f.call(dc.target.name, Run(block.statements.headOption.getOrElse(block.jump)), Run(dc.successor)) - } else if (LibcIntrinsic.intrinsics.contains(dc.target.name)) { - f.call(dc.target.name, Intrinsic(dc.target.name), Run(dc.successor)) - } else { - State.setError(EscapedControlFlow(dc)) - } + for { + actualParams <- State.mapM( + (p: (LocalVar, Expr)) => + for { + v <- Eval.evalLiteral(f)(p._2) + } yield (p._1, v), + dc.actualParams + ) + _ <- { + if (dc.target.entryBlock.isDefined) { + val block = dc.target.entryBlock.get + f.call(dc.target.name, Run(block.statements.headOption.getOrElse(block.jump)), ReturnTo(dc)) + } else if (LibcIntrinsic.intrinsics.contains(dc.target.name)) { + f.call(dc.target.name, Intrinsic(dc.target.name), ReturnTo(dc)) + } else { + State.setError(EscapedControlFlow(dc)) + } + } + _ <- State.sequence( + State.pure(()), + actualParams.map(m => f.storeVar(m._1.name, m._1.toBoogie.scope, Scalar(m._2))) + ) + } yield () } case ic: IndirectCall => { if (ic.target == Register("R30", 64)) { @@ -460,6 +514,9 @@ object InterpFuns { j <- s.storeVar("R31", Scope.Global, Scalar(SP)) k <- s.storeVar("R29", Scope.Global, Scalar(FP)) l <- s.storeVar("R30", Scope.Global, Scalar(LR)) + j <- s.storeVar("R31_in", Scope.Global, Scalar(SP)) + k <- s.storeVar("R29_in", Scope.Global, Scalar(FP)) + l <- s.storeVar("R30_in", Scope.Global, Scalar(LR)) l <- s.storeVar("R0", Scope.Global, Scalar(BitVecLiteral(0, 64))) l <- s.storeVar("R1", Scope.Global, Scalar(BitVecLiteral(0, 64))) _ <- s.storeVar("ghost-funtable", Scope.Global, BasilMapValue(Map.empty, MapType(BitVecType(64), BitVecType(64)))) @@ -503,10 +560,10 @@ object InterpFuns { _ <- State.pure(Logger.debug("INITIALISE MEMORY SECTIONS")) mem <- initMemory("mem", p.initialMemory.values) mem <- initMemory("stack", p.initialMemory.values) - mainfun = { - p.mainProcedure - } + mainfun = p.mainProcedure + r <- f.call("init_activation", Stopped(), Stopped()) // frame for main to return to r <- f.call(mainfun.name, Run(IRWalk.firstInBlock(mainfun.entryBlock.get)), Stopped()) + l <- State.sequence(State.pure(()), mainfun.formalInParam.toList.map(i => f.storeVar(i.name, i.toBoogie.scope, Scalar(BitVecLiteral(0, size(i).get))))) } yield (r) } diff --git a/src/main/scala/ir/eval/Interpreter.scala b/src/main/scala/ir/eval/Interpreter.scala index 6f948269f..e221d2f8a 100644 --- a/src/main/scala/ir/eval/Interpreter.scala +++ b/src/main/scala/ir/eval/Interpreter.scala @@ -18,6 +18,7 @@ sealed trait ExecutionContinuation case class Stopped() extends ExecutionContinuation /* normal program stop */ case class ErrorStop(error: InterpreterError) extends ExecutionContinuation /* program stop in error state */ case class Run(next: Command) extends ExecutionContinuation /* continue by executing next command */ +case class ReturnTo(call: DirectCall) extends ExecutionContinuation /* continue by executing next command */ case class Intrinsic(name: String) extends ExecutionContinuation /* a named intrinsic instruction */ sealed trait InterpreterError @@ -312,6 +313,7 @@ case class MemoryState( } object LibcIntrinsic { + // TODO: make parameter passing work /** * Part of the intrinsics implementation that lives above the Effects interface diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala index 2377515e9..18b8c4648 100644 --- a/src/main/scala/util/RunUtils.scala +++ b/src/main/scala/util/RunUtils.scala @@ -640,7 +640,6 @@ object RunUtils { } if (q.loading.parameterForm) { - ir.transforms.clearParams(ctx.program) ctx = ir.transforms.liftProcedureCallAbstraction(ctx) } else { diff --git a/src/main/scala/util/functional.scala b/src/main/scala/util/functional/State.scala similarity index 100% rename from src/main/scala/util/functional.scala rename to src/main/scala/util/functional/State.scala diff --git a/src/test/scala/DifferentialAnalysis.scala b/src/test/scala/DifferentialAnalysisTest.scala similarity index 70% rename from src/test/scala/DifferentialAnalysis.scala rename to src/test/scala/DifferentialAnalysisTest.scala index f26e268b3..9ca9b382b 100644 --- a/src/test/scala/DifferentialAnalysis.scala +++ b/src/test/scala/DifferentialAnalysisTest.scala @@ -19,7 +19,7 @@ import util.RunUtils.loadAndTranslate import scala.collection.mutable -class DifferentialTest extends AnyFunSuite { +class DifferentialAnalysisTest extends AnyFunSuite { Logger.setLevel(LogLevel.WARN) @@ -72,10 +72,17 @@ class DifferentialTest extends AnyFunSuite { ictx = IRTransform.doCleanup(ictx) var comparectx = IRLoading.load(loading) - comparectx = IRTransform.doCleanup(ictx) + comparectx = IRTransform.doCleanup(comparectx) + + ir.transforms.clearParams(ictx.program) + + ir.transforms.clearParams(comparectx.program) + val analysisres = RunUtils.staticAnalysis(staticAnalysisConfig, comparectx) if (simplify) { + ictx = ir.transforms.liftProcedureCallAbstraction(ictx) + comparectx = ir.transforms.liftProcedureCallAbstraction(comparectx) RunUtils.doSimplify(ictx, Some(staticAnalysisConfig)) } @@ -87,41 +94,6 @@ class DifferentialTest extends AnyFunSuite { class DifferentialTestAnalysis extends DifferentialTest { - test("indirect_call_example") { - val testName = "indirect_call" - val examplePath = System.getProperty("user.dir") + s"/examples/$testName/" - testProgram(testName, examplePath) - } - - - test("jumptable2_example") { - val testName = "jumptable2" - val examplePath = System.getProperty("user.dir") + s"/examples/$testName/" - testProgram(testName, examplePath) - } - - - test("jumptable_example") { - val testName = "jumptable" - val examplePath = System.getProperty("user.dir") + s"/examples/$testName/" - testProgram(testName, examplePath) - } - - test("functionpointer_example") { - val testName = "functionpointer" - val examplePath = System.getProperty("user.dir") + s"/examples/$testName/" - testProgram(testName, examplePath) - } - - - - test("function_got_example") { - val testName = "function_got" - val examplePath = System.getProperty("user.dir") + s"/examples/$testName/" - testProgram(testName, examplePath) - } - - def runSystemTests(): Unit = { val path = System.getProperty("user.dir") + s"/src/test/correct/" @@ -132,12 +104,20 @@ class DifferentialTestAnalysis extends DifferentialTest { val programPath = path + "/" + p val variations = getSubdirectories(programPath) variations.foreach(variation => { - test("analysis_differential:" + p + "/" + variation + ":BAP") { - testProgram(p, path + "/" + p + "/" + variation + "/", suffix=".adt") + val bapPath = path + "/" + p + "/" + variation + "/" + p + ".adt" + val gtirbPath = path + "/" + p + "/" + variation + "/" + p + ".gts" + + if (File(bapPath).exists) { + test("analysis_differential:" + p + "/" + variation + ":BAP") { + testProgram(p, path + "/" + p + "/" + variation + "/", suffix=".adt") + } + } + if (File(gtirbPath).exists) { + test("analysis_differential:" + p + "/" + variation + ":GTIRB") { + testProgram(p, path + "/" + p + "/" + variation + "/", suffix=".gts") + } } - //test("analysis_differential:" + p + "/" + variation + ":GTIRB") { - // testProgram(p, path + "/" + p + "/" + variation + "/", suffix=".gts") - //} + } ) } @@ -147,7 +127,7 @@ class DifferentialTestAnalysis extends DifferentialTest { runSystemTests() } -class DifferentialTestSimplification extends DifferentialTest { +class DifferentialAnalysisTestSimplification extends DifferentialTest { def runSystemTests(): Unit = { @@ -159,12 +139,20 @@ class DifferentialTestSimplification extends DifferentialTest { val programPath = path + "/" + p val variations = getSubdirectories(programPath) variations.foreach(variation => { - test("analysis_differential:" + p + "/" + variation + ":BAP") { - testProgram(p, path + "/" + p + "/" + variation + "/", suffix=".adt", simplify=true) + + val bapPath = path + "/" + p + "/" + variation + "/" + p + ".adt" + val gtirbPath = path + "/" + p + "/" + variation + "/" + p + ".gts" + if (File(bapPath).exists) { + test("analysis_differential:" + p + "/" + variation + ":BAP") { + testProgram(p, path + "/" + p + "/" + variation + "/", suffix=".adt") + } + } + if (File(gtirbPath).exists) { + test("analysis_differential:" + p + "/" + variation + ":GTIRB") { + testProgram(p, path + "/" + p + "/" + variation + "/", suffix=".gts") + } } - //test("analysis_differential:" + p + "/" + variation + ":GTIRB") { - // testProgram(p, path + "/" + p + "/" + variation + "/", suffix=".gts") - //} + } ) }