Skip to content
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.

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

Jumps from outside of the loop into loop body will fail the loop contracts #7517

Closed
qinheping opened this issue Feb 3, 2023 · 2 comments · Fixed by #7541
Closed

Jumps from outside of the loop into loop body will fail the loop contracts #7517

qinheping opened this issue Feb 3, 2023 · 2 comments · Fixed by #7541
Assignees
Labels
aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts

Comments

@qinheping
Copy link
Collaborator

Currently, to apply loop contracts, we instrument

... preamble ...
... eval guard ...
if (!guard)
  goto EXIT;
... loop body ...
goto HEAD;
EXIT:
... postamble ...

to

... preamble ...
PREHEAD: 
    skip;
    /// loop begin
    loop_entry_vars = ...;
    entered_loop = false;
    I_base = <I>;
    in_base_case = true;
    goto HEAD;
STEP:
    assert(I_base);
    in_base_case = false;
    in_loop_havoc_block = true;
    loop_i_havoc_write_set(&w_loop_i);
    in_loop_havoc_block = false;
    assume (invariant_expr);
    D_before = <D>;
HEAD:
    ... eval guard ... // instrument against w_loop_i
    if(!guard)
        GOTO EXIT;
    ... body ...       // instrument against w_loop_i
    entered_loop = true;
    if(in_base_case)
        goto STEP;
    assert(I);
    D_after = <D>;
    assert(D_after < D_before);
    DEAD D_after, D_before;
    assume(false);
EXIT:
    // did we actually do the step
    assert(entered_loop ==> !in_base_case);
    DEAD w_loop_i

... postamble ...

The havocing, all initialization of temporary variables, the snapshotting of the loop invariants all happends in the PREHEAD block or the STEP block. If there are some jumps from out side of the loop into the loop body, they will skip the PREHEAD block and the STEP block; and hence fail the loop contracts.

For example, after the instrumentation, the jump GOTO 2 in the following GOTO program will skip the PREHEAD and the STEP of the loop.

    GOTO 2;
... preamble ...
1:  IF x == 0 THEN GOTO 3;
2:  ASSIGN x := x - 1;
    GOTO 1;
3:
... postamble ...

After instrumentation

    GOTO 2;
... preamble ...

PREHEAD: 
... pre-head block ...
STEP:
... step block ...
HEAD:
1:  IF x == 0 THEN GOTO EXIT;
2:  ASSIGN x := x - 1;
    assert(loop_invariants);
... remaining part of the head block ...
    assume(false);
EXIT:
    ASSERT(entered_loop ==> !in_base_case);

... postamble ...

So, we should apply loop contracts only when there is no jumps from outside into the body of the loop, and error out otherwise.

@qinheping qinheping added the Code Contracts Function and loop contracts label Feb 3, 2023
@qinheping qinheping self-assigned this Feb 3, 2023
@NlightNFotis
Copy link
Contributor

@thomasspriggs is this related to the work you're doing for #7506 or is this unrelated?

@thomasspriggs
Copy link
Collaborator

It is related, in that it might make this ticket easier to resolve. However it seems this is specifically an issue with how the code contracts work is manipulating the goto-program rather than an issue with the rest of the codebase.

@feliperodri feliperodri added the aws Bugs or features of importance to AWS CBMC users label Feb 6, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants