flake: use dynamic hevm output

flake.nix

@@ -4,23 +4,23 @@
   inputs = {
     flake-utils.url = "github:numtide/flake-utils";
     nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
-    hevmUpstream = {
-      url = "github:ethereum/hevm";
+    hevm = {
+      url = "github:ethereum/hevm/dynamic-flake-output";
       inputs.nixpkgs.follows = "nixpkgs";
     };
   };
 
-  outputs = { self, nixpkgs, flake-utils, hevmUpstream, ... }:
+  outputs = { nixpkgs, flake-utils, hevm, ... }:
     flake-utils.lib.eachDefaultSystem (system:
       let
         pkgs = nixpkgs.legacyPackages.${system};
         gitignore = pkgs.nix-gitignore.gitignoreSourcePure [ ./.gitignore ];
-        myHaskellPackages = pkgs.haskellPackages.override {
-          overrides = self: super: rec {
-            hevm = hevmUpstream.packages.${system}.noTests;
+        hspkgs = pkgs.haskellPackages.override {
+          overrides = self: super: {
+            hevm = hevm.packages.${system}.unwrapped;
           };
         };
-        act = (myHaskellPackages.callCabal2nixWithOptions "act" (gitignore ./.) "-fci" {})
+        act = (hspkgs.callCabal2nixWithOptions "act" (gitignore ./.) "-fci" {})
           .overrideAttrs (attrs : {
             buildInputs = attrs.buildInputs ++ [ pkgs.z3 pkgs.cvc5 pkgs.solc ];
           });
@@ -31,13 +31,13 @@
         apps.act = flake-utils.lib.mkApp { drv = packages.act; };
         apps.default = apps.act;
 
-        devShell = with pkgs;
-          let libraryPath = "${lib.makeLibraryPath [ libff secp256k1 gmp ]}";
-          in myHaskellPackages.shellFor {
+        devShell = let
+          libraryPath = "${pkgs.lib.makeLibraryPath (with pkgs; [ libff secp256k1 gmp ])}";
+        in hspkgs.shellFor {
           packages = _: [ act ];
-          buildInputs = with pkgs.haskellPackages; [
-            cabal-install
-            haskell-language-server
+          buildInputs = [
+            hspkgs.cabal-install
+            hspkgs.haskell-language-server
             pkgs.jq
             pkgs.z3
             pkgs.cvc5
@@ -54,7 +54,7 @@
             export PATH=$(pwd)/bin:$PATH
             export DYLD_LIBRARY_PATH="${libraryPath}"
           '';
-        };
-      }
+      };
+    }
   );
-}
+}

src/Act/CLI.hs

@@ -221,15 +221,15 @@ coq' f solver' smttimeout' debug' = do
 decompile' :: FilePath -> Text -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
 decompile' solFile' cid solver' timeout debug' = do
   let config = if debug' then debugActConfig else defaultActConfig
-  cores <- liftM fromIntegral getNumProcessors
+  cores <- fmap fromIntegral getNumProcessors
   json <- solc Solidity =<< TIO.readFile solFile'
   let (Contracts contracts, _, _) = fromJust $ readStdJSON json
   case Map.lookup ("hevm.sol:" <> cid) contracts of
     Nothing -> do
       putStrLn "compilation failed"
       exitFailure
     Just c -> do
-      res <- runEnv (Env config) $ Solvers.withSolvers solver' cores (naturalFromInteger <$> timeout) $ \solvers -> decompile c solvers
+      res <- runEnv (Env config) $ Solvers.withSolvers solver' cores 1 (naturalFromInteger <$> timeout) $ \solvers -> decompile c solvers
       case res of
         Left e -> do
           TIO.putStrLn e
@@ -245,7 +245,7 @@ hevm actspec sol' code' initcode' solver' timeout debug' = do
   specContents <- readFile actspec
   proceed specContents (enrich <$> compile specContents) $ \ (Act store contracts) -> do
     cmap <- createContractMap contracts
-    res <- runEnv (Env config) $ Solvers.withSolvers solver' cores (naturalFromInteger <$> timeout) $ \solvers ->
+    res <- runEnv (Env config) $ Solvers.withSolvers solver' cores 1 (naturalFromInteger <$> timeout) $ \solvers ->
       checkContracts solvers store cmap
     case res of
       Success _ -> pure ()

src/Act/HEVM.hs

@@ -44,7 +44,7 @@ import EVM as EVM hiding (bytecode)
 import qualified EVM.Types as EVM hiding (FrameState(..))
 import EVM.Expr hiding (op2, inRange)
 import EVM.SymExec hiding (EquivResult, isPartial)
-import qualified EVM.SymExec as SymExec (EquivResult)
+import qualified EVM.SymExec as SymExec (EquivResult, ProofResult(..))
 import EVM.SMT (SMTCex(..), assertProps)
 import EVM.Solvers
 import EVM.Effects
@@ -66,7 +66,7 @@ type ContractMap = M.Map (EVM.Expr EVM.EAddr) (EVM.Expr EVM.EContract)
 -- when we encounter a constructor call.
 type CodeMap = M.Map Id (Contract, BS.ByteString, BS.ByteString)
 
-type EquivResult = ProofResult () (T.Text, SMTCex) ()
+type EquivResult = ProofResult () (T.Text, SMTCex) T.Text T.Text
 
 initAddr :: EVM.Expr EVM.EAddr
 initAddr = EVM.SymAddr "entrypoint"
@@ -586,7 +586,8 @@ checkEquiv solvers l1 l2 = do
     toEquivRes :: SymExec.EquivResult -> EquivResult
     toEquivRes (Cex cex) = Cex ("\x1b[1mThe following input results in different behaviours\x1b[m", cex)
     toEquivRes (Qed a) = Qed a
-    toEquivRes (Timeout b) = Timeout b
+    toEquivRes (SymExec.Unknown ()) = SymExec.Unknown ""
+    toEquivRes (SymExec.Error b) = SymExec.Error (T.pack b)
 
 
 checkConstructors :: App m => SolverGroup -> ByteString -> ByteString -> Store -> Contract -> CodeMap -> m (Error String (ContractMap, ActEnv))
@@ -757,18 +758,18 @@ assertSelector txdata sig =
 toVRes :: T.Text -> CheckSatResult -> EquivResult
 toVRes msg res = case res of
   Sat cex -> Cex (msg, cex)
-  EVM.Solvers.Unknown -> Timeout ()
+  EVM.Solvers.Unknown e -> SymExec.Unknown (T.pack e)
   Unsat -> Qed ()
-  Error e -> error $ "Internal Error: solver responded with error: " <> show e
+  EVM.Solvers.Error e -> SymExec.Error (T.pack e)
 
 
 checkResult :: App m => Calldata -> Maybe Sig -> [EquivResult] -> m (Error String ())
 checkResult calldata sig res =
   case any isCex res of
     False ->
-      case any isTimeout res of
+      case any isUnknown res || any isError res of
         True -> do
-          showMsg "\x1b[41mNo discrepancies found but timeout(s) occurred. \x1b[m"
+          showMsg "\x1b[41mNo discrepancies found but timeouts or solver errors were encountered. \x1b[m"
           pure $ Failure $ NE.singleton (nowhere, "Failure: Cannot prove equivalence.")
         False -> do
           showMsg "\x1b[42mNo discrepancies found.\x1b[m "

src/Test/Decompile.hs

@@ -109,7 +109,7 @@ checkDecompilation contract src = do
   json <- solc Solidity src
   let (Contracts sol, _, _) = fromJust $ readStdJSON json
   let c = fromJust $ Map.lookup ("hevm.sol:" <> contract) sol
-  runEnv (Env defaultActConfig) (Solvers.withSolvers CVC5 1 (Just 100000000) (decompile c)) >>= \case
+  runEnv (Env defaultActConfig) (Solvers.withSolvers CVC5 1 1 (Just 100000000) (decompile c)) >>= \case
     Left es -> do
       T.putStrLn es
       assertBool "decompilation should succeed" False