Hi,
I am a final-year Computer Science student at King's College London. As part of my dissertation, I ran coverage-guided fuzzing against Poly/ML on ARM64 using AFL++ with AddressSanitizer and UndefinedBehaviorSanitizer. I found four confirmed faults against commit dfb7e03b, all of which remain present in current upstream master. I am reporting them here with full reproducer inputs.
Finding 1 - UBSan unsigned offset overflow in arm64.cpp (CopyStackFrame)
Triggered by two completely valid SML programs. UBSan reports pointer arithmetic overflow at libpolyml/arm64.cpp (line 246 on dfb7e03b, line 440 in current master) in CopyStackFrame. The unsigned offset is divided by sizeof(PolyWord) (a size_t), causing implicit conversion to unsigned and wrapping on negative values. ARM64-specific - does not occur on x86-64.
Reproducer: seed_fun.sml (attached) - triggers in libpolyml/arm64.cpp:440 (CopyStackFrame)
Proposed fix: cast sizeof(PolyWord) to POLYSIGNED before the division. I have validated this locally and would be happy to submit a pull request if that is welcome.
Finding 2 - Unbounded memory allocation on pathological floating-point exponents (LEX_.ML)
readChars in LEX_.ML reads exponent digits after e/E in a float literal with no length bound. Since there is no upper bound, an exponent of sufficient length will exhaust available memory on any system. Reproduces without sanitisers - memory growth is linear with exponent length.
Note: upstream commit fc874893 ("Fix greedy lexing of reals with fractions") sounds related but is not - it addresses dot consumption, not the exponent path. Lines 323–331 of LEX_.ML are unchanged.
Reproducer: crash_float_9584.bin and crash_float_3136.bin (attached) - feed via poly < crash_float_9584.bin
Proposed fix: cap exponent accumulation at 20 digits and emit a lex error on overflow. I have validated this locally and would be happy to submit a pull request if that is welcome.
Finding 3 - Three faults in module elaboration (TYPE_TREE.ML, TYPECHECK_PARSETREE.sml)
Fuzzing with a module-heavy corpus found three faults in the elaborator, all reproducible without sanitisers.
Crashes 1 and 2: Nested structure seed with AFL++-corrupted identifiers. Input passes the parser and faults in the elaborator. On current upstream master these now produce an infinite hang rather than SIGSEGV, indicating the code path changed but the root cause is unresolved.
Crash 3: 80-byte reproducer:
structure Mat0=struct val 0=0 fun s0uare x=x+x fun e 0=()end;val a=Mat0.s0uare 0.0
val 0 = 0 inside a structure body is accepted by the parser without error. The elaborator then assumes the left-hand side of a val binding is always an identifier and dereferences accordingly into invalid memory. SIGSEGV confirmed on current upstream master.
Reproducers: crash_nested_1.bin, crash_nested_2.bin (crashes 1 and 2), crash_val00.bin (crash 3) - feed via poly < crash_val00.bin
I do not have a proposed fix for Finding 3 - it requires deeper understanding of the elaborator's type safety assumptions.
I am happy to provide any additional details or the full AFL++ campaign logs.
Kind regards,
Aravinth Kaneshalingam
