Ucsan#47
Merged
Merged
Conversation
…nary-based API
Updated the Python binding to handle the new solution_t structure with three
operation types (SET, INSERT, DELETE). Solutions are now returned as
dictionaries instead of tuples for better clarity and extensibility.
Changes:
- Added OpType IntEnum with SET(0), INSERT(1), DELETE(2) to module
- Updated SolveTask to return dictionaries with operation-specific fields:
* SET: {op, id, offset, val}
* INSERT: {op, id, offset, data}
* DELETE: {op, id, offset, len}
- Updated test.py to demonstrate new dictionary-based API
- Fixed CMakeLists.txt to use ${Z3_LIBRARY} for correct Z3 linking
- Added comprehensive API documentation with examples to README.md
The new format supports string constraint solving operations (INSERT/DELETE
for strchr/strstr) while maintaining backward compatibility for byte-level
SET operations.
Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
…red offsets - Add label-level tracking (is_label_bv_, is_label_seq_) to track whether expressions involve bitvector or string/sequence variables - Extend branch_dependency_t to cache input expressions and track whether offsets are used in bitvector and/or string contexts - Add mark_expr_type() to mark offsets with expression types before linking - Add add_string_bitvec_link() to create constraints linking str-X-Y-Z characters with input-X-Y bitvector bytes at the same offsets - Modify add_nested_constraints() to detect overlapping offsets and add linking constraints when the same offset is used in both contexts - Cache string ranges with their z3::expr for efficient linking lookup Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
…ng constraints handling
…ave an empty seed
…on table as symsan
…cking - ObjectOrigin and ObjectMapKey now use uint32_t/int32_t instead of uint64_t - Add range validation before casting to narrower types in lookup_object - Allows negative offsets (e.g., from OP_DUMMY counter) to work correctly - Fix printf format specifiers for the new types Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- buildDangleFunction: call ucsan_wrap_retval for each primitive element in struct returns, load from returned pointer and assemble the struct - Change UCWrapRetvalFn return type from i16* to void* to match runtime - visitReturnInst: use getShadowTy(RT) instead of PrimitiveShadowTy - __taint_set_retval_tls: add index parameter to support struct elements, calculate index from pointer offset (ret_label - __ucsan_retval_tls) - loadShadowRecursive: fix InsertValue chaining in both TaintPass and UCSanPass - return accumulated shadow value instead of discarding it Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
…ro-length under-constrained strings TaintPass: when hoisting strlen bounds checks with UCSan, find and hoist the ucsan_check_pointer call for the string base pointer so that under-constrained objects are materialized before __taint_solve_str_bounds dereferences them. Search all loop blocks (not just header) to find the matching ucsan_check_pointer. dfsan: in __taint_solve_str_bounds, scan shadow memory when strlen returns 0 (under-constrained globals are zero-initialized) to determine tainted extent, and treat tainted zero terminators as input-derived. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Wraps open/openat/close/fopen/freopen/fclose, fseek/fseeko/lseek/ftell/rewind, fgetc/getc/getchar in ucsan_custom.cpp with a fake-file table backed by the existing input objects, so symbolic reads work without touching real libc I/O. Guards the same wrappers in dfsan_custom.cpp behind USE_UCSAN_CUSTOM to avoid duplicate symbol conflicts. fgetc creates an 8-bit byte label and ZExt-extends it to 32 bits to match the int return type. The extension goes through a new __taint_extend_label bridge (weak stub in ucsan.cpp, strong override in dfsan.cpp wrapping do_taint_union) so ucsan can be linked without symsan. All wrappers that don't otherwise store a meaningful return-value label now clear __dfsan_retval_tls explicitly; handleUCSanCall auto-loads that slot after each __dfsw_* call and would otherwise read stale label bits left by an earlier fgetc. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…so fixed return label of read-like functions
Malloc-size minimization could collapse a symbolic allocation size to malloc(0), steering exploration into allocator/null corner cases instead of the intended small heap object. Two complementary, non-conflicting guards: - Thread the concrete allocation size through __taint_minimize_label (label, size, bounds). When the concrete size is 0 and allow_zero_size_alloc is off, fastgen emits a synthetic "size != 0" condition (via __taint_send_cond) so the manager generates a new input with a non-zero size. This is the hard/UCSan path for real malloc(0). - record_minimize gains an allow_zero parameter; when false the z3 optimizer adds (size != 0) only inside the minimize pass (soft: it falls back to the bounded solver if unsat). Adds the allow_zero_size_alloc dfsan flag (default false) and plumbs allow_zero through parse.h / parse-z3.h / the Python binding.
Pass -taint-solve-ub=true in the ucsan,taint pipeline so the analysis of target IR emits UB-solving instrumentation (ClSolveUB). Actual solving remains gated at runtime by the solve_ub dfsan flag.
Add __dfsw_ wrappers for htons/ntohs/htonl/ntohl, __bswap_16/32/64 and __bswapsi2/__bswapdi2 that byte-swap the label via Extract+Concat (net*_label is a no-op on big-endian). Without these, byte-swapped protocol fields (e.g. htons(ETHERTYPE_IP6)) lose their symbolic relationship and dispatch constraints become unsolvable. UCSanPass keeps __bswap_16/32/64 dangle wrappers semantic (emit llvm.bswap) instead of returning an arbitrary symbolic value, so the later TaintPass models them normally. abilist: mark htonl/htons/ntohl/ntohs/__bswap_*/__bswap[sd]i2 as taint (ucsan) / custom (dfsan). Keep them uninstrumented as well (the malloc/memcpy convention) so isInstrumented() is false and TaintPass wraps them as custom instead of renaming them to <name>.taint; __bswap_16/32/64 have no libc entry so they get an explicit uninstrumented mark in done_abilist.
Replace hard-coded UCSAN_OBJECT_SIZE_LIMIT comparisons with ucsan_object_size_limit(), which honors the max_obj_size runtime flag and falls back to UCSAN_OBJECT_SIZE_LIMIT when the flag is unset. The cap can now be tuned per run instead of recompiling. max_obj_size now defaults to 0 (meaning "use UCSAN_OBJECT_SIZE_LIMIT"), so the default behavior is unchanged.
Add a cross-pass summary so loop-bounds reasoning can see writes that happen behind a call (inter-procedural loops) and through UCSan-checked pointers, and hoist the size/bounds *solving* out of the loop. - UCSanSummary.h: shared "ptr_field_access" metadata schema — "callee loads a pointer from arg#N + field_offset and reads/writes access_size bytes through it" — with create/parse helpers. - UCSanPass (producer): record these per function (recordPointerLoadSummary, recordMemoryAccessSummary) and attach as ucsan.mem_summary metadata. - TaintPass (consumer, hoistBoundsChecks): use callee summaries, ucsan_check_pointer-guarded affine accesses, and __taint_solve_bounds to emit hoisted solve_size hints in the preheader. Hard __taint_check_bounds (concrete-range check) is emitted ONLY for proven affine recurrences (Groups / affine SolveGroups). The heuristic paths — inter-procedural callee summaries, the unknown-trip-count guard heuristic, and NonAffineSolveGroups — emit only the soft solve_size hint: their ranges (trip*size, guard_count*size, ConstantIterations*counts) are guesses, not proven extents, so asserting a concrete bound there would risk spurious OOB reports. Per-iteration __taint_check_bounds inside the loop (and the callee's own checks) are left untouched. Also erase ptrtoint temporaries materialized only for SCEV queries. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Extend the single-file simulator so programs that query their input file behave under UCSan replay (useful for any user-mode app that stats/sizes its input, not just afgen targets): - ucsan_file_state tracks the backing-file size (concrete_file_size via stat()), the fake fd, and the fake FILE*; open/openat/fopen record them. - __dfsw_fileno / fileno_unlocked return the synthetic fd. - __dfsw_ucsan_fstat / fstat64 / fxstat / fxstat64 synthesize a regular- file stat whose st_size is the simulated file size. abilist: fileno/fileno_unlocked=custom. Note: fileno is wired directly via the abilist. The fstat wrappers use ucsan_*-prefixed custom ref names and require a per-target metadata mapping (fstat->ucsan_fstat) plus ucsan_-ref custom routing to activate; they are inert in the default configuration.
Mark the EH unwind path uninstrumented in done_abilist.txt (unwinder, personality, __cxa_throw/begin_catch, type-matching) so throws unwind; keep the alloc/free path instrumented so malloc/free stay captured. Rebuild instrumented libc++/libc++abi/libunwind; add tests/cpp_eh.cpp. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
UCSanPass: demangle scope/entry names to match C++ signatures; rebuild EH dangle stubs as passthroughs to the real libc++abi and restore the personality; use getFirstInsertionPt so BB tracing doesn't break landing pads. ko_clang links a plain libc++abi/libunwind EH runtime for ucsan-only C++; add rebuild_native.sh + CMake install to build it. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Under UC exploration a strchr/memchr result is base+index, but the string solver only models the haystack content, not the base pointer. This broke delimiter planting on UC-materialized objects: - the search result pointed into the freshly-malloc'd materialization (np) while the program's pointer stayed a UC pseudo-pointer, so p - c was garbage on replay and the planted-delimiter branch was never taken; - a match at index 0 collapsed to a NULL pseudo-pointer when the pseudo base was 0, so p != NULL failed. Fixes, for the single-char search ops (strchr/memchr/strrchr/memrchr): - ucsan_uncheck_pointer(): inverse of ucsan_check_pointer (phys_to_virt style), translating the materialized result back into the caller's UC pseudo space so p - c == index holds concretely. Driven by a new `retptrN` abilist category; UCSanPass emits the translation after the call and TaintPass propagates the (separate) symsan label through it. - the __dfsw_ wrappers stash the haystack pointer label in op2's high bits (low 8 bits remain the needle char); the solver constrains that base pointer non-null and extends the (PtrToInt(strchr) - PtrToInt(base)) simplification to the tainted (UC) base, yielding index == k instead of index - base_value == k. strstr/strpbrk/memmem keep a needle/accept pointer in op2 (used for concrete content) so they have no room to carry the pointer label and are not enabled here. tests/strchr_plant_*.c, memchr_plant_offset.c: symsan-level coverage for delimiter planting. strchr_sibling_byte.c: covers an indexof constraint conjoined with an overlapping scalar byte constraint (the haystack str-var and the per-byte scalar var are linked so the models agree). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The pipe_msg_type enum slot 3 was renamed from fsize_type to add_constraint_type in the thoroupy backend import, but symsan.cpp still referenced the old name, breaking the AFLPP mutator build. Co-Authored-By: Claude Opus 4.8 <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.
Merge UCSan as a separate Pass, enabling running SymSan and UCSan individually or combined.