Model parsing numbers from Strings, with NumberFormatException as a branch

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<StringCallBranches.Branch> 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<StringCallBranches.Branch> 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<StringCallBranches.Branch> 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
      *

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).
      */

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;
         };

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;
         };

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 <a href="https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/lang/Integer.html#parseInt(java.lang.String)">Integer.parseInt(String)</a>
-     */
-    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;
     }
 

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;
     }
 }