From 4f3c2eef2fdfa503f864bd509fff63cfe0cb9a9b Mon Sep 17 00:00:00 2001 From: Igor Abdrakhimov Date: Tue, 26 Nov 2024 10:31:58 -0800 Subject: [PATCH 1/2] Forward CMake variables to prebuilding dependencies (#1161) Co-authored-by: Igor Abdrakhimov Co-authored-by: Michael Graeb --- cmake/AwsPrebuildDependency.cmake | 80 +++++++++++++++++++++++++++++-- 1 file changed, 77 insertions(+), 3 deletions(-) diff --git a/cmake/AwsPrebuildDependency.cmake b/cmake/AwsPrebuildDependency.cmake index 0a52f69a8..2637f9594 100644 --- a/cmake/AwsPrebuildDependency.cmake +++ b/cmake/AwsPrebuildDependency.cmake @@ -13,11 +13,11 @@ function(aws_prebuild_dependency) set(multiValueArgs CMAKE_ARGUMENTS) cmake_parse_arguments(AWS_PREBUILD "" "${oneValueArgs}" "${multiValueArgs}" ${ARGN}) - if(NOT AWS_PREBUILD_DEPENDENCY_NAME) + if (NOT AWS_PREBUILD_DEPENDENCY_NAME) message(FATAL_ERROR "Missing DEPENDENCY_NAME argument in prebuild_dependency function") endif() - if(NOT AWS_PREBUILD_SOURCE_DIR) + if (NOT AWS_PREBUILD_SOURCE_DIR) message(FATAL_ERROR "Missing SOURCE_DIR argument in prebuild_dependency function") endif() @@ -29,18 +29,31 @@ function(aws_prebuild_dependency) string(REPLACE ";" "\\\\;" ESCAPED_PREFIX_PATH "${CMAKE_PREFIX_PATH}") # For execute_process to accept a dynamically constructed command, it should be passed in a list format. set(cmakeCommand "${CMAKE_COMMAND}") + + # Get the list of optional and platform-specific variables that may affect build process. + set(cmakeOptionalVariables "") + aws_get_variables_for_prebuild_dependency(cmakeOptionalVariables) + list(APPEND cmakeCommand ${cmakeOptionalVariables}) + + # The following variables should always be used. list(APPEND cmakeCommand ${AWS_PREBUILD_SOURCE_DIR}) list(APPEND cmakeCommand -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE}) list(APPEND cmakeCommand -DCMAKE_PREFIX_PATH=${ESCAPED_PREFIX_PATH}) list(APPEND cmakeCommand -DCMAKE_INSTALL_PREFIX=${depInstallDir}) list(APPEND cmakeCommand -DCMAKE_INSTALL_RPATH=${CMAKE_INSTALL_RPATH}) list(APPEND cmakeCommand -DBUILD_SHARED_LIBS=${BUILD_SHARED_LIBS}) + # In case a custom generator was provided via -G option. If we don't propagate it, the default value might + # conflict with other cmake options (e.g. CMAKE_MAKE_PROGRAM) or no make program could be found at all. + if (CMAKE_GENERATOR) + list(APPEND cmakeCommand -G${CMAKE_GENERATOR}) + endif() # Append provided arguments to CMake command. - if(AWS_PREBUILD_CMAKE_ARGUMENTS) + if (AWS_PREBUILD_CMAKE_ARGUMENTS) list(APPEND cmakeCommand ${AWS_PREBUILD_CMAKE_ARGUMENTS}) endif() + message(STATUS "cmake command for dependency ${AWS_PREBUILD_DEPENDENCY_NAME}: ${cmakeCommand}") # Configure dependency project. execute_process( COMMAND ${cmakeCommand} @@ -65,6 +78,10 @@ function(aws_prebuild_dependency) # Make the installation visible for others. list(INSERT CMAKE_PREFIX_PATH 0 ${depInstallDir}/) set(CMAKE_PREFIX_PATH ${CMAKE_PREFIX_PATH} PARENT_SCOPE) + if (CMAKE_CROSSCOMPILING) + list(INSERT CMAKE_FIND_ROOT_PATH 0 ${depInstallDir}) + set(CMAKE_FIND_ROOT_PATH ${CMAKE_FIND_ROOT_PATH} PARENT_SCOPE) + endif() set(${AWS_PREBUILD_DEPENDENCY_NAME}_PREBUILT TRUE CACHE INTERNAL "Indicate that dependency is built and can be used") @@ -75,3 +92,60 @@ function(aws_prebuild_dependency) DESTINATION ${CMAKE_INSTALL_PREFIX} ) endfunction() + +# Get list of optional or platform-specific variables that may affect build process. +function(aws_get_variables_for_prebuild_dependency AWS_CMAKE_PREBUILD_ARGS) + set(variables "") + + # The CMake variables below were chosen for Linux, BSD, and Android platforms. If you want to use the prebuild logic + # on other platforms, the chances are you have to handle additional variables (like CMAKE_OSX_SYSROOT). Refer to + # https://cmake.org/cmake/help/latest/manual/cmake-toolchains.7.html to update the list of handled variables, and + # then you can enable a new platform here. + if ((NOT UNIX) OR APPLE) + message(FATAL_ERROR "aws_get_variables_for_prebuild_dependency is called for unsupported platform") + endif() + + get_cmake_property(vars CACHE_VARIABLES) + foreach(var ${vars}) + # Variables in this block make sense only in cross-compiling mode. The variable list is created from the CMake + # documentation on toolchains: https://cmake.org/cmake/help/latest/manual/cmake-toolchains.7.html + # NOTE: Some variables are missed here (e.g. CMAKE_SYSROOT) because they can be set via toolchain file only. + if (CMAKE_CROSSCOMPILING AND ( + var STREQUAL "CMAKE_TOOLCHAIN_FILE" + OR var STREQUAL "CMAKE_SYSTEM_NAME" + OR var STREQUAL "CMAKE_SYSTEM_VERSION" + OR var STREQUAL "CMAKE_SYSTEM_PROCESSOR" + # Android-specific variables. + OR var MATCHES "^(CMAKE_)?ANDROID_")) + # To store a list within another list, it needs to be escaped first. + string(REPLACE ";" "\\\\;" escapedVar "${${var}}") + if (escapedVar) + list(APPEND variables "-D${var}=${escapedVar}") + endif() + endif() + + # Other optional variables applicable both in cross-compiling and non-cross-compiling modes. + # Refer to https://cmake.org/cmake/help/latest/manual/cmake-variables.7.html for each variable description. + if (var STREQUAL "CMAKE_C_COMPILER" + OR var MATCHES "^CMAKE_C_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?" + OR var STREQUAL "CMAKE_CXX_COMPILER" + OR var MATCHES "^CMAKE_CXX_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?" + OR var STREQUAL "CMAKE_LINKER_TYPE" + OR var MATCHES "^CMAKE_EXE_LINKER_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?" + OR var MATCHES "^CMAKE_MODULE_LINKER_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?" + OR var MATCHES "^CMAKE_STATIC_LINKER_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?" + OR var MATCHES "^CMAKE_SHARED_LINKER_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?" + OR var STREQUAL "CMAKE_MAKE_PROGRAM" + OR var MATCHES "^CMAKE_RUNTIME_OUTPUT_DIRECTORY" + OR var MATCHES "^CMAKE_ARCHIVE_OUTPUT_DIRECTORY" + OR var MATCHES "^CMAKE_LIBRARY_OUTPUT_DIRECTORY") + # To store a list within another list, it needs to be escaped first. + string(REPLACE ";" "\\\\;" escapedVar "${${var}}") + if (escapedVar) + list(APPEND variables "-D${var}=${escapedVar}") + endif() + endif() + endforeach() + + set(${AWS_CMAKE_PREBUILD_ARGS} ${variables} PARENT_SCOPE) +endfunction() From da9e1c3db9f93e0ba7ff1b30bc5c6672c1de9208 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 26 Nov 2024 21:00:23 +0100 Subject: [PATCH 2/2] Update CBMC proof tooling to latest releases (#1164) Co-authored-by: Michael Graeb --- .github/workflows/proof_ci_resources/config.yaml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/proof_ci_resources/config.yaml b/.github/workflows/proof_ci_resources/config.yaml index fb955a76f..0b4c4c723 100644 --- a/.github/workflows/proof_ci_resources/config.yaml +++ b/.github/workflows/proof_ci_resources/config.yaml @@ -1,8 +1,8 @@ # Use exact versions (instead of "latest") so we're not broken by surprise upgrades. -cadical-tag: "rel-2.0.0" # tag of latest release: https://github.com/arminbiere/cadical/releases -cbmc-version: "6.2.0" # semver of latest release: https://github.com/diffblue/cbmc/releases -cbmc-viewer-version: "3.9" # semver of latest release: https://github.com/model-checking/cbmc-viewer/releases -kissat-tag: "rel-4.0.0" # tag of latest release: https://github.com/arminbiere/kissat/releases +cadical-tag: "rel-2.1.0" # tag of latest release: https://github.com/arminbiere/cadical/releases +cbmc-version: "6.4.0" # semver of latest release: https://github.com/diffblue/cbmc/releases +cbmc-viewer-version: "3.10" # semver of latest release: https://github.com/model-checking/cbmc-viewer/releases +kissat-tag: "rel-4.0.1" # tag of latest release: https://github.com/arminbiere/kissat/releases litani-version: "1.29.0" # semver of latest release: https://github.com/awslabs/aws-build-accumulator/releases proofs-dir: verification/cbmc/proofs run-cbmc-proofs-command: ./run-cbmc-proofs.py