From dedd712ac7e19431eaa5e3cb1023c42a5d133303 Mon Sep 17 00:00:00 2001 From: Robby Date: Tue, 1 Oct 2024 15:30:27 -0500 Subject: [PATCH] Streamlined access to Slang runtime library type hierarchy. --- jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala | 2 +- jvm/src/test/scala/org/sireum/logika/LogikaTest.scala | 4 +--- shared/src/main/scala/org/sireum/logika/Logika.scala | 6 +++--- 3 files changed, 5 insertions(+), 7 deletions(-) diff --git a/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala b/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala index cdabb79d..c9a7e634 100644 --- a/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala +++ b/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala @@ -85,7 +85,7 @@ class LogikaRcTest extends SireumRcSpec { val nameExePathMap = Smt2Invoke.nameExePathMap(sireumHome) Logika.checkScript(Some(f.string), content, c, nameExePathMap, Os.numOfProcessors, th => Smt2Impl.create(c, ISZ(), th, reporter), - NoTransitionSmt2Cache.create, reporter, T, Logika.defaultPlugins, _ => (tc.typeHierarchy, rep), line, ISZ(), ISZ()) + NoTransitionSmt2Cache.create, reporter, T, Logika.defaultPlugins, line, ISZ(), ISZ()) reporter.printMessages() val name = f.name.value if (name.startsWith(failPrefix)) { diff --git a/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala b/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala index fa550ed5..15143762 100644 --- a/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala +++ b/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala @@ -32,7 +32,6 @@ import org.sireum.test._ object LogikaTest { val sireumHome: Os.Path = Os.path(Os.env("SIREUM_HOME").get).canon - lazy val (tc, rep) = lang.FrontEnd.checkedLibraryReporterPar(Runtime.getRuntime.availableProcessors) val rlimit: Z = { var r: Z = 1000000 @@ -209,8 +208,7 @@ class LogikaTest extends TestSuite { Smt2Invoke.haltOnError = T val nameExePathMap = Smt2Invoke.nameExePathMap(sireumHome) Logika.checkScript(None(), input, config, nameExePathMap, Os.numOfProcessors, th => Smt2Impl.create(config, ISZ(), - th, reporter), NoTransitionSmt2Cache.create, reporter, T, Logika.defaultPlugins, _ => (tc.typeHierarchy, rep), - 0, ISZ(), ISZ()) + th, reporter), NoTransitionSmt2Cache.create, reporter, T, Logika.defaultPlugins, 0, ISZ(), ISZ()) if (reporter.hasIssue) { msgOpt match { case Some(msg) => diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala index e2be836a..db28d7a9 100644 --- a/shared/src/main/scala/org/sireum/logika/Logika.scala +++ b/shared/src/main/scala/org/sireum/logika/Logika.scala @@ -427,7 +427,7 @@ object Logika { def checkScript(fileUriOpt: Option[String], input: String, config: Config, nameExePathMap: HashMap[String, String], maxCores: Z, smt2f: lang.tipe.TypeHierarchy => Smt2, cache: Logika.Cache, reporter: Reporter, - hasLogika: B, plugins: ISZ[Plugin], thInit: Z => (TypeHierarchy, message.Reporter), line: Z, + hasLogika: B, plugins: ISZ[Plugin], line: Z, skipMethods: ISZ[String], skipTypes: ISZ[String]): Unit = { val parsingStartTime = extension.Time.currentMillis val isWorksheet: B = fileUriOpt match { @@ -449,12 +449,12 @@ object Logika { if (!isWorksheet) { return } - val (th, rep) = extension.Cancel.cancellable(() => thInit(maxCores)) + val (tc, rep) = extension.Cancel.cancellable(() => lang.FrontEnd.checkedLibraryReporter) val typeCheckingStartTime = extension.Time.currentMillis reporter.timing(libraryDesc, typeCheckingStartTime - libraryStartTime) reporter.reports(rep.messages) val (th2, p) = extension.Cancel.cancellable(() => - lang.FrontEnd.checkWorksheet(config.parCores, Some(th), program, reporter)) + lang.FrontEnd.checkWorksheet(config.parCores, Some(tc.typeHierarchy), program, reporter)) if (!reporter.hasError) { lang.tipe.PostTipeAttrChecker.checkProgram(p, reporter) }