liquid-fixpoint-8.10.7: src/Language/Fixpoint/Smt/Interface.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
-- | 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
-- Note [Async SMT API]
--
-- The SMT solver is started in a separate process and liquid-fixpoint
-- communicates with it via pipes. This mechanism introduces some latency
-- since the queries need to reach the buffers in a separate process and
-- the OS has to switch contexts.
--
-- A remedy we currently try for this is to send multiple queries
-- together without waiting for the reply to each one, i.e. asynchronously.
-- We then collect the multiple answers after sending all of the queries.
--
-- The functions named @smt*Async@ implement this scheme.
--
-- An asynchronous thread is used to write the queries to prevent the
-- caller from blocking on IO, should the write buffer be full or should
-- an 'hFlush' call be necessary.
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
, smtExit
, smtSetMbqi
-- * Query API
, smtDecl
, smtDecls
, smtDefineFunc
, smtAssert
, smtFuncDecl
, smtAssertAxiom
, smtCheckUnsat
, smtCheckSat
, smtBracket, smtBracketAt
, smtDistinct
, smtPush, smtPop
, smtAssertAsync
, smtCheckUnsatAsync
, readCheckUnsat
, smtBracketAsyncAt
, smtPushAsync
, smtPopAsync
-- * Check Validity
, checkValid
, checkValid'
, checkValidWithContext
, checkValids
) where
import Control.Concurrent.Async (async, cancel)
import Control.Concurrent.STM
(TVar, atomically, modifyTVar, newTVarIO, readTVar, retry, writeTVar)
import Language.Fixpoint.Types.Config ( SMTSolver (..)
, Config
, solver
, smtTimeout
, gradual
, stringTheory)
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.Char
import qualified Data.HashMap.Strict as M
import Data.Maybe (fromMaybe)
#if !MIN_VERSION_base(4,14,0)
import Data.Semigroup (Semigroup (..))
#endif
import qualified Data.Text as T
-- import Data.Text.Format
import qualified Data.Text.IO as TIO
import qualified Data.Text.Lazy as LT
import qualified Data.Text.Lazy.IO as LTIO
import System.Directory
import System.Console.CmdArgs.Verbosity
import System.Exit hiding (die)
import System.FilePath
import System.IO
import System.Process
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)
{-
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 me !cmd = say >> hear cmd
where
env = ctxSymEnv me
say = smtWrite me ({-# SCC "Command-runSmt2" #-} Builder.toLazyText (runSmt2 env cmd))
hear CheckSat = smtRead me
hear (GetValue _) = smtRead me
hear _ = return Ok
smtExit :: Context -> IO ()
smtExit me = asyncCommand me Exit
smtSetMbqi :: Context -> IO ()
smtSetMbqi me = asyncCommand me SetMbqi
smtWrite :: Context -> Raw -> IO ()
smtWrite me !s = smtWriteRaw me s
smtRead :: Context -> IO Response
smtRead me = {- SCC "smtRead" #-} do
when (ctxVerbose me) $ LTIO.putStrLn "SMT READ"
ln <- smtReadRaw me
res <- A.parseWith (smtReadRaw me) responseP ln
case A.eitherResult res of
Left e -> Misc.errorstar $ "SMTREAD:" ++ e
Right r -> do
maybe (return ()) (\h -> LTIO.hPutStrLn h $ blt ("; SMT Says: " <> (bShow r))) (ctxLog me)
when (ctxVerbose me) $ LTIO.putStrLn $ blt ("SMT Says: " <> bShow r)
return r
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 <> ")"
smtWriteRaw :: Context -> Raw -> IO ()
smtWriteRaw me !s = {- SCC "smtWriteRaw" #-} do
-- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
-- LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
hPutStrLnNow (ctxCout me) s
maybe (return ()) (`LTIO.hPutStrLn` s) (ctxLog me)
smtReadRaw :: Context -> IO T.Text
smtReadRaw me = {- SCC "smtReadRaw" #-} TIO.hGetLine (ctxCin me)
{-# SCC smtReadRaw #-}
hPutStrLnNow :: Handle -> LT.Text -> IO ()
hPutStrLnNow h !s = LTIO.hPutStrLn h s >> hFlush h
{-# SCC hPutStrLnNow #-}
--------------------------------------------------------------------------
-- | SMT Context ---------------------------------------------------------
--------------------------------------------------------------------------
--------------------------------------------------------------------------
makeContext :: Config -> FilePath -> IO Context
--------------------------------------------------------------------------
makeContext cfg f
= do me <- makeProcess cfg
pre <- smtPreamble cfg (solver cfg) me
createDirectoryIfMissing True $ takeDirectory smtFile
hLog <- openFile smtFile WriteMode
hSetBuffering hLog $ BlockBuffering $ Just $ 1024*1024*64
let me' = me { ctxLog = Just hLog }
mapM_ (smtWrite me') pre
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 <- makeProcess cfg
pre <- smtPreamble cfg (solver cfg) me
mapM_ (smtWrite me) pre
return me
makeProcess :: Config -> IO Context
makeProcess cfg
= do (hOut, hIn, _ ,pid) <- runInteractiveCommand $ smtCmd (solver cfg)
loud <- isLoud
hSetBuffering hOut $ BlockBuffering $ Just $ 1024*1024*64
hSetBuffering hIn $ BlockBuffering $ Just $ 1024*1024*64
-- See Note [Async SMT API]
queueTVar <- newTVarIO mempty
writerAsync <- async $ forever $ do
t <- atomically $ do
builder <- readTVar queueTVar
let t = Builder.toLazyText builder
when (LT.null t) retry
writeTVar queueTVar mempty
return t
LTIO.hPutStr hOut t
hFlush hOut
return Ctx { ctxPid = pid
, ctxCin = hIn
, ctxCout = hOut
, ctxLog = Nothing
, ctxVerbose = loud
, ctxSymEnv = mempty
, ctxAsync = writerAsync
, ctxTVar = queueTVar
}
--------------------------------------------------------------------------
cleanupContext :: Context -> IO ExitCode
--------------------------------------------------------------------------
cleanupContext (Ctx {..}) = do
cancel ctxAsync
hCloseMe "ctxCin" ctxCin
hCloseMe "ctxCout" ctxCout
maybe (return ()) (hCloseMe "ctxLog") ctxLog
waitForProcess ctxPid
hCloseMe :: String -> Handle -> IO ()
hCloseMe msg h = hClose h `catch` (\(exn :: IOException) -> putStrLn $ "OOPS, hClose breaks: " ++ msg ++ show exn)
{- "z3 -smt2 -in" -}
{- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}
{- "z3 -smtc -in MBQI=false" -}
smtCmd :: SMTSolver -> String -- T.Text
smtCmd Z3 = "z3 -smt2 -in"
smtCmd Mathsat = "mathsat -input=smt2"
smtCmd Cvc4 = "cvc4 --incremental -L smtlib2"
-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
smtPreamble :: Config -> SMTSolver -> Context -> IO [LT.Text]
smtPreamble cfg Z3 me
= do smtWrite me "(get-info :version)"
v:_ <- T.words . (!!1) . T.splitOn "\"" <$> smtReadRaw me
checkValidStringFlag Z3 v cfg
if T.splitOn "." v `versionGreaterEq` ["4", "3", "2"]
then return $ z3_432_options ++ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3
else return $ z3_options ++ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3
smtPreamble cfg s _
= checkValidStringFlag s "" cfg >> return (Thy.preamble cfg s)
checkValidStringFlag :: SMTSolver -> T.Text -> 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 -> T.Text -> Config -> Bool
noString smt v cfg
= stringTheory cfg
&& not (smt == Z3 && (T.splitOn "." v `versionGreaterEq` ["4", "4", "2"]))
versionGreaterEq :: Ord a => [a] -> [a] -> Bool
versionGreaterEq (x:xs) (y:ys)
| x > y = True
| x == y = versionGreaterEq xs ys
| x < y = False
versionGreaterEq _ [] = True
versionGreaterEq [] _ = False
versionGreaterEq _ _ = Misc.errorstar "Interface.versionGreater called with bad arguments"
-----------------------------------------------------------------------------
-- | 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 params rsort e =
let env = seData (ctxSymEnv me)
in interact' me $
DefineFunc
name
(map (sortSmtSort False env <$>) params)
(sortSmtSort False env rsort)
e
-----------------------------------------------------------------
-- Async calls to the smt
--
-- See Note [Async SMT API]
-----------------------------------------------------------------
asyncCommand :: Context -> Command -> IO ()
asyncCommand me cmd = do
let env = ctxSymEnv me
cmdText = {-# SCC "asyncCommand-runSmt2" #-} Builder.toLazyText $ runSmt2 env cmd
asyncPutStrLn (ctxTVar me) cmdText
maybe (return ()) (`LTIO.hPutStrLn` cmdText) (ctxLog me)
where
asyncPutStrLn :: TVar Builder.Builder -> LT.Text -> IO ()
asyncPutStrLn tv t = atomically $
modifyTVar tv (`mappend` (Builder.fromLazyText t `mappend` Builder.fromString "\n"))
smtAssertAsync :: Context -> Expr -> IO ()
smtAssertAsync me p = asyncCommand me $ Assert Nothing p
smtCheckUnsatAsync :: Context -> IO ()
smtCheckUnsatAsync me = asyncCommand me CheckSat
smtBracketAsyncAt :: SrcSpan -> Context -> String -> IO a -> IO a
smtBracketAsyncAt sp x y z = smtBracketAsync x y z `catch` dieAt sp
smtBracketAsync :: Context -> String -> IO a -> IO a
smtBracketAsync me _msg a = do
smtPushAsync me
r <- a
smtPopAsync me
return r
smtPushAsync, smtPopAsync :: Context -> IO ()
smtPushAsync me = asyncCommand me Push
smtPopAsync me = asyncCommand me Pop
-----------------------------------------------------------------
{-# SCC readCheckUnsat #-}
readCheckUnsat :: Context -> IO Bool
readCheckUnsat me = respSat <$> smtRead me
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 -> [LT.Text]
makeTimeout cfg
| Just i <- smtTimeout cfg = [ LT.pack ("\n(set-option :timeout " ++ (show i) ++ ")\n")]
| otherwise = [""]
makeMbqi :: Config -> [LT.Text]
makeMbqi cfg
| gradual cfg = [""]
| otherwise = ["\n(set-option :smt.mbqi false)"]
-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
z3_432_options :: [LT.Text]
z3_432_options
= [ "(set-option :auto-config false)"
, "(set-option :model true)"
, "(set-option :model.partial false)"]
z3_options :: [LT.Text]
z3_options
= [ "(set-option :auto-config false)"
, "(set-option :model true)"
, "(set-option :model-partial false)"]
--------------------------------------------------------------------------------
declare :: Context -> IO () -- SolveM ()
--------------------------------------------------------------------------------
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 = Misc.mapSnd tx <$> filter (isKind 2) xts
isKind n = (n ==) . symKind env . fst
xts = {- tracepp "symbolSorts" $ -} symbolSorts (F.seSort env)
tx = elaborate "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)