Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Provide API for caller to query BPF register value range and type for call and callx instructions #680

Open
Alan-Jowett opened this issue Sep 12, 2024 · 4 comments

Comments

@Alan-Jowett
Copy link
Contributor

I want to permit bpf2c to use more information from the verifier. What is the best way to have verifier expose this?

  1. Maintain the CFG and invariants in thread local and provide query APIs.
  2. Serialize the CFG + invariants in verifier and deserialize in bpf2c.

This would help for two cases:

  1. Support for callx (if we can determine what the actual call target is, then we can emit a regular call).
  2. Support for faster versions of the map helper functions.
    a) Replace generic map helper functions with type specific ones (i.e. bfp_map_lookup_elem with bpf_hash_map_lookup_elem as an example)
    b) Inline array operations by providing the base address of the BPF_MAP_TYPE_ARRAY.
@agurfinkel
Copy link
Contributor

I do not understand the context. Perhaps someone else has a better opinion. Both cases require a clear language to represent invariants. Having a well defined serialization format would be useful. I do not know whether there is a suitable format already exist. In verification space, we would use SMT-LIB, but I cannot tell if this is appropriate here.

@Alan-Jowett
Copy link
Contributor Author

Here is a hopefully more succinct use case:
When performing code generation for a BPF program, it would be useful to know the range of values a BPF register might contain at a specific point in the code.

This can be used to perform a variety of optimizations, including improving callx instruction support as well as emitting optimal helper function calls for interacting with BPF maps.

Whether it is serialized or access is provided to the data via API's isn't critical to our use case.

@agurfinkel
Copy link
Contributor

In this case, it is easier to design an interface for the specific use case. Register ranges is a very commonly used information and has an easy format to communicate. The only issue is how to name registers consistently since they get re-used throughout execution.

This is much easier than getting an invariant out and then trying to extract intervals from it.

@Alan-Jowett Alan-Jowett changed the title Expose pre-invariants to callers of ebpf_verify_program Provide API for caller to query BPF register value range and type for call and callx instructions Sep 12, 2024
@Alan-Jowett
Copy link
Contributor Author

Updated the title to be constrain this to minimal needed for my scenario.

Use case:
When emitting the machine code for a call or callx instruction, provide an API that can be used to obtain the value ranges and types for registers.

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

No branches or pull requests

2 participants