[BUG] CN can't process do-while loops

[peterohanley]

Summary

CN appears to parse the loop successfully but then fails at a later stage, perhaps in core.

Bug

void f(void)
{
    int x = 0;
    do {x = 1;} while(x == 2);
}

% cn dowhile.c 
dowhile.c:4:5: error: undefined code label
continue_493
    do {x = 1;} while(x == 2);
    ^~~~~~~~~~~~~~~~~~~~~~~~~~ 

Acceptance Criteria

Either confirmation that it is intended behavior or implement this construct in the AST transform to core, or wherever else it should be..

Do

• assign issue to a Milestone
• define acceptance criteria
• add appropriate labels
• Fix appropriate part of CN, perhaps control flow of core?

[cp526]

This is fixed by dbadf3e . The syntax for do-while annotations in CN is as below.

void f(void)
{
    int x = 1;
    do 
    /*@ inv x == 1i32; @*/ 
    {
      x = 0;
    } 
    while(x == 1);
}

This is slightly clunky, but having the inv before the loop body makes clear where the invariant has to hold: each time the loop body is entered (whether for the first time, or when re-entering when the loop condition succeeds).

(Putting inv before the do, while cleaner-looking makes the parser grammar ambiguous.)

This is hardly tested so far. In particular, it's not clear yet whether requiring the invariant to hold on each loop entry is what we want for do-while, or whether we'd prefer loop invariants that don't have to hold on the first loop iteration but only when the loop is re-entered. (Closing for now, please re-open if needed.)

[bcpierce00]

Why not put it before the while and not require that it hold on entry?

…

On Fri, Jun 21, 2024 at 5:53 AM Christopher Pulte ***@***.***> wrote: This is fixed by dbadf3e . The syntax for do-while annotations in CN is as below. void f(void) { int x = 1; do /*@ inv x == 1i32; @*/ { x = 0; } while(x == 1); } This is slightly clunky, but having the inv before the loop body makes clear where the invariant has to hold: each time the loop body is entered (whether for the first time, or when re-entering when the loop condition succeeds). (Putting inv before the do, while cleaner-looking makes the parser grammar ambiguous.) This is hardly tested so far. In particular, it's not clear yet whether requiring the invariant to hold on each loop entry is what we want for do-while, or whether we'd prefer loop invariants that don't have to hold on the first loop iteration but only when the loop is *re*-entered. (Closing for now, please re-open if needed.) — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/GaloisInc/VERSE-Toolchain/issues/100*issuecomment-2182418958__;Iw!!IBzWLUs!Rl5te1eREQ3pxAbFh9_lRCS4mGl4EUxML_DG72XFo2sPKaTRjZZOxV970NEHtzJqWXh3PRMwL7hbq25hirj1ew_3lG6_$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC7OJCVK2ET3SE5Y7D3ZIPZ3HAVCNFSM6AAAAABJQPP5SCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCOBSGQYTQOJVHA__;!!IBzWLUs!Rl5te1eREQ3pxAbFh9_lRCS4mGl4EUxML_DG72XFo2sPKaTRjZZOxV970NEHtzJqWXh3PRMwL7hbq25hirj1exe8W1Bj$> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[cp526]

That's also possible. Is that what one wants for proofs about do-while?

[bcpierce00]

I think so

…

On Fri, Jun 21, 2024 at 10:56 AM Christopher Pulte ***@***.***> wrote: That's also possible. Is that what one wants for proofs about do-while? — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/GaloisInc/VERSE-Toolchain/issues/100*issuecomment-2182913698__;Iw!!IBzWLUs!U5to4JyRTs5IbM_3_A9yuW2dIKhCyQBuU0s0hFNmN0-DSDcuPunZ7mb99de4bmkSpEwwI3iS4eT0RLkx99kEq_iCwRem$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC5DRGDF4E7CTM66DYDZIQ5LRAVCNFSM6AAAAABJQPP5SCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCOBSHEYTGNRZHA__;!!IBzWLUs!U5to4JyRTs5IbM_3_A9yuW2dIKhCyQBuU0s0hFNmN0-DSDcuPunZ7mb99de4bmkSpEwwI3iS4eT0RLkx99kEq70U3nGm$> . You are receiving this because you commented.Message ID: ***@***.***>