From f27e28cc4cdae7504725d87513546d984640a201 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Tue, 17 Sep 2019 19:14:18 +0100 Subject: [PATCH 1/6] Add String.trim() --- .../ConstantEvaluationTrim/Main.class | Bin 0 -> 1578 bytes .../ConstantEvaluationTrim/Main.java | 50 ++++++++++++++++ .../ConstantEvaluationTrim/empty.desc | 9 +++ .../ConstantEvaluationTrim/linebreak.desc | 9 +++ .../middleWhitespace.desc | 9 +++ .../ConstantEvaluationTrim/noTrim.desc | 9 +++ .../ConstantEvaluationTrim/noprop.desc | 9 +++ .../ConstantEvaluationTrim/tab.desc | 9 +++ .../ConstantEvaluationTrim/trim.desc | 9 +++ .../ConstantEvaluationTrim/trimLeft.desc | 9 +++ .../ConstantEvaluationTrim/trimRight.desc | 9 +++ src/goto-symex/goto_symex.cpp | 56 ++++++++++++++++++ src/goto-symex/goto_symex.h | 6 ++ 13 files changed, 193 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/empty.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/linebreak.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/middleWhitespace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noTrim.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noprop.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/tab.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/trim.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/trimLeft.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationTrim/trimRight.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..5c80d03b77f85ebd481d8cd2d47af4d83cbc52fe GIT binary patch literal 1578 zcmb7@TTc^F6ouF6g_%wZy>JyN35Qc%2t2!cEnO@L_RZQ34TV0v*nCGn@oAMjaC zAkjqM{Y}QWP79RKdZClfoU`|y@2s=-oFBiwd;>6#H3OZP)G=ish3OFDxTRx8P0|`> z4QMJkr{lJcJ38id+|_YU$9)|SG(0r$2n!k(1v*EqN=3S!T`E@A?246jWL`k*2(&HQ zMcZ2v@J~#>6bP)A@=_q0v5WF~wUCwWwkl@AbM1ma`<7?r4mPZEEv(@&3B}TOEvKuJ zjC|t>gw$};-reJv`LbIo3v^Fp_N_xJ?O4U#^cE|My9;W~pe&TVcU0h6S-$FU>8vZQ z1A$n<&gUKZYR~p$rEKM>Lto6Xpr+W^DplQ_T(_0J(1v9fXB0nz9`rI`nx>V_@lKTy z^kXT4E_8DlMk9EFWr4nio|Q9yp1E$xrKsA=RA0w%P=^VC#+m#Zw8=F0q~ny#ymcs9 zC}1?^^h{~euoA&jta3Mv)m~)xWscrl2-OV{=$e>pwu#Hjw^hrjTyn9_S(s!aqYe71 z!)^=oKOjaCj^erl}ZGU(RPIJS7@(Kpnq2sUyYJLfMY+e0CWT~ zMDBG)bcmlA(l9`N^56Ur`S1VC50P(>874o{#2;+IH?E{VN`8#|IQfYt{!j~k_)7e4 z@_WedCBLtUZ?c8;R;{1!0RjJK1R96s?8vD;1>uV(to_constant_expr(expr)); + return character > ' '; + }; + + // Note the points where a trim would trim too. + auto &operands = s_data_opt->get().operands(); + auto end_iter = + std::find_if(operands.rbegin(), operands.rend(), is_not_whitespace); + auto start_iter = + std::find_if(operands.begin(), operands.end(), is_not_whitespace); + + // Then copy in the string with leading/trailing whitespace removed. + // Note: if start_iter == operands.end it means the entire string is + // whitespace, so we'll trim it to be empty anyway. + exprt::operandst new_operands; + if(start_iter != operands.end()) + new_operands = exprt::operandst{start_iter, end_iter.base()}; + + const constant_exprt new_char_array_length = + from_integer(new_operands.size(), length_type); + + const array_typet new_char_array_type(char_type, new_char_array_length); + const array_exprt new_char_array( + std::move(new_operands), new_char_array_type); + + assign_string_constant( + state, + symex_assign, + to_ssa_expr(f_l1.arguments().at(0)), + new_char_array_length, + to_ssa_expr(f_l1.arguments().at(1)), + new_char_array); + + return true; +} diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 6f320a01658..d0f6575faef 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -657,6 +657,12 @@ class goto_symext symex_assignt &symex_assign, const function_application_exprt &f_l1); + /// Attempt to constant propagate trim operations. + bool constant_propagate_trim( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1); + /// Assign constant string length and string data given by a char array to /// given ssa variables /// From 030d6a32ef6d01f5d397e39b7dd08e953eb49b2e Mon Sep 17 00:00:00 2001 From: johndumbell Date: Wed, 18 Sep 2019 12:21:21 +0100 Subject: [PATCH 2/6] Add String.contains(...) --- .../ConstantEvaluationContains/Main.class | Bin 0 -> 1223 bytes .../ConstantEvaluationContains/Main.java | 31 ++++++++++++ .../alphanumeric.desc | 9 ++++ .../ConstantEvaluationContains/contains.desc | 9 ++++ .../doesntContain.desc | 9 ++++ .../ConstantEvaluationContains/noPi.desc | 9 ++++ .../ConstantEvaluationContains/nondetArg.desc | 9 ++++ .../ConstantEvaluationContains/noprop.desc | 9 ++++ .../ConstantEvaluationContains/pi.desc | 9 ++++ src/util/simplify_expr.cpp | 46 ++++++++++++++++++ 10 files changed, 140 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationContains/alphanumeric.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationContains/contains.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationContains/doesntContain.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationContains/noPi.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationContains/pi.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..7e72b920b4ec2c53781517e785c4a9e6bca7bdca GIT binary patch literal 1223 zcmaiyT~8B16o%jFw%rewQWgrO2!5gRp`d`Ef&@}EF#$EHF_9ZG-JQTfnXS89uKgSG z2fS7jNHo!VZ~Q~XcxFo}MvIwbcIM34=bZPP^ZnQ7uK?!pz(O8l2CkXN;ktnv7RE85 zW70xa*{2NLG;qtnw1F7|w{_gHFpD`I^9+4sJc>jZ`+VjDskw`?Ijh*l!5d_ycTX#Oc}iJ8B%rHY+kGHaM{=wq3=@E zWw&;cpH&GOp(~#FDjRcyQkhm{8-3_!$ndJ`2^+m|h~#>dm5o6xFcjPI*IG4r9EL$i zl3kBec#j_tGWFxF(n05~T5uquEp_kW-ooOnj*HiO3IycbYQQJZ{hfwP_QVX$0~# z6)ay=is@v6nv8zh3v?TyFQac}@)+!ca>M}b*~F-x22Wj|B1H=rc2esfp&g=s%1Iv~ zbBL}l$i6;?{!IZ=2_OfJ&Kj*WO30u{Hv{Y^N;-xJTRInO5cXYXtU*|l5Y}JVVO$`% z687*U+v0yywGvg`q%@cCG_XN}jC4Xd=2R!uO;j(ToU^FWQ?V-)OO<;l$*SO(j@3zO zlT{$jK#NtRe=l}qbtSBScB9D}B2MWn>rzLS?R1~7afCRdZI(fU)*7k#L?O`YFJvC1$2 literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.java new file mode 100644 index 00000000000..aa05e11b84c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.java @@ -0,0 +1,31 @@ +public class Main { + public void contains() { + String str = "abcde"; + assert str.contains("cd"); + } + + public void doesntContain() { + String str = "abcde"; + assert !str.contains("cda"); + } + + public void noprop(String str) { + assert str.contains("cd"); + } + + public void nondetArg(String str) { + assert "dave".contains(str); + } + + public void noPi() { + assert !"dave".contains("π"); + } + + public void pi() { + assert "dave_loves_π".contains("π"); + } + + public void alphanumeric() { + assert "ad672naksd3".contains("72n"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/alphanumeric.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/alphanumeric.desc new file mode 100644 index 00000000000..bdedcbc0df6 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/alphanumeric.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.alphanumeric --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/contains.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/contains.desc new file mode 100644 index 00000000000..78ec5d2688f --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/contains.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.contains --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/doesntContain.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/doesntContain.desc new file mode 100644 index 00000000000..68996343768 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/doesntContain.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.doesntContain --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noPi.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noPi.desc new file mode 100644 index 00000000000..ea3b279c50c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noPi.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noPi --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc new file mode 100644 index 00000000000..93db2edb075 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc new file mode 100644 index 00000000000..27e95eab525 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/pi.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/pi.desc new file mode 100644 index 00000000000..42cc4811a28 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/pi.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.pi --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 0abfde728e3..b06babf15ac 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -180,6 +180,48 @@ static simplify_exprt::resultt<> simplify_string_endswith( return from_integer(res ? 1 : 0, expr.type()); } +/// Simplify String.contains function when arguments are constant +static simplify_exprt::resultt<> simplify_string_contains( + const function_application_exprt &expr, + const namespacet &ns) +{ + // We want to get both arguments of any starts-with comparison, and + // trace them back to the actual string instance. All variables on the + // way must be constant for us to be sure this will work. + auto &first_argument = to_string_expr(expr.arguments().at(0)); + auto &second_argument = to_string_expr(expr.arguments().at(1)); + + const auto first_value_opt = + try_get_string_data_array(first_argument.content(), ns); + + if(!first_value_opt) + { + return simplify_exprt::unchanged(expr); + } + + const array_exprt &first_value = first_value_opt->get(); + + const auto second_value_opt = + try_get_string_data_array(second_argument.content(), ns); + + if(!second_value_opt) + { + return simplify_exprt::unchanged(expr); + } + + const array_exprt &second_value = second_value_opt->get(); + + // Is our 'contains' array directly contained in our target. + const bool includes = + std::search( + first_value.operands().begin(), + first_value.operands().end(), + second_value.operands().begin(), + second_value.operands().end()) != first_value.operands().end(); + + return from_integer(includes ? 1 : 0, expr.type()); +} + /// Simplify String.isEmpty function when arguments are constant /// \param expr: the expression to simplify /// \param ns: namespace @@ -510,6 +552,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_function_application( { return simplify_string_char_at(expr, ns); } + else if(func_id == ID_cprover_string_contains_func) + { + return simplify_string_contains(expr, ns); + } return unchanged(expr); } From b9b3fea07d40d4baa5d779581774556891f27c18 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Wed, 18 Sep 2019 14:14:36 +0100 Subject: [PATCH 3/6] Add String.toLowerCase() / String.toUpperCase() --- .../ConstantEvaluationToLowerCase/Main.class | Bin 0 -> 1468 bytes .../ConstantEvaluationToLowerCase/Main.java | 43 +++++++++++ .../ConstantEvaluationToLowerCase/empty.desc | 9 +++ .../emptyArg.desc | 9 +++ .../emptyThis.desc | 9 +++ .../noLower.desc | 9 +++ .../nonAlpha.desc | 9 +++ .../nondetArg.desc | 9 +++ .../ConstantEvaluationToLowerCase/noprop.desc | 9 +++ .../ConstantEvaluationToLowerCase/pi.desc | 13 ++++ .../toLower.desc | 9 +++ .../ConstantEvaluationToUpperCase/Main.class | Bin 0 -> 1492 bytes .../ConstantEvaluationToUpperCase/Main.java | 43 +++++++++++ .../ConstantEvaluationToUpperCase/empty.desc | 9 +++ .../emptyArg.desc | 9 +++ .../emptyThis.desc | 9 +++ .../noUpper.desc | 9 +++ .../nonAlpha.desc | 9 +++ .../nondetArg.desc | 9 +++ .../ConstantEvaluationToUpperCase/noprop.desc | 9 +++ .../ConstantEvaluationToUpperCase/pi.desc | 13 ++++ .../toUpper.desc | 9 +++ src/goto-symex/goto_symex.cpp | 70 ++++++++++++++++++ src/goto-symex/goto_symex.h | 7 ++ 24 files changed, 333 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/empty.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyArg.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyThis.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noLower.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nonAlpha.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nondetArg.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noprop.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/pi.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/toLower.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/empty.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyArg.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyThis.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noUpper.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nonAlpha.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nondetArg.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noprop.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/pi.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/toUpper.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..65b208f272dc39f96a12f958dc1bda9141ce2118 GIT binary patch literal 1468 zcmaiz+fNfg6vn^lh237Dr4%eefg)f_6-4n0UTT4-qKOa_c`(_w8(1v6b-Ts*=D#7Y zKKQIAkZ7WbkG}X18RIuwXiI1@o6OG4nf;ybd}sF8->=^REaG7hQOu~g97GzK0QxYi zA}beH6kH8Lk-<3?^D3^XSWt0Y!Hpn4ys6-pz`&GNtLe65SY~a-sAjII2Vd_undqv&el!pZr$0}HFbX%Zz!_i8w*0rh|QE;0<^CZ|~ zT2|o{($@?rEwHW`=A6tH#sK2vz`bZlQovpH z%grj-9H-6z+qs1l?@5&RM?@3S1kOS%fF5xi^%zucU1BAXod2s~whopF1N(?^Ey?lI7;m0_+3GS#6e=x3K znEZ?X=Lg7t-<=;IKS*YX{O}q62u7Jjmb!MVKY2>LrKIEuVwq(@xHxUbwEQih>2i=|wV}wphZz*wvpO1IN zg(Z%|dAKBTW9_(!uDD)_<8U4>MciaNE_FVRUUv4cQS3BvGwry^t~l8hS6#>Z)4*kj vn{DA#Tx#ML-9`ZYvA#n@4xsox!sq=0U+a#a{3+6VKRn?_@~4^N!h`95tAgw= literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.java new file mode 100644 index 00000000000..60ad536fd09 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.java @@ -0,0 +1,43 @@ +public class Main { + public void toLower() { + String str = "ABCDE"; + str = str.toLowerCase(); + assert str.equals("abcde"); + } + + public void noLower() { + String str = "ABCDE"; + str = str.toLowerCase(); + assert !str.equals("abcdE"); + } + + public void noprop(String str) { + str = str.toLowerCase(); + assert str.equals("ABCDE"); + } + + public void nondetArg(String str) { + str = "dave".toLowerCase(); + assert !str.equals(str); + } + + public void pi() { + assert "π".toLowerCase().equals("π"); + } + + public void nonAlpha() { + assert "^£&$1!".toLowerCase().equals("^£&$1!"); + } + + public void empty() { + assert "".toLowerCase().equals(""); + } + + public void emptyThis() { + assert !"".toLowerCase().equals("dave"); + } + + public void emptyArg() { + assert !"dave".toLowerCase().equals(""); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/empty.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/empty.desc new file mode 100644 index 00000000000..15b1a57602c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/empty.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.empty --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyArg.desc new file mode 100644 index 00000000000..279e22eb4bd --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyThis.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyThis.desc new file mode 100644 index 00000000000..7e85f448edb --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyThis.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyThis --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noLower.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noLower.desc new file mode 100644 index 00000000000..9fdcf0d49e2 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noLower.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noLower --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nonAlpha.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nonAlpha.desc new file mode 100644 index 00000000000..49684c9e415 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nonAlpha.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nonAlpha --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nondetArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nondetArg.desc new file mode 100644 index 00000000000..93db2edb075 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nondetArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noprop.desc new file mode 100644 index 00000000000..27e95eab525 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noprop.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/pi.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/pi.desc new file mode 100644 index 00000000000..cbed1f44433 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/pi.desc @@ -0,0 +1,13 @@ +CORE +Main.class +--function Main.pi --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This is technically wrong (as pi has an uppercase) but our current implementation +only constant props things within the 0 - 128 range due to the tolower/toupper methods +currently being used. If this ever changes to be a true all-character case change, +just modify the test. \ No newline at end of file diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/toLower.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/toLower.desc new file mode 100644 index 00000000000..0a218afeeb9 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/toLower.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.toLower --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..ca120cd04d584ae9606ced07bb0e2f2ac52b4885 GIT binary patch literal 1492 zcma)*-A~g{7{;Hob!*oZHp+$r#>WtFV+x}9IYh>QtD%XYiCma;TLZ<>&aT6F=f5Gh zUU;o0Bhf??FTL>}GRF6G?1QkOX>xkbdEfrd^FHtC&p%(j0a(JCi~(Gckd%?aTmT`Y zC0yl;Ya-@lh&;F;;ktxH2{$C%W^xN1>N4^$qb@nJ*`x9o1t&p(TXp(w2B)MagTy# zGw3(1ifvUGqRIS$cBCzoHFIxa+p!IEFT)QAn3h@6ovgjb;Hel45^ZG5m3@uDryo|F zHy*$6(QhhIeyq}$3OfW#f3NjSsXNq{J zU=>-0aGUqIaG)2RGh2=F8G@%C=Cmr2Bgxcxi>M*`tD07(%Fj61pk`9kF{0$H*Sg)H zgxV+P%G6|rp^{!TY`xSfjQZu&C_o+FMS||n0NpDVj&WaT76fTQl*S=ijnSLRgm3Ny z>?2RaB^v$iCJ)70sZZdc2bfen`E(uL{3i&xgNMt^A_gHp& zGE6>>G;yQ!`D9O=!f`ZQgc~E=cqcB=6W3Qqze>YJxCG&*I&o7M;k?|-?*283ogv(8 zC+>1j9Pf&&uIv42;8KK}YvUwLw{S~tBY*)lR7dz2qVNHN_cMg{9dG_A{CfD{QC9g+ KGeZjxX8!^QHu1Xv literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.java new file mode 100644 index 00000000000..c33e55278c1 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.java @@ -0,0 +1,43 @@ +public class Main { + public void toUpper() { + String str = "abcde"; + str = str.toUpperCase(); + assert str.equals("ABCDE"); + } + + public void noUpper() { + String str = "abcde"; + str = str.toUpperCase(); + assert !str.equals("ABCDe"); + } + + public void noprop(String str) { + str = str.toUpperCase(); + assert str.equals("ABCDE"); + } + + public void nondetArg(String str) { + str = "dave".toUpperCase(); + assert !str.equals(str); + } + + public void pi() { + assert "π".toUpperCase().equals("π"); + } + + public void nonAlpha() { + assert "^£&$1!".toUpperCase().equals("^£&$1!"); + } + + public void empty() { + assert "".toLowerCase().equals(""); + } + + public void emptyThis() { + assert !"".toUpperCase().equals("dave"); + } + + public void emptyArg() { + assert !"dave".toUpperCase().equals(""); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/empty.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/empty.desc new file mode 100644 index 00000000000..15b1a57602c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/empty.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.empty --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyArg.desc new file mode 100644 index 00000000000..279e22eb4bd --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyThis.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyThis.desc new file mode 100644 index 00000000000..7e85f448edb --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyThis.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyThis --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noUpper.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noUpper.desc new file mode 100644 index 00000000000..128636cf876 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noUpper.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noUpper --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nonAlpha.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nonAlpha.desc new file mode 100644 index 00000000000..49684c9e415 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nonAlpha.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nonAlpha --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nondetArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nondetArg.desc new file mode 100644 index 00000000000..93db2edb075 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nondetArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noprop.desc new file mode 100644 index 00000000000..27e95eab525 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noprop.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/pi.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/pi.desc new file mode 100644 index 00000000000..cbed1f44433 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/pi.desc @@ -0,0 +1,13 @@ +CORE +Main.class +--function Main.pi --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This is technically wrong (as pi has an uppercase) but our current implementation +only constant props things within the 0 - 128 range due to the tolower/toupper methods +currently being used. If this ever changes to be a true all-character case change, +just modify the test. \ No newline at end of file diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/toUpper.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/toUpper.desc new file mode 100644 index 00000000000..151488ea8b1 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/toUpper.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.toUpper --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index b8e2ccda24d..406b2fc8e09 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -211,6 +211,14 @@ bool goto_symext::constant_propagate_assignment_with_side_effects( { return constant_propagate_trim(state, symex_assign, f_l1); } + else if(func_id == ID_cprover_string_to_lower_case_func) + { + return constant_propagate_case_change(state, symex_assign, f_l1, false); + } + else if(func_id == ID_cprover_string_to_upper_case_func) + { + return constant_propagate_case_change(state, symex_assign, f_l1, true); + } } } @@ -927,6 +935,68 @@ bool goto_symext::constant_propagate_set_char_at( return true; } +bool goto_symext::constant_propagate_case_change( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1, + bool to_upper) +{ + const auto &f_type = to_mathematical_function_type(f_l1.function().type()); + const auto &length_type = f_type.domain().at(0); + const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype(); + + const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2)); + const auto s_data_opt = try_evaluate_constant_string(state, s.content()); + + if(!s_data_opt) + return false; + + array_exprt string_data = s_data_opt->get(); + + auto &operands = string_data.operands(); + for(auto &operand : operands) + { + auto &constant_value = to_constant_expr(operand); + auto character = numeric_cast_v(constant_value); + + // Can't guarantee matches against non-ASCII characters. + if(character >= 128) + return false; + + if(isalpha(character)) + { + if(to_upper) + { + if(islower(character)) + constant_value = + from_integer(toupper(character), constant_value.type()); + } + else + { + if(isupper(character)) + constant_value = + from_integer(tolower(character), constant_value.type()); + } + } + } + + const constant_exprt new_char_array_length = + from_integer(operands.size(), length_type); + + const array_typet new_char_array_type(char_type, new_char_array_length); + const array_exprt new_char_array(std::move(operands), new_char_array_type); + + assign_string_constant( + state, + symex_assign, + to_ssa_expr(f_l1.arguments().at(0)), + new_char_array_length, + to_ssa_expr(f_l1.arguments().at(1)), + new_char_array); + + return true; +} + bool goto_symext::constant_propagate_trim( statet &state, symex_assignt &symex_assign, diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index d0f6575faef..83b24979f34 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -663,6 +663,13 @@ class goto_symext symex_assignt &symex_assign, const function_application_exprt &f_l1); + /// Attempt to constant propagate case changes, both upper and lower. + bool constant_propagate_case_change( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1, + bool to_upper); + /// Assign constant string length and string data given by a char array to /// given ssa variables /// From 9e1f258110e972e0ab4c606dfdb2760cd5df180a Mon Sep 17 00:00:00 2001 From: johndumbell Date: Wed, 18 Sep 2019 14:50:05 +0100 Subject: [PATCH 4/6] Add String.lastIndexOf(...) --- .../ConstantEvaluationLastIndexOf/Main.class | Bin 0 -> 1065 bytes .../ConstantEvaluationLastIndexOf/Main.java | 26 +++++ .../lastIndexOf.desc | 9 ++ .../noIndex.desc | 9 ++ .../ConstantEvaluationLastIndexOf/noprop.desc | 9 ++ .../subsetIndex.desc | 9 ++ .../subsetNoIndex.desc | 9 ++ src/util/simplify_expr.cpp | 101 ++++++++++++------ 8 files changed, 142 insertions(+), 30 deletions(-) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/lastIndexOf.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/noIndex.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/noprop.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/subsetIndex.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/subsetNoIndex.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..61aea99c2ce00779a6a80420aa588038bc3c25af GIT binary patch literal 1065 zcma)(OK;Oa6ot>&N$fbz%W2Zkq(GrS(m=zbJ1QP3Af-*)MGz9*+0GET1Us@F#Bb?_ zC2K%xC6HjxZ$gMW&cosr5l8mSeSCAy+;2ZVeF3nAI~uaMpyFa08LX+eq~S8w6_{zd3xtknM%0{c_(NMOg(m7!=ow(u8!qk?)Nd%8l-^ z`Pys`O?S}lg}&ns?utV)!PpA;ghs5%?qJrgZrj7DCavdA0H$sH1=) z1x(AH{B`7zCqEV`(XoV0hH8BB!*}O3O%`B3V%0BJ&xk=Vws9 z3WO9Pa*$~))003QNt9`)f_+C_L50A}bMWpIT%Uo8(5{-Y_waXU;K(j<`nt~l*BtE simplify_string_compare_to( /// /// \param expr: the expression to simplify /// \param ns: namespace +/// \param search_from_end: return the last instead of the first index /// \return: the modified expression or an unchanged expression static simplify_exprt::resultt<> simplify_string_index_of( const function_application_exprt &expr, - const namespacet &ns) + const namespacet &ns, + const bool search_from_end) { std::size_t starting_index = 0; @@ -336,21 +338,19 @@ static simplify_exprt::resultt<> simplify_string_index_of( const array_exprt &s1_data = s1_data_opt->get(); - if(starting_index >= s1_data.operands().size()) + const auto search_string_size = s1_data.operands().size(); + if(starting_index >= search_string_size) { return from_integer(-1, expr.type()); } - // Iterator pointing to the character in the first string at which the second - // string or character was found - exprt::operandst::const_iterator it; - + unsigned long starting_offset = + starting_index > 0 ? (search_string_size - 1) - starting_index : 0; if(can_cast_expr(expr.arguments().at(1))) { // Second argument is a string - const refined_string_exprt &s2 = - to_string_expr(expr.arguments().at(1)); + const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1)); const auto s2_data_opt = try_get_string_data_array(s2.content(), ns); @@ -361,11 +361,41 @@ static simplify_exprt::resultt<> simplify_string_index_of( const array_exprt &s2_data = s2_data_opt->get(); - it = std::search( - std::next(s1_data.operands().begin(), starting_index), - s1_data.operands().end(), - s2_data.operands().begin(), - s2_data.operands().end()); + // Searching for empty string is a special case and is simply the + // "always found at the first searched position. This needs to take into + // account starting position and if you're starting from the beginning or + // end. + if(s2_data.operands().empty()) + return from_integer( + search_from_end + ? starting_index > 0 ? starting_index : search_string_size + : 0, + expr.type()); + + if(search_from_end) + { + auto end = std::prev(s1_data.operands().end(), starting_offset); + auto it = std::find_end( + s1_data.operands().begin(), + end, + s2_data.operands().begin(), + s2_data.operands().end()); + if(it != end) + return from_integer( + std::distance(s1_data.operands().begin(), it), expr.type()); + } + else + { + auto it = std::search( + std::next(s1_data.operands().begin(), starting_index), + s1_data.operands().end(), + s2_data.operands().begin(), + s2_data.operands().end()); + + if(it != s1_data.operands().end()) + return from_integer( + std::distance(s1_data.operands().begin(), it), expr.type()); + } } else if(expr.arguments().at(1).id() == ID_constant) { @@ -374,33 +404,40 @@ static simplify_exprt::resultt<> simplify_string_index_of( const constant_exprt &c1 = to_constant_expr(expr.arguments().at(1)); const auto c1_val = numeric_cast_v(c1); - auto pred = [&](const exprt &c2) - { + auto pred = [&](const exprt &c2) { const auto c2_val = numeric_cast_v(to_constant_expr(c2)); return c1_val == c2_val; }; - it = std::find_if( - std::next(s1_data.operands().begin(), starting_index), - s1_data.operands().end(), - pred); + if(search_from_end) + { + auto it = std::find_if( + std::next(s1_data.operands().rbegin(), starting_offset), + s1_data.operands().rend(), + pred); + if(it != s1_data.operands().rend()) + return from_integer( + std::distance(s1_data.operands().begin(), it.base() - 1), + expr.type()); + } + else + { + auto it = std::find_if( + std::next(s1_data.operands().begin(), starting_index), + s1_data.operands().end(), + pred); + if(it != s1_data.operands().end()) + return from_integer( + std::distance(s1_data.operands().begin(), it), expr.type()); + } } else { return simplify_exprt::unchanged(expr); } - if(it == s1_data.operands().end()) - { - return from_integer(-1, expr.type()); - } - else - { - const std::size_t idx = std::distance(s1_data.operands().begin(), it); - - return from_integer(idx, expr.type()); - } + return from_integer(-1, expr.type()); } /// Simplify String.charAt function when arguments are constant @@ -546,7 +583,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_function_application( } else if(func_id == ID_cprover_string_index_of_func) { - return simplify_string_index_of(expr, ns); + return simplify_string_index_of(expr, ns, false); } else if(func_id == ID_cprover_string_char_at_func) { @@ -556,6 +593,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_function_application( { return simplify_string_contains(expr, ns); } + else if(func_id == ID_cprover_string_last_index_of_func) + { + return simplify_string_index_of(expr, ns, true); + } return unchanged(expr); } From 79882c606329d9b094f42a0dd9e535bc3db63629 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Wed, 25 Sep 2019 11:55:55 +0100 Subject: [PATCH 5/6] Add String.replace(...) --- .../ConstantEvaluationReplace/Main.class | Bin 0 -> 2641 bytes .../ConstantEvaluationReplace/Main.java | 90 ++++++++++++++ .../fullReplace.desc | 9 ++ .../ConstantEvaluationReplace/noReplace.desc | 9 ++ .../nopropReplace.desc | 9 ++ .../notEqualsReplace.desc | 9 ++ .../randomCharReplace.desc | 9 ++ .../randomCharsReplace.desc | 9 ++ .../ConstantEvaluationReplace/replace.desc | 9 ++ .../stringFullReplace.desc | 9 ++ .../stringLargerReplace.desc | 9 ++ .../stringMultiLargerReplace.desc | 9 ++ .../stringMultiReplace.desc | 9 ++ .../stringMultiSmallerReplace.desc | 9 ++ .../stringNoReplace.desc | 9 ++ .../stringReplace.desc | 9 ++ .../stringSmallerReplace.desc | 9 ++ src/goto-symex/goto_symex.cpp | 112 ++++++++++++++++++ src/goto-symex/goto_symex.h | 6 + 19 files changed, 343 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/fullReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/noReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/nopropReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/notEqualsReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/randomCharReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/randomCharsReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/replace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringFullReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringLargerReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringMultiLargerReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringMultiReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringMultiSmallerReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringNoReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringReplace.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringSmallerReplace.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..bdc0dee456f6879cab3e3fdc85b7d5952961d79e GIT binary patch literal 2641 zcma)-*-{%v6o&uSf?7f#X;_Q{IBYRsw#3GXZ3u=4aAHf?Mi?8ij%EfSA|x`Ba>1K~ z7sz#zDqQ7MCHHxzR4RYZfHWW>Gg3`=pVNK5K1=uf^WVF_0L&v7!4Q@t9!Ic@l`wAM z3yGu}tcI`_K}adrC7wupDe;w3Je7DRk&;MDY)Cwpcp>ppVpAd`u_f_JVq4<1#2bkn ziQN#sj^G=78^U)2U1NH=Y}u83saRgkm-TGHG6lr0K-*%zn6E4e_$MZ}1p>*EX$izq z`J%N^JOxlF~*7jp~BNJrV} z*XG6C@kV_I-L52as22)WeG^@-IHlV;k5qG|>1v^pui3om5neXa=h0oVm2g$-)k2|W zs(sHpl8Z*+ECrEFscIY6dR_%QoYwQjS>RHn=8Sf~@@k12D7;%J#WkjJP zE6`Vu&dPbZ*KE6FpDi}r`6|IerJw7@L7~_a@aZ%V*dswTx%~sCTs4lMP0t#pn&8Xr zvt)AnhN(Kz6&uRdG3CdG$v@X0vp@u*s-ehv6J1dcwK^XK;loC`8G;#w1rFnN7oKMi zEQ9ksqKuPgfnHT0jkUlnSWXoRTqqUS(!wOmebrk+svt95VHFK)!DH@%yeTJE-)6GF zqs1+mRyl85W-ahMC6y`_JXgES)h(WQK*al0-q=e(sI>C^5l4e;1>4}Aw-CRniMY*o zn0w?I6(t@XGJ3;%O2<^Ou{99S_IhHg8*!S}n zKomiu+b}_ig!mVuAxx5S=X#7V8NXc32$K;Zqn(Us17oTQBSJrpFZvN_?MIA^IISnh z&>9%in4vc+tgjr8fl)1zo{sDN3{~0<)wK2=L=Ttt(uo_)R$m=4;)ZG#b7zPx&QqZs z(IOi&{R1RyxP+Pa5&F4ufT0?6s-u>SVVCeRJ~<;iFWxZl9Ie4Az%WEGs> r`|~`J>Pcv~PVwOhLV;fq@c)58{pLRZ2Bget().type()); + array_exprt characters_to_replace(s_data_opt->get().type()); + + // Two main ways to perform a replace: characters or strings. + bool is_single_character = new_data.type().id() == ID_unsignedbv && + old_data.type().id() == ID_unsignedbv; + if(is_single_character) + { + const auto new_char_pointer = try_evaluate_constant(state, new_data); + const auto old_char_pointer = try_evaluate_constant(state, old_data); + + if(!new_char_pointer || !old_char_pointer) + { + return {}; + } + + characters_to_find.operands().emplace_back(old_char_pointer->get()); + characters_to_replace.operands().emplace_back(new_char_pointer->get()); + } + else + { + auto &new_char_array = to_string_expr(new_data); + auto &old_char_array = to_string_expr(old_data); + + const auto new_char_array_opt = + try_evaluate_constant_string(state, new_char_array.content()); + + const auto old_char_array_opt = + try_evaluate_constant_string(state, old_char_array.content()); + + if(!new_char_array_opt || !old_char_array_opt) + { + return {}; + } + + characters_to_find = old_char_array_opt->get(); + characters_to_replace = new_char_array_opt->get(); + } + + // Copy data, then do initial search for a replace sequence. + array_exprt existing_data = s_data_opt->get(); + auto found_pattern = std::search( + existing_data.operands().begin(), + existing_data.operands().end(), + characters_to_find.operands().begin(), + characters_to_find.operands().end()); + + // If we've found a match, proceed to perform a replace on all instances. + while(found_pattern != existing_data.operands().end()) + { + // Find the difference between our first/last match iterator. + auto match_end = found_pattern + characters_to_find.operands().size(); + + // Erase them. + found_pattern = existing_data.operands().erase(found_pattern, match_end); + + // Insert our replacement characters, then move the iterator to the end of + // our new sequence. + found_pattern = existing_data.operands().insert( + found_pattern, + characters_to_replace.operands().begin(), + characters_to_replace.operands().end()) + + characters_to_replace.operands().size(); + + // Then search from there for any additional matches. + found_pattern = std::search( + found_pattern, + existing_data.operands().end(), + characters_to_find.operands().begin(), + characters_to_find.operands().end()); + } + + const constant_exprt new_char_array_length = + from_integer(existing_data.operands().size(), length_type); + + const array_typet new_char_array_type(char_type, new_char_array_length); + const array_exprt new_char_array( + std::move(existing_data.operands()), new_char_array_type); + + assign_string_constant( + state, + symex_assign, + to_ssa_expr(f_l1.arguments().at(0)), + new_char_array_length, + to_ssa_expr(f_l1.arguments().at(1)), + new_char_array); + + return true; +} + bool goto_symext::constant_propagate_trim( statet &state, symex_assignt &symex_assign, diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 83b24979f34..316f9530b76 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -670,6 +670,12 @@ class goto_symext const function_application_exprt &f_l1, bool to_upper); + /// Attempt to constant proagate character replacement. + bool constant_propagate_replace( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1); + /// Assign constant string length and string data given by a char array to /// given ssa variables /// From db1f84488305fa3578f61cdc4ebdd405a44c28ff Mon Sep 17 00:00:00 2001 From: johndumbell Date: Wed, 25 Sep 2019 15:14:15 +0100 Subject: [PATCH 6/6] Add String.equalsIgnoreCase() --- .../Main.class | Bin 0 -> 1644 bytes .../Main.java | 49 ++++++++++++ .../empty.desc | 9 +++ .../emptyArg.desc | 9 +++ .../emptyThis.desc | 9 +++ .../equals.desc | 9 +++ .../longEquals.desc | 9 +++ .../nonAlpha.desc | 9 +++ .../nondetArg.desc | 9 +++ .../nondetString.desc | 9 +++ .../noprop.desc | 9 +++ .../notEqual.desc | 9 +++ .../pi.desc | 9 +++ .../shortEquals.desc | 9 +++ src/util/simplify_expr.cpp | 73 ++++++++++++++++++ 15 files changed, 230 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/empty.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyArg.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyThis.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/equals.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/longEquals.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nonAlpha.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetArg.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetString.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/noprop.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/notEqual.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/pi.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/shortEquals.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..c45d60b5ae295e077c8d9226afbbaf15385f3b38 GIT binary patch literal 1644 zcmaiz%}*0S7{;I3e(ZL4p=J3h0s>N@P^6&v2_mIJVgh=An8?9o+iuEY*)6+U3^)G` zxq9%dCXi^NiAOK~N5*%yl-9&u_Aom$?>oPFo_A(`{rUPGz!C~FdN7kf60;I=66R#w z!n}yQj5uZ_EJ#?Ca9hG12}=_0O1LNDzKjQWDB=-AZ$@`r!|_bpa-W*6UaA=t2DZl# zUokDyTV;r3XI?Tyi+06eNN$;y@w{^eh#cI!Yt*7G&ps^)h*$F!=;oG#aFtLi5cNOAXVr@53ys%2Xh!)qopB$~s5 zQ)Lk9CIf9_6>9Z;ogro%*1Z$T@&CK~CM}ozzMn3wlxr8BwEzW(`PDziAj01EJZMXaiLf;EOz8~&nnV3fUords|}&2m4hTDD^pb(hHh zEh?R0vJEWO=$IJ>Du!!1M&(jG9hujl0G;t3Cg>LR(5+&rG%o@5x=AHfgxUcbjnbcl zBQ|>u_K7EAklMIE$wTSO)Kv)n?9gWjr|8!rTJ#LDQz+jMe{~M=2VXAu%Vqil5n3F@ zkl$lzT6-;!CHbuP!7PzjQYUK|BShpD9@A!gyR@&XFL#wJg(Rvi)F44dLu4h$Vu-9H z$x5|Y+~V~RmK@INC01W2Yb@BJ5{?=qi|H1MTO1EUX-X~}HB6|HPSix8Lsh#%))-vJ_ue$nDA# vYoX1OFm=gVqU!OlM@ya|bqX>15z)vO2<=DMdc*ty#vrI`{5en4KtT2{X@dYj literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.java new file mode 100644 index 00000000000..71ba6076a14 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.java @@ -0,0 +1,49 @@ +public class Main { + public void equals() { + assert "abc".equalsIgnoreCase("ABC"); + } + + public void notEqual() { + assert !"abce".equalsIgnoreCase("ABC"); + } + + public void noprop(String val) { + assert val.equalsIgnoreCase("ABC"); + } + + public void longEquals() { + assert !"abce".equalsIgnoreCase("qwertyuiops"); + } + + public void shortEquals() { + assert !"abce".equalsIgnoreCase("BF"); + } + + public void nondetString(String str) { + assert !str.equalsIgnoreCase("dave"); + } + + public void nondetArg(String str) { + assert !"dave".equalsIgnoreCase(str); + } + + public void pi() { + assert !"π".equalsIgnoreCase("dave"); + } + + public void nonAlpha() { + assert "^£&$1!".equalsIgnoreCase("^£&$1!"); + } + + public void empty() { + assert "".equalsIgnoreCase(""); + } + + public void emptyThis() { + assert !"".equalsIgnoreCase("dave"); + } + + public void emptyArg() { + assert !"dave".equalsIgnoreCase(""); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/empty.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/empty.desc new file mode 100644 index 00000000000..15b1a57602c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/empty.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.empty --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyArg.desc new file mode 100644 index 00000000000..279e22eb4bd --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyThis.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyThis.desc new file mode 100644 index 00000000000..7e85f448edb --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyThis.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyThis --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/equals.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/equals.desc new file mode 100644 index 00000000000..c33e7b70399 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/equals.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.equals --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/longEquals.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/longEquals.desc new file mode 100644 index 00000000000..28c88ee03d8 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/longEquals.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.longEquals --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nonAlpha.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nonAlpha.desc new file mode 100644 index 00000000000..49684c9e415 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nonAlpha.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nonAlpha --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetArg.desc new file mode 100644 index 00000000000..93db2edb075 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetString.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetString.desc new file mode 100644 index 00000000000..a59296a5206 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetString.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nondetString --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/noprop.desc new file mode 100644 index 00000000000..27e95eab525 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/noprop.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/notEqual.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/notEqual.desc new file mode 100644 index 00000000000..f6941d4447c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/notEqual.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.notEqual --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/pi.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/pi.desc new file mode 100644 index 00000000000..6e626865b5d --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/pi.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.pi --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/shortEquals.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/shortEquals.desc new file mode 100644 index 00000000000..b0a227bbcd1 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/shortEquals.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.shortEquals --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index ed35f87be21..8b3665df30b 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -484,6 +484,75 @@ static simplify_exprt::resultt<> simplify_string_char_at( return c; } +/// Take the passed-in constant string array and lower-case every character. +static bool lower_case_string_expression(array_exprt &string_data) +{ + auto &operands = string_data.operands(); + for(auto &operand : operands) + { + auto &constant_value = to_constant_expr(operand); + auto character = numeric_cast_v(constant_value); + + // Can't guarantee matches against non-ASCII characters. + if(character >= 128) + return false; + + if(isalpha(character)) + { + if(isupper(character)) + constant_value = + from_integer(tolower(character), constant_value.type()); + } + } + + return true; +} + +/// Simplify String.equalsIgnorecase function when arguments are constant +/// +/// \param expr: the expression to simplify +/// \param ns: namespace +/// \return: the modified expression or an unchanged expression +static simplify_exprt::resultt<> simplify_string_equals_ignore_case( + const function_application_exprt &expr, + const namespacet &ns) +{ + // We want to get both arguments of any starts-with comparison, and + // trace them back to the actual string instance. All variables on the + // way must be constant for us to be sure this will work. + auto &first_argument = to_string_expr(expr.arguments().at(0)); + auto &second_argument = to_string_expr(expr.arguments().at(1)); + + const auto first_value_opt = + try_get_string_data_array(first_argument.content(), ns); + + if(!first_value_opt) + { + return simplify_exprt::unchanged(expr); + } + + array_exprt first_value = first_value_opt->get(); + + const auto second_value_opt = + try_get_string_data_array(second_argument.content(), ns); + + if(!second_value_opt) + { + return simplify_exprt::unchanged(expr); + } + + array_exprt second_value = second_value_opt->get(); + + // Just lower-case both expressions. + if( + !lower_case_string_expression(first_value) || + !lower_case_string_expression(second_value)) + return simplify_exprt::unchanged(expr); + + bool is_equal = first_value == second_value; + return from_integer(is_equal ? 1 : 0, expr.type()); +} + /// Simplify String.startsWith function when arguments are constant /// /// \param expr: the expression to simplify @@ -597,6 +666,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_function_application( { return simplify_string_index_of(expr, ns, true); } + else if(func_id == ID_cprover_string_equals_ignore_case_func) + { + return simplify_string_equals_ignore_case(expr, ns); + } return unchanged(expr); }