shift amount is reduced modulo 2^(width of left operand), so `int8(5) >> 256` is proved equal to 5

Open
  • Is something wrong?
#17,161 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
48/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Tech stack
cpp, solidity
Domain
compilers, testing

Research direction

The issue points to libsolidity/formal/SMTEncoder.cpp:1960, in bitwiseOperation, and includes a Solidity reproducer in C.sol. Read the shift encoding and run the supplied run.sh with solc and the EVM oracle available. Done means the SMTChecker reports the assertion violation for the reproducer and its result agrees with EVM behavior for the described shift cases.

Written by the indexing model from the issue text.

Description

smt

Found by comparing the semantics described in the Solidity docs 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 and BMC)

What went wrong: Wrong result (a failing assertion is reported safe; counterexamples that do not replay)

Version: 0.8.37+commit.f401782d (static linux release). Also reproduces at develop nightly 0.8.38-nightly.2026.10.19+commit.4c8a81af (soljson, CHC).

Preconditions: SMTChecker enabled (CHC default engine, or BMC); shift amount of a wider type than the left operand that can reach ≥ 2^(bits of left operand), e.g. a uint256 shifting an int8/uint8/bytes1 (≥ 256) or a uint32/bytes4 (≥ 2^32).

Input
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract C {
  function f(int8 a, uint256 s) public pure {
    require(a == 5 && s == 256);
    int8 r = a >> s;
    assert(r == a);
  }
}
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
Info: CHC: Assertion violation check is safe!
 --> C.sol:7:5:
  |
7 |     assert(r == a);
  |     ^^^^^^^^^^^^^^
Command
# runtime bytecode of C.sol (solc --bin-runtime), calldata f(5, 256)
geth evm / revm: run --code <runtime> --calldata a4797c9b<int8 5><uint256 256>
Output
{"tool": "geth", "fork": "osaka", "status": "revert", "returndata": "0x4e487b710000000000000000000000000000000000000000000000000000000000000001", "gas_used": 22047, "logs": [], "storage": {}, "error": "execution reverted"}
{"tool":"revm","fork":"osaka","status":"revert","returndata":"0x4e487b710000000000000000000000000000000000000000000000000000000000000001","gas_used":22047,"logs":[],"storage":{},"error":"execution reverted"}
Expected

An assertion violation for f(5, 256). Docs (Types > Integers > Shifts): "x >> y is equivalent to the mathematical expression x / 2**y, rounded towards negative infinity", so 5 >> 256 == 0; EIP-145 gives 0 for SAR by ≥ 256, and the compiled code panics with 0x01 as shown.

With s == 255 the violation is reported correctly. Also affected: uint8(1) << s, bytes1 >> s, int16 >> 65536, uint32/bytes4 >> 2**32, >>=/<<=, literal a >> 256, BMC as well. The converse also happens: for uint8 r = x << s; assert(r == 0 || s < 8) with x == 1, CHC reports the counterexample s = 258, r = 4, which does not fail on the EVM. Location: libsolidity/formal/SMTEncoder.cpp:1960 (bitwiseOperation): int2bv(_right, bvSize) with bvSize the width of the left operand's type.

Reproducer files

C.sol

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract C {
  function f(int8 a, uint256 s) public pure {
    require(a == 5 && s == 256);
    int8 r = a >> s;
    assert(r == a);
  }
}

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 an assertion safe that fails (Panic 0x01) on geth.
# exit 1 = bug present (SMTChecker "safe" AND oracles show Panic(1)), 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"
"$S" --version | tail -n 1
CALLDATA_ARGS="00000000000000000000000000000000000000000000000000000000000000050000000000000000000000000000000000000000000000000000000000000100"
smt_bug=0
for eng in chc bmc; do
  out="$("$S" --model-checker-engine $eng --model-checker-targets assert,underflow,overflow,divByZero,outOfBounds \
        --model-checker-show-proved-safe --model-checker-show-unproved "$D/C.sol" 2>&1)" || { echo "harness error: solc"; exit 2; }
  echo "--- SMTChecker $eng:"; echo "$out" | grep -E "^(Info|Warning): (CHC|BMC)" 
  echo "$out" | grep -q "Assertion violation check is safe" && smt_bug=$((smt_bug+1))
done
code="$("$S" --bin-runtime "$D/C.sol" | tail -n 1)"
sel="$("$S" --hashes "$D/C.sol" | grep -oE '^[0-9a-f]{8}: f\(' | cut -c1-8)"
[ -n "$code" ] && [ -n "$sel" ] || { echo "harness error: compile"; exit 2; }
cd_hex="$sel$CALLDATA_ARGS"
echo "--- concrete run f(...) calldata 0x$cd_hex"
panic=0
for o in geth; do
  j="$(oracle "$code" "$cd_hex")" || { echo "harness error: $o"; exit 2; }
  echo "$o: $j"
  echo "$j" | grep -q '"returndata": *"0x4e487b710000000000000000000000000000000000000000000000000000000000000001"' && panic=$((panic+1))
done
echo "SMTChecker engines claiming safe: $smt_bug/2; oracles failing the assert (Panic 0x01): $panic/1"
if [ $smt_bug -gt 0 ] && [ $panic -eq 1 ]; then echo "BUG: assertion proved safe but fails on EVM"; exit 1; fi
if [ $panic -ne 1 ] && [ $panic -ne 0 ]; then echo "harness error: oracles disagree"; exit 2; fi
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.