Merge branch 'main' into decompilation

flake.nix

@@ -15,11 +15,11 @@
       let
         pkgs = nixpkgs.legacyPackages.${system};
         gitignore = pkgs.nix-gitignore.gitignoreSourcePure [ ./.gitignore ];
-	myHaskellPackages = pkgs.haskellPackages.override {
+    myHaskellPackages = pkgs.haskellPackages.override {
           overrides = self: super: rec {
-	    hevm = hevmUpstream.packages.${system}.noTests;
+        hevm = hevmUpstream.packages.${system}.noTests;
           };
-	};
+    };
         act = (myHaskellPackages.callCabal2nixWithOptions "act" (gitignore ./src) "-fci" {})
           .overrideAttrs (attrs : {
             buildInputs = attrs.buildInputs ++ [ pkgs.z3 pkgs.cvc5 ];
@@ -52,7 +52,7 @@
           withHoogle = true;
           shellHook = ''
             export PATH=$(pwd)/bin:$PATH
-	    export DYLD_LIBRARY_PATH="${libraryPath}"
+            export DYLD_LIBRARY_PATH="${libraryPath}"
           '';
         };
       }

src/CLI.hs

@@ -238,10 +238,10 @@ hevm actspec cid sol' code' initcode' solver' timeout debug' = do
 
 bytecodes :: Text -> Text -> IO (BS.ByteString, BS.ByteString)
 bytecodes cid src = do
-  (json, path) <- solidity' src
+  json <- solc Solidity src
   let (Contracts sol', _, _) = fromJust $ readStdJSON json
-  pure $ ((fromJust . Map.lookup (path <> ":" <> cid) $ sol').creationCode,
-          (fromJust . Map.lookup (path <> ":" <> cid) $ sol').runtimeCode)
+  pure $ ((fromJust . Map.lookup ("hevm.sol" <> ":" <> cid) $ sol').creationCode,
+          (fromJust . Map.lookup ("hevm.sol" <> ":" <> cid) $ sol').runtimeCode)
 
 
 

src/Coq.hs

@@ -77,7 +77,7 @@ reachable constructor behvs = inductive
 
 -- | non-recursive constructor for the reachable relation
 baseCase :: Constructor -> T.Text
-baseCase (Constructor name i@(Interface _ decls) conds _ _ _ _) =
+baseCase (Constructor name i@(Interface _ decls) conds _ _ _ ) =
   T.pack name <> baseSuffix <> " : " <> universal <> "\n" <> constructorBody
   where
     baseval = parens $ T.pack name <> " " <> envVar <> " " <> arguments i
@@ -113,15 +113,15 @@ reachableStep (Behaviour name _ i conds cases _ _ _) =
 
 -- | definition of a base state
 base :: Store -> Constructor -> T.Text
-base store (Constructor name i _ _ _ updates _) =
+base store (Constructor name i _ _ _ updates) =
   definition (T.pack name) (envDecl <> " " <> interface i) $
     stateval store name (\_ t -> defaultSlotValue t) updates
 
 transition :: Store -> Behaviour -> Fresh T.Text
 transition store (Behaviour name cname i _ _ _ rewrites _) = do
   name' <- fresh name
   return $ definition name' (envDecl <> " " <> stateDecl <> " " <> interface i) $
-    stateval store cname (\ref _ -> storageRef ref) (updatesFromRewrites rewrites)
+    stateval store cname (\ref _ -> storageRef ref) rewrites
 
 -- | inductive definition of a return claim
 -- ignores claims that do not specify a return value

src/Decompile.hs

@@ -157,7 +157,6 @@ mkConstructor cs
             , _cpostconditions = mempty
             , _invariants = mempty
             , _initialStorage = updates
-            , _cstateUpdates = mempty -- TODO
             }
         _ -> error "Internal Error: mkConstructor called on a non Success branch"
   | otherwise = Left "TODO: decompile constructors with multiple branches"
@@ -195,7 +194,7 @@ mkBehvs c = concatMapM (\(i, bs) -> mapM (mkbehv i) (Set.toList bs)) (Map.toList
         , _preconditions = nub pres
         , _caseconditions = mempty -- TODO: what to do here?
         , _postconditions = mempty
-        , _stateUpdates = fmap Rewrite rewrites
+        , _stateUpdates = rewrites
         , _returns = ret
         }
     mkbehv _ _ = error "Internal Error: mkbehv called on a non Success branch"

src/Enrich.hs

@@ -18,36 +18,36 @@ enrich (Act store contracts) = Act store (enrichContract <$> contracts)
 
 -- |Adds type bounds for calldata , environment vars, and external storage vars as preconditions
 enrichConstructor :: Constructor -> Constructor
-enrichConstructor ctor@(Constructor _ (Interface _ decls) pre _ invs _ storageUpdates) =
+enrichConstructor ctor@(Constructor _ (Interface _ decls) pre _ invs _) =
   ctor { _cpreconditions = pre'
        , _invariants = invs' }
     where
       pre' = pre
              <> mkCallDataBounds decls
-             <> mkStorageBounds storageUpdates
              <> mkEthEnvBounds (ethEnvFromConstructor ctor)
       invs' = enrichInvariant ctor <$> invs
 
 -- | Adds type bounds for calldata, environment vars, and storage vars as preconditions
 enrichBehaviour :: Behaviour -> Behaviour
-enrichBehaviour behv@(Behaviour _ _ (Interface _ decls) pre _ _ stateUpdates _) =
+enrichBehaviour behv@(Behaviour _ _ (Interface _ decls) pre cases _ stateUpdates _) =
   behv { _preconditions = pre' }
     where
       pre' = pre
              <> mkCallDataBounds decls
              <> mkStorageBounds stateUpdates
+             <> mkStorageBoundsLoc (concatMap locsFromExp (pre <> cases))
              <> mkEthEnvBounds (ethEnvFromBehaviour behv)
 
 -- | Adds type bounds for calldata, environment vars, and storage vars
 enrichInvariant :: Constructor -> Invariant -> Invariant
-enrichInvariant (Constructor _ (Interface _ decls) _ _ _ _ _) inv@(Invariant _ preconds storagebounds (predicate,_)) =
+enrichInvariant (Constructor _ (Interface _ decls) _ _ _ _) inv@(Invariant _ preconds storagebounds (predicate,_)) =
   inv { _ipreconditions = preconds', _istoragebounds = storagebounds' }
     where
       preconds' = preconds
                   <> mkCallDataBounds decls
                   <> mkEthEnvBounds (ethEnvFromExp predicate)
       storagebounds' = storagebounds
-                       <> mkStorageBounds (Constant <$> locsFromExp predicate)
+                       <> mkStorageBoundsLoc (locsFromExp predicate)
 
 mkEthEnvBounds :: [EthEnv] -> [Exp ABoolean]
 mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars
@@ -74,17 +74,24 @@ mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars
       Nonce -> AbiUIntType 256
 
 -- | extracts bounds from the AbiTypes of Integer values in storage
-mkStorageBounds :: [Rewrite] -> [Exp ABoolean]
-mkStorageBounds refs = catMaybes $ mkBound <$> refs
+mkStorageBounds :: [StorageUpdate] -> [Exp ABoolean]
+mkStorageBounds refs = concatMap mkBound refs
   where
-    mkBound :: Rewrite -> Maybe (Exp ABoolean)
-    mkBound (Constant (Loc SInteger item)) = Just $ fromItem item
-    mkBound (Rewrite (Update SInteger item _)) = Just $ fromItem item
-    mkBound _ = Nothing
+    mkBound :: StorageUpdate -> [Exp ABoolean]
+    mkBound (Update SInteger item _) = [fromItem item]
+    mkBound _ = []
 
-    fromItem :: TStorageItem AInteger -> Exp ABoolean
-    fromItem item@(Item _ (PrimitiveType vt) _) = bound vt (TEntry nowhere Pre item)
-    fromItem (Item _ (ContractType _) _) = LitBool nowhere True
+-- TODO why only Pre items here?
+fromItem :: TStorageItem AInteger -> Exp ABoolean
+fromItem item@(Item _ (PrimitiveType vt) _) = bound vt (TEntry nowhere Pre item)
+fromItem (Item _ (ContractType _) _) = LitBool nowhere True
+
+mkStorageBoundsLoc :: [StorageLocation] -> [Exp ABoolean]
+mkStorageBoundsLoc refs = concatMap mkBound refs
+  where
+    mkBound :: StorageLocation -> [Exp ABoolean]
+    mkBound (Loc SInteger item) = [fromItem item]
+    mkBound _ = []
 
 mkCallDataBounds :: [Decl] -> [Exp ABoolean]
 mkCallDataBounds = concatMap $ \(Decl typ name) -> case fromAbiType typ of

src/HEVM.hs

@@ -122,7 +122,7 @@ translateActConstr (Act store [Contract ctor _]) bytecode = translateConstructor
 translateActConstr (Act _ _) _ = error "TODO multiple contracts"
 
 translateConstructor :: Layout -> Constructor -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata, Sig)
-translateConstructor layout (Constructor cid iface preconds _ _ upds _) bytecode =
+translateConstructor layout (Constructor cid iface preconds _ _ upds) bytecode =
   (cid, [EVM.Success (snd calldata <> (fmap (toProp layout) $ preconds)) mempty (EVM.ConcreteBuf bytecode) (updatesToExpr layout cid upds initmap)],
   calldata, ifaceToSig iface)
   where
@@ -160,10 +160,7 @@ ifaceToSig (Interface name args) = Sig (T.pack name) (fmap fromdecl args)
 
 translateBehv :: Layout -> BS.ByteString -> Behaviour -> EVM.Expr EVM.End
 translateBehv layout bytecode (Behaviour _ cid _ preconds caseconds _ upds ret) =
-  EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (rewritesToExpr layout cid upds bytecode)
-
-rewritesToExpr :: Layout -> Id -> [Rewrite] -> BS.ByteString -> ContractMap
-rewritesToExpr layout cid rewrites bytecode = foldl (flip $ rewriteToExpr layout cid) initmap rewrites
+  EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (updatesToExpr layout cid upds initmap)
   where
     initcontract = EVM.C { EVM.code  = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode)
                          , EVM.storage = EVM.AbstractStore initAddr
@@ -172,10 +169,6 @@ rewritesToExpr layout cid rewrites bytecode = foldl (flip $ rewriteToExpr layout
                          }
     initmap = M.fromList [(initAddr, initcontract)]
 
-rewriteToExpr :: Layout -> Id -> Rewrite -> ContractMap -> ContractMap
-rewriteToExpr _ _ (Constant _) cmap = cmap
-rewriteToExpr layout cid (Rewrite upd) cmap = updateToExpr layout cid upd cmap
-
 updatesToExpr :: Layout -> Id -> [StorageUpdate] -> ContractMap -> ContractMap
 updatesToExpr layout cid upds initmap = foldl (flip $ updateToExpr layout cid) initmap upds