Z3 String Support

.github/workflows/test.yml

@@ -18,7 +18,27 @@ jobs:
     - uses: actions/checkout@v4
 
     - name: install dependencies
-      run: sudo apt-get update && sudo apt-get install -y llvm-14 clang-14 libc++-14-dev libc++abi-14-dev python3-minimal libz3-dev libgoogle-perftools-dev libboost-container-dev python3-dev
+      run: sudo apt-get update && sudo apt-get install -y llvm-14 clang-14 libc++-14-dev libc++abi-14-dev python3-minimal libgoogle-perftools-dev libboost-container-dev python3-dev libbsd-dev
+
+    - name: Cache Z3
+      id: cache-z3
+      uses: actions/cache@v4
+      with:
+        path: ~/z3
+        key: z3-4.15.4-x64-glibc-2.39
+
+    - name: Install Z3
+      run: |
+        if [ ! -d ~/z3 ]; then
+          wget https://github.com/Z3Prover/z3/releases/download/z3-4.15.4/z3-4.15.4-x64-glibc-2.39.zip
+          unzip z3-4.15.4-x64-glibc-2.39.zip
+          mv z3-4.15.4-x64-glibc-2.39 ~/z3
+        fi
+        sudo cp ~/z3/bin/z3 /usr/local/bin/
+        sudo cp ~/z3/bin/libz3.so /usr/local/lib/
+        sudo cp ~/z3/bin/libz3.a /usr/local/lib/
+        sudo cp -r ~/z3/include/* /usr/local/include/
+        sudo ldconfig
     #   run: |
     #     wget https://apt.llvm.org/llvm.sh
     #     chmod +x llvm.sh

CMakeLists.txt

@@ -4,6 +4,42 @@ project(symsan VERSION 1.2.2 LANGUAGES C CXX ASM)
 
 find_package(LLVM 14 REQUIRED CONFIG)
 
+# Find Z3 (minimum version 4.8.15 required for string theory APIs)
+# Prefer /usr/local over system
+find_library(Z3_LIBRARY NAMES z3 PATHS /usr/local/lib NO_DEFAULT_PATH)
+if (NOT Z3_LIBRARY)
+    find_library(Z3_LIBRARY NAMES z3)
+endif()
+find_path(Z3_INCLUDE_DIR NAMES z3.h PATHS /usr/local/include NO_DEFAULT_PATH)
+if (NOT Z3_INCLUDE_DIR)
+    find_path(Z3_INCLUDE_DIR NAMES z3.h)
+endif()
+
+# Check Z3 version
+if (Z3_INCLUDE_DIR)
+    file(READ "${Z3_INCLUDE_DIR}/z3_version.h" Z3_VERSION_CONTENT)
+    string(REGEX MATCH "#define Z3_MAJOR_VERSION[ \t]+([0-9]+)" _ "${Z3_VERSION_CONTENT}")
+    set(Z3_VERSION_MAJOR ${CMAKE_MATCH_1})
+    string(REGEX MATCH "#define Z3_MINOR_VERSION[ \t]+([0-9]+)" _ "${Z3_VERSION_CONTENT}")
+    set(Z3_VERSION_MINOR ${CMAKE_MATCH_1})
+    string(REGEX MATCH "#define Z3_BUILD_NUMBER[ \t]+([0-9]+)" _ "${Z3_VERSION_CONTENT}")
+    set(Z3_VERSION_PATCH ${CMAKE_MATCH_1})
+    set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}")
+
+    message(STATUS "Found Z3 version: ${Z3_VERSION}")
+
+    # Require at least version 4.8.15
+    if (Z3_VERSION_MAJOR LESS 4 OR
+        (Z3_VERSION_MAJOR EQUAL 4 AND Z3_VERSION_MINOR LESS 8) OR
+        (Z3_VERSION_MAJOR EQUAL 4 AND Z3_VERSION_MINOR EQUAL 8 AND Z3_VERSION_PATCH LESS 15))
+        message(FATAL_ERROR "Z3 version ${Z3_VERSION} found, but version 4.8.15 or later is required (for string theory APIs)")
+    endif()
+endif()
+
+message(STATUS "Z3_LIBRARY: ${Z3_LIBRARY}")
+message(STATUS "Z3_INCLUDE_DIR: ${Z3_INCLUDE_DIR}")
+message(STATUS "Z3_VERSION: ${Z3_VERSION}")
+
 if (LLVM_FOUND)
     message(STATUS "LLVM_VERSION_MAJOR: ${LLVM_VERSION_MAJOR}")
     message(STATUS "LLVM_VERSION_MINOR: ${LLVM_VERSION_MINOR}")

backend/fastgen.cpp

@@ -334,7 +334,7 @@ __taint_trace_memcmp(dfsan_label label) {
 
   uint16_t has_content = 1;
   // if both operands are symbolic, skip sending the content
-  if (info->l1 != CONST_LABEL && info->l2 != CONST_LABEL)
+  if ((info->l1 != CONST_LABEL && info->l2 != CONST_LABEL) || info->size == 0)
     has_content = 0;
 
   pipe_msg msg = {
@@ -357,7 +357,10 @@ __taint_trace_memcmp(dfsan_label label) {
   size_t msg_size = sizeof(memcmp_msg) + info->size;
   memcmp_msg *mmsg = (memcmp_msg*)__builtin_alloca(msg_size);
   mmsg->label = label;
-  internal_memcpy(mmsg->content, (void*)info->op1.i, info->size); // concrete oprand is always in op1
+  // Copy concrete content: use op1 if l1 is concrete, else op2
+  void *concrete_ptr = (info->l1 == CONST_LABEL) ? (void*)info->op1.i : (void*)info->op2.i;
+  internal_memcpy(mmsg->content, concrete_ptr, info->size);
+  AOUT("sending memcmp content for label %d, size %u, msg_size=%lu\n", label, info->size, msg_size);
 
   // FIXME: assuming single writer so msg will arrive in the same order
   if (internal_write(__pipe_fd, mmsg, msg_size) < 0) {

compiler/ko_clang.c

@@ -179,7 +179,9 @@ static void add_runtime() {
     cc_params[cc_par_cnt++] = "-Wl,--whole-archive";
     cc_params[cc_par_cnt++] = alloc_printf("%s/libZ3Solver.a", obj_path);
     cc_params[cc_par_cnt++] = "-Wl,--no-whole-archive";
+    cc_params[cc_par_cnt++] = "-L/usr/local/lib";
     cc_params[cc_par_cnt++] = "-lz3";
+    cc_params[cc_par_cnt++] = "-Wl,-rpath,/usr/local/lib";
   }
 
   if (getenv("KO_USE_FASTGEN")) {

driver/CMakeLists.txt

@@ -13,7 +13,7 @@ target_include_directories(FGTest PUBLIC
 target_link_libraries(FGTest PRIVATE
   launcher
   z3parser
-  z3
+  ${Z3_LIBRARY}
   rt
 )
 install (TARGETS FGTest DESTINATION ${SYMSAN_BIN_DIR})

driver/fgtest.cpp

@@ -10,6 +10,7 @@ extern "C" {
 
 #include "parse-z3.h"
 
+#include <algorithm>
 #include <memory>
 #include <unordered_map>
 #include <unordered_set>
@@ -45,33 +46,71 @@ static const char* __output_dir = ".";
 static uint32_t __instance_id = 0;
 static uint32_t __session_id = 0;
 static uint32_t __current_index = 0;
+static int __enum_gep = 0;  // GEP enumeration enabled by default
 static z3::context __z3_context;
 
 // z3parser
 symsan::Z3ParserSolver *__z3_parser = nullptr;
 
 static void generate_input(symsan::Z3ParserSolver::solution_t &solutions) {
+  using op_t = symsan::Z3ParserSolver::solution_op_t;
+
+  // Build the new input in memory to handle INSERT/DELETE properly
+  std::vector<uint8_t> new_input(input_buf, input_buf + input_size);
+
+  // Sort solutions by offset in descending order so INSERT/DELETE don't
+  // invalidate subsequent offsets
+  std::vector<size_t> order(solutions.size());
+  for (size_t i = 0; i < order.size(); ++i) order[i] = i;
+  std::sort(order.begin(), order.end(), [&solutions](size_t a, size_t b) {
+    return solutions[a].offset > solutions[b].offset;
+  });
+
+  for (size_t idx : order) {
+    const auto& sol = solutions[idx];
+    switch (sol.op) {
+      case op_t::SET:
+        if (sol.offset < new_input.size()) {
+          AOUT("SET offset %d = %x\n", sol.offset, sol.val);
+          new_input[sol.offset] = sol.val;
+        }
+        break;
+
+      case op_t::INSERT:
+        if (sol.offset <= new_input.size()) {
+          AOUT("INSERT %zu bytes at offset %d\n", sol.data.size(), sol.offset);
+          new_input.insert(new_input.begin() + sol.offset,
+                          sol.data.begin(), sol.data.end());
+        }
+        break;
+
+      case op_t::DELETE:
+        if (sol.offset < new_input.size()) {
+          size_t del_len = std::min((size_t)sol.len,
+                                    new_input.size() - sol.offset);
+          AOUT("DELETE %zu bytes at offset %d\n", del_len, sol.offset);
+          new_input.erase(new_input.begin() + sol.offset,
+                         new_input.begin() + sol.offset + del_len);
+        }
+        break;
+    }
+  }
+
+  // Write the new input to file
   char path[PATH_MAX];
   snprintf(path, PATH_MAX, "%s/id-%d-%d-%d", __output_dir,
            __instance_id, __session_id, __current_index++);
-  int fd = open(path, O_CREAT | O_WRONLY, S_IRUSR | S_IWUSR);
+  int fd = open(path, O_CREAT | O_WRONLY | O_TRUNC, S_IRUSR | S_IWUSR);
   if (fd == -1) {
     AOUT("failed to open new input file for write");
     return;
   }
 
-  if (write(fd, input_buf, input_size) == -1) {
-    AOUT("failed to copy original input\n");
-    close(fd);
-    return;
-  }
-  AOUT("generate #%d output\n", __current_index - 1);
+  AOUT("generate #%d output (size: %zu -> %zu)\n",
+       __current_index - 1, input_size, new_input.size());
 
-  for (auto const& sol : solutions) {
-    uint8_t value = sol.val;
-    AOUT("offset %d = %x\n", sol.offset, value);
-    lseek(fd, sol.offset, SEEK_SET);
-    write(fd, &value, sizeof(value));
+  if (write(fd, new_input.data(), new_input.size()) == -1) {
+    AOUT("failed to write new input\n");
   }
 
   close(fd);
@@ -89,7 +128,7 @@ static void __solve_cond(dfsan_label label, uint8_t r, bool add_nested, void *ad
   for (auto id : tasks) {
     // solve
     symsan::Z3ParserSolver::solution_t solutions;
-    auto status = __z3_parser->solve_task(id, 5000U, solutions);
+    auto status = __z3_parser->solve_task(id, 30000U, solutions);  // 30 seconds
     if (solutions.size() != 0) {
       AOUT("branch solved\n");
       generate_input(solutions);
@@ -111,14 +150,14 @@ static void __handle_gep(dfsan_label ptr_label, uptr ptr,
 
   std::vector<uint64_t> tasks;
   if (__z3_parser->parse_gep(ptr_label, ptr, index_label, index, num_elems,
-                             elem_size, current_offset, true, tasks)) {
+                             elem_size, current_offset, __enum_gep, tasks)) {
     AOUT("WARNING: failed to parse gep %d @%p\n", index_label, addr);
     return;
   }
 
   for (auto id : tasks) {
     symsan::Z3ParserSolver::solution_t solutions;
-    auto status = __z3_parser->solve_task(id, 5000U, solutions);
+    auto status = __z3_parser->solve_task(id, 30000U, solutions);  // 30 seconds
     if (solutions.size() != 0) {
       AOUT("gep solved\n");
       generate_input(solutions);
@@ -173,13 +212,28 @@ int main(int argc, char* const argv[]) {
         debug = 1;
     }
 
+    // check for session_id
+    char *session_opt = strstr(options, "session_id=");
+    if (session_opt) {
+      session_opt += strlen("session_id=");
+      __session_id = atoi(session_opt);
+    }
+
     // check if solve_ub is enabled
     char *solve_ub_opt = strstr(options, "solve_ub=");
     if (solve_ub_opt) {
       solve_ub_opt += strlen("solve_ub="); // skip "solve_ub="
       if (strcmp(solve_ub_opt, "1") == 0 || strcmp(solve_ub_opt, "true") == 0)
         solve_ub = 1;
     }
+
+    // check if GEP enumeration is disabled
+    char *enum_gep_opt = strstr(options, "enum_gep=");
+    if (enum_gep_opt) {
+      enum_gep_opt += strlen("enum_gep="); // skip "enum_gep="
+      if (strncmp(enum_gep_opt, "0", 1) == 0 || strncmp(enum_gep_opt, "false", 5) == 0)
+        __enum_gep = 0;
+    }
   }
 
   // load input file

include/parse-z3.h

@@ -34,16 +34,30 @@ class Z3AstParser : public ASTParser<z3_task_t> {
   z3::context &context_;
   const char* input_name_format;
   const char* atoi_name_format;
+  const char* strlen_name_format;
+
+  // String ranges for null-byte post-processing (input_id -> list of (start, end))
+  std::unordered_map<uint32_t, std::vector<std::pair<uint32_t, uint32_t>>> string_ranges_;
+
+  // String info cache: label -> (input_id, offset, length)
+  struct string_info_t {
+    uint32_t input_id;
+    uint32_t offset;
+    uint32_t length;
+  };
+  std::unordered_map<dfsan_label, string_info_t> string_info_cache_;
 
 private:
+  // Original input cache
+  std::vector<input_t> inputs_cache_;
+
   // fsize flag
   bool has_fsize;
 
   // input deps
   using input_dep_set_t = std::unordered_set<offset_t, offset_hash>;
 
   // caches
-  std::vector<input_t> inputs_cache_;
   std::vector<uint32_t> tsize_cache_;
   std::vector<input_dep_set_t> deps_cache_;
   std::vector<Z3_ast> expr_cache_;
@@ -116,6 +130,11 @@ class Z3AstParser : public ASTParser<z3_task_t> {
   void construct_index_tasks(z3::expr &index, uint64_t curr,
                              uint64_t lb, uint64_t ub, uint64_t step,
                              z3_task_t &nested, std::vector<uint64_t> &tasks);
+
+  // String theory helpers for strchr/strstr
+  z3::expr build_string_from_label(dfsan_label content_label, input_dep_set_t &deps);
+  z3::expr get_byte_expr(uint32_t input, uint32_t offset, input_dep_set_t &deps);
+  bool label_contains_indexof(dfsan_label label);
 };
 
 class Z3ParserSolver : public Z3AstParser {
@@ -125,10 +144,35 @@ class Z3ParserSolver : public Z3AstParser {
       : Z3AstParser(base, size, context) {}
   ~Z3ParserSolver() {}
 
+  // Solution operation types
+  enum class solution_op_t : uint8_t {
+    SET,     // Set byte at offset to val
+    INSERT,  // Insert bytes at offset (shifts following bytes right)
+    DELETE   // Delete len bytes starting at offset (shifts following bytes left)
+  };
+
   struct solution_val {
-    uint32_t id;
-    uint32_t offset;
-    uint8_t val;
+    solution_op_t op;
+    uint32_t id;       // input id
+    uint32_t offset;   // position in file
+    union {
+      uint8_t val;     // for SET: the byte value
+      uint32_t len;    // for DELETE: number of bytes to delete
+    };
+    std::vector<uint8_t> data; // for INSERT: bytes to insert
+
+    // Constructors for convenience
+    // SET: set single byte at offset
+    solution_val(uint32_t id, uint32_t offset, uint8_t val)
+        : op(solution_op_t::SET), id(id), offset(offset), val(val) {}
+
+    // INSERT: insert bytes at offset
+    solution_val(uint32_t id, uint32_t offset, std::vector<uint8_t> data)
+        : op(solution_op_t::INSERT), id(id), offset(offset), data(std::move(data)) {}
+
+    // DELETE: delete len bytes at offset
+    solution_val(solution_op_t op, uint32_t id, uint32_t offset, uint32_t len)
+        : op(op), id(id), offset(offset), len(len) {}
   };
 
   enum solving_status {