Inconsistent decoding of negative values when using solc 0.6.12 #886
Description
When using solc version 0.6.12 (and posibly others solc 0.6.x versions), the decoding of certain abi value is inconsistent can confuse the users. To reproduce:
forge init test
cd test
rm src/* scripts/* test/*
Then create a new contract in src:
// SPDX-License-Identifier: UNLICENSED
contract Bug {
bool public IS_TEST = true;
function prove_negative(int24 x) public {
assert(x != -42);
}
}Finally add the following line in foundry.toml:
solc_version = "0.6.12"Now we can reproduce this bug. Let's first run using bitwuzla (0.8.2), which shows the correct result:
$ forge clean ; forge build --ast ; hevm test --debug --solver bitwuzla
..
Checking 1 function(s) in contract src/Counter.sol:Bug
[RUNNING] prove_negative(int24)
Exploring call prefix 0xa4e36d39
Flattening expression
Exploration finished, 3 branch(es) to check in call prefix 0xa4e36d39
Keccak preimages in state: 0
Checking for reachability of 1 potential property violation(s) in call prefix 0xa4e36d39
SMT result: Cex SMTCex {vars = fromList [(Var "arg1",0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd6)], addrs = fromList [(SymAddr "miner",0x81f777e94fBe791e0d52386E544c24b2d7c9fd01),(SymAddr "origin",0x604c87E034Bb14FDB20370FFd89D7E13f40a5f19)], buffers = fromList [(AbstractBuf "txdata",Comp Base {byte = 0, length = 0x0})], store = fromList [], blockContext = fromList [], txContext = fromList []}
Found 1 potential counterexample(s) in call prefix 0xa4e36d39
-> debug of func: prove_negative Failure at the end of expr: UnrecognizedOpcode 254
-> debug of func: prove_negative Failure at the end of expr: Revert (ConcreteBuf "")
symRun -- (cex,warnings,unexpectedAllRevert): (True,False,False)
Repro running function: LitAddr 0x000000000000000000000000000000000000ACAb with caller: LitAddr 0x00000000000000000000000000000000DeaDBeef, gas: 281474976710655, and calldata: "a4e36d39ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd6"
Cex reproduction runs' results are: [Right True]
[FAIL] prove_negative
Counterexample: [validated]
calldata: prove_negative(-42)
result: Unrecognized opcode: 254
Using z3 (4.15) shows an incorrect value:
forge clean ; forge build --ast ; hevm test --debug --solver z3
...
Checking 1 function(s) in contract src/Counter.sol:Bug
[RUNNING] prove_negative(int24)
Exploring call prefix 0xa4e36d39
Flattening expression
Exploration finished, 3 branch(es) to check in call prefix 0xa4e36d39
Keccak preimages in state: 0
Checking for reachability of 1 potential property violation(s) in call prefix 0xa4e36d39
SMT result: Cex SMTCex {vars = fromList [(Var "arg1",0xffffd6)], addrs = fromList [(SymAddr "miner",0xfffFfFFFFfFfFFFfffffFFfFdfffFffFfFfFfFf5),(SymAddr "origin",0x200000000000000A)], BUFferS = FRomLiSt [(AbstractBuf "txdata",Comp Base {byte = 0, length = 0x1})], store = fromList [], blockContext = fromList [], txContext = fromList []}
Found 1 potential counterexample(s) in call prefix 0xa4e36d39
-> debug of func: prove_negative Failure at the end of expr: UnrecognizedOpcode 254
-> debug of func: prove_negative Failure at the end of expr: Revert (ConcreteBuf "")
symRun -- (cex,warnings,unexpectedAllRevert): (True,False,False)
Repro running function: LitAddr 0x000000000000000000000000000000000000ACAb with caller: LitAddr 0x00000000000000000000000000000000DeaDBeef, gas: 281474976710655, and calldata: "a4e36d390000000000000000000000000000000000000000000000000000000000ffffd6"
Cex reproduction runs' results are: [Right True]
[FAIL] prove_negative
Counterexample: [validated]
calldata: prove_negative(16777174)
result: Unrecognized opcode: 254
Finally cvc5 (1.2.1):
forge clean ; forge build --ast ; hevm test --debug --solver cvc5
...
Checking 1 function(s) in contract src/Counter.sol:Bug
[RUNNING] prove_negative(int24)
Exploring call prefix 0xa4e36d39
Flattening expression
Exploration finished, 3 branch(es) to check in call prefix 0xa4e36d39
Keccak preimages in state: 0
Checking for reachability of 1 potential property violation(s) in call prefix 0xa4e36d39
SMT result: Cex SMTCex {vars = fromList [(Var "arg1",0xffffd6)], addrs = fromList [(SymAddr "miner",0xa),(SYmADdR "ORIGIN",0Xb)], bUffeRs = FRomLisT [(AbStracTBuf "txdata",Comp Base {byte = 0, length = 0x27})], store = fromList [], blockContext = fromList [], txContext = fromList []}
Found 1 potential counterexample(s) in call prefix 0xa4e36d39
-> debug of func: prove_negative Failure at the end of expr: UnrecognizedOpcode 254
-> debug of func: prove_negative Failure at the end of expr: Revert (ConcreteBuf "")
symRun -- (cex,warnings,unexpectedAllRevert): (True,False,False)
Repro running function: LitAddr 0x000000000000000000000000000000000000ACAb with caller: LitAddr 0x00000000000000000000000000000000DeaDBeef, gas: 281474976710655, and calldata: "a4e36d390000000000000000000000000000000000000000000000000000000000ffffd6000000"
Cex reproduction runs' results are: [Right True]
[FAIL] prove_negative
Counterexample: [validated]
calldata: prove_negative(0000000000000000000000000000000000000000000000000000000000ffffd6000000)
result: Unrecognized opcode: 254
While in all the cases, the CEX is correctly validated (it is using the calldata for that), the decoding is not the same. In the case of Echidna, it will fail to run correctly for z3 and cvc5, since the values are decoded and then re-encoded.