Getting Internal Error For Different Commands When Trying To Execute Symbolic On Live Contracts
#490
Assignees
Labels
bug
Something isn't working
Comments
|
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... |
|
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: However, these issues would take a lot more time to fix. The |
|
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 |
|
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! |
|
Thanks @msooseth for looking into it! I'll try to use Keep it up the great work! |
4 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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
~$ hevm version 0.53.0 [no git revision present]The text was updated successfully, but these errors were encountered: