From c31f787f7c7a2bc6fe63135fd0e61747b35eee9b Mon Sep 17 00:00:00 2001
From: Matthew Brown <github@muglug.com>
Date: Sat, 5 May 2018 20:32:04 -0400
Subject: [PATCH] Convert DNF conditions to CNF

---
 src/Psalm/Checker/AlgebraChecker.php          | 109 ++++++++----------
 .../Checker/Statements/Block/IfChecker.php    |  10 +-
 .../Statements/Expression/BinaryOpChecker.php |   4 +-
 tests/IssetTest.php                           |   3 -
 tests/TypeAlgebraTest.php                     |  73 +++++++++++-
 5 files changed, 124 insertions(+), 75 deletions(-)

diff --git a/src/Psalm/Checker/AlgebraChecker.php b/src/Psalm/Checker/AlgebraChecker.php
index 77e32e2a6..a9ec22be4 100644
--- a/src/Psalm/Checker/AlgebraChecker.php
+++ b/src/Psalm/Checker/AlgebraChecker.php
@@ -53,29 +53,17 @@ class AlgebraChecker
         ) {
             // at the moment we only support formulae in CNF
 
-            if (!$conditional->left instanceof PhpParser\Node\Expr\BinaryOp\BooleanAnd &&
-                !$conditional->left instanceof PhpParser\Node\Expr\BinaryOp\LogicalAnd
-            ) {
-                $left_clauses = self::getFormula(
-                    $conditional->left,
-                    $this_class_name,
-                    $source
-                );
-            } else {
-                $left_clauses = [new Clause([], true)];
-            }
+            $left_clauses = self::getFormula(
+                $conditional->left,
+                $this_class_name,
+                $source
+            );
 
-            if (!$conditional->right instanceof PhpParser\Node\Expr\BinaryOp\BooleanAnd &&
-                !$conditional->right instanceof PhpParser\Node\Expr\BinaryOp\LogicalAnd
-            ) {
-                $right_clauses = self::getFormula(
-                    $conditional->right,
-                    $this_class_name,
-                    $source
-                );
-            } else {
-                $right_clauses = [new Clause([], true)];
-            }
+            $right_clauses = self::getFormula(
+                $conditional->right,
+                $this_class_name,
+                $source
+            );
 
             return self::combineOredClauses($left_clauses, $right_clauses);
         }
@@ -101,11 +89,6 @@ class AlgebraChecker
                         $clauses[] = new Clause([$base_key => ['^!empty']]);
                     }
 
-                    if (!empty($key_parts)) {
-                        $clauses[] = new Clause([$base_key => ['!false']]);
-                        $clauses[] = new Clause([$base_key => ['!int']]);
-                    }
-
                     while ($key_parts) {
                         $divider = array_shift($key_parts);
 
@@ -130,11 +113,6 @@ class AlgebraChecker
                         } else {
                             $clauses[] = new Clause([$base_key => ['^!empty']]);
                         }
-
-                        if (count($key_parts)) {
-                            $clauses[] = new Clause([$base_key => ['!false']]);
-                            $clauses[] = new Clause([$base_key => ['!int']]);
-                        }
                     }
                 } else {
                     $clauses[] = new Clause([$var => [$type]]);
@@ -584,7 +562,9 @@ class AlgebraChecker
                     foreach ($impossible_types as $impossible_type) {
                         $new_clause_possibilities = $grouped_clause->possibilities;
 
-                        if (isset($grouped_clause->possibilities[$var])) {
+                        if (isset($grouped_clause->possibilities[$var])
+                            && !in_array($impossible_type, $new_clause_possibilities[$var])
+                        ) {
                             $new_clause_possibilities[$var][] = $impossible_type;
                         } else {
                             $new_clause_possibilities[$var] = [$impossible_type];
@@ -623,43 +603,50 @@ class AlgebraChecker
      */
     public static function combineOredClauses(array $left_clauses, array $right_clauses)
     {
-        // we cannot deal, at the moment, with orring non-CNF clauses
-        if (count($left_clauses) !== 1 || count($right_clauses) !== 1) {
-            return [new Clause([], true)];
-        }
+        $clauses = [];
 
-        $possibilities = [];
+        $all_wedges = true;
 
-        if ($left_clauses[0]->wedge && $right_clauses[0]->wedge) {
-            return [new Clause([], true)];
-        }
+        foreach ($left_clauses as $left_clause) {
+            foreach ($right_clauses as $right_clause) {
+                $possibilities = [];
 
-        $can_reconcile = true;
+                $can_reconcile = true;
 
-        if ($left_clauses[0]->wedge ||
-            $right_clauses[0]->wedge ||
-            !$left_clauses[0]->reconcilable ||
-            !$right_clauses[0]->reconcilable
-        ) {
-            $can_reconcile = false;
-        }
+                $all_wedges = $all_wedges && $left_clause->wedge && $right_clause->wedge;
 
-        foreach ($left_clauses[0]->possibilities as $var => $possible_types) {
-            if (isset($possibilities[$var])) {
-                $possibilities[$var] = array_merge($possibilities[$var], $possible_types);
-            } else {
-                $possibilities[$var] = $possible_types;
+                if ($left_clause->wedge ||
+                    $right_clause->wedge ||
+                    !$left_clause->reconcilable ||
+                    !$right_clause->reconcilable
+                ) {
+                    $can_reconcile = false;
+                }
+
+                foreach ($left_clause->possibilities as $var => $possible_types) {
+                    if (isset($possibilities[$var])) {
+                        $possibilities[$var] = array_merge($possibilities[$var], $possible_types);
+                    } else {
+                        $possibilities[$var] = $possible_types;
+                    }
+                }
+
+                foreach ($right_clause->possibilities as $var => $possible_types) {
+                    if (isset($possibilities[$var])) {
+                        $possibilities[$var] = array_merge($possibilities[$var], $possible_types);
+                    } else {
+                        $possibilities[$var] = $possible_types;
+                    }
+                }
+
+                $clauses[] = new Clause($possibilities, false, $can_reconcile);
             }
         }
 
-        foreach ($right_clauses[0]->possibilities as $var => $possible_types) {
-            if (isset($possibilities[$var])) {
-                $possibilities[$var] = array_merge($possibilities[$var], $possible_types);
-            } else {
-                $possibilities[$var] = $possible_types;
-            }
+        if ($all_wedges) {
+            return [new Clause([], true)];
         }
 
-        return [new Clause($possibilities, false, $can_reconcile)];
+        return $clauses;
     }
 }
diff --git a/src/Psalm/Checker/Statements/Block/IfChecker.php b/src/Psalm/Checker/Statements/Block/IfChecker.php
index d286a4165..27911ecd1 100644
--- a/src/Psalm/Checker/Statements/Block/IfChecker.php
+++ b/src/Psalm/Checker/Statements/Block/IfChecker.php
@@ -237,7 +237,7 @@ class IfChecker
         // define this before we alter local claues after reconciliation
         $if_scope->reasonable_clauses = $if_context->clauses;
 
-        $if_scope->negated_clauses = AlgebraChecker::negateFormula($if_clauses);
+        $if_scope->negated_clauses = AlgebraChecker::simplifyCNF(AlgebraChecker::negateFormula($if_clauses));
 
         $if_scope->negated_types = AlgebraChecker::getTruthsFromFormula(
             AlgebraChecker::simplifyCNF(
@@ -481,11 +481,9 @@ class IfChecker
 
         if ($context->collect_references) {
             foreach ($newly_unreferenced_locations as $var_id => $locations) {
-                if ((
-                    $stmt->else
-                        && (isset($if_scope->assigned_var_ids[$var_id])
-                            || isset($if_scope->new_vars[$var_id]))
-                    ) || (!isset($context->vars_in_scope[$var_id]))
+                if (($stmt->else
+                        && (isset($if_scope->assigned_var_ids[$var_id]) || isset($if_scope->new_vars[$var_id])))
+                    || !isset($context->vars_in_scope[$var_id])
                 ) {
                     $context->unreferenced_vars[$var_id] = array_shift($locations);
                 }
diff --git a/src/Psalm/Checker/Statements/Expression/BinaryOpChecker.php b/src/Psalm/Checker/Statements/Expression/BinaryOpChecker.php
index 2d53afa22..d6073e83f 100644
--- a/src/Psalm/Checker/Statements/Expression/BinaryOpChecker.php
+++ b/src/Psalm/Checker/Statements/Expression/BinaryOpChecker.php
@@ -861,8 +861,8 @@ class BinaryOpChecker
                             continue;
                         }
 
-                        if (($left_type_part instanceof TFloat && $right_type_part instanceof TInt) ||
-                            ($left_type_part instanceof TInt && $right_type_part instanceof TFloat)
+                        if (($left_type_part instanceof TFloat && $right_type_part instanceof TInt)
+                            || ($left_type_part instanceof TInt && $right_type_part instanceof TFloat)
                         ) {
                             if ($config->strict_binary_operands) {
                                 if ($statements_source && IssueBuffer::accepts(
diff --git a/tests/IssetTest.php b/tests/IssetTest.php
index b5d51bf12..caf4336a7 100644
--- a/tests/IssetTest.php
+++ b/tests/IssetTest.php
@@ -61,9 +61,6 @@ class IssetTest extends TestCase
                     }',
                 'assertions' => [],
                 'error_levels' => ['PossiblyInvalidArrayAccess'],
-                'scope_vars' => [
-                    '$foo' => \Psalm\Type::getArray(),
-                ],
             ],
             'nullCoalesceKeyedOffset' => [
                 '<?php
diff --git a/tests/TypeAlgebraTest.php b/tests/TypeAlgebraTest.php
index b911d004d..8715555e4 100644
--- a/tests/TypeAlgebraTest.php
+++ b/tests/TypeAlgebraTest.php
@@ -522,8 +522,7 @@ class TypeAlgebraTest extends TestCase
                         }
                     } catch (Exception $e) {}',
             ],
-            // because we only support expressions in CNF atm
-            'SKIPPED-instanceofInOr' => [
+            'instanceofInOr' => [
                 '<?php
                     class A {}
                     class B extends A {}
@@ -539,6 +538,74 @@ class TypeAlgebraTest extends TestCase
                         }
                     }',
             ],
+            'instanceofInOrNegated' => [
+                '<?php
+                    class A {}
+                    class B extends A {}
+                    class C extends A {}
+
+                    function takesA(A $a): void {}
+
+                    function foo(?A $a, ?A $b, ?A $c): void {
+                        if (!$a || ($b && $c)
+                        ) {
+                            return;
+                        }
+
+                        takesA($a);
+                    }',
+            ],
+            'instanceofInBothOrs' => [
+                '<?php
+                    class A {}
+                    class B extends A {}
+                    class C extends A {}
+
+                    function takesA(A $a): void {}
+
+                    function foo(?A $a): void {
+                        if (($a instanceof B && rand(0, 1))
+                            || ($a instanceof C && rand(0, 1))
+                        ) {
+                            takesA($a);
+                        }
+                    }',
+            ],
+            'instanceofInBothOrsWithSecondVar' => [
+                '<?php
+                    class A {}
+                    class B extends A {}
+                    class C extends A {}
+
+                    function takesA(A $a): void {}
+
+                    function foo(?A $a, ?A $b): void {
+                        if (($a instanceof B && $b instanceof B)
+                            || ($a instanceof C && $b instanceof C)
+                        ) {
+                            takesA($a);
+                            takesA($b);
+                        }
+                    }',
+            ],
+            'explosionOfCNF' => [
+                '<?php
+                    class A {
+                        /** @var ?string */
+                        public $foo;
+
+                        /** @var ?string */
+                        public $bar;
+                    }
+
+                    $a1 = rand(0, 1) ? new A() : null;
+                    $a4 = rand(0, 1) ? new A() : null;
+                    $a5 = rand(0, 1) ? new A() : null;
+                    $a7 = rand(0, 1) ? new A() : null;
+                    $a8 = rand(0, 1) ? new A() : null;
+
+                    if ($a1 || (($a4 && $a5) || ($a7 && $a8))) {}',
+            ],
             'instanceofInCNFOr' => [
                 '<?php
                     class A {}
@@ -753,7 +820,7 @@ class TypeAlgebraTest extends TestCase
                         if (!$a) return $b;
                         return $a;
                     }',
-                'error_message' => 'NullableReturnStatement',
+                'error_message' => 'ParadoxicalCondition',
             ],
             'twoVarLogicNotNestedWithElseifIncorrectlyReinforcedInIf' => [
                 '<?php