Skip to content

Prevail does not support function calls #451

@H0mTanks

Description

@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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions