diff options
Diffstat (limited to 'patches')
| -rw-r--r-- | patches/e9patch-check.patch | 3 | ||||
| -rw-r--r-- | patches/fuzzolic-python-package.patch | 39 | ||||
| -rw-r--r-- | patches/fuzzolic-relax-perf-test.patch | 13 | ||||
| -rw-r--r-- | patches/fuzzolic-showmap.patch | 69 | ||||
| -rw-r--r-- | patches/fuzzolic-solver-install.patch | 10 | ||||
| -rw-r--r-- | patches/fuzzolic-solver-unbundle.patch | 598 | ||||
| -rw-r--r-- | patches/fuzzolic-test-fix-runner.patch | 326 | ||||
| -rw-r--r-- | patches/fuzzolic-test-skip-nondeterministic.patch | 23 | ||||
| -rw-r--r-- | patches/fuzzolic-timeout-solver.patch | 22 | ||||
| -rw-r--r-- | patches/fuzzolic-unbundle.patch | 108 | ||||
| -rw-r--r-- | patches/fuzzolic-utils-make.patch | 34 | ||||
| -rw-r--r-- | patches/fuzzy-sat-install.patch | 65 | ||||
| -rw-r--r-- | patches/fuzzy-sat-unbundle.patch | 346 | ||||
| -rw-r--r-- | patches/qemu-for-fuzzolic-static-global.patch | 24 | ||||
| -rw-r--r-- | patches/qemu-for-fuzzolic-test-opts-range-beyond.patch | 97 |
15 files changed, 1776 insertions, 1 deletions
diff --git a/patches/e9patch-check.patch b/patches/e9patch-check.patch index d060c9f..bf39bd2 100644 --- a/patches/e9patch-check.patch +++ b/patches/e9patch-check.patch @@ -162,7 +162,7 @@ new file mode 100755 index 000000000000..d22009e99b72 --- /dev/null +++ b/test/regtest/regtest -@@ -0,0 +1,25 @@ +@@ -0,0 +1,26 @@ +#!/bin/sh +fails=() +for exe in $* @@ -176,6 +176,7 @@ index 000000000000..d22009e99b72 + then ./exec.sh ./$cmd 1>$out 2>&1 + else ./exec.sh ./$exe 1>$out 2>&1 + fi ++ sed -i 's/ (core dumped)$//' $out + + diff -u $out $exp + if test $? -ne 0 diff --git a/patches/fuzzolic-python-package.patch b/patches/fuzzolic-python-package.patch new file mode 100644 index 0000000..8ef5559 --- /dev/null +++ b/patches/fuzzolic-python-package.patch @@ -0,0 +1,39 @@ +commit 5098598289744766508d7b390f19d61bad30f54c +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-05-07 14:34:24 +0900 + + Turn fuzzolic/ into a Python package + +diff --git a/fuzzolic/executor.py b/fuzzolic/executor.py +index 39c6aa6dddb9..f2639eb8da6a 100644 +--- a/fuzzolic/executor.py ++++ b/fuzzolic/executor.py +@@ -17,8 +17,8 @@ import random + import ctypes + import resource + +-import minimizer_qsym +-import minimizer ++from . import minimizer_qsym ++from . import minimizer + + SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__)) + SOLVER_SMT_BIN = SCRIPT_DIR + '/../solver/solver-smt' +diff --git a/fuzzolic/fuzzolic.py b/fuzzolic/fuzzolic.py +index ed6aac5cf5ab..3b692fb4b59c 100755 +--- a/fuzzolic/fuzzolic.py ++++ b/fuzzolic/fuzzolic.py +@@ -2,11 +2,12 @@ + + import os + import sys +-import executor + import signal + import argparse + import shutil + ++from . import executor ++ + ABORTING_COUNT = 0 + + diff --git a/patches/fuzzolic-relax-perf-test.patch b/patches/fuzzolic-relax-perf-test.patch new file mode 100644 index 0000000..f1de80a --- /dev/null +++ b/patches/fuzzolic-relax-perf-test.patch @@ -0,0 +1,13 @@ +diff --git a/tests/run.py b/tests/run.py +index 2144d96c7544..1d84a2999662 100755 +--- a/tests/run.py ++++ b/tests/run.py +@@ -78,7 +78,7 @@ def run(test, + if perf_run: + slowdown = emulated_time / native_time + print("Slowdown: %s" % round(slowdown, 1)) +- assert slowdown < 70 ++ assert slowdown < 140 + + if expected_inputs > 0: + testcases = glob.glob(WORKDIR + "/tests/test_*.dat") diff --git a/patches/fuzzolic-showmap.patch b/patches/fuzzolic-showmap.patch new file mode 100644 index 0000000..ec9d99e --- /dev/null +++ b/patches/fuzzolic-showmap.patch @@ -0,0 +1,69 @@ +diff --git a/src/afl-showmap.c b/src/afl-showmap.c +index 881ca2a63ffe..a3485b881b3e 100644 +--- a/src/afl-showmap.c ++++ b/src/afl-showmap.c +@@ -410,15 +410,16 @@ void pre_afl_fsrv_write_to_testcase(afl_forkserver_t *fsrv, u8 *mem, u32 len) { + + /* Execute target application. */ + +-static void showmap_run_target_forkserver(afl_forkserver_t *fsrv, u8 *mem, +- u32 len) { ++static fsrv_run_result_t showmap_run_target_forkserver(afl_forkserver_t *fsrv, ++ u8 *mem, u32 len) { + + pre_afl_fsrv_write_to_testcase(fsrv, mem, len); + + if (!quiet_mode) { SAYF("-- Program output begins --\n" cRST); } + +- if (afl_fsrv_run_target(fsrv, fsrv->exec_tmout, &stop_soon) == +- FSRV_RUN_ERROR) { ++ const fsrv_run_result_t result = ++ afl_fsrv_run_target(fsrv, fsrv->exec_tmout, &stop_soon); ++ if (result == FSRV_RUN_ERROR) { + + FATAL("Error running target"); + +@@ -477,6 +478,7 @@ static void showmap_run_target_forkserver(afl_forkserver_t *fsrv, u8 *mem, + + } + ++ return result; + } + + /* Read initial file. */ +@@ -867,7 +869,11 @@ u32 execute_testcases(u8 *dir) { + + } + +- showmap_run_target_forkserver(fsrv, in_data, in_len); ++ if (showmap_run_target_forkserver(fsrv, in_data, in_len) ++ == FSRV_RUN_CRASH) ++ snprintf(outfile, sizeof(outfile), "%s/%s.crash", out_file, fn2); ++ else ++ snprintf(outfile, sizeof(outfile), "%s/%s", out_file, fn2); + ck_free(in_data); + ++done; + +@@ -1422,9 +1428,19 @@ int main(int argc, char **argv_orig, char **envp) { + + } + +- stdin_file = at_file ? strdup(at_file) +- : (char *)alloc_printf("%s/.afl-showmap-temp-%u", +- use_dir, (u32)getpid()); ++ if (at_file) { ++ stdin_file = strdup(at_file); ++ } else { ++ char* file_ext = get_afl_env("FILE_EXT"); ++ if (file_ext) ++ stdin_file = ++ (char *)alloc_printf("%s/.afl-showmap-temp-%u.%s", ++ use_dir, (u32)getpid(), file_ext); ++ else ++ stdin_file = ++ (char *)alloc_printf("%s/.afl-showmap-temp-%u", ++ use_dir, (u32)getpid()); ++ } + unlink(stdin_file); + + // If @@ are in the target args, replace them and also set use_stdin=false. diff --git a/patches/fuzzolic-solver-install.patch b/patches/fuzzolic-solver-install.patch new file mode 100644 index 0000000..430356e --- /dev/null +++ b/patches/fuzzolic-solver-install.patch @@ -0,0 +1,10 @@ +diff --git a/solver/CMakeLists.txt b/solver/CMakeLists.txt +index a159187a5b27..9618f9a0576d 100644 +--- a/solver/CMakeLists.txt ++++ b/solver/CMakeLists.txt +@@ -28,3 +28,5 @@ set(CMAKE_CXX_FLAGS "-Wall -Wextra -O3 -g") + set(CMAKE_C_FLAGS "-O3 -g") + #set(CMAKE_CXX_FLAGS_DEBUG "-g") + #set(CMAKE_CXX_FLAGS_RELEASE "-O3") ++ ++install(TARGETS solver-smt solver-fuzzy) diff --git a/patches/fuzzolic-solver-unbundle.patch b/patches/fuzzolic-solver-unbundle.patch new file mode 100644 index 0000000..f34940d --- /dev/null +++ b/patches/fuzzolic-solver-unbundle.patch @@ -0,0 +1,598 @@ +commit 7b451dd864314d30aa4137163aa318fad711833b +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-04-29 11:23:26 +0900 + + Unbundle FUZZY-SAT, QEMU, xxHash and Z3 + +diff --git a/solver/CMakeLists.txt b/solver/CMakeLists.txt +index a159187a5b27..4a252172da29 100644 +--- a/solver/CMakeLists.txt ++++ b/solver/CMakeLists.txt +@@ -2,27 +2,40 @@ cmake_minimum_required(VERSION 3.7) + + project(Solver) + +-add_executable(solver-smt main.c i386.c branch_coverage.c opts.c xxHash/xxhash.c) +-add_executable(solver-fuzzy main.c i386.c branch_coverage.c opts.c xxHash/xxhash.c) ++add_executable(solver-smt main.c i386.c branch_coverage.c opts.c) ++add_executable(solver-fuzzy main.c i386.c branch_coverage.c opts.c) + + target_compile_definitions(solver-smt PRIVATE USE_FUZZY_SOLVER=0) + target_compile_definitions(solver-fuzzy PRIVATE USE_FUZZY_SOLVER=1) + + # z3 +-target_link_libraries(solver-smt z3) +-target_link_libraries(solver-fuzzy z3) ++find_package(Z3 REQUIRED) ++target_include_directories(solver-smt PRIVATE ${Z3_INCLUDE_DIRS}) ++target_include_directories(solver-fuzzy PRIVATE ${Z3_INCLUDE_DIRS}) ++target_link_libraries(solver-smt ${Z3_LIBRARIES}) ++target_link_libraries(solver-fuzzy ${Z3_LIBRARIES}) + + # fuzzy +-target_link_libraries(solver-smt ${CMAKE_SOURCE_DIR}/fuzzy-sat/libZ3Fuzzy.a) +-target_link_libraries(solver-fuzzy ${CMAKE_SOURCE_DIR}/fuzzy-sat/libZ3Fuzzy.a) ++find_package(Z3Fuzzy REQUIRED) ++target_include_directories(solver-smt PRIVATE ${Z3Fuzzy_INCLUDE_DIRS}) ++target_include_directories(solver-fuzzy PRIVATE ${Z3Fuzzy_INCLUDE_DIRS}) ++target_link_libraries(solver-smt "Z3Fuzzy") ++target_link_libraries(solver-fuzzy "Z3Fuzzy") + + # glib + find_package(PkgConfig REQUIRED) + pkg_search_module(GLIB REQUIRED glib-2.0) + target_include_directories(solver-smt PRIVATE ${GLIB_INCLUDE_DIRS}) + target_include_directories(solver-fuzzy PRIVATE ${GLIB_INCLUDE_DIRS}) +-target_link_libraries(solver-smt ${GLIB_LDFLAGS}) +-target_link_libraries(solver-fuzzy ${GLIB_LDFLAGS}) ++target_link_libraries(solver-smt ${GLIB_LIBRARIES}) ++target_link_libraries(solver-fuzzy ${GLIB_LIBRARIES}) ++ ++# xxHash ++pkg_search_module(XXHASH REQUIRED libxxhash) ++target_include_directories(solver-smt PRIVATE ${XXHASH_INCLUDE_DIRS}) ++target_include_directories(solver-fuzzy PRIVATE ${XXHASH_INCLUDE_DIRS}) ++target_link_libraries(solver-smt ${XXHASH_LIBRARIES}) ++target_link_libraries(solver-fuzzy ${XXHASH_LIBRARIES}) + + set(CMAKE_CXX_FLAGS "-Wall -Wextra -O3 -g") + set(CMAKE_C_FLAGS "-O3 -g") +diff --git a/solver/branch_coverage.c b/solver/branch_coverage.c +index 4d726f6e592c..88ca22b37ad2 100644 +--- a/solver/branch_coverage.c ++++ b/solver/branch_coverage.c +@@ -3,8 +3,7 @@ + + extern Config config; + +-#define XXH_STATIC_LINKING_ONLY +-#include "xxHash/xxhash.h" ++#include <xxhash.h> + + #include <stdio.h> + +@@ -42,11 +41,13 @@ static inline uintptr_t hash_pc(uintptr_t pc, uint8_t taken) + taken = 1; + } + +- XXH32_state_t state; +- XXH32_reset(&state, 0); // seed = 0 +- XXH32_update(&state, &pc, sizeof(pc)); +- XXH32_update(&state, &taken, sizeof(taken)); +- return XXH32_digest(&state) % BRANCH_BITMAP_SIZE; ++ XXH32_state_t *state = XXH32_createState(); ++ XXH32_reset(state, 0); // seed = 0 ++ XXH32_update(state, &pc, sizeof(pc)); ++ XXH32_update(state, &taken, sizeof(taken)); ++ const uintptr_t digest = XXH32_digest(state) % BRANCH_BITMAP_SIZE; ++ XXH32_freeState(state); ++ return digest; + } + + static inline void load_bitmap(const char* path, uint8_t* data, size_t size) +@@ -126,17 +127,17 @@ static inline int is_interesting_context(uintptr_t h, uint8_t bits) + gpointer key, value; + GHashTableIter iter; + g_hash_table_iter_init(&iter, visited_branches); ++ XXH32_state_t *state = XXH32_createState(); + while (g_hash_table_iter_next(&iter, &key, &value)) { + + uintptr_t prev_h = (uintptr_t)key; + + // Calculate hash(prev_h || h) +- XXH32_state_t state; +- XXH32_reset(&state, 0); +- XXH32_update(&state, &prev_h, sizeof(prev_h)); +- XXH32_update(&state, &h, sizeof(h)); ++ XXH32_reset(state, 0); ++ XXH32_update(state, &prev_h, sizeof(prev_h)); ++ XXH32_update(state, &h, sizeof(h)); + +- uintptr_t hash = XXH32_digest(&state) % (BRANCH_BITMAP_SIZE * CHAR_BIT); ++ uintptr_t hash = XXH32_digest(state) % (BRANCH_BITMAP_SIZE * CHAR_BIT); + uintptr_t idx = hash / CHAR_BIT; + uintptr_t mask = 1 << (hash % CHAR_BIT); + +@@ -145,6 +146,7 @@ static inline int is_interesting_context(uintptr_t h, uint8_t bits) + interesting = 1; + } + } ++ XXH32_freeState(state); + + if (bits == 0) { + g_hash_table_add(visited_branches, (gpointer)h); +diff --git a/solver/debug.h b/solver/debug.h +index b3ce2405074a..02614765f780 100644 +--- a/solver/debug.h ++++ b/solver/debug.h +@@ -17,6 +17,8 @@ + #ifndef _HAVE_DEBUG_H + #define _HAVE_DEBUG_H + ++#include <z3.h> ++ + #include <errno.h> + + //#include "config.h" +diff --git a/solver/eval-driver.c b/solver/eval-driver.c +index 1140a87570a8..25390384114b 100644 +--- a/solver/eval-driver.c ++++ b/solver/eval-driver.c +@@ -14,7 +14,6 @@ + #include <stdlib.h> + #include <assert.h> + #include <sys/time.h> +-static_assert(Z3_VERSION == 487, "This executable requires z3 4.8.7+"); + + typedef struct { + uint8_t* data; +@@ -120,15 +119,15 @@ unsigned long z3fuzz_evaluate_expression_z3(Z3_context ctx, + + // 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); + assert(successfulEval && "Failed to evaluate model"); + + 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); +- assert(successGet == Z3_TRUE && +- "z3fuzz_evaluate_expression_z3() failed to get " ++ bool successGet = Z3_get_numeral_uint64(ctx, solution, &res); ++ assert(successGet ++ && "z3fuzz_evaluate_expression_z3() failed to get " + "constant"); + } else + res = Z3_get_bool_value(ctx, solution) == Z3_L_TRUE ? 1UL : 0UL; +@@ -179,15 +178,11 @@ __evaluate_expression(Z3_context ctx, Z3_ast value, Z3_ast* values, + Z3_symbol s = Z3_get_decl_name(ctx, decl); + #if 0 + int symbol_index = Z3_get_symbol_int(ctx, s); +- Z3_bool successGet = ++ bool successGet = + Z3_get_numeral_uint64(ctx, values[symbol_index], +-#if Z3_VERSION <= 451 +- (long long unsigned int*)&res +-#else + (uint64_t*)&res +-#endif + ); +- assert(successGet == Z3_TRUE && ++ assert(successGet && + "z3fuzz_evaluate_expression() failed to get " + "constant (symbol)"); + #else +@@ -971,15 +966,9 @@ __evaluate_expression(Z3_context ctx, Z3_ast value, Z3_ast* values, + break; + } + case Z3_NUMERAL_AST: { +- Z3_bool successGet = +- Z3_get_numeral_uint64(ctx, value, +-#if Z3_VERSION <= 451 +- (long long unsigned int*)&res +-#else +- (uint64_t*)&res +-#endif +- ); +- assert(successGet == Z3_TRUE && ++ bool successGet = ++ Z3_get_numeral_uint64(ctx, value, (uint64_t*) &res); ++ assert(successGet && + "z3fuzz_evaluate_expression() failed to get constant"); + break; + } +diff --git a/solver/eval.c b/solver/eval.c +index 4fd0e11bc187..837f1152adb9 100644 +--- a/solver/eval.c ++++ b/solver/eval.c +@@ -1,6 +1,4 @@ +- +-#define XXH_STATIC_LINKING_ONLY +-#include "xxHash/xxhash.h" ++#include <xxhash.h> + + #define DICT_DATA_T uint64_t + #include "dict.h" +@@ -534,12 +532,8 @@ static uintptr_t conc_eval(uint8_t* m, size_t n, dict__uint64_t* m_others, + + case Z3_NUMERAL_AST: { + uint64_t value; +- Z3_bool r = Z3_get_numeral_uint64(ctx, e, +-#if Z3_VERSION <= 451 +- (long long unsigned int*) +-#endif +- &value); +- assert(r == Z3_TRUE); ++ bool r = Z3_get_numeral_uint64(ctx, e, &value); ++ assert(r); + res = value; + break; + } +diff --git a/solver/fuzzy-solver-expr.c b/solver/fuzzy-solver-expr.c +index a54b782456d7..f5a44032230c 100644 +--- a/solver/fuzzy-solver-expr.c ++++ b/solver/fuzzy-solver-expr.c +@@ -7,9 +7,6 @@ + #include <time.h> + #include <unistd.h> + +-#include <z3.h> +-#define Z3_VERSION 487 +- + #define USE_COLOR + #include "debug.h" + +@@ -17,7 +14,9 @@ + #define EXPR_QUEUE_POLLING_TIME_NS 5000 + + #include "index-queue.h" +-#include "../tracer/tcg/symbolic/symbolic-struct.h" ++ ++#include <qemu/tcg/symbolic/symbolic-struct.h> ++#include <z3.h> + + static unsigned char* testcase_bytes = 0; + static unsigned char* tmp_testcase = 0; +@@ -40,17 +39,9 @@ static void exitf(const char* message) + exit(1); + } + +-#if Z3_VERSION <= 441 +-static void smt_error_handler(Z3_context c) +-#else + static void smt_error_handler(Z3_context c, Z3_error_code e) +-#endif + { +-#if Z3_VERSION <= 441 +- printf("Error code: %s\n", Z3_get_error_msg(smt_solver.ctx)); +-#else + printf("Error code: %s\n", Z3_get_error_msg(smt_solver.ctx, e)); +-#endif + exitf("incorrect use of Z3"); + } + +@@ -141,14 +132,14 @@ static void smt_dump_solution(Z3_model m) + Z3_ast input_slice = Z3_mk_extract(smt_solver.ctx, (8 * (i + 1)) - 1, + 8 * i, cached_input); + Z3_ast solution; +- Z3_bool successfulEval = ++ bool successfulEval = + Z3_model_eval(smt_solver.ctx, m, input_slice, +- /*model_completion=*/Z3_TRUE, &solution); ++ /*model_completion=*/true, &solution); + assert(successfulEval && "Failed to evaluate model"); + assert(Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_NUMERAL_AST && + "Evaluated expression has wrong sort"); + int solution_byte = 0; +- Z3_bool successGet = ++ bool successGet = + Z3_get_numeral_int(smt_solver.ctx, solution, &solution_byte); + if (solution_byte) + printf("Solution[%ld]: %x\n", i, solution_byte); +diff --git a/solver/fuzzy-solver.c b/solver/fuzzy-solver.c +index 5661dffb0dcb..42bb37f6c890 100644 +--- a/solver/fuzzy-solver.c ++++ b/solver/fuzzy-solver.c +@@ -7,8 +7,6 @@ + #include <time.h> + #include <unistd.h> + +-#include <z3.h> +-#define Z3_VERSION 487 + + #define FOUND_SUB_AND 1 + #define FOUND_COMPARISON 2 +@@ -23,7 +21,9 @@ + + #include "index-queue.h" + #include "testcase-list.h" +-#include "../tracer/tcg/symbolic/symbolic-struct.h" ++ ++#include <qemu/tcg/symbolic/symbolic-struct.h> ++#include <z3.h> + + static int expr_pool_shm_id = -1; + Expr* pool; +@@ -48,17 +48,9 @@ static void exitf(const char* message) + exit(1); + } + +-#if Z3_VERSION <= 441 +-static void smt_error_handler(Z3_context c) +-#else + static void smt_error_handler(Z3_context c, Z3_error_code e) +-#endif + { +-#if Z3_VERSION <= 441 +- printf("Error code: %s\n", Z3_get_error_msg(smt_solver.ctx)); +-#else + printf("Error code: %s\n", Z3_get_error_msg(smt_solver.ctx, e)); +-#endif + exitf("incorrect use of Z3"); + } + +@@ -131,9 +123,9 @@ static void smt_dump_solution(Z3_model m) + Z3_ast input_slice = Z3_mk_extract(smt_solver.ctx, (8 * (i + 1)) - 1, + 8 * i, cached_input); + Z3_ast solution; +- Z3_bool successfulEval = ++ bool successfulEval = + Z3_model_eval(smt_solver.ctx, m, input_slice, +- /*model_completion=*/Z3_TRUE, &solution); ++ /*model_completion=*/true, &solution); + assert(successfulEval && "Failed to evaluate model"); + solution = Z3_simplify(smt_solver.ctx, + solution); // otherwise, concrete expression... +@@ -141,7 +133,7 @@ static void smt_dump_solution(Z3_model m) + assert(Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_NUMERAL_AST && + "Evaluated expression has wrong sort"); + int solution_byte = 0; +- Z3_bool successGet = ++ bool successGet = + Z3_get_numeral_int(smt_solver.ctx, solution, &solution_byte); + if (solution_byte) + printf("Solution[%ld]: %x\n", i, solution_byte); +@@ -191,7 +183,7 @@ static int ast_find_early_constants(Z3_ast v, unsigned long* sub_add, + int res = 0; + switch (Z3_get_ast_kind(smt_solver.ctx, v)) { + case Z3_APP_AST: { +- Z3_bool successGet; ++ bool successGet; + Z3_ast child1, child2; + Z3_app app = Z3_to_app(smt_solver.ctx, v); + Z3_func_decl decl = Z3_get_app_decl(smt_solver.ctx, app); +@@ -218,15 +210,13 @@ static int ast_find_early_constants(Z3_ast v, unsigned long* sub_add, + Z3_NUMERAL_AST) { + successGet = Z3_get_numeral_uint64(smt_solver.ctx, + child1, comparison); +- assert(successGet == Z3_TRUE && +- "failed to get constant"); ++ assert(successGet && "failed to get constant"); + res = FOUND_COMPARISON; + } else if (Z3_get_ast_kind(smt_solver.ctx, child2) == + Z3_NUMERAL_AST) { + successGet = Z3_get_numeral_uint64(smt_solver.ctx, + child2, comparison); +- assert(successGet == Z3_TRUE && +- "failed to get constant"); ++ assert(successGet && "failed to get constant"); + res = FOUND_COMPARISON; + } + +@@ -255,15 +245,13 @@ static int ast_find_early_constants(Z3_ast v, unsigned long* sub_add, + Z3_NUMERAL_AST) { + successGet = Z3_get_numeral_uint64(smt_solver.ctx, + child1, sub_add); +- assert(successGet == Z3_TRUE && +- "failed to get constant"); ++ assert(successGet && "failed to get constant"); + res = FOUND_SUB_AND; + } else if (Z3_get_ast_kind(smt_solver.ctx, child2) == + Z3_NUMERAL_AST) { + successGet = Z3_get_numeral_uint64(smt_solver.ctx, + child2, sub_add); +- assert(successGet == Z3_TRUE && +- "failed to get constant"); ++ assert(successGet && "failed to get constant"); + res = FOUND_SUB_AND; + } + break; +@@ -352,9 +340,9 @@ static void ast_find_involved_inputs(Z3_ast v) + switch (Z3_get_ast_kind(smt_solver.ctx, v)) { + case Z3_NUMERAL_AST: { + unsigned long value = -1; +- Z3_bool successGet = ++ bool successGet = + Z3_get_numeral_uint64(smt_solver.ctx, v, &value); +- assert(successGet == Z3_TRUE && "failed to get constant"); ++ assert(successGet && "failed to get constant"); + ADD_VALUE(value); + break; + } +@@ -457,8 +445,8 @@ static int smt_query_evaluate(Z3_symbol input, Z3_ast input_val, Z3_ast query, + + // evaluate the query in the model + Z3_ast solution; +- Z3_bool successfulEval = +- Z3_model_eval(smt_solver.ctx, z3_m, query, Z3_TRUE, &solution); ++ bool successfulEval = ++ Z3_model_eval(smt_solver.ctx, z3_m, query, true, &solution); + assert(successfulEval && "Failed to evaluate model"); + assert(Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_APP_AST && + "Evaluated expression has wrong sort"); +diff --git a/solver/main.c b/solver/main.c +index 42bedd8841fa..d0a0b58d51cd 100644 +--- a/solver/main.c ++++ b/solver/main.c +@@ -9,11 +9,11 @@ + #include <execinfo.h> + #include <string.h> + ++#include <z3-fuzzy.h> ++ + #include "debug-config.h" + #include "solver.h" + #include "i386.h" +-#include "fuzzy-sat/z3-fuzzy.h" +- + + #define EXPR_QUEUE_POLLING_TIME_SECS 0 + #define EXPR_QUEUE_POLLING_TIME_NS 5000 +@@ -177,17 +177,9 @@ static void exitf(const char* message) + exit(1); + } + +-#if Z3_VERSION <= 451 +-static void smt_error_handler(Z3_context c, Z3_error_code e) +-#else + static void smt_error_handler(Z3_context c, Z3_error_code e) +-#endif + { +-#if Z3_VERSION <= 451 +- printf("Error code: %s\n", Z3_get_error_msg(e)); +-#else + printf("Error code: %s\n", Z3_get_error_msg(smt_solver.ctx, e)); +-#endif + ABORT(); + exitf("incorrect use of Z3"); + } +@@ -834,12 +826,12 @@ static void smt_dump_solution(Z3_context ctx, Z3_model m, size_t idx, + if (input_slice) { + // SAYF("input slice %ld\n", i); + Z3_ast solution; +- Z3_bool successfulEval = Z3_model_eval(ctx, m, input_slice, +- Z3_FALSE, // model_completion ++ bool successfulEval = Z3_model_eval(ctx, m, input_slice, ++ false, // model_completion + &solution); + assert(successfulEval && "Failed to evaluate model"); + if (Z3_get_ast_kind(ctx, solution) == Z3_NUMERAL_AST) { +- Z3_bool successGet = ++ bool successGet = + Z3_get_numeral_int(ctx, solution, &solution_byte); + if (successGet) { // && solution_byte + // printf("Solution[%ld]: 0x%x\n", i, solution_byte); +@@ -997,7 +989,7 @@ static void inline smt_dump_debug_query(Z3_solver solver, Z3_ast expr, uint64_t + Z3_model model = Z3_solver_get_model(smt_solver.ctx, solver); + Z3_model_inc_ref(smt_solver.ctx, model); + Z3_ast solution = NULL; +- Z3_model_eval(smt_solver.ctx, model, expr, Z3_TRUE, &solution); ++ Z3_model_eval(smt_solver.ctx, model, expr, true, &solution); + uint64_t value = 0; + if (is_bool) { + Z3_lbool res = Z3_get_bool_value(smt_solver.ctx, solution); +@@ -1028,9 +1020,10 @@ static void inline smt_dump_debug_query(Z3_solver solver, Z3_ast expr, uint64_t + if (input_slice) { + // SAYF("input slice %ld\n", i); + Z3_ast solution; +- Z3_bool successfulEval = Z3_model_eval(smt_solver.ctx, model, input_slice, +- Z3_FALSE, // model_completion +- &solution); ++ bool successfulEval = Z3_model_eval(smt_solver.ctx, ++ model, input_slice, ++ /*model_completion=*/false, ++ &solution); + assert(successfulEval && "Failed to evaluate model"); + if (Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_NUMERAL_AST) { + Z3_get_numeral_int(smt_solver.ctx, solution, &solution_byte); +@@ -1113,18 +1106,12 @@ static uintptr_t smt_query_eval_uint64(Z3_model m, Z3_ast e) + { + uintptr_t value; + Z3_ast solution; +- Z3_bool successfulEval = +- Z3_model_eval(smt_solver.ctx, m, e, Z3_TRUE, &solution); ++ bool successfulEval = ++ Z3_model_eval(smt_solver.ctx, m, e, true, &solution); + assert(successfulEval && "Failed to evaluate model"); + if (Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_NUMERAL_AST) { +- +-#if Z3_VERSION <= 451 +- Z3_bool successGet = Z3_get_numeral_int64(smt_solver.ctx, solution, +- (long long int*)&value); +-#else +- Z3_bool successGet = ++ bool successGet = + Z3_get_numeral_int64(smt_solver.ctx, solution, (int64_t*)&value); +-#endif + return value; + } else { + ABORT("Failed to evaluate using Z3 model.\n"); +@@ -1204,12 +1191,8 @@ static void print_z3_ast_internal(Z3_ast e, uint8_t invert_op, + Z3_sort sort = Z3_get_sort(ctx, e); + size_t size = Z3_get_bv_sort_size(ctx, sort); + uint64_t value; +- Z3_bool r = Z3_get_numeral_uint64(ctx, e, +-#if Z3_VERSION <= 451 +- (long long unsigned int*) +-#endif +- &value); +- if (r == Z3_TRUE) { ++ bool r = Z3_get_numeral_uint64(ctx, e, &value); ++ if (r) { + printf("%lx#%lu", value, size); + } else { + const char* z3_query_str = Z3_ast_to_string(smt_solver.ctx, e); +@@ -1557,12 +1540,8 @@ static inline uint8_t is_zero_const(Z3_ast e) + + if (kind == Z3_NUMERAL_AST) { + uint64_t value; +- Z3_bool r = Z3_get_numeral_uint64(ctx, e, +-#if Z3_VERSION <= 451 +- (long long unsigned int*) +-#endif +- &value); +- if (r == Z3_FALSE) { ++ bool r = Z3_get_numeral_uint64(ctx, e, &value); ++ if (!r) { + // result does not fit into 64 bits + return 0; + } +@@ -1578,12 +1557,8 @@ static inline uint8_t is_const(Z3_ast e, uint64_t* value) + Z3_ast_kind kind = Z3_get_ast_kind(ctx, e); + + if (kind == Z3_NUMERAL_AST) { +- Z3_bool r = Z3_get_numeral_uint64(ctx, e, +-#if Z3_VERSION <= 451 +- (long long unsigned int*) +-#endif +- value); +- if (r == Z3_FALSE) { ++ bool r = Z3_get_numeral_uint64(ctx, e, value); ++ if (!r) { + // result does not fit into 64 bits + return 0; + } +@@ -5518,8 +5493,8 @@ static int get_eval_uint64(Z3_model m, Z3_ast e, uintptr_t* value) + { + Z3_ast solution; + +- Z3_bool successfulEval = +- Z3_model_eval(smt_solver.ctx, m, e, Z3_FALSE, &solution); ++ bool successfulEval = ++ Z3_model_eval(smt_solver.ctx, m, e, false, &solution); + assert(successfulEval && "Failed to evaluate model"); + + if (Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_NUMERAL_AST) { +diff --git a/solver/solver.h b/solver/solver.h +index 3efb1ebcb163..bea15d608bf7 100644 +--- a/solver/solver.h ++++ b/solver/solver.h +@@ -6,13 +6,11 @@ + + #include <gmodule.h> + +-#include <z3.h> +-#define Z3_VERSION 487 +- + #define USE_COLOR + #include "debug.h" + +-#include "../tracer/tcg/symbolic/symbolic-struct.h" ++#include <qemu/tcg/symbolic/symbolic-struct.h> ++#include <z3.h> + + typedef enum ExprAnnotationType { + COSTANT_AND, diff --git a/patches/fuzzolic-test-fix-runner.patch b/patches/fuzzolic-test-fix-runner.patch new file mode 100644 index 0000000..7610eca --- /dev/null +++ b/patches/fuzzolic-test-fix-runner.patch @@ -0,0 +1,326 @@ +commit c9d5d6f3872991e7f5cffc8146d3abe121883d61 +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-05-08 11:13:10 +0900 + + Use temporary directories for tests + +diff --git a/tests/run.py b/tests/run.py +index 2144d96c7544..0b69d990faf5 100755 +--- a/tests/run.py ++++ b/tests/run.py +@@ -9,14 +9,13 @@ import time + import pytest + + SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__)) +-WORKDIR = SCRIPT_DIR + "/workdir" + + + def pytest_addoption(parser): + parser.addoption("--fuzzy", action="store_true", default="run tests using Fuzzy-SAT") + + +-def run(test, ++def run(test, workdir, + use_duplicate_testcase_checker=False, + expected_inputs=1, + perf_run=False, +@@ -25,8 +24,7 @@ def run(test, + use_fuzzy=False, + use_memory_slice=False, + use_address_reasoning=False): +- +- initial_input = "%s/%s_0.dat" % (SCRIPT_DIR, test) ++ initial_input = os.path.join(SCRIPT_DIR, f"{test}_0.dat") + assert os.path.exists(initial_input) + + env = os.environ.copy() +@@ -36,14 +34,10 @@ def run(test, + native_time = None + if perf_run: + start = time.time() +- p = subprocess.Popen( +- [ +- SCRIPT_DIR + "/driver", test +- ], +- stderr=subprocess.DEVNULL, +- stdin=subprocess.PIPE, +- env=env +- ) ++ p = subprocess.Popen((os.path.join(SCRIPT_DIR, "driver"), test), ++ stderr=subprocess.DEVNULL, ++ stdin=subprocess.PIPE, ++ env=env) + with open(initial_input, "rb") as f: + p.stdin.write(f.read()) + p.stdin.close() +@@ -51,27 +45,18 @@ def run(test, + end = time.time() + native_time = end - start + ++ (workdir/'.fuzzolic_workdir').mkdir() ++ command = ['fuzzolic', '-o', workdir, '-i', initial_input, '-k'] ++ if perf_run: command.extend(('-d', 'out')) ++ if use_lib_models: command.append('-l') ++ if use_fuzzy: command.append('-f') ++ if use_memory_slice: command.append('-s') ++ if use_address_reasoning: command.append('-r') ++ command.extend((os.path.join(SCRIPT_DIR, "driver"), test)) ++ print(*command) ++ + start = time.time() +- p = subprocess.Popen( +- [ +- SCRIPT_DIR + "/../fuzzolic/fuzzolic.py", +- "-o", WORKDIR, +- "-i", initial_input, +- "-k", +- ] +- + (['-d', 'out'] if perf_run else []) +- + (['-l'] if use_lib_models else []) +- + (['-f'] if use_fuzzy else []) +- + (['-s'] if use_memory_slice else []) +- + (['-r'] if use_address_reasoning else []) +- + [ +- SCRIPT_DIR + "/driver", test +- ], +- stderr=subprocess.DEVNULL, +- stdin=subprocess.DEVNULL, +- env=env +- ) +- p.wait() ++ subprocess.run(command, env=env) + end = time.time() + emulated_time = end - start + +@@ -80,25 +65,17 @@ def run(test, + print("Slowdown: %s" % round(slowdown, 1)) + assert slowdown < 70 + +- if expected_inputs > 0: +- testcases = glob.glob(WORKDIR + "/tests/test_*.dat") +- assert len(testcases) == expected_inputs +- else: +- testcases = glob.glob(WORKDIR + "/fuzzolic-00000/test_*.dat") ++ testcases = tuple(workdir.glob('**/test_case_*.dat')) ++ assert len(testcases) >= expected_inputs + + match = False +- + if match_output: + for f in testcases: +- p = subprocess.Popen( +- [ +- SCRIPT_DIR + "/driver", test +- ], +- stderr=subprocess.DEVNULL, +- stdin=subprocess.PIPE, +- stdout=subprocess.PIPE, +- env=env +- ) ++ p = subprocess.Popen([os.path.join(SCRIPT_DIR, "driver"), test], ++ stderr=subprocess.DEVNULL, ++ stdin=subprocess.PIPE, ++ stdout=subprocess.PIPE, ++ env=env) + with open(f, "rb") as fp: + p.stdin.write(fp.read()) + stdout = p.communicate()[0].decode("utf-8") +@@ -114,125 +91,142 @@ def run(test, + assert match + + +-def test_simple_if(fuzzy): +- run("simple_if", use_fuzzy=fuzzy) ++def test_simple_if(tmp_path, fuzzy): ++ run("simple_if", tmp_path, use_fuzzy=fuzzy) + + +-def test_nested_if(fuzzy): +- run("nested_if", expected_inputs=4, use_fuzzy=fuzzy) ++def test_nested_if(tmp_path, fuzzy): ++ run("nested_if", tmp_path, expected_inputs=4, use_fuzzy=fuzzy) + + +-def test_mystrcmp(fuzzy): ++def test_mystrcmp(tmp_path, fuzzy): + # FixMe: to generate the correct input, we have to: + # (1) disable bitmap filtering + # (2) start with a seed with enough bytes +- run("mystrcmp", use_duplicate_testcase_checker=True, expected_inputs=8, use_fuzzy=fuzzy) ++ run("mystrcmp", tmp_path, use_duplicate_testcase_checker=True, ++ expected_inputs=8, use_fuzzy=fuzzy) + + +-def test_all_concrete(fuzzy): ++def test_all_concrete(tmp_path, fuzzy): + # performance test +- run("all_concrete", use_duplicate_testcase_checker=False, expected_inputs=1, perf_run=True, use_fuzzy=fuzzy) ++ run("all_concrete", tmp_path, perf_run=True, ++ use_duplicate_testcase_checker=False, use_fuzzy=fuzzy) + + +-def test_div3(fuzzy): ++def test_div3(tmp_path, fuzzy): + if fuzzy: + pytest.skip("Fuzzy-SAT cannot deterministically solve this") +- run("div3", expected_inputs=1) ++ run("div3", tmp_path) + + +-def test_addq(fuzzy): +- run("addq", expected_inputs=1, match_output=True, use_fuzzy=fuzzy) ++def test_addq(tmp_path, fuzzy): ++ run("addq", tmp_path, match_output=True, use_fuzzy=fuzzy) + + +-def test_addl(fuzzy): +- run("addl", expected_inputs=1, match_output=True, use_fuzzy=fuzzy) ++def test_addl(tmp_path, fuzzy): ++ run("addl", tmp_path, match_output=True, use_fuzzy=fuzzy) + + +-def test_addw(fuzzy): +- run("addw", expected_inputs=1, match_output=True, use_fuzzy=fuzzy) ++def test_addw(tmp_path, fuzzy): ++ run("addw", tmp_path, match_output=True, use_fuzzy=fuzzy) + + +-def test_addb(fuzzy): +- run("addb", expected_inputs=1, match_output=True, use_fuzzy=fuzzy) ++def test_addb(tmp_path, fuzzy): ++ run("addb", tmp_path, match_output=True, use_fuzzy=fuzzy) + + +-def test_adcq(fuzzy): +- run("adcq", expected_inputs=1, match_output=True, use_fuzzy=fuzzy) ++def test_adcq(tmp_path, fuzzy): ++ run("adcq", tmp_path, match_output=True, use_fuzzy=fuzzy) + + +-def test_adcl(fuzzy): +- run("adcl", expected_inputs=1, match_output=True, use_fuzzy=fuzzy) ++def test_adcl(tmp_path, fuzzy): ++ run("adcl", tmp_path, match_output=True, use_fuzzy=fuzzy) + + +-def test_adcw(fuzzy): +- run("adcw", expected_inputs=1, match_output=True, use_fuzzy=fuzzy) ++def test_adcw(tmp_path, fuzzy): ++ run("adcw", tmp_path, match_output=True, use_fuzzy=fuzzy) + + +-def test_adcb(fuzzy): +- run("adcb", expected_inputs=1, match_output=True, use_fuzzy=fuzzy) ++def test_adcb(tmp_path, fuzzy): ++ run("adcb", tmp_path, match_output=True, use_fuzzy=fuzzy) + + +-def test_model_strcmp(fuzzy): +- run("model_strcmp", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++def test_model_strcmp(tmp_path, fuzzy): ++ run("model_strcmp", tmp_path, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_model_strncmp(fuzzy): +- run("model_strncmp", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++def test_model_strncmp(tmp_path, fuzzy): ++ run("model_strncmp", tmp_path, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_model_strlen(fuzzy): +- run("model_strlen", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++def test_model_strlen(tmp_path, fuzzy): ++ run("model_strlen", tmp_path, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_model_strnlen_v0(fuzzy): +- run("model_strnlen_v0", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++def test_model_strnlen_v0(tmp_path, fuzzy): ++ run("model_strnlen_v0", tmp_path, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_model_strnlen_v1(fuzzy): +- run("model_strnlen_v1", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++def test_model_strnlen_v1(tmp_path, fuzzy): ++ run("model_strnlen_v1", tmp_path, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_model_memcmp_v0(fuzzy): +- run("model_memcmp_v0", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++def test_model_memcmp_v0(tmp_path, fuzzy): ++ run("model_memcmp_v0", tmp_path, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_model_memcmp_v1(fuzzy): +- run("model_memcmp_v1", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++def test_model_memcmp_v1(tmp_path, fuzzy): ++ run("model_memcmp_v1", tmp_path, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_model_memchr(fuzzy): +- run("model_memchr", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++def test_model_memchr(tmp_path, fuzzy): ++ run("model_memchr", tmp_path, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_symbolic_index(fuzzy): ++def test_symbolic_index(tmp_path, fuzzy): + pytest.skip("This test requires to build the tracer with memory slice support") +- run("symbolic_index", expected_inputs=1, use_fuzzy=fuzzy, use_memory_slice=True) ++ run("symbolic_index", tmp_path, use_fuzzy=fuzzy, ++ use_memory_slice=True) + + +-def test_symbolic_read(fuzzy): +- run("symbolic_read", expected_inputs=2, match_output=True, use_fuzzy=fuzzy, use_memory_slice=True) ++def test_symbolic_read(tmp_path, fuzzy): ++ run("symbolic_read", tmp_path, expected_inputs=2, match_output=True, ++ use_fuzzy=fuzzy, use_memory_slice=True) + + +-def test_switch(fuzzy): ++def test_switch(tmp_path, fuzzy): + pytest.skip("This test requires to build the tracer with memory slice support") +- run("switch", expected_inputs=7, match_output=True, use_fuzzy=fuzzy, use_address_reasoning=True) ++ run("switch", tmp_path, expected_inputs=7, match_output=True, ++ use_fuzzy=fuzzy, use_address_reasoning=True) + + +-def test_model_malloc_min(fuzzy): ++def test_model_malloc_min(tmp_path, fuzzy): + pytest.skip("We need to revise this test") +- run("model_malloc_min", expected_inputs=0, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++ run("model_malloc_min", tmp_path, expected_inputs=0, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_model_malloc_max(fuzzy): ++def test_model_malloc_max(tmp_path, fuzzy): + pytest.skip("We need to revise this test") +- run("model_malloc_max", expected_inputs=0, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++ run("model_malloc_max", tmp_path, expected_inputs=0, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_model_realloc_min(fuzzy): ++def test_model_realloc_min(tmp_path, fuzzy): + pytest.skip("We need to revise this test") +- run("model_realloc_min", expected_inputs=0, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++ run("model_realloc_min", tmp_path, expected_inputs=0, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) + + +-def test_model_realloc_max(fuzzy): ++def test_model_realloc_max(tmp_path, fuzzy): + pytest.skip("We need to revise this test") +- run("model_realloc_max", expected_inputs=0, match_output=True, use_lib_models=True, use_fuzzy=fuzzy) ++ run("model_realloc_max", tmp_path, expected_inputs=0, match_output=True, ++ use_lib_models=True, use_fuzzy=fuzzy) diff --git a/patches/fuzzolic-test-skip-nondeterministic.patch b/patches/fuzzolic-test-skip-nondeterministic.patch new file mode 100644 index 0000000..2d390db --- /dev/null +++ b/patches/fuzzolic-test-skip-nondeterministic.patch @@ -0,0 +1,23 @@ +commit 8350c6e96aba15b548ecd423b99b88da35310645 +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-05-08 11:23:51 +0900 + + Skip nondeterministic test + + Test div3 probably used to depend on an implementation detail of Z3 + that is no longer present. + +diff --git a/tests/run.py b/tests/run.py +index 0b69d990faf5..7db888dfa973 100755 +--- a/tests/run.py ++++ b/tests/run.py +@@ -114,8 +114,7 @@ def test_all_concrete(tmp_path, fuzzy): + + + def test_div3(tmp_path, fuzzy): +- if fuzzy: +- pytest.skip("Fuzzy-SAT cannot deterministically solve this") ++ pytest.skip("Not deterministic") + run("div3", tmp_path) + + diff --git a/patches/fuzzolic-timeout-solver.patch b/patches/fuzzolic-timeout-solver.patch new file mode 100644 index 0000000..95b971b --- /dev/null +++ b/patches/fuzzolic-timeout-solver.patch @@ -0,0 +1,22 @@ +From f06525aaf9790b0eecef317e4aaf444189e6042b Mon Sep 17 00:00:00 2001 +From: Andrew Haberlandt <ahaberla@andrew.cmu.edu> +Date: Sun, 19 May 2024 06:46:05 +0000 +Subject: [PATCH] fix: executor fails to kill solver if it hangs + +--- + fuzzolic/executor.py | 2 +- + 1 file changed, 1 insertion(+), 1 deletion(-) + +diff --git a/fuzzolic/executor.py b/fuzzolic/executor.py +index 39c6aa6..e660314 100644 +--- a/fuzzolic/executor.py ++++ b/fuzzolic/executor.py +@@ -449,7 +449,7 @@ def fuzz_one(self, testcase, target, force_smt=False): + print('[FUZZOLIC] Solver is taking too long. Let us stop it.') + p_solver.send_signal(signal.SIGUSR2) + try: +- p_solver.wait(SOLVER_TIMEOUT) ++ p_solver.wait(SOLVER_TIMEOUT / 1000) + except subprocess.TimeoutExpired: + print('[FUZZOLIC] Solver will be killed.') + p_solver.send_signal(signal.SIGKILL) diff --git a/patches/fuzzolic-unbundle.patch b/patches/fuzzolic-unbundle.patch new file mode 100644 index 0000000..803f621 --- /dev/null +++ b/patches/fuzzolic-unbundle.patch @@ -0,0 +1,108 @@ +commit 24044a2d0341cfdd3c7cc7320cbbd49591ef28ce +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-04-29 16:44:20 +0900 + + Unbundle required utilities + +diff --git a/fuzzolic/executor.py b/fuzzolic/executor.py +index f2639eb8da6a..06d0253a3b07 100644 +--- a/fuzzolic/executor.py ++++ b/fuzzolic/executor.py +@@ -21,14 +21,9 @@ from . import minimizer_qsym + from . import minimizer + + SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__)) +-SOLVER_SMT_BIN = SCRIPT_DIR + '/../solver/solver-smt' +-SOLVER_FUZZY_BIN = SCRIPT_DIR + '/../solver/solver-fuzzy' +-TRACER_BIN = SCRIPT_DIR + '/../tracer/x86_64-linux-user/qemu-x86_64' +- +-if 'AFL_PATH' not in os.environ: +- AFL_PATH = SCRIPT_DIR + '/../../AFLplusplus/' +-else: +- AFL_PATH = os.environ['AFL_PATH'] ++SOLVER_SMT_BIN = 'solver-smt' ++SOLVER_FUZZY_BIN = 'solver-fuzzy' ++TRACER_BIN = 'qemu-x86_64' + + SOLVER_WAIT_TIME_AT_STARTUP = 0.0010 + SOLVER_TIMEOUT = 1000 +@@ -84,15 +79,12 @@ class Executor(object): + sys.exit('ERROR: invalid AFL workdir') + self.afl = os.path.abspath(afl) + self.minimizer = minimizer_qsym.TestcaseMinimizer( +- [binary] + binary_args, AFL_PATH, output_dir, True, input_fixed_name) ++ [binary] + binary_args, output_dir, True, input_fixed_name) + # self.minimizer = minimizer.TestcaseMinimizer([binary] + binary_args, self.global_bitmap) + else: + self.afl = None +- if minimizer_qsym.is_afl_showmap_available(): +- self.minimizer = minimizer_qsym.TestcaseMinimizer( +- [binary] + binary_args, AFL_PATH, output_dir, True, input_fixed_name) +- else: +- self.minimizer = minimizer.TestcaseMinimizer([binary] + binary_args, self.global_bitmap) ++ self.minimizer = minimizer_qsym.TestcaseMinimizer( ++ [binary] + binary_args, output_dir, True, input_fixed_name) + + self.afl_processed_testcases = set() + self.afl_alt_processed_testcases = set() +@@ -126,16 +118,8 @@ class Executor(object): + + if use_symbolic_models: + plt_info_file = self.__get_root_dir() + "/plt_info.txt" +- p = subprocess.Popen( +- [ +- SCRIPT_DIR + "/find_models_addrs.py", +- "-o", plt_info_file, +- binary +- ], +- # stderr=subprocess.DEVNULL, +- # stdin=subprocess.DEVNULL, +- ) +- p.wait() ++ subprocess.run(["fuzzolic-find-models-addrs", ++ "-o", plt_info_file, binary]) + self.plt_info = plt_info_file + else: + self.plt_info = None +diff --git a/fuzzolic/minimizer_qsym.py b/fuzzolic/minimizer_qsym.py +index 6d0170577392..1c31df0b9f0a 100644 +--- a/fuzzolic/minimizer_qsym.py ++++ b/fuzzolic/minimizer_qsym.py +@@ -81,15 +81,13 @@ def fix_at_file(cmd, testcase): + + return cmd, stdin + +-def is_afl_showmap_available(): +- return os.path.exists(os.path.join(SCRIPT_DIR, "../utils/afl-showmap")) + + class TestcaseMinimizer(object): +- def __init__(self, cmd, afl_path, out_dir, qemu_mode, fixed_name, map_size=MAP_SIZE): ++ def __init__(self, cmd, out_dir, qemu_mode, fixed_name, map_size=MAP_SIZE): + self.cmd = cmd + self.qemu_mode = qemu_mode +- self.showmap = os.path.join(afl_path, "afl-showmap") +- self.showmap_fork = os.path.join(SCRIPT_DIR, "../utils/afl-showmap") ++ self.showmap = "afl-showmap" ++ self.showmap_fork = "fuzzolic-showmap" + self.bitmap_file = os.path.join(out_dir, "afl-bitmap") + self.crash_bitmap_file = os.path.join(out_dir, "afl-crash-bitmap") + _, self.temp_file = tempfile.mkstemp(dir=out_dir) +@@ -225,16 +223,8 @@ class TestcaseMinimizer(object): + return interesting + + def is_interesting_testcase_fork(self, bitmap, my_bitmap_file=None): +- if my_bitmap_file is None: +- my_bitmap_file = self.bitmap_file +- +- cmd = [ +- SCRIPT_DIR + '/../utils/merge_bitmap', +- bitmap, +- my_bitmap_file +- ] +- # print(cmd) +- ++ cmd = ('fuzzolic-merge-bitmap', bitmap, ++ my_bitmap_file or self.bitmap_file) + with open(os.devnull, "wb") as devnull: + proc = sp.Popen(cmd, stdin=None, stdout=devnull, stderr=devnull) + proc.wait() diff --git a/patches/fuzzolic-utils-make.patch b/patches/fuzzolic-utils-make.patch new file mode 100644 index 0000000..4a971a5 --- /dev/null +++ b/patches/fuzzolic-utils-make.patch @@ -0,0 +1,34 @@ +commit 1bfb2b78e56f953956f2125980992b91ad355774 +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-05-08 11:01:05 +0900 + + Build and install utilities + +diff --git a/Makefile b/Makefile +index 395f7a387bd9..feaef92f3266 100644 +--- a/Makefile ++++ b/Makefile +@@ -1,3 +1,23 @@ ++.POSIX: ++.PHONY: all install ++ ++PREFIX ?= /usr/local ++BINDIR ::= $(DESTDIR)$(PREFIX)/bin ++BIN ::= fuzzolic-merge-bitmap fuzzolic-find-models-addrs ++ ++all: $(BIN) ++ ++fuzzolic-find-models-addrs: fuzzolic/find_models_addrs.py ++ cp $< $@ ++ ++fuzzolic-merge-bitmap: utils/merge_bitmap.o ++ $(CC) $(LDFLAGS) $< $(LOADLIBES) $(LDLIBS) -o $@ ++ ++install: $(BIN:%=$(BINDIR)/%) ++ ++$(BINDIR)/%: % ++ install -Dm 755 $< $@ ++ + simpleif: build clean-work-dir + ./fuzzolic/fuzzolic.py -o workdir -i tests/simple_if_0.dat tests/driver simple_if + ./utils/print_test_cases.py workdir/tests diff --git a/patches/fuzzy-sat-install.patch b/patches/fuzzy-sat-install.patch new file mode 100644 index 0000000..2c68cbc --- /dev/null +++ b/patches/fuzzy-sat-install.patch @@ -0,0 +1,65 @@ +commit 3a8ce277d2f26409a1eb139641f0733979bd21ab +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-04-24 13:10:50 +0900 + + Install libraries and tools + +diff --git a/CMakeLists.txt b/CMakeLists.txt +index 7cfa95cc7174..695bc8757fa5 100644 +--- a/CMakeLists.txt ++++ b/CMakeLists.txt +@@ -1,5 +1,5 @@ + cmake_minimum_required(VERSION 3.7) +- ++include(CMakePackageConfigHelpers) + set(CMAKE_POLICY_DEFAULT_CMP0077 NEW) + + project(Z3Fuzzy) +@@ -7,3 +7,10 @@ project(Z3Fuzzy) + set(Z3_BUILD_PYTHON_BINDINGS true) + add_subdirectory(lib) + add_subdirectory(tools) ++ ++install(EXPORT Z3Fuzzy DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/Z3Fuzzy) ++configure_package_config_file(${CMAKE_CURRENT_SOURCE_DIR}/Config.cmake.in ++ "${CMAKE_CURRENT_BINARY_DIR}/Z3FuzzyConfig.cmake" ++ INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/Z3Fuzzy) ++install(FILES "${CMAKE_CURRENT_BINARY_DIR}/Z3FuzzyConfig.cmake" ++ DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/Z3Fuzzy) +diff --git a/Config.cmake.in b/Config.cmake.in +new file mode 100644 +index 000000000000..64b0eaa487fb +--- /dev/null ++++ b/Config.cmake.in +@@ -0,0 +1,3 @@ ++@PACKAGE_INIT@ ++include("${CMAKE_CURRENT_LIST_DIR}/Z3Fuzzy.cmake") ++check_required_components(Z3Fuzzy) +diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt +index 558c01b7c725..c30f0f41206a 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 EXPORT Z3Fuzzy) +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; diff --git a/patches/qemu-for-fuzzolic-static-global.patch b/patches/qemu-for-fuzzolic-static-global.patch new file mode 100644 index 0000000..0cb52af --- /dev/null +++ b/patches/qemu-for-fuzzolic-static-global.patch @@ -0,0 +1,24 @@ +commit a0646eac1b56e4df51e7c6d2e99cb8807c59a1a3 +Author: Nguyễn Gia Phong <cnx@loang.net> +Date: 2025-04-30 12:10:05 +0900 + + Avoid global variable in header + + Such global would be defined in each compilation unit including the header, + preventing them from being linked together. + +diff --git a/tcg/symbolic/symbolic-struct.h b/tcg/symbolic/symbolic-struct.h +index 350522935bf9..684d32acfebd 100644 +--- a/tcg/symbolic/symbolic-struct.h ++++ b/tcg/symbolic/symbolic-struct.h +@@ -503,9 +503,9 @@ static inline size_t get_opkind_width(OPKIND opkind) + } + + #define MAX_PRINT_CHECK (1024 * 1024) +-uint8_t printed[MAX_PRINT_CHECK]; + static inline void print_expr_internal(Expr* expr, uint8_t reset) + { ++ static uint8_t printed[MAX_PRINT_CHECK]; + if (reset) + for (size_t i = 0; i < MAX_PRINT_CHECK; i++) + printed[i] = 0; diff --git a/patches/qemu-for-fuzzolic-test-opts-range-beyond.patch b/patches/qemu-for-fuzzolic-test-opts-range-beyond.patch new file mode 100644 index 0000000..9c7a4e0 --- /dev/null +++ b/patches/qemu-for-fuzzolic-test-opts-range-beyond.patch @@ -0,0 +1,97 @@ +commit 863f195fa823c0c20d734dadfc5908c2aea34330 +Author: Andrey Shinkevich <andrey.shinkevich@virtuozzo.com> +Date: 2019-08-05 20:03:06 +0300 + + make check-unit: use after free in test-opts-visitor + + In the struct OptsVisitor, the 'repeated_opts' member points to a list + in the 'unprocessed_opts' hash table after the list has been destroyed. + A subsequent call to visit_type_int() references the deleted list. + It results in use-after-free issue reproduced by running the test case + under the Valgrind: valgrind tests/test-opts-visitor. + A new mode ListMode::LM_TRAVERSED is declared to mark the list + traversal completed. + + Suggested-by: Markus Armbruster <armbru@redhat.com> + Signed-off-by: Andrey Shinkevich <andrey.shinkevich@virtuozzo.com> + Message-Id: <1565024586-387112-1-git-send-email-andrey.shinkevich@virtuozzo.com> + +diff --git a/qapi/opts-visitor.c b/qapi/opts-visitor.c +index 324b197495a0..5fe0276c1cc8 100644 +--- a/qapi/opts-visitor.c ++++ b/qapi/opts-visitor.c +@@ -24,7 +24,8 @@ enum ListMode + { + LM_NONE, /* not traversing a list of repeated options */ + +- LM_IN_PROGRESS, /* opts_next_list() ready to be called. ++ LM_IN_PROGRESS, /* ++ * opts_next_list() ready to be called. + * + * Generating the next list link will consume the most + * recently parsed QemuOpt instance of the repeated +@@ -36,7 +37,8 @@ enum ListMode + * LM_UNSIGNED_INTERVAL. + */ + +- LM_SIGNED_INTERVAL, /* opts_next_list() has been called. ++ LM_SIGNED_INTERVAL, /* ++ * opts_next_list() has been called. + * + * Generating the next list link will consume the most + * recently stored element from the signed interval, +@@ -48,7 +50,14 @@ enum ListMode + * next element of the signed interval. + */ + +- LM_UNSIGNED_INTERVAL /* Same as above, only for an unsigned interval. */ ++ LM_UNSIGNED_INTERVAL, /* Same as above, only for an unsigned interval. */ ++ ++ LM_TRAVERSED /* ++ * opts_next_list() has been called. ++ * ++ * No more QemuOpt instance in the list. ++ * The traversal has been completed. ++ */ + }; + + typedef enum ListMode ListMode; +@@ -238,6 +247,8 @@ opts_next_list(Visitor *v, GenericList *tail, size_t size) + OptsVisitor *ov = to_ov(v); + + switch (ov->list_mode) { ++ case LM_TRAVERSED: ++ return NULL; + case LM_SIGNED_INTERVAL: + case LM_UNSIGNED_INTERVAL: + if (ov->list_mode == LM_SIGNED_INTERVAL) { +@@ -258,6 +269,8 @@ opts_next_list(Visitor *v, GenericList *tail, size_t size) + opt = g_queue_pop_head(ov->repeated_opts); + if (g_queue_is_empty(ov->repeated_opts)) { + g_hash_table_remove(ov->unprocessed_opts, opt->name); ++ ov->repeated_opts = NULL; ++ ov->list_mode = LM_TRAVERSED; + return NULL; + } + break; +@@ -289,7 +302,8 @@ opts_end_list(Visitor *v, void **obj) + + assert(ov->list_mode == LM_IN_PROGRESS || + ov->list_mode == LM_SIGNED_INTERVAL || +- ov->list_mode == LM_UNSIGNED_INTERVAL); ++ ov->list_mode == LM_UNSIGNED_INTERVAL || ++ ov->list_mode == LM_TRAVERSED); + ov->repeated_opts = NULL; + ov->list_mode = LM_NONE; + } +@@ -306,6 +320,10 @@ lookup_scalar(const OptsVisitor *ov, const char *name, Error **errp) + list = lookup_distinct(ov, name, errp); + return list ? g_queue_peek_tail(list) : NULL; + } ++ if (ov->list_mode == LM_TRAVERSED) { ++ error_setg(errp, "Fewer list elements than expected"); ++ return NULL; ++ } + assert(ov->list_mode == LM_IN_PROGRESS); + return g_queue_peek_head(ov->repeated_opts); + } |