Prevail does not support function calls

[H0mTanks]

Hello, I'm writing a packet parser xdp program which only has an xdp section. The program passes verification and loads successfully with the verifier in the linux kernel, I'm trying to get it verified with PREVAIL as well, since windows is a possible target.

While trying to run it through the verifier with: sudo ./ebpf-verifier/check myxdp.o xdp The verifier returns an error: error: Can't find any maps sections in file myxdp.o

The program was compiled with the command: clang -O2 -g -Wall -target bpf -c myxdp.c -o myxdp.o

llvm-objdump output shows the section headers as follows:

linux@linux-pc:~/dev$ llvm-objdump --section-headers myxdp.o

myxdp.o:	file format elf64-bpf

Sections:
Idx Name                   Size     VMA              Type
  0                        00000000 0000000000000000 
  1 .strtab                000002c0 0000000000000000 
  2 .text                  00000f60 0000000000000000 TEXT
  3 .rel.text              00000040 0000000000000000 
  4 xdp                    000008c0 0000000000000000 TEXT
  5 .relxdp                00000010 0000000000000000 
  6 .rodata.str1.1         000000b0 0000000000000000 DATA
  7 license                00000004 0000000000000000 DATA
  8 .debug_loclists        00000662 0000000000000000 DEBUG
  9 .debug_abbrev          000002bd 0000000000000000 DEBUG
 10 .debug_info            00000bda 0000000000000000 DEBUG
 11 .rel.debug_info        00000060 0000000000000000 
 12 .debug_rnglists        000001ea 0000000000000000 DEBUG
 13 .debug_str_offsets     00000294 0000000000000000 DEBUG
 14 .rel.debug_str_offsets 00000a30 0000000000000000 
 15 .debug_str             00000668 0000000000000000 DEBUG
 16 .debug_addr            00000130 0000000000000000 DEBUG
 17 .rel.debug_addr        00000250 0000000000000000 
 18 .BTF                   00001668 0000000000000000 
 19 .rel.BTF               00000010 0000000000000000 
 20 .BTF.ext               000015f0 0000000000000000 
 21 .rel.BTF.ext           000015f0 0000000000000000 
 22 .debug_frame           000000e8 0000000000000000 DEBUG
 23 .rel.debug_frame       00000120 0000000000000000 
 24 .debug_line            000007ef 0000000000000000 DEBUG
 25 .rel.debug_line        00000150 0000000000000000 
 26 .debug_line_str        000000cf 0000000000000000 DEBUG
 27 .llvm_addrsig          00000002 0000000000000000 
 28 .symtab                000005d0 0000000000000000

A marginally simpler program verifies fine with the tool. The examples provided in the repo work as well, so I can confirm the tool is set up correctly.

Any help would be appreciated, Thank you.

[dthaler]

Can you provide either the .o file or the disassembly? Specifically, does the disassembly contain anything that PREVAIL thinks is a reference to a map?

[H0mTanks]

I don't believe there are any references to a map. The program is simple, has no map structs and the only bpf helper used is bpf_printk.

The following files are of an isomorphic program built on windows with the windows-ebpf headers. I don't have the equivalent linux program which I opened the issue with, at the moment. The problem is the same and reproducible with both the windows headers and the linux headers.

Here is the failing object file: myxdp.o (EDIT: fixed link)

Source code of marginally simpler program that passes: myxdp.c Here if both lines 50-57 and 71-75 are uncommented, the program fails the verifier. However, if ONLY ONE of them (either one) is uncommented, the program passes the verifier successfully. The lines in question are simple if statements comparing packet fields to constants.

Here is the llvm-objdump of the failing object file: myxdp.o objdump

[H0mTanks]

Another example of the same error is when I try to use __builtin_memcpy.

In the below eBPF program, I'm trying to set the destination ipv6 address to loopback.

uint32_t loopback_addr[4] = { 0x00, 0x00, 0x00, 0x01000000 };

int32_t redirect_v6(bpf_sock_addr_t* ctx)
{
    int32_t verdict = BPF_SOCK_ADDR_VERDICT_PROCEED;

    __builtin_memcpy(ctx->user_ip6, loopback_addr, sizeof(ctx->user_ip6));

	// Doing the copy manually works
    // ctx->user_ip6[0] = loopback_addr[0];
    // ctx->user_ip6[1] = loopback_addr[1];
    // ctx->user_ip6[2] = loopback_addr[2];
    // ctx->user_ip6[3] = loopback_addr[3];

    ctx->user_port = 0x901F; //port 8080

    return verdict;
}

SEC("cgroup/connect6")
int32_t connect_redirect6(bpf_sock_addr_t* ctx)
{
    return redirect_v6(ctx);
}

Running this through the verifier also gets me: error: Can't find any maps sections in file myxdp.o

Note that the parsing program in the previous comment did not use __builtin_memcpy. Same error.

[elazarg]

I believe this is due to .rel.debug_info, .rel.BTF etc., that PREVAIL does not understand.

[H0mTanks]

Anything I can do as a user?

[elazarg]

Can you upload the object file again? By the time I got to look at it, it was no longer available.

[H0mTanks]

@elazarg Ah it got deleted, that's strange. Anyway here it is: myxdp_fail.o

[elazarg]

Okay, I was wrong. Turning the excetion into a simple error message gives another error:

error: Unresolved external symbol parse_ethernet_packet at location 12

[H0mTanks]

So does parse_ethernet_packet packet symbol get stripped out for some reason when the offending code is uncommented? That would be strange for clang to do. Does the second program which breaks with builtin_memcpy have a similar issue?

You can find the code of the object file I'm trying to compile and run along with instructions to make it fail the verifier in the third comment of this issue in myxdp.c.

[elazarg]

I think the issue is that we do not support function calls, so all the calls must be inlined.

[dthaler]

@elazarg can the title of this issue be renamed to "Prevail does not support function calls" perhaps?

[elazarg]

@dthaler sure. For some reason I was under the impression we already have an issue for that.