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/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..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 @@ -1,10 +1,12 @@ 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; 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; @@ -14,6 +16,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; /** @@ -25,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. @@ -34,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) {} @@ -85,7 +93,68 @@ 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 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); + ascii(s, other); + } + } + } + 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]); + 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()))), + inBounds); + if (inBounds) { + pin(len); + ascii(s, other); + } + } + } + case "compareToIgnoreCase(Ljava/lang/String;)I" -> { + if (args[0] instanceof StringValue other) { + pin(length(s)); + pin(length(other)); + ascii(s, other); + } + } default -> { } } } @@ -93,7 +162,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 +242,37 @@ 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); + 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); @@ -215,7 +318,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/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..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,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.Utf16; 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 Utf16(context.getFormulaManager()).chars(reversed)); + return this; + } + int n = stringValue.concrete.length(); + if (n > 256) return PlaceHolder.instance; + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + 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 + 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..883c9e9b --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/CaseMapping.java @@ -0,0 +1,125 @@ +package de.uzl.its.swat.symbolic.value.reference.lang; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; +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 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 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 { + + /** 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 (int c = 0; c <= 0xFFFF; c++) { + CLASSES.computeIfAbsent(fold(c), k -> new ArrayList<>()).add(c); + } + } + } + + private final BooleanFormulaManager bmgr; + private final IntegerFormulaManager imgr; + private final StringFormulaManager smgr; + + public CaseMapping(FormulaManager fmgr) { + this.bmgr = fmgr.getBooleanFormulaManager(); + this.imgr = fmgr.getIntegerFormulaManager(); + this.smgr = fmgr.getStringFormulaManager(); + } + + /** 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 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 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 : FoldClasses.CLASSES.get(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; + } + + /** Whether all chars of s are ASCII (below 128). */ + public BooleanFormula isAscii(StringFormula s) { + return smgr.in(s, smgr.closure(smgr.range('\u0000', '\u007f'))); + } + + /** The code of the char of s at index i */ + public IntegerFormula codeAt(StringFormula s, IntegerFormula i) { + return smgr.toCodePoint(smgr.charAt(s, i)); + } + + 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 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); + } + + /** 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), 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 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); + 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/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..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 @@ -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(); + 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); + 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(); + 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); + 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) return PlaceHolder.instance; + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + 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); + 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,68 @@ 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); + // 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) 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()); + } + + /** 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 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), for ASCII strings. + */ + 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) 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(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 = lower ? concrete.toLowerCase(locale) : concrete.toUpperCase(locale); + if (isSymbolic()) return PlaceHolder.instance; + return new StringValue(context, result, new Utf16(context.getFormulaManager()).chars(result), -1); } /** @@ -564,38 +682,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 and the ASCII strings separated. 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 || !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()); } /** @@ -932,7 +1038,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 +1075,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 +1100,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 || !asciiStrings(this, other)) return PlaceHolder.instance; + BooleanFormula ignoringCase = n <= 0 ? bmgr.makeTrue() + : 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); + } + + /** 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 +1136,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 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); } /** @@ -1073,7 +1216,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 +1248,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 +1485,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(true, args); } /** @@ -1348,7 +1515,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(false, args); } /** 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 new file mode 100644 index 00000000..c792ad61 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringCaseRegexModelExactnessTest.groovy @@ -0,0 +1,517 @@ +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 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) } + 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 + } + + // ---- toLowerCase / toUpperCase ---- + + 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") + + expect: + ((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 ---- + + @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: + // 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() + + 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: + (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, + "\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: + (r instanceof PlaceHolder && !ascii(a, b) && StringValue.regionInBounds(a, to, b, oo, len)) + || 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, 1], [0, 1], [-1, 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: + ascii(a, b) ? exactInt(fixed, (IntValue) r, a.compareToIgnoreCase(b)) : r instanceof PlaceHolder + + 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() + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy index 94c95b44..105cfea5 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy @@ -545,9 +545,10 @@ class StringModelExactnessTest extends Specification { def "after a change that is not modelled the chars are unknown, until resynced"() { given: def sb = builder(symbolicString("s", "ab")) + def unmodelled = new ObjectValue(context, "x/Unknown", new IntValue(context, 0), -1) when: - call(sb, "reverse", [], []) + call(sb, "insert", [INT, OBJECT], [new IntValue(context, 0), unmodelled]) then: sb.unknown 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 } }