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 <[email protected]>
runtimeverification · Oct 4, 2023 · 079db21 · 079db21
1 parent 3e7fdeb
commit 079db21
Show file tree

Hide file tree

Showing 33 changed files with 84 additions and 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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> {