From 80ce0f02d2e7453235579cbb97db886b6cca253e Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Mon, 19 Oct 2026 14:44:07 +0000 Subject: [PATCH 1/2] Model parsing numbers from Strings exactly, with NumberFormatException as a branch Integer/Long/Short/Byte parse and valueOf(String), with or without a radix, are exact for strings of any length: a string parses iff it is an optional sign and at least one Character.digit digit (Unicode decimal digits and fullwidth letters included), all but the last K of them zeros, and the value in range. The old models took str.to_int of the whole string, which is wrong for signs and non-ASCII digits. Float/Double parse and valueOf(String): whether the string parses is exact (the Double.valueOf grammar, whitespace, hex, NaN, Infinity). The value is exact for decimals without exponent or whitespace whose digits form an integer below 2^p, with at most 10 (22) fraction digits: one correctly rounded division of exact operands. Other parseable strings give a concrete value and record precision loss. The visitor records these branches for static calls on both sides; a NumberFormatException at the branch is explained by the trace instead of recording context loss. Co-Authored-By: Claude Opus 5.5 --- .../symbolic/SymbolicInstructionVisitor.java | 53 +- .../invoke/java/lang/ByteInvocation.java | 19 +- .../invoke/java/lang/DoubleInvocation.java | 6 +- .../invoke/java/lang/FloatInvocation.java | 6 +- .../invoke/java/lang/IntegerInvocation.java | 24 +- .../invoke/java/lang/LongInvocation.java | 24 +- .../invoke/java/lang/NumberParsing.java | 531 ++++++++++++++++++ .../invoke/java/lang/ShortInvocation.java | 25 +- 8 files changed, 615 insertions(+), 73 deletions(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberParsing.java diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java index bbb2ced5..11d02dcc 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.NumberParsing; 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; @@ -2317,7 +2318,16 @@ public void visitINSTANCEOF(INSTANCEOF inst) throws SymbolicInstructionException * @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); + return recordCallBranches(iid, name, StringCallBranches.of(instance, name, desc, arguments), returned); + } + + /** + * Records the branches of a library call (see {@link #recordStringCallBranches}): on a normal + * return all of them held, a call that threw failed the first one that does not hold. + * + * @return Whether the call threw at one of its branches + */ + private boolean recordCallBranches(long iid, String name, List branches, boolean returned) throws NoThreadContextException { int failed = -1; for (int i = 0; i < branches.size() && failed < 0; i++) { if (!branches.get(i).holds()) failed = i; @@ -2326,7 +2336,7 @@ private boolean recordStringCallBranches(long iid, String name, String desc, Obj // 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(); + FormulaManager fmgr = ThreadHandler.getSolverContext(Thread.currentThread().getId()).getFormulaManager(); for (int i = 0; i <= last; i++) { StringCallBranches.Branch branch = branches.get(i); if (!fmgr.extractVariables(branch.condition()).isEmpty()) { @@ -2469,6 +2479,7 @@ public void visitINVOKESTATIC(INVOKESTATIC inst) throws SymbolicInstructionExcep if (stack.getNextInst() instanceof INVOKEMETHOD_END) { Value[] arguments = stack.fetchArgumentsFromLocals(Type.getArgumentTypes(inst.desc), false); + recordParseCallBranches(inst.iid, inst.owner, inst.name, inst.desc, arguments); Value retVal = InvocationHandler.invoke( symbolicTraceHandler, inst.desc, @@ -2480,7 +2491,7 @@ public void visitINVOKESTATIC(INVOKESTATIC inst) throws SymbolicInstructionExcep null); stack.setReturnValue(retVal); } else if (stack.getNextInst() instanceof INVOKEMETHOD_EXCEPTION) { - recordThrowingCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId, false); + recordThrowingStaticCall(inst.iid, inst.owner, inst.name, inst.desc, inst.invokeId); } if (!inst.owner.equals("de/uzl/its/swat/Main")) { @@ -2492,6 +2503,42 @@ public void visitINVOKESTATIC(INVOKESTATIC inst) throws SymbolicInstructionExcep } } + /** + * Records the branches of a parse call that returned normally (see {@link NumberParsing}): its + * checks, which all held, then those that tell how its value is modelled. + */ + private void recordParseCallBranches(long iid, String owner, String name, String desc, Value[] arguments) throws NoThreadContextException { + List checks = NumberParsing.branches(owner, name, desc, arguments); + if (checks.isEmpty()) return; + recordCallBranches(iid, name, checks, true); + FormulaManager fmgr = ThreadHandler.getSolverContext(Thread.currentThread().getId()).getFormulaManager(); + for (StringCallBranches.Branch branch : NumberParsing.returnBranches(owner, name, desc, arguments)) { + if (!fmgr.extractVariables(branch.condition()).isEmpty()) { + symbolicTraceHandler.checkAndSetLibraryBranch(branch.holds(), branch.condition(), determineIid(iid), "#" + name); + } + } + } + + /** + * As {@link #recordThrowingCall}, unless the call is a parse call that threw a + * NumberFormatException at one of its branches (see {@link NumberParsing#branches}), which the + * trace then explains. + */ + private void recordThrowingStaticCall(long iid, String owner, String name, String desc, long invokeId) throws NoThreadContextException { + boolean explained; + try { + Value[] arguments = stack.fetchArgumentsFromLocals(Type.getArgumentTypes(desc), false); + explained = recordCallBranches(iid, name, NumberParsing.branches(owner, name, desc, arguments), false); + } catch (Exception e) { + explained = false; + } + if (explained) { + recordUnmodelledException(iid); + } else { + recordThrowingCall(iid, owner, name, desc, invokeId, false); + } + } + /** * Invokes a virtual method on an object reference from the symbolic stack * diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/ByteInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/ByteInvocation.java index 537be863..ae57772f 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/ByteInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/ByteInvocation.java @@ -99,6 +99,10 @@ private static IntValue compare(ByteValue x, ByteValue y) { * Invocation handler for Byte.valueOf(byte). */ private static Value invokeValueOf(Value[] args) throws NotImplementedException, ValueConversionException { + if (args[0] instanceof StringValue sv) { + ByteValue b = NumberParsing.parseByte(sv, args); + return new ByteObjectValue(b.context, b, ObjectValue.ADDRESS_UNKNOWN); + } assert args.length == 1 : "Expected 1 argument for valueOf(), got " + args.length; ByteValue b = args[0].asByteValue(); return new ByteObjectValue(b.context, b, ObjectValue.ADDRESS_UNKNOWN); @@ -109,23 +113,12 @@ private static IntValue compare(ByteValue x, ByteValue y) { */ private static Value invokeParseByte(Value[] args) throws NotImplementedException, ValueConversionException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 arguments for parseByte(), got " + args.length; - if (args.length == 1 && args[0] instanceof StringValue sv) { - return parseByte(sv); + if (args[0] instanceof StringValue sv) { + return NumberParsing.parseByte(sv, args); } return PlaceHolder.instance; } - /** - * Symbolic wrapper for Byte.parseByte(String s) - */ - private static ByteValue parseByte(StringValue s) { - SolverContext ctx = s.context; - StringFormulaManager sfm = ctx.getFormulaManager().getStringFormulaManager(); - BitvectorFormulaManager bvmgr = ctx.getFormulaManager().getBitvectorFormulaManager(); - return new ByteValue(ctx, Byte.parseByte(s.concrete), - bvmgr.makeBitvector(8, sfm.toIntegerFormula(s.formula))); - } - /** * Invocation handler for Byte.toString(byte). */ diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/DoubleInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/DoubleInvocation.java index 3960684b..4652c834 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/DoubleInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/DoubleInvocation.java @@ -2,6 +2,7 @@ import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.SWATAssert; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; import de.uzl.its.swat.symbolic.value.PlaceHolder; @@ -30,7 +31,10 @@ public class DoubleInvocation { case "isFinite" -> invokeIsFinite(args); case "isInfinite" -> invokeIsInfinite(args); case "isNaN" -> invokeIsNaN(args); - case "valueOf" -> invokeValueOf(args); + case "parseDouble" -> args[0] instanceof StringValue sv ? NumberParsing.parseDouble(sv, symbolicTraceHandler) : PlaceHolder.instance; + case "valueOf" -> args[0] instanceof StringValue sv + ? new DoubleObjectValue(sv.context, NumberParsing.parseDouble(sv, symbolicTraceHandler), ObjectValue.ADDRESS_UNKNOWN) + : invokeValueOf(args); default -> PlaceHolder.instance; }; diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/FloatInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/FloatInvocation.java index 28c72d6b..b642a7e9 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/FloatInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/FloatInvocation.java @@ -13,6 +13,7 @@ import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.SWATAssert; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; import de.uzl.its.swat.symbolic.value.PlaceHolder; @@ -39,7 +40,10 @@ public class FloatInvocation { case "max" -> invokeMax(args); case "min" -> invokeMin(args); case "sum" -> invokeSum(args); - case "valueOf" -> invokeValueOf(args); + case "parseFloat" -> args[0] instanceof StringValue sv ? NumberParsing.parseFloat(sv, symbolicTraceHandler) : PlaceHolder.instance; + case "valueOf" -> args[0] instanceof StringValue sv + ? new FloatObjectValue(sv.context, NumberParsing.parseFloat(sv, symbolicTraceHandler), ObjectValue.ADDRESS_UNKNOWN) + : invokeValueOf(args); default -> PlaceHolder.instance; }; 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 e18f0273..de20f2fd 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 @@ -440,27 +440,12 @@ private static IntValue min(IntValue a, IntValue b) { throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof StringValue sv) { - return parseInt(sv); + if (args[0] instanceof StringValue sv) { + return NumberParsing.parseInt(sv, args); } - // parseInt with radix not yet supported return PlaceHolder.instance; } - /** - * Symbolic wrapper for Integer.parseInt(String s) - * Parses the string argument as a signed decimal integer. - * - * @param s The String containing the integer representation to be parsed - * @return The integer value represented by the argument - * @see Integer.parseInt(String) - */ - private static IntValue parseInt(StringValue s) { - SolverContext ctx = s.context; - StringFormulaManager sfm = ctx.getFormulaManager().getStringFormulaManager(); - return new IntValue(ctx, Integer.parseInt(s.concrete), sfm.toIntegerFormula(s.formula)); - } - /** * Invocation handler for Integer.parseUnsignedInt(*), handles argument conversion. * @@ -846,12 +831,15 @@ private static LongValue toUnsignedLong(IntValue x) { * type, likely a missing implementation */ private static Value invokeValueOf(Value[] args) - throws IndexOutOfBoundsException, ValueConversionException { + throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; if (args.length == 1 && args[0] instanceof IntValue val) { return valueOf(val); } + if (args[0] instanceof StringValue sv) { + return valueOf(NumberParsing.parseInt(sv, args)); + } return PlaceHolder.instance; } 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 601e6af3..30f4c2a7 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 @@ -439,28 +439,12 @@ private static LongValue min(LongValue a, LongValue b) { throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof StringValue sv) { - return parseLong(sv); + if (args[0] instanceof StringValue sv) { + return NumberParsing.parseLong(sv, args); } - // parseLong with radix not yet supported return PlaceHolder.instance; } - /** - * Symbolic wrapper for Long.parseLong(String s) - * Parses the string argument as a signed decimal long. - * - * @param s The String containing the long representation to be parsed - * @return The long value represented by the argument - */ - private static LongValue parseLong(StringValue s) { - SolverContext ctx = s.context; - StringFormulaManager sfm = ctx.getFormulaManager().getStringFormulaManager(); - BitvectorFormulaManager bvmgr = ctx.getFormulaManager().getBitvectorFormulaManager(); - return new LongValue(ctx, Long.parseLong(s.concrete), - bvmgr.makeBitvector(64, sfm.toIntegerFormula(s.formula))); - } - /** * Invocation handler for Long.parseUnsignedLong(*), handles argument conversion. * @@ -828,6 +812,10 @@ private static StringValue toString(LongValue l) { if (args.length == 1 && args[0] instanceof LongValue val) { return new LongObjectValue(val.context, val, ObjectValue.ADDRESS_UNKNOWN); } + if (args[0] instanceof StringValue sv) { + LongValue val = NumberParsing.parseLong(sv, args); + return new LongObjectValue(val.context, val, ObjectValue.ADDRESS_UNKNOWN); + } return PlaceHolder.instance; } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberParsing.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberParsing.java new file mode 100644 index 00000000..ae4a673f --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/NumberParsing.java @@ -0,0 +1,531 @@ +package de.uzl.its.swat.symbolic.invoke.java.lang; + +import de.uzl.its.swat.symbolic.invoke.java.lang.StringCallBranches.Branch; +import de.uzl.its.swat.symbolic.value.Value; +import de.uzl.its.swat.common.exceptions.NotImplementedException; +import de.uzl.its.swat.common.exceptions.ValueConversionException; +import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; +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 java.math.BigInteger; +import java.util.ArrayList; +import java.util.List; +import java.util.Map; +import java.util.concurrent.ConcurrentHashMap; +import java.util.function.IntPredicate; +import java.util.regex.Matcher; +import java.util.regex.Pattern; +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.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormulaManager; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +/** + * Models of parsing a number from a String: {@code Integer.parseInt}, {@code Long.parseLong}, + * {@code Short.parseShort}, {@code Byte.parseByte} (with or without a radix), {@code + * Float.parseFloat}, {@code Double.parseDouble}, and the {@code valueOf(String)} variants. + * + *

Whether such a call throws a NumberFormatException is a branch on the string (see {@link + * #branches}), which the visitor records on both sides of the call, so the solver can ask for a + * parseable string or for one that is not. + * + *

Integers are exact for strings of any length. A string is parseable iff it is an optional + * sign followed by at least one digit ({@link Character#digit(char, int)}, which accepts every + * Unicode decimal digit and the fullwidth Latin letters), and its value is in range. A value in + * range has at most K significant digits (r^K exceeds the range), so all digits but the last K are + * zeros, and the value is the sum over the last K digits. + * + *

Floats are exact where the decimal-to-binary rounding is a single IEEE operation: no + * exponent, no surrounding whitespace, the digits as an integer M exactly representable (M < + * 2^24 for float, 2^53 for double) and at most 10 (22) digits after the point, so that the value + * is the correctly rounded quotient M / 10^k of two exact operands. NaN and Infinity are exact as + * well. For the other parseable strings (exponents, hexadecimal, many digits, whitespace) the value + * is concrete and the call records precision loss; whether the string is parseable at all is exact + * for every string. + */ +public final class NumberParsing { + + /** An integral type: its range, and the name of its parse method. */ + private enum Integral { + BYTE(Byte.MIN_VALUE, Byte.MAX_VALUE), + SHORT(Short.MIN_VALUE, Short.MAX_VALUE), + INT(Integer.MIN_VALUE, Integer.MAX_VALUE), + LONG(Long.MIN_VALUE, Long.MAX_VALUE); + + final long min; + final long max; + + Integral(long min, long max) { + this.min = min; + this.max = max; + } + + /** The number of significant digits a value in range has at most in this radix. */ + int maxDigits(int radix) { + BigInteger limit = BigInteger.valueOf(min).negate(); + BigInteger p = BigInteger.ONE; + int k = 0; + while (p.compareTo(limit) <= 0) { + p = p.multiply(BigInteger.valueOf(radix)); + k++; + } + return k; + } + + /** Java's result of parsing {@code s}, or null if it throws a NumberFormatException. */ + Long parse(String s, int radix) { + try { + return switch (this) { + case BYTE -> (long) Byte.parseByte(s, radix); + case SHORT -> (long) Short.parseShort(s, radix); + case INT -> (long) Integer.parseInt(s, radix); + case LONG -> Long.parseLong(s, radix); + }; + } catch (NumberFormatException e) { + return null; + } + } + } + + private NumberParsing() {} + + // ---- the calls ---- + + /** The integral type a static call parses to, or null if it is not a modelled parse call. */ + private static Integral integral(String owner, String name, String desc) { + if (!desc.startsWith("(Ljava/lang/String;)") && !desc.startsWith("(Ljava/lang/String;I)")) return null; + return switch (owner + "." + name) { + case "java/lang/Integer.parseInt", "java/lang/Integer.valueOf" -> Integral.INT; + case "java/lang/Long.parseLong", "java/lang/Long.valueOf" -> Integral.LONG; + case "java/lang/Short.parseShort", "java/lang/Short.valueOf" -> Integral.SHORT; + case "java/lang/Byte.parseByte", "java/lang/Byte.valueOf" -> Integral.BYTE; + default -> null; + }; + } + + /** Whether a static call parses a float (false) or a double (true); null if it is not one. */ + private static Boolean floating(String owner, String name, String desc) { + if (!desc.startsWith("(Ljava/lang/String;)")) return null; + return switch (owner + "." + name) { + case "java/lang/Float.parseFloat", "java/lang/Float.valueOf" -> false; + case "java/lang/Double.parseDouble", "java/lang/Double.valueOf" -> true; + default -> null; + }; + } + + /** + * The branches of the static call {@code owner.name desc}, in order: empty if it is not a parse + * call or its string is not symbolic. The last one holds iff the call does not throw a + * NumberFormatException; a pin of a symbolic radix comes first. + */ + public static List branches(String owner, String name, String desc, Value[] args) { + try { + if (args.length == 0 || !(args[0] instanceof StringValue s) || !s.isSymbolic()) return List.of(); + Integral type = integral(owner, name, desc); + if (type != null) { + List branches = new ArrayList<>(); + Integer radix = radix(s.context, args, branches); + if (radix == null) return branches; + branches.add(new Branch(intValid(s.context, s.formula, radix, type), type.parse(s.concrete, radix) != null)); + return branches; + } + Boolean dbl = floating(owner, name, desc); + if (dbl != null) { + return List.of(new Branch(floatValid(s.context, s.formula), parseFloating(s.concrete, dbl) != null)); + } + } catch (Exception e) { + // Arguments of unexpected types: the model returns a PlaceHolder for them as well. + } + return List.of(); + } + + /** + * The branches a parse call that returned normally takes after those of {@link #branches}: for + * floats, whether the value is modelled exactly. It may hold or not. + */ + public static List returnBranches(String owner, String name, String desc, Value[] args) { + if (args.length == 0 || !(args[0] instanceof StringValue s) || !s.isSymbolic()) return List.of(); + Boolean dbl = floating(owner, name, desc); + if (dbl == null || parseFloating(s.concrete, dbl) == null) return List.of(); + return List.of(new Branch(floatExact(s.context, s.formula, dbl), floatExactConcrete(s.concrete, dbl))); + } + + /** + * The radix of a parse call (10 without one), with its branches added: if it is symbolic, the + * range check Java does first, and a pin of its concrete value. Null if the radix is out of + * range, so the call throws whatever the string. + */ + private static Integer radix(SolverContext ctx, Value[] args, List branches) throws Exception { + if (args.length < 2) return 10; + IntValue r = args[1].asIntValue(); + boolean inRange = r.concrete >= Character.MIN_RADIX && r.concrete <= Character.MAX_RADIX; + if (r.isSymbolic()) { + IntegerFormulaManager imgr = ctx.getFormulaManager().getIntegerFormulaManager(); + BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); + IntegerFormula f = r.asIntegerFormula(); + branches.add(new Branch(bmgr.and(imgr.greaterOrEquals(f, imgr.makeNumber(Character.MIN_RADIX)), + imgr.lessOrEquals(f, imgr.makeNumber(Character.MAX_RADIX))), inRange)); + if (inRange) branches.add(new Branch(imgr.equal(f, imgr.makeNumber(r.concrete)), true)); + } else if (!inRange) { + // Throws for every string: a branch without variables, which fails. + branches.add(new Branch(ctx.getFormulaManager().getBooleanFormulaManager().makeFalse(), false)); + } + return inRange ? r.concrete : null; + } + + /** The radix a parse call that returned used. */ + private static int radix(Value[] args) throws NotImplementedException, ValueConversionException { + return args.length < 2 ? 10 : args[1].asIntValue().concrete; + } + + // ---- the models ---- + + /** Integer.parseInt(String[, int]) that returned normally: exact, given the call's branches held. */ + public static IntValue parseInt(StringValue s, Value[] args) throws NotImplementedException, ValueConversionException { + int radix = radix(args); + int v = Integer.parseInt(s.concrete, radix); + if (!s.isSymbolic()) return new IntValue(s.context, v); + return new IntValue(s.context, v, intValue(s.context, s.formula, radix, Integral.INT)); + } + + /** Long.parseLong(String[, int]) that returned normally. */ + public static LongValue parseLong(StringValue s, Value[] args) throws NotImplementedException, ValueConversionException { + int radix = radix(args); + long v = Long.parseLong(s.concrete, radix); + if (!s.isSymbolic()) return new LongValue(s.context, v); + BitvectorFormulaManager bvmgr = s.context.getFormulaManager().getBitvectorFormulaManager(); + return new LongValue(s.context, v, bvmgr.makeBitvector(64, intValue(s.context, s.formula, radix, Integral.LONG))); + } + + /** Short.parseShort(String[, int]) that returned normally. */ + public static ShortValue parseShort(StringValue s, Value[] args) throws NotImplementedException, ValueConversionException { + int radix = radix(args); + short v = Short.parseShort(s.concrete, radix); + if (!s.isSymbolic()) return new ShortValue(s.context, v); + return new ShortValue(s.context, v, intValue(s.context, s.formula, radix, Integral.SHORT)); + } + + /** Byte.parseByte(String[, int]) that returned normally. */ + public static ByteValue parseByte(StringValue s, Value[] args) throws NotImplementedException, ValueConversionException { + int radix = radix(args); + byte v = Byte.parseByte(s.concrete, radix); + if (!s.isSymbolic()) return new ByteValue(s.context, v); + return new ByteValue(s.context, v, intValue(s.context, s.formula, radix, Integral.BYTE)); + } + + /** + * Float.parseFloat(String) that returned normally: exact if {@link #floatExact} holds, which + * the call's branches record; otherwise concrete, with precision loss. + */ + public static FloatValue parseFloat(StringValue s, SymbolicTraceHandler sth) { + float v = Float.parseFloat(s.concrete); + if (!s.isSymbolic()) return new FloatValue(s.context, v); + if (!floatExactConcrete(s.concrete, false)) { + sth.recordSymbolicPrecisionLoss(); + return new FloatValue(s.context, v); + } + return new FloatValue(s.context, v, floatValue(s.context, s.formula, false)); + } + + /** Double.parseDouble(String) that returned normally, as {@link #parseFloat}. */ + public static DoubleValue parseDouble(StringValue s, SymbolicTraceHandler sth) { + double v = Double.parseDouble(s.concrete); + if (!s.isSymbolic()) return new DoubleValue(s.context, v); + if (!floatExactConcrete(s.concrete, true)) { + sth.recordSymbolicPrecisionLoss(); + return new DoubleValue(s.context, v); + } + return new DoubleValue(s.context, v, floatValue(s.context, s.formula, true)); + } + + // ---- integers ---- + + private static final Map> CHAR_CLASSES = new ConcurrentHashMap<>(); + private static final Map DIGIT_TABLES = new ConcurrentHashMap<>(); + + /** The parts of a string parsed as an integer, as formulas. */ + private record IntParts(IntegerFormula signLength, BooleanFormula negative, IntegerFormula digitCount, IntegerFormula value) {} + + private static IntParts intParts(SolverContext ctx, StringFormula s, int radix, Integral type) { + FormulaManager fmgr = ctx.getFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + IntegerFormula len = smgr.length(s); + BooleanFormula negative = smgr.prefix(smgr.makeString("-"), s); + BooleanFormula signed = bmgr.or(negative, smgr.prefix(smgr.makeString("+"), s)); + IntegerFormula signLength = bmgr.ifThenElse(signed, imgr.makeNumber(1), imgr.makeNumber(0)); + IntegerFormula digitCount = imgr.subtract(len, signLength); + CodePointTables.Table digits = digitTable(radix); + List terms = new ArrayList<>(); + BigInteger weight = BigInteger.ONE; + for (int j = 0; j < type.maxDigits(radix); j++) { + IntegerFormula pos = imgr.subtract(len, imgr.makeNumber(j + 1)); + IntegerFormula digit = digitValue(imgr, bmgr, digits.segments(), 0, digits.segments().length, + smgr.toCodePoint(smgr.charAt(s, pos))); + IntegerFormula term = bmgr.ifThenElse(imgr.greaterThan(digitCount, imgr.makeNumber(j)), digit, imgr.makeNumber(0)); + terms.add(weight.equals(BigInteger.ONE) ? term : imgr.multiply(term, imgr.makeNumber(weight))); + weight = weight.multiply(BigInteger.valueOf(radix)); + } + return new IntParts(signLength, negative, digitCount, imgr.sum(terms)); + } + + /** + * Whether {@code s} parses as an integer of {@code type} in {@code radix} (in [2, 36]): an + * optional sign, then at least one digit, of which all but the last K are zeros, and the value + * in range. + */ + private static BooleanFormula intValid(SolverContext ctx, StringFormula s, int radix, Integral type) { + FormulaManager fmgr = ctx.getFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + IntParts p = intParts(ctx, s, radix, type); + RegexFormula digits = smgr.concat(smgr.closure(digitRegex(smgr, radix, true)), + upTo(smgr, digitRegex(smgr, radix, false), type.maxDigits(radix))); + IntegerFormula bound = bmgr.ifThenElse(p.negative(), + imgr.makeNumber(BigInteger.valueOf(type.min).negate()), imgr.makeNumber(type.max)); + return bmgr.and( + imgr.greaterOrEquals(p.digitCount(), imgr.makeNumber(1)), + smgr.in(smgr.substring(s, p.signLength(), p.digitCount()), digits), + imgr.lessOrEquals(p.value(), bound)); + } + + /** The value of {@code s} parsed as an integer of {@code type}, exact if {@link #intValid} holds. */ + private static IntegerFormula intValue(SolverContext ctx, StringFormula s, int radix, Integral type) { + IntParts p = intParts(ctx, s, radix, type); + IntegerFormulaManager imgr = ctx.getFormulaManager().getIntegerFormulaManager(); + return ctx.getFormulaManager().getBooleanFormulaManager().ifThenElse(p.negative(), imgr.negate(p.value()), p.value()); + } + + /** For the tests: {@link #intValid} for the type named int, long, short or byte. */ + public static BooleanFormula intValid(SolverContext ctx, StringFormula s, int radix, String type) { + return intValid(ctx, s, radix, Integral.valueOf(type.toUpperCase())); + } + + /** For the tests: {@link #intValue} for the type named int, long, short or byte. */ + public static IntegerFormula intValue(SolverContext ctx, StringFormula s, int radix, String type) { + return intValue(ctx, s, radix, Integral.valueOf(type.toUpperCase())); + } + + /** Character.digit(char, radix), tabulated over all chars: constant or offset segments. */ + private static CodePointTables.Table digitTable(int radix) { + return DIGIT_TABLES.computeIfAbsent(radix, r -> CodePointTables.table("digit/" + r + "/C", + c -> Character.digit((char) c, r), Character.MAX_VALUE, 32, true, false)); + } + + /** The digit value of code point x (-1 for a non-digit) as a balanced if-then-else tree. */ + private static IntegerFormula digitValue(IntegerFormulaManager imgr, BooleanFormulaManager bmgr, + CodePointTables.Segment[] segs, int from, int to, IntegerFormula x) { + if (to - from == 1) { + CodePointTables.Segment seg = segs[from]; + IntegerFormula value = imgr.makeNumber((int) seg.value()); + return seg.offset() ? imgr.add(x, value) : value; + } + int mid = (from + to) >>> 1; + return bmgr.ifThenElse(imgr.lessThan(x, imgr.makeNumber(segs[mid].lo())), + digitValue(imgr, bmgr, segs, from, mid, x), + digitValue(imgr, bmgr, segs, mid, to, x)); + } + + /** The chars that are digits in the radix ({@code zero}: whose value is 0), as a regex. */ + private static RegexFormula digitRegex(StringFormulaManager smgr, int radix, boolean zero) { + List ranges = CHAR_CLASSES.computeIfAbsent(radix + "/" + zero, k -> charRanges(zero + ? c -> Character.digit((char) c, radix) == 0 + : c -> Character.digit((char) c, radix) >= 0)); + RegexFormula result = null; + for (int[] r : ranges) { + RegexFormula range = smgr.range((char) r[0], (char) r[1]); + result = result == null ? range : smgr.union(result, range); + } + return result == null ? smgr.none() : result; + } + + /** The maximal ranges of chars satisfying {@code p}. */ + private static List charRanges(IntPredicate p) { + List ranges = new ArrayList<>(); + int c = 0; + while (c <= Character.MAX_VALUE) { + if (!p.test(c)) { + c++; + continue; + } + int lo = c; + while (c + 1 <= Character.MAX_VALUE && p.test(c + 1)) c++; + ranges.add(new int[] {lo, c}); + c++; + } + return ranges; + } + + /** r{0,n} */ + private static RegexFormula upTo(StringFormulaManager smgr, RegexFormula r, int n) { + RegexFormula result = smgr.makeRegex(""); + for (int i = 0; i < n; i++) result = smgr.optional(smgr.concat(r, result)); + return result; + } + + // ---- floats ---- + + /** The decimal forms modelled exactly: sign, integer digits, fraction digits. */ + private static final Pattern EXACT_DECIMAL = Pattern.compile("[+-]?(?:([0-9]+)(?:\\.([0-9]*))?|\\.([0-9]+))[fFdD]?"); + private static final Pattern EXACT_SPECIAL = Pattern.compile("[+-]?(?:NaN|Infinity)"); + + /** Java's result of parsing {@code s} as a float or double, or null if that throws. */ + private static Double parseFloating(String s, boolean dbl) { + try { + return dbl ? Double.parseDouble(s) : (double) Float.parseFloat(s); + } catch (NumberFormatException e) { + return null; + } + } + + /** The largest number of fraction digits whose power of ten the type holds exactly. */ + private static int maxFractionDigits(boolean dbl) { + return dbl ? 22 : 10; + } + + /** 2^p, p the type's precision: the digits as an integer must be below it. */ + private static BigInteger mantissaBound(boolean dbl) { + return BigInteger.ONE.shiftLeft(dbl ? 53 : 24); + } + + /** Whether the value of the parseable string {@code s} is modelled exactly (concretely). */ + public static boolean floatExactConcrete(String s, boolean dbl) { + if (EXACT_SPECIAL.matcher(s).matches()) return true; + Matcher m = EXACT_DECIMAL.matcher(s); + if (!m.matches()) return false; + String integer = m.group(1) == null ? "" : m.group(1); + String fraction = m.group(3) != null ? m.group(3) : m.group(2) == null ? "" : m.group(2); + return fraction.length() <= maxFractionDigits(dbl) + && new BigInteger(integer + fraction).compareTo(mantissaBound(dbl)) < 0; + } + + /** + * Whether {@code s} parses as a float or double, i.e. matches the grammar of {@link + * Double#valueOf(String)}, surrounding chars up to U+0020 included. + */ + public static BooleanFormula floatValid(SolverContext ctx, StringFormula s) { + StringFormulaManager smgr = ctx.getFormulaManager().getStringFormulaManager(); + RegexFormula ws = smgr.closure(smgr.range('\u0000', ' ')); + RegexFormula digits = smgr.cross(smgr.range('0', '9')); + RegexFormula hexDigits = smgr.cross(smgr.union(smgr.range('0', '9'), smgr.union(smgr.range('a', 'f'), smgr.range('A', 'F')))); + RegexFormula sign = smgr.optional(smgr.union(smgr.makeRegex("+"), smgr.makeRegex("-"))); + RegexFormula point = smgr.makeRegex("."); + RegexFormula exp = smgr.concat(smgr.union(smgr.makeRegex("e"), smgr.makeRegex("E")), sign, digits); + RegexFormula hexPrefix = smgr.concat(smgr.makeRegex("0"), smgr.union(smgr.makeRegex("x"), smgr.makeRegex("X"))); + RegexFormula decimal = smgr.union( + smgr.concat(digits, smgr.optional(point), smgr.optional(digits), smgr.optional(exp)), + smgr.concat(point, digits, smgr.optional(exp))); + RegexFormula hex = smgr.concat( + smgr.union( + smgr.concat(hexPrefix, hexDigits, smgr.optional(point)), + smgr.concat(hexPrefix, smgr.optional(hexDigits), point, hexDigits)), + smgr.union(smgr.makeRegex("p"), smgr.makeRegex("P")), sign, digits); + RegexFormula suffix = smgr.optional(smgr.union(smgr.union(smgr.makeRegex("f"), smgr.makeRegex("F")), + smgr.union(smgr.makeRegex("d"), smgr.makeRegex("D")))); + RegexFormula number = smgr.union( + smgr.union(smgr.makeRegex("NaN"), smgr.makeRegex("Infinity")), + smgr.concat(smgr.union(decimal, hex), suffix)); + return smgr.in(s, smgr.concat(ws, sign, number, ws)); + } + + /** The parts of a decimal string without exponent, as formulas. */ + private record DecimalParts(BooleanFormula form, BooleanFormula negative, IntegerFormula mantissa, IntegerFormula fractionDigits) {} + + private static DecimalParts decimalParts(SolverContext ctx, StringFormula s) { + FormulaManager fmgr = ctx.getFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + RegexFormula digits = smgr.cross(smgr.range('0', '9')); + RegexFormula point = smgr.makeRegex("."); + RegexFormula suffixChar = smgr.union(smgr.union(smgr.makeRegex("f"), smgr.makeRegex("F")), + smgr.union(smgr.makeRegex("d"), smgr.makeRegex("D"))); + RegexFormula form = smgr.concat( + smgr.optional(smgr.union(smgr.makeRegex("+"), smgr.makeRegex("-"))), + smgr.union(smgr.concat(digits, smgr.optional(smgr.concat(point, smgr.closure(smgr.range('0', '9'))))), + smgr.concat(point, digits)), + smgr.optional(suffixChar)); + IntegerFormula zero = imgr.makeNumber(0); + IntegerFormula one = imgr.makeNumber(1); + IntegerFormula len = smgr.length(s); + BooleanFormula negative = smgr.prefix(smgr.makeString("-"), s); + IntegerFormula start = bmgr.ifThenElse(bmgr.or(negative, smgr.prefix(smgr.makeString("+"), s)), one, zero); + IntegerFormula end = bmgr.ifThenElse(smgr.in(smgr.charAt(s, imgr.subtract(len, one)), suffixChar), + imgr.subtract(len, one), len); + IntegerFormula dot = smgr.indexOf(s, smgr.makeString("."), zero); + BooleanFormula hasDot = imgr.greaterOrEquals(dot, zero); + IntegerFormula integerEnd = bmgr.ifThenElse(hasDot, dot, end); + IntegerFormula fractionStart = imgr.add(dot, one); + IntegerFormula fractionDigits = bmgr.ifThenElse(hasDot, imgr.subtract(end, fractionStart), zero); + StringFormula integer = smgr.substring(s, start, imgr.subtract(integerEnd, start)); + StringFormula fraction = smgr.substring(s, fractionStart, fractionDigits); + StringFormula all = smgr.concat(integer, bmgr.ifThenElse(hasDot, fraction, smgr.makeString(""))); + return new DecimalParts(smgr.in(s, form), negative, smgr.toIntegerFormula(all), fractionDigits); + } + + private static RegexFormula special(StringFormulaManager smgr, String name) { + return smgr.concat(smgr.optional(smgr.union(smgr.makeRegex("+"), smgr.makeRegex("-"))), smgr.makeRegex(name)); + } + + /** + * Whether the value of a parseable {@code s} is modelled exactly: NaN, Infinity, or a decimal + * without exponent and whitespace whose digits form an integer below 2^p, with at most 10 (22) + * of them after the point. + */ + public static BooleanFormula floatExact(SolverContext ctx, StringFormula s, boolean dbl) { + FormulaManager fmgr = ctx.getFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + DecimalParts p = decimalParts(ctx, s); + return bmgr.or( + smgr.in(s, special(smgr, "NaN")), + smgr.in(s, special(smgr, "Infinity")), + bmgr.and(p.form(), + imgr.lessThan(p.mantissa(), imgr.makeNumber(mantissaBound(dbl))), + imgr.lessOrEquals(p.fractionDigits(), imgr.makeNumber(maxFractionDigits(dbl))))); + } + + /** The value of {@code s} parsed as a float or double: exact if {@link #floatExact} holds. */ + public static FloatingPointFormula floatValue(SolverContext ctx, StringFormula s, boolean dbl) { + FormulaManager fmgr = ctx.getFormulaManager(); + StringFormulaManager smgr = fmgr.getStringFormulaManager(); + IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager(); + BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager(); + FloatingPointFormulaManager fpmgr = fmgr.getFloatingPointFormulaManager(); + FormulaType.FloatingPointType type = dbl + ? FormulaType.getDoublePrecisionFloatingPointType() + : FormulaType.getSinglePrecisionFloatingPointType(); + DecimalParts p = decimalParts(ctx, s); + // M below 2^p converts exactly; 10^k for k up to the maximum is exact too, so the division + // rounds once, as Java's conversion of the exact decimal value does. + FloatingPointFormula mantissa = fpmgr.castFrom(bvmgr.makeBitvector(dbl ? 64 : 32, p.mantissa()), true, type); + FloatingPointFormula divisor = fpmgr.makeNumber(1, type); + for (int k = 1; k <= maxFractionDigits(dbl); k++) { + divisor = bmgr.ifThenElse(imgr.equal(p.fractionDigits(), imgr.makeNumber(k)), + fpmgr.makeNumber(BigInteger.TEN.pow(k).toString(), type), divisor); + } + FloatingPointFormula magnitude = fpmgr.divide(mantissa, divisor); + FloatingPointFormula decimal = bmgr.ifThenElse(p.negative(), fpmgr.negate(magnitude), magnitude); + FloatingPointFormula infinity = bmgr.ifThenElse(p.negative(), fpmgr.makeMinusInfinity(type), fpmgr.makePlusInfinity(type)); + return bmgr.ifThenElse(smgr.in(s, special(smgr, "NaN")), fpmgr.makeNaN(type), + bmgr.ifThenElse(smgr.in(s, special(smgr, "Infinity")), infinity, decimal)); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/ShortInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/ShortInvocation.java index 63c36e91..0e9390f1 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/ShortInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/ShortInvocation.java @@ -171,28 +171,12 @@ private static IntValue hashCode(ShortValue value) { throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException { assert args.length == 1 || args.length == 2 : "[SWAT] Expected 1 or 2 argument(s), got " + args.length; - if (args.length == 1 && args[0] instanceof StringValue sv) { - return parseShort(sv); + if (args[0] instanceof StringValue sv) { + return NumberParsing.parseShort(sv, args); } - // parseShort with radix not yet supported return PlaceHolder.instance; } - /** - * Symbolic wrapper for Short.parseShort(String s) - * Parses the string argument as a signed decimal short. - * - * @param s The String containing the short representation to be parsed - * @return The short value represented by the argument - */ - private static ShortValue parseShort(StringValue s) { - SolverContext ctx = s.context; - StringFormulaManager sfm = ctx.getFormulaManager().getStringFormulaManager(); - BitvectorFormulaManager bvmgr = ctx.getFormulaManager().getBitvectorFormulaManager(); - return new ShortValue(ctx, Short.parseShort(s.concrete), - bvmgr.makeBitvector(16, sfm.toIntegerFormula(s.formula))); - } - /** * Invocation handler for Short.reverseBytes(*), handles argument conversion. ToDo: Implement * symbolic handling @@ -355,12 +339,15 @@ private static LongValue toUnsignedLong(ShortValue x) { * type, likely a missing implementation */ private static Value invokeValueOf(Value[] args) - throws IndexOutOfBoundsException, ValueConversionException { + throws IndexOutOfBoundsException, ValueConversionException, NotImplementedException { assert args.length == 1 || args.length == 2 : "Expected 1 or 2 argument(s), got " + args.length; if (args.length == 1 && args[0] instanceof ShortValue val) { return valueOf(val); } + if (args[0] instanceof StringValue sv) { + return valueOf(NumberParsing.parseShort(sv, args)); + } return PlaceHolder.instance; } From 8f36a25f1d9dfe97be79a98a325c37dda2ed26d2 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Mon, 19 Oct 2026 14:44:07 +0000 Subject: [PATCH 2/2] Test that the number parsing models are exact L0: with the string fixed to an edge sample (empty, sign only, overflow, whitespace, hex, non-ASCII digits) and radix 2..36, the branch holds iff the JDK parses, and the value is the JDK's only; floats on fixed and random strings against Double.parseDouble/Float.parseFloat. Co-Authored-By: Claude Opus 5.5 --- .../lang/NumberParsingExactnessTest.groovy | 305 ++++++++++++++++++ 1 file changed, 305 insertions(+) create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/NumberParsingExactnessTest.groovy diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/NumberParsingExactnessTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/NumberParsingExactnessTest.groovy new file mode 100644 index 00000000..a056adaa --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/NumberParsingExactnessTest.groovy @@ -0,0 +1,305 @@ +package de.uzl.its.value.reference.lang + +import de.uzl.its.swat.symbolic.invoke.java.lang.NumberParsing +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.IntValue +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue +import de.uzl.its.swat.thread.ThreadHandler +import org.sosy_lab.java_smt.api.* +import spock.lang.Specification +import spock.lang.Unroll + +import static java.lang.Thread.currentThread + +/** + * L0: the models of parsing numbers from Strings are exact. With the string fixed to a sample, the + * branch of a call must hold iff Java does not throw a NumberFormatException, and the value must + * be Java's only (for floats: where the model claims to be exact). + */ +class NumberParsingExactnessTest extends Specification { + + SolverContext context + FormulaManager fmgr + BooleanFormulaManager bmgr + IntegerFormulaManager imgr + StringFormulaManager smgr + BitvectorFormulaManager bvmgr + FloatingPointFormulaManager fpmgr + + static final List EDGE = ["", "-", "+", "0", "-0", "+0", "+5", "--1", "+-1", "1-", "007", + "2147483647", "2147483648", "-2147483648", "-2147483649", "00000000002147483647", "-000000000002147483648", + " 1", "1 ", "0x1", "1_0", "١", "١٢٣", "-٠٠٧", "１２", "ａ", "१२", + "32767", "32768", "-32768", "-32769", "127", "128", "-128", "-129", + "9223372036854775807", "9223372036854775808", "-9223372036854775808", "-9223372036854775809", + "ff", "FF", "-ff", "z", "Z", "zz", "1a", "7fffffff", "80000000", "-80000000", "zik0zj", "1y2p0ij32e8e7", + "11111111111111111111111111111111", "-10000000000000000000000000000000", + "1111111111111111111111111111111111111111111111111111111111111111"] + + static final List FLOATS = ["0", "1", "-0", "+0", "1.5", ".5", "1.", "-.5F", "0.1", "0.3", "2.50", "33.3333", + "3.3333333", "1.0000001", "123456.7", "16777215", "16777216", "16777217", "0.0000000001", "0.00000000001", + "9007199254740991", "9007199254740992", "0.30000000000000004", "0.1234567890123456789012", "1.5f", "1.5d", "1.5D", + "NaN", "+NaN", "-NaN", "Infinity", "-Infinity", "nan", "NaNf", "1e5", "1E-3", "1e", "e5", ".e1", "0x1p3", + "0x1.8p1", "0X.8P-1f", "0x1", "0x", " 1.5 ", "\t2\n", "1 5", "", " ", ".", "+", "-", "1.5.5", "1_0", "١", + "abc", "fixed", "1f5", "00000000000000000000001.5"] + + def setup() { + ThreadHandler.init() + if (ThreadHandler.hasThreadContext(currentThread().id)) { + ThreadHandler.removeThreadContext(currentThread().id) + } + ThreadHandler.addThreadContext(currentThread().id, "Test-Thread", -2) + context = ThreadHandler.getSolverContext(currentThread().id) + fmgr = context.formulaManager + bmgr = fmgr.booleanFormulaManager + imgr = fmgr.integerFormulaManager + smgr = fmgr.stringFormulaManager + bvmgr = fmgr.bitvectorFormulaManager + fpmgr = fmgr.floatingPointFormulaManager + } + + def cleanup() { + context.close() + ThreadHandler.removeThreadContext(currentThread().id) + } + + /** A Java string as the solver sees it: one SMT char per UTF-16 char. */ + 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 boolean unsat(BooleanFormula... fs) { + context.newProverEnvironment().withCloseable { p -> + fs.each { p.addConstraint(it) } + return p.isUnsat() + } + } + + /** Whether, with s fixed to the sample, f holds (and its negation is unsatisfiable). */ + private boolean holds(StringFormula s, String sample, BooleanFormula f) { + return unsat(smgr.equal(s, chars(sample)), bmgr.not(f)) + } + + private boolean fails(StringFormula s, String sample, BooleanFormula f) { + return unsat(smgr.equal(s, chars(sample)), f) + } + + private static Long javaParse(String type, String s, int radix) { + try { + switch (type) { + case "byte": return (long) Byte.parseByte(s, radix) + case "short": return (long) Short.parseShort(s, radix) + case "int": return (long) Integer.parseInt(s, radix) + default: return Long.parseLong(s, radix) + } + } catch (NumberFormatException e) { + return null + } + } + + /** The branch holds iff Java parses the sample, and then the value is Java's only. */ + private void checkIntegral(String type, String sample, int radix) { + StringFormula s = smgr.makeVariable("s") + Long java = javaParse(type, sample, radix) + BooleanFormula valid = NumberParsing.intValid(context, s, radix, type) + if (java == null) { + assert fails(s, sample, valid): "$type '$sample' radix $radix: Java throws, the model parses" + } else { + assert holds(s, sample, valid): "$type '$sample' radix $radix: Java parses $java, the model throws" + NumeralFormula.IntegerFormula v = NumberParsing.intValue(context, s, radix, type) + assert holds(s, sample, imgr.equal(v, imgr.makeNumber(java))): "$type '$sample' radix $radix: not only $java" + } + } + + @Unroll + def "parsing a #type in radix 10 is exact on the edge strings"() { + expect: + EDGE.each { checkIntegral(type, it, 10) } + + where: + type << ["int", "long", "short", "byte"] + } + + @Unroll + def "parsing an int and a long is exact in radix #radix"() { + expect: + EDGE.each { checkIntegral("int", it, radix) } + EDGE.each { checkIntegral("long", it, radix) } + + where: + radix << (2..36) + } + + @Unroll + def "parsing a short and a byte is exact in radix #radix"() { + expect: + EDGE.each { checkIntegral("short", it, radix) } + EDGE.each { checkIntegral("byte", it, radix) } + + where: + radix << [2, 8, 16, 36] + } + + def "non-ASCII digits parse, as Character.digit accepts them"() { + expect: + Integer.parseInt("١٢") == 12 + checkIntegral("int", "١٢", 10) + checkIntegral("int", "１０", 10) + } + + private BooleanFormula sameFloat(FloatingPointFormula f, double java, boolean dbl) { + def type = dbl ? FormulaType.getDoublePrecisionFloatingPointType() : FormulaType.getSinglePrecisionFloatingPointType() + if (Double.isNaN(java)) return fpmgr.isNaN(f) + // Structural equality: tells -0.0 from 0.0. + return fpmgr.assignment(f, dbl ? fpmgr.makeNumber(java, type) : fpmgr.makeNumber((double) (float) java, type)) + } + + @Unroll + def "parsing a #name is exact where the model says so, and its branch holds iff Java parses"() { + expect: + FLOATS.each { sample -> + StringFormula s = smgr.makeVariable("s") + Double java + try { + java = dbl ? Double.parseDouble(sample) : (double) Float.parseFloat(sample) + } catch (NumberFormatException e) { + java = null + } + BooleanFormula valid = NumberParsing.floatValid(context, s) + if (java == null) { + assert fails(s, sample, valid): "'$sample': Java throws, the model parses" + return + } + assert holds(s, sample, valid): "'$sample': Java parses, the model throws" + BooleanFormula exact = NumberParsing.floatExact(context, s, dbl) + boolean claimed = NumberParsing.floatExactConcrete(sample, dbl) + assert claimed ? holds(s, sample, exact) : fails(s, sample, exact): "'$sample': exactness differs from its concrete check" + if (claimed) { + FloatingPointFormula v = NumberParsing.floatValue(context, s, dbl) + assert holds(s, sample, sameFloat(v, java, dbl)): "'$sample': not only $java" + } + } + + where: + name | dbl + "float" | false + "double" | true + } + + def "the float grammar agrees with Java on random strings"() { + given: + def random = new Random(4711) + def alphabet = "0123456789.+-eEpPxXfFdDaANnIity \t_" + + expect: + (1..400).each { + def sample = (1..random.nextInt(8)).collect { alphabet[random.nextInt(alphabet.length())] }.join() + boolean java = true + try { + Double.parseDouble(sample) + } catch (NumberFormatException e) { + java = false + } + StringFormula s = smgr.makeVariable("s") + BooleanFormula valid = NumberParsing.floatValid(context, s) + assert java ? holds(s, sample, valid) : fails(s, sample, valid): "'$sample': Java ${java ? 'parses' : 'throws'}" + if (java) { + boolean claimed = NumberParsing.floatExactConcrete(sample, true) + assert claimed ? holds(s, sample, NumberParsing.floatExact(context, s, true)) + : fails(s, sample, NumberParsing.floatExact(context, s, true)): "'$sample': exactness differs" + } + } + } + + def "the exact fragment covers the plain decimals, not exponents or many digits"() { + expect: + NumberParsing.floatExactConcrete("1.5", false) + NumberParsing.floatExactConcrete("-0", false) + NumberParsing.floatExactConcrete("16777215", false) + !NumberParsing.floatExactConcrete("16777216", false) + NumberParsing.floatExactConcrete("16777216", true) + !NumberParsing.floatExactConcrete("1e5", true) + !NumberParsing.floatExactConcrete(" 1", true) + !NumberParsing.floatExactConcrete("0x1p3", true) + } + + // ---- the branches of a call ---- + + private StringValue symbolicString(String concrete) { + return new StringValue(context, concrete, smgr.makeVariable("s"), -1) + } + + @Unroll + def "the last branch of Integer.parseInt('#sample') holds iff it does not throw"() { + given: + def s = symbolicString(sample) + def branches = NumberParsing.branches("java/lang/Integer", "parseInt", "(Ljava/lang/String;)I", [s] as Value[]) + + expect: + branches.size() == 1 + branches[0].holds() == (javaParse("int", sample, 10) != null) + + where: + sample << ["", "-", "+", "2147483647", "2147483648", "-2147483648", " 1", "1 ", "0x1", "١"] + } + + def "a symbolic radix is range checked and pinned; an invalid one throws for every string"() { + given: + def s = symbolicString("10") + def r = new IntValue(context, 16, bvmgr.makeVariable(32, "r")) + def bad = new IntValue(context, 37) + + when: + def pinned = NumberParsing.branches("java/lang/Integer", "parseInt", "(Ljava/lang/String;I)I", [s, r] as Value[]) + def invalid = NumberParsing.branches("java/lang/Long", "parseLong", "(Ljava/lang/String;I)J", [s, bad] as Value[]) + + then: + pinned*.holds() == [true, true, true] + invalid*.holds() == [false] + } + + def "a concrete string has no branches"() { + expect: + NumberParsing.branches("java/lang/Integer", "parseInt", "(Ljava/lang/String;)I", + [new StringValue(context, "12", -1)] as Value[]).isEmpty() + } + + def "Float.parseFloat has the validity branch, then, on a return, whether its value is exact"() { + given: + def s = symbolicString(sample) + + expect: + def args = [s] as Value[] + (NumberParsing.branches("java/lang/Float", "parseFloat", "(Ljava/lang/String;)F", args) + + NumberParsing.returnBranches("java/lang/Float", "parseFloat", "(Ljava/lang/String;)F", args))*.holds() == holds + + where: + sample | holds + "fixed" | [false] + "0.5" | [true, true] + "1e5" | [true, false] + } + + def "a value outside the exact fragment is concrete, with precision loss"() { + given: + def sth = ThreadHandler.getSymbolicTraceHandler(currentThread().id) + + when: + FloatValue exact = NumberParsing.parseFloat(symbolicString("2.5"), sth) + boolean lossAfterExact = sth.symbolicTrace.symbolicPrecisionLoss + DoubleValue approx = NumberParsing.parseDouble(symbolicString("1e5"), sth) + + then: + exact.concrete == 2.5f + exact.isSymbolic() + !lossAfterExact + approx.concrete == 1e5d + !approx.isSymbolic() + sth.symbolicTrace.symbolicPrecisionLoss + } +}