GOTO conversion of return inside if-then-else generates unreachable instructions

[remi-delmas-3000]

When a return statement terminates a block in an if-then-else, GOTO conversion emits :

1. a SET_RETURN_VALUE
2. a GOTO statement to encode the return
3. a GOTO statement to jump out of the if- or else-if block

As a result --cover location reports that the block containing the second GOTO statement is unreachable.

Since both GOTO statements have the same source location and there is nothing after the return statement, this makes it look like the return statement is both reachable and unreachable for a user looking at the C code.

Would it be possible to simplify away the second GOTO since it is purely an artifact of goto conversion and statically unreachable ?

int nondet_int();

int main() {
    if (nondet_int()) {
        return -1;
    } else if (nondet_int()) {
        return -1;
    } else if (nondet_int()) {
        return -1;
    }
    return 0;
}

Coverage results:

** coverage results:
[main.coverage.1] file double_goto.c line 4 function main block 1 (lines double_goto.c:main:4): SATISFIED
[main.coverage.2] file double_goto.c line 5 function main block 2 (lines double_goto.c:main:5): SATISFIED
[main.coverage.3] file double_goto.c line 5 function main block 3 (lines double_goto.c:main:5): FAILED
[main.coverage.4] file double_goto.c line 6 function main block 4 (lines double_goto.c:main:6): SATISFIED
[main.coverage.5] file double_goto.c line 7 function main block 5 (lines double_goto.c:main:7): SATISFIED
[main.coverage.6] file double_goto.c line 7 function main block 6 (lines double_goto.c:main:7): FAILED
[main.coverage.7] file double_goto.c line 8 function main block 7 (lines double_goto.c:main:8): SATISFIED
[main.coverage.8] file double_goto.c line 9 function main block 8 (lines double_goto.c:main:9): SATISFIED
[main.coverage.9] file double_goto.c line 11 function main block 9 (lines double_goto.c:main:11): SATISFIED
[main.coverage.10] file double_goto.c line 12 function main block 10 (lines double_goto.c:main:12): SATISFIED

** 8 of 10 covered (80.0%)
** Used 5 iterations

Goto functions :

main /* main */
        // 0 file double_goto.c line 4 function main
        DECL main::$tmp::return_value_nondet_int$1 : signedbv[32]
        // 1 file double_goto.c line 4 function main
        ASSIGN main::$tmp::return_value_nondet_int$1 := side_effect statement="nondet" #identifier="nondet_int" is_nondet_nullable="1"
        // 2 file double_goto.c line 4 function main
        IF ¬(main::$tmp::return_value_nondet_int$1 ≠ 0) THEN GOTO 1

/* reachable */

        // 3 file double_goto.c line 5 function main
        SET RETURN VALUE -1
        // 4 file double_goto.c line 5 function main
        GOTO 6

/* unreachable */
        // 5 file double_goto.c line 5 function main
        GOTO 5

        // 6 file double_goto.c line 6 function main
     1: DECL main::$tmp::return_value_nondet_int$0 : signedbv[32]
        // 7 file double_goto.c line 6 function main
        ASSIGN main::$tmp::return_value_nondet_int$0 := side_effect statement="nondet" #identifier="nondet_int" is_nondet_nullable="1"
        // 8 file double_goto.c line 6 function main
        IF ¬(main::$tmp::return_value_nondet_int$0 ≠ 0) THEN GOTO 2

/* reachable */
        // 9 file double_goto.c line 7 function main
        SET RETURN VALUE -1
        // 10 file double_goto.c line 7 function main
        GOTO 6

/* unreachable */
        // 11 file double_goto.c line 7 function main
        GOTO 4

        // 12 file double_goto.c line 8 function main
     2: DECL main::$tmp::return_value_nondet_int : signedbv[32]
        // 13 file double_goto.c line 8 function main
        ASSIGN main::$tmp::return_value_nondet_int := side_effect statement="nondet" #identifier="nondet_int" is_nondet_nullable="1"
        // 14 file double_goto.c line 8 function main
        IF ¬(main::$tmp::return_value_nondet_int ≠ 0) THEN GOTO 3
        // 15 file double_goto.c line 9 function main
        SET RETURN VALUE -1
        // 16 file double_goto.c line 9 function main
        GOTO 6
        // 17 no location
     3: SKIP
        // 18 no location
     4: SKIP
        // 19 no location
     5: SKIP
        // 20 file double_goto.c line 11 function main
        SET RETURN VALUE 0
        // 21 file double_goto.c line 11 function main
        DEAD main::$tmp::return_value_nondet_int$1
        // 22 file double_goto.c line 11 function main
        DEAD main::$tmp::return_value_nondet_int$0
        // 23 file double_goto.c line 11 function main
        DEAD main::$tmp::return_value_nondet_int
        // 24 file double_goto.c line 11 function main
        GOTO 6
        // 25 file double_goto.c line 12 function main
     6: END_FUNCTION

CBMC version: 5.94.0
Operating system: linux
Exact command line resulting in the issue: cbmc --cover locations main.c
What behaviour did you expect: all blocks reachable
What happened instead: some dead blocks are not reachable

[remi-delmas-3000]

Hi @thomasspriggs , I stumbled upon this while testing #7944. Is there anything that can be done for this case as well ?

[thomasspriggs]

Hi @thomasspriggs , I stumbled upon this while testing #7944. Is there anything that can be done for this case as well ?

Hi @remi-delmas-3000. Thank you for taking the time to do the testing.

I would say that the existing output is technically correct though unhelpful. This is because the end of the code block is not reachable due to the return statement, though it is unhelpful to point this out due to the lack of user code in this location. For comparison consider this variation on your example -

int nondet_int();

int main() {
    if (nondet_int()) {
        return -1;
        assert(2 + 2 == 5);
    } else if (nondet_int()) {
        return -1;
    } else if (nondet_int()) {
        return -1;
    }
    return 0;
}

With cbmc as it currently stands on develop, the only difference in the goto program will be the addition of a single assert instruction. A regular cbmc run will show - [main.assertion.1] line 6 assertion 2 + 2 == 5: SUCCESS. The number of coverage blocks and their outcomes will be as per your initial example. In this case the outcome of the coverage run would be helpful, as it shows that the assertion is unreachable. Therefore I would argue that optimising away unreachable code before coverage instrumentation or block definition could have unhelpful side-effects without careful consideration.

This leaves us with a couple of potential solutions -

1. Insert a special case in the goto_convert process on the conversion of if-then-else to goto which checks for whether the block of code from the "then" case already ends in an unconditional goto. If it does then the extra goto does not not need to be inserted.
2. Filter the blocks in the block definition process. We could check for blocks which are composed of zero or more skip instructions and end in an unconditional goto.

Option 1 should be fairly straight forward to implement. It would however leave the possibility of similar issues being found in future for other control flow constructions. Option 2 is the more robust solution in my view, as it should exclude other variations of the same issue with the minor draw back that other user-specified goto statements could also be excluded from coverage checks.

The other side-issue I see here is the granularity of reporting which we produce for the coverage output. We currently only list line numbers for each given block. More detailed output could help with making sense of what each individual block is referring to. That would however be more of a feature request than a bugfix.

[thomasspriggs]

I am unassigning myself from this for the moment. I consider this to be outside of the scope of the work which we are currently engaged in, but I will leave @TGWDB assigned, for future prioritisation.

[esteffin]

A PR with the fix for the current issue has been created at #8001