Merge pull request #126 from ethereum/errorlogger

Improved error handling

.github/workflows/build.yml

@@ -18,10 +18,10 @@ jobs:
     runs-on: ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v2
-      - uses: cachix/install-nix-action@07da2520eebede906fbeefa9dd0a2b635323909d # v12
+      - uses: cachix/install-nix-action@ef6c38c42ba153b4be4b764b71c87c1610896378 # v15
         with:
           skip_adding_nixpkgs_channel: false
-      - uses: cachix/cachix-action@6e4751ed42b22f60165d3f266cfa4cce66ae406d # v8
+      - uses: cachix/cachix-action@3db1a09d3a573d7b62801116405ad5aa0f59c904 # v10
         with:
           name: dapp
           skipPush: true

src/Main.hs → src/CLI.hs

@@ -6,8 +6,10 @@
 {-# LANGUAGE FlexibleInstances  #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# Language TypeOperators #-}
+{-# LANGUAGE OverloadedLists #-}
+{-# LANGUAGE ApplicativeDo #-}
 
-module Main where
+module CLI (main, compile) where
 
 import Data.Aeson hiding (Bool, Number)
 import EVM.SymExec (ProofResult(..))
@@ -20,6 +22,7 @@ import Data.List
 import Data.Either (lefts)
 import Data.Maybe
 import Data.Tree
+import Data.Traversable
 import qualified EVM.Solidity as Solidity
 import qualified Data.Text as Text
 import qualified Data.Text.IO as TIO
@@ -30,11 +33,13 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 import qualified Data.ByteString.Lazy.Char8 as B
 
 import Control.Monad
+import Control.Lens.Getter
 
-import ErrM
+import Error
 import Lex (lexer, AlexPosn(..))
 import Options.Generic
 import Parse
+import Syntax
 import Syntax.Annotated
 import Syntax.Untyped
 import Enrich
@@ -112,16 +117,12 @@ lex' f = do
 parse' :: FilePath -> IO ()
 parse' f = do
   contents <- readFile f
-  case parse $ lexer contents of
-    Bad e -> prettyErr contents e
-    Ok x -> print x
+  validation (prettyErrs contents) print (parse $ lexer contents)
 
 type' :: FilePath -> IO ()
 type' f = do
   contents <- readFile f
-  case compile contents of
-    Ok a  -> B.putStrLn $ encode a
-    Bad e -> prettyErr contents e
+  validation (prettyErrs contents) (B.putStrLn . encode) (enrich <$> compile contents)
 
 prove :: FilePath -> Maybe Text -> Maybe Integer -> Bool -> IO ()
 prove file' solver' smttimeout' debug' = do
@@ -133,7 +134,7 @@ prove file' solver' smttimeout' debug' = do
       Just _ -> error "unrecognized solver"
     config = SMT.SMTConfig (parseSolver solver') (fromMaybe 20000 smttimeout') debug'
   contents <- readFile file'
-  proceed contents (compile contents) $ \claims -> do
+  proceed contents (enrich <$> compile contents) $ \claims -> do
     let
       catModels results = [m | Sat m <- results]
       catErrors results = [e | e@SMT.Error {} <- results]
@@ -186,19 +187,19 @@ prove file' solver' smttimeout' debug' = do
 coq' :: FilePath -> IO()
 coq' f = do
   contents <- readFile f
-  proceed contents (compile contents) $ \claims ->
+  proceed contents (enrich <$> compile contents) $ \claims ->
     TIO.putStr $ coq claims
 
 k :: FilePath -> FilePath -> Maybe [(Id, String)] -> Maybe String -> Bool -> Maybe String -> IO ()
 k spec' soljson' gas' storage' extractbin' out' = do
   specContents <- readFile spec'
   solContents  <- readFile soljson'
   let kOpts = KOptions (maybe mempty Map.fromList gas') storage' extractbin'
-      errKSpecs = do refinedSpecs <- compile specContents
-                     (sources, _, _) <- errMessage (nowhere, "Could not read sol.json")
-                       $ Solidity.readJSON $ pack solContents
-                     forM [b | B b <- refinedSpecs]
-                       $ makekSpec sources kOpts
+      errKSpecs = do
+        behvs <- toEither $ behvsFromClaims . enrich <$> compile specContents
+        (sources, _, _) <- validate [(nowhere, "Could not read sol.json")]
+                              (Solidity.readJSON . pack) solContents
+        for behvs (makekSpec sources kOpts) ^. revalidate
   proceed specContents errKSpecs $ \kSpecs -> do
     let printFile (filename, content) = case out' of
           Nothing -> putStrLn (filename <> ".k") >> putStrLn content
@@ -209,10 +210,10 @@ hevm :: FilePath -> FilePath -> Maybe Text -> Maybe Integer -> Bool -> IO ()
 hevm spec' soljson' solver' smttimeout' smtdebug' = do
   specContents <- readFile spec'
   solContents  <- readFile soljson'
-  let preprocess = do refinedSpecs  <- compile specContents
-                      (sources, _, _) <- errMessage (nowhere, "Could not read sol.json")
-                        $ Solidity.readJSON $ pack solContents
-                      return ([b | B b <- refinedSpecs], sources)
+  let preprocess = do behvs <- behvsFromClaims . enrich <$> compile specContents
+                      (sources, _, _) <- validate [(nowhere, "Could not read sol.json")]
+                        (Solidity.readJSON . pack) solContents
+                      pure (behvs, sources)
   proceed specContents preprocess $ \(specs, sources) -> do
     -- TODO: prove constructor too
     passes <- forM specs $ \behv -> do
@@ -261,38 +262,36 @@ runSMTWithTimeOut solver' maybeTimeout debug' sym
        runwithz3 = runSMTWith z3{verbose=debug'} $ (setTimeOut timeout) >> sym
 
 -- | Fail on error, or proceed with continuation
-proceed :: String -> Err a -> (a -> IO ()) -> IO ()
-proceed contents (Bad e) _ = prettyErr contents e
-proceed _ (Ok a) continue = continue a
-
-compile :: String -> Err [Claim]
-compile = pure . fmap annotate . enrich <=< typecheck <=< parse . lexer
-
-prettyErr :: String -> (Pn, String) -> IO ()
-prettyErr _ (pn, msg) | pn == nowhere = do
-  hPutStrLn stderr "Internal error:"
-  hPutStrLn stderr msg
-  exitFailure
-prettyErr contents (pn, msg) | pn == lastPos = do
-  let culprit = last $ lines contents
-      line' = length (lines contents) - 1
-      col  = length culprit
-  hPutStrLn stderr $ show line' <> " | " <> culprit
-  hPutStrLn stderr $ unpack (Text.replicate (col + length (show line' <> " | ") - 1) " " <> "^")
-  hPutStrLn stderr msg
-  exitFailure
-prettyErr contents (AlexPn _ line' col, msg) = do
-  let cxt = safeDrop (line' - 1) (lines contents)
-  hPutStrLn stderr $ show line' <> " | " <> head cxt
-  hPutStrLn stderr $ unpack (Text.replicate (col + length (show line' <> " | ") - 1) " " <> "^")
-  hPutStrLn stderr msg
-  exitFailure
+proceed :: Validate err => String -> err (NonEmpty (Pn, String)) a -> (a -> IO ()) -> IO ()
+proceed contents comp continue = validation (prettyErrs contents) continue (comp ^. revalidate)
+
+compile :: String -> Error String [Claim]
+compile = pure . fmap annotate <==< typecheck <==< parse . lexer
+
+prettyErrs :: Traversable t => String -> t (Pn, String) -> IO ()
+prettyErrs contents errs = mapM_ prettyErr errs >> exitFailure
   where
-    safeDrop :: Int -> [a] -> [a]
-    safeDrop 0 a = a
-    safeDrop _ [] = []
-    safeDrop _ [a] = [a]
-    safeDrop n (_:xs) = safeDrop (n-1) xs
+  prettyErr (pn, msg) | pn == nowhere = do
+    hPutStrLn stderr "Internal error:"
+    hPutStrLn stderr msg
+  prettyErr (pn, msg) | pn == lastPos = do
+    let culprit = last $ lines contents
+        line' = length (lines contents) - 1
+        col  = length culprit
+    hPutStrLn stderr $ show line' <> " | " <> culprit
+    hPutStrLn stderr $ unpack (Text.replicate (col + length (show line' <> " | ") - 1) " " <> "^")
+    hPutStrLn stderr msg
+  prettyErr (AlexPn _ line' col, msg) = do
+    let cxt = safeDrop (line' - 1) (lines contents)
+    hPutStrLn stderr $ msg <> ":"
+    hPutStrLn stderr $ show line' <> " | " <> head cxt
+    hPutStrLn stderr $ unpack (Text.replicate (col + length (show line' <> " | ") - 1) " " <> "^")
+    where
+      safeDrop :: Int -> [a] -> [a]
+      safeDrop 0 a = a
+      safeDrop _ [] = []
+      safeDrop _ [a] = [a]
+      safeDrop n (_:xs) = safeDrop (n-1) xs
 
 -- | prints a Doc, with wider output than the built in `putDoc`
 render :: Doc -> IO ()

src/Coq.hs

@@ -162,9 +162,8 @@ stateval store handler updates = T.unwords $ stateConstructor : fmap (valuefor u
   valuefor updates' (name, t) =
     case find (eqName name) updates' of
       Nothing -> parens $ handler name t
-      Just (IntUpdate  item e) -> lambda (ixsFromItem item) 0 e (idFromItem item)
-      Just (BoolUpdate item e) -> lambda (ixsFromItem item) 0 e (idFromItem item)
-      Just (BytesUpdate _ _) -> error "bytestrings not supported"
+      Just (Update SByteStr _ _) -> error "bytestrings not supported"
+      Just (Update _ item e) -> lambda (ixsFromItem item) 0 e (idFromItem item)
 
 -- | filter by name
 eqName :: Id -> StorageUpdate -> Bool
@@ -173,16 +172,17 @@ eqName n update = n == idFromUpdate update
 -- represent mapping update with anonymous function
 lambda :: [TypedExp] -> Int -> Exp a -> Id -> T.Text
 lambda [] _ e _ = parens $ coqexp e
-lambda (x:xs) n e m = parens $
+lambda (TExp argType arg:xs) n e m = parens $
   "fun " <> name <> " =>"
-  <> " if " <> name <> eqsym x <> typedexp x
+  <> " if " <> name <> eqsym <> coqexp arg
   <> " then " <> lambda xs (n + 1) e m
   <> " else " <> T.pack m <> " " <> stateVar <> " " <> lambdaArgs n where
   name = anon <> T.pack (show n)
   lambdaArgs i = T.unwords $ map (\a -> anon <> T.pack (show a)) [0..i]
-  eqsym (ExpInt _) = " =? "
-  eqsym (ExpBool _) = " =?? "
-  eqsym (ExpBytes _) = error "bytestrings not supported"
+  eqsym = case argType of
+    SInteger -> " =? "
+    SBoolean -> " =?? "
+    SByteStr -> error "bytestrings not supported"
 
 -- | produce a block of declarations from an interface
 interface :: Interface -> T.Text
@@ -210,9 +210,9 @@ abiType a = error $ show a
 
 -- | coq syntax for a return type
 returnType :: TypedExp -> T.Text
-returnType (ExpInt _) = "Z"
-returnType (ExpBool _) = "bool"
-returnType (ExpBytes _) = "bytestrings not supported"
+returnType (TExp SInteger _) = "Z"
+returnType (TExp SBoolean _) = "bool"
+returnType (TExp SByteStr _) = error "bytestrings not supported"
 
 -- | default value for a given type
 -- this is used in cases where a value is not set in the constructor
@@ -237,7 +237,7 @@ coqexp :: Exp a -> T.Text
 -- booleans
 coqexp (LitBool True)  = "true"
 coqexp (LitBool False) = "false"
-coqexp (BoolVar name)  = T.pack name
+coqexp (Var SBoolean name)  = T.pack name
 coqexp (And e1 e2)  = parens $ "andb "   <> coqexp e1 <> " " <> coqexp e2
 coqexp (Or e1 e2)   = parens $ "orb"     <> coqexp e1 <> " " <> coqexp e2
 coqexp (Impl e1 e2) = parens $ "implb"   <> coqexp e1 <> " " <> coqexp e2
@@ -251,7 +251,7 @@ coqexp (GEQ e1 e2)  = parens $ coqexp e2 <> " <=? " <> coqexp e1
 
 -- integers
 coqexp (LitInt i) = T.pack $ show i
-coqexp (IntVar name)  = T.pack name
+coqexp (Var SInteger name)  = T.pack name
 coqexp (Add e1 e2) = parens $ coqexp e1 <> " + " <> coqexp e2
 coqexp (Sub e1 e2) = parens $ coqexp e1 <> " - " <> coqexp e2
 coqexp (Mul e1 e2) = parens $ coqexp e1 <> " * " <> coqexp e2
@@ -264,7 +264,7 @@ coqexp (UIntMin n) = parens $ "UINT_MIN " <> T.pack (show n)
 coqexp (UIntMax n) = parens $ "UINT_MAX " <> T.pack (show n)
 
 -- polymorphic
-coqexp (TEntry e w) = entry e w
+coqexp (TEntry w e) = entry e w
 coqexp (ITE b e1 e2) = parens $ "if "
                              <> coqexp b
                              <> " then "
@@ -276,7 +276,7 @@ coqexp (ITE b e1 e2) = parens $ "if "
 coqexp (IntEnv e) = error $ show e <> ": environment values not yet supported"
 coqexp (Cat _ _) = error "bytestrings not supported"
 coqexp (Slice _ _ _) = error "bytestrings not supported"
-coqexp (ByVar _) = error "bytestrings not supported"
+coqexp (Var SByteStr _) = error "bytestrings not supported"
 coqexp (ByStr _) = error "bytestrings not supported"
 coqexp (ByLit _) = error "bytestrings not supported"
 coqexp (ByEnv _) = error "bytestrings not supported"
@@ -300,14 +300,12 @@ coqprop _ = error "ill formed proposition"
 
 -- | coq syntax for a typed expression
 typedexp :: TypedExp -> T.Text
-typedexp (ExpInt e)   = coqexp e
-typedexp (ExpBool e)  = coqexp e
-typedexp (ExpBytes _) = error "bytestrings not supported"
+typedexp (TExp _ e) = coqexp e
 
 entry :: TStorageItem a -> When -> T.Text
-entry BytesItem{} _    = error "bytestrings not supported"
-entry _           Post = error "TODO: missing support for poststate references in coq backend"
-entry item        Pre  = case ixsFromItem item of
+entry (Item SByteStr _ _ _) _    = error "bytestrings not supported"
+entry _                     Post = error "TODO: missing support for poststate references in coq backend"
+entry item                  _    = case ixsFromItem item of
   []       -> parens $ T.pack (idFromItem item) <> " " <> stateVar
   (ix:ixs) -> parens $ T.pack (idFromItem item) <> " s " <> coqargs (ix :| ixs)
 

src/Enrich.hs

@@ -7,11 +7,10 @@ import Data.Maybe
 import Data.List (nub)
 import qualified Data.Map.Strict as Map (lookup)
 
-import EVM.ABI (AbiType(..))
 import EVM.Solidity (SlotType(..))
 
 import Syntax
-import Syntax.Typed
+import Syntax.Annotated
 import Type (bound, defaultStore)
 
 -- | Adds extra preconditions to non constructor behaviours based on the types of their variables
@@ -49,7 +48,7 @@ enrichBehaviour store behv@(Behaviour _ _ _ (Interface _ decls) pre _ stateUpdat
 
 -- | Adds type bounds for calldata, environment vars, and storage vars
 enrichInvariant :: Store -> Constructor -> Invariant -> Invariant
-enrichInvariant store (Constructor _ _ (Interface _ decls) _ _ _ _) inv@(Invariant _ preconds storagebounds predicate) =
+enrichInvariant store (Constructor _ _ (Interface _ decls) _ _ _ _) inv@(Invariant _ preconds storagebounds (predicate,_)) =
   inv { _ipreconditions = preconds', _istoragebounds = storagebounds' }
     where
       preconds' = preconds
@@ -58,12 +57,12 @@ enrichInvariant store (Constructor _ _ (Interface _ decls) _ _ _ _) inv@(Invaria
       storagebounds' = storagebounds
                        <> mkStorageBounds store (Constant <$> locsFromExp predicate)
 
-mkEthEnvBounds :: [EthEnv] -> [Exp Bool t]
+mkEthEnvBounds :: [EthEnv] -> [Exp Bool]
 mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars
   where
-    mkBound :: EthEnv -> Maybe (Exp Bool t)
+    mkBound :: EthEnv -> Maybe (Exp Bool)
     mkBound e = case lookup e defaultStore of
-      Just (Integer) -> Just $ bound (toAbiType e) (IntEnv e)
+      Just Integer -> Just $ bound (toAbiType e) (IntEnv e)
       _ -> Nothing
 
     toAbiType :: EthEnv -> AbiType
@@ -83,16 +82,16 @@ mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars
       Nonce -> AbiUIntType 256
 
 -- | extracts bounds from the AbiTypes of Integer values in storage
-mkStorageBounds :: Store -> [Rewrite] -> [Exp Bool Untimed]
+mkStorageBounds :: Store -> [Rewrite] -> [Exp Bool]
 mkStorageBounds store refs = catMaybes $ mkBound <$> refs
   where
-    mkBound :: Rewrite -> Maybe (Exp Bool Untimed)
-    mkBound (Constant (IntLoc item)) = Just $ fromItem item
-    mkBound (Rewrite (IntUpdate item _)) = Just $ fromItem item
+    mkBound :: Rewrite -> Maybe (Exp Bool)
+    mkBound (Constant (Loc SInteger item)) = Just $ fromItem item
+    mkBound (Rewrite (Update SInteger item _)) = Just $ fromItem item
     mkBound _ = Nothing
 
-    fromItem :: TStorageItem Integer Untimed -> Exp Bool Untimed
-    fromItem item@(IntItem contract name _) = bound (abiType $ slotType contract name) (TEntry item Neither)
+    fromItem :: TStorageItem Integer -> Exp Bool
+    fromItem item@(Item _ contract name _) = bound (abiType $ slotType contract name) (TEntry Pre item)
 
     slotType :: Id -> Id -> SlotType
     slotType contract name = let
@@ -103,7 +102,7 @@ mkStorageBounds store refs = catMaybes $ mkBound <$> refs
     abiType (StorageMapping _ typ) = typ
     abiType (StorageValue typ) = typ
 
-mkCallDataBounds :: [Decl] -> [Exp Bool t]
-mkCallDataBounds = concatMap $ \(Decl typ name) -> case metaType typ of
-  Integer -> [bound typ (IntVar name)]
+mkCallDataBounds :: [Decl] -> [Exp Bool]
+mkCallDataBounds = concatMap $ \(Decl typ name) -> case actType typ of
+  Integer -> [bound typ (_Var name)]
   _ -> []