21993000823

Committed 13 Feb 2026 01:02PM UTC coverage: 86.313% (-0.5%) from 86.783%

Build # 21993000823

Build Type

push

github

Committed by

web-flow

Commit Message

ISA feature support matrix and precise rejection semantics (#999)

* ISA feature support matrix and precise rejection semantics

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Run Details

282 of 380 new or added lines in 14 files covered. (74.21%)

3 existing lines in 3 files now uncovered.

9535 of 11047 relevant lines covered (86.31%)

3060772.25 hits per line

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

79.32

/src/ir/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 "crab/type_encoding.hpp"
#include "crab/var_registry.hpp"
#include "ir/parse.hpp"
#include "ir/unmarshal.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("([us])(\\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*)_"

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

Alan-Jowett / ebpf-verifier / 21993000823

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