Skip to content

Commit

Permalink
[red-knot] Property tests (#14178)
Browse files Browse the repository at this point in the history
## 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
```
  • Loading branch information
sharkdp authored Dec 3, 2024
1 parent a255d79 commit 7430900
Show file tree
Hide file tree
Showing 4 changed files with 309 additions and 34 deletions.
95 changes: 64 additions & 31 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions crates/red_knot_python_semantic/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,8 @@ 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
9 changes: 6 additions & 3 deletions crates/red_knot_python_semantic/src/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,9 @@ mod signatures;
mod string_annotation;
mod unpacker;

#[cfg(test)]
mod property_tests;

#[salsa::tracked(return_ref)]
pub fn check_types(db: &dyn Db, file: File) -> TypeCheckDiagnostics {
let _span = tracing::trace_span!("check_types", file=?file.path(db)).entered();
Expand Down Expand Up @@ -3083,8 +3086,8 @@ pub(crate) mod tests {

/// A test representation of a type that can be transformed unambiguously into a real Type,
/// given a db.
#[derive(Debug, Clone)]
enum Ty {
#[derive(Debug, Clone, PartialEq)]
pub(crate) enum Ty {
Never,
Unknown,
None,
Expand All @@ -3108,7 +3111,7 @@ pub(crate) mod tests {
}

impl Ty {
fn into_type(self, db: &TestDb) -> Type<'_> {
pub(crate) fn into_type(self, db: &TestDb) -> Type<'_> {
match self {
Ty::Never => Type::Never,
Ty::Unknown => Type::Unknown,
Expand Down
Loading

0 comments on commit 7430900

Please sign in to comment.