Skip to content

Commit

Permalink
Merge branch 'release-2.4.1'
Browse files Browse the repository at this point in the history
  • Loading branch information
zvonimir committed Apr 10, 2020
2 parents cff319a + ad34548 commit 212bbdb
Show file tree
Hide file tree
Showing 754 changed files with 2,441 additions and 20,916 deletions.
4 changes: 4 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
[submodule "sea-dsa"]
path = sea-dsa
url = https://github.com/seahorn/sea-dsa.git
branch = llvm-8.0
54 changes: 31 additions & 23 deletions .travis.yml
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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
Expand All @@ -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
142 changes: 53 additions & 89 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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}")
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Doxyfile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -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) |
| --- | --- | --- | --- |

<img src="docs/smack-logo.png" width=400 alt="SMACK Logo" align="right">
Expand Down
6 changes: 0 additions & 6 deletions bin/boogie

This file was deleted.

Loading

0 comments on commit 212bbdb

Please sign in to comment.