Float Point Support - #49

Merged

ChengyuSong merged 27 commits into

mainfrom

Jul 26, 2026

Commits on Jul 23, 2026

Add floating-point solving support (in-process z3 solver)

ChengyuSong
and
claude
committed
d177a68
tests: make fp_arith.c and fcmp.c lit-testable

ChengyuSong
and
claude
committed
482bae3
tests: drop redundant KO_CC=clang-18 from FP tests

ChengyuSong
and
claude
committed
ed2f7eb
tests: remove stale commented KO_CC=clang-14 lines from lit.cfg

ChengyuSong
and
claude
committed
519965b
Model FP predicate/rounding libcalls; fix FP->int cast boundary

ChengyuSong
and
claude
committed
dc5bdbc
tests: add fastgen RUN blocks and RGD-path harness (afltest)

ChengyuSong
and
claude
committed
c2f44ff
rgd: floating-point support in the out-of-process solver path

ChengyuSong
and
claude
committed
fad8664
tests: restore fp challenges to direct-comparison (i2s-solvable) form

ChengyuSong
and
claude
committed
6ab3b69
i2s: heuristically solve direct FP comparisons (solve_fcmp)

ChengyuSong
and
claude
committed
b1f9660

Commits on Jul 24, 2026

i2s: invert single FP arith-with-constant in solve_fcmp

ChengyuSong
and
claude
committed
6370aa5
feat(fp): invert exp/log/pow transcendentals with i2s

ChengyuSong
and
claude
committed
4ca66ec
jigsaw: add floating-point support (JIT + gradient descent)

ChengyuSong
and
claude
committed
be611e2
jigsaw: extend in-solver i2s heuristic to floating-point comparisons

ChengyuSong
and
claude
committed
1e07625
i2s: anchor FP solve_fcmp candidates to the operand's Read offset

ChengyuSong
and
claude
committed
6ca2846
Close out jigsaw FP distance rescale + solve_icmp offset anchor

ChengyuSong
and
claude
committed
068b1db
jigsaw: fix two unsound-SAT bugs (over-width shift/div0, signed compare)

ChengyuSong
and
claude
committed
ab770de
driver: add smttest, a standalone SMT-LIB2 front-end for the jigsaw solver

ChengyuSong
and
claude
committed
246cbe2
jigsaw: iterate i2s to a fixpoint with lateral moves for byte-assembly

ChengyuSong
and
claude
committed
6d5436e
jigsaw: fix Grad::clear() no-op and val_sum() overflow

ChengyuSong
and
claude
committed
e26bd31
jigsaw: clean finite-difference probes in partial_derivative

ChengyuSong
and
claude
committed
1d179f4
jigsaw: skip irrelevant bytes + backtrack overshoot in gradient descent

ChengyuSong
and
claude
committed
31f5195

Commits on Jul 25, 2026

jigsaw: fix signed/unsigned JIT-function-reuse collision (unsound SAT)

ChengyuSong
and
claude
committed
2c0fbd7
jigsaw: raise default budget to 10000 and macro-guard search diagnostics

ChengyuSong
and
claude
committed
f5c901f

Commits on Jul 26, 2026

jigsaw: decorrelate restart PRNG across parallel workers

ChengyuSong
and
claude
committed
d4230ff
jigsaw: rounding-mode-correct FP arithmetic (SMT-LIB directed rounding)

ChengyuSong
and
claude
committed
c93b2a0
fp: capture constrained-FP rounding modes in real-symex instrumentation

ChengyuSong
and
claude
committed
0636374
test(fp): lit test for directed-rounding capture + solver rounding model

ChengyuSong
and
claude
committed
4bd0fb7