Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Getting Internal Error For Different Commands When Trying To Execute Symbolic On Live Contracts #490

Open
caiosabarros opened this issue Apr 25, 2024 · 5 comments
Assignees
Labels
bug Something isn't working

Comments

@caiosabarros
Copy link

caiosabarros commented Apr 25, 2024

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:

$ hevm symbolic --rpc $ETH_RPC_URL --address 0x2A8e1E676Ec238d8A992307B495b45B3fEAa5e86 --assertions '[0x01, 0x11]'

Second Command:

$ hevm symbolic --rpc $ETH_RPC_URL --code $(seth code 0x2A8e1E676Ec238d8A992307B495b45B3fEAa5e86) --assertions '[0x01, 0x11]'

Here are the errors I am getting:
Error for first command:

Exploring contract
hevm: Internal Error: contract marked external not found in cache -- CallStack (from HasCallStack):
  internalError, called at src/EVM.hs:1316:26 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM
CallStack (from HasCallStack):
  error, called at src/EVM/Types.hs:1344:19 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.Types
  internalError, called at src/EVM.hs:1316:26 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM

Partial Output and Error for second command:

Exploring contract
Simplifying expression
Explored contract (37 branches)

WARNING: hevm was only able to partially explore the given contract due to the following issues:

  - Unexpected Symbolic Arguments to Opcode
    msg: "Unable to determine a call target"
    program counter: 2535
    arguments:
      (SLoad
        slot:
          24440054405305269366569402256811496959409073762505157381672968839269610695612]
// ...
Checking for reachability of 2 potential property violation(s)
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
  internalError, called at src/EVM/SMT.hs:899:23 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.SMT
CallStack (from HasCallStack):
  error, called at src/EVM/Types.hs:1344:19 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.Types
  internalError, called at src/EVM/SMT.hs:899:23 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.SMT
hevm: thread blocked indefinitely in an MVar operation

I was triyng to follow this article from the EF.

hevm is latest

~$ hevm version
0.53.0 [no git revision present]
@msooseth msooseth self-assigned this Jul 29, 2024
@msooseth
Copy link
Collaborator

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
Copy link
Collaborator

msooseth commented Jul 29, 2024

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 val

But 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.

@msooseth msooseth mentioned this issue Jul 30, 2024
4 tasks
@msooseth msooseth added the bug Something isn't working label Jul 30, 2024
@msooseth
Copy link
Collaborator

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!

@msooseth
Copy link
Collaborator

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
Copy link
Author

Thanks @msooseth for looking into it!

I'll try to use prove soon and check how it does.

Keep it up the great work!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants