Yaml witness

example/README.md

@@ -2,14 +2,6 @@
 
 Run all of them via `./smoketest.sh` from the repository root.
 
-## mix000.opt.i + mix000.opt.i.graphml (GraphML, format 1.0)
-
-The example witness is incomplete (it does not give a value to `tmp_guard`,
-which would be relevant), so the verdict is not guaranteed; in practice the
-enforced schedule reaches the violation in nearly every execution
-(`ALWAYS`/`SOMETIMES`). The smoketest only checks that the test is generated
-and runs.
-
 ## concurrent-unreach.i + concurrent-unreach.witness-2.2.yml (YAML, format 2.2)
 
 Reachability (`unreach-call`) witness for a concurrent program: the writer

example/concurrent-mem-safety.i

@@ -0,0 +1,34 @@
+// Concurrent memory-safety violation: the freer thread frees p before main
+// dereferences it, so `*p = 1` in main is a use-after-free.
+// Property: G valid-deref
+// Preprocessed equivalent of the sv-witnesses concurrent-mem-safety.c example.
+
+typedef unsigned long int pthread_t;
+union pthread_attr_t { char __size[56]; long int __align; };
+typedef union pthread_attr_t pthread_attr_t;
+extern int pthread_create(pthread_t *__newthread, const pthread_attr_t *__attr, void *(*__start_routine)(void *), void *__arg);
+extern int pthread_join(pthread_t __th, void **__thread_return);
+
+typedef unsigned long size_t;
+extern void free(void *ptr);
+extern void *malloc(size_t size);
+
+int freed = 0;
+int *p;
+
+void *freer(void *arg) {
+    free(p);
+    freed = 1;
+    return ((void *)0);
+}
+
+int main(void) {
+    p = malloc(sizeof(int));
+    pthread_t t;
+    pthread_create(&t, ((void *)0), freer, ((void *)0));
+    if (freed == 1) {
+        *p = 1;
+    }
+    pthread_join(t, ((void *)0));
+    return 0;
+}

example/concurrent-mem-safety.witness-2.2.yml

@@ -0,0 +1,73 @@
+# Violation witness (format 2.2) for example/concurrent-mem-safety.i.
+# Property: G valid-deref (no invalid pointer dereference allowed).
+# The freer thread frees p before main dereferences it, so `*p = 1` in main is
+# a use-after-free, detected at runtime by AddressSanitizer.
+
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.2"
+    uuid: "f5a6b7c8-d9e0-4012-ef01-3456789abcde"
+    creation_time: "2026-06-20T12:00:00Z"
+    producer:
+      name: "Handcrafted"
+      version: "1.0"
+    task:
+      input_files:
+        - "example/concurrent-mem-safety.i"
+      input_file_hashes:
+        "example/concurrent-mem-safety.i": "90cd9b8c8ede6046a0feeabb1af2cb7a6164a2893689d2ac81cd5702c68b879e"
+      specification: "G valid-deref"
+      data_model: "ILP32"
+      language: "C"
+  content:
+  - segment:
+    - waypoint:
+        # registers freer as thread 1 (1st function_enter'd pthread_create)
+        type: function_enter
+        action: follow
+        thread_id: 0
+        location:
+          file_name: "example/concurrent-mem-safety.i"
+          line: 28
+          column: 55
+          function: "main"
+  - segment:
+    - waypoint:
+        # thread 1 has freed p: at its return (after `free(p); freed = 1;`)
+        # freed is 1. Placing this in an earlier segment than main's
+        # dereference makes the free happen-before it.
+        type: assumption
+        action: follow
+        thread_id: 1
+        constraint:
+          value: "freed == 1"
+          format: c_expression
+        location:
+          file_name: "example/concurrent-mem-safety.i"
+          line: 22
+          column: 5
+          function: "freer"
+  - segment:
+    - waypoint:
+        # main observes freed == 1, so the branch is taken
+        type: branching
+        action: follow
+        thread_id: 0
+        constraint:
+          value: "true"
+        location:
+          file_name: "example/concurrent-mem-safety.i"
+          line: 29
+          column: 5
+          function: "main"
+  - segment:
+    - waypoint:
+        # the invalid dereference is the write through the freed pointer p
+        type: target
+        action: follow
+        thread_id: 0
+        location:
+          file_name: "example/concurrent-mem-safety.i"
+          line: 30
+          column: 9
+          function: "main"

example/concurrent-nondet.i

@@ -0,0 +1,29 @@
+// Concurrent violation with nondeterministic values and thread-ID tracking.
+// Thread 1 reads a nondet value; the witness pins it to 1 and orders the
+// write happens-before main's read so reach_error() is reachable.
+// Preprocessed for pycparser (no system headers).
+
+typedef unsigned long int pthread_t;
+union pthread_attr_t { char __size[56]; long int __align; };
+typedef union pthread_attr_t pthread_attr_t;
+extern int pthread_create(pthread_t *__newthread, const pthread_attr_t *__attr, void *(*__start_routine)(void *), void *__arg);
+extern int pthread_join(pthread_t __th, void **__thread_return);
+extern int __VERIFIER_nondet_int(void);
+void reach_error(void);
+
+int x = 0;
+
+void *writer(void *arg) {
+    x = __VERIFIER_nondet_int();
+    return ((void *)0);
+}
+
+int main(void) {
+    pthread_t t;
+    pthread_create(&t, ((void *)0), writer, ((void *)0));
+    if (x == 1) {
+        reach_error();
+    }
+    pthread_join(t, ((void *)0));
+    return 0;
+}

example/concurrent-nondet.witness-2.2.yml

@@ -0,0 +1,76 @@
+# Violation witness (format 2.2) for example/concurrent-nondet.i.
+# Exercises runtime thread-ID-checked nondet: the assumption is guarded by
+# both the segment counter AND the writer thread's logical ID (1), so the
+# value 1 is only injected when the writer thread is in the right epoch.
+
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.2"
+    uuid: "f6a7b8c9-d0e1-4234-efab-234567890123"
+    creation_time: "2026-06-20T12:00:00Z"
+    producer:
+      name: "Handcrafted"
+      version: "1.0"
+    task:
+      input_files:
+        - "example/concurrent-nondet.i"
+      input_file_hashes:
+        "example/concurrent-nondet.i": "9df7b208cf189fbce8fa3fb1fca92652b9bbd1ed948e8da3334f335d4c428020"
+      specification: "G ! call(reach_error())"
+      data_model: "ILP32"
+      language: "C"
+  content:
+  - segment:
+    - waypoint:
+        # Registers writer as thread 1 (1st thread-creating function_enter).
+        # Location is the right-after-name parenthesis of the pthread_create
+        # call (line 23, column 19) at which writer is spawned.
+        type: function_enter
+        action: follow
+        thread_id: 0
+        location:
+          file_name: "example/concurrent-nondet.i"
+          line: 23
+          column: 19
+          function: "main"
+  - segment:
+    - waypoint:
+        # writer's nondet: x = __VERIFIER_nondet_int() on line 17, guarded
+        # by slot==0 AND logical_tid==1.  Assumption anchored after line 18
+        # (the return) so the last nondet assignment to x at or before line 18
+        # is found (line 17).
+        type: assumption
+        action: follow
+        thread_id: 1
+        constraint:
+          value: "x == 1"
+          format: c_expression
+        location:
+          file_name: "example/concurrent-nondet.i"
+          line: 18
+          column: 5
+          function: "writer"
+  - segment:
+    - waypoint:
+        # main observes x == 1 and calls reach_error().
+        type: assumption
+        action: follow
+        thread_id: 0
+        constraint:
+          value: "x == 1"
+          format: c_expression
+        location:
+          file_name: "example/concurrent-nondet.i"
+          line: 24
+          column: 5
+          function: "main"
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        thread_id: 0
+        location:
+          file_name: "example/concurrent-nondet.i"
+          line: 25
+          column: 9
+          function: "main"

example/function-return.i

@@ -0,0 +1,19 @@
+// Property: G ! call(reach_error())
+// Demonstrates a function_return waypoint: the witness pins the return value
+// of get_value() so that the branch triggering reach_error() is taken.
+// Preprocessed for pycparser (no system headers).
+
+extern int __VERIFIER_nondet_int(void);
+void reach_error(void);
+
+int get_value(void) {
+    return __VERIFIER_nondet_int();
+}
+
+int main(void) {
+    int v = get_value();
+    if (v > 0) {
+        reach_error();
+    }
+    return 0;
+}

example/function-return.witness-2.2.yml

@@ -0,0 +1,45 @@
+# Violation witness (format 2.2) for example/function-return.i.
+# Property: G ! call(reach_error())
+# The function_return waypoint pins the return value of get_value() to 1
+# (positive), so the branch that calls reach_error() is taken.
+
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.2"
+    uuid: "e5f6a7b8-c9d0-4123-defa-123456789012"
+    creation_time: "2026-06-20T12:00:00Z"
+    producer:
+      name: "Handcrafted"
+      version: "1.0"
+    task:
+      input_files:
+        - "example/function-return.i"
+      input_file_hashes:
+        "example/function-return.i": "5a8d5665e66fa39bd2cbb439b2b47a3ca420a3cd30d1c596ba4a7b4f89fef070"
+      specification: "G ! call(reach_error())"
+      data_model: "ILP32"
+      language: "C"
+  content:
+  - segment:
+    - waypoint:
+        type: function_return
+        action: follow
+        thread_id: 0
+        constraint:
+          value: "\\result == 1"
+          format: ext_c_expression
+        location:
+          file_name: "example/function-return.i"
+          line: 10
+          column: 34
+          function: "get_value"
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        thread_id: 0
+        location:
+          file_name: "example/function-return.i"
+          line: 16
+          column: 9
+          function: "main"