Do not keep execution graph in memory (#1804)

Author: ttuegel

kore/src/Kore/Exec.hs

@@ -30,6 +30,7 @@ import Control.Error.Util
     )
 import Control.Monad.Catch
     ( MonadCatch
+    , MonadThrow
     )
 import Control.Monad.Trans.Except
     ( runExceptT
@@ -167,6 +168,9 @@ import Kore.Unparser
     ( unparseToText
     , unparseToText2
     )
+import Log
+    ( MonadLog
+    )
 import qualified Log
 import SMT
     ( MonadSMT
@@ -197,10 +201,11 @@ data Execution =
 
 -- | Symbolic execution
 exec
-    ::  ( Log.WithLog Log.LogMessage smt
+    ::  ( MonadIO smt
+        , MonadLog smt
         , MonadProfiler smt
         , MonadSMT smt
-        , MonadIO smt
+        , MonadThrow smt
         )
     => Limit Natural
     -> VerifiedModule StepperAttributes
@@ -234,10 +239,11 @@ exec breadthLimit verifiedModule strategy initialTerm =
 
 -- | Project the value of the exit cell, if it is present.
 execGetExitCode
-    ::  ( Log.WithLog Log.LogMessage smt
+    ::  ( MonadIO smt
+        , MonadLog smt
         , MonadProfiler smt
         , MonadSMT smt
-        , MonadIO smt
+        , MonadThrow smt
         )
     => VerifiedModule StepperAttributes
     -- ^ The main module
@@ -262,10 +268,11 @@ execGetExitCode indexedModule strategy' finalTerm =
 
 -- | Symbolic search
 search
-    ::  ( Log.WithLog Log.LogMessage smt
+    ::  ( MonadIO smt
+        , MonadLog smt
         , MonadProfiler smt
         , MonadSMT smt
-        , MonadIO smt
+        , MonadThrow smt
         )
     => Limit Natural
     -> VerifiedModule StepperAttributes
@@ -404,6 +411,7 @@ boundedModelCheck
         , MonadProfiler smt
         , MonadSMT smt
         , MonadIO smt
+        , MonadThrow smt
         )
     => Limit Natural
     -> Limit Natural
@@ -584,7 +592,7 @@ simplifyReachabilityRule rule = do
 
 -- | Construct an execution graph for the given input pattern.
 execute
-    :: MonadSimplify simplifier
+    :: (MonadSimplify simplifier, MonadThrow simplifier)
     => Limit Natural
     -> VerifiedModule StepperAttributes
     -- ^ The main module

kore/src/Kore/ModelChecker/Bounded.hs

@@ -14,6 +14,9 @@ module Kore.ModelChecker.Bounded
 
 import Prelude.Kore
 
+import Control.Monad.Catch
+    ( MonadThrow
+    )
 import qualified Control.Monad.State.Strict as State
 import qualified Data.Foldable as Foldable
 import qualified Data.Graph.Inductive.Graph as Graph
@@ -100,7 +103,7 @@ bmcStrategy
 
 checkClaim
     :: forall m
-    .  MonadSimplify m
+    .  (MonadSimplify m, MonadThrow m)
     => Limit Natural
     ->  (  CommonModalPattern
         -> [Strategy (Prim CommonModalPattern (RewriteRule Variable))]
@@ -133,14 +136,14 @@ checkClaim
                         , predicate = Predicate.makeTruePredicate_
                         , substitution = mempty
                         }
-        executionGraph <- State.evalStateT
-                            (runStrategyWithSearchOrder
-                                breadthLimit
-                                transitionRule'
-                                strategy
-                                searchOrder
-                                startState)
-                            Nothing
+        executionGraph <-
+            runStrategyWithSearchOrder
+                breadthLimit
+                transitionRule'
+                strategy
+                searchOrder
+                startState
+            & flip State.evalStateT Nothing
 
         Log.logInfo . Text.pack
             $ ("searched states: " ++ (show . Graph.order . graph $ executionGraph))

kore/src/Kore/Profiler/Data.hs

@@ -17,6 +17,10 @@ import Prelude.Kore
 import Control.Monad
     ( when
     )
+import Control.Monad.Catch.Pure
+    ( CatchT
+    , mapCatchT
+    )
 import Control.Monad.Morph
     ( MFunctor (..)
     )
@@ -25,8 +29,8 @@ import Control.Monad.Reader
     )
 import qualified Control.Monad.State.Strict as Strict
 import Control.Monad.Trans.Accum
-    ( AccumT (AccumT)
-    , runAccumT
+    ( AccumT
+    , mapAccumT
     )
 import Control.Monad.Trans.Except
     ( ExceptT
@@ -55,12 +59,10 @@ import System.Clock
 import Control.Monad.Counter
 import ListT
     ( ListT (..)
-    )
-import qualified ListT
-    ( mapListT
+    , mapListT
     )
 
-{- Monad that can also handle profiling events.
+{- | Monad that can also handle profiling events.
 -}
 class Monad profiler => MonadProfiler profiler where
     profile
@@ -257,24 +259,27 @@ profileGhcEventsAnalyze event action = do
     liftIO $ traceEventIO ("STOP " ++ List.intercalate "/" event)
     return a
 
-instance (MonadProfiler m) => MonadProfiler (ReaderT thing m )
-
-instance MonadProfiler m => MonadProfiler (Strict.StateT s m)
+instance (MonadProfiler m, Monoid w) => MonadProfiler (AccumT w m)
+  where
+    profile a = mapAccumT (profile a)
+    {-# INLINE profile #-}
 
-instance MonadProfiler m => MonadProfiler (MaybeT m)
+instance MonadProfiler m => MonadProfiler (CatchT m) where
+    profile a = mapCatchT (profile a)
+    {-# INLINE profile #-}
 
-instance MonadProfiler m => MonadProfiler (IdentityT m)
+instance MonadProfiler m => MonadProfiler (CounterT m)
 
 instance MonadProfiler m => MonadProfiler (ExceptT e m)
 
+instance MonadProfiler m => MonadProfiler (IdentityT m)
+
 instance MonadProfiler m => MonadProfiler (ListT m) where
-    profile a action =
-        ListT.mapListT (profile a) action
+    profile a = mapListT (profile a)
     {-# INLINE profile #-}
 
-instance (MonadProfiler m, Monoid w) => MonadProfiler (AccumT w m)
-  where
-    profile a action = AccumT (profile a . runAccumT action)
-    {-# INLINE profile #-}
+instance MonadProfiler m => MonadProfiler (MaybeT m)
 
-instance MonadProfiler m => MonadProfiler (CounterT m)
+instance MonadProfiler m => MonadProfiler (ReaderT thing m )
+
+instance MonadProfiler m => MonadProfiler (Strict.StateT s m)

kore/src/Kore/Profiler/Profile.hs

@@ -237,11 +237,7 @@ smtDecision (sexpr :| _) action = do
         then profile ["SMT", show $ length $ show sexpr] action
         else action
 
-executionQueueLength
-    :: MonadProfiler profiler
-    => Int -> profiler result -> profiler result
-executionQueueLength len action = do
-    Configuration {logStrategy} <- profileConfiguration
-    when logStrategy
-        (profileValue ["ExecutionQueueLength"] len)
-    action
+executionQueueLength :: MonadProfiler profiler => Int -> profiler ()
+executionQueueLength len = do
+    Configuration { logStrategy } <- profileConfiguration
+    when logStrategy (profileValue ["ExecutionQueueLength"] len)

kore/src/Kore/Step.hs

@@ -61,7 +61,9 @@ import qualified Kore.Step.SMT.Evaluator as SMT.Evaluator
     ( filterMultiOr
     )
 import qualified Kore.Step.Step as Step
-import Kore.Step.Strategy
+import Kore.Step.Strategy hiding
+    ( transitionRule
+    )
 import qualified Kore.Step.Strategy as Strategy
 import qualified Kore.Step.Transition as Transition
 import Kore.Syntax.Variable