-
Notifications
You must be signed in to change notification settings - Fork 32
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Enable using option -DCRAB_USE_PPLITE_NATIVE=ON fix(test): HAVE_PPLITE does not imply HAVE_APRON Before having a native interface for pplite, the pragma HAVE_PPLITE implied HAVE_APRON because pplite was necessarily using the apron interface. However after, that implication does not necessarily holds. However the decoupled domain (specifically convert_to) expects both HAVE_APRON and HAVE_PPLITE enabled if template parameter is instantiated with apron_asc_dsc_pair.
- Loading branch information
Showing
13 changed files
with
971 additions
and
20 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,11 @@ | ||
| if (CRAB_USE_PPLITE_NATIVE) | ||
| set (PPLITE_DOMAINS_REPO "https://github.com/seahorn/crab-pplite.git" | ||
| CACHE STRING "source of wrapper for pplite domains using native interface") | ||
| set (PPLITE_SOURCE_DIR "${CMAKE_SOURCE_DIR}/include/crab/domains/pplite") | ||
| set (PPLITE_WRAPPER "${PPLITE_SOURCE_DIR}/pplite_native_wrapper.hpp") | ||
|
|
||
| if (NOT EXISTS ${PPLITE_WRAPPER}) | ||
| add_custom_target(pplite-native | ||
| ${GIT_EXECUTABLE} clone ${PPLITE_DOMAINS_REPO} ${PPLITE_SOURCE_DIR}) | ||
| endif() | ||
| endif() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,32 @@ | ||
| # | ||
| # Dockerfile for Crab image with pplite library using native interface. | ||
| # | ||
|
|
||
| # Pull base image. | ||
| FROM seahorn/buildpack-deps-crab:jammy | ||
|
|
||
| # Assume that docker-build is ran in the top-level Crab directory | ||
| COPY . /crab | ||
| # Re-create the build directory that might have been present in the source tree | ||
| RUN rm -rf /crab/build /crab/debug /crab/release && mkdir /crab/build | ||
| WORKDIR /crab/build | ||
|
|
||
| ARG BUILD_TYPE | ||
| # Build configuration. | ||
| RUN cmake -GNinja \ | ||
| -DCMAKE_BUILD_TYPE=$BUILD_TYPE \ | ||
| -DCMAKE_INSTALL_PREFIX=run \ | ||
| -DCMAKE_CXX_COMPILER=g++-12 \ | ||
| -DCMAKE_EXPORT_COMPILE_COMMANDS=1 \ | ||
| -DCRAB_USE_PPLITE_NATIVE=ON \ | ||
| -DCRAB_ENABLE_TESTS=ON \ | ||
| ../ && \ | ||
| cmake --build . --target pplite && cmake .. && \ | ||
| cmake --build . --target pplite-native && cmake .. && \ | ||
| cmake --build . --target install | ||
|
|
||
| # Run tests | ||
| RUN /crab/tests/run_tests.sh /crab/tests/expected_results.pplite_native.out /crab/build | ||
|
|
||
| WORKDIR /crab | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,96 @@ | ||
| #pragma once | ||
|
|
||
| #include <crab/config.h> | ||
|
|
||
| #include <crab/domains/abstract_domain.hpp> | ||
| #include <crab/domains/abstract_domain_specialized_traits.hpp> | ||
| #include <crab/numbers/bignums.hpp> | ||
|
|
||
| namespace crab { | ||
| namespace domains { | ||
|
|
||
| namespace pplite_domains { | ||
| /* | ||
| The values of this enumeration need to be kept in sync with | ||
| enum pplite::dynamic::Abs_Poly::Kind | ||
| */ | ||
| //enum pplite_domain_id_t : unsigned int; | ||
|
|
||
| /* | ||
| This enumeration needs to be kept in sync with | ||
| enum pplite::dynamic::Abs_Poly::Kind | ||
| The listed enum values are up-to-date with PPLite 0.11. | ||
| Note: even values are for domains; odd values for _STATS variants. | ||
| */ | ||
| enum pplite_domain_id_t : unsigned int { | ||
| POLY, POLY_STATS, | ||
| B_POLY, B_POLY_STATS, | ||
| F_POLY, F_POLY_STATS, | ||
| U_POLY, U_POLY_STATS, | ||
| UF_POLY, UF_POLY_STATS, | ||
| P_SET, P_SET_STATS, | ||
| FP_SET, FP_SET_STATS | ||
| }; | ||
| } // pplite_domains | ||
|
|
||
| template <typename Number> class PPLiteDefaultParams { | ||
| public: | ||
| // use integers with truncation rounding | ||
| enum { use_integers = 1 }; | ||
| enum { implement_inter_transformers = 0 }; | ||
| }; | ||
|
|
||
| template <> class PPLiteDefaultParams<ikos::q_number> { | ||
| public: | ||
| // use reals | ||
| enum { use_integers = 0 }; | ||
| enum { implement_inter_transformers = 0 }; | ||
| }; | ||
|
|
||
| } // namespace domains | ||
| } // namespace crab | ||
|
|
||
| #if not defined(HAVE_PPLITE) || not defined(HAVE_PPLITE_NATIVE) | ||
|
|
||
| /* | ||
| * Dummy implementation if PPLite not found | ||
| */ | ||
|
|
||
| #include <crab/domains/dummy_abstract_domain.hpp> | ||
|
|
||
| namespace crab { | ||
| namespace domains { | ||
|
|
||
| template <typename N, typename V, pplite_domains::pplite_domain_id_t K, | ||
| class P = PPLiteDefaultParams<N>> | ||
| class pplite_domain final | ||
| : public dummy_abstract_domain<pplite_domain<N,V,K,P>> { | ||
| public: | ||
| std::string not_implemented_msg() const override { | ||
| #ifndef HAVE_PPLITE | ||
| return "No PPLite. Run cmake with -DCRAB_USE_PPLITE=ON"; | ||
| #else | ||
| return "No PPLite. Make sure that pplite_domains can be found"; | ||
| #endif | ||
| } | ||
| }; | ||
|
|
||
| } // namespace domains | ||
| } // namespace crab | ||
|
|
||
| #else // defined(HAVE_PPLITE) | ||
|
|
||
| #include <crab/domains/pplite/pplite_native_wrapper.hpp> | ||
|
|
||
| #endif // HAVE_PPLITE | ||
|
|
||
| namespace crab { | ||
| namespace domains { | ||
| template <typename Number, typename VariableName, pplite_domains::pplite_domain_id_t K, | ||
| class Params> | ||
| struct abstract_domain_traits<pplite_domain<Number, VariableName, K, Params>> { | ||
| using number_t = Number; | ||
| using varname_t = VariableName; | ||
| }; | ||
| } // namespace domains | ||
| } // namespace crab |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.