Skip to content

Commit c13fe2a

Browse files
FedericoPonziFedericoPonzi
committed
Enforce spec validation by default, fixes #14 
1 parent f70f571 commit c13fe2a

File tree

6 files changed

+414
-46
lines changed

6 files changed

+414
-46
lines changed

‎src/main/java/me/fponzi/tlaplusformatter/AstComparator.java‎

Lines changed: 183 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
1+
package me.fponzi.tlaplusformatter;
2+
3+
import tla2sany.st.TreeNode;
4+
5+
import java.util.ArrayList;
6+
import java.util.Collections;
7+
import java.util.List;
8+
9+
/**
10+
* Compares two SANY parse trees for structural equivalence.
11+
* Used to verify that formatting preserves the AST structure.
12+
*/
13+
public final class AstComparator {
14+
15+
private AstComparator() {}
16+
17+
/**
18+
* Result of an AST comparison. Contains mismatch details if the trees differ.
19+
*/
20+
public static final class Result {
21+
private final boolean match;
22+
private final String description;
23+
private final List<String> nodePath;
24+
25+
private Result(boolean match, String description, List<String> nodePath) {
26+
this.match = match;
27+
this.description = description;
28+
this.nodePath = nodePath;
29+
}
30+
31+
/** Creates a failure result for cases where re-parsing itself fails. */
32+
public Result(String description) {
33+
this(false, description, Collections.emptyList());
34+
}
35+
36+
static Result ok() {
37+
return new Result(true, null, Collections.emptyList());
38+
}
39+
40+
static Result mismatch(String description, List<String> path) {
41+
return new Result(false, description, path);
42+
}
43+
44+
public boolean isMatch() {
45+
return match;
46+
}
47+
48+
public String getDescription() {
49+
return description;
50+
}
51+
52+
/** Path from root to the mismatched node, e.g. ["Module", "OpDef", "InfixExpr"]. */
53+
public List<String> getNodePath() {
54+
return Collections.unmodifiableList(nodePath);
55+
}
56+
57+
public String formatDiagnostic() {
58+
if (match) return "ASTs match.";
59+
StringBuilder sb = new StringBuilder();
60+
sb.append("AST verification failed:\n");
61+
sb.append(" ").append(description).append("\n");
62+
sb.append(" Node path: ").append(String.join(" -> ", nodePath)).append("\n");
63+
return sb.toString();
64+
}
65+
}
66+
67+
/**
68+
* Compare two parse trees for structural equivalence.
69+
* Compares node kinds, zero/one children, and pre-comments.
70+
*/
71+
public static Result compare(TreeNode original, TreeNode formatted) {
72+
List<String> path = new ArrayList<>();
73+
return compareRecursive(original, formatted, path);
74+
}
75+
76+
private static Result compareRecursive(TreeNode n1, TreeNode n2, List<String> path) {
77+
String nodeLabel = nodeLabel(n1);
78+
path.add(nodeLabel);
79+
80+
// Compare zero() children
81+
if (n1.zero() != null) {
82+
if (n2.zero() == null) {
83+
return Result.mismatch(
84+
"Node zero[] is null in formatted AST but not in original. Node: " + n1.getImage(),
85+
new ArrayList<>(path));
86+
}
87+
if (n1.zero().length != n2.zero().length) {
88+
return Result.mismatch(
89+
"Node zero[] length mismatch: expected " + n1.zero().length
90+
+ " but found " + n2.zero().length
91+
+ ". Node: " + n1.getImage(),
92+
new ArrayList<>(path));
93+
}
94+
for (int i = 0; i < n1.zero().length; i++) {
95+
Result childResult = compareRecursive(n1.zero()[i], n2.zero()[i], path);
96+
if (!childResult.isMatch()) {
97+
return childResult;
98+
}
99+
}
100+
}
101+
102+
// Compare one() children
103+
if (n1.one() != null) {
104+
if (n2.one() == null) {
105+
return Result.mismatch(
106+
"Node one[] is null in formatted AST but not in original. Node: " + n1.getImage(),
107+
new ArrayList<>(path));
108+
}
109+
if (n1.one().length != n2.one().length) {
110+
return Result.mismatch(
111+
"Node one[] length mismatch: expected " + n1.one().length
112+
+ " but found " + n2.one().length
113+
+ ". Node: " + n1.getImage(),
114+
new ArrayList<>(path));
115+
}
116+
for (int i = 0; i < n1.one().length; i++) {
117+
Result childResult = compareRecursive(n1.one()[i], n2.one()[i], path);
118+
if (!childResult.isMatch()) {
119+
return childResult;
120+
}
121+
}
122+
}
123+
124+
// Compare pre-comments
125+
Result commentResult = compareComments(n1, n2, path);
126+
if (!commentResult.isMatch()) {
127+
return commentResult;
128+
}
129+
130+
// Compare node kind
131+
if (n1.getKind() != n2.getKind()) {
132+
return Result.mismatch(
133+
"Node kind mismatch: expected " + n1.getKind() + " (" + n1.getImage() + ")"
134+
+ " but found " + n2.getKind() + " (" + n2.getImage() + ")",
135+
new ArrayList<>(path));
136+
}
137+
138+
path.remove(path.size() - 1);
139+
return Result.ok();
140+
}
141+
142+
private static Result compareComments(TreeNode n1, TreeNode n2, List<String> path) {
143+
boolean has1 = n1.getPreComments() != null && n1.getPreComments().length > 0;
144+
boolean has2 = n2.getPreComments() != null && n2.getPreComments().length > 0;
145+
if (has1 != has2) {
146+
return Result.mismatch(
147+
"Comment presence mismatch on node: " + n1.getHumanReadableImage()
148+
+ ". Expected comments: " + has1 + ", found: " + has2,
149+
new ArrayList<>(path));
150+
}
151+
if (has1) {
152+
if (n1.getPreComments().length != n2.getPreComments().length) {
153+
return Result.mismatch(
154+
"Comment count mismatch on node: " + n1.getHumanReadableImage()
155+
+ ". Expected " + n1.getPreComments().length
156+
+ " but found " + n2.getPreComments().length,
157+
new ArrayList<>(path));
158+
}
159+
for (int i = 0; i < n1.getPreComments().length; i++) {
160+
if (!n1.getPreComments()[i].equals(n2.getPreComments()[i])) {
161+
return Result.mismatch(
162+
"Comment content mismatch on node: " + n1.getHumanReadableImage()
163+
+ ". Expected: \"" + n1.getPreComments()[i]
164+
+ "\" but found: \"" + n2.getPreComments()[i] + "\"",
165+
new ArrayList<>(path));
166+
}
167+
}
168+
}
169+
return Result.ok();
170+
}
171+
172+
private static String nodeLabel(TreeNode node) {
173+
String hri = node.getHumanReadableImage();
174+
if (hri != null && !hri.isEmpty()) {
175+
return hri + " (kind=" + node.getKind() + ")";
176+
}
177+
String image = node.getImage();
178+
if (image != null && !image.isEmpty()) {
179+
return image + " (kind=" + node.getKind() + ")";
180+
}
181+
return "kind=" + node.getKind();
182+
}
183+
}

‎src/main/java/me/fponzi/tlaplusformatter/Main.java‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package me.fponzi.tlaplusformatter;
22

33
import ch.qos.logback.classic.LoggerContext;
4+
import me.fponzi.tlaplusformatter.exceptions.AstVerificationException;
45
import me.fponzi.tlaplusformatter.exceptions.SanyFrontendException;
56
import org.apache.commons.cli.*;
67
import org.slf4j.Logger;
@@ -27,6 +28,8 @@ public static int mainWrapper(String[] args) {
2728
options.addOption(VERBOSITY_OPTION, "verbosity", true, "Set the verbosity level (ERROR, WARN, *INFO, DEBUG)");
2829
options.addOption("w", "width", true, "Set the target line width for formatting (default: 80)");
2930
options.addOption("i", "indent", true, "Set the number of spaces for indentation (default: 4)");
31+
options.addOption(null, "skip-ast-verification", false,
32+
"Skip AST verification after formatting (not recommended, verification is enabled by default)");
3033

3134
CommandLine cmd;
3235
try {
@@ -90,7 +93,20 @@ public static int mainWrapper(String[] args) {
9093
}
9194

9295
FormatConfig config = new FormatConfig(lineWidth, indentSize);
93-
TLAPlusFormatter formatter = new TLAPlusFormatter(inputFile, config);
96+
boolean verifyAst = !cmd.hasOption("skip-ast-verification");
97+
TLAPlusFormatter formatter;
98+
try {
99+
formatter = new TLAPlusFormatter(inputFile, config, verifyAst);
100+
} catch (AstVerificationException e) {
101+
// AST verification failed: print original input to stdout, diagnostics to stderr
102+
System.out.print(Files.readString(inputFile.toPath()));
103+
System.err.println("AST verification failed after formatting.");
104+
System.err.println("tlaplus-formatter version: " + VersionInfo.getFullVersion());
105+
System.err.println(e.getResult().formatDiagnostic());
106+
System.err.println("This is a bug in the formatter. Please report it at:");
107+
System.err.println(" https://github.com/FedericoPonzi/tlaplus-formatter/issues");
108+
return 1;
109+
}
94110
String formattedOutput = formatter.getOutput();
95111

96112
if (remainingArgs.length == 2) {

‎src/main/java/me/fponzi/tlaplusformatter/TLAPlusFormatter.java‎

Lines changed: 67 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package me.fponzi.tlaplusformatter;
22

33
import com.opencastsoftware.prettier4j.Doc;
4+
import me.fponzi.tlaplusformatter.exceptions.AstVerificationException;
45
import me.fponzi.tlaplusformatter.exceptions.SanyFrontendException;
56
import org.slf4j.Logger;
67
import org.slf4j.LoggerFactory;
@@ -23,14 +24,20 @@ public final class TLAPlusFormatter {
2324
private final TlaDocBuilder docBuilder;
2425
private String output;
2526
private final FormatConfig config;
27+
private final boolean verifyAst;
2628

2729
public TLAPlusFormatter(File specPath) throws IOException, SanyFrontendException {
28-
this(specPath, new FormatConfig());
30+
this(specPath, new FormatConfig(), true);
2931
}
3032

3133
public TLAPlusFormatter(File specPath, FormatConfig config) throws IOException, SanyFrontendException {
34+
this(specPath, config, true);
35+
}
36+
37+
public TLAPlusFormatter(File specPath, FormatConfig config, boolean verifyAst) throws IOException, SanyFrontendException {
3238
this.docBuilder = new TlaDocBuilder(config);
3339
this.config = config.copy();
40+
this.verifyAst = verifyAst;
3441
this.root = SANYWrapper.load(specPath);
3542
this.spec = specPath;
3643

@@ -52,11 +59,15 @@ public String getOutput() {
5259
* @throws IOException
5360
*/
5461
public TLAPlusFormatter(String spec) throws IOException, SanyFrontendException {
55-
this(storeToTmp(spec), new FormatConfig());
62+
this(storeToTmp(spec), new FormatConfig(), true);
5663
}
5764

5865
public TLAPlusFormatter(String spec, FormatConfig config) throws IOException, SanyFrontendException {
59-
this(storeToTmp(spec), config);
66+
this(storeToTmp(spec), config, true);
67+
}
68+
69+
public TLAPlusFormatter(String spec, FormatConfig config, boolean verifyAst) throws IOException, SanyFrontendException {
70+
this(storeToTmp(spec), config, verifyAst);
6071
}
6172

6273
private void format() throws IOException {
@@ -70,6 +81,59 @@ private void format() throws IOException {
7081
this.output = extraSections[0] +
7182
moduleDoc.render(this.config.getLineWidth()) +
7283
extraSections[1];
84+
85+
if (verifyAst) {
86+
verifyAstPreservation();
87+
}
88+
}
89+
90+
/**
91+
* Re-parses the formatted output and compares its AST to the original.
92+
* Throws AstVerificationException if the ASTs differ.
93+
*/
94+
private void verifyAstPreservation() throws IOException {
95+
File tmpFile = null;
96+
try {
97+
// Write to the same directory as the original spec so SANY can resolve EXTENDS
98+
tmpFile = storeForVerification(this.output, this.spec);
99+
TreeNode formattedRoot = SANYWrapper.load(tmpFile);
100+
AstComparator.Result result = AstComparator.compare(this.root, formattedRoot);
101+
if (!result.isMatch()) {
102+
throw new AstVerificationException(result);
103+
}
104+
} catch (SanyFrontendException e) {
105+
throw new AstVerificationException(new AstComparator.Result(
106+
"Formatted output failed to parse: " + e.getMessage()));
107+
} finally {
108+
if (tmpFile != null && !tmpFile.delete()) {
109+
LOG.debug("Failed to delete temporary verification file: {}", tmpFile);
110+
}
111+
}
112+
}
113+
114+
/**
115+
* Writes spec content to a temp directory with copies of sibling .tla files,
116+
* so that SANY can resolve EXTENDS to sibling modules.
117+
*/
118+
private static File storeForVerification(String content, File originalSpec) throws IOException {
119+
File parentDir = originalSpec.getAbsoluteFile().getParentFile();
120+
File tmpDir = java.nio.file.Files.createTempDirectory("sany-verify").toFile();
121+
// Copy sibling .tla files so SANY can resolve EXTENDS
122+
File[] siblings = parentDir.listFiles((dir, name) -> name.endsWith(".tla"));
123+
if (siblings != null) {
124+
for (File sibling : siblings) {
125+
java.nio.file.Files.copy(
126+
sibling.toPath(),
127+
new File(tmpDir, sibling.getName()).toPath(),
128+
java.nio.file.StandardCopyOption.REPLACE_EXISTING);
129+
}
130+
}
131+
// Write the formatted output with the original filename (SANY requires module name = filename)
132+
File verifyFile = new File(tmpDir, originalSpec.getName());
133+
try (java.io.FileWriter writer = new java.io.FileWriter(verifyFile, StandardCharsets.UTF_8)) {
134+
writer.write(content);
135+
}
136+
return verifyFile;
73137
}
74138

75139
static String getModuleName(String spec) {

‎src/main/java/me/fponzi/tlaplusformatter/exceptions/AstVerificationException.java‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
package me.fponzi.tlaplusformatter.exceptions;
2+
3+
import me.fponzi.tlaplusformatter.AstComparator;
4+
5+
/**
6+
* Thrown when the formatted output's AST does not match the original AST.
7+
*/
8+
public class AstVerificationException extends RuntimeException {
9+
private final AstComparator.Result result;
10+
11+
public AstVerificationException(AstComparator.Result result) {
12+
super(result.formatDiagnostic());
13+
this.result = result;
14+
}
15+
16+
public AstComparator.Result getResult() {
17+
return result;
18+
}
19+
}

0 commit comments

Comments
 (0)