Skip to content

Commit

Permalink
add binding for debugging
Browse files Browse the repository at this point in the history
  • Loading branch information
zoep committed Dec 7, 2023
1 parent ec64d3a commit 41057e9
Showing 1 changed file with 34 additions and 2 deletions.
36 changes: 34 additions & 2 deletions src/Act/CLI.hs
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,12 @@ import qualified Data.Text.IO as TIO
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
import GHC.Natural
import Options.Generic

import Control.Monad.State

import qualified Data.ByteString.Lazy.Char8 as B
import qualified Data.ByteString as BS
import Data.ByteString (ByteString)

import Control.Monad
import Control.Lens.Getter

import Act.Error
Expand Down Expand Up @@ -214,6 +213,39 @@ hevm_test cdata contracts = do
endstates <- runEnv (Env debugActConfig) $ Solvers.withSolvers CVC5 1 (Just 1000) $ \solvers -> getRuntimeBranches solvers contracts cdata
putStrLn $ showBehvs endstates

hevm_test' :: FilePath -> FilePath -> Id -> Id -> IO ()
hevm_test' actspec sol' cname behv = do
specContents <- readFile actspec
proceed specContents (enrich <$> compile specContents) $ \ (Act store contracts) -> do
codemap <- createContractMap contracts
runEnv (Env debugActConfig) $ Solvers.withSolvers CVC5 1 (Just 1000) $ \solvers -> do
endstates <- (case Map.lookup cname codemap of
Just (contract@(Contract _ behvs), initcode', bytecode) -> do
(cmap, actenv) <- checkConstructors solvers initcode' bytecode store contract codemap
let (actstorage, hevmstorage) = createStorage cmap
let actbehvs = fst $ flip runState actenv $ translateBehvs actstorage behvs
case find (\(name, _, _, _) -> name == behv) actbehvs of
Just (_,_,calldata, _) -> getRuntimeBranches solvers hevmstorage calldata
Nothing -> error "behaviour not found"
Nothing -> error "contract not found")
liftIO $ putStrLn $ showBehvs endstates


where

createContractMap :: [Contract] -> IO (Map Id (Contract, BS.ByteString, BS.ByteString))
createContractMap contracts = do
foldM (\cmap spec'@(Contract cnstr _) -> do
let cid = _cname cnstr
(initcode'', runtimecode') <- getBytecode cid -- TODO do not reread the file each time
pure $ Map.insert cid (spec', initcode'', runtimecode') cmap
) mempty contracts

getBytecode :: Id -> IO (BS.ByteString, BS.ByteString)
getBytecode cid = do
solContents <- TIO.readFile sol'
bytecodes (Text.pack cid) solContents

hevm :: FilePath -> Maybe FilePath -> Maybe ByteString -> Maybe ByteString -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
hevm actspec sol' code' initcode' solver' timeout debug' = do
specContents <- readFile actspec
Expand Down

0 comments on commit 41057e9

Please sign in to comment.