From 735065ce94f711f4d4a93461ab8901e0a5ef5550 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Mon, 10 Jul 2017 17:17:00 +0100 Subject: [PATCH] Make Long.parseLong work Note the tests are marked THOROUGH as they take a little too long. This should be solved by #702. --- .../java_parselong_1/test.desc | 9 +++++++++ .../java_parselong_1/test_parselong.class | Bin 0 -> 923 bytes .../java_parselong_1/test_parselong.java | 11 +++++++++++ .../java_parselong_2/test.desc | 9 +++++++++ .../java_parselong_2/test_parselong.class | Bin 0 -> 926 bytes .../java_parselong_2/test_parselong.java | 10 ++++++++++ .../java_parselong_3/test.desc | 9 +++++++++ .../java_parselong_3/test_parselong.class | Bin 0 -> 927 bytes .../java_parselong_3/test_parselong.java | 11 +++++++++++ .../java_parselong_4/test.desc | 9 +++++++++ .../java_parselong_4/test_parselong.class | Bin 0 -> 929 bytes .../java_parselong_4/test_parselong.java | 10 ++++++++++ .../java_parselong_5/test.desc | 9 +++++++++ .../java_parselong_5/test_parselong.class | Bin 0 -> 949 bytes .../java_parselong_5/test_parselong.java | 11 +++++++++++ .../java_string_library_preprocess.cpp | 6 ++++++ .../refinement/string_constraint_generator.h | 2 +- .../string_constraint_generator_valueof.cpp | 16 ++++++++++------ 18 files changed, 115 insertions(+), 7 deletions(-) create mode 100644 regression/strings-smoke-tests/java_parselong_1/test.desc create mode 100644 regression/strings-smoke-tests/java_parselong_1/test_parselong.class create mode 100644 regression/strings-smoke-tests/java_parselong_1/test_parselong.java create mode 100644 regression/strings-smoke-tests/java_parselong_2/test.desc create mode 100644 regression/strings-smoke-tests/java_parselong_2/test_parselong.class create mode 100644 regression/strings-smoke-tests/java_parselong_2/test_parselong.java create mode 100644 regression/strings-smoke-tests/java_parselong_3/test.desc create mode 100644 regression/strings-smoke-tests/java_parselong_3/test_parselong.class create mode 100644 regression/strings-smoke-tests/java_parselong_3/test_parselong.java create mode 100644 regression/strings-smoke-tests/java_parselong_4/test.desc create mode 100644 regression/strings-smoke-tests/java_parselong_4/test_parselong.class create mode 100644 regression/strings-smoke-tests/java_parselong_4/test_parselong.java create mode 100644 regression/strings-smoke-tests/java_parselong_5/test.desc create mode 100644 regression/strings-smoke-tests/java_parselong_5/test_parselong.class create mode 100644 regression/strings-smoke-tests/java_parselong_5/test_parselong.java diff --git a/regression/strings-smoke-tests/java_parselong_1/test.desc b/regression/strings-smoke-tests/java_parselong_1/test.desc new file mode 100644 index 00000000000..fa8ad9ccc48 --- /dev/null +++ b/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$ +-- +-- diff --git a/regression/strings-smoke-tests/java_parselong_1/test_parselong.class b/regression/strings-smoke-tests/java_parselong_1/test_parselong.class new file mode 100644 index 0000000000000000000000000000000000000000..d912ed08003c33b066551abc750ef9f2eb82ee74 GIT binary patch literal 923 zcmZuvU2hUm5IuKUSXh>iLP7kdT9me0N~Msd#Mo4QFsnXbnzTNc3vBS#?QXNX_)C0| zKj5>Ph_Q*j`=2z<-PR(~Y;t#I?#!Gs=g!aH-@XHAprs>)MGciWZs|~PTSpa32_&%` z1sLT38dh{9WY!%Wcd@FW#*km+zHfPfa2@}l@Ojs^`V4HJA=Va-2<|gPs!O{J>W(|H*KF<#YMsCnbQ|JuZ$Op#bFPVsA9xaRrjqD}Ad>qNhEyluy*E$!QAmemVTiYT z_US-+#~pe->#>mZ^V1AhWorXj%n|$lVW@F^ZF6&@UT?0qTCJwcThmZCu#S5M(#SBB zCPmwSm3`!SF7ZxJLuqIj*g$g%=y~_R>IDpi>gNrEyY!nsfEbBjoh%%o_? zruQcK`<5>}tA9q31Pg|AL65zU1=^bwZ4AqnI&;Fi*B|l7Iq=pI4Xp-MV{nPrX0e-MO>o4PLFgMSBOQ1w*M-w5$o$= wT=|8HhO%0q`h~M08{q`NTrT+q#t54F0czwkVzUFwHc=?X11ZZ5aunSB13X*2cmMzZ literal 0 HcmV?d00001 diff --git a/regression/strings-smoke-tests/java_parselong_1/test_parselong.java b/regression/strings-smoke-tests/java_parselong_1/test_parselong.java new file mode 100644 index 00000000000..a328af58250 --- /dev/null +++ b/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); + } +} diff --git a/regression/strings-smoke-tests/java_parselong_2/test.desc b/regression/strings-smoke-tests/java_parselong_2/test.desc new file mode 100644 index 00000000000..17db69e3979 --- /dev/null +++ b/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$ +-- +-- diff --git a/regression/strings-smoke-tests/java_parselong_2/test_parselong.class b/regression/strings-smoke-tests/java_parselong_2/test_parselong.class new file mode 100644 index 0000000000000000000000000000000000000000..d0ba8c19bc710603d76026422fffd27612d95e29 GIT binary patch literal 926 zcmZuwO>fgc5Pj=7apE}NO$gs9EhK56NlSnOr6LMN0vR|2Rcbk)O=5zJYge|zFX2MO zodYL8B8WC3GaUVWD5#vDqlv0~4{lPQ zU2fV8g~}6shri@?i`#>G$9GLS4RE+Spvv4a$3(^RU4b}LNpu4c!Tml%qT}=4iwAr! zphL1SMAv%O;XrD~8M-~=t|{o}rWr1a)*8~t5c~gOsBx{)Xm#8Djc1LO)vF?}pr+6Fx;sYCXUJD(hZOQ8C+&3-lpz+(eP9=k zDY{oBJyMgZwnaaj^zR#<=^Fhbj-;4Bqyzff+nA?|lc0OU(nT>9Ss@TjWN6KjSErrP z9$p%Qy(dFLj@C#JWSApcJ4iqt1@dAzfg(jj@f*nW0qgsawz8oyWWAP7e@3|V0g(}M zr8y|CUL(Gb*wz^8w|}CeNmQVQ0@MP;6%Rut{0tP75ydS+6f8=VLr6G@Q?#q}QcmLx z@yO5vIE!<{`+N|Wexa$DL6P4=4t+#qc4W~e3`x5!gtWOoQAlFx}{+r3o7ai`5Er}rWaVQ<3F%`-nPvy1KVMUu33&1tTRNawJipD)9soJ zX~S~NXZ^jl>Aeua3^~K?aC?h;me5a(a`4*n88Sv-`oXJx?)j$eI=#D8XOCMBL$UhO z*yV3|-R4fO-U>X6yde(vdX$+z!%bBDz!QiQnM5}P5!|0JBwGRRym`v^Lpn4ThS*xi zK50m6xqYu=KC%S;{5Zn}QCdd^Sz`Y`3`1(Zv9!9n*jR3?(AN-wiz=3MG_b5Ag)~EH zl(q49v=2ScCE}@ZEEP>1E4V#|^t`=mb^?Y%b+St_pVX+lK@(+&hm9Z0#WRu~*JvQ= zQP!qSCr$^@HGRu7yQds!WI>-Cblf|brkj(bJHs+1(G^J%5KUxh&5>58ozbq$4#7T= zAR$j{G&C|yk*psFpnxK2ahyYmEF$>>Wcq>i14!Gs$PltIm(jjK+4zj;0QvG1)OYWZ zI6!=R2<_)T*1^asP$MB~5emssXmrK1h@nDg_ec{g$`nILIFAdoYxGnu;u7)5(hInZ zE5!S1XqSGYqM|GpD1Z92&1TpGkj*8&LLWetKSGXtL3FZZQAUBJ-xq_qMv8>%e*mr~ BzzhHY literal 0 HcmV?d00001 diff --git a/regression/strings-smoke-tests/java_parselong_3/test_parselong.java b/regression/strings-smoke-tests/java_parselong_3/test_parselong.java new file mode 100644 index 00000000000..e05341bdb86 --- /dev/null +++ b/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); + } +} diff --git a/regression/strings-smoke-tests/java_parselong_4/test.desc b/regression/strings-smoke-tests/java_parselong_4/test.desc new file mode 100644 index 00000000000..17db69e3979 --- /dev/null +++ b/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$ +-- +-- diff --git a/regression/strings-smoke-tests/java_parselong_4/test_parselong.class b/regression/strings-smoke-tests/java_parselong_4/test_parselong.class new file mode 100644 index 0000000000000000000000000000000000000000..89e6a99d4abcb7c4121abf106898def48d7b314c GIT binary patch literal 929 zcmZuwOK;Oa5dPM2;>2;@O$hH63Q1aM`bgUYrJ^bzfeajiDzzNYCRqg+*RE`b-@p&x zLd2ajAQ40*xN+boA%U26A0edjV;(y*-#4?nKmUCF2B3je9Vtv}xE9BC9SSNss;DK9 z#7q?U_2V_Y8fJAQWYi5EH!-K7&QO@g;jL zVJKCfnY;WIuiM<|)|-K6(Q1gpy)I=IPFW@@e&9*Ou}q>Hf=KQU8B)!Fw_iTu`ym|~ z3qyRZZ67tHH{G7s7WXYlzc9*hPL?*1MUL424@0iimF33L;==r~l%ew)77Q$6$v_$z zhVn3P<9N9DJkKTS=}|Nd4Fk(q8Nqte+7<19p;#U7Q%)#7EN{|G84_XZhkEIhqz5$` zNoJU}Y15w57IcJfd7^W|k%kuZXn{6-2UB!*QgpUhwk*3MEdrv69R2fT)k!jv(U}3* z2T~Li=pPH63=^aqhXE*}L{ZHv^*aMKuCqKjJLsQ>FjeJ6Eyk%J?3dOi12XloC1y}z9 D$DqOl literal 0 HcmV?d00001 diff --git a/regression/strings-smoke-tests/java_parselong_4/test_parselong.java b/regression/strings-smoke-tests/java_parselong_4/test_parselong.java new file mode 100644 index 00000000000..67eee61b85a --- /dev/null +++ b/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); + } +} diff --git a/regression/strings-smoke-tests/java_parselong_5/test.desc b/regression/strings-smoke-tests/java_parselong_5/test.desc new file mode 100644 index 00000000000..fa8ad9ccc48 --- /dev/null +++ b/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$ +-- +-- diff --git a/regression/strings-smoke-tests/java_parselong_5/test_parselong.class b/regression/strings-smoke-tests/java_parselong_5/test_parselong.class new file mode 100644 index 0000000000000000000000000000000000000000..deaff359766878fc996234305ee5403faf397641 GIT binary patch literal 949 zcmah|%Wl(95Ixtiv+5S3uh7qNjb*DVbpl}IGtnYlA_&K!@w|N8P3Km#{5q%f;uZVK}nBwW!@MJ<6O z7L?&|_=A$5Vo^gvWL?#;gk=?VhQcfl0?Q9=&kZ*1fVUm1!@zbJ;!WGN!#fPIYHf=_ z-tamWL&mUO>v3n{fG|9 z!Z6h|ouh%Yme=!5>%J}M7seSbi`F`_$PxR0VHoC?R#*Q26ZI=9R&`v%nvOIw4CPU? z^*@T=^L>xzNsm)d(a>=nH^vA&Y42KQ$WW|K4liU&kJ=j~G(#fN{=15A0J-VPR*ue}fREk!KWy@kJvSJ{b$k8)TUY$-xr?M~rdryXh z0zKnVkYSo^{V)MVl*miq6v`A4#cv_gAGm!0X*(YqKsFYY&rsGsAl^rzG7a_h8zc{q z*d9Rp_E)q&iVDzJ1X_YZb{rZleirmy5LlBuL83xA1ccK#L#Ku{oW(h!k)`kAJT4IJ yi&0$qiFp+jxk&Xh$5S?<5rAAi`3ZU-s{9Ue>?7in6N@$qB>k??CT6U7|> literal 0 HcmV?d00001 diff --git a/regression/strings-smoke-tests/java_parselong_5/test_parselong.java b/regression/strings-smoke-tests/java_parselong_5/test_parselong.java new file mode 100644 index 00000000000..ac30cc8af83 --- /dev/null +++ b/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); + } +} diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 03fed3afa9f..d34c4f0308d 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/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; diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 55c453d480d..082508871fa 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/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); diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 24dead705c3..c59a20dab81 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/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(from_integer(10, f.type())): + static_cast(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=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);