README.ebpf

The eBPF backend for CompCert was done by <frederic.besson@inria.fr>
and <vincent.lafeychine@proton.me>.  This backend is based on the
existing RISC-V backend, and should be used to handle 32-bit eBPF
embedded systems (rBPF).

CompCert generates an eBPF text assembly file that is assembled by llvm-mc -triple bpf.
The generated ELF file contains relocations for functions calls and global variables.
As a result, an additional (static/dynamic) linking phase is necessary to get an executable BPF code.

Caveat: the traditional way of specifying BPF helper calls in C is not compatible with CompCert.
Helper calls need to be external functions (not global function pointers assigned to fixed integers).


Other limitations or specificites:
 - There is no linking step (this is the right way for eBPF)
 - Some additional symbols are added in extraction.v (need more investigation)
 - Jump tables are not supported (there is a command-line option to disable jump-table,
   this is should be a configuration option.)
 - Builtin and some arithmetic operations are not supported e.g mulhs, mulhu, mod, mull
 - Instruction selection could be optimised further
 - The backend targets 32 bits eBPF instruction (there is no 64 bits target)
 - There is no support for floating point numbers (could support soft-float)