From fbea4c1cba483302e885b413eac2627efd7de9b4 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Mon, 19 Oct 2026 14:35:43 +0000 Subject: [PATCH 1/4] Model StringBuffer, case mappings, ignore-case comparisons and simple regexes exactly MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - StringBuffer is shadowed by StringBuilderValue (same methods), also when recovered from the heap. - toLowerCase/toUpperCase (default locale, or a known Locale other than tr/az/lt): char by char from tables of the running JVM, surrogate pairs as code points, by the pinned length. Lower case of a string with 'Σ' (final sigma) stays unmodelled, behind a branch. - equalsIgnoreCase, regionMatches(ignoreCase, ...), compareToIgnoreCase: against a concrete string without surrogates as a regex of the case classes; otherwise Java's comparison loop unrolled over the pinned lengths, surrogate pairs included. Replaces the equalsIgnoreCase UF, which assumed ASCII input (an input restriction) and was cut at 50 chars. Boolean.parseBoolean uses the regex. - matches(regex) for simple regexes (literals, positive classes, groups, alternation, greedy/reluctant quantifiers) as SMT regexes; replaceFirst with a literal regex exactly; replaceAll with a literal regex as replace (precision loss). - codePointAt/codePointBefore/codePointCount, repeat, String.join(array), new String(char[], int, int), String.valueOf(StringBuilder/null), StringBuilder.reverse of symbolic chars, with their index checks and pins. - Character.digit with a symbolic radix and Character.forDigit. Co-Authored-By: Claude Opus 5.5 --- .../swat/symbolic/UFs/EqualsIgnoreCaseUF.java | 125 ---- .../its/swat/symbolic/UFs/ToLowerCaseUF.java | 55 -- .../uzl/its/swat/symbolic/UFs/UFHandler.java | 16 - .../invoke/java/lang/BooleanInvocation.java | 42 +- .../invoke/java/lang/CharacterInvocation.java | 53 +- .../invoke/java/lang/StringCallBranches.java | 90 ++- .../invoke/java/lang/StringInvocation.java | 48 ++ .../its/swat/symbolic/value/ValueFactory.java | 17 +- .../value/reference/StringBuilderValue.java | 57 +- .../value/reference/lang/CaseMapping.java | 363 +++++++++++ .../value/reference/lang/JavaRegex.java | 285 +++++++++ .../value/reference/lang/StringValue.java | 275 ++++++-- .../StringCaseRegexModelExactnessTest.groovy | 602 ++++++++++++++++++ 13 files changed, 1725 insertions(+), 303 deletions(-) delete mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/EqualsIgnoreCaseUF.java delete mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/ToLowerCaseUF.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/JavaRegex.java create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/EqualsIgnoreCaseUF.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/EqualsIgnoreCaseUF.java deleted file mode 100644 index a49cb167..00000000 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/EqualsIgnoreCaseUF.java +++ /dev/null @@ -1,125 +0,0 @@ -package de.uzl.its.swat.symbolic.UFs; - -import de.uzl.its.swat.common.exceptions.NoThreadContextException; -import org.sosy_lab.java_smt.api.*; - -import java.util.ArrayList; -import java.util.List; - -public class EqualsIgnoreCaseUF { - private final FunctionDeclaration equalsIgnoreCaseUF; - private final SolverContext ctx; - private final UFManager ufmgr; - private final StringFormulaManager smgr; - private final BooleanFormulaManager bmgr; - private final IntegerFormulaManager imgr; - private final ToLowerCaseUF toLowerUF; - - // Global cap for unrolling; tune as needed. - private static final int MAX_K = 50; - - public EqualsIgnoreCaseUF(SolverContext ctx) throws NoThreadContextException { - this.ctx = ctx; - FormulaManager fmgr = ctx.getFormulaManager(); - this.ufmgr = fmgr.getUFManager(); - this.smgr = fmgr.getStringFormulaManager(); - this.bmgr = fmgr.getBooleanFormulaManager(); - this.imgr = fmgr.getIntegerFormulaManager(); - this.toLowerUF = new ToLowerCaseUF(ctx); - - this.equalsIgnoreCaseUF = ufmgr.declareUF( - "equalsIgnoreCase", - FormulaType.BooleanType, - FormulaType.StringType, - FormulaType.StringType); - } - - public BooleanFormula getUFCall(StringFormula s1, StringFormula s2) { - return ufmgr.callUF(equalsIgnoreCaseUF, s1, s2); - } - - /** - * Create the (always-added) constraints that define equalsIgnoreCase for this call. - * No branching on the concrete result is needed anymore. - * - * @param s1 symbolic term of the receiver - * @param s2 symbolic term of the argument - * @param concrete1 runtime concrete value of s1 (used to choose tighter guards) - * @param concrete2 runtime concrete value of s2 - * @param s1Symbolic whether s1 carries variables (your isSymbolic()) - * @param s2Symbolic whether s2 carries variables - */ - public BooleanFormula createEqualsIgnoreCaseConstraints( - StringFormula s1, StringFormula s2, - String concrete1, String concrete2, - boolean s1Symbolic, boolean s2Symbolic) throws NoThreadContextException { - // UF call and lengths - BooleanFormula uf = getUFCall(s1, s2); - NumeralFormula.IntegerFormula len1 = smgr.length(s1); - NumeralFormula.IntegerFormula len2 = smgr.length(s2); - - // Per-index guarded equalities up to K - final int K; - if (!s1Symbolic && !s2Symbolic) { - // Both concrete → caller can short-circuit; keep small K just in case - K = Math.min(MAX_K, Math.max(concrete1.length(), concrete2.length())); - } else if (!s1Symbolic) { // s1 concrete - K = Math.min(MAX_K, concrete1.length()); - } else if (!s2Symbolic) { // s2 concrete - K = Math.min(MAX_K, concrete2.length()); - } else { - K = MAX_K; - } - - List perIndex = new ArrayList<>(K); - for (int i = 0; i < K; i++) { - NumeralFormula.IntegerFormula iF = imgr.makeNumber(i); - BooleanFormula inBoth = bmgr.and( - imgr.lessThan(iF, len1), - imgr.lessThan(iF, len2)); - StringFormula c1 = smgr.charAt(s1, iF); - StringFormula c2 = smgr.charAt(s2, iF); - NumeralFormula.IntegerFormula code1 = smgr.toCodePoint(c1); // -1 if out-of-range - NumeralFormula.IntegerFormula code2 = smgr.toCodePoint(c2); - NumeralFormula.IntegerFormula low1 = toLowerUF.applyToLower(code1, inBoth); - NumeralFormula.IntegerFormula low2 = toLowerUF.applyToLower(code2, inBoth); - perIndex.add(bmgr.implication(inBoth, imgr.equal(low1, low2))); - } - - BooleanFormula body = bmgr.and( - imgr.equal(len1, len2), - bmgr.and(perIndex)); - - // Algebraic axioms (safe & useful) - BooleanFormula reflexive = getUFCall(s1, s1); // equalsIgnoreCase(s,s) - BooleanFormula symmetric = bmgr.equivalence(uf, getUFCall(s2, s1)); // symmetry - BooleanFormula lenMismatchImpliesFalse = bmgr.implication(bmgr.not(imgr.equal(len1, len2)), bmgr.not(uf)); // different lengths → false - - // Always safe direction: if equal ignoring case, then the first K positions must match - BooleanFormula ufImpliesBody = bmgr.implication(uf, body); - - // Reverse direction guarded by a length regime where unrolling is complete - BooleanFormula reverseGuard; - if (!s1Symbolic && s2Symbolic) { - // s1 is concrete of length L → activate equivalence exactly at L - int L = concrete1.length(); - reverseGuard = bmgr.and( - imgr.equal(len1, imgr.makeNumber(L)), - imgr.equal(len2, imgr.makeNumber(L))); - } else if (s1Symbolic && !s2Symbolic) { - int L = concrete2.length(); - reverseGuard = bmgr.and( - imgr.equal(len1, imgr.makeNumber(L)), - imgr.equal(len2, imgr.makeNumber(L))); - } else { - // both symbolic (or both concrete path kept) → guard by len≤K - reverseGuard = bmgr.and( - imgr.equal(len1, len2), - imgr.lessOrEquals(len1, imgr.makeNumber(K))); - } - BooleanFormula bodyImpliesUf = bmgr.implication(bmgr.and(reverseGuard, body), uf); - - // Bundle all constraints to add to your "UF" trace channel - return bmgr.and(reflexive, symmetric, lenMismatchImpliesFalse, ufImpliesBody, bodyImpliesUf); - } -} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/ToLowerCaseUF.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/ToLowerCaseUF.java deleted file mode 100644 index cb197486..00000000 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/ToLowerCaseUF.java +++ /dev/null @@ -1,55 +0,0 @@ -package de.uzl.its.swat.symbolic.UFs; - -import de.uzl.its.swat.common.exceptions.NoThreadContextException; -import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; -import de.uzl.its.swat.thread.ThreadHandler; -import edu.umd.cs.findbugs.annotations.Nullable; -import org.sosy_lab.java_smt.api.*; - -public class ToLowerCaseUF { - private final FunctionDeclaration toLowerUF; - private final UFManager ufmgr; - private final IntegerFormulaManager imgr; - private final BooleanFormulaManager bmgr; - - public ToLowerCaseUF(SolverContext ctx) throws NoThreadContextException { - SymbolicTraceHandler sth = ThreadHandler.getSymbolicTraceHandler(Thread.currentThread().getId()); - FormulaManager fmgr = ctx.getFormulaManager(); - ufmgr = fmgr.getUFManager(); - imgr = fmgr.getIntegerFormulaManager(); - bmgr = fmgr.getBooleanFormulaManager(); - - toLowerUF = ufmgr.declareUF("toLowerCase", FormulaType.IntegerType, FormulaType.IntegerType); - - // A..Z -> a..z - for (int c = 'A'; c <= 'Z'; c++) { - NumeralFormula.IntegerFormula in = imgr.makeNumber(c); - NumeralFormula.IntegerFormula out = imgr.makeNumber(c + 32); - sth.addConstraint(imgr.equal(ufmgr.callUF(toLowerUF, in), out)); - } - // identity for printable ASCII excluding A..Z - for (int c = 32; c <= 126; c++) { - if (c < 'A' || c > 'Z') { - NumeralFormula.IntegerFormula in = imgr.makeNumber(c); - sth.addConstraint(imgr.equal(ufmgr.callUF(toLowerUF, in), in)); - } - } - // No definition outside printable ASCII (keeps it partial there on purpose) - } - - /** - * Apply toLower with an optional guard that asserts ASCII bounds only when relevant. - */ - public NumeralFormula.IntegerFormula applyToLower( - NumeralFormula.IntegerFormula charCode, - @Nullable BooleanFormula guard) throws NoThreadContextException { - if (guard != null) { - SymbolicTraceHandler sth = ThreadHandler.getSymbolicTraceHandler(Thread.currentThread().getId()); - BooleanFormula inAscii = bmgr.and( - imgr.greaterOrEquals(charCode, imgr.makeNumber(32)), - imgr.lessOrEquals(charCode, imgr.makeNumber(126))); - sth.addConstraint(bmgr.implication(guard, inAscii)); - } - return ufmgr.callUF(toLowerUF, charCode); - } -} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java index 639b2752..d6056b55 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java @@ -5,24 +5,8 @@ import static java.lang.Thread.currentThread; public class UFHandler { - private EqualsIgnoreCaseUF equalsIgnoreCaseUF; - private ToLowerCaseUF toLowerCaseUF; private SinCosUF sinCosUF; - public EqualsIgnoreCaseUF getEqualsIgnoreCaseUF() throws NoThreadContextException { - if (equalsIgnoreCaseUF == null) { - equalsIgnoreCaseUF = new EqualsIgnoreCaseUF(ThreadHandler.getSolverContext(currentThread().getId())); - } - return equalsIgnoreCaseUF; - } - - public ToLowerCaseUF getToLowerCaseUF() throws NoThreadContextException { - if (toLowerCaseUF == null) { - toLowerCaseUF = new ToLowerCaseUF(ThreadHandler.getSolverContext(currentThread().getId())); - } - return toLowerCaseUF; - } - public SinCosUF getSinCosUF() throws NoThreadContextException { if (sinCosUF == null) { sinCosUF = new SinCosUF(ThreadHandler.getSolverContext(currentThread().getId())); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BooleanInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BooleanInvocation.java index 92fc1f08..e38015ec 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BooleanInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BooleanInvocation.java @@ -2,7 +2,7 @@ import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.ValueConversionException; -import de.uzl.its.swat.symbolic.UFs.EqualsIgnoreCaseUF; +import de.uzl.its.swat.symbolic.value.reference.lang.CaseMapping; 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; @@ -229,47 +229,21 @@ private static BooleanValue logicalXor(BooleanValue a, BooleanValue b) { } /** - * Symbolic wrapper for Boolean.parseBoolean(String s). - * Returns true if the string argument equals "true" (case-insensitive). - * Implemented using EqualsIgnoreCaseUF. + * Symbolic wrapper for Boolean.parseBoolean(String s): "true".equalsIgnoreCase(s), i.e. s + * matches "true" char by char ignoring case. * * @param s The string to parse * @return BooleanValue representing the parsed boolean */ private static BooleanValue parseBoolean(StringValue s) { SolverContext ctx = s.context; - StringFormulaManager sfm = ctx.getFormulaManager().getStringFormulaManager(); - - // Fast path: both concrete + boolean result = Boolean.parseBoolean(s.concrete); if (!s.isSymbolic()) { - return new BooleanValue(ctx, Boolean.parseBoolean(s.concrete)); - } - - try { - // Boolean.parseBoolean returns "true".equalsIgnoreCase(s) - StringFormula trueStr = sfm.makeString("true"); - - EqualsIgnoreCaseUF uf = ThreadHandler.getUFHandler(currentThread().getId()).getEqualsIgnoreCaseUF(); - - // The symbolic boolean result - BooleanFormula ufCall = uf.getUFCall(trueStr, s.formula); - - // Create and add constraints that define the UF behavior - BooleanFormula constraints = uf.createEqualsIgnoreCaseConstraints( - trueStr, s.formula, - "true", s.concrete, - false, s.isSymbolic() // "true" is not symbolic, s may be - ); - ThreadHandler.getSymbolicTraceHandler(currentThread().getId()).addConstraint(constraints); - - // Return with concrete result for concolic steering - boolean concreteResult = Boolean.parseBoolean(s.concrete); - return new BooleanValue(ctx, concreteResult, ufCall); - - } catch (Exception e) { - // Fallback to concrete-only if UF setup fails - return new BooleanValue(ctx, Boolean.parseBoolean(s.concrete)); + return new BooleanValue(ctx, result); } + StringFormulaManager smgr = ctx.getFormulaManager().getStringFormulaManager(); + return new BooleanValue(ctx, result, + smgr.in(s.formula, new CaseMapping(ctx.getFormulaManager()).equalIgnoringCase("true"))); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/CharacterInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/CharacterInvocation.java index 7fa8f7bd..25551400 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/CharacterInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/CharacterInvocation.java @@ -36,6 +36,7 @@ public class CharacterInvocation { case "toCodePoint" -> invokeToCodePoint(args); case "valueOf" -> invokeValueOf(args, desc); case "digit" -> invokeDigit(args, desc); + case "forDigit" -> invokeForDigit(args); case "toString" -> args.length == 1 && desc[0].getSort() == Type.CHAR ? args[0].asCharValue().asStringValue() : PlaceHolder.instance; default -> invokeTabulated(name, args, desc); @@ -103,15 +104,55 @@ private static Tabulated predicate(IntUnaryOperator onChar, IntUnaryOperator onI } /** - * Invocation handler for Character.digit(char, int) and Character.digit(int, int). Modelled for - * a concrete radix only, which is the usual case; a symbolic radix is left unmodelled. + * Invocation handler for Character.digit(char, int) and Character.digit(int, int): the value of + * the char in radix 36 (tabulated), if the radix is in [2, 36] and the value below it, else -1. */ private static Value invokeDigit(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { - if (args.length != 2 || args[1].isSymbolic()) return PlaceHolder.instance; - int radix = args[1].asIntValue().concrete; + if (args.length != 2) return PlaceHolder.instance; + IntValue radix = args[1].asIntValue(); boolean onChar = desc[0].getSort() == Type.CHAR; - IntUnaryOperator f = onChar ? c -> Character.digit((char) c, radix) : c -> Character.digit(c, radix); - return tabulated("digit/" + radix + (onChar ? "/C" : "/I"), f, Result.INT, args[0], onChar); + Value base36 = tabulated("digit/36" + (onChar ? "/C" : "/I"), + onChar ? c -> Character.digit((char) c, Character.MAX_RADIX) : c -> Character.digit(c, Character.MAX_RADIX), + Result.INT, args[0], onChar); + if (!(base36 instanceof IntValue value)) return PlaceHolder.instance; + int result = onChar ? Character.digit((char) args[0].asCharValue().concrete, radix.concrete) + : Character.digit(args[0].asIntValue().concrete, radix.concrete); + if (!value.isSymbolic() && !radix.isSymbolic()) return new IntValue(radix.context, result); + BitvectorFormulaManager bvmgr = radix.context.getFormulaManager().getBitvectorFormulaManager(); + BooleanFormulaManager bmgr = radix.context.getFormulaManager().getBooleanFormulaManager(); + BitvectorFormula r = radix.formula; + BitvectorFormula v = value.formula; + BooleanFormula valid = bmgr.and( + bvmgr.greaterOrEquals(r, bvmgr.makeBitvector(32, Character.MIN_RADIX), true), + bvmgr.lessOrEquals(r, bvmgr.makeBitvector(32, Character.MAX_RADIX), true), + bvmgr.greaterOrEquals(v, bvmgr.makeBitvector(32, 0), true), + bvmgr.lessThan(v, r, true)); + return new IntValue(radix.context, result, bmgr.ifThenElse(valid, v, bvmgr.makeBitvector(32, -1))); + } + + /** + * Invocation handler for Character.forDigit(int digit, int radix): '\0' unless digit is in + * [0, radix) and radix in [2, 36]; else '0' + digit below 10 and 'a' + digit - 10 from there. + */ + private static Value invokeForDigit(Value[] args) throws NotImplementedException, ValueConversionException { + if (args.length != 2) return PlaceHolder.instance; + IntValue digit = args[0].asIntValue(); + IntValue radix = args[1].asIntValue(); + char result = Character.forDigit(digit.concrete, radix.concrete); + if (!digit.isSymbolic() && !radix.isSymbolic()) return new CharValue(digit.context, result); + BitvectorFormulaManager bvmgr = digit.context.getFormulaManager().getBitvectorFormulaManager(); + BooleanFormulaManager bmgr = digit.context.getFormulaManager().getBooleanFormulaManager(); + BitvectorFormula d = digit.formula; + BitvectorFormula r = radix.formula; + BooleanFormula valid = bmgr.and( + bvmgr.greaterOrEquals(d, bvmgr.makeBitvector(32, 0), true), + bvmgr.lessThan(d, r, true), + bvmgr.greaterOrEquals(r, bvmgr.makeBitvector(32, Character.MIN_RADIX), true), + bvmgr.lessOrEquals(r, bvmgr.makeBitvector(32, Character.MAX_RADIX), true)); + BitvectorFormula chars = bmgr.ifThenElse(bvmgr.lessThan(d, bvmgr.makeBitvector(32, 10), true), + bvmgr.add(d, bvmgr.makeBitvector(32, '0')), bvmgr.add(d, bvmgr.makeBitvector(32, 'a' - 10))); + BitvectorFormula code = bmgr.ifThenElse(valid, chars, bvmgr.makeBitvector(32, 0)); + return new CharValue(digit.context, result, bvmgr.extract(code, 15, 0)); } /** Applies the tabulated function {@code f}, cached under {@code key}, to the char or code point {@code arg}. */ 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 index 59ce6675..8333c526 100644 --- 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 @@ -1,6 +1,7 @@ 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.BooleanValue; 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; @@ -14,6 +15,7 @@ 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.StringFormula; import org.sosy_lab.java_smt.api.StringFormulaManager; /** @@ -85,7 +87,72 @@ private void ofString(StringValue s, String name, String desc, Value[] arg case "getChars(II[CI)V" -> getChars(s, args); case "toCharArray()[C" -> pin(length(s)); case "([C)V" -> pin(size(args[0])); + case "([CII)V" -> { + // checkBoundsOffCount(offset, count, value.length), then the chars by the concrete + // offset and count + Int offset = num(args[1]); + Int count = num(args[2]); + Int size = size(args[0]); + add(bmgr.and(imgr.greaterOrEquals(offset.f(), zero()), imgr.greaterOrEquals(count.f(), zero()), + imgr.lessOrEquals(offset.f(), imgr.subtract(size.f(), count.f()))), + offset.c() >= 0 && count.c() >= 0 && offset.c() <= size.c() - count.c()); + pin(offset); + pin(count); + pin(size); + } case "lastIndexOf(I)I", "lastIndexOf(II)I" -> pin(num(args[0])); + case "codePointAt(I)I" -> index(s, args[0]); + case "codePointBefore(I)I" -> codePointBefore(s, args[0]); + case "codePointCount(II)I" -> codePointCount(s, args); + case "repeat(I)Ljava/lang/String;" -> { + Int count = num(args[0]); + add(imgr.greaterOrEquals(count.f(), zero()), count.c() >= 0); + if (count.c() >= 0) pin(count); + } + case "equalsIgnoreCase(Ljava/lang/String;)Z" -> { + if (args[0] instanceof StringValue other && (s.isSymbolic() || other.isSymbolic()) + && !StringValue.equalsIgnoreCaseByRegex(s, other)) { + // Strings of different lengths differ, else the comparison by the pinned length + Int len = length(s); + Int otherLen = length(other); + add(imgr.equal(len.f(), otherLen.f()), len.c() == otherLen.c()); + if (len.c() == otherLen.c()) pin(len); + } + } + case "regionMatches(ZILjava/lang/String;II)Z" -> { + // Ignoring case (maybe): the bounds check, then the comparison by the pinned len + BooleanValue ignoreCase = args[0].asBooleanValue(); + if ((ignoreCase.isSymbolic() || ignoreCase.concrete) && args[2] instanceof StringValue other) { + Int toffset = num(args[1]); + Int ooffset = num(args[3]); + Int len = num(args[4]); + add(bmgr.and(imgr.greaterOrEquals(ooffset.f(), zero()), imgr.greaterOrEquals(toffset.f(), zero()), + imgr.lessOrEquals(toffset.f(), imgr.subtract(length(s).f(), len.f())), + imgr.lessOrEquals(ooffset.f(), imgr.subtract(length(other).f(), len.f()))), + StringValue.regionInBounds(s.concrete, (int) toffset.c(), other.concrete, (int) ooffset.c(), (int) len.c())); + if (StringValue.regionInBounds(s.concrete, (int) toffset.c(), other.concrete, (int) ooffset.c(), (int) len.c())) { + pin(len); + } + } + } + case "compareToIgnoreCase(Ljava/lang/String;)I" -> { + if (args[0] instanceof StringValue other) { + pin(length(s)); + pin(length(other)); + } + } + case "toLowerCase()Ljava/lang/String;", "toLowerCase(Ljava/util/Locale;)Ljava/lang/String;" -> { + if (StringValue.caseMappingLocale(args) != null) { + // 'Σ' (final sigma) is not modelled, the rest by the pinned length + StringFormula sigma = smgr.fromCodePoint(imgr.makeNumber('\u03a3')); + boolean noSigma = s.concrete.indexOf('\u03a3') < 0; + add(bmgr.not(smgr.contains(s.formula, sigma)), noSigma); + if (noSigma) pin(length(s)); + } + } + case "toUpperCase()Ljava/lang/String;", "toUpperCase(Ljava/util/Locale;)Ljava/lang/String;" -> { + if (StringValue.caseMappingLocale(args) != null) pin(length(s)); + } default -> { } } } @@ -93,7 +160,10 @@ private void ofString(StringValue s, String name, String desc, Value[] arg 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 "charAt(I)", "setCharAt(IC)", "deleteCharAt(I)", "codePointAt(I)" -> index(s, args[0]); + case "codePointBefore(I)" -> codePointBefore(s, args[0]); + case "codePointCount(II)" -> codePointCount(s, args); + case "reverse()" -> pin(length(s)); 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]); @@ -170,6 +240,24 @@ private void getChars(StringValue s, Value[] args) throws Exception { pin(dstBegin); } + /** codePointBefore(int index): 0 <= index - 1 < length of s */ + private void codePointBefore(StringValue s, Value indexArg) throws Exception { + Int i = num(indexArg); + Int len = length(s); + add(bmgr.and(imgr.greaterOrEquals(i.f(), imgr.makeNumber(1)), imgr.lessOrEquals(i.f(), len.f())), + 1 <= i.c() && i.c() <= len.c()); + } + + /** codePointCount(int begin, int end): 0 <= begin <= end <= length of s, and end - begin pinned */ + private void codePointCount(StringValue s, Value[] args) throws Exception { + Int begin = num(args[0]); + Int end = num(args[1]); + range(s, begin, end); + if (0 <= begin.c() && begin.c() <= end.c() && end.c() <= s.concrete.length()) { + pin(new Int(imgr.subtract(end.f(), begin.f()), end.c() - begin.c(), begin.symbolic() || end.symbolic())); + } + } + /** 0 <= index < length of s */ private void index(StringValue s, Value indexArg) throws Exception { Int i = num(indexArg); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringInvocation.java index 7fcbbbbc..8de9ead1 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringInvocation.java @@ -5,16 +5,23 @@ 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.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.array.ObjectArrayValue; import de.uzl.its.swat.symbolic.value.reference.lang.BoxedValue; import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; import org.objectweb.asm.Type; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; public class StringInvocation { public static Value invokeStaticMethod(String name, Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { return switch (name) { case "valueOf" -> invokeValueOf(args, desc); + case "join" -> invokeJoin(args, desc); default -> PlaceHolder.instance; }; } @@ -51,10 +58,51 @@ public class StringInvocation { */ private static Value invokeValueOfObject(Value obj) throws NotImplementedException, ValueConversionException { if (obj instanceof StringValue str) return str; + if (obj instanceof ObjectValue o && o.isNullValue()) return new StringValue(o.context, "null", -1); + if (obj instanceof StringBuilderValue sb) { + StringValue chars = sb.getContent(); + return chars == null ? PlaceHolder.instance : new StringValue(chars.context, chars.concrete, chars.formula, -1); + } if (obj instanceof BoxedValue boxed) return boxed.invokeMethod("toString", new Type[0], new Value[0]); return PlaceHolder.instance; } + /** + * String.join(CharSequence delimiter, CharSequence... elements) for an array of a concrete + * size: the elements (a null one as "null") with the delimiter between them. join(delimiter, + * Iterable) is not modelled. + */ + private static Value invokeJoin(Value[] args, Type[] desc) throws NotImplementedException { + if (args.length != 2 || !desc[1].getDescriptor().equals("[Ljava/lang/CharSequence;") + || !(args[1] instanceof ObjectArrayValue elements) || elements.getSize().isSymbolic()) { + return PlaceHolder.instance; + } + StringValue delimiter = StringValue.charsOf(args[0]); + if (delimiter == null) return PlaceHolder.instance; + SolverContext ctx = delimiter.context; + StringFormulaManager smgr = ctx.getFormulaManager().getStringFormulaManager(); + StringBuilder concrete = new StringBuilder(); + StringFormula formula = smgr.makeString(""); + for (int i = 0; i < elements.getSize().concrete; i++) { + Value element; + try { + element = elements.getElement(new IntValue(ctx, i)); + } catch (Exception e) { + return PlaceHolder.instance; + } + StringValue chars = element instanceof ObjectValue o && o.isNullValue() + ? new StringValue(ctx, "null", -1) : StringValue.charsOf(element); + if (chars == null) return PlaceHolder.instance; + if (i > 0) { + concrete.append(delimiter.concrete); + formula = smgr.concat(formula, delimiter.formula); + } + concrete.append(chars.concrete); + formula = smgr.concat(formula, chars.formula); + } + return new StringValue(ctx, concrete.toString(), formula, -1); + } + private static Value invokeValueOf(CharArrayValue data, IntValue offset, IntValue count) { return PlaceHolder.instance; } 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 556cd3fb..5d8754ab 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,8 +116,9 @@ 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 StringBuilder || concrete instanceof StringBuffer) { + return new StringBuilderValue(context, Util.formatClassName(concrete.getClass().getName()), + new StringValue(context, concrete.toString(), -1), address); } else if (concrete instanceof Boolean b) { return new BooleanObjectValue(context, new BooleanValue(context, b), address); } else if (concrete instanceof Byte b) { @@ -154,10 +155,15 @@ public static StringValue createStringValue(String concrete, int address) throws Class cls = concrete.getClass(); String className = cls.getName(); int fieldCount = classDepot.getFieldCountWithReflection(className, cls, false); - return new ObjectValue<>( + ObjectValue object = new ObjectValue<>( context, Util.formatClassName(className), createNumericalValue(ValueType.intValue, fieldCount).asIntValue(), address); + if (concrete instanceof Locale) { + // Immutable: the case mappings of String depend on its language. + object.concrete = concrete; + } + return object; } // throw new RuntimeException("ERROR: Unknown type in getObjectValue"); } @@ -196,8 +202,9 @@ public static StringValue createStringValue(String concrete, int address) throws || classInterfacesAndParents.contains(Util.formatClassName(Character.class.getName()))) { ret = new CharacterObjectValue(context, new CharValue(context, '\u0000'), ObjectValue.ADDRESS_UNKNOWN); } else if (className.equals(Util.formatClassName(StringBuilder.class.getName())) - || classInterfacesAndParents.contains(Util.formatClassName(StringBuilder.class.getName()))) { - ret = new StringBuilderValue(context, null, ObjectValue.ADDRESS_UNKNOWN); //Todo what is the correct initialization value here? + || className.equals(Util.formatClassName(StringBuffer.class.getName()))) { + // The chars are set by the constructor, which is the next call. + ret = new StringBuilderValue(context, className, null, ObjectValue.ADDRESS_UNKNOWN); } else if (className.equals(Util.formatClassName(String.class.getName())) || classInterfacesAndParents.contains(Util.formatClassName(String.class.getName()))) { ret = new StringValue(context, "", ObjectValue.ADDRESS_UNKNOWN); // This is not correct but _normally_ the next call should be the function 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 d4b502af..cf97f58f 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 @@ -11,6 +11,7 @@ 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.CaseMapping; import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; import java.util.Set; import org.objectweb.asm.Type; @@ -18,8 +19,10 @@ /** * Shadow of a StringBuilder: - * its chars as a {@link StringValue}, which is replaced (never changed: it may be a String the + * href="https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/lang/StringBuilder.html">StringBuilder + * or a StringBuffer + * (the same methods, synchronized): 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 @@ -42,7 +45,8 @@ public final class StringBuilderValue extends ObjectValue { private IntValue capacity; /** The methods that do not change the capacity. */ - private static final Set KEEP_CAPACITY = Set.of("charAt", "compareTo", "delete", "deleteCharAt", + private static final Set KEEP_CAPACITY = Set.of("charAt", "codePointAt", "codePointBefore", + "codePointCount", "compareTo", "delete", "deleteCharAt", "getChars", "indexOf", "lastIndexOf", "length", "reverse", "setCharAt", "subSequence", "substring", "toString", "capacity"); @@ -53,8 +57,11 @@ public final class StringBuilderValue extends ObjectValue { private static final Set MUTATORS = Set.of("", "append", "appendCodePoint", "delete", "deleteCharAt", "insert", "replace", "reverse", "setCharAt", "setLength"); + private static final String STRING_BUILDER = "java/lang/StringBuilder"; + public StringBuilderValue(SolverContext context) { super(context, ObjectValue.ADDRESS_UNKNOWN); + this.className = STRING_BUILDER; this.smgr = context.getFormulaManager().getStringFormulaManager(); this.imgr = context.getFormulaManager().getIntegerFormulaManager(); @@ -62,7 +69,13 @@ public StringBuilderValue(SolverContext context) { } public StringBuilderValue(SolverContext context, StringValue v, int address) { + this(context, STRING_BUILDER, v, address); + } + + /** @param className java/lang/StringBuilder or java/lang/StringBuffer */ + public StringBuilderValue(SolverContext context, String className, StringValue v, int address) { super(context, address); + this.className = className; this.smgr = context.getFormulaManager().getStringFormulaManager(); this.imgr = context.getFormulaManager().getIntegerFormulaManager(); this.stringValue = v; @@ -118,7 +131,8 @@ public void resync(String chars) { 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 "indexOf", "lastIndexOf", "codePointAt", "codePointBefore", "codePointCount" -> + 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); @@ -343,10 +357,35 @@ private StringValue objectChars(Value obj) throws NotImplementedException, } 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())); + // By the concrete length (pinned, see StringCallBranches): the chars in reverse order, + // where Java then puts each surrogate pair (a low surrogate followed by a high one after + // the reversal) back in order, scanning from the start. + String reversed = new StringBuilder(stringValue.concrete).reverse().toString(); + if (!stringValue.isSymbolic()) { + setChars(reversed, new CaseMapping(context.getFormulaManager()).chars(reversed)); + return this; + } + int n = stringValue.concrete.length(); + if (n > 256) return PlaceHolder.instance; + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + CaseMapping chars = new CaseMapping(context.getFormulaManager()); + NumeralFormula.IntegerFormula[] r = new NumeralFormula.IntegerFormula[n]; + for (int i = 0; i < n; i++) r[i] = chars.codeAt(stringValue.formula, imgr.makeNumber(n - 1 - i)); + // swapped[i]: the pair at i, i + 1 is put back in order + BooleanFormula[] swapped = new BooleanFormula[n]; + for (int i = 0; i < n; i++) { + swapped[i] = i + 1 < n + ? bmgr.and(i > 0 ? bmgr.not(swapped[i - 1]) : bmgr.makeTrue(), chars.isLowSurrogate(r[i]), chars.isHighSurrogate(r[i + 1])) + : bmgr.makeFalse(); + } + StringFormula result = smgr.makeString(""); + for (int i = 0; i < n; i++) { + NumeralFormula.IntegerFormula c = r[i]; + if (i + 1 < n) c = bmgr.ifThenElse(swapped[i], r[i + 1], c); + if (i > 0) c = bmgr.ifThenElse(swapped[i - 1], r[i - 1], c); + result = smgr.concat(result, smgr.fromCodePoint(c)); + } + setChars(reversed, result); return this; } @@ -418,7 +457,7 @@ public String toString() { formulaString.substring(0, Config.instance().getLoggingFormulaLength()) + "..."; } - return "Ljava/lang/StringBuilder @" + return "L" + className + " @" + Integer.toHexString(address) + (unknown ? " (unknown)" : "") + " (" diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java new file mode 100644 index 00000000..d642301d --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java @@ -0,0 +1,363 @@ +package de.uzl.its.swat.symbolic.value.reference.lang; + +import java.util.ArrayList; +import java.util.EnumMap; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; +import java.util.TreeMap; +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.RegexFormula; +import org.sosy_lab.java_smt.api.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +/** + * Java's case mappings, tabulated from the running JVM (java.lang.Character) and encoded as + * formulas over a code (an Int): the code point mappings, the mapping of one char of a String by + * {@code toLowerCase}/{@code toUpperCase} (for a locale other than tr, az and lt), and the key the + * ignore-case comparisons compare by. + */ +public final class CaseMapping { + + public enum Kind { + /** Character.toLowerCase(int) */ + LOWER, + /** Character.toUpperCase(int) */ + UPPER, + /** Character.toLowerCase(Character.toUpperCase(int)): two chars are equal ignoring case iff this is */ + FOLD + } + + /** The codes lo, lo + stride, ..., hi, which all map to code + delta. */ + private record Segment(int lo, int hi, int stride, int delta) {} + + private static final class Tables { + static final Map> SEGMENTS = new EnumMap<>(Kind.class); + + /** + * The chars (no surrogates) that String.toLowerCase/toUpperCase maps to other than the one + * char the code point mapping gives, e.g. 'ß' to "SS". + */ + static final Map> SPECIALS = new EnumMap<>(Kind.class); + + /** The chars by their FOLD key. */ + static final Map> FOLD_CLASSES = new HashMap<>(); + + static { + for (Kind kind : Kind.values()) { + List segments = new ArrayList<>(); + for (int cp = 0; cp <= Character.MAX_CODE_POINT; cp++) { + int delta = map(kind, cp) - cp; + if (delta == 0) continue; + Segment last = segments.isEmpty() ? null : segments.get(segments.size() - 1); + if (last != null && last.delta() == delta + && (cp - last.hi() == last.stride() || (last.lo() == last.hi() && cp - last.hi() <= 2))) { + segments.set(segments.size() - 1, new Segment(last.lo(), cp, cp - last.hi(), delta)); + } else { + segments.add(new Segment(cp, cp, 1, delta)); + } + } + SEGMENTS.put(kind, segments); + } + for (Kind kind : new Kind[] {Kind.LOWER, Kind.UPPER}) { + TreeMap specials = new TreeMap<>(); + for (int c = 0; c <= 0xFFFF; c++) { + if (Character.isSurrogate((char) c)) continue; + String chars = mapString(kind, String.valueOf((char) c)); + if (chars.length() != 1 || chars.charAt(0) != map(kind, c)) specials.put(c, chars); + } + SPECIALS.put(kind, specials); + } + for (int c = 0; c <= 0xFFFF; c++) { + FOLD_CLASSES.computeIfAbsent(map(Kind.FOLD, c), k -> new ArrayList<>()).add(c); + } + } + } + + private final FormulaManager fmgr; + private final BooleanFormulaManager bmgr; + private final IntegerFormulaManager imgr; + private final StringFormulaManager smgr; + + public CaseMapping(FormulaManager fmgr) { + this.fmgr = fmgr; + this.bmgr = fmgr.getBooleanFormulaManager(); + this.imgr = fmgr.getIntegerFormulaManager(); + this.smgr = fmgr.getStringFormulaManager(); + } + + /** The mapping of code point cp, concretely. */ + public static int map(Kind kind, int cp) { + return switch (kind) { + case LOWER -> Character.toLowerCase(cp); + case UPPER -> Character.toUpperCase(cp); + case FOLD -> Character.toLowerCase(Character.toUpperCase(cp)); + }; + } + + /** String.toLowerCase/toUpperCase with a locale whose rules are those of the root locale. */ + static String mapString(Kind kind, String s) { + return kind == Kind.LOWER ? s.toLowerCase(Locale.ROOT) : s.toUpperCase(Locale.ROOT); + } + + /** + * Whether String.toLowerCase/toUpperCase with this locale follows the root locale's rules: + * Java has special rules only for Turkish, Azerbaijani and Lithuanian. + */ + public static boolean rootRules(Locale locale) { + String lang = locale.getLanguage(); + return !lang.equals("tr") && !lang.equals("az") && !lang.equals("lt"); + } + + /** The mapping of code point cp (a formula over the integers). */ + public IntegerFormula apply(Kind kind, IntegerFormula cp) { + List segments = Tables.SEGMENTS.get(kind); + return apply(segments, 0, segments.size(), cp); + } + + /** A balanced decision over the segments [from, to), sorted by their codes. */ + private IntegerFormula apply(List segments, int from, int to, IntegerFormula cp) { + if (from == to) return cp; + if (to - from == 1) { + Segment s = segments.get(from); + BooleanFormula in = bmgr.and(imgr.greaterOrEquals(cp, imgr.makeNumber(s.lo())), + imgr.lessOrEquals(cp, imgr.makeNumber(s.hi()))); + if (s.stride() == 2) { + in = bmgr.and(in, imgr.equal(imgr.modulo(imgr.subtract(cp, imgr.makeNumber(s.lo())), imgr.makeNumber(2)), + imgr.makeNumber(0))); + } + return bmgr.ifThenElse(in, imgr.add(cp, imgr.makeNumber(s.delta())), cp); + } + int mid = (from + to) / 2; + return bmgr.ifThenElse(imgr.lessThan(cp, imgr.makeNumber(segments.get(mid).lo())), + apply(segments, from, mid, cp), apply(segments, mid, to, cp)); + } + + /** + * The chars String.toLowerCase/toUpperCase (kind LOWER or UPPER) maps the char c (not a + * surrogate; for LOWER not 'Σ', whose mapping depends on the chars around it) to. + */ + public StringFormula charString(Kind kind, IntegerFormula c) { + StringFormula result = smgr.fromCodePoint(apply(kind, c)); + for (Map.Entry special : Tables.SPECIALS.get(kind).descendingMap().entrySet()) { + result = bmgr.ifThenElse(imgr.equal(c, imgr.makeNumber(special.getKey())), chars(special.getValue()), result); + } + return result; + } + + /** The chars of a Java string, one SMT char per UTF-16 char (makeString would join surrogate pairs). */ + public StringFormula chars(String s) { + StringFormula f = smgr.makeString(""); + for (char c : s.toCharArray()) { + f = smgr.concat(f, smgr.fromCodePoint(imgr.makeNumber(c))); + } + return f; + } + + /** + * The strings equal to t ignoring case char by char: at each position, the chars with the same + * FOLD key as t's char there. + */ + public RegexFormula equalIgnoringCase(String t) { + RegexFormula regex = smgr.makeRegex(""); + for (char c : t.toCharArray()) { + RegexFormula chars = null; + for (int other : Tables.FOLD_CLASSES.get(map(Kind.FOLD, c))) { + RegexFormula one = smgr.range((char) other, (char) other); + chars = chars == null ? one : smgr.union(chars, one); + } + regex = smgr.concat(regex, chars); + } + return regex; + } + + public BooleanFormula isHighSurrogate(IntegerFormula c) { + return bmgr.and(imgr.greaterOrEquals(c, imgr.makeNumber(Character.MIN_HIGH_SURROGATE)), + imgr.lessOrEquals(c, imgr.makeNumber(Character.MAX_HIGH_SURROGATE))); + } + + public BooleanFormula isLowSurrogate(IntegerFormula c) { + return bmgr.and(imgr.greaterOrEquals(c, imgr.makeNumber(Character.MIN_LOW_SURROGATE)), + imgr.lessOrEquals(c, imgr.makeNumber(Character.MAX_LOW_SURROGATE))); + } + + /** Character.toCodePoint(high, low) */ + public IntegerFormula toCodePoint(IntegerFormula high, IntegerFormula low) { + return imgr.add(imgr.multiply(imgr.subtract(high, imgr.makeNumber(Character.MIN_HIGH_SURROGATE)), imgr.makeNumber(1024)), + imgr.add(imgr.subtract(low, imgr.makeNumber(Character.MIN_LOW_SURROGATE)), + imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT))); + } + + /** Character.highSurrogate(cp) of a supplementary code point */ + public IntegerFormula highSurrogate(IntegerFormula cp) { + return imgr.add(imgr.makeNumber(Character.MIN_HIGH_SURROGATE), + imgr.divide(imgr.subtract(cp, imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT)), imgr.makeNumber(1024))); + } + + /** Character.lowSurrogate(cp) of a supplementary code point */ + public IntegerFormula lowSurrogate(IntegerFormula cp) { + return imgr.add(imgr.makeNumber(Character.MIN_LOW_SURROGATE), + imgr.modulo(imgr.subtract(cp, imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT)), imgr.makeNumber(1024))); + } + + /** The code of the char of s at index i */ + public IntegerFormula codeAt(StringFormula s, IntegerFormula i) { + return smgr.toCodePoint(smgr.charAt(s, i)); + } + + /** + * String.toLowerCase/toUpperCase (kind LOWER or UPPER) of the first n chars of s, for a locale + * with the root locale's rules. For LOWER, s must not contain 'Σ'. A surrogate pair is mapped as + * its code point (whose mapping is again a supplementary code point), a lone surrogate stays. + */ + public StringFormula mapChars(Kind kind, StringFormula s, int n) { + IntegerFormula[] c = new IntegerFormula[n]; + for (int i = 0; i < n; i++) c[i] = codeAt(s, imgr.makeNumber(i)); + StringFormula result = smgr.makeString(""); + for (int i = 0; i < n; i++) { + StringFormula chars = charString(kind, c[i]); + if (i > 0) { + // the low surrogate of a pair: the low surrogate of the pair's mapping + chars = bmgr.ifThenElse(bmgr.and(isLowSurrogate(c[i]), isHighSurrogate(c[i - 1])), + smgr.fromCodePoint(lowSurrogate(apply(kind, toCodePoint(c[i - 1], c[i])))), chars); + } + if (i + 1 < n) { + chars = bmgr.ifThenElse(bmgr.and(isHighSurrogate(c[i]), isLowSurrogate(c[i + 1])), + smgr.fromCodePoint(highSurrogate(apply(kind, toCodePoint(c[i], c[i + 1])))), chars); + } + result = smgr.concat(result, chars); + } + return result; + } + + /** The result of an ignore-case comparison: whether the loop ended without a difference, and the int it returns. */ + public record Comparison(BooleanFormula ended, IntegerFormula value) {} + + /** + * Java's ignore-case comparison of a[aStart, aStart + tlen) with b[bStart, bStart + olen) + * (StringUTF16.compareToCIImpl, which regionMatches and equalsIgnoreCase use too), unrolled + * over the concrete lengths. Equal chars and chars with the same FOLD key match; otherwise the + * code points the two chars belong to are compared, and a high surrogate that starts a pair + * moves past the pair. Since that may move the two indices apart, the loop is unrolled over + * the pairs of indices it may reach. + */ + public Comparison compareIgnoringCase(StringFormula a, IntegerFormula aStart, int tlen, + StringFormula b, IntegerFormula bStart, int olen) { + Side sa = new Side(a, aStart, tlen); + Side sb = new Side(b, bStart, olen); + // reach[k1][k2]: the loop gets to k1, k2 with no difference before + BooleanFormula[][] reach = new BooleanFormula[tlen + 1][olen + 1]; + reach[0][0] = bmgr.makeTrue(); + BooleanFormula ended = bmgr.makeFalse(); + List differs = new ArrayList<>(); + List differences = new ArrayList<>(); + for (int sum = 0; sum <= tlen + olen; sum++) { + for (int k1 = Math.max(0, sum - olen); k1 <= Math.min(tlen, sum); k1++) { + int k2 = sum - k1; + BooleanFormula here = reach[k1][k2]; + if (here == null) continue; + if (k1 == tlen || k2 == olen) { + ended = bmgr.or(ended, here); + continue; + } + BooleanFormula same = imgr.equal(sa.fold(k1), sb.fold(k2)); + step(reach, k1 + 1, k2 + 1, bmgr.and(here, same)); + BooleanFormula mismatch = bmgr.and(here, bmgr.not(same)); + BooleanFormula sameCodePoint = imgr.equal(sa.foldCodePoint(k1), sb.foldCodePoint(k2)); + for (int skip1 = 0; skip1 <= (sa.canSkip(k1) ? 1 : 0); skip1++) { + for (int skip2 = 0; skip2 <= (sb.canSkip(k2) ? 1 : 0); skip2++) { + step(reach, k1 + 1 + skip1, k2 + 1 + skip2, bmgr.and(mismatch, sameCodePoint, + skip1 == 1 ? sa.skip(k1) : bmgr.not(sa.skip(k1)), + skip2 == 1 ? sb.skip(k2) : bmgr.not(sb.skip(k2)))); + } + } + differs.add(bmgr.and(mismatch, bmgr.not(sameCodePoint))); + differences.add(imgr.subtract(sa.foldCodePoint(k1), sb.foldCodePoint(k2))); + } + } + // Exactly one of the differences, or the end, is reached. + IntegerFormula value = imgr.makeNumber(tlen - olen); + for (int i = differs.size() - 1; i >= 0; i--) { + value = bmgr.ifThenElse(differs.get(i), differences.get(i), value); + } + return new Comparison(ended, value); + } + + /** + * The comparison of compareToIgnoreCase for strings of different coders (one Latin-1, i.e. all + * chars below 256, the other not; StringLatin1.compareToCI_UTF16): char by char, by the FOLD keys + * of the chars, without surrogate pairs. + */ + public IntegerFormula compareCharsIgnoringCase(StringFormula a, int tlen, StringFormula b, int olen) { + Side sa = new Side(a, imgr.makeNumber(0), tlen); + Side sb = new Side(b, imgr.makeNumber(0), olen); + IntegerFormula value = imgr.makeNumber(tlen - olen); + for (int k = Math.min(tlen, olen) - 1; k >= 0; k--) { + value = bmgr.ifThenElse(imgr.equal(sa.fold(k), sb.fold(k)), value, imgr.subtract(sa.fold(k), sb.fold(k))); + } + return value; + } + + /** Whether all chars of s are below 256: a String with a Latin-1 coder. */ + public BooleanFormula isLatin1(StringFormula s) { + return smgr.in(s, smgr.closure(smgr.range('\u0000', 'ÿ'))); + } + + private void step(BooleanFormula[][] reach, int k1, int k2, BooleanFormula condition) { + reach[k1][k2] = reach[k1][k2] == null ? condition : bmgr.or(reach[k1][k2], condition); + } + + /** One of the regions of a comparison, with the terms of its chars made once. */ + private final class Side { + final IntegerFormula[] code; + final IntegerFormula[] fold; + final IntegerFormula[] foldCodePoint; + final BooleanFormula[] skip; + final int length; + + Side(StringFormula s, IntegerFormula start, int length) { + this.length = length; + code = new IntegerFormula[length]; + fold = new IntegerFormula[length]; + foldCodePoint = new IntegerFormula[length]; + skip = new BooleanFormula[length]; + for (int k = 0; k < length; k++) code[k] = codeAt(s, imgr.add(start, imgr.makeNumber(k))); + } + + IntegerFormula fold(int k) { + if (fold[k] == null) fold[k] = apply(Kind.FOLD, code[k]); + return fold[k]; + } + + /** As StringUTF16.codePointIncluding: a low surrogate after a high one, or a high one before a low one. */ + private BooleanFormula lowWithHigh(int k) { + return k > 0 ? bmgr.and(isLowSurrogate(code[k]), isHighSurrogate(code[k - 1])) : bmgr.makeFalse(); + } + + boolean canSkip(int k) { + return k + 1 < length; + } + + BooleanFormula skip(int k) { + if (skip[k] == null) { + skip[k] = canSkip(k) ? bmgr.and(isHighSurrogate(code[k]), isLowSurrogate(code[k + 1])) : bmgr.makeFalse(); + } + return skip[k]; + } + + IntegerFormula foldCodePoint(int k) { + if (foldCodePoint[k] == null) { + IntegerFormula cp = code[k]; + if (canSkip(k)) cp = bmgr.ifThenElse(skip(k), toCodePoint(code[k], code[k + 1]), cp); + if (k > 0) cp = bmgr.ifThenElse(lowWithHigh(k), toCodePoint(code[k - 1], code[k]), cp); + foldCodePoint[k] = apply(Kind.FOLD, cp); + } + return foldCodePoint[k]; + } + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/JavaRegex.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/JavaRegex.java new file mode 100644 index 00000000..4cc15486 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/JavaRegex.java @@ -0,0 +1,285 @@ +package de.uzl.its.swat.symbolic.value.reference.lang; + +import java.util.ArrayList; +import java.util.List; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +/** + * Translates the simple Java regular expressions (java.util.regex.Pattern, no flags) whose + * language an SMT regular expression describes exactly: literal chars, the escaped + * metacharacters, positive character classes ([a-z0-9_], \d, \s, \w), groups, alternation and the + * greedy and reluctant quantifiers. Their atoms match only chars outside the surrogates, so a + * surrogate (alone or in a pair, which Java matches as one code point) matches none of them, char + * by char as in Java. + * + *

Everything else (".", negated classes, anchors, back references, lookaround, possessive + * quantifiers, inline flags, ...) is not translated: {@link #toRegex} then returns null. + */ +public final class JavaRegex { + private static final String METACHARS = ".$^|?*+()[]{}\\"; + + private final StringFormulaManager smgr; + private final String pattern; + private int pos = 0; + + private JavaRegex(StringFormulaManager smgr, String pattern) { + this.smgr = smgr; + this.pattern = pattern; + } + + /** The SMT regular expression for the Java one, or null if it is not one of the simple ones. */ + public static RegexFormula toRegex(StringFormulaManager smgr, String pattern) { + JavaRegex parser = new JavaRegex(smgr, pattern); + try { + RegexFormula regex = parser.alternation(); + return parser.pos == pattern.length() ? regex : null; + } catch (Unsupported e) { + return null; + } + } + + /** + * The literal a regular expression stands for if it has no construct but literal chars and + * escaped metacharacters (e.g. "\\*"), else null. + */ + public static String literal(String pattern) { + StringBuilder chars = new StringBuilder(); + for (int i = 0; i < pattern.length(); i++) { + char c = pattern.charAt(i); + if (c == '\\') { + if (i + 1 == pattern.length()) return null; + char next = pattern.charAt(++i); + if (Character.isLetterOrDigit(next) || Character.isSurrogate(next)) return null; + chars.append(next); + } else if (METACHARS.indexOf(c) >= 0 || Character.isSurrogate(c)) { + return null; + } else { + chars.append(c); + } + } + return chars.toString(); + } + + /** Whether a replacement string of replaceAll/replaceFirst stands for itself (no '$' or '\'). */ + public static boolean literalReplacement(String replacement) { + return replacement.indexOf('$') < 0 && replacement.indexOf('\\') < 0; + } + + private static final class Unsupported extends Exception { + Unsupported() { + super(null, null, false, false); + } + } + + private boolean more() { + return pos < pattern.length(); + } + + private char peek() { + return pattern.charAt(pos); + } + + private RegexFormula alternation() throws Unsupported { + RegexFormula regex = sequence(); + while (more() && peek() == '|') { + pos++; + regex = smgr.union(regex, sequence()); + } + return regex; + } + + private RegexFormula sequence() throws Unsupported { + List parts = new ArrayList<>(); + while (more() && peek() != '|' && peek() != ')') { + parts.add(quantified(atom())); + } + if (parts.isEmpty()) return smgr.makeRegex(""); + return parts.size() == 1 ? parts.get(0) : smgr.concat(parts.toArray(new RegexFormula[0])); + } + + private RegexFormula quantified(RegexFormula atom) throws Unsupported { + RegexFormula regex = atom; + if (!more()) return regex; + char c = peek(); + if (c == '*') { + pos++; + regex = smgr.closure(atom); + } else if (c == '+') { + pos++; + regex = smgr.cross(atom); + } else if (c == '?') { + pos++; + regex = smgr.optional(atom); + } else if (c == '{') { + pos++; + int min = number(); + int max = min; + if (more() && peek() == ',') { + pos++; + max = more() && peek() == '}' ? -1 : number(); + } + expect('}'); + if (max != -1 && max < min) throw new Unsupported(); + regex = repeat(atom, min); + if (max == -1) { + regex = smgr.concat(regex, smgr.closure(atom)); + } else { + for (int i = min; i < max; i++) regex = smgr.concat(regex, smgr.optional(atom)); + } + } else { + return regex; + } + // Reluctant matching does not change which strings match; possessive matching does. + if (more() && peek() == '?') { + pos++; + } else if (more() && peek() == '+') { + throw new Unsupported(); + } + if (more() && (peek() == '*' || peek() == '+' || peek() == '?' || peek() == '{')) throw new Unsupported(); + return regex; + } + + /** atom, n times */ + private RegexFormula repeat(RegexFormula atom, int n) { + RegexFormula regex = smgr.makeRegex(""); + for (int i = 0; i < n; i++) regex = smgr.concat(regex, atom); + return regex; + } + + private int number() throws Unsupported { + int start = pos; + while (more() && Character.isDigit(peek()) && peek() < 128) pos++; + if (pos == start || pos - start > 4) throw new Unsupported(); + return Integer.parseInt(pattern.substring(start, pos)); + } + + private void expect(char c) throws Unsupported { + if (!more() || peek() != c) throw new Unsupported(); + pos++; + } + + private RegexFormula atom() throws Unsupported { + char c = peek(); + switch (c) { + case '(' -> { + pos++; + if (more() && peek() == '?') { + // only the non-capturing group (?:...) + pos++; + expect(':'); + } + RegexFormula inner = alternation(); + expect(')'); + return inner; + } + case '[' -> { + pos++; + return characterClass(); + } + case '\\' -> { + pos++; + return escape(false); + } + default -> { + if (METACHARS.indexOf(c) >= 0 || c == ']' || c == '}') throw new Unsupported(); + pos++; + return single(c); + } + } + } + + private RegexFormula single(char c) throws Unsupported { + if (Character.isSurrogate(c)) throw new Unsupported(); + return smgr.range(c, c); + } + + /** After a backslash: a predefined class, a control char, or an escaped non-alphanumeric char. */ + private RegexFormula escape(boolean inClass) throws Unsupported { + if (!more()) throw new Unsupported(); + char c = pattern.charAt(pos++); + return switch (c) { + case 'd' -> smgr.range('0', '9'); + case 's' -> smgr.union(smgr.range(' ', ' '), smgr.range('\t', '\r')); // [ \t\n\x0B\f\r] + case 'w' -> smgr.union(smgr.union(smgr.range('a', 'z'), smgr.range('A', 'Z')), + smgr.union(smgr.range('0', '9'), smgr.range('_', '_'))); + case 't' -> single('\t'); + case 'n' -> single('\n'); + case 'r' -> single('\r'); + case 'f' -> single('\f'); + default -> { + if (Character.isLetterOrDigit(c) || Character.isSurrogate(c)) throw new Unsupported(); + yield single(c); + } + }; + } + + /** A positive class [...] of chars, ranges and predefined classes. */ + private RegexFormula characterClass() throws Unsupported { + if (more() && peek() == '^') throw new Unsupported(); + RegexFormula regex = null; + boolean first = true; + while (more() && (peek() != ']' || first)) { + char c = peek(); + RegexFormula part; + if (c == '[' || (c == '&' && pos + 1 < pattern.length() && pattern.charAt(pos + 1) == '&')) { + throw new Unsupported(); + } else if (c == '\\') { + pos++; + char next = more() ? peek() : 0; + if (next == 'd' || next == 's' || next == 'w') { + part = escape(true); + if (pos + 1 < pattern.length() && peek() == '-' && pattern.charAt(pos + 1) != ']') throw new Unsupported(); + } else { + part = rangeFrom(escapedChar()); + } + } else { + pos++; + part = rangeFrom(c); + } + regex = regex == null ? part : smgr.union(regex, part); + first = false; + } + expect(']'); + if (regex == null) throw new Unsupported(); + return regex; + } + + /** The char of an escape inside a class (not a predefined class). */ + private char escapedChar() throws Unsupported { + if (!more()) throw new Unsupported(); + char c = pattern.charAt(pos++); + return switch (c) { + case 't' -> '\t'; + case 'n' -> '\n'; + case 'r' -> '\r'; + case 'f' -> '\f'; + default -> { + if (Character.isLetterOrDigit(c) || Character.isSurrogate(c)) throw new Unsupported(); + yield c; + } + }; + } + + /** The char from, or the range from-to if a '-' and an end follow. */ + private RegexFormula rangeFrom(char from) throws Unsupported { + if (pos + 1 < pattern.length() && peek() == '-' && pattern.charAt(pos + 1) != ']') { + pos++; + char to; + if (peek() == '\\') { + pos++; + to = escapedChar(); + } else if (peek() == '[') { + throw new Unsupported(); + } else { + to = pattern.charAt(pos++); + } + if (to < from || Character.isSurrogate(from) || Character.isSurrogate(to) + || (from < Character.MIN_SURROGATE && to > Character.MAX_SURROGATE)) { + throw new Unsupported(); + } + return smgr.range(from, to); + } + return single(from); + } +} 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 67c2cc41..fcfe12e9 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 @@ -5,7 +5,6 @@ import de.uzl.its.swat.common.exceptions.SWATAssert; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.config.Config; -import de.uzl.its.swat.symbolic.UFs.EqualsIgnoreCaseUF; import de.uzl.its.swat.symbolic.value.PlaceHolder; import de.uzl.its.swat.symbolic.value.Value; import de.uzl.its.swat.symbolic.value.VoidValue; @@ -234,7 +233,7 @@ public BooleanFormula getBounds(boolean upper) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeInit(Value[] args, Type[] desc) { + private Value invokeInit(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { // 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; @@ -245,8 +244,19 @@ public BooleanFormula getBounds(boolean upper) { // 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) + // new String(String), new String(StringBuilder), new String(StringBuffer) chars = charsOf(args[0]); + } else if (args.length == 3 && args[0] instanceof CharArrayValue array && desc[1].getSort() == Type.INT) { + // new String(char[] value, int offset, int count), by the concrete offset and count, + // which the call's branches check and pin (StringCallBranches). + int offset = args[1].asIntValue().concrete; + int count = args[2].asIntValue().concrete; + chars = new StringValue(context, "", -1); + for (int i = offset; i < offset + count; i++) { + CharValue c = array.getElement(new IntValue(context, i)); + chars = new StringValue(context, chars.concrete + c.concrete, + smgr.concat(chars.formula, c.asStringValue().formula), -1); + } } else { chars = null; } @@ -304,8 +314,21 @@ public BooleanFormula getBounds(boolean upper) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeCodePointAt(Value[] args, Type[] desc) { - return PlaceHolder.instance; + private Value invokeCodePointAt(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + // The index is in range (the call's branch, StringCallBranches): the char there, or the + // code point of the surrogate pair it starts. + if (args.length != 1) return PlaceHolder.instance; + IntValue index = args[0].asIntValue(); + int result = concrete.codePointAt(index.concrete); + if (!isSymbolic() && !index.isSymbolic()) return new IntValue(context, result); + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + CaseMapping chars = new CaseMapping(context.getFormulaManager()); + NumeralFormula.IntegerFormula i = index.asIntegerFormula(); + NumeralFormula.IntegerFormula next = imgr.add(i, imgr.makeNumber(1)); + NumeralFormula.IntegerFormula c = chars.codeAt(formula, i); + NumeralFormula.IntegerFormula d = chars.codeAt(formula, next); + BooleanFormula pair = bmgr.and(chars.isHighSurrogate(c), imgr.lessThan(next, smgr.length(formula)), chars.isLowSurrogate(d)); + return new IntValue(context, result, bmgr.ifThenElse(pair, chars.toCodePoint(c, d), c)); } /** @@ -319,8 +342,21 @@ public BooleanFormula getBounds(boolean upper) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeCodePointBefore(Value[] args, Type[] desc) { - return PlaceHolder.instance; + private Value invokeCodePointBefore(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + // index - 1 is in range (the call's branch, StringCallBranches): the char before index, + // or the code point of the surrogate pair it ends. + if (args.length != 1) return PlaceHolder.instance; + IntValue index = args[0].asIntValue(); + int result = concrete.codePointBefore(index.concrete); + if (!isSymbolic() && !index.isSymbolic()) return new IntValue(context, result); + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + CaseMapping chars = new CaseMapping(context.getFormulaManager()); + NumeralFormula.IntegerFormula before = imgr.subtract(index.asIntegerFormula(), imgr.makeNumber(1)); + NumeralFormula.IntegerFormula twoBefore = imgr.subtract(index.asIntegerFormula(), imgr.makeNumber(2)); + NumeralFormula.IntegerFormula c = chars.codeAt(formula, before); + NumeralFormula.IntegerFormula b = chars.codeAt(formula, twoBefore); + BooleanFormula pair = bmgr.and(chars.isLowSurrogate(c), imgr.greaterOrEquals(twoBefore, imgr.makeNumber(0)), chars.isHighSurrogate(b)); + return new IntValue(context, result, bmgr.ifThenElse(pair, chars.toCodePoint(b, c), c)); } /** @@ -334,8 +370,29 @@ public BooleanFormula getBounds(boolean upper) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeCodePointCount(Value[] args, Type[] desc) { - return PlaceHolder.instance; + private Value invokeCodePointCount(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + // The range is in bounds and its length pinned (the call's branches, StringCallBranches): + // its chars, less one for each surrogate pair, scanned from the start as Java does. + if (args.length != 2) return PlaceHolder.instance; + IntValue begin = args[0].asIntValue(); + IntValue end = args[1].asIntValue(); + int result = concrete.codePointCount(begin.concrete, end.concrete); + if (!isSymbolic() && !begin.isSymbolic() && !end.isSymbolic()) return new IntValue(context, result); + int n = end.concrete - begin.concrete; + if (n > MAX_UNROLLED_MAPPING) return PlaceHolder.instance; + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + CaseMapping chars = new CaseMapping(context.getFormulaManager()); + NumeralFormula.IntegerFormula[] c = new NumeralFormula.IntegerFormula[n]; + for (int k = 0; k < n; k++) c[k] = chars.codeAt(formula, imgr.add(begin.asIntegerFormula(), imgr.makeNumber(k))); + NumeralFormula.IntegerFormula count = imgr.makeNumber(n); + BooleanFormula pairEndsHere = bmgr.makeFalse(); + for (int k = 0; k + 1 < n; k++) { + // a pair starts at k unless k ends one + BooleanFormula pairStarts = bmgr.and(bmgr.not(pairEndsHere), chars.isHighSurrogate(c[k]), chars.isLowSurrogate(c[k + 1])); + count = bmgr.ifThenElse(pairStarts, imgr.subtract(count, imgr.makeNumber(1)), count); + pairEndsHere = pairStarts; + } + return new IntValue(context, result, count); } /** @@ -429,7 +486,72 @@ private static void addDefinition(BooleanFormula definition) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeCompareToIgnoreCase(Value[] args, Type[] desc) { - return PlaceHolder.instance; + if (args.length != 1 || !(args[0] instanceof StringValue other)) return PlaceHolder.instance; + int result = concrete.compareToIgnoreCase(other.concrete); + if (!isSymbolic() && !other.isSymbolic()) return new IntValue(context, result); + // By the concrete lengths, which the call's branches pin (StringCallBranches). + int tlen = concrete.length(); + int olen = other.concrete.length(); + if (Math.max(tlen, olen) > MAX_UNROLLED_COMPARISON) return PlaceHolder.instance; + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + CaseMapping cases = new CaseMapping(context.getFormulaManager()); + // Strings of the same coder are compared by code points (StringUTF16.compareToCI, the same + // as char by char for two Latin-1 strings), a Latin-1 and a UTF-16 one char by char. + NumeralFormula.IntegerFormula byCodePoints = cases.compareIgnoringCase(formula, imgr.makeNumber(0), tlen, + other.formula, imgr.makeNumber(0), olen).value(); + NumeralFormula.IntegerFormula byChars = cases.compareCharsIgnoringCase(formula, tlen, other.formula, olen); + return new IntValue(context, result, bmgr.ifThenElse( + bmgr.equivalence(cases.isLatin1(formula), cases.isLatin1(other.formula)), byCodePoints, byChars)); + } + + /** The longest string an ignore-case comparison is unrolled over; longer ones are not modelled. */ + static final int MAX_UNROLLED_COMPARISON = 64; + + /** The longest string a case mapping is unrolled over; longer ones are not modelled. */ + static final int MAX_UNROLLED_MAPPING = 256; + + /** + * Whether a.equalsIgnoreCase(b) is modelled as a regular expression: one of them is concrete + * and has no surrogate, so the other must match it char by char (a surrogate of the other + * matches none of its chars, also as part of a pair). Otherwise the model is unrolled over the + * concrete length (pinned). + */ + public static boolean equalsIgnoreCaseByRegex(StringValue a, StringValue b) { + if (a.isSymbolic() == b.isSymbolic()) return false; + String t = a.isSymbolic() ? b.concrete : a.concrete; + return t.chars().noneMatch(c -> Character.isSurrogate((char) c)); + } + + /** The concrete Locale of a Locale argument, or null if it is not known. */ + public static java.util.Locale localeOf(Value v) { + return v instanceof ObjectValue o && o.concrete instanceof java.util.Locale locale ? locale : null; + } + + /** + * The locale of a toLowerCase/toUpperCase call with these arguments, if its case mappings are + * modelled (those of the root locale), else null. + */ + public static java.util.Locale caseMappingLocale(Value[] args) { + java.util.Locale locale = args.length == 0 ? java.util.Locale.getDefault() : localeOf(args[0]); + return locale != null && CaseMapping.rootRules(locale) ? locale : null; + } + + /** + * toLowerCase()/toLowerCase(Locale) (kind LOWER) and toUpperCase()/toUpperCase(Locale) (UPPER), + * unrolled over the concrete length, which the call's branches pin (StringCallBranches). The + * lower case of 'Σ' depends on the word around it (final sigma), which is not modelled: the + * call's branches separate the strings that contain it. + */ + private Value invokeCaseMapping(CaseMapping.Kind kind, Value[] args) { + if (args.length > 1) return PlaceHolder.instance; + java.util.Locale locale = caseMappingLocale(args); + if (locale == null) return PlaceHolder.instance; + String result = kind == CaseMapping.Kind.LOWER ? concrete.toLowerCase(locale) : concrete.toUpperCase(locale); + CaseMapping cases = new CaseMapping(context.getFormulaManager()); + if (!isSymbolic()) return new StringValue(context, result, cases.chars(result), -1); + if (kind == CaseMapping.Kind.LOWER && concrete.indexOf('\u03a3') >= 0) return PlaceHolder.instance; + if (concrete.length() > MAX_UNROLLED_MAPPING) return PlaceHolder.instance; + return new StringValue(context, result, cases.mapChars(kind, formula, concrete.length()), -1); } /** @@ -564,38 +686,26 @@ private static void addDefinition(BooleanFormula definition) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeEqualsIgnoreCase(Value[] args, Type[] desc) throws NotImplementedException { - SWATAssert.enforce(args.length == 1, - "Wrong number of arguments for String.equalsIgnoreCase"); - - try { - StringValue rhs = args[0].asStringValue(); - - // fast path if both concrete - if (!this.isSymbolic() && !rhs.isSymbolic()) { - return new BooleanValue(context, this.concrete.equalsIgnoreCase(rhs.concrete)); - } - - EqualsIgnoreCaseUF uf = ThreadHandler.getUFHandler(currentThread().getId()).getEqualsIgnoreCaseUF(); - - // (1) the symbolic boolean you'll return on the stack - BooleanFormula ufCall = uf.getUFCall(this.formula, rhs.formula); - - // (2) "general" constraints that define the UF (never negated) - BooleanFormula constraints = uf.createEqualsIgnoreCaseConstraints( - this.formula, rhs.formula, - this.concrete, rhs.concrete, - this.isSymbolic(), rhs.isSymbolic()); - ThreadHandler.getSymbolicTraceHandler(currentThread().getId()).addConstraint(constraints); - - // also carry the concrete result for concolic steering - boolean concreteResult = this.concrete.equalsIgnoreCase(rhs.concrete); - return new BooleanValue(context, concreteResult, ufCall); - - } catch (Exception e) { - logger.error("Error invoking equalsIgnoreCase on StringValue: {}", e.getMessage()); - return PlaceHolder.instance; + private Value invokeEqualsIgnoreCase(Value[] args, Type[] desc) { + if (args.length != 1) return PlaceHolder.instance; + if (args[0] instanceof ObjectValue o && o.isNullValue()) return new BooleanValue(context, false); + if (!(args[0] instanceof StringValue other)) return PlaceHolder.instance; + boolean result = concrete.equalsIgnoreCase(other.concrete); + if (!isSymbolic() && !other.isSymbolic()) return new BooleanValue(context, result); + CaseMapping cases = new CaseMapping(context.getFormulaManager()); + if (equalsIgnoreCaseByRegex(this, other)) { + StringValue symbolic = isSymbolic() ? this : other; + String t = isSymbolic() ? other.concrete : concrete; + return new BooleanValue(context, result, smgr.in(symbolic.formula, cases.equalIgnoringCase(t))); } + // The call's branches (StringCallBranches): whether the lengths are equal, then the length + // is pinned. Strings of different lengths are not equal. + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + int n = concrete.length(); + if (n != other.concrete.length()) return new BooleanValue(context, false, bmgr.makeFalse()); + if (n > MAX_UNROLLED_COMPARISON) return PlaceHolder.instance; + return new BooleanValue(context, result, cases.compareIgnoringCase(formula, imgr.makeNumber(0), n, + other.formula, imgr.makeNumber(0), n).ended()); } /** @@ -932,7 +1042,13 @@ public StringFormula codePointString(IntValue ch) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeMatches(Value[] args, Type[] desc) { - return PlaceHolder.instance; + // A concrete regular expression of the simple kind (JavaRegex), else not modelled + if (args.length != 1 || !(args[0] instanceof StringValue regex) || regex.isSymbolic()) return PlaceHolder.instance; + RegexFormula language = JavaRegex.toRegex(smgr, regex.concrete); + if (language == null) return PlaceHolder.instance; + boolean result = concrete.matches(regex.concrete); + if (!isSymbolic()) return new BooleanValue(context, result); + return new BooleanValue(context, result, smgr.in(formula, language)); } /** @@ -963,10 +1079,10 @@ public StringFormula codePointString(IntValue ch) { */ private Value invokeRegionMatches(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { int i = 0; + BooleanValue ignoreCase = null; if (args.length == 5) { - // regionMatches(ignoreCase, ...): only the case-sensitive comparison is modelled. - BooleanValue ignoreCase = args[0].asBooleanValue(); - if (ignoreCase.isSymbolic() || ignoreCase.concrete) return PlaceHolder.instance; + ignoreCase = args[0].asBooleanValue(); + if (!ignoreCase.isSymbolic() && !ignoreCase.concrete) ignoreCase = null; i = 1; } else if (args.length != 4) { return PlaceHolder.instance; @@ -988,7 +1104,29 @@ public StringFormula codePointString(IntValue ch) { imgr.lessOrEquals(o, imgr.subtract(smgr.length(other.formula), l))); BooleanFormula matches = bmgr.or(imgr.lessOrEquals(l, zero), smgr.equal(smgr.substring(formula, t, l), smgr.substring(other.formula, o, l))); - return new BooleanValue(context, result, bmgr.and(inBounds, matches)); + if (ignoreCase == null) return new BooleanValue(context, result, bmgr.and(inBounds, matches)); + // Ignoring case (maybe): the call's branches (StringCallBranches) check the bounds, then + // pin len, over which the comparison is unrolled. + boolean ic = ignoreCase.concrete; + result = concrete.regionMatches(ic, toffset.concrete, other.concrete, ooffset.concrete, len.concrete); + if (!isSymbolic() && !other.isSymbolic() && !ignoreCase.isSymbolic() && !toffset.isSymbolic() + && !ooffset.isSymbolic() && !len.isSymbolic()) { + return new BooleanValue(context, result); + } + if (!regionInBounds(concrete, toffset.concrete, other.concrete, ooffset.concrete, len.concrete)) { + return new BooleanValue(context, false, bmgr.makeFalse()); + } + int n = len.concrete; + if (n > MAX_UNROLLED_COMPARISON) return PlaceHolder.instance; + BooleanFormula ignoringCase = n <= 0 ? bmgr.makeTrue() + : new CaseMapping(context.getFormulaManager()).compareIgnoringCase(formula, t, n, other.formula, o, n).ended(); + return new BooleanValue(context, result, ignoreCase.isSymbolic() + ? bmgr.ifThenElse(ignoreCase.formula, ignoringCase, matches) : ignoringCase); + } + + /** The bounds check of regionMatches: both regions start at 0 or later and end in their string. */ + public static boolean regionInBounds(String s, int toffset, String other, int ooffset, int len) { + return ooffset >= 0 && toffset >= 0 && toffset <= (long) s.length() - len && ooffset <= (long) other.length() - len; } /** @@ -1002,8 +1140,17 @@ public StringFormula codePointString(IntValue ch) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeRepeat(Value[] args, Type[] desc) { - return PlaceHolder.instance; + private Value invokeRepeat(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + // count >= 0 (else it throws) and count pinned (the call's branches, StringCallBranches) + if (args.length != 1) return PlaceHolder.instance; + IntValue count = args[0].asIntValue(); + if (count.concrete < 0 || (long) count.concrete * concrete.length() > Integer.MAX_VALUE) return PlaceHolder.instance; + String result = concrete.repeat(count.concrete); + if (!isSymbolic()) return new StringValue(context, result, new CaseMapping(context.getFormulaManager()).chars(result), -1); + if (count.concrete > MAX_UNROLLED_MAPPING) return PlaceHolder.instance; + StringFormula repeated = smgr.makeString(""); + for (int k = 0; k < count.concrete; k++) repeated = smgr.concat(repeated, formula); + return new StringValue(context, result, repeated, -1); } /** @@ -1073,7 +1220,24 @@ private StringValue replaceAll(StringValue target, StringValue replacement) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeReplaceAll(Value[] args, Type[] desc) { - return PlaceHolder.instance; + // A literal regular expression and replacement: replace(target, replacement). The empty + // regex matches between the chars of a surrogate pair or not, which is left unmodelled. + String target = literalRegexArgument(args); + if (target == null || target.isEmpty()) return PlaceHolder.instance; + return replaceAll(new StringValue(context, target, -1), (StringValue) args[1]); + } + + /** + * The literal the regular expression of replaceAll/replaceFirst(regex, replacement) stands + * for, if both are concrete and literal, else null. + */ + private static String literalRegexArgument(Value[] args) { + if (args.length != 2 || !(args[0] instanceof StringValue regex) || regex.isSymbolic() + || !(args[1] instanceof StringValue replacement) || replacement.isSymbolic() + || !JavaRegex.literalReplacement(replacement.concrete)) { + return null; + } + return JavaRegex.literal(regex.concrete); } /** @@ -1088,7 +1252,14 @@ private StringValue replaceAll(StringValue target, StringValue replacement) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeReplaceFirst(Value[] args, Type[] desc) { - return PlaceHolder.instance; + // A literal regular expression and replacement: the first occurrence is replaced, as by + // str.replace (an empty one is inserted at the start). + String target = literalRegexArgument(args); + if (target == null) return PlaceHolder.instance; + StringValue replacement = (StringValue) args[1]; + String result = concrete.replaceFirst(((StringValue) args[0]).concrete, replacement.concrete); + if (!isSymbolic()) return new StringValue(context, result, -1); + return new StringValue(context, result, smgr.replace(formula, smgr.makeString(target), replacement.formula), -1); } /** @@ -1318,7 +1489,7 @@ private StringValue replaceAll(StringValue target, StringValue replacement) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeToLowerCase(Value[] args, Type[] desc) { - return PlaceHolder.instance; + return invokeCaseMapping(CaseMapping.Kind.LOWER, args); } /** @@ -1348,7 +1519,7 @@ private StringValue replaceAll(StringValue target, StringValue replacement) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeToUpperCase(Value[] args, Type[] desc) { - return PlaceHolder.instance; + return invokeCaseMapping(CaseMapping.Kind.UPPER, args); } /** diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy new file mode 100644 index 00000000..79044095 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy @@ -0,0 +1,602 @@ +package de.uzl.its.value.reference.lang + +import de.uzl.its.swat.symbolic.invoke.java.lang.CharacterInvocation +import de.uzl.its.swat.symbolic.invoke.java.lang.StringCallBranches +import de.uzl.its.swat.symbolic.invoke.java.lang.StringInvocation +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.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.array.ObjectArrayValue +import de.uzl.its.swat.symbolic.value.reference.lang.CaseMapping +import de.uzl.its.swat.symbolic.value.reference.lang.JavaRegex +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 case mappings, ignore-case comparisons, simple regular expressions, code point methods, + * StringBuffer and the other String models added after StringModelExactnessTest are exact. As + * there: a model is applied to symbolic strings and ints whose concrete values are the sample, the + * call's branches (index checks, pins) are taken as they hold for the sample, and with the + * variables fixed to the sample the solver must not find a result other than Java's. + */ +class StringCaseRegexModelExactnessTest extends Specification { + + SolverContext context + FormulaManager fmgr + BooleanFormulaManager bmgr + IntegerFormulaManager imgr + StringFormulaManager smgr + BitvectorFormulaManager bvmgr + + static final Type STRING = Type.getType(String) + static final Type LOCALE = Type.getType(Locale) + static final Type INT = Type.INT_TYPE + static final Type BOOLEAN = Type.BOOLEAN_TYPE + + static final String DESERET_UPPER = "𐐀" // U+10400 + static final String DESERET_LOWER = "𐐨" // U+10428 + + /** Strings with the chars whose case mappings are special: 'ß', 'İ', 'ı', 'ſ', 'µ', 'ÿ', title case 'Dž', 'ʼn', a ligature, Greek, surrogates. */ + static final List CASE_SAMPLES = ["", "a", "Ab", "aB", "ß", "SS", "ss", "İ", "i", "I", "ı", + "ſ", "s", "µ", "Μ", "μ", "ÿ", "Ÿ", "DŽ", + "Dž", "dž", "ʼn", "ff", "σ", "ς", "ΐ", + "x" + DESERET_UPPER, "x" + DESERET_LOWER, "\uD801", "\uDC00\uD801", + "Ⴀ", "ⴀ", "", "", "W1E!+O", "w1e!+o"] + + 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) + fmgr = context.formulaManager + bmgr = fmgr.booleanFormulaManager + imgr = fmgr.integerFormulaManager + smgr = fmgr.stringFormulaManager + bvmgr = fmgr.bitvectorFormulaManager + } + + def cleanup() { + context.close() + ThreadHandler.removeThreadContext(currentThread().id) + } + + // ---- helpers ---- + + protected 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 + } + + /** A symbolic string whose concrete value is the sample (the pinned models use it). */ + protected StringValue symbolicString(String name, String concrete) { + return new StringValue(context, concrete, smgr.makeVariable(name), -1) + } + + protected IntValue symbolicInt(String name, int concrete) { + return new IntValue(context, concrete, bvmgr.makeVariable(32, name)) + } + + protected BooleanFormula fix(StringValue v) { + return smgr.equal(v.formula, chars(v.concrete)) + } + + protected BooleanFormula fix(IntValue v) { + return bvmgr.equal(v.formula, bvmgr.makeBitvector(32, v.concrete)) + } + + /** The call's branches as they hold for the concrete values. */ + protected List branches(Value receiver, String name, String desc, List> args) { + return StringCallBranches.of(receiver, name, desc, args as Value[]).collect { + it.holds() ? it.condition() : bmgr.not(it.condition()) + } + } + + protected boolean precisionLoss() { + return ThreadHandler.getSymbolicTraceHandler(currentThread().id).symbolicTrace.symbolicPrecisionLoss + } + + protected boolean onlyJavasResult(List fixed, BooleanFormula other) { + context.newProverEnvironment().withCloseable { p -> + ThreadHandler.getSymbolicTraceHandler(currentThread().id).getConstraints().each { p.addConstraint(it) } + fixed.each { p.addConstraint(it) } + p.addConstraint(other) + return p.isUnsat() + } + } + + protected boolean satisfiable(List constraints) { + context.newProverEnvironment().withCloseable { p -> + constraints.each { p.addConstraint(it) } + return !p.isUnsat() + } + } + + protected boolean exactInt(List fixed, IntValue result, int java) { + return result.concrete == java && onlyJavasResult(fixed, bmgr.not(imgr.equal(result.asIntegerFormula(), imgr.makeNumber(java)))) + } + + protected boolean exactChar(List fixed, CharValue result, char java) { + return result.concrete == java && onlyJavasResult(fixed, bmgr.not(imgr.equal(result.asIntegerFormula(), imgr.makeNumber((int) java)))) + } + + protected boolean exactBoolean(List fixed, BooleanValue result, boolean java) { + return result.concrete == java && onlyJavasResult(fixed, java ? bmgr.not(result.formula) : result.formula) + } + + protected boolean exactString(List fixed, StringValue result, String java) { + return result.concrete == java && onlyJavasResult(fixed, bmgr.not(smgr.equal(result.formula, chars(java)))) + } + + protected Value call(Value receiver, String name, List desc, List> args) { + return ((ObjectValue) receiver).invokeMethod(name, desc as Type[], args as Value[]) + } + + protected ObjectValue locale(Locale l) { + def v = new ObjectValue(context, "java/util/Locale", new IntValue(context, 0), -1) + v.concrete = l + return v + } + + // ---- case mapping tables ---- + + def "the case mapping tables give Java's mapping for every char and every cased code point"() { + given: + def cases = new CaseMapping(fmgr) + def codes = (0..0xFFFF) + (0x10400..0x104FF) + (0x10C80..0x10CFF) + (0x118A0..0x118DF) + (0x16E40..0x16E7F) + + (0x1E900..0x1E94F) + [0x10FFFF] + + expect: + CaseMapping.Kind.values().every { kind -> + codes.every { int cp -> + def mapped = fmgr.simplify(cases.apply(kind, imgr.makeNumber(cp))) + imgr.equal(mapped, imgr.makeNumber(CaseMapping.map(kind, cp))).with { fmgr.simplify(it) } == bmgr.makeTrue() + } + } + } + + def "a supplementary code point maps to a supplementary one with the same high surrogate"() { + expect: + CaseMapping.Kind.values().every { kind -> + (0x10000..0x10FFFF).every { int cp -> + int m = CaseMapping.map(kind, cp) + m == cp || (m >= 0x10000 && Character.highSurrogate(m) == Character.highSurrogate(cp)) + } + } + } + + def "String.toLowerCase/toUpperCase map char by char, except 'Σ'"() { + // The model maps each char (and each surrogate pair) on its own; Java does too, apart from final sigma. + given: + def random = new Random(1) + def pool = ((0..0xFFFF).findAll { !Character.isSurrogate((char) it) && it != 0x3a3 }.collect { String.valueOf((char) it) } + + [DESERET_UPPER, DESERET_LOWER]) + + expect: + (0..<2000).every { + def parts = (0..[]) + + then: + r instanceof PlaceHolder + b.size() == 1 + !b[0].holds() + onlyJavasResult([fix(s)], b[0].condition()) + } + + def "toLowerCase pins the length"() { + given: + def s = symbolicString("s", "Ab") + + when: + def b = branches(s, "toLowerCase", "()Ljava/lang/String;", []) + + then: + onlyJavasResult(b, bmgr.not(imgr.equal(smgr.length(s.formula), imgr.makeNumber(2)))) + satisfiable(b + [smgr.equal(s.formula, chars("xy"))]) + } + + def "toLowerCase with the Turkish locale or an unknown one is not modelled"() { + given: + def s = symbolicString("s", "I") + def unknown = new ObjectValue(context, "java/util/Locale", new IntValue(context, 0), -1) + + expect: + call(s, "toLowerCase", [LOCALE], [locale(new Locale("tr"))]) instanceof PlaceHolder + call(s, "toUpperCase", [LOCALE], [locale(new Locale("lt"))]) instanceof PlaceHolder + call(s, "toLowerCase", [LOCALE], [unknown]) instanceof PlaceHolder + StringCallBranches.of(s, "toLowerCase", "(Ljava/util/Locale;)Ljava/lang/String;", [locale(new Locale("tr"))] as Value[]).isEmpty() + } + + // ---- equalsIgnoreCase / regionMatches(true, ...) / compareToIgnoreCase ---- + + @Unroll + def "equalsIgnoreCase is exact, a concrete and a symbolic string: '#a' '#b'"() { + given: + def s = symbolicString("s", a) + def t = new StringValue(context, b, -1) + + when: + def r1 = call(s, "equalsIgnoreCase", [STRING], [t]) + def r2 = call(t, "equalsIgnoreCase", [STRING], [s]) + + then: + exactBoolean([fix(s)] + branches(s, "equalsIgnoreCase", "(Ljava/lang/String;)Z", [t]), (BooleanValue) r1, a.equalsIgnoreCase(b)) + exactBoolean([fix(s)] + branches(t, "equalsIgnoreCase", "(Ljava/lang/String;)Z", [s]), (BooleanValue) r2, b.equalsIgnoreCase(a)) + !precisionLoss() + + where: + [a, b] << [CASE_SAMPLES, ["", "a", "SS", "ß", "i", "ı", "µ", "Dž", "x" + DESERET_LOWER, ""]].combinations() + } + + @Unroll + def "equalsIgnoreCase is exact, two symbolic strings: '#a' '#b'"() { + given: + def s = symbolicString("s", a) + def t = symbolicString("t", b) + + when: + def r = call(s, "equalsIgnoreCase", [STRING], [t]) + def fixed = [fix(s), fix(t)] + branches(s, "equalsIgnoreCase", "(Ljava/lang/String;)Z", [t]) + + then: + exactBoolean(fixed, (BooleanValue) r, a.equalsIgnoreCase(b)) + + where: + [a, b] << ([["", "a", "A", "ab", "AB", "ß", "DŽ", "dž", "ı", "I", DESERET_UPPER, DESERET_LOWER, + "\uD801𐐀", "𐐨X", "𐐨\uD801"], ["", "a", "AB", "Dž", "i", + DESERET_LOWER, "𐐨X", "\uD801𐐀"]].combinations() + + [["\uD801𐐀", "𐐨X"], ["x𐐀", "x𐐨"]]) + } + + def "equalsIgnoreCase(null) is false"() { + expect: + !((BooleanValue) call(symbolicString("s", "a"), "equalsIgnoreCase", [STRING], [new ObjectValue(context, 0)])).concrete + } + + @Unroll + def "regionMatches(#ic, ...) is exact: '#a' #to '#b' #oo #len"() { + given: + def s = symbolicString("s", a) + def t = symbolicString("t", b) + def ignoreCase = new BooleanValue(context, ic, bmgr.makeVariable("ic")) + def toffset = symbolicInt("to", to) + def ooffset = symbolicInt("oo", oo) + def length = symbolicInt("len", len) + def args = [ignoreCase, toffset, t, ooffset, length] + + when: + def r = call(s, "regionMatches", [BOOLEAN, INT, STRING, INT, INT], args) + def fixed = [fix(s), fix(t), fix(toffset), fix(ooffset), fix(length), ic ? ignoreCase.formula : bmgr.not(ignoreCase.formula)] + + branches(s, "regionMatches", "(ZILjava/lang/String;II)Z", args) + + then: + exactBoolean(fixed, (BooleanValue) r, a.regionMatches(ic, to, b, oo, len)) + + where: + [a, b, ic, to, oo, len] << [["", "aBc", "x" + DESERET_UPPER], ["ABC", "bc", "X" + DESERET_LOWER], [true, false], + [-1, 0, 1], [0, 1], [-1, 0, 2, 5]].combinations() + } + + @Unroll + def "compareToIgnoreCase is exact: '#a' '#b'"() { + given: + def s = symbolicString("s", a) + def t = symbolicString("t", b) + + when: + def r = call(s, "compareToIgnoreCase", [STRING], [t]) + def fixed = [fix(s), fix(t)] + branches(s, "compareToIgnoreCase", "(Ljava/lang/String;)I", [t]) + + then: + exactInt(fixed, (IntValue) r, a.compareToIgnoreCase(b)) + + where: + [a, b] << [["", "a", "B", "abc", "ß", "ÿ", "Ÿ", "Dž", "x" + DESERET_UPPER, "x\uD801", "Ā"], + ["", "A", "b", "ABD", "Ÿ", "x" + DESERET_LOWER, "x\uDC28", "xa", "ā"]].combinations() + } + + def "Boolean.parseBoolean is exact"() { + given: + def s = symbolicString("s", sample) + + expect: + exactBoolean([fix(s)], (BooleanValue) de.uzl.its.swat.symbolic.invoke.java.lang.BooleanInvocation.invokeStaticMethod( + "parseBoolean", [s] as Value[], [STRING] as Type[]), Boolean.parseBoolean(sample)) + + where: + sample << ["", "true", "TRUE", "tRuE", "true ", "ırue", "tru"] + } + + // ---- regular expressions ---- + + static final List REGEXES = ["[A-Z][a-zA-Z]*", "[a-zA-z]+(['-][a-zA-Z]+)*", "\\d+\\s+([a-zA-Z]+|[a-zA-Z]+\\s[a-zA-Z]+)", + "([a-zA-Z]+|[a-zA-Z]+\\s[a-zA-Z]+)", "\\d{5}", "[1-9]\\d{2}-[1-9]\\d{2}-\\d{4}", "a{2,}b?", + "(?:ab|c)*?", "\\w*\\*", "", "[-a]+", "[a-]", "x{0}", "a{1,3}"] + + @Unroll + def "matches(#regex) is exact: '#sample'"() { + given: + def s = symbolicString("s", sample) + + when: + def r = call(s, "matches", [STRING], [new StringValue(context, regex, -1)]) + + then: + exactBoolean([fix(s)], (BooleanValue) r, sample.matches(regex)) + + where: + [regex, sample] << [REGEXES, ["", "a", "Ab", "O'Neil-Smith", "12 Main St", "12 Main", "Lake City", "12345", "1234", + "234-567-8901", "aab", "aaab", "abcab", "x_1*", "a-", "-", "😀", "a\uD83D"]].combinations() + } + + def "regular expressions outside the simple ones are not translated"() { + expect: + ["a.b", "[^a]", '^a', 'a$', "\\D", "\\bx", "(a)\\1", "a*+", "(?i)a", "(?=a)", "\\p{L}", "[a&&b]", "a{2", "\\Qa\\E", "\\u0041"].every { + JavaRegex.toRegex(smgr, it) == null + } + } + + @Unroll + def "replaceFirst with a literal regex is exact, replaceAll a precision loss: '#sample' #regex"() { + given: + def s = symbolicString("s", sample) + def args = [new StringValue(context, regex, -1), new StringValue(context, "^", -1)] + + when: + def first = call(s, "replaceFirst", [STRING, STRING], args) + def all = call(s, "replaceAll", [STRING, STRING], args) + + then: + exactString([fix(s)], (StringValue) first, sample.replaceFirst(regex, "^")) + exactString([fix(s)], (StringValue) all, sample.replaceAll(regex, "^")) + precisionLoss() + + where: + [sample, regex] << [["", "a*b", "**", "Automatic x Automatic"], ["\\*", "Automatic", "b"]].combinations() + } + + def "replaceAll/replaceFirst with a regex or a replacement that is not literal are not modelled"() { + given: + def s = symbolicString("s", "ab") + + expect: + call(s, "replaceAll", [STRING, STRING], [new StringValue(context, "\\w+", -1), new StringValue(context, "x", -1)]) instanceof PlaceHolder + call(s, "replaceAll", [STRING, STRING], [new StringValue(context, "a", -1), new StringValue(context, "\$1", -1)]) instanceof PlaceHolder + call(s, "replaceAll", [STRING, STRING], [new StringValue(context, "", -1), new StringValue(context, "x", -1)]) instanceof PlaceHolder + } + + // ---- code points, repeat, join, new String(char[], int, int) ---- + + @Unroll + def "codePointAt/codePointBefore/codePointCount are exact: '#sample' #i #j"() { + given: + def s = symbolicString("s", sample) + def x = symbolicInt("x", i) + def y = symbolicInt("y", j) + + when: + Integer at = orNull { sample.codePointAt(i) } + Integer before = orNull { sample.codePointBefore(i) } + Integer count = orNull { sample.codePointCount(i, j) } + + then: + at == null || exactInt([fix(s), fix(x)] + branches(s, "codePointAt", "(I)I", [x]), + (IntValue) call(s, "codePointAt", [INT], [x]), at) + before == null || exactInt([fix(s), fix(x)] + branches(s, "codePointBefore", "(I)I", [x]), + (IntValue) call(s, "codePointBefore", [INT], [x]), before) + count == null || exactInt([fix(s), fix(x), fix(y)] + branches(s, "codePointCount", "(II)I", [x, y]), + (IntValue) call(s, "codePointCount", [INT, INT], [x, y]), count) + + where: + [sample, i, j] << [["", "a", "a😀b", "\uDE00\uD83D", "\uD83D😀"], [-1, 0, 1, 2, 3], [0, 2, 3, 4]].combinations() + } + + /** Java's result, or null if it throws (the index checks are tested elsewhere; the model is not used then). */ + protected static Integer orNull(Closure java) { + try { + return java() + } catch (IndexOutOfBoundsException ignored) { + return null + } + } + + def "the index check of codePointBefore holds iff Java does not throw"() { + given: + def s = symbolicString("s", sample) + def x = symbolicInt("x", i) + def b = StringCallBranches.of(s, "codePointBefore", "(I)I", [x] as Value[]) + boolean javaThrows = false + try { sample.codePointBefore(i) } catch (IndexOutOfBoundsException ignored) { javaThrows = true } + + expect: + b.size() == 1 + b[0].holds() == !javaThrows + onlyJavasResult([fix(s), fix(x)], javaThrows ? b[0].condition() : bmgr.not(b[0].condition())) + + where: + [sample, i] << [["", "ab"], [-1, 0, 1, 2, 3]].combinations() + } + + @Unroll + def "repeat(#n) is exact: '#sample'"() { + given: + def s = symbolicString("s", sample) + def count = symbolicInt("n", n) + + expect: + exactString([fix(s), fix(count)] + branches(s, "repeat", "(I)Ljava/lang/String;", [count]), + (StringValue) call(s, "repeat", [INT], [count]), sample.repeat(n)) + + where: + [sample, n] << [["", "ab"], [0, 1, 3]].combinations() + } + + def "String.join of an array is exact"() { + given: + def s = symbolicString("s", "x") + def array = new ObjectArrayValue(context, "java/lang/CharSequence", new IntValue(context, 3)) + array.storeElement(new IntValue(context, 0), s) + array.storeElement(new IntValue(context, 1), new ObjectValue(context, 0)) + array.storeElement(new IntValue(context, 2), new StringBuilderValue(context, new StringValue(context, "y", -1), -1)) + + when: + def r = StringInvocation.invokeStaticMethod("join", [new StringValue(context, ", ", -1), array] as Value[], + [Type.getType(CharSequence), Type.getType(CharSequence[])] as Type[]) + + then: + exactString([fix(s)], (StringValue) r, String.join(", ", "x", null, "y")) + } + + @Unroll + def "new String(char[], #offset, #count) is exact"() { + given: + def array = new CharArrayValue(context, "hello".toCharArray(), -1) + def o = symbolicInt("o", offset) + def c = symbolicInt("c", count) + def s = new StringValue(context, "", -1) + def args = [array, o, c] + def b = StringCallBranches.of(s, "", "([CII)V", args as Value[]) + boolean javaThrows = false + try { new String("hello".toCharArray(), offset, count) } catch (IndexOutOfBoundsException ignored) { javaThrows = true } + + if (!javaThrows) call(s, "", [Type.getType(char[]), INT, INT], args) + + expect: + b[0].holds() == !javaThrows + onlyJavasResult([fix(o), fix(c)], javaThrows ? b[0].condition() : bmgr.not(b[0].condition())) + javaThrows || exactString([fix(o), fix(c)] + b*.condition(), s, new String("hello".toCharArray(), offset, count)) + + where: + [offset, count] << [[-1, 0, 2, 5], [-1, 0, 3, 6]].combinations() + } + + // ---- StringBuilder.reverse, StringBuffer ---- + + @Unroll + def "reverse of a symbolic builder is exact, surrogate pairs kept in order: '#sample'"() { + given: + def s = symbolicString("s", sample) + def sb = new StringBuilderValue(context, s, -1) + def fixed = [fix(s)] + branches(sb, "reverse", "()Ljava/lang/StringBuilder;", []) + + when: + call(sb, "reverse", [], []) + + then: + exactString(fixed, sb.getContent(), new StringBuilder(sample).reverse().toString()) + + where: + sample << ["", "a", "abc", "a😀b", "\uDE00\uD83D", "😀😁", "\uDE00\uD83D\uD83D"] + } + + def "a StringBuffer is modelled as a StringBuilder"() { + given: + def s = symbolicString("s", "ab") + def sb = new StringBuilderValue(context, "java/lang/StringBuffer", null, -1) + + when: + call(sb, "", [STRING], [s]) + call(sb, "append", [STRING], [new StringValue(context, "!", -1)]) + call(sb, "insert", [INT, STRING], [new IntValue(context, 0), new StringValue(context, "<", -1)]) + def str = call(sb, "toString", [], []) + + then: + sb.className == "java/lang/StringBuffer" + sb.isSymbolic() + exactString([fix(s)], (StringValue) str, "[], [Type.getType(Object)] as Type[]), "[], + [Type.CHAR_TYPE, INT] as Type[], null), Character.digit(c as char, radix)) + + where: + [c, radix] << [['0', '7', 'a', 'Z', 'Ａ', '٣', '-'], [-1, 0, 2, 8, 10, 16, 36, 37]].combinations() + } + + def "Character.digit(c, r) is digit(c, 36) if that is below r, for every char and radix"() { + expect: + (0..0xFFFF).every { int c -> + int d = Character.digit((char) c, 36) + (Character.MIN_RADIX..Character.MAX_RADIX).every { int r -> Character.digit((char) c, r) == (d < r ? d : -1) } + } + } + + @Unroll + def "Character.forDigit is exact: #d #radix"() { + given: + def digit = symbolicInt("d", d) + def r = symbolicInt("r", radix) + + expect: + exactChar([fix(digit), fix(r)], (CharValue) CharacterInvocation.invokeStaticMethod("forDigit", [digit, r] as Value[], + [INT, INT] as Type[], null), Character.forDigit(d, radix)) + + where: + [d, radix] << [[-1, 0, 7, 9, 10, 15, 35, 36], [1, 2, 10, 16, 36, 37]].combinations() + } +} From ef7c0ac1c1399c8ff1850a798a56dfd6f51c3169 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Mon, 19 Oct 2026 15:36:15 +0000 Subject: [PATCH 2/4] Model case mappings and ignore-case comparisons for ASCII strings only Unrolled over a string, the full Unicode case tables (a few hundred ranges per char) give queries Z3 does not decide, even simple ones time out. The models now separate the ASCII strings by a branch and leave the others unmodelled. The ignore-case comparison against a concrete string stays a regex of the case classes, for all chars. Splits (a model's cases, which both return) are told apart from index checks, so a call that took a split's other side still records its branches. Co-Authored-By: Claude Opus 5.5 --- .../symbolic/SymbolicInstructionVisitor.java | 2 +- .../invoke/java/lang/StringCallBranches.java | 60 ++-- .../value/reference/StringBuilderValue.java | 6 +- .../value/reference/lang/CaseMapping.java | 330 ++++-------------- .../value/reference/lang/StringValue.java | 70 ++-- .../symbolic/value/reference/lang/Utf16.java | 53 +++ .../StringCaseRegexModelExactnessTest.groovy | 75 ++-- .../lang/StringModelExactnessTest.groovy | 3 +- 8 files changed, 213 insertions(+), 386 deletions(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/Utf16.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 bbb2ced5..6ebb242e 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 @@ -2320,7 +2320,7 @@ private boolean recordStringCallBranches(long iid, String name, String desc, Obj 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; + if (branches.get(i).check() && !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. 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 index 8333c526..58086329 100644 --- 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 @@ -6,6 +6,7 @@ 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.CaseMapping; import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; import java.util.ArrayList; import java.util.List; @@ -27,6 +28,8 @@ *

  • 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. + *
  • Splits: a model with several cases (e.g. strings of equal and of different lengths) + * records which one the call took. *
  • 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. @@ -36,8 +39,11 @@ */ public final class StringCallBranches { - /** A branch: its condition and whether it held in this run. */ - public record Branch(BooleanFormula condition, boolean holds) {} + /** + * A branch: its condition and whether it held in this run, and whether it is a check the call + * throws at if it fails (else the model only distinguishes the cases, and both sides return). + */ + public record Branch(BooleanFormula condition, boolean holds, boolean check) {} /** An int the checks are about, as a formula over the integers and concretely. */ private record Int(IntegerFormula f, long c, boolean symbolic) {} @@ -111,11 +117,11 @@ private void ofString(StringValue s, String name, String desc, Value[] arg } case "equalsIgnoreCase(Ljava/lang/String;)Z" -> { if (args[0] instanceof StringValue other && (s.isSymbolic() || other.isSymbolic()) - && !StringValue.equalsIgnoreCaseByRegex(s, other)) { + && !StringValue.equalsIgnoreCaseByRegex(s, other) && ascii(s, other)) { // Strings of different lengths differ, else the comparison by the pinned length Int len = length(s); Int otherLen = length(other); - add(imgr.equal(len.f(), otherLen.f()), len.c() == otherLen.c()); + split(imgr.equal(len.f(), otherLen.f()), len.c() == otherLen.c()); if (len.c() == otherLen.c()) pin(len); } } @@ -126,32 +132,23 @@ private void ofString(StringValue s, String name, String desc, Value[] arg Int toffset = num(args[1]); Int ooffset = num(args[3]); Int len = num(args[4]); - add(bmgr.and(imgr.greaterOrEquals(ooffset.f(), zero()), imgr.greaterOrEquals(toffset.f(), zero()), + boolean inBounds = StringValue.regionInBounds(s.concrete, (int) toffset.c(), other.concrete, (int) ooffset.c(), (int) len.c()); + split(bmgr.and(imgr.greaterOrEquals(ooffset.f(), zero()), imgr.greaterOrEquals(toffset.f(), zero()), imgr.lessOrEquals(toffset.f(), imgr.subtract(length(s).f(), len.f())), imgr.lessOrEquals(ooffset.f(), imgr.subtract(length(other).f(), len.f()))), - StringValue.regionInBounds(s.concrete, (int) toffset.c(), other.concrete, (int) ooffset.c(), (int) len.c())); - if (StringValue.regionInBounds(s.concrete, (int) toffset.c(), other.concrete, (int) ooffset.c(), (int) len.c())) { - pin(len); - } + inBounds); + if (inBounds && ascii(s, other)) pin(len); } } case "compareToIgnoreCase(Ljava/lang/String;)I" -> { - if (args[0] instanceof StringValue other) { + if (args[0] instanceof StringValue other && ascii(s, other)) { pin(length(s)); pin(length(other)); } } - case "toLowerCase()Ljava/lang/String;", "toLowerCase(Ljava/util/Locale;)Ljava/lang/String;" -> { - if (StringValue.caseMappingLocale(args) != null) { - // 'Σ' (final sigma) is not modelled, the rest by the pinned length - StringFormula sigma = smgr.fromCodePoint(imgr.makeNumber('\u03a3')); - boolean noSigma = s.concrete.indexOf('\u03a3') < 0; - add(bmgr.not(smgr.contains(s.formula, sigma)), noSigma); - if (noSigma) pin(length(s)); - } - } - case "toUpperCase()Ljava/lang/String;", "toUpperCase(Ljava/util/Locale;)Ljava/lang/String;" -> { - if (StringValue.caseMappingLocale(args) != null) pin(length(s)); + case "toLowerCase()Ljava/lang/String;", "toLowerCase(Ljava/util/Locale;)Ljava/lang/String;", + "toUpperCase()Ljava/lang/String;", "toUpperCase(Ljava/util/Locale;)Ljava/lang/String;" -> { + if (StringValue.caseMappingLocale(args) != null && ascii(s)) pin(length(s)); } default -> { } } @@ -240,6 +237,19 @@ private void getChars(StringValue s, Value[] args) throws Exception { pin(dstBegin); } + /** + * Whether the strings are ASCII, the case the case-insensitive models cover (see CaseMapping): + * a split between ASCII strings and the others. + */ + private boolean ascii(StringValue... strings) { + CaseMapping cases = new CaseMapping(context.getFormulaManager()); + BooleanFormula all = bmgr.makeTrue(); + for (StringValue str : strings) all = bmgr.and(all, cases.isAscii(str.formula)); + boolean holds = StringValue.asciiStrings(strings); + split(all, holds); + return holds; + } + /** codePointBefore(int index): 0 <= index - 1 < length of s */ private void codePointBefore(StringValue s, Value indexArg) throws Exception { Int i = num(indexArg); @@ -303,7 +313,13 @@ private IntegerFormula zero() { return imgr.makeNumber(0); } + /** A check: the call throws if it fails. */ private void add(BooleanFormula condition, boolean holds) { - branches.add(new Branch(condition, holds)); + branches.add(new Branch(condition, holds, true)); + } + + /** A branch between the cases of a model, which both return. */ + private void split(BooleanFormula condition, boolean holds) { + branches.add(new Branch(condition, holds, false)); } } 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 cf97f58f..895714d1 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 @@ -11,7 +11,7 @@ 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.CaseMapping; +import de.uzl.its.swat.symbolic.value.reference.lang.Utf16; import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; import java.util.Set; import org.objectweb.asm.Type; @@ -362,13 +362,13 @@ private StringValue objectChars(Value obj) throws NotImplementedException, // the reversal) back in order, scanning from the start. String reversed = new StringBuilder(stringValue.concrete).reverse().toString(); if (!stringValue.isSymbolic()) { - setChars(reversed, new CaseMapping(context.getFormulaManager()).chars(reversed)); + setChars(reversed, new Utf16(context.getFormulaManager()).chars(reversed)); return this; } int n = stringValue.concrete.length(); if (n > 256) return PlaceHolder.instance; BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); - CaseMapping chars = new CaseMapping(context.getFormulaManager()); + Utf16 chars = new Utf16(context.getFormulaManager()); NumeralFormula.IntegerFormula[] r = new NumeralFormula.IntegerFormula[n]; for (int i = 0; i < n; i++) r[i] = chars.codeAt(stringValue.formula, imgr.makeNumber(n - 1 - i)); // swapped[i]: the pair at i, i + 1 is put back in order diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java index d642301d..ba9b0160 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java @@ -1,12 +1,10 @@ package de.uzl.its.swat.symbolic.value.reference.lang; import java.util.ArrayList; -import java.util.EnumMap; import java.util.HashMap; import java.util.List; import java.util.Locale; import java.util.Map; -import java.util.TreeMap; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; import org.sosy_lab.java_smt.api.FormulaManager; @@ -17,139 +15,58 @@ import org.sosy_lab.java_smt.api.StringFormulaManager; /** - * Java's case mappings, tabulated from the running JVM (java.lang.Character) and encoded as - * formulas over a code (an Int): the code point mappings, the mapping of one char of a String by - * {@code toLowerCase}/{@code toUpperCase} (for a locale other than tr, az and lt), and the key the - * ignore-case comparisons compare by. + * Java's case mappings as formulas: the ignore-case comparison against a concrete string as a + * regular expression of the chars' case classes (tabulated from the running JVM), and the case + * mappings and ignore-case comparisons of ASCII strings char by char. + * + *

    Beyond ASCII the mappings are tables of a few hundred ranges; unrolled over a string, Z3 does + * not decide queries over them (even simple ones time out), so a model separates the ASCII strings + * by a branch and leaves the others unmodelled. */ public final class CaseMapping { public enum Kind { - /** Character.toLowerCase(int) */ + /** Character.toLowerCase / String.toLowerCase */ LOWER, - /** Character.toUpperCase(int) */ - UPPER, - /** Character.toLowerCase(Character.toUpperCase(int)): two chars are equal ignoring case iff this is */ - FOLD + /** Character.toUpperCase / String.toUpperCase */ + UPPER } - /** The codes lo, lo + stride, ..., hi, which all map to code + delta. */ - private record Segment(int lo, int hi, int stride, int delta) {} - - private static final class Tables { - static final Map> SEGMENTS = new EnumMap<>(Kind.class); - - /** - * The chars (no surrogates) that String.toLowerCase/toUpperCase maps to other than the one - * char the code point mapping gives, e.g. 'ß' to "SS". - */ - static final Map> SPECIALS = new EnumMap<>(Kind.class); - - /** The chars by their FOLD key. */ - static final Map> FOLD_CLASSES = new HashMap<>(); + /** The chars by their key Character.toLowerCase(Character.toUpperCase(c)), by which the ignore-case comparisons compare. */ + private static final class FoldClasses { + static final Map> CLASSES = new HashMap<>(); static { - for (Kind kind : Kind.values()) { - List segments = new ArrayList<>(); - for (int cp = 0; cp <= Character.MAX_CODE_POINT; cp++) { - int delta = map(kind, cp) - cp; - if (delta == 0) continue; - Segment last = segments.isEmpty() ? null : segments.get(segments.size() - 1); - if (last != null && last.delta() == delta - && (cp - last.hi() == last.stride() || (last.lo() == last.hi() && cp - last.hi() <= 2))) { - segments.set(segments.size() - 1, new Segment(last.lo(), cp, cp - last.hi(), delta)); - } else { - segments.add(new Segment(cp, cp, 1, delta)); - } - } - SEGMENTS.put(kind, segments); - } - for (Kind kind : new Kind[] {Kind.LOWER, Kind.UPPER}) { - TreeMap specials = new TreeMap<>(); - for (int c = 0; c <= 0xFFFF; c++) { - if (Character.isSurrogate((char) c)) continue; - String chars = mapString(kind, String.valueOf((char) c)); - if (chars.length() != 1 || chars.charAt(0) != map(kind, c)) specials.put(c, chars); - } - SPECIALS.put(kind, specials); - } for (int c = 0; c <= 0xFFFF; c++) { - FOLD_CLASSES.computeIfAbsent(map(Kind.FOLD, c), k -> new ArrayList<>()).add(c); + CLASSES.computeIfAbsent(fold(c), k -> new ArrayList<>()).add(c); } } } - private final FormulaManager fmgr; private final BooleanFormulaManager bmgr; private final IntegerFormulaManager imgr; private final StringFormulaManager smgr; public CaseMapping(FormulaManager fmgr) { - this.fmgr = fmgr; this.bmgr = fmgr.getBooleanFormulaManager(); this.imgr = fmgr.getIntegerFormulaManager(); this.smgr = fmgr.getStringFormulaManager(); } - /** The mapping of code point cp, concretely. */ - public static int map(Kind kind, int cp) { - return switch (kind) { - case LOWER -> Character.toLowerCase(cp); - case UPPER -> Character.toUpperCase(cp); - case FOLD -> Character.toLowerCase(Character.toUpperCase(cp)); - }; - } - - /** String.toLowerCase/toUpperCase with a locale whose rules are those of the root locale. */ - static String mapString(Kind kind, String s) { - return kind == Kind.LOWER ? s.toLowerCase(Locale.ROOT) : s.toUpperCase(Locale.ROOT); + /** The key two chars are compared by when case is ignored. */ + static int fold(int c) { + return Character.toLowerCase(Character.toUpperCase(c)); } /** - * Whether String.toLowerCase/toUpperCase with this locale follows the root locale's rules: - * Java has special rules only for Turkish, Azerbaijani and Lithuanian. + * Whether String.toLowerCase/toUpperCase with this locale maps ASCII letters to ASCII letters: + * Java has special rules only for Turkish, Azerbaijani ('I' to dotless 'ı') and Lithuanian. */ public static boolean rootRules(Locale locale) { String lang = locale.getLanguage(); return !lang.equals("tr") && !lang.equals("az") && !lang.equals("lt"); } - /** The mapping of code point cp (a formula over the integers). */ - public IntegerFormula apply(Kind kind, IntegerFormula cp) { - List segments = Tables.SEGMENTS.get(kind); - return apply(segments, 0, segments.size(), cp); - } - - /** A balanced decision over the segments [from, to), sorted by their codes. */ - private IntegerFormula apply(List segments, int from, int to, IntegerFormula cp) { - if (from == to) return cp; - if (to - from == 1) { - Segment s = segments.get(from); - BooleanFormula in = bmgr.and(imgr.greaterOrEquals(cp, imgr.makeNumber(s.lo())), - imgr.lessOrEquals(cp, imgr.makeNumber(s.hi()))); - if (s.stride() == 2) { - in = bmgr.and(in, imgr.equal(imgr.modulo(imgr.subtract(cp, imgr.makeNumber(s.lo())), imgr.makeNumber(2)), - imgr.makeNumber(0))); - } - return bmgr.ifThenElse(in, imgr.add(cp, imgr.makeNumber(s.delta())), cp); - } - int mid = (from + to) / 2; - return bmgr.ifThenElse(imgr.lessThan(cp, imgr.makeNumber(segments.get(mid).lo())), - apply(segments, from, mid, cp), apply(segments, mid, to, cp)); - } - - /** - * The chars String.toLowerCase/toUpperCase (kind LOWER or UPPER) maps the char c (not a - * surrogate; for LOWER not 'Σ', whose mapping depends on the chars around it) to. - */ - public StringFormula charString(Kind kind, IntegerFormula c) { - StringFormula result = smgr.fromCodePoint(apply(kind, c)); - for (Map.Entry special : Tables.SPECIALS.get(kind).descendingMap().entrySet()) { - result = bmgr.ifThenElse(imgr.equal(c, imgr.makeNumber(special.getKey())), chars(special.getValue()), result); - } - return result; - } - /** The chars of a Java string, one SMT char per UTF-16 char (makeString would join surrogate pairs). */ public StringFormula chars(String s) { StringFormula f = smgr.makeString(""); @@ -160,14 +77,15 @@ public StringFormula chars(String s) { } /** - * The strings equal to t ignoring case char by char: at each position, the chars with the same - * FOLD key as t's char there. + * The strings equal to t ignoring case (t has no surrogates): at each position, the chars with + * the same key as t's char there. A surrogate of the other string matches none of them, also + * as part of a pair (Java compares the pair's code point then, whose key is not one of t's). */ public RegexFormula equalIgnoringCase(String t) { RegexFormula regex = smgr.makeRegex(""); for (char c : t.toCharArray()) { RegexFormula chars = null; - for (int other : Tables.FOLD_CLASSES.get(map(Kind.FOLD, c))) { + for (int other : FoldClasses.CLASSES.get(fold(c))) { RegexFormula one = smgr.range((char) other, (char) other); chars = chars == null ? one : smgr.union(chars, one); } @@ -176,188 +94,62 @@ public RegexFormula equalIgnoringCase(String t) { return regex; } - public BooleanFormula isHighSurrogate(IntegerFormula c) { - return bmgr.and(imgr.greaterOrEquals(c, imgr.makeNumber(Character.MIN_HIGH_SURROGATE)), - imgr.lessOrEquals(c, imgr.makeNumber(Character.MAX_HIGH_SURROGATE))); - } - - public BooleanFormula isLowSurrogate(IntegerFormula c) { - return bmgr.and(imgr.greaterOrEquals(c, imgr.makeNumber(Character.MIN_LOW_SURROGATE)), - imgr.lessOrEquals(c, imgr.makeNumber(Character.MAX_LOW_SURROGATE))); - } - - /** Character.toCodePoint(high, low) */ - public IntegerFormula toCodePoint(IntegerFormula high, IntegerFormula low) { - return imgr.add(imgr.multiply(imgr.subtract(high, imgr.makeNumber(Character.MIN_HIGH_SURROGATE)), imgr.makeNumber(1024)), - imgr.add(imgr.subtract(low, imgr.makeNumber(Character.MIN_LOW_SURROGATE)), - imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT))); + /** Whether all chars of s are ASCII (below 128). */ + public BooleanFormula isAscii(StringFormula s) { + return smgr.in(s, smgr.closure(smgr.range('\u0000', '\u007f'))); } - /** Character.highSurrogate(cp) of a supplementary code point */ - public IntegerFormula highSurrogate(IntegerFormula cp) { - return imgr.add(imgr.makeNumber(Character.MIN_HIGH_SURROGATE), - imgr.divide(imgr.subtract(cp, imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT)), imgr.makeNumber(1024))); + /** The code of the char of s at index i */ + public IntegerFormula codeAt(StringFormula s, IntegerFormula i) { + return smgr.toCodePoint(smgr.charAt(s, i)); } - /** Character.lowSurrogate(cp) of a supplementary code point */ - public IntegerFormula lowSurrogate(IntegerFormula cp) { - return imgr.add(imgr.makeNumber(Character.MIN_LOW_SURROGATE), - imgr.modulo(imgr.subtract(cp, imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT)), imgr.makeNumber(1024))); + private BooleanFormula between(IntegerFormula c, char lo, char hi) { + return bmgr.and(imgr.greaterOrEquals(c, imgr.makeNumber(lo)), imgr.lessOrEquals(c, imgr.makeNumber(hi))); } - /** The code of the char of s at index i */ - public IntegerFormula codeAt(StringFormula s, IntegerFormula i) { - return smgr.toCodePoint(smgr.charAt(s, i)); + /** The key of an ASCII char: the lower case of a letter, else the char itself. */ + public IntegerFormula foldAscii(IntegerFormula c) { + return bmgr.ifThenElse(between(c, 'A', 'Z'), imgr.add(c, imgr.makeNumber('a' - 'A')), c); } - /** - * String.toLowerCase/toUpperCase (kind LOWER or UPPER) of the first n chars of s, for a locale - * with the root locale's rules. For LOWER, s must not contain 'Σ'. A surrogate pair is mapped as - * its code point (whose mapping is again a supplementary code point), a lone surrogate stays. - */ - public StringFormula mapChars(Kind kind, StringFormula s, int n) { - IntegerFormula[] c = new IntegerFormula[n]; - for (int i = 0; i < n; i++) c[i] = codeAt(s, imgr.makeNumber(i)); + /** toLowerCase/toUpperCase of the first n chars of s, all ASCII (for a locale with the root rules). */ + public StringFormula mapAscii(Kind kind, StringFormula s, int n) { StringFormula result = smgr.makeString(""); for (int i = 0; i < n; i++) { - StringFormula chars = charString(kind, c[i]); - if (i > 0) { - // the low surrogate of a pair: the low surrogate of the pair's mapping - chars = bmgr.ifThenElse(bmgr.and(isLowSurrogate(c[i]), isHighSurrogate(c[i - 1])), - smgr.fromCodePoint(lowSurrogate(apply(kind, toCodePoint(c[i - 1], c[i])))), chars); - } - if (i + 1 < n) { - chars = bmgr.ifThenElse(bmgr.and(isHighSurrogate(c[i]), isLowSurrogate(c[i + 1])), - smgr.fromCodePoint(highSurrogate(apply(kind, toCodePoint(c[i], c[i + 1])))), chars); - } - result = smgr.concat(result, chars); + StringFormula ch = smgr.charAt(s, imgr.makeNumber(i)); + IntegerFormula c = smgr.toCodePoint(ch); + StringFormula mapped = kind == Kind.LOWER + ? bmgr.ifThenElse(between(c, 'A', 'Z'), smgr.fromCodePoint(imgr.add(c, imgr.makeNumber('a' - 'A'))), ch) + : bmgr.ifThenElse(between(c, 'a', 'z'), smgr.fromCodePoint(imgr.subtract(c, imgr.makeNumber('a' - 'A'))), ch); + result = smgr.concat(result, mapped); } return result; } - /** The result of an ignore-case comparison: whether the loop ended without a difference, and the int it returns. */ - public record Comparison(BooleanFormula ended, IntegerFormula value) {} + /** The result of an ignore-case comparison: whether no char differed, and the int compareToIgnoreCase returns. */ + public record Comparison(BooleanFormula noDifference, IntegerFormula value) {} /** - * Java's ignore-case comparison of a[aStart, aStart + tlen) with b[bStart, bStart + olen) - * (StringUTF16.compareToCIImpl, which regionMatches and equalsIgnoreCase use too), unrolled - * over the concrete lengths. Equal chars and chars with the same FOLD key match; otherwise the - * code points the two chars belong to are compared, and a high surrogate that starts a pair - * moves past the pair. Since that may move the two indices apart, the loop is unrolled over - * the pairs of indices it may reach. + * Java's ignore-case comparison of a[aStart, aStart + tlen) with b[bStart, bStart + olen), both + * ASCII, char by char over the concrete lengths: the difference of the keys of the first chars + * that differ, else tlen - olen. */ - public Comparison compareIgnoringCase(StringFormula a, IntegerFormula aStart, int tlen, - StringFormula b, IntegerFormula bStart, int olen) { - Side sa = new Side(a, aStart, tlen); - Side sb = new Side(b, bStart, olen); - // reach[k1][k2]: the loop gets to k1, k2 with no difference before - BooleanFormula[][] reach = new BooleanFormula[tlen + 1][olen + 1]; - reach[0][0] = bmgr.makeTrue(); - BooleanFormula ended = bmgr.makeFalse(); - List differs = new ArrayList<>(); - List differences = new ArrayList<>(); - for (int sum = 0; sum <= tlen + olen; sum++) { - for (int k1 = Math.max(0, sum - olen); k1 <= Math.min(tlen, sum); k1++) { - int k2 = sum - k1; - BooleanFormula here = reach[k1][k2]; - if (here == null) continue; - if (k1 == tlen || k2 == olen) { - ended = bmgr.or(ended, here); - continue; - } - BooleanFormula same = imgr.equal(sa.fold(k1), sb.fold(k2)); - step(reach, k1 + 1, k2 + 1, bmgr.and(here, same)); - BooleanFormula mismatch = bmgr.and(here, bmgr.not(same)); - BooleanFormula sameCodePoint = imgr.equal(sa.foldCodePoint(k1), sb.foldCodePoint(k2)); - for (int skip1 = 0; skip1 <= (sa.canSkip(k1) ? 1 : 0); skip1++) { - for (int skip2 = 0; skip2 <= (sb.canSkip(k2) ? 1 : 0); skip2++) { - step(reach, k1 + 1 + skip1, k2 + 1 + skip2, bmgr.and(mismatch, sameCodePoint, - skip1 == 1 ? sa.skip(k1) : bmgr.not(sa.skip(k1)), - skip2 == 1 ? sb.skip(k2) : bmgr.not(sb.skip(k2)))); - } - } - differs.add(bmgr.and(mismatch, bmgr.not(sameCodePoint))); - differences.add(imgr.subtract(sa.foldCodePoint(k1), sb.foldCodePoint(k2))); - } - } - // Exactly one of the differences, or the end, is reached. + public Comparison compareAsciiIgnoringCase(StringFormula a, IntegerFormula aStart, int tlen, + StringFormula b, IntegerFormula bStart, int olen) { + int n = Math.min(tlen, olen); + List equal = new ArrayList<>(); IntegerFormula value = imgr.makeNumber(tlen - olen); - for (int i = differs.size() - 1; i >= 0; i--) { - value = bmgr.ifThenElse(differs.get(i), differences.get(i), value); - } - return new Comparison(ended, value); - } - - /** - * The comparison of compareToIgnoreCase for strings of different coders (one Latin-1, i.e. all - * chars below 256, the other not; StringLatin1.compareToCI_UTF16): char by char, by the FOLD keys - * of the chars, without surrogate pairs. - */ - public IntegerFormula compareCharsIgnoringCase(StringFormula a, int tlen, StringFormula b, int olen) { - Side sa = new Side(a, imgr.makeNumber(0), tlen); - Side sb = new Side(b, imgr.makeNumber(0), olen); - IntegerFormula value = imgr.makeNumber(tlen - olen); - for (int k = Math.min(tlen, olen) - 1; k >= 0; k--) { - value = bmgr.ifThenElse(imgr.equal(sa.fold(k), sb.fold(k)), value, imgr.subtract(sa.fold(k), sb.fold(k))); - } - return value; - } - - /** Whether all chars of s are below 256: a String with a Latin-1 coder. */ - public BooleanFormula isLatin1(StringFormula s) { - return smgr.in(s, smgr.closure(smgr.range('\u0000', 'ÿ'))); - } - - private void step(BooleanFormula[][] reach, int k1, int k2, BooleanFormula condition) { - reach[k1][k2] = reach[k1][k2] == null ? condition : bmgr.or(reach[k1][k2], condition); - } - - /** One of the regions of a comparison, with the terms of its chars made once. */ - private final class Side { - final IntegerFormula[] code; - final IntegerFormula[] fold; - final IntegerFormula[] foldCodePoint; - final BooleanFormula[] skip; - final int length; - - Side(StringFormula s, IntegerFormula start, int length) { - this.length = length; - code = new IntegerFormula[length]; - fold = new IntegerFormula[length]; - foldCodePoint = new IntegerFormula[length]; - skip = new BooleanFormula[length]; - for (int k = 0; k < length; k++) code[k] = codeAt(s, imgr.add(start, imgr.makeNumber(k))); - } - - IntegerFormula fold(int k) { - if (fold[k] == null) fold[k] = apply(Kind.FOLD, code[k]); - return fold[k]; - } - - /** As StringUTF16.codePointIncluding: a low surrogate after a high one, or a high one before a low one. */ - private BooleanFormula lowWithHigh(int k) { - return k > 0 ? bmgr.and(isLowSurrogate(code[k]), isHighSurrogate(code[k - 1])) : bmgr.makeFalse(); - } - - boolean canSkip(int k) { - return k + 1 < length; - } - - BooleanFormula skip(int k) { - if (skip[k] == null) { - skip[k] = canSkip(k) ? bmgr.and(isHighSurrogate(code[k]), isLowSurrogate(code[k + 1])) : bmgr.makeFalse(); - } - return skip[k]; - } - - IntegerFormula foldCodePoint(int k) { - if (foldCodePoint[k] == null) { - IntegerFormula cp = code[k]; - if (canSkip(k)) cp = bmgr.ifThenElse(skip(k), toCodePoint(code[k], code[k + 1]), cp); - if (k > 0) cp = bmgr.ifThenElse(lowWithHigh(k), toCodePoint(code[k - 1], code[k]), cp); - foldCodePoint[k] = apply(Kind.FOLD, cp); - } - return foldCodePoint[k]; + IntegerFormula[] diff = new IntegerFormula[n]; + BooleanFormula[] same = new BooleanFormula[n]; + for (int k = 0; k < n; k++) { + IntegerFormula x = foldAscii(codeAt(a, imgr.add(aStart, imgr.makeNumber(k)))); + IntegerFormula y = foldAscii(codeAt(b, imgr.add(bStart, imgr.makeNumber(k)))); + same[k] = imgr.equal(x, y); + diff[k] = imgr.subtract(x, y); + equal.add(same[k]); } + for (int k = n - 1; k >= 0; k--) value = bmgr.ifThenElse(same[k], value, diff[k]); + return new Comparison(bmgr.and(equal), value); } } 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 fcfe12e9..22f6d891 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 @@ -322,7 +322,7 @@ public BooleanFormula getBounds(boolean upper) { int result = concrete.codePointAt(index.concrete); if (!isSymbolic() && !index.isSymbolic()) return new IntValue(context, result); BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); - CaseMapping chars = new CaseMapping(context.getFormulaManager()); + Utf16 chars = new Utf16(context.getFormulaManager()); NumeralFormula.IntegerFormula i = index.asIntegerFormula(); NumeralFormula.IntegerFormula next = imgr.add(i, imgr.makeNumber(1)); NumeralFormula.IntegerFormula c = chars.codeAt(formula, i); @@ -350,7 +350,7 @@ public BooleanFormula getBounds(boolean upper) { int result = concrete.codePointBefore(index.concrete); if (!isSymbolic() && !index.isSymbolic()) return new IntValue(context, result); BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); - CaseMapping chars = new CaseMapping(context.getFormulaManager()); + Utf16 chars = new Utf16(context.getFormulaManager()); NumeralFormula.IntegerFormula before = imgr.subtract(index.asIntegerFormula(), imgr.makeNumber(1)); NumeralFormula.IntegerFormula twoBefore = imgr.subtract(index.asIntegerFormula(), imgr.makeNumber(2)); NumeralFormula.IntegerFormula c = chars.codeAt(formula, before); @@ -379,9 +379,9 @@ public BooleanFormula getBounds(boolean upper) { int result = concrete.codePointCount(begin.concrete, end.concrete); if (!isSymbolic() && !begin.isSymbolic() && !end.isSymbolic()) return new IntValue(context, result); int n = end.concrete - begin.concrete; - if (n > MAX_UNROLLED_MAPPING) return PlaceHolder.instance; + if (n > MAX_UNROLLED) return PlaceHolder.instance; BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); - CaseMapping chars = new CaseMapping(context.getFormulaManager()); + Utf16 chars = new Utf16(context.getFormulaManager()); NumeralFormula.IntegerFormula[] c = new NumeralFormula.IntegerFormula[n]; for (int k = 0; k < n; k++) c[k] = chars.codeAt(formula, imgr.add(begin.asIntegerFormula(), imgr.makeNumber(k))); NumeralFormula.IntegerFormula count = imgr.makeNumber(n); @@ -489,32 +489,31 @@ private static void addDefinition(BooleanFormula definition) { if (args.length != 1 || !(args[0] instanceof StringValue other)) return PlaceHolder.instance; int result = concrete.compareToIgnoreCase(other.concrete); if (!isSymbolic() && !other.isSymbolic()) return new IntValue(context, result); - // By the concrete lengths, which the call's branches pin (StringCallBranches). + // ASCII strings (the call's branches separate them, StringCallBranches) by the pinned lengths + if (!asciiStrings(this, other)) return PlaceHolder.instance; int tlen = concrete.length(); int olen = other.concrete.length(); - if (Math.max(tlen, olen) > MAX_UNROLLED_COMPARISON) return PlaceHolder.instance; - BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); - CaseMapping cases = new CaseMapping(context.getFormulaManager()); - // Strings of the same coder are compared by code points (StringUTF16.compareToCI, the same - // as char by char for two Latin-1 strings), a Latin-1 and a UTF-16 one char by char. - NumeralFormula.IntegerFormula byCodePoints = cases.compareIgnoringCase(formula, imgr.makeNumber(0), tlen, - other.formula, imgr.makeNumber(0), olen).value(); - NumeralFormula.IntegerFormula byChars = cases.compareCharsIgnoringCase(formula, tlen, other.formula, olen); - return new IntValue(context, result, bmgr.ifThenElse( - bmgr.equivalence(cases.isLatin1(formula), cases.isLatin1(other.formula)), byCodePoints, byChars)); + if (Math.max(tlen, olen) > MAX_UNROLLED) return PlaceHolder.instance; + return new IntValue(context, result, new CaseMapping(context.getFormulaManager()) + .compareAsciiIgnoringCase(formula, imgr.makeNumber(0), tlen, other.formula, imgr.makeNumber(0), olen).value()); } - /** The longest string an ignore-case comparison is unrolled over; longer ones are not modelled. */ - static final int MAX_UNROLLED_COMPARISON = 64; + /** Whether all chars of the strings are ASCII, concretely. */ + public static boolean asciiStrings(StringValue... strings) { + for (StringValue s : strings) { + if (!s.concrete.chars().allMatch(c -> c < 128)) return false; + } + return true; + } - /** The longest string a case mapping is unrolled over; longer ones are not modelled. */ - static final int MAX_UNROLLED_MAPPING = 256; + /** The longest string a model is unrolled over, char by char; longer ones are not modelled. */ + static final int MAX_UNROLLED = 256; /** * Whether a.equalsIgnoreCase(b) is modelled as a regular expression: one of them is concrete * and has no surrogate, so the other must match it char by char (a surrogate of the other * matches none of its chars, also as part of a pair). Otherwise the model is unrolled over the - * concrete length (pinned). + * concrete length (pinned), for ASCII strings. */ public static boolean equalsIgnoreCaseByRegex(StringValue a, StringValue b) { if (a.isSymbolic() == b.isSymbolic()) return false; @@ -537,10 +536,9 @@ public static java.util.Locale caseMappingLocale(Value[] args) { } /** - * toLowerCase()/toLowerCase(Locale) (kind LOWER) and toUpperCase()/toUpperCase(Locale) (UPPER), - * unrolled over the concrete length, which the call's branches pin (StringCallBranches). The - * lower case of 'Σ' depends on the word around it (final sigma), which is not modelled: the - * call's branches separate the strings that contain it. + * toLowerCase()/toLowerCase(Locale) (kind LOWER) and toUpperCase()/toUpperCase(Locale) (UPPER) + * of an ASCII string, which the call's branches separate (StringCallBranches), char by char + * over the pinned length. Other strings are not modelled (see CaseMapping). */ private Value invokeCaseMapping(CaseMapping.Kind kind, Value[] args) { if (args.length > 1) return PlaceHolder.instance; @@ -549,9 +547,8 @@ public static java.util.Locale caseMappingLocale(Value[] args) { String result = kind == CaseMapping.Kind.LOWER ? concrete.toLowerCase(locale) : concrete.toUpperCase(locale); CaseMapping cases = new CaseMapping(context.getFormulaManager()); if (!isSymbolic()) return new StringValue(context, result, cases.chars(result), -1); - if (kind == CaseMapping.Kind.LOWER && concrete.indexOf('\u03a3') >= 0) return PlaceHolder.instance; - if (concrete.length() > MAX_UNROLLED_MAPPING) return PlaceHolder.instance; - return new StringValue(context, result, cases.mapChars(kind, formula, concrete.length()), -1); + if (!asciiStrings(this) || concrete.length() > MAX_UNROLLED) return PlaceHolder.instance; + return new StringValue(context, result, cases.mapAscii(kind, formula, concrete.length()), -1); } /** @@ -698,14 +695,15 @@ public static java.util.Locale caseMappingLocale(Value[] args) { String t = isSymbolic() ? other.concrete : concrete; return new BooleanValue(context, result, smgr.in(symbolic.formula, cases.equalIgnoringCase(t))); } - // The call's branches (StringCallBranches): whether the lengths are equal, then the length - // is pinned. Strings of different lengths are not equal. + // The call's branches (StringCallBranches): whether both are ASCII, whether the lengths are + // equal, then the length is pinned. Strings of different lengths are not equal. BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); int n = concrete.length(); + if (!asciiStrings(this, other)) return PlaceHolder.instance; if (n != other.concrete.length()) return new BooleanValue(context, false, bmgr.makeFalse()); - if (n > MAX_UNROLLED_COMPARISON) return PlaceHolder.instance; - return new BooleanValue(context, result, cases.compareIgnoringCase(formula, imgr.makeNumber(0), n, - other.formula, imgr.makeNumber(0), n).ended()); + if (n > MAX_UNROLLED) return PlaceHolder.instance; + return new BooleanValue(context, result, cases.compareAsciiIgnoringCase(formula, imgr.makeNumber(0), n, + other.formula, imgr.makeNumber(0), n).noDifference()); } /** @@ -1117,9 +1115,9 @@ public StringFormula codePointString(IntValue ch) { return new BooleanValue(context, false, bmgr.makeFalse()); } int n = len.concrete; - if (n > MAX_UNROLLED_COMPARISON) return PlaceHolder.instance; + if (n > MAX_UNROLLED || !asciiStrings(this, other)) return PlaceHolder.instance; BooleanFormula ignoringCase = n <= 0 ? bmgr.makeTrue() - : new CaseMapping(context.getFormulaManager()).compareIgnoringCase(formula, t, n, other.formula, o, n).ended(); + : new CaseMapping(context.getFormulaManager()).compareAsciiIgnoringCase(formula, t, n, other.formula, o, n).noDifference(); return new BooleanValue(context, result, ignoreCase.isSymbolic() ? bmgr.ifThenElse(ignoreCase.formula, ignoringCase, matches) : ignoringCase); } @@ -1146,8 +1144,8 @@ public static boolean regionInBounds(String s, int toffset, String other, int oo IntValue count = args[0].asIntValue(); if (count.concrete < 0 || (long) count.concrete * concrete.length() > Integer.MAX_VALUE) return PlaceHolder.instance; String result = concrete.repeat(count.concrete); - if (!isSymbolic()) return new StringValue(context, result, new CaseMapping(context.getFormulaManager()).chars(result), -1); - if (count.concrete > MAX_UNROLLED_MAPPING) return PlaceHolder.instance; + if (!isSymbolic()) return new StringValue(context, result, new Utf16(context.getFormulaManager()).chars(result), -1); + if (count.concrete > MAX_UNROLLED) return PlaceHolder.instance; StringFormula repeated = smgr.makeString(""); for (int k = 0; k < count.concrete; k++) repeated = smgr.concat(repeated, formula); return new StringValue(context, result, repeated, -1); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/Utf16.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/Utf16.java new file mode 100644 index 00000000..dd5f061e --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/Utf16.java @@ -0,0 +1,53 @@ +package de.uzl.its.swat.symbolic.value.reference.lang; + +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.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +/** The UTF-16 chars of a Java string as formulas: their codes, surrogates and surrogate pairs. */ +public final class Utf16 { + private final BooleanFormulaManager bmgr; + private final IntegerFormulaManager imgr; + private final StringFormulaManager smgr; + + public Utf16(FormulaManager fmgr) { + this.bmgr = fmgr.getBooleanFormulaManager(); + this.imgr = fmgr.getIntegerFormulaManager(); + this.smgr = fmgr.getStringFormulaManager(); + } + + /** The code of the char of s at index i */ + public IntegerFormula codeAt(StringFormula s, IntegerFormula i) { + return smgr.toCodePoint(smgr.charAt(s, i)); + } + + public BooleanFormula isHighSurrogate(IntegerFormula c) { + return bmgr.and(imgr.greaterOrEquals(c, imgr.makeNumber(Character.MIN_HIGH_SURROGATE)), + imgr.lessOrEquals(c, imgr.makeNumber(Character.MAX_HIGH_SURROGATE))); + } + + public BooleanFormula isLowSurrogate(IntegerFormula c) { + return bmgr.and(imgr.greaterOrEquals(c, imgr.makeNumber(Character.MIN_LOW_SURROGATE)), + imgr.lessOrEquals(c, imgr.makeNumber(Character.MAX_LOW_SURROGATE))); + } + + /** Character.toCodePoint(high, low) */ + public IntegerFormula toCodePoint(IntegerFormula high, IntegerFormula low) { + return imgr.add(imgr.multiply(imgr.subtract(high, imgr.makeNumber(Character.MIN_HIGH_SURROGATE)), imgr.makeNumber(1024)), + imgr.add(imgr.subtract(low, imgr.makeNumber(Character.MIN_LOW_SURROGATE)), + imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT))); + } + + /** The chars of a Java string, one SMT char per UTF-16 char (makeString would join surrogate pairs). */ + public StringFormula chars(String s) { + StringFormula f = smgr.makeString(""); + for (char c : s.toCharArray()) { + f = smgr.concat(f, smgr.fromCodePoint(imgr.makeNumber(c))); + } + return f; + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy index 79044095..8ed60c4e 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy @@ -111,6 +111,10 @@ class StringCaseRegexModelExactnessTest extends Specification { return ThreadHandler.getSymbolicTraceHandler(currentThread().id).symbolicTrace.symbolicPrecisionLoss } + protected static boolean ascii(String... strings) { + return strings.every { it.chars().allMatch { c -> c < 128 } } + } + protected boolean onlyJavasResult(List fixed, BooleanFormula other) { context.newProverEnvironment().withCloseable { p -> ThreadHandler.getSymbolicTraceHandler(currentThread().id).getConstraints().each { p.addConstraint(it) } @@ -153,50 +157,6 @@ class StringCaseRegexModelExactnessTest extends Specification { return v } - // ---- case mapping tables ---- - - def "the case mapping tables give Java's mapping for every char and every cased code point"() { - given: - def cases = new CaseMapping(fmgr) - def codes = (0..0xFFFF) + (0x10400..0x104FF) + (0x10C80..0x10CFF) + (0x118A0..0x118DF) + (0x16E40..0x16E7F) + - (0x1E900..0x1E94F) + [0x10FFFF] - - expect: - CaseMapping.Kind.values().every { kind -> - codes.every { int cp -> - def mapped = fmgr.simplify(cases.apply(kind, imgr.makeNumber(cp))) - imgr.equal(mapped, imgr.makeNumber(CaseMapping.map(kind, cp))).with { fmgr.simplify(it) } == bmgr.makeTrue() - } - } - } - - def "a supplementary code point maps to a supplementary one with the same high surrogate"() { - expect: - CaseMapping.Kind.values().every { kind -> - (0x10000..0x10FFFF).every { int cp -> - int m = CaseMapping.map(kind, cp) - m == cp || (m >= 0x10000 && Character.highSurrogate(m) == Character.highSurrogate(cp)) - } - } - } - - def "String.toLowerCase/toUpperCase map char by char, except 'Σ'"() { - // The model maps each char (and each surrogate pair) on its own; Java does too, apart from final sigma. - given: - def random = new Random(1) - def pool = ((0..0xFFFF).findAll { !Character.isSurrogate((char) it) && it != 0x3a3 }.collect { String.valueOf((char) it) } - + [DESERET_UPPER, DESERET_LOWER]) - - expect: - (0..<2000).every { - def parts = (0.. Date: Mon, 19 Oct 2026 16:07:40 +0000 Subject: [PATCH 3/4] Leave toLowerCase/toUpperCase of symbolic strings unmodelled; pin before the ASCII split Unrolled over a pinned length, the search reached hardly any other length (the securibench violations were then missed), and unrolled up to a bound Z3 took seconds per query. A concrete string is mapped concretely. The ignore-case comparisons pin the length before they split off the ASCII strings: with the length fixed, Z3 decides the other side of the split at once, where the int2bv of a free string length made it hang. Co-Authored-By: Claude Opus 5.5 --- .../invoke/java/lang/StringCallBranches.java | 23 +++--- .../value/reference/lang/CaseMapping.java | 42 ++--------- .../value/reference/lang/StringValue.java | 28 ++++--- .../StringCaseRegexModelExactnessTest.groovy | 74 +++---------------- 4 files changed, 44 insertions(+), 123 deletions(-) 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 index 58086329..02f4298f 100644 --- 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 @@ -117,12 +117,17 @@ private void ofString(StringValue s, String name, String desc, Value[] arg } case "equalsIgnoreCase(Ljava/lang/String;)Z" -> { if (args[0] instanceof StringValue other && (s.isSymbolic() || other.isSymbolic()) - && !StringValue.equalsIgnoreCaseByRegex(s, other) && ascii(s, other)) { - // Strings of different lengths differ, else the comparison by the pinned length + && !StringValue.equalsIgnoreCaseByRegex(s, other)) { + // Strings of different lengths differ, else the comparison of ASCII strings by + // the pinned length. (The pin comes first: with the length fixed, the solver + // decides the other side of the ASCII split easily.) Int len = length(s); Int otherLen = length(other); split(imgr.equal(len.f(), otherLen.f()), len.c() == otherLen.c()); - if (len.c() == otherLen.c()) pin(len); + if (len.c() == otherLen.c()) { + pin(len); + ascii(s, other); + } } } case "regionMatches(ZILjava/lang/String;II)Z" -> { @@ -137,19 +142,19 @@ private void ofString(StringValue s, String name, String desc, Value[] arg imgr.lessOrEquals(toffset.f(), imgr.subtract(length(s).f(), len.f())), imgr.lessOrEquals(ooffset.f(), imgr.subtract(length(other).f(), len.f()))), inBounds); - if (inBounds && ascii(s, other)) pin(len); + if (inBounds) { + pin(len); + ascii(s, other); + } } } case "compareToIgnoreCase(Ljava/lang/String;)I" -> { - if (args[0] instanceof StringValue other && ascii(s, other)) { + if (args[0] instanceof StringValue other) { pin(length(s)); pin(length(other)); + ascii(s, other); } } - case "toLowerCase()Ljava/lang/String;", "toLowerCase(Ljava/util/Locale;)Ljava/lang/String;", - "toUpperCase()Ljava/lang/String;", "toUpperCase(Ljava/util/Locale;)Ljava/lang/String;" -> { - if (StringValue.caseMappingLocale(args) != null && ascii(s)) pin(length(s)); - } default -> { } } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java index ba9b0160..883c9e9b 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java @@ -15,23 +15,16 @@ import org.sosy_lab.java_smt.api.StringFormulaManager; /** - * Java's case mappings as formulas: the ignore-case comparison against a concrete string as a - * regular expression of the chars' case classes (tabulated from the running JVM), and the case - * mappings and ignore-case comparisons of ASCII strings char by char. + * Java's ignore-case comparisons as formulas: against a concrete string as a regular expression + * of the chars' case classes (tabulated from the running JVM), and of two ASCII strings char by + * char. * - *

    Beyond ASCII the mappings are tables of a few hundred ranges; unrolled over a string, Z3 does - * not decide queries over them (even simple ones time out), so a model separates the ASCII strings - * by a branch and leaves the others unmodelled. + *

    Beyond ASCII the case mappings are tables of a few hundred ranges; unrolled over a string, Z3 + * does not decide queries over them (even simple ones time out), so a model separates the ASCII + * strings by a branch and leaves the others unmodelled. */ public final class CaseMapping { - public enum Kind { - /** Character.toLowerCase / String.toLowerCase */ - LOWER, - /** Character.toUpperCase / String.toUpperCase */ - UPPER - } - /** The chars by their key Character.toLowerCase(Character.toUpperCase(c)), by which the ignore-case comparisons compare. */ private static final class FoldClasses { static final Map> CLASSES = new HashMap<>(); @@ -67,15 +60,6 @@ public static boolean rootRules(Locale locale) { return !lang.equals("tr") && !lang.equals("az") && !lang.equals("lt"); } - /** The chars of a Java string, one SMT char per UTF-16 char (makeString would join surrogate pairs). */ - public StringFormula chars(String s) { - StringFormula f = smgr.makeString(""); - for (char c : s.toCharArray()) { - f = smgr.concat(f, smgr.fromCodePoint(imgr.makeNumber(c))); - } - return f; - } - /** * The strings equal to t ignoring case (t has no surrogates): at each position, the chars with * the same key as t's char there. A surrogate of the other string matches none of them, also @@ -113,20 +97,6 @@ public IntegerFormula foldAscii(IntegerFormula c) { return bmgr.ifThenElse(between(c, 'A', 'Z'), imgr.add(c, imgr.makeNumber('a' - 'A')), c); } - /** toLowerCase/toUpperCase of the first n chars of s, all ASCII (for a locale with the root rules). */ - public StringFormula mapAscii(Kind kind, StringFormula s, int n) { - StringFormula result = smgr.makeString(""); - for (int i = 0; i < n; i++) { - StringFormula ch = smgr.charAt(s, imgr.makeNumber(i)); - IntegerFormula c = smgr.toCodePoint(ch); - StringFormula mapped = kind == Kind.LOWER - ? bmgr.ifThenElse(between(c, 'A', 'Z'), smgr.fromCodePoint(imgr.add(c, imgr.makeNumber('a' - 'A'))), ch) - : bmgr.ifThenElse(between(c, 'a', 'z'), smgr.fromCodePoint(imgr.subtract(c, imgr.makeNumber('a' - 'A'))), ch); - result = smgr.concat(result, mapped); - } - return result; - } - /** The result of an ignore-case comparison: whether no char differed, and the int compareToIgnoreCase returns. */ public record Comparison(BooleanFormula noDifference, IntegerFormula value) {} 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 22f6d891..d55dae19 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 @@ -536,19 +536,18 @@ public static java.util.Locale caseMappingLocale(Value[] args) { } /** - * toLowerCase()/toLowerCase(Locale) (kind LOWER) and toUpperCase()/toUpperCase(Locale) (UPPER) - * of an ASCII string, which the call's branches separate (StringCallBranches), char by char - * over the pinned length. Other strings are not modelled (see CaseMapping). + * toLowerCase()/toLowerCase(Locale) and toUpperCase()/toUpperCase(Locale) of a concrete string. + * Of a symbolic one they are not modelled: unrolled over a pinned length, the search reached + * hardly any other length, and unrolled up to a bound Z3 took seconds per query (see + * CaseMapping for the chars beyond ASCII). */ - private Value invokeCaseMapping(CaseMapping.Kind kind, Value[] args) { + private Value invokeCaseMapping(boolean lower, Value[] args) { if (args.length > 1) return PlaceHolder.instance; java.util.Locale locale = caseMappingLocale(args); if (locale == null) return PlaceHolder.instance; - String result = kind == CaseMapping.Kind.LOWER ? concrete.toLowerCase(locale) : concrete.toUpperCase(locale); - CaseMapping cases = new CaseMapping(context.getFormulaManager()); - if (!isSymbolic()) return new StringValue(context, result, cases.chars(result), -1); - if (!asciiStrings(this) || concrete.length() > MAX_UNROLLED) return PlaceHolder.instance; - return new StringValue(context, result, cases.mapAscii(kind, formula, concrete.length()), -1); + String result = lower ? concrete.toLowerCase(locale) : concrete.toUpperCase(locale); + if (isSymbolic()) return PlaceHolder.instance; + return new StringValue(context, result, new Utf16(context.getFormulaManager()).chars(result), -1); } /** @@ -695,13 +694,12 @@ public static java.util.Locale caseMappingLocale(Value[] args) { String t = isSymbolic() ? other.concrete : concrete; return new BooleanValue(context, result, smgr.in(symbolic.formula, cases.equalIgnoringCase(t))); } - // The call's branches (StringCallBranches): whether both are ASCII, whether the lengths are - // equal, then the length is pinned. Strings of different lengths are not equal. + // The call's branches (StringCallBranches): whether the lengths are equal, then the length + // is pinned and the ASCII strings separated. Strings of different lengths are not equal. BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); int n = concrete.length(); - if (!asciiStrings(this, other)) return PlaceHolder.instance; if (n != other.concrete.length()) return new BooleanValue(context, false, bmgr.makeFalse()); - if (n > MAX_UNROLLED) return PlaceHolder.instance; + if (n > MAX_UNROLLED || !asciiStrings(this, other)) return PlaceHolder.instance; return new BooleanValue(context, result, cases.compareAsciiIgnoringCase(formula, imgr.makeNumber(0), n, other.formula, imgr.makeNumber(0), n).noDifference()); } @@ -1487,7 +1485,7 @@ private static String literalRegexArgument(Value[] args) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeToLowerCase(Value[] args, Type[] desc) { - return invokeCaseMapping(CaseMapping.Kind.LOWER, args); + return invokeCaseMapping(true, args); } /** @@ -1517,7 +1515,7 @@ private static String literalRegexArgument(Value[] args) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeToUpperCase(Value[] args, Type[] desc) { - return invokeCaseMapping(CaseMapping.Kind.UPPER, args); + return invokeCaseMapping(false, args); } /** diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy index 8ed60c4e..c792ad61 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy @@ -159,70 +159,17 @@ class StringCaseRegexModelExactnessTest extends Specification { // ---- toLowerCase / toUpperCase ---- - @Unroll - def "toLowerCase and toUpperCase are exact: '#sample' #localeName"() { - given: - def s = symbolicString("s", sample) - def args = l == null ? [] : [locale(l)] - def desc = l == null ? [] : [LOCALE] - def javaDesc = l == null ? "()Ljava/lang/String;" : "(Ljava/util/Locale;)Ljava/lang/String;" - - when: - def lower = call(s, "toLowerCase", desc, args) - def upper = call(s, "toUpperCase", desc, args) - def fixedLower = [fix(s)] + branches(s, "toLowerCase", javaDesc, args) - def fixedUpper = [fix(s)] + branches(s, "toUpperCase", javaDesc, args) - - then: - // Only ASCII strings are modelled, the others are separated by a branch. - !ascii(sample) || exactString(fixedLower, (StringValue) lower, sample.toLowerCase(l ?: Locale.getDefault())) - !ascii(sample) || exactString(fixedUpper, (StringValue) upper, sample.toUpperCase(l ?: Locale.getDefault())) - ascii(sample) || (lower instanceof PlaceHolder && upper instanceof PlaceHolder) - - where: - [sample, l] << [CASE_SAMPLES + ["Hello World", "aİbßc"], [null, Locale.ROOT, Locale.ENGLISH, Locale.UK]].combinations() - localeName = l == null ? "default" : l.toString() - } - - def "toLowerCase separates the ASCII strings, the others are not modelled"() { - given: - def s = symbolicString("s", "a\u00c4") - - when: - def r = call(s, "toLowerCase", [LOCALE], [locale(Locale.ROOT)]) - def b = StringCallBranches.of(s, "toLowerCase", "(Ljava/util/Locale;)Ljava/lang/String;", [locale(Locale.ROOT)] as Value[]) - - then: - r instanceof PlaceHolder - b.size() == 1 - !b[0].holds() - !b[0].check() - onlyJavasResult([fix(s)], b[0].condition()) - satisfiable([b[0].condition(), smgr.equal(s.formula, chars("aB"))]) - } - - def "toLowerCase pins the length"() { + def "toLowerCase/toUpperCase of a concrete string are concrete, of a symbolic one not modelled"() { given: + def c = new StringValue(context, "Ab\u00df", -1) def s = symbolicString("s", "Ab") - when: - def b = branches(s, "toLowerCase", "()Ljava/lang/String;", []) - - then: - onlyJavasResult(b, bmgr.not(imgr.equal(smgr.length(s.formula), imgr.makeNumber(2)))) - satisfiable(b + [smgr.equal(s.formula, chars("xy"))]) - } - - def "toLowerCase with the Turkish locale or an unknown one is not modelled"() { - given: - def s = symbolicString("s", "I") - def unknown = new ObjectValue(context, "java/util/Locale", new IntValue(context, 0), -1) - expect: - call(s, "toLowerCase", [LOCALE], [locale(new Locale("tr"))]) instanceof PlaceHolder - call(s, "toUpperCase", [LOCALE], [locale(new Locale("lt"))]) instanceof PlaceHolder - call(s, "toLowerCase", [LOCALE], [unknown]) instanceof PlaceHolder - StringCallBranches.of(s, "toLowerCase", "(Ljava/util/Locale;)Ljava/lang/String;", [locale(new Locale("tr"))] as Value[]).isEmpty() + ((StringValue) call(c, "toLowerCase", [LOCALE], [locale(Locale.UK)])).concrete == "ab\u00df" + ((StringValue) call(c, "toUpperCase", [], [])).concrete == "AbSS".toUpperCase() + call(s, "toLowerCase", [], []) instanceof PlaceHolder + call(c, "toLowerCase", [LOCALE], [locale(new Locale("tr"))]) instanceof PlaceHolder + StringCallBranches.of(s, "toLowerCase", "()Ljava/lang/String;", [] as Value[]).isEmpty() } // ---- equalsIgnoreCase / regionMatches(true, ...) / compareToIgnoreCase ---- @@ -238,8 +185,9 @@ class StringCaseRegexModelExactnessTest extends Specification { def r2 = call(t, "equalsIgnoreCase", [STRING], [s]) then: - // Against a concrete string with a surrogate the comparison is modelled for ASCII strings only. - b.chars().anyMatch { Character.isSurrogate((char) it) } ? (r1 instanceof PlaceHolder && r2 instanceof PlaceHolder) : + // Against a concrete string with a surrogate the comparison is modelled for strings of + // different lengths and ASCII strings only. + b.chars().anyMatch { Character.isSurrogate((char) it) } && a.length() == b.length() ? (r1 instanceof PlaceHolder && r2 instanceof PlaceHolder) : (exactBoolean([fix(s)] + branches(s, "equalsIgnoreCase", "(Ljava/lang/String;)Z", [t]), (BooleanValue) r1, a.equalsIgnoreCase(b)) && exactBoolean([fix(s)] + branches(t, "equalsIgnoreCase", "(Ljava/lang/String;)Z", [s]), (BooleanValue) r2, b.equalsIgnoreCase(a))) !precisionLoss() @@ -259,7 +207,7 @@ class StringCaseRegexModelExactnessTest extends Specification { def fixed = [fix(s), fix(t)] + branches(s, "equalsIgnoreCase", "(Ljava/lang/String;)Z", [t]) then: - ascii(a, b) ? exactBoolean(fixed, (BooleanValue) r, a.equalsIgnoreCase(b)) : r instanceof PlaceHolder + (ascii(a, b) || a.length() != b.length()) ? exactBoolean(fixed, (BooleanValue) r, a.equalsIgnoreCase(b)) : r instanceof PlaceHolder where: [a, b] << ([["", "a", "A", "ab", "AB", "ß", "DŽ", "dž", "ı", "I", DESERET_UPPER, DESERET_LOWER, From 29b8c03dda683ad748760841211d6f563ac10f90 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Mon, 19 Oct 2026 17:16:13 +0000 Subject: [PATCH 4/4] Test equalsIgnoreCase of two symbolic strings under its branches The model is exact for the pinned length; the test now takes the call's branches and asks for other strings of that length. Co-Authored-By: Claude Opus 5.5 --- .../reference/lang/StringValueTest.groovy | 21 ++++++++++++------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringValueTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringValueTest.groovy index b31c470b..c9742a9a 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringValueTest.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringValueTest.groovy @@ -1,5 +1,6 @@ package de.uzl.its.value.reference.lang +import de.uzl.its.swat.symbolic.invoke.java.lang.StringCallBranches 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.reference.lang.StringValue @@ -194,7 +195,7 @@ class StringValueTest extends Specification { } @Unroll - def "equalsIgnoreCase(String anotherString) - Two symbolic strings - enforced length" (String s1, String s2, boolean expected) { + def "equalsIgnoreCase(String anotherString) - Two symbolic strings - other strings of the pinned length" (String s1, String s2, boolean expected) { setup: prover.push() def lhs = new StringValue(context, s1, smgr.makeVariable("s1"), -1) @@ -204,20 +205,24 @@ class StringValueTest extends Specification { when: def result = (BooleanValue) lhs.invokeMethod("equalsIgnoreCase", STRING_DESC, args) addUFConstraintsFromTrace() + // The call's branches as they hold here: lengths, pinned length, ASCII strings + StringCallBranches.of(lhs, "equalsIgnoreCase", "(Ljava/lang/String;)Z", args).each { + prover.addConstraint(it.holds() ? it.condition() : bmgr.not(it.condition())) + } + // Other strings than the concrete ones, with the opposite result + prover.addConstraint(bmgr.not(smgr.equal(lhs.formula, smgr.makeString(s1)))) forceMismatch(result.formula, expected) - // |s1| = 10 - prover.addConstraint(imgr.equal(smgr.length(lhs.formula), imgr.makeNumber(10))) then: - !prover.isUnsat() result.concrete == expected noExceptionThrown() and: + // Strings with the other result exist (of the same length), and the model gives it them + !prover.isUnsat() def (s1Model, s2Model) = evaluateModel(lhs.formula, rhs.formula) - assert s1Model != null - assert s1Model.length() == 10 - assert (s1Model.equalsIgnoreCase(s2Model)) != expected + s1Model.length() == s1.length() + s1Model.equalsIgnoreCase(s2Model) != expected cleanup: prover.pop() @@ -225,6 +230,6 @@ class StringValueTest extends Specification { where: s1 | s2 | expected "hello" | "HELLO" | true - "Hello" | "bar" | false + "Hello" | "World" | false } }