search

pschanely / CrossHair

An analysis tool for Python that blurs the line between testing and type systems.
Other
1.03k stars 49 forks source link

The replace function is not dealt with CrossHair #152

Closed kionactf closed 2 years ago

kionactf commented 2 years ago

Expected vs actual behavior Expected: n = 'p./y' Actual Behavior: No counterexample

To Reproduce def make_bigger(n: str) -> str: ''' post: not('py' in return) ''' if 'py' in n: return '' n = n.replace('./', '') return n

pschanely commented 2 years ago

Thanks for this report! CrossHair needs some time to chew on string operations at present, and a plain crosshair check won't usually give it enough time to find a counterexample. I think str.replace is functioning correctly here, but slowly. Please take a look yourself and confirm!

Our docs around timeout options aren't the best, but usually you fiddle with --per_path_timeout and --per_condition_timeout. Here is a crosshair-web example. crosshair-web allows a timeout of up to 5 seconds, and that's approximately what we need here, so I'm seeing it return the counterexample you're looking for: false when calling make_bigger(n = 'p./y').

crosshair watch effectively checks forever with increasing timeouts, so I recommend using that in most cases. It will also find this counterexample after several seconds.

CrossHair performance is one of the next big development arcs that I'm focusing on, so hopefully you can expect improvements soon. That said, prepare yourself to be surprised by CrossHair's wildly varying performance (seemingly similar problems could take seconds, hours, or years to find a counterexample). I still want bug reports for "slow" queries, though, because they can help me try to better align CrossHair's path search tactics to human expectations over time. (I'm adding this example now to a growing list of benchmarks - thanks!)

kionactf commented 2 years ago

Thanks for quick reply. I confirmed str.replace functionality worked correctly when the proper option was set. I look forward to seeing performance improvements of CrossHair.

pschanely commented 2 years ago

Great to hear.

I've added this example to a nascent benchmarking suite here, and going to close this issue out now.

If you're willing, please continue to let me know about cases where crosshair doesn't find the counterexample, or doesn't find it in a reasonable timeframe. Cheers!