diff --git a/test-engine/src/main/java/org/strata/jverify/testengine/JVerifyTestEngine.java b/test-engine/src/main/java/org/strata/jverify/testengine/JVerifyTestEngine.java index e341d495f..f9636bc54 100644 --- a/test-engine/src/main/java/org/strata/jverify/testengine/JVerifyTestEngine.java +++ b/test-engine/src/main/java/org/strata/jverify/testengine/JVerifyTestEngine.java @@ -270,7 +270,7 @@ public static VerifierOptions getVerifierOptions(JVerifyTest annotation, Positio true, annotation.verifyByDefault(), annotation.continueOnErrors(), - positionFilter, true, false + positionFilter, true, false, null ); } diff --git a/verifier/src/main/java/org/strata/jverify/verifier/Main.java b/verifier/src/main/java/org/strata/jverify/verifier/Main.java index 982cdd9bd..29f98eec5 100644 --- a/verifier/src/main/java/org/strata/jverify/verifier/Main.java +++ b/verifier/src/main/java/org/strata/jverify/verifier/Main.java @@ -70,6 +70,12 @@ class AppCommand implements Callable { @Option(names = "--track-time", description = "") private boolean trackTime; + @Option(names = "--keep-all-files", paramLabel = "DIR", + description = "Keep the intermediate Strata IR (Laurel and Core programs emitted after each " + + "pipeline phase) in this directory. The directory is created if it does not exist. " + + "Useful for debugging verification.") + private Path keepAllFilesDir; + @Override public Integer call() throws IOException { var writer = new PrintWriter(spec.commandLine().getOut()); @@ -97,7 +103,7 @@ public Integer call() throws IOException { var verifierOptions = new VerifierOptions(writer, workingDirectory, strataPath, classpathEntries, emitLaurel, emitLaurel != null, showRanges, contractPathEntries, paths, verifyByDefault, false, - positionFilter, verbose, trackTime); + positionFilter, verbose, trackTime, keepAllFilesDir); return verifierOptions.time("Calling Driver.verifyJavaPaths", () -> { try { diff --git a/verifier/src/main/java/org/strata/jverify/verifier/VerifierOptions.java b/verifier/src/main/java/org/strata/jverify/verifier/VerifierOptions.java index c94dafc3a..8f076d3ce 100644 --- a/verifier/src/main/java/org/strata/jverify/verifier/VerifierOptions.java +++ b/verifier/src/main/java/org/strata/jverify/verifier/VerifierOptions.java @@ -22,7 +22,8 @@ public record VerifierOptions(PrintWriter outWriter, boolean continueOnErrors, @Nullable PositionFilter positionFilter, boolean verbose, - boolean shouldTrackTime) { + boolean shouldTrackTime, + @Nullable Path keepAllFilesDir) { public T time(String name, Supplier supply) { if (!shouldTrackTime) { return supply.get(); diff --git a/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java b/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java index c5d92af78..be3d0157b 100644 --- a/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java +++ b/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java @@ -116,9 +116,25 @@ public JVerifyResults verifyJavaFiles( } public JVerifyResults runVerifier(FilesMap filesMap, IonValue serializedProgram) { - var processBuilder = new ProcessBuilder( + var command = new ArrayList<>(List.of( "lake", "exe", "-q", "strata", "laurelAnalyzeBinary", "--solver", "z3" - ); + )); + // Forward --keep-all-files so Strata writes the intermediate Laurel and Core IR for + // debugging. Strata treats the value as a path *prefix* (it appends "...") + // and creates the prefix's parent directory. We resolve the user-provided directory to an + // absolute path (the process runs from the StrataCLI subdirectory, so a relative path would + // otherwise be interpreted relative to that) and use "/program" as the prefix, so every + // emitted file lands inside the requested folder. + if (verifierOptions.keepAllFilesDir() != null) { + var prefix = verifierOptions.workingDirectory() + .resolve(verifierOptions.keepAllFilesDir()) + .resolve("program") + .toAbsolutePath() + .normalize(); + command.add("--keep-all-files"); + command.add(prefix.toString()); + } + var processBuilder = new ProcessBuilder(command); // The `strata` executable lives in the StrataCLI subpackage, so `lake` must be invoked from there. processBuilder.directory(verifierOptions.backendPath().resolve("StrataCLI").toFile()); return verifierOptions.time("Running Strata", () -> { diff --git a/verifier/src/test/java/org/strata/jverify/verifier/EmitLaurelWorkflowTest.java b/verifier/src/test/java/org/strata/jverify/verifier/EmitLaurelWorkflowTest.java index 0fa9231dd..887400212 100644 --- a/verifier/src/test/java/org/strata/jverify/verifier/EmitLaurelWorkflowTest.java +++ b/verifier/src/test/java/org/strata/jverify/verifier/EmitLaurelWorkflowTest.java @@ -104,6 +104,7 @@ private static VerifierOptions withEmit(VerifierOptions base, Path emit, boolean base.continueOnErrors(), base.positionFilter(), base.verbose(), - base.shouldTrackTime()); + base.shouldTrackTime(), + base.keepAllFilesDir()); } }