From f03192d5b6044288d892dd1786d2fc9f2890cb61 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 30 Nov 2025 19:59:46 +0000 Subject: [PATCH] Fix basic block coverage with unsatisfiable ASSUME statements Insert coverage assertions at the end of basic blocks instead of the beginning to ensure blocks are only marked as covered when all instructions, including ASSUME statements, can be executed. Fixes: #826 --- .../cbmc-cover/block-assume-coverage/main.c | 33 +++++++++++++++++++ .../block-assume-coverage/test.desc | 10 ++++++ src/goto-instrument/cover_basic_blocks.cpp | 8 +++-- src/goto-instrument/cover_basic_blocks.h | 4 +-- .../cover_instrument_location.cpp | 7 +++- 5 files changed, 57 insertions(+), 5 deletions(-) create mode 100644 regression/cbmc-cover/block-assume-coverage/main.c create mode 100644 regression/cbmc-cover/block-assume-coverage/test.desc diff --git a/regression/cbmc-cover/block-assume-coverage/main.c b/regression/cbmc-cover/block-assume-coverage/main.c new file mode 100644 index 00000000000..7cad1d01718 --- /dev/null +++ b/regression/cbmc-cover/block-assume-coverage/main.c @@ -0,0 +1,33 @@ +// Test for issue #826: Basic blocks incorrectly considered covered +// with unsatisfiable ASSUME statements +// +// This test demonstrates that basic blocks should only be marked as +// covered when ALL instructions in the block can execute, including +// ASSUME statements. +// +// Before the fix: Block 3 would be incorrectly marked as SATISFIED +// because the coverage assertion was at the beginning of the block. +// After the fix: Block 3 is correctly marked as FAILED because the +// ASSUME statement is unsatisfiable (x >= 0 when x < 0). + +int main() +{ + int x; + + // Block with satisfiable ASSUME - should be covered + if(x > 0) + { + __CPROVER_assume(x > 0); + return 1; + } + + // Block with unsatisfiable ASSUME - should NOT be covered + if(x < 0) + { + __CPROVER_assume(x >= 0); + return 2; + } + + // Block with no ASSUME - should be covered + return 0; +} diff --git a/regression/cbmc-cover/block-assume-coverage/test.desc b/regression/cbmc-cover/block-assume-coverage/test.desc new file mode 100644 index 00000000000..2919af66342 --- /dev/null +++ b/regression/cbmc-cover/block-assume-coverage/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--cover location +^EXIT=0$ +^SIGNAL=0$ +block 1 \(lines main.c:main:\d+\): SATISFIED +block 2 \(lines main.c:main:\d+\): SATISFIED +block 3 \(lines main.c:main:\d+\): FAILED +block 4 \(lines main.c:main:\d+\): SATISFIED +-- diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index 23df805b4dc..396f4683992 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -63,6 +63,7 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) else { block_infos.emplace_back(); + // representative_inst will be updated to the last instruction block_infos.back().representative_inst = it; block_infos.back().source_location = source_locationt::nil(); current_block = block_infos.size() - 1; @@ -77,7 +78,11 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) add_block_lines(block_info, *it); - // set representative program location to instrument + // Update representative instruction to always be the last instruction + block_info.representative_inst = it; + + // set source location for reporting (from first instruction with valid + // location) if( !it->source_location().is_nil() && !it->source_location().get_file().empty() && @@ -85,7 +90,6 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) !it->source_location().is_built_in() && block_info.source_location.is_nil()) { - block_info.representative_inst = it; // update block_info.source_location = it->source_location(); } diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h index 8c9bd2c2a89..d65b4da6536 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/src/goto-instrument/cover_basic_blocks.h @@ -74,7 +74,7 @@ class cover_basic_blockst final : public cover_blocks_baset /// \param block_nr: a block number /// \return the instruction selected for - /// instrumentation representative of the given block + /// instrumentation representative of the given block (last instruction) std::optional instruction_of(std::size_t block_nr) const override; @@ -109,7 +109,7 @@ class cover_basic_blockst final : public cover_blocks_baset struct block_infot { - /// the program location to instrument for this block + /// the program location to instrument for this block (last instruction) std::optional representative_inst; /// the source location representative for this block diff --git a/src/goto-instrument/cover_instrument_location.cpp b/src/goto-instrument/cover_instrument_location.cpp index 64b93dc1936..ca7af1f0674 100644 --- a/src/goto-instrument/cover_instrument_location.cpp +++ b/src/goto-instrument/cover_instrument_location.cpp @@ -25,8 +25,13 @@ void cover_location_instrumentert::instrument( i_it->turn_into_skip(); const std::size_t block_nr = basic_blocks.block_of(i_it); + + // The representative instruction is the last instruction in the block, + // ensuring all instructions (including any ASSUME statements) can be + // executed. const auto representative_instruction = basic_blocks.instruction_of(block_nr); - // we only instrument the selected instruction + + // we only instrument the selected instruction (last in block) if(representative_instruction && *representative_instruction == i_it) { const std::string b = std::to_string(block_nr + 1); // start with 1