From d60607e9ee588ae7854d5ec1cff156cf36fc2c5f Mon Sep 17 00:00:00 2001 From: Byakuren Hijiri Date: Sun, 30 Jun 2024 06:50:38 +0000 Subject: [PATCH 1/6] feat(unboundLoops): The definition of dataflow problem The solver should be based on souffle: https://github.com/nowarp/misti/issues/17 --- src/detectors/builtin/unboundLoops.ts | 249 ++++++++++++++++++++++++++ 1 file changed, 249 insertions(+) create mode 100644 src/detectors/builtin/unboundLoops.ts diff --git a/src/detectors/builtin/unboundLoops.ts b/src/detectors/builtin/unboundLoops.ts new file mode 100644 index 00000000..7d6487de --- /dev/null +++ b/src/detectors/builtin/unboundLoops.ts @@ -0,0 +1,249 @@ +import { + ASTStatement, + ASTRef, + ASTExpression, + ASTStatementWhile, + ASTStatementRepeat, + ASTStatementUntil, +} from "@tact-lang/compiler/dist/grammar/ast"; +import { Detector } from "../detector"; +import { JoinSemilattice } from "../../internals/lattice"; +import { CompilationUnit, Node, CFG } from "../../internals/ir"; +import { MistiContext } from "../../internals/context"; +import { + Context, + Fact, + FactType, + Relation, + Executor, + Rule, + RuleBody, + Atom, +} from "../../internals/souffle"; +import { createError, MistiTactError, Severity } from "../../internals/errors"; +import { foldStatements, forEachExpression } from "../../internals/tactASTUtil"; + +type LoopRef = ASTRef; + +/** + * Describes a dataflow state of local variables within the loop construction. + */ +interface VariableState { + /** Variables defined within dataflow of the current function. */ + defined: Map; + /** Variables used in loop's condition. */ + condition: Map>; + /** Variables modified within loop's body. */ + modified: Map>; +} + +class LoopVariablesLattice implements JoinSemilattice { + bottom(): VariableState { + return { defined: new Map(), condition: new Map(), modified: new Map() }; + } + + join(a: VariableState, b: VariableState): VariableState { + const joinedDefined = this.mergeSimpleMaps(a.defined, b.defined); + const joinedCondition = this.mergeNestedMaps(a.condition, b.condition); + const joinedModified = this.mergeNestedMaps(a.modified, b.modified); + return { + defined: joinedDefined, + condition: joinedCondition, + modified: joinedModified, + }; + } + + leq(a: VariableState, b: VariableState): boolean { + return ( + this.areSimpleMapsSubsets(a.defined, b.defined) && + this.areNestedMapsSubsets(a.condition, b.condition) && + this.areNestedMapsSubsets(a.modified, b.modified) + ); + } + + private mergeSimpleMaps( + a: Map, + b: Map, + ): Map { + const mergedMap = new Map(a); + b.forEach((value, key) => mergedMap.set(key, value)); + return mergedMap; + } + + private mergeNestedMaps( + a: Map>, + b: Map>, + ): Map> { + const mergedMap = new Map(a); + b.forEach((innerMap, key) => { + if (mergedMap.has(key)) { + mergedMap.set(key, this.mergeSimpleMaps(mergedMap.get(key)!, innerMap)); + } else { + mergedMap.set(key, new Map(innerMap)); + } + }); + return mergedMap; + } + + private areSimpleMapsSubsets( + a: Map, + b: Map, + ): boolean { + return [...a].every(([key, value]) => b.has(key) && b.get(key) === value); + } + + private areNestedMapsSubsets( + a: Map>, + b: Map>, + ): boolean { + return [...a].every( + ([key, innerMap]) => + b.has(key) && this.areSimpleMapsSubsets(innerMap, b.get(key)!), + ); + } +} + +interface Transfer { + /** + * Transforms the input state based on the analysis of a CFG node. + * + * This function updates the state of dataflow analysis as it processes + * each node (e.g., statements, expressions) in a control flow graph, + * reflecting changes due to program actions. + * + * @param node The CFG construct being analyzed. + * @param stmt The statement defined within the node. + * @param inState The dataflow state prior to the execution of `node`. + * @returns The updated dataflow state post node execution. + */ + transfer(inState: State, node: Node, stmt: ASTStatement): State; +} + +class LoopTransfer implements Transfer { + public transfer( + inState: VariableState, + _node: Node, + stmt: ASTStatement, + ): VariableState { + const outState = { ...inState }; + switch (stmt.kind) { + case "statement_let": + outState.defined.set(stmt.name, stmt.ref); + break; + case "statement_while": + this.processCondition(outState, stmt.ref, stmt.condition); + this.processBody(outState, stmt); + break; + case "statement_until": + this.processCondition(outState, stmt.ref, stmt.condition); + this.processBody(outState, stmt); + break; + case "statement_repeat": + this.processCondition(outState, stmt.ref, stmt.condition); + this.processBody(outState, stmt); + break; + default: + break; + } + return outState; + } + + /** + * Processes loop's condition collecting the variables defined in it to the out state. + */ + private processCondition( + outState: VariableState, + loopRef: ASTRef, + expr: ASTExpression, + ): void { + forEachExpression(expr, (expr) => { + if (expr.kind === "id" && outState.defined.has(expr.value)) { + this.setDefault(outState.condition, loopRef, expr.value, expr.ref); + } + }); + } + + /** + * Processes loop's body collecting information about variables used within the loop. + */ + private processBody( + outState: VariableState, + loop: ASTStatementWhile | ASTStatementRepeat | ASTStatementUntil, + ): void { + const conditionVars = outState.condition.get(loop.ref); + if (conditionVars === undefined) { + return; // Loop doesn't have variables in its condition + } + loop.statements.forEach((stmt) => { + forEachExpression(stmt, (expr) => { + // Find expressions that potentially modify a value of loop variables + if (expr.kind === "id" && conditionVars.has(expr.value)) { + this.setDefault(outState.modified, stmt.ref, expr.value, expr.ref); + } + }); + }); + } + + /** + * Ensures that a key-value pair is added to a nested map, initializing a new inner map if necessary. + */ + private setDefault( + outerMap: Map>, + loopRef: LoopRef, + innerKey: string, + innerValue: ASTRef, + ): void { + let innerMap = outerMap.get(loopRef); + if (!innerMap) { + innerMap = new Map(); + outerMap.set(loopRef, innerMap); + } + innerMap.set(innerKey, innerValue); + } +} + +/** + * 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[] { + cu.forEachCFG(cu.ast, (cfg: CFG, _: Node, stmt: ASTStatement) => { + if (cfg.origin === "stdlib") { + return; + } + const lattice = new LoopVariablesLattice(); + }); + + // TODO: Create and solve dataflow equations using Souffle + return []; + } + + /** + * Collects dataflow info within a single loop statement. + */ + private collectLoopInfo(lattice: LoopVariablesLattice) {} +} From e18e128962417f39243dc4117b84ec0070250835 Mon Sep 17 00:00:00 2001 From: Byakuren Hijiri Date: Sun, 30 Jun 2024 07:25:28 +0000 Subject: [PATCH 2/6] chore: Refactor; separate the `solver` packge and `transfer`/`results` modules --- .../builtin/neverAccessedVariables.ts | 39 ++++++++----- src/detectors/builtin/unboundLoops.ts | 17 +----- src/internals/solver/index.ts | 3 + src/internals/solver/results.ts | 25 ++++++++ src/internals/solver/souffle.ts | 4 ++ .../{solver.ts => solver/worklist.ts} | 57 ++++++++----------- src/internals/transfer.ts | 21 +++++++ 7 files changed, 101 insertions(+), 65 deletions(-) create mode 100644 src/internals/solver/index.ts create mode 100644 src/internals/solver/results.ts create mode 100644 src/internals/solver/souffle.ts rename src/internals/{solver.ts => solver/worklist.ts} (60%) create mode 100644 src/internals/transfer.ts diff --git a/src/detectors/builtin/neverAccessedVariables.ts b/src/detectors/builtin/neverAccessedVariables.ts index 93dd66f7..f3e7a01f 100644 --- a/src/detectors/builtin/neverAccessedVariables.ts +++ b/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 { } } +class NeverAccessedTransfer implements Transfer { + 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. * @@ -133,20 +154,8 @@ export class NeverAccessedVariables extends Detector { 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 transfer = new NeverAccessedTransfer(); + const solver = new WorklistSolver(cu, cfg, transfer, lattice); const results = solver.findFixpoint(); const declaredVariables = new Map(); diff --git a/src/detectors/builtin/unboundLoops.ts b/src/detectors/builtin/unboundLoops.ts index 7d6487de..260dbdf3 100644 --- a/src/detectors/builtin/unboundLoops.ts +++ b/src/detectors/builtin/unboundLoops.ts @@ -10,6 +10,7 @@ import { Detector } from "../detector"; import { JoinSemilattice } from "../../internals/lattice"; import { CompilationUnit, Node, CFG } from "../../internals/ir"; import { MistiContext } from "../../internals/context"; +import { Transfer } from "../../internals/transfer"; import { Context, Fact, @@ -103,22 +104,6 @@ class LoopVariablesLattice implements JoinSemilattice { } } -interface Transfer { - /** - * Transforms the input state based on the analysis of a CFG node. - * - * This function updates the state of dataflow analysis as it processes - * each node (e.g., statements, expressions) in a control flow graph, - * reflecting changes due to program actions. - * - * @param node The CFG construct being analyzed. - * @param stmt The statement defined within the node. - * @param inState The dataflow state prior to the execution of `node`. - * @returns The updated dataflow state post node execution. - */ - transfer(inState: State, node: Node, stmt: ASTStatement): State; -} - class LoopTransfer implements Transfer { public transfer( inState: VariableState, diff --git a/src/internals/solver/index.ts b/src/internals/solver/index.ts new file mode 100644 index 00000000..0a0fde56 --- /dev/null +++ b/src/internals/solver/index.ts @@ -0,0 +1,3 @@ +// export { SouffleSolver } from "./souffle"; +export { WorklistSolver } from "./worklist"; +export { SolverResults } from "./results"; diff --git a/src/internals/solver/results.ts b/src/internals/solver/results.ts new file mode 100644 index 00000000..0b745aa8 --- /dev/null +++ b/src/internals/solver/results.ts @@ -0,0 +1,25 @@ +import { NodeIdx } from "../ir"; + +/** + * Results of solving a generic dataflow problem. + * @template State The type representing the state in the dataflow analysis. + */ +export class SolverResults { + private stateMap: Map; + + constructor() { + this.stateMap = new Map(); + } + + public getState(idx: NodeIdx): State | undefined { + return this.stateMap.get(idx); + } + + public setState(idx: NodeIdx, state: State): void { + this.stateMap.set(idx, state); + } + + public getStates(): Map { + return this.stateMap; + } +} diff --git a/src/internals/solver/souffle.ts b/src/internals/solver/souffle.ts new file mode 100644 index 00000000..f7ffca0b --- /dev/null +++ b/src/internals/solver/souffle.ts @@ -0,0 +1,4 @@ +/** + * Provides a framework for solving dataflow analysis problems using the Soufflé solver. + */ +export class SouffleSolver {} diff --git a/src/internals/solver.ts b/src/internals/solver/worklist.ts similarity index 60% rename from src/internals/solver.ts rename to src/internals/solver/worklist.ts index 4b53736b..9ff6b273 100644 --- a/src/internals/solver.ts +++ b/src/internals/solver/worklist.ts @@ -1,47 +1,31 @@ -import { JoinSemilattice } from "./lattice"; -import { CFG, Node, NodeIdx } from "./ir"; +import { JoinSemilattice } from "../lattice"; +import { CFG, Node, CompilationUnit } from "../ir"; +import { SolverResults } from "./results"; +import { Transfer } from "../transfer"; /** - * Results of solving a generic dataflow problem. - * @template State The type representing the state in the dataflow analysis. + * Provides a framework for solving dataflow analysis problems by employing a worklist-based algorithm. + * + * This class encapsulates the control flow graph (CFG), node state transformations, + * and lattice properties necessary for the computation of fixpoints in dataflow equations. */ -export class SolverResults { - private stateMap: Map; - - constructor() { - this.stateMap = new Map(); - } - - public getState(idx: NodeIdx): State | undefined { - return this.stateMap.get(idx); - } - - public setState(idx: NodeIdx, state: State): void { - this.stateMap.set(idx, state); - } - - public getStates(): Map { - return this.stateMap; - } -} - -/** - * Solver for generic dataflow problems. - */ -export class Solver { - private cfg: CFG; - private transfer: (node: Node, state: State) => State; - private lattice: JoinSemilattice; +export class WorklistSolver { + private readonly cu: CompilationUnit; + private readonly cfg: CFG; + private transfer: Transfer; + private readonly lattice: JoinSemilattice; /** * @param transfer A function that defines the transfer operation for a node and its state. * @param lattice An instance of a lattice that defines the join, bottom, and leq operations. */ constructor( + cu: CompilationUnit, cfg: CFG, - transfer: (node: Node, state: State) => State, + transfer: Transfer, lattice: JoinSemilattice, ) { + this.cu = cu; this.cfg = cfg; this.transfer = transfer; this.lattice = lattice; @@ -53,7 +37,6 @@ export class Solver { throw new Error( `Incorrect definition in the CFG: Node #${node.idx} has an undefined predecessor`, ); - // return []; } return predecessors; } @@ -77,7 +60,13 @@ export class Solver { return this.lattice.join(acc, results.getState(pred.idx)!); }, this.lattice.bottom()); - const outState = this.transfer(node, inState); + const stmt = this.cu.ast.getStatement(node.stmtID); + if (stmt === undefined) { + throw new Error( + `Cannot find statement #${node.stmtID} defined within node #${node.idx}`, + ); + } + const outState = this.transfer.transfer(inState, node, stmt); if (!this.lattice.leq(outState, results.getState(node.idx)!)) { results.setState(node.idx, outState); diff --git a/src/internals/transfer.ts b/src/internals/transfer.ts new file mode 100644 index 00000000..26d27edc --- /dev/null +++ b/src/internals/transfer.ts @@ -0,0 +1,21 @@ +import { ASTStatement } from "@tact-lang/compiler/dist/grammar/ast"; +import { Node } from "./ir"; + +/** + * Represents an interface for dataflow transfer functions. + */ +export interface Transfer { + /** + * Transforms the input state based on the analysis of a CFG node. + * + * This function updates the state of dataflow analysis as it processes + * each node (e.g., statements, expressions) in a control flow graph, + * reflecting changes due to program actions. + * + * @param node The CFG construct being analyzed. + * @param stmt The statement defined within the node. + * @param inState The dataflow state prior to the execution of `node`. + * @returns The updated dataflow state post node execution. + */ + transfer(inState: State, node: Node, stmt: ASTStatement): State; +} From 85c8975d32285b586b9448d433ac92b1eb91b1a4 Mon Sep 17 00:00:00 2001 From: Byakuren Hijiri Date: Mon, 1 Jul 2024 05:21:36 +0000 Subject: [PATCH 3/6] feat(solver): Draft the skeleton of the Souffle solver --- .../builtin/neverAccessedVariables.ts | 2 +- src/detectors/builtin/unboundLoops.ts | 40 ++--- src/internals/ir.ts | 23 +++ src/internals/solver/index.ts | 3 +- src/internals/solver/solver.ts | 8 + src/internals/solver/souffle.ts | 151 +++++++++++++++++- src/internals/solver/worklist.ts | 25 ++- src/internals/souffle/index.ts | 2 +- 8 files changed, 215 insertions(+), 39 deletions(-) create mode 100644 src/internals/solver/solver.ts diff --git a/src/detectors/builtin/neverAccessedVariables.ts b/src/detectors/builtin/neverAccessedVariables.ts index f3e7a01f..c39fe4ce 100644 --- a/src/detectors/builtin/neverAccessedVariables.ts +++ b/src/detectors/builtin/neverAccessedVariables.ts @@ -156,7 +156,7 @@ export class NeverAccessedVariables extends Detector { const lattice = new VariableUsageLattice(); const transfer = new NeverAccessedTransfer(); const solver = new WorklistSolver(cu, cfg, transfer, lattice); - const results = solver.findFixpoint(); + const results = solver.solve(); const declaredVariables = new Map(); const usedVariables = new Set(); diff --git a/src/detectors/builtin/unboundLoops.ts b/src/detectors/builtin/unboundLoops.ts index 260dbdf3..cc3acef8 100644 --- a/src/detectors/builtin/unboundLoops.ts +++ b/src/detectors/builtin/unboundLoops.ts @@ -7,22 +7,14 @@ import { ASTStatementUntil, } from "@tact-lang/compiler/dist/grammar/ast"; import { Detector } from "../detector"; +import { SouffleSolver, SouffleMapper } from "../../internals/solver"; import { JoinSemilattice } from "../../internals/lattice"; import { CompilationUnit, Node, CFG } from "../../internals/ir"; import { MistiContext } from "../../internals/context"; import { Transfer } from "../../internals/transfer"; -import { - Context, - Fact, - FactType, - Relation, - Executor, - Rule, - RuleBody, - Atom, -} from "../../internals/souffle"; +import { Context } from "../../internals/souffle"; import { createError, MistiTactError, Severity } from "../../internals/errors"; -import { foldStatements, forEachExpression } from "../../internals/tactASTUtil"; +import { forEachExpression } from "../../internals/tactASTUtil"; type LoopRef = ASTRef; @@ -104,6 +96,9 @@ class LoopVariablesLattice implements JoinSemilattice { } } +/** + * The transfer function used by the worklist-based solver. + */ class LoopTransfer implements Transfer { public transfer( inState: VariableState, @@ -187,6 +182,14 @@ class LoopTransfer implements Transfer { } } +export class LoopSouffleMapper implements SouffleMapper { + public addDecls(ctx: Context): void {} + + public addRules(ctx: Context): void {} + + public addConstraints(ctx: Context): void {} +} + /** * A detector that analyzes loop conditions and control flow to ensure loops have proper termination criteria. * @@ -215,20 +218,17 @@ class LoopTransfer implements Transfer { * ``` */ export class UnboundLoops extends Detector { - check(_ctx: MistiContext, cu: CompilationUnit): MistiTactError[] { - cu.forEachCFG(cu.ast, (cfg: CFG, _: Node, stmt: ASTStatement) => { + check(ctx: MistiContext, cu: CompilationUnit): MistiTactError[] { + cu.forEachCFG(cu.ast, (cfg: CFG, _: Node, _stmt: ASTStatement) => { if (cfg.origin === "stdlib") { return; } - const lattice = new LoopVariablesLattice(); + const mapper = new LoopSouffleMapper(); + const solver = new SouffleSolver(this.id, ctx, cu, cfg, mapper); + const results = solver.solve(); + // TODO: Process results and generate warnings }); - // TODO: Create and solve dataflow equations using Souffle return []; } - - /** - * Collects dataflow info within a single loop statement. - */ - private collectLoopInfo(lattice: LoopVariablesLattice) {} } diff --git a/src/internals/ir.ts b/src/internals/ir.ts index e59e3e01..94b8ebad 100644 --- a/src/internals/ir.ts +++ b/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; +} diff --git a/src/internals/solver/index.ts b/src/internals/solver/index.ts index 0a0fde56..77afe333 100644 --- a/src/internals/solver/index.ts +++ b/src/internals/solver/index.ts @@ -1,3 +1,4 @@ -// export { SouffleSolver } from "./souffle"; +export { SouffleSolver, SouffleMapper } from "./souffle"; +export { Solver } from "./solver"; export { WorklistSolver } from "./worklist"; export { SolverResults } from "./results"; diff --git a/src/internals/solver/solver.ts b/src/internals/solver/solver.ts new file mode 100644 index 00000000..1cef27c6 --- /dev/null +++ b/src/internals/solver/solver.ts @@ -0,0 +1,8 @@ +import { SolverResults } from "./results"; + +/** + * A generic interface that defines dataflow-equations solvers. + */ +export interface Solver { + solve(): SolverResults; +} diff --git a/src/internals/solver/souffle.ts b/src/internals/solver/souffle.ts index f7ffca0b..dc4016d7 100644 --- a/src/internals/solver/souffle.ts +++ b/src/internals/solver/souffle.ts @@ -1,4 +1,153 @@ +import { + Context, + Fact, + FactType, + Relation, + SouffleExecutionResult, + FactValue, + Executor, + Rule, + RuleBody, + Atom, +} from "../souffle/"; +import { MistiContext } from "../context"; +import { ASTRef } from "@tact-lang/compiler/dist/grammar/ast"; +import { CFG, NodeIdx, CompilationUnit } from "../ir"; +import { SolverResults } from "./results"; +import { Solver } from "./solver"; + +/** + * Basic block definition added in all the Souffle programs. + */ +const BB_FACT = (idx: NodeIdx): string => `bb_${idx}`; + +/** + * An interface for a specific dataflow problem used to generate a Soufflé program. + * + * It is used to express the dataflow problem and serves the same purpose as the transfer + * function when using the worklist fixpoint algorithm. The join/meet semilattice + * operations should be expressed implicitly in the Soufflé rules. Maintaining the + * monotonicity property is a responsibility of the user, i.e. the designed rules + * must ensure that the dataflow information only grows or remains the same. + * + * When implementing definitions inside the functions of this interface, the user can refer + * to some fields that have special meanings and are added by the Soufflé solver by default: + * * `bb${index}` - Basic block with the given index + * * `edge` - Edge relations between two blocks + */ +export interface SouffleMapper { + /** + * Adds Souffle declarations specific for the dataflow problem. + * + * Example: + * `.decl var_defined(bb: symbol, var: symbol)` - Variables defined in dataflow + */ + addDecls(ctx: Context): void; + + /** + * Adds Souffle rules specific for the dataflow problem. + * + * Example: + * `out(bb, var) :- pred(bb, predBB), in(predBB, var).` - Computes the `out` state based on the `in` state + */ + addRules(ctx: Context): void; + + /** + * Adds Souffle facts to describe constraints for the dataflow problem. + * + * Example: + * `var_defined("bb4", "x").` - Variable `x` is defined within the basic block with index 4 + */ + addConstraints(ctx: Context): void; +} + /** * Provides a framework for solving dataflow analysis problems using the Soufflé solver. */ -export class SouffleSolver {} +export class SouffleSolver implements Solver { + /** + * @param lintId An unique identifier of the lint leveraging this solver. + * @param cu Compilation unit under the analysis. + * @param cfg CFG under the analysis. + * @param mapper An object that defines the transfer operation for a node and its state. + */ + constructor( + private readonly lintId: string, + private readonly ctx: MistiContext, + private readonly cu: CompilationUnit, + private readonly cfg: CFG, + private readonly mapper: SouffleMapper, + ) {} + + /** + * Adds common declarations to represent the dataflow problem. + * @param ctx The Souffle program where the relations are to be added. + */ + private addDataflowDecls(ctx: Context): void { + // Basic block declaration + ctx.add(Relation.from("bb", [["bb", FactType.Symbol]], undefined)); + // Predecessor declaration + ctx.add( + Relation.from( + "pred", + [ + ["bb_src", FactType.Symbol], + ["bb_dst", FactType.Symbol], + ], + undefined, + ), + ); + } + + /** + * Adds common facts to represent the dataflow problem. + * @param ctx The Souffle program where the relations are to be added. + */ + private addDataflowFacts(ctx: Context): void { + this.cfg.forEachNode(this.cu.ast, (stmt, node) => { + ctx.addFact("bb", Fact.from([BB_FACT(node.idx)])); + }); + // TODO: replace w/ predecessors? is it convinient to access that information in user-defined rules? + this.cfg.forEachEdge((edge) => { + ctx.addFact("edge", Fact.from([BB_FACT(edge.src), BB_FACT(edge.dst)])); + }); + } + + /** + * Executes the Souffle program generated within the solver. + */ + private execute(ctx: Context): SouffleExecutionResult { + const executor = this.ctx.config.soufflePath + ? new Executor({ + inputDir: this.ctx.config.soufflePath, + outputDir: this.ctx.config.soufflePath, + }) + : new Executor(); + return executor.executeSync(ctx); + } + + /** + * Converts the souffle execution results to the solver results as required by the class interface. + */ + private createSouffleResults( + souffleResults: Fact[], + ): SolverResults { + throw new Error("NYI"); + } + + public solve(): SolverResults { + const ctx: Context = new Context(this.lintId); + this.addDataflowDecls(ctx); + this.mapper.addDecls(ctx); + this.mapper.addRules(ctx); + this.addDataflowFacts(ctx); + this.mapper.addConstraints(ctx); + const result = this.execute(ctx); + if (!result.success) { + throw new Error(`Error executing Soufflé: ${result.stderr}`); + } + return this.createSouffleResults( + Array.from(result.results.entries.values()), + ); + } +} diff --git a/src/internals/solver/worklist.ts b/src/internals/solver/worklist.ts index 9ff6b273..3c70d2a0 100644 --- a/src/internals/solver/worklist.ts +++ b/src/internals/solver/worklist.ts @@ -1,6 +1,7 @@ import { JoinSemilattice } from "../lattice"; -import { CFG, Node, CompilationUnit } from "../ir"; +import { CFG, Node, CompilationUnit, getPredecessors } from "../ir"; import { SolverResults } from "./results"; +import { Solver } from "./solver"; import { Transfer } from "../transfer"; /** @@ -9,14 +10,14 @@ import { Transfer } from "../transfer"; * This class encapsulates the control flow graph (CFG), node state transformations, * and lattice properties necessary for the computation of fixpoints in dataflow equations. */ -export class WorklistSolver { +export class WorklistSolver implements Solver { private readonly cu: CompilationUnit; private readonly cfg: CFG; private transfer: Transfer; private readonly lattice: JoinSemilattice; /** - * @param transfer A function that defines the transfer operation for a node and its state. + * @param transfer An object that defines the transfer operation for a node and its state. * @param lattice An instance of a lattice that defines the join, bottom, and leq operations. */ constructor( @@ -31,16 +32,6 @@ export class WorklistSolver { this.lattice = lattice; } - private getPredecessors(node: Node): Node[] { - const predecessors = this.cfg.getPredecessors(node.idx); - if (predecessors === undefined) { - throw new Error( - `Incorrect definition in the CFG: Node #${node.idx} has an undefined predecessor`, - ); - } - return predecessors; - } - /** * Finds a fixpoint using the worklist algorithm. * @returns The results of solving the dataflow problem. @@ -56,7 +47,7 @@ export class WorklistSolver { while (worklist.length > 0) { const node = worklist.pop()!; - const inState = this.getPredecessors(node).reduce((acc, pred) => { + const inState = getPredecessors(this.cfg, node).reduce((acc, pred) => { return this.lattice.join(acc, results.getState(pred.idx)!); }, this.lattice.bottom()); @@ -70,10 +61,14 @@ export class WorklistSolver { if (!this.lattice.leq(outState, results.getState(node.idx)!)) { results.setState(node.idx, outState); - worklist.push(...this.getPredecessors(node)); + worklist.push(...getPredecessors(this.cfg, node)); } } return results; } + + public solve(): SolverResults { + return this.findFixpoint(); + } } diff --git a/src/internals/souffle/index.ts b/src/internals/souffle/index.ts index d0b9fca3..2d9ab02e 100644 --- a/src/internals/souffle/index.ts +++ b/src/internals/souffle/index.ts @@ -7,4 +7,4 @@ export { } from "./relation"; export { Atom, RuleHead, RuleName, RuleBody, Rule } from "./rule"; export { Context } from "./context"; -export { Executor } from "./executor"; +export { Executor, SouffleExecutionResult } from "./executor"; From cb86ab0166a6d8ef8e606de7bdf084ca4ea858a2 Mon Sep 17 00:00:00 2001 From: Byakuren Hijiri Date: Sun, 14 Jul 2024 10:35:00 +0000 Subject: [PATCH 4/6] feat(unboundLoops): The Souffle-based lint implementation --- src/detectors/builtin/unboundLoops.ts | 383 +++++++++++---------- src/detectors/detector.ts | 4 + src/internals/config.ts | 1 + test/contracts/unbound-loop-1.cfg.json | 49 +++ test/contracts/unbound-loop-1.expected.out | 1 + test/contracts/unbound-loop-1.tact | 6 + test/contracts/unbound-loop-2.cfg.json | 49 +++ test/contracts/unbound-loop-2.expected.out | 1 + test/contracts/unbound-loop-2.tact | 6 + test/contracts/unbound-loop-3.cfg.json | 70 ++++ test/contracts/unbound-loop-3.expected.out | 1 + test/contracts/unbound-loop-3.tact | 7 + test/contracts/unbound-loop-4.cfg.json | 77 +++++ test/contracts/unbound-loop-4.expected.out | 1 + test/contracts/unbound-loop-4.tact | 10 + test/contracts/zero-address.cfg.json | 4 +- 16 files changed, 478 insertions(+), 192 deletions(-) create mode 100644 test/contracts/unbound-loop-1.cfg.json create mode 100644 test/contracts/unbound-loop-1.expected.out create mode 100644 test/contracts/unbound-loop-1.tact create mode 100644 test/contracts/unbound-loop-2.cfg.json create mode 100644 test/contracts/unbound-loop-2.expected.out create mode 100644 test/contracts/unbound-loop-2.tact create mode 100644 test/contracts/unbound-loop-3.cfg.json create mode 100644 test/contracts/unbound-loop-3.expected.out create mode 100644 test/contracts/unbound-loop-3.tact create mode 100644 test/contracts/unbound-loop-4.cfg.json create mode 100644 test/contracts/unbound-loop-4.expected.out create mode 100644 test/contracts/unbound-loop-4.tact diff --git a/src/detectors/builtin/unboundLoops.ts b/src/detectors/builtin/unboundLoops.ts index cc3acef8..003151d5 100644 --- a/src/detectors/builtin/unboundLoops.ts +++ b/src/detectors/builtin/unboundLoops.ts @@ -1,194 +1,25 @@ import { ASTStatement, ASTRef, - ASTExpression, - ASTStatementWhile, - ASTStatementRepeat, - ASTStatementUntil, } from "@tact-lang/compiler/dist/grammar/ast"; +import { + Context, + Fact, + FactType, + Relation, + Executor, + Rule, + RuleBody, + Atom, +} from "../../internals/souffle"; import { Detector } from "../detector"; -import { SouffleSolver, SouffleMapper } from "../../internals/solver"; -import { JoinSemilattice } from "../../internals/lattice"; import { CompilationUnit, Node, CFG } from "../../internals/ir"; import { MistiContext } from "../../internals/context"; -import { Transfer } from "../../internals/transfer"; -import { Context } from "../../internals/souffle"; import { createError, MistiTactError, Severity } from "../../internals/errors"; -import { forEachExpression } from "../../internals/tactASTUtil"; - -type LoopRef = ASTRef; - -/** - * Describes a dataflow state of local variables within the loop construction. - */ -interface VariableState { - /** Variables defined within dataflow of the current function. */ - defined: Map; - /** Variables used in loop's condition. */ - condition: Map>; - /** Variables modified within loop's body. */ - modified: Map>; -} - -class LoopVariablesLattice implements JoinSemilattice { - bottom(): VariableState { - return { defined: new Map(), condition: new Map(), modified: new Map() }; - } - - join(a: VariableState, b: VariableState): VariableState { - const joinedDefined = this.mergeSimpleMaps(a.defined, b.defined); - const joinedCondition = this.mergeNestedMaps(a.condition, b.condition); - const joinedModified = this.mergeNestedMaps(a.modified, b.modified); - return { - defined: joinedDefined, - condition: joinedCondition, - modified: joinedModified, - }; - } - - leq(a: VariableState, b: VariableState): boolean { - return ( - this.areSimpleMapsSubsets(a.defined, b.defined) && - this.areNestedMapsSubsets(a.condition, b.condition) && - this.areNestedMapsSubsets(a.modified, b.modified) - ); - } - - private mergeSimpleMaps( - a: Map, - b: Map, - ): Map { - const mergedMap = new Map(a); - b.forEach((value, key) => mergedMap.set(key, value)); - return mergedMap; - } - - private mergeNestedMaps( - a: Map>, - b: Map>, - ): Map> { - const mergedMap = new Map(a); - b.forEach((innerMap, key) => { - if (mergedMap.has(key)) { - mergedMap.set(key, this.mergeSimpleMaps(mergedMap.get(key)!, innerMap)); - } else { - mergedMap.set(key, new Map(innerMap)); - } - }); - return mergedMap; - } - - private areSimpleMapsSubsets( - a: Map, - b: Map, - ): boolean { - return [...a].every(([key, value]) => b.has(key) && b.get(key) === value); - } - - private areNestedMapsSubsets( - a: Map>, - b: Map>, - ): boolean { - return [...a].every( - ([key, innerMap]) => - b.has(key) && this.areSimpleMapsSubsets(innerMap, b.get(key)!), - ); - } -} - -/** - * The transfer function used by the worklist-based solver. - */ -class LoopTransfer implements Transfer { - public transfer( - inState: VariableState, - _node: Node, - stmt: ASTStatement, - ): VariableState { - const outState = { ...inState }; - switch (stmt.kind) { - case "statement_let": - outState.defined.set(stmt.name, stmt.ref); - break; - case "statement_while": - this.processCondition(outState, stmt.ref, stmt.condition); - this.processBody(outState, stmt); - break; - case "statement_until": - this.processCondition(outState, stmt.ref, stmt.condition); - this.processBody(outState, stmt); - break; - case "statement_repeat": - this.processCondition(outState, stmt.ref, stmt.condition); - this.processBody(outState, stmt); - break; - default: - break; - } - return outState; - } - - /** - * Processes loop's condition collecting the variables defined in it to the out state. - */ - private processCondition( - outState: VariableState, - loopRef: ASTRef, - expr: ASTExpression, - ): void { - forEachExpression(expr, (expr) => { - if (expr.kind === "id" && outState.defined.has(expr.value)) { - this.setDefault(outState.condition, loopRef, expr.value, expr.ref); - } - }); - } - - /** - * Processes loop's body collecting information about variables used within the loop. - */ - private processBody( - outState: VariableState, - loop: ASTStatementWhile | ASTStatementRepeat | ASTStatementUntil, - ): void { - const conditionVars = outState.condition.get(loop.ref); - if (conditionVars === undefined) { - return; // Loop doesn't have variables in its condition - } - loop.statements.forEach((stmt) => { - forEachExpression(stmt, (expr) => { - // Find expressions that potentially modify a value of loop variables - if (expr.kind === "id" && conditionVars.has(expr.value)) { - this.setDefault(outState.modified, stmt.ref, expr.value, expr.ref); - } - }); - }); - } - - /** - * Ensures that a key-value pair is added to a nested map, initializing a new inner map if necessary. - */ - private setDefault( - outerMap: Map>, - loopRef: LoopRef, - innerKey: string, - innerValue: ASTRef, - ): void { - let innerMap = outerMap.get(loopRef); - if (!innerMap) { - innerMap = new Map(); - outerMap.set(loopRef, innerMap); - } - innerMap.set(innerKey, innerValue); - } -} - -export class LoopSouffleMapper implements SouffleMapper { - public addDecls(ctx: Context): void {} - - public addRules(ctx: Context): void {} - - public addConstraints(ctx: Context): void {} -} +import { + forEachExpression, + forEachStatement, +} from "../../internals/tactASTUtil"; /** * A detector that analyzes loop conditions and control flow to ensure loops have proper termination criteria. @@ -219,16 +50,188 @@ export class LoopSouffleMapper implements SouffleMapper { */ export class UnboundLoops extends Detector { check(ctx: MistiContext, cu: CompilationUnit): MistiTactError[] { - cu.forEachCFG(cu.ast, (cfg: CFG, _: Node, _stmt: ASTStatement) => { + // TODO: Extract method for this shared logic + const souffleCtx = new Context(this.id); + this.addDecls(souffleCtx); + this.addRules(souffleCtx); + this.addConstantConstraints(cu, souffleCtx); + this.addConstraints(cu, souffleCtx); + + const executor = ctx.config.soufflePath + ? new Executor({ + inputDir: ctx.config.soufflePath, + outputDir: ctx.config.soufflePath, + }) + : new Executor(); + 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): 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): 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, + ): 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): void { + cu.forEachCFG(cu.ast, (cfg: CFG, _: Node, stmt: ASTStatement) => { if (cfg.origin === "stdlib") { return; } - const mapper = new LoopSouffleMapper(); - const solver = new SouffleSolver(this.id, ctx, cu, cfg, mapper); - const results = solver.solve(); - // TODO: Process results and generate warnings + 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 = 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), + ); + } + }); + }); + } + } + }); + } }); - - return []; } } diff --git a/src/detectors/detector.ts b/src/detectors/detector.ts index a4160019..3e579cea 100644 --- a/src/detectors/detector.ts +++ b/src/detectors/detector.ts @@ -36,6 +36,10 @@ const BuiltInDetectors: Record Promise> = { 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()), }; diff --git a/src/internals/config.ts b/src/internals/config.ts index 75282b9f..f2825203 100644 --- a/src/internals/config.ts +++ b/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" }, ]; diff --git a/test/contracts/unbound-loop-1.cfg.json b/test/contracts/unbound-loop-1.cfg.json new file mode 100644 index 00000000..712351de --- /dev/null +++ b/test/contracts/unbound-loop-1.cfg.json @@ -0,0 +1,49 @@ +{ + "projectName": "unbound-loop-1", + "functions": [ + { + "name": "test", + "cfg": { + "nodes": [ + { + "id": 1063, + "stmtID": 14060, + "srcEdges": [], + "dstEdges": [ + 1065 + ] + }, + { + "id": 1064, + "stmtID": 14064, + "srcEdges": [ + 1065 + ], + "dstEdges": [ + 1066 + ] + }, + { + "id": 1067, + "stmtID": 14066, + "srcEdges": [], + "dstEdges": [] + } + ], + "edges": [ + { + "id": 1065, + "src": 1063, + "dst": 1064 + }, + { + "id": 1066, + "src": 1064, + "dst": 14066 + } + ] + } + } + ], + "contracts": [] +} \ No newline at end of file diff --git a/test/contracts/unbound-loop-1.expected.out b/test/contracts/unbound-loop-1.expected.out new file mode 100644 index 00000000..8b137891 --- /dev/null +++ b/test/contracts/unbound-loop-1.expected.out @@ -0,0 +1 @@ + diff --git a/test/contracts/unbound-loop-1.tact b/test/contracts/unbound-loop-1.tact new file mode 100644 index 00000000..88b9dabc --- /dev/null +++ b/test/contracts/unbound-loop-1.tact @@ -0,0 +1,6 @@ +fun test(): Int { + let a: Int = 20; + while (a > 10) { // error: a is not changing within the loop + } + return a; +} diff --git a/test/contracts/unbound-loop-2.cfg.json b/test/contracts/unbound-loop-2.cfg.json new file mode 100644 index 00000000..5fb597b9 --- /dev/null +++ b/test/contracts/unbound-loop-2.cfg.json @@ -0,0 +1,49 @@ +{ + "projectName": "unbound-loop-2", + "functions": [ + { + "name": "test", + "cfg": { + "nodes": [ + { + "id": 1212, + "stmtID": 16060, + "srcEdges": [], + "dstEdges": [ + 1214 + ] + }, + { + "id": 1213, + "stmtID": 16064, + "srcEdges": [ + 1214 + ], + "dstEdges": [ + 1215 + ] + }, + { + "id": 1216, + "stmtID": 16066, + "srcEdges": [], + "dstEdges": [] + } + ], + "edges": [ + { + "id": 1214, + "src": 1212, + "dst": 1213 + }, + { + "id": 1215, + "src": 1213, + "dst": 16066 + } + ] + } + } + ], + "contracts": [] +} \ No newline at end of file diff --git a/test/contracts/unbound-loop-2.expected.out b/test/contracts/unbound-loop-2.expected.out new file mode 100644 index 00000000..8b137891 --- /dev/null +++ b/test/contracts/unbound-loop-2.expected.out @@ -0,0 +1 @@ + diff --git a/test/contracts/unbound-loop-2.tact b/test/contracts/unbound-loop-2.tact new file mode 100644 index 00000000..3429387f --- /dev/null +++ b/test/contracts/unbound-loop-2.tact @@ -0,0 +1,6 @@ +fun test(): Int { + let a: Int = 20; + do { // error: a is not changing within the loop + } until (a > 10); + return a; +} diff --git a/test/contracts/unbound-loop-3.cfg.json b/test/contracts/unbound-loop-3.cfg.json new file mode 100644 index 00000000..df57cd98 --- /dev/null +++ b/test/contracts/unbound-loop-3.cfg.json @@ -0,0 +1,70 @@ +{ + "projectName": "unbound-loop-3", + "functions": [ + { + "name": "test", + "cfg": { + "nodes": [ + { + "id": 1361, + "stmtID": 18063, + "srcEdges": [], + "dstEdges": [ + 1363 + ] + }, + { + "id": 1362, + "stmtID": 18070, + "srcEdges": [ + 1363, + 1366 + ], + "dstEdges": [ + 1367 + ] + }, + { + "id": 1364, + "stmtID": 18069, + "srcEdges": [ + 1365 + ], + "dstEdges": [ + 1366 + ] + }, + { + "id": 1368, + "stmtID": 18072, + "srcEdges": [], + "dstEdges": [] + } + ], + "edges": [ + { + "id": 1363, + "src": 1361, + "dst": 1362 + }, + { + "id": 1365, + "src": 1362, + "dst": 1364 + }, + { + "id": 1366, + "src": 1364, + "dst": 1362 + }, + { + "id": 1367, + "src": 1362, + "dst": 18072 + } + ] + } + } + ], + "contracts": [] +} \ No newline at end of file diff --git a/test/contracts/unbound-loop-3.expected.out b/test/contracts/unbound-loop-3.expected.out new file mode 100644 index 00000000..8b137891 --- /dev/null +++ b/test/contracts/unbound-loop-3.expected.out @@ -0,0 +1 @@ + diff --git a/test/contracts/unbound-loop-3.tact b/test/contracts/unbound-loop-3.tact new file mode 100644 index 00000000..cbb669aa --- /dev/null +++ b/test/contracts/unbound-loop-3.tact @@ -0,0 +1,7 @@ +fun test(): Int { + let a: Int = 20; + while (a > 10) { // ok: a is changing within the loop + a += 1; + } + return a; +} diff --git a/test/contracts/unbound-loop-4.cfg.json b/test/contracts/unbound-loop-4.cfg.json new file mode 100644 index 00000000..d49732e4 --- /dev/null +++ b/test/contracts/unbound-loop-4.cfg.json @@ -0,0 +1,77 @@ +{ + "projectName": "unbound-loop-4", + "functions": [ + { + "name": "fn", + "cfg": { + "nodes": [], + "edges": [] + } + }, + { + "name": "test", + "cfg": { + "nodes": [ + { + "id": 1514, + "stmtID": 20075, + "srcEdges": [], + "dstEdges": [ + 1516 + ] + }, + { + "id": 1515, + "stmtID": 20082, + "srcEdges": [ + 1516, + 1519 + ], + "dstEdges": [ + 1520 + ] + }, + { + "id": 1517, + "stmtID": 20081, + "srcEdges": [ + 1518 + ], + "dstEdges": [ + 1519 + ] + }, + { + "id": 1521, + "stmtID": 20084, + "srcEdges": [], + "dstEdges": [] + } + ], + "edges": [ + { + "id": 1516, + "src": 1514, + "dst": 1515 + }, + { + "id": 1518, + "src": 1515, + "dst": 1517 + }, + { + "id": 1519, + "src": 1517, + "dst": 1515 + }, + { + "id": 1520, + "src": 1515, + "dst": 20084 + } + ] + } + } + ], + "contracts": [] +} \ No newline at end of file diff --git a/test/contracts/unbound-loop-4.expected.out b/test/contracts/unbound-loop-4.expected.out new file mode 100644 index 00000000..8b137891 --- /dev/null +++ b/test/contracts/unbound-loop-4.expected.out @@ -0,0 +1 @@ + diff --git a/test/contracts/unbound-loop-4.tact b/test/contracts/unbound-loop-4.tact new file mode 100644 index 00000000..74689416 --- /dev/null +++ b/test/contracts/unbound-loop-4.tact @@ -0,0 +1,10 @@ +fun fn(a: Int) { +} + +fun test(): Int { + let a: Int = 20; + while (a > 10) { // ok: a is using within the loop + fn(a); + } + return a; +} diff --git a/test/contracts/zero-address.cfg.json b/test/contracts/zero-address.cfg.json index c4cbf9ad..2ec16b42 100644 --- a/test/contracts/zero-address.cfg.json +++ b/test/contracts/zero-address.cfg.json @@ -10,8 +10,8 @@ "cfg": { "nodes": [ { - "id": 1063, - "stmtID": 14055, + "id": 1666, + "stmtID": 22073, "srcEdges": [], "dstEdges": [] } From 44b8462b26ffcf68e8063aceba4c76c7ba5171f7 Mon Sep 17 00:00:00 2001 From: Byakuren Hijiri Date: Sun, 14 Jul 2024 10:37:35 +0000 Subject: [PATCH 5/6] chore: Adjust examples --- examples/implicit-init/implicitInit.ts | 4 ---- examples/implicit-init/test/implicitInit.spec.ts | 2 +- test/contracts/never-accessed-1.expected.out | 7 +------ 3 files changed, 2 insertions(+), 11 deletions(-) diff --git a/examples/implicit-init/implicitInit.ts b/examples/implicit-init/implicitInit.ts index f4535cfb..36d24a9f 100644 --- a/examples/implicit-init/implicitInit.ts +++ b/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")) { diff --git a/examples/implicit-init/test/implicitInit.spec.ts b/examples/implicit-init/test/implicitInit.spec.ts index 8a636b87..3be57572 100644 --- a/examples/implicit-init/test/implicitInit.spec.ts +++ b/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. diff --git a/test/contracts/never-accessed-1.expected.out b/test/contracts/never-accessed-1.expected.out index 59884c3f..8b137891 100644 --- a/test/contracts/never-accessed-1.expected.out +++ b/test/contracts/never-accessed-1.expected.out @@ -1,6 +1 @@ -test/contracts/never-accessed-1.tact:2:5: - 1 | fun test(): Int { -> 2 | let a: Int = 20; - ^ - 3 | if (true) { // error: write-only variable -Variable a is never accessed + From 2e7307da0c2a7ae95716baa45a1600f27f7269c1 Mon Sep 17 00:00:00 2001 From: Byakuren Hijiri Date: Sun, 14 Jul 2024 10:37:47 +0000 Subject: [PATCH 6/6] chore: fix ESLint warnings and prettier formatting --- src/detectors/builtin/neverAccessedVariables.ts | 2 +- src/detectors/builtin/unboundLoops.ts | 11 ++++++----- src/internals/solver/souffle.ts | 7 ++----- 3 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/detectors/builtin/neverAccessedVariables.ts b/src/detectors/builtin/neverAccessedVariables.ts index c39fe4ce..c2f637e3 100644 --- a/src/detectors/builtin/neverAccessedVariables.ts +++ b/src/detectors/builtin/neverAccessedVariables.ts @@ -149,7 +149,7 @@ 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; } diff --git a/src/detectors/builtin/unboundLoops.ts b/src/detectors/builtin/unboundLoops.ts index 003151d5..0ead5995 100644 --- a/src/detectors/builtin/unboundLoops.ts +++ b/src/detectors/builtin/unboundLoops.ts @@ -1,7 +1,4 @@ -import { - ASTStatement, - ASTRef, -} from "@tact-lang/compiler/dist/grammar/ast"; +import { ASTStatement, ASTRef } from "@tact-lang/compiler/dist/grammar/ast"; import { Context, Fact, @@ -72,7 +69,11 @@ export class UnboundLoops extends Detector { 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 createError( + "Unbounded loop: the condition variable doesn't change within the loop", + Severity.MEDIUM, + fact.data, + ); }); return warnings; diff --git a/src/internals/solver/souffle.ts b/src/internals/solver/souffle.ts index dc4016d7..8e5a342a 100644 --- a/src/internals/solver/souffle.ts +++ b/src/internals/solver/souffle.ts @@ -6,9 +6,6 @@ import { SouffleExecutionResult, FactValue, Executor, - Rule, - RuleBody, - Atom, } from "../souffle/"; import { MistiContext } from "../context"; import { ASTRef } from "@tact-lang/compiler/dist/grammar/ast"; @@ -104,7 +101,7 @@ export class SouffleSolver implements Solver { * @param ctx The Souffle program where the relations are to be added. */ private addDataflowFacts(ctx: Context): void { - this.cfg.forEachNode(this.cu.ast, (stmt, node) => { + this.cfg.forEachNode(this.cu.ast, (_stmt, node) => { ctx.addFact("bb", Fact.from([BB_FACT(node.idx)])); }); // TODO: replace w/ predecessors? is it convinient to access that information in user-defined rules? @@ -130,7 +127,7 @@ export class SouffleSolver implements Solver { * Converts the souffle execution results to the solver results as required by the class interface. */ private createSouffleResults( - souffleResults: Fact[], + _souffleResults: Fact[], ): SolverResults { throw new Error("NYI"); }