12951530094

Committed 24 Jan 2025 02:26PM UTC coverage: 88.133% (-0.04%) from 88.169%

Build # 12951530094

Build Type

push

github

Committed by

web-flow

Commit Message

add support for 64bit immediate with type 2 (#820)

Add support for 64bit immediate with type 2

From the ISA RFC:
5.4.  64-bit immediate instructions

   Instructions with the IMM 'mode' modifier use the wide instruction
   encoding defined in Instruction encoding (Section 3), and use the
   'src_reg' field of the basic instruction to hold an opcode subtype.

   The following table defines a set of {IMM, DW, LD} instructions with
   opcode subtypes in the 'src_reg' field, using new terms such as "map"
   defined further below:

    +=========+================================+==========+==========+
    | src_reg | pseudocode                     | imm type | dst type |
    +=========+================================+==========+==========+
    | 0x0     | dst = (next_imm << 32) | imm   | integer  | integer  |
    +---------+--------------------------------+----------+----------+
    | 0x1     | dst = map_by_fd(imm)           | map fd   | map      |
    +---------+--------------------------------+----------+----------+
    | 0x2     | dst = map_val(map_by_fd(imm))  | map fd   | data     |
    |         | + next_imm                     |          | address  |
    +---------+--------------------------------+----------+----------+
    | 0x3     | dst = var_addr(imm)            | variable | data     |
    |         |                                | id       | address  |
    +---------+--------------------------------+----------+----------+
    | 0x4     | dst = code_addr(imm)           | integer  | code     |
    |         |                                |          | address  |
    +---------+--------------------------------+----------+----------+
    | 0x5     | dst = map_by_idx(imm)          | map      | map      |
    |         |                                | index    |          |
    +---------+--------------------------------+----------+----------+
    | 0x6     | dst = map_val(map_by_idx(imm)) | map      | data     |
    |         | + next_imm    ... (continued)

Run Details

81 of 92 new or added lines in 12 files covered. (88.04%)

7 existing lines in 1 file now uncovered.

8533 of 9682 relevant lines covered (88.13%)

7382636.56 hits per line

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

53.58

/src/asm_ostream.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#include <fstream>
#include <iomanip>
#include <iostream>
#include <variant>
#include <vector>

#include "asm_syntax.hpp"
#include "crab/cfg.hpp"
#include "crab/fwd_analyzer.hpp"
#include "crab/interval.hpp"
#include "crab/type_encoding.hpp"
#include "crab/variable.hpp"
#include "crab_utils/num_big.hpp"
#include "crab_verifier.hpp"
#include "helpers.hpp"
#include "platform.hpp"
#include "spec_type_descriptors.hpp"

using crab::TypeGroup;
using std::optional;
using std::string;
using std::vector;

namespace crab {

std::string number_t::to_string() const { return _n.str(); }

std::string interval_t::to_string() const {
    std::ostringstream s;
    s << *this;
    return s.str();
}

std::ostream& operator<<(std::ostream& os, const label_t& label) {
    if (label == label_t::entry) {
        return os << "entry";
    }
    if (label == label_t::exit) {
        return os << "exit";
    }
    if (!label.stack_frame_prefix.empty()) {
        os << label.stack_frame_prefix << STACK_FRAME_DELIMITER;
    }
    os << label.from;
    if (label.to != -1) {
        os << ":" << label.to;
    }
    if (!label.special_label.empty()) {
        os << " (" << label.special_label << ")";
    }
    return os;
}

string to_string(label_t const& label) {
    std::stringstream str;
    str << label;
    return str.str();
}

} // namespace crab

struct LineInfoPrinter {
    std::ostream& os;
    std::string previous_source_line;

    void print_line_info(const label_t& label) {
        if (thread_local_options.verbosity_opts.print_line_info) {
            const auto& line_info_map = thread_local_program_info.get().line_info;
            const auto& line_info = line_info_map.find(label.from);
            // Print line info only once.
            if (line_info != line_info_map.end() && line_info->second.source_line != previous_source_line) {
                os << "\n" << line_info->second << "\n";
                previous_source_line = line_info->second.source_line;
            }
        }
    }
};

void print_jump(std::ostream& o, const std::string& direction, const std::set<label_t>& labels) {
    auto [it, et] = std::pair{labels.begin(), labels.end()};
    if (it != et) {
        o << "  " << direction << " ";
        while (it != et) {
            o << *it;
            ++it;
            if (it == et) {
                o << ";";
            } else {
                o << ",";
            }
        }
    }
    o << "\n";
}

void print_program(const Program& prog, std::ostream& os, const bool simplify, const printfunc& prefunc,
                   const printfunc& postfunc) {
    LineInfoPrinter printer{os};
    for (const crab::basic_block_t& bb : crab::basic_block_t::collect_basic_blocks(prog.cfg(), simplify)) {
        prefunc(os, bb.first_label());
        print_jump(os, "from", prog.cfg().parents_of(bb.first_label()));
        os << bb.first_label() << ":\n";
        for (const label_t& label : bb) {
            printer.print_line_info(label);
            for (const auto& pre : prog.assertions_at(label)) {
                os << "  " << "assert " << pre << ";\n";
            }
            os << "  " << prog.instruction_at(label) << ";\n";
        }
        print_jump(os, "goto", prog.cfg().children_of(bb.last_label()));
        postfunc(os, bb.last_label());
    }
    os << "\n";
}

static void nop(std::ostream&, const label_t&) {}

void print_program(const Program& prog, std::ostream& os, const bool simplify) {
    print_program(prog, os, simplify, nop, nop);
}

void print_dot(const Program& prog, std::ostream& out) {
    out << "digraph program {\n";
    out << "    node [shape = rectangle];\n";
    for (const auto& label : prog.labels()) {
        out << "    \"" << label << "\"[xlabel=\"" << label << "\",label=\"";

        for (const auto& pre : prog.assertions_at(label)) {
            out << "assert " << pre << "\\l";
        }
        out << prog.instruction_at(label) << "\\l";

        out << "\"];\n";
        for (const label_t& next : prog.cfg().children_of(label)) {
            out << "    \"" << label << "\" -> \"" << next << "\";\n";
        }
        out << "\n";
    }
    out << "}\n";
}

void print_dot(const Program& prog, const std::string& outfile) {
    std::ofstream out{outfile};
    if (out.fail()) {
        throw std::runtime_error(std::string("Could not open file ") + outfile);
    }
    print_dot(prog, out);
}

void print_reachability(std::ostream& os, const Report& report) {
    for (const auto& [label, notes] : report.reachability) {
        for (const auto& msg : notes) {
            os << label << ": " << msg << "\n";
        }
    }
    os << "\n";
}

void print_warnings(std::ostream& os, const Report& report) {
    LineInfoPrinter printer{os};
    for (const auto& [label, warnings] : report.warnings) {
        for (const auto& msg : warnings) {
            printer.print_line_info(label);
            os << label << ": " << msg << "\n";
        }
    }
    os << "\n";
}

void print_all_messages(std::ostream& os, const Report& report) {
    print_reachability(os, report);
    print_warnings(os, report);
}

void print_invariants(std::ostream& os, const Program& prog, const bool simplify, const Invariants& invariants) {
    print_program(
        prog, os, simplify,
        [&](std::ostream& os, const label_t& label) -> void {
            os << "\nPre-invariant : " << invariants.invariants.at(label).pre << "\n";
        },
        [&](std::ostream& os, const label_t& label) -> void {
            os << "\nPost-invariant : " << invariants.invariants.at(label).post << "\n";
        });
}

namespace asm_syntax {
std::ostream& operator<<(std::ostream& os, const ArgSingle::Kind kind) {
    switch (kind) {
    case ArgSingle::Kind::ANYTHING: return os << "uint64_t";
    case ArgSingle::Kind::PTR_TO_CTX: return os << "ctx";
    case ArgSingle::Kind::MAP_FD: return os << "map_fd";
    case ArgSingle::Kind::MAP_FD_PROGRAMS: return os << "map_fd_programs";
    case ArgSingle::Kind::PTR_TO_MAP_KEY: return os << "map_key";
    case ArgSingle::Kind::PTR_TO_MAP_VALUE: return os << "map_value";
    }
    assert(false);
    return os;
}

std::ostream& operator<<(std::ostream& os, const ArgPair::Kind kind) {
    switch (kind) {
    case ArgPair::Kind::PTR_TO_READABLE_MEM: return os << "mem";
    case ArgPair::Kind::PTR_TO_READABLE_MEM_OR_NULL: return os << "mem?";
    case ArgPair::Kind::PTR_TO_WRITABLE_MEM: return os << "out";
    }
    assert(false);
    return os;
}

std::ostream& operator<<(std::ostream& os, const ArgSingle arg) {
    os << arg.kind << " " << arg.reg;
    return os;
}

std::ostream& operator<<(std::ostream& os, const ArgPair arg) {
    os << arg.kind << " " << arg.mem << "[" << arg.size;
    if (arg.can_be_zero) {
        os << "?";
    }
    os << "], uint64_t " << arg.size;
    return os;
}

std::ostream& operator<<(std::ostream& os, const Bin::Op op) {
    using Op = Bin::Op;
    switch (op) {
    case Op::MOV: return os;
    case Op::MOVSX8: return os << "s8";
    case Op::MOVSX16: return os << "s16";
    case Op::MOVSX32: return os << "s32";
    case Op::ADD: return os << "+";
    case Op::SUB: return os << "-";
    case Op::MUL: return os << "*";
    case Op::UDIV: return os << "/";
    case Op::SDIV: return os << "s/";
    case Op::UMOD: return os << "%";
    case Op::SMOD: return os << "s%";
    case Op::OR: return os << "|";
    case Op::AND: return os << "&";
    case Op::LSH: return os << "<<";
    case Op::RSH: return os << ">>";
    case Op::ARSH: return os << ">>>";
    case Op::XOR: return os << "^";
    }
    assert(false);
    return os;
}

std::ostream& operator<<(std::ostream& os, const Condition::Op op) {
    using Op = Condition::Op;
    switch (op) {
    case Op::EQ: return os << "==";
    case Op::NE: return os << "!=";
    case Op::SET: return os << "&==";
    case Op::NSET: return os << "&!="; // not in ebpf
    case Op::LT: return os << "<";     // TODO: os << "u<";
    case Op::LE: return os << "<=";    // TODO: os << "u<=";
    case Op::GT: return os << ">";     // TODO: os << "u>";
    case Op::GE: return os << ">=";    // TODO: os << "u>=";
    case Op::SLT: return os << "s<";
    case Op::SLE: return os << "s<=";
    case Op::SGT: return os << "s>";
    case Op::SGE: return os << "s>=";
    }
    assert(false);
    return os;
}

static string size(const int w) { return string("u") + std::to_string(w * 8); }

// ReSharper disable CppMemberFunctionMayBeConst
struct AssertionPrinterVisitor {
    std::ostream& _os;

    void operator()(ValidStore const& a) {
        _os << a.mem << ".type != stack -> " << TypeConstraint{a.val, TypeGroup::number};
    }

    void operator()(ValidAccess const& a) {
        if (a.or_null) {
            _os << "(" << TypeConstraint{a.reg, TypeGroup::number} << " and " << a.reg << ".value == 0) or ";
        }
        _os << "valid_access(" << a.reg << ".offset";
        if (a.offset > 0) {
            _os << "+" << a.offset;
        } else if (a.offset < 0) {
            _os << a.offset;
        }

        if (a.width == Value{Imm{0}}) {
            // a.width == 0, meaning we only care it's an in-bound pointer,
            // so it can be compared with another pointer to the same region.
            _os << ") for comparison/subtraction";
        } else {
            _os << ", width=" << a.width << ") for ";
            if (a.access_type == AccessType::read) {
                _os << "read";
            } else {
                _os << "write";
            }
        }
    }

    void operator()(const BoundedLoopCount& a) {
        _os << crab::variable_t::loop_counter(to_string(a.name)) << " < " << a.limit;
    }

    static crab::variable_t typereg(const Reg& r) { return crab::variable_t::reg(crab::data_kind_t::types, r.v); }

    void operator()(ValidSize const& a) {
        const auto op = a.can_be_zero ? " >= " : " > ";
        _os << a.reg << ".value" << op << 0;
    }

    void operator()(ValidCall const& a) {
        const EbpfHelperPrototype proto = thread_local_program_info->platform->get_helper_prototype(a.func);
        _os << "valid call(" << proto.name << ")";
    }

    void operator()(ValidMapKeyValue const& a) {
        _os << "within stack(" << a.access_reg << ":" << (a.key ? "key_size" : "value_size") << "(" << a.map_fd_reg
            << "))";
    }

    void operator()(ZeroCtxOffset const& a) {
        _os << crab::variable_t::reg(crab::data_kind_t::ctx_offsets, a.reg.v) << " == 0";
    }

    void operator()(Comparable const& a) {
        if (a.or_r2_is_number) {
            _os << TypeConstraint{a.r2, TypeGroup::number} << " or ";
        }
        _os << typereg(a.r1) << " == " << typereg(a.r2) << " in " << TypeGroup::singleton_ptr;
    }

    void operator()(Addable const& a) {
        _os << TypeConstraint{a.ptr, TypeGroup::pointer} << " -> " << TypeConstraint{a.num, TypeGroup::number};
    }

    void operator()(ValidDivisor const& a) { _os << a.reg << " != 0"; }

    void operator()(TypeConstraint const& tc) {
        const string cmp_op = is_singleton_type(tc.types) ? "==" : "in";
        _os << typereg(tc.reg) << " " << cmp_op << " " << tc.types;
    }

    void operator()(FuncConstraint const& fc) { _os << typereg(fc.reg) << " is helper"; }
};

// ReSharper disable CppMemberFunctionMayBeConst
struct CommandPrinterVisitor {
    std::ostream& os_;

    void visit(const auto& item) { std::visit(*this, item); }

    void operator()(Undefined const& a) { os_ << "Undefined{" << a.opcode << "}"; }

    void operator()(LoadMapFd const& b) { os_ << b.dst << " = map_fd " << b.mapfd; }

    void operator()(LoadMapAddress const& b) { os_ << b.dst << " = map_val(" << b.mapfd << ") + " << b.offset; }

    // llvm-objdump uses "w<number>" for 32-bit operations and "r<number>" for 64-bit operations.
    // We use the same convention here for consistency.
    static std::string reg_name(Reg const& a, const bool is64) { return ((is64) ? "r" : "w") + std::to_string(a.v); }

    void operator()(Bin const& b) {
        os_ << reg_name(b.dst, b.is64) << " " << b.op << "= " << b.v;
        if (b.lddw) {
            os_ << " ll";
        }
    }

    void operator()(Un const& b) {
        os_ << b.dst << " = ";
        switch (b.op) {
        case Un::Op::BE16: os_ << "be16 "; break;
        case Un::Op::BE32: os_ << "be32 "; break;
        case Un::Op::BE64: os_ << "be64 "; break;
        case Un::Op::LE16: os_ << "le16 "; break;
        case Un::Op::LE32: os_ << "le32 "; break;
        case Un::Op::LE64: os_ << "le64 "; break;
        case Un::Op::SWAP16: os_ << "swap16 "; break;
        case Un::Op::SWAP32: os_ << "swap32 "; break;
        case Un::Op::SWAP64: os_ << "swap64 "; break;
        case Un::Op::NEG: os_ << "-"; break;
        }
        os_ << b.dst;
    }

    void operator()(Call const& call) {
        os_ << "r0 = " << call.name << ":" << call.func << "(";
        for (uint8_t r = 1; r <= 5; r++) {
            // Look for a singleton.
            auto single = std::ranges::find_if(call.singles, [r](const ArgSingle arg) { return arg.reg.v == r; });
            if (single != call.singles.end()) {
                if (r > 1) {
                    os_ << ", ";
                }
                os_ << *single;
                continue;
            }

            // Look for the start of a pair.
            auto pair = std::ranges::find_if(call.pairs, [r](const ArgPair arg) { return arg.mem.v == r; });
            if (pair != call.pairs.end()) {
                if (r > 1) {
                    os_ << ", ";
                }
                os_ << *pair;
                r++;
                continue;
            }

            // Not found.
            break;
        }
        os_ << ")";
    }

    void operator()(CallLocal const& call) { os_ << "call <" << to_string(call.target) << ">"; }

    void operator()(Callx const& callx) { os_ << "callx " << callx.func; }

    void operator()(Exit const& b) { os_ << "exit"; }

    void operator()(Jmp const& b) {
        // A "standalone" jump Instruction.
        // Print the label without offset calculations.
        if (b.cond) {
            os_ << "if ";
            print(*b.cond);
            os_ << " ";
        }
        os_ << "goto label <" << to_string(b.target) << ">";
    }

    void operator()(Jmp const& b, const int offset) {
        const string sign = offset > 0 ? "+" : "";
        const string target = sign + std::to_string(offset) + " <" + to_string(b.target) + ">";

        if (b.cond) {
            os_ << "if ";
            print(*b.cond);
            os_ << " ";
        }
        os_ << "goto " << target;
    }

    void operator()(Packet const& b) {
        /* Direct packet access, R0 = *(uint *) (skb->data + imm32) */
        /* Indirect packet access, R0 = *(uint *) (skb->data + src_reg + imm32) */
        const string s = size(b.width);
        os_ << "r0 = ";
        os_ << "*(" << s << " *)skb[";
        if (b.regoffset) {
            os_ << *b.regoffset;
        }
        if (b.offset != 0) {
            if (b.regoffset) {
                os_ << " + ";
            }
            os_ << b.offset;
        }
        os_ << "]";
    }

    void print(Deref const& access) {
        const string sign = access.offset < 0 ? " - " : " + ";
        int offset = std::abs(access.offset); // what about INT_MIN?
        os_ << "*(" << size(access.width) << " *)";
        os_ << "(" << access.basereg << sign << offset << ")";
    }

    void print(Condition const& cond) {
        os_ << cond.left << " " << ((!cond.is64) ? "w" : "") << cond.op << " " << cond.right;
    }

    void operator()(Mem const& b) {
        if (b.is_load) {
            os_ << b.value << " = ";
        }
        print(b.access);
        if (!b.is_load) {
            os_ << " = " << b.value;
        }
    }

    void operator()(Atomic const& b) {
        os_ << "lock ";
        print(b.access);
        os_ << " ";
        bool showfetch = true;
        switch (b.op) {
        case Atomic::Op::ADD: os_ << "+"; break;
        case Atomic::Op::OR: os_ << "|"; break;
        case Atomic::Op::AND: os_ << "&"; break;
        case Atomic::Op::XOR: os_ << "^"; break;
        case Atomic::Op::XCHG:
            os_ << "x";
            showfetch = false;
            break;
        case Atomic::Op::CMPXCHG:
            os_ << "cx";
            showfetch = false;
            break;
        }
        os_ << "= " << b.valreg;

        if (showfetch && b.fetch) {
            os_ << " fetch";
        }
    }

    void operator()(Assume const& b) {
        os_ << "assume ";
        print(b.cond);
    }

    void operator()(IncrementLoopCounter const& a) { os_ << crab::variable_t::loop_counter(to_string(a.name)) << "++"; }
};
// ReSharper restore CppMemberFunctionMayBeConst

std::ostream& operator<<(std::ostream& os, Instruction const& ins) {
    std::visit(CommandPrinterVisitor{os}, ins);
    return os;
}

string to_string(Instruction const& ins) {
    std::stringstream str;
    str << ins;
    return str.str();
}

std::ostream& operator<<(std::ostream& os, const Assertion& a) {
    std::visit(AssertionPrinterVisitor{os}, a);
    return os;
}

string to_string(Assertion const& constraint) {
    std::stringstream str;
    str << constraint;
    return str.str();
}

auto get_labels(const InstructionSeq& insts) {
    pc_t pc = 0;
    std::map<label_t, pc_t> pc_of_label;
    for (const auto& [label, inst, _] : insts) {
        pc_of_label[label] = pc;
        pc += size(inst);
    }
    return pc_of_label;
}

void print(const InstructionSeq& insts, std::ostream& out, const std::optional<const label_t>& label_to_print,
           const bool print_line_info) {
    const auto pc_of_label = get_labels(insts);
    pc_t pc = 0;
    std::string previous_source;
    CommandPrinterVisitor visitor{out};
    for (const LabeledInstruction& labeled_inst : insts) {
        const auto& [label, ins, line_info] = labeled_inst;
        if (!label_to_print.has_value() || label == label_to_print) {
            if (line_info.has_value() && print_line_info) {
                auto& [file, source, line, column] = line_info.value();
                // Only decorate the first instruction associated with a source line.
                if (source != previous_source) {
                    out << line_info.value();
                    previous_source = source;
                }
            }
            if (label.isjump()) {
                out << "\n";
                out << label << ":\n";
            }
            if (label_to_print.has_value()) {
                out << pc << ": ";
            } else {
                out << std::setw(8) << pc << ":\t";
            }
            if (const auto jmp = std::get_if<Jmp>(&ins)) {
                if (!pc_of_label.contains(jmp->target)) {
                    throw std::runtime_error(string("Cannot find label ") + crab::to_string(jmp->target));
                }
                const pc_t target_pc = pc_of_label.at(jmp->target);
                visitor(*jmp, target_pc - static_cast<int>(pc) - 1);
            } else {
                std::visit(visitor, ins);
            }
            out << "\n";
        }
        pc += size(ins);
    }
}

} // namespace asm_syntax

std::ostream& operator<<(std::ostream& o, const EbpfMapDescriptor& desc) {
    return o << "(" << "original_fd = " << desc.original_fd << ", " << "inner_map_fd = " << desc.inner_map_fd << ", "
             << "type = " << desc.type << ", " << "max_entries = " << desc.max_entries << ", "
             << "value_size = " << desc.value_size << ", " << "key_size = " << desc.key_size << ")";
}

void print_map_descriptors(const std::vector<EbpfMapDescriptor>& descriptors, std::ostream& o) {
    int i = 0;
    for (const auto& desc : descriptors) {
        o << "map " << i << ":" << desc << "\n";
        i++;
    }
}

std::ostream& operator<<(std::ostream& os, const btf_line_info_t& line_info) {
    os << "; " << line_info.file_name << ":" << line_info.line_number << "\n";
    os << "; " << line_info.source_line << "\n";
    return os;
}

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <fstream>
4	#include <iomanip>
5	#include <iostream>
6	#include <variant>
7	#include <vector>
8
9	#include "asm_syntax.hpp"
10	#include "crab/cfg.hpp"
11	#include "crab/fwd_analyzer.hpp"
12	#include "crab/interval.hpp"
13	#include "crab/type_encoding.hpp"
14	#include "crab/variable.hpp"
15	#include "crab_utils/num_big.hpp"
16	#include "crab_verifier.hpp"
17	#include "helpers.hpp"
18	#include "platform.hpp"
19	#include "spec_type_descriptors.hpp"
20
21	using crab::TypeGroup;
22	using std::optional;
23	using std::string;
24	using std::vector;
25
26	namespace crab {
27
28	std::string number_t::to_string() const { return _n.str(); }	×
29
30	std::string interval_t::to_string() const {	×
31	std::ostringstream s;	×
32	s << *this;	×
33	return s.str();	×
34	}	×
35
36	std::ostream& operator<<(std::ostream& os, const label_t& label) {	1,592✔
37	if (label == label_t::entry) {	1,592✔
38	return os << "entry";	6✔
39	}
40	if (label == label_t::exit) {	1,586✔
41	return os << "exit";	6✔
42	}
43	if (!label.stack_frame_prefix.empty()) {	1,580✔
44	os << label.stack_frame_prefix << STACK_FRAME_DELIMITER;	330✔
45	}
46	os << label.from;	1,580✔
47	if (label.to != -1) {	1,580✔
48	os << ":" << label.to;	50✔
49	}
50	if (!label.special_label.empty()) {	1,580✔
51	os << " (" << label.special_label << ")";	20✔
52	}
53	return os;	790✔
54	}
55
56	string to_string(label_t const& label) {	1,546✔
57	std::stringstream str;	1,546✔
58	str << label;	1,546✔
59	return str.str();	3,092✔
60	}	1,546✔
61
62	} // namespace crab
63
64	struct LineInfoPrinter {
65	std::ostream& os;
66	std::string previous_source_line;
67
68	void print_line_info(const label_t& label) {	×
69	if (thread_local_options.verbosity_opts.print_line_info) {	×
70	const auto& line_info_map = thread_local_program_info.get().line_info;	×
71	const auto& line_info = line_info_map.find(label.from);	×
72	// Print line info only once.
73	if (line_info != line_info_map.end() && line_info->second.source_line != previous_source_line) {	×
74	os << "\n" << line_info->second << "\n";	×
75	previous_source_line = line_info->second.source_line;	×
76	}
77	}
78	}	×
79	};
80
81	void print_jump(std::ostream& o, const std::string& direction, const std::set<label_t>& labels) {	×
82	auto [it, et] = std::pair{labels.begin(), labels.end()};	×
83	if (it != et) {	×
84	o << " " << direction << " ";	×
85	while (it != et) {	×
86	o << *it;	×
87	++it;	×
88	if (it == et) {	×
89	o << ";";	×
90	} else {
91	o << ",";	×
92	}
93	}
94	}
95	o << "\n";	×
96	}	×
97
98	void print_program(const Program& prog, std::ostream& os, const bool simplify, const printfunc& prefunc,	×
99	const printfunc& postfunc) {
100	LineInfoPrinter printer{os};	×
101	for (const crab::basic_block_t& bb : crab::basic_block_t::collect_basic_blocks(prog.cfg(), simplify)) {	×
102	prefunc(os, bb.first_label());	×
103	print_jump(os, "from", prog.cfg().parents_of(bb.first_label()));	×
104	os << bb.first_label() << ":\n";	×
105	for (const label_t& label : bb) {	×
106	printer.print_line_info(label);	×
107	for (const auto& pre : prog.assertions_at(label)) {	×
108	os << " " << "assert " << pre << ";\n";	×
109	}	×
110	os << " " << prog.instruction_at(label) << ";\n";	×
111	}
112	print_jump(os, "goto", prog.cfg().children_of(bb.last_label()));	×
113	postfunc(os, bb.last_label());	×
114	}	×
115	os << "\n";	×
116	}	×
117
118	static void nop(std::ostream&, const label_t&) {}	×
119
120	void print_program(const Program& prog, std::ostream& os, const bool simplify) {	×
121	print_program(prog, os, simplify, nop, nop);	×
122	}	×
123
124	void print_dot(const Program& prog, std::ostream& out) {	×
125	out << "digraph program {\n";	×
126	out << " node [shape = rectangle];\n";	×
127	for (const auto& label : prog.labels()) {	×
128	out << " \"" << label << "\"[xlabel=\"" << label << "\",label=\"";	×
129
130	for (const auto& pre : prog.assertions_at(label)) {	×
131	out << "assert " << pre << "\\l";	×
132	}	×
133	out << prog.instruction_at(label) << "\\l";	×
134
135	out << "\"];\n";	×
136	for (const label_t& next : prog.cfg().children_of(label)) {	×
137	out << " \"" << label << "\" -> \"" << next << "\";\n";	×
138	}
139	out << "\n";	×
140	}
141	out << "}\n";	×
142	}	×
143
144	void print_dot(const Program& prog, const std::string& outfile) {	×
145	std::ofstream out{outfile};	×
146	if (out.fail()) {	×
147	throw std::runtime_error(std::string("Could not open file ") + outfile);	×
148	}
149	print_dot(prog, out);	×
150	}	×
151
152	void print_reachability(std::ostream& os, const Report& report) {	×
153	for (const auto& [label, notes] : report.reachability) {	×
154	for (const auto& msg : notes) {	×
155	os << label << ": " << msg << "\n";	×
156	}
157	}
158	os << "\n";	×
159	}	×
160
161	void print_warnings(std::ostream& os, const Report& report) {	×
162	LineInfoPrinter printer{os};	×
163	for (const auto& [label, warnings] : report.warnings) {	×
164	for (const auto& msg : warnings) {	×
165	printer.print_line_info(label);	×
166	os << label << ": " << msg << "\n";	×
167	}
168	}
169	os << "\n";	×
170	}	×
171
172	void print_all_messages(std::ostream& os, const Report& report) {	×
173	print_reachability(os, report);	×
174	print_warnings(os, report);	×
175	}	×
176
177	void print_invariants(std::ostream& os, const Program& prog, const bool simplify, const Invariants& invariants) {	×
178	print_program(	×
179	prog, os, simplify,
180	[&](std::ostream& os, const label_t& label) -> void {	×
181	os << "\nPre-invariant : " << invariants.invariants.at(label).pre << "\n";	×
182	},	×
183	[&](std::ostream& os, const label_t& label) -> void {	×
184	os << "\nPost-invariant : " << invariants.invariants.at(label).post << "\n";	×
185	});	×
186	}	×
187
188	namespace asm_syntax {
189	std::ostream& operator<<(std::ostream& os, const ArgSingle::Kind kind) {	74✔
190	switch (kind) {	74✔
191	case ArgSingle::Kind::ANYTHING: return os << "uint64_t";	14✔
192	case ArgSingle::Kind::PTR_TO_CTX: return os << "ctx";	4✔
193	case ArgSingle::Kind::MAP_FD: return os << "map_fd";	24✔
194	case ArgSingle::Kind::MAP_FD_PROGRAMS: return os << "map_fd_programs";	×
195	case ArgSingle::Kind::PTR_TO_MAP_KEY: return os << "map_key";	24✔
196	case ArgSingle::Kind::PTR_TO_MAP_VALUE: return os << "map_value";	8✔
197	}
198	assert(false);
199	return os;
200	}
201
202	std::ostream& operator<<(std::ostream& os, const ArgPair::Kind kind) {	×
203	switch (kind) {	×
204	case ArgPair::Kind::PTR_TO_READABLE_MEM: return os << "mem";	×
205	case ArgPair::Kind::PTR_TO_READABLE_MEM_OR_NULL: return os << "mem?";	×
206	case ArgPair::Kind::PTR_TO_WRITABLE_MEM: return os << "out";	×
207	}
208	assert(false);
209	return os;
210	}
211
212	std::ostream& operator<<(std::ostream& os, const ArgSingle arg) {	74✔
213	os << arg.kind << " " << arg.reg;	74✔
214	return os;	74✔
215	}
216
217	std::ostream& operator<<(std::ostream& os, const ArgPair arg) {	×
218	os << arg.kind << " " << arg.mem << "[" << arg.size;	×
219	if (arg.can_be_zero) {	×
220	os << "?";	×
221	}
222	os << "], uint64_t " << arg.size;	×
223	return os;	×
224	}
225
226	std::ostream& operator<<(std::ostream& os, const Bin::Op op) {	314✔
227	using Op = Bin::Op;	157✔
228	switch (op) {	314✔
229	case Op::MOV: return os;	81✔
230	case Op::MOVSX8: return os << "s8";	×
231	case Op::MOVSX16: return os << "s16";	×
232	case Op::MOVSX32: return os << "s32";	28✔
233	case Op::ADD: return os << "+";	78✔
234	case Op::SUB: return os << "-";	×
235	case Op::MUL: return os << "*";	×
236	case Op::UDIV: return os << "/";	×
237	case Op::SDIV: return os << "s/";	×
238	case Op::UMOD: return os << "%";	×
239	case Op::SMOD: return os << "s%";	×
240	case Op::OR: return os << "\|";	×
241	case Op::AND: return os << "&";	30✔
242	case Op::LSH: return os << "<<";	12✔
243	case Op::RSH: return os << ">>";	×
244	case Op::ARSH: return os << ">>>";	2✔
245	case Op::XOR: return os << "^";	2✔
246	}
247	assert(false);
248	return os;
249	}
250
251	std::ostream& operator<<(std::ostream& os, const Condition::Op op) {	232✔
252	using Op = Condition::Op;	116✔
253	switch (op) {	232✔
254	case Op::EQ: return os << "==";	38✔
255	case Op::NE: return os << "!=";	12✔
256	case Op::SET: return os << "&==";	×
257	case Op::NSET: return os << "&!="; // not in ebpf	×
258	case Op::LT: return os << "<"; // TODO: os << "u<";	132✔
259	case Op::LE: return os << "<="; // TODO: os << "u<=";	12✔
260	case Op::GT: return os << ">"; // TODO: os << "u>";	22✔
261	case Op::GE: return os << ">="; // TODO: os << "u>=";	6✔
262	case Op::SLT: return os << "s<";	4✔
263	case Op::SLE: return os << "s<=";	×
264	case Op::SGT: return os << "s>";	4✔
265	case Op::SGE: return os << "s>=";	2✔
266	}
267	assert(false);
268	return os;
269	}
270
271	static string size(const int w) { return string("u") + std::to_string(w * 8); }	460✔
272
273	// ReSharper disable CppMemberFunctionMayBeConst
274	struct AssertionPrinterVisitor {
275	std::ostream& _os;
276
277	void operator()(ValidStore const& a) {	2✔
278	_os << a.mem << ".type != stack -> " << TypeConstraint{a.val, TypeGroup::number};	2✔
279	}	2✔
280
281	void operator()(ValidAccess const& a) {	40,238✔
282	if (a.or_null) {	40,238✔
283	_os << "(" << TypeConstraint{a.reg, TypeGroup::number} << " and " << a.reg << ".value == 0) or ";	2,968✔
284	}
285	_os << "valid_access(" << a.reg << ".offset";	40,238✔
286	if (a.offset > 0) {	40,238✔
287	_os << "+" << a.offset;	25,394✔
288	} else if (a.offset < 0) {	14,844✔
289	_os << a.offset;	100✔
290	}
291
292	if (a.width == Value{Imm{0}}) {	40,238✔
293	// a.width == 0, meaning we only care it's an in-bound pointer,
294	// so it can be compared with another pointer to the same region.
295	_os << ") for comparison/subtraction";	3,472✔
296	} else {
297	_os << ", width=" << a.width << ") for ";	36,766✔
298	if (a.access_type == AccessType::read) {	36,766✔
299	_os << "read";	26,896✔
300	} else {
301	_os << "write";	9,870✔
302	}
303	}
304	}	40,238✔
305
306	void operator()(const BoundedLoopCount& a) {	32✔
307	_os << crab::variable_t::loop_counter(to_string(a.name)) << " < " << a.limit;	32✔
308	}	32✔
309
310	static crab::variable_t typereg(const Reg& r) { return crab::variable_t::reg(crab::data_kind_t::types, r.v); }	5,630✔
311
312	void operator()(ValidSize const& a) {	3,508✔
313	const auto op = a.can_be_zero ? " >= " : " > ";	3,508✔
314	_os << a.reg << ".value" << op << 0;	3,508✔
315	}	3,508✔
316
317	void operator()(ValidCall const& a) {	2✔
318	const EbpfHelperPrototype proto = thread_local_program_info->platform->get_helper_prototype(a.func);	2✔
319	_os << "valid call(" << proto.name << ")";	2✔
320	}	2✔
321
322	void operator()(ValidMapKeyValue const& a) {	142✔
323	_os << "within stack(" << a.access_reg << ":" << (a.key ? "key_size" : "value_size") << "(" << a.map_fd_reg	178✔
324	<< "))";	142✔
325	}	142✔
326
327	void operator()(ZeroCtxOffset const& a) {	4,204✔
328	_os << crab::variable_t::reg(crab::data_kind_t::ctx_offsets, a.reg.v) << " == 0";	4,204✔
329	}	4,204✔
330
331	void operator()(Comparable const& a) {	1,852✔
332	if (a.or_r2_is_number) {	1,852✔
333	_os << TypeConstraint{a.r2, TypeGroup::number} << " or ";	306✔
334	}
335	_os << typereg(a.r1) << " == " << typereg(a.r2) << " in " << TypeGroup::singleton_ptr;	1,852✔
336	}	1,852✔
337
338	void operator()(Addable const& a) {	4✔
339	_os << TypeConstraint{a.ptr, TypeGroup::pointer} << " -> " << TypeConstraint{a.num, TypeGroup::number};	8✔
340	}	4✔
341
342	void operator()(ValidDivisor const& a) { _os << a.reg << " != 0"; }	76✔
343
344	void operator()(TypeConstraint const& tc) {	1,920✔
345	const string cmp_op = is_singleton_type(tc.types) ? "==" : "in";	1,946✔
346	_os << typereg(tc.reg) << " " << cmp_op << " " << tc.types;	1,920✔
347	}	1,920✔
348
349	void operator()(FuncConstraint const& fc) { _os << typereg(fc.reg) << " is helper"; }	6✔
350	};
351
352	// ReSharper disable CppMemberFunctionMayBeConst
353	struct CommandPrinterVisitor {
354	std::ostream& os_;
355
356	void visit(const auto& item) { std::visit(*this, item); }
357
358	void operator()(Undefined const& a) { os_ << "Undefined{" << a.opcode << "}"; }	×
359
360	void operator()(LoadMapFd const& b) { os_ << b.dst << " = map_fd " << b.mapfd; }	24✔
361
NEW 362	void operator()(LoadMapAddress const& b) { os_ << b.dst << " = map_val(" << b.mapfd << ") + " << b.offset; }	×
363
364	// llvm-objdump uses "w<number>" for 32-bit operations and "r<number>" for 64-bit operations.
365	// We use the same convention here for consistency.
366	static std::string reg_name(Reg const& a, const bool is64) { return ((is64) ? "r" : "w") + std::to_string(a.v); }	475✔
367
368	void operator()(Bin const& b) {	314✔
369	os_ << reg_name(b.dst, b.is64) << " " << b.op << "= " << b.v;	471✔
370	if (b.lddw) {	314✔
371	os_ << " ll";	2✔
372	}
373	}	314✔
374
375	void operator()(Un const& b) {	12✔
376	os_ << b.dst << " = ";	12✔
377	switch (b.op) {	12✔
378	case Un::Op::BE16: os_ << "be16 "; break;	2✔
379	case Un::Op::BE32: os_ << "be32 "; break;	2✔
380	case Un::Op::BE64: os_ << "be64 "; break;	2✔
381	case Un::Op::LE16: os_ << "le16 "; break;	2✔
382	case Un::Op::LE32: os_ << "le32 "; break;	2✔
383	case Un::Op::LE64: os_ << "le64 "; break;	2✔
384	case Un::Op::SWAP16: os_ << "swap16 "; break;	×
385	case Un::Op::SWAP32: os_ << "swap32 "; break;	×
386	case Un::Op::SWAP64: os_ << "swap64 "; break;	×
387	case Un::Op::NEG: os_ << "-"; break;	×
388	}
389	os_ << b.dst;	12✔
390	}	12✔
391
392	void operator()(Call const& call) {	70✔
393	os_ << "r0 = " << call.name << ":" << call.func << "(";	70✔
394	for (uint8_t r = 1; r <= 5; r++) {	144✔
395	// Look for a singleton.
396	auto single = std::ranges::find_if(call.singles, [r](const ArgSingle arg) { return arg.reg.v == r; });	372✔
397	if (single != call.singles.end()) {	144✔
398	if (r > 1) {	74✔
399	os_ << ", ";	48✔
400	}
401	os_ << *single;	74✔
402	continue;	74✔
403	}
404
405	// Look for the start of a pair.
406	auto pair = std::ranges::find_if(call.pairs, [r](const ArgPair arg) { return arg.mem.v == r; });	70✔
407	if (pair != call.pairs.end()) {	70✔
408	if (r > 1) {	×
409	os_ << ", ";	×
410	}
411	os_ << *pair;	×
412	r++;	×
413	continue;	×
414	}
415
416	// Not found.
417	break;	70✔
418	}
419	os_ << ")";	70✔
420	}	70✔
421
422	void operator()(CallLocal const& call) { os_ << "call <" << to_string(call.target) << ">"; }	×
423
424	void operator()(Callx const& callx) { os_ << "callx " << callx.func; }	×
425
426	void operator()(Exit const& b) { os_ << "exit"; }	50✔
427
428	void operator()(Jmp const& b) {	×
429	// A "standalone" jump Instruction.
430	// Print the label without offset calculations.
431	if (b.cond) {	×
432	os_ << "if ";	×
433	print(*b.cond);	×
434	os_ << " ";	×
435	}
436	os_ << "goto label <" << to_string(b.target) << ">";	×
437	}	×
438
439	void operator()(Jmp const& b, const int offset) {	54✔
440	const string sign = offset > 0 ? "+" : "";	54✔
441	const string target = sign + std::to_string(offset) + " <" + to_string(b.target) + ">";	108✔
442
443	if (b.cond) {	54✔
444	os_ << "if ";	40✔
445	print(*b.cond);	40✔
446	os_ << " ";	40✔
447	}
448	os_ << "goto " << target;	54✔
449	}	54✔
450
451	void operator()(Packet const& b) {	×
452	/* Direct packet access, R0 = (uint ) (skb->data + imm32) */
453	/* Indirect packet access, R0 = (uint ) (skb->data + src_reg + imm32) */
454	const string s = size(b.width);	×
455	os_ << "r0 = ";	×
456	os_ << "(" << s << " )skb[";	×
457	if (b.regoffset) {	×
458	os_ << *b.regoffset;	×
459	}
460	if (b.offset != 0) {	×
461	if (b.regoffset) {	×
462	os_ << " + ";	×
463	}
464	os_ << b.offset;	×
465	}
466	os_ << "]";	×
467	}	×
468
469	void print(Deref const& access) {	184✔
470	const string sign = access.offset < 0 ? " - " : " + ";	212✔
471	int offset = std::abs(access.offset); // what about INT_MIN?	184✔
472	os_ << "(" << size(access.width) << " )";	276✔
473	os_ << "(" << access.basereg << sign << offset << ")";	184✔
474	}	184✔
475
476	void print(Condition const& cond) {	232✔
477	os_ << cond.left << " " << ((!cond.is64) ? "w" : "") << cond.op << " " << cond.right;	273✔
478	}	232✔
479
480	void operator()(Mem const& b) {	184✔
481	if (b.is_load) {	184✔
482	os_ << b.value << " = ";	44✔
483	}
484	print(b.access);	184✔
485	if (!b.is_load) {	184✔
486	os_ << " = " << b.value;	140✔
487	}
488	}	184✔
489
490	void operator()(Atomic const& b) {	×
491	os_ << "lock ";	×
492	print(b.access);	×
493	os_ << " ";	×
494	bool showfetch = true;	×
495	switch (b.op) {	×
496	case Atomic::Op::ADD: os_ << "+"; break;	×
497	case Atomic::Op::OR: os_ << "\|"; break;	×
498	case Atomic::Op::AND: os_ << "&"; break;	×
499	case Atomic::Op::XOR: os_ << "^"; break;	×
500	case Atomic::Op::XCHG:	×
501	os_ << "x";	×
502	showfetch = false;	×
503	break;	×
504	case Atomic::Op::CMPXCHG:	×
505	os_ << "cx";	×
506	showfetch = false;	×
507	break;	×
508	}
509	os_ << "= " << b.valreg;	×
510
511	if (showfetch && b.fetch) {	×
512	os_ << " fetch";	×
513	}
514	}	×
515
516	void operator()(Assume const& b) {	192✔
517	os_ << "assume ";	192✔
518	print(b.cond);	192✔
519	}	192✔
520
521	void operator()(IncrementLoopCounter const& a) { os_ << crab::variable_t::loop_counter(to_string(a.name)) << "++"; }	×
522	};
523	// ReSharper restore CppMemberFunctionMayBeConst
524
525	std::ostream& operator<<(std::ostream& os, Instruction const& ins) {	230✔
526	std::visit(CommandPrinterVisitor{os}, ins);	133✔
527	return os;	115✔
528	}
529
530	string to_string(Instruction const& ins) {	194✔
531	std::stringstream str;	194✔
532	str << ins;	194✔
533	return str.str();	388✔
534	}	194✔
535
536	std::ostream& operator<<(std::ostream& os, const Assertion& a) {	51,986✔
537	std::visit(AssertionPrinterVisitor{os}, a);	26,842✔
538	return os;	26,842✔
539	}
540
541	string to_string(Assertion const& constraint) {	50,288✔
542	std::stringstream str;	50,288✔
543	str << constraint;	50,288✔
544	return str.str();	100,576✔
545	}	50,288✔
546
547	auto get_labels(const InstructionSeq& insts) {	38✔
548	pc_t pc = 0;	38✔
549	std::map<label_t, pc_t> pc_of_label;	38✔
550	for (const auto& [label, inst, _] : insts) {	708✔
551	pc_of_label[label] = pc;	670✔
552	pc += size(inst);	670✔
553	}
554	return pc_of_label;	38✔
555	}	×
556
557	void print(const InstructionSeq& insts, std::ostream& out, const std::optional<const label_t>& label_to_print,	38✔
558	const bool print_line_info) {
559	const auto pc_of_label = get_labels(insts);	38✔
560	pc_t pc = 0;	38✔
561	std::string previous_source;	38✔
562	CommandPrinterVisitor visitor{out};	38✔
563	for (const LabeledInstruction& labeled_inst : insts) {	708✔
564	const auto& [label, ins, line_info] = labeled_inst;	670✔
565	if (!label_to_print.has_value() \|\| label == label_to_print) {	670✔
566	if (line_info.has_value() && print_line_info) {	670✔
567	auto& [file, source, line, column] = line_info.value();	×
568	// Only decorate the first instruction associated with a source line.
569	if (source != previous_source) {	×
570	out << line_info.value();	×
571	previous_source = source;	×
572	}
573	}
574	if (label.isjump()) {	670✔
575	out << "\n";	×
576	out << label << ":\n";	×
577	}
578	if (label_to_print.has_value()) {	670✔
579	out << pc << ": ";	×
580	} else {
581	out << std::setw(8) << pc << ":\t";	670✔
582	}
583	if (const auto jmp = std::get_if<Jmp>(&ins)) {	670✔
584	if (!pc_of_label.contains(jmp->target)) {	54✔
585	throw std::runtime_error(string("Cannot find label ") + crab::to_string(jmp->target));	×
586	}
587	const pc_t target_pc = pc_of_label.at(jmp->target);	54✔
588	visitor(*jmp, target_pc - static_cast<int>(pc) - 1);	54✔
589	} else {
590	std::visit(visitor, ins);	616✔
591	}
592	out << "\n";	670✔
593	}
594	pc += size(ins);	670✔
595	}
596	}	38✔
597
598	} // namespace asm_syntax
599
600	std::ostream& operator<<(std::ostream& o, const EbpfMapDescriptor& desc) {	28✔
601	return o << "(" << "original_fd = " << desc.original_fd << ", " << "inner_map_fd = " << desc.inner_map_fd << ", "	28✔
602	<< "type = " << desc.type << ", " << "max_entries = " << desc.max_entries << ", "	28✔
603	<< "value_size = " << desc.value_size << ", " << "key_size = " << desc.key_size << ")";	28✔
604	}
605
606	void print_map_descriptors(const std::vector<EbpfMapDescriptor>& descriptors, std::ostream& o) {	38✔
607	int i = 0;	38✔
608	for (const auto& desc : descriptors) {	66✔
609	o << "map " << i << ":" << desc << "\n";	28✔
610	i++;	28✔
611	}
612	}	38✔
613
614	std::ostream& operator<<(std::ostream& os, const btf_line_info_t& line_info) {	×
615	os << "; " << line_info.file_name << ":" << line_info.line_number << "\n";	×
616	os << "; " << line_info.source_line << "\n";	×
617	return os;	×
618	}

vbpf / ebpf-verifier / 12951530094

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