diff --git a/example/README.md b/example/README.md index ca710402d5..ba28c07edc 100644 --- a/example/README.md +++ b/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 diff --git a/example/concurrent-mem-safety.i b/example/concurrent-mem-safety.i new file mode 100644 index 0000000000..0cfba18b08 --- /dev/null +++ b/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; +} diff --git a/example/concurrent-mem-safety.witness-2.2.yml b/example/concurrent-mem-safety.witness-2.2.yml new file mode 100644 index 0000000000..1066d5c283 --- /dev/null +++ b/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" diff --git a/example/concurrent-nondet.i b/example/concurrent-nondet.i new file mode 100644 index 0000000000..b4d6a5f730 --- /dev/null +++ b/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; +} diff --git a/example/concurrent-nondet.witness-2.2.yml b/example/concurrent-nondet.witness-2.2.yml new file mode 100644 index 0000000000..48da63415c --- /dev/null +++ b/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" diff --git a/example/function-return.i b/example/function-return.i new file mode 100644 index 0000000000..c7eeb77be9 --- /dev/null +++ b/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; +} diff --git a/example/function-return.witness-2.2.yml b/example/function-return.witness-2.2.yml new file mode 100644 index 0000000000..96c0b52789 --- /dev/null +++ b/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" diff --git a/example/mix000.opt.i b/example/mix000.opt.i deleted file mode 100644 index af6df9dd4d..0000000000 --- a/example/mix000.opt.i +++ /dev/null @@ -1,846 +0,0 @@ -extern _Bool __VERIFIER_nondet_bool(void); -extern void abort(void); -void assume_abort_if_not(int cond) { - if(!cond) {abort();} -} -extern _Bool __VERIFIER_nondet_bool(void); -extern void abort(void); - -extern void __assert_fail (const char *__assertion, const char *__file, - unsigned int __line, const char *__function) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); -extern void __assert_perror_fail (int __errnum, const char *__file, - unsigned int __line, const char *__function) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); -extern void __assert (const char *__assertion, const char *__file, int __line) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); - -void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "mix000.opt.c", 9, __extension__ __PRETTY_FUNCTION__); })); } -void __VERIFIER_assert(int expression) { if (!expression) { ERROR: {reach_error();abort();} }; return; } -extern void __VERIFIER_atomic_begin(); -extern void __VERIFIER_atomic_end(); - -extern void __assert_fail (const char *__assertion, const char *__file, - unsigned int __line, const char *__function) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); -extern void __assert_perror_fail (int __errnum, const char *__file, - unsigned int __line, const char *__function) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); -extern void __assert (const char *__assertion, const char *__file, int __line) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); - -typedef unsigned char __u_char; -typedef unsigned short int __u_short; -typedef unsigned int __u_int; -typedef unsigned long int __u_long; -typedef signed char __int8_t; -typedef unsigned char __uint8_t; -typedef signed short int __int16_t; -typedef unsigned short int __uint16_t; -typedef signed int __int32_t; -typedef unsigned int __uint32_t; -__extension__ typedef signed long long int __int64_t; -__extension__ typedef unsigned long long int __uint64_t; -__extension__ typedef long long int __quad_t; -__extension__ typedef unsigned long long int __u_quad_t; -__extension__ typedef long long int __intmax_t; -__extension__ typedef unsigned long long int __uintmax_t; -__extension__ typedef __u_quad_t __dev_t; -__extension__ typedef unsigned int __uid_t; -__extension__ typedef unsigned int __gid_t; -__extension__ typedef unsigned long int __ino_t; -__extension__ typedef __u_quad_t __ino64_t; -__extension__ typedef unsigned int __mode_t; -__extension__ typedef unsigned int __nlink_t; -__extension__ typedef long int __off_t; -__extension__ typedef __quad_t __off64_t; -__extension__ typedef int __pid_t; -__extension__ typedef struct { int __val[2]; } __fsid_t; -__extension__ typedef long int __clock_t; -__extension__ typedef unsigned long int __rlim_t; -__extension__ typedef __u_quad_t __rlim64_t; -__extension__ typedef unsigned int __id_t; -__extension__ typedef long int __time_t; -__extension__ typedef unsigned int __useconds_t; -__extension__ typedef long int __suseconds_t; -__extension__ typedef int __daddr_t; -__extension__ typedef int __key_t; -__extension__ typedef int __clockid_t; -__extension__ typedef void * __timer_t; -__extension__ typedef long int __blksize_t; -__extension__ typedef long int __blkcnt_t; -__extension__ typedef __quad_t __blkcnt64_t; -__extension__ typedef unsigned long int __fsblkcnt_t; -__extension__ typedef __u_quad_t __fsblkcnt64_t; -__extension__ typedef unsigned long int __fsfilcnt_t; -__extension__ typedef __u_quad_t __fsfilcnt64_t; -__extension__ typedef int __fsword_t; -__extension__ typedef int __ssize_t; -__extension__ typedef long int __syscall_slong_t; -__extension__ typedef unsigned long int __syscall_ulong_t; -typedef __off64_t __loff_t; -typedef char *__caddr_t; -__extension__ typedef int __intptr_t; -__extension__ typedef unsigned int __socklen_t; -typedef int __sig_atomic_t; -static __inline unsigned int -__bswap_32 (unsigned int __bsx) -{ - return __builtin_bswap32 (__bsx); -} -static __inline __uint64_t -__bswap_64 (__uint64_t __bsx) -{ - return __builtin_bswap64 (__bsx); -} -static __inline __uint16_t -__uint16_identity (__uint16_t __x) -{ - return __x; -} -static __inline __uint32_t -__uint32_identity (__uint32_t __x) -{ - return __x; -} -static __inline __uint64_t -__uint64_identity (__uint64_t __x) -{ - return __x; -} -typedef unsigned int size_t; -typedef __time_t time_t; -struct timespec -{ - __time_t tv_sec; - __syscall_slong_t tv_nsec; -}; -typedef __pid_t pid_t; -struct sched_param -{ - int sched_priority; -}; - - -typedef unsigned long int __cpu_mask; -typedef struct -{ - __cpu_mask __bits[1024 / (8 * sizeof (__cpu_mask))]; -} cpu_set_t; - -extern int __sched_cpucount (size_t __setsize, const cpu_set_t *__setp) - __attribute__ ((__nothrow__ , __leaf__)); -extern cpu_set_t *__sched_cpualloc (size_t __count) __attribute__ ((__nothrow__ , __leaf__)) ; -extern void __sched_cpufree (cpu_set_t *__set) __attribute__ ((__nothrow__ , __leaf__)); - - -extern int sched_setparam (__pid_t __pid, const struct sched_param *__param) - __attribute__ ((__nothrow__ , __leaf__)); -extern int sched_getparam (__pid_t __pid, struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__)); -extern int sched_setscheduler (__pid_t __pid, int __policy, - const struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__)); -extern int sched_getscheduler (__pid_t __pid) __attribute__ ((__nothrow__ , __leaf__)); -extern int sched_yield (void) __attribute__ ((__nothrow__ , __leaf__)); -extern int sched_get_priority_max (int __algorithm) __attribute__ ((__nothrow__ , __leaf__)); -extern int sched_get_priority_min (int __algorithm) __attribute__ ((__nothrow__ , __leaf__)); -extern int sched_rr_get_interval (__pid_t __pid, struct timespec *__t) __attribute__ ((__nothrow__ , __leaf__)); - -typedef __clock_t clock_t; -struct tm -{ - int tm_sec; - int tm_min; - int tm_hour; - int tm_mday; - int tm_mon; - int tm_year; - int tm_wday; - int tm_yday; - int tm_isdst; - long int tm_gmtoff; - const char *tm_zone; -}; -typedef __clockid_t clockid_t; -typedef __timer_t timer_t; -struct itimerspec - { - struct timespec it_interval; - struct timespec it_value; - }; -struct sigevent; -struct __locale_struct -{ - struct __locale_data *__locales[13]; - const unsigned short int *__ctype_b; - const int *__ctype_tolower; - const int *__ctype_toupper; - const char *__names[13]; -}; -typedef struct __locale_struct *__locale_t; -typedef __locale_t locale_t; - -extern clock_t clock (void) __attribute__ ((__nothrow__ , __leaf__)); -extern time_t time (time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); -extern double difftime (time_t __time1, time_t __time0) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); -extern time_t mktime (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); -extern size_t strftime (char *__restrict __s, size_t __maxsize, - const char *__restrict __format, - const struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); -extern size_t strftime_l (char *__restrict __s, size_t __maxsize, - const char *__restrict __format, - const struct tm *__restrict __tp, - locale_t __loc) __attribute__ ((__nothrow__ , __leaf__)); -extern struct tm *gmtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); -extern struct tm *localtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); -extern struct tm *gmtime_r (const time_t *__restrict __timer, - struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); -extern struct tm *localtime_r (const time_t *__restrict __timer, - struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__)); -extern char *asctime (const struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); -extern char *ctime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__)); -extern char *asctime_r (const struct tm *__restrict __tp, - char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__)); -extern char *ctime_r (const time_t *__restrict __timer, - char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__)); -extern char *__tzname[2]; -extern int __daylight; -extern long int __timezone; -extern char *tzname[2]; -extern void tzset (void) __attribute__ ((__nothrow__ , __leaf__)); -extern int daylight; -extern long int timezone; -extern int stime (const time_t *__when) __attribute__ ((__nothrow__ , __leaf__)); -extern time_t timegm (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); -extern time_t timelocal (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__)); -extern int dysize (int __year) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); -extern int nanosleep (const struct timespec *__requested_time, - struct timespec *__remaining); -extern int clock_getres (clockid_t __clock_id, struct timespec *__res) __attribute__ ((__nothrow__ , __leaf__)); -extern int clock_gettime (clockid_t __clock_id, struct timespec *__tp) __attribute__ ((__nothrow__ , __leaf__)); -extern int clock_settime (clockid_t __clock_id, const struct timespec *__tp) - __attribute__ ((__nothrow__ , __leaf__)); -extern int clock_nanosleep (clockid_t __clock_id, int __flags, - const struct timespec *__req, - struct timespec *__rem); -extern int clock_getcpuclockid (pid_t __pid, clockid_t *__clock_id) __attribute__ ((__nothrow__ , __leaf__)); -extern int timer_create (clockid_t __clock_id, - struct sigevent *__restrict __evp, - timer_t *__restrict __timerid) __attribute__ ((__nothrow__ , __leaf__)); -extern int timer_delete (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__)); -extern int timer_settime (timer_t __timerid, int __flags, - const struct itimerspec *__restrict __value, - struct itimerspec *__restrict __ovalue) __attribute__ ((__nothrow__ , __leaf__)); -extern int timer_gettime (timer_t __timerid, struct itimerspec *__value) - __attribute__ ((__nothrow__ , __leaf__)); -extern int timer_getoverrun (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__)); -extern int timespec_get (struct timespec *__ts, int __base) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); - -struct __pthread_rwlock_arch_t -{ - unsigned int __readers; - unsigned int __writers; - unsigned int __wrphase_futex; - unsigned int __writers_futex; - unsigned int __pad3; - unsigned int __pad4; - unsigned char __flags; - unsigned char __shared; - signed char __rwelision; - unsigned char __pad2; - int __cur_writer; -}; -typedef struct __pthread_internal_slist -{ - struct __pthread_internal_slist *__next; -} __pthread_slist_t; -struct __pthread_mutex_s -{ - int __lock ; - unsigned int __count; - int __owner; - int __kind; - - unsigned int __nusers; - __extension__ union - { - struct { short __espins; short __eelision; } __elision_data; - __pthread_slist_t __list; - }; - -}; -struct __pthread_cond_s -{ - __extension__ union - { - __extension__ unsigned long long int __wseq; - struct - { - unsigned int __low; - unsigned int __high; - } __wseq32; - }; - __extension__ union - { - __extension__ unsigned long long int __g1_start; - struct - { - unsigned int __low; - unsigned int __high; - } __g1_start32; - }; - unsigned int __g_refs[2] ; - unsigned int __g_size[2]; - unsigned int __g1_orig_size; - unsigned int __wrefs; - unsigned int __g_signals[2]; -}; -typedef unsigned long int pthread_t; -typedef union -{ - char __size[4]; - int __align; -} pthread_mutexattr_t; -typedef union -{ - char __size[4]; - int __align; -} pthread_condattr_t; -typedef unsigned int pthread_key_t; -typedef int pthread_once_t; -union pthread_attr_t -{ - char __size[36]; - long int __align; -}; -typedef union pthread_attr_t pthread_attr_t; -typedef union -{ - struct __pthread_mutex_s __data; - char __size[24]; - long int __align; -} pthread_mutex_t; -typedef union -{ - struct __pthread_cond_s __data; - char __size[48]; - __extension__ long long int __align; -} pthread_cond_t; -typedef union -{ - struct __pthread_rwlock_arch_t __data; - char __size[32]; - long int __align; -} pthread_rwlock_t; -typedef union -{ - char __size[8]; - long int __align; -} pthread_rwlockattr_t; -typedef volatile int pthread_spinlock_t; -typedef union -{ - char __size[20]; - long int __align; -} pthread_barrier_t; -typedef union -{ - char __size[4]; - int __align; -} pthread_barrierattr_t; -typedef int __jmp_buf[6]; -enum -{ - PTHREAD_CREATE_JOINABLE, - PTHREAD_CREATE_DETACHED -}; -enum -{ - PTHREAD_MUTEX_TIMED_NP, - PTHREAD_MUTEX_RECURSIVE_NP, - PTHREAD_MUTEX_ERRORCHECK_NP, - PTHREAD_MUTEX_ADAPTIVE_NP - , - PTHREAD_MUTEX_NORMAL = PTHREAD_MUTEX_TIMED_NP, - PTHREAD_MUTEX_RECURSIVE = PTHREAD_MUTEX_RECURSIVE_NP, - PTHREAD_MUTEX_ERRORCHECK = PTHREAD_MUTEX_ERRORCHECK_NP, - PTHREAD_MUTEX_DEFAULT = PTHREAD_MUTEX_NORMAL -}; -enum -{ - PTHREAD_MUTEX_STALLED, - PTHREAD_MUTEX_STALLED_NP = PTHREAD_MUTEX_STALLED, - PTHREAD_MUTEX_ROBUST, - PTHREAD_MUTEX_ROBUST_NP = PTHREAD_MUTEX_ROBUST -}; -enum -{ - PTHREAD_PRIO_NONE, - PTHREAD_PRIO_INHERIT, - PTHREAD_PRIO_PROTECT -}; -enum -{ - PTHREAD_RWLOCK_PREFER_READER_NP, - PTHREAD_RWLOCK_PREFER_WRITER_NP, - PTHREAD_RWLOCK_PREFER_WRITER_NONRECURSIVE_NP, - PTHREAD_RWLOCK_DEFAULT_NP = PTHREAD_RWLOCK_PREFER_READER_NP -}; -enum -{ - PTHREAD_INHERIT_SCHED, - PTHREAD_EXPLICIT_SCHED -}; -enum -{ - PTHREAD_SCOPE_SYSTEM, - PTHREAD_SCOPE_PROCESS -}; -enum -{ - PTHREAD_PROCESS_PRIVATE, - PTHREAD_PROCESS_SHARED -}; -struct _pthread_cleanup_buffer -{ - void (*__routine) (void *); - void *__arg; - int __canceltype; - struct _pthread_cleanup_buffer *__prev; -}; -enum -{ - PTHREAD_CANCEL_ENABLE, - PTHREAD_CANCEL_DISABLE -}; -enum -{ - PTHREAD_CANCEL_DEFERRED, - PTHREAD_CANCEL_ASYNCHRONOUS -}; - -extern int pthread_create (pthread_t *__restrict __newthread, - const pthread_attr_t *__restrict __attr, - void *(*__start_routine) (void *), - void *__restrict __arg) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 3))); -extern void pthread_exit (void *__retval) __attribute__ ((__noreturn__)); -extern int pthread_join (pthread_t __th, void **__thread_return); -extern int pthread_detach (pthread_t __th) __attribute__ ((__nothrow__ , __leaf__)); -extern pthread_t pthread_self (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); -extern int pthread_equal (pthread_t __thread1, pthread_t __thread2) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); -extern int pthread_attr_init (pthread_attr_t *__attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_attr_destroy (pthread_attr_t *__attr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_attr_getdetachstate (const pthread_attr_t *__attr, - int *__detachstate) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_attr_setdetachstate (pthread_attr_t *__attr, - int __detachstate) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_attr_getguardsize (const pthread_attr_t *__attr, - size_t *__guardsize) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_attr_setguardsize (pthread_attr_t *__attr, - size_t __guardsize) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_attr_getschedparam (const pthread_attr_t *__restrict __attr, - struct sched_param *__restrict __param) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_attr_setschedparam (pthread_attr_t *__restrict __attr, - const struct sched_param *__restrict - __param) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_attr_getschedpolicy (const pthread_attr_t *__restrict - __attr, int *__restrict __policy) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_attr_setschedpolicy (pthread_attr_t *__attr, int __policy) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_attr_getinheritsched (const pthread_attr_t *__restrict - __attr, int *__restrict __inherit) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_attr_setinheritsched (pthread_attr_t *__attr, - int __inherit) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_attr_getscope (const pthread_attr_t *__restrict __attr, - int *__restrict __scope) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_attr_setscope (pthread_attr_t *__attr, int __scope) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_attr_getstackaddr (const pthread_attr_t *__restrict - __attr, void **__restrict __stackaddr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))) __attribute__ ((__deprecated__)); -extern int pthread_attr_setstackaddr (pthread_attr_t *__attr, - void *__stackaddr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) __attribute__ ((__deprecated__)); -extern int pthread_attr_getstacksize (const pthread_attr_t *__restrict - __attr, size_t *__restrict __stacksize) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_attr_setstacksize (pthread_attr_t *__attr, - size_t __stacksize) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_attr_getstack (const pthread_attr_t *__restrict __attr, - void **__restrict __stackaddr, - size_t *__restrict __stacksize) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))); -extern int pthread_attr_setstack (pthread_attr_t *__attr, void *__stackaddr, - size_t __stacksize) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_setschedparam (pthread_t __target_thread, int __policy, - const struct sched_param *__param) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))); -extern int pthread_getschedparam (pthread_t __target_thread, - int *__restrict __policy, - struct sched_param *__restrict __param) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 3))); -extern int pthread_setschedprio (pthread_t __target_thread, int __prio) - __attribute__ ((__nothrow__ , __leaf__)); -extern int pthread_once (pthread_once_t *__once_control, - void (*__init_routine) (void)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_setcancelstate (int __state, int *__oldstate); -extern int pthread_setcanceltype (int __type, int *__oldtype); -extern int pthread_cancel (pthread_t __th); -extern void pthread_testcancel (void); -typedef struct -{ - struct - { - __jmp_buf __cancel_jmp_buf; - int __mask_was_saved; - } __cancel_jmp_buf[1]; - void *__pad[4]; -} __pthread_unwind_buf_t __attribute__ ((__aligned__)); -struct __pthread_cleanup_frame -{ - void (*__cancel_routine) (void *); - void *__cancel_arg; - int __do_it; - int __cancel_type; -}; -extern void __pthread_register_cancel (__pthread_unwind_buf_t *__buf) - __attribute__ ((__regparm__ (1))); -extern void __pthread_unregister_cancel (__pthread_unwind_buf_t *__buf) - __attribute__ ((__regparm__ (1))); -extern void __pthread_unwind_next (__pthread_unwind_buf_t *__buf) - __attribute__ ((__regparm__ (1))) __attribute__ ((__noreturn__)) - __attribute__ ((__weak__)) - ; -struct __jmp_buf_tag; -extern int __sigsetjmp (struct __jmp_buf_tag *__env, int __savemask) __attribute__ ((__nothrow__)); -extern int pthread_mutex_init (pthread_mutex_t *__mutex, - const pthread_mutexattr_t *__mutexattr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutex_destroy (pthread_mutex_t *__mutex) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutex_trylock (pthread_mutex_t *__mutex) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutex_lock (pthread_mutex_t *__mutex) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutex_timedlock (pthread_mutex_t *__restrict __mutex, - const struct timespec *__restrict - __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_mutex_unlock (pthread_mutex_t *__mutex) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutex_getprioceiling (const pthread_mutex_t * - __restrict __mutex, - int *__restrict __prioceiling) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_mutex_setprioceiling (pthread_mutex_t *__restrict __mutex, - int __prioceiling, - int *__restrict __old_ceiling) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 3))); -extern int pthread_mutex_consistent (pthread_mutex_t *__mutex) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutexattr_init (pthread_mutexattr_t *__attr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutexattr_destroy (pthread_mutexattr_t *__attr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutexattr_getpshared (const pthread_mutexattr_t * - __restrict __attr, - int *__restrict __pshared) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_mutexattr_setpshared (pthread_mutexattr_t *__attr, - int __pshared) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutexattr_gettype (const pthread_mutexattr_t *__restrict - __attr, int *__restrict __kind) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_mutexattr_settype (pthread_mutexattr_t *__attr, int __kind) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutexattr_getprotocol (const pthread_mutexattr_t * - __restrict __attr, - int *__restrict __protocol) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_mutexattr_setprotocol (pthread_mutexattr_t *__attr, - int __protocol) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutexattr_getprioceiling (const pthread_mutexattr_t * - __restrict __attr, - int *__restrict __prioceiling) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_mutexattr_setprioceiling (pthread_mutexattr_t *__attr, - int __prioceiling) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_mutexattr_getrobust (const pthread_mutexattr_t *__attr, - int *__robustness) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_mutexattr_setrobust (pthread_mutexattr_t *__attr, - int __robustness) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlock_init (pthread_rwlock_t *__restrict __rwlock, - const pthread_rwlockattr_t *__restrict - __attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlock_destroy (pthread_rwlock_t *__rwlock) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlock_rdlock (pthread_rwlock_t *__rwlock) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlock_tryrdlock (pthread_rwlock_t *__rwlock) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlock_timedrdlock (pthread_rwlock_t *__restrict __rwlock, - const struct timespec *__restrict - __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_rwlock_wrlock (pthread_rwlock_t *__rwlock) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlock_trywrlock (pthread_rwlock_t *__rwlock) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlock_timedwrlock (pthread_rwlock_t *__restrict __rwlock, - const struct timespec *__restrict - __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_rwlock_unlock (pthread_rwlock_t *__rwlock) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlockattr_init (pthread_rwlockattr_t *__attr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlockattr_destroy (pthread_rwlockattr_t *__attr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlockattr_getpshared (const pthread_rwlockattr_t * - __restrict __attr, - int *__restrict __pshared) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_rwlockattr_setpshared (pthread_rwlockattr_t *__attr, - int __pshared) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_rwlockattr_getkind_np (const pthread_rwlockattr_t * - __restrict __attr, - int *__restrict __pref) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_rwlockattr_setkind_np (pthread_rwlockattr_t *__attr, - int __pref) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_cond_init (pthread_cond_t *__restrict __cond, - const pthread_condattr_t *__restrict __cond_attr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_cond_destroy (pthread_cond_t *__cond) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_cond_signal (pthread_cond_t *__cond) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_cond_broadcast (pthread_cond_t *__cond) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_cond_wait (pthread_cond_t *__restrict __cond, - pthread_mutex_t *__restrict __mutex) - __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_cond_timedwait (pthread_cond_t *__restrict __cond, - pthread_mutex_t *__restrict __mutex, - const struct timespec *__restrict __abstime) - __attribute__ ((__nonnull__ (1, 2, 3))); -extern int pthread_condattr_init (pthread_condattr_t *__attr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_condattr_destroy (pthread_condattr_t *__attr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_condattr_getpshared (const pthread_condattr_t * - __restrict __attr, - int *__restrict __pshared) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_condattr_setpshared (pthread_condattr_t *__attr, - int __pshared) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_condattr_getclock (const pthread_condattr_t * - __restrict __attr, - __clockid_t *__restrict __clock_id) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_condattr_setclock (pthread_condattr_t *__attr, - __clockid_t __clock_id) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_spin_init (pthread_spinlock_t *__lock, int __pshared) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_spin_destroy (pthread_spinlock_t *__lock) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_spin_lock (pthread_spinlock_t *__lock) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_spin_trylock (pthread_spinlock_t *__lock) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_spin_unlock (pthread_spinlock_t *__lock) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_barrier_init (pthread_barrier_t *__restrict __barrier, - const pthread_barrierattr_t *__restrict - __attr, unsigned int __count) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_barrier_destroy (pthread_barrier_t *__barrier) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_barrier_wait (pthread_barrier_t *__barrier) - __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_barrierattr_init (pthread_barrierattr_t *__attr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_barrierattr_destroy (pthread_barrierattr_t *__attr) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_barrierattr_getpshared (const pthread_barrierattr_t * - __restrict __attr, - int *__restrict __pshared) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); -extern int pthread_barrierattr_setpshared (pthread_barrierattr_t *__attr, - int __pshared) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_key_create (pthread_key_t *__key, - void (*__destr_function) (void *)) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); -extern int pthread_key_delete (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__)); -extern void *pthread_getspecific (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__)); -extern int pthread_setspecific (pthread_key_t __key, - const void *__pointer) __attribute__ ((__nothrow__ , __leaf__)) ; -extern int pthread_getcpuclockid (pthread_t __thread_id, - __clockid_t *__clock_id) - __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); -extern int pthread_atfork (void (*__prepare) (void), - void (*__parent) (void), - void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__)); - -void * P0(void *arg); -void * P1(void *arg); -void fence(); -void isync(); -void lwfence(); -int __unbuffered_cnt; -int __unbuffered_cnt = 0; -int __unbuffered_p0_EAX; -int __unbuffered_p0_EAX = 0; -int __unbuffered_p0_EBX; -int __unbuffered_p0_EBX = 0; -int __unbuffered_p1_EAX; -int __unbuffered_p1_EAX = 0; -int __unbuffered_p1_EBX; -int __unbuffered_p1_EBX = 0; -_Bool main$tmp_guard0; -_Bool main$tmp_guard1; -int x; -int x = 0; -_Bool x$flush_delayed; -int x$mem_tmp; -_Bool x$r_buff0_thd0; -_Bool x$r_buff0_thd1; -_Bool x$r_buff0_thd2; -_Bool x$r_buff1_thd0; -_Bool x$r_buff1_thd1; -_Bool x$r_buff1_thd2; -_Bool x$read_delayed; -int *x$read_delayed_var; -int x$w_buff0; -_Bool x$w_buff0_used; -int x$w_buff1; -_Bool x$w_buff1_used; -int y; -int y = 0; -_Bool weak$$choice0; -_Bool weak$$choice2; -void * P0(void *arg) -{ - __VERIFIER_atomic_begin(); - y = 1; - __VERIFIER_atomic_end(); - __VERIFIER_atomic_begin(); - __unbuffered_p0_EAX = y; - __VERIFIER_atomic_end(); - __VERIFIER_atomic_begin(); - weak$$choice0 = __VERIFIER_nondet_bool(); - weak$$choice2 = __VERIFIER_nondet_bool(); - x$flush_delayed = weak$$choice2; - x$mem_tmp = x; - x = !x$w_buff0_used || !x$r_buff0_thd1 && !x$w_buff1_used || !x$r_buff0_thd1 && !x$r_buff1_thd1 ? x : (x$w_buff0_used && x$r_buff0_thd1 ? x$w_buff0 : x$w_buff1); - x$w_buff0 = weak$$choice2 ? x$w_buff0 : (!x$w_buff0_used || !x$r_buff0_thd1 && !x$w_buff1_used || !x$r_buff0_thd1 && !x$r_buff1_thd1 ? x$w_buff0 : (x$w_buff0_used && x$r_buff0_thd1 ? x$w_buff0 : x$w_buff0)); - x$w_buff1 = weak$$choice2 ? x$w_buff1 : (!x$w_buff0_used || !x$r_buff0_thd1 && !x$w_buff1_used || !x$r_buff0_thd1 && !x$r_buff1_thd1 ? x$w_buff1 : (x$w_buff0_used && x$r_buff0_thd1 ? x$w_buff1 : x$w_buff1)); - x$w_buff0_used = weak$$choice2 ? x$w_buff0_used : (!x$w_buff0_used || !x$r_buff0_thd1 && !x$w_buff1_used || !x$r_buff0_thd1 && !x$r_buff1_thd1 ? x$w_buff0_used : (x$w_buff0_used && x$r_buff0_thd1 ? (_Bool)0 : x$w_buff0_used)); - x$w_buff1_used = weak$$choice2 ? x$w_buff1_used : (!x$w_buff0_used || !x$r_buff0_thd1 && !x$w_buff1_used || !x$r_buff0_thd1 && !x$r_buff1_thd1 ? x$w_buff1_used : (x$w_buff0_used && x$r_buff0_thd1 ? (_Bool)0 : (_Bool)0)); - x$r_buff0_thd1 = weak$$choice2 ? x$r_buff0_thd1 : (!x$w_buff0_used || !x$r_buff0_thd1 && !x$w_buff1_used || !x$r_buff0_thd1 && !x$r_buff1_thd1 ? x$r_buff0_thd1 : (x$w_buff0_used && x$r_buff0_thd1 ? (_Bool)0 : x$r_buff0_thd1)); - x$r_buff1_thd1 = weak$$choice2 ? x$r_buff1_thd1 : (!x$w_buff0_used || !x$r_buff0_thd1 && !x$w_buff1_used || !x$r_buff0_thd1 && !x$r_buff1_thd1 ? x$r_buff1_thd1 : (x$w_buff0_used && x$r_buff0_thd1 ? (_Bool)0 : (_Bool)0)); - __unbuffered_p0_EBX = x; - x = x$flush_delayed ? x$mem_tmp : x; - x$flush_delayed = (_Bool)0; - __VERIFIER_atomic_end(); - __VERIFIER_atomic_begin(); - __VERIFIER_atomic_end(); - __VERIFIER_atomic_begin(); - __unbuffered_cnt = __unbuffered_cnt + 1; - __VERIFIER_atomic_end(); - return 0; -} -void * P1(void *arg) -{ - __VERIFIER_atomic_begin(); - x$w_buff1 = x$w_buff0; - x$w_buff0 = 1; - x$w_buff1_used = x$w_buff0_used; - x$w_buff0_used = (_Bool)1; - __VERIFIER_assert(!(x$w_buff1_used && x$w_buff0_used)); - x$r_buff1_thd0 = x$r_buff0_thd0; - x$r_buff1_thd1 = x$r_buff0_thd1; - x$r_buff1_thd2 = x$r_buff0_thd2; - x$r_buff0_thd2 = (_Bool)1; - __VERIFIER_atomic_end(); - __VERIFIER_atomic_begin(); - weak$$choice0 = __VERIFIER_nondet_bool(); - weak$$choice2 = __VERIFIER_nondet_bool(); - x$flush_delayed = weak$$choice2; - x$mem_tmp = x; - x = !x$w_buff0_used || !x$r_buff0_thd2 && !x$w_buff1_used || !x$r_buff0_thd2 && !x$r_buff1_thd2 ? x : (x$w_buff0_used && x$r_buff0_thd2 ? x$w_buff0 : x$w_buff1); - x$w_buff0 = weak$$choice2 ? x$w_buff0 : (!x$w_buff0_used || !x$r_buff0_thd2 && !x$w_buff1_used || !x$r_buff0_thd2 && !x$r_buff1_thd2 ? x$w_buff0 : (x$w_buff0_used && x$r_buff0_thd2 ? x$w_buff0 : x$w_buff0)); - x$w_buff1 = weak$$choice2 ? x$w_buff1 : (!x$w_buff0_used || !x$r_buff0_thd2 && !x$w_buff1_used || !x$r_buff0_thd2 && !x$r_buff1_thd2 ? x$w_buff1 : (x$w_buff0_used && x$r_buff0_thd2 ? x$w_buff1 : x$w_buff1)); - x$w_buff0_used = weak$$choice2 ? x$w_buff0_used : (!x$w_buff0_used || !x$r_buff0_thd2 && !x$w_buff1_used || !x$r_buff0_thd2 && !x$r_buff1_thd2 ? x$w_buff0_used : (x$w_buff0_used && x$r_buff0_thd2 ? (_Bool)0 : x$w_buff0_used)); - x$w_buff1_used = weak$$choice2 ? x$w_buff1_used : (!x$w_buff0_used || !x$r_buff0_thd2 && !x$w_buff1_used || !x$r_buff0_thd2 && !x$r_buff1_thd2 ? x$w_buff1_used : (x$w_buff0_used && x$r_buff0_thd2 ? (_Bool)0 : (_Bool)0)); - x$r_buff0_thd2 = weak$$choice2 ? x$r_buff0_thd2 : (!x$w_buff0_used || !x$r_buff0_thd2 && !x$w_buff1_used || !x$r_buff0_thd2 && !x$r_buff1_thd2 ? x$r_buff0_thd2 : (x$w_buff0_used && x$r_buff0_thd2 ? (_Bool)0 : x$r_buff0_thd2)); - x$r_buff1_thd2 = weak$$choice2 ? x$r_buff1_thd2 : (!x$w_buff0_used || !x$r_buff0_thd2 && !x$w_buff1_used || !x$r_buff0_thd2 && !x$r_buff1_thd2 ? x$r_buff1_thd2 : (x$w_buff0_used && x$r_buff0_thd2 ? (_Bool)0 : (_Bool)0)); - __unbuffered_p1_EAX = x; - x = x$flush_delayed ? x$mem_tmp : x; - x$flush_delayed = (_Bool)0; - __VERIFIER_atomic_end(); - __VERIFIER_atomic_begin(); - __unbuffered_p1_EBX = y; - __VERIFIER_atomic_end(); - __VERIFIER_atomic_begin(); - x = x$w_buff0_used && x$r_buff0_thd2 ? x$w_buff0 : (x$w_buff1_used && x$r_buff1_thd2 ? x$w_buff1 : x); - x$w_buff0_used = x$w_buff0_used && x$r_buff0_thd2 ? (_Bool)0 : x$w_buff0_used; - x$w_buff1_used = x$w_buff0_used && x$r_buff0_thd2 || x$w_buff1_used && x$r_buff1_thd2 ? (_Bool)0 : x$w_buff1_used; - x$r_buff0_thd2 = x$w_buff0_used && x$r_buff0_thd2 ? (_Bool)0 : x$r_buff0_thd2; - x$r_buff1_thd2 = x$w_buff0_used && x$r_buff0_thd2 || x$w_buff1_used && x$r_buff1_thd2 ? (_Bool)0 : x$r_buff1_thd2; - __VERIFIER_atomic_end(); - __VERIFIER_atomic_begin(); - __unbuffered_cnt = __unbuffered_cnt + 1; - __VERIFIER_atomic_end(); - return 0; -} -void fence() -{ -} -void isync() -{ -} -void lwfence() -{ -} -int main() -{ - pthread_t t0; - pthread_create(&t0, ((void *)0), P0, ((void *)0)); - pthread_t t1; - pthread_create(&t1, ((void *)0), P1, ((void *)0)); - __VERIFIER_atomic_begin(); - main$tmp_guard0 = __unbuffered_cnt == 2; - __VERIFIER_atomic_end(); - assume_abort_if_not(main$tmp_guard0); - __VERIFIER_atomic_begin(); - x = x$w_buff0_used && x$r_buff0_thd0 ? x$w_buff0 : (x$w_buff1_used && x$r_buff1_thd0 ? x$w_buff1 : x); - x$w_buff0_used = x$w_buff0_used && x$r_buff0_thd0 ? (_Bool)0 : x$w_buff0_used; - x$w_buff1_used = x$w_buff0_used && x$r_buff0_thd0 || x$w_buff1_used && x$r_buff1_thd0 ? (_Bool)0 : x$w_buff1_used; - x$r_buff0_thd0 = x$w_buff0_used && x$r_buff0_thd0 ? (_Bool)0 : x$r_buff0_thd0; - x$r_buff1_thd0 = x$w_buff0_used && x$r_buff0_thd0 || x$w_buff1_used && x$r_buff1_thd0 ? (_Bool)0 : x$r_buff1_thd0; - __VERIFIER_atomic_end(); - __VERIFIER_atomic_begin(); - main$tmp_guard1 = !(__unbuffered_p0_EAX == 1 && __unbuffered_p0_EBX == 0 && __unbuffered_p1_EAX == 1 && __unbuffered_p1_EBX == 0); - __VERIFIER_atomic_end(); - __VERIFIER_assert(main$tmp_guard1); - return 0; -} diff --git a/example/mix000.opt.i.graphml b/example/mix000.opt.i.graphml deleted file mode 100644 index 506063bfe0..0000000000 --- a/example/mix000.opt.i.graphml +++ /dev/null @@ -1,1010 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - false - - - false - - - false - - - - - - violation_witness - theta - C - CHECK( init(main()), LTL(G ! call(reach_error())) ) - /tmp/xcfa6438726142514960239.json - 1427344bf8c0905b63504a8f0111a13fe3d44cc48057d77274e52687b545a602 - 32bit - 2024-11-05T02:45:49Z - - true - - - {0=[main_init {init}]} - {0=[<unknown>]} - (ExplState) - - - {0=[main_init {init}]} - {0=[<unknown>]} - (ExplState) - - - - {0=[__loc_569 ]} - {0=[<unknown>]} - (ExplState (T0::_::main::t0 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 0) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (weak$$choice0 0) (weak$$choice2 0) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 0) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 0) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - - - - {0=[__loc_598 ], 30=[P0_init {init}]} - {0=[<unknown>], 30=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 0) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (weak$$choice0 0) (weak$$choice2 0) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 0) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 0) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - - - {0=[__loc_603 ], 30=[P0_init {init}], 32=[P1_init {init}]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 0) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 0) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 0) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 0) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - {0=[__loc_603 ], 30=[P0_init {init}], 32=[P1_init {init}]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 0) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 0) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 0) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 0) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - {0=[__loc_603 ], 30=[P0_init {init}], 32=[P1_init {init}]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 0) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 0) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 0) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 0) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - {0=[__loc_603 ], 30=[__loc_66 ], 32=[P1_init {init}]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 0) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 0) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 0) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 0) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - {0=[__loc_603 ], 30=[__loc_66 ], 32=[__loc_257 ]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 0) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 0) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 0) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 0) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - - - - - - - {0=[__loc_603 ], 30=[__loc_66 ], 32=[__loc_42_719 ]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 0) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 0) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 0) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 1) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - - - - - - - - - {0=[__loc_603 ], 30=[__loc_66 ], 32=[__loc_338 ]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 0) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 0) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 1) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - - - - - - - - - - - - - - - - - - - {0=[__loc_603 ], 30=[__loc_66 ], 32=[__loc_452 ]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 1) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - - - - {0=[__loc_603 ], 30=[__loc_66 ], 32=[__loc_471 ]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 1) (x$w_buff1 0) (x$w_buff1_used 0) (y 0)) - - - - - - {0=[__loc_603 ], 30=[__loc_85 ], 32=[__loc_471 ]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 0) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 1) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - - - {0=[__loc_603 ], 30=[__loc_104 ], 32=[__loc_471 ]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 1) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - - - - - - - - - - - - - - - - - - {0=[__loc_603 ], 30=[__loc_218 ], 32=[__loc_471 ]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 1) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - - {0=[__loc_603 ], 30=[__loc_230 ], 32=[__loc_471 ]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 0) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 1) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - - - - {0=[__loc_603 ], 30=[P0_final {final}], 32=[__loc_471 ]} - {0=[<unknown>], 30=[<unknown>], 32=[<unknown>]} - (ExplState (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 1) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 1) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - {0=[__loc_603 ], 32=[__loc_471 ]} - {0=[<unknown>], 32=[<unknown>]} - (ExplState (P0_ret 0) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 1) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 0) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 1) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - - - - - - - {0=[__loc_603 ], 32=[__loc_518 ]} - {0=[<unknown>], 32=[<unknown>]} - (ExplState (P0_ret 0) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 1) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 1) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - - - - {0=[__loc_603 ], 32=[P1_final {final}]} - {0=[<unknown>], 32=[<unknown>]} - (ExplState (P0_ret 0) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::P1_ret 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 2) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 1) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - {0=[__loc_603 ]} - {0=[<unknown>]} - (ExplState (P0_ret 0) (P1_ret 0) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::P1_ret 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 2) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 0) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 1) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - - - {0=[__loc_626 ]} - {0=[<unknown>]} - (ExplState (P0_ret 0) (P1_ret 0) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::P1_ret 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 2) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 1) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 1) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - {0=[__loc_8_749 ]} - {0=[<unknown>]} - (ExplState (P0_ret 0) (P1_ret 0) (T0::_::assume_abort_if_not::cond 1) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::P1_ret 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 2) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 1) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 1) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - - {0=[__loc_631 ]} - {0=[<unknown>]} - (ExplState (P0_ret 0) (P1_ret 0) (T0::_::assume_abort_if_not::cond 1) (T0::_::assume_abort_if_not_ret 5) (T0::_::call_assume_abort_if_not_ret32 5) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::P1_ret 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 2) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 1) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 1) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - - - - - - - {0=[__loc_678 ]} - {0=[<unknown>]} - (ExplState (P0_ret 0) (P1_ret 0) (T0::_::assume_abort_if_not::cond 1) (T0::_::assume_abort_if_not_ret 5) (T0::_::call_assume_abort_if_not_ret32 5) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::P1_ret 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 2) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 1) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 1) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - - - {0=[__loc_701 ]} - {0=[<unknown>]} - (ExplState (P0_ret 0) (P1_ret 0) (T0::_::assume_abort_if_not::cond 1) (T0::_::assume_abort_if_not_ret 5) (T0::_::call_assume_abort_if_not_ret32 5) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::P1_ret 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 2) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 1) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 1) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - {0=[__loc_42_768 ]} - {0=[<unknown>]} - (ExplState (P0_ret 0) (P1_ret 0) (T0::_::__VERIFIER_assert::expression 0) (T0::_::assume_abort_if_not::cond 1) (T0::_::assume_abort_if_not_ret 5) (T0::_::call_assume_abort_if_not_ret32 5) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::P1_ret 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 2) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 1) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 1) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - true - {0=[main_error {error}]} - {0=[<unknown>]} - (ExplState (P0_ret 0) (P1_ret 0) (T0::_::__VERIFIER_assert::expression 0) (T0::_::assume_abort_if_not::cond 1) (T0::_::assume_abort_if_not_ret 5) (T0::_::call_assume_abort_if_not_ret32 5) (T0::_::main::t0 0) (T0::_::main::t1 0) (T30::_::P0::arg 0) (T30::_::P0_ret 0) (T32::_::P1::arg 0) (T32::_::P1_ret 0) (T32::_::__VERIFIER_assert::expression 1) (T32::_::__VERIFIER_assert_ret 0) (T32::_::call___VERIFIER_assert_ret16 0) (__unbuffered_cnt 2) (__unbuffered_p0_EAX 1) (__unbuffered_p0_EBX 0) (__unbuffered_p1_EAX 1) (__unbuffered_p1_EBX 0) (main$tmp_guard0 1) (main$tmp_guard1 0) (tmp16_P0::arg 0) (tmp17_P1::arg 0) (weak$$choice0 0) (weak$$choice2 1) (x 1) (x$flush_delayed 0) (x$mem_tmp 0) (x$r_buff0_thd0 0) (x$r_buff0_thd1 0) (x$r_buff0_thd2 1) (x$r_buff1_thd0 0) (x$r_buff1_thd1 0) (x$r_buff1_thd2 0) (x$w_buff0 1) (x$w_buff0_used 0) (x$w_buff1 0) (x$w_buff1_used 0) (y 1)) - - - - 0 - - - 0 - - - condition-true - 0 - (assume (and (>= T0::_::main::t0 0) (<= T0::_::main::t0 4294967295))) - - - 0 - - - 827 - 827 - 36648 - 36697 - 0 - (assign tmp16_P0::arg (mod (mod 0 4294967296) 4294967296)) - pthread_create(&t0, ((void *)0), P0, ((void *)0)); - - - 827 - 827 - 36648 - 36697 - 0 - 30 - pthread_create(&t0, ((void *)0), P0, ((void *)0)); - - - condition-true - 0 - (assume (and (>= T0::_::main::t1 0) (<= T0::_::main::t1 4294967295))) - - - 0 - - - 829 - 829 - 36717 - 36766 - 0 - (assign tmp17_P1::arg (mod (mod 0 4294967296) 4294967296)) - pthread_create(&t1, ((void *)0), P1, ((void *)0)); - - - 829 - 829 - 36717 - 36766 - 0 - 32 - pthread_create(&t1, ((void *)0), P1, ((void *)0)); - - - 30 - - - 32 - - - 30 - - - 32 - - - 32 - - - 773 - 773 - 33679 - 33704 - 32 - __VERIFIER_atomic_begin(); - - - 32 - (assign x$w_buff1 x$w_buff0) - - - 32 - (assign x$w_buff0 1) - - - 32 - (assign x$w_buff1_used x$w_buff0_used) - - - 32 - (assign x$w_buff0_used 1) - - - 778 - 778 - 33814 - 33868 - 32 - (assign T32::_::__VERIFIER_assert::expression (ite (= (ite (and (/= 0 x$w_buff1_used) (/= 0 x$w_buff0_used)) 1 0) 0) 1 0)) - __VERIFIER_assert(!(x$w_buff1_used && x$w_buff0_used)); - - - 32 - - - condition-false - 19 - 19 - 960 - 1011 - 32 - (assume (= (ite (= T32::_::__VERIFIER_assert::expression 0) 1 0) 0)) - if (!expression) { ERROR: {reach_error();abort();} } - - - 19 - 19 - 1014 - 1020 - 32 - (assign T32::_::__VERIFIER_assert_ret 0) - return; - - - 778 - 778 - 33814 - 33868 - 32 - (assign T32::_::call___VERIFIER_assert_ret16 0) - __VERIFIER_assert(!(x$w_buff1_used && x$w_buff0_used)); - - - 32 - (assign x$r_buff1_thd0 x$r_buff0_thd0) - - - 32 - (assign x$r_buff1_thd1 x$r_buff0_thd1) - - - 32 - (assign x$r_buff1_thd2 x$r_buff0_thd2) - - - 32 - (assign x$r_buff0_thd2 1) - - - 783 - 783 - 34006 - 34029 - 32 - __VERIFIER_atomic_end(); - - - 32 - - - 784 - 784 - 34033 - 34058 - 32 - __VERIFIER_atomic_begin(); - - - weak$$choice0 == 0 - 785 - 785 - 34062 - 34102 - 32 - (havoc weak$$choice0) - weak$$choice0 = __VERIFIER_nondet_bool(); - - - 785 - 785 - 34062 - 34102 - 32 - (assume (and (>= weak$$choice0 0) (<= weak$$choice0 1))) - weak$$choice0 = __VERIFIER_nondet_bool(); - - - weak$$choice2 == 1 - 786 - 786 - 34106 - 34146 - 32 - (havoc weak$$choice2) - weak$$choice2 = __VERIFIER_nondet_bool(); - - - 786 - 786 - 34106 - 34146 - 32 - (assume (and (>= weak$$choice2 0) (<= weak$$choice2 1))) - weak$$choice2 = __VERIFIER_nondet_bool(); - - - 32 - (assign x$flush_delayed weak$$choice2) - - - 32 - (assign x$mem_tmp x) - - - 32 - (assign x (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd2 0) 1 0))) 1 0))) 1 0)) x (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) x$w_buff0 x$w_buff1))) - - - 32 - (assign x$w_buff0 (ite (/= 0 weak$$choice2) x$w_buff0 (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd2 0) 1 0))) 1 0))) 1 0)) x$w_buff0 (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) x$w_buff0 x$w_buff0)))) - - - 32 - (assign x$w_buff1 (ite (/= 0 weak$$choice2) x$w_buff1 (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd2 0) 1 0))) 1 0))) 1 0)) x$w_buff1 (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) x$w_buff1 x$w_buff1)))) - - - 32 - (assign x$w_buff0_used (ite (= (ite (/= 0 weak$$choice2) x$w_buff0_used (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd2 0) 1 0))) 1 0))) 1 0)) x$w_buff0_used (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) 0 x$w_buff0_used))) 0) 0 1)) - - - 32 - (assign x$w_buff1_used (ite (= (ite (/= 0 weak$$choice2) x$w_buff1_used (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd2 0) 1 0))) 1 0))) 1 0)) x$w_buff1_used (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) 0 0))) 0) 0 1)) - - - 32 - (assign x$r_buff0_thd2 (ite (= (ite (/= 0 weak$$choice2) x$r_buff0_thd2 (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd2 0) 1 0))) 1 0))) 1 0)) x$r_buff0_thd2 (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) 0 x$r_buff0_thd2))) 0) 0 1)) - - - 32 - (assign x$r_buff1_thd2 (ite (= (ite (/= 0 weak$$choice2) x$r_buff1_thd2 (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd2 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd2 0) 1 0))) 1 0))) 1 0)) x$r_buff1_thd2 (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) 0 0))) 0) 0 1)) - - - 32 - (assign __unbuffered_p1_EAX x) - - - 32 - (assign x (ite (/= 0 x$flush_delayed) x$mem_tmp x)) - - - 32 - (assign x$flush_delayed 0) - - - 799 - 799 - 35786 - 35809 - 32 - __VERIFIER_atomic_end(); - - - 32 - - - 800 - 800 - 35813 - 35838 - 32 - __VERIFIER_atomic_begin(); - - - 32 - (assign __unbuffered_p1_EBX y) - - - 802 - 802 - 35869 - 35892 - 32 - __VERIFIER_atomic_end(); - - - 30 - - - 742 - 742 - 31559 - 31584 - 30 - __VERIFIER_atomic_begin(); - - - 30 - (assign y 1) - - - 744 - 744 - 31597 - 31620 - 30 - __VERIFIER_atomic_end(); - - - 30 - - - 745 - 745 - 31624 - 31649 - 30 - __VERIFIER_atomic_begin(); - - - 30 - (assign __unbuffered_p0_EAX y) - - - 747 - 747 - 31680 - 31703 - 30 - __VERIFIER_atomic_end(); - - - 30 - - - 748 - 748 - 31707 - 31732 - 30 - __VERIFIER_atomic_begin(); - - - weak$$choice0 == 0 - 749 - 749 - 31736 - 31776 - 30 - (havoc weak$$choice0) - weak$$choice0 = __VERIFIER_nondet_bool(); - - - 749 - 749 - 31736 - 31776 - 30 - (assume (and (>= weak$$choice0 0) (<= weak$$choice0 1))) - weak$$choice0 = __VERIFIER_nondet_bool(); - - - weak$$choice2 == 1 - 750 - 750 - 31780 - 31820 - 30 - (havoc weak$$choice2) - weak$$choice2 = __VERIFIER_nondet_bool(); - - - 750 - 750 - 31780 - 31820 - 30 - (assume (and (>= weak$$choice2 0) (<= weak$$choice2 1))) - weak$$choice2 = __VERIFIER_nondet_bool(); - - - 30 - (assign x$flush_delayed weak$$choice2) - - - 30 - (assign x$mem_tmp x) - - - 30 - (assign x (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd1 0) 1 0))) 1 0))) 1 0)) x (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd1)) 1 0)) x$w_buff0 x$w_buff1))) - - - 30 - (assign x$w_buff0 (ite (/= 0 weak$$choice2) x$w_buff0 (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd1 0) 1 0))) 1 0))) 1 0)) x$w_buff0 (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd1)) 1 0)) x$w_buff0 x$w_buff0)))) - - - 30 - (assign x$w_buff1 (ite (/= 0 weak$$choice2) x$w_buff1 (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd1 0) 1 0))) 1 0))) 1 0)) x$w_buff1 (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd1)) 1 0)) x$w_buff1 x$w_buff1)))) - - - 30 - (assign x$w_buff0_used (ite (= (ite (/= 0 weak$$choice2) x$w_buff0_used (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd1 0) 1 0))) 1 0))) 1 0)) x$w_buff0_used (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd1)) 1 0)) 0 x$w_buff0_used))) 0) 0 1)) - - - 30 - (assign x$w_buff1_used (ite (= (ite (/= 0 weak$$choice2) x$w_buff1_used (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd1 0) 1 0))) 1 0))) 1 0)) x$w_buff1_used (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd1)) 1 0)) 0 0))) 0) 0 1)) - - - 30 - (assign x$r_buff0_thd1 (ite (= (ite (/= 0 weak$$choice2) x$r_buff0_thd1 (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd1 0) 1 0))) 1 0))) 1 0)) x$r_buff0_thd1 (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd1)) 1 0)) 0 x$r_buff0_thd1))) 0) 0 1)) - - - 30 - (assign x$r_buff1_thd1 (ite (= (ite (/= 0 weak$$choice2) x$r_buff1_thd1 (ite (/= 0 (ite (or (/= 0 (ite (= x$w_buff0_used 0) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$w_buff1_used 0) 1 0))) 1 0)) (/= 0 (ite (and (/= 0 (ite (= x$r_buff0_thd1 0) 1 0)) (/= 0 (ite (= x$r_buff1_thd1 0) 1 0))) 1 0))) 1 0)) x$r_buff1_thd1 (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd1)) 1 0)) 0 0))) 0) 0 1)) - - - 30 - (assign __unbuffered_p0_EBX x) - - - 30 - (assign x (ite (/= 0 x$flush_delayed) x$mem_tmp x)) - - - 30 - (assign x$flush_delayed 0) - - - 763 - 763 - 33460 - 33483 - 30 - __VERIFIER_atomic_end(); - - - 30 - - - 764 - 764 - 33487 - 33512 - 30 - __VERIFIER_atomic_begin(); - - - 765 - 765 - 33516 - 33539 - 30 - __VERIFIER_atomic_end(); - - - 30 - - - 766 - 766 - 33543 - 33568 - 30 - __VERIFIER_atomic_begin(); - - - 30 - (assign __unbuffered_cnt (+ __unbuffered_cnt 1)) - - - 768 - 768 - 33615 - 33638 - 30 - __VERIFIER_atomic_end(); - - - 769 - 769 - 33642 - 33650 - 30 - (assign T30::_::P0_ret 0) - return 0; - - - 30 - - - 32 - - - 803 - 803 - 35896 - 35921 - 32 - __VERIFIER_atomic_begin(); - - - 32 - (assign x (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) x$w_buff0 (ite (/= 0 (ite (and (/= 0 x$w_buff1_used) (/= 0 x$r_buff1_thd2)) 1 0)) x$w_buff1 x))) - - - 32 - (assign x$w_buff0_used (ite (= (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) 0 x$w_buff0_used) 0) 0 1)) - - - 32 - (assign x$w_buff1_used (ite (= (ite (/= 0 (ite (or (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) (/= 0 (ite (and (/= 0 x$w_buff1_used) (/= 0 x$r_buff1_thd2)) 1 0))) 1 0)) 0 x$w_buff1_used) 0) 0 1)) - - - 32 - (assign x$r_buff0_thd2 (ite (= (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) 0 x$r_buff0_thd2) 0) 0 1)) - - - 32 - (assign x$r_buff1_thd2 (ite (= (ite (/= 0 (ite (or (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd2)) 1 0)) (/= 0 (ite (and (/= 0 x$w_buff1_used) (/= 0 x$r_buff1_thd2)) 1 0))) 1 0)) 0 x$r_buff1_thd2) 0) 0 1)) - - - 809 - 809 - 36426 - 36449 - 32 - __VERIFIER_atomic_end(); - - - 32 - - - 810 - 810 - 36453 - 36478 - 32 - __VERIFIER_atomic_begin(); - - - 32 - (assign __unbuffered_cnt (+ __unbuffered_cnt 1)) - - - 812 - 812 - 36525 - 36548 - 32 - __VERIFIER_atomic_end(); - - - 813 - 813 - 36552 - 36560 - 32 - (assign T32::_::P1_ret 0) - return 0; - - - 32 - - - 0 - - - 830 - 830 - 36770 - 36795 - 0 - __VERIFIER_atomic_begin(); - - - 0 - (assign main$tmp_guard0 (ite (= (ite (= __unbuffered_cnt 2) 1 0) 0) 0 1)) - - - 832 - 832 - 36842 - 36865 - 0 - __VERIFIER_atomic_end(); - - - 0 - - - 833 - 833 - 36869 - 36905 - 0 - (assign T0::_::assume_abort_if_not::cond main$tmp_guard0) - assume_abort_if_not(main$tmp_guard0); - - - 0 - - - condition-false - 4 - 4 - 107 - 126 - 0 - (assume (= (ite (= T0::_::assume_abort_if_not::cond 0) 1 0) 0)) - if(!cond) {abort();} - - - 833 - 833 - 36869 - 36905 - 0 - (assign T0::_::call_assume_abort_if_not_ret32 T0::_::assume_abort_if_not_ret) - assume_abort_if_not(main$tmp_guard0); - - - 0 - - - 834 - 834 - 36909 - 36934 - 0 - __VERIFIER_atomic_begin(); - - - 0 - (assign x (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd0)) 1 0)) x$w_buff0 (ite (/= 0 (ite (and (/= 0 x$w_buff1_used) (/= 0 x$r_buff1_thd0)) 1 0)) x$w_buff1 x))) - - - 0 - (assign x$w_buff0_used (ite (= (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd0)) 1 0)) 0 x$w_buff0_used) 0) 0 1)) - - - 0 - (assign x$w_buff1_used (ite (= (ite (/= 0 (ite (or (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd0)) 1 0)) (/= 0 (ite (and (/= 0 x$w_buff1_used) (/= 0 x$r_buff1_thd0)) 1 0))) 1 0)) 0 x$w_buff1_used) 0) 0 1)) - - - 0 - (assign x$r_buff0_thd0 (ite (= (ite (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd0)) 1 0)) 0 x$r_buff0_thd0) 0) 0 1)) - - - 0 - (assign x$r_buff1_thd0 (ite (= (ite (/= 0 (ite (or (/= 0 (ite (and (/= 0 x$w_buff0_used) (/= 0 x$r_buff0_thd0)) 1 0)) (/= 0 (ite (and (/= 0 x$w_buff1_used) (/= 0 x$r_buff1_thd0)) 1 0))) 1 0)) 0 x$r_buff1_thd0) 0) 0 1)) - - - 840 - 840 - 37439 - 37462 - 0 - __VERIFIER_atomic_end(); - - - 0 - - - 841 - 841 - 37466 - 37491 - 0 - __VERIFIER_atomic_begin(); - - - 0 - (assign main$tmp_guard1 (ite (= (ite (= (ite (and (/= 0 (ite (= __unbuffered_p0_EAX 1) 1 0)) (/= 0 (ite (= __unbuffered_p0_EBX 0) 1 0)) (/= 0 (ite (= __unbuffered_p1_EAX 1) 1 0)) (/= 0 (ite (= __unbuffered_p1_EBX 0) 1 0))) 1 0) 0) 1 0) 0) 0 1)) - - - 843 - 843 - 37628 - 37651 - 0 - __VERIFIER_atomic_end(); - - - 0 - - - 844 - 844 - 37655 - 37689 - 0 - (assign T0::_::__VERIFIER_assert::expression main$tmp_guard1) - __VERIFIER_assert(main$tmp_guard1); - - - 0 - - - condition-true - 19 - 19 - 960 - 1011 - 0 - (assume (/= (ite (= T0::_::__VERIFIER_assert::expression 0) 1 0) 0)) - if (!expression) { ERROR: {reach_error();abort();} } - - - - diff --git a/example/no-overflow.i b/example/no-overflow.i new file mode 100644 index 0000000000..3d7d600f95 --- /dev/null +++ b/example/no-overflow.i @@ -0,0 +1,13 @@ +// Property: G ! overflow +// Demonstrates a no-overflow violation witness: the witness pins x to INT_MAX +// so that x + 1 overflows. Preprocessed for pycparser (no system headers). + +extern int __VERIFIER_nondet_int(void); + +int main(void) { + int x; + x = __VERIFIER_nondet_int(); + int y = x + 1; + (void)y; + return 0; +} diff --git a/example/no-overflow.witness-2.2.yml b/example/no-overflow.witness-2.2.yml new file mode 100644 index 0000000000..e37f4c717a --- /dev/null +++ b/example/no-overflow.witness-2.2.yml @@ -0,0 +1,53 @@ +# Violation witness (format 2.2) for example/no-overflow.i. +# Property: G ! overflow (no integer overflow allowed). +# The witness pins x to INT_MAX so that x + 1 triggers a signed-integer- +# overflow undefined-behaviour, detected at runtime by UBSan. + +- entry_type: violation_sequence + metadata: + format_version: "2.2" + uuid: "d4e5f6a7-b8c9-4012-cdef-01234567890a" + creation_time: "2026-06-20T12:00:00Z" + producer: + name: "Handcrafted" + version: "1.0" + task: + input_files: + - "example/no-overflow.i" + input_file_hashes: + "example/no-overflow.i": "ef35d6ca8c6a5f9104a6a601c8da82083dc54bd2aafa9f872b98691f0c92e680" + specification: "G ! overflow" + data_model: "ILP32" + language: "C" + content: + - segment: + - waypoint: + # YAML assumption anchor: at the sequence point *before* line 10 + # (first character of the statement), x == INT_MAX. The last nondet + # assignment to x before line 10 is line 9 (x = __VERIFIER_nondet_int()), + # which is wrapped to return INT_MAX when the segment counter and + # thread ID match. + type: assumption + action: follow + thread_id: 0 + constraint: + value: "x == 2147483647" + format: c_expression + location: + file_name: "example/no-overflow.i" + line: 10 + column: 5 + function: "main" + - segment: + - waypoint: + # The signed-integer overflow is in the evaluation of `x + 1`, whose + # containing statement is `int y = x + 1;` on line 10 -- the target + # location is its first character, per the Target waypoint rules. + type: target + action: follow + thread_id: 0 + location: + file_name: "example/no-overflow.i" + line: 10 + column: 5 + function: "main" diff --git a/main.py b/main.py index 407dce7ace..6360e3a54e 100644 --- a/main.py +++ b/main.py @@ -21,11 +21,17 @@ import traceback import argparse -from pycparser import preprocess_file, CParser, c_generator +from pycparser import preprocess_file, CParser from Exceptions import KnownErrorVerdict from hacks import hacks -from tweaks import reach_error, fix_inline, fix_struct_def, declare_schedule_functions +from tweaks import ( + reach_error, + fix_inline, + fix_struct_def, + declare_schedule_functions, + LineDirectiveCGenerator, +) from witness2ast import apply_witness HEADERS_DIR = os.path.dirname(os.path.abspath(sys.argv[0])) + os.sep + "headers" @@ -66,7 +72,9 @@ def translate_to_c(filename, witness, mode, timeout): sys.exit(-1) try: - parsed_witness = apply_witness(ast, filename, witness) + parsed_witness = apply_witness( + ast, filename, witness, input_only=(mode == "INPUT_ONLY") + ) except KnownErrorVerdict as e: print("Verdict: " + e.verdict) sys.exit(-1) @@ -81,12 +89,24 @@ def translate_to_c(filename, witness, mode, timeout): if data_race: print("Data race witness: compiling with ThreadSanitizer") + # For a no-overflow witness the violation is an integer overflow detected + # by UBSan at runtime. + no_overflow = parsed_witness.no_overflow + if no_overflow: + print("Overflow witness: compiling with UBSan") + + # For a memory-safety witness the violation is an invalid memory access + # (e.g. a use-after-free) detected by AddressSanitizer at runtime. + memory_safety = parsed_witness.memory_safety + if memory_safety: + print("Memory-safety witness: compiling with AddressSanitizer") + try: fix_inline(ast) fix_struct_def(ast) reach_error(ast) declare_schedule_functions(ast) - generator = c_generator.CGenerator() + generator = LineDirectiveCGenerator() with tempfile.NamedTemporaryFile(suffix=".c", delete=False) as tmp: tmp.write(generator.visit(ast).encode()) tmp.flush() @@ -101,6 +121,12 @@ def translate_to_c(filename, witness, mode, timeout): "-pthread", ] + (["-fsanitize=thread", "-g"] if data_race else []) + + ( + ["-fsanitize=undefined", "-fno-sanitize-recover=all", "-g"] + if no_overflow + else [] + ) + + (["-fsanitize=address", "-g"] if memory_safety else []) + [ tmp.name, os.path.dirname(os.path.abspath(sys.argv[0])) + os.sep + "svcomp.c", @@ -123,6 +149,16 @@ def translate_to_c(filename, witness, mode, timeout): # Stop at the first race and reuse the reach_error() exit # code, so race detection follows the same path below. env["TSAN_OPTIONS"] = "halt_on_error=1 exitcode=74" + if no_overflow: + # UBSan: halt on first overflow and exit with the same + # sentinel code 74 as reach_error(), so the verdict logic + # below is reused unchanged. + env["UBSAN_OPTIONS"] = "halt_on_error=1:exitcode=74:print_stacktrace=1" + if memory_safety: + # ASan: halt on the first invalid access and exit with the same + # sentinel code 74 as reach_error(), so the verdict logic below + # is reused unchanged. + env["ASAN_OPTIONS"] = "halt_on_error=1:exitcode=74" codes = {} for i in range(100): try: @@ -147,6 +183,20 @@ def translate_to_c(filename, witness, mode, timeout): and "ThreadSanitizer: data race" in result.stderr ): reached_error = True + if ( + not reached_error + and no_overflow + and result.stderr + and "runtime error:" in result.stderr + ): + reached_error = True + if ( + not reached_error + and memory_safety + and result.stderr + and "AddressSanitizer:" in result.stderr + ): + reached_error = True if result.stdout: print(result.stdout) if result.stderr: @@ -216,11 +266,14 @@ def parse_arguments(): ) parser.add_argument( "--mode", - choices=["strict", "normal", "permissive"], + choices=["strict", "normal", "permissive", "INPUT_ONLY"], default="normal", help="Mode (default: normal): strict stops at the first execution " "missing the error, permissive at the first one reaching it, " - "normal runs all repetitions", + "normal runs all repetitions, INPUT_ONLY pins the witness' inputs " + "(nondet values, assumptions) but leaves the thread schedule free " + "(no blocking schedule yields; the segment counter still advances " + "per passed segment)", ) parser.add_argument( "--timeout", diff --git a/smoketest.sh b/smoketest.sh index 268c9f448d..8065c91bad 100755 --- a/smoketest.sh +++ b/smoketest.sh @@ -7,13 +7,17 @@ check_verdict() { grep -q "Verdict: ALWAYS" <<< "$out" } -# GraphML (format 1.0) witness. The bundled witness is known to be -# incomplete (see example/README.md), so only successful test generation -# is checked here, not the verdict. -./start.sh example/mix000.opt.i --witness example/mix000.opt.i.graphml --mode permissive - # YAML (format 2.2) concurrent reachability witness check_verdict ./start.sh example/concurrent-unreach.i --witness example/concurrent-unreach.witness-2.2.yml --mode permissive # YAML (format 2.2) data race witness (requires gcc with ThreadSanitizer) check_verdict ./start.sh example/concurrent-data-race.i --witness example/concurrent-data-race.witness-2.2.yml --mode permissive + +# YAML (format 2.2) no-overflow witness (requires gcc with UBSan) +check_verdict ./start.sh example/no-overflow.i --witness example/no-overflow.witness-2.2.yml --mode permissive + +# YAML (format 2.2) function_return waypoint witness +check_verdict ./start.sh example/function-return.i --witness example/function-return.witness-2.2.yml --mode permissive + +# YAML (format 2.2) concurrent reachability with nondet + thread-ID tracking +check_verdict ./start.sh example/concurrent-nondet.i --witness example/concurrent-nondet.witness-2.2.yml --mode permissive diff --git a/svcomp.c b/svcomp.c index 6fcde0a3bd..034f0346d3 100644 --- a/svcomp.c +++ b/svcomp.c @@ -20,6 +20,7 @@ #include #include #include +#include #include void __VERIFIER_atomic_begin() { @@ -28,16 +29,49 @@ void __VERIFIER_atomic_begin() { void __VERIFIER_atomic_end(void) { } +atomic_int c2tt_global_counter = 0; +mtx_t c2tt_mtx; +cnd_t c2tt_cv; +once_flag c2tt_once = ONCE_FLAG_INIT; + +/* The segment counter value the witness expects once every one of its + * segments has been passed, set once (before any thread is spawned, see + * witness2ast.inject_expected_final_slot) from the witness' last computed + * slot. -1 (the default, for any program svcomp.c is linked into that + * isn't actually witness-instrumented) means "no constraint": reach_error() + * always counts. */ +static int c2tt_expected_final_slot = -1; + +void __c2tt_set_expected_final_slot(int slot) { + c2tt_expected_final_slot = slot; +} + void reach_error() { + /* A reach_error() reached while the witness' schedule hasn't been + * fully played out yet -- some other, unrelated nondeterministic + * choice got the program here -- doesn't confirm the witness, so it + * doesn't count as the violation. */ + if (c2tt_expected_final_slot >= 0 + && atomic_load(&c2tt_global_counter) != c2tt_expected_final_slot) { + return; + } printf("Reached error!\n"); fflush( stdout ); exit(74); } -atomic_int c2tt_global_counter = 0; -mtx_t c2tt_mtx; -cnd_t c2tt_cv; -once_flag c2tt_once = ONCE_FLAG_INIT; +/* Thread-local logical thread ID: 0 = main thread, k = k-th spawned thread. + * Spawned threads never set this themselves -- it is fixed before they run + * a single line of program code, by __c2tt_thread_proxy below. The main + * thread is pre-initialized to 0 by c2tt_init(), called from main() below. */ +static _Thread_local int c2tt_logical_tid = -1; + +/* Pre-initialize the main thread's logical tid. Called from main() (the + * real entry point, defined at the bottom of this file) before __c2tt_main + * -- the instrumented program's renamed main -- runs any program code. */ +static void c2tt_init(void) { + c2tt_logical_tid = 0; +} /* call_once keeps the initialization race-free: a plain initialized-flag * would itself be reported as a data race by the thread sanitizer. */ @@ -47,7 +81,72 @@ static void c2tt_initialize(void) { printf("Initialized variables\n"); } +/* Returns 1 iff the current segment counter equals `slot` and the current + * thread's logical witness ID equals `logical_tid`. Used by the runtime + * nondet/assumption/branching guards to decide whether the witness wants + * something to happen right here, right now, on this thread. */ +int __c2tt_should_use_assumed(int slot, int logical_tid) { + return atomic_load(&c2tt_global_counter) == slot + && c2tt_logical_tid == logical_tid; +} + +/* General assumption/branching guard: `matches` is the segment/thread + * check above (or 1, unconditionally, for formats with no segment counter); + * `holds` is whatever the witness claims should be true right now (an + * assumption's expression, or a branching statement's controlling + * expression compared against the witness' recorded direction). If the + * witness wanted this checked and it doesn't hold, this execution has + * diverged from the witness, so it exits cleanly instead of running on + * down a path the witness doesn't describe. */ +void __concurrentwit2test_assume(int matches, int holds) { + if (matches && !holds) { + exit(0); + } +} + +/* Blob handed from pthread_create's caller to __c2tt_thread_proxy: the + * program's real start routine and argument, plus the logical witness ID + * the new thread should run as (or -1 if this particular pthread_create + * call is not the one the witness is pinning -- e.g. a different loop + * iteration spawning with the same start routine). Heap-allocated because + * pthread_create can return, unwinding the caller's stack, before the new + * thread gets around to reading it. */ +struct __c2tt_thread_arg { + void *real_arg; + void *(*real_func)(void *); + int logical_tid; +}; + +void *__c2tt_make_thread_arg(void *(*real_func)(void *), void *real_arg, int logical_tid) { + struct __c2tt_thread_arg *targ = malloc(sizeof(struct __c2tt_thread_arg)); + targ->real_func = real_func; + targ->real_arg = real_arg; + targ->logical_tid = logical_tid; + return targ; +} + +/* Passed to pthread_create in place of the program's real start routine. + * The real routine may be shared by several pthread_create call sites (or + * the same call site looped), so the logical ID lives on this per-call + * argument blob rather than on the routine itself. */ +void *__c2tt_thread_proxy(void *raw_arg) { + struct __c2tt_thread_arg *targ = (struct __c2tt_thread_arg *)raw_arg; + void *real_arg = targ->real_arg; + void *(*real_func)(void *) = targ->real_func; + c2tt_logical_tid = targ->logical_tid; + free(targ); + printf("Thread %d starting\n", c2tt_logical_tid); + return real_func(real_arg); +} + void __concurrentwit2test_yield(int target_value, int threadid) { + /* Code shared by threads outside the witness' schedule (or a thread + * other than the one this particular schedule point targets) must run + * on without participating -- it has nothing to wait for and nothing + * to release. */ + if (c2tt_logical_tid != threadid) { + return; + } call_once(&c2tt_once, c2tt_initialize); mtx_lock(&c2tt_mtx); @@ -67,6 +166,10 @@ void __concurrentwit2test_yield(int target_value, int threadid) { } void __concurrentwit2test_release(int target_value, int threadid) { + /* Symmetric with yield: not the targeted thread, nothing to do. */ + if (c2tt_logical_tid != threadid) { + return; + } call_once(&c2tt_once, c2tt_initialize); mtx_lock(&c2tt_mtx); if (atomic_load(&c2tt_global_counter) > target_value) { @@ -105,3 +208,28 @@ unsigned __VERIFIER_nondet_unsigned(void) { return 0; } unsigned char __VERIFIER_nondet_unsigned_char(void) { return 0; } unsigned int __VERIFIER_nondet_unsigned_int(void) { return 0; } unsigned short __VERIFIER_nondet_ushort(void) { return 0; } + +/* witness2ast renames the instrumented program's main to __c2tt_main and + * normalizes its signature to (int, char **) -- adding the two parameters + * even when the program's main took none -- so this call always matches the + * definition. The match is required on WASM/WASIX (the web demo runtime), + * where a direct call whose signature differs from the callee's definition + * traps, rather than ignoring the extra arguments as a native ABI does. */ +extern int __c2tt_main(int argc, char **argv); + +/* We drive __c2tt_main from a real main here so the process can + * pthread_exit() rather than return. Returning from the original main would + * tear the process down the moment the main thread is done, even while + * spawned threads still have schedule segments -- or, for a data-race + * witness, the final racing access -- left to execute. Calling pthread_exit + * on the main thread instead keeps the process alive until every other + * thread has finished. */ +int main(int argc, char **argv) { + printf("Starting main\n"); + c2tt_init(); + printf("Calling __c2tt_main\n"); + __c2tt_main(argc, argv); + printf("Main done, calling pthread_exit\n"); + pthread_exit(NULL); + return 0; +} diff --git a/tweaks.py b/tweaks.py index c8d58a1752..d936aa0a5c 100644 --- a/tweaks.py +++ b/tweaks.py @@ -14,12 +14,12 @@ limitations under the License. """ -from pycparser import CParser -from pycparser.c_ast import FuncDef, Decl, Struct, TypeDecl +from pycparser import CParser, c_generator +from pycparser.c_ast import FuncDef, Decl, Pragma, Struct, TypeDecl def declare_schedule_functions(ast): - """Add explicit prototypes for the schedule-point functions. + """Add explicit prototypes for the schedule-point and runtime-guard functions. They are otherwise called without ever being declared in the instrumented file (their definition only exists in svcomp.c, compiled @@ -31,12 +31,88 @@ def declare_schedule_functions(ast): .parse( "void __concurrentwit2test_yield(int, int);\n" "void __concurrentwit2test_release(int, int);\n" + "int __c2tt_should_use_assumed(int, int);\n" + "void __concurrentwit2test_assume(int, int);\n" + "void *__c2tt_thread_proxy(void *);\n" + "void *__c2tt_make_thread_arg(void *(*)(void *), void *, int);\n" + "void __c2tt_set_expected_final_slot(int);\n" ) .ext ) ast.ext[0:0] = prototypes +class LineDirectiveCGenerator(c_generator.CGenerator): + """A CGenerator that emits ``#line`` directives ahead of each original + statement/declaration, so the regenerated (reformatted, instrumented) + file's line numbers as seen by the compiler -- and therefore gcc + diagnostics and UBSan/TSan runtime error locations -- match the + *original* source file instead of this generator's own pretty-printed + layout. + + Nodes pycparser parsed from the original source carry a ``.coord`` + (file, line); nodes witness2ast.py constructs and inserts (yield/ + release/assume calls, the rewritten pthread_create arguments, ...) + don't, since there's no original-source line to attribute them to -- + they're left unanchored, and whichever coord-bearing node comes next + re-anchors correctly regardless of how far the implicit line count + drifted in between. Approximate bookkeeping (e.g. opening braces + aren't tracked) can only produce a redundant-but-still-correct extra + directive, never a wrong one, since every directive that *is* emitted + always carries the node's own ground-truth coord. + """ + + def __init__(self, *args, **kwargs): + super().__init__(*args, **kwargs) + self._line_file = None + self._next_line = None + + def _line_prefix(self, coord, upcoming_text): + prefix = "" + if coord is not None and coord.line is not None and coord.file: + if coord.file != self._line_file or coord.line != self._next_line: + prefix = '#line {} "{}"\n'.format(coord.line, coord.file) + self._line_file = coord.file + self._next_line = coord.line + if self._next_line is not None: + self._next_line += upcoming_text.count("\n") + return prefix + + def _generate_stmt(self, n, add_indent=False): + text = super()._generate_stmt(n, add_indent=add_indent) + return self._line_prefix(getattr(n, "coord", None), text) + text + + def visit_FuncDef(self, n): + decl_text = self.visit(n.decl) + prefix = self._line_prefix(getattr(n, "coord", None), decl_text + "\n") + # The body Compound's opening "{" is emitted directly by + # visit_Compound, bypassing _generate_stmt -- so it's an untracked + # physical line. Forget the running belief rather than risk it + # coincidentally (and wrongly) matching the body's first statement's + # real coord, which would suppress a directive that's actually needed. + self._next_line = None + self.indent_level = 0 + body = self.visit(n.body) + if n.param_decls: + knrdecls = ";\n".join(self.visit(p) for p in n.param_decls) + return prefix + decl_text + "\n" + knrdecls + ";\n" + body + "\n" + return prefix + decl_text + "\n" + body + "\n" + + def visit_FileAST(self, n): + s = "" + for ext in n.ext: + if isinstance(ext, FuncDef): + s += self.visit(ext) + continue + text = ( + self.visit(ext) + "\n" + if isinstance(ext, Pragma) + else self.visit(ext) + ";\n" + ) + s += self._line_prefix(getattr(ext, "coord", None), text) + text + return s + + def reach_error(ast): for node in ast.ext: if isinstance(node, FuncDef) and node.decl.name == "reach_error": diff --git a/witness2ast.py b/witness2ast.py index 04cd8f559d..fa6758b5fd 100644 --- a/witness2ast.py +++ b/witness2ast.py @@ -19,14 +19,54 @@ sequence of steps; this module turns those steps into source-level instrumentation: -* steps carrying an ``assumption`` over a ``__VERIFIER_nondet_*()`` - assignment replace the nondeterministic call with the assumed constant; -* steps where the executing thread changes become *schedule points*: a +* Steps carrying an ``assumption`` over a ``__VERIFIER_nondet_*()`` + assignment or declaration initializer (``int x = __VERIFIER_nondet_*()``) + replace the nondeterministic call with a runtime guard: + ``__c2tt_should_use_assumed(slot, logical_tid) ? VALUE : __VERIFIER_nondet_*()``. + The guard checks both the global segment counter (``slot``) and the + calling thread's logical witness ID so that the assumed value is only + injected when the execution is in exactly the right scheduling epoch and + thread. + +* ``function_return`` waypoints work like assumptions but target the + ``return __VERIFIER_nondet_*()`` expression inside the indicated function. + +* Steps where the executing thread changes become *schedule points*: a ``__concurrentwit2test_yield(slot, tid)``/``__concurrentwit2test_release(slot, tid)`` pair (implemented in ``svcomp.c``) that blocks the thread until all earlier schedule points have been passed, realizing the witness' cross-thread ordering. The functions are prefixed to avoid accidentally colliding with - identifiers in the instrumented program. + identifiers in the instrumented program. Both check internally that the + *calling* thread's logical ID matches the targeted ``tid`` before doing + anything, so code shared by several threads (or by the witnessed thread + and unrelated ones) only pauses/advances the schedule on the one thread + it is meant for. + +* ``function_enter`` waypoints at ``pthread_create`` call sites rewrite the + call to go through ``__c2tt_thread_proxy`` (see ``svcomp.c``), handing it + the program's real start routine/argument plus the logical thread ID the + new thread should run as. The ID is only assigned when the *call* happens + in the right segment and on the right calling thread (a runtime check, + since the same call site -- e.g. inside a loop -- may run many times, + only one of which is the one the witness pins); other invocations pass + ``-1``, i.e. "not a thread the witness tracks". This is deliberately not + done by injecting a registration call into the start routine's body, + since that routine may be shared by multiple ``pthread_create`` call + sites with different logical IDs. + +* ``assumption`` waypoints that pin a ``__VERIFIER_nondet_*()`` assignment + to a constant value (the common case) use the runtime guard above to + substitute the value. Any other assumption (a general C expression, not + immediately following a matching nondet call) instead gets a single + ``__concurrentwit2test_assume(matches, EXPR)`` call inserted -- the + helper (see ``svcomp.c``) exits cleanly if ``matches`` (the segment/ + thread check) holds but ``EXPR`` doesn't, since that execution has + diverged from the witness rather than replaying it. + +* ``branching`` waypoints re-check the branching statement's controlling + expression against the witness' recorded direction (or, for ``switch``, + its integer constant) through the same ``__concurrentwit2test_assume`` + call. For a ``no-data-race`` witness the racing accesses (the ``target`` waypoints of the final multi-follow segment) are special: they must stay @@ -37,6 +77,7 @@ import re +from pycparser import CParser from pycparser.c_ast import ( Compound, If, @@ -45,17 +86,96 @@ For, Return, FuncCall, + FuncDef, NodeVisitor, ID, ExprList, Constant, Assignment, + Decl, + TypeDecl, + IdentifierType, + TernaryOp, + UnaryOp, + BinaryOp, ) from Exceptions import KnownErrorVerdict from witnessparser import parse_witness, FORMAT_YAML +def _nondet_call_of(node): + """Return the ``__VERIFIER_nondet_*()`` call that `node` stores into a + variable, or ``None`` if `node` is not such a store. + + Both forms count: an ``x = __VERIFIER_nondet_*()`` assignment and an + ``int x = __VERIFIER_nondet_*()`` declaration-with-initializer. The + latter is a pycparser ``Decl`` (not an ``Assignment``), which is the + common shape of a nondet read in SV-COMP tasks, so the pin logic has to + recognize it too. + """ + if isinstance(node, Assignment): + expr = node.rvalue + elif isinstance(node, Decl): + expr = node.init + else: + return None + if ( + isinstance(expr, FuncCall) + and isinstance(expr.name, ID) + and "__VERIFIER_nondet" in expr.name.name + ): + return expr + return None + + +def _assigned_varname(node): + """Name of the variable an assignment/declaration writes, or ``None``.""" + if isinstance(node, Assignment): + return getattr(node.lvalue, "name", None) + if isinstance(node, Decl): + return node.name + return None + + +def _set_assigned_expr(node, expr): + """Replace the right-hand side / initializer of an assignment or decl.""" + if isinstance(node, Assignment): + node.rvalue = expr + else: # Decl + node.init = expr + + +def _strip_enclosing_parens(expr): + """Strip whitespace and any parentheses that wrap the *whole* expression. + + Producers such as CPAchecker emit assumption constraints fully + parenthesized (``(x == 3)``); without this the ``var == const`` pin + regex would read the variable as ``(x`` and the value as ``3)`` and miss + the pin. Only fully-enclosing balanced parens are removed: ``!(x == 3)`` + and ``(x == 3) && (y == 4)`` are left untouched, so they keep falling + through to the safe full-expression guard rather than being mistaken for + a simple pin. + """ + expr = expr.strip() + while len(expr) >= 2 and expr[0] == "(" and expr[-1] == ")": + depth = 0 + closed_at = -1 + for i, ch in enumerate(expr): + if ch == "(": + depth += 1 + elif ch == ")": + depth -= 1 + if depth == 0: + closed_at = i + break + if closed_at == len(expr) - 1: + expr = expr[1:-1].strip() + else: + break + return expr + + def find_nondet_assignment_on_line(ast, target_line, target_file): class LineVisitor(NodeVisitor): def __init__(self, target_line, target_file): @@ -78,9 +198,7 @@ def visit_Compound(self, node): if ( line >= self.target_line and stmt.coord.file == self.target_file - and type(stmt) == Assignment - and type(stmt.rvalue) == FuncCall - and "__VERIFIER_nondet" in stmt.rvalue.name.name + and _nondet_call_of(stmt) is not None ): self.statement = stmt self.parent = node @@ -98,26 +216,32 @@ def visit_Compound(self, node): def find_last_nondet_assignment_before_line(ast, target_line, varnames, target_file): - """Find the last `var = __VERIFIER_nondet_*()` with var in `varnames` - at or before `target_line`.""" + """Find the last ``var = __VERIFIER_nondet_*()`` -- assignment or + declaration-with-initializer -- with var in `varnames` at or before + `target_line`.""" class LineVisitor(NodeVisitor): def __init__(self): self.statement = None self.line = -1 - def visit_Assignment(self, node): + def _consider(self, node): if ( node.coord and node.coord.file == target_file and self.line < node.coord.line <= target_line - and type(node.rvalue) == FuncCall - and type(node.rvalue.name) == ID - and "__VERIFIER_nondet" in node.rvalue.name.name - and getattr(node.lvalue, "name", None) in varnames + and _nondet_call_of(node) is not None + and _assigned_varname(node) in varnames ): self.statement = node self.line = node.coord.line + + def visit_Assignment(self, node): + self._consider(node) + self.generic_visit(node) + + def visit_Decl(self, node): + self._consider(node) self.generic_visit(node) line_visitor = LineVisitor() @@ -125,39 +249,251 @@ def visit_Assignment(self, node): return line_visitor.statement +def find_return_nondet_on_line(ast, target_line, target_file): + """Find a ``return __VERIFIER_nondet_*()`` statement at or after target_line.""" + + class ReturnVisitor(NodeVisitor): + def __init__(self): + self.statement = None + + def visit_Return(self, node): + if ( + node.coord + and node.coord.file == target_file + and node.coord.line >= target_line + and node.expr is not None + and isinstance(node.expr, FuncCall) + and isinstance(node.expr.name, ID) + and "__VERIFIER_nondet" in node.expr.name.name + and self.statement is None + ): + self.statement = node + self.generic_visit(node) + + v = ReturnVisitor() + v.visit(ast) + return v.statement + + +def _is_nondet_call(node): + return ( + isinstance(node, FuncCall) + and isinstance(node.name, ID) + and "__VERIFIER_nondet" in node.name.name + ) + + +def replace_bare_nondet_on_line(ast, target_line, target_file, make_replacement): + """Replace the first ``__VERIFIER_nondet_*()`` call used as a bare + sub-expression (e.g. ``if (__VERIFIER_nondet_int())``) at or after + ``target_line``, where it is neither returned nor stored into a variable. + + ``make_replacement(call)`` produces the node to splice in. Returns the + original call on success, else ``None``. + """ + found = {"call": None} + + def walk(node): + if found["call"] is not None or node is None: + return + for attr in getattr(node, "__slots__", ()): + if attr in ("coord", "__weakref__"): + continue + child = getattr(node, attr, None) + if isinstance(child, list): + for i, item in enumerate(child): + if _matches(item): + child[i] = make_replacement(item) + found["call"] = item + return + walk(item) + if found["call"] is not None: + return + else: + if _matches(child): + setattr(node, attr, make_replacement(child)) + found["call"] = child + return + walk(child) + if found["call"] is not None: + return + + def _matches(item): + return ( + _is_nondet_call(item) + and item.coord + and item.coord.file == target_file + and item.coord.line >= target_line + ) + + walk(ast) + return found["call"] + + def find_first_statement_on_line(ast, target_line, target_file): class LineVisitor(NodeVisitor): def __init__(self, target_line, target_file): self.target_line = target_line self.target_file = target_file - self.found = False self.statement = None self.parent = None + self.found = False def visit(self, node): if not self.found: super().visit(node) + def _matches(self, stmt): + return ( + hasattr(stmt, "coord") + and stmt.coord + and stmt.coord.file == self.target_file + and stmt.coord.line >= self.target_line + ) + + def _wrap_and_return(self, stmt_ref_owner, field_name, stmt): + compound = Compound(block_items=[stmt]) + setattr(stmt_ref_owner, field_name, compound) + + self.statement = stmt + self.parent = compound + self.found = True + def visit_Compound(self, node): if self.found: return - for stmt in node.block_items if node.block_items else [node]: - if hasattr(stmt, "coord") and stmt.coord: - line = stmt.coord.line - if line >= self.target_line and stmt.coord.file == self.target_file: - self.statement = stmt - self.parent = node - self.found = True + + for stmt in node.block_items or []: + if self.found: + return + + if self._matches(stmt): + self.statement = stmt + self.parent = node + self.found = True + return + + # Check unbraced loop bodies + if isinstance(stmt, (While, DoWhile, For)): + body = stmt.stmt + + if ( + body is not None + and not isinstance(body, Compound) + and self._matches(body) + ): + self._wrap_and_return(stmt, "stmt", body) return - self.generic_visit(stmt) - line_visitor = LineVisitor(target_line, target_file) - line_visitor.visit(ast) + # Check unbraced if branches + elif isinstance(stmt, If): + if ( + stmt.iftrue is not None + and not isinstance(stmt.iftrue, Compound) + and self._matches(stmt.iftrue) + ): + self._wrap_and_return(stmt, "iftrue", stmt.iftrue) + return - if line_visitor.statement: - return line_visitor.statement, line_visitor.parent + if ( + stmt.iffalse is not None + and not isinstance(stmt.iffalse, Compound) + and self._matches(stmt.iffalse) + ): + self._wrap_and_return(stmt, "iffalse", stmt.iffalse) + return + + self.visit(stmt) + + visitor = LineVisitor(target_line, target_file) + visitor.visit(ast) + + return visitor.statement, visitor.parent + + +def find_pthread_create_call(ast, target_line, target_file): + """Return the ``pthread_create(...)`` FuncCall node at target_line, or None.""" + + class Visitor(NodeVisitor): + def __init__(self): + self.call = None + + def visit_FuncCall(self, node): + if ( + self.call is None + and node.coord + and node.coord.file == target_file + and node.coord.line == target_line + and isinstance(node.name, ID) + and node.name.name == "pthread_create" + and node.args is not None + and len(node.args.exprs) >= 4 + ): + self.call = node + self.generic_visit(node) + + v = Visitor() + v.visit(ast) + return v.call + + +def make_segment_match_call(slot, logical_tid): + return FuncCall( + ID("__c2tt_should_use_assumed"), + ExprList( + [ + Constant(type="int", value=str(slot)), + Constant(type="int", value=str(logical_tid)), + ] + ), + ) + + +def instrument_pthread_create( + ast, line, target_file, slot, calling_threadid, logical_tid +): + """Rewrite the ``pthread_create`` call at `line` to spawn through + ``__c2tt_thread_proxy``, so the new thread's logical witness ID is fixed + (to `logical_tid`, or -1 if this particular call turns out, at runtime, + not to be the one the witness pins) before it runs any program code. + + If the call site was already rewritten -- the same source line can + spawn many real threads, e.g. inside a loop, with only one of them + being the one a given function_enter waypoint refers to -- the new + segment/thread check is chained onto the existing logical-tid ternary + instead of overwriting it. + """ + call = find_pthread_create_call(ast, line, target_file) + if call is None: + return + + match_call = make_segment_match_call(slot, calling_threadid) + already_instrumented = ( + isinstance(call.args.exprs[2], ID) + and call.args.exprs[2].name == "__c2tt_thread_proxy" + ) + + if not already_instrumented: + real_func = call.args.exprs[2] + real_arg = call.args.exprs[3] + tid_expr = TernaryOp( + cond=match_call, + iftrue=Constant(type="int", value=str(logical_tid)), + iffalse=Constant(type="int", value="-1"), + ) + call.args.exprs[2] = ID("__c2tt_thread_proxy") + call.args.exprs[3] = FuncCall( + ID("__c2tt_make_thread_arg"), + ExprList([real_func, real_arg, tid_expr]), + ) else: - return None, None + make_thread_arg_call = call.args.exprs[3] + previous_tid_expr = make_thread_arg_call.args.exprs[2] + make_thread_arg_call.args.exprs[2] = TernaryOp( + cond=match_call, + iftrue=Constant(type="int", value=str(logical_tid)), + iffalse=previous_tid_expr, + ) nondet_return_types = { @@ -191,12 +527,97 @@ def visit_Compound(self, node): assumption_pattern = r"([^\s]*)\s*==\s*([^\s]*)" -def apply_assumption(ast, line, assumption, target_file, anchored_after=False): - """Fix the value of a __VERIFIER_nondet_*() assignment near `line`. +def _make_guarded_nondet(nondet_call, ret_type, value, slot, logical_tid): + """Wrap a nondet call in a runtime guard: + ``__c2tt_should_use_assumed(slot, tid) ? VALUE : __VERIFIER_nondet_*()``. + + When slot or logical_tid is None the guard is skipped and the constant + is substituted directly (GraphML path with no slot information, or any + context where the slot is unknown). + """ + if slot is None or logical_tid is None: + return Constant(type=ret_type, value=value) + return TernaryOp( + cond=make_segment_match_call(slot, logical_tid), + iftrue=Constant(type=ret_type, value=value), + iffalse=nondet_call, + ) + + +def make_match_expr(slot, logical_tid): + """An expression that's true exactly when the witness wants something + checked right now: unconditionally true (1) if slot/logical_tid are + unknown (GraphML has no segment counter), else the segment/thread + match check. + """ + if slot is None or logical_tid is None: + return Constant(type="int", value="1") + return make_segment_match_call(slot, logical_tid) + + +def make_assume_call(slot, logical_tid, holds_expr): + """``__concurrentwit2test_assume(matches, holds)`` (see svcomp.c): a + single call standing in for ``if (matches && !holds) exit(0);``, so + general assumption/branching guards are one statement in the AST + instead of a constructed If/Compound/exit tree. + """ + return FuncCall( + ID("__concurrentwit2test_assume"), + ExprList([make_match_expr(slot, logical_tid), holds_expr]), + ) + + +def parse_c_expression(expr_str, target_file): + """Parse a standalone C expression string into a pycparser expression node.""" + wrapper_ast = CParser().parse( + f"void __c2tt_expr_wrapper(void) {{ ({expr_str}); }}", target_file + ) + return wrapper_ast.ext[-1].body.block_items[0] + + +def insert_assumption_guard(ast, line, assumption, target_file, slot, logical_tid): + """General fallback for assumption waypoints that don't pin a nondet + call: insert a ``__concurrentwit2test_assume(matches, EXPR)`` call right + before the located statement. An execution that disagrees with the + witness' assumption is not a replay of it, so it exits cleanly instead + of running on down an unwitnessed path. + """ + statement, parent = find_first_statement_on_line(ast, line, target_file) + if statement is None: + return + try: + expr = parse_c_expression(assumption, target_file) + except Exception: + return + + call = make_assume_call(slot, logical_tid, expr) + idx = parent.block_items.index(statement) + parent.block_items.insert(idx, call) + + +def apply_assumption( + ast, + line, + assumption, + target_file, + anchored_after=False, + slot=None, + logical_tid=None, +): + """Fix the value of a __VERIFIER_nondet_*() assignment near `line`, or + fall back to a general runtime-checked assumption. If the assumption constrains the assigned variable to a constant - (`var == value`), the nondeterministic call is replaced by that - constant. Assumptions of any other shape are ignored. + (`var == value`) immediately after a matching nondet call, the + nondeterministic call is replaced by a runtime guard that returns the + assumed constant only when the global segment counter equals `slot` + and the calling thread's logical ID equals `logical_tid`. When + slot/logical_tid are None (GraphML witnesses) the constant is + substituted unconditionally as before. + + Otherwise (a general assumption, not the "easy" nondet-substitution + case) a guarded ``if (!(EXPR)) exit(0);`` is inserted instead -- see + ``insert_assumption_guard``. The two witness formats anchor assumptions differently: a GraphML edge carries the assumption on the assigning statement itself, while a YAML @@ -204,24 +625,94 @@ def apply_assumption(ast, line, assumption, target_file, anchored_after=False): i.e., it follows the assignment (anchored_after=True). """ # TODO current implementation is limited: will not work if single assignment executes 1+ time (e.g., in a loop) - assumptions = dict(re.findall(assumption_pattern, assumption)) + assumptions = dict( + re.findall(assumption_pattern, _strip_enclosing_parens(assumption)) + ) if anchored_after: nondet_assign_node = find_last_nondet_assignment_before_line( ast, line, set(assumptions), target_file ) else: nondet_assign_node, _ = find_nondet_assignment_on_line(ast, line, target_file) - if nondet_assign_node is None: - return - varname = nondet_assign_node.lvalue.name - if varname in assumptions: - if nondet_assign_node.rvalue.name.name in nondet_return_types: - ret_type = nondet_return_types[nondet_assign_node.rvalue.name.name] - nondet_assign_node.rvalue = Constant( - type=ret_type, value=assumptions[varname] + if nondet_assign_node is not None: + varname = _assigned_varname(nondet_assign_node) + if varname in assumptions: + original_call = _nondet_call_of(nondet_assign_node) + nondet_name = getattr(original_call.name, "name", None) + if nondet_name in nondet_return_types: + ret_type = nondet_return_types[nondet_name] + _set_assigned_expr( + nondet_assign_node, + _make_guarded_nondet( + original_call, + ret_type, + assumptions[varname], + slot, + logical_tid, + ), + ) + return + + insert_assumption_guard(ast, line, assumption, target_file, slot, logical_tid) + + +def apply_function_return( + ast, line, assumption, target_file, slot=None, logical_tid=None +): + """Fix the result of a __VERIFIER_nondet_*() call near `line`. + + The constraint value is parsed with the same ``var == value`` pattern + as assumptions (``var`` is ignored -- only the value matters). The + nondeterministic call is replaced by a runtime guard whether its result + is returned (``return __VERIFIER_nondet_*()``) or stored by an assignment + or declaration initializer (``int x = __VERIFIER_nondet_*()``), the latter + being what producers emit for a plain nondet read. + """ + stripped = _strip_enclosing_parens(assumption) + values = re.findall(assumption_pattern, stripped) + if values: + value = values[0][1] + else: + # Allow bare literal: "5" or "-1" etc. + value = stripped + + ret_node = find_return_nondet_on_line(ast, line, target_file) + nondet_assign_node = None + if ret_node is not None: + original_call = ret_node.expr + else: + nondet_assign_node, _ = find_nondet_assignment_on_line(ast, line, target_file) + original_call = ( + _nondet_call_of(nondet_assign_node) if nondet_assign_node else None + ) + + if original_call is None: + # nondet used as a bare sub-expression, e.g. ``if (__VERIFIER_nondet_int())``: + # splice the guard in place wherever the call sits. + def _replace(call): + name = getattr(call.name, "name", None) + if name not in nondet_return_types: + return call + return _make_guarded_nondet( + call, nondet_return_types[name], value, slot, logical_tid ) + replace_bare_nondet_on_line(ast, line, target_file, _replace) + return + + nondet_name = getattr(original_call.name, "name", None) + if nondet_name not in nondet_return_types: + return + + guarded = _make_guarded_nondet( + original_call, nondet_return_types[nondet_name], value, slot, logical_tid + ) + if ret_node is not None: + ret_node.expr = guarded + else: + _set_assigned_expr(nondet_assign_node, guarded) + def make_schedule_call(name, slot, threadid): return FuncCall( @@ -235,35 +726,73 @@ def make_schedule_call(name, slot, threadid): ) -def insert_schedule_point(ast, line, slot, threadid, target_file, release=True): +def _contains_func_call(node): + """True if `node`'s subtree contains a function call anywhere. + + Used to decide where a schedule point's release goes: a statement that + (however deeply) calls a function may never return, or the next witness + segment may lie *inside* the call (e.g. ``__VERIFIER_assert(...)`` whose + failure path is the violation), so the release has to precede it. + """ + + class _Finder(NodeVisitor): + def __init__(self): + self.found = False + + def visit_FuncCall(self, node): + self.found = True + + finder = _Finder() + finder.visit(node) + return finder.found + + +def insert_schedule_point( + ast, line, slot, threadid, target_file, release=True, input_only=False +): """Instrument the statement at (or first after) `line` as a schedule point. A __concurrentwit2test_yield(slot, threadid) call before the statement blocks the thread until all earlier schedule points have released their slot; a __concurrentwit2test_release(slot, threadid) call afterwards lets - the next schedule point proceed. For control statements the release goes - to the start of the body/branches (so it happens only once the statement - is really being executed), and for a return statement it goes before the - statement (code after a return would never run). + the next schedule point proceed by advancing the segment counter. For + control statements the release goes to the start of the body/branches (so + it happens only once the statement is really being executed), and for a + return statement it goes before the statement (code after a return would + never run). + + When the statement (however deeply) contains a function call the release + is likewise inserted *before* it: the call may not return, or the next + witness segment may occur inside it (e.g. the violation is the + ``reach_error()`` reached within ``__VERIFIER_assert(...)``), so releasing + afterwards would advance the segment counter too late for that segment to + ever be recognized. With release=False only the yield is inserted and the slot is not consumed; this keeps racing accesses of a data-race witness free of synchronization between one another. + With input_only=True the blocking yield is omitted, so the thread + schedule is left free, but the release is still inserted and the slot is + still advanced: the segment counter keeps tracking every passed segment + (so the per-segment input/assumption guards stay meaningful) without the + schedule being steered. + Returns the slot the next schedule point should use. """ statement, parent = find_first_statement_on_line(ast, line, target_file) - yield_func = make_schedule_call("__concurrentwit2test_yield", slot, threadid) - first_index = parent.block_items.index(statement) - parent.block_items.insert(first_index, yield_func) + if not input_only: + yield_func = make_schedule_call("__concurrentwit2test_yield", slot, threadid) + parent.block_items.insert(parent.block_items.index(statement), yield_func) if not release: return slot release_func = make_schedule_call("__concurrentwit2test_release", slot, threadid) + stmt_index = parent.block_items.index(statement) if isinstance(statement, Return): - parent.block_items.insert(first_index + 1, release_func) + parent.block_items.insert(stmt_index, release_func) elif isinstance(statement, Compound): statement.block_items = [release_func] + (statement.block_items or []) elif isinstance(statement, (While, DoWhile, For)): @@ -273,13 +802,152 @@ def insert_schedule_point(ast, line, slot, threadid, target_file, release=True): statement.iftrue = Compound(block_items=[release_func, statement.iftrue]) if statement.iffalse: statement.iffalse = Compound(block_items=[release_func, statement.iffalse]) + elif _contains_func_call(statement): + parent.block_items.insert(stmt_index, release_func) else: - parent.block_items.insert(first_index + 2, release_func) + parent.block_items.insert(stmt_index + 1, release_func) return slot + 1 -def apply_witness(ast, c_file, witnessfile): - """Instrument `ast` according to the witness; returns the ParsedWitness.""" +def apply_branching( + ast, line, constraint_value, target_file, slot=None, logical_tid=None +): + """Branching waypoint: re-check the branching statement's (``if``, + ``while``, ``do``, ``for``, or ``switch``) controlling expression + against the witness' recorded direction, via the same + ``__concurrentwit2test_assume`` helper as general assumptions. + + The controlling expression is duplicated rather than lifted into a + temporary, so this -- like ``apply_assumption`` -- is unsound if it has + side effects; the same known limitation applies here. + """ + statement, parent = find_first_statement_on_line(ast, line, target_file) + if statement is None or getattr(statement, "cond", None) is None: + return + + cond = statement.cond + if constraint_value in ("true", "false"): + wanted_true = constraint_value == "true" + holds = cond if wanted_true else UnaryOp("!", cond) + else: + try: + int(constraint_value) + except (TypeError, ValueError): + # 'default' switch label or other unsupported constraint forms. + return + holds = BinaryOp("==", cond, Constant(type="int", value=str(constraint_value))) + + call = make_assume_call(slot, logical_tid, holds) + idx = parent.block_items.index(statement) + parent.block_items.insert(idx, call) + + +def _argc_argv_param_list(): + """A fresh ``(int __c2tt_argc, char **__c2tt_argv)`` ParamList. + + Built by parsing a throwaway declaration so the nodes match the installed + pycparser's exact shape; freshly parsed each call, so there is no aliasing + between successive uses. + """ + template = CParser().parse( + "int __c2tt_argv_tmpl(int __c2tt_argc, char **__c2tt_argv);" + ) + return template.ext[0].type.args + + +def _real_params(func_decl): + """The function's real parameters, dropping a lone ``(void)`` marker.""" + if func_decl.args is None or not func_decl.args.params: + return [] + real = [] + for p in func_decl.args.params: + t = getattr(p, "type", None) + if ( + isinstance(t, TypeDecl) + and isinstance(t.type, IdentifierType) + and t.type.names == ["void"] + ): + continue + real.append(p) + return real + + +def _ensure_argc_argv(func_decl): + """Give ``__c2tt_main`` an ``(int, char **)`` signature if it lacks one. + + svcomp.c's real ``main`` always calls ``__c2tt_main(argc, argv)``. On + WASM/WASIX (the web demo runtime) a direct call whose argument signature + does not match the callee's *definition* traps -- wasm function types are + part of the type system, unlike a native ABI where extra register + arguments are simply ignored. A program whose ``main`` was ``int + main(void)`` therefore needs the two parameters added (its body never + references them, so synthetic names are safe); a ``main`` that already + takes ``argc``/``argv`` is left untouched so its body keeps resolving. + """ + real = _real_params(func_decl) + if len(real) >= 2: + return + params = _argc_argv_param_list() + if len(real) == 1: + # Keep the program's own first parameter (its body refers to it by + # name); only append the missing second one. + params.params[0] = real[0] + func_decl.args = params + + +def inject_expected_final_slot(ast, final_slot): + """Rename the program's ``main`` to ``__c2tt_main`` and prepend + ``__c2tt_set_expected_final_slot(final_slot)`` to its body. + + The rename lets svcomp.c provide the real ``main``, which runs + ``__c2tt_main`` and then ``pthread_exit()``s instead of returning -- so + the process stays alive for spawned threads that still have schedule + segments (or, for a data-race witness, a final racing access) left to + run, rather than being torn down the moment the main thread is done. + + The injected call makes reach_error() (see svcomp.c) only count as + confirming the witness once every one of its segments has actually been + passed -- not merely whenever the program happens to reach it via some + other, unrelated nondeterministic choice. It must run before any thread + is spawned, hence prepended to ``__c2tt_main`` itself rather than set + some other way. + """ + for node in ast.ext: + if isinstance(node, FuncDef) and node.decl.name == "main": + # The generated function name comes from the innermost + # TypeDecl's declname, not Decl.name, so rename both. + node.decl.name = "__c2tt_main" + type_decl = node.decl.type + while not isinstance(type_decl, TypeDecl): + type_decl = type_decl.type + type_decl.declname = "__c2tt_main" + # svcomp.c always calls __c2tt_main(argc, argv); make sure it + # actually takes them so the signatures match (see _ensure_argc_argv). + _ensure_argc_argv(node.decl.type) + call = FuncCall( + ID("__c2tt_set_expected_final_slot"), + ExprList([Constant(type="int", value=str(final_slot))]), + ) + body = node.body + if body.block_items is None: + body.block_items = [call] + else: + body.block_items.insert(0, call) + return + + +def apply_witness(ast, c_file, witnessfile, input_only=False): + """Instrument `ast` according to the witness; returns the ParsedWitness. + + With ``input_only`` set the blocking schedule yields + (``__concurrentwit2test_yield``) are not inserted, so the thread schedule + is left free; the rest of the instrumentation -- pinned nondet inputs, + assumption/branching guards, the pthread_create thread-ID proxy, and the + ``__concurrentwit2test_release`` calls that advance the segment counter -- + still goes through. The segment counter therefore keeps advancing with + every passed segment in every mode, so the per-segment input/assumption + guards stay meaningful; only the schedule steering is dropped. + """ witness = parse_witness(witnessfile, c_file) if not witness.steps: raise KnownErrorVerdict("Empty witness") @@ -289,19 +957,66 @@ def apply_witness(ast, c_file, witnessfile): slot = 0 anchored_after = witness.format == FORMAT_YAML + + # The k-th function_enter at a pthread_create call gets logical thread k. + next_created_thread = 1 + for coords, data in witness.steps: usable_coords = coords and "startline" in coords - if "assumption" in data and usable_coords: - apply_assumption( - ast, coords["startline"], data["assumption"], c_file, anchored_after - ) + waypoint_type = data.get("type") step_threadid = data["threadId"] if "threadId" in data else threadid + + # function_enter at a pthread_create: route the call through + # __c2tt_thread_proxy so the new thread's logical ID is fixed + # before it runs any program code (see instrument_pthread_create). + if waypoint_type == "function_enter" and usable_coords: + instrument_pthread_create( + ast, + coords["startline"], + c_file, + slot, + step_threadid, + next_created_thread, + ) + next_created_thread += 1 + + if "assumption" in data and usable_coords: + if waypoint_type == "function_return": + apply_function_return( + ast, + coords["startline"], + data["assumption"], + c_file, + slot=slot, + logical_tid=step_threadid, + ) + elif waypoint_type == "branching": + apply_branching( + ast, + coords["startline"], + data["assumption"], + c_file, + slot=slot, + logical_tid=step_threadid, + ) + else: + apply_assumption( + ast, + coords["startline"], + data["assumption"], + c_file, + anchored_after, + slot=slot, + logical_tid=step_threadid, + ) + if step_threadid != threadid and usable_coords: threadid = step_threadid release = not (witness.data_race and data.get("type") == "target") slot = insert_schedule_point( - ast, coords["startline"], slot, threadid, c_file, release + ast, coords["startline"], slot, threadid, c_file, release, input_only ) + inject_expected_final_slot(ast, slot) return witness diff --git a/witnessparser.py b/witnessparser.py index 7d31b0ec75..82cef1e482 100644 --- a/witnessparser.py +++ b/witnessparser.py @@ -34,7 +34,10 @@ ``endline``, ``column``, ``length``, ``content``) or is ``None`` when the witness gives no usable location. ``metadata`` may contain: -* ``assumption``: a C expression that holds at this step, +* ``assumption``: a C expression that holds at this step (for assumption + and function_return waypoints), or the recorded branch direction/case + (for branching waypoints: ``"true"``/``"false"``, or an integer/``"default"`` + for switch), * ``threadId``: the thread executing this step (``0`` = main thread), * ``type``: the waypoint type (YAML witnesses only, e.g. ``target``). """ @@ -61,6 +64,20 @@ def data_race(self): """Whether the witness claims a data race (no-data-race property).""" return "data-race" in self.specification + @property + def no_overflow(self): + """Whether the witness claims an integer overflow (no-overflow property).""" + return "overflow" in self.specification + + @property + def memory_safety(self): + """Whether the witness claims a memory-safety violation. + + Covers the SV-COMP valid-free, valid-deref, and valid-memtrack + properties, whose specifications read ``G valid-free`` etc. + """ + return "valid-" in self.specification + def get_offset_of_line(c_file, line): with open(c_file, "r") as f: @@ -183,6 +200,31 @@ def parse_graphml_witness(witnessfile, c_file): return ParsedWitness(steps, specification, FORMAT_GRAPHML) +def _extract_constraint(waypoint): + """Extract the assumption/constraint value from a YAML waypoint, or None. + + ``assumption`` constraints use ``c_expression``; ``function_return`` + constraints use ``ext_c_expression`` (the function-context grammar that + ``\\result`` belongs to); ``branching`` waypoints omit ``format`` + entirely and carry a YAML bool (or, for ``switch``, an integer/ + ``default``) rather than a C expression string. Normalize all of these + to plain strings so callers don't need to care which waypoint type they + came from. + """ + constraint = waypoint.get("constraint", {}) + if constraint.get("format", "c_expression") not in ( + "c_expression", + "ext_c_expression", + ): + return None + value = constraint.get("value") + if value is None: + return None + if isinstance(value, bool): + return "true" if value else "false" + return str(value) + + def parse_yaml_witness(witnessfile, c_file): with open(witnessfile, "r") as f: entries = yaml.safe_load(f) @@ -215,24 +257,26 @@ def parse_yaml_witness(witnessfile, c_file): # them, so they are skipped. continue + waypoint_type = waypoint.get("type") location = waypoint.get("location", {}) line = location.get("line") coords = get_coords(c_file, startline=line) if line else None metadata = { - "type": waypoint.get("type"), + "type": waypoint_type, # thread_id is the format-2.2 concurrency extension; its # absence means the main thread (thread 0). "threadId": int(waypoint.get("thread_id", 0)), } - constraint = waypoint.get("constraint", {}) - if ( - waypoint.get("type") == "assumption" - and constraint.get("format", "c_expression") == "c_expression" - and constraint.get("value") is not None - ): - metadata["assumption"] = constraint["value"] + # assumption/function_return constraints can pin a nondet call + # to a specific value; branching constraints record which way + # a branch was taken. All three are stored under the same + # "assumption" key since witness2ast dispatches on "type". + if waypoint_type in ("assumption", "function_return", "branching"): + value = _extract_constraint(waypoint) + if value is not None: + metadata["assumption"] = value steps.append((coords, metadata)) diff --git a/www-demo/Dockerfile b/www-demo/Dockerfile index 10695aa775..6bc30906f0 100644 --- a/www-demo/Dockerfile +++ b/www-demo/Dockerfile @@ -56,6 +56,9 @@ FROM nginx:alpine COPY www-demo/nginx.conf /etc/nginx/conf.d/default.conf COPY www-demo/index.html www-demo/style.css www-demo/app.js www-demo/pyodide-worker.js www-demo/wasmer-run.js www-demo/coi-serviceworker.js /usr/share/nginx/html/ COPY svcomp.c /usr/share/nginx/html/svcomp.c +# Bundled examples, fetched by app.js's local-examples sidebar -- not +# duplicated into app.js itself, so they can't drift from the real files. +COPY example/ /usr/share/nginx/html/example/ COPY --from=pytree /py.zip /usr/share/nginx/html/py.zip COPY --from=monaco /build/node_modules/monaco-editor/min/vs /usr/share/nginx/html/vendor/monaco/vs COPY --from=wasmersdk /build/node_modules/@wasmer/sdk/dist /usr/share/nginx/html/vendor/wasmer diff --git a/www-demo/README.md b/www-demo/README.md index 1a87d26056..e5b7ef7d32 100644 --- a/www-demo/README.md +++ b/www-demo/README.md @@ -103,15 +103,16 @@ directory (user-editable via the "Branch/tag" field). approach itself — Wasmer's threading model targets the browser (Web Workers + `SharedArrayBuffer`), which is also this feature's actual runtime, not Node. This needs real-browser testing to confirm. -- On the GitHub Pages deployment (`.github/workflows/gh-pages.yml`), - "Compile & Run" loses real multithreading: `SharedArrayBuffer` needs the - page to be cross-origin isolated, which needs the - `Cross-Origin-Opener-Policy`/`Cross-Origin-Embedder-Policy` response - headers `nginx.conf` sets for the Docker deployment -- and GitHub Pages - has no mechanism to set custom response headers at all (no `_headers` - file support like Netlify/Cloudflare Pages). Everything else (linting, - instrumentation) is unaffected, since it doesn't depend on - cross-origin isolation. Self-host via Docker for full Compile & Run. +- "Compile & Run"'s cross-origin isolation requirement (COOP + COEP headers + for `SharedArrayBuffer`) is handled differently per deployment: `nginx.conf` + sets the headers directly for Docker; on GitHub Pages (which has no mechanism + to set custom response headers), `coi-serviceworker.js` (checked in at + `www-demo/coi-serviceworker.js`, v0.1.7 by Guido Zuidhof) installs a + Service Worker that injects those headers via the fetch event. On first visit + to the GH Pages deployment the Service Worker triggers a one-time reload + before activating; subsequent visits are seamless. The script auto-detects + when `crossOriginIsolated` is already `true` and is a no-op in that case + (Docker deployment). ## Deploying diff --git a/www-demo/app.js b/www-demo/app.js index 79793aa745..363f300ae7 100644 --- a/www-demo/app.js +++ b/www-demo/app.js @@ -46,6 +46,87 @@ async function getSpecificationText(property) { } } +// --------------------------------------------------------------------------- +// Local examples: bundled with ConcurrentWitness2Test (the example/ +// directory, copied verbatim into the image by the Dockerfile), fetched +// from the same origin -- no network round-trip to GitLab, and no +// duplication of the actual files into this script. Each manifest entry +// just names which example/ files to fetch and which spec property to +// preselect. +// --------------------------------------------------------------------------- + +const LOCAL_EXAMPLES = [ + { + label: "concurrent-unreach (unreach-call, thread ordering)", + property: "unreach-call", + base: "concurrent-unreach", + }, + { + label: "concurrent-data-race (no-data-race, racing writes)", + property: "no-data-race", + base: "concurrent-data-race", + }, + { + label: "concurrent-nondet (unreach-call, nondet + thread-ID guard)", + property: "unreach-call", + base: "concurrent-nondet", + }, + { + label: "function-return (unreach-call, function_return waypoint)", + property: "unreach-call", + base: "function-return", + }, + { + label: "no-overflow (no-overflow, UBSan integer overflow)", + property: "no-overflow", + base: "no-overflow", + }, +]; + +async function fetchExampleFile(name) { + const resp = await fetch(`example/${name}`); + if (!resp.ok) throw new Error(`HTTP ${resp.status} fetching example/${name}`); + return await resp.text(); +} + +function renderLocalExamples() { + const list = document.getElementById("local-examples"); + list.innerHTML = ""; + for (const ex of LOCAL_EXAMPLES) { + const li = document.createElement("li"); + li.className = "file"; + li.textContent = ex.label; + li.addEventListener("click", async () => { + if (!cEditor || !yamlEditor) return; + const filename = `${ex.base}.i`; + let c, witness; + try { + [c, witness] = await Promise.all([ + fetchExampleFile(filename), + fetchExampleFile(`${ex.base}.witness-2.2.yml`), + ]); + } catch (err) { + logOutput("instrument", `Failed to load example "${ex.label}":\n${err}`); + return; + } + cEditor.setValue(c); + cFilename.textContent = filename; + // Set the spec selector to match the example's property + if (specSelect && ex.property) { + const option = Array.from(specSelect.options).find( + (o) => o.value === ex.property + ); + if (option) { + specSelect.value = ex.property; + specSelect.dispatchEvent(new Event("change")); + } + } + yamlEditor.setValue(witness); + }); + list.appendChild(li); + } +} + const outputPanels = { linter: document.getElementById("output-linter"), instrument: document.getElementById("output-instrument"), @@ -275,6 +356,7 @@ async function initEditors() { }); yamlEditor.onDidChangeModelContent(debounce(runLint, 400)); + yamlEditor.onDidChangeCursorPosition(() => highlightCLocationForYamlCursor()); addWaypointBtn.addEventListener("click", () => addWaypointAtCursor()); yamlEditor.setValue( @@ -321,6 +403,121 @@ function updateScheduleDecorations() { scheduleDecorations = model.deltaDecorations(scheduleDecorations, decorations); } +// --------------------------------------------------------------------------- +// YAML cursor -> C location highlight: clicking (or moving the cursor) into +// a waypoint's body in the YAML editor highlights the C source location its +// `location:` block points at. +// --------------------------------------------------------------------------- + +// A line-based scan, not a real YAML parse (no YAML library is vendored, +// and the witness schema's shape is fixed enough that this is reliable): +// each `- waypoint:` line starts a new waypoint, owning every line up to +// (not including) the next one, anywhere in the document. +function parseWaypointLocations(yamlText) { + const lines = yamlText.split("\n"); + const starts = []; + for (let i = 0; i < lines.length; i++) { + if (/^\s*-\s*waypoint:\s*$/.test(lines[i])) starts.push(i + 1); // 1-indexed + } + return starts.map((startLine, idx) => { + const endLine = idx + 1 < starts.length ? starts[idx + 1] - 1 : lines.length; + const block = lines.slice(startLine - 1, endLine).join("\n"); + const lineMatch = block.match(/\bline:\s*(\d+)/); + const colMatch = block.match(/\bcolumn:\s*(\d+)/); + return { + startLine, + endLine, + cLine: lineMatch ? parseInt(lineMatch[1], 10) : null, + cColumn: colMatch ? parseInt(colMatch[1], 10) : 1, + }; + }); +} + +// After "Instrument" the C editor shows LineDirectiveCGenerator's output +// (see tweaks.py): the original source reformatted, with instrumentation +// inserted, and `#line N "file"` comments ahead of each original-source +// chunk so the *line numbers* survive the reformatting. A waypoint's +// `location.line` is always in original-source terms, so it has to be +// resolved through those directives to find the right physical Monaco +// line -- forward-simulating the same line count gcc/UBSan/TSan would. +// +// The directives say nothing about *columns*: CGenerator's own +// indentation/formatting means an original column number is meaningless +// on the regenerated physical line, so column-precision highlighting is +// only valid when there are no directives at all (untouched source, where +// physical and original line numbers already coincide). +function resolvePhysicalLine(model, originalLine) { + let curLine = null; + let sawDirective = false; + // A line reached by counting forward from the last directive (no fresh + // directive of its own) is only a best-effort guess -- synthetic + // instrumentation lines with no original-source line of their own can + // coincidentally drift onto the same number. A directive that names + // `originalLine` explicitly is always ground truth and wins outright; + // the counted-forward guess is kept only as a fallback for when no + // directive ever claims that line (e.g. a line whose statement never + // needed its own re-anchoring). + let fallback = null; + const lineCount = model.getLineCount(); + for (let physicalLine = 1; physicalLine <= lineCount; physicalLine++) { + const m = /^\s*#line\s+(\d+)\s+"[^"]*"\s*$/.exec(model.getLineContent(physicalLine)); + if (m) { + sawDirective = true; + curLine = parseInt(m[1], 10); + if (curLine === originalLine) { + return { line: physicalLine + 1, columnReliable: false }; + } + continue; + } + if (curLine !== null) { + if (curLine === originalLine && fallback === null) { + fallback = { line: physicalLine, columnReliable: false }; + } + curLine++; + } + } + if (sawDirective) return fallback; + return { line: originalLine, columnReliable: true }; +} + +let yamlCursorDecorations = []; + +function highlightCLocationForYamlCursor() { + if (!yamlEditor || !cEditor) return; + const model = cEditor.getModel(); + if (!model) return; + + const pos = yamlEditor.getPosition(); + const waypoint = pos + ? parseWaypointLocations(yamlEditor.getValue()).find( + (wp) => pos.lineNumber >= wp.startLine && pos.lineNumber <= wp.endLine + ) + : null; + + const resolved = waypoint && waypoint.cLine ? resolvePhysicalLine(model, waypoint.cLine) : null; + if (!resolved || resolved.line > model.getLineCount()) { + yamlCursorDecorations = model.deltaDecorations(yamlCursorDecorations, []); + return; + } + + const { line, columnReliable } = resolved; + cEditor.revealLineInCenterIfOutsideViewport(line); + const decorations = [ + { + range: new monaco.Range(line, 1, line, 1), + options: { isWholeLine: true, className: "cwt-waypoint-location-line" }, + }, + ]; + if (columnReliable) { + const column = Math.min(waypoint.cColumn, model.getLineMaxColumn(line)); + decorations.push({ + range: new monaco.Range(line, column, line, column + 1), + options: { inlineClassName: "cwt-waypoint-location-col" }, + }); + } + yamlCursorDecorations = model.deltaDecorations(yamlCursorDecorations, decorations); +} + // --------------------------------------------------------------------------- // Witness metadata skeleton // --------------------------------------------------------------------------- @@ -485,16 +682,19 @@ async function runInstrumentPipeline() { logOutput("instrument", `Instrumentation failed to run:\n${response.error}`); return null; } - const { ok, source, error, log, data_race } = response.result; + const { ok, source, error, log, data_race, no_overflow } = response.result; if (!ok) { logOutput("instrument", `Instrumentation failed:\n${error}\n${log || ""}`); return null; } + const notes = []; + if (data_race) notes.push("data-race witness: compile with -fsanitize=thread"); + if (no_overflow) notes.push("overflow witness: compile with -fsanitize=undefined -fno-sanitize-recover=all"); logOutput( "instrument", - `Instrumented successfully${data_race ? " (data-race witness: compile with -fsanitize=thread)" : ""}.` + `Instrumented successfully${notes.length ? " (" + notes.join("; ") + ")" : ""}.` ); - return { source, dataRace: !!data_race }; + return { source, dataRace: !!data_race, noOverflow: !!no_overflow }; } // --------------------------------------------------------------------------- @@ -513,11 +713,17 @@ async function getSvcompSource() { return svcompSourceCache; } -function buildMakefile(dataRace) { - const extraFlags = dataRace ? " -fsanitize=thread -g" : ""; - const runCmd = dataRace - ? 'TSAN_OPTIONS="halt_on_error=1 exitcode=74" ./$(TARGET)' - : "./$(TARGET)"; +function buildMakefile(dataRace, noOverflow) { + let extraFlags = ""; + let runCmd = "./$(TARGET)"; + if (dataRace) { + extraFlags += " -fsanitize=thread -g"; + runCmd = 'TSAN_OPTIONS="halt_on_error=1 exitcode=74" ./$(TARGET)'; + } + if (noOverflow) { + extraFlags += " -fsanitize=undefined -fno-sanitize-recover=all -g"; + runCmd = 'UBSAN_OPTIONS="halt_on_error=1:exitcode=74:print_stacktrace=1" ./$(TARGET)'; + } return `CC ?= gcc CFLAGS ?= -w -Wno-implicit-function-declaration -pthread${extraFlags} TARGET ?= a.out @@ -656,7 +862,7 @@ async function runInstrument(mode) { const zipBlob = makeZipFromTexts([ { name: "instrumented.c", content: source }, { name: "svcomp.c", content: svcompSource }, - { name: "Makefile", content: buildMakefile(dataRace) }, + { name: "Makefile", content: buildMakefile(dataRace, noOverflow) }, ]); const name = (cFilename.textContent || "instrumented").replace(/\.[ci]$/, "") + "-bundle.zip"; downloadBlob(name, zipBlob); @@ -946,6 +1152,7 @@ function wireRefPicker(inputId, onChange) { wireRefPicker("sv-witnesses-ref", () => renderSvWitnessesExamples()); wireRefPicker("sv-benchmarks-ref", () => renderSvBenchmarksCategories()); +renderLocalExamples(); renderSvWitnessesExamples(); renderSvBenchmarksCategories(); initEditors(); diff --git a/www-demo/index.html b/www-demo/index.html index 736e4175cf..f1c25a7244 100644 --- a/www-demo/index.html +++ b/www-demo/index.html @@ -29,6 +29,13 @@

Concurrent Violation Witness Playground