Skip to content

Commit 603b2ca

Browse files
wadoonwadoon
authored
Fix passing of warnings (#3302)
2 parents 3a5f9fd + 44087c2 commit 603b2ca

File tree

8 files changed

+115
-54
lines changed

8 files changed

+115
-54
lines changed

‎key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -51,8 +51,7 @@ public class KeyIO {
5151
private final NamespaceSet nss;
5252
@Nullable
5353
private Namespace<SchemaVariable> schemaNamespace;
54-
@Nullable
55-
private List<BuildingIssue> warnings;
54+
private List<BuildingIssue> warnings = new LinkedList<>();
5655
private AbbrevMap abbrevMap;
5756

5857

@@ -166,23 +165,29 @@ public Loader load(URL u) {
166165
public List<Taclet> findTaclets(KeyAst.File ctx) {
167166
TacletPBuilder visitor = new TacletPBuilder(services, nss);
168167
ctx.accept(visitor);
168+
warnings.addAll(visitor.getBuildingIssues());
169169
return visitor.getTopLevelTaclets();
170170
}
171171

172172
/**
173173
* @param ctx
174+
* @return
174175
*/
175-
public void evalDeclarations(KeyAst.File ctx) {
176+
public List<BuildingIssue> evalDeclarations(KeyAst.File ctx) {
176177
DeclarationBuilder declBuilder = new DeclarationBuilder(services, nss);
177178
ctx.accept(declBuilder);
179+
warnings.addAll(declBuilder.getBuildingIssues());
180+
return declBuilder.getBuildingIssues();
178181
}
179182

180183
/**
181184
* @param ctx
182185
*/
183-
public void evalFuncAndPred(KeyAst.File ctx) {
186+
public List<BuildingIssue> evalFuncAndPred(KeyAst.File ctx) {
184187
FunctionPredicateBuilder visitor = new FunctionPredicateBuilder(services, nss);
185188
ctx.accept(visitor);
189+
warnings.addAll(visitor.getBuildingIssues());
190+
return visitor.getBuildingIssues();
186191
}
187192

188193

@@ -198,7 +203,6 @@ public AbbrevMap getAbbrevMap() {
198203
return abbrevMap;
199204
}
200205

201-
@Nullable
202206
public List<BuildingIssue> getWarnings() {
203207
return warnings;
204208
}

‎key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@
2222
import org.key_project.util.collection.ImmutableSet;
2323

2424
import org.antlr.v4.runtime.Token;
25+
import org.slf4j.Logger;
26+
import org.slf4j.LoggerFactory;
2527

2628
/**
2729
* This visitor evaluates all basic (level 0) declarations. This includes:
@@ -41,6 +43,7 @@
4143
*/
4244
public class DeclarationBuilder extends DefaultBuilder {
4345
private final Map<String, String> category2Default = new HashMap<>();
46+
private static final Logger LOGGER = LoggerFactory.getLogger(DeclarationBuilder.class);
4447

4548
public DeclarationBuilder(Services services, NamespaceSet nss) {
4649
super(services, nss);
@@ -168,7 +171,12 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) {
168171
sorts().add(s);
169172
createdSorts.add(s);
170173
} else {
171-
addWarning(ctx, "Sort declaration is ignored, due to collision.");
174+
// weigl: agreement on KaKeY meeting: this should be ignored until we finally have
175+
// local namespaces
176+
// for generic sorts
177+
// addWarning(ctx, "Sort declaration is ignored, due to collision.");
178+
LOGGER.info("Sort declaration is ignored, due to collision in {}",
179+
BuilderHelpers.getPosition(ctx));
172180
}
173181
}
174182
return createdSorts;

‎key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java‎

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,9 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) {
9696

9797
if (lookup(p.name()) == null) {
9898
functions().add(p);
99+
} else {
100+
// weigl: agreement on KaKeY meeting: this should be an error.
101+
semanticError(ctx, "Predicate '" + p.name() + "' is already defined!");
99102
}
100103
return null;
101104
}
@@ -104,7 +107,7 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) {
104107
public Object visitFunc_decl(KeYParser.Func_declContext ctx) {
105108
boolean unique = ctx.UNIQUE() != null;
106109
Sort retSort = accept(ctx.sortId());
107-
String func_name = accept(ctx.funcpred_name());
110+
String funcName = accept(ctx.funcpred_name());
108111
List<Boolean[]> whereToBind = accept(ctx.where_to_bind());
109112
List<Sort> argSorts = accept(ctx.arg_sorts());
110113
assert argSorts != null;
@@ -114,11 +117,11 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) {
114117
}
115118

116119
Function f = null;
117-
assert func_name != null;
118-
int separatorIndex = func_name.indexOf("::");
120+
assert funcName != null;
121+
int separatorIndex = funcName.indexOf("::");
119122
if (separatorIndex > 0) {
120-
String sortName = func_name.substring(0, separatorIndex);
121-
String baseName = func_name.substring(separatorIndex + 2);
123+
String sortName = funcName.substring(0, separatorIndex);
124+
String baseName = funcName.substring(separatorIndex + 2);
122125
Sort genSort = lookupSort(sortName);
123126
if (genSort instanceof GenericSort) {
124127
f = SortDependingFunction.createFirstInstance((GenericSort) genSort,
@@ -127,14 +130,15 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) {
127130
}
128131

129132
if (f == null) {
130-
f = new Function(new Name(func_name), retSort, argSorts.toArray(new Sort[0]),
133+
f = new Function(new Name(funcName), retSort, argSorts.toArray(new Sort[0]),
131134
whereToBind == null ? null : whereToBind.toArray(new Boolean[0]), unique);
132135
}
133136

134137
if (lookup(f.name()) == null) {
135138
functions().add(f);
136139
} else {
137-
addWarning("Function '" + func_name + "' is already defined!");
140+
// weigl: agreement on KaKeY meeting: this should be an error.
141+
semanticError(ctx, "Function '" + funcName + "' is already defined!");
138142
}
139143
return f;
140144
}

‎key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ public ImmutableSet<PositionedString> read() throws ProofInputException {
105105
ImmutableSet<PositionedString> warnings = DefaultImmutableSet.nil();
106106

107107
// read key file itself (except contracts)
108-
super.readExtendedSignature();
108+
warnings = warnings.union(super.readExtendedSignature());
109109

110110
// read in-code specifications
111111
SLEnvInput slEnvInput = new SLEnvInput(readJavaPath(), readClassPath(), readBootClassPath(),

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java‎

Lines changed: 13 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
import java.net.URISyntaxException;
1212
import java.net.URL;
1313
import java.util.ArrayList;
14+
import java.util.Collection;
1415
import java.util.List;
1516
import java.util.Objects;
1617
import java.util.stream.Collectors;
@@ -315,10 +316,11 @@ public ImmutableSet<PositionedString> readExtendedSignature() {
315316
ChoiceInformation ci = getParseContext().getChoices();
316317
initConfig.addCategory2DefaultChoices(ci.getDefaultOptions());
317318

318-
readSorts();
319-
readFuncAndPred();
319+
var warnings = new ArrayList<PositionedString>();
320+
warnings.addAll(readSorts());
321+
warnings.addAll(readFuncAndPred());
320322

321-
return DefaultImmutableSet.nil();
323+
return DefaultImmutableSet.fromCollection(warnings);
322324
}
323325

324326
/**
@@ -351,27 +353,32 @@ protected ProblemFinder getProblemFinder() {
351353
* reads the sorts declaration of the .key file only, modifying the sort namespace of the
352354
* initial configuration
353355
*/
354-
public void readSorts() {
356+
public Collection<PositionedString> readSorts() {
355357
KeyAst.File ctx = getParseContext();
356358
KeyIO io = new KeyIO(initConfig.getServices(), initConfig.namespaces());
357359
io.evalDeclarations(ctx);
358360
ChoiceInformation choice = getParseContext().getChoices();
359361
// we ignore the namespace of choice finder.
360362
initConfig.addCategory2DefaultChoices(choice.getDefaultOptions());
363+
364+
return io.getWarnings().stream().map(BuildingIssue::asPositionedString).toList();
361365
}
362366

363367

364368
/**
365369
* reads the functions and predicates declared in the .key file only, modifying the function
366370
* namespaces of the respective taclet options.
371+
*
372+
* @return warnings during the interpretation of the AST constructs
367373
*/
368-
public void readFuncAndPred() {
374+
public List<PositionedString> readFuncAndPred() {
369375
if (file == null) {
370-
return;
376+
return null;
371377
}
372378
KeyAst.File ctx = getParseContext();
373379
KeyIO io = new KeyIO(initConfig.getServices(), initConfig.namespaces());
374380
io.evalFuncAndPred(ctx);
381+
return io.getWarnings().stream().map(BuildingIssue::asPositionedString).toList();
375382
}
376383

377384

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java‎

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -110,19 +110,25 @@ public File readBootClassPath() {
110110
* reads all LDTs, i.e., all associated .key files with respect to the given modification
111111
* strategy. Reading is done in a special order: first all sort declarations then all function
112112
* and predicate declarations and third the rules. This procedure makes it possible to use all
113-
* declared sorts in all rules, e.g.
113+
* declared sorts in all rules.
114+
*
115+
* @return a list of warnings during the parsing the process
114116
*/
115117
@Override
116118
public ImmutableSet<PositionedString> read() {
119+
var warnings = new ArrayList<PositionedString>();
120+
117121
if (initConfig == null) {
118122
throw new IllegalStateException("LDTInput: InitConfig not set.");
119123
}
120124

121125
for (KeYFile keYFile : keyFiles) {
122-
keYFile.readSorts();
126+
var w = keYFile.readSorts();
127+
warnings.addAll(w);
123128
}
124129
for (KeYFile file : keyFiles) {
125-
file.readFuncAndPred();
130+
var w = file.readFuncAndPred();
131+
warnings.addAll(w);
126132
}
127133
// create LDT objects to have them available for parsing
128134
initConfig.getServices().getTypeConverter().init();
@@ -135,7 +141,7 @@ public ImmutableSet<PositionedString> read() {
135141
}
136142

137143

138-
return DefaultImmutableSet.nil();
144+
return DefaultImmutableSet.fromCollection(warnings);
139145
}
140146

141147
@Override

‎key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingIssue.java‎

Lines changed: 41 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,50 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.util.parsing;
55

6+
import java.net.URI;
7+
import java.net.URISyntaxException;
8+
69
import de.uka.ilkd.key.java.Position;
10+
import de.uka.ilkd.key.parser.Location;
11+
import de.uka.ilkd.key.speclang.PositionedString;
712

813
import org.antlr.v4.runtime.ParserRuleContext;
914
import org.antlr.v4.runtime.Token;
1015
import org.jspecify.annotations.Nullable;
1116

12-
public record BuildingIssue(String message,@Nullable Throwable cause,boolean isWarning,Position position){
13-
14-
public static BuildingIssue createError(String message,@Nullable ParserRuleContext token,@Nullable Throwable cause){return createError(message,token!=null?token.start:null,cause);}
15-
16-
private static BuildingIssue fromToken(String message,boolean isWarning,@Nullable Token token,@Nullable Throwable cause){if(token!=null){var position=Position.fromToken(token);return new BuildingIssue(message,cause,isWarning,position);}return new BuildingIssue(message,cause,isWarning,Position.UNDEFINED);}
17-
18-
public static BuildingIssue createError(String message,@Nullable Token token,@Nullable Throwable cause){return fromToken(message,false,token,cause);}
19-
20-
public static BuildingIssue createWarning(String message,@Nullable ParserRuleContext token,@Nullable Throwable cause){return createWarning(message,token!=null?token.start:null,cause);}
21-
22-
public static BuildingIssue createWarning(String message,@Nullable Token token,@Nullable Throwable cause){return fromToken(message,true,token,cause);}}
17+
public record BuildingIssue(String message, @Nullable Throwable cause, boolean isWarning,
18+
Position position,
19+
@Nullable String sourceName) {
20+
21+
public static BuildingIssue createError(String message, @Nullable ParserRuleContext token, @Nullable Throwable cause) {
22+
return createError(message, token != null ? token.start : null, cause);
23+
}
24+
25+
private static BuildingIssue fromToken(String message, boolean isWarning, @Nullable Token token, @Nullable Throwable cause) {
26+
if (token != null) {
27+
var position = Position.fromToken(token);
28+
return new BuildingIssue(message, cause, isWarning, position, token.getTokenSource().getSourceName());
29+
}
30+
return new BuildingIssue(message, cause, isWarning, Position.UNDEFINED, null);
31+
}
32+
33+
public static BuildingIssue createError(String message, @Nullable Token token, @Nullable Throwable cause) {
34+
return fromToken(message, false, token, cause);
35+
}
36+
37+
public static BuildingIssue createWarning(String message, @Nullable ParserRuleContext token, @Nullable Throwable cause) {
38+
return createWarning(message, token != null ? token.start : null, cause);
39+
}
40+
41+
public static BuildingIssue createWarning(String message, @Nullable Token token, @Nullable Throwable cause) {
42+
return fromToken(message, true, token, cause);
43+
}
44+
45+
public PositionedString asPositionedString() {
46+
try {
47+
return new PositionedString(message, new Location(new URI(sourceName), position));
48+
} catch (URISyntaxException e) {
49+
return null;
50+
}
51+
}
52+
}

‎key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParser.java‎

Lines changed: 21 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -46,25 +46,27 @@ protected Services getServices() {
4646

4747
@BeforeEach
4848
public void setUp() throws IOException {
49-
parseDecls("""
50-
\\sorts { boolean; elem; list; int; int_sort; numbers; }
51-
\\functions {
52-
elem head(list);
53-
list tail(list);
54-
list nil;
55-
list cons(elem,list);
56-
int aa ;
57-
int bb ;
58-
int cc ;
59-
int dd ;
60-
int ee ;
61-
}
62-
\\predicates {
63-
isempty(list);
64-
}
65-
\\programVariables {int globalIntPV;}"""
66-
67-
);
49+
if (lookup_sort("elem") == null) {// check whether declaration have already been parsed
50+
parseDecls("""
51+
\\sorts { boolean; elem; list; int; int_sort; numbers; }
52+
\\functions {
53+
elem head(list);
54+
list tail(list);
55+
list nil;
56+
list cons(elem,list);
57+
int aa ;
58+
int bb ;
59+
int cc ;
60+
int dd ;
61+
int ee ;
62+
}
63+
\\predicates {
64+
isempty(list);
65+
}
66+
\\programVariables {int globalIntPV;}"""
67+
68+
);
69+
}
6870

6971
elem = lookup_sort("elem");
7072
list = lookup_sort("list");

0 commit comments

Comments
 (0)