diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java index 52faa9af592..e56d8566542 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java @@ -325,4 +325,9 @@ public static boolean isTruthValueEvaluationEnabled(Profile profile) { return false; } } + + @Override + public String displayName() { + return NAME; + } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java index 3ab2c458bd3..e0a4134c77d 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java @@ -27,7 +27,6 @@ import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.OneStepSimplifier; import de.uka.ilkd.key.rule.Taclet; -import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.symbolic_execution.profile.SimplifyTermProfile; @@ -818,8 +817,7 @@ protected ImmutableList computeTermLabelConfiguration() : null; initConfig.setSettings(clonedSettings); initConfig.setTaclet2Builder( - (HashMap>) sourceInitConfig.getTaclet2Builder() - .clone()); + new HashMap<>(sourceInitConfig.getTaclet2Builder())); initConfig.setTaclets(sourceInitConfig.getTaclets()); // Create new ProofEnvironment and initialize it with values from initial one. ProofEnvironment env = new ProofEnvironment(initConfig); diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java index e5f650a2b08..bc8ab3570ec 100644 --- a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java +++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java @@ -4,7 +4,10 @@ package de.uka.ilkd.key.wd; import java.net.URL; +import java.util.ArrayList; +import java.util.List; import java.util.Objects; +import java.util.stream.Collectors; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.proof.Proof; @@ -15,21 +18,30 @@ import de.uka.ilkd.key.proof.io.RuleSourceFactory; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.rule.*; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.util.KeYResourceManager; +import org.key_project.logic.Choice; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * @author Alexander Weigl * @version 1 (7/27/25) */ public class WdProfile extends JavaProfile { + private static final Logger LOGGER = LoggerFactory.getLogger(WdProfile.class); + public static final String PROFILE_ID = "java-wd"; public static final String DISPLAY_NAME = "Java Profile + Well-Definedness Checks"; public static final WdProfile INSTANCE = new WdProfile(); + private final RuleCollection wdStandardRules; public WdProfile() { @@ -97,9 +109,54 @@ public RuleCollection getStandardRules() { return wdStandardRules; } + /// {@inheritDoc} + /// + /// @param additionalProfileOptions a string representing the choice of `wdOperator` + /// @return @Override - public void prepareInitConfig(InitConfig baseConfig) { - var wdChoice = baseConfig.choiceNS().lookup(new Name("wdChecks:on")); - baseConfig.activateChoice(wdChoice); + public List prepareInitConfig(InitConfig baseConfig, + @Nullable Configuration additionalProfileOptions) { + var warnings = new ArrayList(2); + var wdChoiceOn = baseConfig.choiceNS().lookup(new Name("wdChecks:on")); + var wdChoiceOff = baseConfig.choiceNS().lookup(new Name("wdChecks:off")); + + if (baseConfig.isChoiceActive(wdChoiceOff)) { + final var message = + "wdChecks:off was set by in the init config, probably given in KeY file. This setting will be ignored"; + warnings.add(message); + LOGGER.warn(message); // this logging is for finding the spot. + } + baseConfig.activateChoice(wdChoiceOn); + + + if (additionalProfileOptions != null) { + final var wdOperator = "wdOperator"; + final var selectedWdOperator = additionalProfileOptions.getString(wdOperator); + if (selectedWdOperator == null) { + return warnings; + } + + var wdOperatorChoice = baseConfig.choiceNS().lookup(selectedWdOperator); + if (wdOperatorChoice == null) { + var choices = baseConfig.choiceNS().allElements() + .stream() + .filter(it -> wdOperator.equals(it.category())) + .map(Choice::toString) + .collect(Collectors.joining(", ")); + + throw new IllegalStateException("Could not find choice for %s.\n Choices known %s." + .formatted(additionalProfileOptions, choices)); + } else { + if (baseConfig.isChoiceCategorySet(wdOperator) + && !baseConfig.isChoiceActive(wdOperatorChoice)) { + final var message = "Choice for wdOperator will be overwritten " + + "by profile as defined by user in the additional profile options."; + warnings.add(message); + LOGGER.warn(message); // this logging is for finding the spot. + } + baseConfig.activateChoice(wdOperatorChoice); + } + } + return warnings; } } diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java index 49ba53d71a6..e2a255c23b8 100644 --- a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java +++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java @@ -17,7 +17,6 @@ import org.jspecify.annotations.NonNull; import org.jspecify.annotations.NullMarked; -import org.jspecify.annotations.Nullable; @NullMarked @@ -38,10 +37,6 @@ public Name name() { return NAME; } - @Override - public @Nullable String getOrigin() { - return super.getOrigin(); - } protected static class WdWhileInvariantRuleApplier extends WhileInvariantRuleApplier { public WdWhileInvariantRuleApplier(Goal goal, LoopInvariantBuiltInRuleApp ruleApp) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ChoiceInformation.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ChoiceInformation.java index a32d3325b5e..c7763f38556 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/ChoiceInformation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/ChoiceInformation.java @@ -42,7 +42,7 @@ public class ChoiceInformation { /** * This map contains the default option for every category. */ - private final Map defaultOptions = new TreeMap<>(); + private final Map defaultOptions = new TreeMap<>(); public ChoiceInformation() { this(new Namespace<>()); @@ -68,11 +68,11 @@ public Namespace getChoices() { return choices; } - public void setDefaultOption(String category, String choice) { - defaultOptions.put(category, category + ":" + choice); + public void setDefaultOption(String category, Choice choice) { + defaultOptions.put(category, choice); } - public Map getDefaultOptions() { + public Map getDefaultOptions() { return defaultOptions; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index 22a4e64f10d..61b92c54b87 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -191,6 +191,16 @@ public Configuration asConfiguration() { throw new RuntimeException("Error in configuration. Source: " + ctx.start.getTokenSource().getSourceName()); } + + public List asConfigurationList() { + final var cfg = new ConfigurationBuilder(); + List res = cfg.visitCfile(ctx); + if (!res.isEmpty()) + return (List) res.getFirst(); + else + throw new RuntimeException("Error in configuration. Source: " + + ctx.start.getTokenSource().getSourceName()); + } } public static class SetStatementContext extends KeyAst { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java index 06da0a1a4d8..817ec359382 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java @@ -56,8 +56,9 @@ public Object visitChoice(KeYParser.ChoiceContext ctx) { } seq().put(category, new HashSet<>(options)); - choiceInformation.setDefaultOption(category, options.get(0)); - options.forEach(it -> choices().add(new Choice(it, category))); + var choices = options.stream().map(it -> new Choice(it, category)).toList(); + choices.forEach(it -> choices().add(it)); + choiceInformation.setDefaultOption(category, choices.getFirst()); return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java index ba9216516f1..590d7096210 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.op.IProgramVariable; +import de.uka.ilkd.key.nparser.ChoiceInformation; import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.BuiltInRuleIndex; import de.uka.ilkd.key.proof.Node; @@ -19,6 +20,7 @@ import de.uka.ilkd.key.proof.mgt.RuleJustificationInfo; import de.uka.ilkd.key.rule.*; import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.ProofSettings; import org.key_project.logic.Choice; @@ -29,7 +31,6 @@ import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleSet; -import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; @@ -51,29 +52,32 @@ public class InitConfig { private RuleJustificationInfo justifInfo = new RuleJustificationInfo(); - + /// List of all known taclets. private ImmutableList taclets = ImmutableSLList.nil(); /** - * maps categories to their default choice (both represented as Strings), which is used if no - * other choice is specified in the problemfile + * Map of categories to their default choice. The choices are overridden in activateChoice + * by settings given in the {@link KeYUserProblemFile} or + * {@link Profile#prepareInitConfig(InitConfig, Configuration)}. */ - private Map category2DefaultChoice = new LinkedHashMap<>(); + private final Map category2DefaultChoice; - /** - * maps taclets to their TacletBuilders. This information is needed when a taclet contains - * GoalTemplates annotated with taclet-options because in this case a new taclet has to be - * created containing only those GoalTemplates whose options are activated and those who don't - * belong to any specific option. - */ - private HashMap> taclet2Builder = new LinkedHashMap<>(); /** * Set of the rule options activated for the current proof. The rule options ({@link Choice}s) * allow to use different ruleset modelling or skipping certain features (e.g. nullpointer * checks when resolving references) */ - private ImmutableSet activatedChoices = DefaultImmutableSet.nil(); + private final Map activatedChoices = new TreeMap<>(); + + + /** + * maps taclets to their TacletBuilders. This information is needed when a taclet contains + * GoalTemplates annotated with taclet-options because in this case a new taclet has to be + * created containing only those GoalTemplates whose options are activated and those who don't + * belong to any specific option. + */ + private Map> taclet2Builder = new LinkedHashMap<>(); /** HashMap for quick lookups taclet name->taclet */ private Map activatedTacletCache = null; @@ -95,21 +99,54 @@ public class InitConfig { public InitConfig(Services services) { this.services = services; - - category2DefaultChoice = new HashMap<>( - ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices()); + category2DefaultChoice = new TreeMap<>(); } + /// combines the found choices in KeY files, together with the current settings. + /// The namespace of choices has to be filled. + public void computeDefaults(ChoiceInformation ci) { + var currentDefaultChoices = + ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); - // ------------------------------------------------------------------------- - // internal methods - // ------------------------------------------------------------------------- + // defined file choices + this.category2DefaultChoice.putAll(ci.getDefaultOptions()); + // then current user settings. + for (final String s : currentDefaultChoices.values()) { + final Choice c = choiceNS().lookup(new Name(s)); + if (c != null) { + category2DefaultChoice.put(c.category(), c); + } + } + if (currentDefaultChoices.isEmpty()) { // no choices have been read. + currentDefaultChoices = new TreeMap<>(); + for (var entry : category2DefaultChoice.entrySet()) { + currentDefaultChoices.put(entry.getKey(), entry.getValue().name().toString()); + } + ProofSettings.DEFAULT_SETTINGS.getChoiceSettings() + .setDefaultChoices(currentDefaultChoices); + } - // ------------------------------------------------------------------------- - // public interface - // ------------------------------------------------------------------------- + // activate by \settings {} in file KeYUserProblemFile + if (settings != null) { + for (var choice : settings.getChoiceSettings().getDefaultChoicesAsSet()) { + activatedChoices.put(choice.category(), choice); + } + + if (!ci.getActivatedChoices().isEmpty()) { + for (var ac : ci.getActivatedChoices()) { + activatedChoices.put(ac.category(), ac); + } + } + + Map defaults = new TreeMap<>(); + for (var ac : getActivatedChoices()) { + defaults.put(ac.category(), ac.name().toString()); + } + settings.getChoiceSettings().setDefaultChoices(defaults); + } + } /** * returns the Services of this initial configuration providing access to the used program model @@ -126,40 +163,31 @@ public Profile getProfile() { } - /** - * Adds a default option for a category. It does override previous default choices. - * - * @return true if the default was successfully set - */ - public boolean addCategoryDefaultChoice(@NonNull String category, @NonNull String choice) { - if (!category2DefaultChoice.containsKey(category)) { - category2DefaultChoice.put(category, choice); - return true; - } - return false; - } - /** * Adds default choices given in {@code init}. Not overriding previous default choices. */ - public void addCategory2DefaultChoices(@NonNull Map init) { - boolean changed = false; - for (final Map.Entry entry : init.entrySet()) { - changed = addCategoryDefaultChoice(entry.getKey(), entry.getValue()) || changed; - } - if (changed) { - // FIXME weigl: I do not understand why the default choices are back progragated! - // For me this is a design flaw. - Map clone = - new HashMap<>(category2DefaultChoice); - ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().setDefaultChoices(clone); - // invalidate active taclet cache - activatedTacletCache = null; + public void addCategory2DefaultChoices(@NonNull Map init) { + if (init.isEmpty()) { + return; } + category2DefaultChoice.putAll(init); + // FIXME weigl: I do not understand why the default choices are back progragated! + // For me this is a design flaw. + // weigl(2026): This is the way, how the settings are getting updated by the current + // known choices. This is not good! + /* + * Map clone = new HashMap<>(); + * for (Map.Entry entry : category2DefaultChoice.entrySet()) { + * clone.put(entry.getKey(), entry.getValue().name().toString()); + * } + * ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().setDefaultChoices(clone); + */ + // invalidate active taclet cache + activatedTacletCache = null; } - public void setTaclet2Builder(HashMap> taclet2Builder) { + public void setTaclet2Builder(Map> taclet2Builder) { this.taclet2Builder = taclet2Builder; } @@ -171,7 +199,7 @@ public void setTaclet2Builder(HashMap> t * * @return the map from a taclet to its builder */ - public HashMap> getTaclet2Builder() { + public Map> getTaclet2Builder() { return taclet2Builder; } @@ -181,37 +209,22 @@ public HashMap> getTaclet2Builder() { * specified choice the default choice contained in category2DefaultChoice is added. */ public void setActivatedChoices(ImmutableSet activatedChoices) { - category2DefaultChoice = - ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); - - HashMap c2DC = new HashMap<>(category2DefaultChoice); - for (final Choice c : activatedChoices) { - c2DC.remove(c.category()); - } - - ImmutableList category2DefaultChoiceList = ImmutableSLList.nil(); - for (final String s : c2DC.values()) { - final Choice c = choiceNS().lookup(new Name(s)); - if (c != null) { - category2DefaultChoiceList = category2DefaultChoiceList.prepend(c); - } + this.activatedChoices.clear(); + for (Choice choice : activatedChoices) { + this.activatedChoices.put(choice.category(), choice); } - this.activatedChoices = activatedChoices - .union( - DefaultImmutableSet.fromImmutableList(category2DefaultChoiceList)); // invalidate active taclet cache activatedTacletCache = null; } - /** - * Returns the choices which are currently active. For getting the active choices for a specific - * proof, getChoices in de.uka.ilkd.key.proof.Proof - * has to be used. + * Returns the effective activated choices. */ public ImmutableSet getActivatedChoices() { - return activatedChoices; + var effectiveMap = new TreeMap<>(category2DefaultChoice); + effectiveMap.putAll(activatedChoices); + return ImmutableSet.from(effectiveMap.values()); } @@ -256,7 +269,8 @@ private void fillActiveTacletCache() { return; } final LinkedHashMap tacletCache = new LinkedHashMap<>(); - var choices = Collections.unmodifiableSet(activatedChoices.toSet()); + var choices = Collections.unmodifiableSet(getActivatedChoices().toSet()); + for (Taclet t : taclets) { TacletBuilder b = taclet2Builder.get(t); @@ -422,16 +436,14 @@ public InitConfig deepCopy() { * returns a copy of this initial configuration copying the namespaces, the contained JavaInfo * while using the immutable set of taclets in the copy */ - @SuppressWarnings("unchecked") public InitConfig copyWithServices(Services services) { InitConfig ic = new InitConfig(services); if (settings != null) { ic.setSettings(new ProofSettings(settings)); } - ic.setActivatedChoices(activatedChoices); - ic.category2DefaultChoice = new HashMap<>(category2DefaultChoice); - ic.setTaclet2Builder( - (HashMap>) taclet2Builder.clone()); + ic.category2DefaultChoice.putAll(category2DefaultChoice); + ic.activatedChoices.putAll(activatedChoices); + ic.setTaclet2Builder(new HashMap<>(taclet2Builder)); ic.taclets = taclets; ic.originalKeYFileName = originalKeYFileName; ic.header = header; @@ -458,11 +470,27 @@ public void setFileRepo(FileRepo fileRepo) { /// Enforce the given choice. Remove choices of the same category from the current set. public void activateChoice(Choice choice) { - setActivatedChoices( - getActivatedChoices() - .stream().filter(it -> choice.category().equals(it.category())) - .collect(ImmutableSet.collector()) - .add(choice)); + activatedChoices.put(choice.category(), choice); + // invalidate active taclet cache + activatedTacletCache = null; + } + + public boolean isChoiceActive(String choice) { + var c = choiceNS().lookup(choice); + return isChoiceActive(c); + } + + public boolean isChoiceActive(@Nullable Choice c) { + if (c == null) { + return false; + } + + if (activatedChoices.containsValue(c)) { + return true; + } + + return !activatedChoices.containsKey(c.category()) + && category2DefaultChoice.containsValue(c); } /// returns the user-given declarations used during loading @@ -474,4 +502,10 @@ public void activateChoice(Choice choice) { public void setHeader(KeyAst.@Nullable Declarations header) { this.header = header; } + + /// Returns true, if the given category was actively set, e.g., by loading settings or a + /// profile. + public boolean isChoiceCategorySet(String category) { + return activatedChoices.containsKey(category); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java index f887bfea417..9a2858de6cc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java @@ -96,8 +96,7 @@ public ImmutableSet read() throws ProofInputException { initConfig.setSettings(settings); ChoiceInformation ci = getParseContext().getChoices(); - settings.getChoiceSettings().updateWith(ci.getActivatedChoices()); - initConfig.setActivatedChoices(settings.getChoiceSettings().getDefaultChoicesAsSet()); + initConfig.computeDefaults(ci); ImmutableSet warnings = DefaultImmutableSet.nil(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index cdd3c8653d4..a7a475b7a40 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java @@ -34,6 +34,7 @@ import de.uka.ilkd.key.rule.RewriteTaclet; import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.speclang.PositionedString; @@ -53,6 +54,7 @@ import org.key_project.util.collection.ImmutableSet; import org.key_project.util.java.StringUtil; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -69,6 +71,7 @@ public final class ProblemInitializer { */ private FileRepo fileRepo; private ImmutableSet warnings = DefaultImmutableSet.nil(); + private @Nullable Configuration additionalProfileOptions; // ------------------------------------------------------------------------- // constructors @@ -82,13 +85,22 @@ public ProblemInitializer(ProgressMonitor mon, Services services, } public ProblemInitializer(Profile profile) { - if (profile == null) { - throw new IllegalArgumentException("Given profile is null"); - } + this(null, new Services(Objects.requireNonNull(profile, "Given profile is null")), null); + } - this.progMon = null; - this.listener = null; - this.services = new Services(Objects.requireNonNull(profile)); + public ProblemInitializer(Profile profile, @Nullable Configuration additionalProfileOptions) { + this(profile); + this.additionalProfileOptions = additionalProfileOptions; + } + + /// An arbitrary object which is passed to the provided profile, during construction of the + /// `initConfig`. + public @Nullable Configuration getAdditionalProfileOptions() { + return additionalProfileOptions; + } + + public void setAdditionalProfileOptions(@Nullable Configuration additionalProfileOptions) { + this.additionalProfileOptions = additionalProfileOptions; } private void progressStarted(Object sender) { @@ -443,7 +455,7 @@ private InitConfig createInitConfigFor(EnvInput envInput) throws ProofInputExcep for (RuleSource tacletBase : tacletBases) { KeYFile tacletBaseFile = new KeYFile( "taclet base (%s)".formatted(tacletBase.file().getFileName()), - tacletBase, progMon, profile); + tacletBase, progMon, profile, null); readEnvInput(tacletBaseFile, config); } } @@ -454,7 +466,6 @@ private InitConfig createInitConfigFor(EnvInput envInput) throws ProofInputExcep // cache the last used init config BaseConfigCache.setBaseInputConfig(config, inputDigest); config = config.copy(); - profile.prepareInitConfig(config); return config; } @@ -476,9 +487,19 @@ public InitConfig prepare(EnvInput envInput) throws ProofInputException { ic.setHeader(uf.getProblemHeader()); } + // applied after envInput/KeYUserProblemFile was read, and its setting are active. + var warnings = ic.getProfile() + .prepareInitConfig(ic, additionalProfileOptions); + addWarnings(warnings); + return ic; } + private void addWarnings(List warnings) { + this.warnings = + this.warnings.add(warnings.stream().map(PositionedString::new).toList()); + } + private void print(Proof firstProof) { File taclets1; try { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java index 9316c659d0e..7f19e4b2b93 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java @@ -3,6 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.init; +import java.util.Collections; +import java.util.List; + import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.label.TermLabelManager; import de.uka.ilkd.key.proof.Proof; @@ -12,6 +15,7 @@ import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.UseDependencyContractRule; import de.uka.ilkd.key.rule.UseOperationContractRule; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.strategy.StrategyFactory; import org.key_project.logic.Name; @@ -22,6 +26,7 @@ import org.key_project.util.collection.ImmutableSet; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** *

@@ -180,8 +185,14 @@ default UseOperationContractRule getUseOperationContractRule() { /// Taclet base has been loaded, but before Java sources are loaded or the environment is /// established. /// + /// @param baseConfig a initial configuration which can be modified, e.g., forcing Taclet + /// options. + /// @param additionalProfileOptions a nullable object representing selected options in the UI or + /// command line. + /// @return warnings as a list of Strings /// @see ProblemInitializer - default void prepareInitConfig(InitConfig baseConfig) { - + default List prepareInitConfig(InitConfig baseConfig, + @Nullable Configuration additionalProfileOptions) { + return Collections.emptyList(); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java index 851cfa8320b..3d187807b82 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java @@ -64,6 +64,7 @@ public abstract class AbstractProblemLoader { * @see EnvInput#isIgnoreOtherJavaFiles() */ private boolean loadSingleJavaFile = false; + private @Nullable Configuration additionalProfileOptions; public static class ReplayResult { @@ -552,6 +553,7 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException { protected ProblemInitializer createProblemInitializer(FileRepo fileRepo) { Profile profile = forceNewProfileOfNewProofs ? profileOfNewProofs : envInput.getProfile(); ProblemInitializer pi = new ProblemInitializer(control, new Services(profile), control); + pi.setAdditionalProfileOptions(additionalProfileOptions); pi.setFileRepo(fileRepo); return pi; } @@ -859,4 +861,15 @@ public void setLoadSingleJavaFile(boolean loadSingleJavaFile) { public void setIgnoreWarnings(boolean ignoreWarnings) { this.ignoreWarnings = ignoreWarnings; } + + public void setAdditionalProfileOptions(@Nullable Configuration additionalProfileOptions) { + this.additionalProfileOptions = additionalProfileOptions; + } + + /// An arbitrary object representing additional options for the given profile. + /// @see ProblemInitializer + public Configuration getAdditionalProfileOptions() { + return additionalProfileOptions; + } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java index a4d2140f815..a974393b694 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java @@ -179,10 +179,11 @@ protected KeyAst.File getParseContext() { protected ProofSettings getPreferences() { if (initConfig.getSettings() == null) { - return readPreferences(); - } else { - return initConfig.getSettings(); + var settings = readPreferences(); + initConfig.setSettings(settings); + return settings; } + return initConfig.getSettings(); } public ProofSettings readPreferences() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java index 7cd84fdcc85..17a63bd454c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java @@ -31,12 +31,11 @@ public class ChoiceSettings extends AbstractSettings { * maps categories to a set of Strings(representing the choices which are options for this * category). */ - private Map> category2Choices = new LinkedHashMap<>(); - private Map category2Default; + private Map> category2Choices = new TreeMap<>(); + private Map category2Default = new TreeMap<>(); public ChoiceSettings() { - category2Default = new LinkedHashMap<>(); } @@ -84,9 +83,14 @@ private static ImmutableSet choiceMap2choiceSet(Map ccc) return DefaultImmutableSet.fromImmutableList(choices); } - private void setChoiceCategories(HashMap> c2C) { + + public Map> getCategory2Choices() { + return category2Choices; + } + + public void setChoiceCategories(Map> c2C) { var old = category2Choices; - this.category2Choices = new HashMap<>(c2C); + this.category2Choices = new TreeMap<>(c2C); firePropertyChange(PROP_CHOICE_CATEGORIES, old, category2Choices); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 31acea8acba..11bf0d4c1b6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -88,7 +88,8 @@ public boolean exists(String name) { * @see #getTable(String) */ public boolean exists(String name, Class clazz) { - return data.containsKey(name) && clazz.isAssignableFrom(data.get(name).getClass()); + return data.containsKey(name) && data.get(name) != null + && clazz.isAssignableFrom(data.get(name).getClass()); } /** @@ -184,7 +185,7 @@ public long getLong(String name, long defaultValue) { * @throws NullPointerException if no such value entry exists */ public boolean getBool(String name) { - return get(name, Boolean.class); + return Boolean.TRUE.equals(get(name, Boolean.class)); } /** @@ -215,8 +216,7 @@ public double getDouble(String name) { * @param name property name * @throws ClassCastException if the entry is not a {@link String} */ - @Nullable - public String getString(String name) { + public @Nullable String getString(String name) { return get(name, String.class); } @@ -358,7 +358,7 @@ private ConfigurationMeta getOrCreateMeta(String name) { /** * @see #getTable(String) */ - public Configuration getSection(String name) { + public @Nullable Configuration getSection(String name) { return getTable(name); } @@ -373,39 +373,39 @@ public Configuration getSection(String name, boolean createIfNotExists) { return getSection(name); } - public Object set(String name, Object obj) { + public @Nullable Object set(String name, @Nullable Object obj) { return data.put(name, obj); } - public Object set(String name, Boolean obj) { + public @Nullable Object set(String name, @Nullable Boolean obj) { return set(name, (Object) obj); } - public Object set(String name, String obj) { + public @Nullable Object set(String name, @Nullable String obj) { return set(name, (Object) obj); } - public Object set(String name, Long obj) { + public @Nullable Object set(String name, @Nullable Long obj) { return set(name, (Object) obj); } - public Object set(String name, int obj) { + public @Nullable Object set(String name, int obj) { return set(name, (long) obj); } - public Object set(String name, Double obj) { + public @Nullable Object set(String name, @Nullable Double obj) { return set(name, (Object) obj); } - public Object set(String name, Configuration obj) { + public @Nullable Object set(String name, @Nullable Configuration obj) { return set(name, (Object) obj); } - public Object set(String name, List obj) { + public @Nullable Object set(String name, @Nullable List obj) { return set(name, (Object) obj); } - public Object set(String name, String[] seq) { + public @Nullable Object set(String name, @Nullable String[] seq) { return set(name, (Object) Arrays.asList(seq)); } @@ -544,7 +544,7 @@ public ConfigurationWriter printValue(Object value) { } else if (value instanceof Enum) { printValue(value.toString()); } else if (value == null) { - printValue("null"); + out.write("null"); } else { throw new IllegalArgumentException("Unexpected object: " + value); } @@ -552,7 +552,7 @@ public ConfigurationWriter printValue(Object value) { } private ConfigurationWriter printMap(Map value) { - out.format("{ "); + out.format("{"); indent += 4; newline().printIndent(); for (Iterator> iterator = @@ -579,7 +579,7 @@ private ConfigurationWriter print(String s) { } private ConfigurationWriter printSeq(Collection value) { - out.format("[ "); + out.print("["); indent += 4; newline(); printIndent(); @@ -598,13 +598,13 @@ private ConfigurationWriter printSeq(Collection value) { } indent -= 4; newline().printIndent(); - out.format("]"); + out.print("]"); return this; } private ConfigurationWriter printKey(String key) { printValue(key); - out.format(" : "); + out.print(" : "); return this; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java b/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java index 040aa15ba23..ceb01d28406 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java @@ -82,7 +82,7 @@ public static Path getKeyConfigDir() { public static void setKeyConfigDir(String keyConfigDir) { PathConfig.keyConfigDir = Paths.get(keyConfigDir); - recentFileStorage = getKeyConfigDir().resolve("recentFiles.json"); + recentFileStorage = getKeyConfigDir().resolve("recentFiles_v2.json"); proofIndependentSettings = getKeyConfigDir().resolve("proofIndependentSettings.props"); logDirectory = getKeyConfigDir().resolve("logs"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java index 0618c9668f2..ac7cb117a9a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java @@ -6,7 +6,7 @@ import java.io.File; import java.nio.file.Path; import java.util.Collection; -import java.util.HashMap; +import java.util.Map; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.proof.Proof; @@ -83,7 +83,7 @@ public void manageAvailableTaclets(InitConfig initConfig, Taclet tacletToProve) ImmutableList sysTaclets = initConfig.getTaclets(); ImmutableList newTaclets = ImmutableSLList.nil(); - HashMap> map = initConfig.getTaclet2Builder(); + Map> map = initConfig.getTaclet2Builder(); boolean tacletfound = false; for (Taclet taclet : sysTaclets) { if (taclet.equals(tacletToProve)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/SideProofUtil.java b/key.core/src/main/java/de/uka/ilkd/key/util/SideProofUtil.java index 75c1cda207b..4e95bb83890 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/SideProofUtil.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/SideProofUtil.java @@ -16,7 +16,6 @@ import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.OneStepSimplifier; import de.uka.ilkd.key.rule.Taclet; -import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder; import de.uka.ilkd.key.settings.ProofSettings; import org.key_project.logic.Choice; @@ -64,8 +63,7 @@ public static ProofEnvironment cloneProofEnvironmentWithOwnOneStepSimplifier( : null; initConfig.setSettings(clonedSettings); initConfig.setTaclet2Builder( - (HashMap>) sourceInitConfig.getTaclet2Builder() - .clone()); + new HashMap<>(sourceInitConfig.getTaclet2Builder())); initConfig.setTaclets(sourceInitConfig.getTaclets()); // Create new ProofEnvironment and initialize it with values from initial one. ProofEnvironment env = new ProofEnvironment(initConfig); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index 19491d1632d..7e34b84399c 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -366,7 +366,6 @@ public static ProofCollection automaticJavaDL() throws IOException { "heap/BoyerMoore/BM(BM__monoLemma((I,int,int)).JML normal_behavior operation contract.0.proof"); g = c.group("quicksort"); - g.setLocalSettings("[Choice]DefaultChoices=moreSeqRules-moreSeqRules:on"); g.setDirectory("heap/quicksort"); g.provable("toplevel.key"); g.provable("sort.key"); diff --git a/key.ui/examples/heap/quicksort/toplevel.key b/key.ui/examples/heap/quicksort/toplevel.key index 1043d0a42d0..10b721cebec 100644 --- a/key.ui/examples/heap/quicksort/toplevel.key +++ b/key.ui/examples/heap/quicksort/toplevel.key @@ -1,3 +1,7 @@ +\settings { + "[Choice]DefaultChoices=moreSeqRules-moreSeqRules:on" +} + \javaSource "."; \chooseContract "Quicksort[Quicksort::sort([I)].JML normal_behavior operation contract.0"; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserLoadingOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserLoadingOptions.java index c6e35409d7e..b669d84f145 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserLoadingOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserLoadingOptions.java @@ -3,22 +3,28 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui; -import java.util.Arrays; -import java.util.Objects; +import java.util.ArrayList; +import java.util.Map; import java.util.ServiceLoader; import javax.swing.*; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade; import de.uka.ilkd.key.gui.settings.SettingsPanel; -import de.uka.ilkd.key.proof.init.AbstractProfile; import de.uka.ilkd.key.proof.init.DefaultProfileResolver; import de.uka.ilkd.key.proof.init.Profile; +import de.uka.ilkd.key.settings.Configuration; import net.miginfocom.layout.AC; import net.miginfocom.layout.CC; import net.miginfocom.layout.LC; import net.miginfocom.swing.MigLayout; import org.checkerframework.checker.nullness.qual.Nullable; +import org.jspecify.annotations.NonNull; +/// Panel for loading options to be used in {@link KeYFileChooser} +/// @see KeYFileChooser#addLoadingOptions() +/// @author weigl public class KeYFileChooserLoadingOptions extends JPanel { private final JLabel lblProfile = new JLabel("Profile:"); private final JComboBox cboProfile = new JComboBox<>(); @@ -39,6 +45,11 @@ public class KeYFileChooserLoadingOptions extends JPanel { Mark this checkbox to only load the selected Java file. """); + private final Map additionalOptionPanels = + KeYGuiExtensionFacade.createAdditionalOptionPanels(); + + + private KeYGuiExtension.@Nullable OptionPanel currentOptionPanel = null; public KeYFileChooserLoadingOptions(KeYFileChooser chooser) { setLayout(new MigLayout(new LC().fillX().wrapAfter(3).maxWidth("400"), @@ -48,16 +59,23 @@ public KeYFileChooserLoadingOptions(KeYFileChooser chooser) { lblProfileInfo.setWrapStyleWord(true); lblProfileInfo.setLineWrap(true); - var items = ServiceLoader.load(DefaultProfileResolver.class) - .stream().map(it -> it.get().getDefaultProfile()) - .map(ProfileWrapper::new) - .toArray(ProfileWrapper[]::new); + var profiles = + new ArrayList<>(ServiceLoader.load(DefaultProfileResolver.class) + .stream().map(it -> it.get().getDefaultProfile()) + .map(ProfileWrapper::new) + .toList()); + + final var legacyMode = new ProfileWrapper("Respect profile given in file", "", + "Usable on KeY file which defines \\profile inside the file. " + + "If no KeY file is loaded, falls back to legacy behavior", + null); + + profiles.addFirst(legacyMode); + + var items = profiles.toArray(ProfileWrapper[]::new); + cboProfile.setModel(new DefaultComboBoxModel<>(items)); - cboProfile.setSelectedItem( - Arrays.stream(items) - .filter(it -> it.profile.equals(AbstractProfile.getDefaultProfile())) - .findFirst() - .orElse(null)); + cboProfile.setSelectedItem(legacyMode); cboProfile.addItemListener(evt -> updateProfileInfo()); updateProfileInfo(); @@ -78,34 +96,56 @@ private void updateProfileInfo() { } private void updateProfileInfo(@Nullable ProfileWrapper selectedItem) { + if (currentOptionPanel != null) { + currentOptionPanel.deinstall(this); + } + if (selectedItem == null) { lblProfileInfo.setText(""); } else { - lblProfileInfo.setText(selectedItem.profile.description()); + lblProfileInfo.setText(selectedItem.description()); + if (additionalOptionPanels.containsKey(selectedItem.profile)) { + currentOptionPanel = additionalOptionPanels.get(selectedItem.profile); + currentOptionPanel.install(this); + } } } public @Nullable Profile getSelectedProfile() { - var selected = getSelectedProfileName(); - var items = ServiceLoader.load(DefaultProfileResolver.class) - .stream().filter(it -> Objects.equals(selected, it.get().getProfileName())) - .findFirst(); - return items.map(it -> it.get().getDefaultProfile()) - .orElse(null); + var selected = (ProfileWrapper) cboProfile.getSelectedItem(); + if (selected == null) { + return null; + } + return selected.profile(); + } + + public @Nullable Configuration getAdditionalProfileOptions() { + if (currentOptionPanel == null) { + return null; + } + return currentOptionPanel.getResult(); } public @Nullable String getSelectedProfileName() { - return ((ProfileWrapper) cboProfile.getSelectedItem()).profile().ident(); + final var selectedItem = (ProfileWrapper) cboProfile.getSelectedItem(); + if (selectedItem == null) + return null; + return selectedItem.ident(); } public boolean isOnlyLoadSingleJavaFile() { return lblSingleJava.isSelected(); } - record ProfileWrapper(Profile profile) { + record ProfileWrapper(String name, String ident, String description, + @Nullable Profile profile) { + ProfileWrapper(Profile profile) { + this(profile.displayName(), profile.ident(), profile.description(), profile); + } + @Override - public String toString() { - return profile.displayName(); + public @NonNull String toString() { + return name; } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 77bc4ab4aff..140604cd34f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -56,11 +56,9 @@ import de.uka.ilkd.key.gui.sourceview.SourceViewFrame; import de.uka.ilkd.key.gui.utilities.LruCached; import de.uka.ilkd.key.proof.*; +import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.proof.io.ProblemLoader; -import de.uka.ilkd.key.settings.FeatureSettings; -import de.uka.ilkd.key.settings.GeneralSettings; -import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.ViewSettings; +import de.uka.ilkd.key.settings.*; import de.uka.ilkd.key.smt.SolverTypeCollection; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl; @@ -81,6 +79,7 @@ import com.formdev.flatlaf.FlatLightLaf; import com.formdev.flatlaf.util.SystemInfo; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -323,7 +322,7 @@ private MainWindow() { proofListView = new JScrollPane(proofList); notificationManager = new NotificationManager(mediator, this); - recentFileMenu = new RecentFileMenu(mediator); + recentFileMenu = new RecentFileMenu(this); proofTreeView = new ProofTreeView(mediator); infoView = new InfoView(this, mediator); @@ -1388,10 +1387,13 @@ public NotificationManager getNotificationManager() { /** * A file to the menu of recent opened files. * - * @see RecentFileMenu#addRecentFile(String) + * @see RecentFileMenu#addRecentFile(String, Profile, boolean, Configuration) */ - public void addRecentFile(@NonNull String absolutePath) { - recentFileMenu.addRecentFile(absolutePath); + public void addRecentFile(@NonNull String absolutePath, + @Nullable Profile profile, + boolean singleJava, + @Nullable Configuration additionalOption) { + recentFileMenu.addRecentFile(absolutePath, profile, singleJava, additionalOption); } public void openExamples() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java index 61af8cacd0c..1ca36912123 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java @@ -3,19 +3,19 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui; -import java.awt.event.ActionListener; +import java.awt.event.ActionEvent; import java.io.*; import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; -import java.util.HashMap; -import java.util.LinkedHashMap; -import java.util.Map; -import java.util.stream.Collectors; +import java.util.*; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.nparser.ParsingFacade; +import de.uka.ilkd.key.proof.init.DefaultProfileResolver; +import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.PathConfig; @@ -23,6 +23,8 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import static de.uka.ilkd.key.gui.actions.QuickSaveAction.QUICK_SAVE_PATH; + /** * This class offers a mechanism to manage recent files; it adds the necessary menu items to a menu * or even can provide that menu itself. also it offers a way to read the recent files from a @@ -40,6 +42,8 @@ public class RecentFileMenu { */ private static final int MAX_RECENT_FILES = 8; + private final MainWindow mainWindow; + /** * this is the maximal number of recent files. */ @@ -50,19 +54,10 @@ public class RecentFileMenu { */ private final JMenu menu; - /** - * the actionListener to be notified of mouse-clicks or other actionevents on the menu items - */ - private final ActionListener lissy; - - /** - * recent files, unique by path - */ - private final Map pathToRecentFile = new LinkedHashMap<>(); /** * Mapping from menu item to entry */ - private final HashMap menuItemToRecentFile; + private final List recentFiles = new ArrayList<>(); private RecentFileEntry mostRecentFile; @@ -71,97 +66,77 @@ public class RecentFileMenu { * * @param mediator Key mediator */ - public RecentFileMenu(final KeYMediator mediator) { + public RecentFileMenu(final MainWindow mediator) { + this.mainWindow = mediator; this.menu = new JMenu("Recent Files"); - this.lissy = e -> { - String absPath = getAbsolutePath((JMenuItem) e.getSource()); - Path file = Paths.get(absPath); - - // special case proof bundles -> allow to select the proof to load - if (ProofSelectionDialog.isProofBundle(file)) { - Path proofPath = ProofSelectionDialog.chooseProofToLoad(file); - if (proofPath == null) { - // canceled by user! - } else { - mediator.getUI().loadProofFromBundle(file, proofPath); - } - } else { - mediator.getUI().loadProblem(file); - } - }; this.maxNumberOfEntries = MAX_RECENT_FILES; - this.menuItemToRecentFile = new LinkedHashMap<>(); - - menu.setEnabled(menu.getItemCount() != 0); + // menu.setEnabled(menu.getItemCount() != 0); menu.setIcon(IconFactory.recentFiles(16)); loadFrom(PathConfig.getRecentFileStorage()); } private void insertFirstEntry(RecentFileEntry entry) { - menu.insert(entry.getMenuItem(), 0); + menu.insert(entry.createMenuItem(), 0); mostRecentFile = entry; + recentFiles.addFirst(entry); } /** * add path to the menu */ - private void addNewToModelAndView(final String path) { + private void addNewToModelAndView(final String path, + @Nullable Profile profile, + boolean singleJava, @Nullable Configuration additionalOption) { // do not add quick save location to recent files - if (de.uka.ilkd.key.gui.actions.QuickSaveAction.QUICK_SAVE_PATH.endsWith(path)) { + if (QUICK_SAVE_PATH.endsWith(path)) { return; } if (new File(path).exists()) { - final RecentFileEntry entry = new RecentFileEntry(path); - pathToRecentFile.put(entry.getAbsolutePath(), entry); + var entry = new RecentFileEntry(path, profile != null ? profile.ident() : null, + singleJava, additionalOption); + insertFirstEntry(entry); // Recalculate unique names - final String[] paths = pathToRecentFile.keySet().toArray(String[]::new); + final String[] paths = + recentFiles.stream().map(RecentFileEntry::getAbsolutePath).toArray(String[]::new); final ShortUniqueFileNames.Name[] names = ShortUniqueFileNames.makeUniqueNames(paths); + // Set the names - for (ShortUniqueFileNames.Name name : names) { - pathToRecentFile.get(name.getPath()).setName(name.getName()); + for (int i = 0; i < names.length; i++) { + var text = names[i].toString(); + recentFiles.get(i).createMenuItem().getAction().putValue(Action.NAME, text); } - - // Insert the menu item - final JMenuItem item = entry.getMenuItem(); - menuItemToRecentFile.put(item, entry); - item.addActionListener(lissy); - - insertFirstEntry(entry); } } - /** - * - */ - private String getAbsolutePath(JMenuItem item) { - return menuItemToRecentFile.get(item).getAbsolutePath(); - } - - private void addRecentFileNoSave(final String path) { + private void addRecentFileNoSave(final String path, + @Nullable Profile profile, + boolean singleJava, + @Nullable Configuration additionalOption) { LOGGER.trace("Adding file: {}", path); - final RecentFileEntry existingEntry = pathToRecentFile.get(path); + + Optional existingEntry = recentFiles.stream() + .filter(it -> path.equals(it.getAbsolutePath())).findFirst(); // Add the path to the recentFileList: // check whether this path is already there - if (existingEntry != null) { - menu.remove(existingEntry.getMenuItem()); - insertFirstEntry(existingEntry); + if (existingEntry.isPresent()) { + var entry = existingEntry.get(); + recentFiles.remove(entry); + menu.remove(entry.createMenuItem()); + insertFirstEntry(entry); return; } // if appropriate, remove the last entry. if (menu.getItemCount() == maxNumberOfEntries) { - final JMenuItem item = menu.getItem(menu.getItemCount() - 1); - final RecentFileEntry entry = menuItemToRecentFile.get(item); - menuItemToRecentFile.remove(entry.getMenuItem()); - pathToRecentFile.remove(entry.getAbsolutePath()); - menu.remove(entry.getMenuItem()); + var lastEntry = recentFiles.removeLast(); + menu.remove(lastEntry.createMenuItem()); } - addNewToModelAndView(path); + addNewToModelAndView(path, profile, singleJava, additionalOption); menu.setEnabled(menu.getItemCount() != 0); } @@ -172,9 +147,12 @@ private void addRecentFileNoSave(final String path) { * the end. (set the maximum number with the {@link #setMaxNumberOfEntries(int i)} method). * * @param path the path of the file. + * @param singleJava */ - public void addRecentFile(final String path) { - addRecentFileNoSave(path); + public void addRecentFile(final String path, + @Nullable Profile profile, boolean singleJava, + @Nullable Configuration additionalOption) { + addRecentFileNoSave(path, profile, singleJava, additionalOption); save(); } @@ -204,14 +182,23 @@ public JMenu getMenu() { */ public final void loadFrom(Path filename) { try { - var c = Configuration.load(filename); - c.getStringList("recentFiles").forEach(this::addRecentFileNoSave); + var file = ParsingFacade.parseConfigurationFile(filename); + List recent = file.asConfigurationList(); + this.recentFiles.clear(); + for (var c : recent) { + final var e = new RecentFileEntry(c); + if (mostRecentFile != null) { + mostRecentFile = e; + } + recentFiles.add(e); + menu.add(e.createMenuItem()); + } } catch (FileNotFoundException ex) { - LOGGER.debug("Could not read RecentFileList. Did not find file {}", filename); + LOGGER.info("Could not read RecentFileList. Did not find file {}", filename); } catch (IOException ioe) { - LOGGER.debug("Could not read RecentFileList. Some IO Error occured ", ioe); - } catch (Throwable t) { - LOGGER.debug("Could not read RecentFileList. Some Error occured ", t); + LOGGER.error("Could not read RecentFileList. Some IO Error occured ", ioe); + } catch (Exception ioe) { + LOGGER.error("Could not read RecentFileList.", ioe); } } @@ -228,14 +215,11 @@ public String getMostRecent() { * exists) and then re-written so no information will be lost. */ public void store(Path filename) { - Configuration c = new Configuration(); - var seq = menuItemToRecentFile.values().stream() - .map(RecentFileEntry::getAbsolutePath) - .collect(Collectors.toList()); - c.set("recentFiles", seq); - + List config = + recentFiles.stream().map(RecentFileEntry::asConfiguration).toList(); try (var fin = Files.newBufferedWriter(filename)) { - c.save(fin, ""); + var writer = new Configuration.ConfigurationWriter(fin); + writer.printValue(config); } catch (IOException ex) { LOGGER.info("Could not write recent files list ", ex); } @@ -245,37 +229,107 @@ public void save() { store(PathConfig.getRecentFileStorage()); } - private static class RecentFileEntry { - /** - * full path - */ - private final String absolutePath; - /** - * the associated menu item - */ - private final JMenuItem menuItem; - - public RecentFileEntry(String absolutePath) { - this.menuItem = new JMenuItem(); - this.menuItem.setToolTipText(absolutePath); - this.absolutePath = absolutePath; + public class RecentFileEntry { + public static final String KEY_PATH = "path"; + public static final String KEY_PROFILE = "profile"; + public static final String KEY_OPTIONS = "options"; + private static final String KEY_LOAD_SINGLE_JAVA = "singleJava"; + + private @Nullable JMenuItem menuItem; + + private final String path; + private final @Nullable String profile; + private final boolean singleJava; + private final @Nullable Configuration additionalOption; + + public RecentFileEntry( + String path, + @Nullable String profile, + boolean singleJava, + @Nullable Configuration additionalOption) { + this.additionalOption = additionalOption; + this.path = path; + this.profile = profile; + this.singleJava = singleJava; } - public String getAbsolutePath() { - return absolutePath; + public RecentFileEntry(Configuration options) { + this(Objects.requireNonNull(options.getString(KEY_PATH)), + options.getString(KEY_PROFILE), + options.getBool(KEY_LOAD_SINGLE_JAVA, false), + options.getTable(KEY_OPTIONS)); } - public void setName(String name) { - this.menuItem.setText(name); + public Configuration asConfiguration() { + Configuration config = new Configuration(); + config.set(KEY_PATH, path); + config.set(KEY_PROFILE, (Object) profile); + config.set(KEY_LOAD_SINGLE_JAVA, singleJava); + config.set(KEY_OPTIONS, additionalOption); + return config; } - public JMenuItem getMenuItem() { + public String getAbsolutePath() { + return path; + } + + public JMenuItem createMenuItem() { + if (menuItem == null) { + menuItem = new JMenuItem(new RecentFileAction(this)); + } return menuItem; } + } + + private class RecentFileAction extends KeyAction { + private final RecentFileEntry fileEntry; + + public RecentFileAction(RecentFileEntry fileEntry) { + this.fileEntry = fileEntry; + setName(fileEntry.getAbsolutePath()); + setTooltip(fileEntry.getAbsolutePath()); + } @Override - public String toString() { - return absolutePath; + public void actionPerformed(ActionEvent actionEvent) { + String absPath = fileEntry.getAbsolutePath(); + Path file = Paths.get(absPath); + + // special case proof bundles -> allow to select the proof to load + if (ProofSelectionDialog.isProofBundle(file)) { + Path proofPath = ProofSelectionDialog.chooseProofToLoad(file); + if (proofPath == null) { + // canceled by user! + } else { + mainWindow.loadProofFromBundle(file, proofPath); + } + } else { + String profileName = fileEntry.profile; + var selectedProfile = + ServiceLoader.load(DefaultProfileResolver.class) + .stream() + .filter(it -> it.get().getProfileName().equals(profileName)) + .findFirst() + .map(it -> it.get().getDefaultProfile()); + + + if (profileName != null && selectedProfile.isEmpty()) { + JOptionPane.showMessageDialog(mainWindow, + "Could not find previous selected profile %s.".formatted(profileName)); + return; + } + + var profile = selectedProfile.orElse(null); + var additionalProfileOptions = fileEntry.additionalOption; + + mainWindow.loadProblem(file, pl -> { + if (profile != null) { + pl.setProfileOfNewProofs(profile); + pl.setAdditionalProfileOptions(additionalProfileOptions); + } + pl.setLoadSingleJavaFile(fileEntry.singleJava); + }); + } } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index 3b530ba32c0..ab44f1001cf 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -97,9 +97,12 @@ public boolean isAutoModeSupported(Proof proof) { public void loadProblem(Path file, Consumer configure) { - mainWindow.addRecentFile(file.toAbsolutePath().toString()); ProblemLoader problemLoader = getProblemLoader(file, null, null, null, getMediator()); configure.accept(problemLoader); + mainWindow.addRecentFile(file.toAbsolutePath().toString(), + problemLoader.getProfileOfNewProofs(), + problemLoader.isLoadSingleJavaFile(), + problemLoader.getAdditionalProfileOptions()); problemLoader.runAsynchronously(); } @@ -112,16 +115,14 @@ public void loadProblem(Path file, Consumer configure) { */ public void loadProblem(Path file, @Nullable List classPath, @Nullable Path bootClassPath, @Nullable List includes) { - mainWindow.addRecentFile(file.toAbsolutePath().toString()); + mainWindow.addRecentFile(file.toAbsolutePath().toString(), null, false, null); ProblemLoader problemLoader = getProblemLoader(file, classPath, bootClassPath, includes, getMediator()); problemLoader.runAsynchronously(); } public void loadProblem(Path file, Profile profile) { - loadProblem(file, (pl) -> { - pl.setProfileOfNewProofs(profile); - }); + loadProblem(file, (pl) -> pl.setProfileOfNewProofs(profile)); } @Override @@ -131,7 +132,7 @@ public void loadProblem(Path file) { @Override public void loadProofFromBundle(Path proofBundle, Path proofFilename) { - mainWindow.addRecentFile(proofBundle.toAbsolutePath().toString()); + mainWindow.addRecentFile(proofBundle.toAbsolutePath().toString(), null, false, null); ProblemLoader problemLoader = getProblemLoader(proofBundle, null, null, null, getMediator()); problemLoader.setProofPath(proofFilename); @@ -369,7 +370,8 @@ public AbstractProblemLoader load(Profile profile, Path file, List classPa boolean forceNewProfileOfNewProofs, Consumer callback) throws ProblemLoaderException { if (file != null) { - mainWindow.getRecentFiles().addRecentFile(file.toAbsolutePath().toString()); + mainWindow.getRecentFiles().addRecentFile(file.toAbsolutePath().toString(), profile, + false, null); } try { getMediator().stopInterface(true); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java index c0682f40938..aa2393717b2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java @@ -10,6 +10,7 @@ import de.uka.ilkd.key.core.Main; import de.uka.ilkd.key.gui.KeYFileChooser; +import de.uka.ilkd.key.gui.KeYFileChooserLoadingOptions; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.ProofSelectionDialog; import de.uka.ilkd.key.gui.fonticons.IconFactory; @@ -29,7 +30,7 @@ public OpenFileAction(MainWindow mainWindow) { public void actionPerformed(ActionEvent e) { KeYFileChooser fc = new KeYFileChooser(lastSelectedPath); fc.setDialogTitle("Select file to load proof or problem"); - var options = fc.addLoadingOptions(); + KeYFileChooserLoadingOptions options = fc.addLoadingOptions(); fc.addBookmarkPanel(); fc.prepare(); fc.setFileFilter(KeYFileChooser.DEFAULT_FILTER); @@ -64,9 +65,11 @@ public void actionPerformed(ActionEvent e) { } var selectedProfile = options.getSelectedProfile(); + var additionalProfileOptions = options.getAdditionalProfileOptions(); mainWindow.loadProblem(file, pl -> { if (selectedProfile != null) { pl.setProfileOfNewProofs(selectedProfile); + pl.setAdditionalProfileOptions(additionalProfileOptions); } pl.setLoadSingleJavaFile(options.isOnlyLoadSingleJavaFile()); }); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java index c97ab4b2aed..4206b2da39f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java @@ -39,7 +39,8 @@ public void actionPerformed(ActionEvent e) { if (result == JFileChooser.APPROVE_OPTION) { Path file = fc.getSelectedFile().toPath(); - mainWindow.addRecentFile(file.toAbsolutePath().toString()); + mainWindow.addRecentFile(file.toAbsolutePath().toString(), + null, true, null); WindowUserInterfaceControl ui = mainWindow.getUserInterface(); ProblemLoader pl = ui.getProblemLoader(file, Collections.emptyList(), null, diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java index b84924b1591..2ac0d426f44 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java @@ -7,24 +7,25 @@ import java.lang.annotation.RetentionPolicy; import java.util.Collection; import java.util.List; +import java.util.function.Supplier; import javax.swing.Action; import javax.swing.JComponent; import javax.swing.JMenu; import javax.swing.JToolBar; import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.gui.GoalList; -import de.uka.ilkd.key.gui.InfoView; -import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.StrategySelectionView; +import de.uka.ilkd.key.gui.*; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; import de.uka.ilkd.key.gui.nodeviews.SequentView; import de.uka.ilkd.key.gui.prooftree.ProofTreeView; import de.uka.ilkd.key.gui.settings.SettingsProvider; import de.uka.ilkd.key.gui.sourceview.SourceView; import de.uka.ilkd.key.pp.PosInSequent; +import de.uka.ilkd.key.proof.init.Profile; +import de.uka.ilkd.key.settings.Configuration; -import org.jspecify.annotations.NonNull; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.jspecify.annotations.NullMarked; /** * A marker interface for extension of the KeY GUI. Every extension should implement this interface @@ -38,6 +39,7 @@ * @author Alexander Weigl * @version 1 (07.04.19) */ +@NullMarked public interface KeYGuiExtension { @Retention(RetentionPolicy.RUNTIME) @interface Info { @@ -73,8 +75,6 @@ public interface KeYGuiExtension { /** * Loading priority of this extension. Baseline is zero - * - * @return */ int priority() default 0; @@ -102,8 +102,7 @@ interface MainMenu { * @return non-null, emptiable list of actions. * @see de.uka.ilkd.key.gui.actions.KeyAction */ - @NonNull - List getMainMenuActions(@NonNull MainWindow mainWindow); + List getMainMenuActions(MainWindow mainWindow); } /** @@ -139,8 +138,7 @@ interface LeftPanel { * @param window parent of this extension * @param mediator the current mediator */ - @NonNull - Collection getPanels(@NonNull MainWindow window, @NonNull KeYMediator mediator); + Collection getPanels(MainWindow window, KeYMediator mediator); } /** @@ -163,10 +161,9 @@ interface ContextMenu { * @return non-null, emptiable list of actions. * @see de.uka.ilkd.key.gui.actions.KeyAction */ - @NonNull - List getContextActions(@NonNull KeYMediator mediator, - @NonNull ContextMenuKind kind, - @NonNull T underlyingObject); + List getContextActions(KeYMediator mediator, + ContextMenuKind kind, + T underlyingObject); } /** @@ -181,7 +178,6 @@ interface Toolbar { * @param mainWindow the parent of the toolbar * @return non-null */ - @NonNull JToolBar getToolbar(MainWindow mainWindow); } @@ -244,9 +240,6 @@ interface KeyboardShortcuts { String SOURCE_VIEW = SourceView.class.getName(); /** - * @param - * @param mediator - * @param component * @return non-null settings provider */ Collection getShortcuts(KeYMediator mediator, String componentId, @@ -266,11 +259,50 @@ interface TermInfo { * @param pos the position of the term whose info shall be shown. * @return this extension's term information. */ - @NonNull - List getTermInfoStrings(@NonNull MainWindow mainWindow, @NonNull PosInSequent pos); + List getTermInfoStrings(MainWindow mainWindow, PosInSequent pos); default int getTermLabelPriority() { return 0; } } + + /// A {@link LoadOptionPanel} provides additional UI components in the file selection dialog + /// dependent on the selected profile. + /// + /// Implementing this interface requires to provide an {@link OptionPanel}, and associated + /// {@link Profile}. + /// + /// @author weigl + interface LoadOptionPanel extends Supplier { + Profile getProfile(); + } + + /// A provider of UI components for additional options w.r.t. specific profiles. + /// **Lifecycle:** For each {@link Profile} an {@link OptionPanel} is constructed, when the + /// {@link KeYFileChooser} + /// is instantiated. *On selected of a profile*, the current {@link OptionPanel} is + /// `deinstall`ed, and the + /// {@link OptionPanel} for the selected profile is `install`ed. + /// + /// @author weigl + /// @see KeYFileChooserLoadingOptions + interface OptionPanel { + /// Installs the UI components in the given {@link KeYFileChooserLoadingOptions} instance. + /// UI components + /// can be reused, to keep the temporary state. + /// {@link KeYFileChooserLoadingOptions} uses the {@link net.miginfocom.swing.MigLayout} to + /// manage the layout. + void install(KeYFileChooserLoadingOptions panel); + + /// Removes all *installed* UI components from the panel. + void deinstall(KeYFileChooserLoadingOptions panel); + + /// Returning an arbitrary object, representing the selected option in the UI components. + /// The object needs to compatible with the assigned profile in {@link LoadOptionPanel}. + /// + /// @see Profile#prepareInitConfig(InitConfig, Object) + @SuppressWarnings("JavadocReference") + @Nullable + Configuration getResult(); + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java index a3f270f62ee..fcd28de8311 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java @@ -17,9 +17,12 @@ import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension.LoadOptionPanel; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension.OptionPanel; import de.uka.ilkd.key.gui.extension.api.TabPanel; import de.uka.ilkd.key.pp.PosInSequent; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.init.Profile; import org.jspecify.annotations.Nullable; @@ -401,6 +404,19 @@ public static Stream getTermInfoStrings(MainWindow mainWindow, PosInSequ .flatMap(it -> it.getTermInfoStrings(mainWindow, mousePos).stream()); } + /** + * Helper methods that finds matches {@link Profile} and {@link OptionPanel} together. + * This information are provided by {@link LoadOptionPanel} interface. + */ + public static Map createAdditionalOptionPanels() { + List items = getExtensionInstances(LoadOptionPanel.class); + HashMap map = HashMap.newHashMap(4); + for (LoadOptionPanel item : items) { + map.put(item.getProfile(), item.get()); + } + return map; + } + /** * Disables the clazz from further loading. *

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/profileloading/WDLoadDialogOptionPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/profileloading/WDLoadDialogOptionPanel.java new file mode 100644 index 00000000000..5504aef26b4 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/profileloading/WDLoadDialogOptionPanel.java @@ -0,0 +1,118 @@ +/* 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 de.uka.ilkd.key.gui.profileloading; + +import java.awt.*; +import javax.swing.*; + +import de.uka.ilkd.key.gui.KeYFileChooserLoadingOptions; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.proof.init.Profile; +import de.uka.ilkd.key.settings.Configuration; +import de.uka.ilkd.key.wd.WdProfile; + +import net.miginfocom.layout.CC; +import org.checkerframework.checker.nullness.qual.Nullable; + +/// Additional UI components for the selection of the WD semantics. +/// +/// @author weigl +@KeYGuiExtension.Info(experimental = false) +public class WDLoadDialogOptionPanel implements KeYGuiExtension, KeYGuiExtension.LoadOptionPanel { + @Override + public OptionPanel get() { + return new WDLoadDialogOptionPanelImpl(); + } + + @Override + public Profile getProfile() { + return WdProfile.INSTANCE; + } + + public static class WDLoadDialogOptionPanelImpl implements OptionPanel { + private final JRadioButton rdbWDL = new JRadioButton("L"); + private final JRadioButton rdbWDY = new JRadioButton("Y"); + private final JRadioButton rdbWDD = new JRadioButton("D"); + + private final JLabel lblHeader = new JLabel("WD options"); + private final JLabel lblSemantics = new JLabel("Semantics:"); + private final JSeparator sepHeader = new JSeparator(); + + private static final String DESCRIPTION_L_WD_SEMANTIC = """ + More intuitive for software developers and along the lines of + runtime assertion semantics. Well-Definedness checks will be + stricter using this operator, since the order of terms/formulas + matters. It is based on McCarthy logic. + Cf. "Are the Logical Foundations of Verifying Compiler + Prototypes Matching User Expectations?" by Patrice Chalin. + """; + + private static final String DESCRIPTION_D_WD_SEMANTIC = """ + Complete and along the lines of classical logic, where the + order of terms/formulas is irrelevant. This operator is + equivalent to the D-operator, but more efficient. + Cf. "Efficient Well-Definedness Checking" by Ádám Darvas, + Farhad Mehta, and Arsenii Rudich. + """; + + + private static final String DESCRIPTION_Y_WD_SEMANTIC = """ + Complete and along the lines of classical logic, where the + order of terms/formulas is irrelevant. This operator is not as + strict as the L-operator, based on strong Kleene logic. To be + used with care, since formulas may blow up exponentially. + Cf. "Well Defined B" by Patrick Behm, Lilian Burdy, and + Jean-Marc Meynadier + """; + + public WDLoadDialogOptionPanelImpl() { + lblHeader.setFont(lblHeader.getFont().deriveFont(Font.BOLD)); + + rdbWDL.setToolTipText(DESCRIPTION_L_WD_SEMANTIC); + rdbWDD.setToolTipText(DESCRIPTION_D_WD_SEMANTIC); + rdbWDY.setToolTipText(DESCRIPTION_Y_WD_SEMANTIC); + + ButtonGroup btnGrp = new ButtonGroup(); + btnGrp.add(rdbWDD); + btnGrp.add(rdbWDL); + btnGrp.add(rdbWDY); + + rdbWDL.setSelected(true); + } + + @Override + public void install(KeYFileChooserLoadingOptions panel) { + panel.add(lblHeader); + panel.add(sepHeader, new CC().wrap().span(2).growX()); + + panel.add(lblSemantics); + panel.add(rdbWDD, new CC().span(2).split(3)); + panel.add(rdbWDY); + panel.add(rdbWDL); + } + + @Override + public void deinstall(KeYFileChooserLoadingOptions panel) { + panel.remove(lblHeader); + panel.remove(sepHeader); + panel.remove(lblSemantics); + panel.remove(rdbWDL); + panel.remove(rdbWDD); + panel.remove(rdbWDY); + } + + @Override + public @Nullable Configuration getResult() { + Configuration configuration = new Configuration(); + configuration.set("wdOperator", "wdOperator:L"); + if (rdbWDD.isSelected()) { + configuration.set("wdOperator", "wdOperator:D"); + } + if (rdbWDY.isSelected()) { + configuration.set("wdOperator", "wdOperator:Y"); + } + return configuration; + } + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java index 91bb112e251..de5f4c9cc88 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java @@ -8,10 +8,7 @@ import java.io.FileReader; import java.io.IOException; import java.nio.charset.StandardCharsets; -import java.util.Comparator; -import java.util.LinkedList; -import java.util.List; -import java.util.Properties; +import java.util.*; import javax.swing.*; import de.uka.ilkd.key.gui.MainWindow; @@ -92,12 +89,20 @@ public static ProofIndependentSMTSettings getSmtPiSettings() { } public static ChoiceSettings getChoiceSettings(MainWindow window) { - return ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); - /* - * if (null != window.getMediator().getSelectedProof()) { return - * window.getMediator().getSelectedProof().getSettings().getChoiceSettings(); } else { - * return ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); } - */ + var selectedProof = window.getMediator().getSelectedProof(); + if (null != selectedProof) { + ChoiceSettings settings = new ChoiceSettings(); + settings.setDefaultChoices( + selectedProof.getSettings().getChoiceSettings().getDefaultChoices()); + var cat = selectedProof.getSettings().getChoiceSettings().getCategory2Choices(); + if (cat.isEmpty()) { + cat = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getCategory2Choices(); + } + settings.setChoiceCategories(new TreeMap<>(cat)); + return settings; + } else { + return ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); + } } public static Properties loadProperties(File settingsFile) { diff --git a/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension index fff85bf2d6d..646d2f4c102 100644 --- a/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension +++ b/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -8,4 +8,5 @@ de.uka.ilkd.key.gui.LogView de.uka.ilkd.key.gui.plugins.javac.JavacExtension de.uka.ilkd.key.gui.utilities.HeapStatusExt de.uka.ilkd.key.gui.JmlEnabledKeysIndicator -de.uka.ilkd.key.gui.extension.impl.ProfileNameInStatusBar \ No newline at end of file +de.uka.ilkd.key.gui.extension.impl.ProfileNameInStatusBar +de.uka.ilkd.key.gui.profileloading.WDLoadDialogOptionPanel \ No newline at end of file diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java index 7eab97f1b7a..1786e0e32c6 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java @@ -43,6 +43,12 @@ public interface ImmutableSet return DefaultImmutableSet.nil(); } + /// Creates an immutable set populated with the given values. + static ImmutableSet from(Collection values) { + var set = ImmutableSet.empty(); + return set.add(values); + } + /** * @return a {@code Set} containing the same elements as this {@code ImmutableSet} */