move cfg-related structures to cfg/ folder

cfg/cfg.hpp is now MIT; it has very little resemblance to Crab's version, if at all.

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

Author: elazarg

CMakeLists.txt

@@ -97,6 +97,7 @@ link_directories(${Boost_LIBRARY_DIRS})
 
 file(GLOB LIB_SRC
         "./src/*.cpp"
+        "./src/cfg/*.cpp"
         "./src/crab/*.cpp"
         "./src/crab_utils/*.cpp"
         "./src/linux/gpl/spec_prototypes.cpp"

src/asm_cfg.cpp

@@ -7,11 +7,10 @@
 #include <string>
 #include <vector>
 
-#include "config.hpp"
-#include "crab/cfg.hpp"
-#include "crab/wto.hpp"
-
 #include "asm_syntax.hpp"
+#include "cfg/cfg.hpp"
+#include "cfg/wto.hpp"
+#include "config.hpp"
 #include "program.hpp"
 
 using std::optional;

src/asm_files.hpp

@@ -6,7 +6,6 @@
 #include <string>
 #include <vector>
 
-#include "asm_syntax.hpp"
 #include "platform.hpp"
 
 class UnmarshalError final : public std::runtime_error {

src/asm_ostream.cpp

@@ -7,7 +7,7 @@
 #include <vector>
 
 #include "asm_syntax.hpp"
-#include "crab/cfg.hpp"
+#include "cfg/cfg.hpp"
 #include "crab/fwd_analyzer.hpp"
 #include "crab/interval.hpp"
 #include "crab/type_encoding.hpp"

src/asm_syntax.hpp

@@ -10,7 +10,7 @@
 #include <variant>
 #include <vector>
 
-#include "crab/label.hpp"
+#include "cfg/label.hpp"
 #include "crab/type_encoding.hpp"
 #include "crab_utils/num_safety.hpp"
 #include "spec_type_descriptors.hpp"

src/assertions.cpp

@@ -6,7 +6,7 @@
 #include <vector>
 
 #include "asm_syntax.hpp"
-#include "crab/cfg.hpp"
+#include "cfg/cfg.hpp"
 #include "platform.hpp"
 
 using prevail::TypeGroup;

src/crab/cfg.hpp renamed to src/cfg/cfg.hpp

@@ -1,5 +1,5 @@
 // Copyright (c) Prevail Verifier contributors.
-// SPDX-License-Identifier: Apache-2.0
+// SPDX-License-Identifier: MIT
 #pragma once
 
 /*
@@ -10,11 +10,9 @@
 #include <memory>
 #include <ranges>
 #include <set>
-#include <variant>
 #include <vector>
 
-#include "config.hpp"
-#include "crab/label.hpp"
+#include "cfg/label.hpp"
 #include "crab_utils/debug.hpp"
 struct cfg_builder_t;
 namespace prevail {

src/crab/label.hpp renamed to src/cfg/label.hpp

@@ -7,10 +7,8 @@
 #include <climits>
 #include <functional>
 #include <limits>
-#include <ostream>
 #include <string>
 #include <utility>
-#include <vector>
 
 #include "crab_utils/num_safety.hpp"
 

src/crab/wto.cpp renamed to src/cfg/wto.cpp

@@ -1,8 +1,12 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: MIT
+#include <map>
 #include <ranges>
+#include <variant>
 
-#include "wto.hpp"
+#include "cfg/cfg.hpp"
+#include "cfg/label.hpp"
+#include "cfg/wto.hpp"
 
 // This file contains an iterative implementation of the recursive algorithm in
 // Bourdoncle, "Efficient chaotic iteration strategies with widenings", 1993

src/crab/wto.hpp renamed to src/cfg/wto.hpp

@@ -26,10 +26,11 @@
 #include <optional>
 #include <stack>
 #include <utility>
+#include <variant>
 #include <vector>
 
-#include "crab/cfg.hpp"
-#include "crab/label.hpp"
+#include "cfg/cfg.hpp"
+#include "cfg/label.hpp"
 
 namespace prevail {
 

src/crab/bitset_domain.cpp

@@ -1,8 +1,9 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: MIT
-#include "bitset_domain.hpp"
 #include <ostream>
 
+#include "bitset_domain.hpp"
+
 std::ostream& operator<<(std::ostream& o, const bitset_domain_t& b) {
     o << "Numbers -> {";
     bool first = true;

src/crab/dsl_syntax.hpp

@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
-#include "crab/cfg.hpp"
 #include "crab/linear_constraint.hpp"
 
 namespace prevail::dsl_syntax {

src/crab/ebpf_checker.cpp

@@ -11,8 +11,8 @@
 #include "asm_unmarshal.hpp"
 #include "config.hpp"
 #include "crab/array_domain.hpp"
+#include "crab/dsl_syntax.hpp"
 #include "crab/ebpf_domain.hpp"
-#include "dsl_syntax.hpp"
 #include "platform.hpp"
 #include "program.hpp"
 #include "string_constraints.hpp"

src/crab/ebpf_domain.cpp

@@ -12,8 +12,8 @@
 #include "asm_unmarshal.hpp"
 #include "config.hpp"
 #include "crab/array_domain.hpp"
+#include "crab/dsl_syntax.hpp"
 #include "crab/ebpf_domain.hpp"
-#include "dsl_syntax.hpp"
 #include "string_constraints.hpp"
 
 using prevail::NumAbsDomain;

src/crab/ebpf_transformer.cpp

@@ -13,9 +13,9 @@
 #include "asm_unmarshal.hpp"
 #include "config.hpp"
 #include "crab/array_domain.hpp"
+#include "crab/dsl_syntax.hpp"
 #include "crab/ebpf_domain.hpp"
 #include "crab_utils/num_safety.hpp"
-#include "dsl_syntax.hpp"
 #include "platform.hpp"
 #include "string_constraints.hpp"
 

src/crab/fwd_analyzer.cpp

@@ -3,11 +3,11 @@
 #include <utility>
 #include <variant>
 
+#include "cfg/cfg.hpp"
+#include "cfg/wto.hpp"
 #include "config.hpp"
-#include "crab/cfg.hpp"
 #include "crab/ebpf_domain.hpp"
 #include "crab/fwd_analyzer.hpp"
-#include "crab/wto.hpp"
 #include "program.hpp"
 
 namespace prevail {

src/crab/split_dbm.hpp

@@ -22,6 +22,7 @@
 #include <optional>
 #include <unordered_set>
 #include <utility>
+#include <variant>
 
 #include <boost/container/flat_map.hpp>
 

src/crab/thresholds.cpp

@@ -1,8 +1,8 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: Apache-2.0
 #include "crab/thresholds.hpp"
-#include "crab/cfg.hpp"
-#include "crab/label.hpp"
+#include "cfg/cfg.hpp"
+#include "cfg/label.hpp"
 
 namespace prevail {
 

src/crab/thresholds.hpp

@@ -5,12 +5,9 @@
 #include <climits>
 #include <map>
 
-#include <boost/range/iterator_range.hpp>
-
-#include "crab/cfg.hpp"
+#include "cfg/cfg.hpp"
+#include "cfg/wto.hpp"
 #include "crab/interval.hpp"
-#include "crab/linear_constraint.hpp"
-#include "crab/wto.hpp"
 #include "crab_utils/debug.hpp"
 
 namespace prevail {

src/crab/type_domain.cpp

@@ -13,7 +13,7 @@
 #include "crab/type_encoding.hpp"
 #include "crab/variable.hpp"
 #include "crab_utils/debug.hpp"
-#include "dsl_syntax.hpp"
+#include "crab/dsl_syntax.hpp"
 
 namespace prevail {
 

src/crab/type_domain.hpp

@@ -7,13 +7,11 @@
 #include <functional>
 #include <optional>
 
+#include "asm_syntax.hpp" // for Reg
 #include "crab/array_domain.hpp"
-#include "crab/split_dbm.hpp"
 #include "crab/type_encoding.hpp"
 #include "crab/variable.hpp"
 
-#include "asm_syntax.hpp" // for Reg
-
 namespace prevail {
 
 struct reg_pack_t {

src/crab/var_factory.cpp

@@ -4,7 +4,7 @@
  * Factories for variable names.
  */
 
-#include "crab/label.hpp"
+#include "cfg/label.hpp"
 #include "crab/variable.hpp"
 #include "crab_utils/lazy_allocator.hpp"
 

src/crab_utils/debug.cpp

@@ -1,6 +1,6 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: Apache-2.0
-#include "debug.hpp"
+#include "crab_utils/debug.hpp"
 
 namespace prevail {
 bool CrabLogFlag = false;

src/crab_utils/num_big.hpp

@@ -9,8 +9,8 @@
 
 #include <boost/multiprecision/cpp_int.hpp>
 
+#include "crab_utils/debug.hpp"
 #include "crab_utils/num_safety.hpp"
-#include "debug.hpp"
 
 using boost::multiprecision::cpp_int;
 

src/linux/gpl/spec_type_descriptors.hpp

@@ -1,10 +1,4 @@
 #pragma once
-#include <cassert>
-#include <string>
-#include <unordered_map>
-#include <vector>
-
-#include "ebpf_vm_isa.hpp"
 
 constexpr int NMAPS = 64;
 constexpr int NONMAPS = 5;

src/main/linux_verifier.hpp

@@ -3,7 +3,6 @@
 #pragma once
 
 #include "platform.hpp"
-#include <iostream>
 
 #if __linux__
 

src/platform.hpp

@@ -7,6 +7,7 @@
 // can use to call platform-specific functions.
 
 #include "../external/bpf_conformance/include/bpf_conformance.h"
+
 #include "config.hpp"
 #include "helpers.hpp"
 #include "spec_type_descriptors.hpp"

src/program.hpp

@@ -5,11 +5,11 @@
 #include <map>
 #include <vector>
 
-#include "crab/cfg.hpp"
-#include "crab/label.hpp"
-#include "crab_utils/debug.hpp"
-
 #include "asm_syntax.hpp"
+#include "cfg/cfg.hpp"
+#include "cfg/label.hpp"
+#include "config.hpp"
+#include "crab_utils/debug.hpp"
 
 class Program {
     friend struct cfg_builder_t;

src/spec_type_descriptors.hpp

@@ -2,13 +2,13 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
-#include "ebpf_base.h"
-#include "ebpf_vm_isa.hpp"
 #include <map>
 #include <string>
 #include <vector>
 
 #include "crab_utils/lazy_allocator.hpp"
+#include "ebpf_base.h"
+#include "ebpf_vm_isa.hpp"
 
 enum class EbpfMapValueType { ANY, MAP, PROGRAM };
 

src/test/test_wto.cpp

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: MIT
 #include <catch2/catch_all.hpp>
 
-#include "crab/cfg.hpp"
-#include "crab/wto.hpp"
+#include "cfg/cfg.hpp"
+#include "cfg/wto.hpp"
 
 using prevail::label_t;
 using prevail::wto_t;