Comments (5)
msooseth
commented on September 15, 2024
1
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 operation
However, 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.
from hevm.
msooseth
commented on September 15, 2024
1
So I am writing a PR to fix at least the starting point of this issue, #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!
from hevm.
msooseth
commented on September 15, 2024
1
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!
from hevm.
msooseth
commented on September 15, 2024
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...
from hevm.
caiosabarros
commented on September 15, 2024
Thanks @msooseth for looking into it!
I'll try to use prove soon and check how it does.
Keep it up the great work!
from hevm.
Related Issues (20)
- Error: unable to parse: .../out/Base.sol/CommonBase.json HOT 6
- Error `TODO: implement copySlice with a symbolically sized region` reached by Echidna HOT 2
- symAbiArg cannot handle tuples HOT 3
- Move trace printing to prettyprinter
- Improve known cheat code errors HOT 2
- Fuzzer bug in `readWord-equivalence` HOT 1
- Infinite loop with nested arrays HOT 1
- Fuzzer Bug in CopySlice Equiv HOT 1
- Failed to run ["cabal","v2-repl","lib:hevm"] in directory "/root/projects/hevm". HOT 1
- Partial Concrete Storage for symbolic execution HOT 2
- Unexpected Symbolic Arguments to Opcode (SymAddr "caller") HOT 4
- Missing User Acceptance Tests
- Confusion about "Latest" BlockNumber when Symbolic executing a contract HOT 3
- Constant propagation is not working HOT 1
- error: `TODO: symbolic abi encoding for bytes` -- needs `AbiBytesDynamicType` Abi encoding in `symAbiArg` HOT 3
- Display `SymAddr "caller"` in `formatCex` function when call `hevm --get-models` HOT 7
- Collision in address is "possible" as per hevm, even though it's not HOT 1
- Investigate possible ways to make our test suite run faster
- Investigate possible nondeterminism in our test suite HOT 4
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from hevm.