diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..36173c6 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,17 @@ +name: CI + +on: + pull_request: + push: + branches: [main] + +permissions: + contents: read + +jobs: + check: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Configure and test + run: make check diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 0000000..9bcde6b --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,62 @@ +cmake_minimum_required(VERSION 3.20) +project(PTOASLModel VERSION 0.1.0 LANGUAGES C CXX) + +include(CMakePackageConfigHelpers) +include(GNUInstallDirs) + +option(PTO_ASL_MODEL_BUILD_TESTS "Build PTO ASL model tests" ON) + +add_library(pto_asl_model STATIC src/client.cpp) +add_library(PTOASLModel::pto_asl_model ALIAS pto_asl_model) +target_compile_features(pto_asl_model PUBLIC cxx_std_20) +target_compile_options(pto_asl_model PRIVATE -Wall -Wextra -Werror) +target_include_directories(pto_asl_model + PUBLIC + $ + $ +) + +add_executable(pto-model-run tools/pto-model-run.cpp) +target_link_libraries(pto-model-run PRIVATE pto_asl_model) +target_compile_options(pto-model-run PRIVATE -Wall -Wextra -Werror) + +if(PTO_ASL_MODEL_BUILD_TESTS) + enable_testing() + add_executable(pto_asl_model_abi_c_test tests/abi_c.c) + target_link_libraries(pto_asl_model_abi_c_test PRIVATE pto_asl_model) + add_executable(pto_asl_model_abi_cpp_test tests/abi_cpp.cpp) + target_link_libraries(pto_asl_model_abi_cpp_test PRIVATE pto_asl_model) + add_executable(pto_asl_model_client_test tests/client_test.cpp) + target_link_libraries(pto_asl_model_client_test PRIVATE pto_asl_model) + foreach(target + pto_asl_model_abi_c_test + pto_asl_model_abi_cpp_test + pto_asl_model_client_test) + target_compile_options(${target} PRIVATE -Wall -Wextra -Werror) + endforeach() + add_test(NAME pto_asl_model_abi_c COMMAND pto_asl_model_abi_c_test) + add_test(NAME pto_asl_model_abi_cpp COMMAND pto_asl_model_abi_cpp_test) + add_test(NAME pto_asl_model_client COMMAND pto_asl_model_client_test) +endif() + +install(TARGETS pto_asl_model EXPORT PTOASLModelTargets + ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}) +install(TARGETS pto-model-run RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR}) +install(DIRECTORY include/ DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}) +install(EXPORT PTOASLModelTargets + FILE PTOASLModelTargets.cmake + NAMESPACE PTOASLModel:: + DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/PTOASLModel) + +configure_package_config_file( + cmake/PTOASLModelConfig.cmake.in + ${CMAKE_CURRENT_BINARY_DIR}/PTOASLModelConfig.cmake + INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/PTOASLModel) +write_basic_package_version_file( + ${CMAKE_CURRENT_BINARY_DIR}/PTOASLModelConfigVersion.cmake + VERSION ${PROJECT_VERSION} + COMPATIBILITY SameMajorVersion) +install(FILES + ${CMAKE_CURRENT_BINARY_DIR}/PTOASLModelConfig.cmake + ${CMAKE_CURRENT_BINARY_DIR}/PTOASLModelConfigVersion.cmake + DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/PTOASLModel) diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..814f557 --- /dev/null +++ b/Makefile @@ -0,0 +1,14 @@ +PYTHON ?= python3 +BUILD_DIR ?= build + +.PHONY: test check + +test: + PYTHONPATH=src $(PYTHON) -m unittest discover -s tests -p 'test_*.py' + cmake -S . -B $(BUILD_DIR) -DCMAKE_BUILD_TYPE=Release + cmake --build $(BUILD_DIR) -j 8 + ctest --test-dir $(BUILD_DIR) --output-on-failure + +check: test + $(PYTHON) -m py_compile src/pto_asl_model/*.py scripts/pto-asl-run + git diff --check diff --git a/README.md b/README.md index 5518d90..5edf9c9 100644 --- a/README.md +++ b/README.md @@ -10,3 +10,71 @@ model lifecycle, hosted execution, transport, ABI, ELF loading, and validation. Development changes land through pull requests. The initial ASLRef backend is tracked by the repository issue list. + +## Reference runner + +The first closure runs consecutive PTO instructions inside one ASLRef process. +It accepts a checked static ELF whose load segments fit the explicit hosted +memory bound, plus an assembled PTO ASL file: + +```bash +scripts/pto-asl-run \ + --asl-spec /path/to/pto-spec/build/pto-spec.asl \ + --aslref /path/to/aslref \ + --elf program.elf \ + --stop-pc 0x114 \ + --stop-after-hits 2 \ + --start-pc 0x120 \ + --return-pc 0x114 \ + --max-steps 6 \ + --result-address 0x200 \ + --result-size 4 \ + --memory-bytes 0x20000 \ + --tile-elements 1 \ + --runtime-typecheck minimal \ + --memory-backend host-sparse \ + --result-out result.bin \ + --manifest-out run.json \ + --lock pto-lock.json +``` + +Run repository checks with `make check`. + +## Performance status + +The one-shot process backend uses a fresh-process reset specialization. The +pinned ASLRef initializes fresh global storage to zero, so the runner removes +only the redundant byte-by-byte memory-clear loop while retaining every +register, queue, Tile, bundle, fault, ACR, and system-state reset. The +specialization matches the exact PTO reset loop once and fails closed if that +source shape changes. + +Minimal-typecheck runs now default to the model-owned `host-sparse` backend. +It links a small executable against the exact pinned ASLRef `asllib` and binds +only `ReadPhysicalMemoryByte` and `WritePhysicalMemoryByte` to an O(1) sparse +host byte map. Translation, permission, ordering, preflight, faults, decode, +and instruction semantics remain in PTO ASL. The executable is content-addressed +by the ASLRef commit, `asllib` hash, model source hash, and OCaml version. + +On the measured Darwin host, `scalar.abs_i32_thr` fell from 2415.72 seconds +with the ASL reference array to 424.93 seconds with host memory, a 5.68x +improvement, while preserving final TPC and the complete 8 KiB result SHA-256. +The earlier fresh-process reset specialization remains active; on a 128 KiB +TLOAD carrier it reduced 600.6 seconds to 61.0 seconds with the same result. +Use `--memory-backend reference-array` for explicit parity checks. + +The remaining process path is still parse/startup dominated for short cases. +A native persistent-worker prototype reaches sub-millisecond warm decode/step +latency after initialization, while a full reusable-state reset takes 544–582 +seconds. + +The next accelerated backend keeps a pristine initialized worker and forks +one copy-on-write child per case. This reuses the parsed/typechecked model while +preserving case isolation. Worker-pool concurrency must be bounded by memory; +the measured initialized worker peaks near 498 MiB RSS. The one-shot +host-memory backend remains the default until that snapshot backend passes its +promotion gates. + +The reset contract is in [`docs/model-ndf-v1.md`](docs/model-ndf-v1.md). The +snapshot lifecycle, identity, transport, and promotion gates are in +[`docs/worker-snapshot-design.md`](docs/worker-snapshot-design.md). diff --git a/cmake/PTOASLModelConfig.cmake.in b/cmake/PTOASLModelConfig.cmake.in new file mode 100644 index 0000000..eafda52 --- /dev/null +++ b/cmake/PTOASLModelConfig.cmake.in @@ -0,0 +1,3 @@ +@PACKAGE_INIT@ + +include("${CMAKE_CURRENT_LIST_DIR}/PTOASLModelTargets.cmake") diff --git a/docs/aslref-patch-audit.md b/docs/aslref-patch-audit.md new file mode 100644 index 0000000..bd7d8f6 --- /dev/null +++ b/docs/aslref-patch-audit.md @@ -0,0 +1,18 @@ +# ASLRef patch audit + +The reference runner consumes ASLRef commit +`0b6e09066d4186c8a26e02e3bb884bd664d5eb34`, exactly matching the PTO-SPEC +`.aslref-version` at the model lock's PTO commit. + +The initial implementation applies no patch to ASLRef: + +- parser semantic patches: 0; +- typechecker semantic patches: 0; +- interpreter semantic patches: 0; +- standard-library semantic patches: 0. + +Consecutive PTO instructions execute through a generated ASL harness in one +ASLRef process. The harness calls only the PTO-owned +`ExecuteNextPTOInstruction` action and uses reference-profile initialization and +observation functions. ELF parsing, memory initialization, stop policy, and +manifest formatting remain outside ASLRef. diff --git a/docs/model-ndf-v1.md b/docs/model-ndf-v1.md new file mode 100644 index 0000000..433882c --- /dev/null +++ b/docs/model-ndf-v1.md @@ -0,0 +1,99 @@ +# PTO ASL model NDF v1 + +This repository consumes PTO architecture from an exact PTO-SPEC ASL revision. +It does not own instruction semantics. + +## Model architecture + +- `PTO-MODEL-INSTANCE-001`: one model instance carries one isolated projection + of PTO architectural state and model lifecycle state. +- `PTO-MODEL-ASLREF-001`: the reference backend executes the pinned ASLRef + interpreter without parser, typechecker, or interpreter semantic patches. +- `PTO-MODEL-STEP-001`: one step invokes the PTO-owned next-instruction action; + model observations cannot refine its architectural meaning. + +## Hosted runner ABI + +- `PTO-MODEL-ELF-001`: the initial runner accepts little-endian static ELF64 + `ET_EXEC` images with bounded, non-overlapping `PT_LOAD` segments and explicit + stop-PC/result policy. The caller selects a bounded hosted-memory profile; + its memory and Tile capacities are model bounds, not architectural capacity + claims. + The stop policy may select a later occurrence of the same PC, so a return + label embedded in an entry bundle is not mistaken for program completion. + A direct-boot profile may start at a verified executable symbol and seed the + captured return state plus architectural GPR R10 (`ra`) with the verified + return PC, bypassing platform service-request startup glue. The paired state + is model ABI: compiler-generated epilogues may select `ra`, while PTO return + bundle state independently carries the captured target. +- `PTO-MODEL-MANIFEST-001`: each run emits a deterministic JSON manifest bound + to the exact PTO tree, ASLRef pin, ELF hash, entry, stop policy, result bytes, + and final TPC. +- `PTO-MODEL-C-ABI-001`: C and C++ consumers invoke the hosted reference runner + through a versioned standard-layout configuration without observing worker + transport details. +- `PTO-MODEL-HOST-MEMORY-001`: a model-owned executable MAY bind PTO's + `ReadPhysicalMemoryByte` and `WritePhysicalMemoryByte` profile hooks to O(1) + host storage. It MUST NOT replace ASL-owned translation, access permission, + preflight, ordering, fault, decode, or instruction semantics. +- `PTO-MODEL-HOST-MEMORY-IDENTITY-001`: the host-memory executable MUST link + the exact pinned ASLRef `asllib` and MUST be content-addressed by the ASLRef + commit, `asllib` hash, model source hash, and OCaml version. Every run + manifest MUST record that identity and the selected memory backend. + +## Implementation boundary + +The implementation assembles a run-specific ASL harness and executes it once +with the pinned ASLRef interpreter. Consecutive instructions execute inside +that single process. Minimal-typecheck runs default to the model-owned +host-memory executable; strict or explicit `reference-array` runs use the +stock pinned `aslref` binary. ELF parsing, memory initialization, stop policy, +backend selection, and manifest generation are model implementation behavior. + +The transport may later move to a persistent library backend without changing +PTO architecture or the hosted manifest contract. + +## Performance and worker lifecycle + +- `PTO-MODEL-FRESH-RESET-001`: the one-shot process backend MAY remove the + byte-by-byte `_Memory` clear from `ResetProfileState()` only when the pinned + ASLRef process is newly created, its global storage is initially zero, and + the process executes exactly one ELF. Every other architectural and model + state reset MUST remain present. +- `PTO-MODEL-FRESH-RESET-DRIFT-001`: the specialization MUST match the exact + PTO-owned memory-reset loop once and MUST fail closed if the owner changes. + A persistent or reused worker MUST NOT select this policy. +- `PTO-MODEL-FRESH-RESET-PARITY-001`: promotion requires the same ELF, PTO + tree, ASLRef pin, terminal PC, result bytes, and failure class under the full + and fresh-process reset policies. The run manifest MUST record the selected + reset policy. +- `PTO-MODEL-WORKER-SNAPSHOT-001`: an accelerated backend may parse and + initialize the pinned ASL model once, then fork a copy-on-write child for one + case. The pristine parent MUST NOT execute case commands or return into ASL + mutable execution after the snapshot point. +- `PTO-MODEL-CASE-ISOLATION-001`: one case child owns all architectural and + hosted state changes for that run and exits after reporting its terminal + result. A later case MUST begin from the pristine parent snapshot, not from a + full in-model reset of the preceding case. +- `PTO-MODEL-WORKER-POOL-001`: pool size is a model resource policy. It MUST be + bounded independently of GTest concurrency and reported with peak RSS and + cold-ready, case-run, and recycle timings. +- `PTO-MODEL-DARWIN-STACK-001`: a native Darwin ASLRef worker MUST be linked + with an explicit main-thread stack large enough for the pinned model. The + measured minimum working configuration uses a 512 MiB `LC_MAIN` stack; shell + `ulimit` alone is insufficient. + +On the measured host, the original process-per-case path took 526–600 seconds. +Fresh-process reset reduced one 128 KiB TLOAD carrier from 600.6 seconds to +61.0 seconds while preserving its terminal PC and result SHA-256. A persistent +prototype takes about 510 seconds to become ready, then decodes and steps in +less than one millisecond, with roughly 498 MiB peak RSS. Full reusable-state +reset takes 544–582 seconds, so reset-per-case reuse remains rejected; the +snapshot child lifecycle above is the selected direction beyond the one-shot +optimization. + +For a compiler-generated scalar throughput ELF, replacing ASL list-backed +physical memory with the host sparse map reduced 2415.72 seconds to 424.93 +seconds (5.68x) with identical final TPC and complete 8 KiB result SHA-256. +This optimization is orthogonal to snapshot reuse: it removes linear physical +memory indexing, while snapshot reuse removes repeated parse/startup cost. diff --git a/docs/worker-snapshot-design.md b/docs/worker-snapshot-design.md new file mode 100644 index 0000000..88bbbe6 --- /dev/null +++ b/docs/worker-snapshot-design.md @@ -0,0 +1,92 @@ +# Snapshot worker design + +This document defines the selected accelerated lifecycle for the PTO ASL +functional model. It is a model implementation contract, not PTO architecture. + +## Why snapshot workers + +The original process backend was cold-start dominated. On the measured Darwin +host, one specialized run took 526–600 seconds. The fresh-process reset policy +now removes the redundant memory sweep and reduced one 128 KiB TLOAD carrier +from 600.6 seconds to 61.0 seconds without changing its terminal PC or result +SHA-256. A native persistent +prototype takes 510.271 seconds to become ready, after which decode and step +commands take 0.284–0.983 milliseconds. Re-running `ResetProfileState()` takes +544.350–582.447 seconds, so reset-per-case reuse is slower than the current +backend and is rejected. + +The one-shot host-memory backend also removes ASL list-backed physical-memory +indexing. On `scalar.abs_i32_thr` it reduced 2415.72 seconds to 424.93 seconds +with identical final TPC and 8 KiB result SHA-256. It remains one process per +case, so the snapshot design below still targets repeated parse/startup cost. + +The initialized worker peaks near 498 MiB RSS. Pool concurrency therefore must +be explicit and memory-bounded. + +## Selected lifecycle + +The worker is an asl-model-owned executable linked against the exact pinned +ASLRef `asllib`; it does not patch the ASLRef parser, typechecker, interpreter, +or standard library. + +```text +parse and typecheck the specialized PTO specification + -> initialize the interpreter environment + -> enter the static worker ASL wrapper + -> ResetProfileState() exactly once + -> enter HostReadCommand() + pristine parent: accept request, fork, wait/reap; never return to ASL + case child: receive one case, execute one ELF, report, then _exit +``` + +The fork gate belongs in a small C stub called by the model-owned host +primitive. Keeping the parent inside that stub avoids allocating protocol +objects in the parent OCaml heap and minimizes copy-on-write dirtiness. + +## Isolation and identity + +Each case child owns all architectural and hosted mutations for exactly one +run. A child is never reset and reused. A failed, timed-out, or crashed child is +discarded; the next case forks from the unchanged parent snapshot. + +Workers are keyed by all state that can change behavior: + +- PTO tree and ASLRef commit; +- worker executable and protocol version; +- exact `memory_bytes` and `tile_elements` bounds; +- runtime typecheck mode and static wrapper version. + +Profiles must not be coalesced into a larger bound because bounds affect +observable access and fault behavior. + +## Transport + +The shared daemon uses framed Unix-domain `SOCK_STREAM` connections. The +Python runner retains current ELF, sidecar, symbol, hash, and segment +validation, opens the verified ELF once, and passes its read-only descriptor +with `SCM_RIGHTS`. The pristine parent reads only a fixed fork header; the case +child reads variable payload and ELF segments with `pread`. + +The request contains start, return, stop, stack, step, result, profile, segment, +and ELF-hash data. The child initializes memory through PTO-owned ASL accessors, +sets both captured return state and R10, then executes only +`ExecuteNextPTOInstruction()` until the stop policy terminates. + +## Platform requirements + +Darwin workers must be linked with a 512 MiB `LC_MAIN` stack +(`-Wl,-stack_size,0x20000000`). Raising shell stack limits alone is not +sufficient. Linux launchers must set the corresponding stack resource limit. + +## Promotion gates + +The process backend remains the default until the snapshot backend proves: + +1. one cold parent reaches the post-reset fork gate; +2. good–failing–good cases demonstrate pristine isolation; +3. one ELF matches the process backend and independent golden byte-for-byte; +4. eight same-profile children run concurrently without cross-talk; +5. the 124 scalar GTests pass with cold, fork, case, recycle, and memory data; +6. every exact profile required by the 341-case corpus passes; +7. crash, timeout, busy, stale-socket, and parent-restart paths pass; +8. two consecutive complete green runs are reproducible. diff --git a/include/pto/pto_asl_model.h b/include/pto/pto_asl_model.h new file mode 100644 index 0000000..557901e --- /dev/null +++ b/include/pto/pto_asl_model.h @@ -0,0 +1,54 @@ +#ifndef PTO_ASL_MODEL_H +#define PTO_ASL_MODEL_H + +#include + +#ifdef __cplusplus +extern "C" { +#endif + +#define PTO_ASL_MODEL_ABI_VERSION UINT32_C(0x00020000) + +typedef uint32_t pto_model_status_t; +enum { + PTO_MODEL_STATUS_OK = 0, + PTO_MODEL_STATUS_INVALID_ARGUMENT = 1, + PTO_MODEL_STATUS_ABI_MISMATCH = 2, + PTO_MODEL_STATUS_WORKER_LAUNCH_ERROR = 3, + PTO_MODEL_STATUS_WORKER_FAILED = 4 +}; + +typedef struct { + uint32_t abi_version; + uint32_t struct_size; + const char *runner_path; + const char *asl_spec_path; + const char *aslref_path; + const char *lock_path; + const char *elf_path; + const char *sidecar_path; + const char *manifest_output_path; + const char *result_output_path; + uint64_t stop_pc; + uint64_t max_steps; + uint64_t result_address; + uint64_t result_size; + uint64_t stack_top; + uint64_t memory_bytes; + uint64_t tile_elements; + uint64_t stop_after_hits; + uint64_t start_pc; + uint64_t return_pc; +} pto_model_elf_run_config_t; + +/* Execute one complete hosted ELF run through the reference backend. The + * runner transport is implementation-owned; the caller observes only this + * versioned ABI and the deterministic manifest. */ +pto_model_status_t pto_model_run_elf( + const pto_model_elf_run_config_t *config); + +#ifdef __cplusplus +} +#endif + +#endif diff --git a/pto-lock.json b/pto-lock.json new file mode 100644 index 0000000..bef1131 --- /dev/null +++ b/pto-lock.json @@ -0,0 +1,12 @@ +{ + "schema": "pto-asl-model-lock-v1", + "pto_repository": "https://github.com/PTO-ISA/pto-spec.git", + "pto_ref": "refs/heads/main", + "pto_commit": "f56c82779f3e0a02d3bcce493a3f15efde6845db", + "pto_tree": "a257683e309e6bcf3767a51e4cc2821c58474d6d", + "aslref_repository": "https://github.com/herd/herdtools7.git", + "aslref_commit": "0b6e09066d4186c8a26e02e3bb884bd664d5eb34", + "architecture_version": "0.58.5", + "model_abi": "pto-asl-model-experimental-v2", + "worker_protocol": "pto-asl-worker-v1" +} diff --git a/scripts/pto-asl-run b/scripts/pto-asl-run new file mode 100755 index 0000000..810ba88 --- /dev/null +++ b/scripts/pto-asl-run @@ -0,0 +1,12 @@ +#!/usr/bin/env python3 +from __future__ import annotations + +import pathlib +import sys + +ROOT = pathlib.Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / "src")) + +from pto_asl_model.runner import main + +raise SystemExit(main()) diff --git a/src/client.cpp b/src/client.cpp new file mode 100644 index 0000000..e445a9e --- /dev/null +++ b/src/client.cpp @@ -0,0 +1,120 @@ +#include "pto/pto_asl_model.h" + +#include +#include +#include +#include +#include +#include + +extern char **environ; + +namespace { + +bool HasText(const char *value) +{ + return value != nullptr && value[0] != '\0'; +} + +std::string Decimal(std::uint64_t value) +{ + return std::to_string(value); +} + +} // namespace + +extern "C" pto_model_status_t pto_model_run_elf( + const pto_model_elf_run_config_t *config) +{ + if (config == nullptr) { + return PTO_MODEL_STATUS_INVALID_ARGUMENT; + } + if (config->abi_version != PTO_ASL_MODEL_ABI_VERSION || + config->struct_size != sizeof(*config)) { + return PTO_MODEL_STATUS_ABI_MISMATCH; + } + if (!HasText(config->runner_path) || !HasText(config->asl_spec_path) || + !HasText(config->aslref_path) || !HasText(config->elf_path) || + !HasText(config->manifest_output_path) || + (config->max_steps == 0 && !HasText(config->sidecar_path))) { + return PTO_MODEL_STATUS_INVALID_ARGUMENT; + } + + const std::string stop_pc = Decimal(config->stop_pc); + const std::string max_steps = Decimal(config->max_steps); + const std::string result_address = Decimal(config->result_address); + const std::string result_size = Decimal(config->result_size); + const std::string stack_top = Decimal(config->stack_top); + const std::string memory_bytes = Decimal(config->memory_bytes); + const std::string tile_elements = Decimal(config->tile_elements); + const std::string stop_after_hits = Decimal(config->stop_after_hits); + const std::string start_pc = Decimal(config->start_pc); + const std::string return_pc = Decimal(config->return_pc); + std::vector arguments = { + const_cast(config->runner_path), + const_cast("--asl-spec"), + const_cast(config->asl_spec_path), + const_cast("--aslref"), + const_cast(config->aslref_path), + const_cast("--elf"), + const_cast(config->elf_path), + const_cast("--stop-pc"), + const_cast(stop_pc.c_str()), + const_cast("--stop-after-hits"), + const_cast(stop_after_hits.c_str()), + const_cast("--start-pc"), + const_cast(start_pc.c_str()), + const_cast("--return-pc"), + const_cast(return_pc.c_str()), + const_cast("--max-steps"), + const_cast(max_steps.c_str()), + const_cast("--result-address"), + const_cast(result_address.c_str()), + const_cast("--result-size"), + const_cast(result_size.c_str()), + const_cast("--stack-top"), + const_cast(stack_top.c_str()), + const_cast("--memory-bytes"), + const_cast(memory_bytes.c_str()), + const_cast("--tile-elements"), + const_cast(tile_elements.c_str()), + const_cast("--manifest-out"), + const_cast(config->manifest_output_path), + const_cast("--quiet"), + }; + if (HasText(config->lock_path)) { + arguments.push_back(const_cast("--lock")); + arguments.push_back(const_cast(config->lock_path)); + } + if (HasText(config->sidecar_path)) { + arguments.push_back(const_cast("--sidecar")); + arguments.push_back(const_cast(config->sidecar_path)); + } + if (HasText(config->result_output_path)) { + arguments.push_back(const_cast("--result-out")); + arguments.push_back(const_cast(config->result_output_path)); + } + arguments.push_back(nullptr); + + pid_t process = 0; + const int spawn_status = posix_spawn( + &process, + config->runner_path, + nullptr, + nullptr, + arguments.data(), + environ); + if (spawn_status != 0) { + return PTO_MODEL_STATUS_WORKER_LAUNCH_ERROR; + } + int worker_status = 0; + while (waitpid(process, &worker_status, 0) < 0) { + if (errno != EINTR) { + return PTO_MODEL_STATUS_WORKER_FAILED; + } + } + if (!WIFEXITED(worker_status) || WEXITSTATUS(worker_status) != 0) { + return PTO_MODEL_STATUS_WORKER_FAILED; + } + return PTO_MODEL_STATUS_OK; +} diff --git a/src/pto_asl_model/__init__.py b/src/pto_asl_model/__init__.py new file mode 100644 index 0000000..f48d7f2 --- /dev/null +++ b/src/pto_asl_model/__init__.py @@ -0,0 +1,11 @@ +"""PTO ASLRef-backed functional-model tooling.""" + +from .runner import ElfError, ElfImage, LoadSegment, RunConfiguration, run + +__all__ = [ + "ElfError", + "ElfImage", + "LoadSegment", + "RunConfiguration", + "run", +] diff --git a/src/pto_asl_model/aslref_host_memory.ml b/src/pto_asl_model/aslref_host_memory.ml new file mode 100644 index 0000000..33a79d6 --- /dev/null +++ b/src/pto_asl_model/aslref_host_memory.ml @@ -0,0 +1,123 @@ +open Asllib + +module Memory = struct + let bytes : (int, int) Hashtbl.t = Hashtbl.create 16384 + + let integer = function + | Native.NV_Literal (AST.L_BitVector value) -> + Z.to_int (Bitvector.to_z_unsigned value) + | Native.NV_Literal (AST.L_Int value) -> Z.to_int value + | _ -> invalid_arg "physical memory value must be an integer" + + let read address = Option.value (Hashtbl.find_opt bytes address) ~default:0 + + let write address value = + if address < 0 then invalid_arg "negative physical memory address"; + if value < 0 || value > 255 then + invalid_arg "physical memory value is not a byte"; + if value = 0 then Hashtbl.remove bytes address + else Hashtbl.replace bytes address value +end + +let named_ty name = AST.T_Named name |> ASTUtils.add_dummy_pos + +let primitive_decl ?returns ?(side_effecting = false) name args = + let open AST in + { + name; + parameters = []; + args; + body = SB_Primitive side_effecting; + return_type = returns; + subprogram_type = + (match returns with None -> ST_Procedure | Some _ -> ST_Function); + recurse_limit = None; + qualifier = if side_effecting then None else Some Pure; + override = None; + builtin = true; + } + +module HostBackend = struct + include Native.DeterministicBackend + + let read_physical_memory_byte _parameters args = + match args with + | [ address ] -> + let byte = Memory.read (Memory.integer address) in + [ Native.NV_Literal + (AST.L_BitVector (Bitvector.of_int_sized 8 byte)) ] + | _ -> invalid_arg "ReadPhysicalMemoryByte takes one argument" + + let write_physical_memory_byte _parameters args = + match args with + | [ address; value ] -> + Memory.write (Memory.integer address) (Memory.integer value); + [] + | _ -> invalid_arg "WritePhysicalMemoryByte takes two arguments" + + let primitives = + let read = + primitive_decl ~returns:(named_ty "Byte") + "ReadPhysicalMemoryByte" [ ("address", named_ty "Word") ] + in + let write = + primitive_decl ~side_effecting:true "WritePhysicalMemoryByte" + [ ("address", named_ty "Word"); ("value", named_ty "Byte") ] + in + [ (read, read_physical_memory_byte); (write, write_physical_memory_byte) ] + @ Native.DeterministicBackend.primitives +end + +module InterpreterConfig = struct + module Instr = Instrumentation.SemanticsNoInstr + + let unroll = 0 + let recursive_unroll _ = None + let error_handling_time = Error.Dynamic + let empty_branching_effects_optimization = true + let log_nondet_choice = false + let display_call_stack_on_error = false + let track_symbolic_path = false + let bit_clear_optimisation = false +end + +module HostInterpreter = Interpreter.Make (HostBackend) (InterpreterConfig) + +let type_check_config = + (module struct + let check = Typing.Silence + let output_format = Error.HumanReadable + let print_typed = false + let use_field_getter_extension = false + let fine_grained_side_effects = false + let use_conflicting_side_effects_extension = false + let override_mode = Typing.Permissive + end : Typing.ANNOTATE_CONFIG) + +let exit_value = function + | Native.NV_Literal (AST.L_Int value) -> Z.to_int value + | _ -> invalid_arg "ASL main must return an integer" + +let run model_path = + let ast = Builder.from_file `ASLv1 model_path in + let ast = Builder.with_stdlib ~no_stdlib0:true ast in + let ast = Builder.with_primitives HostBackend.primitives ast in + let module T = Typing.Annotate (val type_check_config) in + let typed_ast, static_env = T.type_check_ast ast in + let main_name = T.find_main static_env in + HostInterpreter.run_typed static_env main_name typed_ast |> exit_value + +let model_path () = + match Array.to_list Sys.argv with + | [ _; path ] -> path + | [ _; "--no-type-check"; path ] -> path + | _ -> + Printf.eprintf "usage: %s [--no-type-check] \n%!" Sys.argv.(0); + exit 2 + +let () = + try exit (run (model_path ())) + with exn -> + Printf.eprintf "host-memory ASL runner failed: %s\n%!" + (Printexc.to_string exn); + exit 1 diff --git a/src/pto_asl_model/runner.py b/src/pto_asl_model/runner.py new file mode 100644 index 0000000..be9f503 --- /dev/null +++ b/src/pto_asl_model/runner.py @@ -0,0 +1,1160 @@ +"""Run one static PTO ELF in one pinned ASLRef process.""" + +from __future__ import annotations + +import argparse +import dataclasses +import hashlib +import json +import os +import pathlib +import re +import shutil +import struct +import subprocess +import sys +import tempfile +import time +from collections.abc import Sequence + + +ELF_HEADER = struct.Struct("<16sHHIQQQIHHHHHH") +PROGRAM_HEADER = struct.Struct(" int: + return self.address + self.memory_size + + +@dataclasses.dataclass(frozen=True) +class ElfImage: + entry: int + segments: tuple[LoadSegment, ...] + symbols: tuple["ElfSymbol", ...] + sha256: str + + +@dataclasses.dataclass(frozen=True) +class ElfSymbol: + name: str + value: int + size: int + section_index: int + + +@dataclasses.dataclass(frozen=True) +class RunConfiguration: + asl_spec: pathlib.Path + aslref: pathlib.Path + elf: pathlib.Path + stop_pc: int + max_steps: int + result_address: int + result_size: int + memory_bytes: int = REFERENCE_MEMORY_BYTES + tile_elements: int = REFERENCE_TILE_ELEMENTS + runtime_typecheck: str = "strict" + stop_after_hits: int = 1 + start_pc: int = 0 + return_pc: int = 0 + stack_top: int = 0 + manifest_output: pathlib.Path | None = None + result_output: pathlib.Path | None = None + lock: pathlib.Path | None = None + sidecar: pathlib.Path | None = None + memory_backend: str = "host-sparse" + + +def _checked_range(start: int, size: int, limit: int, label: str) -> tuple[int, int]: + if start < 0 or size < 0 or start > limit or size > limit - start: + raise ElfError(f"{label} range is outside reference memory") + return start, start + size + + +def parse_elf(path: pathlib.Path, + memory_bytes: int = REFERENCE_MEMORY_BYTES) -> ElfImage: + if memory_bytes < 256 or memory_bytes > MAX_HOSTED_MEMORY_BYTES: + raise ElfError("hosted memory bound is outside the supported model profile") + content = path.read_bytes() + if len(content) < ELF_HEADER.size: + raise ElfError("ELF header is truncated") + fields = ELF_HEADER.unpack_from(content) + identification = fields[0] + if identification[:4] != ELF_MAGIC: + raise ElfError("ELF magic mismatch") + if identification[4] != ELF_CLASS_64 or identification[5] != ELF_DATA_LITTLE: + raise ElfError("requires ELF64 little-endian input") + if identification[6] != ELF_VERSION_CURRENT: + raise ElfError("unsupported ELF identification version") + elf_type, machine, version = fields[1:4] + entry, program_offset, section_offset = fields[4:7] + header_size, program_entry_size, program_count = fields[8:11] + section_entry_size, section_count = fields[11:13] + if elf_type != ELF_TYPE_EXEC: + raise ElfError("requires static ET_EXEC input") + if machine != PTO_ELF_MACHINE: + raise ElfError("unexpected ELF machine") + if version != ELF_VERSION_CURRENT or header_size != ELF_HEADER.size: + raise ElfError("unsupported ELF header version or size") + if program_entry_size != PROGRAM_HEADER.size: + raise ElfError("unexpected program-header size") + if section_count and section_entry_size != SECTION_HEADER.size: + raise ElfError("unexpected section-header size") + table_size = program_entry_size * program_count + if program_offset > len(content) or table_size > len(content) - program_offset: + raise ElfError("program-header table is truncated") + + segments: list[LoadSegment] = [] + ranges: list[tuple[int, int]] = [] + for index in range(program_count): + offset = program_offset + index * program_entry_size + (kind, flags, file_offset, virtual_address, physical_address, + file_size, memory_size, alignment) = PROGRAM_HEADER.unpack_from(content, offset) + if kind != PROGRAM_TYPE_LOAD: + continue + if flags & ~(PROGRAM_FLAG_READ | PROGRAM_FLAG_WRITE | PROGRAM_FLAG_EXECUTE): + raise ElfError("PT_LOAD contains unknown permission bits") + if file_size > memory_size: + raise ElfError("PT_LOAD file size exceeds memory size") + if file_offset > len(content) or file_size > len(content) - file_offset: + raise ElfError("PT_LOAD file range is truncated") + if virtual_address != physical_address: + raise ElfError("initial profile requires identical virtual and physical addresses") + start, end = _checked_range( + virtual_address, + memory_size, + memory_bytes, + "PT_LOAD", + ) + if alignment not in (0, 1) and virtual_address % alignment != file_offset % alignment: + raise ElfError("PT_LOAD alignment congruence failed") + for previous_start, previous_end in ranges: + if start < previous_end and previous_start < end: + raise ElfError("PT_LOAD ranges overlap") + ranges.append((start, end)) + payload = content[file_offset:file_offset + file_size] + segments.append(LoadSegment(start, payload, memory_size, flags, alignment)) + + if not segments: + raise ElfError("ELF contains no PT_LOAD segments") + executable_entry = any( + segment.address <= entry < segment.end + and segment.flags & PROGRAM_FLAG_EXECUTE + for segment in segments + ) + if not executable_entry: + raise ElfError("ELF entry is outside an executable PT_LOAD") + + symbols: list[ElfSymbol] = [] + section_table_size = section_entry_size * section_count + if section_count: + if (section_offset > len(content) + or section_table_size > len(content) - section_offset): + raise ElfError("section-header table is truncated") + sections = [ + SECTION_HEADER.unpack_from(content, section_offset + index * section_entry_size) + for index in range(section_count) + ] + for section in sections: + section_type = section[1] + if section_type not in SECTION_TYPE_SYMBOLS: + continue + symbol_offset, symbol_size = section[4], section[5] + string_index, entry_size = section[6], section[9] + if entry_size != SYMBOL_ENTRY.size or string_index >= section_count: + raise ElfError("invalid ELF symbol table metadata") + string_section = sections[string_index] + string_offset, string_size = string_section[4], string_section[5] + if (symbol_offset > len(content) + or symbol_size > len(content) - symbol_offset + or string_offset > len(content) + or string_size > len(content) - string_offset): + raise ElfError("ELF symbol or string table is truncated") + strings = content[string_offset:string_offset + string_size] + if symbol_size % entry_size: + raise ElfError("ELF symbol table has a partial entry") + for offset in range(symbol_offset, symbol_offset + symbol_size, entry_size): + name_offset, _info, _other, symbol_section, value, size = ( + SYMBOL_ENTRY.unpack_from(content, offset) + ) + if name_offset >= len(strings): + raise ElfError("ELF symbol name is outside its string table") + name_end = strings.find(b"\0", name_offset) + if name_end < 0: + raise ElfError("ELF symbol name is unterminated") + name = strings[name_offset:name_end].decode("utf-8", errors="strict") + if name: + symbols.append(ElfSymbol(name, value, size, symbol_section)) + return ElfImage( + entry=entry, + segments=tuple(sorted(segments, key=lambda segment: segment.address)), + symbols=tuple(symbols), + sha256=hashlib.sha256(content).hexdigest(), + ) + + +def _word(value: int) -> str: + if value < 0 or value >= 1 << 64: + raise ValueError("word value is outside 64 bits") + return f"Zeros{{PTO_XLEN}} + 0x{value:x}" + + +def build_harness(image: ElfImage, configuration: RunConfiguration) -> str: + if configuration.max_steps <= 0: + raise ValueError("max_steps must be positive") + if configuration.stop_after_hits <= 0: + raise ValueError("stop_after_hits must be positive") + _checked_range( + configuration.result_address, + configuration.result_size, + configuration.memory_bytes, + "result", + ) + for segment in image.segments: + _checked_range( + segment.address, + segment.memory_size, + configuration.memory_bytes, + "PT_LOAD", + ) + start_pc = configuration.start_pc or image.entry + executable_start = any( + segment.address <= start_pc < segment.end + and segment.flags & PROGRAM_FLAG_EXECUTE + for segment in image.segments + ) + if not executable_start: + raise ElfError("hosted start PC is outside an executable PT_LOAD") + lines = [ + "func main() => integer", + "begin", + " ResetProfileState();", + f" WriteTPC({_word(start_pc)});", + " var model_stop_hits: integer = 0;", + " var previous_pc: bits(PTO_XLEN) = ReadTPC();", + " var previous_previous_pc: bits(PTO_XLEN) = ReadTPC();", + ] + if configuration.return_pc: + lines.extend([ + f" _ReturnAddress = {_word(configuration.return_pc)};", + " WritePEGPR(0, " + f"{PTO_HOSTED_RA_GPR}, {_word(configuration.return_pc)});", + ]) + if configuration.stack_top: + lines.append( + " WritePEGPR(0, " + f"{PTO_HOSTED_SP_GPR}, {_word(configuration.stack_top)});" + ) + for segment in image.segments: + initialized = segment.data + bytes(segment.memory_size - len(segment.data)) + for offset, value in enumerate(initialized): + if value: + lines.append( + " WritePhysicalMemoryByte(" + f"{_word(segment.address + offset)}, Zeros{{8}} + 0x{value:02x});" + ) + rejection_diagnostics: list[str] = [] + if configuration.stack_top: + rejection_diagnostics.extend([ + ' println "PTO_DIAG_STACK_RA ",', + " UInt(LoadTranslatedUnsigned(" + f"{_word(configuration.stack_top - 8)}, 8));", + ' println "PTO_DIAG_STACK_S0 ",', + " UInt(LoadTranslatedUnsigned(" + f"{_word(configuration.stack_top - 16)}, 8));", + ]) + lines.extend([ + f" for model_step = 0 to {configuration.max_steps - 1} do", + " let step_pc = ReadTPC();", + " let status = ExecuteNextPTOInstruction();", + " if status == PTOInstruction_Rejected then", + ' println "PTO_REJECTED_TPC ", UInt(step_pc);', + ' println "PTO_PREVIOUS_TPC ", UInt(previous_pc);', + ' println "PTO_PREVIOUS_PREVIOUS_TPC ",', + " UInt(previous_previous_pc);", + ' println "PTO_FAULT_STATUS ",', + " UInt(PackTrapStatus(CurrentACR()));", + ' println "PTO_DIAG_FAULT_CODE ", _LastFault;', + ' println "PTO_FAULT_ADDRESS ", UInt(_FaultAddress);', + ' println "PTO_DIAG_SP ", UInt(ReadPEGPR(0, 1));', + ' println "PTO_DIAG_RA ", UInt(ReadPEGPR(0, 10));', + ' println "PTO_DIAG_RETURN_ADDRESS ", UInt(_ReturnAddress);', + ' if _BundleActive then', + ' println "PTO_DIAG_BUNDLE_ACTIVE 1";', + ' println "PTO_DIAG_MGATHER_SELECTED ",', + ' if BundleMGATHERSelected() then 1 else 0;', + ' println "PTO_DIAG_MSCATTER_SELECTED ",', + ' if BundleMSCATTERSelected() then 1 else 0;', + ' println "PTO_DIAG_TILE_BINDINGS ",', + ' BundleTileBindingCount();', + ' println "PTO_DIAG_SHARED_BINDINGS ",', + ' BundleSharedBindingCount();', + ' println "PTO_DIAG_SCALAR0_VALID ",', + ' if _BundleScalarBindings[[0]].valid then 1 else 0;', + ' if _BundleScalarBindings[[0]].valid then', + ' println "PTO_DIAG_SCALAR_SOURCE0 ",', + ' _BundleScalarBindings[[0]].source0;', + ' println "PTO_DIAG_SCALAR_SOURCE1 ",', + ' _BundleScalarBindings[[0]].source1;', + ' println "PTO_DIAG_GPR_BASE ",', + ' UInt(ReadPEAbsoluteGPROperand(_CurrentMemoryAgent,', + ' _BundleScalarBindings[[0]].source0));', + ' println "PTO_DIAG_GPR_STRIDE ",', + ' UInt(ReadPEAbsoluteGPROperand(_CurrentMemoryAgent,', + ' _BundleScalarBindings[[0]].source1));', + ' end;', + ' println "PTO_DIAG_DIM0_PRESENT ",', + ' if _BundleDimensionPresent[[0]] then 1 else 0;', + ' println "PTO_DIAG_DIM0 ", UInt(_BundleDimensions[[0]]);', + ' println "PTO_DIAG_DIM1 ", UInt(_BundleDimensions[[1]]);', + ' println "PTO_DIAG_DIM2 ", UInt(_BundleDimensions[[2]]);', + ' let diagnostic_tile_operation =', + ' BundleTileOperationSelected() &&', + ' _BundleOperation.data_type_valid;', + ' println "PTO_DIAG_TILE_OPERATION_SELECTED ",', + ' if diagnostic_tile_operation then 1 else 0;', + ' if diagnostic_tile_operation then', + ' println "PTO_DIAG_DATA_TYPE_CODE ",', + ' UInt(CurrentBundleTileOperationDataTypeCode());', + ' println "PTO_DIAG_DATR_PRESENT ",', + ' if _BundleDataAttributesPresent then 1 else 0;', + ' println "PTO_DIAG_DATR_CMODE ",', + ' UInt(_BundleDataAttributes.comparison_mode);', + ' println "PTO_DIAG_DATR_PAD ",', + ' UInt(_BundleDataAttributes.pad_value);', + ' println "PTO_DIAG_DATR_SAT ",', + ' if _BundleDataAttributes.saturating then 1 else 0;', + ' println "PTO_DIAG_DATR_CANON ",', + ' if _BundleDataAttributes.canonicalize then 1 else 0;', + ' println "PTO_DIAG_DATR_TYPE ",', + ' UInt(_BundleDataAttributes.data_type);', + ' println "PTO_DIAG_DATR_RMODE ",', + ' UInt(_BundleDataAttributes.rounding_mode);', + ' println "PTO_DIAG_DATR_LAYOUT ",', + ' UInt(_BundleDataAttributes.data_layout);', + ' println "PTO_DIAG_DIMENSIONS_LEGAL ",', + ' if BundleMGATHERDimensionsLegal() then 1 else 0;', + ' println "PTO_DIAG_MASKS_LEGAL ",', + ' if SelectedBundleTileMasksLegal() then 1 else 0;', + ' let diagnostic_family = BundleTileDecodeFamily(', + ' _BundleOperation.operation_class);', + ' let diagnostic_code = BundleOperationDecodeCode(', + ' _BundleOperation);', + ' let diagnostic_decoded = DecodeTileOperation(', + ' diagnostic_family, diagnostic_code);', + ' println "PTO_DIAG_DECODED_OPERATION ", diagnostic_decoded;', + ' if diagnostic_decoded != PTO_TILE_OPERATION_COUNT then', + ' let diagnostic_operation = diagnostic_decoded as', + ' integer {0..PTO_TILE_OPERATION_COUNT-1};', + ' println "PTO_DIAG_BINDINGS_COMPLETE ",', + ' if BundleOperationBindingsComplete(', + ' diagnostic_operation) then 1 else 0;', + ' println "PTO_DIAG_GPR_BINDINGS_LEGAL ",', + ' if BundleOperationGPRBindingValuesLegal(', + ' diagnostic_operation) then 1 else 0;', + ' end;', + ' println "PTO_DIAG_MSCATTER_BINDINGS_LEGAL ",', + ' if BundleMSCATTERBindingsLegal() then 1 else 0;', + ' if BundleTileBindingCount() > 0 then', + ' println "PTO_DIAG_BINDING_DEST_VALID ",', + ' if _BundleTileBindings[[0]].destination_valid then 1 else 0;', + ' println "PTO_DIAG_BINDING_SOURCE0_VALID ",', + ' if _BundleTileBindings[[0]].source0_valid then 1 else 0;', + ' println "PTO_DIAG_BINDING_SOURCE1_VALID ",', + ' if _BundleTileBindings[[0]].source1_valid then 1 else 0;', + ' println "PTO_DIAG_BINDING_LAST ",', + ' if _BundleTileBindings[[0]].last then 1 else 0;', + ' println "PTO_DIAG_BINDING_ASSEMBLE_VALID ",', + ' if _BundleTileBindings[[0]].destination_assemble.valid then 1 else 0;', + ' println "PTO_DIAG_BINDING_ASSEMBLE_INIT ",', + ' if _BundleTileBindings[[0]].destination_assemble.init then 1 else 0;', + ' println "PTO_DIAG_BINDING_ASSEMBLE_LAST ",', + ' if _BundleTileBindings[[0]].destination_assemble.last then 1 else 0;', + ' println "PTO_DIAG_BINDING_DEST_SIZE ",', + ' _BundleTileBindings[[0]].destination_size;', + ' println "PTO_DIAG_DEST_CAPACITY_BYTES ",', + ' BundleLocalDestinationAllocationBytes(0);', + ' println "PTO_DIAG_TILE_CAPACITY_LIMIT ",', + ' TileCapacityLimitBytes();', + ' println "PTO_DIAG_TILE_CAPACITY_IN_USE_PE0 ",', + ' TileCapacityInUseForPE(0);', + ' println "PTO_DIAG_DEST_CAPACITY_GROUP_FITS ",', + ' if BundleLocalDestinationCapacityGroupFits()', + ' then 1 else 0;', + ' println "PTO_DIAG_BINDING_DEST_HAND ",', + ' UInt(_BundleTileBindings[[0]].destination_hand);', + ' println "PTO_DIAG_LOCAL_GENERATION_OPEN ",', + ' if BundleLocalGenerationOpenForHand(', + ' UInt(_BundleTileBindings[[0]].destination_hand)', + ' as integer {0..3}) then 1 else 0;', + ' println "PTO_DIAG_BINDING_DEST ",', + ' _BundleTileBindings[[0]].destination;', + ' println "PTO_DIAG_BINDING_SOURCE0 ",', + ' _BundleTileBindings[[0]].source0;', + ' println "PTO_DIAG_BINDING_SOURCE1 ",', + ' _BundleTileBindings[[0]].source1;', + ' if _BundleTileBindings[[0]].source0_valid then', + ' let source0 = _BundleTileBindings[[0]].source0;', + ' println "PTO_DIAG_SOURCE0_ALLOCATED ",', + ' if _Tiles[[source0]].allocated then 1 else 0;', + ' println "PTO_DIAG_SOURCE0_DEFINED ",', + ' if TileSourceContentsDefined(source0) then 1 else 0;', + ' println "PTO_DIAG_SOURCE0_TYPE ",', + ' UInt(TileDataTypeToEncoding(_Tiles[[source0]].data_type));', + ' println "PTO_DIAG_SOURCE0_ROWS ", _Tiles[[source0]].valid_rows;', + ' println "PTO_DIAG_SOURCE0_COLUMNS ", _Tiles[[source0]].valid_columns;', + ' println "PTO_DIAG_SOURCE0_PHYSICAL_COLUMNS ", _Tiles[[source0]].columns;', + ' end;', + ' if _BundleTileBindings[[0]].source1_valid then', + ' let source1 = _BundleTileBindings[[0]].source1;', + ' println "PTO_DIAG_SOURCE1_ALLOCATED ",', + ' if _Tiles[[source1]].allocated then 1 else 0;', + ' println "PTO_DIAG_SOURCE1_DEFINED ",', + ' if TileSourceContentsDefined(source1) then 1 else 0;', + ' println "PTO_DIAG_SOURCE1_TYPE ",', + ' UInt(TileDataTypeToEncoding(_Tiles[[source1]].data_type));', + ' println "PTO_DIAG_SOURCE1_ROWS ", _Tiles[[source1]].valid_rows;', + ' println "PTO_DIAG_SOURCE1_COLUMNS ", _Tiles[[source1]].valid_columns;', + ' println "PTO_DIAG_SOURCE1_PHYSICAL_COLUMNS ", _Tiles[[source1]].columns;', + ' end;', + ' if BundleMGATHERSelected() &&', + ' _BundleDimensionPresent[[0]] &&', + ' UInt(_BundleDimensions[[0]]) > 0 &&', + ' UInt(_BundleDimensions[[0]]) <= 65535 then', + ' let diagnostic_valid_columns =', + ' UInt(_BundleDimensions[[0]]) as', + ' integer {1..65535};', + ' let diagnostic_valid_rows = if', + ' _BundleDimensionPresent[[1]] then', + ' UInt(_BundleDimensions[[1]]) as', + ' integer {1..65535}', + ' else 1;', + ' let diagnostic_columns = if', + ' _BundleDimensionPresent[[2]] then', + ' UInt(_BundleDimensions[[2]]) as', + ' integer {1..65535}', + ' else diagnostic_valid_columns;', + ' let diagnostic_data_type =', + ' TileDataTypeFromEncoding(', + ' CurrentBundleTileOperationDataTypeCode()', + ' as TileDataTypeEncoding);', + ' println "PTO_DIAG_INDEX_TYPE_LEGAL ",', + ' if IndexedTLSUIndexDataTypeLegal(', + ' _Tiles[[_BundleTileBindings[[0]].source0]].data_type)', + ' then 1 else 0;', + ' println "PTO_DIAG_TRANSFER_TYPE_LEGAL ",', + ' if IndexedTLSUTransferDataTypeLegal(', + ' diagnostic_data_type) then 1 else 0;', + ' println "PTO_DIAG_SOURCE_SHAPE_MATCH ",', + ' if _Tiles[[_BundleTileBindings[[0]].source0]].valid_rows ==', + ' diagnostic_valid_rows &&', + ' _Tiles[[_BundleTileBindings[[0]].source0]].valid_columns ==', + ' diagnostic_valid_columns then 1 else 0;', + ' let diagnostic_resolved =', + ' ResolveBundleTileDestinationsWithShapeAndType(', + ' TRUE, diagnostic_valid_rows,', + ' diagnostic_valid_columns, diagnostic_columns,', + ' TRUE, diagnostic_data_type);', + ' println "PTO_DIAG_DEST_RESOLVED ",', + ' if diagnostic_resolved then 1 else 0;', + ' if diagnostic_resolved then', + ' let diagnostic_destination =', + ' _BundleTileBindings[[0]].destination;', + ' println "PTO_DIAG_DEST_DESCRIPTOR_LEGAL ",', + ' if TileDescriptorLegal(diagnostic_destination)', + ' then 1 else 0;', + ' println "PTO_DIAG_DEST_LAYOUT ",', + ' _Tiles[[diagnostic_destination]].layout;', + ' println "PTO_DIAG_DEST_TYPE ",', + ' UInt(TileDataTypeToEncoding(', + ' _Tiles[[diagnostic_destination]].data_type));', + ' println "PTO_DIAG_TILE_OPERANDS_LEGAL ",', + ' if TileOperandsLegal_MGATHER(', + ' diagnostic_destination, Zeros{PTO_XLEN},', + ' ReadPEAbsoluteGPROperand(_CurrentMemoryAgent,', + ' _BundleScalarBindings[[0]].source1),', + ' _BundleTileBindings[[0]].source0,', + ' CurrentBundlePadValue()) then 1 else 0;', + ' RollBackBundleTileDestinations();', + ' end;', + ' end;', + ' end;', + ' end;', + ' else', + ' println "PTO_DIAG_BUNDLE_ACTIVE 0";', + ' end;', + *rejection_diagnostics, + " return 2;", + " end;", + " previous_previous_pc = previous_pc;", + " previous_pc = step_pc;", + f" if ReadTPC() == {_word(configuration.stop_pc)} then", + " model_stop_hits = model_stop_hits + 1;", + f" if model_stop_hits == {configuration.stop_after_hits} then", + f" for result_index = 0 to {configuration.result_size - 1} do" + if configuration.result_size else " pass;", + ]) + if configuration.result_size: + lines.extend([ + ' println "PTO_RESULT_BYTE ", result_index, " ",', + " UInt(ReadPhysicalMemoryByte(" + f" {_word(configuration.result_address)} +" + " NaturalToWord(result_index)));", + " end;", + ]) + lines.extend([ + ' println "PTO_FINAL_TPC ", UInt(ReadTPC());', + " return 0;", + " end;", + " end;", + " end;", + ' println "PTO_STEP_LIMIT";', + " return 3;", + "end;", + "", + ]) + return "\n".join(lines) + + +def specialize_reference_profile(asl_spec: bytes, memory_bytes: int, + tile_elements: int, + *, + fresh_process_reset: bool = False) -> bytes: + """Select bounded hosted storage without changing PTO semantics.""" + if memory_bytes < 256 or memory_bytes > MAX_HOSTED_MEMORY_BYTES: + raise ValueError("hosted memory bound is outside the supported model profile") + if tile_elements < 1 or tile_elements > REFERENCE_TILE_ELEMENTS: + raise ValueError("hosted Tile bound is outside the supported model profile") + replacement = ( + "config PTO_MODEL_MEMORY_BYTES : integer " + f"{{256..{memory_bytes}}} = {memory_bytes};" + ).encode("ascii") + specialized, count = MEMORY_CONFIG_RE.subn(replacement, asl_spec) + if count != 1: + raise ValueError("PTO ASL memory configuration was not found exactly once") + tile_replacement = ( + "config PTO_MODEL_TILE_ELEMENTS : integer " + f"{{1..{REFERENCE_TILE_ELEMENTS}}} = {tile_elements};" + ).encode("ascii") + specialized, count = TILE_CONFIG_RE.subn(tile_replacement, specialized) + if count != 1: + raise ValueError("PTO ASL Tile configuration was not found exactly once") + if fresh_process_reset: + specialized, count = MEMORY_RESET_LOOP_RE.subn( + b" // The hosted runner executes one ELF in a fresh ASLRef " + b"process.\n" + b" // Fresh interpreter storage is already zero; retain full " + b"reset for\n" + b" // every architectural state domain except the redundant " + b"memory sweep.\n" + b" pass;", + specialized, + ) + if count != 1: + raise ValueError( + "PTO ASL memory reset loop was not found exactly once" + ) + return specialized + + +def _load_lock(path: pathlib.Path | None) -> dict[str, object]: + if path is None: + raise ValueError("an exact model lock is required") + value = json.loads(path.read_text(encoding="utf-8")) + if value.get("schema") != "pto-asl-model-lock-v1": + raise ValueError("model lock schema mismatch") + return value + + +def _git_root(path: pathlib.Path) -> pathlib.Path: + candidate = path.resolve() + if candidate.is_file(): + candidate = candidate.parent + for directory in (candidate, *candidate.parents): + if (directory / ".git").exists(): + return directory + raise ValueError(f"cannot resolve a git checkout for {path}") + + +def _git_value(root: pathlib.Path, *arguments: str) -> str: + completed = subprocess.run( + ["git", "-C", str(root), *arguments], + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + check=False, + ) + if completed.returncode != 0: + raise ValueError(completed.stderr.strip() or "git identity query failed") + return completed.stdout.strip() + + +def _file_sha256(path: pathlib.Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def _required_path(path: pathlib.Path, label: str) -> pathlib.Path: + if not path.is_file(): + raise ValueError(f"missing {label}: {path}") + return path + + +def _host_memory_runner( + aslref: pathlib.Path, +) -> tuple[pathlib.Path, dict[str, str]]: + """Build or reuse the model-owned ASLRef host-memory executable.""" + aslref_root = _git_root(aslref) + asllib = aslref_root / "_build" / "default" / "asllib" + cmxa = _required_path(asllib / "asllib.cmxa", "ASLRef asllib.cmxa") + byte_cmi = asllib / ".asllib.objs" / "byte" + native_cmi = asllib / ".asllib.objs" / "native" + if not byte_cmi.is_dir() or not native_cmi.is_dir(): + raise ValueError("missing ASLRef native interface directories") + source = _required_path( + HOST_MEMORY_RUNNER_SOURCE, "host-memory runner source" + ) + opam = shutil.which("opam") + if opam is None: + raise ValueError("opam is required to build the host-memory runner") + prefix_query = subprocess.run( + [opam, "var", "prefix"], + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + check=False, + ) + if prefix_query.returncode != 0: + raise ValueError( + prefix_query.stderr.strip() or "cannot resolve the opam prefix" + ) + opam_prefix = pathlib.Path(prefix_query.stdout.strip()) + ocamlopt = _required_path( + opam_prefix / "bin" / "ocamlopt", "opam ocamlopt" + ) + zarith = opam_prefix / "lib" / "zarith" + menhir = opam_prefix / "lib" / "menhirLib" + dependencies = ( + _required_path(zarith / "zarith.cmxa", "zarith.cmxa"), + _required_path(menhir / "menhirLib.cmxa", "menhirLib.cmxa"), + ) + compiler_version = subprocess.run( + [str(ocamlopt), "-version"], + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + check=True, + ).stdout.strip() + identity = { + "schema": HOST_MEMORY_RUNNER_SCHEMA, + "aslref_commit": _git_value(aslref_root, "rev-parse", "HEAD"), + "asllib_sha256": _file_sha256(cmxa), + "source_sha256": _file_sha256(source), + "ocaml_version": compiler_version, + } + cache_key = hashlib.sha256( + json.dumps(identity, sort_keys=True).encode("utf-8") + ).hexdigest() + cache_root = pathlib.Path( + os.environ.get( + "PTO_ASL_MODEL_CACHE", + pathlib.Path.home() / ".cache" / "pto-asl-model", + ) + ).expanduser() + target = cache_root / "host-memory-runner" / cache_key + executable = target / "aslref-host-memory" + metadata = target / "identity.json" + if executable.is_file() and os.access(executable, os.X_OK) and metadata.is_file(): + try: + if json.loads(metadata.read_text(encoding="utf-8")) == identity: + return executable, identity + except (OSError, json.JSONDecodeError): + pass + + target.mkdir(parents=True, exist_ok=True) + with tempfile.TemporaryDirectory(prefix="build-", dir=target) as directory: + build = pathlib.Path(directory) + build_source = build / source.name + shutil.copy2(source, build_source) + temporary_executable = build / executable.name + command = [str(ocamlopt)] + gmp_directories = [ + pathlib.Path("/opt/homebrew/lib"), + pathlib.Path.home() / ".local" / "lib", + pathlib.Path("/usr/lib/x86_64-linux-gnu"), + ] + gmp_directory = next( + (item for item in gmp_directories + if (item / "libgmp.a").is_file() + or (item / "libgmp.so").is_file() + or (item / "libgmp.dylib").is_file()), + None, + ) + if gmp_directory is not None: + command.extend(("-ccopt", "-L" + str(gmp_directory))) + if sys.platform == "darwin": + command.extend(("-cclib", "-Wl,-stack_size,0x20000000")) + for include in (byte_cmi, native_cmi, zarith, menhir): + command.extend(("-I", str(include))) + command.extend(( + "-o", str(temporary_executable), + *(str(item) for item in dependencies), + str(cmxa), str(build_source), + )) + completed = subprocess.run( + command, + cwd=build, + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + check=False, + ) + if completed.returncode != 0 or not temporary_executable.is_file(): + detail = (completed.stderr or completed.stdout).strip() + raise ValueError( + "failed to build the host-memory runner" + + (f": {detail[-4000:]}" if detail else "") + ) + shutil.copy2(temporary_executable, executable) + executable.chmod(0o755) + metadata.write_text( + json.dumps(identity, indent=2, sort_keys=True) + "\n", + encoding="utf-8", + ) + return executable, identity + + +def _verify_identity(configuration: RunConfiguration, + lock: dict[str, object]) -> None: + pto_root = _git_root(configuration.asl_spec) + aslref_root = _git_root(configuration.aslref) + expected = { + "pto_commit": _git_value(pto_root, "rev-parse", "HEAD"), + "pto_tree": _git_value(pto_root, "rev-parse", "HEAD^{tree}"), + "pto_repository": _git_value(pto_root, "remote", "get-url", "origin"), + "aslref_commit": _git_value(aslref_root, "rev-parse", "HEAD"), + "aslref_repository": _git_value( + aslref_root, "remote", "get-url", "origin" + ), + } + for field, actual in expected.items(): + if lock.get(field) != actual: + raise ValueError( + f"model identity mismatch for {field}: " + f"expected {lock.get(field)!r}, got {actual!r}" + ) + pin = (pto_root / ".aslref-version").read_text(encoding="utf-8").strip() + if pin != lock.get("aslref_commit"): + raise ValueError("PTO ASLRef pin does not match model lock") + + +def _object(value: object, label: str) -> dict[str, object]: + if not isinstance(value, dict): + raise ValueError(f"sidecar {label} must be an object") + return value + + +def _text(value: object, label: str) -> str: + if not isinstance(value, str) or not value: + raise ValueError(f"sidecar {label} must be non-empty text") + return value + + +def _natural(value: object, label: str, *, positive: bool = False) -> int: + if not isinstance(value, int) or isinstance(value, bool) or value < 0: + raise ValueError(f"sidecar {label} must be a non-negative integer") + if positive and value == 0: + raise ValueError(f"sidecar {label} must be positive") + return value + + +def _load_sidecar(configuration: RunConfiguration) -> tuple[ + RunConfiguration, dict[str, object] | None, str | None]: + if configuration.sidecar is None: + return configuration, None, None + content = configuration.sidecar.read_bytes() + document = _object(json.loads(content), "root") + if document.get("schema") != SIDECAR_SCHEMA: + raise ValueError("sidecar schema mismatch") + model = _object(document.get("model"), "model") + execution = _object(document.get("execution"), "execution") + start = _object(document.get("start"), "start") + result = _object(document.get("result"), "result") + configured = dataclasses.replace( + configuration, + memory_bytes=_natural(model.get("memory_bytes"), "model.memory_bytes", positive=True), + tile_elements=_natural(model.get("tile_elements"), "model.tile_elements", positive=True), + runtime_typecheck=_text( + model.get("runtime_typecheck", "minimal"), "model.runtime_typecheck" + ), + stop_pc=_natural(execution.get("stop_pc"), "execution.stop_pc"), + stop_after_hits=_natural( + execution.get("stop_after_hits"), "execution.stop_after_hits", positive=True + ), + max_steps=_natural(execution.get("max_steps"), "execution.max_steps", positive=True), + stack_top=_natural(execution.get("stack_top"), "execution.stack_top"), + start_pc=_natural(start.get("pc"), "start.pc"), + return_pc=_natural(start.get("return_pc"), "start.return_pc"), + result_address=_natural(result.get("address"), "result.address"), + result_size=_natural(result.get("size"), "result.size", positive=True), + ) + return configured, document, hashlib.sha256(content).hexdigest() + + +def _unique_symbol(image: ElfImage, name: str) -> ElfSymbol: + matches = [symbol for symbol in image.symbols if symbol.name == name] + if len(matches) != 1: + raise ValueError(f"ELF must contain exactly one {name!r} symbol") + return matches[0] + + +def _validate_sidecar(configuration: RunConfiguration, image: ElfImage, + lock: dict[str, object], document: dict[str, object]) -> None: + elf = _object(document.get("elf"), "elf") + if pathlib.Path(_text(elf.get("path"), "elf.path")).name != configuration.elf.name: + raise ValueError("sidecar ELF path does not match the selected ELF") + if _text(elf.get("sha256"), "elf.sha256") != image.sha256: + raise ValueError("sidecar ELF hash mismatch") + if _natural(elf.get("machine"), "elf.machine") != PTO_ELF_MACHINE: + raise ValueError("sidecar ELF machine mismatch") + if _natural(elf.get("entry"), "elf.entry") != image.entry: + raise ValueError("sidecar ELF entry mismatch") + expected_segments = [ + { + "address": segment.address, + "filesz": len(segment.data), + "memsz": segment.memory_size, + "flags": segment.flags, + } + for segment in image.segments + ] + if elf.get("segments") != expected_segments: + raise ValueError("sidecar PT_LOAD records mismatch") + + identity = _object(document.get("identity"), "identity") + if identity.get("pto_commit") != lock.get("pto_commit"): + raise ValueError("sidecar PTO identity mismatch") + model = _object(document.get("model"), "model") + if model.get("profile") != "bounded-reference-v1" or model.get("pe_count") != 1: + raise ValueError("unsupported sidecar model profile or PE count") + + start = _object(document.get("start"), "start") + start_symbol_name = _text(start.get("symbol"), "start.symbol") + return_symbol_name = _text(start.get("return_symbol"), "start.return_symbol") + if _unique_symbol(image, start_symbol_name).value != configuration.start_pc: + raise ValueError("sidecar start symbol mismatch") + if _unique_symbol(image, return_symbol_name).value != configuration.return_pc: + raise ValueError("sidecar return symbol mismatch") + + execution = _object(document.get("execution"), "execution") + stop_symbol_name = _text(execution.get("stop_symbol"), "execution.stop_symbol") + if _unique_symbol(image, stop_symbol_name).value != configuration.stop_pc: + raise ValueError("sidecar stop symbol mismatch") + + result = _object(document.get("result"), "result") + result_symbol_name = _text(result.get("symbol"), "result.symbol") + size_symbol_name = _text(result.get("size_symbol"), "result.size_symbol") + result_symbol = _unique_symbol(image, result_symbol_name) + size_symbol = _unique_symbol(image, size_symbol_name) + if (result_symbol.value != configuration.result_address + or result_symbol.size != configuration.result_size): + raise ValueError("sidecar result symbol mismatch") + if (size_symbol.section_index != SECTION_INDEX_ABSOLUTE + or size_symbol.value != configuration.result_size): + raise ValueError("sidecar result-size symbol mismatch") + writable_result = any( + segment.address <= configuration.result_address + and configuration.result_address + configuration.result_size <= segment.end + and segment.flags & PROGRAM_FLAG_WRITE + for segment in image.segments + ) + if not writable_result: + raise ValueError("sidecar result range is not in one writable PT_LOAD") + + golden = _object(result.get("golden"), "result.golden") + golden_path = configuration.sidecar.parent / _text( + golden.get("path"), "result.golden.path" + ) + golden_content = golden_path.read_bytes() + if len(golden_content) != configuration.result_size: + raise ValueError("golden result size mismatch") + if hashlib.sha256(golden_content).hexdigest() != _text( + golden.get("sha256"), "result.golden.sha256"): + raise ValueError("golden result hash mismatch") + + +def parse_result(stdout: str, result_size: int) -> tuple[bytes, int]: + result = bytearray(result_size) + seen: set[int] = set() + final_tpc: int | None = None + for line in stdout.splitlines(): + result_match = RESULT_RE.fullmatch(line.strip()) + if result_match: + index = int(result_match.group(1)) + value = int(result_match.group(2)) + if index >= result_size or value > 255 or index in seen: + raise ValueError("malformed or duplicate result byte") + result[index] = value + seen.add(index) + tpc_match = FINAL_TPC_RE.fullmatch(line.strip()) + if tpc_match: + if final_tpc is not None: + raise ValueError("duplicate final TPC marker") + final_tpc = int(tpc_match.group(1)) + if len(seen) != result_size or final_tpc is None: + raise ValueError("ASLRef output is missing result markers") + return bytes(result), final_tpc + + +def run(configuration: RunConfiguration) -> dict[str, object]: + run_started = time.perf_counter() + configuration, sidecar_document, sidecar_sha256 = _load_sidecar(configuration) + image = parse_elf(configuration.elf, configuration.memory_bytes) + lock = _load_lock(configuration.lock) + _verify_identity(configuration, lock) + if sidecar_document is not None: + _validate_sidecar(configuration, image, lock, sidecar_document) + harness = build_harness(image, configuration) + if configuration.runtime_typecheck not in {"strict", "minimal"}: + raise ValueError("runtime_typecheck must be strict or minimal") + if configuration.memory_backend not in {"host-sparse", "reference-array"}: + raise ValueError("memory_backend must be host-sparse or reference-array") + typecheck_option = ( + "--type-check-strict" + if configuration.runtime_typecheck == "strict" + else "--no-type-check" + ) + aslref_executable = configuration.aslref + runner_backend = "aslref-reference-array-v1" + runner_identity: dict[str, str] | None = None + if (configuration.memory_backend == "host-sparse" + and configuration.runtime_typecheck == "minimal"): + aslref_executable, runner_identity = _host_memory_runner( + configuration.aslref + ) + runner_backend = HOST_MEMORY_RUNNER_SCHEMA + aslref_started = time.perf_counter() + with tempfile.TemporaryDirectory(prefix="pto-asl-model-") as directory: + combined = pathlib.Path(directory) / "model.asl" + combined.write_bytes( + specialize_reference_profile( + configuration.asl_spec.read_bytes(), + configuration.memory_bytes, + configuration.tile_elements, + fresh_process_reset=True, + ) + + b"\n" + + harness.encode("utf-8") + ) + completed = subprocess.run( + [ + "/bin/sh", + "-c", + 'stack_limit=$(ulimit -H -s); ulimit -s "$stack_limit"; exec "$@"', + "pto-aslref", + str(aslref_executable), + typecheck_option, + str(combined), + ], + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + check=False, + ) + aslref_elapsed_ms = (time.perf_counter() - aslref_started) * 1000.0 + if completed.returncode != 0: + diagnostics = "\n".join( + part for part in (completed.stdout.strip(), completed.stderr.strip()) + if part + ) + raise RuntimeError( + f"ASLRef execution failed with {completed.returncode} " + f"after {aslref_elapsed_ms:.3f} ms: " + + diagnostics + ) + result, final_tpc = parse_result(completed.stdout, configuration.result_size) + manifest: dict[str, object] = { + "schema": "pto-asl-model-run-v1", + "status": "passed", + "elf": { + "path": configuration.elf.name, + "sha256": image.sha256, + "entry": image.entry, + "segments": [ + { + "address": segment.address, + "filesz": len(segment.data), + "memsz": segment.memory_size, + "flags": segment.flags, + } + for segment in image.segments + ], + }, + "stop_policy": { + "stop_pc": configuration.stop_pc, + "stop_after_hits": configuration.stop_after_hits, + "max_steps": configuration.max_steps, + }, + "start_policy": { + "start_pc": configuration.start_pc or image.entry, + "return_pc": configuration.return_pc, + "mode": "direct-boot" if configuration.start_pc else "elf-entry", + }, + "model_profile": { + "memory_bytes": configuration.memory_bytes, + "tile_elements": configuration.tile_elements, + "memory_storage": ( + "host-sparse-byte-map" + if runner_identity is not None + else "bounded-reference-array" + ), + "runner_backend": runner_backend, + "runtime_typecheck": configuration.runtime_typecheck, + "reset_policy": "fresh-process-zero-initial-memory", + }, + "final_tpc": final_tpc, + "result": { + "address": configuration.result_address, + "size": configuration.result_size, + "bytes_hex": result.hex(), + "sha256": hashlib.sha256(result).hexdigest(), + }, + "identity": lock, + "host_timing_ms": { + "preflight": round((aslref_started - run_started) * 1000.0, 3), + "aslref": round(aslref_elapsed_ms, 3), + "total": round((time.perf_counter() - run_started) * 1000.0, 3), + }, + } + if sidecar_document is not None: + manifest["sidecar"] = { + "path": configuration.sidecar.name, + "sha256": sidecar_sha256, + "case_id": _text(sidecar_document.get("case_id"), "case_id"), + } + if runner_identity is not None: + manifest["runner_identity"] = runner_identity + if configuration.manifest_output is not None: + configuration.manifest_output.write_text( + json.dumps(manifest, indent=2, sort_keys=True) + "\n", + encoding="utf-8", + ) + if configuration.result_output is not None: + configuration.result_output.write_bytes(result) + return manifest + + +def _integer(text: str) -> int: + return int(text, 0) + + +def main(argv: Sequence[str] | None = None) -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--asl-spec", required=True, type=pathlib.Path) + parser.add_argument("--aslref", required=True, type=pathlib.Path) + parser.add_argument("--elf", required=True, type=pathlib.Path) + parser.add_argument("--sidecar", type=pathlib.Path) + parser.add_argument("--stop-pc", type=_integer, default=0) + parser.add_argument("--stop-after-hits", type=int, default=1) + parser.add_argument("--start-pc", type=_integer, default=0) + parser.add_argument("--return-pc", type=_integer, default=0) + parser.add_argument("--max-steps", type=int, default=0) + parser.add_argument("--result-address", type=_integer, default=0) + parser.add_argument("--result-size", type=int, default=0) + parser.add_argument( + "--memory-bytes", type=_integer, default=REFERENCE_MEMORY_BYTES + ) + parser.add_argument( + "--tile-elements", type=int, default=REFERENCE_TILE_ELEMENTS + ) + parser.add_argument( + "--runtime-typecheck", choices=("strict", "minimal"), default="strict" + ) + parser.add_argument( + "--memory-backend", + choices=("host-sparse", "reference-array"), + default="host-sparse", + ) + parser.add_argument("--stack-top", type=_integer, default=0) + parser.add_argument("--manifest-out", type=pathlib.Path) + parser.add_argument("--result-out", type=pathlib.Path) + parser.add_argument("--quiet", action="store_true") + parser.add_argument("--lock", required=True, type=pathlib.Path) + arguments = parser.parse_args(argv) + manifest = run(RunConfiguration( + asl_spec=arguments.asl_spec, + aslref=arguments.aslref, + elf=arguments.elf, + sidecar=arguments.sidecar, + stop_pc=arguments.stop_pc, + stop_after_hits=arguments.stop_after_hits, + start_pc=arguments.start_pc, + return_pc=arguments.return_pc, + max_steps=arguments.max_steps, + result_address=arguments.result_address, + result_size=arguments.result_size, + memory_bytes=arguments.memory_bytes, + tile_elements=arguments.tile_elements, + runtime_typecheck=arguments.runtime_typecheck, + stack_top=arguments.stack_top, + manifest_output=arguments.manifest_out, + result_output=arguments.result_out, + lock=arguments.lock, + memory_backend=arguments.memory_backend, + )) + if not arguments.quiet: + print(json.dumps(manifest, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/abi_c.c b/tests/abi_c.c new file mode 100644 index 0000000..f6c638e --- /dev/null +++ b/tests/abi_c.c @@ -0,0 +1,9 @@ +#include "pto/pto_asl_model.h" + +int main(void) +{ + pto_model_elf_run_config_t config = {0}; + config.abi_version = PTO_ASL_MODEL_ABI_VERSION; + config.struct_size = sizeof(config); + return config.abi_version == 0 ? 1 : 0; +} diff --git a/tests/abi_cpp.cpp b/tests/abi_cpp.cpp new file mode 100644 index 0000000..260f8f9 --- /dev/null +++ b/tests/abi_cpp.cpp @@ -0,0 +1,10 @@ +#include "pto/pto_asl_model.h" + +#include + +static_assert(std::is_standard_layout_v); + +int main() +{ + return PTO_ASL_MODEL_ABI_VERSION == 0 ? 1 : 0; +} diff --git a/tests/client_test.cpp b/tests/client_test.cpp new file mode 100644 index 0000000..ce854aa --- /dev/null +++ b/tests/client_test.cpp @@ -0,0 +1,55 @@ +#include "pto/pto_asl_model.h" + +namespace { + +pto_model_elf_run_config_t ValidConfig(const char *runner) +{ + pto_model_elf_run_config_t config{}; + config.abi_version = PTO_ASL_MODEL_ABI_VERSION; + config.struct_size = sizeof(config); + config.runner_path = runner; + config.asl_spec_path = "spec.asl"; + config.aslref_path = "aslref"; + config.elf_path = "case.elf"; + config.sidecar_path = nullptr; + config.manifest_output_path = "manifest.json"; + config.stop_pc = 4; + config.max_steps = 1; + config.memory_bytes = 65536; + config.tile_elements = 32768; + config.stop_after_hits = 1; + config.start_pc = 0; + config.return_pc = 0; + return config; +} + +} // namespace + +int main() +{ + if (pto_model_run_elf(nullptr) != PTO_MODEL_STATUS_INVALID_ARGUMENT) { + return 1; + } + + auto mismatch = ValidConfig("/usr/bin/true"); + mismatch.abi_version = 0; + if (pto_model_run_elf(&mismatch) != PTO_MODEL_STATUS_ABI_MISMATCH) { + return 2; + } + + auto success = ValidConfig("/usr/bin/true"); + if (pto_model_run_elf(&success) != PTO_MODEL_STATUS_OK) { + return 3; + } + + auto failure = ValidConfig("/usr/bin/false"); + if (pto_model_run_elf(&failure) != PTO_MODEL_STATUS_WORKER_FAILED) { + return 4; + } + + auto missing = ValidConfig("/path/that/does/not/exist"); + if (pto_model_run_elf(&missing) != PTO_MODEL_STATUS_WORKER_LAUNCH_ERROR) { + return 5; + } + return 0; +} diff --git a/tests/test_runner.py b/tests/test_runner.py new file mode 100644 index 0000000..89829ab --- /dev/null +++ b/tests/test_runner.py @@ -0,0 +1,381 @@ +from __future__ import annotations + +import io +import hashlib +import json +import pathlib +import struct +import tempfile +import unittest +from contextlib import redirect_stdout +from unittest import mock + +from pto_asl_model.runner import ( + ELF_HEADER, + PROGRAM_HEADER, + SECTION_HEADER, + SYMBOL_ENTRY, + ElfError, + RunConfiguration, + build_harness, + main, + parse_elf, + parse_result, + specialize_reference_profile, + _load_sidecar, + _validate_sidecar, +) + + +def make_elf(path: pathlib.Path, *, machine: int = 0xE9, + address: int = 0x100, payload: bytes = b"\x16\x00") -> None: + identification = bytearray(16) + identification[:4] = b"\x7fELF" + identification[4] = 2 + identification[5] = 1 + identification[6] = 1 + program_offset = ELF_HEADER.size + file_offset = ELF_HEADER.size + PROGRAM_HEADER.size + header = ELF_HEADER.pack( + bytes(identification), 2, machine, 1, address, program_offset, 0, 0, + ELF_HEADER.size, PROGRAM_HEADER.size, 1, 0, 0, 0, + ) + program = PROGRAM_HEADER.pack( + 1, 5, file_offset, address, address, len(payload), len(payload) + 2, 1, + ) + path.write_bytes(header + program + payload) + + +def make_symbol_elf(path: pathlib.Path) -> None: + identification = bytearray(16) + identification[:4] = b"\x7fELF" + identification[4:7] = b"\x02\x01\x01" + program_offset = ELF_HEADER.size + file_offset = ELF_HEADER.size + PROGRAM_HEADER.size + payload = b"\x16\x00\x00\x00" + strings = ( + b"\0main\0cross_model_stop\0cross_model_result\0" + b"cross_model_result_size\0" + ) + offsets = { + "main": strings.index(b"main"), + "cross_model_stop": strings.index(b"cross_model_stop"), + "cross_model_result": strings.index(b"cross_model_result"), + "cross_model_result_size": strings.index(b"cross_model_result_size"), + } + symbol_offset = file_offset + len(payload) + symbols = b"".join([ + SYMBOL_ENTRY.pack(0, 0, 0, 0, 0, 0), + SYMBOL_ENTRY.pack(offsets["main"], 0x12, 0, 1, 0x100, 0), + SYMBOL_ENTRY.pack(offsets["cross_model_stop"], 0x10, 0, 1, 0x102, 0), + SYMBOL_ENTRY.pack(offsets["cross_model_result"], 0x11, 0, 1, 0x200, 8192), + SYMBOL_ENTRY.pack( + offsets["cross_model_result_size"], 0x10, 0, 0xFFF1, 8192, 0 + ), + ]) + string_offset = symbol_offset + len(symbols) + section_offset = string_offset + len(strings) + sections = b"".join([ + SECTION_HEADER.pack(0, 0, 0, 0, 0, 0, 0, 0, 0, 0), + SECTION_HEADER.pack( + 0, 2, 0, 0, symbol_offset, len(symbols), 2, 1, 8, SYMBOL_ENTRY.size + ), + SECTION_HEADER.pack(0, 3, 0, 0, string_offset, len(strings), 0, 0, 1, 0), + ]) + header = ELF_HEADER.pack( + bytes(identification), 2, 0xE9, 1, 0x100, program_offset, + section_offset, 0, ELF_HEADER.size, PROGRAM_HEADER.size, 1, + SECTION_HEADER.size, 3, 0, + ) + program = PROGRAM_HEADER.pack( + 1, 7, file_offset, 0x100, 0x100, len(payload), 0x2200, 1, + ) + path.write_bytes(header + program + payload + symbols + strings + sections) + + +class RunnerTests(unittest.TestCase): + def test_quiet_cli_suppresses_manifest_stdout(self) -> None: + with mock.patch( + "pto_asl_model.runner.run", return_value={"status": "passed"} + ) as run_mock: + output = io.StringIO() + with redirect_stdout(output): + status = main([ + "--asl-spec", "spec.asl", + "--aslref", "aslref", + "--elf", "case.elf", + "--lock", "pto-lock.json", + "--quiet", + ]) + self.assertEqual(status, 0) + self.assertEqual(output.getvalue(), "") + self.assertEqual( + run_mock.call_args.args[0].memory_backend, "host-sparse" + ) + + def test_host_memory_runner_owns_only_physical_storage(self) -> None: + source = ( + pathlib.Path(__file__).parents[1] + / "src" / "pto_asl_model" / "aslref_host_memory.ml" + ).read_text(encoding="utf-8") + self.assertIn('"ReadPhysicalMemoryByte"', source) + self.assertIn('"WritePhysicalMemoryByte"', source) + self.assertNotIn("DecodeScalar", source) + self.assertNotIn("ExecutePTOInstruction", source) + + def test_parse_static_elf(self) -> None: + with tempfile.TemporaryDirectory() as directory: + path = pathlib.Path(directory) / "case.elf" + make_elf(path) + image = parse_elf(path) + self.assertEqual(image.entry, 0x100) + self.assertEqual(image.segments[0].data, b"\x16\x00") + self.assertEqual(image.segments[0].memory_size, 4) + + def test_rejects_wrong_machine(self) -> None: + with tempfile.TemporaryDirectory() as directory: + path = pathlib.Path(directory) / "case.elf" + make_elf(path, machine=1) + with self.assertRaisesRegex(ElfError, "machine"): + parse_elf(path) + + def test_high_address_uses_explicit_hosted_memory_bound(self) -> None: + with tempfile.TemporaryDirectory() as directory: + path = pathlib.Path(directory) / "case.elf" + make_elf(path, address=0x111AC) + with self.assertRaisesRegex(ElfError, "reference memory"): + parse_elf(path) + image = parse_elf(path, memory_bytes=0x20000) + self.assertEqual(image.entry, 0x111AC) + + def test_specializes_reference_memory_bound(self) -> None: + source = ( + b"config PTO_MODEL_MEMORY_BYTES : integer {256..65536} = 4096;\n" + b"config PTO_MODEL_TILE_ELEMENTS : integer {1..32768} = 32768;\n" + ) + self.assertEqual( + specialize_reference_profile(source, 0x20000, 1), + b"config PTO_MODEL_MEMORY_BYTES : integer {256..131072} = 131072;\n" + b"config PTO_MODEL_TILE_ELEMENTS : integer {1..32768} = 1;\n", + ) + + def test_fresh_process_reset_skips_only_memory_sweep(self) -> None: + source = ( + b"config PTO_MODEL_MEMORY_BYTES : integer {256..65536} = 4096;\n" + b"config PTO_MODEL_TILE_ELEMENTS : integer {1..32768} = 32768;\n" + b"implementation func ResetProfileState()\n" + b"begin\n" + b" for index = 0 to PTO_MODEL_MEMORY_BYTES - 1 do\n" + b" _Memory[[index]] = Zeros{8};\n" + b" end;\n" + b" ResetBundleControlState();\n" + b"end;\n" + ) + specialized = specialize_reference_profile( + source, 0x20000, 1, fresh_process_reset=True + ) + self.assertNotIn(b"_Memory[[index]] = Zeros{8}", specialized) + self.assertIn(b"ResetBundleControlState();", specialized) + self.assertIn(b"fresh ASLRef process", specialized) + + def test_fresh_process_reset_fails_closed_on_source_drift(self) -> None: + source = ( + b"config PTO_MODEL_MEMORY_BYTES : integer {256..65536} = 4096;\n" + b"config PTO_MODEL_TILE_ELEMENTS : integer {1..32768} = 32768;\n" + ) + with self.assertRaisesRegex(ValueError, "memory reset loop"): + specialize_reference_profile( + source, 0x20000, 1, fresh_process_reset=True + ) + + def test_runtime_typecheck_mode_is_explicit(self) -> None: + with tempfile.TemporaryDirectory() as directory: + path = pathlib.Path(directory) / "case.elf" + make_elf(path) + image = parse_elf(path) + configuration = RunConfiguration( + asl_spec=path, + aslref=path, + elf=path, + stop_pc=0x102, + max_steps=4, + result_address=0, + result_size=0, + runtime_typecheck="minimal", + ) + self.assertIn("ExecuteNextPTOInstruction()", build_harness(image, configuration)) + + def test_harness_executes_consecutive_steps(self) -> None: + with tempfile.TemporaryDirectory() as directory: + path = pathlib.Path(directory) / "case.elf" + make_elf(path) + image = parse_elf(path) + harness = build_harness(image, RunConfiguration( + asl_spec=path, + aslref=path, + elf=path, + stop_pc=0x102, + max_steps=4, + result_address=0x100, + result_size=2, + )) + self.assertIn("ExecuteNextPTOInstruction()", harness) + self.assertIn("for model_step = 0 to 3", harness) + self.assertIn("model_stop_hits == 1", harness) + self.assertIn("PTO_FAULT_STATUS", harness) + self.assertIn("PTO_FAULT_ADDRESS", harness) + self.assertIn("PTO_PREVIOUS_TPC", harness) + self.assertIn("PTO_PREVIOUS_PREVIOUS_TPC", harness) + self.assertIn("PTO_DIAG_SP", harness) + self.assertIn("PTO_DIAG_RA", harness) + self.assertIn("PTO_DIAG_RETURN_ADDRESS", harness) + self.assertIn("PTO_DIAG_BINDINGS_COMPLETE", harness) + self.assertIn("PTO_DIAG_GPR_STRIDE", harness) + self.assertIn("PTO_DIAG_DATR_TYPE", harness) + self.assertIn("PTO_DIAG_TILE_OPERANDS_LEGAL", harness) + self.assertIn("PTO_DIAG_TILE_OPERATION_SELECTED", harness) + self.assertIn( + "if diagnostic_tile_operation then\n" + " println \"PTO_DIAG_DATA_TYPE_CODE \",", + harness, + ) + self.assertNotIn("ExecutePTOInstruction(", harness) + + def test_stop_policy_can_require_a_later_pc_hit(self) -> None: + with tempfile.TemporaryDirectory() as directory: + path = pathlib.Path(directory) / "case.elf" + make_elf(path) + image = parse_elf(path) + harness = build_harness(image, RunConfiguration( + asl_spec=path, + aslref=path, + elf=path, + stop_pc=0x102, + stop_after_hits=2, + max_steps=4, + result_address=0, + result_size=0, + )) + self.assertIn("model_stop_hits == 2", harness) + + def test_direct_boot_initializes_start_and_return_pc(self) -> None: + with tempfile.TemporaryDirectory() as directory: + path = pathlib.Path(directory) / "case.elf" + make_elf(path, payload=b"\x16\x00\x00\x00") + image = parse_elf(path) + harness = build_harness(image, RunConfiguration( + asl_spec=path, + aslref=path, + elf=path, + stop_pc=0x102, + start_pc=0x102, + return_pc=0x104, + stack_top=0x108, + max_steps=4, + result_address=0, + result_size=0, + )) + self.assertIn("WriteTPC(Zeros{PTO_XLEN} + 0x102)", harness) + self.assertIn("_ReturnAddress = Zeros{PTO_XLEN} + 0x104", harness) + self.assertIn( + "WritePEGPR(0, 10, Zeros{PTO_XLEN} + 0x104)", harness + ) + self.assertIn( + "WritePEGPR(0, 1, Zeros{PTO_XLEN} + 0x108)", harness + ) + self.assertIn("PTO_DIAG_STACK_RA", harness) + self.assertIn("PTO_DIAG_STACK_S0", harness) + + def test_verified_sidecar_resolves_elf_symbols(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = pathlib.Path(directory) + elf = root / "case.elf" + golden = root / "case.golden.bin" + sidecar = root / "case.sidecar.json" + make_symbol_elf(elf) + golden.write_bytes(bytes(8192)) + image = parse_elf(elf) + document = { + "schema": "pto-asl-elf-sidecar-v1", + "case_id": "scalar.case", + "identity": {"pto_commit": "pto-commit"}, + "elf": { + "path": elf.name, + "sha256": image.sha256, + "machine": 0xE9, + "entry": image.entry, + "segments": [{ + "address": 0x100, + "filesz": 4, + "memsz": 0x2200, + "flags": 7, + }], + }, + "model": { + "profile": "bounded-reference-v1", + "pe_count": 1, + "memory_bytes": 65536, + "tile_elements": 1, + "runtime_typecheck": "minimal", + }, + "start": { + "symbol": "main", + "pc": 0x100, + "return_symbol": "cross_model_stop", + "return_pc": 0x102, + }, + "execution": { + "stop_symbol": "cross_model_stop", + "stop_pc": 0x102, + "stop_after_hits": 1, + "max_steps": 8, + "stack_top": 0x4000, + }, + "result": { + "symbol": "cross_model_result", + "size_symbol": "cross_model_result_size", + "address": 0x200, + "size": 8192, + "segments": [{ + "offset": 0, + "size": 8192, + "dtype": "opaque-bytes", + "shape": [8192], + "comparison": "exact", + }], + "golden": { + "path": golden.name, + "sha256": hashlib.sha256(golden.read_bytes()).hexdigest(), + }, + }, + } + sidecar.write_text(json.dumps(document), encoding="utf-8") + configuration, loaded, digest = _load_sidecar(RunConfiguration( + asl_spec=elf, + aslref=elf, + elf=elf, + stop_pc=0, + max_steps=0, + result_address=0, + result_size=0, + sidecar=sidecar, + )) + self.assertEqual(configuration.start_pc, 0x100) + self.assertEqual(configuration.result_size, 8192) + self.assertEqual(digest, hashlib.sha256(sidecar.read_bytes()).hexdigest()) + assert loaded is not None + _validate_sidecar( + configuration, image, {"pto_commit": "pto-commit"}, loaded + ) + + def test_result_markers_are_exact(self) -> None: + result, final_tpc = parse_result( + "PTO_RESULT_BYTE 0 25\nPTO_RESULT_BYTE 1 0\nPTO_FINAL_TPC 276\n", + 2, + ) + self.assertEqual(result, b"\x19\x00") + self.assertEqual(final_tpc, 276) + + +if __name__ == "__main__": + unittest.main() diff --git a/tools/pto-model-run.cpp b/tools/pto-model-run.cpp new file mode 100644 index 0000000..4f9c1d8 --- /dev/null +++ b/tools/pto-model-run.cpp @@ -0,0 +1,63 @@ +#include "pto/pto_asl_model.h" + +#include +#include +#include +#include + +namespace { + +bool ParseInteger(const char *text, std::uint64_t *value) +{ + errno = 0; + char *end = nullptr; + const unsigned long long parsed = std::strtoull(text, &end, 0); + if (errno != 0 || end == text || *end != '\0') { + return false; + } + *value = static_cast(parsed); + return true; +} + +} // namespace + +int main(int argc, char **argv) +{ + if (argc != 19) { + std::cerr + << "usage: pto-model-run RUNNER ASL_SPEC ASLREF LOCK ELF SIDECAR MANIFEST " + "RESULT STOP_PC MAX_STEPS RESULT_ADDRESS RESULT_SIZE STACK_TOP " + "MEMORY_BYTES TILE_ELEMENTS STOP_AFTER_HITS START_PC RETURN_PC\n"; + return 2; + } + pto_model_elf_run_config_t config{}; + config.abi_version = PTO_ASL_MODEL_ABI_VERSION; + config.struct_size = sizeof(config); + config.runner_path = argv[1]; + config.asl_spec_path = argv[2]; + config.aslref_path = argv[3]; + config.lock_path = argv[4]; + config.elf_path = argv[5]; + config.sidecar_path = argv[6]; + config.manifest_output_path = argv[7]; + config.result_output_path = argv[8]; + if (!ParseInteger(argv[9], &config.stop_pc) || + !ParseInteger(argv[10], &config.max_steps) || + !ParseInteger(argv[11], &config.result_address) || + !ParseInteger(argv[12], &config.result_size) || + !ParseInteger(argv[13], &config.stack_top) || + !ParseInteger(argv[14], &config.memory_bytes) || + !ParseInteger(argv[15], &config.tile_elements) || + !ParseInteger(argv[16], &config.stop_after_hits) || + !ParseInteger(argv[17], &config.start_pc) || + !ParseInteger(argv[18], &config.return_pc)) { + std::cerr << "invalid integer argument\n"; + return 2; + } + const pto_model_status_t status = pto_model_run_elf(&config); + if (status != PTO_MODEL_STATUS_OK) { + std::cerr << "PTO ASL model failed with status " << status << '\n'; + return 1; + } + return 0; +}