vbpf / ebpf-verifier

eBPF verifier based on abstract interpretation
MIT License
375 stars 39 forks source link

Print failures in wto for easier debugging #633

Closed Alan-Jowett closed 3 months ago

Alan-Jowett commented 4 months ago

Resolves: #632

Why In a recent investigation, there was a single failed assertion, which expanded into over 500 failed assertions further down the graph. Unfortunately, the failure occurred approximately 60% of the way through the section and the code was aggressively in-lined and folded by LLVM.

The result was that of the 500 assertions, the one that represented the root cause is located approximately 60% of the way through the report that is generated, with the remaining assertions being downstream failures.

When the failures are instead printed in WTO, the failure ended up as the 3rd failed assertion in the list (with the first two warning about unreachable code), which was immediately actionable.

 What Add option to print verification failures in weak topographical order (WTO) instead of linear order (as they appear in the ELF file).

Result This tends to bring actionable failures closer to the start of the list of errors.

coveralls commented 4 months ago

Coverage Status

coverage: 90.052% (-0.3%) from 90.348% when pulling 843a7651f263c97100adfd7f259587e5b43344d9 on Alan-Jowett:print_in_weak_topological_order into 64ab8c034eb2fa563bbf4c6d181a482259b9f8eb on vbpf:main.

Alan-Jowett commented 3 months ago

The "assume-assertion" option gives the required result without requiring changes to the verifier, so I am closing out this PR.