[red-knot] Should A ∧ !A always be false? (#15839)

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.

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
+                // We execute the `else` once the condition evaluates to false. This could happen
-                // the pre-loop state before visiting `else`.
+                // without ever executing the body, if the condition is false the first time it's
-                self.flow_merge(pre_loop.clone());
+                // 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
+                        let visibility_constraint = self.add_visibility_constraint(
-                            .add_visibility_constraint(VisibilityConstraint::VisibleIf(constraint));
+                            VisibilityConstraint::VisibleIf(constraint, 0),
+                        );
 
                         let after_expr = self.flow_snapshot();
 

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
+            return a;
-        } else {
+        }
-            self.add(VisibilityConstraint::KleeneAnd(a, b))
+        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()
             }