From 3f3fe09a709d77d1a4360a4e31c2ec7c399438fe Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 4 Mar 2024 22:41:16 -0500 Subject: [PATCH 1/9] Bump scala-maven-plugin to latest version --- matching/pom.xml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/matching/pom.xml b/matching/pom.xml index 334f5e565..021ebea04 100644 --- a/matching/pom.xml +++ b/matching/pom.xml @@ -81,7 +81,7 @@ maven-compiler-plugin - 3.7.0 + 3.12.1 ${java.version} ${java.version} @@ -90,7 +90,7 @@ net.alchim31.maven scala-maven-plugin - 3.3.1 + 4.8.1 scala-compile-first @@ -116,7 +116,7 @@ -language:implicitConversions -language:postfixOps - + -source ${java.version} -target From 89dbcc1f11d3e4245a2d890151881524fe790b46 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 4 Mar 2024 22:42:22 -0500 Subject: [PATCH 2/9] Rely on maven.compiler.release for the Java version --- matching/pom.xml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/matching/pom.xml b/matching/pom.xml index 021ebea04..6c30015bb 100644 --- a/matching/pom.xml +++ b/matching/pom.xml @@ -83,8 +83,7 @@ maven-compiler-plugin 3.12.1 - ${java.version} - ${java.version} + ${java.version} @@ -116,12 +115,6 @@ -language:implicitConversions -language:postfixOps - - -source - ${java.version} - -target - ${java.version} - From f01e96b93bd97dc681d2ef8d3ce3a6699e62e0b5 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 4 Mar 2024 22:43:26 -0500 Subject: [PATCH 3/9] Remove unneeded -Xexperimental flag --- matching/pom.xml | 1 - 1 file changed, 1 deletion(-) diff --git a/matching/pom.xml b/matching/pom.xml index 6c30015bb..2e88cdc44 100644 --- a/matching/pom.xml +++ b/matching/pom.xml @@ -109,7 +109,6 @@ - -Xexperimental -feature -deprecation -language:implicitConversions From 2941f6da847d0fe989d940d6016e773c2ccbf6ab Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 4 Mar 2024 23:29:44 -0500 Subject: [PATCH 4/9] Explicitly import universe.LiteralTag, lest matching on universe.Literal go unchecked due to type erasure --- .../main/scala/org/kframework/backend/llvm/matching/Parser.scala | 1 + 1 file changed, 1 insertion(+) diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala index 878c69f47..e9ab71be9 100644 --- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala +++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala @@ -429,6 +429,7 @@ object Parser { val heuristicMap: Map[Char, Heuristic] = { import scala.reflect.runtime.universe + import universe.LiteralTag val heuristicType = universe.typeOf[Heuristic] val heuristicClass = heuristicType.typeSymbol.asClass From 947b339b484e7ae2580209afcefb049afd4b4621 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 4 Mar 2024 23:32:41 -0500 Subject: [PATCH 5/9] Enable -Werror --- matching/pom.xml | 1 + .../backend/llvm/matching/Constructor.scala | 3 +++ .../backend/llvm/matching/Matrix.scala | 27 ++++++++++--------- .../llvm/matching/pattern/Pattern.scala | 5 +++- .../llvm/matching/pattern/SortCategory.scala | 1 + 5 files changed, 24 insertions(+), 13 deletions(-) diff --git a/matching/pom.xml b/matching/pom.xml index 2e88cdc44..c8ebba204 100644 --- a/matching/pom.xml +++ b/matching/pom.xml @@ -109,6 +109,7 @@ + -Werror -feature -deprecation -language:implicitConversions diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala index 5b1a1a127..5e115bed4 100644 --- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala +++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala @@ -19,6 +19,7 @@ case class Empty() extends Constructor { f.sortInfo.category match { case SetS() => SetP(Seq(), None, symbol, SymbolP(symbol, Seq())) case MapS() => MapP(Seq(), Seq(), None, symbol, SymbolP(symbol, Seq())) + case _ => ??? } } override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this) @@ -118,6 +119,7 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op concat(element(key, value), child) ) } + case _ => ??? } } override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this) @@ -166,6 +168,7 @@ case class HasNoKey(isSet: Boolean, key: Option[Pattern[Option[Occurrence]]]) ex concat(element(wildcard, wildcard), child) ) } + case _ => ??? } } override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this) diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala index e327a6efb..bc495def4 100644 --- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala +++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala @@ -781,18 +781,20 @@ class Matrix private ( ) } // fill out the bindings for list range variables - val withRanges = row.clause.listRanges.foldRight(sc) { case ((o @ Num(_, o2), hd, tl), dt) => - Function( - "hook_LIST_range_long", - o, - Seq( - (o2, "LIST.List"), - (Lit(hd.toString, "MINT.MInt 64"), "MINT.MInt 64"), - (Lit(tl.toString, "MINT.MInt 64"), "MINT.MInt 64") - ), - "LIST.List", - dt - ) + val withRanges = row.clause.listRanges.foldRight(sc) { + case ((o @ Num(_, o2), hd, tl), dt) => + Function( + "hook_LIST_range_long", + o, + Seq( + (o2, "LIST.List"), + (Lit(hd.toString, "MINT.MInt 64"), "MINT.MInt 64"), + (Lit(tl.toString, "MINT.MInt 64"), "MINT.MInt 64") + ), + "LIST.List", + dt + ) + case _ => ??? } val withOverloads = row.clause.overloadChildren.foldRight(withRanges) { case ((SymbolC(inj), f, v), dt) => @@ -810,6 +812,7 @@ class Matrix private ( ), dt ) + case _ => ??? } val withSpecials = row.clause.specializedVars.foldRight(withOverloads) { case ((o, p), dt) => MakePattern(o, p._1.hookAtt, p._2, dt) diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala index 8f63cc406..4af8acc26 100644 --- a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala +++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala @@ -4,7 +4,6 @@ import com.runtimeverification.k.kore import com.runtimeverification.k.kore.implementation.{ DefaultBuilders => B } import com.runtimeverification.k.kore.SymbolOrAlias import org.kframework.backend.llvm.matching._ -import scala.math.min sealed trait Pattern[T] { def signature(clause: Clause): Seq[Constructor] @@ -365,6 +364,7 @@ case class MapP[T] private ( case (HasNoKey(_, Some(p)), _) => !keys.map(_.canonicalize(clause)).contains(p) case (HasKey(_, _, None), None) => keys.nonEmpty && clause.action.priority <= maxPriority case (HasNoKey(_, None), _) => keys.nonEmpty && clause.action.priority > maxPriority + case _ => ??? } def score( h: Heuristic, @@ -419,6 +419,7 @@ case class MapP[T] private ( } else { Seq(keys.head, values.head, MapP(keys.tail, values.tail, frame, ctr, orig)) } + case _ => ??? } def expandOr: Seq[Pattern[T]] = { val withKeys = keys.indices.foldLeft(Seq(this))((accum, ix) => @@ -593,6 +594,7 @@ case class SetP[T] private ( case (HasNoKey(_, Some(p)), _) => !elements.map(_.canonicalize(clause)).contains(p) case (HasKey(_, _, None), None) => elements.nonEmpty && clause.action.priority <= maxPriority case (HasNoKey(_, None), _) => elements.nonEmpty && clause.action.priority > maxPriority + case _ => ??? } def score( h: Heuristic, @@ -640,6 +642,7 @@ case class SetP[T] private ( } else { Seq(elements.head, SetP(elements.tail, frame, ctr, orig)) } + case _ => ??? } def expandOr: Seq[Pattern[T]] = { val withElements = elements.indices.foldLeft(Seq(this))((accum, ix) => diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala index b14de285e..210587a90 100644 --- a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala +++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala @@ -49,6 +49,7 @@ object SortCategory { MatchingException.Type.COMPILER_ERROR, "LLVM Backend does not support multisets. If you are seeing this error due to a configuration cell tagged with multiplicity=\"*\", please add either type=\"Map\" or type=\"Set\". If you still need the collection to not contain duplicates, it is recommended you also add a unique identifier each time a cell is created. You can do this with !X:Int." ); + case _ => ??? } private def getBitwidth(s: Sort, symlib: Parser.SymLib): Int = From f41f9c1bc0747454b6c852973936b1f62cc92a77 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 4 Mar 2024 23:33:37 -0500 Subject: [PATCH 6/9] Remove unneeded -language:implicitConversions and -language:postfixOps flags --- matching/pom.xml | 2 -- 1 file changed, 2 deletions(-) diff --git a/matching/pom.xml b/matching/pom.xml index c8ebba204..5b1ee7828 100644 --- a/matching/pom.xml +++ b/matching/pom.xml @@ -112,8 +112,6 @@ -Werror -feature -deprecation - -language:implicitConversions - -language:postfixOps From 6974d78842c99c46b4d536e7c39a5d6f3bfabd87 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Thu, 14 Mar 2024 16:33:46 -0400 Subject: [PATCH 7/9] Update maven hash --- nix/overlay.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nix/overlay.nix b/nix/overlay.nix index 0978acdf7..82bb62a16 100644 --- a/nix/overlay.nix +++ b/nix/overlay.nix @@ -21,7 +21,7 @@ let llvm-backend-matching = import ./llvm-backend-matching.nix { src = prev.llvm-backend-matching-src; - mvnHash = "sha256-HF6BXeCnV5I7+oRVGK8DGHjaAtHWLfEaCwtkVcQHoGU"; + mvnHash = "sha256-5wHyZF/a4seBo3gOHXkhNJimMyUaXxlSSbMeBH7ET7k="; inherit (final) maven; }; From f303f5b2ec961362a9ffc1c1f087492ffa32a8d0 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 18 Mar 2024 21:37:43 +0000 Subject: [PATCH 8/9] Add source artifacts for Scala compiler bridge (#1016) https://github.com/runtimeverification/llvm-backend/pull/1006 is failing because the Scala Maven plugin is trying to download the sources for the compiler bridge, but can't do so outside of a Nix FOD. This PR adds the bridge to the manually-downloaded Maven artifacts (as we did in https://github.com/runtimeverification/k/pull/4055) --- matching/pom.xml | 5 +++++ nix/llvm-backend-matching.nix | 6 ++++++ nix/overlay.nix | 2 +- 3 files changed, 12 insertions(+), 1 deletion(-) diff --git a/matching/pom.xml b/matching/pom.xml index 5b1ee7828..66ec6d4ab 100644 --- a/matching/pom.xml +++ b/matching/pom.xml @@ -75,6 +75,11 @@ 1.4 linux64 + + org.scala-sbt + compiler-bridge_2.12 + 1.8.0 + diff --git a/nix/llvm-backend-matching.nix b/nix/llvm-backend-matching.nix index 4dcaf0063..bdb7772dc 100644 --- a/nix/llvm-backend-matching.nix +++ b/nix/llvm-backend-matching.nix @@ -12,11 +12,17 @@ let self = maven.buildMavenPackage rec { "org.apache.maven.plugins:maven-compiler-plugin:3.7.0" ]; + manualMvnSourceArtifacts = [ + "org.scala-sbt:compiler-bridge_2.12" + ]; + passthru = { jar = "${self}/share/java/llvm-backend-matching-1.0-SNAPSHOT-jar-with-dependencies.jar"; }; + mvnParameters = "-DsecondaryCacheDir=secondary-cache"; + installPhase = '' mkdir -p $out/share/java install -Dm644 target/*.jar $out/share/java diff --git a/nix/overlay.nix b/nix/overlay.nix index 82bb62a16..1f96aedee 100644 --- a/nix/overlay.nix +++ b/nix/overlay.nix @@ -21,7 +21,7 @@ let llvm-backend-matching = import ./llvm-backend-matching.nix { src = prev.llvm-backend-matching-src; - mvnHash = "sha256-5wHyZF/a4seBo3gOHXkhNJimMyUaXxlSSbMeBH7ET7k="; + mvnHash = "sha256-2X8G3T05Pk1apA0f04Mdu/8DAB89oB9XwTBQ3KVoc/A="; inherit (final) maven; }; From bbc6c7f2830a949ef8d1c7efe6e26641c80cc3df Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Tue, 19 Mar 2024 11:27:24 -0400 Subject: [PATCH 9/9] Update Nix Maven usage --- nix/build-maven-package.nix | 9 +++++---- nix/llvm-backend-matching.nix | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/nix/build-maven-package.nix b/nix/build-maven-package.nix index 8ff94f033..890645c1b 100644 --- a/nix/build-maven-package.nix +++ b/nix/build-maven-package.nix @@ -26,12 +26,13 @@ let mvn dependency:get -Dartifact="$artifactId" -Dmaven.repo.local=$out/.m2 done - for artifactId in ${builtins.toString manualMvnSourceArtifacts} + for artifact in ${builtins.toString manualMvnSourceArtifacts} do - group=$(echo $artifactId | cut -d':' -f1) - artifact=$(echo $artifactId | cut -d':' -f2) + groupId=$(echo $artifact | cut -d':' -f1) + artifactId=$(echo $artifact | cut -d':' -f2) + version=$(echo $artifact | cut -d':' -f3) echo "downloading manual sources $artifactId" - mvn dependency:sources -DincludeGroupIds=$group -DincludeArtifactIds=$artifact -Dmaven.repo.local=$out/.m2 + mvn dependency:get -Dclassifier=sources -DgroupId=$groupId -DartifactId=$artifactId -Dversion=$version -Dmaven.repo.local=$out/.m2 done '' + lib.optionalString (!buildOffline) '' mvn package -Dmaven.repo.local=$out/.m2 ${mvnParameters} diff --git a/nix/llvm-backend-matching.nix b/nix/llvm-backend-matching.nix index bdb7772dc..fc6ae97db 100644 --- a/nix/llvm-backend-matching.nix +++ b/nix/llvm-backend-matching.nix @@ -13,7 +13,7 @@ let self = maven.buildMavenPackage rec { ]; manualMvnSourceArtifacts = [ - "org.scala-sbt:compiler-bridge_2.12" + "org.scala-sbt:compiler-bridge_2.12:1.8.0" ]; passthru = {