enrich outside of compile

src/CLI.hs

@@ -122,7 +122,7 @@ parse' f = do
 type' :: FilePath -> IO ()
 type' f = do
   contents <- readFile f
-  validation (prettyErrs contents) (B.putStrLn . encode) (compile True contents)
+  validation (prettyErrs contents) (B.putStrLn . encode) (enrich <$> compile contents)
 
 prove :: FilePath -> Maybe Text -> Maybe Integer -> Bool -> IO ()
 prove file' solver' smttimeout' debug' = do
@@ -134,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 True contents) $ \claims -> do
+  proceed contents (enrich <$> compile contents) $ \claims -> do
     let
       catModels results = [m | Sat m <- results]
       catErrors results = [e | e@SMT.Error {} <- results]
@@ -187,7 +187,7 @@ prove file' solver' smttimeout' debug' = do
 coq' :: FilePath -> IO()
 coq' f = do
   contents <- readFile f
-  proceed contents (compile True contents) $ \claims ->
+  proceed contents (enrich <$> compile contents) $ \claims ->
     TIO.putStr $ coq claims
 
 k :: FilePath -> FilePath -> Maybe [(Id, String)] -> Maybe String -> Bool -> Maybe String -> IO ()
@@ -196,7 +196,7 @@ k spec' soljson' gas' storage' extractbin' out' = do
   solContents  <- readFile soljson'
   let kOpts = KOptions (maybe mempty Map.fromList gas') storage' extractbin'
       errKSpecs = do
-        behvs <- toEither $ behvsFromClaims <$> compile True specContents
+        behvs <- toEither $ behvsFromClaims . enrich <$> compile specContents
         (sources, _, _) <- validate [(nowhere, "Could not read sol.json")]
                               (Solidity.readJSON . pack) solContents
         for behvs (makekSpec sources kOpts) ^. revalidate
@@ -210,7 +210,7 @@ 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 behvs <- behvsFromClaims <$> compile True specContents
+  let preprocess = do behvs <- behvsFromClaims . enrich <$> compile specContents
                       (sources, _, _) <- validate [(nowhere, "Could not read sol.json")]
                         (Solidity.readJSON . pack) solContents
                       pure (behvs, sources)
@@ -265,10 +265,8 @@ runSMTWithTimeOut solver' maybeTimeout debug' sym
 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]
-compile shouldEnrich = pure . fmap annotate . enrich' <==< typecheck <==< parse . lexer
-  where
-    enrich' = if shouldEnrich then enrich else id
+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

src/Enrich.hs

@@ -10,7 +10,7 @@ import qualified Data.Map.Strict as Map (lookup)
 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
@@ -48,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
@@ -57,10 +57,10 @@ 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)
       _ -> Nothing
@@ -82,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 :: 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@(Item _ contract name _) = bound (abiType $ slotType contract name) (TEntry Neither item)
+    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
@@ -102,7 +102,7 @@ mkStorageBounds store refs = catMaybes $ mkBound <$> refs
     abiType (StorageMapping _ typ) = typ
     abiType (StorageValue typ) = typ
 
-mkCallDataBounds :: [Decl] -> [Exp Bool t]
+mkCallDataBounds :: [Decl] -> [Exp Bool]
 mkCallDataBounds = concatMap $ \(Decl typ name) -> case actType typ of
   Integer -> [bound typ (_Var name)]
   _ -> []

src/test/Test.hs

@@ -52,7 +52,7 @@ main = defaultMain $ testGroup "act"
       -}
       [ testProperty "roundtrip" . withExponents $ do
           behv@(Behaviour name _ contract iface preconds _ _ _) <- sized genBehv
-          let actual = compile False $ prettyBehaviour behv
+          let actual = compile $ prettyBehaviour behv
               expected = if null preconds then
                   [ S Map.empty, B behv ]
                 else