18658728485

Committed 18 Oct 2025 05:56PM UTC coverage: 88.47% (+0.4%) from 88.11%

Build # 18658728485

Build Type

push

github

Committed by

elazarg

Commit Message

Bump external/bpf_conformance from `8f3c2fe` to `6fa6a20`

Bumps [external/bpf_conformance](https://github.com/Alan-Jowett/bpf_conformance) from `8f3c2fe` to `6fa6a20`.
- [Release notes](https://github.com/Alan-Jowett/bpf_conformance/releases)
- [Commits](https://github.com/Alan-Jowett/bpf_conformance/compare/8f3c2fe88...<a class=hub.com/Alan-Jowett/ebpf-verifier/commit/6fa6a20ac6fd3612ea9338312a67408687b9f06b">6fa6a20ac)

---
updated-dependencies:
- dependency-name: external/bpf_conformance
  dependency-version: 6fa6a20ac6fd3612ea9338312a67408687b9f06b
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>

Run Details

8954 of 10121 relevant lines covered (88.47%)

18293099.16 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

80.39

/src/asm_parse.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#include <map>
#include <regex>
#include <sstream>
#include <string>

#include "arith/dsl_syntax.hpp"
#include "arith/linear_constraint.hpp"
#include "asm_parse.hpp"
#include "asm_unmarshal.hpp"
#include "crab/type_encoding.hpp"
#include "crab/var_registry.hpp"
#include "platform.hpp"
#include "string_constraints.hpp"

using std::regex;
using std::regex_match;

namespace prevail {
#define REG R"_(\s*(r\d\d?)\s*)_"
#define WREG R"_(\s*([wr]\d\d?)\s*)_"
#define IMM R"_(\s*\[?([-+]?(?:0x)?[0-9a-f]+)\]?\s*)_"
#define REG_OR_IMM R"_(\s*([+-]?(?:0x)?[0-9a-f]+|r\d\d?)\s*)_"

#define FUNC IMM
#define OPASSIGN R"_(\s*(\S*)=\s*)_"
#define ASSIGN R"_(\s*=\s*)_"
#define LONGLONG R"_(\s*(ll|)\s*)_"
#define UNOP R"_((-|be16|be32|be64|le16|le32|le64|swap16|swap32|swap64))_"
#define ATOMICOP R"_((\+|\||&|\^|x|cx)=)_"

#define PLUSMINUS R"_((\s*[+-])\s*)_"
#define LPAREN R"_(\s*\(\s*)_"
#define RPAREN R"_(\s*\)\s*)_"

#define PAREN(x) LPAREN x RPAREN
#define STAR R"_(\s*\*\s*)_"
#define DEREF STAR PAREN("u(\\d+)" STAR)

#define IN R"_(\s*in\s*)_"
#define TYPE_SET R"_(\s*\{\s*([^}]*)\s*\}\s*)_"

#define CMPOP R"_(\s*(&?[=!]=|s?[<>]=?)\s*)_"
#define LABEL R"_((<\w[a-zA-Z_0-9]*>))_"
#define WRAPPED_LABEL "\\s*" LABEL "\\s*"

#define SPECIAL_VAR R"_(\s*(packet_size|meta_offset)\s*)_"
#define KIND \
    R"_(\s*(svalue|uvalue|ctx_offset|map_fd|map_fd_programs|packet_offset|shared_offset|stack_offset|shared_region_size|stack_numeric_size)\s*)_"
#define INTERVAL R"_(\s*\[([-+]?\d+),\s*([-+]?\d+)\]?\s*)_"
#define ARRAY_RANGE R"_(\s*\[([-+]?\d+)\.\.\.\s*([-+]?\d+)\]?\s*)_"

#define DOT "[.]"
#define TYPE R"_(\s*(shared|number|packet|stack|ctx|map_fd|map_fd_programs)\s*)_"

// Match map_val(fd) + offset
#define MAP_VAL R"_(\s*map_val\((\d+)\)\s*\+\s*(\d+)\s*)_"

// Match map_fd fd
#define MAP_FD R"_(\s*map_fd\s+(\d+)\s*)_"

// Match map_fd fd
#define MAP_FD_PROGRAMS R"_(\s*map_fd_programs\s+(\d+)\s*)_"

static const std::map<std::string, Bin::Op> str_to_binop = {
    {"", Bin::Op::MOV},        {"+", Bin::Op::ADD},   {"-", Bin::Op::SUB},     {"*", Bin::Op::MUL},
    {"/", Bin::Op::UDIV},      {"%", Bin::Op::UMOD},  {"|", Bin::Op::OR},      {"&", Bin::Op::AND},
    {"<<", Bin::Op::LSH},      {">>", Bin::Op::RSH},  {"s>>", Bin::Op::ARSH},  {"^", Bin::Op::XOR},
    {"s/", Bin::Op::SDIV},     {"s%", Bin::Op::SMOD}, {"s8", Bin::Op::MOVSX8}, {"s16", Bin::Op::MOVSX16},
    {"s32", Bin::Op::MOVSX32},
};

static const std::map<std::string, Un::Op> str_to_unop = {
    {"be16", Un::Op::BE16},     {"be32", Un::Op::BE32}, {"be64", Un::Op::BE64},     {"le16", Un::Op::LE16},
    {"le32", Un::Op::LE32},     {"le64", Un::Op::LE64}, {"swap16", Un::Op::SWAP16}, {"swap32", Un::Op::SWAP32},
    {"swap64", Un::Op::SWAP64}, {"-", Un::Op::NEG},
};

static const std::map<std::string, Condition::Op> str_to_cmpop = {
    {"==", Condition::Op::EQ},  {"!=", Condition::Op::NE},   {"&==", Condition::Op::SET}, {"&!=", Condition::Op::NSET},
    {"<", Condition::Op::LT},   {"<=", Condition::Op::LE},   {">", Condition::Op::GT},    {">=", Condition::Op::GE},
    {"s<", Condition::Op::SLT}, {"s<=", Condition::Op::SLE}, {"s>", Condition::Op::SGT},  {"s>=", Condition::Op::SGE},
};

static const std::map<std::string, Atomic::Op> str_to_atomicop = {{"+", Atomic::Op::ADD},  {"|", Atomic::Op::OR},
                                                                  {"&", Atomic::Op::AND},  {"^", Atomic::Op::XOR},
                                                                  {"x", Atomic::Op::XCHG}, {"cx", Atomic::Op::CMPXCHG}};

static const std::map<std::string, int> str_to_width = {
    {"8", 1},
    {"16", 2},
    {"32", 4},
    {"64", 8},
};

static bool is64_reg(const std::string& s) { return s.at(0) == 'r'; }

static int to_int(const std::string& s) { return std::stoi(s, nullptr, 0); }

static Number signed_number(const std::string& s) { return std::stoll(s, nullptr, 0); }

static Number unsigned_number(const std::string& s) { return std::stoull(s, nullptr, 0); }

static Reg reg(const std::string& s) {
    assert(s.at(0) == 'r' || s.at(0) == 'w');
    const uint8_t res = static_cast<uint8_t>(to_int(s.substr(1)));
    return Reg{res};
}

static uint8_t regnum(const std::string& s) { return static_cast<uint8_t>(to_int(s.substr(1))); }

static Imm imm(const std::string& s, const bool lddw) {
    if (lddw) {
        if (s.at(0) == '-') {
            return Imm{static_cast<uint64_t>(std::stoll(s, nullptr, 0))};
        } else {
            return Imm{std::stoull(s, nullptr, 0)};
        }
    } else {
        if (s.at(0) == '-') {
            return Imm{static_cast<uint64_t>(std::stol(s, nullptr, 0))};
        } else {
            return Imm{static_cast<uint64_t>(static_cast<int64_t>(static_cast<int32_t>(std::stoul(s, nullptr, 0))))};
        }
    }
}
static Value reg_or_imm(const std::string& s) {
    if (s.at(0) == 'w' || s.at(0) == 'r') {
        return reg(s);
    } else {
        return imm(s, false);
    }
}

static Deref deref(const std::string& width, const std::string& basereg, const std::string& sign,
                   const std::string& _offset) {
    const int offset = to_int(_offset);
    return Deref{
        .width = str_to_width.at(width),
        .basereg = reg(basereg),
        .offset = (sign == "-" ? -offset : +offset),
    };
}

Instruction parse_instruction(const std::string& line, const std::map<std::string, Label>& label_name_to_label) {
    // treat ";" as a comment
    std::string text = line.substr(0, line.find(';'));
    const size_t end = text.find_last_not_of(' ');
    if (end != std::string::npos) {
        text = text.substr(0, end + 1);
    }
    std::smatch m;
    if (regex_match(text, m, regex("exit"))) {
        return Exit{};
    }
    if (regex_match(text, m, regex("call " FUNC))) {
        const int func = to_int(m[1]);
        return make_call(func, g_ebpf_platform_linux);
    }
    if (regex_match(text, m, regex("call " WRAPPED_LABEL))) {
        return CallLocal{.target = label_name_to_label.at(m[1])};
    }
    if (regex_match(text, m, regex("callx " REG))) {
        return Callx{reg(m[1])};
    }
    if (regex_match(text, m, regex(WREG OPASSIGN WREG))) {
        const std::string r = m[1];
        return Bin{.op = str_to_binop.at(m[2]), .dst = reg(r), .v = reg(m[3]), .is64 = is64_reg(r), .lddw = false};
    }
    if (regex_match(text, m, regex(WREG ASSIGN UNOP WREG))) {
        if (m[1] != m[3]) {
            throw std::invalid_argument(std::string("Invalid unary operation: ") + text);
        }
        return Un{.op = str_to_unop.at(m[2]), .dst = reg(m[1]), .is64 = is64_reg(m[1])};
    }
    if (regex_match(text, m, regex(WREG ASSIGN MAP_VAL))) {
        return LoadMapAddress{.dst = reg(m[1]), .mapfd = to_int(m[2]), .offset = to_int(m[3])};
    }
    if (regex_match(text, m, regex(WREG ASSIGN MAP_FD_PROGRAMS))) {
        return LoadMapFd{.dst = reg(m[1]), .mapfd = to_int(m[2])};
    }
    if (regex_match(text, m, regex(WREG ASSIGN MAP_FD))) {
        return LoadMapFd{.dst = reg(m[1]), .mapfd = to_int(m[2])};
    }
    if (regex_match(text, m, regex(WREG OPASSIGN IMM LONGLONG))) {
        const std::string r = m[1];
        const bool lddw = !m[4].str().empty();
        return Bin{.op = str_to_binop.at(m[2]), .dst = reg(r), .v = imm(m[3], lddw), .is64 = is64_reg(r), .lddw = lddw};
    }
    if (regex_match(text, m, regex(REG ASSIGN DEREF PAREN(REG PLUSMINUS IMM)))) {
        return Mem{
            .access = deref(m[2], m[3], m[4], m[5]),
            .value = reg(m[1]),
            .is_load = true,
        };
    }
    if (regex_match(text, m, regex(DEREF PAREN(REG PLUSMINUS IMM) ASSIGN REG_OR_IMM))) {
        return Mem{
            .access = deref(m[1], m[2], m[3], m[4]),
            .value = reg_or_imm(m[5]),
            .is_load = false,
        };
    }
    if (regex_match(text, m, regex("lock " DEREF PAREN(REG PLUSMINUS IMM) " " ATOMICOP " " REG "( fetch)?"))) {
        const Atomic::Op op = str_to_atomicop.at(m[5]);
        return Atomic{.op = op,
                      .fetch = m[7].matched || op == Atomic::Op::XCHG || op == Atomic::Op::CMPXCHG,
                      .access = deref(m[1], m[2], m[3], m[4]),
                      .valreg = reg(m[6])};
    }
    if (regex_match(text, m, regex("r0 = " DEREF "skb\\[(.*)\\]"))) {
        const auto width = str_to_width.at(m[1]);
        const std::string access = m[2].str();
        if (regex_match(access, m, regex(REG))) {
            return Packet{.width = width, .offset = 0, .regoffset = reg(m[1])};
        }
        if (regex_match(access, m, regex(IMM))) {
            return Packet{.width = width, .offset = static_cast<int32_t>(imm(m[1], false).v), .regoffset = {}};
        }
        if (regex_match(access, m, regex(REG PLUSMINUS REG))) {
            return Packet{.width = width, .offset = 0 /* ? */, .regoffset = reg(m[2])};
        }
        if (regex_match(access, m, regex(REG PLUSMINUS IMM))) {
            return Packet{.width = width, .offset = static_cast<int32_t>(imm(m[2], false).v), .regoffset = reg(m[1])};
        }
        return Undefined{0};
    }
    if (regex_match(text, m, regex("assume " WREG CMPOP REG_OR_IMM))) {
        Assume res{
            .cond =
                Condition{
                    .op = str_to_cmpop.at(m[2]), .left = reg(m[1]), .right = reg_or_imm(m[3]), .is64 = is64_reg(m[1])},
            .is_implicit = false,
        };
        return res;
    }
    if (regex_match(text, m, regex("(?:if " WREG CMPOP REG_OR_IMM " )?goto\\s+(?:" IMM ")?" WRAPPED_LABEL))) {
        // We ignore second IMM
        Jmp res{.cond = {}, .target = label_name_to_label.at(m[5])};
        if (m[1].matched) {
            res.cond = Condition{
                .op = str_to_cmpop.at(m[2]), .left = reg(m[1]), .right = reg_or_imm(m[3]), .is64 = is64_reg(m[1])};
        }
        return res;
    }
    return Undefined{0};
}

[[maybe_unused]]
static InstructionSeq parse_program(std::istream& is) {
    std::string line;
    std::vector<Label> pc_to_label;
    InstructionSeq labeled_insts;
    const std::set<Label> seen_labels;
    std::optional<Label> next_label;
    while (std::getline(is, line)) {
        std::smatch m;
        if (regex_search(line, m, regex(LABEL ":"))) {
            next_label = Label{to_int(m[1])};
            if (seen_labels.contains(*next_label)) {
                throw std::invalid_argument("duplicate labels");
            }
            line = m.suffix();
        }
        if (regex_search(line, m, regex(R"(^\s*(\d+:)?\s*)"))) {
            line = m.suffix();
        }
        if (line.empty()) {
            continue;
        }
        Instruction ins = parse_instruction(line, {});
        if (std::holds_alternative<Undefined>(ins)) {
            continue;
        }

        if (!next_label) {
            next_label = Label(static_cast<int>(labeled_insts.size()));
        }
        labeled_insts.emplace_back(*next_label, ins, std::optional<btf_line_info_t>());
        next_label = {};
    }
    return labeled_insts;
}

static Variable special_var(const std::string& s) {
    if (s == "packet_size") {
        return variable_registry->packet_size();
    }
    if (s == "meta_offset") {
        return variable_registry->meta_offset();
    }
    throw std::runtime_error(std::string() + "Bad special variable: " + s);
}

TypeValueConstraints parse_linear_constraints(const std::set<std::string>& constraints,
                                              std::vector<Interval>& numeric_ranges) {
    using namespace dsl_syntax;

    std::vector<LinearConstraint> value_csts;
    std::vector<LinearConstraint> type_csts;
    for (const std::string& cst_text : constraints) {
        std::smatch m;
        if (regex_match(cst_text, m, regex(SPECIAL_VAR "=" IMM))) {
            value_csts.push_back(special_var(m[1]) == signed_number(m[2]));
        } else if (regex_match(cst_text, m, regex(SPECIAL_VAR "=" INTERVAL))) {
            Variable d = special_var(m[1]);
            Number lb{signed_number(m[2])};
            Number ub{signed_number(m[3])};
            value_csts.push_back(lb <= d);
            value_csts.push_back(d <= ub);
        } else if (regex_match(cst_text, m, regex(SPECIAL_VAR "=" REG DOT KIND))) {
            LinearExpression d = special_var(m[1]);
            LinearExpression s = variable_registry->reg(regkind(m[3]), regnum(m[2]));
            value_csts.push_back(d == s);
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" SPECIAL_VAR))) {
            LinearExpression d = variable_registry->reg(regkind(m[2]), regnum(m[1]));
            LinearExpression s = special_var(m[3]);
            value_csts.push_back(d == s);
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" REG DOT KIND))) {
            LinearExpression d = variable_registry->reg(regkind(m[2]), regnum(m[1]));
            LinearExpression s = variable_registry->reg(regkind(m[4]), regnum(m[3]));
            value_csts.push_back(d == s);
        } else if (regex_match(cst_text, m,
                               regex(REG DOT "type"
                                             "=" REG DOT "type"))) {
            LinearExpression d = variable_registry->type_reg(regnum(m[1]));
            LinearExpression s = variable_registry->type_reg(regnum(m[2]));
            type_csts.push_back(d == s);
        } else if (regex_match(cst_text, m,
                               regex(REG DOT "type"
                                             "=" TYPE))) {
            Variable d = variable_registry->type_reg(regnum(m[1]));
            type_csts.push_back(d == string_to_type_encoding(m[2]));
        } else if (regex_match(cst_text, m, regex(REG DOT "type" IN TYPE_SET))) {
            Variable d = variable_registry->type_reg(regnum(m[1]));
            const std::string inside = m[2]; // everything between the braces

            // Tokenize items inside {...} using the existing TYPE regex.
            static const regex type_tok_regex(TYPE);

            bool any = false;
            Number lb = 0, ub = 0; // initialize once we see the first item

            for (std::sregex_iterator it(inside.begin(), inside.end(), type_tok_regex), end; it != end; ++it) {
                // TYPE has a single capturing group with the symbolic token
                const auto sym = (*it)[1].str();
                const auto enc = string_to_type_encoding(sym);

                // Convert to Number for the DSL constraints
                const Number n = static_cast<int>(enc);
                if (!any) {
                    lb = ub = n;
                    any = true;
                } else {
                    if (n < lb) {
                        lb = n;
                    }
                    if (n > ub) {
                        ub = n;
                    }
                }
            }

            if (!any) {
                throw std::runtime_error("Empty type set in 'in { ... }' constraint: " + cst_text);
            }

            // Emit interval over-approx: lb <= d <= ub
            type_csts.push_back(lb <= d);
            type_csts.push_back(d <= ub);
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" IMM))) {
            Variable d = variable_registry->reg(regkind(m[2]), regnum(m[1]));
            Number value;
            if (m[2] == "uvalue") {
                value = unsigned_number(m[3]);
            } else {
                value = signed_number(m[3]);
            }
            value_csts.push_back(d == value);
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" INTERVAL))) {
            Variable d = variable_registry->reg(regkind(m[2]), regnum(m[1]));
            Number lb, ub;
            if (m[2] == "uvalue") {
                lb = unsigned_number(m[3]);
                ub = unsigned_number(m[4]);
            } else {
                lb = signed_number(m[3]);
                ub = signed_number(m[4]);
            }
            value_csts.push_back(lb <= d);
            value_csts.push_back(d <= ub);
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "-" REG DOT KIND "<=" IMM))) {
            Variable d = variable_registry->reg(regkind(m[2]), regnum(m[1]));
            Variable s = variable_registry->reg(regkind(m[4]), regnum(m[3]));
            Number diff = signed_number(m[5]);
            value_csts.push_back(d - s <= diff);
        } else if (regex_match(cst_text, m,
                               regex("s" ARRAY_RANGE DOT "type"
                                     "=" TYPE))) {
            TypeEncoding type = string_to_type_encoding(m[3]);
            if (type == T_NUM) {
                numeric_ranges.emplace_back(signed_number(m[1]), signed_number(m[2]));
            } else {
                Number lb = signed_number(m[1]);
                Number ub = signed_number(m[2]);
                Variable d = variable_registry->cell_var(DataKind::types, lb, ub - lb + 1);
                type_csts.push_back(d == type);
            }
        } else if (regex_match(cst_text, m,
                               regex("s" ARRAY_RANGE DOT "svalue"
                                     "=" IMM))) {
            Number lb = signed_number(m[1]);
            Number ub = signed_number(m[2]);
            Variable d = variable_registry->cell_var(DataKind::svalues, lb, ub - lb + 1);
            value_csts.push_back(d == signed_number(m[3]));
        } else if (regex_match(cst_text, m,
                               regex("s" ARRAY_RANGE DOT "uvalue"
                                     "=" IMM))) {
            Number lb = signed_number(m[1]);
            Number ub = signed_number(m[2]);
            Variable d = variable_registry->cell_var(DataKind::uvalues, lb, ub - lb + 1);
            value_csts.push_back(d == unsigned_number(m[3]));
        } else {
            throw std::runtime_error(std::string("Unknown constraint: ") + cst_text);
        }
    }
    return {type_csts, value_csts};
}

// return a-b, taking account potential optional-none
StringInvariant StringInvariant::operator-(const StringInvariant& b) const {
    if (this->is_bottom()) {
        return bottom();
    }
    StringInvariant res = top();
    for (const std::string& cst : this->value()) {
        if (b.is_bottom() || !b.contains(cst)) {
            res.maybe_inv->insert(cst);
        }
    }
    return res;
}

// return a+b, taking account potential optional-none
StringInvariant StringInvariant::operator+(const StringInvariant& b) const {
    if (this->is_bottom()) {
        return b;
    }
    StringInvariant res = *this;
    for (const std::string& cst : b.value()) {
        if (res.is_bottom() || !res.contains(cst)) {
            res.maybe_inv->insert(cst);
        }
    }
    return res;
}

std::ostream& operator<<(std::ostream& o, const StringInvariant& inv) {
    if (inv.is_bottom()) {
        return o << "_|_";
    }
    // Intervals
    bool first = true;
    o << "[";
    auto& set = inv.maybe_inv.value();
    std::string lastbase;
    for (const auto& item : set) {
        if (first) {
            first = false;
        } else {
            o << ", ";
        }
        const size_t pos = item.find_first_of(".=[");
        std::string base = item.substr(0, pos);
        if (base != lastbase) {
            o << "\n    ";
            lastbase = base;
        }
        o << item;
    }
    o << "]";
    return o;
}
} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <map>
4	#include <regex>
5	#include <sstream>
6	#include <string>
7
8	#include "arith/dsl_syntax.hpp"
9	#include "arith/linear_constraint.hpp"
10	#include "asm_parse.hpp"
11	#include "asm_unmarshal.hpp"
12	#include "crab/type_encoding.hpp"
13	#include "crab/var_registry.hpp"
14	#include "platform.hpp"
15	#include "string_constraints.hpp"
16
17	using std::regex;
18	using std::regex_match;
19
20	namespace prevail {
21	#define REG R"_(\s(r\d\d?)\s)_"
22	#define WREG R"_(\s([wr]\d\d?)\s)_"
23	#define IMM R"_(\s\[?([-+]?(?:0x)?[0-9a-f]+)\]?\s)_"
24	#define REG_OR_IMM R"_(\s([+-]?(?:0x)?[0-9a-f]+\|r\d\d?)\s)_"
25
26	#define FUNC IMM
27	#define OPASSIGN R"_(\s(\S)=\s*)_"
28	#define ASSIGN R"_(\s=\s)_"
29	#define LONGLONG R"_(\s(ll\|)\s)_"
30	#define UNOP R"_((-\|be16\|be32\|be64\|le16\|le32\|le64\|swap16\|swap32\|swap64))_"
31	#define ATOMICOP R"_((\+\|\\|\|&\|\^\|x\|cx)=)_"
32
33	#define PLUSMINUS R"_((\s[+-])\s)_"
34	#define LPAREN R"_(\s\(\s)_"
35	#define RPAREN R"_(\s\)\s)_"
36
37	#define PAREN(x) LPAREN x RPAREN
38	#define STAR R"_(\s\\s*)_"
39	#define DEREF STAR PAREN("u(\\d+)" STAR)
40
41	#define IN R"_(\sin\s)_"
42	#define TYPE_SET R"_(\s\{\s([^}])\s\}\s*)_"
43
44	#define CMPOP R"_(\s(&?[=!]=\|s?[<>]=?)\s)_"
45	#define LABEL R"_((<\w[a-zA-Z_0-9]*>))_"
46	#define WRAPPED_LABEL "\\s" LABEL "\\s"
47
48	#define SPECIAL_VAR R"_(\s(packet_size\|meta_offset)\s)_"
49	#define KIND \
50	R"_(\s(svalue\|uvalue\|ctx_offset\|map_fd\|map_fd_programs\|packet_offset\|shared_offset\|stack_offset\|shared_region_size\|stack_numeric_size)\s)_"
51	#define INTERVAL R"_(\s\[([-+]?\d+),\s([-+]?\d+)\]?\s*)_"
52	#define ARRAY_RANGE R"_(\s\[([-+]?\d+)\.\.\.\s([-+]?\d+)\]?\s*)_"
53
54	#define DOT "[.]"
55	#define TYPE R"_(\s(shared\|number\|packet\|stack\|ctx\|map_fd\|map_fd_programs)\s)_"
56
57	// Match map_val(fd) + offset
58	#define MAP_VAL R"_(\smap_val\((\d+)\)\s\+\s(\d+)\s)_"
59
60	// Match map_fd fd
61	#define MAP_FD R"_(\smap_fd\s+(\d+)\s)_"
62
63	// Match map_fd fd
64	#define MAP_FD_PROGRAMS R"_(\smap_fd_programs\s+(\d+)\s)_"
65
66	static const std::map<std::string, Bin::Op> str_to_binop = {
67	{"", Bin::Op::MOV}, {"+", Bin::Op::ADD}, {"-", Bin::Op::SUB}, {"*", Bin::Op::MUL},
68	{"/", Bin::Op::UDIV}, {"%", Bin::Op::UMOD}, {"\|", Bin::Op::OR}, {"&", Bin::Op::AND},
69	{"<<", Bin::Op::LSH}, {">>", Bin::Op::RSH}, {"s>>", Bin::Op::ARSH}, {"^", Bin::Op::XOR},
70	{"s/", Bin::Op::SDIV}, {"s%", Bin::Op::SMOD}, {"s8", Bin::Op::MOVSX8}, {"s16", Bin::Op::MOVSX16},
71	{"s32", Bin::Op::MOVSX32},
72	};
73
74	static const std::map<std::string, Un::Op> str_to_unop = {
75	{"be16", Un::Op::BE16}, {"be32", Un::Op::BE32}, {"be64", Un::Op::BE64}, {"le16", Un::Op::LE16},
76	{"le32", Un::Op::LE32}, {"le64", Un::Op::LE64}, {"swap16", Un::Op::SWAP16}, {"swap32", Un::Op::SWAP32},
77	{"swap64", Un::Op::SWAP64}, {"-", Un::Op::NEG},
78	};
79
80	static const std::map<std::string, Condition::Op> str_to_cmpop = {
81	{"==", Condition::Op::EQ}, {"!=", Condition::Op::NE}, {"&==", Condition::Op::SET}, {"&!=", Condition::Op::NSET},
82	{"<", Condition::Op::LT}, {"<=", Condition::Op::LE}, {">", Condition::Op::GT}, {">=", Condition::Op::GE},
83	{"s<", Condition::Op::SLT}, {"s<=", Condition::Op::SLE}, {"s>", Condition::Op::SGT}, {"s>=", Condition::Op::SGE},
84	};
85
86	static const std::map<std::string, Atomic::Op> str_to_atomicop = {{"+", Atomic::Op::ADD}, {"\|", Atomic::Op::OR},
87	{"&", Atomic::Op::AND}, {"^", Atomic::Op::XOR},
88	{"x", Atomic::Op::XCHG}, {"cx", Atomic::Op::CMPXCHG}};
89
90	static const std::map<std::string, int> str_to_width = {
91	{"8", 1},
92	{"16", 2},
93	{"32", 4},
94	{"64", 8},
95	};
96
97	static bool is64_reg(const std::string& s) { return s.at(0) == 'r'; }	141,402✔
98
99	static int to_int(const std::string& s) { return std::stoi(s, nullptr, 0); }	159,350✔
100
101	static Number signed_number(const std::string& s) { return std::stoll(s, nullptr, 0); }	5,148✔
102
103	static Number unsigned_number(const std::string& s) { return std::stoull(s, nullptr, 0); }	1,968✔
104
105	static Reg reg(const std::string& s) {	143,268✔
106	assert(s.at(0) == 'r' \|\| s.at(0) == 'w');	143,268✔
107	const uint8_t res = static_cast<uint8_t>(to_int(s.substr(1)));	143,268✔
108	return Reg{res};	143,268✔
109	}
110
111	static uint8_t regnum(const std::string& s) { return static_cast<uint8_t>(to_int(s.substr(1))); }	6,802✔
112
113	static Imm imm(const std::string& s, const bool lddw) {	61,580✔
114	if (lddw) {	61,580✔
115	if (s.at(0) == '-') {	3,900✔
116	return Imm{static_cast<uint64_t>(std::stoll(s, nullptr, 0))};	2,618✔
117	} else {
118	return Imm{std::stoull(s, nullptr, 0)};	1,282✔
119	}
120	} else {
121	if (s.at(0) == '-') {	57,680✔
122	return Imm{static_cast<uint64_t>(std::stol(s, nullptr, 0))};	7,328✔
123	} else {
124	return Imm{static_cast<uint64_t>(static_cast<int64_t>(static_cast<int32_t>(std::stoul(s, nullptr, 0))))};	50,352✔
125	}
126	}
127	}
128	static Value reg_or_imm(const std::string& s) {	52,486✔
129	if (s.at(0) == 'w' \|\| s.at(0) == 'r') {	52,486✔
130	return reg(s);	17,910✔
131	} else {
132	return imm(s, false);	34,576✔
133	}
134	}
135
136	static Deref deref(const std::string& width, const std::string& basereg, const std::string& sign,	8,314✔
137	const std::string& _offset) {
138	const int offset = to_int(_offset);	8,314✔
139	return Deref{	4,157✔
140	.width = str_to_width.at(width),	8,314✔
141	.basereg = reg(basereg),	8,314✔
142	.offset = (sign == "-" ? -offset : +offset),	8,314✔
143	};	12,471✔
144	}
145
146	Instruction parse_instruction(const std::string& line, const std::map<std::string, Label>& label_name_to_label) {	114,094✔
147	// treat ";" as a comment
148	std::string text = line.substr(0, line.find(';'));	114,094✔
149	const size_t end = text.find_last_not_of(' ');	114,094✔
150	if (end != std::string::npos) {	114,094✔
151	text = text.substr(0, end + 1);	114,094✔
152	}
153	std::smatch m;	114,094✔
154	if (regex_match(text, m, regex("exit"))) {	114,094✔
155	return Exit{};	5,954✔
156	}
157	if (regex_match(text, m, regex("call " FUNC))) {	108,140✔
158	const int func = to_int(m[1]);	954✔
159	return make_call(func, g_ebpf_platform_linux);	1,431✔
160	}
161	if (regex_match(text, m, regex("call " WRAPPED_LABEL))) {	107,186✔
162	return CallLocal{.target = label_name_to_label.at(m[1])};	960✔
163	}
164	if (regex_match(text, m, regex("callx " REG))) {	106,226✔
165	return Callx{reg(m[1])};	1,104✔
166	}
167	if (regex_match(text, m, regex(WREG OPASSIGN WREG))) {	105,122✔
168	const std::string r = m[1];	15,390✔
169	return Bin{.op = str_to_binop.at(m[2]), .dst = reg(r), .v = reg(m[3]), .is64 = is64_reg(r), .lddw = false};	15,390✔
170	}	15,390✔
171	if (regex_match(text, m, regex(WREG ASSIGN UNOP WREG))) {	89,732✔
172	if (m[1] != m[3]) {	1,632✔
173	throw std::invalid_argument(std::string("Invalid unary operation: ") + text);	×
174	}
175	return Un{.op = str_to_unop.at(m[2]), .dst = reg(m[1]), .is64 = is64_reg(m[1])};	1,632✔
176	}
177	if (regex_match(text, m, regex(WREG ASSIGN MAP_VAL))) {	88,100✔
178	return LoadMapAddress{.dst = reg(m[1]), .mapfd = to_int(m[2]), .offset = to_int(m[3])};	4✔
179	}
180	if (regex_match(text, m, regex(WREG ASSIGN MAP_FD_PROGRAMS))) {	88,096✔
181	return LoadMapFd{.dst = reg(m[1]), .mapfd = to_int(m[2])};	×
182	}
183	if (regex_match(text, m, regex(WREG ASSIGN MAP_FD))) {	88,096✔
184	return LoadMapFd{.dst = reg(m[1]), .mapfd = to_int(m[2])};	4✔
185	}
186	if (regex_match(text, m, regex(WREG OPASSIGN IMM LONGLONG))) {	88,092✔
187	const std::string r = m[1];	26,902✔
188	const bool lddw = !m[4].str().empty();	26,902✔
189	return Bin{.op = str_to_binop.at(m[2]), .dst = reg(r), .v = imm(m[3], lddw), .is64 = is64_reg(r), .lddw = lddw};	26,902✔
190	}	26,902✔
191	if (regex_match(text, m, regex(REG ASSIGN DEREF PAREN(REG PLUSMINUS IMM)))) {	61,190✔
192	return Mem{	2,126✔
193	.access = deref(m[2], m[3], m[4], m[5]),	4,252✔
194	.value = reg(m[1]),	4,252✔
195	.is_load = true,
196	};	2,126✔
197	}
198	if (regex_match(text, m, regex(DEREF PAREN(REG PLUSMINUS IMM) ASSIGN REG_OR_IMM))) {	59,064✔
199	return Mem{	1,071✔
200	.access = deref(m[1], m[2], m[3], m[4]),	4,284✔
201	.value = reg_or_imm(m[5]),	4,284✔
202	.is_load = false,
203	};	2,142✔
204	}
205	if (regex_match(text, m, regex("lock " DEREF PAREN(REG PLUSMINUS IMM) " " ATOMICOP " " REG "( fetch)?"))) {	56,922✔
206	const Atomic::Op op = str_to_atomicop.at(m[5]);	4,046✔
207	return Atomic{.op = op,	6,069✔
208	.fetch = m[7].matched \|\| op == Atomic::Op::XCHG \|\| op == Atomic::Op::CMPXCHG,	4,046✔
209	.access = deref(m[1], m[2], m[3], m[4]),	8,092✔
210	.valreg = reg(m[6])};	4,046✔
211	}
212	if (regex_match(text, m, regex("r0 = " DEREF "skb\\[(.*)\\]"))) {	52,876✔
213	const auto width = str_to_width.at(m[1]);	204✔
214	const std::string access = m[2].str();	204✔
215	if (regex_match(access, m, regex(REG))) {	204✔
216	return Packet{.width = width, .offset = 0, .regoffset = reg(m[1])};	102✔
217	}
218	if (regex_match(access, m, regex(IMM))) {	102✔
219	return Packet{.width = width, .offset = static_cast<int32_t>(imm(m[1], false).v), .regoffset = {}};	102✔
220	}
221	if (regex_match(access, m, regex(REG PLUSMINUS REG))) {	×
222	return Packet{.width = width, .offset = 0 /* ? */, .regoffset = reg(m[2])};	×
223	}
224	if (regex_match(access, m, regex(REG PLUSMINUS IMM))) {	×
225	return Packet{.width = width, .offset = static_cast<int32_t>(imm(m[2], false).v), .regoffset = reg(m[1])};	×
226	}
227	return Undefined{0};	×
228	}	204✔
229	if (regex_match(text, m, regex("assume " WREG CMPOP REG_OR_IMM))) {	52,672✔
230	Assume res{	44,704✔
231	.cond =
232	Condition{
233	.op = str_to_cmpop.at(m[2]), .left = reg(m[1]), .right = reg_or_imm(m[3]), .is64 = is64_reg(m[1])},	134,112✔
234	.is_implicit = false,
235	};	89,408✔
236	return res;	44,704✔
237	}
238	if (regex_match(text, m, regex("(?:if " WREG CMPOP REG_OR_IMM " )?goto\\s+(?:" IMM ")?" WRAPPED_LABEL))) {	7,968✔
239	// We ignore second IMM
240	Jmp res{.cond = {}, .target = label_name_to_label.at(m[5])};	7,968✔
241	if (m[1].matched) {	7,968✔
242	res.cond = Condition{	8,460✔
243	.op = str_to_cmpop.at(m[2]), .left = reg(m[1]), .right = reg_or_imm(m[3]), .is64 = is64_reg(m[1])};	8,460✔
244	}
245	return res;	7,968✔
246	}	7,968✔
247	return Undefined{0};	×
248	}	114,094✔
249
250	[[maybe_unused]]
251	static InstructionSeq parse_program(std::istream& is) {
252	std::string line;
253	std::vector<Label> pc_to_label;
254	InstructionSeq labeled_insts;
255	const std::set<Label> seen_labels;
256	std::optional<Label> next_label;
257	while (std::getline(is, line)) {
258	std::smatch m;
259	if (regex_search(line, m, regex(LABEL ":"))) {
260	next_label = Label{to_int(m[1])};
261	if (seen_labels.contains(*next_label)) {
262	throw std::invalid_argument("duplicate labels");
263	}
264	line = m.suffix();
265	}
266	if (regex_search(line, m, regex(R"(^\s(\d+:)?\s)"))) {
267	line = m.suffix();
268	}
269	if (line.empty()) {
270	continue;
271	}
272	Instruction ins = parse_instruction(line, {});
273	if (std::holds_alternative<Undefined>(ins)) {
274	continue;
275	}
276
277	if (!next_label) {
278	next_label = Label(static_cast<int>(labeled_insts.size()));
279	}
280	labeled_insts.emplace_back(*next_label, ins, std::optional<btf_line_info_t>());
281	next_label = {};
282	}
283	return labeled_insts;
284	}
285
286	static Variable special_var(const std::string& s) {	88✔
287	if (s == "packet_size") {	88✔
288	return variable_registry->packet_size();	46✔
289	}
290	if (s == "meta_offset") {	42✔
291	return variable_registry->meta_offset();	42✔
292	}
293	throw std::runtime_error(std::string() + "Bad special variable: " + s);	×
294	}
295
296	TypeValueConstraints parse_linear_constraints(const std::set<std::string>& constraints,	1,828✔
297	std::vector<Interval>& numeric_ranges) {
298	using namespace dsl_syntax;	914✔
299
300	std::vector<LinearConstraint> value_csts;	1,828✔
301	std::vector<LinearConstraint> type_csts;	1,828✔
302	for (const std::string& cst_text : constraints) {	9,092✔
303	std::smatch m;	7,264✔
304	if (regex_match(cst_text, m, regex(SPECIAL_VAR "=" IMM))) {	7,264✔
305	value_csts.push_back(special_var(m[1]) == signed_number(m[2]));	112✔
306	} else if (regex_match(cst_text, m, regex(SPECIAL_VAR "=" INTERVAL))) {	7,208✔
307	Variable d = special_var(m[1]);	16✔
308	Number lb{signed_number(m[2])};	16✔
309	Number ub{signed_number(m[3])};	16✔
310	value_csts.push_back(lb <= d);	32✔
311	value_csts.push_back(d <= ub);	32✔
312	} else if (regex_match(cst_text, m, regex(SPECIAL_VAR "=" REG DOT KIND))) {	7,208✔
313	LinearExpression d = special_var(m[1]);	2✔
314	LinearExpression s = variable_registry->reg(regkind(m[3]), regnum(m[2]));	3✔
315	value_csts.push_back(d == s);	3✔
316	} else if (regex_match(cst_text, m, regex(REG DOT KIND "=" SPECIAL_VAR))) {	7,192✔
317	LinearExpression d = variable_registry->reg(regkind(m[2]), regnum(m[1]));	21✔
318	LinearExpression s = special_var(m[3]);	14✔
319	value_csts.push_back(d == s);	21✔
320	} else if (regex_match(cst_text, m, regex(REG DOT KIND "=" REG DOT KIND))) {	7,190✔
321	LinearExpression d = variable_registry->reg(regkind(m[2]), regnum(m[1]));	549✔
322	LinearExpression s = variable_registry->reg(regkind(m[4]), regnum(m[3]));	549✔
323	value_csts.push_back(d == s);	549✔
324	} else if (regex_match(cst_text, m,	7,176✔
325	regex(REG DOT "type"	13,620✔
326	"=" REG DOT "type"))) {
327	LinearExpression d = variable_registry->type_reg(regnum(m[1]));	2✔
328	LinearExpression s = variable_registry->type_reg(regnum(m[2]));	2✔
329	type_csts.push_back(d == s);	3✔
330	} else if (regex_match(cst_text, m,	6,810✔
331	regex(REG DOT "type"	13,616✔
332	"=" TYPE))) {
333	Variable d = variable_registry->type_reg(regnum(m[1]));	2,274✔
334	type_csts.push_back(d == string_to_type_encoding(m[2]));	3,411✔
335	} else if (regex_match(cst_text, m, regex(REG DOT "type" IN TYPE_SET))) {	4,534✔
336	Variable d = variable_registry->type_reg(regnum(m[1]));	18✔
337	const std::string inside = m[2]; // everything between the braces	18✔
338
339	// Tokenize items inside {...} using the existing TYPE regex.
340	static const regex type_tok_regex(TYPE);	18✔
341
342	bool any = false;	18✔
343	Number lb = 0, ub = 0; // initialize once we see the first item	18✔
344
345	for (std::sregex_iterator it(inside.begin(), inside.end(), type_tok_regex), end; it != end; ++it) {	54✔
346	// TYPE has a single capturing group with the symbolic token
347	const auto sym = (*it)[1].str();	36✔
348	const auto enc = string_to_type_encoding(sym);	36✔
349
350	// Convert to Number for the DSL constraints
351	const Number n = static_cast<int>(enc);	36✔
352	if (!any) {	36✔
353	lb = ub = n;	18✔
354	any = true;	9✔
355	} else {
356	if (n < lb) {	18✔
357	lb = n;	×
358	}
359	if (n > ub) {	18✔
360	ub = n;	36✔
361	}
362	}
363	}	54✔
364
365	if (!any) {	18✔
366	throw std::runtime_error("Empty type set in 'in { ... }' constraint: " + cst_text);	×
367	}
368
369	// Emit interval over-approx: lb <= d <= ub
370	type_csts.push_back(lb <= d);	36✔
371	type_csts.push_back(d <= ub);	36✔
372	} else if (regex_match(cst_text, m, regex(REG DOT KIND "=" IMM))) {	4,534✔
373	Variable d = variable_registry->reg(regkind(m[2]), regnum(m[1]));	3,750✔
374	Number value;	2,500✔
375	if (m[2] == "uvalue") {	2,500✔
376	value = unsigned_number(m[3]);	1,104✔
377	} else {
378	value = signed_number(m[3]);	2,646✔
379	}
380	value_csts.push_back(d == value);	5,000✔
381	} else if (regex_match(cst_text, m, regex(REG DOT KIND "=" INTERVAL))) {	4,516✔
382	Variable d = variable_registry->reg(regkind(m[2]), regnum(m[1]));	1,887✔
383	Number lb, ub;	1,258✔
384	if (m[2] == "uvalue") {	1,258✔
385	lb = unsigned_number(m[3]);	738✔
386	ub = unsigned_number(m[4]);	738✔
387	} else {
388	lb = signed_number(m[3]);	1,149✔
389	ub = signed_number(m[4]);	1,149✔
390	}
391	value_csts.push_back(lb <= d);	2,516✔
392	value_csts.push_back(d <= ub);	2,516✔
393	} else if (regex_match(cst_text, m, regex(REG DOT KIND "-" REG DOT KIND "<=" IMM))) {	2,016✔
394	Variable d = variable_registry->reg(regkind(m[2]), regnum(m[1]));	×
395	Variable s = variable_registry->reg(regkind(m[4]), regnum(m[3]));	×
396	Number diff = signed_number(m[5]);	×
397	value_csts.push_back(d - s <= diff);	×
398	} else if (regex_match(cst_text, m,	758✔
399	regex("s" ARRAY_RANGE DOT "type"	1,516✔
400	"=" TYPE))) {
401	TypeEncoding type = string_to_type_encoding(m[3]);	262✔
402	if (type == T_NUM) {	262✔
403	numeric_ranges.emplace_back(signed_number(m[1]), signed_number(m[2]));	393✔
404	} else {
405	Number lb = signed_number(m[1]);	×
406	Number ub = signed_number(m[2]);	×
407	Variable d = variable_registry->cell_var(DataKind::types, lb, ub - lb + 1);	×
408	type_csts.push_back(d == type);	×
409	}	×
410	} else if (regex_match(cst_text, m,	496✔
411	regex("s" ARRAY_RANGE DOT "svalue"	992✔
412	"=" IMM))) {
413	Number lb = signed_number(m[1]);	248✔
414	Number ub = signed_number(m[2]);	248✔
415	Variable d = variable_registry->cell_var(DataKind::svalues, lb, ub - lb + 1);	372✔
416	value_csts.push_back(d == signed_number(m[3]));	496✔
417	} else if (regex_match(cst_text, m,	496✔
418	regex("s" ARRAY_RANGE DOT "uvalue"	496✔
419	"=" IMM))) {
420	Number lb = signed_number(m[1]);	248✔
421	Number ub = signed_number(m[2]);	248✔
422	Variable d = variable_registry->cell_var(DataKind::uvalues, lb, ub - lb + 1);	372✔
423	value_csts.push_back(d == unsigned_number(m[3]));	496✔
424	} else {	248✔
425	throw std::runtime_error(std::string("Unknown constraint: ") + cst_text);	×
426	}
427	}	7,264✔
428	return {type_csts, value_csts};	1,828✔
429	}	1,828✔
430
431	// return a-b, taking account potential optional-none
432	StringInvariant StringInvariant::operator-(const StringInvariant& b) const {	×
433	if (this->is_bottom()) {	×
434	return bottom();	×
435	}
436	StringInvariant res = top();	×
437	for (const std::string& cst : this->value()) {	×
438	if (b.is_bottom() \|\| !b.contains(cst)) {	×
439	res.maybe_inv->insert(cst);	×
440	}
441	}
442	return res;	×
443	}	×
444
445	// return a+b, taking account potential optional-none
446	StringInvariant StringInvariant::operator+(const StringInvariant& b) const {	2,660✔
447	if (this->is_bottom()) {	2,660✔
448	return b;	1,518✔
449	}
450	StringInvariant res = *this;	2,472✔
451	for (const std::string& cst : b.value()) {	7,352✔
452	if (res.is_bottom() \|\| !res.contains(cst)) {	4,880✔
453	res.maybe_inv->insert(cst);	4,880✔
454	}
455	}
456	return res;	3,708✔
457	}	2,472✔
458
459	std::ostream& operator<<(std::ostream& o, const StringInvariant& inv) {	×
460	if (inv.is_bottom()) {	×
461	return o << "_\|_";	×
462	}
463	// Intervals
464	bool first = true;	×
465	o << "[";	×
466	auto& set = inv.maybe_inv.value();	×
467	std::string lastbase;	×
468	for (const auto& item : set) {	×
469	if (first) {	×
470	first = false;
471	} else {
472	o << ", ";	×
473	}
474	const size_t pos = item.find_first_of(".=[");	×
475	std::string base = item.substr(0, pos);	×
476	if (base != lastbase) {	×
477	o << "\n ";	×
478	lastbase = base;	×
479	}
480	o << item;	×
481	}	×
482	o << "]";	×
483	return o;	×
484	}	×
485	} // namespace prevail

Alan-Jowett / ebpf-verifier / 18658728485

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous