ethereum / hevm

symbolic EVM evaluator
https://hevm.dev
GNU Affero General Public License v3.0
223 stars 45 forks source link

Update GHC to 9.6 #471

Closed arcz closed 3 weeks ago

arcz commented 5 months ago

Description

Around 30 symbolic tests fail due to this update but all concrete tests pass. There is a significant runtime performance improvement (over 30% on concrete tests) probably due to better compiler optimizations. I fixed some cosmetic stuff from hlint on the way.

TODO: debug symbolic tests, update nixpkgs branch once merged into master

Checklist

msooseth commented 5 months ago

There seems to be two issues:

Notes:

$ ldd /nix/store/f1x01z8lk7qb6fm3djbd7h1rbxjg3lxm-bitwuzla-0.3.0/bin/bitwuzla
/nix/store/f1x01z8lk7qb6fm3djbd7h1rbxjg3lxm-bitwuzla-0.3.0/bin/bitwuzla: /nix/store/1x4ijm9r1a88qk7zcmbbfza324gx1aac-glibc-2.37-8/lib/libc.so.6: version `GLIBC_2.38' not found (required by /nix/store/wx2ngazi4zyx1gi55kz3p9q8y6497fsk-gmp-with-cxx-6.3.0/lib/libgmp.so.10)
        linux-vdso.so.1 (0x00007ffc6cf39000)
        libbitwuzla.so.0 => /nix/store/f1x01z8lk7qb6fm3djbd7h1rbxjg3lxm-bitwuzla-0.3.0/lib/libbitwuzla.so.0 (0x00007fd2ffa00000)
        libstdc++.so.6 => /nix/store/2fpmbk0g0ggm9zq89af7phvvvv8dnm7n-gcc-12.3.0-lib/lib/libstdc++.so.6 (0x00007fd2ff600000)
        libgcc_s.so.1 => /nix/store/2fpmbk0g0ggm9zq89af7phvvvv8dnm7n-gcc-12.3.0-lib/lib/libgcc_s.so.1 (0x00007fd2ffdec000)
        libc.so.6 => /nix/store/1x4ijm9r1a88qk7zcmbbfza324gx1aac-glibc-2.37-8/lib/libc.so.6 (0x00007fd2ff41a000)
        libbitwuzlabb.so => /nix/store/f1x01z8lk7qb6fm3djbd7h1rbxjg3lxm-bitwuzla-0.3.0/lib/libbitwuzlabb.so (0x00007fd2ffddd000)
        libbitwuzlabv.so => /nix/store/f1x01z8lk7qb6fm3djbd7h1rbxjg3lxm-bitwuzla-0.3.0/lib/libbitwuzlabv.so (0x00007fd2ffdc7000)
        libbitwuzlals.so => /nix/store/f1x01z8lk7qb6fm3djbd7h1rbxjg3lxm-bitwuzla-0.3.0/lib/libbitwuzlals.so (0x00007fd2ff9a9000)
        libgmp.so.10 => /nix/store/wx2ngazi4zyx1gi55kz3p9q8y6497fsk-gmp-with-cxx-6.3.0/lib/libgmp.so.10 (0x00007fd2ff906000)
        libm.so.6 => /nix/store/1x4ijm9r1a88qk7zcmbbfza324gx1aac-glibc-2.37-8/lib/libm.so.6 (0x00007fd2ff33a000)
        /nix/store/1x4ijm9r1a88qk7zcmbbfza324gx1aac-glibc-2.37-8/lib/ld-linux-x86-64.so.2 => /nix/store/ksk3rnb0ljx8gngzk19jlmbjyvac4hw6-glibc-2.38-44/lib64/ld-linux-x86-64.so.2 (0x00007fd2ffe0f000)
msooseth commented 5 months ago

@arcz can you check what's going on with the build system doing this?

2024-03-11T16:52:22.4496150Z hevm> /nix/store/3frbd0spychry5hg7jfajaiga271nwk1-elfutils-0.190/lib/libdw.a(dwfl_end.o):function dwfl_end:(.text+0x7b): error: undefined reference to 'elf_end'

I'll tackle the bitwuzla thing :)

msooseth commented 5 months ago

@arcz We need this patch to make it work with the new forge that this PR also is introducing. To be more precise, this adds a bit of cleanup AND the --ast flag that is strictly necessary. I think the cleanup is sane, though.

Note that this is due to the updated forge that's part of this nix lock update. Also, this will break ALL previous forge users. Not a big deal, but could be annoying to some users. Old forge compains: --ast is not a flag.

commit c1ce457823f67a7b92139b02b65f494c1e42569f (HEAD -> new-forge, origin/new-forge)
Author: Mate Soos <mate.soos@ethereum.org>
Date:   Wed Mar 13 16:03:32 2024 +0100

    Fixing forge, and some minor code simplification

diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
index b1b33da2..45a69a13 100644
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -347,10 +347,10 @@ readSolc pt root fp = do
   -- NOTE: we cannot and must not use Data.Text.IO.readFile because that takes the locale
   --       and may fail with very strange errors when the JSON it's reading
   --       contains any UTF-8 character -- which it will with foundry
-  let fileContents = fmap Data.Text.Encoding.decodeUtf8 (Data.ByteString.readFile fp)
-  (readJSON pt (T.pack $ takeBaseName fp) <$> fileContents) >>=
-    \case
-      Nothing -> pure . Left $ "unable to parse: " <> fp
+  fileContents <- fmap Data.Text.Encoding.decodeUtf8 $ Data.ByteString.readFile fp
+  let contractName = T.pack $ takeBaseName fp
+  case readJSON pt contractName fileContents of
+      Nothing -> pure . Left $ "unable to parse " <> show pt <> " project JSON: " <> fp
       Just (contracts, asts, sources) -> do
         sourceCache <- makeSourceCache root sources asts
         pure (Right (BuildOutput contracts sourceCache))
diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs
index 523f67b1..16688ec6 100644
--- a/test/EVM/Test/Utils.hs
+++ b/test/EVM/Test/Utils.hs
@@ -79,7 +79,7 @@ compile foundryType root src = do
   case foundryType of
     FoundryStdLib -> initStdForgeDir (root <> "/lib/forge-std")
     Foundry -> pure ()
-  r@(res,_,_) <- readProcessWithExitCode "forge" ["build", "--root", root] ""
+  r@(res,_,_) <- readProcessWithExitCode "forge" ["build", "--ast", "--root", root] ""
   case res of
     ExitFailure _ -> pure . Left $ "compilation failed: " <> show r
     ExitSuccess -> readBuildOutput root Foundry
arcz commented 5 months ago

@msooseth I pinned bitwuzla and forge and there was just one test failing. I ignored some yul optimization tests which appear to be stuck if you want to take a look.