From 6f3b112e90ccc8c88663bdcfd28bd9b4ad2eb543 Mon Sep 17 00:00:00 2001 From: Georgiy Komarov Date: Sun, 17 Nov 2024 13:08:50 +0000 Subject: [PATCH] feat(cellUnderflow): Support storing local builders/slices --- src/detectors/builtin/cellUnderflow.ts | 76 ++++++++++++++++++++++- test/detectors/CellUnderflow.expected.out | 42 +++++++++---- test/detectors/CellUnderflow.tact | 19 +++++- 3 files changed, 122 insertions(+), 15 deletions(-) diff --git a/src/detectors/builtin/cellUnderflow.ts b/src/detectors/builtin/cellUnderflow.ts index 4b49cd56..85ed8f1a 100644 --- a/src/detectors/builtin/cellUnderflow.ts +++ b/src/detectors/builtin/cellUnderflow.ts @@ -56,6 +56,14 @@ type StorageValue = { loaded: Interval; }; +const undecidableStorageValue = (): StorageValue => { + return { + undecidable: true, + stored: Interval.EMPTY, + loaded: Interval.EMPTY, + }; +}; + /** * Tracks data stored by this variable. * It includes only statically decidable information. Storage operations with @@ -72,6 +80,13 @@ type VariableStorage = { dataSize: StorageValue; }; +const undecidableVariableStorage = (): VariableStorage => { + return { + refsNum: undecidableStorageValue(), + dataSize: undecidableStorageValue(), + }; +}; + /** * Variable which has a point of definition. */ @@ -506,6 +521,11 @@ class CellUnderflowTransfer implements Transfer { variable.value.storage.dataSize.loaded.plus(loadSize); return; } + const localVariablesSize = this.getLocalVariablesSize(out, variable, call); + if (localVariablesSize !== undefined) { + variable.value.storage = localVariablesSize; + return; + } } /** @@ -567,12 +587,13 @@ class CellUnderflowTransfer implements Transfer { if (variable.value.kind !== VariableKind.Builder) { return undefined; } + // Try to extract constant store size const size = getConstantStoreSize(call); if (size !== undefined) { return Interval.fromNum(size); } - // TODO: use local variables from `out` + // TODO set undecidable if `store` call but the size is undecidable return undefined; } @@ -603,6 +624,59 @@ class CellUnderflowTransfer implements Transfer { return undefined; } + /** + * Updates storage tracking when builders/slices are stored into other builders. + * + * @param out Current dataflow state containing tracked variables + * @param variable Variable being modified (the builder storing data) + * @param call The storeBuilder/storeSlice method call + * @returns Updated storage state after combining variables, or undefined if not a store operation. + * Returns undecidable storage if the stored variable can't be tracked. + */ + private getLocalVariablesSize( + out: CellUnderflowState, + variable: VariableRhs, + call: AstMethodCall, + ): VariableStorage | undefined { + if (["storeBuilder", "storeSlice"].includes(idText(call.method))) { + // Try to find a stored builder in the dataflow state. + const arg = call.args[0]; + if (arg.kind === "id") { + const builderName = idText(arg) as VariableName; + const builder = out.builders.get(builderName); + if (builder) { + const { storage: varStorage } = variable.value; + const { storage: builderStorage } = builder; + return { + dataSize: { + undecidable: + varStorage.dataSize.undecidable && + builderStorage.dataSize.undecidable, + stored: varStorage.dataSize.stored.plus( + builderStorage.dataSize.stored, + ), + loaded: varStorage.dataSize.loaded, + }, + refsNum: { + undecidable: + varStorage.refsNum.undecidable && + builderStorage.refsNum.undecidable, + stored: varStorage.refsNum.stored.plus( + builderStorage.refsNum.stored, + ), + loaded: varStorage.refsNum.loaded, + }, + }; + } + } + // Unknown Builder/Slice => size is statically undecidable + return undecidableVariableStorage(); + } + + // The call doesn't involve any operations with local variables. + return undefined; + } + /** * Defines or reassignes a new variable in the output state. * diff --git a/test/detectors/CellUnderflow.expected.out b/test/detectors/CellUnderflow.expected.out index c5c6b147..3f8530d3 100644 --- a/test/detectors/CellUnderflow.expected.out +++ b/test/detectors/CellUnderflow.expected.out @@ -1,29 +1,49 @@ [CRITICAL] CellUnderflow: Reference count might go below 0 test/detectors/CellUnderflow.tact:2:9: 1 | fun refs_num_bad(c: Cell) { -> 2 | let s1 = beginCell().storeRef(c).endCell().asSlice(); +> 2 | let s1 = beginCell() ^ - 3 | let ref1 = s1.loadRef(); // OK + 3 | .storeRef(c) The possible number of references stored (1) is less than loaded (2) Help: Remove extra .loadRef operations or store more refs first See: https://nowarp.io/tools/misti/docs/detectors/CellUnderflow [CRITICAL] CellUnderflow: Reference count might go below 0 -test/detectors/CellUnderflow.tact:4:9: - 3 | let ref1 = s1.loadRef(); // OK -> 4 | let ref2 = s1.loadRef(); // Bad: Cell Underflow +test/detectors/CellUnderflow.tact:7:9: + 6 | let ref1 = s1.loadRef(); // OK +> 7 | let ref2 = s1.loadRef(); // Bad: Cell Underflow ^ - 5 | + 8 | The possible number of references stored (1) is less than loaded (2) Help: Remove extra .loadRef operations or store more refs first See: https://nowarp.io/tools/misti/docs/detectors/CellUnderflow [CRITICAL] CellUnderflow: Reference count might go below 0 -test/detectors/CellUnderflow.tact:7:5: - 6 | // Bad: Cell Underflow -> 7 | beginCell() - ^ - 8 | .endCell() +test/detectors/CellUnderflow.tact:9:5: + 8 | +> 9 | beginCell() + ^ + 10 | .endCell() +The possible number of references stored (0) is less than loaded (1) +Help: Remove extra .loadRef operations or store more refs first +See: https://nowarp.io/tools/misti/docs/detectors/CellUnderflow + +[CRITICAL] CellUnderflow: Reference count might go below 0 +test/detectors/CellUnderflow.tact:15:5: + 14 | // Cell Overflow when storing a known local builder +> 15 | let b1 = beginCell() + ^ + 16 | .storeRef(c) +The possible number of references stored (0) is less than loaded (1) +Help: Remove extra .loadRef operations or store more refs first +See: https://nowarp.io/tools/misti/docs/detectors/CellUnderflow + +[CRITICAL] CellUnderflow: Reference count might go below 0 +test/detectors/CellUnderflow.tact:20:5: + 19 | .storeRef(c); // OK: Builder storing 4 references +> 20 | let c1 = beginCell() + ^ + 21 | .storeBuilder(b1) The possible number of references stored (0) is less than loaded (1) Help: Remove extra .loadRef operations or store more refs first See: https://nowarp.io/tools/misti/docs/detectors/CellUnderflow \ No newline at end of file diff --git a/test/detectors/CellUnderflow.tact b/test/detectors/CellUnderflow.tact index 2fc59203..c29ef745 100644 --- a/test/detectors/CellUnderflow.tact +++ b/test/detectors/CellUnderflow.tact @@ -1,11 +1,24 @@ fun refs_num_bad(c: Cell) { - let s1 = beginCell().storeRef(c).endCell().asSlice(); + let s1 = beginCell() + .storeRef(c) + .endCell() + .asSlice(); let ref1 = s1.loadRef(); // OK let ref2 = s1.loadRef(); // Bad: Cell Underflow - // Bad: Cell Underflow beginCell() .endCell() .asSlice() - .loadRef(); + .loadRef(); // Bad: Cell Underflow + + // Cell Overflow when storing a known local builder + let b1 = beginCell() + .storeRef(c) + .storeRef(c) + .storeRef(c) + .storeRef(c); // OK: Builder storing 4 references + let c1 = beginCell() + .storeBuilder(b1) + .storeRef(c) // Bad: We got 5 references + .endCell(); }