Stop execution on ErrorBottomTotalFunction (#2088)

kore/src/Kore/Log/ErrorBottomTotalFunction.hs

@@ -11,6 +11,11 @@ module Kore.Log.ErrorBottomTotalFunction
 
 import Prelude.Kore
 
+import Control.Monad.Catch
+    ( Exception (..)
+    , MonadThrow
+    , throwM
+    )
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 
@@ -45,16 +50,21 @@ instance Pretty ErrorBottomTotalFunction where
             , "has resulted in \\bottom."
             ]
 
+instance Exception ErrorBottomTotalFunction where
+    toException = toException . SomeEntry
+    fromException exn =
+        fromException exn >>= \entry -> fromEntry entry
+
 instance Entry ErrorBottomTotalFunction where
     entrySeverity _ = Error
     helpDoc _ = "errors raised when a total function is undefined"
 
 instance SQL.Table ErrorBottomTotalFunction
 
 errorBottomTotalFunction
-    :: MonadLog logger
+    :: MonadThrow logger
     => InternalVariable variable
     => TermLike variable
     -> logger ()
 errorBottomTotalFunction (mapVariables (pure toVariableName) -> term) =
-    logEntry ErrorBottomTotalFunction { term }
+    throwM ErrorBottomTotalFunction { term }

kore/src/Kore/Step/Function/Evaluator.hs

@@ -21,6 +21,9 @@ import Control.Error
     , maybeT
     , throwE
     )
+import Control.Monad.Catch
+    ( MonadThrow
+    )
 import qualified Data.Foldable as Foldable
 
 import qualified Kore.Attribute.Pattern.Simplified as Attribute.Simplified
@@ -71,6 +74,7 @@ evaluateApplication
     :: forall variable simplifier
     .  ( InternalVariable variable
        , MonadSimplify simplifier
+       , MonadThrow simplifier
        )
     => SideCondition variable
     -- ^ The predicate from the configuration

kore/src/Kore/Step/Simplification/Application.hs

@@ -14,6 +14,10 @@ module Kore.Step.Simplification.Application
 
 import Prelude.Kore
 
+import Control.Monad.Catch
+    ( MonadThrow
+    )
+
 import qualified Kore.Internal.Conditional as Conditional
 import qualified Kore.Internal.MultiOr as MultiOr
     ( fullCrossProduct
@@ -58,7 +62,10 @@ predicates ans substitutions, applying functions on the Application(terms),
 then merging everything into an Pattern.
 -}
 simplify
-    :: (InternalVariable variable, MonadSimplify simplifier)
+    ::  ( InternalVariable variable
+        , MonadSimplify simplifier
+        , MonadThrow simplifier
+        )
     => SideCondition variable
     -> Application Symbol (OrPattern variable)
     -> simplifier (OrPattern variable)
@@ -80,7 +87,10 @@ simplify sideCondition application = do
     childrenCrossProduct = MultiOr.fullCrossProduct children
 
 makeAndEvaluateApplications
-    :: (InternalVariable variable, MonadSimplify simplifier)
+    ::  ( InternalVariable variable
+        , MonadSimplify simplifier
+        , MonadThrow simplifier
+        )
     => SideCondition variable
     -> Symbol
     -> [Pattern variable]
@@ -89,7 +99,10 @@ makeAndEvaluateApplications =
     makeAndEvaluateSymbolApplications
 
 makeAndEvaluateSymbolApplications
-    :: (InternalVariable variable, MonadSimplify simplifier)
+    ::  ( InternalVariable variable
+        , MonadSimplify simplifier
+        , MonadThrow simplifier
+        )
     => SideCondition variable
     -> Symbol
     -> [Pattern variable]
@@ -105,7 +118,10 @@ makeAndEvaluateSymbolApplications sideCondition symbol children = do
     return (MultiOr.mergeAll orResults)
 
 evaluateApplicationFunction
-    :: (InternalVariable variable, MonadSimplify simplifier)
+    ::  ( InternalVariable variable
+        , MonadSimplify simplifier
+        , MonadThrow simplifier
+        )
     => SideCondition variable
     -- ^ The predicate from the configuration
     -> ExpandedApplication variable

kore/src/Kore/Step/Simplification/TermLike.hs

@@ -10,6 +10,9 @@ module Kore.Step.Simplification.TermLike
 import Prelude.Kore
 
 import qualified Control.Lens.Combinators as Lens
+import Control.Monad.Catch
+    ( MonadThrow
+    )
 import Data.Functor.Const
 import qualified Data.Functor.Foldable as Recursive
 
@@ -167,6 +170,7 @@ simplify
     .  HasCallStack
     => InternalVariable variable
     => MonadSimplify simplifier
+    => MonadThrow simplifier
     => SideCondition variable
     -> TermLike variable
     -> simplifier (OrPattern variable)

kore/test/Test/Kore/Builtin/Definition.hs

@@ -437,7 +437,7 @@ elementMapSymbol =
 
 concatMapSymbol :: Internal.Symbol
 concatMapSymbol =
-    binarySymbol "concatMap" mapSort & hook "MAP.concat" & functional
+    binarySymbol "concatMap" mapSort & hook "MAP.concat" & function
 
 inKeysMapSymbol :: Internal.Symbol
 inKeysMapSymbol =
@@ -596,7 +596,7 @@ elementSet x = mkApplySymbol elementSetSymbol [x]
 
 concatSetSymbol :: Internal.Symbol
 concatSetSymbol =
-    binarySymbol "concatSet" setSort & hook "SET.concat" & functional
+    binarySymbol "concatSet" setSort & hook "SET.concat" & function
 
 concatSet
     :: TermLike VariableName

kore/test/Test/Kore/Step/Simplification/TermLike.hs

@@ -10,6 +10,9 @@ import Test.Tasty.HUnit
 import Control.Monad
     ( void
     )
+import Control.Monad.Catch
+    ( MonadThrow
+    )
 
 import Kore.Internal.OrPattern
     ( OrPattern
@@ -45,7 +48,7 @@ simplifyEvaluated original =
 
 newtype TestSimplifier a = TestSimplifier { getTestSimplifier :: Simplifier a }
     deriving (Functor, Applicative, Monad)
-    deriving (MonadLog, MonadSMT)
+    deriving (MonadLog, MonadSMT, MonadThrow)
 
 instance MonadSimplify TestSimplifier where
     askMetadataTools = TestSimplifier askMetadataTools