diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,30 @@ -# v0.2 -- make test-suite compatible with `smtlib-backends-0.2` +# Changelog + +All notable changes to the smtlib-backends-z3 library will be documented in this +file. + +## v0.3 _(2023-02-03)_ + +### Added +- add `Z3.defaultConfig` +- add tests for documenting edge cases of the backends + - what happens when sending an empty command + - what happens when sending a command not producing any output +- **(breaking change)** removed `Data.Default` instance of `Config` + +### Changed +- make test-suite compatible with `smtlib-backends-0.3` +- **(breaking change)** the `Z3.new` and `Z3.with` functions now take a + `Z3.Config` object as argument, which one may use to set some solver options + at initialization time + - add corresponding examples in the test-suite +- dropped dependency on `inline-c` +- removed `Data.Default` instance for `Config` + +## v0.2 _(2022-12-16)_ + +### Added - add usage examples in the test-suite + +### Changed +- make test-suite compatible with `smtlib-backends-0.2` diff --git a/cbits/z3.c b/cbits/z3.c new file mode 100644 --- /dev/null +++ b/cbits/z3.c @@ -0,0 +1,5 @@ +#include "z3.h" + +// This prototype causes compilation to fail if the type +// of Z3_eval_smtlib2_string changes. +const char* Z3_eval_smtlib2_string(Z3_context ctx, const char* cmd); diff --git a/smtlib-backends-z3.cabal b/smtlib-backends-z3.cabal --- a/smtlib-backends-z3.cabal +++ b/smtlib-backends-z3.cabal @@ -1,5 +1,5 @@ name: smtlib-backends-z3 -version: 0.2 +version: 0.3 synopsis: An SMT-LIB backend implemented using Z3's C API. description: This library implements an SMT-LIB backend (in the sense of the smtlib-backends @@ -24,19 +24,18 @@ source-repository this type: git location: https://github.com/tweag/smtlib-backends - tag: 0.2 + tag: 0.3 subdir: smtlib-backends-z3 library hs-source-dirs: src + c-sources: cbits/z3.c ghc-options: -Wall -Wunused-packages exposed-modules: SMTLIB.Backends.Z3 build-depends: - base >=4.14 && <4.17.0 - , bytestring >=0.10.12 && <0.11 - , containers >=0.6.4 && <0.7 - , inline-c >=0.9.1 && <0.10 - , smtlib-backends >=0.2 && <0.3 + base >=4.14 && <4.18 + , bytestring >=0.10.12 && <0.12 + , smtlib-backends >=0.3 && <0.4 -- inspired from haskell-z3 if (os(osx) || os(windows)) @@ -54,7 +53,10 @@ type: exitcode-stdio-1.0 hs-source-dirs: tests main-is: Main.hs - other-modules: Examples + other-modules: + EdgeCases + Examples + ghc-options: -threaded -Wall -Wunused-packages build-depends: base diff --git a/src/SMTLIB/Backends/Z3.hs b/src/SMTLIB/Backends/Z3.hs --- a/src/SMTLIB/Backends/Z3.hs +++ b/src/SMTLIB/Backends/Z3.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CApiFFI #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE QuasiQuotes #-} @@ -5,7 +6,9 @@ -- | A module providing a backend that sends commands to Z3 using its C API. module SMTLIB.Backends.Z3 - ( Handle, + ( Config (..), + Handle, + defaultConfig, new, close, with, @@ -14,66 +17,77 @@ where import Control.Exception (bracket) +import Control.Monad (forM_, void) +import qualified Data.ByteString as BS import Data.ByteString.Builder.Extra ( defaultChunkSize, smallChunkSize, toLazyByteStringWith, untrimmedStrategy, ) -import qualified Data.ByteString.Char8 as BS import qualified Data.ByteString.Lazy.Char8 as LBS -import qualified Data.Map as M -import Foreign.ForeignPtr (ForeignPtr, finalizeForeignPtr, newForeignPtr) -import Foreign.Ptr (Ptr) -import qualified Language.C.Inline as C -import qualified Language.C.Inline.Context as C -import qualified Language.C.Inline.Unsafe as CU -import qualified Language.C.Types as C +import qualified Data.ByteString.Unsafe +import Foreign.C.String (CString) +import Foreign.ForeignPtr (ForeignPtr, finalizeForeignPtr, newForeignPtr, withForeignPtr) +import Foreign.Ptr (FunPtr, Ptr, nullPtr) import SMTLIB.Backends (Backend (..)) -data LogicalContext +data Z3Context -C.context - ( C.baseCtx - <> C.fptrCtx - <> C.bsCtx - <> mempty - { C.ctxTypesTable = - M.singleton (C.TypeName "Z3_context") [t|Ptr LogicalContext|] - } - ) -C.include "z3.h" +data Z3Config -data Handle = Handle +newtype Config = Config + { -- | A list of options to set during the solver's initialization. + -- Each pair is of the form @(paramId, paramValue)@, e.g. + -- @(":produce-models", "true")@. + parameters :: [(BS.ByteString, BS.ByteString)] + } + +-- | By default, don't set any options during initialization. +defaultConfig :: Config +defaultConfig = Config [] + +newtype Handle = Handle { -- | A black-box representing the internal state of the solver. - context :: ForeignPtr LogicalContext + context :: ForeignPtr Z3Context } --- | Create a new solver instance. -new :: IO Handle -new = do - let ctxFinalizer = - [C.funPtr| void free_context(Z3_context ctx) { - Z3_del_context(ctx); - } |] +foreign import capi unsafe "z3.h &Z3_del_context" c_Z3_del_context :: FunPtr (Ptr Z3Context -> IO ()) +foreign import capi unsafe "z3.h Z3_set_param_value" c_Z3_set_param_value :: Ptr Z3Config -> CString -> CString -> IO () + +foreign import capi unsafe "z3.h Z3_mk_config" c_Z3_mk_config :: IO (Ptr Z3Config) + +foreign import capi unsafe "z3.h Z3_mk_context" c_Z3_mk_context :: Ptr Z3Config -> IO (Ptr Z3Context) + +foreign import capi unsafe "z3.h Z3_del_config" c_Z3_del_config :: Ptr Z3Config -> IO () + +foreign import capi unsafe "z3.h Z3_set_error_handler" c_Z3_set_error_handler :: Ptr Z3Context -> Ptr () -> IO () + +-- We use ccall to avoid warnings about constness in the C side +-- In the meantime we check in cbits/z3.c that the type of the function is +-- compatible. +foreign import ccall unsafe "z3.h Z3_eval_smtlib2_string" c_Z3_eval_smtlib2_string :: Ptr Z3Context -> CString -> IO CString + +-- | Create a new solver instance. +new :: Config -> IO Handle +new config = do + -- we don't set a finalizer for this object as we manually delete it during the + -- context's creation + cfg <- c_Z3_mk_config + forM_ (parameters config) $ \(paramId, paramValue) -> + BS.useAsCString paramId $ \cparamId -> + BS.useAsCString paramValue $ \cparamValue -> + c_Z3_set_param_value cfg cparamId cparamValue {- We set the error handler to ignore errors. That way if an error happens it doesn't cause the whole program to crash, and the error message is simply transmitted to the Haskell layer inside the output of the 'send' method. -} - ctx <- - newForeignPtr ctxFinalizer - =<< [CU.block| Z3_context { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_del_config(cfg); - - void ignore_error(Z3_context c, Z3_error_code e) {} - Z3_set_error_handler(ctx, ignore_error); - - return ctx; - } |] + pctx <- c_Z3_mk_context cfg + c_Z3_del_config cfg + c_Z3_set_error_handler pctx nullPtr + ctx <- newForeignPtr c_Z3_del_context pctx return $ Handle ctx -- | Release the resources associated with a Z3 instance. @@ -81,23 +95,24 @@ close = finalizeForeignPtr . context -- | Create a Z3 instance, use it to run a computation and release its resources. -with :: (Handle -> IO a) -> IO a -with = bracket new close +with :: Config -> (Handle -> IO a) -> IO a +with config = bracket (new config) close -- | Create a solver backend out of a Z3 instance. toBackend :: Handle -> Backend -toBackend handle = - Backend $ \cmd -> do - let ctx = context handle - let cmd' = - LBS.toStrict $ - toLazyByteStringWith - (untrimmedStrategy smallChunkSize defaultChunkSize) - "\NUL" - cmd - LBS.fromStrict - <$> ( BS.packCString - =<< [CU.exp| const char* { - Z3_eval_smtlib2_string($fptr-ptr:(Z3_context ctx), $bs-ptr:cmd') - }|] - ) +toBackend handle = Backend backendSend backendSend_ + where + backendSend cmd = do + let ctx = context handle + let cmd' = + LBS.toStrict $ + toLazyByteStringWith + (untrimmedStrategy smallChunkSize defaultChunkSize) + "\NUL" + cmd + Data.ByteString.Unsafe.unsafeUseAsCString cmd' $ \ccmd' -> + withForeignPtr ctx $ \pctx -> do + resp <- c_Z3_eval_smtlib2_string pctx ccmd' + LBS.fromStrict <$> BS.packCString resp + + backendSend_ = void . backendSend diff --git a/tests/EdgeCases.hs b/tests/EdgeCases.hs new file mode 100644 --- /dev/null +++ b/tests/EdgeCases.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE OverloadedStrings #-} + +module EdgeCases (edgeCases) where + +import Data.ByteString.Builder (Builder) +import SMTLIB.Backends as SMT +import qualified SMTLIB.Backends.Z3 as Z3 +import Test.Tasty +import Test.Tasty.HUnit + +edgeCases :: [TestTree] +edgeCases = + [ testCase "Sending an empty command" emptyCommand, + testCase "Sending a command expecting no response" commandNoResponse + ] + +-- | Upon processing an empty command, the backend will respond with an empty output. +emptyCommand :: IO () +emptyCommand = checkEmptyResponse "" + +-- | Upon processing a command producing no output, the backend will respond +-- with an empty output. +commandNoResponse :: IO () +commandNoResponse = checkEmptyResponse "(set-option :print-success false)" + +checkEmptyResponse :: Builder -> IO () +checkEmptyResponse cmd = Z3.with Z3.defaultConfig $ \handle -> do + let backend = Z3.toBackend handle + response <- SMT.send backend cmd + assertEqual "expected no response" "" response diff --git a/tests/Examples.hs b/tests/Examples.hs --- a/tests/Examples.hs +++ b/tests/Examples.hs @@ -2,7 +2,8 @@ module Examples (examples) where -import SMTLIB.Backends (command, initSolver) +import qualified Data.ByteString.Lazy.Char8 as LBS +import SMTLIB.Backends (QueuingFlag (..), command, command_, flushQueue, initSolver) import qualified SMTLIB.Backends.Z3 as Z3 import Test.Tasty import Test.Tasty.HUnit @@ -10,20 +11,67 @@ -- | The examples for the 'Z3' backend (using Z3 as a library). examples :: [TestTree] examples = - [testCase "basic use" basicUse] + [ testCase "basic use" basicUse, + testCase "setting options" settingOptions, + testCase "flushing the queue" flushing + ] -- | Basic use of the 'Z3' backend. basicUse :: IO () basicUse = -- 'Z3.with' runs a computation using the 'Z3' backend - Z3.with $ \handle -> do + -- it takes a configuration object as argument, whose use we describe in + -- 'settingOptions' + -- here we just use the default configuration, literally @'Z3.Config' []@ + Z3.with Z3.defaultConfig $ \handle -> do -- first, we make the z3 handle into an actual backend let backend = Z3.toBackend handle -- then, we create a solver out of the backend -- we enable queuing (it's faster !) - solver <- initSolver backend True + solver <- initSolver Queuing backend -- we send a basic command to the solver and ignore the response -- we can write the command as a simple string because we have enabled the -- OverloadedStrings pragma _ <- command solver "(get-info :name)" return () + +-- | How to set options at initialization time. +settingOptions :: IO () +settingOptions = + -- the Z3 C API is special (as a backend) in that some of its options can only be + -- set when the object representing the state of the solver is created + -- hence the 'Z3.new' and 'Z3.with' functions allow for setting options at + -- initialization time + Z3.with Z3.defaultConfig + -- (Z3.Config [(":produce-unsat-cores", "true")]) + $ + \handle -> do + -- we don't enable queuing so that commands are checked for correctness + solver <- initSolver NoQueuing (Z3.toBackend handle) + -- this is for example the case of the @:produce-assertions@ parameter, and not + -- the case of the @:print-success@ one + command_ solver "(set-option :print-success true)" + -- the following would fail, returning + -- @ + -- (error "line 1 column 33: error setting ':produce-unsat-cores', + -- option value cannot be modified after initialization") + -- @ + result <- command solver "(set-option :produce-unsat-cores true)" + assertBool ("Expecting error message, got: " ++ LBS.unpack result) $ "(error" `LBS.isPrefixOf` result + return () + +-- | An example on how to force the content of the queue to be evaluated. +flushing :: IO () +flushing = do + -- sometimes you want to use 'Queuing' mode but still force some commands not + -- producing any output to be evaluated + -- in that case, using 'command' would lead to your program hanging as it waits + -- for a response from the solver that never comes + -- the solution is to use the 'command_' function and then to flush the queue + Z3.with Z3.defaultConfig $ \handle -> do + -- this example only makes sense in queuing mode + solver <- initSolver Queuing $ Z3.toBackend handle + -- add a command to the queue + command_ solver "(assert true)" + -- force the queue to be evaluated + flushQueue solver diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,6 +1,7 @@ {-# LANGUAGE OverloadedStrings #-} import qualified Data.ByteString.Lazy.Char8 as LBS +import EdgeCases (edgeCases) import Examples (examples) import SMTLIB.Backends import SMTLIB.Backends.Tests @@ -11,13 +12,15 @@ main :: IO () main = do defaultMain $ - testGroup "Tests" $ + testGroup + "Tests" [ testBackend "Basic examples" validSources z3, testGroup "API usage examples" examples, - testBackend "Error handling" failingSources z3 + testBackend "Error handling" failingSources z3, + testGroup "Edge cases" edgeCases ] where - z3 todo = Z3.with $ todo . Z3.toBackend + z3 todo = Z3.with Z3.defaultConfig $ todo . Z3.toBackend validSources = filter (\source -> name source `notElem` ["assertions", "unsat cores"]) sources failingSources = [ Source "invalid command" $ \solver -> do