verifier: Invalid access to map value

[osinstom]

While loading test.c program (with refactored packet size's check) I'm getting the following debug message:

2020-02-03T09:39:58.645Z|24443|verifier|INFO|PC=176, class=0x5, opcode=0x5
2020-02-03T09:39:58.645Z|24444|verifier|INFO|   unconditional jump from PC 176 to PC 212
2020-02-03T09:39:58.645Z|24445|verifier|INFO|PC=212, class=0x3, opcode=0x7b
2020-02-03T09:39:58.645Z|24446|verifier|INFO|   Spilled R8 to stack offset 888
2020-02-03T09:39:58.645Z|24447|verifier|INFO|PC=213, class=0x1, opcode=0x79
2020-02-03T09:39:58.645Z|24448|verifier|INFO|   Loaded R8 from stack offset 872
2020-02-03T09:39:58.645Z|24449|verifier|INFO|PC=214, class=0x7, opcode=0x7
2020-02-03T09:39:58.645Z|24450|verifier|INFO|   R8 (t=4) has updated range [304;304] U [304;304]
2020-02-03T09:39:58.645Z|24451|verifier|INFO|PC=215, class=0x7, opcode=0xb7
2020-02-03T09:39:58.645Z|24452|verifier|INFO|   R1 now has type 0x4, range [38;38] U [38;38]
2020-02-03T09:39:58.645Z|24453|verifier|INFO|PC=216, class=0x7, opcode=0xbf
2020-02-03T09:39:58.645Z|24454|verifier|INFO|   R9 now has type 0x4, range [0;0] U [0;0]
2020-02-03T09:39:58.645Z|24455|verifier|INFO|PC=217, class=0x5, opcode=0x55
2020-02-03T09:39:58.645Z|24456|verifier|INFO|   R3 (t=4) may have updated range [0;0] U [0;0]
2020-02-03T09:39:58.645Z|24457|verifier|INFO|PC=218, class=0x7, opcode=0xb7
2020-02-03T09:39:58.645Z|24458|verifier|INFO|   R1 now has type 0x4, range [34;34] U [34;34]
2020-02-03T09:39:58.645Z|24459|verifier|INFO|PC=219, class=0x0, opcode=0x18
2020-02-03T09:39:58.645Z|24460|bpf|WARN|Failed to load code: invalid access to map value (0 + 8 > 4) at PC 219

test.c

/* Automatically generated by p4c-ubpf from ../examples/tunneling.p4 on Fri Jan 31 15:04:18 2020
 */
#include "test.h"
#include <stdint.h>
#include <stdbool.h>
#include <stddef.h>
#include "ubpf_common.h"

#define BPF_MASK(t, w) ((((t)(1)) << (w)) - (t)1)
#define BYTES(w) ((w) / 8)

void* memcpy(void* dest, const void* src, size_t num);

static void *(*ubpf_map_lookup)(const void *, const void *) = (void *)1;
static int (*ubpf_map_update)(void *, const void *, void *) = (void *)2;
static int (*ubpf_map_delete)(void *, const void *) = (void *)3;
static int (*ubpf_map_add)(void *, const void *) = (void *)4;
static uint64_t (*ubpf_time_get_ns)() = (void *)5;
static uint32_t (*ubpf_hash)(const void *, uint64_t) = (void *)6;
static void (*ubpf_printf)(const char *fmt, ...) = (void *)7;
static void *(*ubpf_packet_data)(const void *) = (void *)9;
static void *(*ubpf_adjust_head)(const void *, uint64_t) = (void *)8;

#define write_partial(a, w, s, v) do { *((uint8_t*)a) = ((*((uint8_t*)a)) & ~(BPF_MASK(uint8_t, w) << s)) | (v << s) ; } while (0)
#define write_byte(base, offset, v) do { *(uint8_t*)((base) + (offset)) = (v); } while (0)

static uint32_t
bpf_htonl(uint32_t val) {
    return htonl(val);
}
static uint16_t
bpf_htons(uint16_t val) {
    return htons(val);
}
static uint64_t
bpf_htonll(uint64_t val) {
    return htonll(val);
}

uint64_t entry(void *ctx, uint64_t pkt_len){
    void *pkt = ubpf_packet_data(ctx);
    struct Headers_t headers = {
        .ethernet = {
            .ebpf_valid = 0
        },
        .mpls = {
            .ebpf_valid = 0
        },
        .ipv4 = {
            .ebpf_valid = 0
        },
    };
    struct metadata meta = {
    };
    int packetOffsetInBits = 0;
    uint8_t pass = 1;
    unsigned char ebpf_byte;

    goto start;
    start: {
        /* extract(headers.ethernet)*/
        if (pkt_len < BYTES(packetOffsetInBits + 112)) {
            goto reject;
        }

        headers.ethernet.dstAddr = (uint64_t)((load_dword(pkt, BYTES(packetOffsetInBits)) >> 16) & BPF_MASK(uint64_t, 48));
        packetOffsetInBits += 48;

        headers.ethernet.srcAddr = (uint64_t)((load_dword(pkt, BYTES(packetOffsetInBits)) >> 16) & BPF_MASK(uint64_t, 48));
        packetOffsetInBits += 48;

        headers.ethernet.etherType = (uint16_t)((load_half(pkt, BYTES(packetOffsetInBits))));
        packetOffsetInBits += 16;

        headers.ethernet.ebpf_valid = 1;
        switch (headers.ethernet.etherType) {
            case 0x800: goto ipv4;
            case 0x8847: goto mpls;
            default: goto reject;
        }
    }
    mpls: {
        /* extract(headers.mpls)*/
        if (pkt_len < BYTES(packetOffsetInBits + 32)) {
            goto reject;
        }

        headers.mpls.label = (uint32_t)((load_word(pkt, BYTES(packetOffsetInBits)) >> 12) & BPF_MASK(uint32_t, 20));
        packetOffsetInBits += 20;

        headers.mpls.tc = (uint8_t)((load_byte(pkt, BYTES(packetOffsetInBits)) >> 1) & BPF_MASK(uint8_t, 3));
        packetOffsetInBits += 3;

        headers.mpls.stack = (uint8_t)((load_byte(pkt, BYTES(packetOffsetInBits))) & BPF_MASK(uint8_t, 1));
        packetOffsetInBits += 1;

        headers.mpls.ttl = (uint8_t)((load_byte(pkt, BYTES(packetOffsetInBits))));
        packetOffsetInBits += 8;

        headers.mpls.ebpf_valid = 1;
        goto ipv4;
    }
    ipv4: {
        /* extract(headers.ipv4)*/
        if (pkt_len < BYTES(packetOffsetInBits + 160)) {
            goto reject;
        }

        headers.ipv4.version = (uint8_t)((load_byte(pkt, BYTES(packetOffsetInBits)) >> 4) & BPF_MASK(uint8_t, 4));
        packetOffsetInBits += 4;

        headers.ipv4.ihl = (uint8_t)((load_byte(pkt, BYTES(packetOffsetInBits))) & BPF_MASK(uint8_t, 4));
        packetOffsetInBits += 4;

        headers.ipv4.diffserv = (uint8_t)((load_byte(pkt, BYTES(packetOffsetInBits))));
        packetOffsetInBits += 8;

        headers.ipv4.totalLen = (uint16_t)((load_half(pkt, BYTES(packetOffsetInBits))));
        packetOffsetInBits += 16;

        headers.ipv4.identification = (uint16_t)((load_half(pkt, BYTES(packetOffsetInBits))));
        packetOffsetInBits += 16;

        headers.ipv4.flags = (uint8_t)((load_byte(pkt, BYTES(packetOffsetInBits)) >> 5) & BPF_MASK(uint8_t, 3));
        packetOffsetInBits += 3;

        headers.ipv4.fragOffset = (uint16_t)((load_half(pkt, BYTES(packetOffsetInBits))) & BPF_MASK(uint16_t, 13));
        packetOffsetInBits += 13;

        headers.ipv4.ttl = (uint8_t)((load_byte(pkt, BYTES(packetOffsetInBits))));
        packetOffsetInBits += 8;

        headers.ipv4.protocol = (uint8_t)((load_byte(pkt, BYTES(packetOffsetInBits))));
        packetOffsetInBits += 8;

        headers.ipv4.hdrChecksum = (uint16_t)((load_half(pkt, BYTES(packetOffsetInBits))));
        packetOffsetInBits += 16;

        headers.ipv4.srcAddr = (uint32_t)((load_word(pkt, BYTES(packetOffsetInBits))));
        packetOffsetInBits += 32;

        headers.ipv4.dstAddr = (uint32_t)((load_word(pkt, BYTES(packetOffsetInBits))));
        packetOffsetInBits += 32;

        headers.ipv4.ebpf_valid = 1;
        goto accept;
    }

    reject: { return 0; }

    accept:
    {
        {

            if (headers.mpls.ebpf_valid) {
                {
                    /* construct key */
                    struct pipe_upstream_tbl_key key = {};
                    key.headers_mpls_label = headers.mpls.label;
                    /* value */
                    struct pipe_upstream_tbl_value *value = NULL;
                    /* perform lookup */
                    value = ubpf_map_lookup(&pipe_upstream_tbl, &key);

                    if (value != NULL) {
                        /* run action */
                        switch (value->action) {
                            case pipe_mpls_decap: 
                            {
                                                                headers.mpls.ebpf_valid = false;
headers.ethernet.etherType = 0x800;
                            }
                            break;
                            case pipe_upstream_tbl_NoAction: 
                            {

                            }
                            break;
                            default: return 0;
                        }
                    }
                    else return 0;
                }
;
            } else {
                {
                    /* construct key */
                    struct pipe_downstream_tbl_key key = {};
                    key.headers_ipv4_dstAddr = headers.ipv4.dstAddr;
                    /* value */
                    struct pipe_downstream_tbl_value *value = NULL;
                    /* perform lookup */
                    value = ubpf_map_lookup(&pipe_downstream_tbl, &key);

                    if (value != NULL) {
                        /* run action */
                        switch (value->action) {
                            case pipe_mpls_encap: 
                            {
                                                                headers.mpls.ebpf_valid = true;
headers.ethernet.etherType = 0x8847;headers.mpls.label = 20;headers.mpls.tc = 5;headers.mpls.stack = 1;headers.mpls.ttl = 64;
                            }
                            break;
                            case pipe_downstream_tbl_NoAction: 
                            {

                            }
                            break;
                            default: return 0;
                        }
                    }
                    else return 0;
                }
;
            }

        }    }
    deparser:
    {
        int outHeaderLength = 0;
        if (headers.ethernet.ebpf_valid) 
        outHeaderLength += 112;
if (headers.mpls.ebpf_valid) 
        outHeaderLength += 32;
if (headers.ipv4.ebpf_valid) 
        outHeaderLength += 160;

        int outHeaderOffset = BYTES(packetOffsetInBits) - BYTES(outHeaderLength);
        pkt = ubpf_adjust_head(ctx, outHeaderOffset);
        pkt_len += outHeaderOffset;
        packetOffsetInBits = 0;
        if (headers.ethernet.ebpf_valid) {
            if (pkt_len < BYTES(packetOffsetInBits + 112)) {
                goto reject;
            }

            headers.ethernet.dstAddr = htonll(headers.ethernet.dstAddr << 16);
            ebpf_byte = ((char*)(&headers.ethernet.dstAddr))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.dstAddr))[1];
            write_byte(pkt, BYTES(packetOffsetInBits) + 1, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.dstAddr))[2];
            write_byte(pkt, BYTES(packetOffsetInBits) + 2, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.dstAddr))[3];
            write_byte(pkt, BYTES(packetOffsetInBits) + 3, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.dstAddr))[4];
            write_byte(pkt, BYTES(packetOffsetInBits) + 4, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.dstAddr))[5];
            write_byte(pkt, BYTES(packetOffsetInBits) + 5, (ebpf_byte));
            packetOffsetInBits += 48;

            headers.ethernet.srcAddr = htonll(headers.ethernet.srcAddr << 16);
            ebpf_byte = ((char*)(&headers.ethernet.srcAddr))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.srcAddr))[1];
            write_byte(pkt, BYTES(packetOffsetInBits) + 1, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.srcAddr))[2];
            write_byte(pkt, BYTES(packetOffsetInBits) + 2, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.srcAddr))[3];
            write_byte(pkt, BYTES(packetOffsetInBits) + 3, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.srcAddr))[4];
            write_byte(pkt, BYTES(packetOffsetInBits) + 4, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.srcAddr))[5];
            write_byte(pkt, BYTES(packetOffsetInBits) + 5, (ebpf_byte));
            packetOffsetInBits += 48;

            headers.ethernet.etherType = bpf_htons(headers.ethernet.etherType);
            ebpf_byte = ((char*)(&headers.ethernet.etherType))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ethernet.etherType))[1];
            write_byte(pkt, BYTES(packetOffsetInBits) + 1, (ebpf_byte));
            packetOffsetInBits += 16;

        }
;        if (headers.mpls.ebpf_valid) {
            if (pkt_len < BYTES(packetOffsetInBits + 32)) {
                goto reject;
            }

            headers.mpls.label = htonl(headers.mpls.label << 12);
            ebpf_byte = ((char*)(&headers.mpls.label))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.mpls.label))[1];
            write_byte(pkt, BYTES(packetOffsetInBits) + 1, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.mpls.label))[2];
            write_partial(pkt + BYTES(packetOffsetInBits) + 2, 4, 4, (ebpf_byte >> 4));
            packetOffsetInBits += 20;

            ebpf_byte = ((char*)(&headers.mpls.tc))[0];
            write_partial(pkt + BYTES(packetOffsetInBits) + 0, 3, 1, (ebpf_byte >> 0));
            packetOffsetInBits += 3;

            ebpf_byte = ((char*)(&headers.mpls.stack))[0];
            write_partial(pkt + BYTES(packetOffsetInBits) + 0, 1, 0, (ebpf_byte >> 0));
            packetOffsetInBits += 1;

            ebpf_byte = ((char*)(&headers.mpls.ttl))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            packetOffsetInBits += 8;

        }
;        if (headers.ipv4.ebpf_valid) {
            if (pkt_len < BYTES(packetOffsetInBits + 160)) {
                goto reject;
            }

            ebpf_byte = ((char*)(&headers.ipv4.version))[0];
            write_partial(pkt + BYTES(packetOffsetInBits) + 0, 4, 4, (ebpf_byte >> 0));
            packetOffsetInBits += 4;

            ebpf_byte = ((char*)(&headers.ipv4.ihl))[0];
            write_partial(pkt + BYTES(packetOffsetInBits) + 0, 4, 0, (ebpf_byte >> 0));
            packetOffsetInBits += 4;

            ebpf_byte = ((char*)(&headers.ipv4.diffserv))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            packetOffsetInBits += 8;

            headers.ipv4.totalLen = bpf_htons(headers.ipv4.totalLen);
            ebpf_byte = ((char*)(&headers.ipv4.totalLen))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ipv4.totalLen))[1];
            write_byte(pkt, BYTES(packetOffsetInBits) + 1, (ebpf_byte));
            packetOffsetInBits += 16;

            headers.ipv4.identification = bpf_htons(headers.ipv4.identification);
            ebpf_byte = ((char*)(&headers.ipv4.identification))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ipv4.identification))[1];
            write_byte(pkt, BYTES(packetOffsetInBits) + 1, (ebpf_byte));
            packetOffsetInBits += 16;

            ebpf_byte = ((char*)(&headers.ipv4.flags))[0];
            write_partial(pkt + BYTES(packetOffsetInBits) + 0, 3, 5, (ebpf_byte >> 0));
            packetOffsetInBits += 3;

            headers.ipv4.fragOffset = bpf_htons(headers.ipv4.fragOffset << 3);
            ebpf_byte = ((char*)(&headers.ipv4.fragOffset))[0];
            write_partial(pkt + BYTES(packetOffsetInBits) + 0, 5, 0, (ebpf_byte >> 3));
            write_partial(pkt + BYTES(packetOffsetInBits) + 0 + 1, 3, 5, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ipv4.fragOffset))[1];
            write_partial(pkt + BYTES(packetOffsetInBits) + 1, 5, 0, (ebpf_byte >> 3));
            packetOffsetInBits += 13;

            ebpf_byte = ((char*)(&headers.ipv4.ttl))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            packetOffsetInBits += 8;

            ebpf_byte = ((char*)(&headers.ipv4.protocol))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            packetOffsetInBits += 8;

            headers.ipv4.hdrChecksum = bpf_htons(headers.ipv4.hdrChecksum);
            ebpf_byte = ((char*)(&headers.ipv4.hdrChecksum))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ipv4.hdrChecksum))[1];
            write_byte(pkt, BYTES(packetOffsetInBits) + 1, (ebpf_byte));
            packetOffsetInBits += 16;

            headers.ipv4.srcAddr = htonl(headers.ipv4.srcAddr);
            ebpf_byte = ((char*)(&headers.ipv4.srcAddr))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ipv4.srcAddr))[1];
            write_byte(pkt, BYTES(packetOffsetInBits) + 1, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ipv4.srcAddr))[2];
            write_byte(pkt, BYTES(packetOffsetInBits) + 2, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ipv4.srcAddr))[3];
            write_byte(pkt, BYTES(packetOffsetInBits) + 3, (ebpf_byte));
            packetOffsetInBits += 32;

            headers.ipv4.dstAddr = htonl(headers.ipv4.dstAddr);
            ebpf_byte = ((char*)(&headers.ipv4.dstAddr))[0];
            write_byte(pkt, BYTES(packetOffsetInBits) + 0, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ipv4.dstAddr))[1];
            write_byte(pkt, BYTES(packetOffsetInBits) + 1, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ipv4.dstAddr))[2];
            write_byte(pkt, BYTES(packetOffsetInBits) + 2, (ebpf_byte));
            ebpf_byte = ((char*)(&headers.ipv4.dstAddr))[3];
            write_byte(pkt, BYTES(packetOffsetInBits) + 3, (ebpf_byte));
            packetOffsetInBits += 32;

        }
;    }
    if (pass)
        return 1;
    else
        return 0;
}

test.h

/* Automatically generated by p4c-ubpf from ../examples/tunneling.p4 on Fri Jan 31 15:04:18 2020
 */
#ifndef _P4_GEN_HEADER_
#define _P4_GEN_HEADER_
#include <stdint.h>
#include <stdbool.h>
#include <stddef.h>
#include "ubpf_common.h"

struct Ethernet_h {
    uint64_t dstAddr; /* EthernetAddress */
    uint64_t srcAddr; /* EthernetAddress */
    uint16_t etherType; /* bit<16> */
    uint8_t ebpf_valid;
};

struct IPv4_h {
    uint8_t version; /* bit<4> */
    uint8_t ihl; /* bit<4> */
    uint8_t diffserv; /* bit<8> */
    uint16_t totalLen; /* bit<16> */
    uint16_t identification; /* bit<16> */
    uint8_t flags; /* bit<3> */
    uint16_t fragOffset; /* bit<13> */
    uint8_t ttl; /* bit<8> */
    uint8_t protocol; /* bit<8> */
    uint16_t hdrChecksum; /* bit<16> */
    uint32_t srcAddr; /* IPv4Address */
    uint32_t dstAddr; /* IPv4Address */
    uint8_t ebpf_valid;
};

struct mpls_h {
    uint32_t label; /* bit<20> */
    uint8_t tc; /* bit<3> */
    uint8_t stack; /* bit<1> */
    uint8_t ttl; /* bit<8> */
    uint8_t ebpf_valid;
};

struct Headers_t {
    struct Ethernet_h ethernet; /* Ethernet_h */
    struct mpls_h mpls; /* mpls_h */
    struct IPv4_h ipv4; /* IPv4_h */
};

struct metadata {
};

enum ubpf_map_type {
    UBPF_MAP_TYPE_HASHMAP = 4,
};
struct ubpf_map_def {
    enum ubpf_map_type type;
    unsigned int key_size;
    unsigned int value_size;
    unsigned int max_entries;
    unsigned int nb_hash_functions;
};

struct pipe_downstream_tbl_key {
    uint32_t headers_ipv4_dstAddr; /* headers.ipv4.dstAddr */
};
enum downstream_tbl_0_actions {
    pipe_mpls_encap,
    pipe_downstream_tbl_NoAction,
};
struct pipe_downstream_tbl_value {
    enum downstream_tbl_0_actions action;
    union {
        struct {
        } pipe_mpls_encap;
        struct {
        } pipe_downstream_tbl_NoAction;
    } u;
};
struct pipe_upstream_tbl_key {
    uint32_t headers_mpls_label; /* headers.mpls.label */
};
enum upstream_tbl_0_actions {
    pipe_mpls_decap,
    pipe_upstream_tbl_NoAction,
};
struct pipe_upstream_tbl_value {
    enum upstream_tbl_0_actions action;
    union {
        struct {
        } pipe_mpls_decap;
        struct {
        } pipe_upstream_tbl_NoAction;
    } u;
};

struct ubpf_map_def pipe_downstream_tbl = {
    .type = UBPF_MAP_TYPE_HASHMAP,
    .key_size = sizeof(struct pipe_downstream_tbl_key),
    .value_size = sizeof(struct pipe_downstream_tbl_value),
    .max_entries = 65535,
    .nb_hash_functions = 0,
};
struct ubpf_map_def pipe_upstream_tbl = {
    .type = UBPF_MAP_TYPE_HASHMAP,
    .key_size = sizeof(struct pipe_upstream_tbl_key),
    .value_size = sizeof(struct pipe_upstream_tbl_value),
    .max_entries = 65535,
    .nb_hash_functions = 0,
};
#endif

\cc @pchaigno