Understanding Python Regular Expression Modeling using Z3

[swag2198]

Hi Phillip,
I am here following your very informative blogpost on modeling python regular expressions using z3.

I am working on a problem that requires me to get z3 regular expressions for arbitrary python re expressions. I was looking into this awesome parser that you wrote for the same purpose. Thank you so much for this helpful parser and the reference to sre_parse.

I had a couple of questions:

1. I see that _handle_seq() is the main functionality and it takes an argument flags which is 0 most of the time. But in some cases in the then crosshair/libimpl/relib_test.py file, I see it taking the value re.A. Could you clarify the purpose of the flag argument here?

2. I understood the groups greediness example that is missing in z3. I also see that you are currently not using z3 based regular expressions in the current version of crosshair. But as far as I understand, I can model every regular expression without such ambiguous/overlapping groups using z3. For example, I think I can use (?: to tell the regex to not match/store subpatterns and get the desired z3 model. I tried with the code and it gave the following z3 regex:

z3re = _handle_seq(sre_parse.parse('M(?:r|s|rs)abc(?:x|y|z)'), 0)
print(z3.simplify(z3re))

re.++(Re("M"),
      re.++(Union(Re("r"), Union(Re("s"), Re("rs"))),
            re.++(Re("a"),
                  re.++(Re("b"),
                        re.++(Re("c"),
                              Union(Re("x"),
                                    Union(Re("y"), Re("z"))))))))

Could you comment on this if my understanding is correct, and if there were any other pressing issues you faced while trying to use z3 regex primitives?

Thank you so much for your time.

[pschanely]

I'm glad this has been helpful for you!

1. The flags argument corresponds to argument of the same name that many regex functions take (e.g. re.compile(pattern, flags)). It's important because many of the flags impact how to interpret the regex.
2. CrossHair attempts to faithfully reproduce all the regex capabilities, but it sounds like you only need to detect whether a match exists? In that case, yes, you are much more likely to be successful using the native z3 regex capabilities.

Other things to watch out for: Can you limit yourself to ASCII? Modern versions of z3 support unicode, but it's fairly recent and probably not super stable. I recall having some trouble with unicode over the Python bindings last year, though not the specifics. You may also run into difficulty supporting character classes like \w and \d over unicode. (z3 won't help you here, so you've got to specify the entire class somehow)

Hope this helps, and good luck on your project!

[swag2198]

Yes, I just want to find if a string is a match to a (z3) regex and I don't care about the group pattern matches. Okay, so since you were trying to replicate all regex capabilities, you had to move beyond z3 in CrossHair. Great!

And you are right. I did face problems while trying to handle regexes having \w, \d, \s, etc. Nonetheless, I can handle those cases separately and your code is a really good starting point for me.

Thanks for your helpful comments!