2019-07-15 22:08:38 +02:00
|
|
|
<?php
|
|
|
|
namespace Psalm\Tests;
|
|
|
|
|
|
|
|
use PhpParser;
|
|
|
|
use Psalm\Context;
|
2020-11-03 22:15:44 +01:00
|
|
|
use Psalm\Internal\Algebra\FormulaGenerator;
|
2019-07-15 22:08:38 +02:00
|
|
|
use Psalm\Internal\Analyzer\FileAnalyzer;
|
|
|
|
use Psalm\Internal\Analyzer\StatementsAnalyzer;
|
2020-11-03 22:15:44 +01:00
|
|
|
use Psalm\Internal\Algebra;
|
2019-07-15 22:08:38 +02:00
|
|
|
use Psalm\Internal\Clause;
|
|
|
|
use Psalm\Internal\Provider\StatementsProvider;
|
|
|
|
|
|
|
|
class AlgebraTest extends TestCase
|
|
|
|
{
|
2020-09-12 17:24:05 +02:00
|
|
|
public function testNegateFormula(): void
|
2019-07-15 22:08:38 +02:00
|
|
|
{
|
|
|
|
$formula = [
|
2020-08-26 21:35:29 +02:00
|
|
|
new Clause(['$a' => ['!falsy']], 1, 1),
|
2019-07-15 22:08:38 +02:00
|
|
|
];
|
|
|
|
|
|
|
|
$negated_formula = Algebra::negateFormula($formula);
|
|
|
|
|
|
|
|
$this->assertCount(1, $negated_formula);
|
|
|
|
$this->assertSame(['$a' => ['falsy']], $negated_formula[0]->possibilities);
|
|
|
|
|
|
|
|
$formula = [
|
2020-08-26 21:35:29 +02:00
|
|
|
new Clause(['$a' => ['!falsy'], '$b' => ['!falsy']], 1, 1),
|
2019-07-15 22:08:38 +02:00
|
|
|
];
|
|
|
|
|
|
|
|
$negated_formula = Algebra::negateFormula($formula);
|
|
|
|
|
|
|
|
$this->assertCount(2, $negated_formula);
|
|
|
|
$this->assertSame(['$a' => ['falsy']], $negated_formula[0]->possibilities);
|
|
|
|
$this->assertSame(['$b' => ['falsy']], $negated_formula[1]->possibilities);
|
|
|
|
|
|
|
|
$formula = [
|
2020-08-26 21:35:29 +02:00
|
|
|
new Clause(['$a' => ['!falsy']], 1, 1),
|
|
|
|
new Clause(['$b' => ['!falsy']], 1, 2),
|
2019-07-15 22:08:38 +02:00
|
|
|
];
|
|
|
|
|
|
|
|
$negated_formula = Algebra::negateFormula($formula);
|
|
|
|
|
|
|
|
$this->assertCount(1, $negated_formula);
|
2020-08-26 16:41:47 +02:00
|
|
|
$this->assertSame(['$b' => ['falsy'], '$a' => ['falsy']], $negated_formula[0]->possibilities);
|
2019-07-15 22:08:38 +02:00
|
|
|
|
|
|
|
$formula = [
|
2020-08-26 21:35:29 +02:00
|
|
|
new Clause(['$a' => ['int', 'string'], '$b' => ['!falsy']], 1, 1),
|
2019-07-15 22:08:38 +02:00
|
|
|
];
|
|
|
|
|
|
|
|
$negated_formula = Algebra::negateFormula($formula);
|
|
|
|
|
|
|
|
$this->assertCount(3, $negated_formula);
|
|
|
|
$this->assertSame(['$a' => ['!int']], $negated_formula[0]->possibilities);
|
|
|
|
$this->assertSame(['$a' => ['!string']], $negated_formula[1]->possibilities);
|
|
|
|
$this->assertSame(['$b' => ['falsy']], $negated_formula[2]->possibilities);
|
|
|
|
}
|
|
|
|
|
2020-11-03 22:44:24 +01:00
|
|
|
public function testNegateFormulaWithUnreconcilableTerm(): void
|
|
|
|
{
|
|
|
|
$formula = [
|
|
|
|
new Clause(['$a' => ['int']], 1, 1),
|
|
|
|
new Clause(['$b' => ['int']], 1, 2, false, false),
|
|
|
|
];
|
|
|
|
|
|
|
|
$negated_formula = Algebra::negateFormula($formula);
|
|
|
|
|
|
|
|
$this->assertCount(1, $negated_formula);
|
|
|
|
$this->assertSame(['$a' => ['!int']], $negated_formula[0]->possibilities);
|
|
|
|
}
|
|
|
|
|
2020-09-12 17:24:05 +02:00
|
|
|
public function testCombinatorialExpansion(): void
|
2019-07-15 22:08:38 +02:00
|
|
|
{
|
|
|
|
$dnf = '<?php ($b0 === true && $b4 === true && $b8 === true)
|
|
|
|
|| ($b0 === true && $b1 === true && $b2 === true)
|
|
|
|
|| ($b0 === true && $b3 === true && $b6 === true)
|
|
|
|
|| ($b1 === true && $b4 === true && $b7 === true)
|
|
|
|
|| ($b2 === true && $b5 === true && $b8 === true)
|
|
|
|
|| ($b2 === true && $b4 === true && $b6 === true)
|
|
|
|
|| ($b3 === true && $b4 === true && $b5 === true)
|
|
|
|
|| ($b6 === true && $b7 === true && $b8 === true);';
|
|
|
|
|
2020-08-09 22:23:43 +02:00
|
|
|
$dnf_stmt = StatementsProvider::parseStatements($dnf, '7.4')[0];
|
2019-07-15 22:08:38 +02:00
|
|
|
|
|
|
|
$this->assertInstanceOf(PhpParser\Node\Stmt\Expression::class, $dnf_stmt);
|
|
|
|
|
|
|
|
$file_analyzer = new FileAnalyzer($this->project_analyzer, 'somefile.php', 'somefile.php');
|
|
|
|
$file_analyzer->context = new Context();
|
2019-11-25 17:44:54 +01:00
|
|
|
$statements_analyzer = new StatementsAnalyzer($file_analyzer, new \Psalm\Internal\Provider\NodeDataProvider());
|
2019-07-15 22:08:38 +02:00
|
|
|
|
2020-11-03 22:15:44 +01:00
|
|
|
$dnf_clauses = FormulaGenerator::getFormula(
|
2020-08-26 21:35:29 +02:00
|
|
|
\spl_object_id($dnf_stmt->expr),
|
2019-12-08 22:35:56 +01:00
|
|
|
\spl_object_id($dnf_stmt->expr),
|
2019-07-15 22:08:38 +02:00
|
|
|
$dnf_stmt->expr,
|
|
|
|
null,
|
|
|
|
$statements_analyzer
|
|
|
|
);
|
|
|
|
|
|
|
|
$this->assertCount(6561, $dnf_clauses);
|
|
|
|
|
|
|
|
$simplified_dnf_clauses = Algebra::simplifyCNF($dnf_clauses);
|
|
|
|
|
|
|
|
$this->assertCount(23, $simplified_dnf_clauses);
|
|
|
|
}
|
|
|
|
|
2020-09-12 17:24:05 +02:00
|
|
|
public function testContainsClause(): void
|
2019-07-15 22:08:38 +02:00
|
|
|
{
|
|
|
|
$this->assertTrue(
|
|
|
|
(new Clause(
|
|
|
|
[
|
|
|
|
'$a' => ['!falsy'],
|
|
|
|
'$b' => ['!falsy'],
|
2020-08-26 21:35:29 +02:00
|
|
|
],
|
|
|
|
1,
|
|
|
|
1
|
2019-07-15 22:08:38 +02:00
|
|
|
))->contains(
|
|
|
|
new Clause(
|
|
|
|
[
|
|
|
|
'$a' => ['!falsy'],
|
2020-08-26 21:35:29 +02:00
|
|
|
],
|
|
|
|
1,
|
|
|
|
1
|
2019-07-15 22:08:38 +02:00
|
|
|
)
|
|
|
|
)
|
|
|
|
);
|
|
|
|
|
|
|
|
$this->assertFalse(
|
|
|
|
(new Clause(
|
|
|
|
[
|
|
|
|
'$a' => ['!falsy'],
|
2020-08-26 21:35:29 +02:00
|
|
|
],
|
|
|
|
1,
|
|
|
|
1
|
2019-07-15 22:08:38 +02:00
|
|
|
))->contains(
|
|
|
|
new Clause(
|
|
|
|
[
|
|
|
|
'$a' => ['!falsy'],
|
|
|
|
'$b' => ['!falsy'],
|
2020-08-26 21:35:29 +02:00
|
|
|
],
|
|
|
|
1,
|
|
|
|
1
|
2019-07-15 22:08:38 +02:00
|
|
|
)
|
|
|
|
)
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
2020-09-12 17:24:05 +02:00
|
|
|
public function testSimplifyCNF(): void
|
2019-07-15 22:08:38 +02:00
|
|
|
{
|
|
|
|
$formula = [
|
2020-08-26 21:35:29 +02:00
|
|
|
new Clause(['$a' => ['!falsy']], 1, 1),
|
|
|
|
new Clause(['$a' => ['falsy'], '$b' => ['falsy']], 1, 2),
|
2019-07-15 22:08:38 +02:00
|
|
|
];
|
|
|
|
|
|
|
|
$simplified_formula = Algebra::simplifyCNF($formula);
|
|
|
|
|
|
|
|
$this->assertCount(2, $simplified_formula);
|
|
|
|
$this->assertSame(['$a' => ['!falsy']], $simplified_formula[0]->possibilities);
|
|
|
|
$this->assertSame(['$b' => ['falsy']], $simplified_formula[1]->possibilities);
|
|
|
|
}
|
2020-03-30 01:42:22 +02:00
|
|
|
|
2020-10-24 17:31:36 +02:00
|
|
|
public function testSimplifyCNFWithUselessTerm(): void
|
|
|
|
{
|
|
|
|
$formula = [
|
|
|
|
new Clause(['$a' => ['!falsy'], '$b' => ['!falsy']], 1, 1),
|
|
|
|
new Clause(['$a' => ['falsy'], '$b' => ['!falsy']], 1, 2),
|
|
|
|
];
|
|
|
|
|
|
|
|
$simplified_formula = Algebra::simplifyCNF($formula);
|
|
|
|
|
|
|
|
$this->assertCount(1, $simplified_formula);
|
|
|
|
$this->assertSame(['$b' => ['!falsy']], $simplified_formula[0]->possibilities);
|
|
|
|
}
|
|
|
|
|
2020-10-26 21:18:42 +01:00
|
|
|
public function testSimplifyCNFWithNonUselessTerm(): void
|
|
|
|
{
|
|
|
|
$formula = [
|
|
|
|
new Clause(['$a' => ['!falsy'], '$b' => ['!falsy']], 1, 1),
|
|
|
|
new Clause(['$a' => ['falsy'], '$b' => ['falsy']], 1, 2),
|
|
|
|
];
|
|
|
|
|
|
|
|
$simplified_formula = Algebra::simplifyCNF($formula);
|
|
|
|
|
|
|
|
$this->assertCount(2, $simplified_formula);
|
|
|
|
$this->assertSame(['$a' => ['!falsy'], '$b' => ['!falsy']], $simplified_formula[0]->possibilities);
|
|
|
|
$this->assertSame(['$a' => ['falsy'], '$b' => ['falsy']], $simplified_formula[1]->possibilities);
|
|
|
|
}
|
|
|
|
|
2020-10-24 17:31:36 +02:00
|
|
|
public function testSimplifyCNFWithUselessTermAndOneInMiddle(): void
|
|
|
|
{
|
|
|
|
$formula = [
|
|
|
|
new Clause(['$a' => ['!falsy'], '$b' => ['!falsy']], 1, 1),
|
|
|
|
new Clause(['$b' => ['!falsy']], 1, 2),
|
|
|
|
new Clause(['$a' => ['falsy'], '$b' => ['!falsy']], 1, 3),
|
|
|
|
];
|
|
|
|
|
|
|
|
$simplified_formula = Algebra::simplifyCNF($formula);
|
|
|
|
|
|
|
|
$this->assertCount(1, $simplified_formula);
|
|
|
|
$this->assertSame(['$b' => ['!falsy']], $simplified_formula[0]->possibilities);
|
|
|
|
}
|
|
|
|
|
2020-03-30 01:42:22 +02:00
|
|
|
public function testGroupImpossibilities() : void
|
|
|
|
{
|
2020-08-26 16:41:47 +02:00
|
|
|
$clause1 = (new \Psalm\Internal\Clause(
|
2020-03-30 01:42:22 +02:00
|
|
|
[
|
|
|
|
'$a' => ['=array']
|
|
|
|
],
|
2020-08-26 21:35:29 +02:00
|
|
|
1,
|
|
|
|
2,
|
2020-03-30 01:42:22 +02:00
|
|
|
false,
|
|
|
|
true,
|
|
|
|
true,
|
2020-08-26 21:35:29 +02:00
|
|
|
[]
|
2020-08-26 16:41:47 +02:00
|
|
|
))->calculateNegation();
|
2020-03-30 01:42:22 +02:00
|
|
|
|
2020-08-26 16:41:47 +02:00
|
|
|
$clause2 = (new \Psalm\Internal\Clause(
|
2020-03-30 01:42:22 +02:00
|
|
|
[
|
|
|
|
'$b' => ['isset']
|
|
|
|
],
|
2020-08-26 21:35:29 +02:00
|
|
|
1,
|
|
|
|
2,
|
2020-03-30 01:42:22 +02:00
|
|
|
false,
|
|
|
|
true,
|
|
|
|
true,
|
2020-08-26 21:35:29 +02:00
|
|
|
[]
|
2020-08-26 16:41:47 +02:00
|
|
|
))->calculateNegation();
|
2020-03-30 01:42:22 +02:00
|
|
|
|
|
|
|
$result_clauses = Algebra::groupImpossibilities([$clause1, $clause2]);
|
|
|
|
|
|
|
|
$this->assertCount(0, $result_clauses);
|
|
|
|
}
|
2019-07-15 22:08:38 +02:00
|
|
|
}
|