[Coverage] Support Branch Coverage #2056

ChenfengWei0 · 2024-10-07T00:01:49Z

Strategy

We follow the strategy as CBMC. That is, we not only count the entry of branches, but also count the entry of functions.

e.g.

int main()
{
    int f = 2;
    if(f==2)
        f =1;
    f = 3;
}

ESBMC Output

>

#--branch-coverage-claims --unwind 2 --no-unwinding-assertions
[Coverage]

Function Entry Points & Branches : 3
Reached : 2
  0     file 1.c line 6 column 5 function main
  !(f == 2)     file 1.c line 7 column 5 function main
Branch Coverage: 66.66666666666667%

CBMC Output

>

#--cover branch --timestamp wall --unwind 3
** coverage results:
2024-10-07T00:58:30.565926 [main.coverage.1] file 1.c line 6 function main entry point: SATISFIED
[main.coverage.2] file 1.c line 7 function main block 1 branch false: SATISFIED
[main.coverage.3] file 1.c line 7 function main block 1 branch true: FAILED

2024-10-07T00:58:30.565950 ** 2 of 3 covered (66.7%)
2024-10-07T00:58:30.565956 ** Used 2 iterations

I am not sure if this is the "Branch Coverage" expected by Testcomp, as the typical branch coverage seems to only count the entry of branches

Known Issue

Currently cannot use this with k-induction or incremental-bmc. It seems in kind/incr, the goto_functions used during the BMC is simplified and incomplete

goto functions in unwind mode

>

        // 20 file 1.c line 6 column 5 function main
        ASSERT 0 // 0
        // 21 file 1.c line 6 column 5 function main
        DECL signed int f;
        // 22 file 1.c line 6 column 5 function main
        ASSIGN f=2;
        // 23 file 1.c line 7 column 5 function main
        ASSERT !(f == 2) // !(f == 2)
        // 24 file 1.c line 7 column 5 function main
        ASSERT !(!(f == 2)) // !(!(f == 2))
        // 25 file 1.c line 7 column 5 function main
        IF !(f == 2) THEN GOTO 1
        // 26 file 1.c line 8 column 9 function main
        ASSIGN f=1;
        // 27 file 1.c line 10 column 5 function main
     1: ASSIGN f=3;
        // 28 file 1.c line 11 column 1 function main
        DEAD c:1.c@39@F@main@f
        // 29 file 1.c line 11 column 1 function main
        RETURN: NONDET(signed int)
        // 30 file 1.c line 11 column 1 function main
        END_FUNCTION // main

goto functions in kind mode

>

        // 20 file 1.c line 6 column 5 function main
        SKIP
        // 21 file 1.c line 6 column 5 function main
        DECL signed int f;
        // 22 file 1.c line 6 column 5 function main
        ASSIGN f=2;
        // 23 file 1.c line 7 column 5 function main
        SKIP
        // 24 file 1.c line 7 column 5 function main
        ASSERT !(!(f == 2)) // !(!(f == 2))
        // 25 file 1.c line 7 column 5 function main
        IF !(f == 2) THEN GOTO 1
        // 26 file 1.c line 8 column 9 function main
        ASSIGN f=1;
        // 27 file 1.c line 10 column 5 function main
     1: ASSIGN f=3;
        // 28 file 1.c line 11 column 1 function main
        DEAD c:1.c@39@F@main@f
        // 29 file 1.c line 11 column 1 function main
        RETURN: NONDET(signed int)
        // 30 file 1.c line 11 column 1 function main
        END_FUNCTION // main

Would anyone happen to know how to disable this simplification feature

src/esbmc/bmc.cpp

src/goto-programs/goto_coverage.cpp

lucasccordeiro · 2024-10-07T11:45:56Z

src/goto-programs/goto_coverage.cpp

@@ -47,32 +58,77 @@ void goto_coveraget::replace_assert_to_guard(
  it->location.user_provided(true);
 }

-void goto_coveraget::add_false_asserts()
+/*
+Branch coverage applies to any control structure that can alter the flow of execution, including:


Clarifications:

How do we handle `try-catch' here?

What would be the difference between branch coverage and statement coverage?

Should our branch coverage also consider conditional expressions in control structures, ensuring all possible outcomes are tested?

I tried supporting 'try-catch' today. The difficulty is that, during the goto conversion, esbmc may add some auxiliary if-goto inside the try-catch body, thereby affecting the counting of the branches. No solution so far.

Branch Coverage = Decision Coverage: Measures whether each possible branch (decision) in the code has been executed. Statement Coverage: check if every line of code is executed at least once

In C, they all converted to if-goto, including if, else if, while, do-while, for, switch-case

mikhailramalho · 2024-10-07T13:40:14Z

What do you mean by incomplete?

ChenfengWei0 · 2024-10-07T15:44:18Z

What do you mean by incomplete?

The goto program is simplified, so the count of the total instrumentation is incomplete. E.g.

        // 20 file 1.c line 6 column 5 function main
        SKIP
        // 21 file 1.c line 6 column 5 function main
        DECL signed int f;
        // 22 file 1.c line 6 column 5 function main
        ASSIGN f=2;
        // 23 file 1.c line 7 column 5 function main
        SKIP
        // 24 file 1.c line 7 column 5 function main
        ASSERT !(!(f == 2)) // !(!(f == 2))

Has been simplified to

        // 20 file 1.c line 6 column 5 function main
        ASSERT 0 // 0
        // 21 file 1.c line 6 column 5 function main
        DECL signed int f;
        // 22 file 1.c line 6 column 5 function main
        ASSIGN f=2;
        // 23 file 1.c line 7 column 5 function main
        ASSERT !(f == 2) // !(f == 2)
        // 24 file 1.c line 7 column 5 function main
        ASSERT !(!(f == 2)) // !(!(f == 2))

in kind/incr. The unwind looks fine.

mikhailramalho · 2024-10-07T15:54:03Z

I think you mean the assertions were simplified to skips, not the other way around, right?

ChenfengWei0 · 2024-10-07T16:01:41Z

I think you mean the assertions were simplified to skips, not the other way around, right?

Yes

ChenfengWei0 · 2024-10-08T01:17:12Z

Update: temporarily fix the kind/incr issues by using static member

src/goto-programs/goto_coverage.cpp

lucasccordeiro

@ChenfengWei0: please consider addressing Rafael's suggestion.

lucasccordeiro

@ChenfengWei0: please consider addressing Rafael's suggestion.

lucasccordeiro · 2024-10-09T06:47:06Z

Thanks for submitting this PR, @ChenfengWei0.

lucasccordeiro requested changes Oct 7, 2024

View reviewed changes

ChenfengWei0 force-pushed the branch_cov branch from 9e0ab9d to b15d6b3 Compare October 8, 2024 02:39

rafaelsamenezes requested changes Oct 8, 2024

View reviewed changes

src/goto-programs/goto_coverage.cpp Outdated Show resolved Hide resolved

lucasccordeiro approved these changes Oct 8, 2024

View reviewed changes

ChenfengWei0 force-pushed the branch_cov branch from 2d90261 to f8c4808 Compare October 8, 2024 15:36

ChenfengWei1 and others added 12 commits October 8, 2024 18:56

[coverage] support branch coverage

2f2fbcc

[coverage] regression for branch cov

0348fc6

[coverage] add documentation

cc0a5b3

Apply automatic changes

ffe253d

[coverage] fix assert cov

7d400dd

[coverage] refactoring

03d11a9

[coverage] add regression

7ed970c

[coverage] fix regression

02ae27f

Apply automatic changes

19b6b84

[coverage] change to insert_swap

fc62b9d

[coverage] bug fix

24c9773

[coverage] fix regressions

e97fa88

ChenfengWei0 force-pushed the branch_cov branch from a246b3d to e97fa88 Compare October 8, 2024 20:52

lucasccordeiro merged commit a4f82bb into master Oct 9, 2024
13 checks passed

lucasccordeiro deleted the branch_cov branch October 9, 2024 06:46

ChenfengWei0 restored the branch_cov branch October 10, 2024 15:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Coverage] Support Branch Coverage #2056

[Coverage] Support Branch Coverage #2056

ChenfengWei0 commented Oct 7, 2024 •

edited

Loading

lucasccordeiro Oct 7, 2024

ChenfengWei0 Oct 8, 2024

mikhailramalho commented Oct 7, 2024

ChenfengWei0 commented Oct 7, 2024

mikhailramalho commented Oct 7, 2024

ChenfengWei0 commented Oct 7, 2024

ChenfengWei0 commented Oct 8, 2024 •

edited

Loading

lucasccordeiro left a comment

lucasccordeiro left a comment

lucasccordeiro commented Oct 9, 2024

[Coverage] Support Branch Coverage #2056

[Coverage] Support Branch Coverage #2056

Conversation

ChenfengWei0 commented Oct 7, 2024 • edited Loading

Strategy

Known Issue

lucasccordeiro Oct 7, 2024

Choose a reason for hiding this comment

ChenfengWei0 Oct 8, 2024

Choose a reason for hiding this comment

mikhailramalho commented Oct 7, 2024

ChenfengWei0 commented Oct 7, 2024

mikhailramalho commented Oct 7, 2024

ChenfengWei0 commented Oct 7, 2024

ChenfengWei0 commented Oct 8, 2024 • edited Loading

lucasccordeiro left a comment

Choose a reason for hiding this comment

lucasccordeiro left a comment

Choose a reason for hiding this comment

lucasccordeiro commented Oct 9, 2024

ChenfengWei0 commented Oct 7, 2024 •

edited

Loading

ChenfengWei0 commented Oct 8, 2024 •

edited

Loading