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

Counterexample Failure #141

Closed
DavePearce opened this Issue Mar 27, 2018 · 5 comments

Comments

Projects
None yet
1 participant
@DavePearce
Member

DavePearce commented Mar 27, 2018

##The following illustrates some kind of failure in counter-example generation:

type nat is (int x) where x >= 0

function f() -> (int r)
ensures r < -1:
    //
    nat i = 0
    //
    return 0

The problem is that, when counter example generation is activated, it fails to report a compile-time error. Running from the command-line is helpful:

./test.whiley:8: postcondition not satisfied
    return 0
    ^^^^^^^^
Exception in thread "main" java.lang.NullPointerException
        at wyal.util.WyalFileResolver.getWyalFile(Unknown Source)
        at wyal.util.WyalFileResolver.nonLocalNameLookup(Unknown Source)
        at wyal.util.WyalFileResolver.resolve(Unknown Source)
        ...
        at wyal.util.Interpreter.evaluateInvoke(Unknown Source)
        ...
        at wyc.command.Compile.findCounterexamples(Compile.java:445)

An exception is arising and this is likely the culprit. But, it's not clear why!

@DavePearce

This comment has been minimized.

Member

DavePearce commented Mar 27, 2018

UPDATE: one interesting thing is that changing nat i = 0 to int i = 0 and it works out fine. Based on that, here's another example which is failing in the same way:

function f() -> (int r)
ensures r < -1:
    //
    int i = 0
    //
    return f()+1

It seems like any kind of resolution from within the interpreter during counterexample generation is doomed.

@DavePearce

This comment has been minimized.

Member

DavePearce commented Mar 27, 2018

The minimal WyAL which causes the problem is this:

type nat is (int x)
where:
    x >= 0


assert:
    forall(nat i):
        if:
            i == 0
        then:
            i < -1

DavePearce added a commit that referenced this issue Mar 27, 2018

Bug fix for #141.
The problem was that a type invariant was being extracted from a
parameter type, but this wasn't rooted in the enclosing heap.  Hence,
when resolution required access to the enclosing heap there was a
problem.
@DavePearce

This comment has been minimized.

Member

DavePearce commented Mar 28, 2018

Have fixed case for constrained types, but not function invocations. The latter is more complex because we need to examine the return type. Furthermore, we ideally need to record what decision we made here.

@DavePearce

This comment has been minimized.

Member

DavePearce commented Mar 28, 2018

This test case is also failing for reasons unknown:

type nat is (int x) where x >= 0

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

Looks like the problem is another exception raised here:

Exception in thread "main" java.lang.NullPointerException
        at wybs.util.AbstractSyntacticHeap.internalAllocate(Unknown Source)
        at wybs.util.AbstractSyntacticHeap.allocate(Unknown Source)
@DavePearce

This comment has been minimized.

Member

DavePearce commented Mar 28, 2018

Am closing this now, as remaining issues are "features" to be implemented.

@DavePearce DavePearce closed this Mar 28, 2018

DavePearce added a commit that referenced this issue Mar 29, 2018

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