diff options
Diffstat (limited to 'patches/fuzzy-sat-unbundle.patch')
| -rw-r--r-- | patches/fuzzy-sat-unbundle.patch | 346 |
1 files changed, 346 insertions, 0 deletions
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; |