IR Program Slicing

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<str>"
+    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
     )
 

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]

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)