SOfter errors

src/EVM/SymExec.hs

@@ -484,18 +484,22 @@ allPanicCodes = [0x00, 0x01, 0x11, 0x12, 0x21, 0x22, 0x31, 0x32, 0x41, 0x51]
 panicMsg :: Word256 -> ByteString
 panicMsg err = selector "Panic(uint256)" <> encodeAbiValue (AbiUInt 256 err)
 
+getRight :: Err b -> b
+getRight (Right y) = y
+getRight (Left err)  = internalError err
+
 -- | Builds a buffer representing calldata from the provided method description
 -- and concrete arguments
-mkCalldata :: Maybe Sig -> [String] -> Err (Expr Buf, [Prop])
+mkCalldata :: Maybe Sig -> [String] -> (Expr Buf, [Prop])
 mkCalldata Nothing _ =
-  pure ( AbstractBuf "txdata"
+  ( AbstractBuf "txdata"
   -- assert that the length of the calldata is never more than 2^64
   -- this is way larger than would ever be allowed by the gas limit
   -- and avoids spurious counterexamples during abi decoding
   -- TODO: can we encode calldata as an array with a smaller length?
   , [Expr.bufLength (AbstractBuf "txdata") .< (Lit (2 ^ (64 :: Integer)))]
   )
-mkCalldata (Just (Sig name types)) args = symCalldata name types args (AbstractBuf "txdata")
+mkCalldata (Just (Sig name types)) args = getRight $ symCalldata name types args (AbstractBuf "txdata")
 
 verifyContract
   :: App m

src/EVM/UnitTest.hs

@@ -190,13 +190,17 @@ runUnitTestContract
           forM testSigs $ \s -> symRun opts vm1 s
         _ -> internalError "setUp() did not end with a result"
 
+getRight :: Err b -> b
+getRight (Right y) = y
+getRight (Left err)  = internalError err
+
 -- Define the thread spawner for symbolic tests
 -- Returns tuple of (No Cex, No warnings)
 symRun :: App m => UnitTestOptions RealWorld -> VM Concrete RealWorld -> Sig -> m (Bool, Bool)
 symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     let callSig = testName <> "(" <> (Text.intercalate "," (map abiTypeSolidity types)) <> ")"
     liftIO $ putStrLn $ "\x1b[96m[RUNNING]\x1b[0m " <> Text.unpack callSig
-    let cd = symCalldata callSig types [] (AbstractBuf "txdata")
+    let cd = getRight $ symCalldata callSig types [] (AbstractBuf "txdata")
         shouldFail = "proveFail" `isPrefixOf` callSig
 
     -- define postcondition depending on `shouldFail`