From fc55324bd9543b4fe993183dd83ff87eefcdb1ff Mon Sep 17 00:00:00 2001 From: Mario Bucev Date: Fri, 8 Oct 2021 11:51:59 +0200 Subject: [PATCH] Cross-compilation for Scala 3.0, with some changes for Inox The small changes are brought to help migrate Inox to Scala 3 --- .gitignore | 4 +- .larabot.conf | 2 +- build.sbt | 17 ++++--- project/build.properties | 2 +- src/it/scala/smtlib/it/TestHelpers.scala | 11 +++-- .../smtlib/interpreters/CVC4Interpreter.scala | 16 ++++--- .../interpreters/ProcessInterpreter.scala | 44 ++++++++++--------- .../smtlib/interpreters/Z3Interpreter.scala | 15 +++++-- .../smtlib/parser/CommandsParserTests.scala | 2 +- 9 files changed, 64 insertions(+), 49 deletions(-) diff --git a/.gitignore b/.gitignore index a1bfd48..da2a724 100644 --- a/.gitignore +++ b/.gitignore @@ -6,6 +6,8 @@ target .metals .bloop .vscode +.idea +.bsp project/.bloop project/metals.sbt -project/project +project/project \ No newline at end of file diff --git a/.larabot.conf b/.larabot.conf index 379454e..56e0402 100644 --- a/.larabot.conf +++ b/.larabot.conf @@ -1,5 +1,5 @@ commands = [ - "sbt -batch ++2.12.13 it:test" + "sbt -batch it:test" ] trusted = [ diff --git a/build.sbt b/build.sbt index 7e6c72d..d68233f 100644 --- a/build.sbt +++ b/build.sbt @@ -4,23 +4,22 @@ git.useGitDescribe := true scalacOptions ++= Seq("-unchecked", "-deprecation", "-feature") -javaOptions in IntegrationTest ++= Seq("-Xss128M") +IntegrationTest / javaOptions ++= Seq("-Xss128M") -fork in IntegrationTest := true +IntegrationTest / fork := true -libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7" -libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7" % "test" +libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7" % "test;it" -logBuffered in IntegrationTest := false +IntegrationTest / logBuffered := false -parallelExecution in Test := true +Test / parallelExecution := true lazy val commonSettings = Seq( organization := "com.regblanc", name := "scala-smtlib", - scalaVersion := "2.12.13", - crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.12.13", "2.13.0", "2.13.5") + scalaVersion := "2.13.6", + crossScalaVersions := Seq("3.0.2") ) lazy val root = (project in file(".")). @@ -30,7 +29,7 @@ lazy val root = (project in file(".")). publishMavenStyle := true -publishArtifact in Test := false +Test / publishArtifact := false pomIncludeRepository := { _ => false } diff --git a/project/build.properties b/project/build.properties index 080a737..10fd9ee 100644 --- a/project/build.properties +++ b/project/build.properties @@ -1 +1 @@ -sbt.version=1.3.0 +sbt.version=1.5.5 diff --git a/src/it/scala/smtlib/it/TestHelpers.scala b/src/it/scala/smtlib/it/TestHelpers.scala index 72eb089..07fe3bf 100644 --- a/src/it/scala/smtlib/it/TestHelpers.scala +++ b/src/it/scala/smtlib/it/TestHelpers.scala @@ -44,19 +44,18 @@ trait TestHelpers { def getCVC4Interpreter: Interpreter = CVC4Interpreter.buildDefault def isZ3Available: Boolean = try { - val output: String = "z3 -help".!! + val _: String = "z3 -help".!! true } catch { - case (_: Exception) => false + case _: Exception => false } def isCVC4Available: Boolean = try { - val output: String = "cvc4".!! + // Make sure to pass a dummy option to cvc4, otherwise it starts in interactive mode (and does not exit) + val _: String = "cvc4 --version".!! true } catch { - case (e: Exception) => { - false - } + case _: Exception => false } def executeZ3(file: File)(f: (String) => Unit): Unit = { diff --git a/src/main/scala/smtlib/interpreters/CVC4Interpreter.scala b/src/main/scala/smtlib/interpreters/CVC4Interpreter.scala index 54b75bc..ffbeeeb 100644 --- a/src/main/scala/smtlib/interpreters/CVC4Interpreter.scala +++ b/src/main/scala/smtlib/interpreters/CVC4Interpreter.scala @@ -1,16 +1,22 @@ package smtlib package interpreters -import trees.Terms._ +import smtlib.lexer.Lexer +import smtlib.parser.Parser +import smtlib.printer.{Printer, RecursivePrinter} import trees.Commands._ -import trees.CommandsResponses._ -class CVC4Interpreter(executable: String, args: Array[String], tailPrinter: Boolean = false) - extends ProcessInterpreter(executable, args, tailPrinter) { +import java.io.BufferedReader + +class CVC4Interpreter(executable: String, + args: Array[String], + printer: Printer = RecursivePrinter, + parserCtor: BufferedReader => Parser = out => new Parser(new Lexer(out))) + extends ProcessInterpreter(executable, args, printer, parserCtor) { printer.printCommand(SetOption(PrintSuccess(true)), in) in.write("\n") - in.flush + in.flush() parser.parseGenResponse } diff --git a/src/main/scala/smtlib/interpreters/ProcessInterpreter.scala b/src/main/scala/smtlib/interpreters/ProcessInterpreter.scala index c501fa8..b9aca00 100644 --- a/src/main/scala/smtlib/interpreters/ProcessInterpreter.scala +++ b/src/main/scala/smtlib/interpreters/ProcessInterpreter.scala @@ -10,17 +10,20 @@ import printer._ import java.io._ -abstract class ProcessInterpreter(protected val process: Process, tailPrinter: Boolean) extends Interpreter { +abstract class ProcessInterpreter private(override val printer: Printer, + override val parser: Parser, + protected val process: Process, + protected val in: BufferedWriter, + protected val out: BufferedReader) extends Interpreter { - def this(executable: String, args: Array[String], tailPrinter: Boolean = false) = { - this(java.lang.Runtime.getRuntime.exec((executable :: args.toList).mkString(" ")), tailPrinter) - } - - lazy val in = new BufferedWriter(new OutputStreamWriter(process.getOutputStream)) - lazy val out = new BufferedReader(new InputStreamReader(process.getInputStream)) + private def this(printer: Printer, otherArgs: (Parser, Process, BufferedWriter, BufferedReader)) = + this(printer, otherArgs._1, otherArgs._2, otherArgs._3, otherArgs._4) - lazy val parser: Parser = new Parser(new Lexer(out)) - lazy val printer: Printer = if (tailPrinter) TailPrinter else RecursivePrinter + def this(executable: String, + args: Array[String], + printer: Printer = RecursivePrinter, + parserCtor: BufferedReader => Parser = out => new Parser(new Lexer(out))) = + this(printer, ProcessInterpreter.ctorHelper(executable, args, parserCtor)) def parseResponseOf(cmd: SExpr): SExpr = cmd match { case CheckSat() => parser.parseCheckSatResponse @@ -98,17 +101,16 @@ abstract class ProcessInterpreter(protected val process: Process, tailPrinter: B override def interrupt(): Unit = synchronized { kill() } +} - /* - * Manos, greatest hack: - * Process.destroyForcibly is only available on java8, - * Using the implicit conversion, if compiled with java7 - * we will fallback to Process.destroy. If compiled on java8, - * it will ignore the implicit conversion as the method exists, - * and call the native Process.destroyForcibly. - */ - private implicit class Java8Process(process: Process) { - def destroyForcibly() = process.destroy +object ProcessInterpreter { + private def ctorHelper(executable: String, + args: Array[String], + parserCtor: BufferedReader => Parser): (Parser, Process, BufferedWriter, BufferedReader) = { + val process = java.lang.Runtime.getRuntime.exec((executable :: args.toList).mkString(" ")) + val in = new BufferedWriter(new OutputStreamWriter(process.getOutputStream)) + val out = new BufferedReader(new InputStreamReader(process.getInputStream)) + val parser = parserCtor(out) + (parser, process, in, out) } - -} +} \ No newline at end of file diff --git a/src/main/scala/smtlib/interpreters/Z3Interpreter.scala b/src/main/scala/smtlib/interpreters/Z3Interpreter.scala index a1d9483..27dc972 100644 --- a/src/main/scala/smtlib/interpreters/Z3Interpreter.scala +++ b/src/main/scala/smtlib/interpreters/Z3Interpreter.scala @@ -2,14 +2,21 @@ package smtlib package interpreters import trees.Commands._ -import printer.RecursivePrinter +import printer.{Printer, RecursivePrinter} +import smtlib.lexer.Lexer +import smtlib.parser.Parser -class Z3Interpreter(executable: String, args: Array[String], tailPrinter: Boolean = false) - extends ProcessInterpreter(executable, args, tailPrinter) { +import java.io.BufferedReader + +class Z3Interpreter(executable: String, + args: Array[String], + printer: Printer = RecursivePrinter, + parserCtor: BufferedReader => Parser = out => new Parser(new Lexer(out))) + extends ProcessInterpreter(executable, args, printer, parserCtor) { printer.printCommand(SetOption(PrintSuccess(true)), in) in.write("\n") - in.flush + in.flush() parser.parseGenResponse } diff --git a/src/test/scala/smtlib/parser/CommandsParserTests.scala b/src/test/scala/smtlib/parser/CommandsParserTests.scala index aebafab..f9c6a95 100644 --- a/src/test/scala/smtlib/parser/CommandsParserTests.scala +++ b/src/test/scala/smtlib/parser/CommandsParserTests.scala @@ -402,7 +402,7 @@ class CommandsParserTests extends AnyFunSuite with TimeLimits { { val declareSort = parseUniqueCmd("(declare-sort A 3)") - assert(parseUniqueCmd("(declare-sort A 3)") === DeclareSort("A", 3)) + assert(parseUniqueCmd("(declare-sort A 3)") === DeclareSort("A", 3)) val DeclareSort(a, n) = declareSort assert(declareSort.getPos === Position(1,1)) assert(a.getPos === Position(1,15))