Allow including multiple backend solvers in cmake builds

Author: zhassan-aws

Diff for: CMakeLists.txt

@@ -273,7 +273,8 @@ else()
     FetchContent_MakeAvailable(Corrosion)
 
     corrosion_import_crate(MANIFEST_PATH src/libcprover-rust/Cargo.toml)
-    corrosion_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR} SAT_IMPL=${sat_impl})
+    list(JOIN sat_impl " " sat_impl_str)
+    corrosion_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR} "SAT_IMPL=${sat_impl_str}")
     corrosion_link_libraries(cprover-api-rust cprover-api-cpp)
     install(TARGETS cprover-api-rust RUNTIME DESTINATION lib)
     # NOTE: We want to rename to a name consistent with the name of the

Diff for: src/libcprover-rust/build.rs

@@ -40,20 +40,26 @@ fn get_cadical_build_dir() -> std::io::Result<PathBuf> {
     ))
 }
 
-fn get_sat_library() -> std::io::Result<&'static str> {
+fn get_sat_libraries() -> std::io::Result<Vec<&'static str>> {
     let env_var_name = "SAT_IMPL";
     let env_var_fetch_result = env::var(env_var_name);
-    if let Ok(sat_impl) = env_var_fetch_result {
-        let solver_lib = match sat_impl.as_str() {
-            "minisat2" => Ok("minisat2-condensed"),
-            "glucose" => Ok("glucose-condensed"),
-            "cadical" => Ok("cadical"),
-            _ => Err(Error::new(
-                ErrorKind::Other,
-                "no identifiable solver detected",
-            )),
-        };
-        return solver_lib;
+    if let Ok(sat_impls) = env_var_fetch_result {
+        let mut solver_libs = Vec::new();
+        for sat_impl in sat_impls.split(" ") {
+            let solver_lib = match sat_impl {
+                "minisat2" => "minisat2-condensed",
+                "glucose" => "glucose-condensed",
+                "cadical" => "cadical",
+                _ => {
+                    return Err(Error::new(
+                        ErrorKind::Other,
+                        "no identifiable solver detected",
+                    ))
+                }
+            };
+            solver_libs.push(solver_lib);
+        }
+        return Ok(solver_libs);
     }
     Err(Error::new(
         ErrorKind::Other,
@@ -80,23 +86,25 @@ fn main() {
         Err(err) => panic!("Error: {}", err),
     };
 
-    let solver_lib = match get_sat_library() {
-        Ok(solver) => solver,
+    let solver_libs = match get_sat_libraries() {
+        Ok(solvers) => solvers,
         Err(err) => panic!("Error: {}", err),
     };
 
-    // Cadical is being built in its own directory, with the resultant artefacts being
-    // present only there. Hence, we need to instruct cargo to look for them in cadical's
-    // build directory, otherwise we're going to get build errors.
-    if solver_lib == "cadical" {
-        let cadical_build_dir = match get_cadical_build_dir() {
-            Ok(cadical_directory) => cadical_directory,
-            Err(err) => panic!("Error: {}", err),
-        };
-        println!(
-            "cargo:rustc-link-search=native={}",
-            cadical_build_dir.display()
-        );
+    for solver_lib in solver_libs.iter() {
+        // Cadical is being built in its own directory, with the resultant artefacts being
+        // present only there. Hence, we need to instruct cargo to look for them in cadical's
+        // build directory, otherwise we're going to get build errors.
+        if *solver_lib == "cadical" {
+            let cadical_build_dir = match get_cadical_build_dir() {
+                Ok(cadical_directory) => cadical_directory,
+                Err(err) => panic!("Error: {}", err),
+            };
+            println!(
+                "cargo:rustc-link-search=native={}",
+                cadical_build_dir.display()
+            );
+        }
     }
 
     println!(
@@ -122,7 +130,9 @@ fn main() {
     println!("cargo:rustc-link-lib=static=statement-list");
     println!("cargo:rustc-link-lib=static=goto-symex");
     println!("cargo:rustc-link-lib=static=pointer-analysis");
-    println!("cargo:rustc-link-lib=static={}", solver_lib);
+    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");
 }

Diff for: src/solvers/CMakeLists.txt

@@ -64,137 +64,132 @@ add_library(solvers ${sources})
 
 include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
 
-if("${sat_impl}" STREQUAL "minisat2")
-    message(STATUS "Building solvers with minisat2")
-
-    # once we upgrade to CMake 3.7 or higher we can specify multiple URLs as a
-    # fall-back in case the first URL fails (the Makefile-based build retries up
-    # to 2 times)
-    download_project(PROJ minisat2
-        URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
-        PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
-        COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt
-        URL_MD5 27faa19ee0508660bd6fb7f894646d42
-    )
+foreach(SOLVER ${sat_impl})
+    if("${SOLVER}" STREQUAL "minisat2")
+        message(STATUS "Building solvers with minisat2")
+
+        # once we upgrade to CMake 3.7 or higher we can specify multiple URLs as a
+        # fall-back in case the first URL fails (the Makefile-based build retries up
+        # to 2 times)
+        download_project(PROJ minisat2
+            URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
+            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt
+            URL_MD5 27faa19ee0508660bd6fb7f894646d42
+        )
 
-    add_subdirectory(${minisat2_SOURCE_DIR} ${minisat2_BINARY_DIR})
+        add_subdirectory(${minisat2_SOURCE_DIR} ${minisat2_BINARY_DIR})
 
-    target_compile_definitions(solvers PUBLIC
-        SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
-    )
-
-    target_sources(solvers PRIVATE ${minisat2_source})
+        target_compile_definitions(solvers PUBLIC
+            SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
+        )
 
-    target_link_libraries(solvers minisat2-condensed)
-elseif("${sat_impl}" STREQUAL "glucose")
-    message(STATUS "Building solvers with glucose")
+        target_sources(solvers PRIVATE ${minisat2_source})
 
-    download_project(PROJ glucose
-        URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz
-        PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch
-        COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
-        URL_MD5 7c539c62c248b74210aef7414787323a
-    )
+        target_link_libraries(solvers minisat2-condensed)
+    elseif("${SOLVER}" STREQUAL "glucose")
+        message(STATUS "Building solvers with glucose")
 
-    add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR})
+        download_project(PROJ glucose
+            URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch
+            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
+            URL_MD5 7c539c62c248b74210aef7414787323a
+        )
 
-    target_compile_definitions(solvers PUBLIC
-        SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
-    )
+        add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR})
 
-    target_sources(solvers PRIVATE ${glucose_source})
+        target_compile_definitions(solvers PUBLIC
+            SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
+        )
 
-    target_link_libraries(solvers glucose-condensed)
-elseif("${sat_impl}" STREQUAL "cadical")
-    message(STATUS "Building solvers with cadical")
+        target_sources(solvers PRIVATE ${glucose_source})
 
-    download_project(PROJ cadical
-        URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz
-        PATCH_COMMAND true
-        COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14
-        URL_MD5 b44874501a175106424f4bd5de29aa59
-    )
+        target_link_libraries(solvers glucose-condensed)
+    elseif("${SOLVER}" STREQUAL "cadical")
+        message(STATUS "Building solvers with cadical")
 
-    message(STATUS "Building CaDiCaL")
-    execute_process(COMMAND make -j WORKING_DIRECTORY ${cadical_SOURCE_DIR})
+        download_project(PROJ cadical
+            URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.4.1-patch
+            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt
+            COMMAND ./configure
+            URL_MD5 b44874501a175106424f4bd5de29aa59
+        )
 
-    target_compile_definitions(solvers PUBLIC
-        SATCHECK_CADICAL HAVE_CADICAL
-    )
+        add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR})
 
-    add_library(cadical STATIC IMPORTED)
+        target_compile_definitions(solvers PUBLIC
+            SATCHECK_CADICAL HAVE_CADICAL
+        )
 
-    set_target_properties(
-        cadical
-        PROPERTIES IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a
-    )
+        target_include_directories(solvers
+            PUBLIC
+            ${cadical_SOURCE_DIR}/src
+        )
 
-    target_include_directories(solvers
-      PUBLIC
-      ${cadical_SOURCE_DIR}/src
-    )
+        target_link_libraries(solvers cadical)
+    elseif("${SOLVER}" STREQUAL "ipasir-cadical")
+        message(STATUS "Building with IPASIR solver linking against: CaDiCaL")
 
-    target_link_libraries(solvers cadical)
-elseif("${sat_impl}" STREQUAL "ipasir-cadical")
-    message(STATUS "Building with IPASIR solver linking against: CaDiCaL")
+        download_project(PROJ cadical
+            URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz
+            PATCH_COMMAND true
+            COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14
+            URL_MD5 b44874501a175106424f4bd5de29aa59
+        )
 
-    download_project(PROJ cadical
-        URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz
-        PATCH_COMMAND true
-        COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14
-        URL_MD5 b44874501a175106424f4bd5de29aa59
-    )
+        message(STATUS "Building CaDiCaL")
+        execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR})
 
-    message(STATUS "Building CaDiCaL")
-    execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR})
+        target_compile_definitions(solvers PUBLIC
+            SATCHECK_IPASIR HAVE_IPASIR IPASIR=${cadical_SOURCE_DIR}/src
+        )
 
-    target_compile_definitions(solvers PUBLIC
-        SATCHECK_IPASIR HAVE_IPASIR IPASIR=${cadical_SOURCE_DIR}/src
-    )
+        add_library(cadical_ipasir STATIC IMPORTED)
+        set_property(TARGET cadical_ipasir
+            PROPERTY IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a
+        )
 
-    add_library(cadical_ipasir STATIC IMPORTED)
-    set_property(TARGET cadical_ipasir
-        PROPERTY IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a
-    )
+        target_include_directories(solvers
+            PUBLIC
+            ${cadical_SOURCE_DIR}/src
+        )
+        target_link_libraries(solvers cadical_ipasir)
+    elseif("${SOLVER}" STREQUAL "ipasir-custom")
+        message(STATUS "Building with IPASIR solver linking: custom solver provided")
+
+        if (NOT DEFINED IPASIR)
+            message(FATAL_ERROR
+              "IPASIR solver source code not provided. Please use -DIPASIR=<location> "
+              "with <location> being the path to the IPASIR solver source code."
+            )
+        endif()
+
+        if (NOT DEFINED IPASIR_LIB)
+            message(FATAL_ERROR
+                "IPASIR solver library not provided. Please use -DIPASIR_LIB=<location> "
+                "with <location> being the path to the IPASIR solver precompiled static "
+                "library."
+            )
+        endif()
+
+        target_compile_definitions(solvers PUBLIC
+            SATCHECK_IPASIR HAVE_IPASIR IPASIR=${IPASIR}
+        )
 
-    target_include_directories(solvers
-        PUBLIC
-        ${cadical_SOURCE_DIR}/src
-    )
-    target_link_libraries(solvers cadical_ipasir)
-elseif("${sat_impl}" STREQUAL "ipasir-custom")
-    message(STATUS "Building with IPASIR solver linking: custom solver provided")
-
-    if (NOT DEFINED IPASIR)
-        message(FATAL_ERROR
-          "IPASIR solver source code not provided. Please use -DIPASIR=<location> "
-          "with <location> being the path to the IPASIR solver source code."
+        add_library(ipasir_custom STATIC IMPORTED)
+        set_property(TARGET ipasir_custom
+            PROPERTY IMPORTED_LOCATION ${IPASIR_LIB}
         )
-    endif()
 
-    if (NOT DEFINED IPASIR_LIB)
-        message(FATAL_ERROR
-            "IPASIR solver library not provided. Please use -DIPASIR_LIB=<location> "
-            "with <location> being the path to the IPASIR solver precompiled static "
-            "library."
+        target_include_directories(solvers
+            PUBLIC
+            ${IPASIR}
         )
+        target_link_libraries(solvers ipasir_custom pthread)
     endif()
-
-    target_compile_definitions(solvers PUBLIC
-        SATCHECK_IPASIR HAVE_IPASIR IPASIR=${IPASIR}
-    )
-
-    add_library(ipasir_custom STATIC IMPORTED)
-    set_property(TARGET ipasir_custom
-        PROPERTY IMPORTED_LOCATION ${IPASIR_LIB}
-    )
-
-    target_include_directories(solvers
-        PUBLIC
-        ${IPASIR}
-    )
-    target_link_libraries(solvers ipasir_custom pthread)
-endif()
+endforeach()
 
 if(CMAKE_USE_CUDD)
     target_link_libraries(solvers util cudd-cplusplus cudd)