Merge branch 'develop' into showTokens

.github/workflows/release.yml

@@ -220,7 +220,7 @@ jobs:
 
   macos-build:
     name: 'Build MacOS Package'
-    runs-on: macos-11
+    runs-on: macos-13
     timeout-minutes: 120
     environment: production
     needs: [set-release-id, source-tarball]
@@ -273,7 +273,7 @@ jobs:
           git commit Formula/$PACKAGE.rb -m "Update ${PACKAGE} to ${VERSION}: part 1"
           ../kframework/package/macos/brew-build-and-update-to-local-bottle ${PACKAGE} ${VERSION} ${ROOT_URL}
           git reset HEAD^
-          LOCAL_BOTTLE_NAME=$(basename $(find . -name "kframework--${VERSION}.big_sur.bottle*.tar.gz"))
+          LOCAL_BOTTLE_NAME=$(basename $(find . -name "kframework--${VERSION}.ventura.bottle*.tar.gz"))
           BOTTLE_NAME=$(echo ${LOCAL_BOTTLE_NAME#./} | sed 's!kframework--!kframework-!')
           ../kframework/package/macos/brew-update-to-final ${PACKAGE} ${VERSION} ${ROOT_URL}
           echo "path=${LOCAL_BOTTLE_NAME}" >> ${GITHUB_OUTPUT}

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java

@@ -26,6 +26,7 @@ public List<Module> getKompileModules() {
         mods.add(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
                 installHaskellBackend(binder());
             }
@@ -54,6 +55,7 @@ public List<Module> getKRunModules() {
         return Collections.singletonList(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 installHaskellRewriter(binder());
             }
         });
@@ -74,6 +76,7 @@ public List<Module> getKProveModules() {
         return Collections.singletonList(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 installHaskellBackend(binder());
                 installHaskellRewriter(binder());
             }

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java

@@ -2,12 +2,15 @@
 package org.kframework.backend.haskell;
 
 import com.beust.jcommander.Parameter;
+import com.google.inject.Inject;
 import org.kframework.backend.kore.ModuleToKORE;
 import org.kframework.utils.inject.RequestScoped;
 import org.kframework.utils.options.BaseEnumConverter;
 
 @RequestScoped
 public class HaskellKRunOptions {
+    @Inject
+    public HaskellKRunOptions() {}
 
     @Parameter(names="--haskell-backend-command", descriptionKey = "command",
             description="Command to run the Haskell backend execution engine.", hidden = true)

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java

@@ -2,11 +2,14 @@
 package org.kframework.backend.haskell;
 
 import com.beust.jcommander.Parameter;
+import com.google.inject.Inject;
 import org.kframework.utils.inject.RequestScoped;
 
 @RequestScoped
 public class HaskellKompileOptions {
 
+    @Inject
+    public HaskellKompileOptions() {}
     @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", descriptionKey = "command", hidden = true)
     public String haskellBackendCommand = "kore-exec";
 

k-distribution/src/main/assembly/bin.xml

@@ -69,7 +69,7 @@
     </fileSet>
     <fileSet>
       <directory>${project.parent.basedir}/package</directory>
-      <outputDirectory>/lib</outputDirectory>
+      <outputDirectory>/lib/kframework</outputDirectory>
       <includes>
         <include>version</include>
       </includes>

k-distribution/src/main/scripts/bin/krun

@@ -37,12 +37,16 @@ filterSubst=
 if [[ "$OSTYPE" == "darwin"* ]]; then
   LLDB_FILE="$(dirname "$0")/../lib/kllvm/lldb/k_lldb_path"
   if [ -f "$LLDB_FILE" ]; then
-    DBG_CMD="$(cat "$LLDB_FILE") -- "
+    DBG_EXE="$(cat "$LLDB_FILE")"
   else
-    DBG_CMD="lldb --"
+    DBG_EXE="lldb"
   fi
+  DBG_CMD=" --"
+  DBG_FLAG=" -s "
 else
-  DBG_CMD="gdb --args "
+  DBG_EXE="gdb"
+  DBG_FLAG=" -x "
+  DBG_CMD=" --args "
 fi
 
 
@@ -112,6 +116,10 @@ $KRUN options:
                            parser. This can be overridden with -p.
       --debugger           Launch the backend in a debugging console.
                            Currently only supported on LLVM backend.
+      --debugger-batch     Launch the backend in a debugging console in batch
+                           mode. Currently only supported on LLVM backend.
+      --debugger-command FILE  Execute GDB commands from FILE to debug program.
+                               Currently only supported on LLVM backend.
   -d, --directory DIR      [DEPRECATED] Look for a kompiled directory ending in "-kompiled"
                            under the directory DIR.
       --dry-run            Do not execute backend, but instead print the
@@ -392,9 +400,24 @@ do
       ;;
 
       --debugger)
-      cmdprefix="$DBG_CMD"
+      cmdprefix="$DBG_EXE $DBG_CMD"
       ;;
 
+      --debugger-command)
+        debugCommandFile="$2"
+        cmdprefix="$DBG_EXE $DBG_FLAG $debugCommandFile $DBG_CMD"
+      shift
+      ;;
+
+      --debugger-batch)
+      if [[ $cmdprefix == *gdb* || $cmdprefix == *lldb* ]]; then
+        cmdprefix="$DBG_EXE --batch $DBG_FLAG $debugCommandFile $DBG_CMD"
+      else
+        DBG_CMD=" --batch $DBG_CMD"
+      fi
+      ;;
+
+
       --statistics)
       statistics=true
       ;;

k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala

@@ -65,18 +65,28 @@ class KoreTest {
     attributes.patterns.exists { case p: Application => p.head.ctr == name }
   }
 
+  // get the rewrite associated with a rule or equational axiom
+  //
+  // \and(\equals(requires, \dv("true")), \and(_, \rewrites(lhs, rhs)))
+  // \and(\top(), \and(_, \rewrites(lhs, rhs)))
+  // \rewrites(\and(\equals(requires, \dv("true")), lhs), \and(_, rhs))
+  // \rewrites(\and(\top(), lhs), \and(_, rhs))
+  // \implies(\equals(requires, \dv("true")), \and(\equals(lhs, rhs), _))
+  // \implies(\top, \and(\equals(lhs, rhs), _))
+  // \implies(\and(_, \equals(requires, \dv("true"))), \and(\equals(lhs, rhs), _))
+  // \implies(\and(_, \top), \and(\equals(lhs, rhs), _))
+  // \equals(lhs, rhs)
   def getRewrite(axiom: AxiomDeclaration): Option[GeneralizedRewrite] = {
     def go(pattern: Pattern): Option[GeneralizedRewrite] = {
       pattern match {
-        case And(_, Equals(_, _, _, _), And(_, _, rw @ Rewrites(_, _, _))) => Some(rw)
-        case And(_, Top(_), And(_, _, rw @ Rewrites(_, _, _))) => Some(rw)
-        case Rewrites(s, And(_, Equals(_, _, _, _), l), And(_, _, r)) => Some(B.Rewrites(s, l, r))
-        case Rewrites(s, And(_, Top(_), l), And(_, _, r)) => Some(B.Rewrites(s, l, r))
-        case Implies(_, Bottom(_), p) => go(p)
-        case Implies(_, Equals(_, _, _, _), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
-        case Implies(_, Top(_), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
-        case Implies(_, And(_, _, Equals(_, _, _, _)), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
-        case Implies(_, And(_, _, Top(_)), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq)
+        case And(_, Equals(_, _, _, _) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()) => Some(rw)
+        case And(_, Top(_) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()) => Some(rw)
+        case Rewrites(s, And(_, Equals(_, _, _, _) +: l +: Seq()), And(_, _ +: r +: Seq())) => Some(B.Rewrites(s, l, r))
+        case Rewrites(s, And(_, Top(_) +: l +: Seq()), And(_, _ +: r +: Seq())) => Some(B.Rewrites(s, l, r))
+        case Implies(_, Equals(_, _, _, _), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
+        case Implies(_, Top(_), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
+        case Implies(_, And(_, _ +: Equals(_, _, _, _) +: Seq()), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
+        case Implies(_, And(_, _ +: Top(_) +: Seq()), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
         case eq @ Equals(_, _, Application(_, _), _) => Some(eq)
         case _ => None
 
@@ -91,7 +101,7 @@ class KoreTest {
 
   def symbols(pat: Pattern): Seq[SymbolOrAlias] = {
     pat match {
-      case And(_, p1, p2) => symbols(p1) ++ symbols(p2)
+      case And(_, ps) => ps.flatMap(symbols)
       case Application(s, ps) => Seq(s).filter(isConcrete) ++ ps.flatMap(symbols)
       case Ceil(_, _, p) => symbols(p)
       case Equals(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
@@ -103,7 +113,7 @@ class KoreTest {
       case Mem(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
 //      case Next(_, p) => symbols(p)
       case Not(_, p) => symbols(p)
-      case Or(_, p1, p2) => symbols(p1) ++ symbols(p2)
+      case Or(_, ps) => ps.flatMap(symbols)
       case Rewrites(_, p1, p2) => symbols(p1) ++ symbols(p2)
       case _ => Seq()
     }

kernel/pom.xml

@@ -32,13 +32,13 @@
     <dependency>
       <groupId>com.google.inject</groupId>
       <artifactId>guice</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <classifier>no_aop</classifier>
     </dependency>
     <dependency>
       <groupId>com.google.inject.extensions</groupId>
       <artifactId>guice-multibindings</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <exclusions>
         <exclusion>
           <groupId>com.google.inject</groupId>
@@ -49,7 +49,7 @@
     <dependency>
       <groupId>com.google.inject.extensions</groupId>
       <artifactId>guice-grapher</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <exclusions>
         <exclusion>
           <groupId>com.google.inject</groupId>
@@ -60,7 +60,7 @@
     <dependency>
       <groupId>com.google.inject.extensions</groupId>
       <artifactId>guice-throwingproviders</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <exclusions>
         <exclusion>
           <groupId>com.google.inject</groupId>

kernel/src/main/java/org/kframework/kast/KastModule.java

@@ -21,6 +21,7 @@ public class KastModule extends AbstractModule {
 
     @Override
     public void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KastFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KAST);
 

kernel/src/main/java/org/kframework/kast/KastOptions.java

@@ -31,6 +31,9 @@
 @RequestScoped
 public final class KastOptions {
 
+    @Inject
+    public KastOptions() {}
+
     @Parameter(description="<file>")
     private List<String> parameters;
 

kernel/src/main/java/org/kframework/kdep/KDepModule.java

@@ -22,7 +22,7 @@
 public class KDepModule extends AbstractModule {
     @Override
     protected void configure() {
-
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KDepFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KDEP);
 

kernel/src/main/java/org/kframework/kdep/KDepOptions.java

@@ -3,6 +3,7 @@
 
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.ParametersDelegate;
+import com.google.inject.Inject;
 import org.kframework.main.GlobalOptions;
 import org.kframework.utils.inject.RequestScoped;
 import org.kframework.utils.options.OuterParsingOptions;
@@ -16,6 +17,9 @@
 @RequestScoped
 public class KDepOptions {
 
+    @Inject
+    public KDepOptions() {}
+
     @ParametersDelegate
     public transient GlobalOptions global = new GlobalOptions();
 

kernel/src/main/java/org/kframework/kil/loader/Context.java

@@ -19,6 +19,9 @@
 @RequestScoped
 public class Context implements Serializable {
 
+    @Inject
+    public Context() {}
+
     /**
      * Represents a map from all Klabels or attributes in string representation
      * to sets of corresponding productions.

kernel/src/main/java/org/kframework/kompile/BackendModule.java

@@ -14,6 +14,7 @@
 public class BackendModule extends AbstractModule {
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         MapBinder<String, Backend> backendBinder = MapBinder.newMapBinder(
                 binder(), String.class, org.kframework.compile.Backend.class);
         backendBinder.addBinding("kore").to(KoreBackend.class);

kernel/src/main/java/org/kframework/kompile/KompileModule.java

@@ -25,6 +25,7 @@ public KompileModule() {
 
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KompileFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KOMPILE);
 

kernel/src/main/java/org/kframework/kompile/KompileOptions.java

@@ -3,6 +3,7 @@
 
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.ParametersDelegate;
+import com.google.inject.Inject;
 import org.apache.commons.io.FilenameUtils;
 import org.kframework.backend.Backends;
 import org.kframework.main.GlobalOptions;
@@ -23,7 +24,8 @@
 
 @RequestScoped
 public class KompileOptions implements Serializable {
-
+    @Inject
+    public KompileOptions() {}
 
     /**
      * WARNING: this field will be non-null in kompile tool, but null when KompileOption is deserialized,

kernel/src/main/java/org/kframework/kprove/KProveModule.java

@@ -20,6 +20,7 @@
 public class KProveModule extends AbstractModule {
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KProveFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KPROVE);
 

kernel/src/main/java/org/kframework/kprove/KProveOptions.java

@@ -4,6 +4,7 @@
 
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.ParametersDelegate;
+import com.google.inject.Inject;
 import org.kframework.unparser.PrintOptions;
 import org.kframework.main.GlobalOptions;
 import org.kframework.utils.file.FileUtil;
@@ -20,6 +21,8 @@
 
 @RequestScoped
 public class KProveOptions {
+    @Inject
+    public KProveOptions() {}
 
     @ParametersDelegate
     private final transient GlobalOptions global = new GlobalOptions();

kernel/src/main/java/org/kframework/kprove/RewriterModule.java

@@ -17,6 +17,7 @@
 public class RewriterModule extends AbstractModule {
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FileUtil.class);
     }