`delete x` on a state variable does not erase knowledge of storage pointers aliasing `x` (false "safe")

Open
  • Is something wrong?
#17,159 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
45/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Tech stack
cpp, solidity
Domain
compilers, testing

Research direction

The report points to libsolidity/formal/SMTEncoder.cpp, specifically endVisit(UnaryOperation) for Token::Delete and assignment(); read those paths and the linked change for #10847 first. Run the supplied C.sol reproducer with the stated SMTChecker commands, then compare its assertions with runtime behavior. Done means CHC and BMC report violations for the cases that fail at runtime, including the expected behavior after deleting the struct and array.

Written by the indexing model from the issue text.

Description

smt

Found by comparing the semantics described in the Solidity documentation with how the Solidity SMTChecker implements them. An AI agent found this bug, reproduced it with solc 35b1cb80 (develop) and drafted this report. A second agent tried to refute it and searched upstream for duplicates. The methodology is described here.

Target detail: solc SMTChecker (CHC, also BMC)

What went wrong: Wrong result (assertion that fails at runtime is reported "safe")

Version: 0.8.37+commit.f401782d (static release binary, built-in z3). Also reproduces at upstream develop 3eb0c3ac (built from source, -DUSE_Z3=ON).

Preconditions: none beyond default CHC engine; a local storage pointer to a state struct/array that is then deleted.

Input

C.sol:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract C {
    struct S { uint x; }
    S s;
    uint[] arr;

    // `delete` of a state variable does not invalidate a local storage pointer to it
    function f(uint v) public {
        s.x = v;
        S storage r = s;
        delete s;
        assert(r.x == v);
    }

    function g(uint v) public {
        arr.push(v);
        uint[] storage p = arr;
        delete arr;
        assert(p.length == 1);
    }
}
Command
SOLC=/path/to/solc ./run.sh   # exit 1 = bug reproduced, 0 = fixed, 2 = tool missing / harness error

solc --model-checker-engine chc --model-checker-targets assert --model-checker-show-proved-safe C.sol
Output

(develop 3eb0c3ac; 0.8.37 prints the same without the pre-release warning)

Warning: This is a pre-release compiler version, please do not use it in production.

Info: CHC: Assertion violation check is safe!
  --> C.sol:13:9:
   |
13 |         assert(r.x == v);
   |         ^^^^^^^^^^^^^^^^

Info: CHC: Assertion violation check is safe!
  --> C.sol:20:9:
   |
20 |         assert(p.length == 1);
   |         ^^^^^^^^^^^^^^^^^^^^^

BMC (--model-checker-engine bmc) also reports line 13 safe. Executing the 0.8.37 runtime code with calldata f(1) / g(1) on geth 1.17.8 and EELS (osaka) reverts with Panic(0x01) in both cases.

Expected

Violations at lines 13 and 20. The docs (Types > delete) say delete a "really behaves like an assignment to a", and their DeleteExample has uint[] storage y = dataArray; delete dataArray; ... assert(y.length == 0);. SMTChecker docs ("Abstraction and False Positives") promise no false negatives, and ("Reference Types and Aliasing") that on assignment "all knowledge regarding variables of the same type and data location is erased". The mirror case is also wrong: assert(r.x == 0) after delete s, and the docs' own assert(y.length == 0), are reported as "Assertion violation happens here" (counterexample y = [1]).

Location: libsolidity/formal/SMTEncoder.cpp:503-507 (endVisit(UnaryOperation), Token::Delete, identifier case) calls newValue/setZeroValue but not resetReferences(*decl), unlike assignment() (:2138-2140, added for #10847 by #11097).

Reproducer files

C.sol

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract C {
    struct S { uint x; }
    S s;
    uint[] arr;

    // `delete` of a state variable does not invalidate a local storage pointer to it
    function f(uint v) public {
        s.x = v;
        S storage r = s;
        delete s;
        assert(r.x == v);
    }

    function g(uint v) public {
        arr.push(v);
        uint[] storage p = arr;
        delete arr;
        assert(p.length == 1);
    }
}

oracle.sh

# Concrete EVM oracle: go-ethereum's `evm` tool (set EVM=/path/to/evm; default: from PATH).
# oracle RUNTIME_HEX [CALLDATA_HEX] [VALUE_WEI] -> one JSON line {status, error, returndata, storage, logs}; rc 2 on tool error.
EVM="${EVM:-evm}"
oracle() {
  local o e rc g=(); o=$(mktemp /tmp/oracle-o.XXXXXX); e=$(mktemp /tmp/oracle-e.XXXXXX)
  if [ "${3:-0}" != 0 ]; then  # fund the sender so a value transfer is possible
    g=(--prestate "$o.g" --sender 0x0000000000000000000000000000000000000001)
    echo '{"config":{"chainId":1,"homesteadBlock":0,"eip150Block":0,"eip155Block":0,"eip158Block":0,"byzantiumBlock":0,"constantinopleBlock":0,"petersburgBlock":0,"istanbulBlock":0,"berlinBlock":0,"londonBlock":0,"mergeNetsplitBlock":0,"shanghaiTime":0,"cancunTime":0,"pragueTime":0,"terminalTotalDifficulty":0,"blobSchedule":{"cancun":{"target":3,"max":6,"baseFeeUpdateFraction":3338477},"prague":{"target":6,"max":9,"baseFeeUpdateFraction":5007716}}},"alloc":{"0x0000000000000000000000000000000000000001":{"balance":"0xffffffffffffffff"}},"difficulty":"0x0","gasLimit":"0x1000000","timestamp":"0x0"}' > "$o.g"
  fi
  "$EVM" run --gas 10000000 --input "${2:-}" --value "${3:-0}" "${g[@]}" --dump --trace "$1" >"$o" 2>"$e"; rc=$?
  [ $rc -eq 0 ] && python3 -I - "$o" "$e" <<'PY'
import json,sys
o,e=open(sys.argv[1]).read(),open(sys.argv[2]).read()
tr=[json.loads(l) for l in e.splitlines() if l.startswith('{')]
last=tr[-1]; err=last.get("error","")
logs=sum(1 for t in tr if str(t.get("opName","")).startswith("LOG"))
accts=json.loads(o[o.index('{'):]).get("accounts",{})
st={}
for a in accts.values(): st.update(a.get("storage",{}))
print(json.dumps({"status":"error" if err else "success","error":err,"returndata":"0x"+last.get("output",""),"storage":st,"logs":logs}))
PY
  rc=$?; rm -f "$o" "$o.g" "$e"; [ $rc -eq 0 ] || echo "harness error: evm run failed" >&2; return $rc
}

run.sh

#!/usr/bin/env bash
# Repro: solc SMTChecker proves assertions safe that fail (Panic 0x01) on geth.
# CALLS lists "function-name:hex-encoded-args"; each call must fail its assert on the oracle,
# and SMTChecker (engines in ENGINES) must report "Assertion violation check is safe!" for it.
# exit 1 = bug present, 0 = correct, 2 = harness error.
set -u
D="$(cd "$(dirname "$0")" && pwd)"
# Tools (override via env; defaults are looked up on PATH): SOLC, EVM (go-ethereum `evm`, the concrete oracle).
S="$(command -v "${SOLC:-solc}")" || { echo "harness error: solc not found (set SOLC)"; exit 2; }
source "$D/oracle.sh"
ENGINES="chc bmc"
ORACLES="${ORACLES:-geth}"; NO=$(echo $ORACLES | wc -w)
CALLS="f:0000000000000000000000000000000000000000000000000000000000000001 g:0000000000000000000000000000000000000000000000000000000000000001"
"$S" --version | tail -n 1
declare -A safe_at
for eng in $ENGINES; do
  out="$("$S" --model-checker-engine $eng --model-checker-targets assert,underflow,overflow,divByZero,outOfBounds,popEmptyArray \
        --model-checker-show-proved-safe --model-checker-show-unproved "$D/C.sol" 2>&1)" || { echo "harness error: solc"; exit 2; }
  echo "--- SMTChecker $eng (verdict + location):"
  echo "$out" | grep -E "^(Info|Warning): (CHC|BMC)|^ *--> " | grep -B1 -E "^ *-->" | grep -v '^--$' | paste -d' ' - - | sed "s#$D/##"
  for ln in $(echo "$out" | grep -A1 "Assertion violation check is safe" | grep -oE "C.sol:[0-9]+" | cut -d: -f2); do safe_at[$eng:$ln]=1; done
done
code="$("$S" --bin-runtime "$D/C.sol" | tail -n 1)"; hs="$("$S" --hashes "$D/C.sol")"
[ -n "$code" ] || { echo "harness error: compile"; exit 2; }
bugs=0; total=0
for c in $CALLS; do
  fn="${c%%:*}"; args="${c#*:}"; total=$((total+1))
  sel="$(echo "$hs" | grep -E "^[0-9a-f]{8}: $fn\(" | cut -c1-8)"; [ -n "$sel" ] || { echo "harness error: no selector $fn"; exit 2; }
  ln="$(grep -n "function $fn(" "$D/C.sol" | cut -d: -f1)"
  aline="$(awk -v s="$ln" 'NR>s && /assert\(/ {print NR; exit}' "$D/C.sol")"
  echo "--- $fn: concrete run calldata 0x$sel$args (assert at C.sol:$aline)"
  p=0
  for o in $ORACLES; do
    j="$(oracle "$code" "$sel$args")" || { echo "harness error: $o"; exit 2; }
    echo "$o: $j"
    echo "$j" | grep -q '"returndata": *"0x4e487b710000000000000000000000000000000000000000000000000000000000000001"' && p=$((p+1))
  done
  s=""; for eng in $ENGINES; do [ -n "${safe_at[$eng:$aline]:-}" ] && s="$s $eng"; done
  echo "$fn: oracles failing the assert $p/$NO; SMTChecker engines claiming safe:${s:- none}"
  [ $p -ne $NO ] && [ $p -ne 0 ] && { echo "harness error: oracles disagree"; exit 2; }
  [ $p -eq $NO ] && [ -n "$s" ] && bugs=$((bugs+1))
done
echo "wrong 'safe' verdicts: $bugs/$total"
[ $bugs -gt 0 ] && { echo "BUG: assertion(s) proved safe but fail on EVM"; exit 1; }
exit 0

If this is intended behaviour or a duplicate, feel free to close it, and I'll use that as feedback to improve future reports. For questions, or to have this re-checked on a newer version of the Solidity SMTChecker, mention @JeroenRobben or email [email protected].

Dominant language
C++
Stars
25.8k
Forks
6.2k
Avg merge
1d 22h
Merged PRs (30d)
43

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from argotorg/solidity

All issues in argotorg/solidity

Similar issues

More C++ issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.