// SPDX-License-Identifier: MIT
pragma solidity ^0.8.15;
import "forge-std/Test.sol";
import {console2} from "forge-std/console2.sol";
import {SymTest} from "halmos-cheatcodes/SymTest.sol";
contract Target {
address excludedSender;
constructor(address _excludedSender) {
excludedSender = _excludedSender;
}
function rejectsExcludedSender() external {
assert(msg.sender != excludedSender);
}
}
contract Test138 is Test, SymTest {
Target target;
function setUp() public {
address excludedSender = svm.createAddress("excluded");
target = new Target(excludedSender);
// excludeSender(excludedSender);
}
function invariant_excludeSender() external {
// nothing to do
}
}halmos --function invariant_excludeSender -vvvvv --debug --dump-smt-queries
DEBUG Running forge build --ast --root /Users/karma/projects/halmos-sandbox --extra-output storageLayout metadata
[⠔] Compiling...
No files changed, compilation skipped
DEBUG Skipped console2.json, no contract definition found
Running 1 tests for test/138_excludeSender.t.sol:Test138
Generating SMT queries in /var/folders/p9/s6g8495n6dqdjq3nn8hkdn840000gn/T/setUp-in51_sfo
Constructor trace:
⠼ Parsing /Users/karma/projects/halmos-sandbox/out CREATE Test138::<0 bytes of initcode>
SLOAD @12 → 0x00
SSTORE @12 ← 0x0000000000000000000000000000000000000000000000000000000000000001
SLOAD @31 → 0x00
SSTORE @31 ← 0x0000000000000000000000000000000000000000000000000000000000000001
↩ RETURN <4538 bytes of code>
DEBUG Address 0xf3993a62377bcd56ae39d773740a5390411e8bc9 not in: [0x7fa9385be102ac3eac297483dd6233d62b3e1496]
DEBUG Empty address: 0xf3993a62377bcd56ae39d773740a5390411e8bc9
setUp() trace #0:
⠼ Parsing /Users/karma/projects/halmos-sandbox/out CALL Test138::setUp() (caller: 0x1804c8ab1f12e6bbf3894d4083f33e07309d1f38)
STATICCALL svm::createAddress(0x000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000000086578636c75646564000000000000000000000000000000000000000000000000) [static] (caller: Test138)
↩ Concat(0x000000000000000000000000, halmos_excluded_address_44aa7dd_01)
CREATE Target::<351 bytes of initcode>
SLOAD @0 → 0x00
SSTORE @0 ← Concat(0x000000000000000000000000, halmos_excluded_address_44aa7dd_01)
↩ RETURN <186 bytes of code>
SLOAD @31 → 0x0000000000000000000000000000000000000000000000000000000000000001
SSTORE @31 ← 0x000000000000000000000000000000000000000000000000000000aaaa000201
↩ STOP 0x
╭──── Initial Invariant Target Functions ─────╮
│ 138_excludeSender.t.sol:Target @ 0xaaaa0002 │
│ └── rejectsExcludedSender() │
╰─────────────────────────────────────────────╯
Generating SMT queries in /var/folders/p9/s6g8495n6dqdjq3nn8hkdn840000gn/T/invariant_excludeSender-fpdnjmvo
Executing invariant_excludeSender
Path #0:
- (empty path condition)
Trace:
CALL Test138::invariant_excludeSender() (caller: 0x1804c8ab1f12e6bbf3894d4083f33e07309d1f38)
↩ STOP 0x
Generating SMT queries in /var/folders/p9/s6g8495n6dqdjq3nn8hkdn840000gn/T/_compute_frontier-g409ypbz
Found potential path with path_id=2 Panic(0x01)
Checking path condition path_id=2
DEBUG Writing SMT query to /var/folders/p9/s6g8495n6dqdjq3nn8hkdn840000gn/T/_compute_frontier-g409ypbz/2.smt2
DEBUG Found yices-2.6.4 binary in PATH: /Users/karma/projects/halmos/.venv/bin/yices-smt2
DEBUG Solver command for 'yices': /Users/karma/projects/halmos/.venv/bin/yices-smt2 --smt2-model-format --bvconst-in-decimal
Checking with external solver process
/Users/karma/projects/halmos/.venv/bin/yices-smt2 --smt2-model-format --bvconst-in-decimal /var/folders/p9/s6g8495n6dqdjq3nn8hkdn840000gn/T/_compute_frontier-g409ypbz/2.smt2 > /var/folders/p9/s6g8495n6dqdjq3nn8hkdn840000gn/T/_compute_frontier-g409ypbz/2.smt2.out
Generating SMT queries in /var/folders/p9/s6g8495n6dqdjq3nn8hkdn840000gn/T/_compute_frontier-0yuxxmmh
[PASS] invariant_excludeSender() (paths: 1, time: 0.04s, bounds: [])
DEBUG sat
Symbolic test result: 1 passed; 0 failed; time: 0.10s
Assertion failure detected in Target.rejectsExcludedSender()
Trace #2:
CALL Target::0x8d1543d3() (value: halmos_msg_value_0x00000000000000000000000000000000aaaa0002_96e3b90_04) (caller: halmos_msg_sender_0x00000000000000000000000000000000aaaa0002_751c549_03)
SLOAD @0 → Concat(0x000000000000000000000000, halmos_excluded_address_44aa7dd_01)
↩ REVERT 0x4e487b710000000000000000000000000000000000000000000000000000000000000001 (error: Revert())
Counterexample:
halmos_excluded_address_44aa7dd_01 = 0x00
halmos_msg_sender_0x00000000000000000000000000000000aaaa0002_751c549_03 = 0x00
⠴ Test138: depth: 1 | starting states: 1 | unique states: 1 | frontier states: 0 | completed paths: 0 halmos_msg_value_0x00000000000000000000000000000000aaaa0002_96e3b90_04 = 0x00[1m[0m
ERROR exception calling callback for <Future at 0x108dce900 state=finished returned SolverOutput>
Traceback (most recent call last):
File "/Users/karma/.pyenv/versions/3.13.0/lib/python3.13/concurrent/futures/_base.py", line 340, in _invoke_callbacks
callback(self)
~~~~~~~~^^^^^^
File "/Users/karma/projects/halmos/src/halmos/__main__.py", line 953, in _solve_end_to_end_callback
print(color_error(f"Counterexample: {model}"))
~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/Users/karma/projects/halmos/.venv/lib/python3.13/site-packages/rich/file_proxy.py", line 31, in write
buffer = self.__buffer
^^^^^^^^^^^^^
AttributeError: 'cell' object has no attribute '_FileProxy__buffer'
