Exhaustive path exploration

[Gondolav]

Hi,

For our master thesis, me and my friend @samuelchassot are working on a platform for developing and running formally verified smart infrastructures. We would like to ask if it would be hard for us to fork CrossHair and modify it to do exhaustive path exploration (path explosion in our case is not a concern)?

Thanks a lot!

[pschanely]

Feel free! You may be interested in the --report_all option which will report when all paths have been covered. (some related discussion)

I'd be more than happy to chat with you about your goals and/or walk you through relevant parts of the codebase; sign up for CrossHair office hours, or reach out directly if those times slots don't work for you.

[samuelchassot]

Hi!
Thanks a lot for your reply!
We tried to use the --report-all flag but it does not seem to do what we want: from what we can see, it only changes the log level. We found a program that makes Crosshair outputs verified over all paths while it obviously miss some of them.
We would like to enforce that all paths are covered before outputting that the contracts holds. In other words, we would like to really verify that the contracts are valid.
Do you think it is feasible to modify Crosshair in that sense? We do not care about path explosion problems for our application.
We will try to find a time that works for us in the office hours availability.

Thanks a lot!
@Gondolav

[pschanely]

We found a program that makes Crosshair outputs verified over all paths while it obviously miss some of them.

I would be very curious to take a look at such an example; this might be a bug. Happy to talk in person too, but feel free to reply with that example right away if you are able to share it. https://crosshair-web.org/ can be handy for this sort of thing.

We would like to enforce that all paths are covered before outputting that the contracts holds. In other words, we would like to really verify that the contracts are valid. Do you think it is feasible to modify Crosshair in that sense?

Yes - this should be possible, particularly if you know that you are working on code with finite execution paths. One caveat - many of the internal implementations of functions and datatypes involve branching that is not present in the original code. For example, many string operations end up branching on the length of the string inside CrossHair.

We do not care about path explosion problems for our application. We will try to find a time that works for us in the office hours availability.

Looking forward to it!

[samuelchassot]

I would be very curious to take a look at such an example; this might be a bug. Happy to talk in person too, but feel free to reply with that example right away if you are able to share it. https://crosshair-web.org/ can be handy for this sort of thing.

Here is one example, that outputs /tmp/main.py:7: info: Confirmed over all paths. on https://crosshair-web.org/ :

import time

def main():
    '''
    pre:
    post: __return__ != 0
    '''
    x = int(time.time())
    if x % 235432 == 0:
        return 0
    else:
        return 1

(we know that the call to the external library is a bit tricky for Crosshair, but we want this type of things to be caught as clearly there it couldn't verify the program over all paths)

Yes - this should be possible, particularly if you know that you are working on code with finite execution paths. One caveat - many of the internal implementations of functions and datatypes involve branching that is not present in the original code. For example, many string operations end up branching on the length of the string inside CrossHair.

That's great news, we really look forward to meeting you to discuss about it!

@Gondolav

[pschanely]

For other folks who might stumble across this discussion:

One of CrossHair's bug limitations is that it expects the analyzed code to always behave the same when given the same inputs. time.time() breaks this expectation and CrossHair produces an inaccurate result in this case.

In situations where you have control over the source, you can work around this by "externalizing" the non-deterministic parts; e.g.:

def compute(tm: int):
    '''
    post: __return__ != 0
    '''
    x = int(tm)
    if x % 235432 == 0:
        return 0
    else:
        return 1

def main():
    return calculate(int(time.time()))