diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BitOps.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BitOps.java index 4562dcd0..1ad13ad0 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BitOps.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/BitOps.java @@ -92,8 +92,13 @@ static BitvectorFormula compare(SolverContext ctx, BitvectorFormula x, Bitvector * The unsigned value of {@code x} in radix 2^shift without leading zeros ("0" for zero), as * Integer/Long.toBinaryString (shift 1), toOctalString (shift 3) and toHexString (shift 4): the * string of all digits (each one str.from_code of its value), from the highest non-zero digit on. + * Radixes up to 8 only have decimal digits and use the str.from_int encoding of {@link + * NumberStrings}, which the solver handles far better. */ static StringFormula toUnsignedPowerOfTwoString(SolverContext ctx, BitvectorFormula x, int width, int shift) { + if (shift <= 3) { + return NumberStrings.unsignedDigits(ctx, x, width, 1 << shift); + } BitvectorFormulaManager bv = ctx.getFormulaManager().getBitvectorFormulaManager(); BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); StringFormulaManager smgr = ctx.getFormulaManager().getStringFormulaManager(); @@ -106,10 +111,8 @@ static StringFormula toUnsignedPowerOfTwoString(SolverContext ctx, BitvectorForm int lo = k * shift; int hi = Math.min(lo + shift, width) - 1; IntegerFormula digit = bv.toIntegerFormula(bv.extract(x, hi, lo), false); - IntegerFormula code = shift < 4 - ? imgr.add(digit, imgr.makeNumber('0')) - : imgr.add(digit, bmgr.ifThenElse(imgr.greaterThan(digit, imgr.makeNumber(9)), - imgr.makeNumber('a' - 10), imgr.makeNumber('0'))); + IntegerFormula code = imgr.add(digit, bmgr.ifThenElse(imgr.greaterThan(digit, imgr.makeNumber(9)), + imgr.makeNumber('a' - 10), imgr.makeNumber('0'))); chars.add(0, smgr.fromCodePoint(code)); if (k > 0) { start = bmgr.ifThenElse(bv.equal(bv.extract(x, hi, lo), c(bv, hi - lo + 1, 0)), diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/IntegerInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/IntegerInvocation.java index ab6e95f1..4b388a22 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/IntegerInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/IntegerInvocation.java @@ -1,5 +1,6 @@ package de.uzl.its.swat.symbolic.invoke.java.lang; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.symbolic.value.PlaceHolder; @@ -16,7 +17,7 @@ public class IntegerInvocation { - public static Value invokeStaticMethod(String name, Value[] args, Type[] desc) throws ValueConversionException, NotImplementedException { + public static Value invokeStaticMethod(String name, Value[] args, Type[] desc) throws ValueConversionException, NotImplementedException, NoThreadContextException { return switch (name) { case "bitCount" -> invokeBitCount(args); case "compare" -> invokeCompare(args); @@ -749,14 +750,16 @@ private static IntValue sum(IntValue a, IntValue b) { * type, likely a missing implementation */ private static Value invokeToString(Value[] args) - throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException { + throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException, NoThreadContextException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof IntValue iv) { - return toString(iv); + if (args.length == 1) { + return args[0] instanceof IntValue iv ? toString(iv) : PlaceHolder.instance; } - // toString with radix not yet supported - return PlaceHolder.instance; + IntValue i = args[0].asIntValue(); + int radix = NumberStrings.selectRadix(args[1].asIntValue()); + return new StringValue(i.context, Integer.toString(i.concrete, radix), + NumberStrings.toString(i.context, i.formula, 32, true, radix), ObjectValue.ADDRESS_UNKNOWN); } /** @@ -840,18 +843,13 @@ private static LongValue toUnsignedLong(IntValue x) { * type, likely a missing implementation */ private static Value invokeToUnsignedString(Value[] args) - throws IndexOutOfBoundsException, ValueConversionException { + throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException, NoThreadContextException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof IntValue i) { - // the decimal digits of the unsigned value; the radix variant is not modelled - SolverContext ctx = i.context; - StringFormulaManager sfm = ctx.getFormulaManager().getStringFormulaManager(); - BitvectorFormulaManager bvmgr = ctx.getFormulaManager().getBitvectorFormulaManager(); - return new StringValue(ctx, Integer.toUnsignedString(i.concrete), - sfm.toStringFormula(bvmgr.toIntegerFormula(i.formula, false)), ObjectValue.ADDRESS_UNKNOWN); - } - return PlaceHolder.instance; + IntValue i = args[0].asIntValue(); + int radix = args.length == 1 ? 10 : NumberStrings.selectRadix(args[1].asIntValue()); + return new StringValue(i.context, Integer.toUnsignedString(i.concrete, radix), + NumberStrings.toString(i.context, i.formula, 32, false, radix), ObjectValue.ADDRESS_UNKNOWN); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/LongInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/LongInvocation.java index bac192bc..b046e8ca 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/LongInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/LongInvocation.java @@ -1,5 +1,6 @@ package de.uzl.its.swat.symbolic.invoke.java.lang; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; @@ -27,7 +28,7 @@ public class LongInvocation { String name, Value[] args, Type[] desc, - SymbolicTraceHandler symbolicTraceHandler) throws ValueConversionException, NotImplementedException { + SymbolicTraceHandler symbolicTraceHandler) throws ValueConversionException, NotImplementedException, NoThreadContextException { return switch (name) { case "bitCount" -> invokeBitCount(args); case "compare" -> invokeCompare(args); @@ -761,14 +762,16 @@ private static LongValue sum(LongValue a, LongValue b) { * type, likely a missing implementation */ private static Value invokeToString(Value[] args) - throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException { + throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException, NoThreadContextException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof LongValue lv) { - return toString(lv); + if (args.length == 1) { + return args[0] instanceof LongValue lv ? toString(lv) : PlaceHolder.instance; } - // toString with radix not yet supported - return PlaceHolder.instance; + LongValue l = args[0].asLongValue(); + int radix = NumberStrings.selectRadix(args[1].asIntValue()); + return new StringValue(l.context, Long.toString(l.concrete, radix), + NumberStrings.toString(l.context, l.formula, 64, true, radix), ObjectValue.ADDRESS_UNKNOWN); } /** @@ -821,18 +824,13 @@ private static StringValue toString(LongValue l) { * type, likely a missing implementation */ private static Value invokeToUnsignedString(Value[] args) - throws IndexOutOfBoundsException, ValueConversionException { + throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException, NoThreadContextException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof LongValue i) { - // the decimal digits of the unsigned value; the radix variant is not modelled - SolverContext ctx = i.context; - StringFormulaManager sfm = ctx.getFormulaManager().getStringFormulaManager(); - BitvectorFormulaManager bvmgr = ctx.getFormulaManager().getBitvectorFormulaManager(); - return new StringValue(ctx, Long.toUnsignedString(i.concrete), - sfm.toStringFormula(bvmgr.toIntegerFormula(i.formula, false)), ObjectValue.ADDRESS_UNKNOWN); - } - return PlaceHolder.instance; + LongValue l = args[0].asLongValue(); + int radix = args.length == 1 ? 10 : NumberStrings.selectRadix(args[1].asIntValue()); + return new StringValue(l.context, Long.toUnsignedString(l.concrete, radix), + NumberStrings.toString(l.context, l.formula, 64, false, radix), ObjectValue.ADDRESS_UNKNOWN); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStrings.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStrings.java new file mode 100644 index 00000000..940e3d18 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStrings.java @@ -0,0 +1,246 @@ +package de.uzl.its.swat.symbolic.invoke.java.lang; + +import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue; +import de.uzl.its.swat.thread.ThreadHandler; +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.List; +import org.sosy_lab.java_smt.api.BitvectorFormula; +import org.sosy_lab.java_smt.api.BitvectorFormulaManager; +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.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +/** + * Exact encodings of the integral number-to-string conversions: Integer/Long/Short/Byte toString, + * toUnsignedString and their radix variants, and the string conversion of numbers in string + * concatenation. Every method takes a bit-vector of the given width and returns the string the JDK + * produces for it, digit for digit. + * + *

A digit string that only has decimal digits (radix 10 and below) is the str.from_int of the + * integer whose decimal digits it has. Z3 decides str.from_int directly, whereas a concatenation of + * one string per digit, cut to a symbolic length, makes even an equality with a constant time out + * or yield a model that violates the constraint. Only radixes above 10 need per-digit characters. + */ +public final class NumberStrings { + + private NumberStrings() {} + + /** + * The decimal string of {@code x}, read as a signed or an unsigned number of {@code width} bits. + * str.from_int is undefined ("") for negative numbers, so a negative value is "-" followed by + * the digits of its magnitude 2^width - x. + */ + public static StringFormula decimal(SolverContext ctx, BitvectorFormula x, int width, boolean signed) { + FormulaManager fmgr = ctx.getFormulaManager(); + BitvectorFormulaManager bv = fmgr.getBitvectorFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + IntegerFormula unsigned = bv.toIntegerFormula(x, false); + if (!signed) { + return smgr.toStringFormula(unsigned); + } + IntegerFormula magnitude = imgr.subtract(imgr.makeNumber(BigInteger.ONE.shiftLeft(width)), unsigned); + return fmgr.getBooleanFormulaManager().ifThenElse( + bv.lessThan(x, bv.makeBitvector(width, 0), true), + smgr.concat(smgr.makeString("-"), smgr.toStringFormula(magnitude)), + smgr.toStringFormula(unsigned)); + } + + /** + * The string of {@code x} in {@code radix} (2 to 36, see {@link #normaliseRadix}), as + * Integer/Long.toString(x, radix) for a signed and toUnsignedString(x, radix) for an unsigned + * {@code x}: the digits of the magnitude without leading zeros ("0" for zero), digits above 9 as + * the letters a to z, and "-" in front of a negative value. + */ + public static StringFormula toString(SolverContext ctx, BitvectorFormula x, int width, boolean signed, int radix) { + assert radix >= Character.MIN_RADIX && radix <= Character.MAX_RADIX : "[SWAT] Radix out of range: " + radix; + if (radix == 10) { + return decimal(ctx, x, width, signed); + } + if (!signed) { + return unsignedDigits(ctx, x, width, radix); + } + FormulaManager fmgr = ctx.getFormulaManager(); + BitvectorFormulaManager bv = fmgr.getBitvectorFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + BooleanFormula negative = bv.lessThan(x, bv.makeBitvector(width, 0), true); + // as an unsigned number, -MIN_VALUE is the magnitude of MIN_VALUE + BitvectorFormula magnitude = bmgr.ifThenElse(negative, bv.negate(x), x); + StringFormula digits = unsignedDigits(ctx, magnitude, width, radix); + return bmgr.ifThenElse(negative, smgr.concat(smgr.makeString("-"), digits), digits); + } + + /** The radix the JDK uses for {@code radix}: radixes outside 2 to 36 mean 10. */ + public static int normaliseRadix(int radix) { + return radix < Character.MIN_RADIX || radix > Character.MAX_RADIX ? 10 : radix; + } + + /** + * The radix a call with the radix argument {@code radix} converts to, after {@link + * #normaliseRadix}. A symbolic radix is pinned to its concrete value by choice branches: a + * binary search over 2 to 36 on the normalised radix, one branch {@code radix < mid} per step, + * each taken as the concrete radix says. The conversion is then exact on this path with a + * constant radix, and the explorer reaches the other radixes by flipping the branches. (A + * formula that chooses between the radixes itself is exact too, but no solver query on it + * finishes.) + * + * @param radix The radix argument + * @return The normalised concrete radix + */ + public static int selectRadix(IntValue radix) throws NoThreadContextException { + int concrete = normaliseRadix(radix.concrete); + SolverContext ctx = radix.context; + FormulaManager fmgr = ctx.getFormulaManager(); + try { + if (fmgr.extractVariables(fmgr.simplify(radix.formula)).isEmpty()) { + return concrete; + } + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + } + BitvectorFormulaManager bv = fmgr.getBitvectorFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + BitvectorFormula r = radix.formula; + BitvectorFormula normalised = bmgr.ifThenElse( + bmgr.or(bv.lessThan(r, bv.makeBitvector(32, Character.MIN_RADIX), true), + bv.greaterThan(r, bv.makeBitvector(32, Character.MAX_RADIX), true)), + bv.makeBitvector(32, 10), r); + long threadId = Thread.currentThread().getId(); + // the call site of the conversion: its frame is the active one while the model runs + long iid = ThreadHandler.getSymbolicVisitor(threadId).getStack().getActiveFrame().getCallSite(); + int lo = Character.MIN_RADIX; + int hi = Character.MAX_RADIX + 1; + int step = 0; + while (hi - lo > 1) { + int mid = lo + (hi - lo) / 2; + boolean below = concrete < mid; + BooleanFormula constraint = bv.lessThan(normalised, bv.makeBitvector(32, mid), true); + ThreadHandler.getSymbolicTraceHandler(threadId).addChoiceBranch(below, constraint, iid, "#radix" + step++); + if (below) { + hi = mid; + } else { + lo = mid; + } + } + return concrete; + } + + /** + * The digits of the unsigned value of {@code m} in {@code radix} (2 to 36, not 10 for a value + * that str.from_int handles directly), without leading zeros ("0" for zero). + */ + static StringFormula unsignedDigits(SolverContext ctx, BitvectorFormula m, int width, int radix) { + int shift = Integer.numberOfTrailingZeros(radix); + boolean powerOfTwo = Integer.bitCount(radix) == 1; + if (radix == 10) { + return decimal(ctx, m, width, false); + } + if (radix < 10) { + return decimalDigitString(ctx, digits(ctx, m, width, radix)); + } + if (powerOfTwo) { + return BitOps.toUnsignedPowerOfTwoString(ctx, m, width, shift); + } + return letterDigitString(ctx, m, width, radix, digits(ctx, m, width, radix)); + } + + /** The number of digits of the largest unsigned value of {@code width} bits in {@code radix}. */ + private static int digitCount(int width, int radix) { + BigInteger max = BigInteger.ONE.shiftLeft(width).subtract(BigInteger.ONE); + BigInteger r = BigInteger.valueOf(radix); + int n = 1; + for (BigInteger p = r; p.compareTo(max) <= 0; p = p.multiply(r)) { + n++; + } + return n; + } + + /** + * The digits of the unsigned value of {@code m} in {@code radix}, least significant first, each + * a bit-vector of width at most 6 (the number of digits {@link #digitCount}). Power-of-two + * digits are bit fields; the others come from a chain of divisions by the constant radix, which + * repeats no subterm (q_k only appears in q_k+1 and in digit k). + */ + private static List digits(SolverContext ctx, BitvectorFormula m, int width, int radix) { + BitvectorFormulaManager bv = ctx.getFormulaManager().getBitvectorFormulaManager(); + int n = digitCount(width, radix); + List digits = new ArrayList<>(n); + if (Integer.bitCount(radix) == 1) { + int shift = Integer.numberOfTrailingZeros(radix); + for (int k = 0; k < n; k++) { + int lo = k * shift; + digits.add(bv.extract(m, Math.min(lo + shift, width) - 1, lo)); + } + return digits; + } + BitvectorFormula r = bv.makeBitvector(width, radix); + BitvectorFormula q = m; + for (int k = 0; k < n; k++) { + digits.add(bv.extract(bv.remainder(q, r, false), 5, 0)); + if (k < n - 1) { + q = bv.divide(q, r, false); + } + } + return digits; + } + + /** + * The string of decimal digits {@code digits} (least significant first, each below 10) without + * leading zeros: str.from_int of the sum of digit_k * 10^k. + */ + private static StringFormula decimalDigitString(SolverContext ctx, List digits) { + FormulaManager fmgr = ctx.getFormulaManager(); + BitvectorFormulaManager bv = fmgr.getBitvectorFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + List terms = new ArrayList<>(digits.size()); + BigInteger power = BigInteger.ONE; + for (BitvectorFormula digit : digits) { + terms.add(imgr.multiply(bv.toIntegerFormula(digit, false), imgr.makeNumber(power))); + power = power.multiply(BigInteger.TEN); + } + return fmgr.getStringFormulaManager().toStringFormula(imgr.sum(terms)); + } + + /** + * The string of the radix-{@code radix} digits {@code digits} of {@code m} (least significant + * first), digits above 9 as the letters a to z: all digits as characters, from the most + * significant non-zero one on. + */ + private static StringFormula letterDigitString(SolverContext ctx, BitvectorFormula m, int width, int radix, + List digits) { + FormulaManager fmgr = ctx.getFormulaManager(); + BitvectorFormulaManager bv = fmgr.getBitvectorFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + int n = digits.size(); + List chars = new ArrayList<>(n); + // index (from the left) of the first character of the result + IntegerFormula start = imgr.makeNumber(n - 1); + BigInteger power = BigInteger.ONE; + for (int k = 0; k < n; k++) { + // the character code in 8 bits: digit + '0' or digit - 10 + 'a' + BitvectorFormula digit = bv.extend(digits.get(k), 8 - bv.getLength(digits.get(k)), false); + BitvectorFormula code = bv.add(digit, bmgr.ifThenElse( + bv.greaterThan(digit, bv.makeBitvector(8, 9), false), + bv.makeBitvector(8, 'a' - 10), bv.makeBitvector(8, '0'))); + chars.add(0, smgr.fromCodePoint(bv.toIntegerFormula(code, false))); + if (k > 0) { + // m >= radix^k: digit k is not a leading zero + start = bmgr.ifThenElse( + bv.greaterOrEquals(m, bv.makeBitvector(width, power), false), + imgr.makeNumber(n - 1 - k), start); + } + power = power.multiply(BigInteger.valueOf(radix)); + } + return smgr.substring(smgr.concat(chars), start, imgr.subtract(imgr.makeNumber(n), start)); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java index 08399f79..a91f3a87 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java @@ -21,6 +21,10 @@ final class BranchElement extends Element { // an array SWAT does not track. It keeps the explorer's walk of that graph in step, but has no // symbolic constraint, so the explorer never tries to flip it. private final boolean concreteOnly; + // A branch the executor adds itself to enumerate the values of a symbolic operand (e.g. which + // element of an object array a symbolic index selects). The static pre-analysis graph has no + // such branch, so the explorer flips it but does not walk the graph over it. + @lombok.Setter private boolean choice; // Where the branch is, for the explorer to check and resynchronise its walk of the static // pre-analysis graph (see BranchKeys): the branch's key, or null if its instruction has none, 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..5988153a 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 @@ -143,7 +143,8 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage } } trace.add(new BranchDTO(be.getIid(), constraint, be.isBranched(), be.isConcreteOnly()) - .place(be.getKey(), be.getPops(), be.getPushes(), be.isCallback())); + .place(be.getKey(), be.getPops(), be.getPushes(), be.isCallback()) + .choice(be.isChoice())); } else if (el instanceof SpecialElement se) { trace.add(new BranchDTO(se.getIid(), se.getInst())); } 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..87f66412 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,25 @@ public void checkAndSetBranch(boolean result, BooleanFormula constraint, long ii symbolicTrace.addTraceElement(current); } + /** + * Records a branch the executor adds itself to enumerate the values of a symbolic operand, e.g. + * one step of the search for the element a symbolic array index selects. It is a branch like + * any other for the explorer, which flips it to try the other values, but the static + * pre-analysis graph has no counterpart for it. + * + * @param result Whether {@code constraint} holds on this execution + * @param constraint The condition branched on + * @param iid The iid of the instruction the operand belongs to + * @param suffix Tells the instruction's branches apart in their keys + */ + public void addChoiceBranch(boolean result, BooleanFormula constraint, long iid, String suffix) throws NoThreadContextException { + FormulaManager fmgr = ThreadHandler.getSolverContext(Thread.currentThread().getId()).getFormulaManager(); + BranchElement branch = new BranchElement(result, result ? constraint : fmgr.getBooleanFormulaManager().not(constraint), iid); + branch.setChoice(true); + place(branch, iid, suffix); + 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/trace/dto/BranchDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java index 5a917bb2..6475567c 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java @@ -32,6 +32,16 @@ public class BranchDTO { @com.fasterxml.jackson.annotation.JsonInclude(com.fasterxml.jackson.annotation.JsonInclude.Include.NON_DEFAULT) private boolean callback; + // See BranchElement: a branch the executor adds that the static pre-analysis graph does not have. + @SuppressWarnings("unused") + @com.fasterxml.jackson.annotation.JsonInclude(com.fasterxml.jackson.annotation.JsonInclude.Include.NON_DEFAULT) + private boolean choice; + + public BranchDTO choice(boolean choice) { + this.choice = choice; + return this; + } + public BranchDTO place(String key, int pops, java.util.List pushes, boolean callback) { this.key = key; this.pops = pops; diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java index 0bacd823..e4737b72 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java @@ -1,5 +1,8 @@ package de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import de.uzl.its.swat.thread.ThreadHandler; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BitvectorFormulaManager; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -441,10 +444,22 @@ public LongValue asLongValue() { return D2L(); } - //@Override - //public StringValue asStringValue() { - // return new StringValue(context, String.valueOf(concrete), -1); - //} + /** + * The string of the concrete value, as String.valueOf(double). The shortest decimal string that + * identifies the value has no practical exact encoding, so a symbolic value loses its link to + * the string: context loss. + */ + @Override + public StringValue asStringValue() { + if (isSymbolic()) { + try { + ThreadHandler.getSymbolicTraceHandler(Thread.currentThread().getId()).recordSymbolicContextLoss(); + } catch (NoThreadContextException e) { + throw new IllegalStateException("[SWAT] No thread context for a symbolic double", e); + } + } + return new StringValue(context, String.valueOf(concrete), ObjectValue.ADDRESS_UNKNOWN); + } @Override public DoubleObjectValue asObjectValue(){ diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java index 2f14df0e..992d7bee 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java @@ -1,5 +1,8 @@ package de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import de.uzl.its.swat.thread.ThreadHandler; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BitvectorFormulaManager; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -391,10 +394,22 @@ public DoubleValue asDoubleValue() { return F2D(); } - //@Override - //public StringValue asStringValue() { - // return new StringValue(context, String.valueOf(concrete), -1); - //} + /** + * The string of the concrete value, as String.valueOf(float). The shortest decimal string that + * identifies the value has no practical exact encoding, so a symbolic value loses its link to + * the string: context loss. + */ + @Override + public StringValue asStringValue() { + if (isSymbolic()) { + try { + ThreadHandler.getSymbolicTraceHandler(Thread.currentThread().getId()).recordSymbolicContextLoss(); + } catch (NoThreadContextException e) { + throw new IllegalStateException("[SWAT] No thread context for a symbolic float", e); + } + } + return new StringValue(context, String.valueOf(concrete), ObjectValue.ADDRESS_UNKNOWN); + } @Override public FloatObjectValue asObjectValue(){ 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..369e184f 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 @@ -1,5 +1,6 @@ package de.uzl.its.swat.symbolic.value.primitive.numeric.integral; +import de.uzl.its.swat.symbolic.invoke.java.lang.NumberStrings; import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue; @@ -402,12 +403,11 @@ public DoubleValue asDoubleValue() { @Override public StringValue asStringValue() { - // String theory requires IntegerFormula, so convert BV to Int - NumeralFormula.IntegerFormula intFormula = bvmgr.toIntegerFormula(formula, true); + // str.from_int of a negative number is "", so the sign is handled separately return new StringValue( this.context, String.valueOf(concrete), - context.getFormulaManager().getStringFormulaManager().toStringFormula(intFormula), + NumberStrings.decimal(context, formula, 64, true), -1); } 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..1980d170 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 @@ -1,5 +1,6 @@ package de.uzl.its.swat.symbolic.value.primitive.numeric.integral; +import de.uzl.its.swat.symbolic.invoke.java.lang.NumberStrings; import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue; @@ -219,12 +220,11 @@ public ShortObjectValue asObjectValue() { @Override public StringValue asStringValue() { - // String theory requires IntegerFormula, so convert BV to Int - NumeralFormula.IntegerFormula intFormula = bvmgr.toIntegerFormula(formula, true); + // str.from_int of a negative number is "", so the sign is handled separately return new StringValue( this.context, String.valueOf(concrete), - context.getFormulaManager().getStringFormulaManager().toStringFormula(intFormula), + NumberStrings.decimal(context, formula, 16, true), -1); } diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStringsSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStringsSpec.groovy new file mode 100644 index 00000000..cf3715cc --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/NumberStringsSpec.groovy @@ -0,0 +1,209 @@ +package de.uzl.its.swat.symbolic.invoke.java.lang + +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.floatingpoint.DoubleValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.ByteValue +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.primitive.numeric.integral.ShortValue +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue +import org.sosy_lab.common.ShutdownManager +import org.sosy_lab.common.configuration.Configuration +import org.sosy_lab.common.log.BasicLogManager +import org.sosy_lab.java_smt.SolverContextFactory +import org.sosy_lab.java_smt.api.BitvectorFormulaManager +import org.sosy_lab.java_smt.api.BooleanFormula +import org.sosy_lab.java_smt.api.BooleanFormulaManager +import org.sosy_lab.java_smt.api.FloatingPointFormulaManager +import org.sosy_lab.java_smt.api.FormulaType +import org.sosy_lab.java_smt.api.SolverContext +import org.sosy_lab.java_smt.api.StringFormulaManager +import spock.lang.Shared +import spock.lang.Specification + +/** + * Compares the number-to-string models with the JDK on edge values: every radix from 2 to 36 and + * radixes outside that range (which the JDK treats as 10). The number is a fresh variable fixed to + * the input, the radix a constant (a symbolic radix is pinned to a constant by choice branches, + * which need a running executor). The model must agree with the JDK in its concrete string and in + * every solution of its formula. + */ +class NumberStringsSpec extends Specification { + + @Shared SolverContext ctx + @Shared BitvectorFormulaManager bv + @Shared BooleanFormulaManager bm + @Shared FloatingPointFormulaManager fp + @Shared StringFormulaManager sm + @Shared int varCount = 0 + + static final List INTS = [0, -1, 1, Integer.MIN_VALUE, Integer.MAX_VALUE, Integer.MIN_VALUE + 1, + 9, 10, 35, 36, -36, 255, 256, 1295, 1296, 0x12345678, 0x87654321 as int, -1440] + static final List LONGS = [0L, -1L, 1L, Long.MIN_VALUE, Long.MAX_VALUE, Long.MIN_VALUE + 1, 35L, 36L, + 0xffffffffL, 0x100000000L, Integer.MIN_VALUE as long, 0x123456789abcdef0L, + 0xfedcba9876543210L, 47009447931686273L] + static final List RADIXES = (2..36) + [-1, 0, 1, 37, Integer.MIN_VALUE, Integer.MAX_VALUE] + static final List SHORTS = [0, -1, 1, Short.MIN_VALUE, Short.MAX_VALUE, 10, -10, 0x1234, -0x1234].collect { (short) it } + static final List BYTES = [0, -1, 1, Byte.MIN_VALUE, Byte.MAX_VALUE, 10, -10].collect { (byte) it } + + def setupSpec() { + ctx = SolverContextFactory.createSolverContext( + Configuration.defaultConfiguration(), + BasicLogManager.create(Configuration.defaultConfiguration()), + ShutdownManager.create().getNotifier(), + SolverContextFactory.Solvers.Z3) + bv = ctx.getFormulaManager().getBitvectorFormulaManager() + bm = ctx.getFormulaManager().getBooleanFormulaManager() + fp = ctx.getFormulaManager().getFloatingPointFormulaManager() + sm = ctx.getFormulaManager().getStringFormulaManager() + } + + def cleanupSpec() { + ctx.close() + } + + // A symbolic argument with the given value: a fresh variable, and the constraint fixing it. + List symbolic(Object v) { + String name = "n" + (varCount++) + switch (v) { + case Integer: + def x = bv.makeVariable(32, name) + return [new IntValue(ctx, v as int, x), bv.equal(x, bv.makeBitvector(32, v as long))] + case Long: + def x = bv.makeVariable(64, name) + return [new LongValue(ctx, v as long, x), bv.equal(x, bv.makeBitvector(64, v as long))] + case Short: + def x = bv.makeVariable(16, name) + return [new ShortValue(ctx, v as short, x), bv.equal(x, bv.makeBitvector(16, v as long))] + case Byte: + def x = bv.makeVariable(8, name) + return [new ByteValue(ctx, v as byte, x), bv.equal(x, bv.makeBitvector(8, v as long))] + } + throw new IllegalArgumentException(v.getClass().toString()) + } + + IntValue constant(int radix) { + new IntValue(ctx, radix, bv.makeBitvector(32, radix)) + } + + /** The mismatch of {@code res} with {@code expected}, or null: the concrete string and every solution. */ + String mismatch(Value res, String expected, List fixing) { + if (res == PlaceHolder.instance || !(res instanceof StringValue)) { + return "no model" + } + if (res.concrete != expected) { + return "concrete ${res.concrete} != ${expected}" + } + def prover = ctx.newProverEnvironment() + try { + fixing.each { prover.addConstraint(it) } + prover.addConstraint(bm.not(sm.equal(res.formula, sm.makeString(expected)))) + return prover.isUnsat() ? null : "formula admits a string other than ${expected}" + } finally { + prover.close() + } + } + + /** Runs {@code model(number, radix)} on all numbers and radixes and returns the mismatches. */ + List radixMismatches(List numbers, Closure model, Closure jdk) { + def errors = [] + for (def n : numbers) { + for (int r : RADIXES) { + def sym = symbolic(n) + def err = mismatch(model(sym[0], constant(r)), jdk(n, r), [sym[1]]) + if (err != null) errors << "${n}, radix ${r}: ${err}" + } + } + errors + } + + def "Integer.toString(int, int) agrees with the JDK"() { + expect: + radixMismatches(INTS, { x, r -> IntegerInvocation.invokeStaticMethod("toString", [x, r] as Value[], null) }, + { int x, int r -> Integer.toString(x, r) }) == [] + } + + def "Integer.toUnsignedString(int, int) agrees with the JDK"() { + expect: + radixMismatches(INTS, { x, r -> IntegerInvocation.invokeStaticMethod("toUnsignedString", [x, r] as Value[], null) }, + { int x, int r -> Integer.toUnsignedString(x, r) }) == [] + } + + def "Long.toString(long, int) agrees with the JDK"() { + expect: + radixMismatches(LONGS, { x, r -> LongInvocation.invokeStaticMethod("toString", [x, r] as Value[], null, null) }, + { long x, int r -> Long.toString(x, r) }) == [] + } + + def "Long.toUnsignedString(long, int) agrees with the JDK"() { + expect: + radixMismatches(LONGS, { x, r -> LongInvocation.invokeStaticMethod("toUnsignedString", [x, r] as Value[], null, null) }, + { long x, int r -> Long.toUnsignedString(x, r) }) == [] + } + + def "#type.#name agrees with the JDK"() { + expect: + values.findAll { v -> + def sym = symbolic(v) + mismatch(model(sym[0]), jdk(v), [sym[1]]) != null + } == [] + + where: + type | name | values | model | jdk + "Integer" | "toString" | INTS | { x -> IntegerInvocation.invokeStaticMethod("toString", [x] as Value[], null) } | { int x -> Integer.toString(x) } + "Integer" | "toUnsignedString" | INTS | { x -> IntegerInvocation.invokeStaticMethod("toUnsignedString", [x] as Value[], null) } | { int x -> Integer.toUnsignedString(x) } + "Integer" | "toBinaryString" | INTS | { x -> IntegerInvocation.invokeStaticMethod("toBinaryString", [x] as Value[], null) } | { int x -> Integer.toBinaryString(x) } + "Integer" | "toOctalString" | INTS | { x -> IntegerInvocation.invokeStaticMethod("toOctalString", [x] as Value[], null) } | { int x -> Integer.toOctalString(x) } + "Long" | "toString" | LONGS | { x -> LongInvocation.invokeStaticMethod("toString", [x] as Value[], null, null) } | { long x -> Long.toString(x) } + "Long" | "toUnsignedString" | LONGS | { x -> LongInvocation.invokeStaticMethod("toUnsignedString", [x] as Value[], null, null) }| { long x -> Long.toUnsignedString(x) } + "Long" | "toBinaryString" | LONGS | { x -> LongInvocation.invokeStaticMethod("toBinaryString", [x] as Value[], null, null) } | { long x -> Long.toBinaryString(x) } + "Long" | "toOctalString" | LONGS | { x -> LongInvocation.invokeStaticMethod("toOctalString", [x] as Value[], null, null) } | { long x -> Long.toOctalString(x) } + "Short" | "toString" | SHORTS | { x -> ShortInvocation.invokeStaticMethod("toString", [x] as Value[], null) } | { short x -> Short.toString(x) } + "Byte" | "toString" | BYTES | { x -> ByteInvocation.invokeStaticMethod("toString", [x] as Value[], null, null) } | { byte x -> Byte.toString(x) } + } + + def "the string of a #type in concatenation agrees with String.valueOf"() { + expect: + values.findAll { v -> + def sym = symbolic(v) + mismatch(sym[0].asStringValue(), String.valueOf(v), [sym[1]]) != null + } == [] + + where: + type | values + "int" | INTS + "long" | LONGS + "short" | SHORTS + } + + def "a concrete #type converts to the string of String.valueOf"() { + expect: + values.findAll { v -> + mismatch(value(v).asStringValue(), String.valueOf(v), []) != null + } == [] + + where: + type | values | value + "double" | [0.0d, -0.0d, 1.0d, 33.333d, 1e-109d, Double.MAX_VALUE, Double.NaN, Double.NEGATIVE_INFINITY] | { double d -> new DoubleValue(ctx, d, fp.makeNumber(d, FormulaType.getDoublePrecisionFloatingPointType())) } + "float" | [0.0f, -0.0f, 1.0f, 2.5f, 2.4012912E30f, Float.MIN_VALUE, Float.NaN, Float.POSITIVE_INFINITY] | { float f -> new FloatValue(ctx, f, fp.makeNumber(f, FormulaType.getSinglePrecisionFloatingPointType())) } + } + + def "a radix outside 2 to 36 means 10"() { + expect: + NumberStrings.normaliseRadix(radix) == expected + + where: + radix | expected + Integer.MIN_VALUE | 10 + -1 | 10 + 0 | 10 + 1 | 10 + 2 | 2 + 10 | 10 + 36 | 36 + 37 | 10 + Integer.MAX_VALUE | 10 + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/RadixChoiceAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/RadixChoiceAgentSpec.groovy new file mode 100644 index 00000000..6c4705c7 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/java/lang/RadixChoiceAgentSpec.groovy @@ -0,0 +1,85 @@ +package de.uzl.its.swat.symbolic.invoke.java.lang + +import com.fasterxml.jackson.databind.ObjectMapper +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): a conversion with a symbolic radix branches on the radix (a binary search over + * 2 to 36 after the JDK's fallback to 10), so that the conversion is exact with a constant radix + * and the explorer reaches the other radixes by flipping the branches. Runs via the {@code + * agentTest} Gradle task (needs the agent jar from {@code copyJar}). + */ +class RadixChoiceAgentSpec 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() + + def "radix #radix is searched in #steps.size() steps, as its concrete value says"() { + given: + def classes = Files.createTempDirectory("swat-radix-spec") + compile(classes) + + when: + def trace = parseTrace(run(classes, ["-Dswat.input.I_0=-1295", "-Dswat.input.I_1=" + radix])) + def choices = trace.trace.findAll { it.choice } + + then: "binary search over [2, 37): the branch radix < mid of each step" + choices*.branched == steps + choices*.key.collect { it.substring(it.indexOf('#')) } == (0.. 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/resources/targets/radix/Main.java b/symbolic-executor/src/test/resources/targets/radix/Main.java new file mode 100644 index 00000000..f6dfe50e --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/radix/Main.java @@ -0,0 +1,13 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +/** Integer.toString(int, int) with a symbolic number and a symbolic radix (see RadixChoiceAgentSpec). */ +public class Main { + public static void main(String[] args) { + int x = Verifier.nondetInt(); + int radix = Verifier.nondetInt(); + String s = Integer.toString(x, radix); + if (s.equals("-zz")) { + System.out.println("found"); + } + } +} diff --git a/symbolic-explorer/data/BinaryExecutionTree/Node.py b/symbolic-explorer/data/BinaryExecutionTree/Node.py index 5a1fd91b..b82ef17c 100755 --- a/symbolic-explorer/data/BinaryExecutionTree/Node.py +++ b/symbolic-explorer/data/BinaryExecutionTree/Node.py @@ -62,6 +62,7 @@ def __init__(self, parent: Optional['Node'], trace: list, inputs: List[Input], u self.pops = 0 self.pushes = () self.callback = False # in a callback from library code: no counterpart in the SA graph + self.choice = False # added by the executor to enumerate an operand's values: not in the SA graph # Validate trace argument if trace is None or len(trace) == 0: @@ -92,6 +93,7 @@ def __init__(self, parent: Optional['Node'], trace: list, inputs: List[Input], u self.pops = branch.pops self.pushes = branch.pushes self.callback = branch.callback + self.choice = branch.choice self.constraint[branch.trace_id] = branch.constraint # Determine whether the branch was taken or skipped and assign child if branch.has_branched: diff --git a/symbolic-explorer/data/trace/Branch.py b/symbolic-explorer/data/trace/Branch.py index afc93cc8..227934fe 100755 --- a/symbolic-explorer/data/trace/Branch.py +++ b/symbolic-explorer/data/trace/Branch.py @@ -14,7 +14,7 @@ class Branch: """ def __init__(self, id: int, trace_id: str, has_branched: bool, constraint: str, concrete_only: bool = False, - key: str | None = None, pops: int = 0, pushes: tuple = (), callback: bool = False): + key: str | None = None, pops: int = 0, pushes: tuple = (), callback: bool = False, choice: bool = False): """ Initializes a new instance of the Branch class. @@ -37,6 +37,8 @@ def __init__(self, id: int, trace_id: str, has_branched: bool, constraint: str, self.pushes = pushes # In application code that library code called back, which the SA graph does not have. self.callback = callback + # Added by the executor to enumerate the values of a symbolic operand; not in the SA graph. + self.choice = choice def __str__(self): return f'[(B) - {self.id} - ({"T" if self.has_branched else "F"})]' \ No newline at end of file diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a6c70f11..99325f8e 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -356,12 +356,17 @@ def solve_candidates(self, candidates: list[Node]) -> tuple[Node | None, dict, b the ones that ran out are tried again, until one is SAT or all are decided. A branch that runs out even at MAX_RLIMIT is given up on. + Choice branches (which the executor adds to enumerate the values of a symbolic operand, + e.g. a radix) go after the program's own branches of the same level: a program branch + leads somewhere new on the path it is on, while a choice branch starts over with another + value of the operand. + The limit only serves to let other branches go first. So once a retry pass is left with a single branch, that one is solved without a limit: escalating it step by step would only redo the same work at each step. """ gave_up = False - pending = sorted(candidates, key=lambda b: self.rlimit_level.get(b.gid, 0)) + pending = sorted(candidates, key=lambda b: (self.rlimit_level.get(b.gid, 0), b.choice)) retry = False while pending: limited = [] diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py index 68be5da1..7355e590 100644 --- a/symbolic-explorer/parse/DataTransferObjects.py +++ b/symbolic-explorer/parse/DataTransferObjects.py @@ -19,6 +19,9 @@ class TraceItem(BaseModel): pushes: list[Optional[str]] = [] # Recorded in application code that library code called back: not in the SA graph. callback: bool = False + # A branch the executor adds to enumerate the values of a symbolic operand (e.g. the element a + # symbolic array index selects): flipped like any other, but not in the SA graph. + choice: bool = False class UFItem(BaseModel): definition: str diff --git a/symbolic-explorer/parse/TraceParser.py b/symbolic-explorer/parse/TraceParser.py index 8b005c7d..439c9843 100755 --- a/symbolic-explorer/parse/TraceParser.py +++ b/symbolic-explorer/parse/TraceParser.py @@ -23,7 +23,8 @@ def parse_trace(trace: List[TraceItem], trace_id: str) -> List[Branch | Special] key=branch.key, pops=branch.pops, pushes=tuple(branch.pushes), - callback=branch.callback)) + callback=branch.callback, + choice=branch.choice)) else: _trace.append(Special(id=branch.iid, trace_id=trace_id, diff --git a/symbolic-explorer/strategy/DFS.py b/symbolic-explorer/strategy/DFS.py index b8d52078..ffc490ef 100755 --- a/symbolic-explorer/strategy/DFS.py +++ b/symbolic-explorer/strategy/DFS.py @@ -57,7 +57,9 @@ def dfs(visited: set[Node], tree, node: Node | Leaf | None, solved_branches: set # If clinit_depth > 0, we do not have corresponding SA information, so pretend that there is no SA and DON'T WALK the SA graph. # Likewise for a branch in application code that library code called back: the graph walks # over the library call, so the walk holds its place until the callback returns. - mask_sa_node = clinit_depth > 0 or node.callback + # A choice branch (the executor's search for the element a symbolic index selects) has no + # graph node either: both of its sides continue from the walk's current place. + mask_sa_node = clinit_depth > 0 or node.callback or node.choice # Get information on interesting paths. If sa_node is None, all paths should be considered interesting if sa_node and not mask_sa_node: @@ -81,7 +83,7 @@ def dfs(visited: set[Node], tree, node: Node | Leaf | None, solved_branches: set skip_is_interesting = mask_sa_node or (sa_node is None) or is_interesting(sa_node.get_fallthrough_child(), sa_stack) branch_is_interesting = mask_sa_node or (sa_node is None) or is_interesting(sa_node.get_branched_child(), sa_stack) - logger.info(f"[DFS] @{node.id}/{("CALLBACK" if node.callback else "CLINIT") if mask_sa_node else sa_node and sa_node.id} ({"branched" if node.branched else ""}{"skipped" if node.skipped else ""}): skip_is_interesting={skip_is_interesting}, branch_is_interesting={branch_is_interesting}") + logger.info(f"[DFS] @{node.id}/{("CALLBACK" if node.callback else "CHOICE" if node.choice else "CLINIT") if mask_sa_node else sa_node and sa_node.id} ({"branched" if node.branched else ""}{"skipped" if node.skipped else ""}): skip_is_interesting={skip_is_interesting}, branch_is_interesting={branch_is_interesting}") # Add the node itself, if eligible if (node.skipped is None and skip_is_interesting) or (node.branched is None and branch_is_interesting): diff --git a/symbolic-explorer/tests/test_sa_walk.py b/symbolic-explorer/tests/test_sa_walk.py index d1977625..21c0074f 100644 --- a/symbolic-explorer/tests/test_sa_walk.py +++ b/symbolic-explorer/tests/test_sa_walk.py @@ -95,7 +95,7 @@ def load(self) -> SAGraph: os.unlink(path) -def branch_node(name, skipped=None, branched=None, key=None, pops=0, pushes=(), callback=False): +def branch_node(name, skipped=None, branched=None, key=None, pops=0, pushes=(), callback=False, choice=False): """A tree node for one branch event; `None` children are unexplored sides.""" n = Node.__new__(Node) n.parent = None @@ -109,6 +109,7 @@ def branch_node(name, skipped=None, branched=None, key=None, pops=0, pushes=(), n.pops = pops n.pushes = pushes n.callback = callback + n.choice = choice n.constraint = {} n.skipped = skipped n.branched = branched @@ -543,6 +544,25 @@ def test_callback_branches_are_masked(self): _, desyncs = self.run_dfs(tree, g) self.assertEqual(len(desyncs), 1) + def test_choice_branches_are_masked(self): + g = self.graph() + plain, _ = self.run_dfs(self.tree(), g) + # Before f is called, an access at a symbolic index adds two choice branches the graph does + # not have, one with an unexplored side. Masked, the walk holds its place over them, and + # they are still solver targets. + tree = self.tree() + nf = tree.skipped + ch2 = branch_node('ch2', skipped=None, branched=nf, key='M|1|aaload|0#idx1', choice=True) + ch1 = branch_node('ch1', skipped=ch2, branched=leaf(), key='M|1|aaload|0#idx0', choice=True) + tree.skipped = ch1 + found, desyncs = self.run_dfs(tree, g) + self.assertEqual(desyncs, []) + self.assertEqual(found, plain | {'ch2'}) + for n in (ch1, ch2): + n.choice = False + _, desyncs = self.run_dfs(tree, g) + self.assertEqual(len(desyncs), 1) + def test_open_ordinal_matches_any_on_its_line(self): g = self.graph() g.nodes['bf'].key = 'F|10|if|*' diff --git a/symbolic-explorer/tests/test_solver_rlimit.py b/symbolic-explorer/tests/test_solver_rlimit.py index 288d0e7f..0c0f60aa 100644 --- a/symbolic-explorer/tests/test_solver_rlimit.py +++ b/symbolic-explorer/tests/test_solver_rlimit.py @@ -20,8 +20,8 @@ BASE = 1000 -def branch(gid): - return SimpleNamespace(gid=gid, id=gid) +def branch(gid, choice=False): + return SimpleNamespace(gid=gid, id=gid, choice=choice) class FakeSolver: @@ -52,6 +52,14 @@ def solve(self, d, candidates, solver): with mock.patch.object(svcomp.StrategyService, 'solve_branch', side_effect=solver): return d.solve_candidates(candidates) + def test_choice_branches_come_after_program_branches(self): + # 1 is a choice branch (e.g. another radix), 2 a branch of the program: both SAT, 2 first. + d = self.driver(rlimit=None) + s = FakeSolver({}, {1: SATResult.SAT, 2: SATResult.SAT}) + found, sol, gave_up = self.solve(d, [branch(1, choice=True), branch(2)], s) + self.assertEqual(found.gid, 2) + self.assertEqual(s.calls, [(2, None)]) + def test_cheap_queries_come_before_retries(self): # 1 needs 20x the base limit, 2 is UNSAT, 3 is SAT: 3 is found before 1 is retried. d = self.driver()