Skip to content

Commit 25b025a

Browse files
refactor verification code to make sure tests are correctly labeled when the verifiction finishes
1 parent 1d40bd0 commit 25b025a

File tree

1 file changed

+12
-10
lines changed

1 file changed

+12
-10
lines changed

lib/Echidna/Campaign.hs

Lines changed: 12 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -297,24 +297,26 @@ runSymWorker callback vm dict workerId _ name = do
297297
-- We can't do callseq vm' [symTx] because callseq might post the full call sequence as an event
298298
newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm [symTx]) txs
299299
let methodSignature = unpack method.methodSignature
300-
unless newCoverage ( do
300+
unless newCoverage $ do
301301
unless (null txs) $ error "No new coverage but symbolic execution found valid txs. Something is wrong."
302-
updateTests $ \test -> do
303-
if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then
304-
pure $ Just $ test { Test.state = Unsolvable }
305-
else
306-
pure $ Just test
307-
pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction."))
308-
302+
when (null errors && null partials) $ do
303+
updateTests $ \test -> do
304+
if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then
305+
pure $ Just $ test { Test.state = Unsolvable }
306+
else
307+
pure $ Just test
308+
309+
unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) solving constraints produced by method " <> methodSignature <> ": " <> show e)) errors
310+
unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic verification of method " <> methodSignature <> ": " <> unpack e)) partials
309311
when (not (null partials) || not (null errors)) $ do
310-
unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) solving constraints produced by method " <> methodSignature <> ": " <> show e)) errors
311-
unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic verification of method " <> methodSignature <> ": " <> unpack e)) partials
312312
updateTests $ \test -> do
313313
if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then
314314
pure $ Just $ test {Test.state = Passed}
315315
else
316316
pure $ Just test
317317

318+
pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction.")
319+
318320
-- | Run a fuzzing campaign given an initial universe state, some tests, and an
319321
-- optional dictionary to generate calls with. Return the 'Campaign' state once
320322
-- we can't solve or shrink anything.

0 commit comments

Comments
 (0)