diff --git a/cabal.project b/cabal.project index 1eeb46463..f313d31fe 100644 --- a/cabal.project +++ b/cabal.project @@ -5,7 +5,7 @@ packages: source-repository-package type: git location: https://github.com/runtimeverification/haskell-backend.git - tag: 093af3153a5e07626d9b2e628d7ad4fc77c5a723 + tag: 8f97e95b77fe590a9fe5a9b0212f32fcad0be35b subdir: kore kore-rpc-types source-repository-package diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release index 54d546889..722e1dfcf 100644 --- a/deps/haskell-backend_release +++ b/deps/haskell-backend_release @@ -1 +1 @@ -093af3153a5e07626d9b2e628d7ad4fc77c5a723 +8f97e95b77fe590a9fe5a9b0212f32fcad0be35b diff --git a/flake.lock b/flake.lock index 8b269cba5..51f3b4083 100644 --- a/flake.lock +++ b/flake.lock @@ -13,17 +13,17 @@ "z3": "z3" }, "locked": { - "lastModified": 1710981151, - "narHash": "sha256-K2Cy4Te3cdiKdgdqeuq9qkPHa1ds9aNIH4NXj9rPgz8=", + "lastModified": 1711373718, + "narHash": "sha256-VxC/knKFORjJVmSILng6jX35GfTNkZnfrVlGL8P1C3o=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "093af3153a5e07626d9b2e628d7ad4fc77c5a723", + "rev": "8f97e95b77fe590a9fe5a9b0212f32fcad0be35b", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "093af3153a5e07626d9b2e628d7ad4fc77c5a723", + "rev": "8f97e95b77fe590a9fe5a9b0212f32fcad0be35b", "type": "github" } }, diff --git a/flake.nix b/flake.nix index ed6337eb9..6a3f312bd 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "hs-backend-booster"; inputs = { - haskell-backend.url = "github:runtimeverification/haskell-backend/093af3153a5e07626d9b2e628d7ad4fc77c5a723"; + haskell-backend.url = "github:runtimeverification/haskell-backend/8f97e95b77fe590a9fe5a9b0212f32fcad0be35b"; stacklock2nix.follows = "haskell-backend/stacklock2nix"; nixpkgs.follows = "haskell-backend/nixpkgs"; }; diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs index dc9a5315c..646e76d97 100644 --- a/library/Booster/JsonRpc.hs +++ b/library/Booster/JsonRpc.hs @@ -24,7 +24,6 @@ import Control.Monad.Logger.CallStack (MonadLoggerIO) import Control.Monad.Logger.CallStack qualified as Log import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT) import Crypto.Hash (SHA256 (..), hashWith) -import Data.Aeson (ToJSON (toJSON)) import Data.Bifunctor (second) import Data.Coerce (coerce) import Data.Foldable @@ -70,13 +69,14 @@ import Booster.Syntax.Json.Internalise ( TermOrPredicates (..), internalisePattern, internaliseTermOrPredicate, + patternErrorToRpcError, pattern CheckSubsorts, pattern DisallowAlias, ) import Booster.Syntax.ParsedKore (parseKoreModule) import Booster.Syntax.ParsedKore.Base hiding (ParsedModule) import Booster.Syntax.ParsedKore.Base qualified as ParsedModule (ParsedModule (..)) -import Booster.Syntax.ParsedKore.Internalise (addToDefinitions) +import Booster.Syntax.ParsedKore.Internalise (addToDefinitions, definitionErrorToRpcError) import Booster.Util (Flag (..), constructorName) import Kore.JsonRpc.Error qualified as RpcError import Kore.JsonRpc.Server (ErrorObj (..), JsonRpcHandler (..), Respond) @@ -105,7 +105,12 @@ respond stateVar = case internalised of Left patternError -> do Log.logDebug $ "Error internalising cterm" <> Text.pack (show patternError) - pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternError + pure $ + Left $ + RpcError.backendError $ + RpcError.CouldNotVerifyPattern + [ patternErrorToRpcError patternError + ] Right (pat, substitution, unsupported) -> do unless (null unsupported) $ do Log.logWarnNS @@ -153,46 +158,43 @@ respond stateVar = state <- liftIO $ takeMVar stateVar let nameAsId = fromMaybe False nameAsId' moduleHash = Text.pack $ ('m' :) . show . hashWith SHA256 $ Text.encodeUtf8 _module - restoreStateAndRethrow (errTy, errMsg) = do + restoreStateAndRethrow err = do liftIO (putMVar stateVar state) - throwE $ RpcError.backendError errTy errMsg + throwE $ RpcError.backendError err listNames :: (HasField "name" a b, HasField "getId" b Text) => [a] -> Text listNames = Text.intercalate ", " . map (.name.getId) flip catchE restoreStateAndRethrow $ do newModule <- - withExceptT ((RpcError.InvalidModule,) . toJSON) $ + withExceptT (RpcError.InvalidModule . RpcError.ErrorOnly . pack) $ except $ parseKoreModule "rpc-request" _module unless (null newModule.sorts) $ - throwE - ( RpcError.InvalidModule - , toJSON $ + throwE $ + RpcError.InvalidModule . RpcError.ErrorOnly $ "Module introduces new sorts: " <> listNames newModule.sorts - ) + unless (null newModule.symbols) $ - throwE - ( RpcError.InvalidModule - , toJSON $ + throwE $ + RpcError.InvalidModule . RpcError.ErrorOnly $ "Module introduces new symbols: " <> listNames newModule.symbols - ) -- check if we already received a module with this name when nameAsId $ case Map.lookup (getId newModule.name) state.addedModules of -- if a different module was already added, throw error - Just m | _module /= m -> throwE (RpcError.DuplicateModuleName, toJSON $ getId newModule.name) + Just m | _module /= m -> throwE $ RpcError.DuplicateModuleName $ getId newModule.name _ -> pure () -- Check for a corner case when we send module M1 with the name "m"" and name-as-id: true -- followed by adding M2. Should not happen in practice... case Map.lookup moduleHash state.addedModules of - Just m | _module /= m -> throwE (RpcError.DuplicateModuleName, toJSON moduleHash) + Just m | _module /= m -> throwE $ RpcError.DuplicateModuleName moduleHash _ -> pure () newDefinitions <- - withExceptT ((RpcError.InvalidModule,) . toJSON) $ + withExceptT (RpcError.InvalidModule . definitionErrorToRpcError) $ except $ runExcept $ addToDefinitions newModule{ParsedModule.name = Id moduleHash} state.definitions @@ -246,13 +248,18 @@ respond stateVar = result <- case internalised of Left patternErrors -> do - Log.logErrorNS "booster" $ - "Error internalising cterm: " <> Text.pack (show patternErrors) + forM_ patternErrors $ \patternError -> + Log.logErrorNS "booster" $ + "Error internalising cterm: " <> pack (show patternError) Log.logOtherNS "booster" (Log.LevelOther "ErrorDetails") (prettyPattern req.state.term) - pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrors + pure $ + Left $ + RpcError.backendError $ + RpcError.CouldNotVerifyPattern $ + map patternErrorToRpcError patternErrors -- term and predicate (pattern) Right (TermAndPredicates pat substitution unsupported) -> do Log.logInfoNS "booster" "Simplifying a pattern" @@ -282,11 +289,11 @@ respond stateVar = (Left ApplyEquations.SideConditionFalse{}, _) -> do let tSort = externaliseSort $ sortOfPattern pat pure $ Right (addHeader $ KoreJson.KJBottom tSort, []) - (Left (ApplyEquations.EquationLoop terms), _) -> - pure . Left . RpcError.backendError RpcError.Aborted $ map externaliseTerm terms -- FIXME + (Left (ApplyEquations.EquationLoop _terms), _) -> + pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected" (Left other, _) -> - pure . Left . RpcError.backendError RpcError.Aborted $ (Text.pack . constructorName $ other) -- FIXME - -- predicate only + pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) + -- predicate only Right (Predicates ps) | null ps.boolPredicates && null ps.ceilPredicates && null ps.substitution && null ps.unsupported -> pure $ @@ -324,7 +331,7 @@ respond stateVar = pure $ Right (addHeader $ Syntax.KJAnd predicateSort result, []) (Left something, _) -> - pure . Left . RpcError.backendError RpcError.Aborted $ show something + pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty something whenJust solver SMT.closeSolver stop <- liftIO $ getTime Monotonic @@ -344,13 +351,18 @@ respond stateVar = internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term case internalised of Left patternErrors -> do - Log.logErrorNS "booster" $ - "Error internalising cterm: " <> Text.pack (show patternErrors) + forM_ patternErrors $ \patternError -> + Log.logErrorNS "booster" $ + "Error internalising cterm: " <> pack (show patternError) Log.logOtherNS "booster" (Log.LevelOther "ErrorDetails") (prettyPattern req.state.term) - pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrors + pure $ + Left $ + RpcError.backendError $ + RpcError.CouldNotVerifyPattern $ + map patternErrorToRpcError patternErrors -- various predicates obtained Right things -> do Log.logInfoNS "booster" "get-model request" @@ -414,13 +426,18 @@ respond stateVar = { satisfiable = RpcTypes.Unsat , substitution = Nothing } + Left SMT.ReasonUnknown{} -> + RpcTypes.GetModelResult + { satisfiable = RpcTypes.Unknown + , substitution = Nothing + } Left SMT.Unknown -> RpcTypes.GetModelResult { satisfiable = RpcTypes.Unknown , substitution = Nothing } Left other -> - error $ "Unexpected result " <> show other <> "from getModelFor" + error $ "Unexpected result " <> show other <> " from getModelFor" Right subst -> let sort = fromMaybe (error "Unknown sort in input") $ sortOfJson req.state.term substitution @@ -463,20 +480,20 @@ respond stateVar = state <- liftIO $ readMVar stateVar let mainName = fromMaybe state.defaultMain mbMainModule case Map.lookup mainName state.definitions of - Nothing -> pure $ Left $ RpcError.backendError RpcError.CouldNotFindModule mainName + Nothing -> pure $ Left $ RpcError.backendError $ RpcError.CouldNotFindModule mainName Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions) handleSmtError :: JsonRpcHandler handleSmtError = JsonRpcHandler $ \case SMT.GeneralSMTError err -> runtimeError "problem" err SMT.SMTTranslationError err -> runtimeError "translation" err - SMT.SMTSolverUnknown premises preds -> do + SMT.SMTSolverUnknown reason premises preds -> do Log.logErrorNS "booster" "SMT returned `Unknown'" let bool = externaliseSort Pattern.SortBool -- predicates are terms of sort Bool externalise = Syntax.KJAnd bool . map (externalisePredicate bool) . Set.toList allPreds = addHeader $ Syntax.KJAnd bool [externalise premises, externalise preds] - pure $ RpcError.backendError RpcError.SmtSolverError $ toJSON allPreds + pure $ RpcError.backendError $ RpcError.SmtSolverError $ RpcError.ErrorWithTerm reason allPreds where runtimeError prefix err = do let msg = "SMT " <> prefix <> ": " <> err diff --git a/library/Booster/JsonRpc/Utils.hs b/library/Booster/JsonRpc/Utils.hs index b25e6ae63..8a8a543fa 100644 --- a/library/Booster/JsonRpc/Utils.hs +++ b/library/Booster/JsonRpc/Utils.hs @@ -21,6 +21,7 @@ import Data.Aeson as Json import Data.Aeson.Encode.Pretty (encodePretty') import Data.Aeson.Types (parseMaybe) import Data.ByteString.Lazy.Char8 qualified as BS + import Data.Maybe (fromMaybe) import Network.JSONRPC import Prettyprinter @@ -33,8 +34,12 @@ import System.Process (readProcessWithExitCode) import Booster.Definition.Base qualified as Internal import Booster.Prettyprinter import Booster.Syntax.Json.Internalise +import Data.Binary.Builder (fromLazyByteString, toLazyByteString) +import Data.List (intersperse) import Data.Map qualified as Map import Data.Set qualified as Set +import Data.Text.Encoding qualified as Text +import Kore.JsonRpc.Error qualified as RpcError import Kore.JsonRpc.Types import Kore.Syntax.Json.Types hiding (Left, Right) import Prettyprinter qualified as Pretty @@ -256,7 +261,21 @@ diffBy def pat1 pat2 = <> if null u then "" else BS.unlines ("Unsupported parts: " : map Json.encode u) internalise = either - (("Pattern could not be internalised: " <>) . Json.encode) + ( ("Pattern could not be internalised: " <>) + . toLazyByteString + . prettyRpcErrors + . map patternErrorToRpcError + ) renderBS . runExcept . internaliseTermOrPredicate DisallowAlias IgnoreSubsorts Nothing def + prettyRpcErrors = \case + [] -> "unknown error" + [e] -> prettyRpcError e + (e : es) -> prettyRpcError e <> "\n" <> prettyRpcErrors es + + prettyRpcError RpcError.ErrorWithTermAndContext{error = err, term, context} = + Text.encodeUtf8Builder err + <> "\n" + <> maybe "" ((<> "\n") . fromLazyByteString . Json.encode) term + <> maybe "" (mconcat . intersperse ", " . map Text.encodeUtf8Builder) context diff --git a/library/Booster/SMT/Base.hs b/library/Booster/SMT/Base.hs index 4c09b4acb..2aacbd872 100644 --- a/library/Booster/SMT/Base.hs +++ b/library/Booster/SMT/Base.hs @@ -14,6 +14,7 @@ import Data.ByteString.Char8 qualified as BS import Data.Data (Data) import Data.Hashable (Hashable) import Data.String +import Data.Text (Text) import GHC.Generics (Generic) import Language.Haskell.TH.Syntax (Lift) @@ -73,6 +74,7 @@ data ControlCommand data QueryCommand = CheckSat | GetValue [SExpr] -- for get-model + | GetReasonUnknown deriving stock (Eq, Ord, Show) data Response @@ -81,6 +83,7 @@ data Response | Unsat | Unknown | Values [(SExpr, Value)] + | ReasonUnknown Text | Error BS.ByteString deriving stock (Eq, Ord, Show) diff --git a/library/Booster/SMT/Interface.hs b/library/Booster/SMT/Interface.hs index ca01ddc1b..139828e10 100644 --- a/library/Booster/SMT/Interface.hs +++ b/library/Booster/SMT/Interface.hs @@ -55,7 +55,7 @@ data SMTOptions = SMTOptions data SMTError = GeneralSMTError Text | SMTTranslationError Text - | SMTSolverUnknown (Set Predicate) (Set Predicate) + | SMTSolverUnknown Text (Set Predicate) (Set Predicate) deriving (Eq, Show) instance Exception SMTError @@ -66,8 +66,8 @@ throwSMT = throw . GeneralSMTError throwSMT' :: String -> a throwSMT' = throwSMT . pack -throwUnknown :: Set Predicate -> Set Predicate -> a -throwUnknown premises preds = throw $ SMTSolverUnknown premises preds +throwUnknown :: Text -> Set Predicate -> Set Predicate -> a +throwUnknown reason premises preds = throw $ SMTSolverUnknown reason premises preds smtTranslateError :: Text -> a smtTranslateError = throw . SMTTranslationError @@ -179,9 +179,12 @@ getModelFor ctxt ps subst Unsat -> do runCmd_ SMT.Pop pure $ Left Unsat - Unknown -> do + Unknown{} -> do + res <- runCmd SMT.GetReasonUnknown runCmd_ SMT.Pop - pure $ Left Unknown + pure $ Left res + r@ReasonUnknown{} -> + pure $ Left r Values{} -> do runCmd_ SMT.Pop throwSMT' $ "Unexpected SMT response to CheckSat: " <> show satResponse @@ -306,8 +309,14 @@ checkPredicates ctxt givenPs givenSubst psToCheck (Sat, Sat) -> fail "Implication not determined" (Sat, Unsat) -> pure True (Unsat, Sat) -> pure False - (Unknown, _) -> throwUnknown givenPs psToCheck - (_, Unknown) -> throwUnknown givenPs psToCheck + (Unknown, _) -> do + smtRun GetReasonUnknown >>= \case + ReasonUnknown reason -> throwUnknown reason givenPs psToCheck + other -> throwSMT' $ "Unexpected result while calling ':reason-unknown': " <> show other + (_, Unknown) -> do + smtRun GetReasonUnknown >>= \case + ReasonUnknown reason -> throwUnknown reason givenPs psToCheck + other -> throwSMT' $ "Unexpected result while calling ':reason-unknown': " <> show other other -> throwSMT' $ "Unexpected result while checking a condition: " <> show other where smtRun_ :: SMTEncode c => c -> MaybeT (SMT io) () diff --git a/library/Booster/SMT/LowLevelCodec.hs b/library/Booster/SMT/LowLevelCodec.hs index 194c114e8..3ed849c6f 100644 --- a/library/Booster/SMT/LowLevelCodec.hs +++ b/library/Booster/SMT/LowLevelCodec.hs @@ -20,6 +20,7 @@ import Data.Functor (($>)) import Text.Read import Booster.SMT.Base +import Data.Text.Encoding (decodeUtf8) readResponse :: BS.ByteString -> Response readResponse = @@ -36,11 +37,12 @@ responseP = <|> A.string "sat" $> Sat <|> A.string "unsat" $> Unsat <|> A.string "unknown" $> Unknown - <|> A.char '(' *> errOrValuesP <* A.char ')' + <|> A.char '(' *> errOrValuesOrReasonUnknownP <* A.char ')' -errOrValuesP :: A.Parser Response -errOrValuesP = +errOrValuesOrReasonUnknownP :: A.Parser Response +errOrValuesOrReasonUnknownP = A.string "error " *> (Error <$> stringP) + <|> A.string ":reason-unknown " *> (ReasonUnknown . decodeUtf8 <$> stringP) <|> Values <$> A.many1' pairP stringP :: A.Parser BS.ByteString @@ -103,6 +105,7 @@ encodeQuery :: QueryCommand -> BS.Builder encodeQuery = \case CheckSat -> BS.shortByteString "(check-sat)" GetValue xs -> toBuilder $ List [atom "get-value", List xs] + GetReasonUnknown -> toBuilder $ List [atom "get-info", atom ":reason-unknown"] atom :: String -> SExpr atom = Atom . SMTId . BS.pack diff --git a/library/Booster/Syntax/Json/Internalise.hs b/library/Booster/Syntax/Json/Internalise.hs index c23d900c6..03d5e6e60 100644 --- a/library/Booster/Syntax/Json/Internalise.hs +++ b/library/Booster/Syntax/Json/Internalise.hs @@ -12,6 +12,7 @@ module Booster.Syntax.Json.Internalise ( internalisePredicates, lookupInternalSort, PatternError (..), + patternErrorToRpcError, internaliseSort, SortError (..), renderSortError, @@ -39,7 +40,6 @@ import Control.Monad import Control.Monad.Extra import Control.Monad.Trans.Except import Control.Monad.Trans.State -import Data.Aeson (ToJSON (..), Value, object, (.=)) import Data.Bifunctor import Data.ByteString.Char8 (ByteString, isPrefixOf) import Data.ByteString.Char8 qualified as BS @@ -67,9 +67,11 @@ import Booster.Pattern.Base qualified as Internal import Booster.Pattern.Bool qualified as Internal import Booster.Pattern.Util (freeVariables, sortOfTerm, substituteInSort) import Booster.Prettyprinter (renderDefault) +import Booster.Syntax.Json (addHeader) import Booster.Syntax.Json.Externalise (externaliseSort) import Booster.Syntax.ParsedKore.Parser (parsePattern) import Booster.Util (Flag (..)) +import Kore.JsonRpc.Error qualified as RpcError import Kore.Syntax.Json.Types qualified as Syntax pattern IsQQ, IsNotQQ :: Flag "qq" @@ -648,38 +650,38 @@ a 'data' object. If the error is a sort error, the message will contain its information while the context provides the pattern where the error occurred. -} -instance ToJSON PatternError where - toJSON = \case - NotSupported p -> - wrap "Pattern not supported" p - NoTermFound p -> - wrap "Pattern must contain at least one term" p - PatternSortError p sortErr -> - wrap (renderSortError sortErr) p - InconsistentPattern p -> - wrap "Inconsistent pattern" p - TermExpected p -> - wrap "Expected a term but found a predicate" p - PredicateExpected p -> - wrap "Expected a predicate but found a term" p - UnknownSymbol sym p -> - wrap ("Unknown symbol '" <> Syntax.getId sym <> "'") p - MacroOrAliasSymbolNotAllowed sym p -> - wrap ("Symbol '" <> Syntax.getId sym <> "' is a macro/alias") p - SubstitutionNotAllowed -> "Substitution predicates are not allowed here" - IncorrectSymbolArity p s expected got -> - wrap - ( "Inconsistent pattern. Symbol '" - <> Syntax.getId s - <> "' expected " - <> (pack $ show expected) - <> " arguments but got " - <> (pack $ show got) - ) - p - where - wrap :: Text -> Syntax.KorePattern -> Value - wrap msg p = object ["error" .= msg, "context" .= toJSON [p]] +patternErrorToRpcError :: PatternError -> RpcError.ErrorWithTermAndContext +patternErrorToRpcError = \case + NotSupported p -> + wrap "Pattern not supported" p + NoTermFound p -> + wrap "Pattern must contain at least one term" p + PatternSortError p sortErr -> + wrap (renderSortError sortErr) p + InconsistentPattern p -> + wrap "Inconsistent pattern" p + TermExpected p -> + wrap "Expected a term but found a predicate" p + PredicateExpected p -> + wrap "Expected a predicate but found a term" p + UnknownSymbol sym p -> + wrap ("Unknown symbol '" <> Syntax.getId sym <> "'") p + MacroOrAliasSymbolNotAllowed sym p -> + wrap ("Symbol '" <> Syntax.getId sym <> "' is a macro/alias") p + SubstitutionNotAllowed -> RpcError.ErrorOnly "Substitution predicates are not allowed here" + IncorrectSymbolArity p s expected got -> + wrap + ( "Inconsistent pattern. Symbol '" + <> Syntax.getId s + <> "' expected " + <> (pack $ show expected) + <> " arguments but got " + <> (pack $ show got) + ) + p + where + wrap :: Text -> Syntax.KorePattern -> RpcError.ErrorWithTermAndContext + wrap err p = RpcError.ErrorWithTerm err $ addHeader p data SortError = UnknownSort Syntax.Sort diff --git a/library/Booster/Syntax/ParsedKore/Internalise.hs b/library/Booster/Syntax/ParsedKore/Internalise.hs index b1832db5e..e53572c06 100644 --- a/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -14,6 +14,7 @@ module Booster.Syntax.ParsedKore.Internalise ( lookupModule, DefinitionError (..), symb, + definitionErrorToRpcError, ) where import Control.Monad @@ -21,7 +22,6 @@ import Control.Monad.Extra (mapMaybeM) import Control.Monad.Trans.Class import Control.Monad.Trans.Except import Control.Monad.Trans.State -import Data.Aeson (ToJSON (..), Value (..), object, (.=)) import Data.Bifunctor (first, second) import Data.ByteString.Char8 (ByteString) import Data.Coerce (Coercible, coerce) @@ -60,6 +60,7 @@ import Booster.Syntax.Json.Internalise import Booster.Syntax.ParsedKore.Base import Booster.Syntax.ParsedKore.Parser (ParsedSentence (SentenceSymbol), parseSentence) import Booster.Util (Flag (..)) +import Kore.JsonRpc.Error qualified as RpcError import Kore.Syntax.Json.Types (Id, Sort) import Kore.Syntax.Json.Types qualified as Syntax @@ -1324,34 +1325,41 @@ instance Pretty DefinitionError where ElemSymbolNotFound sym -> pretty $ "Expected an element{} symbol " <> show sym -{- | ToJSON instance (user-facing for add-module endpoint): +{- | RPC error instance (user-facing for add-module endpoint): Renders the error string as 'error', with minimal context. -} -instance ToJSON DefinitionError where - toJSON = \case - DuplicateSorts sorts -> - "Duplicate sorts" `withContext` map toJSON sorts - DuplicateSymbols syms -> - "Duplicate symbols" `withContext` map toJSON syms - DuplicateAliases aliases -> - "DuplicateAliases" `withContext` map toJSON aliases - DefinitionPatternError ref patErr -> - ("Pattern error at " <> render ref <> " in definition") `withContext` [toJSON patErr] - DefinitionAxiomError (MalformedRewriteRule rule) -> - "Malformed rewrite rule" `withContext` [toJSON rule] - DefinitionAxiomError (MalformedEquation rule) -> - "Malformed equation" `withContext` [toJSON rule] - DefinitionAxiomError (UnexpectedAxiom rule) -> - "Unknown kind of axiom" `withContext` [toJSON rule] - other -> - object ["error" .= render other, "context" .= Null] - where - withContext :: Text -> [Value] -> Value - withContext errMsg context = - object ["error" .= errMsg, "context" .= context] +definitionErrorToRpcError :: DefinitionError -> RpcError.ErrorWithTermAndContext +definitionErrorToRpcError = \case + DuplicateSorts sorts -> + "Duplicate sorts" `withContext` map (.name.getId) sorts + DuplicateSymbols syms -> + "Duplicate symbols" `withContext` map (.name.getId) syms + DuplicateAliases aliases -> + "DuplicateAliases" `withContext` map (.name.getId) aliases + DefinitionPatternError ref patErr -> + let err@RpcError.ErrorWithTermAndContext{context} = patternErrorToRpcError patErr + in err + { RpcError.context = + Just $ "Pattern error at " <> render ref <> " in definition" : fromMaybe [] context + } + DefinitionAxiomError (MalformedRewriteRule rule) -> + "Malformed rewrite rule" `withContext` [renderOneLineText $ location rule] + DefinitionAxiomError (MalformedEquation rule) -> + "Malformed equation" `withContext` [renderOneLineText $ location rule] + DefinitionAxiomError (UnexpectedAxiom rule) -> + "Unknown kind of axiom" `withContext` [renderOneLineText $ location rule] + other -> + RpcError.ErrorOnly $ render other + where + withContext :: Text -> [Text] -> RpcError.ErrorWithTermAndContext + withContext = RpcError.ErrorWithContext + + render :: Pretty a => a -> Text + render = renderOneLineText . pretty - render :: Pretty a => a -> Text - render = renderOneLineText . pretty + location rule = + either (const "unknown location") pretty $ + runExcept (Attributes.readLocation rule.attributes) data AliasError = UnknownAlias AliasName diff --git a/stack.yaml b/stack.yaml index c9cf88e1a..513c29189 100644 --- a/stack.yaml +++ b/stack.yaml @@ -12,7 +12,7 @@ extra-deps: - smtlib-backends-process-0.3 - monad-validate-1.3.0.0 - git: https://github.com/runtimeverification/haskell-backend.git - commit: 093af3153a5e07626d9b2e628d7ad4fc77c5a723 + commit: 8f97e95b77fe590a9fe5a9b0212f32fcad0be35b subdirs: - kore - kore-rpc-types diff --git a/stack.yaml.lock b/stack.yaml.lock index b7717fbc8..bb419aa9d 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -40,29 +40,29 @@ packages: original: hackage: monad-validate-1.3.0.0 - completed: - commit: 093af3153a5e07626d9b2e628d7ad4fc77c5a723 + commit: 8f97e95b77fe590a9fe5a9b0212f32fcad0be35b git: https://github.com/runtimeverification/haskell-backend.git name: kore pantry-tree: - sha256: d3a4733cdda914126a15ac6c79eb20f5539f119e7b8fe9244ddc34359bafefd4 + sha256: a7a48f4ac7cfc7c20acdf6bf477b31483f5850ebc799e3100e82bcaf0d878b1f size: 44685 subdir: kore version: 0.60.0.0 original: - commit: 093af3153a5e07626d9b2e628d7ad4fc77c5a723 + commit: 8f97e95b77fe590a9fe5a9b0212f32fcad0be35b git: https://github.com/runtimeverification/haskell-backend.git subdir: kore - completed: - commit: 093af3153a5e07626d9b2e628d7ad4fc77c5a723 + commit: 8f97e95b77fe590a9fe5a9b0212f32fcad0be35b git: https://github.com/runtimeverification/haskell-backend.git name: kore-rpc-types pantry-tree: - sha256: 109dd68910c8fa563e219647d1e7cb92dea922abe529012e757bed159069f7bc + sha256: c08829b9bd9b68d767f4a6833f0ab56d0e8841ac28571b5cec21ae85f0fc37f4 size: 476 subdir: kore-rpc-types version: 0.60.0.0 original: - commit: 093af3153a5e07626d9b2e628d7ad4fc77c5a723 + commit: 8f97e95b77fe590a9fe5a9b0212f32fcad0be35b git: https://github.com/runtimeverification/haskell-backend.git subdir: kore-rpc-types - completed: diff --git a/test/rpc-integration/test-internalise-symbols/response-incorrect-argument-length.json b/test/rpc-integration/test-internalise-symbols/response-incorrect-argument-length.json index 973b959ed..dbbd57a33 100644 --- a/test/rpc-integration/test-internalise-symbols/response-incorrect-argument-length.json +++ b/test/rpc-integration/test-internalise-symbols/response-incorrect-argument-length.json @@ -3,88 +3,92 @@ "id": 1, "error": { "code": 2, - "data": { - "context": [ - { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "LblisInt", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortK", - "args": [] - } - ], - "args": [ - { - "tag": "EVar", - "name": "VarX", - "sort": { + "data": [ + { + "term": { + "format": "KORE", + "version": 1, + "term": { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "LblisInt", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { "tag": "SortApp", "name": "SortKItem", "args": [] + }, + { + "tag": "SortApp", + "name": "SortK", + "args": [] } - } - ] - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], + ], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + } + ] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'generatedCounter'-GT-'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarGENERATEDCOUNTER'Unds'CELL'Unds'c84b0b5f", + "sort": { + "tag": "SortApp", + "name": "SortInt", "args": [] } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarGENERATEDCOUNTER'Unds'CELL'Unds'c84b0b5f", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] } - } - ] - } - ] - } - ], - "error": "Inconsistent pattern. Symbol 'Lbl'-LT-'generatedTop'-GT-'' expected 3 arguments but got 2" - }, + ] + } + ] + } + }, + "error": "Inconsistent pattern. Symbol 'Lbl'-LT-'generatedTop'-GT-'' expected 3 arguments but got 2" + } + ], "message": "Could not verify pattern" } } \ No newline at end of file diff --git a/test/rpc-integration/test-internalise-symbols/response-incorrect-argument-sort.json b/test/rpc-integration/test-internalise-symbols/response-incorrect-argument-sort.json index 010e0586e..ce2876b93 100644 --- a/test/rpc-integration/test-internalise-symbols/response-incorrect-argument-sort.json +++ b/test/rpc-integration/test-internalise-symbols/response-incorrect-argument-sort.json @@ -3,20 +3,24 @@ "id": 1, "error": { "code": 2, - "data": { - "context": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] + "data": [ + { + "term": { + "format": "KORE", + "version": 1, + "term": { + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + } } - } - ], - "error": "Incorrect sort: expected SortInt{} but got SortBool{}" - }, + }, + "error": "Incorrect sort: expected SortInt{} but got SortBool{}" + } + ], "message": "Could not verify pattern" } } \ No newline at end of file diff --git a/test/rpc-integration/test-pathological-add-module/response-add_module_with_unknown_import_fails-001.json b/test/rpc-integration/test-pathological-add-module/response-add_module_with_unknown_import_fails-001.json index deae476eb..952fad8f4 100644 --- a/test/rpc-integration/test-pathological-add-module/response-add_module_with_unknown_import_fails-001.json +++ b/test/rpc-integration/test-pathological-add-module/response-add_module_with_unknown_import_fails-001.json @@ -4,7 +4,6 @@ "error": { "code": 8, "data": { - "context": null, "error": "Module UNKNOWN not found." }, "message": "Invalid module" diff --git a/test/rpc-integration/test-pathological-add-module/response-add_module_with_unknown_named_import_fails-002.json b/test/rpc-integration/test-pathological-add-module/response-add_module_with_unknown_named_import_fails-002.json index 215bdf12b..6c9d9bf13 100644 --- a/test/rpc-integration/test-pathological-add-module/response-add_module_with_unknown_named_import_fails-002.json +++ b/test/rpc-integration/test-pathological-add-module/response-add_module_with_unknown_named_import_fails-002.json @@ -4,7 +4,6 @@ "error": { "code": 8, "data": { - "context": null, "error": "Module UNKNOWN not found." }, "message": "Invalid module" diff --git a/test/rpc-integration/test-simplify/response-if-then-else-arity-error.json b/test/rpc-integration/test-simplify/response-if-then-else-arity-error.json index 166fe5655..9fe0fcd8c 100644 --- a/test/rpc-integration/test-simplify/response-if-then-else-arity-error.json +++ b/test/rpc-integration/test-simplify/response-if-then-else-arity-error.json @@ -5,8 +5,10 @@ "code": 2, "data": [ { - "context": [ - { + "term": { + "format": "KORE", + "version": 1, + "term": { "tag": "App", "name": "inj", "sorts": [ @@ -55,12 +57,14 @@ } ] } - ], + }, "error": "Expected a predicate but found a term" }, { - "context": [ - { + "term": { + "format": "KORE", + "version": 1, + "term": { "tag": "App", "name": "Lblite", "sorts": [ @@ -91,7 +95,7 @@ } ] } - ], + }, "error": "Inconsistent pattern. Symbol 'Lblite' expected 3 arguments but got 2" } ], diff --git a/test/rpc-integration/test-simplify/response-if-then-else-sort-error.json b/test/rpc-integration/test-simplify/response-if-then-else-sort-error.json index d7d54aa76..933abbfba 100644 --- a/test/rpc-integration/test-simplify/response-if-then-else-sort-error.json +++ b/test/rpc-integration/test-simplify/response-if-then-else-sort-error.json @@ -5,8 +5,10 @@ "code": 2, "data": [ { - "context": [ - { + "term": { + "format": "KORE", + "version": 1, + "term": { "tag": "App", "name": "inj", "sorts": [ @@ -64,12 +66,14 @@ } ] } - ], + }, "error": "Expected a predicate but found a term" }, { - "context": [ - { + "term": { + "format": "KORE", + "version": 1, + "term": { "tag": "DV", "sort": { "tag": "SortApp", @@ -78,7 +82,7 @@ }, "value": "42" } - ], + }, "error": "Incorrect sort: expected SortBool{} but got SortInt{}" } ], diff --git a/test/rpc-integration/test-subsorts/response-not-subsort.json b/test/rpc-integration/test-subsorts/response-not-subsort.json index 01a0696f4..cccbede6a 100644 --- a/test/rpc-integration/test-subsorts/response-not-subsort.json +++ b/test/rpc-integration/test-subsorts/response-not-subsort.json @@ -3,38 +3,42 @@ "id": 1, "error": { "code": 2, - "data": { - "context": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortK", - "args": [] - } - ], - "args": [ - { - "tag": "EVar", - "name": "VarX", - "sort": { + "data": [ + { + "term": { + "format": "KORE", + "version": 1, + "term": { + "tag": "App", + "name": "inj", + "sorts": [ + { "tag": "SortApp", "name": "SortKItem", "args": [] + }, + { + "tag": "SortApp", + "name": "SortK", + "args": [] + } + ], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } } - } - ] - } - ], - "error": "SortKItem{} is not a subsort of SortK{}" - }, + ] + } + }, + "error": "SortKItem{} is not a subsort of SortK{}" + } + ], "message": "Could not verify pattern" } } \ No newline at end of file diff --git a/tools/booster/Proxy.hs b/tools/booster/Proxy.hs index e184798a9..5102a9bdf 100644 --- a/tools/booster/Proxy.hs +++ b/tools/booster/Proxy.hs @@ -506,7 +506,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re Execute <$> ( simplifyResult res `catch` ( \(err :: DecidePredicateUnknown) -> - pure res{reason = Aborted, unknownPredicate = Just . externaliseDecidePredicateUnknown $ err} + pure res{reason = Aborted, unknownPredicate = Just . snd . externaliseDecidePredicateUnknown $ err} ) ) other -> pure other diff --git a/tools/booster/Server.hs b/tools/booster/Server.hs index e8eb99700..b49e4ce73 100644 --- a/tools/booster/Server.hs +++ b/tools/booster/Server.hs @@ -60,7 +60,7 @@ import Kore.IndexedModule.MetadataTools (SmtMetadataTools) import Kore.Internal.TermLike (TermLike, VariableName) import Kore.JsonRpc (ServerState (..)) import Kore.JsonRpc qualified as Kore -import Kore.JsonRpc.Error hiding (Aborted) +import Kore.JsonRpc.Error hiding (Aborted, error) import Kore.JsonRpc.Server import Kore.JsonRpc.Types (API, HaltReason (..), ReqOrRes (Req, Res)) import Kore.JsonRpc.Types.Depth (Depth (..))