Fix #6683 by improving simplification of CNF (#7631)

vimeo · Feb 11, 2022 · 6d05766 · 6d05766
1 parent b49b5f1
commit 6d05766
Show file tree

Hide file tree

Showing 3 changed files with 107 additions and 7 deletions.
diff --git a/src/Psalm/Internal/Algebra.php b/src/Psalm/Internal/Algebra.php
@@ -9,13 +9,15 @@
 
 use function array_diff_key;
 use function array_filter;
+use function array_intersect_key;
 use function array_keys;
 use function array_map;
 use function array_merge;
 use function array_pop;
 use function array_unique;
 use function array_values;
 use function count;
+use function in_array;
 use function mt_rand;
 
 /**
@@ -238,11 +240,90 @@ public static function simplifyCNF(array $clauses): array
             }
 
             if (!$is_redundant) {
-                $simplified_clauses[] = $clause_a;
+                $simplified_clauses[$clause_a->hash] = $clause_a;
             }
         }
 
-        return $simplified_clauses;
+        $clause_count = count($simplified_clauses);
+
+        // simplify (A || X) && (!A || Y) && (X || Y)
+        // to
+        // simplify (A || X) && (!A || Y)
+        // where X and Y are sets of orred terms
+        if ($clause_count > 2 && $clause_count < 256) {
+            $clauses = array_values($simplified_clauses);
+            for ($i = 0; $i < $clause_count; $i++) {
+                $clause_a = $clauses[$i];
+                for ($k = $i + 1; $k < $clause_count; $k++) {
+                    $clause_b = $clauses[$k];
+                    $common_keys = array_keys(
+                        array_intersect_key($clause_a->possibilities, $clause_b->possibilities)
+                    );
+                    if ($common_keys) {
+                        $common_negated_keys = [];
+                        foreach ($common_keys as $common_key) {
+                            if (count($clause_a->possibilities[$common_key]) === 1
+                                && count($clause_b->possibilities[$common_key]) === 1
+                                && $clause_a->possibilities[$common_key][0]->isNegationOf(
+                                    $clause_b->possibilities[$common_key][0]
+                                )
+                            ) {
+                                $common_negated_keys[] = $common_key;
+                            }
+                        }
+
+                        if ($common_negated_keys) {
+                            $new_possibilities = [];
+
+                            foreach ($clause_a->possibilities as $var_id => $possibilities) {
+                                if (in_array($var_id, $common_negated_keys, true)) {
+                                    continue;
+                                }
+
+                                if (!isset($new_possibilities[$var_id])) {
+                                    $new_possibilities[$var_id] = $possibilities;
+                                } else {
+                                    $new_possibilities[$var_id] = array_merge(
+                                        $new_possibilities[$var_id],
+                                        $possibilities,
+                                    );
+                                }
+                            }
+
+                            foreach ($clause_b->possibilities as $var_id => $possibilities) {
+                                if (in_array($var_id, $common_negated_keys, true)) {
+                                    continue;
+                                }
+
+                                if (!isset($new_possibilities[$var_id])) {
+                                    $new_possibilities[$var_id] = $possibilities;
+                                } else {
+                                    $new_possibilities[$var_id] = array_merge(
+                                        $new_possibilities[$var_id],
+                                        $possibilities,
+                                    );
+                                }
+                            }
+
+                            /** @psalm-suppress MixedArgumentTypeCoercion due I think to Psalm bug */
+                            $conflict_clause = (new Clause(
+                                $new_possibilities,
+                                $clause_a->creating_conditional_id,
+                                $clause_a->creating_conditional_id,
+                                false,
+                                true,
+                                true,
+                                []
+                            ))->makeUnique();
+
+                            unset($simplified_clauses[$conflict_clause->hash]);
+                        }
+                    }
+                }
+            }
+        }
+
+        return array_values($simplified_clauses);
     }
 
     /**

diff --git a/src/Psalm/Internal/Analyzer/Statements/Block/IfElseAnalyzer.php b/src/Psalm/Internal/Analyzer/Statements/Block/IfElseAnalyzer.php
@@ -172,14 +172,13 @@ function (Clause $c) use ($mixed_var_ids, $cond_object_id): Clause {
             $assigned_in_conditional_var_ids
         );
 
-        // if we have assignments in the if, we may have duplicate clauses
-        if ($assigned_in_conditional_var_ids) {
-            $if_clauses = Algebra::simplifyCNF($if_clauses);
-        }
+        $if_clauses = Algebra::simplifyCNF($if_clauses);
 
         $if_context_clauses = array_merge($entry_clauses, $if_clauses);
 
-        $if_context->clauses = Algebra::simplifyCNF($if_context_clauses);
+        $if_context->clauses = $entry_clauses
+            ? Algebra::simplifyCNF($if_context_clauses)
+            : $if_context_clauses;
 
         if ($if_context->reconciled_expression_clauses) {
             $reconciled_expression_clauses = $if_context->reconciled_expression_clauses;

diff --git a/tests/TypeReconciliation/TypeAlgebraTest.php b/tests/TypeReconciliation/TypeAlgebraTest.php
@@ -1160,6 +1160,26 @@ final public function map(Throwable $throwable, string $class): ?Throwable
                         }
                     }'
             ],
+            'combineTwoOrredClausesWithUnnecessaryTerm' => [
+                'code' => '<?php
+                    function foo(bool $a, bool $b, bool $c): void {
+                        if (($a && $b) || (!$a && $c)) {
+                            //
+                        } else {
+                            if ($c) {}
+                        }
+                    }'
+            ],
+            'combineTwoOrredClausesWithMoreComplexUnnecessaryTerm' => [
+                'code' => '<?php
+                    function foo(bool $a, bool $b, bool $c): void {
+                        if ((!$a && !$b) || ($a && $b) || ($a && $c)) {
+                            throw new \Exception();
+                        }
+
+                        if ($a) {}
+                    }'
+            ],
         ];
     }