Prepare to use GSL, and particularly gsl::narrow

CMakeLists.txt

@@ -1,70 +1,81 @@
 # Copyright (c) Prevail Verifier contributors.
 # SPDX-License-Identifier: MIT
-cmake_minimum_required(VERSION 3.10)
+cmake_minimum_required(VERSION 3.14)
 project(ebpf_verifier)
 
 include(FetchContent)
-FetchContent_Declare(
-  Catch2
-  GIT_REPOSITORY https://github.com/catchorg/Catch2.git
-  GIT_TAG        fa43b77429ba76c462b1898d6cd2f2d7a9416b14 # v3.7.1
+
+FetchContent_Declare(GSL
+        GIT_REPOSITORY "https://github.com/microsoft/GSL"
+        GIT_TAG "v4.0.0"
+        GIT_SHALLOW ON
+)
+FetchContent_MakeAvailable(GSL)
+get_target_property(GSL_INCLUDE_DIRS Microsoft.GSL::GSL INTERFACE_INCLUDE_DIRECTORIES)
+
+FetchContent_Declare(Catch2
+        GIT_REPOSITORY "https://github.com/catchorg/Catch2.git"
+        GIT_TAG "v3.7.1"
+        GIT_SHALLOW ON
 )
 FetchContent_MakeAvailable(Catch2)
 
 if (IS_DIRECTORY "${PROJECT_SOURCE_DIR}/.git")
-  # Install Git pre-commit hook
-  file(COPY scripts/pre-commit scripts/commit-msg
-       DESTINATION "${PROJECT_SOURCE_DIR}/.git/hooks")
+    # Install Git pre-commit hook
+    file(COPY scripts/pre-commit scripts/commit-msg
+            DESTINATION "${PROJECT_SOURCE_DIR}/.git/hooks")
 endif ()
 
 if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU" OR
-    "${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
-  find_package(yaml-cpp REQUIRED)
-  find_package(Boost REQUIRED)
-  set(CMAKE_CXX_STANDARD 20)
+        "${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
+    find_package(yaml-cpp REQUIRED)
+    find_package(Boost REQUIRED)
+    set(CMAKE_CXX_STANDARD 20)
+    set(CMAKE_CXX_STANDARD_REQUIRED ON)
 elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
-  list(APPEND CMAKE_CONFIGURATION_TYPES FuzzerDebug)
-  list(REMOVE_DUPLICATES CMAKE_CONFIGURATION_TYPES)
-  set(CMAKE_CONFIGURATION_TYPES "${CMAKE_CONFIGURATION_TYPES}" CACHE STRING
-      "Add the configurations that we need"
-      FORCE)
-  set(CMAKE_EXE_LINKER_FLAGS_FUZZERDEBUG "${CMAKE_EXE_LINKER_FLAGS_DEBUG}")
-  set(CMAKE_SHARED_LINKER_FLAGS_FUZZERDEBUG "${CMAKE_SHARED_LINKER_FLAGS_DEBUG}")
-  set(CMAKE_C_FLAGS_FUZZERDEBUG "${CMAKE_C_FLAGS_DEBUG} /fsanitize=address /fsanitize=fuzzer /fsanitize-coverage=inline-bool-flag /fsanitize-coverage=edge /fsanitize-coverage=trace-cmp /fsanitize-coverage=trace-div /ZH:SHA_256")
-  set(CMAKE_CXX_FLAGS_FUZZERDEBUG "${CMAKE_CXX_FLAGS_DEBUG} /fsanitize=address /fsanitize=fuzzer /fsanitize-coverage=inline-bool-flag /fsanitize-coverage=edge /fsanitize-coverage=trace-cmp /fsanitize-coverage=trace-div /ZH:SHA_256")
-
-  find_program(NUGET nuget)
-  if (NOT NUGET)
-    message("ERROR: You must first install nuget.exe from https://www.nuget.org/downloads")
-  else ()
-    execute_process(COMMAND ${NUGET} install "Boost" -Version 1.81.0 -ExcludeVersion -OutputDirectory ${CMAKE_BINARY_DIR}/packages)
-    set(BOOST_VERSION 1.81.0)
-  endif()
-  set(Boost_INCLUDE_DIRS ${CMAKE_BINARY_DIR}/packages/boost/lib/native/include)
-  set(Boost_LIBRARY_DIRS ${CMAKE_BINARY_DIR}/packages/boost_filesystem-vc143/lib/native)
-
-  # MSVC's "std:c++20" option is the current standard that supports all the C++17
-  # features we use. However, cmake can't deal with that here, so we set it below.
-
-  set(EXTERNAL_INSTALL_LOCATION ${CMAKE_BINARY_DIR}/packages/yaml-cpp)
-  include(ExternalProject)
-  ExternalProject_Add(yaml-cpp
-          GIT_REPOSITORY https://github.com/jbeder/yaml-cpp.git
-          GIT_TAG "yaml-cpp-0.7.0"
-          GIT_SHALLOW true
-          CMAKE_ARGS -DCMAKE_INSTALL_PREFIX=${EXTERNAL_INSTALL_LOCATION}
-                     -DYAML_MSVC_SHARED_RT=ON
-                     -DYAML_CPP_BUILD_TESTS=OFF
-                     -DYAML_CPP_BUILD_TOOLS=OFF
-          )
-  set(YAML_CPP_LIBRARIES ${EXTERNAL_INSTALL_LOCATION}/lib/yaml-cpp$<$<CONFIG:DEBUG>:d>.lib)
-  set(YAML_CPP_INCLUDE_DIRS ${EXTERNAL_INSTALL_LOCATION}/include/)
+    list(APPEND CMAKE_CONFIGURATION_TYPES FuzzerDebug)
+    list(REMOVE_DUPLICATES CMAKE_CONFIGURATION_TYPES)
+    set(CMAKE_CONFIGURATION_TYPES "${CMAKE_CONFIGURATION_TYPES}" CACHE STRING
+            "Add the configurations that we need"
+            FORCE)
+    set(CMAKE_EXE_LINKER_FLAGS_FUZZERDEBUG "${CMAKE_EXE_LINKER_FLAGS_DEBUG}")
+    set(CMAKE_SHARED_LINKER_FLAGS_FUZZERDEBUG "${CMAKE_SHARED_LINKER_FLAGS_DEBUG}")
+    set(CMAKE_C_FLAGS_FUZZERDEBUG "${CMAKE_C_FLAGS_DEBUG} /fsanitize=address /fsanitize=fuzzer /fsanitize-coverage=inline-bool-flag /fsanitize-coverage=edge /fsanitize-coverage=trace-cmp /fsanitize-coverage=trace-div /ZH:SHA_256")
+    set(CMAKE_CXX_FLAGS_FUZZERDEBUG "${CMAKE_CXX_FLAGS_DEBUG} /fsanitize=address /fsanitize=fuzzer /fsanitize-coverage=inline-bool-flag /fsanitize-coverage=edge /fsanitize-coverage=trace-cmp /fsanitize-coverage=trace-div /ZH:SHA_256")
+
+    find_program(NUGET nuget)
+    if (NOT NUGET)
+        message("ERROR: You must first install nuget.exe from https://www.nuget.org/downloads")
+    else ()
+        execute_process(COMMAND ${NUGET} install "Boost" -Version 1.81.0 -ExcludeVersion -OutputDirectory ${CMAKE_BINARY_DIR}/packages)
+        set(BOOST_VERSION 1.81.0)
+    endif ()
+    set(Boost_INCLUDE_DIRS ${CMAKE_BINARY_DIR}/packages/boost/lib/native/include)
+    set(Boost_LIBRARY_DIRS ${CMAKE_BINARY_DIR}/packages/boost_filesystem-vc143/lib/native)
+
+    # MSVC's "std:c++20" option is the current standard that supports all the C++17
+    # features we use. However, cmake can't deal with that here, so we set it below.
+
+    set(EXTERNAL_INSTALL_LOCATION ${CMAKE_BINARY_DIR}/packages/yaml-cpp)
+    include(ExternalProject)
+    ExternalProject_Add(yaml-cpp
+            GIT_REPOSITORY https://github.com/jbeder/yaml-cpp.git
+            GIT_TAG "yaml-cpp-0.7.0"
+            GIT_SHALLOW true
+            CMAKE_ARGS -DCMAKE_INSTALL_PREFIX=${EXTERNAL_INSTALL_LOCATION}
+            -DYAML_MSVC_SHARED_RT=ON
+            -DYAML_CPP_BUILD_TESTS=OFF
+            -DYAML_CPP_BUILD_TOOLS=OFF
+    )
+    set(YAML_CPP_LIBRARIES ${EXTERNAL_INSTALL_LOCATION}/lib/yaml-cpp$<$<CONFIG:DEBUG>:d>.lib)
+    set(YAML_CPP_INCLUDE_DIRS ${EXTERNAL_INSTALL_LOCATION}/include/)
 endif ()
 
 include_directories(./external)
 include_directories(./external/bpf_conformance/external/elfio)
 include_directories(./src)
 include_directories(./external/libbtf)
+include_directories(${GSL_INCLUDE_DIRS})
 include_directories(${Boost_INCLUDE_DIRS})
 include_directories(${YAML_CPP_INCLUDE_DIRS})
 link_directories(${Boost_LIBRARY_DIRS})
@@ -73,31 +84,30 @@ file(GLOB LIB_SRC
         "./src/*.cpp"
         "./src/crab/*.cpp"
         "./src/crab_utils/*.cpp"
-        "./src/linux/gpl/*.cpp"
+        "./src/linux/gpl/spec_prototypes.cpp"
         "./src/linux/linux_platform.cpp"
-        )
+)
 
 file(GLOB ALL_TEST
-        "./src/test/test.cpp"
         "./src/test/test_conformance.cpp"
         "./src/test/test_marshal.cpp"
         "./src/test/test_print.cpp"
         "./src/test/test_verify.cpp"
         "./src/test/test_wto.cpp"
         "./src/test/test_yaml.cpp"
-        )
+)
 
 if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU" OR
-    "${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang")
-  set(COMMON_FLAGS -Wall -Wfatal-errors -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8)
+        "${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang")
+    set(COMMON_FLAGS -Wall -Wfatal-errors -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8)
 
-  set(RELEASE_FLAGS -O2 -flto=auto -ffat-lto-objects)
+    set(RELEASE_FLAGS -O2 -flto=auto -ffat-lto-objects)
 
-  set(DEBUG_FLAGS -O0 -g3 -fno-omit-frame-pointer)
+    set(DEBUG_FLAGS -O0 -g3 -fno-omit-frame-pointer)
 
-  set(SANITIZE_FLAGS -fsanitize=address -O1 -fno-omit-frame-pointer)
+    set(SANITIZE_FLAGS -fsanitize=address -O1 -fno-omit-frame-pointer)
 elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} /std:c++20")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} /std:c++20")
 endif ()
 
 add_library(ebpfverifier ${LIB_SRC})
@@ -107,6 +117,8 @@ add_executable(tests ${ALL_TEST})
 add_executable(run_yaml src/main/run_yaml.cpp)
 add_executable(conformance_check src/test/conformance_check.cpp)
 
+target_include_directories(ebpfverifier PRIVATE ${GSL_INCLUDE_DIRS})
+
 set_target_properties(check
         PROPERTIES
         RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/..")
@@ -141,6 +153,14 @@ add_subdirectory("external/libbtf")
 set(ebpfverifier_GUID_CMAKE "7d5b4e68-c0fa-3f86-9405-f6400219b440" CACHE INTERNAL "Project GUID")
 set(yaml-cpp_GUID_CMAKE "98d56b8a-d8eb-3d98-b8ee-c83696b4d58a" CACHE INTERNAL "Project GUID")
 
+set(THREADS_PREFER_PTHREAD_FLAG ON)
+find_package(Threads REQUIRED)
+
+target_link_libraries(ebpfverifier PRIVATE ${YAML_CPP_LIBRARIES})
+target_link_libraries(ebpfverifier PRIVATE libbtf)
+target_link_libraries(ebpfverifier PRIVATE Microsoft.GSL::GSL)
+target_compile_options(ebpfverifier PRIVATE ${COMMON_FLAGS})
+
 target_compile_options(check PRIVATE ${COMMON_FLAGS})
 target_compile_options(check PUBLIC "$<$<CONFIG:DEBUG>:${DEBUG_FLAGS}>")
 target_compile_options(check PUBLIC "$<$<CONFIG:RELEASE>:${RELEASE_FLAGS}>")
@@ -155,16 +175,9 @@ target_compile_options(tests PUBLIC "$<$<CONFIG:SANITIZE>:${SANITIZE_FLAGS}>")
 target_link_libraries(tests PRIVATE ebpfverifier)
 target_link_libraries(tests PRIVATE bpf_conformance)
 target_link_libraries(tests PRIVATE ${CMAKE_DL_LIBS})
-
-set(THREADS_PREFER_PTHREAD_FLAG ON)
-find_package(Threads REQUIRED)
-
 target_link_libraries(tests PRIVATE Threads::Threads)
 target_link_libraries(tests PRIVATE Catch2::Catch2WithMain)
 
-target_link_libraries(ebpfverifier PRIVATE ${YAML_CPP_LIBRARIES})
-target_link_libraries(ebpfverifier PRIVATE libbtf)
-target_compile_options(ebpfverifier PRIVATE ${COMMON_FLAGS})
-
 target_link_libraries(run_yaml PRIVATE ebpfverifier)
+
 target_link_libraries(conformance_check PRIVATE ebpfverifier)

src/crab/array_domain.cpp

@@ -489,14 +489,14 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
         // We can only split a singleton size.
         return;
     }
-    auto size = static_cast<unsigned int>(*n_bytes);
-    offset_t o(static_cast<index_t>(*n));
+    auto size = n_bytes->narrow<unsigned int>();
+    offset_t o(n->narrow<index_t>());
 
     std::vector<cell_t> cells = offset_map.get_overlap_cells(o, size);
     for (cell_t const& c : cells) {
         interval_t intv = c.to_interval();
-        int cell_start_index = static_cast<int>(*intv.lb().number());
-        int cell_end_index = static_cast<int>(*intv.ub().number());
+        int cell_start_index = intv.lb().narrow<int>();
+        int cell_end_index = intv.ub().narrow<int>();
 
         if (!this->num_bytes.all_num(cell_start_index, cell_end_index + 1) ||
             cell_end_index + 1UL < cell_start_index + sizeof(int64_t)) {
@@ -532,9 +532,9 @@ static std::optional<std::pair<offset_t, unsigned>> kill_and_find_var(NumAbsDoma
     if (std::optional<number_t> n = ii.singleton()) {
         interval_t i_elem_size = inv.eval_interval(elem_size);
         if (auto n_bytes = i_elem_size.singleton()) {
-            auto size = static_cast<unsigned int>(*n_bytes);
+            auto size = n_bytes->narrow<unsigned int>();
             // -- Constant index: kill overlapping cells
-            offset_t o(static_cast<index_t>(*n));
+            offset_t o(n->narrow<index_t>());
             cells = offset_map.get_overlap_cells(o, size);
             res = std::make_pair(o, size);
         }
@@ -576,7 +576,7 @@ bool array_domain_t::all_num(const NumAbsDomain& inv, const linear_expression_t&
         return true;
     }
 
-    return this->num_bytes.all_num(static_cast<int32_t>(*min_lb), static_cast<int32_t>(*max_ub));
+    return this->num_bytes.all_num(min_lb->narrow<int32_t>(), max_ub->narrow<int32_t>());
 }
 
 // Get the number of bytes, starting at offset, that are known to be numbers.
@@ -586,8 +586,8 @@ int array_domain_t::min_all_num_size(const NumAbsDomain& inv, const variable_t o
     if (!min_lb || !max_ub || !min_lb->fits<int32_t>() || !max_ub->fits<int32_t>()) {
         return 0;
     }
-    const auto lb = static_cast<int>(min_lb.value());
-    const auto ub = static_cast<int>(max_ub.value());
+    const auto lb = min_lb->narrow<int>();
+    const auto ub = max_ub->narrow<int>();
     return std::max(0, this->num_bytes.all_num_width(lb) - (ub - lb));
 }
 
@@ -635,7 +635,7 @@ std::optional<linear_expression_t> array_domain_t::load(const NumAbsDomain& inv,
     interval_t ii = inv.eval_interval(i);
     if (std::optional<number_t> n = ii.singleton()) {
         offset_map_t& offset_map = lookup_array_map(kind);
-        int64_t k = static_cast<int64_t>(*n);
+        int64_t k = n->narrow<int64_t>();
         if (kind == data_kind_t::types) {
             auto [only_num, only_non_num] = num_bytes.uniformity(k, width);
             if (only_num) {
@@ -730,9 +730,9 @@ std::optional<linear_expression_t> array_domain_t::load(const NumAbsDomain& inv,
         auto ub = ii.ub().number();
         if (lb.has_value() && ub.has_value()) {
             number_t fullwidth = ub.value() - lb.value() + width;
-            if (lb.value().fits<uint32_t>() && fullwidth.fits<uint32_t>()) {
+            if (lb->fits<uint32_t>() && fullwidth.fits<uint32_t>()) {
                 auto [only_num, only_non_num] =
-                    num_bytes.uniformity(static_cast<uint32_t>(lb.value()), static_cast<uint32_t>(fullwidth));
+                    num_bytes.uniformity(lb->narrow<uint32_t>(), fullwidth.narrow<uint32_t>());
                 if (only_num) {
                     return T_NUM;
                 }
@@ -766,7 +766,7 @@ std::optional<variable_t> array_domain_t::store(NumAbsDomain& inv, const data_ki
         auto [offset, size] = *maybe_cell;
         if (kind == data_kind_t::types) {
             const std::optional<number_t> t = inv.eval_interval(val).singleton();
-            if (t && static_cast<int64_t>(*t) == T_NUM) {
+            if (t == number_t{T_NUM}) {
                 num_bytes.reset(offset, size);
             } else {
                 num_bytes.havoc(offset, size);
@@ -786,7 +786,7 @@ std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv, const li
         // perform strong update
         auto [offset, size] = *maybe_cell;
         const std::optional<number_t> t = inv.eval_interval(val).singleton();
-        if (t && static_cast<int64_t>(*t) == T_NUM) {
+        if (t == number_t{T_NUM}) {
             num_bytes.reset(offset, size);
         } else {
             num_bytes.havoc(offset, size);
@@ -837,7 +837,7 @@ void array_domain_t::store_numbers(const NumAbsDomain& inv, const variable_t _id
                   "the number of elements is larger than default limit of ", max_num_elems);
         return;
     }
-    num_bytes.reset(static_cast<int>(*idx_n), static_cast<int>(*width));
+    num_bytes.reset(idx_n->narrow<size_t>(), width->narrow<int>());
 }
 
 void array_domain_t::set_to_top() { num_bytes.set_to_top(); }

src/crab/cfg.hpp

@@ -20,14 +20,12 @@
 
 #include <boost/iterator/transform_iterator.hpp>
 #include <boost/lexical_cast.hpp>
-#include <boost/range/iterator_range.hpp>
-
-#include "crab/variable.hpp"
-#include "crab_utils/debug.hpp"
-#include "crab_utils/num_big.hpp"
+#include <gsl/gsl>
 
 #include "asm_ostream.hpp"
 #include "asm_syntax.hpp"
+#include "crab_utils/debug.hpp"
+#include "crab_utils/num_big.hpp"
 #include "spec_type_descriptors.hpp"
 
 namespace crab {
@@ -100,7 +98,7 @@ class basic_block_t final {
 
     [[nodiscard]]
     size_t size() const {
-        return static_cast<size_t>(std::distance(begin(), end()));
+        return gsl::narrow<size_t>(std::distance(begin(), end()));
     }
 
     [[nodiscard]]
@@ -195,7 +193,7 @@ class basic_block_rev_t final {
 
     [[nodiscard]]
     std::size_t size() const {
-        return static_cast<size_t>(std::distance(begin(), end()));
+        return gsl::narrow<size_t>(std::distance(begin(), end()));
     }
 
     [[nodiscard]]
@@ -382,7 +380,7 @@ class cfg_t final {
 
     [[nodiscard]]
     size_t size() const {
-        return static_cast<size_t>(std::distance(begin(), end()));
+        return gsl::narrow<size_t>(std::distance(begin(), end()));
     }
 
     void simplify() {