BDD node limit of 2^^25 reached on Type erasure

[skavans]

Hi!

I'm making my own qlpack to make CodeQL support another language. I'm using the Kaleidoscope pack as a sample.

I'm done with AST and making CFG now but, for some reason, after adding a few of ControlFlowTree's, any additional one leads to simple queries like below

select count(AstCfgNode node)

make optimizer hanging while doing something with (some) types, on steps:

Running query: Compiling - Optimising query - Stage 13/14 - Optimising - Type spec
Running query: Compiling - Optimising query - Stage 13/14 - Optimising - Type erasure

Then it leads to the exception:

Oops! A fatal internal error occurred. Details:
com.semmle.util.exception.CatastrophicError: BDD factory #52 QL type universe 'AST#72f56b2e::TAstNode': BDD node limit of 2^^25 reached.
        at com.semmle.bdd.SemmleBDDFactory.growNodesList(SemmleBDDFactory.java:446)
        at com.semmle.bdd.SemmleBDDFactory.makeNode(SemmleBDDFactory.java:396)
        at com.semmle.bdd.SemmleBDDFactory.makeBNode(SemmleBDDFactory.java:423)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDDFactory.and(SemmleBDDFactory.java:689)
        at com.semmle.bdd.SemmleBDD.and(SemmleBDD.java:20)
        at com.semmle.dil.proptypes.BDDProposition.intersect(BDDProposition.java:48)
        at com.semmle.dil.typeinference.TTC.and(TTC.java:207)
        at com.semmle.dil.absinthe.types.TypingFactory$Typing.conjoinTTCs(TypingFactory.java:375)
        at com.semmle.dil.absinthe.types.TypingFactory$Typing.and(TypingFactory.java:404)
        at com.semmle.dil.opt.TypeSpecialiser$ContextCollector.visit(TypeSpecialiser.java:194)
        at com.semmle.dil.opt.TypeSpecialiser$ContextCollector.visit(TypeSpecialiser.java:136)
        at com.semmle.dil.ast.Or.accept(Or.java:108)
        at com.semmle.dil.opt.TypeSpecialiser$ContextCollector.lambda$visit$2(TypeSpecialiser.java:173)
        at java.base/java.lang.Iterable.forEach(Unknown Source)
        at com.semmle.dil.opt.TypeSpecialiser$ContextCollector.visit(TypeSpecialiser.java:168)
        at com.semmle.dil.opt.TypeSpecialiser.apply(TypeSpecialiser.java:70)
        at com.semmle.dil.opt.DILOptimiser.lambda$optimiseDILProgram$12(DILOptimiser.java:303)
        at com.semmle.inmemory.planner.Compiler.lambda$optimiseAndCompileOneProgram$1(Compiler.java:232)
        at com.semmle.dil.opt.DILOptimiser.optimiseDILProgram(DILOptimiser.java:299)
        at com.semmle.dil.opt.DILOptimiser.lambda$apply$0(DILOptimiser.java:63)
        at com.semmle.inmemory.planner.Compiler.lambda$optimiseAndCompileOneProgram$1(Compiler.java:232)
        at com.semmle.dil.opt.DILOptimiser.apply(DILOptimiser.java:53)
        at com.semmle.inmemory.planner.Compiler.optimiseAndCompileOneProgram(Compiler.java:223)
        at com.semmle.inmemory.planner.StageDirector.processStratum(StageDirector.java:167)
        at com.semmle.inmemory.planner.StageDirector.computeStagedProgram(StageDirector.java:121)
        at com.semmle.inmemory.QueryCompiler.prepareQuery(QueryCompiler.java:62)
        at com.semmle.api.QLCompilerUtils.compilePipelineToRa(QLCompilerUtils.java:262)
        at com.semmle.cli2.ql.CompilationCommon$OneCompilation.compileInner(CompilationCommon.java:457)
        at com.semmle.cli2.ql.CompilationCommon$OneCompilation.compile(CompilationCommon.java:273)
        at com.semmle.cli2.ql.CompilationCommon.compile(CompilationCommon.java:241)
        at com.semmle.cli2.ql.CompilationCommon.compile(CompilationCommon.java:233)
        at com.semmle.cli2.execute.ExecuteQueriesCommand.compileOrLoad(ExecuteQueriesCommand.java:827)
        at com.semmle.cli2.execute.ExecuteQueriesCommand$ExecutionIterator.startImpl(ExecuteQueriesCommand.java:224)
        at com.semmle.cli2.execute.ExecuteQueriesCommand$ExecutionIterator.start(ExecuteQueriesCommand.java:192)
        at com.semmle.cli2.execute.ExecuteQueriesCommand$ExecutionIterator.lambda$next$0(ExecuteQueriesCommand.java:187)
        at com.semmle.util.concurrent.FutureUtils.supplyCompose(FutureUtils.java:248)
        at com.semmle.util.concurrent.Paralleliser.lambda$startMoreJobs$3(Paralleliser.java:109)
        at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(Unknown Source)
        at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(Unknown Source)
        at java.base/java.lang.Thread.run(Unknown Source)

I tried to simplify the Trees, replace them with Leafs, anything. Doesn't make any sense.

Please help me to understand, where to look for the reason? Is it possible to somehow debug this behavior? I do not even understand what "types" it means.

[skavans]

I can easily select all the AST nodes for just a few seconds. But when I'm trying to select all the CFG ones – the issue appears.

[skavans]

I'm integrating with CFG like

Cfg::Make<Location, Input>;

Do you maybe know, which issues in my ControlFlowTree and StandardPreOrderTree classes could lead to such a behavior.

[adityasharad]

Thanks for reporting, and for your interest using CodeQL for this purpose!

A "type" here refers to a set of possible values, which are usually defined by a column in the database schema, a class you write in QL, or a newtype you write in QL -- https://codeql.github.com/docs/ql-language-reference/types/ has more information.

What you've encountered is a tough problem: it usually means the size of the class/type hierarchy has grown so large that the CodeQL query compiler can no longer represent it in its internal data structures. Since you're able to evaluate your AST layer, I suspect the CFG layer is what pushes your code over the limit.

Would you be able to share your code with us, assuming it's in an open-source branch? The technique we use internally to resolve this issue is to try and simplify the structure and relationships among your node types, so that you have fewer different types of CFG node, or simpler relationships (less nesting) among them. If we can see your code, we can figure out what to suggest more concretely, or whether there's a compiler bug we should fix.

[skavans]

Hi @adityasharad, great thanks for your reply!
I'm glad to share a "concept" of my code since it's not open-sourced (yet).

Cfg.qll:

private import codeql.controlflow.Cfg as Cfg
private import codeql.Locations
private import codeql.mylang.ast.AstNode

class Node = mylangCfg::Node;
class EntryNode = mylangCfg::EntryNode;
class ExitNode = mylangCfg::ExitNode;
class AstCfgNode = mylangCfg::AstCfgNode;

class mylangAstCfgNode extends AstCfgNode {
  mylangCfg::AstCfgNode getLastInstruction() {
    result = this
  }
  
  predicate isTerminal() {
    not exists(this.getASuccessor())
  }
  
  predicate hasNormalCompletion() {
    exists(mylangInput::Completion c |
      mylangCfg::last(this.getAstNode(), _, c) and
      mylangInput::completionIsNormal(c)
    )
  }
}

class ExtendedAstCfgNode = mylangAstCfgNode;

module mylangInput implements Cfg::InputSig<Location> {
  class AstNode = MyAstNode;

  additional newtype TCompletion =
    additional TSimpleCompletion() or
    additional TBooleanCompletion(boolean b) { b in [false, true] } or
    additional TReturnCompletion()

  class Completion extends TCompletion {
    string toString() {
      this = TSimpleCompletion() and result = "simple" or
      this = TBooleanCompletion(true) and result = "boolean(true)" or
      this = TBooleanCompletion(false) and result = "boolean(false)" or
      this = TReturnCompletion() and result = "return"
    }
  }

  cached predicate completionIsNormal(Completion c) {
    c = TSimpleCompletion() or c = TBooleanCompletion(_)
  }

  cached predicate completionIsSimple(Completion c) {
    c = TSimpleCompletion()
  }

  cached private predicate isBooleanCompletionNode(AstNode n) {
    any()
    // n = any(MyIfStatement ifs).getCondition() or
    // n = any(MyWhileStatement ws).getCondition() or
    // n = any(MyDoWhileStatement dws).getCondition() or
    // n = any(MyForStatement fs).getCondition() or
    // n = any(MyConditionalExpression ce).getCondition()
  }

  cached private predicate isReturnCompletionNode(AstNode n) {
    n instanceof MyReturnStatement
  }

  cached predicate completionIsValidFor(Completion c, AstNode n) {
    c = TBooleanCompletion(_) and isBooleanCompletionNode(n)
    or
    c = TReturnCompletion() and isReturnCompletionNode(n)
    or
    c = TSimpleCompletion() and
    not isBooleanCompletionNode(n) and
    not isReturnCompletionNode(n)
  }

  class CfgScope extends MyAstNode {
    CfgScope() {
      this instanceof MyFunctionDefinition and
      exists(this.(MyFunctionDefinition).getBody())
    }

    predicate isFunction() {
      this instanceof MyFunctionDefinition
    }
  }

  cached additional predicate nodeInScope(AstNode n, CfgScope scope) {
    scope = getDirectEnclosingScope(n)
  }
  
  cached private CfgScope getDirectEnclosingScope(AstNode n) {
    result = min(CfgScope scope |
      scope = n.(MyAstNode).getAnAncestorOrSelf() and
      scope instanceof CfgScope
    | scope order by scope.getLocation().getStartLine() desc, scope.getLocation().getStartColumn() desc)
  }

  cached CfgScope getCfgScope(AstNode n) {
    nodeInScope(n, result)
  }

  cached predicate scopeFirst(CfgScope scope, AstNode first) {
    scope instanceof MyFunctionDefinition and
    first = scope.(MyFunctionDefinition).getBody()
  }

  cached predicate scopeLast(CfgScope scope, AstNode last, Completion c) {
    scope instanceof MyFunctionDefinition and
    last = scope.(MyFunctionDefinition).getBody() and
    c = TSimpleCompletion()
  }

  additional newtype TSuccessorType =
    additional TNormalSuccessor() or
    additional TBooleanSuccessor(boolean b) { b in [false, true] } or
    additional TReturnSuccessor()

  class SuccessorType extends TSuccessorType {
    string toString() {
      this = TNormalSuccessor() and result = "normal" or
      this = TBooleanSuccessor(true) and result = "true" or
      this = TBooleanSuccessor(false) and result = "false" or
      this = TReturnSuccessor() and result = "return"
    }
  }

  SuccessorType getAMatchingSuccessorType(Completion c) {
    c = TSimpleCompletion() and result = TNormalSuccessor() or
    c = TBooleanCompletion(true) and result = TBooleanSuccessor(true) or
    c = TBooleanCompletion(false) and result = TBooleanSuccessor(false) or
    c = TReturnCompletion() and result = TReturnSuccessor()
  }

  predicate successorTypeIsSimple(SuccessorType t) {
    t = TNormalSuccessor()
  }

  predicate successorTypeIsCondition(SuccessorType t) {
    t = TBooleanSuccessor(_)
  }

  predicate isAbnormalExitType(SuccessorType t) {
    t = TReturnSuccessor()
  }

  int idOfAstNode(AstNode n) {
    result = n.getId()
  }

  int idOfCfgScope(CfgScope scope) {
    result = scope.getId()
  }

  additional class SplitKindBase extends string {
    SplitKindBase() { this = "default" }
  }
  
  additional class Split extends string {
    Split() { this = "split" }
    string toString() { result = this }
  }

  additional int maxSplits() { result = 0 }
}

module mylangCfg = Cfg::Make<Location, mylangInput>;

private import codeql.mylang.cfg.CFGTreesBase
private import codeql.mylang.cfg.CFGStatements
private import codeql.mylang.cfg.CFGExpressions

AST sample:

class MyBinaryOperation extends MyExpression {
  MyBinaryOperation() { this instanceof TBinaryExpression }
  MyExpression getLeftOperand() { result = unwrap(this.getChild(0).(MyExpression)) }
  MyExpression getRightOperand() { result = unwrap(this.getChild(2).(MyExpression)) }
  string getOperator() { result = toTreeSitter(this.getChild(1).getInternalNode()).(Mylang::Token).getValue() }
  
  override MyType getType() {
    none()
  }
  predicate isLogicalOperator() {
    this.getOperator() = "&&" or this.getOperator() = "||"
  }

  predicate isComparisonOperator() {
    this.getOperator() = "==" or this.getOperator() = "!=" or
    this.getOperator() = "<" or this.getOperator() = ">" or
    this.getOperator() = "<=" or this.getOperator() = ">="
  }

  predicate returnsBool() {
    this.isLogicalOperator() or this.isComparisonOperator()
  }
}

class MyIfStatement extends MyStatement {
  MyIfStatement() {
    this instanceof TIfStatement
  }

  MyExpression getCondition() {
    result = unwrap(TExpression(toTreeSitter(this).(Mylang::IfStatement).getCondition()).(MyExpression))
  }

  MyStatement getThenBranch() {
    result = unwrap(TStatement(toTreeSitter(this).(Mylang::IfStatement).getBody(0)).(MyStatement))
  }

  MyStatement getElseBranch() {
    result = unwrap(TStatement(toTreeSitter(this).(Mylang::IfStatement).getBody(1)).(MyStatement))
  }

  predicate hasElseBranch() { exists(getElseBranch()) }
}

class MyWhileStatement extends MyStatement {
  MyWhileStatement() {
    this instanceof TWhileStatement
  }

  MyExpression getCondition() {
    exists(Mylang::AstNode child |
      child = toTreeSitter(this).(Mylang::WhileStatement).getCondition().getChild() and
      toTreeSitter(result) = child and
      result = unwrap(result)
    )
  }

  MyStatement getBody() {
    exists(Mylang::AstNode child |
      child = toTreeSitter(this).(Mylang::WhileStatement).getBody().getChild() and
      toTreeSitter(result) = child and
      result = unwrap(result)
    )
  }
}

Cfg classes sample:

class MyBinaryOpTree extends MylangCfg::StandardPostOrderTree {
  MyBinaryOpTree() {
    this instanceof MyBinaryOperation and
    not this.(MyBinaryOperation).getOperator() in ["&&", "||"]
  }

  override MyAstNode getChildNode(int i) {
    i = 0 and result = this.(MyBinaryOperation).getLeftOperand() or
    i = 1 and result = this.(MyBinaryOperation).getRightOperand()
  }
}

class MyUnaryOpTree extends MylangCfg::StandardPostOrderTree {
  MyUnaryOpTree() { this instanceof MyUnaryOperation }

  override MyAstNode getChildNode(int i) {
    i = 0 and result = this.(MyUnaryOperation).getOperand()
  }
}

class MyIfStatementTree extends MylangCfg::ControlFlowTree {
  MyIfStatementTree() { this instanceof MyIfStatement }

  private MyIfStatement getIfStmt() { result = this }

  override predicate first(MyAstNode firstNode) {
    MylangCfg::first(getIfStmt().getCondition(), firstNode)
  }

  override predicate succ(MyAstNode predNode, MyAstNode succNode, MylangInput::Completion c) {
    MylangCfg::last(getIfStmt().getCondition(), predNode, MylangInput::TBooleanCompletion(true)) and
    MylangCfg::first(getIfStmt().getThenBranch(), succNode) and
    c = MylangInput::TSimpleCompletion()
    or
    exists(MyStatement elseBranch |
      elseBranch = getIfStmt().getElseBranch() and
      MylangCfg::last(getIfStmt().getCondition(), predNode, MylangInput::TBooleanCompletion(false)) and
      MylangCfg::first(elseBranch, succNode) and
      c = MylangInput::TSimpleCompletion()
    )
  }

  override predicate last(MyAstNode lastNode, MylangInput::Completion c) {
    MylangCfg::last(getIfStmt().getCondition(), lastNode, MylangInput::TBooleanCompletion(false)) and
    not exists(getIfStmt().getElseBranch()) and
    c = MylangInput::TSimpleCompletion()
    or
    MylangCfg::last(getIfStmt().getThenBranch(), lastNode, c)
    or
    exists(MyStatement elseBranch |
      elseBranch = getIfStmt().getElseBranch() and
      MylangCfg::last(elseBranch, lastNode, c)
    )
  }

  override predicate propagatesAbnormal(MyAstNode child) {
    child = getIfStmt().getCondition() or
    child = getIfStmt().getThenBranch() or
    child = getIfStmt().getElseBranch()
  }
}

So, now I have about 23 Cfg classes (Leafs + PostOrderTrees + ControlFlowTrees).
And the query

select count(AstCfgNode node)

make the optimizer fall with BDD node limit of 2^^25 reached. If I comment out a couple of my CFG classes (almost any ones!) – the optimizing starts working fine-ish. The more I comment out – the faster the optimization works.

The difference from the Kaleidoscope code I see is that my getChildNode returns AstNodes, but the Kaleidoscope one returns ControlFlowTrees. But I don't know if it makes any sense.

The code above could have the logical errors and could be non-optimal in some things since it's just a start-level prototype and the LLM is used to assist me in writing. I will definitely fix most of them but now I stuck on the BDD node limit of 2^^25 reached and this is my main stumbling block for now.

If I need to share any other part of the code – just let me know please. Thank you in advance!

[adityasharad]

Very helpful, thank you for sharing your code.

The optimiser bottleneck comes from having many classes that appear to be overlapping to the optimiser because they use logic within characteristic predicates to define their sets of values, rather than inheritance among types. You can alleviate this bottleneck by trying out changes of this form:

Old - AST example:

class MyBinaryOperation extends MyExpression {
  MyBinaryOperation() { this instanceof TBinaryExpression }
  ...
}

New - AST example:

class MyBinaryOperation extends MyExpression instanceof TBinaryExpression { // alternative: `extends MyExpression, TBinaryExpression`
  ...
}

Old - CFG example:

class MyBinaryOpTree extends MylangCfg::StandardPostOrderTree {
  MyBinaryOpTree() {
    this instanceof MyBinaryOperation and
    not this.(MyBinaryOperation).getOperator() in ["&&", "||"]
  }

New - CFG example:

class NonLogicalBinaryOperation extends MyBinaryOperation {
  NonLogicalBinaryOperation() { not this.isLogicalOperator() }
}
// Two changes here:
// Use instanceof in the type declaration
// Use a positive condition `instanceof NonLogicalBinaryOperation` instead of a negative condition `not this.(MyBinaryOperation).getOperator() in ["&&", "||"]`
class MyBinaryOpTree extends MylangCfg::StandardPostOrderTree instanceof NonLogicalBinaryOperation {
  ... 
}

and so on.

There is a slight difference between declaring a supertype with extends or with instanceof. instanceof will declare that the subtype's values are a subset of the supertype's values, but the subtype won't participate in overriding of predicates and fields on the supertype. See https://codeql.github.com/docs/ql-language-reference/types/#instanceof-extensions for more information. Use either as you see fit, but from your example I think you'll find the instanceof version appropriate.

[skavans]

Thank you @adityasharad! I will try this in a couple of days and get the feedback to you.

[skavans]

Wow @adityasharad, it seems working!
Thank you so much 🤝