Support Unicode-aware regex (#4365)

Closes #4357

Convert K Unicode-based regex to an equivalent Flex byte-based regex:
- Outside of a character class, just parenthesize to keep the bytes
grouped
   - `r"😊*"` becomes `r"(\xF0\x9F\x98\x8A)*"`
- Inside a non-negated character class, factor any single Unicode
character out into an explicit `|`
    - `r"[a😊b]"` becomes `r"(\xF0\x9F\x98\x8A)|[ab]"`
- In all other cases (character ranges and negated character classes),
report an error if there are non-ASCII characters

Additionally,
- Check that character ranges `[c1-c2]` have `codepoint(c1) <=
codepoint(c2)`
- Check that numeric ranges `r{n,m}` have `n <= m`

The commit history is incremental, and I'd recommend reviewing
commit-by-commit.

---------

Co-authored-by: Bruce Collie <[email protected]>

k-distribution/tests/regression-new/checks/checkRegexRanges.k

@@ -0,0 +1,8 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module CHECKREGEXRANGES
+syntax lexical Foo = r"a|[1-#]b"
+syntax Bar ::= r"a|[1-#]b"
+
+syntax lexical Baz = r"(a|b|c){100,1}"
+syntax Buz ::= r"(a|b|c){100,1}"
+endmodule

k-distribution/tests/regression-new/checks/checkRegexRanges.k.out

@@ -0,0 +1,21 @@
+[Error] Outer Parser: Invalid character range '1-#'. Start of range U+0031 is greater than end of range U+0023.
+	Source(checkRegexRanges.k)
+	Location(3,1,3,33)
+	3 |	syntax lexical Foo = r"a|[1-#]b"
+	  .	^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Outer Parser: Invalid character range '1-#'. Start of range U+0031 is greater than end of range U+0023.
+	Source(checkRegexRanges.k)
+	Location(4,16,4,27)
+	4 |	syntax Bar ::= r"a|[1-#]b"
+	  .	               ^~~~~~~~~~~
+[Error] Outer Parser: Invalid numeric range '(a|(b|c)){100,1}'. Start of range 100 is greater than end of range 1.
+	Source(checkRegexRanges.k)
+	Location(6,1,6,39)
+	6 |	syntax lexical Baz = r"(a|b|c){100,1}"
+	  .	^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Outer Parser: Invalid numeric range '(a|(b|c)){100,1}'. Start of range 100 is greater than end of range 1.
+	Source(checkRegexRanges.k)
+	Location(7,16,7,33)
+	7 |	syntax Buz ::= r"(a|b|c){100,1}"
+	  .	               ^~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 4 parsing errors.

k-distribution/tests/regression-new/checks/checkRegexUnicode.k

@@ -0,0 +1,5 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module CHECKREGEXUNICODE
+syntax lexical Foo = r"[^a😊][😦-ab-🙁]"
+syntax Bar ::= r"[^a😊][😦-ab-🙁]" [token]
+endmodule

k-distribution/tests/regression-new/checks/checkRegexUnicode.k.out

@@ -0,0 +1,31 @@
+[Error] Outer Parser: Invalid character range '😦-a'. Start of range U+1F626 is greater than end of range U+0061.
+	Source(checkRegexUnicode.k)
+	Location(3,1,3,41)
+	3 |	syntax lexical Foo = r"[^a😊][😦-ab-🙁]"
+	  .	^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Outer Parser: Unsupported non-ASCII characters found in character class range: [😦, 🙁]
+	Source(checkRegexUnicode.k)
+	Location(3,1,3,41)
+	3 |	syntax lexical Foo = r"[^a😊][😦-ab-🙁]"
+	  .	^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Outer Parser: Unsupported non-ASCII characters found in negated character class: [😊]
+	Source(checkRegexUnicode.k)
+	Location(3,1,3,41)
+	3 |	syntax lexical Foo = r"[^a😊][😦-ab-🙁]"
+	  .	^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Outer Parser: Invalid character range '😦-a'. Start of range U+1F626 is greater than end of range U+0061.
+	Source(checkRegexUnicode.k)
+	Location(4,16,4,43)
+	4 |	syntax Bar ::= r"[^a😊][😦-ab-🙁]" [token]
+	  .	               ^~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Outer Parser: Unsupported non-ASCII characters found in character class range: [😦, 🙁]
+	Source(checkRegexUnicode.k)
+	Location(4,16,4,43)
+	4 |	syntax Bar ::= r"[^a😊][😦-ab-🙁]" [token]
+	  .	               ^~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Outer Parser: Unsupported non-ASCII characters found in negated character class: [😊]
+	Source(checkRegexUnicode.k)
+	Location(4,16,4,43)
+	4 |	syntax Bar ::= r"[^a😊][😦-ab-🙁]" [token]
+	  .	               ^~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 6 parsing errors.

k-distribution/tests/regression-new/regex-unicode/1.test

@@ -0,0 +1 @@
+😊🙁

k-distribution/tests/regression-new/regex-unicode/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  😊😦😦 ~> .K
+</k>

k-distribution/tests/regression-new/regex-unicode/Makefile

@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/regex-unicode/test.k

@@ -0,0 +1,13 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module TEST-SYNTAX
+syntax lexical Emote = r"😊?[😦🙁]+"
+
+syntax Emoji ::= r"{Emote}" [token]
+
+endmodule
+
+module TEST
+imports TEST-SYNTAX
+configuration <k> $PGM:Emoji </k>
+rule <k>😊🙁 => 😊😦😦</k>
+endmodule