diff --git a/.gitignore b/.gitignore index 57b3d545..9c44923f 100644 --- a/.gitignore +++ b/.gitignore @@ -24,6 +24,7 @@ targets/applications/openhospital/oh_build/restler_working_dir/Compile targets/applications/openhospital/oh_build/restler_working_dir/RestlerResults targets/sv-comp/sv-benchmarks/ targets/sv-comp/wit4java/ +targets/sv-comp/WitnessCreator/ **/__pycache__ **/.venv/* /.vscode/ diff --git a/scripts/svcomp-package/run-swat.sh b/scripts/svcomp-package/run-swat.sh index 424a3188..62a17e10 100755 --- a/scripts/svcomp-package/run-swat.sh +++ b/scripts/svcomp-package/run-swat.sh @@ -27,37 +27,7 @@ if [ -f "$second_last_path/Main.java" ]; then set -- "${@:1:$(($#-2))}" "$last_path" "$second_last_path" fi -# Loop through all provided paths and copy Java files preserving directory structure -for path in "$@"; do - if [ -d "$path" ]; then - # Find all Java files and preserve relative directory structure - find "$path" -type f -name "*.java" | while read src; do - rel_path="${src#$path/}" - dst_dir="./WitnessCreator/$(dirname "$rel_path")" - mkdir -p "$dst_dir" - cp "$src" "$dst_dir/" - done - echo "Java files from $path copied successfully to ./WitnessCreator/" - elif [ -f "$path" ] && [[ "$path" == *.java ]]; then - # If the argument is a single Java file, copy it - cp "$path" ./WitnessCreator/ - echo "File $path copied successfully to ./WitnessCreator/" - fi -done - -# # copy Main.java for Witness creation -# last_path="${@: -1}" -# file_to_copy="${last_path}/Main.java" -# -# # Check if the file exists -# if [ -f "$file_to_copy" ]; then -# # Copy the Main.java file to the current directory -# cp "$file_to_copy" ./WitnessCreator/. -# echo "File copied successfully to ./WitnessCreator/" -# else -# echo "Error: File not found." -# fi - +# The witness is created by run_swat.py directly from the given input paths. SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" VENV_PYTHON="$SCRIPT_DIR/.venv_ubuntu_24_04_1__x86_64/bin/python3" diff --git a/scripts/svcomp-package/run_swat.py b/scripts/svcomp-package/run_swat.py index 6b883330..8d36dca0 100755 --- a/scripts/svcomp-package/run_swat.py +++ b/scripts/svcomp-package/run_swat.py @@ -7,7 +7,11 @@ logging.basicConfig(level=logging.INFO) logger = logging.getLogger(__name__) SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__)) -WITNESS_PATH = os.path.join(SCRIPT_DIR, 'WitnessCreator/build/libs/WitnessCreator.jar') +ORIGINAL_CWD = os.getcwd() +WITNESS_DIR = os.path.join(SCRIPT_DIR, 'WitnessCreator') +WITNESS_PATH = os.path.join(WITNESS_DIR, 'build/libs/WitnessCreator.jar') +# Output lines carrying witness information: nondet values and the violating location +WITNESS_MARKERS = ('[WITNESS]', '[WITNESS_TARGET]') class ExecutionStatus(enum.Enum): @@ -145,30 +149,50 @@ def extract_last_round(out, marker="============================== ROUND"): return "\n ".join(out).split(marker)[-1] -def extract_markers(out, marker): +def extract_markers(out, markers): + if isinstance(markers, str): + markers = (markers,) res = [] for line in out.split("\n"): print(line) - if marker in line: + if any(marker in line for marker in markers): res.append(line) return res -def generate_witness(witness): - witness_dir = os.path.join(SCRIPT_DIR, 'WitnessCreator/') - with pushd(witness_dir): - # base64 encode the string - enc = base64.b64encode(witness.encode()) - cmd = [ - 'java', - '-jar', - WITNESS_PATH, - enc, - witness_dir - ] - print(cmd) +def swat_version(): + """The package version from BUILD_INFO.txt, written by scripts/package-svcomp.sh.""" + try: + with open(os.path.join(SCRIPT_DIR, 'BUILD_INFO.txt')) as f: + for line in f: + if line.startswith('version='): + return line[len('version='):].strip() + except OSError: + pass + return 'unknown' + +def generate_witness(witness, property_path, input_paths): + """Create witness.yml (format 2.3) and witness.graphml in the WitnessCreator directory. + + `property_path` and `input_paths` are the verifier's arguments as given by BenchExec; + they are resolved against the original working directory and end up in the witness. + """ + enc = base64.b64encode(witness.encode()).decode() + cmd = [ + 'java', + '-jar', + WITNESS_PATH, + enc, + '--out', WITNESS_DIR, + '--property', property_path, + '--producer-version', swat_version(), + ] + for path in input_paths: + cmd.extend(['--input', path]) + print(cmd) + with pushd(ORIGINAL_CWD): _, output = run_command_with_timeout(cmd) - print("WITNESS CREATED") - print(output) + print("WITNESS CREATED") + log_output(output) def log_output(output: List[str]): for line in output: @@ -180,9 +204,11 @@ def log_output(output: List[str]): # Look for property file in arguments # SV-COMP framework passes the .prp file directly as first argument property_file = None + property_path = None for arg in sys.argv[1:]: if arg.endswith('.prp'): property_file = os.path.basename(arg) + property_path = arg logger.info(f"Found property file in arguments: {property_file}") break @@ -193,6 +219,9 @@ def log_output(output: List[str]): logger.info(f"Using property file: {property_file}") + # The task's input files/directories, as given (everything but the property file) + input_paths = [arg for arg in sys.argv[1:] if arg != property_path] + target_dir = sys.argv[-1] cmd = generate_command(sys.argv[1:], property_file) local_target_dir = copy_target(target_dir) @@ -218,12 +247,12 @@ def log_output(output: List[str]): out = extract_last_round(output) verdict = extract_markers(out, f'[VERDICT {property_file}]') if "== ERROR" in str(verdict): - witnesses = extract_markers(out, '[WITNESS]') - generate_witness("\n".join(witnesses)) + witnesses = extract_markers(out, WITNESS_MARKERS) + generate_witness("\n".join(witnesses), property_path, input_paths) print(f'Witnesses:\n {witnesses}') # Print the generated witness file contents for validation on benchmark server - witness_file_path = os.path.join(SCRIPT_DIR, 'WitnessCreator', 'witness.graphml') + witness_file_path = os.path.join(WITNESS_DIR, 'witness.yml') if os.path.exists(witness_file_path): print("\n" + "="*80) print("WITNESS FILE CONTENTS:") diff --git a/scripts/svcomp-package/smoketest.sh b/scripts/svcomp-package/smoketest.sh index 95fb8c05..e816d1d0 100755 --- a/scripts/svcomp-package/smoketest.sh +++ b/scripts/svcomp-package/smoketest.sh @@ -1,12 +1,18 @@ #!/bin/bash cd "$(dirname "$0")" +rm -f WitnessCreator/witness.yml WitnessCreator/witness.graphml output="$("bash" "run-swat.sh" "../../sv-benchmarks/java/properties/valid-assert.prp" "smoketest/common" "smoketest")" -if echo "$output" | grep -q "\[VERDICT valid-assert.prp\] == ERROR"; then - echo "Smoketest passed!" - exit 0 -else - echo "Smoketest failed!" +if ! echo "$output" | grep -q "\[VERDICT valid-assert.prp\] == ERROR"; then + echo "Smoketest failed: no violation verdict!" exit 1 fi +# The violation must come with a YAML witness (format 2.3) for the smoketest target +if ! grep -q 'entry_type: "violation_sequence"' WitnessCreator/witness.yml 2>/dev/null \ + || ! grep -q 'type: "target"' WitnessCreator/witness.yml; then + echo "Smoketest failed: no violation witness with a target waypoint in WitnessCreator/witness.yml!" + exit 1 +fi +echo "Smoketest passed!" +exit 0 diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java index 8ed69119..798cac83 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java @@ -1,6 +1,8 @@ package de.uzl.its.swat.instrument.svcomp; import de.uzl.its.swat.common.Util; +import java.util.HashMap; +import java.util.Map; import org.objectweb.asm.ClassVisitor; import org.objectweb.asm.MethodVisitor; import org.objectweb.asm.Opcodes; @@ -15,6 +17,15 @@ public class SVCompClassAdapter extends ClassVisitor { private final String cname; + /** + * Number of nondet calls seen so far per source line of this class. Shared by all method + * adapters so that the witness can tell apart several nondet calls on one line. + */ + private final Map nondetCallsPerLine = new HashMap<>(); + + /** The source file name of the class (SourceFile attribute), empty if unknown. */ + private String sourceFile = ""; + /** * Constructor that calls the super from the default ClassVisitor * @@ -25,6 +36,14 @@ public SVCompClassAdapter(ClassVisitor cv, String cname) { this.cname = cname; } + @Override + public void visitSource(String source, String debug) { + if (source != null) { + sourceFile = source; + } + super.visitSource(source, debug); + } + /** * Visits a method of the class. This method must return a new MethodVisitor instance (or null) * each time it is called, i.e., it should not return a previously returned visitor. Addition: @@ -55,7 +74,8 @@ public MethodVisitor visitMethod( if (!cname.equals("org/sosy_lab/sv_benchmarks/Verifier")) { SVCompTransformer.getPrintBox().addMsg("Method: " + name); - return new SVCompMethodAdapter(access, mv, cname, name, desc); + return new SVCompMethodAdapter( + access, mv, cname, name, desc, sourceFile, nondetCallsPerLine); } return mv; } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java index df2a3877..c7082ae1 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java @@ -3,6 +3,7 @@ import de.uzl.its.swat.instrument.InternalTransformerType; import de.uzl.its.swat.instrument.Intrinsics; import de.uzl.its.swat.instrument.Transformer; +import java.util.Map; import org.objectweb.asm.Label; import org.objectweb.asm.MethodVisitor; import org.objectweb.asm.Opcodes; @@ -16,6 +17,8 @@ public class SVCompMethodAdapter extends LocalVariablesSorter { private final String cname; private final String name; private final String desc; + private final String sourceFile; + private final Map nondetCallsPerLine; int lineNumber = 0; /** @@ -24,14 +27,25 @@ public class SVCompMethodAdapter extends LocalVariablesSorter { * @param mv Parent MethodVisitor * @param name The method name * @param desc A string description of the parameters of the method + * @param sourceFile The source file name of the class (empty if unknown) + * @param nondetCallsPerLine Per-class counter of nondet calls per source line (shared between + * the methods of the class) */ public SVCompMethodAdapter( - int access, MethodVisitor mv, String cname, String name, String desc) { + int access, + MethodVisitor mv, + String cname, + String name, + String desc, + String sourceFile, + Map nondetCallsPerLine) { super(Opcodes.ASM9, access, desc, mv); identifier = cname + "/" + name; this.desc = desc; this.cname = cname; this.name = name; + this.sourceFile = sourceFile; + this.nondetCallsPerLine = nondetCallsPerLine; } @Override @@ -58,6 +72,9 @@ public void visitMethodInsn( String retType = descriptor.split("\\)")[1]; long nextId = Verifier.getNextId(); + // Index of this call among the nondet calls on the same source line (bytecode order + // follows the left-to-right evaluation order); lets the witness locate the call. + int callIndex = nondetCallsPerLine.merge(lineNumber, 1, Integer::sum) - 1; SVCompTransformer.getPrintBox().setContentPresent(true); SVCompTransformer.getPrintBox() .addMsg(" => Found " + name + " in line " + lineNumber); @@ -72,11 +89,15 @@ public void visitMethodInsn( mv.visitLdcInsn(lineNumber); mv.visitLdcInsn(cname); mv.visitLdcInsn(this.name + this.desc); + mv.visitLdcInsn(callIndex); + mv.visitLdcInsn(sourceFile); mv.visitMethodInsn( Opcodes.INVOKESTATIC, "de/uzl/its/swat/witness/Witness", "recordValue", - "(" + descriptor.substring(2) + "ILjava/lang/String;Ljava/lang/String;)V", + "(" + + descriptor.substring(2) + + "ILjava/lang/String;Ljava/lang/String;ILjava/lang/String;)V", false); mv.visitLdcInsn(nextId); SVCompTransformer.getPrintBox().addMsg(" => Adding Witness recording"); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java index bc59a3f2..5d74772a 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java @@ -67,8 +67,13 @@ private void addEndOfSurrounding() { visitInsn(Opcodes.DUP); + // Prints the stack trace and records the violating location for the witness visitMethodInsn( - Opcodes.INVOKEVIRTUAL, "java/lang/Throwable", "printStackTrace", "()V", false); + Opcodes.INVOKESTATIC, + "de/uzl/its/swat/witness/Witness", + "recordTarget", + "(Ljava/lang/Throwable;)V", + false); // Duplicate exception for instanceof check visitInsn(Opcodes.DUP); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java b/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java index 10e1e79d..db5262fc 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java @@ -3,75 +3,172 @@ import java.math.BigDecimal; import java.util.Base64; +/** + * Emits the witness markers that WitnessCreator turns into an SV-COMP violation witness. + * + *

Two kinds of markers are printed to stdout: + * + *

    + *
  • {@code [WITNESS] } for every value returned by a {@code Verifier.nondet*()} call. + * The payload is {@code + * value@@@line@@@className@@@methodDesc@@@callIndex@@@typeDesc@@@sourceFile}, where {@code + * callIndex} is the (0-based) index of the call among the nondet calls on the same source + * line of the class (bytecode order, which follows the left-to-right evaluation order), + * {@code typeDesc} is the JVM descriptor of the returned type and {@code sourceFile} the + * SourceFile attribute of the class (empty if unknown). + *
  • {@code [WITNESS_TARGET] } once for the uncaught throwable that ends the run. The + * payload is {@code throwableClass@@@frame;frame;...} with frames encoded as {@code + * className@@fileName@@line}, innermost first. + *
+ */ public class Witness { - public static void recordValue(boolean value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; + private static final String SEPARATOR = "@@@"; + private static final int MAX_TARGET_FRAMES = 64; + + private static void record( + String value, + String typeDesc, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { + String witness = + value + + SEPARATOR + + lineNumber + + SEPARATOR + + cname + + SEPARATOR + + desc + + SEPARATOR + + callIndex + + SEPARATOR + + typeDesc + + SEPARATOR + + sourceFile; String enc = Base64.getEncoder().encodeToString(witness.getBytes()); System.out.println("[WITNESS] " + enc); } - public static void recordValue(byte value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + boolean value, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { + record(String.valueOf(value), "Z", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(char value, int lineNumber, String cname, String desc) { - int encVal = Integer.valueOf(value); - String witness = encVal + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + byte value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { + record(String.valueOf(value), "B", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(short value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + char value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { + // Chars are transported as their (unsigned) code point, WitnessCreator renders the literal + record(String.valueOf((int) value), "C", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(int value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + short value, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { + record(String.valueOf(value), "S", lineNumber, cname, desc, callIndex, sourceFile); + } + + public static void recordValue( + int value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { + record(String.valueOf(value), "I", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(float value, int lineNumber, String cname, String desc) { + public static void recordValue( + float value, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { // Use BigDecimal to avoid scientific notation (e.g., -2.022784E-6) // but handle special values (NaN, Infinity) which BigDecimal doesn't support String valueStr; if (Float.isNaN(value) || Float.isInfinite(value)) { valueStr = Float.toString(value); + } else if (value == 0.0f && 1.0f / value < 0.0f) { + valueStr = "-0.0"; // BigDecimal has no negative zero } else { valueStr = BigDecimal.valueOf(value).toPlainString(); } - String witness = valueStr + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + record(valueStr, "F", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(long value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + long value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { + record(String.valueOf(value), "J", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(double value, int lineNumber, String cname, String desc) { + public static void recordValue( + double value, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { // Use BigDecimal to avoid scientific notation (e.g., 1.23E-10) // but handle special values (NaN, Infinity) which BigDecimal doesn't support String valueStr; if (Double.isNaN(value) || Double.isInfinite(value)) { valueStr = Double.toString(value); + } else if (value == 0.0 && 1.0 / value < 0.0) { + valueStr = "-0.0"; // BigDecimal has no negative zero } else { valueStr = BigDecimal.valueOf(value).toPlainString(); } - String witness = valueStr + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + record(valueStr, "D", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(String value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + String value, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { + record( + String.valueOf(value), + "Ljava/lang/String;", + lineNumber, + cname, + desc, + callIndex, + sourceFile); + } + + /** + * Records the throwable that escaped the entry method and prints its stack trace. The stack + * trace locates the violating statement for the witness' target waypoint. + * + * @param throwable the uncaught throwable + */ + public static void recordTarget(Throwable throwable) { + throwable.printStackTrace(); + StringBuilder sb = new StringBuilder(throwable.getClass().getName()).append(SEPARATOR); + StackTraceElement[] frames = throwable.getStackTrace(); + for (int i = 0; i < frames.length && i < MAX_TARGET_FRAMES; i++) { + if (i > 0) sb.append(';'); + StackTraceElement frame = frames[i]; + sb.append(frame.getClassName()) + .append("@@") + .append(frame.getFileName() == null ? "" : frame.getFileName()) + .append("@@") + .append(frame.getLineNumber()); + } + String enc = Base64.getEncoder().encodeToString(sb.toString().getBytes()); + System.out.println("[WITNESS_TARGET] " + enc); } } diff --git a/targets/sv-comp/scripts/README.md b/targets/sv-comp/scripts/README.md index 22ce37c6..2b53be54 100644 --- a/targets/sv-comp/scripts/README.md +++ b/targets/sv-comp/scripts/README.md @@ -61,6 +61,12 @@ scripts/ ./svcomp setup all ``` +Witnesses of violation results are written by WitnessCreator (expected at +`../WitnessCreator/{build/libs/WitnessCreator.jar,witnesses/}`) to the testcase's +`logs/witness/` as `witness.yml` (YAML format 2.3) and `witness.graphml` (legacy, validated with +wit4java). To additionally lint the YAML witness, point `SWAT_WITNESSLINT` at a WitnessLint +command, e.g. `SWAT_WITNESSLINT="/path/venv/bin/python /path/witnesslint/witnesslinter.py"`. + ### Test Commands ```bash diff --git a/targets/sv-comp/scripts/lib/witness.py b/targets/sv-comp/scripts/lib/witness.py index 16fd26c4..97d9d2ce 100644 --- a/targets/sv-comp/scripts/lib/witness.py +++ b/targets/sv-comp/scripts/lib/witness.py @@ -3,7 +3,7 @@ import os import enum import logging -import shutil +import shlex import subprocess import time from typing import List, Optional, Tuple @@ -14,6 +14,11 @@ SCRIPT_DIR = Path(__file__).resolve().parent.parent # Now in lib/, so go up one more level WITNESS_CREATION_PATH = (SCRIPT_DIR.parent / 'WitnessCreator' / 'build' / 'libs' / 'WitnessCreator.jar') WITNESS_VALIDATION_PATH = (SCRIPT_DIR.parent / 'wit4java' / 'bin' / 'wit4java') +# Output lines carrying witness information: nondet values and the violating location +WITNESS_MARKERS = ("[WITNESS]", "[WITNESS_TARGET]") +# Optional: command prefix of WitnessLint (e.g. "/path/venv/bin/python /path/witnesslinter.py"); +# when set, the YAML witness is linted after creation. Proper validator setup is tracked in #47. +WITNESSLINT_ENV = 'SWAT_WITNESSLINT' class ExecutionStatus(enum.Enum): SUCCESS = "success" @@ -38,26 +43,43 @@ def generate_and_validate_witness(ver_task: VerificationTask, output: List[str]) } out = extract_last_round(output) - witnesses = extract_markers(out, "[WITNESS]") + witnesses = extract_markers(out, WITNESS_MARKERS) if not witnesses: logger.debug("No witnesses found in output") return None, 0.0, 0.0 - witness_dir = assemble_files(info) + witness_dir = Path(info['log_dir']) / 'witness' + witness_dir.mkdir(parents=True, exist_ok=True) logger.info("Generating witness files") generation_start = time.perf_counter() - generate_witness(witness_dir, "\n".join(witnesses)) + generate_witness(witness_dir, "\n".join(witnesses), input_dirs(info), property_file(ver_task)) generation_time = time.perf_counter() - generation_start logger.info("Validating witness") validation_start = time.perf_counter() + lint_witness(witness_dir / 'witness.yml', input_dirs(info)) validation_result = validate_witness(info) validation_time = time.perf_counter() - validation_start return validation_result, generation_time, validation_time +def input_dirs(info: dict) -> List[str]: + """The task's source directories (classpath entries that are directories).""" + try: + classpath_index = info['command'].index('--classpath') + classpath_entries = info['command'][classpath_index + 1:] + except ValueError: + classpath_entries = [] + return [folder for folder in classpath_entries if Path(folder).is_dir()] + + +def property_file(ver_task: VerificationTask) -> Path: + """The property file of the task, e.g. sv-benchmarks/java/properties/valid-assert.prp.""" + return ver_task['file_path'].parent.parent / 'properties' / ver_task['category'].value + + def log_output(output: List[str]): for line in output: logger.info(line.strip()) @@ -115,15 +137,18 @@ def extract_last_round(out: List[str], marker: str = "========================== -def extract_markers(out: str, marker: str) -> List[str]: +def extract_markers(out: str, markers) -> List[str]: + if isinstance(markers, str): + markers = (markers,) res: List[str] = [] for line in out.split("\n"): logger.debug(line) - if marker in line: + if any(marker in line for marker in markers): res.append(line) return res -def generate_witness(witness_dir: str, witness: str) -> None: +def generate_witness(witness_dir: Path, witness: str, inputs: List[str], prp: Path) -> None: + """Create witness.yml (format 2.3) and witness.graphml in `witness_dir` from the marker lines.""" with pushd(str(SCRIPT_DIR.parent / 'WitnessCreator')): # base64 encode the string enc = base64.b64encode(witness.encode()).decode() @@ -132,13 +157,30 @@ def generate_witness(witness_dir: str, witness: str) -> None: '-jar', str(WITNESS_CREATION_PATH), enc, - str(witness_dir) + '--out', str(witness_dir), + '--property', str(prp), + '--producer-version', 'local', ] + for folder in inputs: + cmd.extend(['--input', folder]) logger.info(f"Running witness creator: {cmd}") _, output = run_command_with_timeout(cmd) logger.info("Witness created") log_output(output) +def lint_witness(witness_file: Path, inputs: List[str]) -> Optional[bool]: + """Run WitnessLint on the YAML witness if SWAT_WITNESSLINT is set; True iff the witness is well-formed.""" + linter = os.environ.get(WITNESSLINT_ENV) + if not linter or not witness_file.exists(): + return None + cmd = shlex.split(linter) + ['--expectViolationWitness', '--expectedWitnessVersion', '2', + '--witness', str(witness_file)] + inputs + status, output = run_command_with_timeout(cmd) + log_output(output) + ok = status == ExecutionStatus.SUCCESS and any('finished with exit code 0' in line for line in output) + logger.info(f"WitnessLint: {'well-formed' if ok else 'FAULTY'} ({witness_file})") + return ok + def run_command_with_timeout(cmd: list[str], timeout: int = 180) -> tuple[ExecutionStatus, list[str]]: """Executes the given command and returns output from both STDOUT and STDERR.""" @@ -172,28 +214,3 @@ def run_command_with_timeout(cmd: list[str], timeout: int = 180) -> tuple[Execut return ExecutionStatus.ERROR, output + [str(e)] -def assemble_files(info: dict) -> str: - witness_dir = Path(info['log_dir']) / 'witness' - witness_dir.mkdir(parents=True, exist_ok=True) - - try: - classpath_index = info['command'].index('--classpath') - classpath_entries = info['command'][classpath_index + 1:] - except ValueError: - classpath_entries = [] - - for folder in classpath_entries: - folder_path = Path(folder) - if not folder_path.exists(): - continue - for src in folder_path.rglob('*.java'): - # Preserve relative path structure (package directories) for WitnessCreator - rel_path = src.relative_to(folder_path) - dst = witness_dir / rel_path - dst.parent.mkdir(parents=True, exist_ok=True) - logger.info(f"Copying {src} to {dst}") - shutil.copy(str(src), str(dst)) - - return str(witness_dir) - - \ No newline at end of file