merge with main

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/6f87c03094b6c67a678d15e9b6e6bcf49bdb2186";
+    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}"
           '';
-        };
-      }
+      };
+    }
   );
 }

funding.json

@@ -0,0 +1,5 @@
+{
+  "opRetro": {
+    "projectId": "0x2704cd27b8c60b098d4fe8c5c0fbae2f8f5fe9067c687c501a4c6dc6e9887876"
+  }
+}

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/Decompile.hs

@@ -149,7 +149,7 @@ summarize solvers contract = do
 makeIntSafe :: forall m a. App m => SolverGroup -> EVM.Expr a -> m (EVM.Expr a)
 makeIntSafe solvers expr = evalStateT (mapExprM go expr) mempty
   where
-    -- Walks the expression bottom up and checks (using an smt solver) if overflow is possible for any 
+    -- Walks the expression bottom up and checks (using an smt solver) if overflow is possible for any
     -- arithmetic operations it encounters. Results from child nodes are stored and reused as we move up the tree
     go :: forall b. EVM.Expr b -> StateT (Map (EVM.Expr EVM.EWord) EVM.Prop) m (EVM.Expr b)
     go = \case
@@ -225,11 +225,11 @@ mkConstructor cs
 
   where
     addDefaults :: Map (Integer, Integer) (Text, SlotType) -> DistinctStore -> DistinctStore
-    addDefaults layout (DistinctStore storage) = 
+    addDefaults layout (DistinctStore storage) =
       DistinctStore $ Map.foldr (\(name, typ) s -> case Map.lookup name storage of
                                     Just _ -> s
                                     Nothing -> Map.insert name (LitInt nowhere 0, typ) s) storage layout
-    
+
 -- | Build behaviour specs from the summarized bytecode
 mkBehvs :: EVMContract -> Either Text [Behaviour]
 mkBehvs c = concatMapM (\(i, bs) -> mapM (mkbehv i) (Set.toList bs)) (Map.toList c.runtime)
@@ -309,7 +309,7 @@ decomposeStorage layout = go mempty
     checkedInsert :: (Map Text (Exp AInteger, SlotType)) -> (EVM.W256, EVM.Expr EVM.EWord) -> Either Text (Map Text (Exp AInteger, SlotType))
     checkedInsert curr (key, val) =
         case Map.lookup (toInteger key, 0) layout of
-          Just (name, typ) -> 
+          Just (name, typ) ->
             case Map.lookup name curr of
               -- if a key was already written to higher in the write chain, ignore this write
               Just _ -> pure curr
@@ -328,6 +328,9 @@ simplify e = if (mapTerm go e == e)
     go (Neg _ (Neg _ p)) = p
     go (Eq _ SInteger (ITE _ a (LitInt _ 1) (LitInt _ 0)) (LitInt _ 1)) = go a
     go (Eq _ SInteger (ITE _ a (LitInt _ 1) (LitInt _ 0)) (LitInt _ 0)) = go (Neg nowhere (go a))
+    go (Eq _ SInteger (LitInt _ 1) (ITE _ a (LitInt _ 1) (LitInt _ 0))) = go a
+    go (Eq _ SInteger (LitInt _ 0) (ITE _ a (LitInt _ 1) (LitInt _ 0))) = go (Neg nowhere (go a))
+    -- TODO perhaps normalize before simplification to make rewrites less verbose and more robust
 
     -- this is the condition we get for a non overflowing uint multiplication
     --    ~ ((x != 0) & ~ (in_range 256 x))