Z3 String Support#46
Merged
Merged
Conversation
- Add fstrlen operator to operators enum in dfsan.h - Modify __dfsw_strlen to create fstrlen labels with: - l2 = content label (for dependencies) - op1 = null_from_input flag (whether null terminator is tainted) - op2 = actual length - Update dfsan_union to preserve op1/op2 for all higher-order ops (fmemcmp, fsize, fatoi, fstrlen) instead of zeroing them Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Add solution_op_t enum with SET, INSERT, DELETE operations - Extend solution_val struct to support: - SET: set single byte at offset (existing behavior) - INSERT: insert bytes at offset (for extending strings) - DELETE: remove bytes at offset (for shrinking strings) - Update fgtest generate_input to handle all operation types: - Sort solutions by descending offset to avoid invalidation - Build new input in memory before writing This enables atoi and strlen solvers to generate solutions that change the input length, not just byte values. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
strlen solving: - Add strlen_name_format for symbolic strlen variables - Handle fstrlen op in serialize() to create strlen-input-offset-len-null symbols - Add strlen optimization in solve_task() to minimize strlen values - Generate INSERT/DELETE solutions for strlen constraints atoi fixes: - Track original length in atoi_name_format for extend/shrink detection - Add fatoi to ICmp special cases (like fmemcmp) to fix value cache - Generate INSERT/DELETE solutions when atoi result length differs from original Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- strlen_test.c: basic strlen comparisons (>, ==, <) - strlen_extend.c: test extending string length - strlen_shrink.c: test shrinking string length - strlen_json3.c: strlen with JSON parsing (non-null-terminated fields) - strlen_null_from_input.c: test null_from_input flag behavior - cpp_string.cpp: fix expected output file index Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Test atoi with both extending (999 -> 12345) and shrinking (999 -> 42) to verify INSERT/DELETE solution operations work correctly. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Add taint tracking for string search functions using Z3 string theory: Operators added (dfsan.h): - fstrchr: strchr/memchr (find first occurrence) - fstrrchr: strrchr/memrchr (find last occurrence) - fstrstr: strstr (find substring) Runtime wrappers (dfsan_custom.cpp): - __dfsw_strchr: track character search with chaining support - __dfsw_strrchr: track reverse character search - __dfsw_memchr: track memory character search - __dfsw_memrchr: track reverse memory search (new) - __dfsw_strstr: track substring search with needle caching Label structure: - l1 = source content label (supports chaining from previous search) - l2 = target char/needle label (supports symbolic targets) - op1 = concrete target value - op2 = found position (-1 if not found) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Implement Z3 string theory integration for strchr/strstr solving: Z3 AST generation (z3-ts.cpp): - Handle fstrchr: build Z3 string, use indexof() for search - Handle fstrrchr: use last_indexof() for reverse search - Handle fstrstr: support concrete and symbolic needles - Chain detection: track previous search results for offset - ICmp handling: convert index to found/not-found comparison Helper functions: - build_string_from_label(): construct Z3 string from byte labels - get_byte_expr(): get byte expression for input offset Solution generation: - Track string ranges for null-byte post-processing - Handle str-* variables from string constraints Bug fixes: - Change uint8_t to uint16_t for size to handle >255 bit values - Use default solver instead of QF_BV for mixed theories Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Add lit tests for strchr, strrchr, memchr, memrchr, strstr: - strchr.c: basic character search - strrchr.c: reverse character search - memchr.c: memory character search - memrchr.c: reverse memory search - strstr.c: substring search - strchr_chain.c: chained strchr calls Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
When memchr/memrchr is called with a length derived from pointer arithmetic on a previous string op result (e.g., t1 = memrchr(buf, c, n); memrchr(buf, c2, t1-buf)), we now create a fsubstr label to represent the bounded substring. This allows the Z3 solver to use str.substr instead of dealing with PtrToInt operations. Changes: - Add fsubstr operator to dfsan.h for substring with symbolic length - Add get_base_input_label() helper to find base input from content labels - Add find_string_op_source() helper to detect string op ancestry through PtrToInt/Sub/Add operations - Update __dfsw_memchr and __dfsw_memrchr to create fsubstr labels when n_label derives from a string op on the same buffer - Add fsubstr handler in z3-ts.cpp to generate str.substr constraints - Add PtrToInt handler for string op results (converts index to bitvector) - Update fstrchr and fstrrchr handlers to recognize fsubstr sources Co-Authored-By: Claude <noreply@anthropic.com>
- memrchr_chain.c: test chained memrchr (backward search) where second call uses length from first result (last_indexof with substr) - memchr_chain.c: test chained memchr (forward search) where second call uses length from first result (indexof with substr) - memchr_mixed_chain.c: test mixed backward + forward chain where memrchr finds last ';' and memchr finds ':' before it (uses substr) - strchr_mixed_chain.c: test mixed backward + forward chain where strrchr finds last ';' and strchr finds ':' (uses pointer comparison) - str_mem_mixed_chain.c: test strchr followed by memrchr with bounded length (combines null-terminated and bounded search) Co-Authored-By: Claude <noreply@anthropic.com>
- Add fstrpbrk operator for strpbrk string search function - Implement __dfsw_strpbrk wrapper with proper Alloca label filtering - Implement __dfsw_memmem wrapper reusing fstrstr for substring search - Add fstrpbrk handler in Z3 solver using simplified single-character approach to avoid solver timeout with complex nested ite expressions - Update is_strfunc checks to use fstr_op_start/fstr_op_end range instead of listing individual operators - Add tests for strpbrk and memmem Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Add fstr_off operator to track GEP offsets on string op pointers (e.g., sep + 1 where sep is from strchr). Instrumented via __taint_trace_gep_ptr in TaintPass. - Add n_label parameter to get_str_label_n to create fsubstr when the length derives from a string op (enables memchr chaining pattern: memchr(buf, c2, strchr(buf, c1) - buf) even when length is 0). - Add strcmp/strncmp wrappers with fstrcmp operator using Z3 string theory for symbolic string comparison. - Add strncpy wrapper with fsubstr tracking for bounded copies. - Fix pointer arithmetic serialization: (PtrToInt(string_op)) - base_addr now correctly returns just the index, not idx - base_addr. - Clean up verbose debug output (keep VALUE MISMATCH warnings). Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Update __dfsw_strcat to create fstrcat labels tracking string concatenation - Add fstrcat handler in Z3 solver using Z3 string theory concat - Add string_info_cache_ for tracking string bounds across operations - Fix Concat fallback in build_string_from_label to populate cache - Add strcat.c test: strchr + strncpy + strcat + strcmp chain Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
…xOf positions Previously fsubstr only supported prefix mode (substr from 0 to indexOf position). This adds suffix mode (substr from indexOf position to end) for patterns like: - strcpy(suffix, pos + 1) after pos = strchr(buf, '_') - memchr(t1, c, len) where t1 is a previous memchr result Key changes: - Split runtime map into content map (fsubstr/fstrcat) and indexOf map (fstrchr/fstrrchr/fstrstr/fstrpbrk/fstr_off) - Store indexOf labels at result pointer addresses for suffix recovery - Add is_indexof_op() and is_content_string_op() helpers - fsubstr now uses op2: 0=prefix mode, 1=suffix mode - Z3 solver handles suffix mode with substr(str, start_pos, remaining_len) - get_str_label checks indexOf map at null terminator position for strcpy patterns where *pos = '\0' precedes the copy Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Fix string operation labels to ensure l1 matches op1 and l2 matches op2 across all string search operations (strchr, strrchr, strstr, strpbrk, memchr). Update strcat to pass pointers instead of lengths for concrete content access. Add strncat wrapper with proper symbolic handling. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Enable symbolic constraint solving when the haystack (base string) is concrete in strchr/strrchr/strstr/strpbrk by sending concrete content to solver and building Z3 string literals. Repurpose op1 field for haystack pointer and update validation logic to skip indexOf operations where runtime values are not available in the standard location. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
When walking back through chained indexOf operations to find the base haystack, properly track which label sent the concrete content via __taint_trace_memcmp. The concrete content is sent by the indexOf operation that has the concrete haystack as its l1, not the final base label (which is 0). Use concrete_label to track this and look up the correct entry in memcmp_cache. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Replace fixed-size linear-search arrays with open-addressed hash tables optimized for shadow memory address range (0x700000040000-0x800000000000). Move implementation from dfsan_custom.cpp to dfsan.cpp following existing taint_set_file/taint_get_file pattern. Add configurable initial capacity via string_map_capacity flag (default 256, auto-grows at 0.7 load factor). - Hash function: multiplicative hashing on middle bits after removing alignment - Collision resolution: linear probing with power-of-2 capacity for fast modulo - Function naming: taint_set/get_str_content_label, taint_set/get_str_indexof_label - Initialization: InitializeStringMaps() called from dfsan_init() Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Implements fprefixof and fsuffixof operators to enable symbolic execution of prefix/suffix checks. Maps to Z3's built-in prefixof/suffixof functions for constraint solving. Includes lit test for validation. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Add new WrapperKind enum values and instrumentation for string operations: - WK_Strchr, WK_Strrchr, WK_Strstr for character/substring search - WK_Prefixof, WK_Suffixof for prefix/suffix checks - WK_Strcat for string concatenation - WK_Strsub for substring extraction (s, start, len) Change existing WK_Memcmp, WK_Strcmp, WK_Strncmp cases to call __dfsw_* wrapper functions instead of __taint_* helpers, allowing deprecation of the __taint_* functions. Add __dfsw_strsub implementation that: - Handles strsub(s, start, len) with both start and len potentially symbolic - Composes constraint using two nested fsubstr operations: 1. suffix(str, start) for str[start:] 2. prefix(suffix, len) for str[start:start+len] - Allocates and returns new string like xmlStrsub Update abilist with new mappings including xmlStrsub=substr, xmlStrchr=strchr. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add support to trace string constraints and use Z3 to solve them.