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

Failing Verification from WhileyCompiler #124

Closed
DavePearce opened this Issue Jun 2, 2017 · 2 comments

Comments

Projects
None yet
1 participant
@DavePearce
Member

DavePearce commented Jun 2, 2017

The following fails verification when compiled via WyC:

function reverse(int[] ls) -> int[]:
    int i = |ls|
    int[] r = [0; |ls|]
    while i > 0 where i <= |ls| && |r| == |ls|:
        int item = ls[|ls|-i]
        i = i - 1
        r[i] = item
    return r

However, the generated verification conditions are easily dispatched using wy verify. The failing proof is:

 482. exists(int i, int[] ls).((((i == |ls|)) && ((0 >= (|ls| + 1)))))       () 
 486. exists(int i, int[] ls).((i == |ls|) && (0 >= (1 + |ls|)))     (Simp 482) 
 485. (i == |ls|) && (0 >= (1 + |ls|))                           (Exists-E 486) 
 474. i == |ls|                                                     (And-E 485) 
 484. 0 >= (1 + |ls|)                                               (And-E 485) 
 488. 0 >= (1 + i)                                               (Eq-S 484,474) 
./While_Valid_1.whiley:5: negative length possible
    int[] r = [0; |ls|]
              ^^^^^^^^^

Whilst the passing version is:

 530. exists(int i, int[] ls).((((i == |ls|)) && ((0 >= (|ls| + 1)))))       () 
 534. exists(int i, int[] ls).((i == |ls|) && (0 >= (1 + |ls|)))     (Simp 530) 
 533. (i == |ls|) && (0 >= (1 + |ls|))                           (Exists-E 534) 
 532. 0 >= (1 + |ls|)                                               (And-E 533) 
 535. |ls| >= 0                                                  (ArrLen-I 532) 
 521. false                                                     (Ieq-I 535,532) 
@DavePearce

This comment has been minimized.

Member

DavePearce commented Jun 2, 2017

With nonces enabled we have:

 482. exists(int i'20, int[] ls'15).((((i'20 == |ls'15|)) && ((0 >= (|ls'15| () 
 486. exists(int i'20, int[] ls'15).((i'20 == |ls'15|) && (0 >= (1 + (Simp 482) 
 485. (i'20 == |ls'15|) && (0 >= (1 + |ls'15|))                  (Exists-E 486) 
 474. i'20 == |ls'15|                                               (And-E 485) 
 484. 0 >= (1 + |ls'15|)                                            (And-E 485) 
 488. 0 >= (1 + i'20)                                            (Eq-S 484,474)

versus

 530. exists(int i'42, int[] ls'46).((((i'42 == |ls'46|)) && ((0 >= (|ls'46| () 
 534. exists(int i'42, int[] ls'46).((i'42 == |ls'46|) && (0 >= (1 + (Simp 530) 
 533. (i'42 == |ls'46|) && (0 >= (1 + |ls'46|))                  (Exists-E 534) 
 532. 0 >= (1 + |ls'46|)                                            (And-E 533) 
 535. |ls'46| >= 0                                               (ArrLen-I 532) 
 521. false                                                     (Ieq-I 535,532)

Yes, in the first we have i'20 versus ls'15 whilst in the second we have i'42 versus ls'46. This looks like a variable ordering problem.

@DavePearce

This comment has been minimized.

Member

DavePearce commented Oct 9, 2017

Fixed following #136 and #138

@DavePearce DavePearce closed this Oct 9, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment