{-# 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
| AckFail
| 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)
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
(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
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
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")
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))
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))
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