danog/psalm
1
0
Fork 0
mirror of https://github.com/danog/psalm.git synced 2024-11-27 04:45:20 +01:00
Code Issues Projects Releases Wiki Activity

Convert DNF conditions to CNF

Browse Source
This commit is contained in:
Matthew Brown 2018-05-05 20:32:04 -04:00
parent 00838d19b5
commit c31f787f7c
5 changed files with 124 additions and 75 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

109
src/Psalm/Checker/AlgebraChecker.php
View File

@ -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;
}
}

10
src/Psalm/Checker/Statements/Block/IfChecker.php
View File

@ -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);
}

4
src/Psalm/Checker/Statements/Expression/BinaryOpChecker.php
View File

@ -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(

3
tests/IssetTest.php
View File

@ -61,9 +61,6 @@ class IssetTest extends TestCase
}',
'assertions' => [],
'error_levels' => ['PossiblyInvalidArrayAccess'],
'scope_vars' => [
'$foo' => \Psalm\Type::getArray(),
],
],
'nullCoalesceKeyedOffset' => [
'<?php

73
tests/TypeAlgebraTest.php
View File

@ -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