Symbolic Regex Support

[pschanely]

This is a growing list of regex capabilities that CrossHair supports with symbolic execution.

Like Z3, CrossHair won't do much with analysis over a symbolic regex pattern - only symbolic strings tested against a concrete pattern.

• [x] Literal character matching
• [x] Repetitions + * {n, m}
• [x] Unions ( ... | ... )
• [x] Builtin character classes: \w \W \s \S \d \D
• [x] Explicit character classes [...]
• [x] Negated character classes [^...]
• [x] Groups
• [x] Named groups
• [ ] Regex over symbolic bytes (as opposed to symbolic strings)
• [x] Flag: re.IGNORECASE
• [x] Flag: re.ASCII
• [x] Flag: re.DOTALL
• [ ] Flag: re.LOCALE (deprecated Python feature, likely won't bother)
• [X] Zero-width matchers (\A ^ \b \B $ \Z)
• [X] Non-greedy matching (+? *? ?? {n, m}?)
• [X] Backreferences to capture groups
• [X] negative/positive lookahead
• [X] negative/positive lookbehind