wrap namespace prevail everywhere

Signed-off-by: Elazar Gershuni <[email protected]>

Author: elazarg

src/asm_cfg.cpp

@@ -19,6 +19,7 @@ using std::string;
 using std::to_string;
 using std::vector;
 
+namespace prevail {
 struct cfg_builder_t final {
     Program prog;
 
@@ -46,7 +47,7 @@ struct cfg_builder_t final {
         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, prevail::cfg_t::adjacent_t{});
+        prog.m_cfg.neighbours.emplace(_label, cfg_t::adjacent_t{});
         prog.m_instructions.emplace(_label, ins);
     }
 
@@ -82,8 +83,6 @@ struct cfg_builder_t final {
     }
 };
 
-using prevail::basic_block_t;
-
 /// Get the inverse of a given comparison operation.
 static Condition::Op reverse(const Condition::Op op) {
     switch (op) {
@@ -300,7 +299,7 @@ Program Program::from_sequence(const InstructionSeq& inst_seq, const program_inf
     // 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.cfg_opts.check_for_termination) {
-        const prevail::wto_t wto{builder.prog.cfg()};
+        const 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});
         });
@@ -448,7 +447,7 @@ std::map<std::string, int> collect_stats(const Program& prog) {
     return res;
 }
 
-prevail::cfg_t prevail::cfg_from_adjacency_list(const std::map<label_t, std::vector<label_t>>& adj_list) {
+cfg_t 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) {
@@ -463,3 +462,4 @@ prevail::cfg_t prevail::cfg_from_adjacency_list(const std::map<label_t, std::vec
     }
     return builder.prog.cfg();
 }
+} // namespace prevail

src/asm_files.cpp

@@ -16,6 +16,8 @@
 #include "crab_utils/num_safety.hpp"
 #include "platform.hpp"
 
+namespace prevail {
+
 template <typename T>
     requires std::is_trivially_copyable_v<T>
 static std::vector<T> vector_of(const char* data, const ELFIO::Elf_Xword size) {
@@ -646,3 +648,4 @@ std::vector<raw_program> read_elf(std::istream& input_stream, const std::string&
     program_reader.read_programs();
     return std::move(program_reader.raw_programs);
 }
+} // namespace prevail

src/asm_files.hpp

@@ -7,7 +7,7 @@
 #include <vector>
 
 #include "platform.hpp"
-
+namespace prevail {
 class UnmarshalError final : public std::runtime_error {
   public:
     explicit UnmarshalError(const std::string& what) : std::runtime_error(what) {}
@@ -23,3 +23,4 @@ std::vector<raw_program> read_elf(std::istream& input_stream, const std::string&
 void write_binary_file(std::string path, const char* data, size_t size);
 
 std::ifstream open_asm_file(std::string path);
+} // namespace prevail

src/asm_marshal.cpp

@@ -10,6 +10,8 @@
 
 using std::vector;
 
+namespace prevail {
+
 static uint8_t op(const Condition::Op op) {
     using Op = Condition::Op;
     switch (op) {
@@ -296,10 +298,10 @@ struct MarshalVisitor {
 };
 
 vector<ebpf_inst> marshal(const Instruction& ins, const pc_t pc) {
-    return std::visit(MarshalVisitor{prevail::label_to_offset16(pc), prevail::label_to_offset32(pc)}, ins);
+    return std::visit(MarshalVisitor{label_to_offset16(pc), label_to_offset32(pc)}, ins);
 }
 
-int asm_syntax::size(const Instruction& inst) {
+int size(const Instruction& inst) {
     if (const auto pins = std::get_if<Bin>(&inst)) {
         if (pins->lddw) {
             return 2;
@@ -340,3 +342,4 @@ vector<ebpf_inst> marshal(const InstructionSeq& insts) {
     }
     return res;
 }
+} // namespace prevail

src/asm_marshal.hpp

@@ -7,5 +7,9 @@
 #include "asm_syntax.hpp"
 #include "ebpf_vm_isa.hpp"
 
+namespace prevail {
+
 std::vector<ebpf_inst> marshal(const Instruction& ins, pc_t pc);
 // TODO marshal to ostream?
+
+} // namespace prevail

src/asm_ostream.cpp

@@ -18,7 +18,6 @@
 #include "platform.hpp"
 #include "spec_type_descriptors.hpp"
 
-using prevail::TypeGroup;
 using std::optional;
 using std::string;
 using std::vector;
@@ -69,8 +68,6 @@ string to_string(label_t const& label) {
     return str.str();
 }
 
-} // namespace prevail
-
 struct LineInfoPrinter {
     std::ostream& os;
     std::string previous_source_line;
@@ -108,7 +105,7 @@ void print_jump(std::ostream& o, const std::string& direction, const std::set<la
 void print_program(const Program& prog, std::ostream& os, const bool simplify, const printfunc& prefunc,
                    const printfunc& postfunc) {
     LineInfoPrinter printer{os};
-    for (const prevail::basic_block_t& bb : prevail::basic_block_t::collect_basic_blocks(prog.cfg(), simplify)) {
+    for (const basic_block_t& bb : 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";
@@ -195,7 +192,6 @@ void print_invariants(std::ostream& os, const Program& prog, const bool simplify
         });
 }
 
-namespace asm_syntax {
 std::ostream& operator<<(std::ostream& os, const ArgSingle::Kind kind) {
     switch (kind) {
     case ArgSingle::Kind::ANYTHING: return os << "uint64_t";
@@ -314,12 +310,10 @@ struct AssertionPrinterVisitor {
     }
 
     void operator()(const BoundedLoopCount& a) {
-        _os << prevail::variable_t::loop_counter(to_string(a.name)) << " < " << a.limit;
+        _os << variable_t::loop_counter(to_string(a.name)) << " < " << a.limit;
     }
 
-    static prevail::variable_t typereg(const Reg& r) {
-        return prevail::variable_t::reg(prevail::data_kind_t::types, r.v);
-    }
+    static variable_t typereg(const Reg& r) { return variable_t::reg(data_kind_t::types, r.v); }
 
     void operator()(ValidSize const& a) {
         const auto op = a.can_be_zero ? " >= " : " > ";
@@ -336,9 +330,7 @@ struct AssertionPrinterVisitor {
             << "))";
     }
 
-    void operator()(ZeroCtxOffset const& a) {
-        _os << prevail::variable_t::reg(prevail::data_kind_t::ctx_offsets, a.reg.v) << " == 0";
-    }
+    void operator()(ZeroCtxOffset const& a) { _os << variable_t::reg(data_kind_t::ctx_offsets, a.reg.v) << " == 0"; }
 
     void operator()(Comparable const& a) {
         if (a.or_r2_is_number) {
@@ -530,9 +522,7 @@ struct CommandPrinterVisitor {
         print(b.cond);
     }
 
-    void operator()(IncrementLoopCounter const& a) {
-        os_ << prevail::variable_t::loop_counter(to_string(a.name)) << "++";
-    }
+    void operator()(IncrementLoopCounter const& a) { os_ << variable_t::loop_counter(to_string(a.name)) << "++"; }
 };
 // ReSharper restore CppMemberFunctionMayBeConst
 
@@ -596,7 +586,7 @@ void print(const InstructionSeq& insts, std::ostream& out, const std::optional<c
             }
             if (const auto jmp = std::get_if<Jmp>(&ins)) {
                 if (!pc_of_label.contains(jmp->target)) {
-                    throw std::runtime_error(string("Cannot find label ") + prevail::to_string(jmp->target));
+                    throw std::runtime_error(string("Cannot find label ") + to_string(jmp->target));
                 }
                 const pc_t target_pc = pc_of_label.at(jmp->target);
                 visitor(*jmp, target_pc - static_cast<int>(pc) - 1);
@@ -609,8 +599,6 @@ void print(const InstructionSeq& insts, std::ostream& out, const std::optional<c
     }
 }
 
-} // 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 << ", "
@@ -629,4 +617,5 @@ 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;
-}
+}
+} // namespace prevail

src/asm_parse.cpp

@@ -18,10 +18,7 @@
 using std::regex;
 using std::regex_match;
 
-using prevail::linear_constraint_t;
-using prevail::linear_expression_t;
-using prevail::number_t;
-
+namespace prevail {
 #define REG R"_(\s*(r\d\d?)\s*)_"
 #define WREG R"_(\s*([wr]\d\d?)\s*)_"
 #define IMM R"_(\s*\[?([-+]?(?:0x)?[0-9a-f]+)\]?\s*)_"
@@ -279,21 +276,19 @@ static InstructionSeq parse_program(std::istream& is) {
 
 static uint8_t regnum(const std::string& s) { return static_cast<uint8_t>(boost::lexical_cast<uint16_t>(s.substr(1))); }
 
-static prevail::variable_t special_var(const std::string& s) {
+static variable_t special_var(const std::string& s) {
     if (s == "packet_size") {
-        return prevail::variable_t::packet_size();
+        return variable_t::packet_size();
     }
     if (s == "meta_offset") {
-        return prevail::variable_t::meta_offset();
+        return variable_t::meta_offset();
     }
     throw std::runtime_error(std::string() + "Bad special variable: " + s);
 }
 
 std::vector<linear_constraint_t> parse_linear_constraints(const std::set<std::string>& constraints,
-                                                          std::vector<prevail::interval_t>& numeric_ranges) {
-    using namespace prevail::dsl_syntax;
-    using prevail::regkind;
-    using prevail::variable_t;
+                                                          std::vector<interval_t>& numeric_ranges) {
+    using namespace dsl_syntax;
 
     std::vector<linear_constraint_t> res;
     for (const std::string& cst_text : constraints) {
@@ -321,8 +316,8 @@ std::vector<linear_constraint_t> parse_linear_constraints(const std::set<std::st
         } else if (regex_match(cst_text, m,
                                regex(REG DOT "type"
                                              "=" TYPE))) {
-            variable_t d = variable_t::reg(prevail::data_kind_t::types, regnum(m[1]));
-            res.push_back(d == prevail::string_to_type_encoding(m[2]));
+            variable_t d = variable_t::reg(data_kind_t::types, regnum(m[1]));
+            res.push_back(d == string_to_type_encoding(m[2]));
         } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" IMM))) {
             variable_t d = variable_t::reg(regkind(m[2]), regnum(m[1]));
             number_t value;
@@ -352,28 +347,28 @@ std::vector<linear_constraint_t> parse_linear_constraints(const std::set<std::st
         } else if (regex_match(cst_text, m,
                                regex("s" ARRAY_RANGE DOT "type"
                                      "=" TYPE))) {
-            prevail::type_encoding_t type = prevail::string_to_type_encoding(m[3]);
-            if (type == prevail::type_encoding_t::T_NUM) {
+            type_encoding_t type = string_to_type_encoding(m[3]);
+            if (type == T_NUM) {
                 numeric_ranges.emplace_back(signed_number(m[1]), signed_number(m[2]));
             } else {
                 number_t lb = signed_number(m[1]);
                 number_t ub = signed_number(m[2]);
-                variable_t d = variable_t::cell_var(prevail::data_kind_t::types, lb, ub - lb + 1);
+                variable_t d = variable_t::cell_var(data_kind_t::types, lb, ub - lb + 1);
                 res.push_back(d == type);
             }
         } else if (regex_match(cst_text, m,
                                regex("s" ARRAY_RANGE DOT "svalue"
                                      "=" IMM))) {
             number_t lb = signed_number(m[1]);
             number_t ub = signed_number(m[2]);
-            variable_t d = variable_t::cell_var(prevail::data_kind_t::svalues, lb, ub - lb + 1);
+            variable_t d = variable_t::cell_var(data_kind_t::svalues, lb, ub - lb + 1);
             res.push_back(d == signed_number(m[3]));
         } else if (regex_match(cst_text, m,
                                regex("s" ARRAY_RANGE DOT "uvalue"
                                      "=" IMM))) {
             number_t lb = signed_number(m[1]);
             number_t ub = signed_number(m[2]);
-            variable_t d = variable_t::cell_var(prevail::data_kind_t::uvalues, lb, ub - lb + 1);
+            variable_t d = variable_t::cell_var(data_kind_t::uvalues, lb, ub - lb + 1);
             res.push_back(d == unsigned_number(m[3]));
         } else {
             throw std::runtime_error(std::string("Unknown constraint: ") + cst_text);
@@ -385,9 +380,9 @@ std::vector<linear_constraint_t> parse_linear_constraints(const std::set<std::st
 // return a-b, taking account potential optional-none
 string_invariant string_invariant::operator-(const string_invariant& b) const {
     if (this->is_bottom()) {
-        return string_invariant::bottom();
+        return bottom();
     }
-    string_invariant res = string_invariant::top();
+    string_invariant res = top();
     for (const std::string& cst : this->value()) {
         if (b.is_bottom() || !b.contains(cst)) {
             res.maybe_inv->insert(cst);
@@ -436,3 +431,4 @@ std::ostream& operator<<(std::ostream& o, const string_invariant& inv) {
     o << "]";
     return o;
 }
+} // namespace prevail

src/asm_parse.hpp

@@ -6,4 +6,8 @@
 
 #include "asm_syntax.hpp"
 
+namespace prevail {
+
 Instruction parse_instruction(const std::string& line, const std::map<std::string, label_t>& label_name_to_label);
+
+}

src/asm_syntax.hpp

@@ -15,10 +15,8 @@
 #include "crab_utils/num_safety.hpp"
 #include "spec_type_descriptors.hpp"
 
-using prevail::label_t;
-
 // Assembly syntax.
-namespace asm_syntax {
+namespace prevail {
 
 /// Immediate argument.
 struct Imm {
@@ -332,7 +330,6 @@ struct ValidStore {
     constexpr bool operator==(const ValidStore&) const = default;
 };
 
-using prevail::TypeGroup;
 struct TypeConstraint {
     Reg reg;
     TypeGroup types;
@@ -368,7 +365,7 @@ std::string to_string(Instruction const& ins);
 std::ostream& operator<<(std::ostream& os, Bin::Op op);
 std::ostream& operator<<(std::ostream& os, Condition::Op op);
 
-inline std::ostream& operator<<(std::ostream& os, const Imm imm) { return os << prevail::to_signed(imm.v); }
+inline std::ostream& operator<<(std::ostream& os, const Imm imm) { return os << to_signed(imm.v); }
 inline std::ostream& operator<<(std::ostream& os, Reg const& a) { return os << "r" << gsl::narrow<int>(a.v); }
 inline std::ostream& operator<<(std::ostream& os, Value const& a) {
     if (const auto pa = std::get_if<Imm>(&a)) {
@@ -385,12 +382,9 @@ void print(const InstructionSeq& insts, std::ostream& out, const std::optional<c
 
 int size(const Instruction& inst);
 
-} // namespace asm_syntax
-
-using namespace asm_syntax;
-using prevail::pc_t;
-
 template <class... Ts>
 struct overloaded : Ts... {
     using Ts::operator()...;
 };
+
+} // namespace prevail

src/asm_unmarshal.cpp

@@ -13,6 +13,7 @@
 using std::string;
 using std::vector;
 
+namespace prevail {
 int opcode_to_width(const uint8_t opcode) {
     switch (opcode & INST_SIZE_MASK) {
     case INST_SIZE_B: return 1;
@@ -234,9 +235,9 @@ struct Unmarshaller {
         throw InvalidInstruction(pc, "unsupported immediate");
     }
 
-    static uint64_t sign_extend(const int32_t imm) { return prevail::to_unsigned(int64_t{imm}); }
+    static uint64_t sign_extend(const int32_t imm) { return to_unsigned(int64_t{imm}); }
 
-    static uint64_t zero_extend(const int32_t imm) { return uint64_t{prevail::to_unsigned(imm)}; }
+    static uint64_t zero_extend(const int32_t imm) { return uint64_t{to_unsigned(imm)}; }
 
     static auto getBinValue(const pc_t pc, const ebpf_inst inst) -> Value {
         if (inst.opcode & INST_SRC_REG) {
@@ -819,3 +820,4 @@ Call make_call(const int imm, const ebpf_platform_t& platform) {
     const program_info info{.platform = &platform};
     return Unmarshaller{notes, info}.makeCall(imm);
 }
+} // namespace prevail