CONTRACTS: redirect checks to outer write set for loops that get skipped

[remi-delmas-3000]

Skipping the instrumentation of loops that don't have invariant and decrease clauses caused dangling references to non-existent write set variables to be inserted in the program.

We now redirect these references to the write set of the first outer loop that is not skipped, or to the top level write set.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[remi-delmas-3000]

Strange failure on this test:

void main()
{
  int i = 0;
  int j = 0;

HEAD:
  if(i > 5)
    goto EXIT1;
  i++;
  goto HEAD; // first latch
EXIT1:;
  if(j > 5)
    goto EXIT2;
  j++;
  goto HEAD; // second latch
EXIT2:;
}

This program should be rejected because it contains a loop with two latch nodes, and we don't know how to instrument them. However our detection now fails.

Coming straight out of goto-cc instruction 8 is GOTO 1

main /* main */
        // 0 file main.c line 5 function main
        DECL main::1::i : signedbv[32]
        // 1 file main.c line 5 function main
        ASSIGN main::1::i := 0
        // 2 file main.c line 6 function main
        DECL main::1::j : signedbv[32]
        // 3 file main.c line 6 function main
        ASSIGN main::1::j := 0
        // 4 file main.c line 9 function main
        // Labels: HEAD
     1: IF main::1::i > 5 THEN GOTO 2
        // 5 file main.c line 10 function main
        SKIP
        // 6 file main.c line 10 function main
        SKIP
        // 7 file main.c line 11 function main
        ASSIGN main::1::i := main::1::i + 1
        // 8 file main.c line 12 function main
        GOTO 1
        // 9 file main.c line 13 function main
        // Labels: EXIT1
     2: SKIP
        // 10 file main.c line 14 function main
        IF main::1::j > 5 THEN GOTO 3
        // 11 file main.c line 15 function main
        SKIP
        // 12 file main.c line 15 function main
        SKIP
        // 13 file main.c line 16 function main
        ASSIGN main::1::j := main::1::j + 1
        // 14 file main.c line 17 function main
        GOTO 1
        // 15 file main.c line 18 function main
        // Labels: EXIT2
     3: SKIP
        // 16 file main.c line 19 function main
        DEAD main::1::j
        // 17 file main.c line 19 function main
        DEAD main::1::i
        // 18 file main.c line 19 function main
        END_FUNCTION

Right after being reloaded by goto-instrument instruction 8 is GOTO 3 instead of GOTO 1, so we don't have a loop with two latches anymore:

main /* main */
        // 0 file main.c line 5 function main
        DECL main::1::i : signedbv[32]
        // 1 file main.c line 5 function main
        ASSIGN main::1::i := 0
        // 2 file main.c line 6 function main
        DECL main::1::j : signedbv[32]
        // 3 file main.c line 6 function main
        ASSIGN main::1::j := 0
        // 4 file main.c line 9 function main
        // Labels: HEAD
     1: IF main::1::i > 5 THEN GOTO 2
        // 5 file main.c line 10 function main
        SKIP
        // 6 file main.c line 10 function main
        SKIP
        // 7 file main.c line 11 function main
        ASSIGN main::1::i := main::1::i + 1
        // 8 file main.c line 12 function main
        GOTO 3
        // 9 file main.c line 13 function main
        // Labels: EXIT1
     2: SKIP
        // 10 file main.c line 14 function main
        IF main::1::j > 5 THEN GOTO 4
        // 11 file main.c line 15 function main
        SKIP
        // 12 file main.c line 15 function main
        SKIP
        // 13 file main.c line 16 function main
        ASSIGN main::1::j := main::1::j + 1
        // 14 file main.c line 17 function main
     3: GOTO 1
        // 15 file main.c line 18 function main
        // Labels: EXIT2
     4: SKIP
        // 16 file main.c line 19 function main
        DEAD main::1::j
        // 17 file main.c line 19 function main
        DEAD main::1::i
        // 18 file main.c line 19 function main
        END_FUNCTION

@tautschnig any idea of when this GOTO redirection may be happening ?

[remi-delmas-3000]

@tautschnig I think it comes from this added 7 months ago

cbmc/src/goto-instrument/goto_instrument_parse_options.cpp

Line 1203 in b87d38a

ensure_one_backedge_per_target(goto_model);

added here : https://github.com/diffblue/cbmc/pull/8095/files#diff-e0684705f9b9bbef7ee7eb83d9753f74deb51281a40d4fab122fccf48eb99c1a

I'm surprised this test did not break back then ?

Can you think of an example where the ensure_one_backedge_per_target will not normalize the loop ?

I suggest disabling the failing test for now.

[tautschnig]

@tautschnig any idea of when this GOTO redirection may be happening ?

I'll investigate. I have just debugged another situation where loop normalization causes incorrect goto programs, fix coming.

[codecov]

Codecov Report

Attention: Patch coverage is 91.66667% with 1 line in your changes missing coverage. Please review.

Project coverage is 77.85%. Comparing base (2bef701) to head (48aa648).
Report is 3 commits behind head on develop.

Files	Patch %	Lines
...trument/contracts/dynamic-frames/dfcc_cfg_info.cpp	88.88%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8416      +/-   ##
===========================================
- Coverage    77.88%   77.85%   -0.03%     
===========================================
  Files         1726     1726              
  Lines       189804   189886      +82     
  Branches     18234    18223      -11     
===========================================
+ Hits        147826   147835       +9     
- Misses       41978    42051      +73     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[tautschnig]

regression/contracts-dfcc/loop_contracts_do_while/nested.desc now no longer is KNOWNBUG but instead will pass.