Compose native area flooding and recover visibility bit output
Browse files- docs/ASSET_PIPELINE_TODO.md +2 -0
- docs/FINDINGS.md +6 -0
- docs/PROVISIONAL_TODO.md +2 -0
- docs/RESEARCH_LEDGER.md +4 -0
- docs/REVERSE_ENGINEERING_TODO.md +5 -0
- docs/research/AREA_FLOODING.md +45 -0
- docs/research/BSP_REFERENCES.md +2 -0
- docs/research/README.md +2 -0
- docs/research/area-flooding.json +0 -0
- scripts/analyze_area_flooding.py +114 -0
- scripts/analyze_collision_composition.py +13 -7
- scripts/test_area_flooding.py +104 -0
docs/ASSET_PIPELINE_TODO.md
CHANGED
|
@@ -206,3 +206,5 @@ Native collision follow-up: [BSP planes](research/BSP_PLANES.md) records type/si
|
|
| 206 |
Native loading follow-up: [BSP payload loading](research/BSP_LOADING.md) connects plane/node/leaf descriptors 2/3/4 to native conversion. Preserve original disk fields and every map variant; native collision projection omits fields that rendering or other consumers may need. Complete range/reference validation and actual-map conversion remain RE-324 work.
|
| 207 |
|
| 208 |
Reference follow-up: [leaf references and area state](research/BSP_REFERENCES.md) connects native leaf words to brush/surface index arrays and records standalone copy behavior. Validate every source reference and prove inline-loader equivalence before implementing conversion; retain disk bounds and every variant (RE-328).
|
|
|
|
|
|
|
|
|
| 206 |
Native loading follow-up: [BSP payload loading](research/BSP_LOADING.md) connects plane/node/leaf descriptors 2/3/4 to native conversion. Preserve original disk fields and every map variant; native collision projection omits fields that rendering or other consumers may need. Complete range/reference validation and actual-map conversion remain RE-324 work.
|
| 207 |
|
| 208 |
Reference follow-up: [leaf references and area state](research/BSP_REFERENCES.md) connects native leaf words to brush/surface index arrays and records standalone copy behavior. Validate every source reference and prove inline-loader equivalence before implementing conversion; retain disk bounds and every variant (RE-328).
|
| 209 |
+
|
| 210 |
+
Area-state follow-up: [flooding and bit output](research/AREA_FLOODING.md) composes supplied portal matrices and generated labels, without loading actual maps. Validate area/reference ranges and lifecycle across every BSP variant before integrating conversion with runtime visibility (RE-332).
|
docs/FINDINGS.md
CHANGED
|
@@ -348,3 +348,9 @@ Bounded qagame paths recover bomb-plant/inactivity correction requests, direct f
|
|
| 348 |
**F-104 — Observed connectivity priority:** nonzero cm_noAreas returns true before index checks; either negative index returns false before upper bounds; valid areas compare labels in eight-byte records. Supplied labels establish local outcomes, not proven flood generation or runtime connectivity. [REF-002](research/BSP_REFERENCES.md).
|
| 349 |
|
| 350 |
**F-105 — Observed portal references:** nonzero open increments both directed counters and zero decrements both; self-pairs mutate twice. Close-underflow is checked after writes, and successful updates increment the epoch before requesting flooding. Full flood/lifecycle/query composition and runtime safety remain open. [REF-003](research/BSP_REFERENCES.md).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 348 |
**F-104 — Observed connectivity priority:** nonzero cm_noAreas returns true before index checks; either negative index returns false before upper bounds; valid areas compare labels in eight-byte records. Supplied labels establish local outcomes, not proven flood generation or runtime connectivity. [REF-002](research/BSP_REFERENCES.md).
|
| 349 |
|
| 350 |
**F-105 — Observed portal references:** nonzero open increments both directed counters and zero decrements both; self-pairs mutate twice. Close-underflow is checked after writes, and successful updates increment the epoch before requesting flooding. Full flood/lifecycle/query composition and runtime safety remain open. [REF-003](research/BSP_REFERENCES.md).
|
| 351 |
+
|
| 352 |
+
**F-106 — Observed flood compositions:** positive portal counters generate component labels with ascending root labels and current epoch stamps across sampled symmetric graphs, including recursive 32-area cases. Mutable duplicate-open/close sequences rebuild expected labels. ABI, arbitrary graphs and original-runtime behavior remain open. [FLOOD-001](research/AREA_FLOODING.md).
|
| 353 |
+
|
| 354 |
+
**F-107 — Observed revisit/epoch behavior:** matching stamps retain matching labels and request a reflood error on an entry-label mismatch. Native epoch addition wraps modulo 2^32; supplied matching stamps can skip relabeling after wrap. Legal runtime reachability/lifetime and every unrolled mismatch path remain open. [FLOOD-002](research/AREA_FLOODING.md).
|
| 355 |
+
|
| 356 |
+
**F-108 — Observed area-bit output:** ordinary matching-label bits OR into existing bytes; area -1 or nonzero cm_noAreas requests all-ones fill. Tested lengths round area count up to bytes, and canaries are preserved. Caller initialization/union/inversion, index/buffer validity and snapshot/runtime behavior remain open. [FLOOD-003](research/AREA_FLOODING.md).
|
docs/PROVISIONAL_TODO.md
CHANGED
|
@@ -518,3 +518,5 @@ Research progress: [BSP plane boundaries and bounded node traversal](research/BS
|
|
| 518 |
Research progress: [native BSP payload loading](research/BSP_LOADING.md) completes bounded RE-321–323. Complete asset conversion and geometry milestones remain open; RE-324 tracks actual variant audits, validation, reference ownership and runtime fixtures.
|
| 519 |
|
| 520 |
Research progress: [leaf references and area portal state](research/BSP_REFERENCES.md) completes bounded RE-325–327. Broad geometry/networking/runtime milestones remain open; RE-328 tracks complete flooding, reference ownership and snapshot consumers.
|
|
|
|
|
|
|
|
|
| 518 |
Research progress: [native BSP payload loading](research/BSP_LOADING.md) completes bounded RE-321–323. Complete asset conversion and geometry milestones remain open; RE-324 tracks actual variant audits, validation, reference ownership and runtime fixtures.
|
| 519 |
|
| 520 |
Research progress: [leaf references and area portal state](research/BSP_REFERENCES.md) completes bounded RE-325–327. Broad geometry/networking/runtime milestones remain open; RE-328 tracks complete flooding, reference ownership and snapshot consumers.
|
| 521 |
+
|
| 522 |
+
Research progress: [area flooding and bit output](research/AREA_FLOODING.md) completes bounded RE-329–331. Broad runtime/networking milestones remain open; RE-332 tracks real-map labels, lifecycle and snapshot consumers.
|
docs/RESEARCH_LEDGER.md
CHANGED
|
@@ -189,3 +189,7 @@ Completed bounded RE-321–323 with `analyze_bsp_loading.py`: eight verified gra
|
|
| 189 |
## 2026-10-11 — Leaf reference arrays and area portal state
|
| 190 |
|
| 191 |
Completed bounded RE-325–327 with `analyze_bsp_references.py`: sixteen verified native graphs, 48 reference-copy and 48 consumer-address slices, 450 connectivity and 800 portal probes. REF-001–003/F-103–105 distinguish standalone copying from inline map loading, native signed address calculations from valid indices, supplied label equality from flood generation, and directed reference counters from Boolean portal state. Portal frame omission and all stopped callee boundaries are explicit. Eight independent tests verify copies/allocation/canaries, signed addressing, connectivity guard priority, full sampled matrix/write/error/epoch/request outcomes, self-pairs, prior-loader slots, paired outputs and low-byte aliases. The full suite passes 262 tests; new and preceding reports regenerate byte-identically, storage and documentation checks pass. RE-324 remains open; RE-328 tracks inline/range/layout/geometry/flood/lifecycle/snapshot and runtime/platform coverage. No original process, allocator or native callee executes.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 189 |
## 2026-10-11 — Leaf reference arrays and area portal state
|
| 190 |
|
| 191 |
Completed bounded RE-325–327 with `analyze_bsp_references.py`: sixteen verified native graphs, 48 reference-copy and 48 consumer-address slices, 450 connectivity and 800 portal probes. REF-001–003/F-103–105 distinguish standalone copying from inline map loading, native signed address calculations from valid indices, supplied label equality from flood generation, and directed reference counters from Boolean portal state. Portal frame omission and all stopped callee boundaries are explicit. Eight independent tests verify copies/allocation/canaries, signed addressing, connectivity guard priority, full sampled matrix/write/error/epoch/request outcomes, self-pairs, prior-loader slots, paired outputs and low-byte aliases. The full suite passes 262 tests; new and preceding reports regenerate byte-identically, storage and documentation checks pass. RE-324 remains open; RE-328 tracks inline/range/layout/geometry/flood/lifecycle/snapshot and runtime/platform coverage. No original process, allocator or native callee executes.
|
| 192 |
+
|
| 193 |
+
## 2026-10-11 — Area flood composition and visibility bits
|
| 194 |
+
|
| 195 |
+
Completed bounded RE-329–331 with `analyze_area_flooding.py`: eight verified graphs, 108 flood compositions, eighteen mutable portal-update steps, 48 entry revisit/24 epoch probes and 168 area-bit outputs. FLOOD-001–003/F-106–108 distinguish evaluated synthetic recursion from original ABI/callee execution, generated sampled labels from all-graph conformance, epoch arithmetic from legal lifecycle reachability and byte OR from buffer initialization. PUSH omission, caller-register restoration and supplied memset effects are explicit. Eight independent tests verify component/sequence/revisit/epoch/bit/canary/paired/slot oracles and restricted signed-branch/shift/byte operations. The full suite passes 270 tests; new and preceding reports regenerate byte-identically, storage and documentation checks pass. RE-328 remains open; RE-332 tracks complete error/lifecycle/asymmetric/portal-writer/area-bit/snapshot/real-map and runtime/platform coverage. No original process or native callee executes.
|
docs/REVERSE_ENGINEERING_TODO.md
CHANGED
|
@@ -392,3 +392,8 @@ Purpose: turn the supplied installation into an evidence-backed specification of
|
|
| 392 |
- [x] RE-326 Recover area connectivity bypass/index-guard priority and eight-byte record label comparisons ([REF-002](research/BSP_REFERENCES.md)).
|
| 393 |
- [x] RE-327 Recover paired portal counters, self-pair writes, close-underflow/error boundaries and epoch/first-flood requests ([REF-003](research/BSP_REFERENCES.md)).
|
| 394 |
- [ ] RE-328 Recover inline reference-loader equivalence and actual map index ranges, complete brush/surface layouts/stamps/geometry, all unrolled/recursive flooding and epoch/revisit invariants, portal writers/reset/serialization, area-bit/snapshot consumers and original-runtime/all-platform conformance.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 392 |
- [x] RE-326 Recover area connectivity bypass/index-guard priority and eight-byte record label comparisons ([REF-002](research/BSP_REFERENCES.md)).
|
| 393 |
- [x] RE-327 Recover paired portal counters, self-pair writes, close-underflow/error boundaries and epoch/first-flood requests ([REF-003](research/BSP_REFERENCES.md)).
|
| 394 |
- [ ] RE-328 Recover inline reference-loader equivalence and actual map index ranges, complete brush/surface layouts/stamps/geometry, all unrolled/recursive flooding and epoch/revisit invariants, portal writers/reset/serialization, area-bit/snapshot consumers and original-runtime/all-platform conformance.
|
| 395 |
+
|
| 396 |
+
- [x] RE-329 Compose bounded unrolled/recursive area flooding and mutable portal-to-label sequences against an independent component oracle ([FLOOD-001](research/AREA_FLOODING.md)).
|
| 397 |
+
- [x] RE-330 Recover entry revisit-label consistency and isolated modular epoch/stamp aliasing probes ([FLOOD-002](research/AREA_FLOODING.md)).
|
| 398 |
+
- [x] RE-331 Recover bounded area-bit packing, OR retention, bypass memset request/effects and returned byte lengths ([FLOOD-003](research/AREA_FLOODING.md)).
|
| 399 |
+
- [ ] RE-332 Recover asymmetric/malformed/all-unrolled flood/error behavior, reset/stamp/epoch/portal writer/serialization invariants, area-bit buffer initialization/union/inversion and snapshot consumers; compose connectivity/PVS with real-map labels and validate original-runtime/all-platform conformance.
|
docs/research/AREA_FLOODING.md
ADDED
|
@@ -0,0 +1,45 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
# Area flooding, epoch guards and area-bit output
|
| 2 |
+
|
| 3 |
+
Reproduce: `python3 scripts/analyze_area_flooding.py`. Validate: `python3 scripts/test_area_flooding.py`. Evidence: [area-flooding.json](area-flooding.json), with hash-verified graphs for four functions in both Linux ELF64 engines. This extends [portal counter findings](BSP_REFERENCES.md).
|
| 4 |
+
|
| 5 |
+
These are bounded synthetic instruction compositions, not original executable/callee execution. PUSH traffic is explicitly replaced with NOPs; supplied stack windows hold local words. Recursive boundaries evaluate a separate synthetic graph, carry its memory changes back and restore the supplied caller registers before continuing. They do not validate real ABI clobbers, stack frames or exception propagation. Execution stops before epilogues and error calls. Memset effects in the area-bit branch are supplied separately. Counts, matrices, labels/stamps and buffers are fixtures, not loaded maps.
|
| 6 |
+
|
| 7 |
+
## FLOOD-001 — Component generation and portal-to-label composition (RE-329)
|
| 8 |
+
|
| 9 |
+
CM_FloodAreaConnections increments the flood epoch, scans area indices in ascending order, and starts successive labels at one. Each unvisited area starts a new label. The flood graph follows matrix entries whose signed value is **greater than zero**; zero and tested negative entries do not connect areas. Native area records contain label +0 and epoch stamp +4, at stride eight.
|
| 10 |
+
|
| 11 |
+
The collector composes all instructions reached by 108 paired fixtures: area counts 0/1/2/3/4/8/12/16/32 and six symmetric matrix families (empty, chain, clique, star, groups of three, and negative off-diagonal weights). Positive edges use counter two. Outputs agree with an independent breadth-first component oracle, despite the native graph's unrolled depth-first/recursive walk. Initial epoch 40 becomes 41 and every sampled real area receives stamp 41. A zero-area composition still increments the epoch.
|
| 12 |
+
|
| 13 |
+
The 32-area chain/clique fixtures reach recursive call boundaries, with maximum synthetic nesting depth four. The collector bounds nesting at sixteen and each aggregate composition at 200,000 evaluated instructions. Larger traces retain instruction counts/hashes, requested recursive arguments/sites and maximum depth; small fixtures retain addresses. This samples complete output compositions for these families, not every possible branch or malformed graph.
|
| 14 |
+
|
| 15 |
+
Eighteen paired portal-update steps then connect CM_AdjustAreaPortalState to actual synthetic flood instructions. A four-area fixture starts disconnected, opens the same pair twice, closes it once, opens a chain through other areas, closes edges and opens/closes a self-pair. Each update carries matrix and area memory into the next step. The independent oracle checks every matrix, label, stamp and epoch. The duplicate open survives one close; the second close splits the first area away. The self-pair moves its diagonal counter 0→2→0. These valid sampled transitions establish bounded update-to-label behavior; error handling and original runtime remain open.
|
| 16 |
+
|
| 17 |
+
## FLOOD-002 — Revisit consistency and epoch aliasing (RE-330)
|
| 18 |
+
|
| 19 |
+
Forty-eight paired entry probes exercise CM_FloodArea_r with supplied current epoch, previous stamp, previous label and requested label:
|
| 20 |
+
|
| 21 |
+
| Entry state | Observed behavior |
|
| 22 |
+
| --- | --- |
|
| 23 |
+
| Stamp differs from current epoch | Write requested label/current stamp, then walk |
|
| 24 |
+
| Stamp matches and label matches | Return without relabeling |
|
| 25 |
+
| Stamp matches and label differs | Stop at Com_Error request, `FloodArea_r: reflooded` |
|
| 26 |
+
|
| 27 |
+
The error text appears at the retained unrolled consistency-check sites as well, but only the entry mismatch branch is isolated with error fixtures. Complete mismatch coverage across all unrolled/reentrant paths remains open.
|
| 28 |
+
|
| 29 |
+
Twenty-four paired outer-epoch probes cover raw epochs 0/40/0xfffffffe/0xffffffff and stamps 0/1/0xffffffff. The native ADD increments modulo 2^32. When a supplied stamp already equals the incremented epoch, the existing label 77 is retained. In particular, 0xffffffff→0 with stamp zero skips relabeling. This characterizes native word arithmetic and a local aliasing condition; it does not establish that such stale/wrapped states occur in a legal game session, or prescribe target recovery behavior.
|
| 30 |
+
|
| 31 |
+
## FLOOD-003 — Area-bit packing and existing buffer state (RE-331)
|
| 32 |
+
|
| 33 |
+
One hundred sixty-eight paired output probes cover area counts 0/1/7/8/9/16/17, area -1/0, cm_noAreas words 0/1/7 and buffers seeded with 0/0xa0. The returned byte length is `(count + 7) >> 3` for these nonnegative counts.
|
| 34 |
+
|
| 35 |
+
For ordinary area zero, supplied labels `i % 3 + 1` select matching-label areas. Bit `i % 8` goes into byte `i / 8`. The native instruction is byte OR: existing buffer bits are retained, including bits for nonmatching areas. This function does not clear the buffer on the ordinary path. Initialization/union behavior must therefore be recovered from callers before implementing snapshot output.
|
| 36 |
+
|
| 37 |
+
Area -1 or nonzero cm_noAreas requests memset(buffer, 255, returned length). The collector stops there and supplies the requested byte writes before resuming the return-length instructions. This sets unused tail bits too; the regular path only ORs qualifying area bits. Canaries before and after the output remain unchanged in every sampled fixture.
|
| 38 |
+
|
| 39 |
+
The ordinary path reads the requested area's label before its area-count loop guard. The count-zero/area-zero fixture explicitly provides that record; it is not proof that an empty real map can safely call the function. This function's local graph does not validate the requested area's index. Negative values other than -1, count overflow, undersized buffers and complete caller bounds remain open.
|
| 40 |
+
|
| 41 |
+
## Validation and follow-up
|
| 42 |
+
|
| 43 |
+
Eight independent tests cover component labels/stamps and recursion use, mutable portal sequences, revisit errors, modular epoch/stamp aliasing, bit packing/OR/canaries/supplied memset, paired outcomes and prior-state slots. Restricted evaluator additions cover signed greater-than, 32-bit shifts, count masking/zero-count flag preservation and byte OR/alias preservation. Unknown flags and unsupported operations remain errors.
|
| 44 |
+
|
| 45 |
+
RE-332: cover asymmetric/malformed matrices, all unrolled consistency errors and allocator/reset/stamp/epoch lifetime; recover portal writers and error/serialization semantics; connect area-bit buffer initialization/union/inversion and snapshot consumers; compose connectivity/PVS with generated labels and real BSP variants; obtain original-runtime and all-platform differential fixtures. Complete collision geometry and Rust/Bevy/Solari rendering remain open.
|
docs/research/BSP_REFERENCES.md
CHANGED
|
@@ -52,3 +52,5 @@ The retained CM_FloodArea_r graph uses record +0 for the label and +4 for the ep
|
|
| 52 |
Eight independent tests cover copy/allocation/canaries, signed consumer addressing, connectivity guard priority, complete sampled matrix mutations, self-pairs/nonzero open flags, prior-loader slot correspondence, paired outputs/trace lengths and low-byte register preservation. Small slices retain instruction addresses; larger collections retain trace lengths and hashes. The report does not copy any original asset into assets/.
|
| 53 |
|
| 54 |
RE-328: prove inline/reference-loading equivalence and valid reference ranges across all BSP variants; recover complete brush/surface layouts, stamps and geometry; compose full flood generation/revisit/epoch behavior and update-to-connectivity/area-bit/snapshot consumers; connect server/QVM portal writers and lifetime/reset/serialization; obtain original-runtime and other-platform fixtures. Rust/Bevy/Solari collision and rendering implementation remain open.
|
|
|
|
|
|
|
|
|
| 52 |
Eight independent tests cover copy/allocation/canaries, signed consumer addressing, connectivity guard priority, complete sampled matrix mutations, self-pairs/nonzero open flags, prior-loader slot correspondence, paired outputs/trace lengths and low-byte register preservation. Small slices retain instruction addresses; larger collections retain trace lengths and hashes. The report does not copy any original asset into assets/.
|
| 53 |
|
| 54 |
RE-328: prove inline/reference-loading equivalence and valid reference ranges across all BSP variants; recover complete brush/surface layouts, stamps and geometry; compose full flood generation/revisit/epoch behavior and update-to-connectivity/area-bit/snapshot consumers; connect server/QVM portal writers and lifetime/reset/serialization; obtain original-runtime and other-platform fixtures. Rust/Bevy/Solari collision and rendering implementation remain open.
|
| 55 |
+
|
| 56 |
+
Follow-up: [area flooding and bit output](AREA_FLOODING.md) adds bounded generated-label/portal-update compositions and visibility packing. Complete flood/error/lifecycle/real-map/snapshot conformance remains open under RE-328/RE-332.
|
docs/research/README.md
CHANGED
|
@@ -119,3 +119,5 @@ The extension collector adds five focused tests for native tail calls, command-r
|
|
| 119 |
[Native BSP plane, node and leaf loading](BSP_LOADING.md) adds RE-321–323: descriptor routing, bounded payload conversion, derived plane fields, native node pointers, leaf projection/maxima and allocation requests. Reproduce with `python3 scripts/analyze_bsp_loading.py`; check with `python3 scripts/test_bsp_loading.py`. Complete validation/loading/ownership/recursive-query/runtime/platform contracts remain open.
|
| 120 |
|
| 121 |
[Leaf references, connectivity and portal counters](BSP_REFERENCES.md) adds RE-325–327: bounded reference copying/consumer addressing, connectivity guard priority and portal mutation/epoch/flood-request boundaries. Reproduce with `python3 scripts/analyze_bsp_references.py`; check with `python3 scripts/test_bsp_references.py`. Full inline loading/flooding/lifecycle/geometry/runtime/platform contracts remain open.
|
|
|
|
|
|
|
|
|
| 119 |
[Native BSP plane, node and leaf loading](BSP_LOADING.md) adds RE-321–323: descriptor routing, bounded payload conversion, derived plane fields, native node pointers, leaf projection/maxima and allocation requests. Reproduce with `python3 scripts/analyze_bsp_loading.py`; check with `python3 scripts/test_bsp_loading.py`. Complete validation/loading/ownership/recursive-query/runtime/platform contracts remain open.
|
| 120 |
|
| 121 |
[Leaf references, connectivity and portal counters](BSP_REFERENCES.md) adds RE-325–327: bounded reference copying/consumer addressing, connectivity guard priority and portal mutation/epoch/flood-request boundaries. Reproduce with `python3 scripts/analyze_bsp_references.py`; check with `python3 scripts/test_bsp_references.py`. Full inline loading/flooding/lifecycle/geometry/runtime/platform contracts remain open.
|
| 122 |
+
|
| 123 |
+
[Area flooding, epoch guards and area-bit output](AREA_FLOODING.md) adds RE-329–331: bounded unrolled/recursive flood and portal-to-label compositions, entry revisit/epoch guards and byte OR/fill packing. Reproduce with `python3 scripts/analyze_area_flooding.py`; check with `python3 scripts/test_area_flooding.py`. Complete lifecycle/error/asymmetric/real-map/snapshot/runtime/platform contracts remain open.
|
docs/research/area-flooding.json
ADDED
|
The diff for this file is too large to render.
See raw diff
|
|
|
scripts/analyze_area_flooding.py
ADDED
|
@@ -0,0 +1,114 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
#!/usr/bin/env python3
|
| 2 |
+
"""Compose bounded native flood instructions and area-bit output slices."""
|
| 3 |
+
import gzip
|
| 4 |
+
import itertools
|
| 5 |
+
import json
|
| 6 |
+
from pathlib import Path
|
| 7 |
+
from analyze_area_queries import site
|
| 8 |
+
from analyze_bsp_references import errors,global_address,operand,trace_fields
|
| 9 |
+
from analyze_collision_composition import evaluate,get_word,put_word
|
| 10 |
+
from analyze_engine_control import control_flow
|
| 11 |
+
from analyze_native import elf
|
| 12 |
+
from analyze_qvm import write_json
|
| 13 |
+
from analyze_vm_extensions import native_functions,verified
|
| 14 |
+
|
| 15 |
+
|
| 16 |
+
def matrix_for(count,pattern):
|
| 17 |
+
m=[[0]*count for _ in range(count)]
|
| 18 |
+
for a in range(count):
|
| 19 |
+
for b in range(count):
|
| 20 |
+
connected=(a!=b and (pattern=='clique' or pattern=='chain' and abs(a-b)==1 or pattern=='star' and min(a,b)==0 or pattern=='split' and a//3==b//3))
|
| 21 |
+
m[a][b]=2 if connected else -1 if pattern=='negative' and a!=b else 0
|
| 22 |
+
return m
|
| 23 |
+
|
| 24 |
+
|
| 25 |
+
def model(g):
|
| 26 |
+
result=dict(g);result['instructions']=[dict(x) for x in g['instructions']];omitted=[]
|
| 27 |
+
for x in result['instructions']:
|
| 28 |
+
if x['opcode']=='pushq':omitted.append(x['address']);x['opcode']='nop';x['operands']=''
|
| 29 |
+
return result,omitted
|
| 30 |
+
|
| 31 |
+
|
| 32 |
+
def run(g,start,stops,m,regs):return evaluate(g,start,stops,m,regs,limit=50000,capture_registers=True)
|
| 33 |
+
|
| 34 |
+
|
| 35 |
+
def main():
|
| 36 |
+
out={'native':{},'limitations':'Bounded synthetic composition of native instruction graphs, not '
|
| 37 |
+
'original process/callee execution. PUSH traffic is omitted, stack addresses are supplied, '
|
| 38 |
+
'recursive boundaries evaluate a separate synthetic graph and restore the supplied caller '
|
| 39 |
+
'register state; ABI/clobber/frame semantics are not validated. Memset effects are supplied. '
|
| 40 |
+
'Real maps, reset/ownership, malformed/asymmetric states, epoch wrap reachability, snapshots '
|
| 41 |
+
'and original-runtime/all-platform conformance remain open.'}
|
| 42 |
+
areas,matrix,cvar,buffer=0x10000,0x20000,0x30000,0x40000
|
| 43 |
+
for label in ['linux--Quake3-UrT-Ded.x86_64','linux--Quake3-UrT.x86_64']:
|
| 44 |
+
r=json.loads(Path(f'docs/research/native/{label}.json').read_text());data=verified((Path('.cache/UrbanTerror43')/r['source']['path']).read_bytes(),r['source']['sha256'])
|
| 45 |
+
a=r['artifacts']['disassembly.txt'];fs=native_functions(verified(gzip.open(a['path'],'rb').read(),a['uncompressed_sha256']).decode());metadata,_=elf(data)
|
| 46 |
+
graphs={n:control_flow(fs[n]) for n in ['CM_FloodAreaConnections','CM_FloodArea_r','CM_WriteAreaBits','CM_AdjustAreaPortalState']};outer=graphs['CM_FloodAreaConnections'];child=graphs['CM_FloodArea_r'];bits=graphs['CM_WriteAreaBits']
|
| 47 |
+
count_slot=global_address(next(x for x in outer['instructions'] if x['opcode']=='movl' and '(%rip)' in x['operands']))
|
| 48 |
+
epoch_slot=global_address(next(x for x in outer['instructions'] if x['opcode']=='addl' and '(%rip)' in x['operands']))
|
| 49 |
+
area_slot=global_address(next(x for x in outer['instructions'] if x['opcode']=='addq' and '(%rip)' in x['operands'] and operand(x).endswith(', %rdx')))
|
| 50 |
+
matrix_slot=global_address(next(x for x in outer['instructions'] if x['opcode']=='addq' and '(%rip)' in x['operands'] and operand(x).endswith(', %r12')))
|
| 51 |
+
models={};omitted={};ends={};calls={};error_list=errors(child,data,metadata['sections'])
|
| 52 |
+
for name,g in [('CM_FloodAreaConnections',outer),('CM_FloodArea_r',child),('CM_AdjustAreaPortalState',graphs['CM_AdjustAreaPortalState'])]:
|
| 53 |
+
models[name],omitted[name]=model(g);rows=g['instructions'];ends[name]=next(x['address'] for x in rows if x['opcode']=='popq') if name=='CM_AdjustAreaPortalState' else next(x['address'] for x in rows if x['opcode']=='addq' and operand(x).endswith(', %rsp'))
|
| 54 |
+
calls[name]={x['address']:rows[i+1]['address'] for i,x in enumerate(rows) if '<CM_FloodArea_r>' in x['operands']}
|
| 55 |
+
def seed(count,values,epoch=40):
|
| 56 |
+
m={};put_word(m,count_slot,count);put_word(m,epoch_slot,epoch);put_word(m,area_slot,areas,8);put_word(m,matrix_slot,matrix,8)
|
| 57 |
+
for i in range(max(1,count)):put_word(m,areas+8*i,0);put_word(m,areas+8*i+4,0)
|
| 58 |
+
for i,row in enumerate(values):
|
| 59 |
+
for j,v in enumerate(row):put_word(m,matrix+4*(i*count+j),v)
|
| 60 |
+
return m
|
| 61 |
+
def compose(name,m,regs,depth=0):
|
| 62 |
+
if depth>16:raise ValueError('synthetic recursion bound')
|
| 63 |
+
g=models[name];pc=g['entry'];trace=[];requests=[];maximum=depth
|
| 64 |
+
while pc!=ends[name]:
|
| 65 |
+
t=run(g,pc,[ends[name]]+list(calls[name])+[e['call'] for e in error_list],m,regs);m=t['memory'];regs=t['registers'];trace+=t['trace'];pc=t['stop']
|
| 66 |
+
if pc in [e['call'] for e in error_list]:raise ValueError('unexpected flood consistency error')
|
| 67 |
+
if pc in calls[name]:
|
| 68 |
+
area,component=regs['rdi']&0xffffffff,regs['rsi']&0xffffffff;requests.append([name,area,component,pc])
|
| 69 |
+
nested=compose('CM_FloodArea_r',m,{'%rdi':area,'%rsi':component,'%rsp':0x100000-(depth+1)*0x1000},depth+1)
|
| 70 |
+
m=nested['memory'];trace+=nested['trace'];requests+=nested['requests'];maximum=max(maximum,nested['maximum_depth']);pc=calls[name][pc]
|
| 71 |
+
if len(trace)>200000:raise ValueError('synthetic aggregate instruction bound')
|
| 72 |
+
return {'memory':m,'trace':trace,'requests':requests,'maximum_depth':maximum}
|
| 73 |
+
compositions=[]
|
| 74 |
+
for count,pattern in itertools.product([0,1,2,3,4,8,12,16,32],['empty','chain','clique','star','split','negative']):
|
| 75 |
+
values=matrix_for(count,pattern);t=compose('CM_FloodAreaConnections',seed(count,values),{'%rsp':0x100000})
|
| 76 |
+
compositions.append({'count':count,'pattern':pattern,'labels':[get_word(t['memory'],areas+8*i) for i in range(count)],'stamps':[get_word(t['memory'],areas+8*i+4) for i in range(count)],'epoch':get_word(t['memory'],epoch_slot),'requests':t['requests'],'maximum_depth':t['maximum_depth'],**trace_fields(t,count<=2)})
|
| 77 |
+
portal_sequence=[]
|
| 78 |
+
t=compose('CM_FloodAreaConnections',seed(4,matrix_for(4,'empty')),{'%rsp':0x100000});m=t['memory']
|
| 79 |
+
for a1,a2,opened in [(0,1,1),(0,1,7),(0,1,0),(1,2,1),(2,3,-1),(0,1,0),(2,3,0),(0,0,1),(0,0,0)]:
|
| 80 |
+
t=compose('CM_AdjustAreaPortalState',m,{'%rdi':a1,'%rsi':a2,'%rdx':opened,'%rsp':0x100000});m=t['memory']
|
| 81 |
+
portal_sequence.append({'area1':a1,'area2':a2,'open_word':opened,'matrix_words':[get_word(m,matrix+4*i) for i in range(16)],'labels':[get_word(m,areas+8*i) for i in range(4)],'stamps':[get_word(m,areas+8*i+4) for i in range(4)],'epoch':get_word(m,epoch_slot),'requests':t['requests'],'maximum_depth':t['maximum_depth'],**trace_fields(t)})
|
| 82 |
+
# Entry revisit: same epoch/label returns; same epoch/different label requests error.
|
| 83 |
+
revisit=[]
|
| 84 |
+
for epoch,stamp,label_word,requested in itertools.product([40,0xffffffff],[40,0xffffffff,0],[1,2],[1,2]):
|
| 85 |
+
m=seed(1,[[0]],epoch);put_word(m,areas,label_word);put_word(m,areas+4,stamp)
|
| 86 |
+
t=run(models['CM_FloodArea_r'],models['CM_FloodArea_r']['entry'],[ends['CM_FloodArea_r']]+[e['call'] for e in error_list],m,{'%rdi':0,'%rsi':requested,'%rsp':0x100000})
|
| 87 |
+
revisit.append({'epoch':epoch,'stamp_before':stamp,'label_before':label_word,'requested_label':requested,'error':t['stop']!=ends['CM_FloodArea_r'],'label_after':get_word(t['memory'],areas),'stamp_after':get_word(t['memory'],areas+4),**trace_fields(t,True)})
|
| 88 |
+
wrapping=[]
|
| 89 |
+
for epoch in [0,40,0xfffffffe,0xffffffff]:
|
| 90 |
+
for stamp in [0,1,0xffffffff]:
|
| 91 |
+
m=seed(1,[[0]],epoch);put_word(m,areas,77);put_word(m,areas+4,stamp)
|
| 92 |
+
t=compose('CM_FloodAreaConnections',m,{'%rsp':0x100000})
|
| 93 |
+
wrapping.append({'epoch_before':epoch,'stamp_before':stamp,'epoch_after':get_word(t['memory'],epoch_slot),'label_after':get_word(t['memory'],areas),'stamp_after':get_word(t['memory'],areas+4),**trace_fields(t,True)})
|
| 94 |
+
# Output OR loop; all-bits branch stops at memset and receives explicit supplied writes.
|
| 95 |
+
rows=bits['instructions'];start=next(x['address'] for x in rows if x['opcode']=='movl' and '(%rip)' in x['operands']);end=site(bits,'addq','$0x8, %rsp');fill=next(i for i,x in enumerate(rows) if '<memset@plt>' in x['operands']);noareas_slot=global_address(next(x for x in rows if x['opcode']=='movq' and '(%rip)' in x['operands'] and operand(x).endswith(', %rax')))
|
| 96 |
+
outputs=[]
|
| 97 |
+
for count,area,disabled,initial in itertools.product([0,1,7,8,9,16,17],[-1,0],[0,1,7],[0,0xa0]):
|
| 98 |
+
m=seed(count,[[0]*count for _ in range(count)]);put_word(m,noareas_slot,cvar,8);put_word(m,cvar+48,disabled)
|
| 99 |
+
for i in range(max(1,count)):put_word(m,areas+8*i,i%3+1)
|
| 100 |
+
length=(count+7)//8
|
| 101 |
+
for i in range(length+2):m[buffer-1+i]=initial
|
| 102 |
+
t=run(bits,start,[rows[fill]['address'],end],m,{'%rdi':buffer,'%rsi':area});request=None;trace=t['trace']
|
| 103 |
+
if t['stop']!=end:
|
| 104 |
+
regs=t['registers'];request=[regs['rdi'],regs['rsi'],regs['rdx']]
|
| 105 |
+
if request!=[buffer,255,length]:raise ValueError('unexpected memset request')
|
| 106 |
+
for i in range(length):t['memory'][buffer+i]=255
|
| 107 |
+
t=run(bits,rows[fill+1]['address'],[end],t['memory'],regs);trace+=t['trace']
|
| 108 |
+
outputs.append({'count':count,'area':area,'disabled_word':disabled,'initial_byte':initial,'returned_length':t['registers']['rax'],'output_bytes':[t['memory'][buffer+i] for i in range(length)],'canaries':[t['memory'][buffer-1],t['memory'][buffer+length]],'supplied_memset_request':request,**trace_fields({'trace':trace},True)})
|
| 109 |
+
out['native'][label]={'source':r['source'],'disassembly_sha256':a['uncompressed_sha256'],'graphs':graphs,'omitted_pushes':omitted,'slots':{'count':count_slot,'area_base':area_slot,'matrix':matrix_slot,'epoch':epoch_slot,'noareas_cvar_pointer':noareas_slot},'consistency_errors':error_list,'compositions':compositions,'portal_sequence':portal_sequence,'revisit_probes':revisit,'epoch_probes':wrapping,'bit_output_probes':outputs}
|
| 110 |
+
write_json(Path('docs/research/area-flooding.json'),out)
|
| 111 |
+
print('Recovered 108 flood compositions, 18 portal-update steps, 48 revisit/24 epoch probes and 168 area-bit outputs')
|
| 112 |
+
|
| 113 |
+
|
| 114 |
+
if __name__=='__main__':main()
|
scripts/analyze_collision_composition.py
CHANGED
|
@@ -14,7 +14,7 @@ from analyze_vm_extensions import native_functions,verified
|
|
| 14 |
|
| 15 |
def register(r):
|
| 16 |
aliases={'eax':('rax',32),'edi':('rdi',32),'esi':('rsi',32),'edx':('rdx',32),
|
| 17 |
-
'ecx':('rcx',32),'ebp':('rbp',32),'ebx':('rbx',32),'al':('rax',8),'sil':('rsi',8),'dl':('rdx',8),'cl':('rcx',8),'dil':('rdi',8)}
|
| 18 |
r=r.lstrip('%')
|
| 19 |
if r in aliases:return aliases[r]
|
| 20 |
if re.fullmatch(r'r\d+d',r):return r[:-1],32
|
|
@@ -105,17 +105,23 @@ def evaluate(graph,start,stops,memory,registers,limit=128,capture_registers=Fals
|
|
| 105 |
elif len(parts)==3:a,b,dest=parts;v,w=read(a,width),read(b,width)
|
| 106 |
else:raise ValueError('unsupported multiply operands')
|
| 107 |
write(dest,v*w,width);equal=None;signed_le=signed_lt=negative=None;ge=greater=below=None
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 108 |
elif op=='shlq':
|
| 109 |
a,b=args.split(', ');write(b,read(b,8)<<(read(a,8)&63),8)
|
| 110 |
equal=None;signed_le=signed_lt=negative=None;ge=greater=below=None
|
| 111 |
elif op=='sarq':
|
| 112 |
a,b=args.split(', ');v=read(b,8);v=v if v<2**63 else v-2**64
|
| 113 |
write(b,v>>(read(a,8)&63),8);equal=None;signed_le=signed_lt=negative=None;ge=greater=below=None
|
| 114 |
-
elif op in ['xorl','orl','andl','subl','addl','addq','subq']:
|
| 115 |
-
width=8 if op in ['addq','subq'] else 4
|
| 116 |
a,b=args.split(', ')
|
| 117 |
v,w=(0,0) if op=='xorl' and a==b else (read(a,width),read(b,width))
|
| 118 |
-
result=v^w if op=='xorl' else v|w if op
|
| 119 |
write(b,result,width);equal=(result&((1<<(width*8))-1))==0
|
| 120 |
signed_le=signed_lt=negative=None;ge=greater=below=None
|
| 121 |
elif op=='xorps':
|
|
@@ -138,11 +144,11 @@ def evaluate(graph,start,stops,memory,registers,limit=128,capture_registers=Fals
|
|
| 138 |
if op in ['sete','setne'] and equal is None:raise ValueError('unmodeled zero flag')
|
| 139 |
if op in ['setb','setbe','setae'] and below is None:raise ValueError('unmodeled unsigned flags')
|
| 140 |
write(args,int(equal if op=='sete' else not equal if op=='setne' else below if op=='setb' else ge if op=='setae' else below or equal),1)
|
| 141 |
-
elif op in ['je','jne','jae','ja','jb','jbe','jle','jl','jge','js','jns','jmp']:
|
| 142 |
if op in ['je','jne'] and equal is None:raise ValueError('unmodeled zero flag')
|
| 143 |
-
if op in ['jle','jl','jge','js','jns'] and signed_le is None:raise ValueError('unmodeled signed flags')
|
| 144 |
if op in ['jae','ja','jb','jbe'] and ge is None:raise ValueError('unmodeled unsigned flags')
|
| 145 |
-
taken=op=='jmp' or (equal if op=='je' else not equal if op=='jne' else signed_le if op=='jle' else signed_lt if op=='jl' else not signed_lt if op=='jge' else negative if op=='js' else not negative if op=='jns' else greater if op=='ja' else below if op=='jb' else below or equal if op=='jbe' else ge)
|
| 146 |
if taken:pc=int(args.split()[0],16)
|
| 147 |
else:raise ValueError('unsupported composition opcode '+op)
|
| 148 |
result={'trace':trace,'stop':pc,'memory':m,'writes':writes}
|
|
|
|
| 14 |
|
| 15 |
def register(r):
|
| 16 |
aliases={'eax':('rax',32),'edi':('rdi',32),'esi':('rsi',32),'edx':('rdx',32),
|
| 17 |
+
'ecx':('rcx',32),'ebp':('rbp',32),'ebx':('rbx',32),'al':('rax',8),'sil':('rsi',8),'dl':('rdx',8),'cl':('rcx',8),'dil':('rdi',8),'bpl':('rbp',8)}
|
| 18 |
r=r.lstrip('%')
|
| 19 |
if r in aliases:return aliases[r]
|
| 20 |
if re.fullmatch(r'r\d+d',r):return r[:-1],32
|
|
|
|
| 105 |
elif len(parts)==3:a,b,dest=parts;v,w=read(a,width),read(b,width)
|
| 106 |
else:raise ValueError('unsupported multiply operands')
|
| 107 |
write(dest,v*w,width);equal=None;signed_le=signed_lt=negative=None;ge=greater=below=None
|
| 108 |
+
elif op in ['sarl','shll']:
|
| 109 |
+
a,b=args.split(', ');amount=read(a,4)&31;v=read(b,4)
|
| 110 |
+
if amount:
|
| 111 |
+
signed_v=v if v<2**31 else v-2**32
|
| 112 |
+
write(b,signed_v>>amount if op=='sarl' else v<<amount,4)
|
| 113 |
+
equal=None;signed_le=signed_lt=negative=None;ge=greater=below=None
|
| 114 |
elif op=='shlq':
|
| 115 |
a,b=args.split(', ');write(b,read(b,8)<<(read(a,8)&63),8)
|
| 116 |
equal=None;signed_le=signed_lt=negative=None;ge=greater=below=None
|
| 117 |
elif op=='sarq':
|
| 118 |
a,b=args.split(', ');v=read(b,8);v=v if v<2**63 else v-2**64
|
| 119 |
write(b,v>>(read(a,8)&63),8);equal=None;signed_le=signed_lt=negative=None;ge=greater=below=None
|
| 120 |
+
elif op in ['xorl','orl','orb','andl','subl','addl','addq','subq']:
|
| 121 |
+
width=8 if op in ['addq','subq'] else 1 if op=='orb' else 4
|
| 122 |
a,b=args.split(', ')
|
| 123 |
v,w=(0,0) if op=='xorl' and a==b else (read(a,width),read(b,width))
|
| 124 |
+
result=v^w if op=='xorl' else v|w if op in ['orl','orb'] else v&w if op=='andl' else w-v if op in ['subl','subq'] else v+w
|
| 125 |
write(b,result,width);equal=(result&((1<<(width*8))-1))==0
|
| 126 |
signed_le=signed_lt=negative=None;ge=greater=below=None
|
| 127 |
elif op=='xorps':
|
|
|
|
| 144 |
if op in ['sete','setne'] and equal is None:raise ValueError('unmodeled zero flag')
|
| 145 |
if op in ['setb','setbe','setae'] and below is None:raise ValueError('unmodeled unsigned flags')
|
| 146 |
write(args,int(equal if op=='sete' else not equal if op=='setne' else below if op=='setb' else ge if op=='setae' else below or equal),1)
|
| 147 |
+
elif op in ['je','jne','jae','ja','jb','jbe','jle','jl','jge','jg','js','jns','jmp']:
|
| 148 |
if op in ['je','jne'] and equal is None:raise ValueError('unmodeled zero flag')
|
| 149 |
+
if op in ['jle','jl','jge','jg','js','jns'] and signed_le is None:raise ValueError('unmodeled signed flags')
|
| 150 |
if op in ['jae','ja','jb','jbe'] and ge is None:raise ValueError('unmodeled unsigned flags')
|
| 151 |
+
taken=op=='jmp' or (equal if op=='je' else not equal if op=='jne' else signed_le if op=='jle' else signed_lt if op=='jl' else not signed_lt if op=='jge' else not signed_le if op=='jg' else negative if op=='js' else not negative if op=='jns' else greater if op=='ja' else below if op=='jb' else below or equal if op=='jbe' else ge)
|
| 152 |
if taken:pc=int(args.split()[0],16)
|
| 153 |
else:raise ValueError('unsupported composition opcode '+op)
|
| 154 |
result={'trace':trace,'stop':pc,'memory':m,'writes':writes}
|
scripts/test_area_flooding.py
ADDED
|
@@ -0,0 +1,104 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
#!/usr/bin/env python3
|
| 2 |
+
"""Independent components, portal transitions, revisit and bit-packing oracles."""
|
| 3 |
+
import json
|
| 4 |
+
from pathlib import Path
|
| 5 |
+
import unittest
|
| 6 |
+
from analyze_area_flooding import matrix_for
|
| 7 |
+
from analyze_collision_composition import evaluate
|
| 8 |
+
from test_bsp_planes import graph
|
| 9 |
+
|
| 10 |
+
|
| 11 |
+
def components(matrix):
|
| 12 |
+
# Breadth-first independent oracle; native traversal uses unrolled depth-first walks.
|
| 13 |
+
labels=[0]*len(matrix);label=0
|
| 14 |
+
for root in range(len(matrix)):
|
| 15 |
+
if labels[root]:continue
|
| 16 |
+
label+=1;labels[root]=label;queue=[root]
|
| 17 |
+
while queue:
|
| 18 |
+
a=queue.pop(0)
|
| 19 |
+
for b,weight in enumerate(matrix[a]):
|
| 20 |
+
if weight>0 and not labels[b]:labels[b]=label;queue.append(b)
|
| 21 |
+
return labels
|
| 22 |
+
|
| 23 |
+
|
| 24 |
+
class AreaFloodingTests(unittest.TestCase):
|
| 25 |
+
@classmethod
|
| 26 |
+
def setUpClass(cls):cls.r=json.loads(Path('docs/research/area-flooding.json').read_text())
|
| 27 |
+
|
| 28 |
+
def test_flood_components_positive_edges_stamps_and_recursive_coverage(self):
|
| 29 |
+
for n in self.r['native'].values():
|
| 30 |
+
self.assertEqual(len(n['compositions']),54)
|
| 31 |
+
for p in n['compositions']:
|
| 32 |
+
self.assertEqual(p['labels'],components(matrix_for(p['count'],p['pattern'])))
|
| 33 |
+
self.assertEqual(p['stamps'],[41]*p['count']);self.assertEqual(p['epoch'],41)
|
| 34 |
+
chain=next(p for p in n['compositions'] if p['count']==32 and p['pattern']=='chain')
|
| 35 |
+
self.assertGreater(chain['maximum_depth'],1)
|
| 36 |
+
self.assertTrue(any(c[0]=='CM_FloodArea_r' for c in chain['requests']))
|
| 37 |
+
|
| 38 |
+
def test_portal_sequence_reference_counts_and_full_label_rebuild(self):
|
| 39 |
+
for n in self.r['native'].values():
|
| 40 |
+
m=[[0]*4 for _ in range(4)]
|
| 41 |
+
self.assertEqual(len(n['portal_sequence']),9)
|
| 42 |
+
for i,p in enumerate(n['portal_sequence']):
|
| 43 |
+
a,b=p['area1'],p['area2'];delta=1 if p['open_word'] else -1;m[a][b]+=delta;m[b][a]+=delta
|
| 44 |
+
self.assertEqual(p['matrix_words'],[v for row in m for v in row])
|
| 45 |
+
self.assertEqual(p['labels'],components(m));self.assertEqual(p['epoch'],42+i);self.assertEqual(p['stamps'],[42+i]*4)
|
| 46 |
+
rows=n['portal_sequence']
|
| 47 |
+
self.assertEqual(rows[2]['matrix_words'][1],1) # Duplicate open survives one close.
|
| 48 |
+
self.assertEqual(rows[5]['labels'][0],1);self.assertEqual(rows[5]['labels'][1],2)
|
| 49 |
+
self.assertEqual(rows[7]['matrix_words'][0],2);self.assertEqual(rows[8]['matrix_words'][0],0)
|
| 50 |
+
|
| 51 |
+
def test_revisit_same_epoch_checks_label_other_epochs_overwrite(self):
|
| 52 |
+
for n in self.r['native'].values():
|
| 53 |
+
self.assertEqual(len(n['revisit_probes']),24)
|
| 54 |
+
for p in n['revisit_probes']:
|
| 55 |
+
visited=p['epoch']==p['stamp_before']
|
| 56 |
+
self.assertEqual(p['error'],visited and p['label_before']!=p['requested_label'])
|
| 57 |
+
self.assertEqual(p['label_after'],p['label_before'] if visited else p['requested_label'])
|
| 58 |
+
self.assertEqual(p['stamp_after'],p['stamp_before'] if visited else p['epoch'])
|
| 59 |
+
self.assertEqual({e['text'] for e in n['consistency_errors']},{'FloodArea_r: reflooded'})
|
| 60 |
+
|
| 61 |
+
def test_epoch_modular_increment_and_matching_stamp_skip(self):
|
| 62 |
+
for n in self.r['native'].values():
|
| 63 |
+
self.assertEqual(len(n['epoch_probes']),12)
|
| 64 |
+
for p in n['epoch_probes']:
|
| 65 |
+
epoch=(p['epoch_before']+1)&0xffffffff;skip=epoch==p['stamp_before']
|
| 66 |
+
self.assertEqual(p['epoch_after'],epoch);self.assertEqual(p['label_after'],77 if skip else 1);self.assertEqual(p['stamp_after'],p['stamp_before'] if skip else epoch)
|
| 67 |
+
|
| 68 |
+
def test_area_bits_or_existing_bytes_and_supplied_fill(self):
|
| 69 |
+
for n in self.r['native'].values():
|
| 70 |
+
self.assertEqual(len(n['bit_output_probes']),84)
|
| 71 |
+
for p in n['bit_output_probes']:
|
| 72 |
+
size=(p['count']+7)//8;fill=p['disabled_word']!=0 or p['area']==-1;expected=[255 if fill else p['initial_byte']]*size
|
| 73 |
+
if not fill:
|
| 74 |
+
for i in range(p['count']):
|
| 75 |
+
if i%3==0:expected[i//8]|=1<<(i%8)
|
| 76 |
+
self.assertEqual(p['returned_length'],size);self.assertEqual(p['output_bytes'],expected);self.assertEqual(p['canaries'],[p['initial_byte']]*2)
|
| 77 |
+
self.assertEqual(p['supplied_memset_request'],[0x40000,255,size] if fill else None)
|
| 78 |
+
|
| 79 |
+
def test_paired_outcomes_and_known_slots(self):
|
| 80 |
+
a,b=self.r['native'].values()
|
| 81 |
+
def clean(rows):return [{k:([c[:3] for c in v] if k=='requests' else v) for k,v in p.items() if k not in ['trace','trace_sha256']} for p in rows]
|
| 82 |
+
for key in ['compositions','portal_sequence','revisit_probes','epoch_probes','bit_output_probes']:self.assertEqual(clean(a[key]),clean(b[key]))
|
| 83 |
+
prior=json.loads(Path('docs/research/bsp-references.json').read_text())
|
| 84 |
+
for label,n in self.r['native'].items():
|
| 85 |
+
for role,previous in [('count','count'),('area_base','base'),('matrix','matrix'),('epoch','epoch'),('noareas_cvar_pointer','noareas_cvar_pointer')]:self.assertEqual(n['slots'][role],prior['native'][label]['area_slots'][previous])
|
| 86 |
+
|
| 87 |
+
def test_scalar_shifts_mask_count_preserve_zero_flags_and_reject_unknown_flags(self):
|
| 88 |
+
g=graph([('cmpl','$0x1, %eax'),('shll','$0x20, %edi'),('sete','%cl'),('nop','')])
|
| 89 |
+
t=evaluate(g,0,[3],{}, {'%rax':1,'%rdi':3,'%rcx':0},capture_registers=True)
|
| 90 |
+
self.assertEqual(t['registers']['rdi'],3);self.assertEqual(t['registers']['rcx'],1)
|
| 91 |
+
for amount in [0,1,3,31,32,33]:
|
| 92 |
+
g=graph([('sarl',f'${amount}, %eax'),('nop','')]);t=evaluate(g,0,[1],{}, {'%rax':0x80000000},capture_registers=True)
|
| 93 |
+
self.assertEqual(t['registers']['rax'],(-2**31>>(amount&31))&0xffffffff)
|
| 94 |
+
with self.assertRaises(ValueError):evaluate(graph([('shll','$0x1, %eax'),('sete','%cl')]),0,[2],{}, {'%rax':1})
|
| 95 |
+
|
| 96 |
+
def test_byte_or_and_signed_greater_branch(self):
|
| 97 |
+
g=graph([('orb','%bpl, (%rdi)'),('nop','')]);t=evaluate(g,0,[1],{99:0x12,100:0xa0,101:0x34},{'%rbp':0x123408,'%rdi':100})
|
| 98 |
+
self.assertEqual(t['memory'],{99:0x12,100:0xa8,101:0x34})
|
| 99 |
+
g=graph([('cmpl','$0xffffffff, %eax'),('jg','0x3'),('movl','$0x9, %edi'),('nop','')])
|
| 100 |
+
for v in [0xfffffffe,0xffffffff,0,0x7fffffff]:
|
| 101 |
+
t=evaluate(g,0,[3],{}, {'%rax':v,'%rdi':7},capture_registers=True);self.assertEqual(t['registers']['rdi'],7 if v<0x80000000 else 9)
|
| 102 |
+
|
| 103 |
+
|
| 104 |
+
if __name__=='__main__':unittest.main()
|