Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add and modify the non-greedy #1

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

add and modify the non-greedy #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9cf5487
add non-greedy(.*?)
CuiZewen Jun 10, 2020
2e6ecc9
add non-greedy(.*?)
CuiZewen Jun 10, 2020
9aa80f4
Modify non-greedy(.*?)
CuiZewen Jun 10, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
169 changes: 169 additions & 0 deletions src/out/re_ab_dot_star_query_ab.actual.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,169 @@
#include <limits.h>
#include <string.h>
/*@
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 x89;
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 x88;
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*/;
/*@
loop invariant ((x23<=x24) &&
(x24<=x7));
loop assigns x24, x38, x39;
loop variant (x7-x24);
*/
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*/;
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 x82 = x39;
int x86;
if (x82) {
x86 = 0/*false*/;
} else {
int x84 = x38;
x86 = x84;
}
x88 = x86;
} else {
x88 = 0/*false*/;
}
x89 = x88;
} else {
x89 = 0/*false*/;
}
x3 = x89;
}
int x105 = x3;
return x105;
}
18 changes: 17 additions & 1 deletion src/test/scala/lms/verify/RegexTests.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
Expand All @@ -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){
while(!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
}
Expand Down Expand Up @@ -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
Expand All @@ -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)
}
}