diff --git a/src/main/scala/Main.scala b/src/main/scala/Main.scala index d6bb8956e7..ca9560b519 100644 --- a/src/main/scala/Main.scala +++ b/src/main/scala/Main.scala @@ -12,7 +12,7 @@ import scala.collection.{immutable, mutable} import scala.language.postfixOps import scala.sys.process.* import util.* -import mainargs.{Flag, ParserForClass, arg, main} +import mainargs.{Flag, ParserForClass, arg, main, TokensReader} import util.DSAConfig.{Checks, Prereq, Standard} import util.boogie_interaction.BoogieResultKind @@ -216,9 +216,17 @@ object Main { @arg(name = "memory-transform", doc = "Transform memory access to region accesses") memoryTransform: Flag, @arg(name = "noif", doc = "Disable information flow security transform in Boogie output") - noif: Flag + noif: Flag, + @arg(name = "slice", doc = "Block name to begin program slicing from (requires --criterion, --simplify, --dsa, and --memory-transform flags)") + slice: Option[String], + @arg(name = "criterion", doc = "Collection of comma separated variable names outlining the initial slicing criterion values (requires --slice, --simplify, --dsa, and --memory-transform flags)") + criterion: Option[List[String]] ) + implicit object ListStringRead extends TokensReader.Simple[List[String]]: + def shortName = "list" + def read(strs: Seq[String]) = Right(strs.flatMap(_.split(",\\s*")).toList) + def main(args: Array[String]): Unit = { val parser = ParserForClass[Config] val parsed = parser.constructEither(args.toSeq) @@ -327,6 +335,22 @@ object Main { ) } + val slicerConfig = (conf.slice, conf.criterion) match { + case (Some(blockLabel), Some(criterion)) => { + if !conf.memoryTransform.value then throw IllegalArgumentException("Slicer requires --memory-transform") + if !conf.simplify.value then throw IllegalArgumentException("Slicer requires --simplify") + dsa match { + case None => throw IllegalArgumentException("Slicer requires --dsa checks|standard") + case Some(Prereq) => throw IllegalArgumentException("Slicer requires --dsa checks|standard") + case _ => () + } + Some(SlicerConfig(blockLabel, criterion.toSet)) + } + case (Some(_), None) => throw IllegalArgumentException("Slicer requires both --slice AND --criterion") + case (None, Some(_)) => throw IllegalArgumentException("Slicer requires both --slice AND --criterion") + case (None, None) => None + } + if (loadingInputs.specFile.isDefined && loadingInputs.relfFile.isEmpty) { throw IllegalArgumentException("--spec requires --relf") } @@ -353,6 +377,7 @@ object Main { outputPrefix = conf.outFileName, dsaConfig = dsa, memoryTransform = conf.memoryTransform.value, + slicerConfig = slicerConfig, assertCalleeSaved = calleeSaved ) diff --git a/src/main/scala/analysis/IDEAnalysis.scala b/src/main/scala/analysis/IDEAnalysis.scala index 85934552d0..661b949155 100644 --- a/src/main/scala/analysis/IDEAnalysis.scala +++ b/src/main/scala/analysis/IDEAnalysis.scala @@ -2,9 +2,15 @@ package analysis import ir.{CFGPosition, Command, DirectCall, GoTo, Return, IndirectCall, Procedure, Program} +/** + * Adapted from Tip + * https://github.com/cs-au-dk/TIP/blob/master/src/tip/solvers/IDEAnalysis.scala + * + * The special item representing the empty element in IDE. + */ final case class Lambda() -/** Base trait for IDE analyses. +/** Transfer functions that define IDE analysis edges. * * @tparam E * Type of the function entry CFGPosition @@ -19,13 +25,9 @@ final case class Lambda() * @tparam T * type of elements of the value lattice * @tparam L - * the type of the value lattice Adapted from Tip - * https://github.com/cs-au-dk/TIP/blob/master/src/tip/solvers/IDEAnalysis.scala The special item representing the - * empty element in IDE. + * the type of the value lattice */ -trait IDEAnalysis[E, EE, C, R, D, T, L <: Lattice[T]] { - val program: Program - +trait IDETransferFunctions[E, EE, C, R, D, T, L <: Lattice[T]] { type DL = Either[D, Lambda] /** The value lattice. @@ -53,7 +55,33 @@ trait IDEAnalysis[E, EE, C, R, D, T, L <: Lattice[T]] { def edgesOther(n: CFGPosition)(d: DL): Map[DL, EdgeFunction[T]] } -// IndirectCall in these is because they are returns so that can be further tightened in future +/* Traits for Forward and Backward IDE Transfer Functions */ +trait ForwardIDETransferFunctions[D, T, L <: Lattice[T]] extends IDETransferFunctions[Procedure, Return, DirectCall, Command, D, T, L] + +trait BackwardIDETransferFunctions[D, T, L <: Lattice[T]] extends IDETransferFunctions[Return, Procedure, Command, DirectCall, D, T, L] + + +/** Base trait for IDE analyses. + * + * @tparam E + * Type of the function entry CFGPosition + * @tparam EE + * Type of the function exit CFGPosition + * @tparam C + * Type of a function call + * @tparam R + * Type of a call return site + * @tparam D + * the type of items + * @tparam T + * type of elements of the value lattice + * @tparam L + * the type of the value lattice + */ +trait IDEAnalysis[E, EE, C, R, D, T, L <: Lattice[T]] extends IDETransferFunctions[E, EE, C, R, D, T, L] { + val program: Program +} + trait ForwardIDEAnalysis[D, T, L <: Lattice[T]] extends IDEAnalysis[Procedure, Return, DirectCall, Command, D, T, L] trait BackwardIDEAnalysis[D, T, L <: Lattice[T]] extends IDEAnalysis[Return, Procedure, Command, DirectCall, D, T, L] diff --git a/src/main/scala/ir/dsl/DSL.scala b/src/main/scala/ir/dsl/DSL.scala index 484cff0bd8..c8a658976d 100644 --- a/src/main/scala/ir/dsl/DSL.scala +++ b/src/main/scala/ir/dsl/DSL.scala @@ -215,7 +215,7 @@ def directCall(lhs: Iterable[(String, Variable)], rhs: call): EventuallyCall = def directCall(tgt: String): EventuallyCall = directCall(Nil, tgt, Nil) -def directCall(tgt: String, label: Option[String]): EventuallyCall = directCall(Nil, tgt, Nil) +def directCall(tgt: String, label: Option[String]): EventuallyCall = directCall(Nil, tgt, Nil, label) def indirectCall(tgt: Variable): EventuallyIndirectCall = EventuallyIndirectCall(tgt) diff --git a/src/main/scala/ir/transforms/Slicer.scala b/src/main/scala/ir/transforms/Slicer.scala new file mode 100644 index 0000000000..7761e2c226 --- /dev/null +++ b/src/main/scala/ir/transforms/Slicer.scala @@ -0,0 +1,518 @@ +package ir.transforms + +import analysis.solvers.BackwardIDESolver +import analysis.{ + BackwardIDEAnalysis, + BackwardIDETransferFunctions, + EdgeFunction, + EdgeFunctionLattice, + Lambda, + TwoElement, + TwoElementLattice, + TwoElementTop +} +import ir.* +import ir.eval.evaluateExpr +import ir.transforms.{cleanupBlocks, stripUnreachableFunctions} +import util.{LogLevel, PerformanceTimer, SlicerConfig, SlicerLogger} + +import scala.collection.mutable + +/** + * 2 phase IR program slicer. Destructively removes statement from program. + * Phase 1 - Criterion Generation + * Phase 2 - IR Reduction + * + * @param program IR program to slice. + * @param slicerConfig Slicing config to slice wrt. + */ +class Slicer(program: Program, slicerConfig: SlicerConfig) { + protected val performanceTimer: PerformanceTimer = PerformanceTimer("Slicer Timer", LogLevel.INFO) + + /* Parses slicer config into a valid starting criterion and node */ + lazy protected val parsedConfig: Option[(Block, Set[Variable])] = { + def variables(n: Command): Set[Variable] = { + n match { + case a: LocalAssign => a.lhs.variables ++ a.rhs.variables + case a: MemoryAssign => a.lhs.variables ++ a.rhs.variables + case a: MemoryLoad => a.lhs.variables ++ a.index.variables + case m: MemoryStore => m.index.variables ++ m.value.variables + case a: Assume => a.body.variables + case a: Assert => a.body.variables + case c: DirectCall => c.outParams.values.toSet[Variable] ++ c.actualParams.values.flatMap(_.variables) + case i: IndirectCall => Set(i.target) + case r: Return => r.outParams.keys.toSet[Variable] ++ r.outParams.values.flatMap(_.variables) + case s: (NOP | GoTo | Unreachable) => Set() + } + } + + try { + val targetedBlock = program.labelToBlock(slicerConfig.blockLabel) + + val visited = mutable.Map[String, Boolean]().withDefaultValue(false) + + val detectedVariables = mutable.Set[Variable]() + val remainingNames = mutable.Set() ++ slicerConfig.initialCriterion.filter(_.nonEmpty) + + val worklist = mutable.PriorityQueue[Block]()(Ordering.by(b => -b.rpoOrder)) + worklist.addOne(targetedBlock) + + while (worklist.nonEmpty && remainingNames.nonEmpty) { + val b = worklist.dequeue + + if (!visited(b.label)) { + visited.put(b.label, true) + + val blockVars = + (b.statements.flatMap(c => variables(c)) ++ variables(b.jump)).filter(v => remainingNames.contains(v.name)) + detectedVariables.addAll(blockVars) + remainingNames.subtractAll(blockVars.map(_.name)) + + worklist.addAll(IntraProcBlockIRCursor.pred(b)) + worklist.addAll(b.calls.collect { case p if p.returnBlock.isDefined => p.returnBlock.get }) + + // Reached entry of program from target without finding variables. Re-loop from main return. + if (worklist.isEmpty && remainingNames.nonEmpty) { + program.mainProcedure.returnBlock match { + case Some(block) => worklist.addOne(block) + case None => () + } + } + } + } + + if (remainingNames.isEmpty) { + Some((targetedBlock, detectedVariables.toSet)) + } else { + SlicerLogger.error(s"Invalid criterion variables. Could not find variables: ${remainingNames.mkString(", ")}") + None + } + + } catch { + case u: NoSuchElementException => { + SlicerLogger.error(s"Invalid criterion block: ${slicerConfig.blockLabel} does not exist") + None + } + } + } + + /* Initial slicing criterion to be transformed by analysis */ + lazy protected val initialCriterion: Map[CFGPosition, Set[Variable]] = { + parsedConfig match { + case Some(targetedBlock, variables) => Map(targetedBlock.jump -> variables) + case _ => Map() + } + } + + /* Node to begin analysis from */ + lazy protected val startingNode: CFGPosition = { + parsedConfig match { + case Some(targetedBlock, _) => targetedBlock.jump + case _ => IRWalk.lastInProc(program.mainProcedure).getOrElse(program.mainProcedure) + } + } + + /** + * Criterion generation phase of slice. + * + * Transforms initial slicing criterion using IDE Solver transfers. + * Each program statement transforms the criterion to build final result. + */ + class Phase1 { + protected var nop: Option[NOP] = None + + protected def insertNOP(): Unit = startingNode match { + case c: Command => + IRWalk.prevCommandInBlock(c) match { + case Some(d: DirectCall) if d.target.returnBlock.isDefined => + nop = Some(NOP()) + c.parent.statements.insertAfter(d, nop.get) + case _ => () + } + case _ => () + } + + protected def removeNOP(): Unit = nop match { + case Some(n) => n.parent.statements.remove(n) + case _ => () + } + + /** + * Runs phase 1 to generate criterion. + * + * @return A mapping of CFGPositions to the slicing criterion for said position. + */ + def run(): Map[CFGPosition, Set[Variable]] = { + SlicerLogger.info("Slicer :: Slicing Criterion Generation - Phase1") + insertNOP() + val results = SlicerAnalysis(program, startingNode, initialCriterion) + .analyze() + .map({ case (n, e) => n -> e.keys.toSet }) + SlicerLogger.debug(s"Slicer - Analysed ${results.size} CFG Nodes") + performanceTimer.checkPoint("Finished IDE Analysis") + removeNOP() + results + } + } + + /** + * IR reduction phase. Strips away IR components that are outside the criterion domain. + * + * @param results Phase 1 results of CFGPositions to their slicing criterion. + */ + class Phase2(results: Map[CFGPosition, Set[Variable]]) { + val transferFunctions: SlicerTransfers = SlicerTransfers(initialCriterion) + + // Cache of procedure global/memory modifications + private val procedureModifies = mutable.Map[Procedure, Set[Variable]]() + private val procedureMemoryIndexes = mutable.Map[Procedure, Set[Variable]]() + + private def procedures = program.procedures.filterNot(_.isExternal.contains(true)) + + /* Generates transferred criterion for a given position -- transforms initial criterion based on statement. */ + protected def transfer(n: CFGPosition): Map[Variable, EdgeFunction[TwoElement]] = { + val func = transferFunctions.edgesOther(n) + (criterion(n).flatMap(v => func(Left(v))).toMap ++ func(Right(Lambda()))).collect { case (Left(k), v) => k -> v } + } + + /* Slicing criterion for a given position */ + protected def criterion(n: CFGPosition): Set[Variable] = { + (n match { + case c: DirectCall => transfer(c.successor).keys.toSet + case _ => results.getOrElse(n, Set()) + }) ++ initialCriterion.getOrElse(n, Set()) + } + + /* Determines if a given program statement has an impact on the criterion */ + protected def hasCriterionImpact(n: Statement): Boolean = { + val crit = criterion(n) + n match { + case c: DirectCall => + // Iff all out parameters impact criterion. + c.outParams.values.toSet.exists(crit.contains) + // Iff the criterion was directly modified by call. + || !crit.equals(results.getOrElse(c, Set())) + // Iff call modifies global variables in criterion. + || procedureModifies + .getOrElseUpdate( + c.target, + c.target.blocks + .flatMap(_.modifies.collect { case v: Variable => v }) + .toSet + ) + .exists(crit.contains) + // Iff call stores to memory index in criterion. + || procedureMemoryIndexes + .getOrElseUpdate( + c.target, + c.target.blocks + .flatMap( + _.statements.collect { case m: MemoryStore => transferFunctions.convertMemoryIndex(m.index) }.flatten + ) + .toSet + ) + .exists(crit.filter(_.isInstanceOf[Global]).contains) + case _ => { + val transferred = transfer(n) + transferred.values.toSet.contains( + transferFunctions.edgelattice.ConstEdge(transferFunctions.valuelattice.top) + ) || !crit.equals(transferred.keys) + } + } + } + + /** + * Removes procedure in parameters whose value does not modify impact the criterion for all call contexts. + * + * Based on: [[ir.transforms.removeDeadInParams]] + */ + def reduceInParams(): Unit = { + var modified = false + + for (procedure <- procedures.filter(_.entryBlock.isDefined)) { + val unused = procedure.formalInParam.filterNot(criterion(procedure).contains(_)) + + for (unusedFormalInParam <- unused) { + modified = true + procedure.formalInParam.remove(unusedFormalInParam) + + for (call <- procedure.incomingCalls()) { + call.actualParams = call.actualParams.removed(unusedFormalInParam) + } + } + } + if (modified) assert(invariant.correctCalls(program)) + } + + /* Removes procedure out parameters whose value does not modify impact the criterion for all call contexts. */ + def reduceOutParams(): Unit = { + var modified = false + + for (returnBlock <- procedures.flatMap(_.returnBlock)) { + val procedure = returnBlock.parent + + val unused = procedure.formalOutParam.filterNot(criterion(returnBlock.jump)) + + for (unusedFormalOutParam <- unused) { + modified = true + procedure.formalOutParam.remove(unusedFormalOutParam) + + returnBlock.jump match { + case r: Return => r.outParams = r.outParams.removed(unusedFormalOutParam) + case _ => ??? + } + + for (call <- procedure.incomingCalls()) { + call.outParams = call.outParams.removed(unusedFormalOutParam) + } + } + } + if (modified) assert(invariant.correctCalls(program)) + } + + /* Runs phase 2 reduction */ + def run(): Unit = { + SlicerLogger.info("Slicer :: Reductive Slicing Pass - Phase2") + + SlicerLogger.debug("Slicer - Statement Removal") + var total = 0 + var removed = 0 + for (procedure <- procedures) { + if (!program.mainProcedure.equals(procedure) && !results.contains(procedure)) { + // Procedure was not analysed therefore can be removed. + program.removeProcedure(procedure) + } else { + for (block <- procedure.blocks) { + for (statement <- block.statements) { + if (!hasCriterionImpact(statement)) { + // If statement has no impact on the criterion it can be safely removed. + removed += 1 + statement.parent.statements.remove(statement) + } + total += 1 + } + } + } + } + performanceTimer.checkPoint("Finished Statement Removal") + SlicerLogger.info(s"Slicer - Removed $removed statements (${total - removed} remaining)") + + // Remove unused in and out parameters. + SlicerLogger.debug("Slicer - Remove Dead Parameters") + assert(invariant.correctCalls(program)) + reduceInParams() + reduceOutParams() + + // Reduce and cleanup empty blocks. + SlicerLogger.debug("Slicer - Cleanup Blocks") + cleanupBlocks(program) + + // Ensure new IR structural correctness. + SlicerLogger.debug("Slicer - Invariant Checking") + assert(invariant.singleCallBlockEnd(program)) + assert(invariant.cfgCorrect(program)) + assert(invariant.blocksUniqueToEachProcedure(program)) + assert(invariant.procEntryNoIncoming(program)) + + performanceTimer.checkPoint("Finished IR Cleanup") + } + } + + /* Run program slicer to reduce program into slice */ + def run(): Unit = { + SlicerLogger.info("Slicer :: Slicer Start") + if (parsedConfig.isDefined) { + val before = program.procedures.size + stripUnreachableFunctions(program) + SlicerLogger.info( + s"Slicer - Stripping unreachable | Removed ${before - program.procedures.size} functions (${program.procedures.size} remaining)" + ) + + val results = Phase1().run() + Phase2(results).run() + + performanceTimer.checkPoint("Finished Slicer") + } else { + SlicerLogger.error("Skipping Slicer") + } + } +} + +/** + * IDE transfer functions outlining criterion modification across IDE edges. + */ +trait SlicerTransferFunctions(slicingCriterion: Map[CFGPosition, Set[Variable]]) + extends BackwardIDETransferFunctions[Variable, TwoElement, TwoElementLattice] { + + val valuelattice = TwoElementLattice() + val edgelattice = EdgeFunctionLattice(valuelattice) + import edgelattice.{ConstEdge, IdEdge} + + private def fold(variables: Iterable[Variable]): Map[DL, EdgeFunction[TwoElement]] = { + variables.map(v => Left(v) -> ConstEdge(TwoElementTop)).toMap + } + + /** + * Flow from procedure call point to return of called procedure. + * Converts criterion element from actual out -> formal out parameter. + * Prevents local variables but allows global flow. + */ + def edgesCallToEntry(call: Command, entry: Return)(d: DL): Map[DL, EdgeFunction[TwoElement]] = { + d match { + case Left(value) => { + val params = IRWalk.prevCommandInBlock(call) match { + case Some(command) => { + command match { + case c: DirectCall => c.outParams + case i: IndirectCall => Map() + case _ => ??? + } + } + case None => ??? + } + + if params.values.toSet.contains(value) + then fold(params.filter(_._2 == value).keys) + else + value match { + case g: Global => Map(d -> IdEdge()) + case _ => Map() + } + } + case Right(_) => Map(d -> IdEdge()) + } + } + + /** + * Flow from top of procedure back to after call point. + * Converts criterion element from formal in -> actual in parameter. + * Prevents local variable flow but allows global flow. + */ + def edgesExitToAfterCall(exit: Procedure, aftercall: DirectCall)(d: DL): Map[DL, EdgeFunction[TwoElement]] = { + d match { + case Left(value: LocalVar) if aftercall.actualParams.contains(value) => + fold(aftercall.actualParams(value).variables) + case Left(_: LocalVar) => Map() + case _ => Map(d -> IdEdge()) + } + } + + /** + * Flow across call point without entering called procedure. + * Directly passes all local variables not in out parameters across. + */ + def edgesCallToAfterCall(call: Command, aftercall: DirectCall)(d: DL): Map[DL, EdgeFunction[TwoElement]] = { + d match { + case Left(value: LocalVar) if aftercall.outParams.values.toSet.contains(value) => Map() + case Left(_: LocalVar) => Map(d -> IdEdge()) + case Left(_) => Map() + case Right(_) => Map(d -> IdEdge()) + } + } + + /** + * Intraprocedural criterion transforms. Adds initial slicing criterion when first visiting position if required. + */ + def edgesOther(n: CFGPosition)(d: DL): Map[DL, EdgeFunction[TwoElement]] = { + val transferEdge = intraTransferFunctions(n) + d match { + case Left(_) => transferEdge(d) + case Right(_) => transferEdge(d) ++ slicingCriterion.getOrElse(n, Set()).flatMap(v => transferEdge(Left(v))).toMap + } + } + + protected def intraTransferFunctions(n: CFGPosition)(d: DL): Map[DL, EdgeFunction[TwoElement]] = { + n match { + case p: Procedure => Map(d -> IdEdge()) + case b: Block => Map(d -> IdEdge()) + case a: LocalAssign => { + d match { + case Left(value) if value == a.lhs => fold(a.rhs.variables) + case _ => Map(d -> IdEdge()) + } + } + case a: MemoryAssign => { + d match { + case Left(value) if value == a.lhs => fold(a.rhs.variables) + case _ => Map(d -> IdEdge()) + } + } + case a: MemoryLoad => { + d match { + case Left(value) if value == a.lhs => fold(convertMemoryIndex(a.index)) + case _ => Map(d -> IdEdge()) + } + } + case m: MemoryStore => { + d match { + case Left(value) if convertMemoryIndex(m.index).contains(value) => fold(m.value.variables) + case _ => Map(d -> IdEdge()) + } + } + case a: Assume => { + d match { + case Left(_) => Map(d -> IdEdge()) ++ fold(a.body.variables) + case Right(_) => Map(d -> IdEdge()) + } + } + case a: Assert => { + d match { + case Left(_) => Map(d -> IdEdge()) ++ fold(a.body.variables) + case Right(_) => Map(d -> IdEdge()) + } + } + case c: DirectCall => Map(d -> IdEdge()) + case i: IndirectCall => { + d match { + case Left(value: Global) => Map(d -> IdEdge(), Left(i.target) -> ConstEdge(TwoElementTop)) + case _ => Map(d -> IdEdge()) + } + } + case n: NOP => Map(d -> IdEdge()) + case g: GoTo => Map(d -> IdEdge()) + case r: Return => { + d match { + case Left(value: LocalVar) => { + r.outParams.get(value) match { + case Some(returnedValue) => fold(returnedValue.variables) + case None => Map(d -> IdEdge()) + } + } + case _ => Map(d -> IdEdge()) + } + } + case u: Unreachable => Map(d -> IdEdge()) + } + } + + def convertMemoryIndex(index: Expr): Set[Variable] = { + def convertLiteral(l: Literal): Set[Variable] = { + l match { + case bv: BitVecLiteral => Set(Register(bv.toString, bv.size)) + case i: IntLiteral => Set(Register(i.toString, 0)) + case _ => Set() + } + } + + index match { + case v: Variable => Set(v) + case l: (BitVecLiteral | IntLiteral) => convertLiteral(l) + case e => { + evaluateExpr(e) match { + case Some(l: (BitVecLiteral | IntLiteral)) => convertLiteral(l) + case _ => index.variables + } + } + } + } +} + +class SlicerTransfers(slicingCriterion: Map[CFGPosition, Set[Variable]]) + extends SlicerTransferFunctions(slicingCriterion) + +class SlicerAnalysis(program: Program, startingNode: CFGPosition, slicingCriterion: Map[CFGPosition, Set[Variable]]) + extends BackwardIDESolver[Variable, TwoElement, TwoElementLattice](program) + with BackwardIDEAnalysis[Variable, TwoElement, TwoElementLattice] + with SlicerTransferFunctions(slicingCriterion) { + override def start: CFGPosition = startingNode +} diff --git a/src/main/scala/translating/IRToBoogie.scala b/src/main/scala/translating/IRToBoogie.scala index 8673100ca6..7a4f6acad6 100644 --- a/src/main/scala/translating/IRToBoogie.scala +++ b/src/main/scala/translating/IRToBoogie.scala @@ -808,7 +808,7 @@ class IRToBoogie( } else { Nil } - val jump = GoToCmd(g.targets.map(_.label).toSeq) + val jump = if (g.targets.isEmpty) then BAssume(FalseBLiteral, Some("Replaced empty goto")) else GoToCmd(g.targets.map(_.label).toSeq) conditionAssert :+ jump case r: Return => if (r.outParams.nonEmpty) { diff --git a/src/main/scala/util/BASILConfig.scala b/src/main/scala/util/BASILConfig.scala index d14ea4b32c..05a18dca38 100644 --- a/src/main/scala/util/BASILConfig.scala +++ b/src/main/scala/util/BASILConfig.scala @@ -37,6 +37,8 @@ case class StaticAnalysisConfig( irreducibleLoops: Boolean = true ) +case class SlicerConfig(blockLabel: String, initialCriterion: Set[String]) + enum DSAConfig { case Prereq, Standard, Checks } @@ -62,5 +64,6 @@ case class BASILConfig( assertCalleeSaved: Boolean = false, staticAnalysis: Option[StaticAnalysisConfig] = None, boogieTranslation: BoogieGeneratorConfig = BoogieGeneratorConfig(), - outputPrefix: String + outputPrefix: String, + slicerConfig: Option[SlicerConfig] = None ) diff --git a/src/main/scala/util/Logging.scala b/src/main/scala/util/Logging.scala index 4d8fc8d791..8c96588510 100644 --- a/src/main/scala/util/Logging.scala +++ b/src/main/scala/util/Logging.scala @@ -189,3 +189,4 @@ val ConstGenLogger = DSALogger.deriveLogger("Constraint Gen", Console.out).setLe val SVALogger = DSALogger.deriveLogger("SVA").setLevel(LogLevel.OFF) val IntervalDSALogger = DSALogger.deriveLogger("SadDSA", Console.out).setLevel(LogLevel.OFF) val StackLogger = Logger.deriveLogger("Stack").setLevel(LogLevel.OFF) +val SlicerLogger = Logger.deriveLogger("Slicer").setLevel(LogLevel.INFO) diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala index 3e94479f22..dbf831a472 100644 --- a/src/main/scala/util/RunUtils.scala +++ b/src/main/scala/util/RunUtils.scala @@ -35,7 +35,7 @@ import util.{DebugDumpIRLogger, Logger, SimplifyLogger} import java.util.Base64 import util.intrusive_list.IntrusiveList import cilvisitor.* -import ir.transforms.MemoryTransform +import ir.transforms.{MemoryTransform, Slicer} import util.DSAConfig.{Checks, Prereq, Standard} import util.LogLevel.INFO @@ -295,12 +295,14 @@ object IRTransform { ctx.program.determineRelevantMemory(ctx.globalOffsets) } - Logger.info("[!] Stripping unreachable") - val before = ctx.program.procedures.size - transforms.stripUnreachableFunctions(ctx.program, config.loading.procedureTrimDepth) - Logger.info( - s"[!] Removed ${before - ctx.program.procedures.size} functions (${ctx.program.procedures.size} remaining)" - ) + if (config.slicerConfig.isEmpty) { + Logger.info("[!] Stripping unreachable") + val before = ctx.program.procedures.size + transforms.stripUnreachableFunctions(ctx.program, config.loading.procedureTrimDepth) + Logger.info( + s"[!] Removed ${before - ctx.program.procedures.size} functions (${ctx.program.procedures.size} remaining)" + ) + } val dupProcNames = ctx.program.procedures.groupBy(_.name).filter((_, p) => p.size > 1).toList.flatMap(_(1)) assert(dupProcNames.isEmpty) @@ -999,6 +1001,10 @@ object RunUtils { } } + if (conf.slicerConfig.isDefined) { + Slicer(ctx.program, conf.slicerConfig.get).run() + } + IRTransform.prepareForTranslation(q, ctx) if (conf.generateRelyGuarantees) { diff --git a/src/test/scala/SlicerTests.scala b/src/test/scala/SlicerTests.scala new file mode 100644 index 0000000000..0c04d5230a --- /dev/null +++ b/src/test/scala/SlicerTests.scala @@ -0,0 +1,831 @@ +import ir.* +import ir.dsl.* +import ir.transforms.Slicer +import org.scalatest.funsuite.AnyFunSuite +import test_util.BASILTest +import util.* + +/** + * A collection of different scenario case unit tests for the slicer to run against. + * Manually sliced to tag IR statements as kept or removed by pass for given criterion. + */ +@test_util.tags.UnitTest +class SlicerTests extends AnyFunSuite, test_util.CaptureOutput, BASILTest { + Logger.setLevel(LogLevel.OFF) + + protected val SHOULD_REMAIN: Some[String] = Some("Should_Remain") + protected val SHOULD_DELETE: Some[String] = Some("Should_Delete") + + def createSimpleProc(name: String, statements: Seq[NonCallStatement]): EventuallyProcedure = { + proc(name, block(name + "_1", statements.:+(goto(name + "_return")): _*), block(name + "_return", ret)) + } + + def prepareProgram(program: Program): Unit = { + program.procedures.foreach(p => + val returns = p.blocks + .map(_.jump) + .filter(_.isInstanceOf[Return]) + .toSet + assert(returns.size == 1) + p.returnBlock = returns.head.parent + ) + } + + def statements(program: Program): Iterable[Statement] = { + program.procedures.flatMap(_.blocks.flatMap(_.statements)) + } + + def remainingStatements(program: Program): Iterable[Statement] = { + statements(program).filter(_.label.equals(SHOULD_REMAIN)) + } + + def deletableStatements(program: Program): Iterable[Statement] = { + statements(program).filter(_.label.equals(SHOULD_DELETE)) + } + + test("intraproceduralIRCycle") { + val program = prog( + proc( + "main", + block( + "main_1", + LocalAssign(LocalVar("Stack_x", bv32), bv32(1), SHOULD_DELETE), + LocalAssign(LocalVar("Stack_i", bv32), bv32(0)), + goto("main_2") + ), + block("main_2", LocalAssign(LocalVar("load1", bv32), LocalVar("Stack_i", bv32)), goto("main_3", "main_4")), + block("main_3", Assume(BinaryExpr(BVSGT, LocalVar("load1", bv32), bv32(19)), None, None, true), goto("main_7")), + block( + "main_4", + Assume(BinaryExpr(BVSLE, LocalVar("load1", bv32), bv32(19)), None, None, true), + LocalAssign(LocalVar("load2", bv32), Register("Global_y", 32), SHOULD_DELETE), + LocalAssign(LocalVar("load3", bv32), LocalVar("Stack_x", bv32), SHOULD_DELETE), + LocalAssign( + LocalVar("R0_7", bv32), + BinaryExpr(BVMUL, LocalVar("load3", bv32), LocalVar("load2", bv32)), + SHOULD_DELETE + ), + LocalAssign(LocalVar("Stack_x", bv32), LocalVar("R0_7", bv32), SHOULD_DELETE), + LocalAssign(LocalVar("load4", bv32), Register("Global_y", 32)), + goto("main_5", "main_6") + ), + block("main_5", Assume(BinaryExpr(EQ, LocalVar("load4", bv32), bv32(10)), None, None, true), goto("main_7")), + block( + "main_6", + Assume(UnaryExpr(BoolNOT, BinaryExpr(EQ, LocalVar("load4", bv32), bv32(10))), None, None, true), + LocalAssign(LocalVar("load5", bv32), Register("Global_y", 32)), + MemoryAssign(Register("Global_y", 32), BinaryExpr(BVADD, LocalVar("load5", bv32), bv32(5))), + LocalAssign(LocalVar("load6", bv32), LocalVar("Stack_i", bv32)), + LocalAssign(LocalVar("Stack_i", bv32), BinaryExpr(BVADD, LocalVar("load6", bv32), bv32(1))), + goto("main_2") + ), + block("main_7", LocalAssign(LocalVar("Stack_x", bv32), bv32(4), SHOULD_DELETE), goto("main_return")), + block("main_return", ret) + ) + ) + prepareProgram(program) + + val totalStatements = statements(program).size + val toBeDeleted = deletableStatements(program) + + Slicer(program, SlicerConfig("main_7", Set("Global_y"))).run() + + assert(deletableStatements(program).isEmpty) + assert(statements(program).size == totalStatements - toBeDeleted.size) + } + + /* Tests that analysis correctly terminates with infinite loop bug in code */ + test("intraInfiniteLoop") { + val program = prog( + proc( + "main", + block( + "main_1", + LocalAssign(LocalVar("Stack_x", bv32), bv32(0)), + LocalAssign(LocalVar("Stack_y", bv32), bv32(0), SHOULD_DELETE), + goto("main_2") + ), + block("main_2", LocalAssign(LocalVar("load1", bv32), LocalVar("Stack_x", bv32)), goto("main_3", "main_4")), + block( + "main_3", + Assume(BinaryExpr(BVSLE, LocalVar("load1", bv32), bv32(99))), + LocalAssign(LocalVar("load2", bv32), LocalVar("Stack_y", bv32), SHOULD_DELETE), + LocalAssign(LocalVar("Stack_y", bv32), BinaryExpr(BVADD, LocalVar("load2", bv32), bv32(1)), SHOULD_DELETE), + goto("main_2") + ), + block("main_4", Assume(BinaryExpr(BVSGT, LocalVar("load1", bv32), bv32(99))), goto("main_return")), + block("main_return", ret) + ) + ) + prepareProgram(program) + + val totalStatements = statements(program).size + val toBeDeleted = deletableStatements(program) + + Slicer(program, SlicerConfig("main_return", Set("Stack_x"))).run() + + assert(deletableStatements(program).isEmpty) + assert(statements(program).size == totalStatements - toBeDeleted.size) + } + + /* Tests that assume and assert statements are correctly removed when the slicing criterion is dead (empty) */ + test("deadCriterionStatementRemoval") { + val program = prog( + createSimpleProc( + "main", + Seq( + LocalAssign(LocalVar("load1", bv32), bv32(10)), + Assert(BinaryExpr(EQ, LocalVar("load1", bv32), bv32(10))), + Assume(BinaryExpr(EQ, LocalVar("Stack_x", bv32), bv32(10))), + LocalAssign(LocalVar("Stack_x", bv32), bv32(0)), + MemoryAssign(Register("Global_y", 32), bv32(0)), + LocalAssign(LocalVar("Stack_x", bv32), bv32(0), SHOULD_REMAIN), + MemoryAssign(Register("Global_y", 32), bv32(0), SHOULD_REMAIN) + ) + ) + ) + + prepareProgram(program) + + val totalStatements = statements(program).size + val toRemain = remainingStatements(program) + + Slicer(program, SlicerConfig("main_1", Set("Global_y", "Stack_x"))).run() + + assert(totalStatements > statements(program).size) + assert(toRemain.equals(statements(program))) + } + + /* Tests that all assume and assertion statements are preserved if the criterion is alive at that point */ + test("aliveCriterionStatementPreservation") { + val program = prog( + createSimpleProc( + "main", + Seq( + LocalAssign(LocalVar("load1", bv32), bv32(10)), + LocalAssign(LocalVar("load2", bv32), bv32(10)), + LocalAssign(LocalVar("load1", bv32), bv32(10), SHOULD_REMAIN), + LocalAssign(LocalVar("load2", bv32), bv32(10), SHOULD_REMAIN), + Assert(BinaryExpr(EQ, LocalVar("load3", bv32), bv32(10)), label = SHOULD_REMAIN), + Assume(BinaryExpr(EQ, LocalVar("load1", bv32), LocalVar("load2", bv32)), label = SHOULD_REMAIN) + ) + ) + ) + + prepareProgram(program) + + val totalStatements = statements(program).size + val toRemain = remainingStatements(program) + + Slicer(program, SlicerConfig("main_1", Set("load1"))).run() + + assert(totalStatements > statements(program).size) + assert(toRemain.equals(statements(program))) + } + + /* Tests a direct call that only impacts criterion through local variable assignment */ + test("singleCallLocalImpact") { + val program = prog( + proc( + "main", + block( + "main_1", + LocalAssign(LocalVar("Stack_n4_0", bv32), bv32(0)), + LocalAssign(LocalVar("load3", bv32), LocalVar("Stack_n4_0", bv32)), + directCall( + Seq("R0_out" -> LocalVar("R0", bv64, 3)), + "func", + Seq("R0_in" -> ZeroExtend(32, LocalVar("load3", bv32))) + ), + ret + ) + ), + proc( + "func", + Seq("R0_in" -> bv64), + Seq("R0_out" -> bv64), + block( + "func_2", + MemoryAssign(Register("Global_x", 32), bv32(2), SHOULD_DELETE), + LocalAssign(LocalVar("Stack_n20_n16", bv32), Extract(32, 0, LocalVar("R0_in", bv64))), + LocalAssign(LocalVar("load1", bv32), LocalVar("Stack_n20_n16", bv32), SHOULD_DELETE), + LocalAssign(LocalVar("Stack_n4_0", bv32), BinaryExpr(BVADD, LocalVar("load1", bv32), bv32(2)), SHOULD_DELETE), + LocalAssign(LocalVar("load2", bv32), LocalVar("Stack_n20_n16", bv32)), + ret("R0_out" -> ZeroExtend(32, BinaryExpr(BVADD, LocalVar("load2", bv32), bv32(1)))) + ) + ) + ) + prepareProgram(program) + + val totalStatements = statements(program).size + val toBeDeleted = deletableStatements(program) + + Slicer(program, SlicerConfig("main_1", Set("R0_3"))).run() + + assert(deletableStatements(program).isEmpty) + assert(statements(program).size == totalStatements - toBeDeleted.size) + } + + /* Tests a direct call that only impacts the criterion through global variable modification in called procedure */ + test("singleCallGlobalImpact") { + val program = prog( + proc( + "main", + block( + "main_1", + MemoryAssign(Register("Global_y", 32), bv32(4), SHOULD_REMAIN), + directCall("func", SHOULD_REMAIN), + ret + ) + ), + proc( + "func", + block( + "func_2", + LocalAssign(LocalVar("load0", bv32), bv32(0)), + LocalAssign(LocalVar("load1", bv32), Register("Global_y", 32), SHOULD_REMAIN), + MemoryAssign(Register("Global_y", 32), BinaryExpr(BVADD, LocalVar("load1", bv32), bv32(10)), SHOULD_REMAIN), + ret + ) + ) + ) + prepareProgram(program) + + val totalStatements = statements(program).size + val toRemain = remainingStatements(program) + + Slicer(program, SlicerConfig("main_1", Set("Global_y"))).run() + + assert(totalStatements > statements(program).size) + assert(toRemain.equals(statements(program))) + } + + /* - Tests removal of call statements when they have no impact on criterion */ + test("singleCallNoImpact") { + val program = prog( + proc( + "main", + block( + "main_1", + LocalAssign(LocalVar("load0", bv32), bv32(0), SHOULD_REMAIN), + LocalAssign(LocalVar("load1", bv32), bv32(0)), + directCall(Seq("R0_out" -> LocalVar("load2", bv32)), "func", Seq("R0_in" -> LocalVar("load1", bv32))), + goto("main_return") + ), + block("main_return", ret) + ), + proc( + "func", + Seq("R0_in" -> bv32), + Seq("R0_out" -> bv32), + block("func_1", LocalAssign(LocalVar("load3", bv32), LocalVar("R0_in", bv32)), goto("func_return")), + block("func_return", ret("R0_out" -> LocalVar("load3", bv32))) + ) + ) + prepareProgram(program) + + val totalStatements = statements(program).size + val toRemain = remainingStatements(program) + + Slicer(program, SlicerConfig("main_1", Set("load0"))).run() + + assert(totalStatements > statements(program).size) + assert(toRemain.equals(statements(program))) + } + + /* Tests a direct call that only impacts the criterion through modification that introduces new criterion in called procedure */ + test("singleCallGlobalToLocalImpact") { + val program = prog( + proc( + "main", + block( + "main_1", + LocalAssign(LocalVar("load0", bv32), bv32(4), SHOULD_REMAIN), + directCall(Seq(), "func", Seq("R0_in" -> LocalVar("load0", bv32)), SHOULD_REMAIN), + ret + ) + ), + proc( + "func", + Seq("R0_in" -> bv32), + Seq(), + block( + "func_2", + LocalAssign(LocalVar("load0", bv32), LocalVar("R0_in", bv32), SHOULD_REMAIN), + LocalAssign(LocalVar("load1", bv32), bv32(0)), + MemoryAssign(Register("Global_y", 32), LocalVar("load0", bv32), SHOULD_REMAIN), + ret + ) + ) + ) + prepareProgram(program) + + val totalStatements = statements(program).size + val toRemain = remainingStatements(program) + + Slicer(program, SlicerConfig("main_1", Set("Global_y"))).run() + + assert(totalStatements > statements(program).size) + assert(toRemain.equals(statements(program))) + } + + /* Tests cyclical procedure call termination */ + test("callCycle") { + val program = prog( + proc( + "main", + block("main_1", MemoryAssign(Register("Global_y", 32), bv32(0)), directCall("read"), goto("main_return")), + block("main_return", ret) + ), + proc( + "read", + block( + "read_1", + LocalAssign(LocalVar("load1", bv32), Register("Global_y", 32)), + MemoryAssign(Register("Global_y", 32), BinaryExpr(BVADD, LocalVar("load1", bv32), bv32(1))), + directCall("write"), + goto("read_return") + ), + block("read_return", ret) + ), + proc( + "write", + block( + "write_1", + LocalAssign(LocalVar("load1", bv32), bv32(100), SHOULD_DELETE), + LocalAssign(LocalVar("load1", bv32), Register("Global_y", 32)), + MemoryAssign(Register("Global_y", 32), BinaryExpr(BVSUB, LocalVar("load1", bv32), bv32(1))), + goto("write_return") + ), + block("write_2", Assume(BinaryExpr(BVSGT, Register("Global_y", 32), bv32(10))), goto("write_return")), + block( + "write_3", + Assume(BinaryExpr(BVSLE, Register("Global_y", 32), bv32(10))), + directCall("read"), + goto("write_return") + ), + block("write_return", ret) + ) + ) + prepareProgram(program) + + val totalStatements = statements(program).size + val toBeDeleted = deletableStatements(program) + + Slicer(program, SlicerConfig("main_1", Set("Global_y"))).run() + + assert(deletableStatements(program).isEmpty) + assert(statements(program).size == totalStatements - toBeDeleted.size) + + } + + /* Tests that local criterion is correctly handled across calls, even if both procedures have local variables with the same names */ + test("interprocedureLocalCriterionPreservation") { + val program = prog( + proc( + "main", + block( + "main_1", + LocalAssign(LocalVar("a", bv32), bv32(0), SHOULD_DELETE), + LocalAssign(LocalVar("b", bv32), bv32(0)), + LocalAssign(LocalVar("c", bv32), bv32(0)), + MemoryAssign(Register("Global_x", 32), bv32(0)), + directCall(Seq("R0_out" -> LocalVar("a", bv32)), "func", Seq("R0_in" -> LocalVar("b", bv32))), + ret + ) + ), + proc( + "func", + Seq("R0_in" -> bv32), + Seq("R0_out" -> bv32), + block( + "func_1", + LocalAssign(LocalVar("c", bv32), bv32(0), SHOULD_DELETE), + LocalAssign(LocalVar("load1", bv32), LocalVar("R0_in", bv32)), + goto("func_return") + ), + block("func_return", ret("R0_out" -> LocalVar("load1", bv32))) + ) + ) + prepareProgram(program) + + val totalStatements = statements(program).size + val toBeDeleted = deletableStatements(program) + + Slicer(program, SlicerConfig("main_1", Set("a", "Global_x", "c"))).run() + + assert(deletableStatements(program).isEmpty) + assert(statements(program).size == totalStatements - toBeDeleted.size) + } + + /* Tests that global criterion is correctly handled across calls */ + test("interprocedureGlobalCriterionReduction") { + val program = prog( + proc( + "main", + block( + "main_1", + LocalAssign(LocalVar("a", bv32), bv32(0), SHOULD_DELETE), + LocalAssign(LocalVar("b", bv32), bv32(0)), + MemoryAssign(Register("Global_x", 32), bv32(0), SHOULD_DELETE), + directCall(Seq("R0_out" -> LocalVar("a", bv32)), "func", Seq("R0_in" -> LocalVar("b", bv32))), + ret + ) + ), + proc( + "func", + Seq("R0_in" -> bv32), + Seq("R0_out" -> bv32), + block( + "func_1", + MemoryAssign(Register("Global_x", 32), bv32(0)), + LocalAssign(LocalVar("load1", bv32), LocalVar("R0_in", bv32)), + goto("func_return") + ), + block("func_return", ret("R0_out" -> LocalVar("load1", bv32))) + ) + ) + prepareProgram(program) + + val totalStatements = statements(program).size + val toBeDeleted = deletableStatements(program) + + Slicer(program, SlicerConfig("main_1", Set("a", "Global_x"))).run() + + assert(deletableStatements(program).isEmpty) + assert(statements(program).size == totalStatements - toBeDeleted.size) + } + + private def createMultiCallSingleImpact = { + val program = prog( + proc( + "main", + block( + "main_1", + MemoryAssign(Register("Global_x", 32), bv32(0)), + MemoryAssign(Register("Global_y", 32), bv32(0)), + LocalAssign(LocalVar("load0", bv32), Register("Global_x", 32)), + directCall( + Seq("R0_out" -> LocalVar("R0", bv64)), + "f", + Seq("R0_in" -> ZeroExtend(32, LocalVar("load0", bv32))) + ), + goto("main_2") + ), + block( + "main_2", + MemoryAssign(Register("Global_y", 32), bv32(0), SHOULD_REMAIN), + directCall(Seq("R0_out" -> LocalVar("R0", bv64)), "f", Seq("R0_in" -> bv64(5)), SHOULD_REMAIN), + goto("main_return") + ), + block("main_return", ret) + ), + proc( + "f", + Seq("R0_in" -> bv64), + Seq("R0_out" -> bv64), + block( + "f_1", + LocalAssign(LocalVar("Stack_n", bv32), Extract(32, 0, LocalVar("R0_in", bv64))), + LocalAssign(LocalVar("load0", bv32), Register("Global_y", 32), SHOULD_REMAIN), + MemoryAssign(Register("Global_y", 32), BinaryExpr(BVADD, LocalVar("load0", bv32), bv32(10)), SHOULD_REMAIN), + LocalAssign(LocalVar("load1", bv32), Register("Global_x", 32)), + LocalAssign(LocalVar("load2", bv32), LocalVar("Stack_n", bv32)), + LocalAssign( + LocalVar("R0", bv64), + ZeroExtend(32, BinaryExpr(BVADD, LocalVar("load1", bv32), LocalVar("load2", bv32))) + ), + goto("f_return") + ), + block("f_return", ret("R0_out" -> LocalVar("R0", bv64))) + ) + ) + prepareProgram(program) + program + } + + private def createMultiCallMultiImpact = { + val program = prog( + proc( + "main", + block( + "main_1", + MemoryAssign(Register("Global_x", 32), bv32(0)), + MemoryAssign(Register("Global_y", 32), bv32(0), SHOULD_DELETE), + LocalAssign(LocalVar("load0", bv32), Register("Global_x", 32)), + directCall( + Seq("R0_out" -> LocalVar("R0", bv64)), + "f", + Seq("R0_in" -> ZeroExtend(32, LocalVar("load0", bv32))) + ), + goto("main_2") + ), + block( + "main_2", + MemoryAssign(Register("Global_y", 32), Extract(32, 0, LocalVar("R0", bv64))), + directCall(Seq("R0_out" -> LocalVar("R0", bv64)), "f", Seq("R0_in" -> bv64(5))), + goto("main_return") + ), + block("main_return", ret) + ), + proc( + "f", + Seq("R0_in" -> bv64), + Seq("R0_out" -> bv64), + block( + "f_1", + LocalAssign(LocalVar("Stack_n", bv32), Extract(32, 0, LocalVar("R0_in", bv64))), + LocalAssign(LocalVar("load0", bv32), Register("Global_y", 32)), + MemoryAssign(Register("Global_y", 32), BinaryExpr(BVADD, LocalVar("load0", bv32), bv32(10))), + LocalAssign(LocalVar("load1", bv32), Register("Global_x", 32)), + LocalAssign(LocalVar("load2", bv32), LocalVar("Stack_n", bv32)), + LocalAssign( + LocalVar("R0", bv64), + ZeroExtend(32, BinaryExpr(BVADD, LocalVar("load1", bv32), LocalVar("load2", bv32))) + ), + goto("f_return") + ), + block("f_return", ret("R0_out" -> LocalVar("R0", bv64))) + ) + ) + prepareProgram(program) + program + } + + private def createMultiCallPartialReduction = { + val program = prog( + proc( + "main", + block( + "main_1", + directCall( + Seq("R0_out" -> LocalVar("load0", bv64), "R1_out" -> LocalVar("load1", bv32)), + "f", + Seq("R0_in" -> bv64(10), "R1_in" -> bv32(0)) + ), + goto("main_return") + ), + block("main_return", ret) + ), + proc( + "f", + Seq("R0_in" -> bv64, "R1_in" -> bv32), + Seq("R0_out" -> bv64, "R1_out" -> bv32), + block( + "f_1", + LocalAssign(LocalVar("R0", bv64), ZeroExtend(32, LocalVar("R1_in", bv32))), + LocalAssign(LocalVar("R1", bv32), bv32(50)), + goto("f_return") + ), + block("f_return", ret("R0_out" -> LocalVar("R0", bv64), "R1_out" -> LocalVar("R1", bv32))) + ) + ) + prepareProgram(program) + program + } + + /* Tests a procedure with multiple calls statements where only one of the calls has an impact on the criterion */ + test("multiCallSingleImpact") { + val program = createMultiCallSingleImpact + + val totalStatements = statements(program).size + val toRemain = remainingStatements(program) + + Slicer(program, SlicerConfig("main_return", Set("Global_y"))).run() + + assert(totalStatements > statements(program).size) + assert(toRemain.equals(statements(program))) + } + + /* Tests a procedure with multiple calls statements where all calls have an impact on the criterion */ + test("multiCallMultiImpact") { + val program = createMultiCallMultiImpact + val totalStatements = statements(program).size + val toBeDeleted = deletableStatements(program) + + Slicer(program, SlicerConfig("main_return", Set("Global_y"))).run() + + assert(deletableStatements(program).isEmpty) + assert(statements(program).size == totalStatements - toBeDeleted.size) + } + + /* Tests procedure parameter reduction when none of the parameters have an impact on the criterion */ + test("fullParameterReduction") { + val program = createMultiCallSingleImpact + val f = program.nameToProcedure("f") + + assert(f.formalInParam.size == 1) + assert(f.formalOutParam.size == 1) + + Slicer(program, SlicerConfig("main_return", Set("Global_y"))).run() + + assert(f.formalInParam.isEmpty) + assert(f.formalOutParam.isEmpty) + } + + /* Tests parameter reduction when all the parameters have an impact on the criterion */ + test("fullParameterPreservation") { + val program = createMultiCallMultiImpact + val f = program.nameToProcedure("f") + + val fInParam = f.formalInParam.toSet + val fOutParam = f.formalOutParam.toSet + + Slicer(program, SlicerConfig("main_return", Set("Global_y"))).run() + + assert(f.formalInParam.equals(fInParam)) + assert(f.formalOutParam.equals(fOutParam)) + } + + /* Tests parameter reduction when some of the in and out parameters have an impact on the criterion */ + test("partialInOutParameterReduction") { + val program = createMultiCallPartialReduction + val f = program.nameToProcedure("f") + + Slicer(program, SlicerConfig("main_return", Set("load0"))).run() + + assert(f.formalInParam.size == 1) + assert(f.formalInParam.map(v => v.name).contains("R1_in")) + + assert(f.formalOutParam.size == 1) + assert(f.formalOutParam.map(v => v.name).contains("R0_out")) + } + + /* Tests parameter reduction when some of the in parameters and all the out parameters have an impact on the criterion */ + test("partialInOnlyParameterReduction") { + val program = createMultiCallPartialReduction + val f = program.nameToProcedure("f") + + val fOutParam = f.formalOutParam.toSet + + Slicer(program, SlicerConfig("main_return", Set("load0", "load1"))).run() + + assert(f.formalInParam.size == 1) + assert(f.formalInParam.map(v => v.name).contains("R1_in")) + + assert(f.formalOutParam.equals(fOutParam)) + } + + /* Tests slicing a method that is not main to ensure it is preserved despite being 'unreachable' */ + test("sliceNonMain") { + val program = prog( + proc( + "main", + block( + "main_1", + LocalAssign(LocalVar("load0", bv32), bv32(0)), + LocalAssign(LocalVar("load1", bv32), bv32(0)), + directCall( + Seq("R0_out" -> LocalVar("R0", bv32)), + "write", + Seq("R0_in" -> LocalVar("load0", bv32), "R1_in" -> LocalVar("load1", bv32)) + ), + goto("main_return") + ), + block("main_return", ret) + ), + proc( + "write", + Seq("R0_in" -> bv32, "R1_in" -> bv32), + Seq("R0_out" -> bv32), + block( + "write_1", + directCall( + Seq("R0_out" -> LocalVar("R0", bv32)), + "read", + Seq("R0_in" -> BinaryExpr(BVADD, LocalVar("R0_in", bv32), LocalVar("R1_in", bv32))) + ), + goto("write_return") + ), + block("write_return", ret("R0_out" -> LocalVar("R0", bv32))) + ), + proc( + "read", + Seq("R0_in" -> bv32), + Seq("R0_out" -> bv32), + block( + "read_1", + LocalAssign(LocalVar("load2", bv32), LocalVar("R0_in", bv32), SHOULD_REMAIN), + LocalAssign(LocalVar("load3", bv32), BinaryExpr(BVADD, LocalVar("load2", bv32), bv32(10)), SHOULD_REMAIN), + goto("read_return") + ), + block("read_return", ret("R0_out" -> LocalVar("load3", bv32))) + ) + ) + prepareProgram(program) + + val totalStatements = statements(program).size + val toRemain = remainingStatements(program) + + Slicer(program, SlicerConfig("read_return", Set("R0_out"))).run() + + assert(totalStatements > statements(program).size) + assert(toRemain.equals(statements(program))) + } +} + +/** + * Tests that run the slicer against correct system tests to ensure that the resultant Boogie file will still verify. + */ +@test_util.tags.DisabledTest +class SlicerSystemTests extends AnyFunSuite, test_util.CaptureOutput, BASILTest { + Logger.setLevel(LogLevel.OFF) + + private val correctPath = s"${BASILTest.rootDirectory}/src/test/correct/" + + def runExample(name: String, variant: String, slicerConfig: Option[SlicerConfig] = None): (BASILResult, Boolean) = { + val inputFile = s"$correctPath/$name/$variant/$name.gts" + val relfFile = s"$correctPath/$name/$variant/$name.relf" + val staticAnalysisConfig = Some(StaticAnalysisConfig()) + val outputFile = s"$correctPath/$name/$variant/${name}_slicer.bpl" + val result = runBASIL( + inputFile, + relfFile, + None, + outputFile, + staticAnalysisConfig, + simplify = true, + dsa = Some(DSAConfig.Checks), + slicerConfig = slicerConfig + ) + val boogieOutput = runBoogie(s"$correctPath/$name", outputFile, Seq()) + val (_, verified, _) = checkVerify(boogieOutput, true) + (result, verified) + } + + def testSlicerVerification(name: String, variant: String): Unit = { + val (initialResult, initialVerified) = runExample(name, variant) + assert(initialVerified, s"Unsliced program $name does not verify") + + val slicingConfig: SlicerConfig = initialResult.ir.program.mainProcedure.returnBlock match { + case Some(block) => { + SlicerConfig( + block.label, + block.jump match { + case r: Return => r.outParams.keys.toSet.map(_.name) + case _ => ??? + } + ) + } + case None => { + assert(false, s"Program $name does not have main return") + ??? + } + } + + val (slicedResult, slicedVerified) = runExample(name, variant, Some(slicingConfig)) + assert(slicedVerified, s"Sliced program $name does not verify") + } + + def runTests(name: String): Unit = { + BASILTest.getSubdirectories(s"$correctPath/$name").foreach { v => testSlicerVerification(name, v) } + } + + test("arrays_simple") { + runTests("arrays_simple") + } + + test("basic_arrays_read") { + runTests("basic_arrays_read") + } + + test("basic_arrays_write") { + runTests("basic_arrays_write") + } + + test("basic_lock_unlock") { + runTests("basic_lock_unlock") + } + + test("basic_loop_assign") { + runTests("basic_loop_assign") + } + + test("basic_function_call_caller") { + runTests("basic_function_call_caller") + } + + test("cjump") { + runTests("cjump") + } + + test("function") { + runTests("function") + } + + test("function1") { + runTests("function1") + } + + test("functions_with_params") { + runTests("functions_with_params") + } + + test("jumptable2") { + runTests("jumptable2") + } + + test("secret_write") { + runTests("secret_write") + } +} diff --git a/src/test/scala/test_util/BASILTest.scala b/src/test/scala/test_util/BASILTest.scala index 69700b5dc9..3a90efb9cd 100644 --- a/src/test/scala/test_util/BASILTest.scala +++ b/src/test/scala/test_util/BASILTest.scala @@ -12,6 +12,7 @@ import util.{ IRContext, Logger, RunUtils, + SlicerConfig, StaticAnalysisConfig } import util.boogie_interaction.* @@ -31,7 +32,8 @@ case class TestConfig( simplify: Boolean = false, summariseProcedures: Boolean = false, dsa: Option[DSAConfig] = None, - memoryTransform: Boolean = false + memoryTransform: Boolean = false, + slicerConfig: Option[SlicerConfig] = None ) { private val scaledtimespans = new ScaledTimeSpans {} def timeoutFlag = @@ -51,6 +53,7 @@ trait BASILTest { summariseProcedures: Boolean = false, dsa: Option[DSAConfig] = None, memoryTransform: Boolean = false, + slicerConfig: Option[SlicerConfig] = None, postLoad: IRContext => Unit = s => () ): BASILResult = { val specFile = if (specPath.isDefined && File(specPath.get).exists) { @@ -68,7 +71,8 @@ trait BASILTest { util.BoogieGeneratorConfig().copy(memoryFunctionType = util.BoogieMemoryAccessMode.SuccessiveStoreSelect), outputPrefix = BPLPath, dsaConfig = dsa, - memoryTransform = memoryTransform + memoryTransform = memoryTransform, + slicerConfig = slicerConfig ) val result = RunUtils.loadAndTranslate(config, postLoad = postLoad) RunUtils.writeOutput(result) @@ -107,7 +111,7 @@ trait BASILTest { case BoogieResultKind.AssertionFailed if expectVerify => Some("Expected verification success, but got failure.") case k: BoogieResultKind.Unknown => Some(k.toString) } - (failureMsg, boogieResult.kind == BoogieResultKind.Verified, boogieResult.kind == BoogieResultKind.Timeout) + (failureMsg, boogieResult.kind.isInstanceOf[BoogieResultKind.Verified], boogieResult.kind == BoogieResultKind.Timeout) } }