The UnboundLoops lint and the Souffle-based equations solver

examples/implicit-init/implicitInit.ts

@@ -13,10 +13,6 @@ import {
  * It reports all the contracts that doesn't have an explicit implementation of the init function.
  */
 export class ImplicitInit extends Detector {
-  get id(): string {
-    return "II";
-  }
-
   check(_ctx: MistiContext, cu: CompilationUnit): MistiTactError[] {
     return Array.from(cu.contracts).reduce((foundErrors, [_, contract]) => {
       if (!cu.findMethodCFGByName(contract.name, "init")) {

examples/implicit-init/test/implicitInit.spec.ts

@@ -12,7 +12,7 @@ describe("ImplicitInit Detector Tests", () => {
     const driver = await Driver.create(tactConfigPath, { config });
 
     expect(driver.detectors.length).toBe(1);
-    expect(driver.detectors[0].id).toBe("II");
+    expect(driver.detectors[0].id).toBe("ImplicitInit");
 
     const foundErrors = await driver.execute();
     // TODO(bh): Add an error here when Tact v1.3 with implicit inits is released.

src/detectors/builtin/neverAccessedVariables.ts

@@ -1,5 +1,6 @@
 import { ASTStatement, ASTRef } from "@tact-lang/compiler/dist/grammar/ast";
-import { Solver } from "../../internals/solver";
+import { WorklistSolver } from "../../internals/solver/";
+import { Transfer } from "../../internals/transfer";
 import { Detector } from "../detector";
 import { JoinSemilattice } from "../../internals/lattice";
 import { MistiContext } from "../../internals/context";
@@ -37,6 +38,26 @@ class VariableUsageLattice implements JoinSemilattice<VariableState> {
   }
 }
 
+class NeverAccessedTransfer implements Transfer<VariableState> {
+  public transfer(
+    inState: VariableState,
+    _node: Node,
+    stmt: ASTStatement,
+  ): VariableState {
+    const outState = { ...inState };
+    if (stmt.kind === "statement_let") {
+      outState.declared.add([stmt.name, stmt.ref]);
+    } else {
+      forEachExpression(stmt, (expr) => {
+        if (expr.kind === "id") {
+          outState.used.add(expr.value);
+        }
+      });
+    }
+    return outState;
+  }
+}
+
 /**
  * A detector that identifies write-only or unused variables, fields and constants.
  *
@@ -128,26 +149,14 @@ export class NeverAccessedVariables extends Detector {
    */
   checkVariables(cu: CompilationUnit): MistiTactError[] {
     const errors: MistiTactError[] = [];
-    cu.forEachCFG(cu.ast, (cfg: CFG, _: Node, stmt: ASTStatement) => {
+    cu.forEachCFG(cu.ast, (cfg: CFG, _node: Node, _stmt: ASTStatement) => {
       if (cfg.origin === "stdlib") {
         return;
       }
       const lattice = new VariableUsageLattice();
-      const transfer = (_node: Node, inState: VariableState) => {
-        const outState = { ...inState };
-        if (stmt.kind === "statement_let") {
-          outState.declared.add([stmt.name, stmt.ref]);
-        } else {
-          forEachExpression(stmt, (expr) => {
-            if (expr.kind === "id") {
-              outState.used.add(expr.value);
-            }
-          });
-        }
-        return outState;
-      };
-      const solver = new Solver(cfg, transfer, lattice);
-      const results = solver.findFixpoint();
+      const transfer = new NeverAccessedTransfer();
+      const solver = new WorklistSolver(cu, cfg, transfer, lattice);
+      const results = solver.solve();
 
       const declaredVariables = new Map<string, ASTRef>();
       const usedVariables = new Set<string>();

src/detectors/builtin/unboundLoops.ts

@@ -0,0 +1,238 @@
+import { ASTStatement, ASTRef } from "@tact-lang/compiler/dist/grammar/ast";
+import {
+  Context,
+  Fact,
+  FactType,
+  Relation,
+  Executor,
+  Rule,
+  RuleBody,
+  Atom,
+} from "../../internals/souffle";
+import { Detector } from "../detector";
+import { CompilationUnit, Node, CFG } from "../../internals/ir";
+import { MistiContext } from "../../internals/context";
+import { createError, MistiTactError, Severity } from "../../internals/errors";
+import {
+  forEachExpression,
+  forEachStatement,
+} from "../../internals/tactASTUtil";
+
+/**
+ * A detector that analyzes loop conditions and control flow to ensure loops have proper termination criteria.
+ *
+ * ## Why is it bad?
+ * An unbounded loop can be problematic for several reasons:
+ * * Unexpected Behavior: Without a defined termination, loops can lead to unpredictable contract behavior and make debugging difficult.
+ * * Out-of-gas Attacks: Continuous looping without termination can lead to out-of-gas attacks.
+ * * DoS Attacks: Malicious actors can exploit unbounded loops to create denial-of-service attacks, impacting contract's availability.
+ *
+ * ## Example
+ * ```tact
+ * let x: Int = 10;
+ * while (x > 0) {
+ *   // Bad: x is not changed due looping
+ *   send(SendParameters{ to: sender(), ... });
+ * }
+ * ```
+ *
+ * Use instead:
+ * ```tact
+ * let x: Int = 10;
+ * while (x > 0) {
+ *   send(SendParameters{ to: sender(), ... });
+ *   x = x - 1;
+ * }
+ * ```
+ */
+export class UnboundLoops extends Detector {
+  check(ctx: MistiContext, cu: CompilationUnit): MistiTactError[] {
+    // TODO: Extract method for this shared logic
+    const souffleCtx = new Context<ASTRef>(this.id);
+    this.addDecls(souffleCtx);
+    this.addRules(souffleCtx);
+    this.addConstantConstraints(cu, souffleCtx);
+    this.addConstraints(cu, souffleCtx);
+
+    const executor = ctx.config.soufflePath
+      ? new Executor<ASTRef>({
+          inputDir: ctx.config.soufflePath,
+          outputDir: ctx.config.soufflePath,
+        })
+      : new Executor<ASTRef>();
+    const result = executor.executeSync(souffleCtx);
+    if (!result.success) {
+      throw new Error(`Error executing Soufflé: ${result.stderr}`);
+    }
+
+    const warnings = Array.from(result.results.entries.values()).map((fact) => {
+      if (fact.data === undefined) {
+        throw new Error(`AST position for fact ${fact} is not available`);
+      }
+      return createError(
+        "Unbounded loop: the condition variable doesn't change within the loop",
+        Severity.MEDIUM,
+        fact.data,
+      );
+    });
+
+    return warnings;
+  }
+
+  private addDecls(ctx: Context<ASTRef>): void {
+    ctx.add(Relation.from("constDef", [["var", FactType.Symbol]], undefined));
+    ctx.add(
+      Relation.from(
+        "varDef",
+        [
+          ["var", FactType.Symbol],
+          ["func", FactType.Symbol],
+        ],
+        undefined,
+      ),
+    );
+    ctx.add(
+      Relation.from(
+        "loopDef",
+        [
+          ["loopId", FactType.Number],
+          ["func", FactType.Symbol],
+        ],
+        undefined,
+      ),
+    );
+    ctx.add(
+      Relation.from(
+        "loopCondDef",
+        [
+          ["var", FactType.Symbol],
+          ["loopId", FactType.Number],
+          ["func", FactType.Symbol],
+        ],
+        undefined,
+      ),
+    );
+    ctx.add(
+      Relation.from(
+        "loopVarUse",
+        [
+          ["var", FactType.Symbol],
+          ["loopId", FactType.Number],
+          ["func", FactType.Symbol],
+        ],
+        undefined,
+      ),
+    );
+    ctx.add(
+      Relation.from(
+        "unbound",
+        [
+          ["var", FactType.Symbol],
+          ["loopId", FactType.Number],
+          ["func", FactType.Symbol],
+        ],
+        "output",
+      ),
+    );
+  }
+
+  private addRules(ctx: Context<ASTRef>): void {
+    // unbound(var, loopId, func) :-
+    //   varDef(var, func),
+    //   loopDef(loopId, func),
+    //   loopCondDef(var, loopId, func),
+    //   !constDef(var)
+    //   !loopVarUse(var, loopId, func).
+    ctx.add(
+      Rule.from(
+        [Atom.from("unbound", ["var", "loopId", "func"])],
+        RuleBody.from(Atom.from("varDef", ["var", "func"])),
+        RuleBody.from(Atom.from("loopDef", ["loopId", "func"])),
+        RuleBody.from(Atom.from("loopCondDef", ["var", "loopId", "func"])),
+        RuleBody.from(Atom.from("constDef", ["var"]), {
+          negated: true,
+        }),
+        RuleBody.from(Atom.from("loopVarUse", ["var", "loopId", "func"]), {
+          negated: true,
+        }),
+      ),
+    );
+  }
+
+  /**
+   * Generates Souffle facts for constant definitions which should not be reported if used in the loop.
+   */
+  private addConstantConstraints(
+    cu: CompilationUnit,
+    ctx: Context<ASTRef>,
+  ): void {
+    for (const c of cu.ast.getConstants(/* allowStdlib = */ true)) {
+      ctx.addFact("constDef", Fact.from([c.name], c.ref));
+    }
+  }
+
+  /**
+   * Collects facts based on the IR to populate the Souffle program.
+   * @param cu The compilation unit containing the CFGs and AST information.
+   * @param ctx The Souffle program to which the facts are added.
+   */
+  private addConstraints(cu: CompilationUnit, ctx: Context<ASTRef>): void {
+    cu.forEachCFG(cu.ast, (cfg: CFG, _: Node, stmt: ASTStatement) => {
+      if (cfg.origin === "stdlib") {
+        return;
+      }
+      const funName = cfg.name;
+      if (stmt.kind === "statement_let") {
+        ctx.addFact("varDef", Fact.from([stmt.name, funName], stmt.ref));
+        return;
+      }
+      if (
+        stmt.kind === "statement_while" ||
+        stmt.kind === "statement_repeat" ||
+        stmt.kind === "statement_until"
+      ) {
+        const loopId = stmt.id;
+        const usedInCond: Set<string> = new Set(); // names of variables used in this condition
+        ctx.addFact("loopDef", Fact.from([loopId, funName], stmt.ref));
+        forEachExpression(stmt.condition, (expr) => {
+          if (expr.kind === "id") {
+            const varName = expr.value;
+            usedInCond.add(varName);
+            ctx.addFact(
+              "loopCondDef",
+              Fact.from([varName, loopId, funName], expr.ref),
+            );
+          }
+        });
+        forEachStatement(stmt, (s) => {
+          if (
+            s.kind === "statement_assign" ||
+            s.kind === "statement_augmentedassign"
+          ) {
+            ctx.addFact(
+              "loopVarUse",
+              Fact.from([s.id, loopId, funName], s.ref),
+            );
+          } else if (s.kind === "statement_expression") {
+            const callExpr = s.expression;
+            if (
+              callExpr.kind === "op_call" ||
+              callExpr.kind === "op_static_call"
+            ) {
+              callExpr.args.forEach((a) => {
+                forEachExpression(a, (expr) => {
+                  if (expr.kind === "id" && usedInCond.has(expr.value)) {
+                    ctx.addFact(
+                      "loopVarUse",
+                      Fact.from([expr.id, loopId, funName], s.ref),
+                    );
+                  }
+                });
+              });
+            }
+          }
+        });
+      }
+    });
+  }
+}

src/detectors/detector.ts

@@ -36,6 +36,10 @@ const BuiltInDetectors: Record<string, () => Promise<Detector>> = {
     import("./builtin/neverAccessedVariables").then(
       (module) => new module.NeverAccessedVariables(),
     ),
+  UnboundLoops: () =>
+    import("./builtin/unboundLoops").then(
+      (module) => new module.UnboundLoops(),
+    ),
   ZeroAddress: () =>
     import("./builtin/zeroAddress").then((module) => new module.ZeroAddress()),
 };

src/internals/config.ts

@@ -24,6 +24,7 @@ const ConfigSchema = z.object({
 export const BUILTIN_DETECTORS: DetectorConfig[] = [
   { className: "ReadOnlyVariables" },
   { className: "NeverAccessedVariables" },
+  { className: "UnboundLoops" },
   { className: "ZeroAddress" },
 ];
 

src/internals/ir.ts

@@ -542,6 +542,16 @@ export class CFG {
       }
     });
   }
+
+  /**
+   * Iterates over all edges in a CFG, applying a callback to each edge.
+   * @param callback The function to apply to each edge.
+   */
+  forEachEdge(callback: (cfgEdge: Edge) => void) {
+    this.edges.forEach((cfgEdge) => {
+      callback(cfgEdge);
+    });
+  }
 }
 
 /**
@@ -656,3 +666,16 @@ export class CompilationUnit {
     });
   }
 }
+
+/**
+ * An utility funciton that extracts node's predecessors.
+ */
+export function getPredecessors(cfg: CFG, node: Node): Node[] {
+  const predecessors = cfg.getPredecessors(node.idx);
+  if (predecessors === undefined) {
+    throw new Error(
+      `Incorrect definition in the CFG: Node #${node.idx} has an undefined predecessor`,
+    );
+  }
+  return predecessors;
+}