Checks on main/syntax modules during module exclusion (#3561)

* Add test for attributes on main/syntax modules

* Check attributes on main/syntax module when excluding modules

k-distribution/tests/regression-new/excludedModuleAtts/Makefile

@@ -0,0 +1,2 @@
+SUBDIRS=$(filter-out Makefile, $(wildcard *))
+include ../../../include/kframework/ktest-group.mak

k-distribution/tests/regression-new/excludedModuleAtts/haskell/Makefile

@@ -0,0 +1,4 @@
+DEF=test
+KOMPILE_BACKEND=haskell
+
+include ../../../../include/kframework/ktest-fail.mak

k-distribution/tests/regression-new/excludedModuleAtts/haskell/test-entry.k

@@ -0,0 +1,8 @@
+// Copyright (c) K Team. All Rights Reserved.
+module TEST-ENTRY-SYNTAX [concrete]
+
+endmodule
+
+module TEST-ENTRY
+
+endmodule

k-distribution/tests/regression-new/excludedModuleAtts/haskell/test-entry.k.out

@@ -0,0 +1 @@
+[Error] Compiler: Syntax module TEST-ENTRY-SYNTAX has excluded attribute [concrete].

k-distribution/tests/regression-new/excludedModuleAtts/haskell/test-main.k

@@ -0,0 +1,8 @@
+// Copyright (c) K Team. All Rights Reserved.
+module TEST-MAIN-SYNTAX
+
+endmodule
+
+module TEST-MAIN [concrete]
+
+endmodule

k-distribution/tests/regression-new/excludedModuleAtts/haskell/test-main.k.out

@@ -0,0 +1 @@
+[Error] Compiler: Main module TEST-MAIN has excluded attribute [concrete].

k-distribution/tests/regression-new/excludedModuleAtts/llvm/Makefile

@@ -0,0 +1,3 @@
+DEF=test
+
+include ../../../../include/kframework/ktest-fail.mak

k-distribution/tests/regression-new/excludedModuleAtts/llvm/test-entry.k

@@ -0,0 +1,8 @@
+// Copyright (c) K Team. All Rights Reserved.
+module TEST-ENTRY-SYNTAX [symbolic]
+
+endmodule
+
+module TEST-ENTRY
+
+endmodule

k-distribution/tests/regression-new/excludedModuleAtts/llvm/test-entry.k.out

@@ -0,0 +1 @@
+[Error] Compiler: Syntax module TEST-ENTRY-SYNTAX has excluded attribute [symbolic].

k-distribution/tests/regression-new/excludedModuleAtts/llvm/test-main.k

@@ -0,0 +1,8 @@
+// Copyright (c) K Team. All Rights Reserved.
+module TEST-MAIN-SYNTAX
+
+endmodule
+
+module TEST-MAIN [symbolic]
+
+endmodule

k-distribution/tests/regression-new/excludedModuleAtts/llvm/test-main.k.out

@@ -0,0 +1 @@
+[Error] Compiler: Main module TEST-MAIN has excluded attribute [symbolic].

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

@@ -161,7 +161,7 @@ public java.util.Set<Module> parseModules(CompiledDefinition definition, String
                 stream(def.entryModules()).filter(m -> stream(m.sentences()).noneMatch(s -> s instanceof Bubble)));
         def = Definition(def.mainModule(), modules.collect(Collections.toSet()), def.att());
 
-        def = Kompile.excludeModulesByTag(excludeModules).apply(def);
+        def = Kompile.excludeModulesByTag(excludeModules, entryPointModule).apply(def);
         sw.printIntermediate("Outer parsing [" + def.modules().size() + " modules]");
 
         errors = java.util.Collections.synchronizedSet(Sets.newHashSet());
@@ -222,7 +222,7 @@ public Definition parseDefinitionAndResolveBubbles(File definitionFile, String m
                 stream(parsedDefinition.entryModules()).filter(m -> stream(m.sentences()).noneMatch(s -> s instanceof Bubble)));
         Definition trimmed = Definition(parsedDefinition.mainModule(), modules.collect(Collections.toSet()),
                 parsedDefinition.att());
-        trimmed = Kompile.excludeModulesByTag(excludedModuleTags).apply(trimmed);
+        trimmed = Kompile.excludeModulesByTag(excludedModuleTags, mainProgramsModule).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(".");

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

@@ -314,9 +314,27 @@ private static Module excludeModulesByTag(Set<Att.Key> excludedModuleTags, Modul
         return Module(mod.name(), immutable(newImports), mod.localSentences(), mod.att());
     }
 
-    public static Function1<Definition, Definition> excludeModulesByTag(Set<Att.Key> excludedModuleTags) {
-        DefinitionTransformer dt = DefinitionTransformer.from(mod -> excludeModulesByTag(excludedModuleTags, mod), "remove modules based on attributes");
-        return dt.andThen(d -> Definition(d.mainModule(), immutable(stream(d.entryModules()).filter(mod -> excludedModuleTags.stream().noneMatch(tag -> mod.att().contains(tag))).collect(Collectors.toSet())), d.att()));
+    private static Definition excludeModulesByTag(Set<Att.Key> excludedModuleTags, String syntaxModule, Definition d) {
+        for (Att.Key k : excludedModuleTags) {
+            if (d.mainModule().att().contains(k)) {
+                throw KEMException.compilerError("Main module " + d.mainModule().name() + " has excluded attribute [" + k + "].");
+            }
+            d.getModule(syntaxModule).map(m -> {
+                if (m.att().contains(k)) {
+                    throw KEMException.compilerError("Syntax module " + m.name() + " has excluded attribute [" + k + "].");
+                }
+                return null;
+            });
+        }
+
+        return Definition(d.mainModule(), immutable(stream(d.entryModules()).filter(mod -> excludedModuleTags.stream().noneMatch(tag -> mod.att().contains(tag))).collect(Collectors.toSet())), d.att());
+    }
+
+    public static Function1<Definition, Definition> excludeModulesByTag(Set<Att.Key> excludedModuleTags, String syntaxModule) {
+        Function1<Definition, Definition> excludeModules = d -> excludeModulesByTag(excludedModuleTags, syntaxModule, d);
+        DefinitionTransformer walkModules = DefinitionTransformer.from(mod -> excludeModulesByTag(excludedModuleTags, mod), "remove modules based on attributes");
+
+        return excludeModules.andThen(walkModules);
     }
 
     public static Sentence removePolyKLabels(Sentence s) {