From 59fd2ede6e0da55b6488e1fa21d15a69943ee997 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 3 Mar 2026 18:14:19 +0000 Subject: [PATCH 1/4] Document --race-check instrumentation and fix help text Add Doxygen documentation to race_check.h explaining the Eraser-inspired write-guard instrumentation scheme for data-race detection, including the two kinds of races detected (R/W and W/W), the 5-step instrumentation sequence, and how pointer dereferences are resolved through value-set analysis for alias-aware race detection. Document internal functions in race_check.cpp. Fix the --race-check help text, man page, and cprover manual: the option performs general data-race checking, not floating-point specific checks. Add --race-check to the goto-instrument properties table in the cprover manual. Add regression tests exercising the basic race-check scenarios: write-write, read-write, no-race (thread-local), no-race (sequential), conditional write, and pointer-based race detection. Co-authored-by: Kiro --- doc/cprover-manual/properties.md | 1 + doc/man/goto-instrument.1 | 2 +- .../goto-instrument/race-check/conditional.c | 17 +++++++ .../race-check/conditional.desc | 9 ++++ .../race-check/no-race-sequential.c | 8 ++++ .../race-check/no-race-sequential.desc | 9 ++++ .../goto-instrument/race-check/no-race.c | 14 ++++++ .../goto-instrument/race-check/no-race.desc | 9 ++++ .../goto-instrument/race-check/pointer.c | 14 ++++++ .../goto-instrument/race-check/pointer.desc | 9 ++++ .../goto-instrument/race-check/read-write.c | 15 ++++++ .../race-check/read-write.desc | 9 ++++ .../goto-instrument/race-check/write-write.c | 14 ++++++ .../race-check/write-write.desc | 9 ++++ .../goto_instrument_parse_options.cpp | 2 +- src/goto-instrument/race_check.cpp | 18 ++++++++ src/goto-instrument/race_check.h | 46 +++++++++++++++++++ 17 files changed, 203 insertions(+), 2 deletions(-) create mode 100644 regression/goto-instrument/race-check/conditional.c create mode 100644 regression/goto-instrument/race-check/conditional.desc create mode 100644 regression/goto-instrument/race-check/no-race-sequential.c create mode 100644 regression/goto-instrument/race-check/no-race-sequential.desc create mode 100644 regression/goto-instrument/race-check/no-race.c create mode 100644 regression/goto-instrument/race-check/no-race.desc create mode 100644 regression/goto-instrument/race-check/pointer.c create mode 100644 regression/goto-instrument/race-check/pointer.desc create mode 100644 regression/goto-instrument/race-check/read-write.c create mode 100644 regression/goto-instrument/race-check/read-write.desc create mode 100644 regression/goto-instrument/race-check/write-write.c create mode 100644 regression/goto-instrument/race-check/write-write.desc diff --git a/doc/cprover-manual/properties.md b/doc/cprover-manual/properties.md index cd81a5d4635..a074078b70a 100644 --- a/doc/cprover-manual/properties.md +++ b/doc/cprover-manual/properties.md @@ -130,6 +130,7 @@ The goto-instrument program supports these checks: | `--undefined-shift-check` | add range checks for shift distances | | `--nan-check` | add floating-point NaN checks | | `--uninitialized-check` | add checks for uninitialized locals (experimental) | +| `--race-check` | add data race checks for concurrent programs | | `--error-label label` | check that given label is unreachable | As all of these checks apply across the entire input program, we may wish to diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 5d971063565..afd4d967b70 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -249,7 +249,7 @@ add checks for uninitialized locals (experimental) add check that call stack size of non\-inlined functions never exceeds n .TP \fB\-\-race\-check\fR -add floating\-point data race checks +add data race checks for concurrent programs .SS "Semantic transformations:" .TP \fB\-\-nondet\-volatile\fR diff --git a/regression/goto-instrument/race-check/conditional.c b/regression/goto-instrument/race-check/conditional.c new file mode 100644 index 00000000000..f71d6451340 --- /dev/null +++ b/regression/goto-instrument/race-check/conditional.c @@ -0,0 +1,17 @@ +int shared; +_Bool flag; + +void thread(void) +{ + if(flag) + shared = 1; +} + +int main(void) +{ + flag = 1; +__CPROVER_ASYNC_0: + thread(); + shared = 2; + return 0; +} diff --git a/regression/goto-instrument/race-check/conditional.desc b/regression/goto-instrument/race-check/conditional.desc new file mode 100644 index 00000000000..9b62fe820b7 --- /dev/null +++ b/regression/goto-instrument/race-check/conditional.desc @@ -0,0 +1,9 @@ +CORE +conditional.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +W/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/no-race-sequential.c b/regression/goto-instrument/race-check/no-race-sequential.c new file mode 100644 index 00000000000..1a68d84bd04 --- /dev/null +++ b/regression/goto-instrument/race-check/no-race-sequential.c @@ -0,0 +1,8 @@ +int shared; + +int main(void) +{ + shared = 1; + shared = 2; + return 0; +} diff --git a/regression/goto-instrument/race-check/no-race-sequential.desc b/regression/goto-instrument/race-check/no-race-sequential.desc new file mode 100644 index 00000000000..42c0361d6f6 --- /dev/null +++ b/regression/goto-instrument/race-check/no-race-sequential.desc @@ -0,0 +1,9 @@ +CORE +no-race-sequential.c +--race-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +FAILED diff --git a/regression/goto-instrument/race-check/no-race.c b/regression/goto-instrument/race-check/no-race.c new file mode 100644 index 00000000000..2d8b8943ddb --- /dev/null +++ b/regression/goto-instrument/race-check/no-race.c @@ -0,0 +1,14 @@ +__CPROVER_thread_local int thread_local_var; + +void thread(void) +{ + thread_local_var = 1; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + thread(); + thread_local_var = 2; + return 0; +} diff --git a/regression/goto-instrument/race-check/no-race.desc b/regression/goto-instrument/race-check/no-race.desc new file mode 100644 index 00000000000..828749ed230 --- /dev/null +++ b/regression/goto-instrument/race-check/no-race.desc @@ -0,0 +1,9 @@ +CORE +no-race.c +--race-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +FAILED diff --git a/regression/goto-instrument/race-check/pointer.c b/regression/goto-instrument/race-check/pointer.c new file mode 100644 index 00000000000..d1bea54ae85 --- /dev/null +++ b/regression/goto-instrument/race-check/pointer.c @@ -0,0 +1,14 @@ +int x; + +void thread(int *p) +{ + *p = 1; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + thread(&x); + x = 2; + return 0; +} diff --git a/regression/goto-instrument/race-check/pointer.desc b/regression/goto-instrument/race-check/pointer.desc new file mode 100644 index 00000000000..bee1f5a1196 --- /dev/null +++ b/regression/goto-instrument/race-check/pointer.desc @@ -0,0 +1,9 @@ +CORE +pointer.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +data race on x +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/read-write.c b/regression/goto-instrument/race-check/read-write.c new file mode 100644 index 00000000000..46edb50a447 --- /dev/null +++ b/regression/goto-instrument/race-check/read-write.c @@ -0,0 +1,15 @@ +int shared; + +void thread(void) +{ + shared = 1; +} + +int main(void) +{ + int local; +__CPROVER_ASYNC_0: + thread(); + local = shared; + return 0; +} diff --git a/regression/goto-instrument/race-check/read-write.desc b/regression/goto-instrument/race-check/read-write.desc new file mode 100644 index 00000000000..57beaded5c4 --- /dev/null +++ b/regression/goto-instrument/race-check/read-write.desc @@ -0,0 +1,9 @@ +CORE +read-write.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +R/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/write-write.c b/regression/goto-instrument/race-check/write-write.c new file mode 100644 index 00000000000..3bb0020910e --- /dev/null +++ b/regression/goto-instrument/race-check/write-write.c @@ -0,0 +1,14 @@ +int shared; + +void thread(void) +{ + shared = 1; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + thread(); + shared = 2; + return 0; +} diff --git a/regression/goto-instrument/race-check/write-write.desc b/regression/goto-instrument/race-check/write-write.desc new file mode 100644 index 00000000000..75f5ff59dc8 --- /dev/null +++ b/regression/goto-instrument/race-check/write-write.desc @@ -0,0 +1,9 @@ +CORE +write-write.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +W/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 570554155b4..86c51e70538 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1940,7 +1940,7 @@ void goto_instrument_parse_optionst::help() HELP_UNINITIALIZED_CHECK " {y--stack-depth} {un} \t add check that call stack size of non-inlined" " functions never exceeds {un}\n" - " {y--race-check} \t add floating-point data race checks\n" + " {y--race-check} \t add data race checks for concurrent programs\n" "\n" "Semantic transformations:\n" HELP_NONDET_VOLATILE diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index fce1b27d0ed..d7cf5cc82f9 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -10,6 +10,8 @@ Date: February 2006 /// \file /// Race Detection for Threaded Goto Programs +/// +/// \see race_check.h for an overview of the instrumentation scheme. #include "race_check.h" @@ -30,6 +32,10 @@ Date: February 2006 #define L_M_LAST_ARG(x) #endif +/// Manages boolean "write guard" variables used to detect concurrent writes. +/// For each shared variable `x`, a boolean symbol `x$w_guard` is created. +/// These guards are set to true around write accesses and checked by +/// assertions in other threads. class w_guardst { public: @@ -63,6 +69,9 @@ class w_guardst symbol_table_baset &symbol_table; }; +/// Get or create the boolean guard symbol for a shared variable. +/// \param object: the identifier of the shared variable +/// \return the guard symbol `$w_guard` const symbolt &w_guardst::get_guard_symbol(const irep_idt &object) { const irep_idt identifier=id2string(object)+"$w_guard"; @@ -86,6 +95,8 @@ const symbolt &w_guardst::get_guard_symbol(const irep_idt &object) return *symbol_ptr; } +/// Insert assignments to initialize all write guard variables to false +/// at the beginning of the given program. void w_guardst::add_initialization(goto_programt &goto_program) const { goto_programt::targett t=goto_program.instructions.begin(); @@ -105,6 +116,10 @@ void w_guardst::add_initialization(goto_programt &goto_program) const } } +/// Build a human-readable comment for a race-check assertion. +/// \param entry: the read/write set entry describing the access +/// \param write: true if this is a W/W race check, false for R/W +/// \return a string like "R/W data race on x" or "W/W data race on x" static std::string comment(const rw_set_baset::entryt &entry, bool write) { std::string result; @@ -118,6 +133,8 @@ static std::string comment(const rw_set_baset::entryt &entry, bool write) return result; } +/// Check whether a symbol refers to a shared (non-thread-local) variable, +/// excluding internal CPROVER symbols that should not be race-checked. static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) { const irep_idt &identifier=symbol_expr.get_identifier(); @@ -135,6 +152,7 @@ static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) return symbol.is_shared(); } +/// Check whether any entry in the read/write set refers to a shared variable. static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set) { for(rw_set_baset::entriest::const_iterator diff --git a/src/goto-instrument/race_check.h b/src/goto-instrument/race_check.h index e4d6daa3443..6bcb0b8a203 100644 --- a/src/goto-instrument/race_check.h +++ b/src/goto-instrument/race_check.h @@ -10,6 +10,41 @@ Date: February 2006 /// \file /// Race Detection for Threaded Goto Programs +/// +/// This implements a data-race detector for concurrent programs, inspired by +/// the Eraser algorithm (Savage et al., "Eraser: A Dynamic Data Race Detector +/// for Multithreaded Programs", ACM TOCS 1997). While Eraser uses lockset +/// tracking at runtime, this implementation adapts the core idea for static +/// verification via bounded model checking: it instruments the program with +/// boolean "write guard" flags and assertions so that CBMC's exploration of +/// thread interleavings can reveal conflicting concurrent accesses. +/// +/// A data race occurs when two threads access the same shared memory location +/// concurrently and at least one access is a write. This instrumentation +/// detects two kinds of races: +/// - R/W races: one thread reads a variable while another writes it. +/// - W/W races: two threads write the same variable concurrently. +/// +/// For each assignment that accesses shared variables, the instrumentation +/// replaces the original instruction with the following sequence: +/// +/// 1. For each shared variable `x` written: set `x$w_guard` to the guard +/// condition under which the write occurs. +/// 2. Execute the original assignment. +/// 3. For each shared variable `x` written: reset `x$w_guard` to false. +/// 4. For each shared variable `y` read: assert `!y$w_guard` (R/W check). +/// 5. For each shared variable `x` written: assert `!x$w_guard` (W/W check). +/// +/// During symbolic execution of concurrent programs, CBMC explores thread +/// interleavings. If another thread's write guard is set (step 1) when the +/// current thread checks it (steps 4/5), the assertion fails, indicating a +/// data race. +/// +/// Pointer dereferences are resolved using value-set analysis (or, when +/// LOCAL_MAY is defined, local may-alias analysis) so that races through +/// aliased pointer accesses are detected. For example, if thread A writes +/// `*p` and thread B writes `x`, and `p` points to `x`, the instrumentation +/// will detect the W/W race on `x`. #ifndef CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H #define CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H @@ -25,6 +60,12 @@ class goto_programt; class message_handlert; class value_setst; +/// Instrument a single function with data-race detection assertions. +/// \param value_sets: value-set analysis results for pointer resolution +/// \param symbol_table: the symbol table (modified to add guard symbols) +/// \param function_id: identifier of the function being instrumented +/// \param goto_program: the function body to instrument +/// \param message_handler: handler for status and diagnostic messages void race_check( value_setst &, class symbol_table_baset &, @@ -35,6 +76,11 @@ void race_check( goto_programt &goto_program, message_handlert &); +/// Instrument all functions in a goto model with data-race detection +/// assertions. Skips the entry point and the initialization function. +/// \param value_sets: value-set analysis results for pointer resolution +/// \param goto_model: the goto model to instrument +/// \param message_handler: handler for status and diagnostic messages void race_check(value_setst &, goto_modelt &, message_handlert &); #endif // CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H From b0fa32455c93d77718c350c204db27c15445fdb2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 3 Mar 2026 19:25:22 +0000 Subject: [PATCH 2/4] Set property_class on --race-check assertions Set property_class to "race-check" on all generated assertions, consistent with other instrumentation passes (e.g., uninitialized-check, stack-depth). This enables users to filter race-check properties by class and produces property names like [main.race-check.1] instead of [main.1]. Co-authored-by: Kiro --- src/goto-instrument/race_check.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index d7cf5cc82f9..ea94b9c48f8 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -257,6 +257,7 @@ static void race_check( source_locationt annotated_location = original_instruction.source_location(); annotated_location.set_comment(comment(r_entry.second, false)); + annotated_location.set_property_class("race-check"); goto_program.insert_before( i_it, goto_programt::make_assertion( @@ -271,6 +272,7 @@ static void race_check( source_locationt annotated_location = original_instruction.source_location(); annotated_location.set_comment(comment(w_entry.second, true)); + annotated_location.set_property_class("race-check"); goto_program.insert_before( i_it, goto_programt::make_assertion( From 07f164a3471a549356798e05c5b96c80bdb01d36 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 3 Mar 2026 18:34:49 +0000 Subject: [PATCH 3/4] Fix --race-check to instrument all instruction types that can use shared variables The race-check instrumentation previously only instrumented ASSIGN instructions. This missed R/W data races where shared variables are read by other instruction types: - GOTO: reading a shared variable in a branch condition (if/while guard) - FUNCTION_CALL: reading shared variables as function arguments, writing return values - SET_RETURN_VALUE: reading a shared variable in a return statement - ASSUME/ASSERT: reading shared variables in conditions For these instructions, R/W and W/W race-check assertions are now inserted before the instruction to detect concurrent writes by other threads. Also add SET_RETURN_VALUE handling to rw_set_loct::compute(), which previously did not track reads from return statements. Also exclude function symbols from race checking: function symbols are not variables and should not generate race-check assertions when read as part of a FUNCTION_CALL instruction. Co-authored-by: Kiro --- .../race-check/function-call-arg.c | 19 +++++++++++ .../race-check/function-call-arg.desc | 9 +++++ .../race-check/function-call-lhs.c | 19 +++++++++++ .../race-check/function-call-lhs.desc | 9 +++++ .../goto-instrument/race-check/goto-guard.c | 16 +++++++++ .../race-check/goto-guard.desc | 9 +++++ .../race-check/no-race-sequential.desc | 1 - .../goto-instrument/race-check/no-race.desc | 1 - .../goto-instrument/race-check/return-value.c | 20 +++++++++++ .../race-check/return-value.desc | 9 +++++ src/goto-instrument/race_check.cpp | 33 +++++++++++++++++-- src/goto-instrument/race_check.h | 11 +++++-- src/goto-instrument/rw_set.cpp | 4 +++ 13 files changed, 153 insertions(+), 7 deletions(-) create mode 100644 regression/goto-instrument/race-check/function-call-arg.c create mode 100644 regression/goto-instrument/race-check/function-call-arg.desc create mode 100644 regression/goto-instrument/race-check/function-call-lhs.c create mode 100644 regression/goto-instrument/race-check/function-call-lhs.desc create mode 100644 regression/goto-instrument/race-check/goto-guard.c create mode 100644 regression/goto-instrument/race-check/goto-guard.desc create mode 100644 regression/goto-instrument/race-check/return-value.c create mode 100644 regression/goto-instrument/race-check/return-value.desc diff --git a/regression/goto-instrument/race-check/function-call-arg.c b/regression/goto-instrument/race-check/function-call-arg.c new file mode 100644 index 00000000000..a8f14c220e3 --- /dev/null +++ b/regression/goto-instrument/race-check/function-call-arg.c @@ -0,0 +1,19 @@ +int shared; + +void sink(int val) +{ + (void)val; +} + +void writer(void) +{ + shared = 42; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + writer(); + sink(shared); + return 0; +} diff --git a/regression/goto-instrument/race-check/function-call-arg.desc b/regression/goto-instrument/race-check/function-call-arg.desc new file mode 100644 index 00000000000..e52301f58b1 --- /dev/null +++ b/regression/goto-instrument/race-check/function-call-arg.desc @@ -0,0 +1,9 @@ +CORE +function-call-arg.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +R/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/function-call-lhs.c b/regression/goto-instrument/race-check/function-call-lhs.c new file mode 100644 index 00000000000..8bfa90d196c --- /dev/null +++ b/regression/goto-instrument/race-check/function-call-lhs.c @@ -0,0 +1,19 @@ +int shared; + +int source(void) +{ + return 42; +} + +void writer(void) +{ + shared = 1; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + writer(); + shared = source(); + return 0; +} diff --git a/regression/goto-instrument/race-check/function-call-lhs.desc b/regression/goto-instrument/race-check/function-call-lhs.desc new file mode 100644 index 00000000000..437083552d1 --- /dev/null +++ b/regression/goto-instrument/race-check/function-call-lhs.desc @@ -0,0 +1,9 @@ +CORE +function-call-lhs.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +W/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/goto-guard.c b/regression/goto-instrument/race-check/goto-guard.c new file mode 100644 index 00000000000..2a5f2540f29 --- /dev/null +++ b/regression/goto-instrument/race-check/goto-guard.c @@ -0,0 +1,16 @@ +int shared; + +void writer(void) +{ + shared = 42; +} + +int main(void) +{ +__CPROVER_ASYNC_0: + writer(); + if(shared) + { + } + return 0; +} diff --git a/regression/goto-instrument/race-check/goto-guard.desc b/regression/goto-instrument/race-check/goto-guard.desc new file mode 100644 index 00000000000..fb18c2debfd --- /dev/null +++ b/regression/goto-instrument/race-check/goto-guard.desc @@ -0,0 +1,9 @@ +CORE +goto-guard.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +R/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/no-race-sequential.desc b/regression/goto-instrument/race-check/no-race-sequential.desc index 42c0361d6f6..ba3c49dbc2b 100644 --- a/regression/goto-instrument/race-check/no-race-sequential.desc +++ b/regression/goto-instrument/race-check/no-race-sequential.desc @@ -6,4 +6,3 @@ no-race-sequential.c ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring -FAILED diff --git a/regression/goto-instrument/race-check/no-race.desc b/regression/goto-instrument/race-check/no-race.desc index 828749ed230..b2793c39b74 100644 --- a/regression/goto-instrument/race-check/no-race.desc +++ b/regression/goto-instrument/race-check/no-race.desc @@ -6,4 +6,3 @@ no-race.c ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring -FAILED diff --git a/regression/goto-instrument/race-check/return-value.c b/regression/goto-instrument/race-check/return-value.c new file mode 100644 index 00000000000..06bc6d74fdc --- /dev/null +++ b/regression/goto-instrument/race-check/return-value.c @@ -0,0 +1,20 @@ +int shared; + +int get_shared(void) +{ + return shared; +} + +void writer(void) +{ + shared = 42; +} + +int main(void) +{ + int local; +__CPROVER_ASYNC_0: + writer(); + local = get_shared(); + return 0; +} diff --git a/regression/goto-instrument/race-check/return-value.desc b/regression/goto-instrument/race-check/return-value.desc new file mode 100644 index 00000000000..f297e2f06db --- /dev/null +++ b/regression/goto-instrument/race-check/return-value.desc @@ -0,0 +1,9 @@ +CORE +return-value.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +R/W data race on shared +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index ea94b9c48f8..4ebbb78d3be 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -149,7 +149,7 @@ static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) return false; // no race check const symbolt &symbol=ns.lookup(identifier); - return symbol.is_shared(); + return !symbol.is_function() && symbol.is_shared(); } /// Check whether any entry in the read/write set refers to a shared variable. @@ -195,7 +195,7 @@ static void race_check( { goto_programt::instructiont &instruction=*i_it; - if(instruction.is_assign()) + if(instruction.is_assign() || instruction.is_function_call()) { rw_set_loct rw_set( ns, @@ -281,6 +281,35 @@ static void race_check( i_it--; // the for loop already counts us up } + else if( + instruction.is_goto() || instruction.is_assume() || + instruction.is_assert() || instruction.is_set_return_value()) + { + rw_set_loct rw_set( + ns, + value_sets, + function_id, + i_it L_M_LAST_ARG(local_may), + message_handler); + + if(!has_shared_entries(ns, rw_set)) + continue; + + // add R/W assertions for shared reads before the instruction + for(const auto &r_entry : rw_set.r_entries) + { + if(!is_shared(ns, r_entry.second.symbol_expr)) + continue; + + source_locationt annotated_location = instruction.source_location(); + annotated_location.set_comment(comment(r_entry.second, false)); + annotated_location.set_property_class("race-check"); + goto_program.insert_before( + i_it, + goto_programt::make_assertion( + w_guards.get_assertion(r_entry.second), annotated_location)); + } + } } remove_skip(goto_program); diff --git a/src/goto-instrument/race_check.h b/src/goto-instrument/race_check.h index 6bcb0b8a203..542e8bd3570 100644 --- a/src/goto-instrument/race_check.h +++ b/src/goto-instrument/race_check.h @@ -25,16 +25,21 @@ Date: February 2006 /// - R/W races: one thread reads a variable while another writes it. /// - W/W races: two threads write the same variable concurrently. /// -/// For each assignment that accesses shared variables, the instrumentation -/// replaces the original instruction with the following sequence: +/// For each assignment or function call that accesses shared variables, the +/// instrumentation replaces the original instruction with the following +/// sequence: /// /// 1. For each shared variable `x` written: set `x$w_guard` to the guard /// condition under which the write occurs. -/// 2. Execute the original assignment. +/// 2. Execute the original instruction. /// 3. For each shared variable `x` written: reset `x$w_guard` to false. /// 4. For each shared variable `y` read: assert `!y$w_guard` (R/W check). /// 5. For each shared variable `x` written: assert `!x$w_guard` (W/W check). /// +/// For instructions that only read shared variables (GOTO/ASSUME/ASSERT +/// guards, SET_RETURN_VALUE), only R/W assertions (step 4) are added before +/// the instruction. +/// /// During symbolic execution of concurrent programs, CBMC explores thread /// interleavings. If another thread's write guard is set (step 1) when the /// current thread checks it (steps 4/5), the assertion fails, indicating a diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp index b1c03a6c273..a5f81f287f2 100644 --- a/src/goto-instrument/rw_set.cpp +++ b/src/goto-instrument/rw_set.cpp @@ -68,6 +68,10 @@ void _rw_set_loct::compute() if(target->call_lhs().is_not_nil()) write(target->call_lhs()); } + else if(target->is_set_return_value()) + { + read(target->return_value()); + } } void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs) From bae0cd8d7541b6cface7d013ea1a70fce89a40e5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 3 Mar 2026 19:11:19 +0000 Subject: [PATCH 4/4] Use dirty-locals analysis in --race-check to detect races on address-taken locals The race-check instrumentation previously only considered globally shared variables (symbol.is_shared()). Local variables whose address is taken and passed to other threads ("dirty locals") were not instrumented, missing potential data races. Now use the dirtyt analysis, consistent with how goto-symex determines shared access: a variable is considered shared if symbol.is_shared() or dirty(identifier). The dirty analysis is computed once over all functions in the goto_modelt overload. Add a CORE regression test (dirty-local.desc) that verifies the instrumentation is generated for a dirty local by matching on the --show-goto-functions output. Add a KNOWNBUG regression test (dirty-local-verification.desc) that attempts full verification of the dirty-local race. This is marked KNOWNBUG because CBMC's symex currently aborts with "pointer handling for concurrency is unsound" when a pointer to a local is shared between threads. Co-authored-by: Kiro --- .../race-check/dirty-local-verification.desc | 14 ++++++ .../goto-instrument/race-check/dirty-local.c | 13 ++++++ .../race-check/dirty-local.desc | 9 ++++ src/goto-instrument/race_check.cpp | 43 +++++++++++++------ 4 files changed, 67 insertions(+), 12 deletions(-) create mode 100644 regression/goto-instrument/race-check/dirty-local-verification.desc create mode 100644 regression/goto-instrument/race-check/dirty-local.c create mode 100644 regression/goto-instrument/race-check/dirty-local.desc diff --git a/regression/goto-instrument/race-check/dirty-local-verification.desc b/regression/goto-instrument/race-check/dirty-local-verification.desc new file mode 100644 index 00000000000..b0134e4c089 --- /dev/null +++ b/regression/goto-instrument/race-check/dirty-local-verification.desc @@ -0,0 +1,14 @@ +// This test verifies that --race-check detects a W/W data race on a +// dirty local variable (a local whose address is passed to another thread). +// It is marked KNOWNBUG because CBMC's symex aborts with "pointer handling +// for concurrency is unsound" when a pointer to a local variable is shared +// between threads, preventing verification from completing. +KNOWNBUG +dirty-local.c +--race-check +^EXIT=10$ +^SIGNAL=0$ +W/W data race on main::1::local +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/race-check/dirty-local.c b/regression/goto-instrument/race-check/dirty-local.c new file mode 100644 index 00000000000..7b03fe1a6be --- /dev/null +++ b/regression/goto-instrument/race-check/dirty-local.c @@ -0,0 +1,13 @@ +void writer(int *p) +{ + *p = 42; +} + +int main(void) +{ + int local = 0; +__CPROVER_ASYNC_0: + writer(&local); + local = 1; + return 0; +} diff --git a/regression/goto-instrument/race-check/dirty-local.desc b/regression/goto-instrument/race-check/dirty-local.desc new file mode 100644 index 00000000000..8bae3904b2f --- /dev/null +++ b/regression/goto-instrument/race-check/dirty-local.desc @@ -0,0 +1,9 @@ +CORE +dirty-local.c +--race-check +ASSIGN main::1::local\$w_guard := true +W/W data race on main::1::local +^EXIT=6$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index 4ebbb78d3be..f0151941f2b 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -19,6 +19,7 @@ Date: February 2006 #include +#include #include #include "rw_set.h" @@ -135,7 +136,13 @@ static std::string comment(const rw_set_baset::entryt &entry, bool write) /// Check whether a symbol refers to a shared (non-thread-local) variable, /// excluding internal CPROVER symbols that should not be race-checked. -static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) +/// A variable is considered shared if it is globally shared or if it is a +/// "dirty" local (its address has been taken, so it may be accessible from +/// other threads). +static bool is_shared( + const namespacet &ns, + const symbol_exprt &symbol_expr, + const dirtyt &dirty) { const irep_idt &identifier=symbol_expr.get_identifier(); @@ -149,24 +156,27 @@ static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) return false; // no race check const symbolt &symbol=ns.lookup(identifier); - return !symbol.is_function() && symbol.is_shared(); + return !symbol.is_function() && (symbol.is_shared() || dirty(identifier)); } /// Check whether any entry in the read/write set refers to a shared variable. -static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set) +static bool has_shared_entries( + const namespacet &ns, + const rw_set_baset &rw_set, + const dirtyt &dirty) { for(rw_set_baset::entriest::const_iterator it=rw_set.r_entries.begin(); it!=rw_set.r_entries.end(); it++) - if(is_shared(ns, it->second.symbol_expr)) + if(is_shared(ns, it->second.symbol_expr, dirty)) return true; for(rw_set_baset::entriest::const_iterator it=rw_set.w_entries.begin(); it!=rw_set.w_entries.end(); it++) - if(is_shared(ns, it->second.symbol_expr)) + if(is_shared(ns, it->second.symbol_expr, dirty)) return true; return false; @@ -182,6 +192,7 @@ static void race_check( L_M_ARG(const goto_functionst::goto_functiont &goto_function) goto_programt &goto_program, w_guardst &w_guards, + const dirtyt &dirty, message_handlert &message_handler) // clang-format on { @@ -204,7 +215,7 @@ static void race_check( i_it L_M_LAST_ARG(local_may), message_handler); - if(!has_shared_entries(ns, rw_set)) + if(!has_shared_entries(ns, rw_set, dirty)) continue; goto_programt::instructiont original_instruction; @@ -217,7 +228,7 @@ static void race_check( // now add assignments for what is written -- set for(const auto &w_entry : rw_set.w_entries) { - if(!is_shared(ns, w_entry.second.symbol_expr)) + if(!is_shared(ns, w_entry.second.symbol_expr, dirty)) continue; goto_program.insert_before( @@ -237,7 +248,7 @@ static void race_check( // now add assignments for what is written -- reset for(const auto &w_entry : rw_set.w_entries) { - if(!is_shared(ns, w_entry.second.symbol_expr)) + if(!is_shared(ns, w_entry.second.symbol_expr, dirty)) continue; goto_program.insert_before( @@ -251,7 +262,7 @@ static void race_check( // now add assertions for what is read and written for(const auto &r_entry : rw_set.r_entries) { - if(!is_shared(ns, r_entry.second.symbol_expr)) + if(!is_shared(ns, r_entry.second.symbol_expr, dirty)) continue; source_locationt annotated_location = @@ -266,7 +277,7 @@ static void race_check( for(const auto &w_entry : rw_set.w_entries) { - if(!is_shared(ns, w_entry.second.symbol_expr)) + if(!is_shared(ns, w_entry.second.symbol_expr, dirty)) continue; source_locationt annotated_location = @@ -292,13 +303,13 @@ static void race_check( i_it L_M_LAST_ARG(local_may), message_handler); - if(!has_shared_entries(ns, rw_set)) + if(!has_shared_entries(ns, rw_set, dirty)) continue; // add R/W assertions for shared reads before the instruction for(const auto &r_entry : rw_set.r_entries) { - if(!is_shared(ns, r_entry.second.symbol_expr)) + if(!is_shared(ns, r_entry.second.symbol_expr, dirty)) continue; source_locationt annotated_location = instruction.source_location(); @@ -326,6 +337,11 @@ void race_check( message_handlert &message_handler) { w_guardst w_guards(symbol_table); + // When called for a single function we don't have the full goto_functions + // to build a complete dirtyt, so we use an empty one. The goto_modelt + // overload below computes a proper whole-program dirty analysis. + dirtyt dirty; + dirty.build(goto_functionst()); race_check( value_sets, @@ -333,6 +349,7 @@ void race_check( function_id, L_M_ARG(goto_function) goto_program, w_guards, + dirty, message_handler); w_guards.add_initialization(goto_program); @@ -345,6 +362,7 @@ void race_check( message_handlert &message_handler) { w_guardst w_guards(goto_model.symbol_table); + dirtyt dirty(goto_model.goto_functions); for(auto &gf_entry : goto_model.goto_functions.function_map) { @@ -358,6 +376,7 @@ void race_check( gf_entry.first, L_M_ARG(gf_entry.second) gf_entry.second.body, w_guards, + dirty, message_handler); } }