feat(cellUnderflow): Support storing local builders/slices

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<CellUnderflowState> {
         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<CellUnderflowState> {
     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<CellUnderflowState> {
     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.
    *

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

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();
 }