From 3e7fdebda3715f38dda0ca303a434d9f7b09a067 Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <robertogomes@dcc.ufmg.br>
Date: Wed, 4 Oct 2023 15:03:41 -0300
Subject: [PATCH 1/5] Introduces `--debugger-command` flag to krun (#3687)

This PR reflects a new modification on the `llvm-krun` from the
llvm-backend.

This new flag enables the user to pass a file with debug commands to its
debugger and run them in a non-interactive mode!

This new flag also allows testing the debugger on our current CI.
---
 k-distribution/src/main/scripts/bin/krun | 31 +++++++++++++++++++++---
 1 file changed, 27 insertions(+), 4 deletions(-)

diff --git a/k-distribution/src/main/scripts/bin/krun b/k-distribution/src/main/scripts/bin/krun
index 7f684964a01..e5e88599fe4 100755
--- a/k-distribution/src/main/scripts/bin/krun
+++ b/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
       ;;

From 079db219305896100d1d49ad13017db59ffe6e16 Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <robertogomes@dcc.ufmg.br>
Date: Wed, 4 Oct 2023 16:22:36 -0300
Subject: [PATCH 2/5] Updating `Guice` to 4.0 and deleting temporary injections
 (#3644)

This modification aimed to update the
[Guice](https://github.com/google/guice) version from `4.0-beta5` to
`4.0`, deleting the constructors with one void parameter to
```
Prevents instantiation by Guice when not explicitly configured in a Module.
```
And applying the `requireAtInjectOnConstructors` on every
`constructor()` inside a class that extends the `AbstractModule` for
consistency. These modifications made it necessary to explicitly create
constructors with zero parameters and within the `@Injector` annotation.

---------

Co-authored-by: devops <devops@runtimeverification.com>
---
 .../haskell/HaskellBackendKModule.java        |  3 ++
 .../backend/haskell/HaskellKRunOptions.java   |  3 ++
 .../haskell/HaskellKompileOptions.java        |  3 ++
 kernel/pom.xml                                |  8 ++--
 .../java/org/kframework/kast/KastModule.java  |  1 +
 .../java/org/kframework/kast/KastOptions.java |  3 ++
 .../java/org/kframework/kdep/KDepModule.java  |  2 +-
 .../java/org/kframework/kdep/KDepOptions.java |  4 ++
 .../org/kframework/kil/loader/Context.java    |  3 ++
 .../org/kframework/kompile/BackendModule.java |  1 +
 .../org/kframework/kompile/KompileModule.java |  1 +
 .../kframework/kompile/KompileOptions.java    |  4 +-
 .../org/kframework/kprove/KProveModule.java   |  1 +
 .../org/kframework/kprove/KProveOptions.java  |  3 ++
 .../org/kframework/kprove/RewriterModule.java |  1 +
 .../ksearchpattern/KSearchPatternModule.java  |  1 +
 .../ksearchpattern/KSearchPatternOptions.java |  4 ++
 .../org/kframework/kserver/KServerModule.java |  1 +
 .../kframework/kserver/KServerOptions.java    |  4 ++
 .../org/kframework/main/AbstractKModule.java  |  2 +
 .../java/org/kframework/main/FrontEnd.java    |  2 +
 .../org/kframework/main/GlobalOptions.java    |  7 ---
 .../org/kframework/unparser/PrintOptions.java |  8 ----
 .../kframework/utils/inject/CommonModule.java |  1 +
 .../utils/inject/DefinitionLoadingModule.java |  1 +
 .../utils/inject/JCommanderModule.java        |  1 +
 .../utils/inject/OuterParsingModule.java      |  2 +-
 .../utils/options/BackendOptions.java         |  4 --
 .../options/DefinitionLoadingOptions.java     |  4 --
 .../kframework/utils/options/SMTOptions.java  |  7 +--
 .../org/kframework/utils/BaseTestCase.java    |  2 +
 .../backend/llvm/LLVMKompileOptions.java      |  4 ++
 nix/mavenix.lock                              | 48 +++++++++----------
 33 files changed, 84 insertions(+), 60 deletions(-)

diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java
index b2fd5daa67a..d86230dbafa 100644
--- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java
+++ b/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());
             }
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java
index 5c20d442625..3a6649ef34c 100644
--- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java
+++ b/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)
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java
index 69a9c8b4b2c..081be372136 100644
--- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java
+++ b/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";
 
diff --git a/kernel/pom.xml b/kernel/pom.xml
index c932c02dcc6..aa1541af51d 100644
--- a/kernel/pom.xml
+++ b/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>
diff --git a/kernel/src/main/java/org/kframework/kast/KastModule.java b/kernel/src/main/java/org/kframework/kast/KastModule.java
index aeb3976a48d..a28605ce26d 100644
--- a/kernel/src/main/java/org/kframework/kast/KastModule.java
+++ b/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);
 
diff --git a/kernel/src/main/java/org/kframework/kast/KastOptions.java b/kernel/src/main/java/org/kframework/kast/KastOptions.java
index 2aaa084b516..86402c537c6 100644
--- a/kernel/src/main/java/org/kframework/kast/KastOptions.java
+++ b/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;
 
diff --git a/kernel/src/main/java/org/kframework/kdep/KDepModule.java b/kernel/src/main/java/org/kframework/kdep/KDepModule.java
index c068f105368..ed6af4762b9 100644
--- a/kernel/src/main/java/org/kframework/kdep/KDepModule.java
+++ b/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);
 
diff --git a/kernel/src/main/java/org/kframework/kdep/KDepOptions.java b/kernel/src/main/java/org/kframework/kdep/KDepOptions.java
index d830c3b8bf3..c65cc98273e 100644
--- a/kernel/src/main/java/org/kframework/kdep/KDepOptions.java
+++ b/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();
 
diff --git a/kernel/src/main/java/org/kframework/kil/loader/Context.java b/kernel/src/main/java/org/kframework/kil/loader/Context.java
index 2bc8a8252db..a136a3922e6 100644
--- a/kernel/src/main/java/org/kframework/kil/loader/Context.java
+++ b/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.
diff --git a/kernel/src/main/java/org/kframework/kompile/BackendModule.java b/kernel/src/main/java/org/kframework/kompile/BackendModule.java
index 35b91d2654f..5425cabee5c 100644
--- a/kernel/src/main/java/org/kframework/kompile/BackendModule.java
+++ b/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);
diff --git a/kernel/src/main/java/org/kframework/kompile/KompileModule.java b/kernel/src/main/java/org/kframework/kompile/KompileModule.java
index 10ed758e44e..3757d7c6432 100644
--- a/kernel/src/main/java/org/kframework/kompile/KompileModule.java
+++ b/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);
 
diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
index 8d494435b6d..ba96c409fdd 100644
--- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
+++ b/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,
diff --git a/kernel/src/main/java/org/kframework/kprove/KProveModule.java b/kernel/src/main/java/org/kframework/kprove/KProveModule.java
index 84b17c42eb3..ca375b76ad7 100644
--- a/kernel/src/main/java/org/kframework/kprove/KProveModule.java
+++ b/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);
 
diff --git a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java
index b5b59d83917..d25a5b6b6c3 100644
--- a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java
+++ b/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();
diff --git a/kernel/src/main/java/org/kframework/kprove/RewriterModule.java b/kernel/src/main/java/org/kframework/kprove/RewriterModule.java
index 5670711aa9b..90ea42f76b8 100644
--- a/kernel/src/main/java/org/kframework/kprove/RewriterModule.java
+++ b/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);
     }
 
diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java
index 2ae3035c72b..93328edf004 100644
--- a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java
+++ b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java
@@ -22,6 +22,7 @@
 public class KSearchPatternModule extends AbstractModule {
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KSearchPatternFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KSEARCHPATTERN);
 
diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java
index 1c2d9a32a08..9fcc1baec84 100644
--- a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java
+++ b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.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.DefinitionLoadingOptions;
@@ -16,6 +17,9 @@
 @RequestScoped
 public class KSearchPatternOptions {
 
+    @Inject
+    public KSearchPatternOptions() {}
+
     @ParametersDelegate
     public transient GlobalOptions global = new GlobalOptions();
 
diff --git a/kernel/src/main/java/org/kframework/kserver/KServerModule.java b/kernel/src/main/java/org/kframework/kserver/KServerModule.java
index f8e9f4d57bb..865cdfc76f4 100644
--- a/kernel/src/main/java/org/kframework/kserver/KServerModule.java
+++ b/kernel/src/main/java/org/kframework/kserver/KServerModule.java
@@ -20,6 +20,7 @@ public class KServerModule extends AbstractModule {
 
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(Tool.class).toInstance(Tool.KSERVER);
         bind(FrontEnd.class).to(KServerFrontEnd.class);
 
diff --git a/kernel/src/main/java/org/kframework/kserver/KServerOptions.java b/kernel/src/main/java/org/kframework/kserver/KServerOptions.java
index 322b689b874..b09695b0ac3 100644
--- a/kernel/src/main/java/org/kframework/kserver/KServerOptions.java
+++ b/kernel/src/main/java/org/kframework/kserver/KServerOptions.java
@@ -1,6 +1,7 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.kserver;
 
+import com.google.inject.Inject;
 import org.kframework.main.GlobalOptions;
 import org.kframework.utils.inject.RequestScoped;
 
@@ -10,6 +11,9 @@
 @RequestScoped
 public class KServerOptions {
 
+    @Inject
+    public KServerOptions() {}
+
     @ParametersDelegate
     public transient GlobalOptions global = new GlobalOptions();
 
diff --git a/kernel/src/main/java/org/kframework/main/AbstractKModule.java b/kernel/src/main/java/org/kframework/main/AbstractKModule.java
index 9fc12a9cb48..2a8dd35361b 100644
--- a/kernel/src/main/java/org/kframework/main/AbstractKModule.java
+++ b/kernel/src/main/java/org/kframework/main/AbstractKModule.java
@@ -37,6 +37,7 @@ public List<Pair<Class<?>, Boolean>> kproveOptions() {
     }
 
     protected void bindOptions(Supplier<List<Pair<Class<?>, Boolean>>> action, Binder binder) {
+        binder.requireAtInjectOnConstructors();
         Multibinder<Object> optionsBinder = Multibinder.newSetBinder(binder, Object.class, Options.class);
         for (Pair<Class<?>, Boolean> option : action.get()) {
             optionsBinder.addBinding().to(option.getKey());
@@ -81,6 +82,7 @@ public List<Module> getDefinitionSpecificKEqModules() {
 
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 //bind backend implementations of tools to their interfaces
             }
         });
diff --git a/kernel/src/main/java/org/kframework/main/FrontEnd.java b/kernel/src/main/java/org/kframework/main/FrontEnd.java
index 7417d75ee92..08e015488e0 100644
--- a/kernel/src/main/java/org/kframework/main/FrontEnd.java
+++ b/kernel/src/main/java/org/kframework/main/FrontEnd.java
@@ -2,6 +2,7 @@
 package org.kframework.main;
 
 import com.beust.jcommander.ParameterException;
+import com.google.inject.Inject;
 import com.google.inject.Provider;
 import org.kframework.utils.ExitOnTimeoutThread;
 import org.kframework.utils.InterrupterRunnable;
@@ -22,6 +23,7 @@ public abstract class FrontEnd {
     private final JarInfo jarInfo;
     private final Provider<FileUtil> files;
 
+    @Inject
     public FrontEnd(
             KExceptionManager kem,
             GlobalOptions globalOptions,
diff --git a/kernel/src/main/java/org/kframework/main/GlobalOptions.java b/kernel/src/main/java/org/kframework/main/GlobalOptions.java
index f0ae7d82c66..d78fad84535 100644
--- a/kernel/src/main/java/org/kframework/main/GlobalOptions.java
+++ b/kernel/src/main/java/org/kframework/main/GlobalOptions.java
@@ -19,13 +19,6 @@ public final class GlobalOptions {
 
     public GlobalOptions() {}
 
-    //TODO(dwightguth): remove in Guice 4.0
-    /**
-     * Prevents instantiation by Guice when not explicitly configured in a Module.
-     */
-    @Inject
-    public GlobalOptions(Void v) {}
-
     public GlobalOptions(boolean debug, Warnings warnings, boolean verbose) {
         this.debug = debug;
         this.warnings = warnings;
diff --git a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java
index c74146e45ea..74c860c80da 100644
--- a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java
+++ b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java
@@ -23,14 +23,6 @@ public PrintOptions(OutputModes output) {
         this.output = output;
     }
 
-    //TODO(dwightguth): remove in Guice 4.0
-    /**
-     * Prevents instantiation by Guice when not explicitly configured in a Module.
-     */
-    @Inject
-    public PrintOptions(Void v) {
-    }
-
     @Parameter(names = "--color", description = "Use colors in output. Default is on.", descriptionKey = "mode",
             converter=ColorModeConverter.class)
     private ColorSetting color;
diff --git a/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java b/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java
index 1eedd8619c1..bb1a47f6d2c 100644
--- a/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java
+++ b/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java
@@ -22,6 +22,7 @@ public class CommonModule extends AbstractModule {
 
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         SimpleScope requestScope = new SimpleScope();
         bindScope(RequestScoped.class, requestScope);
         DefinitionScope definitionScope = new DefinitionScope();
diff --git a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
index d093fdf0228..9f3f60084de 100644
--- a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
+++ b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
@@ -27,6 +27,7 @@ public class DefinitionLoadingModule extends AbstractModule {
 
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
     }
 
     @Provides @DefinitionScoped
diff --git a/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java b/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java
index 5c5f2c87414..495db016164 100644
--- a/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java
+++ b/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java
@@ -31,6 +31,7 @@ public class JCommanderModule extends AbstractModule  {
 
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(String[].class).annotatedWith(Options.class)
             .toProvider(SimpleScope.seededKeyProvider()).in(RequestScoped.class);;
     }
diff --git a/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java b/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java
index f6f0a7eec3c..cdb86466444 100644
--- a/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java
+++ b/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java
@@ -27,7 +27,7 @@ public class OuterParsingModule extends AbstractModule {
 
     @Override
     protected void configure() {
-
+        binder().requireAtInjectOnConstructors();
     }
 
     @Provides
diff --git a/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java b/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java
index 2046937054e..14c57e748d1 100644
--- a/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java
@@ -10,10 +10,6 @@ public class BackendOptions implements Serializable {
 
     public BackendOptions() {}
 
-    //TODO(dwightguth): remove in Guice 4.0
-    @Inject
-    public BackendOptions(Void v) {}
-
     @Parameter(names="--dry-run", description="Compile program into KORE format but do not run. Only used in Haskell and LLVM backend.")
     public boolean dryRun = false;
 }
diff --git a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java b/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
index 8f9ed1b7b41..a4d1c9c4f8b 100644
--- a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
@@ -8,10 +8,6 @@ public class DefinitionLoadingOptions {
 
     public DefinitionLoadingOptions() {}
 
-    //TODO(dwightguth): remove in Guice 4.0
-    @Inject
-    public DefinitionLoadingOptions(Void v) {}
-
     @Parameter(names={"--directory", "-d"}, description="[DEPRECATED] Path to the directory in which the kompiled " +
             "K definition resides. The default is the unique, only directory with the suffix '-kompiled' " +
             "in the current directory.", descriptionKey = "path", hidden = true)
diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
index b1acb132943..9fd7cc13a32 100644
--- a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
@@ -10,12 +10,7 @@ public class SMTOptions implements Serializable {
 
     public SMTOptions() {}
 
-    //TODO(dwightguth): remove in Guice 4.0
-    @Inject
-    public SMTOptions(Void v) {}
-
-    @Parameter(names="--smt", descriptionKey = "executable", converter=SMTSolverConverter.class,
-            description="SMT solver to use for checking constraints. <executable> is one of [z3|none].", hidden = true)
+    @Parameter(names="--smt", converter=SMTSolverConverter.class, description="SMT solver to use for checking constraints. <executable> is one of [z3|none].", descriptionKey = "executable", hidden = true)
     public SMTSolver smt = SMTSolver.Z3;
 
     public static class SMTSolverConverter extends BaseEnumConverter<SMTSolver> {
diff --git a/kernel/src/test/java/org/kframework/utils/BaseTestCase.java b/kernel/src/test/java/org/kframework/utils/BaseTestCase.java
index 17212387f6a..4ccafc4829a 100644
--- a/kernel/src/test/java/org/kframework/utils/BaseTestCase.java
+++ b/kernel/src/test/java/org/kframework/utils/BaseTestCase.java
@@ -71,6 +71,7 @@ public class DefinitionSpecificTestModule extends AbstractModule {
 
         @Override
         protected void configure() {
+            binder().requireAtInjectOnConstructors();
             bind(KompileOptions.class).toInstance(context.kompileOptions);
             bind(Definition.class).toInstance(definition);
             bind(File.class).annotatedWith(KompiledDir.class).toInstance(kompiledDir);
@@ -88,6 +89,7 @@ public class TestModule extends AbstractModule {
 
         @Override
         protected void configure() {
+            binder().requireAtInjectOnConstructors();
             bind(RunProcess.class).toInstance(rp);
             bind(KastOptions.class).toInstance(new KastOptions());
         }
diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
index e81ce93f110..bb757de59a8 100644
--- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
+++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
@@ -3,6 +3,7 @@
 
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.IStringConverter;
+import com.google.inject.Inject;
 import org.kframework.utils.inject.RequestScoped;
 
 import java.util.Arrays;
@@ -12,6 +13,9 @@
 @RequestScoped
 public class LLVMKompileOptions {
 
+    @Inject
+    public LLVMKompileOptions() {}
+
     @Parameter(names="--enable-llvm-debug", description="Enable debugging support for the LLVM backend.")
     public boolean debug = false;
 
diff --git a/nix/mavenix.lock b/nix/mavenix.lock
index 7be2b7a378a..541407e5860 100644
--- a/nix/mavenix.lock
+++ b/nix/mavenix.lock
@@ -282,52 +282,52 @@
       "sha1": "1b77ba79f9b2b7dfd4e15ea7bb0d568d5eb9cb8d"
     },
     {
-      "path": "com/google/inject/extensions/extensions-parent/4.0-beta5/extensions-parent-4.0-beta5.pom",
-      "sha1": "516d8e5e771cd573364dc6ff53c2c6c13908a713"
+      "path": "com/google/inject/extensions/extensions-parent/4.0/extensions-parent-4.0.pom",
+      "sha1": "db8e45ab989a2347421ff0d32be5446528d6f63f"
     },
     {
-      "path": "com/google/inject/extensions/guice-assistedinject/4.0-beta5/guice-assistedinject-4.0-beta5.jar",
-      "sha1": "820f10e0650cd9ed2591f398937df50f330b147d"
+      "path": "com/google/inject/extensions/guice-assistedinject/4.0/guice-assistedinject-4.0.jar",
+      "sha1": "8fa6431da1a2187817e3e52e967535899e2e46ca"
     },
     {
-      "path": "com/google/inject/extensions/guice-assistedinject/4.0-beta5/guice-assistedinject-4.0-beta5.pom",
-      "sha1": "4b9b352e0537b0ca49cb97533387864b185df09b"
+      "path": "com/google/inject/extensions/guice-assistedinject/4.0/guice-assistedinject-4.0.pom",
+      "sha1": "00c7fc29684b20dd475f517d5dafc850c613efde"
     },
     {
-      "path": "com/google/inject/extensions/guice-grapher/4.0-beta5/guice-grapher-4.0-beta5.jar",
-      "sha1": "dd9a00d72fecfa05a77bf28c7922eacddda23b18"
+      "path": "com/google/inject/extensions/guice-grapher/4.0/guice-grapher-4.0.jar",
+      "sha1": "4e611ae9b12bfc4ddd430a58c65ba1c4328eeaf9"
     },
     {
-      "path": "com/google/inject/extensions/guice-grapher/4.0-beta5/guice-grapher-4.0-beta5.pom",
-      "sha1": "1cd692901e55d382cdb9e647d74617bb68d63126"
+      "path": "com/google/inject/extensions/guice-grapher/4.0/guice-grapher-4.0.pom",
+      "sha1": "86b9c4937ebba7d14054d0f025f0df51d071218d"
     },
     {
-      "path": "com/google/inject/extensions/guice-multibindings/4.0-beta5/guice-multibindings-4.0-beta5.jar",
-      "sha1": "f432356db0a167127ffe4a7921238d7205b12682"
+      "path": "com/google/inject/extensions/guice-multibindings/4.0/guice-multibindings-4.0.jar",
+      "sha1": "f4509545b4470bbcc865aa500ad6fef2e97d28bf"
     },
     {
-      "path": "com/google/inject/extensions/guice-multibindings/4.0-beta5/guice-multibindings-4.0-beta5.pom",
-      "sha1": "3cff7b7b5f418f5edca0fa1b0d4bcd3f3215d9c7"
+      "path": "com/google/inject/extensions/guice-multibindings/4.0/guice-multibindings-4.0.pom",
+      "sha1": "2387a1e5163308cd826b348db825973df0800ad3"
     },
     {
-      "path": "com/google/inject/extensions/guice-throwingproviders/4.0-beta5/guice-throwingproviders-4.0-beta5.jar",
-      "sha1": "8840bd8267a5b09ee84a314a54dbdc6c1b0a7efb"
+      "path": "com/google/inject/extensions/guice-throwingproviders/4.0/guice-throwingproviders-4.0.jar",
+      "sha1": "90876169e80b4db9b61d654367c4c55079ae4e91"
     },
     {
-      "path": "com/google/inject/extensions/guice-throwingproviders/4.0-beta5/guice-throwingproviders-4.0-beta5.pom",
-      "sha1": "cb52affb5a89e66a5f1d9ab3a7fde7dda1cc5baa"
+      "path": "com/google/inject/extensions/guice-throwingproviders/4.0/guice-throwingproviders-4.0.pom",
+      "sha1": "5118433baea2efed034af00a96e324b5717e8059"
     },
     {
-      "path": "com/google/inject/guice-parent/4.0-beta5/guice-parent-4.0-beta5.pom",
-      "sha1": "13d7df2b77236548d1e7cb9ba688686ddd4f19a5"
+      "path": "com/google/inject/guice-parent/4.0/guice-parent-4.0.pom",
+      "sha1": "a59ca1d3d70552158088d7f71e6c7e8779b9a8a1"
     },
     {
-      "path": "com/google/inject/guice/4.0-beta5/guice-4.0-beta5-no_aop.jar",
-      "sha1": "7706f581d709b1afd89b4e0dbf1bebf250abbd9b"
+      "path": "com/google/inject/guice/4.0/guice-4.0-no_aop.jar",
+      "sha1": "199b7acaa05b570bbccf31be998f013963e5e752"
     },
     {
-      "path": "com/google/inject/guice/4.0-beta5/guice-4.0-beta5.pom",
-      "sha1": "1e968b8c1da8cb48b7c0b77ffc565f92f313c392"
+      "path": "com/google/inject/guice/4.0/guice-4.0.pom",
+      "sha1": "688cb7b0d86456e3706573fe583173ee5e728f4e"
     },
     {
       "path": "com/google/j2objc/j2objc-annotations/1.3/j2objc-annotations-1.3.jar",

From a49c3a2659d125124c29cd3530da61c5e7ed6cfd Mon Sep 17 00:00:00 2001
From: Radu Mereuta <headness13@gmail.com>
Date: Thu, 5 Oct 2023 00:06:43 +0300
Subject: [PATCH 3/5] kast --debug-tokens (#3660)

Add an option to kast to show the list of matched tokens, their location
and the token used to match it.
Review with hidden whitespace.
@dkcumming how does this look?

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>
---
 .../issue-3647-debugTokens/Makefile           |  6 ++
 .../issue-3647-debugTokens/a.test.kast        | 14 ++++
 .../issue-3647-debugTokens/a.test.kast.out    | 15 ++++
 .../issue-3647-debugTokens/b.test.kast        |  1 +
 .../issue-3647-debugTokens/b.test.kast.out    |  9 +++
 .../issue-3647-debugTokens/test.k             | 14 ++++
 .../org/kframework/kast/KastFrontEnd.java     | 80 ++++++++++---------
 .../java/org/kframework/kast/KastOptions.java |  3 +
 .../kompile/CompiledDefinition.java           |  6 ++
 .../java/org/kframework/parser/KRead.java     |  4 +
 .../parser/inner/ParseInModule.java           | 54 ++++++++++++-
 .../parser/inner/kernel/EarleyParser.java     | 34 ++++----
 .../parser/inner/kernel/Scanner.java          | 21 +++--
 13 files changed, 194 insertions(+), 67 deletions(-)
 create mode 100644 k-distribution/tests/regression-new/issue-3647-debugTokens/Makefile
 create mode 100644 k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast
 create mode 100644 k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast.out
 create mode 100644 k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast
 create mode 100644 k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast.out
 create mode 100644 k-distribution/tests/regression-new/issue-3647-debugTokens/test.k

diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/Makefile b/k-distribution/tests/regression-new/issue-3647-debugTokens/Makefile
new file mode 100644
index 00000000000..5ab56c86a70
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/Makefile
@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KAST_FLAGS=--debug-tokens
+
+include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast b/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast
new file mode 100644
index 00000000000..0d8c763edc3
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast
@@ -0,0 +1,14 @@
+1 + 2 + aaaaaaaaaaaa
+
+
+
+
+
+
+
+
+
+
++ 10000000
++ "str"
++ "long str that breaks                                                                    alighnment"
diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast.out b/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast.out
new file mode 100644
index 00000000000..903a7ba1fd5
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast.out
@@ -0,0 +1,15 @@
+|"Match"                                                                          | (location)    | Terminal            |
+|---------------------------------------------------------------------------------|---------------|---------------------|
+|"1"                                                                              | (1,1,1,2)     | r"[\\+-]?[0-9]+"    |
+|"+"                                                                              | (1,3,1,4)     | "+"                 |
+|"2"                                                                              | (1,5,1,6)     | r"[\\+-]?[0-9]+"    |
+|"+"                                                                              | (1,7,1,8)     | "+"                 |
+|"aaaaaaaaaaaa"                                                                   | (1,9,1,21)    | r"[a-z][a-zA-Z0-9]*"|
+|"+"                                                                              | (12,1,12,2)   | "+"                 |
+|"10000000"                                                                       | (12,3,12,11)  | r"[\\+-]?[0-9]+"    |
+|"+"                                                                              | (13,1,13,2)   | "+"                 |
+|"\"str\""                                                                        | (13,3,13,8)   | r"[\\\"](([^\\\"\\n\\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]"|
+|"+"                                                                              | (14,1,14,2)   | "+"                 |
+|"\"long str that breaks                                                                    alighnment\"" | (14,3,14,103) | r"[\\\"](([^\\\"\\n\\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]"|
+|""                                                                               | (15,1,15,1)   | "<eof>"             |
+
diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast
new file mode 100644
index 00000000000..f845bb7df41
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast
@@ -0,0 +1 @@
+1 + 2 + aaa
diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast.out b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast.out
new file mode 100644
index 00000000000..1525daf1bc8
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast.out
@@ -0,0 +1,9 @@
+|"Match" | (location) | Terminal            |
+|--------|------------|---------------------|
+|"1"     | (1,1,1,2)  | r"[\\+-]?[0-9]+"    |
+|"+"     | (1,3,1,4)  | "+"                 |
+|"2"     | (1,5,1,6)  | r"[\\+-]?[0-9]+"    |
+|"+"     | (1,7,1,8)  | "+"                 |
+|"aaa"   | (1,9,1,12) | r"[a-z][a-zA-Z0-9]*"|
+|""      | (2,1,2,1)  | "<eof>"             |
+
diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/test.k b/k-distribution/tests/regression-new/issue-3647-debugTokens/test.k
new file mode 100644
index 00000000000..90b98cf29a9
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/test.k
@@ -0,0 +1,14 @@
+// Copyright (c) K Team. All Rights Reserved.
+
+module TEST-SYNTAX
+    imports INT-SYNTAX
+    imports ID-SYNTAX
+    imports STRING-SYNTAX
+    syntax Exp ::= Exp "+" Exp [left] | Int | Id | String
+endmodule
+
+module TEST
+    imports TEST-SYNTAX
+    configuration <k> $PGM:Exp </k>
+
+endmodule
diff --git a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java b/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java
index 9156ed7c766..c222faa9924 100644
--- a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java
+++ b/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java
@@ -135,35 +135,39 @@ public int run() {
                 Source source = options.source();
 
                 try (ParseInModule parseInModule = RuleGrammarGenerator.getCombinedGrammar(mod, true, null)) {
-                    Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> res = parseInModule.parseString(stringToParse, sort, startSymbolLocation, source);
-                    kem.addAllKException(res._2().stream().map(KEMException::getKException).collect(Collectors.toSet()));
-                    if (res._1().isLeft()) {
-                        throw res._1().left().get().iterator().next();
+                    if (options.debugTokens)
+                        System.out.println(parseInModule.tokenizeString(stringToParse, source));
+                    else {
+                        Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> res = parseInModule.parseString(stringToParse, sort, startSymbolLocation, source);
+                        kem.addAllKException(res._2().stream().map(KEMException::getKException).collect(Collectors.toSet()));
+                        if (res._1().isLeft()) {
+                            throw res._1().left().get().iterator().next();
+                        }
+                        // important to get the extension module for unparsing because it contains generated syntax
+                        // like casts, projections and others
+                        Module unparsingMod = parseInModule.getExtensionModule();
+                        K parsed = new TreeNodesToKORE(Outer::parseSort, true).down(res._1().right().get());
+
+                        if (options.expandMacros) {
+                            parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed);
+                        }
+                        ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(mod);
+                        LabelInfo labelInfo = new LabelInfoFromModule(mod);
+                        SortInfo sortInfo = SortInfo.fromModule(mod);
+
+                        Rule r = Rule.apply(parsed, BooleanUtils.TRUE, BooleanUtils.TRUE, Att.empty());
+                        if (options.steps.contains(KompileSteps.anonVars))
+                            r = (Rule) new ResolveAnonVar().resolve(r);
+                        r = (Rule) new ResolveSemanticCasts(false).resolve(r); // move casts to side condition predicates
+                        r = (Rule) new ConstantFolding().fold(unparsingMod, r);
+                        r = (Rule) new CloseCells(configInfo, sortInfo, labelInfo).close(r);
+                        if (options.steps.contains(KompileSteps.concretizeCells)) {
+                            r = (Rule) new AddImplicitComputationCell(configInfo, labelInfo).apply(mod, r);
+                            r = (Rule) new ConcretizeCells(configInfo, labelInfo, sortInfo, mod).concretize(mod, r);
+                        }
+                        K result = r.body();
+                        kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), result, sort);
                     }
-                    // important to get the extension module for unparsing because it contains generated syntax
-                    // like casts, projections and others
-                    Module unparsingMod = parseInModule.getExtensionModule();
-                    K parsed = new TreeNodesToKORE(Outer::parseSort, true).down(res._1().right().get());
-
-                    if (options.expandMacros) {
-                        parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed);
-                    }
-                    ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(mod);
-                    LabelInfo labelInfo = new LabelInfoFromModule(mod);
-                    SortInfo sortInfo = SortInfo.fromModule(mod);
-
-                    Rule r = Rule.apply(parsed, BooleanUtils.TRUE, BooleanUtils.TRUE, Att.empty());
-                    if (options.steps.contains(KompileSteps.anonVars))
-                        r = (Rule) new ResolveAnonVar().resolve(r);
-                    r = (Rule) new ResolveSemanticCasts(false).resolve(r); // move casts to side condition predicates
-                    r = (Rule) new ConstantFolding().fold(unparsingMod, r);
-                    r = (Rule) new CloseCells(configInfo, sortInfo, labelInfo).close(r);
-                    if (options.steps.contains(KompileSteps.concretizeCells)) {
-                        r = (Rule) new AddImplicitComputationCell(configInfo, labelInfo).apply(mod, r);
-                        r = (Rule) new ConcretizeCells(configInfo, labelInfo, sortInfo, mod).concretize(mod, r);
-                    }
-                    K result = r.body();
-                    kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), result, sort);
                 }
 
                 sw.printTotal("Total");
@@ -210,17 +214,21 @@ public int run() {
             } else {
                 Reader stringToParse = options.stringToParse();
                 Source source = options.source();
-                K parsed = kread.prettyRead(parsingMod, sort, startSymbolLocation, def, source, FileUtil.read(stringToParse));
+                if (options.debugTokens)
+                    System.out.println(kread.showTokens(parsingMod, def, FileUtil.read(stringToParse), source));
+                else {
+                    K parsed = kread.prettyRead(parsingMod, sort, startSymbolLocation, def, source, FileUtil.read(stringToParse));
 
-                if (options.expandMacros) {
-                    parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed);
-                }
+                    if (options.expandMacros) {
+                        parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed);
+                    }
 
-                if (sort.equals(Sorts.K())) {
-                    sort = Sorts.KItem();
-                }
+                    if (sort.equals(Sorts.K())) {
+                        sort = Sorts.KItem();
+                    }
 
-                kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), parsed, sort);
+                    kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), parsed, sort);
+                }
             }
 
             sw.printTotal("Total");
diff --git a/kernel/src/main/java/org/kframework/kast/KastOptions.java b/kernel/src/main/java/org/kframework/kast/KastOptions.java
index 86402c537c6..7ef74e430c6 100644
--- a/kernel/src/main/java/org/kframework/kast/KastOptions.java
+++ b/kernel/src/main/java/org/kframework/kast/KastOptions.java
@@ -158,4 +158,7 @@ public Class<InputModes> enumClass() {
             return InputModes.class;
         }
     }
+
+    @Parameter(names="--debug-tokens", description="Print a Markdown table of tokens matched by the scanner. Useful for debugging parsing errors.")
+    public boolean debugTokens = false;
 }
diff --git a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java b/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java
index a2342afd40d..289619a9fa7 100644
--- a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java
+++ b/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java
@@ -207,6 +207,12 @@ public K parseSingleTerm(Module module, Sort programStartSymbol, String startSym
         }
     }
 
+    public String showTokens(Module module, FileUtil files, String s, Source source) {
+        try (ParseInModule parseInModule = RuleGrammarGenerator.getCombinedGrammar(module, true, files)) {
+            return parseInModule.tokenizeString(s, source);
+        }
+    }
+
     public Module getExtensionModule(Module module, FileUtil files) {
         return RuleGrammarGenerator.getCombinedGrammar(module, true, files).getExtensionModule();
     }
diff --git a/kernel/src/main/java/org/kframework/parser/KRead.java b/kernel/src/main/java/org/kframework/parser/KRead.java
index c5b50cf4afb..6ed83e89188 100644
--- a/kernel/src/main/java/org/kframework/parser/KRead.java
+++ b/kernel/src/main/java/org/kframework/parser/KRead.java
@@ -51,6 +51,10 @@ public KRead(
         this.globalOptions = globalOptions;
     }
 
+    public String showTokens(Module mod, CompiledDefinition def, String stringToParse, Source source) {
+        return def.showTokens(mod, files, stringToParse, source);
+    }
+
     public K prettyRead(Module mod, Sort sort, String startSymbolLocation, CompiledDefinition def, Source source, String stringToParse) {
         return prettyRead(mod, sort, startSymbolLocation, def, source, stringToParse, this.input);
     }
diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java
index 3aa8b4bf713..4e3cbdb4066 100644
--- a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java
+++ b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java
@@ -7,6 +7,8 @@
 import org.kframework.attributes.Source;
 import org.kframework.builtin.Sorts;
 import org.kframework.definition.Module;
+import org.kframework.definition.Terminal;
+import org.kframework.definition.TerminalLike;
 import org.kframework.kore.K;
 import org.kframework.kore.Sort;
 import org.kframework.main.GlobalOptions;
@@ -16,6 +18,7 @@
 import org.kframework.parser.inner.kernel.EarleyParser;
 import org.kframework.parser.inner.kernel.Scanner;
 import org.kframework.parser.outer.Outer;
+import org.kframework.utils.StringUtil;
 import org.kframework.utils.errorsystem.KEMException;
 import org.kframework.utils.file.FileUtil;
 import scala.Tuple2;
@@ -28,10 +31,9 @@
 import java.io.IOException;
 import java.io.Serializable;
 import java.nio.charset.StandardCharsets;
-import java.util.Collections;
-import java.util.Queue;
-import java.util.Set;
+import java.util.*;
 import java.util.concurrent.ConcurrentLinkedQueue;
+import java.util.stream.Collectors;
 
 /**
  * A wrapper that takes a module and one can call the parser
@@ -159,6 +161,52 @@ public void initialize() {
         }
     }
 
+    /**
+     * Print the list of tokens matched by the scanner, the location and the Regex Terminal
+     * The output is a valid Markdown table.
+     */
+    public String tokenizeString(String input, Source source) {
+        StringBuilder sb = new StringBuilder();
+        try (Scanner scanner = getScanner()) {
+            EarleyParser.ParserMetadata mdata = new EarleyParser.ParserMetadata(input, scanner, source, 1, 1);
+            Map<Integer, TerminalLike> kind2Token =
+                    scanner.getTokens().entrySet().stream().map(a -> new Tuple2<>(a.getValue()._1, a.getKey()))
+                    .collect(Collectors.toMap(Tuple2::_1, Tuple2::_2));
+            List<Integer> lines = mdata.getLines();
+            List<Integer> columns = mdata.getColumns();
+            int maxTokenLen = 7, maxLocLen = 10, maxTerminalLen = 10;
+            List<String> locs = new ArrayList<>();
+            List<String> tokens = new ArrayList<>();
+            List<String> terminals = new ArrayList<>();
+            List<Scanner.Token> words = mdata.getWords();
+            for (Scanner.Token word : mdata.getWords()) {
+                String loc = String.format("(%d,%d,%d,%d)",
+                        lines.get(word.startLoc), columns.get(word.startLoc),
+                        lines.get(word.endLoc), columns.get(word.endLoc));
+                locs.add(loc);
+                maxLocLen = Math.max(maxLocLen, loc.length());
+                String tok = StringUtil.enquoteKString(word.value);
+                tokens.add(tok);
+                maxTokenLen = Math.max(maxTokenLen, tok.length());
+                String terminal = kind2Token.getOrDefault(word.kind, Terminal.apply("<eof>")).toString();
+                terminals.add(terminal);
+                maxTerminalLen = Math.max(maxTerminalLen, terminal.length());
+            }
+            // if the token is absurdly large limit the column to 80 chars to maintain alignment
+            maxTokenLen = Math.min(maxTokenLen, 80);
+            maxTerminalLen = Math.min(maxTerminalLen, 20);
+            sb.append(String.format("|%-" + maxTokenLen + "s | %-" + maxLocLen + "s | %-" + maxTerminalLen + "s|\n",
+                    "\"Match\"", "(location)", "Terminal"));
+            sb.append(String.format("|-%s|--%s|-%s|\n", "-".repeat(maxTokenLen), "-".repeat(maxLocLen), "-".repeat(maxTerminalLen)));
+            for (int i = 0; i < words.size(); i++) {
+                Scanner.Token word = words.get(i);
+                sb.append(String.format("|%-" + maxTokenLen + "s | %-" + maxLocLen + "s | %-" + maxTerminalLen + "s|\n",
+                        tokens.get(i), locs.get(i), terminals.get(i)));
+            }
+        }
+        return sb.toString();
+    }
+
     public Tuple2<Either<Set<KEMException>, K>, Set<KEMException>>
             parseString(String input, Sort startSymbol, String startSymbolLocation, Source source) {
         try (Scanner scanner = getScanner()) {
diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java
index 7f48bda662e..8f3f541295e 100644
--- a/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java
+++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java
@@ -1,6 +1,7 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.parser.inner.kernel;
 
+import com.google.common.primitives.Ints;
 import org.apache.commons.codec.binary.StringUtils;
 import org.jetbrains.annotations.NotNull;
 import org.kframework.attributes.Att;
@@ -23,18 +24,7 @@
 import org.pcollections.ConsPStack;
 import org.pcollections.PStack;
 
-import java.nio.charset.StandardCharsets;
-import java.util.Arrays;
-import java.util.ArrayList;
-import java.util.BitSet;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.Iterator;
-import java.util.List;
-import java.util.Map;
-import java.util.Objects;
-import java.util.Optional;
-import java.util.Set;
+import java.util.*;
 import java.util.stream.Collectors;
 
 import static org.kframework.Collections.*;
@@ -525,7 +515,7 @@ public void finish() {
    * Metadata about the state of the sentence being parsed. We collect this all in a single place in order to simplify
    * the type signatures of many methods.
    */
-  private static class ParserMetadata {
+  public static class ParserMetadata {
     /**
      * @param input The sentence being parsed
      * @param scanner The scanner to use to tokenize the sentence
@@ -583,15 +573,27 @@ public ParserMetadata(String input, Scanner scanner, Source source, int startLin
     }
 
     // the list of tokens in the sentence
-    Scanner.Token[] words;
+    final Scanner.Token[] words;
     // an array containing the line of each character in the input sentence
-    int[] lines;
+    final int[] lines;
     // an array containing the column of each character in the input sentence
-    int[] columns;
+    final int[] columns;
     // a Source containing the file the sentence was parsed from
     Source source;
     // the original un-tokenized input sentence
     String input;
+
+    public List<Scanner.Token> getWords() {
+      return List.of(words);
+    }
+
+    public List<Integer> getLines() {
+      return Collections.unmodifiableList(Ints.asList(lines));
+    }
+
+    public List<Integer> getColumns() {
+      return Collections.unmodifiableList(Ints.asList(columns));
+    }
   }
 
   /**
diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java
index d59300a5b39..b71d0c44c16 100644
--- a/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java
+++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java
@@ -30,14 +30,7 @@
 import java.nio.ByteOrder;
 import java.nio.file.StandardCopyOption;
 import java.nio.file.Files;
-import java.util.ArrayList;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.LinkedHashMap;
-import java.util.List;
-import java.util.Map;
-import java.util.Set;
-import java.util.TreeMap;
+import java.util.*;
 import java.util.concurrent.Semaphore;
 import java.util.function.BiConsumer;
 import java.util.stream.Collectors;
@@ -57,6 +50,10 @@ public class Scanner implements AutoCloseable {
 
     public static final String COMPILER = OS.current().equals(OS.OSX) ? "clang" : "gcc";
 
+    public Map<TerminalLike, Tuple2<Integer, Integer>> getTokens() {
+        return Collections.unmodifiableMap(tokens);
+    }
+
     public static Map<TerminalLike, Tuple2<Integer, Integer>> getTokens(Module module) {
         Map<TerminalLike, Integer> tokens = new TreeMap<>();
         Set<String> terminals = new HashSet<>();
@@ -349,10 +346,10 @@ public int resolve(TerminalLike terminal) {
     }
 
     public static class Token {
-        final int kind;
-        final String value;
-        final int startLoc;
-        final int endLoc;
+        public final int kind;
+        public final String value;
+        public final int startLoc;
+        public final int endLoc;
 
         public Token(int kind, String value, long startLoc, long endLoc) {
             this.kind = kind;

From b3c4644d21b1d3cd461b36bffaaf984c624aadd3 Mon Sep 17 00:00:00 2001
From: gtrepta <50716988+gtrepta@users.noreply.github.com>
Date: Wed, 4 Oct 2023 18:02:56 -0500
Subject: [PATCH 4/5] Packaging: `version` path fix (#3691)

Follow up to finish #3683

---------

Co-authored-by: Roberto Rosmaninho <robertogomes@dcc.ufmg.br>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>
---
 k-distribution/src/main/scripts/lib/k |  2 +-
 package/test-package                  | 22 ++++++++++++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/k-distribution/src/main/scripts/lib/k b/k-distribution/src/main/scripts/lib/k
index 34f4bf3b639..1d510a2ff60 100755
--- a/k-distribution/src/main/scripts/lib/k
+++ b/k-distribution/src/main/scripts/lib/k
@@ -22,7 +22,7 @@ for flag in "$@"; do
         fi
 
         if [[ -z "${version}" ]]; then
-            version="v"$(cat "${K_BASE}"/version)
+            version="v"$(cat "${K_BASE}"/kframework/version)
         fi
 
         echo "K version:    ${version}"
diff --git a/package/test-package b/package/test-package
index 704750337ac..6c4ae1f0bcb 100755
--- a/package/test-package
+++ b/package/test-package
@@ -23,5 +23,27 @@ sort_int = kllvm.ast.CompositeSort("SortInt")
 assert str(sort_int) == "SortInt{}"
 HERE
 
+# Make sure that the help messages work and that the version of the various components is correct
+PACKAGE_VERSION=$(cat /usr/lib/kframework/version)
+
+kast          --help    | grep -q -- "--version"
+kdep          --help    | grep -q -- "--version"
+kompile       --help    | grep -q -- "--version"
+kprove        --help    | grep -q -- "--version"
+krun          --help    | grep -q -- "--version"
+kserver       --help    | grep -q -- "--version"
+kparse        --help    | grep -q -- "--version"
+kparse-gen    --help    | grep -q -- "--version"
+kore-print    --help    | grep -q -- "--version"
+kast          --version | grep -q ${PACKAGE_VERSION}
+kdep          --version | grep -q ${PACKAGE_VERSION}
+kompile       --version | grep -q ${PACKAGE_VERSION}
+kprove        --version | grep -q ${PACKAGE_VERSION}
+krun          --version | grep -q ${PACKAGE_VERSION}
+kserver       --version | grep -q ${PACKAGE_VERSION}
+kparse        --version | grep -q ${PACKAGE_VERSION}
+kparse-gen    --version | grep -q ${PACKAGE_VERSION}
+kore-print    --version | grep -q ${PACKAGE_VERSION}
+
 # Make sure that the Haskell Backend Booster has been installed properly.
 kore-rpc-booster --help

From 8abe514b4ced4766044ba54561176b5c5f89053e Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Thu, 5 Oct 2023 12:03:36 -0600
Subject: [PATCH 5/5] Use prebuilt z3 images (#3694)

This uses the prebuilt Z3 images from:
https://github.com/runtimeverification/z3-images

This should speed up CI process.

Note that the debian packagaes are not changed in Z3 image used, just
the normal CI. So we are still testing with version 4.8.15 as well in
the packaging process. We could also change that to 4.12.1, but then we
wouldn't be testing the minimum recommended version.

Co-authored-by: Freeman <105403280+F-WRunTime@users.noreply.github.com>
---
 .github/actions/with-docker/action.yml |  9 +--------
 .github/workflows/Dockerfile           |  3 ++-
 .github/workflows/Dockerfile.z3        | 24 ------------------------
 deps/z3                                |  1 +
 4 files changed, 4 insertions(+), 33 deletions(-)
 delete mode 100644 .github/workflows/Dockerfile.z3
 create mode 100644 deps/z3

diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
index 106f8de707e..9dfe5840555 100644
--- a/.github/actions/with-docker/action.yml
+++ b/.github/actions/with-docker/action.yml
@@ -42,20 +42,13 @@ runs:
     run: |
       set -euxo pipefail
 
-      Z3_VERSION=4.8.15
+      Z3_VERSION=$(cat deps/z3)
       K_VERSION=$(cat ${SUBDIR}package/version)
       USER=$(id -un)
       USER_ID=$(id -u)
       GROUP=$(id -gn)
       GROUP_ID=$(id -g)
 
-      docker build ${SUBDIR}                                          \
-          --build-arg USER=${USER} --build-arg USER_ID=${USER_ID}     \
-          --build-arg GROUP=${GROUP} --build-arg GROUP_ID=${GROUP_ID} \
-          --build-arg BASE_OS=${BASE_OS}                              \
-          --build-arg BASE_DISTRO=${BASE_DISTRO}                      \
-          --tag z3:${BASE_DISTRO}-${Z3_VERSION}                       \
-          --file ${SUBDIR}${DOCKERFILE}.z3
       docker build ${SUBDIR}                                          \
           --build-arg USER=${USER} --build-arg USER_ID=${USER_ID}     \
           --build-arg GROUP=${GROUP} --build-arg GROUP_ID=${GROUP_ID} \
diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile
index 1e60083f4ef..d250f1c033d 100644
--- a/.github/workflows/Dockerfile
+++ b/.github/workflows/Dockerfile
@@ -1,8 +1,9 @@
 ARG BASE_OS
 ARG BASE_DISTRO
 ARG K_VERSION
+
 ARG Z3_VERSION
-FROM z3:${BASE_DISTRO}-${Z3_VERSION} as Z3
+FROM runtimeverificationinc/${BASE_OS}-${BASE_DISTRO}-z3:${Z3_VERSION} as Z3
 
 ARG BASE_OS
 ARG BASE_DISTRO
diff --git a/.github/workflows/Dockerfile.z3 b/.github/workflows/Dockerfile.z3
deleted file mode 100644
index c2ec54df25c..00000000000
--- a/.github/workflows/Dockerfile.z3
+++ /dev/null
@@ -1,24 +0,0 @@
-ARG BASE_DISTRO
-ARG BASE_OS
-FROM ${BASE_OS}:${BASE_DISTRO}
-
-ENV TZ=America/Chicago
-RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
-
-RUN    apt-get update        \
-    && apt-get upgrade --yes \
-    && apt-get install --yes \
-            clang            \
-            cmake            \
-            git              \
-            python3
-
-ARG Z3_VERSION=4.8.15
-RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-${Z3_VERSION} \
-    && cd z3                                                                \
-    && python3 scripts/mk_make.py                                           \
-    && cd build                                                             \
-    && make -j8                                                             \
-    && make install                                                         \
-    && cd ../..                                                             \
-    && rm -rf z3
diff --git a/deps/z3 b/deps/z3
new file mode 100644
index 00000000000..53cf85e173b
--- /dev/null
+++ b/deps/z3
@@ -0,0 +1 @@
+4.12.1