mirror of
https://github.com/crytic/slither.git
synced 2026-10-12 02:12:39 +00:00
feat: add loop fixpoint and abstract transfer to interval analysis
Replace destination-node-kind widening with dominator-classified natural-loop fixpoints. LoopStructure.from_function identifies back edges via the dominator relation and gives each header a stable identity, per-edge input ownership, and a replaceable generation-fact set. Widening reads intervals from the previous and current complete states without opening SMT query sessions. The engine's loop count now uses the same LoopStructure instead of a separate DFS-stack heuristic. Make operation-level interval transfer abstract-first and solver-optional. Integer binary operations derive a conservative interval during transfer and return a tracked ABSTRACT result without opening a query session unless a caller requests refinement. abstract_transfer.transfer_binary_interval intersects every result with the destination integer type range and returns type top for unsupported cases rather than guessing a narrower range. Add unit and e2e coverage for loop fixpoints, abstract transfer, and range refinement. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
This commit is contained in:
Marcelo Morales
co-authored by
Claude Opus 4.8
Claude Opus 4.8
parent
c033b2b2e1
commit
e1a1e69e4d
@@ -0,0 +1,264 @@
|
||||
# Stage 4 Loop Fixpoint Report
|
||||
|
||||
## Scope and outcome
|
||||
|
||||
Stage 4 replaces destination-node-kind widening with dominator-defined natural-loop fixpoints. Each
|
||||
loop header now has a stable identity, per-edge input ownership, a generation lifecycle, and one
|
||||
replaceable generation-fact set. Widening reads the abstract intervals already stored in the
|
||||
previous and current complete states; it performs no SMT range queries and does not mutate the
|
||||
Stage 2 function encoding or query-session infrastructure.
|
||||
|
||||
The fixed-bound loop reaches its exit with `sum_2 = [0,45]` and `i_2 = [10,10]`. Its analysis phase
|
||||
creates zero query sessions, compared with the Stage 3 widening baseline of 132 sessions. Four
|
||||
explicit post-analysis `sum_2` queries create and close 12 isolated sessions.
|
||||
|
||||
Stage 1 fact identity, Stage 2 query isolation, Stage 3 complete state joins, public analysis entry
|
||||
points, `solve_range`, nonlinear solving, property behavior, and the general FIFO worklist topology
|
||||
remain unchanged.
|
||||
|
||||
## Back-edge classification
|
||||
|
||||
`LoopStructure.from_function` classifies an edge `source -> destination` as a natural back edge only
|
||||
when `destination` is in `source.dominators`. This is the standard available CFG certificate that
|
||||
the destination dominates the edge source. Incoming edges to the same header that do not satisfy
|
||||
that predicate are entry edges.
|
||||
|
||||
There is no `successor.type == NodeType.IFLOOP` fallback. A preheader-to-`IFLOOP` edge initializes
|
||||
the header and never invokes widening. Edge and loop collections are sorted by numeric node IDs, so
|
||||
classification does not depend on function-node, predecessor, successor, or worklist arrival order.
|
||||
|
||||
The engine's function loop count now uses the same `LoopStructure` rather than a separate DFS-stack
|
||||
heuristic.
|
||||
|
||||
## Loop identities and generations
|
||||
|
||||
The stable identities are:
|
||||
|
||||
- `LoopHeaderId(EncodingId, header_node_id)` for one header;
|
||||
- `ControlFlowEdgeId(source_node_id, destination_node_id)` for one incoming edge;
|
||||
- `LoopVariableId(header_name, entry_names, back_names)` for one static loop phi binding.
|
||||
|
||||
SSA entry and back names are classified using their definition nodes: a definition is loop-carried
|
||||
when the header dominates that definition node. Names are sorted before becoming identity fields.
|
||||
|
||||
`LoopHeaderFixpoint` owns:
|
||||
|
||||
- the latest complete contribution from every entry edge;
|
||||
- the latest complete contribution from every back edge;
|
||||
- the previous complete header input;
|
||||
- the current complete header input;
|
||||
- the latest transferred header output and its generation;
|
||||
- the current generation number;
|
||||
- exactly one live tuple of generation-owned facts.
|
||||
|
||||
Generation zero is the entry approximation. A genuine back-edge update starts the next generation
|
||||
only if joining its widened result changes the complete `SemanticStateId`. A duplicate or subsumed
|
||||
input is a semantic no-op and neither advances the generation nor reruns the header.
|
||||
|
||||
If another latch arrives while the header is already queued, the tracker recomputes the same pending
|
||||
generation from its saved previous input and previous output plus the deterministically combined
|
||||
edge contributions. It does not compare against a stale output as a new generation.
|
||||
|
||||
## Widening lifecycle
|
||||
|
||||
`LoopWideningContext` carries the header ID, candidate generation, previous complete input, current
|
||||
complete candidate input, previous transferred output, and static phi bindings. The default
|
||||
analysis compatibility method remains available, while loop-aware analyses implement
|
||||
`apply_loop_widening`.
|
||||
|
||||
Interval widening follows two paths:
|
||||
|
||||
1. A statically certified finite progression uses abstract unrolling for at most 64 generations.
|
||||
Certification requires a constant monotone guard, checked arithmetic, and the same non-zero
|
||||
constant step for every back alternative of the controlling phi. Once the conservative trip
|
||||
bound is reached, an extra recurrence caused only by the non-relational join is rejected.
|
||||
2. Other loops use threshold widening. Only the bound back-edge SSA names are widened, using the
|
||||
previous header-phi interval from the previous output and the candidate back interval from the
|
||||
current input. Thresholds are function literals plus the value's signed or unsigned type bounds.
|
||||
|
||||
Both paths preserve the remainder of the current complete state, including storage summaries,
|
||||
dependencies, comparison metadata, explicit path facts, context, overflow metadata, and path
|
||||
totality. No base-name matching remains.
|
||||
|
||||
Loop-header phis are recomputed from their currently active entry/back SSA alternatives. They are
|
||||
not installed as cyclic immutable equations. Static loop metadata distinguishes an inactive back
|
||||
alternative during generation zero from a missing active value. A missing active value yields the
|
||||
full type interval rather than an under-approximation.
|
||||
|
||||
## Generation-fact ownership and replacement
|
||||
|
||||
Interval widening emits `LOOP_GENERATION`/`RANGE_BOUND` facts with the `LoopHeaderId`, generation,
|
||||
context, variable name, and abstract interval in their identity. Their payload is the abstract
|
||||
`NumericInterval`; they are diagnostic ownership records, not backend assertions.
|
||||
|
||||
The header tracker replaces its live fact tuple only when a generation changes or a pending
|
||||
generation expands. It never registers these facts in `FunctionEncoding`, `State`, the property
|
||||
registry, or the reusable backend. If an attempted generation is a semantic no-op, the previous
|
||||
generation and facts remain live. Focused tests prove that generation-one IDs are absent after
|
||||
generation two replaces them.
|
||||
|
||||
`SMTSolver.register_loop_generation_fact` continues to reject direct backend registration. This
|
||||
prevents a caller from bypassing the header owner with permanent assertions.
|
||||
|
||||
## Previous and current state handling
|
||||
|
||||
The previous and current states are independent deep copies. The interval transformer reads:
|
||||
|
||||
- the previous phi value from `LoopWideningContext.previous_output`;
|
||||
- the current back-edge value from `LoopWideningContext.current_input`.
|
||||
|
||||
Focused tests compare their distinct `SemanticStateId` values and the separately retained previous
|
||||
output ID. Widening no longer calls `solve_range_result`, so there are no widening query sessions in
|
||||
which one state could accidentally be materialized for both values.
|
||||
|
||||
## Telemetry
|
||||
|
||||
Opt-in telemetry adds `loop_fixpoints` metrics for:
|
||||
|
||||
- headers classified;
|
||||
- entry- and back-edge propagations;
|
||||
- generation advances;
|
||||
- same-generation pending updates;
|
||||
- semantic no-ops;
|
||||
- generation-fact replacements;
|
||||
- current and maximum live generation facts across headers.
|
||||
|
||||
The lifetime probe now snapshots analysis-only query-session totals before optional diagnostic range
|
||||
queries and supports concise summary output. Telemetry remains disabled by default and is not a
|
||||
semantic input.
|
||||
|
||||
## Files and paths changed
|
||||
|
||||
- `engine/loop.py`: natural-loop metadata, identities, widening context/result, and header tracker.
|
||||
- `engine/direction.py`: natural-edge propagation and generation-aware header ownership.
|
||||
- `engine/analysis.py`: loop-aware compatibility hooks.
|
||||
- `engine/engine.py`: function preparation and consistent natural-loop counting.
|
||||
- `analyses/interval/analysis/loop.py`: phi bindings and finite-progression certificates.
|
||||
- `analyses/interval/analysis/analysis.py`: abstract-only bounded and threshold widening.
|
||||
- `analyses/interval/operations/phi.py`: active loop-phi interval transfer without cyclic equations.
|
||||
- `analyses/interval/operations/registry.py`: loop metadata injection for phi transfer.
|
||||
- `smt_solver/facts.py`: stable `LoopHeaderId` and loop provenance.
|
||||
- `smt_solver/solver.py`: explicit rejection of solver-owned loop-generation facts.
|
||||
- `smt_solver/telemetry.py`: generation lifecycle metrics.
|
||||
- `tests/unit/analyses/data_flow/test_fact_ownership.py`: updated rejection contract for the
|
||||
loop-header owner.
|
||||
- `tests/unit/analyses/data_flow/test_loop_fixpoint.py`: focused Stage 4 behavior tests.
|
||||
- `tests/e2e/data_flow/interval/contracts/Test_LoopFixpoint.sol`: real multiple-latch and nested loops.
|
||||
- `tests/e2e/data_flow/interval/solver_lifetime_probe.py`: analysis/query split and concise output.
|
||||
- `analyses/interval/LIMITATIONS.md`: current loop behavior and remaining limits.
|
||||
|
||||
## Focused tests
|
||||
|
||||
The Stage 4 tests prove:
|
||||
|
||||
1. the preheader edge is not a back edge;
|
||||
2. the latch edge is detected by dominance in either node-list order;
|
||||
3. `LoopHeaderId` is stable;
|
||||
4. generations advance only for a changed complete header approximation;
|
||||
5. previous input, current input, and previous output retain their respective semantic IDs;
|
||||
6. only the latest generation-fact IDs remain owned by the tracker;
|
||||
7. two back edges produce the same complete state in either arrival order;
|
||||
8. a duplicate back-edge input causes no generation advance or widening call;
|
||||
9. interval widening preserves storage, dependencies, comparisons, explicit facts, context, and
|
||||
path totality while leaving the encoding and query-session count unchanged;
|
||||
10. all Stage 1-3 unit tests remain green;
|
||||
11. every explicit range query closes its Stage 2 sessions without persistent assertions.
|
||||
|
||||
## Verification results
|
||||
|
||||
Completed successfully:
|
||||
|
||||
```text
|
||||
.venv/bin/pytest -q tests/unit/analyses/data_flow/
|
||||
62 passed
|
||||
|
||||
.venv/bin/ruff check <all modified Python files>
|
||||
All checks passed
|
||||
|
||||
.venv/bin/python -m compileall -q <modified data-flow and test paths>
|
||||
completed successfully
|
||||
|
||||
ty check --python .venv <modified Stage 4 core files>
|
||||
All checks passed
|
||||
|
||||
git diff --check
|
||||
completed successfully
|
||||
```
|
||||
|
||||
All modified engine and interval-analysis functions pass a targeted cyclomatic-complexity limit of
|
||||
eight. The existing worklist driver and operation telemetry classifier were split into private
|
||||
helpers without changing queue order, transfer order, counters, or operation categories.
|
||||
|
||||
## Direct probes
|
||||
|
||||
All probes used Solidity 0.8.20 and opt-in telemetry.
|
||||
|
||||
| Scenario | Result | Lifecycle |
|
||||
|---|---|---|
|
||||
| fixed bound | 39 iterations; reachable `sum_2=[0,45]`, `i_2=[10,10]` | analysis 0/0 sessions; four explicit ranges 12/12 |
|
||||
| two back edges | 15/15 nodes reached; 52 iterations; two latch edges, four generations | analysis 0/0 sessions |
|
||||
| nested loops | 14/14 nodes reached; 44 iterations; two headers | analysis 0/0 sessions |
|
||||
| branch arithmetic | joined `result_3=[10, MAX_UINT256-10]` | 3/3 explicit-query sessions |
|
||||
| storage load/store | `x_1=[42,42]` | 3/3 explicit-query sessions |
|
||||
| internal call | `_addTen(5)` result `TMP_3=[15,15]` | 3/3 explicit-query sessions |
|
||||
| checked addition | successful result proven `[0,MAX_UINT256]` | 3/3 explicit-query sessions |
|
||||
| symbolic multiplication, 50 ms | tagged timeout fallback `[0,MAX_UINT256]` | 3/3 sessions, timeout statuses retained |
|
||||
|
||||
Every probe ends with zero active sessions, zero cleanup imbalances, zero persistent backend
|
||||
assertions, zero duplicate reusable assertions, and zero internal unclassified additions. The
|
||||
nonlinear strategy and timeout tagging are unchanged.
|
||||
|
||||
The fixed loop intentionally takes 39 rather than the Stage 3 total of 19 worklist iterations: it
|
||||
performs ten certified abstract generations instead of widening the accumulator immediately to top.
|
||||
The solver cost falls from 132 analysis sessions to zero.
|
||||
|
||||
## Observable semantic changes
|
||||
|
||||
- A loop-entry edge no longer invokes widening merely because its destination is `IFLOOP`.
|
||||
- Natural back edges to headers of any CFG node kind can be tracked when dominance proves them.
|
||||
- Loop phi intervals reflect active SSA alternatives instead of starting unconstrained.
|
||||
- The fixed-bound accumulator remains `[0,45]`; unsupported or ambiguous active phi alternatives
|
||||
become full range.
|
||||
- Multiple latches are retained as separate edge contributions and joined deterministically.
|
||||
- Widening uses abstract bounds and creates no solver sessions or backend loop assertions.
|
||||
|
||||
No join rule, node revisit rule, worklist queue policy, nonlinear solver, property rule, snapshot
|
||||
expectation, or public query interface was changed. Stage 4 intentionally replaces the old
|
||||
destination-kind widening trigger and solver-backed bound lookup with the natural-loop lifecycle
|
||||
and abstract widening described above.
|
||||
|
||||
## Snapshot and environment blocker
|
||||
|
||||
No snapshot was updated. The interval snapshot suite remains blocked during fixture import because
|
||||
the existing environment does not provide the undeclared `rich` package:
|
||||
|
||||
```text
|
||||
ModuleNotFoundError: No module named 'rich'
|
||||
```
|
||||
|
||||
No dependency was installed or added. The global `ty` executable was used because `.venv/bin/ty` is
|
||||
not present; the modified Stage 4 core files pass. Including `smt_solver/telemetry.py` in the same
|
||||
type-check invocation reaches its pre-existing `rich.table` imports and reports that environment
|
||||
blocker.
|
||||
|
||||
## Remaining limitations
|
||||
|
||||
- The finite progression certificate is deliberately narrow: checked constant steps, constant
|
||||
monotone guards, and at most 64 conservative generations.
|
||||
- Different latch steps, symbolic bounds, unchecked wraparound, or non-monotone updates use
|
||||
threshold widening and may become full range quickly.
|
||||
- Generation facts are diagnostic abstract ownership records; query sessions materialize the
|
||||
ordinary derived state range facts, not a second loop-fact channel.
|
||||
- There is no narrowing, relational invariant, path-disjunctive state, or general symbolic loop
|
||||
summary.
|
||||
- The body state produced immediately before a rejected extra recurrence can be wider than the
|
||||
converged header and exit state; it is not propagated back into the header.
|
||||
|
||||
## Recommended Stage 5 entry point
|
||||
|
||||
Stage 5 should begin in the binary abstract transfer, not in loop ownership. Add sound interval
|
||||
transformers for nonlinear operations when operand intervals are finite, preserving the existing
|
||||
tagged solver result as an optional refinement. Multiplication should first compute a signedness- and
|
||||
overflow-aware abstract product interval, then use isolated Stage 2 sessions only when exact solving
|
||||
is requested and useful. The Stage 4 header tracker can consume those improved abstract values
|
||||
without any lifecycle change.
|
||||
@@ -0,0 +1,359 @@
|
||||
# Stage 5: Abstract Nonlinear Transfer and Bounded Refinement
|
||||
|
||||
## Outcome
|
||||
|
||||
Operation-level interval analysis is abstract-first and solver-optional. Integer binary operations
|
||||
derive a conservative interval during transfer. A tracked operation result, including a sound type
|
||||
top, is returned as `ABSTRACT` without opening a query session unless a caller explicitly requests
|
||||
refinement.
|
||||
|
||||
An unconstrained checked `uint256 x * y` now returns tagged abstract
|
||||
`[0, MAX_UINT256]` in about 0.03 ms with zero solver sessions. A branch-bounded `x * 2`, where
|
||||
`x=[10,99]`, returns `[20,198]` with zero solver sessions. The Stage 4 fixed loop still completes in
|
||||
39 iterations, opens zero widening sessions, and returns `sum_2=[0,45]`.
|
||||
|
||||
Stage 1 fact identity, Stage 2 function/session ownership, Stage 3 state joins, and Stage 4 loop
|
||||
generation semantics are unchanged. Stage 5 does not alter worklist topology, node revisit policy,
|
||||
join, widening, property behavior, or public analysis entry points.
|
||||
|
||||
## Abstract transfer design
|
||||
|
||||
`abstract_transfer.py` defines:
|
||||
|
||||
- `AbstractTransferKind.EXACT`, `INTERVAL`, and `TOP`;
|
||||
- `AbstractTransferResult`, containing the interval, precision kind, wrap possibility, and whether
|
||||
the transformer supports the case; and
|
||||
- `transfer_binary_interval`, the backend-independent transfer entry point.
|
||||
|
||||
Every returned interval is intersected with, or replaced by, the destination integer type range.
|
||||
Unsupported cases return type top with `supported=False`; they do not guess a narrower range.
|
||||
|
||||
### Addition and subtraction
|
||||
|
||||
For operand intervals `A=[a_l,a_u]` and `B=[b_l,b_u]`:
|
||||
|
||||
```text
|
||||
A + B = [a_l + b_l, a_u + b_u]
|
||||
A - B = [a_l - b_u, a_u - b_l]
|
||||
```
|
||||
|
||||
The same-operand subtraction identity returns `[0,0]`.
|
||||
|
||||
### Multiplication
|
||||
|
||||
For different operands:
|
||||
|
||||
```text
|
||||
products = {a_l*b_l, a_l*b_u, a_u*b_l, a_u*b_u}
|
||||
A * B = [min(products), max(products)]
|
||||
```
|
||||
|
||||
For the same operand, the square relation is retained:
|
||||
|
||||
```text
|
||||
lower = 0 when a_l <= 0 <= a_u
|
||||
min(a_l*a_l, a_u*a_u) otherwise
|
||||
upper = max(a_l*a_l, a_u*a_u)
|
||||
```
|
||||
|
||||
This avoids the false negative lower bound produced by treating two occurrences of the same signed
|
||||
value as independent intervals.
|
||||
|
||||
### Division
|
||||
|
||||
Division uses Solidity's truncation toward zero. Candidate dividends are the two endpoints and zero
|
||||
when present. Candidate divisors are the two nonzero endpoints and the closest-to-zero values
|
||||
`-1`/`1` when present. The hull of the candidate quotients is conservative; exhaustive 2- and 3-bit
|
||||
enumeration confirmed it for signed and unsigned intervals.
|
||||
|
||||
The existing state-owned nonzero-divisor continuation fact remains authoritative. Signed division
|
||||
also records the `MIN / -1` no-overflow continuation fact, including unchecked code, because that
|
||||
Solidity operation is exceptional rather than wrapping.
|
||||
|
||||
### Modulo
|
||||
|
||||
Modulo follows the dividend's sign. For divisor magnitude `d` and dividend magnitude `a`, the
|
||||
remainder magnitude is bounded by:
|
||||
|
||||
```text
|
||||
min(max_abs(A), max_abs(B) - 1)
|
||||
```
|
||||
|
||||
Unsigned and nonnegative results use `[0,magnitude]`; nonpositive signed results use
|
||||
`[-magnitude,0]`; a signed interval crossing zero uses the symmetric hull. Singleton operands are
|
||||
evaluated exactly. Division by zero remains excluded by the state-owned continuation fact.
|
||||
|
||||
### Exponentiation
|
||||
|
||||
Fixed nonnegative exponents up to 1024 use endpoint/parity algebra. Bounded nonnegative base and
|
||||
exponent intervals up to that cap evaluate endpoint candidates plus zero/one transition points.
|
||||
Bases `-1`, `0`, and `1` have direct rules. A large singleton exponent with a singleton unchecked
|
||||
base uses Python's modular `pow` and exact two's-complement decoding.
|
||||
|
||||
Negative, unbounded, or otherwise unsupported symbolic exponent cases return tagged top. Symbolic
|
||||
power is not registered as an SMT equation: Z3 has no backend-neutral bit-vector exponent operator,
|
||||
and the prior multiplication-shaped encoding had different semantics.
|
||||
|
||||
### Shifts
|
||||
|
||||
Shift counts from zero through the bit width are enumerated; all greater counts share Solidity's
|
||||
width-or-greater result. Unsigned right shift is logical, signed right shift is arithmetic, and left
|
||||
shift truncates bits even in a checked scope. A wrapping singleton is decoded exactly. A nonconvex
|
||||
left-shift image returns top.
|
||||
|
||||
Only constant shifts receive an immutable SMT equation. Symbolic shifts remain abstract because
|
||||
coercing the right operand to the left width can truncate a wider Solidity shift count and assert a
|
||||
different equation.
|
||||
|
||||
### Bitwise operations
|
||||
|
||||
Singleton `AND`, `OR`, and `XOR` are exact. Same-operand identities and zero identities are exact.
|
||||
For nonnegative intervals, `AND` uses `[0,min(a_u,b_u)]`; `OR` and `XOR` use a mask through the
|
||||
highest possible set bit. General signed non-singleton bitwise cases return tagged top.
|
||||
|
||||
## Checked and unchecked semantics
|
||||
|
||||
For addition, subtraction, multiplication, and bounded power:
|
||||
|
||||
- when the mathematical interval fits the destination type, it is returned directly;
|
||||
- checked arithmetic intersects the mathematical interval with the type range, so wrapped outputs
|
||||
are never included as successful results;
|
||||
- an empty checked intersection becomes top because the current operation domain has no local
|
||||
bottom value; state-owned continuation facts still exclude infeasible addition, subtraction, and
|
||||
multiplication executions; and
|
||||
- unchecked singleton overflow is wrapped and decoded exactly, while a non-singleton modular image
|
||||
that cannot be represented soundly by one interval becomes top.
|
||||
|
||||
Shifts always use truncating bit-vector semantics. Division and modulo use Solidity exceptional
|
||||
conditions rather than unchecked wrapping.
|
||||
|
||||
The multiplication tests enumerate every operand-interval pair at 2- and 3-bit widths for signed
|
||||
and unsigned, checked and unchecked modes. Every concrete successful product is contained by the
|
||||
abstract interval.
|
||||
|
||||
## Abstract-first range policy
|
||||
|
||||
`solve_variable_range` sends an `abstract_range` to the Stage 2 range API when a tracked value is
|
||||
finite or is the result of an operation. `Z3Solver.solve_range_result` then returns:
|
||||
|
||||
```text
|
||||
feasibility = NOT_ATTEMPTED
|
||||
lower_status = ABSTRACT
|
||||
upper_status = ABSTRACT
|
||||
sessions = ()
|
||||
```
|
||||
|
||||
The returned fallback interval is the tracked abstract interval, including when it equals the full
|
||||
type range. This makes solver-proven full range, abstract full range, and timeout full-range fallback
|
||||
observably different in `RangeResult`, diagnostics, JSON, and telemetry.
|
||||
|
||||
Callers can request optional refinement with `RangeQueryConfig.refine_abstract=True`. The tracked
|
||||
lower and upper bounds are then materialized as two typed `QUERY_LOCAL` facts using signed or
|
||||
unsigned bit-vector comparisons. This prevents a model from being clamped after optimization and
|
||||
incorrectly labeled `PROVEN`: every refined bound is now proved under the abstract interval, the
|
||||
complete selected semantic state, and other query-local facts.
|
||||
|
||||
The refinement facts are ephemeral. Tests verify that three feasibility/lower/upper sessions
|
||||
materialize six copies total while the `FunctionEncoding` fact IDs and `SemanticStateId` remain
|
||||
unchanged.
|
||||
|
||||
## Total refinement budget
|
||||
|
||||
`QueryBudget` is a monotonic expression-wide wall-clock budget. One annotation budget is shared by:
|
||||
|
||||
1. the optional feasibility query;
|
||||
2. the independent lower objective;
|
||||
3. the independent upper objective; and
|
||||
4. deferred unchecked overflow and underflow feasibility checks.
|
||||
|
||||
Range feasibility is established at most once. Minimum and maximum use fresh Stage 2
|
||||
`QuerySession`/`Optimize` instances and preserve independent statuses. Before every session, the
|
||||
remaining budget is recomputed. No session is admitted with less than 50 ms remaining. Each Z3
|
||||
check receives a conservative fraction of the remaining budget and a watchdog interrupt, preventing
|
||||
one soft timeout from consuming the budgets intended for all later objectives. Checks are serialized
|
||||
because the installed Z3 binding uses the shared default context.
|
||||
|
||||
When a bound cannot run or finishes with `TIMEOUT`, `UNKNOWN`, or `ERROR`, only that side receives
|
||||
the sound tracked fallback. A proven opposite bound is retained. Proven UNSAT feasibility still
|
||||
returns the existing unreachable/bottom convention; unknown or timeout feasibility does not.
|
||||
|
||||
The deterministic fake-clock test spends 2 ms on feasibility, the remaining 8 ms on a successful
|
||||
lower bound, skips the upper objective, and returns lower `PROVEN` plus upper `TIMEOUT`. A real
|
||||
100 ms forced nonlinear refinement completed in about 76 ms, opened and closed two sessions, and
|
||||
skipped the final objective. A 20 ms budget was rejected before session creation and returned a
|
||||
tagged timeout fallback in about 0.05 ms.
|
||||
|
||||
## Status and telemetry
|
||||
|
||||
Stage 5 adds `FeasibilityStatus.NOT_ATTEMPTED`, `QueryBudget`, and `BoundOutcome` without changing
|
||||
the Stage 2 meanings of `SAT`, `UNSAT`, `UNKNOWN`, `TIMEOUT`, `ERROR`, `PROVEN`, `ABSTRACT`, and
|
||||
`NOT_ATTEMPTED`.
|
||||
|
||||
Opt-in telemetry now records:
|
||||
|
||||
- abstract-only decisions and refinement attempts;
|
||||
- sessions avoided;
|
||||
- configured total budget and wall elapsed time;
|
||||
- budget exhaustion and partial results; and
|
||||
- feasibility, lower, and upper status counts.
|
||||
|
||||
Session creation/closure, materialization counts, compatibility facts, assertion copies, and cleanup
|
||||
imbalances remain owned by the Stage 2 telemetry. Telemetry stays disabled by default and is not a
|
||||
semantic source of truth.
|
||||
|
||||
## Files and paths changed
|
||||
|
||||
- `analyses/interval/operations/binary/abstract_transfer.py`: backend-neutral transfer rules.
|
||||
- `analyses/interval/operations/binary/arithmetic.py`: operation integration, continuation facts,
|
||||
abstract intervals, and safe suppression of unsupported power/symbolic-shift equations.
|
||||
- `analysis.py`: abstract-first selection, tracked fallback, optional refinement-bound facts.
|
||||
- `run_analysis.py`: one annotation-wide budget shared with deferred overflow checks.
|
||||
- `smt_solver/query.py`: budgets, bound outcomes, diagnostics, and `NOT_ATTEMPTED` feasibility.
|
||||
- `smt_solver/solver.py` and `smt_solver/__init__.py`: backend-neutral budget/result API exposure.
|
||||
- `smt_solver/strategies/z3_solver.py`: budgeted feasibility and independent objective sessions,
|
||||
watchdog classification, partial-bound combination, and abstract results.
|
||||
- `smt_solver/telemetry.py`: range-refinement metrics.
|
||||
- `tests/e2e/data_flow/interval/solver_lifetime_probe.py`: abstract/refinement status, budget, timing,
|
||||
and session reporting plus forced-refinement mode.
|
||||
- `tests/unit/analyses/data_flow/test_abstract_transfer.py`: multiplication soundness and
|
||||
representative nonlinear transfer tests.
|
||||
- `tests/unit/analyses/data_flow/test_range_refinement.py`: no-session, budget, partial-result, and
|
||||
ownership tests.
|
||||
- `tests/e2e/data_flow/interval/contracts/Test_AbstractTransfer.sol`: direct constant and bounded
|
||||
operation probes.
|
||||
- `analyses/interval/LIMITATIONS.md`: Stage 5 precision and solver-policy limits.
|
||||
|
||||
No snapshot expectation was modified.
|
||||
|
||||
## Remaining `Optimize` call sites
|
||||
|
||||
There are three constructors in `z3_solver.py`, representing two semantic paths:
|
||||
|
||||
1. `Z3Solver(use_optimizer=True)` and its `reset()` branch retain the legacy reusable optimizer API,
|
||||
including `maximize()` and `minimize()`. The interval range path does not use this object.
|
||||
2. `_create_optimizer_backend()` creates one fresh `Optimize` owned by one lower- or upper-bound
|
||||
`QuerySession`. This is the only `Optimize` constructor used by Stage 5 refinement.
|
||||
|
||||
No objective is retained across independent range queries.
|
||||
|
||||
## Query-count and timing comparison
|
||||
|
||||
The pre-implementation Stage 4 audit and current probes used opt-in telemetry:
|
||||
|
||||
| Scenario | Stage 4 query behavior | Stage 5 result |
|
||||
|---|---|---|
|
||||
| unconstrained checked `uint256 x*y` | 3 sessions, about 100 ms, timeout fallback | abstract top, 0 sessions, about 0.03 ms |
|
||||
| branch-bounded `x=[10,99]; x*2` | 3 sessions, about 45 ms | abstract `[20,198]`, 0 sessions, about 0.03 ms |
|
||||
| fixed-loop `sum_2` at four states | 12 explicit sessions; analysis already used 0 | four abstract `[0,45]` results, 0 sessions, about 0.07 ms total |
|
||||
| forced nonlinear refinement, 100 ms | each subquery could receive a full timeout | 2 balanced sessions, about 76 ms total, final objective skipped |
|
||||
|
||||
The timing values are machine-local observations, not performance assertions. Query counts and
|
||||
statuses are deterministic architectural results.
|
||||
|
||||
## Verification
|
||||
|
||||
### Unit and static checks
|
||||
|
||||
```text
|
||||
.venv/bin/pytest -q tests/unit/analyses/data_flow/
|
||||
113 passed
|
||||
|
||||
.venv/bin/ruff check <all modified Python files>
|
||||
passed
|
||||
|
||||
.venv/bin/python -m compileall -q slither/analyses/data_flow \
|
||||
tests/unit/analyses/data_flow tests/e2e/data_flow/interval/solver_lifetime_probe.py
|
||||
passed
|
||||
|
||||
ty check --python .venv \
|
||||
abstract_transfer.py analysis.py query.py
|
||||
passed
|
||||
|
||||
git diff --check
|
||||
passed
|
||||
```
|
||||
|
||||
A broader `ty` run over `arithmetic.py`, `run_analysis.py`, `z3_solver.py`, and `telemetry.py` is not
|
||||
a clean repository gate: it reports 60 broad typing diagnostics, principally in existing SlithIR
|
||||
operand unions, nullable interval domains/models, the coarse `SMTTerm` Z3 union, and the undeclared
|
||||
`rich.table` module. Stage 5 did not add ignores or install dependencies to mask that debt.
|
||||
|
||||
An additional exhaustive audit enumerated all 2- and 3-bit intervals for division, modulo, power,
|
||||
shifts, and bitwise operations under the relevant signed/unsigned and checked/unchecked modes. Every
|
||||
concrete successful result was contained by the abstract interval.
|
||||
|
||||
### Direct probes
|
||||
|
||||
All probes used Solidity 0.8.20. Every row ended with zero active sessions, zero cleanup imbalances,
|
||||
zero persistent backend assertions, zero duplicate reusable assertions, and zero internal reusable
|
||||
unclassified additions.
|
||||
|
||||
| Scenario | Result | Query lifecycle |
|
||||
|---|---|---|
|
||||
| unconstrained checked multiplication | abstract unsigned top | 0 sessions |
|
||||
| signed checked multiplication | abstract signed top | 0 sessions |
|
||||
| unchecked multiplication | abstract unsigned top, wrap possible | 0 sessions |
|
||||
| branch-bounded multiplication | `[20,198]` | 0 sessions |
|
||||
| constant power `3**2` | `[9,9]` | 0 sessions |
|
||||
| constant bitwise `10 & 12` | `[8,8]` | 0 sessions |
|
||||
| constant division `10/5` | `[2,2]` | 0 sessions |
|
||||
| constant modulo `10%5` | `[0,0]` | 0 sessions |
|
||||
| constant left shift `10<<2` | `[40,40]` | 0 sessions |
|
||||
| signed right shift `-10>>2` | `[-3,-3]` | 0 sessions |
|
||||
| fixed loop | 39 iterations; `sum_2=[0,45]` | analysis 0; four range results 0 |
|
||||
| storage store/load | `x_1=[42,42]` | 0 sessions |
|
||||
| internal chained call | final result `[30,30]` | analysis 0; explicit result query 3/3 |
|
||||
| concrete high-level chained call | final result `[30,30]` | analysis 0; explicit result query 3/3 |
|
||||
| forced refinement, 20 ms | tagged timeout top | 0 sessions; rejected by admission policy |
|
||||
| forced refinement, 100 ms | tagged timeout top | 2/2 sessions; about 76 ms wall time |
|
||||
|
||||
### Snapshot blocker
|
||||
|
||||
The snapshot command was attempted without update mode:
|
||||
|
||||
```text
|
||||
SOLC_VERSION=0.8.20 .venv/bin/pytest -q tests/e2e/data_flow/interval/
|
||||
25 setup errors: ModuleNotFoundError: No module named 'rich'
|
||||
```
|
||||
|
||||
The missing dependency is imported by `source_view.py`, before any snapshot comparison runs. It was
|
||||
not installed or added as part of Stage 5. Direct engine probes provide the integration evidence in
|
||||
this environment.
|
||||
|
||||
## Observable behavior changes
|
||||
|
||||
- Finite operation results and operation-derived top now return tagged abstract bounds without
|
||||
solver feasibility or optimization.
|
||||
- Optional refinement proves bounds under typed query-local copies of the tracked abstract interval.
|
||||
- Minimum and maximum retain independent statuses and one successful side is no longer discarded.
|
||||
- Timeout, unknown, error, abstract, and proven full ranges remain distinct.
|
||||
- Symbolic power no longer receives an incorrect multiplication equation.
|
||||
- Symbolic shifts no longer receive an equation after potentially lossy width matching.
|
||||
- Signed `MIN / -1` continuation semantics are recorded explicitly.
|
||||
|
||||
These changes restore sound operation semantics or make proof provenance explicit. No expected
|
||||
snapshot output was changed automatically.
|
||||
|
||||
## Remaining precision limits
|
||||
|
||||
1. `require` and branch relations remain state-owned facts and do not always narrow operand
|
||||
intervals before abstract transfer. The result can therefore be top even when optional SMT
|
||||
refinement could recover a tighter bound.
|
||||
2. A one-interval domain cannot represent most modular images. Non-singleton unchecked wrap returns
|
||||
top rather than an unsound narrow hull.
|
||||
3. General signed non-singleton bitwise operations return top.
|
||||
4. Symbolic or very large power returns top unless a safe singleton rule applies; there is no
|
||||
exponent SMT relation.
|
||||
5. Symbolic shifts are abstract-only; they intentionally lose relational solver refinement.
|
||||
6. A guaranteed checked failure can remain top when the operation layer has no local bottom. The
|
||||
existing continuation facts preserve infeasibility for addition, subtraction, multiplication,
|
||||
division, and modulo, but there is no general power-overflow fact.
|
||||
7. An abstract-only result has feasibility `NOT_ATTEMPTED`; it is not a solver proof that the selected
|
||||
semantic state is reachable.
|
||||
8. The 50 ms session admission floor and fractional backend allocation are conservative. They favor
|
||||
prompt, tagged fallback over attempting a session unlikely to complete.
|
||||
9. The reusable `Z3Solver(use_optimizer=True)` compatibility surface remains, although interval
|
||||
refinement uses only fresh session-owned optimizers.
|
||||
|
||||
These limits are explicit conservative losses of precision. They do not require changes to Stage 3
|
||||
joins, Stage 4 widening, or the worklist to maintain soundness.
|
||||
@@ -1,5 +1,31 @@
|
||||
# Interval Analysis Limitations
|
||||
|
||||
## Abstract nonlinear transfer
|
||||
|
||||
Binary integer operations are evaluated abstract-first. Multiplication uses the four endpoint
|
||||
products (or the square relation for the same operand), checked arithmetic intersects the
|
||||
mathematical result with the destination type, and unchecked wrapping returns an exact wrapped
|
||||
singleton or type top when a single interval cannot represent the modular image. Division,
|
||||
remainder, bounded exponentiation, shifts, and bitwise operations have conservative interval
|
||||
rules. Unsupported signed bitwise and symbolic-power cases return tagged type top.
|
||||
|
||||
Symbolic exponentiation is deliberately not registered as an SMT equation because the backend has
|
||||
no native bit-vector exponent operator. Similarly, a shift with a symbolic right operand is kept
|
||||
abstract when width matching would truncate the shift count. This loses relational refinement but
|
||||
avoids asserting an equation with different semantics from Solidity.
|
||||
|
||||
The abstract transformer consumes operand intervals, not arbitrary relational facts. A `require`
|
||||
condition remains a state-owned solver fact but does not necessarily rewrite the operand's interval;
|
||||
in such a state the abstract result may remain top. Optional refinement can use the complete state,
|
||||
plus typed query-local copies of the current abstract bounds, subject to the expression-wide query
|
||||
budget.
|
||||
|
||||
Optional range refinement admits a Z3 session only when at least 50 ms remains. Each backend check
|
||||
receives a conservative fraction of the remaining wall budget and a watchdog interrupt; no later
|
||||
objective starts after the budget is exhausted. Z3 interrupts are serialized because the installed
|
||||
backend uses a shared default context. This policy intentionally favors a tagged abstract fallback
|
||||
over repeated nonlinear timeouts.
|
||||
|
||||
## Computed Constants in Non-Linear Operations
|
||||
|
||||
When using a computed constant (e.g., `x * (-2)` where `-2` is `TMP = 0 - 2`) in multiplication or division, the variable's range is not narrowed optimally. The result range is correct, but the input variable retains its full type range.
|
||||
@@ -56,11 +82,13 @@ BOTTOM is the correct lattice element: the path after a revert is unreachable (n
|
||||
|
||||
## Loop Analysis (Widening)
|
||||
|
||||
Loops require special handling to guarantee analysis termination. Without intervention, loop iterations could produce ever-increasing bounds that never stabilize.
|
||||
Loops use dominator-defined natural back edges and generation-scoped header fixpoints. A preheader
|
||||
edge initializes the header; only an edge whose destination dominates its source can trigger
|
||||
widening.
|
||||
|
||||
### Threshold Widening
|
||||
|
||||
We use **threshold widening** to ensure termination while preserving precision. Thresholds are collected from the function's numeric literals, bounded by type extremes:
|
||||
Thresholds are collected from numeric literals and type extremes:
|
||||
|
||||
```
|
||||
thresholds = [type_min, ...constants_from_function..., type_max]
|
||||
@@ -68,89 +96,27 @@ thresholds = [type_min, ...constants_from_function..., type_max]
|
||||
|
||||
For uint256: `[0, ...constants..., 2^256 - 1]`
|
||||
|
||||
When a bound grows past a threshold, it jumps to the next threshold. If values don't stabilize, widening eventually reaches the type extremes (guaranteed fixpoint).
|
||||
When a loop-carried bound grows, it jumps to the next threshold. Stable SSA values and non-loop
|
||||
state components are retained. Widening compares the abstract interval in the previous transferred
|
||||
header state with the back-edge interval in the current complete input; it does not issue solver
|
||||
queries.
|
||||
|
||||
### Architecture
|
||||
|
||||
The engine and analysis layers are separated:
|
||||
Each header tracker owns per-edge entry and back-edge contributions, the previous and current
|
||||
complete inputs, the previous transferred output, and one live generation-fact set. Multiple
|
||||
back-edge contributions are joined in stable edge order. A changed contribution to a header that is
|
||||
already queued updates the pending generation rather than starting a generation against stale
|
||||
output.
|
||||
|
||||
1. **Engine layer** (`direction.py`): Detects back edges (propagation to `NodeType.IFLOOP`) and calls `analysis.apply_widening()`
|
||||
2. **Analysis layer** (`IntervalAnalysis`):
|
||||
- `prepare_for_function()`: Collects thresholds from function literals
|
||||
- `apply_widening()`: Applies domain-specific widening logic
|
||||
3. **Phi handler** (`phi.py`): At loop headers, creates unconstrained variables
|
||||
Loop-header phi intervals are derived from currently active SSA alternatives. They are not asserted
|
||||
as cyclic immutable equations. If an active alternative is unavailable, the phi becomes full range.
|
||||
|
||||
```python
|
||||
# Engine detects back edge, delegates to analysis
|
||||
is_back_edge = successor.type == NodeType.IFLOOP
|
||||
if is_back_edge:
|
||||
state_to_propagate = analysis.apply_widening(state_to_propagate, son_state.pre, set())
|
||||
```
|
||||
### Fixed finite progressions
|
||||
|
||||
This maintains abstraction: the engine knows *when* to widen (back edges) but delegates *how* to widen to each concrete analysis.
|
||||
|
||||
### Selective Widening (Attempted)
|
||||
|
||||
The implementation attempts **selective widening**: only widen variables whose bounds actually grew, preserve stable ones. However, this doesn't achieve the desired effect due to SMT architecture limitations.
|
||||
|
||||
**Algorithm (in `apply_widening`):**
|
||||
```
|
||||
for each variable v:
|
||||
current_bounds = query_smt(current_state, v)
|
||||
previous_bounds = query_smt(previous_state, v) # matched by base name
|
||||
|
||||
if current_bounds ⊆ previous_bounds:
|
||||
# Stable - keep current variable
|
||||
result[v] = current[v]
|
||||
else:
|
||||
# Grew - widen to unconstrained
|
||||
result[v] = create_unconstrained_variable()
|
||||
```
|
||||
|
||||
**Why It Doesn't Work:**
|
||||
|
||||
The issue is that phi nodes at loop headers must create **unconstrained** variables:
|
||||
|
||||
1. If we constrain phi variables to incoming values (e.g., `i_2 == i_1`), the SMT constraints are permanent
|
||||
2. When the loop counter increments (`i_3 = i_2 + 1`), the back-edge value can't feed back because `i_2` is stuck at 0
|
||||
3. This makes loop exits unreachable (the solver finds the path unsatisfiable)
|
||||
|
||||
Since phi creates unconstrained variables:
|
||||
- All loop variables start at `[0, MAX]`
|
||||
- Selective widening compares `[0, MAX]` to `[0, MAX]` → always stable
|
||||
- No precision is gained
|
||||
|
||||
**Example - stable variable that should stay `[0, 0]`:**
|
||||
```solidity
|
||||
function test_constant_increment() public pure returns (uint256) {
|
||||
uint256 result = 0;
|
||||
for (uint256 i = 0; i < 5; i++) {
|
||||
result = result; // never changes!
|
||||
}
|
||||
return result;
|
||||
}
|
||||
```
|
||||
|
||||
**Actual analysis output:**
|
||||
```
|
||||
Line 21: result_1 ∈ [0, 0] # Before loop - precise ✓
|
||||
Line 22: result_2 ∈ [0, MAX] # Loop header phi - widened ✗
|
||||
i_2 ∈ [5, MAX] # At exit - narrowed ✓
|
||||
Line 23: result_2 ∈ [0, MAX] # In body - still widened ✗
|
||||
result_3 ∈ [0, MAX] # After assignment - widened ✗
|
||||
Line 25: result_2 ∈ [0, MAX] # At return - widened ✗ (should be [0, 0])
|
||||
```
|
||||
|
||||
Even though `result = result` never changes the value, the analysis reports `[0, MAX]` because the phi at the loop header creates an unconstrained variable.
|
||||
|
||||
**Potential Fixes (require architectural changes):**
|
||||
1. Track bounds as metadata instead of SMT constraints
|
||||
2. Use solver push/pop to scope constraints per iteration
|
||||
3. Use unique SMT variable names per iteration (e.g., `i_2_iter1`, `i_2_iter2`)
|
||||
|
||||
### Results
|
||||
|
||||
Loop analysis produces **sound but conservative** results:
|
||||
A loop with a statically certified checked induction-variable step and a constant monotone guard is
|
||||
unrolled abstractly for at most 64 generations. Once its conservative trip bound is exhausted, the
|
||||
engine rejects the extra recurrence introduced by the non-relational interval join. For example:
|
||||
|
||||
```solidity
|
||||
function test_fixed_bound_loop() public pure returns (uint256) {
|
||||
@@ -162,42 +128,17 @@ function test_fixed_bound_loop() public pure returns (uint256) {
|
||||
}
|
||||
```
|
||||
|
||||
**Actual analysis output:**
|
||||
```
|
||||
Line 10: sum_1 ∈ [0, 0] # Before loop - precise
|
||||
Line 11: i_1 ∈ [0, 0] # Loop init - precise
|
||||
sum_2 ∈ [0, MAX] # Loop header phi - widened
|
||||
i_2 ∈ [10, MAX] # At exit check - narrowed by i >= 10
|
||||
Line 12: i_2 ∈ [0, 9] # In body - narrowed by i < 10
|
||||
sum_3 ∈ [0, MAX] # After sum += i - widened
|
||||
i_3 ∈ [1, 10] # After i++ - narrowed
|
||||
Line 15: sum_2 ∈ [0, MAX] # At return - widened (actual: 45)
|
||||
i_2 ∈ [10, MAX] # At return - narrowed (actual: 10)
|
||||
sum_2 at the reachable exit: [0, 45]
|
||||
i_2 at the reachable exit: [10, 10]
|
||||
```
|
||||
|
||||
**What works:**
|
||||
- `i_2` in loop body: `[0, 9]` ✓ (correctly narrowed by `i < 10`)
|
||||
- `i_2` at return: `[10, MAX]` ✓ (correctly narrowed by exit `i >= 10`)
|
||||
|
||||
**What doesn't work:**
|
||||
- `sum_2` everywhere: `[0, MAX]` ✗ (should be `[0, 45]` or at return exactly `45`)
|
||||
|
||||
### Trade-offs
|
||||
|
||||
| Aspect | Behavior |
|
||||
|--------|----------|
|
||||
| **Termination** | Guaranteed - widening forces fixpoint |
|
||||
| **Soundness** | Maintained - intervals are over-approximations |
|
||||
| **Precision** | Conservative - loop-modified variables lose bounds |
|
||||
| **Loop counters** | Narrowed by exit conditions (correct final range) |
|
||||
| **Accumulators** | Full type range (no symbolic loop summarization) |
|
||||
|
||||
### Limitations
|
||||
|
||||
1. **No narrowing phase**: Don't recover precision after widening by propagating exit conditions backward
|
||||
2. **No loop unrolling**: Fixed-bound loops aren't unrolled for precise analysis
|
||||
3. **No symbolic summarization**: Can't express "sum = 0 + 1 + ... + 9 = 45"
|
||||
4. **SMT overhead**: Each widening comparison requires SMT solver queries for bounds
|
||||
1. There is no narrowing phase after threshold widening.
|
||||
2. Unchecked, symbolic-bound, non-monotone, or more-than-64-generation loops use threshold widening.
|
||||
3. Different back-edge steps are joined conservatively and may quickly reach full range.
|
||||
4. There is no relational or disjunctive loop invariant and no general symbolic summation.
|
||||
|
||||
## Storage Operations (sstore/sload) - Convex Hull
|
||||
|
||||
|
||||
@@ -8,6 +8,10 @@ from slither.analyses.data_flow.analyses.interval.analysis.domain import (
|
||||
DomainVariant,
|
||||
IntervalDomain,
|
||||
)
|
||||
from slither.analyses.data_flow.analyses.interval.analysis.loop import (
|
||||
PRECISE_LOOP_GENERATION_LIMIT,
|
||||
IntervalLoopMetadata,
|
||||
)
|
||||
from slither.analyses.data_flow.analyses.interval.core.state import ComparisonInfo, State
|
||||
from slither.analyses.data_flow.analyses.interval.core.tracked_variable import (
|
||||
NumericInterval,
|
||||
@@ -25,6 +29,11 @@ from slither.analyses.data_flow.analyses.interval.operations.type_utils import (
|
||||
from slither.analyses.data_flow.engine.analysis import Analysis
|
||||
from slither.analyses.data_flow.engine.direction import Direction, Forward
|
||||
from slither.analyses.data_flow.engine.domain import Domain
|
||||
from slither.analyses.data_flow.engine.loop import (
|
||||
LoopVariableId,
|
||||
LoopWideningContext,
|
||||
LoopWideningResult,
|
||||
)
|
||||
from slither.analyses.data_flow.logger import get_logger
|
||||
from slither.analyses.data_flow.smt_solver.facts import (
|
||||
AnalysisContextId,
|
||||
@@ -34,11 +43,11 @@ from slither.analyses.data_flow.smt_solver.facts import (
|
||||
FactOriginKind,
|
||||
FactOwnerKind,
|
||||
FactProvenance,
|
||||
LoopHeaderId,
|
||||
StaticOperationId,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.solver import SMTSolver
|
||||
from slither.analyses.data_flow.smt_solver.telemetry import get_telemetry
|
||||
from slither.analyses.data_flow.smt_solver.query import BoundStatus
|
||||
from slither.core.cfg.node import Node, NodeType
|
||||
from slither.core.declarations.function import Function
|
||||
from slither.core.solidity_types.elementary_type import ElementaryType
|
||||
@@ -64,6 +73,7 @@ class IntervalAnalysis(Analysis):
|
||||
self._thresholds: list[int] = []
|
||||
self._timeout_ms: int = timeout_ms
|
||||
self._root_context = AnalysisContextId.unbound()
|
||||
self._loop_metadata = IntervalLoopMetadata()
|
||||
|
||||
@property
|
||||
def solver(self) -> SMTSolver:
|
||||
@@ -83,6 +93,8 @@ class IntervalAnalysis(Analysis):
|
||||
self._root_context = AnalysisContextId.root(function)
|
||||
self._solver.bind_function_encoding(self._root_context.encoding_id)
|
||||
self._thresholds = self._collect_thresholds(function)
|
||||
self._loop_metadata = IntervalLoopMetadata.from_function(function)
|
||||
self._registry.configure_loop_metadata(self._loop_metadata)
|
||||
logger.debug(
|
||||
"Collected {count} thresholds for {name}: {thresholds}",
|
||||
count=len(self._thresholds),
|
||||
@@ -129,6 +141,10 @@ class IntervalAnalysis(Analysis):
|
||||
"""Return the sorted list of widening thresholds."""
|
||||
return self._thresholds
|
||||
|
||||
def loop_variables(self, header_id: LoopHeaderId) -> tuple[LoopVariableId, ...]:
|
||||
"""Return the loop-carried SSA bindings for one stable header."""
|
||||
return self._loop_metadata.variables_for(header_id)
|
||||
|
||||
def transfer_function(
|
||||
self,
|
||||
node: Node,
|
||||
@@ -265,77 +281,68 @@ class IntervalAnalysis(Analysis):
|
||||
if telemetry is None or not telemetry.enabled:
|
||||
return
|
||||
|
||||
telemetry.record_transfer_op(self._operation_category(operation), handled=True)
|
||||
|
||||
@staticmethod
|
||||
def _operation_category(operation: Operation) -> str:
|
||||
"""Classify one transfer operation for opt-in telemetry."""
|
||||
from slither.slithir.operations import Assignment
|
||||
from slither.slithir.operations.binary import Binary
|
||||
from slither.slithir.operations.condition import Condition
|
||||
from slither.slithir.operations.high_level_call import HighLevelCall
|
||||
from slither.slithir.operations.internal_call import InternalCall
|
||||
from slither.slithir.operations.library_call import LibraryCall
|
||||
from slither.slithir.operations.solidity_call import SolidityCall
|
||||
from slither.slithir.operations.unary import Unary
|
||||
|
||||
op_type = type(operation)
|
||||
operation_type = type(operation)
|
||||
if operation_type is Binary:
|
||||
return IntervalAnalysis._binary_operation_category(operation)
|
||||
if operation_type is Unary:
|
||||
return "arithmetic"
|
||||
if operation_type is SolidityCall:
|
||||
return IntervalAnalysis._solidity_call_category(operation)
|
||||
if operation_type in (HighLevelCall, InternalCall, LibraryCall):
|
||||
return "call"
|
||||
if operation_type is Condition:
|
||||
return "comparison"
|
||||
if operation_type is Assignment:
|
||||
return "assignment"
|
||||
return "assignment"
|
||||
|
||||
# Categorize by operation type
|
||||
if op_type == Binary:
|
||||
# Further categorize binary operations
|
||||
binary_op = operation
|
||||
op_type_enum = getattr(binary_op, "type", None)
|
||||
if op_type_enum is not None:
|
||||
op_name_str = str(op_type_enum.name) if hasattr(op_type_enum, "name") else ""
|
||||
if op_name_str in (
|
||||
"ADDITION",
|
||||
"SUBTRACTION",
|
||||
"MULTIPLICATION",
|
||||
"DIVISION",
|
||||
"MODULO",
|
||||
"POWER",
|
||||
):
|
||||
telemetry.record_transfer_op("arithmetic", handled=True)
|
||||
elif op_name_str in (
|
||||
"LESS",
|
||||
"GREATER",
|
||||
"LESS_EQUAL",
|
||||
"GREATER_EQUAL",
|
||||
"EQUAL",
|
||||
"NOT_EQUAL",
|
||||
):
|
||||
telemetry.record_transfer_op("comparison", handled=True)
|
||||
elif op_name_str in (
|
||||
"AND",
|
||||
"OR",
|
||||
"LEFT_SHIFT",
|
||||
"RIGHT_SHIFT",
|
||||
"CARET",
|
||||
"OROR",
|
||||
"ANDAND",
|
||||
):
|
||||
telemetry.record_transfer_op("bitwise", handled=True)
|
||||
else:
|
||||
telemetry.record_transfer_op("arithmetic", handled=True)
|
||||
else:
|
||||
telemetry.record_transfer_op("arithmetic", handled=True)
|
||||
elif op_type == Unary:
|
||||
telemetry.record_transfer_op("arithmetic", handled=True)
|
||||
elif op_type == SolidityCall:
|
||||
# Check for memory/storage operations
|
||||
func_name = getattr(operation, "function", None)
|
||||
func_str = str(func_name) if func_name else ""
|
||||
if "mstore" in func_str or "mload" in func_str:
|
||||
telemetry.record_transfer_op("memory", handled=True)
|
||||
elif "sstore" in func_str or "sload" in func_str:
|
||||
telemetry.record_transfer_op("storage", handled=True)
|
||||
else:
|
||||
telemetry.record_transfer_op("call", handled=True)
|
||||
elif op_type in (HighLevelCall, InternalCall, LibraryCall):
|
||||
telemetry.record_transfer_op("call", handled=True)
|
||||
elif op_type == Assignment:
|
||||
telemetry.record_transfer_op("assignment", handled=True)
|
||||
elif op_type == Condition:
|
||||
telemetry.record_transfer_op("comparison", handled=True)
|
||||
else:
|
||||
# Phi, TypeConversion, etc.
|
||||
telemetry.record_transfer_op("assignment", handled=True)
|
||||
@staticmethod
|
||||
def _binary_operation_category(operation: Operation) -> str:
|
||||
operation_kind = getattr(operation, "type", None)
|
||||
operation_name = str(getattr(operation_kind, "name", ""))
|
||||
if operation_name in {
|
||||
"LESS",
|
||||
"GREATER",
|
||||
"LESS_EQUAL",
|
||||
"GREATER_EQUAL",
|
||||
"EQUAL",
|
||||
"NOT_EQUAL",
|
||||
}:
|
||||
return "comparison"
|
||||
if operation_name in {
|
||||
"AND",
|
||||
"OR",
|
||||
"LEFT_SHIFT",
|
||||
"RIGHT_SHIFT",
|
||||
"CARET",
|
||||
"OROR",
|
||||
"ANDAND",
|
||||
}:
|
||||
return "bitwise"
|
||||
return "arithmetic"
|
||||
|
||||
@staticmethod
|
||||
def _solidity_call_category(operation: Operation) -> str:
|
||||
function = getattr(operation, "function", None)
|
||||
function_name = str(function) if function else ""
|
||||
if "mstore" in function_name or "mload" in function_name:
|
||||
return "memory"
|
||||
if "sstore" in function_name or "sload" in function_name:
|
||||
return "storage"
|
||||
return "call"
|
||||
|
||||
def apply_condition(self, domain: Domain, condition: Condition, branch_taken: bool) -> Domain:
|
||||
"""Apply branch-specific narrowing based on a condition.
|
||||
@@ -404,9 +411,7 @@ class IntervalAnalysis(Analysis):
|
||||
) -> bool:
|
||||
"""Apply every non-relational restriction for the selected branch."""
|
||||
for refinement in comparison_info.refinements:
|
||||
reachable = (
|
||||
refinement.true_reachable if branch_taken else refinement.false_reachable
|
||||
)
|
||||
reachable = refinement.true_reachable if branch_taken else refinement.false_reachable
|
||||
if not reachable:
|
||||
return False
|
||||
interval = refinement.true_interval if branch_taken else refinement.false_interval
|
||||
@@ -420,267 +425,129 @@ class IntervalAnalysis(Analysis):
|
||||
return condition_term
|
||||
return self._solver.Not(condition_term)
|
||||
|
||||
def apply_widening(
|
||||
self, current_state: Domain, previous_state: Domain, widening_thresholds: set
|
||||
) -> Domain:
|
||||
"""Selective threshold widening for loop back edges.
|
||||
def apply_loop_widening(self, context: LoopWideningContext) -> LoopWideningResult:
|
||||
"""Widen only loop-carried SSA values using their abstract intervals."""
|
||||
current = self._concrete_interval_domain(context.current_input)
|
||||
if current is None:
|
||||
return LoopWideningResult(context.current_input)
|
||||
precise = self._precise_loop_result(context, current)
|
||||
if precise is not None:
|
||||
return precise
|
||||
previous = self._concrete_interval_domain(context.previous_output)
|
||||
if previous is None:
|
||||
return self._loop_result(context, current)
|
||||
widened = self._widen_loop_variables(context, current, previous)
|
||||
return self._loop_result(context, widened)
|
||||
|
||||
Only widens variables whose bounds actually grew between iterations.
|
||||
Stable variables (bounds unchanged) are preserved with original bounds.
|
||||
@staticmethod
|
||||
def _concrete_interval_domain(domain: Domain | None) -> IntervalDomain | None:
|
||||
"""Return a reachable interval state suitable for abstract widening."""
|
||||
if not isinstance(domain, IntervalDomain):
|
||||
return None
|
||||
if domain.variant is not DomainVariant.STATE or domain.state is None:
|
||||
return None
|
||||
return domain
|
||||
|
||||
SSA names differ across iterations (result_2 vs result_3), so we match
|
||||
variables by base name (stripping the SSA suffix).
|
||||
def _precise_loop_result(
|
||||
self,
|
||||
context: LoopWideningContext,
|
||||
current: IntervalDomain,
|
||||
) -> LoopWideningResult | None:
|
||||
"""Use bounded unrolling only for a statically certified progression."""
|
||||
progression = self._loop_metadata.progression_for(context.header_id)
|
||||
if progression is None or current.state is None:
|
||||
return None
|
||||
maximum = progression.maximum_iterations(current.state)
|
||||
if maximum is None or maximum > PRECISE_LOOP_GENERATION_LIMIT:
|
||||
return None
|
||||
if progression.exhaustively_unrolled(context):
|
||||
return LoopWideningResult(context.previous_input.deep_copy())
|
||||
return self._loop_result(context, current)
|
||||
|
||||
Args:
|
||||
current_state: The state being propagated (from loop body).
|
||||
previous_state: The existing state at the loop header.
|
||||
widening_thresholds: Unused (thresholds stored on analysis).
|
||||
|
||||
Returns:
|
||||
Widened state with selectively widened variables.
|
||||
"""
|
||||
if not isinstance(current_state, IntervalDomain):
|
||||
return current_state
|
||||
|
||||
if current_state.variant != DomainVariant.STATE or current_state.state is None:
|
||||
return current_state
|
||||
|
||||
if not isinstance(previous_state, IntervalDomain):
|
||||
return current_state
|
||||
|
||||
# First iteration (BOTTOM) - no widening needed
|
||||
if previous_state.variant == DomainVariant.BOTTOM:
|
||||
return current_state
|
||||
|
||||
if previous_state.state is None:
|
||||
return current_state
|
||||
|
||||
# Build base name -> variable mappings for both states
|
||||
previous_by_base = self._build_base_name_map(previous_state.state)
|
||||
|
||||
widened_state = current_state.state.deep_copy()
|
||||
|
||||
for variable_name in current_state.state.variable_names():
|
||||
current_variable = current_state.state.get_variable(variable_name)
|
||||
if current_variable is None:
|
||||
def _widen_loop_variables(
|
||||
self,
|
||||
context: LoopWideningContext,
|
||||
current: IntervalDomain,
|
||||
previous: IntervalDomain,
|
||||
) -> IntervalDomain:
|
||||
"""Apply threshold widening to only statically bound back-edge values."""
|
||||
if current.state is None or previous.state is None:
|
||||
raise ValueError("Loop widening requires concrete current and previous states")
|
||||
widened = current.state.deep_copy()
|
||||
for binding in context.variables:
|
||||
previous_value = previous.state.get_variable(binding.header_name)
|
||||
if previous_value is None:
|
||||
continue
|
||||
for name in binding.back_names:
|
||||
candidate = current.state.get_variable(name)
|
||||
if candidate is None:
|
||||
continue
|
||||
interval = self._widened_interval(candidate, previous_value)
|
||||
widened.set_variable(name, candidate.with_interval(interval))
|
||||
return IntervalDomain.with_state(widened)
|
||||
|
||||
# Match by base name (strip SSA suffix)
|
||||
base_name = self._extract_base_name(variable_name)
|
||||
previous_variable = previous_by_base.get(base_name)
|
||||
|
||||
if previous_variable is None:
|
||||
# New variable - keep as-is
|
||||
widened_state.set_variable(variable_name, current_variable)
|
||||
continue
|
||||
|
||||
# Compare bounds to check if value grew
|
||||
if self._bounds_are_stable(current_variable, previous_variable, current_state):
|
||||
# Stable - keep current variable (preserves its constraints)
|
||||
widened_state.set_variable(variable_name, current_variable)
|
||||
else:
|
||||
# Grew - widen to unconstrained (full type range)
|
||||
# NOTE: We cannot add explicit bounds constraints because SMT
|
||||
# constraints are permanent. Asserting bounds makes exit branches
|
||||
# unreachable. Full widening to type range is sound but imprecise.
|
||||
widened_variable = self._create_unconstrained_variable(current_variable)
|
||||
widened_state.set_variable(variable_name, widened_variable)
|
||||
|
||||
return IntervalDomain.with_state(widened_state)
|
||||
|
||||
def _extract_base_name(self, ssa_name: str) -> str:
|
||||
"""Extract base variable name from SSA name (strip _N suffix)."""
|
||||
# SSA names are like "result_3", "i_2", "TMP_5"
|
||||
# We want to extract "result", "i", "TMP"
|
||||
parts = ssa_name.rsplit("_", 1)
|
||||
if len(parts) == 2 and parts[1].isdigit():
|
||||
return parts[0]
|
||||
return ssa_name
|
||||
|
||||
def _build_base_name_map(self, state: State) -> dict[str, TrackedSMTVariable]:
|
||||
"""Build mapping from base name to variable (latest SSA version)."""
|
||||
base_map: dict[str, TrackedSMTVariable] = {}
|
||||
for variable_name in state.variable_names():
|
||||
base_name = self._extract_base_name(variable_name)
|
||||
variable = state.get_variable(variable_name)
|
||||
if variable is not None:
|
||||
# If multiple SSA versions, keep any (they should have same bounds)
|
||||
base_map[base_name] = variable
|
||||
return base_map
|
||||
|
||||
def _bounds_are_stable(
|
||||
def _widened_interval(
|
||||
self,
|
||||
current_variable: TrackedSMTVariable,
|
||||
previous_variable: TrackedSMTVariable,
|
||||
current_state: IntervalDomain,
|
||||
) -> bool:
|
||||
"""Check if current bounds are contained within previous bounds.
|
||||
|
||||
Returns True if current ⊆ previous (no growth).
|
||||
"""
|
||||
current_bounds = self._query_variable_bounds(current_variable, current_state)
|
||||
previous_bounds = self._query_variable_bounds(previous_variable, current_state)
|
||||
|
||||
if current_bounds is None or previous_bounds is None:
|
||||
return False # Unknown - assume unstable
|
||||
|
||||
current_min, current_max = current_bounds
|
||||
previous_min, previous_max = previous_bounds
|
||||
|
||||
# Stable if current is contained within previous
|
||||
return current_min >= previous_min and current_max <= previous_max
|
||||
|
||||
def _query_variable_bounds(
|
||||
self,
|
||||
variable: TrackedSMTVariable,
|
||||
domain: IntervalDomain,
|
||||
) -> tuple[int, int] | None:
|
||||
"""Query min/max bounds for a variable using SMT solver."""
|
||||
if domain.state is None:
|
||||
return None
|
||||
|
||||
result = self._solver.solve_range_result(
|
||||
variable.term,
|
||||
state_id=domain.state.semantic_id(),
|
||||
state_facts=domain.state.get_facts(),
|
||||
timeout_ms=self._timeout_ms,
|
||||
signed=bool(variable.base.metadata.get("is_signed", False)),
|
||||
)
|
||||
|
||||
if result.lower_status is not BoundStatus.PROVEN or (
|
||||
result.upper_status is not BoundStatus.PROVEN
|
||||
):
|
||||
return None
|
||||
|
||||
if result.lower is None or result.upper is None:
|
||||
return None
|
||||
return (result.lower, result.upper)
|
||||
|
||||
def _widen_variable_to_threshold(
|
||||
self,
|
||||
current_variable: TrackedSMTVariable,
|
||||
previous_variable: TrackedSMTVariable,
|
||||
current_state: IntervalDomain,
|
||||
) -> TrackedSMTVariable:
|
||||
"""Create new variable with bounds widened to next threshold."""
|
||||
current_bounds = self._query_variable_bounds(current_variable, current_state)
|
||||
previous_bounds = self._query_variable_bounds(previous_variable, current_state)
|
||||
|
||||
if current_bounds is None or previous_bounds is None:
|
||||
return self._create_unconstrained_variable(current_variable)
|
||||
|
||||
widened_min, widened_max = self._compute_widened_bounds(current_bounds, previous_bounds)
|
||||
|
||||
return self._create_variable_with_bounds(
|
||||
current_variable,
|
||||
widened_min,
|
||||
widened_max,
|
||||
current_state,
|
||||
)
|
||||
|
||||
def _compute_widened_bounds(
|
||||
self,
|
||||
current_bounds: tuple[int, int],
|
||||
previous_bounds: tuple[int, int],
|
||||
) -> tuple[int, int]:
|
||||
"""Compute widened bounds using threshold list."""
|
||||
current_min, current_max = current_bounds
|
||||
previous_min, previous_max = previous_bounds
|
||||
|
||||
widened_min = current_min
|
||||
widened_max = current_max
|
||||
|
||||
# If lower bound decreased, widen to next threshold below
|
||||
if current_min < previous_min:
|
||||
widened_min = self._next_threshold_below(current_min)
|
||||
|
||||
# If upper bound increased, widen to next threshold above
|
||||
if current_max > previous_max:
|
||||
widened_max = self._next_threshold_above(current_max)
|
||||
|
||||
return (widened_min, widened_max)
|
||||
|
||||
def _next_threshold_below(self, value: int) -> int:
|
||||
"""Find largest threshold ≤ value."""
|
||||
for threshold in reversed(self._thresholds):
|
||||
if threshold <= value:
|
||||
return threshold
|
||||
return self._thresholds[0] if self._thresholds else 0
|
||||
|
||||
def _next_threshold_above(self, value: int) -> int:
|
||||
"""Find smallest threshold ≥ value."""
|
||||
for threshold in self._thresholds:
|
||||
if threshold >= value:
|
||||
return threshold
|
||||
return self._thresholds[-1] if self._thresholds else (1 << 256) - 1
|
||||
|
||||
def _create_unconstrained_variable(self, template: TrackedSMTVariable) -> TrackedSMTVariable:
|
||||
"""Create an unconstrained variable with same type as template."""
|
||||
is_signed = bool(template.base.metadata.get("is_signed", False))
|
||||
width_metadata = template.base.metadata.get("bit_width", 256)
|
||||
bit_width = width_metadata if isinstance(width_metadata, int) else 256
|
||||
|
||||
variable = TrackedSMTVariable.create(
|
||||
self._solver,
|
||||
template.name,
|
||||
template.sort,
|
||||
is_signed=is_signed,
|
||||
bit_width=bit_width,
|
||||
)
|
||||
return variable.with_overflow_predicates(
|
||||
no_overflow=template.no_overflow,
|
||||
no_underflow=template.no_underflow,
|
||||
operation_id=template.overflow_operation_id,
|
||||
is_unchecked=template.is_unchecked,
|
||||
)
|
||||
|
||||
def _create_variable_with_bounds(
|
||||
self,
|
||||
template: TrackedSMTVariable,
|
||||
lower_bound: int,
|
||||
upper_bound: int,
|
||||
current_state: IntervalDomain,
|
||||
) -> TrackedSMTVariable:
|
||||
"""Create a variable constrained to [lower_bound, upper_bound]."""
|
||||
is_signed = bool(template.base.metadata.get("is_signed", False))
|
||||
width_metadata = template.base.metadata.get("bit_width", 256)
|
||||
bit_width = width_metadata if isinstance(width_metadata, int) else 256
|
||||
|
||||
new_variable = TrackedSMTVariable.create(
|
||||
self._solver,
|
||||
template.name,
|
||||
template.sort,
|
||||
is_signed=is_signed,
|
||||
bit_width=bit_width,
|
||||
)
|
||||
|
||||
# Add bounds constraints
|
||||
lower_term = self._solver.create_constant(lower_bound, template.sort)
|
||||
upper_term = self._solver.create_constant(upper_bound, template.sort)
|
||||
|
||||
if is_signed:
|
||||
lower_constraint = self._solver.bv_sge(new_variable.term, lower_term)
|
||||
upper_constraint = self._solver.bv_sle(new_variable.term, upper_term)
|
||||
else:
|
||||
lower_constraint = self._solver.bv_uge(new_variable.term, lower_term)
|
||||
upper_constraint = self._solver.bv_ule(new_variable.term, upper_term)
|
||||
|
||||
for role, constraint in (
|
||||
("widened_lower_bound", lower_constraint),
|
||||
("widened_upper_bound", upper_constraint),
|
||||
):
|
||||
fact = Fact(
|
||||
fact_id=FactId(
|
||||
owner=FactOwnerKind.LOOP_GENERATION,
|
||||
kind=FactKind.RANGE_BOUND,
|
||||
provenance=FactProvenance(
|
||||
context_id=current_state.context_id,
|
||||
origin_kind=FactOriginKind.LOOP,
|
||||
),
|
||||
semantic_key=(role, template.name),
|
||||
current: TrackedSMTVariable,
|
||||
previous: TrackedSMTVariable,
|
||||
) -> NumericInterval:
|
||||
"""Widen growing bounds to the nearest literal or type threshold."""
|
||||
current_interval = current.interval
|
||||
previous_interval = previous.interval
|
||||
type_interval = current.type_interval
|
||||
thresholds = sorted(
|
||||
{
|
||||
type_interval.lower,
|
||||
type_interval.upper,
|
||||
*(
|
||||
value
|
||||
for value in self._thresholds
|
||||
if type_interval.lower <= value <= type_interval.upper
|
||||
),
|
||||
formula=constraint,
|
||||
)
|
||||
self._solver.register_loop_generation_fact(fact)
|
||||
}
|
||||
)
|
||||
lower = current_interval.lower
|
||||
upper = current_interval.upper
|
||||
if lower < previous_interval.lower:
|
||||
lower = max(value for value in thresholds if value <= lower)
|
||||
if upper > previous_interval.upper:
|
||||
upper = min(value for value in thresholds if value >= upper)
|
||||
return NumericInterval(lower, upper)
|
||||
|
||||
return new_variable
|
||||
def _loop_result(
|
||||
self,
|
||||
context: LoopWideningContext,
|
||||
domain: IntervalDomain,
|
||||
) -> LoopWideningResult:
|
||||
"""Attach replaceable generation facts to one widened abstract state."""
|
||||
if domain.state is None:
|
||||
return LoopWideningResult(domain)
|
||||
facts: list[Fact[object]] = []
|
||||
for binding in context.variables:
|
||||
for name in binding.back_names:
|
||||
variable = domain.state.get_variable(name)
|
||||
if variable is None or variable.interval == variable.type_interval:
|
||||
continue
|
||||
interval = variable.interval
|
||||
facts.append(
|
||||
Fact(
|
||||
fact_id=FactId(
|
||||
owner=FactOwnerKind.LOOP_GENERATION,
|
||||
kind=FactKind.RANGE_BOUND,
|
||||
provenance=FactProvenance(
|
||||
context_id=domain.context_id,
|
||||
origin_kind=FactOriginKind.LOOP,
|
||||
loop_header_id=context.header_id,
|
||||
loop_generation=context.generation,
|
||||
),
|
||||
semantic_key=(
|
||||
"abstract_loop_range",
|
||||
name,
|
||||
str(interval.lower),
|
||||
str(interval.upper),
|
||||
),
|
||||
),
|
||||
formula=interval,
|
||||
)
|
||||
)
|
||||
return LoopWideningResult(domain, tuple(facts))
|
||||
|
||||
@@ -0,0 +1,280 @@
|
||||
"""Static loop metadata used by interval widening."""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass
|
||||
from typing import TYPE_CHECKING
|
||||
|
||||
from slither.analyses.data_flow.analyses.interval.analysis.domain import (
|
||||
DomainVariant,
|
||||
IntervalDomain,
|
||||
)
|
||||
from slither.analyses.data_flow.engine.loop import (
|
||||
LoopStructure,
|
||||
LoopVariableId,
|
||||
LoopWideningContext,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.facts import LoopHeaderId
|
||||
from slither.slithir.operations.binary import Binary, BinaryType
|
||||
from slither.slithir.operations.condition import Condition
|
||||
from slither.slithir.operations.phi import Phi
|
||||
from slither.slithir.variables.constant import Constant
|
||||
|
||||
|
||||
if TYPE_CHECKING:
|
||||
from slither.analyses.data_flow.analyses.interval.core.state import State
|
||||
from slither.core.cfg.node import Node
|
||||
from slither.core.declarations.function import Function
|
||||
from slither.slithir.operations.operation import Operation
|
||||
|
||||
|
||||
PRECISE_LOOP_GENERATION_LIMIT = 64
|
||||
|
||||
|
||||
def _variable_name(value: object) -> str:
|
||||
"""Return an SSA or ordinary name for metadata-only inspection."""
|
||||
ssa_name = getattr(value, "ssa_name", None)
|
||||
if isinstance(ssa_name, str):
|
||||
return ssa_name
|
||||
name = getattr(value, "name", None)
|
||||
if not isinstance(name, str):
|
||||
raise TypeError(f"Loop operand {value!r} has no variable name")
|
||||
return name
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class LoopProgression:
|
||||
"""Certified monotone induction variable controlling one loop exit."""
|
||||
|
||||
variable: LoopVariableId
|
||||
comparison: BinaryType
|
||||
bound: int
|
||||
step: int
|
||||
|
||||
def maximum_iterations(self, state: State) -> int | None:
|
||||
"""Return a conservative finite trip bound from the entry interval."""
|
||||
entry_interval = None
|
||||
for name in self.variable.entry_names:
|
||||
tracked = state.get_variable(name)
|
||||
if tracked is None:
|
||||
return None
|
||||
entry_interval = (
|
||||
tracked.interval
|
||||
if entry_interval is None
|
||||
else entry_interval.hull(tracked.interval)
|
||||
)
|
||||
if entry_interval is None:
|
||||
return None
|
||||
if self.step > 0:
|
||||
target = self.bound + int(self.comparison is BinaryType.LESS_EQUAL)
|
||||
distance = max(0, target - entry_interval.lower)
|
||||
return (distance + self.step - 1) // self.step
|
||||
target = self.bound - int(self.comparison is BinaryType.GREATER_EQUAL)
|
||||
distance = max(0, entry_interval.upper - target)
|
||||
magnitude = -self.step
|
||||
return (distance + magnitude - 1) // magnitude
|
||||
|
||||
def exhaustively_unrolled(self, context: LoopWideningContext) -> bool:
|
||||
"""Return whether a bounded loop has reached its certified trip limit."""
|
||||
current = context.current_input
|
||||
previous_output = context.previous_output
|
||||
if not isinstance(current, IntervalDomain) or not isinstance(
|
||||
previous_output, IntervalDomain
|
||||
):
|
||||
return False
|
||||
if current.variant is not DomainVariant.STATE or current.state is None:
|
||||
return False
|
||||
if previous_output.variant is not DomainVariant.STATE or previous_output.state is None:
|
||||
return False
|
||||
maximum = self.maximum_iterations(current.state)
|
||||
if maximum is None or maximum > PRECISE_LOOP_GENERATION_LIMIT:
|
||||
return False
|
||||
if context.generation <= maximum:
|
||||
return False
|
||||
header_value = previous_output.state.get_variable(self.variable.header_name)
|
||||
if header_value is None:
|
||||
return False
|
||||
if self.step > 0:
|
||||
return header_value.interval.upper >= self.bound
|
||||
return header_value.interval.lower <= self.bound
|
||||
|
||||
|
||||
class IntervalLoopMetadata:
|
||||
"""Loop-carried SSA bindings and certified finite progressions."""
|
||||
|
||||
def __init__(
|
||||
self,
|
||||
variables: dict[LoopHeaderId, tuple[LoopVariableId, ...]] | None = None,
|
||||
progressions: dict[LoopHeaderId, LoopProgression] | None = None,
|
||||
) -> None:
|
||||
self._variables = dict(variables or {})
|
||||
self._progressions = dict(progressions or {})
|
||||
|
||||
@classmethod
|
||||
def from_function(cls, function: Function) -> IntervalLoopMetadata:
|
||||
"""Derive metadata solely from stable SSA and dominator information."""
|
||||
structure = LoopStructure.from_function(function)
|
||||
nodes = {node.node_id: node for node in function.nodes}
|
||||
definitions = cls._definitions(function)
|
||||
variables = {}
|
||||
progressions = {}
|
||||
for loop in structure.loops:
|
||||
header = nodes[loop.header_id.node_id]
|
||||
bindings = cls._loop_variables(header, definitions)
|
||||
variables[loop.header_id] = bindings
|
||||
progression = cls._progression(header, bindings, definitions)
|
||||
if progression is not None:
|
||||
progressions[loop.header_id] = progression
|
||||
return cls(variables, progressions)
|
||||
|
||||
@staticmethod
|
||||
def _definitions(function: Function) -> dict[str, tuple[Operation, Node]]:
|
||||
definitions = {}
|
||||
for node in function.nodes:
|
||||
for operation in node.irs_ssa or ():
|
||||
lvalue = getattr(operation, "lvalue", None)
|
||||
if lvalue is not None:
|
||||
definitions[_variable_name(lvalue)] = (operation, node)
|
||||
return definitions
|
||||
|
||||
@staticmethod
|
||||
def _loop_variables(
|
||||
header: Node,
|
||||
definitions: dict[str, tuple[Operation, Node]],
|
||||
) -> tuple[LoopVariableId, ...]:
|
||||
variables = []
|
||||
for operation in header.irs_ssa or ():
|
||||
if not isinstance(operation, Phi) or operation.lvalue is None:
|
||||
continue
|
||||
entry_names = []
|
||||
back_names = []
|
||||
for rvalue in operation.rvalues:
|
||||
name = _variable_name(rvalue)
|
||||
definition = definitions.get(name)
|
||||
is_back = definition is not None and header in definition[1].dominators
|
||||
(back_names if is_back else entry_names).append(name)
|
||||
if entry_names and back_names:
|
||||
variables.append(
|
||||
LoopVariableId(
|
||||
_variable_name(operation.lvalue),
|
||||
tuple(sorted(entry_names)),
|
||||
tuple(sorted(back_names)),
|
||||
)
|
||||
)
|
||||
return tuple(sorted(variables))
|
||||
|
||||
@classmethod
|
||||
def _progression(
|
||||
cls,
|
||||
header: Node,
|
||||
variables: tuple[LoopVariableId, ...],
|
||||
definitions: dict[str, tuple[Operation, Node]],
|
||||
) -> LoopProgression | None:
|
||||
comparison = cls._condition_comparison(header)
|
||||
if comparison is None:
|
||||
return None
|
||||
for variable in variables:
|
||||
normalized = cls._normalize_comparison(comparison, variable.header_name)
|
||||
if normalized is None:
|
||||
continue
|
||||
comparison_type, bound = normalized
|
||||
steps = {
|
||||
cls._progression_step(definitions.get(name), variable.header_name)
|
||||
for name in variable.back_names
|
||||
}
|
||||
if None in steps or len(steps) != 1:
|
||||
continue
|
||||
step = steps.pop()
|
||||
if step is None or not cls._moves_toward_exit(comparison_type, step):
|
||||
continue
|
||||
return LoopProgression(variable, comparison_type, bound, step)
|
||||
return None
|
||||
|
||||
@staticmethod
|
||||
def _condition_comparison(header: Node) -> Binary | None:
|
||||
operations = header.irs_ssa or ()
|
||||
conditions = [operation for operation in operations if isinstance(operation, Condition)]
|
||||
if len(conditions) != 1:
|
||||
return None
|
||||
condition_name = _variable_name(conditions[0].value)
|
||||
return next(
|
||||
(
|
||||
operation
|
||||
for operation in operations
|
||||
if isinstance(operation, Binary)
|
||||
and operation.lvalue is not None
|
||||
and _variable_name(operation.lvalue) == condition_name
|
||||
),
|
||||
None,
|
||||
)
|
||||
|
||||
@staticmethod
|
||||
def _normalize_comparison(
|
||||
operation: Binary,
|
||||
variable_name: str,
|
||||
) -> tuple[BinaryType, int] | None:
|
||||
left_name = _variable_name(operation.variable_left)
|
||||
right_name = _variable_name(operation.variable_right)
|
||||
if left_name == variable_name and isinstance(operation.variable_right, Constant):
|
||||
value = operation.variable_right.value
|
||||
return (operation.type, value) if isinstance(value, int) else None
|
||||
if right_name != variable_name or not isinstance(operation.variable_left, Constant):
|
||||
return None
|
||||
value = operation.variable_left.value
|
||||
if not isinstance(value, int):
|
||||
return None
|
||||
reversed_types = {
|
||||
BinaryType.LESS: BinaryType.GREATER,
|
||||
BinaryType.LESS_EQUAL: BinaryType.GREATER_EQUAL,
|
||||
BinaryType.GREATER: BinaryType.LESS,
|
||||
BinaryType.GREATER_EQUAL: BinaryType.LESS_EQUAL,
|
||||
}
|
||||
reversed_type = reversed_types.get(operation.type)
|
||||
return (reversed_type, value) if reversed_type is not None else None
|
||||
|
||||
@staticmethod
|
||||
def _progression_step(
|
||||
definition: tuple[Operation, Node] | None,
|
||||
header_name: str,
|
||||
) -> int | None:
|
||||
if definition is None:
|
||||
return None
|
||||
raw_operation, node = definition
|
||||
if not isinstance(raw_operation, Binary):
|
||||
return None
|
||||
operation = raw_operation
|
||||
if not bool(getattr(node.scope, "is_checked", False)):
|
||||
return None
|
||||
left = operation.variable_left
|
||||
right = operation.variable_right
|
||||
if operation.type is BinaryType.ADDITION:
|
||||
if _variable_name(left) == header_name and isinstance(right, Constant):
|
||||
return right.value if isinstance(right.value, int) else None
|
||||
if _variable_name(right) == header_name and isinstance(left, Constant):
|
||||
return left.value if isinstance(left.value, int) else None
|
||||
if (
|
||||
operation.type is BinaryType.SUBTRACTION
|
||||
and _variable_name(left) == header_name
|
||||
and isinstance(right, Constant)
|
||||
and isinstance(right.value, int)
|
||||
):
|
||||
return -right.value
|
||||
return None
|
||||
|
||||
@staticmethod
|
||||
def _moves_toward_exit(comparison: BinaryType, step: int) -> bool:
|
||||
ascending = comparison in (BinaryType.LESS, BinaryType.LESS_EQUAL)
|
||||
descending = comparison in (BinaryType.GREATER, BinaryType.GREATER_EQUAL)
|
||||
return (ascending and step > 0) or (descending and step < 0)
|
||||
|
||||
def variables_for(self, header_id: LoopHeaderId) -> tuple[LoopVariableId, ...]:
|
||||
"""Return loop-carried bindings for one header."""
|
||||
return self._variables.get(header_id, ())
|
||||
|
||||
def is_loop_header(self, header_id: LoopHeaderId) -> bool:
|
||||
"""Return whether the stable header belongs to a classified natural loop."""
|
||||
return header_id in self._variables
|
||||
|
||||
def progression_for(self, header_id: LoopHeaderId) -> LoopProgression | None:
|
||||
"""Return the certified controlling progression, when available."""
|
||||
return self._progressions.get(header_id)
|
||||
@@ -101,8 +101,7 @@ class State:
|
||||
if any(fact.fact_id.owner is not FactOwnerKind.STATE_LOCAL for fact in facts):
|
||||
raise ValueError("State construction accepts only STATE_LOCAL facts")
|
||||
if any(
|
||||
fact.fact_id.provenance.origin_kind is FactOriginKind.ABSTRACT_STATE
|
||||
for fact in facts
|
||||
fact.fact_id.provenance.origin_kind is FactOriginKind.ABSTRACT_STATE for fact in facts
|
||||
):
|
||||
raise ValueError("Abstract range facts are derived from tracked values")
|
||||
|
||||
@@ -208,9 +207,7 @@ class State:
|
||||
def get_branch_facts(self) -> tuple[Fact[SMTTerm], ...]:
|
||||
"""Derive the branch view from the final active explicit fact set."""
|
||||
return tuple(
|
||||
fact
|
||||
for fact in self.get_explicit_facts()
|
||||
if fact.fact_id.kind is FactKind.BRANCH_GUARD
|
||||
fact for fact in self.get_explicit_facts() if fact.fact_id.kind is FactKind.BRANCH_GUARD
|
||||
)
|
||||
|
||||
def get_branch_fact_ids(self) -> frozenset[FactId]:
|
||||
@@ -514,6 +511,7 @@ class State:
|
||||
provenance.origin_kind.value,
|
||||
repr(provenance.operation_id),
|
||||
repr(provenance.cfg_edge),
|
||||
repr(provenance.loop_header_id),
|
||||
repr(provenance.loop_generation),
|
||||
repr(provenance.property_id),
|
||||
*fact_id.semantic_key,
|
||||
|
||||
@@ -0,0 +1,399 @@
|
||||
"""Sound non-relational interval transfer for integer binary operations."""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass
|
||||
from enum import Enum
|
||||
|
||||
from slither.analyses.data_flow.analyses.interval.core.tracked_variable import NumericInterval
|
||||
from slither.slithir.operations.binary import BinaryType
|
||||
|
||||
|
||||
class AbstractTransferKind(Enum):
|
||||
"""Precision class of one sound abstract operation result."""
|
||||
|
||||
EXACT = "exact"
|
||||
INTERVAL = "interval"
|
||||
TOP = "top"
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class AbstractTransferResult:
|
||||
"""One sound interval result and the reason for its precision."""
|
||||
|
||||
interval: NumericInterval
|
||||
kind: AbstractTransferKind
|
||||
may_wrap: bool = False
|
||||
supported: bool = True
|
||||
|
||||
|
||||
def transfer_binary_interval(
|
||||
operation: BinaryType,
|
||||
left: NumericInterval,
|
||||
right: NumericInterval,
|
||||
*,
|
||||
bit_width: int,
|
||||
is_signed: bool,
|
||||
is_checked: bool,
|
||||
same_operand: bool = False,
|
||||
) -> AbstractTransferResult:
|
||||
"""Return a conservative interval for one Solidity integer operation."""
|
||||
type_interval = NumericInterval.type_range(bit_width, is_signed)
|
||||
if operation is BinaryType.SUBTRACTION and same_operand:
|
||||
return _exact(0)
|
||||
if operation is BinaryType.DIVISION and same_operand:
|
||||
return _exact(1)
|
||||
if operation is BinaryType.MODULO and same_operand:
|
||||
return _exact(0)
|
||||
if operation in (BinaryType.AND, BinaryType.OR) and same_operand:
|
||||
return _interval_result(left, type_interval)
|
||||
if operation is BinaryType.CARET and same_operand:
|
||||
return _exact(0)
|
||||
|
||||
if operation is BinaryType.ADDITION:
|
||||
raw = NumericInterval(left.lower + right.lower, left.upper + right.upper)
|
||||
return _finish_integer_arithmetic(raw, type_interval, bit_width, is_signed, is_checked)
|
||||
if operation is BinaryType.SUBTRACTION:
|
||||
raw = NumericInterval(left.lower - right.upper, left.upper - right.lower)
|
||||
return _finish_integer_arithmetic(raw, type_interval, bit_width, is_signed, is_checked)
|
||||
if operation is BinaryType.MULTIPLICATION:
|
||||
if same_operand:
|
||||
products = (left.lower * left.lower, left.upper * left.upper)
|
||||
raw = NumericInterval(
|
||||
0 if left.lower <= 0 <= left.upper else min(products),
|
||||
max(products),
|
||||
)
|
||||
return _finish_integer_arithmetic(
|
||||
raw, type_interval, bit_width, is_signed, is_checked
|
||||
)
|
||||
products = (
|
||||
left.lower * right.lower,
|
||||
left.lower * right.upper,
|
||||
left.upper * right.lower,
|
||||
left.upper * right.upper,
|
||||
)
|
||||
raw = NumericInterval(min(products), max(products))
|
||||
return _finish_integer_arithmetic(raw, type_interval, bit_width, is_signed, is_checked)
|
||||
if operation is BinaryType.DIVISION:
|
||||
return _division(left, right, type_interval)
|
||||
if operation is BinaryType.MODULO:
|
||||
return _modulo(left, right, type_interval, is_signed)
|
||||
if operation is BinaryType.POWER:
|
||||
return _power(
|
||||
left,
|
||||
right,
|
||||
type_interval,
|
||||
bit_width=bit_width,
|
||||
is_signed=is_signed,
|
||||
is_checked=is_checked,
|
||||
)
|
||||
if operation in (BinaryType.LEFT_SHIFT, BinaryType.RIGHT_SHIFT):
|
||||
return _shift(
|
||||
operation,
|
||||
left,
|
||||
right,
|
||||
type_interval,
|
||||
bit_width=bit_width,
|
||||
is_signed=is_signed,
|
||||
)
|
||||
if operation in (BinaryType.AND, BinaryType.OR, BinaryType.CARET):
|
||||
return _bitwise(
|
||||
operation,
|
||||
left,
|
||||
right,
|
||||
type_interval,
|
||||
bit_width=bit_width,
|
||||
is_signed=is_signed,
|
||||
)
|
||||
return _top(type_interval, supported=False)
|
||||
|
||||
|
||||
def _finish_integer_arithmetic(
|
||||
raw: NumericInterval,
|
||||
type_interval: NumericInterval,
|
||||
bit_width: int,
|
||||
is_signed: bool,
|
||||
is_checked: bool,
|
||||
) -> AbstractTransferResult:
|
||||
if _contains(type_interval, raw):
|
||||
return _interval_result(raw, type_interval)
|
||||
if is_checked:
|
||||
successful = raw.intersection(type_interval)
|
||||
if successful is None:
|
||||
# The interval domain has no operation-local bottom value. The checked
|
||||
# continuation facts retain infeasibility; top is the only sound value.
|
||||
return _top(type_interval)
|
||||
return _interval_result(successful, type_interval)
|
||||
if raw.lower == raw.upper:
|
||||
return AbstractTransferResult(
|
||||
NumericInterval(
|
||||
_wrap_and_decode(raw.lower, bit_width, is_signed),
|
||||
_wrap_and_decode(raw.lower, bit_width, is_signed),
|
||||
),
|
||||
AbstractTransferKind.EXACT,
|
||||
may_wrap=True,
|
||||
)
|
||||
# A single interval cannot in general represent modular images without
|
||||
# becoming disjunctive. Top is sound and avoids an incorrect narrow hull.
|
||||
return _top(type_interval, may_wrap=True)
|
||||
|
||||
|
||||
def _division(
|
||||
left: NumericInterval,
|
||||
right: NumericInterval,
|
||||
type_interval: NumericInterval,
|
||||
) -> AbstractTransferResult:
|
||||
divisors = _nonzero_extreme_values(right)
|
||||
if not divisors:
|
||||
return _top(type_interval)
|
||||
dividends = {left.lower, left.upper}
|
||||
if left.lower <= 0 <= left.upper:
|
||||
dividends.add(0)
|
||||
values = [_truncating_division(a, b) for a in dividends for b in divisors]
|
||||
return _interval_result(NumericInterval(min(values), max(values)), type_interval)
|
||||
|
||||
|
||||
def _modulo(
|
||||
left: NumericInterval,
|
||||
right: NumericInterval,
|
||||
type_interval: NumericInterval,
|
||||
is_signed: bool,
|
||||
) -> AbstractTransferResult:
|
||||
divisors = _nonzero_extreme_values(right)
|
||||
if not divisors:
|
||||
return _top(type_interval)
|
||||
if left.lower == left.upper and right.lower == right.upper and right.lower != 0:
|
||||
quotient = _truncating_division(left.lower, right.lower)
|
||||
return _exact(left.lower - quotient * right.lower)
|
||||
max_divisor_magnitude = max(abs(value) for value in divisors)
|
||||
max_remainder_magnitude = min(
|
||||
max(abs(left.lower), abs(left.upper)),
|
||||
max_divisor_magnitude - 1,
|
||||
)
|
||||
if not is_signed:
|
||||
raw = NumericInterval(0, min(left.upper, max_remainder_magnitude))
|
||||
elif left.lower >= 0:
|
||||
raw = NumericInterval(0, min(left.upper, max_remainder_magnitude))
|
||||
elif left.upper <= 0:
|
||||
raw = NumericInterval(max(left.lower, -max_remainder_magnitude), 0)
|
||||
else:
|
||||
raw = NumericInterval(-max_remainder_magnitude, max_remainder_magnitude)
|
||||
return _interval_result(raw, type_interval)
|
||||
|
||||
|
||||
def _power(
|
||||
base: NumericInterval,
|
||||
exponent: NumericInterval,
|
||||
type_interval: NumericInterval,
|
||||
*,
|
||||
bit_width: int,
|
||||
is_signed: bool,
|
||||
is_checked: bool,
|
||||
) -> AbstractTransferResult:
|
||||
if exponent.lower < 0:
|
||||
return _top(type_interval, supported=False)
|
||||
if base.lower == base.upper and base.lower in (-1, 0, 1):
|
||||
return _small_base_power(base.lower, exponent, type_interval)
|
||||
if exponent.lower == exponent.upper:
|
||||
if exponent.lower > 1024:
|
||||
if base.lower == base.upper and not is_checked:
|
||||
wrapped = pow(base.lower, exponent.lower, 1 << bit_width)
|
||||
return _exact(_wrap_and_decode(wrapped, bit_width, is_signed))
|
||||
return _top(type_interval, supported=False)
|
||||
raw = _fixed_exponent_interval(base, exponent.lower)
|
||||
return _finish_integer_arithmetic(raw, type_interval, bit_width, is_signed, is_checked)
|
||||
# Bounded unsigned exponentiation is monotone in the common non-negative
|
||||
# case. Cap concrete endpoint evaluation to avoid constructing enormous
|
||||
# Python integers for an unconstrained uint256 exponent.
|
||||
if base.lower >= 0 and exponent.upper <= 1024:
|
||||
bases = {base.lower, base.upper}
|
||||
powers = {exponent.lower, exponent.upper}
|
||||
if base.lower <= 1 <= base.upper:
|
||||
bases.add(1)
|
||||
if exponent.lower <= 1 <= exponent.upper:
|
||||
powers.add(1)
|
||||
values = [pow(value, power) for value in bases for power in powers]
|
||||
raw = NumericInterval(min(values), max(values))
|
||||
return _finish_integer_arithmetic(raw, type_interval, bit_width, is_signed, is_checked)
|
||||
return _top(type_interval, supported=False)
|
||||
|
||||
|
||||
def _small_base_power(
|
||||
base: int,
|
||||
exponent: NumericInterval,
|
||||
type_interval: NumericInterval,
|
||||
) -> AbstractTransferResult:
|
||||
if base == 1:
|
||||
return _exact(1)
|
||||
if base == 0:
|
||||
return _exact(0) if exponent.lower > 0 else _interval_result(NumericInterval(0, 1), type_interval)
|
||||
if exponent.lower == exponent.upper:
|
||||
return _exact(-1 if exponent.lower % 2 else 1)
|
||||
return _interval_result(NumericInterval(-1, 1), type_interval)
|
||||
|
||||
|
||||
def _fixed_exponent_interval(base: NumericInterval, exponent: int) -> NumericInterval:
|
||||
if exponent == 0:
|
||||
return NumericInterval(1, 1)
|
||||
if exponent % 2:
|
||||
return NumericInterval(pow(base.lower, exponent), pow(base.upper, exponent))
|
||||
maximum = max(pow(abs(base.lower), exponent), pow(abs(base.upper), exponent))
|
||||
minimum = 0 if base.lower <= 0 <= base.upper else min(
|
||||
pow(abs(base.lower), exponent),
|
||||
pow(abs(base.upper), exponent),
|
||||
)
|
||||
return NumericInterval(minimum, maximum)
|
||||
|
||||
|
||||
def _shift(
|
||||
operation: BinaryType,
|
||||
left: NumericInterval,
|
||||
right: NumericInterval,
|
||||
type_interval: NumericInterval,
|
||||
*,
|
||||
bit_width: int,
|
||||
is_signed: bool,
|
||||
) -> AbstractTransferResult:
|
||||
if right.lower < 0:
|
||||
return _top(type_interval, supported=False)
|
||||
shift_values = range(right.lower, min(right.upper, bit_width - 1) + 1)
|
||||
representative_shifts = list(shift_values)
|
||||
if right.upper >= bit_width:
|
||||
representative_shifts.append(bit_width)
|
||||
results = [
|
||||
_fixed_shift(
|
||||
operation,
|
||||
left,
|
||||
shift,
|
||||
type_interval,
|
||||
bit_width=bit_width,
|
||||
is_signed=is_signed,
|
||||
)
|
||||
for shift in representative_shifts
|
||||
]
|
||||
if not results:
|
||||
return _top(type_interval)
|
||||
if any(result.kind is AbstractTransferKind.TOP for result in results):
|
||||
return _top(type_interval, may_wrap=operation is BinaryType.LEFT_SHIFT)
|
||||
interval = results[0].interval
|
||||
for result in results[1:]:
|
||||
interval = interval.hull(result.interval)
|
||||
combined = _interval_result(interval, type_interval)
|
||||
return AbstractTransferResult(
|
||||
combined.interval,
|
||||
combined.kind,
|
||||
may_wrap=any(result.may_wrap for result in results),
|
||||
)
|
||||
|
||||
|
||||
def _fixed_shift(
|
||||
operation: BinaryType,
|
||||
left: NumericInterval,
|
||||
shift: int,
|
||||
type_interval: NumericInterval,
|
||||
*,
|
||||
bit_width: int,
|
||||
is_signed: bool,
|
||||
) -> AbstractTransferResult:
|
||||
if operation is BinaryType.RIGHT_SHIFT:
|
||||
if shift >= bit_width:
|
||||
if not is_signed:
|
||||
return _exact(0)
|
||||
values = (-1 if left.lower < 0 else 0, -1 if left.upper < 0 else 0)
|
||||
return _interval_result(NumericInterval(min(values), max(values)), type_interval)
|
||||
raw = NumericInterval(left.lower >> shift, left.upper >> shift)
|
||||
return _interval_result(raw, type_interval)
|
||||
if shift >= bit_width:
|
||||
return _exact(0)
|
||||
raw = NumericInterval(left.lower << shift, left.upper << shift)
|
||||
# Solidity shifts truncate bits even in checked scopes.
|
||||
return _finish_integer_arithmetic(raw, type_interval, bit_width, is_signed, False)
|
||||
|
||||
|
||||
def _bitwise(
|
||||
operation: BinaryType,
|
||||
left: NumericInterval,
|
||||
right: NumericInterval,
|
||||
type_interval: NumericInterval,
|
||||
*,
|
||||
bit_width: int,
|
||||
is_signed: bool,
|
||||
) -> AbstractTransferResult:
|
||||
if left.lower == left.upper and right.lower == right.upper:
|
||||
left_bits = left.lower % (1 << bit_width)
|
||||
right_bits = right.lower % (1 << bit_width)
|
||||
if operation is BinaryType.AND:
|
||||
value = left_bits & right_bits
|
||||
elif operation is BinaryType.OR:
|
||||
value = left_bits | right_bits
|
||||
else:
|
||||
value = left_bits ^ right_bits
|
||||
return _exact(_wrap_and_decode(value, bit_width, is_signed))
|
||||
zero = NumericInterval(0, 0)
|
||||
if left == zero:
|
||||
return _exact(0) if operation is BinaryType.AND else _interval_result(right, type_interval)
|
||||
if right == zero:
|
||||
return _exact(0) if operation is BinaryType.AND else _interval_result(left, type_interval)
|
||||
if not is_signed or (left.lower >= 0 and right.lower >= 0):
|
||||
if operation is BinaryType.AND:
|
||||
raw = NumericInterval(0, min(left.upper, right.upper))
|
||||
else:
|
||||
highest = max(left.upper, right.upper).bit_length()
|
||||
raw = NumericInterval(0, (1 << highest) - 1 if highest else 0)
|
||||
return _interval_result(raw, type_interval)
|
||||
return _top(type_interval, supported=False)
|
||||
|
||||
|
||||
def _nonzero_extreme_values(interval: NumericInterval) -> set[int]:
|
||||
values = {value for value in (interval.lower, interval.upper) if value != 0}
|
||||
if interval.lower <= -1 <= interval.upper:
|
||||
values.add(-1)
|
||||
if interval.lower <= 1 <= interval.upper:
|
||||
values.add(1)
|
||||
return values
|
||||
|
||||
|
||||
def _truncating_division(left: int, right: int) -> int:
|
||||
quotient = abs(left) // abs(right)
|
||||
return -quotient if (left < 0) != (right < 0) else quotient
|
||||
|
||||
|
||||
def _wrap_and_decode(value: int, bit_width: int, is_signed: bool) -> int:
|
||||
modulus = 1 << bit_width
|
||||
wrapped = value % modulus
|
||||
if is_signed and wrapped >= 1 << (bit_width - 1):
|
||||
wrapped -= modulus
|
||||
return wrapped
|
||||
|
||||
|
||||
def _contains(outer: NumericInterval, inner: NumericInterval) -> bool:
|
||||
return outer.lower <= inner.lower and inner.upper <= outer.upper
|
||||
|
||||
|
||||
def _interval_result(
|
||||
interval: NumericInterval,
|
||||
type_interval: NumericInterval,
|
||||
) -> AbstractTransferResult:
|
||||
interval = interval.intersection(type_interval) or type_interval
|
||||
kind = AbstractTransferKind.EXACT if interval.lower == interval.upper else (
|
||||
AbstractTransferKind.TOP if interval == type_interval else AbstractTransferKind.INTERVAL
|
||||
)
|
||||
return AbstractTransferResult(interval, kind)
|
||||
|
||||
|
||||
def _exact(value: int) -> AbstractTransferResult:
|
||||
return AbstractTransferResult(NumericInterval(value, value), AbstractTransferKind.EXACT)
|
||||
|
||||
|
||||
def _top(
|
||||
type_interval: NumericInterval,
|
||||
*,
|
||||
may_wrap: bool = False,
|
||||
supported: bool = True,
|
||||
) -> AbstractTransferResult:
|
||||
return AbstractTransferResult(
|
||||
type_interval,
|
||||
AbstractTransferKind.TOP,
|
||||
may_wrap=may_wrap,
|
||||
supported=supported,
|
||||
)
|
||||
@@ -13,6 +13,11 @@ from slither.analyses.data_flow.analyses.interval.core.tracked_variable import (
|
||||
from slither.analyses.data_flow.analyses.interval.operations.base import (
|
||||
BaseOperationHandler,
|
||||
)
|
||||
from slither.analyses.data_flow.analyses.interval.operations.binary.abstract_transfer import (
|
||||
AbstractTransferKind,
|
||||
AbstractTransferResult,
|
||||
transfer_binary_interval,
|
||||
)
|
||||
from slither.analyses.data_flow.analyses.interval.operations.type_utils import (
|
||||
get_bit_width,
|
||||
get_variable_name,
|
||||
@@ -47,6 +52,19 @@ class ConstraintContext:
|
||||
bit_width: int
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class ArithmeticEvaluation:
|
||||
"""Terms and type metadata produced for one binary operation."""
|
||||
|
||||
result: TrackedSMTVariable
|
||||
left: SMTTerm
|
||||
right: SMTTerm
|
||||
result_term: SMTTerm | None
|
||||
bit_width: int
|
||||
is_signed: bool
|
||||
both_constants: bool
|
||||
|
||||
|
||||
ARITHMETIC_OPERATIONS = frozenset(
|
||||
{
|
||||
BinaryType.ADDITION,
|
||||
@@ -99,8 +117,9 @@ class ArithmeticHandler(BaseOperationHandler):
|
||||
left_term,
|
||||
right_term,
|
||||
result_type,
|
||||
is_self_operation,
|
||||
bit_width,
|
||||
is_self_operation=is_self_operation,
|
||||
bit_width=bit_width,
|
||||
constant_right=self._constant_integer(operation.variable_right),
|
||||
)
|
||||
if result_term is not None:
|
||||
self._register_equation(
|
||||
@@ -110,44 +129,101 @@ class ArithmeticHandler(BaseOperationHandler):
|
||||
result_var.term == result_term,
|
||||
"arithmetic_result",
|
||||
)
|
||||
evaluation = ArithmeticEvaluation(
|
||||
result_var,
|
||||
left_term,
|
||||
right_term,
|
||||
result_term,
|
||||
bit_width,
|
||||
signed,
|
||||
both_constants,
|
||||
)
|
||||
self._add_continuation_constraints(operation, node, domain, evaluation)
|
||||
result_var = self._apply_abstract_result(operation, node, domain, evaluation)
|
||||
domain.state.set_variable(result_name, result_var)
|
||||
self._record_operand_dependencies(operation, result_name, domain)
|
||||
|
||||
def _add_continuation_constraints(
|
||||
self,
|
||||
operation: Binary,
|
||||
node: Node,
|
||||
domain: IntervalDomain,
|
||||
evaluation: ArithmeticEvaluation,
|
||||
) -> None:
|
||||
"""Record operation-local success conditions in the current state."""
|
||||
if operation.type in (BinaryType.DIVISION, BinaryType.MODULO):
|
||||
self._add_divisor_nonzero_constraint(
|
||||
operation,
|
||||
node,
|
||||
right_term,
|
||||
bit_width,
|
||||
evaluation.right,
|
||||
evaluation.bit_width,
|
||||
domain=domain,
|
||||
)
|
||||
if (
|
||||
operation.type is BinaryType.DIVISION
|
||||
and evaluation.is_signed
|
||||
and not evaluation.both_constants
|
||||
):
|
||||
self._add_state_fact(
|
||||
operation,
|
||||
node,
|
||||
domain,
|
||||
self.solver.bv_sdiv_no_overflow(evaluation.left, evaluation.right),
|
||||
"signed_division_no_overflow",
|
||||
kind=FactKind.CHECKED_ARITHMETIC,
|
||||
)
|
||||
if node.scope.is_checked and evaluation.result_term is not None:
|
||||
if evaluation.both_constants:
|
||||
return
|
||||
context = ConstraintContext(
|
||||
evaluation.left,
|
||||
evaluation.right,
|
||||
evaluation.result_term,
|
||||
evaluation.is_signed,
|
||||
evaluation.bit_width,
|
||||
)
|
||||
|
||||
overflow_predicates = self._compute_overflow_predicates(
|
||||
operation.type, left_term, right_term, signed, both_constants
|
||||
)
|
||||
|
||||
is_checked = node.scope.is_checked
|
||||
should_check = is_checked and result_term is not None and not both_constants
|
||||
if should_check:
|
||||
context = ConstraintContext(left_term, right_term, result_term, signed, bit_width)
|
||||
self._assert_checked_constraints(operation, node, context, domain)
|
||||
|
||||
result_interval = self._compute_abstract_result_interval(
|
||||
def _apply_abstract_result(
|
||||
self,
|
||||
operation: Binary,
|
||||
node: Node,
|
||||
domain: IntervalDomain,
|
||||
evaluation: ArithmeticEvaluation,
|
||||
) -> TrackedSMTVariable:
|
||||
"""Attach the abstract interval and deferred unchecked predicates."""
|
||||
is_checked = node.scope.is_checked
|
||||
abstract_result = self._compute_abstract_result_interval(
|
||||
operation,
|
||||
domain,
|
||||
bit_width,
|
||||
signed,
|
||||
is_checked,
|
||||
evaluation.bit_width,
|
||||
evaluation.is_signed,
|
||||
is_checked=is_checked,
|
||||
)
|
||||
result_var = result_var.with_interval(result_interval)
|
||||
result = evaluation.result.with_interval(abstract_result.interval)
|
||||
|
||||
# Store predicates and is_checked flag for deferred overflow checking
|
||||
# Overflow is only possible in unchecked contexts (assembly, unchecked blocks)
|
||||
result_var = result_var.with_overflow_predicates(
|
||||
overflow_predicates = self._compute_overflow_predicates(
|
||||
operation.type,
|
||||
evaluation.left,
|
||||
evaluation.right,
|
||||
is_signed=evaluation.is_signed,
|
||||
both_constants=evaluation.both_constants,
|
||||
)
|
||||
if not is_checked and not abstract_result.may_wrap:
|
||||
overflow_predicates = {"no_overflow": None, "no_underflow": None}
|
||||
has_deferred_overflow_check = any(
|
||||
predicate is not None for predicate in overflow_predicates.values()
|
||||
)
|
||||
|
||||
return result.with_overflow_predicates(
|
||||
**overflow_predicates,
|
||||
operation_id=StaticOperationId.from_operation(operation, node),
|
||||
is_unchecked=not is_checked and not both_constants,
|
||||
is_unchecked=(
|
||||
not is_checked
|
||||
and not evaluation.both_constants
|
||||
and has_deferred_overflow_check
|
||||
),
|
||||
)
|
||||
domain.state.set_variable(result_name, result_var)
|
||||
self._record_operand_dependencies(operation, result_name, domain)
|
||||
|
||||
def _prepare_terms(
|
||||
self,
|
||||
@@ -171,37 +247,40 @@ class ArithmeticHandler(BaseOperationHandler):
|
||||
domain: IntervalDomain,
|
||||
bit_width: int,
|
||||
is_signed: bool,
|
||||
*,
|
||||
is_checked: bool,
|
||||
) -> NumericInterval:
|
||||
"""Compute the existing interval transformer for linear add/sub operations."""
|
||||
) -> AbstractTransferResult:
|
||||
"""Compute a sound non-relational transfer before optional SMT refinement."""
|
||||
type_interval = NumericInterval.type_range(bit_width, is_signed)
|
||||
if self._is_same_operand(operation) and operation.type is BinaryType.SUBTRACTION:
|
||||
return NumericInterval(0, 0)
|
||||
left = self._operand_interval(operation.variable_left, domain, type_interval)
|
||||
right = self._operand_interval(operation.variable_right, domain, type_interval)
|
||||
right = self._operand_interval(
|
||||
operation.variable_right,
|
||||
domain,
|
||||
type_interval,
|
||||
allow_wide=operation.type
|
||||
in (BinaryType.POWER, BinaryType.LEFT_SHIFT, BinaryType.RIGHT_SHIFT),
|
||||
)
|
||||
if left is None or right is None:
|
||||
return type_interval
|
||||
if operation.type is BinaryType.ADDITION:
|
||||
raw = NumericInterval(left.lower + right.lower, left.upper + right.upper)
|
||||
elif operation.type is BinaryType.SUBTRACTION:
|
||||
raw = NumericInterval(left.lower - right.upper, left.upper - right.lower)
|
||||
else:
|
||||
return type_interval
|
||||
if type_interval.lower <= raw.lower and raw.upper <= type_interval.upper:
|
||||
return raw
|
||||
if not is_checked:
|
||||
return type_interval
|
||||
lower = max(type_interval.lower, raw.lower)
|
||||
upper = min(type_interval.upper, raw.upper)
|
||||
if lower > upper:
|
||||
return type_interval
|
||||
return NumericInterval(lower, upper)
|
||||
return AbstractTransferResult(type_interval, kind=AbstractTransferKind.TOP)
|
||||
result = transfer_binary_interval(
|
||||
operation.type,
|
||||
left,
|
||||
right,
|
||||
bit_width=bit_width,
|
||||
is_signed=is_signed,
|
||||
is_checked=is_checked,
|
||||
same_operand=self._is_same_operand(operation),
|
||||
)
|
||||
self._record_abstract_transfer(operation.type, result, is_checked)
|
||||
return result
|
||||
|
||||
@staticmethod
|
||||
def _operand_interval(
|
||||
operand: RVALUE,
|
||||
domain: IntervalDomain,
|
||||
type_interval: NumericInterval,
|
||||
*,
|
||||
allow_wide: bool = False,
|
||||
) -> NumericInterval | None:
|
||||
if isinstance(operand, Constant):
|
||||
value = operand.value
|
||||
@@ -209,7 +288,7 @@ class ArithmeticHandler(BaseOperationHandler):
|
||||
value = int(value)
|
||||
if not isinstance(value, int):
|
||||
return None
|
||||
if not type_interval.lower <= value <= type_interval.upper:
|
||||
if not allow_wide and not type_interval.lower <= value <= type_interval.upper:
|
||||
return None
|
||||
return NumericInterval(value, value)
|
||||
tracked = domain.state.get_variable(get_variable_name(operand))
|
||||
@@ -217,6 +296,30 @@ class ArithmeticHandler(BaseOperationHandler):
|
||||
return None
|
||||
return tracked.interval
|
||||
|
||||
@staticmethod
|
||||
def _record_abstract_transfer(
|
||||
operation_type: BinaryType,
|
||||
result: AbstractTransferResult,
|
||||
is_checked: bool,
|
||||
) -> None:
|
||||
from slither.analyses.data_flow.smt_solver.telemetry import get_telemetry
|
||||
|
||||
telemetry = get_telemetry()
|
||||
if telemetry is None or not telemetry.enabled:
|
||||
return
|
||||
telemetry.count(f"abstract_transfer_{operation_type.name.lower()}")
|
||||
telemetry.count(f"abstract_transfer_{result.kind.value}")
|
||||
telemetry.count("abstract_transfer_checked" if is_checked else "abstract_transfer_unchecked")
|
||||
|
||||
@staticmethod
|
||||
def _constant_integer(operand: RVALUE) -> int | None:
|
||||
if not isinstance(operand, Constant):
|
||||
return None
|
||||
value = operand.value
|
||||
if isinstance(value, bool):
|
||||
return int(value)
|
||||
return value if isinstance(value, int) else None
|
||||
|
||||
def _record_operand_dependencies(
|
||||
self,
|
||||
operation: Binary,
|
||||
@@ -263,6 +366,7 @@ class ArithmeticHandler(BaseOperationHandler):
|
||||
operation_type: BinaryType,
|
||||
left_term: SMTTerm,
|
||||
right_term: SMTTerm,
|
||||
*,
|
||||
is_signed: bool,
|
||||
both_constants: bool,
|
||||
) -> dict[str, SMTTerm | None]:
|
||||
@@ -482,6 +586,7 @@ class ArithmeticHandler(BaseOperationHandler):
|
||||
node: Node,
|
||||
divisor: SMTTerm,
|
||||
bit_width: int,
|
||||
*,
|
||||
domain: IntervalDomain,
|
||||
) -> None:
|
||||
"""Add divisor nonzero constraint as path constraint (division by zero reverts)."""
|
||||
@@ -536,8 +641,10 @@ class ArithmeticHandler(BaseOperationHandler):
|
||||
left: SMTTerm,
|
||||
right: SMTTerm,
|
||||
result_type: ElementaryType,
|
||||
*,
|
||||
is_self_operation: bool = False,
|
||||
bit_width: int = 256,
|
||||
constant_right: int | None = None,
|
||||
) -> SMTTerm | None:
|
||||
"""Compute the result term for the operation."""
|
||||
signed = is_signed_type(result_type)
|
||||
@@ -556,14 +663,27 @@ class ArithmeticHandler(BaseOperationHandler):
|
||||
BinaryType.MULTIPLICATION: lambda: self.solver.bv_mul(left, right),
|
||||
BinaryType.DIVISION: lambda: self._division(left, right, signed),
|
||||
BinaryType.MODULO: lambda: self._modulo(left, right, signed),
|
||||
BinaryType.LEFT_SHIFT: lambda: self.solver.bv_shl(left, right),
|
||||
BinaryType.RIGHT_SHIFT: lambda: self._right_shift(left, right, signed),
|
||||
BinaryType.AND: lambda: self.solver.bv_and(left, right),
|
||||
BinaryType.OR: lambda: self.solver.bv_or(left, right),
|
||||
BinaryType.CARET: lambda: self.solver.bv_xor(left, right),
|
||||
BinaryType.POWER: lambda: self._power(left, right),
|
||||
}
|
||||
|
||||
if operation_type in (BinaryType.LEFT_SHIFT, BinaryType.RIGHT_SHIFT):
|
||||
if constant_right is None or constant_right < 0:
|
||||
return None
|
||||
shift = self.solver.create_constant(
|
||||
min(constant_right, bit_width),
|
||||
Sort(SortKind.BITVEC, [bit_width]),
|
||||
)
|
||||
if operation_type is BinaryType.LEFT_SHIFT:
|
||||
return self.solver.bv_shl(left, shift)
|
||||
return self._right_shift(left, shift, signed)
|
||||
if operation_type is BinaryType.POWER:
|
||||
# There is no backend-neutral bit-vector exponent operator. The
|
||||
# abstract transfer remains authoritative instead of registering
|
||||
# a wrapped equation that lacks checked-overflow semantics.
|
||||
return None
|
||||
|
||||
handler = dispatch.get(operation_type)
|
||||
if handler is None:
|
||||
return None
|
||||
@@ -621,11 +741,3 @@ class ArithmeticHandler(BaseOperationHandler):
|
||||
if is_signed:
|
||||
return self.solver.bv_ashr(left, right)
|
||||
return self.solver.bv_lshr(left, right)
|
||||
|
||||
def _power(self, base: SMTTerm, exponent: SMTTerm) -> SMTTerm:
|
||||
"""Power operation (simplified - returns base * exponent for now).
|
||||
|
||||
Full power implementation requires iterative multiplication.
|
||||
"""
|
||||
# TODO: Implement proper power operation with iterative multiplication
|
||||
return self.solver.bv_mul(base, exponent)
|
||||
|
||||
@@ -2,7 +2,7 @@
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from typing import TYPE_CHECKING
|
||||
from typing import TYPE_CHECKING, cast
|
||||
|
||||
from slither.analyses.data_flow.analyses.interval.core.tracked_variable import (
|
||||
NumericInterval,
|
||||
@@ -23,11 +23,19 @@ from slither.slithir.operations.phi import Phi
|
||||
|
||||
|
||||
if TYPE_CHECKING:
|
||||
from slither.analyses.data_flow.analyses.interval.analysis.loop import (
|
||||
IntervalLoopMetadata,
|
||||
)
|
||||
from slither.analyses.data_flow.analyses.interval.analysis.domain import (
|
||||
IntervalDomain,
|
||||
)
|
||||
from slither.analyses.data_flow.analyses.interval.core.state import State
|
||||
from slither.core.cfg.node import Node
|
||||
from slither.slithir.utils.utils import RVALUE
|
||||
from slither.slithir.operations.operation import Operation
|
||||
from slither.slithir.utils.utils import LVALUE, RVALUE
|
||||
from slither.analyses.data_flow.smt_solver.solver import SMTSolver
|
||||
|
||||
from slither.analyses.data_flow.smt_solver.facts import LoopHeaderId
|
||||
|
||||
|
||||
class PhiHandler(BaseOperationHandler):
|
||||
@@ -37,20 +45,26 @@ class PhiHandler(BaseOperationHandler):
|
||||
interprocedural SSA, function entry Phi nodes merge values from ALL
|
||||
call sites.
|
||||
|
||||
Strategy:
|
||||
1. If lvalue already tracked from parameter binding -> preserve it
|
||||
2. At loop headers: selective widening based on comparing incoming to existing
|
||||
3. If rvalues are tracked -> create variable equal to one of them (disjunction)
|
||||
4. If no rvalues tracked -> create unconstrained variable
|
||||
Loop-header values are recomputed from the currently reachable incoming SSA
|
||||
alternatives. The loop fixpoint owns widening and generation state.
|
||||
"""
|
||||
|
||||
def __init__(self, solver: SMTSolver) -> None:
|
||||
super().__init__(solver)
|
||||
self._loop_metadata: IntervalLoopMetadata | None = None
|
||||
|
||||
def configure_loop_metadata(self, metadata: IntervalLoopMetadata) -> None:
|
||||
"""Bind traversal-independent loop SSA classifications."""
|
||||
self._loop_metadata = metadata
|
||||
|
||||
def handle(
|
||||
self,
|
||||
operation: Phi,
|
||||
operation: Operation,
|
||||
domain: IntervalDomain,
|
||||
node: Node,
|
||||
) -> None:
|
||||
"""Process Phi operation by merging incoming values."""
|
||||
operation, state = self._require_phi_state(operation, domain)
|
||||
if operation.lvalue is None:
|
||||
return
|
||||
|
||||
@@ -58,16 +72,15 @@ class PhiHandler(BaseOperationHandler):
|
||||
if not isinstance(lvalue_type, ElementaryType):
|
||||
return
|
||||
|
||||
result_name = get_variable_name(operation.lvalue)
|
||||
is_loop_header = node.type == NodeType.IFLOOP
|
||||
result_name = get_variable_name(cast("LVALUE", operation.lvalue))
|
||||
is_loop_header = self._is_loop_header(node)
|
||||
|
||||
# At loop headers: create unconstrained (widening handled by apply_widening)
|
||||
if is_loop_header:
|
||||
self._handle_loop_header_phi(domain, result_name, lvalue_type)
|
||||
self._handle_loop_header_phi(operation, domain, node, result_name, lvalue_type)
|
||||
return
|
||||
|
||||
# If already tracked (from parameter binding), preserve those constraints
|
||||
existing = domain.state.get_variable(result_name)
|
||||
existing = state.get_variable(result_name)
|
||||
if existing is not None:
|
||||
return
|
||||
|
||||
@@ -98,7 +111,26 @@ class PhiHandler(BaseOperationHandler):
|
||||
equation_variables,
|
||||
)
|
||||
|
||||
domain.state.set_variable(result_name, result_variable)
|
||||
state.set_variable(result_name, result_variable)
|
||||
|
||||
def _is_loop_header(self, node: Node) -> bool:
|
||||
"""Use natural-loop metadata when the engine has prepared the handler."""
|
||||
if self._loop_metadata is None:
|
||||
return node.type is NodeType.IFLOOP
|
||||
return self._loop_metadata.is_loop_header(LoopHeaderId.from_node(node))
|
||||
|
||||
@staticmethod
|
||||
def _require_phi_state(
|
||||
operation: Operation,
|
||||
domain: IntervalDomain,
|
||||
) -> tuple[Phi, State]:
|
||||
"""Validate the registry dispatch and concrete transfer state."""
|
||||
if not isinstance(operation, Phi):
|
||||
raise TypeError("PhiHandler requires a Phi operation")
|
||||
state = domain.state
|
||||
if state is None:
|
||||
raise ValueError("Phi transfer requires a concrete interval state")
|
||||
return operation, state
|
||||
|
||||
@staticmethod
|
||||
def _incoming_interval(incoming: list[TrackedSMTVariable]) -> NumericInterval:
|
||||
@@ -110,35 +142,55 @@ class PhiHandler(BaseOperationHandler):
|
||||
|
||||
def _handle_loop_header_phi(
|
||||
self,
|
||||
operation: Phi,
|
||||
domain: IntervalDomain,
|
||||
node: Node,
|
||||
result_name: str,
|
||||
lvalue_type: ElementaryType,
|
||||
) -> None:
|
||||
"""Handle phi at loop header.
|
||||
|
||||
Creates unconstrained variable. Selective widening is handled by
|
||||
apply_widening() on back edges.
|
||||
|
||||
NOTE: We cannot add constraints here because SMT constraints are permanent.
|
||||
get_or_declare_const returns the same SMT variable, so constraints from
|
||||
earlier iterations accumulate. This makes loop exits unreachable if we
|
||||
constrain phi variables to incoming values.
|
||||
"""
|
||||
"""Recompute a loop phi without creating a cyclic immutable equation."""
|
||||
state = domain.state
|
||||
if state is None:
|
||||
raise ValueError("Loop phi transfer requires a concrete interval state")
|
||||
sort = type_to_sort(lvalue_type)
|
||||
is_signed = is_signed_type(lvalue_type)
|
||||
bit_width = get_bit_width(lvalue_type)
|
||||
|
||||
existing = domain.state.get_variable(result_name)
|
||||
|
||||
# First iteration: create unconstrained variable
|
||||
if existing is None:
|
||||
result_variable = TrackedSMTVariable.create(
|
||||
self.solver, result_name, sort, is_signed=is_signed, bit_width=bit_width
|
||||
result_variable = TrackedSMTVariable.create(
|
||||
self.solver, result_name, sort, is_signed=is_signed, bit_width=bit_width
|
||||
)
|
||||
incoming = self._active_loop_incoming(operation, domain, node, result_name)
|
||||
if incoming:
|
||||
result_variable = result_variable.with_interval(
|
||||
self._incoming_interval(incoming),
|
||||
is_total=True,
|
||||
)
|
||||
domain.state.set_variable(result_name, result_variable)
|
||||
return
|
||||
state.set_variable(result_name, result_variable)
|
||||
|
||||
# Later iterations: keep existing (widening handled by apply_widening)
|
||||
def _active_loop_incoming(
|
||||
self,
|
||||
operation: Phi,
|
||||
domain: IntervalDomain,
|
||||
node: Node,
|
||||
result_name: str,
|
||||
) -> list[TrackedSMTVariable]:
|
||||
"""Resolve every currently active phi alternative or return no precision."""
|
||||
state = domain.state
|
||||
if state is None:
|
||||
raise ValueError("Loop phi lookup requires a concrete interval state")
|
||||
if self._loop_metadata is None:
|
||||
incoming = self._get_incoming_variables(operation.rvalues, domain)
|
||||
return incoming if len(incoming) == len(operation.rvalues) else []
|
||||
bindings = self._loop_metadata.variables_for(LoopHeaderId.from_node(node))
|
||||
binding = next((item for item in bindings if item.header_name == result_name), None)
|
||||
if binding is None:
|
||||
return []
|
||||
active_names = binding.entry_names
|
||||
if state.get_variable(result_name) is not None:
|
||||
active_names = (*active_names, *binding.back_names)
|
||||
incoming = [state.get_variable(name) for name in active_names]
|
||||
if any(variable is None for variable in incoming):
|
||||
return []
|
||||
return [variable for variable in incoming if variable is not None]
|
||||
|
||||
def _get_incoming_variables(
|
||||
self,
|
||||
@@ -146,10 +198,13 @@ class PhiHandler(BaseOperationHandler):
|
||||
domain: IntervalDomain,
|
||||
) -> list[TrackedSMTVariable]:
|
||||
"""Get tracked variables for Phi incoming values."""
|
||||
state = domain.state
|
||||
if state is None:
|
||||
raise ValueError("Phi input lookup requires a concrete interval state")
|
||||
tracked_variables = []
|
||||
for rvalue in rvalues:
|
||||
rvalue_name = get_variable_name(rvalue)
|
||||
tracked = domain.state.get_variable(rvalue_name)
|
||||
tracked = state.get_variable(rvalue_name)
|
||||
if tracked is not None:
|
||||
tracked_variables.append(tracked)
|
||||
return tracked_variables
|
||||
@@ -160,10 +215,13 @@ class PhiHandler(BaseOperationHandler):
|
||||
domain: IntervalDomain,
|
||||
) -> list[TrackedSMTVariable]:
|
||||
"""Return all static phi alternatives, declaring absent symbols locally."""
|
||||
state = domain.state
|
||||
if state is None:
|
||||
raise ValueError("Phi equation lookup requires a concrete interval state")
|
||||
variables = []
|
||||
for rvalue in rvalues:
|
||||
name = get_variable_name(rvalue)
|
||||
tracked = domain.state.get_variable(name)
|
||||
tracked = state.get_variable(name)
|
||||
value_type = getattr(rvalue, "type", None)
|
||||
if tracked is None and isinstance(value_type, ElementaryType):
|
||||
tracked = TrackedSMTVariable.create(
|
||||
|
||||
@@ -95,6 +95,9 @@ from slither.analyses.data_flow.analyses.interval.operations.unpack import (
|
||||
from slither.analyses.data_flow.logger import get_logger
|
||||
|
||||
if TYPE_CHECKING:
|
||||
from slither.analyses.data_flow.analyses.interval.analysis.loop import (
|
||||
IntervalLoopMetadata,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.solver import SMTSolver
|
||||
|
||||
logger = get_logger()
|
||||
@@ -103,7 +106,7 @@ logger = get_logger()
|
||||
class OperationHandlerRegistry:
|
||||
"""Maps operation types to handlers."""
|
||||
|
||||
def __init__(self, solver: "SMTSolver"):
|
||||
def __init__(self, solver: SMTSolver):
|
||||
self._solver = solver
|
||||
self._handlers: dict[type[Operation], BaseOperationHandler] = {}
|
||||
self._register_handlers()
|
||||
@@ -135,10 +138,16 @@ class OperationHandlerRegistry:
|
||||
def get_handler(self, op_type: type[Operation]) -> BaseOperationHandler:
|
||||
"""Get handler for operation type."""
|
||||
if op_type not in self._handlers:
|
||||
implemented = [handler.__name__ for handler in self._handlers.keys()]
|
||||
implemented = [handler.__name__ for handler in self._handlers]
|
||||
logger.error_and_raise(
|
||||
f"Operation '{op_type.__name__}' is not implemented. "
|
||||
f"Implemented: {implemented}",
|
||||
f"Operation '{op_type.__name__}' is not implemented. Implemented: {implemented}",
|
||||
NotImplementedError,
|
||||
)
|
||||
return self._handlers[op_type]
|
||||
|
||||
def configure_loop_metadata(self, metadata: IntervalLoopMetadata) -> None:
|
||||
"""Provide stable loop-carried bindings to the phi handler."""
|
||||
handler = self._handlers[Phi]
|
||||
if not isinstance(handler, PhiHandler):
|
||||
raise TypeError("Phi registry entry is not a PhiHandler")
|
||||
handler.configure_loop_metadata(metadata)
|
||||
|
||||
@@ -16,7 +16,9 @@ from slither.analyses.data_flow.smt_solver.facts import (
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.query import (
|
||||
FeasibilityStatus,
|
||||
QueryBudget,
|
||||
QueryPurpose,
|
||||
RangeInterval,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.solver import SMTSolver
|
||||
from slither.analyses.data_flow.smt_solver.telemetry import SolverTelemetry, get_telemetry
|
||||
@@ -44,6 +46,8 @@ class RangeQueryConfig:
|
||||
skip_optimization: bool = False
|
||||
debug: bool = False
|
||||
cache: RangeQueryCache | None = None
|
||||
refine_abstract: bool = False
|
||||
budget: QueryBudget | None = None
|
||||
|
||||
|
||||
@dataclass
|
||||
@@ -77,6 +81,7 @@ def _check_overflow_possible(
|
||||
state_facts: tuple[Fact[SMTTerm], ...] = (),
|
||||
query_facts: tuple[Fact[SMTTerm], ...] = (),
|
||||
timeout_ms: int = 500,
|
||||
budget: QueryBudget | None = None,
|
||||
) -> bool:
|
||||
"""Check if overflow or underflow is possible for a variable.
|
||||
|
||||
@@ -104,14 +109,17 @@ def _check_overflow_possible(
|
||||
0,
|
||||
state_id.context_id if state_id is not None else None,
|
||||
)
|
||||
effective_timeout = budget.remaining_ms() if budget is not None else timeout_ms
|
||||
if effective_timeout == 0:
|
||||
return True
|
||||
result = solver.check_feasibility(
|
||||
state_id=state_id,
|
||||
state_facts=state_facts,
|
||||
query_facts=(*query_facts, predicate_fact),
|
||||
purpose=QueryPurpose.OVERFLOW,
|
||||
timeout_ms=timeout_ms,
|
||||
timeout_ms=effective_timeout,
|
||||
)
|
||||
return result.status is FeasibilityStatus.SAT
|
||||
return result.status is not FeasibilityStatus.UNSAT
|
||||
|
||||
|
||||
# =============================================================================
|
||||
@@ -233,7 +241,13 @@ def _solve_range_with_solver(
|
||||
config: RangeQueryConfig,
|
||||
) -> tuple[dict | None, dict | None]:
|
||||
"""Use solver's range solving to find min/max values."""
|
||||
if ctx.telemetry:
|
||||
budget = config.budget or QueryBudget(config.timeout_ms)
|
||||
abstract_range = _preferred_abstract_range(ctx.smt_var, config)
|
||||
query_facts = (
|
||||
*ctx.query_facts,
|
||||
*_abstract_refinement_facts(ctx, meta, config.refine_abstract),
|
||||
)
|
||||
if ctx.telemetry and abstract_range is None:
|
||||
ctx.telemetry.count("optimize_min")
|
||||
ctx.telemetry.count("optimize_max")
|
||||
|
||||
@@ -242,9 +256,12 @@ def _solve_range_with_solver(
|
||||
term=ctx.smt_var.term,
|
||||
state_id=ctx.state_id,
|
||||
state_facts=ctx.state_facts,
|
||||
query_facts=ctx.query_facts,
|
||||
query_facts=query_facts,
|
||||
timeout_ms=config.timeout_ms,
|
||||
signed=meta.is_signed,
|
||||
fallback_range=_tracked_fallback_range(ctx.smt_var),
|
||||
abstract_range=abstract_range,
|
||||
budget=budget,
|
||||
)
|
||||
|
||||
if result.feasibility is FeasibilityStatus.UNSAT:
|
||||
@@ -261,15 +278,10 @@ def _solve_range_with_solver(
|
||||
decoded_max = _decode_model_value(result.upper, meta)
|
||||
|
||||
# Check if overflow is possible given constraints
|
||||
has_overflow = _check_overflow_possible(
|
||||
ctx.solver,
|
||||
ctx.smt_var,
|
||||
state_id=ctx.state_id,
|
||||
state_facts=ctx.state_facts,
|
||||
query_facts=ctx.query_facts,
|
||||
timeout_ms=config.timeout_ms,
|
||||
has_overflow = (
|
||||
ctx.smt_var.is_unchecked
|
||||
and (ctx.smt_var.no_overflow is not None or ctx.smt_var.no_underflow is not None)
|
||||
)
|
||||
|
||||
min_result = {
|
||||
"value": decoded_min,
|
||||
"overflow": has_overflow,
|
||||
@@ -288,6 +300,53 @@ def _solve_range_with_solver(
|
||||
return None, None
|
||||
|
||||
|
||||
def _abstract_refinement_facts(
|
||||
ctx: RangeSolveContext,
|
||||
meta: VariableMetadata,
|
||||
enabled: bool,
|
||||
) -> tuple[Fact[SMTTerm], ...]:
|
||||
"""Materialize state-owned interval limits for an optional refinement."""
|
||||
if not enabled or not ctx.smt_var.is_total:
|
||||
return ()
|
||||
interval = ctx.smt_var.interval
|
||||
lower = ctx.solver.create_constant(interval.lower, ctx.smt_var.sort)
|
||||
upper = ctx.solver.create_constant(interval.upper, ctx.smt_var.sort)
|
||||
if meta.is_signed:
|
||||
predicates = (
|
||||
ctx.solver.bv_sge(ctx.smt_var.term, lower),
|
||||
ctx.solver.bv_sle(ctx.smt_var.term, upper),
|
||||
)
|
||||
else:
|
||||
predicates = (
|
||||
ctx.solver.bv_uge(ctx.smt_var.term, lower),
|
||||
ctx.solver.bv_ule(ctx.smt_var.term, upper),
|
||||
)
|
||||
context_id = ctx.state_id.context_id if ctx.state_id is not None else None
|
||||
return tuple(
|
||||
make_query_fact(predicate, "abstract_refinement_bound", index, context_id)
|
||||
for index, predicate in enumerate(predicates)
|
||||
)
|
||||
|
||||
|
||||
def _preferred_abstract_range(
|
||||
smt_var: TrackedSMTVariable,
|
||||
config: RangeQueryConfig,
|
||||
) -> RangeInterval | None:
|
||||
"""Select terminal abstract transfer when refinement is unnecessary."""
|
||||
if config.refine_abstract or not smt_var.is_total:
|
||||
return None
|
||||
interval = smt_var.interval
|
||||
if interval != smt_var.type_interval or smt_var.overflow_operation_id is not None:
|
||||
return RangeInterval(interval.lower, interval.upper)
|
||||
return None
|
||||
|
||||
|
||||
def _tracked_fallback_range(smt_var: TrackedSMTVariable) -> RangeInterval:
|
||||
"""Return the strongest state-owned interval valid for failed objectives."""
|
||||
interval = smt_var.interval if smt_var.is_total else smt_var.type_interval
|
||||
return RangeInterval(interval.lower, interval.upper)
|
||||
|
||||
|
||||
# =============================================================================
|
||||
# RANGE SOLVING
|
||||
# =============================================================================
|
||||
|
||||
@@ -13,6 +13,12 @@ from slither.slithir.operations.condition import Condition
|
||||
from slither.slithir.operations.operation import Operation
|
||||
|
||||
if TYPE_CHECKING:
|
||||
from slither.analyses.data_flow.engine.loop import (
|
||||
LoopVariableId,
|
||||
LoopWideningContext,
|
||||
LoopWideningResult,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.facts import LoopHeaderId
|
||||
from slither.core.declarations.function import Function
|
||||
|
||||
|
||||
@@ -52,9 +58,7 @@ class Analysis(ABC):
|
||||
def bottom_value(self) -> Domain:
|
||||
"""Return the bottom value of the domain for initialization."""
|
||||
|
||||
def apply_condition(
|
||||
self, domain: Domain, condition: Condition, branch_taken: bool
|
||||
) -> Domain:
|
||||
def apply_condition(self, domain: Domain, condition: Condition, branch_taken: bool) -> Domain:
|
||||
"""Apply branch-specific filtering based on a condition.
|
||||
|
||||
Override to implement path-sensitive analysis that constrains
|
||||
@@ -88,6 +92,17 @@ class Analysis(ABC):
|
||||
"""
|
||||
return current_state
|
||||
|
||||
def apply_loop_widening(self, context: "LoopWideningContext") -> "LoopWideningResult":
|
||||
"""Widen one dominator-classified loop-header generation."""
|
||||
from slither.analyses.data_flow.engine.loop import LoopWideningResult
|
||||
|
||||
state = self.apply_widening(context.current_input, context.previous_input, set())
|
||||
return LoopWideningResult(state)
|
||||
|
||||
def loop_variables(self, header_id: "LoopHeaderId") -> tuple["LoopVariableId", ...]:
|
||||
"""Return static loop-carried bindings for one natural-loop header."""
|
||||
return ()
|
||||
|
||||
def prepare_for_function(self, function: "Function") -> None:
|
||||
"""Prepare analysis for a specific function.
|
||||
|
||||
|
||||
@@ -8,10 +8,17 @@ from abc import ABC, abstractmethod
|
||||
from collections import deque
|
||||
from typing import TYPE_CHECKING
|
||||
|
||||
from slither.analyses.data_flow.engine.domain import Domain
|
||||
|
||||
if TYPE_CHECKING:
|
||||
from slither.analyses.data_flow.engine.analysis import A, Analysis, AnalysisState
|
||||
from slither.core.declarations.function import Function
|
||||
|
||||
from slither.analyses.data_flow.engine.loop import (
|
||||
ControlFlowEdgeId,
|
||||
LoopHeaderFixpoint,
|
||||
LoopStructure,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.telemetry import get_telemetry
|
||||
from slither.core.cfg.node import Node, NodeType
|
||||
from slither.slithir.operations.condition import Condition
|
||||
@@ -29,6 +36,10 @@ class Direction(ABC):
|
||||
def IS_FORWARD(self) -> bool:
|
||||
"""Return True for forward analysis, False for backward."""
|
||||
|
||||
def prepare_for_function(self, function: "Function") -> None:
|
||||
"""Reset function-specific traversal metadata."""
|
||||
return None
|
||||
|
||||
@abstractmethod
|
||||
def apply_transfer_function(
|
||||
self,
|
||||
@@ -58,6 +69,26 @@ class Forward(Direction):
|
||||
|
||||
def __init__(self) -> None:
|
||||
"""Initialize forward direction."""
|
||||
self._loops = LoopStructure()
|
||||
self._loop_fixpoints: dict[int, LoopHeaderFixpoint] = {}
|
||||
|
||||
def prepare_for_function(self, function: "Function") -> None:
|
||||
"""Classify natural loops before worklist traversal starts."""
|
||||
self._loops = LoopStructure.from_function(function)
|
||||
self._loop_fixpoints = {}
|
||||
telemetry = get_telemetry()
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_loop_headers(len(self._loops.loops))
|
||||
|
||||
@property
|
||||
def loop_structure(self) -> LoopStructure:
|
||||
"""Return deterministic loop metadata for the active function."""
|
||||
return self._loops
|
||||
|
||||
@property
|
||||
def loop_fixpoints(self) -> tuple[LoopHeaderFixpoint, ...]:
|
||||
"""Return loop trackers ordered by header node ID."""
|
||||
return tuple(self._loop_fixpoints[node_id] for node_id in sorted(self._loop_fixpoints))
|
||||
|
||||
@property
|
||||
def IS_FORWARD(self) -> bool:
|
||||
@@ -72,65 +103,88 @@ class Forward(Direction):
|
||||
worklist: deque[Node],
|
||||
global_state: dict[int, "AnalysisState[A]"],
|
||||
) -> None:
|
||||
"""Transfer one node and propagate each complete outgoing state."""
|
||||
input_domain = current_state.pre
|
||||
output_domain = input_domain.deep_copy()
|
||||
|
||||
# Apply transfer function to an exclusive output builder.
|
||||
condition_op: Condition | None = None
|
||||
for operation in node.irs_ssa or [None]:
|
||||
analysis.transfer_function(node=node, domain=output_domain, operation=operation)
|
||||
# Track the Condition operation if present
|
||||
if isinstance(operation, Condition):
|
||||
condition_op = operation
|
||||
|
||||
# Set post state
|
||||
global_state[node.node_id].post = output_domain
|
||||
self._record_loop_output(node, output_domain)
|
||||
|
||||
# Check if this is a conditional node with exactly 2 successors
|
||||
is_conditional = (
|
||||
node.type in (NodeType.IF, NodeType.IFLOOP)
|
||||
and condition_op is not None
|
||||
and len(node.sons) == 2
|
||||
)
|
||||
|
||||
# Propagate to successors with condition filtering if applicable
|
||||
for i, successor in enumerate(node.sons):
|
||||
if not successor or successor.node_id not in global_state:
|
||||
continue
|
||||
outgoing = output_domain
|
||||
if is_conditional and condition_op is not None:
|
||||
outgoing = analysis.apply_condition(output_domain, condition_op, i == 0)
|
||||
changed = self._propagate_edge(
|
||||
analysis,
|
||||
node,
|
||||
successor,
|
||||
outgoing,
|
||||
global_state[successor.node_id],
|
||||
)
|
||||
self._schedule(successor, changed, worklist)
|
||||
|
||||
son_state = global_state[successor.node_id]
|
||||
def _record_loop_output(self, node: Node, output: "Domain") -> None:
|
||||
tracker = self._loop_fixpoints.get(node.node_id)
|
||||
if tracker is not None:
|
||||
tracker.record_output(output)
|
||||
|
||||
# Detect back edge: propagating to a loop header (IFLOOP)
|
||||
is_back_edge = successor.type == NodeType.IFLOOP
|
||||
def _propagate_edge(
|
||||
self,
|
||||
analysis: "Analysis",
|
||||
source: Node,
|
||||
destination: Node,
|
||||
outgoing: "Domain",
|
||||
destination_state: "AnalysisState",
|
||||
) -> bool:
|
||||
loop = self._loops.header(destination.node_id)
|
||||
if loop is None:
|
||||
return destination_state.pre.join(outgoing)
|
||||
tracker = self._loop_fixpoints.setdefault(
|
||||
destination.node_id,
|
||||
LoopHeaderFixpoint(loop.header_id, analysis.loop_variables(loop.header_id)),
|
||||
)
|
||||
edge = ControlFlowEdgeId(source.node_id, destination.node_id)
|
||||
is_back_edge = self._loops.is_back_edge(edge)
|
||||
telemetry = get_telemetry()
|
||||
if telemetry is not None and telemetry.enabled and is_back_edge:
|
||||
telemetry.record_back_edge()
|
||||
generation_before = tracker.generation
|
||||
facts_before = tracker.generation_fact_ids
|
||||
update = tracker.update(edge, outgoing, is_back_edge, analysis)
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_loop_update(
|
||||
header_key=repr(tracker.header_id),
|
||||
is_back_edge=is_back_edge,
|
||||
changed=update.changed,
|
||||
generation_advanced=tracker.generation > generation_before,
|
||||
facts_replaced=tracker.generation_fact_ids != facts_before,
|
||||
live_generation_facts=len(tracker.generation_fact_ids),
|
||||
)
|
||||
if update.changed and update.state is not None:
|
||||
destination_state.pre = update.state
|
||||
return update.changed
|
||||
|
||||
if is_conditional:
|
||||
# sons[0] is then branch, sons[1] is else branch
|
||||
branch_taken = i == 0
|
||||
filtered_domain = analysis.apply_condition(
|
||||
output_domain, condition_op, branch_taken
|
||||
)
|
||||
# Widen on back edges before joining
|
||||
if is_back_edge:
|
||||
filtered_domain = analysis.apply_widening(filtered_domain, son_state.pre, set())
|
||||
changed = son_state.pre.join(filtered_domain)
|
||||
else:
|
||||
state_to_propagate = output_domain
|
||||
# Widen on back edges before joining
|
||||
if is_back_edge:
|
||||
state_to_propagate = analysis.apply_widening(
|
||||
state_to_propagate, son_state.pre, set()
|
||||
)
|
||||
changed = son_state.pre.join(state_to_propagate)
|
||||
|
||||
if changed and successor not in worklist:
|
||||
worklist.append(successor)
|
||||
telemetry = get_telemetry()
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_worklist_enqueue(len(worklist))
|
||||
elif not changed:
|
||||
telemetry = get_telemetry()
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_transfer_rerun_prevented()
|
||||
@staticmethod
|
||||
def _schedule(successor: Node, changed: bool, worklist: deque[Node]) -> None:
|
||||
telemetry = get_telemetry()
|
||||
if changed and successor not in worklist:
|
||||
worklist.append(successor)
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_worklist_enqueue(len(worklist))
|
||||
elif not changed and telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_transfer_rerun_prevented()
|
||||
|
||||
|
||||
class Backward(Direction):
|
||||
|
||||
@@ -4,18 +4,26 @@ Implements the generic fixpoint computation framework for
|
||||
both forward and backward data flow analyses.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import time
|
||||
from collections import defaultdict, deque
|
||||
from typing import Generic
|
||||
from typing import TYPE_CHECKING, Generic
|
||||
|
||||
from slither.analyses.data_flow.engine.analysis import A, Analysis, AnalysisState
|
||||
from slither.analyses.data_flow.engine.loop import LoopStructure
|
||||
from slither.analyses.data_flow.logger import get_logger
|
||||
from slither.analyses.data_flow.smt_solver.telemetry import get_telemetry
|
||||
from slither.core.cfg.node import Node
|
||||
from slither.core.declarations.function import Function
|
||||
|
||||
if TYPE_CHECKING:
|
||||
from slither.analyses.data_flow.smt_solver.telemetry import SolverTelemetry
|
||||
|
||||
|
||||
logger = get_logger()
|
||||
MAX_ANALYSIS_ITERATIONS = 10_000
|
||||
PROGRESS_INTERVAL_SECONDS = 5.0
|
||||
|
||||
|
||||
class Engine(Generic[A]):
|
||||
@@ -47,7 +55,7 @@ class Engine(Generic[A]):
|
||||
self.last_progress_time: float = 0.0
|
||||
|
||||
@classmethod
|
||||
def new(cls, analysis: Analysis, function: Function) -> "Engine[A]":
|
||||
def new(cls, analysis: Analysis, function: Function) -> Engine[A]:
|
||||
"""Create a new engine for analyzing a function.
|
||||
|
||||
Args:
|
||||
@@ -63,6 +71,7 @@ class Engine(Generic[A]):
|
||||
|
||||
# Allow analysis to prepare for this function (e.g., collect thresholds)
|
||||
analysis.prepare_for_function(function)
|
||||
analysis.direction().prepare_for_function(function)
|
||||
|
||||
# Create state mapping for nodes in this single function only
|
||||
for node in function.nodes:
|
||||
@@ -111,125 +120,21 @@ class Engine(Generic[A]):
|
||||
)
|
||||
|
||||
def _count_loops(self, function: Function) -> int:
|
||||
"""Count loops by detecting back edges in the CFG."""
|
||||
if not function.nodes:
|
||||
return 0
|
||||
|
||||
visited: set[int] = set()
|
||||
in_stack: set[int] = set()
|
||||
back_edges = 0
|
||||
|
||||
def dfs(node: Node) -> None:
|
||||
nonlocal back_edges
|
||||
visited.add(node.node_id)
|
||||
in_stack.add(node.node_id)
|
||||
|
||||
for successor in node.sons:
|
||||
if successor.node_id not in visited:
|
||||
dfs(successor)
|
||||
elif successor.node_id in in_stack:
|
||||
# Back edge found - indicates a loop
|
||||
back_edges += 1
|
||||
|
||||
in_stack.remove(node.node_id)
|
||||
|
||||
entry = function.entry_point
|
||||
if entry is not None:
|
||||
dfs(entry)
|
||||
|
||||
return back_edges
|
||||
"""Count stable dominator-classified natural-loop headers."""
|
||||
return len(LoopStructure.from_function(function).loops)
|
||||
|
||||
def run_analysis(self) -> None:
|
||||
"""Run the worklist algorithm until fixpoint is reached."""
|
||||
worklist: deque[Node] = deque()
|
||||
|
||||
# Instrumentation constants
|
||||
MAX_ITERATIONS = 10000
|
||||
PROGRESS_INTERVAL = 5.0 # seconds
|
||||
|
||||
# Initialize timing
|
||||
self.start_time = time.time()
|
||||
self.last_progress_time = self.start_time
|
||||
self.iteration_count = 0
|
||||
self.node_visit_count.clear()
|
||||
|
||||
if self.analysis.direction().IS_FORWARD:
|
||||
entry_point = self.function.entry_point
|
||||
if entry_point is not None:
|
||||
worklist.append(entry_point)
|
||||
telemetry = get_telemetry()
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_worklist_enqueue(len(worklist))
|
||||
logger.info("Starting analysis of {name}", name=self.function.name)
|
||||
else:
|
||||
raise NotImplementedError("Backward analysis is not implemented")
|
||||
|
||||
# Get telemetry instance
|
||||
telemetry = get_telemetry()
|
||||
worklist = self._initialize_worklist(telemetry)
|
||||
|
||||
while worklist:
|
||||
# Track iteration count
|
||||
self.iteration_count += 1
|
||||
while worklist and self._run_iteration(worklist, telemetry):
|
||||
pass
|
||||
|
||||
# Record telemetry
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_worklist_iteration()
|
||||
|
||||
# Safety limit check
|
||||
if self.iteration_count > MAX_ITERATIONS:
|
||||
logger.error(
|
||||
"Exceeded {max} iterations! Worklist size: {size}",
|
||||
max=MAX_ITERATIONS,
|
||||
size=len(worklist),
|
||||
)
|
||||
top_nodes = sorted(self.node_visit_count.items(), key=lambda x: x[1], reverse=True)[
|
||||
:10
|
||||
]
|
||||
for node_id, count in top_nodes:
|
||||
logger.error("Node {node_id}: {count} visits", node_id=node_id, count=count)
|
||||
break
|
||||
|
||||
# Progress logging every PROGRESS_INTERVAL seconds
|
||||
current_time = time.time()
|
||||
if current_time - self.last_progress_time > PROGRESS_INTERVAL:
|
||||
elapsed = current_time - self.start_time
|
||||
logger.info(
|
||||
"Progress: {iterations} iterations, worklist={size}, {elapsed:.1f}s elapsed",
|
||||
iterations=self.iteration_count,
|
||||
size=len(worklist),
|
||||
elapsed=elapsed,
|
||||
)
|
||||
self.last_progress_time = current_time
|
||||
|
||||
node = worklist.popleft()
|
||||
|
||||
# Track node visits
|
||||
self.node_visit_count[node.node_id] += 1
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_worklist_pop(
|
||||
node.node_id,
|
||||
self.node_visit_count[node.node_id],
|
||||
len(worklist) + 1,
|
||||
self._state_local_constraint_count(self.state[node.node_id].pre),
|
||||
)
|
||||
if self.node_visit_count[node.node_id] == 50:
|
||||
logger.warning("Node {node_id} visited 50 times!", node_id=node.node_id)
|
||||
if self.node_visit_count[node.node_id] == 100:
|
||||
logger.error("Node {node_id} visited 100 times!", node_id=node.node_id)
|
||||
|
||||
current_state = AnalysisState(
|
||||
pre=self.state[node.node_id].pre, post=self.state[node.node_id].post
|
||||
)
|
||||
|
||||
self.analysis.direction().apply_transfer_function(
|
||||
analysis=self.analysis,
|
||||
current_state=current_state,
|
||||
node=node,
|
||||
worklist=worklist,
|
||||
global_state=self.state,
|
||||
)
|
||||
|
||||
# Final statistics
|
||||
total_time = time.time() - self.start_time
|
||||
logger.info(
|
||||
"Analysis of {name} complete: {iterations} iterations in {time:.2f}s",
|
||||
@@ -237,11 +142,95 @@ class Engine(Generic[A]):
|
||||
iterations=self.iteration_count,
|
||||
time=total_time,
|
||||
)
|
||||
|
||||
# Record fixpoint reached
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_fixpoint_reached()
|
||||
|
||||
def _initialize_worklist(self, telemetry: SolverTelemetry | None) -> deque[Node]:
|
||||
"""Create the initial FIFO queue without changing traversal semantics."""
|
||||
if not self.analysis.direction().IS_FORWARD:
|
||||
raise NotImplementedError("Backward analysis is not implemented")
|
||||
worklist: deque[Node] = deque()
|
||||
entry_point = self.function.entry_point
|
||||
if entry_point is None:
|
||||
return worklist
|
||||
worklist.append(entry_point)
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_worklist_enqueue(len(worklist))
|
||||
logger.info("Starting analysis of {name}", name=self.function.name)
|
||||
return worklist
|
||||
|
||||
def _run_iteration(
|
||||
self,
|
||||
worklist: deque[Node],
|
||||
telemetry: SolverTelemetry | None,
|
||||
) -> bool:
|
||||
"""Run one FIFO worklist iteration and report whether to continue."""
|
||||
self.iteration_count += 1
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_worklist_iteration()
|
||||
if self.iteration_count > MAX_ANALYSIS_ITERATIONS:
|
||||
self._log_iteration_limit(worklist)
|
||||
return False
|
||||
self._log_progress_if_due(worklist)
|
||||
node = worklist.popleft()
|
||||
self._record_node_visit(node, worklist, telemetry)
|
||||
current_state = AnalysisState(
|
||||
pre=self.state[node.node_id].pre,
|
||||
post=self.state[node.node_id].post,
|
||||
)
|
||||
self.analysis.direction().apply_transfer_function(
|
||||
analysis=self.analysis,
|
||||
current_state=current_state,
|
||||
node=node,
|
||||
worklist=worklist,
|
||||
global_state=self.state,
|
||||
)
|
||||
return True
|
||||
|
||||
def _log_iteration_limit(self, worklist: deque[Node]) -> None:
|
||||
logger.error(
|
||||
"Exceeded {max} iterations! Worklist size: {size}",
|
||||
max=MAX_ANALYSIS_ITERATIONS,
|
||||
size=len(worklist),
|
||||
)
|
||||
top_nodes = sorted(self.node_visit_count.items(), key=lambda item: item[1], reverse=True)[
|
||||
:10
|
||||
]
|
||||
for node_id, count in top_nodes:
|
||||
logger.error("Node {node_id}: {count} visits", node_id=node_id, count=count)
|
||||
|
||||
def _log_progress_if_due(self, worklist: deque[Node]) -> None:
|
||||
current_time = time.time()
|
||||
if current_time - self.last_progress_time <= PROGRESS_INTERVAL_SECONDS:
|
||||
return
|
||||
logger.info(
|
||||
"Progress: {iterations} iterations, worklist={size}, {elapsed:.1f}s elapsed",
|
||||
iterations=self.iteration_count,
|
||||
size=len(worklist),
|
||||
elapsed=current_time - self.start_time,
|
||||
)
|
||||
self.last_progress_time = current_time
|
||||
|
||||
def _record_node_visit(
|
||||
self,
|
||||
node: Node,
|
||||
worklist: deque[Node],
|
||||
telemetry: SolverTelemetry | None,
|
||||
) -> None:
|
||||
self.node_visit_count[node.node_id] += 1
|
||||
visit_count = self.node_visit_count[node.node_id]
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_worklist_pop(
|
||||
node.node_id,
|
||||
visit_count,
|
||||
len(worklist) + 1,
|
||||
self._state_local_constraint_count(self.state[node.node_id].pre),
|
||||
)
|
||||
if visit_count == 50:
|
||||
logger.warning("Node {node_id} visited 50 times!", node_id=node.node_id)
|
||||
if visit_count == 100:
|
||||
logger.error("Node {node_id} visited 100 times!", node_id=node.node_id)
|
||||
|
||||
@staticmethod
|
||||
def _state_local_constraint_count(domain: object) -> int:
|
||||
"""Count state-local constraints without coupling the engine to a domain."""
|
||||
|
||||
@@ -0,0 +1,257 @@
|
||||
"""Natural-loop identities and generation-scoped header fixpoints."""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass, field
|
||||
from typing import TYPE_CHECKING
|
||||
|
||||
from slither.analyses.data_flow.engine.domain import Domain
|
||||
from slither.analyses.data_flow.smt_solver.facts import Fact, FactId, LoopHeaderId
|
||||
|
||||
|
||||
if TYPE_CHECKING:
|
||||
from slither.analyses.data_flow.engine.analysis import Analysis
|
||||
from slither.core.cfg.node import Node
|
||||
from slither.core.declarations.function import Function
|
||||
|
||||
|
||||
@dataclass(frozen=True, order=True)
|
||||
class ControlFlowEdgeId:
|
||||
"""Stable identity of one directed CFG edge."""
|
||||
|
||||
source_id: int
|
||||
destination_id: int
|
||||
|
||||
|
||||
@dataclass(frozen=True, order=True)
|
||||
class LoopVariableId:
|
||||
"""Static phi binding for one loop-carried source variable."""
|
||||
|
||||
header_name: str
|
||||
entry_names: tuple[str, ...]
|
||||
back_names: tuple[str, ...]
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class NaturalLoop:
|
||||
"""One dominator-defined natural-loop header and its incoming edges."""
|
||||
|
||||
header_id: LoopHeaderId
|
||||
back_edges: frozenset[ControlFlowEdgeId]
|
||||
entry_edges: frozenset[ControlFlowEdgeId]
|
||||
|
||||
|
||||
class LoopStructure:
|
||||
"""Deterministic natural-loop classification for one function CFG."""
|
||||
|
||||
def __init__(self, loops: tuple[NaturalLoop, ...] = ()) -> None:
|
||||
self._loops = {loop.header_id.node_id: loop for loop in loops}
|
||||
self._back_edges = frozenset(edge for loop in loops for edge in loop.back_edges)
|
||||
|
||||
@classmethod
|
||||
def from_function(cls, function: Function) -> LoopStructure:
|
||||
"""Classify an edge as back only when its destination dominates its source."""
|
||||
nodes = sorted(function.nodes, key=lambda node: node.node_id)
|
||||
back_by_header: dict[int, set[ControlFlowEdgeId]] = {}
|
||||
for source in nodes:
|
||||
for destination in sorted(source.sons, key=lambda node: node.node_id):
|
||||
if destination in source.dominators:
|
||||
edge = ControlFlowEdgeId(source.node_id, destination.node_id)
|
||||
back_by_header.setdefault(destination.node_id, set()).add(edge)
|
||||
by_id = {node.node_id: node for node in nodes}
|
||||
loops = tuple(
|
||||
cls._make_loop(by_id[header_id], edges)
|
||||
for header_id, edges in sorted(back_by_header.items())
|
||||
)
|
||||
return cls(loops)
|
||||
|
||||
@staticmethod
|
||||
def _make_loop(header: Node, back_edges: set[ControlFlowEdgeId]) -> NaturalLoop:
|
||||
header_id = LoopHeaderId.from_node(header)
|
||||
entry_edges = frozenset(
|
||||
ControlFlowEdgeId(father.node_id, header.node_id)
|
||||
for father in header.fathers
|
||||
if ControlFlowEdgeId(father.node_id, header.node_id) not in back_edges
|
||||
)
|
||||
return NaturalLoop(header_id, frozenset(back_edges), entry_edges)
|
||||
|
||||
@property
|
||||
def loops(self) -> tuple[NaturalLoop, ...]:
|
||||
"""Return loops ordered by stable header identity."""
|
||||
return tuple(sorted(self._loops.values(), key=lambda loop: loop.header_id))
|
||||
|
||||
def header(self, node_id: int) -> NaturalLoop | None:
|
||||
"""Return natural-loop metadata for a header node ID."""
|
||||
return self._loops.get(node_id)
|
||||
|
||||
def is_back_edge(self, edge: ControlFlowEdgeId) -> bool:
|
||||
"""Return whether the edge closes a dominator-defined natural loop."""
|
||||
return edge in self._back_edges
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class LoopWideningContext:
|
||||
"""Complete previous/current header states for one candidate generation."""
|
||||
|
||||
header_id: LoopHeaderId
|
||||
generation: int
|
||||
previous_input: Domain
|
||||
current_input: Domain
|
||||
previous_output: Domain | None
|
||||
variables: tuple[LoopVariableId, ...]
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class LoopWideningResult:
|
||||
"""One candidate header approximation and its generation-owned facts."""
|
||||
|
||||
state: Domain
|
||||
generation_facts: tuple[Fact[object], ...] = ()
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class LoopUpdate:
|
||||
"""Result of incorporating one incoming edge into a loop header."""
|
||||
|
||||
changed: bool
|
||||
state: Domain | None = None
|
||||
|
||||
|
||||
@dataclass
|
||||
class LoopHeaderFixpoint:
|
||||
"""Own incoming edge contributions and one live loop generation."""
|
||||
|
||||
header_id: LoopHeaderId
|
||||
variables: tuple[LoopVariableId, ...]
|
||||
generation: int = 0
|
||||
previous_input: Domain | None = None
|
||||
current_input: Domain | None = None
|
||||
current_output: Domain | None = None
|
||||
_output_generation: int | None = None
|
||||
_entry_inputs: dict[ControlFlowEdgeId, Domain] = field(default_factory=dict)
|
||||
_back_inputs: dict[ControlFlowEdgeId, Domain] = field(default_factory=dict)
|
||||
_generation_facts: tuple[Fact[object], ...] = ()
|
||||
|
||||
def update(
|
||||
self,
|
||||
edge: ControlFlowEdgeId,
|
||||
incoming: Domain,
|
||||
is_back_edge: bool,
|
||||
analysis: Analysis,
|
||||
) -> LoopUpdate:
|
||||
"""Join one edge contribution and advance only for a changed header state."""
|
||||
inputs = self._back_inputs if is_back_edge else self._entry_inputs
|
||||
if not self._update_input(inputs, edge, incoming):
|
||||
return LoopUpdate(False)
|
||||
candidate = self._combine_inputs()
|
||||
if self.current_input is None:
|
||||
initial = analysis.bottom_value()
|
||||
if not initial.join(candidate):
|
||||
return LoopUpdate(False)
|
||||
self.current_input = initial
|
||||
return LoopUpdate(True, initial.deep_copy())
|
||||
if not is_back_edge:
|
||||
return self._join_entry_candidate(candidate)
|
||||
if self._output_generation != self.generation:
|
||||
return self._update_pending_generation(candidate, analysis)
|
||||
return self._start_generation(candidate, analysis)
|
||||
|
||||
def _start_generation(self, candidate: Domain, analysis: Analysis) -> LoopUpdate:
|
||||
"""Start a generation from the latest transferred header state."""
|
||||
if self.current_input is None:
|
||||
raise RuntimeError("Loop generation started before tracker initialization")
|
||||
next_generation = self.generation + 1
|
||||
context = LoopWideningContext(
|
||||
self.header_id,
|
||||
next_generation,
|
||||
self.current_input.deep_copy(),
|
||||
candidate,
|
||||
self.current_output.deep_copy() if self.current_output is not None else None,
|
||||
self.variables,
|
||||
)
|
||||
result = analysis.apply_loop_widening(context)
|
||||
merged = self.current_input.deep_copy()
|
||||
if not merged.join(result.state):
|
||||
return LoopUpdate(False)
|
||||
self.previous_input = self.current_input.deep_copy()
|
||||
self.current_input = merged
|
||||
self.generation = next_generation
|
||||
self._generation_facts = result.generation_facts
|
||||
return LoopUpdate(True, merged.deep_copy())
|
||||
|
||||
def _update_pending_generation(
|
||||
self,
|
||||
candidate: Domain,
|
||||
analysis: Analysis,
|
||||
) -> LoopUpdate:
|
||||
"""Join another latch into a generation whose header is already queued."""
|
||||
if self.previous_input is None or self.current_input is None:
|
||||
return LoopUpdate(False)
|
||||
context = LoopWideningContext(
|
||||
self.header_id,
|
||||
self.generation,
|
||||
self.previous_input.deep_copy(),
|
||||
candidate,
|
||||
self.current_output.deep_copy() if self.current_output is not None else None,
|
||||
self.variables,
|
||||
)
|
||||
result = analysis.apply_loop_widening(context)
|
||||
merged = self.previous_input.deep_copy()
|
||||
merged.join(result.state)
|
||||
expanded = self.current_input.deep_copy()
|
||||
if not expanded.join(merged):
|
||||
return LoopUpdate(False)
|
||||
self.current_input = expanded
|
||||
self._generation_facts = result.generation_facts
|
||||
return LoopUpdate(True, expanded.deep_copy())
|
||||
|
||||
def _join_entry_candidate(self, candidate: Domain) -> LoopUpdate:
|
||||
if self.current_input is None:
|
||||
raise RuntimeError("Loop entry joined before tracker initialization")
|
||||
merged = self.current_input.deep_copy()
|
||||
if not merged.join(candidate):
|
||||
return LoopUpdate(False)
|
||||
if self._output_generation != self.generation:
|
||||
self.current_input = merged
|
||||
return LoopUpdate(True, merged.deep_copy())
|
||||
self.previous_input = self.current_input.deep_copy()
|
||||
self.current_input = merged
|
||||
self.generation += 1
|
||||
self._generation_facts = ()
|
||||
return LoopUpdate(True, merged.deep_copy())
|
||||
|
||||
@staticmethod
|
||||
def _update_input(
|
||||
inputs: dict[ControlFlowEdgeId, Domain],
|
||||
edge: ControlFlowEdgeId,
|
||||
incoming: Domain,
|
||||
) -> bool:
|
||||
existing = inputs.get(edge)
|
||||
if existing is None:
|
||||
inputs[edge] = incoming.deep_copy()
|
||||
return True
|
||||
return existing.join(incoming)
|
||||
|
||||
def _combine_inputs(self) -> Domain:
|
||||
ordered = sorted((*self._entry_inputs.items(), *self._back_inputs.items()))
|
||||
if not ordered:
|
||||
raise RuntimeError("Loop header has no incoming contributions")
|
||||
combined = ordered[0][1].deep_copy()
|
||||
for _, incoming in ordered[1:]:
|
||||
combined.join(incoming)
|
||||
return combined
|
||||
|
||||
def record_output(self, output: Domain) -> None:
|
||||
"""Associate the latest complete header output with the current generation."""
|
||||
self.current_output = output.deep_copy()
|
||||
self._output_generation = self.generation
|
||||
|
||||
@property
|
||||
def generation_fact_ids(self) -> frozenset[FactId]:
|
||||
"""Return only the currently owned generation fact identities."""
|
||||
return frozenset(fact.fact_id for fact in self._generation_facts)
|
||||
|
||||
@property
|
||||
def generation_facts(self) -> tuple[Fact[object], ...]:
|
||||
"""Return the single live generation-owned fact set."""
|
||||
return self._generation_facts
|
||||
@@ -33,6 +33,7 @@ if TYPE_CHECKING:
|
||||
)
|
||||
from slither.analyses.data_flow.analyses.interval.core.state import State
|
||||
from slither.analyses.data_flow.smt_solver.facts import Fact, SemanticStateId
|
||||
from slither.analyses.data_flow.smt_solver.query import QueryBudget
|
||||
from slither.analyses.data_flow.smt_solver.cache import RangeQueryCache
|
||||
from slither.analyses.data_flow.smt_solver.solver import SMTSolver
|
||||
from slither.core.cfg.node import Node
|
||||
@@ -668,31 +669,24 @@ def _create_annotation(
|
||||
timeout_ms: int | None = None,
|
||||
) -> LineAnnotation | None:
|
||||
"""Create a LineAnnotation from analysis data."""
|
||||
from slither.analyses.data_flow.analysis import (
|
||||
RangeQueryConfig,
|
||||
solve_variable_range,
|
||||
)
|
||||
|
||||
effective_timeout = timeout_ms if timeout_ms is not None else config.timeout_ms
|
||||
range_config = RangeQueryConfig(
|
||||
state_id=state.semantic_id(),
|
||||
state_facts=state.get_facts(),
|
||||
timeout_ms=effective_timeout,
|
||||
skip_optimization=config.skip_solving,
|
||||
min_result, max_result, budget, effective_timeout = _solve_annotation_bounds(
|
||||
smt_var,
|
||||
state,
|
||||
solver,
|
||||
config,
|
||||
cache=cache,
|
||||
timeout_ms=timeout_ms,
|
||||
)
|
||||
min_result, max_result = solve_variable_range(solver, smt_var, range_config)
|
||||
|
||||
if not min_result or not max_result:
|
||||
return None
|
||||
|
||||
# Check for unreachable path
|
||||
if min_result.get("unreachable"):
|
||||
display_name = _simplify_var_name(var_name, keep_ssa=config.show_ssa)
|
||||
if var_name.startswith("TMP_") and tmp_expressions:
|
||||
expr = tmp_expressions.get(var_name)
|
||||
if expr:
|
||||
display_name = f"{display_name} = {expr}"
|
||||
display_name = _annotation_display_name(
|
||||
var_name,
|
||||
config.show_ssa,
|
||||
tmp_expressions,
|
||||
)
|
||||
return LineAnnotation(
|
||||
variable_name=display_name,
|
||||
range_min="⊥",
|
||||
@@ -712,27 +706,17 @@ def _create_annotation(
|
||||
# Only mark actual return statements as returns (not TMP variables)
|
||||
is_return = "return" in var_name.lower() and not var_name.startswith("TMP_")
|
||||
|
||||
# Simplify variable name for display (keep SSA suffix if requested)
|
||||
display_name = _simplify_var_name(var_name, keep_ssa=config.show_ssa)
|
||||
|
||||
# For TMP variables, add the expression they represent
|
||||
if var_name.startswith("TMP_") and tmp_expressions:
|
||||
expr = tmp_expressions.get(var_name)
|
||||
if expr:
|
||||
display_name = f"{display_name} = {expr}"
|
||||
display_name = _annotation_display_name(var_name, config.show_ssa, tmp_expressions)
|
||||
|
||||
# All annotations at same indent (column=0)
|
||||
column = 0
|
||||
|
||||
# Check overflow possibility for unchecked arithmetic (deferred to annotation time)
|
||||
branch_facts = state.get_branch_facts()
|
||||
branch_state_id = state.semantic_id_for_facts(branch_facts, "overflow_precondition")
|
||||
can_overflow, can_underflow = _check_overflow_possible(
|
||||
can_overflow, can_underflow = _annotation_overflow_status(
|
||||
solver,
|
||||
smt_var,
|
||||
state,
|
||||
effective_timeout,
|
||||
branch_state_id,
|
||||
branch_facts,
|
||||
budget=budget,
|
||||
)
|
||||
|
||||
# Record precision metrics
|
||||
@@ -753,43 +737,86 @@ def _create_annotation(
|
||||
)
|
||||
|
||||
|
||||
def _solve_annotation_bounds(
|
||||
smt_var: "TrackedSMTVariable",
|
||||
state: "State",
|
||||
solver: "SMTSolver",
|
||||
config: AnalysisConfig,
|
||||
*,
|
||||
cache: "RangeQueryCache",
|
||||
timeout_ms: int | None,
|
||||
) -> tuple[dict | None, dict | None, "QueryBudget", int]:
|
||||
"""Solve one annotation with a budget shared by deferred predicate checks."""
|
||||
from slither.analyses.data_flow.analysis import RangeQueryConfig, solve_variable_range
|
||||
from slither.analyses.data_flow.smt_solver.query import QueryBudget
|
||||
|
||||
effective_timeout = timeout_ms if timeout_ms is not None else config.timeout_ms
|
||||
budget = QueryBudget(effective_timeout)
|
||||
range_config = RangeQueryConfig(
|
||||
state_id=state.semantic_id(),
|
||||
state_facts=state.get_facts(),
|
||||
timeout_ms=effective_timeout,
|
||||
skip_optimization=config.skip_solving,
|
||||
cache=cache,
|
||||
budget=budget,
|
||||
)
|
||||
minimum, maximum = solve_variable_range(solver, smt_var, range_config)
|
||||
return minimum, maximum, budget, effective_timeout
|
||||
|
||||
|
||||
def _annotation_display_name(
|
||||
var_name: str,
|
||||
keep_ssa: bool,
|
||||
tmp_expressions: dict[str, str] | None,
|
||||
) -> str:
|
||||
"""Build the source-facing name for one annotation."""
|
||||
display_name = _simplify_var_name(var_name, keep_ssa=keep_ssa)
|
||||
if not var_name.startswith("TMP_") or not tmp_expressions:
|
||||
return display_name
|
||||
expression = tmp_expressions.get(var_name)
|
||||
return f"{display_name} = {expression}" if expression else display_name
|
||||
|
||||
|
||||
def _annotation_overflow_status(
|
||||
solver: "SMTSolver",
|
||||
smt_var: "TrackedSMTVariable",
|
||||
state: "State",
|
||||
timeout_ms: int,
|
||||
*,
|
||||
budget: "QueryBudget",
|
||||
) -> tuple[bool, bool]:
|
||||
"""Check deferred arithmetic predicates against branch-owned facts."""
|
||||
branch_facts = state.get_branch_facts()
|
||||
state_id = state.semantic_id_for_facts(branch_facts, "overflow_precondition")
|
||||
return _check_overflow_possible(
|
||||
solver,
|
||||
smt_var,
|
||||
timeout_ms,
|
||||
state_id,
|
||||
branch_facts,
|
||||
budget=budget,
|
||||
)
|
||||
|
||||
|
||||
def _check_overflow_possible(
|
||||
solver: "SMTSolver",
|
||||
smt_var: "TrackedSMTVariable",
|
||||
timeout_ms: int,
|
||||
state_id: "SemanticStateId",
|
||||
state_facts: tuple["Fact", ...],
|
||||
*,
|
||||
budget: "QueryBudget | None" = None,
|
||||
) -> tuple[bool, bool]:
|
||||
"""Check if overflow/underflow is possible for unchecked arithmetic.
|
||||
|
||||
Called at annotation time (after analysis) to avoid slowing down the
|
||||
analysis. Uses a timeout to skip expensive checks. When the solver
|
||||
returns UNKNOWN (timeout), we conservatively report overflow as
|
||||
possible — only an explicit UNSAT proves the operation is safe.
|
||||
|
||||
Branch guards (e.g. from ``if (a > b)``) are included so relational
|
||||
guards like ``if`` suppress false positives the same way ``require``
|
||||
does. Checked-arithmetic path constraints (``result <= left``) are
|
||||
deliberately excluded — they would trivially prove no overflow for
|
||||
the very operation being checked.
|
||||
|
||||
Args:
|
||||
solver: The SMT solver instance.
|
||||
smt_var: The tracked variable with overflow predicates.
|
||||
timeout_ms: Timeout in milliseconds for each check.
|
||||
state_id: Semantic identity of the branch-guard precondition view.
|
||||
state_facts: Typed branch-guard facts from the state
|
||||
containing this arithmetic operation.
|
||||
|
||||
Returns:
|
||||
Tuple of (can_overflow, can_underflow) booleans.
|
||||
"""
|
||||
"""Check deferred predicates, treating every non-UNSAT outcome as possible."""
|
||||
from slither.analyses.data_flow.smt_solver.facts import make_query_fact
|
||||
from slither.analyses.data_flow.smt_solver.query import (
|
||||
FeasibilityStatus,
|
||||
QueryPurpose,
|
||||
)
|
||||
|
||||
if not smt_var.is_unchecked:
|
||||
return False, False
|
||||
|
||||
can_overflow = False
|
||||
can_underflow = False
|
||||
|
||||
@@ -800,14 +827,18 @@ def _check_overflow_possible(
|
||||
0,
|
||||
state_id.context_id,
|
||||
)
|
||||
result = solver.check_feasibility(
|
||||
state_id=state_id,
|
||||
state_facts=state_facts,
|
||||
query_facts=(query_fact,),
|
||||
purpose=QueryPurpose.OVERFLOW,
|
||||
timeout_ms=timeout_ms,
|
||||
)
|
||||
can_overflow = result.status is not FeasibilityStatus.UNSAT
|
||||
remaining_ms = budget.remaining_ms() if budget is not None else timeout_ms
|
||||
if remaining_ms == 0:
|
||||
can_overflow = True
|
||||
else:
|
||||
result = solver.check_feasibility(
|
||||
state_id=state_id,
|
||||
state_facts=state_facts,
|
||||
query_facts=(query_fact,),
|
||||
purpose=QueryPurpose.OVERFLOW,
|
||||
timeout_ms=remaining_ms,
|
||||
)
|
||||
can_overflow = result.status is not FeasibilityStatus.UNSAT
|
||||
|
||||
if smt_var.no_underflow is not None:
|
||||
query_fact = make_query_fact(
|
||||
@@ -816,14 +847,18 @@ def _check_overflow_possible(
|
||||
0,
|
||||
state_id.context_id,
|
||||
)
|
||||
result = solver.check_feasibility(
|
||||
state_id=state_id,
|
||||
state_facts=state_facts,
|
||||
query_facts=(query_fact,),
|
||||
purpose=QueryPurpose.UNDERFLOW,
|
||||
timeout_ms=timeout_ms,
|
||||
)
|
||||
can_underflow = result.status is not FeasibilityStatus.UNSAT
|
||||
remaining_ms = budget.remaining_ms() if budget is not None else timeout_ms
|
||||
if remaining_ms == 0:
|
||||
can_underflow = True
|
||||
else:
|
||||
result = solver.check_feasibility(
|
||||
state_id=state_id,
|
||||
state_facts=state_facts,
|
||||
query_facts=(query_fact,),
|
||||
purpose=QueryPurpose.UNDERFLOW,
|
||||
timeout_ms=remaining_ms,
|
||||
)
|
||||
can_underflow = result.status is not FeasibilityStatus.UNSAT
|
||||
|
||||
return can_overflow, can_underflow
|
||||
|
||||
|
||||
@@ -13,6 +13,7 @@ from .query import (
|
||||
FeasibilityStatus,
|
||||
FunctionEncoding,
|
||||
QueryDiagnostics,
|
||||
QueryBudget,
|
||||
QueryMaterialization,
|
||||
QueryPurpose,
|
||||
QuerySession,
|
||||
@@ -33,6 +34,7 @@ __all__ = [
|
||||
"FeasibilityResult",
|
||||
"FeasibilityStatus",
|
||||
"FunctionEncoding",
|
||||
"QueryBudget",
|
||||
"QueryDiagnostics",
|
||||
"QueryMaterialization",
|
||||
"QueryPurpose",
|
||||
|
||||
@@ -4,7 +4,11 @@ from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass, field, replace
|
||||
from enum import Enum
|
||||
from typing import Generic, TypeVar
|
||||
from typing import Generic, Protocol, TypeVar, cast
|
||||
|
||||
|
||||
class _NodeWithId(Protocol):
|
||||
node_id: int
|
||||
|
||||
|
||||
class FactOwnerKind(Enum):
|
||||
@@ -92,7 +96,7 @@ class StaticOperationId:
|
||||
raise ValueError("CFG node has no function for deterministic operation identity")
|
||||
return cls(
|
||||
encoding_id=EncodingId.from_function(function),
|
||||
node_id=int(node.node_id),
|
||||
node_id=int(cast("_NodeWithId", node).node_id),
|
||||
ir_position=position,
|
||||
)
|
||||
|
||||
@@ -104,11 +108,30 @@ class StaticOperationId:
|
||||
raise ValueError("CFG node has no function for deterministic operation identity")
|
||||
return cls(
|
||||
encoding_id=EncodingId.from_function(function),
|
||||
node_id=int(node.node_id),
|
||||
node_id=int(cast("_NodeWithId", node).node_id),
|
||||
ir_position=ir_position,
|
||||
)
|
||||
|
||||
|
||||
@dataclass(frozen=True, order=True)
|
||||
class LoopHeaderId:
|
||||
"""Stable identity of one natural-loop header in a function encoding."""
|
||||
|
||||
encoding_id: EncodingId
|
||||
node_id: int
|
||||
|
||||
@classmethod
|
||||
def from_node(cls, node: object) -> LoopHeaderId:
|
||||
"""Build an identity from the header's function and CFG node ID."""
|
||||
function = getattr(node, "function", None)
|
||||
if function is None:
|
||||
raise ValueError("Loop header has no function for deterministic identity")
|
||||
return cls(
|
||||
EncodingId.from_function(function),
|
||||
int(cast("_NodeWithId", node).node_id),
|
||||
)
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class AnalysisContextId:
|
||||
"""Identity of a function encoding instantiated in an analysis context."""
|
||||
@@ -176,6 +199,7 @@ class FactProvenance:
|
||||
origin_kind: FactOriginKind
|
||||
operation_id: StaticOperationId | None = None
|
||||
cfg_edge: tuple[int, int] | None = None
|
||||
loop_header_id: LoopHeaderId | None = None
|
||||
loop_generation: int | None = None
|
||||
property_id: str | None = None
|
||||
|
||||
|
||||
@@ -2,6 +2,7 @@
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import math
|
||||
import time
|
||||
from collections.abc import Callable
|
||||
from dataclasses import dataclass
|
||||
@@ -44,6 +45,7 @@ class FeasibilityStatus(Enum):
|
||||
UNKNOWN = "unknown"
|
||||
TIMEOUT = "timeout"
|
||||
ERROR = "error"
|
||||
NOT_ATTEMPTED = "not_attempted"
|
||||
|
||||
|
||||
class BoundStatus(Enum):
|
||||
@@ -209,6 +211,9 @@ class QueryDiagnostics:
|
||||
"""Aggregate diagnostics for a public feasibility or range result."""
|
||||
|
||||
sessions: tuple[QuerySessionDiagnostics, ...] = ()
|
||||
total_budget_ms: int | None = None
|
||||
wall_elapsed_ms: float = 0.0
|
||||
budget_exhausted: bool = False
|
||||
|
||||
@property
|
||||
def elapsed_ms(self) -> float:
|
||||
@@ -224,11 +229,77 @@ class QueryDiagnostics:
|
||||
"""Serialize all independent sessions for diagnostics and future caches."""
|
||||
return {
|
||||
"elapsed_ms": self.elapsed_ms,
|
||||
"total_budget_ms": self.total_budget_ms,
|
||||
"wall_elapsed_ms": self.wall_elapsed_ms,
|
||||
"budget_exhausted": self.budget_exhausted,
|
||||
"cleanup_balanced": self.cleanup_balanced,
|
||||
"sessions": [session.to_dict() for session in self.sessions],
|
||||
}
|
||||
|
||||
|
||||
class QueryBudget:
|
||||
"""One monotonic wall-clock budget shared by an expression's query sessions."""
|
||||
|
||||
def __init__(
|
||||
self,
|
||||
total_ms: int,
|
||||
*,
|
||||
clock: Callable[[], float] = time.perf_counter,
|
||||
) -> None:
|
||||
if total_ms < 0:
|
||||
raise ValueError("Query budget cannot be negative")
|
||||
self.total_ms = total_ms
|
||||
self._clock = clock
|
||||
self._started = clock()
|
||||
self._deadline = self._started + total_ms / 1000
|
||||
self._forced_exhausted = False
|
||||
|
||||
@property
|
||||
def elapsed_ms(self) -> float:
|
||||
"""Return total orchestration wall time since this budget was created."""
|
||||
return max(0.0, (self._clock() - self._started) * 1000)
|
||||
|
||||
@property
|
||||
def exhausted(self) -> bool:
|
||||
"""Return whether no solver time remains."""
|
||||
return self._forced_exhausted or self.total_ms == 0 or self._clock() >= self._deadline
|
||||
|
||||
def remaining_ms(self, cap_ms: int | None = None) -> int:
|
||||
"""Return a positive backend timeout, or zero when the deadline passed."""
|
||||
if self._forced_exhausted:
|
||||
return 0
|
||||
remaining = max(0.0, (self._deadline - self._clock()) * 1000)
|
||||
allocated = math.ceil(remaining)
|
||||
if cap_ms is not None:
|
||||
allocated = min(allocated, max(0, cap_ms))
|
||||
return allocated
|
||||
|
||||
def exhaust(self) -> None:
|
||||
"""Close a budget when the remainder cannot safely admit another session."""
|
||||
self._forced_exhausted = True
|
||||
|
||||
def diagnostics(
|
||||
self,
|
||||
sessions: tuple[QuerySessionDiagnostics, ...] = (),
|
||||
) -> QueryDiagnostics:
|
||||
"""Snapshot aggregate budget and owned-session diagnostics."""
|
||||
return QueryDiagnostics(
|
||||
sessions=sessions,
|
||||
total_budget_ms=self.total_ms,
|
||||
wall_elapsed_ms=self.elapsed_ms,
|
||||
budget_exhausted=self.exhausted,
|
||||
)
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class BoundOutcome:
|
||||
"""One independent bound result, optionally backed by an opened session."""
|
||||
|
||||
value: int | None
|
||||
status: BoundStatus
|
||||
diagnostics: QuerySessionDiagnostics | None = None
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class FeasibilityResult:
|
||||
"""Typed satisfiability result that preserves timeout and error distinctions."""
|
||||
|
||||
@@ -14,6 +14,7 @@ from slither.analyses.data_flow.smt_solver.query import (
|
||||
FeasibilityResult,
|
||||
FunctionEncoding,
|
||||
QueryMaterialization,
|
||||
QueryBudget,
|
||||
QueryPurpose,
|
||||
QuerySession,
|
||||
RangeInterval,
|
||||
@@ -358,10 +359,12 @@ class SMTSolver(ABC):
|
||||
self.function_encoding.bind(encoding_id)
|
||||
|
||||
def register_loop_generation_fact(self, fact: Fact[SMTTerm]) -> None:
|
||||
"""Reject loop facts until Stage 2 provides generation-scoped sessions."""
|
||||
"""Reject loop facts because loop-header fixpoints own their lifecycle."""
|
||||
if fact.fact_id.owner is not FactOwnerKind.LOOP_GENERATION:
|
||||
raise ValueError("Loop facts must use the LOOP_GENERATION owner")
|
||||
raise NotImplementedError("Loop-generation facts require generation-scoped query sessions")
|
||||
raise NotImplementedError(
|
||||
"Loop-generation facts are owned by LoopHeaderFixpoint, not the solver"
|
||||
)
|
||||
|
||||
def add_query_local_assumption(self, fact: Fact[SMTTerm]) -> None:
|
||||
"""Add a classified assumption to the current push/pop query frame."""
|
||||
@@ -708,6 +711,7 @@ class SMTSolver(ABC):
|
||||
signed: bool = False,
|
||||
fallback_range: RangeInterval | None = None,
|
||||
abstract_range: RangeInterval | None = None,
|
||||
budget: QueryBudget | None = None,
|
||||
) -> RangeResult:
|
||||
"""Return independently typed feasibility, lower, and upper outcomes."""
|
||||
pass
|
||||
@@ -728,7 +732,7 @@ class SMTSolver(ABC):
|
||||
Args:
|
||||
term: The bitvector term to optimize.
|
||||
extra_constraints: Additional constraints for this query only.
|
||||
timeout_ms: Timeout in milliseconds for each optimization.
|
||||
timeout_ms: Total wall-clock budget for all range-query sessions.
|
||||
signed: If True, optimize using signed interpretation.
|
||||
|
||||
Returns:
|
||||
|
||||
@@ -1,6 +1,7 @@
|
||||
"""Z3 solver strategy implementation."""
|
||||
|
||||
import os
|
||||
import threading
|
||||
import time
|
||||
|
||||
from z3 import (
|
||||
@@ -51,15 +52,18 @@ from slither.analyses.data_flow.smt_solver.solver import SMTSolver
|
||||
from slither.analyses.data_flow.smt_solver.telemetry import get_telemetry
|
||||
from slither.analyses.data_flow.smt_solver.facts import Fact, SemanticStateId
|
||||
from slither.analyses.data_flow.smt_solver.query import (
|
||||
BoundOutcome,
|
||||
BoundStatus,
|
||||
FeasibilityResult,
|
||||
FeasibilityStatus,
|
||||
QueryDiagnostics,
|
||||
QueryBudget,
|
||||
QueryPurpose,
|
||||
QuerySession,
|
||||
QuerySessionDiagnostics,
|
||||
RangeInterval,
|
||||
RangeResult,
|
||||
empty_state_id,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.types import (
|
||||
CheckSatResult,
|
||||
@@ -76,6 +80,7 @@ DUMP_CONSTRAINTS = os.environ.get("DUMP_CONSTRAINTS", "0") == "1"
|
||||
DUMP_FILE = "/tmp/constraints_dump.txt"
|
||||
_dump_file_handle = None
|
||||
_constraint_history: list[str] = [] # Keep track of constraints for dumping
|
||||
_QUERY_CHECK_LOCK = threading.Lock()
|
||||
|
||||
|
||||
def _get_dump_file():
|
||||
@@ -98,6 +103,9 @@ def _dump(msg: str):
|
||||
class Z3Solver(SMTSolver):
|
||||
"""Z3 implementation of SMT solver interface."""
|
||||
|
||||
minimum_session_budget_ms = 50
|
||||
backend_timeout_fraction = 0.25
|
||||
|
||||
def __init__(self, use_optimizer: bool = False) -> None:
|
||||
"""
|
||||
Initialize Z3 solver.
|
||||
@@ -768,45 +776,72 @@ class Z3Solver(SMTSolver):
|
||||
signed: bool = False,
|
||||
fallback_range: RangeInterval | None = None,
|
||||
abstract_range: RangeInterval | None = None,
|
||||
budget: QueryBudget | None = None,
|
||||
) -> RangeResult:
|
||||
"""Solve lower and upper bounds in independent disposable sessions."""
|
||||
"""Solve bounds in isolated sessions sharing one hard wall-clock budget."""
|
||||
budget = budget or QueryBudget(timeout_ms)
|
||||
fallback_range = fallback_range or self._full_type_range(term, signed)
|
||||
feasibility = self._range_feasibility(
|
||||
state_id=state_id,
|
||||
state_facts=state_facts,
|
||||
query_facts=query_facts,
|
||||
compatibility_constraints=compatibility_constraints,
|
||||
timeout_ms=timeout_ms,
|
||||
)
|
||||
if feasibility.status is FeasibilityStatus.UNSAT:
|
||||
return self._unsat_range_result(feasibility)
|
||||
if abstract_range is not None:
|
||||
return self._abstract_range_result(feasibility, abstract_range)
|
||||
result = self._abstract_range_result(
|
||||
state_id,
|
||||
state_facts,
|
||||
abstract_range,
|
||||
budget,
|
||||
)
|
||||
self._record_range_refinement(result, abstract_only=True)
|
||||
return result
|
||||
feasibility_timeout = budget.remaining_ms(cap_ms=100)
|
||||
if 0 < feasibility_timeout < self.minimum_session_budget_ms:
|
||||
budget.exhaust()
|
||||
feasibility_timeout = 0
|
||||
if feasibility_timeout == 0:
|
||||
feasibility = self._budget_exhausted_feasibility(state_id, budget)
|
||||
else:
|
||||
feasibility = self._range_feasibility(
|
||||
state_id=state_id,
|
||||
state_facts=state_facts,
|
||||
query_facts=query_facts,
|
||||
compatibility_constraints=compatibility_constraints,
|
||||
timeout_ms=feasibility_timeout,
|
||||
budget=budget,
|
||||
)
|
||||
if feasibility.status is FeasibilityStatus.UNSAT:
|
||||
result = self._unsat_range_result(feasibility, budget)
|
||||
self._record_range_refinement(result, abstract_only=False)
|
||||
return result
|
||||
|
||||
objective = self._prepare_objective_term(term, signed)
|
||||
lower = self._execute_bound_query(
|
||||
term,
|
||||
objective,
|
||||
lower = self._execute_budgeted_bound_query(
|
||||
budget,
|
||||
term=term,
|
||||
objective_term=objective,
|
||||
maximize=False,
|
||||
purpose=QueryPurpose.LOWER_BOUND,
|
||||
timeout_ms=timeout_ms,
|
||||
state_id=feasibility.state_id,
|
||||
state_facts=state_facts,
|
||||
query_facts=query_facts,
|
||||
compatibility_constraints=compatibility_constraints,
|
||||
)
|
||||
upper = self._execute_bound_query(
|
||||
term,
|
||||
objective,
|
||||
upper = self._execute_budgeted_bound_query(
|
||||
budget,
|
||||
term=term,
|
||||
objective_term=objective,
|
||||
maximize=True,
|
||||
purpose=QueryPurpose.UPPER_BOUND,
|
||||
timeout_ms=timeout_ms,
|
||||
state_id=feasibility.state_id,
|
||||
state_facts=state_facts,
|
||||
query_facts=query_facts,
|
||||
compatibility_constraints=compatibility_constraints,
|
||||
)
|
||||
return self._combine_range_outcomes(feasibility, lower, upper, fallback_range)
|
||||
result = self._combine_range_outcomes(
|
||||
feasibility,
|
||||
lower,
|
||||
upper,
|
||||
fallback_range,
|
||||
budget,
|
||||
)
|
||||
self._record_range_refinement(result, abstract_only=False)
|
||||
return result
|
||||
|
||||
def _range_feasibility(
|
||||
self,
|
||||
@@ -816,6 +851,7 @@ class Z3Solver(SMTSolver):
|
||||
query_facts: tuple[Fact[SMTTerm], ...],
|
||||
compatibility_constraints: tuple[SMTTerm, ...],
|
||||
timeout_ms: int,
|
||||
budget: QueryBudget | None = None,
|
||||
) -> FeasibilityResult:
|
||||
"""Establish feasibility once for both objective sessions."""
|
||||
session = self.create_query_session(
|
||||
@@ -826,7 +862,7 @@ class Z3Solver(SMTSolver):
|
||||
query_facts=query_facts,
|
||||
compatibility_constraints=compatibility_constraints,
|
||||
)
|
||||
status, reason = self._execute_feasibility_session(session)
|
||||
status, reason = self._execute_feasibility_session(session, budget)
|
||||
del reason
|
||||
return FeasibilityResult(
|
||||
status=status,
|
||||
@@ -838,6 +874,7 @@ class Z3Solver(SMTSolver):
|
||||
def _execute_feasibility_session(
|
||||
self,
|
||||
session: QuerySession[SMTTerm],
|
||||
budget: QueryBudget | None = None,
|
||||
) -> tuple[FeasibilityStatus, str | None]:
|
||||
"""Materialize, execute, classify, and always close one Solver session."""
|
||||
status = FeasibilityStatus.ERROR
|
||||
@@ -846,16 +883,38 @@ class Z3Solver(SMTSolver):
|
||||
with session:
|
||||
solver = self._create_feasibility_backend(session.timeout_ms)
|
||||
session.attach_backend(solver)
|
||||
solver.add(*(fact.formula for fact in session.materialization.facts))
|
||||
started = time.perf_counter()
|
||||
result = solver.check()
|
||||
elapsed_ms = (time.perf_counter() - started) * 1000
|
||||
status, reason = self._classify_feasibility(
|
||||
solver,
|
||||
result,
|
||||
elapsed_ms,
|
||||
session.timeout_ms,
|
||||
solver.add(
|
||||
*(
|
||||
self._translate_for_backend(fact.formula, solver)
|
||||
for fact in session.materialization.facts
|
||||
)
|
||||
)
|
||||
effective_timeout = (
|
||||
min(session.timeout_ms, budget.remaining_ms())
|
||||
if budget is not None
|
||||
else session.timeout_ms
|
||||
)
|
||||
if budget is not None and 0 < effective_timeout < self.minimum_session_budget_ms:
|
||||
budget.exhaust()
|
||||
effective_timeout = 0
|
||||
elif budget is not None:
|
||||
effective_timeout = max(
|
||||
1,
|
||||
int(effective_timeout * self.backend_timeout_fraction),
|
||||
)
|
||||
session.timeout_ms = effective_timeout
|
||||
started = time.perf_counter()
|
||||
if effective_timeout == 0:
|
||||
status, reason = FeasibilityStatus.TIMEOUT, "total budget exhausted"
|
||||
else:
|
||||
result = self._check_with_deadline(solver, effective_timeout)
|
||||
elapsed_ms = (time.perf_counter() - started) * 1000
|
||||
status, reason = self._classify_feasibility(
|
||||
solver,
|
||||
result,
|
||||
elapsed_ms,
|
||||
effective_timeout,
|
||||
)
|
||||
session.close(feasibility_status=status, reason=reason)
|
||||
except Exception as error: # Z3 exceptions become typed query errors.
|
||||
status = FeasibilityStatus.ERROR
|
||||
@@ -884,7 +943,8 @@ class Z3Solver(SMTSolver):
|
||||
state_facts: tuple[Fact[SMTTerm], ...],
|
||||
query_facts: tuple[Fact[SMTTerm], ...],
|
||||
compatibility_constraints: tuple[SMTTerm, ...],
|
||||
) -> tuple[int | None, BoundStatus, QuerySessionDiagnostics]:
|
||||
budget: QueryBudget | None = None,
|
||||
) -> BoundOutcome:
|
||||
"""Execute one minimum or maximum objective in a fresh Optimize instance."""
|
||||
session = self.create_query_session(
|
||||
purpose=purpose,
|
||||
@@ -901,20 +961,44 @@ class Z3Solver(SMTSolver):
|
||||
with session:
|
||||
optimizer = self._create_optimizer_backend(timeout_ms)
|
||||
session.attach_backend(optimizer)
|
||||
optimizer.add(*(fact.formula for fact in session.materialization.facts))
|
||||
objective = optimizer.maximize if maximize else optimizer.minimize
|
||||
objective(objective_term)
|
||||
started = time.perf_counter()
|
||||
result = optimizer.check()
|
||||
elapsed_ms = (time.perf_counter() - started) * 1000
|
||||
status, reason = self._classify_bound(
|
||||
optimizer,
|
||||
result,
|
||||
elapsed_ms,
|
||||
timeout_ms,
|
||||
optimizer.add(
|
||||
*(
|
||||
self._translate_for_backend(fact.formula, optimizer)
|
||||
for fact in session.materialization.facts
|
||||
)
|
||||
)
|
||||
backend_term = self._translate_for_backend(term, optimizer)
|
||||
backend_objective = self._translate_for_backend(objective_term, optimizer)
|
||||
objective = optimizer.maximize if maximize else optimizer.minimize
|
||||
objective(backend_objective)
|
||||
effective_timeout = (
|
||||
min(timeout_ms, budget.remaining_ms())
|
||||
if budget is not None
|
||||
else timeout_ms
|
||||
)
|
||||
if budget is not None and 0 < effective_timeout < self.minimum_session_budget_ms:
|
||||
budget.exhaust()
|
||||
effective_timeout = 0
|
||||
elif budget is not None:
|
||||
effective_timeout = max(
|
||||
1,
|
||||
int(effective_timeout * self.backend_timeout_fraction),
|
||||
)
|
||||
session.timeout_ms = effective_timeout
|
||||
started = time.perf_counter()
|
||||
if effective_timeout == 0:
|
||||
status, reason = BoundStatus.TIMEOUT, "total budget exhausted"
|
||||
else:
|
||||
result = self._check_with_deadline(optimizer, effective_timeout)
|
||||
elapsed_ms = (time.perf_counter() - started) * 1000
|
||||
status, reason = self._classify_bound(
|
||||
optimizer,
|
||||
result,
|
||||
elapsed_ms,
|
||||
effective_timeout,
|
||||
)
|
||||
if status is BoundStatus.PROVEN:
|
||||
value = self._bound_model_value(optimizer, term)
|
||||
value = self._bound_model_value(optimizer, backend_term)
|
||||
if value is None:
|
||||
status = BoundStatus.ERROR
|
||||
reason = "optimizer model did not contain a bitvector value"
|
||||
@@ -924,7 +1008,40 @@ class Z3Solver(SMTSolver):
|
||||
reason = f"{type(error).__name__}: {error}"
|
||||
if session.diagnostics.bound_status is not BoundStatus.ERROR:
|
||||
raise RuntimeError("QuerySession recorded the wrong backend error kind") from error
|
||||
return value, status, session.diagnostics
|
||||
return BoundOutcome(value, status, session.diagnostics)
|
||||
|
||||
def _execute_budgeted_bound_query(
|
||||
self,
|
||||
budget: QueryBudget,
|
||||
term: SMTTerm,
|
||||
objective_term: SMTTerm,
|
||||
*,
|
||||
maximize: bool,
|
||||
purpose: QueryPurpose,
|
||||
state_id: SemanticStateId,
|
||||
state_facts: tuple[Fact[SMTTerm], ...],
|
||||
query_facts: tuple[Fact[SMTTerm], ...],
|
||||
compatibility_constraints: tuple[SMTTerm, ...],
|
||||
) -> BoundOutcome:
|
||||
"""Run one objective only when the expression deadline has time left."""
|
||||
timeout_ms = budget.remaining_ms()
|
||||
if 0 < timeout_ms < self.minimum_session_budget_ms:
|
||||
budget.exhaust()
|
||||
timeout_ms = 0
|
||||
if timeout_ms == 0:
|
||||
return BoundOutcome(None, BoundStatus.TIMEOUT)
|
||||
return self._execute_bound_query(
|
||||
term,
|
||||
objective_term,
|
||||
maximize=maximize,
|
||||
purpose=purpose,
|
||||
timeout_ms=timeout_ms,
|
||||
state_id=state_id,
|
||||
state_facts=state_facts,
|
||||
query_facts=query_facts,
|
||||
compatibility_constraints=compatibility_constraints,
|
||||
budget=budget,
|
||||
)
|
||||
|
||||
@staticmethod
|
||||
def _create_feasibility_backend(timeout_ms: int) -> Solver:
|
||||
@@ -940,6 +1057,40 @@ class Z3Solver(SMTSolver):
|
||||
optimizer.set("timeout", timeout_ms)
|
||||
return optimizer
|
||||
|
||||
@staticmethod
|
||||
def _translate_for_backend(term: SMTTerm, backend: object) -> SMTTerm:
|
||||
"""Translate a term only when a backend uses a distinct Z3 context."""
|
||||
context = getattr(backend, "ctx", None)
|
||||
translate = getattr(term, "translate", None)
|
||||
term_context = getattr(term, "ctx", None)
|
||||
same_context = term_context is context
|
||||
if term_context is not None and context is not None:
|
||||
same_context = term_context.ref() == context.ref()
|
||||
if context is None or translate is None or same_context:
|
||||
return term
|
||||
return translate(context)
|
||||
|
||||
@staticmethod
|
||||
def _check_with_deadline(backend: object, timeout_ms: int) -> object:
|
||||
"""Interrupt the active Z3 check when its soft timeout overruns."""
|
||||
check = getattr(backend, "check", None)
|
||||
if not callable(check):
|
||||
raise TypeError("Z3 query backend does not provide check()")
|
||||
context = getattr(backend, "ctx", None)
|
||||
interrupt = getattr(backend, "interrupt", None)
|
||||
if interrupt is None and context is not None:
|
||||
interrupt = getattr(context, "interrupt", None)
|
||||
if interrupt is None or timeout_ms <= 0:
|
||||
return check()
|
||||
with _QUERY_CHECK_LOCK:
|
||||
watchdog = threading.Timer(timeout_ms / 1000, interrupt)
|
||||
watchdog.daemon = True
|
||||
watchdog.start()
|
||||
try:
|
||||
return check()
|
||||
finally:
|
||||
watchdog.cancel()
|
||||
|
||||
@staticmethod
|
||||
def _classify_feasibility(
|
||||
query_solver: object,
|
||||
@@ -1005,7 +1156,10 @@ class Z3Solver(SMTSolver):
|
||||
return value.as_long() if is_bv_value(value) else None
|
||||
|
||||
@staticmethod
|
||||
def _unsat_range_result(feasibility: FeasibilityResult) -> RangeResult:
|
||||
def _unsat_range_result(
|
||||
feasibility: FeasibilityResult,
|
||||
budget: QueryBudget,
|
||||
) -> RangeResult:
|
||||
"""Return the existing bottom convention after proven UNSAT feasibility."""
|
||||
return RangeResult(
|
||||
lower=None,
|
||||
@@ -1016,37 +1170,43 @@ class Z3Solver(SMTSolver):
|
||||
fallback_range=None,
|
||||
encoding_id=feasibility.encoding_id,
|
||||
state_id=feasibility.state_id,
|
||||
diagnostics=feasibility.diagnostics,
|
||||
diagnostics=budget.diagnostics(feasibility.diagnostics.sessions),
|
||||
)
|
||||
|
||||
@staticmethod
|
||||
def _abstract_range_result(
|
||||
feasibility: FeasibilityResult,
|
||||
self,
|
||||
state_id: SemanticStateId | None,
|
||||
state_facts: tuple[Fact[SMTTerm], ...],
|
||||
interval: RangeInterval,
|
||||
budget: QueryBudget,
|
||||
) -> RangeResult:
|
||||
"""Return an explicitly abstract range without creating objectives."""
|
||||
"""Return an explicitly abstract range without opening any session."""
|
||||
state_id = state_id or empty_state_id(self.function_encoding.encoding_id)
|
||||
if frozenset(fact.fact_id for fact in state_facts) != state_id.active_fact_ids:
|
||||
raise ValueError("Abstract range state facts do not match SemanticStateId")
|
||||
return RangeResult(
|
||||
lower=interval.lower,
|
||||
upper=interval.upper,
|
||||
feasibility=feasibility.status,
|
||||
feasibility=FeasibilityStatus.NOT_ATTEMPTED,
|
||||
lower_status=BoundStatus.ABSTRACT,
|
||||
upper_status=BoundStatus.ABSTRACT,
|
||||
fallback_range=interval,
|
||||
encoding_id=feasibility.encoding_id,
|
||||
state_id=feasibility.state_id,
|
||||
diagnostics=feasibility.diagnostics,
|
||||
encoding_id=self.function_encoding.encoding_id,
|
||||
state_id=state_id,
|
||||
diagnostics=budget.diagnostics(),
|
||||
)
|
||||
|
||||
@staticmethod
|
||||
def _combine_range_outcomes(
|
||||
feasibility: FeasibilityResult,
|
||||
lower: tuple[int | None, BoundStatus, QuerySessionDiagnostics],
|
||||
upper: tuple[int | None, BoundStatus, QuerySessionDiagnostics],
|
||||
lower: BoundOutcome,
|
||||
upper: BoundOutcome,
|
||||
fallback: RangeInterval,
|
||||
budget: QueryBudget,
|
||||
) -> RangeResult:
|
||||
"""Preserve one proven side and fall back only for a failed objective."""
|
||||
lower_value, lower_status, lower_diagnostics = lower
|
||||
upper_value, upper_status, upper_diagnostics = upper
|
||||
lower_value, lower_status = lower.value, lower.status
|
||||
upper_value, upper_status = upper.value, upper.status
|
||||
used_fallback = lower_status is not BoundStatus.PROVEN or (
|
||||
upper_status is not BoundStatus.PROVEN
|
||||
)
|
||||
@@ -1054,10 +1214,10 @@ class Z3Solver(SMTSolver):
|
||||
lower_value = fallback.lower
|
||||
if upper_status is not BoundStatus.PROVEN:
|
||||
upper_value = fallback.upper
|
||||
sessions = (
|
||||
*feasibility.diagnostics.sessions,
|
||||
lower_diagnostics,
|
||||
upper_diagnostics,
|
||||
objective_sessions = tuple(
|
||||
diagnostics
|
||||
for diagnostics in (lower.diagnostics, upper.diagnostics)
|
||||
if diagnostics is not None
|
||||
)
|
||||
return RangeResult(
|
||||
lower=lower_value,
|
||||
@@ -1068,9 +1228,32 @@ class Z3Solver(SMTSolver):
|
||||
fallback_range=fallback if used_fallback else None,
|
||||
encoding_id=feasibility.encoding_id,
|
||||
state_id=feasibility.state_id,
|
||||
diagnostics=QueryDiagnostics(sessions),
|
||||
diagnostics=budget.diagnostics(
|
||||
(*feasibility.diagnostics.sessions, *objective_sessions)
|
||||
),
|
||||
)
|
||||
|
||||
def _budget_exhausted_feasibility(
|
||||
self,
|
||||
state_id: SemanticStateId | None,
|
||||
budget: QueryBudget,
|
||||
) -> FeasibilityResult:
|
||||
"""Represent a feasibility check skipped because no budget remained."""
|
||||
resolved_state = state_id or empty_state_id(self.function_encoding.encoding_id)
|
||||
return FeasibilityResult(
|
||||
status=FeasibilityStatus.TIMEOUT,
|
||||
encoding_id=self.function_encoding.encoding_id,
|
||||
state_id=resolved_state,
|
||||
diagnostics=budget.diagnostics(),
|
||||
)
|
||||
|
||||
@staticmethod
|
||||
def _record_range_refinement(result: RangeResult, *, abstract_only: bool) -> None:
|
||||
"""Record one aggregate refinement decision without driving semantics."""
|
||||
telemetry = get_telemetry()
|
||||
if telemetry is not None and telemetry.enabled:
|
||||
telemetry.record_range_refinement(result, abstract_only=abstract_only)
|
||||
|
||||
def _full_type_range(self, term: SMTTerm, signed: bool) -> RangeInterval:
|
||||
"""Return the sound type interval used when an objective is inconclusive."""
|
||||
if not self.is_bitvector(term):
|
||||
|
||||
@@ -185,6 +185,23 @@ class QuerySessionMetrics:
|
||||
bound_statuses: dict[str, int] = field(default_factory=dict)
|
||||
|
||||
|
||||
@dataclass
|
||||
class RangeRefinementMetrics:
|
||||
"""Aggregate abstract-first and total-budget range decisions."""
|
||||
|
||||
requests: int = 0
|
||||
abstract_only: int = 0
|
||||
refinements_attempted: int = 0
|
||||
sessions_avoided: int = 0
|
||||
budget_exhausted: int = 0
|
||||
partial_results: int = 0
|
||||
configured_total_budget_ms: int = 0
|
||||
wall_elapsed_ms: float = 0.0
|
||||
feasibility_statuses: dict[str, int] = field(default_factory=dict)
|
||||
lower_statuses: dict[str, int] = field(default_factory=dict)
|
||||
upper_statuses: dict[str, int] = field(default_factory=dict)
|
||||
|
||||
|
||||
@dataclass
|
||||
class StateJoinMetrics:
|
||||
"""Opt-in observations of Stage 3 join and convergence behavior."""
|
||||
@@ -195,6 +212,21 @@ class StateJoinMetrics:
|
||||
transfer_reruns_prevented: int = 0
|
||||
|
||||
|
||||
@dataclass
|
||||
class LoopFixpointMetrics:
|
||||
"""Opt-in observations of Stage 4 natural-loop generations."""
|
||||
|
||||
headers_classified: int = 0
|
||||
entry_edge_propagations: int = 0
|
||||
back_edge_propagations: int = 0
|
||||
generation_advances: int = 0
|
||||
pending_generation_updates: int = 0
|
||||
semantic_noops: int = 0
|
||||
generation_fact_replacements: int = 0
|
||||
live_generation_facts: int = 0
|
||||
max_live_generation_facts: int = 0
|
||||
|
||||
|
||||
@dataclass
|
||||
class TransferFunctionMetrics:
|
||||
"""Transfer function operation statistics."""
|
||||
@@ -233,7 +265,9 @@ class EvaluationMetrics:
|
||||
solver_lifetime: SolverLifetimeMetrics = field(default_factory=SolverLifetimeMetrics)
|
||||
facts: FactOwnershipMetrics = field(default_factory=FactOwnershipMetrics)
|
||||
query_sessions: QuerySessionMetrics = field(default_factory=QuerySessionMetrics)
|
||||
range_refinements: RangeRefinementMetrics = field(default_factory=RangeRefinementMetrics)
|
||||
state_joins: StateJoinMetrics = field(default_factory=StateJoinMetrics)
|
||||
loop_fixpoints: LoopFixpointMetrics = field(default_factory=LoopFixpointMetrics)
|
||||
transfer_functions: TransferFunctionMetrics = field(default_factory=TransferFunctionMetrics)
|
||||
precision: PrecisionMetrics = field(default_factory=PrecisionMetrics)
|
||||
|
||||
@@ -295,6 +329,8 @@ class SolverTelemetry:
|
||||
# Exact fingerprints are retained only while telemetry is enabled.
|
||||
_assertion_fingerprints: set[str] = field(default_factory=set)
|
||||
|
||||
_loop_generation_fact_counts: dict[str, int] = field(default_factory=dict)
|
||||
|
||||
def count(self, operation: str, amount: int = 1) -> None:
|
||||
"""Increment counter for an operation."""
|
||||
if not self.enabled:
|
||||
@@ -396,6 +432,43 @@ class SolverTelemetry:
|
||||
return
|
||||
self.evaluation.state_joins.transfer_reruns_prevented += 1
|
||||
|
||||
def record_loop_headers(self, count: int) -> None:
|
||||
"""Record the number of dominator-classified loop headers."""
|
||||
if not self.enabled:
|
||||
return
|
||||
self.evaluation.loop_fixpoints.headers_classified = count
|
||||
|
||||
def record_loop_update(
|
||||
self,
|
||||
*,
|
||||
header_key: str,
|
||||
is_back_edge: bool,
|
||||
changed: bool,
|
||||
generation_advanced: bool,
|
||||
facts_replaced: bool,
|
||||
live_generation_facts: int,
|
||||
) -> None:
|
||||
"""Record one incoming natural-loop edge and its lifecycle result."""
|
||||
if not self.enabled:
|
||||
return
|
||||
metrics = self.evaluation.loop_fixpoints
|
||||
if is_back_edge:
|
||||
metrics.back_edge_propagations += 1
|
||||
else:
|
||||
metrics.entry_edge_propagations += 1
|
||||
metrics.generation_advances += int(generation_advanced)
|
||||
metrics.pending_generation_updates += int(
|
||||
is_back_edge and changed and not generation_advanced
|
||||
)
|
||||
metrics.semantic_noops += int(not changed)
|
||||
metrics.generation_fact_replacements += int(facts_replaced)
|
||||
self._loop_generation_fact_counts[header_key] = live_generation_facts
|
||||
metrics.live_generation_facts = sum(self._loop_generation_fact_counts.values())
|
||||
metrics.max_live_generation_facts = max(
|
||||
metrics.max_live_generation_facts,
|
||||
metrics.live_generation_facts,
|
||||
)
|
||||
|
||||
def record_assertion(
|
||||
self,
|
||||
fingerprint: str,
|
||||
@@ -485,6 +558,27 @@ class SolverTelemetry:
|
||||
self._increment_group(metrics.bound_statuses, bound.value)
|
||||
metrics.timeout_results += int(bound.value == "timeout")
|
||||
|
||||
def record_range_refinement(self, result: Any, *, abstract_only: bool) -> None:
|
||||
"""Record one completed range decision, including zero-session results."""
|
||||
if not self.enabled:
|
||||
return
|
||||
metrics = self.evaluation.range_refinements
|
||||
diagnostics = result.diagnostics
|
||||
metrics.requests += 1
|
||||
metrics.abstract_only += int(abstract_only)
|
||||
metrics.refinements_attempted += int(not abstract_only)
|
||||
metrics.sessions_avoided += int(abstract_only)
|
||||
metrics.budget_exhausted += int(diagnostics.budget_exhausted)
|
||||
metrics.configured_total_budget_ms += diagnostics.total_budget_ms or 0
|
||||
metrics.wall_elapsed_ms += diagnostics.wall_elapsed_ms
|
||||
proven = sum(
|
||||
status.value == "proven" for status in (result.lower_status, result.upper_status)
|
||||
)
|
||||
metrics.partial_results += int(proven == 1)
|
||||
self._increment_group(metrics.feasibility_statuses, result.feasibility.value)
|
||||
self._increment_group(metrics.lower_statuses, result.lower_status.value)
|
||||
self._increment_group(metrics.upper_statuses, result.upper_status.value)
|
||||
|
||||
@staticmethod
|
||||
def _increment_group(groups: dict[str, int], key: str) -> None:
|
||||
"""Increment one telemetry grouping."""
|
||||
@@ -714,6 +808,7 @@ class SolverTelemetry:
|
||||
self.evaluation = EvaluationMetrics()
|
||||
self._query_times_ms.clear()
|
||||
self._assertion_fingerprints.clear()
|
||||
self._loop_generation_fact_counts.clear()
|
||||
|
||||
def get_summary(self) -> dict[str, dict]:
|
||||
"""Get summary of all telemetry data."""
|
||||
|
||||
@@ -0,0 +1,43 @@
|
||||
// SPDX-License-Identifier: MIT
|
||||
pragma solidity ^0.8.20;
|
||||
|
||||
contract Test_AbstractTransfer {
|
||||
function constantPower() public pure returns (uint8) {
|
||||
return 3 ** 2;
|
||||
}
|
||||
|
||||
function constantBitwise() public pure returns (uint8) {
|
||||
return 10 & 12;
|
||||
}
|
||||
|
||||
function boundedCheckedMul(uint8 left, uint8 right) public pure returns (uint8) {
|
||||
require(left >= 2 && left <= 5);
|
||||
require(right >= 3 && right <= 7);
|
||||
return left * right;
|
||||
}
|
||||
|
||||
function boundedDivision(uint8 value) public pure returns (uint8) {
|
||||
require(value >= 10 && value <= 20);
|
||||
return value / 2;
|
||||
}
|
||||
|
||||
function boundedModulo(uint8 value) public pure returns (uint8) {
|
||||
require(value >= 10 && value <= 20);
|
||||
return value % 6;
|
||||
}
|
||||
|
||||
function boundedPower(uint8 value) public pure returns (uint8) {
|
||||
require(value >= 2 && value <= 3);
|
||||
return value ** 2;
|
||||
}
|
||||
|
||||
function boundedShift(uint8 value) public pure returns (uint8) {
|
||||
require(value >= 8 && value <= 31);
|
||||
return value >> 2;
|
||||
}
|
||||
|
||||
function boundedBitwise(uint8 value) public pure returns (uint8) {
|
||||
require(value <= 15);
|
||||
return value & 3;
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,30 @@
|
||||
// SPDX-License-Identifier: MIT
|
||||
pragma solidity ^0.8.20;
|
||||
|
||||
contract Test_LoopFixpoint {
|
||||
function test_multiple_back_edges() public pure returns (uint256) {
|
||||
uint256 i = 0;
|
||||
uint256 sum = 0;
|
||||
while (i < 10) {
|
||||
if (i % 2 == 0) {
|
||||
i += 1;
|
||||
sum += i;
|
||||
continue;
|
||||
}
|
||||
i += 2;
|
||||
sum += i;
|
||||
continue;
|
||||
}
|
||||
return sum;
|
||||
}
|
||||
|
||||
function test_nested_loops() public pure returns (uint256) {
|
||||
uint256 sum = 0;
|
||||
for (uint256 i = 0; i < 3; i++) {
|
||||
for (uint256 j = 0; j < 2; j++) {
|
||||
sum += i + j;
|
||||
}
|
||||
}
|
||||
return sum;
|
||||
}
|
||||
}
|
||||
@@ -29,6 +29,7 @@ from slither.analyses.data_flow.analyses.interval.analysis.domain import (
|
||||
from slither.analyses.data_flow.analyses.interval.core.state import State
|
||||
from slither.analyses.data_flow.engine.engine import Engine
|
||||
from slither.analyses.data_flow.smt_solver import Z3Solver
|
||||
from slither.analyses.data_flow.smt_solver.query import RangeInterval
|
||||
from slither.analyses.data_flow.smt_solver.telemetry import (
|
||||
enable_telemetry,
|
||||
reset_telemetry,
|
||||
@@ -49,6 +50,16 @@ def parse_args() -> argparse.Namespace:
|
||||
help="Use current state-local constraints or omit them for a diagnostic control",
|
||||
)
|
||||
parser.add_argument("--timeout-ms", type=int, default=3000)
|
||||
parser.add_argument(
|
||||
"--force-refinement",
|
||||
action="store_true",
|
||||
help="Refine tracked abstract intervals instead of returning them directly",
|
||||
)
|
||||
parser.add_argument(
|
||||
"--summary-only",
|
||||
action="store_true",
|
||||
help="Print lifecycle totals and selected query results without per-node state dumps",
|
||||
)
|
||||
return parser.parse_args()
|
||||
|
||||
|
||||
@@ -93,12 +104,23 @@ def query_matching_variables(
|
||||
continue
|
||||
seen.add(key)
|
||||
started = time.perf_counter()
|
||||
tracked_interval = RangeInterval(variable.interval.lower, variable.interval.upper)
|
||||
abstract_sufficient = variable.is_total and (
|
||||
variable.interval != variable.type_interval
|
||||
or variable.overflow_operation_id is not None
|
||||
)
|
||||
result = solver.solve_range_result(
|
||||
variable.term,
|
||||
state_id=state_id,
|
||||
state_facts=state_facts,
|
||||
timeout_ms=args.timeout_ms,
|
||||
signed=bool(variable.base.metadata.get("is_signed", False)),
|
||||
fallback_range=tracked_interval,
|
||||
abstract_range=(
|
||||
tracked_interval
|
||||
if abstract_sufficient and not args.force_refinement
|
||||
else None
|
||||
),
|
||||
)
|
||||
queries.append(
|
||||
{
|
||||
@@ -111,6 +133,16 @@ def query_matching_variables(
|
||||
"lower": result.lower,
|
||||
"upper": result.upper,
|
||||
"elapsed_ms": round((time.perf_counter() - started) * 1000, 3),
|
||||
"total_budget_ms": result.diagnostics.total_budget_ms,
|
||||
"budget_elapsed_ms": round(result.diagnostics.wall_elapsed_ms, 3),
|
||||
"budget_exhausted": result.diagnostics.budget_exhausted,
|
||||
"sessions": len(result.diagnostics.sessions),
|
||||
"backend_elapsed_ms": round(result.diagnostics.elapsed_ms, 3),
|
||||
"fallback_range": (
|
||||
result.fallback_range.to_dict()
|
||||
if result.fallback_range is not None
|
||||
else None
|
||||
),
|
||||
}
|
||||
)
|
||||
return queries
|
||||
@@ -178,6 +210,7 @@ def run_probe(args: argparse.Namespace) -> dict:
|
||||
started = time.perf_counter()
|
||||
engine.run_analysis()
|
||||
analysis_elapsed_ms = (time.perf_counter() - started) * 1000
|
||||
analysis_query_sessions = telemetry.get_evaluation_metrics().to_dict()["query_sessions"].copy()
|
||||
queries = []
|
||||
if args.query_variable:
|
||||
pattern = re.compile(args.query_variable)
|
||||
@@ -208,15 +241,61 @@ def run_probe(args: argparse.Namespace) -> dict:
|
||||
"lifetime": lifetime,
|
||||
"fact_ownership": evaluation["facts"],
|
||||
"query_sessions": evaluation["query_sessions"],
|
||||
"range_refinements": evaluation["range_refinements"],
|
||||
"analysis_query_sessions": analysis_query_sessions,
|
||||
"state_joins": evaluation["state_joins"],
|
||||
"loop_fixpoints": evaluation["loop_fixpoints"],
|
||||
"active_query_sessions": solver.active_query_sessions,
|
||||
"query_summary": query_summary,
|
||||
}
|
||||
|
||||
|
||||
def summarize_probe(result: dict) -> dict:
|
||||
"""Return the concise evidence used by direct lifecycle checks."""
|
||||
lifetime = result["lifetime"]
|
||||
facts = result["fact_ownership"]
|
||||
return {
|
||||
"contract": result["contract"],
|
||||
"function": result["function"],
|
||||
"cfg_nodes": result["cfg_nodes"],
|
||||
"iterations": result["iterations"],
|
||||
"analysis_elapsed_ms": result["analysis_elapsed_ms"],
|
||||
"visited_nodes": len(lifetime["node_visits"]),
|
||||
"final_live_assertions": result["final_live_assertions"],
|
||||
"final_duplicate_assertions": result["final_duplicate_assertions"],
|
||||
"internal_unclassified_additions": facts["unclassified_additions"],
|
||||
"analysis_query_sessions": _summarize_sessions(result["analysis_query_sessions"]),
|
||||
"query_sessions": _summarize_sessions(result["query_sessions"]),
|
||||
"range_refinements": result["range_refinements"],
|
||||
"loop_fixpoints": result["loop_fixpoints"],
|
||||
"queries": result["queries"],
|
||||
"active_query_sessions": result["active_query_sessions"],
|
||||
}
|
||||
|
||||
|
||||
def _summarize_sessions(metrics: dict) -> dict:
|
||||
"""Drop high-cardinality identities from session lifecycle output."""
|
||||
keys = (
|
||||
"created",
|
||||
"closed",
|
||||
"active",
|
||||
"cleanup_imbalances",
|
||||
"timeout_results",
|
||||
"compatibility_query_facts",
|
||||
"by_purpose",
|
||||
"feasibility_statuses",
|
||||
"bound_statuses",
|
||||
)
|
||||
return {key: metrics[key] for key in keys}
|
||||
|
||||
|
||||
def main() -> None:
|
||||
"""Run the command-line probe."""
|
||||
print(json.dumps(run_probe(parse_args()), indent=2, sort_keys=True))
|
||||
args = parse_args()
|
||||
result = run_probe(args)
|
||||
if args.summary_only:
|
||||
result = summarize_probe(result)
|
||||
print(json.dumps(result, indent=2, sort_keys=True))
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
|
||||
@@ -0,0 +1,443 @@
|
||||
"""Focused soundness tests for nonlinear abstract interval transfer."""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from collections.abc import Iterable
|
||||
|
||||
import pytest
|
||||
|
||||
from slither.analyses.data_flow.analyses.interval.core.tracked_variable import (
|
||||
NumericInterval,
|
||||
)
|
||||
from slither.analyses.data_flow.analyses.interval.operations.binary.abstract_transfer import (
|
||||
AbstractTransferKind,
|
||||
transfer_binary_interval,
|
||||
)
|
||||
from slither.slithir.operations.binary import BinaryType
|
||||
|
||||
|
||||
def _interval(lower: int, upper: int | None = None) -> NumericInterval:
|
||||
return NumericInterval(lower, lower if upper is None else upper)
|
||||
|
||||
|
||||
def _all_intervals(values: Iterable[int]) -> tuple[NumericInterval, ...]:
|
||||
concrete = tuple(values)
|
||||
return tuple(
|
||||
NumericInterval(lower, upper)
|
||||
for lower in concrete
|
||||
for upper in concrete
|
||||
if lower <= upper
|
||||
)
|
||||
|
||||
|
||||
def _decode_wrapped(value: int, bit_width: int, is_signed: bool) -> int:
|
||||
modulus = 1 << bit_width
|
||||
wrapped = value % modulus
|
||||
if is_signed and wrapped >= 1 << (bit_width - 1):
|
||||
wrapped -= modulus
|
||||
return wrapped
|
||||
|
||||
|
||||
def _concrete_multiplication_results(
|
||||
left: NumericInterval,
|
||||
right: NumericInterval,
|
||||
*,
|
||||
bit_width: int,
|
||||
is_signed: bool,
|
||||
is_checked: bool,
|
||||
) -> set[int]:
|
||||
type_interval = NumericInterval.type_range(bit_width, is_signed)
|
||||
results: set[int] = set()
|
||||
for left_value in range(left.lower, left.upper + 1):
|
||||
for right_value in range(right.lower, right.upper + 1):
|
||||
product = left_value * right_value
|
||||
if is_checked:
|
||||
if type_interval.lower <= product <= type_interval.upper:
|
||||
results.add(product)
|
||||
else:
|
||||
results.add(_decode_wrapped(product, bit_width, is_signed))
|
||||
return results
|
||||
|
||||
|
||||
@pytest.mark.parametrize("bit_width", [2, 3])
|
||||
@pytest.mark.parametrize("is_signed", [False, True])
|
||||
@pytest.mark.parametrize("is_checked", [False, True])
|
||||
def test_multiplication_is_sound_for_every_small_width_interval(
|
||||
bit_width: int,
|
||||
is_signed: bool,
|
||||
is_checked: bool,
|
||||
) -> None:
|
||||
"""Every concrete successful product is contained in the abstract result."""
|
||||
type_interval = NumericInterval.type_range(bit_width, is_signed)
|
||||
intervals = _all_intervals(range(type_interval.lower, type_interval.upper + 1))
|
||||
|
||||
for left in intervals:
|
||||
for right in intervals:
|
||||
result = transfer_binary_interval(
|
||||
BinaryType.MULTIPLICATION,
|
||||
left,
|
||||
right,
|
||||
bit_width=bit_width,
|
||||
is_signed=is_signed,
|
||||
is_checked=is_checked,
|
||||
)
|
||||
concrete = _concrete_multiplication_results(
|
||||
left,
|
||||
right,
|
||||
bit_width=bit_width,
|
||||
is_signed=is_signed,
|
||||
is_checked=is_checked,
|
||||
)
|
||||
|
||||
assert type_interval.lower <= result.interval.lower
|
||||
assert result.interval.upper <= type_interval.upper
|
||||
assert result.supported
|
||||
assert all(
|
||||
result.interval.lower <= value <= result.interval.upper for value in concrete
|
||||
), (left, right, result, concrete)
|
||||
if not concrete:
|
||||
# Operation-local bottom is deliberately represented by top; the
|
||||
# checked continuation facts retain the infeasibility information.
|
||||
assert result.interval == type_interval
|
||||
|
||||
|
||||
@pytest.mark.parametrize(
|
||||
("left", "right", "is_signed", "expected"),
|
||||
[
|
||||
(_interval(2, 4), _interval(3, 5), False, _interval(6, 20)),
|
||||
(_interval(-3, 4), _interval(-2, 5), True, _interval(-15, 20)),
|
||||
(_interval(5), _interval(10), False, _interval(50)),
|
||||
],
|
||||
)
|
||||
def test_finite_checked_multiplication_is_algebraically_bounded(
|
||||
left: NumericInterval,
|
||||
right: NumericInterval,
|
||||
is_signed: bool,
|
||||
expected: NumericInterval,
|
||||
) -> None:
|
||||
result = transfer_binary_interval(
|
||||
BinaryType.MULTIPLICATION,
|
||||
left,
|
||||
right,
|
||||
bit_width=8,
|
||||
is_signed=is_signed,
|
||||
is_checked=True,
|
||||
)
|
||||
|
||||
assert result.interval == expected
|
||||
assert result.kind is (
|
||||
AbstractTransferKind.EXACT
|
||||
if expected.lower == expected.upper
|
||||
else AbstractTransferKind.INTERVAL
|
||||
)
|
||||
assert not result.may_wrap
|
||||
|
||||
|
||||
def test_checked_multiplication_keeps_only_successful_nonoverflowing_values() -> None:
|
||||
result = transfer_binary_interval(
|
||||
BinaryType.MULTIPLICATION,
|
||||
_interval(100, 200),
|
||||
_interval(2, 3),
|
||||
bit_width=8,
|
||||
is_signed=False,
|
||||
is_checked=True,
|
||||
)
|
||||
|
||||
assert result.interval == _interval(200, 255)
|
||||
assert result.kind is AbstractTransferKind.INTERVAL
|
||||
assert not result.may_wrap
|
||||
|
||||
|
||||
def test_checked_signed_square_uses_same_operand_relation() -> None:
|
||||
result = transfer_binary_interval(
|
||||
BinaryType.MULTIPLICATION,
|
||||
_interval(-3, 4),
|
||||
_interval(-3, 4),
|
||||
bit_width=8,
|
||||
is_signed=True,
|
||||
is_checked=True,
|
||||
same_operand=True,
|
||||
)
|
||||
|
||||
assert result.interval == _interval(0, 16)
|
||||
|
||||
|
||||
def test_unchecked_signed_square_returns_top_when_wrapping_can_change_sign() -> None:
|
||||
result = transfer_binary_interval(
|
||||
BinaryType.MULTIPLICATION,
|
||||
_interval(-128, 127),
|
||||
_interval(-128, 127),
|
||||
bit_width=8,
|
||||
is_signed=True,
|
||||
is_checked=False,
|
||||
same_operand=True,
|
||||
)
|
||||
|
||||
assert result.interval == _interval(-128, 127)
|
||||
assert result.kind is AbstractTransferKind.TOP
|
||||
assert result.may_wrap
|
||||
|
||||
|
||||
def test_unchecked_multiplication_wraps_constants_and_tops_nonconvex_images() -> None:
|
||||
constant = transfer_binary_interval(
|
||||
BinaryType.MULTIPLICATION,
|
||||
_interval(200),
|
||||
_interval(2),
|
||||
bit_width=8,
|
||||
is_signed=False,
|
||||
is_checked=False,
|
||||
)
|
||||
wrapping = transfer_binary_interval(
|
||||
BinaryType.MULTIPLICATION,
|
||||
_interval(200, 255),
|
||||
_interval(2),
|
||||
bit_width=8,
|
||||
is_signed=False,
|
||||
is_checked=False,
|
||||
)
|
||||
unconstrained = transfer_binary_interval(
|
||||
BinaryType.MULTIPLICATION,
|
||||
_interval(0, 255),
|
||||
_interval(0, 255),
|
||||
bit_width=8,
|
||||
is_signed=False,
|
||||
is_checked=False,
|
||||
)
|
||||
|
||||
assert constant.interval == _interval(144)
|
||||
assert constant.kind is AbstractTransferKind.EXACT
|
||||
assert constant.may_wrap
|
||||
assert wrapping.interval == unconstrained.interval == _interval(0, 255)
|
||||
assert wrapping.kind is unconstrained.kind is AbstractTransferKind.TOP
|
||||
assert wrapping.may_wrap and unconstrained.may_wrap
|
||||
|
||||
|
||||
@pytest.mark.parametrize(
|
||||
("operation", "left", "right", "is_signed", "expected"),
|
||||
[
|
||||
(BinaryType.DIVISION, _interval(10, 20), _interval(2, 5), False, _interval(2, 10)),
|
||||
(
|
||||
BinaryType.DIVISION,
|
||||
_interval(-20, 20),
|
||||
_interval(-5, -2),
|
||||
True,
|
||||
_interval(-10, 10),
|
||||
),
|
||||
(BinaryType.MODULO, _interval(10, 20), _interval(3, 5), False, _interval(0, 4)),
|
||||
(BinaryType.MODULO, _interval(-20, -10), _interval(3, 5), True, _interval(-4, 0)),
|
||||
(BinaryType.MODULO, _interval(-7), _interval(3), True, _interval(-1)),
|
||||
],
|
||||
)
|
||||
def test_division_and_modulo_representative_intervals(
|
||||
operation: BinaryType,
|
||||
left: NumericInterval,
|
||||
right: NumericInterval,
|
||||
is_signed: bool,
|
||||
expected: NumericInterval,
|
||||
) -> None:
|
||||
result = transfer_binary_interval(
|
||||
operation,
|
||||
left,
|
||||
right,
|
||||
bit_width=8,
|
||||
is_signed=is_signed,
|
||||
is_checked=True,
|
||||
)
|
||||
|
||||
assert result.interval == expected
|
||||
assert result.supported
|
||||
|
||||
|
||||
@pytest.mark.parametrize(
|
||||
("operation", "expected"),
|
||||
[
|
||||
(BinaryType.DIVISION, _interval(1)),
|
||||
(BinaryType.MODULO, _interval(0)),
|
||||
(BinaryType.AND, _interval(3, 9)),
|
||||
(BinaryType.OR, _interval(3, 9)),
|
||||
(BinaryType.CARET, _interval(0)),
|
||||
],
|
||||
)
|
||||
def test_same_operand_identities(operation: BinaryType, expected: NumericInterval) -> None:
|
||||
result = transfer_binary_interval(
|
||||
operation,
|
||||
_interval(3, 9),
|
||||
_interval(3, 9),
|
||||
bit_width=8,
|
||||
is_signed=False,
|
||||
is_checked=True,
|
||||
same_operand=True,
|
||||
)
|
||||
|
||||
assert result.interval == expected
|
||||
|
||||
|
||||
def test_zero_only_divisor_conservatively_returns_top() -> None:
|
||||
result = transfer_binary_interval(
|
||||
BinaryType.DIVISION,
|
||||
_interval(1, 10),
|
||||
_interval(0),
|
||||
bit_width=8,
|
||||
is_signed=False,
|
||||
is_checked=True,
|
||||
)
|
||||
|
||||
assert result.interval == _interval(0, 255)
|
||||
assert result.kind is AbstractTransferKind.TOP
|
||||
|
||||
|
||||
@pytest.mark.parametrize(
|
||||
"case",
|
||||
[
|
||||
(_interval(2, 3), _interval(2), 8, False, True, _interval(4, 9)),
|
||||
(_interval(-3, 2), _interval(2), 8, True, True, _interval(0, 9)),
|
||||
(_interval(2, 3), _interval(2, 3), 8, False, True, _interval(4, 27)),
|
||||
(_interval(0), _interval(0, 3), 8, False, True, _interval(0, 1)),
|
||||
(_interval(20), _interval(2), 8, False, False, _interval(144)),
|
||||
],
|
||||
)
|
||||
def test_power_representative_intervals(
|
||||
case: tuple[NumericInterval, NumericInterval, int, bool, bool, NumericInterval],
|
||||
) -> None:
|
||||
base, exponent, bit_width, is_signed, is_checked, expected = case
|
||||
result = transfer_binary_interval(
|
||||
BinaryType.POWER,
|
||||
base,
|
||||
exponent,
|
||||
bit_width=bit_width,
|
||||
is_signed=is_signed,
|
||||
is_checked=is_checked,
|
||||
)
|
||||
|
||||
assert result.interval == expected
|
||||
|
||||
|
||||
def test_unbounded_power_is_tagged_unsupported_top() -> None:
|
||||
result = transfer_binary_interval(
|
||||
BinaryType.POWER,
|
||||
_interval(2, 3),
|
||||
_interval(0, 2048),
|
||||
bit_width=16,
|
||||
is_signed=False,
|
||||
is_checked=True,
|
||||
)
|
||||
|
||||
assert result.interval == _interval(0, (1 << 16) - 1)
|
||||
assert result.kind is AbstractTransferKind.TOP
|
||||
assert not result.supported
|
||||
|
||||
|
||||
@pytest.mark.parametrize(
|
||||
("operation", "left", "right", "is_signed", "expected"),
|
||||
[
|
||||
(BinaryType.LEFT_SHIFT, _interval(1, 3), _interval(1), False, _interval(2, 6)),
|
||||
(BinaryType.RIGHT_SHIFT, _interval(8, 16), _interval(1, 2), False, _interval(2, 8)),
|
||||
(BinaryType.RIGHT_SHIFT, _interval(-8, -1), _interval(1), True, _interval(-4, -1)),
|
||||
(BinaryType.RIGHT_SHIFT, _interval(-8, 7), _interval(8), True, _interval(-1, 0)),
|
||||
],
|
||||
)
|
||||
def test_shift_representative_intervals(
|
||||
operation: BinaryType,
|
||||
left: NumericInterval,
|
||||
right: NumericInterval,
|
||||
is_signed: bool,
|
||||
expected: NumericInterval,
|
||||
) -> None:
|
||||
result = transfer_binary_interval(
|
||||
operation,
|
||||
left,
|
||||
right,
|
||||
bit_width=8,
|
||||
is_signed=is_signed,
|
||||
is_checked=True,
|
||||
)
|
||||
|
||||
assert result.interval == expected
|
||||
|
||||
|
||||
def test_left_shift_wraps_constants_and_tops_nonconvex_images() -> None:
|
||||
constant = transfer_binary_interval(
|
||||
BinaryType.LEFT_SHIFT,
|
||||
_interval(200),
|
||||
_interval(1),
|
||||
bit_width=8,
|
||||
is_signed=False,
|
||||
is_checked=True,
|
||||
)
|
||||
interval = transfer_binary_interval(
|
||||
BinaryType.LEFT_SHIFT,
|
||||
_interval(100, 200),
|
||||
_interval(1),
|
||||
bit_width=8,
|
||||
is_signed=False,
|
||||
is_checked=True,
|
||||
)
|
||||
|
||||
assert constant.interval == _interval(144)
|
||||
assert constant.kind is AbstractTransferKind.EXACT
|
||||
assert constant.may_wrap
|
||||
assert interval.interval == _interval(0, 255)
|
||||
assert interval.kind is AbstractTransferKind.TOP
|
||||
assert interval.may_wrap
|
||||
|
||||
|
||||
@pytest.mark.parametrize(
|
||||
("operation", "left", "right", "expected"),
|
||||
[
|
||||
(BinaryType.AND, _interval(0b1010), _interval(0b1100), _interval(0b1000)),
|
||||
(BinaryType.OR, _interval(0b1010), _interval(0b0101), _interval(0b1111)),
|
||||
(BinaryType.CARET, _interval(0b1010), _interval(0b1100), _interval(0b0110)),
|
||||
(BinaryType.AND, _interval(0, 15), _interval(0, 3), _interval(0, 3)),
|
||||
(BinaryType.OR, _interval(1, 2), _interval(4), _interval(0, 7)),
|
||||
],
|
||||
)
|
||||
def test_bitwise_representative_intervals(
|
||||
operation: BinaryType,
|
||||
left: NumericInterval,
|
||||
right: NumericInterval,
|
||||
expected: NumericInterval,
|
||||
) -> None:
|
||||
result = transfer_binary_interval(
|
||||
operation,
|
||||
left,
|
||||
right,
|
||||
bit_width=8,
|
||||
is_signed=False,
|
||||
is_checked=True,
|
||||
)
|
||||
|
||||
assert result.interval == expected
|
||||
assert result.supported
|
||||
|
||||
|
||||
@pytest.mark.parametrize("operation", [BinaryType.AND, BinaryType.OR, BinaryType.CARET])
|
||||
def test_nonconstant_signed_bitwise_conservatively_returns_unsupported_top(
|
||||
operation: BinaryType,
|
||||
) -> None:
|
||||
result = transfer_binary_interval(
|
||||
operation,
|
||||
_interval(-8, 3),
|
||||
_interval(-2, 5),
|
||||
bit_width=8,
|
||||
is_signed=True,
|
||||
is_checked=True,
|
||||
)
|
||||
|
||||
assert result.interval == _interval(-128, 127)
|
||||
assert result.kind is AbstractTransferKind.TOP
|
||||
assert not result.supported
|
||||
|
||||
|
||||
def test_unhandled_binary_operation_conservatively_returns_unsupported_top() -> None:
|
||||
result = transfer_binary_interval(
|
||||
BinaryType.LESS,
|
||||
_interval(1, 3),
|
||||
_interval(2, 4),
|
||||
bit_width=8,
|
||||
is_signed=False,
|
||||
is_checked=True,
|
||||
)
|
||||
|
||||
assert result.interval == _interval(0, 255)
|
||||
assert result.kind is AbstractTransferKind.TOP
|
||||
assert not result.supported
|
||||
@@ -266,7 +266,7 @@ def test_nonpersistent_ownership_boundaries_do_not_fall_back_to_assertions() ->
|
||||
assert solver.register_property_obligation(property_fact)
|
||||
assert solver.get_assertions() == []
|
||||
|
||||
with pytest.raises(NotImplementedError, match="generation-scoped query sessions"):
|
||||
with pytest.raises(NotImplementedError, match="owned by LoopHeaderFixpoint"):
|
||||
solver.register_loop_generation_fact(loop_fact)
|
||||
assert solver.get_assertions() == []
|
||||
|
||||
|
||||
@@ -0,0 +1,324 @@
|
||||
"""Tests for dominator-defined loop fixpoints and generation ownership."""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass, field
|
||||
|
||||
from slither.analyses.data_flow.analyses.interval.analysis.analysis import (
|
||||
IntervalAnalysis,
|
||||
)
|
||||
from slither.analyses.data_flow.analyses.interval.analysis.domain import (
|
||||
DomainVariant,
|
||||
IntervalDomain,
|
||||
)
|
||||
from slither.analyses.data_flow.analyses.interval.core.state import ComparisonInfo, State
|
||||
from slither.analyses.data_flow.analyses.interval.core.tracked_variable import (
|
||||
NumericInterval,
|
||||
TrackedSMTVariable,
|
||||
)
|
||||
from slither.analyses.data_flow.engine.analysis import Analysis
|
||||
from slither.analyses.data_flow.engine.direction import Direction, Forward
|
||||
from slither.analyses.data_flow.engine.domain import Domain
|
||||
from slither.analyses.data_flow.engine.loop import (
|
||||
ControlFlowEdgeId,
|
||||
LoopHeaderFixpoint,
|
||||
LoopStructure,
|
||||
LoopVariableId,
|
||||
LoopWideningContext,
|
||||
LoopWideningResult,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver import Z3Solver
|
||||
from slither.analyses.data_flow.smt_solver.facts import (
|
||||
AnalysisContextId,
|
||||
EncodingId,
|
||||
Fact,
|
||||
FactId,
|
||||
FactKind,
|
||||
FactOriginKind,
|
||||
FactOwnerKind,
|
||||
FactProvenance,
|
||||
LoopHeaderId,
|
||||
StaticOperationId,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.types import Sort, SortKind
|
||||
|
||||
|
||||
ENCODING_ID = EncodingId("loop_fixpoint.sol", "C.f()")
|
||||
CONTEXT_ID = AnalysisContextId(ENCODING_ID)
|
||||
HEADER_ID = LoopHeaderId(ENCODING_ID, 2)
|
||||
|
||||
|
||||
@dataclass
|
||||
class _Filename:
|
||||
relative: str = "loop_fixpoint.sol"
|
||||
|
||||
|
||||
@dataclass
|
||||
class _SourceMapping:
|
||||
filename: _Filename = field(default_factory=_Filename)
|
||||
|
||||
|
||||
@dataclass
|
||||
class _FunctionStub:
|
||||
canonical_name: str = "C.f()"
|
||||
source_mapping: _SourceMapping = field(default_factory=_SourceMapping)
|
||||
nodes: list[_NodeStub] = field(default_factory=list)
|
||||
|
||||
|
||||
@dataclass(eq=False)
|
||||
class _NodeStub:
|
||||
node_id: int
|
||||
function: _FunctionStub
|
||||
sons: list[_NodeStub] = field(default_factory=list)
|
||||
fathers: list[_NodeStub] = field(default_factory=list)
|
||||
dominators: set[_NodeStub] = field(default_factory=set)
|
||||
|
||||
|
||||
def _loop_cfg() -> tuple[_FunctionStub, dict[int, _NodeStub]]:
|
||||
function = _FunctionStub()
|
||||
nodes = {node_id: _NodeStub(node_id, function) for node_id in range(1, 6)}
|
||||
edges = ((1, 2), (2, 3), (2, 5), (3, 4), (4, 2))
|
||||
for source_id, destination_id in edges:
|
||||
source = nodes[source_id]
|
||||
destination = nodes[destination_id]
|
||||
source.sons.append(destination)
|
||||
destination.fathers.append(source)
|
||||
nodes[1].dominators = {nodes[1]}
|
||||
nodes[2].dominators = {nodes[1], nodes[2]}
|
||||
nodes[3].dominators = {nodes[1], nodes[2], nodes[3]}
|
||||
nodes[4].dominators = {nodes[1], nodes[2], nodes[3], nodes[4]}
|
||||
nodes[5].dominators = {nodes[1], nodes[2], nodes[5]}
|
||||
function.nodes = list(nodes.values())
|
||||
return function, nodes
|
||||
|
||||
|
||||
def _solver() -> Z3Solver:
|
||||
solver = Z3Solver()
|
||||
solver.bind_function_encoding(ENCODING_ID)
|
||||
return solver
|
||||
|
||||
|
||||
def _tracked(
|
||||
solver: Z3Solver,
|
||||
name: str,
|
||||
lower: int,
|
||||
upper: int,
|
||||
*,
|
||||
total: bool = True,
|
||||
) -> TrackedSMTVariable:
|
||||
variable = TrackedSMTVariable.create(
|
||||
solver,
|
||||
name,
|
||||
Sort(SortKind.BITVEC, [8]),
|
||||
bit_width=8,
|
||||
)
|
||||
return variable.with_interval(NumericInterval(lower, upper), is_total=total)
|
||||
|
||||
|
||||
def _domain(solver: Z3Solver, lower: int, upper: int) -> IntervalDomain:
|
||||
return IntervalDomain.with_state(
|
||||
State({"x": _tracked(solver, "x", lower, upper)}, context_id=CONTEXT_ID)
|
||||
)
|
||||
|
||||
|
||||
class _RecordingAnalysis(Analysis):
|
||||
def __init__(self) -> None:
|
||||
self.contexts: list[LoopWideningContext] = []
|
||||
self._direction = Forward()
|
||||
|
||||
def domain(self) -> Domain:
|
||||
return IntervalDomain.with_state(State(context_id=CONTEXT_ID))
|
||||
|
||||
def direction(self) -> Direction:
|
||||
return self._direction
|
||||
|
||||
def transfer_function(self, node: object, domain: Domain, operation: object) -> None:
|
||||
return None
|
||||
|
||||
def bottom_value(self) -> Domain:
|
||||
return IntervalDomain.bottom(CONTEXT_ID)
|
||||
|
||||
def apply_loop_widening(self, context: LoopWideningContext) -> LoopWideningResult:
|
||||
self.contexts.append(context)
|
||||
fact = Fact(
|
||||
fact_id=FactId(
|
||||
owner=FactOwnerKind.LOOP_GENERATION,
|
||||
kind=FactKind.RANGE_BOUND,
|
||||
provenance=FactProvenance(
|
||||
context_id=CONTEXT_ID,
|
||||
origin_kind=FactOriginKind.LOOP,
|
||||
loop_header_id=context.header_id,
|
||||
loop_generation=context.generation,
|
||||
),
|
||||
semantic_key=("generation", str(context.generation)),
|
||||
),
|
||||
formula=context.generation,
|
||||
)
|
||||
return LoopWideningResult(context.current_input, (fact,))
|
||||
|
||||
|
||||
def test_natural_loop_classification_excludes_preheader_and_is_stable() -> None:
|
||||
function, nodes = _loop_cfg()
|
||||
first = LoopStructure.from_function(function)
|
||||
function.nodes.reverse()
|
||||
second = LoopStructure.from_function(function)
|
||||
preheader = ControlFlowEdgeId(1, 2)
|
||||
back_edge = ControlFlowEdgeId(4, 2)
|
||||
|
||||
assert not first.is_back_edge(preheader)
|
||||
assert first.is_back_edge(back_edge)
|
||||
assert first.loops == second.loops
|
||||
assert first.loops[0].entry_edges == frozenset({preheader})
|
||||
assert first.loops[0].back_edges == frozenset({back_edge})
|
||||
assert first.loops[0].header_id == LoopHeaderId.from_node(nodes[2])
|
||||
assert LoopHeaderId.from_node(nodes[2]) == LoopHeaderId.from_node(nodes[2])
|
||||
|
||||
|
||||
def test_generation_advances_only_for_changed_header_approximation() -> None:
|
||||
solver = _solver()
|
||||
analysis = _RecordingAnalysis()
|
||||
tracker = LoopHeaderFixpoint(HEADER_ID, ())
|
||||
entry = ControlFlowEdgeId(1, 2)
|
||||
back = ControlFlowEdgeId(4, 2)
|
||||
|
||||
assert tracker.update(entry, _domain(solver, 0, 0), False, analysis).changed
|
||||
tracker.record_output(_domain(solver, 0, 0))
|
||||
assert tracker.update(back, _domain(solver, 1, 1), True, analysis).changed
|
||||
assert tracker.generation == 1
|
||||
assert not tracker.update(back, _domain(solver, 1, 1), True, analysis).changed
|
||||
assert tracker.generation == 1
|
||||
assert len(analysis.contexts) == 1
|
||||
|
||||
|
||||
def test_widening_context_keeps_previous_and_current_semantic_states_separate() -> None:
|
||||
solver = _solver()
|
||||
analysis = _RecordingAnalysis()
|
||||
tracker = LoopHeaderFixpoint(HEADER_ID, ())
|
||||
entry_state = _domain(solver, 0, 0)
|
||||
output_state = _domain(solver, 0, 1)
|
||||
|
||||
tracker.update(ControlFlowEdgeId(1, 2), entry_state, False, analysis)
|
||||
tracker.record_output(output_state)
|
||||
tracker.update(ControlFlowEdgeId(4, 2), _domain(solver, 2, 3), True, analysis)
|
||||
context = analysis.contexts[0]
|
||||
|
||||
assert context.previous_input.semantic_id() == entry_state.semantic_id()
|
||||
assert context.current_input.semantic_id() != context.previous_input.semantic_id()
|
||||
assert context.previous_output is not None
|
||||
assert context.previous_output.semantic_id() == output_state.semantic_id()
|
||||
assert context.previous_input is not context.current_input
|
||||
|
||||
|
||||
def test_generation_facts_replace_obsolete_generation() -> None:
|
||||
solver = _solver()
|
||||
analysis = _RecordingAnalysis()
|
||||
tracker = LoopHeaderFixpoint(HEADER_ID, ())
|
||||
entry = ControlFlowEdgeId(1, 2)
|
||||
back = ControlFlowEdgeId(4, 2)
|
||||
|
||||
tracker.update(entry, _domain(solver, 0, 0), False, analysis)
|
||||
tracker.record_output(_domain(solver, 0, 0))
|
||||
tracker.update(back, _domain(solver, 1, 1), True, analysis)
|
||||
first_ids = tracker.generation_fact_ids
|
||||
tracker.record_output(_domain(solver, 0, 1))
|
||||
tracker.update(back, _domain(solver, 1, 2), True, analysis)
|
||||
|
||||
assert tracker.generation == 2
|
||||
assert first_ids.isdisjoint(tracker.generation_fact_ids)
|
||||
assert {fact.fact_id.provenance.loop_generation for fact in tracker.generation_facts} == {2}
|
||||
|
||||
|
||||
def _run_multiple_back_edges(order: tuple[ControlFlowEdgeId, ...]) -> IntervalDomain:
|
||||
solver = _solver()
|
||||
analysis = _RecordingAnalysis()
|
||||
tracker = LoopHeaderFixpoint(HEADER_ID, ())
|
||||
states = {
|
||||
ControlFlowEdgeId(4, 2): _domain(solver, 1, 5),
|
||||
ControlFlowEdgeId(5, 2): _domain(solver, 10, 20),
|
||||
}
|
||||
tracker.update(ControlFlowEdgeId(1, 2), _domain(solver, 0, 0), False, analysis)
|
||||
tracker.record_output(_domain(solver, 0, 0))
|
||||
for edge in order:
|
||||
tracker.update(edge, states[edge], True, analysis)
|
||||
assert isinstance(tracker.current_input, IntervalDomain)
|
||||
assert tracker.generation == 1
|
||||
return tracker.current_input
|
||||
|
||||
|
||||
def test_multiple_back_edges_join_independently_of_arrival_order() -> None:
|
||||
first = ControlFlowEdgeId(4, 2)
|
||||
second = ControlFlowEdgeId(5, 2)
|
||||
left = _run_multiple_back_edges((first, second))
|
||||
right = _run_multiple_back_edges((second, first))
|
||||
|
||||
assert left.semantic_id() == right.semantic_id()
|
||||
assert left.state is not None
|
||||
assert left.state.get_variable("x").interval == NumericInterval(0, 20)
|
||||
|
||||
|
||||
def test_interval_widening_preserves_complete_state_and_solver_ownership() -> None:
|
||||
solver = _solver()
|
||||
analysis = IntervalAnalysis(solver, timeout_ms=10)
|
||||
entry = _tracked(solver, "x_entry", 0, 0)
|
||||
back = _tracked(solver, "x_back", 1, 5, total=False)
|
||||
marker = _tracked(solver, "marker", 7, 7)
|
||||
operation_id = StaticOperationId(ENCODING_ID, 9, 0)
|
||||
comparison = ComparisonInfo(back.term < 10, operation_id)
|
||||
fact = Fact(
|
||||
fact_id=FactId(
|
||||
owner=FactOwnerKind.STATE_LOCAL,
|
||||
kind=FactKind.PATH_CONDITION,
|
||||
provenance=FactProvenance(
|
||||
context_id=CONTEXT_ID,
|
||||
origin_kind=FactOriginKind.CFG_EDGE,
|
||||
operation_id=operation_id,
|
||||
),
|
||||
semantic_key=("preserved",),
|
||||
),
|
||||
formula=back.term != 0,
|
||||
)
|
||||
current = IntervalDomain.with_state(
|
||||
State(
|
||||
{"x_entry": entry, "x_back": back, "marker": marker},
|
||||
{"condition": comparison},
|
||||
facts=(fact,),
|
||||
dependencies={"x_back": {"source"}},
|
||||
storage_slots={"0": ["marker"]},
|
||||
context_id=CONTEXT_ID,
|
||||
)
|
||||
)
|
||||
previous_output = IntervalDomain.with_state(
|
||||
State({"x_phi": _tracked(solver, "x_phi", 0, 0)}, context_id=CONTEXT_ID)
|
||||
)
|
||||
context = LoopWideningContext(
|
||||
HEADER_ID,
|
||||
1,
|
||||
_domain(solver, 0, 0),
|
||||
current,
|
||||
previous_output,
|
||||
(LoopVariableId("x_phi", ("x_entry",), ("x_back",)),),
|
||||
)
|
||||
encoding_before = solver.function_encoding.fact_ids()
|
||||
|
||||
result = analysis.apply_loop_widening(context)
|
||||
|
||||
assert isinstance(result.state, IntervalDomain)
|
||||
assert result.state.variant is DomainVariant.STATE
|
||||
assert result.state.state is not None
|
||||
widened = result.state.state
|
||||
assert widened.get_variable("x_back").interval == NumericInterval(1, 255)
|
||||
assert not widened.get_variable("x_back").is_total
|
||||
assert widened.get_variable("marker").interval == NumericInterval(7, 7)
|
||||
assert widened.get_dependencies("x_back") == {"source"}
|
||||
assert widened.get_storage_writes("0") == ["marker"]
|
||||
assert not widened.storage_may_be_unwritten("0")
|
||||
assert widened.get_comparison("condition") == comparison
|
||||
assert widened.get_explicit_fact_ids() == frozenset({fact.fact_id})
|
||||
assert widened.context_id == CONTEXT_ID
|
||||
assert result.generation_facts
|
||||
assert all(
|
||||
fact.fact_id.owner is FactOwnerKind.LOOP_GENERATION for fact in result.generation_facts
|
||||
)
|
||||
assert all(fact.fact_id not in widened.get_fact_ids() for fact in result.generation_facts)
|
||||
assert solver.function_encoding.fact_ids() == encoding_before
|
||||
assert solver.active_query_sessions == 0
|
||||
@@ -381,6 +381,9 @@ def test_proven_timeout_and_abstract_full_ranges_are_tagged_differently() -> Non
|
||||
BoundStatus.ABSTRACT,
|
||||
BoundStatus.ABSTRACT,
|
||||
)
|
||||
assert abstract.feasibility is FeasibilityStatus.NOT_ATTEMPTED
|
||||
assert abstract.diagnostics.sessions == ()
|
||||
assert abstract_solver.active_query_sessions == 0
|
||||
assert proven.fallback_range is None
|
||||
assert timed_out.fallback_range == abstract.fallback_range == RangeInterval(0, 255)
|
||||
assert proven.to_dict()["lower_status"] == "proven"
|
||||
|
||||
@@ -0,0 +1,256 @@
|
||||
"""Stage 5 abstract-first range refinement and total-budget tests."""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from typing import Any
|
||||
|
||||
from slither.analyses.data_flow.analyses.interval.core.state import State
|
||||
from slither.analyses.data_flow.analyses.interval.core.tracked_variable import (
|
||||
NumericInterval,
|
||||
TrackedSMTVariable,
|
||||
)
|
||||
from slither.analyses.data_flow.analysis import RangeQueryConfig, solve_variable_range
|
||||
from slither.analyses.data_flow.smt_solver import Z3Solver
|
||||
from slither.analyses.data_flow.smt_solver.facts import (
|
||||
AnalysisContextId,
|
||||
EncodingId,
|
||||
StaticOperationId,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.query import (
|
||||
BoundOutcome,
|
||||
BoundStatus,
|
||||
FeasibilityResult,
|
||||
FeasibilityStatus,
|
||||
QueryBudget,
|
||||
QueryDiagnostics,
|
||||
RangeInterval,
|
||||
empty_state_id,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.telemetry import (
|
||||
disable_telemetry,
|
||||
enable_telemetry,
|
||||
reset_telemetry,
|
||||
)
|
||||
from slither.analyses.data_flow.smt_solver.types import Sort, SortKind
|
||||
|
||||
|
||||
ENCODING_ID = EncodingId("range_refinement.sol", "C.f()")
|
||||
CONTEXT_ID = AnalysisContextId(ENCODING_ID)
|
||||
|
||||
|
||||
def _solver() -> Z3Solver:
|
||||
solver = Z3Solver()
|
||||
solver.bind_function_encoding(ENCODING_ID)
|
||||
return solver
|
||||
|
||||
|
||||
def _tracked(
|
||||
solver: Z3Solver,
|
||||
interval: NumericInterval,
|
||||
*,
|
||||
operation_result: bool,
|
||||
) -> TrackedSMTVariable:
|
||||
variable = TrackedSMTVariable.create(
|
||||
solver,
|
||||
"x",
|
||||
Sort(SortKind.BITVEC, [8]),
|
||||
bit_width=8,
|
||||
).with_interval(interval)
|
||||
if operation_result:
|
||||
variable = variable.with_overflow_predicates(
|
||||
operation_id=StaticOperationId(ENCODING_ID, 1, 0)
|
||||
)
|
||||
return variable
|
||||
|
||||
|
||||
def test_abstract_top_operation_avoids_every_solver_session() -> None:
|
||||
telemetry = enable_telemetry()
|
||||
reset_telemetry()
|
||||
solver = _solver()
|
||||
variable = _tracked(solver, NumericInterval(0, 255), operation_result=True)
|
||||
state = State({"x": variable}, context_id=CONTEXT_ID)
|
||||
before_encoding = solver.function_encoding.fact_ids()
|
||||
before_state = state.semantic_id()
|
||||
|
||||
try:
|
||||
lower, upper = solve_variable_range(
|
||||
solver,
|
||||
variable,
|
||||
RangeQueryConfig(
|
||||
state_id=before_state,
|
||||
state_facts=state.get_facts(),
|
||||
timeout_ms=1000,
|
||||
),
|
||||
)
|
||||
|
||||
assert lower == {
|
||||
"value": 0,
|
||||
"overflow": False,
|
||||
"bound_status": "abstract",
|
||||
"feasibility": "not_attempted",
|
||||
}
|
||||
assert upper == {
|
||||
"value": 255,
|
||||
"overflow": False,
|
||||
"bound_status": "abstract",
|
||||
"feasibility": "not_attempted",
|
||||
}
|
||||
sessions = telemetry.evaluation.query_sessions
|
||||
assert sessions.created == sessions.closed == sessions.active == 0
|
||||
refinements = telemetry.evaluation.range_refinements
|
||||
assert refinements.abstract_only == refinements.sessions_avoided == 1
|
||||
assert solver.function_encoding.fact_ids() == before_encoding
|
||||
assert state.semantic_id() == before_state
|
||||
finally:
|
||||
disable_telemetry()
|
||||
|
||||
|
||||
def test_finite_abstract_interval_avoids_refinement_by_default() -> None:
|
||||
telemetry = enable_telemetry()
|
||||
reset_telemetry()
|
||||
solver = _solver()
|
||||
variable = _tracked(solver, NumericInterval(10, 20), operation_result=False)
|
||||
state = State({"x": variable}, context_id=CONTEXT_ID)
|
||||
|
||||
try:
|
||||
lower, upper = solve_variable_range(
|
||||
solver,
|
||||
variable,
|
||||
RangeQueryConfig(
|
||||
state_id=state.semantic_id(),
|
||||
state_facts=state.get_facts(),
|
||||
timeout_ms=1000,
|
||||
),
|
||||
)
|
||||
|
||||
assert lower is not None and upper is not None
|
||||
assert (lower["value"], upper["value"]) == (10, 20)
|
||||
assert lower["bound_status"] == upper["bound_status"] == "abstract"
|
||||
assert telemetry.evaluation.query_sessions.created == 0
|
||||
finally:
|
||||
disable_telemetry()
|
||||
|
||||
|
||||
def test_optional_refinement_uses_tracked_fallback_and_balances_sessions() -> None:
|
||||
telemetry = enable_telemetry()
|
||||
reset_telemetry()
|
||||
solver = _solver()
|
||||
variable = _tracked(solver, NumericInterval(10, 20), operation_result=False)
|
||||
state = State({"x": variable}, context_id=CONTEXT_ID)
|
||||
encoding_before = solver.function_encoding.fact_ids()
|
||||
state_before = state.semantic_id()
|
||||
|
||||
try:
|
||||
lower, upper = solve_variable_range(
|
||||
solver,
|
||||
variable,
|
||||
RangeQueryConfig(
|
||||
state_id=state.semantic_id(),
|
||||
state_facts=state.get_facts(),
|
||||
timeout_ms=1000,
|
||||
refine_abstract=True,
|
||||
),
|
||||
)
|
||||
|
||||
assert lower is not None and upper is not None
|
||||
assert (lower["value"], upper["value"]) == (10, 20)
|
||||
assert lower["bound_status"] == upper["bound_status"] == "proven"
|
||||
sessions = telemetry.evaluation.query_sessions
|
||||
assert sessions.created == sessions.closed == 3
|
||||
assert sessions.active == sessions.cleanup_imbalances == 0
|
||||
assert sessions.query_facts_materialized == 6
|
||||
assert solver.function_encoding.fact_ids() == encoding_before
|
||||
assert state.semantic_id() == state_before
|
||||
finally:
|
||||
disable_telemetry()
|
||||
|
||||
|
||||
class _FakeClock:
|
||||
def __init__(self) -> None:
|
||||
self.now = 0.0
|
||||
|
||||
def __call__(self) -> float:
|
||||
return self.now
|
||||
|
||||
def advance_ms(self, milliseconds: int) -> None:
|
||||
self.now += milliseconds / 1000
|
||||
|
||||
|
||||
class _BudgetSolver(Z3Solver):
|
||||
minimum_session_budget_ms = 0
|
||||
backend_timeout_fraction = 1.0
|
||||
|
||||
def __init__(self, clock: _FakeClock) -> None:
|
||||
super().__init__()
|
||||
self.clock = clock
|
||||
self.allocations: list[tuple[str, int]] = []
|
||||
|
||||
def _range_feasibility(self, *, timeout_ms: int, **query: Any) -> FeasibilityResult:
|
||||
del query
|
||||
self.allocations.append(("feasibility", timeout_ms))
|
||||
self.clock.advance_ms(2)
|
||||
state_id = empty_state_id(self.function_encoding.encoding_id)
|
||||
return FeasibilityResult(
|
||||
FeasibilityStatus.SAT,
|
||||
self.function_encoding.encoding_id,
|
||||
state_id,
|
||||
QueryDiagnostics(),
|
||||
)
|
||||
|
||||
def _execute_bound_query(
|
||||
self,
|
||||
term: Any,
|
||||
objective_term: Any,
|
||||
*,
|
||||
purpose: Any,
|
||||
timeout_ms: int,
|
||||
**query: Any,
|
||||
) -> BoundOutcome:
|
||||
del term, objective_term, query
|
||||
self.allocations.append((purpose.value, timeout_ms))
|
||||
self.clock.advance_ms(timeout_ms)
|
||||
return BoundOutcome(3, BoundStatus.PROVEN)
|
||||
|
||||
|
||||
def test_one_total_budget_retains_lower_and_skips_expired_upper() -> None:
|
||||
clock = _FakeClock()
|
||||
solver = _BudgetSolver(clock)
|
||||
solver.bind_function_encoding(ENCODING_ID)
|
||||
term = solver.get_or_declare_const("x", Sort(SortKind.BITVEC, [8])).term
|
||||
budget = QueryBudget(10, clock=clock)
|
||||
|
||||
result = solver.solve_range_result(
|
||||
term,
|
||||
timeout_ms=1000,
|
||||
fallback_range=RangeInterval(0, 255),
|
||||
budget=budget,
|
||||
)
|
||||
|
||||
assert solver.allocations == [("feasibility", 10), ("lower_bound", 8)]
|
||||
assert result.lower == 3
|
||||
assert result.lower_status is BoundStatus.PROVEN
|
||||
assert result.upper == 255
|
||||
assert result.upper_status is BoundStatus.TIMEOUT
|
||||
assert result.fallback_range == RangeInterval(0, 255)
|
||||
assert result.diagnostics.total_budget_ms == 10
|
||||
assert result.diagnostics.budget_exhausted
|
||||
assert result.diagnostics.wall_elapsed_ms == 10
|
||||
assert solver.active_query_sessions == 0
|
||||
|
||||
|
||||
def test_tiny_budget_is_not_spent_opening_a_z3_session() -> None:
|
||||
telemetry = enable_telemetry()
|
||||
reset_telemetry()
|
||||
solver = _solver()
|
||||
term = solver.get_or_declare_const("tiny", Sort(SortKind.BITVEC, [8])).term
|
||||
|
||||
try:
|
||||
result = solver.solve_range_result(term, timeout_ms=20)
|
||||
|
||||
assert result.lower_status is BoundStatus.TIMEOUT
|
||||
assert result.upper_status is BoundStatus.TIMEOUT
|
||||
assert result.diagnostics.budget_exhausted
|
||||
sessions = telemetry.evaluation.query_sessions
|
||||
assert sessions.created == sessions.closed == 0
|
||||
finally:
|
||||
disable_telemetry()
|
||||
Reference in New Issue
Block a user