[nils-loose]

Builds on #75. It models the String, StringBuffer and Character methods that #75 still left unmodelled. Each new model is exact. Where an exact model is impractical, the call stays unmodelled, so it records a context loss.

What changed

StringBuffer

• StringBuffer is shadowed by StringBuilderValue, with the same models. This covers new, values recovered from the heap, and StringBuffer arguments of String/StringBuilder methods.

Ignore-case comparisons (CaseMapping)

• equalsIgnoreCase against a concrete string without surrogates is a regular expression: at each position, the chars with the same key toLowerCase(toUpperCase(c)) as the concrete char. The key is tabulated from the running JVM. The model is exact for all chars, and Boolean.parseBoolean uses it too.
• Two symbolic strings are handled for equalsIgnoreCase, regionMatches(true/symbolic, ...) and compareToIgnoreCase:
  • The call's branches first split on equal lengths and on the region bounds, then pin the lengths, then split off the ASCII strings.
  • ASCII strings are then compared char by char.
  • Strings that are not ASCII are not modelled.
• The previous equalsIgnoreCase UF is removed. It added "every char is printable ASCII" as a global constraint (an input restriction, unsound for SAFE), was cut at 50 chars, and its table was only added to the first trace.

Regular expressions (JavaRegex)

• matches(regex): a concrete regex of the simple kind becomes an SMT regex. The simple kind is literals, escaped metacharacters, positive classes ([a-z], \d, \s, \w), groups, |, and the greedy and reluctant quantifiers. These atoms never match a surrogate, so the char-level SMT semantics equal Java's code-point semantics.
• The translator rejects everything else (., negated classes, anchors, back references, possessive quantifiers, flags, ...), and such a call stays unmodelled.
• replaceFirst with a literal regex and replacement is str.replace, which is exact.
• replaceAll with a literal regex is Make the String and StringBuilder models sound #75's replace, which records precision loss.

Other models

• codePointAt, codePointBefore and codePointCount, with their index checks (codePointCount pins the range length).
• repeat, with the count >= 0 check and count pinned.
• String.join(delimiter, array), and String.valueOf of a StringBuilder or of null.
• new String(char[], offset, count), with its bounds check and pins.
• StringBuilder.reverse of symbolic chars, by the pinned length, with Java's restoration of surrogate pairs.
• Character.digit with a symbolic radix, and Character.forDigit.

StringCallBranches

• A branch is now either a check, where the call throws if it fails, or a split, where both sides return.
• Before, a split that did not hold was read as "returned normally although a check failed", and the call recorded no branches. Sibling traces then disagreed on the branch at the same depth (Branch id's dont match in the explorer).

Measured

Config: nosa, sv-comp.cfg, 300 s, mem15g. 1168 runs:

• 215 runs with the KB causes;
• 866 baseline-correct runs of tasks whose sources use the touched methods;
• 70 random baseline-correct runs, plus Make the String and StringBuilder models sound #75's 17 reruns.

The base is #75's final results, plus 12 KB runs that #75 had not measured; I ran those on #75's jar.

	runs gained	runs lost	points	new wrong verdicts
vs #75	17	0	+24	0
vs baseline	50	0	+76	0

task	prop	#75	new	pts
securibench Aliasing5, Basic10, Basic15 (StringBuffer)	both	unknown	safe / violation	+9
jbmc StringConstructors01 (new String(char[], int, int))	both	unknown	safe	+4
jbmc StringConstructors04	both	unknown	safe / violation	+3
jbmc Validate02 (matches)	NRE	unknown	safe	+2
autostub equalsIgnoreCase (was a timeout), regionMatches(boolean, ...), compareToIgnoreCase	valid-assert	unknown	violation	+3
autostub Character.digit(char, int), digit(int, int), forDigit	valid-assert	unknown	violation	+3

Tests

• StringCaseRegexModelExactnessTest (L0, about 1300 cases) is in Make the String and StringBuilder models sound #75's style: symbolic strings and ints whose concrete values are the sample, with the call's branches as they hold for the sample. With the variables fixed to the sample, only Java's result is admitted.
  • It covers all the models above, including ß, İ, ı, ſ, µ, ÿ, title-case and Georgian chars, Kelvin-like case classes, surrogate pairs and lone surrogates.
  • It checks that the untranslatable regexes are rejected.
  • It checks Character.digit(c, r) == (digit(c, 36) < r ? digit(c, 36) : -1) for every char and radix.
• StringModelExactnessTest passes. One case now uses an unmodelled insert instead of reverse, which is modelled.

Known limits

• Symbolic toLowerCase/toUpperCase stay unmodelled, as a context loss. I tried three exact encodings:
  • The Unicode case tables unrolled per char: Z3 times out even on simple queries.
  • seq.map/seq.foldl: hangs, and once gave an unsound model.
  • ASCII unrolled by a pinned length: the search reached hardly any other length, and the securibench violations Make the String and StringBuilder models sound #75 finds were lost. Unrolled up to a bound instead, a query took seconds.
• Ignore-case comparisons of two symbolic strings that are not ASCII stay a context loss. That is why StringCompare03 (NRE) is still UNKNOWN.
• split, chars(), codePoints() and StringTokenizer are not modelled.
• An extra string constraint before an index check can make Z3 hang on the int2bv of a free str.len. I saw this on securibench Inter10 during development, with the ASCII split before the pin. This is why the pins come first.

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