Merge pull request diffblue#203 from diffblue/feature/cmake

SEC-62 : Introducing CMAKE build system for security-analyser and removal of Makefile system.

Author: marek-trtik

.gitignore

@@ -11,8 +11,10 @@ src/goto-analyzer/taint_driver_scripts/.idea/*
 /*.creator.user
 /*.files
 /*.includes
-security-scanner/.idea
-security-scanner/*.pyc
+driver/.idea
+driver/*.pyc
+build
+dist
 
 # Ignoring boost
 boost/*

.travis.yml

@@ -39,8 +39,11 @@ jobs:
             - libubsan0
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
-      # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
-      env: COMPILER="ccache g++-5"
+      env:
+        - COMPILER="g++-5"
+        - BUILD_TYPE="Release"
+        - RUN_CBMC_TESTS="true"
+        - RUN_SECURITY_TESTS="true"
 
 # LOCAL CHANGES: Added 'ant' to the OSX package list (needed by security-scanner regression tests)
 
@@ -55,7 +58,11 @@ jobs:
         - mkdir bin ; ln -s /usr/bin/gcc bin/gcc
         - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache ant
         - export PATH=/usr/local/opt/ccache/libexec:$PATH
-      env: COMPILER="ccache g++"
+      env:
+        - COMPILER="g++"
+        - BUILD_TYPE="Release"
+        - RUN_CBMC_TESTS="true"
+        - RUN_SECURITY_TESTS="true"
 
     # OS X using clang++
     - stage: Test different OS/CXX/Flags
@@ -67,12 +74,16 @@ jobs:
         - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache ant
         - export PATH=/usr/local/opt/ccache/libexec:$PATH
       env:
-        - COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
+        - COMPILER="clang++"
+        - BUILD_TYPE="Release"
+        - RUN_CBMC_TESTS="true"
+        - RUN_SECURITY_TESTS="true"
         - CCACHE_CPP2=yes
 
     # Ubuntu Linux with glibc using g++-5, debug mode
     - stage: Test different OS/CXX/Flags
       os: linux
+      dist: trusty
       sudo: false
       compiler: gcc
       cache: ccache
@@ -82,19 +93,24 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - libwww-perl
+            - libthread-pool-simple-perl
             - g++-5
             - libubsan0
+            - parallel
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
-      # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env:
-        - COMPILER="ccache g++-5"
-        - EXTRA_CXXFLAGS="-DDEBUG"
-      script: echo "Not running any tests for a debug build."
+        - COMPILER="g++-5"
+        - BUILD_TYPE="Debug"
+        - RUN_CBMC_TESTS="false"
+        - RUN_SECURITY_TESTS="true"
+        - OS="ubuntu"
+        - TEST_MODELS_LIB="false"
 
     # Ubuntu Linux with glibc using clang++-3.7
     - stage: Test different OS/CXX/Flags
       os: linux
+      dist: trusty
       sudo: false
       compiler: clang
       cache: ccache
@@ -105,16 +121,21 @@ jobs:
             - llvm-toolchain-precise-3.7
           packages:
             - libwww-perl
+            - libthread-pool-simple-perl
             - clang-3.7
             - libstdc++-5-dev
             - libubsan0
+            - parallel
       before_install:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
         - export CCACHE_CPP2=yes
-      # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env:
-        - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
+        - COMPILER="clang++-3.7"
+        - BUILD_TYPE="Release"
+        - RUN_CBMC_TESTS="true"
+        - RUN_SECURITY_TESTS="true"
         - CCACHE_CPP2=yes
+        - OS="ubuntu"
 
     # Ubuntu Linux with glibc using clang++-3.7, debug mode
     - stage: Test different OS/CXX/Flags
@@ -135,39 +156,12 @@ jobs:
       before_install:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
         - export CCACHE_CPP2=yes
-      # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env:
-        - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
+        - COMPILER="clang++-3.7"
+        - BUILD_TYPE="Debug"
+        - RUN_CBMC_TESTS="false"
+        - RUN_SECURITY_TESTS="true"
         - CCACHE_CPP2=yes
-        - EXTRA_CXXFLAGS="-DDEBUG"
-      script: echo "Not running any tests for a debug build."
-
-    - stage: Test different OS/CXX/Flags
-      os: linux
-      cache: ccache
-      env:
-        - BUILD_SYSTEM=cmake
-      addons:
-        apt:
-          sources:
-            - ubuntu-toolchain-r-test
-          packages:
-            - g++-5
-      install:
-        - cmake -Hcbmc -Bcbmc/build '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
-        - cmake --build cbmc/build -- -j4
-      script: (cd cbmc/build; ctest -V -L CORE)
-
-    - stage: Test different OS/CXX/Flags
-      os: osx
-      cache: ccache
-      env:
-        - BUILD_SYSTEM=cmake
-        - CCACHE_CPP2=yes
-      install:
-        - cmake -Hcbmc -Bcbmc/build '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
-        - cmake --build cbmc/build -- -j4
-      script: (cd cbmc/build; ctest -V -L CORE)
 
 
   allow_failures:
@@ -178,20 +172,13 @@ jobs:
 
 install:
   - ccache --max-size=1G
-  - make -C cbmc/src minisat2-download
-  - make -C cbmc/src boost-download
-  - make -C cbmc/src/ansi-c library_check
-  - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g -DUSE_BOOST ${EXTRA_CXXFLAGS}" -j2
-  - make -C cbmc/src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2 goto-analyzer.dir goto-cc.dir goto-diff.dir clobber.dir memory-models.dir
+  - cmake . -Bbuild "-DCMAKE_CXX_COMPILER=${COMPILER}" "-DCMAKE_BUILD_TYPE=${BUILD_TYPE}" "-Denable_security_tests=${RUN_SECURITY_TESTS}" "-Denable_cbmc_tests=${RUN_CBMC_TESTS}"
+  - ( cd build; make install )
 
 # LOCAL CHANGES: Added cbmc/ prefix, and added unit and regression tests to the end of the list.
 
 script:
-  - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-  - env UBSAN_OPTIONS=print_stacktrace=1 make -C cbmc/regression test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}"
-  - make -C cbmc/unit "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
-  - make -C cbmc/unit test
-  - make -C unit test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g -DUSE_BOOST ${EXTRA_CXXFLAGS}"
+  - ( cd build; ctest -V -L CORE )
   - scripts/travis_run_regression_tests.sh
 
 before_cache:

CMakeLists.txt

@@ -0,0 +1,86 @@
+cmake_minimum_required(VERSION 3.2)
+
+project(security-scanner)
+
+if(CMAKE_INSTALL_PREFIX_INITIALIZED_TO_DEFAULT)
+  set(CMAKE_INSTALL_PREFIX "${CMAKE_CURRENT_SOURCE_DIR}/dist" CACHE PATH "Specify the installation directory for the security-scanner." FORCE)
+endif()
+
+if(NOT CMAKE_BUILD_TYPE)
+  set(CMAKE_BUILD_TYPE "Release" CACHE STRING "Choose the type of build, options are: Debug, Release, RelWithDebInfo, MinSizeRel." FORCE)
+endif()
+
+find_program(CCACHE_PROGRAM ccache)
+if(CCACHE_PROGRAM)
+    set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
+    message(STATUS "Rule launch compile: ${CCACHE_PROGRAM}")
+endif()
+
+set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
+
+include(GNUInstallDirs)
+
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+
+set(custom_cxx_flags "" CACHE STRING "Extra flags used to build CXX files")
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+   "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
+)
+    #   Ensure NDEBUG is not set for release builds
+    set(CMAKE_CXX_FLAGS_RELEASE "-O2")
+    #   Enable lots of warnings
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror")
+elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+    #   This would be the place to enable warnings for Windows builds, although
+    #   config.inc doesn't seem to do that currently
+endif()
+
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED true)
+
+set(CMAKE_EXPORT_COMPILE_COMMANDS true)
+
+set(enable_security_tests on CACHE BOOL "Whether tests of the security analyser should be enabled.")
+set(enable_cbmc_tests off CACHE BOOL "Whether CBMC tests should be enabled (the default is to enable just test-gen tests)")
+
+################################################################################
+# BOOST
+
+set(boost_include_root_dir "${CMAKE_CURRENT_SOURCE_DIR}/cbmc/boost-include" )
+set(boost_include_package_download_dir "${boost_include_root_dir}/download" )
+set(boost_include_package_name "boost_1.63_headers.tar.bz2" )
+set(boost_include_package_URL "http://storage.googleapis.com/diffblue-mirror/boost/boost_1.63_headers.tar.bz2?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1542631994&Signature=X2GwPSm1dR8IPGP0D5JoyDmOnL%2Br4F7AI7NUA7SbmOAowMC0JS7Q5A6%2BkQziUzQa88zpddr5gSRbDOLqdoGzwLrYgPNtURS5dJ7l1q6xfJWSS%2FYf8be%2FSbdfLVN8qcXKCsfDe05Hqf%2Bz2cksqjQ1H6L0syj43rftbW4%2F7tp355%2BkinCeE466ulJeyru3CK%2F3RGX2Ul6ZQV6lNxkit1m6QM5BRtLbUQ1GOW0GCK9fWH2fry2n7kRVBCM3oz8fX62kLdKYlaXCf%2BvvXs9hOOmcQurL%2Fa4DCJYoClX%2BpznqXVmjUY%2FI3pD4HlRKbCeiPnoC6de2i1uxFNSVTBpG3w%2BtfA%3D%3D" )
+set(boost_include_include_dir "${boost_include_root_dir}")
+if (NOT EXISTS "${boost_include_package_download_dir}/${boost_include_package_name}")
+    file(DOWNLOAD "${boost_include_package_URL}" "${boost_include_package_download_dir}/${boost_include_package_name}")
+endif()
+
+include(ExternalProject)
+ExternalProject_Add(boost-include
+    PREFIX "${boost_include_root_dir}"
+    SOURCE_DIR "${boost_include_include_dir}/boost"
+    URL "${boost_include_package_download_dir}/${boost_include_package_name}"
+    CONFIGURE_COMMAND ""
+    BUILD_COMMAND ""
+    INSTALL_COMMAND ""
+    )
+
+################################################################################
+
+add_subdirectory(cbmc)
+add_subdirectory(benchmarks/LIBRARIES/models)
+
+add_subdirectory(src)
+
+if(${enable_security_tests})
+    enable_testing()
+endif()
+add_subdirectory(unit)
+add_subdirectory(regression)
+
+install(FILES "./security-analyser.md" DESTINATION doc)
+install(FILES "./security-analyser-driver.py" DESTINATION bin)
+install(DIRECTORY "./driver" DESTINATION lib FILES_MATCHING PATTERN "*.py")

benchmarks/evaluator.py

@@ -135,7 +135,7 @@ def __evaluate_benchmark(record):
 
     # Now we can run the security-scanner on the installed benchmark
     command = (
-        "python \"" + os.path.join(__get_my_dir(), "..", "security-scanner", "run.py") + "\" " +
+        "python \"" + os.path.join(__get_my_dir(), "..", "dist", "lib", "driver", "run.py") + "\" " +
         "-C \"" + os.path.join(__get_my_dir(), record["rules-file"]) + "\" " +
         "-I \"" + os.path.join(__get_my_dir(), record["install-dir"]) + "\" " +
         "-R \"" + os.path.join(__get_my_dir(), record["results-dir"]) + "\" " +

cbmc/src/goto-instrument/CMakeLists.txt

@@ -34,3 +34,5 @@ add_if_library(goto-instrument-lib glpk)
 # Executable
 add_executable(goto-instrument goto_instrument_main.cpp)
 target_link_libraries(goto-instrument goto-instrument-lib)
+
+install(TARGETS goto-instrument DESTINATION bin)

cbmc/src/symex/CMakeLists.txt

@@ -33,3 +33,5 @@ add_if_library(symex-lib php)
 add_executable(symex symex_main.cpp)
 
 target_link_libraries(symex symex-lib)
+
+install(TARGETS symex DESTINATION bin)

security-scanner/__diffblue_full_class_name_parser__.java renamed to driver/__diffblue_full_class_name_parser__.java

@@ -8,16 +8,16 @@ def __get_my_dir(): return os.path.dirname(os.path.realpath(__file__))
 
 
 def get_security_analyser_pathname():
-    return os.path.abspath(os.path.join(__get_my_dir(), "../src/driver/security-analyzer"))
+    return os.path.abspath(os.path.join(__get_my_dir(), "../../bin/security-analyzer"))
 
 def get_goto_instrument_pathname():
-    return os.path.abspath(os.path.join(__get_my_dir(), "../cbmc/src/goto-instrument/goto-instrument"))
+    return os.path.abspath(os.path.join(__get_my_dir(), "../../bin/goto-instrument"))
 
 def get_cbmc_pathname():
-    return os.path.abspath(os.path.join(__get_my_dir(), "../cbmc/src/cbmc/cbmc"))
+    return os.path.abspath(os.path.join(__get_my_dir(), "../../bin/cbmc"))
 
 def get_symex_pathname():
-    return os.path.abspath(os.path.join(__get_my_dir(), "../cbmc/src/symex/symex"))
+    return os.path.abspath(os.path.join(__get_my_dir(), "../../bin/symex"))
 
 
 def run_security_analyser(

security-scanner/__init__.py renamed to driver/__init__.py

@@ -0,0 +1,2 @@
+# We do not have any regression test so far.
+

security-scanner/analyser.py renamed to driver/analyser.py

@@ -7,4 +7,5 @@ if [[ "$CBMC_ALPINE_BUILD" == "yes" ]]; then
   exit 0
 fi
 
-make -C $THISDIR/.. regression
+python $THISDIR/../benchmarks/evaluator.py
+

security-scanner/build.xml renamed to driver/build.xml

@@ -0,0 +1,2 @@
+# TODO: this script should only forwrad its input to the driver script.
+#       Implement it! Until then, this script is bypassed by the evaluator.

security-scanner/mkbench.py renamed to driver/mkbench.py

@@ -0,0 +1 @@
+TODO: add guide how to use the security-analyser product!

security-scanner/mkplot.py renamed to driver/mkplot.py

@@ -0,0 +1,23 @@
+project(SECURITY_ANALYSER)
+
+#   Set the public include locations for a target.
+macro(generic_includes name)
+    target_include_directories(${name}
+        PUBLIC
+        ${SECURITY_ANALYSER_BINARY_DIR}
+        ${SECURITY_ANALYSER_SOURCE_DIR}
+        ${CMAKE_CURRENT_BINARY_DIR}
+        ${CMAKE_CURRENT_SOURCE_DIR}
+        ${CBMC_SOURCE_DIR}
+        ${boost_include_include_dir}
+    )
+endmacro(generic_includes)
+
+
+add_subdirectory(driver)
+add_subdirectory(pointer-analysis)
+add_subdirectory(summaries)
+add_subdirectory(taint-analysis)
+add_subdirectory(taint-slicer)
+add_subdirectory(util)
+