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/CMakeLists.txt b/src/CMakeLists.txt index b2bb12e8a49..c81f5a36db7 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) @@ -102,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) @@ -119,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..278e77f642d 100644 --- a/src/libcprover-cpp/CMakeLists.txt +++ b/src/libcprover-cpp/CMakeLists.txt @@ -1,23 +1,92 @@ -file(GLOB_RECURSE sources "*.cpp" "*.h") +# 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 (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) + +# 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" + "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") + +# 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 + SOVERSION "${CMAKE_PROJECT_VERSION}" + 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 + 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..4b6f4f16043 --- /dev/null +++ b/src/libcprover-cpp/add_dependencies.sh @@ -0,0 +1,25 @@ +#!/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 +shift +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 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 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"); }