Skip to content

Parse value expressions printed on separate lines#70

Merged
theihor merged 2 commits intomasterfrom
state-exprs-msg
Sep 4, 2025
Merged

Parse value expressions printed on separate lines#70
theihor merged 2 commits intomasterfrom
state-exprs-msg

Conversation

@theihor
Copy link
Copy Markdown
Collaborator

@theihor theihor commented Aug 29, 2025

Verifier in some cases may print information about known values
separately from the relevant instruciton, for example:

100: (85) call bpf_ringbuf_reserve#131
101: frame1: R0=ringbuf_mem_or_null(id=5,ref_obj_id=5,sz=196) refs=5
101: (bf) r7 = r0                     ; frame1: R0=ringbuf_mem_or_null(id=5,ref_obj_id=5,sz=196) R7_w=ringbuf_mem_or_null(id=5,ref_obj_id=5,sz=196) refs=5

Note that second line contains state produced by instrcution at 100.

Implement parsing these messages and incorporating the information
from them in the computed array of BpfState objects.

@theihor theihor marked this pull request as ready for review September 3, 2025 19:37
@theihor theihor requested a review from jordalgo September 3, 2025 19:37
@theihor theihor changed the title State exprs msg Parse value expressions printed on separate lines Sep 3, 2025
// the exprs to the state of the _previous_ instruction
const prevIdx = siblingInsLine(lines, idx, -1);
const prevLine = <InstructionLine>lines[prevIdx];
if (prevIdx < idx) {
Copy link
Copy Markdown
Collaborator

@jordalgo jordalgo Sep 4, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this check necessary?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems like it'll only trigger for idx=0.

src/analyzer.ts Outdated
ins.writes = ["r0", ...BPF_SCRATCH_REGS];
}

function updateBpfStateExprs(
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

naming nit - maybe updatePrevInsBpfState

Verifier in some cases may print information about known values
separately from the relevant instruciton, for example:

    100: (85) call bpf_ringbuf_reserve#131
    101: frame1: R0=ringbuf_mem_or_null(id=5,ref_obj_id=5,sz=196) refs=5
    101: (bf) r7 = r0                     ; frame1: R0=ringbuf_mem_or_null(id=5,ref_obj_id=5,sz=196) R7_w=ringbuf_mem_or_null(id=5,ref_obj_id=5,sz=196) refs=5

Note that second line contains state produced by instrcution at 100.

Implement parsing these messages and incorporating the information
from them in the computed array of BpfState objects.
@theihor theihor merged commit 8636c48 into master Sep 4, 2025
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants