diff --git a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java index 105ffdae8b..3005cda089 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java @@ -10,11 +10,14 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; +import java.util.Map; +import java.util.NoSuchElementException; import java.util.Objects; import java.util.Stack; import java.util.concurrent.CompletableFuture; import java.util.concurrent.atomic.AtomicInteger; import java.util.function.Function; +import java.util.stream.Collectors; import java.util.stream.Stream; import java.util.stream.StreamSupport; @@ -86,9 +89,23 @@ public void taskFinished(TaskFinishedInfo info) { }; private final AtomicInteger uniqueCounter = new AtomicInteger(); + // Available macros and script commands are discovered via the service loader + // (a classpath scan). They don't change at runtime, so scan once here instead + // of on every getAvailableMacros/getAvailableScriptCommands/macro request. + private final List availableMacros = loadAll(ProofMacro.class); + private final List availableScriptCommands = + loadAll(ProofScriptCommand.class); + private final Map macrosByName = availableMacros.stream() + .collect(Collectors.toUnmodifiableMap(ProofMacro::getName, m -> m, (a, b) -> a)); + public KeyApiImpl() { } + private static List loadAll(Class service) { + return StreamSupport.stream( + ClassLoaderUtil.loadServices(service).spliterator(), false).toList(); + } + @Override @JsonRequest public CompletableFuture> examples() { @@ -124,18 +141,13 @@ public CompletableFuture getVersion() { @Override public CompletableFuture> getAvailableMacros() { return CompletableFuture.completedFuture( - StreamSupport - .stream(ClassLoaderUtil.loadServices(ProofMacro.class).spliterator(), false) - .map(ProofMacroDesc::from).toList()); + availableMacros.stream().map(ProofMacroDesc::from).toList()); } @Override public CompletableFuture> getAvailableScriptCommands() { return CompletableFuture.completedFuture( - StreamSupport - .stream(ClassLoaderUtil.loadServices(ProofScriptCommand.class).spliterator(), - false) - .map(ProofScriptCommandDesc::from).toList()); + availableScriptCommands.stream().map(ProofScriptCommandDesc::from).toList()); } @Override @@ -162,9 +174,10 @@ public CompletableFuture macro(ProofId proofId, String macroName return CompletableFuture.supplyAsync(() -> { var proof = data.find(proofId); var env = data.find(proofId.env()); - var macro = StreamSupport - .stream(ClassLoaderUtil.loadServices(ProofMacro.class).spliterator(), false) - .filter(it -> it.getName().equals(macroName)).findFirst().orElseThrow(); + var macro = macrosByName.get(macroName); + if (macro == null) { + throw new NoSuchElementException("No macro named '" + macroName + "'"); + } try { var info = diff --git a/keyext.api/src/test/java/org/keyproject/key/api/KeyApiServiceCacheTest.java b/keyext.api/src/test/java/org/keyproject/key/api/KeyApiServiceCacheTest.java new file mode 100644 index 0000000000..8c432bb7e5 --- /dev/null +++ b/keyext.api/src/test/java/org/keyproject/key/api/KeyApiServiceCacheTest.java @@ -0,0 +1,36 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.keyproject.key.api; + +import java.util.NoSuchElementException; +import java.util.concurrent.ExecutionException; + +import org.junit.jupiter.api.Assertions; +import org.junit.jupiter.api.Test; + +/** + * Tests for the cached service-loader lookups (macros / script commands). The + * caching is by construction; these guard against regressions in the behaviour. + */ +class KeyApiServiceCacheTest { + @Test + void availableMacrosAndCommandsAreNonEmptyAndStable() throws Exception { + var api = new KeyApiImpl(); + var macros1 = api.getAvailableMacros().get(); + var macros2 = api.getAvailableMacros().get(); + Assertions.assertFalse(macros1.isEmpty(), "expected built-in macros"); + Assertions.assertEquals(macros1, macros2, "repeated calls must be consistent"); + Assertions.assertFalse(api.getAvailableScriptCommands().get().isEmpty(), + "expected built-in script commands"); + } + + @Test + void macroRejectsUnknownName() throws Exception { + var api = new KeyApiImpl(); + var proofId = api.loadTerm("true").get(); + var ex = Assertions.assertThrows(ExecutionException.class, + () -> api.macro(proofId, "definitely-not-a-real-macro", null).get()); + Assertions.assertInstanceOf(NoSuchElementException.class, ex.getCause()); + } +}