Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make the assertions part of a generalized instruction #779

Merged
merged 11 commits into from
Nov 8, 2024
Merged

Make the assertions part of a generalized instruction #779

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
21add5e
Make the assertions part of the generalized instruction
elazarg Nov 7, 2024
01a02e7
address review comments
elazarg Nov 7, 2024
59db668
minor
elazarg Nov 7, 2024
31ca739
rename: keep Instruction, introduce GuardedInstruction
elazarg Nov 8, 2024
7862db8
minor
elazarg Nov 8, 2024
c72754c
minor
elazarg Nov 8, 2024
4f61041
minor
elazarg Nov 8, 2024
bf98ef7
minor
elazarg Nov 8, 2024
9e61378
InstructionSeq is Instruction, not GuardedInstruction
elazarg Nov 8, 2024
09c297b
move InstructionSeq close to Instruction
elazarg Nov 8, 2024
afd0a48
review comments
elazarg Nov 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions scripts/format-code
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -169,15 +169,15 @@ check_clang-format()
cf=$(command -v clang-format 2> /dev/null)
if [[ ! -x ${cf} ]]; then
echo "clang-format is not installed"
exit 1
exit 0 # do not fail, just warn
elazarg marked this conversation as resolved.
Show resolved Hide resolved
fi
cf="clang-format"
fi

local required_cfver='17.0.3'
# shellcheck disable=SC2155
local cfver=$(${cf} --version | grep -o -E '[0-9]+\.[0-9]+\.[0-9]+' | head -1)
check_version "${required_cfver}" "${cfver}"
# local required_cfver='17.0.3'
# # shellcheck disable=SC2155
# local cfver=$(${cf} --version | grep -o -E '[0-9]+\.[0-9]+\.[0-9]+' | head -1)
# check_version "${required_cfver}" "${cfver}"
}

check_clang-format
Expand Down
40 changes: 19 additions & 21 deletions src/asm_cfg.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t
basic_block_t& caller_node = cfg.get_node(caller_label);
const std::string stack_frame_prefix = to_string(caller_label);
for (auto& inst : caller_node) {
if (const auto pcall = std::get_if<CallLocal>(&inst)) {
if (const auto pcall = std::get_if<CallLocal>(&inst.cmd)) {
pcall->stack_frame_prefix = stack_frame_prefix;
}
}
Expand All @@ -73,9 +73,9 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t
const label_t label{macro_label.from, macro_label.to, stack_frame_prefix};
auto& bb = cfg.insert(label);
for (auto inst : cfg.get_node(macro_label)) {
if (const auto pexit = std::get_if<Exit>(&inst)) {
if (const auto pexit = std::get_if<Exit>(&inst.cmd)) {
pexit->stack_frame_prefix = label.stack_frame_prefix;
} else if (const auto pcall = std::get_if<Call>(&inst)) {
} else if (const auto pcall = std::get_if<Call>(&inst.cmd)) {
pcall->stack_frame_prefix = label.stack_frame_prefix;
}
bb.insert(inst);
Expand Down Expand Up @@ -123,7 +123,7 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t
for (const auto& macro_label : seen_labels) {
for (const label_t label(macro_label.from, macro_label.to, caller_label_str);
const auto& inst : cfg.get_node(label)) {
if (const auto pins = std::get_if<CallLocal>(&inst)) {
if (const auto pins = std::get_if<CallLocal>(&inst.cmd)) {
if (stack_frame_depth >= MAX_CALL_STACK_FRAMES) {
throw std::runtime_error{"too many call stack frames"};
}
Expand All @@ -142,7 +142,7 @@ static cfg_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must
// Do a first pass ignoring all function macro calls.
for (const auto& [label, inst, _] : insts) {

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

Expand All @@ -158,14 +158,14 @@ static cfg_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must
cfg.get_node(*falling_from) >> bb;
falling_from = {};
}
if (has_fall(inst)) {
if (has_fall(inst.cmd)) {
falling_from = label;
}
if (auto jump_target = get_jump(inst)) {
if (auto jump_target = get_jump(inst.cmd)) {
bb >> cfg.insert(*jump_target);
}

if (std::holds_alternative<Exit>(inst)) {
if (std::holds_alternative<Exit>(inst.cmd)) {
bb >> cfg.get_node(cfg.exit_label());
}
}
Expand All @@ -181,7 +181,7 @@ static cfg_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must
// 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)) {
if (const auto pins = std::get_if<CallLocal>(&inst.cmd)) {
add_cfg_nodes(cfg, label, pins->target);
}
}
Expand Down Expand Up @@ -236,9 +236,7 @@ static cfg_t to_nondet(const cfg_t& cfg) {
basic_block_t& newbb = res.insert(this_label);

for (const auto& ins : bb) {
if (!std::holds_alternative<Jmp>(ins)) {
newbb.insert(ins);
}
newbb.insert(ins);
}

for (const label_t& prev_label : bb.prev_blocks_set()) {
Expand All @@ -250,7 +248,7 @@ static cfg_t to_nondet(const cfg_t& cfg) {
auto nextlist = bb.next_blocks_set();
if (nextlist.size() == 2) {
label_t mid_label = this_label;
auto jmp = std::get<Jmp>(*bb.rbegin());
auto jmp = std::get<Jmp>(bb.rbegin()->cmd);

nextlist.erase(jmp.target);
elazarg marked this conversation as resolved.
Show resolved Hide resolved
label_t fallthrough = *nextlist.begin();
Expand All @@ -262,7 +260,7 @@ static cfg_t to_nondet(const cfg_t& cfg) {
for (const auto& [next_label, cond1] : jumps) {
label_t jump_label = label_t::make_jump(mid_label, next_label);
basic_block_t& jump_bb = res.insert(jump_label);
jump_bb.insert(Assume{cond1});
jump_bb.insert({.cmd = Assume{cond1}});
newbb >> jump_bb;
jump_bb >> res.insert(next_label);
}
Expand All @@ -275,7 +273,7 @@ static cfg_t to_nondet(const cfg_t& cfg) {
return res;
}

/// Get the type of given instruction.
/// 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)) {
Expand Down Expand Up @@ -333,21 +331,21 @@ std::map<std::string, int> collect_stats(const cfg_t& cfg) {
res["basic_blocks"]++;
basic_block_t const& bb = cfg.get_node(this_label);

for (Instruction ins : bb) {
if (const auto pins = std::get_if<LoadMapFd>(&ins)) {
for (GuardedInstruction ins : bb) {
if (const auto pins = std::get_if<LoadMapFd>(&ins.cmd)) {
if (pins->mapfd == -1) {
res["map_in_map"] = 1;
}
}
if (const auto pins = std::get_if<Call>(&ins)) {
if (const auto pins = std::get_if<Call>(&ins.cmd)) {
if (pins->reallocate_packet) {
res["reallocate"] = 1;
}
}
if (const auto pins = std::get_if<Bin>(&ins)) {
if (const auto pins = std::get_if<Bin>(&ins.cmd)) {
res[pins->is64 ? "arith64" : "arith32"]++;
}
res[instype(ins)]++;
res[instype(ins.cmd)]++;
}
elazarg marked this conversation as resolved.
Show resolved Hide resolved
if (unique(bb.prev_blocks()).size() > 1) {
res["joins"]++;
Expand All @@ -369,7 +367,7 @@ cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const pr
if (options.check_for_termination) {
const wto_t wto(det_cfg);
wto.for_each_loop_head(
[&](const label_t& label) { det_cfg.get_node(label).insert_front(IncrementLoopCounter{label}); });
[&](const label_t& label) { det_cfg.get_node(label).insert_front({.cmd = IncrementLoopCounter{label}}); });
}

// Annotate the CFG by adding in assertions before every memory instruction.
Expand Down
8 changes: 3 additions & 5 deletions src/asm_marshal.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -205,8 +205,6 @@ struct MarshalVisitor {

vector<ebpf_inst> operator()(Assume const&) const { throw std::invalid_argument("Cannot marshal assumptions"); }

vector<ebpf_inst> operator()(Assert const&) const { throw std::invalid_argument("Cannot marshal assertions"); }

vector<ebpf_inst> operator()(Jmp const& b) const {
if (b.cond) {
ebpf_inst res{
Expand Down Expand Up @@ -315,7 +313,7 @@ static auto get_labels(const InstructionSeq& insts) {
std::map<label_t, pc_t> pc_of_label;
for (const auto& [label, inst, _] : insts) {
pc_of_label[label] = pc;
pc += size(inst);
pc += size(inst.cmd);
elazarg marked this conversation as resolved.
Show resolved Hide resolved
}
return pc_of_label;
}
Expand All @@ -326,10 +324,10 @@ vector<ebpf_inst> marshal(const InstructionSeq& insts) {
pc_t pc = 0;
for (auto [label, ins, _] : insts) {
(void)label; // unused
if (const auto pins = std::get_if<Jmp>(&ins)) {
if (const auto pins = std::get_if<Jmp>(&ins.cmd)) {
pins->target = label_t{gsl::narrow<int>(pc_of_label.at(pins->target))};
}
for (const auto e : marshal(ins, pc)) {
for (const auto e : marshal(ins.cmd, pc)) {
pc++;
res.push_back(e);
}
Expand Down
Loading
Loading