Merge remote-tracking branch 'origin/develop'

runtimeverification · Apr 11, 2024 · b6e2cd3 · b6e2cd3
2 parents f5b931b + 330831d
commit b6e2cd3
Show file tree

Hide file tree

Showing 15 changed files with 83 additions and 51 deletions.
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java
@@ -58,7 +58,7 @@ public void accept(Backend.Holder h) {
       args.add(haskellKompileOptions.haskellBackendCommand);
       args.add("definition.kore");
       args.add("--module");
-      args.add(kompileOptions.mainModule(files));
+      args.add(kompileOptions.mainModule(files).name());
       args.add("--output");
       args.add("haskellDefinition.bin");
       args.add("--serialize");

diff --git a/k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala b/k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala
@@ -54,8 +54,8 @@ class KoreTest {
     files.saveToDefinitionDirectory("test.k", k)
     val defn = compiler.run(
       files.resolveDefinitionDirectory("test.k"),
-      "TEST",
-      "TEST",
+      new KompileOptions.MainModule("TEST", KompileOptions.OptionType.USER_PROVIDED),
+      new KompileOptions.SyntaxModule("TEST", KompileOptions.OptionType.USER_PROVIDED),
       backend.steps,
       backend.excludedModuleTags
     )

diff --git a/k-distribution/tests/regression-new/issue-4153-missing-module/Makefile b/k-distribution/tests/regression-new/issue-4153-missing-module/Makefile
@@ -0,0 +1,2 @@
+KOMPILE_FLAGS=--syntax-module FOO
+include ../../../include/kframework/ktest-fail.mak
diff --git a/k-distribution/tests/regression-new/issue-4153-missing-module/test.k b/k-distribution/tests/regression-new/issue-4153-missing-module/test.k
@@ -0,0 +1,2 @@
+module TEST
+endmodule
diff --git a/k-distribution/tests/regression-new/issue-4153-missing-module/test.k.out b/k-distribution/tests/regression-new/issue-4153-missing-module/test.k.out
@@ -0,0 +1 @@
+[Error] Compiler: Could not find main syntax module with name FOO in definition.
diff --git a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java
@@ -39,7 +39,6 @@
 import org.kframework.definition.ContextAlias;
 import org.kframework.definition.Definition;
 import org.kframework.definition.DefinitionTransformer;
-import org.kframework.definition.Import;
 import org.kframework.definition.Module;
 import org.kframework.definition.Production;
 import org.kframework.definition.Rule;
@@ -134,7 +133,7 @@ public DefinitionParsing(
 
   public java.util.Set<Module> parseModules(
       CompiledDefinition definition,
-      String mainModule,
+      KompileOptions.MainModule mainModule,
       String entryPointModule,
       File definitionFile,
       java.util.Set<Att.Key> excludeModules,
@@ -151,16 +150,17 @@ public java.util.Set<Module> parseModules(
             options.preprocess,
             options.bisonLists);
 
-    if (!def.getModule(mainModule).isDefined()) {
+    if (!def.getModule(mainModule.name()).isDefined()) {
       throw KEMException.criticalError("Module " + mainModule + " does not exist.");
     }
     if (!def.getModule(entryPointModule).isDefined()) {
       throw KEMException.criticalError("Module " + entryPointModule + " does not exist.");
     }
     if (profileRules) // create the temp dir ahead of parsing to avoid a race condition
     files.resolveTemp(".");
-    Stream<Module> modules = Stream.of(def.getModule(mainModule).get());
-    modules = Stream.concat(modules, stream(def.getModule(mainModule).get().importedModules()));
+    Stream<Module> modules = Stream.of(def.getModule(mainModule.name()).get());
+    modules =
+        Stream.concat(modules, stream(def.getModule(mainModule.name()).get().importedModules()));
     modules = Stream.concat(modules, Stream.of(def.getModule(entryPointModule).get()));
     modules =
         Stream.concat(modules, stream(def.getModule(entryPointModule).get().importedModules()));
@@ -217,14 +217,14 @@ private void saveCaches() {
 
   public Definition parseDefinitionAndResolveBubbles(
       File definitionFile,
-      String mainModuleName,
-      String mainProgramsModule,
+      KompileOptions.MainModule mainModuleName,
+      KompileOptions.SyntaxModule mainProgramsModule,
       java.util.Set<Att.Key> excludedModuleTags) {
     Definition parsedDefinition =
         parseDefinition(definitionFile, mainModuleName, mainProgramsModule);
     Stream<Module> modules = Stream.of(parsedDefinition.mainModule());
     modules = Stream.concat(modules, stream(parsedDefinition.mainModule().importedModules()));
-    Option<Module> syntaxModule = parsedDefinition.getModule(mainProgramsModule);
+    Option<Module> syntaxModule = parsedDefinition.getModule(mainProgramsModule.name());
     if (syntaxModule.isDefined()) {
       modules = Stream.concat(modules, Stream.of(syntaxModule.get()));
       modules = Stream.concat(modules, stream(syntaxModule.get().importedModules()));
@@ -249,7 +249,8 @@ public Definition parseDefinitionAndResolveBubbles(
             parsedDefinition.mainModule(),
             modules.collect(Collections.toSet()),
             parsedDefinition.att());
-    trimmed = Kompile.excludeModulesByTag(excludedModuleTags, mainProgramsModule).apply(trimmed);
+    trimmed =
+        Kompile.excludeModulesByTag(excludedModuleTags, mainProgramsModule.name()).apply(trimmed);
     sw.printIntermediate("Outer parsing [" + trimmed.modules().size() + " modules]");
     if (profileRules) // create the temp dir ahead of parsing to avoid a race condition
     files.resolveTemp(".");
@@ -284,7 +285,9 @@ private void throwExceptionIfThereAreErrors() {
   }
 
   public Definition parseDefinition(
-      File definitionFile, String mainModuleName, String mainProgramsModule) {
+      File definitionFile,
+      KompileOptions.MainModule mainModuleName,
+      KompileOptions.SyntaxModule mainProgramsModule) {
     return parser.loadDefinition(
         mainModuleName,
         mainProgramsModule,

diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java
@@ -202,8 +202,8 @@ public Kompile(
    */
   public CompiledDefinition run(
       File definitionFile,
-      String mainModuleName,
-      String mainProgramsModuleName,
+      KompileOptions.MainModule mainModuleName,
+      KompileOptions.SyntaxModule mainProgramsModuleName,
       Function<Definition, Definition> pipeline,
       Set<Att.Key> excludedModuleTags) {
     files.resolveKompiled(".").mkdirs();
@@ -383,8 +383,8 @@ private static String ruleSourceMap(Definition def) {
 
   public Definition parseDefinition(
       File definitionFile,
-      String mainModuleName,
-      String mainProgramsModule,
+      KompileOptions.MainModule mainModuleName,
+      KompileOptions.SyntaxModule mainProgramsModule,
       Set<Att.Key> excludedModuleTags) {
     return definitionParsing.parseDefinitionAndResolveBubbles(
         definitionFile, mainModuleName, mainProgramsModule, excludedModuleTags);
@@ -821,7 +821,7 @@ public Rule compileRule(Definition compiledDef, Rule parsedRule) {
 
   public Set<Module> parseModules(
       CompiledDefinition definition,
-      String mainModule,
+      KompileOptions.MainModule mainModule,
       String entryPointModule,
       File definitionFile,
       Set<Att.Key> excludedModuleTags,

diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
@@ -22,6 +22,11 @@
 
 @RequestScoped
 public class KompileOptions implements Serializable {
+  public enum OptionType {
+    DEFAULT,
+    USER_PROVIDED
+  }
+
   @Inject
   public KompileOptions() {}
 
@@ -62,12 +67,15 @@ GlobalOptions getGlobalOptions_UseOnlyInGuiceProvider() {
               + " extension (.k).")
   private String mainModule;
 
-  public String mainModule(FileUtil files) {
+  public record MainModule(String name, OptionType type) {}
+
+  public MainModule mainModule(FileUtil files) {
     if (mainModule == null) {
-      return FilenameUtils.getBaseName(outerParsing.mainDefinitionFile(files).getName())
-          .toUpperCase();
+      return new MainModule(
+          FilenameUtils.getBaseName(outerParsing.mainDefinitionFile(files).getName()).toUpperCase(),
+          OptionType.DEFAULT);
     }
-    return mainModule;
+    return new MainModule(mainModule, OptionType.USER_PROVIDED);
   }
 
   @Parameter(
@@ -78,11 +86,13 @@ public String mainModule(FileUtil files) {
               + " <main-module>-SYNTAX).")
   private String syntaxModule;
 
-  public String syntaxModule(FileUtil files) {
+  public record SyntaxModule(String name, OptionType type) {}
+
+  public SyntaxModule syntaxModule(FileUtil files) {
     if (syntaxModule == null) {
-      return mainModule(files) + "-SYNTAX";
+      return new SyntaxModule(mainModule(files).name() + "-SYNTAX", OptionType.DEFAULT);
     }
-    return syntaxModule;
+    return new SyntaxModule(syntaxModule, OptionType.USER_PROVIDED);
   }
 
   @Parameter(names = "--coverage", description = "Generate coverage data when executing semantics.")

diff --git a/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java b/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java
@@ -18,6 +18,7 @@
 import org.kframework.definition.Module;
 import org.kframework.kompile.CompiledDefinition;
 import org.kframework.kompile.Kompile;
+import org.kframework.kompile.KompileOptions;
 import org.kframework.utils.Stopwatch;
 import org.kframework.utils.errorsystem.KEMException;
 import org.kframework.utils.file.FileUtil;
@@ -50,7 +51,8 @@ public Tuple2<Definition, Module> build(File specFile, String specModuleName) {
     Set<Module> modules =
         kompile.parseModules(
             compiledDefinition,
-            defModuleNameUpdated,
+            new KompileOptions.MainModule(
+                defModuleNameUpdated, KompileOptions.OptionType.USER_PROVIDED),
             specModuleNameUpdated,
             absSpecFile,
             backend.excludedModuleTags(),

diff --git a/kernel/src/main/java/org/kframework/parser/ParserUtils.java b/kernel/src/main/java/org/kframework/parser/ParserUtils.java
@@ -2,7 +2,6 @@
 package org.kframework.parser;
 
 import static org.kframework.Collections.*;
-import static org.kframework.kore.KORE.*;
 
 import com.google.common.collect.Streams;
 import java.io.File;
@@ -30,6 +29,7 @@
 import org.kframework.kil.Require;
 import org.kframework.kil.loader.Context;
 import org.kframework.kompile.Kompile;
+import org.kframework.kompile.KompileOptions;
 import org.kframework.kore.convertors.KILtoKORE;
 import org.kframework.main.GlobalOptions;
 import org.kframework.main.Main;
@@ -310,7 +310,7 @@ public Set<Module> loadModules(
   }
 
   public org.kframework.definition.Definition loadDefinition(
-      String mainModuleName,
+      KompileOptions.MainModule mainModuleName,
       Set<Module> previousModules,
       String definitionText,
       Source source,
@@ -337,8 +337,8 @@ public org.kframework.definition.Definition loadDefinition(
   }
 
   public org.kframework.definition.Definition loadDefinition(
-      String mainModuleName,
-      String syntaxModuleName,
+      KompileOptions.MainModule mainModuleName,
+      KompileOptions.SyntaxModule syntaxModuleName,
       String definitionText,
       File source,
       File currentDirectory,
@@ -365,8 +365,8 @@ public org.kframework.definition.Definition loadDefinition(
   }
 
   public org.kframework.definition.Definition loadDefinition(
-      String mainModuleName,
-      String syntaxModuleName,
+      KompileOptions.MainModule mainModuleName,
+      KompileOptions.SyntaxModule syntaxModuleName,
       String definitionText,
       Source source,
       File currentDirectory,
@@ -406,15 +406,21 @@ public org.kframework.definition.Definition loadDefinition(
     modules.addAll(previousModules); // add the previous modules, since load modules is not additive
     Module mainModule = getMainModule(mainModuleName, modules);
     Optional<Module> opt;
-    opt = modules.stream().filter(m -> m.name().equals(syntaxModuleName)).findFirst();
+    opt = modules.stream().filter(m -> m.name().equals(syntaxModuleName.name())).findFirst();
     Module syntaxModule;
     if (opt.isEmpty()) {
+      if (syntaxModuleName.type().equals(KompileOptions.OptionType.USER_PROVIDED)) {
+        throw KEMException.compilerError(
+            "Could not find main syntax module with name "
+                + syntaxModuleName.name()
+                + " in definition.");
+      }
       kem.registerCompilerWarning(
           ExceptionType.MISSING_SYNTAX_MODULE,
           "Could not find main syntax module with name "
-              + syntaxModuleName
+              + syntaxModuleName.name()
               + " in definition.  Use --syntax-module to specify one. Using "
-              + mainModuleName
+              + mainModuleName.name()
               + " as default.");
       syntaxModule = mainModule;
     } else {
@@ -425,14 +431,16 @@ public org.kframework.definition.Definition loadDefinition(
         mainModule, immutable(modules), Att.empty().add(Att.SYNTAX_MODULE(), syntaxModule.name()));
   }
 
-  private Module getMainModule(String mainModuleName, Set<Module> modules) {
+  private Module getMainModule(KompileOptions.MainModule mainModuleName, Set<Module> modules) {
     Optional<Module> opt =
-        modules.stream().filter(m -> m.name().equals(mainModuleName)).findFirst();
+        modules.stream().filter(m -> m.name().equals(mainModuleName.name())).findFirst();
     if (opt.isEmpty()) {
-      throw KEMException.compilerError(
-          "Could not find main module with name "
-              + mainModuleName
-              + " in definition. Use --main-module to specify one.");
+      String msg =
+          "Could not find main module with name " + mainModuleName.name() + " in definition.";
+      if (mainModuleName.type().equals(KompileOptions.OptionType.DEFAULT)) {
+        msg += " Use --main-module to specify one.";
+      }
+      throw KEMException.compilerError(msg);
     }
     return opt.get();
   }

diff --git a/kernel/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java b/kernel/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java
@@ -22,6 +22,7 @@
 import org.kframework.definition.Production;
 import org.kframework.definition.Sentence;
 import org.kframework.kompile.Kompile;
+import org.kframework.kompile.KompileOptions;
 import org.kframework.kore.K;
 import org.kframework.kore.KApply;
 import org.kframework.kore.Sort;
@@ -50,8 +51,8 @@ public void setUp() {
 
     def =
         parser.loadDefinition(
-            "K",
-            "K",
+            new KompileOptions.MainModule("K", KompileOptions.OptionType.USER_PROVIDED),
+            new KompileOptions.SyntaxModule("K", KompileOptions.OptionType.USER_PROVIDED),
             definitionText,
             definitionFile,
             definitionFile.getParentFile(),

diff --git a/kernel/src/test/java/org/kframework/kompile/KompileOptionsTest.java b/kernel/src/test/java/org/kframework/kompile/KompileOptionsTest.java
@@ -55,12 +55,12 @@ public void testNoDefinition() throws Exception {
   @Test
   public void testDefaultModuleName() {
     parse("foo.k");
-    assertEquals("FOO", options.mainModule(files));
+    assertEquals("FOO", options.mainModule(files).name());
   }
 
   @Test
   public void testDefaultSyntaxModuleName() {
     parse("--main-module", "BAR", "foo.k");
-    assertEquals("BAR-SYNTAX", options.syntaxModule(files));
+    assertEquals("BAR-SYNTAX", options.syntaxModule(files).name());
   }
 }
diff --git a/kernel/src/test/java/org/kframework/parser/inner/RuleGrammarTest.java b/kernel/src/test/java/org/kframework/parser/inner/RuleGrammarTest.java
@@ -18,6 +18,7 @@
 import org.kframework.definition.RegexTerminal;
 import org.kframework.kompile.DefinitionParsing;
 import org.kframework.kompile.Kompile;
+import org.kframework.kompile.KompileOptions;
 import org.kframework.kore.K;
 import org.kframework.kore.Sort;
 import org.kframework.kore.convertors.KILtoKORE;
@@ -49,8 +50,8 @@ public RuleGrammarGenerator makeRuleGrammarGenerator() {
 
     Definition baseK =
         parser.loadDefinition(
-            "K",
-            "K",
+            new KompileOptions.MainModule("K", KompileOptions.OptionType.USER_PROVIDED),
+            new KompileOptions.SyntaxModule("K", KompileOptions.OptionType.USER_PROVIDED),
             definitionText,
             definitionFile,
             definitionFile.getParentFile(),

diff --git a/kernel/src/test/java/org/kframework/parser/inner/disambiguation/AddEmptyListsTest.java b/kernel/src/test/java/org/kframework/parser/inner/disambiguation/AddEmptyListsTest.java
@@ -16,6 +16,7 @@
 import org.kframework.definition.Definition;
 import org.kframework.definition.Module;
 import org.kframework.kompile.Kompile;
+import org.kframework.kompile.KompileOptions;
 import org.kframework.kore.K;
 import org.kframework.kore.KApply;
 import org.kframework.kore.KLabel;
@@ -58,8 +59,8 @@ private RuleGrammarGenerator makeRuleGrammarGenerator() {
 
     Definition baseK =
         parser.loadDefinition(
-            "K",
-            "K",
+            new KompileOptions.MainModule("K", KompileOptions.OptionType.USER_PROVIDED),
+            new KompileOptions.SyntaxModule("K", KompileOptions.OptionType.USER_PROVIDED),
             definitionText,
             definitionFile,
             definitionFile.getParentFile(),

diff --git a/kernel/src/test/java/org/kframework/unparser/AddBracketsTest.java b/kernel/src/test/java/org/kframework/unparser/AddBracketsTest.java
@@ -13,6 +13,7 @@
 import org.kframework.definition.Definition;
 import org.kframework.definition.Module;
 import org.kframework.kompile.Kompile;
+import org.kframework.kompile.KompileOptions;
 import org.kframework.kore.K;
 import org.kframework.main.GlobalOptions;
 import org.kframework.parser.ParserUtils;
@@ -45,8 +46,8 @@ public RuleGrammarGenerator makeRuleGrammarGenerator() {
 
     Definition baseK =
         parser.loadDefinition(
-            "K",
-            "K",
+            new KompileOptions.MainModule("K", KompileOptions.OptionType.USER_PROVIDED),
+            new KompileOptions.SyntaxModule("K", KompileOptions.OptionType.USER_PROVIDED),
             definitionText,
             definitionFile,
             definitionFile.getParentFile(),
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		KOMPILE_FLAGS=--syntax-module FOO
		include ../../../include/kframework/ktest-fail.mak
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		[Error] Compiler: Could not find main syntax module with name FOO in definition.