From 0a498c394d5526bba2b646d141d8e057f8e02a76 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 9 Feb 2024 12:26:29 -0600 Subject: [PATCH] add back "dead" code that was actually live (#3974) There were a couple methods recently deleted from the K frontend that were actually being used by the Maude backend. I have added them back and annotated them so that they will not be automatically deleted by further dead code elimination in the future. --- .../backend/haskell/HaskellBackend.java | 2 +- .../backend/haskell/HaskellRewriter.java | 2 +- .../kframework/backend/kore/KoreBackend.java | 25 ++++++++++++------- .../utils/errorsystem/KExceptionManager.java | 5 ++++ .../kframework/backend/llvm/LLVMBackend.java | 2 +- 5 files changed, 24 insertions(+), 12 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 index f8a347e878d..db0edf996c9 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java @@ -44,7 +44,7 @@ public HaskellBackend( @Override public void accept(Backend.Holder h) { Stopwatch sw = new Stopwatch(globalOptions); - String kore = getKompiledString(h.def); + String kore = getKompiledString(h.def, true); h.def = null; files.saveToKompiled("definition.kore", kore); sw.printIntermediate(" Print definition.kore"); diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java index de397c0f36d..9d505e12862 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java @@ -365,7 +365,7 @@ private RewriterResult executeKoreCommands( @Override public RewriterResult prove(Module rules, Boolean reuseDef) { - Module kompiledModule = KoreBackend.getKompiledModule(module); + Module kompiledModule = KoreBackend.getKompiledModule(module, true); ModuleToKORE converter = new ModuleToKORE( kompiledModule, diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java index 15b89c6bb6f..85c3bad93d9 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java +++ b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java @@ -57,16 +57,21 @@ public KoreBackend( @Override public void accept(Backend.Holder h) { CompiledDefinition def = h.def; - String kore = getKompiledString(def); + String kore = getKompiledString(def, true); File defFile = kompileOptions.outerParsing.mainDefinitionFile(files); String name = defFile.getName(); String basename = FilenameUtils.removeExtension(name); files.saveToDefinitionDirectory(basename + ".kore", kore); } - /** Convert a CompiledDefinition to a String of a KORE definition. */ - protected String getKompiledString(CompiledDefinition def) { - Module mainModule = getKompiledModule(def.kompiledDefinition.mainModule()); + /** + * Convert a CompiledDefinition to a String of a KORE definition. + * + * @param hasAnd whether the backend in question supports and-patterns during pattern matching. + */ + protected String getKompiledString( + CompiledDefinition def, @SuppressWarnings("unused") boolean hasAnd) { + Module mainModule = getKompiledModule(def.kompiledDefinition.mainModule(), hasAnd); ModuleToKORE converter = new ModuleToKORE(mainModule, def.topCellInitializer, def.kompileOptions); return getKompiledString(converter, files, heatCoolEquations, tool); @@ -94,7 +99,7 @@ public static String getKompiledStringAndWriteSyntaxMacros( return semantics.toString(); } - public static Module getKompiledModule(Module mainModule) { + public static Module getKompiledModule(Module mainModule, boolean hasAnd) { mainModule = ModuleTransformer.fromSentenceTransformer( new AddSortInjections(mainModule)::addInjections, "Add sort injections") @@ -102,10 +107,12 @@ public static Module getKompiledModule(Module mainModule) { mainModule = ModuleTransformer.from(new RemoveUnit()::apply, "Remove unit applications for collections") .apply(mainModule); - mainModule = - ModuleTransformer.fromSentenceTransformer( - new MinimizeTermConstruction(mainModule)::resolve, "Minimize term construction") - .apply(mainModule); + if (hasAnd) { + mainModule = + ModuleTransformer.fromSentenceTransformer( + new MinimizeTermConstruction(mainModule)::resolve, "Minimize term construction") + .apply(mainModule); + } return mainModule; } diff --git a/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java b/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java index 94bf158bf68..4d10cb31174 100644 --- a/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java +++ b/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java @@ -91,6 +91,11 @@ public void registerCriticalWarning(ExceptionType type, String message, Throwabl register(type, KExceptionGroup.CRITICAL, message, e, null, null); } + @SuppressWarnings("unused") + public void registerInternalWarning(ExceptionType type, String message) { + register(type, KExceptionGroup.INTERNAL, message, null, null, null); + } + public void registerInternalWarning(ExceptionType type, String message, Throwable e) { register(type, KExceptionGroup.INTERNAL, message, e, null, null); } diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java index 6b1530eefa8..f977f1eb06c 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java @@ -49,7 +49,7 @@ public LLVMBackend( @Override public void accept(Backend.Holder h) { Stopwatch sw = new Stopwatch(globalOptions); - String kore = getKompiledString(h.def); + String kore = getKompiledString(h.def, true); h.def = null; files.saveToKompiled("definition.kore", kore); sw.printIntermediate(" Print definition.kore");