Detect when a property/optimization is invalid (#1536)

Author: gustavo-grieco

lib/Echidna/Solidity.hs

@@ -42,7 +42,7 @@ import Echidna.ABI
 import Echidna.Deploy (deployContracts, deployBytecodes)
 import Echidna.Exec (execTx, execTxWithCov, initialVM)
 import Echidna.SourceAnalysis.Slither
-import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isFoundryMode)
+import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isFoundryMode, isOptimizationMode)
 import Echidna.Types.Campaign (CampaignConf(..))
 import Echidna.Types.Config (EConfig(..), Env(..))
 import Echidna.Types.Signature
@@ -322,6 +322,18 @@ mkTests solConf campaignConf mainContract = do
     Just (t, _) -> throwM $ TestArgsFound t
     Nothing -> pure ()
 
+  -- Check that property functions return bool
+  when (isPropertyMode solConf.testMode) $
+    forM_ (Map.elems mainContract.abiMap) $ \method ->
+      when (solConf.prefix `T.isPrefixOf` method.name && map snd method.output /= [AbiBoolType]) $
+        throwM $ PropertyWithoutReturn method.name
+
+  -- Check that optimization functions return int256
+  when (isOptimizationMode solConf.testMode) $
+    forM_ (Map.elems mainContract.abiMap) $ \method ->
+      when (solConf.prefix `T.isPrefixOf` method.name && map snd method.output /= [AbiIntType 256]) $
+        throwM $ OptimizationWithWrongReturn method.name
+
   pure $ createTests solConf.testMode
                      solConf.testDestruction
                      testNames

lib/Echidna/Test.hs

@@ -80,6 +80,10 @@ isFoundryMode :: TestMode -> Bool
 isFoundryMode "foundry" = True
 isFoundryMode _          = False
 
+isOptimizationMode :: TestMode -> Bool
+isOptimizationMode "optimization" = True
+isOptimizationMode _               = False
+
 createTests
   :: TestMode
   -> Bool

lib/Echidna/Types/Solidity.hs

@@ -23,11 +23,13 @@ data SolException
   | SolcReadFailure
   | NoContracts
   | TestArgsFound Text
+  | PropertyWithoutReturn Text
+  | OptimizationWithWrongReturn Text
   | ContractNotFound Text
   | NoBytecode Text
   | NoFuncs
   | NoTests
-  | OnlyTests
+
   | ConstructorArgs String
   | DeploymentFailed Addr Text
   | SetUpCallFailed Text
@@ -43,10 +45,12 @@ instance Show SolException where
     NoContracts            -> "No contracts found in given file"
     ContractNotFound c     -> "Given contract " ++ show c ++ " not found in given file"
     TestArgsFound t        -> "Test " ++ show t ++ " has arguments, aborting"
+    PropertyWithoutReturn t -> "Property " ++ show t ++ " does not return bool. Property functions must have signature: function " ++ unpack t ++ "() public returns (bool)"
+    OptimizationWithWrongReturn t -> "Optimization " ++ show t ++ " does not return int256. Optimization functions must have signature: function " ++ unpack t ++ "() public returns (int256)"
     NoBytecode t           -> "No bytecode found for contract " ++ show t
     NoFuncs                -> "ABI is empty, are you sure your constructor is right?"
     NoTests                -> "No tests found in ABI. If you are using assert(), use --test-mode assertion"
-    OnlyTests              -> "Only tests and no public functions found in ABI"
+
     ConstructorArgs s      -> "Constructor arguments are required: " ++ s
     NoCryticCompile        -> "crytic-compile not installed or not found in PATH. To install it, run:\n   pip install crytic-compile"
     InvalidMethodFilters f -> "Applying the filter " ++ show f ++ " to the methods produces an empty list. Are you filtering the correct functions using `filterFunctions` or fuzzing the correct contract?"

src/test/Common.hs

@@ -4,6 +4,7 @@ module Common
   , testContract
   , testContractV
   , solcV
+  , withSolcVersion
   , testContract'
   , testContractNamed
   , checkConstructorConditions

src/test/Tests/Compile.hs

@@ -2,27 +2,26 @@ module Tests.Compile (compilationTests) where
 
 import Control.Monad (void)
 import Control.Monad.Catch (catch)
+import Data.SemVer qualified
 import Data.Text (Text)
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.HUnit (testCase, assertBool)
 
-import Common (testConfig, loadSolTests)
+import Common (testConfig, solcV, withSolcVersion, loadSolTests)
 import Echidna.Solidity (compileContracts)
 import Echidna.Types.Config (EConfig(..))
-import Echidna.Types.Solidity (SolException(..))
+import Echidna.Types.Solidity (SolConf(..), SolException(..))
 
 compilationTests :: TestTree
 compilationTests = testGroup "Compilation and loading tests"
   [ loadFails "bad/nocontract.sol" (Just "c") "failed to warn on contract not found" $
       \case ContractNotFound _ -> True; _ -> False
-  , loadFails "bad/nobytecode.sol" Nothing    "failed to warn on abstract contract" $
+  , loadFailsV (>= solcV (0,6,0)) "bad/nobytecode.sol" Nothing "failed to warn on abstract contract" $
       \case NoBytecode _ -> True; _ -> False
   , loadFails "bad/nofuncs.sol"    Nothing    "failed to warn on no functions found" $
       \case NoFuncs -> True; _ -> False
   , loadFails "bad/notests.sol"    Nothing    "failed to warn on no tests found" $
       \case NoTests -> True; _ -> False
-  , loadFails "bad/onlytests.sol"  Nothing    "failed to warn on no non-tests found" $
-      \case OnlyTests -> True; _ -> False
   , loadFails "bad/testargs.sol"   Nothing    "failed to warn on test args found" $
       \case TestArgsFound _ -> True; _ -> False
   , loadFails "bad/consargs.sol"   Nothing    "failed to warn on cons args found" $
@@ -33,11 +32,26 @@ compilationTests = testGroup "Compilation and loading tests"
       \case DeploymentFailed _ _ -> True; _ -> False
   , loadFails "basic/eip-170.sol"  Nothing    "failed to warn on a failed deployment" $
       \case DeploymentFailed _ _ -> True; _ -> False
+  , loadFailsWith "bad/propaliased.sol" Nothing "property" "failed to warn on property without bool return" $
+      \case PropertyWithoutReturn _ -> True; _ -> False
+  , loadFailsWith "bad/optaliased.sol" Nothing "optimization" "failed to warn on optimization with wrong return" $
+      \case OptimizationWithWrongReturn _ -> True; _ -> False
   ]
 
 loadFails :: FilePath -> Maybe Text -> String -> (SolException -> Bool) -> TestTree
-loadFails fp c e p = testCase fp . catch tryLoad $ assertBool e . p where
+loadFails fp c = loadFailsWith fp c "property"
+
+loadFailsV :: (Data.SemVer.Version -> Bool) -> FilePath -> Maybe Text -> String -> (SolException -> Bool) -> TestTree
+loadFailsV v fp c e p = testCase fp $ withSolcVersion (Just v) $
+  catch tryLoad (assertBool e . p) where
   tryLoad = do
     let cfg = testConfig
     buildOutput <- compileContracts cfg.solConf (pure fp)
     void $ loadSolTests cfg buildOutput c
+
+loadFailsWith :: FilePath -> Maybe Text -> String -> String -> (SolException -> Bool) -> TestTree
+loadFailsWith fp c mode e p = testCase fp . catch tryLoad $ assertBool e . p where
+  tryLoad = do
+    let cfg = testConfig { solConf = testConfig.solConf { testMode = mode } }
+    buildOutput <- compileContracts cfg.solConf (pure fp)
+    void $ loadSolTests cfg buildOutput c

tests/solidity/bad/nobytecode.sol

@@ -1,4 +1,4 @@
-contract Abstract {
-  function nothere() pure public {}
-  function echidna_nothere() pure public {}
+abstract contract Abstract {
+  function nothere() public virtual;
+  function echidna_nothere() public virtual returns (bool);
 }

tests/solidity/bad/onlytests.sol

@@ -0,0 +1,6 @@
+contract Test {
+    function foo() public view {}
+    function echidna_opt_test() public view returns (bool) {
+        return true;
+    }
+}

tests/solidity/bad/optaliased.sol

@@ -0,0 +1,4 @@
+contract Test {
+    function foo() public view {}
+    function echidna_test() public view {}
+}