finding the minimum that is not an FP - instead of finding the minimum and then checking if it was an FP. And detecting more FPs by finding when a witness pass through the accept state

This commit is contained in:
Erik Krogh Kristensen
2020-11-04 21:04:08 +01:00
parent ac514b1739
commit 34fd0d89f5
3 changed files with 25 additions and 23 deletions

View File

@@ -840,7 +840,6 @@ predicate isPumpable(State fork, string w) {
*/
State process(State fork, string w, int i) {
isPumpable(fork, w) and
min(string s | isPumpable(fork, s)).prefix(w.length()) = w and
exists(State prev |
i = 0 and prev = fork
or
@@ -876,9 +875,12 @@ string rotate(string str, int i) {
from RegExpTerm t, string c, int i
where
c = min(string w | isPumpable(Match(t, i), w)) and
not isPumpable(epsilonSucc+(Match(t, i)), _) and
not epsilonSucc*(process(Match(t, i), c, [0 .. c.length() - 1])) = Accept(_)
c =
min(string w |
isPumpable(Match(t, i), w) and
not isPumpable(epsilonSucc+(Match(t, i)), _) and
not epsilonSucc*(process(Match(t, i), w, [0 .. w.length() - 1])) = Accept(_)
)
select t,
"This part of the regular expression may cause exponential backtracking on strings " +
"containing many repetitions of '" + escape(rotate(c, i)) + "'."

View File

@@ -92,19 +92,19 @@
| tst.js:167:15:167:27 | (1s\|[\\da-z])* | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '1s'. |
| tst.js:170:15:170:23 | (0\|[\\d])* | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '0'. |
| tst.js:173:16:173:20 | [\\d]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '0'. |
| tst.js:188:17:188:21 | [^>]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '?'. |
| tst.js:191:16:191:21 | [^>a]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'b'. |
| tst.js:194:17:194:19 | \\s* | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '\\n'. |
| tst.js:197:18:197:20 | \\s+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of ' '. |
| tst.js:200:68:200:79 | [ a-zA-Z{}]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of ' A:'. |
| tst.js:200:81:200:82 | ,? | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of ',A: '. |
| tst.js:182:17:182:21 | [^>]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '?'. |
| tst.js:185:16:185:21 | [^>a]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'b'. |
| tst.js:188:17:188:19 | \\s* | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '\\n'. |
| tst.js:191:18:191:20 | \\s+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of ' '. |
| tst.js:194:68:194:79 | [ a-zA-Z{}]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of ' A:'. |
| tst.js:194:81:194:82 | ,? | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of ',A: '. |
| tst.js:197:15:197:16 | a+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'a'. |
| tst.js:197:18:197:19 | b+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'b'. |
| tst.js:200:17:200:18 | a+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'a'. |
| tst.js:203:15:203:16 | a+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'a'. |
| tst.js:203:18:203:19 | b+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'b'. |
| tst.js:206:17:206:18 | a+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'a'. |
| tst.js:209:15:209:16 | a+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'a'. |
| tst.js:215:15:215:16 | a+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'a'. |
| tst.js:221:15:221:17 | \\n+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '\\n'. |
| tst.js:224:15:224:19 | [^X]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'Y'. |
| tst.js:215:15:215:17 | \\n+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '\\n'. |
| tst.js:218:15:218:19 | [^X]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'Y'. |
| tst.js:221:20:221:20 | b | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'bY'. |
| tst.js:227:20:227:20 | b | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'bY'. |
| tst.js:233:20:233:20 | b | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'bY'. |
| tst.js:248:16:248:17 | ab | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'ab'. |
| tst.js:242:16:242:17 | ab | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'ab'. |

View File

@@ -178,12 +178,6 @@ var good12 = /(\d+(X\d+)?)+/;
// GOOD - there is no witness in the end that could cause the regexp to not match
var good13 = /([0-9]+(X[0-9]*)?)*/;
// NOT GOOD
var bad42 = /([\n\s]+)*(.)/;
// GOOD - any witness passes through the accept state.
var good14 = /(A*A*X)*/;
// GOOD - but still flagged (always matches something)
var good15 = /^([^>]+)*(>|$)/;
@@ -249,3 +243,9 @@ var bad55 = /((ab)+)*$/;
// GOOD
var good23 = /((ab)+)*[a1][b1][a2][b2][a3][b3]/;
// NOT GOOD - but not catched due to the analysis taking an unlucky guess when choosing an arbitary char from `[\n\s]`.
var bad56 = /([\n\s]+)*(.)/;
// GOOD - any witness passes through the accept state.
var good24 = /(A*A*X)*/;