Emit YAML violation witnesses (format 2.3)

.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/

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"

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:")

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
 

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<Integer, Integer> 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;
     }

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<Integer, Integer> 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<Integer, Integer> 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");

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);