[nils-loose]

What changes

Models for parsing numbers from Strings. Whether the call throws a NumberFormatException becomes a branch on the string. The visitor records it on both sides of a static call, so the solver can ask for a parseable string or for one that is not. A throw at that branch is explained by the trace, so it no longer records the context loss from 5ea26bc.

• Integer.parseInt, Long.parseLong, Short.parseShort, Byte.parseByte, valueOf(String), with or without a radix: exact for strings of any length, without pinning the length.
  • A string parses iff it is an optional sign followed by at least one digit, all but the last K digits are zeros, and the value is in range. Digits are those Character.digit(char, radix) accepts, which includes Unicode decimal digits and fullwidth letters. K is the smallest k with radix^k above the range.
  • The value is the sum over the last K digits.
  • A symbolic radix is range-checked and pinned. A radix outside 2..36 throws for every string.
  • The old models took str.to_int of the whole string. That is wrong for a sign and for non-ASCII digits.
• Float.parseFloat, Double.parseDouble, valueOf(String): whether the string parses is exact. This covers the full Double.valueOf grammar: surrounding chars up to U+0020, hex, NaN/Infinity, exponents and suffixes.
  • The value is exact for NaN, Infinity, and plain decimals without exponent or whitespace, where:
    • the digits form an integer M < 2^24 (float) or 2^53 (double);
    • there are at most 10 (float) or 22 (double) fraction digits.
  • There it is one correctly rounded fp.div of two exact operands. This is the JDK's fast path, and the JDK's result for those inputs.
  • A second branch on the returning side records whether the value is in this exact fragment. Other parseable strings give a concrete value and record precision loss.
• New class NumberParsing. The changes to IntegerInvocation/LongInvocation/ShortInvocation/ByteInvocation touch only the parse methods and valueOf(String); the toString work in another branch should merge without conflicts. FloatInvocation/DoubleInvocation gain parseFloat/parseDouble cases. The visitor reuses the String call-branch recording from Make the String and StringBuilder models sound #75 for static calls.

Measured (nosa, 300 s, --sv-comp --mem15g)

There were 114 runs:

• 34 runs in the affected set: all parse-float-unmodelled KB tasks, jbmc-regression/calc, and the other tasks calling parse*/valueOf.
• 80 random baseline-correct runs.

task	prop	base / #75	this PR
CWE369_..._float_connect_tcp_divide_01_bad	valid-assert	UNKNOWN	VIOLATION (+1)
CWE369_..._float_connect_tcp_divide_81a_bad	valid-assert	UNKNOWN	VIOLATION (+1)
CWE369_..._float_console_readLine_divide_54_bad	valid-assert	UNKNOWN	VIOLATION (+1)

+3 points vs the integration baseline and vs #75, 0 lost, 0 new wrong verdicts. The 80 regression runs are unchanged.

Known limits

• The other 15 Juliet float runs go from UNKNOWN in ~2 s to a timeout (0 points either way). Exploration now reaches strings outside the exact fragment, such as 6e0, and these record precision loss, so SAFE is out of reach. The FP queries (string → int → bv → fp.div) take seconds to minutes in Z3. I also tried to_fp from a real and an integer rounding characterisation in z3py; neither was faster. The _version2 bad variants did not find their violation within 300 s.
• jbmc-regression/calc is still UNKNOWN, now for another cause. The parse branches are explored, but the solver picks a huge size for new String[size], which ends in an OOM (uncaught-oom-huge-nondet-array).
• StringValueOf08/09 still need FP-to-String.
• Not modelled: parseUnsignedInt/parseUnsignedLong, decode, and the CharSequence range overloads. They keep the old behaviour.

Tests

NumberParsingExactnessTest (L0, 64 cases): with the string fixed to a sample, the branch holds iff the JDK parses it, and the value can only be the JDK's.

• Integers: edge strings ("", "-", "+", "2147483647", "2147483648", "-2147483648", " 1", "1 ", "0x1", "١", fullwidth digits, long and short bounds), in radix 2..36 for int and long and in a few radixes for short and byte.
• Floats: fixed samples and 400 random strings against Double.parseDouble/Float.parseFloat.

The full executor test suite passes (9452 tests).

🤖 Generated with Claude Code

[nils-loose]

Included in dev through #92 (merge commit 534c182), together with the fixes for interactions between PRs. This PR stays as the record of the change and its measured flips.