Skip to content

Fix duplicate conflicting dead branch warnings due to loop unrolling #1960

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sim642 merged 2 commits into from
Mar 31, 2026
+17 −23
Merged

Fix duplicate conflicting dead branch warnings due to loop unrolling #1960

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
75986c5
Add test 55-loop-unrolling/14-unrolled-loop-dead-branch
sim642 Mar 12, 2026
faa85ec
Fix duplicate conflicting dead branch warnings due to loop unrolling
sim642 Mar 12, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 8 additions & 3 deletions src/lifters/specLifters.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -870,19 +870,24 @@ struct
let context man = S.context (conv man)

let branch man exp tv =
let prev_node =
match man.prev_node with
| Statement s -> Node.Statement (LoopUnrolling.find_original s) (* aggregate all unrolled copies under original to avoid conflicting warnings about same source branch *)
| n -> n (* never unrolled *)
in
if !AnalysisState.postsolving then (
try
let r = branch man exp tv in
(* branch is live *)
man.sideg (V.node man.prev_node) (G.create_node (EM.singleton exp (`Lifted tv))); (* record expression with reached tv *)
man.sideg (V.node prev_node) (G.create_node (EM.singleton exp (`Lifted tv))); (* record expression with reached tv *)
r
with Deadcode ->
(* branch is dead *)
man.sideg (V.node man.prev_node) (G.create_node (EM.singleton exp `Bot)); (* record expression without reached tv *)
man.sideg (V.node prev_node) (G.create_node (EM.singleton exp `Bot)); (* record expression without reached tv *)
raise Deadcode
)
else (
man.sideg (V.node man.prev_node) (G.create_node (EM.bot ())); (* create global variable during solving, to allow postsolving leq hack to pass verify *)
man.sideg (V.node prev_node) (G.create_node (EM.bot ())); (* create global variable during solving, to allow postsolving leq hack to pass verify *)
branch man exp tv
)

Expand Down
20 changes: 0 additions & 20 deletions tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -198,26 +198,6 @@
live: 10
dead: 0
total lines: 10
[Warning][Deadcode][CWE-570] condition 'k < 100' (possibly inserted by CIL) is always false (11-unrolled-loop-invariant.c:9:12-9:19)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:10-8:16)
[Warning][Deadcode][CWE-570] condition 'k < 100' (possibly inserted by CIL) is always false (11-unrolled-loop-invariant.c:9:12-9:19)
[Warning][Deadcode][CWE-570] condition 'k < 100' (possibly inserted by CIL) is always false (11-unrolled-loop-invariant.c:9:12-9:19)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:10-8:16)
[Warning][Deadcode][CWE-570] condition 'k < 100' (possibly inserted by CIL) is always false (11-unrolled-loop-invariant.c:9:12-9:19)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:4:10-4:16)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:4:10-4:16)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:4:10-4:16)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:4:10-4:16)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:4:10-4:16)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:10-8:16)
[Warning][Deadcode][CWE-570] condition 'k < 100' (possibly inserted by CIL) is always false (11-unrolled-loop-invariant.c:9:12-9:19)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:10-8:16)
[Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:9:12-9:19)
[Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:9:12-9:19)
[Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:9:12-9:19)
[Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:9:12-9:19)
[Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:9:12-9:19)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:10-8:16)
[Info][Witness] witness generation summary:
location invariants: 11
loop invariants: 5
Expand Down
9 changes: 9 additions & 0 deletions tests/regression/55-loop-unrolling/14-unrolled-loop-dead-branch.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
// PARAM: --enable ana.dead-code.branches --set exp.unrolling-factor 2
int main() {
for (int i = 0; i < 2; i++) { // NOWARN (dead branch)
if (i == 1) { // NOWARN (dead branch)

}
}
return 0;
}
Loading