diff options
Diffstat (limited to 'patches')
| -rw-r--r-- | patches/afl++-keep-all-crashes.patch | 17 | ||||
| -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 | 123 | ||||
| -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/jasper-lint.patch | 592 | ||||
| -rw-r--r-- | patches/jasper-no-define-int-types.patch | 19 | ||||
| -rw-r--r-- | patches/jasper-sanitized-bmp.patch | 117 | ||||
| -rw-r--r-- | patches/qemu-for-fuzzolic-static-global.patch | 24 | ||||
| -rw-r--r-- | patches/qemu-for-fuzzolic-test-opts-range-beyond.patch | 97 |
19 files changed, 2528 insertions, 9 deletions
diff --git a/patches/afl++-keep-all-crashes.patch b/patches/afl++-keep-all-crashes.patch index e3ce8f6..2b1f57d 100644 --- a/patches/afl++-keep-all-crashes.patch +++ b/patches/afl++-keep-all-crashes.patch @@ -1,16 +1,16 @@ diff --git a/src/afl-fuzz-bitmap.c b/src/afl-fuzz-bitmap.c -index f05bb7db59d5..de275e374ff1 100644 +index 19cdf511149f..dd7cb510b62c 100644 --- a/src/afl-fuzz-bitmap.c +++ b/src/afl-fuzz-bitmap.c -@@ -556,7 +556,6 @@ save_if_interesting(afl_state_t *afl, void *mem, u32 len, u8 fault, u8 inc) { - if (likely(!new_bits && !new_paths)) { +@@ -639,7 +639,6 @@ u8 __attribute__((hot)) save_if_interesting(afl_state_t *afl, void *mem, + if (san_fault == FSRV_RUN_OK) { - if (unlikely(afl->crash_mode)) { ++afl->total_crashes; } -- return 0; + if (unlikely(afl->crash_mode)) { ++afl->total_crashes; } +- return 0; - } + } else { -@@ -837,16 +836,12 @@ save_if_interesting(afl_state_t *afl, void *mem, u32 len, u8 fault, u8 inc) { +@@ -934,8 +933,6 @@ may_save_fault: ++afl->total_crashes; @@ -18,7 +18,8 @@ index f05bb7db59d5..de275e374ff1 100644 - if (likely(!afl->non_instrumented_mode)) { - if (!classified) { classify_counts(&afl->fsrv); } + if (unlikely(!classified)) { +@@ -947,8 +944,6 @@ may_save_fault: simplify_trace(afl, afl->fsrv.trace_bits); 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..d545551 --- /dev/null +++ b/patches/fuzzolic-unbundle.patch @@ -0,0 +1,123 @@ +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/fuzzolic/run_afl_fuzzolic.py b/fuzzolic/run_afl_fuzzolic.py +index 9289cd191437..78c0e256d91f 100755 +--- a/fuzzolic/run_afl_fuzzolic.py ++++ b/fuzzolic/run_afl_fuzzolic.py +@@ -18,8 +18,8 @@ if 'AFL_PATH' not in os.environ: + else: + AFL_PATH = os.environ['AFL_PATH'] + +-AFL_BIN = AFL_PATH + '/afl-fuzz' +-FUZZOLIC_BIN = SCRIPT_DIR + '/fuzzolic.py' ++AFL_BIN = 'afl-fuzz' ++FUZZOLIC_BIN = 'fuzzolic' + DEVNULL = open(os.devnull, 'w') + WAITING_TIME_AFTER_AFL_INSTANCE_START = 30 + 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/jasper-lint.patch b/patches/jasper-lint.patch new file mode 100644 index 0000000..89bc2f9 --- /dev/null +++ b/patches/jasper-lint.patch @@ -0,0 +1,592 @@ +commit d743f7e0ad901dc3419fc1042939a5454de96c16 +Author: Michael Adams <mdadams@ece.uvic.ca> +Date: 2016-10-21 03:14:31 -0700 + + Changed the configure setup so that if GCC is used warnings and pedantic + errors are enabled. + + Fixed some inconsistent use of quotes and angle brackets in include directives. + + Added experimental support in the jas_image code for images with signed + sample values. This code has not been tested yet, except to ensure + it does not crash. + + Fixed a bug in the stream code (jas_stream) that caused memory to leak + when an attempt to open a file failed. + + Commented out an assertion that causes a C99 pedantic build to fail, due + to string literal that is too long. + + In the JPC QMFB/TSFB code, there were several places in function + declarations/definitions where incorrect parameter types were used + (e.g., int* used instead of jpc_fix_t*). + Also, some function prototypes were missing. + This is now fixed. + + Some files were missing includes for jas_debug.h (resulting in missing + function prototypes). This is now fixed. + + Some bugs in the MIF decoder have been fixed. + Also, some improved debugging support has been added for the MIF decoder. + + Numerous cosmetic changes were also made to the code. + +diff --git a/configure.ac b/configure.ac +index 13751b0e9bef..7f28f3ffb4e7 100644 +--- a/configure.ac ++++ b/configure.ac +@@ -375,10 +375,11 @@ esac + ], [debug=no]) + + if test "$GCC" = yes; then +- CFLAGS="$CFLAGS" +- #CFLAGS="$CFLAGS -std=c99" +- #CFLAGS="$CFLAGS -pedantic" +- #CFLAGS="$CFLAGS -pedantic-errors" ++ #CFLAGS="$CFLAGS" ++ CFLAGS="$CFLAGS -std=c99" ++ CFLAGS="$CFLAGS -pedantic" ++ CFLAGS="$CFLAGS -pedantic-errors" ++ CFLAGS="$CFLAGS -Wall" + #CFLAGS="$CFLAGS -W -Wall -Wno-long-long -Wformat -Wmissing-prototypes -Wstrict-prototypes" + fi + +diff --git a/src/appl/jasper.c b/src/appl/jasper.c +index d99e35668bd9..690002958c26 100644 +--- a/src/appl/jasper.c ++++ b/src/appl/jasper.c +@@ -77,6 +77,7 @@ + #include <time.h> + + #include <jasper/jasper.h> ++#include <jasper/jas_debug.h> + + /******************************************************************************\ + * +diff --git a/src/libjasper/base/jas_cm.c b/src/libjasper/base/jas_cm.c +index 6c612b70f7a7..fc8417fb65ba 100644 +--- a/src/libjasper/base/jas_cm.c ++++ b/src/libjasper/base/jas_cm.c +@@ -65,16 +65,17 @@ + * $Id$ + */ + +-#include <jasper/jas_config.h> + #include <math.h> + #include <stdlib.h> + #include <assert.h> +-#include <jasper/jas_cm.h> +-#include <jasper/jas_icc.h> +-#include <jasper/jas_init.h> +-#include <jasper/jas_stream.h> +-#include <jasper/jas_malloc.h> +-#include <jasper/jas_math.h> ++#include "jasper/jas_config.h" ++#include "jasper/jas_cm.h" ++#include "jasper/jas_icc.h" ++#include "jasper/jas_init.h" ++#include "jasper/jas_stream.h" ++#include "jasper/jas_malloc.h" ++#include "jasper/jas_math.h" ++#include "jasper/jas_debug.h" + + static jas_cmprof_t *jas_cmprof_create(void); + static void jas_cmshapmatlut_cleanup(jas_cmshapmatlut_t *); +diff --git a/src/libjasper/base/jas_getopt.c b/src/libjasper/base/jas_getopt.c +index 2a3dfe50addf..9c9724aebe6d 100644 +--- a/src/libjasper/base/jas_getopt.c ++++ b/src/libjasper/base/jas_getopt.c +@@ -76,6 +76,7 @@ + + #include "jasper/jas_getopt.h" + #include "jasper/jas_math.h" ++#include "jasper/jas_debug.h" + + /******************************************************************************\ + * Global data. +diff --git a/src/libjasper/base/jas_icc.c b/src/libjasper/base/jas_icc.c +index 6569bd9dd524..4abee31b9602 100644 +--- a/src/libjasper/base/jas_icc.c ++++ b/src/libjasper/base/jas_icc.c +@@ -60,14 +60,15 @@ + */ + + #include <assert.h> +-#include <jasper/jas_config.h> +-#include <jasper/jas_types.h> +-#include <jasper/jas_malloc.h> +-#include <jasper/jas_debug.h> +-#include <jasper/jas_icc.h> +-#include <jasper/jas_cm.h> +-#include <jasper/jas_stream.h> +-#include <jasper/jas_string.h> ++ ++#include "jasper/jas_config.h" ++#include "jasper/jas_types.h" ++#include "jasper/jas_malloc.h" ++#include "jasper/jas_debug.h" ++#include "jasper/jas_icc.h" ++#include "jasper/jas_cm.h" ++#include "jasper/jas_stream.h" ++#include "jasper/jas_string.h" + + #include <stdlib.h> + #include <ctype.h> +diff --git a/src/libjasper/base/jas_image.c b/src/libjasper/base/jas_image.c +index 04adbba95a28..9d2669ad863f 100644 +--- a/src/libjasper/base/jas_image.c ++++ b/src/libjasper/base/jas_image.c +@@ -81,6 +81,7 @@ + #include "jasper/jas_image.h" + #include "jasper/jas_malloc.h" + #include "jasper/jas_string.h" ++#include "jasper/jas_debug.h" + + /******************************************************************************\ + * Types. +@@ -1227,13 +1228,38 @@ static void jas_image_calcbbox2(jas_image_t *image, jas_image_coord_t *tlx, + *bry = tmpbry; + } + ++static inline long decode_twos_comp(ulong c, int prec) ++{ ++ long result; ++ assert(prec >= 2); ++ jas_eprintf("warning: support for signed data is untested\n"); ++ // NOTE: Is this correct? ++ result = (c & ((1 << (prec - 1)) - 1)) - (c & (1 << (prec - 1))); ++ return result; ++} + ++static inline ulong encode_twos_comp(long n, int prec) ++{ ++ ulong result; ++ assert(prec >= 2); ++ jas_eprintf("warning: support for signed data is untested\n"); ++ // NOTE: Is this correct? ++ if (n < 0) { ++ result = -n; ++ result = (result ^ 0xffffffffUL) + 1; ++ result &= (1 << prec) - 1; ++ } else { ++ result = n; ++ } ++ return result; ++} + + static int getint(jas_stream_t *in, int sgnd, int prec, long *val) + { + long v; + int n; + int c; ++ assert((!sgnd && prec >= 1) || (sgnd && prec >= 2)); + n = (prec + 7) / 8; + v = 0; + while (--n >= 0) { +@@ -1243,8 +1269,7 @@ static int getint(jas_stream_t *in, int sgnd, int prec, long *val) + } + v &= ((1 << prec) - 1); + if (sgnd) { +- /* XXX - Do something here. */ +- abort(); ++ *val = decode_twos_comp(v, prec); + } else { + *val = v; + } +@@ -1255,10 +1280,13 @@ static int putint(jas_stream_t *out, int sgnd, int prec, long val) + { + int n; + int c; ++ bool s; ++ ulong tmp; ++ assert((!sgnd && prec >= 1) || (sgnd && prec >= 2)); + if (sgnd) { +- /* XXX - Do something here. */ +- abort(); ++ val = encode_twos_comp(val, prec); + } ++ assert(val >= 0); + val &= (1 << prec) - 1; + n = (prec + 7) / 8; + while (--n >= 0) { +@@ -1342,16 +1370,20 @@ jas_image_dump(image, stderr); + for (i = 1; i < jas_image_numcmpts(inimage); ++i) { + hstep = jas_image_cmpthstep(inimage, i); + vstep = jas_image_cmptvstep(inimage, i); +- if (hstep < minhstep) ++ if (hstep < minhstep) { + minhstep = hstep; +- if (vstep < minvstep) ++ } ++ if (vstep < minvstep) { + minvstep = vstep; ++ } + } + n = jas_image_numcmpts(inimage); + for (i = 0; i < n; ++i) { + cmpttype = jas_image_cmpttype(inimage, i); +- if (jas_image_sampcmpt(inimage, i, i + 1, 0, 0, minhstep, minvstep, jas_image_cmptsgnd(inimage, i), jas_image_cmptprec(inimage, i))) ++ if (jas_image_sampcmpt(inimage, i, i + 1, 0, 0, minhstep, minvstep, ++ jas_image_cmptsgnd(inimage, i), jas_image_cmptprec(inimage, i))) { + goto error; ++ } + jas_image_setcmpttype(inimage, i + 1, cmpttype); + jas_image_delcmpt(inimage, i); + } +@@ -1362,8 +1394,9 @@ jas_image_dump(image, stderr); + hstep = jas_image_cmpthstep(inimage, 0); + vstep = jas_image_cmptvstep(inimage, 0); + +- inprof = jas_image_cmprof(inimage); +- assert(inprof); ++ if (!(inprof = jas_image_cmprof(inimage))) { ++ abort(); ++ } + numinclrchans = jas_clrspc_numchans(jas_cmprof_clrspc(inprof)); + numinauxchans = jas_image_numcmpts(inimage) - numinclrchans; + numoutclrchans = jas_clrspc_numchans(jas_cmprof_clrspc(outprof)); +@@ -1371,8 +1404,9 @@ jas_image_dump(image, stderr); + numoutchans = numoutclrchans + numoutauxchans; + prec = 8; + +- if (!(outimage = jas_image_create0())) ++ if (!(outimage = jas_image_create0())) { + goto error; ++ } + + /* Create a component for each of the colorants. */ + for (i = 0; i < numoutclrchans; ++i) { +@@ -1456,11 +1490,13 @@ jas_image_dump(image, stderr); + } + } + +- for (i = 0; i < numoutclrchans; ++i) ++ for (i = 0; i < numoutclrchans; ++i) { + jas_free(outcmptfmts[i].buf); ++ } + jas_free(outcmptfmts); +- for (i = 0; i < numinclrchans; ++i) ++ for (i = 0; i < numinclrchans; ++i) { + jas_free(incmptfmts[i].buf); ++ } + jas_free(incmptfmts); + jas_cmxform_destroy(xform); + jas_image_destroy(inimage); +diff --git a/src/libjasper/base/jas_stream.c b/src/libjasper/base/jas_stream.c +index 29e4291cb689..ac51ce25a38a 100644 +--- a/src/libjasper/base/jas_stream.c ++++ b/src/libjasper/base/jas_stream.c +@@ -283,6 +283,9 @@ jas_stream_t *jas_stream_fopen(const char *filename, const char *mode) + + /* Open the underlying file. */ + if ((obj->fd = open(filename, openflags, JAS_STREAM_PERMS)) < 0) { ++ // Free the underlying file object, since it will not otherwise ++ // be freed. ++ jas_free(obj); + jas_stream_destroy(stream); + return 0; + } +diff --git a/src/libjasper/include/jasper/jas_debug.h b/src/libjasper/include/jasper/jas_debug.h +index 2223c6caae15..1619a5ac7684 100644 +--- a/src/libjasper/include/jasper/jas_debug.h ++++ b/src/libjasper/include/jasper/jas_debug.h +@@ -75,8 +75,8 @@ + #include <stdio.h> + + #include <jasper/jas_config.h> +-#include "jasper/jas_types.h" +-#include "jasper/jas_debug.h" ++#include <jasper/jas_types.h> ++#include <jasper/jas_debug.h> + + #ifdef __cplusplus + extern "C" { +diff --git a/src/libjasper/include/jasper/jas_fix.h b/src/libjasper/include/jasper/jas_fix.h +index f91ce25f2100..e9164c7ac4ca 100644 +--- a/src/libjasper/include/jasper/jas_fix.h ++++ b/src/libjasper/include/jasper/jas_fix.h +@@ -80,6 +80,7 @@ + + #include <jasper/jas_config.h> + #include <jasper/jas_types.h> ++#include <jasper/jas_debug.h> + + #ifdef __cplusplus + extern "C" { +diff --git a/src/libjasper/jpc/jpc_bs.c b/src/libjasper/jpc/jpc_bs.c +index c3dd466f8815..f87a40c4b07e 100644 +--- a/src/libjasper/jpc/jpc_bs.c ++++ b/src/libjasper/jpc/jpc_bs.c +@@ -97,8 +97,7 @@ jpc_bitstream_t *jpc_bitstream_sopen(jas_stream_t *stream, char *mode) + jpc_bitstream_t *bitstream; + + /* Ensure that the open mode is valid. */ +-#if 1 +-/* This causes a string literal too long error (with c99 pedantic mode). */ ++#if 0 /* This causes a string literal too long error (with c99 pedantic mode). Why is this so? */ + assert(!strcmp(mode, "r") || !strcmp(mode, "w") || !strcmp(mode, "r+") + || !strcmp(mode, "w+")); + #endif +diff --git a/src/libjasper/jpc/jpc_qmfb.c b/src/libjasper/jpc/jpc_qmfb.c +index af874b4c01b5..bc57b668b57c 100644 +--- a/src/libjasper/jpc/jpc_qmfb.c ++++ b/src/libjasper/jpc/jpc_qmfb.c +@@ -96,7 +96,7 @@ + + int jpc_ft_analyze(jpc_fix_t *a, int xstart, int ystart, int width, int height, + int stride); +-int jpc_ft_synthesize(int *a, int xstart, int ystart, int width, int height, ++int jpc_ft_synthesize(jpc_fix_t *a, int xstart, int ystart, int width, int height, + int stride); + + int jpc_ns_analyze(jpc_fix_t *a, int xstart, int ystart, int width, int height, +@@ -1528,7 +1528,7 @@ int jpc_ft_analyze(jpc_fix_t *a, int xstart, int ystart, int width, int height, + + } + +-int jpc_ft_synthesize(int *a, int xstart, int ystart, int width, int height, ++int jpc_ft_synthesize(jpc_fix_t *a, int xstart, int ystart, int width, int height, + int stride) + { + int numrows = height; +diff --git a/src/libjasper/jpc/jpc_qmfb.h b/src/libjasper/jpc/jpc_qmfb.h +index 75611fe940e4..7bef848eb9bc 100644 +--- a/src/libjasper/jpc/jpc_qmfb.h ++++ b/src/libjasper/jpc/jpc_qmfb.h +@@ -75,6 +75,7 @@ + \******************************************************************************/ + + #include "jasper/jas_seq.h" ++#include "jpc_fix.h" + + /******************************************************************************\ + * Constants. +@@ -101,8 +102,8 @@ any particular platform. Hopefully, it is not too unreasonable, however. */ + #endif + + typedef struct { +- int (*analyze)(int *, int, int, int, int, int); +- int (*synthesize)(int *, int, int, int, int, int); ++ int (*analyze)(jpc_fix_t *, int, int, int, int, int); ++ int (*synthesize)(jpc_fix_t *, int, int, int, int, int); + double *lpenergywts; + double *hpenergywts; + } jpc_qmfb2d_t; +diff --git a/src/libjasper/jpc/jpc_t1dec.c b/src/libjasper/jpc/jpc_t1dec.c +index 8bbe83a5b269..b491ec3b9752 100644 +--- a/src/libjasper/jpc/jpc_t1dec.c ++++ b/src/libjasper/jpc/jpc_t1dec.c +@@ -78,6 +78,7 @@ + #include "jasper/jas_fix.h" + #include "jasper/jas_stream.h" + #include "jasper/jas_math.h" ++#include "jasper/jas_debug.h" + + #include "jpc_bs.h" + #include "jpc_mqdec.h" +diff --git a/src/libjasper/jpc/jpc_tsfb.c b/src/libjasper/jpc/jpc_tsfb.c +index b51b747d6931..50f1437da0cb 100644 +--- a/src/libjasper/jpc/jpc_tsfb.c ++++ b/src/libjasper/jpc/jpc_tsfb.c +@@ -81,6 +81,7 @@ + #include "jpc_cs.h" + #include "jpc_util.h" + #include "jpc_math.h" ++#include "jpc_fix.h" + + void jpc_tsfb_getbands2(jpc_tsfb_t *tsfb, int locxstart, int locystart, + int xstart, int ystart, int xend, int yend, jpc_tsfb_band_t **bands, +@@ -127,7 +128,7 @@ int jpc_tsfb_analyze(jpc_tsfb_t *tsfb, jas_seq2d_t *a) + jas_seq2d_height(a), jas_seq2d_rowstep(a), tsfb->numlvls - 1) : 0; + } + +-int jpc_tsfb_analyze2(jpc_tsfb_t *tsfb, int *a, int xstart, int ystart, ++int jpc_tsfb_analyze2(jpc_tsfb_t *tsfb, jpc_fix_t *a, int xstart, int ystart, + int width, int height, int stride, int numlvls) + { + if (width > 0 && height > 0) { +@@ -155,7 +156,7 @@ int jpc_tsfb_synthesize(jpc_tsfb_t *tsfb, jas_seq2d_t *a) + jas_seq2d_height(a), jas_seq2d_rowstep(a), tsfb->numlvls - 1) : 0; + } + +-int jpc_tsfb_synthesize2(jpc_tsfb_t *tsfb, int *a, int xstart, int ystart, ++int jpc_tsfb_synthesize2(jpc_tsfb_t *tsfb, jpc_fix_t *a, int xstart, int ystart, + int width, int height, int stride, int numlvls) + { + if (numlvls > 0) { +diff --git a/src/libjasper/jpc/jpc_tsfb.h b/src/libjasper/jpc/jpc_tsfb.h +index 1bf9736ae834..33f11f4430d1 100644 +--- a/src/libjasper/jpc/jpc_tsfb.h ++++ b/src/libjasper/jpc/jpc_tsfb.h +@@ -130,6 +130,12 @@ int jpc_tsfb_analyze(jpc_tsfb_t *tsfb, jas_seq2d_t *x); + /* Perform synthesis. */ + int jpc_tsfb_synthesize(jpc_tsfb_t *tsfb, jas_seq2d_t *x); + ++int jpc_tsfb_analyze2(jpc_tsfb_t *tsfb, jpc_fix_t *a, int xstart, int ystart, ++ int width, int height, int stride, int numlvls); ++ ++int jpc_tsfb_synthesize2(jpc_tsfb_t *tsfb, jpc_fix_t *a, int xstart, int ystart, ++ int width, int height, int stride, int numlvls); ++ + /* Get band information for a TSFB. */ + int jpc_tsfb_getbands(jpc_tsfb_t *tsfb, uint_fast32_t xstart, + uint_fast32_t ystart, uint_fast32_t xend, uint_fast32_t yend, +diff --git a/src/libjasper/jpg/jpg_dummy.c b/src/libjasper/jpg/jpg_dummy.c +index db70fca8d860..bc8b7c5182df 100644 +--- a/src/libjasper/jpg/jpg_dummy.c ++++ b/src/libjasper/jpg/jpg_dummy.c +@@ -69,6 +69,7 @@ + #include "jasper/jas_stream.h" + #include "jasper/jas_image.h" + #include "jasper/jas_string.h" ++#include "jasper/jas_debug.h" + + #include "jpg_cod.h" + +diff --git a/src/libjasper/mif/mif_cod.c b/src/libjasper/mif/mif_cod.c +index 5541a22f02d2..724df93c2f0f 100644 +--- a/src/libjasper/mif/mif_cod.c ++++ b/src/libjasper/mif/mif_cod.c +@@ -70,6 +70,7 @@ + #include "jasper/jas_image.h" + #include "jasper/jas_string.h" + #include "jasper/jas_malloc.h" ++#include "jasper/jas_debug.h" + + #include "mif_cod.h" + +@@ -175,6 +176,7 @@ jas_image_t *mif_decode(jas_stream_t *in, char *optstr) + cmpt = hdr->cmpts[cmptno]; + tmpstream = cmpt->data ? jas_stream_fopen(cmpt->data, "rb") : in; + if (!tmpstream) { ++ jas_eprintf("cannot open component file %s\n", cmpt->data); + goto error; + } + if (!(tmpimage = jas_image_decode(tmpstream, -1, 0))) { +@@ -482,26 +484,38 @@ static mif_hdr_t *mif_hdr_get(jas_stream_t *in) + done = false; + do { + if (!mif_getline(in, buf, sizeof(buf))) { ++ jas_eprintf("mif_getline failed\n"); + goto error; + } + if (buf[0] == '\0') { + continue; + } ++ JAS_DBGLOG(10, ("header line: len=%d; %s\n", strlen(buf), buf)); + if (!(tvp = jas_tvparser_create(buf))) { ++ jas_eprintf("jas_tvparser_create failed\n"); + goto error; + } + if (jas_tvparser_next(tvp)) { ++ jas_eprintf("jas_tvparser_next failed\n"); + abort(); + } +- id = jas_taginfo_nonull(jas_taginfos_lookup(mif_tags2, jas_tvparser_gettag(tvp)))->id; ++ id = jas_taginfo_nonull(jas_taginfos_lookup(mif_tags2, ++ jas_tvparser_gettag(tvp)))->id; + jas_tvparser_destroy(tvp); + switch (id) { + case MIF_CMPT: +- mif_process_cmpt(hdr, buf); ++ if (mif_process_cmpt(hdr, buf)) { ++ jas_eprintf("cannot get component information\n"); ++ goto error; ++ } + break; + case MIF_END: + done = 1; + break; ++ default: ++ jas_eprintf("invalid header information: %s\n", buf); ++ goto error; ++ break; + } + } while (!done); + +@@ -524,6 +538,7 @@ static int mif_process_cmpt(mif_hdr_t *hdr, char *buf) + tvp = 0; + + if (!(cmpt = mif_cmpt_create())) { ++ jas_eprintf("cannot create component\n"); + goto error; + } + cmpt->tlx = 0; +@@ -537,8 +552,16 @@ static int mif_process_cmpt(mif_hdr_t *hdr, char *buf) + cmpt->data = 0; + + if (!(tvp = jas_tvparser_create(buf))) { ++ jas_eprintf("cannot create parser\n"); + goto error; + } ++ ++ // Skip the component keyword ++ if ((id = jas_tvparser_next(tvp))) { ++ abort(); ++ } ++ ++ // Process the tag-value pairs. + while (!(id = jas_tvparser_next(tvp))) { + switch (jas_taginfo_nonull(jas_taginfos_lookup(mif_tags, + jas_tvparser_gettag(tvp)))->id) { +@@ -571,12 +594,20 @@ static int mif_process_cmpt(mif_hdr_t *hdr, char *buf) + goto error; + } + break; ++ default: ++ jas_eprintf("invalid component information: %s\n", buf); ++ goto error; ++ break; + } + } + if (!cmpt->sampperx || !cmpt->samppery) { + goto error; + } ++ if (!cmpt->width || !cmpt->height || !cmpt->prec || cmpt->sgnd < 0) { ++ goto error; ++ } + if (mif_hdr_addcmpt(hdr, hdr->numcmpts, cmpt)) { ++ jas_eprintf("cannot add component\n"); + goto error; + } + jas_tvparser_destroy(tvp); +@@ -695,15 +726,16 @@ static int mif_getc(jas_stream_t *in) + do { + switch (c = jas_stream_getc(in)) { + case EOF: +- done = 1; ++ done = true; + break; + case '#': + for (;;) { + if ((c = jas_stream_getc(in)) == EOF) { +- done = 1; ++ done = true; + break; + } + if (c == '\n') { ++ done = true; + break; + } + } +@@ -714,7 +746,7 @@ static int mif_getc(jas_stream_t *in) + } + break; + default: +- done = 1; ++ done = true; + break; + } + } while (!done); +diff --git a/src/libjasper/pnm/pnm_dec.c b/src/libjasper/pnm/pnm_dec.c +index f2ca26e0ac9b..9de7cb7424eb 100644 +--- a/src/libjasper/pnm/pnm_dec.c ++++ b/src/libjasper/pnm/pnm_dec.c +@@ -79,6 +79,7 @@ + #include "jasper/jas_types.h" + #include "jasper/jas_stream.h" + #include "jasper/jas_image.h" ++#include "jasper/jas_debug.h" + + #include "pnm_cod.h" + diff --git a/patches/jasper-no-define-int-types.patch b/patches/jasper-no-define-int-types.patch new file mode 100644 index 0000000..d6a5b0a --- /dev/null +++ b/patches/jasper-no-define-int-types.patch @@ -0,0 +1,19 @@ +--- a/src/libjasper/include/jasper/jas_config.h.in ++++ b/src/libjasper/include/jasper/jas_config.h.in +@@ -152,6 +152,7 @@ + #undef inline + #endif + ++#if 0 + /* Define to `long long' if <sys/types.h> does not define. */ + #undef longlong + +@@ -175,7 +176,7 @@ + + /* Define to `unsigned short' if <sys/types.h> does not define. */ + #undef ushort +- ++#endif + + #else + /* A configure-based build is not being used. */ diff --git a/patches/jasper-sanitized-bmp.patch b/patches/jasper-sanitized-bmp.patch new file mode 100644 index 0000000..d02ee91 --- /dev/null +++ b/patches/jasper-sanitized-bmp.patch @@ -0,0 +1,117 @@ +commit 8f62b4761711d036fd8964df256b938c809b7fca +Author: Michael Adams <mdadams@ece.uvic.ca> +Date: 2016-10-15 20:32:23 -0700 + + Fixed a sanitizer failure in the BMP codec. + Also, added a --debug-level command line option to the imginfo command + for debugging purposes. + +diff --git a/src/appl/imginfo.c b/src/appl/imginfo.c +index 8af19e98aed7..f458a9770e55 100644 +--- a/src/appl/imginfo.c ++++ b/src/appl/imginfo.c +@@ -85,7 +85,8 @@ typedef enum { + OPT_HELP, + OPT_VERSION, + OPT_VERBOSE, +- OPT_INFILE ++ OPT_INFILE, ++ OPT_DEBUG + } optid_t; + + /******************************************************************************\ +@@ -104,6 +105,7 @@ static jas_opt_t opts[] = { + {OPT_VERSION, "version", 0}, + {OPT_VERBOSE, "verbose", 0}, + {OPT_INFILE, "f", JAS_OPT_HASARG}, ++ {OPT_DEBUG, "debug-level", JAS_OPT_HASARG}, + {-1, 0, 0} + }; + +@@ -126,6 +128,7 @@ int main(int argc, char **argv) + int numcmpts; + int verbose; + char *fmtname; ++ int debug; + + if (jas_init()) { + abort(); +@@ -135,6 +138,7 @@ int main(int argc, char **argv) + + infile = 0; + verbose = 0; ++ debug = 0; + + /* Parse the command line options. */ + while ((id = jas_getopt(argc, argv, opts)) >= 0) { +@@ -146,6 +150,9 @@ int main(int argc, char **argv) + printf("%s\n", JAS_VERSION); + exit(EXIT_SUCCESS); + break; ++ case OPT_DEBUG: ++ debug = atoi(jas_optarg); ++ break; + case OPT_INFILE: + infile = jas_optarg; + break; +@@ -156,6 +163,8 @@ int main(int argc, char **argv) + } + } + ++ jas_setdbglevel(debug); ++ + /* Open the image file. */ + if (infile) { + /* The image is to be read from a file. */ +@@ -177,6 +186,7 @@ int main(int argc, char **argv) + + /* Decode the image. */ + if (!(image = jas_image_decode(instream, fmtid, 0))) { ++ jas_stream_close(instream); + fprintf(stderr, "cannot load image\n"); + return EXIT_FAILURE; + } +diff --git a/src/libjasper/bmp/bmp_dec.c b/src/libjasper/bmp/bmp_dec.c +index 7a6dcb157483..6e7d8802cc7b 100644 +--- a/src/libjasper/bmp/bmp_dec.c ++++ b/src/libjasper/bmp/bmp_dec.c +@@ -77,6 +77,7 @@ + #include "jasper/jas_stream.h" + #include "jasper/jas_image.h" + #include "jasper/jas_malloc.h" ++#include "jasper/jas_debug.h" + + #include "bmp_cod.h" + +@@ -122,12 +123,22 @@ jas_image_t *bmp_decode(jas_stream_t *in, char *optstr) + jas_eprintf("cannot get header\n"); + return 0; + } ++ JAS_DBGLOG(1, ( ++ "BMP header: magic 0x%x; siz %d; res1 %d; res2 %d; off %d\n", ++ hdr.magic, hdr.siz, hdr.reserved1, hdr.reserved2, hdr.off ++ )); + + /* Read the bitmap information. */ + if (!(info = bmp_getinfo(in))) { + jas_eprintf("cannot get info\n"); + return 0; + } ++ JAS_DBGLOG(1, ++ ("BMP information: len %d; width %d; height %d; numplanes %d; " ++ "depth %d; enctype %d; siz %d; hres %d; vres %d; numcolors %d; " ++ "mincolors %d\n", info->len, info->width, info->height, info->numplanes, ++ info->depth, info->enctype, info->siz, info->hres, info->vres, ++ info->numcolors, info->mincolors)); + + /* Ensure that we support this type of BMP file. */ + if (!bmp_issupported(&hdr, info)) { +@@ -440,7 +451,7 @@ static int bmp_getint32(jas_stream_t *in, int_fast32_t *val) + if ((c = jas_stream_getc(in)) == EOF) { + return -1; + } +- v |= (c << 24); ++ v |= (JAS_CAST(uint_fast32_t, c) << 24); + if (--n <= 0) { + 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); + } |