diff --git a/CMakeLists.txt b/CMakeLists.txt index 5045d7dbd..750349303 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -100,6 +100,8 @@ string(REGEX REPLACE "([][+.*()^$?|\\\\])" "\\\\\\1" prevail_source_dir_escaped file(GLOB_RECURSE prevail_LIB_SRC CONFIGURE_DEPENDS "${prevail_source_dir}/src/*.cpp") list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/main\\.cpp$") +list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/prevail_mcp\\.cpp$") +list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/mcp/.*") list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/test/.*") add_library(prevail ${prevail_LIB_SRC}) @@ -193,6 +195,37 @@ else () RUNTIME_OUTPUT_DIRECTORY "${prevail_binary_dir}") endif () +# MCP server +option(prevail_ENABLE_MCP "Build MCP server" OFF) +if (prevail_ENABLE_MCP) + FetchContent_Declare(nlohmann_json + GIT_REPOSITORY "https://github.com/nlohmann/json.git" + GIT_TAG "v3.12.0" + GIT_SHALLOW ON + ) + FetchContent_MakeAvailable(nlohmann_json) + + file(GLOB prevail_MCP_SRC CONFIGURE_DEPENDS "${prevail_source_dir}/src/mcp/*.cpp") + add_library(prevail_mcp_lib STATIC ${prevail_MCP_SRC}) + target_link_libraries(prevail_mcp_lib PUBLIC prevail nlohmann_json::nlohmann_json) + target_include_directories(prevail_mcp_lib PUBLIC + "${prevail_source_dir}/src" + ) + + add_executable(prevail_mcp "${prevail_source_dir}/src/prevail_mcp.cpp") + target_link_libraries(prevail_mcp PRIVATE prevail_mcp_lib ${CMAKE_DL_LIBS}) + if (CMAKE_CONFIGURATION_TYPES) + set_target_properties(prevail_mcp PROPERTIES + RUNTIME_OUTPUT_DIRECTORY_DEBUG "${prevail_binary_dir}" + RUNTIME_OUTPUT_DIRECTORY_RELEASE "${prevail_binary_dir}" + RUNTIME_OUTPUT_DIRECTORY_RELWITHDEBINFO "${prevail_binary_dir}" + ) + else () + set_target_properties(prevail_mcp PROPERTIES + RUNTIME_OUTPUT_DIRECTORY "${prevail_binary_dir}") + endif () +endif () + # Tests if (prevail_ENABLE_TESTS) FetchContent_Declare(Catch2 @@ -219,6 +252,11 @@ if (prevail_ENABLE_TESTS) target_link_libraries(tests PRIVATE prevail ebpf_yaml_lib bpf_conformance_core Catch2::Catch2WithMain Threads::Threads yaml-cpp::yaml-cpp) + if (prevail_ENABLE_MCP) + target_link_libraries(tests PRIVATE prevail_mcp_lib) + target_compile_definitions(tests PRIVATE PREVAIL_HAS_MCP) + endif () + if (CMAKE_CONFIGURATION_TYPES) set_target_properties(tests run_yaml PROPERTIES RUNTIME_OUTPUT_DIRECTORY_DEBUG "${prevail_binary_dir}" @@ -249,6 +287,7 @@ install(TARGETS prevail libbtf GSL install(DIRECTORY "${prevail_source_dir}/src/" DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/prevail" FILES_MATCHING PATTERN "*.hpp" PATTERN "*.h" + PATTERN "mcp/*" EXCLUDE PATTERN "test/*" EXCLUDE ) diff --git a/README.md b/README.md index 6b771ef6c..519f4c831 100644 --- a/README.md +++ b/README.md @@ -99,6 +99,12 @@ $ bin/prevail ebpf-samples/cilium/bpf_lxc.o 2/1 PASS: 2/1 ``` +### MCP Server + +An MCP server (`prevail_mcp`) exposes the verifier's analysis as structured JSON +tools for LLM agents. Build with `cmake --build build --target prevail_mcp`. +See [src/mcp/README.md](src/mcp/README.md) for details. +
Usage ```text diff --git a/docs/README.md b/docs/README.md index 5f404e455..4e0f94c2b 100644 --- a/docs/README.md +++ b/docs/README.md @@ -14,6 +14,7 @@ This documentation provides a comprehensive guide to understanding the Prevail e | [Memory Model](memory-model.md) | Stack, packet, context, and shared memory handling | | [Type System](type-system.md) | Type domains and type-guided verification | | [Failure Slicing](failure-slicing.md) | Minimal diagnostic slices for verification failures | +| [MCP Server](../src/mcp/README.md) | Structured verification queries for LLM agents | | [Building](building.md) | Build instructions for all platforms | | [Testing](testing.md) | Test infrastructure and conformance testing | | [Glossary](glossary.md) | Terminology and definitions | @@ -94,6 +95,8 @@ Prevail verifies that eBPF programs: ```text src/ ├── main.cpp # CLI entry point +├── mcp/ # MCP server (structured verification queries for LLM agents) +├── prevail_mcp.cpp # MCP server entry point ├── ir/ # Intermediate representation │ ├── syntax.hpp # Instruction definitions │ └── cfg_builder.cpp @@ -127,7 +130,18 @@ src/ When verification fails, you can use an LLM to help diagnose the issue. -**Quick start** (with GitHub Copilot CLI): +**Using the MCP server** (recommended — structured data, no text parsing): + +Build and start `prevail_mcp` (see [MCP Server](../src/mcp/README.md)): + +```bash +cmake --build build --target prevail_mcp +# Add to your MCP client (Copilot CLI: /mcp add, VS Code: .vscode/mcp.json) +``` + +Then ask your LLM: *"Use get_slice to diagnose the verification failure in program.o"* + +**Using prevail with verbose output** (text-based): ```text Using docs/llm-context.md, run ./bin/prevail
-v and diagnose the failure. @@ -138,7 +152,15 @@ Using docs/llm-context.md, run ./bin/prevail
-v and d 2. Copy the contents of `docs/llm-context.md` into your LLM conversation 3. Paste the verification error and ask for diagnosis -See [llm-context.md](llm-context.md) for the context document and [test-data/llm-context-tests.md](../test-data/llm-context-tests.md) for validated test cases. +**Using prevail with failure slicing** (most concise text output): + +```bash +./bin/prevail program.o section --failure-slice +``` + +See [llm-context.md](llm-context.md) for the diagnostic reference, +[test-data/llm-context-tests.md](../test-data/llm-context-tests.md) for validated test cases, +and [MCP Server](../src/mcp/README.md) for the structured query tools. ### Contributing New Failure Patterns diff --git a/docs/llm-context.md b/docs/llm-context.md index e9fc61ed2..dd87e7fe3 100644 --- a/docs/llm-context.md +++ b/docs/llm-context.md @@ -490,6 +490,20 @@ Typical fixes: When analyzing failures, you may need more context. Here's how to request it: +### MCP Server (Recommended for LLM Agents) + +If the `prevail_mcp` MCP server is available, use it for structured queries instead +of parsing text output. The MCP server exposes the same analysis data as `prevail -v` +and `prevail --failure-slice` through JSON tool calls: + +- **`get_slice`** — Backward slice with register relevance (replaces manual `-v` parsing) +- **`get_invariant`** — Query pre/post state at specific PCs +- **`get_instruction`** — Full detail for specific instructions +- **`check_constraint`** — Test hypotheses about the verifier's state +- **`get_source_mapping`** — Map between C source lines and BPF instructions + +See [src/mcp/README.md](../src/mcp/README.md) for the full tool reference. + ### Verbose Output Run with `-v` flag for verbose output showing invariants at each step: @@ -506,6 +520,14 @@ Request the full disassembly to see surrounding instructions: ./bin/prevail
--asm ``` +### Failure Slicing + +Run with `--failure-slice` for a minimal diagnostic showing only causal instructions: + +```bash +./bin/prevail
--failure-slice +``` + ### Specific Invariant Ask the user to share: diff --git a/src/analysis_engine.cpp b/src/analysis_engine.cpp new file mode 100644 index 000000000..f4aa7306a --- /dev/null +++ b/src/analysis_engine.cpp @@ -0,0 +1,268 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#include "analysis_engine.hpp" + +#include +#include +#include +#include + +namespace prevail { + +AnalysisEngine::AnalysisEngine(PlatformOps* ops) : ops_(ops) {} + +bool AnalysisEngine::analysis_options_equal(const prevail::ebpf_verifier_options_t& a, + const prevail::ebpf_verifier_options_t& b) { + return a.cfg_opts.check_for_termination == b.cfg_opts.check_for_termination && + a.allow_division_by_zero == b.allow_division_by_zero && a.strict == b.strict; +} + +bool AnalysisEngine::session_matches(const std::string& elf_path, const std::string& section, + const std::string& program, const std::string& type, + const prevail::ebpf_verifier_options_t& options) const { + if (!session_) { + return false; + } + if (session_->elf_path != elf_path || session_->section != section || session_->program_name != program || + session_type_ != type) { + return false; + } + if (!analysis_options_equal(session_->options, options)) { + return false; + } + // Re-analyze if the file has been modified since last analysis. + try { + return std::filesystem::last_write_time(elf_path) == session_->file_mtime; + } catch (const std::filesystem::filesystem_error&) { + return false; // File no longer accessible — force re-analysis. + } +} + +const prevail::ebpf_verifier_options_t& AnalysisEngine::session_options() const { + if (session_) { + return session_->options; + } + // No session — return platform defaults. Cache to avoid returning a dangling reference. + static thread_local prevail::ebpf_verifier_options_t defaults; + defaults = ops_->default_options(); + return defaults; +} + +std::vector AnalysisEngine::list_programs(const std::string& elf_path) { + return ops_->list_programs(elf_path); +} + +const AnalysisSession& AnalysisEngine::analyze(const std::string& elf_path, const std::string& section, + const std::string& program, const std::string& type, + const prevail::ebpf_verifier_options_t* options) { + // Use caller-provided options or platform defaults. + prevail::ebpf_verifier_options_t effective_options = options ? *options : ops_->default_options(); + + // Reuse the current session if it matches. + if (session_matches(elf_path, section, program, type, effective_options)) { + return *session_; + } + + // Different program or options — discard old session and run fresh analysis. + session_.reset(); + + ops_->prepare_tls(type); + + // Determine target program using the new ElfObject API. + std::string target_section = section; + std::string target_program = program; + if (target_section.empty() && target_program.empty()) { + auto entries = list_programs(elf_path); + for (const auto& entry : entries) { + if (entry.section != ".text") { + target_section = entry.section; + target_program = entry.function; + break; + } + } + if (target_section.empty() && !entries.empty()) { + target_section = entries.front().section; + target_program = entries.front().function; + } + } + + auto tls_guard = std::make_unique(); + + prevail::ElfObject elf(elf_path, effective_options, ops_->platform()); + const auto& raw_progs = elf.get_programs(target_section, target_program); + + if (raw_progs.empty()) { + throw std::runtime_error("Program not found: " + target_program + " in " + elf_path); + } + const auto& found = raw_progs.front(); + + std::vector> notes; + auto prog_or_error = prevail::unmarshal(found, notes, effective_options); + if (auto* err = std::get_if(&prog_or_error)) { + throw std::runtime_error("Unmarshal error: " + *err); + } + auto& inst_seq = std::get(prog_or_error); + + prevail::Program prog = prevail::Program::from_sequence(inst_seq, found.info, effective_options); + prevail::AnalysisResult result = prevail::analyze(prog); + + // Build session with serialized invariants (while TLS is alive). + AnalysisSession session; + session.elf_path = elf_path; + session.section = found.section_name; + session.program_name = found.function_name; + session.options = effective_options; + session.inst_seq = std::move(inst_seq); + session.program = std::move(prog); + session.failed = result.failed; + session.max_loop_count = result.max_loop_count; + session.exit_value = result.exit_value; + session.file_mtime = std::filesystem::last_write_time(elf_path); + + for (const auto& [label, inv_pair] : result.invariants) { + AnalysisSession::SerializedInvariant si; + si.pre_is_bottom = inv_pair.pre.is_bottom(); + try { + if (!si.pre_is_bottom) { + si.pre = inv_pair.pre.to_set(); + } + if (!inv_pair.post.is_bottom()) { + si.post = inv_pair.post.to_set(); + } + } catch (const std::exception& e) { + std::cerr << "prevail: warning: failed to serialize invariant at label " << label.from << ": " + << e.what() << std::endl; + } + if (inv_pair.error.has_value()) { + si.error_message = inv_pair.error->what(); + si.error_label = inv_pair.error->where; + } + session.invariants.emplace(label, std::move(si)); + } + + // Build source maps from BTF line info. + int pc = 0; + for (const auto& [label, inst, line_info] : session.inst_seq) { + if (line_info.has_value()) { + session.pc_to_source[pc] = *line_info; + auto src_key = std::make_pair(line_info->file_name, static_cast(line_info->line_number)); + session.source_to_pcs[src_key].push_back(pc); + } + pc += prevail::size(inst); + } + + // Build PC → Label lookup. + for (const auto& [label, inv] : session.invariants) { + session.pc_to_labels[label.from].push_back(label); + } + + // Keep live state for check_constraint and slicing. + session.live_result = std::move(result); + session.tls_guard = std::move(tls_guard); + + session_ = std::move(session); + session_type_ = type; + return *session_; +} + +// ─── Live session operations ─────────────────────────────────────────────────── + +prevail::ObservationCheckResult +AnalysisEngine::check_constraint(const std::string& elf_path, const std::string& section, const std::string& program, + const std::string& type, const prevail::Label& label, prevail::InvariantPoint point, + const prevail::StringInvariant& observation, const std::string& mode_str) { + // analyze() ensures the session is live. + analyze(elf_path, section, program, type); + + if (mode_str == "proven") { + auto it = session_->live_result->invariants.find(label); + if (it == session_->live_result->invariants.end()) { + return {.ok = false, .message = "No invariant available for label"}; + } + const auto& abstract_state = (point == prevail::InvariantPoint::post) ? it->second.post : it->second.pre; + if (abstract_state.is_bottom()) { + return {.ok = false, .message = "Invariant at label is bottom (unreachable)"}; + } + + const auto observed_state = observation.is_bottom() + ? prevail::EbpfDomain::bottom() + : prevail::EbpfDomain::from_constraints( + observation.value(), prevail::thread_local_options.setup_constraints); + if (observed_state.is_bottom()) { + return {.ok = false, .message = "Observation constraints are unsatisfiable"}; + } + + if (abstract_state <= observed_state) { + return {.ok = true, .message = ""}; + } + return {.ok = false, + .message = "Invariant does not prove the constraint (A ⊑ C is false). " + "The verifier's state includes possibilities outside the observation."}; + } + + prevail::ObservationCheckMode mode; + if (mode_str == "entailed") { + mode = prevail::ObservationCheckMode::entailed; + } else if (mode_str == "consistent") { + mode = prevail::ObservationCheckMode::consistent; + } else { + return {.ok = false, .message = "Unknown mode: " + mode_str}; + } + return session_->live_result->check_observation_at_label(label, point, observation, mode); +} + +prevail::StringInvariant AnalysisEngine::get_live_invariant(const prevail::Label& label, + prevail::InvariantPoint point) const { + if (!session_ || !session_->live_result) { + return prevail::StringInvariant::bottom(); + } + auto it = session_->live_result->invariants.find(label); + if (it == session_->live_result->invariants.end()) { + return prevail::StringInvariant::bottom(); + } + const auto& abstract_state = (point == prevail::InvariantPoint::post) ? it->second.post : it->second.pre; + if (abstract_state.is_bottom()) { + return prevail::StringInvariant::bottom(); + } + return abstract_state.to_set(); +} + +std::vector +AnalysisEngine::compute_failure_slices(const std::string& elf_path, const std::string& section, + const std::string& program, const std::string& type, + const prevail::Program& prog, size_t max_slices, size_t max_steps) { + analyze(elf_path, section, program, type); + + prevail::AnalysisResult::SliceParams params; + params.max_slices = max_slices; + params.max_steps = max_steps; + return session_->live_result->compute_failure_slices(prog, params); +} + +prevail::FailureSlice AnalysisEngine::compute_slice_from_label(const std::string& elf_path, const std::string& section, + const std::string& program, const std::string& type, + const prevail::Program& prog, + const prevail::Label& label, + const prevail::RelevantState& seed, size_t max_steps) { + analyze(elf_path, section, program, type); + + prevail::RelevantState effective_seed = seed; + if (effective_seed.registers.empty() && effective_seed.stack_offsets.empty()) { + for (const auto& a : prog.assertions_at(label)) { + for (const auto& reg : prevail::extract_assertion_registers(a)) { + effective_seed.registers.insert(reg); + } + } + if (effective_seed.registers.empty()) { + auto deps = prevail::extract_instruction_deps(prog.instruction_at(label), prevail::EbpfDomain::top()); + for (const auto& reg : deps.regs_read) { + effective_seed.registers.insert(reg); + } + } + } + + return session_->live_result->compute_slice_from_label(prog, label, effective_seed, max_steps); +} + +} // namespace prevail diff --git a/src/analysis_engine.hpp b/src/analysis_engine.hpp new file mode 100644 index 000000000..87d8a86a2 --- /dev/null +++ b/src/analysis_engine.hpp @@ -0,0 +1,158 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT +#pragma once + +/// @file Analysis engine: runs the PREVAIL pipeline and holds a single live session. + +#include "platform_ops.hpp" + +#ifdef _MSC_VER +#pragma warning(push) +#pragma warning(disable : 4267) // Conversion from 'size_t' to 'int'. +#endif + +#include "cfg/cfg.hpp" +#include "result.hpp" +#include "string_constraints.hpp" + +#ifdef _MSC_VER +#pragma warning(pop) +#endif + +#include +#include +#include +#include +#include +#include + +namespace prevail { + +/// Holds all outputs from a single verification run. +/// The session is always "live" — it retains both pre-serialized invariants +/// (for callers that iterate or display them) and the live AnalysisResult with +/// EbpfDomain objects (for check_constraint and backward slicing). +/// Only one session exists at a time; analyzing a different program discards it. +struct AnalysisSession { + std::string elf_path; + std::string section; + std::string program_name; + + // The verifier options used for this session. + prevail::ebpf_verifier_options_t options; + + // The instruction sequence (labels + instructions + btf_line_info). + prevail::InstructionSeq inst_seq; + + // The CFG program (for instruction_at, assertions_at, cfg navigation). + prevail::Program program; + + // Overall result metadata. + bool failed = false; + int max_loop_count = 0; + prevail::Interval exit_value = prevail::Interval::top(); + + /// Pre-serialized invariant data per label (serialized while TLS is alive). + struct SerializedInvariant { + prevail::StringInvariant pre; + prevail::StringInvariant post; + std::optional error_message; // VerificationError::what(). + std::optional error_label; // VerificationError::where. + bool pre_is_bottom = false; + }; + std::map invariants; + + // Derived: PC → source line info (built from BTF in InstructionSeq). + std::map pc_to_source; + + // Derived: (file, line) → list of PCs. + std::map, std::vector> source_to_pcs; + + // Derived: PC → labels in the invariant map that have this PC as .from. + std::map> pc_to_labels; + + // Live state: TLS guard keeps variable_registry alive for EbpfDomain ops. + // live_result must be declared BEFORE tls_guard so it is destroyed FIRST + // (C++ destroys members in reverse declaration order), ensuring EbpfDomain + // objects are cleaned up while the thread-local state is still valid. + std::optional live_result; + std::unique_ptr tls_guard; + + // File modification time at analysis time (for staleness detection). + std::filesystem::file_time_type file_mtime; +}; + +/// Runs the PREVAIL pipeline and holds a single live session. +/// Re-analyzes when a different program or different options are requested. +class AnalysisEngine { + public: + explicit AnalysisEngine(PlatformOps* ops); + + /// Run analysis on the given ELF file (or return the current session if it + /// matches). Keeps TLS alive so check_constraint and slicing work without + /// re-analyzing. + /// + /// @param options Verifier options. When null, uses platform defaults. + /// Only the fields that affect analysis results + /// (check_for_termination, allow_division_by_zero, strict) + /// are compared for cache invalidation; verbosity and other + /// flags are passed through to the verifier without affecting + /// session caching. + /// @param type Optional program type name override (e.g. "xdp", "bind"). + /// @throws std::runtime_error on ELF parse, unmarshal, or analysis failure. + const AnalysisSession& analyze(const std::string& elf_path, const std::string& section = "", + const std::string& program = "", const std::string& type = "", + const prevail::ebpf_verifier_options_t* options = nullptr); + + /// Check constraints against the live AnalysisResult (re-analyzes if needed). + /// @param mode_str "consistent", "entailed", or "proven". + prevail::ObservationCheckResult check_constraint(const std::string& elf_path, const std::string& section, + const std::string& program, const std::string& type, + const prevail::Label& label, prevail::InvariantPoint point, + const prevail::StringInvariant& observation, + const std::string& mode_str); + + /// Get the invariant at a label from the live session (calls to_set() on demand). + /// @returns StringInvariant::bottom() if no session, label not found, or state is bottom. + prevail::StringInvariant get_live_invariant(const prevail::Label& label, prevail::InvariantPoint point) const; + + /// Compute failure slices from the live session (re-analyzes if needed). + std::vector compute_failure_slices(const std::string& elf_path, const std::string& section, + const std::string& program, const std::string& type, + const prevail::Program& prog, size_t max_slices = 1, + size_t max_steps = 200); + + /// Compute a backward slice from an arbitrary label (re-analyzes if needed). + prevail::FailureSlice compute_slice_from_label(const std::string& elf_path, const std::string& section, + const std::string& program, const std::string& type, + const prevail::Program& prog, const prevail::Label& label, + const prevail::RelevantState& seed = {}, size_t max_steps = 200); + + /// List all programs in an ELF file. + std::vector list_programs(const std::string& elf_path); + + /// Get the verifier options used for the current session. + /// Returns platform defaults if no session exists. + const prevail::ebpf_verifier_options_t& session_options() const; + + /// Get the platform pointer. + const prevail::ebpf_platform_t* platform() const { return ops_->platform(); } + + /// Get the platform ops. + PlatformOps* ops() const { return ops_; } + + private: + /// Check if the current session matches the requested program and options. + bool session_matches(const std::string& elf_path, const std::string& section, const std::string& program, + const std::string& type, const prevail::ebpf_verifier_options_t& options) const; + + /// Check if two option sets produce the same analysis results. + static bool analysis_options_equal(const prevail::ebpf_verifier_options_t& a, + const prevail::ebpf_verifier_options_t& b); + + PlatformOps* ops_; + std::optional session_; + std::string session_type_; // Program type override used for the current session. +}; + +} // namespace prevail diff --git a/src/mcp/README.md b/src/mcp/README.md new file mode 100644 index 000000000..78ffbb3a9 --- /dev/null +++ b/src/mcp/README.md @@ -0,0 +1,129 @@ +# prevail_mcp — PREVAIL Verifier MCP Server + +An [MCP (Model Context Protocol)](https://modelcontextprotocol.io/) server that exposes +PREVAIL's eBPF verification analysis as structured, queryable tools for LLM agents. + +Instead of parsing verbose text output from `check`, LLM agents can query invariants, +errors, control flow, source mappings, and constraint hypotheses through structured JSON +tool calls. + +## Building + +The MCP server is built alongside the `check` executable: + +```bash +cmake -B build -DCMAKE_BUILD_TYPE=Release +cmake --build build --target prevail_mcp +``` + +Output: `bin/prevail_mcp` + +To disable the MCP server build: + +```bash +cmake -B build -Dprevail_ENABLE_MCP=OFF +``` + +## Usage + +The server communicates via JSON-RPC 2.0 over stdio. Two framing modes are +supported, auto-detected from the first byte of input: +- **Newline-delimited JSON (NDJSON)** — used by GitHub Copilot CLI +- **Content-Length framing** — used by VS Code and spec-compliant clients + +The server is designed to be launched by an MCP client such as GitHub Copilot CLI or VS Code. + +### GitHub Copilot CLI + +``` +/mcp add +``` + +Set **Command** to the path to `prevail_mcp` (e.g. `bin/prevail_mcp`). + +### VS Code + +Add to `.vscode/mcp.json`: + +```json +{ + "servers": { + "prevail-verifier": { + "type": "stdio", + "command": "bin/prevail_mcp" + } + } +} +``` + +### Manual testing + +```bash +echo '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{}} +{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"verify_program","arguments":{"elf_path":"ebpf-samples/build/badhelpercall.o"}}}' | bin/prevail_mcp +``` + +## Tools + +| Tool | Description | +|------|-------------| +| `list_programs` | List all programs (sections/functions) in an ELF file | +| `verify_program` | Run verification, get pass/fail with error summary and stats | +| `get_invariant` | Get pre/post abstract state at one or more instructions | +| `get_instruction` | Full detail: disassembly, assertions, invariants, source, CFG neighbors | +| `get_errors` | All verification errors with pre-invariants and source lines | +| `get_cfg` | Control-flow graph as JSON basic blocks or Graphviz DOT | +| `get_source_mapping` | Bidirectional C source ↔ BPF instruction mapping (requires `-g`) | +| `check_constraint` | Test if constraints are consistent with / proven by verifier state | +| `get_slice` | Backward slice from an error or arbitrary PC with register relevance | +| `get_disassembly` | Instruction listing with source lines for a PC range | +| `verify_assembly` | Verify inline BPF assembly with options, pre-invariants, and observations | + +### Diagnostic Workflow + +These tools support the diagnostic protocol described in +[docs/llm-context.md](../docs/llm-context.md): + +1. **`get_slice`** — Start here. Returns the error, pre-invariant, assertions, + source line, and a backward slice showing only the instructions that causally + contributed to the failure, with per-instruction register relevance tracking. +2. **`check_constraint`** — Test hypotheses: "is `r1.type=packet` possible at PC 5?" + (`consistent` mode) or "does the verifier guarantee `packet_size >= 42`?" + (`proven` mode). +3. **`get_instruction`** / **`get_invariant`** — Deep dive on specific instructions. +4. **`get_source_mapping`** — Find the C source line for a BPF instruction or vice versa. + +### check_constraint Modes + +| Mode | Question it answers | Semantics | +|------|-------------------|-----------| +| `consistent` | "Is this possible?" | Constraints don't contradict the invariant (A ∩ C ≠ ⊥) | +| `proven` | "Does the verifier guarantee this?" | Invariant implies the constraints (A ⊑ C) | +| `entailed` | "Is this a sub-state?" | Observation is contained in invariant (C ⊑ A); requires near-complete constraint set | + +### Failure Slicing + +`get_slice` uses PREVAIL's backward dataflow slicing (same algorithm as +`check --failure-slice`) to identify only the instructions that causally contributed +to a verification failure. Each instruction in the slice includes: + +- The instruction text and PC +- Which registers are relevant at that point +- The post-invariant (constraints after the instruction) +- Source line mapping (if BTF info is available) + +The `trace_depth` parameter (default: 200) controls the maximum backward traversal +steps, matching `check --failure-slice-depth`. + +## Relationship to check + +| Feature | `check` | `prevail_mcp` | +|---------|---------|---------------| +| Interface | CLI (text output) | MCP (JSON-RPC over stdio) | +| Invariant access | All-or-nothing (`-v` flag) | Per-instruction query | +| Error diagnosis | `--failure-slice` | Built into `get_slice` | +| Constraint testing | Not available | `check_constraint` with 3 modes | +| Source mapping | `--line-info` flag | `get_source_mapping` tool | +| CFG output | `--dot` to file | `get_cfg` returns JSON or DOT | +| Platform | Linux | Cross-platform (Linux, Windows) | +| Caching | None (single run) | LRU cache + live session reuse | diff --git a/src/mcp/json_serializers.cpp b/src/mcp/json_serializers.cpp new file mode 100644 index 000000000..92f5a360f --- /dev/null +++ b/src/mcp/json_serializers.cpp @@ -0,0 +1,85 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#include "json_serializers.hpp" + +#include + +namespace prevail { + +nlohmann::json +label_to_json(const prevail::Label& label) +{ + nlohmann::json j; + j["from"] = label.from; + j["to"] = label.to; + if (!label.stack_frame_prefix.empty()) { + j["stack_frame_prefix"] = label.stack_frame_prefix; + } + if (!label.special_label.empty()) { + j["special_label"] = label.special_label; + } + return j; +} + +nlohmann::json +invariant_to_json(const prevail::StringInvariant& inv) +{ + if (inv.is_bottom()) { + return nlohmann::json::array({"_|_"}); + } + nlohmann::json arr = nlohmann::json::array(); + for (const auto& s : inv.value()) { + arr.push_back(s); + } + return arr; +} + +nlohmann::json +error_to_json(const prevail::VerificationError& error) +{ + nlohmann::json j; + if (error.where.has_value()) { + j["label"] = label_to_json(*error.where); + j["pc"] = error.where->from; + } + j["message"] = error.what(); + return j; +} + +nlohmann::json +instruction_to_json(const prevail::Instruction& inst) +{ + std::ostringstream os; + os << inst; + return nlohmann::json{{"text", os.str()}}; +} + +nlohmann::json +assertion_to_json(const prevail::Assertion& assertion) +{ + std::ostringstream os; + os << assertion; + return nlohmann::json{{"text", os.str()}}; +} + +nlohmann::json +line_info_to_json(const prevail::btf_line_info_t& info) +{ + return { + {"file", info.file_name}, + {"line", info.line_number}, + {"column", info.column_number}, + {"source", info.source_line}, + }; +} + +nlohmann::json +interval_to_json(const prevail::Interval& interval) +{ + std::ostringstream os; + os << interval; + return nlohmann::json{{"text", os.str()}}; +} + +} // namespace prevail diff --git a/src/mcp/json_serializers.hpp b/src/mcp/json_serializers.hpp new file mode 100644 index 000000000..d9065e3cf --- /dev/null +++ b/src/mcp/json_serializers.hpp @@ -0,0 +1,37 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT +#pragma once + +/// @file JSON serializers for PREVAIL verifier data structures. +/// All serialization delegates to PREVAIL's own operator<< / to_string(). + +#include "prevail_headers.hpp" + +#ifdef _MSC_VER +#pragma warning(push) +#pragma warning(disable : 26495) // Uninitialized member variable (nlohmann::basic_json::m_data). +#pragma warning(disable : 26819) // Unannotated fallthrough (nlohmann serializer). +#endif +#include +#ifdef _MSC_VER +#pragma warning(pop) +#endif + +namespace prevail { + +nlohmann::json +label_to_json(const prevail::Label& label); +nlohmann::json +invariant_to_json(const prevail::StringInvariant& inv); +nlohmann::json +error_to_json(const prevail::VerificationError& error); +nlohmann::json +instruction_to_json(const prevail::Instruction& inst); +nlohmann::json +assertion_to_json(const prevail::Assertion& assertion); +nlohmann::json +line_info_to_json(const prevail::btf_line_info_t& info); +nlohmann::json +interval_to_json(const prevail::Interval& interval); + +} // namespace prevail diff --git a/src/mcp/mcp_server.cpp b/src/mcp/mcp_server.cpp new file mode 100644 index 000000000..a482e043d --- /dev/null +++ b/src/mcp/mcp_server.cpp @@ -0,0 +1,99 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#include "mcp_server.hpp" + +#include + +namespace prevail { + +void +McpServer::register_tool(ToolInfo tool) +{ + const std::string name = tool.name; + tools_.emplace(name, std::move(tool)); +} + +nlohmann::json +McpServer::dispatch(const std::string& method, const nlohmann::json& params) +{ + if (method == "initialize") { + return handle_initialize(params); + } + if (method == "tools/list") { + return handle_tools_list(params); + } + if (method == "tools/call") { + return handle_tools_call(params); + } + if (method == "notifications/initialized" || method == "notifications/cancelled") { + return nullptr; // Notifications return nothing. + } + + throw std::runtime_error("Unknown method: " + method); +} + +nlohmann::json +McpServer::handle_initialize(const nlohmann::json& /*params*/) +{ + return { + {"protocolVersion", "2024-11-05"}, + {"capabilities", + { + {"tools", nlohmann::json::object()}, + }}, + {"serverInfo", + { + {"name", server_name_}, + {"version", server_version_}, + }}, + }; +} + +nlohmann::json +McpServer::handle_tools_list(const nlohmann::json& /*params*/) +{ + nlohmann::json tool_list = nlohmann::json::array(); + for (const auto& [name, info] : tools_) { + tool_list.push_back({ + {"name", info.name}, + {"description", info.description}, + {"inputSchema", info.input_schema}, + }); + } + return {{"tools", tool_list}}; +} + +nlohmann::json +McpServer::handle_tools_call(const nlohmann::json& params) +{ + const std::string tool_name = params.value("name", ""); + const nlohmann::json arguments = params.value("arguments", nlohmann::json::object()); + + auto it = tools_.find(tool_name); + if (it == tools_.end()) { + throw std::runtime_error("Unknown tool: " + tool_name); + } + + try { + nlohmann::json result = it->second.handler(arguments); + return { + {"content", + {{ + {"type", "text"}, + {"text", result.dump(2)}, + }}}, + }; + } catch (const std::exception& e) { + return { + {"content", + {{ + {"type", "text"}, + {"text", std::string("Error: ") + e.what()}, + }}}, + {"isError", true}, + }; + } +} + +} // namespace prevail diff --git a/src/mcp/mcp_server.hpp b/src/mcp/mcp_server.hpp new file mode 100644 index 000000000..475c04691 --- /dev/null +++ b/src/mcp/mcp_server.hpp @@ -0,0 +1,61 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT +#pragma once + +/// @file MCP server: tool registry, capability negotiation, and request dispatch. + +#include +#include +#ifdef _MSC_VER +#pragma warning(push) +#pragma warning(disable : 26495) // Uninitialized member variable (nlohmann::basic_json::m_data). +#pragma warning(disable : 26819) // Unannotated fallthrough (nlohmann serializer). +#endif +#include +#ifdef _MSC_VER +#pragma warning(pop) +#endif +#include + +namespace prevail { + +/// Metadata and handler for a single MCP tool. +struct ToolInfo +{ + std::string name; + std::string description; + nlohmann::json input_schema; // JSON Schema object for the tool's parameters. + std::function handler; +}; + +/// MCP server that registers tools and dispatches incoming requests. +class McpServer +{ + public: + explicit McpServer( + const std::string& name = "prevail-verifier", const std::string& version = "0.1.0") + : server_name_(name), server_version_(version) + { + } + + void + register_tool(ToolInfo tool); + + /// Dispatch a JSON-RPC request. Suitable as the handler for McpTransport::run(). + nlohmann::json + dispatch(const std::string& method, const nlohmann::json& params); + + private: + nlohmann::json + handle_initialize(const nlohmann::json& params); + nlohmann::json + handle_tools_list(const nlohmann::json& params); + nlohmann::json + handle_tools_call(const nlohmann::json& params); + + std::map tools_; + std::string server_name_; + std::string server_version_; +}; + +} // namespace prevail diff --git a/src/mcp/mcp_transport.cpp b/src/mcp/mcp_transport.cpp new file mode 100644 index 000000000..30e2deb0f --- /dev/null +++ b/src/mcp/mcp_transport.cpp @@ -0,0 +1,189 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#include "mcp_transport.hpp" + +#include +#include +#include +#include +#include + +namespace prevail { + +McpTransport::McpTransport(FILE* output) : output_(output) {} + +nlohmann::json +McpTransport::read_content_length() +{ + // Read headers until blank line. + size_t content_length = 0; + bool found_content_length = false; + + std::string line; + while (std::getline(std::cin, line)) { + // Remove trailing \r if present (Content-Length: N\r\n). + if (!line.empty() && line.back() == '\r') { + line.pop_back(); + } + if (line.empty()) { + break; // End of headers. + } + const std::string prefix = "Content-Length: "; + if (line.size() >= prefix.size() && line.compare(0, prefix.size(), prefix) == 0) { + try { + content_length = std::stoull(line.substr(prefix.size())); + found_content_length = true; + } catch (const std::exception&) { + // Malformed Content-Length value — skip this header. + } + } + // Ignore other headers (Content-Type, etc.). + } + + if (!found_content_length || std::cin.eof()) { + return nullptr; + } + + // Cap allocation to prevent unbounded memory growth from malformed input. + constexpr size_t max_message_size = 64 * 1024 * 1024; // 64 MB. + if (content_length > max_message_size) { + std::cerr << "prevail: Content-Length " << content_length << " exceeds maximum (" + << max_message_size << ")" << std::endl; + return nullptr; + } + + // Read exactly content_length bytes of body. + std::string body(content_length, '\0'); + std::cin.read(body.data(), static_cast(content_length)); + if (std::cin.gcount() != static_cast(content_length)) { + return nullptr; + } + + try { + return nlohmann::json::parse(body); + } catch (const nlohmann::json::parse_error&) { + return nullptr; + } +} + +nlohmann::json +McpTransport::read_ndjson() +{ + std::string line; + while (std::getline(std::cin, line)) { + if (!line.empty() && line.back() == '\r') { + line.pop_back(); + } + if (line.empty()) { + continue; // Skip blank lines. + } + try { + return nlohmann::json::parse(line); + } catch (const nlohmann::json::parse_error&) { + return nullptr; + } + } + return nullptr; // EOF. +} + +nlohmann::json +McpTransport::read_message() +{ + if (framing_ == Framing::unknown) { + // Auto-detect: peek at the first non-whitespace byte. + // '{' → NDJSON, 'C' → Content-Length. + int ch; + while ((ch = std::cin.peek()) != EOF) { + if (ch == ' ' || ch == '\t' || ch == '\r' || ch == '\n') { + std::cin.get(); // Consume whitespace. + continue; + } + break; + } + if (ch == EOF) { + return nullptr; + } + + if (ch == '{') { + framing_ = Framing::ndjson; + std::cerr << "prevail: using NDJSON framing" << std::endl; + } else { + framing_ = Framing::content_length; + std::cerr << "prevail: using Content-Length framing" << std::endl; + } + } + + return (framing_ == Framing::ndjson) ? read_ndjson() : read_content_length(); +} + +void +McpTransport::write_message(const nlohmann::json& msg) +{ + const std::string body = msg.dump(); + + if (framing_ == Framing::ndjson) { + // NDJSON: single line of JSON followed by newline. + fwrite(body.data(), 1, body.size(), output_); + fputc('\n', output_); + } else { + // Content-Length framing. + const std::string frame = "Content-Length: " + std::to_string(body.size()) + "\r\n\r\n" + body; + fwrite(frame.data(), 1, frame.size(), output_); + } + fflush(output_); +} + +void +McpTransport::run(Handler handler) +{ + while (true) { + nlohmann::json request = read_message(); + if (request.is_null()) { + break; // EOF or read error. + } + + try { + if (!request.is_object()) { + throw std::runtime_error("Request is not a JSON object"); + } + + const std::string method = request.value("method", ""); + const nlohmann::json params = request.value("params", nlohmann::json::object()); + const bool is_notification = !request.contains("id") || request["id"].is_null(); + + try { + nlohmann::json result = handler(method, params); + + if (!is_notification) { + nlohmann::json response = { + {"jsonrpc", "2.0"}, + {"id", request["id"]}, + {"result", std::move(result)}, + }; + write_message(response); + } + } catch (const std::exception& e) { + if (!is_notification) { + nlohmann::json error_response = { + {"jsonrpc", "2.0"}, + {"id", request["id"]}, + {"error", + { + {"code", -32603}, // Internal error. + {"message", e.what()}, + }}, + }; + write_message(error_response); + } else { + std::cerr << "prevail: notification handler error: " << e.what() << std::endl; + } + } + } catch (const std::exception& e) { + // Malformed request (not an object, missing fields, etc.). + std::cerr << "prevail: malformed request: " << e.what() << std::endl; + } + } +} + +} // namespace prevail diff --git a/src/mcp/mcp_transport.hpp b/src/mcp/mcp_transport.hpp new file mode 100644 index 000000000..c26eadf6e --- /dev/null +++ b/src/mcp/mcp_transport.hpp @@ -0,0 +1,78 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT +#pragma once + +/// @file MCP JSON-RPC 2.0 transport over stdio. +/// +/// Supports two framing modes, auto-detected from the first byte of input: +/// - Content-Length framing (VS Code, spec-compliant clients) +/// - Newline-delimited JSON / NDJSON (GitHub Copilot CLI) + +#include +#include +#include +#ifdef _MSC_VER +#pragma warning(push) +#pragma warning(disable : 26495) // Uninitialized member variable (nlohmann::basic_json::m_data). +#pragma warning(disable : 26819) // Unannotated fallthrough (nlohmann serializer). +#endif +#include +#ifdef _MSC_VER +#pragma warning(pop) +#endif +#include + +namespace prevail { + +/// Reads JSON-RPC 2.0 messages from stdin and writes responses to a dedicated +/// output FILE* using either Content-Length or NDJSON framing. +/// +/// The output FILE* should be the original stdout pipe, opened in binary mode +/// with buffering disabled. This separation allows linked libraries that write +/// to std::cout / stdout (e.g. the PREVAIL verifier's dump_btf_types or the +/// eBPF API's verbose parse-failure messages) to be safely redirected to stderr +/// without corrupting the protocol framing. +class McpTransport +{ + public: + /// @param output FILE* for writing MCP protocol messages. + /// Must be in binary mode; caller should disable buffering with setvbuf. + explicit McpTransport(FILE* output); + + /// Read one JSON-RPC message from stdin. + /// On the first call, peeks at stdin to auto-detect the framing mode. + /// @return Parsed JSON message, or nullptr on EOF/error. + nlohmann::json + read_message(); + + /// Write one JSON-RPC message to the MCP output stream. + void + write_message(const nlohmann::json& msg); + + /// Main event loop. Reads requests, dispatches to handler, writes responses. + /// The handler receives (method, params) and returns a result JSON. + /// For notifications (no "id") the handler is still called but the return value is ignored. + /// Handler exceptions are caught and returned as JSON-RPC error responses. + /// The loop exits on EOF or malformed input. + using Handler = std::function; + void + run(Handler handler); + + private: + enum class Framing + { + unknown, + content_length, // "Content-Length: N\r\n\r\n{...}" + ndjson, // "{...}\n" + }; + + nlohmann::json + read_content_length(); + nlohmann::json + read_ndjson(); + + FILE* output_; + Framing framing_ = Framing::unknown; +}; + +} // namespace prevail diff --git a/src/mcp/prevail_headers.hpp b/src/mcp/prevail_headers.hpp new file mode 100644 index 000000000..87f511042 --- /dev/null +++ b/src/mcp/prevail_headers.hpp @@ -0,0 +1,51 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT +#pragma once + +/// @file Aggregate include for PREVAIL verifier headers used by the MCP server. +/// On MSVC, suppresses warnings from PREVAIL headers that are treated as errors +/// by projects with /W4 /WX (e.g. ebpf-for-windows). On GCC/Clang these are no-ops. + +// Pre-define the include guard for bpf_conformance's ebpf_inst.h to prevent it +// from being included (its EbpfInst struct conflicts with prevail::EbpfInst). +#ifndef BPF_CONFORMANCE_CORE_EBPF_INST_H +#define BPF_CONFORMANCE_CORE_EBPF_INST_H +#endif + +#ifdef _MSC_VER +#pragma warning(push) +#pragma warning(disable : 4100) // Unreferenced formal parameter. +#pragma warning(disable : 4244) // Conversion, possible loss of data. +#pragma warning(disable : 4267) // Conversion from 'size_t' to 'int'. +#pragma warning(disable : 4458) // Declaration hides class member. +#pragma warning(disable : 26439) // Function may not throw. +#pragma warning(disable : 26450) // Arithmetic overflow. +#pragma warning(disable : 26451) // Arithmetic overflow. +#pragma warning(disable : 26495) // Always initialize a member variable. +#endif + +// Undef macros that conflict with PREVAIL headers on Windows. +#undef FALSE +#undef TRUE +#undef min +#undef max + +#include "cfg/cfg.hpp" +#include "config.hpp" +#include "ebpf_verifier.hpp" +#include "ir/program.hpp" +#include "ir/unmarshal.hpp" +#include "platform.hpp" +#include "result.hpp" +#include "spec/type_descriptors.hpp" +#include "string_constraints.hpp" +#include "verifier.hpp" + +#ifdef _WIN32 +#define FALSE 0 +#define TRUE 1 +#endif + +#ifdef _MSC_VER +#pragma warning(pop) +#endif diff --git a/src/mcp/tools.cpp b/src/mcp/tools.cpp new file mode 100644 index 000000000..c0f27fa8a --- /dev/null +++ b/src/mcp/tools.cpp @@ -0,0 +1,1265 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +#include "tools.hpp" +#include "json_serializers.hpp" + +#include +#include +#include +#include +#include + +#include "ir/parse.hpp" + +using json = nlohmann::json; + +namespace prevail { + +/// Build verifier options from JSON args, starting from engine defaults. +/// Applies check_termination, allow_division_by_zero, strict, and +/// sets verbosity flags needed for MCP tools (print_failures, print_line_info, +/// collect_instruction_deps). +static prevail::ebpf_verifier_options_t build_options(const json& args, AnalysisEngine& engine) { + prevail::ebpf_verifier_options_t options = engine.ops()->default_options(); + if (args.contains("check_termination")) { + options.cfg_opts.check_for_termination = args["check_termination"].get(); + } + if (args.contains("allow_division_by_zero")) { + options.allow_division_by_zero = args["allow_division_by_zero"].get(); + } + if (args.contains("strict")) { + options.strict = args["strict"].get(); + } + options.verbosity_opts.print_failures = true; + options.verbosity_opts.print_line_info = true; + options.verbosity_opts.collect_instruction_deps = true; + return options; +} + +// Helper: find the primary label for a given PC in the analysis session. +// Returns the first label with .to == -1 (sequential flow), or the first available label. +static prevail::Label find_label_for_pc(const AnalysisSession& session, int pc) { + auto it = session.pc_to_labels.find(pc); + if (it == session.pc_to_labels.end() || it->second.empty()) { + throw std::runtime_error("No label found for PC " + std::to_string(pc)); + } + // Prefer the sequential (non-jump) label. + for (const auto& label : it->second) { + if (label.to == -1) { + return label; + } + } + return it->second.front(); +} + +// Helper: get all labels for a PC (may include jump edge labels). +static const std::vector& find_labels_for_pc(const AnalysisSession& session, int pc) { + auto it = session.pc_to_labels.find(pc); + if (it == session.pc_to_labels.end()) { + static const std::vector empty; + return empty; + } + return it->second; +} + +// ─── Tool: list_programs ─────────────────────────────────────────────────────── + +static json handle_list_programs(const json& args, AnalysisEngine& engine) { + const std::string elf_path = args.at("elf_path").get(); + auto entries = engine.list_programs(elf_path); + + json programs = json::array(); + for (const auto& entry : entries) { + programs.push_back({ + {"section", entry.section}, + {"function", entry.function}, + }); + } + return {{"programs", programs}}; +} + +// ─── Tool: verify_program ────────────────────────────────────────────────────── + +static json handle_verify_program(const json& args, AnalysisEngine& engine) { + const std::string elf_path = args.at("elf_path").get(); + const std::string section = args.value("section", ""); + const std::string program = args.value("program", ""); + const std::string type = args.value("program_type", ""); + auto options = build_options(args, engine); + + const auto& session = engine.analyze(elf_path, section, program, type, &options); + + // Count errors. + int error_count = 0; + for (const auto& [label, inv_pair] : session.invariants) { + if (!inv_pair.pre_is_bottom && inv_pair.error_message.has_value()) { + error_count++; + } + } + + // Count unreachable: post is bottom and instruction is Assume with no error. + int total_unreachable = 0; + for (const auto& [label, inv_pair] : session.invariants) { + if (inv_pair.pre_is_bottom) { + continue; + } + if (inv_pair.post.is_bottom() && !inv_pair.error_message.has_value()) { + if (std::get_if(&session.program.instruction_at(label))) { + total_unreachable++; + } + } + } + + json j = { + {"passed", !session.failed}, + {"max_loop_count", session.max_loop_count}, + {"exit_value", interval_to_json(session.exit_value)}, + {"error_count", error_count}, + {"total_unreachable", total_unreachable}, + {"instruction_count", static_cast(session.inst_seq.size())}, + {"section", session.section}, + {"function", session.program_name}, + }; + + // Scan invariants for first error. + for (const auto& [label, inv_pair] : session.invariants) { + if (!inv_pair.pre_is_bottom && inv_pair.error_message.has_value()) { + json fe; + if (inv_pair.error_label.has_value()) { + fe["label"] = label_to_json(*inv_pair.error_label); + fe["pc"] = inv_pair.error_label->from; + } + fe["message"] = *inv_pair.error_message; + // Add source mapping if available. + if (inv_pair.error_label.has_value()) { + auto src_it = session.pc_to_source.find(inv_pair.error_label->from); + if (src_it != session.pc_to_source.end()) { + fe["source"] = line_info_to_json(src_it->second); + } + } + j["first_error"] = fe; + break; + } + } + + return j; +} + +// ─── Tool: get_invariant ─────────────────────────────────────────────────────── + +static json handle_get_invariant(const json& args, AnalysisEngine& engine) { + const std::string elf_path = args.at("elf_path").get(); + const std::string point_str = args.value("point", "pre"); + const std::string section = args.value("section", ""); + const std::string program = args.value("program", ""); + const std::string type = args.value("program_type", ""); + + const auto& session = engine.analyze(elf_path, section, program, type); + const auto pcs = args.at("pcs").get>(); + + // Helper: get invariant results for a single PC. + auto get_invariant_for_pc = [&](int pc) -> json { + const auto& labels = find_labels_for_pc(session, pc); + if (labels.empty()) { + return {{"pc", pc}, {"error", "No label found for PC " + std::to_string(pc)}}; + } + + json results = json::array(); + for (const auto& label : labels) { + auto inv_it = session.invariants.find(label); + if (inv_it == session.invariants.end()) { + continue; + } + const auto& inv_pair = inv_it->second; + const auto& domain = (point_str == "post") ? inv_pair.post : inv_pair.pre; + + json entry = { + {"label", label_to_json(label)}, + {"point", point_str}, + {"constraints", invariant_to_json(domain)}, + }; + results.push_back(entry); + } + + if (results.size() == 1) { + return results[0]; + } + return {{"pc", pc}, {"labels", results}}; + }; + + if (pcs.size() == 1) { + return get_invariant_for_pc(pcs[0]); + } + + json batch_results = json::array(); + for (int pc : pcs) { + json result = get_invariant_for_pc(pc); + result["pc"] = pc; + batch_results.push_back(result); + } + return {{"results", batch_results}}; +} + +// ─── Tool: get_instruction ───────────────────────────────────────────────────── + +static json handle_get_instruction(const json& args, AnalysisEngine& engine) { + const std::string elf_path = args.at("elf_path").get(); + const std::string section = args.value("section", ""); + const std::string program = args.value("program", ""); + const std::string type = args.value("program_type", ""); + + const auto& session = engine.analyze(elf_path, section, program, type); + + const auto pcs = args.at("pcs").get>(); + + // Helper: get instruction detail for a single PC. + auto get_instruction_for_pc = [&](int pc) -> json { + const auto label = find_label_for_pc(session, pc); + json j = {{"pc", pc}, {"label", label_to_json(label)}}; + + // Instruction text. + j["text"] = instruction_to_json(session.program.instruction_at(label))["text"]; + + // Assertions. + json assertions = json::array(); + for (const auto& a : session.program.assertions_at(label)) { + assertions.push_back(assertion_to_json(a)["text"]); + } + j["assertions"] = assertions; + + // Invariants. + auto inv_it = session.invariants.find(label); + if (inv_it != session.invariants.end()) { + j["pre_invariant"] = invariant_to_json(inv_it->second.pre); + if (!inv_it->second.post.is_bottom()) { + j["post_invariant"] = invariant_to_json(inv_it->second.post); + } else { + j["post_invariant"] = nullptr; + } + if (inv_it->second.error_message.has_value()) { + j["error"] = *inv_it->second.error_message; + } + } + + // Source mapping. + auto src_it = session.pc_to_source.find(pc); + if (src_it != session.pc_to_source.end()) { + j["source"] = line_info_to_json(src_it->second); + } + + // CFG neighbors. + json successors = json::array(); + for (const auto& child : session.program.cfg().children_of(label)) { + successors.push_back(child.from); + } + j["successors"] = successors; + + json predecessors = json::array(); + for (const auto& parent : session.program.cfg().parents_of(label)) { + predecessors.push_back(parent.from); + } + j["predecessors"] = predecessors; + + return j; + }; + + // Build results, returning structured errors for invalid PCs. + json batch_results = json::array(); + for (int pc : pcs) { + try { + batch_results.push_back(get_instruction_for_pc(pc)); + } catch (const std::runtime_error& e) { + batch_results.push_back({{"pc", pc}, {"error", e.what()}}); + } + } + return {{"results", batch_results}}; +} + +// ─── Tool: get_errors ────────────────────────────────────────────────────────── + +static json handle_get_errors(const json& args, AnalysisEngine& engine) { + const std::string elf_path = args.at("elf_path").get(); + const std::string section = args.value("section", ""); + const std::string program = args.value("program", ""); + const std::string type = args.value("program_type", ""); + + const auto& session = engine.analyze(elf_path, section, program, type); + + json errors = json::array(); + for (const auto& [label, inv_pair] : session.invariants) { + if (inv_pair.pre_is_bottom) { + continue; + } + if (inv_pair.error_message.has_value()) { + json e; + if (inv_pair.error_label.has_value()) { + e["label"] = label_to_json(*inv_pair.error_label); + e["pc"] = inv_pair.error_label->from; + } + e["message"] = *inv_pair.error_message; + e["pre_invariant"] = invariant_to_json(inv_pair.pre); + e["instruction"] = instruction_to_json(session.program.instruction_at(label))["text"]; + + auto src_it = session.pc_to_source.find(label.from); + if (src_it != session.pc_to_source.end()) { + e["source"] = line_info_to_json(src_it->second); + } + errors.push_back(e); + } + } + + json unreachable = json::array(); + for (const auto& [label, inv_pair] : session.invariants) { + if (inv_pair.pre_is_bottom) { + continue; + } + if (inv_pair.post.is_bottom() && !inv_pair.error_message.has_value()) { + if (const auto passume = std::get_if(&session.program.instruction_at(label))) { + std::string msg = + prevail::to_string(label) + ": Code becomes unreachable (" + prevail::to_string(*passume) + ")"; + unreachable.push_back({{"label", label_to_json(label)}, {"message", msg}}); + } + } + } + + return { + {"passed", !session.failed}, + {"errors", errors}, + {"unreachable", unreachable}, + }; +} + +// ─── Tool: get_cfg ───────────────────────────────────────────────────────────── + +static json handle_get_cfg(const json& args, AnalysisEngine& engine) { + const std::string elf_path = args.at("elf_path").get(); + const std::string format = args.value("format", "json"); + const std::string section = args.value("section", ""); + const std::string program = args.value("program", ""); + const std::string type = args.value("program_type", ""); + + const auto& session = engine.analyze(elf_path, section, program, type); + + if (format == "dot") { + // Generate DOT format inline (same logic as print_dot in printing.cpp). + std::ostringstream dot; + dot << "digraph program {\n"; + dot << " node [shape = rectangle];\n"; + for (const auto& label : session.program.labels()) { + dot << " \"" << label << "\"[label=\""; + for (const auto& pre : session.program.assertions_at(label)) { + dot << "assert " << pre << "\\l"; + } + dot << session.program.instruction_at(label) << "\\l"; + dot << "\"];\n"; + for (const auto& next : session.program.cfg().children_of(label)) { + dot << " \"" << label << "\" -> \"" << next << "\";\n"; + } + dot << "\n"; + } + dot << "}\n"; + return {{"format", "dot"}, {"dot", dot.str()}}; + } + + // JSON mode: serialize basic blocks. + auto basic_blocks = prevail::BasicBlock::collect_basic_blocks(session.program.cfg(), true); + json blocks = json::array(); + for (const auto& bb : basic_blocks) { + json block; + block["first_pc"] = bb.first_label().from; + block["last_pc"] = bb.last_label().from; + + json pcs = json::array(); + for (const auto& label : bb) { + pcs.push_back(label.from); + } + block["pcs"] = pcs; + + json succs = json::array(); + for (const auto& child : session.program.cfg().children_of(bb.last_label())) { + succs.push_back(child.from); + } + block["successors"] = succs; + + blocks.push_back(block); + } + + return {{"format", "json"}, {"basic_blocks", blocks}}; +} + +// ─── Tool: get_source_mapping ────────────────────────────────────────────────── + +static json handle_get_source_mapping(const json& args, AnalysisEngine& engine) { + const std::string elf_path = args.at("elf_path").get(); + const std::string section = args.value("section", ""); + const std::string program = args.value("program", ""); + const std::string type = args.value("program_type", ""); + + const auto& session = engine.analyze(elf_path, section, program, type); + + if (args.contains("pc")) { + const int pc = args["pc"].get(); + auto it = session.pc_to_source.find(pc); + if (it == session.pc_to_source.end()) { + return {{"pc", pc}, {"source", nullptr}, {"note", "No BTF line info for this PC"}}; + } + json j = {{"pc", pc}, {"source", line_info_to_json(it->second)}}; + // Also include instruction text. + auto labels = find_labels_for_pc(session, pc); + if (!labels.empty()) { + j["instruction"] = instruction_to_json(session.program.instruction_at(labels.front()))["text"]; + } + return j; + } + + if (args.contains("source_line")) { + const int source_line = args["source_line"].get(); + const std::string source_file = args.value("source_file", ""); + + // Search all source mappings for matching line. + json matches = json::array(); + for (const auto& [key, pcs] : session.source_to_pcs) { + if (key.second == source_line && + (source_file.empty() || key.first == source_file || key.first.find(source_file) != std::string::npos)) { + for (int matched_pc : pcs) { + json m = {{"pc", matched_pc}}; + auto labels = find_labels_for_pc(session, matched_pc); + if (!labels.empty()) { + m["instruction"] = instruction_to_json(session.program.instruction_at(labels.front()))["text"]; + } + auto src_it = session.pc_to_source.find(matched_pc); + if (src_it != session.pc_to_source.end()) { + m["source"] = line_info_to_json(src_it->second); + } + matches.push_back(m); + } + } + } + return {{"source_line", source_line}, {"matches", matches}}; + } + + // Return entire source map. + if (session.pc_to_source.empty()) { + return { + {"note", "No BTF line info available. Compile with -g to enable source mapping."}, + {"entries", json::array()}, + }; + } + + json entries = json::array(); + for (const auto& [pc, info] : session.pc_to_source) { + entries.push_back({{"pc", pc}, {"source", line_info_to_json(info)}}); + } + return {{"entries", entries}}; +} + +// ─── Tool: check_constraint ──────────────────────────────────────────────────── + +static json handle_check_constraint(const json& args, AnalysisEngine& engine) { + const std::string elf_path = args.at("elf_path").get(); + const std::string point_str = args.value("point", "pre"); + const std::string mode_str = args.value("mode", "consistent"); + const std::string section = args.value("section", ""); + const std::string program = args.value("program", ""); + const std::string type = args.value("program_type", ""); + + auto point = (point_str == "post") ? prevail::InvariantPoint::post : prevail::InvariantPoint::pre; + + // Support single-check or batch-check. + // Single: { "pc": N, "constraints": [...] } + // Batch: { "checks": [{ "pc": N, "constraints": [...], "mode": "...", "point": "..." }, ...] } + struct CheckQuery { + int pc{}; + prevail::InvariantPoint pt{prevail::InvariantPoint::pre}; + std::string md; + std::vector constraints; + }; + + std::vector queries; + + if (args.contains("checks")) { + // Batch mode. + for (const auto& check : args["checks"]) { + CheckQuery q; + q.pc = check.at("pc").get(); + q.constraints = check.at("constraints").get>(); + auto qs = check.value("point", point_str); + q.pt = (qs == "post") ? prevail::InvariantPoint::post : prevail::InvariantPoint::pre; + q.md = check.value("mode", mode_str); + queries.push_back(std::move(q)); + } + } else { + // Single mode. + CheckQuery q; + q.pc = args.at("pc").get(); + q.constraints = args.at("constraints").get>(); + q.pt = point; + q.md = mode_str; + queries.push_back(std::move(q)); + } + + // Run analysis once (engine caches the live session for reuse across calls). + // We need the AnalysisSession for label lookup. + const auto& session = engine.analyze(elf_path, section, program, type); + + // Process all queries against the same analysis. + json results = json::array(); + for (const auto& q : queries) { + json entry = {{"pc", q.pc}}; + try { + auto label = find_label_for_pc(session, q.pc); + + std::set constraint_set(q.constraints.begin(), q.constraints.end()); + prevail::StringInvariant observation{std::move(constraint_set)}; + + auto check_result = + engine.check_constraint(elf_path, section, program, type, label, q.pt, observation, q.md); + entry["ok"] = check_result.ok; + entry["message"] = check_result.message; + + // Include the invariant so agents can see what the verifier knows. + auto inv = engine.get_live_invariant(label, q.pt); + if (!inv.is_bottom()) { + entry["invariant"] = invariant_to_json(inv); + } + } catch (const std::runtime_error& e) { + entry["ok"] = false; + entry["message"] = e.what(); + } + results.push_back(std::move(entry)); + } + + // Single-query returns the result directly; batch returns array. + if (!args.contains("checks") && results.size() == 1) { + return results[0]; + } + return {{"results", results}}; +} + +// ─── Tool: get_slice ─────────────────────────────────────────────────── + +// Serialize a failure slice into JSON. +static json serialize_slice(const prevail::FailureSlice& slice, const AnalysisSession& session, + const prevail::Label& target_label) { + json contributing = json::array(); + auto impacted = slice.impacted_labels(); + for (const auto& label : impacted) { + if (label == target_label) { + continue; + } + json step = { + {"pc", label.from}, + {"text", instruction_to_json(session.program.instruction_at(label))["text"]}, + }; + auto rel_it = slice.relevance.find(label); + if (rel_it != slice.relevance.end()) { + json relevant_regs = json::array(); + for (const auto& reg : rel_it->second.registers) { + relevant_regs.push_back("r" + std::to_string(reg.v)); + } + if (!relevant_regs.empty()) { + step["relevant_registers"] = relevant_regs; + } + } + auto inv_it = session.invariants.find(label); + if (inv_it != session.invariants.end() && !inv_it->second.post.is_bottom()) { + step["post_invariant"] = invariant_to_json(inv_it->second.post); + } + auto trace_src = session.pc_to_source.find(label.from); + if (trace_src != session.pc_to_source.end()) { + step["source"] = line_info_to_json(trace_src->second); + } + contributing.push_back(step); + } + return contributing; +} + +static json handle_get_slice(const json& args, AnalysisEngine& engine) { + const std::string elf_path = args.at("elf_path").get(); + const std::string section = args.value("section", ""); + const std::string program = args.value("program", ""); + const std::string type = args.value("program_type", ""); + const size_t trace_depth = std::min(args.value("trace_depth", static_cast(200)), static_cast(10000)); + auto options = build_options(args, engine); + + const auto& session = engine.analyze(elf_path, section, program, type, &options); + + prevail::Label target_label = prevail::Label::entry; + + if (args.contains("pc")) { + const int pc = args["pc"].get(); + target_label = find_label_for_pc(session, pc); + } else { + const int error_index = args.value("error_index", 0); + int idx = 0; + bool found_error = false; + for (const auto& [label, inv_pair] : session.invariants) { + if (inv_pair.pre_is_bottom) { + continue; + } + if (inv_pair.error_message.has_value()) { + if (idx == error_index) { + target_label = label; + found_error = true; + break; + } + idx++; + } + } + if (!found_error) { + throw std::runtime_error("Error index " + std::to_string(error_index) + " not found"); + } + } + + const auto& inv = session.invariants.at(target_label); + + json j = {{"pc", target_label.from}}; + j["instruction"] = instruction_to_json(session.program.instruction_at(target_label))["text"]; + j["pre_invariant"] = invariant_to_json(inv.pre); + + if (inv.error_message.has_value()) { + json error_json; + if (inv.error_label.has_value()) { + error_json["label"] = label_to_json(*inv.error_label); + error_json["pc"] = inv.error_label->from; + } + error_json["message"] = *inv.error_message; + j["error"] = error_json; + } + + json assertions = json::array(); + for (const auto& a : session.program.assertions_at(target_label)) { + assertions.push_back(assertion_to_json(a)["text"]); + } + j["assertions"] = assertions; + + auto src_it = session.pc_to_source.find(target_label.from); + if (src_it != session.pc_to_source.end()) { + j["source"] = line_info_to_json(src_it->second); + } + + // Use backward slicing from the target label. + // compute_slice_from_label seeds from the instruction's read registers. + try { + auto slice = engine.compute_slice_from_label(elf_path, section, program, type, session.program, target_label, + {}, trace_depth); + j["failure_slice"] = serialize_slice(slice, session, target_label); + } catch (const std::exception& e) { + std::cerr << "prevail: slicing failed: " << e.what() << std::endl; + j["failure_slice"] = json::array(); + } + + return j; +} + +// ─── Tool: verify_assembly ───────────────────────────────────────────────────── + +/// Parse a code string into labeled blocks and build an InstructionSeq. +/// Labels are lines matching `:` (angle brackets required). +/// All code before the first explicit label is placed in the `` block. +static prevail::InstructionSeq parse_assembly(const std::string& code, const prevail::ebpf_platform_t* platform) { + // Split code into lines. + std::vector lines; + std::istringstream stream(code); + std::string line; + while (std::getline(stream, line)) { + // Trim whitespace. + const auto start = line.find_first_not_of(" \t\r\n"); + if (start == std::string::npos) { + continue; // Skip blank lines. + } + const auto end = line.find_last_not_of(" \t\r\n"); + lines.push_back(line.substr(start, end - start + 1)); + } + + // First pass: split into labeled blocks and count instructions for label resolution. + struct Block { + std::string label; // With angle brackets (e.g., ""). + std::vector instructions; + }; + std::vector blocks; + static const std::regex label_regex(R"(<(\w+)>:\s*)"); + + Block current_block{"", {}}; + for (const auto& l : lines) { + std::smatch m; + if (std::regex_match(l, m, label_regex)) { + if (!current_block.instructions.empty()) { + blocks.push_back(std::move(current_block)); + } + current_block = Block{"<" + m[1].str() + ">", {}}; + } else { + // Strip trailing comments ("; ..."). + auto comment_pos = l.find(';'); + std::string inst_text = (comment_pos != std::string::npos) ? l.substr(0, comment_pos) : l; + auto trimmed_end = inst_text.find_last_not_of(" \t"); + if (trimmed_end != std::string::npos) { + current_block.instructions.push_back(inst_text.substr(0, trimmed_end + 1)); + } + } + } + if (!current_block.instructions.empty()) { + blocks.push_back(std::move(current_block)); + } + + // Build label → PC map. + std::map label_map; + int pc = 0; + for (const auto& block : blocks) { + label_map.emplace(block.label, prevail::Label{pc, -1, {}}); + pc += static_cast(block.instructions.size()); + } + + // Second pass: parse each instruction. + // Intercept "call N" to resolve helpers through the server's platform (which may + // have platform-specific helpers not available on g_ebpf_platform_linux). + prevail::InstructionSeq result; + int label_index = 0; + static const std::regex call_regex(R"(call\s+(\d+).*)"); + for (const auto& block : blocks) { + for (const auto& inst_text : block.instructions) { + try { + prevail::Instruction inst; + std::smatch call_match; + if (std::regex_match(inst_text, call_match, call_regex) && platform != nullptr) { + const int func = std::stoi(call_match[1].str()); + inst = prevail::make_call(func, *platform); + } else { + inst = prevail::parse_instruction(inst_text, label_map); + } + result.emplace_back(prevail::Label{label_index, -1, {}}, inst, std::optional()); + } catch (const std::exception& e) { + throw std::runtime_error("Parse error at instruction " + std::to_string(label_index) + " (\"" + + inst_text + "\"): " + e.what()); + } + label_index++; + } + } + + if (result.empty()) { + throw std::runtime_error("No instructions parsed from code"); + } + + return result; +} + +static json handle_verify_assembly(const json& args, AnalysisEngine& engine) { + const std::string code = args.at("code").get(); + const auto pre_vec = args.value("pre", std::vector{}); + const std::string type_name = args.value("program_type", "xdp"); + const int map_key_size = args.value("map_key_size", 4); + const int map_value_size = args.value("map_value_size", 4); + if (map_key_size <= 0 || map_value_size <= 0) { + throw std::runtime_error("map_key_size and map_value_size must be positive"); + } + + // Set up verification options from the current session (or platform defaults). + prevail::ebpf_verifier_options_t options = engine.session_options(); + if (args.contains("check_termination")) { + options.cfg_opts.check_for_termination = args["check_termination"].get(); + } + if (args.contains("allow_division_by_zero")) { + options.allow_division_by_zero = args["allow_division_by_zero"].get(); + } + if (args.contains("strict")) { + options.strict = args["strict"].get(); + } + if (args.contains("big_endian")) { + options.big_endian = args["big_endian"].get(); + } + options.verbosity_opts.print_failures = true; + options.verbosity_opts.collect_instruction_deps = true; + + // Set up pre-invariant. + const bool custom_pre = !pre_vec.empty(); + options.setup_constraints = !custom_pre; + // Assembly snippets don't need to end with exit (matching YAML test behavior). + options.cfg_opts.must_have_exit = false; + + prevail::StringInvariant pre_invariant = prevail::StringInvariant::top(); + if (custom_pre) { + std::set pre_set(pre_vec.begin(), pre_vec.end()); + pre_invariant = prevail::StringInvariant{std::move(pre_set)}; + } + + // Create a local platform copy with callx conformance group enabled + // (assembly testing should support all instruction types). + prevail::ebpf_platform_t local_platform = *engine.platform(); + local_platform.supported_conformance_groups = + local_platform.supported_conformance_groups | bpf_conformance_groups_t::callx; + + // Build ProgramInfo with default map descriptors. + // Two maps: index 0 (fd 0) and index 1 (fd 1) to support both map_by_idx(0) and map_fd 1. + prevail::EbpfMapDescriptor map_desc0{}; + map_desc0.original_fd = 0; + map_desc0.type = 0; + map_desc0.key_size = static_cast(map_key_size); + map_desc0.value_size = static_cast(map_value_size); + map_desc0.max_entries = 4; + map_desc0.inner_map_fd = 0; + + prevail::EbpfMapDescriptor map_desc1{}; + map_desc1.original_fd = 1; + map_desc1.type = 0; + map_desc1.key_size = static_cast(map_key_size); + map_desc1.value_size = static_cast(map_value_size); + map_desc1.max_entries = 4; + map_desc1.inner_map_fd = 0; + + // Set up TLS for analysis. Unlike the normal ELF path (which calls prepare_tls + // then read_elf), we set up thread-local state directly since there's no ELF. + // NOTE: We deliberately do NOT call prepare_tls here because it clears the + // _program_info_cache which is needed for is_helper_usable_windows. Instead, + // we get the program type (which populates the cache) and set TLS manually. + prevail::ThreadLocalGuard tls_guard; + prevail::thread_local_options = options; + + const prevail::EbpfProgramType prog_type = local_platform.get_program_type(type_name, type_name); + const ebpf_context_descriptor_t* ctx_desc = prog_type.context_descriptor; + static const ebpf_context_descriptor_t fallback_ctx{64, 0, 4, -1}; + prevail::EbpfProgramType effective_type = prog_type; + if (ctx_desc == nullptr) { + effective_type.name = type_name; + effective_type.context_descriptor = &fallback_ctx; + } + + prevail::ProgramInfo info{&local_platform, {map_desc0, map_desc1}, effective_type}; + prevail::thread_local_program_info = info; + + // Parse assembly text into InstructionSeq (with TLS program info available). + prevail::InstructionSeq inst_seq = parse_assembly(code, &local_platform); + + // Run analysis. + prevail::Program prog = prevail::Program::from_sequence(inst_seq, info, options); + prevail::AnalysisResult result = prevail::analyze(prog, pre_invariant); + + // Build response. + json j = { + {"passed", !result.failed}, + {"instruction_count", static_cast(inst_seq.size())}, + }; + + // Exit invariant. + prevail::StringInvariant exit_inv = result.invariant_at(prevail::Label::exit); + j["post_invariant"] = invariant_to_json(exit_inv); + j["exit_value"] = interval_to_json(result.exit_value); + + // Collect errors. + json errors = json::array(); + for (const auto& [label, inv_pair] : result.invariants) { + if (inv_pair.pre.is_bottom()) { + continue; + } + if (inv_pair.error.has_value()) { + json e; + e["pc"] = inv_pair.error->where.has_value() ? inv_pair.error->where->from : label.from; + e["message"] = inv_pair.error->what(); + e["pre_invariant"] = invariant_to_json(inv_pair.pre.to_set()); + errors.push_back(e); + } + } + j["errors"] = errors; + + // Process observe assertions (check intermediate invariants). + if (args.contains("observe")) { + json obs_results = json::array(); + for (const auto& obs : args["observe"]) { + const std::string point_str = obs.value("point", "pre"); + const std::string mode_str = obs.value("mode", "consistent"); + if (!obs.contains("constraints")) { + throw std::runtime_error("observe entry missing required 'constraints' field"); + } + const auto constraints_vec = obs.at("constraints").get>(); + + // Determine the label: either "pc" (integer) or "label" (string, e.g. "exit"). + prevail::Label label = prevail::Label::entry; + json obs_entry = json::object(); + if (obs.contains("pc")) { + const int obs_pc = obs["pc"].get(); + if (obs_pc < 0) { + throw std::runtime_error("Invalid observation PC: " + std::to_string(obs_pc)); + } + label = prevail::Label{obs_pc, -1, {}}; + obs_entry = {{"pc", obs_pc}}; + } else if (obs.contains("label")) { + const std::string label_str = obs["label"].get(); + if (label_str == "exit") { + label = prevail::Label::exit; + } else { + obs_entry["ok"] = false; + obs_entry["message"] = "Unknown label: " + label_str + " (supported: \"exit\")"; + obs_results.push_back(obs_entry); + continue; + } + obs_entry = {{"label", label_str}}; + } + + try { + auto point = (point_str == "post") ? prevail::InvariantPoint::post : prevail::InvariantPoint::pre; + prevail::ObservationCheckMode mode; + if (mode_str == "entailed") { + mode = prevail::ObservationCheckMode::entailed; + } else if (mode_str == "consistent") { + mode = prevail::ObservationCheckMode::consistent; + } else { + obs_entry["ok"] = false; + obs_entry["message"] = "Unknown mode: " + mode_str; + obs_results.push_back(obs_entry); + continue; + } + std::set constraint_set(constraints_vec.begin(), constraints_vec.end()); + prevail::StringInvariant observation{std::move(constraint_set)}; + + auto check = result.check_observation_at_label(label, point, observation, mode); + obs_entry["ok"] = check.ok; + obs_entry["message"] = check.message; + + // Include the invariant at this point. + auto it = result.invariants.find(label); + if (it != result.invariants.end()) { + const auto& state = (point == prevail::InvariantPoint::post) ? it->second.post : it->second.pre; + if (!state.is_bottom()) { + obs_entry["invariant"] = invariant_to_json(state.to_set()); + } + } + } catch (const std::exception& e) { + obs_entry["ok"] = false; + obs_entry["message"] = e.what(); + } + obs_results.push_back(obs_entry); + } + j["observations"] = obs_results; + } + + return j; +} + +// ─── Tool: get_disassembly ───────────────────────────────────────────────────── + +static json handle_get_disassembly(const json& args, AnalysisEngine& engine) { + const std::string elf_path = args.at("elf_path").get(); + const std::string section = args.value("section", ""); + const std::string program = args.value("program", ""); + const std::string type = args.value("program_type", ""); + const int from_pc = args.value("from_pc", -1); + const int to_pc = args.value("to_pc", -1); + + const auto& session = engine.analyze(elf_path, section, program, type); + + json instructions = json::array(); + int pc = 0; + for (const auto& [label, inst, line_info] : session.inst_seq) { + if ((from_pc >= 0 && pc < from_pc) || (to_pc >= 0 && pc > to_pc)) { + pc += prevail::size(inst); + continue; + } + + json entry = {{"pc", pc}}; + std::ostringstream os; + os << inst; + entry["text"] = os.str(); + + if (line_info.has_value()) { + entry["source"] = line_info_to_json(*line_info); + } + + instructions.push_back(entry); + pc += prevail::size(inst); + } + + return {{"instructions", instructions}, {"count", static_cast(instructions.size())}}; +} + +// ─── Tool Registration ───────────────────────────────────────────────────────── + +void register_all_tools(McpServer& server, AnalysisEngine& engine) { + server.register_tool({ + "list_programs", + "List all eBPF programs (sections and function names) in an ELF file.", + {{"type", "object"}, + {"properties", {{"elf_path", {{"type", "string"}, {"description", "Path to .o ELF file"}}}}}, + {"required", json::array({"elf_path"})}}, + [&engine](const json& args) { return handle_list_programs(args, engine); }, + }); + + server.register_tool({ + "verify_program", + "Quick pass/fail check. Returns verification result, error count, exit value range, and instruction count. " + "Use this first to confirm whether a program passes or fails before deeper analysis with get_slice.", + {{"type", "object"}, + {"properties", + {{"elf_path", {{"type", "string"}, {"description", "Path to .o ELF file"}}}, + {"section", {{"type", "string"}, {"description", "ELF section name (optional)"}}}, + {"program", {{"type", "string"}, {"description", "Program/function name (optional)"}}}, + {"program_type", + {{"type", "string"}, {"description", "Program type name override (e.g. \"xdp\", \"bind\")"}}}, + {"check_termination", + {{"type", "boolean"}, + {"description", + "Check for termination (loop bounds). Default: platform-specific. Only override by user request."}}}, + {"allow_division_by_zero", + {{"type", "boolean"}, + {"description", + "Allow division by zero per BPF ISA semantics. Default: true. Only override by user request."}}}, + {"strict", + {{"type", "boolean"}, + {"description", + "Enable strict mode (additional runtime failure checks). Default: false. " + "Only override by user request."}}}}}, + {"required", json::array({"elf_path"})}}, + [&engine](const json& args) { return handle_verify_program(args, engine); }, + }); + + server.register_tool({ + "get_invariant", + "Get the pre or post invariant (abstract state) at one or more BPF instructions. Shows register types, value " + "ranges, and all constraints the verifier has proven at that point.", + {{"type", "object"}, + {"properties", + {{"elf_path", {{"type", "string"}}}, + {"pcs", + {{"type", "array"}, {"items", {{"type", "integer"}}}, {"description", "Program counter(s) to query"}}}, + {"point", {{"type", "string"}, {"enum", json::array({"pre", "post"})}, {"default", "pre"}}}, + {"section", {{"type", "string"}}}, + {"program", {{"type", "string"}}}, + {"program_type", + {{"type", "string"}, {"description", "Program type name override (e.g. \"xdp\", \"bind\")"}}}}}, + {"required", json::array({"elf_path", "pcs"})}}, + [&engine](const json& args) { return handle_get_invariant(args, engine); }, + }); + + server.register_tool({ + "get_instruction", + "Deep dive on specific instructions: disassembly text, safety assertions, pre/post invariants, " + "verification error (if any), source line, and CFG neighbors. Use after get_slice to inspect " + "individual instructions in detail, especially to compare pre vs post invariants across a helper call.", + {{"type", "object"}, + {"properties", + {{"elf_path", {{"type", "string"}}}, + {"pcs", + {{"type", "array"}, {"items", {{"type", "integer"}}}, {"description", "Program counter(s) to query"}}}, + {"section", {{"type", "string"}}}, + {"program", {{"type", "string"}}}, + {"program_type", + {{"type", "string"}, {"description", "Program type name override (e.g. \"xdp\", \"bind\")"}}}}}, + {"required", json::array({"elf_path", "pcs"})}}, + [&engine](const json& args) { return handle_get_instruction(args, engine); }, + }); + + server.register_tool({ + "get_errors", + "List all verification errors with pre-invariants and source lines, plus unreachable code. " + "Use for a quick overview of all errors in a multi-error program. Does NOT include failure slices — " + "use get_slice with error_index for detailed causal analysis of a specific error.", + {{"type", "object"}, + {"properties", + {{"elf_path", {{"type", "string"}}}, + {"section", {{"type", "string"}}}, + {"program", {{"type", "string"}}}, + {"program_type", + {{"type", "string"}, {"description", "Program type name override (e.g. \"xdp\", \"bind\")"}}}}}, + {"required", json::array({"elf_path"})}}, + [&engine](const json& args) { return handle_get_errors(args, engine); }, + }); + + server.register_tool({ + "get_cfg", + "Get the control-flow graph: basic blocks with instruction PCs and edges. Supports JSON or DOT format.", + {{"type", "object"}, + {"properties", + {{"elf_path", {{"type", "string"}}}, + {"format", {{"type", "string"}, {"enum", json::array({"json", "dot"})}, {"default", "json"}}}, + {"section", {{"type", "string"}}}, + {"program", {{"type", "string"}}}, + {"program_type", + {{"type", "string"}, {"description", "Program type name override (e.g. \"xdp\", \"bind\")"}}}}}, + {"required", json::array({"elf_path"})}}, + [&engine](const json& args) { return handle_get_cfg(args, engine); }, + }); + + server.register_tool({ + "get_source_mapping", + "Map between C source lines and BPF instructions. Query by PC to find source, by source_line to find BPF " + "instructions, or omit both to get the full map. Requires ELF compiled with -g.", + {{"type", "object"}, + {"properties", + {{"elf_path", {{"type", "string"}}}, + {"pc", {{"type", "integer"}, {"description", "BPF instruction PC to look up"}}}, + {"source_line", {{"type", "integer"}, {"description", "C source line number to look up"}}}, + {"source_file", {{"type", "string"}, {"description", "Source file name filter (optional)"}}}, + {"section", {{"type", "string"}}}, + {"program", {{"type", "string"}}}, + {"program_type", + {{"type", "string"}, {"description", "Program type name override (e.g. \"xdp\", \"bind\")"}}}}}, + {"required", json::array({"elf_path"})}}, + [&engine](const json& args) { return handle_get_source_mapping(args, engine); }, + }); + + server.register_tool({ + "check_constraint", + "Test hypotheses about the verifier's abstract state at a given instruction. " + "Use 'proven' mode to test if the verifier guarantees a constraint (e.g., 'is packet_size >= 42 proven?'). " + "Use 'consistent' mode to test if a constraint is possible (not contradicted). " + "WARNING: 'consistent' returns ok=true for variables absent from the invariant (vacuously true) — " + "always check the 'invariant' field in the response to confirm the variable is tracked. " + "Supports batch mode: pass 'checks' array to test multiple hypotheses in a single call.", + {{"type", "object"}, + {"properties", + {{"elf_path", {{"type", "string"}}}, + {"pc", {{"type", "integer"}}}, + {"constraints", + {{"type", "array"}, {"items", {{"type", "string"}}}, {"description", "Constraint strings to check"}}}, + {"checks", + {{"type", "array"}, + {"description", "Batch mode: array of checks to run in a single analysis pass. " + "Each check has pc, constraints, and optional mode/point overrides."}, + {"items", + {{"type", "object"}, + {"properties", + {{"pc", {{"type", "integer"}}}, + {"constraints", {{"type", "array"}, {"items", {{"type", "string"}}}}}, + {"mode", {{"type", "string"}, {"enum", json::array({"consistent", "entailed", "proven"})}}}, + {"point", {{"type", "string"}, {"enum", json::array({"pre", "post"})}}}}}, + {"required", json::array({"pc", "constraints"})}}}}}, + {"point", {{"type", "string"}, {"enum", json::array({"pre", "post"})}, {"default", "pre"}}}, + {"mode", + {{"type", "string"}, + {"enum", json::array({"consistent", "entailed", "proven"})}, + {"default", "consistent"}, + {"description", + "consistent: constraints are possible (not contradicted). " + "proven: verifier guarantees the constraints (invariant implies observation). " + "entailed: observation is a sub-state of invariant (requires near-complete constraint set)."}}}, + {"section", {{"type", "string"}}}, + {"program", {{"type", "string"}}}, + {"program_type", + {{"type", "string"}, {"description", "Program type name override (e.g. \"xdp\", \"bind\")"}}}}}, + {"required", json::array({"elf_path"})}}, + [&engine](const json& args) { return handle_check_constraint(args, engine); }, + }); + + server.register_tool({ + "get_slice", + "START HERE for failure diagnosis or understanding any instruction. Returns the pre-invariant, assertions, " + "source line, and a backward slice of only the instructions that causally contributed — with per-instruction " + "register relevance tracking. For errors: omit 'pc' to slice the first error. For passing programs: set 'pc' " + "to slice backward from any instruction (e.g., to understand why a read is safe or what feeds a helper call). " + "Read the pre-invariant directly: if a register is listed, it is proven; if absent, it was invalidated.", + {{"type", "object"}, + {"properties", + {{"elf_path", {{"type", "string"}}}, + {"error_index", + {{"type", "integer"}, {"default", 0}, {"description", "Which error to examine (0 = first)"}}}, + {"pc", + {{"type", "integer"}, + {"description", "Slice backward from this PC instead of an error (overrides error_index)"}}}, + {"trace_depth", + {{"type", "integer"}, + {"default", 200}, + {"description", "Maximum backward steps for slicing (default: 200)"}}}, + {"section", {{"type", "string"}}}, + {"program", {{"type", "string"}}}, + {"program_type", + {{"type", "string"}, {"description", "Program type name override (e.g. \"xdp\", \"bind\")"}}}, + {"check_termination", + {{"type", "boolean"}, + {"description", + "Check for termination (loop bounds). Default: platform-specific. Only override by user request."}}}, + {"allow_division_by_zero", + {{"type", "boolean"}, + {"description", + "Allow division by zero per BPF ISA semantics. Default: true. Only override by user request."}}}, + {"strict", + {{"type", "boolean"}, + {"description", + "Enable strict mode (additional runtime failure checks). Default: false. " + "Only override by user request."}}}}}, + {"required", json::array({"elf_path"})}}, + [&engine](const json& args) { return handle_get_slice(args, engine); }, + }); + + server.register_tool({ + "get_disassembly", + "Get the disassembly listing for a range of instructions. Returns instruction text and source lines. " + "Use from_pc/to_pc to limit the range, or omit for the full listing.", + {{"type", "object"}, + {"properties", + {{"elf_path", {{"type", "string"}}}, + {"from_pc", {{"type", "integer"}, {"description", "Start PC (inclusive, default: 0)"}}}, + {"to_pc", {{"type", "integer"}, {"description", "End PC (inclusive, default: last)"}}}, + {"section", {{"type", "string"}}}, + {"program", {{"type", "string"}}}, + {"program_type", + {{"type", "string"}, {"description", "Program type name override (e.g. \"xdp\", \"bind\")"}}}}}, + {"required", json::array({"elf_path"})}}, + [&engine](const json& args) { return handle_get_disassembly(args, engine); }, + }); + + server.register_tool({ + "verify_assembly", + "Verify a block of BPF assembly text without needing a compiled ELF file. " + "Useful for quickly testing instruction sequences, validating fix ideas, or exploring verifier behavior. " + "Syntax: one instruction per line (e.g., 'r0 = r1', 'call 1', 'if r0 == 0 goto ', 'exit'). " + "Labels: ':' on a separate line. Helper IDs: 1=map_lookup, 2=map_update. " + "If 'pre' is omitted, uses standard program entry state (r1=ctx, r10=stack). " + "If 'pre' is provided, only those constraints apply (for testing specific register states).", + {{"type", "object"}, + {"properties", + {{"code", + {{"type", "string"}, + {"description", + "BPF assembly instructions, one per line. " + "Example: \"r0 = 0\\nexit\". Labels: \":\\nr0 += 1\\nif r0 < 10 goto \\nexit\"."}}}, + {"pre", + {{"type", "array"}, + {"items", {{"type", "string"}}}, + {"description", + "Pre-invariant constraints (e.g., [\"r1.type=map_fd\", \"r1.map_fd=1\"]). " + "If omitted, uses standard entry state (r1=ctx, r10=stack)."}}}, + {"program_type", + {{"type", "string"}, + {"default", "xdp"}, + {"description", + "Program type name (e.g., \"xdp\", \"bind\"). Determines available helpers and context layout. " + "Default: \"xdp\"."}}}, + {"map_key_size", {{"type", "integer"}, {"default", 4}, {"description", "Map key size in bytes."}}}, + {"map_value_size", {{"type", "integer"}, {"default", 4}, {"description", "Map value size in bytes."}}}, + {"check_termination", + {{"type", "boolean"}, + {"description", "Check for termination. Default: platform-specific. Only override by user request."}}}, + {"allow_division_by_zero", + {{"type", "boolean"}, + {"description", + "Allow division by zero per BPF ISA semantics. Default: true. Only override by user request."}}}, + {"strict", + {{"type", "boolean"}, + {"description", + "Enable strict mode. Default: false. Only override by user request."}}}, + {"big_endian", + {{"type", "boolean"}, + {"default", false}, + {"description", "Analyze as big-endian BPF program. Default: false (little-endian)."}}}, + {"observe", + {{"type", "array"}, + {"description", + "Check intermediate invariants at specific PCs. Each entry has pc, constraints, " + "and optional point (pre/post) and mode (consistent/entailed)."}, + {"items", + {{"type", "object"}, + {"properties", + {{"pc", {{"type", "integer"}, {"description", "Instruction PC to observe"}}}, + {"label", {{"type", "string"}, {"description", "Label to observe (e.g. \"exit\")"}}}, + {"constraints", {{"type", "array"}, {"items", {{"type", "string"}}}}}, + {"point", {{"type", "string"}, {"enum", json::array({"pre", "post"})}, {"default", "pre"}}}, + {"mode", + {{"type", "string"}, + {"enum", json::array({"consistent", "entailed"})}, + {"default", "consistent"}}}}}, + {"required", json::array({"constraints"})}}}}}}}, + {"required", json::array({"code"})}}, + [&engine](const json& args) { return handle_verify_assembly(args, engine); }, + }); +} + +} // namespace prevail \ No newline at end of file diff --git a/src/mcp/tools.hpp b/src/mcp/tools.hpp new file mode 100644 index 000000000..97f2be120 --- /dev/null +++ b/src/mcp/tools.hpp @@ -0,0 +1,16 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT +#pragma once + +/// @file MCP tool declarations and registration. + +#include "analysis_engine.hpp" +#include "mcp_server.hpp" + +namespace prevail { + +/// Register all PREVAIL MCP tools with the server. +void +register_all_tools(McpServer& server, AnalysisEngine& engine); + +} // namespace prevail diff --git a/src/platform_ops.hpp b/src/platform_ops.hpp new file mode 100644 index 000000000..0d93f50aa --- /dev/null +++ b/src/platform_ops.hpp @@ -0,0 +1,104 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT +#pragma once + +/// @file Platform abstraction for the analysis engine. +/// Implementations provide platform-specific ELF validation, program enumeration, +/// TLS management, and verifier options. This allows the analysis engine to work +/// with different eBPF platforms (Linux, Windows) without compile-time dependencies. + +// Undef Windows macros that conflict with PREVAIL headers (std::numeric_limits::min/max). +#undef FALSE +#undef TRUE +#undef min +#undef max + +// Pre-define the include guard for bpf_conformance's ebpf_inst.h to prevent it +// from being included (its EbpfInst struct conflicts with prevail::EbpfInst). +#ifndef BPF_CONFORMANCE_CORE_EBPF_INST_H +#define BPF_CONFORMANCE_CORE_EBPF_INST_H +#endif + +#ifdef _MSC_VER +#pragma warning(push) +#pragma warning(disable : 4100) // Unreferenced formal parameter. +#pragma warning(disable : 4244) // Conversion, possible loss of data. +#pragma warning(disable : 4267) // Conversion from 'size_t' to 'int'. +#pragma warning(disable : 4458) // Declaration hides class member. +#pragma warning(disable : 26439) // Function may not throw. +#pragma warning(disable : 26450) // Arithmetic overflow. +#pragma warning(disable : 26451) // Arithmetic overflow. +#pragma warning(disable : 26495) // Always initialize a member variable. +#endif + +#include "ebpf_verifier.hpp" + +#ifdef _MSC_VER +#pragma warning(pop) +#endif + +#ifdef _WIN32 +#define FALSE 0 +#define TRUE 1 +#endif + +#include +#include +#include + +namespace prevail { + +/// Entry in the program list returned by PlatformOps::list_programs(). +struct ProgramEntry +{ + std::string section; + std::string function; +}; + +/// Abstract interface for platform-specific operations. +/// The analysis engine calls through this interface instead of directly using +/// platform-specific APIs. +struct PlatformOps +{ + virtual ~PlatformOps() = default; + + /// Get the PREVAIL platform pointer for read_elf/unmarshal/analyze. + [[nodiscard]] virtual const prevail::ebpf_platform_t* + platform() const = 0; + + /// List all programs (sections + function names) in an ELF file. + [[nodiscard]] virtual std::vector + list_programs(const std::string& elf_path) = 0; + + /// Validate ELF data before analysis. + /// @return true if valid (or if no validation is available). + virtual bool + validate_elf(const std::string& /*data*/) + { + return true; + } + + /// Prepare thread-local state before analysis. + /// Clears any cached TLS data and optionally sets a program type override. + virtual void + prepare_tls(const std::string& type_override) = 0; + + /// Get default verifier options for this platform. + [[nodiscard]] virtual prevail::ebpf_verifier_options_t + default_options() = 0; + + /// Attempt fallback verification to produce a clean error message + /// when direct PREVAIL analysis fails (e.g. due to access violation on Windows). + /// @return Error message string, or empty string if no fallback is available. + virtual std::string + fallback_verify( + const std::string& /*data*/, + const std::string& /*section*/, + const std::string& /*program*/, + const std::string& /*type*/) + { + return ""; + } +}; + +} // namespace prevail diff --git a/src/platform_ops_prevail.hpp b/src/platform_ops_prevail.hpp new file mode 100644 index 000000000..e4b477f27 --- /dev/null +++ b/src/platform_ops_prevail.hpp @@ -0,0 +1,60 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT +#pragma once + +/// @file Linux/portable PlatformOps implementation using only PREVAIL APIs. + +#include "platform_ops.hpp" + +namespace prevail { + +/// PlatformOps implementation using only PREVAIL's public API. +/// Works on Linux and Windows (when linking the PREVAIL library directly +/// without ebpf-for-windows). +class PrevailPlatformOps : public PlatformOps +{ + public: + explicit PrevailPlatformOps(const prevail::ebpf_platform_t* platform) : platform_(*platform) {} + explicit PrevailPlatformOps(prevail::ebpf_platform_t platform) : platform_(platform) {} + + [[nodiscard]] const prevail::ebpf_platform_t* + platform() const override + { + return &platform_; + } + + [[nodiscard]] std::vector + list_programs(const std::string& elf_path) override + { + prevail::ElfObject elf(elf_path, default_options(), &platform_); + std::vector result; + for (const auto& info : elf.list_programs()) { + if (prevail::ElfObject::is_valid(info)) { + result.push_back({info.section_name, info.function_name}); + } + } + return result; + } + + void + prepare_tls(const std::string& /*type_override*/) override + { + prevail::ebpf_verifier_clear_thread_local_state(); + } + + [[nodiscard]] prevail::ebpf_verifier_options_t + default_options() override + { + prevail::ebpf_verifier_options_t opts{}; + opts.mock_map_fds = true; + opts.setup_constraints = true; + opts.allow_division_by_zero = true; + opts.verbosity_opts.print_line_info = true; + return opts; + } + + private: + prevail::ebpf_platform_t platform_; +}; + +} // namespace prevail diff --git a/src/prevail_mcp.cpp b/src/prevail_mcp.cpp new file mode 100644 index 000000000..6500c8202 --- /dev/null +++ b/src/prevail_mcp.cpp @@ -0,0 +1,66 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT + +/// @file Entry point for the PREVAIL MCP server (portable/Linux build). + +#include "analysis_engine.hpp" +#include "mcp/mcp_server.hpp" +#include "mcp/mcp_transport.hpp" +#include "platform_ops_prevail.hpp" +#include "mcp/tools.hpp" + +#include "linux/gpl/spec_type_descriptors.hpp" + +#include +#include + +#ifndef _WIN32 +#include +#endif + +int +main() +{ + try { + // Set up the MCP output stream: duplicate stdout for exclusive MCP use, + // then redirect std::cout to std::cerr so that library diagnostics + // (e.g., verbose verifier output) don't corrupt the JSON-RPC framing. + // Note: fd-level stdout is left intact so that parent processes can pipe + // it normally (e.g., subprocess.Popen in Python, Start-Process in PowerShell). + FILE* mcp_out = stdout; +#ifndef _WIN32 + int mcp_fd = dup(fileno(stdout)); + if (mcp_fd >= 0) { + mcp_out = fdopen(mcp_fd, "wb"); + if (!mcp_out) { + close(mcp_fd); + mcp_out = stdout; // Fallback: use stdout directly. + } + } +#endif + setvbuf(mcp_out, nullptr, _IONBF, 0); + + // Redirect C++ std::cout to stderr so library diagnostics don't reach the client. + std::cout.rdbuf(std::cerr.rdbuf()); + + // Use the Linux eBPF platform from PREVAIL. + prevail::PrevailPlatformOps ops(&prevail::g_ebpf_platform_linux); + + prevail::AnalysisEngine engine(&ops); + prevail::McpServer server; + prevail::register_all_tools(server, engine); + + std::cerr << "prevail: server started" << std::endl; + + prevail::McpTransport transport(mcp_out); + transport.run([&server](const std::string& method, const nlohmann::json& params) { + return server.dispatch(method, params); + }); + + std::cerr << "prevail: server stopped" << std::endl; + return 0; + } catch (const std::exception& e) { + std::cerr << "prevail: fatal error: " << e.what() << std::endl; + return 1; + } +} diff --git a/src/result.cpp b/src/result.cpp index 39ab155e9..dd3e56f5f 100644 --- a/src/result.cpp +++ b/src/result.cpp @@ -377,269 +377,279 @@ std::set extract_assertion_registers(const Assertion& assertion) { assertion); } -std::vector AnalysisResult::compute_failure_slices(const Program& prog, const SliceParams params) const { - const auto max_steps = params.max_steps; - const auto max_slices = params.max_slices; - std::vector slices; - - // Find all labels with errors - for (const auto& [label, inv_pair] : invariants) { - if (inv_pair.pre.is_bottom()) { - continue; // Unreachable - } - if (!inv_pair.error) { - continue; // No error here - } - - // Check if we've reached the max slices limit - if (max_slices > 0 && slices.size() >= max_slices) { - break; - } - - FailureSlice slice{ - .failing_label = label, - .error = *inv_pair.error, - .relevance = {}, - }; - - // Seed relevant registers from the actual failing assertion. - // Forward analysis stops at the first failing assertion, which may not be - // assertions[0]. Replay the checks against the pre-state to identify - // the actual failing assertion and seed relevance from it. - RelevantState initial_relevance; - const auto& assertions = prog.assertions_at(label); - bool found_failing = false; - for (const auto& assertion : assertions) { - if (ebpf_domain_check(inv_pair.pre, assertion, label)) { - for (const auto& reg : extract_assertion_registers(assertion)) { - initial_relevance.registers.insert(reg); - } - found_failing = true; - break; - } - } - // Fallback: if no failing assertion was identified (shouldn't happen), - // or if the failing assertion has no register deps, aggregate all assertions. - if (!found_failing || initial_relevance.registers.empty()) { - for (const auto& assertion : assertions) { - for (const auto& reg : extract_assertion_registers(assertion)) { - initial_relevance.registers.insert(reg); - } - } - } +FailureSlice AnalysisResult::compute_slice_from_label(const Program& prog, const Label& label, + const RelevantState& seed_relevance, size_t max_steps) const { + FailureSlice slice{ + .failing_label = label, + .error = VerificationError(""), + .relevance = {}, + }; + + // Copy error if present at this label. + const auto label_it = invariants.find(label); + if (label_it != invariants.end() && label_it->second.error) { + slice.error = *label_it->second.error; + } - // Always include the failing label in the slice, even if no registers were extracted - // (e.g., BoundedLoopCount has no register deps) + // `visited` tracks all explored labels for deduplication during backward traversal. + // `slice_labels` tracks only labels that interact with relevant registers (the output slice). + std::map visited; + std::set