mirror of
https://github.com/astral-sh/ruff.git
synced 2025-10-02 22:55:08 +00:00
[red-knot] Property tests (#14178)
## 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 ```
This commit is contained in:
David Peter
GitHub
parent
a255d79087
commit
74309008fd
4 changed files with 309 additions and 34 deletions
|
|
@ -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();
|
||||
|
|
@ -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,
|
||||
|
|
@ -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,
|
||||
|
|
|
|||
237
crates/red_knot_python_semantic/src/types/property_tests.rs
Normal file
237
crates/red_knot_python_semantic/src/types/property_tests.rs
Normal file
|
|
@ -0,0 +1,237 @@
|
|||
//! This module contains quickcheck-based property tests for `Type`s.
|
||||
//!
|
||||
//! These tests are disabled by default, as they are non-deterministic and slow. You can
|
||||
//! run them explicitly using:
|
||||
//!
|
||||
//! ```sh
|
||||
//! cargo test -p red_knot_python_semantic -- --ignored types::property_tests::stable
|
||||
//! ```
|
||||
//!
|
||||
//! The number of tests (default: 100) can be controlled by setting the `QUICKCHECK_TESTS`
|
||||
//! environment variable. For example:
|
||||
//!
|
||||
//! ```sh
|
||||
//! QUICKCHECK_TESTS=10000 cargo test …
|
||||
//! ```
|
||||
//!
|
||||
//! If you want to run these tests for a longer period of time, it's advisable to run them
|
||||
//! in release mode. As some tests are slower than others, it's advisable to run them in a
|
||||
//! loop until they fail:
|
||||
//!
|
||||
//! ```sh
|
||||
//! export QUICKCHECK_TESTS=100000
|
||||
//! while cargo test --release -p red_knot_python_semantic -- \
|
||||
//! --ignored types::property_tests::stable; do :; done
|
||||
//! ```
|
||||
|
||||
use std::sync::{Arc, Mutex, MutexGuard, OnceLock};
|
||||
|
||||
use super::tests::{setup_db, Ty};
|
||||
use crate::db::tests::TestDb;
|
||||
use crate::types::KnownClass;
|
||||
use quickcheck::{Arbitrary, Gen};
|
||||
|
||||
fn arbitrary_core_type(g: &mut Gen) -> Ty {
|
||||
// We could select a random integer here, but this would make it much less
|
||||
// likely to explore interesting edge cases:
|
||||
let int_lit = Ty::IntLiteral(*g.choose(&[-2, -1, 0, 1, 2]).unwrap());
|
||||
let bool_lit = Ty::BooleanLiteral(bool::arbitrary(g));
|
||||
g.choose(&[
|
||||
Ty::Never,
|
||||
Ty::Unknown,
|
||||
Ty::None,
|
||||
Ty::Any,
|
||||
int_lit,
|
||||
bool_lit,
|
||||
Ty::StringLiteral(""),
|
||||
Ty::StringLiteral("a"),
|
||||
Ty::LiteralString,
|
||||
Ty::BytesLiteral(""),
|
||||
Ty::BytesLiteral("\x00"),
|
||||
Ty::KnownClassInstance(KnownClass::Object),
|
||||
Ty::KnownClassInstance(KnownClass::Str),
|
||||
Ty::KnownClassInstance(KnownClass::Int),
|
||||
Ty::KnownClassInstance(KnownClass::Bool),
|
||||
Ty::KnownClassInstance(KnownClass::List),
|
||||
Ty::KnownClassInstance(KnownClass::Tuple),
|
||||
Ty::KnownClassInstance(KnownClass::FunctionType),
|
||||
Ty::KnownClassInstance(KnownClass::SpecialForm),
|
||||
Ty::KnownClassInstance(KnownClass::TypeVar),
|
||||
Ty::KnownClassInstance(KnownClass::TypeAliasType),
|
||||
Ty::KnownClassInstance(KnownClass::NoDefaultType),
|
||||
Ty::TypingLiteral,
|
||||
Ty::BuiltinClassLiteral("str"),
|
||||
Ty::BuiltinClassLiteral("int"),
|
||||
Ty::BuiltinClassLiteral("bool"),
|
||||
Ty::BuiltinClassLiteral("object"),
|
||||
])
|
||||
.unwrap()
|
||||
.clone()
|
||||
}
|
||||
|
||||
/// Constructs an arbitrary type.
|
||||
///
|
||||
/// The `size` parameter controls the depth of the type tree. For example,
|
||||
/// a simple type like `int` has a size of 0, `Union[int, str]` has a size
|
||||
/// of 1, `tuple[int, Union[str, bytes]]` has a size of 2, etc.
|
||||
fn arbitrary_type(g: &mut Gen, size: u32) -> Ty {
|
||||
if size == 0 {
|
||||
arbitrary_core_type(g)
|
||||
} else {
|
||||
match u32::arbitrary(g) % 4 {
|
||||
0 => arbitrary_core_type(g),
|
||||
1 => Ty::Union(
|
||||
(0..*g.choose(&[2, 3]).unwrap())
|
||||
.map(|_| arbitrary_type(g, size - 1))
|
||||
.collect(),
|
||||
),
|
||||
2 => Ty::Tuple(
|
||||
(0..*g.choose(&[0, 1, 2]).unwrap())
|
||||
.map(|_| arbitrary_type(g, size - 1))
|
||||
.collect(),
|
||||
),
|
||||
3 => Ty::Intersection {
|
||||
pos: (0..*g.choose(&[0, 1, 2]).unwrap())
|
||||
.map(|_| arbitrary_type(g, size - 1))
|
||||
.collect(),
|
||||
neg: (0..*g.choose(&[0, 1, 2]).unwrap())
|
||||
.map(|_| arbitrary_type(g, size - 1))
|
||||
.collect(),
|
||||
},
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Arbitrary for Ty {
|
||||
fn arbitrary(g: &mut Gen) -> Ty {
|
||||
const MAX_SIZE: u32 = 2;
|
||||
arbitrary_type(g, MAX_SIZE)
|
||||
}
|
||||
|
||||
fn shrink(&self) -> Box<dyn Iterator<Item = Self>> {
|
||||
// This is incredibly naive. We can do much better here by
|
||||
// trying various subsets of the elements in unions, tuples,
|
||||
// and intersections. For now, we only try to shrink by
|
||||
// reducing unions/tuples/intersections to a single element.
|
||||
match self.clone() {
|
||||
Ty::Union(types) => Box::new(types.into_iter()),
|
||||
Ty::Tuple(types) => Box::new(types.into_iter()),
|
||||
Ty::Intersection { pos, neg } => Box::new(pos.into_iter().chain(neg)),
|
||||
_ => Box::new(std::iter::empty()),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
static CACHED_DB: OnceLock<Arc<Mutex<TestDb>>> = OnceLock::new();
|
||||
|
||||
fn get_cached_db() -> MutexGuard<'static, TestDb> {
|
||||
let db = CACHED_DB.get_or_init(|| Arc::new(Mutex::new(setup_db())));
|
||||
db.lock().unwrap()
|
||||
}
|
||||
|
||||
/// A macro to define a property test for types.
|
||||
///
|
||||
/// The `$test_name` identifier specifies the name of the test function. The `$db` identifier
|
||||
/// is used to refer to the salsa database in the property to be tested. The actual property is
|
||||
/// specified using the syntax:
|
||||
///
|
||||
/// forall types t1, t2, ..., tn . <property>`
|
||||
///
|
||||
/// where `t1`, `t2`, ..., `tn` are identifiers that represent arbitrary types, and `<property>`
|
||||
/// is an expression using these identifiers.
|
||||
///
|
||||
macro_rules! type_property_test {
|
||||
($test_name:ident, $db:ident, forall types $($types:ident),+ . $property:expr) => {
|
||||
#[quickcheck_macros::quickcheck]
|
||||
#[ignore]
|
||||
fn $test_name($($types: crate::types::tests::Ty),+) -> bool {
|
||||
let db_cached = super::get_cached_db();
|
||||
let $db = &*db_cached;
|
||||
$(let $types = $types.into_type($db);)+
|
||||
|
||||
$property
|
||||
}
|
||||
};
|
||||
// A property test with a logical implication.
|
||||
($name:ident, $db:ident, forall types $($types:ident),+ . $premise:expr => $conclusion:expr) => {
|
||||
type_property_test!($name, $db, forall types $($types),+ . !($premise) || ($conclusion));
|
||||
};
|
||||
}
|
||||
|
||||
mod stable {
|
||||
// `T` is equivalent to itself.
|
||||
type_property_test!(
|
||||
equivalent_to_is_reflexive, db,
|
||||
forall types t. t.is_equivalent_to(db, t)
|
||||
);
|
||||
|
||||
// `T` is a subtype of itself.
|
||||
type_property_test!(
|
||||
subtype_of_is_reflexive, db,
|
||||
forall types t. t.is_subtype_of(db, t)
|
||||
);
|
||||
|
||||
// `S <: T` and `T <: U` implies that `S <: U`.
|
||||
type_property_test!(
|
||||
subtype_of_is_transitive, db,
|
||||
forall types s, t, u. s.is_subtype_of(db, t) && t.is_subtype_of(db, u) => s.is_subtype_of(db, u)
|
||||
);
|
||||
|
||||
// `T` is not disjoint from itself, unless `T` is `Never`.
|
||||
type_property_test!(
|
||||
disjoint_from_is_irreflexive, db,
|
||||
forall types t. t.is_disjoint_from(db, t) => t.is_never()
|
||||
);
|
||||
|
||||
// `S` is disjoint from `T` implies that `T` is disjoint from `S`.
|
||||
type_property_test!(
|
||||
disjoint_from_is_symmetric, db,
|
||||
forall types s, t. s.is_disjoint_from(db, t) == t.is_disjoint_from(db, s)
|
||||
);
|
||||
|
||||
// `S <: T` implies that `S` is not disjoint from `T`, unless `S` is `Never`.
|
||||
type_property_test!(
|
||||
subtype_of_implies_not_disjoint_from, db,
|
||||
forall types s, t. s.is_subtype_of(db, t) => !s.is_disjoint_from(db, t) || s.is_never()
|
||||
);
|
||||
|
||||
// `T` can be assigned to itself.
|
||||
type_property_test!(
|
||||
assignable_to_is_reflexive, db,
|
||||
forall types t. t.is_assignable_to(db, t)
|
||||
);
|
||||
|
||||
// `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)
|
||||
);
|
||||
|
||||
// If `T` is a singleton, it is also single-valued.
|
||||
type_property_test!(
|
||||
singleton_implies_single_valued, db,
|
||||
forall types t. t.is_singleton(db) => t.is_single_valued(db)
|
||||
);
|
||||
}
|
||||
|
||||
/// This module contains property tests that currently lead to many false positives.
|
||||
///
|
||||
/// The reason for this is our insufficient understanding of equivalence of types. For
|
||||
/// example, we currently consider `int | str` and `str | int` to be different types.
|
||||
/// Similar issues exist for intersection types. Once this is resolved, we can move these
|
||||
/// tests to the `stable` section. In the meantime, it can still be useful to run these
|
||||
/// tests (using [`types::property_tests::flaky`]), to see if there are any new obvious bugs.
|
||||
mod flaky {
|
||||
// `S <: T` and `T <: S` implies that `S` is equivalent to `T`.
|
||||
type_property_test!(
|
||||
subtype_of_is_antisymmetric, db,
|
||||
forall types s, t. s.is_subtype_of(db, t) && t.is_subtype_of(db, s) => s.is_equivalent_to(db, t)
|
||||
);
|
||||
|
||||
// Negating `T` twice is equivalent to `T`.
|
||||
type_property_test!(
|
||||
double_negation_is_identity, db,
|
||||
forall types t. t.negate(db).negate(db).is_equivalent_to(db, t)
|
||||
);
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue