Non-deterministic GoTos for indirect call resolution

src/main/scala/Main.scala

@@ -8,7 +8,7 @@ import util.RunUtils
 import scala.collection.mutable.{ArrayBuffer, Set}
 import scala.collection.{immutable, mutable}
 import scala.language.postfixOps
-import scala.sys.process._
+import scala.sys.process.*
 import util.*
 import mainargs.{main, arg, ParserForClass, Flag}
 
@@ -35,7 +35,11 @@ object Main {
       @arg(name = "dump-il", doc = "Dump the Intermediate Language to text.")
       dumpIL: Option[String],
       @arg(name = "help", short = 'h', doc = "Show this help message.")
-      help: Flag
+      help: Flag,
+      @arg(name = "analysis-results", doc = "Log analysis results in files at specified path.")
+      analysisResults: Option[String],
+      @arg(name = "analysis-results-dot", doc = "Log analysis results in .dot form at specified path.")
+      analysisResultsDot: Option[String]
   )
 
   def main(args: Array[String]): Unit = {
@@ -61,12 +65,12 @@ object Main {
     val q = BASILConfig(
       loading = ILLoadingConfig(conf.adtFileName, conf.relfFileName, conf.specFileName, conf.dumpIL),
       runInterpret = conf.interpret.value,
-      staticAnalysis =  if (conf.analyse.value) then Some(StaticAnalysisConfig(conf.dumpIL)) else None,
-      boogieTranslation = BoogieGeneratorConfig(if (conf.lambdaStores.value) then BoogieMemoryAccessMode.LambdaStoreSelect else BoogieMemoryAccessMode.SuccessiveStoreSelect),
-      outputPrefix = conf.outFileName
+      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),
+      outputPrefix = conf.outFileName,
     )
 
-    RunUtils.run(q);
+    RunUtils.run(q)
   }
 
 }

src/main/scala/cfg_visualiser/Output.scala

@@ -7,71 +7,6 @@ import analysis._
   */
 object Output {
 
-  /** Generate an output to a file.
-    * @param file
-    *   the output file
-    * @param kind
-    *   output kind (determines the file name suffix)
-    * @param outFolder
-    *   the output directory
-    */
-  def output(kind: OutputKind, content: String, fileName: String): Unit = {
-    val extension = kind match {
-      case OtherOutput(OutputKindE.`cfg`)  => "_cfg.dot"
-      case OtherOutput(OutputKindE.`icfg`) => "_icfg.dot"
-//      case DataFlowOutput(k) =>
-//        s"_$k.dot"
-      case _ => ???
-    }
-    val outFile = new File(s"$fileName.dot")
-    val pw = new PrintWriter(outFile, "UTF-8")
-    pw.write(content)
-    pw.close()
-  }
-
-  /** Escapes special characters in the given string. Special characters are all Unicode chars except 0x20-0x7e but
-    * including \, ", {, and }.
-    */
-  def escape(s: String): String = {
-    if (s == null)
-      return null
-    val b = new StringBuilder()
-    for (i <- 0 until s.length) {
-      val c = s.charAt(i)
-      c match {
-        case '"' =>
-          b.append("\\\"")
-        case '\\' =>
-          b.append("\\\\")
-        case '\b' =>
-          b.append("\\b")
-        case '\t' =>
-          b.append("\\t")
-        case '\n' =>
-          b.append("\\n")
-        case '\r' =>
-          b.append("\\r")
-        case '\f' =>
-          b.append("\\f")
-        case '<' =>
-          b.append("\\<")
-        case '>' =>
-          b.append("\\>")
-        case '{' =>
-          b.append("\\{")
-        case '}' =>
-          b.append("\\}")
-        case _ =>
-          if (c >= 0x20 && c <= 0x7e)
-            b.append(c)
-          else {
-            b.append("\\%04X".format(c.toInt))
-          }
-      }
-    }
-    b.toString()
-  }
-
   /** Helper function for producing string output for a control-flow graph node after an analysis.
     * @param res
     *   map from control-flow graph nodes to strings, as produced by the analysis
@@ -99,18 +34,4 @@ object Output {
       case callRet: CfgCallReturnNode     => s"callreturn_$uniqueId"
       case _                              => ???
     }
-}
-
-/** Different kinds of output (determine output file names).
-  */
-object OutputKindE extends Enumeration {
-  val cfg, icfg = Value
-}
-
-sealed trait OutputKind
-
-/** Other output kinds (for other processing phases than the actual analysis).
-  */
-case class OtherOutput(kind: OutputKindE.Value) extends OutputKind {
-  override def toString: String = kind.toString
-}
+}

src/main/scala/translating/SpecificationLoader.scala

@@ -361,7 +361,7 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
     val params: Map[String, Parameter] = irProc match {
       case None => Map()
       case Some(p) =>
-        p.in.map { (p: Parameter) => p.name -> p }.toMap ++ p.out.map { (p: Parameter) => p.name -> p }.toMap
+        p.in.map(p => p.name -> p).toMap ++ p.out.map(p => p.name -> p).toMap
     }
 
     val requires = ctx.requires.asScala.collect { case r: ParsedRequiresContext =>

src/main/scala/util/BASILConfig.scala

@@ -2,15 +2,14 @@ package util
 
 case class ILLoadingConfig(adtFile: String, relfFile: String, specFile: Option[String], dumpIL: Option[String])
 case class BoogieGeneratorConfig(memoryFunctionType: BoogieMemoryAccessMode = BoogieMemoryAccessMode.SuccessiveStoreSelect)
-case class StaticAnalysisConfig(dumpILToPath: Option[String] = None)
+case class StaticAnalysisConfig(dumpILToPath: Option[String] = None, analysisResultsPath: Option[String] = None, analysisDotPath: Option[String] = None)
 enum BoogieMemoryAccessMode:
   case SuccessiveStoreSelect, LambdaStoreSelect
 
-case class BASILConfig(
-                   loading: ILLoadingConfig,
-                   runInterpret: Boolean = false,
-                   staticAnalysis: Option[StaticAnalysisConfig] = None,
-                   boogieTranslation: BoogieGeneratorConfig = BoogieGeneratorConfig(),
-                   outputPrefix: String
-                 )
+case class BASILConfig(loading: ILLoadingConfig,
+                       runInterpret: Boolean = false,
+                       staticAnalysis: Option[StaticAnalysisConfig] = None,
+                       boogieTranslation: BoogieGeneratorConfig = BoogieGeneratorConfig(),
+                       outputPrefix: String,
+                      )
 

src/main/scala/util/RunUtils.scala

@@ -8,7 +8,7 @@ import java.io.{BufferedWriter, FileWriter, IOException}
 import scala.jdk.CollectionConverters.*
 import analysis.solvers.*
 import analysis.*
-import cfg_visualiser.{OtherOutput, Output, OutputKindE}
+import cfg_visualiser.Output
 import bap.*
 import ir.*
 import boogie.*
@@ -24,8 +24,6 @@ import scala.collection.mutable
 object RunUtils {
   var memoryRegionAnalysisResults: Map[CfgNode, Set[MemoryRegion]] = Map()
 
-  var iterations = 0
-
   // ids reserved by boogie
   val reserved: Set[String] = Set("free")
 
@@ -93,16 +91,16 @@ object RunUtils {
     IRProgram = renamer.visitProgram(IRProgram)
 
     q.loading.dumpIL match  {
-      case Some(s) => writeToFile(serialiseIL(IRProgram), s + "-before-analysis.il")
+      case Some(s: String) => writeToFile(serialiseIL(IRProgram), s"$s-before-analysis.il")
       case _ =>
     }
 
     q.staticAnalysis match {
       case Some(analysisConfig) =>
-        IRProgram = analyse(IRProgram, externalFunctions, globals, globalOffsets)
+        IRProgram = analyse(IRProgram, externalFunctions, globals, globalOffsets, analysisConfig, 1)
 
         analysisConfig.dumpILToPath match {
-          case Some(s) => writeToFile(serialiseIL(IRProgram), s +  "-after-analysis.il")
+          case Some(s: String) => writeToFile(serialiseIL(IRProgram), s"$s-after-analysis.il")
           case _ =>
         }
       case None =>
@@ -131,15 +129,16 @@ object RunUtils {
       IRProgram: Program,
       externalFunctions: Set[ExternalFunction],
       globals: Set[SpecGlobal],
-      globalOffsets: Map[BigInt, BigInt]
+      globalOffsets: Map[BigInt, BigInt],
+      config: StaticAnalysisConfig,
+      iteration: Int
   ): Program = {
-    iterations += 1
     val subroutines = IRProgram.procedures
       .filter(p => p.address.isDefined)
-      .map { (p: Procedure) => BigInt(p.address.get) -> p.name }
+      .map(p => BigInt(p.address.get) -> p.name)
       .toMap
-    val globalAddresses = globals.map { (s: SpecGlobal) => s.address -> s.name }.toMap
-    val externalAddresses = externalFunctions.map { (e: ExternalFunction) => e.offset -> e.name }.toMap
+    val globalAddresses = globals.map(s => s.address -> s.name).toMap
+    val externalAddresses = externalFunctions.map(e => e.offset -> e.name).toMap
     Logger.info("Globals:")
     Logger.info(globalAddresses)
     Logger.info("Global Offsets: ")
@@ -156,25 +155,29 @@ object RunUtils {
     Logger.info("[!] Running Constant Propagation")
     val constPropSolver = ConstantPropagationAnalysis.WorklistSolver(cfg)
     val constPropResult: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]] = constPropSolver.analyze(true)
-    /*
-    Output.output(
-      OtherOutput(OutputKindE.cfg),
-      cfg.toDot(Output.labeler(constPropResult, constPropSolver.stateAfterNode), Output.dotIder),
-      "cpa"
-    )
-    */
-    writeToFile(printAnalysisResults(cfg, constPropResult), "cpa")
+
+    config.analysisDotPath match {
+      case Some(s) => writeToFile(cfg.toDot(Output.labeler(constPropResult, constPropSolver.stateAfterNode), Output.dotIder), s"${s}_constprop$iteration.dot")
+      case None =>
+    }
+    config.analysisResultsPath match {
+      case Some(s) =>  writeToFile(printAnalysisResults(cfg, constPropResult, iteration), s"${s}_constprop$iteration.txt")
+      case None =>
+    }
 
     Logger.info("[!] Running MRA")
     val mraSolver = MemoryRegionAnalysis.WorklistSolver(cfg, globalAddresses, globalOffsets, mergedSubroutines, constPropResult)
     val mraResult: Map[CfgNode, Set[MemoryRegion]] = mraSolver.analyze(true)
     memoryRegionAnalysisResults = mraResult
-    /* Output.output(
-      OtherOutput(OutputKindE.cfg),
-      cfg.toDot(Output.labeler(mraResult, mraSolver.stateAfterNode), Output.dotIder),
-      "mra"
-    )*/
-    writeToFile(printAnalysisResults(cfg, mraResult), "mra")
+
+    config.analysisDotPath match {
+      case Some(s) => writeToFile(cfg.toDot(Output.labeler(mraResult, mraSolver.stateAfterNode), Output.dotIder), s"${s}_mra$iteration.dot")
+      case None =>
+    }
+    config.analysisResultsPath match {
+      case Some(s) => writeToFile(printAnalysisResults(cfg, mraResult, iteration), s"${s}_mra$iteration.txt")
+      case None =>
+    }
 
     Logger.info("[!] Running MMM")
     val mmm = MemoryModelMap()
@@ -184,35 +187,39 @@ object RunUtils {
     val vsaSolver =
       ValueSetAnalysis.WorklistSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
     val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]]  = vsaSolver.analyze(false)
-    /*
-    Output.output(
-      OtherOutput(OutputKindE.cfg),
-      cfg.toDot(Output.labeler(vsaResult, vsaSolver.stateAfterNode), Output.dotIder),
-      "vsa"
-    )
-    */
-    writeToFile(printAnalysisResults(cfg, vsaResult), "vsa")
+
+    config.analysisDotPath match {
+      case Some(s) => writeToFile(cfg.toDot(Output.labeler(vsaResult, vsaSolver.stateAfterNode), Output.dotIder), s"${s}_vsa$iteration.dot")
+      case None =>
+    }
+    config.analysisResultsPath match {
+      case Some(s) =>     writeToFile(printAnalysisResults(cfg, vsaResult, iteration), s"${s}_vsa$iteration.txt")
+      case None =>
+    }
 
     Logger.info("[!] Resolving CFG")
     val (newIR, modified): (Program, Boolean) = resolveCFG(cfg, vsaResult, IRProgram)
-    /*
     if (modified) {
-      Logger.info(s"[!] Analysing again (iter $iterations)")
-      return analyse(newIR, externalFunctions, globals, globalOffsets)
+      Logger.info(s"[!] Analysing again (iter $iteration)")
+      return analyse(newIR, externalFunctions, globals, globalOffsets, config, iteration + 1)
     }
-    */
-    val newCFG = ProgramCfgFactory().fromIR(newIR)
-    Output.output(OtherOutput(OutputKindE.cfg), newCFG.toDot(x => x.toString, Output.dotIder), "resolvedCFG")
 
-    Logger.info(s"[!] Finished indirect call resolution after $iterations iterations")
+    config.analysisDotPath match {
+      case Some(s) =>
+        val newCFG = ProgramCfgFactory().fromIR(newIR)
+        writeToFile(newCFG.toDot(x => x.toString, Output.dotIder), s"${s}_resolvedCFG.dot")
+      case None =>
+    }
+
+    Logger.info(s"[!] Finished indirect call resolution after $iteration iterations")
 
     newIR
   }
 
-  def printAnalysisResults(cfg: ProgramCfg, result: Map[CfgNode, _]): String = {
+  def printAnalysisResults(cfg: ProgramCfg, result: Map[CfgNode, _], iteration: Int): String = {
     val functionEntries = cfg.nodes.collect { case n: CfgFunctionEntryNode => n }.toSeq.sortBy(_.data.name)
     val s = StringBuilder()
-
+    s.append(System.lineSeparator())
     for (f <- functionEntries) {
       val stack: mutable.Stack[CfgNode] = mutable.Stack()
       val visited: mutable.Set[CfgNode] = mutable.Set()
@@ -406,8 +413,8 @@ object RunUtils {
     (IRProgram, modified)
   }
 
-  def writeToFile(content: String, name: String): Unit = {
-    val outFile = File(name)
+  def writeToFile(content: String, fileName: String): Unit = {
+    val outFile = File(fileName)
     val pw = PrintWriter(outFile, "UTF-8")
     pw.write(content)
     pw.close()