Skip to content

Commit 10ba0f6

Browse files
committed
Fix suitableForSymExec precedence inversion
`not $ null m.inputs && ...` parsed as `not (null m.inputs && ...)`, negating the whole conjunction: the dynamic-argument guard never fired (so bytes/string/dynamic-array methods were handed to the symbolic encoder, which throws). Bind `not` to the emptiness check alone so the filter means what it says: explore methods that have arguments, none dynamic, not opted out.
1 parent 1b444b6 commit 10ba0f6

1 file changed

Lines changed: 6 additions & 1 deletion

File tree

lib/Echidna/SymExec/Common.hs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,12 @@ extractErrors = mapMaybe (\case
8383
_ -> Nothing)
8484

8585
suitableForSymExec :: Method -> Bool
86-
suitableForSymExec m = not $ null m.inputs
86+
suitableForSymExec m =
87+
-- the method must take arguments (otherwise there is nothing to solve for),
88+
-- none of which may be a dynamic ABI type (hevm's symAbiArg cannot encode
89+
-- bytes/string/dynamic arrays symbolically and throws), and it must not opt
90+
-- out via a `_no_symexec` name.
91+
not (null m.inputs)
8792
&& null (filter (\(_, t) -> abiKind t == Dynamic) m.inputs)
8893
&& not (T.isInfixOf "_no_symexec" m.name)
8994

0 commit comments

Comments
 (0)