From bb5db537cc09905688b3b2167ea39bb07c7177ef Mon Sep 17 00:00:00 2001 From: Malcolm Langfield <35980963+langfield@users.noreply.github.com> Date: Fri, 24 Mar 2023 11:36:14 -0400 Subject: [PATCH] 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 | 1 - src/Horus/ContractInfo.hs | 7 +++-- src/Horus/Global.hs | 23 ++++++--------- src/Horus/Global/Runner.hs | 2 -- src/Horus/Module.hs | 60 +++++++++----------------------------- src/Horus/Module/Runner.hs | 21 ------------- 6 files changed, 26 insertions(+), 88 deletions(-) delete mode 100644 src/Horus/Module/Runner.hs diff --git a/horus-check.cabal b/horus-check.cabal index 86b33512..6e5086df 100644 --- a/horus-check.cabal +++ b/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 diff --git a/src/Horus/ContractInfo.hs b/src/Horus/ContractInfo.hs index a60a5314..80fa08ef 100644 --- a/src/Horus/ContractInfo.hs +++ b/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) ] diff --git a/src/Horus/Global.hs b/src/Horus/Global.hs index 9fa0f187..99682863 100644 --- a/src/Horus/Global.hs +++ b/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,7 +62,6 @@ 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) @@ -72,7 +69,7 @@ data GlobalF 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 diff --git a/src/Horus/Global/Runner.hs b/src/Horus/Global/Runner.hs index cff693b1..71c8cc15 100644 --- a/src/Horus/Global/Runner.hs +++ b/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 diff --git a/src/Horus/Module.hs b/src/Horus/Module.hs index 8180c716..2df5f1fc 100644 --- a/src/Horus/Module.hs +++ b/src/Horus/Module.hs @@ -1,11 +1,8 @@ module Horus.Module ( Module (..) - , ModuleL (..) - , ModuleF (..) - , Error (..) , IfElseOutcomeMap , apEqualsFp - , gatherModules + , gatherModulesForF , getModuleNameParts , isPreChecking , dropMain @@ -13,8 +10,6 @@ module Horus.Module 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 diff --git a/src/Horus/Module/Runner.hs b/src/Horus/Module/Runner.hs deleted file mode 100644 index 2d646617..00000000 --- a/src/Horus/Module/Runner.hs +++ /dev/null @@ -1,21 +0,0 @@ -module Horus.Module.Runner (interpret, run) where - -import Control.Arrow (left) -import Control.Monad.Except (Except, catchError, runExcept, throwError) -import Control.Monad.Free.Church (iterM) -import Data.Text (Text) - -import Horus.Module (Error, ModuleF (..), ModuleL (..)) -import Horus.Util (tShow) - -type Impl = Except Error - -interpret :: ModuleL a -> Impl a -interpret = iterM exec . runModuleL - where - exec :: ModuleF (Impl a) -> Impl a - exec (Throw t) = throwError t - exec (Catch m handler cont) = catchError (interpret m) (interpret . handler) >>= cont - -run :: ModuleL a -> Either Text a -run = left tShow . runExcept . interpret