Fix generation and mutation of extreme signed integers (#791)

* fix generation and mutation of extremete signed integers

* add tests

lib/Echidna.hs

@@ -69,7 +69,7 @@ prepareContract cfg fs c g = do
 
   ads <- addresses
   let ads' = AbiAddress <$> v ^. env . EVM.contracts . to keys
-  let constants' = enhanceConstants si ++ timeConstants ++ largeConstants ++ NE.toList ads ++ ads'
+  let constants' = enhanceConstants si ++ timeConstants ++ extremeConstants ++ NE.toList ads ++ ads'
 
   -- load transactions from init sequence (if any)
   es' <- liftIO $ maybe (return []) loadEtheno it

lib/Echidna/ABI.hs

@@ -185,7 +185,7 @@ fixAbiUInt :: Int -> Word256 -> AbiValue
 fixAbiUInt n x = AbiUInt n (x `mod` ((2 ^ n) - 1))
 
 fixAbiInt :: Int -> Int256 -> AbiValue
-fixAbiInt n x = AbiInt n (x `mod` 2 ^ (n - 1))
+fixAbiInt n x = if x <= -(2 ^ (n - 1)) then AbiInt n (-(2 ^ n)) else AbiInt n (x `mod` (2 ^ (n - 1) - 1))
 
 -- | Given a way to generate random 'Word8's and a 'ByteString' b of length l,
 -- generate between 0 and 2l 'Word8's and add insert them into b at random indices.

lib/Echidna/Solidity.hs

@@ -307,13 +307,16 @@ mkLargeAbiInt i = AbiInt i $ 2 ^ (i - 1) - 1
 mkLargeAbiUInt :: Int -> AbiValue
 mkLargeAbiUInt i = AbiUInt i $ 2 ^ i - 1
 
+mkSmallAbiInt :: Int -> AbiValue
+mkSmallAbiInt i = AbiInt i $ -(2 ^ (i - 1))
+
 timeConstants :: [AbiValue]
 timeConstants = concatMap dec [initialTimestamp, initialBlockNumber]
   where dec i = let l f = f <$> commonTypeSizes <*> fmap fromIntegral [i-1..i+1] in
                 catMaybes (l mkValidAbiInt ++ l mkValidAbiUInt)
 
-largeConstants :: [AbiValue]
-largeConstants = concatMap (\i -> [mkLargeAbiInt i, mkLargeAbiUInt i]) commonTypeSizes
+extremeConstants :: [AbiValue]
+extremeConstants = concatMap (\i -> [mkSmallAbiInt i, mkLargeAbiInt i, mkLargeAbiUInt i]) commonTypeSizes
 
 returnTypes :: [SolcContract] -> Text -> Maybe AbiType
 returnTypes cs t = do

src/test/Tests/Values.hs

@@ -20,6 +20,12 @@ valuesTests = testGroup "Value extraction tests"
       [ ("echidna_found_sender failed",            solved      "echidna_found_sender") ]
     , testContract "values/rconstants.sol"   Nothing
       [ ("echidna_found failed",                   solved      "echidna_found") ]
+    , testContract' "values/extreme.sol"   Nothing Nothing (Just "values/extreme.yaml") False
+      [ ("testMinInt8 passed",                   solved      "testMinInt8"),
+        ("testMinInt16 passed",                  solved      "testMinInt16"),
+        ("testMinInt64 passed",                  solved      "testMinInt32"),
+        ("testMinInt128 passed",                 solved      "testMinInt128")
+      ]
     , testContract' "values/create.sol" (Just "C") Nothing Nothing True
       [ ("echidna_state failed",                   solved      "echidna_state") ]
     , testContract "values/time.sol"         (Just "values/time.yaml")

tests/solidity/values/extreme.sol

@@ -0,0 +1,32 @@
+contract Test {
+  int8 private constant MIN8 = -128;  
+  int16 private constant MIN16 = -32768;
+  int32 private constant MIN32 = -2147483648;
+  int64 private constant MIN64 = -9223372036854775808;
+  int128 private constant MININT128 = -170141183460469231731687303715884105728;
+
+  function testMinInt8(int8 xzgx) public {
+    if (xzgx == MIN8)
+      assert(false);
+  }  
+
+  function testMinInt16(int16 xzgx) public {
+    if (xzgx == MIN16)
+      assert(false);
+  } 
+
+  function testMinInt32(int32 xzgx) public {
+    if (xzgx == MIN32)
+      assert(false);
+  } 
+
+  function testMinInt64(int64 xzgx) public {
+    if (xzgx == MIN64)
+      assert(false);
+  }
+
+  function testMinInt128(int128 xzgx) public {
+    if (xzgx == MININT128)
+      assert(false); 
+  }
+}

tests/solidity/values/extreme.yaml

@@ -0,0 +1,2 @@
+testMode: assertion
+seqLen: 1