CrossHair

CrossHair copied to clipboard

(This is a split from the issue #58 where we started discussing what happens with the side effects.)

@pschanely could you describe the current behavior? The symbolic values are passed into the function. What happens if a function has side effects in the body? Both the contracts and the body will be executed on the symbolic values, correct? (Maybe you can also describe the monkey patching and why it is necessary?)

(I know we discussed this already off-line, but maybe I missed a couple of important bits.)

I'd like to challenge my understanding, assemble all the puzzle pieces, and finally try to put it into the docs afterwards.

This is vaguely relevant.

CrossHair calls your function, your real function, repeatedly. Each iteration explores one path through your code. It supplies to your function values that look like real ones, but aren't - they are kinda like "quantum" values which doesn't become real until you observe properties about them. When CrossHair gets to something that needs a real value (like an "if" statement), it'll "realize" that symbolic into a concrete value. It has multiple strategies for doing this, one of which is monkey patching various parts of the standard library.

CrossHair remembers which paths it took previously, and realizes symbolic booleans differently to make the code explore different paths. Under the hood, the SMT solver ensures that CrossHair never makes a decision that is inconsistent with the decisions that it's previously made in that path.

Eh, I think that's the cliff notes :)

Thanks! Following your gist notes, would crosshair make sure that the realized value satisfies the pre-conditions?

Eh, today that's often the case, but not guaranteed. I think we could make it guaranteed, at the cost of some potential effectiveness.

This is where short-circuiting comes in, which I never explained.

The effectiveness of the system is sometimes improved by deferring some work: to do this, we'll sometimes skip over a function call and run it later in hopes that we can make the result match up. The intuition here is that different pieces of code will result in different amounts of realization and the process as a whole works best if we can get to through the low-realization work earlier.

At any rate, if your precondition calls other functions with contracts, we might not run those, and the body of your function would continue with symbolics that could have states that aren't really possible. CrossHair will later narrow the state space again so that it gives you correct results, but technically we could run the body in states that aren't permitted by the preconditions.

As I mentioned above, it might make sense to fully forbid short-circuiting for preconditions (opinions welcome), but that's not the case right now.

(I'll need another pass over the text, so please apologise if I still don't get all the details.)

Just for the sake of the clarification, let me phantasize a strawman. Asdume we are testing the following function:

def some_func(p: pathlib.Path) -> None:
    assert p != pathlib.Path()
    ...

(Let's abstract at the moment that the precondition is written as an assert as it applies equally to icontract or PEP 316 in case we enforced it somehow.)

Let's say we have a shutil.rmtree(p) in the body somewhere. While this would be benign in an unit test or property-based test, as the precondition is enforced (and plausible values for p selected, e.g., a temporary directory), this would mean that the current directory would be deleted when crosshair analyzes the function (assuming that the preconditions are ignored and the realization is the empty path), wouldn't it?

No worries!

In this particular example, we aren't making another function call in the precondition, so I don't think bad things would happen. But it's be easy to invent situations where it would do a removal like the one you describe - just put that check inside another function with a contract. So, still quite dangerous. And beyond anything I say here, of course, CrossHair still has plenty of bugs.

At this point in time, you really don't want to let this thing near side effects at all.

Also, I've been collecting ideas on safety here.

(This is related to #51.)

@pschanely maybe you might want to add the text of your comments in the documentation, even in the current stage, as I found them very informative?

Yup! Just added. It's a start.