limit the search of state-pairs to the ones that are reachable within the given length

This commit is contained in:
Erik Krogh Kristensen
2020-11-17 21:15:32 +01:00
parent c4d7533701
commit 55f2f86a26
4 changed files with 24 additions and 2 deletions

View File

@@ -799,6 +799,7 @@ string concretise(Trace t) {
* a path from `r` back to `(fork, fork)` with `rem` steps. * a path from `r` back to `(fork, fork)` with `rem` steps.
*/ */
predicate isReachableFromFork(State fork, StatePair r, Trace w, int rem) { predicate isReachableFromFork(State fork, StatePair r, Trace w, int rem) {
// base case
exists(InputSymbol s1, InputSymbol s2, State q1, State q2 | exists(InputSymbol s1, InputSymbol s2, State q1, State q2 |
isFork(fork, s1, s2, q1, q2) and isFork(fork, s1, s2, q1, q2) and
r = MkStatePair(q1, q2) and r = MkStatePair(q1, q2) and
@@ -806,11 +807,12 @@ predicate isReachableFromFork(State fork, StatePair r, Trace w, int rem) {
rem = statePairDist(r, MkStatePair(fork, fork)) rem = statePairDist(r, MkStatePair(fork, fork))
) )
or or
// recursive case
exists(StatePair p, Trace v, InputSymbol s1, InputSymbol s2 | exists(StatePair p, Trace v, InputSymbol s1, InputSymbol s2 |
isReachableFromFork(fork, p, v, rem + 1) and isReachableFromFork(fork, p, v, rem + 1) and
step(p, s1, s2, r) and step(p, s1, s2, r) and
w = Step(s1, s2, v) and w = Step(s1, s2, v) and
rem > 0 rem >= statePairDist(r, MkStatePair(fork, fork))
) )
} }

View File

@@ -263,3 +263,8 @@
| tst.js:251:18:251:19 | A* | it can start matching anywhere | | tst.js:251:18:251:19 | A* | it can start matching anywhere |
| tst.js:251:18:251:19 | A* | it can start matching anywhere after the start of the preceeding 'A*' | | tst.js:251:18:251:19 | A* | it can start matching anywhere after the start of the preceeding 'A*' |
| tst.js:260:14:260:21 | (\\n\\s*)+ | it can start matching anywhere | | tst.js:260:14:260:21 | (\\n\\s*)+ | it can start matching anywhere |
| tst.js:266:14:266:91 | (\\w*foobarbaz\\w*foobarbaz\\w*foobarbaz\\w*foobarbaz\\s*foobarbaz\\d*foobarbaz\\w*)+ | it can start matching anywhere |
| tst.js:266:15:266:17 | \\w* | it can start matching anywhere |
| tst.js:269:14:269:116 | (.thisisagoddamnlongstringforstresstestingthequery\|\\sthisisagoddamnlongstringforstresstestingthequery)* | it can start matching anywhere |
| tst.js:272:14:272:77 | (thisisagoddamnlongstringforstresstestingthequery\|this\\w+query)* | it can start matching anywhere |
| tst.js:275:15:275:117 | (thisisagoddamnlongstringforstresstestingthequery\|imanotherbutunrelatedstringcomparedtotheotherstring)* | it can start matching anywhere |

View File

@@ -113,3 +113,6 @@
| tst.js:254:17:254:21 | [^>]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '='. | | tst.js:254:17:254:21 | [^>]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '='. |
| tst.js:257:16:257:21 | [^>a]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '='. | | tst.js:257:16:257:21 | [^>a]+ | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '='. |
| tst.js:260:17:260:19 | \\s* | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '\\n'. | | tst.js:260:17:260:19 | \\s* | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '\\n'. |
| tst.js:266:87:266:89 | \\w* | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of '0foobarbazfoobarbazfoobarbazfoobarbazfoobarbazfoobarbaz'. |
| tst.js:269:14:269:116 | (.thisisagoddamnlongstringforstresstestingthequery\|\\sthisisagoddamnlongstringforstresstestingthequery)* | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of ' thisisagoddamnlongstringforstresstestingthequery'. |
| tst.js:272:14:272:77 | (thisisagoddamnlongstringforstresstestingthequery\|this\\w+query)* | This part of the regular expression may cause exponential backtracking on strings containing many repetitions of 'thisisagoddamnlongstringforstresstestingthequery'. |

View File

@@ -261,3 +261,15 @@ var bad58 = /(\n\s*)+$/;
// GOOD // GOOD
var good26 = /([^\\\]]+)*/ var good26 = /([^\\\]]+)*/
// NOT GOOD
var bad59 = /(\w*foobarbaz\w*foobarbaz\w*foobarbaz\w*foobarbaz\s*foobarbaz\d*foobarbaz\w*)+-/;
// NOT GOOD
var bad60 = /(.thisisagoddamnlongstringforstresstestingthequery|\sthisisagoddamnlongstringforstresstestingthequery)*-/
// NOT GOOD
var bad61 = /(thisisagoddamnlongstringforstresstestingthequery|this\w+query)*-/
// GOOD
var good27 = /(thisisagoddamnlongstringforstresstestingthequery|imanotherbutunrelatedstringcomparedtotheotherstring)*-/