Fix exception handling in parseInt, parseLong

Previously these were directly interpreted by jbmc before exception checking, meaning you could
crash jbmc by passing a constant radix '37' for example.

Author: smowton

src/main/java/java/lang/Integer.java

@@ -410,51 +410,7 @@ public static int parseInt(String s, int radix)
                                             " greater than Character.MAX_RADIX");
         }
 
-        if (radix == 10) {
-            return parseInt(s);
-        }
-
-        //TODO from here on
-        int result = 0;
-        boolean negative = false;
-        int i = 0, len = s.length();
-        int limit = -Integer.MAX_VALUE;
-        int multmin;
-        int digit;
-
-        if (len > 0) {
-            char firstChar = CProverString.charAt(s, 0);
-            if (firstChar < '0') { // Possible leading "+" or "-"
-                if (firstChar == '-') {
-                    negative = true;
-                    limit = Integer.MIN_VALUE;
-                } else if (firstChar != '+')
-                    throw NumberFormatException.forInputString(s);
-
-                if (len == 1) // Cannot have lone "+" or "-"
-                    throw NumberFormatException.forInputString(s);
-                i++;
-            }
-            multmin = limit / radix;
-            while (i < len) {
-                // Accumulating negatively avoids surprises near MAX_VALUE
-                digit = Character.digit(CProverString.charAt(s, i++), radix);
-                if (digit < 0) {
-                    throw NumberFormatException.forInputString(s);
-                }
-                if (result < multmin) {
-                    throw NumberFormatException.forInputString(s);
-                }
-                result *= radix;
-                if (result < limit + digit) {
-                    throw NumberFormatException.forInputString(s);
-                }
-                result -= digit;
-            }
-        } else {
-            throw NumberFormatException.forInputString(s);
-        }
-        return negative ? result : -result;
+        return CProverString.parseInt(s, radix);
     }
 
     /**
@@ -475,7 +431,11 @@ public static int parseInt(String s, int radix)
      *               parsable integer.
      */
     public static int parseInt(String s) throws NumberFormatException {
-        return CProver.nondetInt(); //The function is handled by cbmc internally
+        if (s == null) {
+            throw new NumberFormatException("null");
+        }
+
+        return CProverString.parseInt(s, 10);
     }
 
     /**

src/main/java/java/lang/Long.java

@@ -474,46 +474,7 @@ public static long parseLong(String s, int radix)
                                             " greater than Character.MAX_RADIX");
         }
 
-        long result = 0;
-        boolean negative = false;
-        int i = 0, len = s.length();
-        long limit = -Long.MAX_VALUE;
-        long multmin;
-        int digit;
-
-        if (len > 0) {
-            char firstChar = CProverString.charAt(s, 0);
-            if (firstChar < '0') { // Possible leading "+" or "-"
-                if (firstChar == '-') {
-                    negative = true;
-                    limit = Long.MIN_VALUE;
-                } else if (firstChar != '+')
-                    throw NumberFormatException.forInputString(s);
-
-                if (len == 1) // Cannot have lone "+" or "-"
-                    throw NumberFormatException.forInputString(s);
-                i++;
-            }
-            multmin = limit / radix;
-            while (i < len) {
-                // Accumulating negatively avoids surprises near MAX_VALUE
-                digit = Character.digit(CProverString.charAt(s, i++), radix);
-                if (digit < 0) {
-                    throw NumberFormatException.forInputString(s);
-                }
-                if (result < multmin) {
-                    throw NumberFormatException.forInputString(s);
-                }
-                result *= radix;
-                if (result < limit + digit) {
-                    throw NumberFormatException.forInputString(s);
-                }
-                result -= digit;
-            }
-        } else {
-            throw NumberFormatException.forInputString(s);
-        }
-        return negative ? result : -result;
+        return CProverString.parseLong(s, radix);
     }
 
     /**
@@ -541,7 +502,10 @@ public static long parseLong(String s, int radix)
      *             parsable {@code long}.
      */
     public static long parseLong(String s) throws NumberFormatException {
-        return CProver.nondetLong(); //The function is handled by cbmc internally 
+        if (s == null) {
+            throw new NumberFormatException("null");
+        }
+        return CProverString.parseLong(s, 10);
     }
 
     /**

src/main/java/org/cprover/CProverString.java

@@ -440,4 +440,20 @@ public static String toString(float f) {
     public static String toString(double d) {
         return toString(CProver.doubleToFloat(d));
     }
+
+    /**
+     * Exactly as Integer.parseInt, except s is already checked non-null and the
+     * radix is already checked in-range.
+     */
+    public static int parseInt(String s, int radix) {
+        return CProver.nondetInt();
+    }
+
+    /**
+     * Exactly as Long.parseLong, except s is already checked non-null and the
+     * radix is already checked in-range.
+     */
+    public static long parseLong(String s, int radix) {
+        return CProver.nondetLong();
+    }
 }