From fab86de3ef91460e58496f74ba1ce3edc4b9d69c Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Fri, 31 Jan 2025 14:06:52 -0500 Subject: [PATCH] =?UTF-8?q?[red-knot]=20Should=20A=20=E2=88=A7=20!A=20alwa?= =?UTF-8?q?ys=20be=20false=3F=20(#15839)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This mimics a simplification we have on the OR side, where we simplify `A ∨ !A` to true. This requires changes to how we add `while` statements to the semantic index, since we now need distinct `VisibilityConstraint`s if we need to model evaluating a `Constraint` multiple times at different points in the execution of the program. --- .../src/semantic_index/builder.rs | 43 +++++++++++++++---- .../src/visibility_constraints.rs | 34 ++++++++++++--- 2 files changed, 62 insertions(+), 15 deletions(-) diff --git a/crates/red_knot_python_semantic/src/semantic_index/builder.rs b/crates/red_knot_python_semantic/src/semantic_index/builder.rs index 8b8a6b56a3e50..8252a5f7a4e25 100644 --- a/crates/red_knot_python_semantic/src/semantic_index/builder.rs +++ b/crates/red_knot_python_semantic/src/semantic_index/builder.rs @@ -365,7 +365,7 @@ impl<'db> SemanticIndexBuilder<'db> { constraint: Constraint<'db>, ) -> ScopedVisibilityConstraintId { self.current_use_def_map_mut() - .record_visibility_constraint(VisibilityConstraint::VisibleIf(constraint)) + .record_visibility_constraint(VisibilityConstraint::VisibleIf(constraint, 0)) } /// Records that all remaining statements in the current block are unreachable, and therefore @@ -970,6 +970,14 @@ where let pre_loop = self.flow_snapshot(); let constraint = self.record_expression_constraint(test); + // We need multiple copies of the visibility constraint for the while condition, + // since we need to model situations where the first evaluation of the condition + // returns True, but a later evaluation returns False. + let first_vis_constraint_id = + self.add_visibility_constraint(VisibilityConstraint::VisibleIf(constraint, 0)); + let later_vis_constraint_id = + self.add_visibility_constraint(VisibilityConstraint::VisibleIf(constraint, 1)); + // Save aside any break states from an outer loop let saved_break_states = std::mem::take(&mut self.loop_break_states); @@ -980,26 +988,42 @@ where self.visit_body(body); self.set_inside_loop(outer_loop_state); - let vis_constraint_id = self.record_visibility_constraint(constraint); + // If the body is executed, we know that we've evaluated the condition at least + // once, and that the first evaluation was True. We might not have evaluated the + // condition more than once, so we can't assume that later evaluations were True. + // So the body's full visibility constraint is `first`. + let body_vis_constraint_id = first_vis_constraint_id; + self.record_visibility_constraint_id(body_vis_constraint_id); // Get the break states from the body of this loop, and restore the saved outer // ones. let break_states = std::mem::replace(&mut self.loop_break_states, saved_break_states); - // We may execute the `else` clause without ever executing the body, so merge in - // the pre-loop state before visiting `else`. - self.flow_merge(pre_loop.clone()); + // We execute the `else` once the condition evaluates to false. This could happen + // without ever executing the body, if the condition is false the first time it's + // tested. So the starting flow state of the `else` clause is the union of: + // - the pre-loop state with a visibility constraint that the first evaluation of + // the while condition was false, + // - the post-body state (which already has a visibility constraint that the + // first evaluation was true) with a visibility constraint that a _later_ + // evaluation of the while condition was false. + // To model this correctly, we need two copies of the while condition constraint, + // since the first and later evaluations might produce different results. + let post_body = self.flow_snapshot(); + self.flow_restore(pre_loop.clone()); + self.record_negated_visibility_constraint(first_vis_constraint_id); + self.flow_merge(post_body); self.record_negated_constraint(constraint); self.visit_body(orelse); - self.record_negated_visibility_constraint(vis_constraint_id); + self.record_negated_visibility_constraint(later_vis_constraint_id); // Breaking out of a while loop bypasses the `else` clause, so merge in the break // states after visiting `else`. for break_state in break_states { let snapshot = self.flow_snapshot(); self.flow_restore(break_state); - self.record_visibility_constraint(constraint); + self.record_visibility_constraint_id(body_vis_constraint_id); self.flow_merge(snapshot); } @@ -1523,8 +1547,9 @@ where ast::BoolOp::And => (constraint, self.add_constraint(constraint)), ast::BoolOp::Or => self.add_negated_constraint(constraint), }; - let visibility_constraint = self - .add_visibility_constraint(VisibilityConstraint::VisibleIf(constraint)); + let visibility_constraint = self.add_visibility_constraint( + VisibilityConstraint::VisibleIf(constraint, 0), + ); let after_expr = self.flow_snapshot(); diff --git a/crates/red_knot_python_semantic/src/visibility_constraints.rs b/crates/red_knot_python_semantic/src/visibility_constraints.rs index f19144fb5e072..1120bf0c8b2fc 100644 --- a/crates/red_knot_python_semantic/src/visibility_constraints.rs +++ b/crates/red_knot_python_semantic/src/visibility_constraints.rs @@ -168,11 +168,26 @@ use crate::Db; /// resulting from a few files with a lot of boolean expressions and `if`-statements. const MAX_RECURSION_DEPTH: usize = 24; +/// A ternary formula that defines under what conditions a binding is visible. (A ternary formula +/// is just like a boolean formula, but with `Ambiguous` as a third potential result. See the +/// module documentation for more details.) +/// +/// The primitive atoms of the formula are [`Constraint`]s, which express some property of the +/// runtime state of the code that we are analyzing. +/// +/// We assume that each atom has a stable value each time that the formula is evaluated. An atom +/// that resolves to `Ambiguous` might be true or false, and we can't tell which — but within that +/// evaluation, we assume that the atom has the _same_ unknown value each time it appears. That +/// allows us to perform simplifications like `A ∨ !A → true` and `A ∧ !A → false`. +/// +/// That means that when you are constructing a formula, you might need to create distinct atoms +/// for a particular [`Constraint`], if your formula needs to consider how a particular runtime +/// property might be different at different points in the execution of the program. #[derive(Clone, Debug, PartialEq, Eq)] pub(crate) enum VisibilityConstraint<'db> { AlwaysTrue, Ambiguous, - VisibleIf(Constraint<'db>), + VisibleIf(Constraint<'db>, u8), VisibleIfNot(ScopedVisibilityConstraintId), KleeneAnd(ScopedVisibilityConstraintId, ScopedVisibilityConstraintId), KleeneOr(ScopedVisibilityConstraintId, ScopedVisibilityConstraintId), @@ -221,11 +236,18 @@ impl<'db> VisibilityConstraints<'db> { b: ScopedVisibilityConstraintId, ) -> ScopedVisibilityConstraintId { if a == ScopedVisibilityConstraintId::ALWAYS_TRUE { - b + return b; } else if b == ScopedVisibilityConstraintId::ALWAYS_TRUE { - a - } else { - self.add(VisibilityConstraint::KleeneAnd(a, b)) + return a; + } + match (&self.constraints[a], &self.constraints[b]) { + (_, VisibilityConstraint::VisibleIfNot(id)) if a == *id => self.add( + VisibilityConstraint::VisibleIfNot(ScopedVisibilityConstraintId::ALWAYS_TRUE), + ), + (VisibilityConstraint::VisibleIfNot(id), _) if *id == b => self.add( + VisibilityConstraint::VisibleIfNot(ScopedVisibilityConstraintId::ALWAYS_TRUE), + ), + _ => self.add(VisibilityConstraint::KleeneAnd(a, b)), } } @@ -248,7 +270,7 @@ impl<'db> VisibilityConstraints<'db> { match visibility_constraint { VisibilityConstraint::AlwaysTrue => Truthiness::AlwaysTrue, VisibilityConstraint::Ambiguous => Truthiness::Ambiguous, - VisibilityConstraint::VisibleIf(constraint) => Self::analyze_single(db, constraint), + VisibilityConstraint::VisibleIf(constraint, _) => Self::analyze_single(db, constraint), VisibilityConstraint::VisibleIfNot(negated) => { self.evaluate_impl(db, *negated, max_depth - 1).negate() }