C++23: Replace variant<T, string> with expected

CMakeLists.txt

@@ -249,7 +249,17 @@ install(TARGETS prevail libbtf GSL
 install(DIRECTORY "${prevail_source_dir}/src/"
   DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/prevail"
   FILES_MATCHING PATTERN "*.hpp" PATTERN "*.h"
-  PATTERN "test/*" EXCLUDE
+  PATTERN "test" EXCLUDE
+  PATTERN "ir" EXCLUDE
+)
+
+# ir/ holds both public and internal headers; list the public ones explicitly.
+install(FILES
+  "${prevail_source_dir}/src/ir/marshal.hpp"
+  "${prevail_source_dir}/src/ir/parse.hpp"
+  "${prevail_source_dir}/src/ir/program.hpp"
+  "${prevail_source_dir}/src/ir/syntax.hpp"
+  DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/prevail/ir"
 )
 
 # Install convenience header to top-level include/

docs/architecture.md

@@ -19,6 +19,7 @@ ELF Binary -> Unmarshal -> Build CFG -> Abstract Interpretation -> Result
 3. **Semantic Translation**: Map hardware opcodes to semantic IR
 
 The unmarshaller handles:
+
 - Instruction decoding (opcode, registers, immediate values)
 - Wide instruction handling (64-bit immediates span two instructions)
 - Endianness conversion
@@ -36,6 +37,7 @@ The CFG builder transforms the linear instruction sequence into a control flow g
 4. **Function Inlining**: Inline local function calls with stack frame prefixes
 
 Key transformations:
+
 - Conditional jumps split into two paths with explicit `Assume` instructions
 - Loop heads are identified for widening
 - Exit nodes connect to a special exit label
@@ -57,6 +59,7 @@ The core verification uses forward abstract interpretation:
 **Files**: `src/result.cpp`
 
 The analysis produces:
+
 - **Invariants**: Pre/post states at each program point
 - **Errors**: List of safety violations
 - **Exit value**: Range of possible return values in R0
@@ -81,24 +84,24 @@ EbpfDomain = TypeToNumDomain × ArrayDomain
 
 Implements transfer functions for each instruction type:
 
-| Instruction | Semantic Effect |
-|-------------|-----------------|
-| `Bin` (ADD, SUB, ...) | Update numeric constraints |
-| `Mem` (load/store) | Read/write array domain |
-| `Call` | Apply helper function contracts |
-| `Assume` | Refine domain with branch condition |
-| `Jmp` | No state change (control flow only) |
+| Instruction           | Semantic Effect                     |
+|-----------------------|-------------------------------------|
+| `Bin` (ADD, SUB, ...) | Update numeric constraints          |
+| `Mem` (load/store)    | Read/write array domain             |
+| `Call`                | Apply helper function contracts     |
+| `Assume`              | Refine domain with branch condition |
+| `Jmp`                 | No state change (control flow only) |
 
 ### EbpfChecker (Assertion Verification)
 
 Verifies safety properties by checking domain entailment:
 
-| Assertion | Property Checked |
-|-----------|------------------|
-| `ValidAccess` | Memory access within bounds |
-| `ValidStore` | Type-correct store operation |
-| `ValidDivisor` | Non-zero divisor |
-| `BoundedLoopCount` | Loop iteration limit |
+| Assertion          | Property Checked             |
+|--------------------|------------------------------|
+| `ValidAccess`      | Memory access within bounds  |
+| `ValidStore`       | Type-correct store operation |
+| `ValidDivisor`     | Non-zero divisor             |
+| `BoundedLoopCount` | Loop iteration limit         |
 
 ## Data Flow
 
@@ -141,6 +144,7 @@ Verifies safety properties by checking domain entailment:
 ### 1. Forward Analysis
 
 Prevail uses forward (rather than backward) analysis because:
+
 - eBPF programs have a single entry point
 - Memory safety depends on tracking pointer provenance from entry
 - Type information flows naturally forward
@@ -149,20 +153,23 @@ Prevail uses forward (rather than backward) analysis because:
 ### 2. Composite Domain
 
 The domain hierarchy enables:
+
 - **Type-guided precision**: Different numeric tracking per pointer type
 - **Efficient joins**: Type mismatches detected early
 - **Modular extension**: New pointer types can be added
 
 ### 3. Weak Topological Ordering
 
 WTO-based iteration provides:
+
 - **Efficient convergence**: Widening applied only at loop heads
 - **Nested loop handling**: Inner loops stabilize before outer
 - **Deterministic order**: Reproducible analysis results
 
 ### 4. Assertion-Based Checking
 
 Separating assertions from semantics enables:
+
 - **Modular safety properties**: Easy to add new checks
 - **Precise error reporting**: Knows exactly which property failed
 - **Configurable strictness**: Can enable/disable specific checks
@@ -178,6 +185,7 @@ Separating assertions from semantics enables:
 ```
 
 Options:
+
 - `-q`/`--quiet`: No stdout output, exit code only
 - `--cfg`: Print control-flow graph and exit
 - `--failure-slice`: Print causal trace for failures
@@ -190,20 +198,18 @@ Options:
 ```cpp
 #include "ebpf_verifier.hpp"
 
-// Load and verify
 auto raw_progs = read_elf(filename, section, options, platform);
-auto prog = Program::from_sequence(instructions, info, options);
-auto result = analyze(prog);
-
-// Check result
-if (!result.failed) {
+std::vector<std::vector<std::string>> notes;
+auto prog = Program::from_raw(raw_progs.front(), notes, options);
+if (prog && verify(*prog)) {
     // Program is safe
 }
 ```
 
 ## Thread Safety
 
 The verifier uses thread-local storage for:
+
 - **Variable registry**: Maps variable names to indices
 - **Global program counter**: Tracks current instruction during analysis
 

src/ebpf_verifier.hpp

@@ -5,6 +5,5 @@
 #include "config.hpp"
 #include "io/elf_loader.hpp"
 #include "ir/program.hpp"
-#include "ir/unmarshal.hpp"
 #include "platform.hpp"
 #include "verifier.hpp"

src/ir/cfg_builder.cpp

@@ -14,6 +14,7 @@
 #include "config.hpp"
 #include "ir/program.hpp"
 #include "ir/syntax.hpp"
+#include "ir/unmarshal.hpp"
 #include "platform.hpp"
 
 using std::optional;
@@ -715,6 +716,16 @@ Program Program::from_sequence(const InstructionSeq& inst_seq, const ProgramInfo
     return std::move(builder.prog);
 }
 
+std::optional<Program> Program::from_raw(const RawProgram& raw_prog, std::vector<std::vector<std::string>>& notes,
+                                         const ebpf_verifier_options_t& options) {
+    auto inst_seq = unmarshal(raw_prog, notes, options);
+    if (!inst_seq.has_value()) {
+        notes.push_back({std::move(inst_seq).error()});
+        return std::nullopt;
+    }
+    return from_sequence(*inst_seq, raw_prog.info, options);
+}
+
 std::set<BasicBlock> BasicBlock::collect_basic_blocks(const Cfg& cfg, const bool simplify) {
     if (!simplify) {
         std::set<BasicBlock> res;

src/ir/program.hpp

@@ -3,13 +3,17 @@
 #pragma once
 
 #include <map>
+#include <optional>
+#include <ostream>
+#include <string>
 #include <vector>
 
 #include "cfg/cfg.hpp"
 #include "cfg/label.hpp"
 #include "config.hpp"
 #include "crab_utils/debug.hpp"
 #include "ir/syntax.hpp"
+#include "spec/type_descriptors.hpp"
 
 namespace prevail {
 class Program {
@@ -55,6 +59,12 @@ class Program {
 
     static Program from_sequence(const InstructionSeq& inst_seq, const ProgramInfo& info,
                                  const ebpf_verifier_options_t& options);
+
+    /// Build a Program directly from a raw (ELF-bytecode) representation.
+    /// On failure returns std::nullopt and appends the error message to `notes`
+    /// (the same vector that collects unmarshal warnings).
+    static std::optional<Program> from_raw(const RawProgram& raw_prog, std::vector<std::vector<std::string>>& notes,
+                                           const ebpf_verifier_options_t& options);
 };
 
 class InvalidControlFlow final : public std::runtime_error {
@@ -67,4 +77,9 @@ std::vector<Assertion> get_assertions(const Instruction& ins, const ProgramInfo&
 
 void print_program(const Program& prog, std::ostream& os, bool simplify);
 void print_dot(const Program& prog, const std::string& outfile);
+
+/// Write a textual disassembly of `raw_prog` to `out`. On failure writes the
+/// error message to `out` and returns false.
+bool disassemble(const RawProgram& raw_prog, const ebpf_verifier_options_t& options, std::ostream& out,
+                 const std::optional<Label>& label_to_print = {}, bool print_line_info = false);
 } // namespace prevail

src/ir/syntax.hpp

@@ -457,7 +457,7 @@ inline std::ostream& operator<<(std::ostream& os, Value const& a) {
 std::ostream& operator<<(std::ostream& os, const Assertion& a);
 std::string to_string(const Assertion& constraint);
 
-void print(const InstructionSeq& insts, std::ostream& out, const std::optional<const Label>& label_to_print,
+void print(const InstructionSeq& insts, std::ostream& out, const std::optional<Label>& label_to_print,
            bool print_line_info = false);
 
 int size(const Instruction& inst);

src/ir/unmarshal.cpp

@@ -1,6 +1,7 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: MIT
 #include <cassert>
+#include <expected>
 #include <iostream>
 #include <string>
 #include <vector>
@@ -782,8 +783,7 @@ struct Unmarshaller {
         }
     }
 
-    vector<LabeledInstruction> unmarshal(vector<EbpfInst> const& insts,
-                                         const prevail::ebpf_verifier_options_t& options) {
+    vector<LabeledInstruction> unmarshal(vector<EbpfInst> const& insts, const ebpf_verifier_options_t& options) {
         options.validate();
         subprogram_stack_size = options.subprogram_stack_size;
         vector<LabeledInstruction> prog;
@@ -882,20 +882,20 @@ struct Unmarshaller {
     }
 };
 
-std::variant<InstructionSeq, std::string> unmarshal(const RawProgram& raw_prog, vector<vector<string>>& notes,
-                                                    const prevail::ebpf_verifier_options_t& options) {
+std::expected<InstructionSeq, std::string> unmarshal(const RawProgram& raw_prog, vector<vector<string>>& notes,
+                                                     const ebpf_verifier_options_t& options) {
     thread_local_program_info = raw_prog.info;
     try {
         return Unmarshaller{notes, raw_prog.info}.unmarshal(raw_prog.prog, options);
     } catch (InvalidInstruction& arg) {
         std::ostringstream ss;
         ss << arg.pc << ": " << arg.what() << "\n";
-        return ss.str();
+        return std::unexpected(ss.str());
     }
 }
 
-std::variant<InstructionSeq, std::string> unmarshal(const RawProgram& raw_prog,
-                                                    const prevail::ebpf_verifier_options_t& options) {
+std::expected<InstructionSeq, std::string> unmarshal(const RawProgram& raw_prog,
+                                                     const ebpf_verifier_options_t& options) {
     vector<vector<string>> notes;
     return unmarshal(raw_prog, notes, options);
 }

src/ir/unmarshal.hpp

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
+#include <expected>
 #include <string>
-#include <variant>
 #include <vector>
 
 #include "ir/syntax.hpp"
@@ -17,13 +17,14 @@ namespace prevail {
  *
  *  \param raw_prog is the input program to parse.
  *  \param[out] notes is a vector for storing errors and warnings.
+ *  \param options unmarshalling options
  *  \return a sequence of instructions if successful, an error string otherwise.
  */
-std::variant<InstructionSeq, std::string> unmarshal(const RawProgram& raw_prog,
-                                                    std::vector<std::vector<std::string>>& notes,
-                                                    const prevail::ebpf_verifier_options_t& options);
-std::variant<InstructionSeq, std::string> unmarshal(const RawProgram& raw_prog,
-                                                    const prevail::ebpf_verifier_options_t& options);
+std::expected<InstructionSeq, std::string> unmarshal(const RawProgram& raw_prog,
+                                                     std::vector<std::vector<std::string>>& notes,
+                                                     const ebpf_verifier_options_t& options);
+std::expected<InstructionSeq, std::string> unmarshal(const RawProgram& raw_prog,
+                                                     const ebpf_verifier_options_t& options);
 
 Call make_call(int imm, const ebpf_platform_t& platform);
 } // namespace prevail

src/main.cpp

@@ -4,8 +4,13 @@
 #include <ranges>
 #include <vector>
 
-#include "ebpf_verifier.hpp"
+#include "config.hpp"
 #include "io/elf_loader.hpp"
+#include "ir/program.hpp"
+#include "ir/unmarshal.hpp"
+#include "platform.hpp"
+#include "result.hpp"
+#include "verifier.hpp"
 
 // Avoid affecting other headers by macros.
 #include <CLI11/CLI11.hpp>
@@ -201,16 +206,15 @@ int main(int argc, char** argv) {
     const RawProgram& raw_prog = raw_progs.back();
 
     // Convert the raw program section to a set of instructions.
-    std::variant<InstructionSeq, std::string> prog_or_error = unmarshal(raw_prog, ebpf_verifier_options);
-    if (auto prog = std::get_if<string>(&prog_or_error)) {
-        std::cout << "unmarshaling error at " << *prog << "\n";
+    const auto inst_seq = unmarshal(raw_prog, ebpf_verifier_options);
+    if (!inst_seq.has_value()) {
+        std::cout << "unmarshaling error at " << inst_seq.error() << "\n";
         return 1;
     }
 
-    auto& inst_seq = std::get<InstructionSeq>(prog_or_error);
     if (!asmfile.empty()) {
         std::ofstream out{asmfile};
-        print(inst_seq, out, {});
+        print(*inst_seq, out, {});
         print_map_descriptors(thread_local_program_info->map_descriptors, out);
     }
 
@@ -226,7 +230,7 @@ int main(int argc, char** argv) {
             }
         }
         const auto verbosity = ebpf_verifier_options.verbosity_opts;
-        const Program prog = Program::from_sequence(inst_seq, raw_prog.info, ebpf_verifier_options);
+        const Program prog = Program::from_sequence(*inst_seq, raw_prog.info, ebpf_verifier_options);
 
         if (!dotfile.empty()) {
             print_dot(prog, dotfile);

src/printing.cpp

@@ -13,7 +13,9 @@
 #include "crab/interval.hpp"
 #include "crab/type_encoding.hpp"
 #include "crab/var_registry.hpp"
+#include "ir/program.hpp"
 #include "ir/syntax.hpp"
+#include "ir/unmarshal.hpp"
 #include "platform.hpp"
 #include "spec/function_prototypes.hpp"
 #include "verifier.hpp"
@@ -670,7 +672,7 @@ auto get_labels(const InstructionSeq& insts) {
     return pc_of_label;
 }
 
-void print(const InstructionSeq& insts, std::ostream& out, const std::optional<const Label>& label_to_print,
+void print(const InstructionSeq& insts, std::ostream& out, const std::optional<Label>& label_to_print,
            const bool print_line_info) {
     const auto pc_of_label = get_labels(insts);
     Pc pc = 0;
@@ -725,6 +727,17 @@ void print_map_descriptors(const std::vector<EbpfMapDescriptor>& descriptors, st
     }
 }
 
+bool disassemble(const RawProgram& raw_prog, const ebpf_verifier_options_t& options, std::ostream& out,
+                 const std::optional<Label>& label_to_print, const bool print_line_info) {
+    auto inst_seq = unmarshal(raw_prog, options);
+    if (!inst_seq.has_value()) {
+        out << "unmarshaling error at " << inst_seq.error();
+        return false;
+    }
+    print(*inst_seq, out, label_to_print, print_line_info);
+    return true;
+}
+
 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";