packages/deriver/tests/Unit/Deriver/Evaluator/Domain/LatticeTest.php
1<?php
2
3declare (strict_types=1);
4
5namespace Tests\Unit\Deriver\Evaluator\Domain;
6
7use Deriver\Deriver;
8use Deriver\Deriver\Candidate\ResultRef;
9use Deriver\Deriver\Candidate\Snapshot;
10use Deriver\Deriver\Candidate\Statistics;
11use Deriver\Deriver\Contributions;
12use Deriver\Deriver\DeriverConfig;
13use Deriver\Deriver\Evaluator\Call\Evaluators;
14use Deriver\Deriver\Evaluator\Call\Extensions;
15use Deriver\Deriver\Evaluator\Call\Registrations;
16use Deriver\Deriver\Evaluator\Call\StateRegistry;
17use Deriver\Deriver\Evaluator\Domain\AbstractDomain;
18use Deriver\Deriver\Evaluator\Domain\DomainFact;
19use Deriver\Deriver\Evaluator\Domain\DomainOperations;
20use Deriver\Deriver\Evaluator\Domain\Lattice;
21use Deriver\Deriver\Evaluator\EvaluatorConfig;
22use Deriver\Deriver\Evaluator\Evidence\Frontier;
23use Deriver\Deriver\Evaluator\Execution\Call\ArgumentBinding;
24use Deriver\Deriver\Evaluator\Execution\Call\ArgumentOrder;
25use Deriver\Deriver\Evaluator\Execution\Call\ParameterBinding;
26use Deriver\Deriver\Evaluator\Execution\Call\TypeBinding;
27use Deriver\Deriver\Evaluator\Execution\Call\TypeCheck;
28use Deriver\Deriver\Evaluator\Execution\Completion\Alternative;
29use Deriver\Deriver\Evaluator\Execution\Completion\Assessment;
30use Deriver\Deriver\Evaluator\Execution\Completion\Completion;
31use Deriver\Deriver\Evaluator\Execution\Completion\Quality\DependencyClosure;
32use Deriver\Deriver\Evaluator\Execution\Completion\Quality\Enumeration;
33use Deriver\Deriver\Evaluator\Execution\Completion\Quality\ValuePrecision;
34use Deriver\Deriver\Evaluator\Execution\Completion\StorageSnapshot;
35use Deriver\Deriver\Evaluator\Execution\Constraints;
36use Deriver\Deriver\Evaluator\Execution\Context;
37use Deriver\Deriver\Evaluator\Execution\Control\LoopConvergence;
38use Deriver\Deriver\Evaluator\Execution\Control\ObservationLimit;
39use Deriver\Deriver\Evaluator\Execution\Control\StateJoin;
40use Deriver\Deriver\Evaluator\Execution\Control\Unwinding;
41use Deriver\Deriver\Evaluator\Execution\Demand\Cell;
42use Deriver\Deriver\Evaluator\Execution\Demand\Components;
43use Deriver\Deriver\Evaluator\Execution\Demand\Discovery;
44use Deriver\Deriver\Evaluator\Execution\Demand\Key;
45use Deriver\Deriver\Evaluator\Execution\Demand\Table;
46use Deriver\Deriver\Evaluator\Execution\Dependencies;
47use Deriver\Deriver\Evaluator\Execution\Evaluator;
48use Deriver\Deriver\Evaluator\Execution\EvaluatorConfig as ExecutionEvaluatorConfig;
49use Deriver\Deriver\Evaluator\Execution\InstructionTransfer;
50use Deriver\Deriver\Evaluator\Execution\Memory\Location;
51use Deriver\Deriver\Evaluator\Execution\Memory\Materialization;
52use Deriver\Deriver\Evaluator\Execution\Memory\Memory;
53use Deriver\Deriver\Evaluator\Execution\Memory\ReferenceConstraint;
54use Deriver\Deriver\Evaluator\Execution\Memory\Slots\SlotReference;
55use Deriver\Deriver\Evaluator\Execution\Memory\StorageCapture;
56use Deriver\Deriver\Evaluator\Execution\ObservationCollector;
57use Deriver\Deriver\Evaluator\Execution\Operation\Conversions;
58use Deriver\Deriver\Evaluator\Execution\Operation\ScalarErrors;
59use Deriver\Deriver\Evaluator\Execution\State;
60use Deriver\Deriver\Evaluator\Execution\Summary\CompletionRecord;
61use Deriver\Deriver\Evaluator\Execution\Summary\Evaluation;
62use Deriver\Deriver\Evaluator\Execution\Summary\Invocation;
63use Deriver\Deriver\Evaluator\Execution\Summary\Isolation;
64use Deriver\Deriver\Evaluator\Execution\Trace\Derivation;
65use Deriver\Deriver\Evaluator\Execution\Transfer\CompoundAssignment;
66use Deriver\Deriver\Evaluator\Execution\Transfer\MemoryStep;
67use Deriver\Deriver\Evaluator\Execution\Transfer\PureStep;
68use Deriver\Deriver\Evaluator\Execution\Transfer\ReferenceAssignment;
69use Deriver\Deriver\Evaluator\Projection;
70use Deriver\Deriver\Evaluator\Request\Budget;
71use Deriver\Deriver\Evaluator\Request\EntryPoint;
72use Deriver\Deriver\Evaluator\Request\QueryScope;
73use Deriver\Deriver\Evaluator\Request\ReturnQuery;
74use Deriver\Deriver\Evaluator\Scalar\Arithmetic;
75use Deriver\Deriver\Evaluator\Scalar\Comparison;
76use Deriver\Deriver\Evaluator\Scalar\Identity;
77use Deriver\Deriver\Evaluator\Scalar\Increment;
78use Deriver\Deriver\Evaluator\Scalar\Operations;
79use Deriver\Deriver\Evaluator\Scalar\StringPrefix;
80use Deriver\Deriver\Evaluator\TargetProfile;
81use Deriver\Deriver\Evaluator\Term;
82use Deriver\Deriver\Evaluator\TermKind;
83use Deriver\Deriver\Execution\DerivationResult;
84use Deriver\Deriver\Execution\QueryExecution;
85use Deriver\Deriver\Execution\ResultAssessment;
86use Deriver\Deriver\Identity\QueryEncoding;
87use Deriver\Deriver\Identity\ValueGraph;
88use Deriver\Deriver\Lowerer\AssignmentLowering;
89use Deriver\Deriver\Lowerer\Control\DestructuringLowering;
90use Deriver\Deriver\Lowerer\Control\LoopLowering;
91use Deriver\Deriver\Lowerer\Declaration\CallableIdentity;
92use Deriver\Deriver\Lowerer\Declaration\CallableSource;
93use Deriver\Deriver\Lowerer\Declaration\Index;
94use Deriver\Deriver\Lowerer\Declaration\Indexer;
95use Deriver\Deriver\Lowerer\Declaration\Traits\Composition;
96use Deriver\Deriver\Lowerer\EffectInspection;
97use Deriver\Deriver\Lowerer\ExpressionLowering;
98use Deriver\Deriver\Lowerer\Graph\BasicBlock;
99use Deriver\Deriver\Lowerer\Graph\CallableGraph;
100use Deriver\Deriver\Lowerer\Graph\Instruction;
101use Deriver\Deriver\Lowerer\Graph\Parameter;
102use Deriver\Deriver\Lowerer\Graph\Terminator;
103use Deriver\Deriver\Lowerer\Hierarchy\Dispatch;
104use Deriver\Deriver\Lowerer\InstructionEmitter;
105use Deriver\Deriver\Lowerer\Lowerer;
106use Deriver\Deriver\Lowerer\LoweringScope;
107use Deriver\Deriver\Lowerer\StatementLowering;
108use Deriver\Deriver\MicroEvaluatorConversion;
109use Deriver\Deriver\Parser\Node\File;
110use Deriver\Deriver\Parser\Parser;
111use Deriver\Deriver\Parser\ParserConfig;
112use Deriver\Deriver\Parser\TargetSyntax;
113use Deriver\Deriver\Providers\ProviderExpansion;
114use Deriver\Deriver\Resolver\AssignmentPatterns;
115use Deriver\Deriver\Resolver\ClassScope;
116use Deriver\Deriver\Resolver\ExpressionValidation;
117use Deriver\Deriver\Resolver\MagicContext;
118use Deriver\Deriver\Resolver\Resolver;
119use Deriver\Deriver\Selection\QueryValidation;
120use Deriver\Deriver\SnapshotIdentity;
121use Deriver\Deriver\Sources\LineMap;
122use Deriver\Deriver\Sources\Path;
123use Deriver\Deriver\Sources\Source;
124use Deriver\Deriver\Sources\SourceRef;
125use Deriver\Deriver\Sources\Sources;
126use Deriver\Exception\ParserException;
127use Deriver\Exception\ResolutionException;
128use Override;
129use PHPUnit\Framework\Attributes\CoversClass;
130use PHPUnit\Framework\Attributes\DataProvider;
131use PHPUnit\Framework\Attributes\Small;
132use PHPUnit\Framework\Attributes\UsesClass;
133use PHPUnit\Framework\TestCase;
134
135#[UsesClass(Resolver::class)]
136#[UsesClass(ExpressionValidation::class)]
137#[UsesClass(ResolutionException::class)]
138#[UsesClass(ParserConfig::class)]
139#[UsesClass(ParserException::class)]
140#[CoversClass(Lattice::class)]
141#[UsesClass(QueryExecution::class)]
142#[UsesClass(QueryValidation::class)]
143#[UsesClass(ResultAssessment::class)]
144#[UsesClass(Deriver::class)]
145#[UsesClass(Constraints::class)]
146#[UsesClass(BasicBlock::class)]
147#[UsesClass(CallableGraph::class)]
148#[UsesClass(CallableIdentity::class)]
149#[UsesClass(Instruction::class)]
150#[UsesClass(Parameter::class)]
151#[UsesClass(Terminator::class)]
152#[UsesClass(ArgumentBinding::class)]
153#[UsesClass(ArgumentOrder::class)]
154#[UsesClass(Dispatch::class)]
155#[UsesClass(ParameterBinding::class)]
156#[UsesClass(TypeBinding::class)]
157#[UsesClass(TypeCheck::class)]
158#[UsesClass(Completion::class)]
159#[UsesClass(Context::class)]
160#[UsesClass(LoopConvergence::class)]
161#[UsesClass(ObservationLimit::class)]
162#[UsesClass(StateJoin::class)]
163#[UsesClass(Unwinding::class)]
164#[UsesClass(Cell::class)]
165#[UsesClass(Components::class)]
166#[UsesClass(Discovery::class)]
167#[UsesClass(Key::class)]
168#[UsesClass(Table::class)]
169#[UsesClass(Dependencies::class)]
170#[UsesClass(InstructionTransfer::class)]
171#[UsesClass(Evaluator::class)]
172#[UsesClass(SlotReference::class)]
173#[UsesClass(ObservationCollector::class)]
174#[UsesClass(Conversions::class)]
175#[UsesClass(ScalarErrors::class)]
176#[UsesClass(State::class)]
177#[UsesClass(CompletionRecord::class)]
178#[UsesClass(Evaluation::class)]
179#[UsesClass(Invocation::class)]
180#[UsesClass(Isolation::class)]
181#[UsesClass(CompoundAssignment::class)]
182#[UsesClass(MemoryStep::class)]
183#[UsesClass(PureStep::class)]
184#[UsesClass(ReferenceAssignment::class)]
185#[UsesClass(Location::class)]
186#[UsesClass(Materialization::class)]
187#[UsesClass(Memory::class)]
188#[UsesClass(ReferenceConstraint::class)]
189#[UsesClass(StorageCapture::class)]
190#[UsesClass(DomainFact::class)]
191#[UsesClass(DomainOperations::class)]
192#[UsesClass(Extensions::class)]
193#[UsesClass(ProviderExpansion::class)]
194#[UsesClass(Evaluators::class)]
195#[UsesClass(StateRegistry::class)]
196#[UsesClass(DeriverConfig::class)]
197#[UsesClass(EntryPoint::class)]
198#[UsesClass(Sources::class)]
199#[UsesClass(Path::class)]
200#[UsesClass(Snapshot::class)]
201#[UsesClass(Source::class)]
202#[UsesClass(TargetProfile::class)]
203#[UsesClass(Budget::class)]
204#[UsesClass(QueryScope::class)]
205#[UsesClass(ReturnQuery::class)]
206#[UsesClass(ResultRef::class)]
207#[UsesClass(SourceRef::class)]
208#[UsesClass(Alternative::class)]
209#[UsesClass(Assessment::class)]
210#[UsesClass(Derivation::class)]
211#[UsesClass(DerivationResult::class)]
212#[UsesClass(Frontier::class)]
213#[UsesClass(QueryEncoding::class)]
214#[UsesClass(ValueGraph::class)]
215#[UsesClass(Statistics::class)]
216#[UsesClass(StorageSnapshot::class)]
217#[UsesClass(Parser::class)]
218#[UsesClass(File::class)]
219#[UsesClass(AssignmentLowering::class)]
220#[UsesClass(Lowerer::class)]
221#[UsesClass(DestructuringLowering::class)]
222#[UsesClass(LoopLowering::class)]
223#[UsesClass(EffectInspection::class)]
224#[UsesClass(ExpressionLowering::class)]
225#[UsesClass(InstructionEmitter::class)]
226#[UsesClass(LoweringScope::class)]
227#[UsesClass(StatementLowering::class)]
228#[UsesClass(CallableSource::class)]
229#[UsesClass(Indexer::class)]
230#[UsesClass(Index::class)]
231#[UsesClass(Composition::class)]
232#[UsesClass(LineMap::class)]
233#[UsesClass(MagicContext::class)]
234#[UsesClass(AssignmentPatterns::class)]
235#[UsesClass(ClassScope::class)]
236#[UsesClass(TargetSyntax::class)]
237#[UsesClass(Arithmetic::class)]
238#[UsesClass(Comparison::class)]
239#[UsesClass(Identity::class)]
240#[UsesClass(Increment::class)]
241#[UsesClass(Operations::class)]
242#[UsesClass(Projection::class)]
243#[UsesClass(StringPrefix::class)]
244#[UsesClass(Term::class)]
245#[Small]
246final class LatticeTest extends TestCase
247{
248 public function testTypePreservesTheSemanticContract(): void
249 {
250 $source = '<?php function target(int $n){$s="";for($i=0;$i<$n;$i++){$s.="x";}return $s;}';
251 $symbol = 'target';
252 $input = new Sources([new Source('fixture.php', $source)]);
253 $configuration = new DeriverConfig();
254 $contributions = new Contributions();
255 $target = new TargetProfile($configuration->phpVersion, $configuration->integerBits, $configuration->floatPrecision);
256 $providers = new ProviderExpansion($input, array_map(Term::fromNative(...), $configuration->environment), $contributions);
257 $contributions1 = $providers->contributions;
258 $evaluators = new Evaluators(new TargetProfile($configuration->phpVersion, $configuration->integerBits, $configuration->floatPrecision), new Registrations($contributions1->evaluators, $contributions1->providers, $contributions1->domains, $contributions1->intrinsics, $contributions1->stateSlots), $configuration->standardEvaluators);
259 $settings = new EvaluatorConfig($target, $providers->environment, $configuration->standardEvaluators, array_map((new MicroEvaluatorConversion())->convert(...), $configuration->evaluators));
260 $identity = new SnapshotIdentity($providers->input, $settings, $evaluators, $providers->manifest);
261 $snapshotId = $identity->id;
262 $input1 = $providers->input;
263 $parser = new Parser(new ParserConfig($target->version));
264 $trees = array_map(static fn (Source $source1): File => (new Resolver())->resolve($parser->parse(new Source(Path::normalize($source1->path), $source1->contents, $source1->declarationsOnly))), iterator_to_array($input1, false));
265 $program = new Index($snapshotId, $trees);
266 $result = (new QueryExecution($program, new ExecutionEvaluatorConfig($target, $providers->environment, $configuration->standardEvaluators), $evaluators, $identity->snapshot(array_map(Frontier::fromDiagnostic(...), $program->diagnostics()))))->derive(new ReturnQuery($symbol));
267 self::assertSame(DependencyClosure::Closed, $result->assessment->closure);
268 self::assertSame(ValuePrecision::Abstract, $result->assessment->precision);
269 self::assertSame('WIDENED', $result->frontiers[0]->code);
270 self::assertSame(Enumeration::NotEnumerated, $result->assessment->enumeration);
271 }
272 public function testContainsRespectsOpaqueTypeBounds(): void
273 {
274 $lattice = new Lattice();
275 self::assertFalse($lattice->contains(Term::opaque('boundary', 'int'), Term::constant('a')));
276 self::assertTrue($lattice->contains(Term::opaque('boundary', 'int'), Term::constant(1)));
277 }
278 public function testWidenContainsBothDifferentConstants(): void
279 {
280 $lattice = new Lattice();
281 $joined = $lattice->widen(Term::constant(1), Term::constant(2));
282 self::assertSame(TermKind::Abstract, $joined->kind);
283 self::assertTrue($lattice->contains($joined, Term::constant(1)));
284 self::assertTrue($lattice->contains($joined, Term::constant(2)));
285 }
286 public function testCompatibleRequiresKnownFieldsEvenWhenTheArrayHasAnUnknownRemainder(): void
287 {
288 $upper = Term::array(['required' => Term::constant(1)], true);
289 $lattice = new Lattice();
290 self::assertFalse($lattice->compatible($upper, Term::array([])));
291 self::assertTrue($lattice->compatible($upper, Term::fromNative(['required' => 1, 'other' => 2])));
292 }
293 public function testContainsSharesRepeatedArraySubgraphObligations(): void
294 {
295 $depth = 30;
296 $leaf = Term::constant(1);
297 $leaf = array_reduce(array_fill(0, $depth, null), static fn (Term $leaf): Term => Term::array([$leaf, $leaf]), $leaf);
298 $upper = $leaf;
299 $depth1 = 30;
300 $leaf1 = Term::constant(1);
301 $leaf1 = array_reduce(array_fill(0, $depth1, null), static fn (Term $leaf1): Term => Term::array([$leaf1, $leaf1]), $leaf1);
302 $lower = $leaf1;
303 $lattice = new Lattice();
304 self::assertTrue($lattice->contains($upper, $lower));
305 self::assertFalse($lattice->contains($upper, Term::array([])));
306 }
307 public function testContainsPreservesKnownKeyOrderInsideAnOpenShape(): void
308 {
309 $upper = Term::array(['a' => Term::constant(1), 'b' => Term::constant(2)], true);
310 self::assertFalse((new Lattice())->contains($upper, Term::fromNative(['b' => 2, 'a' => 1])));
311 }
312 public function testCompatibleDoesNotConfuseDomainIdentityWithAStringConstant(): void
313 {
314 $domain = new class () implements AbstractDomain {
315 /**
316 * @return string Domain identity
317 */
318 #[Override]
319 public function id(): string
320 {
321 return 'example.policy';
322 }
323 /**
324 * @return string Semantic version
325 */
326 #[Override]
327 public function version(): string
328 {
329 return '1';
330 }
331 /**
332 * @return DomainFact Empty set
333 */
334 #[Override]
335 public function bottom(): DomainFact
336 {
337 return new DomainFact($this->id(), new Term(TermKind::Bottom));
338 }
339 /**
340 * @return DomainFact All policy records
341 */
342 #[Override]
343 public function top(): DomainFact
344 {
345 return new DomainFact($this->id(), new Term(TermKind::Top));
346 }
347 /**
348 * @param DomainFact $a Contained fact
349 * @param DomainFact $b Containing fact
350 * @return bool Flat-lattice inclusion
351 */
352 #[Override]
353 public function lessOrEqual(DomainFact $a, DomainFact $b): bool
354 {
355 return $a->representation->kind === TermKind::Bottom || $b->representation->kind === TermKind::Top || $a->representation->isConcrete() && $b->representation->isConcrete() && $a->representation->native() === $b->representation->native();
356 }
357 /**
358 * @param DomainFact $a First possibility
359 * @param DomainFact $b Second possibility
360 * @return DomainFact Inclusive alternative
361 */
362 #[Override]
363 public function join(DomainFact $a, DomainFact $b): DomainFact
364 {
365 if ($this->lessOrEqual($a, $b)) {
366 return $b;
367 }
368 return $this->lessOrEqual($b, $a) ? $a : $this->top();
369 }
370 /**
371 * @param DomainFact $previous Previous approximation
372 * @param DomainFact $next New approximation
373 * @return DomainFact Finite widening
374 */
375 #[Override]
376 public function widen(DomainFact $previous, DomainFact $next): DomainFact
377 {
378 return $this->join($previous, $next);
379 }
380 /**
381 * @param DomainFact $value Policy record
382 * @param Projection $projection Selected fields
383 * @return DomainFact Projected fact
384 */
385 #[Override]
386 public function project(DomainFact $value, Projection $projection): DomainFact
387 {
388 $term = $value->representation;
389 foreach ($projection->path as $key) {
390 $term = $term->operands[$key] ?? new Term(TermKind::Top);
391 }
392 return new DomainFact($this->id(), $term);
393 }
394 };
395 $top = $domain->top()->term();
396 $lattice = new Lattice([$domain->id() => $domain]);
397 self::assertFalse($lattice->contains($top, Term::constant($domain->id())));
398 self::assertTrue($lattice->contains($lattice->widen($top, Term::constant($domain->id())), Term::constant($domain->id())));
399 }
400 #[DataProvider('providerTypes')]
401 public function testTypeReturnsConservativeBoundsForEveryValueCategory(Term $value, string $expected): void
402 {
403 self::assertSame($expected, (new Lattice())->type($value));
404 }
405 /**
406 * @return array<string,array{Term,string}>
407 */
408 public static function providerTypes(): array
409 {
410 return ['int' => [Term::constant(1), 'int'], 'float' => [Term::constant(1.5), 'float'], 'bool' => [Term::constant(false), 'bool'], 'string' => [Term::constant('a'), 'string'], 'null' => [Term::constant(null), 'null'], 'array' => [Term::array([]), 'array'], 'object' => [new Term(TermKind::Object, 'id'), 'object'], 'closure' => [new Term(TermKind::Closure, 'id'), 'object'], 'enum' => [new Term(TermKind::Enum, 'id'), 'object'], 'concat' => [new Term(TermKind::Concat), 'string'], 'arithmetic' => [new Term(TermKind::Binary, '+'), 'int|float'], 'array union' => [new Term(TermKind::Binary, '+', attributes: ['type' => 'array']), 'array'], 'comparison' => [new Term(TermKind::Binary, '===', attributes: ['type' => 'bool']), 'bool'], 'declared union' => [Term::parameter('x', 'int|string'), 'int|string'], 'unbounded' => [new Term(TermKind::External, 'x'), 'mixed'], 'malformed bound' => [new Term(TermKind::External, 'x', attributes: ['type' => 42]), 'mixed']];
411 }
412 #[DataProvider('providerInclusion')]
413 public function testContainsPreservesDirectionAndCachesCompleteChildObligations(Term $upper, Term $lower, bool $expected): void
414 {
415 $lattice = new Lattice();
416 $first = $lattice->contains($upper, $lower);
417 $cached = $lattice->contains($upper, $lower);
418 self::assertSame($expected, $first);
419 self::assertSame($expected, $cached);
420 }
421 /**
422 * @return array<string,array{Term,Term,bool}>
423 */
424 public static function providerInclusion(): array
425 {
426 return ['top' => [Term::opaque('unknown'), Term::fromNative(['x' => 1]), true], 'union accepts member' => [Term::opaque('unknown', 'int|string'), Term::constant(1), true], 'union rejects other member' => [Term::opaque('unknown', 'int|string'), Term::constant(null), false], 'narrow rejects union' => [Term::opaque('unknown', 'int'), Term::parameter('x', 'int|string'), false], 'abstract bound' => [new Term(TermKind::Abstract, attributes: ['type' => 'int']), Term::constant(1), true], 'constant equal' => [Term::constant(1), Term::constant(1), true], 'constant different' => [Term::constant(1), Term::constant(2), false], 'constant type distinct' => [Term::constant(1), Term::constant(1.0), false], 'exact input' => [Term::parameter('x', 'int'), Term::parameter('x', 'int'), true], 'independent inputs' => [Term::parameter('x', 'int'), Term::parameter('y', 'int'), false], 'closed keys cannot expand' => [Term::array([]), Term::fromNative([1]), false], 'closed cannot contain open' => [Term::array([]), Term::array([], true), false], 'open admits suffix' => [Term::array(['x' => Term::constant(1)], true), Term::fromNative(['x' => 1, 'y' => 2]), true], 'open admits unknown remainder' => [Term::array(['x' => Term::constant(1)], true), Term::array(['x' => Term::constant(1)], true), true], 'required key cannot disappear' => [Term::array(['x' => Term::constant(1)], true), Term::array([], true), false], 'nested member' => [Term::array(['x' => Term::opaque('bound', 'int')]), Term::fromNative(['x' => 4]), true], 'nested mismatch' => [Term::array(['x' => Term::opaque('bound', 'int')]), Term::fromNative(['x' => 'no']), false], 'known key order' => [Term::fromNative(['a' => 1, 'b' => 2]), Term::fromNative(['b' => 2, 'a' => 1]), false], 'object identity' => [new Term(TermKind::Object, 'a'), new Term(TermKind::Object, 'b'), false]];
427 }
428 #[DataProvider('providerWidening')]
429 public function testWidenIncludesBothInputsWithStableUnionBounds(Term $a, Term $b, string $type): void
430 {
431 $lattice = new Lattice();
432 $result = $lattice->widen($a, $b);
433 self::assertSame(TermKind::Abstract, $result->kind);
434 self::assertSame('WIDENED', $result->literal);
435 self::assertSame($type, $result->attributes['type']);
436 self::assertTrue($lattice->contains($result, $a));
437 self::assertTrue($lattice->contains($result, $b));
438 }
439 /**
440 * @return array<string,array{Term,Term,string}>
441 */
442 public static function providerWidening(): array
443 {
444 return ['integers' => [Term::constant(1), Term::constant(2), 'int|float'], 'floats' => [Term::constant(1.5), Term::constant(2.5), 'int|float'], 'mixed numeric' => [Term::constant(1), Term::constant(2.5), 'int|float'], 'strings' => [Term::constant('a'), Term::constant('b'), 'string'], 'sorted union' => [Term::constant('a'), Term::constant(false), 'bool|string'], 'unbounded' => [Term::constant(1), Term::parameter('x'), 'mixed']];
445 }
446 public function testWidenKeepsTheSharedPrefixOfStrings(): void
447 {
448 $lattice = new Lattice();
449 $widened = $lattice->widen(Term::constant('SELECT * FROM t WHERE 1'), Term::constant('SELECT * FROM t WHERE 1 AND c = ?'));
450 self::assertSame(TermKind::Concat, $widened->kind);
451 self::assertSame('SELECT * FROM t WHERE 1', $widened->operands[0]->native());
452 self::assertSame('string', $lattice->type($widened));
453 self::assertTrue($lattice->contains($widened, Term::constant('SELECT * FROM t WHERE 1')));
454 self::assertTrue($lattice->contains($widened, Term::constant('SELECT * FROM t WHERE 1 AND c = ? AND c = ?')));
455 self::assertFalse($lattice->contains($widened, Term::constant('SELECT 1')));
456 self::assertFalse($lattice->contains($widened, Term::parameter('x', 'string')));
457 $next = new Term(TermKind::Concat, operands: [$widened, Term::constant(' AND d')], attributes: ['type' => 'string']);
458 self::assertSame($widened, $lattice->widen($widened, $next));
459 self::assertSame('WIDENED', $lattice->widen($widened, Term::constant('DELETE'))->literal);
460 }
461 public function testWidenPreservesAnExistingUpperBoundIdentity(): void
462 {
463 $upper = Term::opaque('known-bound', 'int|string');
464 self::assertSame($upper, (new Lattice())->widen($upper, Term::constant('x')));
465 }
466 public function testWidenUsesRegisteredDomainLaws(): void
467 {
468 $domain = new class () implements AbstractDomain {
469 /**
470 * @return string Domain identity
471 */
472 #[Override]
473 public function id(): string
474 {
475 return 'example.policy';
476 }
477 /**
478 * @return string Semantic version
479 */
480 #[Override]
481 public function version(): string
482 {
483 return '1';
484 }
485 /**
486 * @return DomainFact Empty set
487 */
488 #[Override]
489 public function bottom(): DomainFact
490 {
491 return new DomainFact($this->id(), new Term(TermKind::Bottom));
492 }
493 /**
494 * @return DomainFact All policy records
495 */
496 #[Override]
497 public function top(): DomainFact
498 {
499 return new DomainFact($this->id(), new Term(TermKind::Top));
500 }
501 /**
502 * @param DomainFact $a Contained fact
503 * @param DomainFact $b Containing fact
504 * @return bool Flat-lattice inclusion
505 */
506 #[Override]
507 public function lessOrEqual(DomainFact $a, DomainFact $b): bool
508 {
509 return $a->representation->kind === TermKind::Bottom || $b->representation->kind === TermKind::Top || $a->representation->isConcrete() && $b->representation->isConcrete() && $a->representation->native() === $b->representation->native();
510 }
511 /**
512 * @param DomainFact $a First possibility
513 * @param DomainFact $b Second possibility
514 * @return DomainFact Inclusive alternative
515 */
516 #[Override]
517 public function join(DomainFact $a, DomainFact $b): DomainFact
518 {
519 if ($this->lessOrEqual($a, $b)) {
520 return $b;
521 }
522 return $this->lessOrEqual($b, $a) ? $a : $this->top();
523 }
524 /**
525 * @param DomainFact $previous Previous approximation
526 * @param DomainFact $next New approximation
527 * @return DomainFact Finite widening
528 */
529 #[Override]
530 public function widen(DomainFact $previous, DomainFact $next): DomainFact
531 {
532 return $this->join($previous, $next);
533 }
534 /**
535 * @param DomainFact $value Policy record
536 * @param Projection $projection Selected fields
537 * @return DomainFact Projected fact
538 */
539 #[Override]
540 public function project(DomainFact $value, Projection $projection): DomainFact
541 {
542 $term = $value->representation;
543 foreach ($projection->path as $key) {
544 $term = $term->operands[$key] ?? new Term(TermKind::Top);
545 }
546 return new DomainFact($this->id(), $term);
547 }
548 };
549 $a = new DomainFact($domain->id(), Term::constant('a'));
550 $b = new DomainFact($domain->id(), Term::constant('b'));
551 $lattice = new Lattice([$domain->id() => $domain]);
552 $joined = $lattice->widen($a->term(), $b->term());
553 self::assertSame(TermKind::Domain, $joined->kind);
554 self::assertSame($domain->id(), $joined->literal);
555 self::assertTrue($lattice->contains($joined, $a->term()));
556 self::assertTrue($lattice->contains($joined, $b->term()));
557 self::assertFalse($lattice->contains($a->term(), $joined));
558 }
559 public function testWidenKeepsAnExistingContainingTypeBound(): void
560 {
561 $bound = new Term(TermKind::Abstract, 'WIDENED', attributes: ['type' => 'int|float']);
562 $input = Term::constant(4);
563 $lattice = new Lattice();
564 self::assertTrue($lattice->contains($bound, $input));
565 $joined = $lattice->widen($bound, $input);
566 self::assertSame($bound, $joined);
567 self::assertTrue($lattice->contains($joined, $bound));
568 }
569 public function testShapeChecksRequiredOrderAndUnknownRemainders(): void
570 {
571 $lattice = new Lattice();
572 $closed = Term::fromNative(['a' => 1]);
573 $open = Term::array(['a' => Term::constant(1)], true);
574 self::assertFalse($lattice->shape($closed, $open));
575 self::assertFalse($lattice->shape($open, Term::array([])));
576 self::assertTrue($lattice->shape($open, Term::fromNative(['a' => 1, 'b' => 2])));
577 self::assertFalse($lattice->shape(Term::fromNative(['a' => 1, 'b' => 2]), Term::fromNative(['b' => 2, 'a' => 1])));
578 }
579}
580