From b469c2674313bc475d9b1073a3c56377a8778135 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Mon, 27 Feb 2023 18:33:22 +0000 Subject: [PATCH 1/5] Added version from config.inc to cmake project --- src/CMakeLists.txt | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b2bb12e8a49..8c51257d0a1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,4 +1,12 @@ -project(CBMC) +file(STRINGS + "${CMAKE_CURRENT_SOURCE_DIR}/config.inc" + cbmc_version_string + REGEX "CBMC_VERSION.*") + +string(REGEX REPLACE "CBMC_VERSION = (.*)" "\\1" CBMC_VERSION "${cbmc_version_string}") +unset(cbmc_version_string) + +project(CBMC VERSION ${CBMC_VERSION}) find_package(BISON REQUIRED) find_package(FLEX REQUIRED) From 2cee3b182fd2da9749019a3d2a4f1be1be13ea5d Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Mon, 27 Feb 2023 18:34:31 +0000 Subject: [PATCH 2/5] Aggregating all library dependencies into one CBMC is compiled as a collection of static libraries, one per sub-module. This commits add a merging of most submodules into a final libcprover..a, so that it can be installed and used alone (without requiring its sub-module dependencies). --- src/CMakeLists.txt | 2 +- src/libcprover-cpp/CMakeLists.txt | 87 ++++++++++++++++++++------ src/libcprover-cpp/add_dependencies.sh | 15 +++++ 3 files changed, 83 insertions(+), 21 deletions(-) create mode 100755 src/libcprover-cpp/add_dependencies.sh diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8c51257d0a1..c81f5a36db7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -110,7 +110,6 @@ add_subdirectory(jsil) add_subdirectory(json) add_subdirectory(json-symtab-language) add_subdirectory(langapi) -add_subdirectory(libcprover-cpp) add_subdirectory(linking) add_subdirectory(pointer-analysis) add_subdirectory(solvers) @@ -127,6 +126,7 @@ add_subdirectory(goto-diff) add_subdirectory(goto-harness) add_subdirectory(goto-synthesizer) add_subdirectory(symtab2gb) +add_subdirectory(libcprover-cpp) if(UNIX OR WITH_MEMORY_ANALYZER) add_subdirectory(memory-analyzer) diff --git a/src/libcprover-cpp/CMakeLists.txt b/src/libcprover-cpp/CMakeLists.txt index ad5f10d233b..48eb3e18d74 100644 --- a/src/libcprover-cpp/CMakeLists.txt +++ b/src/libcprover-cpp/CMakeLists.txt @@ -1,23 +1,70 @@ -file(GLOB_RECURSE sources "*.cpp" "*.h") +file(GLOB_RECURSE sources "*.cpp") +file(GLOB_RECURSE headers "*.h") -# This step builds the API in the form of a statically linked library (libcprover-api-cpp.a) +# This step builds the API in the form of a statically linked library add_library(cprover-api-cpp ${sources}) + +# Being a library we should include them privately, but for now fair enough generic_includes(cprover-api-cpp) -target_link_libraries(cprover-api-cpp - goto-checker - goto-programs - util - langapi - ansi-c - json-symtab-language - solvers - xml - cpp - cbmc-lib - analyses - statement-list - linking - pointer-analysis - goto-instrument-lib - goto-analyzer-lib - goto-cc-lib) + +target_include_directories(cprover-api-cpp PUBLIC + "$" + "$" + "$") + +get_target_property(LIBRARY_DEPENDENCIES solvers LINK_LIBRARIES) + +list(APPEND + LIBRARY_DEPENDENCIES + "goto-programs" + "util" + "langapi" + "ansi-c" + "analyses" + "goto-instrument-lib" + "big-int" + "linking" + "goto-checker" + "solvers" + "assembler" + "xml" + "json" + "json-symtab-language" + "jsil" + "statement-list" + "goto-symex" + "pointer-analysis" + "cbmc-lib") + +list(REMOVE_DUPLICATES LIBRARY_DEPENDENCIES) + +target_link_libraries(cprover-api-cpp + PRIVATE + ${LIBRARY_DEPENDENCIES}) + +set(DEPENDENCY_TARGETS "") +foreach(dep ${LIBRARY_DEPENDENCIES}) + list(APPEND DEPENDENCY_TARGETS "$") +endforeach(dep LIBRARY_DEPENDENCIES) + +string(REPLACE ";" " " DEPENDENCY_TARGETS "${DEPENDENCY_TARGETS}") + +add_custom_command(TARGET cprover-api-cpp POST_BUILD + COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/add_dependencies.sh" "${CMAKE_AR}" "$" "${DEPENDENCY_TARGETS}" + WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}") + +set_target_properties(cprover-api-cpp + PROPERTIES + OUTPUT_NAME "cprover.${CMAKE_PROJECT_VERSION}" # libcprover..a + SOVERSION "${CMAKE_PROJECT_VERSION}" + PUBLIC_HEADER "${headers}" + ) + +install(TARGETS cprover-api-cpp + ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" + COMPONENT lib + LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}" + COMPONENT lib + PUBLIC_HEADER DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/cprover" + COMPONENT lib + ) diff --git a/src/libcprover-cpp/add_dependencies.sh b/src/libcprover-cpp/add_dependencies.sh new file mode 100755 index 00000000000..7088296fcfc --- /dev/null +++ b/src/libcprover-cpp/add_dependencies.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env sh + +set -e + +AR_COMMAND=$1 +shift +DESTINATION=$1 +shift +LIB_LIST=$@ + +for lib in ${LIB_LIST}; do + ${AR_COMMAND} -x ${lib} +done + +${AR_COMMAND} -rcs ${DESTINATION} *.o From 2a48ee5e7e430e66feea7217114e412ec84d1a9f Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 28 Feb 2023 13:12:56 +0000 Subject: [PATCH 3/5] Renamed api files to avoid object-file clashes --- regression/libcprover-cpp/call_bmc.cpp | 2 +- src/libcprover-cpp/api.h | 2 +- src/libcprover-cpp/{options.cpp => api_options.cpp} | 2 +- src/libcprover-cpp/{options.h => api_options.h} | 0 4 files changed, 3 insertions(+), 3 deletions(-) rename src/libcprover-cpp/{options.cpp => api_options.cpp} (98%) rename src/libcprover-cpp/{options.h => api_options.h} (100%) diff --git a/regression/libcprover-cpp/call_bmc.cpp b/regression/libcprover-cpp/call_bmc.cpp index 44543c0e324..3ac2dc7bf31 100644 --- a/regression/libcprover-cpp/call_bmc.cpp +++ b/regression/libcprover-cpp/call_bmc.cpp @@ -4,7 +4,7 @@ #include #include -#include +#include #include "goto_model.h" diff --git a/src/libcprover-cpp/api.h b/src/libcprover-cpp/api.h index ee82c84e6be..65d8fe61749 100644 --- a/src/libcprover-cpp/api.h +++ b/src/libcprover-cpp/api.h @@ -17,7 +17,7 @@ struct api_session_implementationt; // a pragma like below to silence the warning (at least as long // as the design principle is to be followed.) -#include "options.h" // IWYU pragma: keep +#include "api_options.h" // IWYU pragma: keep /// Opaque message type. Properties of messages to be fetched through further /// api calls. diff --git a/src/libcprover-cpp/options.cpp b/src/libcprover-cpp/api_options.cpp similarity index 98% rename from src/libcprover-cpp/options.cpp rename to src/libcprover-cpp/api_options.cpp index 85546049cf9..d11e01785ac 100644 --- a/src/libcprover-cpp/options.cpp +++ b/src/libcprover-cpp/api_options.cpp @@ -1,6 +1,6 @@ // Author: Fotis Koutoulakis for Diffblue Ltd. -#include "options.h" +#include "api_options.h" #include #include diff --git a/src/libcprover-cpp/options.h b/src/libcprover-cpp/api_options.h similarity index 100% rename from src/libcprover-cpp/options.h rename to src/libcprover-cpp/api_options.h From 3999157a238016f0ab6f54dd2c8f68eb3d796733 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 28 Feb 2023 13:15:49 +0000 Subject: [PATCH 4/5] Removed unecessary dependencies from Rust API --- src/libcprover-rust/build.rs | 26 ++------------------------ 1 file changed, 2 insertions(+), 24 deletions(-) diff --git a/src/libcprover-rust/build.rs b/src/libcprover-rust/build.rs index 028e5b52d40..29874ab61dc 100644 --- a/src/libcprover-rust/build.rs +++ b/src/libcprover-rust/build.rs @@ -111,28 +111,6 @@ fn main() { "cargo:rustc-link-search=native={}", libraries_path.display() ); - println!("cargo:rustc-link-lib=static=goto-programs"); - println!("cargo:rustc-link-lib=static=util"); - println!("cargo:rustc-link-lib=static=langapi"); - println!("cargo:rustc-link-lib=static=ansi-c"); - println!("cargo:rustc-link-lib=static=analyses"); - println!("cargo:rustc-link-lib=static=goto-instrument-lib"); - println!("cargo:rustc-link-lib=static=big-int"); - println!("cargo:rustc-link-lib=static=linking"); - println!("cargo:rustc-link-lib=static=goto-checker"); - println!("cargo:rustc-link-lib=static=solvers"); - println!("cargo:rustc-link-lib=static=assembler"); - println!("cargo:rustc-link-lib=static=xml"); - println!("cargo:rustc-link-lib=static=json"); - println!("cargo:rustc-link-lib=static=json-symtab-language"); - println!("cargo:rustc-link-lib=static=cpp"); - println!("cargo:rustc-link-lib=static=jsil"); - println!("cargo:rustc-link-lib=static=statement-list"); - println!("cargo:rustc-link-lib=static=goto-symex"); - println!("cargo:rustc-link-lib=static=pointer-analysis"); - for solver_lib in solver_libs { - println!("cargo:rustc-link-lib=static={}", solver_lib); - } - println!("cargo:rustc-link-lib=static=cbmc-lib"); - println!("cargo:rustc-link-lib=static=cprover-api-cpp"); + + println!("cargo:rustc-link-lib=static=cprover.5.77.0"); } From cf4817f565d0c172237cf710e590437d3c16a617 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 28 Feb 2023 18:21:16 +0000 Subject: [PATCH 5/5] Added comments to API library CMakeLists.txt --- src/libcprover-cpp/CMakeLists.txt | 24 +++++++++++++++++++++++- src/libcprover-cpp/add_dependencies.sh | 10 ++++++++++ 2 files changed, 33 insertions(+), 1 deletion(-) diff --git a/src/libcprover-cpp/CMakeLists.txt b/src/libcprover-cpp/CMakeLists.txt index 48eb3e18d74..278e77f642d 100644 --- a/src/libcprover-cpp/CMakeLists.txt +++ b/src/libcprover-cpp/CMakeLists.txt @@ -1,4 +1,6 @@ +# Scan for all source files in the current or child directories file(GLOB_RECURSE sources "*.cpp") +# Scan for all header files in the current or child directories (necessary to install them later) file(GLOB_RECURSE headers "*.h") # This step builds the API in the form of a statically linked library @@ -7,13 +9,22 @@ add_library(cprover-api-cpp ${sources}) # Being a library we should include them privately, but for now fair enough generic_includes(cprover-api-cpp) +# Add all the current and the installed `include` directories as a PUBLIC header location target_include_directories(cprover-api-cpp PUBLIC "$" "$" "$") +# To create a full static API library we need to archive together the content of all the other +# module libraries we depend on. To do this we will use the `ar` command to unpack the other module +# static libraries and append to the current library `.a` file. + +# Get the dependency targets of the `solver` target (see `../solver/CMakeLists.txt`), so that they +# are merged to the final library too. (such dependencies are not known statically as the selection +# of the SAT backend is left to the building user. get_target_property(LIBRARY_DEPENDENCIES solvers LINK_LIBRARIES) +# Get all the dependency targets we know statically. list(APPEND LIBRARY_DEPENDENCIES "goto-programs" @@ -36,23 +47,33 @@ list(APPEND "pointer-analysis" "cbmc-lib") +# Remove possible duplicate library targets list(REMOVE_DUPLICATES LIBRARY_DEPENDENCIES) +# Add all the dependency targets as dependencies of `cprover-api-cpp` target_link_libraries(cprover-api-cpp PRIVATE ${LIBRARY_DEPENDENCIES}) +# To be able to invoke `ar` on the dependencies we need the paths of the libraries `.a` files. +# Ths is done by using the cmake generator `$`, that in turn will be +# substituted with the absolute path of the `dependency` output file (a `.a` file in this case). +# Here we prepare a space-separated list of cmake generators that will resolved in absolute paths. set(DEPENDENCY_TARGETS "") foreach(dep ${LIBRARY_DEPENDENCIES}) list(APPEND DEPENDENCY_TARGETS "$") endforeach(dep LIBRARY_DEPENDENCIES) - string(REPLACE ";" " " DEPENDENCY_TARGETS "${DEPENDENCY_TARGETS}") +# To aggregate all the dependencies into a final `.a` file we add a custom pass after target +# `cprover-api-cpp` has been built where the `aggregate_dependencies.sh` script is run with the `ar` +# command, the destination library and the dependencies paths add_custom_command(TARGET cprover-api-cpp POST_BUILD COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/add_dependencies.sh" "${CMAKE_AR}" "$" "${DEPENDENCY_TARGETS}" WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}") +# Set the properties of `cprover-api-cpp`. Mainly the output name `libcprover..a`, its +# version (CBMC version) and the list of public headers to be installed set_target_properties(cprover-api-cpp PROPERTIES OUTPUT_NAME "cprover.${CMAKE_PROJECT_VERSION}" # libcprover..a @@ -60,6 +81,7 @@ set_target_properties(cprover-api-cpp PUBLIC_HEADER "${headers}" ) +# Install the target as usual in `lib` the library and in `include/cprover` the public headers. install(TARGETS cprover-api-cpp ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" COMPONENT lib diff --git a/src/libcprover-cpp/add_dependencies.sh b/src/libcprover-cpp/add_dependencies.sh index 7088296fcfc..4b6f4f16043 100755 --- a/src/libcprover-cpp/add_dependencies.sh +++ b/src/libcprover-cpp/add_dependencies.sh @@ -1,5 +1,12 @@ #!/usr/bin/env sh +# This script adds to a static library archive file `lib.a` all the object files of a set of +# other libraries it depends on. +# This script takes 3 or more arguments: +# 1. the archive command +# 2. the destination library path +# 3. a list of paths of static libraries to be added to the destination library archive + set -e AR_COMMAND=$1 @@ -8,8 +15,11 @@ DESTINATION=$1 shift LIB_LIST=$@ +# For each library to add: for lib in ${LIB_LIST}; do + # Unpack the library ${AR_COMMAND} -x ${lib} done +# Append all the unpacked files to the destination library ${AR_COMMAND} -rcs ${DESTINATION} *.o