Introduce path search heuristic based on code coverage.
Optimize containment checks in symbolic strings. (fixes #207)
Add a new (highly experimental)
crosshair searchcommand. Some people have been using
crosshair checkto look for counterexamples that they intend or expect to find. The
crosshair searchcommand is an easier and more featureful way to do this, and includes an option to search for inputs that score best along some objective. There is nothing in the official docs yet for this, but fiddle with it on the command line and give some feedback in a github discussion!
--example_output_format=argument_dictionaryoption for the cover command never actually output a dictionary! This is now fixed with the similarly named option
--example_output_format=arg_dictionary; the old option will issue a warning for a few releases and then be removed.
Avoid false positive counterexample when user code handles
Exception. (fixes #196)
Reduce path explosion when parsing integers from a string.
Fix CrossHair build from source distribution (notably affects linux arm64 & Apple silicon). We still don’t ship binary packages to PyPI (github actions still does not have runners?) but at least you should be able to build on your own. (Fixes #197)
Add pygls 1.0 compatibility. (this is for the LSP server)
Complete Python 3.11 support!
Add symbolic branch collapsing for
all(). This can significantly reduce the number of branches to explore when these functions are applied to symbolic inputs.
Preserve symbolic bools through the
Fix premature path exhaustion when CrossHair attempts to generate
TypedDictinstances inside containers. (see this discussion)
Fix crash when attempting to create an instance of a user-defined class that has an argument named
typ. (fixes #191)
Save hypothesis counterexamples to the hypothesis database. Now, regular runs of hypothesis will try inputs that CrossHair has found. (thanks Zac-HD!)
Fix a regression in
crosshair watchthat crashes when the code under test attempts to print to stdout.
Fix issue with the new C tracer that could result in the tracer unexpectedly remaining engaged.
crosshair watchfile arguments exist on disk at launch time. (they can still disappear/reappear during execution without issue, however)
Implement several optimizations; CrossHair is >2X faster on nearly all of the official benchmarks!
Switch to an opcode tracer written in C. Build binary wheels on major platforms.
Optimize nondeterminism checking and z3 API usage; reuse SMT decisions.
Fix regex bug: count chars #28-#31 as whitespace in unicode mode.
Switch to use pre-commit for code checks. (no user-facing changes)
Supply encoding for setup.py’s open(). (fixes #179)
[breaking change] Change how custom classes are shown in counterexamples. Previously, CrossHair would call repr() on the instance of the custom class. Now, CrossHair will create an eval()able string that minics how CrossHair created the instance originally (and repr() is not used in the counterexample generation). (fixes #164)
[breaking change] Implement a different strategy for symbolic Callables. Now, symbolic callables simply invent a list of return values that are simply handed out, one at a time. This means that Callable counterexamples may be quite a bit more ugly. On the other hand, this new strategy fixes soundness issues and adds support for complex argument and return types. (only atomic types were supported previously)
[breaking change] Make it easier to work with timeouts. Now, if you specify a
--per_condition_timeout=parameter, CrossHair scales the
--per_path_timeout=default accordingly (namely, to the square root of the per_condition_timeout). That means just increasing the per_condition_timeout is sufficient uniformly scale up the amount of effort to put into a problem.
(Finally!) Upgrade our z3 version to the latest (18.104.22.168). Reach out if you notice significant changes in your environments!
Make some performance enhancements when type annotations are missing or incomplete (e.g.
x: listinstead of
Add missing f-string support for formatting, e.g.
Fix issues in
IgnoreAttemptexception could escape and cause the process to abnormally exit.
Fix a bug where
splitlines()was not splitting on “\r” characters.
Fix a bug where CrossHair mistakenly evaluated
" ".isprintable()to False.
LSP server: ensure the watcher thread has enough time to kill workers on shutdown.
Fix bug in which str/repr for bytes objects returned the NotImplemented object.
Fix important issues with list concatenation and slicing: ensure arguments are always evaluated properly, and that results are real symbolic lists.
Explicitly shut down the LSP server’s worker pool when getting a shutdown message from the client. Reduces the possibility of leaked workers. Ensure your VSCode extension is updated, too!
Unify comment parsing behavior for “raises” phrases in docstrings. (for consistency with other contract syntaxes, unparsable PEP316 raises phrases no longer produce syntax errors)
Preserve symbolics across int-to-str conversions.
Fix deque issues with extend(), extendleft(), and equality comparisons.
Improve performance in counterexample generation and regex against literals.
Add support for symbolic containment checks in concrete dictionaries.
Fix several issues with the LSP server on windows.
Fix cover command errors when applied to wrapped functions and methods of dataclasses.
Do not manually set
typing.TYPE_CHECKINGto True. This is a breaking change - unfortunately, too many regular and correct typing guards will not work at runtime with TYPE_CHECKING on. (for one, you can use a guard to protect an import of a
.pyimodule, e.g. pytorch in #172 ) CrossHair will now only be able to understand types that are present and resolvable at runtime. (previously it might have been able to resolve types in more cases, e.g. the circular dependencies in #32 )
cachedecorations during analysis. (this prevents nondeterministic errors when analyzing code that uses them!)
Disable side-effect detection when importing modules. (fixes #172)
Reduce path explosions when checking for symbolic string containment in a concrete string.
Fix unexpected nondeterminism exception when calling
Finish making sure
unicodedatafunctions are tolerant to symbolic string arguments.
heapqfunctions tolerant to symbolic list arguments.
Fix crash when running
crosshair coverover functions that raise exceptions. (fixes #171)
Add symbolic handling when the callback used in
partialis native and intolerant to symbolics. (string functions, most commonly)
Allow writes to the “nul” file on Windows.
Add various preparations for Python 3.11.
crosshair servercommand. This starts a Language Server Protocol (LSP) server that can simplify integration with several IDEs. (look for new versions of the VSCode extension that use this soon; consider contributing one for your favorite editor!)
Present counterexamples that describe argument aliasing using the “walrus” operator, e.g.
foo([a:=, , a])to describe a counterexample that takes a list of three empty sublists, where the frist and third are the same list. (fixes #48) Note that CrossHair does not yet reliably detect all kinds of aliasing problems; see this issue in particular.
Fix code parse error over docstrings with blank lines.
Fix bug when
get()is called with a numeric symbolic key on a concrete dictionary.
Fix crash when
re.finditer()is invoked on a sliced string.
itertools.groupbycan be itercepted with
Correctly lowercase mid-word, mixed-case characters when titlecasing a string.
Fix a crash when the checked code imports additional modules at runtime which define new namedtuples.
CrossHair can now invent symbolic return values for many calls like
random.randrange. See this issue for what’s supported.
Allow subprocess spawning by standard library modules like
ctypes. Previously, CrossHair would crash on some calls/platforms, complaining about side effects. (fixes #163)
Add support for attaching a contract to an external function. Among other things, this can help you check code involving nondeterministic functions like
time.time(). See the docs for all the details. (thanks to lmontand for this massive effort!)
Correctly handle preconditions with recursive calls to the contracted function. (see this test)
str.capitalize()behavior in python 3.7.
CrossHair now has datetime support that doesn’t destructively modify the system’s datetime module. (fixes #159)
Added a new specs_complete directive: use this to let functions return any value confirming to their contract. This can be useful for (ensuring you don’t depend on implementation details).
Fix formatting symbolic enums as decimals.
Use comparisons to guess types for untyped values.
Permit writes to /dev/null, allowing imports for pytorch. (see #157)
Resolve types dependent on TYPE_CHECKING guards in more cases. (see #158)
Made various diagnosic improvements for
Mix up the message-of-the-day when exiting
Implemented minor performance and search heuristic improvements.
Add support for memoryview. (see #153)
Add path search hueristics to bias for code coverage.
Fix bug in newline detection for
Fix bug for title-case characters in
Correctly model when
issubclassover symbolics raise exceptions.
Completed Python 3.10 support.
Complete symbolic support for all string methods! (see #39)
Complete symbolic support JSON encode and decode!
Add symbolic support for ascii, latin-1, and utf8 encode and decode.
Add symbolic support for StringIO.
Fix bugs in string comparisons, re.finditer, isinstance, delete-by-slice.
Add symbolic support for set comprehensions.
Add minor optimizations for tracing and repeated slicing.
Skip copies for uncopy-able arguments (see #146)
Fix bug for special cases when
__new__should be called without
Completed full symbolic regex support!
The remaining features were non-greedy matching (
.*?), word boundaries (
\b), and negated sets (
Fixed crash on clean installation which expected Deal to be installed - that dependency is now fully optional. (issue)
Avoid crash when
crosshair watchhas been running for a while on trivial cases. (issue)
Add symbolic support for f-strings.
Add symbolic support for dictionary comprehensions with symbolic keys.
Add support for counterexamples in full unicode! (previously, we’d only find counterexamples in latin-1)
Add support for checking Deal contracts! (details)
Give reproducible failures for code involving random number generation.
Add symbolic support for string predicates: isalpha, isspace, isascii, isdecimal, isdigit, islower, isnumeric, isprintable, isalnum, and istitle.
Expand symbolic regex support: search, sub, subn, finditer, re.MULTILINE, lookahead/lookbehind, and lastindex/lastgroup.
Add support for checking Hypothesis tests! (details)
--analysis_kind=assertoption is no longer enabled by default. (it was spuriously detecting functions for analysis too regularly) Enable assert-mode explicitly on the command line if you use CrossHair this way.
analysis_kindoption in code comment “directives.”
Add some minimal symbolic support for the standard library
Add symbolic support for
Expand symbolic support for ord(), chr(), and integer round().
Expand symbolic support for some bitwise operations and
crosshair covercommand. (details)
Implement and document CrossHair’s plugin system. (details)
3rd party Cython modules sometimes include both binary and pure versions of the code. Now CrossHair can access the pure Python code in such distributions, allowing it to symbolically execute them.
Add symbolic support for integer and float parsing.
Add symbolic support for indexing into concrete dictionaries with symbolic keys.
Add regex support for the whitespace (”\s”) class. (regex support is still ASCII-only right now though)
Miscellaneous fixes: string indexing, numeric promotions, named regex groups
Fix regression for
watchcommand, which crashed when watched files have a syntax error.
watchcommand to consistently detect when files are deleted.
Expand symbolic handling for some string containment use cases.
Refactored tracing intercept logic to support arbitrary opcode interceptions (will unlock new symbolic strategies)
The type() function is now patched (it no longer reveals symbolic types).
Completed Python 3.9 support.
Refined (make less magical) and documented custom class suggestions.
Fixed out-of-bounds slicing in certain cases.
Fixed regression breaking check by class name.
Fixed crash on “watch .” and an excessive auditwall block on os.walk.
Fixed issue targeting by line number.
Fixed error on no command line arguments.
Further simplification of
crosshair watchoutput for broader terminal support.
crosshair watchscreen clearing mechanism for terminals like Thonny’s.
Several string methods can now be reasoned about symbolically: split, find, replace, index, partition, count, and more. (thanks Rik-de-Kort!)
Fixed various bugs, including a few specific to icontract analysis.
Modestly increased regex cases that CrossHair handles. (including named groups!)
Enable analysis when only preconditions exist. (this is useful if you just want to catch exceptions!)
--report_verboseoption to customize whether you get verbose multi-line counterexample reports or the single-line, machine-readable reporting. (command help)
Added workaround for missing
crosshair watchoutput in the PyCharm terminal.
Added support for checking plain
Advanced internal code standards: black, mypy, pydocstyle, and more. (thanks mristin!)
Added basic protection against dangerous side-effects with
Analysis can now be targeted by function at line number; e.g.
crosshair check foo.py:42
Modules and functions may include a directive comment like
# crosshair: onor
# crosshair: offto customize targeting.
Realization heuristics enable solutions for some use cases like this that are challenging for Z3.
Enable symbolic reasoning about getattr and friends. (example)
Fixes or improvements related to:
builtin tolerance for symbolic values
User-defined class proxy generation
Classmethods on int & float.
Floordiv and mod operators
list.index()and list ordering
xor operations over sets