Make Long.parseLong work

regression/strings-smoke-tests/java_parselong_1/test.desc

@@ -0,0 +1,9 @@
+THOROUGH
+test_parselong.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
+--
+--

regression/strings-smoke-tests/java_parselong_1/test_parselong.java

@@ -0,0 +1,11 @@
+public class test_parselong
+{
+    public static void main(String[] args)
+    {
+        // 2^40
+        String str = new String("1099511627776");
+        long parsed = Long.parseLong(str);
+        assert(parsed == 1099511627776L);
+        assert(parsed != 1099511627776L);
+    }
+}

regression/strings-smoke-tests/java_parselong_2/test.desc

@@ -0,0 +1,9 @@
+THOROUGH
+test_parselong.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 7.* SUCCESS$
+^\[.*assertion.2\].* line 8.* FAILURE$
+--
+--

regression/strings-smoke-tests/java_parselong_2/test_parselong.java

@@ -0,0 +1,10 @@
+public class test_parselong
+{
+    public static void main(String[] args)
+    {
+        String str = new String("+00AbCdEf0123");
+        long parsed = Long.parseLong(str, 16);
+        assert(parsed == 737894400291L);
+        assert(parsed != 737894400291L);
+    }
+}

regression/strings-smoke-tests/java_parselong_3/test.desc

@@ -0,0 +1,9 @@
+THOROUGH
+test_parselong.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
+--
+--

regression/strings-smoke-tests/java_parselong_3/test_parselong.java

@@ -0,0 +1,11 @@
+public class test_parselong
+{
+    public static void main(String[] args)
+    {
+        // -2^41
+        String str = new String("-2199023255552");
+        long parsed = Long.parseLong(str, 10);
+        assert(parsed == -2199023255552L);
+        assert(parsed != -2199023255552L);
+    }
+}

regression/strings-smoke-tests/java_parselong_4/test.desc

@@ -0,0 +1,9 @@
+THOROUGH
+test_parselong.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 7.* SUCCESS$
+^\[.*assertion.2\].* line 8.* FAILURE$
+--
+--

regression/strings-smoke-tests/java_parselong_4/test_parselong.java

@@ -0,0 +1,10 @@
+public class test_parselong
+{
+    public static void main(String[] args)
+    {
+        String str = new String("7654321076543210");
+        long parsed = Long.parseLong(str, 8);
+        assert(parsed == 275730608604808L);
+        assert(parsed != 275730608604808L);
+    }
+}

regression/strings-smoke-tests/java_parselong_5/test.desc

@@ -0,0 +1,9 @@
+THOROUGH
+test_parselong.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
+--
+--

regression/strings-smoke-tests/java_parselong_5/test_parselong.java

@@ -0,0 +1,11 @@
+public class test_parselong
+{
+    public static void main(String[] args)
+    {
+        // -2^35
+        String str = new String("-100000000000000000000000000000000000");
+        long parsed = Long.parseLong(str, 2);
+        assert(parsed == -34359738368L);
+        assert(parsed != -34359738368L);
+    }
+}

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1945,6 +1945,12 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_function
     ["java::java.lang.Integer.parseInt:(Ljava/lang/String;I)I"]=
       ID_cprover_string_parse_int_func;
+  cprover_equivalent_to_java_function
+    ["java::java.lang.Long.parseLong:(Ljava/lang/String;)J"]=
+      ID_cprover_string_parse_int_func;
+  cprover_equivalent_to_java_function
+    ["java::java.lang.Long.parseLong:(Ljava/lang/String;I)J"]=
+      ID_cprover_string_parse_int_func;
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
       ID_cprover_string_of_int_hex_func;

src/solvers/refinement/string_constraint_generator.h

@@ -294,7 +294,7 @@ class string_constraint_generatort
 
   exprt add_axioms_for_parse_int(const function_application_exprt &f);
   exprt add_axioms_for_correct_number_format(
-    const string_exprt &str, const exprt &radix, std::size_t max_size=10);
+    const string_exprt &str, const exprt &radix, std::size_t max_size);
   exprt add_axioms_for_to_char_array(const function_application_exprt &f);
   exprt add_axioms_for_compare_to(const function_application_exprt &f);
 

src/solvers/refinement/string_constraint_generator_valueof.cpp

@@ -419,7 +419,9 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
   PRECONDITION(f.arguments().size()==1 || f.arguments().size()==2);
   string_exprt str=get_string_expr(f.arguments()[0]);
   const exprt radix=
-    f.arguments().size()==1?from_integer(10, f.type()):f.arguments()[1];
+    f.arguments().size()==1?
+      static_cast<exprt>(from_integer(10, f.type())):
+      static_cast<exprt>(typecast_exprt(f.arguments()[1], f.type()));
 
   const typet &type=f.type();
   symbol_exprt i=fresh_symbol("parsed_int", type);
@@ -436,21 +438,23 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
     not_exprt(or_exprt(starts_with_minus, starts_with_plus));
 
   /// TODO: we should throw an exception when this does not hold:
-  exprt correct=add_axioms_for_correct_number_format(str, radix);
+  const std::size_t max_string_length=40;
+  const exprt &correct=add_axioms_for_correct_number_format(
+    str, radix, max_string_length);
   axioms.push_back(correct);
 
   /// TODO(OJones): size should depend on the radix
   /// TODO(OJones): we should deal with overflow properly
-  for(unsigned size=1; size<=10; size++)
+  for(std::size_t size=1; size<=max_string_length; size++)
   {
     exprt sum=from_integer(0, type);
     exprt first_value=get_numeric_value_from_character(chr, char_type, type);
     equal_exprt premise=str.axiom_for_has_length(size);
 
-    for(unsigned j=1; j<size; j++)
+    for(std::size_t j=1; j<size; j++)
     {
       mult_exprt radix_sum(sum, radix);
-      if(j>=9)
+      if(j>=max_string_length-1)
       {
         // We have to be careful about overflows
         div_exprt div(sum, radix);
@@ -463,7 +467,7 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
         get_numeric_value_from_character(str[j], char_type, type));
 
       mult_exprt first(first_value, radix);
-      if(j>=9)
+      if(j>=max_string_length-1)
       {
         // We have to be careful about overflows
         div_exprt div_first(first, radix);