fix

src/main/scala/ir/Program.scala

@@ -201,7 +201,7 @@ class Procedure private (
                   var ensures: List[BExpr],
                 ) extends Iterable[CFGPosition] {
 
-  def name = procName //  + address.map("_" + _).getOrElse("") 
+  def name = procName + address.map("_" + _).getOrElse("") 
 
   private val _callers = mutable.HashSet[DirectCall]()
   _blocks.foreach(_.parent = this)

src/main/scala/ir/eval/Interpreter.scala

@@ -325,6 +325,14 @@ object LibcIntrinsic {
     _ <- s.doReturn()
   } yield (())
 
+  def twoArg[S, E, T <: Effects[S, E]](name: String)(s: T): State[S, Unit, E] = for {
+    c1 <- s.loadVar("R0")
+    c2 <- s.loadVar("R1")
+    res <- s.callIntrinsic(name, List(c1, c2))
+    _ <- if res.isDefined then s.storeVar("R0", Scope.Global, res.get) else State.pure(())
+    _ <- s.doReturn()
+  } yield (())
+
   def calloc[S, T <: Effects[S, InterpreterError]](s: T): State[S, Unit, InterpreterError] = for {
     size <- s.loadVar("R0")
     res <- s.callIntrinsic("malloc", List(size))
@@ -343,6 +351,7 @@ object LibcIntrinsic {
       "putchar" -> singleArg("putc"),
       "puts" -> singleArg("puts"),
       "printf" -> singleArg("print"),
+      "write" -> twoArg("write"),
       "malloc" -> singleArg("malloc"),
       "__libc_malloc_impl" -> singleArg("malloc"),
       "free" -> singleArg("free"),
@@ -394,6 +403,27 @@ object IntrinsicImpl {
     } yield (Some(filecount.head))
   }
 
+
+  def write[S, T <: Effects[S, InterpreterError]](f: T)(fd: BasilValue, strptr: BasilValue): State[S, Option[BasilValue], InterpreterError] = {
+    for {
+      str <- Eval.getNullTerminatedString(f)("mem", strptr)
+      // TODO: fd mapping in state
+      file = fd match {
+        case Scalar(BitVecLiteral(1, 64)) => "stdout"
+        case Scalar(BitVecLiteral(2, 64)) => "stderr"
+        case _ => "unknown"
+      }
+      baseptr: List[BasilValue] <- f.loadMem("ghost-file-bookkeeping", List(Symbol(s"${file}-ptr")))
+      offs: List[BasilValue] <- State.mapM(
+        ((i: Int) => State.pureE(BasilValue.unsafeAdd(baseptr.head, i))),
+        (0 until (str.size + 1))
+      )
+      _ <- f.storeMem(file, offs.zip(str.map(Scalar(_))).toMap)
+      naddr <- State.pureE(BasilValue.unsafeAdd(baseptr.head, str.size))
+      _ <- f.storeMem("ghost-file-bookkeeping", Map(Symbol(s"${file}-ptr") -> naddr))
+    } yield (None)
+  }
+
   def print[S, T <: Effects[S, InterpreterError]](f: T)(strptr: BasilValue): State[S, Option[BasilValue], InterpreterError] = {
     for {
       str <- Eval.getNullTerminatedString(f)("mem", strptr)
@@ -452,6 +482,7 @@ object NormalInterpreter extends Effects[InterpreterState, InterpreterError] {
         } yield (Some(r))
       case "print" => IntrinsicImpl.print(this)(args.head)
       case "puts"  => IntrinsicImpl.print(this)(args.head) >> IntrinsicImpl.putc(this)(Scalar(BitVecLiteral('\n'.toInt, 64)))
+      case "write"  => IntrinsicImpl.write(this)(args(1), args(2))
       case _       => State.setError(Errored(s"Call undefined intrinsic $name"))
     }
   }

src/main/scala/util/Logging.scala

@@ -55,7 +55,7 @@ class GenericLogger(
     if (level.id < LogLevel.OFF.id) {
       val l = deriveLogger(file.getName(), file)
       l.print(content)
-      close()
+      l.close()
       children.remove(l)
     }
   }
@@ -159,7 +159,6 @@ val StaticAnalysisLogger  = Logger.deriveLogger("analysis", System.out)
 val SimplifyLogger = Logger.deriveLogger("simplify", System.out)
 val DebugDumpIRLogger = {
   val l = Logger.deriveLogger("debugdumpir")
-  l.setLevel(LogLevel.OFF)
   l
 }
 val VSALogger = StaticAnalysisLogger.deriveLogger("vsa")

src/main/scala/util/RunUtils.scala

@@ -322,15 +322,15 @@ object StaticAnalysis {
     StaticAnalysisLogger.debug("Subroutine Addresses:")
     StaticAnalysisLogger.debug(subroutines)
 
-    StaticAnalysisLogger.info("reducible loops")
+    StaticAnalysisLogger.debug("reducible loops")
     // reducible loops
     val detector = LoopDetector(IRProgram)
     val foundLoops = detector.identify_loops()
-    foundLoops.foreach(l => StaticAnalysisLogger.info(s"Loop found: ${l.name}"))
+    foundLoops.foreach(l => StaticAnalysisLogger.debug(s"Loop found: ${l.name}"))
 
     val transformer = LoopTransform(foundLoops)
     val newLoops = transformer.llvm_transform()
-    newLoops.foreach(l => StaticAnalysisLogger.info(s"Loop found: ${l.name}"))
+    newLoops.foreach(l => StaticAnalysisLogger.debug(s"Loop found: ${l.name}"))
 
     config.analysisDotPath.foreach { s =>
       DebugDumpIRLogger.writeToFile(File(s"${s}_graph-after-reduce-$iteration.dot"), dotBlockGraph(IRProgram, IRProgram.map(b => b -> b.toString).toMap))
@@ -342,24 +342,23 @@ object StaticAnalysis {
     val domain = computeDomain(IntraProcIRCursor, IRProgram.procedures)
     val interDomain = computeDomain(InterProcIRCursor, IRProgram.procedures)
 
-    StaticAnalysisLogger.info("[!] Running ANR")
+    StaticAnalysisLogger.debug("[!] Running ANR")
     val ANRSolver = ANRAnalysisSolver(IRProgram)
     val ANRResult = ANRSolver.analyze()
 
-
-    StaticAnalysisLogger.info("[!] Running RNA")
+    StaticAnalysisLogger.debug("[!] Running RNA")
     val RNASolver = RNAAnalysisSolver(IRProgram)
     val RNAResult = RNASolver.analyze()
 
-    StaticAnalysisLogger.info("[!] Running Inter-procedural Constant Propagation")
+    StaticAnalysisLogger.debug("[!] Running Inter-procedural Constant Propagation")
     val interProcConstProp = InterProcConstantPropagation(IRProgram)
     val interProcConstPropResult: Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]] = interProcConstProp.analyze()
 
     config.analysisResultsPath.foreach { s =>
       DebugDumpIRLogger.writeToFile(File(s"${s}OGconstprop$iteration.txt"), printAnalysisResults(IRProgram, interProcConstPropResult))
     }
 
-    StaticAnalysisLogger.info("[!] Variable dependency summaries")
+    StaticAnalysisLogger.debug("[!] Variable dependency summaries")
     val scc = stronglyConnectedComponents(CallGraph, List(IRProgram.mainProcedure))
     val specGlobalAddresses = ctx.specification.globals.map(s => s.address -> s.name).toMap
     val varDepsSummaries = VariableDependencyAnalysis(IRProgram, ctx.specification.globals, specGlobalAddresses, interProcConstPropResult, scc).analyze()
@@ -395,11 +394,11 @@ object StaticAnalysis {
       Map[CFGPosition, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]()
     }
 
-    StaticAnalysisLogger.info("[!] Running GRA")
+    StaticAnalysisLogger.debug("[!] Running GRA")
     val graSolver = GlobalRegionAnalysisSolver(IRProgram, domain.toSet, interProcConstPropResult, reachingDefinitionsAnalysisResults, mmm, previousVSAResults)
     val graResult = graSolver.analyze()
 
-    StaticAnalysisLogger.info("[!] Running MRA")
+    StaticAnalysisLogger.debug("[!] Running MRA")
     val mraSolver = MemoryRegionAnalysisSolver(IRProgram, domain.toSet, globalAddresses, globalOffsets, mergedSubroutines, interProcConstPropResult, ANRResult, RNAResult, reachingDefinitionsAnalysisResults, graResult, mmm)
     val mraResult = mraSolver.analyze()
 
@@ -426,16 +425,16 @@ object StaticAnalysis {
       )
     }
 
-    StaticAnalysisLogger.info("[!] Running MMM")
+    StaticAnalysisLogger.debug("[!] Running MMM")
     mmm.convertMemoryRegions(mraSolver.procedureToStackRegions, mraSolver.procedureToHeapRegions, mraResult, mraSolver.procedureToSharedRegions, graSolver.getDataMap, graResult)
     mmm.logRegions()
 
-    StaticAnalysisLogger.info("[!] Running Steensgaard")
+    StaticAnalysisLogger.debug("[!] Running Steensgaard")
     val steensgaardSolver = InterprocSteensgaardAnalysis(interDomain.toSet, mmm, reachingDefinitionsAnalysisResults, previousVSAResults)
     steensgaardSolver.analyze()
     val steensgaardResults = steensgaardSolver.pointsTo()
 
-    StaticAnalysisLogger.info("[!] Running VSA")
+    StaticAnalysisLogger.debug("[!] Running VSA")
     val vsaSolver = ValueSetAnalysisSolver(IRProgram, mmm, interProcConstPropResult)
     val vsaResult: Map[CFGPosition, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]] = vsaSolver.analyze()
 
@@ -446,7 +445,7 @@ object StaticAnalysis {
       )
     }
 
-    StaticAnalysisLogger.info("[!] Injecting regions")
+    StaticAnalysisLogger.debug("[!] Injecting regions")
     val regionInjector = if (config.memoryRegions) {
       val injector = RegionInjector(IRProgram, mmm)
       injector.nodeVisitor()
@@ -670,14 +669,19 @@ object RunUtils {
       val stdout = fs._1.memoryState.getMem("stdout").toList.sortBy(_._1.value).map(_._2.value.toChar).mkString("")
 
       Logger.info(s"Interpreter stdout:\n${stdout}")
-      writeToFile((fs._2.t.mkString("\n")), "interpret-trace.txt")
+
+      q.loading.dumpIL.foreach(f => {
+        val tf = f"${f}-interpret-trace.txt"
+        writeToFile((fs._2.t.mkString("\n")), tf)
+        Logger.info(s"Finished interpret: trace written to $tf")
+      })
+
       val stopState = fs._1.nextCmd
       if (stopState != eval.Stopped()) {
         Logger.error(s"Interpreter exited with $stopState")
       } else {
         Logger.info("Interpreter stopped normally.")
       }
-      Logger.info(s"Finished interpret: trace written to interpret-trace.txt")
     }
 
     IRTransform.prepareForTranslation(q, ctx)
@@ -783,7 +787,7 @@ object RunUtils {
 }
 
 def writeToFile(content: String, fileName: String): Unit = {
-  Logger.info(s"Writing $fileName (${content.size} bytes)")
+  Logger.debug(s"Writing $fileName (${content.size} bytes)")
   val outFile = File(fileName)
   val pw = PrintWriter(outFile, "UTF-8")
   pw.write(content)

src/test/make/lift-directories.mk

@@ -8,11 +8,11 @@
 NAME=$(notdir $(shell pwd))
 GIT_ROOT?=$(realpath ../../../../)
 
+#CFLAGS=-fno-pic -fno-plt
+TARGET=aarch64-linux-gnu
 GCC ?= aarch64-linux-gnu-gcc
 CLANG ?= clang-15 -target $(TARGET)
 CC ?= $(GCC)
-#CFLAGS=-fno-pic -fno-plt
-TARGET=aarch64-linux-gnu
 
 BAP?=bap
 READELF ?= aarch64-linux-gnu-readelf

src/test/scala/DifferentialAnalysisTest.scala

@@ -61,7 +61,7 @@ class DifferentialTest extends AnyFunSuite {
     assert(filterEvents(traceInit.t).mkString("\n") == filterEvents(traceRes.t).mkString("\n"))
   }
 
-  def testProgram(testName: String, examplePath: String, suffix: String =".adt", staticAnalysisConfig : StaticAnalysisConfig = StaticAnalysisConfig(None, None, None), simplify: Boolean = true) = {
+  def testProgram(testName: String, examplePath: String, suffix: String =".adt", staticAnalysisConfig : StaticAnalysisConfig = StaticAnalysisConfig(None, None, None), simplify: Boolean = false) = {
 
     val loading = ILLoadingConfig(inputFile = examplePath + testName + suffix,
       relfFile = examplePath + testName + ".relf",