Implement callx instruction

src/asm_cfg.cpp

@@ -174,6 +174,8 @@ static std::string instype(Instruction ins) {
             }
         }
         return "call_mem";
+    } else if (std::holds_alternative<Callx>(ins)) {
+        return "callx";
     } else if (std::holds_alternative<Mem>(ins)) {
         return std::get<Mem>(ins).is_load ? "load" : "store";
     } else if (std::holds_alternative<LockAdd>(ins)) {

src/asm_marshal.cpp

@@ -175,7 +175,13 @@ struct MarshalVisitor {
 
     vector<ebpf_inst> operator()(Call const& b) {
         return {
-            ebpf_inst{.opcode = static_cast<uint8_t>(INST_OP_CALL), .dst = 0, .src = 0, .offset = 0, .imm = b.func}};
+            ebpf_inst{.opcode = static_cast<uint8_t>(INST_OP_CALL | INST_SRC_IMM), .dst = 0, .src = 0, .offset = 0, .imm = b.func}};
+    }
+
+    vector<ebpf_inst> operator()(Callx const& b) {
+        // callx is defined to have the register in 'dst' not in 'src'.
+        return {
+            ebpf_inst{.opcode = static_cast<uint8_t>(INST_OP_CALL | INST_SRC_REG), .dst = b.func.v, .src = 0, .offset = 0}};
     }
 
     vector<ebpf_inst> operator()(Exit const& b) {

src/asm_ostream.cpp

@@ -189,6 +189,10 @@ std::ostream& operator<<(std::ostream& os, TypeConstraint const& tc) {
     return os << typereg(tc.reg) << " " << cmp_op << " " << tc.types;
 }
 
+std::ostream& operator<<(std::ostream& os, FuncConstraint const& fc) {
+    return os << typereg(fc.reg) << " is helper";
+}
+
 std::ostream& operator<<(std::ostream& os, AssertionConstraint const& a) {
     return std::visit([&](const auto& a) -> std::ostream& { return os << a; }, a);
 }
@@ -262,6 +266,8 @@ struct InstructionPrinterVisitor {
         os_ << ")";
     }
 
+    void operator()(Callx const& callx) { os_ << "callx " << callx.func; }
+
     void operator()(Exit const& b) { os_ << "exit"; }
 
     void operator()(Jmp const& b) {

src/asm_ostream.hpp

@@ -54,6 +54,7 @@ inline std::ostream& operator<<(std::ostream& os, LoadMapFd const& a) { return o
 inline std::ostream& operator<<(std::ostream& os, Bin const& a) { return os << (Instruction)a; }
 inline std::ostream& operator<<(std::ostream& os, Un const& a) { return os << (Instruction)a; }
 inline std::ostream& operator<<(std::ostream& os, Call const& a) { return os << (Instruction)a; }
+inline std::ostream& operator<<(std::ostream& os, Callx const& a) { return os << (Instruction)a; }
 inline std::ostream& operator<<(std::ostream& os, Exit const& a) { return os << (Instruction)a; }
 inline std::ostream& operator<<(std::ostream& os, Jmp const& a) { return os << (Instruction)a; }
 inline std::ostream& operator<<(std::ostream& os, Packet const& a) { return os << (Instruction)a; }

src/asm_parse.cpp

@@ -148,6 +148,9 @@ Instruction parse_instruction(const std::string& line, const std::map<std::strin
         int func = boost::lexical_cast<int>(m[1]);
         return make_call(func, g_ebpf_platform_linux);
     }
+    if (regex_match(text, m, regex("callx " REG))) {
+        return Callx{reg(m[1])};
+    }
     if (regex_match(text, m, regex(WREG OPASSIGN REG))) {
         std::string r = m[1];
         return Bin{.op = str_to_binop.at(m[2]), .dst = reg(r), .v = reg(m[3]), .is64 = r.at(0) != 'w', .lddw = false};

src/asm_syntax.hpp

@@ -205,6 +205,11 @@ struct Exit {
     constexpr bool operator==(const Exit&) const = default;
 };
 
+struct Callx {
+    Reg func;
+    constexpr bool operator==(const Callx&) const = default;
+};
+
 struct Deref {
     int32_t width{};
     Reg basereg;
@@ -335,14 +340,19 @@ struct TypeConstraint {
     constexpr bool operator==(const TypeConstraint&) const = default;
 };
 
+struct FuncConstraint {
+    Reg reg;
+    constexpr bool operator==(const FuncConstraint&) const = default;
+};
+
 /// Condition check whether something is a valid size.
 struct ZeroCtxOffset {
     Reg reg;
     constexpr bool operator==(const ZeroCtxOffset&) const = default;
 };
 
 using AssertionConstraint =
-    std::variant<Comparable, Addable, ValidDivisor, ValidAccess, ValidStore, ValidSize, ValidMapKeyValue, TypeConstraint, ZeroCtxOffset>;
+    std::variant<Comparable, Addable, ValidDivisor, ValidAccess, ValidStore, ValidSize, ValidMapKeyValue, TypeConstraint, FuncConstraint, ZeroCtxOffset>;
 
 struct Assert {
     AssertionConstraint cst;
@@ -355,7 +365,7 @@ struct IncrementLoopCounter {
     constexpr bool operator==(const IncrementLoopCounter&) const = default;
 };
 
-using Instruction = std::variant<Undefined, Bin, Un, LoadMapFd, Call, Exit, Jmp, Mem, Packet, LockAdd, Assume, Assert, IncrementLoopCounter>;
+using Instruction = std::variant<Undefined, Bin, Un, LoadMapFd, Call, Callx, Exit, Jmp, Mem, Packet, LockAdd, Assume, Assert, IncrementLoopCounter>;
 
 using LabeledInstruction = std::tuple<label_t, Instruction, std::optional<btf_line_info_t>>;
 using InstructionSeq = std::vector<LabeledInstruction>;

src/asm_unmarshal.cpp

@@ -252,7 +252,7 @@ struct Unmarshaller {
                 throw InvalidInstruction(pc, inst.opcode);
             bool isLoad = getMemIsLoad(inst.opcode);
             if (isLoad && inst.dst == R10_STACK_POINTER)
-                throw InvalidInstruction(pc, "Cannot modify r10");
+                throw InvalidInstruction(pc, "cannot modify r10");
             bool isImm = !(inst.opcode & 1);
             if (isImm && inst.src != 0)
                 throw InvalidInstruction(pc, inst.opcode);
@@ -302,7 +302,7 @@ struct Unmarshaller {
 
     auto makeAluOp(size_t pc, ebpf_inst inst) -> Instruction {
         if (inst.dst == R10_STACK_POINTER)
-            throw InvalidInstruction(pc, "Invalid target r10");
+            throw InvalidInstruction(pc, "invalid target r10");
         if (inst.dst > R10_STACK_POINTER || inst.src > R10_STACK_POINTER)
             throw InvalidInstruction(pc, "bad register");
         bool is64 = (inst.opcode & INST_CLS_MASK) == INST_CLS_ALU64;
@@ -379,7 +379,7 @@ struct Unmarshaller {
     auto makeCall(int32_t imm) const {
         EbpfHelperPrototype proto = info.platform->get_helper_prototype(imm);
         if (proto.return_type == EBPF_RETURN_TYPE_UNSUPPORTED) {
-            throw std::runtime_error(std::string("Unsupported function: ") + proto.name);
+            throw std::runtime_error(std::string("unsupported function: ") + proto.name);
         }
         Call res;
         res.func = imm;
@@ -397,7 +397,7 @@ struct Unmarshaller {
         for (size_t i = 1; i < args.size() - 1; i++) {
             switch (args[i]) {
             case EBPF_ARGUMENT_TYPE_UNSUPPORTED: {
-                throw std::runtime_error(std::string("Unsupported function: ") + proto.name);
+                throw std::runtime_error(std::string("unsupported function: ") + proto.name);
             }
             case EBPF_ARGUMENT_TYPE_DONTCARE: return res;
             case EBPF_ARGUMENT_TYPE_ANYTHING:
@@ -422,21 +422,38 @@ struct Unmarshaller {
         return res;
     }
 
+    auto makeCallx(ebpf_inst inst, pc_t pc) const {
+        // callx puts the register number in the 'dst' field rather than the 'src' field.
+        if (inst.dst > R10_STACK_POINTER)
+            throw InvalidInstruction(pc, "bad register");
+        if (inst.imm != 0) {
+            // Clang prior to v19 put the register number into the 'imm' field.
+            if (inst.dst > 0)
+                throw InvalidInstruction(pc, make_opcode_message("nonzero imm for", inst.opcode));
+            if (inst.imm < 0 || inst.imm > R10_STACK_POINTER)
+                throw InvalidInstruction(pc, "bad register");
+            return Callx{(uint8_t)inst.imm};
+        }
+        return Callx{inst.dst};
+    }
+
     auto makeJmp(ebpf_inst inst, const vector<ebpf_inst>& insts, pc_t pc) -> Instruction {
         switch ((inst.opcode >> 4) & 0xF) {
         case INST_CALL:
             if ((inst.opcode & INST_CLS_MASK) != INST_CLS_JMP)
                 throw InvalidInstruction(pc, inst.opcode);
-            if (inst.opcode & INST_SRC_REG)
+            if (!info.platform->callx && (inst.opcode & INST_SRC_REG))
                 throw InvalidInstruction(pc, inst.opcode);
             if (inst.src > 0)
                 throw InvalidInstruction(pc, inst.opcode);
             if (inst.offset != 0)
                 throw InvalidInstruction(pc, make_opcode_message("nonzero offset for", inst.opcode));
+            if (inst.opcode & INST_SRC_REG)
+                return makeCallx(inst, pc);
             if (inst.dst != 0)
                 throw InvalidInstruction(pc, make_opcode_message("nonzero dst for register", inst.opcode));
             if (!info.platform->is_helper_usable(inst.imm))
-                throw InvalidInstruction(pc, "invalid helper function id");
+                throw InvalidInstruction(pc, "invalid helper function id " + std::to_string(inst.imm));
             return makeCall(inst.imm);
         case INST_EXIT:
             if ((inst.opcode & INST_CLS_MASK) != INST_CLS_JMP || (inst.opcode & INST_SRC_REG))

src/assertions.cpp

@@ -105,6 +105,13 @@ class AssertExtractor {
         return res;
     }
 
+    vector<Assert> operator()(Callx const& callx) const {
+        vector<Assert> res;
+        res.emplace_back(TypeConstraint{callx.func, TypeGroup::number});
+        res.emplace_back(FuncConstraint{callx.func});
+        return res;
+    }
+
     [[nodiscard]]
     vector<Assert> explicate(Condition cond) const {
         if (info.type.is_privileged)
@@ -234,6 +241,10 @@ class AssertExtractor {
     }
 };
 
+vector<Assert> get_assertions(Instruction ins, const program_info& info) {
+    return std::visit(AssertExtractor{info}, ins);
+}
+
 /// Annotate the CFG by adding explicit assertions for all the preconditions
 /// of any instruction. For example, jump instructions are asserted not to
 /// compare numbers and pointers, or pointers to potentially distinct memory
@@ -244,7 +255,7 @@ void explicate_assertions(cfg_t& cfg, const program_info& info) {
         (void)label; // unused
         vector<Instruction> insts;
         for (const auto& ins : vector<Instruction>(bb.begin(), bb.end())) {
-            for (auto a : std::visit(AssertExtractor{info}, ins))
+            for (auto a : get_assertions(ins, info))
                 insts.emplace_back(a);
             insts.push_back(ins);
         }

src/crab/cfg.hpp

@@ -519,6 +519,7 @@ std::map<std::string, int> collect_stats(const cfg_t&);
 cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, bool simplify, bool must_have_exit=true);
 
 void explicate_assertions(cfg_t& cfg, const program_info& info);
+std::vector<Assert> get_assertions(Instruction ins, const program_info& info);
 
 void print_dot(const cfg_t& cfg, std::ostream& out);
 void print_dot(const cfg_t& cfg, const std::string& outfile);

src/crab/ebpf_domain.cpp

@@ -15,6 +15,7 @@
 #include "crab/ebpf_domain.hpp"
 
 #include "asm_ostream.hpp"
+#include "asm_unmarshal.hpp"
 #include "config.hpp"
 #include "dsl_syntax.hpp"
 #include "platform.hpp"
@@ -1558,13 +1559,35 @@ void ebpf_domain_t::operator()(const ValidStore& s) {
 
 void ebpf_domain_t::operator()(const TypeConstraint& s) {
     if (!type_inv.is_in_group(m_inv, s.reg, s.types))
-        require(m_inv, linear_constraint_t::FALSE(), "");
+        require(m_inv, linear_constraint_t::FALSE(), "Invalid type");
+}
+
+void ebpf_domain_t::operator()(const FuncConstraint& s) {
+    // Look up the helper function id.
+    const reg_pack_t& reg = reg_pack(s.reg);
+    auto src_interval = m_inv.eval_interval(reg.svalue);
+    if (auto sn = src_interval.singleton()) {
+        if (sn->fits_sint32()) {
+            // We can now process it as if the id was immediate.
+            int32_t imm = sn->cast_to_sint32();
+            if (!global_program_info->platform->is_helper_usable(imm)) {
+                require(m_inv, linear_constraint_t::FALSE(), "invalid helper function id " + std::to_string(imm));
+                return;
+            }
+            Call call = make_call(imm, *global_program_info->platform);
+            for (Assert a : get_assertions(call, *global_program_info)) {
+                (*this)(a);
+            }
+            return;
+        }
+    }
+    require(m_inv, linear_constraint_t::FALSE(), "callx helper function id is not a valid singleton");
 }
 
 void ebpf_domain_t::operator()(const ValidSize& s) {
     using namespace crab::dsl_syntax;
     auto r = reg_pack(s.reg);
-    require(m_inv, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "");
+    require(m_inv, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size");
 }
 
 // Get the start and end of the range of possible map fd values.
@@ -1825,7 +1848,7 @@ void ebpf_domain_t::operator()(const ValidAccess& s) {
 void ebpf_domain_t::operator()(const ZeroCtxOffset& s) {
     using namespace crab::dsl_syntax;
     auto reg = reg_pack(s.reg);
-    require(m_inv, reg.ctx_offset == 0, "");
+    require(m_inv, reg.ctx_offset == 0, "Nonzero context offset");
 }
 
 void ebpf_domain_t::operator()(const Assert& stmt) {
@@ -2232,6 +2255,28 @@ void ebpf_domain_t::operator()(const Call& call) {
     }
 }
 
+void ebpf_domain_t::operator()(const Callx& callx) {
+    using namespace crab::dsl_syntax;
+    if (m_inv.is_bottom())
+        return;
+
+    // Look up the helper function id.
+    const reg_pack_t& reg = reg_pack(callx.func);
+    auto src_interval = m_inv.eval_interval(reg.svalue);
+    if (auto sn = src_interval.singleton()) {
+        if (sn->fits_sint32()) {
+            // We can now process it as if the id was immediate.
+            int32_t imm = sn->cast_to_sint32();
+            if (!global_program_info->platform->is_helper_usable(imm)) {
+                return;
+            }
+            Call call = make_call(imm, *global_program_info->platform);
+            (*this)(call);
+            return;
+        }
+    }
+}
+
 void ebpf_domain_t::do_load_mapfd(const Reg& dst_reg, int mapfd, bool maybe_null) {
     const EbpfMapDescriptor& desc = global_program_info->platform->get_map_descriptor(mapfd);
     const EbpfMapType& type = global_program_info->platform->get_map_type(desc.type);

src/crab/ebpf_domain.hpp

@@ -61,8 +61,10 @@ class ebpf_domain_t final {
     void operator()(const Assume&);
     void operator()(const Bin&);
     void operator()(const Call&);
+    void operator()(const Callx&);
     void operator()(const Comparable&);
     void operator()(const Exit&);
+    void operator()(const FuncConstraint&);
     void operator()(const Jmp&);
     void operator()(const LoadMapFd&);
     void operator()(const LockAdd&);

src/ebpf_vm_isa.hpp

@@ -61,7 +61,8 @@ enum {
 
     INST_OP_JA32 = ((INST_JA << 4) | INST_CLS_JMP32),
     INST_OP_JA16 = ((INST_JA << 4) | INST_CLS_JMP),
-    INST_OP_CALL = ((INST_CALL << 4) | INST_CLS_JMP),
+    INST_OP_CALL = ((INST_CALL << 4) | INST_SRC_IMM | INST_CLS_JMP),
+    INST_OP_CALLX = ((INST_CALL << 4) | INST_SRC_REG | INST_CLS_JMP),
     INST_OP_EXIT = ((INST_EXIT << 4) | INST_CLS_JMP),
 
     INST_ALU_OP_ADD  = 0x00,

src/ebpf_yaml.cpp

@@ -19,20 +19,25 @@
 using std::vector;
 using std::string;
 
+// The YAML tests for Call depend on Linux prototypes.
+// parse_instruction() in asm_parse.cpp explicitly uses
+// g_ebpf_platform_linux when parsing Call instructions
+// so we do the same here.
+
 static EbpfProgramType ebpf_get_program_type(const string& section, const string& path) {
-    return {};
+    return g_ebpf_platform_linux.get_program_type(section, path);
 }
 
 static EbpfMapType ebpf_get_map_type(uint32_t platform_specific_type) {
-    return {};
+    return g_ebpf_platform_linux.get_map_type(platform_specific_type);
 }
 
 static EbpfHelperPrototype ebpf_get_helper_prototype(int32_t n) {
-    return {};
+    return g_ebpf_platform_linux.get_helper_prototype(n);
 }
 
-static bool ebpf_is_helper_usable(int32_t n){
-    return false;
+static bool ebpf_is_helper_usable(int32_t n) {
+    return g_ebpf_platform_linux.is_helper_usable(n);
 }
 
 static void ebpf_parse_maps_section(vector<EbpfMapDescriptor>& map_descriptors, const char* data, size_t map_record_size, int map_count,
@@ -59,6 +64,7 @@ ebpf_platform_t g_platform_test = {
     .get_map_descriptor = ebpf_get_map_descriptor,
     .get_map_type = ebpf_get_map_type,
     .legacy = true,
+    .callx = true
 };
 
 static EbpfProgramType make_program_type(const string& name, ebpf_context_descriptor_t* context_descriptor) {
@@ -321,7 +327,9 @@ ConformanceTestResult run_conformance_test_case(const std::vector<uint8_t>& memo
         pre_invariant = pre_invariant + stack_contents_invariant(memory_bytes);
     }
     raw_program raw_prog{.prog = insts};
-    raw_prog.info.platform = &g_ebpf_platform_linux;
+    ebpf_platform_t platform = g_ebpf_platform_linux;
+    platform.callx = true;
+    raw_prog.info.platform = &platform;
 
     // Convert the raw program section to a set of instructions.
     std::variant<InstructionSeq, std::string> prog_or_error = unmarshal(raw_prog);

src/linux/gpl/spec_prototypes.cpp

@@ -44,6 +44,7 @@ const ebpf_context_descriptor_t g_sock_ops_descr = sock_ops_descr;
 
 static const struct EbpfHelperPrototype bpf_unspec_proto = {
     .name = "unspec",
+    .return_type = EBPF_RETURN_TYPE_UNSUPPORTED
 };
 
 const struct EbpfHelperPrototype bpf_tail_call_proto = {

src/linux/linux_platform.cpp

@@ -255,5 +255,6 @@ const ebpf_platform_t g_ebpf_platform_linux = {
     get_map_descriptor_linux,
     get_map_type_linux,
     resolve_inner_map_references_linux,
-    true // Legacy packet access instructions
+    true, // Legacy packet access instructions
+    false // No callx instructions
 };