diff --git a/CHANGELOG.md b/CHANGELOG.md index 87c7e608d..fb9e67ff3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,11 @@ All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## Fixed +- We now try to simplify expressions fully before trying to cast them to a concrete value + This should improve issues when "Unexpected Symbolic Arguments to Opcode" was + unnecessarily output + ## [0.54.2] - 2024-12-12 ## Fixed diff --git a/test/test.hs b/test/test.hs index e36dccbb9..90ac61b5e 100644 --- a/test/test.hs +++ b/test/test.hs @@ -449,6 +449,14 @@ tests = testGroup "hevm" expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts -- putStrLnM $ T.unpack $ formatExpr expr assertEqualM "Expression is not clean." (badStoresInExpr expr) False + , test "simplify-storage-wordToAddr" $ do + let a = "000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a" + s = ConcreteStore (Map.fromList[(W256 0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,W256 0x5842cf)]) + expr = SLoad (Keccak (ConcreteBuf (hexStringToByteString a))) s + simpExpr = Expr.wordToAddr expr + simpExpr2 = Expr.concKeccakSimpExpr expr + assertEqualM "Expression should simplify to value." simpExpr (Just $ LitAddr 0x5842cf) + assertEqualM "Expression should simplify to value." simpExpr2 (Lit 0x5842cf) ] , testGroup "StorageTests" [ test "read-from-sstore" $ assertEqualM ""