Fix out-of-bounds access in regexp inclusion test (#3242)

If `re.*(re.allchar)` was at the end of a regular expression
concatenation, the regular expression inclusion test could cause
out-of-bound accesses. For `re.*(re.allchar)`, we were blindly adding
the index after it to the set of indices being considered. Later in the
loop, we were assuming that all the indices are smaller than the number
of components in the concatenation, thus leading to out-of-bound
accesses. This commit adds a check before adding the index to the set of
indices.

Signed-off-by: Andres Noetzli <andres.noetzli@gmail.com>

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index b410670e56d9514d2ce7fac9b679e69a83fbdd49..eaf0168622003b30cc1b371c502cc1ec2bb8fbf6 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1687,15 +1687,15 @@ bool RegExpOpr::regExpIncludes(Node r1, Node r2)
   for (const Node& n2 : v2)
   {
     // Transfer elements from `newIdxs` to `idxs`. Out-of-bound indices are
-    // removed and for (re.* re.allchar), we additionally include the
-    // option of skipping it.
+    // removed and for (re.* re.allchar), we additionally include the option of
+    // skipping it. Indices must be smaller than the size of `v1`.
     idxs.clear();
     for (size_t idx : newIdxs)
     {
       if (idx < v1.size())
       {
         idxs.insert(idx);
-        if (v1[idx] == d_sigma_star)
+        if (idx + 1 < v1.size() && v1[idx] == d_sigma_star)
         {
           Assert(idx + 1 == v1.size() || v1[idx + 1] != d_sigma_star);
           idxs.insert(idx + 1);