Skip to content

Make the String and StringBuilder models sound #75

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
nils-loose wants to merge 5 commits into from
Closed

Make the String and StringBuilder models sound #75

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0f84f31
Make the String models match Java
nils-loose Oct 18, 2026
186d971
Make the StringBuilder model exact, and record the index checks of St…
nils-loose Oct 18, 2026
ae83736
Do not count the exactly defined String UFs as precision loss
nils-loose Oct 18, 2026
0df4738
Test that the String and StringBuilder models are exact
nils-loose Oct 18, 2026
ac1a353
Keep the nested replace, as precision loss; model the constructor's c…
nils-loose Oct 18, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 68 additions & 8 deletions symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
import de.uzl.its.swat.metadata.ClassDepotRuntime;
import de.uzl.its.swat.symbolic.instruction.*;
import de.uzl.its.swat.symbolic.invoke.InvocationHandler;
import de.uzl.its.swat.symbolic.invoke.java.lang.StringCallBranches;
import de.uzl.its.swat.symbolic.processor.InstructionProcessor;
import de.uzl.its.swat.symbolic.processor.SymbolicInstructionProcessor;
import de.uzl.its.swat.symbolic.shadow.Frame;
Expand Down Expand Up @@ -1363,11 +1364,16 @@ public void visitGETVALUE_Object(GETVALUE_Object<?> inst) throws SymbolicInstruc
}
Logger shadowStateLogger = ThreadHandler.getShadowStateLogger(currentThread().getId());
shadowStateLogger.info("Recovered object from heap: {}", tmp);
if (tmp instanceof StringBuilderValue sbv) {
StringBuilder sb = (StringBuilder) inst.val;
SWATAssert.check(sbv.getStringValue().concrete.equals(inst.val),
"Concrete value of the StringBuilder does not match the value in the stack: {} | {}",
sbv.getStringValue().concrete, sb.toString());
if (tmp instanceof StringBuilderValue sbv && inst.val != null) {
String chars = inst.val.toString();
if (sbv.isUnknown() || sbv.getStringValue() == null) {
// A change SWAT does not model left its chars unknown: take the concrete ones.
sbv.resync(chars);
} else {
SWATAssert.check(sbv.getStringValue().concrete.equals(chars),
"Concrete value of the StringBuilder does not match the value in the stack: {} | {}",
sbv.getStringValue().concrete, chars);
}
}
stack.pushOperand(tmp);
} else if (inst.address == 0) {
Expand Down Expand Up @@ -2300,6 +2306,57 @@ public void visitINSTANCEOF(INSTANCEOF inst) throws SymbolicInstructionException
}
}

/**
* Records the branches a String or StringBuilder call takes inside the library, which their
* models rely on (see {@link StringCallBranches}): its index checks, and pins of the concrete
* values a model uses. On a normal return all of them held; a call that threw failed one of the
* index checks, if the receiver's chars say so, and that exception is then fully explained by
* the branches.
*
* @param returned Whether the call returned normally
* @return Whether the call threw at one of its index checks
*/
private boolean recordStringCallBranches(long iid, String name, String desc, ObjectValue<?, ?> instance, Value<?, ?>[] arguments, boolean returned) throws NoThreadContextException {
List<StringCallBranches.Branch> branches = StringCallBranches.of(instance, name, desc, arguments);
int failed = -1;
for (int i = 0; i < branches.size() && failed < 0; i++) {
if (!branches.get(i).holds()) failed = i;
}
// A normal return where an index check failed (or a throw where all held): the shadow
// does not match the call; that is left to the model and to recordThrowingCall.
if (branches.isEmpty() || returned == (failed >= 0)) return false;
int last = returned ? branches.size() - 1 : failed;
FormulaManager fmgr = instance.context.getFormulaManager();
for (int i = 0; i <= last; i++) {
StringCallBranches.Branch branch = branches.get(i);
if (!fmgr.extractVariables(branch.condition()).isEmpty()) {
symbolicTraceHandler.checkAndSetLibraryBranch(branch.holds(), branch.condition(), determineIid(iid), "#" + name);
}
}
return !returned;
}

/**
* As {@link #recordThrowingCall}, unless the call threw at an index check of a String or
* StringBuilder method (see {@link #recordStringCallBranches}), which the trace then explains.
*/
private void recordThrowingInstanceCall(long iid, String owner, String name, String desc, long invokeId) throws NoThreadContextException {
boolean explained;
try {
ObjectValue<?, ?> instance = stack.getInstance();
Value<?, ?>[] arguments = stack.fetchArgumentsFromLocals(Type.getArgumentTypes(desc), true);
explained = recordStringCallBranches(iid, name, desc, instance, arguments, false);
} catch (Exception e) {
explained = false;
}
if (explained) {
// Not an exception the static pre-analysis graph models (it walks over library calls).
recordUnmodelledException(iid);
} else {
recordThrowingCall(iid, owner, name, desc, invokeId, true);
}
}

/**
* Handles a call to an uninstrumented method that threw instead of returning: its model, if it
* has one, is not consulted (that happens on a normal return), and whether it throws may depend
Expand Down Expand Up @@ -2340,6 +2397,7 @@ public void visitINVOKEINTERFACE(INVOKEINTERFACE inst) throws SymbolicInstructio

ObjectValue<?, ?> instance = stack.getInstance();
Value<?, ?>[] arguments = stack.fetchArgumentsFromLocals(Type.getArgumentTypes(inst.desc), true);
recordStringCallBranches(inst.iid, inst.name, inst.desc, instance, arguments, true);
Value<?, ?> retVal = InvocationHandler.invoke(
symbolicTraceHandler,
inst.desc,
Expand All @@ -2352,7 +2410,7 @@ public void visitINVOKEINTERFACE(INVOKEINTERFACE inst) throws SymbolicInstructio
stack.setReturnValue(retVal);

} else if (stack.getNextInst() instanceof INVOKEMETHOD_EXCEPTION) {
recordThrowingCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId, true);
recordThrowingInstanceCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId);
}

if (!inst.owner.equals("de/uzl/its/swat/Main")) {
Expand All @@ -2376,6 +2434,7 @@ public void visitINVOKESPECIAL(INVOKESPECIAL inst) throws SymbolicInstructionExc
if (stack.getNextInst() instanceof INVOKEMETHOD_END) {
ObjectValue<?, ?> instance = stack.getInstance();
Value<?, ?>[] arguments = stack.fetchArgumentsFromLocals(Type.getArgumentTypes(inst.desc), true);
recordStringCallBranches(inst.iid, inst.name, inst.desc, instance, arguments, true);
Value<?, ?> retVal = InvocationHandler.invoke(
symbolicTraceHandler,
inst.desc,
Expand All @@ -2387,7 +2446,7 @@ public void visitINVOKESPECIAL(INVOKESPECIAL inst) throws SymbolicInstructionExc
instance);
stack.setReturnValue(retVal);
} else if (stack.getNextInst() instanceof INVOKEMETHOD_EXCEPTION) {
recordThrowingCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId, true);
recordThrowingInstanceCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId);
}

if (!inst.owner.equals("de/uzl/its/swat/Main")) {
Expand Down Expand Up @@ -2458,6 +2517,7 @@ public void visitINVOKEVIRTUAL(INVOKEVIRTUAL inst) throws SymbolicInstructionExc
if (stack.getNextInst() instanceof INVOKEMETHOD_END) {
ObjectValue<?, ?> instance = stack.getInstance();
Value<?, ?>[] arguments = stack.fetchArgumentsFromLocals(Type.getArgumentTypes(inst.desc), true);
recordStringCallBranches(inst.iid, inst.name, inst.desc, instance, arguments, true);
Value<?, ?> retVal = InvocationHandler.invoke(
symbolicTraceHandler,
inst.desc,
Expand All @@ -2469,7 +2529,7 @@ public void visitINVOKEVIRTUAL(INVOKEVIRTUAL inst) throws SymbolicInstructionExc
instance);
stack.setReturnValue(retVal);
} else if (stack.getNextInst() instanceof INVOKEMETHOD_EXCEPTION) {
recordThrowingCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId, true);
recordThrowingInstanceCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId);
}

if (!inst.owner.equals("de/uzl/its/swat/Main")) {
Expand Down
221 changes: 221 additions & 0 deletions ...-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringCallBranches.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,221 @@
package de.uzl.its.swat.symbolic.invoke.java.lang;

import de.uzl.its.swat.symbolic.value.Value;
import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue;
import de.uzl.its.swat.symbolic.value.reference.ObjectValue;
import de.uzl.its.swat.symbolic.value.reference.StringBuilderValue;
import de.uzl.its.swat.symbolic.value.reference.array.CharArrayValue;
import de.uzl.its.swat.symbolic.value.reference.lang.StringValue;
import java.util.ArrayList;
import java.util.List;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.BooleanFormulaManager;
import org.sosy_lab.java_smt.api.FormulaManager;
import org.sosy_lab.java_smt.api.IntegerFormulaManager;
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
import org.sosy_lab.java_smt.api.SolverContext;
import org.sosy_lab.java_smt.api.StringFormulaManager;

/**
* The branches a call of a String or StringBuilder method takes inside the library, which the
* models of these methods (StringValue, StringBuilderValue) rely on. The visitor records them in the
* trace, so the solver can take their other side:
*
* <ul>
* <li>Index checks: the method returns normally iff its indices are in range, and throws an
* IndexOutOfBoundsException otherwise. One check per exception the method may throw, in the
* order Java checks them, so all inputs that fail the same check throw the same exception.
* <li>Pins: a model that works on the concrete value of a symbolic int (e.g. a loop over the
* concrete length of a string) is exact only for that value. The branch {@code x == concrete}
* makes the solver try the other values, in other runs.
* </ul>
*
* Index checks come first: the pins are only reached when the indices are in range.
*/
public final class StringCallBranches {

/** A branch: its condition and whether it held in this run. */
public record Branch(BooleanFormula condition, boolean holds) {}

/** An int the checks are about, as a formula over the integers and concretely. */
private record Int(IntegerFormula f, long c, boolean symbolic) {}

private final SolverContext context;
private final BooleanFormulaManager bmgr;
private final IntegerFormulaManager imgr;
private final StringFormulaManager smgr;
private final List<Branch> branches = new ArrayList<>();

private StringCallBranches(SolverContext context) {
this.context = context;
FormulaManager fmgr = context.getFormulaManager();
this.bmgr = fmgr.getBooleanFormulaManager();
this.imgr = fmgr.getIntegerFormulaManager();
this.smgr = fmgr.getStringFormulaManager();
}

/**
* The branches of calling {@code name} with descriptor {@code desc} on {@code instance}, in
* order: empty if the method has none or is not modelled. The concrete values are those before
* the call.
*/
public static List<Branch> of(Value<?, ?> instance, String name, String desc, Value<?, ?>[] args) {
try {
if (instance instanceof StringValue str) {
StringCallBranches b = new StringCallBranches(str.context);
b.ofString(str, name, desc, args);
return b.branches;
} else if (instance instanceof StringBuilderValue sb && sb.getContent() != null) {
StringCallBranches b = new StringCallBranches(sb.context);
b.ofStringBuilder(sb.getContent(), name, desc, args);
return b.branches;
}
} catch (Exception e) {
// Arguments of unexpected types: the model returns a PlaceHolder for them as well.
}
return List.of();
}

private void ofString(StringValue s, String name, String desc, Value<?, ?>[] args) throws Exception {
switch (name + desc) {
case "charAt(I)C" -> index(s, args[0]);
case "substring(I)Ljava/lang/String;" -> range(s, num(args[0]), length(s));
case "substring(II)Ljava/lang/String;", "subSequence(II)Ljava/lang/CharSequence;" ->
range(s, num(args[0]), num(args[1]));
case "getChars(II[CI)V" -> getChars(s, args);
case "toCharArray()[C" -> pin(length(s));
case "<init>([C)V" -> pin(size(args[0]));
case "lastIndexOf(I)I", "lastIndexOf(II)I" -> pin(num(args[0]));
default -> { }
}
}

private void ofStringBuilder(StringValue s, String name, String desc, Value<?, ?>[] args) throws Exception {
String sig = name + desc.substring(0, desc.indexOf(')') + 1);
switch (sig) {
case "charAt(I)", "setCharAt(IC)", "deleteCharAt(I)" -> index(s, args[0]);
case "delete(II)", "replace(IILjava/lang/String;)" -> {
// An end past the length is taken as the length: start in [0, min(end, length)].
Int start = num(args[0]);
Int end = num(args[1]);
Int len = length(s);
add(bmgr.and(imgr.greaterOrEquals(start.f(), zero()), imgr.lessOrEquals(start.f(), end.f()),
imgr.lessOrEquals(start.f(), len.f())),
0 <= start.c() && start.c() <= end.c() && start.c() <= len.c());
}
case "substring(I)" -> range(s, num(args[0]), length(s));
case "substring(II)", "subSequence(II)" -> range(s, num(args[0]), num(args[1]));
case "setLength(I)" -> {
Int n = num(args[0]);
add(imgr.greaterOrEquals(n.f(), zero()), n.c() >= 0);
pin(n);
}
case "getChars(II[CI)" -> getChars(s, args);
case "appendCodePoint(I)" -> {
Int cp = num(args[0]);
add(bmgr.and(imgr.greaterOrEquals(cp.f(), zero()), imgr.lessOrEquals(cp.f(), imgr.makeNumber(Character.MAX_CODE_POINT))),
Character.isValidCodePoint((int) cp.c()));
}
case "append([C)" -> pin(size(args[0]));
case "append([CII)" -> {
// checkRange(offset, offset + len, str.length), in int arithmetic: with all three
// pinned, the check is concrete.
pin(num(args[1]));
pin(num(args[2]));
pin(size(args[0]));
}
case "append(Ljava/lang/CharSequence;II)" -> {
StringValue seq = sequence(args[0]);
if (seq != null) range(seq, num(args[1]), num(args[2]));
}
default -> {
if (name.equals("insert")) insert(s, desc, args);
}
}
}

private void insert(StringValue s, String desc, Value<?, ?>[] args) throws Exception {
// insert(int offset, ...): the offset in [0, length]
Int offset = num(args[0]);
Int len = length(s);
add(bmgr.and(imgr.greaterOrEquals(offset.f(), zero()), imgr.lessOrEquals(offset.f(), len.f())),
0 <= offset.c() && offset.c() <= len.c());
if (desc.startsWith("(I[CII)")) {
pin(num(args[2]));
pin(num(args[3]));
pin(size(args[1]));
} else if (desc.startsWith("(I[C)")) {
pin(size(args[1]));
} else if (desc.startsWith("(ILjava/lang/CharSequence;II)")) {
StringValue seq = sequence(args[1]);
if (seq != null) range(seq, num(args[2]), num(args[3]));
}
}

/** getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin) of String and StringBuilder. */
private void getChars(StringValue s, Value<?, ?>[] args) throws Exception {
Int srcBegin = num(args[0]);
Int srcEnd = num(args[1]);
range(s, srcBegin, srcEnd);
if (!(args[2] instanceof CharArrayValue)) return;
Int dstBegin = num(args[3]);
Int dstLength = size(args[2]);
// dst[dstBegin, dstBegin + srcEnd - srcBegin) in range (srcBegin <= srcEnd holds here)
IntegerFormula end = imgr.add(dstBegin.f(), imgr.subtract(srcEnd.f(), srcBegin.f()));
add(bmgr.and(imgr.greaterOrEquals(dstBegin.f(), zero()), imgr.lessOrEquals(end, dstLength.f())),
dstBegin.c() >= 0 && dstBegin.c() + srcEnd.c() - srcBegin.c() <= dstLength.c());
// The model copies by the concrete indices.
pin(srcBegin);
pin(srcEnd);
pin(dstBegin);
}

/** 0 <= index < length of s */
private void index(StringValue s, Value<?, ?> indexArg) throws Exception {
Int i = num(indexArg);
Int len = length(s);
add(bmgr.and(imgr.greaterOrEquals(i.f(), zero()), imgr.lessThan(i.f(), len.f())),
0 <= i.c() && i.c() < len.c());
}

/** 0 <= begin <= end <= length of s */
private void range(StringValue s, Int b, Int e) {
Int len = length(s);
add(bmgr.and(imgr.greaterOrEquals(b.f(), zero()), imgr.lessOrEquals(b.f(), e.f()), imgr.lessOrEquals(e.f(), len.f())),
0 <= b.c() && b.c() <= e.c() && e.c() <= len.c());
}

private Int num(Value<?, ?> v) throws Exception {
IntValue i = v.asIntValue();
return new Int(i.asIntegerFormula(), i.concrete, i.isSymbolic());
}

private Int length(StringValue s) {
return new Int(smgr.length(s.formula), s.concrete.length(), s.isSymbolic());
}

private Int size(Value<?, ?> array) throws Exception {
return num(((CharArrayValue) array).size);
}

/** The chars of a CharSequence argument; null is taken as "null", as by append and insert. */
private StringValue sequence(Value<?, ?> v) {
if (v instanceof ObjectValue<?, ?> o && o.isNullValue()) return new StringValue(context, "null", -1);
return StringValue.charsOf(v);
}

/** x == its concrete value, if x is symbolic */
private void pin(Int x) {
if (x.symbolic()) {
add(imgr.equal(x.f(), imgr.makeNumber(x.c())), true);
}
}

private IntegerFormula zero() {
return imgr.makeNumber(0);
}

private void add(BooleanFormula condition, boolean holds) {
branches.add(new Branch(condition, holds));
}
}
6 changes: 5 additions & 1 deletion symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
import de.uzl.its.swat.symbolic.trace.dto.*;
import de.uzl.its.swat.thread.ThreadHandler;
import de.uzl.its.swat.witness.Witness;
import de.uzl.its.swat.symbolic.value.reference.lang.StringValue;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Set;
Expand Down Expand Up @@ -109,8 +110,11 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage
for (InputElement ie : symbolicTrace.getInputs()) {
inputNames.add(ie.getName());
}
// The UFs of the exact String models are defined by the trace's constraints (see
// StringValue.EXACT_UFS), so they are no loss of precision either.
java.util.function.Predicate<String> isInput =
name -> inputNames.contains(name) || name.matches("[A-Z].*_[0-9].*");
name -> inputNames.contains(name) || name.matches("[A-Z].*_[0-9].*")
|| StringValue.EXACT_UFS.contains(name);
boolean symbolicPrecisionLoss = symbolicTrace.isSymbolicPrecisionLoss();
for (Element el : symbolicTrace.getTrace()) {
if (el instanceof BranchElement be) {
Expand Down
Loading
Loading