Merge branch 'release-2.7.0'

.github/workflows/smack-ci.yaml

@@ -4,15 +4,10 @@ on: [push, pull_request]
 
 jobs:
   check-regressions:
-    env:
-      COMPILER_NAME: clang
-      COMPILER: clang++
-      CXX: clang++
-      CC: clang
     runs-on: ubuntu-20.04
     strategy:
       matrix:
-        travis_env:
+        regtest_env:
           [
             "--exhaustive --folder=c/basic",
             "--exhaustive --folder=c/data",
@@ -37,7 +32,9 @@ jobs:
             "--exhaustive --folder=rust/panic --languages=rust",
             "--exhaustive --folder=rust/recursion --languages=rust",
             "--exhaustive --folder=rust/structures --languages=rust",
-            "--exhaustive --folder=rust/vector --languages=rust"
+            "--exhaustive --folder=rust/vector --languages=rust",
+            "--exhaustive --folder=rust/cargo/** --languages=cargo --threads=1",
+            "--exhaustive --folder=llvm --languages=llvm-ir"
           ]
     steps:
       - uses: actions/checkout@v2
@@ -47,20 +44,58 @@ jobs:
           GITHUB_ACTIONS: true
         run: INSTALL_DEV_DEPENDENCIES=1 INSTALL_RUST=1 ./bin/build.sh
 
-      - run: python3 --version
-      - run: $CXX --version
-      - run: $CC --version
-      - run: clang --version
-      - run: clang++ --version
-      - run: llvm-link --version
-      - run: llvm-config --version
-
       - name: format checking
         run: |
           ./format/run-clang-format.py -r lib/smack include/smack tools share/smack/include share/smack/lib test examples
           flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py
-      
+
       - name: compile and test
         env:
-          TRAVIS_ENV: ${{ matrix.travis_env }}
+          REGTEST_ENV: ${{ matrix.regtest_env }}
         run: ./bin/build.sh
+
+  build-and-push-docker:
+    runs-on: ubuntu-20.04
+    needs: check-regressions
+
+    steps:
+      - name: Check Out Repo
+        uses: actions/checkout@v2
+
+      - name: Login to Docker Hub
+        uses: docker/login-action@v1
+        with:
+          username: ${{ secrets.DOCKER_HUB_USERNAME }}
+          password: ${{ secrets.DOCKER_HUB_ACCESS_TOKEN }}
+
+      - name: Set up Docker Buildx
+        id: buildx
+        uses: docker/setup-buildx-action@v1
+
+      # borrowed from:
+      # https://stackoverflow.com/questions/58033366/how-to-get-current-branch-within-github-actions/58035262
+      - name: Extract branch name
+        shell: bash
+        run: echo "##[set-output name=branch;]$(echo ${GITHUB_REF#refs/heads/})"
+        id: extract_branch
+
+      - name: Set tag name
+        shell: bash
+        id: set_tag
+        run: |
+          if [ ${{ steps.extract_branch.outputs.branch }} == 'master' ]; then echo "##[set-output name=docker_tag;]$(echo stable)" && exit 0; fi
+          if [ ${{ steps.extract_branch.outputs.branch }} == 'develop' ]; then echo "##[set-output name=docker_tag;]$(echo latest)" && exit 0; fi
+          echo "##[set-output name=docker_tag;]$(echo none)"
+
+      - name: Build and push
+        if: ${{ steps.set_tag.outputs.docker_tag != 'none' }}
+        id: docker_build
+        uses: docker/build-push-action@v2
+        with:
+          context: ./
+          file: ./Dockerfile
+          push: true
+          tags: smackers/smack:${{ steps.set_tag.outputs.docker_tag }}
+
+      - name: Image digest
+        run: echo ${{ steps.docker_build.outputs.digest }}

CMakeLists.txt

@@ -5,14 +5,20 @@
 cmake_minimum_required(VERSION 3.4.3)
 project(smack)
 
-if (NOT WIN32 OR MSYS OR CYGWIN)
+if(NOT WIN32 OR MSYS OR CYGWIN)
 
-  file(STRINGS "bin/versions" LLVM_VERSION_STR REGEX "LLVM_SHORT_VERSION=\"[0-9]+\"")
+  file(STRINGS "bin/versions" LLVM_VERSION_STR
+    REGEX "LLVM_FULL_VERSION=\"[0-9]+\.[0-9]+\.[0-9]+")
+  string(REGEX MATCH "[0-9]+\.[0-9]+" LLVM_EXTENDED_VERSION "${LLVM_VERSION_STR}")
+
+  file(STRINGS "bin/versions" LLVM_VERSION_STR
+    REGEX "LLVM_SHORT_VERSION=\"[0-9]+")
   string(REGEX MATCH "[0-9]+" LLVM_SHORT_VERSION "${LLVM_VERSION_STR}")
 
-  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-${LLVM_SHORT_VERSION} llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-${LLVM_SHORT_VERSION}
+    llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
 
-  if (LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND")
+  if(LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND")
     message(FATAL_ERROR "llvm-config could not be found!")
   endif()
 
@@ -22,36 +28,12 @@ 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}")
-  string(REPLACE "--no-keep-files-mapped" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
-  string(REPLACE "--no-map-whole-files" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
-  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")
-
-  # 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")
+  # SMACK doesn't catch or throw exceptions, so -fno-exceptions is justified.
+  # SMACK doesn't use C++ runtime type identification features, so -fno-rtti
+  # is justified.
+  # Shaobo: enable O3 so SMACK can save some time.
+  set(CMAKE_CXX_FLAGS
+    "${LLVM_CXXFLAGS} -fno-exceptions -fno-rtti -O3")
 
   execute_process(
     COMMAND ${LLVM_CONFIG_EXECUTABLE} --libs
@@ -76,12 +58,12 @@ else()
   set(LLVM_BUILD "" CACHE PATH "LLVM build directory")
   set(LLVM_BUILD_TYPE "" CACHE STRING "LLVM build type")
 
-  if (NOT EXISTS "${LLVM_SRC}/include/llvm")
+  if(NOT EXISTS "${LLVM_SRC}/include/llvm")
     message(FATAL_ERROR "Invalid LLVM source directory: ${LLVM_SRC}")
   endif()
 
   set(LLVM_LIBDIR "${LLVM_BUILD}/lib/${LLVM_BUILD_TYPE}")
-  if (NOT EXISTS "${LLVM_LIBDIR}")
+  if(NOT EXISTS "${LLVM_LIBDIR}")
     message(FATAL_ERROR "Invalid LLVM build directory: ${LLVM_BUILD}")
   endif()
 
@@ -92,7 +74,11 @@ else()
   set(CMAKE_CXX_FLAGS "\"/I${LLVM_SRC}/include\" \"/I${LLVM_BUILD}/include\" -D_SCL_SECURE_NO_WARNINGS -wd4146 -wd4244 -wd4355 -wd4482 -wd4800")
 
   set(LLVM_LDFLAGS "")
-  set(LLVM_LIBS "${LLVM_LIBDIR}/LLVMTransformUtils.lib" "${LLVM_LIBDIR}/LLVMipa.lib" "${LLVM_LIBDIR}/LLVMAnalysis.lib" "${LLVM_LIBDIR}/LLVMTarget.lib" "${LLVM_LIBDIR}/LLVMMC.lib" "${LLVM_LIBDIR}/LLVMObject.lib" "${LLVM_LIBDIR}/LLVMBitReader.lib" "${LLVM_LIBDIR}/LLVMCore.lib" "${LLVM_LIBDIR}/LLVMSupport.lib")
+  set(LLVM_LIBS "${LLVM_LIBDIR}/LLVMTransformUtils.lib"
+    "${LLVM_LIBDIR}/LLVMipa.lib" "${LLVM_LIBDIR}/LLVMAnalysis.lib"
+    "${LLVM_LIBDIR}/LLVMTarget.lib" "${LLVM_LIBDIR}/LLVMMC.lib"
+    "${LLVM_LIBDIR}/LLVMObject.lib" "${LLVM_LIBDIR}/LLVMBitReader.lib"
+    "${LLVM_LIBDIR}/LLVMCore.lib" "${LLVM_LIBDIR}/LLVMSupport.lib")
 
 endif()
 
@@ -170,13 +156,17 @@ add_executable(llvm2bpl
 )
 
 # 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 ()
+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 ${LLVM_SHORT_VERSION} CONFIG)
+# Borrowed from https://github.com/banach-space/llvm-tutor/commit/72cb20d058b9b3f51717c7a17607f7a4c7398642
+find_package (LLVM ${LLVM_EXTENDED_VERSION} REQUIRED CONFIG)
+if (NOT ${LLVM_SHORT_VERSION} VERSION_EQUAL "${LLVM_VERSION_MAJOR}")
+  message(FATAL_ERROR "Found LLVM ${LLVM_VERSION_MAJOR}, but need ${LLVM_SHORT_VERSION}")
+endif ()
 list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")
 include(AddLLVM)
 include(HandleLLVMOptions)
@@ -188,14 +178,15 @@ set(CMAKE_BUILD_TYPE "Release")
 add_subdirectory(sea-dsa/lib/seadsa)
 set(CMAKE_BUILD_TYPE ${SMACK_BUILD_TYPE})
 
-target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS} ${LLVM_LDFLAGS})
+target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS}
+  ${LLVM_LDFLAGS})
 target_link_libraries(llvm2bpl smackTranslator utils SeaDsaAnalysis)
 
-INSTALL(TARGETS llvm2bpl
+install(TARGETS llvm2bpl
   RUNTIME DESTINATION bin
 )
 
-INSTALL(FILES
+install(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-doctor
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-svcomp-wrapper.sh
@@ -204,30 +195,31 @@ INSTALL(FILES
   DESTINATION bin
 )
 
-INSTALL(DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/share/smack
+install(DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/share/smack
   DESTINATION share
   USE_SOURCE_PERMISSIONS
-  FILES_MATCHING PATTERN "*.py" PATTERN "*.h" PATTERN "*.c" PATTERN "Makefile" PATTERN "*.rs" PATTERN "*.f90" PATTERN "*.di" PATTERN "*.toml"
+  FILES_MATCHING PATTERN "*.py" PATTERN "*.h" PATTERN "*.c" PATTERN "Makefile"
+    PATTERN "*.rs" PATTERN "*.f90" PATTERN "*.di" PATTERN "*.toml"
 )
 
-INSTALL(FILES
+install(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/versions
   DESTINATION share/smack
   RENAME versions.py
 )
 
-INSTALL(FILES
+install(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack/Cargo.toml
   ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack/build.rs
   DESTINATION share/smack/lib
 )
 
-INSTALL(FILES
+install(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack-rust.c
   DESTINATION share/smack/lib/src
 )
 
-INSTALL(FILES
+install(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack.rs
   DESTINATION share/smack/lib/src
   RENAME lib.rs

Dockerfile

@@ -1,13 +1,14 @@
-FROM ubuntu:18.04
-MAINTAINER Shaobo He <[email protected]>
+FROM ubuntu:20.04
+MAINTAINER Shaobo He <[email protected]>
 
 ENV SMACKDIR /home/user/smack
 
 RUN apt-get update && \
       apt-get -y install \
       software-properties-common \
       wget \
-      sudo
+      sudo \
+      g++
 
 # Borrowed from JFS
 # Create `user` user for container with password `user`.  and give it
@@ -26,7 +27,7 @@ ADD --chown=user . $SMACKDIR
 WORKDIR $SMACKDIR
 
 # Build SMACK
-RUN sudo bin/build.sh
+RUN bin/build.sh
 
 # Add envinronment
 RUN echo "source /home/user/smack.environment" >> ~/.bashrc

Doxyfile

@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 2.6.3
+PROJECT_NUMBER         = 2.7.0
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs

LICENSE

@@ -1,8 +1,8 @@
 The MIT License
 
-Copyright (c) 2008-2020 Zvonimir Rakamaric ([email protected]),
+Copyright (c) 2008-2021 Zvonimir Rakamaric ([email protected]),
                         Michael Emmi ([email protected])
-Modified work Copyright (c) 2013-2020 Marek Baranowski,
+Modified work Copyright (c) 2013-2021 Marek Baranowski,
                                       Montgomery Carter,
                                       Pantazis Deligiannis,
                                       Jack J. Garzella,

README.md

@@ -48,7 +48,7 @@ See below for system requirements, installation, usage, and everything else.
 ### Acknowledgements
 
 SMACK project has been partially supported by funding from the National Science
-Foundation, VMware, and Microsoft Research. We also rely on University of
+Foundation, VMware, Amazon, and Microsoft Research. We also rely on University of
 Utah's [Emulab](http://www.emulab.net/) infrastructure for extensive
 benchmarking of SMACK.
 

Vagrantfile

@@ -26,8 +26,8 @@ Vagrant.configure(2) do |config|
   # end
 
   config.vm.provision "shell", binary: true, privileged: false, inline: <<-SHELL
-    apt-get update
-    apt-get install -y software-properties-common
+    sudo apt update
+    sudo apt install -y build-essential
     cd /home/vagrant
     ./#{project_name}/bin/build.sh
     echo source smack.environment >> .bashrc