Remove ModuleL free monad

Change structure of sources:
* `(Function, ScopedName, FuncSpec)` -> `(ScopedFunction, FuncSpec)`

We also get rid of `gatherModules`, replaced with `gatherModulesForF`,
which is only for a single function.

* Remove `Module/Runner.hs` from `horus-check.cabal`

horus-check.cabal

@@ -81,7 +81,6 @@ library
       Horus.JSON.Util
       Horus.Logger
       Horus.Logger.Runner
-      Horus.Module.Runner
       Horus.Preprocessor
       Horus.Preprocessor.Runner
       Horus.Preprocessor.Solvers

src/Horus/ContractInfo.hs

@@ -38,7 +38,7 @@ data ContractInfo = ContractInfo
   , ci_functions :: Map Label ScopedFunction
   , ci_labelledInstrs :: [LabeledInst]
   , ci_program :: Program
-  , ci_sources :: [(Function, ScopedName, FuncSpec)]
+  , ci_sources :: [(ScopedFunction, FuncSpec)]
   , ci_svarSpecs :: Set ScopedName
   , ci_storageVars :: [ScopedName]
   , ci_getApTracking :: forall m. MonadError Text m => Label -> m ApTracking
@@ -218,9 +218,10 @@ mkContractInfo cd = do
    where
     msg = "Can't find 'ret' instructions for " <> tShow name <> ". Is it a function?"
 
-  mkSources :: [ScopedName] -> [(Function, ScopedName, FuncSpec)]
+  mkSources :: [ScopedName] -> [(ScopedFunction, FuncSpec)]
   mkSources generatedNames =
-    [ (f, name, toFuncSpec . getFuncSpec . ScopedFunction name $ fu_pc f)
+    [ (scopedF, toFuncSpec . getFuncSpec $ scopedF)
     | (name, IFunction f) <- Map.toList identifiers
     , name `notElem` generatedNames
+    , let scopedF = ScopedFunction name (fu_pc f)
     ]

src/Horus/Global.hs

@@ -13,7 +13,7 @@ module Horus.Global
 where
 
 import Control.Monad (when)
-import Control.Monad.Except (MonadError (..))
+import Control.Monad.Except (MonadError (..), liftEither)
 import Control.Monad.Free.Church (F, liftF)
 import Data.Foldable (for_)
 import Data.List (groupBy)
@@ -37,16 +37,14 @@ import Horus.CairoSemantics.Runner
 import Horus.CallStack (CallStack, initialWithFunc)
 import Horus.Expr qualified as Expr
 import Horus.Expr.Util (gatherLogicalVariables)
-import Horus.FunctionAnalysis (ScopedFunction (ScopedFunction, sf_pc), isWrapper)
+import Horus.FunctionAnalysis (ScopedFunction (..), isWrapper)
 import Horus.Logger qualified as L (LogL, logDebug, logError, logInfo, logWarning)
-import Horus.Module (Module (..), ModuleL, gatherModules, getModuleNameParts)
+import Horus.Module (Module (..), gatherModulesForF, getModuleNameParts)
 import Horus.Preprocessor (HorusResult (..), PreprocessorL, SolverResult (..), goalListToTextList, optimizeQuery, solve)
 import Horus.Preprocessor.Runner (PreprocessorEnv (..))
 import Horus.Preprocessor.Solvers (Solver, SolverSettings, filterMathsat, includesMathsat, isEmptySolver)
 import Horus.Program (Identifiers, Program (p_prime))
 import Horus.SW.FuncSpec (FuncSpec, FuncSpec' (fs'_pre))
-import Horus.SW.Identifier (Function (..))
-import Horus.SW.ScopedName (ScopedName ())
 import Horus.SW.Std (trustedStdFuncs)
 import Horus.Util (tShow, whenJust)
 
@@ -64,15 +62,14 @@ data GlobalF a
   = forall b. RunCFGBuildL (CFGBuildL b) (CFG -> a)
   | forall b. RunCairoSemanticsL CallStack (CairoSemanticsL b) (ConstraintsState -> a)
   | forall b. RunPreprocessorL PreprocessorEnv (PreprocessorL b) (b -> a)
-  | RunModuleL (ModuleL [Module]) ([Module] -> a)
   | GetCallee LabeledInst (ScopedFunction -> a)
   | GetConfig (Config -> a)
   | GetFuncSpec ScopedFunction (FuncSpec' -> a)
   | GetIdentifiers (Identifiers -> a)
   | GetInlinable (Set ScopedFunction -> a)
   | GetLabelledInstrs ([LabeledInst] -> a)
   | GetProgram (Program -> a)
-  | GetSources ([(Function, ScopedName, FuncSpec)] -> a)
+  | GetSources ([(ScopedFunction, FuncSpec)] -> a)
   | SetConfig Config a
   | PutStrLn' Text a
   | WriteFile' FilePath Text a
@@ -98,9 +95,6 @@ runCFGBuildL cfgBuilder = liftF' (RunCFGBuildL cfgBuilder id)
 runCairoSemanticsL :: CallStack -> CairoSemanticsL a -> GlobalL ConstraintsState
 runCairoSemanticsL initStack smt2Builder = liftF' (RunCairoSemanticsL initStack smt2Builder id)
 
-runModuleL :: ModuleL [Module] -> GlobalL [Module]
-runModuleL builder = liftF' (RunModuleL builder id)
-
 runPreprocessorL :: PreprocessorEnv -> PreprocessorL a -> GlobalL a
 runPreprocessorL penv preprocessor =
   liftF' (RunPreprocessorL penv preprocessor id)
@@ -123,7 +117,7 @@ getLabelledInstructions = liftF' (GetLabelledInstrs id)
 getProgram :: GlobalL Program
 getProgram = liftF' (GetProgram id)
 
-getSources :: GlobalL [(Function, ScopedName, FuncSpec)]
+getSources :: GlobalL [(ScopedFunction, FuncSpec)]
 getSources = liftF' (GetSources id)
 
 getIdentifiers :: GlobalL Identifiers
@@ -154,9 +148,10 @@ verbosePrint what = verbosePutStrLn (tShow what)
 
 makeModules :: (CFG, ScopedFunction -> Bool) -> GlobalL [Module]
 makeModules (cfg, allow) =
-  (runModuleL . gatherModules cfg)
-    . map (\(f, _, spec) -> (f, spec))
-    . filter (\(Function fpc _, name, _) -> allow $ ScopedFunction name fpc)
+  liftEither
+    . fmap concat
+    . mapM (gatherModulesForF cfg)
+    . filter (\(f, _) -> allow f)
     =<< getSources
 
 extractConstraints :: Module -> GlobalL ConstraintsState

src/Horus/Global/Runner.hs

@@ -17,7 +17,6 @@ import Horus.CairoSemantics.Runner qualified as CairoSemantics (run)
 import Horus.ContractInfo (ContractInfo (..))
 import Horus.Global (Config (..), GlobalF (..), GlobalL (..))
 import Horus.Logger.Runner qualified as Logger (interpret, runImpl)
-import Horus.Module.Runner qualified as Module (run)
 import Horus.Preprocessor.Runner qualified as Preprocessor (run)
 
 data Env = Env {e_config :: IORef Config, e_contractInfo :: ContractInfo}
@@ -34,7 +33,6 @@ interpret = iterM exec . runGlobalL
   exec (RunCairoSemanticsL initStack builder cont) = do
     ci <- asks e_contractInfo
     liftEither (CairoSemantics.run initStack ci builder) >>= cont
-  exec (RunModuleL builder cont) = liftEither (Module.run builder) >>= cont
   exec (RunPreprocessorL penv preprocessor cont) = do
     mPreprocessed <- lift (Preprocessor.run penv preprocessor)
     liftEither mPreprocessed >>= cont

src/Horus/Module.hs

@@ -1,20 +1,15 @@
 module Horus.Module
   ( Module (..)
-  , ModuleL (..)
-  , ModuleF (..)
-  , Error (..)
   , IfElseOutcomeMap
   , apEqualsFp
-  , gatherModules
+  , gatherModulesForF
   , getModuleNameParts
   , isPreChecking
   , dropMain
   )
 where
 
 import Control.Applicative ((<|>))
-import Control.Monad.Except (MonadError (..))
-import Control.Monad.Free.Church (F, liftF)
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe (isJust)
@@ -33,12 +28,12 @@ import Horus.Expr (Expr, Ty (..), (.&&), (.==))
 import Horus.Expr qualified as Expr
 import Horus.Expr.SMT (pprExpr)
 import Horus.Expr.Vars (ap, fp)
-import Horus.FunctionAnalysis (FInfo, FuncOp (ArcCall, ArcRet), ScopedFunction (sf_scopedName), isRetArc, sizeOfCall)
+import Horus.FunctionAnalysis (FInfo, FuncOp (ArcCall, ArcRet), ScopedFunction (..), isRetArc, sizeOfCall)
 import Horus.Instruction (LabeledInst, uncheckedCallDestination)
 import Horus.Label (moveLabel)
 import Horus.Program (Identifiers)
 import Horus.SW.FuncSpec (FuncSpec (..))
-import Horus.SW.Identifier (Function (..), getFunctionPc, getLabelPc)
+import Horus.SW.Identifier (getFunctionPc, getLabelPc)
 import Horus.SW.ScopedName (ScopedName (..), toText)
 import Horus.SW.Storage (Storage)
 
@@ -208,36 +203,11 @@ getModuleNameParts idents (Module spec prog ifElseOutcomes calledF _ mbPreChecke
           stackDigest = digestOfCallStack (Map.map sf_scopedName (pcToFun idents)) callstack
        in " Pre<" <> fName <> "|" <> stackDigest <> ">"
 
-data Error
-  = ELoopNoInvariant Label
-  | ELoopWithSVarUpdateSpec
+eLoopNoInvariant :: Label -> Text
+eLoopNoInvariant at = Text.pack $ printf "There is a loop at PC %d with no invariant" (unLabel at)
 
-instance Show Error where
-  show (ELoopNoInvariant at) = printf "There is a loop at PC %d with no invariant" (unLabel at)
-  show ELoopWithSVarUpdateSpec =
-    "Some function contains a loop, but has a spec with @storage_update annotations."
-
-data ModuleF a
-  = Throw Error
-  | forall b. Catch (ModuleL b) (Error -> ModuleL b) (b -> a)
-
-deriving stock instance Functor ModuleF
-
-newtype ModuleL a = ModuleL {runModuleL :: F ModuleF a}
-  deriving newtype (Functor, Applicative, Monad)
-
-instance MonadError Error ModuleL where
-  throwError = throw
-  catchError = catch
-
-liftF' :: ModuleF a -> ModuleL a
-liftF' = ModuleL . liftF
-
-throw :: Error -> ModuleL a
-throw t = liftF' (Throw t)
-
-catch :: ModuleL a -> (Error -> ModuleL a) -> ModuleL a
-catch m h = liftF' (Catch m h id)
+eLoopWithSVarUpdateSpec :: Text
+eLoopWithSVarUpdateSpec = "Some function contains a loop, but has a spec with @storage_update annotations."
 
 {- Revisiting nodes (thus looping) within the CFG is verboten in all cases but
     one, specifically when we are jumping back to a label that is annotated
@@ -271,15 +241,15 @@ visit ::
   FInfo ->
   Set (CallStack, Vertex) ->
   Vertex ->
-  ModuleL [Module]
+  Either Text [Module]
 visit cfg storage fPc ifElseOutcomes callstack insts pre arcCond f visited v@(Vertex _ label preCheckedF)
-  | alreadyVisited && null assertions = throwError (ELoopNoInvariant label)
-  | alreadyVisited && not (null storage) = throwError ELoopWithSVarUpdateSpec
+  | alreadyVisited && null assertions = Left (eLoopNoInvariant label)
+  | alreadyVisited && not (null storage) = Left eLoopWithSVarUpdateSpec
   | alreadyVisited || null outArcs = pure [mdl]
   | null assertions = concat <$> mapM visitArc outArcs
   | otherwise = (mdl :) . concat <$> mapM visitArc outArcs
  where
-  visitArc :: (Vertex, [LabeledInst], ArcCondition, FInfo) -> ModuleL [Module]
+  visitArc :: (Vertex, [LabeledInst], ArcCondition, FInfo) -> Either Text [Module]
   visitArc (dst, arcInsts, arcCond', f') =
     case assertions of
       [] -> visit cfg storage fPc ifElseOutcomes' callstack' (insts <> arcInsts) pre' arcCond' f' visited' dst
@@ -336,16 +306,12 @@ visit cfg storage fPc ifElseOutcomes callstack insts pre arcCond f visited v@(Ve
   A rich module is very much like a plain module except it allows side effects,
   i.e. accesses to storage variables.
 -}
-gatherFromSource :: CFG -> (Function, FuncSpec) -> ModuleL [Module]
-gatherFromSource cfg (function, FuncSpec pre _ storage) =
+gatherModulesForF :: CFG -> (ScopedFunction, FuncSpec) -> Either Text [Module]
+gatherModulesForF cfg (ScopedFunction _ fPc, FuncSpec pre _ storage) =
   concat
     <$> mapM
       (visit cfg storage fPc Map.empty callstack [] funcBeginPre ACNone Nothing Set.empty)
       (verticesLabelledBy cfg fPc)
  where
-  fPc = fu_pc function
   callstack = initialWithFunc fPc
   funcBeginPre = pre .&& (ap .== fp)
-
-gatherModules :: CFG -> [(Function, FuncSpec)] -> ModuleL [Module]
-gatherModules cfg fs = concat <$> mapM (gatherFromSource cfg) fs