Fix string solver string-to-int conversion

Previously this both codified the relationship between strings and integers, *and* constrained the
input string to only contain appropriate characters. The constraint part of that is incorrect: it is
not functional (it has side-effects on its input), which meant the input string was also constrained
in other contexts. "if(s.equals("Hello")) { return 1; } else { return Integer.parseInt(s); }", for
example, would be partly unsatisfiable because s is constrained to only consist of digits due to the
parseInt operation.

This is fixed by splitting is_valid_int from parse_int, and updating models libraries to make the
validation check and throw a NumberFormatException if necessary, before using the now-pure-functional
parse_int routine

Author: smowton

jbmc/lib/java-models-library

@@ -0,0 +1,12 @@
+public class Test4
+{
+    public static void main(String input_string)
+    {
+        if(input_string.length() == 2) {
+            assert(Integer.parseInt(input_string) != 50);
+        }
+        else if(input_string.length() == 4) {
+            assert(!input_string.equals("XYZW"));
+        }
+    }
+}

jbmc/regression/strings-smoke-tests/java_parseint/Test4.class

@@ -0,0 +1,42 @@
+public class Test5
+{
+    public static void main(String input_string)
+    {
+      // Make test outputs readable by constraining length:
+      if(input_string.length() != 4)
+        return;
+      int check = Integer.parseInt(input_string);
+      boolean pass1 = false, pass2 = false, pass3 = false, throw1 = false, throw2 = false, throw3 = false;
+      // If we get here input_string should be validated, so parsing again shouldn't throw:
+      try {
+        Integer.parseInt(input_string);
+        pass1 = true;
+      }
+      catch(NumberFormatException e) {
+        throw1 = true;
+      }
+      // Make it invalid:
+      String broken = input_string + "&";
+      try {
+        Integer.parseInt(broken);
+        pass2 = true;
+      }
+      catch(NumberFormatException e) {
+        throw2 = true;
+      }
+      // Make it valid again:
+      String fixed = broken.substring(0, broken.length() - 1);
+      try {
+        Integer.parseInt(fixed);
+        pass3 = true;
+      }
+      catch(NumberFormatException e) {
+        throw3 = true;
+      }
+
+      // Check we followed the expected path:
+      assert(pass1 && throw2 && pass3 && !throw1 && !pass2 && !throw3);
+      // Check we can get to the end at all:
+      assert(false);
+    }
+}

jbmc/regression/strings-smoke-tests/java_parseint/Test4.java

@@ -0,0 +1,11 @@
+CORE
+Test4
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test4.main --trace
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 6.* FAILURE$
+^\[.*assertion.2\].* line 9.* FAILURE$
+dynamic_object2=\{ '5', '0' \}
+dynamic_object2=\{ 'X', 'Y', 'Z', 'W' \}
+--
+non equal types

jbmc/regression/strings-smoke-tests/java_parseint/Test5.class

@@ -0,0 +1,9 @@
+CORE
+Test5
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test5.main
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion..\].* line 38.* SUCCESS$
+^\[.*assertion..\].* line 40.* FAILURE$
+--
+non equal types

jbmc/regression/strings-smoke-tests/java_parseint/Test5.java

@@ -0,0 +1,42 @@
+public class Test_invalid_number_throws
+{
+    public static void main(String input_string)
+    {
+      // Make test outputs readable by constraining length:
+      if(input_string.length() != 4)
+        return;
+      long check = Long.parseLong(input_string);
+      boolean pass1 = false, pass2 = false, pass3 = false, throw1 = false, throw2 = false, throw3 = false;
+      // If we get here input_string should be validated, so parsing again shouldn't throw:
+      try {
+        Long.parseLong(input_string);
+        pass1 = true;
+      }
+      catch(NumberFormatException e) {
+        throw1 = true;
+      }
+      // Make it invalid:
+      String broken = input_string + "&";
+      try {
+        Long.parseLong(broken);
+        pass2 = true;
+      }
+      catch(NumberFormatException e) {
+        throw2 = true;
+      }
+      // Make it valid again:
+      String fixed = broken.substring(0, broken.length() - 1);
+      try {
+        Long.parseLong(fixed);
+        pass3 = true;
+      }
+      catch(NumberFormatException e) {
+        throw3 = true;
+      }
+
+      // Check we followed the expected path:
+      assert(pass1 && throw2 && pass3 && !throw1 && !pass2 && !throw3);
+      // Check we can get to the end at all:
+      assert(false);
+    }
+}