diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md index 75d8f22a68..caf9c0c499 100644 --- 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 index 6f65969654..5627ff908a 100644 --- 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 index 4fb7280560..834afd26bc 100644 --- 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 index 810ba8df53..b9d850b8ed 100644 --- 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 "" _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"" 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 index 83a8271b14..5514ce72b2 100644 --- 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 index 55667efae2..3b34acde7d 100644 --- 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) + ) diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs index ec082655c5..c8aabf95cf 100644 --- a/kore/src/Kore/Rewrite/SMT/Evaluator.hs +++ b/kore/src/Kore/Rewrite/SMT/Evaluator.hs @@ -174,11 +174,11 @@ decidePredicate onUnknown sideCondition predicates = case result of Unsat -> return False Sat -> empty - Unknown -> do + Unknown reason -> do limit <- SMT.withSolver SMT.askRetryLimit -- depending on the value of `onUnknown`, this call will either log a warning -- or throw an error - throwDecidePredicateUnknown onUnknown limit predicates + throwDecidePredicateUnknown onUnknown limit predicates reason case onUnknown of WarnDecidePredicateUnknown _ _ -> -- the solver may be in an inconsistent state, so we re-initialize @@ -199,7 +199,7 @@ decidePredicate onUnknown sideCondition predicates = SMT.check >>= maybe empty return onErrorUnknown action = - action `Exception.catch` \(_ :: IOException) -> pure Unknown + action `Exception.catch` \(e :: IOException) -> pure $ Unknown $ Text.pack $ show e retry = retryWithScaledTimeout $ query <* debugRetrySolverQuery predicates @@ -211,12 +211,14 @@ retryWithScaledTimeout q = do -- retry it once. let timeoutScales = takeWithin limit [1 ..] retryActions = map (retryOnceWithScaledTimeout q) timeoutScales - combineRetries r1 r2 = r1 >>= whenUnknown r2 + combineRetries [] = pure $ Unknown "retry limit is 0" + combineRetries [r] = r + combineRetries (r : rs) = r >>= whenUnknown (combineRetries rs) -- This works even if 'retryActions' is infinite, because the second -- argument to 'whenUnknown' will be the 'combineRetries' of all of -- the tail of the list. As soon as a result is not 'Unknown', the - -- rest of the fold is discarded. - foldr combineRetries (pure Unknown) retryActions + -- rest of the retries are discarded. + combineRetries retryActions where -- helpers for re-trying solver queries with increasing timeout retryOnceWithScaledTimeout :: MonadSMT m => m a -> Integer -> m a @@ -229,7 +231,7 @@ retryWithScaledTimeout q = do scaleTimeOut n (SMT.TimeOut (Limit r)) = SMT.TimeOut (Limit (n * r)) whenUnknown :: Monad m => m Result -> Result -> m Result -whenUnknown f Unknown = f +whenUnknown f Unknown{} = f whenUnknown _ result = return result {- | Check if the given combination of predicates is satisfiable, and @@ -258,7 +260,7 @@ getModelFor tools predicates = -- FIXME consider variables for uninterpreted terms, too lift . SMT.withSolver $ satQuery smtPredicates (Map.elems variables) case result of - Left Unknown -> pure (Left False) + Left Unknown{} -> pure (Left False) Left Unsat -> pure (Left True) Left Sat -> pure (Left False) -- error "impossible!" Right mapping -> do @@ -280,17 +282,17 @@ getModelFor tools predicates = traverse_ SMT.assert ps satResult <- SMT.check case satResult of - Nothing -> pure $ Left Unknown + Nothing -> pure $ Left $ Unknown "no-solver" Just Unsat -> pure $ Left Unsat - Just Unknown -> pure $ Left Unknown + Just u@Unknown{} -> pure $ Left u Just Sat -> if null vars -- no free variables, trivial case then pure $ Right Map.empty else do mbMapping <- SMT.getValue vars case mbMapping of - Nothing -> pure $ Left Unknown -- something went wrong in getValue - Just mapping -> pure . Right $ Map.fromList mapping + Left e -> pure $ Left $ Unknown e -- something went wrong in getValue + Right mapping -> pure . Right $ Map.fromList mapping mkSubst :: Map.Map (ElementVariable variable) (TermLike.TermLike variable) -> diff --git a/kore/src/Kore/Rewrite/SMT/Lemma.hs b/kore/src/Kore/Rewrite/SMT/Lemma.hs index 22d3d42e97..d2da3fd96e 100644 --- a/kore/src/Kore/Rewrite/SMT/Lemma.hs +++ b/kore/src/Kore/Rewrite/SMT/Lemma.hs @@ -90,13 +90,13 @@ declareSMTLemmas tools lemmas = do Nothing -> pure () Just Sat -> pure () Just Unsat -> errorInconsistentDefinitions - Just Unknown -> do + Just Unknown{} -> do SMT.localTimeOut quadrupleTimeOut $ SMT.checkUsing checkSatTactic >>= \case Nothing -> pure () Just Sat -> pure () Just Unsat -> errorInconsistentDefinitions - Just Unknown -> errorPossiblyInconsistentDefinitions + Just Unknown{} -> errorPossiblyInconsistentDefinitions where checkSatTactic :: SExpr checkSatTactic = List [Atom "check-sat"] diff --git a/kore/src/Kore/Rewrite/SMT/Translate.hs b/kore/src/Kore/Rewrite/SMT/Translate.hs index 7f8d73c9cb..b553c76dc4 100644 --- a/kore/src/Kore/Rewrite/SMT/Translate.hs +++ b/kore/src/Kore/Rewrite/SMT/Translate.hs @@ -541,6 +541,8 @@ backTranslateWith pure $ TermLike.mkApplySymbol koreSym args | otherwise = throwError "backTranslate.List-case: implement me!" + backTranslate String{} = + throwError "backTranslate.String-case: implement me!" -- FIXME unable to recover non-standard sort names (case where Int < OtherSort) simpleSort name = SortActualSort $ SortActual (Id name AstLocationNone) [] @@ -592,3 +594,4 @@ backTranslateWith simpleSort "SortBool" backTranslateSort (List _) = error "reverse the translateSort function" -- FIXME + backTranslateSort String{} = error "invalid sort" diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs index 9865a2f421..69a48e2b33 100644 --- a/kore/src/SMT.hs +++ b/kore/src/SMT.hs @@ -217,7 +217,7 @@ checkUsing = liftSMT . checkSMTUsing {-# INLINE checkUsing #-} -- | Retrieve the given variables from the model (only valid if satisfiable) -getValue :: MonadSMT m => [SExpr] -> m (Maybe [(SExpr, SExpr)]) +getValue :: MonadSMT m => [SExpr] -> m (Either Text [(SExpr, SExpr)]) getValue = liftSMT . getValueSMT {-# INLINE getValue #-} @@ -655,19 +655,19 @@ checkSMTUsing tactic = withSolver' solverSetup (\solver -> SimpleSMT.checkUsing solver (Just tactic)) return (Just result) -getValueSMT :: [SExpr] -> SMT (Maybe [(SExpr, SExpr)]) +getValueSMT :: [SExpr] -> SMT (Either Text [(SExpr, SExpr)]) getValueSMT targets = SMT $ \case - Nothing -> return Nothing + Nothing -> return $ Left "no-solver" Just solverSetup -> traceProf ":solver:get-value" $ - onErrorNothing $ + onErrorLeft $ fmap (map (second SimpleSMT.value)) $ withSolver' solverSetup (flip SimpleSMT.getExprs targets) where - onErrorNothing :: (MonadIO m, MonadCatch m) => m a -> m (Maybe a) - onErrorNothing action = - fmap Just action `Exception.catch` \(_ :: IOException) -> pure Nothing + onErrorLeft :: (MonadIO m, MonadCatch m) => m a -> m (Either Text a) + onErrorLeft action = + fmap Right action `Exception.catch` \(e :: IOException) -> pure $ Left $ Text.pack $ show e ackCommandSMT :: SExpr -> SMT () ackCommandSMT command = diff --git a/kore/src/SMT/AST.hs b/kore/src/SMT/AST.hs index 53850bec06..1b36d83c72 100644 --- a/kore/src/SMT/AST.hs +++ b/kore/src/SMT/AST.hs @@ -68,6 +68,7 @@ import Text.Megaparsec.Char.Lexer qualified as Lexer -- | S-expressions, the basic format for SMT-LIB 2. data SExpr = Atom !Text + | String !Text | List ![SExpr] deriving stock (GHC.Generic, Eq, Ord, Show) deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) @@ -175,6 +176,7 @@ buildSExpr :: SExpr -> Builder buildSExpr = \case Atom x -> Text.Builder.fromText x + String x -> Text.Builder.singleton '"' <> Text.Builder.fromText x <> Text.Builder.singleton '"' List es -> Text.Builder.singleton '(' <> foldMap (\e -> buildSExpr e <> Text.Builder.singleton ' ') es @@ -198,6 +200,10 @@ sendSExpr h = sendSExprWorker sendSExprWorker = \case Atom atom -> Text.hPutStr h atom + String txt -> do + hPutChar h '"' + Text.hPutStr h txt + hPutChar h ')' List atoms -> do hPutChar h '(' mapM_ sendListElement atoms @@ -218,17 +224,21 @@ skipLineComment = Lexer.skipLineComment ";" -- | Basic S-expression parser. parseSExpr :: Parser SExpr -parseSExpr = parseAtom <|> parseList +parseSExpr = parseAtom <|> parseString <|> parseList where parseAtom :: Parser SExpr parseAtom = lexeme (Atom <$> Parser.takeWhile1P Nothing notSpecial) + parseString :: Parser SExpr + parseString = + String <$> (dblQuot *> Parser.takeWhile1P Nothing (/= '"') <* dblQuot) + parseList :: Parser SExpr parseList = List <$> (lparen *> Parser.many parseSExpr <* rparen) special :: Char -> Bool - special c = isSpace c || c == '(' || c == ')' || c == ';' + special c = isSpace c || c == '(' || c == ')' || c == ';' || c == '"' notSpecial :: Char -> Bool notSpecial = not . special @@ -239,6 +249,9 @@ parseSExpr = parseAtom <|> parseList rparen :: Parser Char rparen = lexeme (Parser.char ')') + dblQuot :: Parser Char + dblQuot = lexeme (Parser.char '"') + lexeme :: Parser a -> Parser a lexeme = Lexer.lexeme parseSExprSpace @@ -264,4 +277,5 @@ buildText = Text.Lazy.toStrict . Text.Builder.toLazyText . buildSExpr mapSExpr :: (Text -> Text) -> SExpr -> SExpr mapSExpr f (Atom text) = Atom (f text) +mapSExpr _ (String text) = String text mapSExpr f (List sExprs) = List (mapSExpr f <$> sExprs) diff --git a/kore/src/SMT/SimpleSMT.hs b/kore/src/SMT/SimpleSMT.hs index 31321f0bb7..19fa588f51 100644 --- a/kore/src/SMT/SimpleSMT.hs +++ b/kore/src/SMT/SimpleSMT.hs @@ -258,7 +258,7 @@ data Result | -- | The assertions are unsatisfiable Unsat | -- | The result is inconclusive - Unknown + Unknown Text deriving stock (Eq, Show) -- | Common values returned by SMT solvers. @@ -728,8 +728,8 @@ checkUsing solver tactic = do Monad.when featureProduceAssertions $ do asserts <- command solver Nothing (List [Atom "get-assertions"]) warn solver (buildText asserts) - _ <- command solver Nothing (List [Atom "get-info", Atom ":reason-unknown"]) - return Unknown + reason <- command solver Nothing (List [Atom "get-info", Atom ":reason-unknown"]) + return $ Unknown $ extractReason reason Atom "sat" -> return Sat _ -> fail $ @@ -738,6 +738,9 @@ checkUsing solver tactic = do , " Expected: unsat, unknown, or sat" , " Result: " ++ showSExpr res ] + where + extractReason (List [Atom ":reason-unknown", String reason]) = reason + extractReason other = Text.pack $ showSExpr other -- | Convert an s-expression to a value. sexprToVal :: SExpr -> Value diff --git a/kore/src/SQL.hs b/kore/src/SQL.hs index ad217aae44..838b3599a6 100644 --- a/kore/src/SQL.hs +++ b/kore/src/SQL.hs @@ -125,7 +125,7 @@ instance Column SMT.Result where toColumn SMT.Unsat = toColumn @Text "unsat" toColumn SMT.Sat = toColumn @Text "sat" - toColumn SMT.Unknown = toColumn @Text "unknown" + toColumn SMT.Unknown{} = toColumn @Text "unknown" -- | Reify a 'Column' constraint into a concrete implementation 'ColumnImpl'. mkColumnImpl :: forall a. Column a => ColumnImpl a diff --git a/test/rpc-server/simplify/smt-error/response.golden b/test/rpc-server/simplify/smt-error/response.golden index ae60d8651c..e847244de5 100644 --- a/test/rpc-server/simplify/smt-error/response.golden +++ b/test/rpc-server/simplify/smt-error/response.golden @@ -1 +1 @@ -{"jsonrpc":"2.0","id":1,"error":{"code":5,"data":{"format":"KORE","version":1,"term":{"tag":"And","sort":{"tag":"SortApp","name":"SortBool","args":[]},"patterns":[{"tag":"Ceil","argSort":{"tag":"SortApp","name":"SortInt","args":[]},"sort":{"tag":"SortApp","name":"SortBool","args":[]},"arg":{"tag":"App","name":"Lbl'UndsXor-'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"256"}]}},{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortInt","args":[]},"sort":{"tag":"SortApp","name":"SortBool","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortInt","args":[]}},"second":{"tag":"App","name":"Lbl'UndsXor-'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"256"}]}}]}},"message":"Smt solver error"}} +{"jsonrpc":"2.0","id":1,"error":{"code":5,"data":{"term":{"format":"KORE","version":1,"term":{"tag":"And","sort":{"tag":"SortApp","name":"SortBool","args":[]},"patterns":[{"tag":"Ceil","argSort":{"tag":"SortApp","name":"SortInt","args":[]},"sort":{"tag":"SortApp","name":"SortBool","args":[]},"arg":{"tag":"App","name":"Lbl'UndsXor-'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"256"}]}},{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortInt","args":[]},"sort":{"tag":"SortApp","name":"SortBool","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortInt","args":[]}},"second":{"tag":"App","name":"Lbl'UndsXor-'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"256"}]}}]}},"error":"(incomplete (theory arithmetic))"},"message":"Smt solver error"}}