added some basic verification tests

Author: gustavo-grieco

lib/Echidna/Types/Test.hs

@@ -146,6 +146,11 @@ isPassed t = case t.state of
   Passed -> True
   _      -> False
 
+isVerified :: EchidnaTest -> Bool
+isVerified t = case t.state of
+  Unsolvable -> True
+  _          -> False
+
 instance ToJSON TestState where
   toJSON s =
     object $ ("passed", toJSON passed) : maybeToList desc

src/test/Common.hs

@@ -10,6 +10,7 @@ module Common
   , solnFor
   , solved
   , passed
+  , verified
   , solvedLen
   , solvedWith
   , solvedWithout
@@ -219,6 +220,15 @@ passed n (env, _) = do
     Nothing             -> error ("no test was found with name: " ++ show n)
     _                   -> False
 
+verified :: Text -> (Env, WorkerState) -> IO Bool
+verified n (env, _) = do
+  tests <- traverse readIORef env.testRefs
+  pure $ case getResult n tests of
+    Just t | isVerified t -> True
+    Just t | isOpen t     -> True
+    Nothing               -> error ("no test was found with name: " ++ show n)
+    _                     -> False
+
 solvedLen :: Int -> Text -> (Env, WorkerState) -> IO Bool
 solvedLen i t final = (== Just i) . fmap length <$> solnFor t final
 

src/test/Tests/Symbolic.hs

@@ -1,15 +1,17 @@
 module Tests.Symbolic (symbolicTests) where
 
 import Test.Tasty (TestTree, testGroup)
-import Common (testContract', solved, passed)
+import Common (testContract', solved, verified)
 import Echidna.Types.Campaign (WorkerType(..))
 
 symbolicTests :: TestTree
 symbolicTests = testGroup "Symbolic tests"
-  [ testContract' "symbolic/sym.sol" Nothing Nothing (Just "symbolic/sym.yaml") True SymbolicWorker
-      [ ("echidna_sym passed", passed "echidna_sym") ]
-
-  , testContract' "symbolic/sym-assert.sol" Nothing Nothing (Just "symbolic/sym-assert.yaml") True SymbolicWorker
-      [ ("func_one passed", solved "func_one")
-      , ("func_two passed", solved "func_two") ]
+  [ testContract' "symbolic/verify.sol" Nothing Nothing (Just "symbolic/verify.yaml") True SymbolicWorker
+      [ ("simple passed", solved "simple")
+      , ("array passed", solved "array")
+      , ("negative passed", solved "negative")
+      , ("close passed", solved "close")
+      , ("far not verified", verified "far")
+      , ("correct not verified", verified "correct") 
+    ]
   ]

tests/solidity/symbolic/sym-assert.sol

@@ -0,0 +1,30 @@
+contract VulnerableContract {
+    mapping (uint256 => uint256) a;
+    uint256 private last_number = block.number;
+    function simple(uint256 x) public payable {
+        a[12323] = ((x >> 5) / 7777);
+        if (a[12323] == 2222) {
+            assert(false); // BUG
+        }
+    }
+  function array(uint256[3] calldata xs) public {
+    assert(xs[0] != xs[2] + 1);
+  }
+  
+  function negative(int24 x) public {
+    assert(x != -42);
+  }
+
+  function correct(int24 x) public {
+    assert(int256(x) != type(int256).max);
+  }
+
+  function close(uint256 x) public {
+    assert(block.number != last_number + 123);
+  }
+
+  function far(uint256 x) public {
+    assert(block.number != type(uint256).max);
+  }
+
+}