Float Point Support - #49
Merged
Merged
Conversation
Teach the instrumentation and the in-process z3 solver (z3-ts.cpp) to
collect and reconstruct floating-point expressions, casts, and common FP
intrinsics so branches guarded by FP arithmetic/comparisons can be flipped.
Scope is the in-process z3 flow only; the RGD/jigsaw path is unchanged.
- dfsan.h: self-defined FP ops (fp_neg/fabs/sqrt/round/min/max/copysign);
mark FP arith commutative for dedup.
- dfsan.cpp: preserve FCmp operand bit patterns (like ICmp) for solver
value validation.
- TaintPass.cpp: collect FAdd/FSub/FMul/FDiv/FRem, FNeg, FP<->int casts,
FCmp, and FP intrinsics; decompose fma/fmuladd (from -ffp-contract) into
FMul+FAdd; ClTraceFP defaults on.
- dfsan_custom.cpp/done_abilist.txt: model sqrt and other errno math
libcalls (kept as libcalls at -O0) via custom __dfsw_ wrappers.
- ko_clang.c: KO_NO_TRACE_FP off-switch.
- z3-ts.cpp: lift BV->fpa, compute, lower fpa->BV for FP nodes; FCmp
ordered/unordered predicates; FP cast handling.
- tests: fp_solving.c plus fp_challenge_{float,double}.c adapted from the
AFL test-float/test-double challenges (multi-branch, one input per check).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- fp_arith.c: add z3-only RUN lines; seed x=1.0 misses all four branches so one concolic run flips FP arith, FP->int cast, sqrt, and fabs (one input per branch). - fcmp.c: drop the fastgen RUN lines (RGD path does not model FP) and fix the check-prefix mismatch (source defined CHECK-GEN1/2 but RUN used CHECK-GEN); map the two generated inputs to the double/float equality branches. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
ko-clang defaults its next-stage compiler to plain clang/clang++, and lit.cfg prepends /usr/lib/llvm-18/bin to PATH, so the default clang is already clang-18 -- exactly what every other test relies on. Setting KO_CC explicitly was redundant; remove it for consistency. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The default clang/clang++ from llvm_bin_dir (prepended to PATH) is what the suite uses; these clang-14 overrides were dead relics from the old build. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The =functional ABI is a no-op in SymSan (WK_Functional drops the return
shadow), so math functions marked functional silently lose taint and the
solver can't flip branches that depend on them. Convert the FP predicate
and round-to-int libcalls to custom wrappers that record the real op:
isnan/isinf/__isinf/finite/__signbit -> fp_is_nan/fp_is_inf/
fp_is_finite/fp_signbit
lrint/llrint (+f variants) -> fp_lrint (RNE round -> sbv)
The long double (*l) variants and transcendentals stay functional:
our FP lifting only supports IEEE 16/32/64-bit sorts, and z3's FP
theory has no operation to invert exp/log/pow.
New self-defined ops in dfsan.h, __dfsw_ wrappers in dfsan_custom.cpp,
serialize handlers + OP_MAP names in z3-ts.cpp, and abilist entries.
Also fix a partial-function boundary bug shared by the FPToSI/FPToUI
cast handlers (and the new fp_lrint): INT64_MAX/UINT64_MAX are not
representable as doubles and round up to 2^63/2^64, outside the target
range where to_sbv/to_ubv is undefined -- the solver could pick that
point and assign the result freely, yielding an input that doesn't
satisfy the branch. Use the largest doubles strictly below the overflow
point (2^63-1024 signed, 2^64-2048 unsigned) as the closed upper bound.
Add tests/fp_libcall.c (lrint/llrint/__signbit) and tests/fp_cast64.c
(64-bit signed/unsigned FP->int cast regression). Full FP suite passes.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add KO_USE_FASTGEN=1 %fgtest RUN blocks to the FP lit tests (fcmp,
fp_arith, fp_cast64, fp_challenge_{float,double}, fp_libcall, fp_solving)
so the fastgen instrumentation + out-of-process protocol (through the
in-process z3-ts.cpp) is exercised alongside the existing KO_USE_Z3
blocks, with matching branch/output orderings.
Add driver/afltest.cpp, a standalone harness that drives the RGD
(out-of-process) solver chain -- rgd-parser.cpp + I2S/JIT/z3-solver.cpp --
via the launcher API, mirroring fgtest.cpp but for the RGD AstNode path
that previously had no lit/fgtest coverage. Register the %afltest lit
substitution and the AFLTest CMake target.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Teach the RGD (rgd::AstNode) parser and solvers to reason about floating-point constraints, so branches guarded by FP arithmetic, casts, FP libcalls, and FCmp are solvable via the AFL++ custom mutator path (not just the in-process z3-ts.cpp flow). - z3-solver.cpp: build the solver with logic QF_BVFP instead of QF_BV. Under QF_BV z3 treats the FloatingPoint sort as uninterpreted and returns spurious all-zero SAT. Add FP helpers mirroring z3-ts.cpp (bv<->fpa lifting, rounding modes, FCmp, FP casts with the to_sbv/to_ubv range constraints) and serialize the FP AstNode kinds. - rgd-parser.cpp: parse the FP op labels into AstNode kinds. - ast.h: add the FP op kinds and isFloatingPointKind([FAdd, FUne]); FP comparison kinds are kept outside isRelationalKind() so integer-only solvers reject them. - i2s-solver.cpp / solver.h: reject any constraint whose ops bitset intersects the FP range via a new fp_ops_mask. Input-to-state cannot handle bytes that reach a comparison through an FP op (e.g. (long)x==42, lrint(x)==42): the constant no longer appears literally in the input, so copying it yields a bogus solution that pre-empts z3. Reject and fall through to the FP-aware z3 solver. - jit-solver.cpp: return TIMEOUT (not ERROR) when jigsaw rejects an unsupported (FP) root so the chain advances to z3. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The AFL test-float.c/test-double.c challenges are designed for the input-to-state (i2s) solver: each guard is a DIRECT comparison of an input-derived float/double against a constant, so i2s can flip it by copying the constant's IEEE-754 bytes into the input -- no FP arithmetic reasoning / z3 required. Replace the earlier `fabs(x-mid)<half` rewrite (which forced z3 and defeated the i2s demonstration) with faithful two-sided range checks (`lo <= x && x <= hi`) and, for double, the exact-equality case (`x3 == pi`). Add %afltest RUN blocks exercising the out-of-process RGD path with i2s only (no SYMSAN_USE_Z3), demonstrating that i2s alone solves the challenge; the existing %fgtest / KO_USE_Z3 lines still confirm the in-process z3 solver. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Extend the input-to-state solver to flip a "direct" FCmp -- an input-derived float/double compared against a constant, with no FP arithmetic in between -- by writing the constant's IEEE-754 bytes (or a nextafter-adjusted value for strict inequalities) into the input, the same RedQueen trick i2s already uses for integer comparisons. - fp_ops_mask now covers [FAdd, FpLrint] (all FP arithmetic, casts, and intrinsics/libcalls) but NOT the top-level FP comparisons, so a direct FCmp falls through to the new solve_fcmp path while any FP arithmetic underneath still forces z3. - solve_fcmp decodes the i2s candidate value, identifies the symbolic operand side, computes a target via fp_i2s_target (handling all 14 LLVM FCmp predicates incl. ordered/unordered and NaN), re-decodes, and VERIFIES with i2s_eval_fcmp before committing -- guarding against bogus SAT. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Extend the input-to-state solver to flip an FCmp whose symbolic operand
passes through one FP arithmetic op against a constant -- (x op C) <cmp> K
-- by inverting the op to recover x (write K-C, K/C, ... into the input),
mirroring the integer x op C == K path (_get_binop_value_r / solve_icmp).
- Narrow fp_ops_mask to [FRem, FpLrint] and add fp_arith_mask =
{FAdd,FSub,FMul,FDiv}, so a single invertible FP binop reaches
solve_fcmp instead of being pre-rejected; FRem/FNeg/casts/intrinsics/
libcalls still fall to z3.
- solve_fcmp classifies the comparison by AST structure (is a compare
operand an arith node?) rather than by value matching -- this avoids a
false "direct" match when the arith result coincidentally equals the
raw input bytes (e.g. 0.0 * C == 0.0 on an all-zero seed).
- New precision-aware helpers fp_binop_eval / fp_binop_invert /
fp_binop_const. Only a single arith op that is a direct child of the
comparison and has a constant operand is handled; every guess is
verified end-to-end with i2s_eval_fcmp before committing, so rounding
that breaks an inversion just falls back to z3.
Add tests/fp_arith_i2s.c (FAdd/FMul float, FSub/FDiv double incl. a
const-lhs case), solved by i2s alone (%afltest, no SYMSAN_USE_Z3) plus
the in-process z3 paths.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Several libm FP functions were marked =functional in done_abilist.txt on the rationale that z3's fpa theory cannot invert them. That only applies to z3: the i2s solver computes the closed-form libm inverse for a guard f(x) <cmp> K and verifies it end-to-end, so monotonic transcendentals are exactly solvable there. Make exp/expf/exp2, log/log2/log2f/log10/log1p/log1pf, and pow/powf =custom and invert them in I2SSolver::solve_fcmp: - new op kinds FpExp/FpExp2/FpLog/FpLog2/FpLog10/FpLog1p/FpPow (ast.h, inside [FAdd,FUne] so isFloatingPointKind covers them) + runtime codes in dfsan.h + wrappers in dfsan_custom.cpp + parser mapping in rgd-parser.cpp - unary transcendentals inverted via fp_trans_invert (exp<->log, exp2<->log2, log10->pow(10,.), log1p->expm1) - FpPow is binary, reuses fp_binop_* both directions: exponent-const pow(x,C)==K -> pow(K,1/C), base-const pow(C,x)==K -> log(K)/log(C) - masks: fp_ops_mask=[FRem,FpExp), fp_arith_mask gains FpPow, new fp_trans_mask=[FpExp,FpPow) The RGD chain is i2s->jigsaw->z3 (optimistic), so z3 (z3-solver.cpp, z3-ts.cpp) and jigsaw (jit.cc) explicitly reject the new kinds. fmod, frexp*, modf, nextafter*, nexttoward*, and *l variants stay =functional (not i2s-invertible). Real FP support in jigsaw is left for a future task. New test tests/i2s_transcendental.c (%afltest only -- only i2s inverts transcendentals) covers all 8 forms. Note LLVM's optimizePow rewrites pow(x,2.0)->x*x and pow(2.0,x)->exp2(x) even at -O0, so the test uses a cube exponent and base 3.0 to keep the pow libcall. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The out-of-process RGD chain runs i2s -> jigsaw -> z3, but jigsaw was integer-only: codegen threw on every FP node and addFunction's root gate only accepted integer relational kinds, so FP-rooted constraints fell straight through to z3. FP guards that i2s cannot invert (two symbolic operands, e.g. x*x > 25.0, or an intrinsic like sqrt) thus skipped jigsaw entirely, even though their distance is perfectly measurable for gradient descent. jit.cc: add as_fp/as_bits helpers (FP node values are integers holding IEEE bits) and codegen for every measurable FP kind -- arith, casts, intrinsics, FpRound (rounding mode in index()), transcendentals (llvm.* / libm calls resolved from the solver process; log1p via a direct libm call), FpPow, and FP comparisons (operands FPExt'd to double, stored at arg[0]/arg[1]). Extend the addFunction root gate to accept isFPRelationalKind. The four boolean predicates (FpIsNan/FpIsInf/FpIsFinite/FpSignbit) stay rejected -- a bit, not a magnitude -- and fall back to z3. gd.cc: get_distance dispatches isFPRelationalKind to fp_get_distance, which reinterprets the operands as doubles, computes a non-negative distance d (0 iff satisfied), and returns its IEEE bit-pattern (monotonic in d for d>=0, exactly 0 iff d==0). Strict predicates nudge by DBL_TRUE_MIN at the a==b boundary, mirroring the integer sat_inc(a-b,1). tests/jigsaw_fp.c: 6 inequality branches (FMul/FAdd/FpSqrt/float/FNeg/FpMin) that i2s cannot solve; %afltest + SYMSAN_USE_JIGSAW=1 without SYMSAN_USE_Z3 to isolate jigsaw. GD solves inequalities well but not exact FP equality (that remains z3's job). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
try_i2s now snaps raw input chunks onto FP comparison operands for exact FP equalities gradient descent cannot hit (two symbolic operands, e.g. x==y+1.0). Because an i2s candidate is a maximal run of consecutive symbolic bytes, two adjacent FP operands merge into one oversized run, so the FP branch slides an FP-sized window (8 then 4) across each run rather than requiring the whole run to be exactly 4/8 bytes. Each window promotes float->double, matches against the stored (double-bit) operands, snaps via get_i2s_fp_value (ULP-nudge for strict inequalities), and verifies with try_new_i2s_fp_value (fp_get_distance == 0) before committing. try_new_i2s_fp_value seeds all args from the current input and overrides only the window bytes, so the other symbolic operand is not clobbered (unlike the integer try_new_i2s_value, which broadcasts the value across the whole local_map). Test tests/jigsaw_fp_i2s.c: three adjacent-double equalities (add/sub/reversed operand), isolated with SYMSAN_USE_JIGSAW=1 and no z3; standalone i2s solves none. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The FP arith/trans/direct structural checks in solve_fcmp matched candidates by VALUE only, which two operands holding coincidentally-equal values could fool. For `X == Y op C` on a seed where X == Y, feeding X through `op C` produces the same value as `Y op C`, so the X candidate (which sorts first) passed the check and the inverted result was written to X -- corrupting an unrelated input and leaving the guard unsatisfied. A Read node's index() is its input byte offset, so anchor each candidate to the offset the intended operand actually reads: arith/trans require the candidate offset to equal the symbolic operand's Read offset; direct compares require the matched side's Read offset. When the operand is not a plain Read (transformed input, offset not determinable) fall back to the value-only check to preserve behavior. This also rejects the adjacent-float misdecode (an 8-byte run holding two floats no longer matches a double operand at the run start). Regression test tests/fp_i2s_offset.c: `X == Y op C` guards with X and Y non-adjacent; pre-fix the inverted value was written to X (output Bad), now it is written to Y (guards flip). Solved by standalone i2s, %afltest only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Item 1: rescale jigsaw's FP distance so a mixed FP+integer task converges. fp_get_distance previously returned the raw IEEE bit-pattern of |d|, which is ~2^62 for an O(1) distance -- far larger than typical integer distances, so the FP term dominated (and sat_inc could saturate) the summed per-constraint distance in gd.cc. Shift the bit-pattern down by 32 bits: an O(1) distance now maps to ~2^30 and the whole finite range stays below 2^31, comparable to integer distances, while preserving both GD requirements (still monotonic in d, still 0 iff d==0) and the log-like wide dynamic range (exponent -> octave resolution, retained high mantissa bits -> within-octave resolution). Item 3: fix the same value-only coincidental-offset bug in solve_icmp that solve_fcmp already had. The direct-match branch matched candidates by value alone, so on a seed where two symbolic operands share a value (e.g. `b + 1 == a` on an all-zero seed) it wrote the inverted result to the wrong input. Anchor each direct match to the compared side's Read offset (mirrors solve_fcmp); a non-plain-Read side falls back to the value check and is handled by the binop branch. New regression test tests/i2s_offset.c (integer analogue of fp_i2s_offset.c) fails pre-fix, passes post-fix. All 96 git-tracked lit tests pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Differential testing jigsaw (JIT+GD) against z3 on the SMT-COMP QF_BV sat-labeled set (14,685 files, every SAT model validated by z3) surfaced two pre-existing soundness bugs where jigsaw returned a model z3 rejects. Both affect real fuzzing, not just the smttest driver. 1. Over-width shift / divide-by-zero. codegen() emitted raw LLVM shl/lshr/ashr (poison for amount >= width; the JITed x86 shift also masks the count) and a divisor=1 div-by-zero hack. SMT-LIB2 defines all of these (shift >= width -> 0 / sign-fill; bvudiv x 0 -> ~0; bvurem/bvsrem x 0 -> x; bvsdiv x 0 -> x>=0?~0:1), and SymSan's z3 backends already model SMT semantics -- so jigsaw disagreed with its own oracle. Route these through new helpers (build_shl/lshr/ashr/udiv/sdiv/urem/srem, nonzero_divisor) that implement the SMT-LIB result by default (JIGSAW_SMTLIB_SEMANTICS); define JIGSAW_HW_SEMANTICS to keep the legacy C/C++/hardware behavior instead. 2. Signed comparison sign-extension. The ICmp codegen zero-extended both operands to i64 before storing them for gd.cc get_distance, which does (int64_t)a </<= (int64_t)b. A negative sub-64-bit value (e.g. i32 0xFE000000) zero-extends to a large positive i64, giving the wrong signed distance and an unsound SAT. Sign-extend the operands for the signed kinds (Slt/Sle/Sgt/Sge); unsigned/Equal/Distinct stay zero-extended. After both fixes the QF_BV sat run reports 0 soundness violations (4,958 models z3-validated, 4 trivially-sat with no free vars), down from 3 unsound before. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…olver
smttest reads an SMT-LIB2 file, translates each assertion to NNF then DNF (one
rgd::SearchTask per disjunct), and drives the RGD chain (i2s excluded as unsound
for conjunctions; jigsaw JIT+GD; optional z3) directly -- no target execution,
launcher, or trace parser needed. This is the differential-testing harness used
to validate jigsaw against z3 on the SMT-COMP QF_BV set.
* driver/smttest.cpp -- the front-end (SMT-LIB reader, DNF translator,
SearchTask builder, solver loop) with per-phase timing (parse/codegen/jit/
gd/solve/total, microseconds) behind --time / SMT_TIME.
* driver/CMakeLists.txt -- SMTTest target (installed as `smttest`).
* include/solver.h -- public JITSolver timing accessors
(get_codegen_time / get_jit_time / get_solving_time) that --time reports.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The input-to-state pass only touched unsatisfied constraints and committed only on strict global improvement. For the SAGE byte-assembly pattern (X == (b3<<24)|(b2<<16)|(b1<<8)|b0 coupled with X == const), the all-zero seed leaves X==assemble satisfied (skipped) and X==const unsatisfied. Snapping X=const breaks X==assemble by exactly the amount it fixes X==const, so the global distance is unchanged, the strict-improvement gate reverts the snap, and the assembly bytes are never eligible -> deadlock. Iterate try_i2s to a bounded fixpoint (I2S_MAX_ROUNDS=8), additionally accepting lateral (equal-distance) snaps that shift which constraints are satisfied. A later round then sees X==assemble newly-unsatisfied and snaps b0..b3 to a strict improvement. distance() already refreshes the compare operands live each call, so re-targeting across rounds works. The round cap guarantees termination if lateral snaps cycle. Validated by z3-checked A/B (3 runs each, JIGSAW_I2S toggle, over 6,636 files: 4,962 previously-solved + 1,674 GD-declined): 0 unsound models in either config; mean single-run solved 4,966 -> 4,997, stable (all-3-runs) 4,769 -> 4,841, gains concentrated in the sage family. Also adds a JIGSAW_DEBUG trace of which phase (i2s vs gradient descent) solved a task. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Two latent bugs in the gradient helper: * Grad::clear() iterated `for (auto gradu : grads)` by value, so it zeroed copies and left the real vector untouched. Benign today only because cal_gradient fully overwrites every entry after the restart-loop clear(), but a trap for any future reader. Iterate by reference. * Grad::val_sum() used a plain `ret += gradu.val` (its own //FIXME noted the missing saturating add). On overflow, descend's initial guess_step (f0 / val_sum) becomes garbage. Saturate to UINT64_MAX on overflow, matching sat_inc's convention. Also switch max_val()'s read-only loop to by-reference to avoid copying each GradUnit in the hot `while (grad.max_val() == 0)` restart loop. No search-outcome change (clear() was already masked; overflow is an edge case); pure correctness + throughput. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
partial_derivative does not restore the input between delta probes, so `update(index, dir, delta)` added delta *cumulatively* -- the probe walked orig+1, orig+5, orig+21, orig+85... instead of the intended orig+delta the "if f(x+delta) == f(x)" comment describes. The plus/minus finite differences were therefore measured at drifted, asymmetric offsets, giving noisy gradient signs/magnitudes. Track the accumulated offset and add only the increment (delta - added) so each probe lands exactly at orig+delta -- a clean finite difference. Same number of evaluations (no restore/reprobe), so throughput is unchanged; only the probe point is corrected. z3-validated A/B (JIGSAW_CLEAN_DELTA toggle, since removed; 3 runs each over 6,636 files): 0 unsound in both configs; per-run mean solved 4,987 -> 5,022, union-of-3 ceiling 5,137 -> 5,169 (genuinely new files, not just reliability), stable(all-3) 4,834 -> 4,857. Gains (83) outweigh regressions (51), both sage-dominated -- real signal, not restart noise. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Two throughput-oriented GD search improvements, validated together by a z3-checked A/B (2x2, skip x backtrack, 3 runs each over 6,636 files): #4 cal_gradient: skip bytes touching no currently-unsatisfied constraint. Their partial derivative is definitionally 0 (a byte feeding only satisfied distance-0 constraints cannot lower f0, only keep it 0 or raise it), so partial_derivative would burn ~16 probes just to conclude val=0. Skipping yields a bit-identical gradient while reclaiming that budget for the MAX_EXEC_TIMES-capped search. Standalone: mean 5007->5024, union 5161->5169, stable 4850->4869, 0 unsound, faster wall-clock. #5 descend: on line-search overshoot (f grew between step/2 and step), bisect up to BACKTRACK_MAX times back toward the last-good point along the same gradient instead of abandoning the jumped-over minimum. Negative in isolation (net -13: pure added probes), but the budget #4 frees funds it: combined "both" config beats baseline on every metric -- mean 5027, union ceiling 5182 (+21), stable 4872 (+22), 0 unsound -- and adds +13 ceiling files over skip-alone. Default-on rebuild reconfirmed: 5044 z3-valid, 0 unsound. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The signed-compare SExt fix (commit ab770de) made jigsaw's JIT'd comparison function sign-dependent: signed kinds (Slt/Sle/Sgt/Sge) sign-extend operands to 64-bit, unsigned/equality kinds zero-extend. But the function-reuse cache never accounted for this -- isEqualAstRecursive treats every relational kind as interchangeable, and jit-solver's fCache keys on it (make_constraint also hashes all relational roots to Bool). So a signed comparison could reuse an already-compiled unsigned (zero-extending) function over identical operands. get_distance then applied its signed (int64_t) cast to a zero-extended operand, so a sub-64-bit negative value looked positive -> unsound SAT. Reproduced on sage/app9/bench_824.smt2: (bvsle 0 (bvshl T4_482 3)) with the shift result 0x9b545ff0 (signed-negative) was reported satisfied. Fix: add isSignedRelationalKind (Slt..Sge) and require signed==signed in isEqualAstRecursive, keeping signed and unsigned comparisons in separate JIT-reuse classes. Equal/Distinct stay with the unsigned group (sound, since the JIT zero-extends them). Also harden the compare-operand extend to SExtOrTrunc/ZExtOrTrunc -- bare SExt/ZExt would assert on 64-bit operands. Validated on the full 6636-file QF_BV set (seed 1, config all): 0 sat,invalid at budget 1000 AND 10000 (the 1000 cap had been masking the bug); budget 10000 now safely yields +260 solves. All FP/core lit tests pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Bump MAX_EXEC_TIMES 1000 -> 10000. A full-set QF_BV sweep (seed 1, 6636 files) showed the attempts-to-solve distribution has a long tail: the higher cap recovers ~97% of the budget-limited solves (+260 on the set) then plateaus, and is nearly free for the common case since most tasks solve well under 1000 attempts and stop early. Overridable at runtime via JIGSAW_MAX_EXEC (smttest --budget) through the new jigsaw_max_exec() helper. This is now safe to raise only because the signed/unsigned JIT-reuse soundness bug it exposed (bench_824) was fixed in 2c0fbd7. Consolidate the search-strategy work (near-miss jitter + descend- stagnation escape via do_escape) and gate ALL of jigsaw's diagnostic scaffolding behind a single compile-time switch, JIGSAW_SEARCH_DEBUG (config.h, default 0): the phase/solve tracing (JIGSAW_DEBUG, JIGSAW_REPORT_ITERS), the step tracer (JIGSAW_TRACE / JIGSAW_TARGET), and the A/B strategy toggles (JIGSAW_NO_JITTER / JIGSAW_NO_STAGNATION / JIGSAW_STAG_RESTART). Production builds carry none of these runtime getenv branches in the hot search loop -- g_trace/no_jitter/no_stag/stag_restart become constexpr false and fold away -- and always use the winning strategy (flat-loop + stagnation escape with jitter on). Set the macro to 1 to reproduce the strategy experiments. Validated: full 6636-file set, seed 1, 0 sat,invalid; bench_824 solves soundly at the default budget; all FP/core lit tests pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
MutInput seeded its restart PRNG from time(NULL) (1s granularity) on the non-JIGSAW_SEED path, so parallel fuzzing workers -- and the two MutInputs per solve -- constructed in the same second shared an identical restart stream, killing random-restart exploration diversity. Production path now mixes CLOCK_MONOTONIC nanoseconds, a monotonic counter, and the instance address so no two constructions collide. The JIGSAW_SEED branch stays deterministic (base + counter) so smttest --seed A/B remains reproducible. Sound + throughput-neutral (1500-file mixed QF_BV/FP/BVFP z3-differential sweep: 0 unsound). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
smttest's parser silently dropped the rounding-mode operand of (fp.add rm a b) etc., so directed-rounding benchmark arithmetic was computed as round-to-nearest -- leaving the wintersteiger directed-rounding cluster unsolved and a latent benchmark-soundness gap. Carry the SMT-LIB rounding mode through the RGD AST and JIT rounding-mode-correct arithmetic. - smttest: fp.add/sub/mul/div + fp.sqrt carry the rm selector in index(), folded into hash() so fCache never reuses wrong-mode compiled code (isEqualAstRecursive ignores index()). FpRound hash retrofit too. rna is rejected on arithmetic: x86 MXCSR can't represent it, and the runtime leaves index()==0 on arith to mean "RNE default" (0/1 both == RNE). - jit.cc: detect_fp_mode() finds the formula's single FP mode. A directed mode (rtp/rtn/rtz) sets StrictFP + constrained-FP builder + llvm.set.rounding (MXCSR) at entry, restores RNE before the ret, and emits CreateConstrainedFPBinOp / constrained.sqrt (so the opt passes constant-fold in the chosen mode, and runtime-symbolic ops round via MXCSR). Mixed modes return -1 -> jigsaw bails, driver falls to z3. RNE/no-FP path unchanged. A Phase-0 feasibility spike is kept behind smttest --spike-fp-rounding. - z3-solver.cpp (RGD path): get_arith_rm() (0/1->RNE, else raw) for FAdd/FSub/FMul/FDiv/FpSqrt. - z3-ts.cpp (runtime union-table path): no functional change -- its op1/op2 are operand values, not an rm, and instrumented code always emits RNE fadd; documented why RNE is correct there. Validation (0 unsound mandatory, every model z3-checked against the true rm): 2379/2890 recorded-failure directed files now solve+validate (82.3% net-new); 360 directed + 120 RNE-regression + 550 broad QF_FP/QF_BVFP sweeps all 0 unsound; FP lit 11/11; mixed-mode bail proven correct. Mixed-mode rate on wintersteiger is 0%, so single-mode-first loses nothing. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Directed FP rounding now flows through the real symex path, not just the SMT-LIB benchmark path. LLVM carries rounding in llvm.experimental.constrained.* intrinsics (emitted under strict FP / FENV_ACCESS, e.g. code calling fesetround, including the common round.dynamic case), but TaintPass blanket-filtered all llvm.experimental.* and dropped the taint before it reached the union table. - TaintPass.cpp: capture constrained fadd/fsub/fmul/fdiv/sqrt/fmuladd and constrained fcmp/fcmps before the experimental filter. The rounding selector is packed into the high byte of `op` (the slot cmp uses for its predicate; FP arith carries no predicate). Static modes pack a constant; round.dynamic reads the live MXCSR via @llvm.get.rounding and maps FLT_ROUNDS -> selector at runtime. fcmp/fcmps are modeled as a regular FCmp (predicate in high byte) so strict-FP branches keep their taint. - rgd-parser.cpp / z3-ts.cpp: read the selector from op's high byte for FP arith and sqrt (get_arith_rm: 0/1 -> RNE, 2/3/4 directed). Fold the selector into the node hash so fCache never reuses wrong-mode compiled code (isEqualAstRecursive ignores index()); also retrofits the pre-existing fp_round floor-vs-ceil hash-collision hazard. - dfsan.cpp / dfsan.h: mask op to the base opcode (op & 0xff) in the op1/op2 symbolic-operand zeroing and in is_commutative, so packed FP-arith ops behave like their unpacked counterparts (dedup parity, commutativity). Validated end-to-end (0 unsound) with a rounding-discriminating exact-equality test (target = RTN(x*3) bits, 1 ULP below RNE): the solver recovers the exact input that HITs a strict-FE_DOWNWARD oracle while an RNE model would MISS, via all three consumers (fgtest/z3-ts, afltest RGD+z3, afltest RGD+jigsaw-JIT). FP lit suite 11/11. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adds tests/fp_rounding.c, exercising the real-symex instrumentation path
for constrained FP intrinsics: -frounding-math + FENV_ACCESS ON lowers a
symbolic square to @llvm.experimental.constrained.fmul with round.dynamic,
which TaintPass now captures (rm selector packed in the op high byte) and
the solvers honor.
The guard is x*x == 0x40488000000000ab (== RTN(x*x) for the solution, one
ULP below the round-to-nearest square). This has teeth by construction:
* two symbolic operands (x*x) => i2s cannot invert it, so its
re-execution-based (rounding-agnostic) solve can't mask a regression;
* an exact FP equality => jigsaw gradient descent cannot land it;
* x*x == target is SAT under round-toward-negative but UNSAT under
round-to-nearest (verified with z3) -- so a solver that drops the
captured rounding mode finds it UNSAT, emits no input, and CHECK-GEN
fails. Confirmed by forcing RNE in z3-ts (branch became not solvable).
Covers all consumers: fgtest/z3-ts, afltest RGD+z3, afltest RGD+jigsaw-JIT,
and KO_USE_Z3 in-runtime z3. Generated inputs re-validated against the
-frounding-math oracle (must print HIT).
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.
Adding support for collecting and solving fp constraints.