Skip to content

Commit 0510795

Browse files
committed
Test: Fix processing of yul object files in equivalence checking
The code was already trying to handle yul files with named object format, however, the logic was not correct and we ended up trying to compile empty input, which resulted in error. There are several fixes: - `onlyAfter` now returns only lines *after* the matched line. Previously, the matched line was returned as well. - The regex used to check if we have `object` line in the file now no longer contains quotes. Previously, this regex never matched because of this quotes. - We now extract the object name in case of an object format. This is necessary to pass to the `yul` function. Previously, we always passed empty string. However, in case of named objects, the key in json is the object name.
1 parent f741705 commit 0510795

File tree

1 file changed

+20
-15
lines changed

1 file changed

+20
-15
lines changed

test/EVM/Equivalence/EquivalenceTests.hs

Lines changed: 20 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
{-# LANGUAGE QuasiQuotes #-}
2+
{-# OPTIONS_GHC -Wno-x-partial #-}
23

34
module EVM.Equivalence.EquivalenceTests (tests) where
45

@@ -19,7 +20,7 @@ import Test.Tasty
1920
import Test.Tasty.ExpectedFailure (ignoreTest)
2021
import Test.Tasty.HUnit
2122
import Text.RE.TDFA.String hiding (matches)
22-
import Text.RE.Replace (replaceAll)
23+
import Text.RE.Replace (replaceAll, captureText, CaptureOrdinal(..), CaptureID(..))
2324

2425

2526
import EVM.Effects qualified as Effects
@@ -492,12 +493,6 @@ yulOptimizationsSolcTests = testCase "eq-all-yul-optimization-tests" $ do
492493
, "loadResolver/zero_length_reads_eof.yul"
493494
-- Yul subobjects
494495
, "fullSuite/sub_objects.yul"
495-
-- Parser errors
496-
, "commonSubexpressionEliminator/long_literals_as_builtin_args.yul"
497-
, "commonSubexpressionEliminator/object_access.yul"
498-
, "disambiguator/string_as_hex_and_hex_as_string.yul"
499-
, "expressionSplitter/object_access.yul"
500-
, "equivalentFunctionCombiner/constant_representation_datasize.yul"
501496
]
502497

503498
solcRepo <- fromMaybe (internalError "cannot find solidity repo") <$> (lookupEnv "HEVM_SOLIDITY_REPO")
@@ -511,7 +506,7 @@ yulOptimizationsSolcTests = testCase "eq-all-yul-optimization-tests" $ do
511506
forM_ filesFiltered (\f-> do
512507
origcont <- readFile f
513508
let
514-
onlyAfter pattern (a:ax) = if a =~ pattern then (a:ax) else onlyAfter pattern ax
509+
onlyAfter pattern (a:ax) = if a =~ pattern then ax else onlyAfter pattern ax
515510
onlyAfter _ [] = []
516511
replaceOnce pat repl inp = go inp [] where
517512
go (a:ax) b = if a =~ pat then let a2 = replaceAll repl $ a *=~ pat in b ++ a2:ax
@@ -522,15 +517,25 @@ yulOptimizationsSolcTests = testCase "eq-all-yul-optimization-tests" $ do
522517
-- `calldatacopy(0,0,1024)`. (calldata is symbolic, but memory starts empty).
523518
-- This forces the exploration of more branches, and makes the test vectors a
524519
-- little more thorough.
525-
symbolicMem (a:ax) = if a =~ [re|"^ *object"|] then
526-
let a2 = replaceAll "a calldatacopy(0,0,1024)" $ a *=~ [re|code {|]
527-
in (a2:ax)
528-
else replaceOnce [re|^ *{|] "{\ncalldatacopy(0,0,1024)" $ onlyAfter [re|^ *{|] (a:ax)
520+
symbolicMem program@(a:_) = if a =~ [re|^ *object|] then
521+
let replacementTemplate = "$0\n calldatacopy(0,0,1024)"
522+
replaced = replaceAll replacementTemplate $ (unlines program) *=~ [re|code {|]
523+
in lines replaced
524+
else replaceOnce [re|^ *{|] "{\ncalldatacopy(0,0,1024)" program
529525
symbolicMem _ = internalError "Program too short"
530526

531527
unfiltered = lines origcont
532528
filteredASym = symbolicMem [ x | x <- unfiltered, (not $ x =~ [re|^//|]) && (not $ x =~ [re|^$|]) ]
533-
filteredBSym = symbolicMem [ replaceAll "" $ x *=~[re|^//|] | x <- onlyAfter [re|^// step:|] unfiltered, not $ x =~ [re|^$|] ]
529+
filteredBSym = symbolicMem [ cleaned | x <- onlyAfter [re|^// step:|] unfiltered
530+
, let cleaned = replaceAll "" $ x *=~[re|^//|]
531+
, not $ null cleaned
532+
]
533+
contractName = let
534+
match = head filteredASym ?=~ [re|^ *object +"([^"]+)"|]
535+
success = captureText (IsCaptureOrdinal $ CaptureOrdinal 1) match
536+
in T.pack $ case matched match of
537+
False -> ""
538+
True-> success
534539
start <- getCurrentTime
535540
let verbosity :: Int = 0
536541
when (verbosity > 0) $ putStrLn $ "Checking file: " <> f
@@ -542,8 +547,8 @@ yulOptimizationsSolcTests = testCase "eq-all-yul-optimization-tests" $ do
542547
putStrLn "------------- Filtered B + Symb below-----------------"
543548
mapM_ putStrLn filteredBSym
544549
putStrLn "------------- END -----------------"
545-
Right aPrgm <- yul "" $ T.pack $ unlines filteredASym
546-
Right bPrgm <- yul "" $ T.pack $ unlines filteredBSym
550+
Right aPrgm <- yul contractName $ T.pack $ unlines filteredASym
551+
Right bPrgm <- yul contractName $ T.pack $ unlines filteredBSym
547552
eq <- Effects.runApp $ withSolvers Bitwuzla 1 (Just 100) defMemLimit $ \s -> do
548553
calldata <- mkCalldata Nothing []
549554
equivalenceCheck s Nothing aPrgm bPrgm opts calldata False

0 commit comments

Comments
 (0)