Merge branch 'main' into decompilation

.gitignore

@@ -1,16 +1,16 @@
 # generated code
-src/Lex.hs
-src/Parse.hs
-src/dist-newstyle
+src/Act/Lex.hs
+src/Act/Parse.hs
+dist-newstyle/
 tests/**/*.out
 
 # build results
 bin/
 result*
 
 # cabal
-**/*.cabal.local
-**/cabal.project.local*
+*.cabal.local
+cabal.project.local*
 src/dist/
 
 # coq

Makefile

@@ -1,20 +1,20 @@
 .DEFAULT_GOAL := compiler
 .PHONY: parser compiler docs
 
-parser: src/Lex.hs src/Parse.hs
+parser: src/Act/Lex.hs src/Act/Parse.hs
 
-src/Parse.hs: src/Parse.y src/Syntax/Untyped.hs
-	happy src/Parse.y
+src/Act/Parse.hs: src/Act/Parse.y src/Act/Syntax/Untyped.hs
+	happy src/Act/Parse.y
 
-src/Lex.hs: src/Lex.x
-	alex src/Lex.x
+src/Act/Lex.hs: src/Act/Lex.x
+	alex src/Act/Lex.x
 
 # builds the rest of the haskell files (compiler)
-bin/act: src/*.hs src/*/*.hs
-	cd src && cabal v2-install --installdir=../bin --overwrite-policy=always && cd ..
+bin/act: src/CLI/*.hs src/Act/*.hs
+	cabal v2-install --installdir=bin --overwrite-policy=always
 
-repl: src/Lex.hs src/Parse.hs
-	cd src && cabal v2-repl
+repl: src/Act/Lex.hs src/Act/Parse.hs
+	cabal v2-repl
 
 compiler: bin/act
 

src/act.cabal → act.cabal

@@ -48,16 +48,35 @@ common common
 library
   import:             common
   build-tool-depends: happy:happy, alex:alex
-  hs-source-dirs:     .
+  hs-source-dirs:     src
   default-language:   Haskell2010
-
-  exposed-modules:    CLI Error Print SMT Syntax.Annotated Syntax.TimeAgnostic Decompile Traversals
-  other-modules:      Lex Parse Coq Syntax Syntax.Untyped Syntax.Typed Syntax.Types Syntax.Timing Type Enrich Dev HEVM Consistency
+  exposed-modules:
+    Act.CLI
+    Act.Decompile
+    Act.Error
+    Act.Print
+    Act.SMT
+    Act.Syntax.Annotated
+    Act.Syntax.TimeAgnostic
+    Act.Lex
+    Act.Parse
+    Act.Coq
+    Act.Syntax
+    Act.Syntax.Untyped
+    Act.Syntax.Typed
+    Act.Syntax.Types
+    Act.Syntax.Timing
+    Act.Traversals
+    Act.Type
+    Act.Enrich
+    Act.Dev
+    Act.HEVM
+    Act.Consistency
 
 executable act
   import:             common
   main-is:            Main.hs
-  hs-source-dirs:     main
+  hs-source-dirs:     src/CLI
   default-language:   Haskell2010
   build-depends:      act
   if os(darwin)
@@ -67,9 +86,9 @@ Test-Suite test
   import:           common
   type:             exitcode-stdio-1.0
   default-language: Haskell2010
-  main-is:          Test.hs
-  hs-source-dirs:   test
-  other-modules:    DecompileTest
+  main-is:          Main.hs
+  hs-source-dirs:   src/Test
+  other-modules:    Decompile
   build-depends:    act,
                     pretty-simple          >= 2.2,
                     quickcheck-instances   >= 0.3,

src/hie.yaml → hie.yaml

@@ -1,8 +1,8 @@
 cradle:
   cabal:
-    - path: "."
+    - path: "src/Act"
       component: "lib:act"
-    - path: "./Main.hs"
+    - path: "src/CLI"
       component: "exe:act"
-    - path: "./test"
+    - path: "src/test"
       component: "test:test"

src/CLI.hs → src/Act/CLI.hs

@@ -10,7 +10,7 @@
 {-# LANGUAGE ApplicativeDo #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 
-module CLI (main, compile, proceed, prettyErrs) where
+module Act.CLI (main, compile, proceed, prettyErrs) where
 
 import Data.Aeson hiding (Bool, Number, json)
 import GHC.Generics
@@ -24,26 +24,27 @@ import qualified Data.Text as Text
 import qualified Data.Text.IO as TIO
 import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 import GHC.Natural
+import Options.Generic
 
 
 import qualified Data.ByteString.Lazy.Char8 as B
 import qualified Data.ByteString as BS
+import Data.ByteString (ByteString)
 
 import Control.Monad
 import Control.Lens.Getter
 
-import Error
-import Lex (lexer, AlexPosn(..))
-import Options.Generic
-import Parse
-import Syntax.Annotated
-import Enrich
-import SMT
-import Type
-import Coq hiding (indent)
-import HEVM
-import Consistency
-import Print
+import Act.Error
+import Act.Lex (lexer, AlexPosn(..))
+import Act.Parse
+import Act.Syntax.Annotated
+import Act.Enrich
+import Act.SMT as SMT
+import Act.Type
+import Act.Coq hiding (indent)
+import Act.HEVM
+import Act.Consistency
+import Act.Print
 
 import EVM.SymExec
 import qualified EVM.Solvers as Solvers

src/Consistency.hs → src/Act/Consistency.hs

@@ -6,7 +6,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# Language RecordWildCards #-}
 
-module Consistency (
+module Act.Consistency (
   checkCases
 ) where
 
@@ -18,11 +18,11 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 import System.Exit (exitFailure)
 import Data.Maybe
 
-import Syntax
-import Syntax.Annotated
-import SMT
-import Syntax.Untyped (makeIface)
-import Print
+import Act.Syntax
+import Act.Syntax.Annotated
+import Act.SMT as SMT
+import Act.Syntax.Untyped (makeIface)
+import Act.Print
 
 import qualified EVM.Solvers as Solvers
 

src/Coq.hs → src/Act/Coq.hs

@@ -15,7 +15,7 @@
 {-# Language DataKinds #-}
 
 
-module Coq where
+module Act.Coq where
 
 import Prelude hiding (GT, LT)
 
@@ -27,8 +27,8 @@ import Data.List (groupBy)
 import Control.Monad.State
 
 import EVM.ABI
-import Syntax
-import Syntax.Annotated
+import Act.Syntax
+import Act.Syntax.Annotated
 
 type Fresh = State Int
 

src/Decompile.hs → src/Act/Decompile.hs

@@ -24,14 +24,15 @@ Still required is a stage that transforms the Expr into one that can be safely r
   1. wrap all arithmetic expressions in a mod uint256
   2. walk up the tree from the bottom, asking the solver at each node whether or not the mod can be eliminated
 -}
-module Decompile where
+module Act.Decompile where
 
 import Prelude hiding (LT, GT)
 
 import Control.Concurrent.Async
 import Control.Monad.Except
 import Control.Monad.Extra
 import Control.Monad.State.Strict
+import Data.ByteString (ByteString)
 import Data.Containers.ListUtils
 import Data.List
 import Data.List.NonEmpty qualified as NE
@@ -60,12 +61,12 @@ import EVM.Traversals (mapExprM)
 import GHC.IO hiding (liftIO)
 import EVM.SMT
 
-import Syntax.Annotated
-import Syntax.Untyped (makeIface)
-import HEVM
-import Enrich (enrich)
-import Error
-import Traversals
+import Act.Syntax.Annotated
+import Act.Syntax.Untyped (makeIface)
+import Act.HEVM
+import Act.Enrich (enrich)
+import Act.Error
+import Act.Traversals
 
 
 -- Top Level ---------------------------------------------------------------------------------------

src/Dev.hs → src/Act/Dev.hs

@@ -1,10 +1,10 @@
-module Dev where
+module Act.Dev where
 
 
-import CLI
-import Coq (coq)
-import Enrich
-import Consistency
+import Act.CLI
+import Act.Coq (coq)
+import Act.Enrich
+import Act.Consistency
 import qualified EVM.Solvers as Solvers
 
 import qualified Data.Text as T

src/Enrich.hs → src/Act/Enrich.hs

@@ -1,14 +1,14 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE DataKinds #-}
 
-module Enrich (enrich, mkStorageBounds) where
+module Act.Enrich (enrich, mkStorageBounds) where
 
 import Data.Maybe
 import Data.List (nub)
 
-import Syntax
-import Syntax.Annotated
-import Type (defaultStore)
+import Act.Syntax
+import Act.Syntax.Annotated
+import Act.Type (defaultStore)
 
 -- | Adds extra preconditions to non constructor behaviours based on the types of their variables
 enrich :: Act -> Act

src/Error.hs → src/Act/Error.hs

@@ -1,7 +1,4 @@
 {-# LANGUAGE OverloadedLists #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE RankNTypes #-}
@@ -16,16 +13,16 @@ and keep track of a 'Pn' for every error it logs. There is also some infrastruct
 around modified chaining/branching behaviours.
 -}
 
-module Error (module Error) where
+module Act.Error (module Act.Error) where
 
 import Data.List (find)
 import Data.List.NonEmpty as NE
-import Data.Validation as Error
+import Data.Validation as Act.Error
 
-import Syntax.Untyped (Pn)
+import Act.Syntax.Untyped (Pn)
 
 -- Reexport NonEmpty so that we can use `-XOverloadedLists` without thinking.
-import Data.List.NonEmpty as Error (NonEmpty)
+import Data.List.NonEmpty as Act.Error (NonEmpty)
 
 type Error e = Validation (NonEmpty (Pn,e))
 

src/HEVM.hs → src/Act/HEVM.hs

@@ -11,7 +11,7 @@
 {-# LANGUAGE NoFieldSelectors #-}
 
 
-module HEVM where
+module Act.HEVM where
 
 import qualified Data.Map as M
 import Data.List
@@ -21,6 +21,7 @@ import qualified Data.Text.IO as TIO
 import qualified Data.Text.Lazy.IO as TL
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Char8 as B8 (pack)
+import Data.ByteString (ByteString)
 import Data.Text.Encoding (encodeUtf8)
 import Control.Concurrent.Async
 import Control.Monad
@@ -29,9 +30,9 @@ import Data.Maybe
 import System.Exit ( exitFailure )
 import Control.Monad.ST (stToIO)
 
-import Syntax.Annotated
-import Syntax.Untyped (makeIface)
-import Syntax
+import Act.Syntax.Annotated as Act
+import Act.Syntax.Untyped (makeIface)
+import Act.Syntax
 
 import EVM.ABI (Sig(..))
 import qualified EVM.Types as EVM hiding (Contract(..), FrameState(..))
@@ -125,7 +126,7 @@ translateActConstr (Act _ _) _ = error "TODO multiple contracts"
 
 translateConstructor :: Layout -> Constructor -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata, Sig)
 translateConstructor layout (Constructor cid iface preconds _ _ upds) bytecode =
-  (cid, [EVM.Success (snd calldata <> (fmap (toProp layout) $ preconds)) mempty (EVM.ConcreteBuf bytecode) (updatesToExpr layout cid upds initmap)],
+  (cid, [EVM.Success (snd calldata <> (fmap (toProp layout) preconds)) mempty (EVM.ConcreteBuf bytecode) (updatesToExpr layout cid upds initmap)],
   calldata, ifaceToSig iface)
   where
     calldata = makeCtrCalldata iface
@@ -264,10 +265,10 @@ toProp layout = \case
   (Or _ e1 e2) -> pop2 EVM.POr e1 e2
   (Impl _ e1 e2) -> pop2 EVM.PImpl e1 e2
   (Neg _ e1) -> EVM.PNeg (toProp layout e1)
-  (Syntax.Annotated.LT _ e1 e2) -> op2 EVM.PLT e1 e2
+  (Act.LT _ e1 e2) -> op2 EVM.PLT e1 e2
   (LEQ _ e1 e2) -> op2 EVM.PLEq e1 e2
   (GEQ _ e1 e2) -> op2 EVM.PGEq e1 e2
-  (Syntax.Annotated.GT _ e1 e2) -> op2 EVM.PGT e1 e2
+  (Act.GT _ e1 e2) -> op2 EVM.PGT e1 e2
   (LitBool _ b) -> EVM.PBool b
   (Eq _ SInteger e1 e2) -> op2 EVM.PEq e1 e2
   (Eq _ SBoolean e1 e2) -> op2 EVM.PEq e1 e2
@@ -306,10 +307,10 @@ toExpr layout = stripMods . go
       (Or _ e1 e2) -> op2 EVM.Or e1 e2
       (Impl _ e1 e2) -> op2 (\x y -> EVM.Or (EVM.Not x) y) e1 e2
       (Neg _ e1) -> EVM.Not (toExpr layout e1)
-      (Syntax.Annotated.LT _ e1 e2) -> op2 EVM.LT e1 e2
+      (Act.LT _ e1 e2) -> op2 EVM.LT e1 e2
       (LEQ _ e1 e2) -> op2 EVM.LEq e1 e2
       (GEQ _ e1 e2) -> op2 EVM.GEq e1 e2
-      (Syntax.Annotated.GT _ e1 e2) -> op2 EVM.GT e1 e2
+      (Act.GT _ e1 e2) -> op2 EVM.GT e1 e2
       (LitBool _ b) -> EVM.Lit (fromIntegral $ fromEnum $ b)
       -- integers
       (Add _ e1 e2) -> op2 EVM.Add e1 e2

src/Lex.x → src/Act/Lex.x

@@ -1,5 +1,5 @@
 {
-module Lex
+module Act.Lex
   ( LEX (..)
   , Lexeme (..)
   , AlexPosn (..)
@@ -98,9 +98,9 @@ tokens :-
   ")"                                   { mk RPAREN }
   "["                                   { mk LBRACK }
   "]"                                   { mk RBRACK }
-  "="                                   { mk Lex.EQ }
-  ">"                                   { mk Lex.GT }
-  "<"                                   { mk Lex.LT }
+  "="                                   { mk Act.Lex.EQ }
+  ">"                                   { mk Act.Lex.GT }
+  "<"                                   { mk Act.Lex.LT }
   ":"                                   { mk COLON }
   "+"                                   { mk PLUS }
   "-"                                   { mk MINUS }