[nils-loose]

Stacked on #70 (feat/bitop-models); base is that branch.

What changes

• Integer/Long toString(x, radix) and toUnsignedString(x, radix) are modelled exactly (new NumberStrings).
  • A radix outside 2..36 falls back to 10, as in the JDK.
  • Constant radix up to 10: the digit string is str.from_int of the integer that has the same decimal digits. Power-of-two digits are bit fields; the other radixes use a chain of divisions by the constant radix.
  • Radix above 10: per-digit characters, with the leading zeros cut. 16 and 32 keep the encoding from Exact Integer/Long/Double bit-op models and radix-2^k string conversions #70.
  • Symbolic radix: it is pinned to its concrete value by choice branches. This is a binary search over 2..36 on the normalised radix, 5 to 6 branches. On each path the conversion therefore has a constant radix, and the explorer reaches the other radixes by flipping the branches.
  • I also tried encoding the radix choice inside the formula (an ite over the radixes). It is exact too, but no Z3 query on it finished within 90 s, not even for radix 10.
• toBinaryString / toOctalString divergence (Exact Integer/Long/Double bit-op models and radix-2^k string conversions #70): these now use the same str.from_int encoding.
  • The cause was the old encoding: a concatenation of per-digit str.from_code strings, cut to a symbolic length. On it Z3 4.14 returns models that violate the constraint, or needs 13 to 64 s.
  • With the from_int encoding, the same query (toBinaryString(x) == "11000111010111") takes 0.03 s. Long.toBinaryString no longer times out.
• Number concatenation:
  • invokedynamic makeConcatWithConstants (DynamicInvocation) and StringBuilder.append(I/J/...) both go through Value.asStringValue().
  • IntValue was already exact. LongValue and ShortValue used str.from_int of the signed value, which is "" for a negative number; they now use NumberStrings.decimal.
  • No change in StringBuilderValue, StringValue or StringInvocation.
• Float/Double: asStringValue returns the concrete String.valueOf string. Before, it threw NotImplementedException, which ended the run even for concrete values (e.g. the "pi2_hi = " + pi2_hi in the MathSin constructor). A symbolic value records context loss. I found no exact encoding of the shortest decimal representation that would cover a useful range, so Float/Double.toString stay unmodelled (context loss as before).
• Choice-branch infrastructure: the files are identical to Model symbolic-index accesses to object arrays instead of recording precision loss #69 (BranchElement/BranchDTO/SymbolicTraceHandler.addChoiceBranch, the explorer's choice flag and the SA-walk masking), so the two PRs merge cleanly.
• Explorer branch order: SVCompDriver.solve_candidates now solves choice branches after the program's own branches (a stable sort, so DFS order otherwise). Without this, the explorer enumerated all radixes before it tried the equals branch, and the radix tasks timed out.
  • This also changes the order for Model symbolic-index accesses to object arrays instead of recording precision loss #69's array-index choices.

Measured

Config: --sv-comp, 300 s, 15 GB, no SA. 333 runs:

• 38 affected runs (KB causes context-loss-number-to-string, fp-to-string-not-implemented);
• 235 baseline-correct runs in the touched code paths (autostub Integer/Long/Short/Byte/Double/Float/String/StringBuilder, and every task whose sources call toString/valueOf/append or concatenate strings);
• 60 random baseline-correct runs.

comparison	gained	lost	net	new wrong verdicts
vs integration baseline	+17	0	+17	0
vs feat/bitop-models (#70)	+11	0	+11	0

Flips over #70 (all UNKNOWN or timeout to correct):

task	prop	#70	this PR
Integer.toBinaryString(int)	valid-assert	unknown (divergence)	violation (+1)
Long.toBinaryString(long)	valid-assert	timeout	violation (+1)
Integer.toString(int, int)	valid-assert	unknown	violation (+1)
Long.toString(long, int)	valid-assert	unknown	violation (+1)
Integer.toUnsignedString(int, int)	valid-assert	unknown	violation (+1)
Long.toUnsignedString(long, int)	valid-assert	unknown	violation (+1)
float-nonlinear-calculation/MathSin	valid-assert	unknown	violation (+1)
jbmc-regression/StringValueOf01	valid-assert	unknown	safe (+2)
jbmc-regression/StringValueOf01	no-runtime-exception	unknown	safe (+2)

The other 6 runs of the +17 come from #70 itself (toHexString, toOctalString, toUnsignedString(x)).

Tests

• NumberStringsSpec:
  • Integer/Long toString/toUnsignedString against the JDK on edge values (MIN, MAX, 0, -1, ...), for every radix 2..36 and for -1, 0, 1, 37, MIN and MAX;
  • the one-argument variants, plus Short/Byte.toString;
  • the concatenation string of int/long/short;
  • concrete float/double.
• RadixChoiceAgentSpec (forked agent) checks the choice branches for radixes 36, 0 and 2.
• test_solver_rlimit has a new case for the branch order.
• Executor test: 8819 tests, 0 failures.

Known limits

• Slow radixes: constant radixes other than 2^k and 10 (3, 5, 6, 7, 9, 11..36 except 16 and 32) are exact but slow in Z3: 2 to 30 s for a single equality.
• Float/Double.toString, valueOf and toHexString of a symbolic value are still context loss; the 8 autostub runs stay UNKNOWN.
• Many paths: a SAFE proof over a symbolic radix explores up to 35 radix paths per call.

🤖 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.