Replace LLVM's DSA with sea-dsa

This commit replaces the old LLVM's DSA with the newer sea-dsa:
* Adds sea-dsa as a submodule
* Switches from LLVM's DSA to sea-dsa
* Uses sea-dsa's CompleteCallGraph pass to assist indirect call resolving
* Renames MemCpyd to MemOpd
* Handles the case where values don't have cells
* Makes sure that singletons are not in allocated nodes

Closes #549

.gitmodules

@@ -0,0 +1,4 @@
+[submodule "sea-dsa"]
+  path = sea-dsa
+  url = https://github.com/seahorn/sea-dsa.git
+  branch = llvm-8.0

.travis.yml

@@ -12,6 +12,7 @@ addons:
       - unzip
       - libz-dev
       - libedit-dev
+      - libboost-all-dev
 
 cache:
   directories:

CMakeLists.txt

@@ -2,7 +2,7 @@
 # This file is distributed under the MIT License. See LICENSE for details.
 #
 
-cmake_minimum_required(VERSION 2.8)
+cmake_minimum_required(VERSION 3.4.3)
 project(smack)
 
 if (NOT WIN32 OR MSYS OR CYGWIN)
@@ -93,87 +93,17 @@ else()
 endif()
 
 include_directories(include)
-
-add_library(assistDS STATIC
-  include/assistDS/ArgCast.h
-  include/assistDS/FuncSimplify.h
-  include/assistDS/Int2PtrCmp.h
-  include/assistDS/SimplifyExtractValue.h
-  include/assistDS/StructReturnToPointer.h
-  include/assistDS/DSNodeEquivs.h
-  include/assistDS/FuncSpec.h
-  include/assistDS/SimplifyGEP.h
-  include/assistDS/TypeChecks.h
-  include/assistDS/DataStructureCallGraph.h
-  include/assistDS/GEPExprArgs.h
-  include/assistDS/LoadArgs.h
-  include/assistDS/SimplifyInsertValue.h
-  include/assistDS/TypeChecksOpt.h
-  include/assistDS/Devirt.h
-  include/assistDS/IndCloner.h
-  include/assistDS/MergeGEP.h
-  include/assistDS/SimplifyLoad.h
-  lib/AssistDS/ArgCast.cpp
-  lib/AssistDS/Devirt.cpp
-  lib/AssistDS/GEPExprArgs.cpp
-  lib/AssistDS/LoadArgs.cpp
-  lib/AssistDS/SimplifyExtractValue.cpp
-  lib/AssistDS/StructReturnToPointer.cpp
-  lib/AssistDS/ArgSimplify.cpp
-  lib/AssistDS/DynCount.cpp
-  lib/AssistDS/IndCloner.cpp
-  lib/AssistDS/SimplifyGEP.cpp
-  lib/AssistDS/TypeChecks.cpp
-  lib/AssistDS/DSNodeEquivs.cpp
-  lib/AssistDS/FuncSimplify.cpp
-  lib/AssistDS/Int2PtrCmp.cpp
-  lib/AssistDS/MergeGEP.cpp
-  lib/AssistDS/SimplifyInsertValue.cpp
-  lib/AssistDS/TypeChecksOpt.cpp
-  lib/AssistDS/DataStructureCallGraph.cpp
-  lib/AssistDS/FuncSpec.cpp
-  lib/AssistDS/SVADevirt.cpp
-  lib/AssistDS/SimplifyLoad.cpp
-)
-
-add_library(dsa STATIC
-  include/dsa/AddressTakenAnalysis.h
-  include/dsa/DSCallGraph.h
-  include/dsa/DSNode.h
-  include/dsa/EntryPointAnalysis.h
-  include/dsa/keyiterator.h
-  include/dsa/svset.h
-  include/dsa/AllocatorIdentification.h
-  include/dsa/DSGraph.h
-  include/dsa/DSSupport.h
-  include/dsa/stl_util.h
-  include/dsa/CallTargets.h
-  include/dsa/DSGraphTraits.h
-  include/dsa/DataStructure.h
-  include/dsa/TypeSafety.h
-  include/dsa/super_set.h
-  include/dsa/DSMonitor.h
-  lib/DSA/AddressTakenAnalysis.cpp
-  lib/DSA/CallTargets.cpp
-  lib/DSA/DSTest.cpp
-  lib/DSA/EquivClassGraphs.cpp
-  lib/DSA/StdLibPass.cpp
-  lib/DSA/AllocatorIdentification.cpp
-  lib/DSA/CompleteBottomUp.cpp
-  lib/DSA/DataStructure.cpp
-  lib/DSA/GraphChecker.cpp
-  lib/DSA/Printer.cpp
-  lib/DSA/TopDownClosure.cpp
-  lib/DSA/Basic.cpp
-  lib/DSA/DSCallGraph.cpp
-  lib/DSA/DataStructureStats.cpp
-  lib/DSA/TypeSafety.cpp
-  lib/DSA/BottomUpClosure.cpp
-  lib/DSA/DSGraph.cpp
-  lib/DSA/EntryPointAnalysis.cpp
-  lib/DSA/DSMonitor.cpp
-  lib/DSA/Local.cpp
-  lib/DSA/SanityCheck.cpp
+include_directories(sea-dsa/include)
+
+add_library(utils STATIC
+  include/utils/Devirt.h
+  include/utils/MergeGEP.h
+  include/utils/SimplifyInsertValue.h
+  include/utils/SimplifyExtractValue.h
+  lib/utils/Devirt.cpp
+  lib/utils/MergeGEP.cpp
+  lib/utils/SimplifyInsertValue.cpp
+  lib/utils/SimplifyExtractValue.cpp
 )
 
 add_library(smackTranslator STATIC
@@ -230,8 +160,27 @@ add_executable(llvm2bpl
   tools/llvm2bpl/llvm2bpl.cpp
 )
 
+# We need to include Boost header files at least for macOS
+find_package (Boost 1.55)
+if (Boost_FOUND)
+  include_directories (${Boost_INCLUDE_DIRS})
+endif ()
+# We have to import LLVM's cmake definitions to build sea-dsa
+# Borrowed from sea-dsa's CMakeLists.txt
+find_package (LLVM 8.0.1 EXACT CONFIG)
+list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")
+include(AddLLVM)
+include(HandleLLVMOptions)
+# We need the release build of sea-dsa otherwise we'll see a lot of crashes in
+# sv-comp benchmarks.
+# The following solution is from: https://stackoverflow.com/questions/30985215/passing-variables-down-to-subdirectory-only
+set(SMACK_BUILD_TYPE "${CMAKE_BUILD_TYPE}")
+set(CMAKE_BUILD_TYPE "Release")
+add_subdirectory(sea-dsa/src)
+set(CMAKE_BUILD_TYPE ${SMACK_BUILD_TYPE})
+
 target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS} ${LLVM_LDFLAGS})
-target_link_libraries(llvm2bpl smackTranslator assistDS dsa)
+target_link_libraries(llvm2bpl smackTranslator utils SeaDsaAnalysis)
 
 INSTALL(TARGETS llvm2bpl
   RUNTIME DESTINATION bin

bin/build.sh

@@ -60,7 +60,7 @@ CONFIGURE_INSTALL_PREFIX=
 CMAKE_INSTALL_PREFIX=
 
 # Partial list of dependencies; the rest are added depending on the platform
-DEPENDENCIES="git cmake python3-yaml python3-psutil unzip wget ninja-build"
+DEPENDENCIES="git cmake python3-yaml python3-psutil unzip wget ninja-build libboost-all-dev"
 
 shopt -s extglob
 
@@ -506,6 +506,10 @@ fi
 if [ ${BUILD_SMACK} -eq 1 ] ; then
   puts "Building SMACK"
 
+  cd ${SMACK_DIR}
+  git submodule init
+  git submodule update
+
   mkdir -p ${SMACK_DIR}/build
   cd ${SMACK_DIR}/build
   cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_BUILD_TYPE=Debug .. -G Ninja

docs/installation.md

@@ -82,11 +82,13 @@ SMACK depends on the following projects:
 
 * [LLVM][] version [8.0.1][LLVM-8.0.1]
 * [Clang][] version [8.0.1][Clang-8.0.1]
+* [Boost][] version 1.55 or greater
 * [Python][] version 3.6.8 or greater
 * [Ninja][] version 1.5.1 or greater
 * [Mono][] version 5.0.0 or greater (except on Windows)
 * [Z3][] or compatible SMT-format theorem prover
 * [Boogie][] or [Corral][] or compatible Boogie-format verifier
+* [sea-dsa][]
 
 See [here](https://github.com/smackers/smack/blob/master/bin/versions) for
 compatible version numbers of [Boogie][] and [Corral][]. See the appropriate
@@ -153,9 +155,14 @@ installed via the Microsoft Store.
 
 ### Installing SMACK Itself
 
-SMACK is built using [CMake][] via the following sequence of shell commands
-from SMACK's root directory:
-````Shell
+The prerequisite step for building SMACK is to fetch its submodule
+(i.e., [sea-dsa][]). Then, it is built using [CMake][]. Both steps can be done
+via the following sequence of shell commands from SMACK's root directory:
+```Shell
+# fetch the submodule
+git submodule init
+git submodule update
+# build SMACK
 mkdir build
 cd build
 cmake -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
@@ -218,3 +225,5 @@ shell in the `test` directory by executing
 [Homebrew Cask]: https://formulae.brew.sh/cask/
 [Docker]: https://www.docker.com
 [Ninja]: https://ninja-build.org
+[sea-dsa]: https://github.com/seahorn/sea-dsa
+[Boost]: http://boost.org/