1
1
//! This module contains quickcheck-based property tests for `Type`s.
2
2
//!
3
- //! These tests are feature-gated and disabled by default. You can run them using:
3
+ //! These tests are disabled by default, as they are non-deterministic and slow. You can
4
+ //! run them explicitly using:
4
5
//!
5
6
//! ```sh
6
- //! cargo test -p red_knot_python_semantic --features property_tests types::property_tests
7
+ //! cargo test -p red_knot_python_semantic -- --ignored types::property_tests::stable
7
8
//! ```
8
9
//!
9
- //! You can control the number of tests (default: 100) by setting the `QUICKCHECK_TESTS`
10
- //! variable. For example:
10
+ //! The number of tests (default: 100) can be controlled by setting the `QUICKCHECK_TESTS`
11
+ //! environment variable. For example:
11
12
//!
12
13
//! ```sh
13
14
//! QUICKCHECK_TESTS=10000 cargo test …
19
20
//!
20
21
//! ```sh
21
22
//! export QUICKCHECK_TESTS=100000
22
- //! while cargo test --release -p red_knot_python_semantic \
23
- //! --features property_tests types::property_tests; do :; done
23
+ //! while cargo test --release -p red_knot_python_semantic -- \
24
+ //! --ignored types::property_tests::stable ; do :; done
24
25
//! ```
25
26
26
27
use std:: sync:: { Arc , Mutex , MutexGuard , OnceLock } ;
27
28
28
29
use super :: tests:: { setup_db, Ty } ;
29
- use super :: Type ;
30
30
use crate :: db:: tests:: TestDb ;
31
31
use crate :: types:: KnownClass ;
32
- use crate :: Db ;
33
32
use quickcheck:: { Arbitrary , Gen } ;
34
- use quickcheck_macros:: quickcheck;
35
33
36
34
fn arbitrary_core_type ( g : & mut Gen ) -> Ty {
37
35
// We could select a random integer here, but this would make it much less
@@ -125,27 +123,6 @@ impl Arbitrary for Ty {
125
123
}
126
124
}
127
125
128
- impl < ' db > Type < ' db > {
129
- /// Checks if a type contains `Never` in its tree.
130
- ///
131
- /// This is currently needed since we currently don't propagate/simplify types containing
132
- /// `Never`. For example, the type `tuple[int, Never]` is equivalent to `Never`. Similarly,
133
- /// we simplify `Never` in unions, but we would not simplify `str | tuple[int, Never]`, so
134
- /// we need to descent into unions and intersections as well.
135
- fn contains_never ( & self , db : & ' db dyn Db ) -> bool {
136
- match self {
137
- Type :: Never => true ,
138
- Type :: Union ( types) => types. elements ( db) . iter ( ) . any ( |t| t. contains_never ( db) ) ,
139
- Type :: Tuple ( types) => types. elements ( db) . iter ( ) . any ( |t| t. contains_never ( db) ) ,
140
- Type :: Intersection ( inner) => {
141
- inner. positive ( db) . iter ( ) . any ( |t| t. contains_never ( db) )
142
- || inner. negative ( db) . iter ( ) . any ( |t| t. contains_never ( db) )
143
- }
144
- _ => false ,
145
- }
146
- }
147
- }
148
-
149
126
static CACHED_DB : OnceLock < Arc < Mutex < TestDb > > > = OnceLock :: new ( ) ;
150
127
151
128
fn get_cached_db ( ) -> MutexGuard < ' static , TestDb > {
@@ -155,9 +132,10 @@ fn get_cached_db() -> MutexGuard<'static, TestDb> {
155
132
156
133
macro_rules! type_property_test {
157
134
( $name: ident, $db: ident, ( $( $types: ident) ,+) , $body: expr) => {
158
- #[ quickcheck]
159
- fn $name( $( $types: Ty ) ,+) -> bool {
160
- let db_cached = get_cached_db( ) ;
135
+ #[ quickcheck_macros:: quickcheck]
136
+ #[ ignore]
137
+ fn $name( $( $types: crate :: types:: tests:: Ty ) ,+) -> bool {
138
+ let db_cached = super :: get_cached_db( ) ;
161
139
let $db = & * db_cached;
162
140
$( let $types = $types. into_type( $db) ; ) +
163
141
@@ -178,72 +156,83 @@ macro_rules! type_property_test {
178
156
} ;
179
157
}
180
158
181
- // `T` is equivalent to itself.
182
- type_property_test ! ( equivalent_to_is_reflexive, db, t, t. is_equivalent_to( db, t) ) ;
183
-
184
- // `T` is a subtype of itself.
185
- type_property_test ! ( subtype_of_is_reflexive, db, t, t. is_subtype_of( db, t) ) ;
186
-
187
- // `S <: T` and `T <: S` implies that `S` is equivalent to `T`.
188
- type_property_test ! (
189
- subtype_of_is_antisymmetric,
190
- db,
191
- ( s, t) ,
192
- s. is_subtype_of( db, t) && t. is_subtype_of( db, s) => s. is_equivalent_to( db, t)
193
- ) ;
194
-
195
- // `S <: T` and `T <: U` implies that `S <: U`.
196
- type_property_test ! (
197
- subtype_of_is_transitive,
198
- db,
199
- ( s, t, u) ,
200
- s. is_subtype_of( db, t) && t. is_subtype_of( db, u) => s. is_subtype_of( db, u)
201
- ) ;
202
-
203
- // `T` is not disjoint from itself, unless `T` is `Never`.
204
- type_property_test ! (
205
- disjoint_from_is_irreflexive,
206
- db,
207
- t,
208
- t. is_disjoint_from( db, t) => t. contains_never( db)
209
- ) ;
210
-
211
- // `S` is disjoint from `T` implies that `T` is disjoint from `S`.
212
- type_property_test ! (
213
- disjoint_from_is_symmetric,
214
- db,
215
- ( s, t) ,
216
- s. is_disjoint_from( db, t) == t. is_disjoint_from( db, s)
217
- ) ;
218
-
219
- // `S <: T` implies that `S` is not disjoint from `T`, unless `S` is `Never`.
220
- type_property_test ! ( subtype_of_implies_not_disjoint_from, db, ( s, t) ,
221
- s. is_subtype_of( db, t) => !s. is_disjoint_from( db, t) || s. contains_never( db)
222
- ) ;
223
-
224
- // `T` can be assigned to itself.
225
- type_property_test ! ( assignable_to_is_reflexive, db, t, t. is_assignable_to( db, t) ) ;
226
-
227
- // `S <: T` implies that `S` can be assigned to `T`.
228
- type_property_test ! (
229
- subtype_of_implies_assignable_to,
230
- db,
231
- ( s, t) ,
232
- s. is_subtype_of( db, t) => s. is_assignable_to( db, t)
233
- ) ;
234
-
235
- // If `T` is a singleton, it is also single-valued.
236
- type_property_test ! (
237
- singleton_implies_single_valued,
238
- db,
239
- t,
240
- t. is_singleton( db) => t. is_single_valued( db)
241
- ) ;
242
-
243
- // Negating `T` twice is equivalent to `T`.
244
- type_property_test ! (
245
- double_negation_is_identity,
246
- db,
247
- t,
248
- t. negate( db) . negate( db) . is_equivalent_to( db, t)
249
- ) ;
159
+ mod stable {
160
+ // `T` is equivalent to itself.
161
+ type_property_test ! ( equivalent_to_is_reflexive, db, t, t. is_equivalent_to( db, t) ) ;
162
+
163
+ // `T` is a subtype of itself.
164
+ type_property_test ! ( subtype_of_is_reflexive, db, t, t. is_subtype_of( db, t) ) ;
165
+
166
+ // `S <: T` and `T <: U` implies that `S <: U`.
167
+ type_property_test ! (
168
+ subtype_of_is_transitive,
169
+ db,
170
+ ( s, t, u) ,
171
+ s. is_subtype_of( db, t) && t. is_subtype_of( db, u) => s. is_subtype_of( db, u)
172
+ ) ;
173
+
174
+ // `T` is not disjoint from itself, unless `T` is `Never`.
175
+ type_property_test ! (
176
+ disjoint_from_is_irreflexive,
177
+ db,
178
+ t,
179
+ t. is_disjoint_from( db, t) => t. is_never( )
180
+ ) ;
181
+
182
+ // `S` is disjoint from `T` implies that `T` is disjoint from `S`.
183
+ type_property_test ! (
184
+ disjoint_from_is_symmetric,
185
+ db,
186
+ ( s, t) ,
187
+ s. is_disjoint_from( db, t) == t. is_disjoint_from( db, s)
188
+ ) ;
189
+
190
+ // `S <: T` implies that `S` is not disjoint from `T`, unless `S` is `Never`.
191
+ type_property_test ! ( subtype_of_implies_not_disjoint_from, db, ( s, t) ,
192
+ s. is_subtype_of( db, t) => !s. is_disjoint_from( db, t) || s. is_never( )
193
+ ) ;
194
+
195
+ // `T` can be assigned to itself.
196
+ type_property_test ! ( assignable_to_is_reflexive, db, t, t. is_assignable_to( db, t) ) ;
197
+
198
+ // `S <: T` implies that `S` can be assigned to `T`.
199
+ type_property_test ! (
200
+ subtype_of_implies_assignable_to,
201
+ db,
202
+ ( s, t) ,
203
+ s. is_subtype_of( db, t) => s. is_assignable_to( db, t)
204
+ ) ;
205
+
206
+ // If `T` is a singleton, it is also single-valued.
207
+ type_property_test ! (
208
+ singleton_implies_single_valued,
209
+ db,
210
+ t,
211
+ t. is_singleton( db) => t. is_single_valued( db)
212
+ ) ;
213
+ }
214
+
215
+ /// This module contains property tests that currently lead to many false positives.
216
+ ///
217
+ /// The reason for this is our insufficient understanding of equivalence of types. For
218
+ /// example, we currently consider `int | str` and `str | int` to be different types.
219
+ /// Similar issues exist for intersection types. Once this is resolved, we can move these
220
+ /// tests to the `stable` section. In the meantime, it can still be useful to run these
221
+ /// tests (using [`types::property_tests::flaky`]), to see if there are any new obvious bugs.
222
+ mod flaky {
223
+ // `S <: T` and `T <: S` implies that `S` is equivalent to `T`.
224
+ type_property_test ! (
225
+ subtype_of_is_antisymmetric,
226
+ db,
227
+ ( s, t) ,
228
+ s. is_subtype_of( db, t) && t. is_subtype_of( db, s) => s. is_equivalent_to( db, t)
229
+ ) ;
230
+
231
+ // Negating `T` twice is equivalent to `T`.
232
+ type_property_test ! (
233
+ double_negation_is_identity,
234
+ db,
235
+ t,
236
+ t. negate( db) . negate( db) . is_equivalent_to( db, t)
237
+ ) ;
238
+ }
0 commit comments