constraints on input in test case generation mode (cover)

[zhenkun]

def mylen(lst: list[int]) -> int:
    """
    pre: len(lst) < 3
    """
    assert len(lst) < 3
    return len(lst)

Using cover mode, crosshair generates lists that have more than 3 elements.
I am interested in generating input lists that have less than 3 elements, for example, how do I tell the tool to do so?
I tried preconditions and assertions at the beginning, but nothing works so far.

I appreciate any inputs.
-zk

[pschanely]

Preconditions and postconditions are only considered when checking contracts (crosshair check or crosshair watch), so they are ignored in your case.

OOC, are you just generally trying to find coverage inputs that are smaller than what you're getting? Crosshair cover doesn't really bias for small inputs right now, but I've just added a feature request for this.

Depending on what you're ultimately trying to do, you might also be interested in the not-yet-documented search command; e.g. crosshair search --optimization=minimize_int attempts to find inputs that minimize the return value of the function.

[zhenkun]

Thank you @pschanely for your explanation.That makes sense.
In general, what I want to do is to reduce the search space in real world applications, where the number of paths is exponential to the inputs. Kind of like what klee_assume() does in KLEE.
Another example could be: given functiondef f(x: int, y: int) -> int, the user is only interested in test cases in which x > y by specifying that as a precondition.

What's the difference between crosshair cover and crosshair search? Does it have the option to minimize the size of a list if my function takes a list as input?

Thanks,
-zk

[pschanely]

Thank you @pschanely for your explanation.That makes sense. In general, what I want to do is to reduce the search space in real world applications, where the number of paths is exponential to the inputs. Kind of like what klee_assume() does in KLEE. Another example could be: given functiondef f(x: int, y: int) -> int, the user is only interested in test cases in which x > y by specifying that as a precondition.

Interesting! Ok, so my default suggestion is to wrap the code under analysis in a big if statement that checks the condition you want (e.g. x > y), and then filter the crosshair cover output to remove the case(s) that don't satisfy the same condition. Not sure how painful that is for your use case.

If you don't mind depending on crosshair internals that could change in future releases, you can raise CrossHair's internal IgnoreAttempt exception in the case you want to discard; then you won't need to filter the output. It'd look like this:

from crosshair.util import IgnoreAttempt
def mylen(lst: list[int]) -> int:
    if len(lst) >= 3:
        raise IgnoreAttempt
    ...

What's the difference between crosshair cover and crosshair search? Does it have the option to minimize the size of a list if my function takes a list as input?

crosshair search will only give you one input, while crosshair cover will give you a bunch of inputs that collectively give you code coverage. Another way to think about it is that the search command is a kind of an "optimizer." And, yes, you can use crosshair search to try and find a small list that satisfies some condition. Here are the relevant bits of the command help!:

% crosshair search -h
The search command finds arguments for a function that causes it to
complete without error.
options:
  --optimization OPTIMIZATION_TYPE
                        Controls what kind of arguments are produced.
                        Optimization effectiveness will vary wildly depnding on the nature of
                        the function.
                            simplify     : [default] Attempt to minimize the size
                                           (in characters) of the arguments.
                            none         : Output the first set of arguments found.
                            minimize_int : Attempt to minimize an integer returned by the
                                           function. Negative return values are ignored.

You can make the search command try harder with the --per_condition_timeout option too.

[zhenkun]

I'll try using raise IgnoreAttempt.
Generally speaking, would it possible to let crosshair cover respect the preconditions? After all, they are part of the contract of the function.

This is really a cool tool, and I appreciate your detailed reply @pschanely.

[pschanely]

Generally speaking, would it possible to let crosshair cover respect the preconditions? After all, they are part of the contract of the function.

It's conceivable, but begs additional questions, and I kinda suspect the answer changes depending on WHY you're calling cover in the first place. (for that matter, I'd love to hear about your case and goals):

• If you're generating tests, it's unclear whether you want to include inputs outside the precondition. It might be quite reasonable to want to test failure modes, even when the caller isn't adhering to the contract.
• In general, running the preconditions (and preconditions implied by class invariants) will make the path tree larger; is it acceptable to pay that cost for every use case?
• If you have a raises: clause, should the cover command not generate inputs that raise those exceptions? I am not sure.

I'm not shooting the idea down, mind you! Just musing about all the details.