Skip to content

Commit 2287113

Browse files
erik-krogherik-krogh
committed
simplify the recursion between TTrace and isReachableFromStartTuple
similar to the fix made by Shack in `ExponentialBackTracking.qll`
1 parent be37763 commit 2287113

4 files changed

Lines changed: 76 additions & 112 deletions

File tree

‎java/ql/lib/semmle/code/java/security/regexp/SuperlinearBackTracking.qll‎

Lines changed: 19 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -218,14 +218,7 @@ string minAndMaxIntersect(InputSymbol a, InputSymbol b) {
218218
private newtype TTrace =
219219
Nil() or
220220
Step(InputSymbol s1, InputSymbol s2, InputSymbol s3, TTrace t) {
221-
exists(StateTuple p |
222-
isReachableFromStartTuple(_, _, p, t, _) and
223-
step(p, s1, s2, s3, _)
224-
)
225-
or
226-
exists(State pivot, State succ | isStartLoops(pivot, succ) |
227-
t = Nil() and step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, _)
228-
)
221+
isReachableFromStartTuple(_, _, t, s1, s2, s3, _, _)
229222
}
230223

231224
/**
@@ -274,36 +267,34 @@ int distBackFromEnd(StateTuple r, StateTuple end) =
274267
* and there is a distance of `dist` from `tuple` to the nearest end-tuple `(pivot, succ, succ)`,
275268
* and a path from a start-state to `tuple` follows the transitions in `trace`.
276269
*/
277-
predicate isReachableFromStartTuple(State pivot, State succ, StateTuple tuple, Trace trace, int dist) {
278-
// base case. The first step is inlined to start the search after all possible 1-steps, and not just the ones with the shortest path.
279-
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, State q1, State q2, State q3 |
270+
private predicate isReachableFromStartTuple(State pivot, State succ, StateTuple r, Trace w, int rem) {
271+
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace v |
272+
isReachableFromStartTuple(pivot, succ, v, s1, s2, s3, r, rem) and
273+
w = Step(s1, s2, s3, v)
274+
)
275+
}
276+
277+
private predicate isReachableFromStartTuple(
278+
State pivot, State succ, Trace trace, InputSymbol s1, InputSymbol s2, InputSymbol s3,
279+
StateTuple tuple, int dist
280+
) {
281+
// base case.
282+
exists(State q1, State q2, State q3 |
280283
isStartLoops(pivot, succ) and
281284
step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, tuple) and
282285
tuple = MkStateTuple(q1, q2, q3) and
283-
trace = Step(s1, s2, s3, Nil()) and
286+
trace = Nil() and
284287
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ))
285288
)
286289
or
287290
// recursive case
288-
exists(StateTuple p, Trace v, InputSymbol s1, InputSymbol s2, InputSymbol s3 |
289-
isReachableFromStartTuple(pivot, succ, p, v, dist + 1) and
290-
dist = isReachableFromStartTupleHelper(pivot, succ, tuple, p, s1, s2, s3) and
291-
trace = Step(s1, s2, s3, v)
291+
exists(StateTuple p |
292+
isReachableFromStartTuple(pivot, succ, p, trace, dist + 1) and
293+
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ)) and
294+
step(p, s1, s2, s3, tuple)
292295
)
293296
}
294297

295-
/**
296-
* Helper predicate for the recursive case in `isReachableFromStartTuple`.
297-
*/
298-
pragma[noinline]
299-
private int isReachableFromStartTupleHelper(
300-
State pivot, State succ, StateTuple r, StateTuple p, InputSymbol s1, InputSymbol s2,
301-
InputSymbol s3
302-
) {
303-
result = distBackFromEnd(r, MkStateTuple(pivot, succ, succ)) and
304-
step(p, s1, s2, s3, r)
305-
}
306-
307298
/**
308299
* Gets the tuple `(pivot, succ, succ)` from the product automaton.
309300
*/

‎javascript/ql/lib/semmle/javascript/security/regexp/SuperlinearBackTracking.qll‎

Lines changed: 19 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -218,14 +218,7 @@ string minAndMaxIntersect(InputSymbol a, InputSymbol b) {
218218
private newtype TTrace =
219219
Nil() or
220220
Step(InputSymbol s1, InputSymbol s2, InputSymbol s3, TTrace t) {
221-
exists(StateTuple p |
222-
isReachableFromStartTuple(_, _, p, t, _) and
223-
step(p, s1, s2, s3, _)
224-
)
225-
or
226-
exists(State pivot, State succ | isStartLoops(pivot, succ) |
227-
t = Nil() and step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, _)
228-
)
221+
isReachableFromStartTuple(_, _, t, s1, s2, s3, _, _)
229222
}
230223

231224
/**
@@ -274,36 +267,34 @@ int distBackFromEnd(StateTuple r, StateTuple end) =
274267
* and there is a distance of `dist` from `tuple` to the nearest end-tuple `(pivot, succ, succ)`,
275268
* and a path from a start-state to `tuple` follows the transitions in `trace`.
276269
*/
277-
predicate isReachableFromStartTuple(State pivot, State succ, StateTuple tuple, Trace trace, int dist) {
278-
// base case. The first step is inlined to start the search after all possible 1-steps, and not just the ones with the shortest path.
279-
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, State q1, State q2, State q3 |
270+
private predicate isReachableFromStartTuple(State pivot, State succ, StateTuple r, Trace w, int rem) {
271+
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace v |
272+
isReachableFromStartTuple(pivot, succ, v, s1, s2, s3, r, rem) and
273+
w = Step(s1, s2, s3, v)
274+
)
275+
}
276+
277+
private predicate isReachableFromStartTuple(
278+
State pivot, State succ, Trace trace, InputSymbol s1, InputSymbol s2, InputSymbol s3,
279+
StateTuple tuple, int dist
280+
) {
281+
// base case.
282+
exists(State q1, State q2, State q3 |
280283
isStartLoops(pivot, succ) and
281284
step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, tuple) and
282285
tuple = MkStateTuple(q1, q2, q3) and
283-
trace = Step(s1, s2, s3, Nil()) and
286+
trace = Nil() and
284287
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ))
285288
)
286289
or
287290
// recursive case
288-
exists(StateTuple p, Trace v, InputSymbol s1, InputSymbol s2, InputSymbol s3 |
289-
isReachableFromStartTuple(pivot, succ, p, v, dist + 1) and
290-
dist = isReachableFromStartTupleHelper(pivot, succ, tuple, p, s1, s2, s3) and
291-
trace = Step(s1, s2, s3, v)
291+
exists(StateTuple p |
292+
isReachableFromStartTuple(pivot, succ, p, trace, dist + 1) and
293+
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ)) and
294+
step(p, s1, s2, s3, tuple)
292295
)
293296
}
294297

295-
/**
296-
* Helper predicate for the recursive case in `isReachableFromStartTuple`.
297-
*/
298-
pragma[noinline]
299-
private int isReachableFromStartTupleHelper(
300-
State pivot, State succ, StateTuple r, StateTuple p, InputSymbol s1, InputSymbol s2,
301-
InputSymbol s3
302-
) {
303-
result = distBackFromEnd(r, MkStateTuple(pivot, succ, succ)) and
304-
step(p, s1, s2, s3, r)
305-
}
306-
307298
/**
308299
* Gets the tuple `(pivot, succ, succ)` from the product automaton.
309300
*/

‎python/ql/lib/semmle/python/security/regexp/SuperlinearBackTracking.qll‎

Lines changed: 19 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -218,14 +218,7 @@ string minAndMaxIntersect(InputSymbol a, InputSymbol b) {
218218
private newtype TTrace =
219219
Nil() or
220220
Step(InputSymbol s1, InputSymbol s2, InputSymbol s3, TTrace t) {
221-
exists(StateTuple p |
222-
isReachableFromStartTuple(_, _, p, t, _) and
223-
step(p, s1, s2, s3, _)
224-
)
225-
or
226-
exists(State pivot, State succ | isStartLoops(pivot, succ) |
227-
t = Nil() and step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, _)
228-
)
221+
isReachableFromStartTuple(_, _, t, s1, s2, s3, _, _)
229222
}
230223

231224
/**
@@ -274,36 +267,34 @@ int distBackFromEnd(StateTuple r, StateTuple end) =
274267
* and there is a distance of `dist` from `tuple` to the nearest end-tuple `(pivot, succ, succ)`,
275268
* and a path from a start-state to `tuple` follows the transitions in `trace`.
276269
*/
277-
predicate isReachableFromStartTuple(State pivot, State succ, StateTuple tuple, Trace trace, int dist) {
278-
// base case. The first step is inlined to start the search after all possible 1-steps, and not just the ones with the shortest path.
279-
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, State q1, State q2, State q3 |
270+
private predicate isReachableFromStartTuple(State pivot, State succ, StateTuple r, Trace w, int rem) {
271+
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace v |
272+
isReachableFromStartTuple(pivot, succ, v, s1, s2, s3, r, rem) and
273+
w = Step(s1, s2, s3, v)
274+
)
275+
}
276+
277+
private predicate isReachableFromStartTuple(
278+
State pivot, State succ, Trace trace, InputSymbol s1, InputSymbol s2, InputSymbol s3,
279+
StateTuple tuple, int dist
280+
) {
281+
// base case.
282+
exists(State q1, State q2, State q3 |
280283
isStartLoops(pivot, succ) and
281284
step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, tuple) and
282285
tuple = MkStateTuple(q1, q2, q3) and
283-
trace = Step(s1, s2, s3, Nil()) and
286+
trace = Nil() and
284287
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ))
285288
)
286289
or
287290
// recursive case
288-
exists(StateTuple p, Trace v, InputSymbol s1, InputSymbol s2, InputSymbol s3 |
289-
isReachableFromStartTuple(pivot, succ, p, v, dist + 1) and
290-
dist = isReachableFromStartTupleHelper(pivot, succ, tuple, p, s1, s2, s3) and
291-
trace = Step(s1, s2, s3, v)
291+
exists(StateTuple p |
292+
isReachableFromStartTuple(pivot, succ, p, trace, dist + 1) and
293+
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ)) and
294+
step(p, s1, s2, s3, tuple)
292295
)
293296
}
294297

295-
/**
296-
* Helper predicate for the recursive case in `isReachableFromStartTuple`.
297-
*/
298-
pragma[noinline]
299-
private int isReachableFromStartTupleHelper(
300-
State pivot, State succ, StateTuple r, StateTuple p, InputSymbol s1, InputSymbol s2,
301-
InputSymbol s3
302-
) {
303-
result = distBackFromEnd(r, MkStateTuple(pivot, succ, succ)) and
304-
step(p, s1, s2, s3, r)
305-
}
306-
307298
/**
308299
* Gets the tuple `(pivot, succ, succ)` from the product automaton.
309300
*/

‎ruby/ql/lib/codeql/ruby/security/regexp/SuperlinearBackTracking.qll‎

Lines changed: 19 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -218,14 +218,7 @@ string minAndMaxIntersect(InputSymbol a, InputSymbol b) {
218218
private newtype TTrace =
219219
Nil() or
220220
Step(InputSymbol s1, InputSymbol s2, InputSymbol s3, TTrace t) {
221-
exists(StateTuple p |
222-
isReachableFromStartTuple(_, _, p, t, _) and
223-
step(p, s1, s2, s3, _)
224-
)
225-
or
226-
exists(State pivot, State succ | isStartLoops(pivot, succ) |
227-
t = Nil() and step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, _)
228-
)
221+
isReachableFromStartTuple(_, _, t, s1, s2, s3, _, _)
229222
}
230223

231224
/**
@@ -274,36 +267,34 @@ int distBackFromEnd(StateTuple r, StateTuple end) =
274267
* and there is a distance of `dist` from `tuple` to the nearest end-tuple `(pivot, succ, succ)`,
275268
* and a path from a start-state to `tuple` follows the transitions in `trace`.
276269
*/
277-
predicate isReachableFromStartTuple(State pivot, State succ, StateTuple tuple, Trace trace, int dist) {
278-
// base case. The first step is inlined to start the search after all possible 1-steps, and not just the ones with the shortest path.
279-
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, State q1, State q2, State q3 |
270+
private predicate isReachableFromStartTuple(State pivot, State succ, StateTuple r, Trace w, int rem) {
271+
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace v |
272+
isReachableFromStartTuple(pivot, succ, v, s1, s2, s3, r, rem) and
273+
w = Step(s1, s2, s3, v)
274+
)
275+
}
276+
277+
private predicate isReachableFromStartTuple(
278+
State pivot, State succ, Trace trace, InputSymbol s1, InputSymbol s2, InputSymbol s3,
279+
StateTuple tuple, int dist
280+
) {
281+
// base case.
282+
exists(State q1, State q2, State q3 |
280283
isStartLoops(pivot, succ) and
281284
step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, tuple) and
282285
tuple = MkStateTuple(q1, q2, q3) and
283-
trace = Step(s1, s2, s3, Nil()) and
286+
trace = Nil() and
284287
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ))
285288
)
286289
or
287290
// recursive case
288-
exists(StateTuple p, Trace v, InputSymbol s1, InputSymbol s2, InputSymbol s3 |
289-
isReachableFromStartTuple(pivot, succ, p, v, dist + 1) and
290-
dist = isReachableFromStartTupleHelper(pivot, succ, tuple, p, s1, s2, s3) and
291-
trace = Step(s1, s2, s3, v)
291+
exists(StateTuple p |
292+
isReachableFromStartTuple(pivot, succ, p, trace, dist + 1) and
293+
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ)) and
294+
step(p, s1, s2, s3, tuple)
292295
)
293296
}
294297

295-
/**
296-
* Helper predicate for the recursive case in `isReachableFromStartTuple`.
297-
*/
298-
pragma[noinline]
299-
private int isReachableFromStartTupleHelper(
300-
State pivot, State succ, StateTuple r, StateTuple p, InputSymbol s1, InputSymbol s2,
301-
InputSymbol s3
302-
) {
303-
result = distBackFromEnd(r, MkStateTuple(pivot, succ, succ)) and
304-
step(p, s1, s2, s3, r)
305-
}
306-
307298
/**
308299
* Gets the tuple `(pivot, succ, succ)` from the product automaton.
309300
*/

0 commit comments

Comments
 (0)