diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java index 771f7759..bbb2ced5 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java @@ -16,6 +16,7 @@ import de.uzl.its.swat.metadata.ClassDepotRuntime; import de.uzl.its.swat.symbolic.instruction.*; import de.uzl.its.swat.symbolic.invoke.InvocationHandler; +import de.uzl.its.swat.symbolic.invoke.java.lang.StringCallBranches; import de.uzl.its.swat.symbolic.processor.InstructionProcessor; import de.uzl.its.swat.symbolic.processor.SymbolicInstructionProcessor; import de.uzl.its.swat.symbolic.shadow.Frame; @@ -1363,11 +1364,16 @@ public void visitGETVALUE_Object(GETVALUE_Object inst) throws SymbolicInstruc } Logger shadowStateLogger = ThreadHandler.getShadowStateLogger(currentThread().getId()); shadowStateLogger.info("Recovered object from heap: {}", tmp); - if (tmp instanceof StringBuilderValue sbv) { - StringBuilder sb = (StringBuilder) inst.val; - SWATAssert.check(sbv.getStringValue().concrete.equals(inst.val), - "Concrete value of the StringBuilder does not match the value in the stack: {} | {}", - sbv.getStringValue().concrete, sb.toString()); + if (tmp instanceof StringBuilderValue sbv && inst.val != null) { + String chars = inst.val.toString(); + if (sbv.isUnknown() || sbv.getStringValue() == null) { + // A change SWAT does not model left its chars unknown: take the concrete ones. + sbv.resync(chars); + } else { + SWATAssert.check(sbv.getStringValue().concrete.equals(chars), + "Concrete value of the StringBuilder does not match the value in the stack: {} | {}", + sbv.getStringValue().concrete, chars); + } } stack.pushOperand(tmp); } else if (inst.address == 0) { @@ -2300,6 +2306,57 @@ public void visitINSTANCEOF(INSTANCEOF inst) throws SymbolicInstructionException } } + /** + * Records the branches a String or StringBuilder call takes inside the library, which their + * models rely on (see {@link StringCallBranches}): its index checks, and pins of the concrete + * values a model uses. On a normal return all of them held; a call that threw failed one of the + * index checks, if the receiver's chars say so, and that exception is then fully explained by + * the branches. + * + * @param returned Whether the call returned normally + * @return Whether the call threw at one of its index checks + */ + private boolean recordStringCallBranches(long iid, String name, String desc, ObjectValue instance, Value[] arguments, boolean returned) throws NoThreadContextException { + List branches = StringCallBranches.of(instance, name, desc, arguments); + int failed = -1; + for (int i = 0; i < branches.size() && failed < 0; i++) { + if (!branches.get(i).holds()) failed = i; + } + // A normal return where an index check failed (or a throw where all held): the shadow + // does not match the call; that is left to the model and to recordThrowingCall. + if (branches.isEmpty() || returned == (failed >= 0)) return false; + int last = returned ? branches.size() - 1 : failed; + FormulaManager fmgr = instance.context.getFormulaManager(); + for (int i = 0; i <= last; i++) { + StringCallBranches.Branch branch = branches.get(i); + if (!fmgr.extractVariables(branch.condition()).isEmpty()) { + symbolicTraceHandler.checkAndSetLibraryBranch(branch.holds(), branch.condition(), determineIid(iid), "#" + name); + } + } + return !returned; + } + + /** + * As {@link #recordThrowingCall}, unless the call threw at an index check of a String or + * StringBuilder method (see {@link #recordStringCallBranches}), which the trace then explains. + */ + private void recordThrowingInstanceCall(long iid, String owner, String name, String desc, long invokeId) throws NoThreadContextException { + boolean explained; + try { + ObjectValue instance = stack.getInstance(); + Value[] arguments = stack.fetchArgumentsFromLocals(Type.getArgumentTypes(desc), true); + explained = recordStringCallBranches(iid, name, desc, instance, arguments, false); + } catch (Exception e) { + explained = false; + } + if (explained) { + // Not an exception the static pre-analysis graph models (it walks over library calls). + recordUnmodelledException(iid); + } else { + recordThrowingCall(iid, owner, name, desc, invokeId, true); + } + } + /** * Handles a call to an uninstrumented method that threw instead of returning: its model, if it * has one, is not consulted (that happens on a normal return), and whether it throws may depend @@ -2340,6 +2397,7 @@ public void visitINVOKEINTERFACE(INVOKEINTERFACE inst) throws SymbolicInstructio ObjectValue instance = stack.getInstance(); Value[] arguments = stack.fetchArgumentsFromLocals(Type.getArgumentTypes(inst.desc), true); + recordStringCallBranches(inst.iid, inst.name, inst.desc, instance, arguments, true); Value retVal = InvocationHandler.invoke( symbolicTraceHandler, inst.desc, @@ -2352,7 +2410,7 @@ public void visitINVOKEINTERFACE(INVOKEINTERFACE inst) throws SymbolicInstructio stack.setReturnValue(retVal); } else if (stack.getNextInst() instanceof INVOKEMETHOD_EXCEPTION) { - recordThrowingCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId, true); + recordThrowingInstanceCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId); } if (!inst.owner.equals("de/uzl/its/swat/Main")) { @@ -2376,6 +2434,7 @@ public void visitINVOKESPECIAL(INVOKESPECIAL inst) throws SymbolicInstructionExc if (stack.getNextInst() instanceof INVOKEMETHOD_END) { ObjectValue instance = stack.getInstance(); Value[] arguments = stack.fetchArgumentsFromLocals(Type.getArgumentTypes(inst.desc), true); + recordStringCallBranches(inst.iid, inst.name, inst.desc, instance, arguments, true); Value retVal = InvocationHandler.invoke( symbolicTraceHandler, inst.desc, @@ -2387,7 +2446,7 @@ public void visitINVOKESPECIAL(INVOKESPECIAL inst) throws SymbolicInstructionExc instance); stack.setReturnValue(retVal); } else if (stack.getNextInst() instanceof INVOKEMETHOD_EXCEPTION) { - recordThrowingCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId, true); + recordThrowingInstanceCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId); } if (!inst.owner.equals("de/uzl/its/swat/Main")) { @@ -2458,6 +2517,7 @@ public void visitINVOKEVIRTUAL(INVOKEVIRTUAL inst) throws SymbolicInstructionExc if (stack.getNextInst() instanceof INVOKEMETHOD_END) { ObjectValue instance = stack.getInstance(); Value[] arguments = stack.fetchArgumentsFromLocals(Type.getArgumentTypes(inst.desc), true); + recordStringCallBranches(inst.iid, inst.name, inst.desc, instance, arguments, true); Value retVal = InvocationHandler.invoke( symbolicTraceHandler, inst.desc, @@ -2469,7 +2529,7 @@ public void visitINVOKEVIRTUAL(INVOKEVIRTUAL inst) throws SymbolicInstructionExc instance); stack.setReturnValue(retVal); } else if (stack.getNextInst() instanceof INVOKEMETHOD_EXCEPTION) { - recordThrowingCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId, true); + recordThrowingInstanceCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId); } if (!inst.owner.equals("de/uzl/its/swat/Main")) { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringCallBranches.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringCallBranches.java new file mode 100644 index 00000000..59ce6675 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/StringCallBranches.java @@ -0,0 +1,221 @@ +package de.uzl.its.swat.symbolic.invoke.java.lang; + +import de.uzl.its.swat.symbolic.value.Value; +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue; +import de.uzl.its.swat.symbolic.value.reference.ObjectValue; +import de.uzl.its.swat.symbolic.value.reference.StringBuilderValue; +import de.uzl.its.swat.symbolic.value.reference.array.CharArrayValue; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import java.util.ArrayList; +import java.util.List; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +/** + * The branches a call of a String or StringBuilder method takes inside the library, which the + * models of these methods (StringValue, StringBuilderValue) rely on. The visitor records them in the + * trace, so the solver can take their other side: + * + * + * + * Index checks come first: the pins are only reached when the indices are in range. + */ +public final class StringCallBranches { + + /** A branch: its condition and whether it held in this run. */ + public record Branch(BooleanFormula condition, boolean holds) {} + + /** An int the checks are about, as a formula over the integers and concretely. */ + private record Int(IntegerFormula f, long c, boolean symbolic) {} + + private final SolverContext context; + private final BooleanFormulaManager bmgr; + private final IntegerFormulaManager imgr; + private final StringFormulaManager smgr; + private final List branches = new ArrayList<>(); + + private StringCallBranches(SolverContext context) { + this.context = context; + FormulaManager fmgr = context.getFormulaManager(); + this.bmgr = fmgr.getBooleanFormulaManager(); + this.imgr = fmgr.getIntegerFormulaManager(); + this.smgr = fmgr.getStringFormulaManager(); + } + + /** + * The branches of calling {@code name} with descriptor {@code desc} on {@code instance}, in + * order: empty if the method has none or is not modelled. The concrete values are those before + * the call. + */ + public static List of(Value instance, String name, String desc, Value[] args) { + try { + if (instance instanceof StringValue str) { + StringCallBranches b = new StringCallBranches(str.context); + b.ofString(str, name, desc, args); + return b.branches; + } else if (instance instanceof StringBuilderValue sb && sb.getContent() != null) { + StringCallBranches b = new StringCallBranches(sb.context); + b.ofStringBuilder(sb.getContent(), name, desc, args); + return b.branches; + } + } catch (Exception e) { + // Arguments of unexpected types: the model returns a PlaceHolder for them as well. + } + return List.of(); + } + + private void ofString(StringValue s, String name, String desc, Value[] args) throws Exception { + switch (name + desc) { + case "charAt(I)C" -> index(s, args[0]); + case "substring(I)Ljava/lang/String;" -> range(s, num(args[0]), length(s)); + case "substring(II)Ljava/lang/String;", "subSequence(II)Ljava/lang/CharSequence;" -> + range(s, num(args[0]), num(args[1])); + case "getChars(II[CI)V" -> getChars(s, args); + case "toCharArray()[C" -> pin(length(s)); + case "([C)V" -> pin(size(args[0])); + case "lastIndexOf(I)I", "lastIndexOf(II)I" -> pin(num(args[0])); + default -> { } + } + } + + private void ofStringBuilder(StringValue s, String name, String desc, Value[] args) throws Exception { + String sig = name + desc.substring(0, desc.indexOf(')') + 1); + switch (sig) { + case "charAt(I)", "setCharAt(IC)", "deleteCharAt(I)" -> index(s, args[0]); + case "delete(II)", "replace(IILjava/lang/String;)" -> { + // An end past the length is taken as the length: start in [0, min(end, length)]. + Int start = num(args[0]); + Int end = num(args[1]); + Int len = length(s); + add(bmgr.and(imgr.greaterOrEquals(start.f(), zero()), imgr.lessOrEquals(start.f(), end.f()), + imgr.lessOrEquals(start.f(), len.f())), + 0 <= start.c() && start.c() <= end.c() && start.c() <= len.c()); + } + case "substring(I)" -> range(s, num(args[0]), length(s)); + case "substring(II)", "subSequence(II)" -> range(s, num(args[0]), num(args[1])); + case "setLength(I)" -> { + Int n = num(args[0]); + add(imgr.greaterOrEquals(n.f(), zero()), n.c() >= 0); + pin(n); + } + case "getChars(II[CI)" -> getChars(s, args); + case "appendCodePoint(I)" -> { + Int cp = num(args[0]); + add(bmgr.and(imgr.greaterOrEquals(cp.f(), zero()), imgr.lessOrEquals(cp.f(), imgr.makeNumber(Character.MAX_CODE_POINT))), + Character.isValidCodePoint((int) cp.c())); + } + case "append([C)" -> pin(size(args[0])); + case "append([CII)" -> { + // checkRange(offset, offset + len, str.length), in int arithmetic: with all three + // pinned, the check is concrete. + pin(num(args[1])); + pin(num(args[2])); + pin(size(args[0])); + } + case "append(Ljava/lang/CharSequence;II)" -> { + StringValue seq = sequence(args[0]); + if (seq != null) range(seq, num(args[1]), num(args[2])); + } + default -> { + if (name.equals("insert")) insert(s, desc, args); + } + } + } + + private void insert(StringValue s, String desc, Value[] args) throws Exception { + // insert(int offset, ...): the offset in [0, length] + Int offset = num(args[0]); + Int len = length(s); + add(bmgr.and(imgr.greaterOrEquals(offset.f(), zero()), imgr.lessOrEquals(offset.f(), len.f())), + 0 <= offset.c() && offset.c() <= len.c()); + if (desc.startsWith("(I[CII)")) { + pin(num(args[2])); + pin(num(args[3])); + pin(size(args[1])); + } else if (desc.startsWith("(I[C)")) { + pin(size(args[1])); + } else if (desc.startsWith("(ILjava/lang/CharSequence;II)")) { + StringValue seq = sequence(args[1]); + if (seq != null) range(seq, num(args[2]), num(args[3])); + } + } + + /** getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin) of String and StringBuilder. */ + private void getChars(StringValue s, Value[] args) throws Exception { + Int srcBegin = num(args[0]); + Int srcEnd = num(args[1]); + range(s, srcBegin, srcEnd); + if (!(args[2] instanceof CharArrayValue)) return; + Int dstBegin = num(args[3]); + Int dstLength = size(args[2]); + // dst[dstBegin, dstBegin + srcEnd - srcBegin) in range (srcBegin <= srcEnd holds here) + IntegerFormula end = imgr.add(dstBegin.f(), imgr.subtract(srcEnd.f(), srcBegin.f())); + add(bmgr.and(imgr.greaterOrEquals(dstBegin.f(), zero()), imgr.lessOrEquals(end, dstLength.f())), + dstBegin.c() >= 0 && dstBegin.c() + srcEnd.c() - srcBegin.c() <= dstLength.c()); + // The model copies by the concrete indices. + pin(srcBegin); + pin(srcEnd); + pin(dstBegin); + } + + /** 0 <= index < length of s */ + private void index(StringValue s, Value indexArg) throws Exception { + Int i = num(indexArg); + Int len = length(s); + add(bmgr.and(imgr.greaterOrEquals(i.f(), zero()), imgr.lessThan(i.f(), len.f())), + 0 <= i.c() && i.c() < len.c()); + } + + /** 0 <= begin <= end <= length of s */ + private void range(StringValue s, Int b, Int e) { + Int len = length(s); + add(bmgr.and(imgr.greaterOrEquals(b.f(), zero()), imgr.lessOrEquals(b.f(), e.f()), imgr.lessOrEquals(e.f(), len.f())), + 0 <= b.c() && b.c() <= e.c() && e.c() <= len.c()); + } + + private Int num(Value v) throws Exception { + IntValue i = v.asIntValue(); + return new Int(i.asIntegerFormula(), i.concrete, i.isSymbolic()); + } + + private Int length(StringValue s) { + return new Int(smgr.length(s.formula), s.concrete.length(), s.isSymbolic()); + } + + private Int size(Value array) throws Exception { + return num(((CharArrayValue) array).size); + } + + /** The chars of a CharSequence argument; null is taken as "null", as by append and insert. */ + private StringValue sequence(Value v) { + if (v instanceof ObjectValue o && o.isNullValue()) return new StringValue(context, "null", -1); + return StringValue.charsOf(v); + } + + /** x == its concrete value, if x is symbolic */ + private void pin(Int x) { + if (x.symbolic()) { + add(imgr.equal(x.f(), imgr.makeNumber(x.c())), true); + } + } + + private IntegerFormula zero() { + return imgr.makeNumber(0); + } + + private void add(BooleanFormula condition, boolean holds) { + branches.add(new Branch(condition, holds)); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java index e272cf71..b202d940 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java @@ -17,6 +17,7 @@ import de.uzl.its.swat.symbolic.trace.dto.*; import de.uzl.its.swat.thread.ThreadHandler; import de.uzl.its.swat.witness.Witness; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; import java.util.ArrayList; import java.util.HashSet; import java.util.Set; @@ -109,8 +110,11 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage for (InputElement ie : symbolicTrace.getInputs()) { inputNames.add(ie.getName()); } + // The UFs of the exact String models are defined by the trace's constraints (see + // StringValue.EXACT_UFS), so they are no loss of precision either. java.util.function.Predicate isInput = - name -> inputNames.contains(name) || name.matches("[A-Z].*_[0-9].*"); + name -> inputNames.contains(name) || name.matches("[A-Z].*_[0-9].*") + || StringValue.EXACT_UFS.contains(name); boolean symbolicPrecisionLoss = symbolicTrace.isSymbolicPrecisionLoss(); for (Element el : symbolicTrace.getTrace()) { if (el instanceof BranchElement be) { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java index d8e1b62c..2cddaa2c 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java @@ -67,6 +67,21 @@ public void checkAndSetBranch(boolean result, BooleanFormula constraint, long ii symbolicTrace.addTraceElement(current); } + /** + * As {@link #checkAndSetBranch(boolean, BooleanFormula, long, String)}, for a branch inside a + * library call that SWAT models (e.g. the index check of String.charAt). The static pre-analysis + * graph walks over library calls, so the branch is marked as one in a callback: the explorer's + * walk of the graph holds its place, as for application code a library calls back. + */ + public void checkAndSetLibraryBranch(boolean result, BooleanFormula constraint, long iid, String suffix) throws NoThreadContextException { + BooleanFormulaManager bmgr = ThreadHandler.getSolverContext(Thread.currentThread().getId()) + .getFormulaManager().getBooleanFormulaManager(); + BranchElement branch = new BranchElement(result, result ? constraint : bmgr.not(constraint), iid); + place(branch, iid, suffix); + branch.setCallback(true); + symbolicTrace.addTraceElement(branch); + } + /** Records where a branch is: its key and the change of the frame stack since the last branch. */ private static void place(BranchElement branch, long iid, String suffix) throws NoThreadContextException { String key = BranchKeys.keyOf(iid); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java index fe32e31c..556cd3fb 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ValueFactory.java @@ -116,6 +116,8 @@ public static StringValue createStringValue(String concrete, int address) throws return new StringValue(context, s, address); } else if (concrete instanceof IASString s) { return new StringValue(context, s.getString(), address); + } else if (concrete instanceof StringBuilder sb) { + return new StringBuilderValue(context, new StringValue(context, sb.toString(), -1), address); } else if (concrete instanceof Boolean b) { return new BooleanObjectValue(context, new BooleanValue(context, b), address); } else if (concrete instanceof Byte b) { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java index 36c157ef..2cc2dfc7 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java @@ -402,13 +402,16 @@ public DoubleValue asDoubleValue() { @Override public StringValue asStringValue() { - // String theory requires IntegerFormula, so convert BV to Int + // String theory requires IntegerFormula, so convert BV to Int. str.from_int gives "" for a + // negative number, so its digits are those of its absolute value, after a "-". NumeralFormula.IntegerFormula intFormula = bvmgr.toIntegerFormula(formula, true); - return new StringValue( - this.context, - String.valueOf(concrete), - context.getFormulaManager().getStringFormulaManager().toStringFormula(intFormula), - -1); + StringFormulaManager smgr = context.getFormulaManager().getStringFormulaManager(); + IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager(); + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + StringFormula str = bmgr.ifThenElse(imgr.lessThan(intFormula, imgr.makeNumber(0)), + smgr.concat(smgr.makeString("-"), smgr.toStringFormula(imgr.negate(intFormula))), + smgr.toStringFormula(intFormula)); + return new StringValue(this.context, String.valueOf(concrete), str, -1); } @Override diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java index 16645268..274dc03b 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java @@ -219,13 +219,16 @@ public ShortObjectValue asObjectValue() { @Override public StringValue asStringValue() { - // String theory requires IntegerFormula, so convert BV to Int + // String theory requires IntegerFormula, so convert BV to Int. str.from_int gives "" for a + // negative number, so its digits are those of its absolute value, after a "-". NumeralFormula.IntegerFormula intFormula = bvmgr.toIntegerFormula(formula, true); - return new StringValue( - this.context, - String.valueOf(concrete), - context.getFormulaManager().getStringFormulaManager().toStringFormula(intFormula), - -1); + StringFormulaManager smgr = context.getFormulaManager().getStringFormulaManager(); + IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager(); + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + StringFormula str = bmgr.ifThenElse(imgr.lessThan(intFormula, imgr.makeNumber(0)), + smgr.concat(smgr.makeString("-"), smgr.toStringFormula(imgr.negate(intFormula))), + smgr.toStringFormula(intFormula)); + return new StringValue(this.context, String.valueOf(concrete), str, -1); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java index d2854f05..d4b502af 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/StringBuilderValue.java @@ -1,5 +1,6 @@ package de.uzl.its.swat.symbolic.value.reference; +import com.google.common.collect.ImmutableSet; import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.config.Config; @@ -9,16 +10,49 @@ import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.CharValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue; import de.uzl.its.swat.symbolic.value.reference.array.CharArrayValue; +import de.uzl.its.swat.symbolic.value.reference.lang.BoxedValue; import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import java.util.Set; import org.objectweb.asm.Type; import org.sosy_lab.java_smt.api.*; +/** + * Shadow of a StringBuilder: + * its chars as a {@link StringValue}, which is replaced (never changed: it may be a String the + * program holds) on every change. + * + *

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

After a change SWAT does not model (it returned a PlaceHolder), the chars are unknown: every + * method then returns a PlaceHolder, until the builder is recovered from the heap with its concrete + * value ({@link #resync}). + */ public final class StringBuilderValue extends ObjectValue { private final StringFormulaManager smgr; private final IntegerFormulaManager imgr; private StringValue stringValue; + + /** + * The capacity while it is the one the constructor set; null after a change that may grow it + * (the growth policy is not modelled). + */ private IntValue capacity; + /** The methods that do not change the capacity. */ + private static final Set KEEP_CAPACITY = Set.of("charAt", "compareTo", "delete", "deleteCharAt", + "getChars", "indexOf", "lastIndexOf", "length", "reverse", "setCharAt", "subSequence", "substring", + "toString", "capacity"); + + /** Whether a change SWAT does not model left the chars unknown. */ + private boolean unknown = false; + + /** The methods that change the builder: if one is not modelled, the chars are unknown. */ + private static final Set MUTATORS = Set.of("", "append", "appendCodePoint", "delete", + "deleteCharAt", "insert", "replace", "reverse", "setCharAt", "setLength"); + public StringBuilderValue(SolverContext context) { super(context, ObjectValue.ADDRESS_UNKNOWN); this.smgr = context.getFormulaManager().getStringFormulaManager(); @@ -38,6 +72,25 @@ public StringBuilderValue(SolverContext context, StringValue v, int address) { return stringValue; } + /** The chars, or null if they are not known. */ + public StringValue getContent() { + return unknown ? null : stringValue; + } + + public boolean isUnknown() { + return unknown; + } + + /** + * Takes the concrete chars of the builder, e.g. when it is recovered from the heap after a + * change SWAT does not model. A symbolic content was lost at that change already (with a + * context loss: the call returned a PlaceHolder for a symbolic receiver). + */ + public void resync(String chars) { + this.stringValue = new StringValue(context, chars, -1); + this.unknown = false; + } + /** * Handles method invocation for Java's StringBuilder @@ -51,832 +104,303 @@ public StringBuilderValue(SolverContext context, StringValue v, int address) { */ @Override public Value invokeMethod(String name, Type[] desc, Value[] args) throws NotImplementedException, ValueConversionException { - return switch (name) { - case "" -> invokeInit(args, desc); - case "append" -> invokeAppend(args, desc); - case "appendCodePoint" -> invokeAppendCodePoint(args, desc); - case "capacity" -> invokeCapacity(args, desc); - case "charAt" -> invokeCharAt(args, desc); - case "chars" -> invokeChars(args, desc); - case "codePointAt" -> invokeCodePointAt(args, desc); - case "codePointBefore" -> invokeCodePointBefore(args, desc); - case "codePointCount" -> invokeCodePointCount(args, desc); - case "codePoints" -> invokeCodePoints(args, desc); - case "compareTo" -> invokeCompareTo(args, desc); - case "delete" -> invokeDelete(args, desc); - case "deleteCharAt" -> invokeDeleteCharAt(args, desc); - case "ensureCapacity" -> invokeEnsureCapacity(args, desc); - case "getChars" -> invokeGetChars(args, desc); - case "indexOf" -> invokeIndexOf(args, desc); - case "insert" -> invokeInsert(args, desc); - case "lastIndexOf" -> invokeLastIndexOf(args, desc); - case "length" -> invokeLength(args, desc); - case "offsetByCodePoints" -> invokeOffsetByCodePoints(args, desc); - case "replace" -> invokeReplace(args, desc); - case "reverse" -> invokeReverse(args, desc); - case "setCharAt" -> invokeSetCharAt(args, desc); - case "setLength" -> invokeSetLength(args, desc); - case "subSequence" -> invokeSubSequence(args, desc); - case "substring" -> invokeSubstring(args, desc); - case "toString" -> invokeToString(args, desc); - case "trimToSize" -> invokeTrimToSize(args, desc); - default -> PlaceHolder.instance; - }; - } - - /** - * Invocation handling for the String instance method Init(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeInit(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { - int numberOfArgs = args.length; - if (numberOfArgs == 0) { - return invokeInit(); - } else if (numberOfArgs == 1) { - return switch (desc[0].getDescriptor()) { - case "I" -> invokeInit(args[0].asIntValue()); - case "Ljava/lang/String;" -> invokeInit(args[0].asStringValue()); - case "Ljava/lang/CharSequence;" -> invokeInit(args[0].asObjectValue()); + if ((unknown || stringValue == null) && !name.equals("")) return PlaceHolder.instance; + Value result; + try { + result = switch (name) { + case "" -> invokeInit(args, desc); + case "append" -> invokeAppend(args, desc); + case "appendCodePoint" -> invokeAppendCodePoint(args); + case "capacity" -> capacity != null ? capacity : PlaceHolder.instance; + case "charAt" -> invokeCharAt(args); + case "compareTo" -> invokeCompareTo(args); + case "delete" -> invokeDelete(args); + case "deleteCharAt" -> invokeDeleteCharAt(args); + case "ensureCapacity", "trimToSize" -> VoidValue.instance; // the chars stay the same + case "getChars" -> invokeGetChars(args); + case "indexOf", "lastIndexOf" -> stringValue.invokeMethod(name, desc, args); + case "insert" -> invokeInsert(args, desc); + case "length" -> new IntValue(context, stringValue.concrete.length(), smgr.length(stringValue.formula)); + case "replace" -> invokeReplace(args); + case "reverse" -> invokeReverse(); + case "setCharAt" -> invokeSetCharAt(args); + case "setLength" -> invokeSetLength(args); + case "subSequence", "substring" -> invokeSubstring(args); + case "toString" -> new StringValue(context, stringValue.concrete, stringValue.formula, -1); default -> PlaceHolder.instance; }; + } catch (NotImplementedException e) { + // e.g. a double appended, which has no model as a String + result = PlaceHolder.instance; } - return PlaceHolder.instance; - } - - private Value invokeInit() { - this.capacity = new IntValue(this.context, 16); - this.stringValue = new StringValue(this.context, "", -1); - return VoidValue.instance; - } - - private Value invokeInit(IntValue capacity) { - this.capacity = capacity; - this.stringValue = new StringValue(this.context, "", -1); - return VoidValue.instance; - } - - private Value invokeInit(@SuppressWarnings("unused") ObjectValue seq) { - return PlaceHolder.instance; - } - - private Value invokeInit(StringValue str) { - this.capacity = new IntValue(this.context, 16 + str.concrete.length()); - this.stringValue = str; - return VoidValue.instance; - } - - /** - * Invocation handling for the String instance method Append(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeAppend(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { - int numberOfArgs = args.length; - if (numberOfArgs == 1) { - return switch (desc[0].getDescriptor()) { - case "I" -> invokeAppend(args[0].asIntValue().asStringValue()); - case "Z" -> invokeAppend(args[0].asBooleanValue().asStringValue()); - case "C" -> invokeAppend(args[0].asCharValue().asStringValue()); - case "D" -> invokeAppend(args[0].asDoubleValue().asStringValue()); - case "F" -> invokeAppend(args[0].asFloatValue().asStringValue()); - case "J" -> invokeAppend(args[0].asLongValue().asStringValue()); - case "Ljava/lang/String;" -> invokeAppend(args[0].asStringValue()); - case "Ljava/lang/CharSequence;", - "Ljava/lang/StringBuffer;", - "Ljava/lang/Object;" -> invokeAppend(args[0].asObjectValue()); - case "[C" -> invokeAppend( - args[0].asObjectValue().asArrayValue().asCharArrayValue()); - default -> PlaceHolder.instance; - }; - } else if (numberOfArgs == 3) { - return switch (desc[0].getDescriptor()) { - case "[C" -> invokeAppend( - args[0].asObjectValue().asArrayValue().asCharArrayValue(), - args[1].asIntValue(), - args[2].asIntValue()); - case "Ljava/lang/CharSequence;" -> invokeAppend( - args[0].asObjectValue(), args[1].asIntValue(), args[2].asIntValue()); - default -> PlaceHolder.instance; - }; + if (!name.equals("") && !KEEP_CAPACITY.contains(name)) { + capacity = null; } - return PlaceHolder.instance; - } - - private StringBuilderValue invokeAppend(StringValue s) throws NotImplementedException, ValueConversionException { - String desc = "(Ljava.lang.String;)"; - Type[] type = Type.getArgumentTypes(desc); - this.stringValue = - (StringValue) stringValue.invokeMethod("concat", type, new StringValue[] {s}); - return this; - } - - private Value invokeAppend(CharArrayValue str) throws NotImplementedException, ValueConversionException { - int size = str.size.concrete; - for (int i = 0; i < size; i++) { - invokeAppend(str.getElement(new IntValue(str.getContext(), i)).asStringValue()); + if (result instanceof PlaceHolder && MUTATORS.contains(name)) { + unknown = true; } - - return this; - } - - private Value invokeAppend(@SuppressWarnings("unused") ObjectValue obj) { - return PlaceHolder.instance; - } - - private Value invokeAppend(ObjectValue obj, IntValue start, IntValue end) { - try { - StringValue s = obj.asStringValue(); - Type[] desc = new Type[] {Type.INT_TYPE, Type.INT_TYPE}; - Value[] args = new Value[] {start, end}; - StringValue substring = (StringValue) s.invokeMethod("substring", desc, args); - return invokeAppend(substring); - } catch (Exception ignored) { - return PlaceHolder.instance; + return result; + } + + private Value invokeInit(Value[] args, Type[] desc) { + StringValue chars; + capacity = null; + if (args.length == 0) { + chars = new StringValue(context, "", -1); + capacity = new IntValue(context, 16); + } else if (desc[0].getSort() == Type.INT) { + // new StringBuilder(int capacity) + chars = new StringValue(context, "", -1); + capacity = args[0] instanceof IntValue c ? c : null; + } else if (args.length == 1) { + // new StringBuilder(String), new StringBuilder(CharSequence): length + 16 + chars = StringValue.charsOf(args[0]); + if (chars != null) { + capacity = new IntValue(context, chars.concrete.length() + 16, + imgr.add(smgr.length(chars.formula), imgr.makeNumber(16))); + } + } else { + chars = null; } + if (chars == null) return PlaceHolder.instance; + this.stringValue = chars; + this.unknown = false; + return VoidValue.instance; } - private Value invokeAppend(CharArrayValue str, IntValue offset, IntValue len) throws NotImplementedException, ValueConversionException { - for (int i = 0; i < len.concrete; i++) { - invokeAppend( - str.getElement(new IntValue(str.getContext(), i + offset.concrete)) - .asStringValue()); - } - - return this; + private void setChars(String concrete, StringFormula formula) { + this.stringValue = new StringValue(context, concrete, formula, -1); } - /** - * Invocation handling for the String instance method AppendCodePoint(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeAppendCodePoint( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private StringValue concat(StringValue a, StringValue b) { + return new StringValue(context, a.concrete + b.concrete, smgr.concat(a.formula, b.formula), -1); } - /** - * Invocation handling for the String instance method Capacity(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCapacity( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return capacity; + private NumeralFormula.IntegerFormula length() { + return smgr.length(stringValue.formula); } - /** - * Invocation handling for the String instance method CharAt(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCharAt(Value[] args, @SuppressWarnings("unused") Type[] desc) throws NotImplementedException, ValueConversionException { - return new CharValue( - context, - this.stringValue.concrete.charAt(args[0].asIntValue().concrete), - this.smgr.charAt(this.stringValue.formula, args[0].asIntValue().asIntegerFormula())); + /** The chars from begin to end of the content. */ + private StringFormula chars(NumeralFormula.IntegerFormula begin, NumeralFormula.IntegerFormula end) { + return smgr.substring(stringValue.formula, begin, imgr.subtract(end, begin)); } /** - * Invocation handling for the String instance method Chars(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance + * The chars a value of type {@code type} is appended or inserted as (String.valueOf), or null + * if that is not modelled. */ - private Value invokeChars( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private StringValue charsOf(Value value, Type type) throws NotImplementedException, ValueConversionException { + return switch (type.getDescriptor()) { + case "I" -> value.asIntValue().asStringValue(); + case "Z" -> value.asBooleanValue().asStringValue(); + case "C" -> value.asCharValue().asStringValue(); + case "J" -> value.asLongValue().asStringValue(); + case "D" -> value.isSymbolic() ? null + : new StringValue(context, String.valueOf(value.asDoubleValue().concrete), -1); + case "F" -> value.isSymbolic() ? null + : new StringValue(context, String.valueOf(value.asFloatValue().concrete), -1); + case "[C" -> value instanceof CharArrayValue array ? array.asStringValue() : null; + default -> objectChars(value); + }; } - /** - * Invocation handling for the String instance method CodePointAt(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCodePointAt( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + /** String.valueOf(obj) for an Object, CharSequence or String argument, or null if not modelled. */ + private StringValue objectChars(Value obj) throws NotImplementedException, ValueConversionException { + if (obj instanceof ObjectValue o && o.isNullValue()) return new StringValue(context, "null", -1); + StringValue chars = StringValue.charsOf(obj); + if (chars != null) return chars; + if (obj instanceof BoxedValue boxed + && boxed.invokeMethod("toString", new Type[0], new Value[0]) instanceof StringValue str) { + return str; + } + return null; } - /** - * Invocation handling for the String instance method CodePointBefore(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCodePointBefore( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private Value invokeAppend(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + StringValue chars; + if (args.length == 1) { + chars = charsOf(args[0], desc[0]); + } else if (args.length == 3 && args[0] instanceof CharArrayValue array) { + // append(char[] str, int offset, int len), by the concrete offset and len (pinned) + int offset = args[1].asIntValue().concrete; + int len = args[2].asIntValue().concrete; + chars = new StringValue(context, "", -1); + for (int i = offset; i < offset + len; i++) { + chars = concat(chars, array.getElement(new IntValue(context, i)).asStringValue()); + } + } else if (args.length == 3 && desc[0].getDescriptor().equals("Ljava/lang/CharSequence;")) { + // append(CharSequence s, int start, int end); s == null appends a part of "null" + StringValue s = objectChars(args[0]); + if (s == null) return PlaceHolder.instance; + IntValue start = args[1].asIntValue(); + IntValue end = args[2].asIntValue(); + chars = new StringValue(context, s.concrete.substring(start.concrete, end.concrete), + smgr.substring(s.formula, start.asIntegerFormula(), + imgr.subtract(end.asIntegerFormula(), start.asIntegerFormula())), -1); + } else { + chars = null; + } + if (chars == null) return PlaceHolder.instance; + setChars(stringValue.concrete + chars.concrete, smgr.concat(stringValue.formula, chars.formula)); + return this; } - /** - * Invocation handling for the String instance method CodePointCount(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCodePointCount( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private Value invokeAppendCodePoint(Value[] args) throws NotImplementedException, ValueConversionException { + // A valid code point (else it throws, which StringCallBranches checks) + IntValue codePoint = args[0].asIntValue(); + String chars = new String(Character.toChars(codePoint.concrete)); + setChars(stringValue.concrete + chars, smgr.concat(stringValue.formula, stringValue.codePointString(codePoint))); + return this; } - /** - * Invocation handling for the String instance method CodePoints(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCodePoints( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private Value invokeCharAt(Value[] args) throws NotImplementedException, ValueConversionException { + IntValue index = args[0].asIntValue(); + return new CharValue(context, stringValue.concrete.charAt(index.concrete), + smgr.charAt(stringValue.formula, index.asIntegerFormula())); } - /** - * Invocation handling for the String instance method CompareTo(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeCompareTo( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private Value invokeCompareTo(Value[] args) throws NotImplementedException, ValueConversionException { + // As the Strings of both: compareTo(StringBuilder another) compares lexicographically too. + StringValue other = StringValue.charsOf(args[0]); + if (other == null) return PlaceHolder.instance; + return stringValue.invokeMethod("compareTo", new Type[] {Type.getType(String.class)}, new Value[] {other}); } - /** - * Invocation handling for the String instance method Delete(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeDelete(Value[] args, @SuppressWarnings("unused") Type[] desc) { - IntValue start = (IntValue) args[0]; - IntValue end = (IntValue) args[1]; - NumeralFormula.IntegerFormula remainingLength = - this.imgr.subtract(this.smgr.length(this.stringValue.formula), end.asIntegerFormula()); - this.stringValue.formula = - this.smgr.concat( - this.smgr.substring( - this.stringValue.formula, - new IntValue(context, 0).asIntegerFormula(), - start.asIntegerFormula()), - this.smgr.substring( - this.stringValue.formula, end.asIntegerFormula(), remainingLength)); - StringBuilder deleteBuilder = new StringBuilder(this.stringValue.concrete); - this.stringValue.concrete = deleteBuilder.delete(start.concrete, end.concrete).toString(); + private Value invokeDelete(Value[] args) throws NotImplementedException, ValueConversionException { + IntValue start = args[0].asIntValue(); + IntValue end = args[1].asIntValue(); + // An end past the length deletes up to the end; substring gives "" from there. + NumeralFormula.IntegerFormula e = end.asIntegerFormula(); + setChars(new StringBuilder(stringValue.concrete).delete(start.concrete, end.concrete).toString(), + smgr.concat(chars(imgr.makeNumber(0), start.asIntegerFormula()), + smgr.substring(stringValue.formula, e, imgr.subtract(length(), e)))); return this; } - /** - * Invocation handling for the String instance method DeleteCharAt(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeDeleteCharAt( - Value[] args, @SuppressWarnings("unused") Type[] desc) throws NotImplementedException, ValueConversionException { - IntValue endIndex = - new IntValue( - this.context, - args[0].asIntValue().concrete + 1, - this.imgr.add( - args[0].asIntValue().asIntegerFormula(), - new IntValue(this.context, 1).asIntegerFormula())); - return invokeDelete( - new Value[] {args[0], endIndex}, new Type[] {Type.INT_TYPE, Type.INT_TYPE}); - } - - /** - * Invocation handling for the String instance method EnsureCapacity(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeEnsureCapacity( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method GetChars(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeGetChars( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + private Value invokeDeleteCharAt(Value[] args) throws NotImplementedException, ValueConversionException { + IntValue index = args[0].asIntValue(); + IntValue end = new IntValue(context, index.concrete + 1, + imgr.add(index.asIntegerFormula(), imgr.makeNumber(1))); + return invokeDelete(new Value[] {index, end}); } - /** - * Invocation handling for the String instance method IndexOf(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeIndexOf(Value[] args, @SuppressWarnings("unused") Type[] desc) throws NotImplementedException, ValueConversionException { - if (args.length == 1) { - return invokeIndexOf(args[0].asStringValue()); - } else if (args.length == 2) { - return invokeIndexOf(args[0].asStringValue(), args[1].asIntValue()); + private Value invokeGetChars(Value[] args) throws NotImplementedException, ValueConversionException { + // getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin), by the concrete indices (pinned) + if (!(args[2] instanceof CharArrayValue dst)) return PlaceHolder.instance; + int srcBegin = args[0].asIntValue().concrete; + int srcEnd = args[1].asIntValue().concrete; + int dstBegin = args[3].asIntValue().concrete; + for (int i = srcBegin; i < srcEnd; i++) { + dst.storeElement(new IntValue(context, dstBegin + i - srcBegin), + (CharValue) invokeCharAt(new Value[] {new IntValue(context, i)})); } - return PlaceHolder.instance; - } - - private Value invokeIndexOf(StringValue str) { - return new IntValue( - this.context, - this.stringValue.concrete.indexOf(str.concrete), - this.smgr.indexOf( - this.stringValue.formula, - str.formula, - new IntValue(this.context, 0).asIntegerFormula())); - } - - private Value invokeIndexOf(StringValue str, IntValue fromIndex) { - return new IntValue( - this.context, - this.stringValue.concrete.indexOf(str.concrete), - this.smgr.indexOf(this.stringValue.formula, str.formula, fromIndex.asIntegerFormula())); + return VoidValue.instance; } - /** - * Invocation handling for the String instance method Insert(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ private Value invokeInsert(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + IntValue offset = args[0].asIntValue(); + StringValue chars; if (args.length == 2) { - return switch (desc[1].getDescriptor()) { - case "I" -> invokeInsert( - args[0].asIntValue(), args[1].asIntValue().asStringValue()); - case "Z" -> invokeInsert( - args[0].asIntValue(), args[1].asBooleanValue().asStringValue()); - case "C" -> invokeInsert( - args[0].asIntValue(), args[1].asCharValue().asStringValue()); - case "D" -> invokeInsert( - args[0].asIntValue(), args[1].asDoubleValue().asStringValue()); - case "F" -> invokeInsert( - args[0].asIntValue(), args[1].asFloatValue().asStringValue()); - case "J" -> invokeInsert( - args[0].asIntValue(), args[1].asLongValue().asStringValue()); - case "Ljava/lang/String;" -> invokeInsert( - args[0].asIntValue(), args[1].asStringValue()); - case "Ljava/lang/CharSequence;", "Ljava/lang/Object;" -> invokeInsert( - args[0].asIntValue(), args[1].asObjectValue()); - case "[C" -> invokeInsert( - args[0].asIntValue(), - args[1].asObjectValue().asArrayValue().asCharArrayValue()); - default -> PlaceHolder.instance; - }; - } else if (args.length == 4) { - return switch (desc[1].getDescriptor()) { - case "Ljava/lang/CharSequence;" -> invokeInsert( - args[0].asIntValue(), - args[1].asObjectValue(), - args[2].asIntValue(), - args[3].asIntValue()); - case "[C" -> invokeInsert( - args[0].asIntValue(), - args[1].asObjectValue().asArrayValue().asCharArrayValue(), - args[2].asIntValue(), - args[3].asIntValue()); - default -> PlaceHolder.instance; - }; + chars = charsOf(args[1], desc[1]); + } else if (args.length == 4 && args[1] instanceof CharArrayValue array) { + // insert(int index, char[] str, int offset, int len), by the concrete offset and len (pinned) + int from = args[2].asIntValue().concrete; + int len = args[3].asIntValue().concrete; + chars = new StringValue(context, "", -1); + for (int i = from; i < from + len; i++) { + chars = concat(chars, array.getElement(new IntValue(context, i)).asStringValue()); + } + } else if (args.length == 4 && desc[1].getDescriptor().equals("Ljava/lang/CharSequence;")) { + // insert(int dstOffset, CharSequence s, int start, int end) + StringValue s = objectChars(args[1]); + if (s == null) return PlaceHolder.instance; + IntValue start = args[2].asIntValue(); + IntValue end = args[3].asIntValue(); + chars = new StringValue(context, s.concrete.substring(start.concrete, end.concrete), + smgr.substring(s.formula, start.asIntegerFormula(), + imgr.subtract(end.asIntegerFormula(), start.asIntegerFormula())), -1); + } else { + chars = null; } - return PlaceHolder.instance; - } - - private Value invokeInsert(IntValue offset, StringValue str) { - this.stringValue.formula = - this.smgr.concat( - smgr.substring( - this.stringValue.formula, - new IntValue(this.context, 0).asIntegerFormula(), - offset.asIntegerFormula()), - str.formula, - smgr.substring( - this.stringValue.formula, - offset.asIntegerFormula(), - smgr.length(stringValue.formula))); - this.stringValue.concrete = - this.stringValue - .concrete - .substring(0, offset.concrete) - .concat(String.valueOf(str.concrete)) - .concat(this.stringValue.concrete.substring(offset.concrete)); + if (chars == null) return PlaceHolder.instance; + NumeralFormula.IntegerFormula off = offset.asIntegerFormula(); + String c = stringValue.concrete; + setChars(c.substring(0, offset.concrete) + chars.concrete + c.substring(offset.concrete), + smgr.concat(chars(imgr.makeNumber(0), off), chars.formula, chars(off, length()))); return this; } - private Value invokeInsert( - @SuppressWarnings("unused") IntValue offset, - @SuppressWarnings("unused") ObjectValue obj) { - return PlaceHolder.instance; - } - - private Value invokeInsert(IntValue offset, CharArrayValue str) throws NotImplementedException, ValueConversionException { - int size = str.size.concrete; - StringValue newStr = new StringValue(this.context, "", -1); - for (int i = 0; i < size; i++) { - newStr.invokeMethod( - "concat", - new Type[] {Type.getType("Ljava/lang/String;")}, - new Value[] { - str.getElement(new IntValue(str.getContext(), i)).asStringValue() - }); - } - invokeInsert(offset, newStr); + private Value invokeReplace(Value[] args) throws NotImplementedException, ValueConversionException { + // replace(int start, int end, String str); an end past the length replaces up to the end + if (!(args[2] instanceof StringValue str)) return PlaceHolder.instance; + IntValue start = args[0].asIntValue(); + IntValue end = args[1].asIntValue(); + NumeralFormula.IntegerFormula e = end.asIntegerFormula(); + setChars(new StringBuilder(stringValue.concrete).replace(start.concrete, end.concrete, str.concrete).toString(), + smgr.concat(chars(imgr.makeNumber(0), start.asIntegerFormula()), str.formula, + smgr.substring(stringValue.formula, e, imgr.subtract(length(), e)))); return this; } - private Value invokeInsert( - IntValue index, CharArrayValue str, IntValue offset, IntValue len) throws NotImplementedException, ValueConversionException { - StringValue newStr = new StringValue(this.context, "", -1); - for (int i = 0; i < len.concrete; i++) { - newStr.invokeMethod( - "concat", - new Type[] {Type.getType("Ljava/lang/String;")}, - new Value[] { - str.getElement(new IntValue(str.getContext(), i + offset.concrete)) - .asStringValue() - }); - } - invokeInsert(index, newStr); + private Value invokeReverse() { + // Only concrete chars: a symbolic string cannot be reversed in the string theory. + if (stringValue.isSymbolic()) return PlaceHolder.instance; + setChars(new StringBuilder(stringValue.concrete).reverse().toString(), + smgr.makeString(new StringBuilder(stringValue.concrete).reverse().toString())); return this; } - private Value invokeInsert( - @SuppressWarnings("unused") IntValue index, - @SuppressWarnings("unused") ObjectValue str, - @SuppressWarnings("unused") IntValue offset, - @SuppressWarnings("unused") IntValue len) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method LastIndexOf(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeLastIndexOf( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method Length(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeLength( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return new IntValue( - this.context, - this.stringValue.concrete.length(), - this.smgr.length(this.stringValue.formula)); - } - - /** - * Invocation handling for the String instance method OffsetByCodePoints(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeOffsetByCodePoints( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method Replace(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeReplace(Value[] args, @SuppressWarnings("unused") Type[] desc) { - IntValue start = (IntValue) args[0]; - IntValue end = (IntValue) args[1]; - StringValue replacement = (StringValue) args[2]; - StringFormula substring = - this.smgr.substring( - this.stringValue.formula, - start.asIntegerFormula(), - this.imgr.subtract(end.asIntegerFormula(), start.asIntegerFormula())); - this.stringValue.formula = - smgr.replace(this.stringValue.formula, substring, replacement.formula); - StringBuilder builderReplace = new StringBuilder(this.stringValue.concrete); - this.stringValue.concrete = - builderReplace - .replace(start.concrete, end.concrete, replacement.concrete) - .toString(); - return this; - } - - /** - * Invocation handling for the String instance method Reverse(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeReverse( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method SetCharAt(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeSetCharAt( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - /* - IntValue index = args[0].asIntValue(); - CharValue newChar = args[1].asCharValue(); - - NumeralFormula.IntegerFormula secondIndex = this.imgr.add(index.formula, new IntValue(this.context, 1).formula); - NumeralFormula.IntegerFormula lengthOfSecondSubstring = - this.imgr.subtract(this.smgr.length(this.stringValue.formula), secondIndex); - this.stringValue.formula = this.smgr.concat( - this.smgr.substring(this.stringValue.formula, new IntValue(this.context, 0).formula, index.formula), - newChar.formula, - this.smgr.substring(this.stringValue.formula, this.imgr.add(index.formula, secondIndex), lengthOfSecondSubstring)); - - StringBuilder builderSetCharAt = new StringBuilder(this.stringValue.concrete); - builderSetCharAt.setCharAt(index.concrete, newChar.concrete); - this.stringValue.concrete = builderSetCharAt.toString(); - } - */ - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method SetLength(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeSetLength(Value[] args, @SuppressWarnings("unused") Type[] desc) - throws NotImplementedException, ValueConversionException { - IntValue newLength = args[0].asIntValue(); - if (newLength.isSymbolic() || newLength.concrete < 0) { - return PlaceHolder.instance; // a symbolic length is not modelled - } - int n = newLength.concrete; - int length = this.stringValue.concrete.length(); - if (n <= length) { - // Truncation, e.g. setLength(0) to reuse the builder - this.stringValue.formula = this.smgr.substring(this.stringValue.formula, - new IntValue(context, 0).asIntegerFormula(), newLength.asIntegerFormula()); - this.stringValue.concrete = this.stringValue.concrete.substring(0, n); - } else { - // Growing pads with null characters - String padding = "\0".repeat(n - length); - this.stringValue.formula = this.smgr.concat(this.stringValue.formula, this.smgr.makeString(padding)); - this.stringValue.concrete = this.stringValue.concrete + padding; - } + private Value invokeSetCharAt(Value[] args) throws NotImplementedException, ValueConversionException { + IntValue index = args[0].asIntValue(); + CharValue ch = args[1].asCharValue(); + NumeralFormula.IntegerFormula i = index.asIntegerFormula(); + StringBuilder sb = new StringBuilder(stringValue.concrete); + sb.setCharAt(index.concrete, ch.concrete); + setChars(sb.toString(), smgr.concat(chars(imgr.makeNumber(0), i), ch.asStringValue().formula, + chars(imgr.add(i, imgr.makeNumber(1)), length()))); return VoidValue.instance; } - /** - * Invocation handling for the String instance method SubSequence(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeSubSequence( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; - } - - /** - * Invocation handling for the String instance method Substring(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeSubstring( - Value[] args, @SuppressWarnings("unused") Type[] desc) throws NotImplementedException, ValueConversionException { - if (args.length == 1) { - return invokeSubstring(args[0].asIntValue()); - } else if (args.length == 2) { - return invokeSubstring(args[0].asIntValue(), args[1].asIntValue()); - } - return PlaceHolder.instance; + private Value invokeSetLength(Value[] args) throws NotImplementedException, ValueConversionException { + // By the concrete length (pinned): the first n chars of the content padded with n '\0's. + int n = args[0].asIntValue().concrete; + StringBuilder sb = new StringBuilder(stringValue.concrete); + sb.setLength(n); + setChars(sb.toString(), smgr.substring(smgr.concat(stringValue.formula, smgr.makeString("\0".repeat(n))), + imgr.makeNumber(0), imgr.makeNumber(n))); + return VoidValue.instance; } - private Value invokeSubstring(IntValue start) { - NumeralFormula.IntegerFormula remainingLength = - this.imgr.subtract(this.smgr.length(this.stringValue.formula), start.asIntegerFormula()); - this.stringValue.formula = - this.smgr.substring(this.stringValue.formula, start.asIntegerFormula(), remainingLength); - this.stringValue.concrete = this.stringValue.concrete.substring(start.concrete); - return new StringValue( - this.context, this.stringValue.concrete, this.stringValue.formula, -1); + private Value invokeSubstring(Value[] args) throws NotImplementedException, ValueConversionException { + // substring(start) is substring(start, length()); subSequence(start, end) is substring(start, end) + if (args.length != 1 && args.length != 2) return PlaceHolder.instance; + IntValue start = args[0].asIntValue(); + IntValue end = args.length == 2 ? args[1].asIntValue() + : new IntValue(context, stringValue.concrete.length(), length()); + return new StringValue(context, stringValue.concrete.substring(start.concrete, end.concrete), + chars(start.asIntegerFormula(), end.asIntegerFormula()), -1); } - private Value invokeSubstring(IntValue start, IntValue end) { - this.stringValue.formula = - this.smgr.substring(this.stringValue.formula, start.asIntegerFormula(), end.asIntegerFormula()); - this.stringValue.concrete = - this.stringValue.concrete.substring(start.concrete, end.concrete); - return new StringValue( - this.context, this.stringValue.concrete, this.stringValue.formula, -1); + @Override + public boolean isSymbolic() { + return stringValue != null && stringValue.isSymbolic(); } - /** - * Invocation handling for the String instance method ToString(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeToString( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return new StringValue( - this.context, this.stringValue.concrete, this.stringValue.formula, -1); + @Override + public boolean isSymbolic(Set> visited) { + return isSymbolic(); } - /** - * Invocation handling for the String instance method TrimToSize(). - * Returns PlaceHolder::instance if the method is not yet implemented, or the Value that - * represents the result of the method including symbolic handling. - * - * @param args List of Values that correspond to the method arguments - * @param desc Array of Type descriptions of the methods' signature. No guarantee is given that - * the Value in args is of the same type. - * @return The resulting Value or PlaceHolder::instance - */ - private Value invokeTrimToSize( - @SuppressWarnings("unused") Value[] args, - @SuppressWarnings("unused") Type[] desc) { - return PlaceHolder.instance; + @Override + public ImmutableSet getSymbolicVariables() { + return stringValue == null ? ImmutableSet.of() : stringValue.getSymbolicVariables(); } @Override - public StringValue asStringValue() { + public StringValue asStringValue() throws NotImplementedException { + if (unknown || stringValue == null) { + throw new NotImplementedException("The chars of this StringBuilder are not known"); + } return this.stringValue; } @@ -896,6 +420,7 @@ public String toString() { return "Ljava/lang/StringBuilder @" + Integer.toHexString(address) + + (unknown ? " (unknown)" : "") + " (" + concreteString + ", " diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java index b273156a..67c2cc41 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java @@ -27,6 +27,14 @@ public class StringValue extends ObjectValue { @Getter private static final String symbolicPrefix = Type.getType(String.class).getInternalName(); + /** + * The UFs the models of compareTo, trim and lastIndexOf introduce. Each is defined exactly by a + * constraint on its arguments that is added to the trace (addDefinition): it has one value for + * any arguments (trim's bounds of an all-blank string excepted, where only lo == hi matters), + * so a constraint over them is as exact as one over the inputs. + */ + public static final java.util.Set EXACT_UFS = java.util.Set.of("commonPrefixLength", "trimStart", "trimEnd", "lastIndexOf"); + static final int REPLACE_COUNT = 10; private StringFormulaManager smgr; private IntegerFormulaManager imgr; @@ -227,13 +235,24 @@ public BooleanFormula getBounds(boolean upper) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeInit(Value[] args, Type[] desc) { - if (args.length == 1 && args[0] instanceof StringValue s) { - this.concrete = s.concrete; - this.formula = s.formula; - } // Mark this string as user-de-interned since it was created via new String() // in user code (as opposed to SWAT's NoCacheMethodAdapter de-interning) this.userDeInterned = true; + StringValue chars; + if (args.length == 0) { + chars = new StringValue(context, "", -1); + } else if (args.length == 1 && args[0] instanceof CharArrayValue array) { + // The concrete number of chars, which the call's branches pin (StringCallBranches). + chars = array.asStringValue(); + } else if (args.length == 1) { + // new String(String), new String(StringBuilder) + chars = charsOf(args[0]); + } else { + chars = null; + } + if (chars == null) return PlaceHolder.instance; + this.concrete = chars.concrete; + this.formula = chars.formula; return VoidValue.instance; } @@ -371,6 +390,24 @@ public BooleanFormula getBounds(boolean upper) { return new IntValue(context, result, cmp); } + /** Records that a model is not exact for this call, so an exhausted search proves nothing. */ + static void recordPrecisionLoss() { + try { + ThreadHandler.getSymbolicTraceHandler(currentThread().getId()).recordSymbolicPrecisionLoss(); + } catch (Exception e) { + throw new IllegalStateException("No symbolic trace handler for the current thread", e); + } + } + + /** + * The chars of a CharSequence SWAT tracks: a String or a StringBuilder's content, else null. + */ + public static StringValue charsOf(Value sequence) { + if (sequence instanceof StringValue str) return str; + if (sequence instanceof de.uzl.its.swat.symbolic.value.reference.StringBuilderValue sb) return sb.getContent(); + return null; + } + /** Adds a constraint that defines the UFs a model introduced; it holds on every path and is never negated. */ private static void addDefinition(BooleanFormula definition) { try { @@ -428,7 +465,8 @@ private static void addDefinition(BooleanFormula definition) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeContains(Value[] args, Type[] desc) { - if (args.length == 1 && args[0] instanceof StringValue s) { + StringValue s = args.length == 1 ? charsOf(args[0]) : null; + if (s != null) { boolean result = concrete.contains(s.concrete); return new BooleanValue(context, result, smgr.contains(formula, s.formula)); } else { @@ -448,7 +486,9 @@ private static void addDefinition(BooleanFormula definition) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeContentEquals(Value[] args, Type[] desc) { - return PlaceHolder.instance; + StringValue other = args.length == 1 ? charsOf(args[0]) : null; + if (other == null) return PlaceHolder.instance; + return new BooleanValue(context, concrete.contentEquals(other.concrete), smgr.equal(formula, other.formula)); } /** @@ -500,15 +540,14 @@ private static void addDefinition(BooleanFormula definition) { */ private Value invokeEquals(Value[] args, Type[] desc) { if (args.length == 1) { - Value anObject = args[0]; - try { - StringValue str = anObject.asStringValue(); + // Only a String is equal to a String (not, e.g., a StringBuilder with the same chars). + if (args[0] instanceof StringValue str) { boolean result = concrete.equals(str.concrete); return new BooleanValue(context, result, smgr.equal(formula, str.formula)); - } catch (Exception ignored) { - System.out.println("No String indeed!"); - return PlaceHolder.instance; + } else if (args[0] instanceof ObjectValue obj && obj.getAddress() == ObjectValue.ADDRESS_NULL) { + return new BooleanValue(context, false); } + return PlaceHolder.instance; } else { return PlaceHolder.instance; } @@ -607,11 +646,12 @@ private static void addDefinition(BooleanFormula definition) { IntValue srcEnd = args[1].asIntValue(); CharArrayValue dst = args[2].asObjectValue().asArrayValue().asCharArrayValue(); IntValue dstBegin = args[3].asIntValue(); + // By the concrete indices, which the call's branches pin (StringCallBranches). for (int idx = srcBegin.concrete; idx < srcEnd.concrete; idx++) { Value[] charAtArgs = new Value[] { new IntValue(context, idx) }; Type[] charAtDesc = new Type[] { Type.INT_TYPE }; dst.storeElement( - new IntValue(context, dstBegin.concrete + idx), + new IntValue(context, dstBegin.concrete + idx - srcBegin.concrete), (CharValue) invokeCharAt(charAtArgs, charAtDesc)); } return VoidValue.instance; @@ -708,7 +748,43 @@ private static void addDefinition(BooleanFormula definition) { } private Value invokeIndexOf(IntValue ch, IntValue fromIndex) { - return invokeIndexOf(ch.asStringValue(), fromIndex); + int result = concrete.indexOf(ch.concrete, fromIndex.concrete); + if (!isSymbolic() && !ch.isSymbolic() && !fromIndex.isSymbolic()) return new IntValue(context, result); + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + IntValue index = (IntValue) invokeIndexOf(new StringValue(context, "", codePointString(ch), -1), fromIndex); + // No code point, no match (as Java, which searches for a code point, not for its digits). + return new IntValue(context, result, bmgr.ifThenElse(isCodePoint(ch), index.asIntegerFormula(), imgr.makeNumber(-1))); + } + + /** Whether ch is a code point, i.e. in [0, 0x10FFFF]: the chars indexOf(int)/lastIndexOf(int) can find. */ + private BooleanFormula isCodePoint(IntValue ch) { + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + if (!ch.isSymbolic()) return bmgr.makeBoolean(Character.isValidCodePoint(ch.concrete)); + NumeralFormula.IntegerFormula c = ch.asIntegerFormula(); + return bmgr.and(imgr.greaterOrEquals(c, imgr.makeNumber(0)), + imgr.lessOrEquals(c, imgr.makeNumber(Character.MAX_CODE_POINT))); + } + + /** + * The chars of code point ch in a Java string (String.valueOf(Character.toChars(ch))): the char + * itself in the BMP, else its surrogate pair. Meaningful only if {@link #isCodePoint} holds. + */ + public StringFormula codePointString(IntValue ch) { + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + if (!ch.isSymbolic()) { + // Char by char: makeString would take a surrogate pair for one (SMT) character. + if (!Character.isValidCodePoint(ch.concrete)) return smgr.makeString(""); + StringFormula chars = smgr.makeString(""); + for (char c : Character.toChars(ch.concrete)) chars = smgr.concat(chars, smgr.fromCodePoint(imgr.makeNumber(c))); + return chars; + } + NumeralFormula.IntegerFormula c = ch.asIntegerFormula(); + NumeralFormula.IntegerFormula offset = imgr.subtract(c, imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT)); + NumeralFormula.IntegerFormula high = imgr.add(imgr.makeNumber(Character.MIN_HIGH_SURROGATE), imgr.divide(offset, imgr.makeNumber(1024))); + NumeralFormula.IntegerFormula low = imgr.add(imgr.makeNumber(Character.MIN_LOW_SURROGATE), imgr.modulo(offset, imgr.makeNumber(1024))); + return bmgr.ifThenElse(imgr.lessThan(c, imgr.makeNumber(Character.MIN_SUPPLEMENTARY_CODE_POINT)), + smgr.fromCodePoint(c), + smgr.concat(smgr.fromCodePoint(high), smgr.fromCodePoint(low))); } /** @@ -771,14 +847,14 @@ private static void addDefinition(BooleanFormula definition) { if (args.length < 1 || args.length > 2) return PlaceHolder.instance; IntValue from = args.length == 2 ? args[1].asIntValue() : new IntValue(context, Integer.MAX_VALUE); StringValue target; + IntValue ch = null; int result; if (desc[0].getSort() == Type.INT) { - IntValue ch = args[0].asIntValue(); - // Supplementary code points are two chars in a Java string but one in the solver's, so - // only BMP chars are modelled exactly (the UF below flags the result as imprecise anyway). - if (ch.concrete < 0 || ch.concrete > Character.MAX_VALUE) return PlaceHolder.instance; - target = new StringValue(context, String.valueOf((char) (int) ch.concrete), - smgr.fromCodePoint(ch.asIntegerFormula()), -1); + // The chars of the code point; for anything else there is no match. By the concrete + // char, which the call's branches pin (StringCallBranches): with a symbolic one the + // window encoding below is too hard for the solver. + ch = new IntValue(context, args[0].asIntValue().concrete); + target = new StringValue(context, "", codePointString(ch), -1); result = concrete.lastIndexOf(ch.concrete, from.concrete); } else if (args[0] instanceof StringValue str) { target = str; @@ -811,7 +887,7 @@ private static void addDefinition(BooleanFormula definition) { bmgr.and(imgr.greaterOrEquals(r, imgr.makeNumber(0)), imgr.lessOrEquals(r, last), smgr.equal(smgr.substring(formula, r, tlen), target.formula), bmgr.not(smgr.contains(afterR, target.formula)))))); - return new IntValue(context, result, r); + return new IntValue(context, result, ch == null ? r : bmgr.ifThenElse(isCodePoint(ch), r, imgr.makeNumber(-1))); } /** @@ -955,41 +1031,33 @@ private static void addDefinition(BooleanFormula definition) { } private Value invokeReplace(ObjectValue target, ObjectValue replacement) { - if (target instanceof StringValue oldString && replacement instanceof StringValue newString) { - // ToDo (Nils): This is the correct implementation. However replaceAll is currently not - // supported by Z3 - /* - formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula); - */ - - var newConcrete = this.concrete.replace(oldString.concrete, newString.concrete); - var newFormula = this.formula; - for (int i = 0; i < REPLACE_COUNT; i++) { - newFormula = smgr.replace(newFormula, oldString.formula, newString.formula); - } - - return new StringValue(context, newConcrete, newFormula, ObjectValue.ADDRESS_UNKNOWN); - } else { - return PlaceHolder.instance; - } + StringValue oldString = charsOf(target); + StringValue newString = charsOf(replacement); + if (oldString == null || newString == null) return PlaceHolder.instance; + return replaceAll(oldString, newString); } private Value invokeReplace(CharValue oldChar, CharValue newChar) { - StringValue oldString = oldChar.asStringValue(); - StringValue newString = newChar.asStringValue(); - // ToDo (Nils): This is the correct implementation. However replaceAll is currently not - // supported by Z3 - // See: https://git.its.uni-luebeck.de/research-projects/pet-hmr/knife-fuzzer/-/issues/54 - /* - formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula); - */ - - var newConcrete = this.concrete.replace(oldString.concrete, newString.concrete); - var newFormula = this.formula; + return replaceAll(oldChar.asStringValue(), newChar.asStringValue()); + } + + /** + * String.replace: every occurrence of target, left to right. Z3 hardly decides str.replace_all + * (with a concrete target it gave up or hung where this did not), so only the first + * REPLACE_COUNT occurrences are replaced, one by one, which is exact only for strings with as + * many occurrences at most (and str.replace differs from Java for an empty target): precision + * loss. + */ + private StringValue replaceAll(StringValue target, StringValue replacement) { + String newConcrete = this.concrete.replace(target.concrete, replacement.concrete); + if (!isSymbolic() && !target.isSymbolic() && !replacement.isSymbolic()) { + return new StringValue(context, newConcrete, ObjectValue.ADDRESS_UNKNOWN); + } + recordPrecisionLoss(); + StringFormula newFormula = formula; for (int i = 0; i < REPLACE_COUNT; i++) { - newFormula = smgr.replace(newFormula, oldString.formula, newString.formula); + newFormula = smgr.replace(newFormula, target.formula, replacement.formula); } - return new StringValue(context, newConcrete, newFormula, ObjectValue.ADDRESS_UNKNOWN); } @@ -1083,12 +1151,17 @@ private static void addDefinition(BooleanFormula definition) { } private Value invokeStartsWith(StringValue prefix, IntValue toffset) { + // As Java: false unless the prefix fits at toffset, i.e. 0 <= toffset <= length - prefix length. + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + NumeralFormula.IntegerFormula t = toffset.asIntegerFormula(); + NumeralFormula.IntegerFormula plen = smgr.length(prefix.formula); return new BooleanValue( context, - concrete.startsWith(prefix.concrete), - smgr.equal( - prefix.formula, - smgr.substring(formula, toffset.asIntegerFormula(), smgr.length(prefix.formula)))); + concrete.startsWith(prefix.concrete, toffset.concrete), + bmgr.and( + imgr.greaterOrEquals(t, imgr.makeNumber(0)), + imgr.lessOrEquals(t, imgr.subtract(smgr.length(formula), plen)), + smgr.equal(prefix.formula, smgr.substring(formula, t, plen)))); } /** @@ -1162,8 +1235,10 @@ private static void addDefinition(BooleanFormula definition) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeSubSequence(Value[] args, Type[] desc) { - return PlaceHolder.instance; + private Value invokeSubSequence(Value[] args, Type[] desc) + throws NotImplementedException, ValueConversionException { + // subSequence(begin, end) is substring(begin, end) + return args.length == 2 ? invokeSubstring(args, desc) : PlaceHolder.instance; } /** @@ -1219,21 +1294,16 @@ private static void addDefinition(BooleanFormula definition) { private Value invokeToCharArray(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { - if (!concrete.isEmpty()) { - CharArrayValue dst = new CharArrayValue(context, new IntValue(context, concrete.length()), -1); - for (int idx = 0; idx < concrete.length(); idx++) { - Value[] charAtArgs = new Value[] { new IntValue(context, idx) }; - Type[] charAtDesc = new Type[] { Type.INT_TYPE }; - dst.storeElement( - new IntValue(context, idx), - (CharValue) invokeCharAt(charAtArgs, charAtDesc)); - } - return dst; - } else { - new CharArrayValue(context, new IntValue(context, 0), -1); + // As long as the concrete string, which the call's branches pin (StringCallBranches). + CharArrayValue dst = new CharArrayValue(context, new IntValue(context, concrete.length()), -1); + for (int idx = 0; idx < concrete.length(); idx++) { + Value[] charAtArgs = new Value[] { new IntValue(context, idx) }; + Type[] charAtDesc = new Type[] { Type.INT_TYPE }; + dst.storeElement( + new IntValue(context, idx), + (CharValue) invokeCharAt(charAtArgs, charAtDesc)); } - - return PlaceHolder.instance; + return dst; } /** diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StringIndexCheckAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StringIndexCheckAgentSpec.groovy new file mode 100644 index 00000000..c746d25e --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/StringIndexCheckAgentSpec.groovy @@ -0,0 +1,92 @@ +package de.uzl.its.swat.symbolic + +import com.fasterxml.jackson.databind.ObjectMapper +import spock.lang.Shared +import spock.lang.Specification + +import javax.tools.ToolProvider +import java.nio.file.Files +import java.nio.file.Path +import java.util.concurrent.TimeUnit + +/** + * L2 (forked agent): the index check of String.charAt is a branch of the trace, on both sides. A + * tiny SV-COMP style target calls charAt(5) on a nondet string and catches the exception; it is run + * with the agent in {@code solver.mode=PRINT}, once with the default input "fixed" (too short: the + * call throws) and once with a longer one. Runs via the {@code agentTest} Gradle task (needs the + * agent jar from {@code copyJar}). + */ +class StringIndexCheckAgentSpec extends Specification { + + static final Path AGENT_JAR = Path.of("lib", "symbolic-executor.jar").toAbsolutePath() + static final Path NATIVE_LIBS = Path.of("..", "libs", "java-library-path").toAbsolutePath() + static final Path TARGETS = Path.of("src", "test", "resources", "targets").toAbsolutePath() + + @Shared Path classes + @Shared Map shortTrace + @Shared Map longTrace + + def setupSpec() { + assert Files.isRegularFile(AGENT_JAR): "agent jar missing, run copyJar first: ${AGENT_JAR}" + classes = Files.createTempDirectory("swat-string-index-agent-spec") + compile(classes) + shortTrace = parseTrace(run(classes, [])) + longTrace = parseTrace(run(classes, ["-Dswat.input.java/lang/String_0=abcdefgh"])) + } + + def cleanupSpec() { + classes?.toFile()?.deleteDir() + } + + private static List indexChecks(Map trace) { + return trace.trace.findAll { it.callback && it.constraint?.contains("str.len") } + } + + def "a call that throws at the index check records the failed check, not a context loss"() { + expect: + indexChecks(shortTrace).size() == 1 + !indexChecks(shortTrace)[0].branched + !shortTrace.symbolicContextLoss + } + + def "a call that returns records the check as held"() { + expect: + indexChecks(longTrace).size() == 1 + indexChecks(longTrace)[0].branched + !longTrace.symbolicContextLoss + } + + private static void compile(Path outDir) { + def sources = [TARGETS.resolve("svcomp-strings/Main.java"), + TARGETS.resolve("svcomp/org/sosy_lab/sv_benchmarks/Verifier.java")]*.toString() + def args = ["-source", "1.8", "-target", "1.8", "-g", "-d", outDir.toString()] + sources + def err = new ByteArrayOutputStream() + int rc = ToolProvider.getSystemJavaCompiler().run(null, null, err, args as String[]) + assert rc == 0: "javac failed: ${err}" + } + + private static String run(Path classes, List inputs) { + def java = Path.of(System.getProperty("java.home"), "bin", "java").toString() + def cmd = [java, + "-javaagent:${AGENT_JAR}".toString(), + "-Djava.library.path=${NATIVE_LIBS}".toString(), + "-Dconfig.path=/nonexistent/swat.cfg", + "-Dinstrumentation.transformer=SV_COMP", + "-Dsolver.mode=PRINT", + "-DexitOnError=false", + "-DlogShadowStateToConsole=false"] + inputs + + ["-cp", classes.toString(), "-ea", "Main"] + def proc = new ProcessBuilder(cmd).directory(classes.toFile()).redirectErrorStream(true).start() + def out = proc.inputStream.text + assert proc.waitFor(5, TimeUnit.MINUTES): "target did not finish:\n${out}" + return out + } + + /** The TraceDTO is the single pretty-printed JSON object whose braces start at column 0. */ + private static Map parseTrace(String out) { + int start = out.indexOf("\n{\n") + int end = out.indexOf("\n}\n", start) + assert start >= 0 && end > start: "no trace JSON in output:\n${out}" + return new ObjectMapper().readValue(out.substring(start + 1, end + 2), Map) + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy new file mode 100644 index 00000000..94c95b44 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringModelExactnessTest.groovy @@ -0,0 +1,680 @@ +package de.uzl.its.value.reference.lang + +import de.uzl.its.swat.symbolic.invoke.java.lang.StringCallBranches +import de.uzl.its.swat.symbolic.value.PlaceHolder +import de.uzl.its.swat.symbolic.value.Value +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.BooleanValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.CharValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.LongValue +import de.uzl.its.swat.symbolic.value.reference.ObjectValue +import de.uzl.its.swat.symbolic.value.reference.StringBuilderValue +import de.uzl.its.swat.symbolic.value.reference.array.CharArrayValue +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue +import de.uzl.its.swat.thread.ThreadHandler +import org.objectweb.asm.Type +import org.sosy_lab.java_smt.api.* +import spock.lang.Specification +import spock.lang.Unroll + +import static java.lang.Thread.currentThread + +/** + * L0: the String and StringBuilder models are exact. A model is applied to a symbolic string (and + * symbolic ints); then, with the variables fixed to a sample, the solver must not find a result + * other than Java's. A model that is too strict there would make the solver call a feasible path + * infeasible: a false SAFE. + */ +class StringModelExactnessTest extends Specification { + + SolverContext context + ProverEnvironment prover + FormulaManager fmgr + BooleanFormulaManager bmgr + IntegerFormulaManager imgr + StringFormulaManager smgr + BitvectorFormulaManager bvmgr + + static final Type STRING = Type.getType(String) + static final Type CHAR_SEQUENCE = Type.getType(CharSequence) + static final Type OBJECT = Type.getType(Object) + static final Type INT = Type.INT_TYPE + + static final List SAMPLES = ["", "a", "abc", "aXa", "97", "xaxax", "a😀b", " \t pad \n", "aaaaaaaaaaaaaaa"] + + def setup() { + ThreadHandler.init() + if (ThreadHandler.hasThreadContext(currentThread().id)) { + ThreadHandler.removeThreadContext(currentThread().id) + } + ThreadHandler.addThreadContext(currentThread().id, "Test-Thread", -2) + context = ThreadHandler.getSolverContext(currentThread().id) + prover = context.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS) + fmgr = context.formulaManager + bmgr = fmgr.booleanFormulaManager + imgr = fmgr.integerFormulaManager + smgr = fmgr.stringFormulaManager + bvmgr = fmgr.bitvectorFormulaManager + } + + def cleanup() { + prover.close() + context.close() + ThreadHandler.removeThreadContext(currentThread().id) + } + + // ---- helpers ---- + + /** A Java string as the solver sees it: one SMT char per UTF-16 char (makeString would join surrogate pairs). */ + private StringFormula chars(String s) { + StringFormula f = smgr.makeString("") + for (char c : s.toCharArray()) { + f = smgr.concat(f, smgr.fromCodePoint(imgr.makeNumber((int) c))) + } + return f + } + + private StringValue symbolicString(String name, String concrete) { + return new StringValue(context, concrete, smgr.makeVariable(name), -1) + } + + private IntValue symbolicInt(String name, int concrete) { + return new IntValue(context, concrete, bvmgr.makeVariable(32, name)) + } + + private BooleanFormula fixString(StringValue v, String sample) { + return smgr.equal(v.formula, chars(sample)) + } + + private BooleanFormula fixInt(IntValue v, int sample) { + return bvmgr.equal(v.formula, bvmgr.makeBitvector(32, sample)) + } + + private boolean precisionLoss() { + return ThreadHandler.getSymbolicTraceHandler(currentThread().id).symbolicTrace.symbolicPrecisionLoss + } + + /** Whether, under the given fixing constraints (and the definitions of the UFs), `other` is unsatisfiable. */ + private boolean onlyJavasResult(List fixed, BooleanFormula other) { + // A fresh prover per query: after a push, Z3's incremental mode gets stuck on some of them. + context.newProverEnvironment().withCloseable { p -> + ThreadHandler.getSymbolicTraceHandler(currentThread().id).getConstraints().each { p.addConstraint(it) } + fixed.each { p.addConstraint(it) } + p.addConstraint(other) + return p.isUnsat() + } + } + + /** + * Whether, under the given fixing constraints, Java's result is possible: the direction that + * matters for soundness (the converse, that it is the only one, Z3 cannot always show for UFs). + */ + private boolean allowsJava(List fixed, BooleanFormula java) { + return !onlyJavasResult(fixed, java) + } + + private boolean exactInt(List fixed, IntValue result, int java) { + return onlyJavasResult(fixed, bmgr.not(imgr.equal(result.asIntegerFormula(), imgr.makeNumber(java)))) + } + + private boolean exactBoolean(List fixed, BooleanValue result, boolean java) { + return onlyJavasResult(fixed, java ? bmgr.not(result.formula) : result.formula) + } + + private boolean exactString(List fixed, StringFormula result, String java) { + return onlyJavasResult(fixed, bmgr.not(smgr.equal(result, chars(java)))) + } + + private Value call(Value receiver, String name, List desc, List> args) { + return ((ObjectValue) receiver).invokeMethod(name, desc as Type[], args as Value[]) + } + + // ---- String ---- + + @Unroll + def "indexOf(int ch) and indexOf(int ch, int from) search for the char, not its digits: #sample, #ch, #from"() { + given: + def s = symbolicString("s", "fixed") + def c = symbolicInt("ch", 97) + def f = symbolicInt("from", 0) + def fixed = [fixString(s, sample), fixInt(c, ch), fixInt(f, from)] + + when: + def one = (IntValue) call(s, "indexOf", [INT], [c]) + def two = (IntValue) call(s, "indexOf", [INT, INT], [c, f]) + + then: + exactInt(fixed, one, sample.indexOf(ch)) + exactInt(fixed, two, sample.indexOf(ch, from)) + + where: + [sample, ch, from] << [["", "a", "aXa", "97", "a\uD83D\uDE00b"], [(int) 'a', (int) '9', -1, 0x1F600, 0xD83D, 0x110000], + [-3, 0, 2]].combinations() + } + + def "indexOf('a') on a concrete char has the Java result concretely"() { + expect: + ((IntValue) call(new StringValue(context, "xab", -1), "indexOf", [INT], [new IntValue(context, (int) 'a')])).concrete == 1 + ((IntValue) call(new StringValue(context, "x97a", -1), "indexOf", [INT, INT], [new IntValue(context, (int) 'a'), new IntValue(context, 0)])).concrete == 3 + } + + @Unroll + def "lastIndexOf(int ch, int from) is exact, with the char pinned: #sample, #ch, #from"() { + given: + def s = symbolicString("s", "fixed") + def c = symbolicInt("ch", ch) + def f = symbolicInt("from", 0) + def pins = StringCallBranches.of(s, "lastIndexOf", "(II)I", [c, f] as Value[]) + def fixed = [fixString(s, sample), fixInt(f, from)] + pins*.condition() + + when: + def r = (IntValue) call(s, "lastIndexOf", [INT, INT], [c, f]) + + then: + exactInt(fixed, r, sample.lastIndexOf(ch, from)) + + where: + [sample, ch, from] << [["", "a", "aXa", "a\uD83D\uDE00b"], [(int) 'a', -1, 0x1F600, 0x110000], [-1, 0, 2, 100]].combinations() + } + + @Unroll + def "lastIndexOf(String str, int from) is exact: #sample, #target, #from"() { + given: + def s = symbolicString("s", "fixed") + def t = symbolicString("t", "x") + def f = symbolicInt("from", 0) + def fixed = [fixString(s, sample), fixString(t, target), fixInt(f, from)] + + when: + def r = (IntValue) call(s, "lastIndexOf", [STRING, INT], [t, f]) + + then: + exactInt(fixed, r, sample.lastIndexOf(target, from)) + + where: + [sample, target, from] << [["", "aXa", "xaxax"], ["", "a", "xa"], [-1, 0, 3, 100]].combinations() + } + + @Unroll + def "indexOf(String str, int from) is exact: #sample, #target, #from"() { + given: + def s = symbolicString("s", "fixed") + def t = symbolicString("t", "x") + def f = symbolicInt("from", 0) + def fixed = [fixString(s, sample), fixString(t, target), fixInt(f, from)] + + when: + def r = (IntValue) call(s, "indexOf", [STRING, INT], [t, f]) + + then: + exactInt(fixed, r, sample.indexOf(target, from)) + + where: + [sample, target, from] << [["", "aXa", "xaxax"], ["", "a", "xa"], [-1, 0, 3, 100]].combinations() + } + + @Unroll + def "startsWith(String prefix, int toffset) is false for an offset out of range: #sample, #prefix, #offset"() { + given: + def s = symbolicString("s", "fixed") + def p = symbolicString("p", "x") + def o = symbolicInt("o", 0) + def fixed = [fixString(s, sample), fixString(p, prefix), fixInt(o, offset)] + + when: + def r = (BooleanValue) call(s, "startsWith", [STRING, INT], [p, o]) + + then: + exactBoolean(fixed, r, sample.startsWith(prefix, offset)) + + where: + [sample, prefix, offset] << [["", "abc"], ["", "a", "abc"], [-1, 0, 1, 3, 4]].combinations() + } + + def "startsWith(String prefix, int toffset) has the concrete result of the offset"() { + expect: + ((BooleanValue) call(new StringValue(context, "tested", -1), "startsWith", [STRING, INT], + [new StringValue(context, "ste", -1), new IntValue(context, 2)])).concrete + } + + @Unroll + def "replace is exact up to ten occurrences, and precision loss: #sample, #target -> #replacement"() { + given: + def s = symbolicString("s", "fixed") + def fixed = [fixString(s, sample)] + + when: + def r = (StringValue) call(s, "replace", [CHAR_SEQUENCE, CHAR_SEQUENCE], + [new StringValue(context, target, -1), new StringValue(context, replacement, -1)]) + + then: + precisionLoss() + exactString(fixed, r.formula, sample.replace(target, replacement)) + + where: + [sample, target, replacement] << [["", "aaaaaaaaa", "xaxax"], ["a", "aa", "xa"], ["", "b"]].combinations() + } + + def "replace(char, char) of more than ten occurrences is not exact, and precision loss"() { + given: + def s = symbolicString("s", "fixed") + def sample = "a" * 25 + + when: + def r = (StringValue) call(s, "replace", [Type.CHAR_TYPE, Type.CHAR_TYPE], + [new CharValue(context, 'a' as char), new CharValue(context, 'c' as char)]) + + then: + precisionLoss() + !exactString([fixString(s, sample)], r.formula, sample.replace('a' as char, 'c' as char)) + } + + def "replace on concrete strings is concrete"() { + when: + def r = (StringValue) call(new StringValue(context, "abab", -1), "replace", [Type.CHAR_TYPE, Type.CHAR_TYPE], + [new CharValue(context, 'a' as char), new CharValue(context, 'c' as char)]) + + then: + r.concrete == "cbcb" + !precisionLoss() + } + + def "replace with an empty or a symbolic target is not modelled exactly"() { + when: + call(symbolicString("s", "ab"), "replace", [CHAR_SEQUENCE, CHAR_SEQUENCE], + [new StringValue(context, "", -1), new StringValue(context, "-", -1)]) + + then: + precisionLoss() + } + + @Unroll + def "trim() is exact: '#sample'"() { + given: + def s = symbolicString("s", "fixed") + + when: + def r = (StringValue) call(s, "trim", [], []) + + then: + exactString([fixString(s, sample)], r.formula, sample.trim()) + + where: + sample << SAMPLES + [" ", "\u0000a\u0000", " a b "] + } + + @Unroll + def "compareTo(String) allows the Java result: #a vs #b"() { + given: + def s = symbolicString("s", "fixed") + def t = symbolicString("t", "fixed") + + when: + def r = (IntValue) call(s, "compareTo", [STRING], [t]) + + then: + allowsJava([fixString(s, a), fixString(t, b)], imgr.equal(r.asIntegerFormula(), imgr.makeNumber(a.compareTo(b)))) + // (That it is the only one, Z3 does not show within reasonable time for some samples.) + + where: + // (Some samples, e.g. "B" vs "abd", take Z3 minutes even to satisfy.) + [a, b] << [["", "a", "ab"], ["", "a", "abd"]].combinations() + } + + @Unroll + def "regionMatches(int, String, int, int) is exact: #toffset #ooffset #len"() { + given: + def s = symbolicString("s", "fixed") + def o = symbolicString("o", "fixed") + def t = symbolicInt("t", 0) + def oo = symbolicInt("oo", 0) + def l = symbolicInt("l", 0) + def fixed = [fixString(s, "abcab"), fixString(o, "xab"), fixInt(t, toffset), fixInt(oo, ooffset), fixInt(l, len)] + + when: + def r = (BooleanValue) call(s, "regionMatches", [INT, STRING, INT, INT], [t, o, oo, l]) + + then: + exactBoolean(fixed, r, "abcab".regionMatches(toffset, "xab", ooffset, len)) + + where: + [toffset, ooffset, len] << [[-1, 0, 3], [-1, 1, 2], [-1, 0, 2]].combinations() + } + + def "equals(StringBuilder) and equals(null) are false"() { + given: + def s = new StringValue(context, "ab", -1) + def sb = new StringBuilderValue(context, new StringValue(context, "ab", -1), -1) + + expect: + call(s, "equals", [OBJECT], [sb]) == PlaceHolder.instance + !((BooleanValue) call(s, "equals", [OBJECT], [new ObjectValue(context, ObjectValue.ADDRESS_NULL)])).concrete + } + + def "contentEquals(StringBuilder) compares the chars"() { + given: + def s = symbolicString("s", "ab") + def sb = new StringBuilderValue(context, new StringValue(context, "ab", -1), -1) + + when: + def r = (BooleanValue) call(s, "contentEquals", [CHAR_SEQUENCE], [sb]) + + then: + r.concrete + exactBoolean([fixString(s, "ab")], r, true) + exactBoolean([fixString(s, "abc")], r, false) + } + + def "getChars copies to the destination offset"() { + given: + def s = new StringValue(context, "abcdef", -1) + def dst = new CharArrayValue(context, new IntValue(context, 4), -1) + + when: + call(s, "getChars", [INT, INT, Type.getType(char[]), INT], + [new IntValue(context, 2), new IntValue(context, 4), dst, new IntValue(context, 1)]) + + then: + (0..3).collect { dst.getElement(new IntValue(context, it)).concrete } == ['\u0000', 'c', 'd', '\u0000'].collect { it as char } + } + + def "toCharArray of the empty string is an empty array"() { + expect: + ((CharArrayValue) call(new StringValue(context, "", -1), "toCharArray", [], [])).size.concrete == 0 + } + + def "new String(char[]) takes the chars of the array"() { + given: + def s = new StringValue(context, "", -1) + def array = new CharArrayValue(context, "hi".toCharArray(), -1) + + when: + call(s, "", [Type.getType(char[])], [array]) + + then: + s.concrete == "hi" + exactString([], s.formula, "hi") + } + + @Unroll + def "long #v and short #v as a String keep their sign"() { + given: + def l = new LongValue(context, (long) v, bvmgr.makeVariable(64, "l")) + + when: + def r = l.asStringValue() + + then: + exactString([bvmgr.equal(l.formula, bvmgr.makeBitvector(64, (long) v))], r.formula, String.valueOf((long) v)) + + where: + v << [0L, 7L, -7L, Long.MIN_VALUE, Long.MAX_VALUE] + } + + // ---- StringBuilder ---- + + private StringBuilderValue builder(StringValue chars) { + return new StringBuilderValue(context, chars, -1) + } + + @Unroll + def "setLength(#n) truncates or pads a symbolic builder: '#sample'"() { + given: + def s = symbolicString("s", "fixed") + def sb = builder(s) + + when: + call(sb, "setLength", [INT], [new IntValue(context, n)]) + + then: + def java = new StringBuilder(sample) + java.setLength(n) + exactString([fixString(s, sample)], sb.content.formula, java.toString()) + + where: + [sample, n] << [["", "ab", "abcdef"], [0, 1, 3, 5]].combinations() + } + + def "substring does not change the builder, and substring(start, end) takes end - start chars"() { + given: + def s = symbolicString("s", "abcdefgh") + def sb = builder(s) + + when: + def sub = (StringValue) call(sb, "substring", [INT, INT], [new IntValue(context, 2), new IntValue(context, 5)]) + def rest = (StringValue) call(sb, "substring", [INT], [new IntValue(context, 6)]) + + then: + sub.concrete == "cde" + rest.concrete == "gh" + sb.content.concrete == "abcdefgh" + exactString([fixString(s, "abcdefgh")], sub.formula, "cde") + exactString([fixString(s, "abcdefgh")], sb.content.formula, "abcdefgh") + } + + def "a builder made from a String does not change that String"() { + given: + def s = new StringValue(context, "abc", -1) + def sb = builder(s) + + when: + call(sb, "deleteCharAt", [INT], [new IntValue(context, 0)]) + call(sb, "insert", [INT, STRING], [new IntValue(context, 0), new StringValue(context, "x", -1)]) + + then: + s.concrete == "abc" + exactString([], s.formula, "abc") + sb.content.concrete == "xbc" + } + + @Unroll + def "replace(#start, #end, str) replaces that range: '#sample'"() { + given: + def s = symbolicString("s", "fixed") + def sb = builder(s) + + when: + call(sb, "replace", [INT, INT, STRING], [new IntValue(context, start), new IntValue(context, end), new StringValue(context, "XY", -1)]) + + then: + exactString([fixString(s, sample)], sb.content.formula, new StringBuilder(sample).replace(start, end, "XY").toString()) + + where: + [sample, start, end] << [["abab", "abcdef"], [0, 1, 2], [2, 3, 10]].combinations() + } + + @Unroll + def "delete(#start, #end) is exact: '#sample'"() { + given: + def s = symbolicString("s", "fixed") + def sb = builder(s) + + when: + call(sb, "delete", [INT, INT], [new IntValue(context, start), new IntValue(context, end)]) + + then: + exactString([fixString(s, sample)], sb.content.formula, new StringBuilder(sample).delete(start, end).toString()) + + where: + [sample, start, end] << [["abab", "abcdef"], [0, 1, 2], [2, 3, 10]].combinations() + } + + def "indexOf(String, int) of a builder uses the from index"() { + given: + def s = symbolicString("s", "xaxa") + def f = symbolicInt("f", 2) + + when: + def r = (IntValue) call(builder(s), "indexOf", [STRING, INT], [new StringValue(context, "a", -1), f]) + + then: + r.concrete == 3 + exactInt([fixString(s, "xaxa"), fixInt(f, 2)], r, 3) + exactInt([fixString(s, "xaxa"), fixInt(f, -4)], r, 1) + } + + def "setCharAt is modelled"() { + given: + def s = symbolicString("s", "Hello") + def sb = builder(s) + + when: + call(sb, "setCharAt", [INT, Type.CHAR_TYPE], [new IntValue(context, 1), new CharValue(context, 'a' as char)]) + + then: + sb.content.concrete == "Hallo" + exactString([fixString(s, "Hello")], sb.content.formula, "Hallo") + exactString([fixString(s, "xy")], sb.content.formula, "xa") + } + + def "append(Object) appends a String, a builder and null"() { + given: + def sb = builder(new StringValue(context, "a", -1)) + + when: + call(sb, "append", [OBJECT], [new StringValue(context, "b", -1)]) + call(sb, "append", [CHAR_SEQUENCE], [builder(new StringValue(context, "c", -1))]) + call(sb, "append", [OBJECT], [new ObjectValue(context, ObjectValue.ADDRESS_NULL)]) + call(sb, "append", [Type.DOUBLE_TYPE], [new de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue(context, 1.5d)]) + + then: + sb.content.concrete == "abcnull1.5" + !sb.unknown + } + + def "after a change that is not modelled the chars are unknown, until resynced"() { + given: + def sb = builder(symbolicString("s", "ab")) + + when: + call(sb, "reverse", [], []) + + then: + sb.unknown + sb.symbolic + call(sb, "length", [], []) == PlaceHolder.instance + call(sb, "toString", [], []) == PlaceHolder.instance + + when: + sb.resync("ba") + + then: + !sb.unknown + ((StringValue) call(sb, "toString", [], [])).concrete == "ba" + } + + def "the capacity is the constructor's until the builder may grow"() { + given: + def s = symbolicString("s", "abc") + def sb = builder(null) + call(sb, "", [STRING], [s]) + + when: + def capacity = (IntValue) call(sb, "capacity", [], []) + + then: + capacity.concrete == 19 + exactInt([fixString(s, "hello")], capacity, 21) + + when: + call(sb, "append", [STRING], [new StringValue(context, "x", -1)]) + + then: + call(sb, "capacity", [], []) == PlaceHolder.instance + } + + def "a builder with symbolic chars is symbolic"() { + expect: + builder(symbolicString("s", "ab")).symbolic + !builder(new StringValue(context, "ab", -1)).symbolic + } + + // ---- branches of the library calls ---- + + private boolean branchHoldsExactly(List branches, List fixed, boolean javaThrows) { + // The call returns normally iff all of its index checks hold. + BooleanFormula all = bmgr.and(branches*.condition()) + return onlyJavasResult(fixed, javaThrows ? all : bmgr.not(all)) + } + + private static boolean throwsIn(Closure c) { + try { + c() + return false + } catch (IndexOutOfBoundsException ignored) { + return true + } + } + + @Unroll + def "the index checks of String.#name hold iff Java does not throw: '#sample' #a #b"() { + given: + def s = symbolicString("s", "fixed") + def x = symbolicInt("x", a) + def y = symbolicInt("y", b) + def args = desc.startsWith("(II") ? [x, y] : [x] + def fixed = [fixString(s, sample), fixInt(x, a), fixInt(y, b)] + + when: + def branches = StringCallBranches.of(s, name, desc, args as Value[]) + + then: + !branches.isEmpty() + branchHoldsExactly(branches, fixed, throwsIn(java.curry(sample, a, b))) + + where: + [sample, a, b, call] << [["", "abc"], [-1, 0, 3, 4], [-1, 2, 4], + [["charAt", "(I)C", { String str, int i, int j -> str.charAt(i) }], + ["substring", "(I)Ljava/lang/String;", { String str, int i, int j -> str.substring(i) }], + ["substring", "(II)Ljava/lang/String;", { String str, int i, int j -> str.substring(i, j) }]]].combinations() + name = call[0] + desc = call[1] + java = call[2] + } + + @Unroll + def "the index checks of StringBuilder.#name hold iff Java does not throw: '#sample' #a #b"() { + given: + def s = symbolicString("s", "fixed") + def x = symbolicInt("x", a) + def y = symbolicInt("y", b) + def fixed = [fixString(s, sample), fixInt(x, a), fixInt(y, b)] + def args = desc.startsWith("(II") ? [x, y] : desc.startsWith("(IC") ? [x, new CharValue(context, 'z' as char)] + : desc.startsWith("(ILjava/lang/String;") ? [x, new StringValue(context, "q", -1)] : [x] + if (desc.startsWith("(IILjava/lang/String;")) args = [x, y, new StringValue(context, "q", -1)] + + when: + def branches = StringCallBranches.of(builder(s), name, desc, args as Value[]) + + then: + !branches.isEmpty() + branchHoldsExactly(branches, fixed, throwsIn(java.curry(new StringBuilder(sample), a, b))) + + where: + [sample, a, b, call] << [["", "abc"], [-1, 0, 3, 4], [-1, 2, 4], + [["charAt", "(I)C", { StringBuilder str, int i, int j -> str.charAt(i) }], + ["setCharAt", "(IC)V", { StringBuilder str, int i, int j -> str.setCharAt(i, 'z' as char) }], + ["deleteCharAt", "(I)Ljava/lang/StringBuilder;", { StringBuilder str, int i, int j -> str.deleteCharAt(i) }], + ["delete", "(II)Ljava/lang/StringBuilder;", { StringBuilder str, int i, int j -> str.delete(i, j) }], + ["replace", "(IILjava/lang/String;)Ljava/lang/StringBuilder;", { StringBuilder str, int i, int j -> str.replace(i, j, "q") }], + ["insert", "(ILjava/lang/String;)Ljava/lang/StringBuilder;", { StringBuilder str, int i, int j -> str.insert(i, "q") }], + ["substring", "(II)Ljava/lang/String;", { StringBuilder str, int i, int j -> str.substring(i, j) }], + ["setLength", "(I)V", { StringBuilder str, int i, int j -> str.setLength(i) }]]].combinations() + name = call[0] + desc = call[1] + java = call[2] + } + + def "a model that uses a concrete length pins it"() { + given: + def s = symbolicString("s", "abc") + + when: + def branches = StringCallBranches.of(s, "toCharArray", "()[C", [] as Value[]) + + then: + branches.size() == 1 + branches[0].holds() + onlyJavasResult([branches[0].condition()], bmgr.not(imgr.equal(smgr.length(s.formula), imgr.makeNumber(3)))) + } +} diff --git a/symbolic-executor/src/test/resources/targets/svcomp-strings/Main.java b/symbolic-executor/src/test/resources/targets/svcomp-strings/Main.java new file mode 100644 index 00000000..c1d56f9a --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/svcomp-strings/Main.java @@ -0,0 +1,17 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +/** + * SV-COMP style target for the agent test of the index checks of String methods: charAt throws + * for a nondet string shorter than 6 chars, and the exception is caught. + */ +public class Main { + public static void main(String[] args) { + String s = Verifier.nondetString(); + try { + char c = s.charAt(5); + assert c != 'x'; + } catch (StringIndexOutOfBoundsException e) { + // too short + } + } +}