Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -270,7 +270,7 @@ public static VerifierOptions getVerifierOptions(JVerifyTest annotation, Positio
true,
annotation.verifyByDefault(),
annotation.continueOnErrors(),
positionFilter, true, false
positionFilter, true, false, null
);
}

Expand Down
8 changes: 7 additions & 1 deletion verifier/src/main/java/org/strata/jverify/verifier/Main.java
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,12 @@ class AppCommand implements Callable<Integer> {
@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());
Expand Down Expand Up @@ -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 {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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> T time(String name, Supplier<T> supply) {
if (!shouldTrackTime) {
return supply.get();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 ".<n>.<phase>.<ext>")
// 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 "<dir>/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", () -> {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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());
}
}
Loading