packages/deriver/src/Deriver/Evaluator/Execution/Control/ResidualPaths.php

1<?php
2
3declare(strict_types=1);
4
5namespace Deriver\Deriver\Evaluator\Execution\Control;
6
7use Deriver\Deriver\Evaluator\Execution\Completion\Completion;
8use Deriver\Deriver\Evaluator\Execution\Context;
9use Deriver\Deriver\Evaluator\Execution\Havoc;
10use Deriver\Deriver\Evaluator\Execution\State;
11use Deriver\Deriver\Evaluator\Term;
12use Deriver\Deriver\Sources\SourceRef;
13
14/**
15 * Seals unexplored execution with inclusive normal and exceptional completions.
16 * @visibility Deriver\Deriver\Evaluator
17 * @visibility Deriver\Deriver\Evaluator\Execution
18 */
19final class ResidualPaths
20{
21    /**
22     * @param Context $context Query budget and frontier records
23     */
24    public function __construct(public readonly Context $context)
25    {
26    }
27
28    /**
29     * Seals an invocation that is not entered, havocking only what the callee can reach, as for an unknown call.
30     * @param State $entry Bound callee entry, whose locals hold the arguments, captures, and receiver
31     * @param SourceRef $source Callee source
32     * @param string $operation Limit that refused the invocation
33     * @param string|null $reason Frontier code, defaulting to BUDGET_EXCEEDED
34     * @return list<State> Normal and exceptional residuals
35     */
36    public function invocation(State $entry, SourceRef $source, string $operation, ?string $reason = null): array
37    {
38        $reason ??= 'BUDGET_EXCEEDED';
39        $value = $this->context->frontier($reason, $source, $operation);
40        (new Havoc())->call($entry, [], array_values($entry->locals), $reason);
41        return $this->complete($entry, $value);
42    }
43
44    /**
45     * Keeps unexplored effects and exceptions when a logical limit interrupts execution.
46     * @param State $state Interrupted execution path
47     * @param SourceRef $source Interrupted source operation
48     * @param string $operation Limit or capability that stopped progress
49     * @param string|null $reason Frontier code, defaulting to BUDGET_EXCEEDED
50     * @return list<State> Normal and exceptional residuals
51     */
52    public function seal(State $state, SourceRef $source, string $operation, ?string $reason = null): array
53    {
54        $reason ??= 'BUDGET_EXCEEDED';
55        $value = $this->context->frontier($reason, $source, $operation);
56        (new Havoc())->symbols($state, $reason);
57        return $this->complete($state, $value);
58    }
59
60    /**
61     * Completes an already havocked path with a residual return and an unknown throwable.
62     * @param State $state Interrupted execution path
63     * @param Term $value Residual return value
64     * @return list<State> Normal and exceptional residuals
65     */
66    public function complete(State $state, Term $value): array
67    {
68        $state->constraints = [];
69        $state->completion = new Completion(\Deriver\Deriver\Evaluator\Execution\Completion\CompletionKind::Return, $value);
70        $exception = $state->fork();
71        $exception->completion = new Completion(\Deriver\Deriver\Evaluator\Execution\Completion\CompletionKind::Throw, new Term(\Deriver\Deriver\Evaluator\TermKind::Throwable, 'Throwable', attributes: ['uncertain' => true]));
72        return [$state, $exception];
73    }
74}
75