15194704016

Committed 22 May 2025 08:53AM UTC coverage: 88.11% (-0.07%) from 88.177%

Build # 15194704016

Build Type

push

github

Committed by

elazarg

Commit Message

uniform class names and explicit constructors for adapt_sgraph.hpp

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

Run Details

27 of 30 new or added lines in 1 file covered. (90.0%)

481 existing lines in 33 files now uncovered.

8552 of 9706 relevant lines covered (88.11%)

9089054.61 hits per line

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

78.76

/src/asm_parse.cpp

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

#include <boost/lexical_cast.hpp>

#include "asm_parse.hpp"
#include "asm_unmarshal.hpp"
#include "crab/dsl_syntax.hpp"
#include "crab/linear_constraint.hpp"
#include "crab/type_encoding.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 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*(type|svalue|uvalue|ctx_offset|map_fd|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*)_"

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 Reg reg(const std::string& s) {
    assert(s.at(0) == 'r' || s.at(0) == 'w');
    const uint8_t res = static_cast<uint8_t>(boost::lexical_cast<uint16_t>(s.substr(1)));
    return Reg{res};
}

static Imm imm(const std::string& s, const bool lddw) {
    const int base = s.find("0x") != std::string::npos ? 16 : 10;

    if (lddw) {
        if (s.at(0) == '-') {
            return Imm{static_cast<uint64_t>(std::stoll(s, nullptr, base))};
        } else {
            return Imm{std::stoull(s, nullptr, base)};
        }
    } else {
        if (s.at(0) == '-') {
            return Imm{static_cast<uint64_t>(std::stol(s, nullptr, base))};
        } else {
            return Imm{static_cast<uint64_t>(static_cast<int64_t>(static_cast<int32_t>(std::stoul(s, nullptr, base))))};
        }
    }
}

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

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

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 = boost::lexical_cast<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 = boost::lexical_cast<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 = boost::lexical_cast<int>(m[2]), .offset = boost::lexical_cast<int>(m[3])};
    }
    if (regex_match(text, m, regex(WREG ASSIGN MAP_FD))) {
        return LoadMapFd{.dst = reg(m[1]), .mapfd = boost::lexical_cast<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(boost::lexical_cast<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 uint8_t regnum(const std::string& s) { return static_cast<uint8_t>(boost::lexical_cast<uint16_t>(s.substr(1))); }

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

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

    std::vector<LinearConstraint> res;
    for (const std::string& cst_text : constraints) {
        std::smatch m;
        if (regex_match(cst_text, m, regex(SPECIAL_VAR "=" IMM))) {
            res.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])};
            res.push_back(lb <= d);
            res.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::reg(regkind(m[3]), regnum(m[2]));
            res.push_back(d == s);
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" SPECIAL_VAR))) {
            LinearExpression d = Variable::reg(regkind(m[2]), regnum(m[1]));
            LinearExpression s = special_var(m[3]);
            res.push_back(d == s);
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" REG DOT KIND))) {
            LinearExpression d = Variable::reg(regkind(m[2]), regnum(m[1]));
            LinearExpression s = Variable::reg(regkind(m[4]), regnum(m[3]));
            res.push_back(d == s);
        } else if (regex_match(cst_text, m,
                               regex(REG DOT "type"
                                             "=" TYPE))) {
            Variable d = Variable::reg(DataKind::types, regnum(m[1]));
            res.push_back(d == string_to_type_encoding(m[2]));
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" IMM))) {
            Variable d = Variable::reg(regkind(m[2]), regnum(m[1]));
            Number value;
            if (m[2] == "uvalue") {
                value = unsigned_number(m[3]);
            } else {
                value = signed_number(m[3]);
            }
            res.push_back(d == value);
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" INTERVAL))) {
            Variable d = Variable::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]);
            }
            res.push_back(lb <= d);
            res.push_back(d <= ub);
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "-" REG DOT KIND "<=" IMM))) {
            Variable d = Variable::reg(regkind(m[2]), regnum(m[1]));
            Variable s = Variable::reg(regkind(m[4]), regnum(m[3]));
            Number diff = signed_number(m[5]);
            res.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::cell_var(DataKind::types, lb, ub - lb + 1);
                res.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::cell_var(DataKind::svalues, lb, ub - lb + 1);
            res.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::cell_var(DataKind::uvalues, lb, ub - lb + 1);
            res.push_back(d == unsigned_number(m[3]));
        } else {
            throw std::runtime_error(std::string("Unknown constraint: ") + cst_text);
        }
    }
    return res;
}

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

Alan-Jowett / ebpf-verifier / 15194704016

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