Closed ggrieco-tob closed 5 days ago
Example provided by @ggrieco-tob
contract VulnerableContract {
mapping (uint256 => uint256) a;
bool y;
bool z;
struct Pair {
uint256 x;
uint256 y;
}
function func_one(Pair calldata p) public payable {
a[12323] = ((p.x >> 5) / 7777);
if (a[12323] == 2222) {
y = true;
}
if ((p.y >> 5) / 7777 == 2222) {
z = true;
}
}
function echidna_sym() public returns (bool) {
return !(y && z);
}
}
Error:
echidna tests/solidity/symbolic/sym.sol --workers 1 --sym-exec true --format text
[2024-07-31 14:38:39.30] Compiling tests/solidity/symbolic/sym.sol... Done! (0.312785437s)
Analyzing contract: /home/g/Code/echidna/tests/solidity/symbolic/sym.sol:VulnerableContract
[2024-07-31 14:38:39.61] Running slither on tests/solidity/symbolic/sym.sol... Done! (0.466798581s)
[2024-07-31 14:38:40.12] [Worker 0] New coverage: 203 instr, 1 contracts, 1 seqs in corpus
echidna: Internal Error: TODO: symbolic abi encoding for (uint256,uint256) -- CallStack (from HasCallStack):
internalError, called at src/EVM/SymExec.hs:124:8 in hevm-0.53.0-74NSVYQSNIwG52xVGKHxbQ:EVM.SymExec
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1350:19 in hevm-0.53.0-74NSVYQSNIwG52xVGKHxbQ:EVM.Types
internalError, called at src/EVM/SymExec.hs:124:8 in hevm-0.53.0-74NSVYQSNIwG52xVGKHxbQ:EVM.SymExec
Will be fixed by https://github.com/ethereum/hevm/pull/522
Let's merge that PR and close this issue :)
Closed via #522. Will open new Issue about User Acceptance Testing missing and will reference the code above that should be part of UAT.
It seems that hevm used to have some code to encode tuples in
symAbiArg
function but it was commented out, and later, never re-added.