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

64.66

/src/asm_cfg.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#include <algorithm>
#include <cassert>
#include <map>
#include <optional>
#include <string>
#include <vector>

#include "config.hpp"
#include "crab/cfg.hpp"
#include "crab/wto.hpp"

#include "asm_syntax.hpp"
#include "program.hpp"

using std::optional;
using std::set;
using std::string;
using std::to_string;
using std::vector;

struct cfg_builder_t final {
    Program prog;

    // TODO: ins should be inserted elsewhere
    void insert_after(const label_t& prev_label, const label_t& new_label, const Instruction& ins) {
        if (prev_label == new_label) {
            CRAB_ERROR("Cannot insert after the same label ", to_string(new_label));
        }
        std::set<label_t> prev_children;
        std::swap(prev_children, prog.m_cfg.get_node(prev_label).children);

        for (const label_t& next_label : prev_children) {
            prog.m_cfg.get_node(next_label).parents.erase(prev_label);
        }

        insert(new_label, ins);
        for (const label_t& next_label : prev_children) {
            add_child(prev_label, new_label);
            add_child(new_label, next_label);
        }
    }

    // TODO: ins should be inserted elsewhere
    void insert(const label_t& _label, const Instruction& ins) {
        if (const auto it = prog.m_cfg.neighbours.find(_label); it != prog.m_cfg.neighbours.end()) {
            CRAB_ERROR("Label ", to_string(_label), " already exists");
        }
        prog.m_cfg.neighbours.emplace(_label, crab::cfg_t::adjacent_t{});
        prog.m_instructions.emplace(_label, ins);
    }

    // TODO: ins should be inserted elsewhere
    label_t insert_jump(const label_t& from, const label_t& to, const Instruction& ins) {
        const label_t jump_label = label_t::make_jump(from, to);
        if (prog.m_cfg.contains(jump_label)) {
            CRAB_ERROR("Jump label ", to_string(jump_label), " already exists");
        }
        insert(jump_label, ins);
        add_child(from, jump_label);
        add_child(jump_label, to);
        return jump_label;
    }

    void add_child(const label_t& a, const label_t& b) {
        assert(b != label_t::entry);
        assert(a != label_t::exit);
        prog.m_cfg.neighbours.at(a).children.insert(b);
        prog.m_cfg.neighbours.at(b).parents.insert(a);
    }

    void remove_child(const label_t& a, const label_t& b) {
        prog.m_cfg.get_node(a).children.erase(b);
        prog.m_cfg.get_node(b).parents.erase(a);
    }

    void set_assertions(const label_t& label, const std::vector<Assertion>& assertions) {
        if (!prog.m_cfg.contains(label)) {
            CRAB_ERROR("Label ", to_string(label), " not found in the CFG: ");
        }
        prog.m_assertions.insert_or_assign(label, assertions);
    }
};

using crab::basic_block_t;

/// Get the inverse of a given comparison operation.
static Condition::Op reverse(const Condition::Op op) {
    switch (op) {
    case Condition::Op::EQ: return Condition::Op::NE;
    case Condition::Op::NE: return Condition::Op::EQ;

    case Condition::Op::GE: return Condition::Op::LT;
    case Condition::Op::LT: return Condition::Op::GE;

    case Condition::Op::SGE: return Condition::Op::SLT;
    case Condition::Op::SLT: return Condition::Op::SGE;

    case Condition::Op::LE: return Condition::Op::GT;
    case Condition::Op::GT: return Condition::Op::LE;

    case Condition::Op::SLE: return Condition::Op::SGT;
    case Condition::Op::SGT: return Condition::Op::SLE;

    case Condition::Op::SET: return Condition::Op::NSET;
    case Condition::Op::NSET: return Condition::Op::SET;
    }
    assert(false);
    return {};
}

/// Get the inverse of a given comparison condition.
static Condition reverse(const Condition& cond) {
    return {.op = reverse(cond.op), .left = cond.left, .right = cond.right, .is64 = cond.is64};
}

static bool has_fall(const Instruction& ins) {
    if (std::holds_alternative<Exit>(ins)) {
        return false;
    }

    if (const auto pins = std::get_if<Jmp>(&ins)) {
        if (!pins->cond) {
            return false;
        }
    }

    return true;
}

/// Update a control-flow graph to inline function macros.
static void add_cfg_nodes(cfg_builder_t& builder, const label_t& caller_label, const label_t& entry_label) {
    bool first = true;

    // Get the label of the node to go to on returning from the macro.
    label_t exit_to_label = builder.prog.cfg().get_child(caller_label);

    // Construct the variable prefix to use for the new stack frame,
    // and store a copy in the CallLocal instruction since the instruction-specific
    // labels may only exist until the CFG is simplified.
    const std::string stack_frame_prefix = to_string(caller_label);
    if (const auto pcall = std::get_if<CallLocal>(&builder.prog.instruction_at(caller_label))) {
        pcall->stack_frame_prefix = stack_frame_prefix;
    }

    // Walk the transitive closure of CFG nodes starting at entry_label and ending at
    // any exit instruction.
    std::set macro_labels{entry_label};
    std::set seen_labels{entry_label};
    while (!macro_labels.empty()) {
        label_t macro_label = *macro_labels.begin();
        macro_labels.erase(macro_label);

        if (stack_frame_prefix == macro_label.stack_frame_prefix) {
            throw InvalidControlFlow{stack_frame_prefix + ": illegal recursion"};
        }

        // Clone the macro block into a new block with the new stack frame prefix.
        const label_t label{macro_label.from, macro_label.to, stack_frame_prefix};
        auto inst = builder.prog.instruction_at(macro_label);
        if (const auto pexit = std::get_if<Exit>(&inst)) {
            pexit->stack_frame_prefix = label.stack_frame_prefix;
        } else if (const auto pcall = std::get_if<Call>(&inst)) {
            pcall->stack_frame_prefix = label.stack_frame_prefix;
        }
        builder.insert(label, inst);

        if (first) {
            // Add an edge from the caller to the new block.
            first = false;
            builder.add_child(caller_label, label);
        }

        // Add an edge from any other predecessors.
        for (const auto& prev_macro_nodes = builder.prog.cfg().parents_of(macro_label);
             const auto& prev_macro_label : prev_macro_nodes) {
            const label_t prev_label(prev_macro_label.from, prev_macro_label.to, to_string(caller_label));
            if (const auto& labels = builder.prog.cfg().labels();
                std::ranges::find(labels, prev_label) != labels.end()) {
                builder.add_child(prev_label, label);
            }
        }

        // Walk all successor nodes.
        for (const auto& next_macro_nodes = builder.prog.cfg().children_of(macro_label);
             const auto& next_macro_label : next_macro_nodes) {
            if (next_macro_label == builder.prog.cfg().exit_label()) {
                // This is an exit transition, so add edge to the block to execute
                // upon returning from the macro.
                builder.add_child(label, exit_to_label);
            } else if (!seen_labels.contains(next_macro_label)) {
                // Push any other unprocessed successor label onto the list to be processed.
                if (!macro_labels.contains(next_macro_label)) {
                    macro_labels.insert(next_macro_label);
                }
                seen_labels.insert(macro_label);
            }
        }
    }

    // Remove the original edge from the caller node to its successor,
    // since processing now goes through the function macro instead.
    builder.remove_child(caller_label, exit_to_label);

    // Finally, recurse to replace any nested function macros.
    string caller_label_str = to_string(caller_label);
    const long stack_frame_depth = std::ranges::count(caller_label_str, STACK_FRAME_DELIMITER) + 2;
    for (const auto& macro_label : seen_labels) {
        const label_t label{macro_label.from, macro_label.to, caller_label_str};
        if (const auto pins = std::get_if<CallLocal>(&builder.prog.instruction_at(label))) {
            if (stack_frame_depth >= MAX_CALL_STACK_FRAMES) {
                throw InvalidControlFlow{"too many call stack frames"};
            }
            add_cfg_nodes(builder, label, pins->target);
        }
    }
}

/// Convert an instruction sequence to a control-flow graph (CFG).
static cfg_builder_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must_have_exit) {
    cfg_builder_t builder;

    // First add all instructions to the CFG without connecting
    for (const auto& [label, inst, _] : insts) {
        if (std::holds_alternative<Undefined>(inst)) {
            continue;
        }
        builder.insert(label, inst);
    }

    if (insts.size() == 0) {
        throw InvalidControlFlow{"empty instruction sequence"};
    } else {
        const auto& [label, inst, _0] = insts[0];
        builder.add_child(builder.prog.cfg().entry_label(), label);
    }

    // Do a first pass ignoring all function macro calls.
    for (size_t i = 0; i < insts.size(); i++) {
        const auto& [label, inst, _0] = insts[i];

        if (std::holds_alternative<Undefined>(inst)) {
            continue;
        }

        label_t fallthrough{builder.prog.cfg().exit_label()};
        if (i + 1 < insts.size()) {
            fallthrough = std::get<0>(insts[i + 1]);
        } else {
            if (has_fall(inst) && must_have_exit) {
                throw InvalidControlFlow{"fallthrough in last instruction"};
            }
        }
        if (const auto jmp = std::get_if<Jmp>(&inst)) {
            if (const auto cond = jmp->cond) {
                label_t target_label = jmp->target;
                if (target_label == fallthrough) {
                    builder.add_child(label, fallthrough);
                    continue;
                }
                if (!builder.prog.cfg().contains(target_label)) {
                    throw InvalidControlFlow{"jump to undefined label " + to_string(target_label)};
                }
                builder.insert_jump(label, target_label, Assume{.cond = *cond, .is_implicit = true});
                builder.insert_jump(label, fallthrough, Assume{.cond = reverse(*cond), .is_implicit = true});
            } else {
                builder.add_child(label, jmp->target);
            }
        } else {
            if (has_fall(inst)) {
                builder.add_child(label, fallthrough);
            }
        }
        if (std::holds_alternative<Exit>(inst)) {
            builder.add_child(label, builder.prog.cfg().exit_label());
        }
    }

    // Now replace macros. We have to do this as a second pass so that
    // we only add new nodes that are actually reachable, based on the
    // results of the first pass.
    for (const auto& [label, inst, _] : insts) {
        if (const auto pins = std::get_if<CallLocal>(&inst)) {
            add_cfg_nodes(builder, label, pins->target);
        }
    }

    return builder;
}

Program Program::from_sequence(const InstructionSeq& inst_seq, const program_info& info,
                               const prepare_cfg_options& options) {
    thread_local_program_info.set(info);

    // Convert the instruction sequence to a deterministic control-flow graph.
    cfg_builder_t builder = instruction_seq_to_cfg(inst_seq, options.must_have_exit);

    // Detect loops using Weak Topological Ordering (WTO) and insert counters at loop entry points. WTO provides a
    // hierarchical decomposition of the CFG that identifies all strongly connected components (cycles) and their entry
    // points. These entry points serve as natural locations for loop counters that help verify program termination.
    if (options.check_for_termination) {
        const crab::wto_t wto{builder.prog.cfg()};
        wto.for_each_loop_head([&](const label_t& label) -> void {
            builder.insert_after(label, label_t::make_increment_counter(label), IncrementLoopCounter{label});
        });
    }

    // Annotate the CFG by explicitly adding in assertions before every memory instruction.
    for (const auto& label : builder.prog.labels()) {
        builder.set_assertions(label, get_assertions(builder.prog.instruction_at(label), info, label));
    }
    return builder.prog;
}

std::set<basic_block_t> basic_block_t::collect_basic_blocks(const cfg_t& cfg, const bool simplify) {
    if (!simplify) {
        std::set<basic_block_t> res;
        for (const label_t& label : cfg.labels()) {
            if (label != cfg.entry_label() && label != cfg.exit_label()) {
                res.insert(basic_block_t{label});
            }
        }
        return res;
    }

    std::set<basic_block_t> res;
    std::set<label_t> worklist;
    for (const label_t& label : cfg.labels()) {
        worklist.insert(label);
    }
    std::set<label_t> seen;
    while (!worklist.empty()) {
        label_t label = *worklist.begin();
        worklist.erase(label);
        if (seen.contains(label)) {
            continue;
        }
        seen.insert(label);

        if (cfg.in_degree(label) == 1 && cfg.num_siblings(label) == 1) {
            continue;
        }
        basic_block_t bb{label};
        while (cfg.out_degree(label) == 1) {
            const label_t& next_label = cfg.get_child(bb.last_label());

            if (seen.contains(next_label) || next_label == cfg.exit_label() || cfg.in_degree(next_label) != 1) {
                break;
            }

            if (bb.first_label() == cfg.entry_label()) {
                // Entry instruction is Undefined. We want to start with 0
                bb.m_ts.clear();
            }
            bb.m_ts.push_back(next_label);

            worklist.erase(next_label);
            seen.insert(next_label);

            label = next_label;
        }
        res.emplace(std::move(bb));
    }
    return res;
}

/// Get the type of given Instruction.
/// Most of these type names are also statistics header labels.
static std::string instype(Instruction ins) {
    if (const auto pcall = std::get_if<Call>(&ins)) {
        if (pcall->is_map_lookup) {
            return "call_1";
        }
        if (pcall->pairs.empty()) {
            if (std::ranges::all_of(pcall->singles,
                                    [](const ArgSingle kr) { return kr.kind == ArgSingle::Kind::ANYTHING; })) {
                return "call_nomem";
            }
        }
        return "call_mem";
    } else if (std::holds_alternative<Callx>(ins)) {
        return "callx";
    } else if (const auto pimm = std::get_if<Mem>(&ins)) {
        return pimm->is_load ? "load" : "store";
    } else if (std::holds_alternative<Atomic>(ins)) {
        return "load_store";
    } else if (std::holds_alternative<Packet>(ins)) {
        return "packet_access";
    } else if (const auto pins = std::get_if<Bin>(&ins)) {
        switch (pins->op) {
        case Bin::Op::MOV:
        case Bin::Op::MOVSX8:
        case Bin::Op::MOVSX16:
        case Bin::Op::MOVSX32: return "assign";
        default: return "arith";
        }
    } else if (std::holds_alternative<Un>(ins)) {
        return "arith";
    } else if (std::holds_alternative<LoadMapFd>(ins)) {
        return "assign";
    } else if (std::holds_alternative<LoadMapAddress>(ins)) {
        return "assign";
    } else if (std::holds_alternative<Assume>(ins)) {
        return "assume";
    } else {
        return "other";
    }
}

std::vector<std::string> stats_headers() {
    return {
        "instructions", "joins",      "other",      "jumps",         "assign",  "arith",
        "load",         "store",      "load_store", "packet_access", "call_1",  "call_mem",
        "call_nomem",   "reallocate", "map_in_map", "arith64",       "arith32",
    };
}

std::map<std::string, int> collect_stats(const Program& prog) {
    std::map<std::string, int> res;
    for (const auto& h : stats_headers()) {
        res[h] = 0;
    }
    for (const auto& label : prog.labels()) {
        res["instructions"]++;
        const auto cmd = prog.instruction_at(label);
        if (const auto pins = std::get_if<LoadMapFd>(&cmd)) {
            if (pins->mapfd == -1) {
                res["map_in_map"] = 1;
            }
        }
        if (const auto pins = std::get_if<Call>(&cmd)) {
            if (pins->reallocate_packet) {
                res["reallocate"] = 1;
            }
        }
        if (const auto pins = std::get_if<Bin>(&cmd)) {
            res[pins->is64 ? "arith64" : "arith32"]++;
        }
        res[instype(cmd)]++;
        if (prog.cfg().in_degree(label) > 1) {
            res["joins"]++;
        }
        if (prog.cfg().out_degree(label) > 1) {
            res["jumps"]++;
        }
    }
    return res;
}

crab::cfg_t crab::cfg_from_adjacency_list(const std::map<label_t, std::vector<label_t>>& adj_list) {
    cfg_builder_t builder;
    for (const auto& label : std::views::keys(adj_list)) {
        if (label == label_t::entry || label == label_t::exit) {
            continue;
        }
        builder.insert(label, Undefined{});
    }
    for (const auto& [label, children] : adj_list) {
        for (const auto& child : children) {
            builder.add_child(label, child);
        }
    }
    return builder.prog.cfg();
}

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <algorithm>
4	#include <cassert>
5	#include <map>
6	#include <optional>
7	#include <string>
8	#include <vector>
9
10	#include "config.hpp"
11	#include "crab/cfg.hpp"
12	#include "crab/wto.hpp"
13
14	#include "asm_syntax.hpp"
15	#include "program.hpp"
16
17	using std::optional;
18	using std::set;
19	using std::string;
20	using std::to_string;
21	using std::vector;
22
23	struct cfg_builder_t final {	1,243✔
24	Program prog;
25
26	// TODO: ins should be inserted elsewhere
27	void insert_after(const label_t& prev_label, const label_t& new_label, const Instruction& ins) {	32✔
28	if (prev_label == new_label) {	32✔
29	CRAB_ERROR("Cannot insert after the same label ", to_string(new_label));	×
30	}
31	std::set<label_t> prev_children;	32✔
32	std::swap(prev_children, prog.m_cfg.get_node(prev_label).children);	32✔
33
34	for (const label_t& next_label : prev_children) {	72✔
35	prog.m_cfg.get_node(next_label).parents.erase(prev_label);	40✔
36	}
37
38	insert(new_label, ins);	32✔
39	for (const label_t& next_label : prev_children) {	72✔
40	add_child(prev_label, new_label);	40✔
41	add_child(new_label, next_label);	40✔
42	}
43	}	32✔
44
45	// TODO: ins should be inserted elsewhere
46	void insert(const label_t& _label, const Instruction& ins) {	336,342✔
47	if (const auto it = prog.m_cfg.neighbours.find(_label); it != prog.m_cfg.neighbours.end()) {	336,342✔
48	CRAB_ERROR("Label ", to_string(_label), " already exists");	×
49	}
50	prog.m_cfg.neighbours.emplace(_label, crab::cfg_t::adjacent_t{});	336,342✔
51	prog.m_instructions.emplace(_label, ins);	336,342✔
52	}	336,342✔
53
54	// TODO: ins should be inserted elsewhere
55	label_t insert_jump(const label_t& from, const label_t& to, const Instruction& ins) {	50,448✔
56	const label_t jump_label = label_t::make_jump(from, to);	50,448✔
57	if (prog.m_cfg.contains(jump_label)) {	50,448✔
58	CRAB_ERROR("Jump label ", to_string(jump_label), " already exists");	×
59	}
60	insert(jump_label, ins);	50,448✔
61	add_child(from, jump_label);	50,448✔
62	add_child(jump_label, to);	50,448✔
63	return jump_label;	50,448✔
64	}	×
65
66	void add_child(const label_t& a, const label_t& b) {	364,270✔
67	assert(b != label_t::entry);	364,270✔
68	assert(a != label_t::exit);	364,270✔
69	prog.m_cfg.neighbours.at(a).children.insert(b);	364,270✔
70	prog.m_cfg.neighbours.at(b).parents.insert(a);	364,270✔
71	}	364,270✔
72
73	void remove_child(const label_t& a, const label_t& b) {	136✔
74	prog.m_cfg.get_node(a).children.erase(b);	136✔
75	prog.m_cfg.get_node(b).parents.erase(a);	136✔
76	}	136✔
77
78	void set_assertions(const label_t& label, const std::vector<Assertion>& assertions) {	341,152✔
79	if (!prog.m_cfg.contains(label)) {	341,152✔
80	CRAB_ERROR("Label ", to_string(label), " not found in the CFG: ");	×
81	}
82	prog.m_assertions.insert_or_assign(label, assertions);	341,152✔
83	}	341,152✔
84	};
85
86	using crab::basic_block_t;
87
88	/// Get the inverse of a given comparison operation.
89	static Condition::Op reverse(const Condition::Op op) {	25,224✔
90	switch (op) {	25,224✔
91	case Condition::Op::EQ: return Condition::Op::NE;	5,153✔
92	case Condition::Op::NE: return Condition::Op::EQ;	4,394✔
93
94	case Condition::Op::GE: return Condition::Op::LT;	150✔
95	case Condition::Op::LT: return Condition::Op::GE;	243✔
96
97	case Condition::Op::SGE: return Condition::Op::SLT;	17✔
98	case Condition::Op::SLT: return Condition::Op::SGE;	616✔
99
100	case Condition::Op::LE: return Condition::Op::GT;	17✔
101	case Condition::Op::GT: return Condition::Op::LE;	1,055✔
102
103	case Condition::Op::SLE: return Condition::Op::SGT;	17✔
104	case Condition::Op::SGT: return Condition::Op::SLE;	935✔
105
106	case Condition::Op::SET: return Condition::Op::NSET;	13✔
107	case Condition::Op::NSET: return Condition::Op::SET;	2✔
108	}
109	assert(false);
110	return {};
111	}
112
113	/// Get the inverse of a given comparison condition.
114	static Condition reverse(const Condition& cond) {	25,224✔
115	return {.op = reverse(cond.op), .left = cond.left, .right = cond.right, .is64 = cond.is64};	25,224✔
116	}
117
118	static bool has_fall(const Instruction& ins) {	258,066✔
119	if (std::holds_alternative<Exit>(ins)) {	258,066✔
120	return false;	1,277✔
121	}
122
123	if (const auto pins = std::get_if<Jmp>(&ins)) {	255,512✔
124	if (!pins->cond) {	114✔
125	return false;	57✔
126	}
127	}
128
129	return true;	127,699✔
130	}
131
132	/// Update a control-flow graph to inline function macros.
133	static void add_cfg_nodes(cfg_builder_t& builder, const label_t& caller_label, const label_t& entry_label) {	140✔
134	bool first = true;	140✔
135
136	// Get the label of the node to go to on returning from the macro.
137	label_t exit_to_label = builder.prog.cfg().get_child(caller_label);	140✔
138
139	// Construct the variable prefix to use for the new stack frame,
140	// and store a copy in the CallLocal instruction since the instruction-specific
141	// labels may only exist until the CFG is simplified.
142	const std::string stack_frame_prefix = to_string(caller_label);	140✔
143	if (const auto pcall = std::get_if<CallLocal>(&builder.prog.instruction_at(caller_label))) {	210✔
144	pcall->stack_frame_prefix = stack_frame_prefix;	140✔
145	}
146
147	// Walk the transitive closure of CFG nodes starting at entry_label and ending at
148	// any exit instruction.
149	std::set macro_labels{entry_label};	367✔
150	std::set seen_labels{entry_label};	367✔
151	while (!macro_labels.empty()) {	662✔
152	label_t macro_label = *macro_labels.begin();	526✔
153	macro_labels.erase(macro_label);	526✔
154
155	if (stack_frame_prefix == macro_label.stack_frame_prefix) {	526✔
156	throw InvalidControlFlow{stack_frame_prefix + ": illegal recursion"};	6✔
157	}
158
159	// Clone the macro block into a new block with the new stack frame prefix.
160	const label_t label{macro_label.from, macro_label.to, stack_frame_prefix};	785✔
161	auto inst = builder.prog.instruction_at(macro_label);	522✔
162	if (const auto pexit = std::get_if<Exit>(&inst)) {	522✔
163	pexit->stack_frame_prefix = label.stack_frame_prefix;	142✔
164	} else if (const auto pcall = std::get_if<Call>(&inst)) {	452✔
165	pcall->stack_frame_prefix = label.stack_frame_prefix;	2✔
166	}
167	builder.insert(label, inst);	522✔
168
169	if (first) {	522✔
170	// Add an edge from the caller to the new block.
171	first = false;	140✔
172	builder.add_child(caller_label, label);	140✔
173	}
174
175	// Add an edge from any other predecessors.
176	for (const auto& prev_macro_nodes = builder.prog.cfg().parents_of(macro_label);	783✔
177	const auto& prev_macro_label : prev_macro_nodes) {	1,173✔
178	const label_t prev_label(prev_macro_label.from, prev_macro_label.to, to_string(caller_label));	390✔
179	if (const auto& labels = builder.prog.cfg().labels();	390✔
180	std::ranges::find(labels, prev_label) != labels.end()) {	390✔
181	builder.add_child(prev_label, label);	384✔
182	}
183	}	390✔
184
185	// Walk all successor nodes.
186	for (const auto& next_macro_nodes = builder.prog.cfg().children_of(macro_label);	1,047✔
187	const auto& next_macro_label : next_macro_nodes) {	1,311✔
188	if (next_macro_label == builder.prog.cfg().exit_label()) {	792✔
189	// This is an exit transition, so add edge to the block to execute
190	// upon returning from the macro.
191	builder.add_child(label, exit_to_label);	140✔
192	} else if (!seen_labels.contains(next_macro_label)) {	388✔
193	// Push any other unprocessed successor label onto the list to be processed.
194	if (!macro_labels.contains(next_macro_label)) {	388✔
195	macro_labels.insert(next_macro_label);	386✔
196	}
197	seen_labels.insert(macro_label);	388✔
198	}
199	}
200	}	1,048✔
201
202	// Remove the original edge from the caller node to its successor,
203	// since processing now goes through the function macro instead.
204	builder.remove_child(caller_label, exit_to_label);	136✔
205
206	// Finally, recurse to replace any nested function macros.
207	string caller_label_str = to_string(caller_label);	136✔
208	const long stack_frame_depth = std::ranges::count(caller_label_str, STACK_FRAME_DELIMITER) + 2;	136✔
209	for (const auto& macro_label : seen_labels) {	480✔
210	const label_t label{macro_label.from, macro_label.to, caller_label_str};	576✔
211	if (const auto pins = std::get_if<CallLocal>(&builder.prog.instruction_at(label))) {	546✔
212	if (stack_frame_depth >= MAX_CALL_STACK_FRAMES) {	82✔
213	throw InvalidControlFlow{"too many call stack frames"};	10✔
214	}
215	add_cfg_nodes(builder, label, pins->target);	78✔
216	}
217	}	374✔
218	}	588✔
219
220	/// Convert an instruction sequence to a control-flow graph (CFG).
221	static cfg_builder_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must_have_exit) {	2,494✔
222	cfg_builder_t builder;	2,494✔
223
224	// First add all instructions to the CFG without connecting
225	for (const auto& [label, inst, _] : insts) {	287,800✔
226	if (std::holds_alternative<Undefined>(inst)) {	285,306✔
227	continue;	×
228	}
229	builder.insert(label, inst);	285,306✔
230	}
231
232	if (insts.size() == 0) {	2,494✔
233	throw InvalidControlFlow{"empty instruction sequence"};	×
234	} else {
235	const auto& [label, inst, _0] = insts[0];	2,494✔
236	builder.add_child(builder.prog.cfg().entry_label(), label);	2,498✔
237	}
238
239	// Do a first pass ignoring all function macro calls.
240	for (size_t i = 0; i < insts.size(); i++) {	287,800✔
241	const auto& [label, inst, _0] = insts[i];	285,306✔
242
243	if (std::holds_alternative<Undefined>(inst)) {	285,306✔
244	continue;	6✔
245	}
246
247	label_t fallthrough{builder.prog.cfg().exit_label()};	285,306✔
248	if (i + 1 < insts.size()) {	285,306✔
249	fallthrough = std::get<0>(insts[i + 1]);	282,812✔
250	} else {
251	if (has_fall(inst) && must_have_exit) {	3,171✔
252	throw InvalidControlFlow{"fallthrough in last instruction"};	×
253	}
254	}
255	if (const auto jmp = std::get_if<Jmp>(&inst)) {	285,306✔
256	if (const auto cond = jmp->cond) {	29,734✔
257	label_t target_label = jmp->target;	25,230✔
258	if (target_label == fallthrough) {	25,230✔
259	builder.add_child(label, fallthrough);	6✔
260	continue;	6✔
261	}
262	if (!builder.prog.cfg().contains(target_label)) {	25,224✔
263	throw InvalidControlFlow{"jump to undefined label " + to_string(target_label)};	×
264	}
265	builder.insert_jump(label, target_label, Assume{.cond = *cond, .is_implicit = true});	37,836✔
266	builder.insert_jump(label, fallthrough, Assume{.cond = reverse(*cond), .is_implicit = true});	50,448✔
267	} else {	25,230✔
268	builder.add_child(label, jmp->target);	4,504✔
269	}
270	} else {
271	if (has_fall(inst)) {	255,572✔
272	builder.add_child(label, fallthrough);	254,158✔
273	}
274	}
275	if (std::holds_alternative<Exit>(inst)) {	285,300✔
276	builder.add_child(label, builder.prog.cfg().exit_label());	2,121✔
277	}
278	}	285,306✔
279
280	// Now replace macros. We have to do this as a second pass so that
281	// we only add new nodes that are actually reachable, based on the
282	// results of the first pass.
283	for (const auto& [label, inst, _] : insts) {	287,744✔
284	if (const auto pins = std::get_if<CallLocal>(&inst)) {	285,285✔
285	add_cfg_nodes(builder, label, pins->target);	62✔
286	}
287	}
288
289	return builder;	2,486✔
290	}	8✔
291
292	Program Program::from_sequence(const InstructionSeq& inst_seq, const program_info& info,	2,494✔
293	const prepare_cfg_options& options) {
294	thread_local_program_info.set(info);	3,741✔
295
296	// Convert the instruction sequence to a deterministic control-flow graph.
297	cfg_builder_t builder = instruction_seq_to_cfg(inst_seq, options.must_have_exit);	2,494✔
298
299	// Detect loops using Weak Topological Ordering (WTO) and insert counters at loop entry points. WTO provides a
300	// hierarchical decomposition of the CFG that identifies all strongly connected components (cycles) and their entry
301	// points. These entry points serve as natural locations for loop counters that help verify program termination.
302	if (options.check_for_termination) {	2,486✔
303	const crab::wto_t wto{builder.prog.cfg()};	34✔
304	wto.for_each_loop_head([&](const label_t& label) -> void {	34✔
305	builder.insert_after(label, label_t::make_increment_counter(label), IncrementLoopCounter{label});	64✔
306	});	32✔
307	}	34✔
308
309	// Annotate the CFG by explicitly adding in assertions before every memory instruction.
310	for (const auto& label : builder.prog.labels()) {	343,638✔
311	builder.set_assertions(label, get_assertions(builder.prog.instruction_at(label), info, label));	682,304✔
312	}
313	return builder.prog;	3,729✔
314	}	2,486✔
315
316	std::set<basic_block_t> basic_block_t::collect_basic_blocks(const cfg_t& cfg, const bool simplify) {	×
317	if (!simplify) {	×
318	std::set<basic_block_t> res;	×
319	for (const label_t& label : cfg.labels()) {	×
320	if (label != cfg.entry_label() && label != cfg.exit_label()) {	×
321	res.insert(basic_block_t{label});	×
322	}
323	}
324	return res;	×
325	}	×
326
327	std::set<basic_block_t> res;	×
328	std::set<label_t> worklist;	×
329	for (const label_t& label : cfg.labels()) {	×
330	worklist.insert(label);	×
331	}
332	std::set<label_t> seen;	×
333	while (!worklist.empty()) {	×
334	label_t label = *worklist.begin();	×
335	worklist.erase(label);	×
336	if (seen.contains(label)) {	×
337	continue;	×
338	}
339	seen.insert(label);	×
340
341	if (cfg.in_degree(label) == 1 && cfg.num_siblings(label) == 1) {	×
342	continue;	×
343	}
344	basic_block_t bb{label};	×
345	while (cfg.out_degree(label) == 1) {	×
346	const label_t& next_label = cfg.get_child(bb.last_label());	×
347
348	if (seen.contains(next_label) \|\| next_label == cfg.exit_label() \|\| cfg.in_degree(next_label) != 1) {	×
349	break;
350	}
351
352	if (bb.first_label() == cfg.entry_label()) {	×
353	// Entry instruction is Undefined. We want to start with 0
354	bb.m_ts.clear();	×
355	}
356	bb.m_ts.push_back(next_label);	×
357
358	worklist.erase(next_label);	×
359	seen.insert(next_label);	×
360
361	label = next_label;	×
362	}	×
363	res.emplace(std::move(bb));	×
364	}	×
365	return res;	×
366	}	×
367
368	/// Get the type of given Instruction.
369	/// Most of these type names are also statistics header labels.
370	static std::string instype(Instruction ins) {	×
371	if (const auto pcall = std::get_if<Call>(&ins)) {	×
372	if (pcall->is_map_lookup) {	×
373	return "call_1";	×
374	}
375	if (pcall->pairs.empty()) {	×
376	if (std::ranges::all_of(pcall->singles,	×
377	[](const ArgSingle kr) { return kr.kind == ArgSingle::Kind::ANYTHING; })) {
378	return "call_nomem";	×
379	}
380	}
381	return "call_mem";	×
382	} else if (std::holds_alternative<Callx>(ins)) {
383	return "callx";	×
384	} else if (const auto pimm = std::get_if<Mem>(&ins)) {	×
385	return pimm->is_load ? "load" : "store";	×
386	} else if (std::holds_alternative<Atomic>(ins)) {
387	return "load_store";	×
388	} else if (std::holds_alternative<Packet>(ins)) {
389	return "packet_access";	×
390	} else if (const auto pins = std::get_if<Bin>(&ins)) {	×
391	switch (pins->op) {	×
392	case Bin::Op::MOV:	×
393	case Bin::Op::MOVSX8:
394	case Bin::Op::MOVSX16:
395	case Bin::Op::MOVSX32: return "assign";	×
396	default: return "arith";	×
397	}
398	} else if (std::holds_alternative<Un>(ins)) {
399	return "arith";	×
400	} else if (std::holds_alternative<LoadMapFd>(ins)) {
401	return "assign";	×
402	} else if (std::holds_alternative<LoadMapAddress>(ins)) {
NEW 403	return "assign";	×
404	} else if (std::holds_alternative<Assume>(ins)) {
405	return "assume";	×
406	} else {
407	return "other";	×
408	}
409	}
410
411	std::vector<std::string> stats_headers() {	×
412	return {
413	"instructions", "joins", "other", "jumps", "assign", "arith",
414	"load", "store", "load_store", "packet_access", "call_1", "call_mem",
415	"call_nomem", "reallocate", "map_in_map", "arith64", "arith32",
416	};	×
417	}
418
419	std::map<std::string, int> collect_stats(const Program& prog) {	×
420	std::map<std::string, int> res;	×
421	for (const auto& h : stats_headers()) {	×
422	res[h] = 0;	×
423	}	×
424	for (const auto& label : prog.labels()) {	×
425	res["instructions"]++;	×
426	const auto cmd = prog.instruction_at(label);	×
427	if (const auto pins = std::get_if<LoadMapFd>(&cmd)) {	×
428	if (pins->mapfd == -1) {	×
429	res["map_in_map"] = 1;	×
430	}
431	}
432	if (const auto pins = std::get_if<Call>(&cmd)) {	×
433	if (pins->reallocate_packet) {	×
434	res["reallocate"] = 1;	×
435	}
436	}
437	if (const auto pins = std::get_if<Bin>(&cmd)) {	×
438	res[pins->is64 ? "arith64" : "arith32"]++;	×
439	}
440	res[instype(cmd)]++;	×
441	if (prog.cfg().in_degree(label) > 1) {	×
442	res["joins"]++;	×
443	}
444	if (prog.cfg().out_degree(label) > 1) {	×
445	res["jumps"]++;	×
446	}
447	}	×
448	return res;	×
449	}	×
450
451	crab::cfg_t crab::cfg_from_adjacency_list(const std::map<label_t, std::vector<label_t>>& adj_list) {	6✔
452	cfg_builder_t builder;	6✔
453	for (const auto& label : std::views::keys(adj_list)) {	46✔
454	if (label == label_t::entry \|\| label == label_t::exit) {	40✔
455	continue;	6✔
456	}
457	builder.insert(label, Undefined{});	51✔
458	}
459	for (const auto& [label, children] : adj_list) {	46✔
460	for (const auto& child : children) {	94✔
461	builder.add_child(label, child);	54✔
462	}
463	}
464	return builder.prog.cfg();	12✔
465	}	6✔

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