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>

1 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index b410670e5..eaf016862 100644
--- 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);