From 0f84f3159eb0259b41ebcec2fca139a597ca231b Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 22:25:07 +0000 Subject: [PATCH 1/5] Make the String models match Java - indexOf(int ch[, from]) searches for the char (or the surrogate pair of a supplementary code point), not for its decimal digits; no code point, no match. - lastIndexOf(int ch[, from]) has no match for a ch that is no code point, also when ch is symbolic; the char is taken concretely (pinned by the caller). - startsWith(prefix, toffset) is false for an offset out of range, and its concrete result uses the offset. - replace uses str.replace_all instead of ten first-occurrence replaces; an empty or symbolic target (where Java and str.replace_all differ) is precision loss. - equals is true only for a String argument (false for null, not modelled for others); contentEquals and contains take a StringBuilder too. - getChars writes to dst from dstBegin, not from dstBegin + srcBegin. - toCharArray of "" returns an empty array; subSequence is substring. - new String(), new String(char[]) and new String(StringBuilder) are modelled; other constructors return a PlaceHolder (a missing invocation) instead of silently keeping the empty string. - Long and Short values convert to a String with their sign. Co-Authored-By: Claude Opus 5.5 --- .../primitive/numeric/integral/LongValue.java | 15 +- .../numeric/integral/ShortValue.java | 15 +- .../value/reference/lang/StringValue.java | 241 ++++++++++++------ 3 files changed, 186 insertions(+), 85 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java index 36c157ef..2cc2dfc7 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java @@ -402,13 +402,16 @@ public DoubleValue asDoubleValue() { @Override public StringValue asStringValue() { - // String theory requires IntegerFormula, so convert BV to Int + // String theory requires IntegerFormula, so convert BV to Int. str.from_int gives "" for a + // negative number, so its digits are those of its absolute value, after a "-". NumeralFormula.IntegerFormula intFormula = bvmgr.toIntegerFormula(formula, true); - return new StringValue( - this.context, - String.valueOf(concrete), - context.getFormulaManager().getStringFormulaManager().toStringFormula(intFormula), - -1); + StringFormulaManager smgr = context.getFormulaManager().getStringFormulaManager(); + IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager(); + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + StringFormula str = bmgr.ifThenElse(imgr.lessThan(intFormula, imgr.makeNumber(0)), + smgr.concat(smgr.makeString("-"), smgr.toStringFormula(imgr.negate(intFormula))), + smgr.toStringFormula(intFormula)); + return new StringValue(this.context, String.valueOf(concrete), str, -1); } @Override diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java index 16645268..274dc03b 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java @@ -219,13 +219,16 @@ public ShortObjectValue asObjectValue() { @Override public StringValue asStringValue() { - // String theory requires IntegerFormula, so convert BV to Int + // String theory requires IntegerFormula, so convert BV to Int. str.from_int gives "" for a + // negative number, so its digits are those of its absolute value, after a "-". NumeralFormula.IntegerFormula intFormula = bvmgr.toIntegerFormula(formula, true); - return new StringValue( - this.context, - String.valueOf(concrete), - context.getFormulaManager().getStringFormulaManager().toStringFormula(intFormula), - -1); + StringFormulaManager smgr = context.getFormulaManager().getStringFormulaManager(); + IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager(); + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + StringFormula str = bmgr.ifThenElse(imgr.lessThan(intFormula, imgr.makeNumber(0)), + smgr.concat(smgr.makeString("-"), smgr.toStringFormula(imgr.negate(intFormula))), + smgr.toStringFormula(intFormula)); + return new StringValue(this.context, String.valueOf(concrete), str, -1); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java index b273156a..34d48bf2 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java @@ -20,6 +20,7 @@ import lombok.Getter; import org.objectweb.asm.Type; import org.sosy_lab.java_smt.api.*; +import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; import static java.lang.Thread.currentThread; @@ -27,7 +28,14 @@ public class StringValue extends ObjectValue { @Getter private static final String symbolicPrefix = Type.getType(String.class).getInternalName(); - static final int REPLACE_COUNT = 10; + /** + * The UFs the models of compareTo, trim and lastIndexOf introduce. Each is defined exactly by a + * constraint on its arguments that is added to the trace (addDefinition): it has one value for + * any arguments (trim's bounds of an all-blank string excepted, where only lo == hi matters), + * so a constraint over them is as exact as one over the inputs. + */ + public static final java.util.Set EXACT_UFS = java.util.Set.of("commonPrefixLength", "trimStart", "trimEnd", "lastIndexOf"); + private StringFormulaManager smgr; private IntegerFormulaManager imgr; @@ -227,13 +235,24 @@ public BooleanFormula getBounds(boolean upper) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeInit(Value[] args, Type[] desc) { - if (args.length == 1 && args[0] instanceof StringValue s) { - this.concrete = s.concrete; - this.formula = s.formula; - } // Mark this string as user-de-interned since it was created via new String() // in user code (as opposed to SWAT's NoCacheMethodAdapter de-interning) this.userDeInterned = true; + StringValue chars; + if (args.length == 0) { + chars = new StringValue(context, "", -1); + } else if (args.length == 1 && args[0] instanceof CharArrayValue array) { + // The concrete number of chars, which the call's branches pin (StringCallBranches). + chars = array.asStringValue(); + } else if (args.length == 1) { + // new String(String), new String(StringBuilder) + chars = charsOf(args[0]); + } else { + chars = null; + } + if (chars == null) return PlaceHolder.instance; + this.concrete = chars.concrete; + this.formula = chars.formula; return VoidValue.instance; } @@ -371,6 +390,24 @@ public BooleanFormula getBounds(boolean upper) { return new IntValue(context, result, cmp); } + /** Records that a model is not exact for this call, so an exhausted search proves nothing. */ + static void recordPrecisionLoss() { + try { + ThreadHandler.getSymbolicTraceHandler(currentThread().getId()).recordSymbolicPrecisionLoss(); + } catch (Exception e) { + throw new IllegalStateException("No symbolic trace handler for the current thread", e); + } + } + + /** + * The chars of a CharSequence SWAT tracks: a String or a StringBuilder's content, else null. + */ + public static StringValue charsOf(Value sequence) { + if (sequence instanceof StringValue str) return str; + if (sequence instanceof de.uzl.its.swat.symbolic.value.reference.StringBuilderValue sb) return sb.getContent(); + return null; + } + /** Adds a constraint that defines the UFs a model introduced; it holds on every path and is never negated. */ private static void addDefinition(BooleanFormula definition) { try { @@ -428,7 +465,8 @@ private static void addDefinition(BooleanFormula definition) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeContains(Value[] args, Type[] desc) { - if (args.length == 1 && args[0] instanceof StringValue s) { + StringValue s = args.length == 1 ? charsOf(args[0]) : null; + if (s != null) { boolean result = concrete.contains(s.concrete); return new BooleanValue(context, result, smgr.contains(formula, s.formula)); } else { @@ -448,7 +486,9 @@ private static void addDefinition(BooleanFormula definition) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeContentEquals(Value[] args, Type[] desc) { - return PlaceHolder.instance; + StringValue other = args.length == 1 ? charsOf(args[0]) : null; + if (other == null) return PlaceHolder.instance; + return new BooleanValue(context, concrete.contentEquals(other.concrete), smgr.equal(formula, other.formula)); } /** @@ -500,15 +540,14 @@ private static void addDefinition(BooleanFormula definition) { */ private Value invokeEquals(Value[] args, Type[] desc) { if (args.length == 1) { - Value anObject = args[0]; - try { - StringValue str = anObject.asStringValue(); + // Only a String is equal to a String (not, e.g., a StringBuilder with the same chars). + if (args[0] instanceof StringValue str) { boolean result = concrete.equals(str.concrete); return new BooleanValue(context, result, smgr.equal(formula, str.formula)); - } catch (Exception ignored) { - System.out.println("No String indeed!"); - return PlaceHolder.instance; + } else if (args[0] instanceof ObjectValue obj && obj.getAddress() == ObjectValue.ADDRESS_NULL) { + return new BooleanValue(context, false); } + return PlaceHolder.instance; } else { return PlaceHolder.instance; } @@ -607,11 +646,12 @@ private static void addDefinition(BooleanFormula definition) { IntValue srcEnd = args[1].asIntValue(); CharArrayValue dst = args[2].asObjectValue().asArrayValue().asCharArrayValue(); IntValue dstBegin = args[3].asIntValue(); + // By the concrete indices, which the call's branches pin (StringCallBranches). for (int idx = srcBegin.concrete; idx < srcEnd.concrete; idx++) { Value[] charAtArgs = new Value[] { new IntValue(context, idx) }; Type[] charAtDesc = new Type[] { Type.INT_TYPE }; dst.storeElement( - new IntValue(context, dstBegin.concrete + idx), + new IntValue(context, dstBegin.concrete + idx - srcBegin.concrete), (CharValue) invokeCharAt(charAtArgs, charAtDesc)); } return VoidValue.instance; @@ -708,7 +748,43 @@ private static void addDefinition(BooleanFormula definition) { } private Value invokeIndexOf(IntValue ch, IntValue fromIndex) { - return invokeIndexOf(ch.asStringValue(), fromIndex); + int result = concrete.indexOf(ch.concrete, fromIndex.concrete); + if (!isSymbolic() && !ch.isSymbolic() && !fromIndex.isSymbolic()) return new IntValue(context, result); + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + IntValue index = (IntValue) invokeIndexOf(new StringValue(context, "", codePointString(ch), -1), fromIndex); + // No code point, no match (as Java, which searches for a code point, not for its digits). + return new IntValue(context, result, bmgr.ifThenElse(isCodePoint(ch), index.asIntegerFormula(), imgr.makeNumber(-1))); + } + + /** Whether ch is a code point, i.e. in [0, 0x10FFFF]: the chars indexOf(int)/lastIndexOf(int) can find. */ + private BooleanFormula isCodePoint(IntValue ch) { + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + if (!ch.isSymbolic()) return bmgr.makeBoolean(Character.isValidCodePoint(ch.concrete)); + NumeralFormula.IntegerFormula c = ch.asIntegerFormula(); + return bmgr.and(imgr.greaterOrEquals(c, imgr.makeNumber(0)), + imgr.lessOrEquals(c, imgr.makeNumber(Character.MAX_CODE_POINT))); + } + + /** + * The chars of code point ch in a Java string (String.valueOf(Character.toChars(ch))): the char + * itself in the BMP, else its surrogate pair. Meaningful only if {@link #isCodePoint} holds. + */ + public StringFormula codePointString(IntValue ch) { + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + if (!ch.isSymbolic()) { + // Char by char: makeString would take a surrogate pair for one (SMT) character. + if (!Character.isValidCodePoint(ch.concrete)) return smgr.makeString(""); + StringFormula chars = smgr.makeString(""); + for (char c : Character.toChars(ch.concrete)) chars = smgr.concat(chars, smgr.fromCodePoint(imgr.makeNumber(c))); + return chars; + } + NumeralFormula.IntegerFormula c = ch.asIntegerFormula(); + NumeralFormula.IntegerFormula offset = imgr.subtract(c, imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT)); + NumeralFormula.IntegerFormula high = imgr.add(imgr.makeNumber(Character.MIN_HIGH_SURROGATE), imgr.divide(offset, imgr.makeNumber(1024))); + NumeralFormula.IntegerFormula low = imgr.add(imgr.makeNumber(Character.MIN_LOW_SURROGATE), imgr.modulo(offset, imgr.makeNumber(1024))); + return bmgr.ifThenElse(imgr.lessThan(c, imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT)), + smgr.fromCodePoint(c), + smgr.concat(smgr.fromCodePoint(high), smgr.fromCodePoint(low))); } /** @@ -771,14 +847,14 @@ private static void addDefinition(BooleanFormula definition) { if (args.length < 1 || args.length > 2) return PlaceHolder.instance; IntValue from = args.length == 2 ? args[1].asIntValue() : new IntValue(context, Integer.MAX_VALUE); StringValue target; + IntValue ch = null; int result; if (desc[0].getSort() == Type.INT) { - IntValue ch = args[0].asIntValue(); - // Supplementary code points are two chars in a Java string but one in the solver's, so - // only BMP chars are modelled exactly (the UF below flags the result as imprecise anyway). - if (ch.concrete < 0 || ch.concrete > Character.MAX_VALUE) return PlaceHolder.instance; - target = new StringValue(context, String.valueOf((char) (int) ch.concrete), - smgr.fromCodePoint(ch.asIntegerFormula()), -1); + // The chars of the code point; for anything else there is no match. By the concrete + // char, which the call's branches pin (StringCallBranches): with a symbolic one the + // window encoding below is too hard for the solver. + ch = new IntValue(context, args[0].asIntValue().concrete); + target = new StringValue(context, "", codePointString(ch), -1); result = concrete.lastIndexOf(ch.concrete, from.concrete); } else if (args[0] instanceof StringValue str) { target = str; @@ -811,7 +887,7 @@ private static void addDefinition(BooleanFormula definition) { bmgr.and(imgr.greaterOrEquals(r, imgr.makeNumber(0)), imgr.lessOrEquals(r, last), smgr.equal(smgr.substring(formula, r, tlen), target.formula), bmgr.not(smgr.contains(afterR, target.formula)))))); - return new IntValue(context, result, r); + return new IntValue(context, result, ch == null ? r : bmgr.ifThenElse(isCodePoint(ch), r, imgr.makeNumber(-1))); } /** @@ -955,42 +1031,59 @@ private static void addDefinition(BooleanFormula definition) { } private Value invokeReplace(ObjectValue target, ObjectValue replacement) { - if (target instanceof StringValue oldString && replacement instanceof StringValue newString) { - // ToDo (Nils): This is the correct implementation. However replaceAll is currently not - // supported by Z3 - /* - formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula); - */ - - var newConcrete = this.concrete.replace(oldString.concrete, newString.concrete); - var newFormula = this.formula; - for (int i = 0; i < REPLACE_COUNT; i++) { - newFormula = smgr.replace(newFormula, oldString.formula, newString.formula); - } - - return new StringValue(context, newConcrete, newFormula, ObjectValue.ADDRESS_UNKNOWN); - } else { - return PlaceHolder.instance; - } + StringValue oldString = charsOf(target); + StringValue newString = charsOf(replacement); + if (oldString == null || newString == null) return PlaceHolder.instance; + return replaceAll(oldString, newString); } private Value invokeReplace(CharValue oldChar, CharValue newChar) { - StringValue oldString = oldChar.asStringValue(); - StringValue newString = newChar.asStringValue(); - // ToDo (Nils): This is the correct implementation. However replaceAll is currently not - // supported by Z3 - // See: https://git.its.uni-luebeck.de/research-projects/pet-hmr/knife-fuzzer/-/issues/54 - /* - formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula); - */ - - var newConcrete = this.concrete.replace(oldString.concrete, newString.concrete); - var newFormula = this.formula; - for (int i = 0; i < REPLACE_COUNT; i++) { - newFormula = smgr.replace(newFormula, oldString.formula, newString.formula); + return replaceAll(oldChar.asStringValue(), newChar.asStringValue()); + } + + /** + * String.replace: every occurrence of target, left to right, which is str.replace_all for a + * non-empty target. For an empty one Java puts the replacement between any two chars and at both + * ends, where str.replace_all leaves the string as it is: not modelled. + */ + private StringValue replaceAll(StringValue target, StringValue replacement) { + String newConcrete = this.concrete.replace(target.concrete, replacement.concrete); + if (!isSymbolic() && !target.isSymbolic() && !replacement.isSymbolic()) { + return new StringValue(context, newConcrete, ObjectValue.ADDRESS_UNKNOWN); + } + if (target.isSymbolic() || target.concrete.isEmpty()) { + recordPrecisionLoss(); } + return new StringValue(context, newConcrete, replaceAll(formula, target.formula, replacement.formula), + ObjectValue.ADDRESS_UNKNOWN); + } - return new StringValue(context, newConcrete, newFormula, ObjectValue.ADDRESS_UNKNOWN); + /** + * str.replace_all(s, target, replacement). JavaSMT's Z3 backend does not offer it, so the term + * is parsed from SMT-LIB, over placeholder variables that are then substituted. + */ + private StringFormula replaceAll(StringFormula s, StringFormula target, StringFormula replacement) { + FormulaManager fmgr = context.getFormulaManager(); + StringFormula sVar = smgr.makeVariable("swat.replaceAll.s"); + StringFormula tVar = smgr.makeVariable("swat.replaceAll.t"); + StringFormula rVar = smgr.makeVariable("swat.replaceAll.r"); + StringFormula result = smgr.makeVariable("swat.replaceAll.result"); + BooleanFormula definition = fmgr.parse("(declare-fun |swat.replaceAll.s| () String)" + + "(declare-fun |swat.replaceAll.t| () String)(declare-fun |swat.replaceAll.r| () String)" + + "(declare-fun |swat.replaceAll.result| () String)" + + "(assert (= |swat.replaceAll.result| (str.replace_all |swat.replaceAll.s| |swat.replaceAll.t| |swat.replaceAll.r|)))"); + Formula term = fmgr.visit(definition, new DefaultFormulaVisitor() { + @Override + protected Formula visitDefault(Formula f) { + return null; + } + + @Override + public Formula visitFunction(Formula f, java.util.List args, FunctionDeclaration decl) { + return args.get(0).equals(result) ? args.get(1) : args.get(0); + } + }); + return fmgr.substitute((StringFormula) term, java.util.Map.of(sVar, s, tVar, target, rVar, replacement)); } /** @@ -1083,12 +1176,17 @@ private static void addDefinition(BooleanFormula definition) { } private Value invokeStartsWith(StringValue prefix, IntValue toffset) { + // As Java: false unless the prefix fits at toffset, i.e. 0 <= toffset <= length - prefix length. + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + NumeralFormula.IntegerFormula t = toffset.asIntegerFormula(); + NumeralFormula.IntegerFormula plen = smgr.length(prefix.formula); return new BooleanValue( context, - concrete.startsWith(prefix.concrete), - smgr.equal( - prefix.formula, - smgr.substring(formula, toffset.asIntegerFormula(), smgr.length(prefix.formula)))); + concrete.startsWith(prefix.concrete, toffset.concrete), + bmgr.and( + imgr.greaterOrEquals(t, imgr.makeNumber(0)), + imgr.lessOrEquals(t, imgr.subtract(smgr.length(formula), plen)), + smgr.equal(prefix.formula, smgr.substring(formula, t, plen)))); } /** @@ -1162,8 +1260,10 @@ private static void addDefinition(BooleanFormula definition) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeSubSequence(Value[] args, Type[] desc) { - return PlaceHolder.instance; + private Value invokeSubSequence(Value[] args, Type[] desc) + throws NotImplementedException, ValueConversionException { + // subSequence(begin, end) is substring(begin, end) + return args.length == 2 ? invokeSubstring(args, desc) : PlaceHolder.instance; } /** @@ -1219,21 +1319,16 @@ private static void addDefinition(BooleanFormula definition) { private Value invokeToCharArray(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { - if (!concrete.isEmpty()) { - CharArrayValue dst = new CharArrayValue(context, new IntValue(context, concrete.length()), -1); - for (int idx = 0; idx < concrete.length(); idx++) { - Value[] charAtArgs = new Value[] { new IntValue(context, idx) }; - Type[] charAtDesc = new Type[] { Type.INT_TYPE }; - dst.storeElement( - new IntValue(context, idx), - (CharValue) invokeCharAt(charAtArgs, charAtDesc)); - } - return dst; - } else { - new CharArrayValue(context, new IntValue(context, 0), -1); + // As long as the concrete string, which the call's branches pin (StringCallBranches). + CharArrayValue dst = new CharArrayValue(context, new IntValue(context, concrete.length()), -1); + for (int idx = 0; idx < concrete.length(); idx++) { + Value[] charAtArgs = new Value[] { new IntValue(context, idx) }; + Type[] charAtDesc = new Type[] { Type.INT_TYPE }; + dst.storeElement( + new IntValue(context, idx), + (CharValue) invokeCharAt(charAtArgs, charAtDesc)); } - - return PlaceHolder.instance; + return dst; } /** From 186d971f401045f36bdb0a6936697c965e0e8d52 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 22:25:19 +0000 Subject: [PATCH 2/5] Make the StringBuilder model exact, and record the index checks of String calls StringBuilder: the chars are a StringValue that is replaced on every change, never changed in place (it may be a String the program still holds). substring no longer truncates the builder (and takes end - start chars), replace replaces the range instead of the first occurrence of its contents, indexOf(str, from) and lastIndexOf use the String models, setLength is exact for any content. New models: append/insert of an Object, CharSequence, null, double and float, setCharAt, getChars, appendCodePoint, reverse of concrete chars, compareTo, subSequence, ensureCapacity/trimToSize; capacity is taken concretely. A builder with symbolic chars is symbolic now, so a method that is not modelled causes a context loss. After a change that is not modelled the chars are unknown: every method then returns a PlaceHolder until the builder is recovered from the heap, where it takes the concrete chars. (The consistency check of that recovery compared a String with a StringBuilder and always failed; it compares the chars now.) A StringBuilder from uninstrumented code gets a StringBuilderValue with its concrete chars. Index checks: String.charAt/substring/subSequence/getChars and the index methods of StringBuilder throw an IndexOutOfBoundsException for an index out of range, a branch inside the library that the trace did not have, so the solver never tried the other side. StringCallBranches gives these checks, in Java's order, and the visitor records them as branches (marked as in a callback, so the static pre-analysis walk holds its place). A call that threw at a failed check is explained by them and no longer counts as a context loss. Pins: where a model works on the concrete value of a symbolic int (the length in toCharArray, the indices of getChars, setLength's length, the char of lastIndexOf, char[] arguments' sizes and ranges), a branch x == concrete makes the solver try the other values in other runs, so the model is exact. Co-Authored-By: Claude Opus 5.5 --- .../symbolic/SymbolicInstructionVisitor.java | 76 +- .../invoke/java/lang/StringCallBranches.java | 221 ++++ .../symbolic/trace/SymbolicTraceHandler.java | 15 + .../its/swat/symbolic/value/ValueFactory.java | 2 + .../value/reference/StringBuilderValue.java | 1026 +++++------------ 5 files changed, 570 insertions(+), 770 deletions(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringCallBranches.java diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java index 771f7759..bbb2ced5 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java @@ -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; @@ -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) { @@ -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 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 @@ -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, @@ -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")) { @@ -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, @@ -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")) { @@ -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, @@ -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")) { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringCallBranches.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringCallBranches.java new file mode 100644 index 00000000..59ce6675 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringCallBranches.java @@ -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: + * + *
    + *
  • 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. + *
  • 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. + *
+ * + * 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 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 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 "([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)); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java index d8e1b62c..2cddaa2c 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java @@ -67,6 +67,21 @@ public void checkAndSetBranch(boolean result, BooleanFormula constraint, long ii symbolicTrace.addTraceElement(current); } + /** + * As {@link #checkAndSetBranch(boolean, BooleanFormula, long, String)}, for a branch inside a + * library call that SWAT models (e.g. the index check of String.charAt). The static pre-analysis + * graph walks over library calls, so the branch is marked as one in a callback: the explorer's + * walk of the graph holds its place, as for application code a library calls back. + */ + public void checkAndSetLibraryBranch(boolean result, BooleanFormula constraint, long iid, String suffix) throws NoThreadContextException { + BooleanFormulaManager bmgr = ThreadHandler.getSolverContext(Thread.currentThread().getId()) + .getFormulaManager().getBooleanFormulaManager(); + BranchElement branch = new BranchElement(result, result ? constraint : bmgr.not(constraint), iid); + place(branch, iid, suffix); + branch.setCallback(true); + symbolicTrace.addTraceElement(branch); + } + /** Records where a branch is: its key and the change of the frame stack since the last branch. */ private static void place(BranchElement branch, long iid, String suffix) throws NoThreadContextException { String key = BranchKeys.keyOf(iid); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java index fe32e31c..556cd3fb 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java @@ -116,6 +116,8 @@ public static StringValue createStringValue(String concrete, int address) throws return new StringValue(context, s, address); } else if (concrete instanceof IASString s) { return new StringValue(context, s.getString(), address); + } else if (concrete instanceof StringBuilder sb) { + return new StringBuilderValue(context, new StringValue(context, sb.toString(), -1), address); } else if (concrete instanceof Boolean b) { return new BooleanObjectValue(context, new BooleanValue(context, b), address); } else if (concrete instanceof Byte b) { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java index d2854f05..431c7c1f 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java @@ -1,5 +1,6 @@ package de.uzl.its.swat.symbolic.value.reference; +import com.google.common.collect.ImmutableSet; import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.config.Config; @@ -9,15 +10,37 @@ import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.CharValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue; import de.uzl.its.swat.symbolic.value.reference.array.CharArrayValue; +import de.uzl.its.swat.symbolic.value.reference.lang.BoxedValue; import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import java.util.Set; import org.objectweb.asm.Type; import org.sosy_lab.java_smt.api.*; +/** + * Shadow of a StringBuilder: + * its chars as a {@link StringValue}, which is replaced (never changed: it may be a String the + * program holds) on every change. + * + *

The index checks of the methods (when they throw an IndexOutOfBoundsException) and the + * concrete values the models rely on are recorded by the caller as branches, see + * StringCallBranches. The models below assume those hold. + * + *

After a change SWAT does not model (it returned a PlaceHolder), the chars are unknown: every + * method then returns a PlaceHolder, until the builder is recovered from the heap with its concrete + * value ({@link #resync}). + */ public final class StringBuilderValue extends ObjectValue { private final StringFormulaManager smgr; private final IntegerFormulaManager imgr; private StringValue stringValue; - private IntValue capacity; + + /** Whether a change SWAT does not model left the chars unknown. */ + private boolean unknown = false; + + /** The methods that change the builder: if one is not modelled, the chars are unknown. */ + private static final Set MUTATORS = Set.of("", "append", "appendCodePoint", "delete", + "deleteCharAt", "insert", "replace", "reverse", "setCharAt", "setLength"); public StringBuilderValue(SolverContext context) { super(context, ObjectValue.ADDRESS_UNKNOWN); @@ -38,6 +61,25 @@ public StringBuilderValue(SolverContext context, StringValue v, int address) { return stringValue; } + /** The chars, or null if they are not known. */ + public StringValue getContent() { + return unknown ? null : stringValue; + } + + public boolean isUnknown() { + return unknown; + } + + /** + * Takes the concrete chars of the builder, e.g. when it is recovered from the heap after a + * change SWAT does not model. A symbolic content was lost at that change already (with a + * context loss: the call returned a PlaceHolder for a symbolic receiver). + */ + public void resync(String chars) { + this.stringValue = new StringValue(context, chars, -1); + this.unknown = false; + } + /** * Handles method invocation for Java's StringBuilder @@ -51,832 +93,291 @@ public StringBuilderValue(SolverContext context, StringValue v, int address) { */ @Override public Value invokeMethod(String name, Type[] desc, Value[] args) throws NotImplementedException, ValueConversionException { - return switch (name) { - case "" -> invokeInit(args, desc); - case "append" -> invokeAppend(args, desc); - case "appendCodePoint" -> invokeAppendCodePoint(args, desc); - case "capacity" -> invokeCapacity(args, desc); - case "charAt" -> invokeCharAt(args, desc); - case "chars" -> invokeChars(args, desc); - case "codePointAt" -> invokeCodePointAt(args, desc); - case "codePointBefore" -> invokeCodePointBefore(args, desc); - case "codePointCount" -> invokeCodePointCount(args, desc); - case "codePoints" -> invokeCodePoints(args, desc); - case "compareTo" -> invokeCompareTo(args, desc); - case "delete" -> invokeDelete(args, desc); - case "deleteCharAt" -> invokeDeleteCharAt(args, desc); - case "ensureCapacity" -> invokeEnsureCapacity(args, desc); - case "getChars" -> invokeGetChars(args, desc); - case "indexOf" -> invokeIndexOf(args, desc); - case "insert" -> invokeInsert(args, desc); - case "lastIndexOf" -> invokeLastIndexOf(args, desc); - case "length" -> invokeLength(args, desc); - case "offsetByCodePoints" -> invokeOffsetByCodePoints(args, desc); - case "replace" -> invokeReplace(args, desc); - case "reverse" -> invokeReverse(args, desc); - case "setCharAt" -> invokeSetCharAt(args, desc); - case "setLength" -> invokeSetLength(args, desc); - case "subSequence" -> invokeSubSequence(args, desc); - case "substring" -> invokeSubstring(args, desc); - case "toString" -> invokeToString(args, desc); - case "trimToSize" -> invokeTrimToSize(args, desc); - default -> PlaceHolder.instance; - }; - } - - /** - * Invocation handling for the String instance method Init(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeInit(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { - int numberOfArgs = args.length; - if (numberOfArgs == 0) { - return invokeInit(); - } else if (numberOfArgs == 1) { - return switch (desc[0].getDescriptor()) { - case "I" -> invokeInit(args[0].asIntValue()); - case "Ljava/lang/String;" -> invokeInit(args[0].asStringValue()); - case "Ljava/lang/CharSequence;" -> invokeInit(args[0].asObjectValue()); - default -> PlaceHolder.instance; - }; - } - return PlaceHolder.instance; - } - - private Value invokeInit() { - this.capacity = new IntValue(this.context, 16); - this.stringValue = new StringValue(this.context, "", -1); - return VoidValue.instance; - } - - private Value invokeInit(IntValue capacity) { - this.capacity = capacity; - this.stringValue = new StringValue(this.context, "", -1); - return VoidValue.instance; - } - - private Value invokeInit(@SuppressWarnings("unused") ObjectValue seq) { - return PlaceHolder.instance; - } - - private Value invokeInit(StringValue str) { - this.capacity = new IntValue(this.context, 16 + str.concrete.length()); - this.stringValue = str; - return VoidValue.instance; - } - - /** - * Invocation handling for the String instance method Append(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeAppend(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { - int numberOfArgs = args.length; - if (numberOfArgs == 1) { - return switch (desc[0].getDescriptor()) { - case "I" -> invokeAppend(args[0].asIntValue().asStringValue()); - case "Z" -> invokeAppend(args[0].asBooleanValue().asStringValue()); - case "C" -> invokeAppend(args[0].asCharValue().asStringValue()); - case "D" -> invokeAppend(args[0].asDoubleValue().asStringValue()); - case "F" -> invokeAppend(args[0].asFloatValue().asStringValue()); - case "J" -> invokeAppend(args[0].asLongValue().asStringValue()); - case "Ljava/lang/String;" -> invokeAppend(args[0].asStringValue()); - case "Ljava/lang/CharSequence;", - "Ljava/lang/StringBuffer;", - "Ljava/lang/Object;" -> invokeAppend(args[0].asObjectValue()); - case "[C" -> invokeAppend( - args[0].asObjectValue().asArrayValue().asCharArrayValue()); - default -> PlaceHolder.instance; - }; - } else if (numberOfArgs == 3) { - return switch (desc[0].getDescriptor()) { - case "[C" -> invokeAppend( - args[0].asObjectValue().asArrayValue().asCharArrayValue(), - args[1].asIntValue(), - args[2].asIntValue()); - case "Ljava/lang/CharSequence;" -> invokeAppend( - args[0].asObjectValue(), args[1].asIntValue(), args[2].asIntValue()); + if ((unknown || stringValue == null) && !name.equals("")) return PlaceHolder.instance; + Value result; + try { + result = switch (name) { + case "" -> invokeInit(args, desc); + case "append" -> invokeAppend(args, desc); + case "appendCodePoint" -> invokeAppendCodePoint(args); + case "capacity" -> PlaceHolder.instance; // depends on the growth policy, so taken concretely + case "charAt" -> invokeCharAt(args); + case "compareTo" -> invokeCompareTo(args); + case "delete" -> invokeDelete(args); + case "deleteCharAt" -> invokeDeleteCharAt(args); + case "ensureCapacity", "trimToSize" -> VoidValue.instance; // the chars stay the same + case "getChars" -> invokeGetChars(args); + case "indexOf", "lastIndexOf" -> stringValue.invokeMethod(name, desc, args); + case "insert" -> invokeInsert(args, desc); + case "length" -> new IntValue(context, stringValue.concrete.length(), smgr.length(stringValue.formula)); + case "replace" -> invokeReplace(args); + case "reverse" -> invokeReverse(); + case "setCharAt" -> invokeSetCharAt(args); + case "setLength" -> invokeSetLength(args); + case "subSequence", "substring" -> invokeSubstring(args); + case "toString" -> new StringValue(context, stringValue.concrete, stringValue.formula, -1); default -> PlaceHolder.instance; }; + } catch (NotImplementedException e) { + // e.g. a double appended, which has no model as a String + result = PlaceHolder.instance; } - return PlaceHolder.instance; - } - - private StringBuilderValue invokeAppend(StringValue s) throws NotImplementedException, ValueConversionException { - String desc = "(Ljava.lang.String;)"; - Type[] type = Type.getArgumentTypes(desc); - this.stringValue = - (StringValue) stringValue.invokeMethod("concat", type, new StringValue[] {s}); - return this; - } - - private Value invokeAppend(CharArrayValue str) throws NotImplementedException, ValueConversionException { - int size = str.size.concrete; - for (int i = 0; i < size; i++) { - invokeAppend(str.getElement(new IntValue(str.getContext(), i)).asStringValue()); + if (result instanceof PlaceHolder && MUTATORS.contains(name)) { + unknown = true; } - - return this; + return result; } - private Value invokeAppend(@SuppressWarnings("unused") ObjectValue obj) { - return PlaceHolder.instance; - } - - private Value invokeAppend(ObjectValue obj, IntValue start, IntValue end) { - try { - StringValue s = obj.asStringValue(); - Type[] desc = new Type[] {Type.INT_TYPE, Type.INT_TYPE}; - Value[] args = new Value[] {start, end}; - StringValue substring = (StringValue) s.invokeMethod("substring", desc, args); - return invokeAppend(substring); - } catch (Exception ignored) { - return PlaceHolder.instance; + private Value invokeInit(Value[] args, Type[] desc) { + StringValue chars; + if (args.length == 0 || desc[0].getSort() == Type.INT) { + // new StringBuilder(), new StringBuilder(int capacity) + chars = new StringValue(context, "", -1); + } else if (args.length == 1) { + // new StringBuilder(String), new StringBuilder(CharSequence) + chars = StringValue.charsOf(args[0]); + } else { + chars = null; } + if (chars == null) return PlaceHolder.instance; + this.stringValue = chars; + this.unknown = false; + return VoidValue.instance; } - private Value invokeAppend(CharArrayValue str, IntValue offset, IntValue len) throws NotImplementedException, ValueConversionException { - for (int i = 0; i < len.concrete; i++) { - invokeAppend( - str.getElement(new IntValue(str.getContext(), i + offset.concrete)) - .asStringValue()); - } - - return this; + private void setChars(String concrete, StringFormula formula) { + this.stringValue = new StringValue(context, concrete, formula, -1); } - /** - * Invocation handling for the String instance method AppendCodePoint(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeAppendCodePoint( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private StringValue concat(StringValue a, StringValue b) { + return new StringValue(context, a.concrete + b.concrete, smgr.concat(a.formula, b.formula), -1); } - /** - * Invocation handling for the String instance method Capacity(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCapacity( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return capacity; + private NumeralFormula.IntegerFormula length() { + return smgr.length(stringValue.formula); } - /** - * Invocation handling for the String instance method CharAt(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCharAt(Value[] args, @SuppressWarnings("unused") Type[] desc) throws NotImplementedException, ValueConversionException { - return new CharValue( - context, - this.stringValue.concrete.charAt(args[0].asIntValue().concrete), - this.smgr.charAt(this.stringValue.formula, args[0].asIntValue().asIntegerFormula())); + /** The chars from begin to end of the content. */ + private StringFormula chars(NumeralFormula.IntegerFormula begin, NumeralFormula.IntegerFormula end) { + return smgr.substring(stringValue.formula, begin, imgr.subtract(end, begin)); } /** - * Invocation handling for the String instance method Chars(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance + * The chars a value of type {@code type} is appended or inserted as (String.valueOf), or null + * if that is not modelled. */ - private Value invokeChars( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private StringValue charsOf(Value value, Type type) throws NotImplementedException, ValueConversionException { + return switch (type.getDescriptor()) { + case "I" -> value.asIntValue().asStringValue(); + case "Z" -> value.asBooleanValue().asStringValue(); + case "C" -> value.asCharValue().asStringValue(); + case "J" -> value.asLongValue().asStringValue(); + case "D" -> value.isSymbolic() ? null + : new StringValue(context, String.valueOf(value.asDoubleValue().concrete), -1); + case "F" -> value.isSymbolic() ? null + : new StringValue(context, String.valueOf(value.asFloatValue().concrete), -1); + case "[C" -> value instanceof CharArrayValue array ? array.asStringValue() : null; + default -> objectChars(value); + }; } - /** - * Invocation handling for the String instance method CodePointAt(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCodePointAt( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + /** String.valueOf(obj) for an Object, CharSequence or String argument, or null if not modelled. */ + private StringValue objectChars(Value obj) throws NotImplementedException, ValueConversionException { + if (obj instanceof ObjectValue o && o.isNullValue()) return new StringValue(context, "null", -1); + StringValue chars = StringValue.charsOf(obj); + if (chars != null) return chars; + if (obj instanceof BoxedValue boxed + && boxed.invokeMethod("toString", new Type[0], new Value[0]) instanceof StringValue str) { + return str; + } + return null; } - /** - * Invocation handling for the String instance method CodePointBefore(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCodePointBefore( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private Value invokeAppend(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + StringValue chars; + if (args.length == 1) { + chars = charsOf(args[0], desc[0]); + } else if (args.length == 3 && args[0] instanceof CharArrayValue array) { + // append(char[] str, int offset, int len), by the concrete offset and len (pinned) + int offset = args[1].asIntValue().concrete; + int len = args[2].asIntValue().concrete; + chars = new StringValue(context, "", -1); + for (int i = offset; i < offset + len; i++) { + chars = concat(chars, array.getElement(new IntValue(context, i)).asStringValue()); + } + } else if (args.length == 3 && desc[0].getDescriptor().equals("Ljava/lang/CharSequence;")) { + // append(CharSequence s, int start, int end); s == null appends a part of "null" + StringValue s = objectChars(args[0]); + if (s == null) return PlaceHolder.instance; + IntValue start = args[1].asIntValue(); + IntValue end = args[2].asIntValue(); + chars = new StringValue(context, s.concrete.substring(start.concrete, end.concrete), + smgr.substring(s.formula, start.asIntegerFormula(), + imgr.subtract(end.asIntegerFormula(), start.asIntegerFormula())), -1); + } else { + chars = null; + } + if (chars == null) return PlaceHolder.instance; + setChars(stringValue.concrete + chars.concrete, smgr.concat(stringValue.formula, chars.formula)); + return this; } - /** - * Invocation handling for the String instance method CodePointCount(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCodePointCount( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private Value invokeAppendCodePoint(Value[] args) throws NotImplementedException, ValueConversionException { + // A valid code point (else it throws, which StringCallBranches checks) + IntValue codePoint = args[0].asIntValue(); + String chars = new String(Character.toChars(codePoint.concrete)); + setChars(stringValue.concrete + chars, smgr.concat(stringValue.formula, stringValue.codePointString(codePoint))); + return this; } - /** - * Invocation handling for the String instance method CodePoints(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCodePoints( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private Value invokeCharAt(Value[] args) throws NotImplementedException, ValueConversionException { + IntValue index = args[0].asIntValue(); + return new CharValue(context, stringValue.concrete.charAt(index.concrete), + smgr.charAt(stringValue.formula, index.asIntegerFormula())); } - /** - * Invocation handling for the String instance method CompareTo(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCompareTo( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private Value invokeCompareTo(Value[] args) throws NotImplementedException, ValueConversionException { + // As the Strings of both: compareTo(StringBuilder another) compares lexicographically too. + StringValue other = StringValue.charsOf(args[0]); + if (other == null) return PlaceHolder.instance; + return stringValue.invokeMethod("compareTo", new Type[] {Type.getType(String.class)}, new Value[] {other}); } - /** - * Invocation handling for the String instance method Delete(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeDelete(Value[] args, @SuppressWarnings("unused") Type[] desc) { - IntValue start = (IntValue) args[0]; - IntValue end = (IntValue) args[1]; - NumeralFormula.IntegerFormula remainingLength = - this.imgr.subtract(this.smgr.length(this.stringValue.formula), end.asIntegerFormula()); - this.stringValue.formula = - this.smgr.concat( - this.smgr.substring( - this.stringValue.formula, - new IntValue(context, 0).asIntegerFormula(), - start.asIntegerFormula()), - this.smgr.substring( - this.stringValue.formula, end.asIntegerFormula(), remainingLength)); - StringBuilder deleteBuilder = new StringBuilder(this.stringValue.concrete); - this.stringValue.concrete = deleteBuilder.delete(start.concrete, end.concrete).toString(); + private Value invokeDelete(Value[] args) throws NotImplementedException, ValueConversionException { + IntValue start = args[0].asIntValue(); + IntValue end = args[1].asIntValue(); + // An end past the length deletes up to the end; substring gives "" from there. + NumeralFormula.IntegerFormula e = end.asIntegerFormula(); + setChars(new StringBuilder(stringValue.concrete).delete(start.concrete, end.concrete).toString(), + smgr.concat(chars(imgr.makeNumber(0), start.asIntegerFormula()), + smgr.substring(stringValue.formula, e, imgr.subtract(length(), e)))); return this; } - /** - * Invocation handling for the String instance method DeleteCharAt(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeDeleteCharAt( - Value[] args, @SuppressWarnings("unused") Type[] desc) throws NotImplementedException, ValueConversionException { - IntValue endIndex = - new IntValue( - this.context, - args[0].asIntValue().concrete + 1, - this.imgr.add( - args[0].asIntValue().asIntegerFormula(), - new IntValue(this.context, 1).asIntegerFormula())); - return invokeDelete( - new Value[] {args[0], endIndex}, new Type[] {Type.INT_TYPE, Type.INT_TYPE}); + private Value invokeDeleteCharAt(Value[] args) throws NotImplementedException, ValueConversionException { + IntValue index = args[0].asIntValue(); + IntValue end = new IntValue(context, index.concrete + 1, + imgr.add(index.asIntegerFormula(), imgr.makeNumber(1))); + return invokeDelete(new Value[] {index, end}); } - /** - * Invocation handling for the String instance method EnsureCapacity(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeEnsureCapacity( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method GetChars(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeGetChars( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method IndexOf(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeIndexOf(Value[] args, @SuppressWarnings("unused") Type[] desc) throws NotImplementedException, ValueConversionException { - if (args.length == 1) { - return invokeIndexOf(args[0].asStringValue()); - } else if (args.length == 2) { - return invokeIndexOf(args[0].asStringValue(), args[1].asIntValue()); + private Value invokeGetChars(Value[] args) throws NotImplementedException, ValueConversionException { + // getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin), by the concrete indices (pinned) + if (!(args[2] instanceof CharArrayValue dst)) return PlaceHolder.instance; + int srcBegin = args[0].asIntValue().concrete; + int srcEnd = args[1].asIntValue().concrete; + int dstBegin = args[3].asIntValue().concrete; + for (int i = srcBegin; i < srcEnd; i++) { + dst.storeElement(new IntValue(context, dstBegin + i - srcBegin), + (CharValue) invokeCharAt(new Value[] {new IntValue(context, i)})); } - return PlaceHolder.instance; - } - - private Value invokeIndexOf(StringValue str) { - return new IntValue( - this.context, - this.stringValue.concrete.indexOf(str.concrete), - this.smgr.indexOf( - this.stringValue.formula, - str.formula, - new IntValue(this.context, 0).asIntegerFormula())); - } - - private Value invokeIndexOf(StringValue str, IntValue fromIndex) { - return new IntValue( - this.context, - this.stringValue.concrete.indexOf(str.concrete), - this.smgr.indexOf(this.stringValue.formula, str.formula, fromIndex.asIntegerFormula())); + return VoidValue.instance; } - /** - * Invocation handling for the String instance method Insert(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ private Value invokeInsert(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + IntValue offset = args[0].asIntValue(); + StringValue chars; if (args.length == 2) { - return switch (desc[1].getDescriptor()) { - case "I" -> invokeInsert( - args[0].asIntValue(), args[1].asIntValue().asStringValue()); - case "Z" -> invokeInsert( - args[0].asIntValue(), args[1].asBooleanValue().asStringValue()); - case "C" -> invokeInsert( - args[0].asIntValue(), args[1].asCharValue().asStringValue()); - case "D" -> invokeInsert( - args[0].asIntValue(), args[1].asDoubleValue().asStringValue()); - case "F" -> invokeInsert( - args[0].asIntValue(), args[1].asFloatValue().asStringValue()); - case "J" -> invokeInsert( - args[0].asIntValue(), args[1].asLongValue().asStringValue()); - case "Ljava/lang/String;" -> invokeInsert( - args[0].asIntValue(), args[1].asStringValue()); - case "Ljava/lang/CharSequence;", "Ljava/lang/Object;" -> invokeInsert( - args[0].asIntValue(), args[1].asObjectValue()); - case "[C" -> invokeInsert( - args[0].asIntValue(), - args[1].asObjectValue().asArrayValue().asCharArrayValue()); - default -> PlaceHolder.instance; - }; - } else if (args.length == 4) { - return switch (desc[1].getDescriptor()) { - case "Ljava/lang/CharSequence;" -> invokeInsert( - args[0].asIntValue(), - args[1].asObjectValue(), - args[2].asIntValue(), - args[3].asIntValue()); - case "[C" -> invokeInsert( - args[0].asIntValue(), - args[1].asObjectValue().asArrayValue().asCharArrayValue(), - args[2].asIntValue(), - args[3].asIntValue()); - default -> PlaceHolder.instance; - }; - } - return PlaceHolder.instance; - } - - private Value invokeInsert(IntValue offset, StringValue str) { - this.stringValue.formula = - this.smgr.concat( - smgr.substring( - this.stringValue.formula, - new IntValue(this.context, 0).asIntegerFormula(), - offset.asIntegerFormula()), - str.formula, - smgr.substring( - this.stringValue.formula, - offset.asIntegerFormula(), - smgr.length(stringValue.formula))); - this.stringValue.concrete = - this.stringValue - .concrete - .substring(0, offset.concrete) - .concat(String.valueOf(str.concrete)) - .concat(this.stringValue.concrete.substring(offset.concrete)); - return this; - } - - private Value invokeInsert( - @SuppressWarnings("unused") IntValue offset, - @SuppressWarnings("unused") ObjectValue obj) { - return PlaceHolder.instance; - } - - private Value invokeInsert(IntValue offset, CharArrayValue str) throws NotImplementedException, ValueConversionException { - int size = str.size.concrete; - StringValue newStr = new StringValue(this.context, "", -1); - for (int i = 0; i < size; i++) { - newStr.invokeMethod( - "concat", - new Type[] {Type.getType("Ljava/lang/String;")}, - new Value[] { - str.getElement(new IntValue(str.getContext(), i)).asStringValue() - }); + chars = charsOf(args[1], desc[1]); + } else if (args.length == 4 && args[1] instanceof CharArrayValue array) { + // insert(int index, char[] str, int offset, int len), by the concrete offset and len (pinned) + int from = args[2].asIntValue().concrete; + int len = args[3].asIntValue().concrete; + chars = new StringValue(context, "", -1); + for (int i = from; i < from + len; i++) { + chars = concat(chars, array.getElement(new IntValue(context, i)).asStringValue()); + } + } else if (args.length == 4 && desc[1].getDescriptor().equals("Ljava/lang/CharSequence;")) { + // insert(int dstOffset, CharSequence s, int start, int end) + StringValue s = objectChars(args[1]); + if (s == null) return PlaceHolder.instance; + IntValue start = args[2].asIntValue(); + IntValue end = args[3].asIntValue(); + chars = new StringValue(context, s.concrete.substring(start.concrete, end.concrete), + smgr.substring(s.formula, start.asIntegerFormula(), + imgr.subtract(end.asIntegerFormula(), start.asIntegerFormula())), -1); + } else { + chars = null; } - invokeInsert(offset, newStr); + if (chars == null) return PlaceHolder.instance; + NumeralFormula.IntegerFormula off = offset.asIntegerFormula(); + String c = stringValue.concrete; + setChars(c.substring(0, offset.concrete) + chars.concrete + c.substring(offset.concrete), + smgr.concat(chars(imgr.makeNumber(0), off), chars.formula, chars(off, length()))); return this; } - private Value invokeInsert( - IntValue index, CharArrayValue str, IntValue offset, IntValue len) throws NotImplementedException, ValueConversionException { - StringValue newStr = new StringValue(this.context, "", -1); - for (int i = 0; i < len.concrete; i++) { - newStr.invokeMethod( - "concat", - new Type[] {Type.getType("Ljava/lang/String;")}, - new Value[] { - str.getElement(new IntValue(str.getContext(), i + offset.concrete)) - .asStringValue() - }); - } - invokeInsert(index, newStr); + private Value invokeReplace(Value[] args) throws NotImplementedException, ValueConversionException { + // replace(int start, int end, String str); an end past the length replaces up to the end + if (!(args[2] instanceof StringValue str)) return PlaceHolder.instance; + IntValue start = args[0].asIntValue(); + IntValue end = args[1].asIntValue(); + NumeralFormula.IntegerFormula e = end.asIntegerFormula(); + setChars(new StringBuilder(stringValue.concrete).replace(start.concrete, end.concrete, str.concrete).toString(), + smgr.concat(chars(imgr.makeNumber(0), start.asIntegerFormula()), str.formula, + smgr.substring(stringValue.formula, e, imgr.subtract(length(), e)))); return this; } - private Value invokeInsert( - @SuppressWarnings("unused") IntValue index, - @SuppressWarnings("unused") ObjectValue str, - @SuppressWarnings("unused") IntValue offset, - @SuppressWarnings("unused") IntValue len) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method LastIndexOf(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeLastIndexOf( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method Length(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeLength( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return new IntValue( - this.context, - this.stringValue.concrete.length(), - this.smgr.length(this.stringValue.formula)); - } - - /** - * Invocation handling for the String instance method OffsetByCodePoints(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeOffsetByCodePoints( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method Replace(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeReplace(Value[] args, @SuppressWarnings("unused") Type[] desc) { - IntValue start = (IntValue) args[0]; - IntValue end = (IntValue) args[1]; - StringValue replacement = (StringValue) args[2]; - StringFormula substring = - this.smgr.substring( - this.stringValue.formula, - start.asIntegerFormula(), - this.imgr.subtract(end.asIntegerFormula(), start.asIntegerFormula())); - this.stringValue.formula = - smgr.replace(this.stringValue.formula, substring, replacement.formula); - StringBuilder builderReplace = new StringBuilder(this.stringValue.concrete); - this.stringValue.concrete = - builderReplace - .replace(start.concrete, end.concrete, replacement.concrete) - .toString(); + private Value invokeReverse() { + // Only concrete chars: a symbolic string cannot be reversed in the string theory. + if (stringValue.isSymbolic()) return PlaceHolder.instance; + setChars(new StringBuilder(stringValue.concrete).reverse().toString(), + smgr.makeString(new StringBuilder(stringValue.concrete).reverse().toString())); return this; } - /** - * Invocation handling for the String instance method Reverse(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeReverse( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method SetCharAt(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeSetCharAt( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - /* - IntValue index = args[0].asIntValue(); - CharValue newChar = args[1].asCharValue(); - - NumeralFormula.IntegerFormula secondIndex = this.imgr.add(index.formula, new IntValue(this.context, 1).formula); - NumeralFormula.IntegerFormula lengthOfSecondSubstring = - this.imgr.subtract(this.smgr.length(this.stringValue.formula), secondIndex); - this.stringValue.formula = this.smgr.concat( - this.smgr.substring(this.stringValue.formula, new IntValue(this.context, 0).formula, index.formula), - newChar.formula, - this.smgr.substring(this.stringValue.formula, this.imgr.add(index.formula, secondIndex), lengthOfSecondSubstring)); - - StringBuilder builderSetCharAt = new StringBuilder(this.stringValue.concrete); - builderSetCharAt.setCharAt(index.concrete, newChar.concrete); - this.stringValue.concrete = builderSetCharAt.toString(); - } - */ - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method SetLength(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeSetLength(Value[] args, @SuppressWarnings("unused") Type[] desc) - throws NotImplementedException, ValueConversionException { - IntValue newLength = args[0].asIntValue(); - if (newLength.isSymbolic() || newLength.concrete < 0) { - return PlaceHolder.instance; // a symbolic length is not modelled - } - int n = newLength.concrete; - int length = this.stringValue.concrete.length(); - if (n <= length) { - // Truncation, e.g. setLength(0) to reuse the builder - this.stringValue.formula = this.smgr.substring(this.stringValue.formula, - new IntValue(context, 0).asIntegerFormula(), newLength.asIntegerFormula()); - this.stringValue.concrete = this.stringValue.concrete.substring(0, n); - } else { - // Growing pads with null characters - String padding = "\0".repeat(n - length); - this.stringValue.formula = this.smgr.concat(this.stringValue.formula, this.smgr.makeString(padding)); - this.stringValue.concrete = this.stringValue.concrete + padding; - } + private Value invokeSetCharAt(Value[] args) throws NotImplementedException, ValueConversionException { + IntValue index = args[0].asIntValue(); + CharValue ch = args[1].asCharValue(); + NumeralFormula.IntegerFormula i = index.asIntegerFormula(); + StringBuilder sb = new StringBuilder(stringValue.concrete); + sb.setCharAt(index.concrete, ch.concrete); + setChars(sb.toString(), smgr.concat(chars(imgr.makeNumber(0), i), ch.asStringValue().formula, + chars(imgr.add(i, imgr.makeNumber(1)), length()))); return VoidValue.instance; } - /** - * Invocation handling for the String instance method SubSequence(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeSubSequence( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method Substring(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeSubstring( - Value[] args, @SuppressWarnings("unused") Type[] desc) throws NotImplementedException, ValueConversionException { - if (args.length == 1) { - return invokeSubstring(args[0].asIntValue()); - } else if (args.length == 2) { - return invokeSubstring(args[0].asIntValue(), args[1].asIntValue()); - } - return PlaceHolder.instance; + private Value invokeSetLength(Value[] args) throws NotImplementedException, ValueConversionException { + // By the concrete length (pinned): the first n chars of the content padded with n '\0's. + int n = args[0].asIntValue().concrete; + StringBuilder sb = new StringBuilder(stringValue.concrete); + sb.setLength(n); + setChars(sb.toString(), smgr.substring(smgr.concat(stringValue.formula, smgr.makeString("\0".repeat(n))), + imgr.makeNumber(0), imgr.makeNumber(n))); + return VoidValue.instance; } - private Value invokeSubstring(IntValue start) { - NumeralFormula.IntegerFormula remainingLength = - this.imgr.subtract(this.smgr.length(this.stringValue.formula), start.asIntegerFormula()); - this.stringValue.formula = - this.smgr.substring(this.stringValue.formula, start.asIntegerFormula(), remainingLength); - this.stringValue.concrete = this.stringValue.concrete.substring(start.concrete); - return new StringValue( - this.context, this.stringValue.concrete, this.stringValue.formula, -1); + private Value invokeSubstring(Value[] args) throws NotImplementedException, ValueConversionException { + // substring(start) is substring(start, length()); subSequence(start, end) is substring(start, end) + if (args.length != 1 && args.length != 2) return PlaceHolder.instance; + IntValue start = args[0].asIntValue(); + IntValue end = args.length == 2 ? args[1].asIntValue() + : new IntValue(context, stringValue.concrete.length(), length()); + return new StringValue(context, stringValue.concrete.substring(start.concrete, end.concrete), + chars(start.asIntegerFormula(), end.asIntegerFormula()), -1); } - private Value invokeSubstring(IntValue start, IntValue end) { - this.stringValue.formula = - this.smgr.substring(this.stringValue.formula, start.asIntegerFormula(), end.asIntegerFormula()); - this.stringValue.concrete = - this.stringValue.concrete.substring(start.concrete, end.concrete); - return new StringValue( - this.context, this.stringValue.concrete, this.stringValue.formula, -1); + @Override + public boolean isSymbolic() { + return stringValue != null && stringValue.isSymbolic(); } - /** - * Invocation handling for the String instance method ToString(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeToString( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return new StringValue( - this.context, this.stringValue.concrete, this.stringValue.formula, -1); + @Override + public boolean isSymbolic(Set> visited) { + return isSymbolic(); } - /** - * Invocation handling for the String instance method TrimToSize(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeTrimToSize( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + @Override + public ImmutableSet getSymbolicVariables() { + return stringValue == null ? ImmutableSet.of() : stringValue.getSymbolicVariables(); } @Override - public StringValue asStringValue() { + public StringValue asStringValue() throws NotImplementedException { + if (unknown || stringValue == null) { + throw new NotImplementedException("The chars of this StringBuilder are not known"); + } return this.stringValue; } @@ -896,6 +397,7 @@ public String toString() { return "Ljava/lang/StringBuilder @" + Integer.toHexString(address) + + (unknown ? " (unknown)" : "") + " (" + concreteString + ", " From ae837363be39e6fa32e5d8bc96a8f8ab17825284 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 22:25:24 +0000 Subject: [PATCH 3/5] Do not count the exactly defined String UFs as precision loss compareTo, trim and lastIndexOf introduce UFs (commonPrefixLength, trimStart, trimEnd, lastIndexOf) that a trace constraint defines exactly for any arguments, so a branch over them is as exact as one over the inputs. Co-Authored-By: Claude Opus 5.5 --- .../java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java index e272cf71..b202d940 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java @@ -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; @@ -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 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) { From 0df4738ceff640c675591d1c62c3dcfe4c9c431d Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 22:26:06 +0000 Subject: [PATCH 4/5] Test that the String and StringBuilder models are exact L0: each model, applied to symbolic strings and ints, admits only Java's result once the variables are fixed to a sample (for compareTo only that it admits Java's); the index checks hold iff Java does not throw. L2: a forked agent run records the index check of charAt on both sides, and no context loss when it throws. Co-Authored-By: Claude Opus 5.5 --- .../symbolic/StringIndexCheckAgentSpec.groovy | 92 +++ .../lang/StringModelExactnessTest.groovy | 650 ++++++++++++++++++ .../targets/svcomp-strings/Main.java | 17 + 3 files changed, 759 insertions(+) create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StringIndexCheckAgentSpec.groovy create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy create mode 100644 symbolic-executor/src/test/resources/targets/svcomp-strings/Main.java diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StringIndexCheckAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StringIndexCheckAgentSpec.groovy new file mode 100644 index 00000000..c746d25e --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StringIndexCheckAgentSpec.groovy @@ -0,0 +1,92 @@ +package de.uzl.its.swat.symbolic + +import com.fasterxml.jackson.databind.ObjectMapper +import spock.lang.Shared +import spock.lang.Specification + +import javax.tools.ToolProvider +import java.nio.file.Files +import java.nio.file.Path +import java.util.concurrent.TimeUnit + +/** + * L2 (forked agent): the index check of String.charAt is a branch of the trace, on both sides. A + * tiny SV-COMP style target calls charAt(5) on a nondet string and catches the exception; it is run + * with the agent in {@code solver.mode=PRINT}, once with the default input "fixed" (too short: the + * call throws) and once with a longer one. Runs via the {@code agentTest} Gradle task (needs the + * agent jar from {@code copyJar}). + */ +class StringIndexCheckAgentSpec extends Specification { + + static final Path AGENT_JAR = Path.of("lib", "symbolic-executor.jar").toAbsolutePath() + static final Path NATIVE_LIBS = Path.of("..", "libs", "java-library-path").toAbsolutePath() + static final Path TARGETS = Path.of("src", "test", "resources", "targets").toAbsolutePath() + + @Shared Path classes + @Shared Map shortTrace + @Shared Map longTrace + + def setupSpec() { + assert Files.isRegularFile(AGENT_JAR): "agent jar missing, run copyJar first: ${AGENT_JAR}" + classes = Files.createTempDirectory("swat-string-index-agent-spec") + compile(classes) + shortTrace = parseTrace(run(classes, [])) + longTrace = parseTrace(run(classes, ["-Dswat.input.java/lang/String_0=abcdefgh"])) + } + + def cleanupSpec() { + classes?.toFile()?.deleteDir() + } + + private static List indexChecks(Map trace) { + return trace.trace.findAll { it.callback && it.constraint?.contains("str.len") } + } + + def "a call that throws at the index check records the failed check, not a context loss"() { + expect: + indexChecks(shortTrace).size() == 1 + !indexChecks(shortTrace)[0].branched + !shortTrace.symbolicContextLoss + } + + def "a call that returns records the check as held"() { + expect: + indexChecks(longTrace).size() == 1 + indexChecks(longTrace)[0].branched + !longTrace.symbolicContextLoss + } + + private static void compile(Path outDir) { + def sources = [TARGETS.resolve("svcomp-strings/Main.java"), + TARGETS.resolve("svcomp/org/sosy_lab/sv_benchmarks/Verifier.java")]*.toString() + def args = ["-source", "1.8", "-target", "1.8", "-g", "-d", outDir.toString()] + sources + def err = new ByteArrayOutputStream() + int rc = ToolProvider.getSystemJavaCompiler().run(null, null, err, args as String[]) + assert rc == 0: "javac failed: ${err}" + } + + private static String run(Path classes, List inputs) { + def java = Path.of(System.getProperty("java.home"), "bin", "java").toString() + def cmd = [java, + "-javaagent:${AGENT_JAR}".toString(), + "-Djava.library.path=${NATIVE_LIBS}".toString(), + "-Dconfig.path=/nonexistent/swat.cfg", + "-Dinstrumentation.transformer=SV_COMP", + "-Dsolver.mode=PRINT", + "-DexitOnError=false", + "-DlogShadowStateToConsole=false"] + inputs + + ["-cp", classes.toString(), "-ea", "Main"] + def proc = new ProcessBuilder(cmd).directory(classes.toFile()).redirectErrorStream(true).start() + def out = proc.inputStream.text + assert proc.waitFor(5, TimeUnit.MINUTES): "target did not finish:\n${out}" + return out + } + + /** The TraceDTO is the single pretty-printed JSON object whose braces start at column 0. */ + private static Map parseTrace(String out) { + int start = out.indexOf("\n{\n") + int end = out.indexOf("\n}\n", start) + assert start >= 0 && end > start: "no trace JSON in output:\n${out}" + return new ObjectMapper().readValue(out.substring(start + 1, end + 2), Map) + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy new file mode 100644 index 00000000..db356254 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy @@ -0,0 +1,650 @@ +package de.uzl.its.value.reference.lang + +import de.uzl.its.swat.symbolic.invoke.java.lang.StringCallBranches +import de.uzl.its.swat.symbolic.value.PlaceHolder +import de.uzl.its.swat.symbolic.value.Value +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.BooleanValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.CharValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.LongValue +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 de.uzl.its.swat.thread.ThreadHandler +import org.objectweb.asm.Type +import org.sosy_lab.java_smt.api.* +import spock.lang.Specification +import spock.lang.Unroll + +import static java.lang.Thread.currentThread + +/** + * L0: the String and StringBuilder models are exact. A model is applied to a symbolic string (and + * symbolic ints); then, with the variables fixed to a sample, the solver must not find a result + * other than Java's. A model that is too strict there would make the solver call a feasible path + * infeasible: a false SAFE. + */ +class StringModelExactnessTest extends Specification { + + SolverContext context + ProverEnvironment prover + FormulaManager fmgr + BooleanFormulaManager bmgr + IntegerFormulaManager imgr + StringFormulaManager smgr + BitvectorFormulaManager bvmgr + + static final Type STRING = Type.getType(String) + static final Type CHAR_SEQUENCE = Type.getType(CharSequence) + static final Type OBJECT = Type.getType(Object) + static final Type INT = Type.INT_TYPE + + static final List SAMPLES = ["", "a", "abc", "aXa", "97", "xaxax", "a😀b", " \t pad \n", "aaaaaaaaaaaaaaa"] + + def setup() { + ThreadHandler.init() + if (ThreadHandler.hasThreadContext(currentThread().id)) { + ThreadHandler.removeThreadContext(currentThread().id) + } + ThreadHandler.addThreadContext(currentThread().id, "Test-Thread", -2) + context = ThreadHandler.getSolverContext(currentThread().id) + prover = context.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS) + fmgr = context.formulaManager + bmgr = fmgr.booleanFormulaManager + imgr = fmgr.integerFormulaManager + smgr = fmgr.stringFormulaManager + bvmgr = fmgr.bitvectorFormulaManager + } + + def cleanup() { + prover.close() + context.close() + ThreadHandler.removeThreadContext(currentThread().id) + } + + // ---- helpers ---- + + /** A Java string as the solver sees it: one SMT char per UTF-16 char (makeString would join surrogate pairs). */ + private StringFormula chars(String s) { + StringFormula f = smgr.makeString("") + for (char c : s.toCharArray()) { + f = smgr.concat(f, smgr.fromCodePoint(imgr.makeNumber((int) c))) + } + return f + } + + private StringValue symbolicString(String name, String concrete) { + return new StringValue(context, concrete, smgr.makeVariable(name), -1) + } + + private IntValue symbolicInt(String name, int concrete) { + return new IntValue(context, concrete, bvmgr.makeVariable(32, name)) + } + + private BooleanFormula fixString(StringValue v, String sample) { + return smgr.equal(v.formula, chars(sample)) + } + + private BooleanFormula fixInt(IntValue v, int sample) { + return bvmgr.equal(v.formula, bvmgr.makeBitvector(32, sample)) + } + + private boolean precisionLoss() { + return ThreadHandler.getSymbolicTraceHandler(currentThread().id).symbolicTrace.symbolicPrecisionLoss + } + + /** Whether, under the given fixing constraints (and the definitions of the UFs), `other` is unsatisfiable. */ + private boolean onlyJavasResult(List fixed, BooleanFormula other) { + // A fresh prover per query: after a push, Z3's incremental mode gets stuck on some of them. + context.newProverEnvironment().withCloseable { p -> + ThreadHandler.getSymbolicTraceHandler(currentThread().id).getConstraints().each { p.addConstraint(it) } + fixed.each { p.addConstraint(it) } + p.addConstraint(other) + return p.isUnsat() + } + } + + /** + * Whether, under the given fixing constraints, Java's result is possible: the direction that + * matters for soundness (the converse, that it is the only one, Z3 cannot always show for UFs). + */ + private boolean allowsJava(List fixed, BooleanFormula java) { + return !onlyJavasResult(fixed, java) + } + + private boolean exactInt(List fixed, IntValue result, int java) { + return onlyJavasResult(fixed, bmgr.not(imgr.equal(result.asIntegerFormula(), imgr.makeNumber(java)))) + } + + private boolean exactBoolean(List fixed, BooleanValue result, boolean java) { + return onlyJavasResult(fixed, java ? bmgr.not(result.formula) : result.formula) + } + + private boolean exactString(List fixed, StringFormula result, String java) { + return onlyJavasResult(fixed, bmgr.not(smgr.equal(result, chars(java)))) + } + + private Value call(Value receiver, String name, List desc, List> args) { + return ((ObjectValue) receiver).invokeMethod(name, desc as Type[], args as Value[]) + } + + // ---- String ---- + + @Unroll + def "indexOf(int ch) and indexOf(int ch, int from) search for the char, not its digits: #sample, #ch, #from"() { + given: + def s = symbolicString("s", "fixed") + def c = symbolicInt("ch", 97) + def f = symbolicInt("from", 0) + def fixed = [fixString(s, sample), fixInt(c, ch), fixInt(f, from)] + + when: + def one = (IntValue) call(s, "indexOf", [INT], [c]) + def two = (IntValue) call(s, "indexOf", [INT, INT], [c, f]) + + then: + exactInt(fixed, one, sample.indexOf(ch)) + exactInt(fixed, two, sample.indexOf(ch, from)) + + where: + [sample, ch, from] << [["", "a", "aXa", "97", "a\uD83D\uDE00b"], [(int) 'a', (int) '9', -1, 0x1F600, 0xD83D, 0x110000], + [-3, 0, 2]].combinations() + } + + def "indexOf('a') on a concrete char has the Java result concretely"() { + expect: + ((IntValue) call(new StringValue(context, "xab", -1), "indexOf", [INT], [new IntValue(context, (int) 'a')])).concrete == 1 + ((IntValue) call(new StringValue(context, "x97a", -1), "indexOf", [INT, INT], [new IntValue(context, (int) 'a'), new IntValue(context, 0)])).concrete == 3 + } + + @Unroll + def "lastIndexOf(int ch, int from) is exact, with the char pinned: #sample, #ch, #from"() { + given: + def s = symbolicString("s", "fixed") + def c = symbolicInt("ch", ch) + def f = symbolicInt("from", 0) + def pins = StringCallBranches.of(s, "lastIndexOf", "(II)I", [c, f] as Value[]) + def fixed = [fixString(s, sample), fixInt(f, from)] + pins*.condition() + + when: + def r = (IntValue) call(s, "lastIndexOf", [INT, INT], [c, f]) + + then: + exactInt(fixed, r, sample.lastIndexOf(ch, from)) + + where: + [sample, ch, from] << [["", "a", "aXa", "a\uD83D\uDE00b"], [(int) 'a', -1, 0x1F600, 0x110000], [-1, 0, 2, 100]].combinations() + } + + @Unroll + def "lastIndexOf(String str, int from) is exact: #sample, #target, #from"() { + given: + def s = symbolicString("s", "fixed") + def t = symbolicString("t", "x") + def f = symbolicInt("from", 0) + def fixed = [fixString(s, sample), fixString(t, target), fixInt(f, from)] + + when: + def r = (IntValue) call(s, "lastIndexOf", [STRING, INT], [t, f]) + + then: + exactInt(fixed, r, sample.lastIndexOf(target, from)) + + where: + [sample, target, from] << [["", "aXa", "xaxax"], ["", "a", "xa"], [-1, 0, 3, 100]].combinations() + } + + @Unroll + def "indexOf(String str, int from) is exact: #sample, #target, #from"() { + given: + def s = symbolicString("s", "fixed") + def t = symbolicString("t", "x") + def f = symbolicInt("from", 0) + def fixed = [fixString(s, sample), fixString(t, target), fixInt(f, from)] + + when: + def r = (IntValue) call(s, "indexOf", [STRING, INT], [t, f]) + + then: + exactInt(fixed, r, sample.indexOf(target, from)) + + where: + [sample, target, from] << [["", "aXa", "xaxax"], ["", "a", "xa"], [-1, 0, 3, 100]].combinations() + } + + @Unroll + def "startsWith(String prefix, int toffset) is false for an offset out of range: #sample, #prefix, #offset"() { + given: + def s = symbolicString("s", "fixed") + def p = symbolicString("p", "x") + def o = symbolicInt("o", 0) + def fixed = [fixString(s, sample), fixString(p, prefix), fixInt(o, offset)] + + when: + def r = (BooleanValue) call(s, "startsWith", [STRING, INT], [p, o]) + + then: + exactBoolean(fixed, r, sample.startsWith(prefix, offset)) + + where: + [sample, prefix, offset] << [["", "abc"], ["", "a", "abc"], [-1, 0, 1, 3, 4]].combinations() + } + + def "startsWith(String prefix, int toffset) has the concrete result of the offset"() { + expect: + ((BooleanValue) call(new StringValue(context, "tested", -1), "startsWith", [STRING, INT], + [new StringValue(context, "ste", -1), new IntValue(context, 2)])).concrete + } + + @Unroll + def "replace(CharSequence, CharSequence) replaces every occurrence: #sample, #target -> #replacement"() { + given: + def s = symbolicString("s", "fixed") + def fixed = [fixString(s, sample)] + + when: + def r = (StringValue) call(s, "replace", [CHAR_SEQUENCE, CHAR_SEQUENCE], + [new StringValue(context, target, -1), new StringValue(context, replacement, -1)]) + + then: + exactString(fixed, r.formula, sample.replace(target, replacement)) + !precisionLoss() + + where: + [sample, target, replacement] << [["", "aaaaaaaaaaaaaaa", "xaxax"], ["a", "aa", "xa"], ["", "aa"]].combinations() + } + + def "replace(char, char) replaces more than ten occurrences"() { + given: + def s = symbolicString("s", "fixed") + def sample = "a" * 25 + "b" + "a" * 3 + + when: + def r = (StringValue) call(s, "replace", [Type.CHAR_TYPE, Type.CHAR_TYPE], + [new CharValue(context, 'a' as char), new CharValue(context, 'c' as char)]) + + then: + exactString([fixString(s, sample)], r.formula, sample.replace('a' as char, 'c' as char)) + !precisionLoss() + } + + def "replace with an empty or a symbolic target is not modelled exactly"() { + when: + call(symbolicString("s", "ab"), "replace", [CHAR_SEQUENCE, CHAR_SEQUENCE], + [new StringValue(context, "", -1), new StringValue(context, "-", -1)]) + + then: + precisionLoss() + } + + @Unroll + def "trim() is exact: '#sample'"() { + given: + def s = symbolicString("s", "fixed") + + when: + def r = (StringValue) call(s, "trim", [], []) + + then: + exactString([fixString(s, sample)], r.formula, sample.trim()) + + where: + sample << SAMPLES + [" ", "\u0000a\u0000", " a b "] + } + + @Unroll + def "compareTo(String) allows the Java result: #a vs #b"() { + given: + def s = symbolicString("s", "fixed") + def t = symbolicString("t", "fixed") + + when: + def r = (IntValue) call(s, "compareTo", [STRING], [t]) + + then: + allowsJava([fixString(s, a), fixString(t, b)], imgr.equal(r.asIntegerFormula(), imgr.makeNumber(a.compareTo(b)))) + // (That it is the only one, Z3 does not show within reasonable time for some samples.) + + where: + // (Some samples, e.g. "B" vs "abd", take Z3 minutes even to satisfy.) + [a, b] << [["", "a", "ab"], ["", "a", "abd"]].combinations() + } + + @Unroll + def "regionMatches(int, String, int, int) is exact: #toffset #ooffset #len"() { + given: + def s = symbolicString("s", "fixed") + def o = symbolicString("o", "fixed") + def t = symbolicInt("t", 0) + def oo = symbolicInt("oo", 0) + def l = symbolicInt("l", 0) + def fixed = [fixString(s, "abcab"), fixString(o, "xab"), fixInt(t, toffset), fixInt(oo, ooffset), fixInt(l, len)] + + when: + def r = (BooleanValue) call(s, "regionMatches", [INT, STRING, INT, INT], [t, o, oo, l]) + + then: + exactBoolean(fixed, r, "abcab".regionMatches(toffset, "xab", ooffset, len)) + + where: + [toffset, ooffset, len] << [[-1, 0, 3], [-1, 1, 2], [-1, 0, 2]].combinations() + } + + def "equals(StringBuilder) and equals(null) are false"() { + given: + def s = new StringValue(context, "ab", -1) + def sb = new StringBuilderValue(context, new StringValue(context, "ab", -1), -1) + + expect: + call(s, "equals", [OBJECT], [sb]) == PlaceHolder.instance + !((BooleanValue) call(s, "equals", [OBJECT], [new ObjectValue(context, ObjectValue.ADDRESS_NULL)])).concrete + } + + def "contentEquals(StringBuilder) compares the chars"() { + given: + def s = symbolicString("s", "ab") + def sb = new StringBuilderValue(context, new StringValue(context, "ab", -1), -1) + + when: + def r = (BooleanValue) call(s, "contentEquals", [CHAR_SEQUENCE], [sb]) + + then: + r.concrete + exactBoolean([fixString(s, "ab")], r, true) + exactBoolean([fixString(s, "abc")], r, false) + } + + def "getChars copies to the destination offset"() { + given: + def s = new StringValue(context, "abcdef", -1) + def dst = new CharArrayValue(context, new IntValue(context, 4), -1) + + when: + call(s, "getChars", [INT, INT, Type.getType(char[]), INT], + [new IntValue(context, 2), new IntValue(context, 4), dst, new IntValue(context, 1)]) + + then: + (0..3).collect { dst.getElement(new IntValue(context, it)).concrete } == ['\u0000', 'c', 'd', '\u0000'].collect { it as char } + } + + def "toCharArray of the empty string is an empty array"() { + expect: + ((CharArrayValue) call(new StringValue(context, "", -1), "toCharArray", [], [])).size.concrete == 0 + } + + def "new String(char[]) takes the chars of the array"() { + given: + def s = new StringValue(context, "", -1) + def array = new CharArrayValue(context, "hi".toCharArray(), -1) + + when: + call(s, "", [Type.getType(char[])], [array]) + + then: + s.concrete == "hi" + exactString([], s.formula, "hi") + } + + @Unroll + def "long #v and short #v as a String keep their sign"() { + given: + def l = new LongValue(context, (long) v, bvmgr.makeVariable(64, "l")) + + when: + def r = l.asStringValue() + + then: + exactString([bvmgr.equal(l.formula, bvmgr.makeBitvector(64, (long) v))], r.formula, String.valueOf((long) v)) + + where: + v << [0L, 7L, -7L, Long.MIN_VALUE, Long.MAX_VALUE] + } + + // ---- StringBuilder ---- + + private StringBuilderValue builder(StringValue chars) { + return new StringBuilderValue(context, chars, -1) + } + + @Unroll + def "setLength(#n) truncates or pads a symbolic builder: '#sample'"() { + given: + def s = symbolicString("s", "fixed") + def sb = builder(s) + + when: + call(sb, "setLength", [INT], [new IntValue(context, n)]) + + then: + def java = new StringBuilder(sample) + java.setLength(n) + exactString([fixString(s, sample)], sb.content.formula, java.toString()) + + where: + [sample, n] << [["", "ab", "abcdef"], [0, 1, 3, 5]].combinations() + } + + def "substring does not change the builder, and substring(start, end) takes end - start chars"() { + given: + def s = symbolicString("s", "abcdefgh") + def sb = builder(s) + + when: + def sub = (StringValue) call(sb, "substring", [INT, INT], [new IntValue(context, 2), new IntValue(context, 5)]) + def rest = (StringValue) call(sb, "substring", [INT], [new IntValue(context, 6)]) + + then: + sub.concrete == "cde" + rest.concrete == "gh" + sb.content.concrete == "abcdefgh" + exactString([fixString(s, "abcdefgh")], sub.formula, "cde") + exactString([fixString(s, "abcdefgh")], sb.content.formula, "abcdefgh") + } + + def "a builder made from a String does not change that String"() { + given: + def s = new StringValue(context, "abc", -1) + def sb = builder(s) + + when: + call(sb, "deleteCharAt", [INT], [new IntValue(context, 0)]) + call(sb, "insert", [INT, STRING], [new IntValue(context, 0), new StringValue(context, "x", -1)]) + + then: + s.concrete == "abc" + exactString([], s.formula, "abc") + sb.content.concrete == "xbc" + } + + @Unroll + def "replace(#start, #end, str) replaces that range: '#sample'"() { + given: + def s = symbolicString("s", "fixed") + def sb = builder(s) + + when: + call(sb, "replace", [INT, INT, STRING], [new IntValue(context, start), new IntValue(context, end), new StringValue(context, "XY", -1)]) + + then: + exactString([fixString(s, sample)], sb.content.formula, new StringBuilder(sample).replace(start, end, "XY").toString()) + + where: + [sample, start, end] << [["abab", "abcdef"], [0, 1, 2], [2, 3, 10]].combinations() + } + + @Unroll + def "delete(#start, #end) is exact: '#sample'"() { + given: + def s = symbolicString("s", "fixed") + def sb = builder(s) + + when: + call(sb, "delete", [INT, INT], [new IntValue(context, start), new IntValue(context, end)]) + + then: + exactString([fixString(s, sample)], sb.content.formula, new StringBuilder(sample).delete(start, end).toString()) + + where: + [sample, start, end] << [["abab", "abcdef"], [0, 1, 2], [2, 3, 10]].combinations() + } + + def "indexOf(String, int) of a builder uses the from index"() { + given: + def s = symbolicString("s", "xaxa") + def f = symbolicInt("f", 2) + + when: + def r = (IntValue) call(builder(s), "indexOf", [STRING, INT], [new StringValue(context, "a", -1), f]) + + then: + r.concrete == 3 + exactInt([fixString(s, "xaxa"), fixInt(f, 2)], r, 3) + exactInt([fixString(s, "xaxa"), fixInt(f, -4)], r, 1) + } + + def "setCharAt is modelled"() { + given: + def s = symbolicString("s", "Hello") + def sb = builder(s) + + when: + call(sb, "setCharAt", [INT, Type.CHAR_TYPE], [new IntValue(context, 1), new CharValue(context, 'a' as char)]) + + then: + sb.content.concrete == "Hallo" + exactString([fixString(s, "Hello")], sb.content.formula, "Hallo") + exactString([fixString(s, "xy")], sb.content.formula, "xa") + } + + def "append(Object) appends a String, a builder and null"() { + given: + def sb = builder(new StringValue(context, "a", -1)) + + when: + call(sb, "append", [OBJECT], [new StringValue(context, "b", -1)]) + call(sb, "append", [CHAR_SEQUENCE], [builder(new StringValue(context, "c", -1))]) + call(sb, "append", [OBJECT], [new ObjectValue(context, ObjectValue.ADDRESS_NULL)]) + call(sb, "append", [Type.DOUBLE_TYPE], [new de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue(context, 1.5d)]) + + then: + sb.content.concrete == "abcnull1.5" + !sb.unknown + } + + def "after a change that is not modelled the chars are unknown, until resynced"() { + given: + def sb = builder(symbolicString("s", "ab")) + + when: + call(sb, "reverse", [], []) + + then: + sb.unknown + sb.symbolic + call(sb, "length", [], []) == PlaceHolder.instance + call(sb, "toString", [], []) == PlaceHolder.instance + + when: + sb.resync("ba") + + then: + !sb.unknown + ((StringValue) call(sb, "toString", [], [])).concrete == "ba" + } + + def "a builder with symbolic chars is symbolic"() { + expect: + builder(symbolicString("s", "ab")).symbolic + !builder(new StringValue(context, "ab", -1)).symbolic + } + + // ---- branches of the library calls ---- + + private boolean branchHoldsExactly(List branches, List fixed, boolean javaThrows) { + // The call returns normally iff all of its index checks hold. + BooleanFormula all = bmgr.and(branches*.condition()) + return onlyJavasResult(fixed, javaThrows ? all : bmgr.not(all)) + } + + private static boolean throwsIn(Closure c) { + try { + c() + return false + } catch (IndexOutOfBoundsException ignored) { + return true + } + } + + @Unroll + def "the index checks of String.#name hold iff Java does not throw: '#sample' #a #b"() { + given: + def s = symbolicString("s", "fixed") + def x = symbolicInt("x", a) + def y = symbolicInt("y", b) + def args = desc.startsWith("(II") ? [x, y] : [x] + def fixed = [fixString(s, sample), fixInt(x, a), fixInt(y, b)] + + when: + def branches = StringCallBranches.of(s, name, desc, args as Value[]) + + then: + !branches.isEmpty() + branchHoldsExactly(branches, fixed, throwsIn(java.curry(sample, a, b))) + + where: + [sample, a, b, call] << [["", "abc"], [-1, 0, 3, 4], [-1, 2, 4], + [["charAt", "(I)C", { String str, int i, int j -> str.charAt(i) }], + ["substring", "(I)Ljava/lang/String;", { String str, int i, int j -> str.substring(i) }], + ["substring", "(II)Ljava/lang/String;", { String str, int i, int j -> str.substring(i, j) }]]].combinations() + name = call[0] + desc = call[1] + java = call[2] + } + + @Unroll + def "the index checks of StringBuilder.#name hold iff Java does not throw: '#sample' #a #b"() { + given: + def s = symbolicString("s", "fixed") + def x = symbolicInt("x", a) + def y = symbolicInt("y", b) + def fixed = [fixString(s, sample), fixInt(x, a), fixInt(y, b)] + def args = desc.startsWith("(II") ? [x, y] : desc.startsWith("(IC") ? [x, new CharValue(context, 'z' as char)] + : desc.startsWith("(ILjava/lang/String;") ? [x, new StringValue(context, "q", -1)] : [x] + if (desc.startsWith("(IILjava/lang/String;")) args = [x, y, new StringValue(context, "q", -1)] + + when: + def branches = StringCallBranches.of(builder(s), name, desc, args as Value[]) + + then: + !branches.isEmpty() + branchHoldsExactly(branches, fixed, throwsIn(java.curry(new StringBuilder(sample), a, b))) + + where: + [sample, a, b, call] << [["", "abc"], [-1, 0, 3, 4], [-1, 2, 4], + [["charAt", "(I)C", { StringBuilder str, int i, int j -> str.charAt(i) }], + ["setCharAt", "(IC)V", { StringBuilder str, int i, int j -> str.setCharAt(i, 'z' as char) }], + ["deleteCharAt", "(I)Ljava/lang/StringBuilder;", { StringBuilder str, int i, int j -> str.deleteCharAt(i) }], + ["delete", "(II)Ljava/lang/StringBuilder;", { StringBuilder str, int i, int j -> str.delete(i, j) }], + ["replace", "(IILjava/lang/String;)Ljava/lang/StringBuilder;", { StringBuilder str, int i, int j -> str.replace(i, j, "q") }], + ["insert", "(ILjava/lang/String;)Ljava/lang/StringBuilder;", { StringBuilder str, int i, int j -> str.insert(i, "q") }], + ["substring", "(II)Ljava/lang/String;", { StringBuilder str, int i, int j -> str.substring(i, j) }], + ["setLength", "(I)V", { StringBuilder str, int i, int j -> str.setLength(i) }]]].combinations() + name = call[0] + desc = call[1] + java = call[2] + } + + def "a model that uses a concrete length pins it"() { + given: + def s = symbolicString("s", "abc") + + when: + def branches = StringCallBranches.of(s, "toCharArray", "()[C", [] as Value[]) + + then: + branches.size() == 1 + branches[0].holds() + onlyJavasResult([branches[0].condition()], bmgr.not(imgr.equal(smgr.length(s.formula), imgr.makeNumber(3)))) + } +} diff --git a/symbolic-executor/src/test/resources/targets/svcomp-strings/Main.java b/symbolic-executor/src/test/resources/targets/svcomp-strings/Main.java new file mode 100644 index 00000000..c1d56f9a --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/svcomp-strings/Main.java @@ -0,0 +1,17 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +/** + * SV-COMP style target for the agent test of the index checks of String methods: charAt throws + * for a nondet string shorter than 6 chars, and the exception is caught. + */ +public class Main { + public static void main(String[] args) { + String s = Verifier.nondetString(); + try { + char c = s.charAt(5); + assert c != 'x'; + } catch (StringIndexOutOfBoundsException e) { + // too short + } + } +} From ac1a3536e8ab4f28d467ede69b6e88373db121ac Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:11:06 +0000 Subject: [PATCH 5/5] Keep the nested replace, as precision loss; model the constructor's capacity str.replace_all made Z3 give up (incomplete theory seq) or hang on queries the ten nested first-occurrence replaces solved, so replace keeps that encoding and records precision loss: it is exact only up to ten occurrences, and not when the replacement contains the target. StringBuilder.capacity() is the constructor's (16, the given one, or the length + 16) until a change that may grow the builder; then it is taken concretely, as before. Co-Authored-By: Claude Opus 5.5 --- .../value/reference/StringBuilderValue.java | 31 ++++++++++-- .../value/reference/lang/StringValue.java | 47 +++++-------------- .../lang/StringModelExactnessTest.groovy | 42 ++++++++++++++--- 3 files changed, 74 insertions(+), 46 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java index 431c7c1f..d4b502af 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java @@ -35,6 +35,17 @@ public final class StringBuilderValue extends ObjectValue { private final IntegerFormulaManager imgr; private StringValue stringValue; + /** + * The capacity while it is the one the constructor set; null after a change that may grow it + * (the growth policy is not modelled). + */ + private IntValue capacity; + + /** The methods that do not change the capacity. */ + private static final Set KEEP_CAPACITY = Set.of("charAt", "compareTo", "delete", "deleteCharAt", + "getChars", "indexOf", "lastIndexOf", "length", "reverse", "setCharAt", "subSequence", "substring", + "toString", "capacity"); + /** Whether a change SWAT does not model left the chars unknown. */ private boolean unknown = false; @@ -100,7 +111,7 @@ public void resync(String chars) { case "" -> invokeInit(args, desc); case "append" -> invokeAppend(args, desc); case "appendCodePoint" -> invokeAppendCodePoint(args); - case "capacity" -> PlaceHolder.instance; // depends on the growth policy, so taken concretely + case "capacity" -> capacity != null ? capacity : PlaceHolder.instance; case "charAt" -> invokeCharAt(args); case "compareTo" -> invokeCompareTo(args); case "delete" -> invokeDelete(args); @@ -122,6 +133,9 @@ public void resync(String chars) { // e.g. a double appended, which has no model as a String result = PlaceHolder.instance; } + if (!name.equals("") && !KEEP_CAPACITY.contains(name)) { + capacity = null; + } if (result instanceof PlaceHolder && MUTATORS.contains(name)) { unknown = true; } @@ -130,12 +144,21 @@ public void resync(String chars) { private Value invokeInit(Value[] args, Type[] desc) { StringValue chars; - if (args.length == 0 || desc[0].getSort() == Type.INT) { - // new StringBuilder(), new StringBuilder(int capacity) + capacity = null; + if (args.length == 0) { + chars = new StringValue(context, "", -1); + capacity = new IntValue(context, 16); + } else if (desc[0].getSort() == Type.INT) { + // new StringBuilder(int capacity) chars = new StringValue(context, "", -1); + capacity = args[0] instanceof IntValue c ? c : null; } else if (args.length == 1) { - // new StringBuilder(String), new StringBuilder(CharSequence) + // new StringBuilder(String), new StringBuilder(CharSequence): length + 16 chars = StringValue.charsOf(args[0]); + if (chars != null) { + capacity = new IntValue(context, chars.concrete.length() + 16, + imgr.add(smgr.length(chars.formula), imgr.makeNumber(16))); + } } else { chars = null; } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java index 34d48bf2..67c2cc41 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java @@ -20,7 +20,6 @@ import lombok.Getter; import org.objectweb.asm.Type; import org.sosy_lab.java_smt.api.*; -import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; import static java.lang.Thread.currentThread; @@ -36,6 +35,7 @@ public class StringValue extends ObjectValue { */ public static final java.util.Set EXACT_UFS = java.util.Set.of("commonPrefixLength", "trimStart", "trimEnd", "lastIndexOf"); + static final int REPLACE_COUNT = 10; private StringFormulaManager smgr; private IntegerFormulaManager imgr; @@ -1042,48 +1042,23 @@ public StringFormula codePointString(IntValue ch) { } /** - * String.replace: every occurrence of target, left to right, which is str.replace_all for a - * non-empty target. For an empty one Java puts the replacement between any two chars and at both - * ends, where str.replace_all leaves the string as it is: not modelled. + * String.replace: every occurrence of target, left to right. Z3 hardly decides str.replace_all + * (with a concrete target it gave up or hung where this did not), so only the first + * REPLACE_COUNT occurrences are replaced, one by one, which is exact only for strings with as + * many occurrences at most (and str.replace differs from Java for an empty target): precision + * loss. */ private StringValue replaceAll(StringValue target, StringValue replacement) { String newConcrete = this.concrete.replace(target.concrete, replacement.concrete); if (!isSymbolic() && !target.isSymbolic() && !replacement.isSymbolic()) { return new StringValue(context, newConcrete, ObjectValue.ADDRESS_UNKNOWN); } - if (target.isSymbolic() || target.concrete.isEmpty()) { - recordPrecisionLoss(); + recordPrecisionLoss(); + StringFormula newFormula = formula; + for (int i = 0; i < REPLACE_COUNT; i++) { + newFormula = smgr.replace(newFormula, target.formula, replacement.formula); } - return new StringValue(context, newConcrete, replaceAll(formula, target.formula, replacement.formula), - ObjectValue.ADDRESS_UNKNOWN); - } - - /** - * str.replace_all(s, target, replacement). JavaSMT's Z3 backend does not offer it, so the term - * is parsed from SMT-LIB, over placeholder variables that are then substituted. - */ - private StringFormula replaceAll(StringFormula s, StringFormula target, StringFormula replacement) { - FormulaManager fmgr = context.getFormulaManager(); - StringFormula sVar = smgr.makeVariable("swat.replaceAll.s"); - StringFormula tVar = smgr.makeVariable("swat.replaceAll.t"); - StringFormula rVar = smgr.makeVariable("swat.replaceAll.r"); - StringFormula result = smgr.makeVariable("swat.replaceAll.result"); - BooleanFormula definition = fmgr.parse("(declare-fun |swat.replaceAll.s| () String)" - + "(declare-fun |swat.replaceAll.t| () String)(declare-fun |swat.replaceAll.r| () String)" - + "(declare-fun |swat.replaceAll.result| () String)" - + "(assert (= |swat.replaceAll.result| (str.replace_all |swat.replaceAll.s| |swat.replaceAll.t| |swat.replaceAll.r|)))"); - Formula term = fmgr.visit(definition, new DefaultFormulaVisitor() { - @Override - protected Formula visitDefault(Formula f) { - return null; - } - - @Override - public Formula visitFunction(Formula f, java.util.List args, FunctionDeclaration decl) { - return args.get(0).equals(result) ? args.get(1) : args.get(0); - } - }); - return fmgr.substitute((StringFormula) term, java.util.Map.of(sVar, s, tVar, target, rVar, replacement)); + return new StringValue(context, newConcrete, newFormula, ObjectValue.ADDRESS_UNKNOWN); } /** diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy index db356254..94c95b44 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy @@ -238,7 +238,7 @@ class StringModelExactnessTest extends Specification { } @Unroll - def "replace(CharSequence, CharSequence) replaces every occurrence: #sample, #target -> #replacement"() { + def "replace is exact up to ten occurrences, and precision loss: #sample, #target -> #replacement"() { given: def s = symbolicString("s", "fixed") def fixed = [fixString(s, sample)] @@ -248,24 +248,34 @@ class StringModelExactnessTest extends Specification { [new StringValue(context, target, -1), new StringValue(context, replacement, -1)]) then: + precisionLoss() exactString(fixed, r.formula, sample.replace(target, replacement)) - !precisionLoss() where: - [sample, target, replacement] << [["", "aaaaaaaaaaaaaaa", "xaxax"], ["a", "aa", "xa"], ["", "aa"]].combinations() + [sample, target, replacement] << [["", "aaaaaaaaa", "xaxax"], ["a", "aa", "xa"], ["", "b"]].combinations() } - def "replace(char, char) replaces more than ten occurrences"() { + def "replace(char, char) of more than ten occurrences is not exact, and precision loss"() { given: def s = symbolicString("s", "fixed") - def sample = "a" * 25 + "b" + "a" * 3 + def sample = "a" * 25 when: def r = (StringValue) call(s, "replace", [Type.CHAR_TYPE, Type.CHAR_TYPE], [new CharValue(context, 'a' as char), new CharValue(context, 'c' as char)]) then: - exactString([fixString(s, sample)], r.formula, sample.replace('a' as char, 'c' as char)) + precisionLoss() + !exactString([fixString(s, sample)], r.formula, sample.replace('a' as char, 'c' as char)) + } + + def "replace on concrete strings is concrete"() { + when: + def r = (StringValue) call(new StringValue(context, "abab", -1), "replace", [Type.CHAR_TYPE, Type.CHAR_TYPE], + [new CharValue(context, 'a' as char), new CharValue(context, 'c' as char)]) + + then: + r.concrete == "cbcb" !precisionLoss() } @@ -553,6 +563,26 @@ class StringModelExactnessTest extends Specification { ((StringValue) call(sb, "toString", [], [])).concrete == "ba" } + def "the capacity is the constructor's until the builder may grow"() { + given: + def s = symbolicString("s", "abc") + def sb = builder(null) + call(sb, "", [STRING], [s]) + + when: + def capacity = (IntValue) call(sb, "capacity", [], []) + + then: + capacity.concrete == 19 + exactInt([fixString(s, "hello")], capacity, 21) + + when: + call(sb, "append", [STRING], [new StringValue(context, "x", -1)]) + + then: + call(sb, "capacity", [], []) == PlaceHolder.instance + } + def "a builder with symbolic chars is symbolic"() { expect: builder(symbolicString("s", "ab")).symbolic