Use os-lib to rewrite Z3ModelChecker (#2223)

* add os-lib to dependency.

* use os-lib in Z3ModelChecker

* fix for review by Kevin.

1 files changed, 25 insertions, 38 deletions

diff --git a/src/test/scala/firrtl/backends/experimental/smt/end2end/EndToEndSMTSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/end2end/EndToEndSMTSpec.scala
index b1ba8e32..cbd4256d 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/end2end/EndToEndSMTSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/end2end/EndToEndSMTSpec.scala
@@ -2,16 +2,15 @@
 
 package firrtl.backends.experimental.smt.end2end
 
-import java.io.{File, PrintWriter}
-
 import firrtl.annotations.{Annotation, CircuitTarget, PresetAnnotation}
 import firrtl.backends.experimental.smt.{Btor2Emitter, SMTLibEmitter}
 import firrtl.options.TargetDirAnnotation
 import firrtl.stage.{FirrtlCircuitAnnotation, FirrtlStage, OutputFileAnnotation, RunFirrtlTransformAnnotation}
-import firrtl.util.BackendCompilationUtilities
+import firrtl.util.BackendCompilationUtilities.timeStamp
 import logger.{LazyLogging, LogLevel, LogLevelAnnotation}
 import org.scalatest.flatspec.AnyFlatSpec
 import org.scalatest.matchers.must.Matchers
+import os._
 
 import scala.sys.process._
 
@@ -132,7 +131,10 @@ abstract class EndToEndSMTBaseSpec extends AnyFlatSpec with Matchers {
     }
     val fir = firrtl.Parser.parse(src)
     val name = fir.main
-    val testDir = BackendCompilationUtilities.createTestDirectory("EndToEndSMT." + name)
+    // @todo rewrite BackendCompilationUtilities
+    val testBaseDir = os.pwd / "test_run_dir" / s"EndToEndSMT.$name"
+    os.makeDir.all(testBaseDir)
+    val testDir = os.temp.dir(testBaseDir, timeStamp, deleteOnExit = false)
     // we automagically add a preset annotation if an input called preset exists
     val presetAnno = if (!src.contains("input preset")) { None }
     else {
@@ -145,7 +147,7 @@ abstract class EndToEndSMTBaseSpec extends AnyFlatSpec with Matchers {
         RunFirrtlTransformAnnotation(new SMTLibEmitter),
         RunFirrtlTransformAnnotation(new Btor2Emitter),
         FirrtlCircuitAnnotation(fir),
-        TargetDirAnnotation(testDir.getAbsolutePath)
+        TargetDirAnnotation(testDir.toString)
       ) ++ presetAnno ++ annos
     )
     assert(res.collectFirst { case _: OutputFileAnnotation => true }.isDefined)
@@ -167,42 +169,33 @@ private object Z3ModelChecker extends LazyLogging {
     version
   }
 
-  def bmc(testDir: File, main: String, kmax: Int): MCResult = {
+  def bmc(testDir: Path, main: String, kmax: Int): MCResult = {
     assert(kmax >= 0 && kmax < 50, "Trying to keep kmax in a reasonable range.")
-    val smtFile = new File(testDir, main + ".smt2")
-    val header = read(smtFile)
-    val steps = (0 to kmax).map(k => new File(testDir, main + s"_step$k.smt2")).zipWithIndex
-    steps.foreach {
-      case (f, k) =>
-        writeStep(f, main, header, k)
-        val success = executeStep(f.getAbsolutePath)
-        if (!success) return MCFail(k)
+    (0 to kmax).foreach { k =>
+      val stepFile = testDir / s"${main}_step$k.smt2"
+      os.copy(testDir / s"$main.smt2", stepFile)
+      os.write.append(stepFile, s"""${step(main, k)}
+                                   |(check-sat)
+                                   |""".stripMargin)
+      val success = executeStep(stepFile)
+      if (!success) return MCFail(k)
     }
     MCSuccess
   }
 
-  private def executeStep(filename: String): Boolean = {
-    val (out, ret) = executeCmd(filename)
-    assert(ret == 0, s"expected success (0), not $ret: `$out`\nz3 $filename")
-    assert(out == "sat" || out == "unsat", s"Unexpected output: $out")
-    out == "unsat"
+  private def executeStep(path: Path): Boolean = {
+    val (out, ret) = executeCmd(path.toString)
+    assert(ret == 0, s"expected success (0), not $ret: `$out`\nz3 ${path.toString}")
+    assert(out == "sat\n" || out == "unsat\n", s"Unexpected output: $out")
+    out == "unsat\n"
   }
 
   private def executeCmd(cmd: String): (String, Int) = {
-    var out = ""
-    val log = ProcessLogger(s => out = s, logger.warn(_))
-    val ret = Process(Seq("z3", cmd)).run(log).exitValue()
-    (out, ret)
-  }
-
-  private def writeStep(f: File, main: String, header: Iterable[String], k: Int): Unit = {
-    val pw = new PrintWriter(f)
-    val lines = header ++ step(main, k) ++ List("(check-sat)")
-    lines.foreach(pw.println)
-    pw.close()
+    val process = os.proc("z3", cmd).call(stderr = ProcessOutput.Readlines(logger.warn(_)))
+    (process.out.chunks.mkString, process.exitCode)
   }
 
-  private def step(main: String, k: Int): Iterable[String] = {
+  private def step(main: String, k: Int): String = {
     // define all states
     (0 to k).map(ii => s"(declare-fun s$ii () $main$StateTpe)") ++
       // assert that init holds in state 0
@@ -215,13 +208,7 @@ private object Z3ModelChecker extends LazyLogging {
       (0 until k).map(ii => s"(assert ($main$Asserts s$ii))") ++
       // check to see if we can violate the assertions in the last state
       List(s"(assert (not ($main$Asserts s$k)))")
-  }
-
-  private def read(f: File): Iterable[String] = {
-    val source = scala.io.Source.fromFile(f)
-    try source.getLines().toVector
-    finally source.close()
-  }
+  }.mkString("\n")
 
   // the following suffixes have to match the ones in [[SMTTransitionSystemEncoder]]
   private val Transition = "_t"