Open caiosabarros opened 3 months ago
msooseth
commented
2 weeks ago Hmmm so this reproduces with latest. No idea how/why this is happening. Apparently the contract doesn't get pulled into the cache via RPC. Even when I try to force it to be pulled in. I'm looking at it...
msooseth
commented
2 weeks ago So this solves some of the issues:
diff --git a/src/EVM.hs b/src/EVM.hs
index 51d3be79..dc5bc7df 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -9,6 +9,7 @@ import Optics.State
import Optics.State.Operators
import Optics.Zoom
import Optics.Operators.Unsafe
+-- import Debug.Trace (trace)
import EVM.ABI
import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord,
@@ -1270,19 +1271,20 @@ choose = assign #result . Just . HandleEffect . Choose
-- | Construct RPC Query and halt execution until resolved
fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
-fetchAccount addr continue =
- use (#env % #contracts % at addr) >>= \case
- Just c -> continue c
- Nothing -> case addr of
+fetchAccount addr continue = case addr of
SymAddr _ -> do
pc <- use (#state % #pc)
partial $ UnexpectedSymbolicArg pc "trying to access a symbolic address that isn't already present in storage" (wrap [addr])
LitAddr a -> do
+ -- use (#env % #contracts % at addr) >>= \case
+ -- Just c -> trace ("just C here with c: " <> show c) $ continue c
+ -- _ -> case addr of
+ -- LitAddr a -> do
use (#cache % #fetched % at a) >>= \case
- Just c -> do
+ Just c -> do --trace ("found contract addr" <> show addr) $ do
assign (#env % #contracts % at addr) (Just c)
continue c
- Nothing -> do
+ Nothing -> do --trace ("Nothing contract addr" <> show addr) $ do
base <- use (#config % #baseState)
assign (#result) . Just . HandleEffect . Query $
PleaseFetchContract a base
@@ -1315,13 +1317,14 @@ accessStorage addr slot continue = do
fetchAccount addr $ \_ ->
accessStorage addr slot continue
where
- rpcCall c slotConc = if c.external
+ rpcCall c slotConc = fetchAccount addr $ \_ ->
+ if c.external
then forceConcreteAddr addr "cannot read storage from symbolic addresses via rpc" $ \addr' ->
forceConcrete slotConc "cannot read symbolic slots via RPC" $ \slot' -> do
-- check if the slot is cached
contract <- preuse (#cache % #fetched % ix addr')
case contract of
- Nothing -> internalError "contract marked external not found in cache"
+ Nothing -> internalError $ "contract addr " <> show addr' <> " marked external not found in cache"
Just fetched -> case readStorage (Lit slot') fetched.storage of
Nothing -> mkQuery addr' slot'
Just val -> continue valBut you still will get a bunch of issues:
WARNING: hevm was only able to partially explore the call prefix 0xunknown due to the following issue(s):
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
36
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
36
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
36
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "trying to access a symbolic address that isn't already present in storage"
program counter: 6500
arguments:
(SymAddr "caller")
- Unexpected Symbolic Arguments to Opcode
msg: "trying to access a symbolic address that isn't already present in storage"
program counter: 6500
arguments:
(SymAddr "caller")
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 3248
arguments:
(And
1461501637330902918203684832716283019655932542975
(ReadWord
idx:
4
buf:
(AbstractBuf "txdata")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 3248
arguments:
(And
1461501637330902918203684832716283019655932542975
(ReadWord
idx:
4
buf:
(AbstractBuf "txdata")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
36
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
36
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
36
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "trying to access a symbolic address that isn't already present in storage"
program counter: 6500
arguments:
(SymAddr "caller")
- Unexpected Symbolic Arguments to Opcode
msg: "trying to access a symbolic address that isn't already present in storage"
program counter: 6500
arguments:
(SymAddr "caller")
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
36
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
36
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
36
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "EXTCODESIZE"
program counter: 6500
arguments:
(ReadWord
idx:
4
buf:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(CopySlice
srcOffset: 0
dstOffset: 0
size: (BufLength
(AbstractBuf "txdata")
)
src:
(AbstractBuf "txdata")
dst:
(ConcreteBuf
Length: 96 (0x60) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0040: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0050: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 80 ................
)
)
dst:
(ConcreteBuf "")
)
)
- Unexpected Symbolic Arguments to Opcode
msg: "trying to access a symbolic address that isn't already present in storage"
program counter: 6500
arguments:
(SymAddr "caller")
- Unexpected Symbolic Arguments to Opcode
msg: "trying to access a symbolic address that isn't already present in storage"
program counter: 6500
arguments:
(SymAddr "caller")
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
CallStack (from HasCallStack):
error, called at src/EVM/Types.hs:1347:19 in hevm-0.53.0-inplace:EVM.Types
internalError, called at src/EVM/SMT.hs:913:23 in hevm-0.53.0-inplace:EVM.SMT
hevm: thread blocked indefinitely in an MVar operationHowever, these issues would take a lot more time to fix. The copySlice with a symbolically sized region is a whole thing on its own that will take a few months. The thread blocked indefinitely in an MVar operation is weird, and may be unrelated or just too many errors. The EXTCODESIZE may be fixable with the copySlice fix, or may need a hack/another fix.
msooseth
commented
2 weeks ago So I am writing a PR to fix at least the starting point of this issue, https://github.com/ethereum/hevm/pull/515 However, it'll take quite a bit to actually, fully, fix this -- and even then, it'll likely not terminate running. I'd suggest taking the code of the contract, putting in a forge project, and writing test cases for it by hand, with prove_ in front, see: https://hevm.dev/ds-test-tutorial.html That, in my opinion, will do much better!
msooseth
commented
2 weeks ago OK, so that PR seems to fix the issue. However, it will still not work the way you'd like to :) But we'd be getting closer!
caiosabarros
commented
2 weeks ago Thanks @msooseth for looking into it!
I'll try to use prove soon and check how it does.
Keep it up the great work!
Hi! Thanks for the tool! Just started using it, but having some problems so far. Any guidance is appreciated 👍
Here are the commands I have tried (inside a foundry project): First Command:
Second Command:
Here are the errors I am getting: Error for first command:
Partial Output and Error for second command:
I was triyng to follow this article from the EF.
hevm is latest