From 985684ac70c80e8e2bfdce9e64c303cce0405ebd Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 6 Dec 2017 13:10:31 +0000
Subject: [PATCH 1/2] Prevent overflow with argument of lastIndexOf

---
 src/solvers/refinement/string_constraint_generator_indexof.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 11067029b5a..27f7e96bfb7 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -348,7 +348,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   axioms.push_back(a3);
 
   const exprt index1 = from_integer(1, index_type);
-  const plus_exprt from_index_plus_one(from_index, index1);
+  const exprt from_index_plus_one =
+    plus_exprt_with_overflow_check(from_index, index1);
   const if_exprt end_index(
     binary_relation_exprt(from_index_plus_one, ID_le, str.length()),
     from_index_plus_one,

From 3ab853ec23e60c9b6c45df25ad3e61268513b4eb Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 6 Dec 2017 13:05:15 +0000
Subject: [PATCH 2/2] Test comparing jbmc lastIndexOf with loop version

---
 .../VerifStringLastIndexOf/Test.class         | Bin 0 -> 886 bytes
 .../VerifStringLastIndexOf/Test.java          |  27 ++++++++++++++++++
 .../VerifStringLastIndexOf/test.desc          |   7 +++++
 3 files changed, 34 insertions(+)
 create mode 100644 regression/jbmc-strings/VerifStringLastIndexOf/Test.class
 create mode 100644 regression/jbmc-strings/VerifStringLastIndexOf/Test.java
 create mode 100644 regression/jbmc-strings/VerifStringLastIndexOf/test.desc

diff --git a/regression/jbmc-strings/VerifStringLastIndexOf/Test.class b/regression/jbmc-strings/VerifStringLastIndexOf/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..12663adb2783f83a973a204e2984045fb44a827d
GIT binary patch
literal 886
zcmY*X%Wl&^6g`uS?ZkDSt<yjpN}-QDpoOaHh6+&ykRlbjNQFc;mE%ksx2c0{7x4jn
zMOlE@bkhwWr4mT6=U4ax1e81OBVbE2_s%`{o_o*C_dlP%0$9e94g;2sGOp>+F(s|*
z(wdgmjU-t&HO%Npz|t_QV-E8gDh%T@b`S_ZbO&DW&<*TPUvwE*n?YT5JvY415U*69
zG4RHqD;P5Ct|y)z?01B}DZvbheLL)J?Yka>QfW4;O@>q}w4J>t_KS1KgfF&*FFZ%A
z+d<g$y5iNwHp66Peb;_zFZOM3XR#IfuD5fq5fxCJo^bZ4_NvoA??P`44tz&Eb|q(W
zQv~6HOg4}~RzuZ54Rr(Km@se)w+$39X<$LRDWn;SBc`>Bfgkz)z^BP%F%63b?%*y%
zc7)vM><TCR@93;eQl~Gxov;_FLldh`&-T{{$}7!kgJG=y@1U7c$p!@ihC){at}nWm
zy^vzz0R>3xHm2#i47yjAEz0i6Qb5upOKXn2GVM&B)=t1aNFegGs?nhgkqop-=n`Ux
z)1E9@@1c~Atz&Xx5j-6QRI07fpM*(~IG9G6B;I-c7B~Tb`C7R?M2vTbh_7&yzd@mH
z@*%kO4ywtIU-Q$W(;u->^+J@EBBnGf>V1kPnI%uM=!pM9isgPra}_Vi+C-*OyjrVU
z<sp<69_{Li@)6o0@+LQxw;20^#Pbs*znRL2E>EeTzLQieha$c2D-jh<^BZ%Fo)R5g
o=(kM6$uF1JhZsAA#*e_`pP)%C&&0XVQnsrgW;~FxUX8+~zlT$oeE<Le

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/VerifStringLastIndexOf/Test.java b/regression/jbmc-strings/VerifStringLastIndexOf/Test.java
new file mode 100644
index 00000000000..4f3fe7db63d
--- /dev/null
+++ b/regression/jbmc-strings/VerifStringLastIndexOf/Test.java
@@ -0,0 +1,27 @@
+public class Test {
+  // This compares the model of indexOf to an implementation
+  // using loops
+
+  public int math_min(int i, int j) {
+    if (i < j)
+      return i;
+    else
+      return j;
+  }
+
+  public int referenceLastIndexOf(String s, char ch, int fromIndex) {
+    for (int i = math_min(fromIndex, s.length() - 1); i >= 0; i--) {
+      if (s.charAt(i) == ch) {
+        return i;
+      }
+    }
+    return -1;
+  }
+
+  public int check(String s, char ch, int fromIndex) {
+    int reference = referenceLastIndexOf(s, ch, fromIndex);
+    int jbmc_result = s.lastIndexOf(ch, fromIndex);
+    assert(reference == jbmc_result);
+    return jbmc_result;
+  }
+}
diff --git a/regression/jbmc-strings/VerifStringLastIndexOf/test.desc b/regression/jbmc-strings/VerifStringLastIndexOf/test.desc
new file mode 100644
index 00000000000..5f238b0d996
--- /dev/null
+++ b/regression/jbmc-strings/VerifStringLastIndexOf/test.desc
@@ -0,0 +1,7 @@
+THOROUGH
+Test.class
+--function Test.check --refine-strings --string-max-length 50 --unwind 50 --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 32 .* SUCCESS$
+assertion at file Test.java line 34 .* FAILURE$