diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 000000000..fe7950bd7
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,4 @@
+[submodule "sea-dsa"]
+ path = sea-dsa
+ url = https://github.com/seahorn/sea-dsa.git
+ branch = llvm-8.0
diff --git a/.travis.yml b/.travis.yml
index 70f6ce234..f8ff1c6ac 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,18 +1,18 @@
language: generic
-dist: xenial
-sudo: required
-compiler: clang
+os: linux
+dist: bionic
addons:
apt:
packages:
- git
- cmake
- - python-yaml
- - python-psutil
+ - python3-yaml
+ - python3-psutil
- unzip
- libz-dev
- libedit-dev
+ - libboost-all-dev
cache:
directories:
@@ -24,30 +24,37 @@ cache:
env:
global:
- COMPILER_NAME=clang COMPILER=clang++ CXX=clang++ CC=clang
- matrix:
- - TRAVIS_ENV="--exhaustive --folder=basic"
- - TRAVIS_ENV="--exhaustive --folder=data"
- - TRAVIS_ENV="--exhaustive --folder=ntdrivers-simplified"
- - TRAVIS_ENV="--exhaustive --folder=bits"
- - TRAVIS_ENV="--exhaustive --folder=float"
- - TRAVIS_ENV="--exhaustive --folder=locks"
- - TRAVIS_ENV="--exhaustive --folder=contracts"
- - TRAVIS_ENV="--exhaustive --folder=simd"
- - TRAVIS_ENV="--exhaustive --folder=memory-safety"
- - TRAVIS_ENV="--exhaustive --folder=pthread"
- - TRAVIS_ENV="--exhaustive --folder=strings"
+ jobs:
+ - TRAVIS_ENV="--exhaustive --folder=c/basic"
+ - TRAVIS_ENV="--exhaustive --folder=c/data"
+ - TRAVIS_ENV="--exhaustive --folder=c/ntdrivers-simplified"
+ - TRAVIS_ENV="--exhaustive --folder=c/bits"
+ - TRAVIS_ENV="--exhaustive --folder=c/float"
+ - TRAVIS_ENV="--exhaustive --folder=c/locks"
+ - TRAVIS_ENV="--exhaustive --folder=c/contracts"
+ - TRAVIS_ENV="--exhaustive --folder=c/simd"
+ - TRAVIS_ENV="--exhaustive --folder=c/memory-safety"
+ - TRAVIS_ENV="--exhaustive --folder=c/pthread"
+ - TRAVIS_ENV="--exhaustive --folder=c/strings"
+ - TRAVIS_ENV="--exhaustive --folder=c/special"
+ - TRAVIS_ENV="--exhaustive --folder=rust/basic --languages=rust"
+ - TRAVIS_ENV="--exhaustive --folder=rust/functions --languages=rust"
+ - TRAVIS_ENV="--exhaustive --folder=rust/generics --languages=rust"
+ - TRAVIS_ENV="--exhaustive --folder=rust/loops --languages=rust"
+ - TRAVIS_ENV="--exhaustive --folder=rust/recursion --languages=rust"
+ - TRAVIS_ENV="--exhaustive --folder=rust/structures --languages=rust"
+ - TRAVIS_ENV="--exhaustive --folder=rust/vector --languages=rust"
before_install:
- - sudo rm -rf /usr/local/clang-7.0.0
- - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-8 main"
- wget -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
+ - sudo add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-8 main"
- sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
- sudo apt-get install -y apt-transport-https
- - echo "deb https://download.mono-project.com/repo/ubuntu stable-xenial main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
+ - echo "deb https://download.mono-project.com/repo/ubuntu stable-bionic main" | sudo tee /etc/apt/sources.list.d/mono-official-stable.list
- sudo apt-get update
install:
- - sudo apt-get install -y clang-8 clang-format-8 llvm-8-dev mono-complete ninja-build
+ - sudo apt-get install -y clang-8 clang-format-8 llvm-8-dev mono-complete ca-certificates-mono ninja-build
- sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-8 20
- sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-8 20
- sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-8 20
@@ -58,11 +65,12 @@ install:
script:
- python --version
+ - python3 --version
- $CXX --version
- $CC --version
- clang --version
- clang++ --version
- llvm-link --version
- llvm-config --version
- - ./format/run-clang-format.py -e test/basic/transform-out.c -r lib/smack include/smack share/smack/include share/smack/lib test examples
- - ./bin/build.sh
+ - ./format/run-clang-format.py -e test/c/basic/transform-out.c -r lib/smack include/smack share/smack/include share/smack/lib test examples
+ - INSTALL_RUST=1 ./bin/build.sh
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 40f5078cc..c73d88a73 100644
--- a/CMakeLists.txt
+++ b/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)
@@ -18,6 +18,7 @@ if (NOT WIN32 OR MSYS OR CYGWIN)
OUTPUT_STRIP_TRAILING_WHITESPACE
)
+ # TODO: explain why these are required.
string(REPLACE "-DNDEBUG" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
string(REPLACE "-Wno-maybe-uninitialized" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
string(REPLACE "-fuse-ld=gold" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
@@ -26,9 +27,27 @@ if (NOT WIN32 OR MSYS OR CYGWIN)
string(REPLACE "-Wl," "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
string(REPLACE "-gsplit-dwarf" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
string(REGEX REPLACE "-O[0-9]" "" CMAKE_CXX_FLAGS "${LLVM_CXXFLAGS}")
+
+ # TODO: append these one at a time; give rationale.
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fno-exceptions -fno-rtti -Wno-undefined-var-template")
- set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0")
- set(CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -O0")
+
+ # Apparently avoids a problem with inconsistent visibility settings from LLVM:
+ #
+ # > ld: warning: direct access in function 'llvm::_'
+ # > from file '/usr/local/opt/llvm@8/lib/_'
+ # > to global weak symbol 'llvm::_'
+ # > from file 'libsmackTranslator.a(_.cpp.o)'
+ # > means the weak symbol cannot be overridden at runtime.
+ # > This was likely caused by different translation units being compiled
+ # > with different visibility settings.
+ #
+ # Solution found on Stack Overflow:
+ # https://stackoverflow.com/questions/8685045/xcode-with-boost-linkerid-warning-about-visibility-settings
+ string(APPEND CMAKE_CXX_FLAGS_DEBUG " -fvisibility=hidden")
+
+ # TODO: explain why these are required.
+ string(APPEND CMAKE_CXX_FLAGS_DEBUG " -O0")
+ string(APPEND CMAKE_C_FLAGS_DEBUG " -O0")
execute_process(
COMMAND ${LLVM_CONFIG_EXECUTABLE} --libs
@@ -74,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
@@ -211,18 +160,33 @@ 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
)
INSTALL(FILES
- ${CMAKE_CURRENT_SOURCE_DIR}/bin/boogie
- ${CMAKE_CURRENT_SOURCE_DIR}/bin/corral
- ${CMAKE_CURRENT_SOURCE_DIR}/bin/symbooglix
- ${CMAKE_CURRENT_SOURCE_DIR}/bin/lockpwn
${CMAKE_CURRENT_SOURCE_DIR}/bin/smack
${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-doctor
${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-svcomp-wrapper.sh
diff --git a/Doxyfile b/Doxyfile
index f77267f29..8f750c35f 100644
--- a/Doxyfile
+++ b/Doxyfile
@@ -5,7 +5,7 @@
#---------------------------------------------------------------------------
DOXYFILE_ENCODING = UTF-8
PROJECT_NAME = smack
-PROJECT_NUMBER = 2.4.0
+PROJECT_NUMBER = 2.4.1
PROJECT_BRIEF = "A bounded software verifier."
PROJECT_LOGO =
OUTPUT_DIRECTORY = docs
diff --git a/README.md b/README.md
index 0367ec47d..912394b6d 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-| **master** | [![Build Status](https://travis-ci.org/smackers/smack.svg?branch=master)](https://travis-ci.org/smackers/smack) | **develop** | [![Build Status](https://travis-ci.org/smackers/smack.svg?branch=develop)](https://travis-ci.org/smackers/smack) |
+| **master** | [![Build Status](https://travis-ci.com/smackers/smack.svg?branch=master)](https://travis-ci.com/smackers/smack) | **develop** | [![Build Status](https://travis-ci.com/smackers/smack.svg?branch=develop)](https://travis-ci.com/smackers/smack) |
| --- | --- | --- | --- |
diff --git a/bin/boogie b/bin/boogie
deleted file mode 100755
index 1ea15b4fb..000000000
--- a/bin/boogie
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/bash
-if [ -z "$BOOGIE" ] ; then
- echo "The required BOOGIE environment variable is not set. See SMACK documentation for details."
- exit 1
-fi
-$BOOGIE "$@"
diff --git a/bin/build.sh b/bin/build.sh
index c20615efd..1fc78fc7a 100755
--- a/bin/build.sh
+++ b/bin/build.sh
@@ -23,6 +23,7 @@
# Set these flags to control various installation options
INSTALL_DEPENDENCIES=1
INSTALL_Z3=1
+INSTALL_CVC4=1
BUILD_BOOGIE=1
BUILD_CORRAL=1
BUILD_SYMBOOGLIX=1
@@ -34,12 +35,13 @@ BUILD_MONO=0 # mono is typically installed from packages (see below)
# Support for more programming languages
INSTALL_OBJECTIVEC=0
-INSTALL_RUST=0
+INSTALL_RUST=${INSTALL_RUST:-0}
# PATHS
SMACK_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && cd .. && pwd )"
ROOT="$( cd "${SMACK_DIR}" && cd .. && pwd )"
Z3_DIR="${ROOT}/z3"
+CVC4_DIR="${ROOT}/cvc4"
BOOGIE_DIR="${ROOT}/boogie"
CORRAL_DIR="${ROOT}/corral"
SYMBOOGLIX_DIR="${ROOT}/symbooglix"
@@ -58,7 +60,7 @@ CONFIGURE_INSTALL_PREFIX=
CMAKE_INSTALL_PREFIX=
# Partial list of dependencies; the rest are added depending on the platform
-DEPENDENCIES="git cmake python-yaml python-psutil unzip wget ninja-build"
+DEPENDENCIES="git cmake python3-yaml python3-psutil unzip wget ninja-build libboost-all-dev"
shopt -s extglob
@@ -182,23 +184,23 @@ puts "Detected distribution: $distro"
case "$distro" in
linux-opensuse*)
Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/Z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-debian-8.10.zip"
- DEPENDENCIES+=" llvm-clang llvm-devel gcc-c++ mono-complete make"
+ DEPENDENCIES+=" llvm-clang llvm-devel gcc-c++ mono-complete ca-certificates-mono make"
DEPENDENCIES+=" ncurses-devel zlib-devel"
;;
linux-@(ubuntu|neon)-14*)
Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/Z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-14.04.zip"
- DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev mono-complete libz-dev libedit-dev"
+ DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev mono-complete ca-certificates-mono libz-dev libedit-dev"
;;
linux-@(ubuntu|neon)-16*)
Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/Z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-16.04.zip"
- DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev mono-complete libz-dev libedit-dev"
+ DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev mono-complete ca-certificates-mono libz-dev libedit-dev"
;;
linux-@(ubuntu|neon)-18*)
Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/Z3-${Z3_SHORT_VERSION}/z3-${Z3_FULL_VERSION}-x64-ubuntu-16.04.zip"
- DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev mono-complete libz-dev libedit-dev"
+ DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev mono-complete ca-certificates-mono libz-dev libedit-dev"
;;
linux-ubuntu-12*)
@@ -377,7 +379,7 @@ if [ ${INSTALL_OBJECTIVEC} -eq 1 ] ; then
echo ". /usr/share/GNUstep/Makefiles/GNUstep.sh" >> ${SMACKENV}
puts "Installed Objective-C"
-fi
+fi
if [ ${INSTALL_RUST} -eq 1 ] ; then
puts "Installing Rust"
@@ -385,9 +387,10 @@ if [ ${INSTALL_RUST} -eq 1 ] ; then
${WGET} https://static.rust-lang.org/dist/${RUST_VERSION}/rust-nightly-x86_64-unknown-linux-gnu.tar.gz -O rust.tar.gz
tar xf rust.tar.gz
cd rust-nightly-x86_64-unknown-linux-gnu
- sudo ./install.sh
+ sudo ./install.sh --without=rust-docs
cd ..
-
+ rm -r rust-nightly-x86_64-unknown-linux-gnu rust.tar.gz
+
puts "Installed Rust"
fi
@@ -405,6 +408,17 @@ if [ ${INSTALL_Z3} -eq 1 ] ; then
fi
fi
+if [ ${INSTALL_CVC4} -eq 1 ] ; then
+ if [ ! -d "$CVC4_DIR" ] ; then
+ puts "Installing CVC4"
+ mkdir -p ${CVC4_DIR}
+ ${WGET} https://github.com/CVC4/CVC4/releases/download/${CVC4_VERSION}/cvc4-${CVC4_VERSION}-x86_64-linux-opt -O ${CVC4_DIR}/cvc4
+ chmod +x ${CVC4_DIR}/cvc4
+ puts "Installed CVC4"
+ else
+ puts "CVC4 already installed"
+ fi
+fi
if [ ${BUILD_BOOGIE} -eq 1 ] ; then
if ! upToDate $BOOGIE_DIR $BOOGIE_COMMIT ; then
@@ -420,10 +434,12 @@ if [ ${BUILD_BOOGIE} -eq 1 ] ; then
rm -rf /tmp/nuget/
msbuild Boogie.sln /p:Configuration=Release
ln -sf ${Z3_DIR}/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe
+ ln -sf ${CVC4_DIR}/cvc4 ${BOOGIE_DIR}/Binaries/cvc4.exe
puts "Built Boogie"
else
puts "Boogie already built"
fi
+ echo export PATH=\"${BOOGIE_DIR}/Binaries:\$PATH\" >> ${SMACKENV}
fi
@@ -439,10 +455,13 @@ if [ ${BUILD_CORRAL} -eq 1 ] ; then
git submodule update
msbuild cba.sln /p:Configuration=Release
ln -sf ${Z3_DIR}/bin/z3 ${CORRAL_DIR}/bin/Release/z3.exe
+ ln -sf ${CVC4_DIR}/cvc4 ${CORRAL_DIR}/bin/Release/cvc4.exe
+ sed -i.debug -e's/Debug/Release/' ${CORRAL_DIR}/bin/corral
puts "Built Corral"
else
puts "Corral already built"
fi
+ echo export PATH=\"${CORRAL_DIR}/bin:\$PATH\" >> ${SMACKENV}
fi
if [ ${BUILD_SYMBOOGLIX} -eq 1 ] ; then
@@ -459,10 +478,12 @@ if [ ${BUILD_SYMBOOGLIX} -eq 1 ] ; then
xbuild Symbooglix.sln /p:Configuration=Release
ln -s ${Z3_DIR}/bin/z3 ${SYMBOOGLIX_DIR}/src/SymbooglixDriver/bin/Release/z3.exe
ln -s ${Z3_DIR}/bin/z3 ${SYMBOOGLIX_DIR}/src/Symbooglix/bin/Release/z3.exe
+ sed -i.debug -e's/Debug/Release/' ${SYMBOOGLIX_DIR}/bin/symbooglix
puts "Built Symbooglix"
else
puts "Symbooglix already built"
fi
+ echo export PATH=\"${SYMBOOGLIX_DIR}/bin:\$PATH\" >> ${SMACKENV}
fi
if [ ${BUILD_LOCKPWN} -eq 1 ] ; then
@@ -479,11 +500,16 @@ if [ ${BUILD_LOCKPWN} -eq 1 ] ; then
else
puts "Lockpwn already built"
fi
+ echo export PATH=\"${LOCKPWN_DIR}/Binaries:\$PATH\" >> ${SMACKENV}
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
@@ -491,10 +517,6 @@ if [ ${BUILD_SMACK} -eq 1 ] ; then
sudo ninja install
puts "Configuring shell environment"
- echo export BOOGIE=\"mono ${BOOGIE_DIR}/Binaries/Boogie.exe\" >> ${SMACKENV}
- echo export CORRAL=\"mono ${CORRAL_DIR}/bin/Release/corral.exe\" >> ${SMACKENV}
- echo export SYMBOOGLIX=\"mono ${SYMBOOGLIX_DIR}/src/SymbooglixDriver/bin/Release/sbx.exe\" >> ${SMACKENV}
- echo export LOCKPWN=\"mono ${LOCKPWN_DIR}/Binaries/lockpwn.exe\" >> ${SMACKENV}
source ${SMACKENV}
puts "The required environment variables have been set in ${SMACKENV}"
puts "You should source ${SMACKENV} in your .bashrc"
diff --git a/bin/corral b/bin/corral
deleted file mode 100755
index b26192e81..000000000
--- a/bin/corral
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/bash
-if [ -z "$CORRAL" ] ; then
- echo "The required CORRAL environment variable is not set. See SMACK documentation for details."
- exit 1
-fi
-$CORRAL "$@"
diff --git a/bin/lockpwn b/bin/lockpwn
deleted file mode 100755
index c8cdfec33..000000000
--- a/bin/lockpwn
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/bash
-if [ -z "$LOCKPWN" ] ; then
- echo "The required LOCKPWN environment variable is not set. See SMACK documentation for details."
- exit 1
-fi
-$LOCKPWN "$@"
diff --git a/bin/smack b/bin/smack
index bbc4e0601..e8efa74db 100755
--- a/bin/smack
+++ b/bin/smack
@@ -1,4 +1,4 @@
-#!/usr/bin/env python2
+#!/usr/bin/env python3
#
# This file is distributed under the MIT License. See LICENSE for details.
#
diff --git a/bin/smack-doctor b/bin/smack-doctor
index c206adfd9..10610c495 100755
--- a/bin/smack-doctor
+++ b/bin/smack-doctor
@@ -1,4 +1,4 @@
-#!/usr/bin/env python2
+#!/usr/bin/env python3
#
# This file is distributed under the MIT License. See LICENSE for details.
#
diff --git a/bin/symbooglix b/bin/symbooglix
deleted file mode 100755
index 79c20a3cb..000000000
--- a/bin/symbooglix
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/bash
-if [ -z "$SYMBOOGLIX" ] ; then
- echo "The required SYMBOOGLIX environment variable is not set. See SMACK documentation for details."
- exit 1
-fi
-$SYMBOOGLIX "$@"
diff --git a/bin/versions b/bin/versions
index d9e780e1d..7436fd763 100644
--- a/bin/versions
+++ b/bin/versions
@@ -1,10 +1,11 @@
MONO_VERSION=5.0.0.100
Z3_SHORT_VERSION=4.8.5
Z3_FULL_VERSION=4.8.5
+CVC4_VERSION=1.7
BOOGIE_COMMIT=5c829b6340
-CORRAL_COMMIT=c446f5e827
-SYMBOOGLIX_COMMIT=7210e5d09b
-LOCKPWN_COMMIT=73eddf97bd
+CORRAL_COMMIT=6437c41d34
+SYMBOOGLIX_COMMIT=ccb2e7f2b3
+LOCKPWN_COMMIT=12ba58f1ec
LLVM_SHORT_VERSION=8
LLVM_FULL_VERSION=8.0.1
-RUST_VERSION=2016-12-16
+RUST_VERSION=2019-07-16
diff --git a/bin/vsmack b/bin/vsmack
index 8cbbdf037..253c3ad73 100755
--- a/bin/vsmack
+++ b/bin/vsmack
@@ -1,4 +1,4 @@
-#!/usr/bin/env python2
+#!/usr/bin/env python3
import argparse
import os.path
@@ -84,7 +84,7 @@ if __name__ == '__main__':
raise Exception('failed to halt the box')
except Exception as e:
- print 'error:', e
+ print('error:', e)
finally:
pass
diff --git a/docs/installation.md b/docs/installation.md
index e129dd08b..9af8d42bf 100644
--- a/docs/installation.md
+++ b/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]
-* [Python][] version 2.7 or greater
+* [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
@@ -169,17 +176,17 @@ prefix, add the additional flag:
````
substituting the string `PREFIX` for the desired location.
-Actually running SMACK relies on the environment variables `BOOGIE` and
-`CORRAL` targeting the `Boogie.exe` and `corral.exe` executables, for instance
-residing in paths prefixed by `XXX` and `YYY`:
-````Shell
-export BOOGIE="mono /XXX/Boogie/Binaries/Boogie.exe"
-export CORRAL="mono /YYY/Corral/bin/Release/corral.exe"
+Actually running SMACK relies on `boogie` and `corral` being in the executable
+path. For instance, if you have built Boogie and Corral from source at paths
+at `$BOOGIE_SOURCE` and `$CORRAL_SOURCE`:
+````bash
+export PATH="$BOOGIE_SOURCE/Binaries:$PATH"
+export PATH="$CORRAL_SOURCE/bin:$PATH"
````
Source the preceding lines in your shell's `.profile`, and ensure they invoke
Boogie/Corral correctly. For example, running
-````Shell
-BOOGIE
+````console
+$ boogie
````
should result in
````
@@ -215,6 +222,8 @@ shell in the `test` directory by executing
[build.sh]: https://github.com/smackers/smack/blob/master/bin/build.sh
[Xcode]: https://developer.apple.com/xcode/
[Homebrew]: http://brew.sh/
-[Homebrew Cask]: http://caskroom.io
+[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/
diff --git a/format/run-clang-format.py b/format/run-clang-format.py
index 3d0cca0a9..2923ee31a 100755
--- a/format/run-clang-format.py
+++ b/format/run-clang-format.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
"""A wrapper script around clang-format, suitable for linting multiple files
and to use for continuous integration.
@@ -126,7 +126,7 @@ def run_clang_format_diff(args, file):
#
# It's not pretty, due to Python 2 & 3 compatibility.
encoding_py3 = {}
- if sys.version_info[0] >= 3:
+ if sys.version_info[0] >= 3 and sys.version_info[1] >= 6:
encoding_py3['encoding'] = 'utf-8'
try:
diff --git a/include/assistDS/ArgCast.h b/include/assistDS/ArgCast.h
deleted file mode 100644
index 4c0bf8765..000000000
--- a/include/assistDS/ArgCast.h
+++ /dev/null
@@ -1,35 +0,0 @@
-//===-------- ArgCast.cpp - Cast Arguments to Calls -----------------------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-// Convert
-// call(bitcast (.., T1 arg, ...)F to(..., T2 arg, ...))(..., T2 val, ...)
-// to
-// val1 = bitcast T2 val to T1
-// call F (..., T1 val1, ...)
-//===----------------------------------------------------------------------===//
-
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Constants.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Pass.h"
-
-namespace llvm {
- //
- // Class: ArgCast
- //
- // Description:
- // Implement an LLVM pass that cleans up call sites that take casted args
- //
- class ArgCast : public ModulePass {
- public:
- static char ID;
- ArgCast() : ModulePass(ID) {}
- virtual bool runOnModule(Module& M);
- };
-}
-
diff --git a/include/assistDS/DSNodeEquivs.h b/include/assistDS/DSNodeEquivs.h
deleted file mode 100644
index e05a542c7..000000000
--- a/include/assistDS/DSNodeEquivs.h
+++ /dev/null
@@ -1,68 +0,0 @@
-//===- DSNodeEquivs.h - Build DSNode equivalence classes ------------------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file was developed by the LLVM research group and is distributed under
-// the University of Illinois Open Source License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// This pass computes equivalence classes of DSNodes across DSGraphs.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef DSNODEEQUIVS_H
-#define DSNODEEQUIVS_H
-
-#include "dsa/DataStructure.h"
-#include "dsa/DSGraph.h"
-#include "dsa/DSNode.h"
-
-#include "llvm/ADT/EquivalenceClasses.h"
-
-#include
-
-namespace llvm {
-
-typedef std::vector FunctionList;
-typedef FunctionList::iterator FunctionList_it;
-
-class DSNodeEquivs : public ModulePass {
-private:
- EquivalenceClasses Classes;
-
- void buildDSNodeEquivs(Module &M);
-
- void addNodesFromGraph(DSGraph *G);
- FunctionList getCallees(CallSite &CS);
- void equivNodesThroughCallsite(CallInst *CI);
- void equivNodesToGlobals(DSGraph *G);
- void equivNodeMapping(DSGraph::NodeMapTy & NM);
-
-public:
- static char ID;
-
- DSNodeEquivs() : ModulePass(ID) {}
-
- void getAnalysisUsage(AnalysisUsage &AU) const {
- AU.addRequiredTransitive();
- AU.setPreservesAll();
- }
-
- bool runOnModule(Module &M);
-
- // Returns the computed equivalence classes. Two DSNodes in the same
- // equivalence class may alias. DSNodes may also alias if they have the
- // Incomplete, Unknown, or External flags set (even if they are in different
- // equivalence classes).
- const EquivalenceClasses &getEquivalenceClasses();
-
- // Returns a DSNode for the specified value. Note that two nodes may alias
- // even if they have different DSNodes (because the DSNodes may belong to
- // different DSGraphs).
- const DSNode *getMemberForValue(const Value *V);
-};
-
-}
-
-#endif // DSNODEEQUIVS_H
diff --git a/include/assistDS/DataStructureCallGraph.h b/include/assistDS/DataStructureCallGraph.h
deleted file mode 100644
index ed5dcf9bf..000000000
--- a/include/assistDS/DataStructureCallGraph.h
+++ /dev/null
@@ -1,107 +0,0 @@
-//===- DataStructureCallGraph.h - Provide a CallGraph using DSA -----------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// This file declares the DataStructureCallGraph implementation of the
-// CallGraph analysis. Based on llvm/lib/Analysis/IPA/CallGraph.cpp.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef _DATA_STRUCTURE_CALLGRAPH_H
-#define _DATA_STRUCTURE_CALLGRAPH_H
-
-#include "dsa/CallTargets.h"
-#include "dsa/DataStructure.h"
-
-#include "llvm/IR/Module.h"
-#include "llvm/Analysis/CallGraph.h"
-#include "llvm/Support/raw_ostream.h"
-
-namespace llvm {
-
-class DataStructureCallGraph : public CallGraphWrapperPass {
- // Root is root of the call graph, or the external node if a 'main' function
- // couldn't be found.
- CallGraphNode *Root;
-
- // ExternalCallingNode - This node has edges to all external functions and
- // those internal functions that have their address taken.
- CallGraphNode *ExternalCallingNode;
-
- // CallsExternalNode - This node has edges to it from all functions making
- // indirect calls or calling an external function.
- CallGraphNode *CallsExternalNode;
-
- typedef dsa::CallTargetFinder CallTargetFinderTy;
-
-public:
- static char ID;
- DataStructureCallGraph() :
- Root(0), ExternalCallingNode(0), CallsExternalNode(0) { }
-
- virtual bool runOnModule(Module &M);
-
- virtual void getAnalysisUsage(AnalysisUsage &AU) const {
- AU.addRequired();
- AU.addRequired();
- AU.setPreservesAll();
- }
-
- virtual void print(raw_ostream &OS, const Module *) const {
- OS << "CallGraph Root is: ";
- if (Function *F = getRoot()->getFunction())
- OS << F->getName() << "\n";
- else {
- OS << "<>\n";
- }
-
- CallGraphWrapperPass::print(OS, 0);
- }
-
- virtual void releaseMemory() {
- destroy();
- }
-
- // getAdjustedAnalysisPointer - This method is used when a pass implements an
- // analysis interface through multiple inheritance. If needed, it should
- // override this to adjust the this pointer as needed for the specified pass
- // info.
- virtual void *getAdjustedAnalysisPointer(AnalysisID PI) {
- if (PI == CallGraphAnalysis::ID())
- return (CallGraph*)this;
- return this;
- }
-
- CallGraphNode* getExternalCallingNode() const { return ExternalCallingNode; }
- CallGraphNode* getCallsExternalNode() const { return CallsExternalNode; }
-
- // getRoot - Return the root of the call graph, which is either main, or if
- // main cannot be found, the external node.
- CallGraphNode *getRoot() { return Root; }
- const CallGraphNode *getRoot() const { return Root; }
-
-private:
- // addToCallGraph - Add a function to the call graph, and link the node to all
- // of the functions that it calls.
- void addToCallGraph(Function *F);
-
- // destroy - Release memory for the call graph
- virtual void destroy() {
- // CallsExternalNode is not in the function map, delete it explicitly.
- if (CallsExternalNode) {
- // CallsExternalNode->allReferencesDropped(); FIXME FIXME FIXME FIXME
- delete CallsExternalNode;
- CallsExternalNode = 0;
- }
- CallGraphWrapperPass::releaseMemory();
- }
-};
-
-}
-
-#endif // _DATA_STRUCTURE_CALLGRAPH_H
diff --git a/include/assistDS/FuncSimplify.h b/include/assistDS/FuncSimplify.h
deleted file mode 100644
index ad4a93648..000000000
--- a/include/assistDS/FuncSimplify.h
+++ /dev/null
@@ -1,30 +0,0 @@
-//===-------- ArgCast.cpp - Cast Arguments to Calls -----------------------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//===----------------------------------------------------------------------===//
-
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Pass.h"
-
-namespace llvm {
- //
- // Class: FuncSimplify
- //
- // Description:
- // Replace all internal aliases with the
- // aliasee value
- //
- class FuncSimplify : public ModulePass {
- public:
- static char ID;
- FuncSimplify() : ModulePass(ID) {}
- virtual bool runOnModule(Module& M);
- };
-}
-
diff --git a/include/assistDS/FuncSpec.h b/include/assistDS/FuncSpec.h
deleted file mode 100644
index 433d98c96..000000000
--- a/include/assistDS/FuncSpec.h
+++ /dev/null
@@ -1,35 +0,0 @@
-//===-- FuncSpec.cpp - Clone Functions With Constant Function Ptr Args ----===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// This pass clones functions that take constant function pointers as arguments
-// from some call sites. It changes those call sites to call cloned functions.
-//
-//===----------------------------------------------------------------------===//
-
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Pass.h"
-
-namespace llvm {
- //
- // Class: FuncSpec
- //
- // Description:
- // Implement an LLVM pass that clones functions which are passed
- // as an argument
- //
- //
- class FuncSpec : public ModulePass {
- public:
- static char ID;
- FuncSpec() : ModulePass(ID) {}
- virtual bool runOnModule(Module& M);
- };
-}
-
diff --git a/include/assistDS/GEPExprArgs.h b/include/assistDS/GEPExprArgs.h
deleted file mode 100644
index 201097bd5..000000000
--- a/include/assistDS/GEPExprArgs.h
+++ /dev/null
@@ -1,34 +0,0 @@
-
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// Identify GEPs used as arguments to call sites.
-//
-//===----------------------------------------------------------------------===//
-
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Pass.h"
-
-namespace llvm {
- //
- // Class: GEPExprArgs
- //
- // Description:
- // Implement an LLVM pass that clones functions which are passed GEPs
- // as an argument
- //
- //
- class GEPExprArgs : public ModulePass {
- public:
- static char ID;
- GEPExprArgs() : ModulePass(ID) {}
- virtual bool runOnModule(Module& M);
- };
-}
-
diff --git a/include/assistDS/IndCloner.h b/include/assistDS/IndCloner.h
deleted file mode 100644
index d99200ad6..000000000
--- a/include/assistDS/IndCloner.h
+++ /dev/null
@@ -1,34 +0,0 @@
-//===-- IndCloner.h - Clone Indirectly Called Functions -------------------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// This code defines a pass which clones functions which could potentially be
-// used in indirect function calls.
-//
-//===----------------------------------------------------------------------===//
-
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Pass.h"
-
-namespace llvm {
- //
- // Class: IndClone
- //
- // Description:
- // Implement an LLVM pass that clones functions which could be used for
- // indirect function calls.
- //
- class IndClone : public ModulePass {
- public:
- static char ID;
- IndClone() : ModulePass(ID) {}
- virtual bool runOnModule(Module& M);
- };
-}
-
diff --git a/include/assistDS/Int2PtrCmp.h b/include/assistDS/Int2PtrCmp.h
deleted file mode 100644
index e9356a97c..000000000
--- a/include/assistDS/Int2PtrCmp.h
+++ /dev/null
@@ -1,36 +0,0 @@
-//===-- Int2PtrCmp.cpp - Merge inttoptr/ptrtoint --------------------------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// Remove unnecessary inttoptr casts
-// Specially ones used in just compares
-// Most cases derived from InstCombine
-//
-//===----------------------------------------------------------------------===//
-
-#include "llvm/IR/DataLayout.h"
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Pass.h"
-
-
-namespace llvm {
- //
- // Class: Int2PtrCmp
- //
- //
- class Int2PtrCmp : public ModulePass {
- private:
- const DataLayout * TD;
- public:
- static char ID;
- Int2PtrCmp() : ModulePass(ID) {}
- virtual bool runOnModule(Module& M);
- };
-}
-
diff --git a/include/assistDS/LoadArgs.h b/include/assistDS/LoadArgs.h
deleted file mode 100644
index 760ce5c5b..000000000
--- a/include/assistDS/LoadArgs.h
+++ /dev/null
@@ -1,36 +0,0 @@
-//===-- LoadArgs.cpp - Promote args if they came from loads ---------------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// Identify calls, that are passed arguemtns that are LoadInsts.
-// Pass the original pointer instead. Helps improve some
-// context sensitivity.
-//
-//===----------------------------------------------------------------------===//
-
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Pass.h"
-
-namespace llvm {
- //
- // Class: LoadArgs
- //
- // Description:
- // Implement an LLVM pass that clones functions which are passed loads
- // as an argument
- //
- //
- class LoadArgs : public ModulePass {
- public:
- static char ID;
- LoadArgs() : ModulePass(ID) {}
- virtual bool runOnModule(Module& M);
- };
-}
-
diff --git a/include/assistDS/SimplifyGEP.h b/include/assistDS/SimplifyGEP.h
deleted file mode 100644
index e8a48749d..000000000
--- a/include/assistDS/SimplifyGEP.h
+++ /dev/null
@@ -1,32 +0,0 @@
-//===--------------- SimplifyGEP.cpp - Simplify GEPs types ---------------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// Simplify GEPs with bitcasts (mostly cloned from InstCombine)
-//
-//===----------------------------------------------------------------------===//
-
-#include "llvm/IR/DataLayout.h"
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Pass.h"
-
-namespace llvm {
- //
- // Class: SimplifyGEP
- //
- class SimplifyGEP : public ModulePass {
- private:
- const DataLayout * TD;
- public:
- static char ID;
- SimplifyGEP() : ModulePass(ID) {}
- virtual bool runOnModule(Module& M);
- };
-}
-
diff --git a/include/assistDS/SimplifyLoad.h b/include/assistDS/SimplifyLoad.h
deleted file mode 100644
index 75c03f852..000000000
--- a/include/assistDS/SimplifyLoad.h
+++ /dev/null
@@ -1,29 +0,0 @@
-//===--------------- SimplifyLoad.cpp - Simplify load insts ---------------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// Derived from InstCombine
-//
-//===----------------------------------------------------------------------===//
-
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Pass.h"
-
-namespace llvm {
- //
- // Class: SimplifyLoad
- //
- class SimplifyLoad : public ModulePass {
- public:
- static char ID;
- SimplifyLoad() : ModulePass(ID) {}
- virtual bool runOnModule(Module& M);
- };
-}
-
diff --git a/include/assistDS/StructReturnToPointer.h b/include/assistDS/StructReturnToPointer.h
deleted file mode 100644
index 9cbd01a36..000000000
--- a/include/assistDS/StructReturnToPointer.h
+++ /dev/null
@@ -1,30 +0,0 @@
-//===-------- StructReturnToPointer.cpp ------------------------------------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// For functions that return structures,
-// transform them to return a pointer to the structure instead.
-//
-//===----------------------------------------------------------------------===//
-
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Pass.h"
-
-namespace llvm {
- //
- // Class: StructRet
- //
- class StructRet : public ModulePass {
- public:
- static char ID;
- StructRet() : ModulePass(ID) {}
- virtual bool runOnModule(Module& M);
- };
-}
-
diff --git a/include/assistDS/TypeChecks.h b/include/assistDS/TypeChecks.h
deleted file mode 100644
index cf1cf2fea..000000000
--- a/include/assistDS/TypeChecks.h
+++ /dev/null
@@ -1,116 +0,0 @@
-//===------------- TypeChecks.h - Insert runtime type checks --------------===//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file was developed by the LLVM research group and is distributed under
-// the University of Illinois Open Source License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// This pass inserts checks to enforce type safety during runtime.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef TYPE_CHECKS_H
-#define TYPE_CHECKS_H
-
-#include "dsa/AddressTakenAnalysis.h"
-
-#include "llvm/IR/DataLayout.h"
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Function.h"
-#include "llvm/Pass.h"
-#include "llvm/IR/CallSite.h"
-#include "llvm/IR/Dominators.h"
-#include "llvm/Analysis/LoopInfo.h"
-
-#include