Refactor rpc error types and add smt unknown reason (#3748)

Fixes #3747 --------- Co-authored-by: github-actions <[email protected]>
runtimeverification · Mar 22, 2024 · 9ee4834 · 9ee4834
1 parent 093af31
commit 9ee4834
Show file tree

Hide file tree

Showing 14 changed files with 209 additions and 77 deletions.
diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md
@@ -715,7 +715,7 @@ This error wraps an error message from the internal implication check routine, i
 ```json
 {
   "jsonrpc":"2.0",
-  "id":1
+  "id":1,
   "error": {
     "code": 4,
     "message": "Implication check error",
@@ -742,9 +742,12 @@ Error returned when the SMT solver crashes or is unable to discharge a goal.
     "code": 5,
     "message": "Smt solver error",
     "data": {
-      "format": "KORE",
-      "version": 1,
-      "term": {}
+      "term": {
+        "format": "KORE",
+        "version": 1,
+        "term": {}
+      },
+      "error": "(incomplete (theory arithmetic))",
     }
   }
 }

diff --git a/kore-rpc-types/src/Kore/JsonRpc/Error.hs b/kore-rpc-types/src/Kore/JsonRpc/Error.hs
@@ -1,13 +1,28 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
 module Kore.JsonRpc.Error (module Kore.JsonRpc.Error) where
 
 import Control.Exception (ErrorCall (..), SomeException)
 import Control.Monad.Logger (logWarnN)
 import Data.Aeson
 import Data.Char (toLower)
+import Data.Kind (Type)
 import Data.Text qualified as Text
 import Kore.JsonRpc.Server (ErrorObj (..), JsonRpcHandler (..))
+import Kore.Syntax.Json.Types (KoreJson)
 import Text.Casing (Identifier (unIdentifier), fromHumps)
 
+import Deriving.Aeson (
+    CamelToKebab,
+    FieldLabelModifier,
+    OmitNothingFields,
+    SumUntaggedValue,
+ )
+import Deriving.Aeson.Stock (CustomJSON (CustomJSON))
+import GHC.Generics
+
 toSentence :: Identifier String -> String
 toSentence = unwords . sentence . unIdentifier
   where
@@ -28,25 +43,70 @@ unsupportedOption = ErrorObj "Unsupported option" (-32003) . toJSON
 
 -- Runtime backend errors
 
+data ErrorWithContext = ErrorWithContext
+    { error :: Text.Text
+    , context :: Maybe [Text.Text]
+    }
+    deriving stock (Generic, Show, Eq)
+    deriving
+        (ToJSON)
+        via CustomJSON
+                '[SumUntaggedValue, OmitNothingFields, FieldLabelModifier '[CamelToKebab]]
+                ErrorWithContext
+
+data ErrorWithTerm = ErrorWithTerm
+    { error :: Text.Text
+    , term :: Maybe KoreJson
+    }
+    deriving stock (Generic, Show, Eq)
+    deriving
+        (ToJSON)
+        via CustomJSON '[SumUntaggedValue, OmitNothingFields, FieldLabelModifier '[CamelToKebab]] ErrorWithTerm
+
 {- | Do NOT re-order the constructors in this type!
     If new error types are to be added, only append at the end.
-    This restriction is due to using the Enum instance to generate
+    This restriction is due to using the CN typeclass to generate
     the error codes in `ErrorObj`.
 -}
 data JsonRpcBackendError
-    = CouldNotParsePattern
-    | CouldNotVerifyPattern
-    | CouldNotFindModule
-    | ImplicationCheckError
-    | SmtSolverError
-    | Aborted
-    | MultipleStates
-    | InvalidModule
-    | DuplicateModuleName
-    deriving stock (Enum, Show)
-
-backendError :: ToJSON a => JsonRpcBackendError -> a -> ErrorObj
-backendError err detail = ErrorObj (toSentence $ fromHumps $ show err) (fromEnum err + 1) (toJSON detail)
+    = CouldNotParsePattern ErrorWithContext
+    | CouldNotVerifyPattern ErrorWithContext
+    | CouldNotFindModule Text.Text
+    | ImplicationCheckError ErrorWithContext
+    | SmtSolverError ErrorWithTerm
+    | Aborted Text.Text
+    | MultipleStates Text.Text
+    | InvalidModule ErrorWithContext
+    | DuplicateModuleName Text.Text
+    deriving stock (Generic, Show, Eq)
+    deriving
+        (ToJSON)
+        via CustomJSON '[SumUntaggedValue] JsonRpcBackendError
+
+class CN (f :: Type -> Type) where
+    constructorCodeAndName' :: Int -> f x -> (Int, String)
+    countConstructors :: proxy f -> Int
+
+instance CN f => CN (D1 c f) where
+    constructorCodeAndName' n (M1 x) = constructorCodeAndName' n x
+    countConstructors _ = countConstructors @f undefined
+instance (CN f, CN g) => CN (f :+: g) where
+    constructorCodeAndName' n (L1 l) = constructorCodeAndName' n l
+    constructorCodeAndName' n (R1 r) = constructorCodeAndName' (n + countConstructors @f undefined) r
+
+    countConstructors _ = countConstructors @f undefined + countConstructors @g undefined
+
+instance Constructor c => CN (C1 c f) where
+    constructorCodeAndName' n x = (n, conName x)
+    countConstructors _ = 1
+
+constructorCodeAndName :: (CN (Rep a), Generic a) => a -> (Int, String)
+constructorCodeAndName = constructorCodeAndName' 1 . from
+
+backendError :: JsonRpcBackendError -> ErrorObj
+backendError detail = ErrorObj (toSentence $ fromHumps nm) code (toJSON detail)
+  where
+    (code, nm) = constructorCodeAndName detail
 
 -- Common runtime error handlers
 

diff --git a/kore/src/Kore/Attribute/Smtlib.hs b/kore/src/Kore/Attribute/Smtlib.hs
@@ -41,12 +41,14 @@ applySExpr ::
 applySExpr =
     \case
         Atom symb -> \args -> List (fillAtom symb args : args)
+        String str -> \_ -> String str
         list@(List _) -> fillPlacesWorker list
   where
     fillPlacesWorker =
         \case
             List sExprs -> List <$> traverse fillPlacesWorker sExprs
             Atom symb -> fillAtom symb
+            String s -> \_ -> String s
 
     fillAtom symb = fromMaybe (\_ -> Atom symb) (fillPlace symb)
 

diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs
@@ -13,7 +13,7 @@ import Control.Monad.Except (MonadError (throwError), liftEither, runExceptT, wi
 import Control.Monad.Logger (runLoggingT)
 import Control.Monad.Trans.Except (catchE)
 import Crypto.Hash (SHA256 (..), hashWith)
-import Data.Aeson.Types (ToJSON (..))
+import Data.Bifunctor (second)
 import Data.Coerce (coerce)
 import Data.Conduit.Network (serverSettings)
 import Data.Default (Default (..))
@@ -26,7 +26,7 @@ import Data.Map.Strict qualified as Map
 import Data.Sequence as Seq (Seq, empty)
 import Data.Set qualified as Set
 import Data.String (fromString)
-import Data.Text (Text)
+import Data.Text (Text, pack)
 import Data.Text.Encoding (encodeUtf8)
 import GlobalMain (
     LoadedDefinition (..),
@@ -36,6 +36,7 @@ import Kore.Attribute.Attributes (Attributes)
 import Kore.Attribute.Axiom (Label (Label), UniqueId (UniqueId), getUniqueId, unLabel)
 import Kore.Attribute.Symbol (StepperAttributes)
 import Kore.Builtin qualified as Builtin
+import Kore.Error (Error (..))
 import Kore.Exec qualified as Exec
 import Kore.Exec.GraphTraversal qualified as GraphTraversal
 import Kore.IndexedModule.MetadataTools (SmtMetadataTools)
@@ -147,7 +148,14 @@ respond serverState moduleName runSMT =
                 } -> withMainModule (coerce _module) $ \serializedModule lemmas -> do
                 start <- liftIO $ getTime Monotonic
                 case verifyIn serializedModule state of
-                    Left err -> pure $ Left $ backendError CouldNotVerifyPattern err
+                    Left Error{errorError, errorContext} ->
+                        pure $
+                            Left $
+                                backendError $
+                                    CouldNotVerifyPattern $
+                                        ErrorWithContext (pack errorError) $
+                                            Just $
+                                                map pack errorContext
                     Right verifiedPattern -> do
                         let tracingEnabled =
                                 fromMaybe False logSuccessfulRewrites || fromMaybe False logSuccessfulSimplifications
@@ -340,9 +348,9 @@ respond serverState moduleName runSMT =
                                         }
                     -- these are programmer errors
                     result@GraphTraversal.Aborted{} ->
-                        Left $ backendError Kore.JsonRpc.Error.Aborted $ show result
+                        Left $ backendError $ Kore.JsonRpc.Error.Aborted $ pack $ show result
                     other ->
-                        Left $ backendError MultipleStates $ show other
+                        Left $ backendError $ MultipleStates $ pack $ show other
 
                 patternToExecState ::
                     Bool ->
@@ -410,8 +418,14 @@ respond serverState moduleName runSMT =
         Implies ImpliesRequest{antecedent, consequent, _module, logSuccessfulSimplifications, logTiming} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do
             start <- liftIO $ getTime Monotonic
             case PatternVerifier.runPatternVerifier (verifierContext serializedModule) verify of
-                Left err ->
-                    pure $ Left $ backendError CouldNotVerifyPattern $ toJSON err
+                Left Error{errorError, errorContext} ->
+                    pure $
+                        Left $
+                            backendError $
+                                CouldNotVerifyPattern $
+                                    ErrorWithContext (pack errorError) $
+                                        Just $
+                                            map pack errorContext
                 Right (antVerified, consVerified) -> do
                     let leftPatt =
                             mkRewritingPattern $ Pattern.parsePatternFromTermLike antVerified
@@ -465,7 +479,13 @@ respond serverState moduleName runSMT =
                         , substitution = fromMaybe noSubstitution mbSubstitution
                         }
 
-            buildResult _ _ (Left err) = Left $ backendError ImplicationCheckError $ toJSON err
+            buildResult _ _ (Left Error{errorError, errorContext}) =
+                Left $
+                    backendError $
+                        ImplicationCheckError $
+                            ErrorWithContext (pack errorError) $
+                                Just $
+                                    map pack errorContext
             buildResult logs sort (Right (term, r)) =
                 let jsonTerm =
                         PatternJson.fromTermLike $
@@ -486,8 +506,14 @@ respond serverState moduleName runSMT =
         Simplify SimplifyRequest{state, _module, logSuccessfulSimplifications, logTiming} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do
             start <- liftIO $ getTime Monotonic
             case verifyIn serializedModule state of
-                Left err ->
-                    pure $ Left $ backendError CouldNotVerifyPattern err
+                Left Error{errorError, errorContext} ->
+                    pure $
+                        Left $
+                            backendError $
+                                CouldNotVerifyPattern $
+                                    ErrorWithContext (pack errorError) $
+                                        Just $
+                                            map pack errorContext
                 Right stateVerified -> do
                     let patt =
                             mkRewritingPattern $ Pattern.parsePatternFromTermLike stateVerified
@@ -522,7 +548,7 @@ respond serverState moduleName runSMT =
         AddModule AddModuleRequest{_module, nameAsId = nameAsId'} -> runExceptT $ do
             let nameAsId = fromMaybe False nameAsId'
             parsedModule@Module{moduleName = name} <-
-                withExceptT (backendError InvalidModule) $
+                withExceptT (\err -> backendError $ InvalidModule $ ErrorWithContext (pack err) Nothing) $
                     liftEither $
                         parseKoreModule "<add-module>" _module
             st@ServerState
@@ -539,13 +565,13 @@ respond serverState moduleName runSMT =
                 when nameAsId $
                     case Map.lookup (coerce name) receivedModules of
                         -- if a different module was already added, throw error
-                        Just m | _module /= m -> throwError $ backendError DuplicateModuleName name
+                        Just m | _module /= m -> throwError $ backendError $ DuplicateModuleName $ coerce name
                         _ -> pure ()
 
                 -- Check for a corner case when we send module M1 with the name "m<hash of M2>"" and name-as-id: true
                 -- followed by adding M2. Should not happen in practice...
                 case Map.lookup (coerce moduleHash) receivedModules of
-                    Just m | _module /= m -> throwError $ backendError DuplicateModuleName moduleHash
+                    Just m | _module /= m -> throwError $ backendError $ DuplicateModuleName $ coerce moduleHash
                     _ -> pure ()
 
                 case (Map.lookup (coerce moduleHash) indexedModules, Map.lookup (coerce moduleHash) serializedModules) of
@@ -573,16 +599,18 @@ respond serverState moduleName runSMT =
                         pure . AddModule $ AddModuleResult (getModuleName moduleHash)
                     _ -> do
                         (newIndexedModules, newDefinedNames) <-
-                            withExceptT (backendError InvalidModule) $
-                                liftEither $
-                                    verifyAndIndexDefinitionWithBase
-                                        (indexedModules, definedNames)
-                                        Builtin.koreVerifiers
-                                        (Definition (def @Attributes) [parsedModule{moduleName = moduleHash}])
+                            withExceptT
+                                ( \Error{errorError, errorContext} -> backendError $ InvalidModule $ ErrorWithContext (pack errorError) $ Just $ map pack errorContext
+                                )
+                                $ liftEither
+                                $ verifyAndIndexDefinitionWithBase
+                                    (indexedModules, definedNames)
+                                    Builtin.koreVerifiers
+                                    (Definition (def @Attributes) [parsedModule{moduleName = moduleHash}])
 
                         newModule <-
                             liftEither $
-                                maybe (Left $ backendError CouldNotFindModule moduleHash) Right $
+                                maybe (Left $ backendError $ CouldNotFindModule $ coerce moduleHash) Right $
                                     Map.lookup (coerce moduleHash) newIndexedModules
 
                         let metadataTools = MetadataTools.build newModule
@@ -626,8 +654,14 @@ respond serverState moduleName runSMT =
         GetModel GetModelRequest{state, _module} ->
             withMainModule (coerce _module) $ \serializedModule lemmas ->
                 case verifyIn serializedModule state of
-                    Left err ->
-                        pure $ Left $ backendError CouldNotVerifyPattern err
+                    Left Error{errorError, errorContext} ->
+                        pure $
+                            Left $
+                                backendError $
+                                    CouldNotVerifyPattern $
+                                        ErrorWithContext (pack errorError) $
+                                            Just $
+                                                map pack errorContext
                     Right stateVerified -> do
                         let sort = TermLike.termLikeSort stateVerified
                             patt =
@@ -672,7 +706,7 @@ respond serverState moduleName runSMT =
         let mainModule = fromMaybe moduleName module'
         ServerState{serializedModules} <- liftIO $ MVar.readMVar serverState
         case Map.lookup mainModule serializedModules of
-            Nothing -> pure $ Left $ backendError CouldNotFindModule mainModule
+            Nothing -> pure $ Left $ backendError $ CouldNotFindModule $ coerce mainModule
             Just (SerializedDefinition{serializedModule, lemmas}) ->
                 act serializedModule lemmas
 
@@ -776,4 +810,10 @@ runServer port serverState mainModule runSMT Log.LoggerEnv{logAction} = do
 
 handleDecidePredicateUnknown :: JsonRpcHandler
 handleDecidePredicateUnknown = JsonRpcHandler $ \(err :: DecidePredicateUnknown) ->
-    pure (backendError SmtSolverError $ externaliseDecidePredicateUnknown err)
+    pure
+        ( backendError $
+            SmtSolverError $
+                uncurry (ErrorWithTerm) $
+                    second Just $
+                        externaliseDecidePredicateUnknown err
+        )
diff --git a/kore/src/Kore/Log/DebugEvaluateCondition.hs b/kore/src/Kore/Log/DebugEvaluateCondition.hs
@@ -54,7 +54,7 @@ instance Pretty DebugEvaluateCondition where
         case result of
             Unsat -> "solver returned unsatisfiable"
             Sat -> "solver returned satisfiable"
-            Unknown -> "solver returned unknown"
+            Unknown condition -> "solver returned unknown: " <> pretty condition
 
 instance Entry DebugEvaluateCondition where
     entrySeverity _ = Debug

diff --git a/kore/src/Kore/Log/DecidePredicateUnknown.hs b/kore/src/Kore/Log/DecidePredicateUnknown.hs
@@ -20,6 +20,7 @@ import Control.Exception (
     Exception (..),
     throw,
  )
+import Data.Text (Text)
 import Debug
 import Kore.Attribute.SourceLocation (
     SourceLocation (..),
@@ -55,6 +56,7 @@ srcLoc = qLocation >>= liftLoc
 data DecidePredicateUnknown = DecidePredicateUnknown
     { action :: OnDecidePredicateUnknown
     , smtLimit :: SMT.RetryLimit
+    , message :: Text
     , predicates :: NonEmpty (Predicate VariableName)
     }
     deriving stock (Show, Eq)
@@ -108,18 +110,21 @@ throwDecidePredicateUnknown ::
     OnDecidePredicateUnknown ->
     SMT.RetryLimit ->
     NonEmpty (Predicate variable) ->
+    Text ->
     log ()
-throwDecidePredicateUnknown action smtLimit predicates' =
+throwDecidePredicateUnknown action smtLimit predicates' message =
     case action of
         WarnDecidePredicateUnknown _ _ ->
-            logEntry DecidePredicateUnknown{action, smtLimit, predicates}
+            logEntry DecidePredicateUnknown{action, smtLimit, predicates, message}
         ErrorDecidePredicateUnknown _ _ ->
-            throw DecidePredicateUnknown{action, smtLimit, predicates}
+            throw DecidePredicateUnknown{action, smtLimit, predicates, message}
   where
     predicates = Predicate.mapVariables (pure toVariableName) <$> predicates'
 
-externaliseDecidePredicateUnknown :: DecidePredicateUnknown -> PatternJson.KoreJson
-externaliseDecidePredicateUnknown err =
-    PatternJson.fromPredicate
+externaliseDecidePredicateUnknown :: DecidePredicateUnknown -> (Text, PatternJson.KoreJson)
+externaliseDecidePredicateUnknown err@DecidePredicateUnknown{message} =
+    ( message
+    , PatternJson.fromPredicate
         (TermLike.SortActualSort $ TermLike.SortActual (TermLike.Id "SortBool" TermLike.AstLocationNone) [])
         (Predicate.makeMultipleAndPredicate . toList $ predicates err)
+    )