13958948275

Committed 19 Mar 2025 11:53PM UTC coverage: 88.194% (-0.5%) from 88.66%

Build # 13958948275

Build Type

push

github

Committed by

web-flow

Commit Message

Finite domain (#849)

* Move arithmetic and bit operations functions to finite_domain.cpp
* Remove operator-= (now havoc) and operator+= (now add_constraint)
* Abort early when registers are not usable; clear type variable instead of explicitly assigning T_UNINIT. Update YAML tests accordingly
---------
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Run Details

847 of 898 new or added lines in 11 files covered. (94.32%)

57 existing lines in 8 files now uncovered.

8628 of 9783 relevant lines covered (88.19%)

9034663.84 hits per line

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

77.63

/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;

using crab::linear_constraint_t;
using crab::linear_expression_t;
using crab::number_t;

#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_t signed_number(const std::string& s) { return std::stoll(s); }

static number_t 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_t>& 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_t> pc_to_label;
    InstructionSeq labeled_insts;
    const std::set<label_t> seen_labels;
    std::optional<label_t> next_label;
    while (std::getline(is, line)) {
        std::smatch m;
        if (regex_search(line, m, regex(LABEL ":"))) {
            next_label = label_t(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_t(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 crab::variable_t special_var(const std::string& s) {
    if (s == "packet_size") {
        return crab::variable_t::packet_size();
    }
    if (s == "meta_offset") {
        return crab::variable_t::meta_offset();
    }
    throw std::runtime_error(std::string() + "Bad special variable: " + s);
}

std::vector<linear_constraint_t> parse_linear_constraints(const std::set<std::string>& constraints,
                                                          std::vector<crab::interval_t>& numeric_ranges) {
    using namespace crab::dsl_syntax;
    using crab::regkind;
    using crab::variable_t;

    std::vector<linear_constraint_t> 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_t d = special_var(m[1]);
            number_t lb{signed_number(m[2])};
            number_t 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))) {
            linear_expression_t d = special_var(m[1]);
            linear_expression_t s = variable_t::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))) {
            linear_expression_t d = variable_t::reg(regkind(m[2]), regnum(m[1]));
            linear_expression_t s = special_var(m[3]);
            res.push_back(d == s);
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" REG DOT KIND))) {
            linear_expression_t d = variable_t::reg(regkind(m[2]), regnum(m[1]));
            linear_expression_t s = variable_t::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_t d = variable_t::reg(crab::data_kind_t::types, regnum(m[1]));
            res.push_back(d == crab::string_to_type_encoding(m[2]));
        } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" IMM))) {
            variable_t d = variable_t::reg(regkind(m[2]), regnum(m[1]));
            number_t 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_t d = variable_t::reg(regkind(m[2]), regnum(m[1]));
            number_t 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_t d = variable_t::reg(regkind(m[2]), regnum(m[1]));
            variable_t s = variable_t::reg(regkind(m[4]), regnum(m[3]));
            number_t 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))) {
            crab::type_encoding_t type = crab::string_to_type_encoding(m[3]);
            if (type == crab::type_encoding_t::T_NUM) {
                numeric_ranges.emplace_back(signed_number(m[1]), signed_number(m[2]));
            } else {
                number_t lb = signed_number(m[1]);
                number_t ub = signed_number(m[2]);
                variable_t d = variable_t::cell_var(crab::data_kind_t::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_t lb = signed_number(m[1]);
            number_t ub = signed_number(m[2]);
            variable_t d = variable_t::cell_var(crab::data_kind_t::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_t lb = signed_number(m[1]);
            number_t ub = signed_number(m[2]);
            variable_t d = variable_t::cell_var(crab::data_kind_t::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
string_invariant string_invariant::operator-(const string_invariant& b) const {
    if (this->is_bottom()) {
        return string_invariant::bottom();
    }
    string_invariant res = string_invariant::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
string_invariant string_invariant::operator+(const string_invariant& b) const {
    if (this->is_bottom()) {
        return b;
    }
    string_invariant 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 string_invariant& 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;
}

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

vbpf / ebpf-verifier / 13958948275

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