|
| 1 | +/** |
| 2 | + * @name Candidate predicate not marked as `nomagic` |
| 3 | + * @description A candidate predicate should be marked as `nomagic` to prevent unnecessary computation. |
| 4 | + * @kind problem |
| 5 | + * @problem.severity warning |
| 6 | + * @id ql/cand-missing-nomagic |
| 7 | + * @tags performance |
| 8 | + * @precision medium |
| 9 | + */ |
| 10 | + |
| 11 | +import ql |
| 12 | + |
| 13 | +/** |
| 14 | + * Holds if the set of tuples satisfying `cand` is an upper bound for |
| 15 | + * the set of tuples satisfying `f` |
| 16 | + */ |
| 17 | +predicate guards(Predicate cand, Formula f) { |
| 18 | + forex(Formula child | child = f.(Disjunction).getAnOperand() | guards(cand, child)) |
| 19 | + or |
| 20 | + guards(cand, f.(Conjunction).getAnOperand()) |
| 21 | + or |
| 22 | + exists(Call call | f = call | |
| 23 | + call.getTarget() = cand |
| 24 | + or |
| 25 | + guards(cand, call.getTarget().(Predicate).getBody()) |
| 26 | + ) |
| 27 | + or |
| 28 | + exists(Quantifier q | f = q | guards(cand, [q.getFormula(), q.getRange()])) |
| 29 | + or |
| 30 | + exists(IfFormula ifFormula | ifFormula = f | |
| 31 | + guards(cand, ifFormula.getThenPart()) and guards(cand, ifFormula.getElsePart()) |
| 32 | + ) |
| 33 | +} |
| 34 | + |
| 35 | +pragma[noinline] |
| 36 | +predicate hasNameWithNumberSuffix(Predicate p, string name, int n) { |
| 37 | + n = [1 .. 10] and |
| 38 | + p.getName() = name + n.toString() |
| 39 | +} |
| 40 | + |
| 41 | +/** |
| 42 | + * A candidate predicate for another predicate. |
| 43 | + * |
| 44 | + * A predicate `p0` is a candidate for another predicate `p` when the tuples |
| 45 | + * that satisfy `p0` upper bounds the set of tuples that satisfy `p`. |
| 46 | + */ |
| 47 | +class CandidatePredicate extends Predicate { |
| 48 | + Predicate pred; |
| 49 | + |
| 50 | + CandidatePredicate() { |
| 51 | + // This predicate "guards" the predicate `pred` (i.e., it's always evaluated before `pred`). |
| 52 | + guards(this, pred.getBody()) and |
| 53 | + ( |
| 54 | + // The name of `pred` is "foo", and the name of this predicate is `foo0`, or `fooHelper`, or any |
| 55 | + // other the other cases. |
| 56 | + pragma[only_bind_into](pred).getName() = |
| 57 | + this.getName() |
| 58 | + .regexpCapture("(.+)" + ["0", "helper", "aux", "cand", "Helper", "Aux", "Cand"], 1) |
| 59 | + or |
| 60 | + // Or this this predicate is named "foo02" and `pred` is named "foo01". |
| 61 | + exists(int n, string name | |
| 62 | + hasNameWithNumberSuffix(pred, name, n) and |
| 63 | + hasNameWithNumberSuffix(this, name, n - 1) |
| 64 | + ) |
| 65 | + ) |
| 66 | + } |
| 67 | + |
| 68 | + /** Holds if this predicate is a candidate predicate for `p`. */ |
| 69 | + predicate isCandidateFor(Predicate p) { p = pred } |
| 70 | +} |
| 71 | + |
| 72 | +from CandidatePredicate cand, Predicate pred |
| 73 | +where |
| 74 | + // The candidate predicate is not in a test directory. |
| 75 | + not cand.getLocation().getFile().getAbsolutePath().matches("%/" + ["meta", "test"] + "/%") and |
| 76 | + cand.isCandidateFor(pred) and |
| 77 | + not cand.getAnAnnotation() instanceof NoMagic and |
| 78 | + not cand.getAnAnnotation() instanceof NoOpt |
| 79 | +select cand, "Candidate predicate to $@ is not marked as nomagic.", pred, pred.getName() |
0 commit comments