AE: replace legacy interval state with native Box

.github/workflows/github-action.yml

@@ -34,13 +34,13 @@ jobs:
         run: |
           XCODE_PATH=$(dirname $(dirname $(xcode-select -p)))
           sudo ln -sfn "$XCODE_PATH" /Applications/Xcode.app
-          brew install astyle
+          brew install astyle gmp mpfr
 
       - name: ubuntu-setup
         if: runner.os == 'Linux'
         run: |
           sudo apt-get update
-          sudo apt-get install cmake gcc g++ nodejs doxygen graphviz lcov libncurses5-dev libtinfo6 libzstd-dev astyle
+          sudo apt-get install cmake gcc g++ nodejs doxygen graphviz lcov libncurses5-dev libtinfo6 libzstd-dev libgmp-dev libmpfr-dev astyle
 
       # build-svf
       - name: build-svf
@@ -97,10 +97,10 @@ jobs:
         run:
           ctest -R double_free -VV
 
-      - name: ctest ae_symabs
+      - name: ctest box domain and integration
         working-directory: ${{github.workspace}}/Release-build
         run:
-          ctest -R symabs -VV
+          ctest -R '^box-' -VV
 
       - name: ctest ae_assert
         working-directory: ${{github.workspace}}/Release-build

.github/workflows/svf-lib_binaries.yml

@@ -40,14 +40,14 @@ jobs:
         run: |
           XCODE_PATH=$(dirname $(dirname $(xcode-select -p)))
           sudo ln -sfn "$XCODE_PATH" /Applications/Xcode.app
-          brew install astyle
+          brew install astyle gmp mpfr
 
       # Ubuntu settings
       - name: ubuntu-setup
         if: runner.os == 'Linux'
         run: |
           sudo apt-get update
-          sudo apt-get install -y cmake gcc g++ nodejs doxygen graphviz libncurses5-dev libtinfo6 libzstd-dev astyle
+          sudo apt-get install -y cmake gcc g++ nodejs doxygen graphviz libncurses5-dev libtinfo6 libzstd-dev libgmp-dev libmpfr-dev astyle
 
       - name: env-setup
         if: github.event_name == 'push' && github.repository == 'SVF-tools/SVF'

CMakeLists.txt

@@ -45,6 +45,10 @@ include(CMakePackageConfigHelpers)
 # Allow checking for IPO support by the used compiler
 include(CheckIPOSupported)
 
+# Define BUILD_TESTING consistently even when the historical Test-Suite
+# directory is absent.  AE/Core tests are registered independently below.
+include(CTest)
+
 # Since SVF builds into non-standard directories; symlink/copy compile commands into top-level directory
 if(WIN32
    OR MINGW
@@ -93,6 +97,15 @@ option(SVF_EXPORT_DYNAMIC "Export all (not only the actually used) symbols to dy
 option(SVF_ENABLE_ASSERTIONS "Always enable debugging assertions, also if the build type is a release build")
 option(SVF_ENABLE_RTTI "Adds -fno-rtti to disable runtime type information (RTTI)" ON)
 option(SVF_ENABLE_EXCEPTIONS "Adds -fno-exceptions to disable exception handling" ON)
+option(SVF_BUILD_ABSTRACT_DOMAIN_TESTS
+       "Build Box domain unit and abstract-execution integration tests"
+       ${BUILD_TESTING})
+
+if(NOT SVF_ENABLE_EXCEPTIONS)
+  message(FATAL_ERROR
+          "AbstractDomainCore uses exception-based API diagnostics; "
+          "SVF_ENABLE_EXCEPTIONS must be ON")
+endif()
 
 # If building dynamic libraries, always enable PIC
 if(SVF_SHARED_LIBS AND NOT SVF_USE_PIC)
@@ -224,6 +237,18 @@ message(
   Z3 C++ include dirs:  ${Z3_CXX_INCLUDE_DIRS}"
 )
 
+find_package(GMP REQUIRED)
+find_package(MPFR REQUIRED)
+message(
+  STATUS
+    "Using Box numeric libraries:
+  GMP include directory:  ${GMP_INCLUDE_DIR}
+  GMP C library:          ${GMP_LIBRARY}
+  GMP C++ library:        ${GMPXX_LIBRARY}
+  MPFR include directory: ${MPFR_INCLUDE_DIR}
+  MPFR library:           ${MPFR_LIBRARY}"
+)
+
 # =================================================================================
 # SVF configuration interface library
 # =================================================================================
@@ -272,8 +297,7 @@ install(TARGETS SvfFlags EXPORT SVFTargets)
 # =================================================================================
 
 # If ./Test-Suite exists, add & run the tests
-if(EXISTS "${SVF_SOURCE_DIR}/Test-Suite")
-  include(CTest)
+if(EXISTS "${SVF_SOURCE_DIR}/Test-Suite/CMakeLists.txt")
   enable_testing()
   add_subdirectory(Test-Suite)
 endif()
@@ -285,13 +309,30 @@ endif()
 add_subdirectory(svf)
 add_subdirectory(svf-llvm)
 
+if(SVF_BUILD_ABSTRACT_DOMAIN_TESTS)
+  enable_testing()
+  add_subdirectory(svf/lib/AE/Test)
+endif()
+
 # =================================================================================
 # SVF build configuration handling (post linking LLVM)
 # =================================================================================
 
 # Expose the required ABI flags (e.g., whether RTTI was disabled) in the build & install trees
 target_compile_options(SvfFlags INTERFACE $<$<NOT:$<BOOL:${SVF_ENABLE_RTTI}>>:-fno-rtti>)
 target_link_options(SvfFlags INTERFACE $<$<NOT:$<BOOL:${SVF_ENABLE_RTTI}>>:-fno-rtti>)
+if(TARGET AbstractStateCore)
+  target_compile_options(
+    AbstractStateCore PUBLIC
+    $<$<NOT:$<BOOL:${SVF_ENABLE_RTTI}>>:-fno-rtti>
+  )
+endif()
+if(TARGET AbstractDomainCore)
+  target_compile_options(
+    AbstractDomainCore PUBLIC
+    $<$<NOT:$<BOOL:${SVF_ENABLE_RTTI}>>:-fno-rtti>
+  )
+endif()
 
 # Expose build/link flags not required for users of SVF only in the build tree
 target_compile_options(

Dockerfile

@@ -18,7 +18,7 @@ ENV HOME=/home/SVF-tools
 # Launchpad PPA infrastructure has been intermittently unreachable
 # (HTTP 504 from add-apt-repository), and SVF itself does not pin a Python
 # version, so the base-image python is sufficient.
-ENV lib_deps="cmake g++ gcc git zlib1g-dev libncurses5-dev libtinfo6 build-essential libssl-dev libpcre2-dev zip libzstd-dev python3-dev"
+ENV lib_deps="cmake g++ gcc git zlib1g-dev libncurses5-dev libtinfo6 build-essential libssl-dev libpcre2-dev zip libzstd-dev libgmp-dev libmpfr-dev python3-dev"
 ENV build_deps="wget xz-utils git tcl"
 
 # Fetch dependencies.

build.sh

@@ -12,7 +12,8 @@
 # If LLVM_DIR or Z3_DIR points to an existing directory, that installation is used.
 # Otherwise, this script installs/downloads the supported prebuilt dependencies.
 #
-# Linux dependencies include: build-essential libncurses5 libncurses-dev cmake zlib1g-dev unzip xz-utils
+# Linux dependencies include: build-essential libncurses5 libncurses-dev cmake
+# zlib1g-dev libgmp-dev libmpfr-dev unzip xz-utils
 
 set -e
 set -o pipefail
@@ -246,7 +247,7 @@ install_llvm_with_brew() {
     check_and_install_brew
 
     echo "Installing LLVM ${MajorLLVMVer} via Homebrew for ${PLATFORM}."
-    brew install "llvm@${MajorLLVMVer}"
+    brew install "llvm@${MajorLLVMVer}" gmp mpfr
 
     mkdir -p "$SVFHOME/$LLVMHome"
     ln -s "$(brew --prefix llvm@${MajorLLVMVer})"/* "$SVFHOME/$LLVMHome"

cmake/Modules/FindGMP.cmake

@@ -0,0 +1,40 @@
+# Find the GMP C and C++ libraries.
+
+include(FindPackageHandleStandardArgs)
+
+set(_GMP_HINTS ${GMP_ROOT} $ENV{GMP_ROOT} ${GMP_DIR} $ENV{GMP_DIR})
+
+find_path(GMP_INCLUDE_DIR NAMES gmp.h gmpxx.h
+          HINTS ${_GMP_HINTS} PATH_SUFFIXES include)
+find_library(GMP_LIBRARY NAMES gmp libgmp
+             HINTS ${_GMP_HINTS} PATH_SUFFIXES lib lib64)
+find_library(GMPXX_LIBRARY NAMES gmpxx libgmpxx
+             HINTS ${_GMP_HINTS} PATH_SUFFIXES lib lib64)
+
+find_package_handle_standard_args(
+  GMP REQUIRED_VARS GMP_INCLUDE_DIR GMP_LIBRARY GMPXX_LIBRARY
+)
+
+if(GMP_FOUND)
+  if(NOT TARGET GMP::GMP)
+    add_library(GMP::GMP UNKNOWN IMPORTED)
+    set_target_properties(
+      GMP::GMP PROPERTIES
+      IMPORTED_LOCATION "${GMP_LIBRARY}"
+      INTERFACE_INCLUDE_DIRECTORIES "${GMP_INCLUDE_DIR}"
+    )
+  endif()
+  if(NOT TARGET GMP::GMPXX)
+    add_library(GMP::GMPXX UNKNOWN IMPORTED)
+    set_target_properties(
+      GMP::GMPXX PROPERTIES
+      IMPORTED_LOCATION "${GMPXX_LIBRARY}"
+      INTERFACE_INCLUDE_DIRECTORIES "${GMP_INCLUDE_DIR}"
+      INTERFACE_LINK_LIBRARIES GMP::GMP
+    )
+  endif()
+  set(GMP_INCLUDE_DIRS "${GMP_INCLUDE_DIR}")
+  set(GMP_LIBRARIES GMP::GMPXX GMP::GMP)
+endif()
+
+mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARY GMPXX_LIBRARY)

cmake/Modules/FindMPFR.cmake

@@ -0,0 +1,33 @@
+# Find MPFR and expose MPFR::MPFR.
+
+include(FindPackageHandleStandardArgs)
+
+set(_MPFR_HINTS ${MPFR_ROOT} $ENV{MPFR_ROOT} ${MPFR_DIR} $ENV{MPFR_DIR})
+
+find_path(MPFR_INCLUDE_DIR NAMES mpfr.h
+          HINTS ${_MPFR_HINTS} PATH_SUFFIXES include)
+find_library(MPFR_LIBRARY NAMES mpfr libmpfr
+             HINTS ${_MPFR_HINTS} PATH_SUFFIXES lib lib64)
+
+find_package_handle_standard_args(
+  MPFR REQUIRED_VARS MPFR_INCLUDE_DIR MPFR_LIBRARY
+)
+
+if(MPFR_FOUND)
+  if(NOT TARGET GMP::GMP)
+    find_package(GMP REQUIRED)
+  endif()
+  if(NOT TARGET MPFR::MPFR)
+    add_library(MPFR::MPFR UNKNOWN IMPORTED)
+    set_target_properties(
+      MPFR::MPFR PROPERTIES
+      IMPORTED_LOCATION "${MPFR_LIBRARY}"
+      INTERFACE_INCLUDE_DIRECTORIES "${MPFR_INCLUDE_DIR}"
+      INTERFACE_LINK_LIBRARIES GMP::GMP
+    )
+  endif()
+  set(MPFR_INCLUDE_DIRS "${MPFR_INCLUDE_DIR}")
+  set(MPFR_LIBRARIES MPFR::MPFR)
+endif()
+
+mark_as_advanced(MPFR_INCLUDE_DIR MPFR_LIBRARY)

cmake/SVFConfig.cmake.in

@@ -4,9 +4,6 @@
 # Ensure the CMake files in this package's directory can be found
 list(PREPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}" "${CMAKE_CURRENT_LIST_DIR}/Modules")
 
-# Ensure SVF's targets & settings are available publicly
-include("${CMAKE_CURRENT_LIST_DIR}/SVFTargets.cmake")
-
 # Set basic variables from this SVF build
 set(SVF_VERSION @SVF_VERSION@)
 set(SVF_BUILD_TYPE @SVF_BUILD_TYPE@)
@@ -69,18 +66,25 @@ set(SVF_BUILD_DIR "@SVF_BINARY_DIR@")
 set(SVF_BUILD_EXTAPI_BC "@SVF_BUILD_EXTAPI_BC@")
 set(SVF_EXTAPI_BC_NAME "@SVF_EXTAPI_BC_NAME@")
 
-# Add the absolute paths of the extapi.bc bitcode file to the imported target's compiler definitions interface
-target_compile_definitions(SVF::SvfFlags INTERFACE SVF_INSTALL_EXTAPI_BC="${SVF_INSTALL_EXTAPI_BC}")
-
 # Make `find_dependency()` available
 include(CMakeFindDependencyMacro)
 
 # Find Z3 (required)
 find_dependency(Z3 REQUIRED)
 
+# Box uses exact GMP rationals and explicit MPFR rounding.
+find_dependency(GMP REQUIRED)
+find_dependency(MPFR REQUIRED)
+
 # Find upstream LLVM (required)
 find_dependency(LLVM CONFIG REQUIRED)
 
+# Load exported targets only after all imported dependency targets exist.
+include("${CMAKE_CURRENT_LIST_DIR}/SVFTargets.cmake")
+
+# Add the absolute path of extapi.bc after the imported target exists.
+target_compile_definitions(SVF::SvfFlags INTERFACE SVF_INSTALL_EXTAPI_BC="${SVF_INSTALL_EXTAPI_BC}")
+
 # Make the include/link directories & definitions available globally for users of SVF
 separate_arguments(_LLVM_DEFINITIONS NATIVE_COMMAND ${LLVM_DEFINITIONS})
 include_directories(SYSTEM ${LLVM_INCLUDE_DIRS})

svf-llvm/CMakeLists.txt

@@ -168,8 +168,16 @@ if(CMAKE_CXX_COMPILER_ID STREQUAL "GNU")
   )
 endif()
 
-# Only expose the headers in the source tree to in-tree users of SVF
-target_include_directories(SvfLLVM PUBLIC $<BUILD_INTERFACE:${CMAKE_CURRENT_LIST_DIR}/include>)
+# Only expose the headers in the source tree to in-tree users of SVF.  SvfLLVM's
+# public headers include LLVM headers, so their build-tree include directories
+# are part of the public build interface as well.
+target_include_directories(
+  SvfLLVM
+  PUBLIC $<BUILD_INTERFACE:${CMAKE_CURRENT_LIST_DIR}/include>
+)
+target_include_directories(
+  SvfLLVM SYSTEM PUBLIC "$<BUILD_INTERFACE:${LLVM_INCLUDE_DIRS}>"
+)
 
 # Set the library & .so version of the LLVM library
 set_target_properties(SvfLLVM PROPERTIES VERSION ${SVF_VERSION} SOVERSION ${SVF_VERSION_MAJOR})