[nils-loose]

Since afbd1db, constraints over String inputs no longer count as precision loss, so every String model is trusted for SAFE. Several models were not exact (review of #65, B3). This PR makes them exact, or records precision loss or context loss where an exact model is impractical.

What changed

String models (StringValue)

• indexOf(int ch[, from]) searches for the char, or for the surrogate pair of a supplementary code point. It no longer searches for the decimal digits ("97"). A ch that is no code point gives -1.
• lastIndexOf(int ch[, from]): a ch that is no code point gives -1, also when ch is symbolic. The char is pinned (see below), because the window encoding with a symbolic char was too hard for Z3.
• startsWith(prefix, toffset) is false for an offset out of range, and its concrete result now uses the offset.
• replace keeps the ten nested first-occurrence replaces and records precision loss. That encoding is inexact beyond ten occurrences, for an empty target, and when the replacement contains the target. str.replace_all was tried: Z3 gave up or hung on queries the nested form solves (securibench/Basic5 went from VIOLATION to timeout).
• equals is true only for a String argument: false for null, not modelled for others. The old model made "ab".equals(sb) true and "null".equals(null) true.
• getChars writes from dstBegin, not from dstBegin + srcBegin. toCharArray("") returns an empty array.
• New models: subSequence, contentEquals, new String(), new String(char[]) and new String(StringBuilder). Other constructors return a PlaceHolder, which records a missing invocation and a context loss when the argument is symbolic. Before, they silently kept "".
• contains also accepts a StringBuilder argument.
• Long and Short values keep their sign when converted to a String. str.from_int gives "" for a negative number.

StringBuilder model (StringBuilderValue)

• The content is replaced on every change, never changed in place. It was mutated in place, which also changed the String the builder was made from.
• Bugs fixed:
  • substring truncated the builder and took end chars instead of end - start.
  • replace(start, end, str) replaced the first occurrence of the range's contents instead of the range.
  • indexOf(str, from) ignored from in its concrete result.
  • setLength was exact only for the concrete length of the content.
• New models:
  • append/insert of an Object, a CharSequence, null, a double or a float (concrete only);
  • setCharAt, getChars, appendCodePoint, compareTo, subSequence;
  • reverse (concrete content only);
  • ensureCapacity/trimToSize;
  • capacity() while it is the constructor's value.
• A builder with symbolic content is now symbolic, so a method that is not modelled records a context loss. Before, isSymbolic was always false.
• After a change that is not modelled, the content is unknown. Every method then returns a PlaceHolder until the builder is recovered from the heap, where it takes the concrete content.
• The consistency check of that recovery compared a String with a StringBuilder, so it always failed and halted the executor. It now compares the chars.

Branches inside library calls (StringCallBranches, visitor)

• Index checks:
  • Covered methods: String.charAt, substring, subSequence and getChars, and the index methods of StringBuilder (charAt, setCharAt, deleteCharAt, delete, replace, insert, substring, setLength, getChars, appendCodePoint, append(CharSequence, int, int)).
  • Each check is recorded as a branch, in Java's order, so the solver can take the out-of-bounds side.
  • A call that throws at a failed check is fully explained by these branches, so it no longer counts as a context loss.
  • The branches are marked as callback branches, so the SA walk holds its place.
• Pins:
  • Where a model works on the concrete value of a symbolic int, a branch x == concrete makes the model exact; the solver tries other values in other runs.
  • Pinned values: the length in toCharArray, the indices of getChars, the length in setLength, the char of lastIndexOf, and the sizes and ranges of char[] arguments.

DTOBuilder

• The UFs of the exact models (commonPrefixLength, trimStart, trimEnd, lastIndexOf) no longer count as precision loss. Each one is defined exactly by a trace constraint on its arguments.
• I checked these models, and also regionMatches, valueOf(Object) and indexOf(String, int), against the Java spec. The tests cover them.

Measured

• Config: nosa, sv-comp.cfg, 300 s, mem15g, against baseline-results.jsonl. 568 runs:
  • 211 runs with the KB causes context-loss-string, indexof-char-arg-encoded-as-decimal, string-startswith-offset-concrete-wrong, string-index-bounds-not-branched, string-encoding-imprecise and stringbuilder-unmodelled-mutator-desync;
  • 287 baseline-correct string-related runs: jbmc String*/StringBuilder*/CharSequence*, autostub String*/Character*, securibench, argv-tasks, and tasks whose sources call String methods;
  • 70 random baseline-correct runs.
• The runs that use replace or capacity (the last changes) were re-run on the final jar.
• Result: +49 points, 31 runs gained, 0 lost, 0 new wrong verdicts.

task	prop	base	new	pts
jbmc StringBuilderAppend01/02, CapLen01, Chars01, InsertDelete01/02/03	both	unknown	safe (10 runs)	+20
jbmc StringBuilderAppend02, Chars04/05/06, InsertDelete02/03	valid-assert	unknown	violation	+6
jbmc StringIndexMethods01, StringStartEnd01	both	unknown	safe	+8
jbmc StringCompare04, StringIndexMethods03/05	NRE	unknown	safe	+6
jbmc SubString02/03, StringValueOf02/03	valid-assert	unknown	violation	+4
securibench Inter10	NRE	unknown	violation	+1
autostub String lastIndexOf_int, lastIndexOf_int_int	valid-assert	unknown	violation	+2

Tests

• StringModelExactnessTest (L0, 658 cases): each model is applied to symbolic strings and ints. With the variables fixed to a sample, it must admit only Java's result. For compareTo the test checks only that Java's result is admitted, because Z3 does not show uniqueness through the UF within reasonable time. The index checks must hold iff Java does not throw.
• StringIndexCheckAgentSpec (L2, forked agent): charAt records its index check on both sides, and no context loss when it throws.
• The full test and agentTest suites pass.

Known limits

• replace stays precision loss.
• reverse of symbolic content, codePointAt and similar methods, and StringBuffer stay unmodelled (context loss).
• Z3 struggles with the compareTo/lastIndexOf UF encodings (Static pre-analysis pruning, with soundness fixes #65): some queries end UNKNOWN by timeout.
• The added index-check branches add solver queries in loops over charAt. The negations are trivially UNSAT, and no timeouts appeared in the measured set.

Overlap with #71

• Decide precision loss by symbol kind instead of by variable name #71 decides precision loss by symbol kind and edits StringValue: it declares the same four UFs as MODEL_FUNCTION and records precision loss for lastIndexOf(int) with a symbolic char.
• Here, StringValue.EXACT_UFS plus a check in DTOBuilder does the same for the UFs. On merge, keep Decide precision loss by symbol kind instead of by variable name #71's registry and drop EXACT_UFS.
• For lastIndexOf(int) this PR pins the char (exact) instead. With the pin, the precision loss Decide precision loss by symbol kind instead of by variable name #71 records for a symbolic char is no longer needed.
• Inexact models here call recordSymbolicPrecisionLoss(), as Decide precision loss by symbol kind instead of by variable name #71 expects.

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