From 9cf54879c228c898efd62e8b9671defe5f37bc47 Mon Sep 17 00:00:00 2001 From: CUIZEWEN <57898114+CuiZewen@users.noreply.github.com> Date: Wed, 10 Jun 2020 16:05:22 +0800 Subject: [PATCH 1/3] add non-greedy(.*?) --- src/test/scala/lms/verify/RegexTests.scala | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/test/scala/lms/verify/RegexTests.scala b/src/test/scala/lms/verify/RegexTests.scala index f90edd1..0c512e3 100644 --- a/src/test/scala/lms/verify/RegexTests.scala +++ b/src/test/scala/lms/verify/RegexTests.scala @@ -27,6 +27,8 @@ trait StagedRegexpMatcher extends Dsl { true else if (regexp(restart)=='$' && restart+1==regexp.length) start==text.length + else if (restart+2 < regexp.length && regexp(restart+1)=='*' && regexp(restart+2)=='?') + matchstarquery(regexp(restart), regexp, restart+3, text, start) else if (restart+1 < regexp.length && regexp(restart+1)=='*') matchstar(regexp(restart), regexp, restart+2, text, start) else if (start < text.length && matchchar(regexp(restart), text(start))) @@ -48,6 +50,18 @@ trait StagedRegexpMatcher extends Dsl { !failed && found } + def matchstarquery(c: Char, regexp: String, restart: Int, text: Rep[String], start: Rep[Int]): Rep[Boolean] = { + var sqstart = start + var found = matchhere(regexp, restart, text, sqstart) + var failed = false + loop (start <= sqstart && sqstart <= text.length, List[Any](sqstart, found, failed), text.length-sqstart){ + if(!failed && !found && sqstart < text.length) { + failed = !matchchar(c, text(sqstart)) + found = matchhere(regexp, restart, text, sqstart) + }} + !failed && found + } + def matchchar(c: Char, t: Rep[Char]): Rep[Boolean] = { c == '.' || c == t } @@ -76,6 +90,8 @@ class RegexTests extends TestSuite { gen("a_end", "a$") gen("a", "a") gen("ab_dot_star_ab", "ab.*ab") + gen("ab_dot_star_query_ab","ab.*?ab") + // exponential code size!!! /* cloc -by-file re_alpha_*.actual.c @@ -99,7 +115,7 @@ SUM: 0 10260 114256 var r = "" for (i <- 0 until 10) { val c = ('a'+i).toChar - r = r+c+c+"*" + r = r+c+c+"*"+"?" //gen("alpha_"+c, r) } } From 2e6ecc931792477f52105d87a183ce10f90a355f Mon Sep 17 00:00:00 2001 From: CUIZEWEN <57898114+CuiZewen@users.noreply.github.com> Date: Wed, 10 Jun 2020 16:10:29 +0800 Subject: [PATCH 2/3] add non-greedy(.*?) --- src/out/re_ab_dot_star_query_ab.actual.c | 135 +++++++++++++++++++++++ 1 file changed, 135 insertions(+) create mode 100644 src/out/re_ab_dot_star_query_ab.actual.c diff --git a/src/out/re_ab_dot_star_query_ab.actual.c b/src/out/re_ab_dot_star_query_ab.actual.c new file mode 100644 index 0000000..a937437 --- /dev/null +++ b/src/out/re_ab_dot_star_query_ab.actual.c @@ -0,0 +1,135 @@ +#include +#include +/*@ +requires ((strlen(x0)>=0) && +\valid(x0+(0..strlen(x0)))); +*/ +int matcher(char * x0) { + int x2 = -1; + int x3 = 0/*false*/; + int x7 = strlen(x0); + /*@ + loop invariant ((-1<=x2) && + (x2<=x7)); + loop assigns x2, x3; + loop variant (x7-x2); + */ + for (;;) { + int x4 = x3; + int x10; + if (x4) { + x10 = 0/*false*/; + } else { + int x6 = x2; + int x8 = x6 < x7; + x10 = x8; + } + if (!x10) break; + x2 += 1; + int x13 = x2; + int x14 = x13 < x7; + int x17; + if (x14) { + char x15 = x0[x13]; + int x16 = 'a' == x15; + x17 = x16; + } else { + x17 = 0/*false*/; + } + int x72; + if (x17) { + int x18 = x13 + 1; + int x19 = x18 < x7; + int x22; + if (x19) { + char x20 = x0[x18]; + int x21 = 'b' == x20; + x22 = x21; + } else { + x22 = 0/*false*/; + } + int x71; + if (x22) { + int x23 = x18 + 1; + int x24 = x23; + int x25 = x24; + int x26 = x25 < x7; + int x29; + if (x26) { + char x27 = x0[x25]; + int x28 = 'a' == x27; + x29 = x28; + } else { + x29 = 0/*false*/; + } + int x37; + if (x29) { + int x30 = x25 + 1; + int x31 = x30 < x7; + int x34; + if (x31) { + char x32 = x0[x30]; + int x33 = 'b' == x32; + x34 = x33; + } else { + x34 = 0/*false*/; + } + int x36; + if (x34) { + x36 = 1/*true*/; + } else { + x36 = 0/*false*/; + } + x37 = x36; + } else { + x37 = 0/*false*/; + } + int x38 = x37; + int x39 = 0/*false*/; + int x40 = x39; + int x45; + if (x40) { + x45 = 0/*false*/; + } else { + int x42 = x38; + int x43 = !x42; + x45 = x43; + } + int x46; + if (x45) { + x46 = x26; + } else { + x46 = 0/*false*/; + } + /*@ + loop invariant ((x23<=x24) && + (x24<=x7)); + loop assigns x24, x38, x39; + loop variant (x7-x24); + */ + if (x46) { + x39 = 0/*false*/; + x38 = x37; + } else { + } + int x65 = x39; + int x69; + if (x65) { + x69 = 0/*false*/; + } else { + int x67 = x38; + x69 = x67; + } + x71 = x69; + } else { + x71 = 0/*false*/; + } + x72 = x71; + } else { + x72 = 0/*false*/; + } + x3 = x72; + } + int x88 = x3; + return x88; +} From 9aa80f41aeae8e632a85409b80388ee25f7b79b5 Mon Sep 17 00:00:00 2001 From: CUIZEWEN <57898114+CuiZewen@users.noreply.github.com> Date: Wed, 10 Jun 2020 16:37:58 +0800 Subject: [PATCH 3/3] Modify non-greedy(.*?) --- src/out/re_ab_dot_star_query_ab.actual.c | 100 ++++++++++++++------- src/test/scala/lms/verify/RegexTests.scala | 2 +- 2 files changed, 68 insertions(+), 34 deletions(-) diff --git a/src/out/re_ab_dot_star_query_ab.actual.c b/src/out/re_ab_dot_star_query_ab.actual.c index a937437..31dc4d0 100644 --- a/src/out/re_ab_dot_star_query_ab.actual.c +++ b/src/out/re_ab_dot_star_query_ab.actual.c @@ -36,7 +36,7 @@ int matcher(char * x0) { } else { x17 = 0/*false*/; } - int x72; + int x89; if (x17) { int x18 = x13 + 1; int x19 = x18 < x7; @@ -48,7 +48,7 @@ int matcher(char * x0) { } else { x22 = 0/*false*/; } - int x71; + int x88; if (x22) { int x23 = x18 + 1; int x24 = x23; @@ -86,50 +86,84 @@ int matcher(char * x0) { } int x38 = x37; int x39 = 0/*false*/; - int x40 = x39; - int x45; - if (x40) { - x45 = 0/*false*/; - } else { - int x42 = x38; - int x43 = !x42; - x45 = x43; - } - int x46; - if (x45) { - x46 = x26; - } else { - x46 = 0/*false*/; - } /*@ loop invariant ((x23<=x24) && (x24<=x7)); loop assigns x24, x38, x39; loop variant (x7-x24); */ - if (x46) { + for (;;) { + int x40 = x39; + int x45; + if (x40) { + x45 = 0/*false*/; + } else { + int x42 = x38; + int x43 = !x42; + x45 = x43; + } + int x49; + if (x45) { + int x46 = x24; + int x47 = x46 < x7; + x49 = x47; + } else { + x49 = 0/*false*/; + } + if (!x49) break; + int x51 = x24; x39 = 0/*false*/; - x38 = x37; - } else { + int x55 = x51 < x7; + int x57; + if (x55) { + char x52 = x0[x51]; + int x56 = 'a' == x52; + x57 = x56; + } else { + x57 = 0/*false*/; + } + int x65; + if (x57) { + int x58 = x51 + 1; + int x59 = x58 < x7; + int x62; + if (x59) { + char x60 = x0[x58]; + int x61 = 'b' == x60; + x62 = x61; + } else { + x62 = 0/*false*/; + } + int x64; + if (x62) { + x64 = 1/*true*/; + } else { + x64 = 0/*false*/; + } + x65 = x64; + } else { + x65 = 0/*false*/; + } + x38 = x65; } - int x65 = x39; - int x69; - if (x65) { - x69 = 0/*false*/; + int x82 = x39; + int x86; + if (x82) { + x86 = 0/*false*/; } else { - int x67 = x38; - x69 = x67; + int x84 = x38; + x86 = x84; } - x71 = x69; + x88 = x86; } else { - x71 = 0/*false*/; + x88 = 0/*false*/; } - x72 = x71; + x89 = x88; } else { - x72 = 0/*false*/; + x89 = 0/*false*/; } - x3 = x72; + x3 = x89; } - int x88 = x3; - return x88; + int x105 = x3; + return x105; } diff --git a/src/test/scala/lms/verify/RegexTests.scala b/src/test/scala/lms/verify/RegexTests.scala index 0c512e3..56acdcd 100644 --- a/src/test/scala/lms/verify/RegexTests.scala +++ b/src/test/scala/lms/verify/RegexTests.scala @@ -55,7 +55,7 @@ trait StagedRegexpMatcher extends Dsl { var found = matchhere(regexp, restart, text, sqstart) var failed = false loop (start <= sqstart && sqstart <= text.length, List[Any](sqstart, found, failed), text.length-sqstart){ - if(!failed && !found && sqstart < text.length) { + while(!failed && !found && sqstart < text.length) { failed = !matchchar(c, text(sqstart)) found = matchhere(regexp, restart, text, sqstart) }}