Skip to content

Commit 8e2d966

Browse files
wadoonwadoon
committed
adding the possibility to have a Profile-dependent option panel
# Conflicts: # key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java
1 parent 88a545e commit 8e2d966

23 files changed

Lines changed: 626 additions & 241 deletions

File tree

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -325,4 +325,9 @@ public static boolean isTruthValueEvaluationEnabled(Profile profile) {
325325
return false;
326326
}
327327
}
328+
329+
@Override
330+
public String displayName() {
331+
return NAME;
332+
}
328333
}

‎key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java‎

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@
2020
import org.key_project.logic.Name;
2121
import org.key_project.util.collection.ImmutableList;
2222

23+
import org.jspecify.annotations.Nullable;
24+
2325
/**
2426
* @author Alexander Weigl
2527
* @version 1 (7/27/25)
@@ -97,9 +99,19 @@ public RuleCollection getStandardRules() {
9799
return wdStandardRules;
98100
}
99101

102+
/// {@inheritDoc}
103+
///
104+
/// @param additionalProfileOptions a string representing the choice of `wdOperator`
100105
@Override
101-
public void prepareInitConfig(InitConfig baseConfig) {
106+
public void prepareInitConfig(InitConfig baseConfig,
107+
@Nullable Object additionalProfileOptions) {
102108
var wdChoice = baseConfig.choiceNS().lookup(new Name("wdChecks:on"));
103109
baseConfig.activateChoice(wdChoice);
110+
111+
if (additionalProfileOptions != null) {
112+
var wdOperator =
113+
baseConfig.choiceNS().lookup(new Name(additionalProfileOptions.toString()));
114+
baseConfig.activateChoice(wdOperator);
115+
}
104116
}
105117
}

‎key.core/src/main/antlr4/KeYParser.g4‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,7 @@ one_sort_decl
101101

102102
parametric_sort_decl
103103
:
104+
DOC_COMMENT?
104105
simple_ident_dots
105106
formal_sort_param_decls
106107
;

‎key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.ldt;
55

6+
import java.util.Objects;
7+
68
import de.uka.ilkd.key.proof.init.InitConfig;
79
import de.uka.ilkd.key.settings.ProofSettings;
810

@@ -51,8 +53,8 @@ public static boolean isFinalEnabled(@NonNull InitConfig initConfig) {
5153
* @return true if final fields are treated as immutable
5254
*/
5355
public static boolean isFinalEnabled(@NonNull ProofSettings settings) {
54-
return settings.getChoiceSettings().getDefaultChoices().get(SETTING)
55-
.equals(IMMUTABLE_OPTION);
56+
return Objects.equals(settings.getChoiceSettings().getDefaultChoices().get(SETTING),
57+
IMMUTABLE_OPTION);
5658
}
5759

5860
/**

‎key.core/src/main/java/de/uka/ilkd/key/logic/DocSpace.java‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
package de.uka.ilkd.key.logic;
5+
6+
import java.util.Map;
7+
import java.util.TreeMap;
8+
9+
import org.key_project.logic.HasDocumentation;
10+
11+
import org.jspecify.annotations.NullMarked;
12+
import org.jspecify.annotations.Nullable;
13+
14+
@NullMarked
15+
public class DocSpace {
16+
private @Nullable DocSpace parent;
17+
private final Map<String, String> documentation = new TreeMap<>();
18+
19+
public DocSpace() {}
20+
21+
public DocSpace(Map<String, String> documentation) {
22+
this.documentation.putAll(documentation);
23+
}
24+
25+
public DocSpace(DocSpace parent) {
26+
this.parent = parent;
27+
}
28+
29+
public DocSpace(@Nullable DocSpace parent, Map<String, String> documentation) {
30+
this(documentation);
31+
this.parent = parent;
32+
}
33+
34+
public @Nullable String find(String key) {
35+
var value = documentation.get(key);
36+
if (value != null)
37+
return value;
38+
if (parent != null)
39+
return parent.find(key);
40+
return null;
41+
}
42+
43+
public @Nullable String find(HasDocumentation entity) {
44+
var doc = entity.getDocumentation();
45+
if (doc != null) {
46+
return doc;
47+
}
48+
return find(entity.getDocumentationKey());
49+
}
50+
51+
public void add(DocSpace space) {
52+
this.documentation.putAll(space.documentation);
53+
}
54+
55+
public @Nullable DocSpace parent() {
56+
return parent;
57+
}
58+
59+
public void describe(HasDocumentation entity, @Nullable String doc) {
60+
if (doc == null) {
61+
return;
62+
}
63+
documentation.put(entity.getDocumentationKey(), doc);
64+
}
65+
66+
public DocSpace copy() {
67+
return new DocSpace(parent, documentation);
68+
}
69+
}

‎key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java‎

Lines changed: 66 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@
44
package de.uka.ilkd.key.logic;
55

66

7+
import java.util.Objects;
8+
79
import de.uka.ilkd.key.logic.op.IProgramVariable;
810
import de.uka.ilkd.key.logic.op.ParametricFunctionDecl;
911
import de.uka.ilkd.key.logic.sort.ParametricSortDecl;
@@ -19,32 +21,51 @@
1921
import org.key_project.prover.rules.RuleSet;
2022

2123
import org.jspecify.annotations.NonNull;
24+
import org.jspecify.annotations.NullMarked;
2225
import org.jspecify.annotations.Nullable;
2326

27+
@NullMarked
2428
public class NamespaceSet {
2529

26-
private Namespace<@NonNull QuantifiableVariable> varNS = new Namespace<>();
27-
private Namespace<@NonNull IProgramVariable> progVarNS = new Namespace<>();
30+
private Namespace<QuantifiableVariable> varNS = new Namespace<>();
31+
private Namespace<IProgramVariable> progVarNS = new Namespace<>();
2832
// TODO: Operators should not be local to goals
29-
private Namespace<@NonNull Function> funcNS = new Namespace<>();
30-
private Namespace<@NonNull RuleSet> ruleSetNS = new Namespace<>();
31-
private Namespace<@NonNull Sort> sortNS = new Namespace<>();
33+
private Namespace<Function> funcNS = new Namespace<>();
34+
private Namespace<RuleSet> ruleSetNS = new Namespace<>();
35+
private Namespace<Sort> sortNS = new Namespace<>();
3236
private Namespace<@NonNull SortAlias> sortAliases = new Namespace<>();
33-
private Namespace<@NonNull ParametricSortDecl> parametricSortNS = new Namespace<>();
34-
private Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS = new Namespace<>();
35-
private Namespace<@NonNull Choice> choiceNS = new Namespace<>();
37+
private Namespace<ParametricSortDecl> parametricSortNS = new Namespace<>();
38+
private Namespace<ParametricFunctionDecl> parametricFuncNS = new Namespace<>();
39+
private Namespace<Choice> choiceNS = new Namespace<>();
40+
private DocSpace documentation = new DocSpace();
3641

3742
public NamespaceSet() {
3843
}
3944

40-
public NamespaceSet(Namespace<@NonNull QuantifiableVariable> varNS,
41-
Namespace<@NonNull Function> funcNS,
42-
Namespace<@NonNull Sort> sortNS, Namespace<@NonNull SortAlias> sortAliases,
43-
Namespace<@NonNull RuleSet> ruleSetNS,
44-
Namespace<@NonNull ParametricSortDecl> parametricSortNS,
45-
Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS,
46-
Namespace<@NonNull Choice> choiceNS,
47-
Namespace<@NonNull IProgramVariable> programVarNS) {
45+
public NamespaceSet(Namespace<QuantifiableVariable> varNS,
46+
Namespace<Function> funcNS,
47+
Namespace<Sort> sortNS,
48+
Namespace<SortAlias> sortAliases,
49+
Namespace<RuleSet> ruleSetNS,
50+
Namespace<ParametricSortDecl> parametricSortNS,
51+
Namespace<ParametricFunctionDecl> parametricFuncNS,
52+
Namespace<Choice> choiceNS,
53+
Namespace<IProgramVariable> programVarNS) {
54+
this(varNS, funcNS, sortNS, sortAliases, ruleSetNS,
55+
parametricSortNS, parametricFuncNS,
56+
choiceNS, programVarNS, new DocSpace());
57+
}
58+
59+
public NamespaceSet(Namespace<QuantifiableVariable> varNS,
60+
Namespace<Function> funcNS,
61+
Namespace<Sort> sortNS,
62+
Namespace<SortAlias> sortAliases,
63+
Namespace<RuleSet> ruleSetNS,
64+
Namespace<ParametricSortDecl> parametricSortNS,
65+
Namespace<ParametricFunctionDecl> parametricFuncNS,
66+
Namespace<Choice> choiceNS,
67+
Namespace<IProgramVariable> programVarNS,
68+
DocSpace documentation) {
4869
this.varNS = varNS;
4970
this.progVarNS = programVarNS;
5071
this.funcNS = funcNS;
@@ -54,21 +75,23 @@ public NamespaceSet(Namespace<@NonNull QuantifiableVariable> varNS,
5475
this.choiceNS = choiceNS;
5576
this.parametricSortNS = parametricSortNS;
5677
this.parametricFuncNS = parametricFuncNS;
78+
this.documentation = Objects.requireNonNull(documentation);
5779
}
5880

81+
5982
public NamespaceSet copy() {
6083
return new NamespaceSet(variables().copy(), functions().copy(),
6184
sorts().copy(), sortAliases().copy(),
6285
ruleSets().copy(), parametricSortNS.copy(), parametricFuncNS.copy(), choices().copy(),
63-
programVariables().copy());
86+
programVariables().copy(),
87+
documentation.copy());
6488
}
6589

6690
public NamespaceSet shallowCopy() {
6791
return new NamespaceSet(variables(), functions(), sorts(), sortAliases(), ruleSets(),
6892
parametricSorts(),
6993
parametricFunctions(),
70-
choices(),
71-
programVariables());
94+
choices(), programVariables(), new DocSpace(documentation));
7295
}
7396

7497
// TODO MU: Rename into sth with wrap or similar
@@ -77,46 +100,47 @@ public NamespaceSet copyWithParent() {
77100
new Namespace<>(functions()), new Namespace<>(sorts()), new Namespace<>(sortAliases()),
78101
new Namespace<>(ruleSets()), new Namespace<>(parametricSorts()),
79102
new Namespace<>(parametricFunctions()), new Namespace<>(choices()),
80-
new Namespace<>(programVariables()));
103+
new Namespace<>(programVariables()),
104+
new DocSpace(documentation));
81105
}
82106

83-
public Namespace<@NonNull QuantifiableVariable> variables() {
107+
public Namespace<QuantifiableVariable> variables() {
84108
return varNS;
85109
}
86110

87-
public void setVariables(Namespace<@NonNull QuantifiableVariable> varNS) {
111+
public void setVariables(Namespace<QuantifiableVariable> varNS) {
88112
this.varNS = varNS;
89113
}
90114

91-
public Namespace<@NonNull IProgramVariable> programVariables() {
115+
public Namespace<IProgramVariable> programVariables() {
92116
return progVarNS;
93117
}
94118

95-
public void setProgramVariables(Namespace<@NonNull IProgramVariable> progVarNS) {
119+
public void setProgramVariables(Namespace<IProgramVariable> progVarNS) {
96120
this.progVarNS = progVarNS;
97121
}
98122

99-
public Namespace<@NonNull Function> functions() {
123+
public Namespace<Function> functions() {
100124
return funcNS;
101125
}
102126

103-
public void setFunctions(Namespace<@NonNull Function> funcNS) {
127+
public void setFunctions(Namespace<Function> funcNS) {
104128
this.funcNS = funcNS;
105129
}
106130

107-
public Namespace<@NonNull RuleSet> ruleSets() {
131+
public Namespace<RuleSet> ruleSets() {
108132
return ruleSetNS;
109133
}
110134

111-
public void setRuleSets(Namespace<@NonNull RuleSet> ruleSetNS) {
135+
public void setRuleSets(Namespace<RuleSet> ruleSetNS) {
112136
this.ruleSetNS = ruleSetNS;
113137
}
114138

115-
public Namespace<@NonNull Sort> sorts() {
139+
public Namespace<Sort> sorts() {
116140
return sortNS;
117141
}
118142

119-
public void setSorts(Namespace<@NonNull Sort> sortNS) {
143+
public void setSorts(Namespace<Sort> sortNS) {
120144
this.sortNS = sortNS;
121145
}
122146

@@ -128,28 +152,28 @@ public void setSortAliases(Namespace<@NonNull SortAlias> sortAliases) {
128152
this.sortAliases = sortAliases;
129153
}
130154

131-
public Namespace<@NonNull ParametricSortDecl> parametricSorts() {
155+
public Namespace<ParametricSortDecl> parametricSorts() {
132156
return parametricSortNS;
133157
}
134158

135-
public void setParametricSorts(Namespace<@NonNull ParametricSortDecl> parametricSortNS) {
159+
public void setParametricSorts(Namespace<ParametricSortDecl> parametricSortNS) {
136160
this.parametricSortNS = parametricSortNS;
137161
}
138162

139-
public Namespace<@NonNull ParametricFunctionDecl> parametricFunctions() {
163+
public Namespace<ParametricFunctionDecl> parametricFunctions() {
140164
return parametricFuncNS;
141165
}
142166

143167
public void setParametricFunctions(
144-
Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS) {
168+
Namespace<ParametricFunctionDecl> parametricFuncNS) {
145169
this.parametricFuncNS = parametricFuncNS;
146170
}
147171

148-
public Namespace<@NonNull Choice> choices() {
172+
public Namespace<Choice> choices() {
149173
return choiceNS;
150174
}
151175

152-
public void setChoices(Namespace<@NonNull Choice> choiceNS) {
176+
public void setChoices(Namespace<Choice> choiceNS) {
153177
this.choiceNS = choiceNS;
154178
}
155179

@@ -278,14 +302,14 @@ public NamespaceSet simplify() {
278302
return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(),
279303
sortAliases.simplify(),
280304
ruleSetNS.simplify(), parametricSortNS.simplify(), parametricFuncNS.simplify(),
281-
choiceNS.simplify(), progVarNS.simplify());
305+
choiceNS.simplify(), progVarNS.simplify(), documentation);
282306
}
283307

284308
public NamespaceSet getCompression() {
285309
return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(),
286310
sortAliases.compress(),
287311
ruleSetNS.compress(), parametricSortNS.compress(), parametricFuncNS.compress(),
288-
choiceNS.compress(), progVarNS.compress());
312+
choiceNS.compress(), progVarNS.compress(), documentation);
289313
}
290314

291315
public void flushToParent() {
@@ -298,7 +322,10 @@ public NamespaceSet getParent() {
298322
return new NamespaceSet(varNS.parent(), funcNS.parent(), sortNS.parent(),
299323
sortAliases.parent(),
300324
ruleSetNS.parent(), parametricSortNS.parent(), parametricFuncNS.parent(),
301-
choiceNS.parent(), progVarNS.parent());
325+
choiceNS.parent(), progVarNS.parent(), documentation.parent());
302326
}
303327

328+
public DocSpace docs() {
329+
return documentation;
330+
}
304331
}

‎key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55

66
import de.uka.ilkd.key.logic.GenericParameter;
77

8+
import org.key_project.logic.HasDocumentation;
89
import org.key_project.logic.Name;
910
import org.key_project.logic.Named;
1011
import org.key_project.logic.Sorted;
@@ -18,8 +19,8 @@
1819
/// The abstract declaration of a parametric function, e.g., `append<[E]>(List<[E]>, List<[E]>)`.
1920
///
2021
/// To get an instantiated instance, use [ParametricFunctionInstance#get(ParametricFunctionDecl,
21-
/// ImmutableList, Services)].
22-
public final class ParametricFunctionDecl implements Named, Sorted {
22+
/// ImmutableList, de.uka.ilkd.key.java.Services)].
23+
public final class ParametricFunctionDecl implements Named, Sorted, HasDocumentation {
2324
private final Name name;
2425
private final ImmutableList<GenericParameter> parameters;
2526
private final ImmutableArray<Sort> argSorts;
@@ -76,4 +77,9 @@ public ImmutableList<GenericParameter> getParameters() {
7677
public @NonNull Name name() {
7778
return name;
7879
}
80+
81+
@Override
82+
public String getDocumentationKey() {
83+
return "pfun/" + name();
84+
}
7985
}

0 commit comments

Comments
 (0)