Merge branch 'release-2.4.1'

smackers · Apr 10, 2020 · 212bbdb · 212bbdb
2 parents cff319a + ad34548
commit 212bbdb
Show file tree

Hide file tree

Showing 754 changed files with 2,441 additions and 20,916 deletions.
diff --git a/.gitmodules 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
@@ -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
@@ -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
@@ -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
@@ -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">

diff --git a/bin/boogie b/bin/boogie