Draft
Conversation
Collaborator
tautschnig
commented
Mar 31, 2026
tautschnig
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
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 <kiro-agent@users.noreply.github.com>
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 <kiro-agent@users.noreply.github.com>
…red 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 <kiro-agent@users.noreply.github.com>
…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 <kiro-agent@users.noreply.github.com>
Add scripts/coverage_report.py that parses lcov .info files and reports: - Per-module coverage sorted worst-first - Files with 0% coverage - Files with very low coverage (<20%) Supports both text and --markdown output. Integrated into the coverage CI workflow as a step summary. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises unified_diff.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises change_impact.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Tests goto-cl, goto-link, goto-armcc, goto-as, and goto-cw modes via a modes.sh helper that creates symlinks to goto-cc. Exercises ms_cl_mode.cpp, ms_link_mode.cpp, armcc_mode.cpp, as_mode.cpp, and cw_mode.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…enumerator In sat_path_enumerator::build_fixed(), the conditions for forward jumps were inverted: !loop.contains(target) (target outside loop) was treated as 'within the loop' and vice versa. Additionally, modifying fixedt->targets while iterating over t->targets caused loss of multi-target GOTO information. Fix by: 1. Correcting the condition: forward jumps outside the loop are killed, forward jumps within the loop are kept. 2. Collecting all target decisions before modifying fixedt->targets. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
scratch_programt::get_default_options() did not set the 'depth' option, causing symex_configt::max_depth to default to 0. This made symex kill all paths after the very first instruction, rendering the entire SAT-based path enumeration and polynomial fitting non-functional. Set depth to UINT_MAX so scratch programs can be fully explored. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
extract_polynomial() used binary2integer() to parse coefficient values, but constant_exprt stores bitvector values in bvrep format (hexadecimal strings via integer2bvrep), not binary strings. This caused coefficient 1 to be interpreted as signed 1-bit binary (-1) and coefficient 2 to be parsed as invalid binary (0), producing completely wrong polynomials. Fix by using bvrep2integer() which correctly handles the bvrep format. Also switch the scratch program's decision procedure back to the SAT solver (bv_pointerst) from Z3 (smt2_dect). Promotes 10 KNOWNBUG acceleration tests to CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The polynomial fitting overflow check rejected negative signed coefficients when cast to unsigned, preventing acceleration of decrementing loops like 'x -= 2'. For unsigned target variables, wrapping arithmetic is well-defined, so the overflow check on the polynomial expression is unnecessary. Promotes simple_unsafe4 (decrementing unsigned loop) to CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Array-safe tests require Z3 (smt-backend tag) since proving correctness requires the quantified array constraints to be interpreted. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The loop accelerator only handles innermost loops. The outer loop contains a nested inner loop, so it is skipped. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises show_locations.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises skip_loops.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises havoc_loops.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises undefined_functions.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises function_assigns.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises points_to.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises alignment_checks.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises loop_ids.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises show_goto_functions_xml.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises counterexample_beautification.cpp, prop_minimize.cpp, and bv_minimize.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises call_sequences.cpp which previously had <20% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises branch.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises function.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises interrupt.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercises thread_instrumentation.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…e-false Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Further exercises function.cpp. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
global_may_alias_domaint::transform() had a DATA_INVARIANT(false) for OTHER instructions, causing a crash on any program with OUTPUT or similar OTHER-type instructions. Ignoring OTHER is a valid over-approximation, consistent with how ASSUME and SKIP are handled. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
interval_domaint::transform() requires SET_RETURN_VALUE instructions to be removed before analysis, but --show-intervals did not call do_remove_returns(). This caused a DATA_INVARIANT crash on any program. Add the missing do_remove_returns() call, consistent with how --show-global-may-alias handles this. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The --mmio option was not registered in the option definitions, causing the command-line parser to treat it as a positional argument. Also, the guard condition for the analysis block that includes mmio did not check for --mmio, so the value_set_analysis setup was skipped. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The --concurrency option was not registered, causing the command-line parser to treat it as a positional argument. Exercises concurrency.cpp which previously had 0% coverage. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8940 +/- ##
===========================================
+ Coverage 80.00% 81.78% +1.77%
===========================================
Files 1703 1704 +1
Lines 188397 188694 +297
Branches 73 73
===========================================
+ Hits 150736 154325 +3589
+ Misses 37661 34369 -3292 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.