liquid-fixpoint-0.9.6.3.2: src/Language/Fixpoint/Smt/Interface.hs
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DoAndIfThenElse #-}
-- | This module contains an SMTLIB2 interface for
-- 1. checking the validity, and,
-- 2. computing satisfying assignments
-- for formulas.
-- By implementing a binary interface over the SMTLIB2 format defined at
-- http://www.smt-lib.org/
-- http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf
module Language.Fixpoint.Smt.Interface (
-- * Commands
Command (..)
-- * Responses
, Response (..)
-- * Typeclass for SMTLIB2 conversion
, SMTLIB2 (..)
-- * Creating and killing SMTLIB2 Process
, Context (..)
, makeContext
, makeContextNoLog
, makeContextWithSEnv
, cleanupContext
-- * Execute Queries
, command
, smtSetMbqi
-- * Query API
, smtDecl
, smtDecls
, smtDefineFunc
, smtAssert
, smtFuncDecl
, smtAssertAxiom
, smtCheckUnsat
, smtCheckSat
, smtBracket, smtBracketAt
, smtDistinct
, smtPush, smtPop
-- * Check Validity
, checkValid
, checkValid'
, checkValidWithContext
, checkValids
) where
import Language.Fixpoint.Types.Config ( SMTSolver (..), solverFlags
, Config (solver, smtTimeout, gradual, stringTheory, save))
import qualified Language.Fixpoint.Misc as Misc
import Language.Fixpoint.Types.Errors
import Language.Fixpoint.Utils.Files
import Language.Fixpoint.Types hiding (allowHO)
import qualified Language.Fixpoint.Types as F
import Language.Fixpoint.Smt.Types
import qualified Language.Fixpoint.Smt.Theories as Thy
import Language.Fixpoint.Smt.Serialize ()
import Control.Applicative ((<|>))
import Control.Monad
import Control.Exception
import Data.ByteString.Builder (Builder)
import qualified Data.ByteString.Builder as BS
import qualified Data.ByteString.Lazy as LBS
import qualified Data.ByteString.Lazy.Char8 as Char8
import Data.Char
import qualified Data.HashMap.Strict as M
import Data.Maybe (fromMaybe)
import qualified Data.Text as T
import qualified Data.Text.Encoding as TE
import qualified Data.Text.IO
-- import Data.Text.Format
import qualified Data.Text.Lazy.IO as LTIO
import System.Directory
import System.Console.CmdArgs.Verbosity
import System.FilePath
import System.IO
import qualified Data.Attoparsec.Text as A
-- import qualified Data.HashMap.Strict as M
import Data.Attoparsec.Internal.Types (Parser)
import Text.PrettyPrint.HughesPJ (text)
import Language.Fixpoint.SortCheck
import Language.Fixpoint.Utils.Builder as Builder
-- import qualified Language.Fixpoint.Types as F
-- import Language.Fixpoint.Types.PrettyPrint (tracepp)
import qualified SMTLIB.Backends
import qualified SMTLIB.Backends.Process as Process
import qualified Language.Fixpoint.Conditional.Z3 as Conditional.Z3
import Control.Concurrent.Async (async)
{-
runFile f
= readFile f >>= runString
runString str
= runCommands $ rr str
runCommands cmds
= do me <- makeContext Z3
mapM_ (T.putStrLn . smt2) cmds
zs <- mapM (command me) cmds
return zs
-}
checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValidWithContext me xts p q =
smtBracket me "checkValidWithContext" $
checkValid' me xts p q
-- | type ClosedPred E = {v:Pred | subset (vars v) (keys E) }
-- checkValid :: e:Env -> ClosedPred e -> ClosedPred e -> IO Bool
checkValid :: Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid cfg f xts p q = do
me <- makeContext cfg f
checkValid' me xts p q
checkValid' :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' me xts p q = do
smtDecls me xts
smtAssert me $ pAnd [p, PNot q]
smtCheckUnsat me
-- | If you already HAVE a context, where all the variables have declared types
-- (e.g. if you want to make MANY repeated Queries)
-- checkValid :: e:Env -> [ClosedPred e] -> IO [Bool]
checkValids :: Config -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]
checkValids cfg f xts ps
= do me <- makeContext cfg f
smtDecls me xts
forM ps $ \p ->
smtBracket me "checkValids" $
smtAssert me (PNot p) >> smtCheckUnsat me
-- debugFile :: FilePath
-- debugFile = "DEBUG.smt2"
--------------------------------------------------------------------------------
-- | SMT IO --------------------------------------------------------------------
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
{-# SCC command #-}
command :: Context -> Command -> IO Response
--------------------------------------------------------------------------------
command Ctx{..} !cmd = do
-- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
-- LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
forM_ ctxLog $ \h -> do
BS.hPutBuilder h cmdBS
LBS.hPutStr h "\n"
case cmd of
CheckSat -> commandRaw
GetValue _ -> commandRaw
_ -> SMTLIB.Backends.command_ ctxSolver cmdBS >> return Ok
where
commandRaw = do
resp <- SMTLIB.Backends.command ctxSolver cmdBS
let respTxt =
TE.decodeUtf8With (const $ const $ Just ' ') $
LBS.toStrict resp
parse respTxt
cmdBS = {-# SCC "Command-runSmt2" #-} runSmt2 ctxSymEnv cmd
parse resp = do
case A.parseOnly responseP resp of
Left e -> Misc.errorstar $ "SMTREAD:" ++ e
Right r -> do
let textResponse = "; SMT Says: " <> T.pack (show r)
forM_ ctxLog $ \h ->
Data.Text.IO.hPutStrLn h textResponse
when ctxVerbose $
Data.Text.IO.putStrLn textResponse
return r
smtSetMbqi :: Context -> IO ()
smtSetMbqi me = interact' me SetMbqi
type SmtParser a = Parser T.Text a
responseP :: SmtParser Response
responseP = {- SCC "responseP" -} A.char '(' *> sexpP
<|> A.string "sat" *> return Sat
<|> A.string "unsat" *> return Unsat
<|> A.string "unknown" *> return Unknown
sexpP :: SmtParser Response
sexpP = {- SCC "sexpP" -} A.string "error" *> (Error <$> errorP)
<|> Values <$> valuesP
errorP :: SmtParser T.Text
errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")"
valuesP :: SmtParser [(Symbol, T.Text)]
valuesP = A.many1' pairP <* A.char ')'
pairP :: SmtParser (Symbol, T.Text)
pairP = {- SCC "pairP" -}
do A.skipSpace
_ <- A.char '('
!x <- symbolP
A.skipSpace
!v <- valueP
_ <- A.char ')'
return (x,v)
symbolP :: SmtParser Symbol
symbolP = {- SCC "symbolP" -} symbol <$> A.takeWhile1 (not . isSpace)
valueP :: SmtParser T.Text
valueP = {- SCC "valueP" -} negativeP
<|> A.takeWhile1 (\c -> not (c == ')' || isSpace c))
negativeP :: SmtParser T.Text
negativeP
= do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')'
return $ "(" <> v <> ")"
--------------------------------------------------------------------------
-- | SMT Context ---------------------------------------------------------
--------------------------------------------------------------------------
--------------------------------------------------------------------------
makeContext :: Config -> FilePath -> IO Context
--------------------------------------------------------------------------
makeContext cfg f
= do mb_hLog <- if not (save cfg) then pure Nothing else do
createDirectoryIfMissing True $ takeDirectory smtFile
hLog <- openFile smtFile WriteMode
hSetBuffering hLog $ BlockBuffering $ Just $ 1024 * 1024 * 64
return $ Just hLog
me <- makeContext' cfg mb_hLog
pre <- smtPreamble cfg (solver cfg) me
forM_ pre $ \line -> do
SMTLIB.Backends.command_ (ctxSolver me) line
forM_ mb_hLog $ \hLog -> do
BS.hPutBuilder hLog line
LBS.hPutStr hLog "\n"
return me
where
smtFile = extFileName Smt2 f
makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context
makeContextWithSEnv cfg f env = do
ctx <- makeContext cfg f
let ctx' = ctx {ctxSymEnv = env}
declare ctx'
return ctx'
-- where msg = "makeContextWithSEnv" ++ show env
makeContextNoLog :: Config -> IO Context
makeContextNoLog cfg
= do me <- makeContext' cfg Nothing
pre <- smtPreamble cfg (solver cfg) me
mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre
return me
makeProcess
:: Maybe Handle
-> Process.Config
-> IO (SMTLIB.Backends.Backend, IO ())
makeProcess ctxLog cfg
= do handl@Process.Handle {hMaybeErr = Just hErr, ..} <- Process.new cfg
case ctxLog of
Nothing -> return ()
Just hLog -> void $ async $ forever
(do errTxt <- LTIO.hGetLine hErr
LTIO.hPutStrLn hLog $ "OOPS, SMT solver error:" <> errTxt
) `catch` \ SomeException {} -> return ()
let backend = Process.toBackend handl
hSetBuffering hOut $ BlockBuffering $ Just $ 1024 * 1024 * 64
hSetBuffering hIn $ BlockBuffering $ Just $ 1024 * 1024 * 64
return (backend, Process.close handl)
makeContext' :: Config -> Maybe Handle -> IO Context
makeContext' cfg ctxLog
= do let slv = solver cfg
(backend, closeIO) <- case slv of
Z3 ->
{- "z3 -smt2 -in" -}
{- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}
{- "z3 -smtc -in MBQI=false" -}
makeProcess ctxLog $ Process.defaultConfig
{ Process.exe = "z3"
, Process.args = ["-smt2", "-in"] }
Z3mem -> Conditional.Z3.makeZ3
Mathsat -> makeProcess ctxLog $ Process.defaultConfig
{ Process.exe = "mathsat"
, Process.args = ["-input=smt2"] }
Cvc4 -> makeProcess ctxLog $
Process.defaultConfig
{ Process.exe = "cvc4"
, Process.args = ["--incremental", "-L", "smtlib2"] }
Cvc5 -> makeProcess ctxLog $
Process.defaultConfig
{ Process.exe = "cvc5"
, Process.args = ["--incremental", "-L", "smtlib2"] }
solver <- SMTLIB.Backends.initSolver SMTLIB.Backends.Queuing backend
loud <- isLoud
return Ctx { ctxSolver = solver
, ctxElabF = solverFlags slv
, ctxClose = closeIO
, ctxLog = ctxLog
, ctxVerbose = loud
, ctxSymEnv = mempty
}
-- | Close file handles and release the solver backend's resources.
cleanupContext :: Context -> IO ()
cleanupContext Ctx {..} = do
maybe (return ()) (hCloseMe "ctxLog") ctxLog
ctxClose
hCloseMe :: String -> Handle -> IO ()
hCloseMe msg h = hClose h `catch` (\(exn :: IOException) -> putStrLn $ "OOPS, hClose breaks: " ++ msg ++ show exn)
smtPreamble :: Config -> SMTSolver -> Context -> IO [Builder]
smtPreamble cfg s me
| s == Z3 || s == Z3mem
= do v <- getZ3Version me
checkValidStringFlag Z3 v cfg
return $ z3_options ++ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3
| otherwise
= checkValidStringFlag s [] cfg >> return (Thy.preamble cfg s)
getZ3Version :: Context -> IO [Int]
getZ3Version me
= do -- resp is like (:version "4.8.15")
resp <- SMTLIB.Backends.command (ctxSolver me) "(get-info :version)"
case Char8.split '"' resp of
_:rText:_ -> do
-- strip off potential " - build hashcode ..." suffix
let vText = Char8.takeWhile (not . isSpace) rText
let parsedComponents = [ reads (Char8.unpack cText) | cText <- Char8.split '.' vText ]
sequence
[ case pComponent of
[(c, "")] -> return c
xs -> error $ "Can't parse z3 version: " ++ show xs
| pComponent <- parsedComponents
]
xs -> error $ "Can't parse z3 (get-info :version): " ++ show xs
checkValidStringFlag :: SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag smt v cfg
= when (noString smt v cfg) $
die $ err dummySpan (text "stringTheory is only supported by z3 version >=4.2.2")
noString :: SMTSolver -> [Int] -> Config -> Bool
noString smt v cfg
= stringTheory cfg
&& not (smt == Z3 && (v >= [4, 4, 2]))
-----------------------------------------------------------------------------
-- | SMT Commands -----------------------------------------------------------
-----------------------------------------------------------------------------
smtPush, smtPop :: Context -> IO ()
smtPush me = interact' me Push
smtPop me = interact' me Pop
smtDecls :: Context -> [(Symbol, Sort)] -> IO ()
smtDecls = mapM_ . uncurry . smtDecl
smtDecl :: Context -> Symbol -> Sort -> IO ()
smtDecl me x t = interact' me ({- notracepp msg $ -} Declare (symbolSafeText x) ins' out')
where
ins' = sortSmtSort False env <$> ins
out' = sortSmtSort False env out
(ins, out) = deconSort t
_msg = "smtDecl: " ++ showpp (x, t, ins, out)
env = seData (ctxSymEnv me)
smtFuncDecl :: Context -> T.Text -> ([SmtSort], SmtSort) -> IO ()
smtFuncDecl me x (ts, t) = interact' me (Declare x ts t)
smtDataDecl :: Context -> [DataDecl] -> IO ()
smtDataDecl me ds = interact' me (DeclData ds)
deconSort :: Sort -> ([Sort], Sort)
deconSort t = case functionSort t of
Just (_, ins, out) -> (ins, out)
Nothing -> ([], t)
-- hack now this is used only for checking gradual condition.
smtCheckSat :: Context -> Expr -> IO Bool
smtCheckSat me p
= smtAssert me p >> (ans <$> command me CheckSat)
where
ans Sat = True
ans _ = False
smtAssert :: Context -> Expr -> IO ()
smtAssert me p = interact' me (Assert Nothing p)
smtDefineFunc :: Context -> Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> IO ()
smtDefineFunc me name symList rsort e =
let env = seData (ctxSymEnv me)
in interact' me $
DefineFunc
name
(map (sortSmtSort False env <$>) symList)
(sortSmtSort False env rsort)
e
-----------------------------------------------------------------
smtAssertAxiom :: Context -> Triggered Expr -> IO ()
smtAssertAxiom me p = interact' me (AssertAx p)
smtDistinct :: Context -> [Expr] -> IO ()
smtDistinct me az = interact' me (Distinct az)
smtCheckUnsat :: Context -> IO Bool
smtCheckUnsat me = respSat <$> command me CheckSat
smtBracketAt :: SrcSpan -> Context -> String -> IO a -> IO a
smtBracketAt sp x y z = smtBracket x y z `catch` dieAt sp
smtBracket :: Context -> String -> IO a -> IO a
smtBracket me _msg a = do
smtPush me
r <- a
smtPop me
return r
respSat :: Response -> Bool
respSat Unsat = True
respSat Sat = False
respSat Unknown = False
respSat r = die $ err dummySpan $ text ("crash: SMTLIB2 respSat = " ++ show r)
interact' :: Context -> Command -> IO ()
interact' me cmd = void $ command me cmd
makeTimeout :: Config -> [Builder]
makeTimeout cfg
| Just i <- smtTimeout cfg = [ "\n(set-option :timeout " <> fromString (show i) <> ")\n"]
| otherwise = [""]
makeMbqi :: Config -> [Builder]
makeMbqi cfg
| gradual cfg = [""]
| otherwise = ["\n(set-option :smt.mbqi false)"]
z3_options :: [Builder]
z3_options
= [ "(set-option :auto-config false)"
, "(set-option :model true)" ]
--------------------------------------------------------------------------------
declare :: Context -> IO ()
--------------------------------------------------------------------------------
declare me = do
forM_ dss $ smtDataDecl me
forM_ thyXTs $ uncurry $ smtDecl me
forM_ qryXTs $ uncurry $ smtDecl me
forM_ ats $ uncurry $ smtFuncDecl me
forM_ ess $ smtDistinct me
forM_ axs $ smtAssert me
where
env = ctxSymEnv me
dss = dataDeclarations env
lts = F.toListSEnv . F.seLits $ env
ess = distinctLiterals lts
axs = Thy.axiomLiterals lts
thyXTs = filter (isKind 1) xts
qryXTs = fmap tx <$> filter (isKind 2) xts
isKind n = (n ==) . symKind env . fst
xts = {- tracepp "symbolSorts" $ -} symbolSorts (F.seSort env)
tx = elaborate (ElabParam (ctxElabF me) "declare" env)
ats = funcSortVars env
symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)]
symbolSorts env = [(x, tx t) | (x, t) <- F.toListSEnv env ]
where
tx t@(FObj a) = fromMaybe t (F.lookupSEnv a env)
tx t = t
dataDeclarations :: SymEnv -> [[DataDecl]]
dataDeclarations = orderDeclarations . map snd . F.toListSEnv . F.seData
funcSortVars :: F.SymEnv -> [(T.Text, ([F.SmtSort], F.SmtSort))]
funcSortVars env = [(var applyName t , appSort t) | t <- ts]
++ [(var coerceName t , ([t1],t2)) | t@(t1, t2) <- ts]
++ [(var lambdaName t , lamSort t) | t <- ts]
++ [(var (lamArgSymbol i) t , argSort t) | t@(_,F.SInt) <- ts, i <- [1..Thy.maxLamArg] ]
where
var n = F.symbolAtSmtName n env ()
ts = M.keys (F.seAppls env)
appSort (s,t) = ([F.SInt, s], t)
lamSort (s,t) = ([s, t], F.SInt)
argSort (s,_) = ([] , s)
-- | 'symKind' returns {0, 1, 2} where:
-- 0 = Theory-Definition,
-- 1 = Theory-Declaration,
-- 2 = Query-Binder
symKind :: F.SymEnv -> F.Symbol -> Int
symKind env x = case F.tsInterp <$> F.symEnvTheory x env of
Just F.Theory -> 0
Just F.Ctor -> 0
Just F.Test -> 0
Just F.Field -> 0
Just F.Uninterp -> 1
Nothing -> 2
-- Just t -> if tsInterp t then 0 else 1
-- assumes :: [F.Expr] -> SolveM ()
-- assumes es = withContext $ \me -> forM_ es $ smtAssert me
-- | `distinctLiterals` is used solely to determine the set of literals
-- (of each sort) that are *disequal* to each other, e.g. EQ, LT, GT,
-- or string literals "cat", "dog", "mouse". These should only include
-- non-function sorted values.
distinctLiterals :: [(F.Symbol, F.Sort)] -> [[F.Expr]]
distinctLiterals xts = [ es | (_, es) <- tess ]
where
tess = Misc.groupList [(t, F.expr x) | (x, t) <- xts, notFun t]
notFun = not . F.isFunctionSortedReft . (`F.RR` F.trueReft)
-- _notStr = not . (F.strSort ==) . F.sr_sort . (`F.RR` F.trueReft)