Draft
Conversation
|
Important Review skippedDraft detected. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Repository UI Review profile: ASSERTIVE Plan: Pro Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
WalkthroughAdds a Model Context Protocol (MCP) server and toolset: transport, JSON-RPC dispatch, analysis engine and platform adapters, JSON serializers, a suite of MCP tools, tests, docs, and CMake changes to build optional Changes
Estimated code review effort🎯 5 (Critical) | ⏱️ ~120 minutes Possibly related PRs
Suggested labels
🚥 Pre-merge checks | ✅ 1 | ❌ 2❌ Failed checks (1 warning, 1 inconclusive)
✅ Passed checks (1 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 20
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@src/mcp/analysis_engine.cpp`:
- Around line 219-221: The current code coercively maps any non-"entailed"
mode_str to prevail::ObservationCheckMode::consistent; change this to validate
mode_str explicitly: parse mode_str into a prevail::ObservationCheckMode by
checking for known values (e.g., "entailed" -> ObservationCheckMode::entailed,
"consistent" -> ObservationCheckMode::consistent) and if it doesn't match
either, return/propagate an error (or throw an exception / log and return a
failure) instead of defaulting; update the call site that uses
session_->live_result->check_observation_at_label(label, point, observation,
mode) to only run when parsing succeeds so unknown mode_str values are rejected
rather than coerced.
- Around line 48-63: The code seeds new_opts from current_opts_ causing
overrides to persist; instead initialize new_opts from a fresh default (e.g.,
VerificationOptions() or a default_options_ instance) so absent optional
parameters do not inherit previous call state, then apply the has_value()
overrides to new_opts, compare against current_opts_ and only reset session_ and
assign current_opts_ if the computed new_opts differs; reference
VerificationOptions, new_opts, current_opts_, session_ and the has_value checks
in the diff when making the change.
In `@src/mcp/analysis_engine.hpp`:
- Around line 110-112: The header comment for get_live_invariant is incorrect:
it claims the fallback is an "empty StringInvariant" but the implementation
returns prevail::StringInvariant::bottom(); update the contract to match the
implementation by changing the comment to state that when no session or label is
found the function returns StringInvariant::bottom(); mention
prevail::StringInvariant::bottom(), the function get_live_invariant(const
prevail::Label&, prevail::InvariantPoint) const, and that callers expecting an
"empty" invariant should convert or call to_set() as needed.
In `@src/mcp/mcp_transport.cpp`:
- Around line 20-21: The code reads peer-controlled Content-Length into
content_length (and uses found_content_length) and then allocates a buffer
directly from it; you must enforce a hard upper bound before any allocation or
resize. Add a MAX_CONTENT_LENGTH constant, validate content_length after parsing
(and before any vector.reserve/resize or new) to cap it or reject requests that
exceed the limit, and handle the error path cleanly (return error/log and avoid
allocating). Update all places that use content_length (the variables
content_length and found_content_length and the buffer allocation sites) so they
check/cap the value and prevent unbounded memory growth.
- Around line 138-141: The code extracts request metadata (method, params, id)
before entering the try block, causing nlohmann::json::type_error.306 when
request is not a JSON object; move the lines that compute method, params and
is_notification (the uses of request.value(...) and request["id"]) into the
existing try block and first validate request.is_object(), returning or throwing
a JSON-RPC "Invalid Request" error for non-object payloads; ensure all accesses
use request.value(...) or contains() inside the try to avoid direct [] access on
malformed JSON and produce a proper JSON-RPC error response instead of allowing
the exception to escape the message loop.
In `@src/mcp/mcp_transport.hpp`:
- Line 47: The comment for run is inaccurate: update the contract on the run
method in mcp_transport.hpp to state that the loop only exits on EOF (or input
stream closure) and does not exit when a handler throws because handler
exceptions are caught, converted to JSON-RPC error responses, and the loop
continues; reference the run method and the exception-to-JSON-RPC error handling
behavior so the comment accurately reflects that handler exceptions are handled
and do not terminate the loop.
In `@src/mcp/platform_ops.hpp`:
- Around line 37-38: Add the [[nodiscard]] attribute to the pure-virtual method
declaration for list_programs so callers are warned if they ignore the returned
std::vector<ProgramEntry>; update the declaration of list_programs(const
std::string& elf_path) in platform_ops.hpp to include [[nodiscard]] (e.g.
[[nodiscard]] virtual std::vector<ProgramEntry> list_programs(const std::string&
elf_path) = 0;) so the compiler emits a warning when the return value is
discarded.
- Around line 33-34: Add the [[nodiscard]] attribute to the virtual method
declaration platform() so callers are warned if they ignore the returned
prevail::ebpf_platform_t*; update the declaration virtual const
prevail::ebpf_platform_t* platform() const = 0; to virtual [[nodiscard]] const
prevail::ebpf_platform_t* platform() const = 0; and propagate the attribute to
all overrides/implementations of platform() (matching signatures in derived
classes) to ensure the compiler enforces checking the return value.
- Around line 54-55: The method prevail::ebpf_verifier_options_t
default_options() should be marked [[nodiscard]] to prevent callers from
accidentally ignoring the returned options; update the declaration of
default_options() in platform_ops.hpp to be [[nodiscard]] virtual
prevail::ebpf_verifier_options_t default_options() = 0; and propagate the same
[[nodiscard]] attribute to all overriding implementations (methods named
default_options in derived classes) so the compiler enforces non-discard
semantics across the hierarchy.
In `@src/mcp/prevail_headers.hpp`:
- Around line 10-12: The header currently defines the include guard macro
BPF_CONFORMANCE_CORE_EBPF_INST_H and immediately closes it, which is
non‑obvious; update src/mcp/prevail_headers.hpp by adding a brief comment next
to the macro (BPF_CONFORMANCE_CORE_EBPF_INST_H) explaining that the empty guard
intentionally marks this header as a sentinel/placeholder (to prevent multiple
inclusion or to signal no declarations are needed here) so future readers
understand why the guard is present without any content.
In `@src/mcp/README.md`:
- Around line 64-76: The tool list in the MCP README is missing the exposed tool
verify_assembly; add a new table row for `verify_assembly` alongside the
existing entries (e.g., near `verify_program` / `get_invariant`) with a concise
description such as "Verify assembled BPF code/assembly and report pass/fail
with error summary" so MCP clients can discover this tool; ensure the backtick
name `verify_assembly` matches the exposed tool identifier exactly.
- Around line 34-36: The fenced code block containing "/mcp add" in README.md is
missing a language tag (triggering markdownlint MD040); update that fenced block
to include an explicit language identifier such as "text" (i.e., change the
triple-backtick fence to ```text) so the block is typed and linter warnings are
resolved.
- Around line 29-30: Update the README sentence "The server communicates via
JSON-RPC 2.0 over stdio (newline-delimited JSON)." to state that the MCP
supports both Content-Length framed JSON-RPC (HTTP-like) and newline-delimited
JSON (NDJSON) over stdio, and revise the usage section/examples to show both
framing modes (Content-Length headers example and NDJSON example) so the docs
match runtime behavior.
In `@src/mcp/tools.cpp`:
- Around line 570-571: The code reads a caller-controlled trace_depth via
args.value("trace_depth", 200) without bounds; clamp this value before any
slicing or heavy work by introducing a bounded variable (e.g., compute size_t
bounded_trace_depth = std::clamp(trace_depth, MIN_TRACE_DEPTH, MAX_TRACE_DEPTH)
or equivalent) and use bounded_trace_depth wherever trace_depth is passed into
slicing logic; define sensible MIN_TRACE_DEPTH and MAX_TRACE_DEPTH constants
(for example MIN=1 and a reasonable upper limit) and validate/adjust the value
coming from args.value before any use (also keep opt_termination handling
unchanged).
- Around line 758-760: In verify_assembly, after reading map_key_size and
map_value_size from args via args.value, validate that both are strictly
positive and reject invalid values immediately (e.g., log an error and return
false or throw) instead of forwarding them into the map descriptor creation
later; update the code that constructs the map descriptors (the block that uses
map_key_size and map_value_size around the map descriptor creation) to assume
only positive sizes by failing fast when map_key_size <= 0 or map_value_size <=
0, referencing the variables map_key_size, map_value_size and the
verify_assembly function to locate the change.
- Around line 883-899: The code silently treats any unknown observation label as
prevail::Label::entry which causes misrouting; in the label-handling branch (the
obs.contains("label") block) explicitly check for known labels (e.g. "exit" and
"entry") and set label to prevail::Label::exit or prevail::Label::entry
accordingly, and for any other string throw a std::runtime_error (including the
unknown label value) instead of leaving label as the default; ensure obs_entry
is still set to {{"label", label_str}} and preserve the existing
obs.contains("pc") branch that sets label via prevail::Label{obs_pc, -1, {}}.
- Around line 713-719: The code builds label_map and advances pc by
block.instructions.size(), which counts instructions not BPF slots; replace the
simple size increment with summing each instruction's slot-size so pc advances
by the actual BPF slot count per instruction (e.g., iterate block.instructions
and add the instruction's slot-size getter/field for each instruction), and
apply the same change in the later loop that advances pc (the block iteration
around lines ~725-744) so jump targets and observation PCs use slot-accurate
PCs; update uses of pc, prevail::Label, and block.instructions accordingly.
In `@src/prevail_mcp.cpp`:
- Around line 31-38: The dup(fd) + fdopen() block can leak the duplicated
descriptor mcp_fd when fdopen(fails) returns null; update the code around
mcp_fd, dup(fileno(stdout)), and the fdopen call so that if fdopen(mcp_fd, "wb")
returns nullptr you call close(mcp_fd) and then set mcp_out = stdout as the
fallback (or otherwise ensure the descriptor is closed before abandoning it),
keeping the successful-path behavior of assigning mcp_out to the fdopen result
when it succeeds.
In `@src/result.cpp`:
- Around line 380-554: The compute_slice_from_label function is overly
complex—extract the dependency-analysis and contribution-determination logic
into a helper compute_relevant_before(const Program&, const Label&, const
RelevantState&, const InvariantDeps&, const std::vector<Label>&
parents_of_target, bool conservative_mode) that returns RelevantState and a bool
indicating instruction_contributes (use symbols deps, relevant_after,
relevant_before, instruction_contributes), and extract the predecessor/worklist
expansion logic into expand_join_points(const Program&, Label, const
RelevantState&, std::vector<std::pair<Label,RelevantState>>& worklist) to
encapsulate parents_of/current parent handling; replace the inlined blocks in
compute_slice_from_label with calls to these helpers to reduce cognitive
complexity while preserving behavior (keep uses of invariants, slice_labels,
visited, conservative_visited, and steps unchanged).
In `@src/test/test_mcp.cpp`:
- Around line 247-365: Add two deterministic tests to src/test/test_mcp.cpp
using McpTestHarness::call_tool: (1) a sound regression named like
"verify_assembly: wide-instruction pc mapping" that supplies assembly containing
a multi-slot/wide instruction sequence and an observe entry using a pc that hits
the second slot; assert the result["passed"] == true and correct
instruction_count mapping so multi-slot PCs map to the expected instruction
index; (2) an unsound regression named like "verify_assembly: observe invalid
label" that calls verify_assembly with an observe entry using an
unsupported/invalid label string and assert the tool throws or returns failure
(REQUIRE_THROWS or REQUIRE(result["passed"] == false)) to ensure invalid
observe.label is rejected; use the same call pattern as other TEST_CASEs
(McpTestHarness h; h.call_tool(...)) and mirror existing assertion style to keep
tests deterministic.
ℹ️ Review info
Configuration used: Repository UI
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (22)
CMakeLists.txtREADME.mddocs/README.mddocs/llm-context.mdsrc/mcp/README.mdsrc/mcp/analysis_engine.cppsrc/mcp/analysis_engine.hppsrc/mcp/json_serializers.cppsrc/mcp/json_serializers.hppsrc/mcp/mcp_server.cppsrc/mcp/mcp_server.hppsrc/mcp/mcp_transport.cppsrc/mcp/mcp_transport.hppsrc/mcp/platform_ops.hppsrc/mcp/platform_ops_prevail.hppsrc/mcp/prevail_headers.hppsrc/mcp/tools.cppsrc/mcp/tools.hppsrc/prevail_mcp.cppsrc/result.cppsrc/result.hppsrc/test/test_mcp.cpp
Comment on lines
+48
to
+63
| VerificationOptions new_opts = current_opts_; | ||
| if (check_termination.has_value()) { | ||
| new_opts.check_termination = *check_termination; | ||
| } | ||
| if (allow_division_by_zero.has_value()) { | ||
| new_opts.allow_division_by_zero = *allow_division_by_zero; | ||
| } | ||
| if (strict.has_value()) { | ||
| new_opts.strict = *strict; | ||
| } | ||
|
|
||
| // If options changed, invalidate the current session. | ||
| if (new_opts != current_opts_) { | ||
| session_.reset(); | ||
| current_opts_ = new_opts; | ||
| } |
There was a problem hiding this comment.
Option overrides persist across later calls without explicit overrides.
Lines 48-63 seed new_opts from current_opts_, so a single overridden call changes behavior of subsequent calls that omit options. This makes tool results order-dependent.
Proposed fix
- VerificationOptions new_opts = current_opts_;
+ const auto defaults = ops_->default_options();
+ VerificationOptions new_opts{
+ defaults.cfg_opts.check_for_termination,
+ defaults.allow_division_by_zero,
+ defaults.strict,
+ };
if (check_termination.has_value()) {
new_opts.check_termination = *check_termination;
}
if (allow_division_by_zero.has_value()) {
new_opts.allow_division_by_zero = *allow_division_by_zero;
}
if (strict.has_value()) {
new_opts.strict = *strict;
}🧰 Tools
🪛 Cppcheck (2.19.0)
[performance] 49-49: Function parameter 'variable_terms' should be passed by const reference.
(passedByValue)
[style] 49-49: The function 'call_stack_depth' is never used.
(unusedFunction)
[style] 50-50: The function 'is_valid' is never used.
(unusedFunction)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/mcp/analysis_engine.cpp` around lines 48 - 63, The code seeds new_opts
from current_opts_ causing overrides to persist; instead initialize new_opts
from a fresh default (e.g., VerificationOptions() or a default_options_
instance) so absent optional parameters do not inherit previous call state, then
apply the has_value() overrides to new_opts, compare against current_opts_ and
only reset session_ and assign current_opts_ if the computed new_opts differs;
reference VerificationOptions, new_opts, current_opts_, session_ and the
has_value checks in the diff when making the change.
Comment on lines
+20
to
+21
| size_t content_length = 0; | ||
| bool found_content_length = false; |
There was a problem hiding this comment.
Cap Content-Length before buffer allocation.
Line 49 allocates directly from peer-controlled Content-Length. This allows unbounded memory growth from malformed input.
Suggested fix
size_t content_length = 0;
+ constexpr size_t kMaxContentLength = 16 * 1024 * 1024; // 16 MiB
@@
content_length = std::stoull(line.substr(prefix.size()));
+ if (content_length > kMaxContentLength) {
+ return nullptr;
+ }
found_content_length = true;Also applies to: 35-36, 49-50
🧰 Tools
🪛 Clang (14.0.6)
[warning] 20-20: variable 'content_length' is not initialized
(cppcoreguidelines-init-variables)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/mcp/mcp_transport.cpp` around lines 20 - 21, The code reads
peer-controlled Content-Length into content_length (and uses
found_content_length) and then allocates a buffer directly from it; you must
enforce a hard upper bound before any allocation or resize. Add a
MAX_CONTENT_LENGTH constant, validate content_length after parsing (and before
any vector.reserve/resize or new) to cap it or reject requests that exceed the
limit, and handle the error path cleanly (return error/log and avoid
allocating). Update all places that use content_length (the variables
content_length and found_content_length and the buffer allocation sites) so they
check/cap the value and prevent unbounded memory growth.
Comment on lines
+138
to
+141
| 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(); | ||
|
|
There was a problem hiding this comment.
🧩 Analysis chain
🌐 Web query:
nlohmann json v3.12.0 value() contains() method non-object type_error exception
💡 Result:
In nlohmann::json v3.12.0:
-
j.value("key", default)(the key-based overload) requiresjto be a JSON object.
Ifjis not an object (e.g.,null, array, string, number), it throwsjson.exception.type_error.306(“cannot use value() with …”). [1][3]Fix: guard or ensure object:
if (j.is_object()) x = j.value("key", default_value); else x = default_value; // or: j = nlohmann::json::object();
(If your
jsonwas default-constructed, it’snull, not{}—initialize asjson::object()/json({})if you need an empty object.) [1][3] -
j.contains("key")is safe on any JSON type: ifjis not an object, it simply returnsfalse(notype_error). [2]
Notes:
contains(json_pointer)can throwparse_errorfor malformed pointers/array indices, but that’s unrelated to the non-objecttype_erroryou’re seeing withvalue(). [2]
Sources: value() docs (type_error.306) [1], contains() docs (returns false if not object) [2], exception listing for type_error.306 [3].
🏁 Script executed:
# First, find and read the actual file to see the context
fd -t f "mcp_transport.cpp" --exec wc -l {} \;Repository: vbpf/prevail
Length of output: 87
🏁 Script executed:
# Get the relevant section of code
sed -n '130,160p' src/mcp/mcp_transport.cppRepository: vbpf/prevail
Length of output: 1180
🏁 Script executed:
# Check lines 142-153 to see what the "Also applies to" section is
sed -n '142,153p' src/mcp/mcp_transport.cppRepository: vbpf/prevail
Length of output: 463
Move request metadata extraction inside try block with object validation.
request.value("method", "") and request.value("params", ...) throw type_error.306 when request is not a JSON object. These calls on lines 138-139 execute before the try block, so exceptions bypass error handling and kill the message loop. Malformed requests (null, array, etc.) will crash the connection instead of returning a JSON-RPC error response.
Guard with is_object() and move extraction inside the try block:
Suggested fix
- 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 {
+ if (!request.is_object() || !request.contains("method") || !request["method"].is_string()) {
+ nlohmann::json error_response = {
+ {"jsonrpc", "2.0"},
+ {"id", request.is_object() && request.contains("id") ? request["id"] : nlohmann::json(nullptr)},
+ {"error", {{"code", -32600}, {"message", "Invalid Request"}}},
+ };
+ write_message(error_response);
+ continue;
+ }
+
+ const std::string method = request["method"].get<std::string>();
+ const nlohmann::json params = request.value("params", nlohmann::json::object());
+ const bool is_notification = !request.contains("id") || request["id"].is_null();
nlohmann::json result = handler(method, params);Also applies to: 142-153 (unsafe request["id"] access on non-object payloads)
🧰 Tools
🪛 Clang (14.0.6)
[warning] 138-138: variable 'method' is not initialized
(cppcoreguidelines-init-variables)
[warning] 139-139: variable 'params' is not initialized
(cppcoreguidelines-init-variables)
[warning] 140-140: variable 'is_notification' is not initialized
(cppcoreguidelines-init-variables)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/mcp/mcp_transport.cpp` around lines 138 - 141, The code extracts request
metadata (method, params, id) before entering the try block, causing
nlohmann::json::type_error.306 when request is not a JSON object; move the lines
that compute method, params and is_notification (the uses of request.value(...)
and request["id"]) into the existing try block and first validate
request.is_object(), returning or throwing a JSON-RPC "Invalid Request" error
for non-object payloads; ensure all accesses use request.value(...) or
contains() inside the try to avoid direct [] access on malformed JSON and
produce a proper JSON-RPC error response instead of allowing the exception to
escape the message loop.
Comment on lines
+758
to
+760
| const int map_key_size = args.value("map_key_size", 4); | ||
| const int map_value_size = args.value("map_value_size", 4); | ||
|
|
There was a problem hiding this comment.
Reject invalid map sizes in verify_assembly.
Lines 758-759 accept non-positive values and forward them into map descriptors at Lines 804-815. Fail fast on invalid sizes.
Proposed fix
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");
+ }Also applies to: 804-815
🧰 Tools
🪛 Clang (14.0.6)
[warning] 758-758: variable 'map_key_size' is not initialized
(cppcoreguidelines-init-variables)
[warning] 759-759: variable 'map_value_size' is not initialized
(cppcoreguidelines-init-variables)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/mcp/tools.cpp` around lines 758 - 760, In verify_assembly, after reading
map_key_size and map_value_size from args via args.value, validate that both are
strictly positive and reject invalid values immediately (e.g., log an error and
return false or throw) instead of forwarding them into the map descriptor
creation later; update the code that constructs the map descriptors (the block
that uses map_key_size and map_value_size around the map descriptor creation) to
assume only positive sizes by failing fast when map_key_size <= 0 or
map_value_size <= 0, referencing the variables map_key_size, map_value_size and
the verify_assembly function to locate the change.
Comment on lines
+883
to
+899
| prevail::Label label = prevail::Label::entry; | ||
| json obs_entry = json::object(); | ||
| if (obs.contains("pc")) { | ||
| const int obs_pc = obs["pc"].get<int>(); | ||
| 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<std::string>(); | ||
| if (label_str == "exit") { | ||
| label = prevail::Label::exit; | ||
| } | ||
| obs_entry = {{"label", label_str}}; | ||
| } | ||
|
|
There was a problem hiding this comment.
Do not silently coerce unknown observation labels to entry.
Lines 892-898 only resolve "exit". Any other label currently falls back to Label::entry, which checks the wrong location.
Proposed fix
} else if (obs.contains("label")) {
const std::string label_str = obs["label"].get<std::string>();
if (label_str == "exit") {
label = prevail::Label::exit;
+ } else {
+ throw std::runtime_error("Unsupported observe label: " + label_str);
}
obs_entry = {{"label", label_str}};
+ } else {
+ throw std::runtime_error("observe entry must include either 'pc' or 'label'");
}🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/mcp/tools.cpp` around lines 883 - 899, The code silently treats any
unknown observation label as prevail::Label::entry which causes misrouting; in
the label-handling branch (the obs.contains("label") block) explicitly check for
known labels (e.g. "exit" and "entry") and set label to prevail::Label::exit or
prevail::Label::entry accordingly, and for any other string throw a
std::runtime_error (including the unknown label value) instead of leaving label
as the default; ensure obs_entry is still set to {{"label", label_str}} and
preserve the existing obs.contains("pc") branch that sets label via
prevail::Label{obs_pc, -1, {}}.
Comment on lines
+31
to
+38
| #ifndef _WIN32 | ||
| int mcp_fd = dup(fileno(stdout)); | ||
| if (mcp_fd >= 0) { | ||
| mcp_out = fdopen(mcp_fd, "wb"); | ||
| if (!mcp_out) { | ||
| mcp_out = stdout; // Fallback: use stdout directly. | ||
| } | ||
| } |
There was a problem hiding this comment.
Resource leak: mcp_fd is not closed if fdopen fails.
If fdopen returns null, the duplicated file descriptor mcp_fd is leaked.
🔧 Proposed fix
`#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`📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| #ifndef _WIN32 | |
| int mcp_fd = dup(fileno(stdout)); | |
| if (mcp_fd >= 0) { | |
| mcp_out = fdopen(mcp_fd, "wb"); | |
| if (!mcp_out) { | |
| mcp_out = stdout; // Fallback: use stdout directly. | |
| } | |
| } | |
| `#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` |
🧰 Tools
🪛 Clang (14.0.6)
[warning] 32-32: variable 'mcp_fd' is not initialized
(cppcoreguidelines-init-variables)
🪛 Cppcheck (2.19.0)
[style] 32-32: The function 'make_increment_counter' is never used.
(unusedFunction)
[style] 35-35: The function 'instruction_at' is never used.
(unusedFunction)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/prevail_mcp.cpp` around lines 31 - 38, The dup(fd) + fdopen() block can
leak the duplicated descriptor mcp_fd when fdopen(fails) returns null; update
the code around mcp_fd, dup(fileno(stdout)), and the fdopen call so that if
fdopen(mcp_fd, "wb") returns nullptr you call close(mcp_fd) and then set mcp_out
= stdout as the fallback (or otherwise ensure the descriptor is closed before
abandoning it), keeping the successful-path behavior of assigning mcp_out to the
fdopen result when it succeeds.
Comment on lines
+380
to
+554
| 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<Label, RelevantState> visited; | ||
| std::set<Label> conservative_visited; // Dedup for empty-relevance labels in conservative mode | ||
| std::map<Label, RelevantState> slice_labels; | ||
|
|
||
| // `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<Label, RelevantState> visited; | ||
| std::set<Label> conservative_visited; // Dedup for empty-relevance labels in conservative mode | ||
| std::map<Label, RelevantState> slice_labels; | ||
| // Worklist: (label, relevant_state_after_this_label) | ||
| std::vector<std::pair<Label, RelevantState>> worklist; | ||
| worklist.emplace_back(label, seed_relevance); | ||
|
|
||
| // Worklist: (label, relevant_state_after_this_label) | ||
| std::vector<std::pair<Label, RelevantState>> worklist; | ||
| worklist.emplace_back(label, initial_relevance); | ||
| // When the seed has no register/stack deps (e.g., BoundedLoopCount), | ||
| // perform a conservative backward walk so the slice still shows the | ||
| // loop structure and control flow leading to the failure. | ||
| const bool conservative_mode = seed_relevance.registers.empty() && seed_relevance.stack_offsets.empty(); | ||
|
|
||
| // When the seed has no register/stack deps (e.g., BoundedLoopCount), | ||
| // perform a conservative backward walk so the slice still shows the | ||
| // loop structure and control flow leading to the failure. | ||
| const bool conservative_mode = initial_relevance.registers.empty() && initial_relevance.stack_offsets.empty(); | ||
| size_t steps = 0; | ||
|
|
||
| size_t steps = 0; | ||
| // Hoist the parent lookup for the target label outside the hot loop; | ||
| // it is invariant and parents_of() may return a temporary. | ||
| const auto parents_of_target = prog.cfg().parents_of(label); | ||
|
|
||
| // Hoist the parent lookup for the failing label outside the hot loop; | ||
| // it is invariant and parents_of() may return a temporary. | ||
| const auto parents_of_fail = prog.cfg().parents_of(label); | ||
| while (!worklist.empty() && steps < max_steps) { | ||
| auto [current_label, relevant_after] = worklist.back(); | ||
| worklist.pop_back(); | ||
|
|
||
| while (!worklist.empty() && steps < max_steps) { | ||
| auto [current_label, relevant_after] = worklist.back(); | ||
| worklist.pop_back(); | ||
| // Skip if nothing is relevant — unless we're in conservative mode | ||
| // (empty-seed assertions like BoundedLoopCount) or this is the target label. | ||
| if (!conservative_mode && current_label != label && relevant_after.registers.empty() && | ||
| relevant_after.stack_offsets.empty()) { | ||
| continue; | ||
| } | ||
|
|
||
| // Skip if nothing is relevant — unless we're in conservative mode | ||
| // (empty-seed assertions like BoundedLoopCount) or this is the failing label. | ||
| if (!conservative_mode && current_label != label && relevant_after.registers.empty() && | ||
| relevant_after.stack_offsets.empty()) { | ||
| // Merge with existing relevance at this label (for deduplication) | ||
| auto& existing = visited[current_label]; | ||
| const size_t prev_size = existing.registers.size() + existing.stack_offsets.size(); | ||
| existing.registers.insert(relevant_after.registers.begin(), relevant_after.registers.end()); | ||
| existing.stack_offsets.insert(relevant_after.stack_offsets.begin(), relevant_after.stack_offsets.end()); | ||
| const size_t new_size = existing.registers.size() + existing.stack_offsets.size(); | ||
|
|
||
| // If no new relevance was added, skip (already processed with same or broader relevance). | ||
| // In conservative mode with empty relevance, use a separate visited set for dedup. | ||
| if (new_size == prev_size) { | ||
| if (prev_size > 0) { | ||
| continue; | ||
| } | ||
|
|
||
| // Merge with existing relevance at this label (for deduplication) | ||
| auto& existing = visited[current_label]; | ||
| const size_t prev_size = existing.registers.size() + existing.stack_offsets.size(); | ||
| existing.registers.insert(relevant_after.registers.begin(), relevant_after.registers.end()); | ||
| existing.stack_offsets.insert(relevant_after.stack_offsets.begin(), relevant_after.stack_offsets.end()); | ||
| const size_t new_size = existing.registers.size() + existing.stack_offsets.size(); | ||
|
|
||
| // If no new relevance was added, skip (already processed with same or broader relevance). | ||
| // In conservative mode with empty relevance, use a separate visited set for dedup. | ||
| if (new_size == prev_size) { | ||
| if (prev_size > 0) { | ||
| continue; | ||
| } | ||
| // Empty relevance (conservative mode): skip if we already visited this label | ||
| if (!conservative_visited.insert(current_label).second) { | ||
| continue; | ||
| } | ||
| // Empty relevance (conservative mode): skip if we already visited this label | ||
| if (!conservative_visited.insert(current_label).second) { | ||
| continue; | ||
| } | ||
| } | ||
|
|
||
| // Compute what's relevant BEFORE this instruction using deps | ||
| RelevantState relevant_before; | ||
| const auto inv_it = invariants.find(current_label); | ||
| if (inv_it != invariants.end() && inv_it->second.deps) { | ||
| const auto& deps = *inv_it->second.deps; | ||
| // Compute what's relevant BEFORE this instruction using deps | ||
| RelevantState relevant_before; | ||
| const auto inv_it = invariants.find(current_label); | ||
| if (inv_it != invariants.end() && inv_it->second.deps) { | ||
| const auto& deps = *inv_it->second.deps; | ||
|
|
||
| // Start with what's relevant after | ||
| relevant_before = relevant_after; | ||
| // Start with what's relevant after | ||
| relevant_before = relevant_after; | ||
|
|
||
| // Remove registers that are written by this instruction | ||
| // (they weren't relevant before their definition) | ||
| for (const auto& reg : deps.regs_written) { | ||
| relevant_before.registers.erase(reg); | ||
| } | ||
| // Remove registers that are written by this instruction | ||
| // (they weren't relevant before their definition) | ||
| for (const auto& reg : deps.regs_written) { | ||
| relevant_before.registers.erase(reg); | ||
| } | ||
|
|
||
| // Remove registers that are clobbered (killed without reading). | ||
| // These stop propagation for post-instruction uses but don't add read-deps. | ||
| for (const auto& reg : deps.regs_clobbered) { | ||
| relevant_before.registers.erase(reg); | ||
| } | ||
| // Remove registers that are clobbered (killed without reading). | ||
| // These stop propagation for post-instruction uses but don't add read-deps. | ||
| for (const auto& reg : deps.regs_clobbered) { | ||
| relevant_before.registers.erase(reg); | ||
| } | ||
|
|
||
| // Determine if this instruction contributes to the slice. | ||
| // An instruction contributes when it writes to a relevant register/stack slot, | ||
| // or when it is a control-flow decision (Jmp/Assume) that reads relevant registers. | ||
| bool instruction_contributes = false; | ||
| for (const auto& reg : deps.regs_written) { | ||
| if (relevant_after.registers.contains(reg)) { | ||
| instruction_contributes = true; | ||
| break; | ||
| } | ||
| // Determine if this instruction contributes to the slice. | ||
| // An instruction contributes when it writes to a relevant register/stack slot, | ||
| // or when it is a control-flow decision (Jmp/Assume) that reads relevant registers. | ||
| bool instruction_contributes = false; | ||
| for (const auto& reg : deps.regs_written) { | ||
| if (relevant_after.registers.contains(reg)) { | ||
| instruction_contributes = true; | ||
| break; | ||
| } | ||
| for (const auto& offset : deps.stack_written) { | ||
| if (relevant_after.stack_offsets.contains(offset)) { | ||
| instruction_contributes = true; | ||
| break; | ||
| } | ||
| } | ||
| for (const auto& offset : deps.stack_written) { | ||
| if (relevant_after.stack_offsets.contains(offset)) { | ||
| instruction_contributes = true; | ||
| break; | ||
| } | ||
| } | ||
|
|
||
| // Control-flow instructions (Jmp/Assume) that read relevant registers | ||
| // contribute to the slice because they shape the path to the failure. | ||
| if (!instruction_contributes) { | ||
| const auto& ins = prog.instruction_at(current_label); | ||
| if (std::holds_alternative<Jmp>(ins) || std::holds_alternative<Assume>(ins)) { | ||
| for (const auto& reg : deps.regs_read) { | ||
| if (relevant_after.registers.contains(reg)) { | ||
| instruction_contributes = true; | ||
| break; | ||
| } | ||
| // Control-flow instructions (Jmp/Assume) that read relevant registers | ||
| // contribute to the slice because they shape the path to the target. | ||
| if (!instruction_contributes) { | ||
| const auto& ins = prog.instruction_at(current_label); | ||
| if (std::holds_alternative<Jmp>(ins) || std::holds_alternative<Assume>(ins)) { | ||
| for (const auto& reg : deps.regs_read) { | ||
| if (relevant_after.registers.contains(reg)) { | ||
| instruction_contributes = true; | ||
| break; | ||
| } | ||
| } | ||
| } | ||
| } | ||
|
|
||
| // Immediate path guard: when the current label is a direct predecessor | ||
| // of the failing label and is an Assume instruction, its condition | ||
| // registers are causally relevant — they determine reachability. | ||
| if (std::holds_alternative<Assume>(prog.instruction_at(current_label))) { | ||
| if (std::find(parents_of_fail.begin(), parents_of_fail.end(), current_label) != | ||
| parents_of_fail.end()) { | ||
| instruction_contributes = true; | ||
| } | ||
| } | ||
|
|
||
| // At the failing label, the assertion depends on registers the instruction | ||
| // reads (e.g., base pointer r3 in a store). Since stores write to memory | ||
| // not registers, instruction_contributes would be false without this. | ||
| if (current_label == label) { | ||
| // Immediate path guard: when the current label is a direct predecessor | ||
| // of the target label and is an Assume instruction, its condition | ||
| // registers are causally relevant — they determine reachability. | ||
| if (std::holds_alternative<Assume>(prog.instruction_at(current_label))) { | ||
| if (std::find(parents_of_target.begin(), parents_of_target.end(), current_label) != | ||
| parents_of_target.end()) { | ||
| instruction_contributes = true; | ||
| } | ||
| } | ||
|
|
||
| // In conservative mode (empty seed, e.g., BoundedLoopCount), include all | ||
| // reachable labels so the slice shows the loop structure and control flow. | ||
| if (conservative_mode) { | ||
| instruction_contributes = true; | ||
| } | ||
| // At the target label, the assertion depends on registers the instruction | ||
| // reads (e.g., base pointer r3 in a store). Since stores write to memory | ||
| // not registers, instruction_contributes would be false without this. | ||
| if (current_label == label) { | ||
| instruction_contributes = true; | ||
| } | ||
|
|
||
| if (instruction_contributes) { | ||
| for (const auto& reg : deps.regs_read) { | ||
| relevant_before.registers.insert(reg); | ||
| } | ||
| for (const auto& offset : deps.stack_read) { | ||
| relevant_before.stack_offsets.insert(offset); | ||
| } | ||
| } | ||
| // In conservative mode (empty seed, e.g., BoundedLoopCount), include all | ||
| // reachable labels so the slice shows the loop structure and control flow. | ||
| if (conservative_mode) { | ||
| instruction_contributes = true; | ||
| } | ||
|
|
||
| // Remove stack locations that are written by this instruction, | ||
| // but preserve offsets that are also read (read-modify-write, e.g., Atomic). | ||
| // Done before storing to slice_labels for consistency with register handling | ||
| // (written registers are removed before storage at lines 476-478). | ||
| for (const auto& offset : deps.stack_written) { | ||
| if (!deps.stack_read.contains(offset)) { | ||
| relevant_before.stack_offsets.erase(offset); | ||
| } | ||
| if (instruction_contributes) { | ||
| for (const auto& reg : deps.regs_read) { | ||
| relevant_before.registers.insert(reg); | ||
| } | ||
| for (const auto& offset : deps.stack_read) { | ||
| relevant_before.stack_offsets.insert(offset); | ||
| } | ||
| } | ||
|
|
||
| if (instruction_contributes) { | ||
| // Only include contributing labels in the output slice. | ||
| // Store relevant_before so pre-invariant filtering shows the | ||
| // instruction's read-deps (the true upstream dependencies). | ||
| slice_labels[current_label] = relevant_before; | ||
| // Remove stack locations that are written by this instruction, | ||
| // but preserve offsets that are also read (read-modify-write, e.g., Atomic). | ||
| for (const auto& offset : deps.stack_written) { | ||
| if (!deps.stack_read.contains(offset)) { | ||
| relevant_before.stack_offsets.erase(offset); | ||
| } | ||
| } else { | ||
| // No deps available: conservatively treat this label as contributing | ||
| // and propagate all current relevance to predecessors. | ||
| relevant_before = relevant_after; | ||
| slice_labels[current_label] = relevant_before; | ||
| } | ||
|
|
||
| // Add predecessors to worklist | ||
| for (const auto& parent : prog.cfg().parents_of(current_label)) { | ||
| worklist.emplace_back(parent, relevant_before); | ||
| if (instruction_contributes) { | ||
| // Only include contributing labels in the output slice. | ||
| slice_labels[current_label] = relevant_before; | ||
| } | ||
| } else { | ||
| // No deps available: conservatively treat this label as contributing | ||
| // and propagate all current relevance to predecessors. | ||
| relevant_before = relevant_after; | ||
| slice_labels[current_label] = relevant_before; | ||
| } | ||
|
|
||
| ++steps; | ||
| // Add predecessors to worklist | ||
| for (const auto& parent : prog.cfg().parents_of(current_label)) { | ||
| worklist.emplace_back(parent, relevant_before); | ||
| } | ||
|
|
||
| // Expand join points: for any traversed label that is a join point | ||
| // (≥2 predecessors) where at least one predecessor is already in the slice, | ||
| // add the join-point label itself and all predecessors that have invariants. | ||
| // This ensures the causal trace shows converging paths that cause precision loss. | ||
| // Note: predecessors may not be in `visited` if the worklist budget was exhausted | ||
| // before reaching them, so we check the invariant map directly. | ||
| std::map<Label, RelevantState> join_expansion; | ||
| for (const auto& [v_label, v_relevance] : visited) { | ||
| const auto& parents = prog.cfg().parents_of(v_label); | ||
| if (parents.size() < 2) { | ||
| continue; | ||
| } | ||
| // Check that at least one predecessor is in the slice (this join is relevant) | ||
| bool has_slice_parent = false; | ||
| for (const auto& parent : parents) { | ||
| if (slice_labels.contains(parent)) { | ||
| has_slice_parent = true; | ||
| break; | ||
| } | ||
| ++steps; | ||
| } |
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Consider extracting helper functions to reduce cognitive complexity.
The function has a cognitive complexity of 42 (threshold 25 per static analysis). While the algorithm is correct and well-documented, consider extracting some logical blocks into helper functions for maintainability:
- Lines 445-546: The dependency analysis and contribution check block could become
compute_relevant_before() - Lines 556-594: Join point expansion could become
expand_join_points()
This is optional since the current structure with inline comments is readable.
🧰 Tools
🪛 Clang (14.0.6)
[warning] 380-380: use a trailing return type for this function
(modernize-use-trailing-return-type)
[warning] 380-380: method 'compute_slice_from_label' can be made static
(readability-convert-member-functions-to-static)
[warning] 380-380: function 'compute_slice_from_label' has cognitive complexity of 42 (threshold 25)
(readability-function-cognitive-complexity)
[note] 390-390: +1, including nesting penalty of 0, nesting level increased to 1
(clang)
[note] 407-407: +1
(clang)
[note] 415-415: +1, including nesting penalty of 0, nesting level increased to 1
(clang)
[note] 421-421: +2, including nesting penalty of 1, nesting level increased to 2
(clang)
[note] 435-435: +2, including nesting penalty of 1, nesting level increased to 2
(clang)
[note] 436-436: +3, including nesting penalty of 2, nesting level increased to 3
(clang)
[note] 440-440: +3, including nesting penalty of 2, nesting level increased to 3
(clang)
[note] 448-448: +2, including nesting penalty of 1, nesting level increased to 2
(clang)
[note] 485-485: +3, including nesting penalty of 2, nesting level increased to 3
(clang)
[note] 487-487: +4, including nesting penalty of 3, nesting level increased to 4
(clang)
[note] 500-500: +3, including nesting penalty of 2, nesting level increased to 3
(clang)
[note] 501-501: +4, including nesting penalty of 3, nesting level increased to 4
(clang)
[note] 510-510: +3, including nesting penalty of 2, nesting level increased to 3
(clang)
[note] 516-516: +3, including nesting penalty of 2, nesting level increased to 3
(clang)
[note] 520-520: +3, including nesting penalty of 2, nesting level increased to 3
(clang)
[note] 537-537: +3, including nesting penalty of 2, nesting level increased to 3
(clang)
[note] 541-541: +1, nesting level increased to 2
(clang)
[warning] 409-409: variable 'steps' is not initialized
(cppcoreguidelines-init-variables)
[warning] 428-428: variable 'prev_size' is not initialized
(cppcoreguidelines-init-variables)
[warning] 431-431: variable 'new_size' is not initialized
(cppcoreguidelines-init-variables)
🪛 Cppcheck (2.19.0)
[style] 434-434: The function 'fill_ones' is never used.
(unusedFunction)
[style] 400-400: The function 'abs' is never used.
(unusedFunction)
[style] 459-459: The function 'select_potentials' is never used.
(unusedFunction)
[style] 530-530: The function 'close_after_meet' is never used.
(unusedFunction)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/result.cpp` around lines 380 - 554, The compute_slice_from_label function
is overly complex—extract the dependency-analysis and contribution-determination
logic into a helper compute_relevant_before(const Program&, const Label&, const
RelevantState&, const InvariantDeps&, const std::vector<Label>&
parents_of_target, bool conservative_mode) that returns RelevantState and a bool
indicating instruction_contributes (use symbols deps, relevant_after,
relevant_before, instruction_contributes), and extract the predecessor/worklist
expansion logic into expand_join_points(const Program&, Label, const
RelevantState&, std::vector<std::pair<Label,RelevantState>>& worklist) to
encapsulate parents_of/current parent handling; replace the inlined blocks in
compute_slice_from_label with calls to these helpers to reduce cognitive
complexity while preserving behavior (keep uses of invariants, slice_labels,
visited, conservative_visited, and steps unchanged).
Comment on lines
+247
to
+365
| TEST_CASE("verify_assembly: labels and jumps", "[mcp][assembly]") { | ||
| McpTestHarness h; | ||
| auto result = h.call_tool("verify_assembly", { | ||
| {"code", | ||
| "r0 = 1\n" | ||
| "if r0 == 0 goto <skip>\n" | ||
| "r0 = 42\n" | ||
| "<skip>:\n" | ||
| "exit"}, | ||
| }); | ||
|
|
||
| REQUIRE(result["passed"] == true); | ||
| REQUIRE(result["instruction_count"] == 4); // Labels don't count as instructions. | ||
| } | ||
|
|
||
| TEST_CASE("verify_assembly: custom pre-invariant", "[mcp][assembly]") { | ||
| McpTestHarness h; | ||
| // Without custom pre, r3 is uninitialized. With it, we define r3 as a number. | ||
| auto result = h.call_tool("verify_assembly", { | ||
| {"code", "r0 = r3\nexit"}, | ||
| {"pre", json::array({"r3.type=number", "r3.svalue=99", "r3.uvalue=99"})}, | ||
| }); | ||
|
|
||
| REQUIRE(result["passed"] == true); | ||
| } | ||
|
|
||
| TEST_CASE("verify_assembly: observe at pc", "[mcp][assembly]") { | ||
| McpTestHarness h; | ||
| auto result = h.call_tool("verify_assembly", { | ||
| {"code", "r0 = 42\nexit"}, | ||
| {"observe", json::array({ | ||
| {{"pc", 1}, {"constraints", json::array({"r0.type=number"})}}, | ||
| })}, | ||
| }); | ||
|
|
||
| REQUIRE(result["passed"] == true); | ||
| REQUIRE(result["observations"].is_array()); | ||
| REQUIRE(result["observations"].size() == 1); | ||
| REQUIRE(result["observations"][0]["ok"] == true); | ||
| } | ||
|
|
||
| TEST_CASE("verify_assembly: observe at exit label", "[mcp][assembly]") { | ||
| McpTestHarness h; | ||
| auto result = h.call_tool("verify_assembly", { | ||
| {"code", "r0 = 0\nexit"}, | ||
| {"observe", json::array({ | ||
| {{"label", "exit"}, {"constraints", json::array({"r0.type=number"})}}, | ||
| })}, | ||
| }); | ||
|
|
||
| REQUIRE(result["observations"][0]["ok"] == true); | ||
| } | ||
|
|
||
| TEST_CASE("verify_assembly: program_type parameter", "[mcp][assembly]") { | ||
| McpTestHarness h; | ||
| for (const auto& type : {"xdp", "sk_skb", "socket_filter"}) { | ||
| DYNAMIC_SECTION("type: " << type) { | ||
| auto result = h.call_tool("verify_assembly", { | ||
| {"code", "r0 = 0\nexit"}, | ||
| {"program_type", type}, | ||
| }); | ||
| REQUIRE(result["passed"] == true); | ||
| } | ||
| } | ||
| } | ||
|
|
||
| TEST_CASE("verify_assembly: helper call resolution", "[mcp][assembly]") { | ||
| McpTestHarness h; | ||
| // Tests the call N regex interception and make_call(func, *platform) routing. | ||
| auto result = h.call_tool("verify_assembly", { | ||
| {"code", | ||
| "r2 = r10\n" | ||
| "r2 += -4\n" | ||
| "*(u32 *)(r10 - 4) = r0\n" | ||
| "r1 = 1\n" | ||
| "r3 = r2\n" | ||
| "r4 = 0\n" | ||
| "call 2\n" // bpf_map_update_elem | ||
| "r0 = 0\n" | ||
| "exit"}, | ||
| }); | ||
|
|
||
| REQUIRE(result.contains("passed")); | ||
| REQUIRE(result["instruction_count"] == 9); | ||
| } | ||
|
|
||
| TEST_CASE("verify_assembly: empty code is an error", "[mcp][assembly]") { | ||
| McpTestHarness h; | ||
| REQUIRE_THROWS(h.call_tool("verify_assembly", {{"code", ""}})); | ||
| } | ||
|
|
||
| TEST_CASE("verify_assembly: invalid instruction is an error", "[mcp][assembly]") { | ||
| McpTestHarness h; | ||
| REQUIRE_THROWS(h.call_tool("verify_assembly", {{"code", "not_a_valid_instruction"}})); | ||
| } | ||
|
|
||
| TEST_CASE("verify_assembly: verification options forwarding", "[mcp][assembly]") { | ||
| McpTestHarness h; | ||
|
|
||
| SECTION("allow_division_by_zero=true (default)") { | ||
| auto result = h.call_tool("verify_assembly", { | ||
| {"code", "r0 = 0\nr1 = 0\nr0 /= r1\nexit"}, | ||
| {"pre", json::array({"r0.type=number", "r0.svalue=10", "r0.uvalue=10", | ||
| "r1.type=number", "r1.svalue=0", "r1.uvalue=0"})}, | ||
| {"allow_division_by_zero", true}, | ||
| }); | ||
| REQUIRE(result["passed"] == true); | ||
| } | ||
|
|
||
| SECTION("allow_division_by_zero=false") { | ||
| auto result = h.call_tool("verify_assembly", { | ||
| {"code", "r0 = 0\nr1 = 0\nr0 /= r1\nexit"}, | ||
| {"pre", json::array({"r0.type=number", "r0.svalue=10", "r0.uvalue=10", | ||
| "r1.type=number", "r1.svalue=0", "r1.uvalue=0"})}, | ||
| {"allow_division_by_zero", false}, | ||
| }); | ||
| REQUIRE(result["passed"] == false); | ||
| } | ||
| } |
There was a problem hiding this comment.
🛠️ Refactor suggestion | 🟠 Major
Add deterministic regression cases for wide-instruction PCs and invalid observe.label.
Current assembly tests do not cover (1) multi-slot instruction PC mapping and (2) unsupported observation labels. Add one sound and one unsound deterministic case so these paths stay guarded.
As per coding guidelines: Add deterministic tests or YAML fixtures that demonstrate both the sound and the unsound outcomes when needing executable evidence of invariants.
🧰 Tools
🪛 Cppcheck (2.19.0)
[performance] 258-258: Function parameter 'premise_set' should be passed by const reference.
(passedByValue)
[performance] 259-259: Function parameter 'conclusion_set' should be passed by const reference.
(passedByValue)
[performance] 264-264: Function parameter 'conclusion_set' should be passed by const reference.
(passedByValue)
[style] 281-281: The function 'truncate_to' is never used.
(unusedFunction)
[style] 257-257: The function 'cast_to_sint' is never used.
(unusedFunction)
[style] 269-269: The function 'cast_to_uint' is never used.
(unusedFunction)
[style] 308-308: The function 'signed_int' is never used.
(unusedFunction)
[style] 318-318: The function 'unsigned_int' is never used.
(unusedFunction)
[style] 328-328: The function 'nonnegative' is never used.
(unusedFunction)
[style] 338-338: The function 'negative' is never used.
(unusedFunction)
[style] 348-348: The function 'unsigned_high' is never used.
(unusedFunction)
[style] 251-251: The function 'forget' is never used.
(unusedFunction)
[style] 333-333: The function 'update_edge' is never used.
(unusedFunction)
[style] 277-277: The function 'assume_eq_types' is never used.
(unusedFunction)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/test/test_mcp.cpp` around lines 247 - 365, Add two deterministic tests to
src/test/test_mcp.cpp using McpTestHarness::call_tool: (1) a sound regression
named like "verify_assembly: wide-instruction pc mapping" that supplies assembly
containing a multi-slot/wide instruction sequence and an observe entry using a
pc that hits the second slot; assert the result["passed"] == true and correct
instruction_count mapping so multi-slot PCs map to the expected instruction
index; (2) an unsound regression named like "verify_assembly: observe invalid
label" that calls verify_assembly with an observe entry using an
unsupported/invalid label string and assert the tool throws or returns failure
(REQUIRE_THROWS or REQUIRE(result["passed"] == false)) to ensure invalid
observe.label is rejected; use the same call pattern as other TEST_CASEs
(McpTestHarness h; h.call_tool(...)) and mirror existing assertion style to keep
tests deterministic.
There was a problem hiding this comment.
♻️ Duplicate comments (12)
src/mcp/README.md (3)
29-30:⚠️ Potential issue | 🟡 MinorDocument both supported framing modes.
The transport supports Content-Length framing and NDJSON, but this text states NDJSON only.
🔧 Suggested fix
-The server communicates via JSON-RPC 2.0 over stdio (newline-delimited JSON). +The server communicates via JSON-RPC 2.0 over stdio using either +Content-Length framing or newline-delimited JSON (NDJSON).🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/README.md` around lines 29 - 30, The README currently states the server communicates via NDJSON only; update the sentence to document both supported framing modes by mentioning that the server supports JSON-RPC 2.0 over stdio using either Content-Length framing or newline-delimited JSON (NDJSON), and note that clients (e.g., GitHub Copilot CLI, VS Code) may use either framing mode so implementations should handle both; edit the sentence describing transport in src/mcp/README.md accordingly.
64-76:⚠️ Potential issue | 🟡 MinorTool table is missing
verify_assembly.The PR adds 11 tools but only 10 are listed here.
🔧 Suggested fix
| `verify_program` | Run verification, get pass/fail with error summary and stats | +| `verify_assembly` | Verify BPF assembly text without needing a compiled ELF file | | `get_invariant` | Get pre/post abstract state at one or more instructions |🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/README.md` around lines 64 - 76, The tools table in README.md omits the new `verify_assembly` tool; add a table row for `verify_assembly` in the same list as `verify_program`/`get_instruction` etc., with a short description (e.g., "Verify assembly-level properties or equivalence for assembled BPF code, returning pass/fail with error summary and stats") so the README reflects all 11 tools and matches the PR changes.
34-36:⚠️ Potential issue | 🟡 MinorAdd language tag to fenced code block.
Triggers markdownlint MD040.
🔧 Suggested fix
-``` +```text /mcp add ```🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/README.md` around lines 34 - 36, Update the fenced code block that contains the command "/mcp add" to include a language tag (e.g., add "text" after the opening backticks) so the block becomes a labeled code fence and satisfies markdownlint MD040; locate the fenced block in README.md by searching for the exact text "/mcp add" and add the language identifier to the opening ``` line.src/prevail_mcp.cpp (1)
31-38:⚠️ Potential issue | 🟡 MinorResource leak:
mcp_fdnot closed iffdopenfails.If
fdopenreturns null, the duplicated file descriptor leaks.🔧 Proposed fix
`#ifndef` _WIN32 - int mcp_fd = dup(fileno(stdout)); + 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`🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/prevail_mcp.cpp` around lines 31 - 38, The dup'd file descriptor mcp_fd is leaked when fdopen(fileno(stdout)) returns nullptr; modify the block that creates mcp_fd and assigns mcp_out (referencing mcp_fd, mcp_out, fileno, fdopen) so that if fdopen fails you close(mcp_fd) before falling back to using stdout, and only assign mcp_out after handling the close; ensure you still handle the case where dup() itself fails (mcp_fd < 0) and keep the existing fallback to stdout.src/mcp/tools.cpp (4)
883-898:⚠️ Potential issue | 🟠 MajorUnknown observation labels silently coerce to entry.
Lines 892-898 only handle
"exit". Any other label string falls through withlabelremainingLabel::entry, checking constraints at the wrong location.🔧 Proposed fix
} else if (obs.contains("label")) { const std::string label_str = obs["label"].get<std::string>(); if (label_str == "exit") { label = prevail::Label::exit; + } else if (label_str == "entry") { + label = prevail::Label::entry; + } else { + throw std::runtime_error("Unsupported observe label: " + label_str); } obs_entry = {{"label", label_str}}; + } else { + throw std::runtime_error("observe entry must include either 'pc' or 'label'"); }🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 883 - 898, The code currently treats any non-"exit" label string as prevail::Label::entry, causing misplacement of constraints; update the obs handling in the block that checks obs.contains("label") to validate label_str explicitly: accept known names (e.g., "exit" -> prevail::Label::exit, "entry" -> prevail::Label::entry or any other supported variants) and otherwise throw a descriptive std::runtime_error (including label_str) so unknown labels fail fast; ensure you still set obs_entry = {{"label", label_str}} after validation and use the same prevail::Label variable to hold the validated value.
713-719:⚠️ Potential issue | 🟠 MajorVerify PC accounting for wide instructions.
Lines 715-718 advance
pcby instruction count, not BPF slot size. Wide instructions (e.g., 64-bit immediate loadslddw) occupy 2 slots, which would shift subsequent PCs and break jump target resolution.#!/bin/bash # Check if prevail::size() is available and how wide instructions are handled rg -n "prevail::size" --type cpp -C 3 # Check parse_instruction return type and if it exposes slot size ast-grep --pattern 'parse_instruction($$$)'🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 713 - 719, The PC is advanced by block.instructions.size(), which ignores multi-slot (wide) instructions like lddw; update the PC accounting to sum each instruction's slot width instead of counting instructions. In the loop that builds label_map (symbols: label_map, blocks, prevail::Label, block.instructions), replace the pc += static_cast<int>(block.instructions.size()) logic with iterating block.instructions and adding each instruction's slot count (use whatever API exists such as prevail::size(inst) or an instruction.slot_count()/width() accessor exposed by parse_instruction) so PCs reflect true BPF slots and jump targets resolve correctly.
570-570:⚠️ Potential issue | 🟠 MajorBound
trace_depthbefore slicing.Caller-controlled depth without range checks could cause pathological slice workloads.
🔧 Proposed fix
- const size_t trace_depth = args.value("trace_depth", 200); + const int trace_depth_raw = args.value("trace_depth", 200); + if (trace_depth_raw < 0 || trace_depth_raw > 10000) { + throw std::runtime_error("trace_depth must be in [0, 10000]"); + } + const size_t trace_depth = static_cast<size_t>(trace_depth_raw);🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` at line 570, The caller-controlled trace_depth must be clamped before any slice operations to prevent pathological workloads; change the initialization of trace_depth to enforce a safe range (e.g., define a constant kMaxTraceDepth and compute trace_depth = std::min(std::max<size_t>(args.value("trace_depth", 200), 0), kMaxTraceDepth) or equivalent), and use that bounded variable wherever trace_depth is used (reference symbol: trace_depth and the args.value("trace_depth", 200) call); ensure kMaxTraceDepth is documented and chosen conservatively.
758-759:⚠️ Potential issue | 🟠 MajorReject invalid map sizes in
verify_assembly.Non-positive values for
map_key_sizeormap_value_sizewould be cast to large unsigned values at lines 804-815.🔧 Proposed fix
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"); + }🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 758 - 759, In verify_assembly, validate that the parsed map_key_size and map_value_size (from args.value) are positive before they're used/cast; if either is <= 0, return an error or fail verification with a clear message (e.g., "invalid map_key_size" / "invalid map_value_size") so they cannot be cast to large unsigned values later in the function; update any callers or error handling as needed to propagate this failure.src/mcp/prevail_headers.hpp (1)
9-12: 🧹 Nitpick | 🔵 TrivialAdd clarifying comment for the empty guard.
The pattern of defining
BPF_CONFORMANCE_CORE_EBPF_INST_Hwithout including anything works but is non-obvious.📝 Suggested clarification
// Prevent bpf_conformance's ebpf_inst.h from conflicting with prevail::EbpfInst. +// Define the guard macro so that if ebpf_inst.h is included later, it becomes a no-op. `#ifndef` BPF_CONFORMANCE_CORE_EBPF_INST_H `#define` BPF_CONFORMANCE_CORE_EBPF_INST_H `#endif`🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/prevail_headers.hpp` around lines 9 - 12, The empty include guard for BPF_CONFORMANCE_CORE_EBPF_INST_H is intended to prevent bpf_conformance's ebpf_inst.h from conflicting with prevail::EbpfInst but lacks an explanatory note; update the file to add a brief clarifying comment above the guard mentioning that defining BPF_CONFORMANCE_CORE_EBPF_INST_H intentionally prevents inclusion of bpf_conformance's ebpf_inst.h to avoid symbol conflict with prevail::EbpfInst and reference that this is an intentional empty guard rather than an accidental no-op.src/mcp/analysis_engine.hpp (1)
110-112:⚠️ Potential issue | 🟡 MinorAlign
get_live_invariantcomment with actual fallback semantics.Line 111 says “empty StringInvariant,” but the implementation returns
prevail::StringInvariant::bottom()when no session/label exists.Proposed fix
- /// `@returns` empty StringInvariant if no session or label not found. + /// `@returns` prevail::StringInvariant::bottom() if no session exists or the label is missing.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/analysis_engine.hpp` around lines 110 - 112, The comment for get_live_invariant is inaccurate: update the documentation for prevail::StringInvariant get_live_invariant(const prevail::Label& label, prevail::InvariantPoint point) const to state that it returns prevail::StringInvariant::bottom() when there is no live session or the label isn’t found (and that it calls to_set() on demand), instead of saying it returns an “empty StringInvariant”; ensure the wording matches the implementation semantics (bottom() fallback) and mention the to_set() behavior.src/test/test_mcp.cpp (1)
247-365: 🛠️ Refactor suggestion | 🟠 MajorAdd deterministic regressions for wide-instruction PC mapping and invalid
observe.label.The
verify_assemblyblock at Line 247 onward still misses two guardrails:
- a sound case where an observe PC targets a second slot of a wide instruction, and
- an unsound case where an unsupported
observe.labelis rejected.As per coding guidelines:
Add deterministic tests or YAML fixtures that demonstrate both the sound and the unsound outcomes when needing executable evidence of invariants.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/test/test_mcp.cpp` around lines 247 - 365, Add two deterministic regression tests to the verify_assembly suite: one that exercises a wide (64-bit) instruction whose second-slot PC is targeted by an observe entry (create a snippet with a wide instruction like a 64-bit load/store so the tool must map PCs deterministically) and assert the tool either maps that PC to the instruction’s canonical slot or returns a clear error (use the existing h.call_tool("verify_assembly", {...}) pattern and assert result["observations"] or REQUIRE_THROWS accordingly); and a second test that submits an observe entry with an unsupported label (e.g., {"label": "nonexistent"}) and assert the call is rejected (use REQUIRE_THROWS or REQUIRE(result["passed"] == false) as appropriate). Place these new TEST_CASEs near the other verify_assembly tests (refer to McpTestHarness, h.call_tool, and the "observe" handling in existing tests) so they deterministically document the sound and unsound outcomes.src/mcp/analysis_engine.cpp (1)
219-221:⚠️ Potential issue | 🟠 MajorReject unknown
mode_strvalues instead of coercing toconsistent.At Line 219, any value other than
"entailed"is treated asconsistent, which silently alters semantics on typos/malformed input.Proposed fix
- auto mode = - (mode_str == "entailed") ? prevail::ObservationCheckMode::entailed : prevail::ObservationCheckMode::consistent; - return session_->live_result->check_observation_at_label(label, point, observation, mode); + 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);🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/analysis_engine.cpp` around lines 219 - 221, The code currently coerces any mode_str other than "entailed" into prevail::ObservationCheckMode::consistent which masks typos; update the handling of mode_str before calling session_->live_result->check_observation_at_label so that only "entailed" maps to prevail::ObservationCheckMode::entailed and only "consistent" maps to prevail::ObservationCheckMode::consistent, and for any other value return/propagate an error (or throw an exception / log and return an error result) instead of silently defaulting—modify the branch around mode_str and the call site (referencing mode_str, prevail::ObservationCheckMode, and session_->live_result->check_observation_at_label) to perform explicit validation and an early error return on unknown values.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In `@src/mcp/analysis_engine.cpp`:
- Around line 219-221: The code currently coerces any mode_str other than
"entailed" into prevail::ObservationCheckMode::consistent which masks typos;
update the handling of mode_str before calling
session_->live_result->check_observation_at_label so that only "entailed" maps
to prevail::ObservationCheckMode::entailed and only "consistent" maps to
prevail::ObservationCheckMode::consistent, and for any other value
return/propagate an error (or throw an exception / log and return an error
result) instead of silently defaulting—modify the branch around mode_str and the
call site (referencing mode_str, prevail::ObservationCheckMode, and
session_->live_result->check_observation_at_label) to perform explicit
validation and an early error return on unknown values.
In `@src/mcp/analysis_engine.hpp`:
- Around line 110-112: The comment for get_live_invariant is inaccurate: update
the documentation for prevail::StringInvariant get_live_invariant(const
prevail::Label& label, prevail::InvariantPoint point) const to state that it
returns prevail::StringInvariant::bottom() when there is no live session or the
label isn’t found (and that it calls to_set() on demand), instead of saying it
returns an “empty StringInvariant”; ensure the wording matches the
implementation semantics (bottom() fallback) and mention the to_set() behavior.
In `@src/mcp/prevail_headers.hpp`:
- Around line 9-12: The empty include guard for BPF_CONFORMANCE_CORE_EBPF_INST_H
is intended to prevent bpf_conformance's ebpf_inst.h from conflicting with
prevail::EbpfInst but lacks an explanatory note; update the file to add a brief
clarifying comment above the guard mentioning that defining
BPF_CONFORMANCE_CORE_EBPF_INST_H intentionally prevents inclusion of
bpf_conformance's ebpf_inst.h to avoid symbol conflict with prevail::EbpfInst
and reference that this is an intentional empty guard rather than an accidental
no-op.
In `@src/mcp/README.md`:
- Around line 29-30: The README currently states the server communicates via
NDJSON only; update the sentence to document both supported framing modes by
mentioning that the server supports JSON-RPC 2.0 over stdio using either
Content-Length framing or newline-delimited JSON (NDJSON), and note that clients
(e.g., GitHub Copilot CLI, VS Code) may use either framing mode so
implementations should handle both; edit the sentence describing transport in
src/mcp/README.md accordingly.
- Around line 64-76: The tools table in README.md omits the new
`verify_assembly` tool; add a table row for `verify_assembly` in the same list
as `verify_program`/`get_instruction` etc., with a short description (e.g.,
"Verify assembly-level properties or equivalence for assembled BPF code,
returning pass/fail with error summary and stats") so the README reflects all 11
tools and matches the PR changes.
- Around line 34-36: Update the fenced code block that contains the command
"/mcp add" to include a language tag (e.g., add "text" after the opening
backticks) so the block becomes a labeled code fence and satisfies markdownlint
MD040; locate the fenced block in README.md by searching for the exact text
"/mcp add" and add the language identifier to the opening ``` line.
In `@src/mcp/tools.cpp`:
- Around line 883-898: The code currently treats any non-"exit" label string as
prevail::Label::entry, causing misplacement of constraints; update the obs
handling in the block that checks obs.contains("label") to validate label_str
explicitly: accept known names (e.g., "exit" -> prevail::Label::exit, "entry" ->
prevail::Label::entry or any other supported variants) and otherwise throw a
descriptive std::runtime_error (including label_str) so unknown labels fail
fast; ensure you still set obs_entry = {{"label", label_str}} after validation
and use the same prevail::Label variable to hold the validated value.
- Around line 713-719: The PC is advanced by block.instructions.size(), which
ignores multi-slot (wide) instructions like lddw; update the PC accounting to
sum each instruction's slot width instead of counting instructions. In the loop
that builds label_map (symbols: label_map, blocks, prevail::Label,
block.instructions), replace the pc +=
static_cast<int>(block.instructions.size()) logic with iterating
block.instructions and adding each instruction's slot count (use whatever API
exists such as prevail::size(inst) or an instruction.slot_count()/width()
accessor exposed by parse_instruction) so PCs reflect true BPF slots and jump
targets resolve correctly.
- Line 570: The caller-controlled trace_depth must be clamped before any slice
operations to prevent pathological workloads; change the initialization of
trace_depth to enforce a safe range (e.g., define a constant kMaxTraceDepth and
compute trace_depth = std::min(std::max<size_t>(args.value("trace_depth", 200),
0), kMaxTraceDepth) or equivalent), and use that bounded variable wherever
trace_depth is used (reference symbol: trace_depth and the
args.value("trace_depth", 200) call); ensure kMaxTraceDepth is documented and
chosen conservatively.
- Around line 758-759: In verify_assembly, validate that the parsed map_key_size
and map_value_size (from args.value) are positive before they're used/cast; if
either is <= 0, return an error or fail verification with a clear message (e.g.,
"invalid map_key_size" / "invalid map_value_size") so they cannot be cast to
large unsigned values later in the function; update any callers or error
handling as needed to propagate this failure.
In `@src/prevail_mcp.cpp`:
- Around line 31-38: The dup'd file descriptor mcp_fd is leaked when
fdopen(fileno(stdout)) returns nullptr; modify the block that creates mcp_fd and
assigns mcp_out (referencing mcp_fd, mcp_out, fileno, fdopen) so that if fdopen
fails you close(mcp_fd) before falling back to using stdout, and only assign
mcp_out after handling the close; ensure you still handle the case where dup()
itself fails (mcp_fd < 0) and keep the existing fallback to stdout.
In `@src/test/test_mcp.cpp`:
- Around line 247-365: Add two deterministic regression tests to the
verify_assembly suite: one that exercises a wide (64-bit) instruction whose
second-slot PC is targeted by an observe entry (create a snippet with a wide
instruction like a 64-bit load/store so the tool must map PCs deterministically)
and assert the tool either maps that PC to the instruction’s canonical slot or
returns a clear error (use the existing h.call_tool("verify_assembly", {...})
pattern and assert result["observations"] or REQUIRE_THROWS accordingly); and a
second test that submits an observe entry with an unsupported label (e.g.,
{"label": "nonexistent"}) and assert the call is rejected (use REQUIRE_THROWS or
REQUIRE(result["passed"] == false) as appropriate). Place these new TEST_CASEs
near the other verify_assembly tests (refer to McpTestHarness, h.call_tool, and
the "observe" handling in existing tests) so they deterministically document the
sound and unsound outcomes.
ℹ️ Review info
Configuration used: Repository UI
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (22)
CMakeLists.txtREADME.mddocs/README.mddocs/llm-context.mdsrc/mcp/README.mdsrc/mcp/analysis_engine.cppsrc/mcp/analysis_engine.hppsrc/mcp/json_serializers.cppsrc/mcp/json_serializers.hppsrc/mcp/mcp_server.cppsrc/mcp/mcp_server.hppsrc/mcp/mcp_transport.cppsrc/mcp/mcp_transport.hppsrc/mcp/platform_ops.hppsrc/mcp/platform_ops_prevail.hppsrc/mcp/prevail_headers.hppsrc/mcp/tools.cppsrc/mcp/tools.hppsrc/prevail_mcp.cppsrc/result.cppsrc/result.hppsrc/test/test_mcp.cpp
There was a problem hiding this comment.
♻️ Duplicate comments (6)
src/mcp/tools.cpp (4)
570-571:⚠️ Potential issue | 🟠 MajorValidate and bound
trace_depthbefore slicing.Line 570 accepts caller-controlled depth without range checks and forwards it directly to expensive slicing paths.
Proposed fix
- const size_t trace_depth = args.value("trace_depth", 200); + const int trace_depth_arg = args.value("trace_depth", 200); + if (trace_depth_arg < 0 || trace_depth_arg > 10000) { + throw std::runtime_error("trace_depth must be in [0, 10000]"); + } + const size_t trace_depth = static_cast<size_t>(trace_depth_arg);🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 570 - 571, The code reads a caller-controlled trace_depth via args.value("trace_depth", 200) and passes it into expensive slicing paths; clamp and validate this value immediately after reading it to a safe range (e.g. ensure it's >=1 and <= a defined MAX_TRACE_DEPTH constant) by replacing uses of trace_depth with a bounded variable (e.g. bounded_trace_depth = std::min(std::max(trace_depth, (size_t)1), MAX_TRACE_DEPTH)); use bounded_trace_depth wherever slicing or heavy operations are invoked (search for usages of trace_depth in this file and in functions that perform slicing) and add a clear MAX_TRACE_DEPTH constant and optional log/warning if the caller-supplied value was adjusted.
713-719:⚠️ Potential issue | 🔴 Critical
parse_assemblyuses instruction index PCs instead of slot-accurate PCs.Line 718 and Line 743 advance by instruction count. Wide instructions occupy multiple BPF slots, so label targets and
observe.pcresolution can become incorrect.Also applies to: 725-744
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 713 - 719, The label-to-PC map currently advances pc using block.instructions.size(), which counts instructions not BPF slots; update parse_assembly to compute pc by summing each instruction's slot width (e.g., call the instruction's slot/width accessor on each element of block.instructions) when populating label_map and when advancing pc elsewhere (affecting the same loop range around label_map, pc, blocks, block.instructions and the subsequent pass that resolves observe.pc). Replace uses of static_cast<int>(block.instructions.size()) with the sum of per-instruction slot counts so label targets and observe.pc are slot-accurate.
758-760:⚠️ Potential issue | 🟠 MajorReject non-positive map sizes before descriptor construction.
Negative/zero map sizes are accepted at Line 758-759 and then cast to unsigned at Line 804-813.
Proposed fix
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"); + }Also applies to: 804-815
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 758 - 760, The code currently accepts non-positive values for map_key_size and map_value_size (variables map_key_size and map_value_size) and later casts them to unsigned when building the descriptor; add an explicit validation immediately after reading these args to reject values <= 0 (e.g., return an error/throw or log and exit) before any descriptor construction or unsigned casts occur (the check should be placed alongside the arg reads and will prevent the later casting paths around the descriptor construction code that uses these variables).
892-899:⚠️ Potential issue | 🟠 MajorDo not coerce unknown
observe.labelvalues to entry.Only
"exit"is handled, and every other label silently falls through toLabel::entry, checking the wrong program point.Proposed fix
} else if (obs.contains("label")) { const std::string label_str = obs["label"].get<std::string>(); if (label_str == "exit") { label = prevail::Label::exit; + } else if (label_str == "entry") { + label = prevail::Label::entry; + } else { + throw std::runtime_error("Unsupported observe label: " + label_str); } obs_entry = {{"label", label_str}}; + } else { + throw std::runtime_error("observe entry must include either 'pc' or 'label'"); }🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 892 - 899, The code in tools.cpp erroneously treats any unrecognized observe.label as Label::entry: when handling obs.contains("label") inside the observer parsing block, only "exit" is checked and everything else silently falls through; change this to validate the label_str explicitly—if label_str == "exit" set label = prevail::Label::exit and set obs_entry accordingly, else do not override label (do not set it to entry) and instead handle the unknown label by either logging/erroring or skipping the observation (e.g., return/continue or set an error flag). Update the obs.contains("label") branch (the label_str variable and the branch that assigns label and obs_entry) to only assign for recognized labels and to handle unknown values explicitly.src/test/test_mcp.cpp (2)
399-413:⚠️ Potential issue | 🟠 MajorThis test currently locks in unsupported-label fallback behavior.
It expects
"bogus"to proceed instead of being rejected. The assertion should enforce failure/throw for invalid labels.As per coding guidelines:
Add deterministic tests or YAML fixtures that demonstrate both the sound and the unsound outcomes when needing executable evidence of invariants.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/test/test_mcp.cpp` around lines 399 - 413, The test verify_assembly: observe with unsupported label currently accepts an invalid label ("bogus") and asserts a successful observation; change it to enforce that invalid labels cause failure by updating the TEST_CASE (and/or the McpTestHarness call to "verify_assembly") so the call_tool invocation with observe label "bogus" either throws or returns an error result; replace the current assertions about result["observations"] with an assertion that an exception is thrown or that result indicates failure (e.g., contains an "error" field or a non-zero status), ensuring the test no longer relies on fallback-to-Label::entry behavior.
300-314: 🛠️ Refactor suggestion | 🟠 MajorAdd a slot-accurate wide-instruction regression assertion.
This case only checks
pc=0; it does not verify behavior at PCs after a 2-slot instruction, where mapping bugs show up.As per coding guidelines:
Add deterministic tests or YAML fixtures that demonstrate both the sound and the unsound outcomes when needing executable evidence of invariants.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/test/test_mcp.cpp` around lines 300 - 314, The test only asserts the observation at pc=0; add a slot-accurate assertion for the PC after the 2-slot lddw to catch mapping regressions: update the TEST_CASE "verify_assembly: lddw wide instruction" (where McpTestHarness h calls verify_assembly with code "r0 = 42 ll\nexit") to include an observe entry for {"pc": 2, "constraints": ["r0.type=number"]} (or the expected constraints at that PC) and add REQUIRE checks that the corresponding observations element for pc==2 exists and has ["ok"]==true (and/or assert the correct instruction_count mapping). This ensures behavior is verified both at the start of the wide instruction and at the PC after it.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In `@src/mcp/tools.cpp`:
- Around line 570-571: The code reads a caller-controlled trace_depth via
args.value("trace_depth", 200) and passes it into expensive slicing paths; clamp
and validate this value immediately after reading it to a safe range (e.g.
ensure it's >=1 and <= a defined MAX_TRACE_DEPTH constant) by replacing uses of
trace_depth with a bounded variable (e.g. bounded_trace_depth =
std::min(std::max(trace_depth, (size_t)1), MAX_TRACE_DEPTH)); use
bounded_trace_depth wherever slicing or heavy operations are invoked (search for
usages of trace_depth in this file and in functions that perform slicing) and
add a clear MAX_TRACE_DEPTH constant and optional log/warning if the
caller-supplied value was adjusted.
- Around line 713-719: The label-to-PC map currently advances pc using
block.instructions.size(), which counts instructions not BPF slots; update
parse_assembly to compute pc by summing each instruction's slot width (e.g.,
call the instruction's slot/width accessor on each element of
block.instructions) when populating label_map and when advancing pc elsewhere
(affecting the same loop range around label_map, pc, blocks, block.instructions
and the subsequent pass that resolves observe.pc). Replace uses of
static_cast<int>(block.instructions.size()) with the sum of per-instruction slot
counts so label targets and observe.pc are slot-accurate.
- Around line 758-760: The code currently accepts non-positive values for
map_key_size and map_value_size (variables map_key_size and map_value_size) and
later casts them to unsigned when building the descriptor; add an explicit
validation immediately after reading these args to reject values <= 0 (e.g.,
return an error/throw or log and exit) before any descriptor construction or
unsigned casts occur (the check should be placed alongside the arg reads and
will prevent the later casting paths around the descriptor construction code
that uses these variables).
- Around line 892-899: The code in tools.cpp erroneously treats any unrecognized
observe.label as Label::entry: when handling obs.contains("label") inside the
observer parsing block, only "exit" is checked and everything else silently
falls through; change this to validate the label_str explicitly—if label_str ==
"exit" set label = prevail::Label::exit and set obs_entry accordingly, else do
not override label (do not set it to entry) and instead handle the unknown label
by either logging/erroring or skipping the observation (e.g., return/continue or
set an error flag). Update the obs.contains("label") branch (the label_str
variable and the branch that assigns label and obs_entry) to only assign for
recognized labels and to handle unknown values explicitly.
In `@src/test/test_mcp.cpp`:
- Around line 399-413: The test verify_assembly: observe with unsupported label
currently accepts an invalid label ("bogus") and asserts a successful
observation; change it to enforce that invalid labels cause failure by updating
the TEST_CASE (and/or the McpTestHarness call to "verify_assembly") so the
call_tool invocation with observe label "bogus" either throws or returns an
error result; replace the current assertions about result["observations"] with
an assertion that an exception is thrown or that result indicates failure (e.g.,
contains an "error" field or a non-zero status), ensuring the test no longer
relies on fallback-to-Label::entry behavior.
- Around line 300-314: The test only asserts the observation at pc=0; add a
slot-accurate assertion for the PC after the 2-slot lddw to catch mapping
regressions: update the TEST_CASE "verify_assembly: lddw wide instruction"
(where McpTestHarness h calls verify_assembly with code "r0 = 42 ll\nexit") to
include an observe entry for {"pc": 2, "constraints": ["r0.type=number"]} (or
the expected constraints at that PC) and add REQUIRE checks that the
corresponding observations element for pc==2 exists and has ["ok"]==true (and/or
assert the correct instruction_count mapping). This ensures behavior is verified
both at the start of the wide instruction and at the PC after it.
ℹ️ Review info
Configuration used: Repository UI
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (4)
src/mcp/analysis_engine.cppsrc/mcp/analysis_engine.hppsrc/mcp/tools.cppsrc/test/test_mcp.cpp
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (5)
src/mcp/tools.cpp (4)
713-719:⚠️ Potential issue | 🔴 CriticalUse slot-accurate PC accounting in
parse_assembly.Line 718 and Line 743 advance by instruction count, not BPF slot size. Wide instructions shift PCs and can corrupt label resolution, jump targets, and later PC-based queries.
Also applies to: 725-744
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 713 - 719, The label→PC build uses instruction counts (pc += block.instructions.size()) which is wrong for BPF wide instructions; update parse_assembly to advance pc by slot-accurate sizes by iterating each block.instructions and adding each instruction's slot count (e.g., use the instruction method that returns slot/width or compute slots = (instruction.size_in_bytes()/BPF_SLOT_BYTES) ) instead of the vector size; apply the same slot-accurate accumulation wherever pc is advanced (including the later loop around lines 725-744) so label_map, jump targets and PC queries use slot-accurate PCs.
885-899:⚠️ Potential issue | 🟠 MajorFail fast on invalid observation targets instead of defaulting to entry.
Lines 892-899 only map
"exit". Unknown labels, or missing bothpcandlabel, currently fall back toLabel::entry, which can silently check the wrong location.Suggested fix
if (obs.contains("pc")) { const int obs_pc = obs["pc"].get<int>(); 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<std::string>(); - if (label_str == "exit") { + if (label_str == "exit") { label = prevail::Label::exit; + } else if (label_str == "entry") { + label = prevail::Label::entry; + } else { + throw std::runtime_error("Unsupported observe label: " + label_str); } obs_entry = {{"label", label_str}}; + } else { + throw std::runtime_error("observe entry must include either 'pc' or 'label'"); }🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 885 - 899, The parsing code that builds a prevail::Label from JSON should fail fast for invalid or missing targets instead of defaulting to Label::entry: in the block handling obs (the logic using obs.contains("pc") and obs.contains("label")), add explicit error handling to throw a std::runtime_error when neither "pc" nor "label" is present, and when a "label" string is present but is not the recognized value (e.g., not "exit"); keep the existing behavior for a valid pc (obs_pc >= 0) and for "exit" mapping to prevail::Label::exit, but replace any implicit fallback to Label::entry with a clear exception that includes the offending input (use obs or label_str in the error message) so callers cannot silently use the wrong label.
758-759:⚠️ Potential issue | 🟠 MajorReject non-positive map sizes in
verify_assembly.Lines 758-759 accept signed values and Lines 804/812 cast them to unsigned. Negative inputs become huge map sizes.
Suggested fix
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"); + }Also applies to: 804-815
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 758 - 759, In verify_assembly, reject non-positive map sizes by validating the signed integers returned for map_key_size and map_value_size (from args.value) immediately after they are read: if either <= 0, log an error or return a failure before they are cast to unsigned (where they currently become huge values, e.g., the code paths around the casts at the later map construction in the verify_assembly function). Update the code that reads map_key_size and map_value_size to perform the check and handle the error (throw/return false/log) so only positive sizes are used for subsequent static_cast<size_t> conversions; apply the same validation pattern to any other size parameters handled in the 804-815 region.
570-571:⚠️ Potential issue | 🟠 MajorValidate and bound
trace_depthbefore converting tosize_t.Line 570 accepts caller input directly as
size_t. Negative values can wrap to huge positive depths and drive pathological slicing work at Lines 645 and 653.Suggested fix
- const size_t trace_depth = args.value("trace_depth", 200); + const int trace_depth_arg = args.value("trace_depth", 200); + if (trace_depth_arg < 0 || trace_depth_arg > 10000) { + throw std::runtime_error("trace_depth must be in [0, 10000]"); + } + const size_t trace_depth = static_cast<size_t>(trace_depth_arg);Also applies to: 645-653
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/tools.cpp` around lines 570 - 571, The code reads trace_depth directly via args.value("trace_depth", 200) into a size_t which lets negative inputs wrap to huge values; change to read into a signed integer (e.g., int or long), validate it is >= 0, clamp it to a safe upper bound (introduce/use a constant like MAX_TRACE_DEPTH), then convert to size_t and assign to trace_depth; update all uses of trace_depth (the slicing logic referenced around where trace_depth is consumed) to rely on this validated/clamped value and ensure opt_termination handling remains unchanged.src/mcp/mcp_transport.hpp (1)
52-56:⚠️ Potential issue | 🟡 MinorCorrect the
runcontract comment to match actual loop behavior.Line 55 states the loop exits when the handler throws. The transport behavior is to translate handler failures to JSON-RPC errors and continue processing.
Suggested fix
- /// The loop exits on EOF or when the handler throws. + /// The loop exits on EOF/read error. + /// Handler exceptions are translated to JSON-RPC errors for requests with "id".🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@src/mcp/mcp_transport.hpp` around lines 52 - 56, Update the comment on the run loop to reflect actual behavior: instead of saying "The loop exits on EOF or when the handler throws", state that the loop only exits on EOF or transport-level/fatal errors; handler exceptions are caught, translated into JSON-RPC error responses, and processing continues. Reference the Handler type alias and the run loop behavior in mcp_transport.hpp so readers know exceptions from Handler (std::function<nlohmann::json(const std::string& method, const nlohmann::json& params)>) are handled and not used to terminate the loop.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@src/mcp/mcp_server.hpp`:
- Line 7: The public header mcp_server.hpp currently `#includes` mcp_transport.hpp
even though the header does not use any transport symbols; remove the
unnecessary include from mcp_server.hpp to reduce compile-time coupling, and
move the `#include` "mcp_transport.hpp" into the corresponding implementation file
(e.g., mcp_server.cpp) where transport types are actually used; if any inline or
templated functions in mcp_server.hpp later need transport types, replace the
include with a forward declaration or reintroduce the include only in those
specific cases.
In `@src/mcp/tools.cpp`:
- Around line 590-605: The code selects an error by error_index using
args.value("error_index", 0) and sets target_label/is_error_query by iterating
session.invariants, but later always returns slices.front() (and computes a
single failure_slice) which can mismatch the chosen error when error_index > 0;
modify the slice selection logic in the same scope that assembles slices (the
code that produces failure_slice and returns slices.front()) so it picks the
failure slice that corresponds to the same error_index/target_label (e.g., track
the idx used when scanning session.invariants and use that index into slices, or
match slices to invariant labels and pick the slice whose label == target_label)
so the returned failure_slice/returned element aligns with the originally
selected error (refer to symbols: args.value("error_index", 0),
session.invariants, target_label, is_error_query, slices, slices.front(),
failure_slice).
---
Duplicate comments:
In `@src/mcp/mcp_transport.hpp`:
- Around line 52-56: Update the comment on the run loop to reflect actual
behavior: instead of saying "The loop exits on EOF or when the handler throws",
state that the loop only exits on EOF or transport-level/fatal errors; handler
exceptions are caught, translated into JSON-RPC error responses, and processing
continues. Reference the Handler type alias and the run loop behavior in
mcp_transport.hpp so readers know exceptions from Handler
(std::function<nlohmann::json(const std::string& method, const nlohmann::json&
params)>) are handled and not used to terminate the loop.
In `@src/mcp/tools.cpp`:
- Around line 713-719: The label→PC build uses instruction counts (pc +=
block.instructions.size()) which is wrong for BPF wide instructions; update
parse_assembly to advance pc by slot-accurate sizes by iterating each
block.instructions and adding each instruction's slot count (e.g., use the
instruction method that returns slot/width or compute slots =
(instruction.size_in_bytes()/BPF_SLOT_BYTES) ) instead of the vector size; apply
the same slot-accurate accumulation wherever pc is advanced (including the later
loop around lines 725-744) so label_map, jump targets and PC queries use
slot-accurate PCs.
- Around line 885-899: The parsing code that builds a prevail::Label from JSON
should fail fast for invalid or missing targets instead of defaulting to
Label::entry: in the block handling obs (the logic using obs.contains("pc") and
obs.contains("label")), add explicit error handling to throw a
std::runtime_error when neither "pc" nor "label" is present, and when a "label"
string is present but is not the recognized value (e.g., not "exit"); keep the
existing behavior for a valid pc (obs_pc >= 0) and for "exit" mapping to
prevail::Label::exit, but replace any implicit fallback to Label::entry with a
clear exception that includes the offending input (use obs or label_str in the
error message) so callers cannot silently use the wrong label.
- Around line 758-759: In verify_assembly, reject non-positive map sizes by
validating the signed integers returned for map_key_size and map_value_size
(from args.value) immediately after they are read: if either <= 0, log an error
or return a failure before they are cast to unsigned (where they currently
become huge values, e.g., the code paths around the casts at the later map
construction in the verify_assembly function). Update the code that reads
map_key_size and map_value_size to perform the check and handle the error
(throw/return false/log) so only positive sizes are used for subsequent
static_cast<size_t> conversions; apply the same validation pattern to any other
size parameters handled in the 804-815 region.
- Around line 570-571: The code reads trace_depth directly via
args.value("trace_depth", 200) into a size_t which lets negative inputs wrap to
huge values; change to read into a signed integer (e.g., int or long), validate
it is >= 0, clamp it to a safe upper bound (introduce/use a constant like
MAX_TRACE_DEPTH), then convert to size_t and assign to trace_depth; update all
uses of trace_depth (the slicing logic referenced around where trace_depth is
consumed) to rely on this validated/clamped value and ensure opt_termination
handling remains unchanged.
ℹ️ Review info
Configuration used: Repository UI
Review profile: ASSERTIVE
Plan: Pro
📒 Files selected for processing (4)
src/mcp/json_serializers.hppsrc/mcp/mcp_server.hppsrc/mcp/mcp_transport.hppsrc/mcp/tools.cpp
|
|
||
| /// @file MCP server: tool registry, capability negotiation, and request dispatch. | ||
|
|
||
| #include "mcp_transport.hpp" |
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Remove unused transport dependency from the public server header.
Line 7 includes mcp_transport.hpp, but this header does not use transport symbols. Keeping it increases compile-time coupling.
Suggested fix
-#include "mcp_transport.hpp"
-
`#include` <functional>
`#include` <map>📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| #include "mcp_transport.hpp" | |
| `#include` <functional> | |
| `#include` <map> |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/mcp/mcp_server.hpp` at line 7, The public header mcp_server.hpp currently
`#includes` mcp_transport.hpp even though the header does not use any transport
symbols; remove the unnecessary include from mcp_server.hpp to reduce
compile-time coupling, and move the `#include` "mcp_transport.hpp" into the
corresponding implementation file (e.g., mcp_server.cpp) where transport types
are actually used; if any inline or templated functions in mcp_server.hpp later
need transport types, replace the include with a forward declaration or
reintroduce the include only in those specific cases.
Comment on lines
+590
to
+605
| 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; | ||
| is_error_query = true; | ||
| break; | ||
| } | ||
| idx++; | ||
| } |
There was a problem hiding this comment.
error_index selection and returned failure_slice can disagree.
Lines 590-605 pick the requested error label, but Lines 645-648 always compute one slice and return slices.front(). For error_index > 0, the error metadata and slice can point to different failures.
Suggested fix
- prevail::Label target_label = prevail::Label::entry;
+ prevail::Label target_label = prevail::Label::entry;
+ int requested_error_index = 0;
bool is_error_query = false;
@@
- const int error_index = args.value("error_index", 0);
+ requested_error_index = args.value("error_index", 0);
int idx = 0;
bool found_error = false;
@@
- if (idx == error_index) {
+ if (idx == requested_error_index) {
@@
- throw std::runtime_error("Error index " + std::to_string(error_index) + " not found");
+ throw std::runtime_error("Error index " + std::to_string(requested_error_index) + " not found");
}
@@
if (is_error_query && session.failed) {
- auto slices =
- engine.compute_failure_slices(elf_path, section, program, type, session.program, 1, trace_depth);
- if (!slices.empty()) {
- j["failure_slice"] = serialize_slice(slices.front(), session, target_label);
+ const int slice_count = requested_error_index + 1;
+ auto slices = engine.compute_failure_slices(
+ elf_path, section, program, type, session.program, slice_count, trace_depth);
+ if (requested_error_index >= 0 &&
+ static_cast<size_t>(requested_error_index) < slices.size()) {
+ j["failure_slice"] =
+ serialize_slice(slices[static_cast<size_t>(requested_error_index)], session, target_label);
return j;
}
}Also applies to: 643-648
🧰 Tools
🪛 Clang (14.0.6)
[warning] 590-590: variable 'error_index' is not initialized
(cppcoreguidelines-init-variables)
🪛 Cppcheck (2.19.0)
[style] 591-591: The function 'close_after_assign' is never used.
(unusedFunction)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/mcp/tools.cpp` around lines 590 - 605, The code selects an error by
error_index using args.value("error_index", 0) and sets
target_label/is_error_query by iterating session.invariants, but later always
returns slices.front() (and computes a single failure_slice) which can mismatch
the chosen error when error_index > 0; modify the slice selection logic in the
same scope that assembles slices (the code that produces failure_slice and
returns slices.front()) so it picks the failure slice that corresponds to the
same error_index/target_label (e.g., track the idx used when scanning
session.invariants and use that index into slices, or match slices to invariant
labels and pick the slice whose label == target_label) so the returned
failure_slice/returned element aligns with the originally selected error (refer
to symbols: args.value("error_index", 0), session.invariants, target_label,
is_error_query, slices, slices.front(), failure_slice).
Collaborator
|
Thanks for the PR! The MCP server is a feature I was actually about to implement - having structured access to invariants and slicing is valuable beyond just LLM agents. A few things to address: Split the PR.This PR bundles three separable changes:
Move the analysis engine into the core library
Smaller items
Happy to discuss the split boundaries if it's not clear where to draw the lines. |
Contributor
Author
Thanks for the feedback. I'll refactor/split this PR by sometime early next week. |
Refactor backward slicing to expose a general-purpose compute_slice_from_label() method on AnalysisResult that accepts an arbitrary label and seed relevance. The existing compute_failure_slices() now delegates to it, iterating error labels and extracting initial relevance from assertions. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Signed-off-by: Michael Agun <danielagun@microsoft.com>
Contributor
Author
|
Hey @elazarg -- I did an initial split of this PR into 3, and I agree with your general split. I have found it very useful (and to improve context efficiency for verification analysis/debugging) to give agents access to the mcp server, so looking forward to completing this work and getting it merged (I've been using it locally, just got busy the last few weeks so haven't updated).
|
Merge per-label relevance instead of overwriting when a label is revisited from a different successor, preserving registers and stack offsets from earlier visits. Only fall back to aggregating all assertion registers when the failing assertion was not identified. When it was found but has no register deps, leave the seed empty so compute_slice_from_label enters conservative mode. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Signed-off-by: Michael Agun <danielagun@microsoft.com>
Move the analysis engine (session management, caching, re-analysis on
file change) and platform abstraction into the core library so both
prevail CLI and MCP frontends can share it.
Changes from the original src/mcp/ versions:
- Replace prevail_headers.hpp with direct includes
- Add [[nodiscard]] to PlatformOps virtual methods
- Fix option overrides persisting across calls (init from defaults)
- Remove no-op catch (...) { throw; } in analyze()
- Fix stale 'check.exe' reference in PrevailPlatformOps (now 'prevail')
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Signed-off-by: Michael Agun <danielagun@microsoft.com>
Replace the 3 optional<bool> parameters on analyze() with a pointer to ebpf_verifier_options_t, giving callers full control over verbosity, conformance groups, and all other verifier settings. When null, platform defaults are used. Remove the VerificationOptions struct (subset of ebpf_verifier_options_t that is no longer needed). Store the full options in AnalysisSession so callers can inspect them. Stop hardcoding verbosity flags in analyze() — each frontend (CLI, MCP) sets its own verbosity before calling the engine. Accept ebpf_platform_t by value in PrevailPlatformOps so callers can configure conformance groups before constructing the ops object. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Signed-off-by: Michael Agun <danielagun@microsoft.com>
JSON-RPC 2.0 server over stdio providing tools for verification, invariant inspection, constraint checking, backward slicing, and assembly verification. Uses the AnalysisEngine from the core library. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Signed-off-by: Michael Agun <danielagun@microsoft.com>
Update tools.cpp to use the new analyze(options*) signature via a build_options() helper that constructs ebpf_verifier_options_t from JSON args with MCP-appropriate verbosity flags. Replace engine.options() with engine.session_options() in verify_assembly for seeding local options from the current session. Update test_mcp.cpp to pass ebpf_verifier_options_t to analyze() and use session_options() instead of the removed options() getter. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Signed-off-by: Michael Agun <danielagun@microsoft.com>
This was referenced Apr 15, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
JSON-RPC 2.0 server over stdio that exposes PREVAIL verification results as MCP tools. Uses the AnalysisEngine from the core library.
Transport: Auto-detects Content-Length framing (VS Code) or NDJSON (GitHub Copilot CLI).
Tools:
Build: Gated behind prevail_ENABLE_MCP (OFF by default). Fetches nlohmann_json v3.12.0 via FetchContent when enabled.
Tests: 74 test cases (521 assertions) covering transport framing, protocol semantics, JSON serialization, all tools, engine session behavior, and error cases.
Depends on #1061 (compute_slice_from_label) and #1062 (AnalysisEngine).
Files:
Summary by CodeRabbit
New Features
Documentation
Tests