{-|
This module defines types and operations for parsing SMTLib2 solver responses.

These are high-level responses, as describe in
@https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf@,
page 47, Figure 3.9.

This parser is designed to be the top level handling for solver
responses, and to be used in conjuction with
What4.Protocol.SMTLib2.Parse and What4.Protocol.SExp with the latter
handling detailed parsing of specific constructs returned in the body
of the general response.
-}

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}

module What4.Protocol.SMTLib2.Response
  (
    SMTResponse(..)
  , SMTLib2Exception(..)
  , getSolverResponse
  , getLimitedSolverResponse
  , smtParseOptions
  , strictSMTParsing
  , strictSMTParseOpt
  )
where

import           Control.Applicative
import           Control.Exception
import qualified Data.Attoparsec.Text as AT
import           Data.Maybe ( isJust )
import           Data.Text ( Text )
import qualified Data.Text as Text
import qualified Data.Text.Lazy as Lazy
import qualified Data.Text.Lazy.Builder as Builder
import qualified Prettyprinter.Util as PPU
import qualified System.IO.Streams as Streams
import qualified System.IO.Streams.Attoparsec.Text as AStreams

import qualified What4.BaseTypes as BT
import qualified What4.Config as CFG
import           What4.Protocol.SExp
import qualified What4.Protocol.SMTLib2.Syntax as SMT2
import qualified What4.Protocol.SMTWriter as SMTWriter
import           What4.Utils.Process ( filterAsync )


strictSMTParsing :: CFG.ConfigOption BT.BaseBoolType
strictSMTParsing :: ConfigOption BaseBoolType
strictSMTParsing = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
CFG.configOption BaseTypeRepr BaseBoolType
BT.BaseBoolRepr String
"solver.strict_parsing"

strictSMTParseOpt :: CFG.ConfigDesc
strictSMTParseOpt :: ConfigDesc
strictSMTParseOpt =
  forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
CFG.mkOpt ConfigOption BaseBoolType
strictSMTParsing OptionStyle BaseBoolType
CFG.boolOptSty
  (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Text -> Doc ann
PPU.reflow forall a b. (a -> b) -> a -> b
$
   [Text] -> Text
Text.concat [Text
"Strictly parse SMT responses and fail on"
               , Text
"unrecognized data (the default)."
               , Text
"This might need to be disabled when running"
               , Text
"the SMT solver in verbose mode."
               ])
  forall a. Maybe a
Nothing

smtParseOptions :: [CFG.ConfigDesc]
smtParseOptions :: [ConfigDesc]
smtParseOptions = [ ConfigDesc
strictSMTParseOpt ]


data SMTResponse = AckSuccess
                 | AckUnsupported
                 | AckError Text
                 | AckSat
                 | AckUnsat
                 | AckUnknown
                 | AckInfeasible -- SyGuS response
                 | AckFail -- SyGuS response
                 | RspName Text
                 | RspVersion Text
                 | RspErrBehavior Text
                 | RspOutOfMemory
                 | RspRsnIncomplete
                 | RspUnkReason SExp
                 | AckSuccessSExp SExp
                 | AckSkipped Text SMTResponse
                 deriving (SMTResponse -> SMTResponse -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMTResponse -> SMTResponse -> Bool
$c/= :: SMTResponse -> SMTResponse -> Bool
== :: SMTResponse -> SMTResponse -> Bool
$c== :: SMTResponse -> SMTResponse -> Bool
Eq, Int -> SMTResponse -> ShowS
[SMTResponse] -> ShowS
SMTResponse -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SMTResponse] -> ShowS
$cshowList :: [SMTResponse] -> ShowS
show :: SMTResponse -> String
$cshow :: SMTResponse -> String
showsPrec :: Int -> SMTResponse -> ShowS
$cshowsPrec :: Int -> SMTResponse -> ShowS
Show)

-- | Called to get a response from the SMT connection.

getSolverResponse :: SMTWriter.WriterConn t h
                  -> IO (Either SomeException SMTResponse)
getSolverResponse :: forall t h. WriterConn t h -> IO (Either SomeException SMTResponse)
getSolverResponse WriterConn t h
conn = do
  Either SomeException SMTResponse
mb <- forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync
        (forall r. Parser r -> InputStream Text -> IO r
AStreams.parseFromStream
          -- n.b. the parseFromStream with an attoparsec parser used
          -- here will throw
          -- System.IO.Streams.Attoparsec.ParseException on a parser
          -- failure; the rspParser throws some other parse errors
          (ResponseStrictness -> Parser SMTResponse
rspParser (forall t h. WriterConn t h -> ResponseStrictness
SMTWriter.strictParsing WriterConn t h
conn))
          (forall t h. WriterConn t h -> InputStream Text
SMTWriter.connInputHandle WriterConn t h
conn))
  forall (m :: Type -> Type) a. Monad m => a -> m a
return Either SomeException SMTResponse
mb


-- | Gets a limited set of responses, throwing an exception when a
-- response is not matched by the filter.  Also throws exceptions for
-- standard error results.  The passed command and intent arguments
-- are only used for marking error messages.
--
-- Callers which do not want exceptions thrown for standard error
-- conditions should feel free to use 'getSolverResponse' and handle
-- all response cases themselves.

getLimitedSolverResponse :: String
                         -> (SMTResponse -> Maybe a)
                         -> SMTWriter.WriterConn t h
                         -> SMT2.Command
                         -> IO a
getLimitedSolverResponse :: forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
getLimitedSolverResponse String
intent SMTResponse -> Maybe a
handleResponse WriterConn t h
conn Command
cmd =
  let validateResp :: SMTResponse -> m a
validateResp SMTResponse
rsp =
        case SMTResponse
rsp of
          SMTResponse
AckUnsupported -> forall a e. Exception e => e -> a
throw (Command -> SMTLib2Exception
SMTLib2Unsupported Command
cmd)
          (AckError Text
msg) -> forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2Error Command
cmd Text
msg)
          (AckSkipped Text
_line SMTResponse
rest) -> SMTResponse -> m a
validateResp SMTResponse
rest
          SMTResponse
_ -> case SMTResponse -> Maybe a
handleResponse SMTResponse
rsp of
                 Just a
x -> forall (m :: Type -> Type) a. Monad m => a -> m a
return a
x
                 Maybe a
Nothing -> forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$ Command -> String -> SMTResponse -> SMTLib2Exception
SMTLib2InvalidResponse Command
cmd String
intent SMTResponse
rsp
  in forall t h. WriterConn t h -> IO (Either SomeException SMTResponse)
getSolverResponse WriterConn t h
conn forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right SMTResponse
rsp -> forall {m :: Type -> Type}. Monad m => SMTResponse -> m a
validateResp SMTResponse
rsp
    Left se :: SomeException
se@(SomeException e
e)
      | forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ SomeException -> Maybe SomeException
filterAsync SomeException
se -> forall a e. Exception e => e -> a
throw e
e
      | Just (AStreams.ParseException String
_) <- forall e. Exception e => SomeException -> Maybe e
fromException SomeException
se
        -> do -- Parser failed and left the unparseable input in the
              -- stream; extract it to show the user
              Maybe Text
curInp <- forall a. InputStream a -> IO (Maybe a)
Streams.read (forall t h. WriterConn t h -> InputStream Text
SMTWriter.connInputHandle WriterConn t h
conn)
              forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$ String -> [Command] -> Text -> SMTLib2Exception
SMTLib2ParseError String
intent [Command
cmd] forall a b. (a -> b) -> a -> b
$ String -> Text
Text.pack forall a b. (a -> b) -> a -> b
$
                [String] -> String
unlines [ String
"Solver response parsing failure."
                        , String
"*** Exception: " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> String
displayException e
e
                        , String
"Attempting to parse input for " forall a. Semigroup a => a -> a -> a
<> String
intent forall a. Semigroup a => a -> a -> a
<> String
":"
                        , forall a. Show a => a -> String
show Maybe Text
curInp
                        ]
      | Bool
otherwise -> forall a e. Exception e => e -> a
throw e
e



rspParser :: SMTWriter.ResponseStrictness -> AT.Parser SMTResponse
rspParser :: ResponseStrictness -> Parser SMTResponse
rspParser ResponseStrictness
strictness =
  let lexeme :: Parser Text b -> Parser Text b
lexeme Parser Text b
p = Parser ()
skipSpaceOrNewline forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Text b
p
      parens :: Parser Text a -> Parser Text a
parens Parser Text a
p = Char -> Parser Char
AT.char Char
'(' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Text a
p forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
AT.char Char
')'
      errParser :: Parser SMTResponse
errParser = forall {a}. Parser Text a -> Parser Text a
parens forall a b. (a -> b) -> a -> b
$ forall {a}. Parser Text a -> Parser Text a
lexeme (Text -> Parser Text
AT.string Text
"error")
                  forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> (Text -> SMTResponse
AckError forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a}. Parser Text a -> Parser Text a
lexeme Parser Text
parseSMTLib2String)
      specific_success_response :: Parser SMTResponse
specific_success_response = Parser SMTResponse
check_sat_response forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
check_synth_response forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
get_info_response
      check_sat_response :: Parser SMTResponse
check_sat_response = (SMTResponse
AckSat forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text
AT.string Text
"sat")
                           forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (SMTResponse
AckUnsat forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text
AT.string Text
"unsat")
                           forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (SMTResponse
AckUnknown forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text
AT.string Text
"unknown")
      check_synth_response :: Parser SMTResponse
check_synth_response = (SMTResponse
AckInfeasible forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text
AT.string Text
"infeasible")
                             forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (SMTResponse
AckFail forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text
AT.string Text
"fail")
      get_info_response :: Parser SMTResponse
get_info_response = forall {a}. Parser Text a -> Parser Text a
parens Parser SMTResponse
info_response
      info_response :: Parser SMTResponse
info_response = Parser SMTResponse
errBhvParser
                      forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
nameParser
                      forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
unkReasonParser
                      forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
versionParser
      nameParser :: Parser SMTResponse
nameParser = forall {a}. Parser Text a -> Parser Text a
lexeme (Text -> Parser Text
AT.string Text
":name")
                   forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall {a}. Parser Text a -> Parser Text a
lexeme (Text -> SMTResponse
RspName forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
parseSMTLib2String)
      versionParser :: Parser SMTResponse
versionParser = forall {a}. Parser Text a -> Parser Text a
lexeme (Text -> Parser Text
AT.string Text
":version")
                      forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall {a}. Parser Text a -> Parser Text a
lexeme (Text -> SMTResponse
RspVersion forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
parseSMTLib2String)
      errBhvParser :: Parser SMTResponse
errBhvParser = forall {a}. Parser Text a -> Parser Text a
lexeme (Text -> Parser Text
AT.string Text
":error-behavior")
                     forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall {a}. Parser Text a -> Parser Text a
lexeme (Text -> SMTResponse
RspErrBehavior forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
                                (Text -> Parser Text
AT.string Text
"continued-execution"
                                 forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
AT.string Text
"immediate-exit")
                                 -- Explicit error instead of generic
                                 -- fallback since :error-behavior was
                                 -- matched but behavior type was not.
                                 forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2ResponseUnrecognized
                                            Command
SMT2.getErrorBehavior
                                            Text
"bad :error-behavior value")
                               )
      unkReasonParser :: Parser SMTResponse
unkReasonParser =
        forall {a}. Parser Text a -> Parser Text a
lexeme (Text -> Parser Text
AT.string Text
":reason-unknown")
        forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall {a}. Parser Text a -> Parser Text a
lexeme (SMTResponse
RspOutOfMemory forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text
AT.string Text
"memout"
                    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> SMTResponse
RspRsnIncomplete forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text
AT.string Text
"incomplete"
                    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (Char -> Parser Char
AT.char Char
'(' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> (SExp -> SMTResponse
RspUnkReason forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text -> Parser SExp
parseSExpBody Parser Text
parseSMTLib2String))
                    -- already matched :reason-unknown, so any other
                    -- arguments to that are errors.
                    forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> forall a e. Exception e => e -> a
throw (Command -> Text -> SMTLib2Exception
SMTLib2ResponseUnrecognized
                               (Builder -> Command
SMT2.Cmd Builder
"reason?")
                               Text
"bad :reason-unknown value")
                  )
  in Parser ()
skipSpaceOrNewline forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*>
     ((SMTResponse
AckSuccess forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text
AT.string Text
"success")
      forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (SMTResponse
AckUnsupported forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ Text -> Parser Text
AT.string Text
"unsupported")
      forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
specific_success_response
      forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser SMTResponse
errParser
      forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (Char -> Parser Char
AT.char Char
'(' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> (SExp -> SMTResponse
AckSuccessSExp forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text -> Parser SExp
parseSExpBody Parser Text
parseSMTLib2String))
      -- sometimes verbose output mode will generate interim text
      -- before the actual ack; the following skips lines of input
      -- that aren't recognized.
       forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (case ResponseStrictness
strictness of
              ResponseStrictness
SMTWriter.Strict -> forall (f :: Type -> Type) a. Alternative f => f a
empty
              ResponseStrictness
SMTWriter.Lenient -> Text -> SMTResponse -> SMTResponse
AckSkipped
                                   forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> Parser Text
AT.takeWhile1 (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
AT.isEndOfLine)
                                   forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (ResponseStrictness -> Parser SMTResponse
rspParser ResponseStrictness
strictness))
     )

parseSMTLib2String :: AT.Parser Text
parseSMTLib2String :: Parser Text
parseSMTLib2String = Char -> Parser Char
AT.char Char
'\"' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Parser Text
go
 where
 go :: AT.Parser Text
 go :: Parser Text
go = do Text
xs <- (Char -> Bool) -> Parser Text
AT.takeWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Eq a => a -> a -> Bool
==Char
'\"'))
         Char
_ <- Char -> Parser Char
AT.char Char
'\"'
         (do Char
_ <- Char -> Parser Char
AT.char Char
'\"'
             Text
ys <- Parser Text
go
             forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text
xs forall a. Semigroup a => a -> a -> a
<> Text
"\"" forall a. Semigroup a => a -> a -> a
<> Text
ys)
          ) forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> forall (m :: Type -> Type) a. Monad m => a -> m a
return Text
xs

----------------------------------------------------------------------

data SMTLib2Exception
  = SMTLib2Unsupported SMT2.Command
  | SMTLib2Error SMT2.Command Text
  | SMTLib2ParseError SMTLib2Intent [SMT2.Command] Text
  | SMTLib2ResponseUnrecognized SMT2.Command Text
  | SMTLib2InvalidResponse SMT2.Command SMTLib2Intent SMTResponse

type SMTLib2Intent = String

instance Show SMTLib2Exception where
  show :: SMTLib2Exception -> String
show =
    let showCmd :: Command -> String
showCmd (SMT2.Cmd Builder
c) = Text -> String
Lazy.unpack forall a b. (a -> b) -> a -> b
$ Builder -> Text
Builder.toLazyText Builder
c
    in [String] -> String
unlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      (SMTLib2Unsupported Command
cmd) ->
        [ String
"unsupported command:"
        , String
"  " forall a. Semigroup a => a -> a -> a
<> Command -> String
showCmd Command
cmd
        ]
      (SMTLib2Error Command
cmd Text
msg) ->
        [ String
"Solver reported an error:"
        , String
"  " forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
msg
        , String
"in response to command:"
        , String
"  " forall a. Semigroup a => a -> a -> a
<> Command -> String
showCmd Command
cmd
        ]
      (SMTLib2ParseError String
intent [Command]
cmds Text
msg) ->
        [ String
"Could not parse solver response:"
        , String
"  " forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
msg
        , String
"in response to commands for " forall a. Semigroup a => a -> a -> a
<> String
intent forall a. Semigroup a => a -> a -> a
<> String
":"
        ] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Command -> String
showCmd [Command]
cmds
      (SMTLib2ResponseUnrecognized Command
cmd Text
rsp) ->
        [ String
"Unrecognized response from solver:"
        , String
"  " forall a. Semigroup a => a -> a -> a
<> Text -> String
Text.unpack Text
rsp
        , String
"in response to command:"
        , String
"  " forall a. Semigroup a => a -> a -> a
<> Command -> String
showCmd Command
cmd
        ]
      (SMTLib2InvalidResponse Command
cmd String
intent SMTResponse
rsp) ->
        [ String
"Received parsed and understood but unexpected response from solver:"
        , String
"  " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show SMTResponse
rsp
        , String
"in response to command for " forall a. Semigroup a => a -> a -> a
<> String
intent forall a. Semigroup a => a -> a -> a
<> String
":"
        , String
"  " forall a. Semigroup a => a -> a -> a
<> Command -> String
showCmd Command
cmd
        ]

instance Exception SMTLib2Exception