smtlib-backends-z3 0.2 → 0.3

raw patch · 7 files changed

+205/−75 lines, 7 filesdep −containersdep −inline-cdep ~basedep ~smtlib-backendsPVP ok

version bump matches the API change (PVP)

Dependencies removed: containers, inline-c

Dependency ranges changed: base, smtlib-backends

API changes (from Hackage documentation)

Files

• CHANGELOG.md +29/−2
• cbits/z3.c +5/−0
• smtlib-backends-z3.cabal +10/−8
• src/SMTLIB/Backends/Z3.hs +73/−58
• tests/EdgeCases.hs +30/−0
• tests/Examples.hs +52/−4
• tests/Main.hs +6/−3

@@ -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`

@@ -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);

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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