Skip to content

Commit 46d69cf

Browse files
hvitvedhvitved
committed
Regex: Further tweaks to concretise computations
1 parent 5181544 commit 46d69cf

File tree

6 files changed

+144
-87
lines changed

6 files changed

+144
-87
lines changed

‎javascript/ql/lib/semmle/javascript/security/performance/ExponentialBackTracking.qll

Lines changed: 23 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -310,36 +310,43 @@ private StatePair getAForkPair(State fork) {
310310
result = MkStatePair(epsilonPred*(fork), epsilonPred*(fork))
311311
}
312312

313-
private class RelevantTrace extends Trace {
313+
private predicate hasSuffix(Trace suffix, Trace t, int i) {
314+
// Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the
315+
// recursive case, so instead we check it explicitly here.
316+
t instanceof RelevantTrace and
317+
i = 0 and
318+
suffix = t
319+
or
320+
hasSuffix(Step(_, _, suffix), t, i - 1)
321+
}
322+
323+
pragma[noinline]
324+
private predicate hasTuple(InputSymbol s1, InputSymbol s2, Trace t, int i) {
325+
hasSuffix(Step(s1, s2, _), t, i)
326+
}
327+
328+
private class RelevantTrace extends Trace, Step {
314329
RelevantTrace() {
315330
exists(State fork, StatePair q |
316331
isReachableFromFork(fork, q, this, _) and
317332
q = getAForkPair(fork)
318333
)
319334
}
320335

321-
private Trace getSuffix(int i) {
322-
i = 0 and
323-
result = this
324-
or
325-
this.getSuffix(i - 1) = Step(_, _, result)
326-
}
327-
328-
private predicate hasTuple(int i, InputSymbol s1, InputSymbol s2) {
329-
this.getSuffix(i) = Step(s1, s2, _)
336+
pragma[noinline]
337+
private string intersect(int i) {
338+
exists(InputSymbol s1, InputSymbol s2 |
339+
hasTuple(s1, s2, this, i) and
340+
result = intersect(s1, s2)
341+
)
330342
}
331343

332344
/** Gets a string corresponding to this trace. */
333345
// the pragma is needed for the case where `intersect(s1, s2)` has multiple values,
334346
// not for recursion
335347
language[monotonicAggregates]
336348
string concretise() {
337-
result =
338-
concat(int i, InputSymbol s1, InputSymbol s2 |
339-
this.hasTuple(i, s1, s2)
340-
|
341-
intersect(s1, s2) order by i desc
342-
)
349+
result = strictconcat(int i | hasTuple(_, _, this, i) | this.intersect(i) order by i desc)
343350
}
344351
}
345352

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

Lines changed: 25 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -321,23 +321,35 @@ StateTuple getAnEndTuple(State pivot, State succ) {
321321
result = MkStateTuple(pivot, succ, succ)
322322
}
323323

324-
private class RelevantTrace extends Trace {
324+
private predicate hasSuffix(Trace suffix, Trace t, int i) {
325+
// Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the
326+
// recursive case, so instead we check it explicitly here.
327+
t instanceof RelevantTrace and
328+
i = 0 and
329+
suffix = t
330+
or
331+
hasSuffix(Step(_, _, _, suffix), t, i - 1)
332+
}
333+
334+
pragma[noinline]
335+
private predicate hasTuple(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace t, int i) {
336+
hasSuffix(Step(s1, s2, s3, _), t, i)
337+
}
338+
339+
private class RelevantTrace extends Trace, Step {
325340
RelevantTrace() {
326341
exists(State pivot, State succ, StateTuple q |
327342
isReachableFromStartTuple(pivot, succ, q, this, _) and
328343
q = getAnEndTuple(pivot, succ)
329344
)
330345
}
331346

332-
private Trace getSuffix(int i) {
333-
i = 0 and
334-
result = this
335-
or
336-
this.getSuffix(i - 1) = Step(_, _, _, result)
337-
}
338-
339-
private predicate hasTuple(int i, InputSymbol s1, InputSymbol s2, InputSymbol s3) {
340-
this.getSuffix(i) = Step(s1, s2, s3, _)
347+
pragma[noinline]
348+
private string getAThreewayIntersect(int i) {
349+
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3 |
350+
hasTuple(s1, s2, s3, this, i) and
351+
result = getAThreewayIntersect(s1, s2, s3)
352+
)
341353
}
342354

343355
/** Gets a string corresponding to this trace. */
@@ -346,10 +358,10 @@ private class RelevantTrace extends Trace {
346358
language[monotonicAggregates]
347359
string concretise() {
348360
result =
349-
concat(int i, InputSymbol s1, InputSymbol s2, InputSymbol s3 |
350-
this.hasTuple(i, s1, s2, s3)
361+
strictconcat(int i |
362+
hasTuple(_, _, _, this, i)
351363
|
352-
getAThreewayIntersect(s1, s2, s3) order by i desc
364+
this.getAThreewayIntersect(i) order by i desc
353365
)
354366
}
355367
}

‎python/ql/lib/semmle/python/security/performance/ExponentialBackTracking.qll

Lines changed: 23 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -310,36 +310,43 @@ private StatePair getAForkPair(State fork) {
310310
result = MkStatePair(epsilonPred*(fork), epsilonPred*(fork))
311311
}
312312

313-
private class RelevantTrace extends Trace {
313+
private predicate hasSuffix(Trace suffix, Trace t, int i) {
314+
// Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the
315+
// recursive case, so instead we check it explicitly here.
316+
t instanceof RelevantTrace and
317+
i = 0 and
318+
suffix = t
319+
or
320+
hasSuffix(Step(_, _, suffix), t, i - 1)
321+
}
322+
323+
pragma[noinline]
324+
private predicate hasTuple(InputSymbol s1, InputSymbol s2, Trace t, int i) {
325+
hasSuffix(Step(s1, s2, _), t, i)
326+
}
327+
328+
private class RelevantTrace extends Trace, Step {
314329
RelevantTrace() {
315330
exists(State fork, StatePair q |
316331
isReachableFromFork(fork, q, this, _) and
317332
q = getAForkPair(fork)
318333
)
319334
}
320335

321-
private Trace getSuffix(int i) {
322-
i = 0 and
323-
result = this
324-
or
325-
this.getSuffix(i - 1) = Step(_, _, result)
326-
}
327-
328-
private predicate hasTuple(int i, InputSymbol s1, InputSymbol s2) {
329-
this.getSuffix(i) = Step(s1, s2, _)
336+
pragma[noinline]
337+
private string intersect(int i) {
338+
exists(InputSymbol s1, InputSymbol s2 |
339+
hasTuple(s1, s2, this, i) and
340+
result = intersect(s1, s2)
341+
)
330342
}
331343

332344
/** Gets a string corresponding to this trace. */
333345
// the pragma is needed for the case where `intersect(s1, s2)` has multiple values,
334346
// not for recursion
335347
language[monotonicAggregates]
336348
string concretise() {
337-
result =
338-
concat(int i, InputSymbol s1, InputSymbol s2 |
339-
this.hasTuple(i, s1, s2)
340-
|
341-
intersect(s1, s2) order by i desc
342-
)
349+
result = strictconcat(int i | hasTuple(_, _, this, i) | this.intersect(i) order by i desc)
343350
}
344351
}
345352

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

Lines changed: 25 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -321,23 +321,35 @@ StateTuple getAnEndTuple(State pivot, State succ) {
321321
result = MkStateTuple(pivot, succ, succ)
322322
}
323323

324-
private class RelevantTrace extends Trace {
324+
private predicate hasSuffix(Trace suffix, Trace t, int i) {
325+
// Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the
326+
// recursive case, so instead we check it explicitly here.
327+
t instanceof RelevantTrace and
328+
i = 0 and
329+
suffix = t
330+
or
331+
hasSuffix(Step(_, _, _, suffix), t, i - 1)
332+
}
333+
334+
pragma[noinline]
335+
private predicate hasTuple(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace t, int i) {
336+
hasSuffix(Step(s1, s2, s3, _), t, i)
337+
}
338+
339+
private class RelevantTrace extends Trace, Step {
325340
RelevantTrace() {
326341
exists(State pivot, State succ, StateTuple q |
327342
isReachableFromStartTuple(pivot, succ, q, this, _) and
328343
q = getAnEndTuple(pivot, succ)
329344
)
330345
}
331346

332-
private Trace getSuffix(int i) {
333-
i = 0 and
334-
result = this
335-
or
336-
this.getSuffix(i - 1) = Step(_, _, _, result)
337-
}
338-
339-
private predicate hasTuple(int i, InputSymbol s1, InputSymbol s2, InputSymbol s3) {
340-
this.getSuffix(i) = Step(s1, s2, s3, _)
347+
pragma[noinline]
348+
private string getAThreewayIntersect(int i) {
349+
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3 |
350+
hasTuple(s1, s2, s3, this, i) and
351+
result = getAThreewayIntersect(s1, s2, s3)
352+
)
341353
}
342354

343355
/** Gets a string corresponding to this trace. */
@@ -346,10 +358,10 @@ private class RelevantTrace extends Trace {
346358
language[monotonicAggregates]
347359
string concretise() {
348360
result =
349-
concat(int i, InputSymbol s1, InputSymbol s2, InputSymbol s3 |
350-
this.hasTuple(i, s1, s2, s3)
361+
strictconcat(int i |
362+
hasTuple(_, _, _, this, i)
351363
|
352-
getAThreewayIntersect(s1, s2, s3) order by i desc
364+
this.getAThreewayIntersect(i) order by i desc
353365
)
354366
}
355367
}

‎ruby/ql/lib/codeql/ruby/security/performance/ExponentialBackTracking.qll

Lines changed: 23 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -310,36 +310,43 @@ private StatePair getAForkPair(State fork) {
310310
result = MkStatePair(epsilonPred*(fork), epsilonPred*(fork))
311311
}
312312

313-
private class RelevantTrace extends Trace {
313+
private predicate hasSuffix(Trace suffix, Trace t, int i) {
314+
// Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the
315+
// recursive case, so instead we check it explicitly here.
316+
t instanceof RelevantTrace and
317+
i = 0 and
318+
suffix = t
319+
or
320+
hasSuffix(Step(_, _, suffix), t, i - 1)
321+
}
322+
323+
pragma[noinline]
324+
private predicate hasTuple(InputSymbol s1, InputSymbol s2, Trace t, int i) {
325+
hasSuffix(Step(s1, s2, _), t, i)
326+
}
327+
328+
private class RelevantTrace extends Trace, Step {
314329
RelevantTrace() {
315330
exists(State fork, StatePair q |
316331
isReachableFromFork(fork, q, this, _) and
317332
q = getAForkPair(fork)
318333
)
319334
}
320335

321-
private Trace getSuffix(int i) {
322-
i = 0 and
323-
result = this
324-
or
325-
this.getSuffix(i - 1) = Step(_, _, result)
326-
}
327-
328-
private predicate hasTuple(int i, InputSymbol s1, InputSymbol s2) {
329-
this.getSuffix(i) = Step(s1, s2, _)
336+
pragma[noinline]
337+
private string intersect(int i) {
338+
exists(InputSymbol s1, InputSymbol s2 |
339+
hasTuple(s1, s2, this, i) and
340+
result = intersect(s1, s2)
341+
)
330342
}
331343

332344
/** Gets a string corresponding to this trace. */
333345
// the pragma is needed for the case where `intersect(s1, s2)` has multiple values,
334346
// not for recursion
335347
language[monotonicAggregates]
336348
string concretise() {
337-
result =
338-
concat(int i, InputSymbol s1, InputSymbol s2 |
339-
this.hasTuple(i, s1, s2)
340-
|
341-
intersect(s1, s2) order by i desc
342-
)
349+
result = strictconcat(int i | hasTuple(_, _, this, i) | this.intersect(i) order by i desc)
343350
}
344351
}
345352

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

Lines changed: 25 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -321,23 +321,35 @@ StateTuple getAnEndTuple(State pivot, State succ) {
321321
result = MkStateTuple(pivot, succ, succ)
322322
}
323323

324-
private class RelevantTrace extends Trace {
324+
private predicate hasSuffix(Trace suffix, Trace t, int i) {
325+
// Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the
326+
// recursive case, so instead we check it explicitly here.
327+
t instanceof RelevantTrace and
328+
i = 0 and
329+
suffix = t
330+
or
331+
hasSuffix(Step(_, _, _, suffix), t, i - 1)
332+
}
333+
334+
pragma[noinline]
335+
private predicate hasTuple(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace t, int i) {
336+
hasSuffix(Step(s1, s2, s3, _), t, i)
337+
}
338+
339+
private class RelevantTrace extends Trace, Step {
325340
RelevantTrace() {
326341
exists(State pivot, State succ, StateTuple q |
327342
isReachableFromStartTuple(pivot, succ, q, this, _) and
328343
q = getAnEndTuple(pivot, succ)
329344
)
330345
}
331346

332-
private Trace getSuffix(int i) {
333-
i = 0 and
334-
result = this
335-
or
336-
this.getSuffix(i - 1) = Step(_, _, _, result)
337-
}
338-
339-
private predicate hasTuple(int i, InputSymbol s1, InputSymbol s2, InputSymbol s3) {
340-
this.getSuffix(i) = Step(s1, s2, s3, _)
347+
pragma[noinline]
348+
private string getAThreewayIntersect(int i) {
349+
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3 |
350+
hasTuple(s1, s2, s3, this, i) and
351+
result = getAThreewayIntersect(s1, s2, s3)
352+
)
341353
}
342354

343355
/** Gets a string corresponding to this trace. */
@@ -346,10 +358,10 @@ private class RelevantTrace extends Trace {
346358
language[monotonicAggregates]
347359
string concretise() {
348360
result =
349-
concat(int i, InputSymbol s1, InputSymbol s2, InputSymbol s3 |
350-
this.hasTuple(i, s1, s2, s3)
361+
strictconcat(int i |
362+
hasTuple(_, _, _, this, i)
351363
|
352-
getAThreewayIntersect(s1, s2, s3) order by i desc
364+
this.getAThreewayIntersect(i) order by i desc
353365
)
354366
}
355367
}

0 commit comments

Comments
 (0)