22160684311

Committed 18 Feb 2026 09:20PM UTC coverage: 88.256% (+1.1%) from 87.142%

Build # 22160684311

Build Type

push

github

Committed by

elazarg

Commit Message

lint

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

Run Details

78 of 82 new or added lines in 6 files covered. (95.12%)

402 existing lines in 18 files now uncovered.

10731 of 12159 relevant lines covered (88.26%)

837642.51 hits per line

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

87.79

/src/ir/parse.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#include <cassert>
#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 "result.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<TypeEquality> type_equalities;
    std::vector<TypeSetRestriction> type_restrictions;
    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"))) {
            Variable d = variable_registry->type_reg(regnum(m[1]));
            Variable s = variable_registry->type_reg(regnum(m[2]));
            type_equalities.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_restrictions.push_back({d, TypeSet{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);

            TypeSet ts{};
            bool any = false;

            for (std::sregex_iterator it(inside.begin(), inside.end(), type_tok_regex), end; it != end; ++it) {
                const auto sym = (*it)[1].str();
                const auto enc = string_to_type_encoding(sym);
                ts |= TypeSet{enc};
                any = true;
            }

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

            type_restrictions.push_back({d, ts});
        } 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_restrictions.push_back({d, TypeSet{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_equalities, type_restrictions, 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 << "_|_";
    }

    // Check for invariant filter
    const RelevantState* filter = get_invariant_filter(o);

    // Intervals
    bool first = true;
    o << "[";
    auto& set = inv.maybe_inv.value();
    std::string lastbase;
    for (const auto& item : set) {
        // Skip items that don't involve relevant registers (if filter is set)
        if (filter && !filter->is_relevant_constraint(item)) {
            continue;
        }

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

Alan-Jowett / ebpf-verifier / 22160684311

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