commit 6033d69cf4826ced4f94e7b1543a2bb0ab7a5cbc Author: Nguyễn Gia Phong 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 $) add_library(Z3Fuzzy_shared SHARED $) -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 +#include #include #include #include @@ -92,7 +93,7 @@ static int performing_aggressive_optimistic = 0; #ifdef USE_MD5_HASH #include "md5.h" #else -#include "xxhash/xxh3.h" +#include #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 #include #include #include @@ -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 #include #include #include @@ -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;