74309008fd
## Summary This PR adds a new `property_tests` module with quickcheck-based tests that verify certain properties of types. The following properties are currently checked: * `is_equivalent_to`: * is reflexive: `T` is equivalent to itself * `is_subtype_of`: * is reflexive: `T` is a subtype of `T` * is antisymmetric: if `S <: T` and `T <: S`, then `S` is equivalent to `T` * is transitive: `S <: T` & `T <: U` => `S <: U` * `is_disjoint_from`: * is irreflexive: `T` is not disjoint from `T` * is symmetric: `S` disjoint from `T` => `T` disjoint from `S` * `is_assignable_to`: * is reflexive * `negate`: * is an involution: `T.negate().negate()` is equivalent to `T` There are also some tests that validate higher-level properties like: * `S <: T` implies that `S` is not disjoint from `T` * `S <: T` implies that `S` is assignable to `T` * A singleton type must also be single-valued These tests found a few bugs so far: - #14177 - #14195 - #14196 - #14210 - #14731 Some additional notes: - Quickcheck-based property tests are non-deterministic and finding counter-examples might take an arbitrary long time. This makes them bad candidates for running in CI (for every PR). We can think of running them in a cron-job way from time to time, similar to fuzzing. But for now, it's only possible to run them locally (see instructions in source code). - Some tests currently find false positive "counterexamples" because our understanding of equivalence of types is not yet complete. We do not understand that `int | str` is the same as `str | int`, for example. These tests are in a separate `property_tests::flaky` module. - Properties can not be formulated in every way possible, due to the fact that `is_disjoint_from` and `is_subtype_of` can produce false negative answers. - The current shrinking implementation is very naive, which leads to counterexamples that are very long (`str & Any & ~tuple[Any] & ~tuple[Unknown] & ~Literal[""] & ~Literal["a"] | str & int & ~tuple[Any] & ~tuple[Unknown]`), requiring the developer to simplify manually. It has not been a major issue so far, but there is a comment in the code how this can be improved. - The tests are currently implemented using a macro. This is a single commit on top which can easily be reverted, if we prefer the plain code instead. With the macro: ```rs // `S <: T` implies that `S` can be assigned to `T`. type_property_test!( subtype_of_implies_assignable_to, db, forall types s, t. s.is_subtype_of(db, t) => s.is_assignable_to(db, t) ); ``` without the macro: ```rs /// `S <: T` implies that `S` can be assigned to `T`. #[quickcheck] fn subtype_of_implies_assignable_to(s: Ty, t: Ty) -> bool { let db = get_cached_db(); let s = s.into_type(&db); let t = t.into_type(&db); !s.is_subtype_of(&*db, t) || s.is_assignable_to(&*db, t) } ``` ## Test Plan ```bash while cargo test --release -p red_knot_python_semantic --features property_tests types::property_tests; do :; done ```
57 lines
1.6 KiB
TOML
57 lines
1.6 KiB
TOML
[package]
|
|
name = "red_knot_python_semantic"
|
|
version = "0.0.0"
|
|
publish = false
|
|
authors = { workspace = true }
|
|
edition = { workspace = true }
|
|
rust-version = { workspace = true }
|
|
homepage = { workspace = true }
|
|
documentation = { workspace = true }
|
|
repository = { workspace = true }
|
|
license = { workspace = true }
|
|
|
|
[dependencies]
|
|
ruff_db = { workspace = true }
|
|
ruff_index = { workspace = true }
|
|
ruff_python_ast = { workspace = true }
|
|
ruff_python_parser = { workspace = true }
|
|
ruff_python_stdlib = { workspace = true }
|
|
ruff_source_file = { workspace = true }
|
|
ruff_text_size = { workspace = true }
|
|
ruff_python_literal = { workspace = true }
|
|
|
|
anyhow = { workspace = true }
|
|
bitflags = { workspace = true }
|
|
camino = { workspace = true }
|
|
compact_str = { workspace = true }
|
|
countme = { workspace = true }
|
|
indexmap = { workspace = true }
|
|
itertools = { workspace = true }
|
|
ordermap = { workspace = true }
|
|
salsa = { workspace = true }
|
|
thiserror = { workspace = true }
|
|
tracing = { workspace = true }
|
|
rustc-hash = { workspace = true }
|
|
hashbrown = { workspace = true }
|
|
serde = { workspace = true, optional = true }
|
|
smallvec = { workspace = true }
|
|
static_assertions = { workspace = true }
|
|
test-case = { workspace = true }
|
|
memchr = { workspace = true }
|
|
|
|
[dev-dependencies]
|
|
ruff_db = { workspace = true, features = ["os", "testing"] }
|
|
ruff_python_parser = { workspace = true }
|
|
red_knot_test = { workspace = true }
|
|
red_knot_vendored = { workspace = true }
|
|
|
|
anyhow = { workspace = true }
|
|
dir-test = { workspace = true }
|
|
insta = { workspace = true }
|
|
tempfile = { workspace = true }
|
|
quickcheck = { version = "1.0.3", default-features = false }
|
|
quickcheck_macros = { version = "1.0.0" }
|
|
|
|
[lints]
|
|
workspace = true
|