Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improved error handling #126

Merged
merged 37 commits into from
Nov 16, 2021
Merged
Show file tree
Hide file tree
Changes from 30 commits
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
634602c
add `ErrorLogger`
kjekac Jul 14, 2021
063c36c
error handling using `Validation` and `Writer` in `Type.hs`
kjekac Sep 1, 2021
18d78b0
add `semigroupoids` build dependency
kjekac Sep 2, 2021
68217e6
singleton types work; lets us remove several ugly `(>>=?)`
kjekac Sep 9, 2021
9e3930e
remove bad `do`
kjekac Sep 9, 2021
2a6a550
completely `Applicative` style in `Type.hs`
kjekac Sep 13, 2021
0e57111
custom `Alt`-function, `TStorageItem` uses `Sing`
kjekac Sep 13, 2021
db8b853
new error handling done in `Type.hs`
kjekac Sep 15, 2021
ed28424
parser uses new error handling
kjekac Sep 15, 2021
26d9b69
`Error` doesn't require a `Pn` (backends don't have them)
kjekac Sep 21, 2021
78327c8
add test to check error messages of polymorphic stuff
kjekac Sep 21, 2021
f76384c
`K.hs` uses `Error.hs`
kjekac Sep 27, 2021
f8c08bd
cleanup, reorg, some adaptations to new styles
kjekac Sep 27, 2021
04031e9
restructure cabal file to avoid repeated builds
kjekac Sep 27, 2021
0294e84
cleanup
kjekac Sep 27, 2021
e113d41
fix build errors
kjekac Sep 27, 2021
ebeaea3
cleanup
kjekac Sep 29, 2021
d6f125e
retrieve `Typeable` instance without extra type layer or pattern noise
kjekac Sep 29, 2021
d81dd69
all AST constructors use singletons
kjekac Oct 2, 2021
3673272
fix CI build errors
kjekac Oct 2, 2021
c5e1a0a
cleanup
kjekac Oct 2, 2021
731ad47
fix CI build errors
kjekac Oct 2, 2021
5e49b6e
Merge branch 'master' into errorlogger
kjekac Oct 2, 2021
31f33c7
cleanup
kjekac Oct 2, 2021
0b4c157
documentation
kjekac Oct 3, 2021
dab0a6b
docs
kjekac Oct 3, 2021
6a72abd
minor comment rephrasing
kjekac Oct 13, 2021
eb0c990
Apply suggestions from code review
kjekac Nov 1, 2021
b24087c
make `MType` a type synonym instead of an ADT
kjekac Nov 1, 2021
5511d0f
remove `Pn` from `Transition`
kjekac Nov 1, 2021
6c0d335
`MType` patterns and clearer `metaType` implementation
kjekac Nov 2, 2021
7031b20
simplifications, fewer constraints, COMPLETE patterns, ...
kjekac Nov 10, 2021
53b4e6f
remove custom instance reflection stuff
kjekac Nov 10, 2021
5b38496
fix CI errors
kjekac Nov 14, 2021
30e2571
restructure and rename defs in 'Syntax.Types'
kjekac Nov 14, 2021
5241996
GADT instead of existential types
kjekac Nov 14, 2021
b90f163
`enrich` outside of `compile`
kjekac Nov 14, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
101 changes: 51 additions & 50 deletions src/Main.hs → src/CLI.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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(..))
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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) (compile True contents)

prove :: FilePath -> Maybe Text -> Maybe Integer -> Bool -> IO ()
prove file' solver' smttimeout' debug' = do
Expand All @@ -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 (compile True contents) $ \claims -> do
let
catModels results = [m | Sat m <- results]
catErrors results = [e | [email protected] {} <- results]
Expand Down Expand Up @@ -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 (compile True 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 <$> compile True 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
Expand All @@ -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 <$> compile True 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
Expand Down Expand Up @@ -261,38 +262,38 @@ 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 :: Bool -> String -> Error String [Claim]
kjekac marked this conversation as resolved.
Show resolved Hide resolved
compile shouldEnrich = pure . fmap annotate . enrich' <==< typecheck <==< parse . lexer
where
enrich' = if shouldEnrich then enrich else id

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 ()
Expand Down
40 changes: 19 additions & 21 deletions src/Coq.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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 "
Expand All @@ -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"
Expand All @@ -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)

Expand Down
11 changes: 5 additions & 6 deletions src/Enrich.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ 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
Expand Down Expand Up @@ -63,7 +62,7 @@ mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars
where
mkBound :: EthEnv -> Maybe (Exp Bool t)
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
Expand All @@ -87,12 +86,12 @@ mkStorageBounds :: Store -> [Rewrite] -> [Exp Bool Untimed]
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 (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 item@(Item _ contract name _) = bound (abiType $ slotType contract name) (TEntry Neither item)

slotType :: Id -> Id -> SlotType
slotType contract name = let
Expand All @@ -105,5 +104,5 @@ mkStorageBounds store refs = catMaybes $ mkBound <$> refs

mkCallDataBounds :: [Decl] -> [Exp Bool t]
mkCallDataBounds = concatMap $ \(Decl typ name) -> case metaType typ of
Integer -> [bound typ (IntVar name)]
Integer -> [bound typ (_Var name)]
_ -> []
43 changes: 0 additions & 43 deletions src/ErrM.hs

This file was deleted.

Loading