diff options
| -rw-r--r-- | README.md | 5 | ||||
| -rw-r--r-- | REUSE.toml | 4 | ||||
| -rw-r--r-- | loftix/deduction.scm | 87 | ||||
| -rw-r--r-- | loftix/fuzzing.scm | 28 | ||||
| -rw-r--r-- | patches/fuzzy-sat-include.patch | 83 | ||||
| -rw-r--r-- | patches/fuzzy-sat-install.patch | 34 | ||||
| -rw-r--r-- | patches/fuzzy-sat-unbundle.patch | 346 |
7 files changed, 585 insertions, 2 deletions
diff --git a/README.md b/README.md index eb35d2e..f8e23a4 100644 --- a/README.md +++ b/README.md @@ -36,6 +36,10 @@ Then run `guix pull`. - [python-pacfix]: PAC-learning-based program synthesizer - [taosc]: Makeshift binary patch generator +### Theorem Proving + +- [fuzzy-sat]: Approximate solver for concolic execution + [Guix channel]: https://guix.gnu.org/manual/devel/en/html_node/Channels.html [afl-dyninst]: https://trong.loang.net/~cnx/afl-dyninst/about [Dyninst]: https://github.com/dyninst/dyninst @@ -44,3 +48,4 @@ Then run `guix pull`. [e9patch]: https://github.com/GJDuck/e9patch [python-pacfix]: https://github.com/hsh814/pacfix-python [taosc]: https://trong.loang.net/~cnx/taosc/about +[fuzzy-sat]: https://github.com/season-lab/fuzzy-sat diff --git a/REUSE.toml b/REUSE.toml index 99e95fe..0ed0433 100644 --- a/REUSE.toml +++ b/REUSE.toml @@ -103,10 +103,12 @@ SPDX-License-Identifier = 'CC0-1.0' path = [ 'bugs/cve/2017/14745/crash_1', 'bugs/cve/2017/15025/floatexception.elf' ] SPDX-FileCopyrightText = 'Junchao Luan' +SPDX-License-Identifier = 'CC0-1.0' [[annotations]] path = 'bugs/cve/2017/15232/*.jpg' SPDX-FileCopyrightText = 'Zhao Liang' +S232PDX-License-Identifier = 'CC0-1.0' [[annotations]] path = 'bugs/cve/2018/8806/heap-use-after-free.swf' @@ -121,6 +123,7 @@ SPDX-License-Identifier = 'CC0-1.0' [[annotations]] path = 'bugs/cve/2018/14498/*.bmp' SPDX-FileCopyrightText = 'Hongxu Chen' +SPDX-License-Identifier = 'CC0-1.0' [[annotations]] path = 'bugs/cve/2018/19664/heap-buffer-overflow-2.jpg' @@ -147,6 +150,7 @@ SPDX-License-Identifier = 'CC0-1.0' path = [ 'patches/afl++-*.patch', 'patches/e9patch-*.patch', 'patches/evocatio-*.patch', + 'patches/fuzzy-sat-*.patch', 'patches/jasper-no-define-int-types.patch' ] SPDX-FileCopyrightText = 'Nguyễn Gia Phong' SPDX-License-Identifier = 'GPL-3.0-or-later' diff --git a/loftix/deduction.scm b/loftix/deduction.scm new file mode 100644 index 0000000..bea4420 --- /dev/null +++ b/loftix/deduction.scm @@ -0,0 +1,87 @@ +;;; Packages for theorem provers +;;; +;;; SPDX-FileCopyrightText: 2025 Nguyễn Gia Phong +;;; SPDX-License-Identifier: GPL-3.0-or-later + +(define-module (loftix deduction) + #:use-module (gnu packages) + #:use-module (gnu packages check) + #:use-module (gnu packages digest) + #:use-module (gnu packages maths) + #:use-module (gnu packages pkg-config) + #:use-module (gnu packages python-build) + #:use-module (guix build-system cmake) + #:use-module (guix build-system pyproject) + #:use-module (guix download) + #:use-module (guix gexp) + #:use-module (guix git-download) + #:use-module ((guix licenses) #:prefix license:) + #:use-module (guix packages)) + +(define z3-for-fuzzolic + (let* ((base z3) + (base-version "4.14.1") + (base-tag (string-append "z3-" base-version)) + (revision "fuzzolic") + (commit "8a9e291dc2117e5cf48bdf2810f254000c6dd3d9") + (upstream "https://github.com/Z3Prover/z3")) + (package + (inherit base) + (name "z3-for-fuzzolic") + (version (git-version base-version revision commit)) + (source + (origin + (inherit (package-source base)) + (uri (git-reference (url upstream) + (commit base-tag))) + (file-name (git-file-name name version)) + (sha256 + (base32 "1gdknrqnnigfh1h833ks3vbrp4j74mfg6188c0k4xbl5zv6h6fx5")) + (patches + (list + (origin + (method url-fetch) + (uri (string-append upstream "/compare/" base-tag + ".." commit ".diff")) + (sha256 + (base32 "1qgfz4rz4xm1ivr5s0wz5d16mc1gr5yyc400sfbxm8r288pb56bq")) + (file-name (string-append name ".patch"))))))) + (home-page "https://github.com/season-lab/z3") + (synopsis "Z3 for FUZZOLIC")))) + +(define-public fuzzy-sat + (let ((commit "5939b998a28ce2017b2c0dd89434792ab9ce5e51")) + (package + (name "fuzzy-sat") + (version (git-version "0.1" "master" commit)) + (home-page "https://github.com/season-lab/fuzzy-sat") + (source + (origin + (method git-fetch) + (uri (git-reference (url home-page) + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 "1wm8sznv9w09vfb6nk1c4kbych34zpiywxkz37az81wsvpbwk82s")) + (patches (search-patches "patches/fuzzy-sat-include.patch" + "patches/fuzzy-sat-unbundle.patch" + "patches/fuzzy-sat-install.patch")))) + (build-system cmake-build-system) + (arguments + '(#:phases (modify-phases %standard-phases + (replace 'check + (lambda* (#:key source tests? #:allow-other-keys) + (when (not tests?) + (setenv "FUZZY_BIN" "tools/fuzzy-solver") + (invoke "pytest" "-p" "no:cacheprovider" "-v" + (string-append source "/tests/run.py")))))))) + (native-inputs (list pkg-config python-pytest)) + (inputs (list xxhash z3-for-fuzzolic)) + (synopsis "Approximate solver for concolic execution") + (description "Fuzzy SAT is an approximate solver that borrows ideas +from the fuzzing domain. It is tailored to the symbolic expressions +generated by concolic engines and can replace classic SMT solvers +in this context. By analyzing the expressions contained in symbolic queries, +Fuzzy SAT performs informed mutations to possibly generate +new valuable inputs.") + (license license:gpl2+)))) diff --git a/loftix/fuzzing.scm b/loftix/fuzzing.scm index 6ec3a35..ad8d587 100644 --- a/loftix/fuzzing.scm +++ b/loftix/fuzzing.scm @@ -1,6 +1,6 @@ ;;; Packages for software fuzzing ;;; -;;; SPDX-FileCopyrightText: 2024 Nguyễn Gia Phong +;;; SPDX-FileCopyrightText: 2024-2025 Nguyễn Gia Phong ;;; SPDX-License-Identifier: GPL-3.0-or-later (define-module (loftix fuzzing) @@ -16,7 +16,8 @@ #:use-module (guix git-download) #:use-module ((guix licenses) #:prefix license:) #:use-module (guix packages) - #:use-module (guix utils)) + #:use-module (guix utils) + #:export (for-evocatio)) (define-public afl-dyninst (package @@ -123,3 +124,26 @@ of how an attacker can exploit a bug. Evocatio leverages a capability-guided fuzzer to efficiently uncover new bug capabilities (rather than only generating a single crashing test case for a given bug, as a traditional greybox fuzzer does).")))) + +(define (for-evocatio base) + (package + (inherit base) + (name (string-append (package-name base) "-for-evocatio")) + (arguments + (substitute-keyword-arguments (package-arguments base) + ((#:configure-flags flags #~'()) + #~(cons (string-append "CC=" #$evocatio "/bin/afl-cc") + #$flags)) + ((#:phases phases #~%standard-phases) + #~(modify-phases #$phases + (add-before 'configure 'set-env + (lambda _ + (setenv "CC" #$(file-append evocatio "/bin/afl-cc")) + (setenv "AFL_USE_ASAN" "1") + (setenv "AFL_USE_UBSAN" "1") + (setenv "ASAN_OPTIONS" "detect_leaks=0"))))) + ((#:tests? _ #f) + #f))) + (native-inputs + (modify-inputs (package-native-inputs base) + (append evocatio))))) diff --git a/patches/fuzzy-sat-include.patch b/patches/fuzzy-sat-include.patch new file mode 100644 index 0000000..6798bbd --- /dev/null +++ b/patches/fuzzy-sat-include.patch @@ -0,0 +1,83 @@ +commit bfd24f9cb93fab5317d16c879857221cc70e54c8 +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-04-24 11:25:20 +0900 + + Include stdio.h + +diff --git a/lib/testcase-list.c b/lib/testcase-list.c +index 0aa223b7a7e4..6457fd5cab87 100644 +--- a/lib/testcase-list.c ++++ b/lib/testcase-list.c +@@ -1,4 +1,5 @@ + #include <fts.h> ++#include <stdio.h> + #include <stdlib.h> + #include "testcase-list.h" + +diff --git a/lib/z3-fuzzy-debug-utils.h b/lib/z3-fuzzy-debug-utils.h +index 0f6f3b891a52..7b88add6c294 100644 +--- a/lib/z3-fuzzy-debug-utils.h ++++ b/lib/z3-fuzzy-debug-utils.h +@@ -1,3 +1,5 @@ ++#include <stdio.h> ++ + static inline void print_index_queue(ast_info_ptr data) + { + index_group_t* group; +diff --git a/lib/z3-fuzzy.c b/lib/z3-fuzzy.c +index cac1c329088d..69ecb006fd1f 100644 +--- a/lib/z3-fuzzy.c ++++ b/lib/z3-fuzzy.c +@@ -1,6 +1,7 @@ + #define FUZZY_SOURCE + + #include <fcntl.h> ++#include <stdio.h> + #include <stdlib.h> + #include <unistd.h> + #include "gradient_descend.h" +diff --git a/tools/fuzzy-solver-notify.c b/tools/fuzzy-solver-notify.c +index 821d3aaff15f..97abd8f71488 100644 +--- a/tools/fuzzy-solver-notify.c ++++ b/tools/fuzzy-solver-notify.c +@@ -1,5 +1,6 @@ + #define FUZZY_SOURCE + ++#include <stdio.h> + #include <stdlib.h> + #include <assert.h> + #include <sys/time.h> +diff --git a/tools/fuzzy-solver-vs-z3.c b/tools/fuzzy-solver-vs-z3.c +index 8803ff390fa2..ba4e8f5b979a 100644 +--- a/tools/fuzzy-solver-vs-z3.c ++++ b/tools/fuzzy-solver-vs-z3.c +@@ -1,3 +1,4 @@ ++#include <stdio.h> + #include <stdlib.h> + #include <assert.h> + #include <sys/time.h> +diff --git a/tools/stats-collection-fuzzy.c b/tools/stats-collection-fuzzy.c +index fdef41761726..c793b1df717d 100644 +--- a/tools/stats-collection-fuzzy.c ++++ b/tools/stats-collection-fuzzy.c +@@ -1,3 +1,4 @@ ++#include <stdio.h> + #include <stdlib.h> + #include <assert.h> + #include <sys/time.h> +diff --git a/tools/stats-collection-z3.c b/tools/stats-collection-z3.c +index 504648a1a6c3..f101eeedb32f 100644 +--- a/tools/stats-collection-z3.c ++++ b/tools/stats-collection-z3.c +@@ -1,3 +1,4 @@ ++#include <stdio.h> + #include <stdlib.h> + #include <assert.h> + #include <sys/time.h> +@@ -105,4 +106,4 @@ int main(int argc, char* argv[]) + Z3_del_context(ctx); + fclose(log_file); + return 0; +-} +\ No newline at end of file ++} diff --git a/patches/fuzzy-sat-install.patch b/patches/fuzzy-sat-install.patch new file mode 100644 index 0000000..3ea77a1 --- /dev/null +++ b/patches/fuzzy-sat-install.patch @@ -0,0 +1,34 @@ +commit d36429fa541c69c566f981cd159b82f85d02b4fd +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-04-24 13:10:50 +0900 + + Install libraries and tools + +diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt +index 558c01b7c725..aca4d9210862 100644 +--- a/lib/CMakeLists.txt ++++ b/lib/CMakeLists.txt +@@ -31,7 +31,9 @@ target_link_libraries(Z3Fuzzy_static + target_link_libraries(Z3Fuzzy_shared + PUBLIC ${XXHASH_LIBRARIES} + PUBLIC ${Z3_LIBRARIES}) +-set_target_properties(Z3Fuzzy_static PROPERTIES OUTPUT_NAME Z3Fuzzy) +-set_target_properties(Z3Fuzzy_shared PROPERTIES OUTPUT_NAME Z3Fuzzy) ++set_target_properties(Z3Fuzzy_static PROPERTIES OUTPUT_NAME Z3Fuzzy ++ PUBLIC_HEADER z3-fuzzy.h) ++set_target_properties(Z3Fuzzy_shared PROPERTIES OUTPUT_NAME Z3Fuzzy ++ PUBLIC_HEADER z3-fuzzy.h) + +-install(FILES z3-fuzzy.h DESTINATION include) ++install(TARGETS Z3Fuzzy_shared Z3Fuzzy_static) +diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt +index a9c1a07fc541..732818c3ad9e 100644 +--- a/tools/CMakeLists.txt ++++ b/tools/CMakeLists.txt +@@ -27,3 +27,6 @@ add_executable(stats-collection-z3 + stats-collection-z3.c + pretty-print.c) + LinkBin(stats-collection-z3) ++ ++install(TARGETS fuzzy-solver fuzzy-solver-vs-z3 ++ stats-collection-fuzzy stats-collection-z3) diff --git a/patches/fuzzy-sat-unbundle.patch b/patches/fuzzy-sat-unbundle.patch new file mode 100644 index 0000000..116369d --- /dev/null +++ b/patches/fuzzy-sat-unbundle.patch @@ -0,0 +1,346 @@ +commit 6033d69cf4826ced4f94e7b1543a2bb0ab7a5cbc +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-04-24 11:34:16 +0900 + + Unbundle xxHash and Fuzzolic Z3 + +diff --git a/CMakeLists.txt b/CMakeLists.txt +index 13622ddc6ff4..7cfa95cc7174 100644 +--- a/CMakeLists.txt ++++ b/CMakeLists.txt +@@ -5,6 +5,5 @@ set(CMAKE_POLICY_DEFAULT_CMP0077 NEW) + project(Z3Fuzzy) + + set(Z3_BUILD_PYTHON_BINDINGS true) +-add_subdirectory(fuzzolic-z3) + add_subdirectory(lib) + add_subdirectory(tools) +diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt +index df3a4fa9a614..558c01b7c725 100644 +--- a/lib/CMakeLists.txt ++++ b/lib/CMakeLists.txt +@@ -1,5 +1,9 @@ + cmake_minimum_required(VERSION 3.7) + ++find_package(PkgConfig REQUIRED) ++pkg_check_modules(XXHASH REQUIRED libxxhash) ++find_package(Z3 REQUIRED) ++ + # Strip the binary in release mode + set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -s") + +@@ -18,9 +22,15 @@ set_property(TARGET objZ3FuzzyLib PROPERTY POSITION_INDEPENDENT_CODE 1) + add_library(Z3Fuzzy_static STATIC $<TARGET_OBJECTS:objZ3FuzzyLib>) + add_library(Z3Fuzzy_shared SHARED $<TARGET_OBJECTS:objZ3FuzzyLib>) + +-target_include_directories (objZ3FuzzyLib PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/../fuzzolic-z3/src/api") +-target_link_libraries (Z3Fuzzy_shared LINK_PUBLIC libz3) +- ++target_include_directories(objZ3FuzzyLib ++ PUBLIC ${Z3_C_INCLUDE_DIRS} ++ PUBLIC ${XXHASH_C_INCLUDE_DIRS}) ++target_link_libraries(Z3Fuzzy_static ++ PRIVATE ${XXHASH_LIBRARIES} ++ PRIVATE ${Z3_LIBRARIES}) ++target_link_libraries(Z3Fuzzy_shared ++ PUBLIC ${XXHASH_LIBRARIES} ++ PUBLIC ${Z3_LIBRARIES}) + set_target_properties(Z3Fuzzy_static PROPERTIES OUTPUT_NAME Z3Fuzzy) + set_target_properties(Z3Fuzzy_shared PROPERTIES OUTPUT_NAME Z3Fuzzy) + +diff --git a/lib/z3-fuzzy.c b/lib/z3-fuzzy.c +index 69ecb006fd1f..b5cb8206ebb5 100644 +--- a/lib/z3-fuzzy.c ++++ b/lib/z3-fuzzy.c +@@ -1,6 +1,7 @@ + #define FUZZY_SOURCE + + #include <fcntl.h> ++#include <stdbool.h> + #include <stdio.h> + #include <stdlib.h> + #include <unistd.h> +@@ -92,7 +93,7 @@ static int performing_aggressive_optimistic = 0; + #ifdef USE_MD5_HASH + #include "md5.h" + #else +-#include "xxhash/xxh3.h" ++#include <xxhash.h> + #endif + + // generate parametric data structures +@@ -1491,18 +1492,18 @@ static int __detect_input_group(fuzzy_ctx_t* ctx, Z3_ast node, + unsigned long mask; + if (Z3_get_ast_kind(ctx->z3_ctx, child_1) == + Z3_NUMERAL_AST) { +- Z3_bool successGet = Z3_get_numeral_uint64( ++ bool successGet = Z3_get_numeral_uint64( + ctx->z3_ctx, child_1, (uint64_t*)&mask); +- if (successGet == Z3_FALSE) { ++ if (successGet == false) { + res = 0; + goto BVAND_EXIT; + } + subexpr = child_2; + } else if (Z3_get_ast_kind(ctx->z3_ctx, child_2) == + Z3_NUMERAL_AST) { +- Z3_bool successGet = Z3_get_numeral_uint64( ++ bool successGet = Z3_get_numeral_uint64( + ctx->z3_ctx, child_2, (uint64_t*)&mask); +- if (successGet == Z3_FALSE) { ++ if (successGet == false) { + res = 0; // constant is too big + goto BVAND_EXIT; + } +@@ -1668,7 +1669,7 @@ static int __detect_input_group(fuzzy_ctx_t* ctx, Z3_ast node, + Z3_ast subexpr = NULL; + if (Z3_get_ast_kind(ctx->z3_ctx, child_2) == + Z3_NUMERAL_AST) { +- Z3_bool successGet = Z3_get_numeral_uint64( ++ bool successGet = Z3_get_numeral_uint64( + ctx->z3_ctx, child_2, + (uint64_t*)&shift_val); + if (!successGet) +@@ -1806,7 +1807,7 @@ static int __detect_input_group(fuzzy_ctx_t* ctx, Z3_ast node, + } + case Z3_NUMERAL_AST: { + // uint64_t v; +- // Z3_bool successGet = ++ // bool successGet = + // Z3_get_numeral_uint64(ctx->z3_ctx, node, (uint64_t*)&v); + // if (!successGet || v != 0) + // *approx = 1; +@@ -1918,9 +1919,9 @@ static void __detect_input_to_state_query(fuzzy_ctx_t* ctx, Z3_ast node, + Z3_ast other_child = Z3_get_app_arg(ctx->z3_ctx, node_app, const_operand); + Z3_inc_ref(ctx->z3_ctx, other_child); + if (Z3_get_ast_kind(ctx->z3_ctx, other_child) == Z3_NUMERAL_AST) { +- Z3_bool successGet = Z3_get_numeral_uint64( ++ bool successGet = Z3_get_numeral_uint64( + ctx->z3_ctx, other_child, (uint64_t*)&data->input_to_state_const); +- if (successGet == Z3_FALSE) { ++ if (successGet == false) { + Z3_dec_ref(ctx->z3_ctx, other_child); + data->is_input_to_state = 0; + return; // constant is too big +@@ -2308,7 +2309,7 @@ static void __detect_early_constants(fuzzy_ctx_t* ctx, Z3_ast v, + unsigned long tmp_const; + switch (Z3_get_ast_kind(ctx->z3_ctx, v)) { + case Z3_APP_AST: { +- Z3_bool successGet; ++ bool successGet; + Z3_ast child1, child2; + Z3_app app = Z3_to_app(ctx->z3_ctx, v); + Z3_func_decl decl = Z3_get_app_decl(ctx->z3_ctx, app); +@@ -2364,7 +2365,7 @@ static void __detect_early_constants(fuzzy_ctx_t* ctx, Z3_ast v, + Z3_NUMERAL_AST) { + successGet = Z3_get_numeral_uint64( + ctx->z3_ctx, child1, (uint64_t*)&tmp_const); +- if (successGet == Z3_FALSE) ++ if (successGet == false) + break; // constant bigger than 64 + da_add_item__ulong(&data->values, tmp_const); + da_add_item__ulong(&data->values, tmp_const + 1); +@@ -2373,7 +2374,7 @@ static void __detect_early_constants(fuzzy_ctx_t* ctx, Z3_ast v, + Z3_NUMERAL_AST) { + successGet = Z3_get_numeral_uint64( + ctx->z3_ctx, child2, (uint64_t*)&tmp_const); +- if (successGet == Z3_FALSE) ++ if (successGet == false) + break; // constant bigger than 64 + da_add_item__ulong(&data->values, tmp_const); + da_add_item__ulong(&data->values, tmp_const + 1); +@@ -2400,8 +2401,7 @@ static void __detect_early_constants(fuzzy_ctx_t* ctx, Z3_ast v, + Z3_NUMERAL_AST) { + successGet = Z3_get_numeral_uint64( + ctx->z3_ctx, child1, (uint64_t*)&tmp_const); +- ASSERT_OR_ABORT(successGet == Z3_TRUE, +- "failed to get constant"); ++ ASSERT_OR_ABORT(successGet, "failed to get constant"); + da_add_item__ulong(&data->values, tmp_const); + da_add_item__ulong(&data->values, tmp_const + 1); + da_add_item__ulong(&data->values, tmp_const - 1); +@@ -2409,8 +2409,7 @@ static void __detect_early_constants(fuzzy_ctx_t* ctx, Z3_ast v, + Z3_NUMERAL_AST) { + successGet = Z3_get_numeral_uint64( + ctx->z3_ctx, child2, (uint64_t*)&tmp_const); +- ASSERT_OR_ABORT(successGet == Z3_TRUE, +- "failed to get constant"); ++ ASSERT_OR_ABORT(successGet, "failed to get constant"); + da_add_item__ulong(&data->values, tmp_const); + da_add_item__ulong(&data->values, tmp_const + 1); + da_add_item__ulong(&data->values, tmp_const - 1); +@@ -2527,9 +2526,9 @@ __detect_all_constants(fuzzy_ctx_t* ctx, Z3_ast v, ast_data_t* data) + } + case Z3_NUMERAL_AST: { + unsigned long tmp_const; +- Z3_bool successGet = ++ bool successGet = + Z3_get_numeral_uint64(ctx->z3_ctx, v, (uint64_t*)&tmp_const); +- ASSERT_OR_ABORT(successGet == Z3_TRUE, "failed to get constant"); ++ ASSERT_OR_ABORT(successGet, "failed to get constant"); + da_add_item__ulong(&data->values, tmp_const); + da_add_item__ulong(&data->values, tmp_const + 1); + da_add_item__ulong(&data->values, tmp_const - 1); +@@ -2695,9 +2694,9 @@ static inline int __find_child_constant(Z3_context ctx, Z3_app app, + for (i = 0; i < num_fields; ++i) { + Z3_ast child = Z3_get_app_arg(ctx, app, i); + if (Z3_get_ast_kind(ctx, child) == Z3_NUMERAL_AST) { +- Z3_bool successGet = ++ bool successGet = + Z3_get_numeral_uint64(ctx, child, (uint64_t*)constant); +- if (successGet == Z3_FALSE) ++ if (successGet == false) + return 0; // constant is too big + condition_ok = 1; + *const_operand = i; +@@ -2915,10 +2914,10 @@ static inline int __check_if_range(fuzzy_ctx_t* ctx, Z3_ast expr, + + if (Z3_get_ast_kind(ctx->z3_ctx, tmp_expr) == Z3_NUMERAL_AST) { + uint64_t v; +- Z3_bool successGet = ++ bool successGet = + Z3_get_numeral_uint64(ctx->z3_ctx, tmp_expr, &v); + +- if (successGet != Z3_FALSE && v == 0) { ++ if (successGet != false && v == 0) { + has_zext = 1; + Z3_ast old_non_const_operand = non_const_operand; + non_const_operand = +@@ -3163,7 +3162,7 @@ static inline int __detect_strcmp_pattern(fuzzy_ctx_t* ctx, Z3_ast ast, + ... + (ite (= inp_i const_i) #b1 #b0))) + */ +- Z3_bool successGet; ++ bool successGet; + unsigned i; + Z3_ast_kind kind = Z3_get_ast_kind(ctx->z3_ctx, ast); + if (kind != Z3_APP_AST) +@@ -8353,14 +8352,14 @@ unsigned long z3fuzz_evaluate_expression_z3(fuzzy_ctx_t* ctx, Z3_ast query, + + // evaluate the query in the model + Z3_ast solution; +- Z3_bool successfulEval = +- Z3_model_eval(ctx->z3_ctx, z3_m, query, Z3_TRUE, &solution); ++ bool successfulEval = ++ Z3_model_eval(ctx->z3_ctx, z3_m, query, true, &solution); + ASSERT_OR_ABORT(successfulEval, "Failed to evaluate model"); + + Z3_model_dec_ref(ctx->z3_ctx, z3_m); + if (Z3_get_ast_kind(ctx->z3_ctx, solution) == Z3_NUMERAL_AST) { +- Z3_bool successGet = Z3_get_numeral_uint64(ctx->z3_ctx, solution, &res); +- ASSERT_OR_ABORT(successGet == Z3_TRUE, ++ bool successGet = Z3_get_numeral_uint64(ctx->z3_ctx, solution, &res); ++ ASSERT_OR_ABORT(successGet, + "z3fuzz_evaluate_expression_z3() failed to get " + "constant"); + } else +diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt +index 7af05f878bec..a9c1a07fc541 100644 +--- a/tools/CMakeLists.txt ++++ b/tools/CMakeLists.txt +@@ -1,9 +1,10 @@ + cmake_minimum_required(VERSION 3.7) + ++find_package(Z3 REQUIRED) + macro(LinkBin exe_name) +- target_link_libraries(${exe_name} LINK_PUBLIC libz3) ++ target_link_libraries(${exe_name} LINK_PUBLIC ${Z3_LIBRARIES}) + target_link_libraries(${exe_name} LINK_PUBLIC Z3Fuzzy_static) +- target_include_directories(${exe_name} PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/../fuzzolic-z3/src/api") ++ target_include_directories(${exe_name} PUBLIC ${Z3_C_INCLUDE_DIRS}) + target_include_directories(${exe_name} PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/../lib") + endmacro() + +diff --git a/tools/fuzzy-solver-notify.c b/tools/fuzzy-solver-notify.c +index 97abd8f71488..c0cca0ecb6ee 100644 +--- a/tools/fuzzy-solver-notify.c ++++ b/tools/fuzzy-solver-notify.c +@@ -1,5 +1,6 @@ + #define FUZZY_SOURCE + ++#include <stdbool.h> + #include <stdio.h> + #include <stdlib.h> + #include <assert.h> +@@ -119,8 +120,8 @@ static uint64_t Z3_eval(Z3_context ctx, Z3_ast query, uint64_t* data, + + // evaluate the query in the model + Z3_ast solution; +- Z3_bool successfulEval = +- Z3_model_eval(ctx, z3_m, query, Z3_TRUE, &solution); ++ bool successfulEval = ++ Z3_model_eval(ctx, z3_m, query, true, &solution); + if (!successfulEval) { + puts("Failed to evaluate model"); + exit(1); +@@ -128,8 +129,8 @@ static uint64_t Z3_eval(Z3_context ctx, Z3_ast query, uint64_t* data, + + Z3_model_dec_ref(ctx, z3_m); + if (Z3_get_ast_kind(ctx, solution) == Z3_NUMERAL_AST) { +- Z3_bool successGet = Z3_get_numeral_uint64(ctx, solution, &res); +- if (successGet != Z3_TRUE) { ++ bool successGet = Z3_get_numeral_uint64(ctx, solution, &res); ++ if (successGet != true) { + puts("Z3_get_numeral_uint64() failed to get constant"); + exit(1); + } +diff --git a/tools/maxmin-driver.c b/tools/maxmin-driver.c +index 2e32f6410f68..26963f780223 100644 +--- a/tools/maxmin-driver.c ++++ b/tools/maxmin-driver.c +@@ -1,3 +1,4 @@ ++#include <stdbool.h> + #include <stdlib.h> + #include <assert.h> + #include <sys/time.h> +@@ -36,14 +37,14 @@ static inline void dump_proof(Z3_context ctx, Z3_model m, + Z3_ast s_bv = Z3_mk_const(ctx, s, bsort); + + Z3_ast solution; +- Z3_bool successfulEval = ++ bool successfulEval = + Z3_model_eval(ctx, m, s_bv, +- /*model_completion=*/Z3_TRUE, &solution); ++ /*model_completion=*/true, &solution); + assert(successfulEval && "Failed to evaluate model"); + + int solution_byte = 0; +- Z3_bool successGet = Z3_get_numeral_int(ctx, solution, &solution_byte); +- assert (successGet == Z3_TRUE); ++ bool successGet = Z3_get_numeral_int(ctx, solution, &solution_byte); ++ assert (successGet); + fwrite(&solution_byte, sizeof(char), 1, fp); + } + fclose(fp); +@@ -140,12 +141,12 @@ int main(int argc, char* argv[]) + dump_proof(ctx, m, "tests/max_val_z3.bin"); + + Z3_ast solution; +- Z3_bool successfulEval = ++ bool successfulEval = + Z3_model_eval(ctx, m, bv, +- /*model_completion=*/Z3_TRUE, &solution); ++ /*model_completion=*/true, &solution); + assert(successfulEval && "Failed to evaluate model"); + +- Z3_bool successGet = Z3_get_numeral_uint64(ctx, solution, &max_val_z3); ++ bool successGet = Z3_get_numeral_uint64(ctx, solution, &max_val_z3); + assert(successGet && "Failed to get numeral int"); + + Z3_model_dec_ref(ctx, m); +@@ -172,12 +173,12 @@ int main(int argc, char* argv[]) + dump_proof(ctx, m, "tests/min_val_z3.bin"); + + Z3_ast solution; +- Z3_bool successfulEval = ++ bool successfulEval = + Z3_model_eval(ctx, m, bv, +- /*model_completion=*/Z3_TRUE, &solution); ++ /*model_completion=*/true, &solution); + assert(successfulEval && "Failed to evaluate model"); + +- Z3_bool successGet = Z3_get_numeral_uint64(ctx, solution, &min_val_z3); ++ bool successGet = Z3_get_numeral_uint64(ctx, solution, &min_val_z3); + assert(successGet && "Failed to get numeral int"); + Z3_model_dec_ref(ctx, m); + break; |