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

Verification of Type Invariants #751

Closed
DavePearce opened this Issue May 29, 2017 · 1 comment

Comments

Projects
None yet
1 participant
@DavePearce
Member

DavePearce commented May 29, 2017

Verification is, of course, currently a bottleneck in overall compiler performance. One simple improvement would be to reduce the number of verification conditions generated. Currently, verification conditions are generated for checking type invariants even when they are not required. For example, for this Whiley program:

function f(int x) -> (int r):
    //
    x = x + 1
    return x

The following verification conditions are generated:

assert "type invariant not satisfied":
    forall(int x):
        if:
            true
        then:
            (x + 1) is int


assert "type invariant not satisfied":
    forall(int x, int x$1):
        if:
            x$1 == (x + 1)
        then:
            x$1 is int

One is for the assignment, and one for the return. Clearly, this is wasteful...

@DavePearce DavePearce added the Feature label May 29, 2017

@DavePearce

This comment has been minimized.

Show comment
Hide comment
@DavePearce

DavePearce May 29, 2017

Member

UPDATE A partial implementation of this reduces overall time to verify all verification tests from 56s to 42s.

Member

DavePearce commented May 29, 2017

UPDATE A partial implementation of this reduces overall time to verify all verification tests from 56s to 42s.

@DavePearce DavePearce closed this May 29, 2017

DavePearce added a commit that referenced this issue May 29, 2017

Implemented #751.
This provides a partial implementation for issue 751 which covers the
vast majority of cases.  This does improve overall verification
performance.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment