Fix duplicate conflicting dead branch warnings due to loop unrolling

[sim642]

Previously the added test output contained

[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (tests/regression/55-loop-unrolling/14-unrolled-loop-dead-branch.c:3:17-3:24)
[Warning][Deadcode][CWE-570] condition 'i == 1' is always false (tests/regression/55-loop-unrolling/14-unrolled-loop-dead-branch.c:4:9-4:15)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (tests/regression/55-loop-unrolling/14-unrolled-loop-dead-branch.c:3:17-3:24)
[Warning][Deadcode][CWE-571] condition 'i == 1' is always true (tests/regression/55-loop-unrolling/14-unrolled-loop-dead-branch.c:4:9-4:15)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (tests/regression/55-loop-unrolling/14-unrolled-loop-dead-branch.c:3:17-3:24)

which is just plain confusing both sides of both conditions are live.
The branches are only dead in the internal unrolling of the loop and that's the point of loop unrolling.
It's strange that activating loop unrolling would previously generate more warnings.

[Copilot]

Pull request overview

This PR addresses confusing, duplicate, and even conflicting dead-branch warnings that occurred when loop unrolling was enabled, by attributing dead-branch tracking to the original (pre-unrolling) CFG node rather than to each unrolled copy.

Changes:

• Add a regression test ensuring loop unrolling no longer triggers spurious dead-branch warnings.
• In the dead-branch lifter, normalize prev_node to the original statement node using LoopUnrolling.find_original, aggregating unrolled copies under the same reporting key.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
tests/regression/55-loop-unrolling/14-unrolled-loop-dead-branch.c	New regression test expecting no dead-branch warnings under loop unrolling.
src/lifters/specLifters.ml	Record dead-branch info under the original statement node to avoid duplicate/conflicting warnings from unrolled copies.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[michael-schwarz]

Does this also fix the behavior for asserts that are in the unrolled loop?
I remember seeing things such as is unknown, will succeed for the same assert. (which btw also happens with path sensitivity)

[sim642]

No, this is specific to the dead branch lifting which maintains its own global unknowns to aggregate over paths, contexts and now unrollings.

When it comes to asserts (and pretty much all other messages), this makes no difference because it's all very text-based. Doing the same global unknowns aggregation for everything else would be quite messy.
This is actually something the dashboard checks system should solve because it's more semantic than just textual. Currently the checks kind of duplicate the messages where they are supported but eventually I'd like to use the checks (aggregated) to produce the messages. That would provide a very general mechanism to fix these conflicting messages and could even replace the special logic in the dead branch lifter.