diff options
| -rw-r--r-- | build.sbt | 1 | ||||
| -rw-r--r-- | build.sc | 3 | ||||
| -rw-r--r-- | src/test/scala/firrtl/backends/experimental/smt/end2end/EndToEndSMTSpec.scala | 63 |
3 files changed, 28 insertions, 39 deletions
@@ -36,6 +36,7 @@ lazy val firrtlSettings = Seq( "org.json4s" %% "json4s-native" % "3.6.11", "org.apache.commons" % "commons-text" % "1.8", "io.github.alexarchambault" %% "data-class" % "0.2.5", + "com.lihaoyi" %% "os-lib" % "0.7.6", ), // macros for the data-class library libraryDependencies ++= { @@ -45,7 +45,8 @@ class firrtlCrossModule(val crossScalaVersion: String) extends CrossSbtModule wi ivy"org.apache.commons:commons-text:1.8", ivy"io.github.alexarchambault::data-class:0.2.5", ivy"org.antlr:antlr4-runtime:$antlr4Version", - ivy"com.google.protobuf:protobuf-java:$protocVersion" + ivy"com.google.protobuf:protobuf-java:$protocVersion", + ivy"com.lihaoyi::os-lib:0.7.6", ) ++ { if (majorVersion == 13) Agg(ivy"org.scala-lang.modules::scala-parallel-collections:1.0.3") 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" |