From 43fa3638d89ceabb0bed51dbd16dc58d089f0d1e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hans-J=C3=B6rg=20Schurr?= Date: Thu, 20 Jul 2023 18:55:39 -0500 Subject: [PATCH 1/2] Add cmake build files and Github workflow --- .github/workflows/main.yml | 43 ++++++++++++++++++++++++++++++++++++++ .gitignore | 1 + CMakeLists.txt | 40 +++++++++++++++++++++++++++++++++++ cmake/FindGMP.cmake | 12 +++++++++++ proofs/CMakeLists.txt | 20 ++++++++++++++++++ src/CMakeLists.txt | 3 +++ tests/CMakeLists.txt | 27 ++++++++++++++++++++++++ 7 files changed, 146 insertions(+) create mode 100644 .github/workflows/main.yml create mode 100644 .gitignore create mode 100644 CMakeLists.txt create mode 100644 cmake/FindGMP.cmake create mode 100644 proofs/CMakeLists.txt create mode 100644 src/CMakeLists.txt create mode 100644 tests/CMakeLists.txt diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml new file mode 100644 index 0000000..b9b7209 --- /dev/null +++ b/.github/workflows/main.yml @@ -0,0 +1,43 @@ +name: CI + +on: + push: + branches: [ master, ci-test ] + pull_request: + branches: [ master ] + +jobs: + build: + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + name: [ production ] + + name: ${{ matrix.os }}:${{ matrix.name }} + # The type of runner that the job will run on + runs-on: ${{ matrix.os }} + + steps: + - uses: actions/checkout@v2 + - name: Install Packages + if: runner.os == 'Linux' + run: | + sudo apt-get update + sudo apt-get install -y \ + libgmp-dev + - name: Install Packages (MacOS) + if: runner.os == 'macOS' + run: | + brew install \ + gmp + - name: Setup Build Dir + run: mkdir build + - name: Configure + run: cmake .. + working-directory: build + - name: Build + run: make -j2 + working-directory: build + - name: Test + run: ctest --output-on-failure + working-directory: build diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..378eac2 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +build diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 0000000..b1535e7 --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,40 @@ +cmake_minimum_required (VERSION 3.12) + +macro(add_cxx_flag flag) + message(STATUS "Configure with flag '${flag}'") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}") +endmacro() + +project (alethelf_checker) + +set (CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) + +find_package(GMP REQUIRED) +set(LIBRARIES ${LIBRARIES} ${GMP_LIBRARIES}) +include_directories(${GMP_INCLUDE_DIR}) + +if(NOT CMAKE_BUILD_TYPE) + message(STATUS "Defaulting to release build.") + set(CMAKE_BUILD_TYPE Release CACHE STRING "" FORCE) +endif() + +add_cxx_flag("-Wall") +add_cxx_flag("-Wno-deprecated") +add_cxx_flag("-std=gnu++17") + +if(CMAKE_BUILD_TYPE STREQUAL "Debug") + add_cxx_flag("-g") + message(STATUS "Configured debug build.") +elseif(CMAKE_BUILD_TYPE STREQUAL "Release") + message(STATUS "Configured release build.") +else() + message(FATAL_ERROR "Invalid build type '${CMAKE_BUILD_TYPE}'") +endif() + +enable_testing() + +include_directories(src) +add_subdirectory(src) +add_subdirectory(tests) +add_subdirectory(proofs) + diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake new file mode 100644 index 0000000..4325f66 --- /dev/null +++ b/cmake/FindGMP.cmake @@ -0,0 +1,12 @@ +# Try to find the GMP librairies +# GMP_FOUND - system has GMP lib +# GMP_INCLUDE_DIR - the GMP include directory +# GMP_LIBRARIES - Libraries needed to use GMP + +find_path(GMP_INCLUDE_DIR NAMES gmp.h) +find_library(GMP_LIBRARIES NAMES gmp libgmp) + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES) + +mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES) diff --git a/proofs/CMakeLists.txt b/proofs/CMakeLists.txt new file mode 100644 index 0000000..d02537b --- /dev/null +++ b/proofs/CMakeLists.txt @@ -0,0 +1,20 @@ +set(atc_test_file_list + theories/ArithBridge.smt2 + theories/BitVectors.smt2 + theories/Core.smt2 + theories/Ints.smt2 + theories/Reals.smt2 +) + +macro(atc_test file) + add_test( + NAME ${file} + COMMAND $ ${CMAKE_CURRENT_LIST_DIR}/${file} + WORKING_DIRECTORY ${CMAKE_SOURCE_DIR} + ) + set_tests_properties(${file} PROPERTIES TIMEOUT 40) +endmacro() + +foreach(file ${atc_test_file_list}) + atc_test(${file}) +endforeach() \ No newline at end of file diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt new file mode 100644 index 0000000..9c0b3d7 --- /dev/null +++ b/src/CMakeLists.txt @@ -0,0 +1,3 @@ +file(GLOB atc_SRC CONFIGURE_DEPENDS "*.h" "*.cpp") + +add_executable(atc ${atc_SRC}) diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt new file mode 100644 index 0000000..b41b994 --- /dev/null +++ b/tests/CMakeLists.txt @@ -0,0 +1,27 @@ +set(atc_test_file_list + Bools.smt2 + literals.smt2 + simple-pf2.smt2 + simple.smt2 + bv-dep-type.smt2 + quoted.smt2 + simple-pf-implicit.smt2 + requires.smt2 + simple-pf.smt2 + evaluate.smt2 + simple-include.smt2 + simple-program.smt2 +) + +macro(atc_test file) + add_test( + NAME ${file} + COMMAND $ ${CMAKE_CURRENT_LIST_DIR}/${file} + WORKING_DIRECTORY ${CMAKE_SOURCE_DIR} + ) + set_tests_properties(${file} PROPERTIES TIMEOUT 40) +endmacro() + +foreach(file ${atc_test_file_list}) + atc_test(${file}) +endforeach() \ No newline at end of file From 2e626fa2c01e73b4ddeb6b6f7f63eba6dfb8bd12 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hans-J=C3=B6rg=20Schurr?= Date: Thu, 20 Jul 2023 19:16:45 -0500 Subject: [PATCH 2/2] Fix on part of workflow file --- .github/workflows/main.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index b9b7209..9f33a7a 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -2,9 +2,9 @@ name: CI on: push: - branches: [ master, ci-test ] + branches: [ main, devel/cmake ] pull_request: - branches: [ master ] + branches: [ main ] jobs: build: