Merge branch 'main' into igor/z3-params

.unreleased/features/z3-stats.md

@@ -0,0 +1 @@
+Periodically print Z3 statistics when `--debug` is on (#2992)

CHANGES.md

@@ -1,6 +1,12 @@
 <!-- NOTE: This file is generated. Do not write release notes here.
  Notes for unreleased changes go in the .unreleased/ directory. -->
 
+## 0.45.6 - 2024-09-19
+
+### Features
+
+- Added an `apalache-mc.bat` file to easily start Apalache on Windows, see #2980
+
 ## 0.45.4 - 2024-09-02
 
 ### Features

VERSION

@@ -1 +1 @@
-0.45.5-SNAPSHOT
+0.45.7-SNAPSHOT

project/Dependencies.scala

@@ -21,7 +21,7 @@ object Dependencies {
     val commonsBeanutils =
       "commons-beanutils" % "commons-beanutils" % "1.9.4" // Apparently an untracked dependency of commonsConfiguration2
     val commonsConfiguration2 = "org.apache.commons" % "commons-configuration2" % "2.11.0"
-    val commonsIo = "commons-io" % "commons-io" % "2.16.1"
+    val commonsIo = "commons-io" % "commons-io" % "2.17.0"
     val guice = "com.google.inject" % "guice" % "7.0.0"
     val kiama = "org.bitbucket.inkytonik.kiama" %% "kiama" % "2.5.1"
     val logbackClassic = "ch.qos.logback" % "logback-classic" % logbackVersion
@@ -40,7 +40,7 @@ object Dependencies {
     val zio = "dev.zio" %% "zio" % zioVersion
     // Keep up to sync with version in plugins.sbt
     val zioGrpcCodgen = "com.thesamet.scalapb.zio-grpc" %% "zio-grpc-codegen" % "0.6.0-test3" % "provided"
-    val grpcNetty = "io.grpc" % "grpc-netty" % "1.66.0"
+    val grpcNetty = "io.grpc" % "grpc-netty" % "1.68.0"
     val scalapbRuntimGrpc =
       "com.thesamet.scalapb" %% "scalapb-runtime-grpc" % scalapb.compiler.Version.scalapbVersion
     // Ensures we have access to commonly used protocol buffers (e.g., google.protobuf.Struct)

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala

@@ -76,14 +76,16 @@ class BoundedCheckerPassImpl @Inject() (
 
     val smtProfile = options.common.smtprof
     val smtRandomSeed = tuning.getOrElse("smt.randomSeed", "0").toInt
+    val smtStatsSec =
+      tuning.getOrElse("smt.statsSec", SolverConfig.default.z3StatsSec.toString).toInt
     // Parse the tuning parameters that are relevant to Z3.
     // Currently, `tuning` may contain more configuration options (added by some passes) than we parse in
     // `FineTuningParser`.
     val z3Parameters = FineTuningParser.fromStrings(tuning.filter(_._1.startsWith("z3."))) match {
       case Right(params) => params.map { case (k, v) => (k.substring("z3.".length), v) }
       case Left(error)   => throw new PassOptionException(s"Error in tuning parameters: $error")
     }
-    val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtEncoding, z3Parameters)
+    val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtEncoding, smtStatsSec, z3Parameters)
 
     val result = options.checker.algo match {
       case Algorithm.Incremental => runIncrementalChecker(params, input, tuning, solverConfig)

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala

@@ -25,6 +25,7 @@ sealed case class SolverConfig(
     profile: Boolean,
     randomSeed: Int,
     smtEncoding: SMTEncoding,
+    z3StatsSec: Int,
     z3Params: Map[String, Object] = Map()) {}
 
 object SolverConfig {
@@ -34,5 +35,5 @@ object SolverConfig {
    */
   val default: SolverConfig =
     new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19,
-        z3Params = Map())
+        z3StatsSec = 60, z3Params = Map())
 }

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala

@@ -18,6 +18,7 @@ import com.typesafe.scalalogging.LazyLogging
 
 import java.io.PrintWriter
 import java.util.concurrent.atomic.AtomicLong
+import java.util.concurrent.locks.ReentrantLock
 import scala.collection.mutable
 import scala.collection.mutable.ListBuffer
 
@@ -132,17 +133,61 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
    */
   private var maxCellIdPerContext = List(-1)
 
+  private trait ContextState
+  private case class Running() extends ContextState
+  private case class Disposed() extends ContextState
+
+  // the state of the context: Running or Disposed
+  private var state: ContextState = Running()
+
+  // the lock shared between the context and the statistics thread
+  private val statisticsLock: ReentrantLock = new ReentrantLock()
+  // start a new thread to collect statistics
+  private val statisticsThread = new Thread(() => {
+    while (state == Running()) {
+      // Sleep for a while.
+      // If we call printStatistics right away, we can easily run into a race condition with Z3 initializing.
+      // This produces a core dump.
+      Thread.sleep(config.z3StatsSec * 1000)
+      // make sure that the context is not being disposed right now. Otherwise, we can get a nice core dump.
+      statisticsLock.lock()
+      try {
+        if (state == Running()) {
+          printStatistics()
+        }
+      } finally {
+        statisticsLock.unlock()
+      }
+    }
+  })
+
+  if (config.debug && config.z3StatsSec > 0) {
+    statisticsThread.start()
+  }
+
   /**
    * Dispose whatever has to be disposed in the end.
    */
   override def dispose(): Unit = {
     logger.debug(s"Disposing Z3 solver context ${id}")
-    z3context.close()
-    closeLogs()
-    cellCache.clear()
-    inCache.clear()
-    funDecls.clear()
-    cellSorts.clear()
+    state = Disposed()
+    // Try to obtain the lock, to let the statistics thread finish its work.
+    // If it is stuck for some reason, continue after the timeout in any case.
+    statisticsLock.tryLock(2 * config.z3StatsSec, java.util.concurrent.TimeUnit.SECONDS)
+    try {
+      if (config.debug) {
+        printStatistics()
+      }
+      z3context.close()
+      closeLogs()
+      cellCache.clear()
+      inCache.clear()
+      funDecls.clear()
+      cellSorts.clear()
+    } finally {
+      // it's not that important at this point, but let's unlock it for the piece of mind
+      statisticsLock.unlock()
+    }
   }
 
   /**
@@ -1026,6 +1071,14 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
     flushLogs()
     throw e
   }
+
+  private def printStatistics(): Unit = {
+    logger.info(s"Z3 statistics for context $id...")
+    val entries = z3solver.getStatistics.getEntries.map(stat => {
+      s"${stat.Key}=${stat.getValueString}"
+    })
+    logger.info(entries.mkString(",") + "\n")
+  }
 }
 
 object Z3SolverContext {

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala

@@ -183,7 +183,8 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers {
     val checkerParams = new ModelCheckerParams(checkerInput, 0)
 
     val solverContext =
-      new Z3SolverContext(new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = smtEncoding))
+      new Z3SolverContext(new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = smtEncoding,
+              z3StatsSec = 0))
     val rewriter: SymbStateRewriterImpl = smtEncoding match {
       case SMTEncoding.OOPSLA19  => new SymbStateRewriterImpl(solverContext, renaming)
       case SMTEncoding.Arrays    => new SymbStateRewriterImplWithArrays(solverContext, renaming)

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithArrays.scala

@@ -13,7 +13,7 @@ import org.scalatestplus.junit.JUnitRunner
 class TestSeqModelCheckerWithArrays extends TestSeqModelCheckerTrait {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.Arrays))
+      .createZ3(None, SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays))
     val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl)
     test(rewriter)
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala

@@ -13,7 +13,8 @@ import org.scalatestplus.junit.JUnitRunner
 class TestSeqModelCheckerWithFunArrays extends TestSeqModelCheckerTrait {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.FunArrays))
+      .createZ3(None,
+          SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays))
     val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl)
     test(rewriter)
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala

@@ -13,7 +13,8 @@ import org.scalatestplus.junit.JUnitRunner
 class TestSeqModelCheckerWithOOPSLA19 extends TestSeqModelCheckerTrait {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.OOPSLA19))
+      .createZ3(None,
+          SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19))
     val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl)
     test(rewriter)
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala

@@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner
 @RunWith(classOf[JUnitRunner])
 class TestRecordingSolverContextWithArrays extends TestRecordingSolverContext {
   override protected def withFixture(test: NoArgTest): Outcome = {
-    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.Arrays)
+    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+        smtEncoding = SMTEncoding.Arrays)
     test()
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala

@@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner
 @RunWith(classOf[JUnitRunner])
 class TestRecordingSolverContextWithFunArrays extends TestRecordingSolverContext {
   override protected def withFixture(test: NoArgTest): Outcome = {
-    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.FunArrays)
+    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+        smtEncoding = SMTEncoding.FunArrays)
     test()
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala

@@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner
 @RunWith(classOf[JUnitRunner])
 class TestRecordingSolverContextWithOOPSLA19 extends TestRecordingSolverContext {
   override protected def withFixture(test: NoArgTest): Outcome = {
-    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19)
+    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+        smtEncoding = SMTEncoding.OOPSLA19)
     test()
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala

@@ -12,7 +12,7 @@ class TestTransitionExecutorWithIncrementalAndArrays
     with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver =
-      new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0,
+      new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
               smtEncoding = SMTEncoding.Arrays))
     withFixtureInContext(solver, new IncrementalExecutionContext(_), test)
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala

@@ -11,7 +11,7 @@ class TestTransitionExecutorWithIncrementalAndFunArrays
     extends TestTransitionExecutorImpl[IncrementalExecutionContextSnapshot]
     with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
-    val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0,
+    val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
             smtEncoding = SMTEncoding.FunArrays))
     withFixtureInContext(solver, new IncrementalExecutionContext(_), test)
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala

@@ -18,7 +18,7 @@ class TestTransitionExecutorWithIncrementalAndOOPSLA19
     with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver =
-      new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0,
+      new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
               smtEncoding = SMTEncoding.OOPSLA19))
     withFixtureInContext(solver, new IncrementalExecutionContext(_), test)
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala

@@ -12,7 +12,9 @@ import org.scalatestplus.junit.JUnitRunner
 class TestTransitionExecutorWithOfflineAndArrays extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.Arrays))
+      .createZ3(None,
+          SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+              smtEncoding = SMTEncoding.Arrays))
     withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test)
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala

@@ -13,7 +13,9 @@ class TestTransitionExecutorWithOfflineAndFunArrays
     extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.FunArrays))
+      .createZ3(None,
+          SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+              smtEncoding = SMTEncoding.FunArrays))
     withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test)
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala

@@ -18,7 +18,9 @@ import org.scalatestplus.junit.JUnitRunner
 class TestTransitionExecutorWithOfflineAndOOPSLA19 extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] {
   override def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19))
+      .createZ3(None,
+          SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+              smtEncoding = SMTEncoding.OOPSLA19))
     withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test)
   }
 }