From 0edb1a739653211488c17e2b9d6f6775c5320034 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sun, 21 Jun 2026 16:13:30 +0200 Subject: [PATCH 01/10] Updated demo site and handled feature set --- example/concurrent-nondet.i | 29 ++ example/concurrent-nondet.witness-2.2.yml | 76 +++++ example/function-return.i | 19 ++ example/function-return.witness-2.2.yml | 45 +++ example/no-overflow.i | 13 + example/no-overflow.witness-2.2.yml | 53 +++ main.py | 23 ++ smoketest.sh | 9 + svcomp.c | 66 ++++ tweaks.py | 6 +- witness2ast.py | 398 ++++++++++++++++++++-- witnessparser.py | 47 ++- www-demo/Dockerfile | 3 + www-demo/README.md | 19 +- www-demo/app.js | 173 +++++++++- www-demo/index.html | 7 + www-demo/py/cwt/instrument.py | 2 +- www-demo/py/shim.py | 3 +- www-demo/style.css | 10 + 19 files changed, 951 insertions(+), 50 deletions(-) create mode 100644 example/concurrent-nondet.i create mode 100644 example/concurrent-nondet.witness-2.2.yml create mode 100644 example/function-return.i create mode 100644 example/function-return.witness-2.2.yml create mode 100644 example/no-overflow.i create mode 100644 example/no-overflow.witness-2.2.yml diff --git a/example/concurrent-nondet.i b/example/concurrent-nondet.i new file mode 100644 index 000000000..b4d6a5f73 --- /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 000000000..48da63415 --- /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 000000000..c7eeb77be --- /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 000000000..96c0b5278 --- /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/no-overflow.i b/example/no-overflow.i new file mode 100644 index 000000000..3d7d600f9 --- /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 000000000..e37f4c717 --- /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 407dce7ac..b20f6124a 100644 --- a/main.py +++ b/main.py @@ -81,6 +81,12 @@ 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") + try: fix_inline(ast) fix_struct_def(ast) @@ -101,6 +107,11 @@ 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 [] + ) + [ tmp.name, os.path.dirname(os.path.abspath(sys.argv[0])) + os.sep + "svcomp.c", @@ -123,6 +134,11 @@ 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" codes = {} for i in range(100): try: @@ -147,6 +163,13 @@ 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 result.stdout: print(result.stdout) if result.stderr: diff --git a/smoketest.sh b/smoketest.sh index 268c9f448..85d49efae 100755 --- a/smoketest.sh +++ b/smoketest.sh @@ -17,3 +17,12 @@ check_verdict ./start.sh example/concurrent-unreach.i --witness example/concurre # 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 6fcde0a3b..1ced21987 100644 --- a/svcomp.c +++ b/svcomp.c @@ -39,6 +39,18 @@ 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 the constructor below. */ +static _Thread_local int c2tt_logical_tid = -1; + +/* Pre-initialize the main thread's logical tid before main() runs. */ +__attribute__((constructor)) +static void c2tt_main_thread_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. */ static void c2tt_initialize(void) { @@ -47,7 +59,57 @@ 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; +} + +/* 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); + 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 +129,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) { diff --git a/tweaks.py b/tweaks.py index c8d58a175..4fad4fcee 100644 --- a/tweaks.py +++ b/tweaks.py @@ -19,7 +19,7 @@ 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,6 +31,10 @@ 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 *__c2tt_thread_proxy(void *);\n" + "void *__c2tt_make_thread_arg(void *(*)(void *), void *, int);\n" + "void exit(int);\n" ) .ext ) diff --git a/witness2ast.py b/witness2ast.py index 04cd8f559..edcafd1e2 100644 --- a/witness2ast.py +++ b/witness2ast.py @@ -19,14 +19,52 @@ 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 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 guarded + ``if (!(EXPR)) exit(0);`` -- if the witness' assumption does not hold on + this particular execution, that execution is not a witness replay and + exits cleanly rather than running on down an unwitnessed path. + +* ``branching`` waypoints re-check the branching statement's controlling + expression against the witness' recorded direction (or, for ``switch``, + its integer constant) and ``exit(0)`` on a mismatch, under the same + segment/thread guard. 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 +75,7 @@ import re +from pycparser import CParser from pycparser.c_ast import ( Compound, If, @@ -50,6 +89,9 @@ ExprList, Constant, Assignment, + TernaryOp, + UnaryOp, + BinaryOp, ) from Exceptions import KnownErrorVerdict @@ -125,6 +167,32 @@ 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 find_first_statement_on_line(ast, target_line, target_file): class LineVisitor(NodeVisitor): def __init__(self, target_line, target_file): @@ -160,6 +228,91 @@ def visit_Compound(self, node): return None, None +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: + 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 = { "__VERIFIER_nondet_bool": "_Bool", "__VERIFIER_nondet_char": "char", @@ -191,12 +344,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_exit_call(): + return FuncCall(ID("exit"), ExprList([Constant(type="int", value="0")])) + + +def wrap_with_match_guard(stmt, slot, logical_tid): + """Wrap `stmt` in ``if (__c2tt_should_use_assumed(slot, tid)) { stmt }`` + so it only runs in the exact segment/thread the witness means it for. + With slot/logical_tid unknown (GraphML) the statement runs unguarded. + """ + if slot is None or logical_tid is None: + return stmt + return If( + cond=make_segment_match_call(slot, logical_tid), + iftrue=Compound(block_items=[stmt]), + iffalse=None, + ) + + +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 ``if (!(EXPR)) exit(0);`` (under the segment/thread guard) + 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 + + check = If( + cond=UnaryOp("!", expr), + iftrue=Compound(block_items=[make_exit_call()]), + iffalse=None, + ) + guard = wrap_with_match_guard(check, slot, logical_tid) + idx = parent.block_items.index(statement) + parent.block_items.insert(idx, guard) + + +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 @@ -211,16 +449,51 @@ def apply_assumption(ast, line, assumption, target_file, anchored_after=False): ) else: nondet_assign_node, _ = find_nondet_assignment_on_line(ast, line, target_file) - if nondet_assign_node is None: + + if nondet_assign_node is not None: + varname = nondet_assign_node.lvalue.name + if varname in assumptions: + nondet_name = getattr(nondet_assign_node.rvalue.name, "name", None) + if nondet_name in nondet_return_types: + ret_type = nondet_return_types[nondet_name] + original_call = nondet_assign_node.rvalue + nondet_assign_node.rvalue = _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 return value of a __VERIFIER_nondet_*() return statement near `line`. + + The constraint value is parsed with the same ``var == value`` pattern + as assumptions (``var`` is ignored for return statements -- only the + value matters). The return expression is replaced by a runtime guard. + """ + values = re.findall(assumption_pattern, assumption) + if values: + value = values[0][1] + else: + # Allow bare literal: "5" or "-1" etc. + value = assumption.strip() + + ret_node = find_return_nondet_on_line(ast, line, target_file) + if ret_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] - ) + nondet_name = getattr(ret_node.expr.name, "name", None) + if nondet_name not in nondet_return_types: + return + + ret_type = nondet_return_types[nondet_name] + original_call = ret_node.expr + ret_node.expr = _make_guarded_nondet( + original_call, ret_type, value, slot, logical_tid + ) def make_schedule_call(name, slot, threadid): @@ -278,6 +551,45 @@ def insert_schedule_point(ast, line, slot, threadid, target_file, release=True): return slot + 1 +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, ``exit(0)`` on a mismatch. + + 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" + mismatch = UnaryOp("!", cond) if wanted_true else cond + else: + try: + int(constraint_value) + except (TypeError, ValueError): + # 'default' switch label or other unsupported constraint forms. + return + mismatch = BinaryOp( + "!=", cond, Constant(type="int", value=str(constraint_value)) + ) + + check = If( + cond=mismatch, + iftrue=Compound(block_items=[make_exit_call()]), + iffalse=None, + ) + guard = wrap_with_match_guard(check, slot, logical_tid) + idx = parent.block_items.index(statement) + parent.block_items.insert(idx, guard) + + def apply_witness(ast, c_file, witnessfile): """Instrument `ast` according to the witness; returns the ParsedWitness.""" witness = parse_witness(witnessfile, c_file) @@ -289,14 +601,60 @@ 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") diff --git a/witnessparser.py b/witnessparser.py index 7d31b0ec7..d979842ce 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,11 @@ 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 + def get_offset_of_line(c_file, line): with open(c_file, "r") as f: @@ -183,6 +191,25 @@ 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. + + ``branching`` waypoints omit ``format`` 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") != "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 +242,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 10695aa77..6bc30906f 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 1a87d2605..e5b7ef7d3 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 79793aa74..33761c7a6 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,69 @@ 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, + }; + }); +} + +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; + + if (!waypoint || !waypoint.cLine || waypoint.cLine > model.getLineCount()) { + yamlCursorDecorations = model.deltaDecorations(yamlCursorDecorations, []); + return; + } + + const column = Math.min(waypoint.cColumn, model.getLineMaxColumn(waypoint.cLine)); + cEditor.revealLineInCenterIfOutsideViewport(waypoint.cLine); + yamlCursorDecorations = model.deltaDecorations(yamlCursorDecorations, [ + { + range: new monaco.Range(waypoint.cLine, 1, waypoint.cLine, 1), + options: { isWholeLine: true, className: "cwt-waypoint-location-line" }, + }, + { + range: new monaco.Range(waypoint.cLine, column, waypoint.cLine, column + 1), + options: { inlineClassName: "cwt-waypoint-location-col" }, + }, + ]); +} + // --------------------------------------------------------------------------- // Witness metadata skeleton // --------------------------------------------------------------------------- @@ -485,16 +630,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 +661,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 +810,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 +1100,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 736e4175c..f1c25a724 100644 --- a/www-demo/index.html +++ b/www-demo/index.html @@ -29,6 +29,13 @@

Concurrent Violation Witness Playground