Skip to content

Commit 44b59e7

Browse files
wadoonwadoon
committed
add test case
1 parent 44c8446 commit 44b59e7

File tree

5 files changed

+254
-199
lines changed

5 files changed

+254
-199
lines changed

‎key.format/src/main/java/de/uka/ilkd/key/nparser/format/ExpressionVisitor.java‎

Lines changed: 24 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -3,40 +3,40 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.nparser.format;
55

6-
import java.util.Set;
7-
86
import de.uka.ilkd.key.nparser.KeYLexer;
97
import de.uka.ilkd.key.nparser.KeYParser;
108
import de.uka.ilkd.key.nparser.KeYParserBaseVisitor;
11-
129
import org.antlr.v4.runtime.CommonTokenStream;
1310
import org.antlr.v4.runtime.tree.TerminalNode;
1411

12+
import java.util.Set;
13+
1514
/**
16-
*
1715
* @author Julian Wiesler
1816
*/
1917
class ExpressionVisitor extends KeYParserBaseVisitor<Void> {
2018
private static final Set<Integer> OPERATORS = Set.of(
21-
KeYLexer.LESS,
22-
KeYLexer.LESSEQUAL,
23-
KeYLexer.GREATER,
24-
KeYLexer.GREATEREQUAL,
25-
KeYLexer.EQUALS,
26-
KeYLexer.NOT_EQUALS,
27-
KeYLexer.IMP,
28-
KeYLexer.SEQARROW,
29-
KeYLexer.NOT_EQUALS,
30-
KeYLexer.AND,
31-
KeYLexer.OR,
32-
KeYLexer.PARALLEL,
33-
KeYLexer.EXP,
34-
KeYLexer.PERCENT,
35-
KeYLexer.STAR,
36-
KeYLexer.MINUS,
37-
KeYLexer.PLUS,
38-
KeYLexer.EQV,
39-
KeYLexer.ASSIGN);
19+
KeYLexer.LESS,
20+
KeYLexer.LESSEQUAL,
21+
KeYLexer.GREATER,
22+
KeYLexer.GREATEREQUAL,
23+
KeYLexer.EQUALS,
24+
KeYLexer.IMP,
25+
KeYLexer.SEQARROW,
26+
KeYLexer.NOT_EQUALS,
27+
KeYLexer.AND,
28+
KeYLexer.OR,
29+
KeYLexer.PARALLEL,
30+
KeYLexer.EXP,
31+
KeYLexer.PERCENT,
32+
KeYLexer.STAR,
33+
KeYLexer.MINUS,
34+
KeYLexer.PLUS,
35+
KeYLexer.EQV,
36+
KeYLexer.ASSIGN);
37+
38+
private static final Set<Integer> BRACES = Set.of(
39+
KeYLexer.LBRACE, KeYLexer.LPAREN, KeYLexer.LBRACKET, KeYLexer.LGUILLEMETS);
4040

4141
private final CommonTokenStream ts;
4242
private final Output output;
@@ -80,8 +80,7 @@ private static void outputModality(String text, Output output) {
8080
public Void visitTerminal(TerminalNode node) {
8181
int token = node.getSymbol().getType();
8282

83-
boolean isLBrace = token == KeYLexer.LBRACE || token == KeYLexer.LPAREN
84-
|| token == KeYLexer.LBRACKET || token == KeYLexer.LGUILLEMETS;
83+
boolean isLBrace = BRACES.contains(token);
8584
if (token == KeYLexer.RBRACE || token == KeYLexer.RPAREN || token == KeYLexer.RBRACKET
8685
|| token == KeYLexer.RGUILLEMETS) {
8786
output.noSpaceBeforeNext();

‎key.format/src/main/java/de/uka/ilkd/key/nparser/format/KeYFileFormatter.java‎

Lines changed: 47 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -3,25 +3,48 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.nparser.format;
55

6+
import java.io.IOException;
7+
import java.nio.file.Path;
68
import java.util.List;
79

810
import de.uka.ilkd.key.nparser.KeYLexer;
911
import de.uka.ilkd.key.nparser.KeYParser;
1012
import de.uka.ilkd.key.nparser.KeYParserBaseVisitor;
1113

14+
import de.uka.ilkd.key.nparser.ParsingFacade;
1215
import org.antlr.v4.runtime.*;
1316
import org.antlr.v4.runtime.tree.ParseTree;
1417
import org.antlr.v4.runtime.tree.RuleNode;
1518
import org.antlr.v4.runtime.tree.TerminalNode;
1619
import org.jspecify.annotations.Nullable;
1720

21+
/**
22+
* {@link KeYFileFormatter} is the entry point for reformatting operation on KeY files.
23+
* <p>
24+
* It works on the AST and also on the token stream
25+
* to also capture hidden tokens like comments.
26+
* <p>
27+
* For the future, it would be nice to move this onto a stable pretty-printing engine,
28+
* which also allows line breaks with indentation if necessary.
29+
* We already have such an engine for Java in the background
30+
* ({@link de.uka.ilkd.key.util.pp.Layouter}).
31+
*
32+
* @author Julian Wiesler
33+
*/
1834
public class KeYFileFormatter extends KeYParserBaseVisitor<Void> {
19-
/** Maximum newlines between tokens (2 equals to 1 empty line) */
35+
/**
36+
* Maximum newlines between tokens (2 means one empty line)
37+
*/
2038
private static final int MAX_NEWLINES_BETWEEN = 2;
2139

2240
private final Output output = new Output();
2341
private final CommonTokenStream ts;
2442

43+
/**
44+
* Create a {@link KeYFileFormatter} with the given stream of tokens.
45+
*
46+
* @param ts a token stream created by {@link KeYLexer}
47+
*/
2548
public KeYFileFormatter(CommonTokenStream ts) {
2649
this.ts = ts;
2750
}
@@ -138,14 +161,14 @@ public Void visitModifiers(KeYParser.ModifiersContext ctx) {
138161

139162
@Override
140163
public Void visitVarexplist(KeYParser.VarexplistContext ctx) {
141-
var varexps = ctx.varexp();
164+
var varConditions = ctx.varexp();
142165
var commas = ctx.COMMA();
143-
boolean multiline = varexps.size() > 3;
144-
for (int i = 0; i < varexps.size(); i++) {
166+
boolean multiline = varConditions.size() > 3;
167+
for (int i = 0; i < varConditions.size(); i++) {
145168
if (multiline) {
146169
output.assertNewLineAndIndent();
147170
}
148-
visit(varexps.get(i));
171+
visit(varConditions.get(i));
149172
if (i < commas.size()) {
150173
visit(commas.get(i));
151174
if (!multiline && output.isNewLine()) {
@@ -239,8 +262,8 @@ private static void processHiddenTokens(@Nullable List<Token> tokens, Output out
239262
}
240263
}
241264

242-
private static void processHiddenTokensAfterCurrent(Token currentToken, CommonTokenStream ts,
243-
Output output) {
265+
static void processHiddenTokensAfterCurrent(Token currentToken, CommonTokenStream ts,
266+
Output output) {
244267
// add hidden tokens after the current token (whitespace, comments etc.)
245268
List<Token> list = ts.getHiddenTokensToRight(currentToken.getTokenIndex());
246269
processHiddenTokens(list, output);
@@ -330,7 +353,7 @@ public Void visitTerminal(TerminalNode node) {
330353
var token = node.getSymbol().getType();
331354

332355
boolean isLBrace =
333-
token == KeYLexer.LBRACE || token == KeYLexer.LPAREN || token == KeYLexer.LBRACKET;
356+
token == KeYLexer.LBRACE || token == KeYLexer.LPAREN || token == KeYLexer.LBRACKET;
334357
if (isLBrace) {
335358
output.spaceBeforeNext();
336359
} else if (token == KeYLexer.RBRACE || token == KeYLexer.RPAREN
@@ -344,9 +367,9 @@ public Void visitTerminal(TerminalNode node) {
344367
}
345368

346369
var noSpaceAround =
347-
token == KeYLexer.COLON || token == KeYLexer.DOT || token == KeYLexer.DOUBLECOLON;
370+
token == KeYLexer.COLON || token == KeYLexer.DOT || token == KeYLexer.DOUBLECOLON;
348371
var noSpaceBefore =
349-
token == KeYLexer.SEMI || token == KeYLexer.COMMA || token == KeYLexer.LPAREN;
372+
token == KeYLexer.SEMI || token == KeYLexer.COMMA || token == KeYLexer.LPAREN;
350373
if (noSpaceBefore || noSpaceAround) {
351374
output.noSpaceBeforeNext();
352375
}
@@ -376,29 +399,29 @@ private static int countNLs(String text) {
376399

377400
/**
378401
* Entry level method to the formatter.
379-
* The formatter uses System.lineSeparator as line separator and accepts any line separator as
380-
* input.
381402
*
382-
* @param text the input text
383-
* @return the formatted text *or null*, if the input was not parseable
403+
* @param stream char stream
404+
* @return the formatted text
405+
* @throws de.uka.ilkd.key.util.parsing.SyntaxErrorReporter.ParserException if the given text is not parser
384406
*/
385-
public static @Nullable String format(String text) {
386-
var in = CharStreams.fromString(text.replaceAll("\\r\\n?", "\n"));
387-
KeYLexer lexer = new KeYLexer(in);
388-
lexer.setTokenFactory(new CommonTokenFactory(true));
407+
public static String format(CharStream stream) {
408+
//weigl: Not necessary is handled within the lexer
409+
// var in = CharStreams.fromString(text.replaceAll("\\r\\n?", "\n"));
410+
411+
var lexer = ParsingFacade.createLexer(stream);
412+
//weigl: Should not be necessary
413+
// lexer.setTokenFactory(new CommonTokenFactory(true));
389414

390415
CommonTokenStream tokens = new CommonTokenStream(lexer);
391416
tokens.fill();
392417

393418
KeYParser parser = new KeYParser(tokens);
394-
KeYParser.FileContext ctx = parser.file();
395-
if (parser.getNumberOfSyntaxErrors() > 0) {
396-
return null;
397-
}
419+
parser.removeErrorListeners();
420+
parser.addErrorListener(parser.getErrorReporter());
398421

422+
KeYParser.FileContext ctx = parser.file();
399423
KeYFileFormatter formatter = new KeYFileFormatter(tokens);
400424
formatter.visitFile(ctx);
401-
var formatted = formatter.output.toString().trim() + "\n";
402-
return formatted.replaceAll("\n", System.lineSeparator());
425+
return formatter.output.toString().trim() + "\n";
403426
}
404427
}

‎key.format/src/main/java/de/uka/ilkd/key/nparser/format/KeyFormatFacade.java‎

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
package de.uka.ilkd.key.nparser.format;/* 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+
5+
import de.uka.ilkd.key.util.parsing.SyntaxErrorReporter;
6+
import org.antlr.v4.runtime.CharStreams;
7+
import org.slf4j.Logger;
8+
import org.slf4j.LoggerFactory;
9+
import picocli.CommandLine;
10+
import picocli.CommandLine.Command;
11+
import picocli.CommandLine.Parameters;
12+
13+
import java.io.FileNotFoundException;
14+
import java.io.IOException;
15+
import java.nio.file.Files;
16+
import java.nio.file.Path;
17+
import java.util.ArrayList;
18+
import java.util.Collections;
19+
import java.util.List;
20+
import java.util.concurrent.Callable;
21+
import java.util.stream.Collectors;
22+
import java.util.stream.Stream;
23+
24+
import static de.uka.ilkd.key.nparser.format.KeYFileFormatter.format;
25+
26+
/**
27+
* The program interface of the KeY formatter utility.
28+
* You can run it using Gradle: {@code gradle :key.format:run}
29+
*
30+
* @author Alexander Weigl
31+
*/
32+
public class KeyFormatFacade {
33+
/**
34+
*
35+
*/
36+
public static boolean CONVERGENT_CHECK = false;
37+
38+
public static final Logger LOGGER = LoggerFactory.getLogger(KeyFormatFacade.class);
39+
40+
/**
41+
* Reformat the given path and store it in {@code output}.
42+
* <p>
43+
* {@code} output is not written when an error occurred.
44+
*
45+
* @param input source file
46+
* @param output target file
47+
* @throws IOException file not found or not readable.
48+
*/
49+
public static void formatSingleFile(Path input, Path output) throws IOException {
50+
var content = CharStreams.fromPath(input);
51+
try {
52+
var formatted = format(content);
53+
54+
if (CONVERGENT_CHECK) {
55+
var secondInput = CharStreams.fromString(formatted);
56+
try {
57+
if (!formatted.equals(format(secondInput))) {
58+
LOGGER.error("{} | Formatter is not convergent on ", input);
59+
}
60+
} catch (SyntaxErrorReporter.ParserException e) {
61+
LOGGER.error("{} | Formatter produces rubbish", input);
62+
}
63+
}
64+
65+
Files.writeString(output, formatted);
66+
} catch (SyntaxErrorReporter.ParserException e) {
67+
System.err.println(input + " | Failed to format");
68+
}
69+
}
70+
71+
private static void formatSingleFileTo(Path input, Path outputDir) throws IOException {
72+
var output = outputDir.resolve(input.getFileName());
73+
formatSingleFile(input, output);
74+
}
75+
76+
public static boolean checkFile(Path file) throws IOException {
77+
var formatted = format(CharStreams.fromPath(file));
78+
var content = Files.readString(file);
79+
return !content.equals(formatted);
80+
}
81+
82+
private static List<Path> expandPath(Path path) throws IOException {
83+
if (!Files.exists(path)) {
84+
throw new FileNotFoundException();
85+
}
86+
87+
if (Files.isDirectory(path)) {
88+
try (Stream<Path> s = Files.walk(path)) {
89+
return s.collect(Collectors.toList());
90+
}
91+
} else {
92+
return Collections.singletonList(path);
93+
}
94+
}
95+
96+
@Command(name = "format")
97+
private static class Format implements Callable<Integer> {
98+
@Parameters(arity = "1..*", description = "", paramLabel = "PATH")
99+
private List<Path> paths = new ArrayList<>();
100+
101+
@Override
102+
public Integer call() {
103+
for (var path : paths) {
104+
try {
105+
var files = expandPath(path);
106+
for (Path file : files) {
107+
try {
108+
formatSingleFileTo(file, file);
109+
} catch (SyntaxErrorReporter.ParserException e) {
110+
LOGGER.error("{} | Parser error", path, e);
111+
}
112+
}
113+
} catch (IOException e) {
114+
LOGGER.error("{} | could not read directory", path, e);
115+
}
116+
}
117+
return 0;
118+
}
119+
}
120+
121+
@Command(name = "check")
122+
private static class Check implements Callable<Integer> {
123+
@Parameters(arity = "1..*", description = "", paramLabel = "PATH")
124+
private List<Path> paths = new ArrayList<>();
125+
126+
@Override
127+
public Integer call() {
128+
var valid = true;
129+
for (Path path : paths) {
130+
try {
131+
for (Path file : expandPath(path)) {
132+
try {
133+
if (checkFile(file)) {
134+
valid = false;
135+
LOGGER.warn("{} | File is not formatted properly", path);
136+
}
137+
} catch (SyntaxErrorReporter.ParserException e) {
138+
LOGGER.error("{} | Syntax errors in file", path, e);
139+
}
140+
}
141+
} catch (IOException e) {
142+
LOGGER.error("{} | could not read directory", path, e);
143+
}
144+
}
145+
return valid ? 0 : 1;
146+
}
147+
}
148+
149+
@Command()
150+
private static class Cmd {
151+
}
152+
153+
public static void main(String[] args) {
154+
int exitCode = new CommandLine(new Cmd())
155+
.addSubcommand(new Format())
156+
.addSubcommand(new Check())
157+
.execute(args);
158+
System.exit(exitCode);
159+
}
160+
}

0 commit comments

Comments
 (0)