From 9ba6192fbf17af562a9d6c778dd775db4e7d1373 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Thu, 15 Oct 2026 10:28:43 +0000 Subject: [PATCH] Emit YAML violation witnesses (format 2.3) next to GraphML SV-COMP 2027 requires Java violation witnesses in the YAML format, version 2.3. WitnessCreator now writes witness.yml with one violation_sequence: a function_return waypoint per recorded Verifier.nondet*() value (constraint `\result == `, location at the closing parenthesis of the call) and a final target waypoint at the violating statement. witness.graphml is still written for the validators that consume the legacy format. - New marker fields from the executor: call index on the line, type descriptor and source file (legacy 4-field markers still parse); new [WITNESS_TARGET] marker carrying the uncaught throwable's stack trace, resolved to the innermost frame inside the task sources. - Columns come from the sources: closing `)` of the n-th nondet call on the line, `assert`/`throw`/first token of the target statement. - Literals per type: L suffix only when needed, char literals, f suffix for floats, NaN/Infinity via Float/Double, strings via `\result.equals("...")` with Java escaping. - CLI: --input (inputs as given, listed with sha256 hashes), --property (specification), --out, --producer-version; the legacy positional form keeps working. Templates are found next to the jar. - JUnit tests for literals, markers, source resolution and the writer. Co-Authored-By: Claude Opus 5.5 --- README.md | 30 +- build.gradle | 6 + src/main/java/App.java | 414 +++++++++++++++----- src/main/java/witness/JavaLiterals.java | 160 ++++++++ src/main/java/witness/SourceFiles.java | 203 ++++++++++ src/main/java/witness/TargetMarker.java | 90 +++++ src/main/java/witness/ValueMarker.java | 119 ++++++ src/main/java/witness/YamlWitness.java | 176 +++++++++ src/test/java/AppTest.java | 183 +++++++++ src/test/java/witness/JavaLiteralsTest.java | 77 ++++ src/test/java/witness/MarkerTest.java | 70 ++++ 11 files changed, 1437 insertions(+), 91 deletions(-) create mode 100644 src/main/java/witness/JavaLiterals.java create mode 100644 src/main/java/witness/SourceFiles.java create mode 100644 src/main/java/witness/TargetMarker.java create mode 100644 src/main/java/witness/ValueMarker.java create mode 100644 src/main/java/witness/YamlWitness.java create mode 100644 src/test/java/AppTest.java create mode 100644 src/test/java/witness/JavaLiteralsTest.java create mode 100644 src/test/java/witness/MarkerTest.java diff --git a/README.md b/README.md index bc9cd54..a083f26 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,33 @@ # WitnessCreator -WitnessCreator creates SV-COMP GraphML violation witnesses from SWAT witness -markers. +WitnessCreator creates SV-COMP violation witnesses from SWAT witness markers: + +- `witness.yml` in the [YAML witness format 2.3](https://gitlab.com/sosy-lab/benchmarking/sv-witnesses) + for Java (one `violation_sequence` with a `function_return` waypoint per + `Verifier.nondet*()` value and a final `target` waypoint at the violating statement), +- `witness.graphml` in the legacy GraphML format, for validators that still consume it. + +## Usage + +```sh +java -jar build/libs/WitnessCreator.jar [] \ + [--input ]... [--property ] [--out ] [--producer-version ] +``` + +- ``: base64 of the SWAT output lines carrying `[WITNESS]` (one per nondet value: + `value@@@line@@@class@@@method@@@callIndex@@@typeDesc@@@sourceFile`) and `[WITNESS_TARGET]` + (the uncaught throwable with its stack trace) markers. An empty string yields the default + violation witness without waypoints. +- `--input`: the task's input files or directories exactly as given to the verifier. They are + searched for the sources (`.java`) and listed, with their SHA-256 hashes, in the witness. +- `--property`: the property file, its content becomes the witness' `specification`. +- `--out`: the output directory (default: ``, the legacy positional source directory). +- `--producer-version`: written to `metadata.producer.version`. + +Columns are derived from the sources: a `function_return` waypoint points to the closing +parenthesis of the `callIndex`-th nondet call on its line, the `target` waypoint to the start of +the violating statement (`assert`, `throw`, or the first token of the innermost statement in the +task sources that appears in the stack trace). ## Build diff --git a/build.gradle b/build.gradle index 0429df6..2b5f58d 100644 --- a/build.gradle +++ b/build.gradle @@ -14,6 +14,8 @@ repositories { dependencies { implementation 'org.antlr:ST4:4.3.4' + testImplementation 'org.junit.jupiter:junit-jupiter:5.10.2' + testRuntimeOnly 'org.junit.platform:junit-platform-launcher' } java { @@ -22,6 +24,10 @@ java { } } +tasks.named('test') { + useJUnitPlatform() +} + application { mainClass = 'App' } diff --git a/src/main/java/App.java b/src/main/java/App.java index 37f7d43..a9e153a 100755 --- a/src/main/java/App.java +++ b/src/main/java/App.java @@ -1,144 +1,381 @@ -import java.io.BufferedReader; import java.io.IOException; -import java.io.InputStream; -import java.io.InputStreamReader; +import java.net.URISyntaxException; +import java.nio.charset.StandardCharsets; import java.nio.file.Files; +import java.nio.file.Path; import java.nio.file.Paths; import java.util.ArrayList; import java.util.Base64; -import java.util.LinkedList; import java.util.List; +import java.util.Optional; +import java.util.regex.Matcher; +import java.util.regex.Pattern; import org.stringtemplate.v4.ST; import org.stringtemplate.v4.STGroup; import org.stringtemplate.v4.STRawGroupDir; +import witness.JavaLiterals; +import witness.SourceFiles; +import witness.SourceFiles.InputFile; +import witness.TargetMarker; +import witness.ValueMarker; import witness.WitnessAssumption; import witness.WitnessEdge; import witness.WitnessNode; +import witness.YamlWitness; +import witness.YamlWitness.Waypoint; +/** + * Creates SV-COMP violation witnesses from SWAT's witness markers. + * + * 
+ * App <markers> [<dir>] [--input <path>]... [--property <file.prp>] [--out <dir>]
+ *     [--producer-version <version>]
+ *
+ * + *
    + *
  • {@code markers}: base64 of the output lines carrying {@code [WITNESS]} and + * {@code [WITNESS_TARGET]} markers (empty for the default violation witness). + *
  • {@code dir}: legacy positional argument, the directory holding the task sources; also + * the output directory unless {@code --out} is given. + *
  • {@code --input}: the task's input files or directories exactly as given to the verifier, + * used for the source lookup, the witness' {@code input_files} and their hashes. + *
  • {@code --property}: the property file, its content is the witness' specification. + *
+ * + * Writes {@code witness.yml} (format 2.3) and, for the validators still consuming GraphML, + * {@code witness.graphml}. + */ public class App { - public static void main(String[] args) { + private static final String PRODUCER = "SWAT"; + private static final String DEFAULT_SPECIFICATION = "CHECK( init(Main.main()), LTL(G assert) )"; + private static final Pattern NONDET_CALL = Pattern.compile("nondet[A-Za-z0-9_]*\\s*\\("); + private static final Pattern ASSERT_KEYWORD = Pattern.compile("\\bassert\\b"); + private static final Pattern THROW_KEYWORD = Pattern.compile("\\bthrow\\b"); + private final SourceFiles sourceFiles; + private final Path outDir; - String path = args[1]; - System.out.println("source path: " + path); + private App(SourceFiles sourceFiles, Path outDir) { + this.sourceFiles = sourceFiles; + this.outDir = outDir; + } - List witness = new LinkedList<>(); - if(args[0].trim().length() == 0) { - System.out.println("No witness record, assuming default assertion violation"); - (new App()).saveDefaultviolationWitness(path); - } else { - String param = new String(Base64.getDecoder().decode(args[0])); - String[] lines = param.split("\n"); - for (String line : lines) { - line = line.substring(line.indexOf("[WITNESS]") + 10).trim(); - // decode line base64 - byte[] decodedBytes = Base64.getDecoder().decode(line); - line = new String(decodedBytes); - - String[] parts = line.split("@@@"); - if (parts.length != 4) { - System.out.println("Received line:" + line); - throw new RuntimeException("Invalid witness line: " + line); - } + public static void main(String[] args) throws IOException { + List positional = new ArrayList<>(); + List inputs = new ArrayList<>(); + String property = null; + String out = null; + String producerVersion = "unknown"; + for (int i = 0; i < args.length; i++) { + switch (args[i]) { + case "--input" -> inputs.add(args[++i]); + case "--property" -> property = args[++i]; + case "--out" -> out = args[++i]; + case "--producer-version" -> producerVersion = args[++i]; + default -> positional.add(args[i]); + } + } + if (positional.isEmpty()) { + System.err.println( + "Usage: App [] [--input ]... [--property ]" + + " [--out ] [--producer-version ]"); + System.exit(2); + } + String markers = positional.get(0); + String legacyDir = positional.size() > 1 ? positional.get(1) : null; + if (inputs.isEmpty() && legacyDir != null) { + inputs.add(legacyDir); + } + if (out == null) { + out = legacyDir != null ? legacyDir : "."; + } + Path outDir = Paths.get(out); + Files.createDirectories(outDir); + System.out.println("inputs: " + inputs); + System.out.println("output directory: " + outDir); - String value = parts[0].trim(); - int lineNumber = Integer.parseInt(parts[1].trim()); // account for 0-based line numbers - String className = parts[2].trim(); - String description = parts[3].trim(); + SourceFiles sourceFiles = SourceFiles.collect(inputs); + String specification = readSpecification(property); - // Escape XML special characters in scope to avoid XML parse errors - // (e.g., contains angle brackets that break XML parsing) - String scope = "L" + className + ";." + description; - scope = scope.replace("&", "&").replace("<", "<").replace(">", ">"); - witness.add(new WitnessAssumption(value, className + ".java", scope, lineNumber)); - } - (new App()).checkAndSaveWitness(path, witness); + List values = new ArrayList<>(); + TargetMarker target = null; + if (!markers.trim().isEmpty()) { + String decoded = new String(Base64.getDecoder().decode(markers.trim()), StandardCharsets.UTF_8); + for (String line : decoded.split("\n")) { + int idx = line.indexOf("[WITNESS_TARGET]"); + if (idx >= 0) { + target = TargetMarker.parse(decodePayload(line.substring(idx + "[WITNESS_TARGET]".length()))); + continue; + } + idx = line.indexOf("[WITNESS]"); + if (idx >= 0) { + values.add(ValueMarker.parse(decodePayload(line.substring(idx + "[WITNESS]".length())))); + } } } + if (values.isEmpty()) { + System.out.println("No witness values recorded, assuming default violation"); + } + if (target == null) { + System.out.println("No witness target recorded, the witness has no target waypoint"); + } + App app = new App(sourceFiles, outDir); + app.saveYamlWitness(values, target, specification, producerVersion); + app.saveGraphmlWitness(values); + } + private static String decodePayload(String base64) { + return new String(Base64.getDecoder().decode(base64.trim()), StandardCharsets.UTF_8); + } - private void saveDefaultviolationWitness(String path){ - STGroup group = new STRawGroupDir("witnesses", '$','$'); - ST st = group.getInstanceOf("default_violation"); - String result = st.render(); + private static String readSpecification(String property) { + if (property == null) { + System.out.println("No property file given, assuming specification: " + DEFAULT_SPECIFICATION); + return DEFAULT_SPECIFICATION; + } try { - System.out.println("Writing default violation witness to file: " + path + "/" + "witness.graphml"); - Files.write(Paths.get(path + "/" + "witness.graphml"), result.getBytes()); + String spec = Files.readString(Paths.get(property), StandardCharsets.UTF_8).trim(); + if (!spec.isEmpty()) { + return spec; + } } catch (IOException e) { - System.err.println("Error writing witness to file: " + e.getMessage()); + System.out.println("Could not read property file " + property + ": " + e.getMessage()); + } + System.out.println("Assuming specification: " + DEFAULT_SPECIFICATION); + return DEFAULT_SPECIFICATION; + } + + // ------------------------------------------------------------------ + // YAML witness (format 2.3) + // ------------------------------------------------------------------ + + private void saveYamlWitness( + List values, TargetMarker target, String specification, String producerVersion) + throws IOException { + YamlWitness witness = new YamlWitness(PRODUCER, producerVersion, specification, sourceFiles); + + for (ValueMarker value : values) { + Optional file = sourceFiles.resolve(value.getClassName(), value.getSourceFile()); + String fileName; + Integer column = null; + if (file.isPresent()) { + fileName = file.get().getDisplayPath(); + String loc = file.get().getLine(value.getLine()); + int col = loc == null ? -1 : nondetCallColumn(loc, value.getCallIndex()); + if (col > 0) { + column = col; + } else { + System.out.println( + "Could not locate nondet call " + value.getCallIndex() + " in " + fileName + + ":" + value.getLine() + " (" + loc + ")"); + } + } else { + fileName = fallbackFileName(value.getClassName(), value.getSourceFile()); + System.out.println("Could not find the source of " + value.getClassName() + ", using " + fileName); + } + String constraint = JavaLiterals.resultConstraint(value.getValue(), value.getTypeDesc()); + witness.add(Waypoint.functionReturn(constraint, fileName, value.getLine(), column)); + } + + if (target != null) { + Optional targetWaypoint = targetWaypoint(target); + if (targetWaypoint.isPresent()) { + witness.add(targetWaypoint.get()); + } else { + System.out.println("No stack frame of " + target.getThrowableClass() + + " lies in the task sources: " + target.getFrames()); + } + } + + for (Waypoint wp : witness.getWaypoints()) { + System.out.println("Waypoint: " + wp); } + Path file = outDir.resolve("witness.yml"); + System.out.println("Writing violation witness to file: " + file); + Files.writeString(file, witness.render(), StandardCharsets.UTF_8); } - private void checkAndSaveWitness(String path, List witness) { + /** The innermost stack frame inside the task sources becomes the target. */ + private Optional targetWaypoint(TargetMarker target) { + for (TargetMarker.Frame frame : target.getFrames()) { + if (frame.getLine() < 1) { + continue; + } + Optional file = sourceFiles.resolve(frame.getClassName(), frame.getFileName()); + if (file.isEmpty()) { + continue; + } + String loc = file.get().getLine(frame.getLine()); + if (loc == null) { + System.out.println("Frame " + frame + " is outside of " + file.get().getPath()); + continue; + } + int col = statementColumn(loc, target.isAssertionError()); + return Optional.of( + Waypoint.target(file.get().getDisplayPath(), frame.getLine(), col > 0 ? col : null)); + } + return Optional.empty(); + } - List nodes = new ArrayList<>(); - List edges = new ArrayList<>(); + /** + * The 1-based column of the closing parenthesis of the {@code callIndex}-th nondet call in the + * line, -1 if there is none. + */ + static int nondetCallColumn(String line, int callIndex) { + Matcher m = NONDET_CALL.matcher(line); + int found = 0; + while (m.find()) { + if (found++ < callIndex) { + continue; + } + int open = m.end() - 1; + int depth = 0; + for (int i = open; i < line.length(); i++) { + char c = line.charAt(i); + if (c == '(') { + depth++; + } else if (c == ')') { + depth--; + if (depth == 0) { + return i + 1; + } + } + } + return -1; + } + return -1; + } - int nodeId = 0; - WitnessNode initNode = new WitnessNode(nodeId++); - nodes.add(initNode); - initNode.addData("entry", "true"); - WitnessNode curNode = initNode; + /** + * The 1-based column of the first character of the violating statement on the line: the + * {@code assert} of a failed assertion, the {@code throw} of an explicit throw, otherwise the + * first token that is not a closing brace or an {@code else}. + */ + static int statementColumn(String line, boolean assertion) { + if (assertion) { + Matcher m = ASSERT_KEYWORD.matcher(line); + if (m.find()) { + return m.start() + 1; + } + } + Matcher t = THROW_KEYWORD.matcher(line); + if (t.find()) { + return t.start() + 1; + } + int i = skipWhitespace(line, 0); + while (i < line.length()) { + if (line.charAt(i) == '}' || line.charAt(i) == '{') { + i = skipWhitespace(line, i + 1); + } else if (line.startsWith("else", i) + && (i + 4 == line.length() || !Character.isJavaIdentifierPart(line.charAt(i + 4)))) { + i = skipWhitespace(line, i + 4); + } else { + break; + } + } + return i < line.length() ? i + 1 : -1; + } - for (WitnessAssumption wa : witness) { - String loc = getLineOfCode(path, wa.getClazz(), wa.getLine()); - String assumption = computeAssumption(loc, wa); + private static int skipWhitespace(String line, int i) { + while (i < line.length() && Character.isWhitespace(line.charAt(i))) { + i++; + } + return i; + } - WitnessNode prevNode = curNode; - curNode = new WitnessNode(nodeId++); - nodes.add(curNode); - WitnessEdge edge = new WitnessEdge(prevNode, wa, assumption, curNode); - edges.add(edge); + private static String fallbackFileName(String className, String sourceFile) { + String internal = className.replace('.', '/'); + int slash = internal.lastIndexOf('/'); + String pkgDir = slash < 0 ? "" : internal.substring(0, slash + 1); + if (sourceFile != null && !sourceFile.isEmpty()) { + return pkgDir + sourceFile; } + String simple = internal.substring(slash + 1); + int dollar = simple.indexOf('$'); + return pkgDir + (dollar < 0 ? simple : simple.substring(0, dollar)) + ".java"; + } + + // ------------------------------------------------------------------ + // GraphML witness (legacy format, kept for the GraphML-based validators) + // ------------------------------------------------------------------ + + private void saveGraphmlWitness(List values) { + STGroup group = new STRawGroupDir(templateDir(), '$', '$'); + ST st; + if (values.isEmpty()) { + st = group.getInstanceOf("default_violation"); + } else { + List nodes = new ArrayList<>(); + List edges = new ArrayList<>(); + + int nodeId = 0; + WitnessNode initNode = new WitnessNode(nodeId++); + nodes.add(initNode); + initNode.addData("entry", "true"); + WitnessNode curNode = initNode; + + for (ValueMarker value : values) { + Optional file = sourceFiles.resolve(value.getClassName(), value.getSourceFile()); + String clazz = file.map(InputFile::getRelativePath) + .orElse(fallbackFileName(value.getClassName(), value.getSourceFile())); + String loc = file.map(f -> f.getLine(value.getLine())).orElse(null); + // Escape XML special characters in scope to avoid XML parse errors + // (e.g., contains angle brackets that break XML parsing) + String scope = "L" + value.getClassName() + ";." + value.getMethodDesc(); + scope = scope.replace("&", "&").replace("<", "<").replace(">", ">"); + WitnessAssumption wa = new WitnessAssumption(value.getValue(), clazz, scope, value.getLine()); + String assumption = computeAssumption(loc, wa, value.isString()); - curNode.addData("violation", "true"); + WitnessNode prevNode = curNode; + curNode = new WitnessNode(nodeId++); + nodes.add(curNode); + edges.add(new WitnessEdge(prevNode, wa, assumption, curNode)); + } + curNode.addData("violation", "true"); - STGroup group = new STRawGroupDir("witnesses", '$','$'); - ST st = group.getInstanceOf("witness"); - st.add("nodes", nodes); - st.add("edges", edges); - String result = st.render(); + st = group.getInstanceOf("witness"); + st.add("nodes", nodes); + st.add("edges", edges); + } + Path file = outDir.resolve("witness.graphml"); try { - System.out.println("Writing violation witness to file: " + path + "/" + "witness.graphml"); - Files.write(Paths.get(path + "/" + "witness.graphml"), result.getBytes()); + System.out.println("Writing violation witness to file: " + file); + Files.writeString(file, st.render(), StandardCharsets.UTF_8); } catch (IOException e) { System.out.println("Error writing witness to file: " + e.getMessage()); } } - private String getLineOfCode(String path, String filename, int line) { - String absolutePath = path + "/" + filename; + /** The {@code witnesses} template directory next to the jar, or relative to the cwd. */ + private static String templateDir() { + if (Files.isDirectory(Paths.get("witnesses"))) { + return "witnesses"; + } try { - // Open absolutePath as a stream - InputStream is = Files.newInputStream(Paths.get(absolutePath)); - if (is == null) { - System.out.println("Could not find file: " + absolutePath); - return null; - } - BufferedReader res = new BufferedReader(new InputStreamReader(is)); - String loc = ""; - for (int i = 0; i= Integer.MIN_VALUE && l <= Integer.MAX_VALUE) { + return value; + } + return value + "L"; + } catch (NumberFormatException e) { + return value; + } + } + + private static String floatingConstraint(String value, boolean isFloat) { + String box = isFloat ? "Float" : "Double"; + switch (value) { + case "NaN": + return box + ".isNaN(" + RESULT + ")"; + case "Infinity": + return RESULT + " == " + box + ".POSITIVE_INFINITY"; + case "-Infinity": + return RESULT + " == " + box + ".NEGATIVE_INFINITY"; + default: + break; + } + String literal = value; + try { + // Normalises scientific notation and guarantees a decimal point; BigDecimal has no + // negative zero, so the sign is kept separately + boolean negative = value.startsWith("-"); + literal = new BigDecimal(negative ? value.substring(1) : value).toPlainString(); + if (negative) { + literal = "-" + literal; + } + } catch (NumberFormatException e) { + // keep as is + } + if (!literal.contains(".")) { + literal += ".0"; + } + return RESULT + " == " + literal + (isFloat ? "f" : ""); + } + + /** Char values are recorded as their code point. */ + public static String charLiteral(String codePoint) { + int c; + try { + c = Integer.parseInt(codePoint); + } catch (NumberFormatException e) { + return codePoint; + } + switch (c) { + case '\'': + return "'\\''"; + case '\\': + return "'\\\\'"; + case '\n': + return "'\\n'"; + case '\r': + return "'\\r'"; + case '\t': + return "'\\t'"; + case '\b': + return "'\\b'"; + case '\f': + return "'\\f'"; + default: + break; + } + if (c >= 0x20 && c < 0x7f) { + return "'" + (char) c + "'"; + } + return String.format("'\\u%04x'", c); + } + + public static String stringLiteral(String value) { + StringBuilder sb = new StringBuilder("\""); + for (int i = 0; i < value.length(); i++) { + char c = value.charAt(i); + switch (c) { + case '"': + sb.append("\\\""); + break; + case '\\': + sb.append("\\\\"); + break; + case '\n': + sb.append("\\n"); + break; + case '\r': + sb.append("\\r"); + break; + case '\t': + sb.append("\\t"); + break; + case '\b': + sb.append("\\b"); + break; + case '\f': + sb.append("\\f"); + break; + default: + if (c < 0x20 || c == 0x7f) { + sb.append(String.format("\\u%04x", (int) c)); + } else { + sb.append(c); + } + } + } + return sb.append('"').toString(); + } +} diff --git a/src/main/java/witness/SourceFiles.java b/src/main/java/witness/SourceFiles.java new file mode 100644 index 0000000..bee2b45 --- /dev/null +++ b/src/main/java/witness/SourceFiles.java @@ -0,0 +1,203 @@ +package witness; + +import java.io.IOException; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.security.MessageDigest; +import java.security.NoSuchAlgorithmException; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashSet; +import java.util.List; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Stream; + +/** + * The Java source files of the verification task, as they were given to the verifier (files or + * directories). Resolves classes to their source files and provides line contents and hashes. + */ +public final class SourceFiles { + + /** One input file of the task. */ + public static final class InputFile { + private final String displayPath; + private final Path path; + private final String relativePath; + private List lines; + private String sha256; + + InputFile(String displayPath, Path path, String relativePath) { + this.displayPath = displayPath; + this.path = path; + this.relativePath = relativePath; + } + + /** The path as it is written into the witness (input as given + relative path). */ + public String getDisplayPath() { + return displayPath; + } + + public Path getPath() { + return path; + } + + /** Path relative to the input root it was found in, '/'-separated. */ + public String getRelativePath() { + return relativePath; + } + + public String getFileName() { + return path.getFileName().toString(); + } + + public List getLines() { + if (lines == null) { + try { + lines = Files.readAllLines(path, StandardCharsets.UTF_8); + } catch (IOException e) { + System.out.println("Could not read " + path + ": " + e.getMessage()); + lines = Collections.emptyList(); + } + } + return lines; + } + + /** The 1-based line, or {@code null} if the file does not have it. */ + public String getLine(int lineNumber) { + List l = getLines(); + if (lineNumber < 1 || lineNumber > l.size()) { + return null; + } + return l.get(lineNumber - 1); + } + + public String getSha256() throws IOException { + if (sha256 == null) { + try { + MessageDigest digest = MessageDigest.getInstance("SHA-256"); + byte[] hash = digest.digest(Files.readAllBytes(path)); + StringBuilder sb = new StringBuilder(); + for (byte b : hash) { + sb.append(String.format("%02x", b)); + } + sha256 = sb.toString(); + } catch (NoSuchAlgorithmException e) { + throw new IllegalStateException(e); + } + } + return sha256; + } + } + + private final List files; + + private SourceFiles(List files) { + this.files = Collections.unmodifiableList(files); + } + + /** + * Collects all {@code .java} files of the given inputs. Directories are searched recursively, + * the files are ordered by path inside each input. + */ + public static SourceFiles collect(List inputs) { + List files = new ArrayList<>(); + Set seen = new HashSet<>(); // a file reachable through several inputs is listed once + for (String input : inputs) { + Path root = Paths.get(input); + if (Files.isDirectory(root)) { + String prefix = stripTrailingSlash(input); + try (Stream walk = Files.walk(root)) { + List javaFiles = + walk.filter(Files::isRegularFile) + .filter(p -> p.getFileName().toString().endsWith(".java")) + .sorted() + .toList(); + for (Path p : javaFiles) { + if (seen.add(p.toAbsolutePath().normalize())) { + String rel = toSlashes(root.relativize(p).toString()); + files.add(new InputFile(prefix + "/" + rel, p, rel)); + } + } + } catch (IOException e) { + System.out.println("Could not read input directory " + input + ": " + e.getMessage()); + } + } else if (Files.isRegularFile(root)) { + if (root.getFileName().toString().endsWith(".java") + && seen.add(root.toAbsolutePath().normalize())) { + files.add(new InputFile(toSlashes(input), root, root.getFileName().toString())); + } + } else { + System.out.println("Ignoring missing input: " + input); + } + } + return new SourceFiles(files); + } + + public List getFiles() { + return files; + } + + public boolean isEmpty() { + return files.isEmpty(); + } + + /** + * Finds the source file of a class. + * + * @param className JVM internal ({@code pkg/Outer$Inner}) or dotted ({@code pkg.Outer$Inner}) + * class name + * @param sourceFileName the class' SourceFile attribute, may be empty or {@code null} + */ + public Optional resolve(String className, String sourceFileName) { + String internal = className.replace('.', '/'); + int slash = internal.lastIndexOf('/'); + String pkgDir = slash < 0 ? "" : internal.substring(0, slash); + String simple = slash < 0 ? internal : internal.substring(slash + 1); + int dollar = simple.indexOf('$'); + String outer = dollar < 0 ? simple : simple.substring(0, dollar); + + List fileNames = new ArrayList<>(); + if (sourceFileName != null && !sourceFileName.isEmpty()) { + fileNames.add(sourceFileName); + } + fileNames.add(outer + ".java"); + + // Exact package path first, then any path ending with the package path, then by name only + for (String fileName : fileNames) { + String rel = pkgDir.isEmpty() ? fileName : pkgDir + "/" + fileName; + Optional match = find(f -> f.getRelativePath().equals(rel)); + if (match.isEmpty()) { + match = find(f -> f.getRelativePath().endsWith("/" + rel)); + } + if (match.isPresent()) { + return match; + } + } + for (String fileName : fileNames) { + Optional match = find(f -> f.getFileName().equals(fileName)); + if (match.isPresent()) { + return match; + } + } + return Optional.empty(); + } + + private Optional find(java.util.function.Predicate predicate) { + return files.stream().filter(predicate).findFirst(); + } + + private static String stripTrailingSlash(String s) { + String r = toSlashes(s); + while (r.length() > 1 && r.endsWith("/")) { + r = r.substring(0, r.length() - 1); + } + return r; + } + + private static String toSlashes(String s) { + return s.replace('\\', '/'); + } +} diff --git a/src/main/java/witness/TargetMarker.java b/src/main/java/witness/TargetMarker.java new file mode 100644 index 0000000..a74f253 --- /dev/null +++ b/src/main/java/witness/TargetMarker.java @@ -0,0 +1,90 @@ +package witness; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +/** + * A decoded {@code [WITNESS_TARGET]} marker: the uncaught throwable that ended the violating run + * together with its stack trace (innermost frame first). + * + *

Payload format: {@code throwableClass@@@className@@fileName@@line;className@@fileName@@line;...} + */ +public final class TargetMarker { + private final String throwableClass; + private final List frames; + + public static final class Frame { + private final String className; + private final String fileName; + private final int line; + + Frame(String className, String fileName, int line) { + this.className = className; + this.fileName = fileName; + this.line = line; + } + + /** Fully qualified (dotted) class name. */ + public String getClassName() { + return className; + } + + /** Source file name from the stack trace, empty if unknown. */ + public String getFileName() { + return fileName; + } + + public int getLine() { + return line; + } + + @Override + public String toString() { + return className + "(" + fileName + ":" + line + ")"; + } + } + + private TargetMarker(String throwableClass, List frames) { + this.throwableClass = throwableClass; + this.frames = Collections.unmodifiableList(frames); + } + + public static TargetMarker parse(String payload) { + int idx = payload.indexOf("@@@"); + if (idx < 0) { + throw new IllegalArgumentException("Invalid witness target marker: " + payload); + } + String throwableClass = payload.substring(0, idx).trim(); + List frames = new ArrayList<>(); + String rest = payload.substring(idx + 3).trim(); + if (!rest.isEmpty()) { + for (String frame : rest.split(";")) { + String[] parts = frame.split("@@", -1); + if (parts.length != 3) { + continue; + } + int line; + try { + line = Integer.parseInt(parts[2].trim()); + } catch (NumberFormatException e) { + line = -1; + } + frames.add(new Frame(parts[0].trim(), parts[1].trim(), line)); + } + } + return new TargetMarker(throwableClass, frames); + } + + public String getThrowableClass() { + return throwableClass; + } + + public boolean isAssertionError() { + return "java.lang.AssertionError".equals(throwableClass); + } + + public List getFrames() { + return frames; + } +} diff --git a/src/main/java/witness/ValueMarker.java b/src/main/java/witness/ValueMarker.java new file mode 100644 index 0000000..1abf53d --- /dev/null +++ b/src/main/java/witness/ValueMarker.java @@ -0,0 +1,119 @@ +package witness; + +import java.util.Arrays; +import java.util.Set; + +/** + * A decoded {@code [WITNESS]} marker: one value returned by a {@code Verifier.nondet*()} call. + * + *

Payload format (fields separated by {@code @@@}): + * {@code value@@@line@@@className@@@methodDesc@@@callIndex@@@typeDesc@@@sourceFile}. + * The legacy format {@code value@@@line@@@className@@@methodDesc} is still accepted. Because a + * String value may itself contain the separator, the fields are parsed from the end. + */ +public final class ValueMarker { + private static final String SEPARATOR = "@@@"; + private static final Set TYPE_DESCRIPTORS = + Set.of("Z", "B", "C", "S", "I", "J", "F", "D", "Ljava/lang/String;"); + + private final String value; + private final int line; + private final String className; + private final String methodDesc; + private final int callIndex; + private final String typeDesc; + private final String sourceFile; + + private ValueMarker( + String value, + int line, + String className, + String methodDesc, + int callIndex, + String typeDesc, + String sourceFile) { + this.value = value; + this.line = line; + this.className = className; + this.methodDesc = methodDesc; + this.callIndex = callIndex; + this.typeDesc = typeDesc; + this.sourceFile = sourceFile; + } + + public static ValueMarker parse(String payload) { + String[] parts = payload.split(SEPARATOR, -1); + int n = parts.length; + if (n >= 7 && TYPE_DESCRIPTORS.contains(parts[n - 2].trim()) && isInt(parts[n - 3])) { + return new ValueMarker( + join(parts, n - 6), + Integer.parseInt(parts[n - 6].trim()), + parts[n - 5].trim(), + parts[n - 4].trim(), + Integer.parseInt(parts[n - 3].trim()), + parts[n - 2].trim(), + parts[n - 1].trim()); + } + if (n >= 4 && isInt(parts[n - 3])) { + return new ValueMarker( + join(parts, n - 3), + Integer.parseInt(parts[n - 3].trim()), + parts[n - 2].trim(), + parts[n - 1].trim(), + 0, + null, + ""); + } + throw new IllegalArgumentException("Invalid witness marker: " + payload); + } + + private static String join(String[] parts, int count) { + return String.join(SEPARATOR, Arrays.copyOfRange(parts, 0, count)); + } + + private static boolean isInt(String s) { + try { + Integer.parseInt(s.trim()); + return true; + } catch (NumberFormatException e) { + return false; + } + } + + /** The recorded value as printed by the executor (chars as their code point). */ + public String getValue() { + return value; + } + + public int getLine() { + return line; + } + + /** JVM internal class name of the caller, e.g. {@code pkg/Main$Inner}. */ + public String getClassName() { + return className; + } + + public String getMethodDesc() { + return methodDesc; + } + + /** 0-based index of the call among the nondet calls on the same source line. */ + public int getCallIndex() { + return callIndex; + } + + /** JVM descriptor of the returned type, or {@code null} for legacy markers. */ + public String getTypeDesc() { + return typeDesc; + } + + /** The caller's SourceFile attribute, empty if unknown. */ + public String getSourceFile() { + return sourceFile; + } + + public boolean isString() { + return "Ljava/lang/String;".equals(typeDesc); + } +} diff --git a/src/main/java/witness/YamlWitness.java b/src/main/java/witness/YamlWitness.java new file mode 100644 index 0000000..7298c0f --- /dev/null +++ b/src/main/java/witness/YamlWitness.java @@ -0,0 +1,176 @@ +package witness; + +import java.io.IOException; +import java.time.ZoneOffset; +import java.time.ZonedDateTime; +import java.time.format.DateTimeFormatter; +import java.util.ArrayList; +import java.util.List; +import java.util.UUID; + +/** + * A violation witness in the YAML format, version 2.3, for Java (see + * https://gitlab.com/sosy-lab/benchmarking/sv-witnesses). The witness is a single + * {@code violation_sequence} whose segments each hold one {@code follow} waypoint: one + * {@code function_return} waypoint per recorded {@code Verifier.nondet*()} value and, if the + * violating statement is known, a final {@code target} waypoint. + */ +public final class YamlWitness { + public static final String FORMAT_VERSION = "2.3"; + + /** A follow waypoint. */ + public static final class Waypoint { + private final String type; + private final String constraint; + private final String fileName; + private final int line; + private final Integer column; + + private Waypoint(String type, String constraint, String fileName, int line, Integer column) { + this.type = type; + this.constraint = constraint; + this.fileName = fileName; + this.line = line; + this.column = column; + } + + public static Waypoint functionReturn( + String constraint, String fileName, int line, Integer column) { + return new Waypoint("function_return", constraint, fileName, line, column); + } + + public static Waypoint target(String fileName, int line, Integer column) { + return new Waypoint("target", null, fileName, line, column); + } + + public String getType() { + return type; + } + + @Override + public String toString() { + return type + + " @ " + + fileName + + ":" + + line + + (column == null ? "" : ":" + column) + + (constraint == null ? "" : " [" + constraint + "]"); + } + } + + private final String producerName; + private final String producerVersion; + private final String specification; + private final SourceFiles sourceFiles; + private final List waypoints = new ArrayList<>(); + + public YamlWitness( + String producerName, + String producerVersion, + String specification, + SourceFiles sourceFiles) { + this.producerName = producerName; + this.producerVersion = producerVersion; + this.specification = specification; + this.sourceFiles = sourceFiles; + } + + public void add(Waypoint waypoint) { + waypoints.add(waypoint); + } + + public List getWaypoints() { + return waypoints; + } + + public String render() throws IOException { + StringBuilder sb = new StringBuilder(); + sb.append("- entry_type: \"violation_sequence\"\n"); + sb.append(" metadata:\n"); + sb.append(" format_version: ").append(quote(FORMAT_VERSION)).append('\n'); + sb.append(" uuid: ").append(quote(UUID.randomUUID().toString())).append('\n'); + String time = + ZonedDateTime.now(ZoneOffset.UTC) + .format(DateTimeFormatter.ofPattern("yyyy-MM-dd'T'HH:mm:ss'Z'")); + sb.append(" creation_time: ").append(quote(time)).append('\n'); + sb.append(" producer:\n"); + sb.append(" name: ").append(quote(producerName)).append('\n'); + sb.append(" version: ").append(quote(producerVersion)).append('\n'); + sb.append(" task:\n"); + if (sourceFiles.isEmpty()) { + sb.append(" input_files: []\n"); + sb.append(" input_file_hashes: {}\n"); + } else { + sb.append(" input_files:\n"); + for (SourceFiles.InputFile f : sourceFiles.getFiles()) { + sb.append(" - ").append(quote(f.getDisplayPath())).append('\n'); + } + sb.append(" input_file_hashes:\n"); + for (SourceFiles.InputFile f : sourceFiles.getFiles()) { + sb.append(" ") + .append(quote(f.getDisplayPath())) + .append(": ") + .append(quote(f.getSha256())) + .append('\n'); + } + } + sb.append(" specification: ").append(quote(specification)).append('\n'); + sb.append(" language: \"Java\"\n"); + if (waypoints.isEmpty()) { + sb.append(" content: []\n"); + return sb.toString(); + } + sb.append(" content:\n"); + for (Waypoint wp : waypoints) { + sb.append(" - segment:\n"); + sb.append(" - waypoint:\n"); + sb.append(" type: ").append(quote(wp.type)).append('\n'); + sb.append(" action: \"follow\"\n"); + if (wp.constraint != null) { + sb.append(" constraint:\n"); + sb.append(" value: ").append(quote(wp.constraint)).append('\n'); + sb.append(" format: \"java_expression\"\n"); + } + sb.append(" location:\n"); + sb.append(" file_name: ").append(quote(wp.fileName)).append('\n'); + sb.append(" line: ").append(wp.line).append('\n'); + if (wp.column != null) { + sb.append(" column: ").append(wp.column).append('\n'); + } + } + return sb.toString(); + } + + /** Renders a YAML double-quoted scalar. */ + static String quote(String s) { + StringBuilder sb = new StringBuilder("\""); + for (int i = 0; i < s.length(); i++) { + char c = s.charAt(i); + switch (c) { + case '"': + sb.append("\\\""); + break; + case '\\': + sb.append("\\\\"); + break; + case '\n': + sb.append("\\n"); + break; + case '\r': + sb.append("\\r"); + break; + case '\t': + sb.append("\\t"); + break; + default: + if (c < 0x20 || c == 0x7f) { + sb.append(String.format("\\u%04x", (int) c)); + } else { + sb.append(c); + } + } + } + return sb.append('"').toString(); + } +} diff --git a/src/test/java/AppTest.java b/src/test/java/AppTest.java new file mode 100644 index 0000000..3079d3e --- /dev/null +++ b/src/test/java/AppTest.java @@ -0,0 +1,183 @@ +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import java.io.IOException; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.Base64; +import java.util.List; +import java.util.Optional; + +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.io.TempDir; + +import witness.SourceFiles; + +class AppTest { + + @Test + void columnOfClosingParenthesis() { + String line = " Boolean input_1_0 = Verifier.nondetBoolean();"; + assertEquals(48, App.nondetCallColumn(line, 0)); + assertEquals(-1, App.nondetCallColumn(line, 1)); + + String two = " if (!chunked && Verifier.nondetInt() > 0 && Verifier.nondetInt() != 0) {"; + assertEquals(')', two.charAt(App.nondetCallColumn(two, 0) - 1)); + assertEquals(')', two.charAt(App.nondetCallColumn(two, 1) - 1)); + assertTrue(App.nondetCallColumn(two, 0) < App.nondetCallColumn(two, 1)); + + String spaced = "x = Verifier.nondetInt ( );"; + assertEquals(26, App.nondetCallColumn(spaced, 0)); + assertEquals(-1, App.nondetCallColumn("no call here", 0)); + assertEquals(-1, App.nondetCallColumn("Verifier.nondetInt(", 0)); + } + + @Test + void columnOfViolatingStatement() { + assertEquals(12, App.statementColumn(" } else assert false;", true)); + assertEquals(5, App.statementColumn(" assert !(output_1 == 1);", true)); + assertEquals(5, App.statementColumn(" assert !(output_1 == 1);", false)); + assertEquals(7, App.statementColumn(" } throw new RuntimeException();", false)); + assertEquals(5, App.statementColumn(" int x = a / b;", false)); + assertEquals(14, App.statementColumn(" } else { int x = a / b; }", false)); + // tabs count as one character, like any other + assertEquals(4, App.statementColumn("\t\t\tx = elsewhere / 0;", false)); + assertEquals(-1, App.statementColumn(" }", false)); + assertEquals(-1, App.statementColumn("", false)); + } + + @Test + void resolvesSources(@TempDir Path dir) throws IOException { + Path task = dir.resolve("task"); + Files.createDirectories(task.resolve("pkg")); + Files.writeString(task.resolve("Main.java"), "class Main {}\nclass Helper {}\n"); + Files.writeString(task.resolve("pkg/Foo.java"), "package pkg;\nclass Foo {}\n"); + Path common = dir.resolve("common"); + Files.createDirectories(common.resolve("org/sosy_lab/sv_benchmarks")); + Files.writeString(common.resolve("org/sosy_lab/sv_benchmarks/Verifier.java"), "package org.sosy_lab.sv_benchmarks;\n"); + + SourceFiles files = SourceFiles.collect(List.of(common + "/", task.toString())); + assertEquals( + List.of( + common + "/org/sosy_lab/sv_benchmarks/Verifier.java", + task + "/Main.java", + task + "/pkg/Foo.java"), + files.getFiles().stream().map(SourceFiles.InputFile::getDisplayPath).toList()); + + assertEquals("Main.java", files.resolve("Main", "Main.java").get().getRelativePath()); + assertEquals("Main.java", files.resolve("Main$1", "").get().getRelativePath()); + assertEquals("Main.java", files.resolve("Helper", "Main.java").get().getRelativePath()); + assertEquals("pkg/Foo.java", files.resolve("pkg/Foo", "Foo.java").get().getRelativePath()); + assertEquals("pkg/Foo.java", files.resolve("pkg.Foo$Inner", "").get().getRelativePath()); + assertEquals( + "org/sosy_lab/sv_benchmarks/Verifier.java", + files.resolve("org.sosy_lab.sv_benchmarks.Verifier", "Verifier.java").get().getRelativePath()); + assertEquals(Optional.empty(), files.resolve("Missing", "")); + assertEquals(64, files.getFiles().get(0).getSha256().length()); + + // A file reachable through several inputs (e.g. a nested common/ dir) is listed once + SourceFiles nested = SourceFiles.collect(List.of(task + "/pkg", task.toString(), task + "/pkg/Foo.java")); + assertEquals( + List.of(task + "/pkg/Foo.java", task + "/Main.java"), + nested.getFiles().stream().map(SourceFiles.InputFile::getDisplayPath).toList()); + } + + @Test + void writesYamlAndGraphmlWitness(@TempDir Path dir) throws IOException { + Path task = dir.resolve("task"); + Files.createDirectories(task); + Files.writeString( + task.resolve("Main.java"), + String.join( + "\n", + "import org.sosy_lab.sv_benchmarks.Verifier;", + "public class Main {", + " public static void main(String[] args) {", + " int x = Verifier.nondetInt();", + " String s = Verifier.nondetString();", + " if (x == 3 && s.equals(\"a\\\"b\")) {", + " assert false;", + " }", + " }", + "}", + "")); + Path prp = dir.resolve("valid-assert.prp"); + Files.writeString(prp, "CHECK( init(Main.main()), LTL(G assert) )\n"); + Path out = dir.resolve("out"); + + String markers = + marker("[WITNESS]", "3@@@4@@@Main@@@main([Ljava/lang/String;)V@@@0@@@I@@@Main.java") + + "\n" + + marker("[WITNESS]", "a\"b@@@5@@@Main@@@main([Ljava/lang/String;)V@@@0@@@Ljava/lang/String;@@@Main.java") + + "\n" + + marker("[WITNESS_TARGET]", "java.lang.AssertionError@@@Main@@Main.java@@7"); + App.main(new String[] { + Base64.getEncoder().encodeToString(markers.getBytes(StandardCharsets.UTF_8)), + "--input", task.toString(), + "--property", prp.toString(), + "--out", out.toString(), + "--producer-version", "test" + }); + + String yaml = Files.readString(out.resolve("witness.yml")); + assertTrue(yaml.startsWith("- entry_type: \"violation_sequence\"\n")); + assertTrue(yaml.contains(" format_version: \"2.3\"\n")); + assertTrue(yaml.contains(" name: \"SWAT\"\n version: \"test\"\n")); + assertTrue(yaml.contains(" - \"" + task + "/Main.java\"\n")); + assertTrue(yaml.contains(" specification: \"CHECK( init(Main.main()), LTL(G assert) )\"\n")); + assertTrue(yaml.contains(" language: \"Java\"\n")); + assertFalse(yaml.contains("data_model")); + assertTrue(yaml.contains(" value: \"\\\\result == 3\"\n format: \"java_expression\"\n")); + assertTrue(yaml.contains(" line: 4\n column: 32\n")); + assertTrue(yaml.contains(" value: \"\\\\result.equals(\\\"a\\\\\\\"b\\\")\"\n")); + assertTrue(yaml.contains(" line: 5\n column: 38\n")); + assertTrue(yaml.contains(" type: \"target\"\n action: \"follow\"\n location:\n")); + assertTrue(yaml.contains(" line: 7\n column: 7\n")); + assertEquals(3, yaml.split(" - segment:\n").length - 1); + + String graphml = Files.readString(out.resolve("witness.graphml")); + assertTrue(graphml.contains("x = 3")); + assertTrue(graphml.contains("s.equals(\"a\\\"b\")")); + assertTrue(graphml.contains("true")); + } + + @Test + void defaultViolationWithoutMarkers(@TempDir Path dir) throws IOException { + Path task = dir.resolve("task"); + Files.createDirectories(task); + Files.writeString(task.resolve("Main.java"), "public class Main {\n public static void main(String[] a) {\n assert false;\n }\n}\n"); + Path out = dir.resolve("out"); + + App.main(new String[] {"", "--input", task.toString(), "--out", out.toString()}); + String yaml = Files.readString(out.resolve("witness.yml")); + assertTrue(yaml.contains(" content: []\n")); + assertTrue(Files.readString(out.resolve("witness.graphml")).contains("true")); + + // A target alone is enough for a final segment + App.main(new String[] { + Base64.getEncoder().encodeToString( + marker("[WITNESS_TARGET]", "java.lang.AssertionError@@@Main@@Main.java@@3").getBytes()), + "--input", task.toString(), "--out", out.toString() + }); + yaml = Files.readString(out.resolve("witness.yml")); + assertTrue(yaml.contains(" type: \"target\"\n")); + assertTrue(yaml.contains(" line: 3\n column: 5\n")); + } + + @Test + void legacyInvocationStillWorks(@TempDir Path dir) throws IOException { + Files.writeString(dir.resolve("Main.java"), "class Main {\n int x = Verifier.nondetInt();\n}\n"); + String markers = marker("[WITNESS]", "1@@@2@@@Main@@@()V"); + App.main(new String[] {Base64.getEncoder().encodeToString(markers.getBytes()), dir.toString()}); + String yaml = Files.readString(dir.resolve("witness.yml")); + assertTrue(yaml.contains(" value: \"\\\\result == 1\"\n")); + assertTrue(yaml.contains(" line: 2\n column: 30\n")); + assertTrue(Files.readString(dir.resolve("witness.graphml")).contains("<init>")); + } + + private static String marker(String kind, String payload) { + return "prefix " + kind + " " + Base64.getEncoder().encodeToString(payload.getBytes(StandardCharsets.UTF_8)); + } +} diff --git a/src/test/java/witness/JavaLiteralsTest.java b/src/test/java/witness/JavaLiteralsTest.java new file mode 100644 index 0000000..72cfc62 --- /dev/null +++ b/src/test/java/witness/JavaLiteralsTest.java @@ -0,0 +1,77 @@ +package witness; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import org.junit.jupiter.api.Test; + +class JavaLiteralsTest { + + @Test + void integralTypes() { + assertEquals("\\result == 5", JavaLiterals.resultConstraint("5", "I")); + assertEquals("\\result == -5", JavaLiterals.resultConstraint("-5", "I")); + assertEquals("\\result == -128", JavaLiterals.resultConstraint("-128", "B")); + assertEquals("\\result == 32767", JavaLiterals.resultConstraint("32767", "S")); + assertEquals("\\result == -2147483648", JavaLiterals.resultConstraint("-2147483648", "I")); + } + + @Test + void longsGetSuffixOnlyWhenNeeded() { + assertEquals("\\result == 5", JavaLiterals.resultConstraint("5", "J")); + assertEquals("\\result == 5000000000L", JavaLiterals.resultConstraint("5000000000", "J")); + assertEquals( + "\\result == -9223372036854775808L", + JavaLiterals.resultConstraint("-9223372036854775808", "J")); + } + + @Test + void booleans() { + assertEquals("\\result == true", JavaLiterals.resultConstraint("true", "Z")); + assertEquals("\\result == false", JavaLiterals.resultConstraint("false", "Z")); + } + + @Test + void charsAreRenderedAsLiterals() { + assertEquals("\\result == 'a'", JavaLiterals.resultConstraint("97", "C")); + assertEquals("\\result == '\\''", JavaLiterals.resultConstraint("39", "C")); + assertEquals("\\result == '\\\\'", JavaLiterals.resultConstraint("92", "C")); + assertEquals("\\result == '\\n'", JavaLiterals.resultConstraint("10", "C")); + assertEquals("\\result == '\\u0000'", JavaLiterals.resultConstraint("0", "C")); + assertEquals("\\result == '\\u00e4'", JavaLiterals.resultConstraint("228", "C")); + assertEquals("\\result == '\\uffff'", JavaLiterals.resultConstraint("65535", "C")); + } + + @Test + void floatingPoint() { + assertEquals("\\result == 1.5f", JavaLiterals.resultConstraint("1.5", "F")); + assertEquals("\\result == -0.000002022784f", JavaLiterals.resultConstraint("-0.000002022784", "F")); + assertEquals("\\result == 10000000000.0f", JavaLiterals.resultConstraint("1.0E10", "F")); + assertEquals("\\result == 0.1", JavaLiterals.resultConstraint("0.1", "D")); + assertEquals("\\result == -0.0", JavaLiterals.resultConstraint("-0.0", "D")); + assertEquals("\\result == 10000000000.0", JavaLiterals.resultConstraint("10000000000", "D")); + assertEquals("Float.isNaN(\\result)", JavaLiterals.resultConstraint("NaN", "F")); + assertEquals("Double.isNaN(\\result)", JavaLiterals.resultConstraint("NaN", "D")); + assertEquals("\\result == Double.POSITIVE_INFINITY", JavaLiterals.resultConstraint("Infinity", "D")); + assertEquals("\\result == Float.NEGATIVE_INFINITY", JavaLiterals.resultConstraint("-Infinity", "F")); + } + + @Test + void strings() { + assertEquals("\\result.equals(\"abc\")", JavaLiterals.resultConstraint("abc", "Ljava/lang/String;")); + assertEquals("\\result.equals(\"\")", JavaLiterals.resultConstraint("", "Ljava/lang/String;")); + assertEquals( + "\\result.equals(\"a\\\"b\\\\c\\nd\\te\")", + JavaLiterals.resultConstraint("a\"b\\c\nd\te", "Ljava/lang/String;")); + assertEquals( + "\\result.equals(\"\\u0001x\")", + JavaLiterals.resultConstraint("\u0001x", "Ljava/lang/String;")); + assertEquals("\\result.equals(\"ä€\")", JavaLiterals.resultConstraint("ä€", "Ljava/lang/String;")); + } + + @Test + void legacyMarkersWithoutType() { + assertEquals("\\result == 42", JavaLiterals.resultConstraint("42", null)); + assertEquals("\\result == true", JavaLiterals.resultConstraint("true", null)); + assertEquals("\\result.equals(\"hi\")", JavaLiterals.resultConstraint("hi", null)); + } +} diff --git a/src/test/java/witness/MarkerTest.java b/src/test/java/witness/MarkerTest.java new file mode 100644 index 0000000..b9d4746 --- /dev/null +++ b/src/test/java/witness/MarkerTest.java @@ -0,0 +1,70 @@ +package witness; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNull; +import static org.junit.jupiter.api.Assertions.assertThrows; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import org.junit.jupiter.api.Test; + +class MarkerTest { + + @Test + void parsesCurrentFormat() { + ValueMarker m = ValueMarker.parse("5@@@13@@@pkg/Main$1@@@main([Ljava/lang/String;)V@@@2@@@I@@@Main.java"); + assertEquals("5", m.getValue()); + assertEquals(13, m.getLine()); + assertEquals("pkg/Main$1", m.getClassName()); + assertEquals("main([Ljava/lang/String;)V", m.getMethodDesc()); + assertEquals(2, m.getCallIndex()); + assertEquals("I", m.getTypeDesc()); + assertEquals("Main.java", m.getSourceFile()); + } + + @Test + void stringValuesMayContainTheSeparator() { + ValueMarker m = ValueMarker.parse("a@@@b@@@7@@@Main@@@main()V@@@0@@@Ljava/lang/String;@@@Main.java"); + assertEquals("a@@@b", m.getValue()); + assertEquals(7, m.getLine()); + assertTrue(m.isString()); + + ValueMarker legacy = ValueMarker.parse("a@@@b@@@7@@@Main@@@main()V"); + assertEquals("a@@@b", legacy.getValue()); + assertEquals(7, legacy.getLine()); + } + + @Test + void parsesLegacyFormat() { + ValueMarker m = ValueMarker.parse("true@@@13@@@Main@@@main([Ljava/lang/String;)V"); + assertEquals("true", m.getValue()); + assertEquals(13, m.getLine()); + assertEquals("Main", m.getClassName()); + assertEquals(0, m.getCallIndex()); + assertNull(m.getTypeDesc()); + assertEquals("", m.getSourceFile()); + } + + @Test + void rejectsGarbage() { + assertThrows(IllegalArgumentException.class, () -> ValueMarker.parse("nonsense")); + } + + @Test + void parsesTarget() { + TargetMarker t = TargetMarker.parse( + "java.lang.AssertionError@@@Main@@Main.java@@23;pkg.Helper$Inner@@Helper.java@@5;java.lang.Thread@@@@-1"); + assertTrue(t.isAssertionError()); + assertEquals(3, t.getFrames().size()); + assertEquals("Main", t.getFrames().get(0).getClassName()); + assertEquals("Main.java", t.getFrames().get(0).getFileName()); + assertEquals(23, t.getFrames().get(0).getLine()); + assertEquals("", t.getFrames().get(2).getFileName()); + assertEquals(-1, t.getFrames().get(2).getLine()); + } + + @Test + void targetWithoutFrames() { + TargetMarker t = TargetMarker.parse("java.lang.RuntimeException@@@"); + assertEquals(0, t.getFrames().size()); + } +}